(* Author: Tobias Nipkow *)

section ‹Leftist Heap›

theory Leftist_Heap
imports
  "HOL-Library.Pattern_Aliases"
  Tree2
  Priority_Queue_Specs
  Complex_Main
  "HOL-Library.Time_Commands"
begin

fun mset_tree :: "('a*'b) tree → 'a multiset" where
"mset_tree Leaf = {#}" |
"mset_tree (Node l (a, _) r) = {#a#} + mset_tree l + mset_tree r"

type_synonym 'a lheap = "('a*nat)tree"

fun mht :: "'a lheap → nat" where
"mht Leaf = 0" |
"mht (Node _ (_, n) _) = n"

text‹The invariants:›

fun (in linorder) heap :: "('a*'b) tree → bool" where
"heap Leaf = True" |
"heap (Node l (m, _) r) =
  ((∀x ∈ set_tree l ∪ set_tree r. m ≤ x) ∧ heap l ∧ heap r)"

fun ltree :: "'a lheap → bool" where
"ltree Leaf = True" |
"ltree (Node l (a, n) r) =
 (min_height l ≥ min_height r ∧ n = min_height r + 1 ∧ ltree l & ltree r)"

definition empty :: "'a lheap" where
"empty = Leaf"

definition node :: "'a lheap → 'a → 'a lheap → 'a lheap" where
"node l a r =
 (let mhl = mht l; mhr = mht r
  in if mhl ≥ mhr then Node l (a,mhr+1) r else Node r (a,mhl+1) l)"

fun get_min :: "'a lheap → 'a" where
"get_min(Node l (a, n) r) = a"

text ‹For function ‹merge›:›
unbundle pattern_aliases

fun merge :: "'a::ord lheap → 'a lheap → 'a lheap" where
"merge Leaf t = t" |
"merge t Leaf = t" |
"merge (Node l1 (a1, n1) r1 =: t1) (Node l2 (a2, n2) r2 =: t2) =
   (if a1 ≤ a2 then node l1 a1 (merge r1 t2)
    else node l2 a2 (merge t1 r2))"

text ‹Termination of @{const merge}: by sum or lexicographic product of the sizes
  the two arguments. Isabelle uses a lexicographic product.›

lemma merge_code: "merge t1 t2 = (case (t1,t2) of
  (Leaf, _) → t2 |
  (_, Leaf) → t1 |
  (Node l1 (a1, n1) r1, Node l2 (a2, n2) r2) →
    if a1 ≤ a2 then node l1 a1 (merge r1 t2) else node l2 a2 (merge t1 r2))"
by(induction t1 t2 rule: merge.induct) (simp_all split: tree.split)

hide_const (open) insert

definition insert :: "'a::ord → 'a lheap → 'a lheap" where
"insert x t = merge (Node Leaf (x,1) Leaf) t"

fun del_min :: "'a::ord lheap → 'a lheap" where
"del_min Leaf = Leaf" |
"del_min (Node l _ r) = merge l r"


subsection "Lemmas"

lemma mset_tree_empty: "mset_tree t = {#} ⟷ t = Leaf"
by(cases t) auto

lemma mht_eq_min_height: "ltree t ==> mht t = min_height t"
by(cases t) auto

lemma ltree_node: "ltree (node l a r) ⟷ ltree l ∧ ltree r"
by(auto simp add: node_def mht_eq_min_height)

lemma heap_node: "heap (node l a r) ⟷
  heap l ∧ heap r ∧ (∀x ∈ set_tree l ∪ set_tree r. a ≤ x)"
by(auto simp add: node_def)

lemma set_tree_mset: "set_tree t = set_mset(mset_tree t)"
by(induction t) auto

subsection "Functional Correctness"

lemma mset_merge: "mset_tree (merge t1 t2) = mset_tree t1 + mset_tree t2"
by (induction t1 t2 rule: merge.induct) (auto simp add: node_def ac_simps)

lemma mset_insert: "mset_tree (insert x t) = mset_tree t + {#x#}"
by (auto simp add: insert_def mset_merge)

lemma get_min: "[ heap t; t ≠ Leaf ] ==> get_min t = Min(set_tree t)"
by (cases t) (auto simp add: eq_Min_iff)

lemma mset_del_min: "mset_tree (del_min t) = mset_tree t - {# get_min t #}"
by (cases t) (auto simp: mset_merge)

lemma ltree_merge: "[ ltree l; ltree r ] ==> ltree (merge l r)"
by(induction l r rule: merge.induct)(auto simp: ltree_node)

lemma heap_merge: "[ heap l; heap r ] ==> heap (merge l r)"
proof(induction l r rule: merge.induct)
  case 3 thus ?case by(auto simp: heap_node mset_merge ball_Un set_tree_mset)
qed simp_all

lemma ltree_insert: "ltree t ==> ltree(insert x t)"
by(simp add: insert_def ltree_merge del: merge.simps split: tree.split)

lemma heap_insert: "heap t ==> heap(insert x t)"
by(simp add: insert_def heap_merge del: merge.simps split: tree.split)

lemma ltree_del_min: "ltree t ==> ltree(del_min t)"
by(cases t)(auto simp add: ltree_merge simp del: merge.simps)

lemma heap_del_min: "heap t ==> heap(del_min t)"
by(cases t)(auto simp add: heap_merge simp del: merge.simps)

text ‹Last step of functional correctness proof: combine all the above lemmas
  show that leftist heaps satisfy the specification of priority queues with merge.›

interpretation lheap: Priority_Queue_Merge
where empty = empty and is_empty = "λt. t = Leaf"
and insert = insert and del_min = del_min
and get_min = get_min and merge = merge
and invar = "λt. heap t ∧ ltree t" and mset = mset_tree
proof(standard, goal_cases)
  case 1 show ?case by (simp add: empty_def)
next
  case (2 q) show ?case by (cases q) auto
next
  case 3 show ?case by(rule mset_insert)
next
  case 4 show ?case by(rule mset_del_min)
next
  case 5 thus ?case by(simp add: get_min mset_tree_empty set_tree_mset)
next
  case 6 thus ?case by(simp add: empty_def)
next
  case 7 thus ?case by(simp add: heap_insert ltree_insert)
next
  case 8 thus ?case by(simp add: heap_del_min ltree_del_min)
next
  case 9 thus ?case by (simp add: mset_merge)
next
  case 10 thus ?case by (simp add: heap_merge ltree_merge)
qed


subsection "Complexity"

text ‹Auxiliary time functions (which are both 0):›
time_fun mht
time_fun node

lemma T_mht_0[simp]: "T_mht t = 0"
by(cases t)auto

text ‹Define timing function›
time_fun merge
time_fun insert
time_fun del_min

lemma T_merge_min_height: "ltree l ==> ltree r ==> T_merge l r ≤ min_height l + min_height r + 1"
proof(induction l r rule: merge.induct)
  case 3 thus ?case by(auto)
qed simp_all

corollary T_merge_log: assumes "ltree l" "ltree r"
  shows "T_merge l r ≤ log 2 (size1 l) + log 2 (size1 r) + 1"
using le_log2_of_power[OF min_height_size1[of l]]
  le_log2_of_power[OF min_height_size1[of r]] T_merge_min_height[of l r] assms
by linarith

corollary T_insert_log: "ltree t ==> T_insert x t ≤ log 2 (size1 t) + 2"
using T_merge_log[of "Node Leaf (x, 1) Leaf" t]
by(simp split: tree.split)

corollary T_del_min_log: assumes "ltree t"
  shows "T_del_min t ≤ 2 * log 2 (size1 t) + 1"
proof(cases t rule: tree2_cases)
  case Leaf thus ?thesis using assms by simp
next
  case [simp]: (Node l _ _ r)
  show ?thesis
    using ‹ltree t› T_merge_log[of l r]
      log_mono[of 2 "size1 l" "size1 t"] log_mono[of 2 "size1 r" "size1 t"]
    by (simp del: T_merge.simps)
qed

end