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