theory Hw05
  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
  "deldups [] = []"
| "deldups (x#xs) = (if x\<in>set xs then deldups xs else x#deldups xs)"

lemma deldups_set:
  shows "set (deldups xs) = set xs"
by (induct xs) (auto)


text {* Prove the lemma: *}

lemma 
  shows "distinct (deldups xs)"
by (induct xs) (auto simp add: deldups_set)

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"
proof -
  { assume a: "A\<longrightarrow>B"
    assume b: "B\<longrightarrow>C"
    assume c: "A"
    from a c have "B" by (rule mp)
    with b have "C" by (rule mp)
  }
  then have "\<lbrakk>A \<longrightarrow> B;B \<longrightarrow> C\<rbrakk> \<Longrightarrow> A \<longrightarrow> C" by (rule impI)
  then have "A \<longrightarrow> B \<Longrightarrow> (B \<longrightarrow> C) \<longrightarrow> A \<longrightarrow> C" by (rule impI)
  then show "(A \<longrightarrow> B) \<longrightarrow> (B\<longrightarrow>C) \<longrightarrow> A \<longrightarrow> C" by (rule impI)
qed

section {* Task 3 (easy) *}

text {* 
  
  Define the function calculating the Fibonacci 
  numbers. 

*}

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

text {* Prove the lemma: *}

lemma
  shows "fib n = fib (n + 2) - fib (n + 1)"
by (induct n) (auto)

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
  "m \<up> 0 = 1"
| "m \<up> (Suc n) = m * (m \<up> n)"

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

text {* 
  
  Prove the following inequality. 

  Hint 1: Use inductions.

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

  *}

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)

lemma
  shows "2 \<up> (n+4) < fac (n+4)"
proof(induct n)
  case 0
  then show "2 \<up> (0 + 4) < fac (0 + 4)" by (simp add: nat_number)
next
  case (Suc n)
  have ih: "2 \<up> (n + 4) < fac (n + 4)" by fact
  have "2 \<up> (Suc n + 4) = 2 * (2 \<up> (n + 4))" by (simp add: nat_number)
  also have "\<dots> < (Suc n + 4) * (2 \<up> (n + 4))" 
    by (rule aux1) (simp_all add: nat_number aux2)
  also have "\<dots> < (Suc n + 4) * fac (n + 4)" using ih by (auto)
  also have "\<dots> = fac (Suc n + 4)" by (simp add: nat_number)
  finally show "2 \<up> (Suc n + 4) < fac (Suc n + 4)" by simp
qed

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
  "ack 0 m = Suc m"
| "ack (Suc n) 0 = ack n (Suc 0)"
| "ack (Suc n) (Suc m) = ack n (ack (Suc n) m)"

text {* Establish the next three lemmas. *}

lemma ack1:
  shows "ack 0 y = Suc y"
by simp

lemma ack2:
  shows "ack (Suc 0) y = Suc (Suc y)"
by (induct y) (auto)

lemma ack3:
  shows "ack (Suc (Suc 0)) y = 2 * y + 3"
by (induct y) (auto simp add: ack2)

section {* Task 6 (?) *}

text {* Prove the following lemma. *}

lemma m6: "6 < 2 \<up> ((Suc y) + 3)"
  by (induct y) (auto simp add: nat_number)
  
lemma ack4_susanne:
  shows "ack (Suc (Suc (Suc 0))) y = (2 \<up> (y + 3)) - 3"
proof (induct y)
  case 0
  show " ack (Suc (Suc (Suc 0))) 0 = (2 \<up> (0 + 3)) - 3" by (simp add: nat_number)
next
  case (Suc y)
  have ih: "ack (Suc (Suc (Suc 0))) y = (2 \<up> (y + 3)) - 3" by fact
  have a: "ack (Suc (Suc 0)) ((2 \<up> (y + 3)) - 3) = 2 * ((2 \<up> (y + 3)) - 3) + 3" using ack3 by simp
    have "2 *(2 \<up> (y+3)) = 2 \<up> (Suc y + 3)" by (simp add: nat_number)
  then have b: "2 * ((2 \<up> (y+3)) - 3) + 3 = (2 \<up> (Suc y + 3)) - 6 + 3" by (auto)
  have c: "ack (Suc (Suc (Suc 0))) (Suc y) = ack (Suc (Suc 0)) (ack (Suc (Suc (Suc 0))) y)" by simp
  have "6 < (2 \<up> (Suc y + 3))" by (rule m6)
  then have d: "(2 \<up> (Suc y + 3)) - 6 + 3 = (2 \<up> (Suc y + 3)) - 3" by auto 
  from a b c d show "ack (Suc (Suc (Suc 0))) (Suc y) = (2 \<up> (Suc y + 3)) - 3" using ih by simp
qed

end