finite_setScript.sml

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