theory RedBlackTree_Insert
imports RedBlackTree
begin

consts
  insert :: "nat \<Rightarrow> rbt \<Rightarrow> rbt"
  ins :: "nat \<Rightarrow> rbt \<Rightarrow> rbt"
  make_black :: "rbt \<Rightarrow> rbt"
  balance :: "rbt \<Rightarrow> rbt" 

recdef balance "{}"
  "balance (Tr B (Tr R (Tr R a x b) y c) z d) = (Tr R (Tr B a x b) y (Tr B c z d))" 
  "balance (Tr B (Tr R a x (Tr R b y c)) z d) = (Tr R (Tr B a x b) y (Tr B c z d))"
  "balance (Tr B a x (Tr R (Tr R b y c) z d)) = (Tr R (Tr B a x b) y (Tr B c z d))" 
  "balance (Tr B a x (Tr R b y (Tr R c z d))) = (Tr R (Tr B a x b) y (Tr B c z d))" 
  "balance t = t"

primrec
  "ins x E = Tr R E x E"
  "ins x (Tr c l n r) = (if x < n then balance (Tr c (ins x l) n r)
    else if x > n then balance (Tr c l n (ins x r)) else (Tr c l n r) )"

primrec
  "make_black E = E"
  "make_black (Tr c l n r) = Tr B l n r"

primrec
  "insert x E = make_black (ins x E)"
  "insert x (Tr c l n r) = make_black (ins x (Tr c l n r))"

lemma "isrbt t \<Longrightarrow> inv2 (insert x t)"
  oops

lemma assumes balanced_rbt: "isrbt t"
      shows "isrbt(insert x t)"
  oops
 
end