theory week02B_demo_Isar imports Main begin \ \ ------------------------------------------------------------------ \ \ \ {* Motivation *} \ lemma "(A \ B) = (B \ \A)" by blast value "True \ False" value "False \ \ True" lemma "(A \ B) = (B \ \A)" apply (rule iffI) apply (cases A) apply (rule disjI1) apply (erule impE) apply assumption apply assumption apply (rule disjI2) apply assumption apply (rule impI) apply (erule disjE) apply assumption apply (erule notE) apply assumption done lemma "(A \ B) = (B \ \A)" proof (rule iffI) assume AimpB: "A\B" show "B \ \ A" proof (cases A) assume A: "A" from AimpB A have B:"B" by (rule impE) from B show "B \ \A" by (rule disjI1) next assume notA: "\ A" from notA show "B \ \A" by (rule disjI2) qed next assume BA: "B \ \ A" show "A\B" proof (rule impI) assume A: "A" from BA A show B proof (elim disjE) assume B: "B" from B show B by assumption next assume notA: "\ A" from A notA show B by (elim notE) qed qed qed (* with this/thus/hence/etc *) lemma "(A \ B) = (B \ \A)" proof assume AimpB: "A \ B" show " B \ \ A" proof (cases A) assume A with AimpB have B by (rule impE) thus ?thesis by (rule disjI1) next assume "\A" thus ?thesis by (rule disjI2) qed next assume BA: "B \ \A" show " A \ B" proof assume A: A from BA show B proof assume B thus B by assumption next assume notA: "\A" from notA A show ?thesis by (rule notE) qed qed qed \ \ ------------------------------------------------------------------ \ \ \ {* Isar *} \ lemma "\ A; B \ \ A \ B" proof (rule conjI) assume A: "A" from A show "A" by assumption next assume "B" from `B` show "B" by assumption qed lemma assumes A: "A" assumes B: "B" shows "A \ B" proof (rule conjI) from A show "A" by assumption from B show "B" by assumption qed lemma "(x::nat) + 1 = 1 + x" proof - have A: "x + 1 = Suc x" by simp have B: "1 + x = Suc x" by simp show "x + 1 = 1 + x" by (simp only: A B) qed \ \ ------------------------------------------------------------------ \ section "More Isar" \ \ {* . = by assumption, .. = by rule *} \ lemma "\ A; B \ \ B \ A" proof assume A: "A" and B: "B" from A show "A" . from B show "B" . qed lemma "\ A; B \ \ B \ A" proof - assume A: "A" and B: "B" from B A show "B \ A" .. qed \ \ {* backward/forward *} \ lemma "A \ B \ B \ A" proof assume AB: "A \ B" from AB show "B \ A" proof assume "B" "A" from this show "B \ A" .. qed qed \ \ {* fix *} \ lemma assumes P: "\x. P x" shows "\x. P (f x)" proof fix a (* from P show "P (f a)" by (rule spec) *) from P show "P (f a)" .. qed \ \ {* Proof text can only refer to global constants, free variables in the lemma, and local names introduced via fix or obtain. *} \ lemma assumes Pf: "\x. P (f x)" shows "\y. P y" proof - from Pf show ?thesis proof fix x assume "P (f x)" from this show ?thesis .. qed qed \ \ {* obtain *} \ lemma assumes Pf: "\x. P (f x)" shows "\y. P y" proof - from Pf obtain x where "P(f x)" .. thus "\y. P y" .. qed lemma assumes ex: "\x. \y. P x y" shows "\y. \x. P x y" proof fix y from ex obtain x where "\y. P x y" .. from this have "P x y" .. (*hence "P x y" ..*) from this show "\x. P x y" .. (*thus "\x. P x y" .. *) qed thm exE lemma assumes A: "\x y. P x y \ Q x y" shows "\x y. P x y \ Q x y" proof - from A obtain x y where P: "P x y" and Q: "Q x y" by blast thus ?thesis by blast qed lemma assumes A: "\x y. P x y \ Q x y" shows "\x y. P x y \ Q x y" apply(rule exI) apply(rule exI) apply(insert A) apply(drule spec) apply(drule spec) apply assumption done \ \ {* moreover *} \ lemma "A \ B \ B \ A" proof assume AB: "A \ B" from AB have "B" by (rule conjunct2) moreover from AB have "A" by (rule conjunct1) ultimately show "B \ A" by (rule conjI) qed thm mono_def thm monoI lemma assumes mono_f: "mono (f::int\int)" and mono_g: "mono (g::int\int)" shows "mono (\i. f i + g i)" proof (rule monoI) fix i and j :: "int" assume A: "i \ j" from A mono_f have "f i \ f j" by (simp add: mono_def) moreover from A mono_g have "g i \ g j" by (simp add: mono_def) ultimately show "f i + g i \ f j + g j" by simp qed \ \ --------------------------------------- \ lemma "\A; B\ \ A \ B" apply(rule conjI) proof - assume A thus A . assume B thus B . qed end