src/HOL/Data_Structures/RBT_Set.thy
changeset 64960 8be78855ee7a
parent 64953 f9cfb10761ff
child 66087 6e0c330f4051
     1.1 --- a/src/HOL/Data_Structures/RBT_Set.thy	Fri Jan 27 22:27:03 2017 +0100
     1.2 +++ b/src/HOL/Data_Structures/RBT_Set.thy	Sat Jan 28 15:12:19 2017 +0100
     1.3 @@ -14,8 +14,8 @@
     1.4  "ins x Leaf = R Leaf x Leaf" |
     1.5  "ins x (B l a r) =
     1.6    (case cmp x a of
     1.7 -     LT \<Rightarrow> bal (ins x l) a r |
     1.8 -     GT \<Rightarrow> bal l a (ins x r) |
     1.9 +     LT \<Rightarrow> baliL (ins x l) a r |
    1.10 +     GT \<Rightarrow> baliR l a (ins x r) |
    1.11       EQ \<Rightarrow> B l a r)" |
    1.12  "ins x (R l a r) =
    1.13    (case cmp x a of
    1.14 @@ -36,9 +36,9 @@
    1.15       LT \<Rightarrow> delL x l a r |
    1.16       GT \<Rightarrow> delR x l a r |
    1.17       EQ \<Rightarrow> combine l r)" |
    1.18 -"delL x (B t1 a t2) b t3 = balL (del x (B t1 a t2)) b t3" |
    1.19 +"delL x (B t1 a t2) b t3 = baldL (del x (B t1 a t2)) b t3" |
    1.20  "delL x l a r = R (del x l) a r" |
    1.21 -"delR x t1 a (B t2 b t3) = balR t1 a (del x (B t2 b t3))" | 
    1.22 +"delR x t1 a (B t2 b t3) = baldR t1 a (del x (B t2 b t3))" | 
    1.23  "delR x l a r = R l a (del x r)"
    1.24  
    1.25  definition delete :: "'a::linorder \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
    1.26 @@ -50,30 +50,37 @@
    1.27  lemma inorder_paint: "inorder(paint c t) = inorder t"
    1.28  by(cases t) (auto)
    1.29  
    1.30 -lemma inorder_bal:
    1.31 -  "inorder(bal l a r) = inorder l @ a # inorder r"
    1.32 -by(cases "(l,a,r)" rule: bal.cases) (auto)
    1.33 +lemma inorder_baliL:
    1.34 +  "inorder(baliL l a r) = inorder l @ a # inorder r"
    1.35 +by(cases "(l,a,r)" rule: baliL.cases) (auto)
    1.36 +
    1.37 +lemma inorder_baliR:
    1.38 +  "inorder(baliR l a r) = inorder l @ a # inorder r"
    1.39 +by(cases "(l,a,r)" rule: baliR.cases) (auto)
    1.40  
    1.41  lemma inorder_ins:
    1.42    "sorted(inorder t) \<Longrightarrow> inorder(ins x t) = ins_list x (inorder t)"
    1.43 -by(induction x t rule: ins.induct) (auto simp: ins_list_simps inorder_bal)
    1.44 +by(induction x t rule: ins.induct)
    1.45 +  (auto simp: ins_list_simps inorder_baliL inorder_baliR)
    1.46  
    1.47  lemma inorder_insert:
    1.48    "sorted(inorder t) \<Longrightarrow> inorder(insert x t) = ins_list x (inorder t)"
    1.49  by (simp add: insert_def inorder_ins inorder_paint)
    1.50  
    1.51 -lemma inorder_balL:
    1.52 -  "inorder(balL l a r) = inorder l @ a # inorder r"
    1.53 -by(cases "(l,a,r)" rule: balL.cases)(auto simp: inorder_bal inorder_paint)
    1.54 +lemma inorder_baldL:
    1.55 +  "inorder(baldL l a r) = inorder l @ a # inorder r"
    1.56 +by(cases "(l,a,r)" rule: baldL.cases)
    1.57 +  (auto simp:  inorder_baliL inorder_baliR inorder_paint)
    1.58  
    1.59 -lemma inorder_balR:
    1.60 -  "inorder(balR l a r) = inorder l @ a # inorder r"
    1.61 -by(cases "(l,a,r)" rule: balR.cases) (auto simp: inorder_bal inorder_paint)
    1.62 +lemma inorder_baldR:
    1.63 +  "inorder(baldR l a r) = inorder l @ a # inorder r"
    1.64 +by(cases "(l,a,r)" rule: baldR.cases)
    1.65 +  (auto simp:  inorder_baliL inorder_baliR inorder_paint)
    1.66  
    1.67  lemma inorder_combine:
    1.68    "inorder(combine l r) = inorder l @ inorder r"
    1.69  by(induction l r rule: combine.induct)
    1.70 -  (auto simp: inorder_balL inorder_balR split: tree.split color.split)
    1.71 +  (auto simp: inorder_baldL inorder_baldR split: tree.split color.split)
    1.72  
    1.73  lemma inorder_del:
    1.74   "sorted(inorder t) \<Longrightarrow>  inorder(del x t) = del_list x (inorder t)"
    1.75 @@ -82,7 +89,7 @@
    1.76   "sorted(inorder r) \<Longrightarrow>  inorder(delR x l a r) =
    1.77      inorder l @ a # del_list x (inorder r)"
    1.78  by(induction x t and x l a r and x l a r rule: del_delL_delR.induct)
    1.79 -  (auto simp: del_list_simps inorder_combine inorder_balL inorder_balR)
    1.80 +  (auto simp: del_list_simps inorder_combine inorder_baldL inorder_baldR)
    1.81  
    1.82  lemma inorder_delete:
    1.83    "sorted(inorder t) \<Longrightarrow> inorder(delete x t) = del_list x (inorder t)"
    1.84 @@ -135,17 +142,29 @@
    1.85  lemma invh_paint: "invh t \<Longrightarrow> invh (paint c t)"
    1.86  by (cases t) auto
    1.87  
    1.88 -lemma invc_bal:
    1.89 -  "\<lbrakk>invc l \<and> invc2 r \<or> invc2 l \<and> invc r\<rbrakk> \<Longrightarrow> invc (bal l a r)" 
    1.90 -by (induct l a r rule: bal.induct) auto
    1.91 +lemma invc_baliL:
    1.92 +  "\<lbrakk>invc2 l; invc r\<rbrakk> \<Longrightarrow> invc (baliL l a r)" 
    1.93 +by (induct l a r rule: baliL.induct) auto
    1.94 +
    1.95 +lemma invc_baliR:
    1.96 +  "\<lbrakk>invc l; invc2 r\<rbrakk> \<Longrightarrow> invc (baliR l a r)" 
    1.97 +by (induct l a r rule: baliR.induct) auto
    1.98 +
    1.99 +lemma bheight_baliL:
   1.100 +  "bheight l = bheight r \<Longrightarrow> bheight (baliL l a r) = Suc (bheight l)"
   1.101 +by (induct l a r rule: baliL.induct) auto
   1.102  
   1.103 -lemma bheight_bal:
   1.104 -  "bheight l = bheight r \<Longrightarrow> bheight (bal l a r) = Suc (bheight l)"
   1.105 -by (induct l a r rule: bal.induct) auto
   1.106 +lemma bheight_baliR:
   1.107 +  "bheight l = bheight r \<Longrightarrow> bheight (baliR l a r) = Suc (bheight l)"
   1.108 +by (induct l a r rule: baliR.induct) auto
   1.109  
   1.110 -lemma invh_bal: 
   1.111 -  "\<lbrakk> invh l; invh r; bheight l = bheight r \<rbrakk> \<Longrightarrow> invh (bal l a r)"
   1.112 -by (induct l a r rule: bal.induct) auto
   1.113 +lemma invh_baliL: 
   1.114 +  "\<lbrakk> invh l; invh r; bheight l = bheight r \<rbrakk> \<Longrightarrow> invh (baliL l a r)"
   1.115 +by (induct l a r rule: baliL.induct) auto
   1.116 +
   1.117 +lemma invh_baliR: 
   1.118 +  "\<lbrakk> invh l; invh r; bheight l = bheight r \<rbrakk> \<Longrightarrow> invh (baliR l a r)"
   1.119 +by (induct l a r rule: baliR.induct) auto
   1.120  
   1.121  
   1.122  subsubsection \<open>Insertion\<close>
   1.123 @@ -153,12 +172,13 @@
   1.124  lemma invc_ins: assumes "invc t"
   1.125    shows "color t = Black \<Longrightarrow> invc (ins x t)" "invc2 (ins x t)"
   1.126  using assms
   1.127 -by (induct x t rule: ins.induct) (auto simp: invc_bal invc2I)
   1.128 +by (induct x t rule: ins.induct) (auto simp: invc_baliL invc_baliR invc2I)
   1.129  
   1.130  lemma invh_ins: assumes "invh t"
   1.131    shows "invh (ins x t)" "bheight (ins x t) = bheight t"
   1.132  using assms
   1.133 -by (induct x t rule: ins.induct) (auto simp: invh_bal bheight_bal)
   1.134 +by(induct x t rule: ins.induct)
   1.135 +  (auto simp: invh_baliL invh_baliR bheight_baliL bheight_baliR)
   1.136  
   1.137  theorem rbt_insert: "rbt t \<Longrightarrow> rbt (insert x t)"
   1.138  by (simp add: invc_ins invh_ins color_paint_Black invc_paint_Black invh_paint
   1.139 @@ -171,71 +191,72 @@
   1.140    "color t = Black \<Longrightarrow> bheight (paint Red t) = bheight t - 1"
   1.141  by (cases t) auto
   1.142  
   1.143 -lemma balL_invh_with_invc:
   1.144 -  assumes "invh lt" "invh rt" "bheight lt + 1 = bheight rt" "invc rt"
   1.145 -  shows "bheight (balL lt a rt) = bheight lt + 1"  "invh (balL lt a rt)"
   1.146 +lemma baldL_invh_with_invc:
   1.147 +  assumes "invh l" "invh r" "bheight l + 1 = bheight r" "invc r"
   1.148 +  shows "bheight (baldL l a r) = bheight l + 1"  "invh (baldL l a r)"
   1.149  using assms 
   1.150 -by (induct lt a rt rule: balL.induct)
   1.151 -   (auto simp: invh_bal invh_paint bheight_bal bheight_paint_Red)
   1.152 +by (induct l a r rule: baldL.induct)
   1.153 +   (auto simp: invh_baliR invh_paint bheight_baliR bheight_paint_Red)
   1.154  
   1.155 -lemma balL_invh_app: 
   1.156 -  assumes "invh lt" "invh rt" "bheight lt + 1 = bheight rt" "color rt = Black"
   1.157 -  shows "invh (balL lt a rt)" 
   1.158 -        "bheight (balL lt a rt) = bheight rt"
   1.159 +lemma baldL_invh_app: 
   1.160 +  assumes "invh l" "invh r" "bheight l + 1 = bheight r" "color r = Black"
   1.161 +  shows "invh (baldL l a r)" 
   1.162 +        "bheight (baldL l a r) = bheight r"
   1.163  using assms 
   1.164 -by (induct lt a rt rule: balL.induct) (auto simp add: invh_bal bheight_bal) 
   1.165 +by (induct l a r rule: baldL.induct) (auto simp add: invh_baliR bheight_baliR) 
   1.166  
   1.167 -lemma balL_invc: "\<lbrakk>invc2 l; invc r; color r = Black\<rbrakk> \<Longrightarrow> invc (balL l a r)"
   1.168 -by (induct l a r rule: balL.induct) (simp_all add: invc_bal)
   1.169 +lemma baldL_invc: "\<lbrakk>invc2 l; invc r; color r = Black\<rbrakk> \<Longrightarrow> invc (baldL l a r)"
   1.170 +by (induct l a r rule: baldL.induct) (simp_all add: invc_baliR)
   1.171  
   1.172 -lemma balL_invc2: "\<lbrakk> invc2 lt; invc rt \<rbrakk> \<Longrightarrow> invc2 (balL lt a rt)"
   1.173 -by (induct lt a rt rule: balL.induct) (auto simp: invc_bal paint_invc2 invc2I)
   1.174 +lemma baldL_invc2: "\<lbrakk> invc2 l; invc r \<rbrakk> \<Longrightarrow> invc2 (baldL l a r)"
   1.175 +by (induct l a r rule: baldL.induct) (auto simp: invc_baliR paint_invc2 invc2I)
   1.176  
   1.177 -lemma balR_invh_with_invc:
   1.178 -  assumes "invh lt" "invh rt" "bheight lt = bheight rt + 1" "invc lt"
   1.179 -  shows "invh (balR lt a rt) \<and> bheight (balR lt a rt) = bheight lt"
   1.180 +lemma baldR_invh_with_invc:
   1.181 +  assumes "invh l" "invh r" "bheight l = bheight r + 1" "invc l"
   1.182 +  shows "invh (baldR l a r) \<and> bheight (baldR l a r) = bheight l"
   1.183  using assms
   1.184 -by(induct lt a rt rule: balR.induct)
   1.185 -  (auto simp: invh_bal bheight_bal invh_paint bheight_paint_Red)
   1.186 +by(induct l a r rule: baldR.induct)
   1.187 +  (auto simp: invh_baliL bheight_baliL invh_paint bheight_paint_Red)
   1.188  
   1.189 -lemma invc_balR: "\<lbrakk>invc a; invc2 b; color a = Black\<rbrakk> \<Longrightarrow> invc (balR a x b)"
   1.190 -by (induct a x b rule: balR.induct) (simp_all add: invc_bal)
   1.191 +lemma invc_baldR: "\<lbrakk>invc a; invc2 b; color a = Black\<rbrakk> \<Longrightarrow> invc (baldR a x b)"
   1.192 +by (induct a x b rule: baldR.induct) (simp_all add: invc_baliL)
   1.193  
   1.194 -lemma invc2_balR: "\<lbrakk> invc lt; invc2 rt \<rbrakk> \<Longrightarrow>invc2 (balR lt x rt)"
   1.195 -by (induct lt x rt rule: balR.induct) (auto simp: invc_bal paint_invc2 invc2I)
   1.196 +lemma invc2_baldR: "\<lbrakk> invc l; invc2 r \<rbrakk> \<Longrightarrow>invc2 (baldR l x r)"
   1.197 +by (induct l x r rule: baldR.induct) (auto simp: invc_baliL paint_invc2 invc2I)
   1.198  
   1.199  lemma invh_combine:
   1.200 -  assumes "invh lt" "invh rt" "bheight lt = bheight rt"
   1.201 -  shows "bheight (combine lt rt) = bheight lt" "invh (combine lt rt)"
   1.202 +  assumes "invh l" "invh r" "bheight l = bheight r"
   1.203 +  shows "bheight (combine l r) = bheight l" "invh (combine l r)"
   1.204  using assms 
   1.205 -by (induct lt rt rule: combine.induct) 
   1.206 -   (auto simp: balL_invh_app split: tree.splits color.splits)
   1.207 +by (induct l r rule: combine.induct) 
   1.208 +   (auto simp: baldL_invh_app split: tree.splits color.splits)
   1.209  
   1.210  lemma invc_combine: 
   1.211 -  assumes "invc lt" "invc rt"
   1.212 -  shows "color lt = Black \<Longrightarrow> color rt = Black \<Longrightarrow> invc (combine lt rt)"
   1.213 -         "invc2 (combine lt rt)"
   1.214 +  assumes "invc l" "invc r"
   1.215 +  shows "color l = Black \<Longrightarrow> color r = Black \<Longrightarrow> invc (combine l r)"
   1.216 +         "invc2 (combine l r)"
   1.217  using assms 
   1.218 -by (induct lt rt rule: combine.induct)
   1.219 -   (auto simp: balL_invc invc2I split: tree.splits color.splits)
   1.220 +by (induct l r rule: combine.induct)
   1.221 +   (auto simp: baldL_invc invc2I split: tree.splits color.splits)
   1.222  
   1.223  
   1.224 -lemma assumes "invh lt" "invc lt"
   1.225 -  shows
   1.226 -  del_invc_invh: "invh (del x lt) \<and> (color lt = Red \<and> bheight (del x lt) = bheight lt \<and> invc (del x lt) 
   1.227 -  \<or> color lt = Black \<and> bheight (del x lt) = bheight lt - 1 \<and> invc2 (del x lt))"
   1.228 -and  "\<lbrakk>invh rt; bheight lt = bheight rt; invc rt\<rbrakk> \<Longrightarrow>
   1.229 -   invh (delL x lt k rt) \<and> 
   1.230 -   bheight (delL x lt k rt) = bheight lt \<and> 
   1.231 -   (color lt = Black \<and> color rt = Black \<and> invc (delL x lt k rt) \<or> 
   1.232 -    (color lt \<noteq> Black \<or> color rt \<noteq> Black) \<and> invc2 (delL x lt k rt))"
   1.233 -  and "\<lbrakk>invh rt; bheight lt = bheight rt; invc rt\<rbrakk> \<Longrightarrow>
   1.234 -  invh (delR x lt k rt) \<and> 
   1.235 -  bheight (delR x lt k rt) = bheight lt \<and> 
   1.236 -  (color lt = Black \<and> color rt = Black \<and> invc (delR x lt k rt) \<or> 
   1.237 -   (color lt \<noteq> Black \<or> color rt \<noteq> Black) \<and> invc2 (delR x lt k rt))"
   1.238 +lemma assumes "invh l" "invc l"
   1.239 +  shows del_invc_invh:
   1.240 +   "invh (del x l) \<and>
   1.241 +   (color l = Red \<and> bheight (del x l) = bheight l \<and> invc (del x l) \<or>
   1.242 +    color l = Black \<and> bheight (del x l) = bheight l - 1 \<and> invc2 (del x l))"
   1.243 +and  "\<lbrakk>invh r; bheight l = bheight r; invc r\<rbrakk> \<Longrightarrow>
   1.244 +   invh (delL x l k r) \<and> 
   1.245 +   bheight (delL x l k r) = bheight l \<and> 
   1.246 +   (color l = Black \<and> color r = Black \<and> invc (delL x l k r) \<or> 
   1.247 +    (color l \<noteq> Black \<or> color r \<noteq> Black) \<and> invc2 (delL x l k r))"
   1.248 +  and "\<lbrakk>invh r; bheight l = bheight r; invc r\<rbrakk> \<Longrightarrow>
   1.249 +  invh (delR x l k r) \<and> 
   1.250 +  bheight (delR x l k r) = bheight l \<and> 
   1.251 +  (color l = Black \<and> color r = Black \<and> invc (delR x l k r) \<or> 
   1.252 +   (color l \<noteq> Black \<or> color r \<noteq> Black) \<and> invc2 (delR x l k r))"
   1.253  using assms
   1.254 -proof (induct x lt and x lt k rt and x lt k rt rule: del_delL_delR.induct)
   1.255 +proof (induct x l and x l k r and x l k r rule: del_delL_delR.induct)
   1.256  case (2 y c _ y')
   1.257    have "y = y' \<or> y < y' \<or> y > y'" by auto
   1.258    thus ?case proof (elim disjE)
   1.259 @@ -250,11 +271,11 @@
   1.260      with 2 show ?thesis by (cases c) (auto simp: invc2I)
   1.261    qed
   1.262  next
   1.263 -  case (3 y lt z rta y' bb)
   1.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)+
   1.265 +  case (3 y l z ra y' bb)
   1.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)+
   1.267  next
   1.268 -  case (5 y a y' lt z rta)
   1.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)+
   1.270 +  case (5 y a y' l z ra)
   1.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)+
   1.272  next
   1.273    case ("6_1" y a y') thus ?case by (cases "color a = Black \<and> color Leaf = Black") simp+
   1.274  qed auto