split balance into two, clearer etc
authornipkow
Sat Jan 28 15:12:19 2017 +0100 (2017-01-28)
changeset 649608be78855ee7a
parent 64959 9ca021bd718d
child 64961 d19a5579ffb8
split balance into two, clearer etc
src/HOL/Data_Structures/RBT.thy
src/HOL/Data_Structures/RBT_Map.thy
src/HOL/Data_Structures/RBT_Set.thy
     1.1 --- a/src/HOL/Data_Structures/RBT.thy	Fri Jan 27 22:27:03 2017 +0100
     1.2 +++ b/src/HOL/Data_Structures/RBT.thy	Sat Jan 28 15:12:19 2017 +0100
     1.3 @@ -13,35 +13,31 @@
     1.4  abbreviation R where "R l a r \<equiv> Node Red l a r"
     1.5  abbreviation B where "B l a r \<equiv> Node Black l a r"
     1.6  
     1.7 -fun bal :: "'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
     1.8 -"bal (R (R t1 a1 t2) a2 t3) a3 t4 = R (B t1 a1 t2) a2 (B t3 a3 t4)" |
     1.9 -"bal (R t1 a1 (R t2 a2 t3)) a3 t4 = R (B t1 a1 t2) a2 (B t3 a3 t4)" |
    1.10 -"bal t1 a1 (R (R t2 a2 t3) a3 t4) = R (B t1 a1 t2) a2 (B t3 a3 t4)" |
    1.11 -"bal t1 a1 (R t2 a2 (R t3 a3 t4)) = R (B t1 a1 t2) a2 (B t3 a3 t4)" |
    1.12 -"bal t1 a t2 = B t1 a t2"
    1.13 -(* Warning: takes 30 secs to compile (2017) *)
    1.14 -text\<open>Markus Reiter and Alexander Krauss added a first line not found in Okasaki:
    1.15 -@{prop "bal (R t1 a1 t2) a2 (R t3 a3 t4) = R (B t1 a1 t2) a2 (B t3 a3 t4)"}
    1.16 -The motivation is unclear. However: it speeds up pattern compilation
    1.17 -and lemma \<open>invc_bal\<close> below can be simplified to
    1.18 -  @{prop "\<lbrakk>invc_sons l; invc_sons r\<rbrakk> \<Longrightarrow> invc (bal l a r)"}
    1.19 -All other proofs are unaffected.\<close>
    1.20 +fun baliL :: "'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
    1.21 +"baliL (R (R t1 a1 t2) a2 t3) a3 t4 = R (B t1 a1 t2) a2 (B t3 a3 t4)" |
    1.22 +"baliL (R t1 a1 (R t2 a2 t3)) a3 t4 = R (B t1 a1 t2) a2 (B t3 a3 t4)" |
    1.23 +"baliL t1 a t2 = B t1 a t2"
    1.24 +
    1.25 +fun baliR :: "'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
    1.26 +"baliR t1 a1 (R (R t2 a2 t3) a3 t4) = R (B t1 a1 t2) a2 (B t3 a3 t4)" |
    1.27 +"baliR t1 a1 (R t2 a2 (R t3 a3 t4)) = R (B t1 a1 t2) a2 (B t3 a3 t4)" |
    1.28 +"baliR t1 a t2 = B t1 a t2"
    1.29  
    1.30  fun paint :: "color \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
    1.31  "paint c Leaf = Leaf" |
    1.32  "paint c (Node _ l a r) = Node c l a r"
    1.33  
    1.34 -fun balL :: "'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
    1.35 -"balL (R t1 x t2) y t3 = R (B t1 x t2) y t3" |
    1.36 -"balL bl x (B t1 y t2) = bal bl x (R t1 y t2)" |
    1.37 -"balL bl x (R (B t1 y t2) z t3) = R (B bl x t1) y (bal t2 z (paint Red t3))" |
    1.38 -"balL t1 x t2 = R t1 x t2"
    1.39 +fun baldL :: "'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
    1.40 +"baldL (R t1 x t2) y t3 = R (B t1 x t2) y t3" |
    1.41 +"baldL bl x (B t1 y t2) = baliR bl x (R t1 y t2)" |
    1.42 +"baldL bl x (R (B t1 y t2) z t3) = R (B bl x t1) y (baliR t2 z (paint Red t3))" |
    1.43 +"baldL t1 x t2 = R t1 x t2"
    1.44  
    1.45 -fun balR :: "'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
    1.46 -"balR t1 x (R t2 y t3) = R t1 x (B t2 y t3)" |
    1.47 -"balR (B t1 x t2) y t3 = bal (R t1 x t2) y t3" |
    1.48 -"balR (R t1 x (B t2 y t3)) z t4 = R (bal (paint Red t1) x t2) y (B t3 z t4)" |
    1.49 -"balR t1 x t2 = R t1 x t2"
    1.50 +fun baldR :: "'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
    1.51 +"baldR t1 x (R t2 y t3) = R t1 x (B t2 y t3)" |
    1.52 +"baldR (B t1 x t2) y t3 = baliL (R t1 x t2) y t3" |
    1.53 +"baldR (R t1 x (B t2 y t3)) z t4 = R (baliL (paint Red t1) x t2) y (B t3 z t4)" |
    1.54 +"baldR t1 x t2 = R t1 x t2"
    1.55  
    1.56  fun combine :: "'a rbt \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
    1.57  "combine Leaf t = t" |
    1.58 @@ -53,7 +49,7 @@
    1.59  "combine (B t1 a t2) (B t3 c t4) =
    1.60    (case combine t2 t3 of
    1.61       R t2' b t3' \<Rightarrow> R (B t1 a t2') b (B t3' c t4) |
    1.62 -     t23 \<Rightarrow> balL t1 a (B t23 c t4))" |
    1.63 +     t23 \<Rightarrow> baldL t1 a (B t23 c t4))" |
    1.64  "combine t1 (R t2 a t3) = R (combine t1 t2) a t3" |
    1.65  "combine (R t1 a t2) t3 = R t1 a (combine t2 t3)" 
    1.66  
     2.1 --- a/src/HOL/Data_Structures/RBT_Map.thy	Fri Jan 27 22:27:03 2017 +0100
     2.2 +++ b/src/HOL/Data_Structures/RBT_Map.thy	Sat Jan 28 15:12:19 2017 +0100
     2.3 @@ -11,8 +11,8 @@
     2.4  fun upd :: "'a::linorder \<Rightarrow> 'b \<Rightarrow> ('a*'b) rbt \<Rightarrow> ('a*'b) rbt" where
     2.5  "upd x y Leaf = R Leaf (x,y) Leaf" |
     2.6  "upd x y (B l (a,b) r) = (case cmp x a of
     2.7 -  LT \<Rightarrow> bal (upd x y l) (a,b) r |
     2.8 -  GT \<Rightarrow> bal l (a,b) (upd x y r) |
     2.9 +  LT \<Rightarrow> baliL (upd x y l) (a,b) r |
    2.10 +  GT \<Rightarrow> baliR l (a,b) (upd x y r) |
    2.11    EQ \<Rightarrow> B l (x,y) r)" |
    2.12  "upd x y (R l (a,b) r) = (case cmp x a of
    2.13    LT \<Rightarrow> R (upd x y l) (a,b) r |
    2.14 @@ -31,9 +31,9 @@
    2.15    LT \<Rightarrow> delL x t1 (a,b) t2 |
    2.16    GT \<Rightarrow> delR x t1 (a,b) t2 |
    2.17    EQ \<Rightarrow> combine t1 t2)" |
    2.18 -"delL x (B t1 a t2) b t3 = balL (del x (B t1 a t2)) b t3" |
    2.19 +"delL x (B t1 a t2) b t3 = baldL (del x (B t1 a t2)) b t3" |
    2.20  "delL x t1 a t2 = R (del x t1) a t2" |
    2.21 -"delR x t1 a (B t2 b t3) = balR t1 a (del x (B t2 b t3))" | 
    2.22 +"delR x t1 a (B t2 b t3) = baldR t1 a (del x (B t2 b t3))" | 
    2.23  "delR x t1 a t2 = R t1 a (del x t2)"
    2.24  
    2.25  definition delete :: "'a::linorder \<Rightarrow> ('a*'b) rbt \<Rightarrow> ('a*'b) rbt" where
    2.26 @@ -45,7 +45,7 @@
    2.27  lemma inorder_upd:
    2.28    "sorted1(inorder t) \<Longrightarrow> inorder(upd x y t) = upd_list x y (inorder t)"
    2.29  by(induction x y t rule: upd.induct)
    2.30 -  (auto simp: upd_list_simps inorder_bal)
    2.31 +  (auto simp: upd_list_simps inorder_baliL inorder_baliR)
    2.32  
    2.33  lemma inorder_update:
    2.34    "sorted1(inorder t) \<Longrightarrow> inorder(update x y t) = upd_list x y (inorder t)"
    2.35 @@ -58,7 +58,7 @@
    2.36   "sorted1(inorder t2) \<Longrightarrow>  inorder(delR x t1 a t2) =
    2.37      inorder t1 @ a # del_list x (inorder t2)"
    2.38  by(induction x t1 and x t1 a t2 and x t1 a t2 rule: del_delL_delR.induct)
    2.39 -  (auto simp: del_list_simps inorder_combine inorder_balL inorder_balR)
    2.40 +  (auto simp: del_list_simps inorder_combine inorder_baldL inorder_baldR)
    2.41  
    2.42  lemma inorder_delete:
    2.43    "sorted1(inorder t) \<Longrightarrow> inorder(delete x t) = del_list x (inorder t)"
     3.1 --- a/src/HOL/Data_Structures/RBT_Set.thy	Fri Jan 27 22:27:03 2017 +0100
     3.2 +++ b/src/HOL/Data_Structures/RBT_Set.thy	Sat Jan 28 15:12:19 2017 +0100
     3.3 @@ -14,8 +14,8 @@
     3.4  "ins x Leaf = R Leaf x Leaf" |
     3.5  "ins x (B l a r) =
     3.6    (case cmp x a of
     3.7 -     LT \<Rightarrow> bal (ins x l) a r |
     3.8 -     GT \<Rightarrow> bal l a (ins x r) |
     3.9 +     LT \<Rightarrow> baliL (ins x l) a r |
    3.10 +     GT \<Rightarrow> baliR l a (ins x r) |
    3.11       EQ \<Rightarrow> B l a r)" |
    3.12  "ins x (R l a r) =
    3.13    (case cmp x a of
    3.14 @@ -36,9 +36,9 @@
    3.15       LT \<Rightarrow> delL x l a r |
    3.16       GT \<Rightarrow> delR x l a r |
    3.17       EQ \<Rightarrow> combine l r)" |
    3.18 -"delL x (B t1 a t2) b t3 = balL (del x (B t1 a t2)) b t3" |
    3.19 +"delL x (B t1 a t2) b t3 = baldL (del x (B t1 a t2)) b t3" |
    3.20  "delL x l a r = R (del x l) a r" |
    3.21 -"delR x t1 a (B t2 b t3) = balR t1 a (del x (B t2 b t3))" | 
    3.22 +"delR x t1 a (B t2 b t3) = baldR t1 a (del x (B t2 b t3))" | 
    3.23  "delR x l a r = R l a (del x r)"
    3.24  
    3.25  definition delete :: "'a::linorder \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
    3.26 @@ -50,30 +50,37 @@
    3.27  lemma inorder_paint: "inorder(paint c t) = inorder t"
    3.28  by(cases t) (auto)
    3.29  
    3.30 -lemma inorder_bal:
    3.31 -  "inorder(bal l a r) = inorder l @ a # inorder r"
    3.32 -by(cases "(l,a,r)" rule: bal.cases) (auto)
    3.33 +lemma inorder_baliL:
    3.34 +  "inorder(baliL l a r) = inorder l @ a # inorder r"
    3.35 +by(cases "(l,a,r)" rule: baliL.cases) (auto)
    3.36 +
    3.37 +lemma inorder_baliR:
    3.38 +  "inorder(baliR l a r) = inorder l @ a # inorder r"
    3.39 +by(cases "(l,a,r)" rule: baliR.cases) (auto)
    3.40  
    3.41  lemma inorder_ins:
    3.42    "sorted(inorder t) \<Longrightarrow> inorder(ins x t) = ins_list x (inorder t)"
    3.43 -by(induction x t rule: ins.induct) (auto simp: ins_list_simps inorder_bal)
    3.44 +by(induction x t rule: ins.induct)
    3.45 +  (auto simp: ins_list_simps inorder_baliL inorder_baliR)
    3.46  
    3.47  lemma inorder_insert:
    3.48    "sorted(inorder t) \<Longrightarrow> inorder(insert x t) = ins_list x (inorder t)"
    3.49  by (simp add: insert_def inorder_ins inorder_paint)
    3.50  
    3.51 -lemma inorder_balL:
    3.52 -  "inorder(balL l a r) = inorder l @ a # inorder r"
    3.53 -by(cases "(l,a,r)" rule: balL.cases)(auto simp: inorder_bal inorder_paint)
    3.54 +lemma inorder_baldL:
    3.55 +  "inorder(baldL l a r) = inorder l @ a # inorder r"
    3.56 +by(cases "(l,a,r)" rule: baldL.cases)
    3.57 +  (auto simp:  inorder_baliL inorder_baliR inorder_paint)
    3.58  
    3.59 -lemma inorder_balR:
    3.60 -  "inorder(balR l a r) = inorder l @ a # inorder r"
    3.61 -by(cases "(l,a,r)" rule: balR.cases) (auto simp: inorder_bal inorder_paint)
    3.62 +lemma inorder_baldR:
    3.63 +  "inorder(baldR l a r) = inorder l @ a # inorder r"
    3.64 +by(cases "(l,a,r)" rule: baldR.cases)
    3.65 +  (auto simp:  inorder_baliL inorder_baliR inorder_paint)
    3.66  
    3.67  lemma inorder_combine:
    3.68    "inorder(combine l r) = inorder l @ inorder r"
    3.69  by(induction l r rule: combine.induct)
    3.70 -  (auto simp: inorder_balL inorder_balR split: tree.split color.split)
    3.71 +  (auto simp: inorder_baldL inorder_baldR split: tree.split color.split)
    3.72  
    3.73  lemma inorder_del:
    3.74   "sorted(inorder t) \<Longrightarrow>  inorder(del x t) = del_list x (inorder t)"
    3.75 @@ -82,7 +89,7 @@
    3.76   "sorted(inorder r) \<Longrightarrow>  inorder(delR x l a r) =
    3.77      inorder l @ a # del_list x (inorder r)"
    3.78  by(induction x t and x l a r and x l a r rule: del_delL_delR.induct)
    3.79 -  (auto simp: del_list_simps inorder_combine inorder_balL inorder_balR)
    3.80 +  (auto simp: del_list_simps inorder_combine inorder_baldL inorder_baldR)
    3.81  
    3.82  lemma inorder_delete:
    3.83    "sorted(inorder t) \<Longrightarrow> inorder(delete x t) = del_list x (inorder t)"
    3.84 @@ -135,17 +142,29 @@
    3.85  lemma invh_paint: "invh t \<Longrightarrow> invh (paint c t)"
    3.86  by (cases t) auto
    3.87  
    3.88 -lemma invc_bal:
    3.89 -  "\<lbrakk>invc l \<and> invc2 r \<or> invc2 l \<and> invc r\<rbrakk> \<Longrightarrow> invc (bal l a r)" 
    3.90 -by (induct l a r rule: bal.induct) auto
    3.91 +lemma invc_baliL:
    3.92 +  "\<lbrakk>invc2 l; invc r\<rbrakk> \<Longrightarrow> invc (baliL l a r)" 
    3.93 +by (induct l a r rule: baliL.induct) auto
    3.94 +
    3.95 +lemma invc_baliR:
    3.96 +  "\<lbrakk>invc l; invc2 r\<rbrakk> \<Longrightarrow> invc (baliR l a r)" 
    3.97 +by (induct l a r rule: baliR.induct) auto
    3.98 +
    3.99 +lemma bheight_baliL:
   3.100 +  "bheight l = bheight r \<Longrightarrow> bheight (baliL l a r) = Suc (bheight l)"
   3.101 +by (induct l a r rule: baliL.induct) auto
   3.102  
   3.103 -lemma bheight_bal:
   3.104 -  "bheight l = bheight r \<Longrightarrow> bheight (bal l a r) = Suc (bheight l)"
   3.105 -by (induct l a r rule: bal.induct) auto
   3.106 +lemma bheight_baliR:
   3.107 +  "bheight l = bheight r \<Longrightarrow> bheight (baliR l a r) = Suc (bheight l)"
   3.108 +by (induct l a r rule: baliR.induct) auto
   3.109  
   3.110 -lemma invh_bal: 
   3.111 -  "\<lbrakk> invh l; invh r; bheight l = bheight r \<rbrakk> \<Longrightarrow> invh (bal l a r)"
   3.112 -by (induct l a r rule: bal.induct) auto
   3.113 +lemma invh_baliL: 
   3.114 +  "\<lbrakk> invh l; invh r; bheight l = bheight r \<rbrakk> \<Longrightarrow> invh (baliL l a r)"
   3.115 +by (induct l a r rule: baliL.induct) auto
   3.116 +
   3.117 +lemma invh_baliR: 
   3.118 +  "\<lbrakk> invh l; invh r; bheight l = bheight r \<rbrakk> \<Longrightarrow> invh (baliR l a r)"
   3.119 +by (induct l a r rule: baliR.induct) auto
   3.120  
   3.121  
   3.122  subsubsection \<open>Insertion\<close>
   3.123 @@ -153,12 +172,13 @@
   3.124  lemma invc_ins: assumes "invc t"
   3.125    shows "color t = Black \<Longrightarrow> invc (ins x t)" "invc2 (ins x t)"
   3.126  using assms
   3.127 -by (induct x t rule: ins.induct) (auto simp: invc_bal invc2I)
   3.128 +by (induct x t rule: ins.induct) (auto simp: invc_baliL invc_baliR invc2I)
   3.129  
   3.130  lemma invh_ins: assumes "invh t"
   3.131    shows "invh (ins x t)" "bheight (ins x t) = bheight t"
   3.132  using assms
   3.133 -by (induct x t rule: ins.induct) (auto simp: invh_bal bheight_bal)
   3.134 +by(induct x t rule: ins.induct)
   3.135 +  (auto simp: invh_baliL invh_baliR bheight_baliL bheight_baliR)
   3.136  
   3.137  theorem rbt_insert: "rbt t \<Longrightarrow> rbt (insert x t)"
   3.138  by (simp add: invc_ins invh_ins color_paint_Black invc_paint_Black invh_paint
   3.139 @@ -171,71 +191,72 @@
   3.140    "color t = Black \<Longrightarrow> bheight (paint Red t) = bheight t - 1"
   3.141  by (cases t) auto
   3.142  
   3.143 -lemma balL_invh_with_invc:
   3.144 -  assumes "invh lt" "invh rt" "bheight lt + 1 = bheight rt" "invc rt"
   3.145 -  shows "bheight (balL lt a rt) = bheight lt + 1"  "invh (balL lt a rt)"
   3.146 +lemma baldL_invh_with_invc:
   3.147 +  assumes "invh l" "invh r" "bheight l + 1 = bheight r" "invc r"
   3.148 +  shows "bheight (baldL l a r) = bheight l + 1"  "invh (baldL l a r)"
   3.149  using assms 
   3.150 -by (induct lt a rt rule: balL.induct)
   3.151 -   (auto simp: invh_bal invh_paint bheight_bal bheight_paint_Red)
   3.152 +by (induct l a r rule: baldL.induct)
   3.153 +   (auto simp: invh_baliR invh_paint bheight_baliR bheight_paint_Red)
   3.154  
   3.155 -lemma balL_invh_app: 
   3.156 -  assumes "invh lt" "invh rt" "bheight lt + 1 = bheight rt" "color rt = Black"
   3.157 -  shows "invh (balL lt a rt)" 
   3.158 -        "bheight (balL lt a rt) = bheight rt"
   3.159 +lemma baldL_invh_app: 
   3.160 +  assumes "invh l" "invh r" "bheight l + 1 = bheight r" "color r = Black"
   3.161 +  shows "invh (baldL l a r)" 
   3.162 +        "bheight (baldL l a r) = bheight r"
   3.163  using assms 
   3.164 -by (induct lt a rt rule: balL.induct) (auto simp add: invh_bal bheight_bal) 
   3.165 +by (induct l a r rule: baldL.induct) (auto simp add: invh_baliR bheight_baliR) 
   3.166  
   3.167 -lemma balL_invc: "\<lbrakk>invc2 l; invc r; color r = Black\<rbrakk> \<Longrightarrow> invc (balL l a r)"
   3.168 -by (induct l a r rule: balL.induct) (simp_all add: invc_bal)
   3.169 +lemma baldL_invc: "\<lbrakk>invc2 l; invc r; color r = Black\<rbrakk> \<Longrightarrow> invc (baldL l a r)"
   3.170 +by (induct l a r rule: baldL.induct) (simp_all add: invc_baliR)
   3.171  
   3.172 -lemma balL_invc2: "\<lbrakk> invc2 lt; invc rt \<rbrakk> \<Longrightarrow> invc2 (balL lt a rt)"
   3.173 -by (induct lt a rt rule: balL.induct) (auto simp: invc_bal paint_invc2 invc2I)
   3.174 +lemma baldL_invc2: "\<lbrakk> invc2 l; invc r \<rbrakk> \<Longrightarrow> invc2 (baldL l a r)"
   3.175 +by (induct l a r rule: baldL.induct) (auto simp: invc_baliR paint_invc2 invc2I)
   3.176  
   3.177 -lemma balR_invh_with_invc:
   3.178 -  assumes "invh lt" "invh rt" "bheight lt = bheight rt + 1" "invc lt"
   3.179 -  shows "invh (balR lt a rt) \<and> bheight (balR lt a rt) = bheight lt"
   3.180 +lemma baldR_invh_with_invc:
   3.181 +  assumes "invh l" "invh r" "bheight l = bheight r + 1" "invc l"
   3.182 +  shows "invh (baldR l a r) \<and> bheight (baldR l a r) = bheight l"
   3.183  using assms
   3.184 -by(induct lt a rt rule: balR.induct)
   3.185 -  (auto simp: invh_bal bheight_bal invh_paint bheight_paint_Red)
   3.186 +by(induct l a r rule: baldR.induct)
   3.187 +  (auto simp: invh_baliL bheight_baliL invh_paint bheight_paint_Red)
   3.188  
   3.189 -lemma invc_balR: "\<lbrakk>invc a; invc2 b; color a = Black\<rbrakk> \<Longrightarrow> invc (balR a x b)"
   3.190 -by (induct a x b rule: balR.induct) (simp_all add: invc_bal)
   3.191 +lemma invc_baldR: "\<lbrakk>invc a; invc2 b; color a = Black\<rbrakk> \<Longrightarrow> invc (baldR a x b)"
   3.192 +by (induct a x b rule: baldR.induct) (simp_all add: invc_baliL)
   3.193  
   3.194 -lemma invc2_balR: "\<lbrakk> invc lt; invc2 rt \<rbrakk> \<Longrightarrow>invc2 (balR lt x rt)"
   3.195 -by (induct lt x rt rule: balR.induct) (auto simp: invc_bal paint_invc2 invc2I)
   3.196 +lemma invc2_baldR: "\<lbrakk> invc l; invc2 r \<rbrakk> \<Longrightarrow>invc2 (baldR l x r)"
   3.197 +by (induct l x r rule: baldR.induct) (auto simp: invc_baliL paint_invc2 invc2I)
   3.198  
   3.199  lemma invh_combine:
   3.200 -  assumes "invh lt" "invh rt" "bheight lt = bheight rt"
   3.201 -  shows "bheight (combine lt rt) = bheight lt" "invh (combine lt rt)"
   3.202 +  assumes "invh l" "invh r" "bheight l = bheight r"
   3.203 +  shows "bheight (combine l r) = bheight l" "invh (combine l r)"
   3.204  using assms 
   3.205 -by (induct lt rt rule: combine.induct) 
   3.206 -   (auto simp: balL_invh_app split: tree.splits color.splits)
   3.207 +by (induct l r rule: combine.induct) 
   3.208 +   (auto simp: baldL_invh_app split: tree.splits color.splits)
   3.209  
   3.210  lemma invc_combine: 
   3.211 -  assumes "invc lt" "invc rt"
   3.212 -  shows "color lt = Black \<Longrightarrow> color rt = Black \<Longrightarrow> invc (combine lt rt)"
   3.213 -         "invc2 (combine lt rt)"
   3.214 +  assumes "invc l" "invc r"
   3.215 +  shows "color l = Black \<Longrightarrow> color r = Black \<Longrightarrow> invc (combine l r)"
   3.216 +         "invc2 (combine l r)"
   3.217  using assms 
   3.218 -by (induct lt rt rule: combine.induct)
   3.219 -   (auto simp: balL_invc invc2I split: tree.splits color.splits)
   3.220 +by (induct l r rule: combine.induct)
   3.221 +   (auto simp: baldL_invc invc2I split: tree.splits color.splits)
   3.222  
   3.223  
   3.224 -lemma assumes "invh lt" "invc lt"
   3.225 -  shows
   3.226 -  del_invc_invh: "invh (del x lt) \<and> (color lt = Red \<and> bheight (del x lt) = bheight lt \<and> invc (del x lt) 
   3.227 -  \<or> color lt = Black \<and> bheight (del x lt) = bheight lt - 1 \<and> invc2 (del x lt))"
   3.228 -and  "\<lbrakk>invh rt; bheight lt = bheight rt; invc rt\<rbrakk> \<Longrightarrow>
   3.229 -   invh (delL x lt k rt) \<and> 
   3.230 -   bheight (delL x lt k rt) = bheight lt \<and> 
   3.231 -   (color lt = Black \<and> color rt = Black \<and> invc (delL x lt k rt) \<or> 
   3.232 -    (color lt \<noteq> Black \<or> color rt \<noteq> Black) \<and> invc2 (delL x lt k rt))"
   3.233 -  and "\<lbrakk>invh rt; bheight lt = bheight rt; invc rt\<rbrakk> \<Longrightarrow>
   3.234 -  invh (delR x lt k rt) \<and> 
   3.235 -  bheight (delR x lt k rt) = bheight lt \<and> 
   3.236 -  (color lt = Black \<and> color rt = Black \<and> invc (delR x lt k rt) \<or> 
   3.237 -   (color lt \<noteq> Black \<or> color rt \<noteq> Black) \<and> invc2 (delR x lt k rt))"
   3.238 +lemma assumes "invh l" "invc l"
   3.239 +  shows del_invc_invh:
   3.240 +   "invh (del x l) \<and>
   3.241 +   (color l = Red \<and> bheight (del x l) = bheight l \<and> invc (del x l) \<or>
   3.242 +    color l = Black \<and> bheight (del x l) = bheight l - 1 \<and> invc2 (del x l))"
   3.243 +and  "\<lbrakk>invh r; bheight l = bheight r; invc r\<rbrakk> \<Longrightarrow>
   3.244 +   invh (delL x l k r) \<and> 
   3.245 +   bheight (delL x l k r) = bheight l \<and> 
   3.246 +   (color l = Black \<and> color r = Black \<and> invc (delL x l k r) \<or> 
   3.247 +    (color l \<noteq> Black \<or> color r \<noteq> Black) \<and> invc2 (delL x l k r))"
   3.248 +  and "\<lbrakk>invh r; bheight l = bheight r; invc r\<rbrakk> \<Longrightarrow>
   3.249 +  invh (delR x l k r) \<and> 
   3.250 +  bheight (delR x l k r) = bheight l \<and> 
   3.251 +  (color l = Black \<and> color r = Black \<and> invc (delR x l k r) \<or> 
   3.252 +   (color l \<noteq> Black \<or> color r \<noteq> Black) \<and> invc2 (delR x l k r))"
   3.253  using assms
   3.254 -proof (induct x lt and x lt k rt and x lt k rt rule: del_delL_delR.induct)
   3.255 +proof (induct x l and x l k r and x l k r rule: del_delL_delR.induct)
   3.256  case (2 y c _ y')
   3.257    have "y = y' \<or> y < y' \<or> y > y'" by auto
   3.258    thus ?case proof (elim disjE)
   3.259 @@ -250,11 +271,11 @@
   3.260      with 2 show ?thesis by (cases c) (auto simp: invc2I)
   3.261    qed
   3.262  next
   3.263 -  case (3 y lt z rta y' bb)
   3.264 -  thus ?case by (cases "color (Node Black lt z rta) = Black \<and> color bb = Black") (simp add: balL_invh_with_invc balL_invc balL_invc2)+
   3.265 +  case (3 y l z ra y' bb)
   3.266 +  thus ?case by (cases "color (Node Black l z ra) = Black \<and> color bb = Black") (simp add: baldL_invh_with_invc baldL_invc baldL_invc2)+
   3.267  next
   3.268 -  case (5 y a y' lt z rta)
   3.269 -  thus ?case by (cases "color a = Black \<and> color (Node Black lt z rta) = Black") (simp add: balR_invh_with_invc invc_balR invc2_balR)+
   3.270 +  case (5 y a y' l z ra)
   3.271 +  thus ?case by (cases "color a = Black \<and> color (Node Black l z ra) = Black") (simp add: baldR_invh_with_invc invc_baldR invc2_baldR)+
   3.272  next
   3.273    case ("6_1" y a y') thus ?case by (cases "color a = Black \<and> color Leaf = Black") simp+
   3.274  qed auto