Theory RBT_Comparator_Impl

subsection ‹A Comparator-Interface to Red-Black-Trees›

theory RBT_Comparator_Impl
imports 
  "HOL-Library.RBT_Impl"
  Comparator
begin

text ‹For all of the main algorithms of red-black trees, we
  provide alternatives which are completely based on comparators,
  and which are provable equivalent. At the time of writing,
  this interface is used in the Container AFP-entry.
  
  It does not rely on the modifications of code-equations as in 
  the previous subsection.›

context 
  fixes c :: "'a comparator"
begin

primrec rbt_comp_lookup :: "('a, 'b) rbt ⇒ 'a ⇀ 'b"
where
  "rbt_comp_lookup RBT_Impl.Empty k = None"
| "rbt_comp_lookup (Branch _ l x y r) k = 
   (case c k x of Lt ⇒ rbt_comp_lookup l k 
     | Gt ⇒ rbt_comp_lookup r k 
     | Eq ⇒ Some y)"

fun
  rbt_comp_ins :: "('a ⇒ 'b ⇒ 'b ⇒ 'b) ⇒ 'a ⇒ 'b ⇒ ('a,'b) rbt ⇒ ('a,'b) rbt"
where
  "rbt_comp_ins f k v RBT_Impl.Empty = Branch RBT_Impl.R RBT_Impl.Empty k v  RBT_Impl.Empty" |
  "rbt_comp_ins f k v (Branch RBT_Impl.B l x y r) = (case c k x of 
      Lt ⇒ balance (rbt_comp_ins f k v l) x y r
    | Gt ⇒ balance l x y (rbt_comp_ins f k v r)
    | Eq ⇒ Branch RBT_Impl.B l x (f k y v) r)" |
  "rbt_comp_ins f k v (Branch RBT_Impl.R l x y r) = (case c k x of 
      Lt ⇒ Branch RBT_Impl.R (rbt_comp_ins f k v l) x y r
    | Gt ⇒ Branch RBT_Impl.R l x y (rbt_comp_ins f k v r)
    | Eq ⇒ Branch RBT_Impl.R l x (f k y v) r)"

definition rbt_comp_insert_with_key :: "('a ⇒ 'b ⇒ 'b ⇒ 'b) ⇒ 'a ⇒ 'b ⇒ ('a,'b) rbt ⇒ ('a,'b) rbt"
where "rbt_comp_insert_with_key f k v t = paint RBT_Impl.B (rbt_comp_ins f k v t)"

definition rbt_comp_insert :: "'a ⇒ 'b ⇒ ('a, 'b) rbt ⇒ ('a, 'b) rbt" where
  "rbt_comp_insert = rbt_comp_insert_with_key (λ_ _ nv. nv)"

fun
  rbt_comp_del_from_left :: "'a ⇒ ('a,'b) rbt ⇒ 'a ⇒ 'b ⇒ ('a,'b) rbt ⇒ ('a,'b) rbt" and
  rbt_comp_del_from_right :: "'a ⇒ ('a,'b) rbt ⇒ 'a ⇒ 'b ⇒ ('a,'b) rbt ⇒ ('a,'b) rbt" and
  rbt_comp_del :: "'a⇒ ('a,'b) rbt ⇒ ('a,'b) rbt"
where
  "rbt_comp_del x RBT_Impl.Empty = RBT_Impl.Empty" |
  "rbt_comp_del x (Branch _ a y s b) = 
   (case c x y of 
        Lt ⇒ rbt_comp_del_from_left x a y s b 
      | Gt ⇒ rbt_comp_del_from_right x a y s b
      | Eq ⇒ combine a b)" |
  "rbt_comp_del_from_left x (Branch RBT_Impl.B lt z v rt) y s b = balance_left (rbt_comp_del x (Branch RBT_Impl.B lt z v rt)) y s b" |
  "rbt_comp_del_from_left x a y s b = Branch RBT_Impl.R (rbt_comp_del x a) y s b" |
  "rbt_comp_del_from_right x a y s (Branch RBT_Impl.B lt z v rt) = balance_right a y s (rbt_comp_del x (Branch RBT_Impl.B lt z v rt))" | 
  "rbt_comp_del_from_right x a y s b = Branch RBT_Impl.R a y s (rbt_comp_del x b)"

definition "rbt_comp_delete k t = paint RBT_Impl.B (rbt_comp_del k t)"

definition "rbt_comp_bulkload xs = foldr (λ(k, v). rbt_comp_insert k v) xs RBT_Impl.Empty"

primrec
  rbt_comp_map_entry :: "'a ⇒ ('b ⇒ 'b) ⇒ ('a, 'b) rbt ⇒ ('a, 'b) rbt"
where
  "rbt_comp_map_entry k f RBT_Impl.Empty = RBT_Impl.Empty"
| "rbt_comp_map_entry k f (Branch cc lt x v rt) =
    (case c k x of 
        Lt ⇒ Branch cc (rbt_comp_map_entry k f lt) x v rt
      | Gt ⇒ Branch cc lt x v (rbt_comp_map_entry k f rt)
      | Eq ⇒ Branch cc lt x (f v) rt)"

function comp_sunion_with :: "('a ⇒ 'b ⇒ 'b ⇒ 'b) ⇒ ('a × 'b) list ⇒ ('a × 'b) list ⇒ ('a × 'b) list" 
where
  "comp_sunion_with f ((k, v) # as) ((k', v') # bs) =
   (case c k' k of 
        Lt ⇒ (k', v') # comp_sunion_with f ((k, v) # as) bs
      | Gt ⇒ (k, v) # comp_sunion_with f as ((k', v') # bs)
      | Eq ⇒ (k, f k v v') # comp_sunion_with f as bs)"
| "comp_sunion_with f [] bs = bs"
| "comp_sunion_with f as [] = as"
by pat_completeness auto
termination by lexicographic_order

function comp_sinter_with :: "('a ⇒ 'b ⇒ 'b ⇒ 'b) ⇒ ('a × 'b) list ⇒ ('a × 'b) list ⇒ ('a × 'b) list"
where
  "comp_sinter_with f ((k, v) # as) ((k', v') # bs) =
  (case c k' k of 
      Lt ⇒ comp_sinter_with f ((k, v) # as) bs
    | Gt ⇒ comp_sinter_with f as ((k', v') # bs)
    | Eq ⇒ (k, f k v v') # comp_sinter_with f as bs)"
| "comp_sinter_with f [] _ = []"
| "comp_sinter_with f _ [] = []"
by pat_completeness auto
termination by lexicographic_order

fun rbt_split_comp :: "('a, 'b) rbt ⇒ 'a ⇒ ('a, 'b) rbt × 'b option × ('a, 'b) rbt" where
  "rbt_split_comp RBT_Impl.Empty k = (RBT_Impl.Empty, None, RBT_Impl.Empty)"
| "rbt_split_comp (RBT_Impl.Branch _ l a b r) x = (case c x a of
    Lt ⇒ (case rbt_split_comp l x of (l1, β, l2) ⇒ (l1, β, rbt_join l2 a b r))
  | Gt ⇒ (case rbt_split_comp r x of (r1, β, r2) ⇒ (rbt_join l a b r1, β, r2))
  | Eq ⇒ (l, Some b, r))"

lemma rbt_split_comp_size: "(l2, b, r2) = rbt_split_comp t2 a ⟹ size l2 + size r2 ≤ size t2"
  by (induction t2 a arbitrary: l2 b r2 rule: rbt_split_comp.induct)
     (auto split: order.splits if_splits prod.splits)

function rbt_comp_union_rec :: "('a ⇒ 'b ⇒ 'b ⇒ 'b) ⇒ ('a, 'b) rbt ⇒ ('a, 'b) rbt ⇒ ('a, 'b) rbt" where
  "rbt_comp_union_rec f t1 t2 = (let (f, t2, t1) =
    if flip_rbt t2 t1 then (λk v v'. f k v' v, t1, t2) else (f, t2, t1) in
    if small_rbt t2 then RBT_Impl.fold (rbt_comp_insert_with_key f) t2 t1
    else (case t1 of RBT_Impl.Empty ⇒ t2
      | RBT_Impl.Branch _ l1 a b r1 ⇒
        case rbt_split_comp t2 a of (l2, β, r2) ⇒
          rbt_join (rbt_comp_union_rec f l1 l2) a (case β of None ⇒ b | Some b' ⇒ f a b b') (rbt_comp_union_rec f r1 r2)))"
  by pat_completeness auto
termination
  using rbt_split_comp_size
  by (relation "measure (λ(f,t1,t2). size t1 + size t2)") (fastforce split: if_splits)+

declare rbt_comp_union_rec.simps[simp del]

function rbt_comp_union_swap_rec :: "('a ⇒ 'b ⇒ 'b ⇒ 'b) ⇒ bool ⇒ ('a, 'b) rbt ⇒ ('a, 'b) rbt ⇒ ('a, 'b) rbt" where
  "rbt_comp_union_swap_rec f γ t1 t2 = (let (γ, t2, t1) =
    if flip_rbt t2 t1 then (¬γ, t1, t2) else (γ, t2, t1);
    f' = (if γ then (λk v v'. f k v' v) else f) in
    if small_rbt t2 then RBT_Impl.fold (rbt_comp_insert_with_key f') t2 t1
    else case t1 of rbt.Empty ⇒ t2
      | Branch x l1 a b r1 ⇒
        case rbt_split_comp t2 a of (l2, β, r2) ⇒
          rbt_join (rbt_comp_union_swap_rec f γ l1 l2) a (case β of None ⇒ b | Some x ⇒ f' a b x) (rbt_comp_union_swap_rec f γ r1 r2))"
  by pat_completeness auto
termination
  using rbt_split_comp_size
  by (relation "measure (λ(f,γ,t1, t2). size t1 + size t2)") (fastforce split: if_splits)+

declare rbt_comp_union_swap_rec.simps[simp del]

lemma rbt_comp_union_swap_rec: "rbt_comp_union_swap_rec f γ t1 t2 =
  rbt_comp_union_rec (if γ then (λk v v'. f k v' v) else f) t1 t2"
proof (induction f γ t1 t2 rule: rbt_comp_union_swap_rec.induct)
  case (1 f γ t1 t2)
  show ?case
    using 1[OF refl _ refl refl _ refl _ refl]
    unfolding rbt_comp_union_swap_rec.simps[of _ _ t1] rbt_comp_union_rec.simps[of _ t1]
    by (auto simp: Let_def split: rbt.splits prod.splits option.splits) (* slow *)
qed

lemma rbt_comp_union_swap_rec_code[code]: "rbt_comp_union_swap_rec f γ t1 t2 = (
    let bh1 = bheight t1; bh2 = bheight t2; (γ, t2, bh2, t1, bh1) =
    if bh1 < bh2 then (¬γ, t1, bh1, t2, bh2) else (γ, t2, bh2, t1, bh1);
    f' = (if γ then (λk v v'. f k v' v) else f) in
    if bh2 < 4 then RBT_Impl.fold (rbt_comp_insert_with_key f') t2 t1
    else case t1 of rbt.Empty ⇒ t2
      | Branch x l1 a b r1 ⇒
        case rbt_split_comp t2 a of (l2, β, r2) ⇒
          rbt_join (rbt_comp_union_swap_rec f γ l1 l2) a (case β of None ⇒ b | Some x ⇒ f' a b x) (rbt_comp_union_swap_rec f γ r1 r2))"
  by (auto simp: rbt_comp_union_swap_rec.simps flip_rbt_def small_rbt_def)

definition "rbt_comp_union_with_key f t1 t2 = paint RBT_Impl.B (rbt_comp_union_swap_rec f False t1 t2)"

definition "map_filter_comp_inter f t1 t2 = List.map_filter (λ(k, v).
  case rbt_comp_lookup t1 k of None ⇒ None
  | Some v' ⇒ Some (k, f k v' v)) (RBT_Impl.entries t2)"

function rbt_comp_inter_rec :: "('a ⇒ 'b ⇒ 'b ⇒ 'b) ⇒ ('a, 'b) rbt ⇒ ('a, 'b) rbt ⇒ ('a, 'b) rbt" where
  "rbt_comp_inter_rec f t1 t2 = (let (f, t2, t1) =
    if flip_rbt t2 t1 then (λk v v'. f k v' v, t1, t2) else (f, t2, t1) in
    if small_rbt t2 then rbtreeify (map_filter_comp_inter f t1 t2)
    else case t1 of RBT_Impl.Empty ⇒ RBT_Impl.Empty
    | RBT_Impl.Branch _ l1 a b r1 ⇒
      case rbt_split_comp t2 a of (l2, β, r2) ⇒ let l' = rbt_comp_inter_rec f l1 l2; r' = rbt_comp_inter_rec f r1 r2 in
      (case β of None ⇒ rbt_join2 l' r' | Some b' ⇒ rbt_join l' a (f a b b') r'))"
  by pat_completeness auto
termination
  using rbt_split_comp_size
  by (relation "measure (λ(f,t1,t2). size t1 + size t2)") (fastforce split: if_splits)+

declare rbt_comp_inter_rec.simps[simp del]

function rbt_comp_inter_swap_rec :: "('a ⇒ 'b ⇒ 'b ⇒ 'b) ⇒ bool ⇒ ('a, 'b) rbt ⇒ ('a, 'b) rbt ⇒ ('a, 'b) rbt" where
  "rbt_comp_inter_swap_rec f γ t1 t2 = (let (γ, t2, t1) =
    if flip_rbt t2 t1 then (¬γ, t1, t2) else (γ, t2, t1);
    f' = if γ then (λk v v'. f k v' v) else f in
    if small_rbt t2 then rbtreeify (map_filter_comp_inter f' t1 t2)
    else case t1 of rbt.Empty ⇒ rbt.Empty
    | Branch x l1 a b r1 ⇒
      (case rbt_split_comp t2 a of (l2, β, r2) ⇒ let l' = rbt_comp_inter_swap_rec f γ l1 l2; r' = rbt_comp_inter_swap_rec f γ r1 r2 in
      (case β of None ⇒ rbt_join2 l' r' | Some b' ⇒ rbt_join l' a (f' a b b') r')))"
  by pat_completeness auto
termination
  using rbt_split_comp_size
  by (relation "measure (λ(f,γ,t1,t2). size t1 + size t2)") (fastforce split: if_splits)+

declare rbt_comp_inter_swap_rec.simps[simp del]

lemma rbt_comp_inter_swap_rec: "rbt_comp_inter_swap_rec f γ t1 t2 =
  rbt_comp_inter_rec (if γ then (λk v v'. f k v' v) else f) t1 t2"
proof (induction f γ t1 t2 rule: rbt_comp_inter_swap_rec.induct)
  case (1 f γ t1 t2)
  show ?case
    using 1[OF refl _ refl refl _ refl _ refl]
    unfolding rbt_comp_inter_swap_rec.simps[of _ _ t1] rbt_comp_inter_rec.simps[of _ t1]
    by (auto simp: Let_def split: rbt.splits prod.splits option.splits)
qed

lemma comp_inter_with_key_code[code]: "rbt_comp_inter_swap_rec f γ t1 t2 = (
  let bh1 = bheight t1; bh2 = bheight t2; (γ, t2, bh2, t1, bh1) =
  if bh1 < bh2 then (¬γ, t1, bh1, t2, bh2) else (γ, t2, bh2, t1, bh1);
  f' = (if γ then (λk v v'. f k v' v) else f) in
  if bh2 < 4 then rbtreeify (map_filter_comp_inter f' t1 t2)
  else case t1 of rbt.Empty ⇒ rbt.Empty
    | Branch x l1 a b r1 ⇒
      (case rbt_split_comp t2 a of (l2, β, r2) ⇒ let l' = rbt_comp_inter_swap_rec f γ l1 l2; r' = rbt_comp_inter_swap_rec f γ r1 r2 in
      (case β of None ⇒ rbt_join2 l' r' | Some b' ⇒ rbt_join l' a (f' a b b') r')))"
  by (auto simp: rbt_comp_inter_swap_rec.simps flip_rbt_def small_rbt_def)

definition "rbt_comp_inter_with_key f t1 t2 = paint RBT_Impl.B (rbt_comp_inter_swap_rec f False t1 t2)"

definition "filter_comp_minus t1 t2 =
  filter (λ(k, _). rbt_comp_lookup t2 k = None) (RBT_Impl.entries t1)"

fun comp_minus :: "('a, 'b) rbt ⇒ ('a, 'b) rbt ⇒ ('a, 'b) rbt" where
  "comp_minus t1 t2 = (if small_rbt t2 then RBT_Impl.fold (λk _ t. rbt_comp_delete k t) t2 t1
    else if small_rbt t1 then rbtreeify (filter_comp_minus t1 t2)
    else case t2 of RBT_Impl.Empty ⇒ t1
      | RBT_Impl.Branch _ l2 a b r2 ⇒
        case rbt_split_comp t1 a of (l1, _, r1) ⇒ rbt_join2 (comp_minus l1 l2) (comp_minus r1 r2))"

declare comp_minus.simps[simp del]

definition "rbt_comp_minus t1 t2 = paint RBT_Impl.B (comp_minus t1 t2)"

context
  assumes c: "comparator c"
begin

lemma rbt_comp_lookup: "rbt_comp_lookup = ord.rbt_lookup (lt_of_comp c)" 
proof (intro ext)
  fix k and t :: "('a,'b)rbt"
  show "rbt_comp_lookup t k = ord.rbt_lookup (lt_of_comp c) t k"
    by (induct t, unfold rbt_comp_lookup.simps ord.rbt_lookup.simps
      comparator.two_comparisons_into_case_order[OF c]) 
      (auto split: order.splits)
qed  

lemma rbt_comp_ins: "rbt_comp_ins = ord.rbt_ins (lt_of_comp c)" 
proof (intro ext)
  fix f k v and t :: "('a,'b)rbt"
  show "rbt_comp_ins f k v t = ord.rbt_ins (lt_of_comp c) f k v t"
    by (induct f k v t rule: rbt_comp_ins.induct, unfold rbt_comp_ins.simps ord.rbt_ins.simps
      comparator.two_comparisons_into_case_order[OF c]) 
      (auto split: order.splits)
qed  

lemma rbt_comp_insert_with_key: "rbt_comp_insert_with_key = ord.rbt_insert_with_key (lt_of_comp c)"
  unfolding rbt_comp_insert_with_key_def[abs_def] ord.rbt_insert_with_key_def[abs_def]
  unfolding rbt_comp_ins ..

lemma rbt_comp_insert: "rbt_comp_insert = ord.rbt_insert (lt_of_comp c)"
  unfolding rbt_comp_insert_def[abs_def] ord.rbt_insert_def[abs_def]
  unfolding rbt_comp_insert_with_key ..

lemma rbt_comp_del: "rbt_comp_del = ord.rbt_del (lt_of_comp c)" 
proof - {
  fix k a b and s t :: "('a,'b)rbt"
  have 
    "rbt_comp_del_from_left k t a b s = ord.rbt_del_from_left (lt_of_comp c) k t a b s"
    "rbt_comp_del_from_right k t a b s = ord.rbt_del_from_right (lt_of_comp c) k t a b s"
    "rbt_comp_del k t = ord.rbt_del (lt_of_comp c) k t"
  by (induct k t a b s and k t a b s and k t rule: rbt_comp_del_from_left_rbt_comp_del_from_right_rbt_comp_del.induct,
    unfold 
      rbt_comp_del.simps ord.rbt_del.simps
      rbt_comp_del_from_left.simps ord.rbt_del_from_left.simps
      rbt_comp_del_from_right.simps ord.rbt_del_from_right.simps
      comparator.two_comparisons_into_case_order[OF c],
    auto split: order.split) 
  }
  thus ?thesis by (intro ext)
qed  

lemma rbt_comp_delete: "rbt_comp_delete = ord.rbt_delete (lt_of_comp c)"
  unfolding rbt_comp_delete_def[abs_def] ord.rbt_delete_def[abs_def]
  unfolding rbt_comp_del ..

lemma rbt_comp_bulkload: "rbt_comp_bulkload = ord.rbt_bulkload (lt_of_comp c)"
  unfolding rbt_comp_bulkload_def[abs_def] ord.rbt_bulkload_def[abs_def]
  unfolding rbt_comp_insert ..

lemma rbt_comp_map_entry: "rbt_comp_map_entry = ord.rbt_map_entry (lt_of_comp c)" 
proof (intro ext)
  fix f k and t :: "('a,'b)rbt"
  show "rbt_comp_map_entry f k t = ord.rbt_map_entry (lt_of_comp c) f k t"
    by (induct t, unfold rbt_comp_map_entry.simps ord.rbt_map_entry.simps
      comparator.two_comparisons_into_case_order[OF c]) 
      (auto split: order.splits)
qed  

lemma comp_sunion_with: "comp_sunion_with = ord.sunion_with (lt_of_comp c)"
proof (intro ext)
  fix f and as bs :: "('a × 'b)list"
  show "comp_sunion_with f as bs = ord.sunion_with (lt_of_comp c) f as bs"
    by (induct f as bs rule: comp_sunion_with.induct,
      unfold comp_sunion_with.simps ord.sunion_with.simps
      comparator.two_comparisons_into_case_order[OF c]) 
      (auto split: order.splits)
qed

lemma anti_sym: "lt_of_comp c a x ⟹ lt_of_comp c x a ⟹ False"
  by (metis c comparator.Gt_lt_conv comparator.Lt_lt_conv order.distinct(5))

lemma rbt_split_comp: "rbt_split_comp t x = ord.rbt_split (lt_of_comp c) t x"
  by (induction t x rule: rbt_split_comp.induct)
     (auto simp: ord.rbt_split.simps comparator.le_lt_convs[OF c]
      split: order.splits prod.splits dest: anti_sym)

lemma comp_union_with_key: "rbt_comp_union_rec f t1 t2 = ord.rbt_union_rec (lt_of_comp c) f t1 t2"
proof (induction f t1 t2 rule: rbt_comp_union_rec.induct)
  case (1 f t1 t2)
  obtain f' t1' t2' where flip: "(f', t2', t1') =
    (if flip_rbt t2 t1 then (λk v v'. f k v' v, t1, t2) else (f, t2, t1))"
    by fastforce
  show ?case
  proof (cases t1')
    case (Branch _ l1 a b r1)
    have t1_not_Empty: "t1' ≠ RBT_Impl.Empty"
      by (auto simp: Branch)
    obtain l2 β r2 where split: "rbt_split_comp t2' a = (l2, β, r2)"
      by (cases "rbt_split_comp t2' a") auto
    show ?thesis
      using 1[OF flip refl _ _ Branch]
      unfolding rbt_comp_union_rec.simps[of _ t1] ord.rbt_union_rec.simps[of _ _ t1] flip[symmetric]
      by (auto simp: Branch split rbt_split_comp[symmetric] rbt_comp_insert_with_key
          split: prod.splits)
  qed (auto simp: rbt_comp_union_rec.simps[of _ t1] ord.rbt_union_rec.simps[of _ _ t1] flip[symmetric]
       rbt_comp_insert_with_key rbt_split_comp[symmetric])
qed

lemma comp_sinter_with: "comp_sinter_with = ord.sinter_with (lt_of_comp c)"
proof (intro ext)
  fix f and as bs :: "('a × 'b)list"
  show "comp_sinter_with f as bs = ord.sinter_with (lt_of_comp c) f as bs"
    by (induct f as bs rule: comp_sinter_with.induct,
      unfold comp_sinter_with.simps ord.sinter_with.simps
      comparator.two_comparisons_into_case_order[OF c]) 
      (auto split: order.splits)
qed

lemma rbt_comp_union_with_key: "rbt_comp_union_with_key = ord.rbt_union_with_key (lt_of_comp c)"
  by (rule ext)+
     (auto simp: rbt_comp_union_with_key_def rbt_comp_union_swap_rec ord.rbt_union_with_key_def
      ord.rbt_union_swap_rec comp_union_with_key)

lemma comp_inter_with_key: "rbt_comp_inter_rec f t1 t2 = ord.rbt_inter_rec (lt_of_comp c) f t1 t2"
proof (induction f t1 t2 rule: rbt_comp_inter_rec.induct)
  case (1 f t1 t2)
  obtain f' t1' t2' where flip: "(f', t2', t1') =
    (if flip_rbt t2 t1 then (λk v v'. f k v' v, t1, t2) else (f, t2, t1))"
    by fastforce
  show ?case
  proof (cases t1')
    case (Branch _ l1 a b r1)
    have t1_not_Empty: "t1' ≠ RBT_Impl.Empty"
      by (auto simp: Branch)
    obtain l2 β r2 where split: "rbt_split_comp t2' a = (l2, β, r2)"
      by (cases "rbt_split_comp t2' a") auto
    show ?thesis
      using 1[OF flip refl _ _ Branch]
      unfolding rbt_comp_inter_rec.simps[of _ t1] ord.rbt_inter_rec.simps[of _ _ t1] flip[symmetric]
      by (auto simp: Branch split rbt_split_comp[symmetric] rbt_comp_lookup
          ord.map_filter_inter_def map_filter_comp_inter_def split: prod.splits)
  qed (auto simp: rbt_comp_inter_rec.simps[of _ t1] ord.rbt_inter_rec.simps[of _ _ t1] flip[symmetric]
       ord.map_filter_inter_def map_filter_comp_inter_def rbt_comp_lookup rbt_split_comp[symmetric])
qed

lemma rbt_comp_inter_with_key: "rbt_comp_inter_with_key = ord.rbt_inter_with_key (lt_of_comp c)"
  by (rule ext)+
     (auto simp: rbt_comp_inter_with_key_def rbt_comp_inter_swap_rec
      ord.rbt_inter_with_key_def ord.rbt_inter_swap_rec comp_inter_with_key)

lemma comp_minus: "comp_minus t1 t2 = ord.rbt_minus_rec (lt_of_comp c) t1 t2"
proof (induction t1 t2 rule: comp_minus.induct)
  case (1 t1 t2)
  show ?case
  proof (cases t2)
    case (Branch _ l2 a u r2)
    have t2_not_Empty: "t2 ≠ RBT_Impl.Empty"
      by (auto simp: Branch)
    obtain l1 β r1 where split: "rbt_split_comp t1 a = (l1, β, r1)"
      by (cases "rbt_split_comp t1 a") auto
    show ?thesis
      using 1[OF _ _ Branch]
      unfolding comp_minus.simps[of t1 t2] ord.rbt_minus_rec.simps[of _ t1 t2]
      by (auto simp: Branch split rbt_split_comp[symmetric] rbt_comp_delete rbt_comp_lookup
          filter_comp_minus_def ord.filter_minus_def split: prod.splits)
  qed (auto simp: comp_minus.simps[of t1] ord.rbt_minus_rec.simps[of _ t1]
       filter_comp_minus_def ord.filter_minus_def
       rbt_comp_delete rbt_comp_lookup rbt_split_comp[symmetric])
qed

lemma rbt_comp_minus: "rbt_comp_minus = ord.rbt_minus (lt_of_comp c)"
  by (rule ext)+ (auto simp: rbt_comp_minus_def ord.rbt_minus_def comp_minus)

lemmas rbt_comp_simps = 
  rbt_comp_insert
  rbt_comp_lookup
  rbt_comp_delete
  rbt_comp_bulkload
  rbt_comp_map_entry
  rbt_comp_union_with_key
  rbt_comp_inter_with_key
  rbt_comp_minus
end
end

end