(*Author: Harald Zankl*)

section \<open>Homework of Functional Programming Week 7\<close>

theory S07
  imports Exercises
begin

fun rev :: "'a list \<Rightarrow> 'a list"
  where
    "rev Nil = Nil"
  | "rev (Cons x xs) = app (rev xs) (Cons x Nil)"

-- \<open>Exercise 5\<close>
lemma rev_app: 
  "rev (app xs ys) = app (rev ys) (rev xs)" 
proof (induct "xs")
  case Nil
  have "rev (app Nil ys) = rev ys" by simp
  also have "... = app (rev ys) Nil" by (simp add: app_Nil)
  also have "... = app (rev ys) (rev Nil)" by simp
  finally show ?case by simp
next
  case IH: (Cons x xs)
  have "rev (app (Cons x xs) ys) = rev (Cons x (app xs ys))" by simp
  also have "... = app (rev (app xs ys)) (Cons x Nil)" by simp
  also have "... = app (app (rev ys) (rev xs)) (Cons x Nil)" by (simp add: IH)
  also have "... = app (rev ys) (app (rev xs) (Cons x Nil))" by (simp add: app_assoc)
  also have "... = app (rev ys) (rev (Cons x xs))" by simp
  finally show ?case by simp
qed

-- \<open>Exercise 6\<close>
lemma rev_rev: 
  "rev (rev xs) = xs"
proof (induct "xs")
  case Nil 
  then show ?case by simp
next
  case IH: (Cons x xs)
  have "rev (rev (Cons x xs)) = rev (app (rev xs) (Cons x Nil))" by simp
  also have "... = app (rev (Cons x Nil)) (rev (rev xs))" by (simp add: rev_app)
  also have "... = app (Cons x Nil) (rev (rev xs))" by simp
  also have "... = app (Cons x Nil) xs" by (simp add: IH)
  also have "... = Cons x (app Nil xs)" by simp
  also have "... = Cons x xs" by simp
  finally show ?case by simp
qed

end