1open HolKernel Parse boolLib bossLib 2 3open boolSimps BasicProvers llistTheory; 4 5(* ---------------------------------------------------------------------- 6 a theory of "lazy" binary trees; that is potentially infinite binary 7 tree, with constructors 8 Lf : 'a lbtree 9 Nd : 'a -> 'a lbtree -> 'a lbtree -> 'a lbtree 10 ---------------------------------------------------------------------- *) 11 12val _ = new_theory "lbtree" 13 14(* set up the representative type and operations on it *) 15 16val Lfrep_def = Define`Lfrep = \l. NONE` 17 18val Ndrep_def = Define` 19 Ndrep a t1 t2 = \l. case l of 20 [] => SOME a 21 | T::xs => t1 xs 22 | F::xs => t2 xs 23`; 24 25val is_lbtree_def = Define` 26 is_lbtree t = ?P. (!t. P t ==> (t = Lfrep) \/ 27 ?a t1 t2. P t1 /\ P t2 /\ 28 (t = Ndrep a t1 t2)) /\ 29 P t 30`; 31 32val type_inhabited = prove( 33 ``?t. is_lbtree t``, 34 Q.EXISTS_TAC `Lfrep` THEN SRW_TAC [][is_lbtree_def] THEN 35 Q.EXISTS_TAC `(=) Lfrep` THEN SRW_TAC [][]); 36 37val lbtree_tydef = new_type_definition ("lbtree", type_inhabited) 38 39val repabs_fns = define_new_type_bijections { 40 name = "lbtree_absrep", 41 ABS = "lbtree_abs", 42 REP = "lbtree_rep", 43 tyax = lbtree_tydef 44}; 45 46val (lbtree_absrep, lbtree_repabs) = CONJ_PAIR repabs_fns 47val _ = BasicProvers.augment_srw_ss [rewrites [lbtree_absrep]] 48 49val is_lbtree_lbtree_rep = prove( 50 ``is_lbtree (lbtree_rep t)``, 51 SRW_TAC [][lbtree_repabs]); 52val _ = BasicProvers.augment_srw_ss [rewrites [is_lbtree_lbtree_rep]] 53 54val lbtree_rep_11 = prove( 55 ``(lbtree_rep t1 = lbtree_rep t2) = (t1 = t2)``, 56 SRW_TAC [][EQ_IMP_THM] THEN 57 POP_ASSUM (MP_TAC o AP_TERM ``lbtree_abs``) THEN SRW_TAC [][]); 58val _ = BasicProvers.augment_srw_ss [rewrites [lbtree_rep_11]] 59 60val lbtree_abs_11 = prove( 61 ``is_lbtree f1 /\ is_lbtree f2 ==> 62 ((lbtree_abs f1 = lbtree_abs f2) = (f1 = f2))``, 63 SRW_TAC [][lbtree_repabs, EQ_IMP_THM] THEN METIS_TAC []); 64 65val lbtree_repabs' = #1 (EQ_IMP_RULE (SPEC_ALL lbtree_repabs)) 66 67val is_lbtree_rules = prove( 68 ``is_lbtree Lfrep /\ 69 (is_lbtree t1 /\ is_lbtree t2 ==> is_lbtree (Ndrep a t1 t2))``, 70 SRW_TAC [][is_lbtree_def] THENL [ 71 Q.EXISTS_TAC `(=) Lfrep` THEN SRW_TAC [][], 72 Q.EXISTS_TAC `\t. P t \/ P' t \/ (t = Ndrep a t1 t2)` THEN 73 SRW_TAC [][] THEN METIS_TAC [] 74 ]); 75 76val is_lbtree_cases = prove( 77 ``is_lbtree t <=> 78 (t = Lfrep) \/ 79 ?a t1 t2. (t = Ndrep a t1 t2) /\ is_lbtree t1 /\ is_lbtree t2``, 80 SIMP_TAC (srw_ss() ++ DNF_ss) [EQ_IMP_THM, is_lbtree_rules] THEN 81 SRW_TAC [][is_lbtree_def] THEN RES_TAC THEN SRW_TAC [][] THEN 82 DISJ2_TAC THEN MAP_EVERY Q.EXISTS_TAC [`a`, `t1`, `t2`] THEN 83 SRW_TAC [][] THEN Q.EXISTS_TAC `P` THEN SRW_TAC [][]); 84 85val forall_lbtree = prove( 86 ``(!t. P t) = (!f. is_lbtree f ==> P (lbtree_abs f))``, 87 SRW_TAC [][EQ_IMP_THM] THEN ONCE_REWRITE_TAC [GSYM lbtree_absrep] THEN 88 SRW_TAC [][]); 89 90val Ndrep_11 = prove( 91 ``(Ndrep a1 t1 u1 = Ndrep a2 t2 u2) <=> (a1 = a2) /\ (t1 = t2) /\ (u1 = u2)``, 92 SRW_TAC [][Ndrep_def, EQ_IMP_THM, FUN_EQ_THM] THENL [ 93 POP_ASSUM (Q.SPEC_THEN `[]` MP_TAC) THEN SRW_TAC [][], 94 POP_ASSUM (Q.SPEC_THEN `T::x` MP_TAC) THEN SRW_TAC [][], 95 POP_ASSUM (Q.SPEC_THEN `F::x` MP_TAC) THEN SRW_TAC [][] 96 ]); 97 98(* this is only used in the one proof below *) 99val is_lbtree_coinduction = prove( 100 ``(!f. P f ==> (f = Lfrep) \/ 101 (?a t1 t2. P t1 /\ P t2 /\ (f = Ndrep a t1 t2))) ==> 102 !f. P f ==> is_lbtree f``, 103 SRW_TAC [][is_lbtree_def] THEN Q.EXISTS_TAC `P` THEN SRW_TAC [][]); 104 105(* the path_follow function motivates the unique co-recursive function. 106 for the moment we are still at the concrete/representative level *) 107 108val path_follow_def = Define` 109 (path_follow g x [] = OPTION_MAP FST (g x)) /\ 110 (path_follow g x (h::t) = 111 case g x of 112 NONE => NONE 113 | SOME (a,y,z) => path_follow g (if h then y else z) t) 114`; 115 116 117val path_follow_is_lbtree = prove( 118 ``!g x. is_lbtree (path_follow g x)``, 119 REPEAT GEN_TAC THEN 120 Q_TAC SUFF_TAC `!f. (?x. f = path_follow g x) ==> is_lbtree f` 121 THEN1 METIS_TAC [] THEN 122 HO_MATCH_MP_TAC is_lbtree_coinduction THEN SRW_TAC [][] THEN 123 `(g x = NONE) \/ ?a b1 b2. g x = SOME (a, b1, b2)` 124 by METIS_TAC [pairTheory.pair_CASES, optionTheory.option_CASES] 125 THENL [ 126 DISJ1_TAC THEN SRW_TAC [][FUN_EQ_THM] THEN 127 Cases_on `x'` THEN SRW_TAC [][path_follow_def, Lfrep_def], 128 DISJ2_TAC THEN 129 MAP_EVERY Q.EXISTS_TAC [`a`, `path_follow g b1`, `path_follow g b2`] THEN 130 SRW_TAC [][] THENL [ 131 METIS_TAC [], 132 METIS_TAC [], 133 SRW_TAC [][FUN_EQ_THM] THEN Cases_on `x'` THEN 134 SRW_TAC [][path_follow_def, Ndrep_def] 135 ] 136 ]); 137 138(* now start to lift the representative operations to the abstract level *) 139 140(* first define the constructors *) 141val Lf_def = Define`Lf = lbtree_abs Lfrep` 142val Nd_def = Define` 143 Nd a t1 t2 = lbtree_abs (Ndrep a (lbtree_rep t1) (lbtree_rep t2)) 144` 145 146val lbtree_cases = store_thm( 147 "lbtree_cases", 148 ``!t. (t = Lf) \/ (?a t1 t2. t = Nd a t1 t2)``, 149 SIMP_TAC (srw_ss()) [Lf_def, Nd_def, forall_lbtree, lbtree_abs_11, 150 is_lbtree_rules] THEN 151 ONCE_REWRITE_TAC [is_lbtree_cases] THEN SRW_TAC [][] THEN 152 METIS_TAC [lbtree_repabs']); 153 154val Lf_NOT_Nd = store_thm( 155 "Lf_NOT_Nd", 156 ``~(Lf = Nd a t1 t2)``, 157 SRW_TAC [][Lf_def, Nd_def, lbtree_abs_11, is_lbtree_rules] THEN 158 SRW_TAC [][Lfrep_def, Ndrep_def, FUN_EQ_THM] THEN 159 Q.EXISTS_TAC `[]` THEN SRW_TAC [][]); 160val _ = export_rewrites ["Lf_NOT_Nd"] 161 162Theorem Nd_11[simp]: 163 (Nd a1 t1 u1 = Nd a2 t2 u2) <=> (a1 = a2) /\ (t1 = t2) /\ (u1 = u2) 164Proof 165 SRW_TAC [][Nd_def, lbtree_abs_11, is_lbtree_rules, Ndrep_11] 166QED 167 168(* ---------------------------------------------------------------------- 169 co-recursion/finality axiom 170 ---------------------------------------------------------------------- *) 171 172val lbtree_ue_Axiom = store_thm( 173 "lbtree_ue_Axiom", 174 ``!f : 'a -> ('b # 'a # 'a) option. 175 ?!g : 'a -> 'b lbtree. 176 !x. g x = case f x of 177 NONE => Lf 178 | SOME(b,y,z) => Nd b (g y) (g z)``, 179 GEN_TAC THEN 180 SRW_TAC [][EXISTS_UNIQUE_THM] THENL [ 181 Q.EXISTS_TAC `\x. lbtree_abs (path_follow f x)` THEN 182 SRW_TAC [][] THEN 183 `(f x = NONE) \/ ?a b1 b2. f x = SOME(a,b1,b2)` 184 by METIS_TAC [pairTheory.pair_CASES, optionTheory.option_CASES] 185 THENL [ 186 SRW_TAC [][Lf_def, lbtree_abs_11, is_lbtree_rules, 187 path_follow_is_lbtree] THEN 188 SRW_TAC [][FUN_EQ_THM, Lfrep_def] THEN 189 Cases_on `x'` THEN SRW_TAC [][path_follow_def], 190 SRW_TAC [][Nd_def, lbtree_abs_11, is_lbtree_rules, 191 path_follow_is_lbtree, lbtree_repabs'] THEN 192 SRW_TAC [][FUN_EQ_THM, Ndrep_def] THEN 193 Cases_on `x'` THEN SRW_TAC [][path_follow_def] 194 ], 195 196 Q_TAC SUFF_TAC `!x. g x = g' x` THEN1 SIMP_TAC (srw_ss()) [FUN_EQ_THM] THEN 197 Q_TAC SUFF_TAC `!x. lbtree_rep (g x) = lbtree_rep (g' x)` 198 THEN1 SIMP_TAC (srw_ss()) [] THEN 199 Q_TAC SUFF_TAC `!l x. lbtree_rep (g x) l = lbtree_rep (g' x) l` 200 THEN1 SIMP_TAC bool_ss [FUN_EQ_THM] THEN 201 Q_TAC SUFF_TAC `!l x. (lbtree_rep (g x) l = path_follow f x l) /\ 202 (lbtree_rep (g' x) l = path_follow f x l)` 203 THEN1 SIMP_TAC bool_ss [] THEN 204 Induct THENL [ 205 ONCE_ASM_REWRITE_TAC [] THEN 206 SIMP_TAC (srw_ss()) [path_follow_def] THEN 207 GEN_TAC THEN 208 `(f x = NONE) \/ ?a b1 b2. f x = SOME (a, b1, b2)` 209 by METIS_TAC [pairTheory.pair_CASES, optionTheory.option_CASES] THEN 210 POP_ASSUM SUBST_ALL_TAC THENL [ 211 SIMP_TAC (srw_ss()) [Lf_def, lbtree_repabs', is_lbtree_rules] THEN 212 SRW_TAC [][Lfrep_def], 213 SIMP_TAC (srw_ss()) [Nd_def, lbtree_repabs', is_lbtree_rules] THEN 214 SIMP_TAC (srw_ss())[Ndrep_def] 215 ], 216 ONCE_ASM_REWRITE_TAC [] THEN SIMP_TAC (srw_ss()) [path_follow_def] THEN 217 REPEAT GEN_TAC THEN POP_ASSUM MP_TAC THEN 218 `(f x = NONE) \/ ?a b1 b2. f x = SOME (a, b1, b2)` 219 by METIS_TAC [pairTheory.pair_CASES, optionTheory.option_CASES] THEN 220 POP_ASSUM SUBST_ALL_TAC THENL [ 221 SIMP_TAC (srw_ss()) [Lf_def, lbtree_repabs', is_lbtree_rules] THEN 222 SIMP_TAC (srw_ss()) [Lfrep_def], 223 SIMP_TAC (srw_ss()) [Nd_def, lbtree_repabs', is_lbtree_rules] THEN 224 SIMP_TAC (srw_ss()) [Ndrep_def] THEN 225 REPEAT (POP_ASSUM (K ALL_TAC)) THEN SRW_TAC [][] 226 ] 227 ] 228 ]); 229 230(* ---------------------------------------------------------------------- 231 define a case constant - wouldn't it be nice if we could use nice case 232 syntax with this? 233 ---------------------------------------------------------------------- *) 234 235val lbtree_case_def = Define` 236 lbtree_case e f t = if t = Lf then e 237 else f (@a. ?t1 t2. t = Nd a t1 t2) 238 (@t1. ?a t2. t = Nd a t1 t2) 239 (@t2. ?a t1. t = Nd a t1 t2) 240`; 241 242val lbtree_case_thm = store_thm( 243 "lbtree_case_thm", 244 ``(lbtree_case e f Lf = e) /\ 245 (lbtree_case e f (Nd a t1 t2) = f a t1 t2)``, 246 SRW_TAC [][lbtree_case_def]); 247val _ = export_rewrites ["lbtree_case_thm"] 248 249(* ---------------------------------------------------------------------- 250 Bisimulation 251 252 Strong and weak versions. Follows as a consequence of the finality 253 theorem. 254 ---------------------------------------------------------------------- *) 255 256val lbtree_bisimulation = store_thm( 257 "lbtree_bisimulation", 258 ``!t u. (t = u) = 259 ?R. R t u /\ 260 !t u. R t u ==> 261 (t = Lf) /\ (u = Lf) \/ 262 ?a t1 u1 t2 u2. 263 R t1 u1 /\ R t2 u2 /\ 264 (t = Nd a t1 t2) /\ (u = Nd a u1 u2)``, 265 REPEAT GEN_TAC THEN EQ_TAC THENL [ 266 DISCH_THEN SUBST_ALL_TAC THEN Q.EXISTS_TAC `(=)` THEN SRW_TAC [][] THEN 267 METIS_TAC [lbtree_cases], 268 SRW_TAC [][] THEN 269 Q.ISPEC_THEN 270 `\ (t, u). 271 if R t u then 272 lbtree_case NONE 273 (\a t1 t2. SOME(a, (t1, (@u1. ?u2. u = Nd a u1 u2)), 274 (t2, (@u2. ?u1. u = Nd a u1 u2)))) 275 t 276 else 277 NONE` 278 (ASSUME_TAC o 279 Q.SPECL [`\ (t,u). if R t u then t else Lf`, 280 `\ (t,u). if R t u then u else Lf`] o 281 CONJUNCT2 o 282 SIMP_RULE bool_ss [EXISTS_UNIQUE_THM]) 283 lbtree_ue_Axiom THEN 284 Q_TAC SUFF_TAC `(\ (t,u). if R t u then t else Lf) = 285 (\ (t,u). if R t u then u else Lf)` 286 THEN1 (SRW_TAC [][FUN_EQ_THM, pairTheory.FORALL_PROD] THEN 287 METIS_TAC []) THEN 288 POP_ASSUM MATCH_MP_TAC THEN 289 ASM_SIMP_TAC (srw_ss()) [pairTheory.FORALL_PROD] THEN 290 SRW_TAC [][] THENL [ 291 `(p_1 = Lf) \/ (?a t1 t2. p_1 = Nd a t1 t2)` 292 by METIS_TAC [lbtree_cases] 293 THENL [ 294 SRW_TAC [][], 295 `?u1 u2. (p_2 = Nd a u1 u2) /\ R t1 u1 /\ R t2 u2` 296 by METIS_TAC [Lf_NOT_Nd, Nd_11] THEN 297 SRW_TAC [][] 298 ], 299 `(p_2 = Lf) \/ (?a u1 u2. p_2 = Nd a u1 u2)` 300 by METIS_TAC [lbtree_cases] 301 THENL [ 302 `p_1 = Lf` by METIS_TAC [Lf_NOT_Nd] THEN SRW_TAC [][], 303 `?t1 t2. (p_1 = Nd a t1 t2) /\ R t1 u1 /\ R t2 u2` 304 by METIS_TAC [Lf_NOT_Nd, Nd_11] THEN 305 SRW_TAC [][] 306 ] 307 ] 308 ]); 309 310val lbtree_strong_bisimulation = store_thm( 311 "lbtree_strong_bisimulation", 312 ``!t u. 313 (t = u) = 314 ?R. R t u /\ 315 !t u. 316 R t u ==> (t = u) \/ 317 ?a t1 u1 t2 u2. 318 R t1 u1 /\ R t2 u2 /\ 319 (t = Nd a t1 t2) /\ (u = Nd a u1 u2)``, 320 REPEAT GEN_TAC THEN EQ_TAC THENL [ 321 DISCH_THEN SUBST_ALL_TAC THEN Q.EXISTS_TAC `(=)` THEN SRW_TAC [][], 322 STRIP_TAC THEN ONCE_REWRITE_TAC [lbtree_bisimulation] THEN 323 Q.EXISTS_TAC `\t u. R t u \/ (t = u)` THEN 324 SRW_TAC [][] THENL [ 325 `(t' = u') \/ 326 ?a t1 u1 t2 u2. R t1 u1 /\ R t2 u2 /\ (t' = Nd a t1 t2) /\ 327 (u' = Nd a u1 u2)` 328 by METIS_TAC [] THEN 329 SRW_TAC [][] THEN 330 `(t' = Lf) \/ (?a t1 t2. t' = Nd a t1 t2)` 331 by METIS_TAC [lbtree_cases] THEN 332 SRW_TAC [][], 333 `(t' = Lf) \/ (?a t1 t2. t' = Nd a t1 t2)` 334 by METIS_TAC [lbtree_cases] THEN 335 SRW_TAC [][] 336 ] 337 ]); 338 339(* ---------------------------------------------------------------------- 340 mem : 'a -> 'a lbtree -> bool 341 342 inductively defined 343 ---------------------------------------------------------------------- *) 344 345val (mem_rules, mem_ind, mem_cases) = Hol_reln` 346 (!a t1 t2. mem a (Nd a t1 t2)) /\ 347 (!a b t1 t2. mem a t1 ==> mem a (Nd b t1 t2)) /\ 348 (!a b t1 t2. mem a t2 ==> mem a (Nd b t1 t2)) 349`; 350 351Theorem mem_thm[simp]: 352 (mem a Lf = F) /\ 353 (mem a (Nd b t1 t2) <=> (a = b) \/ mem a t1 \/ mem a t2) 354Proof 355 CONJ_TAC THEN CONV_TAC (LAND_CONV (ONCE_REWRITE_CONV [mem_cases])) THEN 356 SRW_TAC [][] THEN METIS_TAC [] 357QED 358 359 360(* ---------------------------------------------------------------------- 361 map : ('a -> 'b) -> 'a lbtree -> 'b lbtree 362 363 co-recursively defined 364 ---------------------------------------------------------------------- *) 365 366val map_def = new_specification("map_def", ["map"], 367 prove( 368 ``?map. !f : 'a -> 'b. 369 (map f Lf = Lf) /\ 370 (!a t1 t2. map f (Nd a t1 t2) = Nd (f a) (map f t1) (map f t2))``, 371 Q.ISPEC_THEN 372 `lbtree_case NONE (\a:'a t1 t2. SOME (f a:'b, t1, t2))` 373 (STRIP_ASSUME_TAC o CONV_RULE SKOLEM_CONV o GEN_ALL o 374 CONJUNCT1 o SIMP_RULE bool_ss [EXISTS_UNIQUE_THM]) 375 lbtree_ue_Axiom THEN 376 Q.EXISTS_TAC `g` THEN REPEAT STRIP_TAC THEN 377 POP_ASSUM (fn th => CONV_TAC (LAND_CONV (ONCE_REWRITE_CONV [th]))) THEN 378 SRW_TAC [][])); 379val _ = export_rewrites ["map_def"] 380 381val map_eq_Lf = store_thm( 382 "map_eq_Lf", 383 ``((map f t = Lf) = (t = Lf)) /\ ((Lf = map f t) = (t = Lf))``, 384 `(t = Lf) \/ ?a t1 t2. t = Nd a t1 t2` by METIS_TAC [lbtree_cases] THEN 385 SRW_TAC [][]); 386val _ = export_rewrites ["map_eq_Lf"] 387 388val map_eq_Nd = store_thm( 389 "map_eq_Nd", 390 ``(map f t = Nd a t1 t2) = 391 ?a' t1' t2'. (t = Nd a' t1' t2') /\ (a = f a') /\ 392 (t1 = map f t1') /\ (t2 = map f t2')``, 393 `(t = Lf) \/ ?a' t1' t2'. t = Nd a' t1' t2'` by METIS_TAC [lbtree_cases] THEN 394 SRW_TAC [][] THEN METIS_TAC []); 395 396 397(* ---------------------------------------------------------------------- 398 finite : 'a lbtree -> bool 399 400 inductively defined 401 ---------------------------------------------------------------------- *) 402 403val (finite_rules, finite_ind, finite_cases) = Hol_reln` 404 finite Lf /\ 405 !a t1 t2. finite t1 /\ finite t2 ==> finite (Nd a t1 t2) 406`; 407 408Theorem finite_thm[simp]: 409 (finite Lf = T) /\ 410 (finite (Nd a t1 t2) <=> finite t1 /\ finite t2) 411Proof 412 CONJ_TAC THEN 413 CONV_TAC (LAND_CONV (ONCE_REWRITE_CONV [finite_cases])) THEN 414 SRW_TAC [][] 415QED 416 417 418val finite_map = store_thm( 419 "finite_map", 420 ``finite (map f t) = finite t``, 421 Q_TAC SUFF_TAC `(!t. finite t ==> finite (map f t)) /\ 422 !t. finite t ==> !t'. (t = map f t') ==> finite t'` 423 THEN1 METIS_TAC [] THEN 424 CONJ_TAC THENL [ 425 HO_MATCH_MP_TAC finite_ind THEN SRW_TAC [][], 426 HO_MATCH_MP_TAC finite_ind THEN SRW_TAC [][map_eq_Nd] THEN 427 SRW_TAC [][] 428 ]); 429val _ = export_rewrites ["finite_map"] 430 431(* ---------------------------------------------------------------------- 432 bf_flatten : 'a lbtree list -> 'a llist 433 434 breadth-first flatten, takes a list of trees because the recursion 435 needs to maintain a queue of trees at the current fringe of 436 exploration 437 ---------------------------------------------------------------------- *) 438 439(* helper function that we "delete" immediately after def'n below *) 440val drop_while_def = zDefine` 441 (drop_while P [] = []) /\ 442 (drop_while P (h::t) = if P h then drop_while P t else h::t) 443`; 444 445val bf_flatten_def = new_specification( 446 "bf_flatten_def", 447 ["bf_flatten"], 448 prove(``?f. (f [] = LNIL) /\ 449 (!ts. f (Lf::ts) = f ts) /\ 450 (!a t1 t2 ts. f (Nd a t1 t2::ts) = a:::f (ts ++ [t1; t2]))``, 451 Q.ISPEC_THEN 452 `\l. case drop_while ((=) Lf) l of 453 [] => NONE 454 | t::ts => lbtree_case NONE 455 (\a t1 t2. SOME (ts ++ [t1;t2], a)) 456 t` 457 STRIP_ASSUME_TAC llist_Axiom_1 THEN 458 Q.EXISTS_TAC `g` THEN 459 REPEAT STRIP_TAC THENL [ 460 ONCE_ASM_REWRITE_TAC [] THEN 461 POP_ASSUM (K ALL_TAC) THEN 462 SRW_TAC [][drop_while_def], 463 ONCE_ASM_REWRITE_TAC [] THEN 464 SIMP_TAC (srw_ss()) [drop_while_def], 465 POP_ASSUM (fn th => CONV_TAC (LAND_CONV 466 (ONCE_REWRITE_CONV [th]))) THEN 467 SRW_TAC [][drop_while_def] 468 ])) 469 470val _ = delete_const "drop_while" 471 472(* simple properties of bf_flatten *) 473val bf_flatten_eq_lnil = store_thm( 474 "bf_flatten_eq_lnil", 475 ``!l. (bf_flatten l = [||]) = EVERY ((=)Lf) l``, 476 Induct THEN SRW_TAC [][bf_flatten_def] THEN 477 `(h = Lf) \/ (?a t1 t2. h = Nd a t1 t2)` 478 by METIS_TAC [lbtree_cases] THEN 479 SRW_TAC [][bf_flatten_def]); 480 481val bf_flatten_append = store_thm( 482 "bf_flatten_append", 483 ``!l1. EVERY ((=) Lf) l1 ==> (bf_flatten (l1 ++ l2) = bf_flatten l2)``, 484 Induct THEN SRW_TAC [][] THEN SRW_TAC [][bf_flatten_def]); 485 486(* a somewhat more complicated property, requiring one simple lemma about 487 lists and EXISTS first *) 488val EXISTS_FIRST = store_thm( 489 "EXISTS_FIRST", 490 ``!l. EXISTS P l ==> ?l1 x l2. (l = l1 ++ (x::l2)) /\ EVERY ((~) o P) l1 /\ 491 P x``, 492 Induct THEN SRW_TAC [][] THENL [ 493 MAP_EVERY Q.EXISTS_TAC [`[]`, `h`, `l`] THEN SRW_TAC [][], 494 Cases_on `P h` THENL [ 495 MAP_EVERY Q.EXISTS_TAC [`[]`, `h`, `l`] THEN SRW_TAC [][], 496 RES_TAC THEN 497 MAP_EVERY Q.EXISTS_TAC [`h::l1`, `x`, `l2`] THEN SRW_TAC [][] 498 ] 499 ]); 500 501Theorem exists_bf_flatten: 502 exists ((=)x) (bf_flatten tlist) ==> EXISTS (mem x) tlist 503Proof 504 ���!l. exists ((=)x) l ==> 505 !tlist. (l = bf_flatten tlist) ==> 506 EXISTS (mem x) tlist��� suffices_by metis_tac[] >> 507 HO_MATCH_MP_TAC exists_ind THEN SRW_TAC [][] THENL [ 508 ���~EVERY ($= Lf) tlist��� 509 by METIS_TAC [LCONS_NOT_NIL, bf_flatten_eq_lnil] THEN 510 ���EXISTS ($~ o $= Lf) tlist��� 511 by FULL_SIMP_TAC (srw_ss()) [listTheory.NOT_EVERY] THEN 512 ���?l1 x l2. EVERY ($~ o $~ o $= Lf) l1 /\ ($~ o $= Lf) x /\ 513 (tlist = l1 ++ (x :: l2))��� 514 by METIS_TAC [EXISTS_FIRST] THEN 515 ���EVERY ((=) Lf) l1��� 516 by FULL_SIMP_TAC (srw_ss() ++ ETA_ss) 517 [combinTheory.o_DEF, Excl "NORMEQ_CONV"] THEN 518 ���Lf <> x��� by FULL_SIMP_TAC (srw_ss()) [] THEN 519 ���?a t1 t2. x = Nd a t1 t2��� by METIS_TAC [lbtree_cases] THEN 520 FULL_SIMP_TAC (srw_ss()) [] THEN 521 (bf_flatten_append |> Q.SPEC ���l1��� |> Q.INST [���l2���|->���[Nd a t1 t2] ++ l2���] |> MP_TAC) THEN 522 SRW_TAC [][bf_flatten_def] THEN FULL_SIMP_TAC (srw_ss()) [], 523 ���~EVERY ($= Lf) tlist��� 524 by METIS_TAC [LCONS_NOT_NIL, bf_flatten_eq_lnil] THEN 525 ���EXISTS ($~ o $= Lf) tlist��� 526 by FULL_SIMP_TAC (srw_ss()) [listTheory.NOT_EVERY] THEN 527 ���?l1 y l2. EVERY ($~ o $~ o $= Lf) l1 /\ ($~ o $= Lf) y /\ 528 (tlist = l1 ++ (y :: l2))��� 529 by METIS_TAC [EXISTS_FIRST] THEN 530 ���EVERY ((=) Lf) l1��� 531 by FULL_SIMP_TAC (srw_ss() ++ ETA_ss) 532 [combinTheory.o_DEF, Excl "NORMEQ_CONV"] THEN 533 ���~(Lf = y)��� by FULL_SIMP_TAC (srw_ss()) [] THEN 534 ���?a t1 t2. y = Nd a t1 t2��� by METIS_TAC [lbtree_cases] THEN 535 FULL_SIMP_TAC (srw_ss()) [bf_flatten_def, bf_flatten_append] THEN 536 FIRST_X_ASSUM (Q.SPEC_THEN ���l2 ++ [t1;t2]��� MP_TAC) THEN 537 SRW_TAC [][] THEN SRW_TAC [][] THEN 538 (bf_flatten_append |> Q.SPEC ���l1��� |> Q.INST [���l2���|->���[Nd a t1 t2] ++ l2���] |> MP_TAC) THEN 539 SRW_TAC [][bf_flatten_def] THEN FULL_SIMP_TAC (srw_ss()) [] THEN 540 METIS_TAC [] 541 ] 542QED 543 544(* ---------------------------------------------------------------------- 545 Now it starts to get HIDEOUS. 546 547 Everything in the rest of the file is an indictment of something, 548 maybe 549 * theorem-proving in general; or 550 * HOL4; or 551 * me 552 553 Whatever it is, the following development of what is really a very 554 simple proof is just ghastly. 555 556 The proof is of the converse of the last lemma, that 557 558 EXISTS (mem x) tlist ==> exists ((=) x) (bf_flatten tlist) 559 560 This can't be proved by a structural induction on tlist because of 561 the way tlist actually gets bigger as the flatten proceeds. Nor 562 can we induct on the "size" of tlist (taking into consideration 563 the sizes of the tree-elements) because of the presence of 564 infinite trees. Instead, we induct on the lexicographic product 565 of the minimum depth at which x occurs in a tree, and the minimum 566 index within the list of a tree containing x to that depth. 567 568 This is reduced because of the following: 569 570 If the tree with x in it is not at the head of the list, then 571 the depth number doesn't change, but the index goes down because 572 all of the trees in the list move forward (as a Lf is either 573 discarded from the head of the list, or as a Nd is pulled off, 574 and two sub-trees are enqueued at the back of the list). 575 576 If the tree with x in it is at the head of the list then it's 577 either at the top of the tree in which case we're done, or it 578 moves to the end of the list, but at a reduced depth. 579 580 This reads fairly clearly I think, and feels as if it should be 581 straightforward. It's anything but. 582 583 ---------------------------------------------------------------------- *) 584 585 586(* depth x t n means that x occurs in tree t at depth n *) 587val (depth_rules, depth_ind, depth_cases) = Hol_reln` 588 (!x t1 t2. depth x (Nd x t1 t2) 0) /\ 589 (!m x a t1 t2. depth x t1 m ==> depth x (Nd a t1 t2) (SUC m)) /\ 590 (!m x a t1 t2. depth x t2 m ==> depth x (Nd a t1 t2) (SUC m)) 591`; 592 593val mem_depth = store_thm( 594 "mem_depth", 595 ``!x t. mem x t ==> ?n. depth x t n``, 596 HO_MATCH_MP_TAC mem_ind THEN SRW_TAC [][] THEN 597 METIS_TAC [depth_rules]); 598 599val depth_mem = store_thm( 600 "depth_mem", 601 ``!x t n. depth x t n ==> mem x t``, 602 HO_MATCH_MP_TAC depth_ind THEN SRW_TAC [][]); 603 604(* mindepth x t returns SOME n if x occurs in t at minimum depth n, 605 else NONE *) 606val mindepth_def = Define` 607 mindepth x t = if mem x t then SOME (LEAST n. depth x t n) else NONE 608`; 609 610open numLib 611(* following tactic is used twice in theorem below - yerk *) 612val lelim = REWRITE_RULE [GSYM AND_IMP_INTRO] whileTheory.LEAST_ELIM 613val min_tac = 614 SRW_TAC [ETA_ss][] THEN 615 IMP_RES_THEN (fn th => th |> MATCH_MP lelim |> DEEP_INTRO_TAC) mem_depth THEN 616 Q.X_GEN_TAC `t1d` THEN NTAC 2 STRIP_TAC THEN 617 Q.X_GEN_TAC `t2d` THEN NTAC 2 STRIP_TAC THEN 618 LEAST_ELIM_TAC THEN 619 ONCE_REWRITE_TAC [depth_cases] THEN 620 SRW_TAC [][EXISTS_OR_THM] THEN1 METIS_TAC [] THENL[ 621 `m = t1d` 622 by (SPOSE_NOT_THEN ASSUME_TAC THEN 623 `m < t1d \/ t1d < m` by DECIDE_TAC THENL [ 624 METIS_TAC [], 625 METIS_TAC [DECIDE ``SUC x < SUC y <=> x < y``, 626 depth_rules] 627 ]) THEN 628 SRW_TAC [][arithmeticTheory.MIN_DEF] THEN 629 SPOSE_NOT_THEN ASSUME_TAC THEN 630 `t2d < m` by DECIDE_TAC THEN 631 METIS_TAC [DECIDE ``SUC x < SUC y <=> x < y``, depth_rules], 632 `m = t2d` 633 by (SPOSE_NOT_THEN ASSUME_TAC THEN 634 `m < t2d \/ t2d < m` by DECIDE_TAC THENL [ 635 METIS_TAC [], 636 METIS_TAC [DECIDE ``SUC x < SUC y <=> x < y``, 637 depth_rules] 638 ]) THEN 639 SRW_TAC [][arithmeticTheory.MIN_DEF] THEN 640 METIS_TAC [DECIDE ``SUC x < SUC y <=> x < y``, depth_rules] 641 ] 642 643(* a minimum function lifted to option type: NONEs are treated as if they 644 are +ve infinity *) 645val optmin_def = Define` 646 (optmin NONE NONE = NONE) /\ 647 (optmin (SOME x) NONE = SOME x) /\ 648 (optmin NONE (SOME y) = SOME y) /\ 649 (optmin (SOME x) (SOME y) = SOME (MIN x y)) 650`; 651 652(* recursive characterisation of mindepth *) 653val mindepth_thm = store_thm( 654 "mindepth_thm", 655 ``(mindepth x Lf = NONE) /\ 656 (mindepth x (Nd a t1 t2) = 657 if x = a then SOME 0 658 else OPTION_MAP SUC (optmin (mindepth x t1) (mindepth x t2)))``, 659 SRW_TAC [][mindepth_def] THEN FULL_SIMP_TAC (srw_ss()) [optmin_def] THENL [ 660 LEAST_ELIM_TAC THEN SRW_TAC [][] THEN1 METIS_TAC [depth_rules] THEN 661 Cases_on `n` THEN SRW_TAC [][] THEN 662 FIRST_X_ASSUM (Q.SPEC_THEN `0` MP_TAC) THEN SRW_TAC [][depth_rules], 663 664 min_tac, 665 min_tac, 666 667 SRW_TAC [ETA_ss][] THEN 668 IMP_RES_THEN (DEEP_INTRO_TAC o MATCH_MP lelim) mem_depth THEN SRW_TAC [][] THEN 669 LEAST_ELIM_TAC THEN SRW_TAC [][] 670 THEN1 METIS_TAC [mem_depth, depth_rules] THEN 671 POP_ASSUM MP_TAC THEN 672 `!n. ~depth x t2 n` by METIS_TAC [depth_mem] THEN 673 ONCE_REWRITE_TAC [depth_cases] THEN SRW_TAC [][] THEN 674 Q_TAC SUFF_TAC `~(m < n) /\ ~(n < m)` THEN1 DECIDE_TAC THEN 675 REPEAT STRIP_TAC THEN METIS_TAC [DECIDE ``SUC x < SUC y <=> x < y``, 676 depth_rules], 677 678 SRW_TAC [ETA_ss][] THEN 679 IMP_RES_THEN (DEEP_INTRO_TAC o MATCH_MP lelim) mem_depth THEN SRW_TAC [][] THEN 680 LEAST_ELIM_TAC THEN SRW_TAC [][] 681 THEN1 METIS_TAC [mem_depth, depth_rules] THEN 682 POP_ASSUM MP_TAC THEN 683 `!n. ~depth x t1 n` by METIS_TAC [depth_mem] THEN 684 ONCE_REWRITE_TAC [depth_cases] THEN SRW_TAC [][] THEN 685 Q_TAC SUFF_TAC `~(m < n) /\ ~(n < m)` THEN1 DECIDE_TAC THEN 686 REPEAT STRIP_TAC THEN METIS_TAC [DECIDE ``SUC x < SUC y <=> x < y``, 687 depth_rules] 688 ]); 689 690val mem_mindepth = store_thm( 691 "mem_mindepth", 692 ``!x t. mem x t ==> (?n. mindepth x t = SOME n)``, 693 METIS_TAC [mindepth_def]); 694 695val mindepth_depth = store_thm( 696 "mindepth_depth", 697 ``(mindepth x t = SOME n) ==> depth x t n``, 698 SRW_TAC [][mindepth_def] THEN LEAST_ELIM_TAC THEN SRW_TAC [][] THEN 699 METIS_TAC [mem_depth]); 700 701(* is_mmindex f l n d says that n is the least index of the element with 702 minimal weight (d), as defined by f : 'a -> num option 703 704 Defining this relation as a recursive function to calculate n and d 705 results in a complicated function with accumulators that is very fiddly 706 to prove correct. Its option return type also makes the ultimate proof 707 ugly --- I decided it was a mistake bothering with it. *) 708val is_mmindex_def = Define` 709 is_mmindex f l n d <=> 710 n < LENGTH l /\ 711 (f (EL n l) = SOME d) /\ 712 !i. i < LENGTH l ==> 713 (f (EL i l) = NONE) \/ 714 ?d'. (f (EL i l) = SOME d') /\ 715 d <= d' /\ (i < n ==> d < d') 716`; 717 718(* the crucial fact about minimums -- two levels of LEAST-ness going on in 719 here *) 720val mmindex_EXISTS = store_thm( 721 "mmindex_EXISTS", 722 ``EXISTS (\e. ?n. f e = SOME n) l ==> ?i m. is_mmindex f l i m``, 723 SRW_TAC [][is_mmindex_def] THEN 724 Q.ABBREV_TAC `P = \n. ?i. i < LENGTH l /\ (f (EL i l) = SOME n)` THEN 725 `?d. P d` 726 by (FULL_SIMP_TAC (srw_ss()) [listTheory.EXISTS_MEM] THEN 727 Q.EXISTS_TAC `n` THEN SRW_TAC [][Abbr`P`] THEN 728 METIS_TAC [listTheory.MEM_EL]) THEN 729 Q.ABBREV_TAC `min_d = LEAST x. P x` THEN 730 Q.ABBREV_TAC `Inds = \i . i < LENGTH l /\ (f (EL i l) = SOME min_d)` THEN 731 MAP_EVERY Q.EXISTS_TAC [`LEAST x. Inds(x)`, `min_d`] THEN 732 LEAST_ELIM_TAC THEN CONJ_TAC THENL [ 733 SRW_TAC [][Abbr`Inds`, Abbr`min_d`] THEN 734 LEAST_ELIM_TAC THEN SRW_TAC [][] THEN1 METIS_TAC [] THEN 735 Q.UNABBREV_TAC `P` THEN 736 FULL_SIMP_TAC (srw_ss()) [] THEN 737 METIS_TAC [], 738 SIMP_TAC (srw_ss()) [] THEN Q.UNABBREV_TAC `Inds` THEN 739 ASM_SIMP_TAC (srw_ss()) [] THEN Q.X_GEN_TAC `n` THEN 740 STRIP_TAC THEN Q.X_GEN_TAC `i` THEN STRIP_TAC THEN 741 Cases_on `f (EL i l)` THEN SRW_TAC [][] THENL [ 742 `P x` by (SRW_TAC [][Abbr`P`] THEN METIS_TAC []) THEN 743 Q.UNABBREV_TAC `min_d` THEN LEAST_ELIM_TAC THEN 744 SRW_TAC [][] THEN1 METIS_TAC [] THEN 745 METIS_TAC [DECIDE ``x <= y <=> ~(y < x)``], 746 `P x` by (SRW_TAC [][Abbr`P`] THEN METIS_TAC []) THEN 747 Q.UNABBREV_TAC `min_d` THEN LEAST_ELIM_TAC THEN 748 CONJ_TAC THEN1 METIS_TAC [] THEN 749 Q.X_GEN_TAC `m` THEN STRIP_TAC THEN 750 `(LEAST x. P x) = m` 751 by (LEAST_ELIM_TAC THEN SRW_TAC [][] THEN1 METIS_TAC [] THEN 752 METIS_TAC [DECIDE ``(x = y) <=> ~(x < y) /\ ~(y < x)``]) THEN 753 POP_ASSUM SUBST_ALL_TAC THEN 754 `m <= x` by METIS_TAC [DECIDE ``~(x < y) <=> y <= x``] THEN 755 Q_TAC SUFF_TAC `~(m = x)` THEN1 DECIDE_TAC THEN 756 METIS_TAC [] 757 ] 758 ]); 759 760val mmindex_unique = store_thm( 761 "mmindex_unique", 762 ``is_mmindex f l i m ==> !j n. is_mmindex f l j n <=> (j = i) /\ (n = m)``, 763 SIMP_TAC (srw_ss()) [EQ_IMP_THM] THEN 764 SIMP_TAC (srw_ss()) [is_mmindex_def] THEN 765 STRIP_TAC THEN REPEAT GEN_TAC THEN STRIP_TAC THEN 766 Q_TAC SUFF_TAC `~(j < i) /\ ~(i < j) /\ ~(n < m) /\ ~(m < n)` 767 THEN1 DECIDE_TAC THEN 768 REPEAT STRIP_TAC THEN 769 METIS_TAC [DECIDE ``~(x < y /\ y <= x)``, 770 optionTheory.SOME_11, optionTheory.NOT_SOME_NONE]); 771 772val mmindex_bump = prove( 773 ``(f x = NONE) ==> (is_mmindex f (x::t) (SUC j) n = is_mmindex f t j n)``, 774 SRW_TAC [][EQ_IMP_THM, is_mmindex_def] THENL [ 775 FIRST_X_ASSUM (Q.SPEC_THEN `SUC i` MP_TAC) THEN 776 SRW_TAC [][], 777 Cases_on `i` THEN SRW_TAC [][] THEN 778 FULL_SIMP_TAC (srw_ss()) [] 779 ]); 780 781(* set up the induction principle the final proof will use *) 782val WF_ltlt = prove( 783 ``WF ((<) LEX (<))``, 784 SRW_TAC [][prim_recTheory.WF_LESS, pairTheory.WF_LEX]); 785val ltlt_induction = MATCH_MP relationTheory.WF_INDUCTION_THM WF_ltlt 786 787(* this or something like it is in rich_listTheory - am tempted to put it 788 in listTheory *) 789val EL_APPEND = prove( 790 ``!l1 l2 n. n < LENGTH l1 + LENGTH l2 ==> 791 (EL n (l1 ++ l2) = 792 if n < LENGTH l1 then EL n l1 793 else EL (n - LENGTH l1) l2)``, 794 Induct THEN SRW_TAC [][] THENL [ 795 Cases_on `n` THEN 796 FULL_SIMP_TAC (srw_ss()) [arithmeticTheory.ADD_CLAUSES], 797 Cases_on `n` THEN FULL_SIMP_TAC (srw_ss()) [] THEN 798 FULL_SIMP_TAC (srw_ss()) [arithmeticTheory.ADD_CLAUSES] 799 ]); 800 801val optmin_EQ_NONE = prove( 802 ``(optmin n m = NONE) <=> (n = NONE) /\ (m = NONE)``, 803 Cases_on `n` THEN Cases_on `m` THEN SRW_TAC [][optmin_def]); 804 805val mem_bf_flatten = store_thm( 806 "mem_bf_flatten", 807 ``exists ((=)x) (bf_flatten tlist) = EXISTS (mem x) tlist``, 808 EQ_TAC THENL [ 809 METIS_TAC [exists_bf_flatten], 810 Q_TAC SUFF_TAC 811 `!p tlist x. 812 (SND p = @i. ?d. is_mmindex (mindepth x) tlist i d) /\ 813 (FST p = THE (mindepth x (EL (SND p) tlist))) /\ 814 EXISTS (mem x) tlist ==> 815 exists ((=) x) (bf_flatten tlist)` THEN1 816 SRW_TAC [][pairTheory.FORALL_PROD] THEN 817 HO_MATCH_MP_TAC ltlt_induction THEN 818 SIMP_TAC (srw_ss()) [pairTheory.FORALL_PROD] THEN 819 MAP_EVERY Q.X_GEN_TAC [`td`, `ld`] THEN 820 SRW_TAC [DNF_ss][pairTheory.LEX_DEF] THEN 821 `EXISTS (\e. ?n. mindepth x e = SOME n) tlist` 822 by (FULL_SIMP_TAC (srw_ss()) [listTheory.EXISTS_MEM] THEN 823 METIS_TAC [mem_mindepth]) THEN 824 `?i d. is_mmindex (mindepth x) tlist i d` 825 by METIS_TAC [mmindex_EXISTS] THEN 826 `!j n. is_mmindex (mindepth x) tlist j n <=> (j = i) /\ (n = d)` 827 by METIS_TAC [mmindex_unique] THEN 828 FULL_SIMP_TAC (srw_ss()) [] THEN 829 `mindepth x (EL i tlist) = SOME d` by METIS_TAC [is_mmindex_def] THEN 830 FULL_SIMP_TAC (srw_ss()) [] THEN 831 `?h t. tlist = h::t` 832 by METIS_TAC [listTheory.list_CASES, listTheory.EXISTS_DEF] THEN 833 `(h = Lf) \/ ?a t1 t2. h = Nd a t1 t2` by METIS_TAC [lbtree_cases] THENL [ 834 SRW_TAC [][bf_flatten_def] THEN 835 `?i0. i = SUC i0` 836 by (Cases_on `i` THEN FULL_SIMP_TAC (srw_ss()) [mindepth_thm]) THEN 837 `is_mmindex (mindepth x) (Lf::t) (SUC i0) d` by SRW_TAC [][] THEN 838 `is_mmindex (mindepth x) t i0 d` 839 by METIS_TAC [mmindex_bump, mindepth_thm] THEN 840 `!j n. is_mmindex (mindepth x) t j n <=> (j = i0) /\ (n = d)` 841 by METIS_TAC [mmindex_unique] THEN 842 FULL_SIMP_TAC (srw_ss()) [] THEN 843 FIRST_X_ASSUM (MP_TAC o SPECL [``t : 'a lbtree list``, ``x:'a``]) THEN 844 ASM_SIMP_TAC (srw_ss() ++ ARITH_ss) [], 845 846 SRW_TAC [][bf_flatten_def] THEN 847 Cases_on `x = a` THEN SRW_TAC [][] THEN 848 Cases_on `i` THENL [ 849 REPEAT (Q.PAT_X_ASSUM `EXISTS P l` (K ALL_TAC)) THEN 850 FULL_SIMP_TAC (srw_ss()) [] THEN 851 FULL_SIMP_TAC (srw_ss()) [mindepth_thm] THEN 852 Cases_on `mindepth x t1` THENL [ 853 Cases_on `mindepth x t2` THEN 854 FULL_SIMP_TAC (srw_ss()) [optmin_def] THEN 855 `mem x t2` by METIS_TAC [depth_mem, mindepth_depth] THEN 856 FIRST_X_ASSUM 857 (MP_TAC o 858 SPECL [``(t:'a lbtree list) ++ [t1; t2]``, ``x:'a``]) THEN 859 SRW_TAC [][] THEN FIRST_X_ASSUM MATCH_MP_TAC THEN 860 Q_TAC SUFF_TAC 861 `is_mmindex (mindepth x) (t ++ [t1;t2]) (LENGTH t + 1) x'` 862 THEN1 (DISCH_THEN (ASSUME_TAC o MATCH_MP mmindex_unique) THEN 863 SRW_TAC [ARITH_ss][EL_APPEND]) THEN 864 `is_mmindex (mindepth x) (Nd a t1 t2::t) 0 (SUC x')` 865 by SRW_TAC [][] THEN 866 POP_ASSUM MP_TAC THEN 867 FIRST_X_ASSUM (K ALL_TAC o assert (is_forall o concl)) THEN 868 SRW_TAC [][is_mmindex_def] THENL [ 869 SRW_TAC [ARITH_ss][EL_APPEND], 870 Cases_on `i < LENGTH t` THENL [ 871 SRW_TAC [][EL_APPEND] THEN 872 FIRST_X_ASSUM (Q.SPEC_THEN `SUC i` MP_TAC) THEN 873 SRW_TAC [][] THEN SRW_TAC [ARITH_ss][], 874 SRW_TAC [ARITH_ss][EL_APPEND] THEN 875 `(i = LENGTH t) \/ (i = SUC (LENGTH t))` by DECIDE_TAC THENL [ 876 SRW_TAC [][], 877 SRW_TAC [ARITH_ss][DECIDE ``SUC x - x = SUC 0``] 878 ] 879 ] 880 ], 881 Cases_on `mindepth x t2` THENL [ 882 FULL_SIMP_TAC (srw_ss()) [optmin_def] THEN 883 `mem x t1` by METIS_TAC [depth_mem, mindepth_depth] THEN 884 FIRST_X_ASSUM 885 (MP_TAC o 886 SPECL [``(t:'a lbtree list) ++ [t1; t2]``, ``x:'a``]) THEN 887 SRW_TAC [][] THEN FIRST_X_ASSUM MATCH_MP_TAC THEN 888 Q_TAC SUFF_TAC 889 `is_mmindex (mindepth x) (t ++ [t1;t2]) (LENGTH t) x'` 890 THEN1 (DISCH_THEN (ASSUME_TAC o MATCH_MP mmindex_unique) THEN 891 SRW_TAC [ARITH_ss][EL_APPEND]) THEN 892 `is_mmindex (mindepth x) (Nd a t1 t2::t) 0 (SUC x')` 893 by SRW_TAC [][] THEN 894 POP_ASSUM MP_TAC THEN 895 FIRST_X_ASSUM (K ALL_TAC o assert (is_forall o concl)) THEN 896 SRW_TAC [ARITH_ss][is_mmindex_def, EL_APPEND] THEN 897 Cases_on `i < LENGTH t` THENL [ 898 SRW_TAC [][] THEN 899 FIRST_X_ASSUM (Q.SPEC_THEN `SUC i` MP_TAC) THEN 900 ASM_SIMP_TAC (srw_ss() ++ DNF_ss ++ ARITH_ss) [], 901 `(i = LENGTH t) \/ (i = LENGTH t + 1)` by DECIDE_TAC 902 THENL [ 903 SRW_TAC [][], 904 SRW_TAC [][DECIDE ``x + 1 - x = 1``] 905 ] 906 ], 907 FULL_SIMP_TAC (srw_ss()) [optmin_def] THEN 908 `mem x t1 /\ mem x t2` 909 by METIS_TAC [depth_mem, mindepth_depth] THEN 910 FIRST_X_ASSUM 911 (MP_TAC o 912 SPECL [``(t:'a lbtree list) ++ [t1;t2]``, ``x:'a``]) THEN 913 SRW_TAC [][] THEN FIRST_X_ASSUM MATCH_MP_TAC THEN 914 Cases_on `x' < x''` THENL [ 915 Q_TAC SUFF_TAC 916 `is_mmindex (mindepth x) (t ++ [t1;t2]) (LENGTH t) x'` 917 THEN1 (DISCH_THEN (ASSUME_TAC o 918 MATCH_MP mmindex_unique) THEN 919 SRW_TAC [ARITH_ss][EL_APPEND, 920 arithmeticTheory.MIN_DEF]) THEN 921 `is_mmindex (mindepth x) (Nd a t1 t2::t) 0 (SUC x')` 922 by SRW_TAC [][arithmeticTheory.MIN_DEF] THEN 923 POP_ASSUM MP_TAC THEN 924 FIRST_X_ASSUM (K ALL_TAC o assert (is_forall o concl)) THEN 925 SRW_TAC [ARITH_ss][is_mmindex_def, EL_APPEND] THEN 926 Cases_on `i < LENGTH t` THENL [ 927 SRW_TAC [][] THEN 928 FIRST_X_ASSUM (Q.SPEC_THEN `SUC i` MP_TAC) THEN 929 ASM_SIMP_TAC (srw_ss() ++ DNF_ss ++ ARITH_ss) [], 930 `(i = LENGTH t) \/ (i = LENGTH t + 1)` by DECIDE_TAC 931 THENL [ 932 SRW_TAC [][], 933 SRW_TAC [ARITH_ss][DECIDE ``x + 1 - x = 1``] 934 ] 935 ], 936 Cases_on `x' = x''` THENL [ 937 Q_TAC SUFF_TAC 938 `is_mmindex (mindepth x) (t ++ [t1;t2]) (LENGTH t) x'` 939 THEN1 (DISCH_THEN (ASSUME_TAC o 940 MATCH_MP mmindex_unique) THEN 941 SRW_TAC [ARITH_ss][EL_APPEND, 942 arithmeticTheory.MIN_DEF])THEN 943 `is_mmindex (mindepth x) (Nd a t1 t2::t) 0 (SUC x')` 944 by SRW_TAC [][arithmeticTheory.MIN_DEF] THEN 945 POP_ASSUM MP_TAC THEN 946 FIRST_X_ASSUM (K ALL_TAC o assert (is_forall o concl)) THEN 947 SRW_TAC [ARITH_ss][is_mmindex_def, EL_APPEND] THEN 948 Cases_on `i < LENGTH t` THENL [ 949 SRW_TAC [][] THEN 950 FIRST_X_ASSUM (Q.SPEC_THEN `SUC i` MP_TAC) THEN 951 ASM_SIMP_TAC (srw_ss() ++ DNF_ss ++ ARITH_ss) [], 952 `(i = LENGTH t) \/ (i = LENGTH t + 1)` by DECIDE_TAC 953 THENL [ 954 SRW_TAC [ARITH_ss][], 955 SRW_TAC [ARITH_ss][DECIDE ``x + 1 - x = 1``] 956 ] 957 ], 958 `x'' < x'` by DECIDE_TAC THEN 959 Q_TAC SUFF_TAC 960 `is_mmindex (mindepth x) (t ++ [t1;t2]) (LENGTH t + 1) x''` 961 THEN1 (DISCH_THEN (ASSUME_TAC o 962 MATCH_MP mmindex_unique) THEN 963 SRW_TAC [ARITH_ss][EL_APPEND, 964 arithmeticTheory.MIN_DEF]) THEN 965 `is_mmindex (mindepth x) (Nd a t1 t2::t) 0 (SUC x'')` 966 by SRW_TAC [][arithmeticTheory.MIN_DEF] THEN 967 POP_ASSUM MP_TAC THEN 968 FIRST_X_ASSUM (K ALL_TAC o assert (is_forall o concl)) THEN 969 SRW_TAC [ARITH_ss][is_mmindex_def, EL_APPEND] THEN 970 Cases_on `i < LENGTH t` THENL [ 971 SRW_TAC [][] THEN 972 FIRST_X_ASSUM (Q.SPEC_THEN `SUC i` MP_TAC) THEN 973 ASM_SIMP_TAC (srw_ss() ++ DNF_ss ++ ARITH_ss) [], 974 `(i = LENGTH t) \/ (i = LENGTH t + 1)` by DECIDE_TAC 975 THENL [ 976 SRW_TAC [ARITH_ss][], 977 SRW_TAC [ARITH_ss][DECIDE ``x + 1 - x = 1``] 978 ] 979 ] 980 ] 981 ] 982 ] 983 ], 984 Q_TAC SUFF_TAC 985 `is_mmindex (mindepth x) (t ++ [t1; t2]) n d` 986 THEN1 (DISCH_THEN (ASSUME_TAC o MATCH_MP mmindex_unique) THEN 987 FIRST_X_ASSUM (MP_TAC o 988 SPECL [``(t:'a lbtree list) ++ [t1;t2]``, 989 ``x:'a``]) THEN 990 SRW_TAC [ARITH_ss][] THEN 991 FIRST_X_ASSUM MATCH_MP_TAC THEN 992 `n < LENGTH t` 993 by METIS_TAC [is_mmindex_def, listTheory.LENGTH, 994 DECIDE ``SUC x < SUC y <=> x < y``] THEN 995 FULL_SIMP_TAC (srw_ss() ++ ARITH_ss) 996 [mindepth_thm, EL_APPEND]) THEN 997 `is_mmindex (mindepth x) (Nd a t1 t2::t) (SUC n) d` 998 by SRW_TAC [][] THEN 999 POP_ASSUM MP_TAC THEN 1000 REPEAT (POP_ASSUM (K ALL_TAC)) THEN 1001 SRW_TAC [ARITH_ss][is_mmindex_def, EL_APPEND] THEN 1002 Cases_on `i < LENGTH t` THENL [ 1003 FIRST_X_ASSUM (Q.SPEC_THEN `SUC i` MP_TAC) THEN 1004 SRW_TAC [ARITH_ss][], 1005 `(i = LENGTH t) \/ (i = LENGTH t + 1)` by DECIDE_TAC 1006 THENL [ 1007 SRW_TAC [ARITH_ss][] THEN 1008 FIRST_X_ASSUM (Q.SPEC_THEN `0` MP_TAC) THEN 1009 SRW_TAC [][mindepth_thm, optmin_EQ_NONE] THEN 1010 SRW_TAC [][] THEN 1011 Cases_on `mindepth x t1` THEN 1012 Cases_on `mindepth x t2` THEN 1013 FULL_SIMP_TAC (srw_ss() ++ ARITH_ss) [arithmeticTheory.MIN_DEF, 1014 optmin_def], 1015 SRW_TAC [ARITH_ss][] THEN 1016 FIRST_X_ASSUM (Q.SPEC_THEN `0` MP_TAC) THEN 1017 SRW_TAC [][mindepth_thm, optmin_EQ_NONE] THEN 1018 SRW_TAC [][] THEN 1019 Cases_on `mindepth x t1` THEN 1020 Cases_on `mindepth x t2` THEN 1021 FULL_SIMP_TAC (srw_ss() ++ ARITH_ss) [arithmeticTheory.MIN_DEF, 1022 optmin_def] 1023 ] 1024 ] 1025 ] 1026 ] 1027 ]) 1028 1029(* "delete" all the totally boring auxiliaries *) 1030val _ = app (fn s => remove_ovl_mapping s {Name = s, Thy = "lbtree"}) 1031 ["optmin", "depth", "mindepth", "is_mmindex"] 1032 1033val _ = export_theory () 1034