src/HOL/Data_Structures/RBT_Set.thy
author nipkow
Wed Jun 13 15:24:20 2018 +0200 (10 months ago)
changeset 68440 6826718f732d
parent 68431 b294e095f64c
child 68998 818898556504
permissions -rw-r--r--
qualify interpretations to avoid clashes
     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 definition empty :: "'a rbt" where
    14 "empty = Leaf"
    15 
    16 fun ins :: "'a::linorder \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
    17 "ins x Leaf = R Leaf x Leaf" |
    18 "ins x (B l a r) =
    19   (case cmp x a of
    20      LT \<Rightarrow> baliL (ins x l) a r |
    21      GT \<Rightarrow> baliR l a (ins x r) |
    22      EQ \<Rightarrow> B l a r)" |
    23 "ins x (R l a r) =
    24   (case cmp x a of
    25     LT \<Rightarrow> R (ins x l) a r |
    26     GT \<Rightarrow> R l a (ins x r) |
    27     EQ \<Rightarrow> R l a r)"
    28 
    29 definition insert :: "'a::linorder \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
    30 "insert x t = paint Black (ins x t)"
    31 
    32 fun color :: "'a rbt \<Rightarrow> color" where
    33 "color Leaf = Black" |
    34 "color (Node _ _ c _) = c"
    35 
    36 fun del :: "'a::linorder \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
    37 "del x Leaf = Leaf" |
    38 "del x (Node l a _ r) =
    39   (case cmp x a of
    40      LT \<Rightarrow> if l \<noteq> Leaf \<and> color l = Black
    41            then baldL (del x l) a r else R (del x l) a r |
    42      GT \<Rightarrow> if r \<noteq> Leaf\<and> color r = Black
    43            then baldR l a (del x r) else R l a (del x r) |
    44      EQ \<Rightarrow> combine l r)"
    45 
    46 definition delete :: "'a::linorder \<Rightarrow> 'a rbt \<Rightarrow> 'a rbt" where
    47 "delete x t = paint Black (del x t)"
    48 
    49 
    50 subsection "Functional Correctness Proofs"
    51 
    52 lemma inorder_paint: "inorder(paint c t) = inorder t"
    53 by(cases t) (auto)
    54 
    55 lemma inorder_baliL:
    56   "inorder(baliL l a r) = inorder l @ a # inorder r"
    57 by(cases "(l,a,r)" rule: baliL.cases) (auto)
    58 
    59 lemma inorder_baliR:
    60   "inorder(baliR l a r) = inorder l @ a # inorder r"
    61 by(cases "(l,a,r)" rule: baliR.cases) (auto)
    62 
    63 lemma inorder_ins:
    64   "sorted(inorder t) \<Longrightarrow> inorder(ins x t) = ins_list x (inorder t)"
    65 by(induction x t rule: ins.induct)
    66   (auto simp: ins_list_simps inorder_baliL inorder_baliR)
    67 
    68 lemma inorder_insert:
    69   "sorted(inorder t) \<Longrightarrow> inorder(insert x t) = ins_list x (inorder t)"
    70 by (simp add: insert_def inorder_ins inorder_paint)
    71 
    72 lemma inorder_baldL:
    73   "inorder(baldL l a r) = inorder l @ a # inorder r"
    74 by(cases "(l,a,r)" rule: baldL.cases)
    75   (auto simp:  inorder_baliL inorder_baliR inorder_paint)
    76 
    77 lemma inorder_baldR:
    78   "inorder(baldR l a r) = inorder l @ a # inorder r"
    79 by(cases "(l,a,r)" rule: baldR.cases)
    80   (auto simp:  inorder_baliL inorder_baliR inorder_paint)
    81 
    82 lemma inorder_combine:
    83   "inorder(combine l r) = inorder l @ inorder r"
    84 by(induction l r rule: combine.induct)
    85   (auto simp: inorder_baldL inorder_baldR split: tree.split color.split)
    86 
    87 lemma inorder_del:
    88  "sorted(inorder t) \<Longrightarrow>  inorder(del x t) = del_list x (inorder t)"
    89 by(induction x t rule: del.induct)
    90   (auto simp: del_list_simps inorder_combine inorder_baldL inorder_baldR)
    91 
    92 lemma inorder_delete:
    93   "sorted(inorder t) \<Longrightarrow> inorder(delete x t) = del_list x (inorder t)"
    94 by (auto simp: delete_def inorder_del inorder_paint)
    95 
    96 
    97 subsection \<open>Structural invariants\<close>
    98 
    99 text\<open>The proofs are due to Markus Reiter and Alexander Krauss.\<close>
   100 
   101 fun bheight :: "'a rbt \<Rightarrow> nat" where
   102 "bheight Leaf = 0" |
   103 "bheight (Node l x c r) = (if c = Black then bheight l + 1 else bheight l)"
   104 
   105 fun invc :: "'a rbt \<Rightarrow> bool" where
   106 "invc Leaf = True" |
   107 "invc (Node l a c r) =
   108   (invc l \<and> invc r \<and> (c = Red \<longrightarrow> color l = Black \<and> color r = Black))"
   109 
   110 fun invc2 :: "'a rbt \<Rightarrow> bool" \<comment> \<open>Weaker version\<close> where
   111 "invc2 Leaf = True" |
   112 "invc2 (Node l a c r) = (invc l \<and> invc r)"
   113 
   114 fun invh :: "'a rbt \<Rightarrow> bool" where
   115 "invh Leaf = True" |
   116 "invh (Node l x c r) = (invh l \<and> invh r \<and> bheight l = bheight r)"
   117 
   118 lemma invc2I: "invc t \<Longrightarrow> invc2 t"
   119 by (cases t) simp+
   120 
   121 definition rbt :: "'a rbt \<Rightarrow> bool" where
   122 "rbt t = (invc t \<and> invh t \<and> color t = Black)"
   123 
   124 lemma color_paint_Black: "color (paint Black t) = Black"
   125 by (cases t) auto
   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 _ y c)
   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 S: Set_by_Ordered
   260 where empty = empty 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 add: empty_def)
   264 next
   265   case 2 thus ?case by(simp add: isin_set_inorder)
   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_def empty_def) 
   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: "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: "rbt t \<Longrightarrow> height t / 2 \<le> bheight t "
   289 by(auto simp: rbt_def dest: rbt_height_bheight_if)
   290 
   291 lemma bheight_size_bound:  "invc t \<Longrightarrow> invh t \<Longrightarrow> 2 ^ (bheight t) \<le> size1 t"
   292 by (induction t) auto
   293 
   294 lemma rbt_height_le: assumes "rbt t" shows "height t \<le> 2 * log 2 (size1 t)"
   295 proof -
   296   have "2 powr (height t / 2) \<le> 2 powr bheight t"
   297     using rbt_height_bheight[OF assms] by (simp)
   298   also have "\<dots> \<le> size1 t" using assms
   299     by (simp add: powr_realpow bheight_size_bound rbt_def)
   300   finally have "2 powr (height t / 2) \<le> size1 t" .
   301   hence "height t / 2 \<le> log 2 (size1 t)"
   302     by (simp add: le_log_iff size1_def del: divide_le_eq_numeral1(1))
   303   thus ?thesis by simp
   304 qed
   305 
   306 end