theory week08A_demo_Isar2 imports Main begin
\ \ ----------------------------------------------------------------\
text \ 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
text \ structural induction \
(* apply style *)
lemma "2 * (\iii induction with @{text"\"} 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
\ \ ----------------------------------------------------------------\
text \ calculational reasoning\
text \ "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
text \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
text \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
text \antisymmetry\
lemma blub
proof -
have "a < (b::nat)" sorry
also
have "b < a" sorry
finally
show blub .
qed
text \notE as trans\
thm notE
declare notE [trans]
lemma blub
proof -
have "\P" sorry
also
have "P" sorry
finally
show blub .
qed
text \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