theory Auto_Proof_Demo imports Main begin section{* Logic and sets *} lemma "ALL x. EX y. x=y" by auto lemma "A \ B \ C \ A \ B \ C" by auto text{* Note the bounded quantification notation: *} lemma "\ \xs \ A. \ys. xs = ys @ ys; us:A \ \ \n. length us = n+n" by fastforce text{* Most simple proofs in FOL and set theory are automatic. Example: if T is total, A is antisymmetric and T is a subset of A, then A is a subset of T. *} lemma AT: "\ \x y. T x y \ T y x; \x y. A x y \ A y x \ x = y; \x y. T x y \ A x y \ \ \x y. A x y \ T x y" by blast section{* Sledgehammer *} lemma "R^* \ (R \ S)^*" oops lemma "a # xs = ys @ [a] \ P" oops lemma "xs @ ys = ys @ xs \ P" oops section{* Arithmetic *} lemma "\ (k::nat) > 7. \ i j. k = 3*i + 5*j" by arith end