diff -r fb788bd799d9 -r cd0b0717c4e4 src/HOL/Data_Structures/RBT_Set.thy
--- a/src/HOL/Data_Structures/RBT_Set.thy	Sat Dec 28 23:44:26 2019 +0100
+++ b/src/HOL/Data_Structures/RBT_Set.thy	Tue Jan 07 06:43:09 2020 +0100
@@ -96,6 +96,9 @@
 
 subsection \<open>Structural invariants\<close>
 
+lemma neq_Black[simp]: "(c \<noteq> Black) = (c = Red)"
+by (cases c) auto
+
 text\<open>The proofs are due to Markus Reiter and Alexander Krauss.\<close>
 
 fun bheight :: "'a rbt \<Rightarrow> nat" where
@@ -176,7 +179,7 @@
 theorem rbt_insert: "rbt t \<Longrightarrow> rbt (insert x t)"
 by (simp add: invc_ins invh_ins color_paint_Black invh_paint rbt_def insert_def)
 
-text \<open>All in one variant:\<close>
+text \<open>All in one:\<close>
 
 lemma inv_ins: "\<lbrakk> invc t; invh t \<rbrakk> \<Longrightarrow>
   invc2 (ins x t) \<and> (color t = Black \<longrightarrow> invc (ins x t)) \<and>
@@ -234,34 +237,41 @@
 by (induct l r rule: combine.induct)
    (auto simp: invc_baldL invc2I split: tree.splits color.splits)
 
+text \<open>All in one:\<close>
+
+lemma inv_baldL:
+  "\<lbrakk> invh l;  invh r;  bheight l + 1 = bheight r; invc2 l; invc r \<rbrakk>
+   \<Longrightarrow> invh (baldL l a r) \<and> bheight (baldL l a r) = bheight r
+  \<and> invc2 (baldL l a r) \<and> (color r = Black \<longrightarrow> invc (baldL l a r))"
+by (induct l a r rule: baldL.induct)
+   (auto simp: inv_baliR invh_paint bheight_baliR bheight_paint_Red paint2 invc2I)
+
+lemma inv_baldR:
+  "\<lbrakk> invh l;  invh r;  bheight l = bheight r + 1; invc l; invc2 r \<rbrakk>
+   \<Longrightarrow> invh (baldR l a r) \<and> bheight (baldR l a r) = bheight l
+  \<and> invc2 (baldR l a r) \<and> (color l = Black \<longrightarrow> invc (baldR l a r))"
+by (induct l a r rule: baldR.induct)
+   (auto simp: inv_baliL invh_paint bheight_baliL bheight_paint_Red paint2 invc2I)
+
+lemma inv_combine:
+  "\<lbrakk> invh l; invh r; bheight l = bheight r; invc l; invc r \<rbrakk>
+  \<Longrightarrow> invh (combine l r) \<and> bheight (combine l r) = bheight l
+  \<and> invc2 (combine l r) \<and> (color l = Black \<and> color r = Black \<longrightarrow> invc (combine l r))"
+by (induct l r rule: combine.induct) 
+   (auto simp: invh_baldL_Black inv_baldL invc2I split: tree.splits color.splits)
+
 lemma neq_LeafD: "t \<noteq> Leaf \<Longrightarrow> \<exists>l x c r. t = Node l (x,c) r"
 by(cases t rule: tree2_cases) auto
 
-lemma del_invc_invh: "invh t \<Longrightarrow> invc t \<Longrightarrow> invh (del x t) \<and>
+lemma inv_del: "\<lbrakk> invh t; invc t \<rbrakk> \<Longrightarrow>
+   invh (del x t) \<and>
    (color t = Red \<and> bheight (del x t) = bheight t \<and> invc (del x t) \<or>
     color t = Black \<and> bheight (del x t) = bheight t - 1 \<and> invc2 (del x t))"
-proof (induct x t rule: del.induct)
-case (2 x _ y c)
-  have "x = y \<or> x < y \<or> x > y" by auto
-  thus ?case proof (elim disjE)
-    assume "x = y"
-    with 2 show ?thesis
-    by (cases c) (simp_all add: invh_combine invc_combine)
-  next
-    assume "x < y"
-    with 2 show ?thesis
-      by(cases c)
-        (auto simp: invh_baldL_invc invc_baldL invc2_baldL dest: neq_LeafD)
-  next
-    assume "y < x"
-    with 2 show ?thesis
-      by(cases c)
-        (auto simp: invh_baldR_invc invc_baldR invc2_baldR dest: neq_LeafD)
-  qed
-qed auto
+by(induct x t rule: del.induct)
+  (auto simp: inv_baldL inv_baldR inv_combine dest!: neq_LeafD)
 
 theorem rbt_delete: "rbt t \<Longrightarrow> rbt (delete x t)"
-by (metis delete_def rbt_def color_paint_Black del_invc_invh invc2I invh_paint)
+by (metis delete_def rbt_def color_paint_Black inv_del invc2I invh_paint)
 
 text \<open>Overall correctness:\<close>
 
@@ -287,9 +297,6 @@
 
 subsection \<open>Height-Size Relation\<close>
 
-lemma neq_Black[simp]: "(c \<noteq> Black) = (c = Red)"
-by (cases c) auto
-
 lemma rbt_height_bheight_if: "invc t \<Longrightarrow> invh t \<Longrightarrow>
   height t \<le> 2 * bheight t + (if color t = Black then 0 else 1)"
 by(induction t) (auto split: if_split_asm)