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