--- a/src/HOL/Data_Structures/AVL_Set.thy Mon Aug 19 21:31:54 2019 +0200
+++ b/src/HOL/Data_Structures/AVL_Set.thy Mon Aug 19 21:37:34 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 Mon Aug 19 21:31:54 2019 +0200
+++ b/src/HOL/Data_Structures/RBT.thy Mon Aug 19 21:37:34 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 Mon Aug 19 21:31:54 2019 +0200
+++ b/src/HOL/Data_Structures/RBT_Set.thy Mon Aug 19 21:37:34 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>
--- a/src/HOL/Data_Structures/Set2_Join.thy Mon Aug 19 21:31:54 2019 +0200
+++ b/src/HOL/Data_Structures/Set2_Join.thy Mon Aug 19 21:37:34 2019 +0200
@@ -85,9 +85,10 @@
fun split :: "('a,'b)tree \<Rightarrow> 'a \<Rightarrow> ('a,'b)tree \<times> bool \<times> ('a,'b)tree" where
"split Leaf k = (Leaf, False, Leaf)" |
"split (Node l a _ r) x =
- (if x < a then let (l1,b,l2) = split l x in (l1, b, join l2 a r) else
- if a < x then let (r1,b,r2) = split r x in (join l a r1, b, r2)
- else (l, True, r))"
+ (case cmp x a of
+ LT \<Rightarrow> let (l1,b,l2) = split l x in (l1, b, join l2 a r) |
+ GT \<Rightarrow> let (r1,b,r2) = split r x in (join l a r1, b, r2) |
+ EQ \<Rightarrow> (l, True, r))"
lemma split: "split t x = (l,xin,r) \<Longrightarrow> bst t \<Longrightarrow>
set_tree l = {a \<in> set_tree t. a < x} \<and> set_tree r = {a \<in> set_tree t. x < a}