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 t \ size t + 1" by (induction t) (auto simp: rh_def) corollary Glog: "lrh t \ log 2 (size1 t)" by (metis Gexp le_log2_of_power size1_size) lemma Dexp: "2 ^ rlh t \ size t + 1" by (induction t) (auto simp: rh_def) corollary Dlog: "rlh t \ log 2 (size1 t)" by (metis Dexp le_log2_of_power size1_size) 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 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 "size1(merge t1 t2) = size1 t1 + size1 t2 - 1" by(simp add: size1_size size_merge) 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 tree \ int" where "T_insert a t = T_merge (Node Leaf a Leaf) t + 1" -lemma a_insert: "T_insert a t + \(Skew_Heap.insert a t) - \ t \ 3 * log 2 (size1 t + 2) + 2" +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) +by (simp add: numeral_eq_Suc T_insert_def rh_def) 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 t + \(del_min t) - \ t \ 3 * log 2 (size1 t + 2) + 2" +lemma a_del_min: "T_del_min t + \(skew_heap.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 t1 t2 \ 0" by(induction t1 t2 rule: T_merge.induct) auto fun exec :: "'a::linorder op \ 'a tree list \ 'a tree" where "exec Empty [] = Leaf" | -"exec (Insert a) [t] = Skew_Heap.insert a t" | -"exec Del_min [t] = del_min t" | +"exec (Insert a) [t] = skew_heap.insert a t" | +"exec Del_min [t] = skew_heap.del_min t" | "exec Merge [t1,t2] = merge t1 t2" fun cost :: "'a::linorder op \ 'a tree list \ nat" where "cost Empty [] = 1" | -"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 (Insert a) [t] = T_merge (Node Leaf a Leaf) t + 1" | +"cost Del_min [t] = (case t of Leaf \ 1 | Node t1 a t2 \ T_merge t1 t2 + 1)" | "cost Merge [t1,t2] = T_merge t1 t2" fun U where "U Empty [] = 1" | -"U (Insert _) [t] = 3 * log 2 (size1 t + 2) + 1" | -"U Del_min [t] = 3 * log 2 (size1 t + 2) + 3" | +"U (Insert _) [t] = 3 * log 2 (size1 t + 2) + 2" | +"U Del_min [t] = 3 * log 2 (size1 t + 2) + 2" | "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 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 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 t where [simp]: "ss = [t]" using 3(2) by (auto) thus ?thesis 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 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,135 +1,79 @@ section "Skew Heap" theory Skew_Heap imports "HOL-Library.Tree_Multiset" "HOL-Library.Pattern_Aliases" - "HOL-Data_Structures.Priority_Queue_Specs" + "HOL-Data_Structures.Heaps" 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 +The implementation below could be generalized to separate the elements from their priorities.\ - -subsection "Get Minimum" - -fun get_min :: "('a::linorder) tree \ 'a" where -"get_min(Node l m r) = m" - -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) 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 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 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) 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" +lemma size_merge: "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" +lemma size_merge2: "size(merge2 t1 t2) = size t1 + size t2" by(induction t1 t2 rule: merge2.induct) auto 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 t1 t2) = set_tree t1 \ set_tree t2" by (metis mset_merge set_mset_tree set_mset_union) lemma heap_merge: - "heap t1 \ heap t2 \ heap (merge t1 t2)" + "\ 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 tree \ 'a tree" where -"insert a t = merge (Node Leaf a Leaf) t" - -lemma heap_insert: "heap t \ heap (insert a t)" -by (simp add: insert_def heap_merge) - -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 tree \ 'a tree" where -"del_min Leaf = Leaf" | -"del_min (Node l m r) = merge l r" - -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 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 +interpretation skew_heap: Heap_Merge +where merge = merge 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) + case 1 thus ?case by(simp add: mset_merge) 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) + case 2 thus ?case by(simp add: heap_merge) qed end