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