theory Demo05
imports Main
begin
section {* Isar *}
lemma "\ A; B \ \ A \ B"
proof (rule conjI)
assume A: "A"
from A show "A" by assumption
next
assume B: "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
-- ------------------------------------------------
text {* . = 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 and A show "B \ A" ..
qed
text {* backward/forward *}
lemma "A \ B \ B \ A"
proof
assume AB: "A \ B"
from AB show "B \ A"
proof
assume A: "A" and B: "B"
from B A show "B \ A" ..
qed
qed
-- "Backtick: refer to facts without naming them"
lemma "A \ B \ B \ A"
proof
assume "A \ B"
from `A \ B` show "B \ A"
proof
assume "A" "B"
from `B` `A` show "B \ A" ..
qed
qed
-- "then = from this"
lemma "A \ B \ B \ A"
proof
assume "A \ B"
then show "B \ A"
proof
assume "B" "A"
then show "B \ A" ..
qed
qed
text{* fix *}
lemma assumes P: "\x. P x" shows "\x. P (f x)"
proof
fix a
from P show "P (f a)" ..
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)"
then 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)" ..
then show "\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" ..
then have "P x y" ..
then show "\x. P x y" ..
qed
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
then show ?thesis by blast
qed
lemma "\x. P x \ (\x. P x)"
oops
text {* Isar: moreover/ultimately *}
thm mono_def 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 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 auto
qed
text {* Isar: 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
-- "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 "x + 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
-- "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 ring_simps [simp]
lemma "(a+b::int)\ \ 2*(a\ + b\)"
proof -
have "(a+b)\ \ (a+b)\ + (a-b)\" by simp
also have "(a+b)\ \ a\ + b\ + 2*a*b" by (simp add: numeral_2_eq_2)
also have "(a-b)\ = a\ + b\ - 2*a*b" by (simp add: numeral_2_eq_2)
finally show ?thesis by simp
qed
end