theory Demo7 imports Main GCD begin section{* Predicate logic *} text{* A warming up exercise: propositional logic. *} lemma "A \ (B \ C) \ A \ B \ A \ C" oops text{* Quantifier reasoning *} text{* A successful proof: *} lemma "\ x. \ y. x = y" apply (rule allI) apply (rule exI) apply (rule refl) done lemma "\ x. \ y. x = y" apply (rule allI) apply (rule_tac x = "x" in exI) apply (rule refl) done declare [[show_types = true]] text{* Isar style: *} lemma shows "\ (x::'a). \ y. x = y" proof (rule allI) fix x::'a show "\ y. x = y" proof (rule exI) show "x = x" by (rule refl) qed qed text{* An unsuccessful proof: *} lemma "\ y. \ x. x = y" apply(rule exI) apply(rule allI) (* Does not work: apply(rule refl) *) oops lemma "\ y. \ x. x = y" proof (rule exI) (* We are stuck. The metavariable is not allowed in the goal statement show " \x\'a. x = (?y\'a)" *) oops text{* Intro and elim reasoning: *} lemma assumes Hyp: "\ y. \ x. P x y" shows "\ x::'a. \ y::'b. P x y" (* the safe rules first: *) proof (rule allI) fix x::'a from Hyp show "\ y::'b. P x y" proof (rule exE) fix y::'b assume Hyp1: "\ x. P x y" (* now the unsafe ones: *) show ?thesis proof (rule_tac x = "y" in exI) from Hyp1 show "P x y" by (rule allE) qed qed qed lemma fixes P assumes Hyp: "\ y. \ x. P x y" shows "\ x. \ y. P x y" proof (rule allI) from Hyp obtain y where Hyp1: "\ x. P x y" by (rule exE) fix x show "\ y. P x y" proof (rule exI) from Hyp1 show "P x y" by (rule allE) qed qed lemma fixes P assumes Hyp: "\ y. \ x. P x y" shows "\ x. \ y. P x y" proof fix x from Hyp obtain y where "\ x. P x y" .. (* rule exE *) from this have "P x y" .. (* rule allE *) from this show "\ y. P x y" .. (* rule exI *) qed text{* What happens if an unsafe rule is tried too early: *} lemma assumes Hyp: "\ y. \ x. P x y" shows "\ x. \ y. P x y" proof (rule allI) fix x show "\ y. P x y" proof (rule exI) (* What is the value of ?y *) from Hyp obtain y where "\ x. P x y" by (rule exE) from this have "P x y" by (rule allE) (* Fails now: from this show "P x y" by(assumption) *) oops text{* Principle: First the safe rules (allI, exE: they generate parameters), then the unsafe rules (allE, exI: they generate unknowns). *} subsection{* Proof methods*} subsubsection{*More instantiation examples*} text{* Instantiating allE: *} lemma assumes A: "\ xs. xs@ys = zs" shows "ys=zs" thm allE using A proof(erule_tac x = "[]" in allE) assume A: "[] @ ys = zs" from A show ?thesis by(simp) qed text{* Instantiating exI: *} lemma "\ n. P(f n) \ \ m. P m" proof (erule exE) fix n assume A: "P (f n)" from A show ?thesis thm exI by(rule_tac x = "f n" in exI) qed text{* Instantiation removes ambiguity: *} lemma "\ A \ B; C \ D \ \ D" thm conjE proof (erule_tac P = "C" in conjE) (* without instantiation, the wrong one is chosen (first) *) assume D: "D" from this show ?thesis proof assumption qed qed lemma "\ A \ B; C \ D \ \ D" by (erule conjE) thm dvd_add dvd_refl thm dvd_add[OF dvd_refl dvd_refl] text{* Using lemmas as assumptions and forward reasoning *} subsubsection{* Forward reasoning *} lemma "A \ B \ \ \ A" thm conjunct1 apply(drule conjunct1) apply blast done lemma "A \ B \ \ \ A" thm conjunct1 apply(frule conjunct1) apply blast done thm sym iffD2; thm sym iffD2 sym [THEN iffD2] thm refl iffD2 iffD2 [OF refl] thm gcd_mult_distrib_nat lemma relprime_dvd_mult: "\gcd (k\nat) n = 1; k dvd m * n\ \ k dvd m" thm gcd_mult_distrib_nat apply (cut_tac gcd_mult_distrib_nat [of m k n]) oops lemma relprime_dvd_mult: "(gcd k (n\nat) = 1 \ k dvd m * n) \ k dvd m" apply (cut_tac gcd_mult_distrib_nat [where k="m" and m="k" and n="n"]) oops lemma relprime_dvd_mult: "(gcd k (n\nat) = 1 \ k dvd m * n) \ k dvd m" apply (cut_tac k="m" and m="k" and n="n" in gcd_mult_distrib_nat) oops (* For honesty, here is the full proof *) lemma relprime_dvd_mult: "(gcd k (n\nat) = 1 \ k dvd m * n) \ k dvd m" apply (cut_tac k="m" and m="k" and n="n" in gcd_mult_distrib_nat) apply simp thm subst apply (erule subst [OF sym]) thm gcd_greatest_nat apply (rule gcd_greatest_nat) apply simp apply simp done lemma relprime_dvd_mult_isar: fixes k and n and m assumes A: "(gcd k (n\nat) = 1 \ k dvd m * n)" shows "k dvd m" proof - from gcd_mult_distrib_nat [where k="m" and m="k" and n="n"] have B: " m * gcd k n = gcd (m * k) (m * n)" by assumption from A and B have B: "m = gcd (m * k) (m * n)" by simp from B show ?thesis proof (rule subst [OF sym]) show "k dvd gcd (m * k) (m * n)" thm gcd_greatest_nat proof (rule_tac k = "k" and m = "(m * k)" and n = "(m * n)" in gcd_greatest_nat) show "k dvd m * k" by simp next from A show "k dvd m * n" by simp qed qed qed subsubsection{* Clarification *} lemma "\ x y. P x y \ Q x y \ R x y" apply(clarify) oops lemma "\ x y. P x y \ Q x y \ R x y" apply(intro allI conjI) oops lemma "\ x y. x = 5 \ y = 7 \ y < z \ P(x+y\nat)" apply(clarsimp) oops end