# HG changeset patch
# User nipkow
# Date 1566226164 -7200
# Node ID e72daea2aab6b35e2ed9a848bbe70f4323f1440e
# Parent  d94456876f2d3d5900588d241f1be39642eebb5b
tuned names

diff -r d94456876f2d -r e72daea2aab6 src/HOL/Data_Structures/AVL_Set.thy
--- 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:
diff -r d94456876f2d -r e72daea2aab6 src/HOL/Data_Structures/RBT.thy
--- 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" |
diff -r d94456876f2d -r e72daea2aab6 src/HOL/Data_Structures/RBT_Set.thy
--- 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>