theory Ex05_Tut_Sol imports Complex_Main "HOL-Library.Tree" begin lemma exp_fact_estimate: "n>3 \ (2::nat)^n < fact n" proof (induction n) case 0 then show ?case by auto next case (Suc n) show ?case text \Fill in a proof here. Hint: Start with a case distinction whether \n>3\ or \n=3\. \ proof - have "n>3 \ n=3" using Suc.prems by auto then show "(2::nat) ^ Suc n < fact (Suc n)" proof assume GT: "n>3" from Suc.IH[OF GT] have "(2::nat) * 2 ^ n < fact n + fact n" by simp also have "\ < fact n + n*fact n" using GT by simp finally have "2 * 2 ^ n < fact n + n * fact n" . then show "(2::nat) ^ Suc n < fact (Suc n)" by simp next assume "n=3" thus ?case by (simp add: eval_nat_numeral) qed qed qed lemma "2^n \ 2^Suc n" apply auto oops text \Leaves the subgoal \2 ^ n \ 2 * 2 ^ n\\ lemma "(2::nat)^n \ 2^Suc n" by simp fun sumto :: "(nat \ nat) \ nat \ nat" where "sumto f 0 = f 0" | "sumto f (Suc n) = sumto f n + f(Suc n)" lemma sum_of_naturals: "2 * sumto (\x. x) n = n * (n + 1)" by (induction n) auto lemma "sumto (\x. x) n ^ 2 = sumto (\x. x^3) n" proof (induct n) case 0 show ?case by simp next case (Suc n) assume IH: "(sumto (\x. x) n)\<^sup>2 = sumto (\x. x ^ 3) n" note [simp] = algebra_simps \\Extend the simpset only in this block\ show "(sumto (\x. x) (Suc n))\<^sup>2 = sumto (\x. x ^ 3) (Suc n)" proof - have "sumto (\x. x) (Suc n) ^ 2 = (sumto (\x. x) n + (n+1))^2" by (simp) also have "\ = sumto (\x. x) n ^ 2 + 2 * sumto (\x. x) n * (n+1) + (n+1)^2" by (simp add: power2_eq_square) also have "\ = sumto (\x. x^3) n + 2 * sumto (\x. x) n * (n+1) + (n+1)^2" using IH by (simp) also have "\ = sumto (\x. x^3) n + n * (n+1) * (n+1) + (n+1)^2" by (simp add: sum_of_naturals) also have "\ = sumto (\x. x^3) n + (n+1)^3" by (simp add: eval_nat_numeral) also have "\ = sumto (\x. x^3) (Suc n)" by (simp) finally show ?thesis . qed qed datatype 'a tchar = L | N 'a fun pretty :: "'a tree \ 'a tchar list" where "pretty Leaf = [L]" | "pretty (Node l x r) = N x # pretty l @ pretty r" value "pretty (Node (Node Leaf 0 Leaf) (1::nat) (Node Leaf 2 Leaf)) = [N 1, N 0, L, L, N 2, L, L]" lemma pretty_unique_aux: "pretty t @ xs = pretty t' @ xs' \ t=t'" proof (induction t arbitrary: t' xs xs') case Leaf then show ?case proof(cases t') case Leaf then show ?thesis by (rule sym) next case (Node _ x' _) then obtain xs' where "pretty t' = N x' # xs'" by simp with Leaf.prems have False by simp thus ?thesis .. qed next case (Node l x r) then show ?case proof (cases t') case Leaf with Node.prems show ?thesis by simp next fix l' x' r' assume [simp]: "t' = Node l' x' r'" from Node have l: "l = l'" by auto from Node have r: "r = r'" by fastforce from l r Node.prems show ?thesis by simp qed qed lemma pretty_unique: "pretty t = pretty t' \ t=t'" using pretty_unique_aux[where xs="[]" and xs'="[]"] by simp fun bin_tree2 :: "'a tree \ 'b tree \ bool" where "bin_tree2 Leaf Leaf = True" | "bin_tree2 (Node l x r) (Node l' x' r') = (bin_tree2 l l' \ bin_tree2 r r')" | "bin_tree2 _ _ = False" print_statement bin_tree2.induct lemma pretty_unique_aux': "pretty t @ xs = pretty t' @ xs' \ t=t'" apply (induction t t' arbitrary: xs xs' rule: bin_tree2.induct) apply auto apply fastforce done end