theory Demo = Main:

(*** Forward proofs: ***)

thm conjunct1

lemma "A & B ==> ~~A"
apply(drule conjunct1)
by blast

lemma "A & B ==> B & A"
apply(frule conjunct1)
apply(drule conjunct2)
by blast;

(* with instantiation: *)
lemma "[| A & B; C & D |] ==> ~~C"
apply(drule_tac P = C in conjunct1)
by blast;
(* similar: frule_tac *)

(** Combining theorems **)

lemma AAA: "A --> A&A"
by(blast);

(* translation of --> into ==>: *)
thm mp
thm mp[OF AAA]
thm AAA[THEN mp];

(* you can give new lemmas a name: *)
lemmas aaa =  AAA[THEN mp];
thm aaa

lemma contrived: "ALL x. A x --> A x & True"
by blast

thm spec
thm contrived[THEN spec, THEN mp];

(* rule_format is shorter: *)
lemma quicker[rule_format]: "ALL x. A x --> A x & True"
by blast;

(* forward reasoning with multiple/specific premises: *)
thm trans sym
thm trans[OF sym sym]
thm trans[OF _   sym];


(** explicit substitution. Important for nonterminating equations! **)

thm lfp_unfold

lemma "lfp f = xxx"
apply(subst lfp_unfold)
oops;


(*** Sets. Type 'a set ***)

(* is element of: *)
lemma "a : {a}"
by(blast)

(* is not element of: *)
lemma "a ~= b ==> a ~: {b}"
by(blast)

(* inserting a single element: *)
lemma "insert a (insert b A) = insert b (insert a A)"
by(blast)

(* binary union and intersection *)
lemma "{a,b} Un {c,d} = {a,c} Un {d,b}"
by(blast)

lemma "A Int B = B Int A"
by(blast)

(* difference: *)
lemma "(A Un B) - C = A-C Un B-C"
by(blast)

(* complement: *)
lemma "-(A Un B) = (-A Int -B)"
by(blast)

(* set comprehension: *)
lemma "{x . P x & Q x} = {x . P x} Int {x. Q x}"
by(blast)

(* the set of all elements (of a given type!): *)
lemma "UNIV = {x. True}"
by(blast)

(* big union and intersection of a set of sets: *)
(* Union, Inter :: 'a set set => 'a set *)

lemma "Union{A. A <= M} = M"
by(blast)

lemma "Inter{A. A <= M} = {}"
by(blast)

(* Indexed union and intersection: *)
lemma "(UN n::nat. {i. i <= n}) = UNIV"
by(blast)

lemma "(UN a:A. M a Un N a) = (UN a:A. M a) Un (UN a:A. N a)"
by(blast)

lemma "(INT n::nat. {i. i <= n}) = {0}"
by(blast)

lemma "(INT a:A. M a Int N a) = (INT a:A. M a) Int (INT a:A. N a)"
by(blast)

(* If you have to do things by hand, you must find the necessary rules.
   The following ones should be helpful:
*)

thm subset_antisym
thm subsetI

(* An example: *)

lemma "A Un B = B Un A"
apply(rule subset_antisym)
 apply(rule subsetI)
 apply(erule UnE)
  apply(rule UnI2)
  apply(assumption)
 apply(rule UnI1)
 apply(assumption)
apply(rule subsetI)
apply(erule UnE)
 apply(rule UnI2)
 apply(assumption)
apply(rule UnI1)
apply(assumption)
done

(*** Further useful tactics ***)

(* clarify: performs the obvious logical steps *)

lemma "(EX x. P x) & (EX x. Q x) \<longrightarrow> (EX x. P x & Q x)"
apply clarify
oops

(* clarsimp: interleaves clarify with simp: *)
lemma "ALL ys. (EX ys. xs = ys@ys) & P xs \<longrightarrow> Q ys"
apply clarsimp;
oops

(* fast: similar to blast, in general slower and less powerful,
         but in special situations better than blast *)
(* fast (but not blast!) fails if P(f a) is replaced by P(f(f a)): *)
lemma "(ALL x. P x \<longrightarrow> P(f x)) \<longrightarrow> P a \<longrightarrow> P(f a)"
apply fast
done

(* fastsimp and force combine fast and simp; force can be slow *)
lemma "(ALL x y. f x = f y \<longrightarrow> x = y) & (ALL x. g x = f x)
       \<longrightarrow> (ALL x y. g x = g y \<longrightarrow> x = y)"
apply fastsimp
done

end