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