# Theory SkewBinomialHeap

section "Skew Binomial Heaps"

theory SkewBinomialHeap
imports Main "HOL-Library.Multiset"
begin

text ‹Skew Binomial Queues as specified by Brodal and Okasaki \<^cite>‹"BrOk96"›
are a data structure for priority queues with worst case O(1) {\em findMin},
{\em insert}, and {\em meld} operations, and worst-case logarithmic
{\em deleteMin} operation.
They are derived from priority queues in three steps:
\begin{enumerate}
\item Skew binomial trees are used to eliminate the possibility of
of an insert operation to $O(1)$.
\item The current minimal element is cached. This approach, known as
{\em global root}, reduces the cost of a {\em findMin}-operation to
O(1).
\item By allowing skew binomial queues to contain skew binomial queues,
the cost for meld-operations is reduced to $O(1)$. This approach
is known as {\em data-structural bootstrapping}.
\end{enumerate}

In this theory, we combine Steps~2 and 3, i.e. we first implement skew binomial
queues, and then bootstrap them. The bootstrapping implicitly introduces a
global root, such that we also get a constant time findMin operation.
›

locale SkewBinomialHeapStruc_loc
begin

subsection "Datatype"

datatype ('e, 'a) SkewBinomialTree =
Node (val: 'e) (prio: "'a::linorder") (rank: nat) (children: "('e , 'a) SkewBinomialTree list")

type_synonym ('e, 'a) SkewBinomialQueue = "('e, 'a::linorder) SkewBinomialTree list"

subsubsection "Abstraction to Multisets"
text ‹Returns a multiset with all (element, priority) pairs from a queue›
fun tree_to_multiset
:: "('e, 'a::linorder) SkewBinomialTree ⇒ ('e × 'a) multiset"
and queue_to_multiset
:: "('e, 'a::linorder) SkewBinomialQueue ⇒ ('e × 'a) multiset" where
"tree_to_multiset (Node e a r ts) = {#(e,a)#} + queue_to_multiset ts" |
"queue_to_multiset [] = {#}" |
"queue_to_multiset (t#q) = tree_to_multiset t + queue_to_multiset q"

lemma ttm_children: "tree_to_multiset t =
{#(val t,prio t)#} + queue_to_multiset (children t)"
by (cases t) auto

(*lemma qtm_cons[simp]: "queue_to_multiset (t#q)
= queue_to_multiset q + tree_to_multiset t"
apply(induct q arbitrary: t)
apply simp
done*)

lemma qtm_conc[simp]: "queue_to_multiset (q@q')
= queue_to_multiset q + queue_to_multiset q'"
by (induct q) (auto simp add: union_ac)

subsubsection "Invariant"

text ‹Link two trees of rank $r$ to a new tree of rank $r+1$›
fun  link :: "('e, 'a::linorder) SkewBinomialTree ⇒ ('e, 'a) SkewBinomialTree ⇒
('e, 'a) SkewBinomialTree" where
"link (Node e1 a1 r1 ts1) (Node e2 a2 r2 ts2) =
(if  a1≤a2
then (Node e1 a1 (Suc r1) ((Node e2 a2 r2 ts2)#ts1))
else (Node e2 a2 (Suc r2) ((Node e1 a1 r1 ts1)#ts2)))"

text ‹Link two trees of rank $r$ and a new element to a new tree of
rank $r+1$›
fun skewlink :: "'e ⇒ 'a::linorder ⇒ ('e, 'a) SkewBinomialTree ⇒
('e, 'a) SkewBinomialTree ⇒ ('e, 'a) SkewBinomialTree" where
"skewlink e a t t' = (if a ≤ (prio t) ∧ a ≤ (prio t')
then (Node e a (Suc (rank t)) [t,t'])
else (if (prio t) ≤ (prio t')
then
Node (val t)  (prio t)  (Suc (rank t))  (Node e a 0 [] # t' # children t)
else
Node (val t') (prio t') (Suc (rank t')) (Node e a 0 [] # t # children t')))"

text ‹
The invariant for trees claims that a tree labeled rank $0$ has no children,
and a tree labeled rank $r + 1$ is the result of an ordinary link or
a skew link of two trees with rank $r$.›
function tree_invar :: "('e, 'a::linorder) SkewBinomialTree ⇒ bool" where
"tree_invar (Node e a 0 ts) = (ts = [])" |
"tree_invar (Node e a (Suc r) ts) = (∃ e1 a1 ts1 e2 a2 ts2 e' a'.
tree_invar (Node e1 a1 r ts1) ∧ tree_invar (Node e2 a2 r ts2) ∧
((Node e a (Suc r) ts) = link (Node e1 a1 r ts1) (Node e2 a2 r ts2) ∨
(Node e a (Suc r) ts) = skewlink e' a' (Node e1 a1 r ts1) (Node e2 a2 r ts2)))"
by pat_completeness auto
termination
apply(relation "measure rank")
apply auto
done

text ‹A heap satisfies the invariant, if all contained trees satisfy the
invariant, the ranks of the trees in the heap are distinct, except that the
first two trees may have same rank, and the ranks are ordered in ascending
order.›

text ‹First part: All trees inside the queue satisfy the invariant.›
definition queue_invar :: "('e, 'a::linorder) SkewBinomialQueue ⇒ bool" where
"queue_invar q ≡ (∀t ∈ set q. tree_invar t)"

lemma queue_invar_simps[simp]:
"queue_invar []"
"queue_invar (t#q) ⟷ tree_invar t ∧ queue_invar q"
"queue_invar (q@q') ⟷ queue_invar q ∧ queue_invar q'"
"queue_invar q ⟹ t∈set q ⟹ tree_invar t"
unfolding queue_invar_def by auto

text ‹Second part: The ranks of the trees in the heap are distinct,
except that the first two trees may have same rank, and the ranks are
ordered in ascending order.›

text ‹For tail of queue›
fun rank_invar :: "('e, 'a::linorder) SkewBinomialQueue ⇒ bool" where
"rank_invar [] = True" |
"rank_invar [t] = True" |
"rank_invar (t # t' # bq) = (rank t < rank t' ∧ rank_invar (t' # bq))"

text ‹For whole queue: First two elements may have same rank›
fun rank_skew_invar :: "('e, 'a::linorder) SkewBinomialQueue ⇒ bool" where
"rank_skew_invar [] = True" |
"rank_skew_invar [t] = True" |
"rank_skew_invar (t # t' # bq) = ((rank t ≤ rank t') ∧ rank_invar (t' # bq))"

definition tail_invar :: "('e, 'a::linorder) SkewBinomialQueue ⇒ bool" where
"tail_invar bq = (queue_invar bq ∧ rank_invar bq)"

definition invar :: "('e, 'a::linorder) SkewBinomialQueue ⇒ bool" where
"invar bq = (queue_invar bq ∧ rank_skew_invar bq)"

lemma invar_empty[simp]:
"invar []"
"tail_invar []"
unfolding invar_def tail_invar_def by auto

lemma invar_tail_invar:
"invar (t # bq) ⟹ tail_invar bq"
unfolding invar_def tail_invar_def
by (cases bq) simp_all

= tree_to_multiset t1 +tree_to_multiset t2"
by (cases t1, cases t2, auto simp add:union_ac)

lemma link_tree_invar: "⟦tree_invar t1; tree_invar t2; rank t1 = rank t2⟧ ⟹
by (cases t1, cases t2, simp, blast)

= {# (e,a) #} +  tree_to_multiset t1 + tree_to_multiset t2"
by (cases t1, cases t2, auto simp add:union_ac)

lemma skewlink_tree_invar: "⟦tree_invar t1; tree_invar t2; rank t1 = rank t2⟧ ⟹
tree_invar (skewlink e a t1 t2)"
by (cases t1, cases t2, simp, blast)

lemma rank_link: "rank t = rank t' ⟹ rank (link t t') = rank t + 1"
apply (cases t)
apply (cases t')
apply(auto)
done

lemma rank_skew_rank_invar: "rank_skew_invar (t # bq) ⟹ rank_invar bq"
by (cases bq) simp_all

lemma rank_invar_rank_skew:
assumes "rank_invar q"
shows "rank_skew_invar q"
proof (cases q)
case Nil
then show ?thesis by simp
next
case (Cons _ list)
with assms show ?thesis
by (cases list) simp_all
qed

lemma rank_invar_cons_up:
"⟦rank_invar (t # bq); rank t' < rank t⟧ ⟹ rank_invar (t' # t # bq)"
by simp

lemma rank_skew_cons_up:
"⟦rank_invar (t # bq); rank t' ≤ rank t⟧ ⟹ rank_skew_invar (t' # t # bq)"
by simp

lemma rank_invar_cons_down: "rank_invar (t # bq) ⟹ rank_invar bq"
by (cases bq) simp_all

lemma rank_invar_hd_cons:
"⟦rank_invar bq; rank t < rank (hd bq)⟧ ⟹ rank_invar (t # bq)"
apply(cases bq)
apply(auto)
done

lemma tail_invar_cons_up:
"⟦tail_invar (t # bq); rank t' < rank t; tree_invar t'⟧
⟹ tail_invar (t' # t # bq)"
unfolding tail_invar_def
apply (cases bq)
apply simp_all
done

lemma tail_invar_cons_up_invar:
"⟦tail_invar (t # bq); rank t' ≤ rank t; tree_invar t'⟧ ⟹ invar (t' # t # bq)"
by (cases bq) (simp_all add: invar_def tail_invar_def)

lemma tail_invar_cons_down:
"tail_invar (t # bq) ⟹ tail_invar bq"
unfolding tail_invar_def
by (cases bq) simp_all

lemma tail_invar_app_single:
"⟦tail_invar bq; ∀t ∈ set bq. rank t < rank t'; tree_invar t'⟧
⟹ tail_invar (bq @ [t'])"
proof (induct bq)
case Nil
then show ?case by (simp add: tail_invar_def)
next
case (Cons a bq)
from ‹tail_invar (a # bq)› have "tail_invar bq"
by (rule tail_invar_cons_down)
with Cons have "tail_invar (bq @ [t'])" by simp
with Cons show ?case
by (cases bq) (simp_all add: tail_invar_cons_up tail_invar_def)
qed

lemma invar_app_single:
"⟦invar bq; ∀t ∈ set bq. rank t < rank t'; tree_invar t'⟧
⟹ invar (bq @ [t'])"
proof (induct bq)
case Nil
then show ?case by (simp add: invar_def)
next
case (Cons a bq)
show ?case
proof (cases bq)
case Nil
with Cons show ?thesis by (simp add: invar_def)
next
case Cons': (Cons ta qa)
from Cons(2) have a1: "tail_invar bq" by (rule invar_tail_invar)
from Cons(3) have a2: "∀t∈set bq. rank t < rank t'" by simp
from a1 a2 Cons(4) tail_invar_app_single[of "bq" "t'"]
have "tail_invar (bq @ [t'])" by simp
with Cons Cons' show ?thesis
by (simp_all add: tail_invar_cons_up_invar invar_def tail_invar_def)
qed
qed

lemma invar_children:
assumes "tree_invar ((Node e a r ts)::(('e, 'a::linorder) SkewBinomialTree))"
shows "queue_invar ts" using assms
proof (induct r arbitrary: e a ts)
case 0
then show ?case by simp
next
case (Suc r)
from Suc(2) obtain e1 a1 ts1 e2 a2 ts2 e' a' where
inv_t1: "tree_invar (Node e1 a1 r ts1)" and
inv_t2: "tree_invar (Node e2 a2 r ts2)" and
"((Node e a (Suc r) ts) = link (Node e1 a1 r ts1) (Node e2 a2 r ts2)
∨ (Node e a (Suc r) ts)
= skewlink e' a' (Node e1 a1 r ts1) (Node e2 a2 r ts2))"
by (simp only: tree_invar.simps) blast
from Suc(1)[OF inv_t1] inv_t2
have case1: "queue_invar ((Node e2 a2 r ts2) # ts1)" by simp
from Suc(1)[OF inv_t2] inv_t1
have case2: "queue_invar ((Node e1 a1 r ts1) # ts2)" by simp
show ?case
proof (cases "(Node e a (Suc r) ts) = link (Node e1 a1 r ts1) (Node e2 a2 r ts2)")
case True
hence "ts =
(if a1 ≤ a2
then (Node e2 a2 r ts2) # ts1
else (Node e1 a1 r ts1) # ts2)" by auto
with case1 case2 show ?thesis by simp
next
case False
have "Node e a (Suc r) ts =
skewlink e' a' (Node e1 a1 r ts1) (Node e2 a2 r ts2)" by simp
hence "ts =
(if a' ≤ a1 ∧ a' ≤ a2
then [(Node e1 a1 r ts1),(Node e2 a2 r ts2)]
else (if a1 ≤ a2
then (Node e' a' 0 []) # (Node e2 a2 r ts2) # ts1
else (Node e' a' 0 []) # (Node e1 a1 r ts1) # ts2))" by auto
with case1 case2 show ?thesis by simp
qed
qed

subsubsection "Heap Order"

fun heap_ordered :: "('e, 'a::linorder) SkewBinomialTree ⇒ bool" where
"heap_ordered (Node e a r ts)
= (∀x ∈ set_mset (queue_to_multiset ts). a ≤ snd x)"

text ‹The invariant for trees implies heap order.›
lemma tree_invar_heap_ordered:
fixes t :: "('e, 'a::linorder) SkewBinomialTree"
assumes "tree_invar t"
shows "heap_ordered t"
proof (cases t)
case (Node e a nat list)
with assms show ?thesis
proof (induct nat arbitrary: t e a list)
case 0
then show ?case by simp
next
case (Suc nat)
from Suc(2,3) obtain t1 e1 a1 ts1 t2 e2 a2 ts2 e' a' where
inv_t1: "tree_invar t1" and
inv_t2: "tree_invar t2" and
eq_t1[simp]: "t1 = (Node e1 a1 nat ts1)" and
eq_t2[simp]: "t2 = (Node e2 a2 nat ts2)"
by (simp only: tree_invar.simps) blast
note heap_t1 = Suc(1)[OF inv_t1 eq_t1]
note heap_t2 = Suc(1)[OF inv_t2 eq_t2]
from link_or_skew heap_t1 heap_t2 show ?case
by (cases "t = link t1 t2") auto
qed
qed

(***********************************************************)

(***********************************************************)

subsubsection "Height and Length"
text ‹
Although complexity of HOL-functions cannot be expressed within
HOL, we can express the height and length of a binomial heap.
By showing that both, height and length, are logarithmic in the number
of contained elements, we give strong evidence that our functions have
logarithmic complexity in the number of elements.
›

text ‹Height of a tree and queue›
fun height_tree :: "('e, ('a::linorder)) SkewBinomialTree ⇒ nat" and
height_queue :: "('e, ('a::linorder)) SkewBinomialQueue ⇒ nat"
where
"height_tree (Node e a r ts) = height_queue ts" |
"height_queue [] = 0" |
"height_queue (t # ts) = max (Suc (height_tree t)) (height_queue ts)"

size (tree_to_multiset t1) + size (tree_to_multiset t2)"
apply(cases t1)
apply(cases t2)
apply simp
done

lemma tree_rank_estimate_upper:
"tree_invar (Node e a r ts) ⟹
size (tree_to_multiset (Node e a r ts)) ≤ (2::nat)^(Suc r) - 1"
proof (induct r arbitrary: e a ts)
case 0
then show ?case by simp
next
case (Suc r)
from Suc(2) obtain e1 a1 ts1 e2 a2 ts2 e' a' where
"(Node e a (Suc r) ts) = link (Node e1 a1 r ts1) (Node e2 a2 r ts2) ∨
(Node e a (Suc r) ts) = skewlink e' a' (Node e1 a1 r ts1) (Node e2 a2 r ts2)"
and inv1: "tree_invar (Node e1 a1 r ts1)"
and inv2: "tree_invar (Node e2 a2 r ts2)"
by simp blast
note iv1 = Suc(1)[OF inv1]
note iv2 = Suc(1)[OF inv2]
have "(2::nat)^r - 1 + (2::nat)^r - 1 ≤ (2::nat)^(Suc r) - 1" by simp
apply (cases "Node e a (Suc r) ts = link (Node e1 a1 r ts1) (Node e2 a2 r ts2)")
using iv1 iv2 apply (simp del: link.simps)
using iv1 iv2 apply (simp del: skewlink.simps)
done
qed

lemma tree_rank_estimate_lower:
"tree_invar (Node e a r ts) ⟹
size (tree_to_multiset (Node e a r ts)) ≥ (2::nat)^r"
proof (induct r arbitrary: e a ts)
case 0
then show ?case by simp
next
case (Suc r)
from Suc(2) obtain e1 a1 ts1 e2 a2 ts2 e' a' where
"(Node e a (Suc r) ts) = link (Node e1 a1 r ts1) (Node e2 a2 r ts2) ∨
(Node e a (Suc r) ts) = skewlink e' a' (Node e1 a1 r ts1) (Node e2 a2 r ts2)"
and inv1: "tree_invar (Node e1 a1 r ts1)"
and inv2: "tree_invar (Node e2 a2 r ts2)"
by simp blast
note iv1 = Suc(1)[OF inv1]
note iv2 = Suc(1)[OF inv2]
have "(2::nat)^r - 1 + (2::nat)^r - 1 ≤ (2::nat)^(Suc r) - 1" by simp
apply (cases "Node e a (Suc r) ts = link (Node e1 a1 r ts1) (Node e2 a2 r ts2)")
using iv1 iv2 apply (simp del: link.simps)
using iv1 iv2 apply (simp del: skewlink.simps)
done
qed

lemma tree_rank_height:
"tree_invar (Node e a r ts) ⟹ height_tree (Node e a r ts) = r"
proof (induct r arbitrary: e a ts)
case 0
then show ?case by simp
next
case (Suc r)
from Suc(2) obtain e1 a1 ts1 e2 a2 ts2 e' a' where
"(Node e a (Suc r) ts) = link (Node e1 a1 r ts1) (Node e2 a2 r ts2) ∨
(Node e a (Suc r) ts) = skewlink e' a' (Node e1 a1 r ts1) (Node e2 a2 r ts2)"
and inv1: "tree_invar (Node e1 a1 r ts1)"
and inv2: "tree_invar (Node e2 a2 r ts2)"
by simp blast
note iv1 = Suc(1)[OF inv1]
note iv2 = Suc(1)[OF inv2]
apply (cases "Node e a (Suc r) ts = link (Node e1 a1 r ts1) (Node e2 a2 r ts2)")
apply (cases "a1 ≤ a2")
using iv1 iv2 apply simp
using iv1 iv2 apply simp
apply (cases "a' ≤ a1 ∧ a' ≤ a2")
apply (simp only: height_tree.simps)
using iv1 iv2 apply simp
apply (cases "a1 ≤ a2")
using iv1 iv2
using iv1 iv2
done
qed

text ‹A skew binomial tree of height $h$ contains at most  $2^{h+1} - 1$
elements›
theorem tree_height_estimate_upper:
"tree_invar t ⟹
size (tree_to_multiset t) ≤ (2::nat)^(Suc (height_tree t)) - 1"
apply (cases t, simp only:)
apply (frule tree_rank_estimate_upper)
apply (frule tree_rank_height)
apply (simp only: )
done

text ‹A skew binomial tree of height $h$ contains at least  $2^{h}$ elements›
theorem tree_height_estimate_lower:
"tree_invar t ⟹ size (tree_to_multiset t) ≥ (2::nat)^(height_tree t)"
apply (cases t, simp only:)
apply (frule tree_rank_estimate_lower)
apply (frule tree_rank_height)
apply (simp only: )
done

lemma size_mset_tree_upper: "tree_invar t ⟹
size (tree_to_multiset t) ≤ (2::nat)^(Suc (rank t)) - (1::nat)"
apply (cases t)
by (simp only: tree_rank_estimate_upper SkewBinomialTree.sel(3))

lemma size_mset_tree_lower: "tree_invar t ⟹
size (tree_to_multiset t) ≥ (2::nat)^(rank t)"
apply (cases t)
by (simp only: tree_rank_estimate_lower SkewBinomialTree.sel(3))

lemma invar_butlast: "invar (bq @ [t]) ⟹ invar bq"
unfolding invar_def
apply (induct bq)
apply simp
apply (case_tac bq)
apply simp
apply (case_tac list)
by simp_all

lemma invar_last_max:
"invar ((b#b'#bq) @ [m]) ⟹ ∀ t ∈ set (b'#bq). rank t < rank m"
unfolding invar_def
apply (induct bq) apply simp apply (case_tac bq) apply simp by simp

lemma invar_last_max': "invar ((b#b'#bq) @ [m]) ⟹ rank b ≤ rank b'"
unfolding invar_def by simp

lemma invar_length: "invar bq ⟹ length bq ≤ Suc (Suc (rank (last bq)))"
proof (induct bq rule: rev_induct)
case Nil thus ?case by simp
next
case (snoc x xs)
show ?case proof (cases xs)
case Nil thus ?thesis by simp
next
case [simp]: (Cons xxs xx)
note Cons' = Cons
thus ?thesis
proof (cases xx)
case Nil with snoc.prems Cons show ?thesis by simp
next
case (Cons xxxs xxx)
from snoc.hyps[OF invar_butlast[OF snoc.prems]] have
IH: "length xs ≤ Suc (Suc (rank (last xs)))" .
also from invar_last_max[OF snoc.prems[unfolded Cons' Cons]]
invar_last_max'[OF snoc.prems[unfolded Cons' Cons]]
last_in_set[of xs] Cons have
"Suc (rank (last xs)) ≤ rank (last (xs @ [x]))" by auto
finally show ?thesis by simp
qed
qed
qed

lemma size_queue_sum_list:
"size (queue_to_multiset bq) = sum_list (map (size ∘ tree_to_multiset) bq)"
by (induct bq) simp_all

text ‹
A skew binomial heap of length $l$ contains at least $2^{l-1} - 1$ elements.
›
theorem queue_length_estimate_lower:
"invar bq ⟹ (size (queue_to_multiset bq)) ≥ 2^(length bq - 1) - 1"
proof (induct bq rule: rev_induct)
case Nil thus ?case by simp
next
case (snoc x xs) thus ?case
proof (cases xs)
case Nil thus ?thesis by simp
next
case [simp]: (Cons xx xxs)
from snoc.hyps[OF invar_butlast[OF snoc.prems]]
have IH: "2 ^ (length xs - 1) ≤ Suc (size (queue_to_multiset xs))" by simp
have size_q:
"size (queue_to_multiset (xs @ [x])) =
size (queue_to_multiset xs) + size (tree_to_multiset x)"
moreover
from snoc.prems have inv_x: "tree_invar x" by (simp add: invar_def)
from size_mset_tree_lower[OF this]
have "2 ^ (rank x) ≤ size (tree_to_multiset x)" .
ultimately have
eq: "size (queue_to_multiset xs) + (2::nat)^(rank x) ≤
size (queue_to_multiset (xs @ [x]))" by simp
from invar_length[OF snoc.prems] have "length xs ≤ (rank x + 1)" by simp
hence snd: "(2::nat) ^ (length xs - 1) ≤ (2::nat) ^ ((rank x))"
by (simp del: power.simps)
have
"(2::nat) ^ (length (xs @ [x]) - 1) =
(2::nat) ^ (length xs - 1) + (2::nat) ^ (length xs - 1)"
by auto
with IH have
"2 ^ (length (xs @ [x]) - 1) ≤
Suc (size (queue_to_multiset xs)) + 2 ^ (length xs - 1)"
by simp
with snd have "2 ^ (length (xs @ [x]) - 1) ≤
Suc (size (queue_to_multiset xs)) + 2 ^ rank x"
by arith
with eq show ?thesis by simp
qed
qed

subsection "Operations"
subsubsection "Empty Tree"
lemma empty_correct: "q=Nil ⟷ queue_to_multiset q = {#}"
apply (cases q)
apply simp
apply (case_tac a)
apply auto
done

subsubsection "Insert"
text ‹Inserts a tree into the queue, such that two trees of same rank get
linked and are recursively inserted. This is the same definition as for
binomial queues and is used for melding.›
fun ins :: "('e, 'a::linorder) SkewBinomialTree ⇒ ('e, 'a) SkewBinomialQueue ⇒
('e, 'a) SkewBinomialQueue" where
"ins t [] = [t]" |
"ins t' (t # bq) =
(if (rank t') < (rank t)
then t' # t # bq
else (if (rank t) < (rank t')
then t # (ins t' bq)
else ins (link t' t) bq))"

text ‹Insert an element with priority into a queue using skewlinks.›
fun insert :: "'e ⇒ 'a::linorder ⇒ ('e, 'a) SkewBinomialQueue ⇒
('e, 'a) SkewBinomialQueue" where
"insert e a [] = [Node e a 0 []]" |
"insert e a [t] = [Node e a 0 [],t]" |
"insert e a (t # t' # bq) =
(if rank t ≠ rank t'
then (Node e a 0 []) # t # t' # bq
else (skewlink e a t t') # bq)"

lemma ins_mset:
"⟦tree_invar t; queue_invar q⟧ ⟹
queue_to_multiset (ins t q) = tree_to_multiset t + queue_to_multiset q"
by (induct q arbitrary: t) (auto simp: union_ac link_tree_invar)

lemma insert_mset: "queue_invar q ⟹
queue_to_multiset (insert e a q) =
queue_to_multiset q + {# (e,a) #}"
by (induct q rule: insert.induct) (auto simp add: union_ac ttm_children)

lemma ins_queue_invar: "⟦tree_invar t; queue_invar q⟧ ⟹ queue_invar (ins t q)"
proof (induct q arbitrary: t)
case Nil
then show ?case by simp
next
case (Cons a q)
note iv = Cons(1)
from Cons(2,3) show ?case
apply (cases "rank t < rank a")
apply simp
apply (cases "rank t = rank a")
defer
using iv[of "t"] apply simp
proof goal_cases
case prems: 1
from prems(2) have inv_a: "tree_invar a" by simp
from prems(2) have inv_q: "queue_invar q" by simp
from iv[OF inv_link inv_q] prems(4) show ?case by simp
qed
qed

lemma insert_queue_invar: "queue_invar q ⟹ queue_invar (insert e a q)"
proof (induct q rule: insert.induct)
case 1
then show ?case by simp
next
case 2
then show ?case by simp
next
case (3 e a t t' bq)
show ?case
proof (cases "rank t = rank t'")
case False
with 3 show ?thesis by simp
next
case True
from 3 have inv_t: "tree_invar t" by simp
from 3 have inv_t': "tree_invar t'" by simp
from 3 skewlink_tree_invar[OF inv_t inv_t' True, of e a] True
show ?thesis by simp
qed
qed

lemma rank_ins2:
"rank_invar bq ⟹
rank t ≤ rank (hd (ins t bq))
∨ (rank (hd (ins t bq)) = rank (hd bq) ∧ bq ≠ [])"
apply (induct bq arbitrary: t)
apply auto
proof goal_cases
case prems: (1 a bq t)
with prems and prems(1)[of "(link t a)"] show ?case
apply (cases bq)
apply auto
done
qed

lemma insert_rank_invar: "rank_skew_invar q ⟹ rank_skew_invar (insert e a q)"
proof (cases q, simp)
fix t q'
assume "rank_skew_invar q" "q = t # q'"
thus "rank_skew_invar (insert e a q)"
proof (cases "q'", (auto intro: gr0I)[1])
fix t' q''
assume "rank_skew_invar q" "q = t # q'" "q' = t' # q''"
thus "rank_skew_invar (insert e a q)"
apply(cases "rank t = rank t'") defer
apply (auto intro: gr0I)[1]
proof goal_cases
case prems: 1
with rank_invar_cons_down[of "t'" "q'"] have "rank_invar q'" by simp
show ?case
proof (cases q'')
case Nil
then show ?thesis by simp
next
case (Cons t'' q''')
with prems have "rank t' < rank t''" by simp
with prems have "rank (skewlink e a t t') ≤ rank t''" by simp
with prems Cons rank_skew_cons_up[of "t''" "q'''" "skewlink e a t t'"]
show ?thesis by simp
qed
qed
qed
qed

lemma insert_invar: "invar q ⟹ invar (insert e a q)"
unfolding invar_def
using insert_queue_invar[of q] insert_rank_invar[of q]
by simp

theorem insert_correct:
assumes I: "invar q"
shows
"invar (insert e a q)"
"queue_to_multiset (insert e a q) = queue_to_multiset q + {# (e,a) #}"
using insert_mset[of q] insert_invar[of q] I
unfolding invar_def by simp_all

subsubsection "meld"
text ‹Remove duplicate tree ranks by inserting the first tree of the
queue into the rest of the queue.›
fun uniqify
:: "('e, 'a::linorder) SkewBinomialQueue ⇒ ('e, 'a) SkewBinomialQueue"
where
"uniqify [] = []" |
"uniqify (t#bq) = ins t bq"

text ‹Meld two uniquified queues using the same definition as for
binomial queues.›
fun meldUniq
:: "('e, 'a::linorder) SkewBinomialQueue ⇒ ('e,'a) SkewBinomialQueue ⇒
('e, 'a) SkewBinomialQueue" where
"meldUniq [] bq = bq" |
"meldUniq bq [] = bq" |
"meldUniq (t1#bq1) (t2#bq2) = (if rank t1 < rank t2
then t1 # (meldUniq bq1 (t2#bq2))
else (if rank t2 < rank t1
then t2 # (meldUniq (t1#bq1) bq2)
else ins (link t1 t2) (meldUniq bq1 bq2)))"

text ‹Meld two queues using above functions.›
definition meld
:: "('e, 'a::linorder) SkewBinomialQueue ⇒ ('e, 'a) SkewBinomialQueue ⇒
('e, 'a) SkewBinomialQueue" where
"meld bq1 bq2 = meldUniq (uniqify bq1) (uniqify bq2)"

lemma invar_uniqify: "queue_invar q ⟹ queue_invar (uniqify q)"
apply(cases q, simp)
done

lemma invar_meldUniq: "⟦queue_invar q; queue_invar q'⟧ ⟹ queue_invar (meldUniq q q')"
proof (induct q q' rule: meldUniq.induct)
case 1
then show ?case by simp
next
case 2
then show ?case by simp
next
case (3 t1 bq1 t2 bq2)
consider (lt) "rank t1 < rank t2" | (gt) "rank t1 > rank t2" | (eq) "rank t1 = rank t2"
by atomize_elim auto
then show ?case
proof cases
case t1t2: lt
from 3(4) have inv_bq1: "queue_invar bq1" by simp
from 3(4) have inv_t1: "tree_invar t1" by simp
from 3(1)[OF t1t2 inv_bq1 3(5)] inv_t1 t1t2
show ?thesis by simp
next
case t1t2: gt
from 3(5) have inv_bq2: "queue_invar bq2" by simp
from 3(5) have inv_t2: "tree_invar t2" by simp
from t1t2 have "¬ rank t1 < rank t2" by simp
from 3(2) [OF this t1t2 3(4) inv_bq2] inv_t2 t1t2
show ?thesis by simp
next
case t1t2: eq
from 3(4) have inv_bq1: "queue_invar bq1" by simp
from 3(4) have inv_t1: "tree_invar t1" by simp
from 3(5) have inv_bq2: "queue_invar bq2" by simp
from 3(5) have inv_t2: "tree_invar t2" by simp
from t1t2 have "¬ rank t1 < rank t2" "¬ rank t2 < rank t1" by auto
note inv_meld = 3(3)[OF this inv_bq1 inv_bq2]
show ?thesis by simp
qed
qed

lemma meld_queue_invar:
assumes "queue_invar q"
and "queue_invar q'"
shows "queue_invar (meld q q')"
proof -
note inv_uniq_q = invar_uniqify[OF assms(1)]
note inv_uniq_q' = invar_uniqify[OF assms(2)]
note inv_meldUniq = invar_meldUniq[OF inv_uniq_q inv_uniq_q']
thus ?thesis by (simp add: meld_def)
qed

lemma uniqify_mset: "queue_invar q ⟹ queue_to_multiset q = queue_to_multiset (uniqify q)"
apply (cases q)
apply simp
done

lemma meldUniq_mset: "⟦queue_invar q; queue_invar q'⟧ ⟹
queue_to_multiset (meldUniq q q') =
queue_to_multiset q + queue_to_multiset q'"
by(induct q q' rule: meldUniq.induct)
(auto simp: ins_mset link_tree_invar invar_meldUniq union_ac)

lemma meld_mset:
"⟦ queue_invar q; queue_invar q' ⟧ ⟹
queue_to_multiset (meld q q') = queue_to_multiset q + queue_to_multiset q'"
by (simp add: meld_def meldUniq_mset invar_uniqify uniqify_mset[symmetric])

text ‹Ins operation satisfies rank invariant, see binomial queues›
lemma rank_ins: "rank_invar bq ⟹ rank_invar (ins t bq)"
proof (induct bq arbitrary: t)
case Nil
then show ?case by simp
next
case (Cons a bq)
then show ?case
apply auto
proof goal_cases
case prems: 1
hence inv: "rank_invar (ins t bq)" by (cases bq) simp_all
from prems have hd: "bq ≠ [] ⟹ rank a < rank (hd bq)"  by (cases bq) auto
from prems have "rank t ≤ rank (hd (ins t bq))
∨ (rank (hd (ins t bq)) = rank (hd bq) ∧ bq ≠ [])"
by (metis rank_ins2 rank_invar_cons_down)
with prems have "rank a < rank (hd (ins t bq))
∨ (rank (hd (ins t bq)) = rank (hd bq) ∧ bq ≠ [])" by auto
with prems and inv and hd show ?case
next
case prems: 2
hence inv: "rank_invar bq" by (cases bq) simp_all
with prems and prems(1)[of "(link t a)"] show ?case by simp
qed
qed

lemma rank_uniqify:
assumes "rank_skew_invar q"
shows "rank_invar (uniqify q)"
proof (cases q)
case Nil
then show ?thesis by simp
next
case (Cons a list)
with rank_skew_rank_invar[of "a" "list"] rank_ins[of "list" "a"] assms
show ?thesis by simp
qed

lemma rank_ins_min: "rank_invar bq ⟹ rank (hd (ins t bq)) ≥ min (rank t) (rank (hd bq))"
proof (induct bq arbitrary: t)
case Nil
then show ?case by simp
next
case (Cons a bq)
then show ?case
apply auto
proof goal_cases
case prems: 1
hence inv: "rank_invar bq" by (cases bq) simp_all
from prems have r: "rank (link t a) = rank a + 1" by (simp add: rank_link)
with prems and inv and prems(1)[of "(link t a)"] show ?case
by (cases bq) auto
qed
qed

lemma rank_invar_not_empty_hd: "⟦rank_invar (t # bq); bq ≠ []⟧ ⟹ rank t < rank (hd bq)"
by (induct bq arbitrary: t) auto

lemma rank_invar_meldUniq_strong:
"⟦rank_invar bq1; rank_invar bq2⟧ ⟹
rank_invar (meldUniq bq1 bq2)
∧ rank (hd (meldUniq bq1 bq2)) ≥ min (rank (hd bq1)) (rank (hd bq2))"
proof (induct bq1 bq2 rule: meldUniq.induct)
case 1
then show ?case by simp
next
case 2
then show ?case by simp
next
case (3 t1 bq1 t2 bq2)
from 3 have inv1: "rank_invar bq1" by (cases bq1) simp_all
from 3 have inv2: "rank_invar bq2" by (cases bq2) simp_all

from inv1 and inv2 and 3 show ?case
apply auto
proof goal_cases
let ?t = "t2"
let ?bq = "bq2"
let ?meldUniq = "rank t2 < rank (hd (meldUniq (t1 # bq1) bq2))"
case prems: 1
hence "?bq ≠ [] ⟹ rank ?t < rank (hd ?bq)"
with prems have ne: "?bq ≠ [] ⟹ ?meldUniq" by simp
from prems have "?bq = [] ⟹ ?meldUniq" by simp
with ne have "?meldUniq" by (cases "?bq = []")
with prems show ?case by (simp add: rank_invar_hd_cons)
next ― ‹analog›
let ?t = "t1"
let ?bq = "bq1"
let ?meldUniq = "rank t1 < rank (hd (meldUniq bq1 (t2 # bq2)))"
case prems: 2
hence "?bq ≠ [] ⟹ rank ?t < rank (hd ?bq)"
with prems have ne: "?bq ≠ [] ⟹ ?meldUniq" by simp
from prems have "?bq = [] ⟹ ?meldUniq" by simp
with ne have "?meldUniq" by (cases "?bq = []")
with prems show ?case by (simp add: rank_invar_hd_cons)
next
case 3
thus ?case by (simp add: rank_ins)
next
case prems: 4 (* Ab hier wirds hässlich *)
have m: "meldUniq bq1 [] = bq1" by (cases bq1) auto

from inv1 and inv2 and prems have
mm: "min (rank (hd bq1)) (rank (hd bq2)) ≤ rank (hd (meldUniq bq1 bq2))"
by simp
from ‹rank_invar (t1 # bq1)› have "bq1 ≠ [] ⟹ rank t1 < rank (hd bq1)"
with prems have r1: "bq1 ≠ [] ⟹ rank t2 < rank (hd bq1)" by simp
from ‹rank_invar (t2 # bq2)› have r2: "bq2 ≠ [] ⟹ rank t2 < rank (hd bq2)"

from inv1 r r1 rank_ins_min[of bq1 "(link t1 t2)"] have
abc1: "bq1 ≠ [] ⟹ rank t2 ≤ rank (hd (ins (link t1 t2) bq1))" by simp
from inv2 r r2 rank_ins_min[of bq2 "(link t1 t2)"] have
abc2: "bq2 ≠ [] ⟹ rank t2 ≤ rank (hd (ins (link t1 t2) bq2))" by simp

from r1 r2 mm have
"⟦bq1 ≠ []; bq2 ≠ []⟧ ⟹ rank t2 < rank (hd (meldUniq bq1 bq2))"
by (simp)
with ‹rank_invar (meldUniq bq1 bq2)› r
rank_ins_min[of "meldUniq bq1 bq2" "link t1 t2"]
have "⟦bq1 ≠ []; bq2 ≠ []⟧ ⟹
rank t2 < rank (hd (ins (link t1 t2) (meldUniq bq1 bq2)))"
by simp
with inv1 and inv2 and r m r1 show ?case
apply(cases "bq2 = []")
apply(cases "bq1 = []")
apply(simp)
apply(cases "bq1 = []")
apply(simp)
done
qed
qed

lemma rank_meldUniq:
"⟦rank_invar bq1; rank_invar bq2⟧ ⟹ rank_invar (meldUniq bq1 bq2)"
by (simp only: rank_invar_meldUniq_strong)

lemma rank_meld:
"⟦rank_skew_invar q1; rank_skew_invar q2⟧ ⟹ rank_skew_invar (meld q1 q2)"
by (simp only: meld_def rank_meldUniq rank_uniqify rank_invar_rank_skew)

theorem meld_invar:
"⟦invar bq1; invar bq2⟧
⟹ invar (meld bq1 bq2)"
by (metis meld_queue_invar rank_meld invar_def)

theorem meld_correct:
assumes I: "invar q" "invar q'"
shows
"invar (meld q q')"
"queue_to_multiset (meld q q') = queue_to_multiset q + queue_to_multiset q'"
using meld_invar[of q q'] meld_mset[of q q'] I
unfolding invar_def by simp_all

subsubsection "Find Minimal Element"
text ‹Find the tree containing the minimal element.›
fun getMinTree :: "('e, 'a::linorder) SkewBinomialQueue ⇒
('e, 'a) SkewBinomialTree" where
"getMinTree [t] = t" |
"getMinTree (t#bq) =
(if prio t ≤ prio (getMinTree bq)
then t
else (getMinTree bq))"

text ‹Find the minimal Element in the queue.›
definition findMin :: "('e, 'a::linorder) SkewBinomialQueue ⇒ ('e × 'a)" where
"findMin bq = (let min = getMinTree bq in (val min, prio min))"

lemma mintree_exists: "(bq ≠ []) = (getMinTree bq ∈ set bq)"
proof (induct bq)
case Nil
then show ?case by simp
next
case (Cons _ bq)
then show ?case by (cases bq) simp_all
qed

"t ∈ set bq ⟹ (val t, prio t) ∈# (queue_to_multiset bq)"
by (induct bq, simp, cases t, auto)

lemma heap_ordered_single:
"heap_ordered t = (∀x ∈ set_mset (tree_to_multiset t). prio t ≤ snd x)"
by (cases t) auto

lemma getMinTree_cons:
"prio (getMinTree (y # x # xs)) ≤ prio (getMinTree (x # xs))"
by (induct xs rule: getMinTree.induct) simp_all

lemma getMinTree_min_tree: "t ∈ set bq  ⟹ prio (getMinTree bq) ≤ prio t"
by (induct bq arbitrary: t rule: getMinTree.induct) (simp, fastforce, simp)

lemma getMinTree_min_prio:
assumes "queue_invar bq"
and "y ∈ set_mset (queue_to_multiset bq)"
shows "prio (getMinTree bq) ≤ snd y"
proof -
from assms have "bq ≠ []" by (cases bq) simp_all
with assms have "∃t ∈ set bq. (y ∈ set_mset (tree_to_multiset t))"
proof (induct bq)
case Nil
then show ?case by simp
next
case (Cons a bq)
then show ?case
apply (cases "y ∈ set_mset (tree_to_multiset a)")
apply simp
apply (cases bq)
apply simp_all
done
qed
from this obtain t where O:
"t ∈ set bq"
"y ∈ set_mset ((tree_to_multiset t))" by blast
obtain e a r ts where [simp]: "t = (Node e a r ts)" by (cases t) blast
from O assms(1) have inv: "tree_invar t" by simp
from tree_invar_heap_ordered[OF inv] heap_ordered.simps[of e a r ts] O
have "prio t ≤ snd y" by auto
with getMinTree_min_tree[OF O(1)] show ?thesis by simp
qed

lemma findMin_mset:
assumes I: "queue_invar q"
assumes NE: "q≠Nil"
shows "findMin q ∈# queue_to_multiset q"
"∀y∈set_mset (queue_to_multiset q). snd (findMin q) ≤ snd y"
proof -
from NE have "getMinTree q ∈ set q" by (simp only: mintree_exists)
thus "findMin q ∈# queue_to_multiset q"
show "∀y∈set_mset (queue_to_multiset q). snd (findMin q) ≤ snd y"
by (simp add: getMinTree_min_prio findMin_def Let_def NE I)
qed

theorem findMin_correct:
assumes I: "invar q"
assumes NE: "q≠Nil"
shows "findMin q ∈# queue_to_multiset q"
"∀y∈set_mset (queue_to_multiset q). snd (findMin q) ≤ snd y"
using I NE findMin_mset
unfolding invar_def by auto

subsubsection "Delete Minimal Element"

text ‹Insert the roots of a given queue into an other queue.›
fun insertList ::
"('e, 'a::linorder) SkewBinomialQueue ⇒ ('e, 'a) SkewBinomialQueue ⇒
('e, 'a) SkewBinomialQueue" where
"insertList [] tbq = tbq" |
"insertList (t#bq) tbq = insertList bq (insert (val t) (prio t) tbq)"

text ‹Remove the first tree, which has the priority $a$ within his root.›
fun remove1Prio :: "'a ⇒ ('e, 'a::linorder) SkewBinomialQueue ⇒
('e, 'a) SkewBinomialQueue" where
"remove1Prio a [] = []" |
"remove1Prio a (t#bq) =
(if (prio t) = a then bq else t # (remove1Prio a bq))"

lemma remove1Prio_remove1[simp]:
"remove1Prio (prio (getMinTree bq)) bq = remove1 (getMinTree bq) bq"
proof (induct bq)
case Nil thus ?case by simp
next
case (Cons t bq)
note iv = Cons
thus ?case
proof (cases "t = getMinTree (t # bq)")
case True
with iv show ?thesis by simp
next
case False
hence ne: "bq ≠ []" by auto
with False have down: "getMinTree (t # bq) = getMinTree bq"
by (induct bq rule: getMinTree.induct) auto
from ne False have "prio t ≠ prio (getMinTree bq)"
by (induct bq rule: getMinTree.induct) auto
with down iv False ne show ?thesis by simp
qed
qed

text ‹Return the queue without the minimal element found by findMin›
definition deleteMin :: "('e, 'a::linorder) SkewBinomialQueue ⇒
('e, 'a) SkewBinomialQueue" where
"deleteMin bq = (let min = getMinTree bq in insertList
(filter (λ t. rank t = 0) (children min))
(meld (rev (filter (λ t. rank t > 0) (children min)))
(remove1Prio (prio min) bq)))"

lemma invar_rev[simp]: "queue_invar (rev q) ⟷ queue_invar q"
by (unfold queue_invar_def) simp

lemma invar_remove1: "queue_invar q ⟹ queue_invar (remove1 t q)"
by (unfold queue_invar_def) (auto)

lemma mset_rev: "queue_to_multiset (rev q) = queue_to_multiset q"
by (induct q) (auto simp add: union_ac)

lemma in_set_subset: "t ∈ set q ⟹ tree_to_multiset t ⊆# queue_to_multiset q"
proof (induct q)
case Nil
then show ?case by simp
next
case (Cons a q)
show ?case
proof (cases "t = a")
case True
then show ?thesis by simp
next
case False
with Cons have t_in_q: "t ∈ set q" by simp
have "queue_to_multiset q ⊆# queue_to_multiset (a # q)"
by simp
from subset_mset.order_trans[OF Cons(1)[OF t_in_q] this] show ?thesis .
qed
qed

lemma mset_remove1: "t ∈ set q ⟹
queue_to_multiset (remove1 t q) =
queue_to_multiset q - tree_to_multiset t"
by (induct q) (auto simp: in_set_subset)

lemma invar_children':
assumes "tree_invar t"
shows "queue_invar (children t)"
proof (cases t)
case (Node e a nat list)
with assms have inv: "tree_invar (Node e a nat list)" by simp
from Node invar_children[OF inv] show ?thesis by simp
qed

lemma invar_filter: "queue_invar q ⟹ queue_invar (filter f q)"
by (unfold queue_invar_def) simp

lemma insertList_queue_invar: "queue_invar q ⟹ queue_invar (insertList ts q)"
proof (induct ts arbitrary: q)
case Nil
then show ?case by simp
next
case (Cons a q)
note inv_insert = insert_queue_invar[OF Cons(2), of "val a" "prio a"]
from Cons(1)[OF inv_insert] show ?case by simp
qed

lemma deleteMin_queue_invar:
"⟦queue_invar q; queue_to_multiset q ≠ {#}⟧ ⟹
queue_invar (deleteMin q)"
unfolding deleteMin_def Let_def
proof goal_cases
case prems: 1
from prems(2) have q_ne: "q ≠ []" by auto
with prems(1) mintree_exists[of q]
have inv_min: "tree_invar (getMinTree q)" by simp
note inv_rem = invar_remove1[OF prems(1), of "getMinTree q"]
note inv_children = invar_children'[OF inv_min]
note inv_filter = invar_filter[OF inv_children, of "λt. 0 < rank t"]
note inv_rev = iffD2[OF invar_rev inv_filter]
note inv_meld = meld_queue_invar[OF inv_rev inv_rem]
note inv_ins =
insertList_queue_invar[OF inv_meld,
of "[t←children (getMinTree q). rank t = 0]"]
then show ?case by simp
qed

lemma mset_children: "queue_to_multiset (children t) =
tree_to_multiset t - {# (val t, prio t) #}"
by(cases t, auto)

lemma mset_insertList:
"⟦∀t ∈ set ts. rank t = 0 ∧ children t = [] ; queue_invar q⟧ ⟹
queue_to_multiset (insertList ts q) =
queue_to_multiset ts + queue_to_multiset q"
proof (induct ts arbitrary: q)
case Nil
then show ?case by simp
next
case (Cons a ts)
from Cons(2) have ball_ts: "∀t∈set ts. rank t = 0 ∧ children t = []" by simp
note inv_insert = insert_queue_invar[OF Cons(3), of "val a" "prio a"]
note iv = Cons(1)[OF ball_ts inv_insert]
from Cons(2) have mset_a: "tree_to_multiset a = {# (val a, prio a)#}"
by (cases a) simp
note insert_mset[OF Cons(3), of "val a" "prio a"]
with mset_a iv show ?case by (simp add: union_ac)
qed

lemma mset_filter: "(queue_to_multiset [t←q . rank t = 0]) +
queue_to_multiset [t←q . 0 < rank t] =
queue_to_multiset q"
by (induct q) (auto simp add: union_ac)

lemma deleteMin_mset:
assumes "queue_invar q"
and "queue_to_multiset q ≠ {#}"
shows "queue_to_multiset (deleteMin q) = queue_to_multiset q - {# (findMin q) #}"
proof -
from assms(2) have q_ne: "q ≠ []" by auto
with mintree_exists[of q]
have min_in_q: "getMinTree q ∈ set q" by simp
with assms(1) have inv_min: "tree_invar (getMinTree q)" by simp
note inv_rem = invar_remove1[OF assms(1), of "getMinTree q"]
note inv_children = invar_children'[OF inv_min]
note inv_filter = invar_filter[OF inv_children, of "λt. 0 < rank t"]
note inv_rev = iffD2[OF invar_rev inv_filter]
note inv_meld = meld_queue_invar[OF inv_rev inv_rem]
note mset_rem = mset_remove1[OF min_in_q]
note mset_rev = mset_rev[of "[t←children (getMinTree q). 0 < rank t]"]
note mset_meld = meld_mset[OF inv_rev inv_rem]
note mset_children = mset_children[of "getMinTree q"]
thm mset_insertList[of "[t←children (getMinTree q) .
rank t = 0]"]
have "⟦tree_invar t; rank t = 0⟧ ⟹ children t = []" for t
by (cases t) simp
with inv_children
have ball_min: "∀t∈set [t←children (getMinTree q). rank t = 0].
rank t = 0 ∧ children t = []" by (unfold queue_invar_def) auto
note mset_insertList = mset_insertList[OF ball_min inv_meld]
note mset_filter = mset_filter[of "children (getMinTree q)"]
let ?Q = "queue_to_multiset q"
let ?MT = "tree_to_multiset (getMinTree q)"
"{# (val (getMinTree q), prio (getMinTree q)) #} ⊆# ?MT"
by(cases "getMinTree q") simp
note min_subset_q = in_set_subset[OF min_in_q]
from mset_insertList mset_meld mset_rev mset_rem mset_filter mset_children
multiset_diff_union_assoc[OF head_subset_min, of "?Q - ?MT"]
mset_subset_eq_multiset_union_diff_commute[OF min_subset_q, of "?MT"]
show ?thesis
by (auto simp add: deleteMin_def Let_def union_ac findMin_def)
qed

lemma rank_insertList: "rank_skew_invar q ⟹ rank_skew_invar (insertList ts q)"
by (induct ts arbitrary: q) (simp_all add: insert_rank_invar)

lemma insertList_invar: "invar q ⟹ invar (insertList ts q)"
proof (induct ts arbitrary: q)
case Nil
then show ?case by simp
next
case (Cons a q)
show ?case
apply (unfold insertList.simps)
proof goal_cases
case 1
from Cons(2) insert_rank_invar[of "q" "val a" "prio a"]
have a1: "rank_skew_invar (insert (val a) (prio a) q)"
from Cons(2) insert_queue_invar[of "q" "val a" "prio a"]
have a2: "queue_invar (insert (val a) (prio a) q)" by (simp add: invar_def)
from a1 a2 have "invar (insert (val a) (prio a) q)" by (simp add: invar_def)
with Cons(1)[of "(insert (val a) (prio a) q)"] show ?case .
qed
qed

lemma children_rank_less:
assumes "tree_invar t"
shows "∀t' ∈ set (children t). rank t' < rank t"
proof (cases t)
case (Node e a nat list)
with assms show ?thesis
proof (induct nat arbitrary: t e a list)
case 0
then show ?case by simp
next
case (Suc nat)
then obtain e1 a1 ts1 e2 a2 ts2 e' a' where
O: "tree_invar (Node e1 a1 nat ts1)"  "tree_invar (Node e2 a2 nat ts2)"
"t = link (Node e1 a1 nat ts1) (Node e2 a2 nat ts2)
∨ t = skewlink e' a' (Node e1 a1 nat ts1) (Node e2 a2 nat ts2)"
by (simp only: tree_invar.simps) blast
hence ch_id:
"children t = (if a1 ≤ a2 then (Node e2 a2 nat ts2)#ts1
else (Node e1 a1 nat ts1)#ts2) ∨
children t =
(if a' ≤ a1 ∧ a' ≤ a2 then [(Node e1 a1 nat ts1), (Node e2 a2 nat ts2)]
else (if a1 ≤ a2 then (Node e' a' 0 []) # (Node e2 a2 nat ts2) # ts1
else (Node e' a' 0 []) # (Node e1 a1 nat ts1) # ts2))"
by auto
from O Suc(1)[of "Node e1 a1 nat ts1" "e1" "a1" "ts1"]
have  p1: "∀t'∈set ((Node e2 a2 nat ts2) # ts1). rank t' < Suc nat" by auto
from O Suc(1)[of "Node e2 a2 nat ts2" "e2" "a2" "ts2"]
have p2: "∀t'∈set ((Node e1 a1 nat ts1) # ts2). rank t' < Suc nat" by auto
from O have
p3: "∀t' ∈ set [(Node e1 a1 nat ts1), (Node e2 a2 nat ts2)].
rank t' < Suc nat" by simp
from O Suc(1)[of "Node e1 a1 nat ts1" "e1" "a1" "ts1"]
have
p4: "∀t' ∈ set ((Node e' a' 0 []) # (Node e2 a2 nat ts2) # ts1).
rank t' < Suc nat" by auto
from O Suc(1)[of "Node e2 a2 nat ts2" "e2" "a2" "ts2"]
have p5:
"∀t' ∈ set ((Node e' a' 0 []) # (Node e1 a1 nat ts1) # ts2).
rank t' < Suc nat" by auto
from Suc(3) p1 p2 p3 p4 p5 ch_id show ?case
by(cases "children t = (if a1 ≤ a2 then Node e2 a2 nat ts2 # ts1
else Node e1 a1 nat ts1 # ts2)") simp_all
qed
qed

lemma strong_rev_children:
assumes "tree_invar t"
shows "invar (rev [t ← children t. 0 < rank t])"
proof (cases t)
case (Node e a nat list)
with assms show ?thesis
proof (induct "nat" arbitrary: t e a list)
case 0
then show ?case by (simp add: invar_def)
next
case (Suc nat)
show ?case
proof (cases "nat")
case 0
with Suc obtain e1 a1 e2 a2 e' a' where
O: "tree_invar (Node e1 a1 0 [])" "tree_invar (Node e2 a2 0 [])"
"t = link (Node e1 a1 0 []) (Node e2 a2 0 [])
∨ t = skewlink e' a' (Node e1 a1 0 []) (Node e2 a2 0 [])"
by (simp only: tree_invar.simps) blast
hence "[t ← children t. 0 < rank t] = []" by auto
then show ?thesis by (simp add: invar_def)
next
case Suc': (Suc n)
from Suc obtain e1 a1 ts1 e2 a2 ts2 e' a' where
O: "tree_invar (Node e1 a1 nat ts1)" "tree_invar (Node e2 a2 nat ts2)"
"t = link (Node e1 a1 nat ts1) (Node e2 a2 nat ts2)
∨ t = skewlink e' a' (Node e1 a1 nat ts1) (Node e2 a2 nat ts2)"
by (simp only: tree_invar.simps) blast
hence ch_id:
"children t = (if a1 ≤ a2 then
(Node e2 a2 nat ts2)#ts1
else (Node e1 a1 nat ts1)#ts2)
∨
children t = (if a' ≤ a1 ∧ a' ≤ a2 then
[(Node e1 a1 nat ts1), (Node e2 a2 nat ts2)]
else (if a1 ≤ a2 then
(Node e' a' 0 []) # (Node e2 a2 nat ts2) # ts1
else (Node e' a' 0 []) # (Node e1 a1 nat ts1) # ts2))"
by auto
from O Suc(1)[of "Node e1 a1 nat ts1" "e1" "a1" "ts1"] have
rev_ts1: "invar (rev [t ← ts1. 0 < rank t])" by simp
from O children_rank_less[of "Node e1 a1 nat ts1"] have
"∀t∈set (rev [t ← ts1. 0 < rank t]). rank t < rank (Node e2 a2 nat ts2)"
by simp
with O rev_ts1
invar_app_single[of "rev [t ← ts1. 0 < rank t]"
"Node e2 a2 nat ts2"]
have
"invar (rev ((Node e2 a2 nat ts2) # [t ← ts1. 0 < rank t]))"
by simp
with Suc' have p1: "invar (rev [t ← ((Node e2 a2 nat ts2) # ts1). 0 < rank t])"
by simp
from O Suc(1)[of "Node e2 a2 nat ts2" "e2" "a2" "ts2"]
have rev_ts2: "invar (rev [t ← ts2. 0 < rank t])" by simp
from O children_rank_less[of "Node e2 a2 nat ts2"]
have "∀t∈set (rev [t ← ts2. 0 < rank t]).
rank t < rank (Node e1 a1 nat ts1)" by simp
with O rev_ts2 invar_app_single[of "rev [t ← ts2. 0 < rank t]"
"Node e1 a1 nat ts1"]
have "invar (rev [t ← ts2. 0 < rank t] @ [Node e1 a1 nat ts1])"
by simp
with Suc' have p2: "invar (rev [t ← ((Node e1 a1 nat ts1) # ts2). 0 < rank t])"
by simp
from O(1-2)
have p3: "invar (rev (filter (λ t. 0 < rank t)
[(Node e1 a1 nat ts1), (Node e2 a2 nat ts2)]))"
by (cases "children t = (if a1