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
"HOL-Data_Structures.Define_Time_Function"
begin
text
‹Amortized analysis of a modified version of the pairing heaps defined by Okasaki \<^cite>‹"Okasaki"›.
Simplified version of proof in the Nipkow and Brinkop paper.›
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"
consts sz :: "'a ⇒ nat"
overloading
size_hps ≡ "sz :: 'a hp list ⇒ nat"
size_hp ≡ "sz :: 'a hp ⇒ nat"
size_heap ≡ "sz :: 'a heap ⇒ nat"
begin
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 = sz(hps h) + 1"
definition size_heap :: "'a heap ⇒ nat" where
[simp]: "size_heap ≡ lift_hp 0 sz"
end
consts Φ :: "'a ⇒ real"
overloading
Φ_hps ≡ "Φ :: 'a hp list ⇒ real"
Φ_hp ≡ "Φ :: 'a hp ⇒ real"
Φ_heap ≡ "Φ :: 'a heap ⇒ real"
begin
fun Φ_hps :: "'a hp list ⇒ real" where
"Φ_hps [] = 0" |
"Φ_hps (Hp x hsl # hsr) = Φ_hps hsl + Φ_hps hsr + log 2 (sz hsl + sz hsr + 1)"
definition Φ_hp :: "'a hp ⇒ real" where
[simp]: "Φ_hp h = Φ (hps h) + log 2 (sz(hps(h))+1)"
definition Φ_heap :: "'a heap ⇒ real" where
[simp]: "Φ_heap ≡ lift_hp 0 Φ"
end
lemma Φ_hps_ge0: "Φ (hs::_ hp list) ≥ 0"
by (induction hs rule: size_hps.induct) auto
declare algebra_simps[simp]
lemma sz_hps_Cons[simp]: "sz(h # hs) = sz (h::_ hp) + sz 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 sz_hps_link: "sz(hps (link h1 h2)) = sz h1 + sz h2 - 1"
by (induction rule: link.induct) simp_all
lemma pass⇩1_size[simp]: "sz (pass⇩1 hs) = sz hs"
by (induction hs rule: pass⇩1.induct) (simp_all add: sz_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 (sz h + 1)"
by(cases h)(auto simp: link2 split: hp.split)
lemma ΔΦ_link: "Φ (link h1 h2) - Φ h1 - Φ h2 ≤ 2 * log 2 (sz h1 + sz h2)"
by (cases "(h1,h2)" rule: link.cases) (simp add: add_increasing)
lemma ΔΦ_pass1: "Φ (pass⇩1 hs) - Φ hs ≤ 2 * log 2 (sz hs + 1) - length hs + 2"
proof (induction hs rule: pass⇩1.induct)
case (1 h1 h2 hs)
let ?hs' = "h1 # h2 # hs" let ?m = "sz hs"
obtain x1 hs1 x2 hs2 where h12: "h1 = Hp x1 hs1" "h2 = Hp x2 hs2"
using hp.exhaust_sel by blast
let ?n1 = "sz hs1" let ?n2 = "sz hs2"
have "Φ (pass⇩1 ?hs') - Φ ?hs' = Φ (pass⇩1 hs) + log 2 (?n1+?n2+1) - Φ hs - log 2 (?n2+?m+1)"
by (simp add: h12)
also have "… ≤ log 2 (?n1+?n2+1) - log 2 (?n2+?m+1) + 2 * log 2 (?m+1) - length hs + 2"
using 1 by (simp)
also have "… ≤ 2 * log 2 (?n1+?n2+?m+2) - log 2 (?n2+?m+1) + log 2 (?m+1) - length hs"
using ld_sum_inequality [of "?n1+?n2+1" "?m+1"] by(simp)
also have "… ≤ 2 * log 2 (?n1+?n2+?m+2) - length hs" by simp
also have "… = 2 * log 2 (sz ?hs') - length ?hs' + 2" using h12 by simp
also have "… ≤ 2 * log 2 (sz ?hs' + 1) - length ?hs' + 2" using h12 by simp
finally show ?case .
qed simp_all
lemma size_hps_pass2: "sz(pass⇩2 hs) = sz hs"
apply(induction hs rule: pass⇩2.induct)
apply(auto simp: sz_hps_link split: option.split)
done
lemma ΔΦ_pass2: "hs ≠ [] ⟹ Φ (pass⇩2 hs) - Φ hs ≤ log 2 (sz hs)"
proof (induction hs)
case IH: (Cons h1 hs)
obtain x hs1 where [simp]: "h1 = Hp x hs1" by (metis hp.exhaust)
show ?case
proof (cases "hs = []")
case False
then obtain h2 where [simp]: "pass⇩2 hs = Some h2" by fastforce
then obtain y hs2 where [simp]: "h2 = Hp y hs2" by (metis hp.exhaust)
from False size_hps_pass2[of hs,symmetric] IH(1) have ?thesis
by(simp add: add_mono)
let ?n1 = "sz hs1" let ?n2 = "sz hs2"
have *: "Φ (link h1 h2) = Φ hs1 + Φ hs2 + log 2 (?n1+?n2+1) + log 2 (?n1+?n2+2)"
by simp
have [simp]: "sz hs = sz hs2 + 1" using size_hps_pass2[of hs] by simp
hence IH2: "Φ (hs2) - Φ hs ≤ 0" using IH(1)[OF False] by simp
have "Φ (pass⇩2 (h1 # hs)) - Φ (h1 # hs) = Φ (link h1 h2) - (Φ hs1 + Φ hs + log 2 (?n1+sz hs+1))"
by simp
also have "… = Φ hs2 + log 2 (?n1+?n2+1) - Φ hs"
using * by simp
also have "… ≤ log 2 (?n1+?n2+1)"
using IH2 by simp
also have "… ≤ log 2 (sz(h1 # hs))" by simp
finally show ?thesis .
qed simp
qed simp
corollary ΔΦ_pass2': "Φ (pass⇩2 hs) - Φ hs ≤ log 2 (sz hs + 1)"
proof cases
assume "hs = []" thus ?thesis by simp
next
assume "hs ≠ []"
hence "log 2 (sz hs) ≤ log 2 (sz hs + 1)" by (auto simp: neq_Nil_conv)
then show ?thesis using ΔΦ_pass2[OF ‹hs ≠ []›] by linarith
qed
lemma ΔΦ_del_min:
shows "Φ (del_min (Some h)) - Φ (Some h)
≤ 2 * log 2 (sz(hps h) + 1) - length (hps h) + 2"
proof -
obtain x hs where [simp]: "h = Hp x hs" by (meson hp.exhaust_sel)
have "Φ (del_min (Some h)) - Φ (Some h) =
Φ (pass⇩2 (pass⇩1 hs)) - (log 2 (sz hs + 1) + Φ hs)" by simp
also have "… ≤ Φ (pass⇩1 hs) - Φ hs"
using ΔΦ_pass2'[of "pass⇩1 hs"] by(simp)
also have "… ≤ 2 * log 2 (sz hs + 1) - length hs + 2" by(rule ΔΦ_pass1)
finally show ?thesis by simp
qed
time_fun link
lemma T_link_0[simp]: "T_link h1 h2 = 0"
by (cases "(h1,h2)" rule: T_link.cases) auto
time_fun pass⇩1
time_fun pass⇩2
time_fun del_min
time_fun Pairing_Heap_List2.insert
lemma T_insert_0[simp]: "T_insert a h = 0"
by (cases h) auto
time_fun merge
lemma T_merge_0[simp]: "T_merge h1 h2 = 0"
by (cases "(h1,h2)" rule: merge.cases) auto
lemma A_insert: "T_insert a ho + Φ(Pairing_Heap_List2.insert a ho) - Φ ho ≤ log 2 (sz ho + 1)"
using ΔΦ_insert by auto
lemma A_merge:
"T_merge ho1 ho2 + Φ (merge ho1 ho2) - Φ ho1 - Φ ho2 ≤ 2 * log 2 (sz ho1 + sz ho2 + 1)"
proof (cases "(ho1,ho2)" rule: merge.cases)
case (3 h1 h2)
then show ?thesis using ΔΦ_link[of "the ho1" "the ho2"] apply auto
by (smt (verit, best) log_mono of_nat_0_le_iff)
qed auto
lemma A_del_min:
"T_del_min ho + Φ (del_min ho) - Φ ho ≤ 2*log 2 (sz ho + 1) + 4"
proof (cases ho)
case [simp]: (Some h)
show ?thesis
proof (cases h)
case [simp]: (Hp x hs)
have "T_pass⇩2 (pass⇩1 hs) + T_pass⇩1 hs ≤ 2 + length hs"
by (induct hs rule: T_pass⇩1.induct) (auto split: option.split)
hence "T_del_min ho ≤ …" by simp
moreover
have "Φ (del_min ho) - Φ ho ≤ 2*log 2 (sz ho) - length hs + 2"
using ΔΦ_del_min[of h] by (simp)
moreover
have "… ≤ 2*log 2 (sz ho + 1) - length hs + 2" by simp
ultimately show ?thesis
by linarith
qed
qed simp
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 cost :: "'a :: linorder op ⇒ 'a heap list ⇒ nat" where
"cost Empty _ = 0" |
"cost Del_min [h] = T_del_min h" |
"cost (Insert a) [h] = T_insert a h" |
"cost Merge [h1,h2] = T_merge h1 h2"
fun U :: "'a :: linorder op ⇒ 'a heap list ⇒ real" where
"U Empty _ = 0" |
"U (Insert a) [h] = log 2 (sz h + 1)" |
"U Del_min [h] = 2*log 2 (sz h + 1) + 4" |
"U Merge [h1,h2] = 2*log 2 (sz h1 + sz h2 + 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 A_insert 3 by auto
next
case [simp]: Del_min
then obtain ho where "ss = [ho]" using 3 by auto
thus ?thesis using A_del_min by fastforce
next
case [simp]: Merge
then obtain ho1 ho2 where "ss = [ho1, ho2]"
using 3 by(auto simp: numeral_eq_Suc)
thus ?thesis using A_merge by auto
qed
qed simp
end