section \Solutions for Session 1\ theory Solutions01 imports Main begin (*avoid theory name prefix for ambiguous constant names in output*) declare [[names_short]] \ \A data type for finite lists/stacks.\ datatype 'a list = Nil | Cons 'a "'a list" \ \Appending two lists.\ fun append :: "'a list \ 'a list \ 'a list" where "append Nil ys = ys" | "append (Cons x xs) ys = Cons x (append xs ys)" \ \Reversing a list.\ fun rev :: "'a list \ '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 \Exercise 1\ fun map :: "('a \ 'b) \ 'a list \ '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 \ g) xs" by (induction xs) auto subsection \Exercise 2\ lemma map_append: "map f (append xs ys) = append (map f xs) (map f ys)" by (induction xs) auto subsection \Exercise 3\ fun concat :: "'a list list \ '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 \Exercise 4\ fun add :: "nat \ nat \ 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 \Exercise 5\ fun length :: "'a list \ 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 \Exercise 6\ fun sum_list :: "nat list \ 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 \Exercise 7\ fun snoc :: "'a list \ 'a \ '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