# Theory Prio_Map_Specs

section ‹Priority Map Specifications›

theory Prio_Map_Specs
imports "HOL-Data_Structures.Map_Specs"
begin

(*<*)
(** TODO/FIXME:
Duplicated from List_Ins_Del.
We cannot import this theory, as it has name clashed with AList_Upd_Del!
*)
lemma sorted_Cons_iff:
"sorted(x # xs) = ((∀y ∈ set xs. x < y) ∧ sorted xs)"

(** TODO: Belongs into AList_Upd_Del *)
lemma sorted_map_of_Some_eq:
"sorted1 xs ⟹ map_of xs k = Some v ⟷ (k,v)∈set xs"
by (induction xs arbitrary: k v) (auto split: if_splits simp: sorted_Cons_iff)

(*>*)

subsection ‹Abstract Data Type›

locale PrioMap = Map where lookup = lookup
for lookup :: "'m ⇒ 'a ⇒ 'b::linorder option" +
fixes is_empty :: "'m ⇒ bool"
fixes getmin :: "'m ⇒ 'a × 'b"
assumes map_is_empty: "invar m ⟹ is_empty m ⟷ lookup m = Map.empty"
and map_getmin: "getmin m = (k,p) ⟹ invar m ⟹ lookup m ≠ Map.empty
⟹ lookup m k = Some p ∧ (∀p'∈ran (lookup m). p≤p')"
begin

lemmas prio_map_specs = map_specs map_is_empty

lemma map_getminE:
assumes "getmin m = (k,p)" "invar m" "lookup m ≠ Map.empty"
obtains "lookup m k = Some p" "∀k' p'. lookup m k' = Some p' ⟶ p≤p'"
using map_getmin[OF assms] by (auto simp: ran_def)

end

definition is_min2 :: "(_×'a::linorder) ⇒ (_×'a) set ⇒ bool" where
"is_min2 x xs ≡ x∈xs ∧ (∀y∈xs. snd x ≤ snd y)"

subsection ‹Inorder-Based Specification›

locale PrioMap_by_Ordered = Map_by_Ordered
where lookup=lookup for lookup :: "'t ⇒ 'a::linorder ⇒ 'b::linorder option" +
fixes is_empty :: "'t ⇒ bool"
fixes getmin :: "'t ⇒ 'a×'b"
assumes inorder_isempty': "⟦inv t; sorted1 (inorder t)⟧
⟹ is_empty t ⟷ inorder t = []"
and inorder_getmin':
"⟦inv t; sorted1 (inorder t); inorder t ≠ []; getmin t = (a,b)⟧
⟹ is_min2 (a,b) (set (inorder t))"
begin

lemma
inorder_isempty: "invar t ⟹ is_empty t ⟷ inorder t = []"
and inorder_getmin: "⟦invar t; inorder t ≠ []; getmin t = (a,b)⟧
⟹ is_min2 (a,b) (set (inorder t))"
unfolding invar_def by (auto simp: inorder_isempty' inorder_getmin')

lemma inorder_lookup_empty_iff:
"invar m ⟹ lookup m = Map.empty ⟷ inorder m = []"
using inorder_lookup[of m]
apply (auto split: if_splits simp: invar_def)
by (metis map_of.elims option.discI)

lemma inorder_lookup_ran_eq:
"⟦inv m; sorted1 (inorder m)⟧ ⟹ ran (lookup m) = snd  set (inorder m)"
using inorder_lookup[of m] unfolding ran_def
by (force simp: sorted_map_of_Some_eq)

sublocale PrioMap empty update delete invar lookup is_empty getmin
apply unfold_locales
apply (auto simp: inorder_isempty inorder_lookup_empty_iff)
apply (frule (2) inorder_getmin)
apply (auto simp: is_min2_def sorted_map_of_Some_eq invar_def inorder_lookup) []
apply (frule (2) inorder_getmin)
apply (force simp: is_min2_def sorted_map_of_Some_eq inorder_lookup_ran_eq
eq_Min_iff invar_def inorder_lookup) []
done

end

end


# Theory PST_General

section ‹General Priority Search Trees›

theory PST_General
imports
"HOL-Data_Structures.Tree2"
Prio_Map_Specs
begin

text ‹\noindent
We show how to implement priority maps
by augmented binary search trees. That is, the basic data structure is some
arbitrary binary search tree, e.g.\ a red-black tree, implementing the map
from @{typ 'a} to @{typ 'b} by storing pairs ‹(k,p)› in each node. At this
point we need to assume that the keys are also linearly ordered. To
implement ‹getmin› efficiently we annotate/augment each node with another pair
‹(k',p')›, the intended result of ‹getmin› when applied to that subtree. The
specification of ‹getmin› tells us that ‹(k',p')› must be in that subtree and
that ‹p'› is the minimal priority in that subtree. Thus the annotation can be
computed by passing the ‹(k',p')› with the minimal ‹p'› up the tree. We will
now make this more precise for balanced binary trees in general.

We assume that our trees are either leaves of the form @{term Leaf} or nodes
of the form @{term "Node l (kp, b) r"} where ‹l› and ‹r› are subtrees, ‹kp› is
the contents of the node (a key-priority pair) and ‹b› is some additional
balance information (e.g.\ colour, height, size, \dots). Augmented nodes are
of the form \<^term>‹Node l (kp, (b,kp')) r›.
›

type_synonym ('k,'p,'c) pstree = "(('k×'p) × ('c × ('k × 'p))) tree"

text ‹
The following invariant states that a node annotation is actually a minimal
key-priority pair for the node's subtree.
›

fun invpst :: "('k,'p::linorder,'c) pstree ⇒ bool" where
"invpst Leaf = True"
| "invpst (Node l (x, _,mkp) r) ⟷ invpst l ∧ invpst r
∧ is_min2 mkp (set (inorder l @ x # inorder r))"

text ‹The implementation of ‹getmin› is trivial:›

fun pst_getmin where
"pst_getmin (Node _ (_, _,a) _) = a"

lemma pst_getmin_ismin:
"invpst t ⟹ t≠Leaf ⟹ is_min2 (pst_getmin t) (set_tree t)"
by (cases t rule: pst_getmin.cases) auto

text ‹
It remains to upgrade the existing map operations to work with augmented nodes.
Therefore we now show how to transform any function definition on un-augmented
trees into one on trees augmented with ‹(k',p')› pairs. A defining equation
‹f pats = e› for the original type of nodes is transformed into an equation
‹f pats' = e'› on the augmented type of nodes as follows:
▪ Every pattern @{term "Node l (kp, b) r"} in ‹pats› and ‹e› is replaced by
@{term "Node l (kp, (b,DUMMY)) r"} to obtain ‹pats'› and ‹e⇩2›.
▪ To obtain ‹e'›, every expression @{term "Node l (kp, b) r"} in ‹e⇩2› is
replaced by ‹mkNode l kp b r› where:
›

definition "min2 ≡ λ(k,p) (k',p'). if p≤p' then (k,p) else (k',p')"

definition "min_kp a l r ≡ case (l,r) of
(Leaf,Leaf) ⇒ a
| (Leaf,Node _ (_, (_,kpr)) _) ⇒ min2 a kpr
| (Node _ (_, (_,kpl)) _,Leaf) ⇒ min2 a kpl
| (Node _ (_, (_,kpl)) _,Node _ (_, (_,kpr)) _) ⇒ min2 a (min2 kpl kpr)"

definition "mkNode c l a r ≡ Node l (a, (c,min_kp a l r)) r"

text ‹
Note that this transformation does not affect the asymptotic complexity
of ‹f›. Therefore the priority search tree operations have the same complexity
as the underlying search tree operations, i.e.\ typically logarithmic
(‹update›, ‹delete›, ‹lookup›) and constant time (‹empty›, ‹is_empty›).
›

text ‹It is straightforward to show that @{const mkNode} preserves the invariant:›

lemma is_min2_Empty[simp]: "¬is_min2 x {}"
by (auto simp: is_min2_def)

lemma is_min2_singleton[simp]: "is_min2 a {b} ⟷ b=a"
by (auto simp: is_min2_def)

lemma is_min2_insert:
"is_min2 x (insert y ys)
⟷ (y=x ∧ (∀z∈ys. snd x ≤ snd z)) ∨ (snd x ≤ snd y ∧ is_min2 x ys)"
by (auto simp: is_min2_def)

lemma is_min2_union:
"is_min2 x (ys ∪ zs)
⟷ (is_min2 x ys ∧ (∀z∈zs. snd x ≤ snd z))
∨ ((∀y∈ys. snd x ≤ snd y) ∧ is_min2 x zs)"
by (auto simp: is_min2_def)

lemma is_min2_min2_insI: "is_min2 y ys ⟹ is_min2 (min2 x y) (insert x ys)"
by (auto simp: is_min2_def min2_def split: prod.split)

lemma is_min2_mergeI:
"is_min2 x xs ⟹ is_min2 y ys ⟹ is_min2 (min2 x y) (xs ∪ ys)"
by (auto simp: is_min2_def min2_def split: prod.split)

theorem invpst_mkNode[simp]: "invpst (mkNode c l a r) ⟷ invpst l ∧ invpst r"
apply (cases l rule: invpst.cases;
cases r rule: invpst.cases;
subgoal using is_min2_min2_insI by blast
subgoal by (auto intro!: is_min2_min2_insI simp: insert_commute)
subgoal by (smt Un_insert_left Un_insert_right is_min2_mergeI is_min2_min2_insI
sup_assoc)
done

end


# Theory PST_RBT

section ‹Priority Search Trees on top of RBTs›

theory PST_RBT
imports
"HOL-Data_Structures.Cmp"
"HOL-Data_Structures.Isin2"
"HOL-Data_Structures.Lookup2"
PST_General
begin

text ‹
We obtain a priority search map based on red-black trees via the
general priority search tree augmentation.

This theory has been derived from the standard Isabelle implementation of red
black trees in @{session "HOL-Data_Structures"}.
›

subsection ‹Definitions›

subsubsection ‹The Code›

datatype tcolor = Red | Black

type_synonym ('k,'p) rbth = "(('k×'p) × (tcolor × ('k × 'p))) tree"

abbreviation R where "R mkp l a r ≡ Node l (a, Red,mkp) r"
abbreviation B where "B mkp l a r ≡ Node l (a, Black,mkp) r"

abbreviation "mkR ≡ mkNode Red"
abbreviation "mkB ≡ mkNode Black"

fun baliL :: "('k,'p::linorder) rbth ⇒ 'k×'p ⇒ ('k,'p) rbth ⇒ ('k,'p) rbth"
where
"baliL (R _ (R _ t1 a1 t2) a2 t3) a3 t4 = mkR (mkB t1 a1 t2) a2 (mkB t3 a3 t4)"
| "baliL (R _ t1 a1 (R _ t2 a2 t3)) a3 t4 = mkR (mkB t1 a1 t2) a2 (mkB t3 a3 t4)"
| "baliL t1 a t2 = mkB t1 a t2"

fun baliR :: "('k,'p::linorder) rbth ⇒ 'k×'p ⇒ ('k,'p) rbth ⇒ ('k,'p) rbth"
where
"baliR t1 a1 (R _ (R _ t2 a2 t3) a3 t4) = mkR (mkB t1 a1 t2) a2 (mkB t3 a3 t4)" |
"baliR t1 a1 (R _ t2 a2 (R _ t3 a3 t4)) = mkR (mkB t1 a1 t2) a2 (mkB t3 a3 t4)" |
"baliR t1 a t2 = mkB t1 a t2"

fun paint :: "tcolor ⇒ ('k,'p::linorder) rbth ⇒ ('k,'p::linorder) rbth" where
"paint c Leaf = Leaf" |
"paint c (Node l (a, (_,mkp)) r) = Node l (a, (c,mkp)) r"

fun baldL :: "('k,'p::linorder) rbth ⇒ 'k × 'p ⇒ ('k,'p::linorder) rbth
⇒ ('k,'p::linorder) rbth"
where
"baldL (R _ t1 x t2) y t3 = mkR (mkB t1 x t2) y t3" |
"baldL bl x (B _ t1 y t2) = baliR bl x (mkR t1 y t2)" |
"baldL bl x (R _ (B _ t1 y t2) z t3)
= mkR (mkB bl x t1) y (baliR t2 z (paint Red t3))" |
"baldL t1 x t2 = mkR t1 x t2"

fun baldR :: "('k,'p::linorder) rbth ⇒ 'k × 'p ⇒ ('k,'p::linorder) rbth
⇒ ('k,'p::linorder) rbth"
where
"baldR t1 x (R _ t2 y t3) = mkR t1 x (mkB t2 y t3)" |
"baldR (B _ t1 x t2) y t3 = baliL (mkR t1 x t2) y t3" |
"baldR (R _ t1 x (B _ t2 y t3)) z t4
= mkR (baliL (paint Red t1) x t2) y (mkB t3 z t4)" |
"baldR t1 x t2 = mkR t1 x t2"

fun combine :: "('k,'p::linorder) rbth ⇒ ('k,'p::linorder) rbth
⇒ ('k,'p::linorder) rbth"
where
"combine Leaf t = t" |
"combine t Leaf = t" |
"combine (R _ t1 a t2) (R _ t3 c t4) =
(case combine t2 t3 of
R _ u2 b u3 ⇒ (mkR (mkR t1 a u2) b (mkR u3 c t4)) |
t23 ⇒ mkR t1 a (mkR t23 c t4))" |
"combine (B _ t1 a t2) (B _ t3 c t4) =
(case combine t2 t3 of
R _ t2' b t3' ⇒ mkR (mkB t1 a t2') b (mkB t3' c t4) |
t23 ⇒ baldL t1 a (mkB t23 c t4))" |
"combine t1 (R _ t2 a t3) = mkR (combine t1 t2) a t3" |
"combine (R _ t1 a t2) t3 = mkR t1 a (combine t2 t3)"

fun color :: "('k,'p) rbth ⇒ tcolor" where
"color Leaf = Black" |
"color (Node _ (_, (c,_)) _) = c"

fun upd :: "'a::linorder ⇒ 'b::linorder ⇒ ('a,'b) rbth ⇒ ('a,'b) rbth" where
"upd x y Leaf = mkR Leaf (x,y) Leaf" |
"upd x y (B _ l (a,b) r) = (case cmp x a of
LT ⇒ baliL (upd x y l) (a,b) r |
GT ⇒ baliR l (a,b) (upd x y r) |
EQ ⇒ mkB l (x,y) r)" |
"upd x y (R _ l (a,b) r) = (case cmp x a of
LT ⇒ mkR (upd x y l) (a,b) r |
GT ⇒ mkR l (a,b) (upd x y r) |
EQ ⇒ mkR l (x,y) r)"

definition update :: "'a::linorder ⇒ 'b::linorder ⇒ ('a,'b) rbth ⇒ ('a,'b) rbth"
where
"update x y t = paint Black (upd x y t)"

fun del :: "'a::linorder ⇒ ('a,'b::linorder)rbth ⇒ ('a,'b)rbth" where
"del x Leaf = Leaf" |
"del x (Node l ((a,b), (c,_)) r) = (case cmp x a of
LT ⇒ if l ≠ Leaf ∧ color l = Black
then baldL (del x l) (a,b) r else mkR (del x l) (a,b) r |
GT ⇒ if r ≠ Leaf∧ color r = Black
then baldR l (a,b) (del x r) else mkR l (a,b) (del x r) |
EQ ⇒ combine l r)"

definition delete :: "'a::linorder ⇒ ('a,'b::linorder) rbth ⇒ ('a,'b) rbth" where
"delete x t = paint Black (del x t)"

subsubsection ‹Invariants›

fun bheight :: "('k,'p) rbth ⇒ nat" where
"bheight Leaf = 0" |
"bheight (Node l (x, (c,_)) r) = (if c = Black then bheight l + 1 else bheight l)"

fun invc :: "('k,'p) rbth ⇒ bool" where
"invc Leaf = True" |
"invc (Node l (a, (c,_)) r) =
(invc l ∧ invc r ∧ (c = Red ⟶ color l = Black ∧ color r = Black))"

fun invc2 :: "('k,'p) rbth ⇒ bool" ― ‹Weaker version› where
"invc2 Leaf = True" |
"invc2 (Node l (a, _) r) = (invc l ∧ invc r)"

fun invh :: "('k,'p) rbth ⇒ bool" where
"invh Leaf = True" |
"invh (Node l (x, _) r) = (invh l ∧ invh r ∧ bheight l = bheight r)"

definition rbt :: "('k,'p::linorder) rbth ⇒ bool" where
"rbt t = (invc t ∧ invh t ∧ invpst t ∧ color t = Black)"

subsection ‹Functional Correctness›

lemma inorder_paint[simp]: "inorder(paint c t) = inorder t"
by(cases t) (auto)

lemma inorder_mkNode[simp]:
"inorder (mkNode c l a r) = inorder l @ a # inorder r"
by (auto simp: mkNode_def)

lemma inorder_baliL[simp]:
"inorder(baliL l a r) = inorder l @ a # inorder r"
by(cases "(l,a,r)" rule: baliL.cases) (auto)

lemma inorder_baliR[simp]:
"inorder(baliR l a r) = inorder l @ a # inorder r"
by(cases "(l,a,r)" rule: baliR.cases) (auto)

lemma inorder_baldL[simp]:
"inorder(baldL l a r) = inorder l @ a # inorder r"
by (cases "(l,a,r)" rule: baldL.cases) auto

lemma inorder_baldR[simp]:
"inorder(baldR l a r) = inorder l @ a # inorder r"
by(cases "(l,a,r)" rule: baldR.cases) auto

lemma inorder_combine[simp]:
"inorder(combine l r) = inorder l @ inorder r"
by (induction l r rule: combine.induct) (auto split: tree.split tcolor.split)

lemma inorder_upd:
"sorted1(inorder t) ⟹ inorder(upd x y t) = upd_list x y (inorder t)"
by(induction x y t rule: upd.induct)
(auto simp: upd_list_simps)

lemma inorder_update:
"sorted1(inorder t) ⟹ inorder(update x y t) = upd_list x y (inorder t)"

lemma inorder_del:
"sorted1(inorder t) ⟹  inorder(del x t) = del_list x (inorder t)"
by(induction x t rule: del.induct)
(auto simp: del_list_simps)

lemma inorder_delete:
"sorted1(inorder t) ⟹ inorder(delete x t) = del_list x (inorder t)"

subsection ‹Invariant Preservation›

lemma color_paint_Black: "color (paint Black t) = Black"
by (cases t) auto

theorem rbt_Leaf: "rbt Leaf"

lemma invc2I: "invc t ⟹ invc2 t"
by (cases t rule: invc.cases) simp+

lemma paint_invc2: "invc2 t ⟹ invc2 (paint c t)"
by (cases t) auto

lemma invc_paint_Black: "invc2 t ⟹ invc (paint Black t)"
by (cases t) auto

lemma invh_paint: "invh t ⟹ invh (paint c t)"
by (cases t) auto

lemma invc_mkRB[simp]:
"invc (mkR l a r) ⟷ invc l ∧ invc r ∧ color l = Black ∧ color r = Black"
"invc (mkB l a r) ⟷ invc l ∧ invc r"

lemma color_mkNode[simp]: "color (mkNode c l a r) = c"

subsubsection ‹Update›

lemma invc_baliL:
"⟦invc2 l; invc r⟧ ⟹ invc (baliL l a r)"
by (induct l a r rule: baliL.induct) auto

lemma invc_baliR:
"⟦invc l; invc2 r⟧ ⟹ invc (baliR l a r)"
by (induct l a r rule: baliR.induct) auto

lemma bheight_mkRB[simp]:
"bheight (mkR l a r) = bheight l"
"bheight (mkB l a r) = Suc (bheight l)"

lemma bheight_baliL:
"bheight l = bheight r ⟹ bheight (baliL l a r) = Suc (bheight l)"
by (induct l a r rule: baliL.induct) auto

lemma bheight_baliR:
"bheight l = bheight r ⟹ bheight (baliR l a r) = Suc (bheight l)"
by (induct l a r rule: baliR.induct) auto

lemma invh_mkNode[simp]:
"invh (mkNode c l a r) ⟷ invh l ∧ invh r ∧ bheight l = bheight r"

lemma invh_baliL:
"⟦ invh l; invh r; bheight l = bheight r ⟧ ⟹ invh (baliL l a r)"
by (induct l a r rule: baliL.induct) auto

lemma invh_baliR:
"⟦ invh l; invh r; bheight l = bheight r ⟧ ⟹ invh (baliR l a r)"
by (induct l a r rule: baliR.induct) auto

lemma invc_upd: assumes "invc t"
shows "color t = Black ⟹ invc (upd x y t)" "invc2 (upd x y t)"
using assms
by (induct x y t rule: upd.induct)
(auto simp: invc_baliL invc_baliR invc2I mkNode_def)

lemma invh_upd: assumes "invh t"
shows "invh (upd x y t)" "bheight (upd x y t) = bheight t"
using assms
by(induct x y t rule: upd.induct)
(auto simp: invh_baliL invh_baliR bheight_baliL bheight_baliR)

lemma invpst_paint[simp]: "invpst (paint c t) = invpst t"
by (cases "(c,t)" rule: paint.cases) auto

lemma invpst_baliR: "invpst l ⟹ invpst r ⟹ invpst (baliR l a r)"
by (cases "(l,a,r)" rule: baliR.cases) auto

lemma invpst_baliL: "invpst l ⟹ invpst r ⟹ invpst (baliL l a r)"
by (cases "(l,a,r)" rule: baliL.cases) auto

lemma invpst_upd: "invpst t ⟹ invpst (upd x y t)"
by (induct x y t rule: upd.induct) (auto simp: invpst_baliR invpst_baliL)

theorem rbt_update: "rbt t ⟹ rbt (update x y t)"
by (simp add: invc_upd(2) invh_upd(1) color_paint_Black invc_paint_Black
invh_paint rbt_def update_def invpst_upd)

subsubsection ‹Delete›

lemma bheight_paint_Red:
"color t = Black ⟹ bheight (paint Red t) = bheight t - 1"
by (cases t) auto

lemma invh_baldL_invc:
"⟦ invh l;  invh r;  bheight l + 1 = bheight r;  invc r ⟧
⟹ invh (baldL l a r) ∧ bheight (baldL l a r) = bheight l + 1"
by (induct l a r rule: baldL.induct)
(auto simp: invh_baliR invh_paint bheight_baliR bheight_paint_Red)

lemma invh_baldL_Black:
"⟦ invh l;  invh r;  bheight l + 1 = bheight r;  color r = Black ⟧
⟹ invh (baldL l a r) ∧ bheight (baldL l a r) = bheight r"
by (induct l a r rule: baldL.induct) (auto simp add: invh_baliR bheight_baliR)

lemma invc_baldL: "⟦invc2 l; invc r; color r = Black⟧ ⟹ invc (baldL l a r)"
by (induct l a r rule: baldL.induct) (auto simp: invc_baliR invc2I mkNode_def)

lemma invc2_baldL: "⟦ invc2 l; invc r ⟧ ⟹ invc2 (baldL l a r)"
by (induct l a r rule: baldL.induct)
(auto simp: invc_baliR paint_invc2 invc2I mkNode_def)

lemma invh_baldR_invc:
"⟦ invh l;  invh r;  bheight l = bheight r + 1;  invc l ⟧
⟹ invh (baldR l a r) ∧ bheight (baldR l a r) = bheight l"
by(induct l a r rule: baldR.induct)
(auto simp: invh_baliL bheight_baliL invh_paint bheight_paint_Red)

lemma invc_baldR: "⟦invc a; invc2 b; color a = Black⟧ ⟹ invc (baldR a x b)"
by (induct a x b rule: baldR.induct) (simp_all add: invc_baliL mkNode_def)

lemma invc2_baldR: "⟦ invc l; invc2 r ⟧ ⟹invc2 (baldR l x r)"
by (induct l x r rule: baldR.induct)
(auto simp: invc_baliL paint_invc2 invc2I mkNode_def)

lemma invh_combine:
"⟦ invh l; invh r; bheight l = bheight r ⟧
⟹ invh (combine l r) ∧ bheight (combine l r) = bheight l"
by (induct l r rule: combine.induct)
(auto simp: invh_baldL_Black split: tree.splits tcolor.splits)

lemma invc_combine:
assumes "invc l" "invc r"
shows "color l = Black ⟹ color r = Black ⟹ invc (combine l r)"
"invc2 (combine l r)"
using assms
by (induct l r rule: combine.induct)
(auto simp: invc_baldL invc2I mkNode_def split: tree.splits tcolor.splits)

lemma neq_LeafD: "t ≠ Leaf ⟹ ∃l x c r. t = Node l (x,c) r"
by(cases t) auto

lemma del_invc_invh: "invh t ⟹ invc t ⟹ invh (del x t) ∧
(color t = Red ∧ bheight (del x t) = bheight t ∧ invc (del x t) ∨
color t = Black ∧ bheight (del x t) = bheight t - 1 ∧ invc2 (del x t))"
proof (induct x t rule: del.induct)
case (2 x _ y _ c)
have "x = y ∨ x < y ∨ x > y" by auto
thus ?case proof (elim disjE)
assume "x = y"
with 2 show ?thesis
by (cases c) (simp_all add: invh_combine invc_combine)
next
assume "x < y"
with 2 show ?thesis
by(cases c)
(auto
simp: invh_baldL_invc invc_baldL invc2_baldL mkNode_def
dest: neq_LeafD)
next
assume "y < x"
with 2 show ?thesis
by(cases c)
(auto
simp: invh_baldR_invc invc_baldR invc2_baldR mkNode_def
dest: neq_LeafD)
qed
qed auto

lemma invpst_baldR: "invpst l ⟹ invpst r ⟹ invpst (baldR l a r)"
by (cases "(l,a,r)" rule: baldR.cases) (auto simp: invpst_baliL)

lemma invpst_baldL: "invpst l ⟹ invpst r ⟹ invpst (baldL l a r)"
by (cases "(l,a,r)" rule: baldL.cases) (auto simp: invpst_baliR)

lemma invpst_combine: "invpst l ⟹ invpst r ⟹ invpst (combine l r)"
by(induction l r rule: combine.induct)
(auto split: tree.splits tcolor.splits simp: invpst_baldR invpst_baldL)

lemma invpst_del: "invpst t ⟹ invpst (del x t)"
by(induct x t rule: del.induct)
(auto simp: invpst_baldR invpst_baldL invpst_combine)

theorem rbt_delete: "rbt t ⟹ rbt (delete k t)"
apply (clarsimp simp: delete_def rbt_def)
apply (frule (1) del_invc_invh[where x=k])
apply (auto simp: invc_paint_Black invh_paint color_paint_Black invpst_del)
done

lemma rbt_getmin_ismin:
"rbt t ⟹ t≠Leaf ⟹ is_min2 (pst_getmin t) (set_tree t)"
unfolding rbt_def by (simp add: pst_getmin_ismin)

definition "rbt_is_empty t ≡ t = Leaf"

lemma rbt_is_empty: "rbt_is_empty t ⟷ inorder t = []"
by (cases t) (auto simp: rbt_is_empty_def)

definition empty where "empty = Leaf"

subsection ‹Overall Correctness›

interpretation PM: PrioMap_by_Ordered
where empty = empty and lookup = lookup and update = update and delete = delete
and inorder = inorder and inv = "rbt" and is_empty = rbt_is_empty
and getmin = pst_getmin
apply standard
apply (auto simp: lookup_map_of inorder_update inorder_delete rbt_update
rbt_delete rbt_Leaf rbt_is_empty empty_def
dest: rbt_getmin_ismin)
done

end
`