theory Isar_Demo
imports Main
begin
section{* An introductory example *}
lemma "\ surj(f :: 'a \ 'a set)"
proof
assume 0: "surj f"
from 0 have 1: "\A. \a. A = f a" by(simp add: surj_def)
from 1 have 2: "\a. {x. x \ f x} = f a" by blast
from 2 show "False" by blast
qed
text{* A bit shorter: *}
lemma "\ surj(f :: 'a \ 'a set)"
proof
assume 0: "surj f"
from 0 have 1: "\a. {x. x \ f x} = f a" by(auto simp: surj_def)
from 1 show "False" by blast
qed
subsection{* this, then, hence and thus *}
text{* Avoid labels, use this: *}
lemma "\ surj(f :: 'a \ 'a set)"
proof
assume "surj f"
from this have "\a. {x. x \ f x} = f a" by(auto simp: surj_def)
from this show "False" by blast
qed
text{* then = from this *}
lemma "\ surj(f :: 'a \ 'a set)"
proof
assume "surj f"
then have "\a. {x. x \ f x} = f a" by(auto simp: surj_def)
then show "False" by blast
qed
text{* hence = then have, thus = then show *}
lemma "\ surj(f :: 'a \ 'a set)"
proof
assume "surj f"
hence "\a. {x. x \ f x} = f a" by(auto simp: surj_def)
thus "False" by blast
qed
subsection{* Structured statements: fixes, assumes, shows *}
lemma
fixes f :: "'a \ 'a set"
assumes s: "surj f"
shows "False"
proof - (* no automatic proof step! *)
have "\ a. {x. x \ f x} = f a" using s
by(auto simp: surj_def)
thus "False" by blast
qed
section{* Proof patterns *}
lemma "P \ Q"
proof
assume "P"
show "Q" sorry
next
assume "Q"
show "P" sorry
qed
lemma "A = (B::'a set)"
proof
show "A \ B" sorry
next
show "B \ A" sorry
qed
lemma "A \ B"
proof
fix a
assume "a \ A"
show "a \ B" sorry
qed
text{* Contradiction *}
lemma P
proof (rule ccontr)
assume "\P"
show "False" sorry
qed
text{* Case distinction *}
lemma "R"
proof cases
assume "P"
show "R" sorry
next
assume "\ P"
show "R" sorry
qed
lemma "R"
proof -
have "P \ Q" sorry
then show "R"
proof
assume "P"
show "R" sorry
next
assume "Q"
show "R" sorry
qed
qed
text{* obtain example *}
lemma "\ surj(f :: 'a \ 'a set)"
proof
assume "surj f"
hence "\a. {x. x \ f x} = f a" by(auto simp: surj_def)
then obtain a where "{x. x \ f x} = f a" by blast
hence "a \ f a \ a \ f a" by blast
thus "False" by blast
qed
text{* Interactive exercise: *}
lemma assumes "EX x. ALL y. P x y" shows "ALL y. EX x. P x y"
oops (* solution at the bottom *)
section{* Streamlining proofs *}
subsection{* Pattern matching and ?-variables *}
text{* Show EX *}
lemma "EX xs. length xs = 0" (is "EX xs. ?P xs")
proof
show "?P([])" by simp
qed
text{* Multiple EX easier with forward proof: *}
lemma "EX x y :: int. x < z & z < y" (is "EX x y. ?P x y")
proof -
have "?P (z - 1) (z + 1)" by arith
thus ?thesis by blast
qed
subsection{* Quoting facts: *}
lemma assumes "x < (0::int)" shows "x*x > 0"
proof -
from `x<0` show ?thesis by(metis mult_neg_neg)
qed
subsection {* Example: Top Down Proof Development *}
text{* The key idea: case distinction on length: *}
lemma "(EX ys zs. xs = ys @ zs \ length ys = length zs) |
(EX ys zs. xs = ys @ zs & length ys = length zs + 1)"
proof cases
assume "EX n. length xs = n+n"
show ?thesis sorry
next
assume "\ (EX n. length xs = n+n)"
show ?thesis sorry
qed
text{* A proof skeleton: *}
lemma "(EX ys zs. xs = ys @ zs \ length ys = length zs) |
(EX ys zs. xs = ys @ zs & length ys = length zs + 1)"
proof cases
assume "EX n. length xs = n+n"
then obtain n where "length xs = n+n" by blast
let ?ys = "take n xs"
let ?zs = "take n (drop n xs)"
have "xs = ?ys @ ?zs \ length ?ys = length ?zs" sorry
thus ?thesis by blast
next
assume "\ (EX n. length xs = n+n)"
then obtain n where "length xs = Suc(n+n)" sorry
let ?ys = "take (Suc n) xs"
let ?zs = "take n (drop (Suc n) xs)"
have "xs = ?ys @ ?zs \ length ?ys = length ?zs + 1" sorry
then show ?thesis by blast
qed
text{* The complete proof: *}
lemma "(EX ys zs. xs = ys @ zs \ length ys = length zs) |
(EX ys zs. xs = ys @ zs & length ys = length zs + 1)"
proof cases
assume "EX n. length xs = n+n"
then obtain n where "length xs = n+n" by blast
let ?ys = "take n xs"
let ?zs = "take n (drop n xs)"
have "xs = ?ys @ ?zs \ length ?ys = length ?zs"
by (simp add: `length xs = n + n`)
thus ?thesis by blast
next
assume "\ (EX n. length xs = n+n)"
hence "EX n. length xs = Suc(n+n)" by arith
then obtain n where l: "length xs = Suc(n+n)" by blast
let ?ys = "take (Suc n) xs"
let ?zs = "take n (drop (Suc n) xs)"
have "xs = ?ys @ ?zs \ length ?ys = length ?zs + 1" by (simp add: l)
thus ?thesis by blast
qed
subsection {* moreover *}
lemma assumes "A \ B" shows "B \ A"
proof -
from `A \ B` have "A" by auto
moreover
from `A \ B` have "B" by auto
ultimately show "B \ A" by auto
qed
subsection{* Raw proof blocks *}
lemma fixes k :: int assumes "k dvd (n+k)" shows "k dvd n"
proof -
{ fix a assume a: "n+k = k*a"
have "EX b. n = k*b"
proof
show "n = k*(a - 1)" using a by(simp add: algebra_simps)
qed }
with assms show ?thesis by (auto simp add: dvd_def)
qed
text{* Solution to interactive exercise: *}
lemma assumes "EX x. ALL y. P x y" shows "ALL y. EX x. P x y"
proof
fix b
from assms obtain a where 0: "ALL y. P a y" by blast
show "EX x. P x b"
proof
show "P a b" using 0 by blast
qed
qed
end