(*<*) theory tmpl10 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 _ _ = undefined" lemma mset_lh_insert: "mset_tree (lh_insert x t) = mset_tree t + {# x #}" oops lemma "heap t \ heap (lh_insert x t)" oops lemma "ltree t \ ltree (lh_insert x t)" oops fun t_lh_insert :: "'a::ord \ 'a lheap \ nat" where "t_lh_insert _ _ = undefined" lemma "t_lh_insert x t \ rank t + 1" oops 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 = Foo_Bar 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 definition empty :: "('a,'s) bs_pq" where "empty = undefined" fun is_empty :: "('a,'s) bs_pq \ bool" where "is_empty _ \ undefined" fun insert :: "'a \ ('a,'s) bs_pq \ ('a,'s) bs_pq" where "insert _ _ = undefined" fun get_min :: "('a,'s) bs_pq \ 'a" where "get_min _ = undefined" fun del_min :: "('a,'s) bs_pq \ ('a,'s) bs_pq" where "del_min _ = undefined" fun invar :: "('a,'s) bs_pq \ bool" where "invar _ = undefined" fun mset :: "('a,'s) bs_pq \ 'a multiset" where "mset _ = undefined" 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 sorry next case (2 q) then show ?case sorry next case (3 q x) then show ?case sorry next case (4 q) then show ?case sorry next case (5 q) then show ?case sorry next case 6 then show ?case sorry next case (7 q x) then show ?case sorry next case (8 q) then show ?case sorry 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 (*>*)