section \<open>Solutions for Session 1\<close>

theory Solutions01
  imports Main
begin

(*avoid theory name prefix for ambiguous constant names in output*)
declare [[names_short]]

\<comment> \<open>A data type for finite lists/stacks.\<close>
datatype 'a list = Nil | Cons 'a "'a list"

\<comment> \<open>Appending two lists.\<close>
fun append :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
  where
    "append Nil ys = ys"
  | "append (Cons x xs) ys = Cons x (append xs ys)"

\<comment> \<open>Reversing a list.\<close>
fun rev :: "'a list \<Rightarrow> 'a list"
  where
    "rev Nil = Nil"
  | "rev (Cons x xs) = append (rev xs) (Cons x Nil)"

lemma append_Nil_right: "append xs Nil = xs"
  by (induction xs) auto

lemma append_assoc: "append (append xs ys) zs = append xs (append ys zs)"
  by (induction xs) auto

lemma rev_append: "rev (append xs ys) = append (rev ys) (rev xs)"
  by (induction xs) (auto simp: append_Nil_right append_assoc)

lemma rev_rev: "rev (rev xs) = xs"
  by (induction xs) (auto simp: rev_append)


subsection \<open>Exercise 1\<close>

fun map :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list"
  where
    "map f Nil = Nil"
  | "map f (Cons x xs) = Cons (f x) (map f xs)"

lemma map_map: "map f (map g xs) = map (f \<circ> g) xs"
  by (induction xs) auto


subsection \<open>Exercise 2\<close>

lemma map_append: "map f (append xs ys) = append (map f xs) (map f ys)"
  by (induction xs) auto


subsection \<open>Exercise 3\<close>

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

lemma concat_append: "concat (append xs ys) = append (concat xs) (concat ys)"
  by (induction xs) (auto simp: append_assoc)


subsection \<open>Exercise 4\<close>

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

lemma add_0_right: "add x 0 = x"
  by (induction x) auto

lemma add_Suc_right: "add x (Suc y) = Suc (add x y)"
  by (induction x) auto

lemma add_commute: "add x y = add y x"
  by (induction x) (auto simp: add_0_right add_Suc_right)


subsection \<open>Exercise 5\<close>

fun length :: "'a list \<Rightarrow> nat"
  where
    "length Nil = 0"
  | "length (Cons x xs) = Suc (length xs)"

lemma length_map: "length (map f xs) = length xs"
  by (induction xs) auto


subsection \<open>Exercise 6\<close>

fun sum_list :: "nat list \<Rightarrow> nat"
  where
    "sum_list Nil = 0"
  | "sum_list (Cons x xs) = add x (sum_list xs)"

lemma length_append: "length (append xs ys) = add (length xs) (length ys)"
  by (induction xs) auto

lemma length_concat: "length (concat xs) = sum_list (map length xs)"
  by (induction xs) (auto simp: length_append)


subsection \<open>Exercise 7\<close>

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

lemma snoc_append: "snoc (append xs ys) z = append xs (snoc ys z)"
  by (induction xs) auto

lemma snoc_rev: "snoc (rev xs) y = rev (Cons y xs)"
  by (induction xs) (auto simp: snoc_append append_assoc)

end