theory Hw03
  imports Main
begin


section {* Task 1 (easy) *}

text {* 

  Define the function deldups which deleting 
  duplicates from a list. For example the list

  [1,2,3,1,2,3]
  
  should be transformed to

  [1,2,3].

*}

(*
fun
  deldups :: "'a list \<Rightarrow> 'a list"
where
 \<dots>
*)

text {* Prove the lemma: *}

lemma 
  shows "distinct (deldups xs)"
sorry

section {* Task 2 (easy) *}

text {* 
  
  Give a detailed proof (not using simp, auto, etc)
  for the formula:

*}

lemma "(A \<longrightarrow> B) \<longrightarrow> (B \<longrightarrow> C) \<longrightarrow> A \<longrightarrow> C"
sorry

section {* Task 3 (easy) *}

text {* 
  
  Define the function calculating the Fibonacci 
  numbers. 

*}

(*
fun
  fib :: "nat \<Rightarrow> nat"
where
\<dots>
*)

text {* Prove the lemma: *}

lemma
  shows "fib n = fib (n + 2) - fib (n + 1)"
sorry

section {* Task 4 (harder) *}

text {*

  Define the function calculating the power
  of two numbers and the factorial function.

*}

(*
fun 
 pow :: "nat \<Rightarrow> nat \<Rightarrow> nat" ("_ \<up> _")
where
\<dots>
*)

(*
fun
  fac :: "nat \<Rightarrow> nat"
where
\<dots>
*)

text {* 
  
  Prove the following inequality. 

  Hint 1: Use inductions.

  Hint 2: The lemmas aux1 and aux2 might be helpful.

  *}

lemma
  shows "2 \<up> (n+4) < fac (n+4)"
sorry

lemma aux1: 
  fixes a b c::"nat"
  assumes a: "a < b" "0 < c"
  shows " (a * c) < (b * c)"
using a by (auto)

lemma aux2: 
  fixes a b::"nat"
  assumes h: "0 < a"
  shows "0 < a \<up> b"
using h by (induct b) (auto)

section {* Task 5 (easy) *}

text {*

  Define the Ackermann Function. The cases
  should be

   ack 0 m = \<dots>
   ack (Suc n) 0 = \<dots>
   ack (Suc n) (Suc m) = \<dots>

  *}

(*
fun 
  ack :: "nat \<Rightarrow> nat \<Rightarrow> nat"
where
\<dots>
*)

text {* Establish the next three lemmas. *}

lemma ack1:
  shows "ack 0 y = Suc y"
sorry

lemma ack2:
  shows "ack (Suc 0) y = Suc (Suc y)"
sorry

lemma ack3:
  shows "ack (Suc (Suc 0)) y = 2 * y + 3"
sorry

section {* Task 6 (?) *}

text {* Prove the following lemma. *}

lemma ack4:
  shows "ack (Suc (Suc (Suc 0))) y = 2 \<up> (y + 3) - 3"
sorry
  

end