(* \$Id: ex.thy,v 1.3 2011/06/28 18:11:39 webertj Exp \$ Author: Martin Strecker *) header {* Folding Lists and Trees *} (*<*) theory ex imports Main begin (*>*) subsubsection {* Some more list functions *} text {* Recall the summation function *} primrec sum :: "nat list \ nat" where "sum [] = 0" | "sum (x # xs) = x + sum xs" text {* In the Isabelle library, you will find (in the theory {\tt List.thy}) the functions @{text foldr} and @{text foldl}, which allow you to define some list functions, among them @{text sum} and @{text length}. Show the following: *} lemma sum_foldr: "sum xs = foldr (op +) xs 0" (*<*) oops (*>*) lemma length_foldr: "length xs = foldr (\ x res. 1 + res) xs 0" (*<*) oops (*>*) text {* Repeated application of @{text foldr} and @{text map} has the disadvantage that a list is traversed several times. A single traversal is sufficient, as illustrated by the following example: *} lemma "sum (map (\ x. x + 3) xs) = foldr h xs b" (*<*) oops (*>*) text {* Find terms @{text h} and @{text b} which solve this equation. *} text {* Generalize this result, i.e.\ show for appropriate @{text h} and @{text b}: *} lemma "foldr g (map f xs) a = foldr h xs b" (*<*) oops (*>*) text {* Hint: Isabelle can help you find the solution if you use the equalities arising during a proof attempt. *} text {* The following function @{text rev_acc} reverses a list in linear time: *} primrec rev_acc :: "['a list, 'a list] \ 'a list" where "rev_acc [] ys = ys" | "rev_acc (x#xs) ys = (rev_acc xs (x#ys))" text {* Show that @{text rev_acc} can be defined by means of @{text foldl}. *} lemma rev_acc_foldl: "rev_acc xs a = foldl (\ ys x. x # ys) a xs" (*<*) oops (*>*) text {* Prove the following distributivity property for @{text sum}: *} lemma sum_append [simp]: "sum (xs @ ys) = sum xs + sum ys" (*<*) oops (*>*) text {* Prove a similar property for @{text foldr}, i.e.\ something like @{text "foldr f (xs @ ys) a = f (foldr f xs a) (foldr f ys a)"}. However, you will have to strengthen the premises by taking into account algebraic properties of @{text f} and @{text a}. *} lemma foldr_append: "foldr f (xs @ ys) a = f (foldr f xs a) (foldr f ys a)" (*<*) oops (*>*) text {* Now, define the function @{text prod}, which computes the product of all list elements *} (*<*) consts (*>*) prod :: "nat list \ nat" text {* directly with the aid of a fold and prove the following: *} lemma "prod (xs @ ys) = prod xs * prod ys" (*<*) oops (*>*) subsubsection {* Functions on Trees *} text {* Consider the following type of binary trees: *} datatype 'a tree = Tip | Node "'a tree" 'a "'a tree" text {* Define functions which convert a tree into a list by traversing it in pre-, resp.\ postorder: *} (*<*) consts (*>*) preorder :: "'a tree \ 'a list" postorder :: "'a tree \ 'a list" text {* You have certainly realized that computation of postorder traversal can be efficiently realized with an accumulator, in analogy to @{text rev_acc}: *} consts postorder_acc :: "['a tree, 'a list] \ 'a list" text {* Define this function and show: *} lemma "postorder_acc t xs = (postorder t) @ xs" (*<*) oops (*>*) text {* @{text postorder_acc} is the instance of a function @{text foldl_tree}, which is similar to @{text foldl}. *} consts foldl_tree :: "('b => 'a => 'b) \ 'b \ 'a tree \ 'b" text {* Show the following: *} lemma "\ a. postorder_acc t a = foldl_tree (\ xs x. Cons x xs) a t" (*<*) oops (*>*) text {* Define a function @{text tree_sum} that computes the sum of the elements of a tree of natural numbers: *} consts tree_sum :: "nat tree \ nat" text {* and show that this function satisfies *} lemma "tree_sum t = sum (preorder t)" (*<*) oops (*>*) (*<*) end (*>*)