theory Ex02_Tut_Sol
  imports Main
begin

thm fold.simps

fun list_sum :: "nat list \<Rightarrow> nat" where
  "list_sum [] = 0"
| "list_sum (x#xs) = x + list_sum xs"

definition list_sum' :: "nat list \<Rightarrow> nat" where
  "list_sum' xs \<equiv> fold (+) xs 0"

lemma aux: "fold (+) xs a = list_sum xs + a"
  by (induction xs arbitrary: a) auto

lemma  "list_sum xs = list_sum' xs"
unfolding list_sum'_def by (simp add: aux)

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

fun inorder :: "'a ltree \<Rightarrow> 'a list" where
  "inorder (Leaf x) = [x]"
| "inorder (Node l r) = inorder l @ inorder r"

value "inorder (Node (Leaf 1) (Leaf (2::nat)))"


fun fold_ltree :: "('a \<Rightarrow> 's \<Rightarrow> 's) \<Rightarrow> 'a ltree \<Rightarrow> 's \<Rightarrow> 's" where
  "fold_ltree f (Leaf x) s = f x s"
| "fold_ltree f (Node l r) s = fold_ltree f r (fold_ltree f l s)"  

lemma  "fold f (inorder t) s = fold_ltree f t s"  
  by (induction t arbitrary: s) auto

fun mirror where
  "mirror (Node l r) = Node (mirror r) (mirror l)"
| "mirror (Leaf x) = Leaf x"      

lemma  "inorder (mirror t) = rev (inorder t)"  
  by (induction t) auto



fun shuffles :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list list" where
  "shuffles xs [] = [xs]"
| "shuffles [] ys = [ys]"  
| "shuffles (x#xs) (y#ys) = map (\<lambda>xs. x # xs) (shuffles xs (y#ys)) @ map (\<lambda>ys. y # ys) (shuffles (x#xs) ys)"  

lemma  "zs \<in> set (shuffles xs ys) \<Longrightarrow> length zs = length xs + length ys"
  apply (induction xs ys arbitrary: zs rule: shuffles.induct)
    apply auto  
  done

end