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 162val Nd_11 = store_thm( 163 "Nd_11", 164 ``(Nd a1 t1 u1 = Nd a2 t2 u2) = (a1 = a2) /\ (t1 = t2) /\ (u1 = u2)``, 165 SRW_TAC [][Nd_def, lbtree_abs_11, is_lbtree_rules, Ndrep_11]); 166val _ = export_rewrites ["Nd_11"] 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 351val mem_thm = store_thm( 352 "mem_thm", 353 ``(mem a Lf = F) /\ 354 (mem a (Nd b t1 t2) = (a = b) \/ mem a t1 \/ mem a t2)``, 355 CONJ_TAC THEN CONV_TAC (LAND_CONV (ONCE_REWRITE_CONV [mem_cases])) THEN 356 SRW_TAC [][] THEN METIS_TAC []); 357val _ = export_rewrites ["mem_thm"] 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 408val finite_thm = store_thm( 409 "finite_thm", 410 ``(finite Lf = T) /\ 411 (finite (Nd a t1 t2) = finite t1 /\ finite t2)``, 412 CONJ_TAC THEN 413 CONV_TAC (LAND_CONV (ONCE_REWRITE_CONV [finite_cases])) THEN 414 SRW_TAC [][]); 415val _ = export_rewrites ["finite_thm"] 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 501val exists_bf_flatten = store_thm( 502 "exists_bf_flatten", 503 ``exists ((=)x) (bf_flatten tlist) ==> EXISTS (mem x) tlist``, 504 Q_TAC SUFF_TAC `!l. exists ((=)x) l ==> 505 !tlist. (l = bf_flatten tlist) ==> 506 EXISTS (mem x) tlist` 507 THEN1 METIS_TAC [] THEN 508 HO_MATCH_MP_TAC exists_ind THEN SRW_TAC [][] THENL [ 509 `~EVERY ($= Lf) tlist` 510 by METIS_TAC [LCONS_NOT_NIL, bf_flatten_eq_lnil] THEN 511 `EXISTS ($~ o $= Lf) tlist` 512 by FULL_SIMP_TAC (srw_ss()) [listTheory.NOT_EVERY] THEN 513 `?l1 x l2. EVERY ($~ o $~ o $= Lf) l1 /\ ($~ o $= Lf) x /\ 514 (tlist = l1 ++ (x :: l2))` 515 by METIS_TAC [EXISTS_FIRST] THEN 516 `EVERY ((=) Lf) l1` 517 by FULL_SIMP_TAC (srw_ss() ++ ETA_ss) [combinTheory.o_DEF] 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) [combinTheory.o_DEF] THEN 532 `~(Lf = y)` by FULL_SIMP_TAC (srw_ss()) [] THEN 533 `?a t1 t2. y = Nd a t1 t2` by METIS_TAC [lbtree_cases] THEN 534 FULL_SIMP_TAC (srw_ss()) [bf_flatten_def, bf_flatten_append] THEN 535 FIRST_X_ASSUM (Q.SPEC_THEN `l2 ++ [t1;t2]` MP_TAC) THEN 536 SRW_TAC [][] THEN SRW_TAC [][] THEN 537 (bf_flatten_append |> Q.SPEC `l1` |> Q.INST [`l2`|->`[Nd a t1 t2] ++ l2`] |> MP_TAC) THEN 538 SRW_TAC [][bf_flatten_def] THEN FULL_SIMP_TAC (srw_ss()) [] THEN METIS_TAC [] 539 ]); 540 541(* ---------------------------------------------------------------------- 542 Now it starts to get HIDEOUS. 543 544 Everything in the rest of the file is an indictment of something, 545 maybe 546 * theorem-proving in general; or 547 * HOL4; or 548 * me 549 550 Whatever it is, the following development of what is really a very 551 simple proof is just ghastly. 552 553 The proof is of the converse of the last lemma, that 554 555 EXISTS (mem x) tlist ==> exists ((=) x) (bf_flatten tlist) 556 557 This can't be proved by a structural induction on tlist because of 558 the way tlist actually gets bigger as the flatten proceeds. Nor 559 can we induct on the "size" of tlist (taking into consideration 560 the sizes of the tree-elements) because of the presence of 561 infinite trees. Instead, we induct on the lexicographic product 562 of the minimum depth at which x occurs in a tree, and the minimum 563 index within the list of a tree containing x to that depth. 564 565 This is reduced because of the following: 566 567 If the tree with x in it is not at the head of the list, then 568 the depth number doesn't change, but the index goes down because 569 all of the trees in the list move forward (as a Lf is either 570 discarded from the head of the list, or as a Nd is pulled off, 571 and two sub-trees are enqueued at the back of the list). 572 573 If the tree with x in it is at the head of the list then it's 574 either at the top of the tree in which case we're done, or it 575 moves to the end of the list, but at a reduced depth. 576 577 This reads fairly clearly I think, and feels as if it should be 578 straightforward. It's anything but. 579 580 ---------------------------------------------------------------------- *) 581 582 583(* depth x t n means that x occurs in tree t at depth n *) 584val (depth_rules, depth_ind, depth_cases) = Hol_reln` 585 (!x t1 t2. depth x (Nd x t1 t2) 0) /\ 586 (!m x a t1 t2. depth x t1 m ==> depth x (Nd a t1 t2) (SUC m)) /\ 587 (!m x a t1 t2. depth x t2 m ==> depth x (Nd a t1 t2) (SUC m)) 588`; 589 590val mem_depth = store_thm( 591 "mem_depth", 592 ``!x t. mem x t ==> ?n. depth x t n``, 593 HO_MATCH_MP_TAC mem_ind THEN SRW_TAC [][] THEN 594 METIS_TAC [depth_rules]); 595 596val depth_mem = store_thm( 597 "depth_mem", 598 ``!x t n. depth x t n ==> mem x t``, 599 HO_MATCH_MP_TAC depth_ind THEN SRW_TAC [][]); 600 601(* mindepth x t returns SOME n if x occurs in t at minimum depth n, 602 else NONE *) 603val mindepth_def = Define` 604 mindepth x t = if mem x t then SOME (LEAST n. depth x t n) else NONE 605`; 606 607open numLib 608(* following tactic is used twice in theorem below - yerk *) 609val lelim = REWRITE_RULE [GSYM AND_IMP_INTRO] whileTheory.LEAST_ELIM 610val min_tac = 611 SRW_TAC [ETA_ss][] THEN 612 IMP_RES_THEN (fn th => th |> MATCH_MP lelim |> DEEP_INTRO_TAC) mem_depth THEN 613 Q.X_GEN_TAC `t1d` THEN NTAC 2 STRIP_TAC THEN 614 Q.X_GEN_TAC `t2d` THEN NTAC 2 STRIP_TAC THEN 615 LEAST_ELIM_TAC THEN 616 ONCE_REWRITE_TAC [depth_cases] THEN 617 SRW_TAC [][EXISTS_OR_THM] THEN1 METIS_TAC [] THENL[ 618 `m = t1d` 619 by (SPOSE_NOT_THEN ASSUME_TAC THEN 620 `m < t1d \/ t1d < m` by DECIDE_TAC THENL [ 621 METIS_TAC [], 622 METIS_TAC [DECIDE ``SUC x < SUC y = x < y``, 623 depth_rules] 624 ]) THEN 625 SRW_TAC [][arithmeticTheory.MIN_DEF] THEN 626 SPOSE_NOT_THEN ASSUME_TAC THEN 627 `t2d < m` by DECIDE_TAC THEN 628 METIS_TAC [DECIDE ``SUC x < SUC y = x < y``, depth_rules], 629 `m = t2d` 630 by (SPOSE_NOT_THEN ASSUME_TAC THEN 631 `m < t2d \/ t2d < m` by DECIDE_TAC THENL [ 632 METIS_TAC [], 633 METIS_TAC [DECIDE ``SUC x < SUC y = x < y``, 634 depth_rules] 635 ]) THEN 636 SRW_TAC [][arithmeticTheory.MIN_DEF] THEN 637 METIS_TAC [DECIDE ``SUC x < SUC y = x < y``, depth_rules] 638 ] 639 640(* a minimum function lifted to option type: NONEs are treated as if they 641 are +ve infinity *) 642val optmin_def = Define` 643 (optmin NONE NONE = NONE) /\ 644 (optmin (SOME x) NONE = SOME x) /\ 645 (optmin NONE (SOME y) = SOME y) /\ 646 (optmin (SOME x) (SOME y) = SOME (MIN x y)) 647`; 648 649(* recursive characterisation of mindepth *) 650val mindepth_thm = store_thm( 651 "mindepth_thm", 652 ``(mindepth x Lf = NONE) /\ 653 (mindepth x (Nd a t1 t2) = 654 if x = a then SOME 0 655 else OPTION_MAP SUC (optmin (mindepth x t1) (mindepth x t2)))``, 656 SRW_TAC [][mindepth_def] THEN FULL_SIMP_TAC (srw_ss()) [optmin_def] THENL [ 657 LEAST_ELIM_TAC THEN SRW_TAC [][] THEN1 METIS_TAC [depth_rules] THEN 658 Cases_on `n` THEN SRW_TAC [][] THEN 659 FIRST_X_ASSUM (Q.SPEC_THEN `0` MP_TAC) THEN SRW_TAC [][depth_rules], 660 661 min_tac, 662 min_tac, 663 664 SRW_TAC [ETA_ss][] THEN 665 IMP_RES_THEN (DEEP_INTRO_TAC o MATCH_MP lelim) mem_depth THEN SRW_TAC [][] THEN 666 LEAST_ELIM_TAC THEN SRW_TAC [][] 667 THEN1 METIS_TAC [mem_depth, depth_rules] THEN 668 POP_ASSUM MP_TAC THEN 669 `!n. ~depth x t2 n` by METIS_TAC [depth_mem] THEN 670 ONCE_REWRITE_TAC [depth_cases] THEN SRW_TAC [][] THEN 671 Q_TAC SUFF_TAC `~(m < n) /\ ~(n < m)` THEN1 DECIDE_TAC THEN 672 REPEAT STRIP_TAC THEN METIS_TAC [DECIDE ``SUC x < SUC y = x < y``, 673 depth_rules], 674 675 SRW_TAC [ETA_ss][] THEN 676 IMP_RES_THEN (DEEP_INTRO_TAC o MATCH_MP lelim) mem_depth THEN SRW_TAC [][] THEN 677 LEAST_ELIM_TAC THEN SRW_TAC [][] 678 THEN1 METIS_TAC [mem_depth, depth_rules] THEN 679 POP_ASSUM MP_TAC THEN 680 `!n. ~depth x t1 n` by METIS_TAC [depth_mem] THEN 681 ONCE_REWRITE_TAC [depth_cases] THEN SRW_TAC [][] THEN 682 Q_TAC SUFF_TAC `~(m < n) /\ ~(n < m)` THEN1 DECIDE_TAC THEN 683 REPEAT STRIP_TAC THEN METIS_TAC [DECIDE ``SUC x < SUC y = x < y``, 684 depth_rules] 685 ]); 686 687val mem_mindepth = store_thm( 688 "mem_mindepth", 689 ``!x t. mem x t ==> (?n. mindepth x t = SOME n)``, 690 METIS_TAC [mindepth_def]); 691 692val mindepth_depth = store_thm( 693 "mindepth_depth", 694 ``(mindepth x t = SOME n) ==> depth x t n``, 695 SRW_TAC [][mindepth_def] THEN LEAST_ELIM_TAC THEN SRW_TAC [][] THEN 696 METIS_TAC [mem_depth]); 697 698(* is_mmindex f l n d says that n is the least index of the element with 699 minimal weight (d), as defined by f : 'a -> num option 700 701 Defining this relation as a recursive function to calculate n and d 702 results in a complicated function with accumulators that is very fiddly 703 to prove correct. Its option return type also makes the ultimate proof 704 ugly --- I decided it was a mistake bothering with it. *) 705val is_mmindex_def = Define` 706 is_mmindex f l n d = 707 n < LENGTH l /\ 708 (f (EL n l) = SOME d) /\ 709 !i. i < LENGTH l ==> 710 (f (EL i l) = NONE) \/ 711 ?d'. (f (EL i l) = SOME d') /\ 712 d <= d' /\ (i < n ==> d < d') 713`; 714 715(* the crucial fact about minimums -- two levels of LEAST-ness going on in 716 here *) 717val mmindex_EXISTS = store_thm( 718 "mmindex_EXISTS", 719 ``EXISTS (\e. ?n. f e = SOME n) l ==> ?i m. is_mmindex f l i m``, 720 SRW_TAC [][is_mmindex_def] THEN 721 Q.ABBREV_TAC `P = \n. ?i. i < LENGTH l /\ (f (EL i l) = SOME n)` THEN 722 `?d. P d` 723 by (FULL_SIMP_TAC (srw_ss()) [listTheory.EXISTS_MEM] THEN 724 Q.EXISTS_TAC `n` THEN SRW_TAC [][Abbr`P`] THEN 725 METIS_TAC [listTheory.MEM_EL]) THEN 726 Q.ABBREV_TAC `min_d = LEAST x. P x` THEN 727 Q.ABBREV_TAC `Inds = \i . i < LENGTH l /\ (f (EL i l) = SOME min_d)` THEN 728 MAP_EVERY Q.EXISTS_TAC [`LEAST x. Inds(x)`, `min_d`] THEN 729 LEAST_ELIM_TAC THEN CONJ_TAC THENL [ 730 SRW_TAC [][Abbr`Inds`, Abbr`min_d`] THEN 731 LEAST_ELIM_TAC THEN SRW_TAC [][] THEN1 METIS_TAC [] THEN 732 Q.UNABBREV_TAC `P` THEN 733 FULL_SIMP_TAC (srw_ss()) [] THEN 734 METIS_TAC [], 735 SIMP_TAC (srw_ss()) [] THEN Q.UNABBREV_TAC `Inds` THEN 736 ASM_SIMP_TAC (srw_ss()) [] THEN Q.X_GEN_TAC `n` THEN 737 STRIP_TAC THEN Q.X_GEN_TAC `i` THEN STRIP_TAC THEN 738 Cases_on `f (EL i l)` THEN SRW_TAC [][] THENL [ 739 `P x` by (SRW_TAC [][Abbr`P`] THEN METIS_TAC []) THEN 740 Q.UNABBREV_TAC `min_d` THEN LEAST_ELIM_TAC THEN 741 SRW_TAC [][] THEN1 METIS_TAC [] THEN 742 METIS_TAC [DECIDE ``x <= y = ~(y < x)``], 743 `P x` by (SRW_TAC [][Abbr`P`] THEN METIS_TAC []) THEN 744 Q.UNABBREV_TAC `min_d` THEN LEAST_ELIM_TAC THEN 745 CONJ_TAC THEN1 METIS_TAC [] THEN 746 Q.X_GEN_TAC `m` THEN STRIP_TAC THEN 747 `(LEAST x. P x) = m` 748 by (LEAST_ELIM_TAC THEN SRW_TAC [][] THEN1 METIS_TAC [] THEN 749 METIS_TAC [DECIDE ``(x = y) = ~(x < y) /\ ~(y < x)``]) THEN 750 POP_ASSUM SUBST_ALL_TAC THEN 751 `m <= x` by METIS_TAC [DECIDE ``~(x < y) = y <= x``] THEN 752 Q_TAC SUFF_TAC `~(m = x)` THEN1 DECIDE_TAC THEN 753 METIS_TAC [] 754 ] 755 ]); 756 757val mmindex_unique = store_thm( 758 "mmindex_unique", 759 ``is_mmindex f l i m ==> !j n. is_mmindex f l j n = (j = i) /\ (n = m)``, 760 SIMP_TAC (srw_ss()) [EQ_IMP_THM] THEN 761 SIMP_TAC (srw_ss()) [is_mmindex_def] THEN 762 STRIP_TAC THEN REPEAT GEN_TAC THEN STRIP_TAC THEN 763 Q_TAC SUFF_TAC `~(j < i) /\ ~(i < j) /\ ~(n < m) /\ ~(m < n)` 764 THEN1 DECIDE_TAC THEN 765 REPEAT STRIP_TAC THEN 766 METIS_TAC [DECIDE ``~(x < y /\ y <= x)``, 767 optionTheory.SOME_11, optionTheory.NOT_SOME_NONE]); 768 769val mmindex_bump = prove( 770 ``(f x = NONE) ==> (is_mmindex f (x::t) (SUC j) n = is_mmindex f t j n)``, 771 SRW_TAC [][EQ_IMP_THM, is_mmindex_def] THENL [ 772 FIRST_X_ASSUM (Q.SPEC_THEN `SUC i` MP_TAC) THEN 773 SRW_TAC [][], 774 Cases_on `i` THEN SRW_TAC [][] THEN 775 FULL_SIMP_TAC (srw_ss()) [] 776 ]); 777 778(* set up the induction principle the final proof will use *) 779val WF_ltlt = prove( 780 ``WF ((<) LEX (<))``, 781 SRW_TAC [][prim_recTheory.WF_LESS, pairTheory.WF_LEX]); 782val ltlt_induction = MATCH_MP relationTheory.WF_INDUCTION_THM WF_ltlt 783 784(* this or something like it is in rich_listTheory - am tempted to put it 785 in listTheory *) 786val EL_APPEND = prove( 787 ``!l1 l2 n. n < LENGTH l1 + LENGTH l2 ==> 788 (EL n (l1 ++ l2) = 789 if n < LENGTH l1 then EL n l1 790 else EL (n - LENGTH l1) l2)``, 791 Induct THEN SRW_TAC [][] THENL [ 792 Cases_on `n` THEN 793 FULL_SIMP_TAC (srw_ss()) [arithmeticTheory.ADD_CLAUSES], 794 Cases_on `n` THEN FULL_SIMP_TAC (srw_ss()) [] THEN 795 FULL_SIMP_TAC (srw_ss()) [arithmeticTheory.ADD_CLAUSES] 796 ]); 797 798val optmin_EQ_NONE = prove( 799 ``(optmin n m = NONE) = (n = NONE) /\ (m = NONE)``, 800 Cases_on `n` THEN Cases_on `m` THEN SRW_TAC [][optmin_def]); 801 802val mem_bf_flatten = store_thm( 803 "mem_bf_flatten", 804 ``exists ((=)x) (bf_flatten tlist) = EXISTS (mem x) tlist``, 805 EQ_TAC THENL [ 806 METIS_TAC [exists_bf_flatten], 807 Q_TAC SUFF_TAC 808 `!p tlist x. 809 (SND p = @i. ?d. is_mmindex (mindepth x) tlist i d) /\ 810 (FST p = THE (mindepth x (EL (SND p) tlist))) /\ 811 EXISTS (mem x) tlist ==> 812 exists ((=) x) (bf_flatten tlist)` THEN1 813 SRW_TAC [][pairTheory.FORALL_PROD] THEN 814 HO_MATCH_MP_TAC ltlt_induction THEN 815 SIMP_TAC (srw_ss()) [pairTheory.FORALL_PROD] THEN 816 MAP_EVERY Q.X_GEN_TAC [`td`, `ld`] THEN 817 SRW_TAC [DNF_ss][pairTheory.LEX_DEF] THEN 818 `EXISTS (\e. ?n. mindepth x e = SOME n) tlist` 819 by (FULL_SIMP_TAC (srw_ss()) [listTheory.EXISTS_MEM] THEN 820 METIS_TAC [mem_mindepth]) THEN 821 `?i d. is_mmindex (mindepth x) tlist i d` 822 by METIS_TAC [mmindex_EXISTS] THEN 823 `!j n. is_mmindex (mindepth x) tlist j n = (j = i) /\ (n = d)` 824 by METIS_TAC [mmindex_unique] THEN 825 FULL_SIMP_TAC (srw_ss()) [] THEN 826 `mindepth x (EL i tlist) = SOME d` by METIS_TAC [is_mmindex_def] THEN 827 FULL_SIMP_TAC (srw_ss()) [] THEN 828 `?h t. tlist = h::t` 829 by METIS_TAC [listTheory.list_CASES, listTheory.EXISTS_DEF] THEN 830 `(h = Lf) \/ ?a t1 t2. h = Nd a t1 t2` by METIS_TAC [lbtree_cases] THENL [ 831 SRW_TAC [][bf_flatten_def] THEN 832 `?i0. i = SUC i0` 833 by (Cases_on `i` THEN FULL_SIMP_TAC (srw_ss()) [mindepth_thm]) THEN 834 `is_mmindex (mindepth x) (Lf::t) (SUC i0) d` by SRW_TAC [][] THEN 835 `is_mmindex (mindepth x) t i0 d` 836 by METIS_TAC [mmindex_bump, mindepth_thm] THEN 837 `!j n. is_mmindex (mindepth x) t j n = (j = i0) /\ (n = d)` 838 by METIS_TAC [mmindex_unique] THEN 839 FULL_SIMP_TAC (srw_ss()) [] THEN 840 FIRST_X_ASSUM (MP_TAC o SPECL [``t : 'a lbtree list``, ``x:'a``]) THEN 841 ASM_SIMP_TAC (srw_ss() ++ ARITH_ss) [], 842 843 SRW_TAC [][bf_flatten_def] THEN 844 Cases_on `x = a` THEN SRW_TAC [][] THEN 845 Cases_on `i` THENL [ 846 REPEAT (Q.PAT_X_ASSUM `EXISTS P l` (K ALL_TAC)) THEN 847 FULL_SIMP_TAC (srw_ss()) [] THEN 848 FULL_SIMP_TAC (srw_ss()) [mindepth_thm] THEN 849 Cases_on `mindepth x t1` THENL [ 850 Cases_on `mindepth x t2` THEN 851 FULL_SIMP_TAC (srw_ss()) [optmin_def] THEN 852 `mem x t2` by METIS_TAC [depth_mem, mindepth_depth] THEN 853 FIRST_X_ASSUM 854 (MP_TAC o 855 SPECL [``(t:'a lbtree list) ++ [t1; t2]``, ``x:'a``]) THEN 856 SRW_TAC [][] THEN FIRST_X_ASSUM MATCH_MP_TAC THEN 857 Q_TAC SUFF_TAC 858 `is_mmindex (mindepth x) (t ++ [t1;t2]) (LENGTH t + 1) x'` 859 THEN1 (DISCH_THEN (ASSUME_TAC o MATCH_MP mmindex_unique) THEN 860 SRW_TAC [ARITH_ss][EL_APPEND]) THEN 861 `is_mmindex (mindepth x) (Nd a t1 t2::t) 0 (SUC x')` 862 by SRW_TAC [][] THEN 863 POP_ASSUM MP_TAC THEN 864 FIRST_X_ASSUM (K ALL_TAC o assert (is_forall o concl)) THEN 865 SRW_TAC [][is_mmindex_def] THENL [ 866 SRW_TAC [ARITH_ss][EL_APPEND], 867 Cases_on `i < LENGTH t` THENL [ 868 SRW_TAC [][EL_APPEND] THEN 869 FIRST_X_ASSUM (Q.SPEC_THEN `SUC i` MP_TAC) THEN 870 SRW_TAC [][] THEN SRW_TAC [ARITH_ss][], 871 SRW_TAC [ARITH_ss][EL_APPEND] THEN 872 `(i = LENGTH t) \/ (i = SUC (LENGTH t))` by DECIDE_TAC THENL [ 873 SRW_TAC [][], 874 SRW_TAC [ARITH_ss][DECIDE ``SUC x - x = SUC 0``] 875 ] 876 ] 877 ], 878 Cases_on `mindepth x t2` THENL [ 879 FULL_SIMP_TAC (srw_ss()) [optmin_def] THEN 880 `mem x t1` by METIS_TAC [depth_mem, mindepth_depth] THEN 881 FIRST_X_ASSUM 882 (MP_TAC o 883 SPECL [``(t:'a lbtree list) ++ [t1; t2]``, ``x:'a``]) THEN 884 SRW_TAC [][] THEN FIRST_X_ASSUM MATCH_MP_TAC THEN 885 Q_TAC SUFF_TAC 886 `is_mmindex (mindepth x) (t ++ [t1;t2]) (LENGTH t) x'` 887 THEN1 (DISCH_THEN (ASSUME_TAC o MATCH_MP mmindex_unique) THEN 888 SRW_TAC [ARITH_ss][EL_APPEND]) THEN 889 `is_mmindex (mindepth x) (Nd a t1 t2::t) 0 (SUC x')` 890 by SRW_TAC [][] THEN 891 POP_ASSUM MP_TAC THEN 892 FIRST_X_ASSUM (K ALL_TAC o assert (is_forall o concl)) THEN 893 SRW_TAC [ARITH_ss][is_mmindex_def, EL_APPEND] THEN 894 Cases_on `i < LENGTH t` THENL [ 895 SRW_TAC [][] THEN 896 FIRST_X_ASSUM (Q.SPEC_THEN `SUC i` MP_TAC) THEN 897 ASM_SIMP_TAC (srw_ss() ++ DNF_ss ++ ARITH_ss) [], 898 `(i = LENGTH t) \/ (i = LENGTH t + 1)` by DECIDE_TAC 899 THENL [ 900 SRW_TAC [][], 901 SRW_TAC [][DECIDE ``x + 1 - x = 1``] 902 ] 903 ], 904 FULL_SIMP_TAC (srw_ss()) [optmin_def] THEN 905 `mem x t1 /\ mem x t2` 906 by METIS_TAC [depth_mem, mindepth_depth] THEN 907 FIRST_X_ASSUM 908 (MP_TAC o 909 SPECL [``(t:'a lbtree list) ++ [t1;t2]``, ``x:'a``]) THEN 910 SRW_TAC [][] THEN FIRST_X_ASSUM MATCH_MP_TAC THEN 911 Cases_on `x' < x''` THENL [ 912 Q_TAC SUFF_TAC 913 `is_mmindex (mindepth x) (t ++ [t1;t2]) (LENGTH t) x'` 914 THEN1 (DISCH_THEN (ASSUME_TAC o 915 MATCH_MP mmindex_unique) THEN 916 SRW_TAC [ARITH_ss][EL_APPEND, 917 arithmeticTheory.MIN_DEF]) THEN 918 `is_mmindex (mindepth x) (Nd a t1 t2::t) 0 (SUC x')` 919 by SRW_TAC [][arithmeticTheory.MIN_DEF] THEN 920 POP_ASSUM MP_TAC THEN 921 FIRST_X_ASSUM (K ALL_TAC o assert (is_forall o concl)) THEN 922 SRW_TAC [ARITH_ss][is_mmindex_def, EL_APPEND] THEN 923 Cases_on `i < LENGTH t` THENL [ 924 SRW_TAC [][] THEN 925 FIRST_X_ASSUM (Q.SPEC_THEN `SUC i` MP_TAC) THEN 926 ASM_SIMP_TAC (srw_ss() ++ DNF_ss ++ ARITH_ss) [], 927 `(i = LENGTH t) \/ (i = LENGTH t + 1)` by DECIDE_TAC 928 THENL [ 929 SRW_TAC [][], 930 SRW_TAC [ARITH_ss][DECIDE ``x + 1 - x = 1``] 931 ] 932 ], 933 Cases_on `x' = x''` THENL [ 934 Q_TAC SUFF_TAC 935 `is_mmindex (mindepth x) (t ++ [t1;t2]) (LENGTH t) x'` 936 THEN1 (DISCH_THEN (ASSUME_TAC o 937 MATCH_MP mmindex_unique) THEN 938 SRW_TAC [ARITH_ss][EL_APPEND, 939 arithmeticTheory.MIN_DEF])THEN 940 `is_mmindex (mindepth x) (Nd a t1 t2::t) 0 (SUC x')` 941 by SRW_TAC [][arithmeticTheory.MIN_DEF] THEN 942 POP_ASSUM MP_TAC THEN 943 FIRST_X_ASSUM (K ALL_TAC o assert (is_forall o concl)) THEN 944 SRW_TAC [ARITH_ss][is_mmindex_def, EL_APPEND] THEN 945 Cases_on `i < LENGTH t` THENL [ 946 SRW_TAC [][] THEN 947 FIRST_X_ASSUM (Q.SPEC_THEN `SUC i` MP_TAC) THEN 948 ASM_SIMP_TAC (srw_ss() ++ DNF_ss ++ ARITH_ss) [], 949 `(i = LENGTH t) \/ (i = LENGTH t + 1)` by DECIDE_TAC 950 THENL [ 951 SRW_TAC [ARITH_ss][], 952 SRW_TAC [ARITH_ss][DECIDE ``x + 1 - x = 1``] 953 ] 954 ], 955 `x'' < x'` by DECIDE_TAC THEN 956 Q_TAC SUFF_TAC 957 `is_mmindex (mindepth x) (t ++ [t1;t2]) (LENGTH t + 1) x''` 958 THEN1 (DISCH_THEN (ASSUME_TAC o 959 MATCH_MP mmindex_unique) THEN 960 SRW_TAC [ARITH_ss][EL_APPEND, 961 arithmeticTheory.MIN_DEF]) THEN 962 `is_mmindex (mindepth x) (Nd a t1 t2::t) 0 (SUC x'')` 963 by SRW_TAC [][arithmeticTheory.MIN_DEF] THEN 964 POP_ASSUM MP_TAC THEN 965 FIRST_X_ASSUM (K ALL_TAC o assert (is_forall o concl)) THEN 966 SRW_TAC [ARITH_ss][is_mmindex_def, EL_APPEND] THEN 967 Cases_on `i < LENGTH t` THENL [ 968 SRW_TAC [][] THEN 969 FIRST_X_ASSUM (Q.SPEC_THEN `SUC i` MP_TAC) THEN 970 ASM_SIMP_TAC (srw_ss() ++ DNF_ss ++ ARITH_ss) [], 971 `(i = LENGTH t) \/ (i = LENGTH t + 1)` by DECIDE_TAC 972 THENL [ 973 SRW_TAC [ARITH_ss][], 974 SRW_TAC [ARITH_ss][DECIDE ``x + 1 - x = 1``] 975 ] 976 ] 977 ] 978 ] 979 ] 980 ], 981 Q_TAC SUFF_TAC 982 `is_mmindex (mindepth x) (t ++ [t1; t2]) n d` 983 THEN1 (DISCH_THEN (ASSUME_TAC o MATCH_MP mmindex_unique) THEN 984 FIRST_X_ASSUM (MP_TAC o 985 SPECL [``(t:'a lbtree list) ++ [t1;t2]``, 986 ``x:'a``]) THEN 987 SRW_TAC [ARITH_ss][] THEN 988 FIRST_X_ASSUM MATCH_MP_TAC THEN 989 `n < LENGTH t` 990 by METIS_TAC [is_mmindex_def, listTheory.LENGTH, 991 DECIDE ``SUC x < SUC y = x < y``] THEN 992 FULL_SIMP_TAC (srw_ss() ++ ARITH_ss) 993 [mindepth_thm, EL_APPEND]) THEN 994 `is_mmindex (mindepth x) (Nd a t1 t2::t) (SUC n) d` 995 by SRW_TAC [][] THEN 996 POP_ASSUM MP_TAC THEN 997 REPEAT (POP_ASSUM (K ALL_TAC)) THEN 998 SRW_TAC [ARITH_ss][is_mmindex_def, EL_APPEND] THEN 999 Cases_on `i < LENGTH t` THENL [ 1000 FIRST_X_ASSUM (Q.SPEC_THEN `SUC i` MP_TAC) THEN 1001 SRW_TAC [ARITH_ss][], 1002 `(i = LENGTH t) \/ (i = LENGTH t + 1)` by DECIDE_TAC 1003 THENL [ 1004 SRW_TAC [ARITH_ss][] THEN 1005 FIRST_X_ASSUM (Q.SPEC_THEN `0` MP_TAC) THEN 1006 SRW_TAC [][mindepth_thm, optmin_EQ_NONE] THEN 1007 SRW_TAC [][] THEN 1008 Cases_on `mindepth x t1` THEN 1009 Cases_on `mindepth x t2` THEN 1010 FULL_SIMP_TAC (srw_ss() ++ ARITH_ss) [arithmeticTheory.MIN_DEF, 1011 optmin_def], 1012 SRW_TAC [ARITH_ss][] THEN 1013 FIRST_X_ASSUM (Q.SPEC_THEN `0` MP_TAC) THEN 1014 SRW_TAC [][mindepth_thm, optmin_EQ_NONE] THEN 1015 SRW_TAC [][] THEN 1016 Cases_on `mindepth x t1` THEN 1017 Cases_on `mindepth x t2` THEN 1018 FULL_SIMP_TAC (srw_ss() ++ ARITH_ss) [arithmeticTheory.MIN_DEF, 1019 optmin_def] 1020 ] 1021 ] 1022 ] 1023 ] 1024 ]) 1025 1026(* "delete" all the totally boring auxiliaries *) 1027val _ = app (fn s => remove_ovl_mapping s {Name = s, Thy = "lbtree"}) 1028 ["optmin", "depth", "mindepth", "is_mmindex"] 1029 1030val _ = export_theory () 1031