theory week12A_demo imports Main begin -- ------------------------------------------------------------------ text {* Motivation *} lemma "(A \ B) = (B \ \A)" by blast value "True \ False" value "False \ \ True" lemma "(A \ B) = (B \ \A)" (* apply style *) apply(rule iffI) apply(case_tac A) apply(erule (1) impE) apply(erule disjI1) apply(erule disjI2) apply(erule disjE) apply(rule impI) apply assumption apply(rule impI) apply(erule notE) apply assumption done lemma "(A \ B) = (B \ \A)" proof (rule iffI) assume AB: "A \ B" show "B \ \ A" proof (cases A) assume A: "A" from AB A have "B" by(rule impE) thus ?thesis by(rule disjI1) next assume "\ A" thus ?thesis by (rule disjI2) qed next assume "B \ \ A" thus "A \ B" proof (rule disjE) assume "B" thus ?thesis by(rule impI) next assume notA: "\ A" show ?thesis proof (rule impI) assume "A" from notA this show "B" by (rule notE) qed qed qed -- ---------------------------------------- text {* Isar *} lemma "\ A; B \ \ A \ B" proof assume A_is_true: "A" from A_is_true show "A" by assumption next assume B_is_true: "B" from B_is_true show "B" by simp qed lemma assumes PorQ: "P \ Q" shows "Q \ P" using PorQ proof assume P: "P" from P show "Q \ P" by(rule disjI2) next assume "Q" from this show "Q \ P" by(rule disjI1) qed lemma assumes "A" assumes B_is_true: "B" shows "A \ B" proof(rule conjI) show "B" by (rule B_is_true) from `A` show "A" by assumption qed lemma "(x::nat) + 1 = 1 + x" proof - have l: "x + 1 = Suc x" by simp have r: "1 + x = Suc x" by simp show "x + 1 = 1 + x" by (simp only: l r) qed -- ------------------------------------------------------------------ section "More Isar" text {* . = by assumption, .. = by rule *} lemma "\ A; B \ \ B \ A" proof assume "B" from `B` show "B" . next assume "A" from this show "A" . qed lemma "\ A; B \ \ B \ A" proof - assume B: "B" and A: "A" from B A show "B \ A" by(rule conjI) qed text {* backward/forward *} lemma "A \ B \ B \ A" proof assume "A \ B" from this have "A" .. from `A \ B` have "B" .. from `B` `A` show "B \ A" .. qed text{* fix *} lemma assumes P: "\x. P x" shows "\x. P (f x)" proof fix x from P show "P (f x)" by(rule spec) qed text{* 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 text {* obtain *} lemma assumes Pf: "\x. P (f x)" shows "\y. P y" proof - from Pf obtain x where "P (f x)" .. from this show ?thesis .. qed lemma assumes ex: "\x. \y. P x y" shows "\y. \x. P x y" proof fix y show "\x. P x y" proof - from ex obtain x where "\y. P x y" .. hence "P x y" .. thus ?thesis .. qed qed text {* moreover *} lemma "A \ B \ B \ A" proof assume "A \ B" from `A \ B` have "B" .. moreover from `A \ B` have "A" .. ultimately show "B \ A" .. 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 fix x y assume le: "(x::int) \ y" from mono_f le have "f x \ f y" .. moreover from mono_g le have "g x \ g y" .. ultimately show "f x + g x \ f y + g y" by(rule add_mono) qed -- --------------------------------------------------------------- -- {* Isar, case distinction *} declare length_tl[simp del] (* isar style, just using "proof (cases xs)", not using case *) lemma "length (tl xs) = length xs - 1" proof(cases xs) assume "xs = []" thus ?thesis by simp next fix y ys assume "xs = y#ys" thus ?thesis by simp qed (* isar style, using case *) lemma "length (tl xs) = length xs - 1" proof(cases xs) case Nil thus ?thesis by simp next case (Cons y ys) from Cons show ?thesis by simp qed -- {* structural induction *} (* apply style *) lemma "2 * (\iii"} or @{text"\"} *} lemma assumes A: "(\n. (\m. m < n \ P m) \ P n)" shows "P (n::nat)" proof(rule A) show "\m. m < n \ P m" proof(induct n) case 0 thus ?case by simp next case (Suc n) show ?case proof(cases) assume eq: "m = n" from A Suc have "P n" by blast with eq show "P m" by simp next assume neq: "m \ n" from Suc neq have "m < n" by arith thus "P m" by(rule Suc) qed qed qed -- --------------------------------------------------------------- -- "calculational reasoning" -- "also/finally" lemma right_inverse: fixes prod :: "'a \ 'a \ 'a" (infixl "\" 70) fixes inv :: "'a \ 'a" ("(_\<^sup>-)" [1000] 999) fixes one :: 'a ("\") assumes assoc: "\x y z. (x \ y) \ z = x \ (y \ z)" assumes left_inv: "\x. x\<^sup>- \ x = \" assumes left_one: "\x. \ \ x = x" shows "x \ x\<^sup>- = \" proof - have "x \ x\<^sup>- = \ \ (x \ x\<^sup>-)" by (simp only: left_one) also have "\ = \ \ x \ x\<^sup>-" by (simp only: assoc) also have "\ = (x\<^sup>-)\<^sup>- \ x\<^sup>- \ x \ x\<^sup>-" by (simp only: left_inv) also have "\ = (x\<^sup>-)\<^sup>- \ (x\<^sup>- \ x) \ x\<^sup>-" by (simp only: assoc) also have "\ = (x\<^sup>-)\<^sup>- \ \ \ x\<^sup>-" by (simp only: left_inv) also have "\ = (x\<^sup>-)\<^sup>- \ (\ \ x\<^sup>-)" by (simp only: assoc) also have "\ = (x\<^sup>-)\<^sup>- \ x\<^sup>-" by (simp only: left_one) also have "\ = \" by (simp only: left_inv) finally show ?thesis . qed print_trans_rules -- "mixed operators" lemma "1 < (5::nat)" proof - have "1 < Suc 1" by simp also have "Suc 1 = 2" by simp also have "2 \ (5::nat)" by simp finally show ?thesis . qed -- "substitution" lemma blah proof - have "2*y + 2*y = (0::nat)" sorry also have "2*y = x" sorry also have "(0::nat) \ 2*c" sorry also have "c = d div 2" sorry also have "d = 2 * x" sorry finally have "x + x \ 2 * x " by simp oops print_trans_rules -- "antisymmetry" lemma blub proof - have "a < (b::nat)" sorry also have "b < a" sorry finally show blub . qed -- "notE as trans" thm notE declare notE [trans] lemma blub proof - have "\P" sorry also have "P" sorry finally show blub . qed -- "monotonicity" lemma "a+b \ 2*a + 2*(b::nat)" proof - have "a + b \ 2*a + b" by simp also have "b \ 2*b" by simp finally show "a+b \ 2*a + 2*b" by simp qed lemma "a+b \ 2*a + 2*(b::nat)" proof - have "a + b \ 2*a + b" by simp also have "b \ 2*b" by simp also have "\x y. x \ y \ 2 * a + x \ 2 * a + y" by simp ultimately show "a+b \ 2*a + 2*(b::nat)" . qed declare algebra_simps [simp] lemma "(a+b::int)\<^sup>2 \ 2*(a\<^sup>2 + b\<^sup>2)" proof - have "(a+b)\<^sup>2 \ (a+b)\<^sup>2 + (a-b)\<^sup>2" by simp thm numeral_2_eq_2 also have "(a+b)\<^sup>2 \ a\<^sup>2 + b\<^sup>2 + 2*a*b" by (simp add: numeral_2_eq_2) also have "(a-b)\<^sup>2 = a\<^sup>2 + b\<^sup>2 - 2*a*b" by (simp add:numeral_2_eq_2) finally show ?thesis by simp qed -- --------------------------------------------------------------- end