theory Demo = Main:

(* a simple backward step: *)
lemma "A & B"
apply(rule conjI)
oops;

(* a simple backward proof: *)
lemma "B & A --> A & B"
apply(rule impI)
apply(rule conjI)
 apply(rule conjE)
  apply(assumption)
 apply(rule conjE)
  apply(assumption)
 apply(assumption)
apply(rule conjE)
 apply(assumption)
apply(assumption)
done;

(* a shorter version: *)
lemma "B & A --> A & B"
apply(rule impI)
apply(rule conjE)
 apply(assumption)
apply(rule conjI)
 apply(assumption)
apply(assumption)
done;

(* still shorter, using elim-resolution: *)
lemma "B & A --> A & B"
apply(rule impI)
apply(erule conjE)
apply(rule conjI)
 apply(assumption)
apply(assumption)
done;

(* automatically: *)
lemma "B & A --> A & B"
apply(blast)
(* works as well:
apply(fast)
apply(auto)
*)
done;

(* explicit case distinctions: *)
lemma "((P --> Q) --> P) --> P"
apply(case_tac P)
 apply(simp)
apply(simp)
done;

(* How to convert --> back to ==> automatically: *)
lemma [rule_format]: "A & A --> A"
apply blast
done

(* explicit backtracking *)
lemma "[| P & Q; A & B |] ==> A"
apply(erule conjE)
back
apply(assumption)
(* UGLY! NOT ALLOWED IN FINAL SOLUTION *)
oops;

(* implict backtracking *)
lemma "[| P & Q; A & B |] ==> A"
apply(erule conjE, assumption)
done;

(*** Basic rules ***)

(* \<and> *)
thm conjI conjE conjunct1 conjunct2;
(* \<or> *)
thm disjI1 disjI2 disjE;
(* \<longrightarrow> *)
thm impI impE mp;
(* = (iff) *)
thm iffI iffE iffD1 iffD2;
(* \<not> *)
thm notI notE;
(* Contradictions *)
thm FalseE ccontr classical;
(* Contrapositives *)
thm contrapos_nn contrapos_pp contrapos_np;

end