enumeralScript.sml
1(* file HS/PIN/enumeralScript.sml, created 4/15/13 F.L. Morris *)
2(* PIN-based finite set representation; name a homage to numeralTheory *)
3(* Revision of 5/12/13 - bringing back bt & bl to avoid finiteness hyps. *)
4Theory enumeral
5Ancestors
6 pred_set relation res_quan toto list
7Libs
8 pred_setLib res_quanLib
9
10
11(* app load ["totoTheory", "res_quanLib"]; *)
12
13val _ = set_trace "Unicode" 0;
14val cpn_nchotomy = TypeBase.nchotomy_of ``:ordering``
15Type cpn[local] = “:ordering”
16val _ = ParseExtras.temp_loose_equality()
17
18(* "enumeral" for "enumerated finite set", wordplay on "NUMERAL" *)
19
20(* My habitual abbreviations: *)
21
22val AR = ASM_REWRITE_TAC [];
23fun ulist x = [x];
24
25Datatype: bt = nt | node bt 'a bt
26End
27Datatype: bl = nbl | zerbl bl | onebl 'a ('a bt) bl
28End
29
30val bt_size_def = definition "bt_size_def";
31val bl_size_def = definition "bl_size_def";
32
33(* helper function, BL_ACCUM, for use only by BL_CONS: *)
34
35Definition BL_ACCUM: (BL_ACCUM (a:'a) ac nbl = onebl a ac nbl)
36 /\ (BL_ACCUM a ac (zerbl bl) = onebl a ac bl)
37 /\ (BL_ACCUM a ac (onebl r rft bl) =
38 zerbl (BL_ACCUM a (node ac r rft) bl))
39End
40
41Definition BL_CONS: BL_CONS (a:'a) bl = BL_ACCUM a nt bl
42End
43
44Definition list_to_bl: (list_to_bl [] = nbl)
45 /\ (list_to_bl (a:'a :: l) = BL_CONS a (list_to_bl l))
46End
47
48(* flatten a bt back to a list, without and with an accumulating parameter. *)
49
50Definition bt_to_list:
51 (bt_to_list (nt:'a bt) = []) /\
52 (bt_to_list (node l x r) = bt_to_list l ++ [x] ++ bt_to_list r)
53End
54
55Definition bt_to_list_ac:
56 (bt_to_list_ac (nt:'a bt) m = m) /\
57 (bt_to_list_ac (node l x r) m = bt_to_list_ac l (x :: bt_to_list_ac r m))
58End
59
60Theorem bt_to_list_ac_thm[local]:
61 !t:'a bt m. bt_to_list_ac t m = bt_to_list t ++ m
62Proof
63Induct THEN SRW_TAC [] [bt_to_list, bt_to_list_ac]
64QED
65
66Theorem bt_to_list_thm:
67 !t:'a bt. bt_to_list t = bt_to_list_ac t []
68Proof
69REWRITE_TAC [bt_to_list_ac_thm, APPEND_NIL]
70QED
71
72(* Although we should have no need to prove in HOL that bl's built with
73BL_CONS have the desirable balance properties that make them efficient,
74we do need a lemma about the size of bl's to support inductive definitions.*)
75
76(* helper function, bt_rev, for use here and below by bt_to_bl: *)
77
78Definition bt_rev:
79 (bt_rev (nt:'a bt) bl = bl)
80 /\ (bt_rev (node lft r rft) bl = bt_rev lft (onebl r rft bl))
81End
82
83Definition K2: K2 (a:'a) = 2
84End
85
86Theorem bt_rev_size[local]:
87 !ft bl:'a bl. bl_size K2 (bt_rev ft bl) = bt_size K2 ft + bl_size K2 bl
88Proof
89Induct THEN
90ASM_REWRITE_TAC [bl_size_def, bt_size_def, K2,bt_rev,arithmeticTheory.ADD] THEN
91SIMP_TAC arith_ss []
92QED
93
94(* How to turn a bl into a bt (unreversibly). bl_rev is named after the
95 classical helper function for reverse (listTheory's REV). *)
96
97Definition bl_rev: (bl_rev ft (nbl:'a bl) = ft) /\
98 (bl_rev ft (zerbl b) = bl_rev ft b) /\
99 (bl_rev ft (onebl a f b) = bl_rev (node ft a f) b)
100End
101
102Definition bl_to_bt: bl_to_bt = bl_rev (nt:'a bt)
103End
104
105(* And how to turn a bt into a condensed bl (or "cl") - zerbls omitted -
106 by dissasembling left subtrees only. Helper bt_rev is defined above. *)
107
108Definition bt_to_bl: bt_to_bl (t:'a bt) = bt_rev t nbl
109End
110
111(* Likely to be needed: *)
112
113Theorem slinky[local]:
114 !(t:'a bt) bb. bl_to_bt (bt_rev t bb) = bl_rev t bb
115Proof
116Induct THENL
117[REWRITE_TAC [bl_to_bt, bt_rev]
118,REPEAT GEN_TAC THEN ASM_REWRITE_TAC [bt_rev, bl_rev]]
119QED
120
121Theorem bt_to_bl_to_bt_ID[local]:
122 !t:'a bt. bl_to_bt (bt_to_bl t) = t
123Proof
124REWRITE_TAC [bt_to_bl, slinky, bl_rev]
125QED
126
127Definition list_to_bt: list_to_bt (l:'c list) = bl_to_bt (list_to_bl l)
128End
129
130(* ***** We use "OL" for strictly ***** *)
131(* ***** ordered lists where the whole element is the key; ***** *)
132(* ***** eventually "ORL" for function-modeling sorted lists. ***** *)
133
134Definition OL: (OL (cmp:'a toto) ([]:'a list) = T) /\
135 (OL cmp (a :: l) = OL cmp l /\
136 (!p. MEM p l ==> (apto cmp a p = LESS)))
137End
138
139(* ***************************************************************** *)
140(* merge sorting for sets here, with initial "s"; plain merge etc. *)
141(* are reserved as names for association-list sorting. *)
142(* ***************************************************************** *)
143
144Definition smerge:
145 (smerge (cmp:'a toto) [] [] = []) /\
146 (smerge cmp (x:'a :: l) [] = x :: l) /\
147 (smerge cmp [] (y:'a :: m) = y :: m) /\
148 (smerge cmp (x :: l) (y :: m) = case apto cmp x y of
149 LESS => x :: (smerge cmp l (y :: m))
150 | EQUAL => x :: (smerge cmp l m)
151 | GREATER => y :: (smerge cmp (x :: l) m))
152End
153
154Theorem smerge_nil:
155 !cmp:'a toto l. (smerge cmp l [] = l) /\ (smerge cmp [] l = l)
156Proof
157REPEAT STRIP_TAC THEN Cases_on `l` THEN REWRITE_TAC [smerge]
158QED
159
160(* corresponding merge_set will need ORL hypotheses, and corresp. merge_ORL
161 will need 3 `merge ... = ... UNION ...` by MATCH_MP_TAC merge_set THEN...*)
162
163Theorem smerge_set[local]:
164 !cmp:'a toto l m. (set (smerge cmp l m) = set l UNION set m)
165Proof
166GEN_TAC THEN Induct THEN
167SRW_TAC [] [smerge, smerge_nil] THEN
168Induct_on `m` THEN
169SRW_TAC [] [smerge, smerge_nil] THEN
170Cases_on `apto cmp h h'` THENL
171[ALL_TAC, `h = h'` by IMP_RES_TAC toto_equal_eq, ALL_TAC] THEN
172SRW_TAC [] [toto_equal_eq] THEN
173RW_TAC bool_ss [toto_equal_eq, EXTENSION, IN_INSERT, IN_UNION, DISJ_ASSOC] THEN
174tautLib.TAUT_TAC
175QED
176
177Theorem smerge_OL:
178 !cmp:'a toto l m. OL cmp l /\ OL cmp m ==> OL cmp (smerge cmp l m)
179Proof
180GEN_TAC THEN Induct THEN
181SRW_TAC [] [smerge, OL, smerge_nil] THEN
182Induct_on `m` THEN
183SRW_TAC [] [smerge, OL, smerge_nil] THEN
184Cases_on `apto cmp h h'` THEN SRW_TAC [] [OL] THENL
185[`MEM p l \/ MEM p (h' :: m)`
186 by (RW_TAC bool_ss [GSYM IN_UNION] THEN
187 ASM_REWRITE_TAC [GSYM smerge_set]) THENL
188 [RES_TAC
189 ,`(p = h') \/ MEM p m` by ASM_REWRITE_TAC [GSYM MEM] THENL
190 [AR, RES_TAC THEN IMP_RES_TAC totoLLtrans
191 ]]
192,`MEM p l \/ MEM p m`
193 by (RW_TAC bool_ss [GSYM IN_UNION] THEN
194 ASM_REWRITE_TAC [GSYM smerge_set]) THENL
195 [RES_TAC
196 ,RES_TAC THEN IMP_RES_TAC totoELtrans
197 ]
198,`MEM p (h :: l) \/ MEM p m`
199 by (RW_TAC bool_ss [GSYM IN_UNION] THEN
200 ASM_REWRITE_TAC [GSYM smerge_set]) THENL
201 [`(p = h) \/ MEM p l` by ASM_REWRITE_TAC [GSYM MEM] THENL
202 [ASM_REWRITE_TAC [GSYM toto_antisym],
203 RES_TAC THEN IMP_RES_TAC totoGLtrans
204 ]
205 ,RES_TAC
206]]
207QED
208
209Definition OL_sublists:
210 (OL_sublists cmp ([]:'a list option list) = T) /\
211 (OL_sublists cmp (NONE :: lol) = OL_sublists cmp lol) /\
212 (OL_sublists cmp (SOME m :: lol) = OL cmp m /\ OL_sublists cmp lol)
213End
214
215val OL_sublists_ind = theorem "OL_sublists_ind";
216
217(* OL_sublists_ind = |- !P. (!cmp. P cmp []) /\
218 (!cmp lol. P cmp lol ==> P cmp (NONE::lol)) /\
219 (!cmp m lol. P cmp lol ==> P cmp (SOME m::lol)) ==> !v v1. P v v1 *)
220
221Definition lol_set:
222 (lol_set ([]:'a list option list) = {}) /\
223 (lol_set (NONE :: lol) = lol_set lol) /\
224 (lol_set (SOME m :: lol) = set m UNION lol_set lol)
225End
226
227Definition incr_smerge:
228 (incr_smerge cmp (l:'a list) [] = [SOME l]) /\
229 (incr_smerge cmp l (NONE :: lol) = SOME l :: lol) /\
230 (incr_smerge cmp l (SOME m :: lol) =
231 NONE :: incr_smerge cmp (smerge cmp l m) lol)
232End
233
234Theorem incr_smerge_set[local]:
235 !cmp lol l:'a list.
236 lol_set (incr_smerge cmp l lol) = set l UNION lol_set lol
237Proof
238HO_MATCH_MP_TAC OL_sublists_ind THEN
239RW_TAC bool_ss [incr_smerge, smerge_set, lol_set, UNION_ASSOC]
240QED
241
242Theorem incr_smerge_OL: !cmp lol l:'a list.
243OL_sublists cmp lol /\ OL cmp l ==> OL_sublists cmp (incr_smerge cmp l lol)
244Proof
245HO_MATCH_MP_TAC OL_sublists_ind THEN
246RW_TAC bool_ss [incr_smerge, smerge_OL, OL_sublists]
247QED
248
249Definition smerge_out:
250 (smerge_out (cmp:'a toto) l ([]:'a list option list) = l) /\
251 (smerge_out cmp l (NONE :: lol) = smerge_out cmp l lol) /\
252 (smerge_out cmp l (SOME m :: lol) = smerge_out cmp (smerge cmp l m) lol)
253End
254
255val smerge_out_ind = theorem "smerge_out_ind";
256
257(* smerge_out_ind = |- !P. (!cmp l. P cmp l []) /\
258 (!cmp l lol. P cmp l lol ==> P cmp l (NONE::lol)) /\
259 (!cmp l m lol. P cmp (smerge cmp l m) lol ==> P cmp l (SOME m::lol)) ==>
260 !v v1 v2. P v v1 v2 *)
261
262Theorem smerge_out_set[local]:
263 !cmp:'a toto l:'a list lol.
264 set (smerge_out cmp l lol) = set l UNION lol_set lol
265Proof
266HO_MATCH_MP_TAC smerge_out_ind THEN
267RW_TAC bool_ss [smerge_out, lol_set, smerge_set, UNION_EMPTY, UNION_ASSOC]
268QED
269
270Theorem smerge_out_OL[local]:
271 !cmp:'a toto l:'a list lol.
272OL cmp l /\ OL_sublists cmp lol ==> OL cmp (smerge_out cmp l lol)
273Proof
274HO_MATCH_MP_TAC smerge_out_ind THEN
275RW_TAC bool_ss [smerge_out, OL_sublists] THEN
276METIS_TAC [smerge_OL]
277QED
278
279Definition incr_sbuild:
280 (incr_sbuild (cmp:'a toto) [] = []) /\
281 (incr_sbuild cmp (x :: l) = incr_smerge cmp [x] (incr_sbuild cmp l))
282End
283
284Theorem incr_sbuild_set[local]:
285 !cmp l:'a list. lol_set (incr_sbuild cmp l) = set l
286Proof
287GEN_TAC THEN Induct THEN
288SRW_TAC [] [lol_set, incr_sbuild, incr_smerge_set, INSERT_UNION_EQ]
289QED
290
291Theorem OL_EMPTY[local]:
292 !cmp:'a toto. OL cmp []
293Proof
294REWRITE_TAC [OL]
295QED
296
297Theorem OL_SING[local]:
298 !cmp:'a toto x. OL cmp [x]
299Proof
300RW_TAC bool_ss [OL, MEM]
301QED
302
303Theorem incr_sbuild_OL[local]:
304 !cmp l:'a list. OL_sublists cmp (incr_sbuild cmp l)
305Proof
306GEN_TAC THEN Induct THEN
307SRW_TAC [] [incr_sbuild, incr_smerge_OL, OL_sublists] THEN
308METIS_TAC [OL_SING, incr_smerge_OL]
309QED
310
311Definition incr_ssort:
312 incr_ssort (cmp:'a toto) l = smerge_out cmp [] (incr_sbuild cmp l)
313End
314
315Theorem incr_ssort_set[local]:
316 !cmp:'a toto l. set (incr_ssort cmp l) = set l
317Proof
318SRW_TAC [] [incr_ssort, smerge_out_set, incr_sbuild_set]
319QED
320
321Theorem incr_ssort_OL[local]:
322 !cmp:'a toto l. OL cmp (incr_ssort cmp l)
323Proof
324REWRITE_TAC [incr_ssort] THEN
325METIS_TAC [incr_sbuild_OL, OL, smerge_out_OL]
326QED
327
328Theorem OL_MEM_EQ[local]:
329 !cmp:'a toto l m. OL cmp l /\ OL cmp m ==>
330 ((!x. MEM x l = MEM x m) <=> (l = m))
331Proof
332GEN_TAC THEN Induct THENL
333[Induct THENL
334 [REWRITE_TAC []
335 ,REPEAT STRIP_TAC THEN EQ_TAC THENL
336 [CONV_TAC LEFT_IMP_FORALL_CONV THEN Q.EXISTS_TAC `h` THEN
337 REWRITE_TAC [MEM]
338 ,REWRITE_TAC [GSYM NOT_CONS_NIL]
339 ]]
340,GEN_TAC THEN Induct THENL
341 [STRIP_TAC THEN EQ_TAC THENL
342 [CONV_TAC LEFT_IMP_FORALL_CONV THEN Q.EXISTS_TAC `h` THEN
343 REWRITE_TAC [MEM]
344 ,REWRITE_TAC [NOT_CONS_NIL]
345 ]
346 ,GEN_TAC THEN REWRITE_TAC [OL, MEM, CONS_11] THEN STRIP_TAC THEN
347 `(!x. MEM x l <=> MEM x m) <=> (l = m)` by RES_TAC THEN
348 EQ_TAC THENL [ALL_TAC, RW_TAC bool_ss []] THEN
349 `~MEM h l /\ ~MEM h' m` by METIS_TAC [CONJUNCT1 toto_glneq] THEN
350 CONV_TAC LEFT_IMP_FORALL_CONV THEN Cases_on `apto cmp h h'` THENL
351 [Q.EXISTS_TAC `h` THEN AR THEN METIS_TAC [totoLLtrans, CONJUNCT1 toto_glneq]
352 ,CONV_TAC EXISTS_IMP_CONV THEN DISCH_TAC THEN
353 `h = h'` by IMP_RES_TAC toto_equal_eq THEN
354 `!x. MEM x l <=> MEM x m` by METIS_TAC[] THEN
355 AR THEN RES_TAC
356 ,Q.EXISTS_TAC `h'` THEN AR THEN IMP_RES_TAC toto_antisym THEN
357 METIS_TAC [totoLLtrans, CONJUNCT1 toto_glneq]
358]]]
359QED
360
361(* *********** end of digression to program sorting ************** *)
362
363(* Define the set represented (according to a total order) by a bt *)
364
365(* Following should really be called "bt_to_set", but ENUMERAL, like
366 NUMERAL, will flag the terms that represent sets as trees. *)
367
368Definition bt_to_set:
369 (ENUMERAL cmp nt = {}) /\
370 (ENUMERAL (cmp:'a toto) (node l x r) =
371 {y | y IN ENUMERAL cmp l /\ (apto cmp y x = LESS)} UNION {x} UNION
372 {z | z IN ENUMERAL cmp r /\ (apto cmp x z = LESS)})
373End
374
375Definition bt_to_set_lb: bt_to_set_lb cmp (lb:'a) t =
376 {x | x IN ENUMERAL cmp t /\ (apto cmp lb x = LESS)}
377End
378
379Definition bt_to_set_ub: bt_to_set_ub cmp t (ub:'a) =
380 {x | x IN ENUMERAL cmp t /\ (apto cmp x ub = LESS)}
381End
382
383Theorem bt_to_set_mut_rec[local]:
384 !cmp:'a toto l x r. ENUMERAL cmp (node l x r) =
385 bt_to_set_ub cmp l x UNION {x} UNION bt_to_set_lb cmp x r
386Proof
387REWRITE_TAC [bt_to_set_lb, bt_to_set_ub] THEN REWRITE_TAC [bt_to_set]
388QED
389
390Definition bt_to_set_lb_ub: bt_to_set_lb_ub cmp lb t (ub:'a) =
391{x | x IN ENUMERAL cmp t /\ (apto cmp lb x = LESS) /\ (apto cmp x ub = LESS)}
392End
393
394Theorem IN_bt_to_set:
395 (!cmp:'a toto y. y IN ENUMERAL cmp nt = F) /\
396 (!cmp:'a toto l x r y. y IN ENUMERAL cmp (node l x r) =
397 y IN ENUMERAL cmp l /\ (apto cmp y x = LESS) \/ (y = x) \/
398 y IN ENUMERAL cmp r /\ (apto cmp x y = LESS))
399Proof
400SRW_TAC [] [bt_to_set] THEN CONV_TAC (DEPTH_CONV SET_SPEC_CONV) THEN
401tautLib.TAUT_TAC
402QED
403
404(* Following look-up function (disguised as two theorems) to make bt's
405 imitate IN on finite sets, may or may not be the reasonable way to go. *)
406
407Theorem NOT_IN_nt = CONJUNCT1 IN_bt_to_set;
408
409(* NOT_IN_nt = |- !cmp y. y IN ENUMERAL cmp nt <=> F *)
410
411Theorem IN_node:
412 !cmp x:'a l y r. x IN ENUMERAL cmp (node l y r) <=> case apto cmp x y of
413 LESS => x IN ENUMERAL cmp l | EQUAL => T | GREATER => x IN ENUMERAL cmp r
414Proof
415SRW_TAC [] [bt_to_set] THEN Cases_on `apto cmp x y` THEN
416(Q.SUBGOAL_THEN `(x = y) = (apto cmp x y = EQUAL)` SUBST1_TAC
417 THEN1 MATCH_ACCEPT_TAC (GSYM toto_equal_eq)) THEN
418IMP_RES_TAC toto_antisym THEN SRW_TAC [] []
419QED
420
421(* Following "mut_rec" theorems seem relevant to conversion to ol's, not to
422 evaluating IN. *)
423
424Theorem bt_to_set_lb_ub_mut_rec[local]:
425 !cmp:'a toto lb l x r ub. bt_to_set_lb_ub cmp lb (node l x r) ub =
426 if apto cmp lb x = LESS then
427 if apto cmp x ub = LESS then
428 bt_to_set_lb_ub cmp lb l x UNION {x} UNION bt_to_set_lb_ub cmp x r ub
429 else
430 bt_to_set_lb_ub cmp lb l ub
431 else
432 bt_to_set_lb_ub cmp lb r ub
433Proof
434SRW_TAC [] [bt_to_set_lb_ub, EXTENSION, IN_bt_to_set] THEN
435EQ_TAC THEN STRIP_TAC THEN AR THEN IMP_RES_TAC totoLLtrans THENL
436[Q.UNDISCH_TAC `apto cmp x' ub = LESS` THEN AR
437,IMP_RES_TAC NOT_EQ_LESS_IMP THEN SRW_TAC [] []
438,Q.UNDISCH_TAC `apto cmp lb x' = LESS` THEN AR
439,IMP_RES_TAC NOT_EQ_LESS_IMP THEN SRW_TAC [] []
440]
441QED
442
443Theorem bt_to_set_lb_mut_rec[local]:
444 !cmp:'a toto lb l x r. bt_to_set_lb cmp lb (node l x r) =
445 if apto cmp lb x = LESS then
446 bt_to_set_lb_ub cmp lb l x UNION {x} UNION bt_to_set_lb cmp x r
447 else
448 bt_to_set_lb cmp lb r
449Proof
450SRW_TAC [] [bt_to_set_lb, bt_to_set_lb_ub, EXTENSION, IN_bt_to_set] THEN
451EQ_TAC THEN STRIP_TAC THEN AR THEN IMP_RES_TAC totoLLtrans THENL
452[Q.UNDISCH_TAC `apto cmp lb x' = LESS` THEN AR
453,IMP_RES_TAC NOT_EQ_LESS_IMP THEN SRW_TAC [] []
454]
455QED
456
457Theorem bt_to_set_ub_mut_rec[local]:
458 !cmp:'a toto ub l x r. bt_to_set_ub cmp (node l x r) ub =
459 if apto cmp x ub = LESS then
460 bt_to_set_ub cmp l x UNION {x} UNION bt_to_set_lb_ub cmp x r ub
461 else
462 bt_to_set_ub cmp l ub
463Proof
464SRW_TAC [] [bt_to_set_ub, bt_to_set_lb_ub, EXTENSION, IN_bt_to_set] THEN
465EQ_TAC THEN STRIP_TAC THEN AR THEN IMP_RES_TAC totoLLtrans THENL
466[Q.UNDISCH_TAC `apto cmp x' ub = LESS` THEN AR
467,IMP_RES_TAC NOT_EQ_LESS_IMP THEN SRW_TAC [] []
468]
469QED
470
471(* ****************************************************************** *)
472(* For computational purposes, we need to go from ENUMERAL-terms to *)
473(* ordered lists of the same elements. Possiibly to no purpose, we *)
474(* supply first a general translation that extracts from any bt at all*)
475(* the list of the same elements as are in bt_to_set of it. Later, we *)
476(* will see that checking for no out-of-order elements separately *)
477(* allows a faster translation by bt_to_list, with about half the *)
478(* comparisons of the general method. (See better_bt_to_ol below.) *)
479(* ****************************************************************** *)
480
481Definition bt_to_ol_lb_ub:
482 (bt_to_ol_lb_ub (cmp:'a toto) lb nt ub = []) /\
483 (bt_to_ol_lb_ub cmp lb (node l x r) ub =
484 if apto cmp lb x = LESS then
485 if apto cmp x ub = LESS then
486 bt_to_ol_lb_ub cmp lb l x ++ [x] ++ bt_to_ol_lb_ub cmp x r ub
487 else bt_to_ol_lb_ub cmp lb l ub
488 else bt_to_ol_lb_ub cmp lb r ub)
489End
490
491Definition bt_to_ol_lb:
492 (bt_to_ol_lb (cmp:'a toto) lb nt = []) /\
493 (bt_to_ol_lb cmp lb (node l x r) =
494 if apto cmp lb x = LESS then
495 bt_to_ol_lb_ub cmp lb l x ++ [x] ++ bt_to_ol_lb cmp x r
496 else bt_to_ol_lb cmp lb r)
497End
498
499Definition bt_to_ol_ub:
500 (bt_to_ol_ub (cmp:'a toto) nt ub = []) /\
501 (bt_to_ol_ub cmp (node l x r) ub =
502 if apto cmp x ub = LESS then
503 bt_to_ol_ub cmp l x ++ [x] ++ bt_to_ol_lb_ub cmp x r ub
504 else bt_to_ol_ub cmp l ub)
505End
506
507Definition bt_to_ol:
508 (bt_to_ol (cmp:'a toto) nt = []) /\
509 (bt_to_ol cmp (node l x r) =
510 bt_to_ol_ub cmp l x ++ [x] ++ bt_to_ol_lb cmp x r)
511End
512
513(* Show ordered lists have the correct sets of elements: *)
514
515Theorem ol_set_lb_ub[local]:
516 !cmp:'a toto t lb ub.
517 bt_to_set_lb_ub cmp lb t ub = set (bt_to_ol_lb_ub cmp lb t ub)
518Proof
519GEN_TAC THEN Induct THEN
520SRW_TAC [] [bt_to_set_lb_ub_mut_rec, bt_to_ol_lb_ub,
521 LIST_TO_SET_APPEND, EXTENSION] THEN
522SRW_TAC [] [NOT_IN_nt, bt_to_set_lb_ub]
523QED
524
525Theorem ol_set_lb[local]:
526 !cmp:'a toto t lb.
527 bt_to_set_lb cmp lb t = set (bt_to_ol_lb cmp lb t)
528Proof
529GEN_TAC THEN Induct THEN
530SRW_TAC [] [bt_to_set_lb_mut_rec, bt_to_ol_lb,
531 LIST_TO_SET_APPEND, EXTENSION, ol_set_lb_ub] THEN
532SRW_TAC [] [NOT_IN_nt, bt_to_set_lb]
533QED
534
535Theorem ol_set_ub[local]:
536 !cmp:'a toto t ub.
537 bt_to_set_ub cmp t ub = set (bt_to_ol_ub cmp t ub)
538Proof
539GEN_TAC THEN Induct THEN
540SRW_TAC [] [bt_to_set_ub_mut_rec, bt_to_ol_ub,
541 LIST_TO_SET_APPEND, EXTENSION, ol_set_lb_ub] THEN
542SRW_TAC [] [NOT_IN_nt, bt_to_set_ub]
543QED
544
545Theorem ol_set:
546 !cmp:'a toto t. ENUMERAL cmp t = set (bt_to_ol cmp t)
547Proof
548GEN_TAC THEN Induct THEN
549SRW_TAC [] [bt_to_set_mut_rec, bt_to_ol,
550 LIST_TO_SET_APPEND, EXTENSION, ol_set_lb, ol_set_ub] THEN
551REWRITE_TAC [NOT_IN_nt]
552QED
553
554(* We have neglected so far to prove that bt_to_ol and its kin produce
555 lists satisfying OL cmp. *)
556
557Theorem list_split_lem[local]:
558 !cmp:'a toto l x r. OL cmp (l ++ [x] ++ r) <=>
559 OL cmp l /\ (!a. a IN set l ==> (apto cmp a x = LESS)) /\
560 OL cmp r /\ (!z. z IN set r ==> (apto cmp x z = LESS))
561Proof
562GEN_TAC THEN Induct THEN SRW_TAC [] [OL] THEN EQ_TAC THEN
563SRW_TAC [] [] THENL
564[POP_ASSUM MATCH_MP_TAC THEN REWRITE_TAC []
565,RES_TAC
566,RES_TAC
567,Q.UNDISCH_THEN `!a. (a = h) \/ MEM a l ==> (apto cmp a p = LESS)`
568 MATCH_MP_TAC THEN REWRITE_TAC []
569,MATCH_MP_TAC totoLLtrans THEN Q.EXISTS_TAC `x` THEN CONJ_TAC THENL
570 [Q.UNDISCH_THEN `!a. (a = h) \/ MEM a l ==> (apto cmp a x = LESS)`
571 MATCH_MP_TAC THEN REWRITE_TAC []
572 ,RES_TAC
573]]
574QED
575
576Theorem MEM_lb_ub_lem[local]:
577 !cmp:'a toto lb t ub a. MEM a (bt_to_ol_lb_ub cmp lb t ub) ==>
578 (apto cmp lb a = LESS) /\ (apto cmp a ub = LESS)
579Proof
580REWRITE_TAC [GSYM ol_set_lb_ub] THEN
581SRW_TAC [] [bt_to_set_lb_ub]
582QED
583
584Theorem OL_bt_to_ol_lb_ub:
585 !cmp:'a toto t lb ub. OL cmp (bt_to_ol_lb_ub cmp lb t ub)
586Proof
587GEN_TAC THEN Induct THEN
588SRW_TAC [] [bt_to_ol_lb_ub, ol_set_lb_ub, list_split_lem] THEN
589IMP_RES_TAC MEM_lb_ub_lem THEN REWRITE_TAC [OL]
590QED
591
592Theorem MEM_lb_lem[local]:
593 !cmp:'a toto lb t a. MEM a (bt_to_ol_lb cmp lb t) ==>(apto cmp lb a = LESS)
594Proof
595REWRITE_TAC [GSYM ol_set_lb] THEN
596SRW_TAC [] [bt_to_set_lb]
597QED
598
599Theorem OL_bt_to_ol_lb:
600 !cmp:'a toto t lb. OL cmp (bt_to_ol_lb cmp lb t)
601Proof
602GEN_TAC THEN Induct THEN
603SRW_TAC []
604 [bt_to_ol_lb, ol_set_lb, list_split_lem, OL_bt_to_ol_lb_ub] THENL
605[REWRITE_TAC [OL]
606,IMP_RES_TAC MEM_lb_ub_lem
607,IMP_RES_TAC MEM_lb_lem
608]
609QED
610
611Theorem MEM_ub_lem[local]:
612 !cmp:'a toto t ub a. MEM a (bt_to_ol_ub cmp t ub) ==>(apto cmp a ub = LESS)
613Proof
614REWRITE_TAC [GSYM ol_set_ub] THEN
615SRW_TAC [] [bt_to_set_ub]
616QED
617
618Theorem OL_bt_to_ol_ub:
619 !cmp:'a toto t ub. OL cmp (bt_to_ol_ub cmp t ub)
620Proof
621GEN_TAC THEN Induct THEN
622SRW_TAC []
623 [bt_to_ol_ub, ol_set_ub, list_split_lem, OL_bt_to_ol_lb_ub] THENL
624[REWRITE_TAC [OL]
625,IMP_RES_TAC MEM_ub_lem
626,IMP_RES_TAC MEM_lb_ub_lem
627]
628QED
629
630Theorem OL_bt_to_ol:
631 !cmp:'a toto t. OL cmp (bt_to_ol cmp t)
632Proof
633GEN_TAC THEN Induct THEN
634SRW_TAC []
635 [bt_to_ol, ol_set, list_split_lem, OL_bt_to_ol_lb, OL_bt_to_ol_ub] THENL
636[REWRITE_TAC [OL]
637,IMP_RES_TAC MEM_ub_lem
638,IMP_RES_TAC MEM_lb_lem
639]
640QED
641
642(* ******* Now to suppress the APPENDing ******** *)
643
644Definition bt_to_ol_lb_ub_ac:
645 (bt_to_ol_lb_ub_ac (cmp:'a toto) lb nt ub m = m) /\
646 (bt_to_ol_lb_ub_ac cmp lb (node l x r) ub m =
647 if apto cmp lb x = LESS then
648 if apto cmp x ub = LESS then
649 bt_to_ol_lb_ub_ac cmp lb l x (x :: bt_to_ol_lb_ub_ac cmp x r ub m)
650 else bt_to_ol_lb_ub_ac cmp lb l ub m
651 else bt_to_ol_lb_ub_ac cmp lb r ub m)
652End
653
654Theorem ol_lb_ub_ac_thm[local]:
655 !cmp:'a toto t lb ub m. bt_to_ol_lb_ub_ac cmp lb t ub m =
656 bt_to_ol_lb_ub cmp lb t ub ++ m
657Proof
658GEN_TAC THEN Induct THEN SRW_TAC [][bt_to_ol_lb_ub, bt_to_ol_lb_ub_ac]
659QED
660
661Definition bt_to_ol_lb_ac:
662 (bt_to_ol_lb_ac (cmp:'a toto) lb nt m = m) /\
663 (bt_to_ol_lb_ac cmp lb (node l x r) m =
664 if apto cmp lb x = LESS then
665 bt_to_ol_lb_ub_ac cmp lb l x (x :: bt_to_ol_lb_ac cmp x r m)
666 else bt_to_ol_lb_ac cmp lb r m)
667End
668
669Theorem ol_lb_ac_thm[local]:
670 !cmp:'a toto t lb m. bt_to_ol_lb_ac cmp lb t m = bt_to_ol_lb cmp lb t ++ m
671Proof
672GEN_TAC THEN Induct THEN
673SRW_TAC [][bt_to_ol_lb, bt_to_ol_lb_ac, ol_lb_ub_ac_thm]
674QED
675
676Definition bt_to_ol_ub_ac:
677 (bt_to_ol_ub_ac (cmp:'a toto) nt ub m = m) /\
678 (bt_to_ol_ub_ac cmp (node l x r) ub m =
679 if apto cmp x ub = LESS then
680 bt_to_ol_ub_ac cmp l x (x :: bt_to_ol_lb_ub_ac cmp x r ub m)
681 else bt_to_ol_ub_ac cmp l ub m)
682End
683
684Theorem ol_ub_ac_thm[local]:
685 !cmp:'a toto t ub m. bt_to_ol_ub_ac cmp t ub m = bt_to_ol_ub cmp t ub ++ m
686Proof
687GEN_TAC THEN Induct THEN
688SRW_TAC [][bt_to_ol_ub, bt_to_ol_ub_ac, ol_lb_ub_ac_thm]
689QED
690
691Definition bt_to_ol_ac:
692 (bt_to_ol_ac (cmp:'a toto) nt m = m) /\
693 (bt_to_ol_ac cmp (node l x r) m =
694 bt_to_ol_ub_ac cmp l x (x :: bt_to_ol_lb_ac cmp x r m))
695End
696
697Theorem ol_ac_thm[local]:
698 !cmp:'a toto t m. bt_to_ol_ac cmp t m = bt_to_ol cmp t ++ m
699Proof
700GEN_TAC THEN Induct THEN
701SRW_TAC [][bt_to_ol, bt_to_ol_ac, ol_lb_ac_thm, ol_ub_ac_thm]
702QED
703
704(* ********* "OWL" for [set] Ordered With List *********** *)
705
706Definition OWL: OWL (cmp:'a toto) (s:'a set) (l:'a list) =
707(s = set l) /\ OL cmp l
708End
709
710Theorem OWL_unique[local]:
711 !cmp:'a toto s l m. OWL cmp s l /\ OWL cmp s m ==> (l = m)
712Proof
713RW_TAC bool_ss [OWL] THEN
714METIS_TAC [OL_MEM_EQ]
715QED
716
717(* We want to compute bt_to_ol with as few comparisons as may be. The
718 definitions have used APPEND. *)
719
720Theorem bt_FINITE[local]:
721 !cmp:'a toto t:'a bt. FINITE (ENUMERAL cmp t)
722Proof
723REWRITE_TAC [ol_set, FINITE_LIST_TO_SET]
724QED
725
726Theorem OWL_bt_to_ol:
727 !cmp:'a toto t. OWL cmp (ENUMERAL cmp t) (bt_to_ol cmp t)
728Proof
729RW_TAC bool_ss [OWL, ol_set, OL_bt_to_ol]
730QED
731
732(* We already have the two pieces of OWL:
733
734 OL_bt_to_ol = |- !t cmp. OL cmp (bt_to_ol cmp t)
735 ol_set = |- !cmp t. ENUMERAL cmp t = set (bt_to_ol cmp t) *)
736
737(* ************* Stuff about ZSL, OSL, and OU (some interesting proofs)
738 appeared not of any use, exiled to OU.stuff ********************* *)
739
740(* Prove that bt_to_ol inverts list_to_bt for ordered lists, using OL_MEM_EQ *)
741
742Theorem OL_set_EQ[local]:
743 !cmp:'a toto l m. OL cmp l /\ OL cmp m ==> ((set l = set m) <=> (l = m))
744Proof
745REPEAT GEN_TAC THEN DISCH_THEN (MP_TAC o MATCH_MP OL_MEM_EQ) THEN
746REWRITE_TAC [EXTENSION]
747QED
748
749(* "OU" for "Ordered Union" - used for intermediate (tree, binary list) pair
750 in converting betw. binary lists and rightist trees. *)
751
752Definition OU: OU (cmp:'a toto) (t:'a set) (u:'a set) =
753 {x | x IN t /\ (!z. z IN u ==> (apto cmp x z = LESS))} UNION u
754End
755
756Definition UO: UO (cmp:'a toto) (s:'a set) (t:'a set) =
757 s UNION {y | y IN t /\ (!z. z IN s ==> (apto cmp z y = LESS))}
758End
759
760Theorem EMPTY_OU:
761 !cmp:'a toto sl:'a set. OU cmp {} sl = sl
762Proof
763REWRITE_TAC [OU, NOT_IN_EMPTY, UNION_EMPTY, GSPEC_F]
764QED
765
766Theorem OU_EMPTY:
767 !cmp:'a toto t:'a set. OU cmp t {} = t
768Proof
769REWRITE_TAC [OU, NOT_IN_EMPTY, UNION_EMPTY, GSPEC_ID]
770QED
771
772Theorem sing_UO[local]:
773 !cmp:'a toto x:'a t:'a set.
774 {x} UNION {y | y IN t /\ (apto cmp x y = LESS)} = UO cmp {x} t
775Proof
776RW_TAC bool_ss [UO, IN_SING]
777QED
778
779Theorem LESS_UO_LEM:
780 !cmp:'a toto x:'a y:'a s:'a set.
781 (!z. z IN UO cmp {x} s ==> (apto cmp y z = LESS)) <=> (apto cmp y x = LESS)
782Proof
783RW_TAC bool_ss [GSYM sing_UO] THEN EQ_TAC THEN
784REWRITE_TAC [IN_UNION, IN_SING] THEN
785CONV_TAC (ONCE_DEPTH_CONV SET_SPEC_CONV) THENL
786[CONV_TAC LEFT_IMP_FORALL_CONV THEN
787 Q.EXISTS_TAC `x` THEN RW_TAC bool_ss []
788,REPEAT STRIP_TAC THENL [AR, IMP_RES_TAC toto_trans_less]
789]
790QED
791
792Theorem bt_to_set_OU_UO[local]:
793 !cmp:'a toto l:'a bt x:'a r:'a bt. ENUMERAL cmp (node l x r) =
794 OU cmp (ENUMERAL cmp l) (UO cmp {x} (ENUMERAL cmp r))
795Proof
796RW_TAC bool_ss [OU, bt_to_set, LESS_UO_LEM] THEN
797REWRITE_TAC [GSYM UNION_ASSOC] THEN ONCE_REWRITE_TAC [sing_UO] THEN REFL_TAC
798QED
799
800Theorem OU_UO_OU_LEM[local]:
801 !cmp:'a toto l x r. OU cmp l (UO cmp {x} r) = UO cmp (OU cmp l {x}) r
802Proof
803SRW_TAC [] [OU, UO, EXTENSION, IN_UNION] THEN
804EQ_TAC THEN REPEAT STRIP_TAC THEN AR THEN
805METIS_TAC [totoLLtrans]
806QED
807
808Definition LESS_ALL: LESS_ALL (cmp:'a toto) (x:'a) (s:'a set) =
809 !y. y IN s ==> (apto cmp x y = LESS)
810End
811
812Theorem IN_OU[local]:
813 !cmp:'a toto x:'a u:'a set v:'a set.
814 x IN OU cmp u v <=> (if LESS_ALL cmp x v then x IN u else x IN v)
815Proof
816RW_TAC bool_ss [OU, LESS_ALL, IN_UNION] THEN
817CONV_TAC (ONCE_DEPTH_CONV SET_SPEC_CONV) THEN AR THEN
818Q.SUBGOAL_THEN `x NOTIN v` (REWRITE_TAC o ulist) THEN
819DISCH_TAC THEN RES_THEN MP_TAC THEN REWRITE_TAC [toto_refl, all_cpn_distinct]
820QED
821
822Theorem OU_SUBSET_UNION[local]:
823 !cmp:'a toto u:'a set v:'a set. OU cmp u v SUBSET u UNION v
824Proof
825REPEAT GEN_TAC THEN REWRITE_TAC [SUBSET_DEF, IN_OU, IN_UNION] THEN
826METIS_TAC []
827QED
828
829Theorem LESS_ALL_UNION[local]:
830 !cmp:'a toto x:'a u:'a set v:'a set.
831 LESS_ALL cmp x (u UNION v) = LESS_ALL cmp x u /\ LESS_ALL cmp x v
832Proof
833RW_TAC bool_ss [LESS_ALL, IN_UNION] THEN METIS_TAC []
834QED
835
836Theorem NOT_IN_OU_LEM[local]:
837 !cmp:'a toto x:'a u:'a set v:'a set.
838 x IN u UNION v ==> x NOTIN OU cmp u v ==> ?y. y IN v /\ apto cmp x y <> LESS
839Proof
840RW_TAC bool_ss [IN_UNION, IN_OU, LESS_ALL] THENL
841[RES_THEN MP_TAC THEN REWRITE_TAC [toto_refl, all_cpn_distinct]
842,METIS_TAC []]
843QED
844
845Theorem cpn_NOT_LESS[local]:
846 !c:cpn. c <> LESS ==> (c = GREATER) \/ (c = EQUAL)
847Proof
848METIS_TAC [cpn_nchotomy]
849QED
850
851Theorem LESS_ALL_OU:
852 !cmp:'a toto x:'a u:'a set v:'a set.
853 LESS_ALL cmp x (OU cmp u v) = LESS_ALL cmp x u /\ LESS_ALL cmp x v
854Proof
855RW_TAC bool_ss [GSYM LESS_ALL_UNION] THEN REWRITE_TAC [LESS_ALL] THEN
856EQ_TAC THENL
857[REPEAT STRIP_TAC THEN Cases_on `y IN OU cmp u v` THENL
858 [RES_TAC
859 ,IMP_RES_TAC NOT_IN_OU_LEM THEN
860 Q.SUBGOAL_THEN `y' IN OU cmp u v` ASSUME_TAC
861 THEN1 ASM_REWRITE_TAC [OU, IN_UNION] THEN
862 RES_TAC THEN IMP_RES_TAC cpn_NOT_LESS THENL
863 [IMP_RES_TAC toto_trans_less
864 ,IMP_RES_TAC toto_equal_sym THEN IMP_RES_TAC toto_trans_less
865 ]
866 ]
867,METIS_TAC [OU_SUBSET_UNION, SUBSET_DEF]
868]
869QED
870
871Theorem OU_ASSOC:
872 !cmp a b c:'a set. OU cmp a (OU cmp b c) = OU cmp (OU cmp a b) c
873Proof
874RW_TAC bool_ss [IN_OU, EXTENSION, IN_UNION] THEN
875REWRITE_TAC [LESS_ALL_OU] THEN METIS_TAC []
876QED
877
878Definition bl_to_set:
879 (bl_to_set (cmp:'a toto) (nbl:'a bl) = {}) /\
880 (bl_to_set cmp (zerbl b) = bl_to_set cmp b) /\
881 (bl_to_set cmp (onebl x t b) =
882 OU cmp ({x} UNION {y | y IN ENUMERAL cmp t /\ (apto cmp x y = LESS)})
883 (bl_to_set cmp b))
884End
885
886Theorem bl_to_set_OU_UO[local]:
887 !cmp:'a toto x t b. bl_to_set cmp (onebl x t b) =
888 OU cmp (UO cmp {x} (ENUMERAL cmp t)) (bl_to_set cmp b)
889Proof
890REWRITE_TAC [bl_to_set, sing_UO]
891QED
892
893Theorem bl_rev_set_lem[local]:
894 !cmp:'a toto b t.
895 ENUMERAL cmp (bl_rev t b) = OU cmp (ENUMERAL cmp t) (bl_to_set cmp b)
896Proof
897GEN_TAC THEN Induct THEN
898SRW_TAC [] [bl_rev, bl_to_set_OU_UO] THEN
899REWRITE_TAC [bl_to_set, OU_EMPTY] THEN
900REWRITE_TAC [bt_to_set_OU_UO, OU_ASSOC]
901QED
902
903(* Converting a bl to a bt preserves the represented set: *)
904
905Theorem bl_to_bt_set[local]:
906 !cmp:'a toto b. ENUMERAL cmp (bl_to_bt b) = bl_to_set cmp b
907Proof
908REWRITE_TAC [bl_to_bt, bl_rev_set_lem, bt_to_set, EMPTY_OU]
909QED
910
911(* Now to show that building a bl from a list does the same. *)
912
913(* We aim to show that LESS_ALL cmp a (bl_to_set cmp b) ==>
914 (bl_to_set cmp (BL_CONS a bl) = a INSERT bl_to_set cmp b). *)
915
916(* Generalizing for the recursion in BL_ACCUM, we hope to show that
917 LESS_ALL cmp a (ENUMERAL cmp t) /\ LESS_ALL cmp a (bl_to_set b) ==>
918 (bl_to_set cmp (BL_ACCUM a t b) =
919 a INSERT (OU cmp (ENUMERAL cmp t) (bl_to_set cmp b))) . *)
920
921Theorem LESS_ALL_UO_LEM:
922 !cmp:'a toto a s. LESS_ALL cmp a s ==> (UO cmp {a} s = a INSERT s)
923Proof
924SRW_TAC [] [LESS_ALL, UO, EXTENSION, IN_UNION] THEN METIS_TAC []
925QED
926
927Theorem LESS_ALL_OU_UO_LEM:
928 !cmp:'a toto a s t. LESS_ALL cmp a s /\ LESS_ALL cmp a t ==>
929 (OU cmp (UO cmp {a} s) t = a INSERT (OU cmp s t))
930Proof
931REPEAT STRIP_TAC THEN IMP_RES_THEN SUBST1_TAC LESS_ALL_UO_LEM THEN
932SRW_TAC [] [UO, OU, EXTENSION, IN_UNION] THEN
933METIS_TAC [LESS_ALL]
934QED
935
936Theorem BL_ACCUM_set[local]:
937 !cmp:'a toto a b t.
938 LESS_ALL cmp a (ENUMERAL cmp t) /\ LESS_ALL cmp a (bl_to_set cmp b) ==>
939 (bl_to_set cmp (BL_ACCUM a t b) =
940 a INSERT (OU cmp (ENUMERAL cmp t) (bl_to_set cmp b)))
941Proof
942GEN_TAC THEN GEN_TAC THEN Induct THEN
943SRW_TAC [] [BL_ACCUM, bl_to_set_OU_UO, bt_to_set_OU_UO] THENL
944[METIS_TAC [LESS_ALL_UO_LEM, LESS_ALL_OU_UO_LEM, bl_to_set]
945,METIS_TAC [LESS_ALL_UO_LEM, LESS_ALL_OU_UO_LEM, bl_to_set]
946,REWRITE_TAC [bl_to_set] THEN
947`LESS_ALL cmp a (UO cmp {a'} (ENUMERAL cmp b0)) /\
948 LESS_ALL cmp a (bl_to_set cmp b)` by ASM_REWRITE_TAC [GSYM LESS_ALL_OU] THEN
949`LESS_ALL cmp a (ENUMERAL cmp (node t a' b0))`
950 by ASM_REWRITE_TAC [bt_to_set_OU_UO, LESS_ALL_OU] THEN
951 RES_TAC THEN ASM_REWRITE_TAC [bt_to_set_OU_UO, OU_ASSOC]
952]
953QED
954
955Theorem BL_CONS_set[local]:
956 !cmp:'a toto a b. LESS_ALL cmp a (bl_to_set cmp b) ==>
957 (bl_to_set cmp (BL_CONS a b) = a INSERT bl_to_set cmp b)
958Proof
959REPEAT STRIP_TAC THEN REWRITE_TAC [BL_CONS] THEN
960Q.SUBGOAL_THEN `OU cmp (ENUMERAL cmp nt) (bl_to_set cmp b) = bl_to_set cmp b`
961(SUBST1_TAC o SYM)
962THEN1 REWRITE_TAC [bt_to_set, EMPTY_OU] THEN
963`LESS_ALL cmp a (ENUMERAL cmp nt)`
964 by REWRITE_TAC [LESS_ALL, NOT_IN_EMPTY, bt_to_set] THEN
965IMP_RES_TAC BL_ACCUM_set
966QED
967
968Theorem list_to_bl_set[local]:
969 !cmp:'a toto l. OL cmp l ==> (bl_to_set cmp (list_to_bl l) = set l)
970Proof
971GEN_TAC THEN Induct THEN
972SRW_TAC [] [bl_to_set, list_to_bl, LIST_TO_SET_THM, OL] THEN
973RES_THEN (SUBST1_TAC o SYM) THEN MATCH_MP_TAC BL_CONS_set THEN
974RES_THEN SUBST1_TAC THEN RW_TAC bool_ss [LESS_ALL]
975QED
976
977Theorem bt_to_ol_ID[local]:
978 !cmp:'a toto. !l::OL cmp. bt_to_ol cmp (list_to_bt l) = l
979Proof
980GEN_TAC THEN CONV_TAC RES_FORALL_CONV THEN
981REWRITE_TAC [SPECIFICATION] THEN GEN_TAC THEN DISCH_TAC THEN
982Q.SUBGOAL_THEN `OL cmp (bt_to_ol cmp (list_to_bt l)) /\ OL cmp l`
983(REWRITE_TAC o ulist o GSYM o MATCH_MP OL_set_EQ)
984THEN1 ASM_REWRITE_TAC [OL_bt_to_ol] THEN
985IMP_RES_THEN (SUBST1_TAC o SYM) list_to_bl_set THEN
986REWRITE_TAC [GSYM bl_to_bt_set, list_to_bt, ol_set]
987QED
988
989Theorem bt_to_ol_ID_IMP = REWRITE_RULE [SPECIFICATION]
990 (CONV_RULE (ONCE_DEPTH_CONV RES_FORALL_CONV) bt_to_ol_ID);
991
992(* bt_to_ol_ID_IMP: |- !cmp l. OL cmp l ==> (bt_to_ol cmp (list_to_bt l) = l) *)
993
994Theorem list_to_bt_ID[local]:
995 !cmp:'a toto t:'a bt.
996 ENUMERAL cmp (list_to_bt (bt_to_ol cmp t)) = ENUMERAL cmp t
997Proof
998METIS_TAC [bt_to_ol_ID_IMP, ol_set, OL_bt_to_ol]
999QED
1000
1001(* Set operations. We already have smerge_set and smerge_OL. *)
1002(* "OL_UNION" possibly not the best name. *)
1003
1004Theorem OL_UNION[local]:
1005 !cmp:'a toto. !l m::OL cmp. OL cmp (smerge cmp l m) /\
1006 (set (smerge cmp l m) = set l UNION set m)
1007Proof
1008CONV_TAC (DEPTH_CONV RES_FORALL_CONV) THEN
1009SRW_TAC [] [SPECIFICATION, smerge_set, smerge_OL]
1010QED
1011
1012Theorem OL_UNION_IMP = REWRITE_RULE [SPECIFICATION]
1013 (CONV_RULE (DEPTH_CONV RES_FORALL_CONV) OL_UNION);
1014
1015(* OL_UNION_IMP = |- !cmp l. OL cmp l ==> !m. OL cmp m ==>
1016 OL cmp (smerge cmp l m) /\ (set (smerge cmp l m) = set l UNION set m) *)
1017
1018Theorem ENUMERAL_UNION[local]:
1019 !cmp:'a toto s t:'a bt.
1020 ENUMERAL cmp (list_to_bt (smerge cmp (bt_to_ol cmp s) (bt_to_ol cmp t))) =
1021 ENUMERAL cmp s UNION ENUMERAL cmp t
1022Proof
1023RW_TAC bool_ss [ol_set] THEN
1024`OL cmp (bt_to_ol cmp s) /\ OL cmp (bt_to_ol cmp t)`
1025 by REWRITE_TAC [OL_bt_to_ol] THEN
1026`OL cmp (smerge cmp (bt_to_ol cmp s) (bt_to_ol cmp t))`
1027 by IMP_RES_TAC smerge_OL THEN
1028IMP_RES_THEN SUBST1_TAC bt_to_ol_ID_IMP THEN
1029REWRITE_TAC [smerge_set]
1030QED
1031
1032(* **************** Similar treatment of intersection: ************* *)
1033
1034Definition sinter:
1035 (sinter (cmp:'a toto) [] [] = []) /\
1036 (sinter cmp (x:'a :: l) [] = []) /\
1037 (sinter cmp [] (y:'a :: m) = []) /\
1038 (sinter cmp (x :: l) (y :: m) = case apto cmp x y of
1039 LESS => sinter cmp l (y :: m)
1040 | EQUAL => x :: (sinter cmp l m)
1041 | GREATER => sinter cmp (x :: l) m)
1042End
1043
1044val sinter_ind = theorem "sinter_ind";
1045
1046Theorem sinter_nil[local]:
1047 !cmp:'a toto l. (sinter cmp l [] = []) /\ (sinter cmp [] l = [])
1048Proof
1049REPEAT STRIP_TAC THEN Cases_on `l` THEN REWRITE_TAC [sinter]
1050QED
1051
1052Theorem sinter_subset_inter[local]:
1053 !cmp:'a toto l m x. MEM x (sinter cmp l m) ==> MEM x l /\ MEM x m
1054Proof
1055HO_MATCH_MP_TAC sinter_ind THEN
1056RW_TAC (srw_ss()) [sinter, MEM] THEN POP_ASSUM MP_TAC THEN
1057Cases_on `apto cmp x y` THEN SRW_TAC [] [] THEN RES_TAC THEN AR THEN
1058DISJ1_TAC THEN IMP_RES_TAC toto_equal_eq
1059QED
1060
1061Theorem sinter_OL[local]:
1062 !cmp:'a toto l m. OL cmp l /\ OL cmp m ==> OL cmp (sinter cmp l m)
1063Proof
1064HO_MATCH_MP_TAC sinter_ind THEN
1065RW_TAC (srw_ss()) [sinter, sinter_nil, OL] THEN
1066Cases_on `apto cmp x y` THEN SRW_TAC [] [OL] THEN
1067IMP_RES_TAC sinter_subset_inter THEN RES_TAC
1068QED
1069
1070Theorem inter_subset_sinter[local]:
1071 !cmp:'a toto x l. OL cmp l /\ MEM x l ==>
1072 !m. OL cmp m /\ MEM x m ==> MEM x (sinter cmp l m)
1073Proof
1074GEN_TAC THEN GEN_TAC THEN Induct THEN REWRITE_TAC [MEM] THEN
1075GEN_TAC THEN STRIP_TAC THEN Induct THEN REWRITE_TAC [MEM] THEN
1076RW_TAC (srw_ss()) [sinter] THENL
1077[SRW_TAC [] [toto_refl, MEM]
1078,Cases_on `apto cmp h h'` THEN RES_TAC THEN
1079 SRW_TAC [] [sinter, MEM] THENL
1080 [IMP_RES_TAC OL THEN IMP_RES_TAC totoLLtrans THEN
1081 IMP_RES_TAC toto_not_less_refl
1082 ,IMP_RES_TAC OL THEN RES_TAC
1083 ]
1084,Cases_on `apto cmp h h'` THEN RES_TAC THEN
1085 SRW_TAC [] [sinter, MEM] THENL
1086 [`OL cmp l` by IMP_RES_TAC OL THEN RES_TAC THEN
1087 `MEM h' (h' :: m)` by REWRITE_TAC [MEM] THEN RES_TAC
1088 ,IMP_RES_TAC toto_equal_eq THEN AR
1089 ,`apto cmp h h' = LESS` by IMP_RES_TAC OL THEN
1090 IMP_RES_TAC totoLGtrans THEN IMP_RES_TAC toto_not_less_refl
1091 ]
1092,Cases_on `apto cmp h h'` THEN RES_TAC THEN
1093 SRW_TAC [] [sinter, MEM] THENL
1094 [`MEM x (h' :: m)` by ASM_REWRITE_TAC [MEM] THEN IMP_RES_TAC OL THEN RES_TAC
1095 ,DISJ2_TAC THEN IMP_RES_TAC OL THEN RES_TAC
1096 ,IMP_RES_TAC OL THEN RES_TAC
1097]]
1098QED
1099
1100(* Note that sinter_set, unlike smerge_set, depends on sorted input lists. *)
1101
1102Theorem sinter_set[local]:
1103 !cmp:'a toto l m.
1104 OL cmp l /\ OL cmp m ==> (set (sinter cmp l m) = set l INTER set m)
1105Proof
1106SRW_TAC [] [IN_INTER, EXTENSION] THEN EQ_TAC THENL
1107[MATCH_ACCEPT_TAC sinter_subset_inter
1108,METIS_TAC [inter_subset_sinter]
1109]
1110QED
1111
1112Theorem OL_INTER[local]:
1113 !cmp:'a toto. !l m::OL cmp. OL cmp (sinter cmp l m) /\
1114 (set (sinter cmp l m) = set l INTER set m)
1115Proof
1116CONV_TAC (DEPTH_CONV RES_FORALL_CONV) THEN
1117SRW_TAC [] [SPECIFICATION, sinter_set, sinter_OL]
1118QED
1119
1120Theorem OL_INTER_IMP = REWRITE_RULE [SPECIFICATION]
1121 (CONV_RULE (DEPTH_CONV RES_FORALL_CONV) OL_INTER);
1122
1123(* OL_INTER_IMP = |- !cmp l. OL cmp l ==> !m. OL cmp m ==>
1124 OL cmp (sinter cmp l m) /\ (set (sinter cmp l m) = set l INTER set m) *)
1125
1126Theorem ENUMERAL_INTER[local]:
1127 !cmp:'a toto s t:'a bt.
1128 ENUMERAL cmp (list_to_bt (sinter cmp (bt_to_ol cmp s) (bt_to_ol cmp t))) =
1129 ENUMERAL cmp s INTER ENUMERAL cmp t
1130Proof
1131RW_TAC bool_ss [ol_set] THEN
1132`OL cmp (bt_to_ol cmp s) /\ OL cmp (bt_to_ol cmp t)`
1133 by REWRITE_TAC [OL_bt_to_ol] THEN
1134`OL cmp (sinter cmp (bt_to_ol cmp s) (bt_to_ol cmp t))`
1135 by IMP_RES_TAC sinter_OL THEN
1136IMP_RES_THEN SUBST1_TAC bt_to_ol_ID_IMP THEN
1137MATCH_MP_TAC sinter_set THEN AR
1138QED
1139
1140(* **************** Similar treatment of set difference: ************* *)
1141
1142Definition sdiff:
1143 (sdiff (cmp:'a toto) [] [] = []) /\
1144 (sdiff cmp (x:'a :: l) [] = (x::l)) /\
1145 (sdiff cmp [] (y:'a :: m) = []) /\
1146 (sdiff cmp (x :: l) (y :: m) = case apto cmp x y of
1147 LESS => x :: sdiff cmp l (y :: m)
1148 | EQUAL => sdiff cmp l m
1149 | GREATER => sdiff cmp (x :: l) m)
1150End
1151
1152val sdiff_ind = theorem "sdiff_ind";
1153
1154Theorem sdiff_nil[local]:
1155 !cmp:'a toto l. (sdiff cmp l [] = l) /\ (sdiff cmp [] l = [])
1156Proof
1157REPEAT STRIP_TAC THEN Cases_on `l` THEN REWRITE_TAC [sdiff]
1158QED
1159
1160Theorem diff_subset_sdiff[local]:
1161 !cmp:'a toto l m x. MEM x l /\ ~MEM x m ==> MEM x (sdiff cmp l m)
1162Proof
1163HO_MATCH_MP_TAC sdiff_ind THEN
1164RW_TAC (srw_ss()) [sdiff, MEM] THEN POP_ASSUM MP_TAC THEN
1165Cases_on `apto cmp x y` THEN SRW_TAC [] [] THEN RES_TAC THEN AR THEN
1166IMP_RES_TAC toto_equal_eq
1167QED
1168
1169Theorem OL_NOT_MEM[local]:
1170 !cmp:'a toto x l. OL cmp (x::l) ==> ~MEM x l
1171Proof
1172REPEAT GEN_TAC THEN REWRITE_TAC [OL] THEN STRIP_TAC THEN
1173DISCH_TAC THEN RES_THEN MP_TAC THEN
1174REWRITE_TAC [toto_refl, all_cpn_distinct]
1175QED
1176
1177Theorem sdiff_subset_diff[local]:
1178 !cmp:'a toto x l m. OL cmp l /\ OL cmp m ==>
1179 MEM x (sdiff cmp l m) ==> MEM x l /\ ~MEM x m
1180Proof
1181GEN_TAC THEN GEN_TAC THEN Induct THEN REWRITE_TAC [MEM, sdiff_nil] THEN
1182GEN_TAC THEN Induct THEN REWRITE_TAC [MEM] THEN
1183RW_TAC (srw_ss()) [sdiff] THEN POP_ASSUM MP_TAC THEN
1184`OL cmp m` by IMP_RES_TAC OL THEN `OL cmp l` by IMP_RES_TAC OL THENL
1185[Cases_on `apto cmp h h'` THEN
1186 SRW_TAC [] [sdiff, MEM] THEN DISJ2_TAC THEN RES_TAC
1187,Cases_on `apto cmp h h'` THEN
1188 SRW_TAC [] [sdiff, MEM] THENL
1189 [IMP_RES_TAC toto_glneq
1190 ,METIS_TAC [MEM]
1191 ,IMP_RES_TAC toto_equal_eq THEN METIS_TAC [OL_NOT_MEM]
1192 ,`(x = h) \/ MEM x l` by METIS_TAC [] THEN IMP_RES_TAC toto_antisym THENL
1193 [AR THEN IMP_RES_TAC toto_glneq
1194 ,METIS_TAC [OL, totoLLtrans, toto_glneq]
1195 ]]
1196,Cases_on `apto cmp h h'` THEN
1197 SRW_TAC [] [sdiff, MEM] THENL
1198 [METIS_TAC [OL, totoLLtrans, toto_glneq]
1199 ,METIS_TAC [MEM]
1200]]
1201QED
1202
1203Theorem sdiff_OL[local]:
1204 !cmp:'a toto l m. OL cmp l /\ OL cmp m ==> OL cmp (sdiff cmp l m)
1205Proof
1206GEN_TAC THEN Induct THEN1 REWRITE_TAC [sdiff_nil, OL] THEN GEN_TAC THEN
1207Induct THEN1 (REWRITE_TAC [sdiff_nil] THEN tautLib.TAUT_TAC) THEN
1208SRW_TAC [] [sdiff] THEN REWRITE_TAC [OL] THEN
1209IMP_RES_TAC OL THEN
1210Cases_on `apto cmp h h'` THEN SRW_TAC [] [OL] THEN
1211IMP_RES_TAC sdiff_subset_diff THEN RES_TAC
1212QED
1213
1214(* Note that sdiff_set, like sinter_set, depends on sorted input lists. *)
1215
1216Theorem sdiff_set[local]:
1217 !cmp:'a toto l m.
1218 OL cmp l /\ OL cmp m ==> (set (sdiff cmp l m) = set l DIFF set m)
1219Proof
1220SRW_TAC [] [IN_DIFF, EXTENSION] THEN EQ_TAC THENL
1221[METIS_TAC [sdiff_subset_diff]
1222,MATCH_ACCEPT_TAC diff_subset_sdiff
1223]
1224QED
1225
1226Theorem OL_DIFF[local]:
1227 !cmp:'a toto. !l m::OL cmp. OL cmp (sdiff cmp l m) /\
1228 (set (sdiff cmp l m) = set l DIFF set m)
1229Proof
1230CONV_TAC (DEPTH_CONV RES_FORALL_CONV) THEN
1231SRW_TAC [] [SPECIFICATION, sdiff_set, sdiff_OL]
1232QED
1233
1234Theorem OL_DIFF_IMP = REWRITE_RULE [SPECIFICATION]
1235 (CONV_RULE (DEPTH_CONV RES_FORALL_CONV) OL_DIFF);
1236
1237(* OL_DIFF_IMP = |- !cmp l. OL cmp l ==> !m. OL cmp m ==>
1238 OL cmp (sdiff cmp l m) /\ (set (sdiff cmp l m) = set l DIFF set m) *)
1239
1240Theorem ENUMERAL_DIFF[local]:
1241 !cmp:'a toto s t:'a bt.
1242 ENUMERAL cmp (list_to_bt (sdiff cmp (bt_to_ol cmp s) (bt_to_ol cmp t))) =
1243 ENUMERAL cmp s DIFF ENUMERAL cmp t
1244Proof
1245RW_TAC bool_ss [ol_set] THEN
1246`OL cmp (bt_to_ol cmp s) /\ OL cmp (bt_to_ol cmp t)`
1247 by REWRITE_TAC [OL_bt_to_ol] THEN
1248`OL cmp (sdiff cmp (bt_to_ol cmp s) (bt_to_ol cmp t))`
1249 by IMP_RES_TAC sdiff_OL THEN
1250IMP_RES_THEN SUBST1_TAC bt_to_ol_ID_IMP THEN
1251MATCH_MP_TAC sdiff_set THEN AR
1252QED
1253
1254(* ********************************************************************* *)
1255(* Theorems to assist conversions *)
1256(* ********************************************************************* *)
1257
1258Theorem ENUMERAL_set:
1259 !cmp l:'a list. set l = ENUMERAL cmp (list_to_bt (incr_ssort cmp l))
1260Proof
1261REPEAT GEN_TAC THEN CONV_TAC (LAND_CONV (REWR_CONV (GSYM incr_ssort_set))) THEN
1262Q.SUBGOAL_THEN
1263`incr_ssort cmp l = bt_to_ol cmp (list_to_bt (incr_ssort cmp l))`
1264SUBST1_TAC THENL
1265[MATCH_MP_TAC (GSYM bt_to_ol_ID_IMP) THEN MATCH_ACCEPT_TAC incr_ssort_OL
1266,REWRITE_TAC [list_to_bt_ID, ol_set]
1267]
1268QED
1269
1270Theorem OL_ENUMERAL:
1271 !cmp l:'a list. OL cmp l ==> (set l = ENUMERAL cmp (list_to_bt l))
1272Proof
1273REPEAT STRIP_TAC THEN
1274Q.SUBGOAL_THEN
1275`l = bt_to_ol cmp (list_to_bt l)` SUBST1_TAC THENL
1276[MATCH_MP_TAC (GSYM bt_to_ol_ID_IMP) THEN AR
1277,REWRITE_TAC [list_to_bt_ID, ol_set]
1278]
1279QED
1280
1281Theorem bt_to_ol_thm[local]:
1282 !cmp:'a toto t. bt_to_ol cmp t = bt_to_ol_ac cmp t []
1283Proof
1284SRW_TAC [] [ol_ac_thm]
1285QED
1286
1287Theorem OWL_UNION_THM: !cmp:'a toto s l t m.
1288 OWL cmp s l /\ OWL cmp t m ==> OWL cmp (s UNION t) (smerge cmp l m)
1289Proof
1290METIS_TAC [OWL, OL_UNION_IMP]
1291QED
1292
1293Theorem OWL_INTER_THM: !cmp:'a toto s l t m.
1294 OWL cmp s l /\ OWL cmp t m ==> OWL cmp (s INTER t) (sinter cmp l m)
1295Proof
1296METIS_TAC [OWL, OL_INTER_IMP]
1297QED
1298
1299Theorem OWL_DIFF_THM: !cmp:'a toto s l t m.
1300 OWL cmp s l /\ OWL cmp t m ==> OWL cmp (s DIFF t) (sdiff cmp l m)
1301Proof
1302METIS_TAC [OWL, OL_DIFF_IMP]
1303QED
1304
1305(* ******************************************************************* *)
1306(* Test for a bt with no spurious nodes, as should be invariably the *)
1307(* case, and justify quicker bt_to_ol for bt's passing the test, *)
1308(* makes exactly n - 1 comparisons in passing a tree with n nodes. *)
1309(* ******************************************************************* *)
1310
1311Definition OL_bt_lb_ub:
1312 (OL_bt_lb_ub cmp lb (nt:'a bt) ub = (apto cmp lb ub = LESS)) /\
1313 (OL_bt_lb_ub cmp lb (node l x r) ub = OL_bt_lb_ub cmp lb l x /\
1314 OL_bt_lb_ub cmp x r ub)
1315End
1316
1317Definition OL_bt_lb:
1318 (OL_bt_lb cmp lb (nt:'a bt) = T) /\
1319 (OL_bt_lb cmp lb (node l x r) = OL_bt_lb_ub cmp lb l x /\
1320 OL_bt_lb cmp x r)
1321End
1322
1323Definition OL_bt_ub:
1324 (OL_bt_ub cmp (nt:'a bt) ub = T) /\
1325 (OL_bt_ub cmp (node l x r) ub = OL_bt_ub cmp l x /\
1326 OL_bt_lb_ub cmp x r ub)
1327End
1328
1329Definition OL_bt:
1330 (OL_bt cmp (nt:'a bt) = T) /\
1331 (OL_bt cmp (node l x r) = OL_bt_ub cmp l x /\ OL_bt_lb cmp x r)
1332End
1333
1334Theorem OL_bt_lb_ub_lem[local]:
1335 !cmp t lb ub. OL_bt_lb_ub cmp lb t ub ==> (apto cmp lb ub = LESS)
1336Proof
1337GEN_TAC THEN Induct THEN
1338SRW_TAC [] [OL_bt_lb_ub] THEN METIS_TAC [ totoLLtrans]
1339QED
1340
1341Theorem OL_bt_lb_ub_thm[local]:
1342 !cmp t:'a bt lb ub. OL_bt_lb_ub cmp lb t ub ==>
1343 (bt_to_ol_lb_ub cmp lb t ub = bt_to_list t)
1344Proof
1345GEN_TAC THEN Induct THEN
1346SRW_TAC [] [OL_bt_lb_ub, bt_to_ol_lb_ub, bt_to_list] THEN
1347METIS_TAC [OL_bt_lb_ub_lem]
1348QED
1349
1350Theorem OL_bt_lb_thm[local]:
1351 !cmp t:'a bt lb. OL_bt_lb cmp lb t ==>
1352 (bt_to_ol_lb cmp lb t = bt_to_list t)
1353Proof
1354GEN_TAC THEN Induct THEN
1355SRW_TAC [] [OL_bt_lb, bt_to_ol_lb, OL_bt_lb_ub_thm, bt_to_list] THEN
1356METIS_TAC [OL_bt_lb_ub_lem]
1357QED
1358
1359Theorem OL_bt_ub_thm[local]:
1360 !cmp t:'a bt ub. OL_bt_ub cmp t ub ==>
1361 (bt_to_ol_ub cmp t ub = bt_to_list t)
1362Proof
1363GEN_TAC THEN Induct THEN
1364SRW_TAC [] [OL_bt_ub, bt_to_ol_ub, OL_bt_lb_ub_thm, bt_to_list] THEN
1365METIS_TAC [OL_bt_lb_ub_lem]
1366QED
1367
1368Theorem OL_bt_thm[local]:
1369 !cmp t:'a bt. OL_bt cmp t ==> (bt_to_ol cmp t = bt_to_list t)
1370Proof
1371GEN_TAC THEN Cases THEN
1372SRW_TAC [] [OL_bt, bt_to_ol, OL_bt_lb_thm, OL_bt_ub_thm, bt_to_list]
1373QED
1374
1375Theorem better_bt_to_ol:
1376 !cmp t:'a bt. bt_to_ol cmp t = if OL_bt cmp t then bt_to_list_ac t []
1377 else bt_to_ol_ac cmp t []
1378Proof
1379METIS_TAC [OL_bt_thm, bt_to_list_thm, bt_to_ol_thm]
1380QED
1381
1382(* ******************* Theorem to support set_TO_OWL ********************* *)
1383
1384Theorem set_OWL_thm:
1385 !cmp l:'a list. OWL cmp (set l) (incr_ssort cmp l)
1386Proof
1387REWRITE_TAC [OWL, incr_ssort_set, incr_ssort_OL]
1388QED