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