theory Demo2 imports Main begin section{*Case distinction and induction*} lemma "length(tl xs) = length xs - 1" proof (cases xs) case Nil thus ?thesis by simp next case Cons thus ?thesis by simp qed subsection{*Structural induction*} lemma "(\i\n. i) = n*(n+1::nat) div 2" by (induct n, simp_all) lemma "(\i\n. i) = n*(n+1::nat) 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 lemma "(\i\n. i) = n*(n+1::nat) div 2" proof (induct n) case 0 show ?case by simp next case Suc thus ?case by simp qed text{* If we want to name the variable in the Suc-case: *} lemma fixes n::nat shows "n < n*n + 1" proof (induct n) case 0 show ?case by simp next case (Suc i) hence "i+1 < i*i + 2" by simp thus ?case by simp qed 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) hence "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 by auto hence "a#xs = (a#ys) @ x # zs" by simp thus ?thesis by blast qed qed 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 thus ?case by simp next case Ev2 thus ?case by arith qed lemma assumes n: "Ev n" shows "\k. n = 2*k" using n proof induct case Ev0 thus ?case by simp next case Ev2 thus ?case by arith qed lemma assumes n: "Ev n" shows "\k. n = 2*k" using n proof induct case Ev0 thus ?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" .. qed subsection{*Induction with fun*} fun rot :: "'a list \ 'a list" where "rot [] = []" | "rot [x] = [x]" | "rot (x#y#zs) = y # rot(x#zs)" lemma "xs \ [] \ rot xs = tl xs @ [hd xs]" proof (induct xs rule: rot.induct) case 1 thus ?case by simp next case 2 show ?case by simp next case (3 a b cs) have "rot (a # b # cs) = b # rot(a # cs)" by simp also have "\ = b # tl(a # cs) @ [hd(a # cs)]" by(simp add:3) also have "\ = tl (a # b # cs) @ [hd (a # b # cs)]" by simp finally show ?case . --" proof by assumption" qed lemma "xs \ [] \ rot xs = tl xs @ [hd xs]" by (induct xs rule: rot.induct, simp_all) subsection{*Chains of (in)equations*} text{* A little bit of also/finally inside *} lemma fixes m :: int assumes mn: "abs(m*n) = 1" shows "abs m = 1" sorry (* Fill in the proof! *) lemma fixes m :: int assumes mn: "abs(m*n) = 1" shows "abs m = 1" proof - have "m \ 0" "n \ 0" using mn by auto have "\ (2 \ abs m)" proof assume "2 \ abs m" hence "2*abs n \ abs m * abs n" by(simp add: mult_mono) also have "\ = 1" using mn by(simp add: abs_mult) finally show False using `n \ 0` by simp qed thus "abs m = 1" using `m \ 0` by arith qed subsection{* Monotonicity reasoning *} lemma fixes a :: int shows "(a+b)\ \ 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 algebra_simps) also have "(a-b)\ = a\ + b\ - 2*a*b" by(simp add:numeral_2_eq_2 algebra_simps) finally show ?thesis by simp qed subsection{*Accumulating facts*} thm mono_def lemma assumes monof: "mono(f::int\int)" and monog: "mono(g::int\int)" shows "mono(\i. f i + g i)" proof --"rule monoI used automatically" fix i j :: int assume A: "i \ j" have "f i \ f j" using A monof by(simp add:mono_def) moreover have "g i \ g j" using A monog by(simp add:mono_def) ultimately show "f i + g i \ f j + g j" by arith qed lemma dvd_minus: assumes du: "(d::int) dvd u" assumes dv: "d dvd v" shows "d dvd u - v" proof - from du obtain ku where "u = d * ku" by(fastsimp simp: dvd_def) moreover from dv obtain kv where "v = d * kv" by(fastsimp simp: dvd_def) ultimately have "u - v = d * ku - d * kv" by simp also have "\ = d * (ku - kv)" by (simp add: algebra_simps) finally show ?thesis by simp qed end