(* Author: Tobias Nipkow *)

section ‹Alternative Deletion in Red-Black Trees›

theory RBT_Set2
imports RBT_Set
begin

text ‹This is a conceptually simpler version of deletion. Instead of the tricky ‹join›
  this version follows the standard approach of replacing the deleted element
 in function ‹del›) by the minimal element in its right subtree.›

fun split_min :: "'a rbt → 'a × 'a rbt" where
"split_min (Node l (a, _) r) =
  (if l = Leaf then (a,r)
   else let (x,l') = split_min l
        in (x, if color l = Black then baldL l' a r else R l' a r))"

fun del :: "'a::linorder → 'a rbt → 'a rbt" where
"del x Leaf = Leaf" |
"del x (Node l (a, _) r) =
  (case cmp x a of
     LT → let l' = del x l in if l ≠ Leaf ∧ color l = Black
           then baldL l' a r else R l' a r |
     GT → let r' = del x r in if r ≠ Leaf ∧ color r = Black
           then baldR l a r' else R l a r' |
     EQ → if r = Leaf then l else let (a',r') = split_min r in
           if color r = Black then baldR l a' r' else R l a' r')"

text ‹The first two ‹let›s speed up the automatic proof of ‹inv_del› below.›

definition delete :: "'a::linorder → 'a rbt → 'a rbt" where
"delete x t = paint Black (del x t)"


subsection "Functional Correctness Proofs"

declare Let_def[simp]

lemma split_minD:
  "split_min t = (x,t') ==> t ≠ Leaf ==> x # inorder t' = inorder t"
by(induction t arbitrary: t' rule: split_min.induct)
  (auto simp: inorder_baldL sorted_lems split: prod.splits if_splits)

lemma inorder_del:
 "sorted(inorder t) ==> inorder(del x t) = del_list x (inorder t)"
by(induction x t rule: del.induct)
  (auto simp: del_list_simps inorder_baldL inorder_baldR split_minD split: prod.splits)

lemma inorder_delete:
  "sorted(inorder t) ==> inorder(delete x t) = del_list x (inorder t)"
by (auto simp: delete_def inorder_del inorder_paint)


subsection ‹Structural invariants›

lemma neq_Red[simp]: "(c ≠ Red) = (c = Black)"
by (cases c) auto


subsubsection ‹Deletion›

lemma inv_split_min: "[ split_min t = (x,t'); t ≠ Leaf; invh t; invc t ] ==>
   invh t' ∧
   (color t = Red ⟶ bheight t' = bheight t ∧ invc t') ∧
   (color t = Black ⟶ bheight t' = bheight t - 1 ∧ invc2 t')"
apply(induction t arbitrary: x t' rule: split_min.induct)
apply(auto simp: inv_baldR inv_baldL invc2I dest!: neq_LeafD
           split: if_splits prod.splits)
done

text ‹An automatic proof. It is quite brittle, e.g. inlining the ‹let›s in @{const del} breaks it.›
lemma inv_del: "[ 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))"
apply(induction x t rule: del.induct)
apply(auto simp: inv_baldR inv_baldL invc2I dest!: inv_split_min dest: neq_LeafD
           split!: prod.splits if_splits)
done

text‹A structured proof where one can see what is used in each case.›
lemma inv_del2: "[ 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(induction x t rule: del.induct)
  case (1 x)
  then show ?case by simp
next
  case (2 x l a c r)
  note if_split[split del]
  show ?case
  proof cases
    assume "x < a"
    show ?thesis
    proof cases (* For readability; is automated more (below) *)
      assume "l = Leaf" thus ?thesis using ‹x < a› "2.prems" by(auto)
    next
      assume l: "l ≠ Leaf"
      show ?thesis
      proof (cases "color l")
        assume *: "color l = Black"
        hence "bheight l > 0" using l neq_LeafD[of l] by auto
        thus ?thesis using ‹x < a› "2.IH"(1) "2.prems" inv_baldL[of "del x l"] * l by(auto)
      next
        assume "color l = Red"
        thus ?thesis using ‹x < a› "2.prems" "2.IH"(1) by(auto)
      qed
    qed
  next (* more automation: *)
    assume "¬ x < a"
    show ?thesis
    proof cases
      assume "x > a"
      show ?thesis using ‹a < x› "2.IH"(2) "2.prems" neq_LeafD[of r] inv_baldR[of _ "del x r"]
          by(auto split: if_split)
    
    next
      assume "¬ x > a"
      show ?thesis using "2.prems" ‹¬ x < a› ‹¬ x > a›
          by(auto simp: inv_baldR invc2I dest!: inv_split_min dest: neq_LeafD split: prod.split if_split)
    qed
  qed
qed

theorem rbt_delete: "rbt t ==> rbt (delete x t)"
by (metis delete_def rbt_def color_paint_Black inv_del invh_paint)

text ‹Overall correctness:›

interpretation S: Set_by_Ordered
where empty = empty and isin = isin and insert = insert and delete = delete
and inorder = inorder and inv = rbt
proof (standard, goal_cases)
  case 1 show ?case by (simp add: empty_def)
next
  case 2 thus ?case by(simp add: isin_set_inorder)
next
  case 3 thus ?case by(simp add: inorder_insert)
next
  case 4 thus ?case by(simp add: inorder_delete)
next
  case 5 thus ?case by (simp add: rbt_def empty_def) 
next
  case 6 thus ?case by (simp add: rbt_insert) 
next
  case 7 thus ?case by (simp add: rbt_delete) 
qed


end