src/HOL/Data_Structures/RBT_Set.thy
author nipkow
Sat Jan 28 15:12:19 2017 +0100 (2017-01-28)
changeset 64960 8be78855ee7a
parent 64953 f9cfb10761ff
child 66087 6e0c330f4051
permissions -rw-r--r--
split balance into two, clearer etc
     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 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 = baldL (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) = baldR 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_baliL:
    54   "inorder(baliL l a r) = inorder l @ a # inorder r"
    55 by(cases "(l,a,r)" rule: baliL.cases) (auto)
    56 
    57 lemma inorder_baliR:
    58   "inorder(baliR l a r) = inorder l @ a # inorder r"
    59 by(cases "(l,a,r)" rule: baliR.cases) (auto)
    60 
    61 lemma inorder_ins:
    62   "sorted(inorder t) \<Longrightarrow> inorder(ins x t) = ins_list x (inorder t)"
    63 by(induction x t rule: ins.induct)
    64   (auto simp: ins_list_simps inorder_baliL inorder_baliR)
    65 
    66 lemma inorder_insert:
    67   "sorted(inorder t) \<Longrightarrow> inorder(insert x t) = ins_list x (inorder t)"
    68 by (simp add: insert_def inorder_ins inorder_paint)
    69 
    70 lemma inorder_baldL:
    71   "inorder(baldL l a r) = inorder l @ a # inorder r"
    72 by(cases "(l,a,r)" rule: baldL.cases)
    73   (auto simp:  inorder_baliL inorder_baliR inorder_paint)
    74 
    75 lemma inorder_baldR:
    76   "inorder(baldR l a r) = inorder l @ a # inorder r"
    77 by(cases "(l,a,r)" rule: baldR.cases)
    78   (auto simp:  inorder_baliL inorder_baliR inorder_paint)
    79 
    80 lemma inorder_combine:
    81   "inorder(combine l r) = inorder l @ inorder r"
    82 by(induction l r rule: combine.induct)
    83   (auto simp: inorder_baldL inorder_baldR split: tree.split color.split)
    84 
    85 lemma inorder_del:
    86  "sorted(inorder t) \<Longrightarrow>  inorder(del x t) = del_list x (inorder t)"
    87  "sorted(inorder l) \<Longrightarrow>  inorder(delL x l a r) =
    88     del_list x (inorder l) @ a # inorder r"
    89  "sorted(inorder r) \<Longrightarrow>  inorder(delR x l a r) =
    90     inorder l @ a # del_list x (inorder r)"
    91 by(induction x t and x l a r and x l a r rule: del_delL_delR.induct)
    92   (auto simp: del_list_simps inorder_combine inorder_baldL inorder_baldR)
    93 
    94 lemma inorder_delete:
    95   "sorted(inorder t) \<Longrightarrow> inorder(delete x t) = del_list x (inorder t)"
    96 by (auto simp: delete_def inorder_del inorder_paint)
    97 
    98 
    99 subsection \<open>Structural invariants\<close>
   100 
   101 text\<open>The proofs are due to Markus Reiter and Alexander Krauss.\<close>
   102 
   103 fun color :: "'a rbt \<Rightarrow> color" where
   104 "color Leaf = Black" |
   105 "color (Node c _ _ _) = c"
   106 
   107 fun bheight :: "'a rbt \<Rightarrow> nat" where
   108 "bheight Leaf = 0" |
   109 "bheight (Node c l x r) = (if c = Black then bheight l + 1 else bheight l)"
   110 
   111 fun invc :: "'a rbt \<Rightarrow> bool" where
   112 "invc Leaf = True" |
   113 "invc (Node c l a r) =
   114   (invc l \<and> invc r \<and> (c = Red \<longrightarrow> color l = Black \<and> color r = Black))"
   115 
   116 fun invc2 :: "'a rbt \<Rightarrow> bool" \<comment> \<open>Weaker version\<close> where
   117 "invc2 Leaf = True" |
   118 "invc2 (Node c l a r) = (invc l \<and> invc r)"
   119 
   120 fun invh :: "'a rbt \<Rightarrow> bool" where
   121 "invh Leaf = True" |
   122 "invh (Node c l x r) = (invh l \<and> invh r \<and> bheight l = bheight r)"
   123 
   124 lemma invc2I: "invc t \<Longrightarrow> invc2 t"
   125 by (cases t) simp+
   126 
   127 definition rbt :: "'a rbt \<Rightarrow> bool" where
   128 "rbt t = (invc t \<and> invh t \<and> color t = Black)"
   129 
   130 lemma color_paint_Black: "color (paint Black t) = Black"
   131 by (cases t) auto
   132 
   133 theorem rbt_Leaf: "rbt Leaf"
   134 by (simp add: rbt_def)
   135 
   136 lemma paint_invc2: "invc2 t \<Longrightarrow> invc2 (paint c t)"
   137 by (cases t) auto
   138 
   139 lemma invc_paint_Black: "invc2 t \<Longrightarrow> invc (paint Black t)"
   140 by (cases t) auto
   141 
   142 lemma invh_paint: "invh t \<Longrightarrow> invh (paint c t)"
   143 by (cases t) auto
   144 
   145 lemma invc_baliL:
   146   "\<lbrakk>invc2 l; invc r\<rbrakk> \<Longrightarrow> invc (baliL l a r)" 
   147 by (induct l a r rule: baliL.induct) auto
   148 
   149 lemma invc_baliR:
   150   "\<lbrakk>invc l; invc2 r\<rbrakk> \<Longrightarrow> invc (baliR l a r)" 
   151 by (induct l a r rule: baliR.induct) auto
   152 
   153 lemma bheight_baliL:
   154   "bheight l = bheight r \<Longrightarrow> bheight (baliL l a r) = Suc (bheight l)"
   155 by (induct l a r rule: baliL.induct) auto
   156 
   157 lemma bheight_baliR:
   158   "bheight l = bheight r \<Longrightarrow> bheight (baliR l a r) = Suc (bheight l)"
   159 by (induct l a r rule: baliR.induct) auto
   160 
   161 lemma invh_baliL: 
   162   "\<lbrakk> invh l; invh r; bheight l = bheight r \<rbrakk> \<Longrightarrow> invh (baliL l a r)"
   163 by (induct l a r rule: baliL.induct) auto
   164 
   165 lemma invh_baliR: 
   166   "\<lbrakk> invh l; invh r; bheight l = bheight r \<rbrakk> \<Longrightarrow> invh (baliR l a r)"
   167 by (induct l a r rule: baliR.induct) auto
   168 
   169 
   170 subsubsection \<open>Insertion\<close>
   171 
   172 lemma invc_ins: assumes "invc t"
   173   shows "color t = Black \<Longrightarrow> invc (ins x t)" "invc2 (ins x t)"
   174 using assms
   175 by (induct x t rule: ins.induct) (auto simp: invc_baliL invc_baliR invc2I)
   176 
   177 lemma invh_ins: assumes "invh t"
   178   shows "invh (ins x t)" "bheight (ins x t) = bheight t"
   179 using assms
   180 by(induct x t rule: ins.induct)
   181   (auto simp: invh_baliL invh_baliR bheight_baliL bheight_baliR)
   182 
   183 theorem rbt_insert: "rbt t \<Longrightarrow> rbt (insert x t)"
   184 by (simp add: invc_ins invh_ins color_paint_Black invc_paint_Black invh_paint
   185   rbt_def insert_def)
   186 
   187 
   188 subsubsection \<open>Deletion\<close>
   189 
   190 lemma bheight_paint_Red:
   191   "color t = Black \<Longrightarrow> bheight (paint Red t) = bheight t - 1"
   192 by (cases t) auto
   193 
   194 lemma baldL_invh_with_invc:
   195   assumes "invh l" "invh r" "bheight l + 1 = bheight r" "invc r"
   196   shows "bheight (baldL l a r) = bheight l + 1"  "invh (baldL l a r)"
   197 using assms 
   198 by (induct l a r rule: baldL.induct)
   199    (auto simp: invh_baliR invh_paint bheight_baliR bheight_paint_Red)
   200 
   201 lemma baldL_invh_app: 
   202   assumes "invh l" "invh r" "bheight l + 1 = bheight r" "color r = Black"
   203   shows "invh (baldL l a r)" 
   204         "bheight (baldL l a r) = bheight r"
   205 using assms 
   206 by (induct l a r rule: baldL.induct) (auto simp add: invh_baliR bheight_baliR) 
   207 
   208 lemma baldL_invc: "\<lbrakk>invc2 l; invc r; color r = Black\<rbrakk> \<Longrightarrow> invc (baldL l a r)"
   209 by (induct l a r rule: baldL.induct) (simp_all add: invc_baliR)
   210 
   211 lemma baldL_invc2: "\<lbrakk> invc2 l; invc r \<rbrakk> \<Longrightarrow> invc2 (baldL l a r)"
   212 by (induct l a r rule: baldL.induct) (auto simp: invc_baliR paint_invc2 invc2I)
   213 
   214 lemma baldR_invh_with_invc:
   215   assumes "invh l" "invh r" "bheight l = bheight r + 1" "invc l"
   216   shows "invh (baldR l a r) \<and> bheight (baldR l a r) = bheight l"
   217 using assms
   218 by(induct l a r rule: baldR.induct)
   219   (auto simp: invh_baliL bheight_baliL invh_paint bheight_paint_Red)
   220 
   221 lemma invc_baldR: "\<lbrakk>invc a; invc2 b; color a = Black\<rbrakk> \<Longrightarrow> invc (baldR a x b)"
   222 by (induct a x b rule: baldR.induct) (simp_all add: invc_baliL)
   223 
   224 lemma invc2_baldR: "\<lbrakk> invc l; invc2 r \<rbrakk> \<Longrightarrow>invc2 (baldR l x r)"
   225 by (induct l x r rule: baldR.induct) (auto simp: invc_baliL paint_invc2 invc2I)
   226 
   227 lemma invh_combine:
   228   assumes "invh l" "invh r" "bheight l = bheight r"
   229   shows "bheight (combine l r) = bheight l" "invh (combine l r)"
   230 using assms 
   231 by (induct l r rule: combine.induct) 
   232    (auto simp: baldL_invh_app split: tree.splits color.splits)
   233 
   234 lemma invc_combine: 
   235   assumes "invc l" "invc r"
   236   shows "color l = Black \<Longrightarrow> color r = Black \<Longrightarrow> invc (combine l r)"
   237          "invc2 (combine l r)"
   238 using assms 
   239 by (induct l r rule: combine.induct)
   240    (auto simp: baldL_invc invc2I split: tree.splits color.splits)
   241 
   242 
   243 lemma assumes "invh l" "invc l"
   244   shows del_invc_invh:
   245    "invh (del x l) \<and>
   246    (color l = Red \<and> bheight (del x l) = bheight l \<and> invc (del x l) \<or>
   247     color l = Black \<and> bheight (del x l) = bheight l - 1 \<and> invc2 (del x l))"
   248 and  "\<lbrakk>invh r; bheight l = bheight r; invc r\<rbrakk> \<Longrightarrow>
   249    invh (delL x l k r) \<and> 
   250    bheight (delL x l k r) = bheight l \<and> 
   251    (color l = Black \<and> color r = Black \<and> invc (delL x l k r) \<or> 
   252     (color l \<noteq> Black \<or> color r \<noteq> Black) \<and> invc2 (delL x l k r))"
   253   and "\<lbrakk>invh r; bheight l = bheight r; invc r\<rbrakk> \<Longrightarrow>
   254   invh (delR x l k r) \<and> 
   255   bheight (delR x l k r) = bheight l \<and> 
   256   (color l = Black \<and> color r = Black \<and> invc (delR x l k r) \<or> 
   257    (color l \<noteq> Black \<or> color r \<noteq> Black) \<and> invc2 (delR x l k r))"
   258 using assms
   259 proof (induct x l and x l k r and x l k r rule: del_delL_delR.induct)
   260 case (2 y c _ y')
   261   have "y = y' \<or> y < y' \<or> y > y'" by auto
   262   thus ?case proof (elim disjE)
   263     assume "y = y'"
   264     with 2 show ?thesis
   265     by (cases c) (simp_all add: invh_combine invc_combine)
   266   next
   267     assume "y < y'"
   268     with 2 show ?thesis by (cases c) (auto simp: invc2I)
   269   next
   270     assume "y' < y"
   271     with 2 show ?thesis by (cases c) (auto simp: invc2I)
   272   qed
   273 next
   274   case (3 y l z ra y' bb)
   275   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)+
   276 next
   277   case (5 y a y' l z ra)
   278   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)+
   279 next
   280   case ("6_1" y a y') thus ?case by (cases "color a = Black \<and> color Leaf = Black") simp+
   281 qed auto
   282 
   283 theorem rbt_delete: "rbt t \<Longrightarrow> rbt (delete k t)"
   284 by (metis delete_def rbt_def color_paint_Black del_invc_invh invc_paint_Black invc2I invh_paint)
   285 
   286 text \<open>Overall correctness:\<close>
   287 
   288 interpretation Set_by_Ordered
   289 where empty = Leaf and isin = isin and insert = insert and delete = delete
   290 and inorder = inorder and inv = rbt
   291 proof (standard, goal_cases)
   292   case 1 show ?case by simp
   293 next
   294   case 2 thus ?case by(simp add: isin_set)
   295 next
   296   case 3 thus ?case by(simp add: inorder_insert)
   297 next
   298   case 4 thus ?case by(simp add: inorder_delete)
   299 next
   300   case 5 thus ?case by (simp add: rbt_Leaf) 
   301 next
   302   case 6 thus ?case by (simp add: rbt_insert) 
   303 next
   304   case 7 thus ?case by (simp add: rbt_delete) 
   305 qed
   306 
   307 
   308 subsection \<open>Height-Size Relation\<close>
   309 
   310 lemma neq_Black[simp]: "(c \<noteq> Black) = (c = Red)"
   311 by (cases c) auto
   312 
   313 lemma rbt_height_bheight_if_nat: "invc t \<Longrightarrow> invh t \<Longrightarrow>
   314   height t \<le> (if color t = Black then 2 * bheight t else 2 * bheight t + 1)"
   315 by(induction t) (auto split: if_split_asm)
   316 
   317 lemma rbt_height_bheight_if: "invc t \<Longrightarrow> invh t \<Longrightarrow>
   318   (if color t = Black then height t / 2 else (height t - 1) / 2) \<le> bheight t"
   319 by(induction t) (auto split: if_split_asm)
   320 
   321 lemma rbt_height_bheight: "rbt t \<Longrightarrow> height t / 2 \<le> bheight t "
   322 by(auto simp: rbt_def dest: rbt_height_bheight_if)
   323 
   324 lemma bheight_size_bound:  "invc t \<Longrightarrow> invh t \<Longrightarrow> size1 t \<ge>  2 ^ (bheight t)"
   325 by (induction t) auto
   326 
   327 lemma rbt_height_le: assumes "rbt t" shows "height t \<le> 2 * log 2 (size1 t)"
   328 proof -
   329   have "2 powr (height t / 2) \<le> 2 powr bheight t"
   330     using rbt_height_bheight[OF assms] by (simp)
   331   also have "\<dots> \<le> size1 t" using assms
   332     by (simp add: powr_realpow bheight_size_bound rbt_def)
   333   finally have "2 powr (height t / 2) \<le> size1 t" .
   334   hence "height t / 2 \<le> log 2 (size1 t)"
   335     by(simp add: le_log_iff size1_def del: Int.divide_le_eq_numeral1(1))
   336   thus ?thesis by simp
   337 qed
   338 
   339 end