author nipkow Tue, 15 Sep 2020 08:57:47 +0200 changeset 72260 d488d643e677 parent 72259 25cf074a4188 child 72261 5193570b739a
```--- a/src/HOL/Data_Structures/Set2_Join_RBT.thy	Sun Sep 13 16:11:05 2020 +0100
+++ b/src/HOL/Data_Structures/Set2_Join_RBT.thy	Tue Sep 15 08:57:47 2020 +0200
@@ -80,10 +80,6 @@
by(auto simp: invh_baliL bheight_joinL joinL.simps[of l x r] split!: tree.split color.split)
qed

-lemma bheight_baliR:
-  "bheight l = bheight r \<Longrightarrow> bheight (baliR l a r) = Suc (bheight l)"
-by (cases "(l,a,r)" rule: baliR.cases) auto
-
lemma bheight_joinR:
"\<lbrakk> invh l;  invh r;  bheight l \<ge> bheight r \<rbrakk> \<Longrightarrow> bheight (joinR l x r) = bheight l"
proof (induct l x r rule: joinR.induct)
@@ -99,10 +95,27 @@
split!: tree.split color.split)
qed

+text \<open>All invariants in one:\<close>
+
+lemma inv_joinL: "\<lbrakk> invc l; invc r; invh l; invh r; bheight l \<le> bheight r \<rbrakk>
+ \<Longrightarrow> invc2 (joinL l x r) \<and> (bheight l \<noteq> bheight r \<and> color r = Black \<longrightarrow>  invc (joinL l x r))
+     \<and> invh (joinL l x r) \<and> bheight (joinL l x r) = bheight r"
+proof (induct l x r rule: joinL.induct)
+  case (1 l x r) thus ?case
+    by(auto simp: inv_baliL invc2I joinL.simps[of l x r] split!: tree.splits if_splits)
+qed
+
+lemma inv_joinR: "\<lbrakk> invc l; invc r; invh l; invh r; bheight l \<ge> bheight r \<rbrakk>
+ \<Longrightarrow> invc2 (joinR l x r) \<and> (bheight l \<noteq> bheight r \<and> color l = Black \<longrightarrow>  invc (joinR l x r))
+     \<and> invh (joinR l x r) \<and> bheight (joinR l x r) = bheight l"
+proof (induct l x r rule: joinR.induct)
+  case (1 l x r) thus ?case
+    by(auto simp: inv_baliR invc2I joinR.simps[of l x r] split!: tree.splits if_splits)
+qed
+
(* unused *)
lemma rbt_join: "\<lbrakk> invc l; invh l; invc r; invh r \<rbrakk> \<Longrightarrow> rbt(join l x r)"
-by(simp add: invc2_joinL invc2_joinR invh_joinL invh_joinR invh_paint rbt_def
-    color_paint_Black join_def)
+by(simp add: inv_joinL inv_joinR invh_paint rbt_def color_paint_Black join_def)

text \<open>To make sure the the black height is not increased unnecessarily:\<close>
```