(*<*) theory tut10 imports "../../../Public/Thys/Leftist_Heap" begin (*>*) text {* \ExerciseSheet{10}{30.~6.~2017} *} text \ \Exercise{Insert for Leftist Heap} \<^item> Define a function to directly insert an element into a leftist heap. Do not construct an intermediate heap like insert via meld does! \<^item> Show that your function is correct \<^item> Define a timing function for your insert function, and show that it is linearly bounded by the rank of the tree. \ fun lh_insert :: "'a::ord \ 'a lheap \ 'a lheap" where "lh_insert a \\ = \1,\\,a,\\\" | "lh_insert a \h,l,b,r\ = ( if a\b then node l a (lh_insert b r) else node l b (lh_insert a r) )" find_theorems node ltree find_theorems node heap find_theorems node mset_tree lemma mset_tree_node[simp]: "mset_tree (node l a r) = mset_tree l + {#a#} + mset_tree r" unfolding node_def by auto lemma mset_lh_insert[simp]: shows "mset_tree (lh_insert x t) = mset_tree t + {# x #}" apply (induction x t rule: lh_insert.induct) apply (auto) done declare heap_node[simp] lemma heap_lh_insert[intro, simp]: "heap t \ heap (lh_insert x t)" by (induction x t rule: lh_insert.induct) force+ lemma "heap t \ heap (lh_insert x t)" apply (induction x t rule: lh_insert.induct) subgoal by (simp) subgoal by (force) done declare ltree_node[simp] lemma "ltree t \ ltree (lh_insert x t)" by (induction x t rule: lh_insert.induct) auto fun t_lh_insert :: "'a::ord \ 'a lheap \ nat" where "t_lh_insert a \\ = 1" | "t_lh_insert a \h,l,b,r\ = 1 + ( if a\b then 1+t_lh_insert b r else 1+t_lh_insert a r )" lemma "t_lh_insert x t \ 2*rank t + 1" by (induction x t rule: lh_insert.induct) auto text \ \Exercise{Bootstrapping a Priority Queue} Given a generic priority queue implementation with \O(1)\ \empty\, \is_empty\ operations, \O(f\<^sub>1 n)\ insert, and \O(f\<^sub>2 n)\ \get_min\ and \del_min\ operations. Derive an implementation with \O(1)\ \get_min\, and the asymptotic complexities of the other operations unchanged! Hint: Store the current minimal element! As you know nothing about \f\<^sub>1\ and \f\<^sub>2\, you must not use \get_min/del_min\ in your new \insert\ operation, and vice versa! \ text \For technical reasons, you have to define the new implementations type outside the locale!\ datatype ('a,'s) bs_pq = Empty | Heap 'a 's locale Bs_Priority_Queue = orig: Priority_Queue orig_empty orig_is_empty orig_insert orig_get_min orig_del_min orig_invar orig_mset for orig_empty orig_is_empty orig_insert orig_get_min orig_del_min orig_invar and orig_mset :: "'s \ 'a::linorder multiset" begin text \In here, the original implementation is available with the prefix \orig\, e.g. \ term orig_empty term orig_invar thm orig.invar_empty fun mset :: "('a,'s) bs_pq \ 'a multiset" where "mset Empty = {#}" | "mset (Heap a h) = orig_mset h" definition empty :: "('a,'s) bs_pq" where "empty = Empty" fun is_empty :: "('a,'s) bs_pq \ bool" where "is_empty Empty \ True" | "is_empty _ \ False" fun insert :: "'a \ ('a,'s) bs_pq \ ('a,'s) bs_pq" where "insert a Empty = Heap a (orig_insert a orig_empty)" | "insert a (Heap b h) = Heap (min a b) (orig_insert a h)" fun get_min :: "('a,'s) bs_pq \ 'a" where "get_min (Heap a _) = a" fun del_min :: "('a,'s) bs_pq \ ('a,'s) bs_pq" where "del_min (Heap a h) = (let h = orig_del_min h in if orig_is_empty h then Empty else Heap (orig_get_min h) h )" fun invar :: "('a,'s) bs_pq \ bool" where "invar Empty = True" | "invar (Heap a h) \ orig_invar h \ orig_mset h \ {#} \ a = Min_mset (orig_mset h)" text \Show that your new implementation satisfies the priority queue interface!\ sublocale Priority_Queue empty is_empty insert get_min del_min invar mset apply unfold_locales proof goal_cases case 1 then show ?case by (auto simp: empty_def) next case (2 q) then show ?case by (cases q) (auto) next case (3 q x) then show ?case by (cases q) (auto) next case (4 q) then show ?case by (cases q) (auto) next case (5 q) then show ?case by (cases q) (auto) next case 6 then show ?case by (auto simp: empty_def) next case (7 q x) then show ?case by (cases q) (auto) next case (8 q) then show ?case by (cases q) (auto) qed end text\ \Homework{Constructing a Heap from a List of Elements}{7.~7.~2017} The naive solution of starting with the empty heap and inserting the elements one by one can be improved by repeatedly merging heaps of roughly equal size. Start by turning the list of elements into a list of singleton heaps. Now make repeated passes over the list, merging adjacent pairs of heaps in each pass (thus halving the list length) until only a single heap is left. It can be shown that this takes linear time. Define a function \heap_of_list ::\ @{typ "'a list \ 'a lheap"} and prove its functional correctness. \ definition heap_of_list :: "'a::ord list \ 'a lheap" where "heap_of_list _ = undefined" lemma mset_heap_of_list: "mset_tree (heap_of_list xs) = mset xs" sorry lemma heap_heap_of_list: "heap (heap_of_list xs)" sorry lemma ltree_ltree_of_list: "ltree (heap_of_list xs)" sorry (*<*) end (*>*)