bnfPrelimsScript.sml

1Theory bnfPrelims[bare]
2Ancestors sum pair option pred_set cardinal quotient
3Libs HolKernel Parse boolLib BasicProvers simpLib TotalDefn[qualified] QLib
4     metisLib
5
6
7fun sum_nm s : KernelSig.kernelname = {Thy = "sum", Name = s}
8fun pair_nm s : KernelSig.kernelname = {Thy = "pair", Name = s}
9fun pnm s : KernelSig.kernelname = {Thy = "bnfPrelims", Name = s}
10val T = {Name = "TRUTH", Thy = "bool"} (* placeholder *)
11
12(* ----------------------------------------------------------------------
13    some bossLib emulation
14   ---------------------------------------------------------------------- *)
15
16fun simp ths = simpLib.ASM_SIMP_TAC (srw_ss()) ths
17val metis_tac = METIS_TAC
18val op >~ = Q.>~
19
20(* ----------------------------------------------------------------------
21    Utility results that all constructions will likely use
22   ---------------------------------------------------------------------- *)
23
24Theorem IMAGE_o_equal:
25  IMAGE f o (=) = (=) o f
26Proof
27  simp[FUN_EQ_THM, IN_DEF, EQ_SYM_EQ]
28QED
29
30Theorem KlamF:
31  K (λx. F) = K {}
32Proof
33  simp[FUN_EQ_THM]
34QED
35
36Theorem o_INTRO:
37  (∀x. f (g x) = h x) ⇔ f o g = h
38Proof
39  simp[combinTheory.o_DEF, FUN_EQ_THM]
40QED
41
42Theorem UNION_CARDLE:
43  INFINITE CC ∧ A ≼ CC ∧ B ≼ CC ⇒ A ∪ B ≼ CC
44Proof
45  strip_tac >>
46  resolve_then Any irule UNION_LE_ADD_C cardleq_TRANS >>
47  irule CARD_ADD2_ABSORB_LE >> simp[]
48QED
49
50Theorem IN_equal:
51  x ∈ (=) y ⇔ x = y
52Proof
53  simp[IN_DEF, EQ_SYM_EQ]
54QED
55
56(* not generally safe as an unbounded rewrite *)
57Theorem EQ_SING:
58  $= x = {x}
59Proof
60  simp[EXTENSION, IN_equal]
61QED
62
63Theorem SING_CARDLE:
64  ({x} ≼ A ⇔ A ≠ ∅) ∧ ((=) x ≼ A ⇔ A ≠ ∅)
65Proof
66  ‘(=) x = {x}’ by MATCH_ACCEPT_TAC EQ_SING >> simp[] >>
67  simp[EQ_IMP_THM, INJ_DEF, cardleq_def, GSYM MEMBER_NOT_EMPTY] >>
68  rpt strip_tac >~
69  [‘∃f. f x ∈ A’, ‘a ∈ A (* a *)’]
70  >- (qexists_tac ‘K a’ >> simp[]) >>
71  first_assum $ irule_at Any
72QED
73
74Theorem IMAGE_KEMPTY_CARDLE:
75  IMAGE (K ∅) A ≼ B ⇔ A = ∅ ∨ B ≠ ∅
76Proof
77  simp[EQ_IMP_THM, DISJ_IMP_THM] >> Cases_on ‘A = ∅’ >> simp[] >>
78  Cases_on ‘B = ∅’ >> simp[] >>
79  ‘IMAGE (K ∅) A = {∅}’
80    by (simp[Once EXTENSION] >> simp[EQ_IMP_THM, PULL_EXISTS] >>
81        RULE_ASSUM_TAC (REWRITE_RULE[GSYM MEMBER_NOT_EMPTY]) >>
82        simp[]) >>
83  simp[SING_CARDLE]
84QED
85
86Theorem UNIQUE_SKOLEM:
87  (∀x. ∃!y. P x y) ⇔ ∃!f. ∀x. P x (f x)
88Proof
89  eq_tac >> simp[EXISTS_UNIQUE_THM] >> rpt strip_tac
90  >- (qexists_tac ‘λx. @y. P x y’ >> simp[] >> gen_tac >> SELECT_ELIM_TAC >>
91      METIS_TAC[])
92  >- (simp[FUN_EQ_THM] >> METIS_TAC[])
93  >- METIS_TAC[]
94  >- (rename [‘P x a’, ‘P x b’, ‘a = b’] >>
95      Cases_on ‘f x = a’
96      >- (pop_assum (SUBST_ALL_TAC o SYM) >>
97          first_x_assum $ qspecl_then [‘f’, ‘f (| x |-> b |)’] mp_tac >>
98          simp[combinTheory.APPLY_UPDATE_THM] >>
99          disch_then irule >> METIS_TAC[]) >>
100      first_x_assum $ qspecl_then [‘f(|x|->a|)’, ‘f’] mp_tac >>
101      simp[combinTheory.APPLY_UPDATE_THM, FUN_EQ_THM] >> METIS_TAC[])
102QED
103
104Overload BIMG = “(o) BIGUNION o IMAGE”
105
106Theorem BIMG_EQUAL:
107  BIMG $= = I
108Proof
109  ONCE_REWRITE_TAC[FUN_EQ_THM] >>
110  simp[Once EXTENSION, PULL_EXISTS, IN_equal]
111QED
112
113Theorem BIMG_EQUAL_L:
114  BIGUNION o IMAGE $= o f = f
115Proof
116  simp[Once FUN_EQ_THM] >>
117  simp[Once EXTENSION, PULL_EXISTS, IN_equal]
118QED
119
120Theorem BIMG_K0:
121  BIMG (K ∅) = K ∅
122Proof
123  simp[Once FUN_EQ_THM] >> qx_gen_tac ‘A’ >> Cases_on ‘A = {}’ >>
124  simp[EXTENSION] >> METIS_TAC[MEMBER_NOT_EMPTY]
125QED
126
127Theorem BIMG_IMAGE:
128  BIMG (λx. IMAGE f (g x)) A = IMAGE f (BIMG g A)
129Proof
130  simp[Once EXTENSION, PULL_EXISTS] >> METIS_TAC[]
131QED
132
133Theorem SKg_thm:
134  S (K v) g = v o g
135Proof
136  simp[FUN_EQ_THM]
137QED
138
139Theorem UNION_EMPTY1:
140  (UNION) {} = I
141Proof
142  simp[Once FUN_EQ_THM]
143QED
144
145Theorem BIMG_IMAGEo:
146  BIMG (IMAGE f o g) = IMAGE f o BIMG g
147Proof
148  CONV_TAC (ONCE_REWRITE_CONV [FUN_EQ_THM]) >>
149  simp[Once EXTENSION, PULL_EXISTS, AC CONJ_ASSOC CONJ_COMM] >>
150  METIS_TAC[]
151QED
152
153Theorem IMAGE_IMAGE_lo:
154  (f o IMAGE g) o IMAGE h = f o IMAGE (g o h)
155Proof
156  simp[FUN_EQ_THM, GSYM IMAGE_o]
157QED
158
159Theorem IMAGE_IMAGE_o = REWRITE_RULE [GSYM combinTheory.o_ASSOC] IMAGE_IMAGE_lo
160
161Theorem IMAGE_IMAGE_ro:
162  IMAGE g o (IMAGE h o f) = IMAGE (g o h) o f
163Proof
164  simp[FUN_EQ_THM, PULL_EXISTS]
165QED
166
167Theorem BIGUNION_o_IMAGE_IMAGE:
168  BIGUNION o IMAGE (IMAGE f o g) = IMAGE f o BIGUNION o IMAGE g
169Proof
170  simp[Once FUN_EQ_THM]>> simp[Once EXTENSION, PULL_EXISTS] >>
171  metis_tac[]
172QED
173
174Theorem BIGUNION_o_IMAGE_IMAGEr:
175  BIGUNION o (IMAGE (IMAGE f o g) o h) = IMAGE f o BIGUNION o IMAGE g o h
176Proof
177  simp[Once FUN_EQ_THM]>> simp[Once EXTENSION, PULL_EXISTS] >>
178  metis_tac[]
179QED
180
181Theorem IMAGE_BIGUNIONo:
182  BIGUNION (IMAGE (IMAGE f o h) A) = IMAGE f (BIGUNION (IMAGE h A))
183Proof
184  simp[Once EXTENSION, PULL_EXISTS, AC CONJ_ASSOC CONJ_COMM] >>
185  metis_tac[]
186QED
187
188
189(* ----------------------------------------------------------------------
190    record the sum type's Bounded Natural Functor nature
191   ---------------------------------------------------------------------- *)
192
193Theorem sumMap_def[unlisted] =
194        SUM_MAP_def
195        |> INST_TYPE [alpha |-> “:'a1”, beta |-> “:'a2”,
196                      gamma |-> “:'c1”, delta |-> “:'c2”]
197
198Theorem sumMap_ID[unlisted] =
199        SUM_MAP_I
200        |> INST_TYPE [alpha |-> “:'a1”, beta |-> “:'a2”]
201
202Theorem sumMap_O[unlisted] =
203        SUM_MAP_o
204        |> INST_TYPE [alpha |-> “:'a1”, beta |-> “:'a2”,
205                      gamma |-> “:'d1”, delta |-> “:'d2”,
206                      “:'e” |-> “:'c1”, “:'f” |-> “:'c2”
207                     ]
208        |> Q.INST [‘f’ |-> ‘f1’, ‘g’ |-> ‘f2’,
209                   ‘h’ |-> ‘g1’, ‘k’ |-> ‘g2’]
210
211Theorem sumMapIMAGE1:
212  ∀f1 f2 s.
213    setL (SUM_MAP (f1:'a1 -> 'c1) (f2:'a2 -> 'c2) (s:'a1 + 'a2)) =
214    IMAGE f1 (setL s)
215Proof
216  GEN_TAC >> GEN_TAC >> Cases_on ‘s’ >>
217  SIMP_TAC (srw_ss()) [EXTENSION]
218QED
219
220Theorem sumMapIMAGE2:
221  ∀f1 f2 s.
222    setR (SUM_MAP (f1:'a1 -> 'c1) (f2:'a2 -> 'c2) (s:'a1 + 'a2)) =
223    IMAGE f2 (setR s)
224Proof
225  GEN_TAC >> GEN_TAC >> Cases_on ‘s’ >>
226  SIMP_TAC (srw_ss()) [EXTENSION]
227QED
228
229Theorem sumMapCONG =
230        sumTheory.SUM_MAP_CONG
231          |> INST_TYPE [alpha |-> “:'a1”, beta |-> “:'a2”,
232                        gamma |-> “:'c1”, delta |-> “:'c2”]
233
234Theorem sum_bnd1:
235  ∀s : 'a + 'b. setL s ≼ univ(:num)
236Proof
237  GEN_TAC >> Cases_on ‘s’ >> simp[cardleq_def, INJ_DEF]
238QED
239
240Theorem sum_bnd2:
241  ∀s : 'a + 'b. setR s ≼ univ(:num)
242Proof
243  GEN_TAC >> Cases_on ‘s’ >> simp[cardleq_def, INJ_DEF]
244QED
245
246val _ = bnfBase.updateDB (
247  {Name = "sum", Thy = "sum"},
248  bnfBase.bI {
249    bnd = “UNIV : num set”,
250    bndthms = [pnm "sum_bnd1", pnm "sum_bnd2"],
251    canontype = “:'a1 + 'a2”,
252
253    map = “SUM_MAP : ('a1 -> 'c1) -> ('a2 -> 'c2) -> 'a1 + 'a2 -> 'c1 + 'c2”,
254    mapID = pnm "sumMap_ID",
255    mapO = pnm "sumMap_O",
256    mapIMAGE = [pnm "sumMapIMAGE1", pnm "sumMapIMAGE2"],
257    mapCONG = pnm "sumMapCONG",
258
259    relator = “SUM_REL : ('a1 -> 'c1 -> bool) -> ('a2 -> 'c2 -> bool) ->
260                         'a1 + 'a2 -> 'c1 + 'c2 -> bool”,
261    set = [“setL : 'a1 + 'a2 -> 'a1 set”, “setR : 'a1 + 'a2 -> 'a2 set”],
262    siblings = []
263  }
264)
265
266(* ----------------------------------------------------------------------
267    record the pair type's Bounded Natural Functor nature
268   ---------------------------------------------------------------------- *)
269
270Theorem pairMap_ID = PAIR_MAP_I |> INST_TYPE [alpha |-> “:'a1”, beta |-> “:'a2”]
271
272Theorem pairMap_O:
273  ((f1:'c1 -> 'd1) ## (f2 : 'c2 -> 'd2)) o
274  ((g1:'a1 -> 'c1) ## (g2 : ('a2 -> 'c2))) =
275  ((f1 o g1) ## (f2 o g2))
276Proof
277  simp[FUN_EQ_THM] >> Cases >> simp[]
278QED
279
280Theorem pairMapIMAGE1:
281  ∀f1 f2 p. setFST (((f1 : 'a1 -> 'c1) ## (f2 : 'a2 -> 'c2)) p) =
282            IMAGE f1 (setFST p)
283Proof
284  Cases_on ‘p’ >> simp[PAIR_MAP_SET, EXTENSION, EQ_SYM_EQ]
285QED
286
287Theorem pairMapIMAGE2:
288  ∀f1 f2 p. setSND (((f1 : 'a1 -> 'c1) ## (f2 : 'a2 -> 'c2)) p) =
289            IMAGE f2 (setSND p)
290Proof
291  Cases_on ‘p’ >> simp[PAIR_MAP_SET, EXTENSION, EQ_SYM_EQ]
292QED
293
294Theorem pairMapCONG:
295  (∀a1:'a1. a1 ∈ setFST p ⇒ (f1 : 'a1 -> 'c1) a1 = g1 a1) ∧
296  (∀a2:'a2. a2 ∈ setSND p ⇒ (f2 : 'a2 -> 'c2) a2 = g2 a2) ⇒
297  (f1 ## f2) p = (g1 ## g2) p
298Proof
299  Cases_on ‘p’ >> simp[]
300QED
301
302Theorem pair_bnd1:
303  ∀p : 'a1 # 'a2. setFST p ≼ univ(:num)
304Proof
305  Cases >> simp[cardleq_def, INJ_DEF]
306QED
307
308Theorem pair_bnd2:
309  ∀p : 'a1 # 'a2. setSND p ≼ univ(:num)
310Proof
311  Cases >> simp[cardleq_def, INJ_DEF]
312QED
313
314val _ = bnfBase.updateDB (
315  {Thy = "pair", Name = "prod"},
316  bnfBase.bI {
317    canontype = “:'a1 # 'a2”,
318    siblings = [],
319
320    map = “pair$## : ('a1 -> 'c1) -> ('a2 -> 'c2) -> 'a1 # 'a2 -> 'c1 # 'c2”,
321    set = [“setFST : 'a1 # 'a2 -> 'a1 set”, “setSND : 'a1 # 'a2 -> 'a2 set”],
322    mapID = pnm "pairMap_ID",
323    mapO = pnm "pairMap_O",
324    mapIMAGE = [pnm "pairMapIMAGE1", pnm "pairMapIMAGE2"],
325    mapCONG = pnm "pairMapCONG",
326    relator = “pair$RPROD : ('a1 -> 'c1 -> bool) -> ('a2 -> 'c2 -> bool) ->
327                            ('a1 # 'a2 -> 'c1 # 'c2 -> bool)”,
328    bnd = “univ(:num)”,
329    bndthms = [pnm "pair_bnd1", pnm "pair_bnd2"]
330  }
331)
332
333(* ----------------------------------------------------------------------
334    record the function type's Bounded Natural Functor nature
335      (in its 2nd arg, the range)
336   ---------------------------------------------------------------------- *)
337
338Overload fmap[local,inferior] = “$o”
339Overload fset[local,inferior] =
340  “combin$C IMAGE univ(:'b1) : ('b1 -> 'a1) -> 'a1 set”
341Overload frel[local,inferior] =
342  “quotient$===> $= : ('a1 -> 'c1 -> bool) ->
343                      (('b1 -> 'a1) -> ('b1 -> 'c1) -> bool)”
344Theorem funMap_ID:
345  fmap (I:'a1 -> 'a1) = I : ('b1 -> 'a1) -> ('b1 -> 'a1)
346Proof
347  simp[FUN_EQ_THM]
348QED
349
350Theorem funMap_O:
351  fmap (f1:'c1 -> 'd1) o fmap (g1:'a1 -> 'c1) =
352  fmap (f1 o g1) : ('b1 -> 'a1) -> ('b1 -> 'd1)
353Proof
354  simp[FUN_EQ_THM]
355QED
356
357Theorem funMapIMAGE1:
358  ∀(f : 'a1 -> 'c1) (fn : 'b1 -> 'a1). fset (fmap f fn) = IMAGE f (fset fn)
359Proof
360  simp[EXTENSION, PULL_EXISTS]
361QED
362
363Theorem funMapCONG:
364  (∀a1. a1 ∈ fset (fn : 'b1 -> 'a1) ⇒ ((f1 : 'a1 -> 'c1) a1 = g1 a1)) ⇒
365  fmap f1 fn = fmap g1 fn
366Proof
367  simp[EXTENSION, PULL_EXISTS, FUN_EQ_THM]
368QED
369
370Theorem fun_bnd1:
371  ∀f : 'b1 -> 'a1. fset f ≼ univ(:'b1)
372Proof
373  simp[cardleq_def] >> gen_tac >> irule SURJ_IMP_INJ >>
374  irule_at Any SURJ_IMAGE
375QED
376
377val _ = bnfBase.updateDB (
378  {Thy = "min", Name = "fun"},
379  bnfBase.bI {
380    canontype = “:'b1 -> 'a1”,
381    siblings = [],
382    map = “combin$o : ('a1 -> 'c1) -> ('b1 -> 'a1) -> ('b1 -> 'c1)”,
383    set = [“fset: ('b1 -> 'a1) -> 'a1 set”],
384    mapID = pnm "funMap_ID",
385    mapO = pnm "funMap_O",
386    mapIMAGE = [pnm "funMapIMAGE1"],
387    mapCONG = pnm "funMapCONG",
388    relator = “quotient$===> $= : ('a1 -> 'c1 -> bool) ->
389                                  (('b1 -> 'a1) -> ('b1 -> 'c1) -> bool)”,
390    bnd = “univ(:'b1)”,
391    bndthms = [pnm "fun_bnd1"]
392  }
393)
394
395Theorem frel_thm[local]:
396  frel (R:'a1 -> 'a2 -> bool) (f1:'b1 -> 'a1) (f2:'b1 -> 'a2) ⇔
397    ∃f. f1 = fmap FST f ∧ f2 = fmap SND f ∧
398        ∀x y. (x,y) ∈ fset f ⇒ R x y
399Proof
400  simp[FUN_REL, PULL_EXISTS] >> iff_tac
401  >- (strip_tac >> Q.EXISTS_TAC ‘λb. (f1 b, f2 b)’ >> simp[FUN_EQ_THM]) >>
402  SRW_TAC[][combinTheory.o_DEF] >> simp[] >> Q.RENAME_TAC [‘FST (f b)’] >>
403  Cases_on ‘f b’ >> simp[] >> first_x_assum irule >>
404  first_x_assum (irule_at Any o SYM)
405QED
406
407(* ----------------------------------------------------------------------
408    record the option type's Bounded Natural Functor nature
409   ---------------------------------------------------------------------- *)
410
411Theorem optMap_ID:
412  OPTION_MAP (I:'a1 -> 'a1) = I : 'a1 option -> 'a1 option
413Proof
414  simp[FUN_EQ_THM]
415QED
416
417Theorem optMap_O:
418  OPTION_MAP (f1:'c1 -> 'd1) o OPTION_MAP (g1:'a1 -> 'c1) =
419  OPTION_MAP (f1 o g1) : 'a1 option -> 'd1 option
420Proof
421  simp[FUN_EQ_THM] >> Cases >> simp[]
422QED
423
424Definition optSET_def:
425  optSET NONE = {} ∧
426  optSET (SOME x) = {x}
427End
428
429Theorem optMapIMAGE1:
430  ∀(f : 'a1 -> 'c1) (x : 'a1 option).
431    optSET (OPTION_MAP f x) = IMAGE f (optSET x)
432Proof
433  Cases_on ‘x’ >> simp[EXTENSION, PULL_EXISTS, optSET_def]
434QED
435
436Theorem optMapCONG:
437  (∀a1. a1 ∈ optSET (x : 'a1 option) ⇒ ((f1 : 'a1 -> 'c1) a1 = g1 a1)) ⇒
438  OPTION_MAP f1 x = OPTION_MAP g1 x
439Proof
440  Cases_on ‘x’ >> simp[optSET_def]
441QED
442
443Theorem opt_bnd1:
444  ∀x : 'a1 option. optSET x ≼ univ(:num)
445Proof
446  Cases >> simp[cardleq_def, optSET_def, INJ_DEF]
447QED
448
449val _ = bnfBase.updateDB (
450  {Thy = "option", Name = "option"},
451  bnfBase.bI {
452    canontype = “:'a1 option”,
453    siblings = [],
454    map = “option$OPTION_MAP : ('a1 -> 'c1) -> 'a1 option -> 'c1 option”,
455    set = [“optSET : 'a1 option -> 'a1 set”],
456    mapID = pnm "optMap_ID",
457    mapO = pnm "optMap_O",
458    mapIMAGE = [pnm "optMapIMAGE1"],
459    mapCONG = pnm "optMapCONG",
460    relator = “option$OPTREL : ('a1 -> 'c1 -> bool) ->
461                               ('a1 option -> 'c1 option -> bool)”,
462    bnd = “univ(:num)”,
463    bndthms = [pnm "opt_bnd1"]
464  }
465)
466
467Theorem optrel_thm[local]:
468  OPTREL (R:'a1 -> 'a2 -> bool) (x1:'a1 option) (x2:'a2 option) ⇔
469    ∃x:('a1#'a2) option.
470      x1 = OPTION_MAP FST x ∧ x2 = OPTION_MAP SND x ∧
471      ∀a b. (a,b) ∈ optSET x ⇒ R a b
472Proof
473  Cases_on ‘x1’ >> Cases_on ‘x2’ >> simp[OPTREL_def, PULL_EXISTS, optSET_def] >>
474  iff_tac
475  >- (strip_tac >> Q.RENAME_TAC [‘a = FST _ ∧ b = SND _ ∧ _’] >>
476      Q.EXISTS_TAC ‘(a,b)’ >> simp[]) >>
477  simp[pairTheory.EXISTS_PROD]
478QED