theory Ex02_Tut_Sol imports Main begin thm fold.simps fun listsum :: "nat list \ nat" where "listsum [] = 0" | "listsum (x#xs) = x + listsum xs" definition listsum' :: "nat list \ nat" where "listsum' xs = fold (+) xs 0" lemma aux: "fold (+) xs a = listsum xs + a" by (induction xs arbitrary: a) auto lemma "listsum xs = listsum' xs" unfolding listsum'_def by (simp add: aux) datatype 'a ltree = Leaf 'a | Node "'a ltree" "'a ltree" fun inorder :: "'a ltree \ '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 \ 's \ 's) \ 'a ltree \ 's \ '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 \ 'a list \ 'a list list" where "shuffles xs [] = [xs]" | "shuffles [] ys = [ys]" | "shuffles (x#xs) (y#ys) = map (\xs. x # xs) (shuffles xs (y#ys)) @ map (\ys. y # ys) (shuffles (x#xs) ys)" lemma "zs \set (shuffles xs ys) \ length zs = length xs + length ys" apply (induction xs ys arbitrary: zs rule: shuffles.induct) apply auto done end