diff --git a/thys/Amortized_Complexity/Skew_Heap_Analysis.thy b/thys/Amortized_Complexity/Skew_Heap_Analysis.thy --- a/thys/Amortized_Complexity/Skew_Heap_Analysis.thy +++ b/thys/Amortized_Complexity/Skew_Heap_Analysis.thy @@ -1,201 +1,201 @@ (* Author: Tobias Nipkow *) section "Skew Heap Analysis" theory Skew_Heap_Analysis imports Complex_Main Skew_Heap.Skew_Heap Amortized_Framework Priority_Queue_ops_merge begin text\The following proof is a simplified version of the one by Kaldewaij and Schoenmakers~\cite{KaldewaijS-IPL91}.\ text \right-heavy:\ definition rh :: "'a tree => 'a tree => nat" where "rh l r = (if size l < size r then 1 else 0)" text \Function \\\ in \cite{KaldewaijS-IPL91}: number of right-heavy nodes on left spine.\ fun lrh :: "'a tree \ nat" where "lrh Leaf = 0" | "lrh (Node l _ r) = rh l r + lrh l" text \Function \\\ in \cite{KaldewaijS-IPL91}: number of not-right-heavy nodes on right spine.\ fun rlh :: "'a tree \ nat" where "rlh Leaf = 0" | "rlh (Node l _ r) = (1 - rh l r) + rlh r" -lemma Gexp: "2 ^ lrh h \ size h + 1" -by (induction h) (auto simp: rh_def) +lemma Gexp: "2 ^ lrh t \ size t + 1" +by (induction t) (auto simp: rh_def) -corollary Glog: "lrh h \ log 2 (size1 h)" +corollary Glog: "lrh t \ log 2 (size1 t)" by (metis Gexp le_log2_of_power size1_size) -lemma Dexp: "2 ^ rlh h \ size h + 1" -by (induction h) (auto simp: rh_def) +lemma Dexp: "2 ^ rlh t \ size t + 1" +by (induction t) (auto simp: rh_def) -corollary Dlog: "rlh h \ log 2 (size1 h)" +corollary Dlog: "rlh t \ log 2 (size1 t)" by (metis Dexp le_log2_of_power size1_size) -function t_merge :: "'a::linorder heap \ 'a heap \ nat" where -"t_merge Leaf h = 1" | -"t_merge h Leaf = 1" | +function t_merge :: "'a::linorder tree \ 'a tree \ nat" where +"t_merge Leaf t = 1" | +"t_merge t Leaf = 1" | "t_merge (Node l1 a1 r1) (Node l2 a2 r2) = (if a1 \ a2 then t_merge (Node l2 a2 r2) r1 else t_merge (Node l1 a1 r1) r2) + 1" by pat_completeness auto termination by (relation "measure (\(x, y). size x + size y)") auto -fun \ :: "'a heap \ int" where +fun \ :: "'a tree \ int" where "\ Leaf = 0" | "\ (Node l _ r) = \ l + \ r + rh l r" lemma \_nneg: "\ t \ 0" by (induction t) auto lemma plus_log_le_2log_plus: "\ x > 0; y > 0; b > 1 \ \ log b x + log b y \ 2 * log b (x + y)" by(subst mult_2; rule add_mono; auto) lemma rh1: "rh l r \ 1" by(simp add: rh_def) lemma amor_le_long: "t_merge t1 t2 + \ (merge t1 t2) - \ t1 - \ t2 \ lrh(merge t1 t2) + rlh t1 + rlh t2 + 1" proof (induction t1 t2 rule: merge.induct) case 1 thus ?case by simp next case 2 thus ?case by simp next case (3 l1 a1 r1 l2 a2 r2) show ?case proof (cases "a1 \ a2") case True let ?t1 = "Node l1 a1 r1" let ?t2 = "Node l2 a2 r2" let ?m = "merge ?t2 r1" have "t_merge ?t1 ?t2 + \ (merge ?t1 ?t2) - \ ?t1 - \ ?t2 = t_merge ?t2 r1 + 1 + \ ?m + \ l1 + rh ?m l1 - \ ?t1 - \ ?t2" using True by (simp) also have "\ = t_merge ?t2 r1 + 1 + \ ?m + rh ?m l1 - \ r1 - rh l1 r1 - \ ?t2" by simp also have "\ \ lrh ?m + rlh ?t2 + rlh r1 + rh ?m l1 + 2 - rh l1 r1" using "3.IH"(1)[OF True] by linarith also have "\ = lrh ?m + rlh ?t2 + rlh r1 + rh ?m l1 + 1 + (1 - rh l1 r1)" using rh1[of l1 r1] by (simp) also have "\ = lrh ?m + rlh ?t2 + rlh ?t1 + rh ?m l1 + 1" by (simp) also have "\ = lrh (merge ?t1 ?t2) + rlh ?t1 + rlh ?t2 + 1" using True by(simp) finally show ?thesis . next case False with 3 show ?thesis by auto qed qed lemma amor_le: "t_merge t1 t2 + \ (merge t1 t2) - \ t1 - \ t2 \ lrh(merge t1 t2) + rlh t1 + rlh t2 + 1" by(induction t1 t2 rule: merge.induct)(auto) lemma a_merge: "t_merge t1 t2 + \(merge t1 t2) - \ t1 - \ t2 \ 3 * log 2 (size1 t1 + size1 t2) + 1" (is "?l \ _") proof - have "?l \ lrh(merge t1 t2) + rlh t1 + rlh t2 + 1" using amor_le[of t1 t2] by arith also have "\ = real(lrh(merge t1 t2)) + rlh t1 + rlh t2 + 1" by simp also have "\ = real(lrh(merge t1 t2)) + (real(rlh t1) + rlh t2) + 1" by simp also have "rlh t1 \ log 2 (size1 t1)" by(rule Dlog) also have "rlh t2 \ log 2 (size1 t2)" by(rule Dlog) also have "lrh (merge t1 t2) \ log 2 (size1(merge t1 t2))" by(rule Glog) also have "size1(merge t1 t2) = size1 t1 + size1 t2 - 1" by(simp add: size1_size) also have "log 2 (size1 t1 + size1 t2 - 1) \ log 2 (size1 t1 + size1 t2)" by(simp add: size1_size) also have "log 2 (size1 t1) + log 2 (size1 t2) \ 2 * log 2 (real(size1 t1) + (size1 t2))" by(rule plus_log_le_2log_plus) (auto simp: size1_size) finally show ?thesis by(simp) qed -definition t_insert :: "'a::linorder \ 'a heap \ int" where -"t_insert a h = t_merge (Node Leaf a Leaf) h + 1" +definition t_insert :: "'a::linorder \ 'a tree \ int" where +"t_insert a t = t_merge (Node Leaf a Leaf) t + 1" -lemma a_insert: "t_insert a h + \(Skew_Heap.insert a h) - \ h \ 3 * log 2 (size1 h + 2) + 2" -using a_merge[of "Node Leaf a Leaf" "h"] +lemma a_insert: "t_insert a t + \(Skew_Heap.insert a t) - \ t \ 3 * log 2 (size1 t + 2) + 2" +using a_merge[of "Node Leaf a Leaf" "t"] by (simp add: numeral_eq_Suc t_insert_def Skew_Heap.insert_def rh_def) -definition t_del_min :: "('a::linorder) heap \ int" where -"t_del_min h = (case h of Leaf \ 1 | Node t1 a t2 \ t_merge t1 t2 + 1)" +definition t_del_min :: "('a::linorder) tree \ int" where +"t_del_min t = (case t of Leaf \ 1 | Node t1 a t2 \ t_merge t1 t2 + 1)" -lemma a_del_min: "t_del_min h + \(del_min h) - \ h \ 3 * log 2 (size1 h + 2) + 2" -proof (cases h) +lemma a_del_min: "t_del_min t + \(del_min t) - \ t \ 3 * log 2 (size1 t + 2) + 2" +proof (cases t) case Leaf thus ?thesis by (simp add: t_del_min_def) next case (Node t1 _ t2) have [arith]: "log 2 (2 + (real (size t1) + real (size t2))) \ log 2 (4 + (real (size t1) + real (size t2)))" by simp from Node show ?thesis using a_merge[of t1 t2] by (simp add: size1_size t_del_min_def rh_def) qed subsubsection "Instantiation of Amortized Framework" -lemma t_merge_nneg: "t_merge h1 h2 \ 0" -by(induction h1 h2 rule: t_merge.induct) auto +lemma t_merge_nneg: "t_merge t1 t2 \ 0" +by(induction t1 t2 rule: t_merge.induct) auto -fun exec :: "'a::linorder op \ 'a heap list \ 'a heap" where +fun exec :: "'a::linorder op \ 'a tree list \ 'a tree" where "exec Empty [] = Leaf" | -"exec (Insert a) [h] = Skew_Heap.insert a h" | -"exec Del_min [h] = del_min h" | -"exec Merge [h1,h2] = merge h1 h2" +"exec (Insert a) [t] = Skew_Heap.insert a t" | +"exec Del_min [t] = del_min t" | +"exec Merge [t1,t2] = merge t1 t2" -fun cost :: "'a::linorder op \ 'a heap list \ nat" where +fun cost :: "'a::linorder op \ 'a tree list \ nat" where "cost Empty [] = 1" | -"cost (Insert a) [h] = t_merge (Node Leaf a Leaf) h" | -"cost Del_min [h] = (case h of Leaf \ 1 | Node t1 a t2 \ t_merge t1 t2)" | -"cost Merge [h1,h2] = t_merge h1 h2" +"cost (Insert a) [t] = t_merge (Node Leaf a Leaf) t" | +"cost Del_min [t] = (case t of Leaf \ 1 | Node t1 a t2 \ t_merge t1 t2)" | +"cost Merge [t1,t2] = t_merge t1 t2" fun U where "U Empty [] = 1" | -"U (Insert _) [h] = 3 * log 2 (size1 h + 2) + 1" | -"U Del_min [h] = 3 * log 2 (size1 h + 2) + 3" | -"U Merge [h1,h2] = 3 * log 2 (size1 h1 + size1 h2) + 1" +"U (Insert _) [t] = 3 * log 2 (size1 t + 2) + 1" | +"U Del_min [t] = 3 * log 2 (size1 t + 2) + 3" | +"U Merge [t1,t2] = 3 * log 2 (size1 t1 + size1 t2) + 1" interpretation Amortized where arity = arity and exec = exec and inv = "\_. True" and cost = cost and \ = \ and U = U proof (standard, goal_cases) case 1 show ?case by simp next - case (2 h) show ?case using \_nneg[of h] by linarith + case (2 t) show ?case using \_nneg[of t] by linarith next case (3 ss f) show ?case proof (cases f) case Empty thus ?thesis using 3(2) by (auto) next case [simp]: (Insert a) - obtain h where [simp]: "ss = [h]" using 3(2) by (auto) - thus ?thesis using a_merge[of "Node Leaf a Leaf" "h"] + obtain t where [simp]: "ss = [t]" using 3(2) by (auto) + thus ?thesis using a_merge[of "Node Leaf a Leaf" "t"] by (simp add: numeral_eq_Suc insert_def rh_def t_merge_nneg) next case [simp]: Del_min - obtain h where [simp]: "ss = [h]" using 3(2) by (auto) + obtain t where [simp]: "ss = [t]" using 3(2) by (auto) thus ?thesis - proof (cases h) + proof (cases t) case Leaf with Del_min show ?thesis by simp next case (Node t1 _ t2) have [arith]: "log 2 (2 + (real (size t1) + real (size t2))) \ log 2 (4 + (real (size t1) + real (size t2)))" by simp from Del_min Node show ?thesis using a_merge[of t1 t2] by (simp add: size1_size t_merge_nneg) qed next case [simp]: Merge - obtain h1 h2 where "ss = [h1,h2]" using 3(2) by (auto simp: numeral_eq_Suc) - thus ?thesis using a_merge[of h1 h2] by (simp add: t_merge_nneg) + obtain t1 t2 where "ss = [t1,t2]" using 3(2) by (auto simp: numeral_eq_Suc) + thus ?thesis using a_merge[of t1 t2] by (simp add: t_merge_nneg) qed qed end diff --git a/thys/Skew_Heap/Skew_Heap.thy b/thys/Skew_Heap/Skew_Heap.thy --- a/thys/Skew_Heap/Skew_Heap.thy +++ b/thys/Skew_Heap/Skew_Heap.thy @@ -1,137 +1,135 @@ section "Skew Heap" theory Skew_Heap imports "HOL-Library.Tree_Multiset" "HOL-Library.Pattern_Aliases" "HOL-Data_Structures.Priority_Queue_Specs" begin unbundle pattern_aliases text\Skew heaps~\cite{SleatorT-SIAM86} are possibly the simplest functional priority queues that have logarithmic (albeit amortized) complexity. The implementation below should be generalized to separate the elements from their priorities.\ -type_synonym 'a heap = "'a tree" - subsection "Get Minimum" -fun get_min :: "'a::linorder heap \ 'a" where +fun get_min :: "('a::linorder) tree \ 'a" where "get_min(Node l m r) = m" -lemma get_min: "\ heap h; h \ Leaf \ \ get_min h = Min_mset (mset_tree h)" +lemma get_min: "\ heap t; t \ Leaf \ \ get_min t = Min_mset (mset_tree t)" by (auto simp add: eq_Min_iff neq_Leaf_iff) subsection "Merge" -function merge :: "('a::linorder) heap \ 'a heap \ 'a heap" where -"merge Leaf h = h" | -"merge h Leaf = h" | -"merge (Node l1 a1 r1 =: h1) (Node l2 a2 r2 =: h2) = - (if a1 \ a2 then Node (merge h2 r1) a1 l1 - else Node (merge h1 r2) a2 l2)" +function merge :: "('a::linorder) tree \ 'a tree \ 'a tree" where +"merge Leaf t = t" | +"merge t Leaf = t" | +"merge (Node l1 a1 r1 =: t1) (Node l2 a2 r2 =: t2) = + (if a1 \ a2 then Node (merge t2 r1) a1 l1 + else Node (merge t1 r2) a2 l2)" by pat_completeness auto termination by (relation "measure (\(x, y). size x + size y)") auto -lemma merge_code: "merge h1 h2 = - (case h1 of - Leaf \ h2 | - Node l1 a1 r1 \ (case h2 of - Leaf \ h1 | +lemma merge_code: "merge t1 t2 = + (case t1 of + Leaf \ t2 | + Node l1 a1 r1 \ (case t2 of + Leaf \ t1 | Node l2 a2 r2 \ (if a1 \ a2 - then Node (merge h2 r1) a1 l1 - else Node (merge h1 r2) a2 l2)))" + then Node (merge t2 r1) a1 l1 + else Node (merge t1 r2) a2 l2)))" by(auto split: tree.split) text\An alternative version that always walks to the Leaf of both heaps:\ -function merge2 :: "('a::linorder) heap \ 'a heap \ 'a heap" where +function merge2 :: "('a::linorder) tree \ 'a tree \ 'a tree" where "merge2 Leaf Leaf = Leaf" | "merge2 Leaf (Node l2 a2 r2) = Node (merge2 r2 Leaf) a2 l2" | "merge2 (Node l1 a1 r1) Leaf = Node (merge2 r1 Leaf) a1 l1" | "merge2 (Node l1 a1 r1) (Node l2 a2 r2) = (if a1 \ a2 then Node (merge2 (Node l2 a2 r2) r1) a1 l1 else Node (merge2 (Node l1 a1 r1) r2) a2 l2)" by pat_completeness auto termination by (relation "measure (\(x, y). size x + size y)") auto lemma size_merge[simp]: "size(merge t1 t2) = size t1 + size t2" by(induction t1 t2 rule: merge.induct) auto lemma size_merge2[simp]: "size(merge2 t1 t2) = size t1 + size t2" by(induction t1 t2 rule: merge2.induct) auto -lemma mset_merge: "mset_tree (merge h1 h2) = mset_tree h1 + mset_tree h2" -by (induction h1 h2 rule: merge.induct) (auto simp add: ac_simps) +lemma mset_merge: "mset_tree (merge t1 t2) = mset_tree t1 + mset_tree t2" +by (induction t1 t2 rule: merge.induct) (auto simp add: ac_simps) -lemma set_merge: "set_tree (merge h1 h2) = set_tree h1 \ set_tree h2" +lemma set_merge: "set_tree (merge t1 t2) = set_tree t1 \ set_tree t2" by (metis mset_merge set_mset_tree set_mset_union) lemma heap_merge: - "heap h1 \ heap h2 \ heap (merge h1 h2)" -by (induction h1 h2 rule: merge.induct)(auto simp: ball_Un set_merge) + "heap t1 \ heap t2 \ heap (merge t1 t2)" +by (induction t1 t2 rule: merge.induct)(auto simp: ball_Un set_merge) subsection "Insert" hide_const (open) insert -definition insert :: "'a::linorder \ 'a heap \ 'a heap" where +definition insert :: "'a::linorder \ 'a tree \ 'a tree" where "insert a t = merge (Node Leaf a Leaf) t" -lemma heap_insert: "heap h \ heap (insert a h)" +lemma heap_insert: "heap t \ heap (insert a t)" by (simp add: insert_def heap_merge) -lemma mset_insert: "mset_tree (insert a h) = {#a#} + mset_tree h" +lemma mset_insert: "mset_tree (insert a t) = {#a#} + mset_tree t" by (auto simp: mset_merge insert_def) subsection "Delete minimum" -fun del_min :: "'a::linorder heap \ 'a heap" where +fun del_min :: "'a::linorder tree \ 'a tree" where "del_min Leaf = Leaf" | "del_min (Node l m r) = merge l r" -lemma heap_del_min: "heap h \ heap (del_min h)" -by (cases h) (auto simp: heap_merge) +lemma heap_del_min: "heap t \ heap (del_min t)" +by (cases t) (auto simp: heap_merge) -lemma mset_del_min: "mset_tree (del_min h) = mset_tree h - {# get_min h #}" -by (cases h) (auto simp: mset_merge ac_simps) +lemma mset_del_min: "mset_tree (del_min t) = mset_tree t - {# get_min t #}" +by (cases t) (auto simp: mset_merge ac_simps) interpretation skew_heap: Priority_Queue_Merge where empty = Leaf and is_empty = "\h. h = Leaf" and merge = merge and insert = insert and del_min = del_min and get_min = get_min and invar = heap and mset = mset_tree proof(standard, goal_cases) case 1 show ?case by simp next case (2 q) show ?case by (cases q) auto next case 3 show ?case by(simp add: mset_insert) next case 4 show ?case by(rule mset_del_min) next case 5 thus ?case using get_min mset_tree.simps(1) by blast next case 6 thus ?case by(simp) next case 7 thus ?case by(simp add: heap_insert) next case 8 thus ?case by(simp add: heap_del_min) next case 9 thus ?case by(simp add: mset_merge) next case 10 thus ?case by(simp add: heap_merge) qed end