src/HOL/Data_Structures/Tree23_Set.thy
author nipkow
Wed Jun 13 15:24:20 2018 +0200 (10 months ago)
changeset 68440 6826718f732d
parent 68431 b294e095f64c
child 69597 ff784d5a5bfb
permissions -rw-r--r--
qualify interpretations to avoid clashes
     1 (* Author: Tobias Nipkow *)
     2 
     3 section \<open>2-3 Tree Implementation of Sets\<close>
     4 
     5 theory Tree23_Set
     6 imports
     7   Tree23
     8   Cmp
     9   Set_Specs
    10 begin
    11 
    12 declare sorted_wrt.simps(2)[simp del]
    13 
    14 definition empty :: "'a tree23" where
    15 "empty = Leaf"
    16 
    17 fun isin :: "'a::linorder tree23 \<Rightarrow> 'a \<Rightarrow> bool" where
    18 "isin Leaf x = False" |
    19 "isin (Node2 l a r) x =
    20   (case cmp x a of
    21      LT \<Rightarrow> isin l x |
    22      EQ \<Rightarrow> True |
    23      GT \<Rightarrow> isin r x)" |
    24 "isin (Node3 l a m b r) x =
    25   (case cmp x a of
    26      LT \<Rightarrow> isin l x |
    27      EQ \<Rightarrow> True |
    28      GT \<Rightarrow>
    29        (case cmp x b of
    30           LT \<Rightarrow> isin m x |
    31           EQ \<Rightarrow> True |
    32           GT \<Rightarrow> isin r x))"
    33 
    34 datatype 'a up\<^sub>i = T\<^sub>i "'a tree23" | Up\<^sub>i "'a tree23" 'a "'a tree23"
    35 
    36 fun tree\<^sub>i :: "'a up\<^sub>i \<Rightarrow> 'a tree23" where
    37 "tree\<^sub>i (T\<^sub>i t) = t" |
    38 "tree\<^sub>i (Up\<^sub>i l a r) = Node2 l a r"
    39 
    40 fun ins :: "'a::linorder \<Rightarrow> 'a tree23 \<Rightarrow> 'a up\<^sub>i" where
    41 "ins x Leaf = Up\<^sub>i Leaf x Leaf" |
    42 "ins x (Node2 l a r) =
    43    (case cmp x a of
    44       LT \<Rightarrow>
    45         (case ins x l of
    46            T\<^sub>i l' => T\<^sub>i (Node2 l' a r) |
    47            Up\<^sub>i l1 b l2 => T\<^sub>i (Node3 l1 b l2 a r)) |
    48       EQ \<Rightarrow> T\<^sub>i (Node2 l x r) |
    49       GT \<Rightarrow>
    50         (case ins x r of
    51            T\<^sub>i r' => T\<^sub>i (Node2 l a r') |
    52            Up\<^sub>i r1 b r2 => T\<^sub>i (Node3 l a r1 b r2)))" |
    53 "ins x (Node3 l a m b r) =
    54    (case cmp x a of
    55       LT \<Rightarrow>
    56         (case ins x l of
    57            T\<^sub>i l' => T\<^sub>i (Node3 l' a m b r) |
    58            Up\<^sub>i l1 c l2 => Up\<^sub>i (Node2 l1 c l2) a (Node2 m b r)) |
    59       EQ \<Rightarrow> T\<^sub>i (Node3 l a m b r) |
    60       GT \<Rightarrow>
    61         (case cmp x b of
    62            GT \<Rightarrow>
    63              (case ins x r of
    64                 T\<^sub>i r' => T\<^sub>i (Node3 l a m b r') |
    65                 Up\<^sub>i r1 c r2 => Up\<^sub>i (Node2 l a m) b (Node2 r1 c r2)) |
    66            EQ \<Rightarrow> T\<^sub>i (Node3 l a m b r) |
    67            LT \<Rightarrow>
    68              (case ins x m of
    69                 T\<^sub>i m' => T\<^sub>i (Node3 l a m' b r) |
    70                 Up\<^sub>i m1 c m2 => Up\<^sub>i (Node2 l a m1) c (Node2 m2 b r))))"
    71 
    72 hide_const insert
    73 
    74 definition insert :: "'a::linorder \<Rightarrow> 'a tree23 \<Rightarrow> 'a tree23" where
    75 "insert x t = tree\<^sub>i(ins x t)"
    76 
    77 datatype 'a up\<^sub>d = T\<^sub>d "'a tree23" | Up\<^sub>d "'a tree23"
    78 
    79 fun tree\<^sub>d :: "'a up\<^sub>d \<Rightarrow> 'a tree23" where
    80 "tree\<^sub>d (T\<^sub>d t) = t" |
    81 "tree\<^sub>d (Up\<^sub>d t) = t"
    82 
    83 (* Variation: return None to signal no-change *)
    84 
    85 fun node21 :: "'a up\<^sub>d \<Rightarrow> 'a \<Rightarrow> 'a tree23 \<Rightarrow> 'a up\<^sub>d" where
    86 "node21 (T\<^sub>d t1) a t2 = T\<^sub>d(Node2 t1 a t2)" |
    87 "node21 (Up\<^sub>d t1) a (Node2 t2 b t3) = Up\<^sub>d(Node3 t1 a t2 b t3)" |
    88 "node21 (Up\<^sub>d t1) a (Node3 t2 b t3 c t4) = T\<^sub>d(Node2 (Node2 t1 a t2) b (Node2 t3 c t4))"
    89 
    90 fun node22 :: "'a tree23 \<Rightarrow> 'a \<Rightarrow> 'a up\<^sub>d \<Rightarrow> 'a up\<^sub>d" where
    91 "node22 t1 a (T\<^sub>d t2) = T\<^sub>d(Node2 t1 a t2)" |
    92 "node22 (Node2 t1 b t2) a (Up\<^sub>d t3) = Up\<^sub>d(Node3 t1 b t2 a t3)" |
    93 "node22 (Node3 t1 b t2 c t3) a (Up\<^sub>d t4) = T\<^sub>d(Node2 (Node2 t1 b t2) c (Node2 t3 a t4))"
    94 
    95 fun node31 :: "'a up\<^sub>d \<Rightarrow> 'a \<Rightarrow> 'a tree23 \<Rightarrow> 'a \<Rightarrow> 'a tree23 \<Rightarrow> 'a up\<^sub>d" where
    96 "node31 (T\<^sub>d t1) a t2 b t3 = T\<^sub>d(Node3 t1 a t2 b t3)" |
    97 "node31 (Up\<^sub>d t1) a (Node2 t2 b t3) c t4 = T\<^sub>d(Node2 (Node3 t1 a t2 b t3) c t4)" |
    98 "node31 (Up\<^sub>d t1) a (Node3 t2 b t3 c t4) d t5 = T\<^sub>d(Node3 (Node2 t1 a t2) b (Node2 t3 c t4) d t5)"
    99 
   100 fun node32 :: "'a tree23 \<Rightarrow> 'a \<Rightarrow> 'a up\<^sub>d \<Rightarrow> 'a \<Rightarrow> 'a tree23 \<Rightarrow> 'a up\<^sub>d" where
   101 "node32 t1 a (T\<^sub>d t2) b t3 = T\<^sub>d(Node3 t1 a t2 b t3)" |
   102 "node32 t1 a (Up\<^sub>d t2) b (Node2 t3 c t4) = T\<^sub>d(Node2 t1 a (Node3 t2 b t3 c t4))" |
   103 "node32 t1 a (Up\<^sub>d t2) b (Node3 t3 c t4 d t5) = T\<^sub>d(Node3 t1 a (Node2 t2 b t3) c (Node2 t4 d t5))"
   104 
   105 fun node33 :: "'a tree23 \<Rightarrow> 'a \<Rightarrow> 'a tree23 \<Rightarrow> 'a \<Rightarrow> 'a up\<^sub>d \<Rightarrow> 'a up\<^sub>d" where
   106 "node33 l a m b (T\<^sub>d r) = T\<^sub>d(Node3 l a m b r)" |
   107 "node33 t1 a (Node2 t2 b t3) c (Up\<^sub>d t4) = T\<^sub>d(Node2 t1 a (Node3 t2 b t3 c t4))" |
   108 "node33 t1 a (Node3 t2 b t3 c t4) d (Up\<^sub>d t5) = T\<^sub>d(Node3 t1 a (Node2 t2 b t3) c (Node2 t4 d t5))"
   109 
   110 fun split_min :: "'a tree23 \<Rightarrow> 'a * 'a up\<^sub>d" where
   111 "split_min (Node2 Leaf a Leaf) = (a, Up\<^sub>d Leaf)" |
   112 "split_min (Node3 Leaf a Leaf b Leaf) = (a, T\<^sub>d(Node2 Leaf b Leaf))" |
   113 "split_min (Node2 l a r) = (let (x,l') = split_min l in (x, node21 l' a r))" |
   114 "split_min (Node3 l a m b r) = (let (x,l') = split_min l in (x, node31 l' a m b r))"
   115 
   116 text \<open>In the base cases of \<open>split_min\<close> and \<open>del\<close> it is enough to check if one subtree is a \<open>Leaf\<close>,
   117 in which case balancedness implies that so are the others. Exercise.\<close>
   118 
   119 fun del :: "'a::linorder \<Rightarrow> 'a tree23 \<Rightarrow> 'a up\<^sub>d" where
   120 "del x Leaf = T\<^sub>d Leaf" |
   121 "del x (Node2 Leaf a Leaf) =
   122   (if x = a then Up\<^sub>d Leaf else T\<^sub>d(Node2 Leaf a Leaf))" |
   123 "del x (Node3 Leaf a Leaf b Leaf) =
   124   T\<^sub>d(if x = a then Node2 Leaf b Leaf else
   125      if x = b then Node2 Leaf a Leaf
   126      else Node3 Leaf a Leaf b Leaf)" |
   127 "del x (Node2 l a r) =
   128   (case cmp x a of
   129      LT \<Rightarrow> node21 (del x l) a r |
   130      GT \<Rightarrow> node22 l a (del x r) |
   131      EQ \<Rightarrow> let (a',t) = split_min r in node22 l a' t)" |
   132 "del x (Node3 l a m b r) =
   133   (case cmp x a of
   134      LT \<Rightarrow> node31 (del x l) a m b r |
   135      EQ \<Rightarrow> let (a',m') = split_min m in node32 l a' m' b r |
   136      GT \<Rightarrow>
   137        (case cmp x b of
   138           LT \<Rightarrow> node32 l a (del x m) b r |
   139           EQ \<Rightarrow> let (b',r') = split_min r in node33 l a m b' r' |
   140           GT \<Rightarrow> node33 l a m b (del x r)))"
   141 
   142 definition delete :: "'a::linorder \<Rightarrow> 'a tree23 \<Rightarrow> 'a tree23" where
   143 "delete x t = tree\<^sub>d(del x t)"
   144 
   145 
   146 subsection "Functional Correctness"
   147 
   148 subsubsection "Proofs for isin"
   149 
   150 lemma isin_set: "sorted(inorder t) \<Longrightarrow> isin t x = (x \<in> set (inorder t))"
   151 by (induction t) (auto simp: isin_simps ball_Un)
   152 
   153 
   154 subsubsection "Proofs for insert"
   155 
   156 lemma inorder_ins:
   157   "sorted(inorder t) \<Longrightarrow> inorder(tree\<^sub>i(ins x t)) = ins_list x (inorder t)"
   158 by(induction t) (auto simp: ins_list_simps split: up\<^sub>i.splits)
   159 
   160 lemma inorder_insert:
   161   "sorted(inorder t) \<Longrightarrow> inorder(insert a t) = ins_list a (inorder t)"
   162 by(simp add: insert_def inorder_ins)
   163 
   164 
   165 subsubsection "Proofs for delete"
   166 
   167 lemma inorder_node21: "height r > 0 \<Longrightarrow>
   168   inorder (tree\<^sub>d (node21 l' a r)) = inorder (tree\<^sub>d l') @ a # inorder r"
   169 by(induct l' a r rule: node21.induct) auto
   170 
   171 lemma inorder_node22: "height l > 0 \<Longrightarrow>
   172   inorder (tree\<^sub>d (node22 l a r')) = inorder l @ a # inorder (tree\<^sub>d r')"
   173 by(induct l a r' rule: node22.induct) auto
   174 
   175 lemma inorder_node31: "height m > 0 \<Longrightarrow>
   176   inorder (tree\<^sub>d (node31 l' a m b r)) = inorder (tree\<^sub>d l') @ a # inorder m @ b # inorder r"
   177 by(induct l' a m b r rule: node31.induct) auto
   178 
   179 lemma inorder_node32: "height r > 0 \<Longrightarrow>
   180   inorder (tree\<^sub>d (node32 l a m' b r)) = inorder l @ a # inorder (tree\<^sub>d m') @ b # inorder r"
   181 by(induct l a m' b r rule: node32.induct) auto
   182 
   183 lemma inorder_node33: "height m > 0 \<Longrightarrow>
   184   inorder (tree\<^sub>d (node33 l a m b r')) = inorder l @ a # inorder m @ b # inorder (tree\<^sub>d r')"
   185 by(induct l a m b r' rule: node33.induct) auto
   186 
   187 lemmas inorder_nodes = inorder_node21 inorder_node22
   188   inorder_node31 inorder_node32 inorder_node33
   189 
   190 lemma split_minD:
   191   "split_min t = (x,t') \<Longrightarrow> bal t \<Longrightarrow> height t > 0 \<Longrightarrow>
   192   x # inorder(tree\<^sub>d t') = inorder t"
   193 by(induction t arbitrary: t' rule: split_min.induct)
   194   (auto simp: inorder_nodes split: prod.splits)
   195 
   196 lemma inorder_del: "\<lbrakk> bal t ; sorted(inorder t) \<rbrakk> \<Longrightarrow>
   197   inorder(tree\<^sub>d (del x t)) = del_list x (inorder t)"
   198 by(induction t rule: del.induct)
   199   (auto simp: del_list_simps inorder_nodes split_minD split!: if_split prod.splits)
   200 
   201 lemma inorder_delete: "\<lbrakk> bal t ; sorted(inorder t) \<rbrakk> \<Longrightarrow>
   202   inorder(delete x t) = del_list x (inorder t)"
   203 by(simp add: delete_def inorder_del)
   204 
   205 
   206 subsection \<open>Balancedness\<close>
   207 
   208 
   209 subsubsection "Proofs for insert"
   210 
   211 text\<open>First a standard proof that @{const ins} preserves @{const bal}.\<close>
   212 
   213 instantiation up\<^sub>i :: (type)height
   214 begin
   215 
   216 fun height_up\<^sub>i :: "'a up\<^sub>i \<Rightarrow> nat" where
   217 "height (T\<^sub>i t) = height t" |
   218 "height (Up\<^sub>i l a r) = height l"
   219 
   220 instance ..
   221 
   222 end
   223 
   224 lemma bal_ins: "bal t \<Longrightarrow> bal (tree\<^sub>i(ins a t)) \<and> height(ins a t) = height t"
   225 by (induct t) (auto split!: if_split up\<^sub>i.split) (* 15 secs in 2015 *)
   226 
   227 text\<open>Now an alternative proof (by Brian Huffman) that runs faster because
   228 two properties (balance and height) are combined in one predicate.\<close>
   229 
   230 inductive full :: "nat \<Rightarrow> 'a tree23 \<Rightarrow> bool" where
   231 "full 0 Leaf" |
   232 "\<lbrakk>full n l; full n r\<rbrakk> \<Longrightarrow> full (Suc n) (Node2 l p r)" |
   233 "\<lbrakk>full n l; full n m; full n r\<rbrakk> \<Longrightarrow> full (Suc n) (Node3 l p m q r)"
   234 
   235 inductive_cases full_elims:
   236   "full n Leaf"
   237   "full n (Node2 l p r)"
   238   "full n (Node3 l p m q r)"
   239 
   240 inductive_cases full_0_elim: "full 0 t"
   241 inductive_cases full_Suc_elim: "full (Suc n) t"
   242 
   243 lemma full_0_iff [simp]: "full 0 t \<longleftrightarrow> t = Leaf"
   244   by (auto elim: full_0_elim intro: full.intros)
   245 
   246 lemma full_Leaf_iff [simp]: "full n Leaf \<longleftrightarrow> n = 0"
   247   by (auto elim: full_elims intro: full.intros)
   248 
   249 lemma full_Suc_Node2_iff [simp]:
   250   "full (Suc n) (Node2 l p r) \<longleftrightarrow> full n l \<and> full n r"
   251   by (auto elim: full_elims intro: full.intros)
   252 
   253 lemma full_Suc_Node3_iff [simp]:
   254   "full (Suc n) (Node3 l p m q r) \<longleftrightarrow> full n l \<and> full n m \<and> full n r"
   255   by (auto elim: full_elims intro: full.intros)
   256 
   257 lemma full_imp_height: "full n t \<Longrightarrow> height t = n"
   258   by (induct set: full, simp_all)
   259 
   260 lemma full_imp_bal: "full n t \<Longrightarrow> bal t"
   261   by (induct set: full, auto dest: full_imp_height)
   262 
   263 lemma bal_imp_full: "bal t \<Longrightarrow> full (height t) t"
   264   by (induct t, simp_all)
   265 
   266 lemma bal_iff_full: "bal t \<longleftrightarrow> (\<exists>n. full n t)"
   267   by (auto elim!: bal_imp_full full_imp_bal)
   268 
   269 text \<open>The @{const "insert"} function either preserves the height of the
   270 tree, or increases it by one. The constructor returned by the @{term
   271 "insert"} function determines which: A return value of the form @{term
   272 "T\<^sub>i t"} indicates that the height will be the same. A value of the
   273 form @{term "Up\<^sub>i l p r"} indicates an increase in height.\<close>
   274 
   275 fun full\<^sub>i :: "nat \<Rightarrow> 'a up\<^sub>i \<Rightarrow> bool" where
   276 "full\<^sub>i n (T\<^sub>i t) \<longleftrightarrow> full n t" |
   277 "full\<^sub>i n (Up\<^sub>i l p r) \<longleftrightarrow> full n l \<and> full n r"
   278 
   279 lemma full\<^sub>i_ins: "full n t \<Longrightarrow> full\<^sub>i n (ins a t)"
   280 by (induct rule: full.induct) (auto split: up\<^sub>i.split)
   281 
   282 text \<open>The @{const insert} operation preserves balance.\<close>
   283 
   284 lemma bal_insert: "bal t \<Longrightarrow> bal (insert a t)"
   285 unfolding bal_iff_full insert_def
   286 apply (erule exE)
   287 apply (drule full\<^sub>i_ins [of _ _ a])
   288 apply (cases "ins a t")
   289 apply (auto intro: full.intros)
   290 done
   291 
   292 
   293 subsection "Proofs for delete"
   294 
   295 instantiation up\<^sub>d :: (type)height
   296 begin
   297 
   298 fun height_up\<^sub>d :: "'a up\<^sub>d \<Rightarrow> nat" where
   299 "height (T\<^sub>d t) = height t" |
   300 "height (Up\<^sub>d t) = height t + 1"
   301 
   302 instance ..
   303 
   304 end
   305 
   306 lemma bal_tree\<^sub>d_node21:
   307   "\<lbrakk>bal r; bal (tree\<^sub>d l'); height r = height l' \<rbrakk> \<Longrightarrow> bal (tree\<^sub>d (node21 l' a r))"
   308 by(induct l' a r rule: node21.induct) auto
   309 
   310 lemma bal_tree\<^sub>d_node22:
   311   "\<lbrakk>bal(tree\<^sub>d r'); bal l; height r' = height l \<rbrakk> \<Longrightarrow> bal (tree\<^sub>d (node22 l a r'))"
   312 by(induct l a r' rule: node22.induct) auto
   313 
   314 lemma bal_tree\<^sub>d_node31:
   315   "\<lbrakk> bal (tree\<^sub>d l'); bal m; bal r; height l' = height r; height m = height r \<rbrakk>
   316   \<Longrightarrow> bal (tree\<^sub>d (node31 l' a m b r))"
   317 by(induct l' a m b r rule: node31.induct) auto
   318 
   319 lemma bal_tree\<^sub>d_node32:
   320   "\<lbrakk> bal l; bal (tree\<^sub>d m'); bal r; height l = height r; height m' = height r \<rbrakk>
   321   \<Longrightarrow> bal (tree\<^sub>d (node32 l a m' b r))"
   322 by(induct l a m' b r rule: node32.induct) auto
   323 
   324 lemma bal_tree\<^sub>d_node33:
   325   "\<lbrakk> bal l; bal m; bal(tree\<^sub>d r'); height l = height r'; height m = height r' \<rbrakk>
   326   \<Longrightarrow> bal (tree\<^sub>d (node33 l a m b r'))"
   327 by(induct l a m b r' rule: node33.induct) auto
   328 
   329 lemmas bals = bal_tree\<^sub>d_node21 bal_tree\<^sub>d_node22
   330   bal_tree\<^sub>d_node31 bal_tree\<^sub>d_node32 bal_tree\<^sub>d_node33
   331 
   332 lemma height'_node21:
   333    "height r > 0 \<Longrightarrow> height(node21 l' a r) = max (height l') (height r) + 1"
   334 by(induct l' a r rule: node21.induct)(simp_all)
   335 
   336 lemma height'_node22:
   337    "height l > 0 \<Longrightarrow> height(node22 l a r') = max (height l) (height r') + 1"
   338 by(induct l a r' rule: node22.induct)(simp_all)
   339 
   340 lemma height'_node31:
   341   "height m > 0 \<Longrightarrow> height(node31 l a m b r) =
   342    max (height l) (max (height m) (height r)) + 1"
   343 by(induct l a m b r rule: node31.induct)(simp_all add: max_def)
   344 
   345 lemma height'_node32:
   346   "height r > 0 \<Longrightarrow> height(node32 l a m b r) =
   347    max (height l) (max (height m) (height r)) + 1"
   348 by(induct l a m b r rule: node32.induct)(simp_all add: max_def)
   349 
   350 lemma height'_node33:
   351   "height m > 0 \<Longrightarrow> height(node33 l a m b r) =
   352    max (height l) (max (height m) (height r)) + 1"
   353 by(induct l a m b r rule: node33.induct)(simp_all add: max_def)
   354 
   355 lemmas heights = height'_node21 height'_node22
   356   height'_node31 height'_node32 height'_node33
   357 
   358 lemma height_split_min:
   359   "split_min t = (x, t') \<Longrightarrow> height t > 0 \<Longrightarrow> bal t \<Longrightarrow> height t' = height t"
   360 by(induct t arbitrary: x t' rule: split_min.induct)
   361   (auto simp: heights split: prod.splits)
   362 
   363 lemma height_del: "bal t \<Longrightarrow> height(del x t) = height t"
   364 by(induction x t rule: del.induct)
   365   (auto simp: heights max_def height_split_min split: prod.splits)
   366 
   367 lemma bal_split_min:
   368   "\<lbrakk> split_min t = (x, t'); bal t; height t > 0 \<rbrakk> \<Longrightarrow> bal (tree\<^sub>d t')"
   369 by(induct t arbitrary: x t' rule: split_min.induct)
   370   (auto simp: heights height_split_min bals split: prod.splits)
   371 
   372 lemma bal_tree\<^sub>d_del: "bal t \<Longrightarrow> bal(tree\<^sub>d(del x t))"
   373 by(induction x t rule: del.induct)
   374   (auto simp: bals bal_split_min height_del height_split_min split: prod.splits)
   375 
   376 corollary bal_delete: "bal t \<Longrightarrow> bal(delete x t)"
   377 by(simp add: delete_def bal_tree\<^sub>d_del)
   378 
   379 
   380 subsection \<open>Overall Correctness\<close>
   381 
   382 interpretation S: Set_by_Ordered
   383 where empty = empty and isin = isin and insert = insert and delete = delete
   384 and inorder = inorder and inv = bal
   385 proof (standard, goal_cases)
   386   case 2 thus ?case by(simp add: isin_set)
   387 next
   388   case 3 thus ?case by(simp add: inorder_insert)
   389 next
   390   case 4 thus ?case by(simp add: inorder_delete)
   391 next
   392   case 6 thus ?case by(simp add: bal_insert)
   393 next
   394   case 7 thus ?case by(simp add: bal_delete)
   395 qed (simp add: empty_def)+
   396 
   397 end