bnfPrelimsScript.sml

1Theory bnfPrelims[bare]
2Ancestors sum pair option pred_set cardinalityCore quotient basicSize
3Libs HolKernel Parse boolLib BasicProvers simpLib TotalDefn[qualified] QLib
4     metisLib
5
6(* cardinalityCoreTheory makes no grammar of its own -- it is every
7   theory's ancestor through the datatype package, and the ASCII
8   forms are tokens wherever they reach.  What this theory writes
9   it sets up for itself. *)
10Overload "<<="[local] = “cardleq”
11Overload cardlt[local] = “λs1 s2. ¬cardleq s2 s1”
12val _ = temp_set_fixity "<</=" (Infix(NONASSOC, 450));
13val _ = Unicode.temp_unicode_version {u = UTF8.chr 0x227A, tmnm = "<</="};
14Overload "<</="[local] = “cardlt”
15val _ = temp_set_fixity "=~" (Infix(NONASSOC, 450));
16val _ = Unicode.temp_unicode_version {u = UTF8.chr 0x2248, tmnm = "=~"};
17Overload "=~"[local] = “cardeq”
18Overload cardlt[local] = “λs1 s2. ¬cardleq s2 s1”
19val _ = temp_set_fixity "<</=" (Infix(NONASSOC, 450));
20val _ = Unicode.temp_unicode_version {u = UTF8.chr 0x227A, tmnm = "<</="};
21Overload "<</="[local] = “cardlt”
22val _ = temp_set_fixity "=~" (Infix(NONASSOC, 450));
23val _ = Unicode.temp_unicode_version {u = UTF8.chr 0x2248, tmnm = "=~"};
24Overload "=~"[local] = “cardeq”
25
26
27
28fun sum_nm s : KernelSig.kernelname = {Thy = "sum", Name = s}
29fun pair_nm s : KernelSig.kernelname = {Thy = "pair", Name = s}
30fun pnm s : KernelSig.kernelname = {Thy = "bnfPrelims", Name = s}
31val T = {Name = "TRUTH", Thy = "bool"} (* placeholder *)
32
33(* ----------------------------------------------------------------------
34    some bossLib emulation
35   ---------------------------------------------------------------------- *)
36
37fun simp ths g ctxt = simpLib.ASM_SIMP_TAC (srw_ss_of ctxt) ths g ctxt
38val metis_tac = METIS_TAC
39val op >~ = Q.>~
40
41(* ----------------------------------------------------------------------
42    Utility results that all constructions will likely use
43   ---------------------------------------------------------------------- *)
44
45Theorem IMAGE_o_equal:
46  IMAGE f o (=) = (=) o f
47Proof
48  simp[FUN_EQ_THM, IN_DEF, EQ_SYM_EQ]
49QED
50
51Theorem KlamF:
52  K (λx. F) = K {}
53Proof
54  simp[FUN_EQ_THM]
55QED
56
57Theorem o_INTRO:
58  (∀x. f (g x) = h x) ⇔ f o g = h
59Proof
60  simp[combinTheory.o_DEF, FUN_EQ_THM]
61QED
62
63Theorem UNION_CARDLE:
64  INFINITE CC ∧ A ≼ CC ∧ B ≼ CC ⇒ A ∪ B ≼ CC
65Proof
66  strip_tac >>
67  resolve_then Any irule UNION_LE_ADD_C cardleq_TRANS >>
68  irule CARD_ADD2_ABSORB_LE >> simp[]
69QED
70
71Theorem IN_equal:
72  x ∈ (=) y ⇔ x = y
73Proof
74  simp[IN_DEF, EQ_SYM_EQ]
75QED
76
77(* not generally safe as an unbounded rewrite *)
78Theorem EQ_SING:
79  $= x = {x}
80Proof
81  simp[EXTENSION, IN_equal]
82QED
83
84Theorem SING_CARDLE:
85  ({x} ≼ A ⇔ A ≠ ∅) ∧ ((=) x ≼ A ⇔ A ≠ ∅)
86Proof
87  ‘(=) x = {x}’ by MATCH_ACCEPT_TAC EQ_SING >> simp[] >>
88  simp[EQ_IMP_THM, INJ_DEF, cardleq_def, GSYM MEMBER_NOT_EMPTY] >>
89  rpt strip_tac >~
90  [‘∃f. f x ∈ A’, ‘a ∈ A (* a *)’]
91  >- (qexists_tac ‘K a’ >> simp[]) >>
92  first_assum $ irule_at Any
93QED
94
95Theorem IMAGE_KEMPTY_CARDLE:
96  IMAGE (K ∅) A ≼ B ⇔ A = ∅ ∨ B ≠ ∅
97Proof
98  simp[EQ_IMP_THM, DISJ_IMP_THM] >> Cases_on ‘A = ∅’ >> simp[] >>
99  Cases_on ‘B = ∅’ >> simp[] >>
100  ‘IMAGE (K ∅) A = {∅}’
101    by (simp[Once EXTENSION] >> simp[EQ_IMP_THM, PULL_EXISTS] >>
102        RULE_ASSUM_TAC (REWRITE_RULE[GSYM MEMBER_NOT_EMPTY]) >>
103        simp[]) >>
104  simp[SING_CARDLE]
105QED
106
107Theorem UNIQUE_SKOLEM:
108  (∀x. ∃!y. P x y) ⇔ ∃!f. ∀x. P x (f x)
109Proof
110  eq_tac >> simp[EXISTS_UNIQUE_THM] >> rpt strip_tac
111  >- (qexists_tac ‘λx. @y. P x y’ >> simp[] >> gen_tac >> SELECT_ELIM_TAC >>
112      METIS_TAC[])
113  >- (simp[FUN_EQ_THM] >> METIS_TAC[])
114  >- METIS_TAC[]
115  >- (rename [‘P x a’, ‘P x b’, ‘a = b’] >>
116      Cases_on ‘f x = a’
117      >- (pop_assum (SUBST_ALL_TAC o SYM) >>
118          first_x_assum $ qspecl_then [‘f’, ‘f (| x |-> b |)’] mp_tac >>
119          simp[combinTheory.APPLY_UPDATE_THM] >>
120          disch_then irule >> METIS_TAC[]) >>
121      first_x_assum $ qspecl_then [‘f(|x|->a|)’, ‘f’] mp_tac >>
122      simp[combinTheory.APPLY_UPDATE_THM, FUN_EQ_THM] >> METIS_TAC[])
123QED
124
125Overload BIMG = “(o) BIGUNION o IMAGE”
126
127Theorem BIMG_EQUAL:
128  BIMG $= = I
129Proof
130  ONCE_REWRITE_TAC[FUN_EQ_THM] >>
131  simp[Once EXTENSION, PULL_EXISTS, IN_equal]
132QED
133
134Theorem BIMG_EQUAL_L:
135  BIGUNION o IMAGE $= o f = f
136Proof
137  simp[Once FUN_EQ_THM] >>
138  simp[Once EXTENSION, PULL_EXISTS, IN_equal]
139QED
140
141Theorem BIMG_K0:
142  BIMG (K ∅) = K ∅
143Proof
144  simp[Once FUN_EQ_THM] >> qx_gen_tac ‘A’ >> Cases_on ‘A = {}’ >>
145  simp[EXTENSION] >> METIS_TAC[MEMBER_NOT_EMPTY]
146QED
147
148Theorem BIMG_IMAGE:
149  BIMG (λx. IMAGE f (g x)) A = IMAGE f (BIMG g A)
150Proof
151  simp[Once EXTENSION, PULL_EXISTS] >> METIS_TAC[]
152QED
153
154Theorem SKg_thm:
155  S (K v) g = v o g
156Proof
157  simp[FUN_EQ_THM]
158QED
159
160Theorem UNION_EMPTY1:
161  (UNION) {} = I
162Proof
163  simp[Once FUN_EQ_THM]
164QED
165
166Theorem BIMG_IMAGEo:
167  BIMG (IMAGE f o g) = IMAGE f o BIMG g
168Proof
169  CONV_TAC (ONCE_REWRITE_CONV [FUN_EQ_THM]) >>
170  simp[Once EXTENSION, PULL_EXISTS, AC CONJ_ASSOC CONJ_COMM] >>
171  METIS_TAC[]
172QED
173
174Theorem IMAGE_IMAGE_lo:
175  (f o IMAGE g) o IMAGE h = f o IMAGE (g o h)
176Proof
177  simp[FUN_EQ_THM, GSYM IMAGE_o]
178QED
179
180Theorem IMAGE_IMAGE_o = REWRITE_RULE [GSYM combinTheory.o_ASSOC] IMAGE_IMAGE_lo
181
182Theorem IMAGE_IMAGE_ro:
183  IMAGE g o (IMAGE h o f) = IMAGE (g o h) o f
184Proof
185  simp[FUN_EQ_THM, PULL_EXISTS]
186QED
187
188Theorem BIGUNION_o_IMAGE_IMAGE:
189  BIGUNION o IMAGE (IMAGE f o g) = IMAGE f o BIGUNION o IMAGE g
190Proof
191  simp[Once FUN_EQ_THM]>> simp[Once EXTENSION, PULL_EXISTS] >>
192  metis_tac[]
193QED
194
195Theorem BIGUNION_o_IMAGE_IMAGEr:
196  BIGUNION o (IMAGE (IMAGE f o g) o h) = IMAGE f o BIGUNION o IMAGE g o h
197Proof
198  simp[Once FUN_EQ_THM]>> simp[Once EXTENSION, PULL_EXISTS] >>
199  metis_tac[]
200QED
201
202Theorem IMAGE_BIGUNIONo:
203  BIGUNION (IMAGE (IMAGE f o h) A) = IMAGE f (BIGUNION (IMAGE h A))
204Proof
205  simp[Once EXTENSION, PULL_EXISTS, AC CONJ_ASSOC CONJ_COMM] >>
206  metis_tac[]
207QED
208
209
210(* ----------------------------------------------------------------------
211    Results supporting the compositional derivation of a composite
212    functor's nonemptiness witnesses, and of the fact that each of its
213    arguments is inhabited.
214
215    A witness takes one argument per genuine type variable and its
216    theorem bounds each of the composite's set functions either by ∅ (the
217    witness didn't need that argument) or by the singleton of the
218    argument it was given.  So the lemmas below are stated with an
219    arbitrary bounding set: each says how bounds on a node's parts bound
220    the whole, and the bound only becomes a singleton at the leaf where
221    the argument itself sits.
222   ---------------------------------------------------------------------- *)
223
224Theorem K0_SUBSET:
225  ∀W x:'b. (K ∅ : 'b -> 'a set) x ⊆ W
226Proof
227  simp[]
228QED
229
230Theorem EQ_SUBSET:
231  ∀a:'a. $= a ⊆ {a}
232Proof
233  simp[EQ_SING]
234QED
235
236Theorem EMPTY_ALL:
237  ∀(s:'b -> 'a set) W. ∀w. w ∈ (∅ : 'b set) ⇒ s w ⊆ W
238Proof
239  simp[]
240QED
241
242Theorem SING_ALL:
243  ∀(s:'b -> 'a set) a W. s a ⊆ W ⇒ ∀w. w ∈ {a} ⇒ s w ⊆ W
244Proof
245  simp[]
246QED
247
248Theorem BIMGo_SUBSET:
249  ∀s st x V W. st x ⊆ V ∧ (∀w. w ∈ V ⇒ s w ⊆ W) ⇒ (BIMG s o st) x ⊆ W
250Proof
251  simp[PULL_EXISTS, SUBSET_DEF] >> metis_tac[]
252QED
253
254Theorem LU_SUBSET:
255  ∀a b x W. a x ⊆ W ∧ b x ⊆ W ⇒ S ($UNION o a) b x ⊆ W
256Proof
257  simp[combinTheory.S_THM]
258QED
259
260Theorem EQ_IN:
261  ∀v:'a. v ∈ $= v
262Proof
263  simp[IN_equal]
264QED
265
266Theorem BIMGo_IN:
267  ∀s st x t v. t ∈ st x ∧ v ∈ s t ⇒ v ∈ (BIMG s o st) x
268Proof
269  simp[PULL_EXISTS] >> metis_tac[]
270QED
271
272Theorem LU_IN1:
273  ∀a b x v. v ∈ a x ⇒ v ∈ S ($UNION o a) b x
274Proof
275  simp[combinTheory.S_THM]
276QED
277
278Theorem LU_IN2:
279  ∀a b x v. v ∈ b x ⇒ v ∈ S ($UNION o a) b x
280Proof
281  simp[combinTheory.S_THM]
282QED
283
284(* ----------------------------------------------------------------------
285    record the sum type's Bounded Natural Functor nature
286   ---------------------------------------------------------------------- *)
287
288Theorem sumMap_def[unlisted] =
289        SUM_MAP_def
290        |> INST_TYPE [alpha |-> “:'a1”, beta |-> “:'a2”,
291                      gamma |-> “:'c1”, delta |-> “:'c2”]
292
293Theorem sumMap_ID[unlisted] =
294        SUM_MAP_I
295        |> INST_TYPE [alpha |-> “:'a1”, beta |-> “:'a2”]
296
297Theorem sumMap_O[unlisted] =
298        SUM_MAP_o
299        |> INST_TYPE [alpha |-> “:'a1”, beta |-> “:'a2”,
300                      gamma |-> “:'d1”, delta |-> “:'d2”,
301                      “:'e” |-> “:'c1”, “:'f” |-> “:'c2”
302                     ]
303        |> Q.INST [‘f’ |-> ‘f1’, ‘g’ |-> ‘f2’,
304                   ‘h’ |-> ‘g1’, ‘k’ |-> ‘g2’]
305
306Theorem sumMapIMAGE1:
307  ∀f1 f2 s.
308    setL (SUM_MAP (f1:'a1 -> 'c1) (f2:'a2 -> 'c2) (s:'a1 + 'a2)) =
309    IMAGE f1 (setL s)
310Proof
311  GEN_TAC >> GEN_TAC >> Cases_on ‘s’ >>
312  SIMP_TAC (srw_ss()) [EXTENSION]
313QED
314
315Theorem sumMapIMAGE2:
316  ∀f1 f2 s.
317    setR (SUM_MAP (f1:'a1 -> 'c1) (f2:'a2 -> 'c2) (s:'a1 + 'a2)) =
318    IMAGE f2 (setR s)
319Proof
320  GEN_TAC >> GEN_TAC >> Cases_on ‘s’ >>
321  SIMP_TAC (srw_ss()) [EXTENSION]
322QED
323
324Theorem sumMapCONG =
325        sumTheory.SUM_MAP_CONG
326          |> INST_TYPE [alpha |-> “:'a1”, beta |-> “:'a2”,
327                        gamma |-> “:'c1”, delta |-> “:'c2”]
328
329Theorem sum_bnd1:
330  ∀s : 'a + 'b. setL s ≼ univ(:num)
331Proof
332  GEN_TAC >> Cases_on ‘s’ >> simp[cardleq_def, INJ_DEF]
333QED
334
335Theorem sum_bnd2:
336  ∀s : 'a + 'b. setR s ≼ univ(:num)
337Proof
338  GEN_TAC >> Cases_on ‘s’ >> simp[cardleq_def, INJ_DEF]
339QED
340
341Theorem sum_wit1:
342  ∀(a1:'a1) (a2:'a2).
343    setL ((K o INL) a1 a2 : 'a1 + 'a2) ⊆ {a1} ∧
344    setR ((K o INL) a1 a2 : 'a1 + 'a2) ⊆ ∅
345Proof
346  simp[SUBSET_DEF, EXTENSION, IN_DEF]
347QED
348
349Theorem sum_wit2:
350  ∀(a1:'a1) (a2:'a2).
351    setL (K INR a1 a2 : 'a1 + 'a2) ⊆ ∅ ∧
352    setR (K INR a1 a2 : 'a1 + 'a2) ⊆ {a2}
353Proof
354  simp[SUBSET_DEF, EXTENSION, IN_DEF]
355QED
356
357Theorem sum_inh1:
358  ∀v:'a1. v ∈ setL (INL v : 'a1 + 'a2)
359Proof
360  simp[SUBSET_DEF, EXTENSION, IN_DEF]
361QED
362
363Theorem sum_inh2:
364  ∀v:'a2. v ∈ setR (INR v : 'a1 + 'a2)
365Proof
366  simp[SUBSET_DEF, EXTENSION, IN_DEF]
367QED
368
369val _ = bnfBase.updateDB (
370  {Name = "sum", Thy = "sum"},
371  bnfBase.bI {
372    bnd = “UNIV : num set”,
373    bndthms = [pnm "sum_bnd1", pnm "sum_bnd2"],
374    canontype = “:'a1 + 'a2”,
375
376    map = “SUM_MAP : ('a1 -> 'c1) -> ('a2 -> 'c2) -> 'a1 + 'a2 -> 'c1 + 'c2”,
377    mapID = pnm "sumMap_ID",
378    mapO = pnm "sumMap_O",
379    mapIMAGE = [pnm "sumMapIMAGE1", pnm "sumMapIMAGE2"],
380    mapCONG = pnm "sumMapCONG",
381
382    relator = “SUM_REL : ('a1 -> 'c1 -> bool) -> ('a2 -> 'c2 -> bool) ->
383                         'a1 + 'a2 -> 'c1 + 'c2 -> bool”,
384    set = [“setL : 'a1 + 'a2 -> 'a1 set”, “setR : 'a1 + 'a2 -> 'a2 set”],
385
386    wits = [(“(K o INL) : 'a1 -> 'a2 -> 'a1 + 'a2”, pnm "sum_wit1"),
387            (“K INR : 'a1 -> 'a2 -> 'a1 + 'a2”, pnm "sum_wit2")],
388    inhabits = [(“INL : 'a1 -> 'a1 + 'a2”, pnm "sum_inh1"),
389                (“INR : 'a2 -> 'a1 + 'a2”, pnm "sum_inh2")]
390  }
391)
392
393(* ----------------------------------------------------------------------
394    record the pair type's Bounded Natural Functor nature
395   ---------------------------------------------------------------------- *)
396
397Theorem pairMap_ID = PAIR_MAP_I |> INST_TYPE [alpha |-> “:'a1”, beta |-> “:'a2”]
398
399Theorem pairMap_O:
400  ((f1:'c1 -> 'd1) ## (f2 : 'c2 -> 'd2)) o
401  ((g1:'a1 -> 'c1) ## (g2 : ('a2 -> 'c2))) =
402  ((f1 o g1) ## (f2 o g2))
403Proof
404  simp[FUN_EQ_THM] >> Cases >> simp[]
405QED
406
407Theorem pairMapIMAGE1:
408  ∀f1 f2 p. setFST (((f1 : 'a1 -> 'c1) ## (f2 : 'a2 -> 'c2)) p) =
409            IMAGE f1 (setFST p)
410Proof
411  Cases_on ‘p’ >> simp[PAIR_MAP_SET, EXTENSION, EQ_SYM_EQ]
412QED
413
414Theorem pairMapIMAGE2:
415  ∀f1 f2 p. setSND (((f1 : 'a1 -> 'c1) ## (f2 : 'a2 -> 'c2)) p) =
416            IMAGE f2 (setSND p)
417Proof
418  Cases_on ‘p’ >> simp[PAIR_MAP_SET, EXTENSION, EQ_SYM_EQ]
419QED
420
421Theorem pairMapCONG:
422  (∀a1:'a1. a1 ∈ setFST p ⇒ (f1 : 'a1 -> 'c1) a1 = g1 a1) ∧
423  (∀a2:'a2. a2 ∈ setSND p ⇒ (f2 : 'a2 -> 'c2) a2 = g2 a2) ⇒
424  (f1 ## f2) p = (g1 ## g2) p
425Proof
426  Cases_on ‘p’ >> simp[]
427QED
428
429Theorem pair_bnd1:
430  ∀p : 'a1 # 'a2. setFST p ≼ univ(:num)
431Proof
432  Cases >> simp[cardleq_def, INJ_DEF]
433QED
434
435Theorem pair_bnd2:
436  ∀p : 'a1 # 'a2. setSND p ≼ univ(:num)
437Proof
438  Cases >> simp[cardleq_def, INJ_DEF]
439QED
440
441Theorem pair_wit1:
442  ∀(a1:'a1) (a2:'a2). setFST ($, a1 a2) ⊆ {a1} ∧ setSND ($, a1 a2) ⊆ {a2}
443Proof
444  simp[SUBSET_DEF, EXTENSION, IN_DEF]
445QED
446
447Theorem pair_inh1:
448  ∀v:'a1. v ∈ setFST (flip $, (ARB:'a2) v)
449Proof
450  simp[SUBSET_DEF, EXTENSION, IN_DEF]
451QED
452
453Theorem pair_inh2:
454  ∀v:'a2. v ∈ setSND ($, (ARB:'a1) v)
455Proof
456  simp[SUBSET_DEF, EXTENSION, IN_DEF]
457QED
458
459val _ = bnfBase.updateDB (
460  {Thy = "pair", Name = "prod"},
461  bnfBase.bI {
462    canontype = “:'a1 # 'a2”,
463
464    map = “pair$## : ('a1 -> 'c1) -> ('a2 -> 'c2) -> 'a1 # 'a2 -> 'c1 # 'c2”,
465    set = [“setFST : 'a1 # 'a2 -> 'a1 set”, “setSND : 'a1 # 'a2 -> 'a2 set”],
466    mapID = pnm "pairMap_ID",
467    mapO = pnm "pairMap_O",
468    mapIMAGE = [pnm "pairMapIMAGE1", pnm "pairMapIMAGE2"],
469    mapCONG = pnm "pairMapCONG",
470    relator = “pair$RPROD : ('a1 -> 'c1 -> bool) -> ('a2 -> 'c2 -> bool) ->
471                            ('a1 # 'a2 -> 'c1 # 'c2 -> bool)”,
472    bnd = “univ(:num)”,
473    bndthms = [pnm "pair_bnd1", pnm "pair_bnd2"],
474
475    wits = [(“$, : 'a1 -> 'a2 -> 'a1 # 'a2”, pnm "pair_wit1")],
476    inhabits = [(“flip $, (ARB:'a2) : 'a1 -> 'a1 # 'a2”, pnm "pair_inh1"),
477                (“$, (ARB:'a1) : 'a2 -> 'a1 # 'a2”, pnm "pair_inh2")]
478  }
479)
480
481(* ----------------------------------------------------------------------
482    record the function type's Bounded Natural Functor nature
483      (in its 2nd arg, the range)
484   ---------------------------------------------------------------------- *)
485
486Overload fmap[local,inferior] = “$o”
487Overload fset[local,inferior] =
488  “combin$C IMAGE univ(:'b1) : ('b1 -> 'a1) -> 'a1 set”
489Overload frel[local,inferior] =
490  “quotient$===> $= : ('a1 -> 'c1 -> bool) ->
491                      (('b1 -> 'a1) -> ('b1 -> 'c1) -> bool)”
492Theorem funMap_ID:
493  fmap (I:'a1 -> 'a1) = I : ('b1 -> 'a1) -> ('b1 -> 'a1)
494Proof
495  simp[FUN_EQ_THM]
496QED
497
498Theorem funMap_O:
499  fmap (f1:'c1 -> 'd1) o fmap (g1:'a1 -> 'c1) =
500  fmap (f1 o g1) : ('b1 -> 'a1) -> ('b1 -> 'd1)
501Proof
502  simp[FUN_EQ_THM]
503QED
504
505Theorem funMapIMAGE1:
506  ∀(f : 'a1 -> 'c1) (fn : 'b1 -> 'a1). fset (fmap f fn) = IMAGE f (fset fn)
507Proof
508  simp[EXTENSION, PULL_EXISTS]
509QED
510
511Theorem funMapCONG:
512  (∀a1. a1 ∈ fset (fn : 'b1 -> 'a1) ⇒ ((f1 : 'a1 -> 'c1) a1 = g1 a1)) ⇒
513  fmap f1 fn = fmap g1 fn
514Proof
515  simp[EXTENSION, PULL_EXISTS, FUN_EQ_THM]
516QED
517
518Theorem fun_bnd1:
519  ∀f : 'b1 -> 'a1. fset f ≼ univ(:'b1)
520Proof
521  simp[cardleq_def] >> gen_tac >> irule SURJ_IMP_INJ >>
522  irule_at Any SURJ_IMAGE
523QED
524
525Theorem fun_wit1:
526  ∀a1:'a1. fset (K a1 : 'b1 -> 'a1) ⊆ {a1}
527Proof
528  simp[SUBSET_DEF, PULL_EXISTS, IN_DEF]
529QED
530
531Theorem fun_inh1:
532  ∀v:'a1. v ∈ fset (K v : 'b1 -> 'a1)
533Proof
534  simp[SUBSET_DEF, EXTENSION, IN_DEF]
535QED
536
537val _ = bnfBase.updateDB (
538  {Thy = "min", Name = "fun"},
539  bnfBase.bI {
540    canontype = “:'b1 -> 'a1”,
541    map = “combin$o : ('a1 -> 'c1) -> ('b1 -> 'a1) -> ('b1 -> 'c1)”,
542    set = [“fset: ('b1 -> 'a1) -> 'a1 set”],
543    mapID = pnm "funMap_ID",
544    mapO = pnm "funMap_O",
545    mapIMAGE = [pnm "funMapIMAGE1"],
546    mapCONG = pnm "funMapCONG",
547    relator = “quotient$===> $= : ('a1 -> 'c1 -> bool) ->
548                                  (('b1 -> 'a1) -> ('b1 -> 'c1) -> bool)”,
549    bnd = “univ(:'b1)”,
550    bndthms = [pnm "fun_bnd1"],
551
552    wits = [(“K : 'a1 -> 'b1 -> 'a1”, pnm "fun_wit1")],
553    inhabits = [(“K : 'a1 -> 'b1 -> 'a1”, pnm "fun_inh1")]
554  }
555)
556
557Theorem frel_thm[local]:
558  frel (R:'a1 -> 'a2 -> bool) (f1:'b1 -> 'a1) (f2:'b1 -> 'a2) ⇔
559    ∃f. f1 = fmap FST f ∧ f2 = fmap SND f ∧
560        ∀x y. (x,y) ∈ fset f ⇒ R x y
561Proof
562  simp[FUN_REL, PULL_EXISTS] >> iff_tac
563  >- (strip_tac >> Q.EXISTS_TAC ‘λb. (f1 b, f2 b)’ >> simp[FUN_EQ_THM]) >>
564  SRW_TAC[][combinTheory.o_DEF] >> simp[] >> Q.RENAME_TAC [‘FST (f b)’] >>
565  Cases_on ‘f b’ >> simp[] >> first_x_assum irule >>
566  first_x_assum (irule_at Any o SYM)
567QED
568
569(* ----------------------------------------------------------------------
570    record the option type's Bounded Natural Functor nature
571   ---------------------------------------------------------------------- *)
572
573Theorem optMap_ID:
574  OPTION_MAP (I:'a1 -> 'a1) = I : 'a1 option -> 'a1 option
575Proof
576  simp[FUN_EQ_THM]
577QED
578
579Theorem optMap_O:
580  OPTION_MAP (f1:'c1 -> 'd1) o OPTION_MAP (g1:'a1 -> 'c1) =
581  OPTION_MAP (f1 o g1) : 'a1 option -> 'd1 option
582Proof
583  simp[FUN_EQ_THM] >> Cases >> simp[]
584QED
585
586(* what a registered operator's set function says at the operator's own
587   constructors is what a proof about the operator's contents needs, so
588   it simplifies: listTheory's LIST_TO_SET already does *)
589Definition optSET_def[simp]:
590  optSET NONE = {} ∧
591  optSET (SOME x) = {x}
592End
593
594Theorem optMapIMAGE1:
595  ∀(f : 'a1 -> 'c1) (x : 'a1 option).
596    optSET (OPTION_MAP f x) = IMAGE f (optSET x)
597Proof
598  Cases_on ‘x’ >> simp[EXTENSION, PULL_EXISTS, optSET_def]
599QED
600
601Theorem optMapCONG:
602  (∀a1. a1 ∈ optSET (x : 'a1 option) ⇒ ((f1 : 'a1 -> 'c1) a1 = g1 a1)) ⇒
603  OPTION_MAP f1 x = OPTION_MAP g1 x
604Proof
605  Cases_on ‘x’ >> simp[optSET_def]
606QED
607
608Theorem opt_bnd1:
609  ∀x : 'a1 option. optSET x ≼ univ(:num)
610Proof
611  Cases >> simp[cardleq_def, optSET_def, INJ_DEF]
612QED
613
614Theorem opt_wit1:
615  ∀a1:'a1. optSET (K NONE a1 : 'a1 option) ⊆ ∅
616Proof
617  simp[optSET_def, SUBSET_DEF, EXTENSION, IN_DEF]
618QED
619
620Theorem opt_wit2:
621  ∀a1:'a1. optSET (SOME a1) ⊆ {a1}
622Proof
623  simp[optSET_def, SUBSET_DEF, EXTENSION, IN_DEF]
624QED
625
626Theorem opt_inh1:
627  ∀v:'a1. v ∈ optSET (SOME v)
628Proof
629  simp[optSET_def, SUBSET_DEF, EXTENSION, IN_DEF]
630QED
631
632val _ = bnfBase.updateDB (
633  {Thy = "option", Name = "option"},
634  bnfBase.bI {
635    canontype = “:'a1 option”,
636    map = “option$OPTION_MAP : ('a1 -> 'c1) -> 'a1 option -> 'c1 option”,
637    set = [“optSET : 'a1 option -> 'a1 set”],
638    mapID = pnm "optMap_ID",
639    mapO = pnm "optMap_O",
640    mapIMAGE = [pnm "optMapIMAGE1"],
641    mapCONG = pnm "optMapCONG",
642    relator = “option$OPTREL : ('a1 -> 'c1 -> bool) ->
643                               ('a1 option -> 'c1 option -> bool)”,
644    bnd = “univ(:num)”,
645    bndthms = [pnm "opt_bnd1"],
646
647    wits = [(“K NONE : 'a1 -> 'a1 option”, pnm "opt_wit1"),
648            (“SOME : 'a1 -> 'a1 option”, pnm "opt_wit2")],
649    inhabits = [(“SOME : 'a1 -> 'a1 option”, pnm "opt_inh1")]
650  }
651)
652
653Theorem optrel_thm[local]:
654  OPTREL (R:'a1 -> 'a2 -> bool) (x1:'a1 option) (x2:'a2 option) ⇔
655    ∃x:('a1#'a2) option.
656      x1 = OPTION_MAP FST x ∧ x2 = OPTION_MAP SND x ∧
657      ∀a b. (a,b) ∈ optSET x ⇒ R a b
658Proof
659  Cases_on ‘x1’ >> Cases_on ‘x2’ >> simp[OPTREL_def, PULL_EXISTS, optSET_def] >>
660  iff_tac
661  >- (strip_tac >> Q.RENAME_TAC [‘a = FST _ ∧ b = SND _ ∧ _’] >>
662      Q.EXISTS_TAC ‘(a,b)’ >> simp[]) >>
663  simp[pairTheory.EXISTS_PROD]
664QED
665
666(* ----------------------------------------------------------------------
667    Results supporting the compositional derivation of bounds for
668    composite functors.
669
670    A composite functor's set-function is built (see bnfLib) out of
671
672       $=                     (at the functor's own argument)
673       K ∅                    (at argument-free positions)
674       BIMG s ∘ set           (descending through a component functor)
675       S ($UNION ∘ s₁) s₂     (combining a component's various arguments)
676
677    so a bound for the composite follows from bounds for the pieces, as
678    long as the bound is infinite.  The results below are the four cases.
679   ---------------------------------------------------------------------- *)
680
681Theorem EQ_CARDLE:
682  ∀B. B ≠ ∅ ⇒ ∀x:'a. $= x ≼ B
683Proof
684  simp[SING_CARDLE]
685QED
686
687Theorem CARDEQ_IMP_CARDLEQ:
688  ∀s t. s ≈ t ⇒ s ≼ t
689Proof
690  metis_tac[cardleq_lteq]
691QED
692
693Theorem CARDLEQ_INFINITE:
694  ∀s t. INFINITE s ∧ s ≼ t ⇒ INFINITE t
695Proof
696  metis_tac[CARD_LE_FINITE]
697QED
698
699Theorem INFINITE_NOT_EMPTY:
700  ∀B. INFINITE B ⇒ B ≠ ∅
701Proof
702  metis_tac[FINITE_EMPTY]
703QED
704
705Theorem K0_CARDLE:
706  ∀B x:'b. (K ∅ : 'b -> 'a set) x ≼ B
707Proof
708  simp[]
709QED
710
711Theorem LU_CARDLE:
712  ∀B f1 f2.
713    INFINITE B ∧ (∀x. f1 x ≼ B) ∧ (∀x. f2 x ≼ B) ⇒
714    ∀x. S ($UNION o f1) f2 x ≼ B
715Proof
716  rpt gen_tac >> strip_tac >> simp[combinTheory.S_THM] >> gen_tac >>
717  irule UNION_CARDLE >> simp[]
718QED
719
720Theorem BIMGo_CARDLE:
721  ∀B g st.
722    INFINITE B ∧ (∀y. g y ≼ B) ∧ (∀x. st x ≼ B) ⇒
723    ∀x. (BIMG g o st) x ≼ B
724Proof
725  rpt gen_tac >> strip_tac >> simp[combinTheory.o_THM] >> gen_tac >>
726  irule CARD_BIGUNION >> simp[PULL_EXISTS] >>
727  irule IMAGE_cardleq_rwt >> simp[]
728QED
729
730(* ----------------------------------------------------------------------
731    ... and the results used to see that a component functor's own bound
732    is dominated by the composite's, which is always of the form
733    univ(:num + τ₁ + ... + τₙ)
734   ---------------------------------------------------------------------- *)
735
736Theorem UNIV_CARD_LE_ADDR:
737  univ(:'a) ≼ univ(:'a + 'b)
738Proof
739  simp[disjUNION_UNIV, CARD_LE_ADDR]
740QED
741
742Theorem UNIV_CARD_LE_ADDL:
743  univ(:'b) ≼ univ(:'a + 'b)
744Proof
745  simp[disjUNION_UNIV, CARD_LE_ADDL]
746QED
747
748Theorem INFINITE_num_sum[simp]:
749  INFINITE univ(:num + 'a)
750Proof
751  ‘INJ INL univ(:num) univ(:num + 'a)’ by simp[INJ_DEF] >>
752  metis_tac[INFINITE_INJ, num_INFINITE]
753QED
754
755Theorem UNIV_NUM_NOT_EMPTY[simp]:
756  univ(:num) ≠ ∅
757Proof
758  simp[EXTENSION]
759QED
760
761(* ----------------------------------------------------------------------
762    Results supporting the compositional derivation of the map/set laws
763    for a composite functor.  Each result handles one node of the
764    composite's set-function (see bnfLib): the functor's own argument
765    ($=), an argument-free position (K ∅), a descent through a component
766    functor (BIMG s ∘ set), and the combination of a component's various
767    arguments (S ($UNION ∘ s₁) s₂).
768   ---------------------------------------------------------------------- *)
769
770Theorem EQ_natural:
771  ∀f:'a -> 'b. $= o f = IMAGE f o $=
772Proof
773  MATCH_ACCEPT_TAC (GSYM IMAGE_o_equal)
774QED
775
776(* the map is arbitrary, not I: in an n-ary functor an occurrence of a
777   *different* argument contributes nothing to this argument's set, but
778   still has that argument's function applied to it *)
779Theorem K0_natural:
780  ∀(f:'a -> 'b) (h:'c -> 'd).
781    (K ∅ : 'd -> 'b set) o h = IMAGE f o (K ∅ : 'c -> 'a set)
782Proof
783  simp[FUN_EQ_THM]
784QED
785
786Theorem BIMG_o_natural:
787  ∀stB stA sB sA mp h f.
788    stB o mp = IMAGE h o stA ∧ sB o h = IMAGE f o sA ⇒
789    (BIMG sB o stB) o mp = IMAGE f o (BIMG sA o stA)
790Proof
791  rpt gen_tac >> strip_tac >>
792  RULE_ASSUM_TAC (SIMP_RULE bool_ss [Once FUN_EQ_THM, combinTheory.o_THM]) >>
793  CONV_TAC (ONCE_REWRITE_CONV [FUN_EQ_THM]) >>
794  simp[combinTheory.o_THM, IMAGE_IMAGE, combinTheory.o_DEF, IMAGE_BIGUNION]
795QED
796
797Theorem LU_natural:
798  ∀aB aA bB bA mp f.
799    aB o mp = IMAGE f o aA ∧ bB o mp = IMAGE f o bA ⇒
800    S ($UNION o aB) bB o mp = IMAGE f o S ($UNION o aA) bA
801Proof
802  rpt gen_tac >> strip_tac >>
803  RULE_ASSUM_TAC (SIMP_RULE bool_ss [Once FUN_EQ_THM, combinTheory.o_THM]) >>
804  CONV_TAC (ONCE_REWRITE_CONV [FUN_EQ_THM]) >>
805  simp[combinTheory.o_THM, combinTheory.S_THM, IMAGE_UNION]
806QED
807
808Theorem EQ_CONG:
809  ∀f g x. (∀a. a ∈ $= x ⇒ f a = g a) ⇒ f x = g x
810Proof
811  simp[IN_DEF]
812QED
813
814Theorem BIMG_o_CONG_hyp:
815  ∀sA stA x y f g.
816    (∀a. a ∈ (BIMG sA o stA) x ⇒ f a = g a) ∧ y ∈ stA x ⇒
817    ∀a. a ∈ sA y ⇒ f a = g a
818Proof
819  rpt strip_tac >> first_x_assum irule >> simp[PULL_EXISTS] >>
820  metis_tac[]
821QED
822
823Theorem LU_CONG_hyp:
824  ∀aA bA x f g.
825    (∀a. a ∈ S ($UNION o aA) bA x ⇒ f a = g a) ⇒
826    (∀a. a ∈ aA x ⇒ f a = g a) ∧ (∀a. a ∈ bA x ⇒ f a = g a)
827Proof
828  simp[combinTheory.S_THM] >> rpt strip_tac >> first_x_assum irule >> simp[]
829QED
830
831(* ----------------------------------------------------------------------
832    What a size says about a mapped value.
833
834    A datatype recursing through an operator has its size read off the
835    value the recursion hands over, which is the argument with the size
836    already mapped across it: `1 + option_size (λx. x) (OPTION_MAP sz v)`.
837    Termination proofs take that apart with the operator's own size
838    clauses, which are about `option_size sz v`, so the two are brought
839    together here — `list_size_map` says the same of lists.
840   ---------------------------------------------------------------------- *)
841
842Theorem option_size_map:
843  option_size f (OPTION_MAP g x) = option_size (\a. f (g a)) x
844Proof
845  Cases_on ‘x’ >> simp[]
846QED
847
848val _ = TotalDefn.export_termsimp "bnfPrelims.option_size_map"
849
850(* and of a sum, whose size counts the tag *)
851Theorem sum_size_map:
852  full_sum_size f g (SUM_MAP h k s) =
853  full_sum_size (\a. f (h a)) (\b. g (k b)) s
854Proof
855  Cases_on ‘s’ >> simp[basicSizeTheory.full_sum_size_thm]
856QED
857
858val _ = TotalDefn.export_termsimp "bnfPrelims.sum_size_map"
859
860(* and the same of a pair, whose map is written with ## *)
861Theorem pair_size_map:
862  pair_size f g ((h ## k) p) = pair_size (\a. f (h a)) (\b. g (k b)) p
863Proof
864  Cases_on ‘p’ >> simp[]
865QED
866
867val _ = TotalDefn.export_termsimp "bnfPrelims.pair_size_map"