src/HOL/Data_Structures/RBT_Set.thy
changeset 63411 e051eea34990
parent 62526 347150095fd2
child 64242 93c6f0da5c70
     1.1 --- a/src/HOL/Data_Structures/RBT_Set.thy	Thu Jul 07 09:24:03 2016 +0200
     1.2 +++ b/src/HOL/Data_Structures/RBT_Set.thy	Thu Jul 07 18:08:02 2016 +0200
     1.3 @@ -1,4 +1,4 @@
     1.4 -(* Author: Tobias Nipkow *)
     1.5 +(* Author: Tobias Nipkow, Daniel Stüwe *)
     1.6  
     1.7  section \<open>Red-Black Tree Implementation of Sets\<close>
     1.8  
     1.9 @@ -9,7 +9,7 @@
    1.10    Isin2
    1.11  begin
    1.12  
    1.13 -fun ins :: "'a::cmp \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
    1.14 +fun ins :: "'a::linorder \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
    1.15  "ins x Leaf = R Leaf x Leaf" |
    1.16  "ins x (B l a r) =
    1.17    (case cmp x a of
    1.18 @@ -22,12 +22,12 @@
    1.19      GT \<Rightarrow> R l a (ins x r) |
    1.20      EQ \<Rightarrow> R l a r)"
    1.21  
    1.22 -definition insert :: "'a::cmp \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
    1.23 +definition insert :: "'a::linorder \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
    1.24  "insert x t = paint Black (ins x t)"
    1.25  
    1.26 -fun del :: "'a::cmp \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt"
    1.27 -and delL :: "'a::cmp \<Rightarrow> 'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt"
    1.28 -and delR :: "'a::cmp \<Rightarrow> 'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt"
    1.29 +fun del :: "'a::linorder \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt"
    1.30 +and delL :: "'a::linorder \<Rightarrow> 'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt"
    1.31 +and delR :: "'a::linorder \<Rightarrow> 'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt"
    1.32  where
    1.33  "del x Leaf = Leaf" |
    1.34  "del x (Node _ l a r) =
    1.35 @@ -40,7 +40,7 @@
    1.36  "delR x t1 a (B t2 b t3) = balR t1 a (del x (B t2 b t3))" | 
    1.37  "delR x l a r = R l a (del x r)"
    1.38  
    1.39 -definition delete :: "'a::cmp \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
    1.40 +definition delete :: "'a::linorder \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
    1.41  "delete x t = paint Black (del x t)"
    1.42  
    1.43  
    1.44 @@ -88,21 +88,9 @@
    1.45  by (auto simp: delete_def inorder_del inorder_paint)
    1.46  
    1.47  
    1.48 -interpretation Set_by_Ordered
    1.49 -where empty = Leaf and isin = isin and insert = insert and delete = delete
    1.50 -and inorder = inorder and inv = "\<lambda>_. True"
    1.51 -proof (standard, goal_cases)
    1.52 -  case 1 show ?case by simp
    1.53 -next
    1.54 -  case 2 thus ?case by(simp add: isin_set)
    1.55 -next
    1.56 -  case 3 thus ?case by(simp add: inorder_insert)
    1.57 -next
    1.58 -  case 4 thus ?case by(simp add: inorder_delete)
    1.59 -qed auto
    1.60 +subsection \<open>Structural invariants\<close>
    1.61  
    1.62 -
    1.63 -subsection \<open>Structural invariants\<close>
    1.64 +text\<open>The proofs are due to Markus Reiter and Alexander Krauss,\<close>
    1.65  
    1.66  fun color :: "'a rbt \<Rightarrow> color" where
    1.67  "color Leaf = Black" |
    1.68 @@ -112,24 +100,24 @@
    1.69  "bheight Leaf = 0" |
    1.70  "bheight (Node c l x r) = (if c = Black then Suc(bheight l) else bheight l)"
    1.71  
    1.72 -fun inv1 :: "'a rbt \<Rightarrow> bool" where
    1.73 -"inv1 Leaf = True" |
    1.74 -"inv1 (Node c l a r) =
    1.75 -  (inv1 l \<and> inv1 r \<and> (c = Black \<or> color l = Black \<and> color r = Black))"
    1.76 +fun invc :: "'a rbt \<Rightarrow> bool" where
    1.77 +"invc Leaf = True" |
    1.78 +"invc (Node c l a r) =
    1.79 +  (invc l \<and> invc r \<and> (c = Black \<or> color l = Black \<and> color r = Black))"
    1.80  
    1.81 -fun inv1_root :: "'a rbt \<Rightarrow> bool" \<comment> \<open>Weaker version\<close> where
    1.82 -"inv1_root Leaf = True" |
    1.83 -"inv1_root (Node c l a r) = (inv1 l \<and> inv1 r)"
    1.84 +fun invc_sons :: "'a rbt \<Rightarrow> bool" \<comment> \<open>Weaker version\<close> where
    1.85 +"invc_sons Leaf = True" |
    1.86 +"invc_sons (Node c l a r) = (invc l \<and> invc r)"
    1.87  
    1.88 -fun inv2 :: "'a rbt \<Rightarrow> bool" where
    1.89 -"inv2 Leaf = True" |
    1.90 -"inv2 (Node c l x r) = (inv2 l \<and> inv2 r \<and> bheight l = bheight r)"
    1.91 +fun invh :: "'a rbt \<Rightarrow> bool" where
    1.92 +"invh Leaf = True" |
    1.93 +"invh (Node c l x r) = (invh l \<and> invh r \<and> bheight l = bheight r)"
    1.94  
    1.95 -lemma inv1_rootI[simp]: "inv1 t \<Longrightarrow> inv1_root t"
    1.96 +lemma invc_sonsI: "invc t \<Longrightarrow> invc_sons t"
    1.97  by (cases t) simp+
    1.98  
    1.99  definition rbt :: "'a rbt \<Rightarrow> bool" where
   1.100 -"rbt t = (inv1 t \<and> inv2 t \<and> color t = Black)"
   1.101 +"rbt t = (invc t \<and> invh t \<and> color t = Black)"
   1.102  
   1.103  lemma color_paint_Black: "color (paint Black t) = Black"
   1.104  by (cases t) auto
   1.105 @@ -137,142 +125,386 @@
   1.106  theorem rbt_Leaf: "rbt Leaf"
   1.107  by (simp add: rbt_def)
   1.108  
   1.109 -lemma paint_inv1_root: "inv1_root t \<Longrightarrow> inv1_root (paint c t)"
   1.110 +lemma paint_invc_sons: "invc_sons t \<Longrightarrow> invc_sons (paint c t)"
   1.111  by (cases t) auto
   1.112  
   1.113 -lemma inv1_paint_Black: "inv1_root t \<Longrightarrow> inv1 (paint Black t)"
   1.114 +lemma invc_paint_Black: "invc_sons t \<Longrightarrow> invc (paint Black t)"
   1.115  by (cases t) auto
   1.116  
   1.117 -lemma inv2_paint: "inv2 t \<Longrightarrow> inv2 (paint c t)"
   1.118 +lemma invh_paint: "invh t \<Longrightarrow> invh (paint c t)"
   1.119  by (cases t) auto
   1.120  
   1.121 -lemma inv1_bal: "\<lbrakk>inv1_root l; inv1_root r\<rbrakk> \<Longrightarrow> inv1 (bal l a r)" 
   1.122 +lemma invc_bal: "\<lbrakk>invc_sons l; invc_sons r\<rbrakk> \<Longrightarrow> invc (bal l a r)" 
   1.123  by (induct l a r rule: bal.induct) auto
   1.124  
   1.125  lemma bheight_bal:
   1.126    "bheight l = bheight r \<Longrightarrow> bheight (bal l a r) = Suc (bheight l)"
   1.127  by (induct l a r rule: bal.induct) auto
   1.128  
   1.129 -lemma inv2_bal: 
   1.130 -  "\<lbrakk> inv2 l; inv2 r; bheight l = bheight r \<rbrakk> \<Longrightarrow> inv2 (bal l a r)"
   1.131 +lemma invh_bal: 
   1.132 +  "\<lbrakk> invh l; invh r; bheight l = bheight r \<rbrakk> \<Longrightarrow> invh (bal l a r)"
   1.133  by (induct l a r rule: bal.induct) auto
   1.134  
   1.135  
   1.136  subsubsection \<open>Insertion\<close>
   1.137  
   1.138 -lemma inv1_ins: assumes "inv1 t"
   1.139 -  shows "color t = Black \<Longrightarrow> inv1 (ins x t)" "inv1_root (ins x t)"
   1.140 +lemma invc_ins: assumes "invc t"
   1.141 +  shows "color t = Black \<Longrightarrow> invc (ins x t)" "invc_sons (ins x t)"
   1.142  using assms
   1.143 -by (induct x t rule: ins.induct) (auto simp: inv1_bal)
   1.144 +by (induct x t rule: ins.induct) (auto simp: invc_bal invc_sonsI)
   1.145  
   1.146 -lemma inv2_ins: assumes "inv2 t"
   1.147 -  shows "inv2 (ins x t)" "bheight (ins x t) = bheight t"
   1.148 +lemma invh_ins: assumes "invh t"
   1.149 +  shows "invh (ins x t)" "bheight (ins x t) = bheight t"
   1.150  using assms
   1.151 -by (induct x t rule: ins.induct) (auto simp: inv2_bal bheight_bal)
   1.152 +by (induct x t rule: ins.induct) (auto simp: invh_bal bheight_bal)
   1.153  
   1.154 -theorem rbt_ins: "rbt t \<Longrightarrow> rbt (insert x t)"
   1.155 -by (simp add: inv1_ins inv2_ins color_paint_Black inv1_paint_Black inv2_paint
   1.156 +theorem rbt_insert: "rbt t \<Longrightarrow> rbt (insert x t)"
   1.157 +by (simp add: invc_ins invh_ins color_paint_Black invc_paint_Black invh_paint
   1.158    rbt_def insert_def)
   1.159  
   1.160 -(*
   1.161 -lemma bheight_paintR'[simp]: "color t = Black \<Longrightarrow> bheight (paint Red t) = bheight t - 1"
   1.162 +
   1.163 +subsubsection \<open>Deletion\<close>
   1.164 +
   1.165 +lemma bheight_paint_Red:
   1.166 +  "color t = Black \<Longrightarrow> bheight (paint Red t) = bheight t - 1"
   1.167  by (cases t) auto
   1.168  
   1.169 -lemma balL_inv2_with_inv1:
   1.170 -  assumes "inv2 lt" "inv2 rt" "bheight lt + 1 = bheight rt" "inv1 rt"
   1.171 -  shows "bheight (balL lt a rt) = bheight lt + 1"  "inv2 (balL lt a rt)"
   1.172 +lemma balL_invh_with_invc:
   1.173 +  assumes "invh lt" "invh rt" "bheight lt + 1 = bheight rt" "invc rt"
   1.174 +  shows "bheight (balL lt a rt) = bheight lt + 1"  "invh (balL lt a rt)"
   1.175  using assms 
   1.176 -by (induct lt a rt rule: balL.induct) (auto simp: inv2_bal inv2_paint bheight_bal)
   1.177 +by (induct lt a rt rule: balL.induct)
   1.178 +   (auto simp: invh_bal invh_paint bheight_bal bheight_paint_Red)
   1.179  
   1.180 -lemma balL_inv2_app: 
   1.181 -  assumes "inv2 lt" "inv2 rt" "bheight lt + 1 = bheight rt" "color rt = Black"
   1.182 -  shows "inv2 (balL lt a rt)" 
   1.183 +lemma balL_invh_app: 
   1.184 +  assumes "invh lt" "invh rt" "bheight lt + 1 = bheight rt" "color rt = Black"
   1.185 +  shows "invh (balL lt a rt)" 
   1.186          "bheight (balL lt a rt) = bheight rt"
   1.187  using assms 
   1.188 -by (induct lt a rt rule: balL.induct) (auto simp add: inv2_bal bheight_bal) 
   1.189 +by (induct lt a rt rule: balL.induct) (auto simp add: invh_bal bheight_bal) 
   1.190  
   1.191 -lemma balL_inv1: "\<lbrakk>inv1_root l; inv1 r; color r = Black\<rbrakk> \<Longrightarrow> inv1 (balL l a r)"
   1.192 -by (induct l a r rule: balL.induct) (simp_all add: inv1_bal)
   1.193 +lemma balL_invc: "\<lbrakk>invc_sons l; invc r; color r = Black\<rbrakk> \<Longrightarrow> invc (balL l a r)"
   1.194 +by (induct l a r rule: balL.induct) (simp_all add: invc_bal)
   1.195  
   1.196 -lemma balL_inv1_root: "\<lbrakk> inv1_root lt; inv1 rt \<rbrakk> \<Longrightarrow> inv1_root (balL lt a rt)"
   1.197 -by (induct lt a rt rule: balL.induct) (auto simp: inv1_bal paint_inv1_root)
   1.198 +lemma balL_invc_sons: "\<lbrakk> invc_sons lt; invc rt \<rbrakk> \<Longrightarrow> invc_sons (balL lt a rt)"
   1.199 +by (induct lt a rt rule: balL.induct) (auto simp: invc_bal paint_invc_sons invc_sonsI)
   1.200  
   1.201 -lemma balR_inv2_with_inv1:
   1.202 -  assumes "inv2 lt" "inv2 rt" "bheight lt = bheight rt + 1" "inv1 lt"
   1.203 -  shows "inv2 (balR lt a rt) \<and> bheight (balR lt a rt) = bheight lt"
   1.204 +lemma balR_invh_with_invc:
   1.205 +  assumes "invh lt" "invh rt" "bheight lt = bheight rt + 1" "invc lt"
   1.206 +  shows "invh (balR lt a rt) \<and> bheight (balR lt a rt) = bheight lt"
   1.207  using assms
   1.208 -by(induct lt a rt rule: balR.induct)(auto simp: inv2_bal bheight_bal inv2_paint)
   1.209 +by(induct lt a rt rule: balR.induct)
   1.210 +  (auto simp: invh_bal bheight_bal invh_paint bheight_paint_Red)
   1.211  
   1.212 -lemma balR_inv1: "\<lbrakk>inv1 a; inv1_root b; color a = Black\<rbrakk> \<Longrightarrow> inv1 (balR a x b)"
   1.213 -by (induct a x b rule: balR.induct) (simp_all add: inv1_bal)
   1.214 +lemma invc_balR: "\<lbrakk>invc a; invc_sons b; color a = Black\<rbrakk> \<Longrightarrow> invc (balR a x b)"
   1.215 +by (induct a x b rule: balR.induct) (simp_all add: invc_bal)
   1.216  
   1.217 -lemma balR_inv1_root: "\<lbrakk> inv1 lt; inv1_root rt \<rbrakk> \<Longrightarrow>inv1_root (balR lt x rt)"
   1.218 -by (induct lt x rt rule: balR.induct) (auto simp: inv1_bal paint_inv1_root)
   1.219 +lemma invc_sons_balR: "\<lbrakk> invc lt; invc_sons rt \<rbrakk> \<Longrightarrow>invc_sons (balR lt x rt)"
   1.220 +by (induct lt x rt rule: balR.induct) (auto simp: invc_bal paint_invc_sons invc_sonsI)
   1.221  
   1.222 -lemma combine_inv2:
   1.223 -  assumes "inv2 lt" "inv2 rt" "bheight lt = bheight rt"
   1.224 -  shows "bheight (combine lt rt) = bheight lt" "inv2 (combine lt rt)"
   1.225 +lemma invh_combine:
   1.226 +  assumes "invh lt" "invh rt" "bheight lt = bheight rt"
   1.227 +  shows "bheight (combine lt rt) = bheight lt" "invh (combine lt rt)"
   1.228  using assms 
   1.229  by (induct lt rt rule: combine.induct) 
   1.230 -   (auto simp: balL_inv2_app split: tree.splits color.splits)
   1.231 +   (auto simp: balL_invh_app split: tree.splits color.splits)
   1.232  
   1.233 -lemma combine_inv1: 
   1.234 -  assumes "inv1 lt" "inv1 rt"
   1.235 -  shows "color lt = Black \<Longrightarrow> color rt = Black \<Longrightarrow> inv1 (combine lt rt)"
   1.236 -         "inv1_root (combine lt rt)"
   1.237 +lemma invc_combine: 
   1.238 +  assumes "invc lt" "invc rt"
   1.239 +  shows "color lt = Black \<Longrightarrow> color rt = Black \<Longrightarrow> invc (combine lt rt)"
   1.240 +         "invc_sons (combine lt rt)"
   1.241  using assms 
   1.242  by (induct lt rt rule: combine.induct)
   1.243 -   (auto simp: balL_inv1 split: tree.splits color.splits)
   1.244 +   (auto simp: balL_invc invc_sonsI split: tree.splits color.splits)
   1.245  
   1.246  
   1.247 -lemma 
   1.248 -  assumes "inv2 lt" "inv1 lt"
   1.249 +lemma assumes "invh lt" "invc lt"
   1.250    shows
   1.251 -  "\<lbrakk>inv2 rt; bheight lt = bheight rt; inv1 rt\<rbrakk> \<Longrightarrow>
   1.252 -   inv2 (rbt_del_from_left x lt k v rt) \<and> 
   1.253 -   bheight (rbt_del_from_left x lt k v rt) = bheight lt \<and> 
   1.254 -   (color_of lt = B \<and> color_of rt = B \<and> inv1 (rbt_del_from_left x lt k v rt) \<or> 
   1.255 -    (color_of lt \<noteq> B \<or> color_of rt \<noteq> B) \<and> inv1l (rbt_del_from_left x lt k v rt))"
   1.256 -  and "\<lbrakk>inv2 rt; bheight lt = bheight rt; inv1 rt\<rbrakk> \<Longrightarrow>
   1.257 -  inv2 (rbt_del_from_right x lt k v rt) \<and> 
   1.258 -  bheight (rbt_del_from_right x lt k v rt) = bheight lt \<and> 
   1.259 -  (color_of lt = B \<and> color_of rt = B \<and> inv1 (rbt_del_from_right x lt k v rt) \<or> 
   1.260 -   (color_of lt \<noteq> B \<or> color_of rt \<noteq> B) \<and> inv1l (rbt_del_from_right x lt k v rt))"
   1.261 -  and rbt_del_inv1_inv2: "inv2 (rbt_del x lt) \<and> (color_of lt = R \<and> bheight (rbt_del x lt) = bheight lt \<and> inv1 (rbt_del x lt) 
   1.262 -  \<or> color_of lt = B \<and> bheight (rbt_del x lt) = bheight lt - 1 \<and> inv1l (rbt_del x lt))"
   1.263 +  del_invc_invh: "invh (del x lt) \<and> (color lt = Red \<and> bheight (del x lt) = bheight lt \<and> invc (del x lt) 
   1.264 +  \<or> color lt = Black \<and> bheight (del x lt) = bheight lt - 1 \<and> invc_sons (del x lt))"
   1.265 +and  "\<lbrakk>invh rt; bheight lt = bheight rt; invc rt\<rbrakk> \<Longrightarrow>
   1.266 +   invh (delL x lt k rt) \<and> 
   1.267 +   bheight (delL x lt k rt) = bheight lt \<and> 
   1.268 +   (color lt = Black \<and> color rt = Black \<and> invc (delL x lt k rt) \<or> 
   1.269 +    (color lt \<noteq> Black \<or> color rt \<noteq> Black) \<and> invc_sons (delL x lt k rt))"
   1.270 +  and "\<lbrakk>invh rt; bheight lt = bheight rt; invc rt\<rbrakk> \<Longrightarrow>
   1.271 +  invh (delR x lt k rt) \<and> 
   1.272 +  bheight (delR x lt k rt) = bheight lt \<and> 
   1.273 +  (color lt = Black \<and> color rt = Black \<and> invc (delR x lt k rt) \<or> 
   1.274 +   (color lt \<noteq> Black \<or> color rt \<noteq> Black) \<and> invc_sons (delR x lt k rt))"
   1.275  using assms
   1.276 -proof (induct x lt k v rt and x lt k v rt and x lt rule: rbt_del_from_left_rbt_del_from_right_rbt_del.induct)
   1.277 +proof (induct x lt and x lt k rt and x lt k rt rule: del_delL_delR.induct)
   1.278  case (2 y c _ y')
   1.279    have "y = y' \<or> y < y' \<or> y > y'" by auto
   1.280    thus ?case proof (elim disjE)
   1.281      assume "y = y'"
   1.282 -    with 2 show ?thesis by (cases c) (simp add: combine_inv2 combine_inv1)+
   1.283 +    with 2 show ?thesis
   1.284 +    by (cases c) (simp_all add: invh_combine invc_combine)
   1.285    next
   1.286      assume "y < y'"
   1.287 -    with 2 show ?thesis by (cases c) auto
   1.288 +    with 2 show ?thesis by (cases c) (auto simp: invc_sonsI)
   1.289    next
   1.290      assume "y' < y"
   1.291 -    with 2 show ?thesis by (cases c) auto
   1.292 +    with 2 show ?thesis by (cases c) (auto simp: invc_sonsI)
   1.293    qed
   1.294  next
   1.295 -  case (3 y lt z v rta y' ss bb) 
   1.296 -  thus ?case by (cases "color_of (Branch B lt z v rta) = B \<and> color_of bb = B") (simp add: balance_left_inv2_with_inv1 balance_left_inv1 balance_left_inv1l)+
   1.297 +  case (3 y lt z rta y' bb)
   1.298 +  thus ?case by (cases "color (Node Black lt z rta) = Black \<and> color bb = Black") (simp add: balL_invh_with_invc balL_invc balL_invc_sons)+
   1.299  next
   1.300 -  case (5 y a y' ss lt z v rta)
   1.301 -  thus ?case by (cases "color_of a = B \<and> color_of (Branch B lt z v rta) = B") (simp add: balance_right_inv2_with_inv1 balance_right_inv1 balance_right_inv1l)+
   1.302 +  case (5 y a y' lt z rta)
   1.303 +  thus ?case by (cases "color a = Black \<and> color (Node Black lt z rta) = Black") (simp add: balR_invh_with_invc invc_balR invc_sons_balR)+
   1.304  next
   1.305 -  case ("6_1" y a y' ss) thus ?case by (cases "color_of a = B \<and> color_of Empty = B") simp+
   1.306 +  case ("6_1" y a y') thus ?case by (cases "color a = Black \<and> color Leaf = Black") simp+
   1.307  qed auto
   1.308  
   1.309 -theorem rbt_delete_is_rbt [simp]: assumes "rbt t" shows "rbt (delete k t)"
   1.310 +theorem rbt_delete: "rbt t \<Longrightarrow> rbt (delete k t)"
   1.311 +by (metis delete_def rbt_def color_paint_Black del_invc_invh invc_paint_Black invc_sonsI invh_paint)
   1.312 +
   1.313 +text \<open>Overall correctness:\<close>
   1.314 +
   1.315 +interpretation Set_by_Ordered
   1.316 +where empty = Leaf and isin = isin and insert = insert and delete = delete
   1.317 +and inorder = inorder and inv = rbt
   1.318 +proof (standard, goal_cases)
   1.319 +  case 1 show ?case by simp
   1.320 +next
   1.321 +  case 2 thus ?case by(simp add: isin_set)
   1.322 +next
   1.323 +  case 3 thus ?case by(simp add: inorder_insert)
   1.324 +next
   1.325 +  case 4 thus ?case by(simp add: inorder_delete)
   1.326 +next
   1.327 +  case 5 thus ?case by (simp add: rbt_Leaf) 
   1.328 +next
   1.329 +  case 6 thus ?case by (simp add: rbt_insert) 
   1.330 +next
   1.331 +  case 7 thus ?case by (simp add: rbt_delete) 
   1.332 +qed
   1.333 +
   1.334 +
   1.335 +subsection \<open>Height-Size Relation\<close>
   1.336 +
   1.337 +text \<open>By Daniel St\"uwe\<close>
   1.338 +
   1.339 +lemma color_RedE:"color t = Red \<Longrightarrow> invc t =
   1.340 + (\<exists> l a r . t = R l a r \<and> color l = Black \<and> color r = Black \<and> invc l \<and> invc r)"
   1.341 +by (cases t) auto
   1.342 +
   1.343 +lemma rbt_induct[consumes 1]:
   1.344 +  assumes "rbt t"
   1.345 +  assumes [simp]: "P Leaf"
   1.346 +  assumes "\<And> t l a r. \<lbrakk>t = B l a r; invc t; invh t; Q(l); Q(r)\<rbrakk> \<Longrightarrow> P t"
   1.347 +  assumes "\<And> t l a r. \<lbrakk>t = R l a r; invc t; invh t; P(l); P(r)\<rbrakk> \<Longrightarrow> Q t"
   1.348 +  assumes "\<And> t . P(t) \<Longrightarrow> Q(t)"
   1.349 +  shows "P t"
   1.350 +using assms(1) unfolding rbt_def apply safe
   1.351 +proof (induction t rule: measure_induct[of size])
   1.352 +case (1 t)
   1.353 +  note * = 1 assms
   1.354 +  show ?case proof (cases t)
   1.355 +    case [simp]: (Node c l a r)
   1.356 +    show ?thesis proof (cases c)
   1.357 +      case Red thus ?thesis using 1 by simp
   1.358 +    next
   1.359 +      case [simp]: Black
   1.360 +      show ?thesis
   1.361 +      proof (cases "color l")
   1.362 +        case Red
   1.363 +        thus ?thesis using * by (cases "color r") (auto simp: color_RedE)
   1.364 +      next
   1.365 +        case Black
   1.366 +        thus ?thesis using * by (cases "color r") (auto simp: color_RedE)
   1.367 +      qed
   1.368 +    qed
   1.369 +  qed simp
   1.370 +qed
   1.371 +
   1.372 +lemma rbt_b_height: "rbt t \<Longrightarrow> bheight t * 2 \<ge> height t"
   1.373 +by (induction t rule: rbt_induct[where Q="\<lambda> t. bheight t * 2 + 1 \<ge> height t"]) auto
   1.374 +
   1.375 +lemma red_b_height: "invc t \<Longrightarrow> invh t \<Longrightarrow> bheight t * 2 + 1 \<ge> height t"
   1.376 +apply (cases t) apply simp
   1.377 +  using rbt_b_height unfolding rbt_def
   1.378 +  by (cases "color t") fastforce+
   1.379 +
   1.380 +lemma red_b_height2: "invc t \<Longrightarrow> invh t \<Longrightarrow> bheight t \<ge> height t div 2"
   1.381 +using red_b_height by fastforce
   1.382 +
   1.383 +lemma rbt_b_height2: "bheight t \<le> height t"
   1.384 +by (induction t) auto
   1.385 +
   1.386 +lemma "rbt t \<Longrightarrow> size1 t \<le>  4 ^ (bheight t)"
   1.387 +by(induction t rule: rbt_induct[where Q="\<lambda> t. size1 t \<le>  2 * 4 ^ (bheight t)"]) auto
   1.388 +
   1.389 +lemma bheight_size_bound:  "rbt t \<Longrightarrow> size1 t \<ge>  2 ^ (bheight t)"
   1.390 +by (induction t rule: rbt_induct[where Q="\<lambda> t. size1 t \<ge>  2 ^ (bheight t)"]) auto
   1.391 +
   1.392 +text \<open>Balanced red-balck tree with all black nodes:\<close>
   1.393 +inductive balB :: "nat \<Rightarrow> unit rbt \<Rightarrow> bool"  where
   1.394 +"balB 0 Leaf" |
   1.395 +"balB h t \<Longrightarrow> balB (Suc h) (B t () t)"
   1.396 +
   1.397 +inductive_cases [elim!]: "balB 0 t"
   1.398 +inductive_cases [elim]: "balB (Suc h) t"
   1.399 +
   1.400 +lemma balB_hs: "balB h t \<Longrightarrow> bheight t = height t"
   1.401 +by (induction h t rule: "balB.induct") auto
   1.402 +
   1.403 +lemma balB_h: "balB h t \<Longrightarrow> h = height t"
   1.404 +by (induction h t rule: "balB.induct") auto
   1.405 +
   1.406 +lemma "rbt t \<Longrightarrow> balB (bheight t) t' \<Longrightarrow> size t' \<le> size t"
   1.407 +by (induction t arbitrary: t' 
   1.408 + rule: rbt_induct[where Q="\<lambda> t . \<forall> h t'. balB (bheight t) t' \<longrightarrow> size t' \<le> size t"])
   1.409 + fastforce+
   1.410 +
   1.411 +lemma balB_bh: "invc t \<Longrightarrow> invh t \<Longrightarrow> balB (bheight t) t' \<Longrightarrow> size t' \<le> size t"
   1.412 +by (induction t arbitrary: t') (fastforce split: if_split_asm)+
   1.413 +
   1.414 +lemma balB_bh3:"\<lbrakk> balB h t; balB (h' + h) t' \<rbrakk> \<Longrightarrow> size t \<le> size t'"
   1.415 +by (induction h t arbitrary: t' h' rule: balB.induct)  fastforce+
   1.416 +
   1.417 +corollary balB_bh3': "\<lbrakk> balB h t; balB h' t'; h \<le> h' \<rbrakk> \<Longrightarrow> size t \<le> size t'"
   1.418 +using balB_bh3 le_Suc_ex by (fastforce simp: algebra_simps)
   1.419 +
   1.420 +lemma exist_pt: "\<exists> t . balB h t"
   1.421 +by (induction h) (auto intro: balB.intros)
   1.422 +
   1.423 +corollary compact_pt:
   1.424 +  assumes "invc t" "invh t" "h \<le> bheight t" "balB h t'"
   1.425 +  shows   "size t' \<le> size t"
   1.426  proof -
   1.427 -  from assms have "inv2 t" and "inv1 t" unfolding rbt_def by auto 
   1.428 -  hence "inv2 (del k t) \<and> (color t = Red \<and> bheight (del k t) = bheight t \<and> inv1 (del k t) \<or> color t = Black \<and> bheight (del k t) = bheight t - 1 \<and> inv1_root (del k t))"
   1.429 -    by (rule rbt_del_inv1_inv2)
   1.430 -  hence "inv2 (del k t) \<and> inv1l (rbt_del k t)" by (cases "color_of t") auto
   1.431 -  with assms show ?thesis
   1.432 -    unfolding is_rbt_def rbt_delete_def
   1.433 -    by (auto intro: paint_rbt_sorted rbt_del_rbt_sorted)
   1.434 +  obtain t'' where "balB (bheight t) t''" using exist_pt by blast
   1.435 +  thus ?thesis using assms balB_bh[of t t''] balB_bh3'[of h t' "bheight t" t''] by auto
   1.436 +qed
   1.437 +
   1.438 +lemma balB_bh2: "balB (bheight t) t'\<Longrightarrow> invc t \<Longrightarrow> invh t \<Longrightarrow> height t' \<le> height t"
   1.439 +apply (induction "(bheight t)" t' arbitrary: t rule: balB.induct)
   1.440 +using balB_h rbt_b_height2 by auto
   1.441 +
   1.442 +lemma balB_rbt: "balB h t \<Longrightarrow> rbt t"
   1.443 +unfolding rbt_def
   1.444 +by (induction h t rule: balB.induct) auto
   1.445 +
   1.446 +lemma balB_size[simp]: "balB h t \<Longrightarrow> size1 t = 2^h"
   1.447 +by (induction h t rule: balB.induct) auto
   1.448 +
   1.449 +text \<open>Red-black tree (except that the root may be red) of minimal size
   1.450 +for a given height:\<close>
   1.451 +
   1.452 +inductive RB :: "nat \<Rightarrow> unit rbt \<Rightarrow> bool" where
   1.453 +"RB 0 Leaf" |
   1.454 +"balB (h div 2) t \<Longrightarrow> RB h t' \<Longrightarrow> color t' = Red \<Longrightarrow> RB (Suc h) (B t' () t)" |
   1.455 +"balB (h div 2) t \<Longrightarrow> RB h t' \<Longrightarrow> color t' = Black \<Longrightarrow> RB (Suc h) (R t' () t)" 
   1.456 +
   1.457 +lemmas RB.intros[intro]
   1.458 +
   1.459 +lemma RB_invc: "RB h t \<Longrightarrow> invc t"
   1.460 +apply (induction h t rule: RB.induct)
   1.461 +using balB_rbt unfolding rbt_def by auto
   1.462 +
   1.463 +lemma RB_h: "RB h t \<Longrightarrow> h = height t"
   1.464 +apply (induction h t rule: RB.induct)
   1.465 +using balB_h by auto
   1.466 +
   1.467 +lemma RB_mod: "RB h t \<Longrightarrow> (color t = Black \<longleftrightarrow> h mod 2 = 0)"
   1.468 +apply (induction h t rule: RB.induct)
   1.469 +apply auto
   1.470 +by presburger
   1.471 +
   1.472 +lemma RB_b_height: "RB h t \<Longrightarrow> height t div 2 = bheight t"
   1.473 +proof  (induction h t rule: RB.induct)
   1.474 +  case 1 
   1.475 +  thus ?case by auto 
   1.476 +next
   1.477 +  case (2 h t t')
   1.478 +  with RB_mod obtain n where "2*n + 1 = h" 
   1.479 +    by (metis color.distinct(1) mod_div_equality2 parity) 
   1.480 +  with 2 balB_h RB_h show ?case by auto
   1.481 +next
   1.482 +  case (3 h t t')
   1.483 +  with RB_mod[OF 3(2)] parity obtain n where "2*n = h" by blast
   1.484 +  with 3 balB_h RB_h show ?case by auto
   1.485  qed
   1.486 -*)
   1.487 +
   1.488 +lemma weak_RB_induct[consumes 1]: 
   1.489 +  "RB h t \<Longrightarrow> P 0 \<langle>\<rangle> \<Longrightarrow> (\<And>h t t' c . balB (h div 2) t \<Longrightarrow> RB h t' \<Longrightarrow>
   1.490 +    P h t' \<Longrightarrow> P (Suc h) (Node c t' () t)) \<Longrightarrow> P h t"
   1.491 +using RB.induct by metis
   1.492 +
   1.493 +lemma RB_invh: "RB h t \<Longrightarrow> invh t"
   1.494 +apply (induction h t rule: weak_RB_induct)
   1.495 +  using balB_h balB_hs RB_h balB_rbt RB_b_height
   1.496 +  unfolding rbt_def
   1.497 +by auto
   1.498 +
   1.499 +lemma RB_bheight_minimal:
   1.500 +  "\<lbrakk>RB (height t') t; invc t'; invh t'\<rbrakk> \<Longrightarrow> bheight t \<le> bheight t'"
   1.501 +using RB_b_height RB_h red_b_height2 by fastforce
   1.502 +
   1.503 +lemma RB_minimal: "RB (height t') t \<Longrightarrow> invh t \<Longrightarrow> invc t' \<Longrightarrow> invh t' \<Longrightarrow> size t \<le> size t'"
   1.504 +proof (induction "(height t')" t arbitrary: t' rule: weak_RB_induct)
   1.505 +  case 1 thus ?case by auto 
   1.506 +next
   1.507 +  case (2 h t t'')
   1.508 +  have ***: "size (Node c t'' () t) \<le> size t'"
   1.509 +    if assms:
   1.510 +      "\<And> (t' :: 'a rbt) . \<lbrakk> h = height t'; invh t''; invc t'; invh t' \<rbrakk>
   1.511 +                            \<Longrightarrow> size t'' \<le> size t'"
   1.512 +      "Suc h = height t'" "balB (h div 2) t" "RB h t''"
   1.513 +      "invc t'" "invh t'" "height l \<ge> height r"
   1.514 +      and tt[simp]:"t' = Node c l a r" and last: "invh (Node c t'' () t)"
   1.515 +  for t' :: "'a rbt" and c l a r
   1.516 +  proof -
   1.517 +    from assms have inv: "invc r" "invh r" by auto
   1.518 +    from assms have "height l = h" using max_def by auto
   1.519 +    with RB_bheight_minimal[of l t''] have
   1.520 +      "bheight t \<le> bheight r" using assms last by auto
   1.521 +    with compact_pt[OF inv] balB_h balB_hs have 
   1.522 +      "size t \<le> size r" using assms(3) by auto moreover
   1.523 +    have "size t'' \<le> size l" using assms last by auto ultimately
   1.524 +    show ?thesis by simp
   1.525 +  qed
   1.526 +  
   1.527 +  from 2 obtain c l a r where 
   1.528 +    t': "t' = Node c l a r" by (cases t') auto
   1.529 +  with 2 have inv: "invc l" "invh l" "invc r" "invh r" by auto
   1.530 +  show ?case proof (cases "height r \<le> height l")
   1.531 +    case True thus ?thesis using ***[OF 2(3,4,1,2,6,7)] t' 2(5) by auto
   1.532 +  next
   1.533 +    case False 
   1.534 +    obtain t''' where t''' : "t''' = Node c r a l" "invc t'''" "invh t'''" using 2 t' by auto
   1.535 +    have "size t''' = size t'" and 4 : "Suc h = height t'''" using 2(4) t' t''' by auto
   1.536 +    thus ?thesis using ***[OF 2(3) 4 2(1,2) t'''(2,3) _ t'''(1)] 2(5) False by auto
   1.537 +  qed
   1.538 +qed
   1.539 +
   1.540 +lemma RB_size: "RB h t \<Longrightarrow> size1 t + 1 = 2^((h+1) div 2) + 2^(h div 2)"
   1.541 +by (induction h t rule: "RB.induct" ) auto
   1.542 +
   1.543 +lemma RB_exist: "\<exists> t . RB h t"
   1.544 +proof (induction h) 
   1.545 +  case (Suc n)
   1.546 +  obtain r where r: "balB (n div 2) r"  using  exist_pt by blast
   1.547 +  obtain l where l: "RB n l"  using  Suc by blast
   1.548 +  obtain t where 
   1.549 +    "color l = Red   \<Longrightarrow> t = B l () r"
   1.550 +    "color l = Black \<Longrightarrow> t = R l () r" by auto
   1.551 +  with l and r have "RB (Suc n) t" by (cases "color l") auto
   1.552 +  thus ?case by auto
   1.553 +qed auto
   1.554 +
   1.555 +lemma bound:
   1.556 +  assumes "invc t"  "invh t" and [simp]:"height t = h"
   1.557 +  shows "size t \<ge> 2^((h+1) div 2) + 2^(h div 2) - 2"
   1.558 +proof -
   1.559 +  obtain t' where t': "RB h t'" using RB_exist by auto
   1.560 +  show ?thesis using RB_size[OF t'] 
   1.561 +  RB_minimal[OF _ _ assms(1,2), simplified, OF t' RB_invh[OF t']] assms t' 
   1.562 +  unfolding  size1_def by auto
   1.563 +qed
   1.564 +
   1.565 +corollary "rbt t \<Longrightarrow> h = height t \<Longrightarrow> size t \<ge> 2^((h+1) div 2) + 2^(h div 2) - 2"
   1.566 +using bound unfolding rbt_def by blast
   1.567 +
   1.568  end