fmapalScript.sml
1(* file HS/PIN/fmapalScript.sml, created 6/2/13 F.L. Morris *)
2(* tree-based finite function representation; name a homage to numeralTheory *)
3(* Uses bt, bl basics from enumeralScript, puts 'a#'b in place of 'a. *)
4(* Revised 13 Dec. 2013 for HOL_Kananaskis 9. *)
5Theory fmapal
6Ancestors
7 pred_set relation res_quan pair option finite_map toto list
8 enumeral
9Libs
10 pred_setLib res_quanLib PairRules
11
12
13val _ = set_trace "Unicode" 0;
14val _ = ParseExtras.temp_loose_equality()
15val cpn_case_def = TypeBase.case_def_of ``:ordering``
16val cpn_distinct = TypeBase.distinct_of ``:ordering``
17val cpn_nchotomy = TypeBase.nchotomy_of ``:ordering``
18
19(* "fmapal" for "numeral-ish finite map", wordplay on "NUMERAL", "enumeral". *)
20(* Temptation to call it "funeralTheory" reluctantly resisted. *)
21
22(* My habitual abbreviations: *)
23
24val AR = ASM_REWRITE_TAC [];
25fun ulist x = [x];
26fun rrs th = REWRITE_RULE [SPECIFICATION] th;
27
28(* ****** Make FUNION infix. ********* *)
29
30val _ = set_fixity "FUNION" (Infixl 500);
31
32Definition ORL: (ORL (cmp:'a toto) ([]:('a#'b)list) = T) /\
33 (ORL cmp ((a,b) :: l) = ORL cmp l /\
34 (!p q. MEM (p,q) l ==> (apto cmp a p = LESS)))
35End
36
37Theorem ORL_LEM[local]:
38 !cmp l:('a#'b)list m. ORL cmp (l ++ m) ==> ORL cmp l /\ ORL cmp m
39Proof
40GEN_TAC THEN Induct THEN REWRITE_TAC [APPEND, ORL] THEN
41P_PGEN_TAC (Term`x:'a,y:'b`) THEN ASM_REWRITE_TAC [ORL] THEN
42REWRITE_TAC [MEM_APPEND] THEN REPEAT STRIP_TAC THEN RES_TAC THEN AR
43QED
44
45Theorem MEM_FST[local]:
46 !x l:('a#'b)list. (?y. MEM (x,y) l) <=> MEM x (MAP FST l)
47Proof
48GEN_TAC THEN Induct THENL
49[REWRITE_TAC [MEM, MAP]
50,P_PGEN_TAC ``a:'a, b:'b`` THEN SRW_TAC [] [MAP,MEM] THEN
51 METIS_TAC [MEM]
52]
53QED
54
55Theorem ORL_OL_FST[local]:
56 !cmp:'a toto l:('a#'b) list. ORL cmp l <=> OL cmp (MAP FST l)
57Proof
58GEN_TAC THEN Induct THENL
59[REWRITE_TAC [ORL, OL, MAP]
60,P_PGEN_TAC ``a:'a, b:'b`` THEN SRW_TAC [] [MAP, ORL, OL] THEN
61 CONV_TAC (LAND_CONV (ONCE_DEPTH_CONV FORALL_IMP_CONV)) THEN
62 REWRITE_TAC [MEM_FST]
63]
64QED
65
66(* A useful way of combining option values, that I don't find premade: *)
67
68Definition optry: (optry (SOME p) (q:'z option) = SOME p)
69 /\ (optry NONE q = q)
70End
71
72Theorem optry_case[local]:
73 !p q:'z option. optry p q = case p of SOME x => SOME x | NONE => q
74Proof
75REPEAT GEN_TAC THEN Cases_on `p` THEN REWRITE_TAC [optry, option_CLAUSES] THEN
76BETA_TAC THEN REFL_TAC
77QED
78
79Theorem optry_ASSOC[local]:
80 !p q r:'z option. optry p (optry q r) = optry (optry p q) r
81Proof
82REPEAT GEN_TAC THEN
83Cases_on `p` THEN REWRITE_TAC [option_case_def, optry]
84QED
85
86Theorem optry_ID[local]:
87 (!p:'z option. optry p NONE = p) /\ (!p:'z option. optry NONE p = p)
88Proof
89REWRITE_TAC [optry] THEN Cases THEN REWRITE_TAC [optry]
90QED
91
92Theorem IS_SOME_optry[local]:
93 !a b:'a option. IS_SOME a ==> (optry a b = a)
94Proof
95REPEAT GEN_TAC THEN Cases_on `a` THEN
96ASM_REWRITE_TAC [optry, option_CLAUSES]
97QED
98
99Definition optry_list:
100 (optry_list (f:'z->'g option) ([]:'z option list) = NONE)
101/\ (optry_list f ((NONE:'z option) :: l) = optry_list f l)
102/\ (optry_list f (SOME (z:'z) :: l) = optry (f z) (optry_list f l))
103End
104
105(* We define the following function, assocv, to give the option-valued
106function embodied by an association list. The name is chosen both to
107avoid confusion with the usual contraction for "associative" and to
108indicate departure from the Lisp-ML tradition of assoc's that return
109the argument-value pair; "v" is for "value [only]". *)
110
111Definition assocv: (assocv ([]:('a#'b)list) (a:'a) = NONE)
112 /\ (assocv ((x:'a, y:'b) :: l) a =
113 if a = x then SOME y else assocv l a)
114End
115
116(* But for more convenient partial application below at incr_merge_lem: *)
117
118Definition vcossa: vcossa a (l:('a#'b)list) = assocv l a
119End
120
121(* Define an update-like binary operation on option valued functions: *)
122
123Definition OPTION_UPDATE:
124 OPTION_UPDATE (f:'a->'b option) g x = optry (f x) (g x)
125End
126
127Theorem IS_SOME_OPTION_UPDATE[local]:
128 !u (v:'a -> 'b option). IS_SOME o OPTION_UPDATE u v =
129 IS_SOME o u UNION IS_SOME o v
130Proof
131REPEAT GEN_TAC THEN CONV_TAC FUN_EQ_CONV THEN GEN_TAC THEN
132REWRITE_TAC [rrs IN_UNION, combinTheory.o_THM, OPTION_UPDATE, optry_case] THEN
133Cases_on `u x` THEN REWRITE_TAC [option_CLAUSES] THEN
134BETA_TAC THEN REWRITE_TAC [option_CLAUSES]
135QED
136
137(* ***************************************************************** *)
138(* merge sorting for functions (as association lists here. We call *)
139(* the basic list-combining function, which gives priority to the *)
140(* first argument, just "merge". This corresponds to FUNION in fmap,*)
141(* not to FMERGE. Corresponding set functions use "smerge", etc. *)
142(* ***************************************************************** *)
143
144Definition merge: (merge (cmp:'a toto) [] (l:('a#'b)list) = l)
145 /\ (merge (cmp:'a toto) l [] = l)
146 /\ (merge (cmp:'a toto) ((a1, b1) :: l1) ((a2, b2) :: l2) =
147 case apto cmp a1 a2 of
148 LESS => (a1, b1) :: merge cmp l1 ((a2, b2) :: l2)
149 | EQUAL => (a1, b1:'b) :: merge cmp l1 l2
150 | GREATER => (a2, b2) :: merge cmp ((a1, b1) :: l1) l2)
151End
152
153val merge_ind = theorem "merge_ind";
154
155(* merge_ind = |- !P.
156 (!cmp l. P cmp [] l) /\ (!cmp v4 v5. P cmp (v4::v5) []) /\
157 (!cmp a1 b1 l1 a2 b2 l2.
158 ((apto cmp a1 a2 = EQUAL) ==> P cmp l1 l2) /\
159 ((apto cmp a1 a2 = GREATER) ==> P cmp ((a1,b1)::l1) l2) /\
160 ((apto cmp a1 a2 = LESS) ==> P cmp l1 ((a2,b2)::l2)) ==>
161 P cmp ((a1,b1)::l1) ((a2,b2)::l2)) ==>
162 !v v1 v2. P v v1 v2 *)
163
164Theorem merge_thm[local]:
165 !cmp:'a toto. (!m:('a#'b)list. merge cmp [] m = m)
166 /\ (!l:('a#'b)list. merge cmp l [] = l)
167 /\ (!a1:'a b1:'b a2:'a b2:'b l1 l2.
168 merge cmp ((a1, b1) :: l1) ((a2, b2) :: l2) =
169 case apto cmp a1 a2 of
170 LESS => (a1, b1) :: merge cmp l1 ((a2, b2) :: l2)
171 | EQUAL => (a1, b1:'b) :: merge cmp l1 l2
172 | GREATER => (a2, b2) :: merge cmp ((a1, b1) :: l1) l2)
173Proof
174GEN_TAC THEN REWRITE_TAC [merge] THEN
175Cases_on `l:('a#'b)list` THENL
176[REWRITE_TAC [merge]
177,PURE_ONCE_REWRITE_TAC [GSYM PAIR] THEN REWRITE_TAC [merge]]
178QED
179
180(* If we are to use incr_sort, we doubtless will need to prove that its
181ouput is sorted and contains the pairs that assocv would find from its
182argument. *)
183
184(* Possibly better imitate enumeral more: _ORL thms might come from
185 lemmas like MAP FST (merge cmp l m) = smerge cmp (MAP FST l) (MAP FST m),
186 and corresponding to _set thms might be _assocv thms, or direct to fmaps.*)
187
188Theorem merge_FST_smerge[local]:
189 !cmp:'a toto l m:('a#'b)list.
190 MAP FST (merge cmp l m) = smerge cmp (MAP FST l) (MAP FST m)
191Proof
192GEN_TAC THEN Induct THENL
193[REPEAT STRIP_TAC THEN ASM_REWRITE_TAC [merge_thm, smerge_nil, MAP]
194,P_PGEN_TAC (Term`(a:'a,b:'b)`) THEN Induct THENL
195 [REPEAT STRIP_TAC THEN ASM_REWRITE_TAC [merge_thm, smerge_nil, MAP]
196 ,P_PGEN_TAC (Term`(a':'a,b':'b)`) THEN
197 SRW_TAC [] [merge_thm, smerge, MAP, FST] THEN
198 Cases_on `apto cmp a a'` THEN
199 SRW_TAC [] []
200]]
201QED
202
203Theorem merge_ORL[local]:
204 !cmp:'a toto l m:('a#'b)list.
205 ORL cmp l /\ ORL cmp m ==> ORL cmp (merge cmp l m)
206Proof
207METIS_TAC [smerge_OL, merge_FST_smerge, ORL_OL_FST]
208QED
209
210(* **** We need to show that assocv is preserved by sorting **** *)
211
212Theorem merge_subset_union[local]:
213 !cmp:'a toto l m:('a#'b)list h.
214 MEM h (merge cmp l m) ==> MEM h l \/ MEM h m
215Proof
216HO_MATCH_MP_TAC merge_ind THEN
217REPEAT CONJ_TAC THEN REPEAT GEN_TAC THENL
218[REWRITE_TAC [MEM, merge]
219,REWRITE_TAC [MEM, merge]
220,CONV_TAC (RAND_CONV (REWRITE_CONV [merge])) THEN
221 Cases_on `apto cmp a1 a2` THEN
222 REWRITE_TAC [all_cpn_distinct] THEN
223 STRIP_TAC THEN GEN_TAC THEN REWRITE_TAC [cpn_case_def] THEN
224 CONV_TAC (LAND_CONV (REWRITE_CONV [MEM])) THEN
225 STRIP_TAC THEN RES_TAC THEN ASM_REWRITE_TAC [MEM]]
226QED
227
228Theorem MEM_MEM_merge[local]:
229 !cmp:'a toto l m:('a#'b)list x y.
230 MEM (x,y) l ==> MEM (x,y) (merge cmp l m)
231Proof
232HO_MATCH_MP_TAC merge_ind THEN
233REPEAT CONJ_TAC THEN REPEAT GEN_TAC THEN REWRITE_TAC [MEM, merge] THEN
234Cases_on `apto cmp a1 a2` THEN
235REWRITE_TAC [all_cpn_distinct] THEN
236REPEAT STRIP_TAC THEN REWRITE_TAC [cpn_case_def, MEM] THEN RES_TAC THEN AR
237QED
238
239Theorem NOT_MEM_merge[local]:
240 !cmp:'a toto l m:('a#'b)list x y. (!z.~MEM (x,z) l) ==>
241 (MEM (x,y) (merge cmp l m) <=> MEM (x,y) m)
242Proof
243HO_MATCH_MP_TAC merge_ind THEN
244REPEAT CONJ_TAC THEN REPEAT GEN_TAC THEN REWRITE_TAC [MEM, merge] THENL
245[DISCH_TAC THEN AR
246,REWRITE_TAC [DE_MORGAN_THM] THEN CONV_TAC (DEPTH_CONV FORALL_AND_CONV) THEN
247 Cases_on `apto cmp a1 a2` THEN
248 REWRITE_TAC [cpn_distinct, GSYM cpn_distinct] THEN
249 REPEAT STRIP_TAC THEN
250 REWRITE_TAC [cpn_case_def, MEM] THENL
251 [RES_TAC THEN AR
252 ,IMP_RES_THEN (REWRITE_TAC o ulist o SYM) toto_equal_imp_eq THEN
253 RES_TAC THEN UNDISCH_TAC (Term`!z. (x:'a,z:'b) <> (a1,b1)`) THEN
254 ASM_REWRITE_TAC [PAIR_EQ, DE_MORGAN_THM] THEN
255 CONV_TAC (LAND_CONV (FORALL_OR_CONV THENC (RAND_CONV FORALL_NOT_CONV))) THEN
256 SUBGOAL_THEN (Term`?z:'b.z=b1`) (REWRITE_TAC o ulist) THENL
257 [EXISTS_TAC (Term`b1:'b`) THEN REFL_TAC
258 ,DISCH_TAC THEN AR
259 ]
260 ,RES_TAC THEN AR
261]]
262QED
263
264(* By good fortune, the previous three lemmas about merge (including
265 merge_subset_union) did not care if the lists were sorted or not. *)
266
267(* ****** more lemmas that do need an ORL hypothesis ****** *)
268
269Theorem ORL_single_valued[local]:
270 !cmp l. ORL cmp l ==>
271 !x:'a y:'b z. MEM (x,y) l /\ MEM (x,z) l ==> (z = y)
272Proof
273GEN_TAC THEN Induct THENL
274[REWRITE_TAC [MEM]
275,P_PGEN_TAC (Term`p:'a,q:'b`) THEN
276 DISCH_TAC THEN IMP_RES_TAC ORL THEN REPEAT GEN_TAC THEN
277 Cases_on `apto cmp x p` THEN
278 IMP_RES_TAC toto_glneq THEN IMP_RES_TAC toto_equal_imp_eq THEN
279 ASM_REWRITE_TAC [MEM, PAIR_EQ] THEN STRIP_TAC THEN RES_TAC THENL
280 [AR
281 ,IMP_RES_THEN MP_TAC toto_glneq THEN REWRITE_TAC []
282 ,IMP_RES_THEN MP_TAC toto_glneq THEN REWRITE_TAC []
283 ]]
284QED
285
286Theorem merge_MEM_thm[local]:
287 !cmp:'a toto l m:('a#'b)list. ORL cmp l /\ ORL cmp m ==>
288 (!x y. MEM (x,y) (merge cmp l m)
289 <=> MEM (x,y) l \/ MEM (x,y) m /\ !z.~MEM (x,z) l)
290Proof
291REPEAT STRIP_TAC THEN EQ_TAC THENL
292[Cases_on `!z. ~MEM (x,z) l` THENL
293 [DISCH_TAC THEN IMP_RES_TAC merge_subset_union THEN AR
294 ,DISCH_TAC THEN
295 UNDISCH_TAC (Term`~!z. ~MEM (x:'a,z:'b) l`) THEN
296 CONV_TAC (LAND_CONV NOT_FORALL_CONV) THEN REWRITE_TAC [] THEN STRIP_TAC THEN
297 SUBGOAL_THEN (Term`MEM (x:'a,z:'b) (merge cmp l m)`) ASSUME_TAC THENL
298 [IMP_RES_TAC MEM_MEM_merge THEN AR
299 ,SUBGOAL_THEN (Term`ORL cmp (merge cmp (l:('a#'b)list) m)`)
300 (MP_TAC o MATCH_MP ORL_single_valued) THENL
301 [MATCH_MP_TAC merge_ORL THEN AR
302 ,DISCH_THEN (fn imp =>
303 SUBGOAL_THEN (Term`y:'b = z`) (ASM_REWRITE_TAC o ulist) THEN
304 MATCH_MP_TAC imp) THEN
305 EXISTS_TAC (Term`x:'a`) THEN AR
306 ]]]
307,STRIP_TAC THENL
308 [IMP_RES_TAC MEM_MEM_merge THEN AR
309 ,IMP_RES_TAC NOT_MEM_merge THEN AR
310]]
311QED
312
313Theorem ORL_TL[local]:
314 !cmp ab:('a#'b) l. ORL cmp (ab::l) ==> ORL cmp l
315Proof
316GEN_TAC THEN P_PGEN_TAC (Term`a:'a,b:'b`) THEN
317REWRITE_TAC [ORL] THEN REPEAT STRIP_TAC THEN AR
318QED
319
320Theorem assocv_MEM_thm[local]:
321 !cmp l. ORL cmp l ==> (!x:'a y:'b. (assocv l x = SOME y) <=> MEM (x,y) l)
322Proof
323GEN_TAC THEN Induct THENL
324[REWRITE_TAC [assocv, MEM, option_CLAUSES]
325,P_PGEN_TAC (Term`p:'a,q:'b`) THEN
326 DISCH_TAC THEN REPEAT GEN_TAC THEN IMP_RES_TAC ORL_TL THEN RES_TAC THEN
327 Cases_on `x = p` THENL
328 [EQ_TAC THENL
329 [ASM_REWRITE_TAC [assocv, MEM, PAIR_EQ, option_CLAUSES] THEN
330 DISCH_TAC THEN AR
331 ,SUBGOAL_THEN (Term`MEM (x:'a,q:'b) ((p,q)::l)`) ASSUME_TAC THENL
332 [ASM_REWRITE_TAC [MEM]
333 ,DISCH_TAC THEN SUBGOAL_THEN (Term`q:'b = y`)
334 (fn eq => ASSUME_TAC eq THEN
335 ASM_REWRITE_TAC [assocv, option_CLAUSES]) THEN
336 IMP_RES_TAC ORL_single_valued]]
337 ,ASM_REWRITE_TAC [MEM, assocv, PAIR_EQ]
338]]
339QED
340
341(* Following 2 lemmas can be proved with hypothesis ORL cmp l from
342 assoc_MEM_thm, but are easier to use without the hypothesis. *)
343
344Theorem assocv_NOT_MEM[local]:
345 !x:'a l. (assocv l x = NONE) <=> !y:'b. ~MEM (x,y) l
346Proof
347GEN_TAC THEN Induct THEN REWRITE_TAC [assocv, MEM] THEN
348P_PGEN_TAC (Term`a:'a,b:'b`) THEN
349ASM_REWRITE_TAC [assocv, PAIR_EQ] THEN COND_CASES_TAC THENL
350[REWRITE_TAC [option_CLAUSES] THEN CONV_TAC NOT_FORALL_CONV THEN
351 EXISTS_TAC (Term`b:'b`) THEN REWRITE_TAC []
352,AR]
353QED
354
355Theorem NOT_MEM_merge[local]:
356 !cmp:'a toto l m. ORL cmp l /\ ORL cmp m ==>
357 !a. (!z. ~MEM (a:'a,z:'b) (merge cmp l m)) ==>
358 (!z. ~MEM (a,z) l) /\ (!z. ~MEM (a,z) m)
359Proof
360REPEAT GEN_TAC THEN DISCH_THEN (fn conj => GEN_TAC THEN
361 ASSUME_TAC (MATCH_MP merge_ORL conj) THEN
362CONV_TAC (RAND_CONV (AND_FORALL_CONV THENC
363 QUANT_CONV (REWRITE_CONV [GSYM DE_MORGAN_THM])) THENC
364 BINOP_CONV FORALL_NOT_CONV THENC
365 CONTRAPOS_CONV THENC REWRITE_CONV [NOT_CLAUSES]) THEN
366STRIP_TAC THEN MP_TAC (MATCH_MP merge_MEM_thm conj)) THENL
367[DISCH_TAC THEN EXISTS_TAC (Term`z:'b`) THEN
368 MATCH_MP_TAC MEM_MEM_merge THEN AR
369,DISCH_THEN (REWRITE_TAC o ulist) THEN
370 Cases_on `?y. MEM (a,y) l` THENL
371 [UNDISCH_TAC (Term`?y. MEM (a:'a,y:'b) l`) THEN STRIP_TAC THEN
372 EXISTS_TAC (Term`y:'b`) THEN AR
373 ,UNDISCH_TAC (Term`~?y. MEM (a:'a,y:'b) l`) THEN
374 CONV_TAC (LAND_CONV NOT_EXISTS_CONV) THEN DISCH_TAC THEN
375 EXISTS_TAC (Term`z:'b`) THEN AR
376]]
377QED
378
379Theorem assocv_merge[local]:
380 !cmp l m:('a#'b)list a.
381 ORL cmp l /\ ORL cmp m ==>
382 (assocv (merge cmp l m) a = optry (assocv l a) (assocv m a))
383Proof
384REPEAT GEN_TAC THEN DISCH_THEN (fn conj =>
385 ASSUME_TAC (MATCH_MP merge_ORL conj) THEN
386 MP_TAC (MATCH_MP merge_MEM_thm conj) THEN
387 ASSUME_TAC conj) THEN
388Cases_on `assocv (merge cmp l m) a` THEN
389REWRITE_TAC [optry_case] THENL
390[DISCH_THEN (fn th => ALL_TAC) THEN IMP_RES_TAC assocv_NOT_MEM THEN
391 SUBGOAL_THEN (Term`(!b. ~MEM (a:'a,b:'b) l) /\ !b. ~MEM (a:'a,b:'b) m`)
392 MP_TAC THENL
393 [CONJ_TAC THEN IMP_RES_TAC (MATCH_MP NOT_MEM_merge
394 (ASSUME (Term`ORL cmp (l:('a#'b)list) /\
395 ORL cmp (m:('a#'b)list)`)))
396 ,REWRITE_TAC [GSYM assocv_NOT_MEM] THEN STRIP_TAC THEN
397 ASM_REWRITE_TAC [option_CLAUSES]
398 ]
399,IMP_RES_TAC assocv_MEM_thm THEN
400 DISCH_THEN (IMP_RES_THEN MP_TAC) THEN
401 UNDISCH_TAC (Term`ORL cmp (l:('a#'b)list) /\
402 ORL cmp (m:('a#'b)list)`) THEN STRIP_TAC THEN
403 STRIP_TAC THENL
404 [IMP_RES_TAC assocv_MEM_thm THEN ASM_REWRITE_TAC [option_CLAUSES] THEN
405 BETA_TAC THEN REFL_TAC
406 ,IMP_RES_TAC assocv_NOT_MEM THEN
407 IMP_RES_TAC assocv_MEM_thm THEN ASM_REWRITE_TAC [option_CLAUSES]
408 ]]
409QED
410
411Theorem merge_fun[local]:
412 !cmp:'a toto l:('a#'b)list m. ORL cmp l /\ ORL cmp m ==>
413(assocv (merge cmp l m) = OPTION_UPDATE (assocv l) (assocv m))
414Proof
415REPEAT STRIP_TAC THEN
416CONV_TAC FUN_EQ_CONV THEN REWRITE_TAC [OPTION_UPDATE] THEN
417MATCH_MP_TAC assocv_merge THEN AR
418QED
419
420(* Continue development of sorting in same imitative style as for merge. *)
421
422Definition incr_merge:
423 (incr_merge cmp (l:('a#'b)list) [] = [SOME l])
424/\ (incr_merge cmp (l:('a#'b)list) (NONE :: lol) = SOME l :: lol)
425/\ (incr_merge cmp (l:('a#'b)list) (SOME m :: lol) =
426 NONE :: incr_merge cmp (merge cmp l m) lol)
427End
428
429Definition ORL_sublists: (ORL_sublists cmp ([]:('a#'b)list option list) = T)
430 /\ (ORL_sublists cmp (NONE :: (lol:('a#'b)list option list)) =
431 ORL_sublists cmp lol)
432 /\ (ORL_sublists cmp (SOME m :: (lol:('a#'b)list option list)) =
433 ORL cmp m /\ ORL_sublists cmp lol)
434End
435
436val ORL_sublists_ind = theorem"ORL_sublists_ind";
437
438(* ORL_sublists_ind =
439 |- !P. (!cmp. P cmp []) /\ (!cmp lol. P cmp lol ==> P cmp (NONE::lol)) /\
440 (!cmp m lol. P cmp lol ==> P cmp (SOME m::lol)) ==>
441 !v v1. P v v1 *)
442
443Theorem ORL_OL_FST_sublists[local]:
444 !cmp lol:('a#'b)list option list. ORL_sublists cmp lol =
445 OL_sublists cmp (MAP (OPTION_MAP (MAP FST)) lol)
446Proof
447GEN_TAC THEN Induct THENL
448[RW_TAC (srw_ss()) [ORL_sublists, OL_sublists, MAP]
449,Cases THEN
450 SRW_TAC [] [ORL_sublists, OL_sublists, MAP, OPTION_MAP_DEF] THEN
451 ASM_REWRITE_TAC [ORL_OL_FST]
452]
453QED
454
455Theorem incr_merge_FST_smerge[local]:
456 !cmp lol l:('a#'b)list. MAP (OPTION_MAP (MAP FST)) (incr_merge cmp l lol) =
457incr_smerge cmp (MAP FST l) (MAP (OPTION_MAP (MAP FST)) lol)
458Proof
459GEN_TAC THEN Induct THENL
460[RW_TAC (srw_ss()) [incr_merge, incr_smerge, MAP]
461,Cases THEN
462 SRW_TAC [] [incr_merge, incr_smerge, MAP, OPTION_MAP_DEF] THEN
463 REWRITE_TAC [merge_FST_smerge]
464]
465QED
466
467Theorem incr_merge_ORL[local]:
468 !cmp:'a toto l:('a#'b)list lol. ORL cmp l /\
469 ORL_sublists cmp lol ==> ORL_sublists cmp (incr_merge cmp l lol)
470Proof
471METIS_TAC [smerge_OL, incr_smerge_OL, merge_ORL, merge_FST_smerge,
472 incr_merge_FST_smerge, ORL_OL_FST, ORL_OL_FST_sublists]
473QED
474
475Theorem NOT_MEM_NIL[local]:
476 (!x:'c. ~MEM x l) <=> (l = [])
477Proof
478EQ_TAC THENL
479[CONV_TAC (CONTRAPOS_CONV THENC (RAND_CONV (NOT_FORALL_CONV))) THEN
480 Cases_on `l` THEN SRW_TAC [] [] THEN
481 Q.EXISTS_TAC `h` THEN REWRITE_TAC []
482,RW_TAC bool_ss [MEM]]
483QED
484
485Theorem SOME_MEM_NOT_NIL[local]:
486 ~(!ab:'a#'b. MEM ab ((x,y)::l) <=> MEM ab [])
487Proof
488RW_TAC (srw_ss()) [MEM] THEN Q.EXISTS_TAC `x,y` THEN REWRITE_TAC []
489QED
490
491Theorem ORL_NOT_MEM[local]:
492 (!cmp (b:'b) x y l. ORL cmp ((x:'a,y)::l) ==> ~MEM (x,b) l) /\
493 (!cmp (a:'a) (b:'b) x y l. ORL cmp ((x,y)::l) /\ (apto cmp a x = LESS) ==>
494 ~MEM (a,b) ((x,y)::l))
495Proof
496CONJ_TAC THEN REPEAT GEN_TAC THEN REWRITE_TAC [ORL] THEN STRIP_TAC THENL
497[DISCH_TAC THEN RES_THEN MP_TAC
498,REWRITE_TAC [MEM, DE_MORGAN_THM, PAIR_EQ] THEN
499 IMP_RES_TAC toto_glneq THEN AR THEN
500 STRIP_TAC THEN RES_TAC THEN IMP_RES_TAC totoLLtrans THEN
501 UNDISCH_TAC (Term`apto cmp a (a:'a) = LESS`)] THEN
502REWRITE_TAC [toto_refl, all_cpn_distinct]
503QED
504
505Theorem ORL_MEM_FST[local]:
506 !cmp l:('a#'b)list. ORL cmp l ==>
507 !x y p q. MEM (x,y) l /\ MEM (p,q) l /\ (x = p) ==> (y = q)
508Proof
509GEN_TAC THEN Induct THENL
510[REWRITE_TAC [MEM]
511,P_PGEN_TAC ``g:'a,h:'b`` THEN SRW_TAC [] [] THENL
512[`~MEM (g,q) l`
513 by (MATCH_MP_TAC (CONJUNCT1 ORL_NOT_MEM) THEN
514 Q.EXISTS_TAC `cmp` THEN Q.EXISTS_TAC `h` THEN AR)
515,`~MEM (g,y) l` by (MATCH_MP_TAC (CONJUNCT1 ORL_NOT_MEM) THEN
516 Q.EXISTS_TAC `cmp` THEN Q.EXISTS_TAC `h` THEN AR)
517,IMP_RES_TAC ORL_TL THEN `p = p` by REFL_TAC THEN RES_TAC
518]]
519QED
520
521Theorem ORL_MEM_EQ[local]:
522 !cmp l m:('a#'b)list. ORL cmp l /\ ORL cmp m ==>
523 ((!ab. MEM ab l <=> MEM ab m) <=> (l = m))
524Proof
525GEN_TAC THEN Induct THENL
526[SRW_TAC [] [GSYM NOT_MEM_NIL]
527,P_PGEN_TAC ``x:'a,y:'b`` THEN Induct THENL
528 [RW_TAC (srw_ss()) [SOME_MEM_NOT_NIL]
529 ,P_PGEN_TAC ``p:'a,q:'b`` THEN
530 STRIP_TAC THEN IMP_RES_TAC ORL_NOT_MEM THEN
531 EQ_TAC THENL
532 [Cases_on `apto cmp x p` THENL
533 [CONV_TAC LEFT_IMP_FORALL_CONV THEN
534 Q.EXISTS_TAC `x,y` THEN
535 `~MEM (x,y) ((p,q)::m)` by (RES_TAC THEN AR) THEN ASM_REWRITE_TAC [MEM]
536 ,REWRITE_TAC [list_11, PAIR_EQ] THEN
537 Q.SUBGOAL_THEN `(!ab. MEM ab l <=> MEM ab m) <=> (l = m)` (SUBST1_TAC o SYM)
538 THEN1 (IMP_RES_TAC ORL_TL THEN RES_TAC) THEN
539 `x = p` by IMP_RES_TAC toto_equal_eq THEN
540 `MEM (x,y) ((x,y)::l)` by REWRITE_TAC [MEM] THEN
541 `MEM (p,q) ((p,q)::m)` by REWRITE_TAC [MEM] THEN
542 DISCH_THEN (fn eq => `MEM (p,q) ((x,y)::l)` by ASM_REWRITE_TAC [eq] THEN
543 ASSUME_TAC eq) THEN
544 `y = q` by IMP_RES_TAC ORL_MEM_FST THEN
545 AR THEN P_PGEN_TAC ``g:'a,h:'b`` THEN
546 Cases_on `(g = x) /\ (h = y)` THENL
547 [METIS_TAC [PAIR_EQ]
548 ,Q.SUBGOAL_THEN `MEM (g,h) l = MEM (g,h) ((x,y)::l)` SUBST1_TAC
549 THEN1 (REWRITE_TAC [MEM, PAIR_EQ] THEN METIS_TAC []) THEN
550 Q.SUBGOAL_THEN `MEM (g,h) m = MEM (g,h) ((p,q)::m)` SUBST1_TAC
551 THEN1 (REWRITE_TAC [MEM, PAIR_EQ] THEN METIS_TAC []) THEN AR
552 ]
553 ,`apto cmp p x = LESS` by IMP_RES_TAC toto_antisym THEN
554 CONV_TAC LEFT_IMP_FORALL_CONV THEN
555 Q.EXISTS_TAC `p,q` THEN
556 `~MEM (p,q) ((x,y)::l)` by (RES_TAC THEN AR) THEN ASM_REWRITE_TAC [MEM]
557 ]
558 ,DISCH_TAC THEN AR
559]]]
560QED
561
562Theorem merge_ASSOC[local]:
563 !cmp:'a toto k l m:('a#'b)list. ORL cmp k /\ ORL cmp l /\ ORL cmp m ==>
564 (merge cmp k (merge cmp l m) = merge cmp (merge cmp k l) m)
565Proof
566REPEAT STRIP_TAC THEN
567`ORL cmp (merge cmp l m) /\ ORL cmp (merge cmp k l)` by
568 (CONJ_TAC THEN MATCH_MP_TAC merge_ORL THEN AR) THEN
569Q.SUBGOAL_THEN `ORL cmp (merge cmp k (merge cmp l m)) /\
570 ORL cmp (merge cmp (merge cmp k l) m)`
571(fn cj => REWRITE_TAC [GSYM (MATCH_MP ORL_MEM_EQ cj)] THEN STRIP_ASSUME_TAC cj)
572THEN1 (CONJ_TAC THEN MATCH_MP_TAC merge_ORL THEN AR) THEN
573P_PGEN_TAC ``x:'a,y:'b`` THEN
574REWRITE_TAC [MATCH_MP merge_MEM_thm (CONJ (Q.ASSUME `ORL cmp k`)
575 (Q.ASSUME `ORL cmp (merge cmp l m)`))]
576 THEN
577REWRITE_TAC [MATCH_MP merge_MEM_thm (CONJ (Q.ASSUME `ORL cmp l`)
578 (Q.ASSUME `ORL cmp m`))] THEN
579REWRITE_TAC [MATCH_MP merge_MEM_thm (CONJ (Q.ASSUME `ORL cmp
580 (merge cmp k l)`) (Q.ASSUME `ORL cmp m`))] THEN
581REWRITE_TAC [MATCH_MP merge_MEM_thm (CONJ (Q.ASSUME `ORL cmp k`)
582 (Q.ASSUME `ORL cmp l`))] THEN
583METIS_TAC []
584QED
585
586(* Now to figure out how to use merge_ASSOC. Idea, I think, is to show
587 that assocv o merge_out is preserved throughout. *)
588
589Theorem OPTION_UPDATE_ASSOC[local]:
590 !f g h:'a -> 'b option. OPTION_UPDATE f (OPTION_UPDATE g h) =
591 OPTION_UPDATE (OPTION_UPDATE f g) h
592Proof
593REPEAT GEN_TAC THEN CONV_TAC FUN_EQ_CONV THEN
594REWRITE_TAC [OPTION_UPDATE, optry_ASSOC]
595QED
596
597Definition incr_build: (incr_build cmp [] = [])
598 /\ (incr_build cmp (ab:('a#'b) :: l) =
599 incr_merge cmp [ab] (incr_build cmp l))
600End
601
602Theorem incr_build_ORL[local]:
603 !cmp l:('a#'b)list. ORL_sublists cmp (incr_build cmp l)
604Proof
605GEN_TAC THEN Induct THEN REWRITE_TAC [incr_build] THENL
606[REWRITE_TAC [ORL_sublists]
607,P_PGEN_TAC (Term`a:'a,b:'b`) THEN MATCH_MP_TAC incr_merge_ORL THEN
608 ASM_REWRITE_TAC [ORL, MEM]]
609QED
610
611Definition merge_out:
612 (merge_out (cmp:'a toto) (l:('a#'b)list) ([]:('a#'b)list option list) = l)
613/\ (merge_out cmp (l:('a#'b)list) (NONE :: lol) = merge_out cmp l lol)
614/\ (merge_out cmp (l:('a#'b)list) ((SOME (m:('a#'b)list)) :: lol) =
615 merge_out cmp (merge cmp l m) lol)
616End
617
618Theorem merge_out_ORL[local]:
619 !cmp lol:('a#'b)list option list l. ORL cmp l /\
620 ORL_sublists cmp lol ==> ORL cmp (merge_out cmp l lol)
621Proof
622HO_MATCH_MP_TAC ORL_sublists_ind THEN REPEAT STRIP_TAC THEN
623ASM_REWRITE_TAC [merge_out] THEN
624IMP_RES_TAC ORL_sublists THEN RES_TAC THEN
625SUBGOAL_THEN (Term`ORL cmp (merge cmp l m:('a#'b)list)`)
626 (fn th => ASSUME_TAC th THEN RES_TAC) THEN
627IMP_RES_TAC merge_ORL
628QED
629
630Definition incr_flat: incr_flat
631 (cmp:'a toto) (lol:('a#'b)list option list) = merge_out cmp [] lol
632End
633
634(* by not utilizing incr_flat in incr_sort, we ease writing conversions. *)
635
636Definition incr_sort: incr_sort (cmp:'a toto) (l:('a#'b)list) =
637 merge_out cmp [] (incr_build cmp l)
638End
639
640Theorem incr_sort_ORL[local]:
641 !cmp l:('a#'b)list. ORL cmp (incr_sort cmp l)
642Proof
643REPEAT GEN_TAC THEN REWRITE_TAC [incr_sort, incr_flat] THEN
644MATCH_MP_TAC merge_out_ORL THEN
645REWRITE_TAC [ORL, incr_build_ORL]
646QED
647
648(* ************ work up to incr_sort_fun *********** *)
649
650Definition OPTION_FLAT:
651 (OPTION_FLAT ([]:'z list option list) = []) /\
652 (OPTION_FLAT (NONE:'z list option :: l) = OPTION_FLAT l) /\
653 (OPTION_FLAT (SOME a :: l) = a ++ OPTION_FLAT l)
654End
655
656val OPTION_FLAT_ind = theorem "OPTION_FLAT_ind";
657
658(* OPTION_FLAT_ind = |- !P. P [] /\ (!l. P l ==> P (NONE::l)) /\
659 (!a l. P l ==> P (SOME a::l)) ==> !v. P v *)
660
661Theorem assocv_optry_lem[local]:
662 !x l:('a#'b)list m. assocv (l ++ m) x = optry (assocv l x) (assocv m x)
663Proof
664GEN_TAC THEN Induct THEN REWRITE_TAC [APPEND, optry_ID, assocv] THEN
665P_PGEN_TAC (Term`p:'a,q:'b`) THEN
666REWRITE_TAC [assocv] THEN Cases_on `x = p` THEN AR THEN REWRITE_TAC [optry]
667QED
668
669Theorem assocv_APPEND[local]:
670 !l:('a#'b)list m. assocv (l ++ m) = OPTION_UPDATE (assocv l) (assocv m)
671Proof
672REPEAT GEN_TAC THEN CONV_TAC FUN_EQ_CONV THEN
673REWRITE_TAC [OPTION_UPDATE, assocv_optry_lem]
674QED
675
676Theorem assocv_merge_out[local]:
677 !cmp lol:('a#'b)list option list l. ORL cmp l /\ ORL_sublists cmp lol ==>
678 (assocv (merge_out cmp l lol) = assocv (l ++ OPTION_FLAT lol))
679Proof
680GEN_TAC THEN
681HO_MATCH_MP_TAC OPTION_FLAT_ind THEN
682SRW_TAC [] [OPTION_FLAT, merge_out] THENL
683[`ORL_sublists cmp lol` by (ONCE_REWRITE_TAC [GSYM ORL_sublists] THEN AR) THEN
684 RES_TAC
685,`ORL cmp a /\ ORL_sublists cmp lol` by REWRITE_TAC [REWRITE_RULE
686 [ORL_sublists] (Q.ASSUME `ORL_sublists cmp (SOME a ::lol)`)] THEN
687 `ORL cmp (merge cmp l a)` by
688 (MATCH_MP_TAC merge_ORL THEN AR) THEN
689 RES_TAC THEN IMP_RES_TAC merge_fun THEN ASM_REWRITE_TAC [assocv_APPEND]
690]
691QED
692
693Theorem assocv_incr_flat[local]:
694 !cmp lol:('a#'b)list option list. ORL_sublists cmp lol ==>
695 (assocv (incr_flat cmp lol) = assocv (OPTION_FLAT lol))
696Proof
697REPEAT STRIP_TAC THEN `ORL cmp []` by REWRITE_TAC [ORL] THEN
698IMP_RES_TAC assocv_merge_out THEN POP_ASSUM MP_TAC THEN
699REWRITE_TAC [incr_flat, APPEND]
700QED
701
702Theorem assocv_incr_merge[local]:
703 !cmp lol:('a#'b)list option list l m. ORL cmp l /\ ORL cmp m /\
704 ORL_sublists cmp lol ==>
705 (assocv (merge_out cmp l (incr_merge cmp m lol)) =
706 assocv (merge_out cmp (merge cmp l m) lol))
707Proof
708GEN_TAC THEN Induct THEN SRW_TAC []
709 [assocv_merge_out, OPTION_FLAT, merge_out, incr_merge, assocv_APPEND] THEN
710Cases_on `h` THEN SRW_TAC [] [incr_merge, merge_out] THEN
711`ORL cmp x /\ ORL_sublists cmp lol` by METIS_TAC [ORL_sublists] THEN
712Q.SUBGOAL_THEN `merge cmp (merge cmp l m) x = merge cmp l (merge cmp m x)`
713SUBST1_TAC THEN1 (MATCH_MP_TAC (GSYM merge_ASSOC) THEN AR) THEN
714`ORL cmp (merge cmp m x)` by (MATCH_MP_TAC merge_ORL THEN AR) THEN
715`ORL_sublists cmp (incr_merge cmp (merge cmp m x) lol)` by
716 (MATCH_MP_TAC incr_merge_ORL THEN AR) THEN
717METIS_TAC [assocv_merge_out]
718QED
719
720Theorem assocv_NIL[local]:
721 assocv ([]:('a#'b)list) = K NONE
722Proof
723CONV_TAC FUN_EQ_CONV THEN SRW_TAC [] [assocv]
724QED
725
726Theorem OPTION_UPDATE_K_NONE[local]:
727 !f:'a->'b option. (OPTION_UPDATE f (K NONE) = f) /\
728 (OPTION_UPDATE (K NONE) f = f)
729Proof
730CONV_TAC (ONCE_DEPTH_CONV FUN_EQ_CONV) THEN
731SRW_TAC [] [OPTION_UPDATE, optry_ID]
732QED
733
734Theorem ORL_SING[local]:
735 !cmp x:('a#'b). ORL cmp [x]
736Proof
737GEN_TAC THEN P_PGEN_TAC ``a:'a,b:'b`` THEN REWRITE_TAC [ORL, MEM]
738QED
739
740Theorem assocv_incr_build[local]:
741 !cmp:'a toto m l:('a#'b)list. ORL cmp l ==>
742 (assocv (merge_out cmp l (incr_build cmp m)) = assocv (l ++ m))
743Proof
744GEN_TAC THEN Induct THEN
745SRW_TAC [] [assocv_APPEND, incr_build, merge_out] THENL
746[REWRITE_TAC [OPTION_UPDATE_K_NONE, assocv_NIL, merge_thm]
747,Q.SUBGOAL_THEN
748 `OPTION_UPDATE (assocv l) (assocv (h::m)) = assocv ((l ++ [h]) ++ m)`
749 SUBST1_TAC THENL
750 [Q.SUBGOAL_THEN `h::m = [h] ++ m` SUBST1_TAC THEN1 REWRITE_TAC [APPEND] THEN
751 SRW_TAC [] [assocv_APPEND, OPTION_UPDATE_ASSOC]
752 ,`ORL cmp [h]` by MATCH_ACCEPT_TAC ORL_SING THEN
753 `ORL_sublists cmp (incr_build cmp m)` by MATCH_ACCEPT_TAC incr_build_ORL THEN
754 Q.SUBGOAL_THEN
755 `assocv (merge_out cmp l (incr_merge cmp [h] (incr_build cmp m))) =
756 assocv (merge_out cmp (merge cmp l [h]) (incr_build cmp m))`
757 SUBST1_TAC THEN1 (MATCH_MP_TAC assocv_incr_merge THEN AR) THEN
758 `ORL cmp (merge cmp l [h])` by (MATCH_MP_TAC merge_ORL THEN AR) THEN
759 RES_THEN SUBST1_TAC THEN
760 METIS_TAC [merge_fun, assocv_APPEND]
761]]
762QED
763
764(* at last: incr_sort not only sorts, but it is stable in the sense that
765 the list coming out (with guaranteed only one entry for any key) has the
766 same behavior under assocv as the (possibly duplicitous) list going in. *)
767
768Theorem incr_sort_fun[local]:
769 !cmp: 'a toto l:('a#'b)list. assocv (incr_sort cmp l) = assocv l
770Proof
771REPEAT GEN_TAC THEN REWRITE_TAC [incr_sort, incr_flat] THEN
772Q.SUBGOAL_THEN `assocv l = assocv ([] ++ l)` SUBST1_TAC
773THEN1 REWRITE_TAC [APPEND] THEN
774MATCH_MP_TAC assocv_incr_build THEN REWRITE_TAC [ORL]
775QED
776
777(* ********** Relating association lists to finite maps ************ *)
778(* Define "unlookup", sending an option-valued function to an fmap. *)
779(* ***************************************************************** *)
780
781Definition unlookup: unlookup (f:'a -> 'b option) =
782 FUN_FMAP (THE o f) (IS_SOME o f)
783End
784
785(* and prove that unlookup sends OPTION_UPDATE to FUNION *)
786
787(* ********* We require a short interlude relating option-valued ******** *)
788(* ********* and finite functions, via FLOOKUP and unlookup. ******** *)
789
790Theorem FUPDATE_ALT[local]:
791 !f:'a |-> 'b l. f |++ REVERSE l = FOLDR (combin$C FUPDATE) f l
792Proof
793REPEAT GEN_TAC THEN REWRITE_TAC [FUPDATE_LIST, combinTheory.C_DEF]
794THEN BETA_TAC THEN REWRITE_TAC [rich_listTheory.FOLDL_REVERSE]
795QED
796
797Theorem IS_SOME_FDOM[local]:
798 !f:'a |-> 'b. IS_SOME o FLOOKUP f = FDOM f
799Proof
800Induct THEN CONJ_TAC THENL
801[REWRITE_TAC [EXTENSION, FDOM_FEMPTY, NOT_IN_EMPTY] THEN
802 REWRITE_TAC [SPECIFICATION, combinTheory.o_THM, option_CLAUSES, FLOOKUP_EMPTY]
803,GEN_TAC THEN DISCH_THEN (ASSUME_TAC o REWRITE_RULE [combinTheory.o_THM] o
804 CONV_RULE FUN_EQ_CONV) THEN
805 REPEAT STRIP_TAC THEN
806 ASM_REWRITE_TAC [FDOM_FUPDATE, EXTENSION, IN_INSERT] THEN GEN_TAC THEN
807 REWRITE_TAC [SPECIFICATION, combinTheory.o_THM, FLOOKUP_UPDATE] THEN
808 Cases_on `x = x'` THEN ASM_REWRITE_TAC [option_CLAUSES] THEN
809 REWRITE_TAC [GSYM (ASSUME ``x:'a <> x'``)]]
810QED
811
812Theorem FINITE_FLOOKUP[local]:
813 !f:'a |-> 'b. FINITE (IS_SOME o FLOOKUP f)
814Proof
815REWRITE_TAC [IS_SOME_FDOM, FDOM_FINITE]
816QED
817
818Theorem FLOOKUP_unlookup_FDOM[local]:
819 !f:'a |-> 'b. FDOM (unlookup (FLOOKUP f)) = FDOM f
820Proof
821REWRITE_TAC [unlookup] THEN ASSUME_TAC (SPEC_ALL FINITE_FLOOKUP) THEN
822IMP_RES_TAC FUN_FMAP_DEF THEN ASM_REWRITE_TAC [IS_SOME_FDOM] THEN
823GEN_TAC THEN ASSUME_TAC (SPEC ``f':'a |-> 'b`` FDOM_FINITE) THEN
824IMP_RES_TAC FUN_FMAP_DEF THEN AR
825QED
826
827Theorem FLOOKUP_unlookup_ID[local]:
828 !f:'a |-> 'b. unlookup (FLOOKUP f) = f
829Proof
830GEN_TAC THEN REWRITE_TAC [fmap_EXT] THEN CONJ_TAC THEN
831REWRITE_TAC [FLOOKUP_unlookup_FDOM] THEN REPEAT STRIP_TAC THEN
832REWRITE_TAC [unlookup] THEN ASSUME_TAC (SPEC_ALL FINITE_FLOOKUP) THEN
833IMP_RES_THEN
834 (STRIP_ASSUME_TAC o REWRITE_RULE [IS_SOME_FDOM]) FUN_FMAP_DEF THEN
835ASM_REWRITE_TAC [IS_SOME_FDOM] THEN RES_TAC THEN
836ASM_REWRITE_TAC [option_CLAUSES, FLOOKUP_DEF, combinTheory.o_THM]
837QED
838
839Theorem unlookup_FLOOKUP_ID[local]:
840 !g:'a->'b option.
841 FINITE (IS_SOME o g) ==> (FLOOKUP (unlookup g) = g)
842Proof
843GEN_TAC THEN REWRITE_TAC [unlookup] THEN DISCH_TAC THEN
844IMP_RES_TAC (REWRITE_RULE [SPECIFICATION] FUN_FMAP_DEF) THEN
845CONV_TAC FUN_EQ_CONV THEN GEN_TAC THEN
846ASM_REWRITE_TAC [FLOOKUP_DEF, SPECIFICATION] THEN
847Cases_on `(IS_SOME o g) x` THEN
848ASM_REWRITE_TAC [option_CLAUSES] THEN REWRITE_TAC [combinTheory.o_THM] THENL
849[RES_TAC THEN AR THEN
850 UNDISCH_TAC ``(IS_SOME o (g:'a->'b option)) x`` THEN
851 ASM_REWRITE_TAC [combinTheory.o_THM, option_CLAUSES]
852,UNDISCH_TAC ``~(IS_SOME o (g:'a->'b option)) x`` THEN
853 ASM_REWRITE_TAC [combinTheory.o_THM, option_CLAUSES] THEN
854 DISCH_THEN SUBST1_TAC THEN REFL_TAC]
855QED
856
857Theorem unlookup_FDOM[local]:
858 !g:'a->'b option.
859 FINITE (IS_SOME o g) ==> (FDOM (unlookup g) = IS_SOME o g)
860Proof
861GEN_TAC THEN
862DISCH_THEN (SUBST1_TAC o SYM o MATCH_MP unlookup_FLOOKUP_ID) THEN
863REWRITE_TAC [IS_SOME_FDOM, FLOOKUP_unlookup_ID]
864QED
865
866Theorem unlookup_11[local]:
867 !f g:'a ->'b option. FINITE (IS_SOME o f) /\ FINITE (IS_SOME o g) ==>
868 (unlookup f = unlookup g) ==> (f = g)
869Proof
870REPEAT STRIP_TAC THEN
871IMP_RES_THEN
872 (PURE_ONCE_REWRITE_TAC o ulist o SYM) unlookup_FLOOKUP_ID THEN AR
873QED
874
875(* ******* end of interlude as described above; still more ********* *)
876(* ******* lemmas to come, adjusting to finite_mapTheory. ********* *)
877
878Theorem unlookup_FUNION[local]:
879 !u (v:'a -> 'b option). FINITE (IS_SOME o u) /\ FINITE (IS_SOME o v) ==>
880 (unlookup u FUNION unlookup v = unlookup (OPTION_UPDATE u v))
881Proof
882REPEAT STRIP_TAC THEN
883SUBGOAL_THEN ``FINITE (IS_SOME o OPTION_UPDATE u (v:'a -> 'b option))``
884 ASSUME_TAC
885THEN1 ASM_REWRITE_TAC [IS_SOME_OPTION_UPDATE, FINITE_UNION] THEN
886REWRITE_TAC [fmap_EXT] THEN CONJ_TAC THEN
887IMP_RES_TAC unlookup_FDOM THEN
888ASM_REWRITE_TAC [FUNION_DEF, IS_SOME_OPTION_UPDATE, IN_UNION] THEN
889REPEAT STRIP_TAC THEN
890(SUBGOAL_THEN ``x IN (IS_SOME o OPTION_UPDATE (u:'a->'b option) v)`` ASSUME_TAC
891 THEN1 ASM_REWRITE_TAC [IS_SOME_OPTION_UPDATE, IN_UNION]) THEN
892REWRITE_TAC [unlookup] THENL
893[ALL_TAC, Cases_on `x IN IS_SOME o u` THEN AR] THEN
894IMP_RES_TAC FUN_FMAP_DEF THEN
895ASM_REWRITE_TAC [combinTheory.o_THM] THEN
896IMP_RES_TAC (fst (EQ_IMP_RULE (SPEC_ALL SPECIFICATION))) THEN
897ASM_REWRITE_TAC [OPTION_UPDATE, option_CLAUSES, optry] THEN
898AP_TERM_TAC THEN
899IMP_RES_TAC (fst (EQ_IMP_RULE (INST_TYPE [beta |-> ``:bool``]
900 (SPEC_ALL combinTheory.o_THM)))) THEN
901IMP_RES_THEN (REWRITE_TAC o ulist) IS_SOME_optry THEN
902UNDISCH_TAC ``x NOTIN IS_SOME o (u:'a -> 'b option)`` THEN
903REWRITE_TAC [SPECIFICATION, combinTheory.o_THM] THEN
904Cases_on `u x` THEN REWRITE_TAC [optry, option_CLAUSES]
905QED
906
907(* ****** Get back to imitating enumeralTheory with a constant FMAPAL ***** *)
908(* ****** of type ('a#'b)bt -> ('a |-> 'b) (but call the definition ***** *)
909(* ****** bt_to_fmap, like the bt_to_set of enumeralTheory). ***** *)
910
911Definition bt_to_fmap:
912 (FMAPAL (cmp:'a toto) nt = (FEMPTY:'a|->'b)) /\
913 (FMAPAL (cmp:'a toto) (node l (x:'a,v:'b) r) =
914 DRESTRICT (FMAPAL cmp l) {y | apto cmp y x = LESS} FUNION
915 FEMPTY |+ (x,v) FUNION
916 DRESTRICT (FMAPAL cmp r) {z | apto cmp x z = LESS})
917End
918
919(* bt_to_fmap_ind = |- !P.
920 (!cmp. P cmp nt) /\
921 (!cmp l x v r. P cmp l /\ P cmp r ==> P cmp (node l (x,v) r))
922 ==> !v v1. P v v1 *)
923
924(* lemmas to help with FAPPLY_node, various _mut_rec's *)
925
926(*cf. DRESTRICT_FUNION*)
927Theorem FUNION_DRESTRICT[local]:
928 !f:'a|->'b g s.
929 DRESTRICT (f FUNION g) s = DRESTRICT f s FUNION DRESTRICT g s
930Proof
931REPEAT GEN_TAC THEN REWRITE_TAC [fmap_EXT, FDOM_DRESTRICT, FDOM_FUNION] THEN
932CONJ_TAC THENL
933[ONCE_REWRITE_TAC [INTER_COMM] THEN MATCH_ACCEPT_TAC UNION_OVER_INTER
934,GEN_TAC THEN Cases_on `x IN FDOM f` THEN ASM_REWRITE_TAC [DRESTRICT_DEF] THEN
935 ASM_REWRITE_TAC [IN_UNION, IN_INTER] THEN
936 SRW_TAC [] [FDOM_FUNION, FDOM_DRESTRICT, FUNION_DEF, DRESTRICT_DEF]]
937QED
938
939Theorem DRESTRICT_SING[local]:
940 !x:'a y:'b s. x IN s ==> (DRESTRICT (FEMPTY |+ (x,y)) s = FEMPTY |+ (x,y))
941Proof
942SRW_TAC [] [DRESTRICT_DEF]
943QED
944
945Theorem DRESTRICT_SING_FEMPTY[local]:
946 !x:'a y:'b s. x NOTIN s ==> (DRESTRICT (FEMPTY |+ (x,y)) s = FEMPTY)
947Proof
948SRW_TAC [] [DRESTRICT_DEF]
949QED
950
951Theorem DRESTRICT_IN[local]:
952 !s x f:'a|->'b. x IN s ==> (DRESTRICT f s ' x = f ' x)
953Proof
954GEN_TAC THEN GEN_TAC THEN Induct THEN
955SRW_TAC [] [DRESTRICT_DEF, IN_INTER, FAPPLY_FUPDATE_THM]
956QED
957
958Theorem DRESTRICT_NOT_IN[local]:
959 !s x f:'a|->'b. x NOTIN s ==> (DRESTRICT f s ' x = FEMPTY ' x)
960Proof
961SRW_TAC [] [DRESTRICT_DEF, IN_INTER]
962QED
963
964Theorem IN_FDOM_DRESTRICT_IMP[local]:
965 !f:'a|->'b s x. x IN FDOM (DRESTRICT f s) ==> x IN s
966Proof
967METIS_TAC [FDOM_DRESTRICT, IN_INTER]
968QED
969
970(* Following two theorems should be used by application conversion. *)
971
972Theorem FAPPLY_nt:
973 !cmp x. FMAPAL cmp (nt:('a#'b)bt) ' x = FEMPTY ' x
974Proof
975REWRITE_TAC [bt_to_fmap]
976QED
977
978Theorem FAPPLY_node:
979 !cmp x l a:'a b:'b r.
980 FMAPAL cmp (node l (a,b) r) ' x =
981 case apto cmp x a of
982 LESS => FMAPAL cmp l ' x
983 | EQUAL => b
984 | GREATER => FMAPAL cmp r ' x
985Proof
986 SRW_TAC [] [bt_to_fmap, FUNION_DEF] THENL [
987 Q.SUBGOAL_THEN `x IN {y | apto cmp y a = LESS}`
988 (fn xin => SRW_TAC [] [MATCH_MP DRESTRICT_IN xin,
989 CONV_RULE SET_SPEC_CONV xin]) THEN
990 METIS_TAC [IN_INTER, FDOM_DRESTRICT],
991
992 `apto cmp a a = LESS`
993 by IMP_RES_THEN (MATCH_ACCEPT_TAC o CONV_RULE SET_SPEC_CONV)
994 IN_FDOM_DRESTRICT_IMP THEN
995 METIS_TAC [toto_refl, all_cpn_distinct],
996
997 SRW_TAC [] [toto_refl, FAPPLY_FUPDATE_THM],
998
999 POP_ASSUM (MP_TAC o CONV_RULE (ONCE_DEPTH_CONV SET_SPEC_CONV) o
1000 REWRITE_RULE [FDOM_DRESTRICT, IN_INTER]) THEN
1001 SRW_TAC [] [] THEN
1002 Cases_on `apto cmp x a` THEN SRW_TAC [] [] THENL [
1003 IMP_RES_THEN SUBST1_TAC NOT_FDOM_FAPPLY_FEMPTY THEN
1004 Q.SUBGOAL_THEN `x NOTIN {z | apto cmp a z = LESS}`
1005 (REWRITE_TAC o ulist o MATCH_MP DRESTRICT_NOT_IN) THEN
1006 CONV_TAC (RAND_CONV SET_SPEC_CONV) THEN
1007 SRW_TAC [] [GSYM toto_antisym],
1008
1009 METIS_TAC [toto_equal_eq],
1010
1011 Q.SUBGOAL_THEN `x IN {z | apto cmp a z = LESS}`
1012 (REWRITE_TAC o ulist o MATCH_MP DRESTRICT_IN) THEN
1013 CONV_TAC SET_SPEC_CONV THEN ASM_REWRITE_TAC [GSYM toto_antisym]
1014 ]
1015 ]
1016QED
1017
1018(* Following theorems prepare for converting bt's to association lists. *)
1019
1020Definition bt_to_fmap_lb: bt_to_fmap_lb cmp lb (t:('a#'b)bt) =
1021 DRESTRICT (FMAPAL cmp t) {x | apto cmp lb x = LESS}
1022End
1023
1024Definition bt_to_fmap_ub: bt_to_fmap_ub cmp (t:('a#'b)bt) ub =
1025 DRESTRICT (FMAPAL cmp t) {x | apto cmp x ub = LESS}
1026End
1027
1028Theorem bt_to_fmap_mut_rec[local]:
1029 !cmp:'a toto l x y r. FMAPAL cmp (node l (x:'a,y:'b) r) =
1030 bt_to_fmap_ub cmp l x FUNION FEMPTY |+ (x,y) FUNION bt_to_fmap_lb cmp x r
1031Proof
1032 REWRITE_TAC [bt_to_fmap_lb, bt_to_fmap_ub, bt_to_fmap]
1033QED
1034
1035Definition bt_to_fmap_lb_ub: bt_to_fmap_lb_ub cmp lb (t:('a#'b)bt) ub =
1036DRESTRICT (FMAPAL cmp t) {x | (apto cmp lb x = LESS) /\
1037 (apto cmp x ub = LESS)}
1038End
1039
1040(* ******** Interlude defining bt_map and connecting it with ENUMERAL, FST,
1041 FMAPAL, and FDOM. bt_map will be used by o_f_CONV. ****** *)
1042
1043Definition bt_map:
1044 (bt_map (f:'a ->'b) (nt:'a bt) = (nt:'b bt)) /\
1045 (bt_map f (node l x r) = node (bt_map f l) (f x) (bt_map f r))
1046End
1047
1048Theorem bt_FST_FDOM:
1049 !cmp t:('a#'b)bt. FDOM (FMAPAL cmp t) = ENUMERAL cmp (bt_map FST t)
1050Proof
1051GEN_TAC THEN Induct THENL
1052[SRW_TAC [] [bt_to_set, bt_to_fmap, bt_map]
1053,P_PGEN_TAC ``x:'a,y:'b`` THEN
1054 SRW_TAC [] [bt_to_set, bt_to_fmap, bt_map, FDOM_DRESTRICT] THEN
1055 REWRITE_TAC [EXTENSION, IN_INTER, IN_UNION] THEN
1056 GEN_TAC THEN CONV_TAC (ONCE_DEPTH_CONV SET_SPEC_CONV) THEN REFL_TAC]
1057QED
1058
1059Theorem bt_fst_lb_FDOM[local]:
1060 !cmp lb t:('a#'b)bt.
1061 FDOM (bt_to_fmap_lb cmp lb t) = bt_to_set_lb cmp lb (bt_map FST t)
1062Proof
1063SRW_TAC [] [bt_to_set_lb, bt_to_fmap_lb, bt_FST_FDOM, FDOM_DRESTRICT]
1064THEN REWRITE_TAC [EXTENSION, IN_INTER] THEN GEN_TAC THEN
1065CONV_TAC (ONCE_DEPTH_CONV SET_SPEC_CONV) THEN REFL_TAC
1066QED
1067
1068Theorem bt_fst_ub_FDOM[local]:
1069 !cmp t:('a#'b)bt ub.
1070 FDOM (bt_to_fmap_ub cmp t ub) = bt_to_set_ub cmp (bt_map FST t) ub
1071Proof
1072SRW_TAC [] [bt_to_set_ub, bt_to_fmap_ub, bt_FST_FDOM, FDOM_DRESTRICT]
1073THEN REWRITE_TAC [EXTENSION, IN_INTER] THEN GEN_TAC THEN
1074CONV_TAC (ONCE_DEPTH_CONV SET_SPEC_CONV) THEN REFL_TAC
1075QED
1076
1077Theorem bt_fst_lb_ub_FDOM[local]:
1078 !cmp lb t:('a#'b)bt ub. FDOM (bt_to_fmap_lb_ub cmp lb t ub) =
1079 bt_to_set_lb_ub cmp lb (bt_map FST t) ub
1080Proof
1081SRW_TAC []
1082 [bt_to_set_lb_ub, bt_to_fmap_lb_ub, bt_FST_FDOM, FDOM_DRESTRICT]
1083THEN REWRITE_TAC [EXTENSION, IN_INTER] THEN GEN_TAC THEN
1084CONV_TAC (ONCE_DEPTH_CONV SET_SPEC_CONV) THEN REFL_TAC
1085QED
1086
1087Theorem IN_lb_ub_imp[local]:
1088 !cmp x lb t:'a bt ub. x IN bt_to_set_lb_ub cmp lb t ub ==>
1089 (apto cmp lb x = LESS) /\ (apto cmp x ub = LESS)
1090Proof
1091SRW_TAC [] [bt_to_set_lb_ub]
1092QED
1093
1094Theorem IN_lb_imp[local]:
1095 !cmp x lb t:'a bt. x IN bt_to_set_lb cmp lb t ==> (apto cmp lb x = LESS)
1096Proof
1097SRW_TAC [] [bt_to_set_lb]
1098QED
1099
1100Theorem IN_ub_imp[local]:
1101 !cmp x t:'a bt ub. x IN bt_to_set_ub cmp t ub ==> (apto cmp x ub = LESS)
1102Proof
1103SRW_TAC [] [bt_to_set_ub]
1104QED
1105
1106Theorem piecewise_FUNION[local]:
1107 !a b c x y z:'a|->'b.(a=x)/\(b=y)/\(c=z)==>
1108 (a FUNION b FUNION c = x FUNION y FUNION z)
1109Proof
1110METIS_TAC []
1111QED
1112
1113Theorem bt_to_fmap_lb_ub_mut_rec[local]:
1114 !cmp lb l x:'a y:'b r ub. bt_to_fmap_lb_ub cmp lb (node l (x,y) r) ub =
1115 if apto cmp lb x = LESS then
1116 if apto cmp x ub = LESS then
1117 bt_to_fmap_lb_ub cmp lb l x FUNION FEMPTY |+ (x,y) FUNION
1118 bt_to_fmap_lb_ub cmp x r ub
1119 else
1120 bt_to_fmap_lb_ub cmp lb l ub
1121 else
1122 bt_to_fmap_lb_ub cmp lb r ub
1123Proof
1124SRW_TAC [] [fmap_EXT, bt_fst_lb_ub_FDOM] THEN
1125SRW_TAC [] [bt_to_fmap_lb_ub, bt_to_set_lb_ub, bt_map] THENL
1126[REWRITE_TAC [EXTENSION, IN_UNION, bt_to_set] THEN GEN_TAC THEN
1127 CONV_TAC (DEPTH_CONV SET_SPEC_CONV) THEN
1128 METIS_TAC [totoLLtrans, IN_SING]
1129,IMP_RES_TAC IN_lb_ub_imp THEN
1130 REWRITE_TAC [bt_to_fmap, FUNION_DRESTRICT, DRESTRICT_DRESTRICT] THEN
1131 AP_THM_TAC THEN AP_TERM_TAC THEN
1132 MATCH_MP_TAC piecewise_FUNION THEN
1133 REPEAT CONJ_TAC THENL
1134 [AP_TERM_TAC THEN REWRITE_TAC [EXTENSION, IN_INTER] THEN GEN_TAC THEN
1135 CONV_TAC (ONCE_DEPTH_CONV SET_SPEC_CONV) THEN METIS_TAC [totoLLtrans]
1136 ,MATCH_MP_TAC DRESTRICT_SING THEN
1137 CONV_TAC SET_SPEC_CONV THEN AR
1138 ,AP_TERM_TAC THEN REWRITE_TAC [EXTENSION, IN_INTER] THEN GEN_TAC THEN
1139 CONV_TAC (ONCE_DEPTH_CONV SET_SPEC_CONV) THEN METIS_TAC [totoLLtrans]
1140 ]
1141,REWRITE_TAC [bt_to_set, EXTENSION, IN_UNION] THEN GEN_TAC THEN
1142 CONV_TAC (DEPTH_CONV SET_SPEC_CONV) THEN EQ_TAC THEN STRIP_TAC THEN AR THEN
1143 METIS_TAC [totoLLtrans, IN_SING, NOT_EQ_LESS_IMP]
1144,IMP_RES_TAC IN_lb_ub_imp THEN
1145 REWRITE_TAC [bt_to_fmap, FUNION_DRESTRICT, DRESTRICT_DRESTRICT] THEN
1146 Q.SUBGOAL_THEN `({z | apto cmp x z = LESS} INTER
1147 {x | (apto cmp lb x = LESS) /\ (apto cmp x ub = LESS)}) = {}` SUBST1_TAC THENL
1148 [REWRITE_TAC [EXTENSION, IN_INTER, NOT_IN_EMPTY] THEN GEN_TAC THEN
1149 CONV_TAC (ONCE_DEPTH_CONV SET_SPEC_CONV) THEN METIS_TAC [totoLLtrans]
1150 ,Q.SUBGOAL_THEN
1151 `x NOTIN {x | (apto cmp lb x = LESS) /\ (apto cmp x ub = LESS)}`
1152 (REWRITE_TAC o ulist o MATCH_MP DRESTRICT_SING_FEMPTY) THENL
1153 [CONV_TAC (RAND_CONV SET_SPEC_CONV) THEN METIS_TAC [totoLLtrans]
1154 ,REWRITE_TAC [DRESTRICT_IS_FEMPTY, FUNION_FEMPTY_2] THEN
1155 Q.SUBGOAL_THEN `{x | (apto cmp lb x = LESS) /\ (apto cmp x ub = LESS)}
1156 SUBSET {y | apto cmp y x = LESS}`
1157 (SUBST1_TAC o REWRITE_RULE [SYM (CONJUNCT2 INTER_SUBSET_EQN)]) THENL
1158 [REWRITE_TAC [SUBSET_DEF] THEN GEN_TAC THEN
1159 CONV_TAC (ONCE_DEPTH_CONV SET_SPEC_CONV) THEN
1160 METIS_TAC [totoLLtrans, NOT_EQ_LESS_IMP]
1161 ,REFL_TAC
1162 ]]]
1163,REWRITE_TAC [bt_to_set, EXTENSION, IN_UNION] THEN GEN_TAC THEN
1164 CONV_TAC (DEPTH_CONV SET_SPEC_CONV) THEN EQ_TAC THEN STRIP_TAC THEN AR THEN
1165 METIS_TAC [totoLLtrans, IN_SING, NOT_EQ_LESS_IMP]
1166,IMP_RES_TAC IN_lb_ub_imp THEN
1167 REWRITE_TAC [bt_to_fmap, FUNION_DRESTRICT, DRESTRICT_DRESTRICT] THEN
1168 Q.SUBGOAL_THEN `({y | apto cmp y x = LESS} INTER
1169 {x | (apto cmp lb x = LESS) /\ (apto cmp x ub = LESS)}) = {}` SUBST1_TAC THENL
1170 [REWRITE_TAC [EXTENSION, IN_INTER, NOT_IN_EMPTY] THEN GEN_TAC THEN
1171 CONV_TAC (ONCE_DEPTH_CONV SET_SPEC_CONV) THEN METIS_TAC [totoLLtrans]
1172 ,Q.SUBGOAL_THEN
1173 `x NOTIN {x | (apto cmp lb x = LESS) /\ (apto cmp x ub = LESS)}`
1174 (REWRITE_TAC o ulist o MATCH_MP DRESTRICT_SING_FEMPTY) THENL
1175 [CONV_TAC (RAND_CONV SET_SPEC_CONV) THEN METIS_TAC [totoLLtrans]
1176 ,REWRITE_TAC [DRESTRICT_IS_FEMPTY, FUNION_FEMPTY_1] THEN
1177 Q.SUBGOAL_THEN `{x | (apto cmp lb x = LESS) /\ (apto cmp x ub = LESS)}
1178 SUBSET {z | apto cmp x z = LESS}`
1179 (SUBST1_TAC o REWRITE_RULE [SYM (CONJUNCT2 INTER_SUBSET_EQN)]) THENL
1180 [REWRITE_TAC [SUBSET_DEF] THEN GEN_TAC THEN
1181 CONV_TAC (ONCE_DEPTH_CONV SET_SPEC_CONV) THEN
1182 METIS_TAC [totoLLtrans, NOT_EQ_LESS_IMP]
1183 ,REFL_TAC
1184 ]]]
1185]
1186QED
1187
1188Theorem bt_to_fmap_lb_mut_rec[local]:
1189 !cmp lb l x:'a y:'b r. bt_to_fmap_lb cmp lb (node l (x,y) r) =
1190 if apto cmp lb x = LESS then
1191 bt_to_fmap_lb_ub cmp lb l x FUNION FEMPTY |+ (x,y) FUNION
1192 bt_to_fmap_lb cmp x r
1193 else
1194 bt_to_fmap_lb cmp lb r
1195Proof
1196SRW_TAC [] [fmap_EXT, bt_fst_lb_ub_FDOM, bt_fst_lb_FDOM] THEN
1197SRW_TAC [] [bt_to_fmap_lb_ub, bt_to_set_lb_ub, bt_map,
1198 bt_to_fmap_lb, bt_to_set_lb] THENL
1199[REWRITE_TAC [EXTENSION, IN_UNION, bt_to_set] THEN GEN_TAC THEN
1200 CONV_TAC (DEPTH_CONV SET_SPEC_CONV) THEN
1201 METIS_TAC [totoLLtrans, IN_SING]
1202,IMP_RES_TAC IN_lb_imp THEN
1203 REWRITE_TAC [bt_to_fmap, FUNION_DRESTRICT, DRESTRICT_DRESTRICT] THEN
1204 AP_THM_TAC THEN AP_TERM_TAC THEN
1205 MATCH_MP_TAC piecewise_FUNION THEN
1206 REPEAT CONJ_TAC THENL
1207 [AP_TERM_TAC THEN REWRITE_TAC [EXTENSION, IN_INTER] THEN GEN_TAC THEN
1208 CONV_TAC (ONCE_DEPTH_CONV SET_SPEC_CONV) THEN METIS_TAC [totoLLtrans]
1209 ,MATCH_MP_TAC DRESTRICT_SING THEN
1210 CONV_TAC SET_SPEC_CONV THEN AR
1211 ,AP_TERM_TAC THEN REWRITE_TAC [EXTENSION, IN_INTER] THEN GEN_TAC THEN
1212 CONV_TAC (ONCE_DEPTH_CONV SET_SPEC_CONV) THEN METIS_TAC [totoLLtrans]
1213 ]
1214,REWRITE_TAC [bt_to_set, EXTENSION, IN_UNION] THEN GEN_TAC THEN
1215 CONV_TAC (DEPTH_CONV SET_SPEC_CONV) THEN EQ_TAC THEN STRIP_TAC THEN AR THEN
1216 METIS_TAC [totoLLtrans, IN_SING, NOT_EQ_LESS_IMP]
1217,IMP_RES_TAC IN_lb_imp THEN
1218 REWRITE_TAC [bt_to_fmap, FUNION_DRESTRICT, DRESTRICT_DRESTRICT] THEN
1219 Q.SUBGOAL_THEN `({y | apto cmp y x = LESS} INTER
1220 {x | (apto cmp lb x = LESS)}) = {}` SUBST1_TAC THENL
1221 [REWRITE_TAC [EXTENSION, IN_INTER, NOT_IN_EMPTY] THEN GEN_TAC THEN
1222 CONV_TAC (ONCE_DEPTH_CONV SET_SPEC_CONV) THEN METIS_TAC [totoLLtrans]
1223 ,Q.SUBGOAL_THEN
1224 `x NOTIN {x | (apto cmp lb x = LESS)}`
1225 (REWRITE_TAC o ulist o MATCH_MP DRESTRICT_SING_FEMPTY) THENL
1226 [CONV_TAC (RAND_CONV SET_SPEC_CONV) THEN METIS_TAC [totoLLtrans]
1227 ,REWRITE_TAC [DRESTRICT_IS_FEMPTY, FUNION_FEMPTY_1] THEN
1228 Q.SUBGOAL_THEN `{x | (apto cmp lb x = LESS)}
1229 SUBSET {z | apto cmp x z = LESS}`
1230 (SUBST1_TAC o REWRITE_RULE [SYM (CONJUNCT2 INTER_SUBSET_EQN)]) THENL
1231 [REWRITE_TAC [SUBSET_DEF] THEN GEN_TAC THEN
1232 CONV_TAC (ONCE_DEPTH_CONV SET_SPEC_CONV) THEN
1233 METIS_TAC [totoLLtrans, NOT_EQ_LESS_IMP]
1234 ,REFL_TAC
1235 ]]]
1236]
1237QED
1238
1239Theorem bt_to_fmap_ub_mut_rec[local]:
1240 !cmp l x:'a y:'b r ub. bt_to_fmap_ub cmp (node l (x,y) r) ub =
1241 if apto cmp x ub = LESS then
1242 bt_to_fmap_ub cmp l x FUNION FEMPTY |+ (x,y) FUNION
1243 bt_to_fmap_lb_ub cmp x r ub
1244 else
1245 bt_to_fmap_ub cmp l ub
1246Proof
1247SRW_TAC [] [fmap_EXT, bt_fst_lb_ub_FDOM, bt_fst_ub_FDOM] THEN
1248SRW_TAC [] [bt_to_fmap_lb_ub, bt_to_set_lb_ub, bt_map,
1249 bt_to_fmap_ub, bt_to_set_ub] THENL
1250[REWRITE_TAC [EXTENSION, IN_UNION, bt_to_set] THEN GEN_TAC THEN
1251 CONV_TAC (DEPTH_CONV SET_SPEC_CONV) THEN
1252 METIS_TAC [totoLLtrans, IN_SING]
1253,IMP_RES_TAC IN_ub_imp THEN
1254 REWRITE_TAC [bt_to_fmap, FUNION_DRESTRICT, DRESTRICT_DRESTRICT] THEN
1255 AP_THM_TAC THEN AP_TERM_TAC THEN
1256 MATCH_MP_TAC piecewise_FUNION THEN
1257 REPEAT CONJ_TAC THENL
1258 [AP_TERM_TAC THEN REWRITE_TAC [EXTENSION, IN_INTER] THEN GEN_TAC THEN
1259 CONV_TAC (ONCE_DEPTH_CONV SET_SPEC_CONV) THEN METIS_TAC [totoLLtrans]
1260 ,MATCH_MP_TAC DRESTRICT_SING THEN
1261 CONV_TAC SET_SPEC_CONV THEN AR
1262 ,AP_TERM_TAC THEN REWRITE_TAC [EXTENSION, IN_INTER] THEN GEN_TAC THEN
1263 CONV_TAC (ONCE_DEPTH_CONV SET_SPEC_CONV) THEN METIS_TAC [totoLLtrans]
1264 ]
1265,REWRITE_TAC [bt_to_set, EXTENSION, IN_UNION] THEN GEN_TAC THEN
1266 CONV_TAC (DEPTH_CONV SET_SPEC_CONV) THEN EQ_TAC THEN STRIP_TAC THEN AR THEN
1267 METIS_TAC [totoLLtrans, IN_SING, NOT_EQ_LESS_IMP]
1268,IMP_RES_TAC IN_ub_imp THEN
1269 REWRITE_TAC [bt_to_fmap, FUNION_DRESTRICT, DRESTRICT_DRESTRICT] THEN
1270 Q.SUBGOAL_THEN `{z | apto cmp x z = LESS} INTER {x | apto cmp x ub = LESS}
1271 = {}` SUBST1_TAC THENL
1272 [REWRITE_TAC [EXTENSION, IN_INTER, NOT_IN_EMPTY] THEN GEN_TAC THEN
1273 CONV_TAC (ONCE_DEPTH_CONV SET_SPEC_CONV) THEN METIS_TAC [totoLLtrans]
1274 ,Q.SUBGOAL_THEN
1275 `x NOTIN {x | (apto cmp x ub = LESS)}`
1276 (REWRITE_TAC o ulist o MATCH_MP DRESTRICT_SING_FEMPTY) THENL
1277 [CONV_TAC (RAND_CONV SET_SPEC_CONV) THEN METIS_TAC [totoLLtrans]
1278 ,REWRITE_TAC [DRESTRICT_IS_FEMPTY, FUNION_FEMPTY_2] THEN
1279 Q.SUBGOAL_THEN `{x | (apto cmp x ub = LESS)}
1280 SUBSET {y | apto cmp y x = LESS}`
1281 (SUBST1_TAC o REWRITE_RULE [SYM (CONJUNCT2 INTER_SUBSET_EQN)]) THENL
1282 [REWRITE_TAC [SUBSET_DEF] THEN GEN_TAC THEN
1283 CONV_TAC (ONCE_DEPTH_CONV SET_SPEC_CONV) THEN
1284 METIS_TAC [totoLLtrans, NOT_EQ_LESS_IMP]
1285 ,REFL_TAC
1286 ]]]
1287]
1288QED
1289
1290(* ******************************************************************* *)
1291(* Continue to imitate enumeralTheory with conversion to ordered lists *)
1292(* As with sets, we supply a general translation, good for any junky *)
1293(* tree. As far as can be foreseen, only the better_bt_to_orl, which *)
1294(* checks by ORL_bt that the tree is ordered and then uses bt_to_list, *)
1295(* will be needed in practice. *)
1296(* ******************************************************************* *)
1297
1298Definition bt_to_orl_lb_ub:
1299 (bt_to_orl_lb_ub (cmp:'a toto) lb nt ub = []) /\
1300 (bt_to_orl_lb_ub cmp lb (node l (x:'a,y:'b) r) ub =
1301 if apto cmp lb x = LESS then
1302 if apto cmp x ub = LESS then
1303 bt_to_orl_lb_ub cmp lb l x ++ [(x,y)] ++ bt_to_orl_lb_ub cmp x r ub
1304 else bt_to_orl_lb_ub cmp lb l ub
1305 else bt_to_orl_lb_ub cmp lb r ub)
1306End
1307
1308Definition bt_to_orl_lb:
1309 (bt_to_orl_lb (cmp:'a toto) lb nt = []) /\
1310 (bt_to_orl_lb cmp lb (node l (x:'a,y:'b) r) =
1311 if apto cmp lb x = LESS then
1312 bt_to_orl_lb_ub cmp lb l x ++ [(x,y)] ++ bt_to_orl_lb cmp x r
1313 else bt_to_orl_lb cmp lb r)
1314End
1315
1316Definition bt_to_orl_ub:
1317 (bt_to_orl_ub (cmp:'a toto) nt ub = []) /\
1318 (bt_to_orl_ub cmp (node l (x:'a,y:'b) r) ub =
1319 if apto cmp x ub = LESS then
1320 bt_to_orl_ub cmp l x ++ [(x,y)] ++ bt_to_orl_lb_ub cmp x r ub
1321 else bt_to_orl_ub cmp l ub)
1322End
1323
1324Definition bt_to_orl:
1325 (bt_to_orl (cmp:'a toto) nt = []) /\
1326 (bt_to_orl cmp (node l (x:'a,y:'b) r) =
1327 bt_to_orl_ub cmp l x ++ [(x,y)] ++ bt_to_orl_lb cmp x r)
1328End
1329
1330(* Analogous to "set" as a constant denoting conversion from 'a list to
1331 'a set, we use "fmap" for conversion from association list to ('a,'b)fmap. *)
1332
1333Definition fmap:
1334 fmap (l:('a#'b)list) = FEMPTY |++ REVERSE l
1335End
1336
1337Theorem FUPDATE_LIST_FUNION[local]:
1338 !f l:('a#'b)list g. g |++ l FUNION f = (g FUNION f) |++ l
1339Proof
1340GEN_TAC THEN Induct THENL
1341[REWRITE_TAC [FUPDATE_LIST_THM]
1342,P_PGEN_TAC ``x:'a,y:'b`` THEN
1343 SRW_TAC [] [FUPDATE_LIST_THM, FUNION_FUPDATE_1]
1344]
1345QED
1346
1347Theorem fmap_rec[local]:
1348 (fmap ([]:('a#'b)list) = FEMPTY) /\
1349 (!h:'a#'b l. fmap (h::l) = fmap l |+ h)
1350Proof
1351CONJ_TAC THEN REWRITE_TAC [fmap, REVERSE_DEF, FUPDATE_LIST_THM] THEN
1352REWRITE_TAC [FUPDATE_LIST_APPEND, FUPDATE_LIST_THM]
1353QED
1354
1355Theorem fmap_NIL[local]:
1356 fmap ([]:('a#'b)list) = FEMPTY
1357Proof
1358REWRITE_TAC [fmap_rec]
1359QED
1360
1361Theorem fmap_UNIT[local]:
1362 !h:'a#'b. fmap [h] = FEMPTY |+ h
1363Proof
1364REWRITE_TAC [fmap_rec]
1365QED
1366
1367Theorem fmap_APPEND[local]:
1368 !m n:('a#'b)list. fmap (m ++ n) = fmap m FUNION fmap n
1369Proof
1370SRW_TAC [] [fmap, FUPDATE_LIST_APPEND, REVERSE_APPEND] THEN
1371REWRITE_TAC [FUPDATE_LIST_FUNION, FUNION_FEMPTY_1]
1372QED
1373
1374(* Show ordered lists represent the right finite maps. *)
1375
1376Theorem orl_fmap_lb_ub[local]:
1377 !cmp t:('a#'b)bt lb ub.
1378 bt_to_fmap_lb_ub cmp lb t ub = fmap (bt_to_orl_lb_ub cmp lb t ub)
1379Proof
1380GEN_TAC THEN Induct THENL
1381[SRW_TAC [] [bt_to_orl_lb_ub, fmap_NIL, bt_to_fmap_lb_ub,
1382 bt_to_fmap, DRESTRICT_FEMPTY]
1383,P_PGEN_TAC ``x:'a,y:'b`` THEN
1384 SRW_TAC [] [bt_to_fmap_lb_ub_mut_rec, bt_to_orl_lb_ub,
1385 fmap_APPEND, fmap_UNIT]
1386]
1387QED
1388
1389Theorem orl_fmap_lb[local]:
1390 !cmp t:('a#'b)bt lb.
1391 bt_to_fmap_lb cmp lb t = fmap (bt_to_orl_lb cmp lb t)
1392Proof
1393GEN_TAC THEN Induct THENL
1394[SRW_TAC [] [bt_to_orl_lb, fmap_NIL, bt_to_fmap_lb,
1395 bt_to_fmap, DRESTRICT_FEMPTY]
1396,P_PGEN_TAC ``x:'a,y:'b`` THEN
1397 SRW_TAC [] [bt_to_fmap_lb_mut_rec, bt_to_orl_lb,
1398 fmap_APPEND, fmap_UNIT, orl_fmap_lb_ub]
1399]
1400QED
1401
1402Theorem orl_fmap_ub[local]:
1403 !cmp t:('a#'b)bt ub.
1404 bt_to_fmap_ub cmp t ub = fmap (bt_to_orl_ub cmp t ub)
1405Proof
1406GEN_TAC THEN Induct THENL
1407[SRW_TAC [] [bt_to_orl_ub, fmap_NIL, bt_to_fmap_ub,
1408 bt_to_fmap, DRESTRICT_FEMPTY]
1409,P_PGEN_TAC ``x:'a,y:'b`` THEN
1410 SRW_TAC [] [bt_to_fmap_ub_mut_rec, bt_to_orl_ub,
1411 fmap_APPEND, fmap_UNIT, orl_fmap_lb_ub]
1412]
1413QED
1414
1415Theorem orl_fmap[local]:
1416 !cmp t:('a#'b)bt. FMAPAL cmp t = fmap (bt_to_orl cmp t)
1417Proof
1418GEN_TAC THEN Induct THENL
1419[SRW_TAC [] [bt_to_orl, fmap_NIL, bt_to_fmap,
1420 bt_to_fmap, DRESTRICT_FEMPTY]
1421,P_PGEN_TAC ``x:'a,y:'b`` THEN
1422 SRW_TAC [] [bt_to_fmap_mut_rec, bt_to_orl, fmap_APPEND,
1423 fmap_UNIT, orl_fmap_lb, orl_fmap_ub]
1424]
1425QED
1426
1427(* But we must prove that results from bt_to_orl etc. satisfy ORL cmp. *)
1428
1429Theorem MEM_MAP_FST_LEM[local]:
1430 !x l:('a#'b)list. MEM x (MAP FST l) <=> ?y. (MEM (x,y) l)
1431Proof
1432GEN_TAC THEN Induct THEN REWRITE_TAC [MAP, MEM] THEN
1433P_PGEN_TAC ``a:'a,b:'b`` THEN REWRITE_TAC [PAIR_EQ] THEN
1434EQ_TAC THEN STRIP_TAC THEN REPEAT GEN_TAC THEN AR THENL
1435[Q.EXISTS_TAC `b` THEN REWRITE_TAC []
1436,RES_TAC THEN Q.EXISTS_TAC `y` THEN AR
1437,DISJ2_TAC THEN Q.EXISTS_TAC `y` THEN AR
1438]
1439QED
1440
1441Theorem ORL_ALT[local]:
1442 (!cmp. ORL cmp ([]:('a#'b)list) = T) /\
1443 (!cmp b a l. ORL cmp ((a:'a,b:'b)::l) <=> ORL cmp l /\
1444 !p. MEM p (MAP FST l) ==> (apto cmp a p = LESS))
1445Proof
1446REWRITE_TAC [ORL, MEM_MAP_FST_LEM] THEN
1447CONV_TAC (ONCE_DEPTH_CONV LEFT_IMP_EXISTS_CONV) THEN
1448REPEAT GEN_TAC THEN REFL_TAC
1449QED
1450
1451Theorem ORL_split_lem[local]:
1452 !cmp l x:'a y:'b r. ORL cmp (l ++ [(x,y)] ++ r) <=>
1453 ORL cmp l /\ (!a. a IN set (MAP FST l) ==> (apto cmp a x = LESS)) /\
1454 ORL cmp r /\ (!z. z IN set (MAP FST r) ==> (apto cmp x z = LESS))
1455Proof
1456GEN_TAC THEN Induct THENL
1457[SRW_TAC [] [ORL_ALT]
1458,P_PGEN_TAC ``p:'a,q:'b`` THEN SRW_TAC [] [ORL_ALT] THEN EQ_TAC THEN
1459 SRW_TAC [] [] THENL
1460 [POP_ASSUM MATCH_MP_TAC THEN REWRITE_TAC []
1461 ,RES_TAC
1462 ,RES_TAC
1463 ,Q.UNDISCH_THEN `!a. (a = p) \/ MEM a (MAP FST l) ==> (apto cmp a p' = LESS)`
1464 MATCH_MP_TAC THEN REWRITE_TAC []
1465 ,MATCH_MP_TAC totoLLtrans THEN Q.EXISTS_TAC `x` THEN CONJ_TAC THENL
1466 [Q.UNDISCH_THEN `!a. (a = p) \/ MEM a (MAP FST l) ==> (apto cmp a x = LESS)`
1467 MATCH_MP_TAC THEN REWRITE_TAC []
1468 ,RES_TAC
1469]]]
1470QED
1471
1472Theorem bt_orl_ol_lb_ub[local]:
1473 !cmp t:('a#'b)bt lb ub. MAP FST (bt_to_orl_lb_ub cmp lb t ub) =
1474 bt_to_ol_lb_ub cmp lb (bt_map FST t) ub
1475Proof
1476GEN_TAC THEN Induct THENL
1477[REWRITE_TAC [bt_to_ol_lb_ub, bt_to_orl_lb_ub, bt_map, MAP]
1478,P_PGEN_TAC ``x:'a,y:'b`` THEN
1479 RW_TAC (srw_ss()) [bt_to_ol_lb_ub, bt_to_orl_lb_ub, bt_map, MAP]
1480]
1481QED
1482
1483Theorem ORL_bt_to_orl_lb_ub[local]:
1484 !cmp t:('a#'b)bt lb ub. ORL cmp (bt_to_orl_lb_ub cmp lb t ub)
1485Proof
1486REWRITE_TAC [ORL_OL_FST, bt_orl_ol_lb_ub, OL_bt_to_ol_lb_ub]
1487QED
1488
1489Theorem bt_orl_ol_lb[local]:
1490 !cmp t:('a#'b)bt lb. MAP FST (bt_to_orl_lb cmp lb t) =
1491 bt_to_ol_lb cmp lb (bt_map FST t)
1492Proof
1493GEN_TAC THEN Induct THENL
1494[REWRITE_TAC [bt_to_ol_lb, bt_to_orl_lb, bt_map, MAP]
1495,P_PGEN_TAC ``x:'a,y:'b`` THEN RW_TAC (srw_ss())
1496 [bt_to_ol_lb, bt_to_orl_lb, bt_orl_ol_lb_ub, bt_map, MAP]
1497]
1498QED
1499
1500Theorem ORL_bt_to_orl_lb[local]:
1501 !cmp t:('a#'b)bt lb. ORL cmp (bt_to_orl_lb cmp lb t)
1502Proof
1503REWRITE_TAC [ORL_OL_FST, bt_orl_ol_lb, OL_bt_to_ol_lb]
1504QED
1505
1506Theorem bt_orl_ol_ub[local]:
1507 !cmp t:('a#'b)bt ub. MAP FST (bt_to_orl_ub cmp t ub) =
1508 bt_to_ol_ub cmp (bt_map FST t) ub
1509Proof
1510GEN_TAC THEN Induct THENL
1511[REWRITE_TAC [bt_to_ol_ub, bt_to_orl_ub, bt_map, MAP]
1512,P_PGEN_TAC ``x:'a,y:'b`` THEN RW_TAC (srw_ss())
1513 [bt_to_ol_ub, bt_to_orl_ub, bt_orl_ol_lb_ub, bt_map, MAP]
1514]
1515QED
1516
1517Theorem ORL_bt_to_orl_ub[local]:
1518 !cmp t:('a#'b)bt ub. ORL cmp (bt_to_orl_ub cmp t ub)
1519Proof
1520REWRITE_TAC [ORL_OL_FST, bt_orl_ol_ub, OL_bt_to_ol_ub]
1521QED
1522
1523Theorem bt_orl_ol[local]:
1524 !cmp t:('a#'b)bt. MAP FST (bt_to_orl cmp t) =
1525 bt_to_ol cmp (bt_map FST t)
1526Proof
1527GEN_TAC THEN Induct THENL
1528[REWRITE_TAC [bt_to_ol, bt_to_orl, bt_map, MAP]
1529,P_PGEN_TAC ``x:'a,y:'b`` THEN RW_TAC (srw_ss())
1530 [bt_to_ol, bt_to_orl, bt_orl_ol_lb, bt_orl_ol_ub, bt_map, MAP]
1531]
1532QED
1533
1534Theorem ORL_bt_to_orl[local]:
1535 !cmp t:('a#'b)bt. ORL cmp (bt_to_orl cmp t)
1536Proof
1537REWRITE_TAC [ORL_OL_FST, bt_orl_ol, OL_bt_to_ol]
1538QED
1539
1540(* Now, still imitating enumeralTheory, to remove the APPENDs. *)
1541
1542Definition bt_to_orl_lb_ub_ac:
1543 (bt_to_orl_lb_ub_ac cmp lb (nt:('a#'b)bt) ub m = m) /\
1544 (bt_to_orl_lb_ub_ac cmp lb (node l (x:'a,y:'b) r) ub m =
1545 if apto cmp lb x = LESS then
1546 if apto cmp x ub = LESS then
1547 bt_to_orl_lb_ub_ac cmp lb l x ((x,y) :: bt_to_orl_lb_ub_ac cmp x r ub m)
1548 else bt_to_orl_lb_ub_ac cmp lb l ub m
1549 else bt_to_orl_lb_ub_ac cmp lb r ub m)
1550End
1551
1552Theorem orl_lb_ub_ac_thm[local]:
1553 !cmp t:('a#'b)bt lb ub m. bt_to_orl_lb_ub_ac cmp lb t ub m =
1554 bt_to_orl_lb_ub cmp lb t ub ++ m
1555Proof
1556GEN_TAC THEN Induct THENL
1557[SRW_TAC [][bt_to_orl_lb_ub, bt_to_orl_lb_ub_ac]
1558,P_PGEN_TAC ``x:'a,y:'b`` THEN
1559 SRW_TAC [][bt_to_orl_lb_ub, bt_to_orl_lb_ub_ac]
1560]
1561QED
1562
1563Definition bt_to_orl_lb_ac:
1564 (bt_to_orl_lb_ac cmp lb (nt:('a#'b)bt) m = m) /\
1565 (bt_to_orl_lb_ac cmp lb (node l (x:'a,y:'b) r) m =
1566 if apto cmp lb x = LESS then
1567 bt_to_orl_lb_ub_ac cmp lb l x ((x,y) :: bt_to_orl_lb_ac cmp x r m)
1568 else bt_to_orl_lb_ac cmp lb r m)
1569End
1570
1571Theorem orl_lb_ac_thm[local]:
1572 !cmp t:('a#'b)bt lb m. bt_to_orl_lb_ac cmp lb t m =
1573 bt_to_orl_lb cmp lb t ++ m
1574Proof
1575GEN_TAC THEN Induct THENL
1576[SRW_TAC [][bt_to_orl_lb, bt_to_orl_lb_ac]
1577,P_PGEN_TAC ``x:'a,y:'b`` THEN
1578 SRW_TAC [][bt_to_orl_lb, bt_to_orl_lb_ac, orl_lb_ub_ac_thm]
1579]
1580QED
1581
1582Definition bt_to_orl_ub_ac:
1583 (bt_to_orl_ub_ac cmp (nt:('a#'b)bt) ub m = m) /\
1584 (bt_to_orl_ub_ac cmp (node l (x:'a,y:'b) r) ub m =
1585 if apto cmp x ub = LESS then
1586 bt_to_orl_ub_ac cmp l x ((x,y) :: bt_to_orl_lb_ub_ac cmp x r ub m)
1587 else bt_to_orl_ub_ac cmp l ub m)
1588End
1589
1590Theorem orl_ub_ac_thm[local]:
1591 !cmp t:('a#'b)bt ub m. bt_to_orl_ub_ac cmp t ub m =
1592 bt_to_orl_ub cmp t ub ++ m
1593Proof
1594GEN_TAC THEN Induct THENL
1595[SRW_TAC [][bt_to_orl_ub, bt_to_orl_ub_ac]
1596,P_PGEN_TAC ``x:'a,y:'b`` THEN
1597 SRW_TAC [][bt_to_orl_ub, bt_to_orl_ub_ac, orl_lb_ub_ac_thm]
1598]
1599QED
1600
1601Definition bt_to_orl_ac:
1602 (bt_to_orl_ac cmp (nt:('a#'b)bt) m = m) /\
1603 (bt_to_orl_ac cmp (node l (x:'a,y:'b) r) m =
1604 bt_to_orl_ub_ac cmp l x ((x,y) :: bt_to_orl_lb_ac cmp x r m))
1605End
1606
1607Theorem orl_ac_thm[local]:
1608 !cmp t:('a#'b)bt m. bt_to_orl_ac cmp t m = bt_to_orl cmp t ++ m
1609Proof
1610GEN_TAC THEN Induct THENL
1611[SRW_TAC [][bt_to_orl, bt_to_orl_ac]
1612,P_PGEN_TAC ``x:'a,y:'b`` THEN
1613 SRW_TAC [][bt_to_orl, bt_to_orl_ac, orl_lb_ac_thm, orl_ub_ac_thm]
1614]
1615QED
1616
1617(* ********* "ORWL" for (fmap) ORdered With List ************ *)
1618
1619Definition ORWL: ORWL cmp (f:'a|->'b) l = (f = fmap l) /\ ORL cmp l
1620End
1621
1622Theorem MEM_IN_DOM_fmap[local]:
1623 !cmp l:('a#'b)list. ORL cmp l ==> (!a b. MEM (a,b) l <=>
1624 a IN FDOM (fmap l) /\ (b = fmap l ' a))
1625Proof
1626GEN_TAC THEN Induct THENL
1627[REWRITE_TAC [FDOM_FEMPTY, fmap_rec, NOT_IN_EMPTY, MEM]
1628,P_PGEN_TAC ``x:'a,y:'b`` THEN
1629 DISCH_THEN (fn orlc =>
1630 STRIP_ASSUME_TAC (MATCH_MP (CONJUNCT1 ORL_NOT_MEM) orlc) THEN
1631 STRIP_ASSUME_TAC (REWRITE_RULE [ORL] orlc)) THEN
1632 SRW_TAC [] [fmap_rec, FAPPLY_FUPDATE_THM, FDOM_FUPDATE] THEN
1633 METIS_TAC []
1634]
1635QED
1636
1637Theorem ORWL_unique[local]:
1638 !cmp f:'a|->'b l m. ORWL cmp f l /\ ORWL cmp f m ==> (l = m)
1639Proof
1640RW_TAC bool_ss [ORWL] THEN
1641Q.SUBGOAL_THEN `ORL cmp l /\ ORL cmp m`
1642 (SUBST1_TAC o SYM o MATCH_MP ORL_MEM_EQ) THEN1 AR THEN
1643P_PGEN_TAC ``a:'a,b:'b`` THEN METIS_TAC [MEM_IN_DOM_fmap]
1644QED
1645
1646Theorem assocv_fmap_thm[local]:
1647 !l:('a#'b)list. assocv l = FLOOKUP (fmap l)
1648Proof
1649Induct THEN CONV_TAC (ONCE_DEPTH_CONV FUN_EQ_CONV) THENL
1650[RW_TAC (srw_ss()) [assocv, FLOOKUP_DEF, fmap_rec, FDOM_FEMPTY]
1651,P_PGEN_TAC ``a:'a,b:'b`` THEN
1652 SRW_TAC [] [assocv, FLOOKUP_DEF, fmap_rec] THENL
1653 [METIS_TAC []
1654 ,METIS_TAC [FAPPLY_FUPDATE_THM]
1655 ,METIS_TAC []
1656]]
1657QED
1658
1659Theorem fmap_ALT[local]:
1660 !l:('a#'b)list. fmap l = unlookup (assocv l)
1661Proof
1662SRW_TAC [] [assocv_fmap_thm, FLOOKUP_unlookup_ID]
1663QED
1664
1665Theorem incr_sort_fmap[local]:
1666 !cmp l:('a#'b)list. fmap (incr_sort cmp l) = fmap l
1667Proof
1668REWRITE_TAC [fmap_ALT, incr_sort_fun]
1669QED
1670
1671Theorem ORWL_bt_to_orl:
1672 !cmp t:('a#'b)bt. ORWL cmp (FMAPAL cmp t) (bt_to_orl cmp t)
1673Proof
1674RW_TAC bool_ss [ORWL, orl_fmap, ORL_bt_to_orl]
1675QED
1676
1677(* We already have the two separate pieces of the above:
1678 ORL_bt_to_orl = |- !cmp t. ORL cmp (bt_to_orl cmp t)
1679 orl_fmap = |- !cmp t. FMAPAL cmp t = fmap (bt_to_orl cmp t) *)
1680
1681Theorem IS_SOME_assocv_rec[local]:
1682 (IS_SOME o assocv ([]:('a#'b)list) = {}) /\
1683 (!a:'a b:'b l. IS_SOME o assocv ((a,b)::l) = a INSERT IS_SOME o assocv l)
1684Proof
1685SRW_TAC [] [assocv, combinTheory.o_THM, EXTENSION, SPECIFICATION] THEN
1686Cases_on `x = a` THEN SRW_TAC [] []
1687QED
1688
1689Theorem FINITE_assocv[local]:
1690 !l:('a#'b)list. FINITE (IS_SOME o assocv l)
1691Proof
1692Induct THENL
1693[REWRITE_TAC [FINITE_EMPTY, IS_SOME_assocv_rec]
1694,P_PGEN_TAC ``x:'a,y:'b`` THEN
1695 ASM_REWRITE_TAC [FINITE_INSERT, IS_SOME_assocv_rec]
1696]
1697QED
1698
1699Theorem assocv_one_to_one[local]:
1700 !cmp l m:('a#'b)list. ORL cmp l /\ ORL cmp m ==>
1701 (assocv l = assocv m) ==> (l = m)
1702Proof
1703REPEAT GEN_TAC THEN
1704DISCH_THEN (fn cj => REWRITE_TAC [SYM (MATCH_MP ORL_MEM_EQ cj)]
1705 THEN STRIP_ASSUME_TAC cj) THEN
1706REPEAT STRIP_TAC THEN
1707Q.SPEC_TAC (`ab`,`ab`) THEN P_PGEN_TAC ``a:'a,b:'b`` THEN
1708IMP_RES_THEN (REWRITE_TAC o ulist o GSYM) assocv_MEM_thm THEN AR
1709QED
1710
1711(* Prove bt_to_orl inverts list_to_bt for ordered lists, using above lemmas. *)
1712
1713Theorem ORL_fmap_EQ[local]:
1714 !cmp l m:('a#'b)list. ORL cmp l /\ ORL cmp m ==>
1715 ((fmap l = fmap m) <=> (l = m))
1716Proof
1717REPEAT GEN_TAC THEN
1718DISCH_THEN (ASSUME_TAC o MATCH_MP assocv_one_to_one) THEN EQ_TAC THENL
1719[REWRITE_TAC [fmap_ALT] THEN METIS_TAC [FINITE_assocv, unlookup_11]
1720,STRIP_TAC THEN AR
1721]
1722QED
1723
1724(* OFU, UFO imitate OU, UO from enumeralTheory respectively *)
1725
1726Definition OFU: OFU cmp (f:'a|->'b) (g:'a|->'b) =
1727 DRESTRICT f {x | LESS_ALL cmp x (FDOM g)} FUNION g
1728End
1729
1730Definition UFO: UFO cmp (f:'a|->'b) (g:'a|->'b) =
1731 f FUNION DRESTRICT g {y | !z. z IN FDOM f ==> (apto cmp z y = LESS)}
1732End
1733
1734Theorem FDOM_OFU[local]:
1735 !cmp (f:'a|->'b) (g:'a|->'b). FDOM (OFU cmp f g) = OU cmp (FDOM f) (FDOM g)
1736Proof
1737RW_TAC (srw_ss())
1738 [OFU, OU, LESS_ALL, FDOM_DRESTRICT, EXTENSION, IN_UNION, IN_INTER]
1739QED
1740
1741Theorem FDOM_UFO[local]:
1742 !cmp (f:'a|->'b) (g:'a|->'b). FDOM (UFO cmp f g) = UO cmp (FDOM f) (FDOM g)
1743Proof
1744RW_TAC (srw_ss())
1745 [UFO, UO, FDOM_DRESTRICT, EXTENSION, IN_UNION, IN_INTER]
1746QED
1747
1748Theorem sing_UFO[local]:
1749 !cmp x:'a y:'b t:'a|->'b. UFO cmp (FEMPTY |+ (x,y)) t =
1750 (FEMPTY |+ (x,y)) FUNION (DRESTRICT t {z | apto cmp x z = LESS})
1751Proof
1752SRW_TAC [] [UFO]
1753QED
1754
1755Theorem bt_to_fmap_OFU_UFO[local]:
1756 !cmp l x:'a y:'b r. FMAPAL cmp (node l (x,y) r) =
1757 OFU cmp (FMAPAL cmp l) (UFO cmp (FEMPTY |+ (x,y)) (FMAPAL cmp r))
1758Proof
1759SRW_TAC [] [OFU, bt_to_fmap, LESS_UO_LEM, FDOM_OFU, FDOM_UFO] THEN
1760REWRITE_TAC [GSYM FUNION_ASSOC] THEN
1761ONCE_REWRITE_TAC [GSYM sing_UFO] THEN AP_THM_TAC THEN AP_TERM_TAC THEN
1762AP_TERM_TAC THEN SRW_TAC [] [UO, LESS_ALL, EXTENSION] THEN
1763METIS_TAC [totoLLtrans]
1764QED
1765
1766Theorem FAPPLY_OFU[local]:
1767 !cmp x u:'a|->'b v:'a|->'b. OFU cmp u v ' x =
1768 if LESS_ALL cmp x (FDOM v) then u ' x else v ' x
1769Proof
1770SRW_TAC [] [OFU, FDOM_OFU, FUNION_DEF, DRESTRICT_DEF] THEN
1771`x NOTIN FDOM u` by METIS_TAC [] THEN
1772`x NOTIN FDOM v` by METIS_TAC [LESS_ALL, all_cpn_distinct, toto_equal_eq] THEN
1773IMP_RES_THEN SUBST1_TAC NOT_FDOM_FAPPLY_FEMPTY THEN REFL_TAC
1774QED
1775
1776Theorem OFU_FEMPTY[local]:
1777 !cmp t:'a|->'b. OFU cmp t FEMPTY = t
1778Proof
1779SRW_TAC [] [fmap_EXT, OU_EMPTY, FDOM_OFU, FAPPLY_OFU, LESS_ALL]
1780QED
1781
1782Theorem FEMPTY_OFU[local]:
1783 !cmp f:'a|->'b. OFU cmp FEMPTY f = f
1784Proof
1785SRW_TAC [] [fmap_EXT, EMPTY_OU, FDOM_OFU, FAPPLY_OFU] THEN
1786`~LESS_ALL cmp x (FDOM f)`
1787 by (SRW_TAC [] [LESS_ALL] THEN
1788 Q.EXISTS_TAC `x` THEN SRW_TAC [] [toto_refl]) THEN
1789AR
1790QED
1791
1792Theorem LESS_ALL_OFU[local]:
1793 !cmp x u:'a|->'b v:'a|->'b. LESS_ALL cmp x (FDOM (OFU cmp u v)) <=>
1794 LESS_ALL cmp x (FDOM u) /\ LESS_ALL cmp x (FDOM v)
1795Proof
1796METIS_TAC [FDOM_OFU, LESS_ALL_OU]
1797QED
1798
1799Theorem OFU_ASSOC[local]:
1800 !cmp f g h:'a|->'b. OFU cmp f (OFU cmp g h) = OFU cmp (OFU cmp f g) h
1801Proof
1802RW_TAC bool_ss [fmap_EXT, FDOM_OFU, OU_ASSOC] THEN
1803RW_TAC bool_ss [FAPPLY_OFU, FUNION_DEF, OFU, LESS_ALL_OFU] THEN METIS_TAC []
1804QED
1805
1806Definition bl_to_fmap:
1807 (bl_to_fmap cmp (nbl:('a#'b)bl) = FEMPTY) /\
1808 (bl_to_fmap cmp (zerbl b) = bl_to_fmap cmp b) /\
1809 (bl_to_fmap cmp (onebl (x,y) t b) =
1810 OFU cmp (FEMPTY |+ (x,y) FUNION
1811 DRESTRICT (FMAPAL cmp t) {z | apto cmp x z = LESS})
1812 (bl_to_fmap cmp b))
1813End
1814
1815Theorem bl_to_fmap_OFU_UFO[local]:
1816 !cmp x:'a y:'b t b. bl_to_fmap cmp (onebl (x,y) t b) =
1817 OFU cmp (UFO cmp (FEMPTY |+ (x,y)) (FMAPAL cmp t)) (bl_to_fmap cmp b)
1818Proof
1819REWRITE_TAC [bl_to_fmap, sing_UFO]
1820QED
1821
1822Theorem bl_rev_fmap_lem[local]:
1823 !cmp b t:('a#'b)bt.
1824 FMAPAL cmp (bl_rev t b) = OFU cmp (FMAPAL cmp t) (bl_to_fmap cmp b)
1825Proof
1826GEN_TAC THEN Induct THEN TRY (GEN_TAC THEN P_PGEN_TAC ``x:'a,y:'b``) THEN
1827SRW_TAC [] [bl_rev, bl_to_fmap_OFU_UFO] THEN
1828REWRITE_TAC [bl_to_fmap, OFU_FEMPTY, bt_to_fmap_OFU_UFO, OFU_ASSOC]
1829QED
1830
1831(* Converting a bl to a bt preserves the represented fmap. *)
1832
1833Theorem bl_to_bt_fmap[local]:
1834 !cmp b:('a#'b)bl. FMAPAL cmp (bl_to_bt b) = bl_to_fmap cmp b
1835Proof
1836REWRITE_TAC [bl_to_bt, bl_rev_fmap_lem, bt_to_fmap, FEMPTY_OFU]
1837QED
1838
1839(* Imitating enumeralTheory as usual, we next aim to show that building a
1840 bl from a list does the same, and to begin with that
1841
1842 LESS_ALL cmp x (FDOM (bl_to_fmap cmp b)) ==>
1843 (bl_to_fmap cmp (BL_CONS (x,y) b) = bl_to_fmap cmp b |+ (x,y),
1844
1845 or generalizing to suit BL_ACCUM, that
1846
1847 LESS_ALL cmp x (FDOM (FMAPAL cmp t)) /\
1848 LESS_ALL cmp x (FDOM (bl_to_fmap cmp b)) ==>
1849 (bl_to_fmap cmp (BL_ACCUM (x,y) t b) =
1850 (OFU cmp (FMAPAL cmp t) (bl_to_fmap cmp b)) |+ (x,y) . *)
1851
1852Theorem LESS_ALL_UFO_LEM[local]:
1853 !cmp x:'a y:'b f. LESS_ALL cmp x (FDOM f) ==>
1854 (UFO cmp (FEMPTY |+ (x,y)) f = f |+ (x,y))
1855Proof
1856SRW_TAC [] [LESS_ALL, UFO, fmap_EXT, FUNION_DEF, DRESTRICT_DEF,
1857 EXTENSION, FAPPLY_FUPDATE_THM] THEN
1858METIS_TAC []
1859QED
1860
1861Theorem LESS_ALL_OFU_UFO_LEM[local]:
1862 !cmp x:'a y:'b f g. LESS_ALL cmp x (FDOM f) /\ LESS_ALL cmp x (FDOM g) ==>
1863(OFU cmp (UFO cmp (FEMPTY |+ (x,y)) f) g = (OFU cmp f g) |+ (x,y))
1864Proof
1865REPEAT STRIP_TAC THEN IMP_RES_THEN (REWRITE_TAC o ulist) LESS_ALL_UFO_LEM THEN
1866SRW_TAC [] [fmap_EXT] THENL
1867[REWRITE_TAC [FDOM_OFU, FDOM_FUPDATE] THEN
1868 IMP_RES_THEN SUBST1_TAC (GSYM LESS_ALL_UO_LEM) THEN
1869 IMP_RES_TAC LESS_ALL_OU_UO_LEM
1870,SRW_TAC [] [FAPPLY_OFU, FAPPLY_FUPDATE_THM] THEN RES_TAC
1871]
1872QED
1873
1874Theorem DRESTRICT_SUPERSET[local]:
1875 !f:'a|->'b s. FDOM f SUBSET s ==> (DRESTRICT f s = f)
1876Proof
1877SRW_TAC [] [DRESTRICT_DEF, SUBSET_DEF, fmap_EXT] THEN
1878METIS_TAC [EXTENSION, IN_INTER]
1879QED
1880
1881Theorem SING_FUNION[local]:
1882 !f x:'a y:'b. FEMPTY |+ (x,y) FUNION f = f |+ (x,y)
1883Proof
1884SRW_TAC []
1885 [fmap_EXT, FUNION_DEF, FAPPLY_FUPDATE_THM, GSYM INSERT_SING_UNION]
1886QED
1887
1888Theorem BL_ACCUM_fmap[local]:
1889 !cmp x:'a y:'b b t. LESS_ALL cmp x (FDOM (FMAPAL cmp t)) /\
1890 LESS_ALL cmp x (FDOM (bl_to_fmap cmp b)) ==>
1891 (bl_to_fmap cmp (BL_ACCUM (x,y) t b) =
1892 OFU cmp (FMAPAL cmp t) (bl_to_fmap cmp b) |+ (x,y))
1893Proof
1894GEN_TAC THEN GEN_TAC THEN GEN_TAC THEN Induct THEN
1895TRY (GEN_TAC THEN P_PGEN_TAC ``p:'a,q:'b``) THEN
1896SRW_TAC [] [BL_ACCUM, bl_to_fmap_OFU_UFO, bt_to_fmap_OFU_UFO] THENL
1897[METIS_TAC [LESS_ALL_UFO_LEM, LESS_ALL_OFU_UFO_LEM, bl_to_fmap]
1898,METIS_TAC [LESS_ALL_UFO_LEM, LESS_ALL_OFU_UFO_LEM, bl_to_fmap]
1899,REWRITE_TAC [bl_to_fmap] THEN
1900 `LESS_ALL cmp x (FDOM (UFO cmp (FEMPTY |+ (p,q)) (FMAPAL cmp b0))) /\
1901 LESS_ALL cmp x (FDOM (bl_to_fmap cmp b))` by
1902 ASM_REWRITE_TAC [GSYM LESS_ALL_OFU] THEN
1903 `LESS_ALL cmp x (FDOM (FMAPAL cmp (node t (p,q) b0)))`
1904 by ASM_REWRITE_TAC [bt_to_fmap_OFU_UFO, LESS_ALL_OFU] THEN
1905 RES_TAC THEN ASM_REWRITE_TAC [bt_to_fmap_OFU_UFO, OFU_ASSOC]
1906]
1907QED
1908
1909Theorem BL_CONS_fmap[local]:
1910 !cmp x:'a y:'b b. LESS_ALL cmp x (FDOM (bl_to_fmap cmp b)) ==>
1911 (bl_to_fmap cmp (BL_CONS (x,y) b) = bl_to_fmap cmp b |+ (x,y))
1912Proof
1913REPEAT STRIP_TAC THEN REWRITE_TAC [BL_CONS] THEN
1914Q.SUBGOAL_THEN `OFU cmp (FMAPAL cmp nt) (bl_to_fmap cmp b) = bl_to_fmap cmp b`
1915(SUBST1_TAC o SYM)
1916THEN1 REWRITE_TAC [bt_to_fmap, FEMPTY_OFU] THEN
1917`LESS_ALL cmp x (FDOM (FMAPAL cmp nt))`
1918by REWRITE_TAC [LESS_ALL, NOT_IN_EMPTY, bt_to_fmap, FDOM_FEMPTY] THEN
1919IMP_RES_TAC BL_ACCUM_fmap THEN AR
1920QED
1921
1922Theorem list_to_bl_fmap[local]:
1923 !cmp l:('a#'b)list. ORL cmp l ==>
1924 (bl_to_fmap cmp (list_to_bl l) = fmap l)
1925Proof
1926GEN_TAC THEN Induct THEN TRY (P_PGEN_TAC ``x:'a, y:'b``) THEN
1927SRW_TAC [] [bl_to_fmap, list_to_bl, fmap_rec, ORL] THEN
1928RES_THEN (SUBST1_TAC o SYM) THEN MATCH_MP_TAC BL_CONS_fmap THEN
1929RES_THEN SUBST1_TAC THEN METIS_TAC [MEM_IN_DOM_fmap, LESS_ALL]
1930QED
1931
1932Theorem bt_to_orl_ID[local]:
1933 !cmp. !l::ORL cmp. bt_to_orl cmp (list_to_bt l) = (l:('a#'b)list)
1934Proof
1935GEN_TAC THEN CONV_TAC RES_FORALL_CONV THEN
1936REWRITE_TAC [SPECIFICATION] THEN GEN_TAC THEN DISCH_TAC THEN
1937Q.SUBGOAL_THEN `ORL cmp (bt_to_orl cmp (list_to_bt l)) /\ ORL cmp l`
1938(REWRITE_TAC o ulist o GSYM o MATCH_MP ORL_fmap_EQ)
1939THEN1 ASM_REWRITE_TAC [ORL_bt_to_orl] THEN
1940IMP_RES_THEN (SUBST1_TAC o SYM) list_to_bl_fmap THEN
1941REWRITE_TAC [GSYM bl_to_bt_fmap, list_to_bt, orl_fmap]
1942QED
1943
1944Theorem bt_to_orl_ID_IMP = REWRITE_RULE
1945 [SPECIFICATION] (CONV_RULE (ONCE_DEPTH_CONV RES_FORALL_CONV) bt_to_orl_ID);
1946
1947(* bt_to_orl_ID_IMP = !cmp l. ORL cmp l ==> (bt_to_orl cmp (list_to_bt l) = l)*)
1948
1949Theorem orl_to_bt_ID[local]:
1950 !cmp t:('a#'b)bt.
1951 FMAPAL cmp (list_to_bt (bt_to_orl cmp t)) = FMAPAL cmp t
1952Proof
1953METIS_TAC [bt_to_orl_ID_IMP, orl_fmap, ORL_bt_to_orl]
1954QED
1955
1956(* ************************************************************************* *)
1957(* *********************** Now to prove merge_fmap ************************* *)
1958(* ************************************************************************* *)
1959
1960Theorem assocv_MEM_MAP_THE[local]:
1961 !x f:'a->'b option l. MEM x l /\ ALL_DISTINCT l /\ IS_SOME (f x) ==>
1962 (assocv (MAP (\x. (x, THE (f x))) l) x = f x)
1963Proof
1964GEN_TAC THEN GEN_TAC THEN Induct THEN
1965REWRITE_TAC [MEM, ALL_DISTINCT, MAP] THEN BETA_TAC THEN
1966REPEAT STRIP_TAC THEN ASM_REWRITE_TAC [assocv] THENL
1967[UNDISCH_TAC (Term`IS_SOME ((f:'a->'b option) x)`) THEN
1968 ASM_REWRITE_TAC [option_CLAUSES]
1969,COND_CASES_TAC THENL
1970 [UNDISCH_TAC (Term`MEM (x:'a) l`) THEN AR
1971 ,RES_TAC]]
1972QED
1973
1974(* ********* merge_smerge not used, but seems hygienic *********** *)
1975
1976Theorem merge_smerge[local]:
1977 !cmp l m:('a#'b)list.
1978 MAP FST (merge cmp l m) = smerge cmp (MAP FST l) (MAP FST m)
1979Proof
1980GEN_TAC THEN Induct THEN TRY (P_PGEN_TAC ``a:'a,b:'b``) THEN
1981SRW_TAC [] [merge_thm] THEN
1982Induct_on `m` THEN TRY (P_PGEN_TAC ``c:'a,d:'b``) THEN
1983Cases_on `apto cmp a c` THEN
1984SRW_TAC [] [smerge, smerge_nil, merge_thm, MAP]
1985QED
1986
1987Theorem IS_SOME_assocv[local]:
1988 !l:('a#'b)list. IS_SOME o (assocv l) = set (MAP FST l)
1989Proof
1990CONV_TAC (QUANT_CONV FUN_EQ_CONV) THEN
1991REWRITE_TAC [combinTheory.o_THM] THEN Induct THENL
1992[SRW_TAC [] [assocv, LIST_TO_SET, combinTheory.C_THM]
1993,P_PGEN_TAC (Term`y:'a,z:'b`) THEN GEN_TAC THEN
1994 ASM_REWRITE_TAC [assocv, LIST_TO_SET_THM, MAP, FST, HD] THEN
1995 CONV_TAC (RAND_CONV (REWR_CONV (GSYM SPECIFICATION))) THEN
1996 REWRITE_TAC [IN_INSERT] THEN Cases_on `x = y` THEN AR THENL
1997 [REWRITE_TAC [option_CLAUSES]
1998 ,REWRITE_TAC [SPECIFICATION]
1999]]
2000QED
2001
2002Theorem FDOM_assocv[local]:
2003 !l:('a#'b)list. FDOM (unlookup (assocv l)) = set (MAP FST l)
2004Proof
2005GEN_TAC THEN
2006MP_TAC (ISPEC ``MAP FST (l:('a#'b)list)`` FINITE_LIST_TO_SET) THEN
2007REWRITE_TAC [GSYM IS_SOME_assocv] THEN
2008MATCH_ACCEPT_TAC unlookup_FDOM
2009QED
2010
2011Theorem fmap_FDOM:
2012 !l:('a#'b)list. FDOM (fmap l) = set (MAP FST l)
2013Proof
2014REWRITE_TAC [fmap, FDOM_FUPDATE_LIST,
2015 LIST_TO_SET_REVERSE, FDOM_FEMPTY, UNION_EMPTY,
2016 rich_listTheory.MAP_REVERSE]
2017QED
2018
2019Theorem FUPDATE_LIST_SNOC[local]:
2020 !l:('a#'b)list fm xy. fm |++ (l ++ [xy]) = (fm |++ l) |+ xy
2021Proof
2022REWRITE_TAC [FUPDATE_LIST_APPEND, FUPDATE_LIST, FOLDL]
2023QED
2024
2025Theorem FINITE_IS_SOME_assocv[local]:
2026 !l:('a#'b)list. FINITE (IS_SOME o assocv l)
2027Proof
2028REWRITE_TAC [IS_SOME_assocv, FINITE_LIST_TO_SET]
2029QED
2030
2031Theorem fmap_ALT[local]:
2032 !l:('a#'b)list. fmap l = unlookup (assocv l)
2033Proof
2034REWRITE_TAC [FUPDATE_ALT, fmap_EXT] THEN GEN_TAC THEN CONJ_TAC THENL
2035[REWRITE_TAC [fmap_FDOM, FDOM_assocv]
2036,GEN_TAC THEN
2037 REWRITE_TAC [fmap_FDOM, fmap, SPECIFICATION] THEN
2038 Induct_on `l` THENL
2039 [REWRITE_TAC [MAP, LIST_TO_SET_THM, rrs NOT_IN_EMPTY]
2040 ,P_PGEN_TAC ``y:'a,v:'b`` THEN
2041 ASSUME_TAC (ISPEC ``(y:'a,v:'b)::l`` FINITE_IS_SOME_assocv) THEN
2042 ASSUME_TAC (SPEC_ALL FINITE_IS_SOME_assocv) THEN
2043 IMP_RES_THEN (ASSUME_TAC o
2044 REWRITE_RULE [IS_SOME_assocv, SPECIFICATION]) FUN_FMAP_DEF THEN
2045 DISCH_THEN (fn ins => MP_TAC ins THEN ASSUME_TAC ins) THEN
2046 REWRITE_TAC [MAP, FST, LIST_TO_SET_THM, rrs IN_INSERT] THEN
2047 REWRITE_TAC [REVERSE_DEF, FUPDATE_LIST_SNOC, unlookup] THEN
2048 Cases_on `x = y` THEN ASM_REWRITE_TAC [FAPPLY_FUPDATE_THM] THENL
2049 [SUBGOAL_THEN ``set (MAP FST ((y:'a,v:'b)::l)) y`` ASSUME_TAC
2050 THEN1 REWRITE_TAC [MAP, FST, LIST_TO_SET_THM, rrs IN_INSERT] THEN
2051 REWRITE_TAC [IS_SOME_assocv] THEN
2052 RES_THEN (REWRITE_TAC o ulist) THEN
2053 REWRITE_TAC [THE_DEF, assocv, combinTheory.o_THM]
2054 ,DISCH_TAC THEN RES_THEN (REWRITE_TAC o ulist) THEN
2055 ASM_REWRITE_TAC [unlookup, IS_SOME_assocv] THEN
2056 RES_THEN (REWRITE_TAC o ulist) THEN
2057 ASM_REWRITE_TAC [combinTheory.o_THM, assocv]
2058]]]
2059QED
2060
2061Theorem merge_fmap[local]:
2062 !cmp l m:('a#'b)list. ORL cmp l /\ ORL cmp m ==>
2063 (fmap (merge cmp l m) = fmap l FUNION fmap m)
2064Proof
2065RW_TAC bool_ss [fmap_ALT] THEN
2066SUBST1_TAC (MATCH_MP unlookup_FUNION (CONJ
2067 (Q.SPEC `l` FINITE_IS_SOME_assocv) (Q.SPEC `m` FINITE_IS_SOME_assocv))) THEN
2068AP_TERM_TAC THEN IMP_RES_TAC merge_fun
2069QED
2070
2071(* *** Summary theorems, with and without restricted quantification: **** *)
2072
2073Theorem ORL_FUNION[local]:
2074 !cmp. !l:('a#'b)list m::ORL cmp. ORL cmp (merge cmp l m) /\
2075 (fmap (merge cmp l m) = fmap l FUNION fmap m)
2076Proof
2077CONV_TAC (DEPTH_CONV RES_FORALL_CONV) THEN
2078SRW_TAC [] [SPECIFICATION, merge_ORL, merge_fmap]
2079QED
2080
2081Theorem ORL_FUNION_IMP = REWRITE_RULE [SPECIFICATION]
2082 (CONV_RULE (DEPTH_CONV RES_FORALL_CONV) ORL_FUNION);
2083
2084(* ORL_FUNION_IMP = |- !cmp l. ORL cmp l ==> !m. ORL cmp m ==>
2085 ORL cmp (merge cmp l m) /\ (fmap (merge cmp l m) = fmap l FUNION fmap m) *)
2086
2087Theorem FMAPAL_FUNION[local]:
2088 !cmp f g:('a#'b)bt.
2089 FMAPAL cmp (list_to_bt (merge cmp (bt_to_orl cmp f) (bt_to_orl cmp g))) =
2090 FMAPAL cmp f FUNION FMAPAL cmp g
2091Proof
2092RW_TAC bool_ss [orl_fmap] THEN
2093`ORL cmp (bt_to_orl cmp f) /\ ORL cmp (bt_to_orl cmp g)`
2094by REWRITE_TAC [ORL_bt_to_orl] THEN
2095`ORL cmp (merge cmp (bt_to_orl cmp f) (bt_to_orl cmp g))`
2096by IMP_RES_TAC merge_ORL THEN
2097IMP_RES_THEN SUBST1_TAC bt_to_orl_ID_IMP THEN
2098IMP_RES_TAC merge_fmap
2099QED
2100
2101(* We really need a merge-like computation rule for DRESTRICT. It might
2102 be that and a logarithmic rule for IN FDOM wd. be enough for now. *)
2103
2104Theorem FMAPAL_FDOM_THM:
2105 (!cmp x:'a. x IN FDOM (FMAPAL cmp (nt:('a#'b)bt)) = F) /\
2106 (!cmp x a:'a b:'b l r. x IN FDOM (FMAPAL cmp (node l (a,b) r)) =
2107 case apto cmp x a of
2108 LESS => x IN FDOM (FMAPAL cmp l)
2109 | EQUAL => T
2110 | GREATER => x IN FDOM (FMAPAL cmp r))
2111Proof
2112SRW_TAC [] [IN_bt_to_set, bt_FST_FDOM, bt_map] THEN
2113Q.SUBGOAL_THEN `(x = a) <=> (apto cmp x a = EQUAL)` SUBST1_TAC
2114THEN1 MATCH_ACCEPT_TAC (GSYM toto_equal_eq) THEN
2115Cases_on `apto cmp x a` THEN
2116SRW_TAC [] [GSYM toto_antisym]
2117QED
2118
2119(* *********************************************************************** *)
2120(* inter_merge, for domain restriction, followed by diff_merge, for *)
2121(* domain restriction to the complement, are shown to implement DRESTRICT. *)
2122(* *********************************************************************** *)
2123
2124Definition inter_merge:
2125 (inter_merge cmp [] [] = []) /\
2126 (inter_merge cmp ((a:'a,b:'b)::l) ([]:'a list) = []) /\
2127 (inter_merge cmp [] (y:'a::m) = []) /\
2128 (inter_merge cmp ((a,b)::l) (y::m) = case apto cmp a y of
2129 LESS => inter_merge cmp l (y::m)
2130 | EQUAL => (a,b) :: inter_merge cmp l m
2131 | GREATER => inter_merge cmp ((a,b)::l) m)
2132End
2133
2134val inter_merge_ind = theorem "inter_merge_ind";
2135
2136(* inter_merge_ind = |- !P.
2137 (!cmp. P cmp [] []) /\ (!cmp a b l. P cmp ((a,b)::l) []) /\
2138 (!cmp y m. P cmp [] (y::m)) /\
2139 (!cmp a b l y m.
2140 ((apto cmp a y = EQUAL) ==> P cmp l m) /\
2141 ((apto cmp a y = GREATER) ==> P cmp ((a,b)::l) m) /\
2142 ((apto cmp a y = LESS) ==> P cmp l (y::m)) ==>
2143 P cmp ((a,b)::l) (y::m)) ==>
2144 !v v1 v2. P v v1 v2 *)
2145
2146Theorem inter_merge_subset_inter[local]:
2147 !cmp:'a toto l:('a#'b)list m.
2148 !x z. MEM (x,z) (inter_merge cmp l m) ==> MEM (x,z) l /\ MEM x m
2149Proof
2150HO_MATCH_MP_TAC inter_merge_ind THEN
2151REPEAT CONJ_TAC THEN REPEAT GEN_TAC THEN
2152REWRITE_TAC [inter_merge, MEM] THEN
2153Cases_on `apto cmp a y` THEN
2154REWRITE_TAC [all_cpn_distinct] THEN
2155STRIP_TAC THEN REPEAT GEN_TAC THEN REWRITE_TAC [cpn_case_def] THENL
2156[METIS_TAC [MEM]
2157,`a = y` by IMP_RES_TAC toto_equal_eq THEN
2158 RW_TAC bool_ss [MEM] THEN DISJ2_TAC THEN RES_TAC
2159,METIS_TAC [MEM]
2160]
2161QED
2162
2163Theorem LESS_NOT_MEM[local]:
2164 !cmp x m y:'a. (apto cmp x y = LESS) /\ OL cmp (y::m) ==> ~MEM x m
2165Proof
2166GEN_TAC THEN GEN_TAC THEN Induct THEN SRW_TAC [] [MEM] THENL
2167[METIS_TAC [OL, MEM, totoLLtrans, toto_glneq]
2168,IMP_RES_TAC OL THEN
2169 `apto cmp x h = LESS` by (MATCH_MP_TAC totoLLtrans THEN
2170 Q.EXISTS_TAC `y` THEN AR THEN
2171 METIS_TAC [OL, MEM]) THEN
2172 RES_TAC
2173]
2174QED
2175
2176Theorem inter_subset_inter_merge[local]:
2177 !cmp:'a toto l:('a#'b)list m. ORL cmp l /\ OL cmp m ==>
2178 !x z. MEM (x,z) l /\ MEM x m ==> MEM (x,z) (inter_merge cmp l m)
2179Proof
2180HO_MATCH_MP_TAC inter_merge_ind THEN
2181REPEAT CONJ_TAC THEN REPEAT GEN_TAC THEN
2182REWRITE_TAC [inter_merge, MEM] THEN
2183Cases_on `apto cmp a y` THEN
2184REWRITE_TAC [all_cpn_distinct, MEM] THEN STRIP_TAC THEN
2185STRIP_TAC THEN REPEAT GEN_TAC THEN REWRITE_TAC [cpn_case_def] THENL
2186[`a <> y` by IMP_RES_TAC toto_glneq THEN ASM_REWRITE_TAC [PAIR_EQ] THEN
2187 IMP_RES_TAC LESS_NOT_MEM THEN
2188 `ORL cmp l` by IMP_RES_TAC ORL THEN METIS_TAC []
2189,`a = y` by IMP_RES_TAC toto_equal_eq THEN ASM_REWRITE_TAC [MEM, PAIR_EQ] THEN
2190 `OL cmp m` by IMP_RES_TAC OL THEN
2191 `ORL cmp l` by IMP_RES_TAC ORL THEN
2192 IMP_RES_TAC ORL_NOT_MEM THEN METIS_TAC []
2193,`a <> y` by IMP_RES_TAC toto_glneq THEN
2194 IMP_RES_TAC LESS_NOT_MEM THEN
2195 `OL cmp m` by IMP_RES_TAC OL THEN
2196 IMP_RES_TAC toto_antisym THEN IMP_RES_TAC ORL_NOT_MEM THEN
2197 `y <> a` by IMP_RES_TAC toto_glneq THEN
2198 REPEAT STRIP_TAC THENL
2199 [METIS_TAC [PAIR_EQ]
2200 ,METIS_TAC []
2201 ,METIS_TAC [MEM, ORL_NOT_MEM]
2202 ,METIS_TAC []
2203]]
2204QED
2205
2206Theorem inter_merge_MEM_thm[local]:
2207 !cmp:'a toto l:('a#'b)list m. ORL cmp l /\ OL cmp m ==>
2208 (!x y. MEM (x,y) (inter_merge cmp l m) <=> MEM (x,y) l /\ MEM x m)
2209Proof
2210REPEAT STRIP_TAC THEN EQ_TAC THENL
2211[MATCH_ACCEPT_TAC inter_merge_subset_inter
2212,IMP_RES_TAC inter_subset_inter_merge THEN STRIP_TAC THEN RES_TAC
2213]
2214QED
2215
2216Theorem FST_inter_merge[local]:
2217 !cmp l:('a#'b)list m. ORL cmp l /\ OL cmp m ==>
2218 (set (MAP FST (inter_merge cmp l m)) = set (MAP FST l) INTER set m)
2219Proof
2220SRW_TAC []
2221 [inter_merge_MEM_thm, EXTENSION, MEM_MAP_FST_LEM] THEN
2222CONV_TAC (LAND_CONV EXISTS_AND_CONV) THEN REFL_TAC
2223QED
2224
2225Theorem inter_merge_ORL[local]:
2226 !cmp l:('a#'b)list m. ORL cmp l /\ OL cmp m ==>
2227 ORL cmp (inter_merge cmp l m)
2228Proof
2229GEN_TAC THEN Induct THEN TRY (P_PGEN_TAC ``x:'a,y:'b``) THEN Induct THEN
2230SRW_TAC [] [inter_merge] THEN REWRITE_TAC [ORL] THEN
2231IMP_RES_TAC ORL THEN IMP_RES_TAC OL THEN
2232Cases_on `apto cmp x h` THEN SRW_TAC [] [] THEN
2233RW_TAC bool_ss [ORL] THEN IMP_RES_TAC inter_merge_subset_inter THEN RES_TAC
2234QED
2235
2236Theorem IN_IS_SOME_NOT_NONE[local]:
2237 !x f:'a->'b option. (f x = NONE) ==> ~(x IN IS_SOME o f)
2238Proof
2239REWRITE_TAC [SPECIFICATION, combinTheory.o_THM] THEN
2240METIS_TAC [option_CLAUSES]
2241QED
2242
2243Theorem inter_merge_fmap[local]:
2244 !cmp l:('a#'b)list m. ORL cmp l /\ OL cmp m ==>
2245 (fmap (inter_merge cmp l m) = DRESTRICT (fmap l) (set m))
2246Proof
2247RW_TAC bool_ss
2248 [fmap_ALT, fmap_EXT, FDOM_assocv, DRESTRICT_DEF, FST_inter_merge] THEN
2249REWRITE_TAC [unlookup] THEN
2250`x IN set (MAP FST (inter_merge cmp l m))`
2251 by (IMP_RES_TAC FST_inter_merge THEN AR) THEN
2252`x IN set (MAP FST l)` by IMP_RES_TAC IN_INTER THEN
2253`x IN IS_SOME o assocv (inter_merge cmp l m) /\ x IN IS_SOME o assocv l`
2254 by ASM_REWRITE_TAC [IS_SOME_assocv] THEN
2255`FINITE (IS_SOME o assocv (inter_merge cmp l m)) /\ FINITE (IS_SOME o assocv l)`
2256 by REWRITE_TAC [FINITE_IS_SOME_assocv] THEN
2257IMP_RES_TAC FUN_FMAP_DEF THEN ASM_REWRITE_TAC [combinTheory.o_THM] THEN
2258AP_TERM_TAC THEN
2259STRIP_ASSUME_TAC (ISPEC ``assocv (l:('a#'b)list) x`` option_nchotomy) THENL
2260[METIS_TAC [IN_IS_SOME_NOT_NONE]
2261,AR THEN
2262 Q.SUBGOAL_THEN `ORL cmp (inter_merge cmp l m)`
2263 (REWRITE_TAC o ulist o MATCH_MP assocv_MEM_thm)
2264 THEN1 IMP_RES_TAC inter_merge_ORL THEN
2265 REWRITE_TAC [MATCH_MP inter_merge_MEM_thm
2266 (CONJ (Q.ASSUME `ORL cmp l`) (Q.ASSUME `OL cmp m`))] THEN
2267 CONJ_TAC THENL
2268 [METIS_TAC [assocv_MEM_thm]
2269 ,METIS_TAC [IN_INTER]
2270]]
2271QED
2272
2273(* *** Summary theorems, with and without restricted quantification: **** *)
2274
2275Theorem ORL_DRESTRICT[local]:
2276 !cmp. !l:('a#'b)list::ORL cmp. !m::OL cmp. ORL cmp (inter_merge cmp l m) /\
2277 (fmap (inter_merge cmp l m) = DRESTRICT (fmap l) (set m))
2278Proof
2279CONV_TAC (DEPTH_CONV RES_FORALL_CONV) THEN
2280SRW_TAC [] [SPECIFICATION, inter_merge_ORL, inter_merge_fmap]
2281QED
2282
2283Theorem ORL_DRESTRICT_IMP =
2284REWRITE_RULE [SPECIFICATION]
2285 (CONV_RULE (DEPTH_CONV RES_FORALL_CONV) ORL_DRESTRICT);
2286
2287(* ORL_DRESTRICT_IMP = |- !cmp l. ORL cmp l ==> !m. OL cmp m ==>
2288 ORL cmp (inter_merge cmp l m) /\
2289 (fmap (inter_merge cmp l m) = DRESTRICT (fmap l) (set m)) *)
2290
2291Theorem FMAPAL_DRESTRICT[local]:
2292 !cmp f:('a#'b)bt s:'a bt.
2293 FMAPAL cmp (list_to_bt (inter_merge cmp (bt_to_orl cmp f) (bt_to_ol cmp s))) =
2294 DRESTRICT (FMAPAL cmp f) (ENUMERAL cmp s)
2295Proof
2296RW_TAC bool_ss [orl_fmap, ol_set] THEN
2297`ORL cmp (bt_to_orl cmp f) /\ OL cmp (bt_to_ol cmp s)`
2298by REWRITE_TAC [ORL_bt_to_orl, OL_bt_to_ol] THEN
2299`ORL cmp (inter_merge cmp (bt_to_orl cmp f) (bt_to_ol cmp s))`
2300by IMP_RES_TAC inter_merge_ORL THEN
2301IMP_RES_THEN SUBST1_TAC bt_to_orl_ID_IMP THEN
2302IMP_RES_TAC inter_merge_fmap
2303QED
2304
2305(* ********* Do the corresponding stuff for diff_merge ******* *)
2306
2307Definition diff_merge:
2308 (diff_merge cmp [] [] = []) /\
2309 (diff_merge cmp ((a:'a,b:'b)::l) ([]:'a list) = (a,b)::l) /\
2310 (diff_merge cmp [] (y:'a::m) = []) /\
2311 (diff_merge cmp ((a,b)::l) (y::m) = case apto cmp a y of
2312 LESS => (a,b) :: diff_merge cmp l (y::m)
2313 | EQUAL => diff_merge cmp l m
2314 | GREATER => diff_merge cmp ((a,b)::l) m)
2315End
2316
2317val diff_merge_ind = theorem "diff_merge_ind";
2318
2319(* diff_merge_ind = |- !P.
2320 (!cmp. P cmp [] []) /\ (!cmp a b l. P cmp ((a,b)::l) []) /\
2321 (!cmp y m. P cmp [] (y::m)) /\
2322 (!cmp a b l y m.
2323 ((apto cmp a y = EQUAL) ==> P cmp l m) /\
2324 ((apto cmp a y = GREATER) ==> P cmp ((a,b)::l) m) /\
2325 ((apto cmp a y = LESS) ==> P cmp l (y::m)) ==>
2326 P cmp ((a,b)::l) (y::m)) ==>
2327 !v v1 v2. P v v1 v2 *)
2328
2329Theorem inter_subset_diff_merge[local]:
2330 !cmp:'a toto l:('a#'b)list m.
2331 !x z. MEM (x,z) l /\ ~MEM x m ==> MEM (x,z) (diff_merge cmp l m)
2332Proof
2333HO_MATCH_MP_TAC diff_merge_ind THEN
2334REPEAT CONJ_TAC THEN REPEAT GEN_TAC THEN
2335REWRITE_TAC [diff_merge, MEM] THEN
2336Cases_on `apto cmp a y` THEN
2337REWRITE_TAC [all_cpn_distinct] THEN
2338STRIP_TAC THEN REPEAT GEN_TAC THEN ASM_REWRITE_TAC [cpn_case_def] THENL
2339[METIS_TAC [MEM]
2340,`a = y` by IMP_RES_TAC toto_equal_eq THEN
2341 RW_TAC bool_ss [MEM] THEN RES_TAC
2342,METIS_TAC [MEM]
2343]
2344QED
2345
2346Theorem diff_merge_subset_inter[local]:
2347 !cmp:'a toto l:('a#'b)list m. ORL cmp l /\ OL cmp m ==>
2348 !x z. MEM (x,z) (diff_merge cmp l m) ==> MEM (x,z) l /\ ~MEM x m
2349Proof
2350HO_MATCH_MP_TAC diff_merge_ind THEN
2351REPEAT CONJ_TAC THEN REPEAT GEN_TAC THEN
2352REWRITE_TAC [diff_merge, MEM] THEN
2353Cases_on `apto cmp a y` THEN
2354REWRITE_TAC [all_cpn_distinct, MEM] THEN STRIP_TAC THEN
2355STRIP_TAC THEN REPEAT GEN_TAC THEN REWRITE_TAC [cpn_case_def] THENL
2356[`a <> y` by IMP_RES_TAC toto_glneq THEN
2357 IMP_RES_TAC LESS_NOT_MEM THEN
2358 `OL cmp m` by IMP_RES_TAC OL THEN
2359 IMP_RES_TAC ORL_NOT_MEM THEN
2360 IMP_RES_TAC toto_antisym THEN `y <> a` by IMP_RES_TAC toto_glneq THEN
2361 IMP_RES_TAC ORL THEN
2362 REPEAT STRIP_TAC THENL
2363 [IMP_RES_TAC MEM THENL
2364 [ASM_REWRITE_TAC [GSYM PAIR_EQ]
2365 ,DISJ2_TAC THEN RES_TAC
2366 ]
2367 ,METIS_TAC [MEM]
2368 ,METIS_TAC [MEM, PAIR_EQ]
2369 ]
2370,`a = y` by IMP_RES_TAC toto_equal_eq THEN ASM_REWRITE_TAC [MEM, PAIR_EQ] THEN
2371 `OL cmp m` by IMP_RES_TAC OL THEN
2372 `ORL cmp l` by IMP_RES_TAC ORL THEN
2373 IMP_RES_TAC ORL_NOT_MEM THEN METIS_TAC []
2374,`a <> y` by IMP_RES_TAC toto_glneq THEN ASM_REWRITE_TAC [PAIR_EQ] THEN
2375 IMP_RES_TAC toto_antisym THEN IMP_RES_TAC LESS_NOT_MEM THEN
2376 `OL cmp m` by IMP_RES_TAC OL THEN
2377 METIS_TAC [MEM, PAIR_EQ, ORL_NOT_MEM]
2378]
2379QED
2380
2381Theorem diff_merge_MEM_thm[local]:
2382 !cmp:'a toto l:('a#'b)list m. ORL cmp l /\ OL cmp m ==>
2383 (!x y. MEM (x,y) (diff_merge cmp l m) <=> MEM (x,y) l /\ ~MEM x m)
2384Proof
2385REPEAT STRIP_TAC THEN EQ_TAC THENL
2386[STRIP_TAC THEN IMP_RES_TAC diff_merge_subset_inter THEN AR
2387,MATCH_ACCEPT_TAC inter_subset_diff_merge
2388]
2389QED
2390
2391Theorem FST_diff_merge[local]:
2392 !cmp l:('a#'b)list m. ORL cmp l /\ OL cmp m ==>
2393 (set (MAP FST (diff_merge cmp l m)) = set (MAP FST l) DIFF set m)
2394Proof
2395SRW_TAC []
2396 [diff_merge_MEM_thm, EXTENSION, MEM_MAP_FST_LEM] THEN
2397CONV_TAC (LAND_CONV EXISTS_AND_CONV) THEN REFL_TAC
2398QED
2399
2400Theorem diff_merge_ORL[local]:
2401 !cmp l:('a#'b)list m. ORL cmp l /\ OL cmp m ==>
2402 ORL cmp (diff_merge cmp l m)
2403Proof
2404GEN_TAC THEN Induct THEN TRY (P_PGEN_TAC ``x:'a,y:'b``) THEN Induct THEN
2405SRW_TAC [] [diff_merge] THEN REWRITE_TAC [ORL] THEN
2406IMP_RES_TAC ORL THEN IMP_RES_TAC OL THEN
2407Cases_on `apto cmp x h` THEN SRW_TAC [] [] THEN
2408RW_TAC bool_ss [ORL] THEN IMP_RES_TAC diff_merge_subset_inter THEN RES_TAC
2409QED
2410
2411Theorem INTER_OVER_DIFF[local]:
2412 !a b c:'a set. a INTER (b DIFF c) = a INTER b DIFF a INTER c
2413Proof
2414RW_TAC bool_ss [EXTENSION, IN_INTER, IN_DIFF] THEN tautLib.TAUT_TAC
2415QED
2416
2417Theorem INTER_COMPL_DIFF[local]:
2418 !a b:'a set. a INTER (COMPL b) = a DIFF b
2419Proof
2420RW_TAC bool_ss [EXTENSION, IN_INTER, IN_DIFF, IN_COMPL]
2421QED
2422
2423Theorem diff_merge_fmap[local]:
2424 !cmp l:('a#'b)list m. ORL cmp l /\ OL cmp m ==>
2425 (fmap (diff_merge cmp l m) = DRESTRICT (fmap l) (COMPL (set m)))
2426Proof
2427RW_TAC bool_ss [fmap_ALT, fmap_EXT, FDOM_assocv, DRESTRICT_DEF,
2428 FST_diff_merge, INTER_COMPL_DIFF] THEN
2429REWRITE_TAC [unlookup] THEN
2430`x IN set (MAP FST (diff_merge cmp l m))`
2431 by (IMP_RES_TAC FST_diff_merge THEN AR) THEN
2432`x IN set (MAP FST l)` by IMP_RES_TAC IN_DIFF THEN
2433`x IN IS_SOME o assocv (diff_merge cmp l m) /\ x IN IS_SOME o assocv l`
2434 by ASM_REWRITE_TAC [IS_SOME_assocv] THEN
2435`FINITE (IS_SOME o assocv (diff_merge cmp l m)) /\ FINITE (IS_SOME o assocv l)`
2436 by REWRITE_TAC [FINITE_IS_SOME_assocv] THEN
2437IMP_RES_TAC FUN_FMAP_DEF THEN ASM_REWRITE_TAC [combinTheory.o_THM] THEN
2438AP_TERM_TAC THEN
2439STRIP_ASSUME_TAC (ISPEC ``assocv (l:('a#'b)list) x`` option_nchotomy) THENL
2440[METIS_TAC [IN_IS_SOME_NOT_NONE]
2441,AR THEN
2442 Q.SUBGOAL_THEN `ORL cmp (diff_merge cmp l m)`
2443 (REWRITE_TAC o ulist o MATCH_MP assocv_MEM_thm)
2444 THEN1 IMP_RES_TAC diff_merge_ORL THEN
2445 REWRITE_TAC [MATCH_MP diff_merge_MEM_thm
2446 (CONJ (Q.ASSUME `ORL cmp l`) (Q.ASSUME `OL cmp m`))] THEN
2447 CONJ_TAC THENL
2448 [METIS_TAC [assocv_MEM_thm]
2449 ,METIS_TAC [IN_DIFF]
2450]]
2451QED
2452
2453(* *** Summary theorems, with and without restricted quantification: **** *)
2454
2455Theorem ORL_DRESTRICT_COMPL[local]:
2456 !cmp. !l:('a#'b)list::ORL cmp. !m::OL cmp. ORL cmp (diff_merge cmp l m) /\
2457(fmap (diff_merge cmp l m) = DRESTRICT (fmap l) (COMPL (set m)))
2458Proof
2459CONV_TAC (DEPTH_CONV RES_FORALL_CONV) THEN
2460SRW_TAC [] [SPECIFICATION, diff_merge_ORL, diff_merge_fmap]
2461QED
2462
2463Theorem ORL_DRESTRICT_COMPL_IMP =
2464REWRITE_RULE [SPECIFICATION]
2465 (CONV_RULE (DEPTH_CONV RES_FORALL_CONV) ORL_DRESTRICT_COMPL);
2466
2467(* ORL_DRESTRICT_COMPL_IMP = |- !cmp l. ORL cmp l ==> !m. OL cmp m ==>
2468 ORL cmp (diff_merge cmp l m) /\
2469 (fmap (diff_merge cmp l m) = DRESTRICT (fmap l) (COMPL (set m))) *)
2470
2471Theorem FMAPAL_DRESTRICT_COMPL[local]:
2472 !cmp f:('a#'b)bt s:'a bt.
2473FMAPAL cmp (list_to_bt (diff_merge cmp (bt_to_orl cmp f) (bt_to_ol cmp s))) =
2474DRESTRICT (FMAPAL cmp f) (COMPL (ENUMERAL cmp s))
2475Proof
2476RW_TAC bool_ss [orl_fmap, ol_set] THEN
2477`ORL cmp (bt_to_orl cmp f) /\ OL cmp (bt_to_ol cmp s)`
2478by REWRITE_TAC [ORL_bt_to_orl, OL_bt_to_ol] THEN
2479`ORL cmp (diff_merge cmp (bt_to_orl cmp f) (bt_to_ol cmp s))`
2480by IMP_RES_TAC diff_merge_ORL THEN
2481IMP_RES_THEN SUBST1_TAC bt_to_orl_ID_IMP THEN
2482IMP_RES_TAC diff_merge_fmap
2483QED
2484
2485(* ********************************************************************* *)
2486(* Theorems to assist conversions *)
2487(* ********************************************************************* *)
2488
2489Theorem FMAPAL_fmap:
2490 !cmp l:('a#'b)list. fmap l = FMAPAL cmp (list_to_bt (incr_sort cmp l))
2491Proof
2492REPEAT GEN_TAC THEN CONV_TAC (LAND_CONV (REWR_CONV (GSYM incr_sort_fmap))) THEN
2493Q.SUBGOAL_THEN
2494`incr_sort cmp l = bt_to_orl cmp (list_to_bt (incr_sort cmp l))`
2495SUBST1_TAC THENL
2496[MATCH_MP_TAC (GSYM bt_to_orl_ID_IMP) THEN MATCH_ACCEPT_TAC incr_sort_ORL
2497,REWRITE_TAC [orl_to_bt_ID, orl_fmap]
2498]
2499QED
2500
2501Theorem ORL_FMAPAL:
2502 !cmp l:('a#'b)list. ORL cmp l ==> (fmap l = FMAPAL cmp (list_to_bt l))
2503Proof
2504REPEAT STRIP_TAC THEN
2505Q.SUBGOAL_THEN
2506`l = bt_to_orl cmp (list_to_bt l)` SUBST1_TAC THENL
2507[MATCH_MP_TAC (GSYM bt_to_orl_ID_IMP) THEN AR
2508,REWRITE_TAC [orl_to_bt_ID, orl_fmap]
2509]
2510QED
2511
2512Theorem bt_to_orl_thm[local]:
2513 !cmp t:('a#'b)bt. bt_to_orl cmp t = bt_to_orl_ac cmp t []
2514Proof
2515SRW_TAC [] [orl_ac_thm]
2516QED
2517
2518Theorem ORWL_FUNION_THM: !cmp s:'a|->'b l t m.
2519 ORWL cmp s l /\ ORWL cmp t m ==> ORWL cmp (s FUNION t) (merge cmp l m)
2520Proof
2521METIS_TAC [ORWL, ORL_FUNION_IMP]
2522QED
2523
2524Theorem ORWL_DRESTRICT_THM: !cmp s:'a|->'b l t m.
2525ORWL cmp s l /\ OWL cmp t m ==> ORWL cmp (DRESTRICT s t)(inter_merge cmp l m)
2526Proof
2527METIS_TAC [OWL, ORWL, ORL_DRESTRICT_IMP]
2528QED
2529
2530Theorem ORWL_DRESTRICT_COMPL_THM:
2531 !cmp s:'a|->'b l t m. ORWL cmp s l /\ OWL cmp t m ==>
2532 ORWL cmp (DRESTRICT s (COMPL t)) (diff_merge cmp l m)
2533Proof
2534METIS_TAC [OWL, ORWL, ORL_DRESTRICT_COMPL_IMP]
2535QED
2536
2537Theorem bt_map_ACTION[local]:
2538 !f:'b->'c g:'a->'b t:'a bt. bt_map f (bt_map g t) = bt_map (f o g) t
2539Proof
2540GEN_TAC THEN GEN_TAC THEN Induct THEN SRW_TAC [] [bt_map]
2541QED
2542
2543(* The following may be useful for o_f_CONV, and more so for tc_CONV. *)
2544
2545Definition AP_SND: AP_SND (f:'b->'c) (a:'a,b:'b) = (a, f b)
2546End
2547
2548Theorem FST_two_ways[local]:
2549 !f:'b->'c. FST o AP_SND f = (FST:'a#'b->'a)
2550Proof
2551GEN_TAC THEN CONV_TAC FUN_EQ_CONV THEN
2552P_PGEN_TAC ``a:'a,b:'b`` THEN SRW_TAC [] [combinTheory.o_THM, AP_SND]
2553QED
2554
2555Theorem o_f_bt_map:
2556 !cmp f:'b -> 'c t:('a#'b)bt.
2557 f o_f FMAPAL cmp t = FMAPAL cmp (bt_map (AP_SND f) t)
2558Proof
2559REPEAT GEN_TAC THEN REWRITE_TAC [fmap_EXT, FDOM_o_f] THEN CONJ_TAC THENL
2560[REWRITE_TAC [bt_FST_FDOM, bt_map_ACTION, FST_two_ways]
2561,GEN_TAC THEN ONCE_REWRITE_TAC [EQ_SYM_EQ] THEN
2562 Induct_on `t` THENL
2563 [REWRITE_TAC [bt_FST_FDOM, bt_to_set, bt_map, NOT_IN_EMPTY]
2564 ,P_PGEN_TAC ``a:'a,b:'b`` THEN
2565 DISCH_THEN (fn infd => ASSUME_TAC infd THEN
2566 IMP_RES_THEN (REWRITE_TAC o ulist)
2567 (REWRITE_RULE [GSYM o_f_FDOM] o_f_DEF) THEN
2568 MP_TAC (REWRITE_RULE [FMAPAL_FDOM_THM] infd)) THEN
2569 REWRITE_TAC [bt_map, AP_SND, FAPPLY_node] THEN
2570 Cases_on `apto cmp x a` THEN SRW_TAC [] []
2571]]
2572QED
2573
2574(* **** following is for INSERT - {} sets, adapted to fmap etc. **** *)
2575
2576Theorem FAPPLY_fmap_NIL:
2577 !x:'a. fmap ([]:('a#'b)list) ' x = FEMPTY ' x
2578Proof
2579SRW_TAC [] [fmap, FUPDATE_LIST_THM]
2580QED
2581
2582Theorem FAPPLY_fmap_CONS:
2583 !x y:'a z:'b l. fmap ((y,z)::l) ' x =
2584 if x = y then z else fmap l ' x
2585Proof
2586SRW_TAC [] [fmap, FUPDATE_LIST_SNOC, FAPPLY_FUPDATE_THM]
2587QED
2588
2589Theorem fmap_CONS[local]:
2590 !x:'a y:'b l. fmap ((x,y)::l) = fmap l |+ (x,y)
2591Proof
2592SRW_TAC [] [fmap, FUPDATE_LIST_SNOC, FAPPLY_FUPDATE_THM]
2593QED
2594
2595Theorem o_f_FUPDATE_ALT[local]:
2596 !f:'b->'c fm:'a|->'b k v. f o_f (fm |+ (k,v)) = (f o_f fm) |+ (k,f v)
2597Proof
2598REPEAT GEN_TAC THEN
2599REWRITE_TAC [fmap_EXT, FDOM_o_f, FDOM_FUPDATE] THEN
2600GEN_TAC THEN REWRITE_TAC [IN_INSERT, FAPPLY_FUPDATE_THM, o_f_FAPPLY] THEN
2601ASM_REWRITE_TAC [o_f_FUPDATE, FAPPLY_FUPDATE_THM] THEN
2602Cases_on `x = k` THEN STRIP_TAC THEN ASM_REWRITE_TAC [] THEN
2603`x IN FDOM (fm \\ k)` by METIS_TAC [FDOM_DOMSUB, IN_DELETE] THEN
2604IMP_RES_TAC o_f_FAPPLY THEN ASM_REWRITE_TAC [DOMSUB_FAPPLY_THM] THEN
2605`k <> x` by METIS_TAC [] THEN AR
2606QED
2607
2608Theorem o_f_fmap:
2609 !f:'b->'c l:('a#'b)list. f o_f fmap l = fmap (MAP (AP_SND f) l)
2610Proof
2611GEN_TAC THEN Induct THENL
2612[SRW_TAC [] [fmap, FUPDATE_LIST_THM]
2613,P_PGEN_TAC ``y:'a, z:'b`` THEN
2614 RW_TAC bool_ss [MAP, fmap_CONS, AP_SND, o_f_FUPDATE_ALT]
2615]
2616QED
2617
2618(* ******************************************************************* *)
2619(* Test for a bt with no spurious nodes, as should be invariably the *)
2620(* case, and justify quicker bt_to_orl for bt's passing the test, *)
2621(* makes exactly n - 1 comparisons in passing a tree with n nodes. *)
2622(* (A carbon copy of what is done with bt_to_ol in enumeralTheory.) *)
2623(* ******************************************************************* *)
2624
2625Definition ORL_bt_lb_ub:
2626 (ORL_bt_lb_ub cmp lb (nt:('a#'b) bt) ub = (apto cmp lb ub = LESS)) /\
2627 (ORL_bt_lb_ub cmp lb (node l (x,y) r) ub = ORL_bt_lb_ub cmp lb l x /\
2628 ORL_bt_lb_ub cmp x r ub)
2629End
2630
2631Definition ORL_bt_lb:
2632 (ORL_bt_lb cmp lb (nt:('a#'b) bt) = T) /\
2633 (ORL_bt_lb cmp lb (node l (x,y) r) = ORL_bt_lb_ub cmp lb l x /\
2634 ORL_bt_lb cmp x r)
2635End
2636
2637Definition ORL_bt_ub:
2638 (ORL_bt_ub cmp (nt:('a#'b) bt) ub = T) /\
2639 (ORL_bt_ub cmp (node l (x,y) r) ub = ORL_bt_ub cmp l x /\
2640 ORL_bt_lb_ub cmp x r ub)
2641End
2642
2643Definition ORL_bt:
2644 (ORL_bt cmp (nt:('a#'b) bt) = T) /\
2645 (ORL_bt cmp (node l (x,y) r) = ORL_bt_ub cmp l x /\ ORL_bt_lb cmp x r)
2646End
2647
2648Theorem ORL_bt_lb_ub_lem[local]:
2649 !cmp t lb ub. ORL_bt_lb_ub cmp lb t ub ==> (apto cmp lb ub = LESS)
2650Proof
2651GEN_TAC THEN Induct THENL
2652[SRW_TAC [] [ORL_bt_lb_ub]
2653,P_PGEN_TAC ``x:'a,y:'b`` THEN
2654 SRW_TAC [] [ORL_bt_lb_ub] THEN METIS_TAC [totoLLtrans]
2655]
2656QED
2657
2658Theorem ORL_bt_lb_ub_thm[local]:
2659 !cmp t:('a#'b) bt lb ub. ORL_bt_lb_ub cmp lb t ub ==>
2660 (bt_to_orl_lb_ub cmp lb t ub = bt_to_list t)
2661Proof
2662GEN_TAC THEN Induct THENL
2663[REWRITE_TAC [bt_to_orl_lb_ub, bt_to_list]
2664,P_PGEN_TAC ``a:'a,b:'b`` THEN
2665 SRW_TAC [] [ORL_bt_lb_ub, bt_to_orl_lb_ub, bt_to_list] THEN
2666 METIS_TAC [ORL_bt_lb_ub_lem]
2667]
2668QED
2669
2670Theorem ORL_bt_lb_thm[local]:
2671 !cmp t:('a#'b) bt lb. ORL_bt_lb cmp lb t ==>
2672 (bt_to_orl_lb cmp lb t = bt_to_list t)
2673Proof
2674GEN_TAC THEN Induct THENL
2675[REWRITE_TAC [bt_to_orl_lb, bt_to_list]
2676,P_PGEN_TAC ``a:'a,b:'b`` THEN
2677 SRW_TAC [] [ORL_bt_lb, bt_to_orl_lb, ORL_bt_lb_ub_thm, bt_to_list] THEN
2678 METIS_TAC [ORL_bt_lb_ub_lem]
2679]
2680QED
2681
2682Theorem ORL_bt_ub_thm[local]:
2683 !cmp t:('a#'b) bt ub. ORL_bt_ub cmp t ub ==>
2684 (bt_to_orl_ub cmp t ub = bt_to_list t)
2685Proof
2686GEN_TAC THEN Induct THENL
2687[REWRITE_TAC [bt_to_orl_ub, bt_to_list]
2688,P_PGEN_TAC ``a:'a,b:'b`` THEN
2689 SRW_TAC [] [ORL_bt_ub, bt_to_orl_ub, ORL_bt_lb_ub_thm, bt_to_list] THEN
2690 METIS_TAC [ORL_bt_lb_ub_lem]
2691]
2692QED
2693
2694Theorem ORL_bt_thm[local]:
2695 !cmp t:('a#'b) bt. ORL_bt cmp t ==> (bt_to_orl cmp t = bt_to_list t)
2696Proof
2697GEN_TAC THEN Induct THENL (* really Cases, but need !a to use P_PGEN_TAC *)
2698[REWRITE_TAC [bt_to_orl, bt_to_list]
2699,P_PGEN_TAC ``a:'a,b:'b`` THEN SRW_TAC []
2700 [ORL_bt, bt_to_orl, ORL_bt_lb_thm, ORL_bt_ub_thm, bt_to_list]]
2701QED
2702
2703Theorem better_bt_to_orl:
2704 !cmp t:('a#'b) bt. bt_to_orl cmp t = if ORL_bt cmp t then bt_to_list_ac t []
2705 else bt_to_orl_ac cmp t []
2706Proof
2707METIS_TAC [ORL_bt_thm, bt_to_list_thm, bt_to_orl_thm]
2708QED
2709
2710(* ****************************************************************** *)
2711(* Theorems to support FUPDATE_CONV, for both FMAPAL and fmap terms. *)
2712(* *** NOTE: FUPDATE_CONV will fail if it is asked to extend the *** *)
2713(* *** domain, that is convert f |+ (x,y) where x NOTIN FDOM f, *** *)
2714(* *** which could not be done efficiently for a FMAPAL, and *** *)
2715(* *** has no clearly best implementation for fmap [ ... ]'s. *** *)
2716(* ****************************************************************** *)
2717
2718(* Making list_rplacv_cn exit directly on its error condition (not finding
2719 x) and use a continuation otherwise seems like reasonable programming;
2720 however, encoding the error condition as a return of the empty list
2721 (since that can never be a successful answer) is a hack, into which I
2722 am lured to save the bother of using an option type. *)
2723
2724Definition list_rplacv_cn:
2725 (list_rplacv_cn (x:'a,y:'b) [] (cn:('a#'b)list -> ('a#'b)list) = []) /\
2726 (list_rplacv_cn (x,y) ((w,z)::l) cn =
2727 if x = w then cn ((x,y)::l)
2728 else list_rplacv_cn (x,y) l (\m. cn ((w,z)::m)))
2729End
2730
2731Theorem fmap_FDOM_rec:
2732 (!x:'a. x IN FDOM (fmap ([]:('a#'b)list)) = F) /\
2733 (!x w:'a z:'b l. x IN FDOM (fmap ((w,z)::l)) =
2734 (x = w) \/ x IN FDOM (fmap l))
2735Proof
2736SRW_TAC [] [fmap_FDOM]
2737QED
2738
2739Theorem list_rplacv_NIL[local]:
2740 !x:'a y:'b l cn. (!m. cn m <> []) ==>
2741 ((list_rplacv_cn (x,y) l cn = []) <=> x NOTIN FDOM (fmap l))
2742Proof
2743GEN_TAC THEN GEN_TAC THEN Induct THENL
2744[RW_TAC (srw_ss()) [list_rplacv_cn, fmap_FDOM_rec]
2745,P_PGEN_TAC ``w:'a,z:'b`` THEN
2746 RW_TAC (srw_ss()) [list_rplacv_cn, fmap_FDOM_rec]
2747]
2748QED
2749
2750Theorem list_rplacv_cont_lem[local]:
2751 !x:'a y:'b l cn cn'. list_rplacv_cn (x,y) l cn <> [] ==>
2752 (list_rplacv_cn (x,y) l (cn' o cn) =
2753 cn' (list_rplacv_cn (x,y) l cn))
2754Proof
2755GEN_TAC THEN GEN_TAC THEN Induct THENL
2756[SRW_TAC [] [list_rplacv_cn]
2757,P_PGEN_TAC ``w:'a,z:'b`` THEN
2758 SRW_TAC [] [list_rplacv_cn] THEN RES_TAC THEN
2759 Q.SUBGOAL_THEN `(\m. cn' (cn ((w,z)::m))) = (cn' o (\m. cn ((w,z)::m)))`
2760 (ASM_REWRITE_TAC o ulist) THEN
2761 CONV_TAC FUN_EQ_CONV THEN SRW_TAC [] []
2762]
2763QED
2764
2765Theorem bool_lem[local]:
2766 !P Q.(if ~P then ~P else P /\ Q) <=> P ==> Q
2767Proof
2768RW_TAC bool_ss [IMP_DISJ_THM]
2769QED
2770
2771Theorem list_rplacv_thm:
2772 !x:'a y:'b l.
2773let ans = list_rplacv_cn (x,y) l (\m.m)
2774in if ans = [] then x NOTIN FDOM (fmap l)
2775 else x IN FDOM (fmap l) /\ (fmap l |+ (x,y) = fmap ans)
2776Proof
2777GEN_TAC THEN GEN_TAC THEN REWRITE_TAC [LET_THM] THEN BETA_TAC THEN
2778Induct THENL
2779[SRW_TAC [] [list_rplacv_cn, fmap_FDOM, MAP]
2780,P_PGEN_TAC ``w:'a,z:'b`` THEN
2781 REWRITE_TAC [list_rplacv_cn, fmap_FDOM_rec] THEN Cases_on `x = w` THEN AR THENL
2782 [SRW_TAC [] [fmap_CONS]
2783 ,`!m.(\m. (\m.m) ((w,z)::m)) m <> []` by SRW_TAC [] [] THEN
2784 IMP_RES_THEN (REWRITE_TAC o ulist) list_rplacv_NIL THEN
2785 REWRITE_TAC [bool_lem] THEN DISCH_TAC THEN
2786 `(fmap (list_rplacv_cn (x,y) l (\m.m)) = fmap l |+ (x,y)) /\
2787 list_rplacv_cn (x,y) l (\m.m) <> []` by METIS_TAC [] THEN
2788 Q.SUBGOAL_THEN `(\m. (\m.m)((w,z)::m)) = (\m. ((w,z)::m)) o (\m.m)` SUBST1_TAC
2789 THEN1 (CONV_TAC FUN_EQ_CONV THEN SRW_TAC [] []) THEN
2790 IMP_RES_THEN (REWRITE_TAC o ulist) list_rplacv_cont_lem THEN BETA_TAC THEN
2791 ASM_REWRITE_TAC [fmap_CONS] THEN MATCH_MP_TAC FUPDATE_COMMUTES THEN
2792 CONV_TAC (RAND_CONV (REWR_CONV EQ_SYM_EQ)) THEN AR
2793]]
2794QED
2795
2796(* *************************************************************** *)
2797(* Now to treat similarly terms of the form *)
2798(* FMAPAL cmp (node ... ) |+ (x,y), with similar provision that *)
2799(* domain will not be extended. *)
2800(* *************************************************************** *)
2801
2802Definition bt_rplacv_cn:
2803 (bt_rplacv_cn cmp (x:'a,y:'b) nt (cn:('a#'b)bt -> ('a#'b)bt) = nt) /\
2804 (bt_rplacv_cn cmp (x,y) (node l (w,z) r) cn =
2805 case apto cmp x w of
2806 LESS => bt_rplacv_cn cmp (x,y) l (\m. cn (node m (w,z) r))
2807 | EQUAL => cn (node l (x,y) r)
2808 | GREATER => bt_rplacv_cn cmp (x,y) r (\m. cn (node l (w,z) m)))
2809End
2810
2811(* FMAPAL_FDOM_THM (corresp. to fmap_FDOM_rec) has already been proved. *)
2812
2813Theorem bt_rplacv_nt[local]:
2814 !cmp x:'a y:'b t cn. (!m. cn m <> nt) ==>
2815 ((bt_rplacv_cn cmp (x,y) t cn = nt) <=> x NOTIN FDOM (FMAPAL cmp t))
2816Proof
2817GEN_TAC THEN GEN_TAC THEN GEN_TAC THEN Induct THENL
2818[RW_TAC (srw_ss()) [bt_rplacv_cn, FMAPAL_FDOM_THM]
2819,P_PGEN_TAC ``w:'a,z:'b`` THEN
2820 RW_TAC (srw_ss()) [bt_rplacv_cn, FMAPAL_FDOM_THM] THEN
2821 Cases_on `apto cmp x w` THEN SRW_TAC [] []
2822]
2823QED
2824
2825Theorem bt_rplacv_cont_lem[local]:
2826 !cmp x:'a y:'b t cn cn'. bt_rplacv_cn cmp (x,y) t cn <> nt ==>
2827 (bt_rplacv_cn cmp (x,y) t (cn' o cn) =
2828 cn' (bt_rplacv_cn cmp (x,y) t cn))
2829Proof
2830GEN_TAC THEN GEN_TAC THEN GEN_TAC THEN Induct THENL
2831[SRW_TAC [] [bt_rplacv_cn]
2832,P_PGEN_TAC ``w:'a,z:'b`` THEN Cases_on `apto cmp x w` THEN
2833 SRW_TAC [] [bt_rplacv_cn] THEN RES_TAC THENL
2834 [Q.SUBGOAL_THEN `(\m. cn' (cn (node m (w,z) t'))) =
2835 (cn' o (\m. cn (node m (w,z) t')))`
2836 (ASM_REWRITE_TAC o ulist)
2837 ,Q.SUBGOAL_THEN `(\m. cn' (cn (node t (w,z) m))) =
2838 (cn' o (\m. cn (node t (w,z) m)))`
2839 (ASM_REWRITE_TAC o ulist)
2840 ] THEN
2841 CONV_TAC FUN_EQ_CONV THEN SRW_TAC [] []
2842]
2843QED
2844
2845(* FUNION_FUPDATE_1 =
2846 |- !f g x y. f |+ (x,y) FUNION g = (f FUNION g) |+ (x,y)
2847 FUNION_FUPDATE_2 =
2848 (|- !f g x y. f FUNION g |+ (x,y) =
2849 if x IN FDOM f then f FUNION g else (f FUNION g) |+ (x,y) *)
2850
2851Theorem FUNION_FUPDATE_HALF_2[local]:
2852 !f:'a|->'b g x y. x NOTIN FDOM f ==>
2853 ((f FUNION g) |+ (x,y) = f FUNION g |+ (x,y))
2854Proof
2855METIS_TAC [FUNION_FUPDATE_2]
2856QED
2857
2858Theorem bt_rplacv_thm:
2859 !cmp x:'a y:'b t.
2860let ans = bt_rplacv_cn cmp (x,y) t (\m.m)
2861in if ans = nt then x NOTIN FDOM (FMAPAL cmp t)
2862else x IN FDOM (FMAPAL cmp t) /\ (FMAPAL cmp t |+ (x,y) = FMAPAL cmp ans)
2863Proof
2864GEN_TAC THEN GEN_TAC THEN GEN_TAC THEN REWRITE_TAC [LET_THM] THEN BETA_TAC THEN
2865Induct THENL
2866[SRW_TAC [] [bt_rplacv_cn, FMAPAL_FDOM_THM]
2867,P_PGEN_TAC ``w:'a,z:'b`` THEN
2868 REWRITE_TAC [bt_rplacv_cn, FMAPAL_FDOM_THM] THEN
2869 Cases_on `apto cmp x w` THEN ASM_REWRITE_TAC [cpn_case_def] THENL
2870 [`!m.(\m. (\m.m) (node m (w,z) t')) m <> nt` by SRW_TAC [] [] THEN
2871 IMP_RES_THEN (REWRITE_TAC o ulist) bt_rplacv_nt THEN
2872 REWRITE_TAC [bool_lem] THEN DISCH_TAC THEN
2873 `(FMAPAL cmp (bt_rplacv_cn cmp (x,y) t (\m.m)) = FMAPAL cmp t |+ (x,y)) /\
2874 bt_rplacv_cn cmp (x,y) t (\m.m) <> nt` by METIS_TAC [] THEN
2875 Q.SUBGOAL_THEN
2876 `(\m. (\m.m)(node m (w,z) t')) = (\m. (node m (w,z) t')) o (\m.m)` SUBST1_TAC
2877 THEN1 (CONV_TAC FUN_EQ_CONV THEN SRW_TAC [] []) THEN
2878 IMP_RES_THEN (REWRITE_TAC o ulist) bt_rplacv_cont_lem THEN BETA_TAC THEN
2879 ASM_REWRITE_TAC [bt_to_fmap, DRESTRICT_FUPDATE] THEN
2880 Q.SUBGOAL_THEN `x IN {z | apto cmp z w = LESS}` (REWRITE_TAC o ulist)
2881 THEN1 (CONV_TAC SET_SPEC_CONV THEN AR) THEN
2882 REWRITE_TAC [FUNION_FUPDATE_1]
2883 ,SRW_TAC [] [bt_to_fmap] THEN
2884 ONCE_REWRITE_TAC [GSYM FUNION_FUPDATE_1] THEN
2885 Q.SUBGOAL_THEN
2886 `x NOTIN FDOM (DRESTRICT (FMAPAL cmp t) {y | apto cmp y w = LESS})`
2887 (REWRITE_TAC o ulist o MATCH_MP FUNION_FUPDATE_HALF_2) THENL
2888 [REWRITE_TAC [FDOM_DRESTRICT, IN_INTER, DE_MORGAN_THM] THEN
2889 DISJ2_TAC THEN CONV_TAC (RAND_CONV SET_SPEC_CONV) THEN SRW_TAC [] []
2890 ,IMP_RES_TAC toto_equal_imp_eq THEN ASM_REWRITE_TAC [FUPDATE_EQ]
2891 ]
2892 ,`!m.(\m. (\m.m) (node t (w,z) m)) m <> nt` by SRW_TAC [] [] THEN
2893 IMP_RES_THEN (REWRITE_TAC o ulist) bt_rplacv_nt THEN
2894 REWRITE_TAC [bool_lem] THEN DISCH_TAC THEN
2895 `(FMAPAL cmp (bt_rplacv_cn cmp (x,y) t' (\m.m)) = FMAPAL cmp t' |+ (x,y)) /\
2896 bt_rplacv_cn cmp (x,y) t' (\m.m) <> nt` by METIS_TAC [] THEN
2897 Q.SUBGOAL_THEN
2898 `(\m. (\m.m) (node t (w,z) m)) = (\m. (node t (w,z) m)) o (\m.m)` SUBST1_TAC
2899 THEN1 (CONV_TAC FUN_EQ_CONV THEN SRW_TAC [] []) THEN
2900 IMP_RES_THEN (REWRITE_TAC o ulist) bt_rplacv_cont_lem THEN BETA_TAC THEN
2901 ASM_REWRITE_TAC [bt_to_fmap, DRESTRICT_FUPDATE] THEN
2902 Q.SUBGOAL_THEN `x IN {z | apto cmp w z = LESS}` (REWRITE_TAC o ulist)
2903 THEN1 (CONV_TAC SET_SPEC_CONV THEN ASM_REWRITE_TAC [GSYM toto_antisym]) THEN
2904 Q.SUBGOAL_THEN
2905 `x NOTIN FDOM (DRESTRICT (FMAPAL cmp t) {y | apto cmp y w = LESS} FUNION
2906 FEMPTY |+ (w,z))`
2907 (REWRITE_TAC o ulist o MATCH_MP FUNION_FUPDATE_HALF_2) THEN
2908 REWRITE_TAC [FDOM_FUNION, IN_UNION, FDOM_DRESTRICT, IN_INTER, DE_MORGAN_THM,
2909 FDOM_FUPDATE, IN_INSERT, FDOM_FEMPTY, NOT_IN_EMPTY] THEN
2910 CONJ_TAC THENL
2911 [DISJ2_TAC THEN CONV_TAC (RAND_CONV SET_SPEC_CONV) THEN SRW_TAC [] []
2912 ,IMP_RES_TAC (CONJUNCT2 toto_glneq)
2913]]]
2914QED
2915
2916(* ***************************************************************** *)
2917(* Theorems to support FUN_fmap_CONV *)
2918(* ***************************************************************** *)
2919
2920Theorem FST_PAIR_ID[local]:
2921 !f:'a->'b. FST o (\x. (x,f x)) = I
2922Proof
2923GEN_TAC THEN CONV_TAC FUN_EQ_CONV THEN SRW_TAC [][combinTheory.o_THM]
2924QED
2925
2926Theorem FUN_fmap_thm:
2927 !f:'a->'b l:'a list. fmap (MAP (\x. (x, f x)) l) = FUN_FMAP f (set l)
2928Proof
2929GEN_TAC THEN Induct THENL
2930[RW_TAC (srw_ss()) [LIST_TO_SET_THM, FUN_FMAP_DEF, fmap_NIL]
2931,RW_TAC (srw_ss()) [LIST_TO_SET_THM, FUN_FMAP_DEF, fmap_CONS, fmap_EXT] THENL
2932 [REWRITE_TAC [FAPPLY_FUPDATE]
2933 ,REWRITE_TAC [FAPPLY_FUPDATE_THM] THEN
2934 Cases_on `x = h` THEN AR THEN
2935 `FINITE (set l)` by MATCH_ACCEPT_TAC FINITE_LIST_TO_SET THEN
2936 `x IN set l` by ASM_REWRITE_TAC [] THEN
2937 IMP_RES_TAC FUN_FMAP_DEF THEN AR
2938]]
2939QED
2940
2941(* ******************* Theorem to support fmap_TO_ORWL ********************* *)
2942
2943Theorem fmap_ORWL_thm:
2944 !cmp l:('a#'b)list. ORWL cmp (fmap l) (incr_sort cmp l)
2945Proof
2946REWRITE_TAC [ORWL, incr_sort_fmap, incr_sort_ORL]
2947QED
2948
2949Theorem T_OR[unlisted]:
2950 !p. T \/ p = T
2951Proof
2952 REWRITE_TAC [OR_CLAUSES]
2953QED
2954
2955Theorem F_OR[unlisted]:
2956 !p. F \/ p = p
2957Proof
2958 REWRITE_TAC [OR_CLAUSES]
2959QED
2960
2961Theorem NOT_CONS_NIL_EQN[unlisted]:
2962 !ab:'a#'b l. ((ab::l) = []) = F
2963Proof
2964 REWRITE_TAC [NOT_CONS_NIL]
2965QED
2966
2967Theorem NOT_node_nt_EQN[unlisted]:
2968 !ab:'a#'b l r. ((node l ab r) = nt) = F
2969Proof
2970 REWRITE_TAC [GSYM bt_distinct]
2971QED