Theory Pairing_Heap_List2_Analysis
subsection ‹Okasaki's Pairing Heap (Modified)›
theory Pairing_Heap_List2_Analysis
imports
Pairing_Heap.Pairing_Heap_List2
Amortized_Framework
Priority_Queue_ops_merge
Lemmas_log
begin
text
‹Amortized analysis of a modified version of the pairing heaps
defined by Okasaki \<^cite>‹"Okasaki"›.›
fun lift_hp :: "'b ⇒ ('a hp ⇒ 'b) ⇒ 'a heap ⇒ 'b" where
"lift_hp c f None = c" |
"lift_hp c f (Some h) = f h"
fun size_hps :: "'a hp list ⇒ nat" where
"size_hps(Hp x hsl # hsr) = size_hps hsl + size_hps hsr + 1" |
"size_hps [] = 0"
definition size_hp :: "'a hp ⇒ nat" where
[simp]: "size_hp h = size_hps(hps h) + 1"
fun Φ_hps :: "'a hp list ⇒ real" where
"Φ_hps [] = 0" |
"Φ_hps (Hp x hsl # hsr) = Φ_hps hsl + Φ_hps hsr + log 2 (size_hps hsl + size_hps hsr + 1)"
definition Φ_hp :: "'a hp ⇒ real" where
[simp]: "Φ_hp h = Φ_hps (hps h) + log 2 (size_hps(hps(h))+1)"
abbreviation Φ :: "'a heap ⇒ real" where
"Φ ≡ lift_hp 0 Φ_hp"
abbreviation size_heap :: "'a heap ⇒ nat" where
"size_heap ≡ lift_hp 0 size_hp"
lemma Φ_hps_ge0: "Φ_hps hs ≥ 0"
by (induction hs rule: size_hps.induct) auto
declare algebra_simps[simp]
lemma size_hps_Cons[simp]: "size_hps(h # hs) = size_hp h + size_hps hs"
by(cases h) simp
lemma link2: "link (Hp x lx) h = (case h of (Hp y ly) ⇒
(if x < y then Hp x (Hp y ly # lx) else Hp y (Hp x lx # ly)))"
by(simp split: hp.split)
lemma size_hps_link: "size_hps(hps (link h1 h2)) = size_hp h1 + size_hp h2 - 1"
by (induction rule: link.induct) simp_all
lemma pass⇩1_size[simp]: "size_hps (pass⇩1 hs) = size_hps hs"
by (induct hs rule: pass⇩1.induct) (simp_all add: size_hps_link)
lemma pass⇩2_None[simp]: "pass⇩2 hs = None ⟷ hs = []"
by(cases hs) auto
lemma ΔΦ_insert:
"Φ (Pairing_Heap_List2.insert x h) - Φ h ≤ log 2 (size_heap h + 1)"
by(induct h)(auto simp: link2 split: hp.split)
lemma ΔΦ_link: "Φ_hp (link h1 h2) - Φ_hp h1 - Φ_hp h2 ≤ 2 * log 2 (size_hp h1 + size_hp h2)"
by (induction h1 h2 rule: link.induct) (simp add: add_increasing)
fun sum_ub :: "'a hp list ⇒ real" where
"sum_ub [] = 0"
| "sum_ub [Hp _ _] = 0"
| "sum_ub [Hp _ lx, Hp _ ly] = 2*log 2 (2 + size_hps lx + size_hps ly)"
| "sum_ub (Hp _ lx # Hp _ ly # ry) = 2*log 2 (2 + size_hps lx + size_hps ly + size_hps ry)
- 2*log 2 (size_hps ry) - 2 + sum_ub ry"
lemma ΔΦ_pass1_sum_ub: "Φ_hps (pass⇩1 h) - Φ_hps h ≤ sum_ub h"
proof (induction h rule: sum_ub.induct)
case (3 lx x ly y)
have 0: "⋀x y::real. 0 ≤ x ⟹ x ≤ y ⟹ x ≤ 2*y" by linarith
show ?case by (simp add: add_increasing 0)
next
case (4 x hsx y hsy z hsize_hp)
let ?ry = "z # hsize_hp"
let ?rx = "Hp y hsy # ?ry"
let ?h = "Hp x hsx # ?rx"
have "Φ_hps(pass⇩1 ?h) - Φ_hps ?h
≤ log 2 (1 + size_hps hsx + size_hps hsy) - log 2 (1 + size_hps hsy + size_hps ?ry) + sum_ub ?ry"
using "4.IH" by simp
also have "log 2 (1 + size_hps hsx + size_hps hsy) - log 2 (1 + size_hps hsy + size_hps ?ry)
≤ 2*log 2 (size_hps ?h) - 2*log 2 (size_hps ?ry) - 2"
proof -
have "log 2 (1 + size_hps hsx + size_hps hsy) + log 2 (size_hps ?ry) - 2*log 2 (size_hps ?h)
= log 2 ((1 + size_hps hsx + size_hps hsy)/(size_hps ?h) ) + log 2 (size_hps ?ry / size_hps ?h)"
by (simp add: log_divide)
also have "… ≤ -2"
proof -
have "2 + …
≤ 2*log 2 ((1 + size_hps hsx + size_hps hsy) / size_hps ?h + size_hps ?ry / size_hps ?h)"
using ld_sum_inequality [of "(1 + size_hps hsx + size_hps hsy) / size_hps ?h" "(size_hps ?ry / size_hps ?h)"] by simp
also have "… ≤ 0" by (simp add: field_simps log_divide add_pos_nonneg)
finally show ?thesis by linarith
qed
finally have "log 2 (1 + size_hps hsx + size_hps hsy) + log 2 (size_hps ?ry) + 2
≤ 2*log 2 (size_hps ?h)" by simp
moreover have "log 2 (size_hps ?ry) ≤ log 2 (size_hps ?rx)" by simp
ultimately have "log 2 (1 + size_hps hsx + size_hps hsy) - …
≤ 2*log 2 (size_hps ?h) - 2*log 2 (size_hps ?ry) - 2" by linarith
thus ?thesis by simp
qed
finally show ?case by (simp)
qed simp_all
lemma ΔΦ_pass1: assumes "hs ≠ []"
shows "Φ_hps (pass⇩1 hs) - Φ_hps hs ≤ 2 * log 2 (size_hps hs) - length hs + 2"
proof -
have "sum_ub hs ≤ 2 * log 2 (size_hps hs) - length hs + 2"
using assms by (induct hs rule: sum_ub.induct) (simp_all)
thus ?thesis using ΔΦ_pass1_sum_ub[of hs] by linarith
qed
lemma size_hps_pass2: "pass⇩2 hs = Some h ⟹ size_hps hs = size_hps(hps h)+1"
apply(induction hs arbitrary: h rule: Φ_hps.induct)
apply (auto simp: link2 split: option.split hp.split)
done
lemma ΔΦ_pass2: "hs ≠ [] ⟹ Φ (pass⇩2 hs) - Φ_hps hs ≤ log 2 (size_hps hs)"
proof (induction hs)
case (Cons h hs)
thus ?case
proof -
obtain x hs2 where [simp]: "h = Hp x hs2" by (metis hp.exhaust)
show ?thesis
proof (cases "pass⇩2 hs")
case [simp]: (Some h2)
obtain y hs3 where [simp]: "h2 = Hp y hs3" by (metis hp.exhaust)
from size_hps_pass2[OF Some] Cons show ?thesis
by(cases "hs=[]")(auto simp: add_mono)
qed simp
qed
qed simp
lemma ΔΦ_del_min: assumes "hps h ≠ []"
shows "Φ (del_min (Some h)) - Φ (Some h)
≤ 3 * log 2 (size_hps(hps h)) - length(hps h) + 2"
proof -
let ?ΔΦ⇩1 = "Φ_hps(hps h) - Φ_hp h"
let ?ΔΦ⇩2 = "Φ(pass⇩2(pass⇩1 (hps h))) - Φ_hps (hps h)"
let ?ΔΦ = "Φ (del_min (Some h)) - Φ (Some h)"
have "Φ(pass⇩2(pass⇩1(hps h))) - Φ_hps (pass⇩1(hps h)) ≤ log 2 (size_hps(hps h))"
using ΔΦ_pass2[of "pass⇩1(hps h)"] using size_hps.elims assms by force
moreover have "Φ_hps (pass⇩1 (hps h)) - Φ_hps (hps h) ≤ 2*… - length (hps h) + 2"
using ΔΦ_pass1[OF assms] by blast
moreover have "?ΔΦ⇩1 ≤ 0" by (cases h) simp
moreover have "?ΔΦ = ?ΔΦ⇩1 + ?ΔΦ⇩2" by (cases h) simp
ultimately show ?thesis by linarith
qed
fun exec :: "'a :: linorder op ⇒ 'a heap list ⇒ 'a heap" where
"exec Empty [] = None" |
"exec Del_min [h] = del_min h" |
"exec (Insert x) [h] = Pairing_Heap_List2.insert x h" |
"exec Merge [h1,h2] = merge h1 h2"
fun T⇩p⇩a⇩s⇩s⇩1 :: "'a hp list ⇒ nat" where
"T⇩p⇩a⇩s⇩s⇩1 [] = 1"
| "T⇩p⇩a⇩s⇩s⇩1 [_] = 1"
| "T⇩p⇩a⇩s⇩s⇩1 (_ # _ # hs) = 1 + T⇩p⇩a⇩s⇩s⇩1 hs"
fun T⇩p⇩a⇩s⇩s⇩2 :: "'a hp list ⇒ nat" where
"T⇩p⇩a⇩s⇩s⇩2 [] = 1" |
"T⇩p⇩a⇩s⇩s⇩2 (_ # hs) = 1 + T⇩p⇩a⇩s⇩s⇩2 hs"
fun cost :: "'a :: linorder op ⇒ 'a heap list ⇒ nat" where
"cost Empty _ = 1" |
"cost Del_min [None] = 1" |
"cost Del_min [Some(Hp x hs)] = 1 + T⇩p⇩a⇩s⇩s⇩2 (pass⇩1 hs) + T⇩p⇩a⇩s⇩s⇩1 hs" |
"cost (Insert a) _ = 1" |
"cost Merge _ = 1"
fun U :: "'a :: linorder op ⇒ 'a heap list ⇒ real" where
"U Empty _ = 1" |
"U (Insert a) [h] = log 2 (size_heap h + 1) + 1" |
"U Del_min [h] = 3*log 2 (size_heap h + 1) + 5" |
"U Merge [h1,h2] = 2*log 2 (size_heap h1 + size_heap h2 + 1) + 1"
interpretation pairing: Amortized
where arity = arity and exec = exec and cost = cost and inv = "λ_. True"
and Φ = Φ and U = U
proof (standard, goal_cases)
case (2 s) show ?case by (cases s) (auto simp: Φ_hps_ge0)
next
case (3 ss f) show ?case
proof (cases f)
case Empty with 3 show ?thesis by(auto)
next
case Insert
thus ?thesis using Insert ΔΦ_insert 3 by auto
next
case [simp]: Del_min
then obtain ho where [simp]: "ss = [ho]" using 3 by auto
show ?thesis
proof (cases ho)
case [simp]: (Some h)
show ?thesis
proof (cases h)
case [simp]: (Hp x hs)
have "T⇩p⇩a⇩s⇩s⇩2 (pass⇩1 hs) + T⇩p⇩a⇩s⇩s⇩1 hs ≤ 2 + length hs"
by (induct hs rule: pass⇩1.induct) simp_all
hence "cost f ss ≤ 1 + …" by simp
moreover have "Φ (del_min ho) - Φ ho ≤ 3*log 2 (size_heap ho + 1) - length hs + 2"
proof (cases "hs = []")
case False
hence "Φ (del_min ho) - Φ ho ≤ 3*log 2 (size_hps hs) - length hs + 2"
using ΔΦ_del_min[of h] by simp
also have "… ≤ 3*log 2 (size_heap ho + 1) - length hs + 2"
using False size_hps.elims by force
finally show ?thesis .
qed simp
ultimately show ?thesis by simp
qed
qed simp
next
case [simp]: Merge
then obtain ho1 ho2 where [simp]: "ss = [ho1, ho2]"
using 3 by(auto simp: numeral_eq_Suc)
show ?thesis
proof (cases "ho1 = None ∨ ho2 = None")
case True thus ?thesis by auto
next
case False
then obtain h1 h2 where [simp]: "ho1 = Some h1" "ho2 = Some h2" by auto
have "Φ (merge ho1 ho2) - Φ ho1 - Φ ho2 ≤ 2 * log 2 (size_heap ho1 + size_heap ho2)"
using ΔΦ_link[of h1 h2] by simp
also have "… ≤ 2 * log 2 (size_hp h1 + size_hp h2 + 1)" by (simp)
finally show ?thesis by(simp)
qed
qed
qed simp
end