theory Demo = Main:

(* a test: solve the following goal in single steps *)
lemma "A&(B|C) ==> A&B | C";
oops;

(* renaming parameters *)
lemma "\<And>x y z. P x y z"
apply(rename_tac a b)
oops

(* rule application with instantiation *)
(* here: removes ambiguity *)
lemma "\<lbrakk> A & B; C & D \<rbrakk> \<Longrightarrow> D"
thm conjE
apply(erule_tac P = "C" in conjE)
(* without instantiation, the wrong one is chosen (first) *)
apply assumption
done;

(*** Quantifier reasoning ***)

(* a successful example of quantifier reasoning: *)
lemma "ALL x. EX y. x = y"
apply(rule allI)
apply(rule exI)
apply(rule refl)
done;

(* an unsuccessful example of quantifier reasoning: *)
lemma "EX y. ALL x. x = y"
apply(rule exI)
apply(rule allI)
(* Does not work:
apply(rule refl)
*)
oops;

(* I and E rules *)
lemma "(EX y. ALL x. P x y) ==> (ALL x. EX y. P x y)"
(* the safe rules first: *)
apply(rule allI)
apply(erule exE)
(* now the unsafe ones: *)
apply(rule_tac x=y in exI)
apply(erule_tac x=x in allE)
apply(assumption)
done;

(* what happens if an unsafe rule is tried too early: *)
lemma "(EX y. ALL x. P x y) ==> (ALL x. EX y. P x y)"
apply(rule allI)
apply(rule exI)
apply(erule exE)
apply(erule allE)
(* Fails now:
apply(assumption)
*)
oops;

(* Lehre:
   Zuerst sicher Quantoren Regeln (allI, exE: sie erzeugen Parameter),
   dann die unsicheren Quantoren Regeln (allE, exI: sie erzeugen ?-Variablen)
*)


(** More renaming **)

(* choosing your own names for convenience *)
lemma "xs \<noteq> [] \<longrightarrow> P xs"
apply(induct_tac xs)
apply simp
apply(rename_tac elem rest)
oops;

(* rename to avoid names chosen by Isabelle *)
lemma "ALL x. P x \<Longrightarrow> ALL x. ALL x. P x"
apply(rule allI)
apply(rule allI)
apply(rename_tac X)
apply(erule_tac x=X in allE)
apply assumption
done

(** More instantiation **)

(* Variables in rules can be instantiated directly
   (based on their position in the rule) *)
   
thm exI
thm exI[of _ "1::nat"];

lemma "EX n::nat. n*n = n"
apply(rule exI[of _ "1"])
apply(simp)
done;

(* instantiating allE *)
lemma "ALL xs. xs@ys = zs \<Longrightarrow> ys=zs"
thm allE
thm allE[of _ "[]"]
apply(erule allE[of _ "[]"])
apply(simp)
done;

(* Some more instantiations *)
lemma "EX n. P(f n) \<Longrightarrow> EX m. P m"
apply(erule exE)
(* Does not work:
apply(rule exI[of _ "f n"])
*)
apply(rule_tac x = "f n" in exI)
apply assumption
done;

lemma "\<lbrakk> EX n. P n; ALL m. P(m) \<longrightarrow> P(f m) \<rbrakk> \<Longrightarrow> EX a. P(f a)"
apply(erule exE)
apply(erule_tac x = "n" in allE)
apply blast
done;

(** Forward reasoning **)

lemma "A & B \<Longrightarrow> \<not> \<not> A"
thm conjunct1
apply(drule conjunct1)
apply blast
done;

thm dvd_add dvd_refl
thm dvd_add[OF dvd_refl dvd_refl]

end