theory Recursive_Function_Exercises imports Main begin fun to_set :: "'a list \ 'a set" where "to_set [] = {}" | "to_set (x#xs) = {x} \ to_set xs" lemma shows "to_set (xs@ys) = to_set xs \ to_set ys" sorry lemma shows "to_set (xs@[x]) = {x} \ to_set xs" sorry lemma shows "to_set (rev xs) = to_set xs" sorry lemma shows "to_set (filter p xs) = { x. x\to_set xs \ p x}" sorry fun take :: "nat \ 'a list \ 'a list" where "take m [] = []" | "take m (x#xs) = (case m of 0 \ [] | Suc m \ x#take m xs)" lemma shows "to_set (take m xs) \ to_set xs" sorry lemma shows "length (take m xs) = min (length xs) m" sorry lemma shows "take m (map f xs) = map f (take m xs)" sorry (*replace the consts command with an implementation*) consts mem :: "'a \ 'a list \ bool" lemma shows "mem e xs \ e \ to_set xs" sorry lemma assumes "mem e xs" shows "mem e (xs@ys)" sorry lemma assumes "mem e xs" shows "mem (f e) (map f xs)" sorry consts append :: "'a list \ 'a list \ 'a list" consts reverse :: "'a list \ 'a list" lemma shows "reverse (reverse xs) = xs" sorry lemma shows "reverse (append xs ys) = append (reverse ys) (reverse xs)" sorry (*replace the consts command with an implementation*) consts concat_map :: "'a list \ ('a \ 'b list) \ 'b list" lemma shows "concat_map xs (\x. [x]) = xs" sorry lemma shows "concat_map [x] f = f x" sorry lemma shows "concat_map (concat_map xs f) g = concat_map xs (\y. concat_map (f y) g)" sorry datatype 'a tree = Leaf | Node "'a" "'a forest" and 'a forest = Nil | Cons "'a tree" "'a forest" consts count_tree :: "'a tree \ 'a \ nat" count_forest :: "'a forest \ 'a \ nat" consts member_tree :: "'a tree \ 'a \ bool" member_forest :: "'a forest \ 'a \ bool" lemma shows "(member_tree t x \ (count_tree t x \ 0)) \ (member_forest f x \ (count_forest f x \ 0))" sorry end