--- a/src/HOL/Data_Structures/AVL_Set.thy Sat Aug 17 19:04:03 2019 +0200
+++ b/src/HOL/Data_Structures/AVL_Set.thy Mon Aug 19 16:49:24 2019 +0200
@@ -133,7 +133,7 @@
declare Let_def [simp]
-lemma [simp]: "avl t \<Longrightarrow> ht t = height t"
+lemma ht_height[simp]: "avl t \<Longrightarrow> ht t = height t"
by (induct t) simp_all
lemma height_balL:
@@ -148,7 +148,7 @@
height (balR l a r) = height l + 3"
by (cases r) (auto simp add:node_def balR_def split:tree.split)
-lemma [simp]: "height(node l a r) = max (height l) (height r) + 1"
+lemma height_node[simp]: "height(node l a r) = max (height l) (height r) + 1"
by (simp add: node_def)
lemma avl_node:
--- a/src/HOL/Data_Structures/RBT.thy Sat Aug 17 19:04:03 2019 +0200
+++ b/src/HOL/Data_Structures/RBT.thy Mon Aug 19 16:49:24 2019 +0200
@@ -14,13 +14,13 @@
abbreviation B where "B l a r \<equiv> Node l a Black r"
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 (R (R t1 a t2) b t3) c t4 = R (B t1 a t2) b (B t3 c t4)" |
+"baliL (R t1 a (R t2 b t3)) c t4 = R (B t1 a t2) b (B t3 c 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 t2 a2 (R t3 a3 t4)) = R (B t1 a1 t2) a2 (B t3 a3 t4)" |
-"baliR t1 a1 (R (R t2 a2 t3) a3 t4) = R (B t1 a1 t2) a2 (B t3 a3 t4)" |
+"baliR t1 a (R t2 b (R t3 c t4)) = R (B t1 a t2) b (B t3 c t4)" |
+"baliR t1 a (R (R t2 b t3) c t4) = R (B t1 a t2) b (B t3 c t4)" |
"baliR t1 a t2 = B t1 a t2"
fun paint :: "color \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
@@ -28,16 +28,16 @@
"paint c (Node l a _ r) = Node l a c r"
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"
+"baldL (R t1 a t2) b t3 = R (B t1 a t2) b t3" |
+"baldL bl a (B t1 b t2) = baliR bl a (R t1 b t2)" |
+"baldL bl a (R (B t1 b t2) c t3) = R (B bl a t1) b (baliR t2 c (paint Red t3))" |
+"baldL t1 a t2 = R t1 a 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"
+"baldR t1 a (R t2 b t3) = R t1 a (B t2 b t3)" |
+"baldR (B t1 a t2) b t3 = baliL (R t1 a t2) b t3" |
+"baldR (R t1 a (B t2 b t3)) c t4 = R (baliL (paint Red t1) a t2) b (B t3 c t4)" |
+"baldR t1 a t2 = R t1 a t2"
fun combine :: "'a rbt \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
"combine Leaf t = t" |
--- a/src/HOL/Data_Structures/RBT_Set.thy Sat Aug 17 19:04:03 2019 +0200
+++ b/src/HOL/Data_Structures/RBT_Set.thy Mon Aug 19 16:49:24 2019 +0200
@@ -205,11 +205,11 @@
by(induct l a r rule: baldR.induct)
(auto simp: invh_baliL bheight_baliL invh_paint bheight_paint_Red)
-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 invc_baldR: "\<lbrakk>invc l; invc2 r; color l = Black\<rbrakk> \<Longrightarrow> invc (baldR l a r)"
+by (induct l a r rule: baldR.induct) (simp_all add: invc_baliL)
-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 invc2_baldR: "\<lbrakk> invc l; invc2 r \<rbrakk> \<Longrightarrow>invc2 (baldR l a r)"
+by (induct l a r rule: baldR.induct) (auto simp: invc_baliL paint_invc2 invc2I)
lemma invh_combine:
"\<lbrakk> invh l; invh r; bheight l = bheight r \<rbrakk>
@@ -251,7 +251,7 @@
qed
qed auto
-theorem rbt_delete: "rbt t \<Longrightarrow> rbt (delete k t)"
+theorem rbt_delete: "rbt t \<Longrightarrow> rbt (delete x t)"
by (metis delete_def rbt_def color_paint_Black del_invc_invh invc_paint_Black invc2I invh_paint)
text \<open>Overall correctness:\<close>