Theory Splay_Heap_Analysis

section "Splay Heap"

theory Splay_Heap_Analysis
imports
  Splay_Tree.Splay_Heap
  Amortized_Framework
  Priority_Queue_ops
  Lemmas_log
  "HOL-Data_Structures.Define_Time_Function"
begin

text ‹Timing functions must be kept in sync with the corresponding functions
on splay heaps.›

time_fun partition

time_fun insert

time_fun del_min

abbreviation "φ t == log 2 (size1 t)"

fun Φ :: "'a tree ⇒ real" where
"Φ Leaf = 0" |
"Φ (Node l a r) = Φ l + Φ r + φ (Node l a r)"

lemma amor_del_min: "T_del_min t + Φ (del_min t) - Φ t ≤ 2 * φ t + 1"
proof(induction t rule: T_del_min.induct)
  case (3 ll a lr b r)
  let ?t = "Node (Node ll a lr) b r"
  show ?case
  proof cases
    assume [simp]: "ll = Leaf"
    have 1: "log 2 (real (size1 lr) + real (size1 r))
        ≤ 3 * log 2 (1 + (real (size1 lr) + real (size1 r)))" (is "?l ≤ 3 * ?r")
    proof -
      have "?l ≤ ?r" by(simp add: size1_size)
      also have "… ≤ 3 * ?r" by(simp)
      finally show ?thesis .
    qed
    have 2: "log 2 (1 + real (size1 lr)) ≥ 0" by simp
    thus ?case apply simp using 1 2 by linarith
  next
    assume ll[simp]: "¬ ll = Leaf"
    let ?l' = "del_min ll"
    let ?s = "Node ll a lr"  let ?t = "Node ?s b r"
    let ?s' = "Node lr b r"  let ?t' = "Node ?l' a ?s'"
    have 0: "φ ?t' ≤ φ ?t" by(simp add: size1_size)
    have 1: "φ ll < φ ?s" by(simp add: size1_size)
    have 2: "log 2 (size1 ll + size1 ?s') ≤ log 2 (size1 ?t)" by(simp add: size1_size)
    have "T_del_min ?t + Φ (del_min ?t) - Φ ?t
        = 1 + T_del_min ll + Φ (del_min ?t) - Φ ?t" by simp
    also have "… ≤ 2 + 2 * φ ll + Φ ll - Φ ?l'  + Φ (del_min ?t) - Φ ?t"
      using 3 ll by linarith
    also have "… = 2 + 2 * φ ll + φ ?t' + φ ?s' - φ ?t - φ ?s" by(simp)
    also have "… ≤ 2 + φ ll + φ ?s'" using 0 1 by linarith
    also have "… < 2 * φ ?t + 1" using 2 ld_ld_1_less[of "size1 ll" "size1 ?s'"]
      by (simp add: size1_size)
    finally show ?case by simp
  qed
qed auto

lemma zig_zig:
fixes s u r r1' r2' T a b
defines "t == Node s a (Node u b r)" and "t' == Node (Node s a u) b r1'"
assumes "size r1' ≤ size r"
    "T_partition p r + Φ r1' + Φ r2' - Φ r ≤ 2 * φ r + 1"
shows "T_partition p r + 1 + Φ t' + Φ r2' - Φ t ≤ 2 * φ t + 1"
proof -
  have 1: "φ r ≤ φ (Node u b r)" by (simp add: size1_size)
  have 2: "log 2 (real (size1 s + size1 u + size1 r1')) ≤ φ t"
    using assms(3) by (simp add: t_def size1_size)
  from ld_ld_1_less[of "size1 s + size1 u" "size1 r"] 
  have "1 + φ r + log 2 (size1 s + size1 u) ≤ 2 * log 2 (size1 s + size1 u + size1 r)"
    by(simp add: size1_size)
  thus ?thesis using assms 1 2 by (simp add: algebra_simps)
qed

lemma zig_zag:
fixes s u r r1' r2' a b
defines "t ≡ Node s a (Node r b u)" and "t1' == Node s a r1'" and "t2' ≡ Node u b r2'"
assumes "size r = size r1' + size r2'"
    "T_partition p r + Φ r1' + Φ r2' - Φ r ≤ 2 * φ r + 1"
shows "T_partition p r + 1 + Φ t1' + Φ t2' - Φ t ≤ 2 * φ t + 1"
proof -
  have 1: "φ r ≤ φ (Node u b r)" by (simp add: size1_size)
  have 2: "φ r ≤ φ t" by (simp add: t_def size1_size)
  from ld_ld_less2[of "size1 s + size1 r1'" "size1 u + size1 r2'"] 
  have "1 + log 2 (size1 s + size1 r1') + log 2 (size1 u + size1 r2') ≤ 2 * φ t"
    by(simp add: assms(4) size1_size t_def ac_simps)
  thus ?thesis using assms 1 2 by (simp add: algebra_simps)
qed

lemma amor_partition: "bst_wrt (≤) t ⟹ partition p t = (l',r')
  ⟹ T_partition p t + Φ l' + Φ r' - Φ t ≤ 2 * log 2 (size1 t) + 1"
proof(induction p t arbitrary: l' r' rule: partition.induct)
  case 1 thus ?case by simp
next
  case (2 p l a r)
  show ?case
  proof cases
    assume "a ≤ p"
    show ?thesis
    proof (cases r)
      case Leaf thus ?thesis using ‹a ≤ p› "2.prems" by fastforce
    next
      case [simp]: (Node rl b rr)
      let ?t = "Node l a r"
      show ?thesis
      proof cases
        assume "b ≤ p"
        with ‹a ≤ p› "2.prems" obtain rrl
          where 0: "partition p rr = (rrl, r')" "l' = Node (Node l a rl) b rrl"
          by (auto split: tree.splits prod.splits)
        have "size rrl ≤ size rr"
          using size_partition[OF 0(1)] by (simp add: size1_size)
        with 0 ‹a ≤ p› ‹b ≤ p› "2.prems"(1) "2.IH"(1)[OF _ Node , of rrl r']
          zig_zig[where s=l and u=rl and r=rr and r1'=rrl and r2'=r' and p=p, of a b]
        show ?thesis by (simp add: algebra_simps)
      next
        assume "¬ b ≤ p"
        with ‹a ≤ p› "2.prems" obtain rll rlr 
          where 0: "partition p rl = (rll, rlr)" "l' = Node l a rll" "r' = Node rlr b rr"
          by (auto split: tree.splits prod.splits)
        from 0 ‹a ≤ p› ‹¬ b ≤ p› "2.prems"(1) "2.IH"(2)[OF _ Node, of rll rlr]
          size_partition[OF 0(1)]
          zig_zag[where s=l and u=rr and r=rl and r1'=rll and r2'=rlr and p=p, of a b]
        show ?thesis by (simp add: algebra_simps)
      qed
    qed
  next
    assume "¬ a ≤ p"
    show ?thesis
    proof (cases l)
      case Leaf thus ?thesis using ‹¬ a ≤ p› "2.prems" by fastforce
    next
      case [simp]: (Node ll b lr)
      let ?t = "Node l a r"
      show ?thesis
      proof cases
        assume "b ≤ p"
        with ‹¬ a ≤ p› "2.prems" obtain lrl lrr 
          where 0: "partition p lr = (lrl, lrr)" "l' = Node ll b lrl" "r' = Node lrr a r"
          by (auto split: tree.splits prod.splits)
        from 0 ‹¬ a ≤ p› ‹b ≤ p› "2.prems"(1) "2.IH"(3)[OF _ Node, of lrl lrr]
          size_partition[OF 0(1)]
          zig_zag[where s=r and u=ll and r=lr and r1'=lrr and r2'=lrl and p=p, of a b]
        show ?thesis by (auto simp: algebra_simps)
      next
        assume "¬ b ≤ p"
        with ‹¬ a ≤ p› "2.prems" obtain llr
          where 0: "partition p ll = (l',llr)" "r' = Node llr b (Node lr a r)"
          by (auto split: tree.splits prod.splits)
        have "size llr ≤ size ll"
          using size_partition[OF 0(1)] by (simp add: size1_size)
        with 0 ‹¬ a ≤ p› ‹¬ b ≤ p› "2.prems"(1) "2.IH"(4)[OF _ Node, of l' llr]
          zig_zig[where s=r and u=lr and r=ll and r1'=llr and r2'=l' and p=p, of a b]
        show ?thesis by (auto simp: algebra_simps)
      qed
    qed
  qed
qed

fun exec :: "'a::linorder op ⇒ 'a tree list ⇒ 'a tree" where
"exec Empty [] = Leaf" |
"exec (Insert a) [t] = insert a t" |
"exec Del_min [t] = del_min t"

fun cost :: "'a::linorder op ⇒ 'a tree list ⇒ nat" where
"cost Empty [] = 0" |
"cost (Insert a) [t] = T_insert a t" |
"cost Del_min [t] = T_del_min t"

fun U where
"U Empty [] = 0" |
"U (Insert _) [t] = 3 * log 2 (size1 t + 1) + 1" |
"U Del_min [t] = 2 * φ t + 1"

interpretation Amortized
where arity = arity and exec = exec and inv = "bst_wrt (≤)"
and cost = cost and Φ = Φ and U = U
proof (standard, goal_cases)
  case (1 _ f) thus ?case
    by(cases f)
       (auto simp: insert_def bst_del_min dest!: bst_partition split: prod.splits)
next
  case (2 h) thus ?case by(induction h) (auto simp: size1_size)
next
  case (3 s f)
  show ?case
  proof (cases f)
    case Empty with 3 show ?thesis by(auto)
  next
    case Del_min with 3 show ?thesis by(auto simp: amor_del_min)
  next
    case [simp]: (Insert x)
    then obtain t where [simp]: "s = [t]" "bst_wrt (≤) t" using 3 by auto
    { fix l r assume 1: "partition x t = (l,r)"
      have "log 2 (1 + size t) < log 2 (2 + size t)" by simp
      with 1 amor_partition[OF ‹bst_wrt (≤) t› 1] size_partition[OF 1] have ?thesis
        by(simp add: insert_def algebra_simps size1_size
             del: log_less_cancel_iff) }
    thus ?thesis by(simp add: insert_def split: prod.split)
  qed
qed

end