src/HOL/Data_Structures/RBT_Set.thy
 author haftmann Sat Dec 02 16:50:53 2017 +0000 (18 months ago) changeset 67118 ccab07d1196c parent 66088 c9c9438cfc0f child 67963 9541f2c5ce8d permissions -rw-r--r--
more simplification rules
```     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> baliL (ins x l) a r |
```
```    18      GT \<Rightarrow> baliR 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 color :: "'a rbt \<Rightarrow> color" where
```
```    30 "color Leaf = Black" |
```
```    31 "color (Node c _ _ _) = c"
```
```    32
```
```    33 fun del :: "'a::linorder \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
```
```    34 "del x Leaf = Leaf" |
```
```    35 "del x (Node _ l a r) =
```
```    36   (case cmp x a of
```
```    37      LT \<Rightarrow> if l \<noteq> Leaf \<and> color l = Black
```
```    38            then baldL (del x l) a r else R (del x l) a r |
```
```    39      GT \<Rightarrow> if r \<noteq> Leaf\<and> color r = Black
```
```    40            then baldR l a (del x r) else R l a (del x r) |
```
```    41      EQ \<Rightarrow> combine l r)"
```
```    42
```
```    43 definition delete :: "'a::linorder \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
```
```    44 "delete x t = paint Black (del x t)"
```
```    45
```
```    46
```
```    47 subsection "Functional Correctness Proofs"
```
```    48
```
```    49 lemma inorder_paint: "inorder(paint c t) = inorder t"
```
```    50 by(cases t) (auto)
```
```    51
```
```    52 lemma inorder_baliL:
```
```    53   "inorder(baliL l a r) = inorder l @ a # inorder r"
```
```    54 by(cases "(l,a,r)" rule: baliL.cases) (auto)
```
```    55
```
```    56 lemma inorder_baliR:
```
```    57   "inorder(baliR l a r) = inorder l @ a # inorder r"
```
```    58 by(cases "(l,a,r)" rule: baliR.cases) (auto)
```
```    59
```
```    60 lemma inorder_ins:
```
```    61   "sorted(inorder t) \<Longrightarrow> inorder(ins x t) = ins_list x (inorder t)"
```
```    62 by(induction x t rule: ins.induct)
```
```    63   (auto simp: ins_list_simps inorder_baliL inorder_baliR)
```
```    64
```
```    65 lemma inorder_insert:
```
```    66   "sorted(inorder t) \<Longrightarrow> inorder(insert x t) = ins_list x (inorder t)"
```
```    67 by (simp add: insert_def inorder_ins inorder_paint)
```
```    68
```
```    69 lemma inorder_baldL:
```
```    70   "inorder(baldL l a r) = inorder l @ a # inorder r"
```
```    71 by(cases "(l,a,r)" rule: baldL.cases)
```
```    72   (auto simp:  inorder_baliL inorder_baliR inorder_paint)
```
```    73
```
```    74 lemma inorder_baldR:
```
```    75   "inorder(baldR l a r) = inorder l @ a # inorder r"
```
```    76 by(cases "(l,a,r)" rule: baldR.cases)
```
```    77   (auto simp:  inorder_baliL inorder_baliR inorder_paint)
```
```    78
```
```    79 lemma inorder_combine:
```
```    80   "inorder(combine l r) = inorder l @ inorder r"
```
```    81 by(induction l r rule: combine.induct)
```
```    82   (auto simp: inorder_baldL inorder_baldR split: tree.split color.split)
```
```    83
```
```    84 lemma inorder_del:
```
```    85  "sorted(inorder t) \<Longrightarrow>  inorder(del x t) = del_list x (inorder t)"
```
```    86 by(induction x t rule: del.induct)
```
```    87   (auto simp: del_list_simps inorder_combine inorder_baldL inorder_baldR)
```
```    88
```
```    89 lemma inorder_delete:
```
```    90   "sorted(inorder t) \<Longrightarrow> inorder(delete x t) = del_list x (inorder t)"
```
```    91 by (auto simp: delete_def inorder_del inorder_paint)
```
```    92
```
```    93
```
```    94 subsection \<open>Structural invariants\<close>
```
```    95
```
```    96 text\<open>The proofs are due to Markus Reiter and Alexander Krauss.\<close>
```
```    97
```
```    98 fun bheight :: "'a rbt \<Rightarrow> nat" where
```
```    99 "bheight Leaf = 0" |
```
```   100 "bheight (Node c l x r) = (if c = Black then bheight l + 1 else bheight l)"
```
```   101
```
```   102 fun invc :: "'a rbt \<Rightarrow> bool" where
```
```   103 "invc Leaf = True" |
```
```   104 "invc (Node c l a r) =
```
```   105   (invc l \<and> invc r \<and> (c = Red \<longrightarrow> color l = Black \<and> color r = Black))"
```
```   106
```
```   107 fun invc2 :: "'a rbt \<Rightarrow> bool" \<comment> \<open>Weaker version\<close> where
```
```   108 "invc2 Leaf = True" |
```
```   109 "invc2 (Node c l a r) = (invc l \<and> invc r)"
```
```   110
```
```   111 fun invh :: "'a rbt \<Rightarrow> bool" where
```
```   112 "invh Leaf = True" |
```
```   113 "invh (Node c l x r) = (invh l \<and> invh r \<and> bheight l = bheight r)"
```
```   114
```
```   115 lemma invc2I: "invc t \<Longrightarrow> invc2 t"
```
```   116 by (cases t) simp+
```
```   117
```
```   118 definition rbt :: "'a rbt \<Rightarrow> bool" where
```
```   119 "rbt t = (invc t \<and> invh t \<and> color t = Black)"
```
```   120
```
```   121 lemma color_paint_Black: "color (paint Black t) = Black"
```
```   122 by (cases t) auto
```
```   123
```
```   124 theorem rbt_Leaf: "rbt Leaf"
```
```   125 by (simp add: rbt_def)
```
```   126
```
```   127 lemma paint_invc2: "invc2 t \<Longrightarrow> invc2 (paint c t)"
```
```   128 by (cases t) auto
```
```   129
```
```   130 lemma invc_paint_Black: "invc2 t \<Longrightarrow> invc (paint Black t)"
```
```   131 by (cases t) auto
```
```   132
```
```   133 lemma invh_paint: "invh t \<Longrightarrow> invh (paint c t)"
```
```   134 by (cases t) auto
```
```   135
```
```   136 lemma invc_baliL:
```
```   137   "\<lbrakk>invc2 l; invc r\<rbrakk> \<Longrightarrow> invc (baliL l a r)"
```
```   138 by (induct l a r rule: baliL.induct) auto
```
```   139
```
```   140 lemma invc_baliR:
```
```   141   "\<lbrakk>invc l; invc2 r\<rbrakk> \<Longrightarrow> invc (baliR l a r)"
```
```   142 by (induct l a r rule: baliR.induct) auto
```
```   143
```
```   144 lemma bheight_baliL:
```
```   145   "bheight l = bheight r \<Longrightarrow> bheight (baliL l a r) = Suc (bheight l)"
```
```   146 by (induct l a r rule: baliL.induct) auto
```
```   147
```
```   148 lemma bheight_baliR:
```
```   149   "bheight l = bheight r \<Longrightarrow> bheight (baliR l a r) = Suc (bheight l)"
```
```   150 by (induct l a r rule: baliR.induct) auto
```
```   151
```
```   152 lemma invh_baliL:
```
```   153   "\<lbrakk> invh l; invh r; bheight l = bheight r \<rbrakk> \<Longrightarrow> invh (baliL l a r)"
```
```   154 by (induct l a r rule: baliL.induct) auto
```
```   155
```
```   156 lemma invh_baliR:
```
```   157   "\<lbrakk> invh l; invh r; bheight l = bheight r \<rbrakk> \<Longrightarrow> invh (baliR l a r)"
```
```   158 by (induct l a r rule: baliR.induct) auto
```
```   159
```
```   160
```
```   161 subsubsection \<open>Insertion\<close>
```
```   162
```
```   163 lemma invc_ins: assumes "invc t"
```
```   164   shows "color t = Black \<Longrightarrow> invc (ins x t)" "invc2 (ins x t)"
```
```   165 using assms
```
```   166 by (induct x t rule: ins.induct) (auto simp: invc_baliL invc_baliR invc2I)
```
```   167
```
```   168 lemma invh_ins: assumes "invh t"
```
```   169   shows "invh (ins x t)" "bheight (ins x t) = bheight t"
```
```   170 using assms
```
```   171 by(induct x t rule: ins.induct)
```
```   172   (auto simp: invh_baliL invh_baliR bheight_baliL bheight_baliR)
```
```   173
```
```   174 theorem rbt_insert: "rbt t \<Longrightarrow> rbt (insert x t)"
```
```   175 by (simp add: invc_ins(2) invh_ins(1) color_paint_Black invc_paint_Black invh_paint
```
```   176   rbt_def insert_def)
```
```   177
```
```   178
```
```   179 subsubsection \<open>Deletion\<close>
```
```   180
```
```   181 lemma bheight_paint_Red:
```
```   182   "color t = Black \<Longrightarrow> bheight (paint Red t) = bheight t - 1"
```
```   183 by (cases t) auto
```
```   184
```
```   185 lemma invh_baldL_invc:
```
```   186   "\<lbrakk> invh l;  invh r;  bheight l + 1 = bheight r;  invc r \<rbrakk>
```
```   187    \<Longrightarrow> invh (baldL l a r) \<and> bheight (baldL l a r) = bheight l + 1"
```
```   188 by (induct l a r rule: baldL.induct)
```
```   189    (auto simp: invh_baliR invh_paint bheight_baliR bheight_paint_Red)
```
```   190
```
```   191 lemma invh_baldL_Black:
```
```   192   "\<lbrakk> invh l;  invh r;  bheight l + 1 = bheight r;  color r = Black \<rbrakk>
```
```   193    \<Longrightarrow> invh (baldL l a r) \<and> bheight (baldL l a r) = bheight r"
```
```   194 by (induct l a r rule: baldL.induct) (auto simp add: invh_baliR bheight_baliR)
```
```   195
```
```   196 lemma invc_baldL: "\<lbrakk>invc2 l; invc r; color r = Black\<rbrakk> \<Longrightarrow> invc (baldL l a r)"
```
```   197 by (induct l a r rule: baldL.induct) (simp_all add: invc_baliR)
```
```   198
```
```   199 lemma invc2_baldL: "\<lbrakk> invc2 l; invc r \<rbrakk> \<Longrightarrow> invc2 (baldL l a r)"
```
```   200 by (induct l a r rule: baldL.induct) (auto simp: invc_baliR paint_invc2 invc2I)
```
```   201
```
```   202 lemma invh_baldR_invc:
```
```   203   "\<lbrakk> invh l;  invh r;  bheight l = bheight r + 1;  invc l \<rbrakk>
```
```   204   \<Longrightarrow> invh (baldR l a r) \<and> bheight (baldR l a r) = bheight l"
```
```   205 by(induct l a r rule: baldR.induct)
```
```   206   (auto simp: invh_baliL bheight_baliL invh_paint bheight_paint_Red)
```
```   207
```
```   208 lemma invc_baldR: "\<lbrakk>invc a; invc2 b; color a = Black\<rbrakk> \<Longrightarrow> invc (baldR a x b)"
```
```   209 by (induct a x b rule: baldR.induct) (simp_all add: invc_baliL)
```
```   210
```
```   211 lemma invc2_baldR: "\<lbrakk> invc l; invc2 r \<rbrakk> \<Longrightarrow>invc2 (baldR l x r)"
```
```   212 by (induct l x r rule: baldR.induct) (auto simp: invc_baliL paint_invc2 invc2I)
```
```   213
```
```   214 lemma invh_combine:
```
```   215   "\<lbrakk> invh l; invh r; bheight l = bheight r \<rbrakk>
```
```   216   \<Longrightarrow> invh (combine l r) \<and> bheight (combine l r) = bheight l"
```
```   217 by (induct l r rule: combine.induct)
```
```   218    (auto simp: invh_baldL_Black split: tree.splits color.splits)
```
```   219
```
```   220 lemma invc_combine:
```
```   221   assumes "invc l" "invc r"
```
```   222   shows "color l = Black \<Longrightarrow> color r = Black \<Longrightarrow> invc (combine l r)"
```
```   223          "invc2 (combine l r)"
```
```   224 using assms
```
```   225 by (induct l r rule: combine.induct)
```
```   226    (auto simp: invc_baldL invc2I split: tree.splits color.splits)
```
```   227
```
```   228 lemma neq_LeafD: "t \<noteq> Leaf \<Longrightarrow> \<exists>c l x r. t = Node c l x r"
```
```   229 by(cases t) auto
```
```   230
```
```   231 lemma del_invc_invh: "invh t \<Longrightarrow> invc t \<Longrightarrow> invh (del x t) \<and>
```
```   232    (color t = Red \<and> bheight (del x t) = bheight t \<and> invc (del x t) \<or>
```
```   233     color t = Black \<and> bheight (del x t) = bheight t - 1 \<and> invc2 (del x t))"
```
```   234 proof (induct x t rule: del.induct)
```
```   235 case (2 x c _ y)
```
```   236   have "x = y \<or> x < y \<or> x > y" by auto
```
```   237   thus ?case proof (elim disjE)
```
```   238     assume "x = y"
```
```   239     with 2 show ?thesis
```
```   240     by (cases c) (simp_all add: invh_combine invc_combine)
```
```   241   next
```
```   242     assume "x < y"
```
```   243     with 2 show ?thesis
```
```   244       by(cases c)
```
```   245         (auto simp: invh_baldL_invc invc_baldL invc2_baldL dest: neq_LeafD)
```
```   246   next
```
```   247     assume "y < x"
```
```   248     with 2 show ?thesis
```
```   249       by(cases c)
```
```   250         (auto simp: invh_baldR_invc invc_baldR invc2_baldR dest: neq_LeafD)
```
```   251   qed
```
```   252 qed auto
```
```   253
```
```   254 theorem rbt_delete: "rbt t \<Longrightarrow> rbt (delete k t)"
```
```   255 by (metis delete_def rbt_def color_paint_Black del_invc_invh invc_paint_Black invc2I invh_paint)
```
```   256
```
```   257 text \<open>Overall correctness:\<close>
```
```   258
```
```   259 interpretation Set_by_Ordered
```
```   260 where empty = Leaf and isin = isin and insert = insert and delete = delete
```
```   261 and inorder = inorder and inv = rbt
```
```   262 proof (standard, goal_cases)
```
```   263   case 1 show ?case by simp
```
```   264 next
```
```   265   case 2 thus ?case by(simp add: isin_set)
```
```   266 next
```
```   267   case 3 thus ?case by(simp add: inorder_insert)
```
```   268 next
```
```   269   case 4 thus ?case by(simp add: inorder_delete)
```
```   270 next
```
```   271   case 5 thus ?case by (simp add: rbt_Leaf)
```
```   272 next
```
```   273   case 6 thus ?case by (simp add: rbt_insert)
```
```   274 next
```
```   275   case 7 thus ?case by (simp add: rbt_delete)
```
```   276 qed
```
```   277
```
```   278
```
```   279 subsection \<open>Height-Size Relation\<close>
```
```   280
```
```   281 lemma neq_Black[simp]: "(c \<noteq> Black) = (c = Red)"
```
```   282 by (cases c) auto
```
```   283
```
```   284 lemma rbt_height_bheight_if_nat: "invc t \<Longrightarrow> invh t \<Longrightarrow>
```
```   285   height t \<le> (if color t = Black then 2 * bheight t else 2 * bheight t + 1)"
```
```   286 by(induction t) (auto split: if_split_asm)
```
```   287
```
```   288 lemma rbt_height_bheight_if: "invc t \<Longrightarrow> invh t \<Longrightarrow>
```
```   289   (if color t = Black then height t / 2 else (height t - 1) / 2) \<le> bheight t"
```
```   290 by(induction t) (auto split: if_split_asm)
```
```   291
```
```   292 lemma rbt_height_bheight: "rbt t \<Longrightarrow> height t / 2 \<le> bheight t "
```
```   293 by(auto simp: rbt_def dest: rbt_height_bheight_if)
```
```   294
```
```   295 lemma bheight_size_bound:  "invc t \<Longrightarrow> invh t \<Longrightarrow> size1 t \<ge>  2 ^ (bheight t)"
```
```   296 by (induction t) auto
```
```   297
```
```   298 lemma rbt_height_le: assumes "rbt t" shows "height t \<le> 2 * log 2 (size1 t)"
```
```   299 proof -
```
```   300   have "2 powr (height t / 2) \<le> 2 powr bheight t"
```
```   301     using rbt_height_bheight[OF assms] by (simp)
```
```   302   also have "\<dots> \<le> size1 t" using assms
```
```   303     by (simp add: powr_realpow bheight_size_bound rbt_def)
```
```   304   finally have "2 powr (height t / 2) \<le> size1 t" .
```
```   305   hence "height t / 2 \<le> log 2 (size1 t)"
```
```   306     by (simp add: le_log_iff size1_def del: divide_le_eq_numeral1(1))
```
```   307   thus ?thesis by simp
```
```   308 qed
```
```   309
```
```   310 end
```