theory Isar_Induct_Demo imports Main begin section{*Case distinction and induction*} subsection{*Case distinction*} text{* Explicit: *} 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 text{* Implicit: *} lemma "length(tl xs) = length xs - 1" proof (cases xs) case Nil thm Nil thus ?thesis by simp next case (Cons y ys) thm Cons thus ?thesis by simp qed subsection{*Structural induction for nat*} text{* Explicit: *} lemma "\{0..n::nat} = n*(n+1) div 2" (is "?P n") proof (induct n) show "?P 0" by simp next fix n assume "?P n" thus "?P(Suc n)" by simp qed text{* Implicit: *} lemma "\{0..n::nat} = n*(n+1) div 2" proof (induct n) case 0 show ?case by simp next case (Suc n) thm Suc thus ?case by simp qed text{* After the induct or cases step, the PG menu item Isabelle/Show me/cases displays the different cases. *} text{* Induction with @{text "\"} *} lemma split_list: "x : set xs \ \ys zs. xs = ys @ x # zs" proof (induct xs) case Nil thus ?case by simp next case (Cons a xs) thm Cons.hyps --"Induction hypothesis" thm Cons.prems --"Premises of the step case" thm Cons from Cons.prems have "x = a \ x : set xs" by simp thus ?case proof assume "x = a" hence "a#xs = [] @ x # xs" by simp thus ?thesis by blast next assume "x : set xs" then obtain ys zs where "xs = ys @ x # zs" using Cons.hyps by auto hence "a#xs = (a#ys) @ x # zs" by simp thus ?thesis by blast qed qed (* Display the different cases with ProofGeneral: Isabelle/Show me/cases after "proof (induct xs)" *) subsection{*Rule induction*} inductive Ev :: "nat => bool" where Ev0: "Ev 0" | Ev2: "Ev n \ Ev(n+2)" declare Ev.intros [simp] lemma "Ev n \ \k. n = 2*k" proof (induct rule: Ev.induct) case Ev0 show ?case by simp next case Ev2 thus ?case by arith qed lemma "Ev n \ \k. n = 2*k" proof (induct rule: Ev.induct) case Ev0 show ?case by simp next case (Ev2 m) then obtain k where "m = 2*k" by blast hence "m+2 = 2*(k+1)" by simp thus "\k. m+2 = 2*k" by blast qed (* Display the different cases with ProofGeneral: Isabelle/Show me/cases Note the hyp "Ev n" in addition to "EX k. n = 2*k" *) subsection{*Inductive definition of the reflexive transitive closure *} consts step :: "'a \ 'a \ bool" (infix "\" 55) inductive steps :: "'a \ 'a \ bool" (infix "\*" 55) where refl: "x \* x" | step: "\ x \ y; y \* z \ \ x \* z" declare refl[simp, intro] text{* Explicit and by hand: *} lemma "x \* y \ y \* z \ x \* z" proof(induct rule: steps.induct) fix x assume "x \* z" thus "x \* z" . --"by assumption" next fix x' x y :: 'a assume "x' \ x" and "x \* y" assume IH: "y \* z \ x \* z" assume "y \* z" show "x' \* z" by(rule step[OF `x' \ x` IH[OF `y\*z`]]) qed text{* Implicit and automatic: *} lemma "x \* y \ y \* z \ x \* z" proof(induct rule: steps.induct) case refl thus ?case . next case (step x' x y) --"x' x y not used in proof text, just for demo" thm step thm step.hyps thm step.prems show ?case by (metis step.hyps(1) step.hyps(3) step.prems steps.step) qed end