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