# Theory Binomial_Queue

Up to index of Isabelle/HOL/Binomial-Queues

theory Binomial_Queue
imports PQ
(* Authors:  RenĂ© Neumann and Florian Haftmann, TU Muenchen *)header {* Functional Binomial Queues *}theory Binomial_Queueimports PQbeginsubsection {* 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 (Cons x xs) thus ?case by (cases x) simp_allqed simptext {*  \noindent Terminology:  \begin{itemize}    \item values @{text "v, w"} or @{text "v1, v2"}    \item priorities @{text "a, b"} or @{text "a1, a2"}    \item bintrees @{text "t, r"} or @{text "t1, t2"}    \item bintree lists @{text "ts, rs"} or @{text "ts1, ts2"}    \item binqueue element @{text "x, y"} or @{text "x1, x2"}    \item binqueues = binqueue element lists @{text "xs, ys"} or @{text "xs1, xs2"}    \item abstract priority queues @{text "q, p"} or @{text "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_alllemma is_bintree_list_children_last:  assumes "is_bintree_list l ts" and "ts ≠ []"  shows "children (last ts) = []"  using assms by induct autolemma is_bintree_children_length_desc:  assumes "is_bintree_list l ts"  shows "map (length o children) ts = rev [0..<l]"  using assms by (induct ts) simp_allsubsubsection {* 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) autolemma is_heap_children_larger:  "is_heap t ==> ∀ x ∈ set (children t). priority x ≥ priority t"  by (erule is_heap_list.induct) simp_alllemma 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_alllemma is_binqueue_head:  "is_binqueue l (x#xs) ==> is_binqueue l [x]"  by (cases x) simp_alllemma 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_allnext  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)  qedqedlemma 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_alllemma 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_alllemma normalized_add:  assumes "normalized xs"  shows "normalized (add x xs)"  using assms by (induct xs rule: add.induct) simp_alllemma is_binqueue_add_None:  assumes "is_binqueue l xs"  shows "is_binqueue l (add None xs)"  using assms by simplemma 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_orderlemma meld_singleton_add [simp]:  "meld [Some t] xs = add (Some t) xs"  by (induct "Some t" xs rule: add.induct) simp_alllemma nonempty_meld [simp]:  "xs ≠ [] ==> meld xs ys ≠ []"  "ys ≠ [] ==> meld xs ys ≠ []"  by (induct xs ys rule: meld.induct) autolemma nonempty_meld_commute:  "meld xs ys ≠ [] ==> meld xs ys ≠ []"  by (induct xs ys rule: meld.induct) autolemma is_binqueue_meld:  assumes "is_binqueue l xs"  and     "is_binqueue l ys"  shows "is_binqueue l (meld xs ys)"using assmsproof (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_allnext  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_allqed (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 assmsproof (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_allnext  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_allqed (simp_all add: normalized_add)lemma normalized_meld_weak:  assumes "normalized xs"  and "length ys ≤ length xs"  shows "normalized (meld xs ys)"using assmsproof (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_allnext  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_allqed (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 simpinterpretation least!: semilattice least proofqed (auto simp add: least_def split: option.split)definition min :: "('a::linorder, 'b) binqueue => 'a option" where  "min xs = fold least (map (Option.map 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 (Option.map 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_alllemma min_None_trans:  assumes "min (x#xs) = None"  shows "min xs = None"using assms proof (cases x)  case None with assms show ?thesis by simpnext  case (Some t) with assms show ?thesis by (simp only: min_Some_not_None)qedlemma 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 autonext  show "xs = [] ∨ set xs = {None} ==> min xs = None"    by (induct xs) (auto dest: subset_singletonD)qedlemma 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 simpqed simp_alllemma min_exists:  assumes "min xs = Some a"  shows "Some a ∈ Option.map priority  set xs"proof (rule ccontr)  assume "Some a ∉ Option.map 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 simpqedprimrec 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 (Option.map priority) xs)"  shows "∃t. find a xs = Some t ∧ priority t = a"  using assms by (induct xs) autolemma find_works_not_None:  "Some a ∈ set (map (Option.map priority) xs) ==> find a xs ≠ None"  by (drule find_works) autolemma find_None:  "find a xs = None ==> Some a ∉ set (map (Option.map 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  qedqedlemma 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  qedqedlemma 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)qedlemma 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) simplemma 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`