Theory Skew_Heap_Analysis
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 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"
using a_merge[of "Node Leaf a Leaf" "t"]
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 + Φ(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] = 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 + 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) + 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