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

text \<open>For this exercise sheet you will have to figure out several auxiliary lemmas on your own!\<close>

theory Exercise03
  imports 
    Main
begin

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

text \<open>Consider the append function from the lecture\<close>

fun app :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list" where 
  "app [] ys = ys" 
| "app (x # xs) ys = x # (app xs ys)" 

datatype 'a tree = Leaf | Node "'a tree" 'a "'a tree" 

text \<open>The function \<open>count\<close> counts the number of nodes in a tree.\<close>
fun count :: "'a tree \<Rightarrow> nat" where
  "count Leaf = 0" 
| "count (Node l x r) = count l + 1 + count r" 

text \<open>Flatten a tree into a list.\<close>
fun flatten :: "'a tree \<Rightarrow> 'a list" where
  "flatten Leaf = []" 
| "flatten (Node l x r) = app (flatten l) (x # flatten r)"

text \<open>Prove the following property:\<close>

lemma len_flatten: "length (flatten t) = count t" sorry


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

text \<open>Consider insertion sort\<close>

fun insert_sorted :: "'a :: linorder \<Rightarrow> 'a list \<Rightarrow> 'a list" where
  "insert_sorted x Nil = Cons x Nil" 
| "insert_sorted x (Cons y ys) = (case x \<le> y of 
      True \<Rightarrow> Cons x (Cons y ys)
    | False \<Rightarrow> Cons y (insert_sorted x ys))" 

fun ins_sort :: "'a :: linorder list \<Rightarrow> 'a list" where
  "ins_sort Nil = Nil" 
| "ins_sort (Cons x xs) = insert_sorted x (ins_sort xs)" 


text \<open>Prove the property that insertion sort preserves the length.\<close>

lemma length_ins_sort: "length (ins_sort xs) = length xs" sorry


section \<open>Exercise 3 -- Natural numbers\<close>

text \<open>Isabelle contains natural numbers corresponding to the datatype definition:

  datatype nat = 0 | Suc nat

  Standard arithmetic operations are already predefined, e.g., +, *, <, ...,
  but in this exercise we provide our own arithmetic operations and prove
  properties about these.
\<close>

fun add :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
  "add x 0 = x" 
| "add x (Suc y) = Suc (add x y)" 

fun mult :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
  "mult x 0 = 0" 
| "mult x (Suc y) = add x (mult x y)" 


subsection \<open>Exercise 3.1 -- 2 points\<close>

text \<open>Prove that addition is commutative.\<close>

lemma add_comm: "add x y = add y x" sorry


subsection \<open>Exercise 3.2 -- 3 points\<close>

text \<open>Prove that multiplication is commutative\<close>

text \<open>Hint: you even can use commutativity of addition as simplification
  rule without introducing non-termination: Isabelle has special-treatment 
  of commutativity laws which then normalize terms like @{term "add t1 t2"}
  to either @{term "add t1 t2"} or @{term "add t2 t1"}, depending on whether
  some internal order on terms makes @{term t1} larger or smaller than @{term t2}.
  However, the evaluation "add t1 t2 = add t2 t1 = add t1 t2 = ... " will not happen.\<close>

text \<open>Example: here y and x are swapped once.\<close>

lemma "add y x = z" proof (simp add: add_comm) oops

lemma mult_comm: "mult x y = mult y x" sorry

end