Theory Binomial_Queue

(* Authors:  René Neumann and Florian Haftmann, TU Muenchen *)

section ‹Functional Binomial Queues›

theory Binomial_Queue
imports PQ
begin

subsection ‹Type definition and projections›

datatype ('a, 'b) bintree = Node "'a" "'b" "('a, 'b) bintree list"

primrec priority :: "('a, 'b) bintree ⇒ 'a" where
  "priority (Node a _ _) = a"

primrec val :: "('a, 'b) bintree ⇒ 'b" where
  "val (Node _ v _) = v"

primrec children :: "('a, 'b) bintree ⇒ ('a, 'b) bintree list" where
  "children (Node _ _ ts) = ts"

type_synonym ('a, 'b) binqueue = "('a, 'b) bintree option list"

lemma binqueue_induct [case_names Empty None Some, induct type: binqueue]:
  assumes "P []"
    and "⋀xs. P xs ⟹ P (None # xs)"
    and "⋀x xs. P xs ⟹ P (Some x # xs)"
  shows "P xs"
  using assms
proof (induct xs)
  case Nil
  then show ?case by simp
next
  case (Cons x xs)
  then show ?case by (cases x) simp_all
qed

text ‹
  \noindent Terminology:

  \begin{itemize}

    \item values ‹v, w› or ‹v1, v2›

    \item priorities ‹a, b› or ‹a1, a2›

    \item bintrees ‹t, r› or ‹t1, t2›

    \item bintree lists ‹ts, rs› or ‹ts1, ts2›

    \item binqueue element ‹x, y› or ‹x1, x2›

    \item binqueues = binqueue element lists ‹xs, ys› or ‹xs1, xs2›

    \item abstract priority queues ‹q, p› or ‹q1, q2›

  \end{itemize}
›


subsection ‹Binomial queue properties›

subsubsection ‹Binomial tree property›

inductive is_bintree_list :: "nat ⇒ ('a, 'b) bintree list ⇒ bool" where
  is_bintree_list_Nil [simp]: "is_bintree_list 0 []"
| is_bintree_list_Cons: "is_bintree_list l ts ⟹ is_bintree_list l (children t)
    ⟹ is_bintree_list (Suc l) (t # ts)"

abbreviation (input) "is_bintree k t ≡ is_bintree_list k (children t)"

lemma is_bintree_list_triv [simp]:
  "is_bintree_list 0 ts ⟷ ts = []"
  "is_bintree_list l [] ⟷ l = 0"
  by (auto intro: is_bintree_list.intros elim: is_bintree_list.cases)

lemma is_bintree_list_simp [simp]:
  "is_bintree_list (Suc l) (t # ts) ⟷
    is_bintree_list l (children t) ∧ is_bintree_list l ts"
  by (auto intro: is_bintree_list.intros elim: is_bintree_list.cases)

lemma is_bintree_list_length [simp]:
  "is_bintree_list l ts ⟹ length ts = l"
  by (erule is_bintree_list.induct) simp_all

lemma is_bintree_list_children_last:
  assumes "is_bintree_list l ts" and "ts ≠ []"
  shows "children (last ts) = []"
  using assms by induct auto

lemma is_bintree_children_length_desc:
  assumes "is_bintree_list l ts"
  shows "map (length ∘ children) ts = rev [0..<l]"
  using assms by (induct ts) simp_all


subsubsection ‹Heap property›

inductive is_heap_list :: "'a::linorder ⇒ ('a, 'b) bintree list ⇒ bool" where
  is_heap_list_Nil: "is_heap_list h []"
| is_heap_list_Cons: "is_heap_list h ts ⟹ is_heap_list (priority t) (children t)
    ⟹ (priority t) ≥ h ⟹ is_heap_list h (t # ts)"

abbreviation (input) "is_heap t ≡ is_heap_list (priority t) (children t)"

lemma is_heap_list_simps [simp]:
  "is_heap_list h [] ⟷ True"
  "is_heap_list h (t # ts) ⟷
    is_heap_list h ts ∧ is_heap_list (priority t) (children t) ∧ priority t ≥ h"
  by (auto intro: is_heap_list.intros elim: is_heap_list.cases)

lemma is_heap_list_append_dest [dest]:
  "is_heap_list l (ts@rs) ⟹ is_heap_list l ts"
  "is_heap_list l (ts@rs) ⟹ is_heap_list l rs"
  by (induct ts) (auto intro: is_heap_list.intros elim: is_heap_list.cases)

lemma is_heap_list_rev:
  "is_heap_list l ts ⟹ is_heap_list l (rev ts)"
  by (induct ts rule: rev_induct) auto

lemma is_heap_children_larger:
  "is_heap t ⟹ ∀ x ∈ set (children t). priority x ≥ priority t"
  by (erule is_heap_list.induct) simp_all

lemma is_heap_Min_children_larger:
  "is_heap t ⟹ children t ≠ [] ⟹ 
   priority t ≤ Min (priority ` set (children t))"
  by (simp add: is_heap_children_larger)


subsubsection ‹Combination of both: binqueue property›

inductive is_binqueue :: "nat ⇒ ('a::linorder, 'b) binqueue ⇒ bool" where
  Empty: "is_binqueue l []"
| None: "is_binqueue (Suc l) xs ⟹ is_binqueue l (None # xs)"
| Some: "is_binqueue (Suc l) xs ⟹ is_bintree l t
    ⟹ is_heap t ⟹ is_binqueue l (Some t # xs)"

lemma is_binqueue_simp [simp]:
  "is_binqueue l [] ⟷ True"
  "is_binqueue l (Some t # xs) ⟷
    is_bintree l t ∧ is_heap t ∧ is_binqueue (Suc l) xs"
  "is_binqueue l (None # xs) ⟷ is_binqueue (Suc l) xs"
  by (auto intro: is_binqueue.intros elim: is_binqueue.cases)

lemma is_binqueue_trans:
  "is_binqueue l (x#xs) ⟹ is_binqueue (Suc l) xs"
  by (cases x) simp_all

lemma is_binqueue_head:
  "is_binqueue l (x#xs) ⟹ is_binqueue l [x]"
  by (cases x) simp_all

lemma is_binqueue_append:
  "is_binqueue l xs ⟹ is_binqueue (length xs + l) ys ⟹ is_binqueue l (xs @ ys)"
  by (induct xs arbitrary: l) (auto intro: is_binqueue.intros elim: is_binqueue.cases)

lemma is_binqueue_append_dest [dest]:
  "is_binqueue l (xs @ ys) ⟹ is_binqueue l xs"
  by (induct xs arbitrary: l) (auto intro: is_binqueue.intros elim: is_binqueue.cases)

lemma is_binqueue_children:
  assumes "is_bintree_list l ts"
  and "is_heap_list t ts"
  shows "is_binqueue 0 (map Some (rev ts))"
  using assms by (induct ts) (auto simp add: is_binqueue_append)

lemma is_binqueue_select:
  "is_binqueue l xs ⟹ Some t ∈ set xs ⟹ ∃k. is_bintree k t ∧ is_heap t"
  by (induct xs arbitrary: l) (auto intro: is_binqueue.intros elim: is_binqueue.cases)


subsubsection ‹Normalized representation›

inductive normalized :: "('a, 'b) binqueue ⇒ bool" where
  normalized_Nil: "normalized []"
| normalized_single: "normalized [Some t]"
| normalized_append: "xs ≠ [] ⟹ normalized xs ⟹ normalized (ys @ xs)"

lemma normalized_last_not_None:
  ― ‹\ sometimes the inductive definition might work better›
  "normalized xs ⟷ xs = [] ∨ last xs ≠ None"
proof
  assume "normalized xs"
  then show "xs = [] ∨ last xs ≠ None"
    by (rule normalized.induct) simp_all
next
  assume *: "xs = [] ∨ last xs ≠ None"
  show "normalized xs" proof (cases xs rule: rev_cases)
    case Nil then show ?thesis by (simp add: normalized.intros)
  next
    case (snoc ys x) with * obtain t where "last xs = Some t" by auto
    with snoc have "xs = ys @ [Some t]" by simp
    then show ?thesis by (simp add: normalized.intros)
  qed
qed

lemma normalized_simps [simp]:
  "normalized [] ⟷ True"
  "normalized (Some t # xs) ⟷ normalized xs"
  "normalized (None # xs) ⟷ xs ≠ [] ∧ normalized xs"
  by (simp_all add: normalized_last_not_None)

lemma normalized_map_Some [simp]:
  "normalized (map Some xs)"
  by (induct xs) simp_all

lemma normalized_Cons:
  "normalized (x#xs) ⟹ normalized xs"
  by (auto simp add: normalized_last_not_None)

lemma normalized_append:
  "normalized xs ⟹ normalized ys ⟹ normalized (xs@ys)"
  by (cases ys) (simp_all add: normalized_last_not_None)

lemma normalized_not_None:
  "normalized xs ⟹ set xs ≠ {None}"
  by (induct xs) (auto simp add: normalized_Cons [of _ ts] dest: subset_singletonD) 

primrec normalize' :: "('a, 'b) binqueue ⇒ ('a, 'b) binqueue" where
  "normalize' [] = []"
| "normalize' (x # xs) =
    (case x of None ⇒ normalize' xs | Some t ⇒ (x # xs))"

definition normalize :: "('a, 'b) binqueue ⇒ ('a, 'b) binqueue" where
  "normalize xs = rev (normalize' (rev xs))"

lemma normalized_normalize:
  "normalized (normalize xs)"
proof (induct xs rule: rev_induct)
  case (snoc y ys) then show ?case 
    by (cases y) (simp_all add: normalized_last_not_None normalize_def)
qed (simp add: normalize_def)

lemma is_binqueue_normalize:
  "is_binqueue l xs ⟹ is_binqueue l (normalize xs)"
  unfolding normalize_def
    by (induct xs arbitrary: l rule: rev_induct) (auto split: option.split)


subsection ‹Operations›

subsubsection ‹Adding data›

definition merge :: "('a::linorder, 'b) bintree ⇒ ('a, 'b) bintree ⇒ ('a, 'b) bintree" where
  "merge t1 t2 = (if priority t1 < priority t2
    then Node (priority t1) (val t1) (t2 # children t1) 
    else Node (priority t2) (val t2) (t1 # children t2))"

lemma is_bintree_list_merge:
  assumes "is_bintree l t1" "is_bintree l t2"
  shows "is_bintree (Suc l) (merge t1 t2)"
  using assms by (simp add: merge_def)

lemma is_heap_merge:
  assumes "is_heap t1" "is_heap t2"
  shows "is_heap (merge t1 t2)"
  using assms by (auto simp add: merge_def)

fun
  add :: "('a::linorder, 'b) bintree option ⇒ ('a, 'b) binqueue ⇒ ('a, 'b) binqueue"
where
  "add None xs = xs"
| "add (Some t) [] = [Some t]"
| "add (Some t) (None # xs) = Some t # xs"
| "add (Some t) (Some r # xs) = None # add (Some (merge t r)) xs"

lemma add_Some_not_Nil [simp]:
  "add (Some t) xs ≠ []"
  by (induct "Some t" xs rule: add.induct) simp_all

lemma normalized_add:
  assumes "normalized xs"
  shows "normalized (add x xs)"
  using assms by (induct xs rule: add.induct) simp_all

lemma is_binqueue_add_None:
  assumes "is_binqueue l xs"
  shows "is_binqueue l (add None xs)"
  using assms by simp

lemma is_binqueue_add_Some:
  assumes "is_binqueue l xs"
  and     "is_bintree l t"
  and     "is_heap t"
  shows "is_binqueue l (add (Some t) xs)"
  using assms by (induct xs arbitrary: t) (simp_all add: is_bintree_list_merge is_heap_merge)

function
  meld :: "('a::linorder, 'b) binqueue ⇒ ('a, 'b) binqueue ⇒ ('a, 'b) binqueue"
where
  "meld [] ys = ys"
| "meld xs [] = xs"
| "meld (None # xs) (y # ys) = y # meld xs ys"
| "meld (x # xs) (None # ys) = x # meld xs ys"
| "meld (Some t # xs) (Some r # ys) =
    None # add (Some (merge t r)) (meld xs ys)"
  by pat_completeness auto termination by lexicographic_order

lemma meld_singleton_add [simp]:
  "meld [Some t] xs = add (Some t) xs"
  by (induct "Some t" xs rule: add.induct) simp_all

lemma nonempty_meld [simp]:
  "xs ≠ [] ⟹ meld xs ys ≠ []"
  "ys ≠ [] ⟹ meld xs ys ≠ []"
  by (induct xs ys rule: meld.induct) auto

lemma nonempty_meld_commute:
  "meld xs ys ≠ [] ⟹ meld xs ys ≠ []"
  by (induct xs ys rule: meld.induct) auto

lemma is_binqueue_meld:
  assumes "is_binqueue l xs"
  and     "is_binqueue l ys"
  shows "is_binqueue l (meld xs ys)"
using assms
proof (induct xs ys arbitrary: l rule: meld.induct)
  fix xs ys :: "('a, 'b) binqueue"
  fix y :: "('a, 'b) bintree option"
  fix l :: nat
  assume "⋀ l. is_binqueue l xs ⟹ is_binqueue l ys
      ⟹ is_binqueue l (meld xs ys)"
    and "is_binqueue l (None # xs)"
    and "is_binqueue l (y # ys)"
  then show "is_binqueue l (meld (None # xs) (y # ys))" by (cases y) simp_all
next
  fix xs ys :: "('a, 'b) binqueue"
  fix x :: "('a, 'b) bintree option"
  fix l :: nat
  assume "⋀ l. is_binqueue l xs ⟹ is_binqueue l ys
      ⟹ is_binqueue l (meld xs ys)"
    and "is_binqueue l (x # xs)"
    and "is_binqueue l (None # ys)"
  then show "is_binqueue l (meld (x # xs) (None # ys))" by (cases x) simp_all
qed (simp_all add: is_bintree_list_merge is_heap_merge is_binqueue_add_Some)

lemma normalized_meld:
  assumes "normalized xs"
  and     "normalized ys"
  shows   "normalized (meld xs ys)"
using assms
proof (induct xs ys rule: meld.induct)
  fix xs ys :: "('a, 'b) binqueue"
  fix y :: "('a, 'b) bintree option"
  assume "normalized xs ⟹ normalized ys ⟹ normalized (meld xs ys)"
    and  "normalized (None # xs)"
    and  "normalized (y # ys)"
  then show "normalized (meld (None # xs) (y # ys))" by (cases y) simp_all
next
  fix xs ys :: "('a, 'b) binqueue"
  fix x :: "('a, 'b) bintree option"
  assume "normalized xs ⟹ normalized ys ⟹ normalized (meld xs ys)"
    and  "normalized (x # xs)"
    and  "normalized (None # ys)"
  then show "normalized (meld (x # xs) (None # ys))" by (cases x) simp_all
qed (simp_all add: normalized_add)

lemma normalized_meld_weak:
  assumes "normalized xs"
  and "length ys ≤ length xs"
  shows "normalized (meld xs ys)"
using assms
proof (induct xs ys rule: meld.induct)
  fix xs ys :: "('a, 'b) binqueue"
  fix y :: "('a, 'b) bintree option"
  assume "normalized xs ⟹ length ys ≤ length xs ⟹ normalized (meld xs ys)"
    and  "normalized (None # xs)"
    and  "length (y # ys) ≤ length (None # xs)"
  then show "normalized (meld (None # xs) (y # ys))" by (cases y) simp_all
next
  fix xs ys :: "('a, 'b) binqueue"
  fix x :: "('a, 'b) bintree option"
  assume "normalized xs ⟹ length ys ≤ length xs ⟹ normalized (meld xs ys)"
    and  "normalized (x # xs)"
    and  "length (None # ys) ≤ length (x # xs)"
  then show "normalized (meld (x # xs) (None # ys))" by (cases x) simp_all
qed (simp_all add: normalized_add)

definition least :: "'a::linorder option ⇒ 'a option ⇒ 'a option" where
  "least x y = (case x of
      None ⇒ y
    | Some x' ⇒ (case y of
           None ⇒ x
         | Some y' ⇒ if x' ≤ y' then x else y))"

lemma least_simps [simp, code]:
  "least None x = x"
  "least x None = x"
  "least (Some x') (Some y') = (if x' ≤ y' then Some x' else Some y')"
  unfolding least_def by (simp_all) (cases x, simp_all)

lemma least_split:
  assumes "least x y = Some z"
  shows "x = Some z ∨ y = Some z"
using assms proof (cases x)
  case (Some x') with assms show ?thesis by (cases y) (simp_all add: eq_commute)
qed simp

interpretation least: semilattice least proof
qed (auto simp add: least_def split: option.split)

definition min :: "('a::linorder, 'b) binqueue ⇒ 'a option" where
  "min xs = fold least (map (map_option priority) xs) None"

lemma min_simps [simp]:
  "min [] = None"
  "min (None # xs) = min xs"
  "min (Some t # xs) = least (Some (priority t)) (min xs)"
  by (simp_all add: min_def fold_commute_apply [symmetric]
    fun_eq_iff least.left_commute del: least_simps)

lemma [code]:
  "min xs = fold (λ x. least (map_option priority x)) xs None"
  by (simp add: min_def fold_map o_def)

lemma min_single:
  "min [x] = Some a ⟹ priority (the x) = a"
  "min [x] = None ⟹ x = None"
  by (auto simp add: min_def)

lemma min_Some_not_None:
  "min (Some t # xs) ≠ None"
  by (cases "min xs") simp_all

lemma min_None_trans:
  assumes "min (x#xs) = None"
  shows "min xs = None"
using assms proof (cases x)
  case None with assms show ?thesis by simp
next
  case (Some t) with assms show ?thesis by (simp only: min_Some_not_None)
qed

lemma min_None_None:
  "min xs = None ⟷ xs = [] ∨ set xs = {None}"
proof (rule iffI)
  have splitQ: "⋀ xs. xs ⊆ {None} ⟹ xs = {} ∨ xs = {None}" by auto

  assume "min xs = None"
  then have "set xs ⊆ {None}"
  proof (induct xs)
    case (None ys) thus ?case using min_None_trans[of _ ys] by simp_all
  next
    case (Some t ys) thus ?case using min_Some_not_None[of t ys] by simp 
  qed simp
 
  with splitQ show "xs = [] ∨ set xs = {None}" by auto
next
  show "xs = [] ∨ set xs = {None} ⟹ min xs = None"
    by (induct xs) (auto dest: subset_singletonD)
qed

lemma normalized_min_not_None:
  "normalized xs ⟹ xs ≠ [] ⟹ min xs ≠ None"
  by (simp add: min_None_None normalized_not_None)

lemma min_is_min:
  assumes "normalized xs"
  and "xs ≠ []"
  and "min xs = Some a"
  shows "∀x ∈ set xs. x = None ∨ a ≤ priority (the x)"
using assms proof (induct xs arbitrary: a rule: binqueue_induct)
  case (Some t ys) thus ?case
  proof (cases "ys = []")
    case False
    with Some have N: "normalized ys" using normalized_Cons[of _ ys] by simp
    with ‹ys ≠ []› have "min ys ≠ None"
      by (simp add: normalized_min_not_None)
    then obtain a' where oa': "min ys = Some a'" by auto
    with Some N False
      have "∀y ∈ set ys. y = None ∨ a' ≤ priority (the y)" by simp

    with Some oa' show ?thesis
      by (cases "a' ≤ priority t") (auto simp add: least.commute)
  qed simp
qed simp_all

lemma min_exists:
  assumes "min xs = Some a"
  shows "Some a ∈ map_option priority ` set xs"
proof (rule ccontr)
  assume "Some a ∉ map_option priority ` set xs"
  then have "∀x ∈ set xs. x = None ∨ priority (the x) ≠ a" by (induct xs) auto
  then have "min xs ≠ Some a"  
  proof (induct xs arbitrary: a)
    case (Some t ys) 
    hence "priority t ≠ a" and "min ys ≠ Some a" by simp_all
    show ?case
    proof (rule ccontr, simp)
      assume "least (Some (priority t)) (min ys) = Some a"
      hence "Some (priority t) = Some a ∨ min ys = Some a" by (rule least_split)
      with ‹min ys ≠ Some a› have "priority t = a" by simp
      with ‹priority t ≠ a› show False by simp
    qed
  qed simp_all
  with assms show False by simp
qed

primrec find :: "'a::linorder ⇒ ('a, 'b) binqueue ⇒ ('a, 'b) bintree option" where
  "find a [] = None"
| "find a (x#xs) = (case x of None ⇒ find a xs
    | Some t ⇒ if priority t = a then Some t else find a xs)"

declare find.simps [simp del]

lemma find_simps [simp, code]:
  "find a [] = None"
  "find a (None # xs) = find a xs"
  "find a (Some t # xs) = (if priority t = a then Some t else find a xs)"
  by (simp_all add: find_def)

lemma find_works:
  assumes "Some a ∈ set (map (map_option priority) xs)"
  shows "∃t. find a xs = Some t ∧ priority t = a"
  using assms by (induct xs) auto

lemma find_works_not_None:
  "Some a ∈ set (map (map_option priority) xs) ⟹ find a xs ≠ None"
  by (drule find_works) auto

lemma find_None:
  "find a xs = None ⟹ Some a ∉ set (map (map_option priority) xs)"
  by (auto simp add: find_works_not_None)

lemma find_exist:
  "find a xs = Some t ⟹ Some t ∈ set xs"
  by (induct xs) (simp_all add: eq_commute)

definition find_min :: "('a::linorder, 'b) binqueue ⇒ ('a, 'b) bintree option" where
  "find_min xs = (case min xs of None ⇒ None | Some a ⇒ find a xs)"

lemma find_min_simps [simp]:
  "find_min [] = None"
  "find_min (None # xs) = find_min xs"
  by (auto simp add: find_min_def split: option.split)

lemma find_min_single:
  "find_min [x] = x"
  by (cases x) (auto simp add: find_min_def)

lemma min_eq_find_min_None:
  "min xs = None ⟷ find_min xs = None"
proof (rule iffI)
  show "min xs = None ⟹ find_min xs = None"
    by (simp add: find_min_def)
next
  assume *: "find_min xs = None"
  show "min xs = None"
  proof (rule ccontr)
    assume "min xs ≠ None"
    
    then obtain a where "min xs = Some a" by auto
    hence "find_min xs ≠ None"
      by (simp add: find_min_def min_exists find_works_not_None)
    with * show False by simp
  qed
qed

lemma min_eq_find_min_Some:
  "min xs = Some a ⟷ (∃ t. find_min xs = Some t ∧ priority t = a)"
proof (rule iffI)
  show D1: "⋀a. min xs = Some a
    ⟹ (∃ t. find_min xs = Some t ∧ priority t = a)"
    by (simp add: find_min_def find_works min_exists)
  (* no 'next' here to keep D1 in scope as it is needed in the other part *)
  assume *: "∃ t. find_min xs = Some t ∧ priority t = a"
  show "min xs = Some a"
  proof (rule ccontr)
    assume "min xs ≠ Some a" thus False
    proof (cases "min xs")
      case None 
      hence "find_min xs = None" by (simp only: min_eq_find_min_None)
      with * show False by simp
    next
      case (Some b) 
      with ‹min xs ≠ Some a› have "a ≠ b" by simp
      with * Some show False using D1 by auto
    qed
  qed
qed

lemma find_min_exist:
  assumes "find_min xs = Some t"
  shows "Some t ∈ set xs"
proof -
  from assms have "min xs ≠ None" by (simp add: min_eq_find_min_None)
  with assms show ?thesis by (auto simp add: find_min_def find_exist)
qed

lemma find_min_is_min:
  assumes "normalized xs"
  and "xs ≠ []"
  and "find_min xs = Some t"
  shows "∀x ∈ set xs. x = None ∨ (priority t) ≤ priority (the x)"
  using assms by (simp add: min_eq_find_min_Some min_is_min)

lemma normalized_find_min_exists:
  "normalized xs ⟹ xs ≠ [] ⟹ ∃t. find_min xs = Some t"
by (drule normalized_min_not_None) (simp_all add: min_eq_find_min_None)

primrec
  match :: "'a::linorder ⇒ ('a, 'b) bintree option ⇒ ('a, 'b) bintree option"
where
  "match a None = None"
| "match a (Some t) = (if priority t = a then None else Some t)"

definition delete_min :: "('a::linorder, 'b) binqueue ⇒ ('a, 'b) binqueue" where
  "delete_min xs = (case find_min xs
    of Some (Node a v ts) ⇒
         normalize (meld (map Some (rev ts)) (map (match a) xs)) 
     | None ⇒ [])"

lemma delete_min_empty [simp]:
  "delete_min [] = []"
  by (simp add: delete_min_def)

lemma delete_min_nonempty [simp]:
  "normalized xs ⟹ xs ≠ [] ⟹ find_min xs = Some t
    ⟹ delete_min xs = normalize
      (meld (map Some (rev (children t))) (map (match (priority t)) xs))"
  unfolding delete_min_def by (cases t) simp

lemma is_binqueue_delete_min:
  assumes "is_binqueue 0 xs"
  shows "is_binqueue 0 (delete_min xs)"
proof (cases "find_min xs")
  case (Some t)
  from assms have "is_binqueue 0 (map (match (priority t)) xs)"
    by (induct xs) simp_all

  moreover
  from Some have "Some t ∈ set xs" by (rule find_min_exist)
  with assms have "∃l. is_bintree l t" and "is_heap t"
    using is_binqueue_select[of 0 xs t] by auto
  with assms have "is_binqueue 0 (map Some (rev (children t)))"
    by (auto simp add: is_binqueue_children)
  
  ultimately show ?thesis using Some
    by (auto simp add: is_binqueue_meld delete_min_def is_binqueue_normalize
      split: bintree.split)
qed (simp add: delete_min_def)

lemma normalized_delete_min:
  "normalized (delete_min xs)"
  by (cases "find_min xs")
    (auto simp add: delete_min_def normalized_normalize split: bintree.split)


subsubsection ‹Dedicated grand unified operation for generated program›

definition
  meld' :: "('a, 'b) bintree option ⇒ ('a::linorder, 'b) binqueue
    ⇒ ('a, 'b) binqueue ⇒ ('a, 'b) binqueue"
where
  "meld' z xs ys = add z (meld xs ys)"

lemma [code]:
  "add z xs = meld' z [] xs"
  "meld xs ys = meld' None xs ys"
  by (simp_all add: meld'_def)

lemma [code]:
  "meld' z (Some t # xs) (Some r # ys) =
    z # (meld' (Some (merge t r)) xs ys)"
  "meld' (Some t) (Some r # xs) (None # ys) =
    None # (meld' (Some (merge t r)) xs ys)"
  "meld' (Some t) (None # xs) (Some r # ys) =
    None # (meld' (Some (merge t r)) xs ys)"
  "meld' None (x # xs) (None # ys) = x # (meld' None xs ys)"
  "meld' None (None # xs) (y # ys) = y # (meld' None xs ys)"
  "meld' z (None # xs) (None # ys) = z # (meld' None xs ys)"
  "meld' z xs [] = meld' z [] xs"
  "meld' z [] (y # ys) = meld' None [z] (y # ys)"
  "meld' (Some t) [] ys = meld' None [Some t] ys"
  "meld' None [] ys = ys"
  by (simp add: meld'_def | cases z)+


subsubsection ‹Interface operations›

abbreviation (input) empty :: "('a,'b) binqueue" where
  "empty ≡ []"

definition
  insert :: "'a::linorder ⇒ 'b ⇒ ('a, 'b) binqueue ⇒ ('a, 'b) binqueue"
where
  "insert a v xs = add (Some (Node a v [])) xs"

lemma insert_simps [simp]:
  "insert a v [] = [Some (Node a v [])]"
  "insert a v (None # xs) = Some (Node a v []) # xs"
  "insert a v (Some t # xs) = None # add (Some (merge (Node a v []) t)) xs"
  by (simp_all add: insert_def)

lemma is_binqueue_insert:
  "is_binqueue 0 xs ⟹ is_binqueue 0 (insert a v xs)"
  by (simp add: is_binqueue_add_Some insert_def)

lemma normalized_insert:
  "normalized xs ⟹ normalized (insert a v xs)"
  by (simp add: normalized_add insert_def)

definition
  pop :: "('a::linorder, 'b) binqueue ⇒ (('b × 'a) option × ('a, 'b) binqueue)"
where
  "pop xs = (case find_min xs of 
      None ⇒ (None, xs) 
    | Some t  ⇒ (Some (val t, priority t), delete_min xs))"

lemma pop_empty [simp]:
  "pop empty = (None, empty)"
  by (simp add: pop_def empty_def)

lemma pop_nonempty [simp]:
  "normalized xs ⟹ xs ≠ [] ⟹ find_min xs = Some t
    ⟹ pop xs = (Some (val t, priority t), normalize
      (meld (map Some (rev (children t))) (map (match (priority t)) xs)))"
  by (simp add: pop_def)

lemma pop_code [code]:
  "pop xs = (case find_min xs of 
      None ⇒ (None, xs) 
    | Some t  ⇒ (Some (val t, priority t), normalize
       (meld (map Some (rev (children t))) (map (match (priority t)) xs))))"
  by (cases "find_min xs") (simp_all add: pop_def delete_min_def split: bintree.split)

end