theory Ex02_Tut 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' _ = undefined" lemma "listsum xs = listsum' xs" sorry datatype 'a ltree = TODO fun inorder :: "'a ltree \ 'a list" where "inorder _ = undefined" fun fold_ltree :: "('a \ 's \ 's) \ 'a ltree \ 's \ 's" where "fold_ltree _ = undefined" lemma "fold f (inorder t) s = fold_ltree f t s" sorry lemma "inorder (mirror t) = rev (inorder t)" sorry fun shuffles :: "'a list \ 'a list \ 'a list list" where "shuffles _ = undefined" lemma "zs \set (shuffles xs ys) \ length zs = length xs + length ys" sorry end