Theory Pairing_Heap_List2_Analysis

(* Author: Tobias Nipkow (based on Hauke Brinkop's tree proofs) *)

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 pass1_size[simp]: "size_hps (pass1 hs) = size_hps hs" 
by (induct hs rule: pass1.induct) (simp_all add: size_hps_link)

lemma pass2_None[simp]: "pass2 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 (pass1 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(pass1 ?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 (pass1 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: "pass2 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  []  Φ (pass2 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 "pass2 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 = "Φ(pass2(pass1 (hps h))) - Φ_hps (hps h)"
  let ?ΔΦ = "Φ (del_min (Some h)) - Φ (Some h)"
  have "Φ(pass2(pass1(hps h))) - Φ_hps (pass1(hps h))  log 2 (size_hps(hps h))" 
    using ΔΦ_pass2[of "pass1(hps h)"] using size_hps.elims assms by force
  moreover have "Φ_hps (pass1 (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 Tpass1 :: "'a hp list  nat" where
  "Tpass1 [] = 1"
| "Tpass1 [_] = 1"
| "Tpass1 (_ # _ # hs) = 1 + Tpass1 hs"

fun Tpass2 :: "'a hp list  nat" where
"Tpass2 [] = 1" |
"Tpass2 (_ # hs) = 1 + Tpass2 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 + Tpass2 (pass1 hs) + Tpass1 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 "Tpass2 (pass1 hs) + Tpass1 hs  2 + length hs"
          by (induct hs rule: pass1.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