--- a/src/HOL/Data_Structures/RBT.thy Fri Jan 27 22:27:03 2017 +0100
+++ b/src/HOL/Data_Structures/RBT.thy Sat Jan 28 15:12:19 2017 +0100
@@ -13,35 +13,31 @@
abbreviation R where "R l a r \<equiv> Node Red l a r"
abbreviation B where "B l a r \<equiv> Node Black l a r"
-fun bal :: "'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
-"bal (R (R t1 a1 t2) a2 t3) a3 t4 = R (B t1 a1 t2) a2 (B t3 a3 t4)" |
-"bal (R t1 a1 (R t2 a2 t3)) a3 t4 = R (B t1 a1 t2) a2 (B t3 a3 t4)" |
-"bal t1 a1 (R (R t2 a2 t3) a3 t4) = R (B t1 a1 t2) a2 (B t3 a3 t4)" |
-"bal t1 a1 (R t2 a2 (R t3 a3 t4)) = R (B t1 a1 t2) a2 (B t3 a3 t4)" |
-"bal t1 a t2 = B t1 a t2"
-(* Warning: takes 30 secs to compile (2017) *)
-text\<open>Markus Reiter and Alexander Krauss added a first line not found in Okasaki:
-@{prop "bal (R t1 a1 t2) a2 (R t3 a3 t4) = R (B t1 a1 t2) a2 (B t3 a3 t4)"}
-The motivation is unclear. However: it speeds up pattern compilation
-and lemma \<open>invc_bal\<close> below can be simplified to
- @{prop "\<lbrakk>invc_sons l; invc_sons r\<rbrakk> \<Longrightarrow> invc (bal l a r)"}
-All other proofs are unaffected.\<close>
+fun baliL :: "'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
+"baliL (R (R t1 a1 t2) a2 t3) a3 t4 = R (B t1 a1 t2) a2 (B t3 a3 t4)" |
+"baliL (R t1 a1 (R t2 a2 t3)) a3 t4 = R (B t1 a1 t2) a2 (B t3 a3 t4)" |
+"baliL t1 a t2 = B t1 a t2"
+
+fun baliR :: "'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
+"baliR t1 a1 (R (R t2 a2 t3) a3 t4) = R (B t1 a1 t2) a2 (B t3 a3 t4)" |
+"baliR t1 a1 (R t2 a2 (R t3 a3 t4)) = R (B t1 a1 t2) a2 (B t3 a3 t4)" |
+"baliR t1 a t2 = B t1 a t2"
fun paint :: "color \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
"paint c Leaf = Leaf" |
"paint c (Node _ l a r) = Node c l a r"
-fun balL :: "'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
-"balL (R t1 x t2) y t3 = R (B t1 x t2) y t3" |
-"balL bl x (B t1 y t2) = bal bl x (R t1 y t2)" |
-"balL bl x (R (B t1 y t2) z t3) = R (B bl x t1) y (bal t2 z (paint Red t3))" |
-"balL t1 x t2 = R t1 x t2"
+fun baldL :: "'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
+"baldL (R t1 x t2) y t3 = R (B t1 x t2) y t3" |
+"baldL bl x (B t1 y t2) = baliR bl x (R t1 y t2)" |
+"baldL bl x (R (B t1 y t2) z t3) = R (B bl x t1) y (baliR t2 z (paint Red t3))" |
+"baldL t1 x t2 = R t1 x t2"
-fun balR :: "'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
-"balR t1 x (R t2 y t3) = R t1 x (B t2 y t3)" |
-"balR (B t1 x t2) y t3 = bal (R t1 x t2) y t3" |
-"balR (R t1 x (B t2 y t3)) z t4 = R (bal (paint Red t1) x t2) y (B t3 z t4)" |
-"balR t1 x t2 = R t1 x t2"
+fun baldR :: "'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
+"baldR t1 x (R t2 y t3) = R t1 x (B t2 y t3)" |
+"baldR (B t1 x t2) y t3 = baliL (R t1 x t2) y t3" |
+"baldR (R t1 x (B t2 y t3)) z t4 = R (baliL (paint Red t1) x t2) y (B t3 z t4)" |
+"baldR t1 x t2 = R t1 x t2"
fun combine :: "'a rbt \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
"combine Leaf t = t" |
@@ -53,7 +49,7 @@
"combine (B t1 a t2) (B t3 c t4) =
(case combine t2 t3 of
R t2' b t3' \<Rightarrow> R (B t1 a t2') b (B t3' c t4) |
- t23 \<Rightarrow> balL t1 a (B t23 c t4))" |
+ t23 \<Rightarrow> baldL t1 a (B t23 c t4))" |
"combine t1 (R t2 a t3) = R (combine t1 t2) a t3" |
"combine (R t1 a t2) t3 = R t1 a (combine t2 t3)"
--- a/src/HOL/Data_Structures/RBT_Map.thy Fri Jan 27 22:27:03 2017 +0100
+++ b/src/HOL/Data_Structures/RBT_Map.thy Sat Jan 28 15:12:19 2017 +0100
@@ -11,8 +11,8 @@
fun upd :: "'a::linorder \<Rightarrow> 'b \<Rightarrow> ('a*'b) rbt \<Rightarrow> ('a*'b) rbt" where
"upd x y Leaf = R Leaf (x,y) Leaf" |
"upd x y (B l (a,b) r) = (case cmp x a of
- LT \<Rightarrow> bal (upd x y l) (a,b) r |
- GT \<Rightarrow> bal l (a,b) (upd x y r) |
+ LT \<Rightarrow> baliL (upd x y l) (a,b) r |
+ GT \<Rightarrow> baliR l (a,b) (upd x y r) |
EQ \<Rightarrow> B l (x,y) r)" |
"upd x y (R l (a,b) r) = (case cmp x a of
LT \<Rightarrow> R (upd x y l) (a,b) r |
@@ -31,9 +31,9 @@
LT \<Rightarrow> delL x t1 (a,b) t2 |
GT \<Rightarrow> delR x t1 (a,b) t2 |
EQ \<Rightarrow> combine t1 t2)" |
-"delL x (B t1 a t2) b t3 = balL (del x (B t1 a t2)) b t3" |
+"delL x (B t1 a t2) b t3 = baldL (del x (B t1 a t2)) b t3" |
"delL x t1 a t2 = R (del x t1) a t2" |
-"delR x t1 a (B t2 b t3) = balR t1 a (del x (B t2 b t3))" |
+"delR x t1 a (B t2 b t3) = baldR t1 a (del x (B t2 b t3))" |
"delR x t1 a t2 = R t1 a (del x t2)"
definition delete :: "'a::linorder \<Rightarrow> ('a*'b) rbt \<Rightarrow> ('a*'b) rbt" where
@@ -45,7 +45,7 @@
lemma inorder_upd:
"sorted1(inorder t) \<Longrightarrow> inorder(upd x y t) = upd_list x y (inorder t)"
by(induction x y t rule: upd.induct)
- (auto simp: upd_list_simps inorder_bal)
+ (auto simp: upd_list_simps inorder_baliL inorder_baliR)
lemma inorder_update:
"sorted1(inorder t) \<Longrightarrow> inorder(update x y t) = upd_list x y (inorder t)"
@@ -58,7 +58,7 @@
"sorted1(inorder t2) \<Longrightarrow> inorder(delR x t1 a t2) =
inorder t1 @ a # del_list x (inorder t2)"
by(induction x t1 and x t1 a t2 and x t1 a t2 rule: del_delL_delR.induct)
- (auto simp: del_list_simps inorder_combine inorder_balL inorder_balR)
+ (auto simp: del_list_simps inorder_combine inorder_baldL inorder_baldR)
lemma inorder_delete:
"sorted1(inorder t) \<Longrightarrow> inorder(delete x t) = del_list x (inorder t)"
--- a/src/HOL/Data_Structures/RBT_Set.thy Fri Jan 27 22:27:03 2017 +0100
+++ b/src/HOL/Data_Structures/RBT_Set.thy Sat Jan 28 15:12:19 2017 +0100
@@ -14,8 +14,8 @@
"ins x Leaf = R Leaf x Leaf" |
"ins x (B l a r) =
(case cmp x a of
- LT \<Rightarrow> bal (ins x l) a r |
- GT \<Rightarrow> bal l a (ins x r) |
+ LT \<Rightarrow> baliL (ins x l) a r |
+ GT \<Rightarrow> baliR l a (ins x r) |
EQ \<Rightarrow> B l a r)" |
"ins x (R l a r) =
(case cmp x a of
@@ -36,9 +36,9 @@
LT \<Rightarrow> delL x l a r |
GT \<Rightarrow> delR x l a r |
EQ \<Rightarrow> combine l r)" |
-"delL x (B t1 a t2) b t3 = balL (del x (B t1 a t2)) b t3" |
+"delL x (B t1 a t2) b t3 = baldL (del x (B t1 a t2)) b t3" |
"delL x l a r = R (del x l) a r" |
-"delR x t1 a (B t2 b t3) = balR t1 a (del x (B t2 b t3))" |
+"delR x t1 a (B t2 b t3) = baldR t1 a (del x (B t2 b t3))" |
"delR x l a r = R l a (del x r)"
definition delete :: "'a::linorder \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
@@ -50,30 +50,37 @@
lemma inorder_paint: "inorder(paint c t) = inorder t"
by(cases t) (auto)
-lemma inorder_bal:
- "inorder(bal l a r) = inorder l @ a # inorder r"
-by(cases "(l,a,r)" rule: bal.cases) (auto)
+lemma inorder_baliL:
+ "inorder(baliL l a r) = inorder l @ a # inorder r"
+by(cases "(l,a,r)" rule: baliL.cases) (auto)
+
+lemma inorder_baliR:
+ "inorder(baliR l a r) = inorder l @ a # inorder r"
+by(cases "(l,a,r)" rule: baliR.cases) (auto)
lemma inorder_ins:
"sorted(inorder t) \<Longrightarrow> inorder(ins x t) = ins_list x (inorder t)"
-by(induction x t rule: ins.induct) (auto simp: ins_list_simps inorder_bal)
+by(induction x t rule: ins.induct)
+ (auto simp: ins_list_simps inorder_baliL inorder_baliR)
lemma inorder_insert:
"sorted(inorder t) \<Longrightarrow> inorder(insert x t) = ins_list x (inorder t)"
by (simp add: insert_def inorder_ins inorder_paint)
-lemma inorder_balL:
- "inorder(balL l a r) = inorder l @ a # inorder r"
-by(cases "(l,a,r)" rule: balL.cases)(auto simp: inorder_bal inorder_paint)
+lemma inorder_baldL:
+ "inorder(baldL l a r) = inorder l @ a # inorder r"
+by(cases "(l,a,r)" rule: baldL.cases)
+ (auto simp: inorder_baliL inorder_baliR inorder_paint)
-lemma inorder_balR:
- "inorder(balR l a r) = inorder l @ a # inorder r"
-by(cases "(l,a,r)" rule: balR.cases) (auto simp: inorder_bal inorder_paint)
+lemma inorder_baldR:
+ "inorder(baldR l a r) = inorder l @ a # inorder r"
+by(cases "(l,a,r)" rule: baldR.cases)
+ (auto simp: inorder_baliL inorder_baliR inorder_paint)
lemma inorder_combine:
"inorder(combine l r) = inorder l @ inorder r"
by(induction l r rule: combine.induct)
- (auto simp: inorder_balL inorder_balR split: tree.split color.split)
+ (auto simp: inorder_baldL inorder_baldR split: tree.split color.split)
lemma inorder_del:
"sorted(inorder t) \<Longrightarrow> inorder(del x t) = del_list x (inorder t)"
@@ -82,7 +89,7 @@
"sorted(inorder r) \<Longrightarrow> inorder(delR x l a r) =
inorder l @ a # del_list x (inorder r)"
by(induction x t and x l a r and x l a r rule: del_delL_delR.induct)
- (auto simp: del_list_simps inorder_combine inorder_balL inorder_balR)
+ (auto simp: del_list_simps inorder_combine inorder_baldL inorder_baldR)
lemma inorder_delete:
"sorted(inorder t) \<Longrightarrow> inorder(delete x t) = del_list x (inorder t)"
@@ -135,17 +142,29 @@
lemma invh_paint: "invh t \<Longrightarrow> invh (paint c t)"
by (cases t) auto
-lemma invc_bal:
- "\<lbrakk>invc l \<and> invc2 r \<or> invc2 l \<and> invc r\<rbrakk> \<Longrightarrow> invc (bal l a r)"
-by (induct l a r rule: bal.induct) auto
+lemma invc_baliL:
+ "\<lbrakk>invc2 l; invc r\<rbrakk> \<Longrightarrow> invc (baliL l a r)"
+by (induct l a r rule: baliL.induct) auto
+
+lemma invc_baliR:
+ "\<lbrakk>invc l; invc2 r\<rbrakk> \<Longrightarrow> invc (baliR l a r)"
+by (induct l a r rule: baliR.induct) auto
+
+lemma bheight_baliL:
+ "bheight l = bheight r \<Longrightarrow> bheight (baliL l a r) = Suc (bheight l)"
+by (induct l a r rule: baliL.induct) auto
-lemma bheight_bal:
- "bheight l = bheight r \<Longrightarrow> bheight (bal l a r) = Suc (bheight l)"
-by (induct l a r rule: bal.induct) auto
+lemma bheight_baliR:
+ "bheight l = bheight r \<Longrightarrow> bheight (baliR l a r) = Suc (bheight l)"
+by (induct l a r rule: baliR.induct) auto
-lemma invh_bal:
- "\<lbrakk> invh l; invh r; bheight l = bheight r \<rbrakk> \<Longrightarrow> invh (bal l a r)"
-by (induct l a r rule: bal.induct) auto
+lemma invh_baliL:
+ "\<lbrakk> invh l; invh r; bheight l = bheight r \<rbrakk> \<Longrightarrow> invh (baliL l a r)"
+by (induct l a r rule: baliL.induct) auto
+
+lemma invh_baliR:
+ "\<lbrakk> invh l; invh r; bheight l = bheight r \<rbrakk> \<Longrightarrow> invh (baliR l a r)"
+by (induct l a r rule: baliR.induct) auto
subsubsection \<open>Insertion\<close>
@@ -153,12 +172,13 @@
lemma invc_ins: assumes "invc t"
shows "color t = Black \<Longrightarrow> invc (ins x t)" "invc2 (ins x t)"
using assms
-by (induct x t rule: ins.induct) (auto simp: invc_bal invc2I)
+by (induct x t rule: ins.induct) (auto simp: invc_baliL invc_baliR invc2I)
lemma invh_ins: assumes "invh t"
shows "invh (ins x t)" "bheight (ins x t) = bheight t"
using assms
-by (induct x t rule: ins.induct) (auto simp: invh_bal bheight_bal)
+by(induct x t rule: ins.induct)
+ (auto simp: invh_baliL invh_baliR bheight_baliL bheight_baliR)
theorem rbt_insert: "rbt t \<Longrightarrow> rbt (insert x t)"
by (simp add: invc_ins invh_ins color_paint_Black invc_paint_Black invh_paint
@@ -171,71 +191,72 @@
"color t = Black \<Longrightarrow> bheight (paint Red t) = bheight t - 1"
by (cases t) auto
-lemma balL_invh_with_invc:
- assumes "invh lt" "invh rt" "bheight lt + 1 = bheight rt" "invc rt"
- shows "bheight (balL lt a rt) = bheight lt + 1" "invh (balL lt a rt)"
+lemma baldL_invh_with_invc:
+ assumes "invh l" "invh r" "bheight l + 1 = bheight r" "invc r"
+ shows "bheight (baldL l a r) = bheight l + 1" "invh (baldL l a r)"
using assms
-by (induct lt a rt rule: balL.induct)
- (auto simp: invh_bal invh_paint bheight_bal bheight_paint_Red)
+by (induct l a r rule: baldL.induct)
+ (auto simp: invh_baliR invh_paint bheight_baliR bheight_paint_Red)
-lemma balL_invh_app:
- assumes "invh lt" "invh rt" "bheight lt + 1 = bheight rt" "color rt = Black"
- shows "invh (balL lt a rt)"
- "bheight (balL lt a rt) = bheight rt"
+lemma baldL_invh_app:
+ assumes "invh l" "invh r" "bheight l + 1 = bheight r" "color r = Black"
+ shows "invh (baldL l a r)"
+ "bheight (baldL l a r) = bheight r"
using assms
-by (induct lt a rt rule: balL.induct) (auto simp add: invh_bal bheight_bal)
+by (induct l a r rule: baldL.induct) (auto simp add: invh_baliR bheight_baliR)
-lemma balL_invc: "\<lbrakk>invc2 l; invc r; color r = Black\<rbrakk> \<Longrightarrow> invc (balL l a r)"
-by (induct l a r rule: balL.induct) (simp_all add: invc_bal)
+lemma baldL_invc: "\<lbrakk>invc2 l; invc r; color r = Black\<rbrakk> \<Longrightarrow> invc (baldL l a r)"
+by (induct l a r rule: baldL.induct) (simp_all add: invc_baliR)
-lemma balL_invc2: "\<lbrakk> invc2 lt; invc rt \<rbrakk> \<Longrightarrow> invc2 (balL lt a rt)"
-by (induct lt a rt rule: balL.induct) (auto simp: invc_bal paint_invc2 invc2I)
+lemma baldL_invc2: "\<lbrakk> invc2 l; invc r \<rbrakk> \<Longrightarrow> invc2 (baldL l a r)"
+by (induct l a r rule: baldL.induct) (auto simp: invc_baliR paint_invc2 invc2I)
-lemma balR_invh_with_invc:
- assumes "invh lt" "invh rt" "bheight lt = bheight rt + 1" "invc lt"
- shows "invh (balR lt a rt) \<and> bheight (balR lt a rt) = bheight lt"
+lemma baldR_invh_with_invc:
+ assumes "invh l" "invh r" "bheight l = bheight r + 1" "invc l"
+ shows "invh (baldR l a r) \<and> bheight (baldR l a r) = bheight l"
using assms
-by(induct lt a rt rule: balR.induct)
- (auto simp: invh_bal bheight_bal invh_paint bheight_paint_Red)
+by(induct l a r rule: baldR.induct)
+ (auto simp: invh_baliL bheight_baliL invh_paint bheight_paint_Red)
-lemma invc_balR: "\<lbrakk>invc a; invc2 b; color a = Black\<rbrakk> \<Longrightarrow> invc (balR a x b)"
-by (induct a x b rule: balR.induct) (simp_all add: invc_bal)
+lemma invc_baldR: "\<lbrakk>invc a; invc2 b; color a = Black\<rbrakk> \<Longrightarrow> invc (baldR a x b)"
+by (induct a x b rule: baldR.induct) (simp_all add: invc_baliL)
-lemma invc2_balR: "\<lbrakk> invc lt; invc2 rt \<rbrakk> \<Longrightarrow>invc2 (balR lt x rt)"
-by (induct lt x rt rule: balR.induct) (auto simp: invc_bal paint_invc2 invc2I)
+lemma invc2_baldR: "\<lbrakk> invc l; invc2 r \<rbrakk> \<Longrightarrow>invc2 (baldR l x r)"
+by (induct l x r rule: baldR.induct) (auto simp: invc_baliL paint_invc2 invc2I)
lemma invh_combine:
- assumes "invh lt" "invh rt" "bheight lt = bheight rt"
- shows "bheight (combine lt rt) = bheight lt" "invh (combine lt rt)"
+ assumes "invh l" "invh r" "bheight l = bheight r"
+ shows "bheight (combine l r) = bheight l" "invh (combine l r)"
using assms
-by (induct lt rt rule: combine.induct)
- (auto simp: balL_invh_app split: tree.splits color.splits)
+by (induct l r rule: combine.induct)
+ (auto simp: baldL_invh_app split: tree.splits color.splits)
lemma invc_combine:
- assumes "invc lt" "invc rt"
- shows "color lt = Black \<Longrightarrow> color rt = Black \<Longrightarrow> invc (combine lt rt)"
- "invc2 (combine lt rt)"
+ assumes "invc l" "invc r"
+ shows "color l = Black \<Longrightarrow> color r = Black \<Longrightarrow> invc (combine l r)"
+ "invc2 (combine l r)"
using assms
-by (induct lt rt rule: combine.induct)
- (auto simp: balL_invc invc2I split: tree.splits color.splits)
+by (induct l r rule: combine.induct)
+ (auto simp: baldL_invc invc2I split: tree.splits color.splits)
-lemma assumes "invh lt" "invc lt"
- shows
- del_invc_invh: "invh (del x lt) \<and> (color lt = Red \<and> bheight (del x lt) = bheight lt \<and> invc (del x lt)
- \<or> color lt = Black \<and> bheight (del x lt) = bheight lt - 1 \<and> invc2 (del x lt))"
-and "\<lbrakk>invh rt; bheight lt = bheight rt; invc rt\<rbrakk> \<Longrightarrow>
- invh (delL x lt k rt) \<and>
- bheight (delL x lt k rt) = bheight lt \<and>
- (color lt = Black \<and> color rt = Black \<and> invc (delL x lt k rt) \<or>
- (color lt \<noteq> Black \<or> color rt \<noteq> Black) \<and> invc2 (delL x lt k rt))"
- and "\<lbrakk>invh rt; bheight lt = bheight rt; invc rt\<rbrakk> \<Longrightarrow>
- invh (delR x lt k rt) \<and>
- bheight (delR x lt k rt) = bheight lt \<and>
- (color lt = Black \<and> color rt = Black \<and> invc (delR x lt k rt) \<or>
- (color lt \<noteq> Black \<or> color rt \<noteq> Black) \<and> invc2 (delR x lt k rt))"
+lemma assumes "invh l" "invc l"
+ shows del_invc_invh:
+ "invh (del x l) \<and>
+ (color l = Red \<and> bheight (del x l) = bheight l \<and> invc (del x l) \<or>
+ color l = Black \<and> bheight (del x l) = bheight l - 1 \<and> invc2 (del x l))"
+and "\<lbrakk>invh r; bheight l = bheight r; invc r\<rbrakk> \<Longrightarrow>
+ invh (delL x l k r) \<and>
+ bheight (delL x l k r) = bheight l \<and>
+ (color l = Black \<and> color r = Black \<and> invc (delL x l k r) \<or>
+ (color l \<noteq> Black \<or> color r \<noteq> Black) \<and> invc2 (delL x l k r))"
+ and "\<lbrakk>invh r; bheight l = bheight r; invc r\<rbrakk> \<Longrightarrow>
+ invh (delR x l k r) \<and>
+ bheight (delR x l k r) = bheight l \<and>
+ (color l = Black \<and> color r = Black \<and> invc (delR x l k r) \<or>
+ (color l \<noteq> Black \<or> color r \<noteq> Black) \<and> invc2 (delR x l k r))"
using assms
-proof (induct x lt and x lt k rt and x lt k rt rule: del_delL_delR.induct)
+proof (induct x l and x l k r and x l k r rule: del_delL_delR.induct)
case (2 y c _ y')
have "y = y' \<or> y < y' \<or> y > y'" by auto
thus ?case proof (elim disjE)
@@ -250,11 +271,11 @@
with 2 show ?thesis by (cases c) (auto simp: invc2I)
qed
next
- case (3 y lt z rta y' bb)
- thus ?case by (cases "color (Node Black lt z rta) = Black \<and> color bb = Black") (simp add: balL_invh_with_invc balL_invc balL_invc2)+
+ case (3 y l z ra y' bb)
+ thus ?case by (cases "color (Node Black l z ra) = Black \<and> color bb = Black") (simp add: baldL_invh_with_invc baldL_invc baldL_invc2)+
next
- case (5 y a y' lt z rta)
- thus ?case by (cases "color a = Black \<and> color (Node Black lt z rta) = Black") (simp add: balR_invh_with_invc invc_balR invc2_balR)+
+ case (5 y a y' l z ra)
+ thus ?case by (cases "color a = Black \<and> color (Node Black l z ra) = Black") (simp add: baldR_invh_with_invc invc_baldR invc2_baldR)+
next
case ("6_1" y a y') thus ?case by (cases "color a = Black \<and> color Leaf = Black") simp+
qed auto