finite_setScript.sml
1Theory finite_set
2Ancestors
3 arithmetic list lifting transfer cardinalityCore
4Libs
5 quotient transferLib bnfBase
6
7(* the bound is a cardinality, and cardinalityCoreTheory makes no
8 grammar of its own; this is kept to itself so that a theory
9 declaring a datatype does not inherit the notation *)
10Overload "<<="[local] = “cardleq”
11
12
13Theorem psEXTENSION[local] = pred_setTheory.EXTENSION
14
15Overload FUN_REL[local] = “$===>”
16
17Theorem RSUBSET_I:
18 R1 RSUBSET R2 ==> R1 x y ==> R2 x y
19Proof
20 simp[relationTheory.RSUBSET]
21QED
22
23
24Theorem FUN_REL_O:
25 ((D1 |==> R1) O (D2 |==> R2)) RSUBSET ((D1 O D2) |==> (R1 O R2))
26Proof
27 simp[FUN_REL_def, relationTheory.O_DEF, relationTheory.RSUBSET] >> metis_tac[]
28QED
29
30Theorem RSUBSET_REFL[simp]:
31 R RSUBSET R
32Proof
33 simp[relationTheory.RSUBSET]
34QED
35
36Theorem FUN_REL_RSUBSET[simp]:
37 D2 RSUBSET D1 /\ R1 RSUBSET R2 ==> (D1 |==> R1) RSUBSET (D2 |==> R2)
38Proof
39 simp[relationTheory.RSUBSET, FUN_REL_def]>>metis_tac[]
40QED
41
42fun INTRO th =
43 goal_assum (resolve_then.resolve_then resolve_then.Any mp_tac th)
44
45Definition fsequiv_def:
46 fsequiv l1 l2 <=> set l1 = set l2
47End
48
49Theorem fsequiv_refl[simp]:
50 fsequiv l l
51Proof
52 simp[fsequiv_def]
53QED
54
55Theorem fsequiv_equiv:
56 EQUIV fsequiv
57Proof
58 simp[quotientTheory.EQUIV_def, FUN_EQ_THM, fsequiv_def] >>
59 metis_tac[]
60QED
61
62val _ = define_quotient_types
63 {defs = [], old_thms = [],
64 poly_preserves = [],
65 poly_respects = [],
66 respects = [],
67 tyop_equivs = [],
68 tyop_quotients = [],
69 tyop_simps = [],
70 types = [{equiv = fsequiv_equiv, name = "fset"}]}
71
72(* map from list to set is fset_ABS, in other direction it's fset_REP *)
73val fset_ABS_REP_CLASS = theorem "fset_ABS_REP_CLASS"
74Theorem bijection2 = fset_ABS_REP_CLASS
75 |> CONJUNCT2 |> SPEC_ALL |> EQ_IMP_RULE |> #1
76 |> GEN_ALL
77 |> SIMP_RULE bool_ss [PULL_EXISTS, fsequiv_refl]
78
79Theorem REP_CLASS_11[simp]:
80 fset_REP_CLASS fs1 = fset_REP_CLASS fs2 <=> fs1 = fs2
81Proof
82 metis_tac[fset_ABS_REP_CLASS]
83QED
84
85Theorem REP_ABS_equiv[simp]:
86 fset_REP_CLASS (fset_ABS_CLASS (fsequiv r)) = fsequiv r
87Proof
88 simp[GSYM (CONJUNCT2 fset_ABS_REP_CLASS)] >> metis_tac[]
89QED
90
91Theorem ABS_CLASS_onto:
92 !fs. ?r. fs = fset_ABS_CLASS (fsequiv r)
93Proof
94 metis_tac[fset_ABS_REP_CLASS]
95QED
96
97Theorem REP_CLASS_NONEMPTY:
98 !fs. ?x. fset_REP_CLASS fs x
99Proof
100 gen_tac >> qspec_then ‘fs’ (qx_choose_then ‘r’ assume_tac) ABS_CLASS_onto >>
101 simp[] >> metis_tac[fsequiv_refl]
102QED
103
104Theorem fset_ABS_REP[simp]:
105 fset_ABS (fset_REP s) = s
106Proof
107 simp[definition "fset_ABS_def", definition "fset_REP_def"] >>
108 ‘fsequiv ($@ (fset_REP_CLASS s)) = fset_REP_CLASS s’
109 suffices_by metis_tac[REP_CLASS_11, REP_ABS_equiv] >>
110 simp[FUN_EQ_THM] >> qx_gen_tac ‘a’ >> SELECT_ELIM_TAC >> conj_tac
111 >- metis_tac[REP_CLASS_NONEMPTY] >>
112 rw[EQ_IMP_THM] >>
113 qspec_then ‘s’ (qx_choose_then ‘r’ assume_tac) ABS_CLASS_onto >> fs[] >>
114 metis_tac[quotientTheory.EQUIV_def, fsequiv_equiv]
115QED
116
117Theorem fset_REP_11[simp]:
118 fset_REP fs1 = fset_REP fs2 <=> fs1 = fs2
119Proof
120 metis_tac[fset_ABS_REP]
121QED
122
123Theorem fset_ABS_onto:
124 !fs. ?l. fset_ABS l = fs
125Proof
126 metis_tac[fset_ABS_REP]
127QED
128
129Definition FSET_def:
130 FSET AB al bfs <=> ?bl. LIST_REL AB al bl /\ bfs = fset_ABS bl
131End
132
133Theorem FSET_AB_eqn:
134 FSET AB = FSET (=) O LIST_REL AB
135Proof
136 simp[FSET_def, FUN_EQ_THM, relationTheory.O_DEF]
137QED
138
139Theorem FSET_right_unique[transfer_safe]:
140 right_unique AB ==> right_unique (FSET AB)
141Proof
142 simp[FSET_def, PULL_EXISTS, right_unique_def] >>
143 metis_tac[LIST_REL_right_unique, right_unique_def, fsequiv_refl]
144QED
145
146Theorem FSET_surj[transfer_safe]:
147 surj AB ==> surj (FSET AB)
148Proof
149 simp[FSET_def, surj_def] >> metis_tac[fset_ABS_onto, LIST_REL_surj, surj_def]
150QED
151
152Theorem fset_ABS_11[simp]:
153 fset_ABS l1 = fset_ABS l2 <=> fsequiv l1 l2
154Proof
155 rw[EQ_IMP_THM, definition "fset_ABS_def"]
156 >- (pop_assum (mp_tac o Q.AP_TERM ‘fset_REP_CLASS’) >>
157 simp[bijection2, Excl "REP_CLASS_11"]) >>
158 ‘fsequiv l1 = fsequiv l2’ suffices_by metis_tac[bijection2, REP_CLASS_11] >>
159 metis_tac[fsequiv_equiv, quotientTheory.EQUIV_def]
160QED
161
162Theorem total_FSET[transfer_safe]:
163 total AB ==> total (FSET AB)
164Proof
165 simp[total_def, FSET_def] >> metis_tac[LIST_REL_total, total_def]
166QED
167
168Theorem RDOM_FSET0[simp,transfer_simp]:
169 RDOM (FSET AB) = \al. !x. MEM x al ==> RDOM AB x
170Proof
171 simp[psEXTENSION, IN_DEF, relationTheory.RDOM_DEF, FSET_def] >>
172 Induct >> simp[] >> simp[IN_DEF, relationTheory.RDOM_DEF] >> metis_tac[]
173QED
174
175Theorem fset0Q[simp]:
176 Qt fsequiv fset_ABS fset_REP (FSET (=))
177Proof
178 simp[Qt_def, relationTheory.O_DEF, relationTheory.inv_DEF, FUN_EQ_THM,
179 FSET_def]
180QED
181
182Overload FSET0[local] = “FSET $=”
183
184(* important for predicates over the new type - generic version of this
185 should be proved *)
186Theorem RDOM_FSET0set[simp,transfer_simp]:
187 RDOM (FSET0 |==> ($= : bool -> bool -> bool)) =
188 \lP. (!l1 l2. lP l1 /\ fsequiv l1 l2 ==> lP l2)
189Proof
190 rw[relationTheory.RDOM_DEF, Once FUN_EQ_THM, FUN_REL_def, FSET_def] >>
191 eq_tac >> rw[]
192 >- metis_tac[fset_ABS_11] >>
193 qexists_tac ‘\fs. lP (fset_REP fs)’ >> simp[] >>
194 metis_tac[R_repabs, fsequiv_equiv, quotientTheory.EQUIV_def, fsequiv_refl,
195 fset0Q]
196QED
197
198Theorem surj_FSET0[transfer_safe] = MATCH_MP Qt_surj fset0Q
199Theorem right_unique_FSET0[transfer_safe] = MATCH_MP Qt_right_unique fset0Q
200Theorem FSETEQ[transfer_rule] = MATCH_MP Qt_EQ fset0Q
201
202Definition fIN_def:
203 fIN = (I ---> fset_REP ---> I) MEM
204End
205
206Theorem MEM_transfers[transfer_rule]:
207 bi_unique AB ==> (AB |==> LIST_REL AB |==> (=)) MEM MEM
208Proof
209 rw[FUN_REL_def] >> fs[LIST_REL_EL_EQN, MEM_EL]>>
210 metis_tac[bi_unique_def, right_unique_def, left_unique_def]
211QED
212
213Theorem fIN_relates[transfer_rule]:
214 bi_unique AB ==> (AB |==> FSET AB |==> (=)) MEM fIN
215Proof
216 strip_tac >> simp[Once FSET_AB_eqn] >> irule RSUBSET_I >>
217 qexists_tac ‘(=) O AB |==> FSET0 O LIST_REL AB |==> (=) O (=)’ >>
218 reverse conj_tac >- simp[] >> irule RSUBSET_I >>
219 qexists_tac ‘$= O AB |==> ((FSET0 |==> (=)) O (LIST_REL AB |==> (=)))’ >>
220 reverse conj_tac >- (irule FUN_REL_RSUBSET >> simp[FUN_REL_O]) >>
221 irule RSUBSET_I >> INTRO FUN_REL_O >>
222 simp[relationTheory.O_DEF] >> INTRO MEM_transfers >> simp[] >>
223 irule HK_thm2 >> INTRO fIN_def >> INTRO funQ >> INTRO funQ >>
224 INTRO fset0Q >> INTRO idQ >> INTRO idQ >>
225 simp[FUN_REL_def, fsequiv_def]
226QED
227
228Theorem EXTENSION:
229 !s1 s2. (s1 = s2) <=> !e. fIN e s1 <=> fIN e s2
230Proof
231 xfer_back_tac [] >> simp[fsequiv_def, psEXTENSION]
232QED
233
234Definition fUNION_def:
235 fUNION = (fset_REP ---> fset_REP ---> fset_ABS) APPEND
236End
237
238Theorem fUNION_relates[transfer_rule]:
239 (FSET0 |==> FSET0 |==> FSET0) APPEND fUNION
240Proof
241 map_every INTRO [HK_thm2, fUNION_def, funQ, funQ, fset0Q, fset0Q, fset0Q] >>
242 (* respectfulness *)
243 simp[FUN_REL_def, fsequiv_def]
244QED
245
246Theorem IN_UNION[simp]:
247 !e s1 s2. fIN e (fUNION s1 s2) <=> fIN e s1 \/ fIN e s2
248Proof
249 xfer_back_tac [] >> simp[]
250QED
251
252Definition fEMPTY_def:
253 fEMPTY = fset_ABS []
254End
255
256Theorem fEMPTY_relates[transfer_rule]:
257 FSET0 [] fEMPTY
258Proof
259 map_every INTRO [HK_thm2, fEMPTY_def, fset0Q] (* INTRO fsequiv_refl *) >>
260 simp[]
261QED
262
263Theorem NOT_IN_EMPTY[simp]:
264 !e. ~fIN e fEMPTY
265Proof
266 xfer_back_tac [] >> simp[]
267QED
268
269Definition fINSERT_def:
270 fINSERT = (I ---> fset_REP ---> fset_ABS) CONS
271End
272
273Theorem fINSERT_relates[transfer_rule]:
274 ((=) |==> FSET0 |==> FSET0) CONS fINSERT
275Proof
276 map_every INTRO [HK_thm2, fINSERT_def, funQ, funQ, fset0Q, fset0Q, idQ] >>
277 simp[FUN_REL_def, fsequiv_def] (* respectfulness *)
278QED
279
280Theorem IN_INSERT[simp]:
281 !e1 e2 s. fIN e1 (fINSERT e2 s) <=> e1 = e2 \/ fIN e1 s
282Proof
283 xfer_back_tac [] >> simp[]
284QED
285
286Theorem IN_KT[local,simp]: !x. x IN K T
287Proof simp[IN_DEF]
288QED
289
290Theorem fABSORPTION:
291 !a A. fIN a A <=> fINSERT a A = A
292Proof
293 xfer_back_tac [] >> simp[fsequiv_def, pred_setTheory.ABSORPTION]
294QED
295
296Theorem fset_cases:
297 !s:'a fset. s = fEMPTY \/ ?e s0. s = fINSERT e s0 /\ ~fIN e s0
298Proof
299 xfer_back_tac [] >> simp[fsequiv_def, pred_setTheory.SUBSET_DEF] >> Cases >>
300 simp[] >>
301 rename [‘e INSERT set L = _ INSERT set _’] >> qexists_tac ‘e’ >>
302 qexists_tac ‘FILTER ($~ o (=) e) L’ >>
303 simp[MEM_FILTER, LIST_TO_SET_FILTER,
304 psEXTENSION] >>
305 metis_tac[]
306QED
307
308Theorem fINSERT_duplicates[simp]:
309 !e s. fINSERT e (fINSERT e s) = fINSERT e s
310Proof
311 xfer_back_tac [] >> simp[fsequiv_def]
312QED
313
314Theorem fINSERT_commutes:
315 !e1 e2 s. fINSERT e1 (fINSERT e2 s) = fINSERT e2 (fINSERT e1 s)
316Proof
317 xfer_back_tac [] >> simp[fsequiv_def, psEXTENSION] >> metis_tac[]
318QED
319
320Theorem fset_induction:
321 !P. P fEMPTY /\ (!e s. P s /\ ~fIN e s ==> P (fINSERT e s)) ==> !s. P s
322Proof
323 xfer_back_tac [] >> qx_gen_tac ‘P’ >> ntac 2 strip_tac >> Induct >> simp[] >>
324 qx_gen_tac ‘h’ >> rename [‘P []’, ‘P (h::t)’] >>
325 reverse (Cases_on ‘MEM h t’) >- simp[] >>
326 ‘fsequiv t (h::t)’ suffices_by metis_tac[] >>
327 simp[fsequiv_def, psEXTENSION] >> metis_tac[]
328QED
329
330Theorem NOT_EMPTY_INSERT[simp]:
331 !h t. fEMPTY <> fINSERT h t
332Proof
333 xfer_back_tac [] >> simp[fsequiv_def]
334QED
335
336Theorem fUNION_COMM:
337 !s1 s2. fUNION s1 s2 = fUNION s2 s1
338Proof
339 xfer_back_tac [] >> simp[fsequiv_def, pred_setTheory.UNION_COMM]
340QED
341
342Theorem fUNION_ASSOC:
343 !s1 s2 s3. fUNION s1 (fUNION s2 s3) = fUNION (fUNION s1 s2) s3
344Proof
345 xfer_back_tac [] >> simp[fsequiv_def, pred_setTheory.UNION_ASSOC]
346QED
347
348Theorem fUNION_EMPTY[simp]:
349 !s. fUNION fEMPTY s = s /\ fUNION s fEMPTY = s
350Proof
351 xfer_back_tac [] >> simp[]
352QED
353
354Theorem fUNION_EQ_EMPTY[simp]:
355 !s1 s2. fUNION s1 s2 = fEMPTY <=> s1 = fEMPTY /\ s2 = fEMPTY
356Proof
357 xfer_back_tac [] >> simp[fsequiv_def]
358QED
359
360Theorem fUNION_IDEMPOT[simp]:
361 !s. fUNION s s = s
362Proof
363 xfer_back_tac [] >> simp[fsequiv_def]
364QED
365
366Theorem fUNION_INSERT:
367 fUNION (fINSERT a A) B = fINSERT a (fUNION A B)
368Proof
369 simp[EXTENSION] >> metis_tac[]
370QED
371
372Definition fDELETE_def:
373 fDELETE = (I ---> fset_REP ---> fset_ABS) (\e. FILTER ($~ o $= e))
374End
375
376Theorem fDELETE_relates[transfer_rule]:
377 ((=) |==> FSET0 |==> FSET0) (\e. FILTER ($~ o $= e)) fDELETE
378Proof
379 map_every INTRO [HK_thm2, fDELETE_def, funQ, funQ, fset0Q, fset0Q, idQ] >>
380 (* respectfulness *)
381 simp[FUN_REL_def, fsequiv_def, LIST_TO_SET_FILTER]
382QED
383
384Theorem fDELETE_nonelement[simp]:
385 !e s. ~fIN e s ==> fDELETE e s = s
386Proof
387 xfer_back_tac [] >> simp[fsequiv_def, psEXTENSION, MEM_FILTER] >>
388 metis_tac[]
389QED
390
391Theorem IN_DELETE[simp]:
392 !a b s. fIN a (fDELETE b s) <=> a <> b /\ fIN a s
393Proof
394 xfer_back_tac [] >> simp[MEM_FILTER] >> metis_tac[]
395QED
396
397Theorem INSERT_DELETE[simp]:
398 !e s. fINSERT e (fDELETE e s) = fINSERT e s
399Proof
400 simp[EXTENSION] >> metis_tac[]
401QED
402
403Theorem DELETE_EMPTY[simp]:
404 !e. fDELETE e fEMPTY = fEMPTY
405Proof
406 simp[EXTENSION]
407QED
408
409Theorem fDELETE_UNION:
410 fDELETE e (fUNION A B) = fUNION (fDELETE e A) (fDELETE e B)
411Proof
412 simp[EXTENSION] >> metis_tac[]
413QED
414
415Theorem fDELETE_INSERT[simp]:
416 fDELETE a (fINSERT a A) = fDELETE a A
417Proof
418 simp[EXTENSION] >> metis_tac[]
419QED
420
421Definition fCARD_def:
422 fCARD = (fset_REP ---> I) (LENGTH o nub)
423End
424
425Theorem fCARD_relates[transfer_rule]:
426 (FSET0 |==> $=) (LENGTH o nub) fCARD
427Proof
428 map_every INTRO [HK_thm2, fCARD_def, funQ, idQ, fset0Q] >>
429 simp[fsequiv_def, FUN_REL_def] >>
430 (* respectfulness *)
431 Induct>> rw[nub_def]
432 >- metis_tac[pred_setTheory.ABSORPTION_RWT] >>
433 ‘MEM h b’ by metis_tac[pred_setTheory.IN_INSERT] >>
434 pop_assum (strip_assume_tac o
435 SIMP_RULE (srw_ss()) [Once MEM_SPLIT_APPEND_first]) >>
436 rw[length_nub_append, nub_def] >>
437 qabbrev_tac ‘b' = pfx ++ FILTER (\x. ~MEM x pfx /\ x <> h) sfx’ >>
438 ‘set a = set b'’
439 by (simp[Abbr‘b'’, LIST_TO_SET_FILTER, psEXTENSION]>>
440 fs[psEXTENSION] >> metis_tac[]) >>
441 ‘LENGTH (nub b') = LENGTH (nub a)’ by metis_tac[] >>
442 fs[Abbr‘b'’, length_nub_append, rich_listTheory.FILTER_FILTER] >>
443 pop_assum mp_tac >> csimp[]
444QED
445
446Theorem fCARD_THM[simp]:
447 fCARD fEMPTY = 0 /\
448 !e s. fCARD (fINSERT e s) = 1 + fCARD (fDELETE e s)
449Proof
450 xfer_back_tac [] >> simp[nub_def] >> rpt strip_tac >>
451 rename [‘MEM h t’] >> rw[]
452 >- (fs[Once MEM_SPLIT_APPEND_first] >>
453 csimp[length_nub_append, nub_def, FILTER_APPEND_DISTRIB,
454 MEM_FILTER, rich_listTheory.FILTER_FILTER] >>
455 rename [‘~MEM h pfx’] >>
456 ‘FILTER ($~ o $= h) pfx = pfx’ suffices_by (simp[] >> simp[EQ_SYM_EQ]) >>
457 rw[] >> pop_assum mp_tac >> Induct_on ‘pfx’ >> simp[]) >>
458 rename [‘~MEM h list’] >>
459 ‘FILTER ($~ o $= h) list = list’ suffices_by (simp[] >> simp[EQ_SYM_EQ]) >>
460 rw[] >> pop_assum mp_tac >> Induct_on ‘list’ >> simp[]
461QED
462
463Theorem fCARD_EQ0[simp]:
464 !s. fCARD s = 0 <=> s = fEMPTY
465Proof
466 xfer_back_tac [] >> simp[fsequiv_def]
467QED
468
469Definition fIMAGE_def:
470 fIMAGE = ((I ---> I) ---> fset_REP ---> fset_ABS) MAP
471End
472
473Theorem MAP_relates[transfer_rule]:
474 ((AB |==> CD) |==> LIST_REL AB |==> LIST_REL CD) MAP MAP
475Proof
476 rw[FUN_REL_def] >>
477 rename [‘LIST_REL CD (MAP f l1) (MAP g l2)’] >>
478 pop_assum mp_tac >> map_every qid_spec_tac [‘l2’, ‘l1’] >>
479 Induct_on ‘LIST_REL’ >> simp[]
480QED
481
482Theorem fIMAGE_relates[transfer_rule]:
483 ((AB |==> CD) |==> FSET AB |==> FSET CD) MAP fIMAGE
484Proof
485 irule RSUBSET_I >> INTRO FUN_REL_RSUBSET >>
486 simp[Once FSET_AB_eqn, SimpL “FUN_REL”] >>
487 simp[Once FSET_AB_eqn, SimpR “FUN_REL”] >>
488 INTRO FUN_REL_O >>
489 qexists_tac ‘(=) O (AB |==> CD)’ >> conj_tac >- simp[] >>
490 irule RSUBSET_I >>
491 INTRO FUN_REL_O >>
492 simp[relationTheory.O_DEF] >> qexists_tac ‘MAP’ >> simp[MAP_relates] >>
493 irule HK_thm2 >> rpt (INTRO funQ) >>
494 INTRO fIMAGE_def >> simp[] >> rpt (INTRO fset0Q) >>
495 INTRO idQ >> simp[FUN_REL_def, fsequiv_def, LIST_TO_SET_MAP]
496QED
497
498Theorem fIMAGE_thm[simp]:
499 (!f. fIMAGE (f:'a -> 'b) fEMPTY = fEMPTY) /\
500 (!(f:'a -> 'b) e s. fIMAGE f (fINSERT e s) = fINSERT (f e) (fIMAGE f s))
501Proof
502 xfer_back_tac [] >> simp[fsequiv_def]
503QED
504
505Theorem surjfns[transfer_safe]:
506 surj AB /\ right_unique AB /\ surj CD ==> surj (AB |==> CD)
507Proof
508 rw[FUN_REL_def, surj_def, right_unique_def] >>
509 qexists_tac ‘\a. let b = @b. AB a b in @c. CD c (y b)’ >>
510 metis_tac[]
511QED
512
513Theorem IN_IMAGE[simp]:
514 !f x s. fIN x (fIMAGE f s) <=> ?y. fIN y s /\ x = f y
515Proof
516 xfer_back_tac [] >> simp[MEM_MAP] >> metis_tac[]
517QED
518
519Theorem fIMAGE_11:
520 (!x y. f x = f y <=> x = y) ==>
521 (fIMAGE f x = fIMAGE f y <=> x = y)
522Proof
523 simp[EXTENSION] >> metis_tac[]
524QED
525
526Theorem fIMAGE_COMPOSE:
527 fIMAGE (f o g) s = fIMAGE f (fIMAGE g s)
528Proof
529 simp[EXTENSION] >> metis_tac[]
530QED
531
532Theorem fIMAGE_fUNION:
533 fIMAGE f (fUNION s1 s2) =
534 fUNION (fIMAGE f s1) (fIMAGE f s2)
535Proof
536 rw[EXTENSION, EQ_IMP_THM]
537 \\ metis_tac[]
538QED
539
540Theorem fIMAGE_ID[simp]:
541 fIMAGE (λx. x) s = s /\ fIMAGE I s = s
542Proof
543 simp[EXTENSION] >> metis_tac[]
544QED
545
546Definition fINTER_def:
547 fINTER = (fset_REP ---> fset_REP ---> fset_ABS)
548 (FILTER o flip (IN) o set)
549End
550
551Theorem fINTER_relates[transfer_rule]:
552 (FSET0 |==> FSET0 |==> FSET0) (FILTER o flip (IN) o set) fINTER
553Proof
554 map_every INTRO [HK_thm2, fINTER_def, funQ, funQ, fset0Q, fset0Q, fset0Q] >>
555 simp[FUN_REL_def, fsequiv_def, LIST_TO_SET_FILTER]
556QED
557
558Theorem IN_INTER[simp]:
559 !e s1 s2. fIN e (fINTER s1 s2) <=> fIN e s1 /\ fIN e s2
560Proof
561 xfer_back_tac [] >> simp[MEM_FILTER, CONJ_COMM]
562QED
563
564Theorem flip_IN_EMPTY[local]:
565 flip (IN) {} = \x. F
566Proof
567 simp[FUN_EQ_THM]
568QED
569
570Theorem fINTER_EMPTY[simp]:
571 !x. fINTER x fEMPTY = fEMPTY /\ fINTER fEMPTY x = fEMPTY
572Proof
573 xfer_back_tac [] >> simp[fsequiv_def, flip_IN_EMPTY]
574QED
575
576Theorem fINTER_IDEMPOT[simp]:
577 !x. fINTER x x = x
578Proof
579 xfer_back_tac [] >> simp[fsequiv_def, psEXTENSION, MEM_FILTER]
580QED
581
582Theorem fINTER_COMM:
583 fINTER a b = fINTER b a
584Proof
585 simp[EXTENSION] >> metis_tac[]
586QED
587
588Theorem fINTER_INSERT:
589 (fINTER (fINSERT a A) B =
590 if fIN a B then fINSERT a (fINTER A B) else fINTER A B) /\
591 (fINTER A (fINSERT b B) =
592 if fIN b A then fINSERT b (fINTER A B) else fINTER A B)
593Proof
594 rw[EXTENSION] >> metis_tac[]
595QED
596
597Definition fDIFF_def:
598 fDIFF = (fset_REP ---> fset_REP ---> fset_ABS)
599 (\l1 l2. FILTER (\x. ~MEM x l2) l1)
600End
601
602Theorem fDIFF_relates[transfer_rule]:
603 (FSET0 |==> FSET0 |==> FSET0) (\l1 l2. FILTER (\x. ~MEM x l2) l1) fDIFF
604Proof
605 map_every INTRO [HK_thm2, fDIFF_def, funQ, funQ] >>
606 rpt (INTRO fset0Q) >>
607 simp[FUN_REL_def, fsequiv_def, LIST_TO_SET_FILTER]
608QED
609
610Theorem IN_DIFF[simp]:
611 !e s1 s2. fIN e (fDIFF s1 s2) <=> fIN e s1 /\ ~fIN e s2
612Proof
613 xfer_back_tac [] >> simp[MEM_FILTER, CONJ_COMM]
614QED
615
616
617Definition fset_REL_def:
618 fset_REL AB fs1 fs2 <=> !a b. AB a b ==> (fIN a fs1 <=> fIN b fs2)
619End
620
621Definition toSet_def:
622 toSet fs = { x | fIN x fs }
623End
624
625Theorem toSet_fEMPTY[simp]:
626 toSet fEMPTY = {}
627Proof
628 rw[toSet_def]
629QED
630
631Theorem toSet_fINSERT:
632 toSet (fINSERT x s) = x INSERT (toSet s)
633Proof
634 rw[toSet_def, pred_setTheory.EXTENSION]
635QED
636
637Theorem toSet_fIMAGE:
638 toSet (fIMAGE f s) = IMAGE f (toSet s)
639Proof
640 rw[toSet_def, pred_setTheory.EXTENSION, EQ_IMP_THM]
641 \\ metis_tac[]
642QED
643
644Definition rel_set_def:
645 rel_set AB A B <=>
646 (!a. a IN A ==> ?b. b IN B /\ AB a b) /\
647 (!b. b IN B ==> ?a. a IN A /\ AB a b)
648End
649
650Theorem rel_set_empty[simp]:
651 rel_set AB {} {}
652Proof
653 simp[rel_set_def]
654QED
655
656Theorem LIST_TO_SET_rel_set:
657 (LIST_REL AB |==> rel_set AB) set set
658Proof
659 simp[FUN_REL_def] >> Induct_on ‘LIST_REL’ >> simp[] >>
660 simp[rel_set_def] >> metis_tac[]
661QED
662
663Theorem rel_set_RSUBSET:
664 bi_unique AB ==>
665 rel_set AB RSUBSET (AB |==> (=))
666Proof
667 simp[rel_set_def, relationTheory.RSUBSET, FUN_REL_def, IN_DEF,
668 bi_unique_def, left_unique_def, right_unique_def] >>
669 metis_tac[]
670QED
671
672Theorem RSUBSET_rel_set:
673 bitotal AB ==>
674 (AB |==> (=)) RSUBSET rel_set AB
675Proof
676 simp[rel_set_def, relationTheory.RSUBSET, FUN_REL_def, IN_DEF,
677 bitotal_def, total_def, surj_def] >>
678 metis_tac[]
679QED
680
681
682Theorem LIST_TO_SET_transfer:
683 (LIST_REL AB |==> rel_set AB) set set
684Proof
685 simp[FUN_REL_def] >> Induct_on ‘LIST_REL’ >> simp[] >>
686 simp[rel_set_def] >> metis_tac[]
687QED
688
689Theorem toSet_rel_set_relates[transfer_rule]:
690 (FSET AB |==> rel_set AB) set toSet
691Proof
692 simp[Once FSET_AB_eqn] >>
693 irule RSUBSET_I >>
694 qexists_tac ‘(FSET0 |==> (=)) O (LIST_REL AB |==> rel_set AB)’ >>
695 reverse conj_tac
696 >- (simp[relationTheory.RSUBSET, relationTheory.O_DEF, FUN_REL_def] >>
697 metis_tac[]) >>
698 simp[relationTheory.O_DEF] >>
699 map_every INTRO [LIST_TO_SET_transfer, HK_thm2, funQ, fset0Q, idQ] >>
700 rw[]
701 >- (simp[Once FUN_EQ_THM, toSet_def] >>
702 simp[psEXTENSION, fIN_def]) >>
703 simp[FUN_REL_def, fsequiv_def]
704QED
705
706Theorem toSet_relates:
707 bi_unique AB ==>
708 (FSET AB |==> AB |==> (=)) set toSet
709Proof
710 strip_tac >> simp[Once FSET_AB_eqn] >>
711 irule RSUBSET_I >>
712 qexists_tac ‘(FSET0 O LIST_REL AB) |==>
713 (((=) |==> (=)) O (AB |==> (=)))’ >> reverse conj_tac
714 >- simp[relationTheory.O_DEF, relationTheory.RSUBSET] >>
715 irule RSUBSET_I >> INTRO FUN_REL_O >>
716 simp[relationTheory.O_DEF] >>
717 qexists_tac ‘set’ >>
718 conj_tac
719 >- (simp[FUN_REL_def, LIST_REL_EL_EQN] >>
720 metis_tac[IN_DEF, MEM_EL, bi_unique_def, left_unique_def,
721 right_unique_def]) >>
722 map_every INTRO [HK_thm2, funQ, idQ, fset0Q] >> conj_tac
723 >- simp[toSet_def, FUN_EQ_THM, fIN_def, IN_DEF] >>
724 simp[FUN_REL_def, fsequiv_def]
725QED
726
727Theorem FINITE_toSet[simp]:
728 !s. FINITE (toSet s)
729Proof
730 ho_match_mp_tac fset_induction >> simp[toSet_def, pred_setTheory.GSPEC_OR]
731QED
732
733Definition fBIGUNION_def:
734 fBIGUNION = ((MAP fset_REP o fset_REP) ---> fset_ABS) FLAT
735End
736
737Theorem Qt_composes:
738 Qt R1 Abs1 Rep1 Tf1 /\ Qt R2 Abs2 Rep2 Tf2 ==>
739 Qt (inv Tf1 O R2 O Tf1) (Abs2 o Abs1) (Rep1 o Rep2) (Tf2 O Tf1)
740Proof
741 simp[Qt_def, relationTheory.inv_DEF, relationTheory.O_DEF, FUN_EQ_THM] >>
742 metis_tac[]
743QED
744
745Theorem MEM_FSET0:
746 FSET0 l fs ==> (!a. MEM a l <=> fIN a fs)
747Proof
748 mp_tac (fIN_relates |> INST_TYPE [beta |-> alpha] |> Q.INST [‘AB’ |-> ‘$=’])>>
749 simp[FUN_REL_def]
750QED
751
752Theorem LIST_REL_FSET0:
753 Qt (LIST_REL fsequiv) (MAP fset_ABS) (MAP fset_REP) (LIST_REL FSET0)
754Proof
755 simp[listQ]
756QED
757
758Theorem LIST_REL_FSET0_Abs:
759 LIST_REL FSET0 ll lfs ==> lfs = MAP fset_ABS ll
760Proof
761 metis_tac[LIST_REL_FSET0, Qt_def]
762QED
763
764Theorem FLAT_relates:
765 (LIST_REL (LIST_REL AB) |==> LIST_REL AB) FLAT FLAT
766Proof
767 simp[FUN_REL_def] >> Induct_on ‘LIST_REL’ >> simp[] >>
768 metis_tac[LIST_REL_APPEND]
769QED
770
771Theorem fBIGUNION_relates[transfer_rule]:
772 (FSET (FSET AB) |==> FSET AB) FLAT fBIGUNION
773Proof
774 simp[Once FSET_AB_eqn, SimpL “FUN_REL”] >>
775 simp[Once FSET_AB_eqn, SimpL “FUN_REL”, SimpR “$O”] >>
776 simp[LIST_REL_O] >>
777 simp[Once FSET_AB_eqn, SimpR “FUN_REL”] >>
778 simp[relationTheory.O_ASSOC] >> irule RSUBSET_I >> INTRO FUN_REL_O >>
779 simp[relationTheory.O_DEF] >>
780 map_every INTRO [FLAT_relates, HK_thm2, fBIGUNION_def, funQ, fset0Q,
781 Qt_composes, fset0Q, listQ, fset0Q] >>
782 rw[FUN_REL_def, relationTheory.O_DEF, relationTheory.inv_DEF,PULL_EXISTS]>>
783 rename [‘fsequiv (FLAT l1) (FLAT l2)’, ‘LIST_REL _ l1 fsl1’,
784 ‘LIST_REL _ l2 fsl2’] >>
785 ‘fsl1 = MAP fset_ABS l1 /\ fsl2 = MAP fset_ABS l2’
786 by metis_tac[LIST_REL_FSET0_Abs] >>
787 fs[fsequiv_def, LIST_TO_SET_MAP, LIST_TO_SET_FLAT] >>
788 simp[Once psEXTENSION, PULL_EXISTS] >>
789 fs[Once psEXTENSION, EQ_IMP_THM, FORALL_AND_THM, PULL_EXISTS,
790 fsequiv_def] >> metis_tac[]
791QED
792
793Theorem rel_setEQ[transfer_simp,simp]:
794 rel_set $= = $=
795Proof
796 simp[FUN_EQ_THM, rel_set_def, IN_DEF] >> metis_tac[]
797QED
798
799Theorem BIGUNION_relates[transfer_rule]:
800 (rel_set (rel_set AB) |==> rel_set AB) BIGUNION BIGUNION
801Proof
802 simp[FUN_REL_def, rel_set_def] >> metis_tac[]
803QED
804
805Theorem left_unique_rel_set[transfer_safe]:
806 left_unique AB ==> left_unique (rel_set AB)
807Proof
808 simp[left_unique_def, rel_set_def] >> rw[] >>
809 simp[psEXTENSION] >> metis_tac[]
810QED
811
812Theorem right_unique_rel_set[transfer_safe]:
813 right_unique AB ==> right_unique (rel_set AB)
814Proof
815 simp[right_unique_def, rel_set_def] >> rw[] >>
816 simp[psEXTENSION] >> metis_tac[]
817QED
818
819Theorem set_BIGUNION:
820 !fss. toSet (fBIGUNION fss) = BIGUNION (toSet (fIMAGE toSet fss))
821Proof
822 xfer_back_tac [] >> simp[LIST_TO_SET_FLAT]
823QED
824
825Theorem toSet_11:
826 !fs1 fs2. (toSet fs1 = toSet fs2) <=> fs1 = fs2
827Proof
828 xfer_back_tac [] >> simp[fsequiv_def]
829QED
830
831Theorem equalityp_relset[transfer_safe]:
832 equalityp AB ==> equalityp (rel_set AB)
833Proof
834 simp[equalityp_def]
835QED
836
837Theorem fIN_IN:
838 !e fs. fIN e fs <=> e IN toSet fs
839Proof
840 xfer_back_tac []
841QED
842
843Theorem set_IMAGE:
844 !f fs. toSet (fIMAGE f fs) = IMAGE f (toSet fs)
845Proof
846 xfer_back_tac [] >> simp[LIST_TO_SET_MAP, psEXTENSION]
847QED
848
849Theorem IN_BIGUNION:
850 fIN e (fBIGUNION fss) = ?fs. fIN fs fss /\ fIN e fs
851Proof
852 simp[fIN_IN, set_BIGUNION, set_IMAGE, PULL_EXISTS] >> metis_tac[]
853QED
854
855Inductive fITSETr:
856 fITSETr f fEMPTY A A /\
857 (!e s A0 A1. fITSETr f s A0 A1 /\ ~fIN e s ==>
858 fITSETr f (fINSERT e s) A0 (f e A1))
859End
860
861val _ = TypeBase.export [
862 TypeBasePure.mk_nondatatype_info
863 (“:'a fset”,
864 {nchotomy = SOME fset_cases,
865 induction = SOME fset_induction,
866 size = NONE,
867 encode=NONE})
868 ]
869
870Theorem CARD_toSet:
871 CARD (toSet s) = fCARD s
872Proof
873 Induct_on`s` \\ gs[toSet_fINSERT, fIN_IN]
874QED
875
876Theorem IN_toSet_fINSERT:
877 x ∈ toSet (fINSERT a s) ⇔ x = a ∨ x ∈ toSet s
878Proof
879 rw[GSYM fIN_IN]
880QED
881
882Theorem fITSETr_total:
883 !s f a0. ?a. fITSETr f s a0 a
884Proof
885 Induct >> metis_tac[fITSETr_rules]
886QED
887
888Theorem DECOMPOSITION:
889 fIN e s <=> ?s0. s = fINSERT e s0 /\ ~fIN e s0
890Proof
891 Induct_on ‘s’ >> simp[] >> rw[] >> eq_tac >> rw[]
892 >- metis_tac[]
893 >- (fs[] >> rename [‘fINSERT e1 (fINSERT e2 ss) = fINSERT e2 _’] >>
894 qexists_tac ‘fINSERT e1 ss’ >> simp[fINSERT_commutes]) >>
895 rename [‘e1 = e2 \/ _’, ‘fINSERT e2 s2 = fINSERT e1 s1’] >>
896 Cases_on ‘e1 = e2’ >> simp[] >>
897 ‘fIN e1 s2’ by (fs[EXTENSION] >> metis_tac[]) >>
898 pop_assum mp_tac >> simp[]
899QED
900
901Theorem fITSETr_functional:
902 (!x y a. f x (f y a) = f y (f x a)) ==>
903 !s a0 a1 a2. fITSETr f s a0 a1 /\ fITSETr f s a0 a2 ==> a1 = a2
904Proof
905 strip_tac >>
906 completeInduct_on ‘fCARD s’ >> fs[PULL_FORALL] >>
907 rpt gen_tac >>
908 Cases_on ‘fCARD s = 0’ >> fs[] >> strip_tac >>
909 ONCE_REWRITE_TAC [fITSETr_cases] >> simp[] >>
910 disch_then $ CONJUNCTS_THEN2
911 (qx_choosel_then [‘e1’, ‘s1’, ‘A1’] strip_assume_tac)
912 (qx_choosel_then [‘e2’, ‘s2’, ‘A2’] strip_assume_tac) >>
913 rw[] >> Cases_on ‘e1 = e2’ >> fs[]
914 >- (‘s1 = s2’ suffices_by metis_tac[DECIDE “x < x + 1”] >>
915 fs[EXTENSION] >> metis_tac[]) >>
916 ‘fIN e1 s2 /\ fIN e2 s1’ by metis_tac[IN_INSERT, EXTENSION] >>
917 ‘?s0. s1 = fINSERT e2 s0 /\ s2 = fINSERT e1 s0 /\ ~fIN e2 s0 /\ ~fIN e1 s0’
918 by (‘?s0. s1 = fINSERT e2 s0 /\ ~fIN e2 s0’ by metis_tac[DECOMPOSITION] >>
919 qexists_tac ‘s0’ >> simp[] >> rw[] >> fs[] >>
920 qpat_x_assum ‘fINSERT _ _ = fINSERT _ _’ mp_tac >>
921 simp[EXTENSION] >> metis_tac[]) >>
922 fs[] >> ‘?a00. fITSETr f s0 a0 a00’ by metis_tac[fITSETr_total] >>
923 ‘fITSETr f (fINSERT e1 s0) a0 (f e1 a00) /\
924 fITSETr f (fINSERT e2 s0) a0 (f e2 a00)’
925 by PROVE_TAC[fITSETr_rules] >>
926 ‘A1 = f e2 a00 /\ A2 = f e1 a00’ suffices_by metis_tac[] >>
927 conj_tac >> first_x_assum irule
928 >- (qexistsl_tac [‘a0’, ‘fINSERT e2 s0’] >> simp[]) >>
929 qexistsl_tac [‘a0’, ‘fINSERT e1 s0’] >> simp[]
930QED
931
932Definition fITSET_def:
933 fITSET f s a0 = @a. fITSETr f s a0 a
934End
935
936Theorem fITSET_EMPTY[simp]:
937 fITSET f fEMPTY a = a
938Proof
939 simp[fITSET_def, Once fITSETr_cases]
940QED
941
942Theorem fITSET_INSERT:
943 (!x y a. f x (f y a) = f y (f x a)) ==>
944 !e s a. fITSET f (fINSERT e s) a = f e (fITSET f (fDELETE e s) a)
945Proof
946 simp[fITSET_def] >> rpt strip_tac >> SELECT_ELIM_TAC >>
947 conj_tac >- metis_tac[fITSETr_total] >> qx_gen_tac ‘a1’ >>
948 SELECT_ELIM_TAC >> conj_tac >- metis_tac[fITSETr_total]>> qx_gen_tac ‘a2’ >>
949 strip_tac >>
950 drule_then (qspec_then ‘e’ mp_tac)(fITSETr_rules |> SPEC_ALL |> CONJUNCT2) >>
951 simp[] >> PROVE_TAC[fITSETr_functional]
952QED
953
954Theorem fITSET_INSERT_tail:
955 (!x y a. f x (f y a) = f y (f x a)) ==>
956 !e s a. fITSET f (fINSERT e s) a = fITSET f (fDELETE e s) (f e a)
957Proof
958 strip_tac >> Induct_on ‘s’ >> rpt strip_tac >- simp[fITSET_INSERT] >>
959 rename [‘fITSET _ (fINSERT e1 (fINSERT e2 _))’] >>
960 Cases_on ‘e1 = e2’ >> simp[] >>
961 ‘fINSERT e1 (fINSERT e2 s) = fINSERT e2 (fINSERT e1 s)’
962 by simp[fINSERT_commutes] >>
963 pop_assum SUBST1_TAC >> simp[Once fITSET_INSERT] >>
964 ‘fDELETE e1 (fINSERT e2 s) = fINSERT e2 (fDELETE e1 s)’
965 by (simp[EXTENSION] >> metis_tac[]) >>
966 pop_assum SUBST1_TAC >> simp[fITSET_INSERT]
967QED
968
969Definition fSUM_IMAGE_def:
970 fSUM_IMAGE f s = fITSET (λe a. f e + a) s 0
971End
972
973Theorem fSUM_IMAGE_THM[simp]:
974 fSUM_IMAGE f fEMPTY = 0 /\
975 fSUM_IMAGE f (fINSERT e A) = f e + fSUM_IMAGE f (fDELETE e A)
976Proof
977 simp[fSUM_IMAGE_def, fITSET_INSERT]
978QED
979
980Theorem fSUM_IMAGE_SUBSET:
981 !A B. (!a. fIN a A ==> fIN a B) ==> fSUM_IMAGE f A <= fSUM_IMAGE f B
982Proof
983 Induct_on ‘B’ >> simp[] >> rw[]
984 >- (Cases_on ‘A’ >> gs[FORALL_AND_THM]) >>
985 reverse $ Cases_on ‘fIN e A’ >> simp[]
986 >- (‘!a. fIN a A ==> fIN a B’ by metis_tac [] >> first_x_assum drule >>
987 simp[]) >>
988 pop_assum (strip_assume_tac o SRULE[Once DECOMPOSITION]) >> simp[] >>
989 first_x_assum irule >> gvs[DISJ_IMP_THM] >> metis_tac[]
990QED
991
992Theorem fSUM_IMAGE_UNION:
993 !A B.
994 fSUM_IMAGE f (fUNION A B) =
995 fSUM_IMAGE f A + fSUM_IMAGE f B - fSUM_IMAGE f (fINTER A B)
996Proof
997 Induct_on ‘A’ >> simp[fUNION_INSERT, fDELETE_UNION] >> rw[] >>
998 reverse $ Cases_on ‘fIN e B’ >> simp[]
999 >- (‘fINTER (fINSERT e A) B = fINTER A B /\
1000 fSUM_IMAGE f (fINTER A B) <= fSUM_IMAGE f A’
1001 suffices_by simp[] >>
1002 conj_tac >- (simp[EXTENSION] >> metis_tac[]) >>
1003 irule fSUM_IMAGE_SUBSET >> simp[]) >>
1004 pop_assum (strip_assume_tac o SRULE[Once DECOMPOSITION]) >>
1005 simp[fINTER_INSERT] >>
1006 rename [‘fINTER A0 B0’] >>
1007 ‘fSUM_IMAGE f (fINTER A0 B0) <= fSUM_IMAGE f A0’ suffices_by simp[] >>
1008 irule fSUM_IMAGE_SUBSET >> simp[]
1009QED
1010
1011Definition fMAX_SET_def:
1012 fMAX_SET s = fITSET MAX s 0
1013End
1014
1015Theorem fIN_fMAX_SET:
1016 !A e. fIN e A ==> e <= fMAX_SET A
1017Proof
1018 Induct >>
1019 simp[fMAX_SET_def, fITSET_INSERT, DISJ_IMP_THM, FORALL_AND_THM,
1020 AC MAX_ASSOC MAX_COMM]
1021QED
1022
1023Theorem fMAX_SET_fIN:
1024 A <> fEMPTY ==> fIN (fMAX_SET A) A
1025Proof
1026 Induct_on ‘A’ >> rw[fMAX_SET_def, fITSET_INSERT, AC MAX_COMM MAX_ASSOC] >>
1027 rw[MAX_DEF] >> Cases_on ‘A’ >> gs[]
1028QED
1029
1030Theorem fMAX_SET_SUBSET:
1031 !A B. (!e. fIN e A ==> fIN e B) ==> fMAX_SET A <= fMAX_SET B
1032Proof
1033 rw[] >> Cases_on ‘A = fEMPTY’ >- simp[fMAX_SET_def] >>
1034 simp[fMAX_SET_fIN, fIN_fMAX_SET]
1035QED
1036
1037Theorem fMAX_SET_THM[simp]:
1038 fMAX_SET fEMPTY = 0 /\
1039 fMAX_SET (fINSERT e A) = MAX e (fMAX_SET A)
1040Proof
1041 simp[fMAX_SET_def, fITSET_INSERT, AC MAX_ASSOC MAX_COMM] >>
1042 rw[MAX_DEF] >> gs[GSYM fMAX_SET_def] >~
1043 [‘fMAX_SET (fDELETE e A) = fMAX_SET A’]
1044 >- (irule LESS_EQUAL_ANTISYM >> conj_tac >> irule fIN_fMAX_SET >~
1045 [‘fIN (fMAX_SET A) (fDELETE e A)’]
1046 >- (simp[] >> irule fMAX_SET_fIN >> strip_tac >> gs[fMAX_SET_def]) >>
1047 ‘!a. fIN a (fDELETE e A) ==> fIN a A’ by simp[] >> pop_assum irule >>
1048 irule fMAX_SET_fIN >> strip_tac >> gs[fMAX_SET_def]) >~
1049 [‘e < fMAX_SET A’, ‘~(e < fMAX_SET (fDELETE e A))’]
1050 >- (gs[NOT_LESS] >> ‘A <> fEMPTY’ by (strip_tac >> gs[fMAX_SET_def]) >>
1051 ‘fIN (fMAX_SET A) A’ by simp[fMAX_SET_fIN] >>
1052 ‘fMAX_SET A <> e’ by simp[] >>
1053 ‘fIN (fMAX_SET A) (fDELETE e A)’ by simp[] >>
1054 ‘fMAX_SET A <= fMAX_SET (fDELETE e A)’ by simp[fIN_fMAX_SET] >> simp[]) >~
1055 [‘e < fMAX_SET (fDELETE e A)’, ‘~(e < fMAX_SET A)’]
1056 >- (gs[NOT_LESS] >> ‘fMAX_SET A < fMAX_SET (fDELETE e A)’ by simp[] >>
1057 pop_assum mp_tac >> simp_tac (srw_ss()) [NOT_LESS] >> irule fMAX_SET_SUBSET >>
1058 simp[])
1059QED
1060
1061(*
1062Definition FSET':
1063 FSET' AB l fs <=> (!a. MEM a l ==> ?b. AB a b /\ fIN b fs) /\
1064 (!b. fIN b fs ==> ?a. AB a b /\ MEM a l)
1065End
1066
1067Theorem fset_repabs =
1068 MATCH_MP R_repabs fset0Q |> SIMP_RULE (srw_ss()) [fsequiv_def]
1069
1070Theorem FSET0:
1071 FSET' $= = FSET0
1072Proof
1073 simp[FSET', FUN_EQ_THM, fIN_def, FSET_def, EQ_IMP_THM] >> rw[fset_repabs] >>
1074 rename [‘fs = fset_ABS l’] >>
1075 ‘?l'. fs = fset_ABS l'’ by metis_tac[fset_ABS_onto] >>
1076 fs[fset_repabs, fsequiv_def, psEXTENSION] >> metis_tac[]
1077QED
1078
1079Definition fSUB_def:
1080 fSUB fs1 fs2 <=> !e. fIN e fs1 ==> fIN e fs2
1081End
1082
1083(* opposite direction doesn't hold:
1084 FSET' AB holds between [a] and set {b1,b2} if AB a b1 & AB a b2 hold
1085 but there's no LIST_REL possible between a and a list that has both
1086 b1 and b2 in it
1087*)
1088Theorem FSET'_decompose:
1089 FSET0 O LIST_REL AB RSUBSET FSET' AB
1090Proof
1091 simp[FSET', FUN_EQ_THM, relationTheory.O_DEF, fIN_def, FSET_def,
1092 relationTheory.RSUBSET, PULL_EXISTS, fset_repabs] >>
1093 simp[LIST_REL_EL_EQN] >> metis_tac[MEM_EL]
1094QED
1095
1096Theorem FSET'_total:
1097 total AB ==> total (FSET' AB)
1098Proof
1099 simp[FSET', total_def, fIN_def, surj_def, bi_unique_def,
1100 right_unique_def] >> rw[] >>
1101 rename [‘MEM _ l ==> _ ’] >>
1102 qexists_tac ‘fset_ABS (MAP (\a. @b. AB a b) l)’ >>
1103 rw[fset_repabs, MEM_MAP, PULL_EXISTS] >> metis_tac[]
1104QED
1105
1106Theorem right_unique_fIN_relates[transfer_rule]:
1107 right_unique AB ==> (AB |==> FSET AB |==> $==>) MEM fIN
1108Proof
1109 simp[FUN_REL_def, FSET_def, fIN_def, PULL_EXISTS, fset_repabs,
1110 right_unique_def] >>
1111 simp[LIST_REL_EL_EQN] >> metis_tac[MEM_EL]
1112QED
1113
1114Theorem IN_BIGUNION:
1115 !x fss. fIN x (fBIGUNION fss) = ?fs. fIN fs fss /\ fIN x fs
1116Proof
1117
1118 xfer_back_tac []
1119*)
1120
1121Definition fromSet_def:
1122 fromSet s = ITSET fINSERT s fEMPTY
1123End
1124
1125Theorem fromSet_EMPTY[simp]:
1126 fromSet {} = fEMPTY
1127Proof
1128 simp[fromSet_def]
1129QED
1130
1131Theorem IN_fromSet:
1132 FINITE s ==> (fIN e (fromSet s) <=> e IN s)
1133Proof
1134 Induct_on ‘FINITE’ >>
1135 simp[pred_setTheory.COMMUTING_ITSET_RECURSES, fINSERT_commutes, fromSet_def,
1136 pred_setTheory.DELETE_NON_ELEMENT]
1137QED
1138
1139Theorem fromSet_INSERT:
1140 FINITE s ==> fromSet (e INSERT s) = fINSERT e (fromSet s)
1141Proof
1142 simp[EXTENSION, IN_fromSet]
1143QED
1144
1145Theorem fromSet_toSet[simp]:
1146 fromSet (toSet s) = s
1147Proof
1148 simp[EXTENSION, IN_fromSet, GSYM fIN_IN]
1149QED
1150
1151Theorem toSet_fromSet:
1152 FINITE s ==> toSet (fromSet s) = s
1153Proof
1154 simp[pred_setTheory.EXTENSION, GSYM fIN_IN, IN_fromSet]
1155QED
1156
1157val fset_QUOTIENT = theorem"fset_QUOTIENT";
1158
1159Theorem fromSet_set:
1160 !l. fromSet (set l) = fset_ABS l
1161Proof
1162 Induct \\ gvs[GSYM fEMPTY_def, fromSet_INSERT]
1163 \\ rw[Once fINSERT_def, fsequiv_def]
1164 \\ AP_TERM_TAC
1165 \\ mp_tac fset_QUOTIENT
1166 \\ rewrite_tac[quotientTheory.QUOTIENT_def] \\ strip_tac
1167 \\ metis_tac[fsequiv_def]
1168QED
1169
1170Theorem toSet_fset_ABS:
1171 !l. toSet (fset_ABS l) = set l
1172Proof
1173 gen_tac \\
1174 qspec_then`l`(SUBST1_TAC o SYM o Q.AP_TERM`toSet`)fromSet_set
1175 \\ irule toSet_fromSet
1176 \\ rw[]
1177QED
1178
1179Theorem toSet_fUNION[simp]:
1180 toSet (fUNION s1 s2) = (toSet s1) UNION (toSet s2)
1181Proof
1182 rw[pred_setTheory.EXTENSION, GSYM fIN_IN]
1183QED
1184
1185Theorem toSet_Qt:
1186 Qt (λx y. FINITE x /\ x = y) fromSet toSet (λs fs. s = toSet fs)
1187Proof
1188 simp[Qt_def] >> ntac 2 (ONCE_REWRITE_TAC [FUN_EQ_THM]) >>
1189 simp[relationTheory.O_DEF] >> rw[EQ_IMP_THM] >~
1190 [‘s = toSet _’]
1191 >- (irule_at Any (GSYM toSet_fromSet) >> simp[]) >>
1192 simp[]
1193QED
1194
1195Definition sfSETREL_def:
1196 sfSETREL AB s fs <=>
1197 (!a. a IN s ==> ?b. fIN b fs /\ AB a b) /\
1198 (!b. fIN b fs ==> ?a. a IN s /\ AB a b)
1199End
1200
1201Theorem fIN_sfSETREL:
1202 bi_unique AB ==>
1203 (AB |==> sfSETREL AB |==> (=)) (IN) fIN
1204Proof
1205 simp[FUN_REL_def, sfSETREL_def, bi_unique_def, left_unique_def,
1206 right_unique_def] >>
1207 metis_tac[]
1208QED
1209
1210Theorem fINSERT_sfSETREL:
1211 (AB |==> sfSETREL AB |==> sfSETREL AB) (INSERT) fINSERT
1212Proof
1213 simp[FUN_REL_def, sfSETREL_def, DISJ_IMP_THM, FORALL_AND_THM] >>
1214 rw[] >> metis_tac[]
1215QED
1216
1217Theorem fUNION_sfSETREL:
1218 (sfSETREL AB |==> sfSETREL AB |==> sfSETREL AB) (UNION) fUNION
1219Proof
1220 simp[FUN_REL_def, sfSETREL_def] >> metis_tac[]
1221QED
1222
1223Theorem MEM_fset_REP:
1224 MEM x (fset_REP fs) <=> fIN x fs
1225Proof
1226 rw[fIN_def]
1227QED
1228
1229Theorem fset_ABS_MAP:
1230 fset_ABS (MAP f l) = fIMAGE f (fset_ABS l)
1231Proof
1232 rw[EXTENSION, fIN_IN, toSet_fset_ABS, MEM_MAP]
1233 \\ metis_tac[]
1234QED
1235
1236Theorem fset_REP_fEMPTY[simp]:
1237 fset_REP fEMPTY = []
1238Proof
1239 rw[rich_listTheory.NIL_NO_MEM, MEM_fset_REP]
1240QED
1241
1242Theorem fIN_fset_ABS:
1243 fIN x (fset_ABS l) <=> MEM x l
1244Proof
1245 rw[fIN_def]
1246 \\ mp_tac fset_QUOTIENT
1247 \\ rewrite_tac[quotientTheory.QUOTIENT_def,fsequiv_def]
1248 \\ rpt strip_tac
1249 \\ `set (fset_REP (fset_ABS l)) = set l`
1250 suffices_by (
1251 rewrite_tac[pred_setTheory.EXTENSION]
1252 \\ metis_tac[] )
1253 \\ asm_simp_tac std_ss []
1254QED
1255
1256Theorem fBIGUNION_fset_ABS_FOLDL_aux[local]:
1257 !l s. FOLDL fUNION s l = fUNION s (fBIGUNION (fset_ABS l))
1258Proof
1259 Induct \\ rw[fBIGUNION_def, GSYM fEMPTY_def]
1260 \\ rw[GSYM fUNION_ASSOC] \\ AP_TERM_TAC
1261 \\ rw[EXTENSION]
1262 \\ qmatch_goalsub_abbrev_tac`_ \/ fIN e s <=> fIN e hs`
1263 \\ `hs = fUNION h s`
1264 by (
1265 rw[Once (GSYM toSet_11)]
1266 \\ rw[Abbr`hs`, Abbr`s`, toSet_fset_ABS]
1267 \\ rw[pred_setTheory.EXTENSION, MEM_FLAT, PULL_EXISTS, MEM_MAP]
1268 \\ rw[MEM_fset_REP, fIN_fset_ABS, GSYM fIN_IN]
1269 \\ metis_tac[] )
1270 \\ rw[]
1271QED
1272
1273Theorem fBIGUNION_fset_ABS_FOLDL:
1274 fBIGUNION (fset_ABS l) = FOLDL fUNION fEMPTY l
1275Proof
1276 rw[fBIGUNION_fset_ABS_FOLDL_aux]
1277QED
1278
1279
1280(* ----------------------------------------------------------------------
1281 Finite sets as a bounded natural functor, so that a datatype
1282 specification can recurse through one: fIMAGE is the map, toSet the
1283 set function, rel_set on the elements the relator, and a finite set
1284 holds no more atoms than there are numbers.
1285 ---------------------------------------------------------------------- *)
1286
1287fun bnm s : KernelSig.kernelname = {Thy = "finite_set", Name = s}
1288
1289Definition fsetREL_def:
1290 fsetREL AB fs1 fs2 <=> rel_set AB (toSet fs1) (toSet fs2)
1291End
1292
1293Theorem fsetMap_ID:
1294 fIMAGE (I:'a1 -> 'a1) = (I : 'a1 fset -> 'a1 fset)
1295Proof
1296 simp[FUN_EQ_THM]
1297QED
1298
1299Theorem fsetMap_O:
1300 fIMAGE (f1:'c1 -> 'd1) o fIMAGE (g1:'a1 -> 'c1) = fIMAGE (f1 o g1)
1301Proof
1302 simp[FUN_EQ_THM, fIMAGE_COMPOSE]
1303QED
1304
1305Theorem fsetMapIMAGE1:
1306 !(f1:'a1 -> 'c1) s. toSet (fIMAGE f1 s) = IMAGE f1 (toSet s)
1307Proof
1308 simp[toSet_fIMAGE]
1309QED
1310
1311Theorem fsetMapCONG:
1312 (!a1. a1 IN toSet (s:'a1 fset) ==> (f1:'a1 -> 'c1) a1 = g1 a1) ==>
1313 fIMAGE f1 s = fIMAGE g1 s
1314Proof
1315 strip_tac >> simp[GSYM toSet_11, toSet_fIMAGE] >>
1316 irule pred_setTheory.IMAGE_CONG >> simp[]
1317QED
1318
1319Theorem fset_bnd1:
1320 !s : 'a1 fset. toSet s <<= univ(:num)
1321Proof
1322 gen_tac >> ONCE_REWRITE_TAC[cardinalityCoreTheory.cardleq_lteq] >>
1323 disj1_tac >> simp[GSYM cardinalityCoreTheory.FINITE_CARD_LT]
1324QED
1325
1326Theorem fset_wit1:
1327 !a1:'a1. toSet (K fEMPTY a1 : 'a1 fset) SUBSET {}
1328Proof
1329 simp[]
1330QED
1331
1332Theorem fset_inh1:
1333 !v:'a1. v IN toSet (combin$C fINSERT fEMPTY v)
1334Proof
1335 simp[toSet_fINSERT]
1336QED
1337
1338val _ = bnfBase.updateDB (
1339 {Thy = "finite_set", Name = "fset"},
1340 bnfBase.bI {
1341 canontype = “:'a1 fset”,
1342
1343 map = “finite_set$fIMAGE : ('a1 -> 'c1) -> 'a1 fset -> 'c1 fset”,
1344 set = [“finite_set$toSet : 'a1 fset -> 'a1 set”],
1345 mapID = bnm "fsetMap_ID",
1346 mapO = bnm "fsetMap_O",
1347 mapIMAGE = [bnm "fsetMapIMAGE1"],
1348 mapCONG = bnm "fsetMapCONG",
1349
1350 relator = “finite_set$fsetREL : ('a1 -> 'c1 -> bool) ->
1351 'a1 fset -> 'c1 fset -> bool”,
1352 bnd = “univ(:num)”,
1353 bndthms = [bnm "fset_bnd1"],
1354
1355 wits = [(“K fEMPTY : 'a1 -> 'a1 fset”, bnm "fset_wit1")],
1356 inhabits = [(“combin$C fINSERT fEMPTY : 'a1 -> 'a1 fset”,
1357 bnm "fset_inh1")]
1358 }
1359)