# HG changeset patch
# User nipkow
# Date 1485612739 -3600
# Node ID 8be78855ee7adfc17edbe4dc432461a2fae0baa4
# Parent  9ca021bd718da3280a1b860fd7efbcf70b949b51
split balance into two, clearer etc

diff -r 9ca021bd718d -r 8be78855ee7a src/HOL/Data_Structures/RBT.thy
--- 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)" 
 
diff -r 9ca021bd718d -r 8be78855ee7a src/HOL/Data_Structures/RBT_Map.thy
--- 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)"
diff -r 9ca021bd718d -r 8be78855ee7a src/HOL/Data_Structures/RBT_Set.thy
--- 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