(* Template for exercise and homework. * IF YOU USE THIS FOR HOMEWORK, PLEASE DELETE THE EXERCISE PARTS THAT ARE * NOT REQUIRED FOR HOMEWORK SOLUTION, AND MAKE SURE THAT THE REST DOES NOT * CONTAIN ANY \sorry\s! *) (*<*) theory tut05 imports Complex_Main "~~/src/HOL/Library/Tree" begin (*>*) text {* \ExerciseSheet{5}{26.~5.~2017} *} text \ \<^item> Import \Complex_Main\ and \"~~/src/HOL/Library/Tree"\! \<^item> For this exercise sheet (and homework!), you are not allowed to use sledgehammer! Proofs using the \smt, metis, meson, or moura\ methods are forbidden! \ text \ \Exercise{Estimating power-of-two by factorial} Prove that, for all natural numbers $n>3$, we have $2^n < n!$. We have already prepared the proof skeleton for you. \ 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) assume IH: "3 < n \ (2::nat) ^ n < fact n" assume PREM: "3 < Suc n" from PREM have "n>3 \ n=3" by auto then show "(2::nat) ^ Suc n < fact (Suc n)" proof assume A: "3 < 2*fact n" using IH[OF A] by simp also have "\ < (n+1) * fact n" using PREM by simp also have "\ = fact (Suc n)" by simp finally show ?thesis . next assume "n=3" then show ?thesis by (simp add: eval_nat_numeral) qed (* have ?case proof cases assume "3(3 \vspace{1em} {\bfseries Warning!} Make sure that your numerals have the right type, otherwise proofs will not work! To check the type of a numeral, hover the mouse over it with pressed CTRL (Mac: CMD) key. Example: \ lemma "2^n \ 2^Suc n" apply auto oops -- \Leaves the subgoal \2 ^ n \ 2 * 2 ^ n\\ text \You will find out that the numeral \2\ has type @{typ 'a}, for which you do not have any ordering laws. So you have to manually restrict the numeral's type to, e.g., @{typ nat}.\ lemma "(2::nat)^n \ 2^Suc n" by simp -- \Note: Type inference will infer \nat\ for the unannotated numeral, too. Use CTRL+hover to double check!\ text \ \vspace{1em} \ text \\Exercise{Sum Squared is Sum of Cubes} \<^item> Define a recursive function $sumto~f~n = \sum_{i=0\ldots n} f(i)$. \<^item> Show that $\left(\sum_{i=0\ldots n}i\right)^2 = \sum_{i=0\ldots n} i^3$. \ fun sumto :: "(nat \ nat) \ nat \ nat" where "sumto f 0 = f 0" | "sumto f (Suc n) = f (Suc n) + sumto f n" text \You may need the following lemma:\ lemma sum_of_naturals: "2 * sumto (\x. x) n = n * Suc n" by (induction n) auto lemma "sumto (\x. x) n ^ 2 = sumto (\x. x^3) n" proof (induction n) case 0 show ?case by simp (* by simp Should be trivial. *) 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\ have "(sumto (\x. x) (Suc n))\<^sup>2 = ((Suc n) + sumto (\x. x) n)\<^sup>2" by simp also have "\ = (Suc n)\<^sup>2 + 2*sumto (\x. x) n*(Suc n) + (sumto (\x. x) n)\<^sup>2" by (simp add: eval_nat_numeral) also have "\ = (Suc n)\<^sup>2 + (Suc n)*n*(Suc n) + (sumto (\x. x) n)\<^sup>2" by (simp add: sum_of_naturals) also have "\ = (Suc n)^3 + (sumto (\x. x) n)\<^sup>2" by (simp add: eval_nat_numeral) also have "\ = (Suc n)^3 + sumto (\x. x ^ 3) n" by (simp add: IH) also have "\ = sumto (\x. x ^ 3) (Suc n)" by simp finally show "(sumto (\x. x) (Suc n))\<^sup>2 = sumto (\x. x ^ 3) (Suc n)" . qed text \ \Exercise{Paths in Graphs} A graph is described by its adjacency matrix, i.e., \G :: 'a \ 'a \ bool\. Define a predicate \path G u p v\ that is true if \p\ is a path from \u\ to \v\, i.e., \p\ is a list of nodes, not including \u\, such that the nodes on the path are connected with edges. In other words, \path G u (p\<^sub>1\p\<^sub>n) v\, iff \G u p\<^sub>1\, \G p\<^sub>i p\<^sub>i\<^sub>+\<^sub>1\, and \p\<^sub>n = v\. For the empty path (\n=0\), we have \u=v\. \ fun path :: "('a \ 'a \ bool) \ 'a \ 'a list \ 'a \ bool" where "path G u [] v \ u=v" | "path G u (w#p) v \ G u w \ path G w p v" text \Test cases\ definition "nat_graph x y \ y=Suc x" value \path nat_graph 2 [] 2\ value \path nat_graph 2 [3,4,5] 5\ value \\ path nat_graph 3 [3,4,5] 6\ value \\ path nat_graph 2 [3,4,5] 6\ text \Show the following lemma, that decomposes paths. Register it as simp-lemma.\ lemma path_append[simp]: "path G u (p1@p2) v \ (\w. path G u p1 w \ path G w p2 v)" apply (induction p1 arbitrary: u) by auto text \ Show that, for a non-distinct path from \u\ to \v\, we find a longer non-distinct path from \u\ to \v\. Note: This can be seen as a simple pumping-lemma, allowing to pump the length of the path. Hint: Theorem @{thm [source] not_distinct_decomp}. \ lemma pump_nondistinct_path: assumes P: "path G u p v" assumes ND: "\distinct p" shows "\p'. length p' > length p \ \distinct p' \ path G u p' v" proof - from not_distinct_decomp[OF ND] obtain xs ys zs y where [simp]: "p=xs @ [y] @ ys @ [y] @ zs" by blast let ?p'="(xs@[y]@ys@[y]@ys@[y]@zs)" from P have "path G u ?p' v" by auto then have "length ?p' > length p \ \distinct ?p' \ path G u ?p' v" by simp then show ?thesis by blast qed text \ \NumHomework{Estimate for Number of Leafs}{June 2} Recall: Use Isar, proofs using \metis, smt, meson, or moura\ (as generated by sledgehammer) are forbidden! Define a function to count the number of leafs in a binary tree: \ fun num_leafs :: "'a tree \ nat" where "num_leafs _ = undefined" text \ Start by showing the following auxiliary lemma: \ lemma auxl: assumes IHl: "num_leafs l \ 2 ^ height l" and IHr: "num_leafs r \ 2 ^ height r" and lr: "height l \ height r" shows "num_leafs(Node l x r) \ 2 ^ height(Node l x r)" oops text \Also show the symmetric statement. Hint: Copy-paste-adjust! \ lemma auxr: assumes IHl: "num_leafs l \ 2 ^ height l" and IHr: "num_leafs r \ 2 ^ height r" and rl: "\ height l \ height r" shows "num_leafs(Node l x r) \ 2 ^ height(Node l x r)" oops text \Finally, show that we can estimate the number of leafs in a tree as follows:\ lemma "num_leafs t \ 2^height t" proof (induction t) case Leaf show ?case sorry (* by auto should be straightforward. *) next case (Node l x r) assume IHl: "num_leafs l \ 2 ^ height l" assume IHr: "num_leafs r \ 2 ^ height r" show "num_leafs \l, x, r\ \ 2 ^ height \l, x, r\" text \Fill in your proof here\ sorry qed text \ \NumHomework{Simple Paths}{June 2} This homework is worth 5 bonus points. A simple path is a path without loops, or, in other words, a path where no node occurs twice. (Note that the first node of the path is not included, such that there may be a simple path from \u\ to \u\.) Show that for every path, there is a corresponding simple path: \ lemma exists_simple_path: assumes "path G u p v" shows "\p'. path G u p' v \ distinct p'" using assms proof (induction p rule: length_induct) case (1 p) assume IH: "\pp. length pp < length p \ path G u pp v \ (\p'. path G u p' v \ distinct p')" assume PREM: "path G u p v" show "\p'. path G u p' v \ distinct p'" text \Fill in your proof here.\ sorry qed (*<*) end (*>*)