chapter \<open>Exercise Sheet -- Week 4\<close> theory Exercise04 imports Main begin section \<open>Exercise 1 -- 2 points\<close> fun add :: "nat \<Rightarrow> nat \<Rightarrow> nat" where "add x 0 = x" | "add x (Suc y) = Suc (add x y)" fun add_it :: "nat \<Rightarrow> nat \<Rightarrow> nat" where "add_it x 0 = x" | "add_it x (Suc y) = add_it (Suc x) y" text \<open>Prove the equivalence of @{const add} and @{const add_it}.\<close> lemma add_it_eq_add: "add_it x y = add x y" sorry section \<open>Exercise 2 -- 4 points\<close> fun gp :: "'a :: field \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 'a" where "gp x m 0 = x^m" | "gp x m (Suc n) = x^m + gp x (Suc m) n" text \<open>The function @{const gp} computes a geometric progression, i.e., @{prop "gp x m n = (\<Sum> i \<in> {m .. m+n}. x^i)"}.\<close> text \<open>Prove the closed formula for geometric progressions. Hint: don't forget to activate @{thm [source] field_simps} at certain points in the proof, so that division can be handled by the simplifier.\<close> lemma closed_formula: "x \<noteq> 1 \<Longrightarrow> gp x m n = (x^m - x^(m+n+1)) / (1 - x)" sorry section \<open>Exercise 3 -- 4 points\<close> fun factorial :: "nat \<Rightarrow> nat" where "factorial 0 = 1" | "factorial (Suc n) = Suc n * factorial n" text \<open>Prove the following lemma.\<close> text \<open>Remarks: \<^item> in the induction case @{term "Suc n"} perform a case analysis on @{prop "n \<ge> 4"}: these cases will then correspond to the standard base/induction-cases that we would perform on paper \<^item> calculational reasoning might be helpful \<^item> don't forget @{command find_theorems}, e.g. to find some lemma that might be useful for proving @{prop "x * y \<le> z * u"} \<^item> have a look at the simp rules / simpsets on slide 4/16 for the base case \<close> lemma "n \<ge> 4 \<Longrightarrow> 2^n < factorial n" sorry end