1 theory ProofAutomation

     2 imports Main

     3 begin

     4 

     5 lemma "\<forall>x. \<exists>y. x = y"

     6 by auto

     7 

     8 lemma "A \<subseteq> B \<inter> C \<Longrightarrow> A \<subseteq> B \<union> C"

     9 by auto

    10 

    11 lemma "\<lbrakk> \<forall> xs \<in> A. \<exists> ys. xs = ys @ ys; us \<in> A \<rbrakk> \<Longrightarrow> \<exists>n. length us = n+n"

    12 by fastforce

    13 

    14 lemma "\<lbrakk>xs @ ys = ys @ xs; length xs = length ys \<rbrakk> \<Longrightarrow> xs = ys"

    15 by auto

    16 

    17 lemma "\<lbrakk> (a::nat) \<le> x + b; 2*x < c\<rbrakk> \<Longrightarrow> 2*a + 1 \<le> 2*b + c"

    18 by arith

    19 

    20 lemma "\<lbrakk> (a::nat) \<le> b; b \<le> c; c \<le> d; d \<le> e \<rbrakk> \<Longrightarrow> a \<le> e"

    21 by (blast intro: le_trans)

    22 

    23 lemma "Suc(Suc(Suc a)) \<le> b \<Longrightarrow> a \<le> b"

    24 by(blast dest: Suc_leD)

    25 

    26 inductive ev :: "nat \<Rightarrow> bool" where

    27 ev0: "ev 0" |

    28 evSS: "ev n \<Longrightarrow> ev (n + 2)"

    29 

    30 fun even :: "nat \<Rightarrow> bool" where

    31 "even 0 = True" |

    32 "even (Suc 0) = False" |

    33 "even (Suc(Suc n)) = even n"

    34 

    35 lemma "ev m \<Longrightarrow> even m"

    36