(*<*) theory sol04 imports "../../fds_ss17/Demos/BST_Demo" begin (*>*) text {* \ExerciseSheet{4}{19.~5.~2017} *} text \ \Exercise{Height-Preserving In-Order Join} Write a function that joins two binary trees such that \<^item> The in-order traversal of the new tree is the concatenation of the in-order traversals of the original tree \<^item> The new tree is at most one higher than the highest original tree Hint: Once you got the function right, proofs are easy! \ fun join :: "'a tree \ 'a tree \ 'a tree" (*<*) where "join t Leaf = t" | "join Leaf t = t" | "join (Node l1 a1 r1) (Node l2 a2 r2) = (case join r1 l2 of Leaf \ Node l1 a1 (Node Leaf a2 r2) | Node l b r \ Node (Node l1 a1 l) b (Node r a2 r2))" (*>*) lemma "inorder(join t1 t2) = inorder t1 @ inorder t2" (*<*) apply(induction t1 t2 rule: join.induct) apply (auto split: tree.split) done (*>*) lemma "height(join t1 t2) \ max (height t1) (height t2) + 1" (*<*) apply(induction t1 t2 rule: join.induct) apply (auto split: tree.split) done (*>*) text \ \Exercise{Enumerate Elements in Interval} Write a function to in-order enumerate all elements of a BST in a given interval. I.e., \in_range t u v\ shall enumerate all elements \x\ with \u\x\v\. Write a recursive function that does not descend into nodes that definitely contain no elements in the given range. \ fun in_range :: "'a::linorder tree \ 'a \ 'a \ 'a list" (*<*) where "in_range Leaf u v = []" | "in_range (Node l x r) u v = (if ux \ x\v then [x] else []) @ (if x*) text \Show that you enumerate the right set of elements\ lemma "bst t \ set (in_range t u v) = {x\set_tree t. u\x \ x\v}" (*<*) apply (induction t) apply auto done (*>*) (*<*) lemma [simp]: "[v] = xs@w#ys \ (xs=[] \ ys=[] \ v=w)" by (metis Nil_is_append_conv append_self_conv2 butlast.simps(2) butlast_append list.discI nth_Cons_0) (*lemma [simp]: "NO_MATCH x [] \ [] = x \ x = []" by auto *) lemma [simp]: "[] = filter P x \ filter P x = []" by auto (*>*) text \Show that your enumeration is actually in-order\ lemma "bst t \ in_range t u v = filter (\x. u\x \ x\v) (inorder t)" (*<*) apply (induction t) apply (auto simp: filter_empty_conv split!: if_splits) done (*>*) (*<*) (* Different function, less lemmas \ *) fun in_range' where "in_range' Leaf u v = []" | "in_range' (Node l x r) u v = (if u\x \ x\v then in_range' l u v@x#in_range' r u v else if x \ v then in_range' r u v else if u\x then in_range' l u v else [] )" lemma "bst t \ set (in_range' t u v) = {x\set_tree t. u\x \ x\v}" apply (induction t) apply auto done lemma "bst t \ in_range' t u v = filter (\x. u\x \ x\v) (inorder t)" apply (induction t) apply (auto simp: filter_empty_conv) done (*>*) text \\Exercise{Pretty Printing of Binary Trees}\ text \Define a function that checks whether two binary trees have the same structure. The values at the nodes may differ.\ fun bin_tree2 :: "'a tree \ 'b tree \ bool" (*<*) where "bin_tree2 Leaf Leaf \ True" | "bin_tree2 (Node l x r) (Node l' x' r') \ bin_tree2 l l' \ bin_tree2 r r'" | "bin_tree2 _ _ \ False" (*>*) text \While this function itself is not very useful, the induction rule generated by the function package is! It allows simultaneous induction over two trees:\ print_statement bin_tree2.induct text \Binary trees can be uniquely pretty-printed by emitting a symbol L for a leaf, and a symbol N for a node. Each N is followed by the pretty-prints of the left and right tree. No additional brackets are required!\ datatype 'a tchar = L | N 'a fun pretty :: "'a tree \ 'a tchar list" (*<*) where "pretty Leaf = [L]" | "pretty (Node l x r) = N x # pretty l @ pretty r" (*>*) text \Show that pretty-printing is actually unique, i.e., no two different trees are pretty-printed the same way. Hint: Auxiliary lemma. Simultaneous induction over both trees. \ (*<*) lemma pretty_unique_aux: "pretty t @ xs = pretty t' @ xs' \ t=t'" apply (induction t t' arbitrary: xs xs' rule: bin_tree2.induct) apply auto apply fastforce done (*>*) lemma pretty_unique: "pretty t = pretty t' \ t=t'" (*<*) using pretty_unique_aux[where xs="[]" and xs'="[]"] by simp (*>*) (*<*) end (*>*)