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