src/HOL/Data_Structures/RBT_Set.thy
 author nipkow Fri Jan 27 17:35:08 2017 +0100 (2017-01-27) changeset 64953 f9cfb10761ff parent 64952 f11e974b47e0 child 64960 8be78855ee7a permissions -rw-r--r--
tuned name
```     1 (* Author: Tobias Nipkow *)
```
```     2
```
```     3 section \<open>Red-Black Tree Implementation of Sets\<close>
```
```     4
```
```     5 theory RBT_Set
```
```     6 imports
```
```     7   Complex_Main
```
```     8   RBT
```
```     9   Cmp
```
```    10   Isin2
```
```    11 begin
```
```    12
```
```    13 fun ins :: "'a::linorder \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
```
```    14 "ins x Leaf = R Leaf x Leaf" |
```
```    15 "ins x (B l a r) =
```
```    16   (case cmp x a of
```
```    17      LT \<Rightarrow> bal (ins x l) a r |
```
```    18      GT \<Rightarrow> bal l a (ins x r) |
```
```    19      EQ \<Rightarrow> B l a r)" |
```
```    20 "ins x (R l a r) =
```
```    21   (case cmp x a of
```
```    22     LT \<Rightarrow> R (ins x l) a r |
```
```    23     GT \<Rightarrow> R l a (ins x r) |
```
```    24     EQ \<Rightarrow> R l a r)"
```
```    25
```
```    26 definition insert :: "'a::linorder \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
```
```    27 "insert x t = paint Black (ins x t)"
```
```    28
```
```    29 fun del :: "'a::linorder \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt"
```
```    30 and delL :: "'a::linorder \<Rightarrow> 'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt"
```
```    31 and delR :: "'a::linorder \<Rightarrow> 'a rbt \<Rightarrow> 'a \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt"
```
```    32 where
```
```    33 "del x Leaf = Leaf" |
```
```    34 "del x (Node _ l a r) =
```
```    35   (case cmp x a of
```
```    36      LT \<Rightarrow> delL x l a r |
```
```    37      GT \<Rightarrow> delR x l a r |
```
```    38      EQ \<Rightarrow> combine l r)" |
```
```    39 "delL x (B t1 a t2) b t3 = balL (del x (B t1 a t2)) b t3" |
```
```    40 "delL x l a r = R (del x l) a r" |
```
```    41 "delR x t1 a (B t2 b t3) = balR t1 a (del x (B t2 b t3))" |
```
```    42 "delR x l a r = R l a (del x r)"
```
```    43
```
```    44 definition delete :: "'a::linorder \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
```
```    45 "delete x t = paint Black (del x t)"
```
```    46
```
```    47
```
```    48 subsection "Functional Correctness Proofs"
```
```    49
```
```    50 lemma inorder_paint: "inorder(paint c t) = inorder t"
```
```    51 by(cases t) (auto)
```
```    52
```
```    53 lemma inorder_bal:
```
```    54   "inorder(bal l a r) = inorder l @ a # inorder r"
```
```    55 by(cases "(l,a,r)" rule: bal.cases) (auto)
```
```    56
```
```    57 lemma inorder_ins:
```
```    58   "sorted(inorder t) \<Longrightarrow> inorder(ins x t) = ins_list x (inorder t)"
```
```    59 by(induction x t rule: ins.induct) (auto simp: ins_list_simps inorder_bal)
```
```    60
```
```    61 lemma inorder_insert:
```
```    62   "sorted(inorder t) \<Longrightarrow> inorder(insert x t) = ins_list x (inorder t)"
```
```    63 by (simp add: insert_def inorder_ins inorder_paint)
```
```    64
```
```    65 lemma inorder_balL:
```
```    66   "inorder(balL l a r) = inorder l @ a # inorder r"
```
```    67 by(cases "(l,a,r)" rule: balL.cases)(auto simp: inorder_bal inorder_paint)
```
```    68
```
```    69 lemma inorder_balR:
```
```    70   "inorder(balR l a r) = inorder l @ a # inorder r"
```
```    71 by(cases "(l,a,r)" rule: balR.cases) (auto simp: inorder_bal inorder_paint)
```
```    72
```
```    73 lemma inorder_combine:
```
```    74   "inorder(combine l r) = inorder l @ inorder r"
```
```    75 by(induction l r rule: combine.induct)
```
```    76   (auto simp: inorder_balL inorder_balR split: tree.split color.split)
```
```    77
```
```    78 lemma inorder_del:
```
```    79  "sorted(inorder t) \<Longrightarrow>  inorder(del x t) = del_list x (inorder t)"
```
```    80  "sorted(inorder l) \<Longrightarrow>  inorder(delL x l a r) =
```
```    81     del_list x (inorder l) @ a # inorder r"
```
```    82  "sorted(inorder r) \<Longrightarrow>  inorder(delR x l a r) =
```
```    83     inorder l @ a # del_list x (inorder r)"
```
```    84 by(induction x t and x l a r and x l a r rule: del_delL_delR.induct)
```
```    85   (auto simp: del_list_simps inorder_combine inorder_balL inorder_balR)
```
```    86
```
```    87 lemma inorder_delete:
```
```    88   "sorted(inorder t) \<Longrightarrow> inorder(delete x t) = del_list x (inorder t)"
```
```    89 by (auto simp: delete_def inorder_del inorder_paint)
```
```    90
```
```    91
```
```    92 subsection \<open>Structural invariants\<close>
```
```    93
```
```    94 text\<open>The proofs are due to Markus Reiter and Alexander Krauss.\<close>
```
```    95
```
```    96 fun color :: "'a rbt \<Rightarrow> color" where
```
```    97 "color Leaf = Black" |
```
```    98 "color (Node c _ _ _) = c"
```
```    99
```
```   100 fun bheight :: "'a rbt \<Rightarrow> nat" where
```
```   101 "bheight Leaf = 0" |
```
```   102 "bheight (Node c l x r) = (if c = Black then bheight l + 1 else bheight l)"
```
```   103
```
```   104 fun invc :: "'a rbt \<Rightarrow> bool" where
```
```   105 "invc Leaf = True" |
```
```   106 "invc (Node c l a r) =
```
```   107   (invc l \<and> invc r \<and> (c = Red \<longrightarrow> color l = Black \<and> color r = Black))"
```
```   108
```
```   109 fun invc2 :: "'a rbt \<Rightarrow> bool" \<comment> \<open>Weaker version\<close> where
```
```   110 "invc2 Leaf = True" |
```
```   111 "invc2 (Node c l a r) = (invc l \<and> invc r)"
```
```   112
```
```   113 fun invh :: "'a rbt \<Rightarrow> bool" where
```
```   114 "invh Leaf = True" |
```
```   115 "invh (Node c l x r) = (invh l \<and> invh r \<and> bheight l = bheight r)"
```
```   116
```
```   117 lemma invc2I: "invc t \<Longrightarrow> invc2 t"
```
```   118 by (cases t) simp+
```
```   119
```
```   120 definition rbt :: "'a rbt \<Rightarrow> bool" where
```
```   121 "rbt t = (invc t \<and> invh t \<and> color t = Black)"
```
```   122
```
```   123 lemma color_paint_Black: "color (paint Black t) = Black"
```
```   124 by (cases t) auto
```
```   125
```
```   126 theorem rbt_Leaf: "rbt Leaf"
```
```   127 by (simp add: rbt_def)
```
```   128
```
```   129 lemma paint_invc2: "invc2 t \<Longrightarrow> invc2 (paint c t)"
```
```   130 by (cases t) auto
```
```   131
```
```   132 lemma invc_paint_Black: "invc2 t \<Longrightarrow> invc (paint Black t)"
```
```   133 by (cases t) auto
```
```   134
```
```   135 lemma invh_paint: "invh t \<Longrightarrow> invh (paint c t)"
```
```   136 by (cases t) auto
```
```   137
```
```   138 lemma invc_bal:
```
```   139   "\<lbrakk>invc l \<and> invc2 r \<or> invc2 l \<and> invc r\<rbrakk> \<Longrightarrow> invc (bal l a r)"
```
```   140 by (induct l a r rule: bal.induct) auto
```
```   141
```
```   142 lemma bheight_bal:
```
```   143   "bheight l = bheight r \<Longrightarrow> bheight (bal l a r) = Suc (bheight l)"
```
```   144 by (induct l a r rule: bal.induct) auto
```
```   145
```
```   146 lemma invh_bal:
```
```   147   "\<lbrakk> invh l; invh r; bheight l = bheight r \<rbrakk> \<Longrightarrow> invh (bal l a r)"
```
```   148 by (induct l a r rule: bal.induct) auto
```
```   149
```
```   150
```
```   151 subsubsection \<open>Insertion\<close>
```
```   152
```
```   153 lemma invc_ins: assumes "invc t"
```
```   154   shows "color t = Black \<Longrightarrow> invc (ins x t)" "invc2 (ins x t)"
```
```   155 using assms
```
```   156 by (induct x t rule: ins.induct) (auto simp: invc_bal invc2I)
```
```   157
```
```   158 lemma invh_ins: assumes "invh t"
```
```   159   shows "invh (ins x t)" "bheight (ins x t) = bheight t"
```
```   160 using assms
```
```   161 by (induct x t rule: ins.induct) (auto simp: invh_bal bheight_bal)
```
```   162
```
```   163 theorem rbt_insert: "rbt t \<Longrightarrow> rbt (insert x t)"
```
```   164 by (simp add: invc_ins invh_ins color_paint_Black invc_paint_Black invh_paint
```
```   165   rbt_def insert_def)
```
```   166
```
```   167
```
```   168 subsubsection \<open>Deletion\<close>
```
```   169
```
```   170 lemma bheight_paint_Red:
```
```   171   "color t = Black \<Longrightarrow> bheight (paint Red t) = bheight t - 1"
```
```   172 by (cases t) auto
```
```   173
```
```   174 lemma balL_invh_with_invc:
```
```   175   assumes "invh lt" "invh rt" "bheight lt + 1 = bheight rt" "invc rt"
```
```   176   shows "bheight (balL lt a rt) = bheight lt + 1"  "invh (balL lt a rt)"
```
```   177 using assms
```
```   178 by (induct lt a rt rule: balL.induct)
```
```   179    (auto simp: invh_bal invh_paint bheight_bal bheight_paint_Red)
```
```   180
```
```   181 lemma balL_invh_app:
```
```   182   assumes "invh lt" "invh rt" "bheight lt + 1 = bheight rt" "color rt = Black"
```
```   183   shows "invh (balL lt a rt)"
```
```   184         "bheight (balL lt a rt) = bheight rt"
```
```   185 using assms
```
```   186 by (induct lt a rt rule: balL.induct) (auto simp add: invh_bal bheight_bal)
```
```   187
```
```   188 lemma balL_invc: "\<lbrakk>invc2 l; invc r; color r = Black\<rbrakk> \<Longrightarrow> invc (balL l a r)"
```
```   189 by (induct l a r rule: balL.induct) (simp_all add: invc_bal)
```
```   190
```
```   191 lemma balL_invc2: "\<lbrakk> invc2 lt; invc rt \<rbrakk> \<Longrightarrow> invc2 (balL lt a rt)"
```
```   192 by (induct lt a rt rule: balL.induct) (auto simp: invc_bal paint_invc2 invc2I)
```
```   193
```
```   194 lemma balR_invh_with_invc:
```
```   195   assumes "invh lt" "invh rt" "bheight lt = bheight rt + 1" "invc lt"
```
```   196   shows "invh (balR lt a rt) \<and> bheight (balR lt a rt) = bheight lt"
```
```   197 using assms
```
```   198 by(induct lt a rt rule: balR.induct)
```
```   199   (auto simp: invh_bal bheight_bal invh_paint bheight_paint_Red)
```
```   200
```
```   201 lemma invc_balR: "\<lbrakk>invc a; invc2 b; color a = Black\<rbrakk> \<Longrightarrow> invc (balR a x b)"
```
```   202 by (induct a x b rule: balR.induct) (simp_all add: invc_bal)
```
```   203
```
```   204 lemma invc2_balR: "\<lbrakk> invc lt; invc2 rt \<rbrakk> \<Longrightarrow>invc2 (balR lt x rt)"
```
```   205 by (induct lt x rt rule: balR.induct) (auto simp: invc_bal paint_invc2 invc2I)
```
```   206
```
```   207 lemma invh_combine:
```
```   208   assumes "invh lt" "invh rt" "bheight lt = bheight rt"
```
```   209   shows "bheight (combine lt rt) = bheight lt" "invh (combine lt rt)"
```
```   210 using assms
```
```   211 by (induct lt rt rule: combine.induct)
```
```   212    (auto simp: balL_invh_app split: tree.splits color.splits)
```
```   213
```
```   214 lemma invc_combine:
```
```   215   assumes "invc lt" "invc rt"
```
```   216   shows "color lt = Black \<Longrightarrow> color rt = Black \<Longrightarrow> invc (combine lt rt)"
```
```   217          "invc2 (combine lt rt)"
```
```   218 using assms
```
```   219 by (induct lt rt rule: combine.induct)
```
```   220    (auto simp: balL_invc invc2I split: tree.splits color.splits)
```
```   221
```
```   222
```
```   223 lemma assumes "invh lt" "invc lt"
```
```   224   shows
```
```   225   del_invc_invh: "invh (del x lt) \<and> (color lt = Red \<and> bheight (del x lt) = bheight lt \<and> invc (del x lt)
```
```   226   \<or> color lt = Black \<and> bheight (del x lt) = bheight lt - 1 \<and> invc2 (del x lt))"
```
```   227 and  "\<lbrakk>invh rt; bheight lt = bheight rt; invc rt\<rbrakk> \<Longrightarrow>
```
```   228    invh (delL x lt k rt) \<and>
```
```   229    bheight (delL x lt k rt) = bheight lt \<and>
```
```   230    (color lt = Black \<and> color rt = Black \<and> invc (delL x lt k rt) \<or>
```
```   231     (color lt \<noteq> Black \<or> color rt \<noteq> Black) \<and> invc2 (delL x lt k rt))"
```
```   232   and "\<lbrakk>invh rt; bheight lt = bheight rt; invc rt\<rbrakk> \<Longrightarrow>
```
```   233   invh (delR x lt k rt) \<and>
```
```   234   bheight (delR x lt k rt) = bheight lt \<and>
```
```   235   (color lt = Black \<and> color rt = Black \<and> invc (delR x lt k rt) \<or>
```
```   236    (color lt \<noteq> Black \<or> color rt \<noteq> Black) \<and> invc2 (delR x lt k rt))"
```
```   237 using assms
```
```   238 proof (induct x lt and x lt k rt and x lt k rt rule: del_delL_delR.induct)
```
```   239 case (2 y c _ y')
```
```   240   have "y = y' \<or> y < y' \<or> y > y'" by auto
```
```   241   thus ?case proof (elim disjE)
```
```   242     assume "y = y'"
```
```   243     with 2 show ?thesis
```
```   244     by (cases c) (simp_all add: invh_combine invc_combine)
```
```   245   next
```
```   246     assume "y < y'"
```
```   247     with 2 show ?thesis by (cases c) (auto simp: invc2I)
```
```   248   next
```
```   249     assume "y' < y"
```
```   250     with 2 show ?thesis by (cases c) (auto simp: invc2I)
```
```   251   qed
```
```   252 next
```
```   253   case (3 y lt z rta y' bb)
```
```   254   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)+
```
```   255 next
```
```   256   case (5 y a y' lt z rta)
```
```   257   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)+
```
```   258 next
```
```   259   case ("6_1" y a y') thus ?case by (cases "color a = Black \<and> color Leaf = Black") simp+
```
```   260 qed auto
```
```   261
```
```   262 theorem rbt_delete: "rbt t \<Longrightarrow> rbt (delete k t)"
```
```   263 by (metis delete_def rbt_def color_paint_Black del_invc_invh invc_paint_Black invc2I invh_paint)
```
```   264
```
```   265 text \<open>Overall correctness:\<close>
```
```   266
```
```   267 interpretation Set_by_Ordered
```
```   268 where empty = Leaf and isin = isin and insert = insert and delete = delete
```
```   269 and inorder = inorder and inv = rbt
```
```   270 proof (standard, goal_cases)
```
```   271   case 1 show ?case by simp
```
```   272 next
```
```   273   case 2 thus ?case by(simp add: isin_set)
```
```   274 next
```
```   275   case 3 thus ?case by(simp add: inorder_insert)
```
```   276 next
```
```   277   case 4 thus ?case by(simp add: inorder_delete)
```
```   278 next
```
```   279   case 5 thus ?case by (simp add: rbt_Leaf)
```
```   280 next
```
```   281   case 6 thus ?case by (simp add: rbt_insert)
```
```   282 next
```
```   283   case 7 thus ?case by (simp add: rbt_delete)
```
```   284 qed
```
```   285
```
```   286
```
```   287 subsection \<open>Height-Size Relation\<close>
```
```   288
```
```   289 lemma neq_Black[simp]: "(c \<noteq> Black) = (c = Red)"
```
```   290 by (cases c) auto
```
```   291
```
```   292 lemma rbt_height_bheight_if_nat: "invc t \<Longrightarrow> invh t \<Longrightarrow>
```
```   293   height t \<le> (if color t = Black then 2 * bheight t else 2 * bheight t + 1)"
```
```   294 by(induction t) (auto split: if_split_asm)
```
```   295
```
```   296 lemma rbt_height_bheight_if: "invc t \<Longrightarrow> invh t \<Longrightarrow>
```
```   297   (if color t = Black then height t / 2 else (height t - 1) / 2) \<le> bheight t"
```
```   298 by(induction t) (auto split: if_split_asm)
```
```   299
```
```   300 lemma rbt_height_bheight: "rbt t \<Longrightarrow> height t / 2 \<le> bheight t "
```
```   301 by(auto simp: rbt_def dest: rbt_height_bheight_if)
```
```   302
```
```   303 lemma bheight_size_bound:  "invc t \<Longrightarrow> invh t \<Longrightarrow> size1 t \<ge>  2 ^ (bheight t)"
```
```   304 by (induction t) auto
```
```   305
```
```   306 lemma rbt_height_le: assumes "rbt t" shows "height t \<le> 2 * log 2 (size1 t)"
```
```   307 proof -
```
```   308   have "2 powr (height t / 2) \<le> 2 powr bheight t"
```
```   309     using rbt_height_bheight[OF assms] by (simp)
```
```   310   also have "\<dots> \<le> size1 t" using assms
```
```   311     by (simp add: powr_realpow bheight_size_bound rbt_def)
```
```   312   finally have "2 powr (height t / 2) \<le> size1 t" .
```
```   313   hence "height t / 2 \<le> log 2 (size1 t)"
```
```   314     by(simp add: le_log_iff size1_def del: Int.divide_le_eq_numeral1(1))
```
```   315   thus ?thesis by simp
```
```   316 qed
```
```   317
```
```   318 end
```