chapter \<open>Exercise Sheet -- Week 4\<close>

theory Exercise04
  imports 
    Main
begin

section \<open>Exercise 1 -- 2 points\<close>

fun factorial :: "nat \<Rightarrow> nat" where
  "factorial 0 = 1" 
| "factorial (Suc n) = Suc n * factorial n" 

fun fact_it :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
  "fact_it r 0  = r" 
| "fact_it r (Suc n) = fact_it (r * Suc n) n" 

fun factorial_it :: "nat \<Rightarrow> nat" where
  "factorial_it n = fact_it 1 n"  

text \<open>Prove that both implementations of the factorial function
  are equivalent. Note that @{thm [source] algebra_simps} contains
  distributive laws.\<close>

lemma "factorial_it n = factorial n" 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)"
proof -
  assume x1: "x \<noteq> 1" 
  show ?thesis sorry
qed


section \<open>Exercise 3 -- 4 points\<close>

text \<open>Prove the following lemma about the factorial function.\<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"
proof (induction n)  
  case (Suc n)
  show ?case sorry
qed auto
  
end