bnfInitialScript.sml

1Theory bnfInitial[bare]
2Ancestors
3  pred_set cardinalityCore ordinalBasic combin pair
4Libs
5  HolKernel Parse boolLib BasicProvers simpLib boolSimps metisLib numLib
6  pred_setLib pairLib QLib TotalDefn[qualified]
7
8(* cardinalityCoreTheory makes no grammar of its own -- it is every
9   theory's ancestor through the datatype package, and the ASCII
10   forms are tokens wherever they reach.  What this theory writes
11   it sets up for itself. *)
12Overload "<<="[local] = “cardleq”
13Overload cardlt[local] = “λs1 s2. ¬cardleq s2 s1”
14val _ = temp_set_fixity "<</=" (Infix(NONASSOC, 450));
15val _ = Unicode.temp_unicode_version {u = UTF8.chr 0x227A, tmnm = "<</="};
16Overload "<</="[local] = “cardlt”
17val _ = temp_set_fixity "=~" (Infix(NONASSOC, 450));
18val _ = Unicode.temp_unicode_version {u = UTF8.chr 0x2248, tmnm = "=~"};
19Overload "=~"[local] = “cardeq”
20Overload "𝟚"[local] = “{T;F}”
21Overload cardlt[local] = “λs1 s2. ¬cardleq s2 s1”
22val _ = temp_set_fixity "<</=" (Infix(NONASSOC, 450));
23val _ = Unicode.temp_unicode_version {u = UTF8.chr 0x227A, tmnm = "<</="};
24Overload "<</="[local] = “cardlt”
25val _ = temp_set_fixity "=~" (Infix(NONASSOC, 450));
26val _ = Unicode.temp_unicode_version {u = UTF8.chr 0x2248, tmnm = "=~"};
27Overload "=~"[local] = “cardeq”
28
29
30(* ----------------------------------------------------------------------
31    bossLib is not built yet — the package has to be, so that Datatype
32    can use it, and so this is the part of bossLib's environment these
33    proofs need.  The same emulation cardinalScript uses.
34   ---------------------------------------------------------------------- *)
35
36fun simp ths = simpLib.ASM_SIMP_TAC (srw_ss()) ths
37fun csimp ths = simp (SF CONJ_ss :: ths)
38fun dsimp ths = simp (SF DNF_ss :: ths)
39fun gs ths = simpLib.global_simp_tac
40               {elimvars = false, strip = true, droptrues = true,
41                oldestfirst = true} (srw_ss()) ths
42fun gvs ths = simpLib.global_simp_tac
43                {elimvars = true, strip = true, droptrues = true,
44                 oldestfirst = true} (srw_ss()) ths
45fun rw ths = BasicProvers.SRW_TAC [] ths
46val metis_tac = metisLib.METIS_TAC
47fun SRULE ths th = SIMP_RULE (srw_ss()) ths th
48val qexists = Q.EXISTS_TAC
49
50(* The construction counts in ordinals, whose notation ordinalTheory
51   exports and this theory must not: everything that declares a datatype
52   loads this one.  So the notation is here for these proofs alone. *)
53Overload "<"[local] = “ordlt”
54Overload "<="[local] = “\a b. ~ordlt b a”
55Overload "+"[local] = “ordADD”
56Overload "ω"[local] = “omega”
57Overload islimit[local] = “\a:'a ordinal. omax (preds a) = NONE”
58Overload TC[local] = “ordSUC”   (* which is what writes a successor a⁺ *)
59(* and the same for the sets' own exponent, which cardinalTheory keeps
60   to itself for the same reason *)
61Overload "**"[local] = “set_exp”
62val _ = temp_add_numeral_form (#"o", SOME "fromNat")
63val op >~ = Q.>~
64val op >>~ = Q.>>~
65
66
67(* ----------------------------------------------------------------------
68    The initial-algebra construction, proved once.
69
70    HOL has no type-operator variables, so a functor F cannot be
71    quantified over directly.  It can, however, be *parameterised*: each
72    instance F[τ] that the construction needs becomes an ordinary type
73    variable, and the functor's map and set functions become ordinary
74    term variables, with the BNF laws carried as hypotheses.  The
75    development below never mentions a particular functor, so it is
76    proved once and a datatype package only has to instantiate it — no
77    parsing, no tactics, and no per-datatype proof.
78
79    Throughout, 'f is F[α], 'g is F[β] and 'h is F[γ]; mp_ab is F's map
80    from α to β, and sta its set function at α.
81   ---------------------------------------------------------------------- *)
82
83(* the elements of F[α] all of whose α-atoms lie in As *)
84Definition FIN_def:
85  bnfFIN (sta : 'f -> 'a set) As = { a : 'f | sta a ⊆ As }
86End
87
88Theorem IN_FIN[simp]:
89  a ∈ bnfFIN sta As ⇔ sta a ⊆ As
90Proof
91  simp[FIN_def]
92QED
93
94Theorem FIN_UNIV[simp]:
95  bnfFIN sta UNIV = UNIV
96Proof
97  simp[EXTENSION]
98QED
99
100Definition ALG_def:
101  bnfALG (sta : 'f -> 'a set) (A, s) ⇔ ∀x. x ∈ bnfFIN sta A ⇒ s x ∈ A
102End
103
104(* the pointwise form: ALG_def's own right-hand side has a leading
105   quantifier, which no backward step can match against a goal about one
106   element *)
107Theorem ALG_closed:
108  bnfALG sta (A,s) ∧ sta x ⊆ A ⇒ s x ∈ A
109Proof
110  simp[ALG_def]
111QED
112
113Theorem ALG_UNIV[simp]:
114  bnfALG sta (UNIV, s)
115Proof
116  simp[ALG_def]
117QED
118
119Definition MINSET_def:
120  bnfMINSET (sta : 'f -> 'a set) s = BIGINTER { B | bnfALG sta (B,s) }
121End
122
123Theorem MINSET_is_ALG[simp]:
124  bnfALG sta (bnfMINSET sta s, s)
125Proof
126  simp[MINSET_def, ALG_def, SUBSET_BIGINTER]
127QED
128
129Theorem IN_MINSET:
130  x ∈ bnfMINSET sta s ⇔ ∀A. bnfALG sta (A,s) ⇒ x ∈ A
131Proof
132  simp[MINSET_def]
133QED
134
135Definition HOM_def:
136  bnfHOM (mp : ('a -> 'b) -> 'f -> 'g) sta stb h (A,s) (B,t) ⇔
137    bnfALG sta (A,s) ∧ bnfALG stb (B,t) ∧ (∀a. a ∈ A ⇒ h a ∈ B) ∧
138    ∀af. af ∈ bnfFIN sta A ⇒ t (mp h af) = h (s af)
139End
140
141(* ----------------------------------------------------------------------
142    The BNF laws, as predicates over the parameters.  Each names the
143    instances it relates, so a lemma can ask for exactly the ones it
144    needs.
145   ---------------------------------------------------------------------- *)
146
147Definition MapId_def:
148  bnfMapId (mp : ('a -> 'a) -> 'f -> 'f) ⇔ ∀x. mp I x = x
149End
150
151Definition MapComp_def:
152  bnfMapComp (mp_ab : ('a -> 'b) -> 'f -> 'g)
153          (mp_bc : ('b -> 'c) -> 'g -> 'h)
154          (mp_ac : ('a -> 'c) -> 'f -> 'h) ⇔
155    ∀f g x. mp_bc g (mp_ab f x) = mp_ac (g o f) x
156End
157
158Definition Natural_def:
159  bnfNatural (mp : ('a -> 'b) -> 'f -> 'g) sta stb ⇔
160    ∀f x. stb (mp f x) = IMAGE f (sta x)
161End
162
163Definition MapCong_def:
164  bnfMapCong (mp : ('a -> 'b) -> 'f -> 'g) sta ⇔
165    ∀f g x. (∀a. a ∈ sta x ⇒ f a = g a) ⇒ mp f x = mp g x
166End
167
168(* bnfMapCong comes first because it fixes both mp and sta, so drule can
169   resolve it against an assumption and know what the rest means *)
170Theorem Map_eq_id:
171  bnfMapCong mp sta ∧ bnfMapId mp ⇒
172  ∀f x. (∀a. a ∈ sta x ⇒ f a = a) ⇒ mp f x = x
173Proof
174  simp[MapId_def, MapCong_def] >> rpt strip_tac >>
175  ‘mp f x = mp I x’ by (first_x_assum irule >> simp[]) >>
176  simp[]
177QED
178
179(* ----------------------------------------------------------------------
180    The functor's value at one type, replaced by a copy of it.
181
182    A law is about the functor at a tuple of types, and its statement
183    carries those types at every leaf.  Where one of them is large and
184    the construction only passes it along, a type standing for it shrinks
185    every law that mentions it -- the initial algebra's F[carrier] is the
186    case, and these are the laws its copy satisfies.
187
188    Only `rep o abs = I` is wanted, in whichever direction the law puts
189    the copy: nothing here asks the copy to be injective, and `bnfMapCong`
190    is never demanded of a map the copy is the value of.
191
192    All four take that equation, including the two whose proofs do not
193    need it.  It is what says which copy the law is about: `abs` and `rep`
194    appear in these conclusions and nowhere else, so without a hypothesis
195    naming them a use of the law would leave them free, and two laws
196    transported for the same construction would not be about the same
197    copy.
198   ---------------------------------------------------------------------- *)
199
200Theorem Natural_ABS_out:
201  (∀x. rep (abs x) = x) ∧ bnfNatural mp sta stb ⇒
202  bnfNatural (λf. abs o mp f) sta (stb o rep)
203Proof
204  simp[Natural_def, o_THM] >> rpt strip_tac >> simp[]
205QED
206
207Theorem Natural_REP_in:
208  (∀x. rep (abs x) = x) ∧ bnfNatural mp sta stb ⇒
209  bnfNatural (λf. mp f o rep) (sta o rep) stb
210Proof
211  simp[Natural_def, o_THM]
212QED
213
214Theorem MapComp_ABS_out:
215  (∀x. rep (abs x) = x) ∧ bnfMapComp mp_ab mp_bc mp_ac ⇒
216  bnfMapComp mp_ab (λg. abs o mp_bc g) (λg. abs o mp_ac g)
217Proof
218  simp[MapComp_def, o_THM]
219QED
220
221Theorem MapComp_ABS_mid:
222  (∀x. rep (abs x) = x) ∧ bnfMapComp mp_ab mp_bc mp_ac ⇒
223  bnfMapComp (λf. abs o mp_ab f) (λg. mp_bc g o rep) mp_ac
224Proof
225  simp[MapComp_def, o_THM] >> rpt strip_tac >> simp[]
226QED
227
228(* ----------------------------------------------------------------------
229    algebras and homomorphisms
230   ---------------------------------------------------------------------- *)
231
232Theorem ALG_nonempty:
233  (∃w:'f. sta w = ∅) ⇒ bnfALG sta (A, s) ⇒ A ≠ ∅
234Proof
235  rpt strip_tac >> gvs[ALG_def] >> metis_tac[SUBSET_REFL, NOT_IN_EMPTY]
236QED
237
238Theorem HOMs_on_same_domain:
239  bnfMapCong mp sta ⇒
240  bnfHOM mp sta stb h (A,s) (B,t) ∧ (∀a. a ∈ A ⇒ h' a = h a) ⇒
241  bnfHOM mp sta stb h' (A,s) (B,t)
242Proof
243  simp[HOM_def, MapCong_def] >> rw[] >>
244  ‘s af ∈ A’ by gs[ALG_def] >> simp[] >>
245  ‘mp h' af = mp h af’ suffices_by simp[] >>
246  first_x_assum irule >> metis_tac[SUBSET_DEF]
247QED
248
249(* Combine assumptions with a rule, forward: the assumptions are named
250   by pattern and MATCH_MPed into the rule in the order its antecedents
251   appear.  irule cannot do these steps, because a composition's
252   intermediate carrier does not appear in the conclusion, and HOL
253   cannot leave a *type* existentially quantified. *)
254fun byrule rule pats ttac =
255    let fun recurse acc [] = ttac (MATCH_MP rule (LIST_CONJ (List.rev acc)))
256          | recurse acc (p::ps) = qpat_assum p (fn th => recurse (th::acc) ps)
257    in recurse [] pats end
258
259(* the intermediate algebra and everything about it is quantified out
260   in front: none of it appears in the conclusion, so irule leaves it
261   existential in this order for a use site to name *)
262Theorem HOMs_compose:
263  ∀stb mp_ab mp_bc (B:'b set) t.
264    bnfMapComp mp_ab mp_bc mp_ac ∧ bnfNatural mp_ab sta stb ∧
265    bnfHOM mp_ab sta stb f (A:'a set,s) (B,t) ∧
266    bnfHOM mp_bc stb stc g (B,t) (C:'c set,u) ⇒
267    bnfHOM mp_ac sta stc (g o f) (A,s) (C,u)
268Proof
269  simp[MapComp_def, Natural_def] >> rpt gen_tac >> strip_tac >>
270  gs[HOM_def] >> rw[] >>
271  ‘stb (mp_ab f af) ⊆ B’ by (simp[] >> gs[SUBSET_DEF, PULL_EXISTS]) >>
272  qpat_x_assum ‘∀af. stb af ⊆ B ⇒ _’ (qspec_then ‘mp_ab f af’ assume_tac) >>
273  qpat_x_assum ‘∀af. sta af ⊆ A ⇒ _’ (qspec_then ‘af’ assume_tac) >>
274  gs[]
275QED
276
277Theorem MINSET_ind:
278  ∀P. (∀x. sta x ⊆ bnfMINSET sta s ∧ (∀y. y ∈ sta x ⇒ P y) ⇒ P (s x)) ⇒
279      ∀x. x ∈ bnfMINSET sta s ⇒ P x
280Proof
281  gen_tac >> strip_tac >>
282  ‘bnfMINSET sta s ⊆ P INTER bnfMINSET sta s’
283    suffices_by simp[SUBSET_DEF, IN_DEF] >>
284  simp[MINSET_def, SimpL “$SUBSET”] >> irule BIGINTER_SUBSET >>
285  qexists_tac ‘P INTER bnfMINSET sta s’ >>
286  simp[ALG_def, SUBSET_DEF] >> rw[]
287  >- gs[IN_DEF, SUBSET_DEF] >>
288  ntac 2 (last_x_assum (K ALL_TAC)) >>
289  gs[ALG_def, SUBSET_DEF, IN_MINSET]
290QED
291
292Theorem MINSET_ind':
293  ∀P. (∀x. (∀y. y ∈ sta x ⇒ y ∈ bnfMINSET sta s ∧ P y) ⇒ P (s x)) ⇒
294      ∀x. x ∈ bnfMINSET sta s ⇒ P x
295Proof
296  metis_tac[MINSET_ind, SUBSET_DEF]
297QED
298
299Theorem MINSET_unique_homs:
300  bnfMapCong mp sta ∧
301  bnfHOM mp sta stb h1 (bnfMINSET sta s, s) (B,t) ∧
302  bnfHOM mp sta stb h2 (bnfMINSET sta s, s) (B,t) ⇒
303  ∀a. a ∈ bnfMINSET sta s ⇒ h1 a = h2 a
304Proof
305  simp[MapCong_def] >> strip_tac >>
306  ho_match_mp_tac MINSET_ind' >> gs[HOM_def] >>
307  rpt strip_tac >> RULE_ASSUM_TAC GSYM >> simp[] >> gs[SUBSET_DEF] >>
308  AP_TERM_TAC >> first_x_assum irule >> simp[]
309QED
310
311Definition SUBALG_def:
312  bnfSUBALG sta (A,s) (B,t) ⇔
313    bnfALG sta (A,s) ∧ bnfALG sta (B,t) ∧
314    (∀af. af ∈ bnfFIN sta A ⇒ s af = t af) ∧ A ⊆ B
315End
316
317Theorem SUBALGs_preserve_homs:
318  bnfSUBALG sta A1 A2 ∧ bnfHOM mp sta stb f A2 C ⇒ bnfHOM mp sta stb f A1 C
319Proof
320  Cases_on ‘A1’ >> Cases_on ‘A2’ >> Cases_on ‘C’ >>
321  simp[HOM_def, SUBALG_def] >> metis_tac[SUBSET_DEF]
322QED
323
324Theorem MINSET_SUBALG:
325  bnfALG sta (A,s) ⇒ bnfSUBALG sta (bnfMINSET sta s, s) (A,s)
326Proof
327  simp[SUBALG_def, MINSET_def] >> strip_tac >>
328  irule BIGINTER_SUBSET >> simp[] >> metis_tac[SUBSET_REFL]
329QED
330
331Theorem MINSET_I_HOM:
332  bnfMapId mp ⇒ bnfALG sta (A,s) ⇒ bnfHOM mp sta sta I (bnfMINSET sta s, s) (A,s)
333Proof
334  simp[MapId_def] >> rpt strip_tac >> drule MINSET_SUBALG >>
335  simp[HOM_def, SUBALG_def, SUBSET_DEF]
336QED
337
338(* ----------------------------------------------------------------------
339    The product of all algebras over a fixed carrier type.
340
341    A pair that isn't an algebra is coerced to one, so the product can be
342    indexed by the plain pair type and the construction needs no type
343    definition of its own.  'fp is F at the product's carrier.
344   ---------------------------------------------------------------------- *)
345
346Definition MKALG_def:
347  bnfMKALG (sta : 'f -> 'a set) p = if bnfALG sta p then p else (UNIV, SND p)
348End
349
350Theorem MKALG_ALG[simp]:
351  bnfALG sta (bnfMKALG sta p)
352Proof
353  rw[MKALG_def] >> Cases_on ‘p’ >> simp[]
354QED
355
356Theorem MKALG_ID:
357  bnfALG sta p ⇒ bnfMKALG sta p = p
358Proof
359  simp[MKALG_def]
360QED
361
362Definition BIGPROD_def:
363  bnfBIGPROD (mp : ((('a set # ('f -> 'a)) -> 'a) -> 'a) -> 'fp -> 'f) sta =
364    ({ ff : ('a set # ('f -> 'a)) -> 'a | ∀i. ff i ∈ FST (bnfMKALG sta i) },
365     λ(fv:'fp) i. SND (bnfMKALG sta i) (mp (λff. ff i) fv))
366End
367
368Theorem BIGPROD_ALG[simp]:
369  bnfNatural mp stp sta ⇒ bnfALG stp (bnfBIGPROD mp sta)
370Proof
371  simp[Natural_def] >> strip_tac >>
372  simp[BIGPROD_def, ALG_def] >> rpt strip_tac >>
373  Cases_on ‘bnfMKALG sta i’ >> rename [‘bnfMKALG sta i = (A,s)’] >>
374  ‘bnfALG sta (A,s)’ by metis_tac[MKALG_ALG] >> simp[] >>
375  gs[ALG_def] >> first_assum irule >>
376  gs[SUBSET_DEF, PULL_EXISTS] >> metis_tac[FST]
377QED
378
379Theorem BIGPROD_proj:
380  bnfNatural mp stp sta ⇒
381  bnfALG sta (A,s) ⇒
382  bnfHOM mp stp sta (λff. ff (A,s)) (bnfBIGPROD mp sta) (A,s)
383Proof
384  strip_tac >> strip_tac >> simp[HOM_def, BIGPROD_def] >> rpt strip_tac
385  >- metis_tac[BIGPROD_ALG, BIGPROD_def]
386  >- (‘bnfMKALG sta (A,s) = (A,s)’ by metis_tac[MKALG_ID] >>
387      first_x_assum $ qspec_then ‘(A,s)’ mp_tac >> simp[]) >>
388  ‘bnfMKALG sta (A,s) = (A,s)’ by metis_tac[MKALG_ID] >> simp[]
389QED
390
391(* ----------------------------------------------------------------------
392    Traytel's K function (MSc thesis, p 15): iterate the algebra's
393    operation through the ordinals until it closes off.
394   ---------------------------------------------------------------------- *)
395
396val KK_def = new_specification(
397  "KK_def", ["bnfKK"],
398  ord_RECURSION |> Q.ISPEC ‘∅ : 'c set’
399                |> Q.SPEC ‘λx r. r ∪ { s(x) | sta x ⊆ r }’
400                |> Q.SPEC ‘λx rs. BIGUNION rs’
401                |> SRULE[]
402                |> Q.GENL [‘sta’, ‘s’]
403                |> CONV_RULE (BINDER_CONV SKOLEM_CONV THENC SKOLEM_CONV));
404
405Theorem KK_mono:
406  ∀b a. a < b ⇒ bnfKK sta s a ⊆ bnfKK sta s b
407Proof
408  ho_match_mp_tac simple_ord_induction >>
409  simp[KK_def, ordlt_SUC_DISCRETE, DISJ_IMP_THM, FORALL_AND_THM] >>
410  rw[] >- metis_tac[IN_UNION, SUBSET_DEF] >>
411  gs[omax_NONE] >>
412  last_x_assum $ drule_then strip_assume_tac >>
413  first_x_assum $ drule_all_then assume_tac >>
414  irule SUBSET_BIGUNION_I >> simp[]
415QED
416
417Theorem KK_mono_LE:
418  ∀a b. a ≤ b ⇒ bnfKK sta s a ⊆ bnfKK sta s b
419Proof
420  metis_tac[SUBSET_REFL, KK_mono, ordle_lteq]
421QED
422
423Theorem KK_SUB_MINSET:
424  ∀a. bnfKK sta s a ⊆ bnfMINSET sta s
425Proof
426  ho_match_mp_tac simple_ord_induction >> simp[KK_def] >> rw[]
427  >- (simp[SUBSET_DEF, PULL_EXISTS] >> rpt strip_tac >>
428      ‘bnfALG sta (bnfMINSET sta s, s)’ by simp[] >>
429      gs[ALG_def, Excl "MINSET_is_ALG"] >>
430      metis_tac[SUBSET_DEF]) >>
431  simp[SUBSET_DEF, PULL_EXISTS] >> metis_tac[SUBSET_DEF]
432QED
433
434Theorem KK_fixp_is_ALG:
435  { s x | x | sta x ⊆ bnfKK sta s e } = bnfKK sta s e ⇒ bnfALG sta (bnfKK sta s e, s)
436Proof
437  rw[ALG_def] >> gs[EXTENSION] >> metis_tac[]
438QED
439
440Theorem KK_sup:
441  ords ≼ 𝕌(:num + 'g) ⇒
442  bnfKK sta s (sup ords : 'g ordinal) = BIGUNION (IMAGE (bnfKK sta s) ords)
443Proof
444  strip_tac >> Cases_on ‘ords = ∅’ >> simp[KK_def] >>
445  Cases_on ‘omax ords’
446  >- (gs[omax_NONE] >>
447      ‘islimit (sup ords)’
448        by (simp[omax_NONE, sup_thm, PULL_EXISTS] >>
449            metis_tac[ordlt_TRANS]) >>
450      Cases_on ‘sup ords = 0’ >- gs[KK_def, sup_EQ_0] >>
451      ‘0 < sup ords’ by metis_tac[IFF_ZERO_lt] >>
452      simp[KK_def] >> irule SUBSET_ANTISYM >>
453      simp[SUBSET_DEF, PULL_EXISTS, sup_thm] >> rw[] >>
454      metis_tac[SUBSET_DEF, KK_mono]) >>
455  gs[omax_SOME] >> rename [‘_ ≤ mx’, ‘mx ∈ ords’] >>
456  ‘sup ords = mx’ by metis_tac[sup_eq_max] >> simp[] >>
457  irule SUBSET_ANTISYM >> simp[SUBSET_DEF, PULL_EXISTS] >> rw[]
458  >- metis_tac[] >>
459  metis_tac[KK_mono_LE, SUBSET_DEF]
460QED
461
462Theorem KK_preds_subset:
463  BIGUNION (IMAGE (bnfKK sta s) (preds a)) ⊆ bnfKK sta s a
464Proof
465  qid_spec_tac ‘a’ >> ho_match_mp_tac simple_ord_induction >>
466  rw[]
467  >- (simp[KK_def, preds_ordSUC] >> irule SUBSET_TRANS >> goal_assum drule >>
468      simp[]) >>
469  simp[KK_def]
470QED
471
472Theorem KK_thm:
473  bnfKK sta s a = if a = 0 then ∅
474               else BIGUNION (IMAGE (λb. { s fv | fv | sta fv ⊆ bnfKK sta s b})
475                              (preds a))
476Proof
477  qid_spec_tac ‘a’ >> ho_match_mp_tac simple_ord_induction >>
478  rw[]
479  >- simp[KK_def]
480  >- (simp[preds_nat] >> ‘count 1 = {0}’ by simp[EXTENSION] >>
481      simp[KK_def, GSYM ORD_ONE, Excl "ORD_ONE"])
482  >- (qpat_x_assum ‘bnfKK _ _ _ = BIGUNION _’ (assume_tac o SYM) >>
483      simp[KK_def, preds_ordSUC, UNION_COMM]) >>
484  pop_assum (assume_tac o GSYM) >>
485  simp[KK_def] >> irule SUBSET_ANTISYM >> conj_tac >>
486  simp[Once SUBSET_DEF, PULL_EXISTS]
487  >- (rpt strip_tac >> rename [‘v ∈ bnfKK sta s b’] >>
488      ‘b ≠ 0’ by (strip_tac >> gs[KK_def]) >>
489      ‘bnfKK sta s b = BIGUNION (IMAGE (λb0. { s fv | fv | sta fv ⊆ bnfKK sta s b0})
490                              (preds b))’ by metis_tac[] >>
491      gs[PULL_EXISTS] >> metis_tac[ordlt_TRANS]) >>
492  rpt strip_tac >> rename [‘b < a’, ‘sta fv ⊆ bnfKK sta s b’] >>
493  qexists_tac ‘b⁺’ >> simp[KK_def] >> metis_tac[islimit_SUC_lt]
494QED
495
496(* ----------------------------------------------------------------------
497    The iteration closes off by csuc of the functor's bound.
498   ---------------------------------------------------------------------- *)
499
500Theorem sucbnd_suffices:
501  ω ≤ (bd : 'g ordinal) ∧ (∀x : 'f. sta x ≼ preds bd) ⇒
502  bnfALG sta (bnfKK sta (s : 'f -> 'a) (csuc bd), s)
503Proof
504  strip_tac >>
505  ‘INFINITE (preds bd)’ by (simp[FINITE_preds] >> rpt strip_tac >> gvs[]) >>
506  irule KK_fixp_is_ALG >> irule SUBSET_ANTISYM >> conj_tac >>
507  ONCE_REWRITE_TAC [SUBSET_DEF] >> simp[PULL_EXISTS] >>
508  rpt strip_tac
509  >- (rename [‘s fv ∈ bnfKK sta s _’] >>
510      drule_then strip_assume_tac csuc_is_nonzero_limit >>
511      simp[KK_def, PULL_EXISTS, lt_csuc] >>
512      gs[SUBSET_DEF, KK_def, PULL_EXISTS, lt_csuc] >>
513      gs[GSYM RIGHT_EXISTS_IMP_THM, SKOLEM_THM] >>
514      rename [‘_ ∈ bnfKK sta s (g _)’, ‘preds (g _) ≼ preds bd’] >>
515      qabbrev_tac ‘B = sup (IMAGE g $ sta fv)’ >>
516      ‘IMAGE g $ sta fv ≼ univ(:num + ('g + num -> bool))’
517        by (irule IMAGE_cardleq_rwt >>
518            first_assum (C (resolve_then (Pos hd) irule) cardleq_TRANS) >>
519            resolve_then (Pos hd) irule preds_inj_univ cardleq_TRANS >>
520            simp[cardleq_lteq, bumpUNIV_cardlt]) >>
521      ‘∀a. a < B ⇔ ∃v. v ∈ sta fv ∧ a < g v’
522        by simp[Abbr‘B’, sup_thm, PULL_EXISTS] >>
523      qexists_tac ‘B⁺’ >> simp[KK_def] >> reverse conj_tac
524      >- (simp[preds_ordSUC, INFINITE_cardleq_INSERT] >>
525          simp[Abbr‘B’, preds_sup, dclose_BIGUNION] >>
526          irule CARD_BIGUNION >>
527          simp[IMAGE_cardleq_rwt, PULL_EXISTS]) >>
528      ‘bnfKK sta s B = BIGUNION (IMAGE (bnfKK sta s) (IMAGE g (sta fv)))’
529        by simp[KK_sup, Abbr‘B’] >> disj2_tac >>
530      qexists_tac ‘fv’ >> simp[SUBSET_DEF, PULL_EXISTS] >> metis_tac[]) >>
531  rename [‘v ∈ bnfKK sta s (csuc bd)’] >>
532  drule_then strip_assume_tac csuc_is_nonzero_limit >>
533  gvs[KK_def] >>
534  rename [‘v ∈ bnfKK sta s a’, ‘a < csuc bd’] >>
535  qpat_x_assum ‘v ∈ bnfKK sta s a’ mp_tac >> simp[Once KK_thm] >> rw[] >>
536  gs[] >> qexists_tac ‘fv’ >> simp[] >> irule SUBSET_BIGUNION_SUBSET_I >>
537  simp[PULL_EXISTS] >> metis_tac[ordlt_TRANS]
538QED
539
540(* mp has to be annotated into the same instance as sta and s: the
541   parameterisation makes that explicit where a real functor would have
542   made it implicit *)
543Theorem KKbnd_EQ_MINSET:
544  bnfMapId (mp : ('a -> 'a) -> 'f -> 'f) ⇒
545  ω ≤ (bd : 'g ordinal) ∧ (∀x : 'f. (sta : 'f -> 'a set) x ≼ preds bd) ⇒
546  bnfKK sta (s : 'f -> 'a) (csuc bd) = bnfMINSET sta s
547Proof
548  strip_tac >> strip_tac >>
549  drule_all_then (qspec_then ‘s’ assume_tac) sucbnd_suffices >>
550  irule SUBSET_ANTISYM >> simp[KK_SUB_MINSET] >>
551  ‘bnfHOM mp sta sta I (bnfMINSET sta s, s) (bnfKK sta s (csuc bd), s)’
552    by (irule MINSET_I_HOM >> simp[]) >>
553  gs[HOM_def, SUBSET_DEF]
554QED
555
556(* ----------------------------------------------------------------------
557    Because F is not constant, an algebra's carrier is no bigger than the
558    collection of F-values over it.
559   ---------------------------------------------------------------------- *)
560
561Theorem NontrivialBs:
562  bnfNatural (mp : ('c -> 'a) -> 'h -> 'f) stc sta ⇒
563  (∃x:'h. stc x ≠ ∅) ⇒
564  ∀B:'a set. B ≼ bnfFIN sta B
565Proof
566  simp[Natural_def] >> strip_tac >> strip_tac >> strip_tac >>
567  simp[cardleq_def] >>
568  qexists_tac ‘λb. mp (K b) x’ >> simp[INJ_IFF] >>
569  conj_tac >- simp[SUBSET_DEF, PULL_EXISTS] >>
570  rpt strip_tac >> iff_tac >> simp[] >> strip_tac >>
571  ‘IMAGE (K b) (stc x) = IMAGE (K b') (stc x)’ by metis_tac[] >>
572  gs[GSYM MEMBER_NOT_EMPTY] >>
573  qpat_x_assum ‘IMAGE _ _ = IMAGE _ _’ mp_tac >>
574  simp[Once EXTENSION] >> metis_tac[]
575QED
576
577Theorem FIN_MONO:
578  s ⊆ t ⇒ (bnfFIN sta s : 'f set) ⊆ bnfFIN sta t
579Proof
580  simp[SUBSET_DEF] >> metis_tac[]
581QED
582
583Theorem FIN_cardleq:
584  bnfMapId (mp_aa : ('a -> 'a) -> 'f -> 'f) ∧ bnfMapCong mp_aa sta ∧
585  bnfNatural (mp_ab : ('a -> 'b) -> 'f -> 'g) sta stb ∧
586  bnfMapComp mp_ab (mp_ba : ('b -> 'a) -> 'g -> 'f) mp_aa ⇒
587  s ≼ t ⇒ (bnfFIN sta s : 'f set) ≼ (bnfFIN stb t : 'g set)
588Proof
589  strip_tac >>
590  drule_then (drule_then assume_tac) Map_eq_id >>
591  simp[cardleq_def] >>
592  disch_then $ qx_choose_then ‘f’ strip_assume_tac >>
593  qexists_tac ‘mp_ab f’ >> gs[Natural_def, INJ_IFF] >>
594  rpt strip_tac >- gs[SUBSET_DEF, PULL_EXISTS, INJ_IFF] >>
595  iff_tac >> simp[] >> strip_tac >>
596  ‘mp_ba (LINV f s) (mp_ab f x) = mp_ba (LINV f s) (mp_ab f y)’ by simp[] >>
597  gs[MapComp_def] >>
598  ‘INJ f s t’ by simp[INJ_IFF] >>
599  drule_then assume_tac LINV_DEF >>
600  ‘mp_aa (LINV f s o f) x = x ∧ mp_aa (LINV f s o f) y = y’
601    by (conj_tac >> first_x_assum irule >> gs[SUBSET_DEF]) >>
602  gs[]
603QED
604
605(* ----------------------------------------------------------------------
606    The cardinality bound.  Beyond the map and set functions this needs
607    F at the ordinal carrier as well, and the facts it uses about
608    nontriviality are taken as hypotheses rather than re-derived, so the
609    driver discharges them once with NontrivialBs.
610
611    See Lemma 33 of Blanchette, Popescu and Traytel, "Cardinals in
612    Isabelle/HOL", ITP 2014.
613   ---------------------------------------------------------------------- *)
614
615Overload "𝟙"[local] = “{()}”
616
617(* CARDEQ_IMP_CARDLEQ and cardleq_INFINITE duplicate cardinalTheory's
618   CARDEQ_SUBSET_CARDLEQ and CARD_LE_INFINITE, which this theory already
619   has as an ancestor; they should be dropped in favour of those.  The
620   two below them are genuine local instantiations. *)
621Theorem CARDEQ_IMP_CARDLEQ[local]:
622  ∀s t. s ≈ t ⇒ s ≼ t
623Proof
624  metis_tac[cardleq_lteq]
625QED
626
627Theorem ordlt_preds_mono[local]:
628  a < b ⇒ preds a ≼ preds b
629Proof
630  strip_tac >> irule CARD_LE_SUBSET >> simp[SUBSET_DEF] >>
631  metis_tac[ordlt_TRANS]
632QED
633
634Theorem cardleq_INFINITE[local]:
635  ∀s t. INFINITE s ∧ s ≼ t ⇒ INFINITE t
636Proof
637  metis_tac[CARD_LE_FINITE]
638QED
639
640Theorem CBDb:
641  bnfNatural (mp_a2o : ('a -> 'g ordinal) -> 'f -> 'fo) sta sto ∧
642  bnfNatural (mp_o2a : ('g ordinal -> 'a) -> 'fo -> 'f) sto sta ∧
643  bnfMapComp mp_a2o mp_o2a (mp_aa : ('a -> 'a) -> 'f -> 'f) ∧
644  bnfMapId mp_aa ∧ bnfMapCong mp_aa sta ∧
645  (∀C : 'g ordinal set. C ≼ bnfFIN sto C) ⇒
646  ω ≤ (bd : 'g ordinal) ∧ (∀x:'f. sta x ≼ preds bd) ⇒
647  ∀B:'a set. 𝟚 ≼ B ⇒
648             (bnfFIN sta B : 'f set) ≼ B ** cardSUC (bnfFIN sto (preds bd))
649Proof
650  strip_tac >>
651  drule_then (drule_then assume_tac) Map_eq_id >>
652  rpt strip_tac >>
653  qabbrev_tac ‘kA = (bnfFIN sto (preds bd) : 'fo set) CROSS (B ** preds bd)’ >>
654  qmatch_abbrev_tac ‘_ ≼ B ** k’ >>
655  ‘kA ≼ B ** k’
656    by (simp[Abbr‘k’, Abbr‘kA’] >> irule CARD_MUL2_ABSORB_LE >>
657        simp[] >> rpt strip_tac >~
658        [‘𝟚 ≼ B’, ‘B ≼ 𝟙’] >- (drule_all cardleq_TRANS >> simp[]) >~
659        [‘INFINITE (bnfFIN sto (preds bd))’]
660        >- (disj2_tac >>
661            irule (ISPEC “preds (bd:'g ordinal)” cardleq_INFINITE) >>
662            qexists_tac ‘bd’ >> conj_tac
663            >- (simp[FINITE_preds] >> rpt strip_tac >> gvs[]) >>
664            simp[]) >~
665        [‘bnfFIN sto (preds bd) ≼ B ** cardSUC _’]
666        >- (resolve_then (Pos last) irule CARD_LE_EXP cardleq_TRANS >>
667            simp[]) >>
668        irule set_exp_cardle_cong >> simp[] >> rpt strip_tac >>
669        gvs[cardleq_empty] >>
670        first_x_assum $ qspec_then ‘preds bd’ assume_tac >>
671        first_x_assum $ C (resolve_then (Pos hd) irule) cardleq_TRANS >>
672        simp[]) >>
673  first_assum $ C (resolve_then (Pos last) irule) cardleq_TRANS >>
674  qabbrev_tac ‘d = λ(y:'fo,fn). mp_o2a fn y’ >>
675  simp[cardleq_def] >>
676  irule_at Any (SRULE [PULL_EXISTS] SURJ_IMP_INJ) >> qexists_tac ‘d’ >>
677  simp[SURJ_DEF] >> conj_tac
678  >- (simp[FORALL_PROD, Abbr‘kA’, Abbr‘d’, set_exp_def] >>
679      gs[Natural_def] >> rw[] >> simp[SUBSET_DEF, PULL_EXISTS] >>
680      qx_gen_tac ‘b’ >> strip_tac >>
681      ‘b ∈ preds bd’ by metis_tac[SUBSET_DEF] >> gs[] >>
682      first_assum drule >> simp[PULL_EXISTS]) >>
683  qx_gen_tac ‘vf’ >> strip_tac >>
684  ‘?g. INJ g (sta vf) (preds bd)’ by metis_tac[cardleq_def] >>
685  qabbrev_tac ‘y = mp_a2o g vf’ >>
686  ‘sta vf ⊆ B’ by gs[] >>
687  ‘?fn. (!b. b ∈ sta vf ⇒ fn (g b) = b) /\ (!bp. bp < bd ==> fn bp ∈ B)’
688    by (‘?be. be ∈ B’ by (simp[MEMBER_NOT_EMPTY] >>
689                          strip_tac >> gvs[cardleq_empty]) >>
690        qexists_tac ‘λbp. case some b. b IN sta vf /\ g b = bp of
691                            NONE => be
692                          | SOME b => b
693                    ’ >> conj_tac >> simp[] >> rpt strip_tac
694        >- (gs[INJ_IFF, SF CONJ_ss] >> csimp[]) >>
695        DEEP_INTRO_TAC optionTheory.some_intro >> simp[] >>
696        gs[SUBSET_DEF]) >>
697  qexists_tac ‘(y, λbp. if bp ∈ preds bd then fn bp else ARB)’ >>
698  conj_tac
699  >- (simp[Abbr‘kA’, Abbr‘y’] >> gs[Natural_def] >> conj_tac
700      >- gs[INJ_IFF, SUBSET_DEF, PULL_EXISTS] >>
701      simp[set_exp_def]) >>
702  simp[Abbr‘d’, Abbr‘y’] >> gs[MapComp_def] >>
703  first_x_assum irule >> simp[] >> gs[INJ_IFF]
704QED
705
706Theorem preds_bd_lemma:
707  (∀C : 'g ordinal set. C ≼ bnfFIN sto C) ⇒
708  preds (bd:'g ordinal) ≼
709  preds (oleast a:'fo ordinal. preds a ≈ (bnfFIN sto (preds bd) : 'fo set))
710Proof
711  strip_tac >> first_x_assum (qspec_then ‘preds bd’ assume_tac) >>
712  pop_assum mp_tac >>
713  simp[Once cardleq_lteq, SimpL “$==>”] >> strip_tac
714  >- (DEEP_INTRO_TAC oleast_intro >> conj_tac
715      >- (irule cardeq_ordinals_exist >>
716          simp[Once disjUNION_UNIV] >>
717          resolve_then (Pos hd) irule CARD_LE_UNIV CARD_LE_TRANS >>
718          simp[CARD_LE_ADDL]) >>
719      metis_tac[cardleq_lteq, CARD_LT_CONG, CARD_EQ_REFL]) >>
720  DEEP_INTRO_TAC oleast_intro >> conj_tac
721  >- (irule cardeq_ordinals_exist >>
722      simp[Once disjUNION_UNIV] >>
723      resolve_then (Pos hd) irule CARD_LE_UNIV CARD_LE_TRANS >>
724      simp[CARD_LE_ADDL]) >>
725  metis_tac[CARD_LE_REFL, CARD_LE_CONG]
726QED
727
728Theorem preds_csuc_lemma:
729  preds a ≼ preds (csuc a)
730Proof
731  simp[csuc_def] >> DEEP_INTRO_TAC oleast_intro >>
732  simp[cardinality_bump_exists] >> metis_tac[cardleq_lteq]
733QED
734
735(* the middle set of a cardleq_TRANS chain has a type of its own, and
736   irule cannot guess it; INST_TYPE says which one is meant *)
737Theorem preds_cardSUC_cardleq[local]:
738  preds (i:'i ordinal) ≼ preds (bd:'bo ordinal) ∧
739  preds bd ≼ preds (oleast a:'fo ordinal. preds a ≈ (Q : 'fo set)) ⇒
740  preds i ≼ cardSUC Q
741Proof
742  simp[cardSUC_def] >> strip_tac >>
743  irule (INST_TYPE [beta |-> “:'bo ordinal”] cardleq_TRANS) >>
744  qexists_tac ‘preds bd’ >> simp[] >>
745  irule (INST_TYPE [beta |-> “:'fo ordinal”] cardleq_TRANS) >>
746  qexists_tac ‘preds (oleast a:'fo ordinal. preds a ≈ Q)’ >> simp[] >>
747  MATCH_ACCEPT_TAC preds_csuc_lemma
748QED
749
750Theorem cardADD2[local]:
751  s ≼ s +_c 𝟚
752Proof
753  simp[CARD_LE_ADDR]
754QED
755
756(* The bound on the iteration.  This asks only for the *conclusions* of
757   FIN_cardleq and CBDb at the instances it uses, so the driver chains
758   the lemmas rather than re-supplying their hypotheses here. *)
759Theorem ALG_cardinality_bound:
760  (∀C : 'g ordinal set. C ≼ bnfFIN sto C) ∧
761  (∀u:'a set. ∀v:('a + bool) set.
762     u ≼ v ⇒ (bnfFIN sta u : 'f set) ≼ (bnfFIN stab v : 'fab set)) ∧
763  (∀B : ('a + bool) set.
764     𝟚 ≼ B ⇒ (bnfFIN stab B : 'fab set) ≼ B ** cardSUC (bnfFIN sto (preds bd))) ⇒
765  ω ≤ (bd : 'g ordinal) ⇒
766  bnfKK sta (s : 'f -> 'a) (csuc bd) ≼ 𝟚 ** cardSUC (bnfFIN sto (preds bd))
767Proof
768  strip_tac >> strip_tac >>
769  qmatch_abbrev_tac ‘_ ≼ 𝟚 ** BD’ >>
770  ‘INFINITE BD’
771    by (simp[Abbr‘BD’] >>
772        irule (ISPEC “preds (bd:'g ordinal)” cardleq_INFINITE) >>
773        qexists_tac ‘bd’ >> conj_tac
774        >- (simp[FINITE_preds] >> rpt strip_tac >> gvs[]) >>
775        simp[]) >>
776  ‘BD ≠ ∅’ by (rpt strip_tac >> gs[]) >>
777  qpat_assum ‘∀C. _ ≼ bnfFIN sto _’ (assume_tac o MATCH_MP preds_bd_lemma) >>
778  ‘∀i. i < csuc bd ⇒ bnfKK sta s i ≼ 𝟚 ** BD’
779    suffices_by (strip_tac >> simp[KK_def, csuc_is_nonzero_limit] >>
780                 irule CARD_BIGUNION >> simp[PULL_EXISTS] >>
781                 irule IMAGE_cardleq_rwt >>
782                 resolve_then Any
783                              (fn th =>
784                                 resolve_then (Pos hd) irule th cardleq_TRANS)
785                              cardleq_REFL
786                              CARD_LE_EXP >>
787                 irule set_exp_cardle_cong >> simp[Abbr‘BD’, cardSUC_def] >>
788                 irule cardleq_preds_csuc >> simp[]) >>
789  ho_match_mp_tac ord_induction >> rw[] >>
790  simp[Once KK_thm] >> rw[] >> irule CARD_BIGUNION >>
791  simp[PULL_EXISTS] >> rpt conj_tac >~
792  [‘IMAGE _ (preds i) ≼ _’]
793  >- (irule IMAGE_cardleq_rwt >> gs[lt_csuc] >>
794      resolve_then Any
795                   (fn th =>
796                      resolve_then (Pos hd) irule th cardleq_TRANS)
797                   cardleq_REFL
798                   CARD_LE_EXP >> irule set_exp_cardle_cong >> simp[] >>
799      simp[Abbr‘BD’] >>
800      drule_all_then MATCH_ACCEPT_TAC preds_cardSUC_cardleq) >>
801  qx_gen_tac ‘j’ >> strip_tac >>
802  ‘{ s fv | fv | sta fv ⊆ bnfKK sta s j} = IMAGE s (bnfFIN sta (bnfKK sta s j))’
803    by simp[EXTENSION] >> simp[] >>
804  irule IMAGE_cardleq_rwt >>
805  ‘(bnfFIN sta (bnfKK sta s j) : 'f set) ≼ (bnfFIN stab (bnfKK sta s j +_c 𝟚) : 'fab set)’
806    by (first_x_assum irule >> simp[CARD_LE_ADDR]) >>
807  pop_assum (C (resolve_then (Pos hd) irule) cardleq_TRANS) >>
808  first_x_assum (qspec_then ‘bnfKK sta s j +_c 𝟚’ mp_tac) >>
809  impl_tac >- simp[CARD_LE_ADDL] >>
810  disch_then $ C (resolve_then (Pos hd) irule) cardleq_TRANS >>
811  first_x_assum $ qspec_then ‘j’ mp_tac >> simp[] >>
812  impl_tac >- metis_tac[ordlt_TRANS] >>
813  disch_then
814    (C (resolve_then (Pos hd) (qspecl_then [‘𝟚’, ‘𝟚’] mp_tac)) CARD_LE_ADD) >>
815  simp[] >> strip_tac >>
816  pop_assum (
817    C (resolve_then (Pos (el 2)) (resolve_then (Pos last)
818                                  (qspec_then ‘BD’ mp_tac) cardleq_REFL))
819    set_exp_cardle_cong) >>
820  impl_tac >- simp[] >>
821  disch_then (C (resolve_then (Pos hd) irule) cardleq_TRANS) >>
822  ‘𝟚 ≼ 𝟚 ** BD’ by (simp[cardleq_setexp]) >>
823  ‘INFINITE (𝟚 ** BD)’ by simp[] >>
824  ‘𝟚 ** BD +_c 𝟚 ≈ 𝟚 ** BD’
825    by metis_tac[CARD_ADD_SYM, CARD_ADD_ABSORB, cardeq_TRANS] >>
826  ‘(𝟚 ** BD +_c 𝟚) ** BD ≼ (𝟚 ** BD) ** BD’
827    by (irule CARDEQ_IMP_CARDLEQ >> irule set_exp_card_cong >> simp[]) >>
828  ‘(𝟚 ** BD) ** BD ≼ 𝟚 ** (BD CROSS BD)’
829    by (irule CARDEQ_IMP_CARDLEQ >> MATCH_ACCEPT_TAC set_exp_product) >>
830  ‘𝟚 ** (BD CROSS BD) ≼ 𝟚 ** BD’
831    by (irule set_exp_cardle_cong >> simp[] >>
832        ONCE_REWRITE_TAC [cardleq_lteq] >> simp[CARD_SQUARE_INFINITE]) >>
833  metis_tac[cardleq_TRANS]
834QED
835
836(* ----------------------------------------------------------------------
837    An algebra can be copied onto any carrier big enough to hold it.
838   ---------------------------------------------------------------------- *)
839
840(* mp_aa and B are quantified out in front because neither appears in
841   the conclusion: irule then turns them into existentials in this
842   order, so a use site can name them with qexistsl_tac rather than
843   leaving them to be guessed *)
844Theorem copy_alg_back:
845  ∀(mp_aa : ('a -> 'a) -> 'f -> 'f) (B : 'b set).
846    bnfNatural (mp_ba : ('b -> 'a) -> 'g -> 'f) stb sta ∧
847    bnfNatural (mp_ab : ('a -> 'b) -> 'f -> 'g) sta stb ∧
848    bnfMapComp mp_ab mp_ba mp_aa ∧ bnfMapId mp_aa ∧ bnfMapCong mp_aa sta ∧
849    (A:'a set) ≼ B ∧ bnfALG sta (A, s : 'f -> 'a) ⇒
850    ∃(B0:'b set) (s' : 'g -> 'b) h j.
851      bnfHOM mp_ba stb sta h (B0,s') (A,s) ∧
852      bnfHOM mp_ab sta stb j (A,s) (B0,s') ∧
853      (∀a. a ∈ A ⇒ h (j a) = a) ∧ (∀b. b ∈ B0 ⇒ j (h b) = b)
854Proof
855  rpt gen_tac >> simp[cardleq_def] >> strip_tac >>
856  drule_then (drule_then assume_tac) Map_eq_id >>
857  rename [‘INJ h0 A B’] >>
858  qexistsl_tac [‘IMAGE h0 A’, ‘λbv. h0 (s (mp_ba (LINV h0 A) bv))’,
859                ‘LINV h0 A’, ‘h0’] >>
860  csimp[HOM_def, PULL_EXISTS] >>
861  drule_then assume_tac LINV_DEF >> gs[Natural_def] >> rw[] >~
862  [‘bnfALG stb (IMAGE h0 A, _)’]
863  >- (gs[ALG_def, SUBSET_DEF] >> rw[] >>
864      irule_at Any EQ_REFL >> first_assum irule >>
865      simp[PULL_EXISTS] >> rw[] >> first_assum drule >>
866      simp[PULL_EXISTS]) >~
867  [‘LINV h0 A (h0 (s _))’]
868  >- (‘s (mp_ba (LINV h0 A) bv) ∈ A’
869        by (gs[ALG_def] >> first_assum irule >>
870            gs[SUBSET_DEF, PULL_EXISTS] >> rw[] >>
871            first_assum drule >> simp[PULL_EXISTS]) >>
872      simp[]) >>
873  gs[MapComp_def] >> ntac 2 AP_TERM_TAC >>
874  first_x_assum irule >> gs[SUBSET_DEF]
875QED
876
877(* ----------------------------------------------------------------------
878    The whole cardinality argument, as one theorem.
879
880    Its hypotheses are BNF laws at three instances — the carrier 'a, the
881    carrier extended by a point, and the ordinals that bound F's sets —
882    plus F's non-triviality and the bound itself.  A package instantiates
883    it and gets the one fact the construction needs: every minimal
884    algebra fits inside a set fixed by F alone.
885   ---------------------------------------------------------------------- *)
886
887(* the step from the bound to a whole type, which is the form the
888   construction's hypothesis takes *)
889Theorem CARDLEQ_UNIV[simp]:
890  ∀s : 'a set. s ≼ 𝕌(:'a)
891Proof
892  gen_tac >> irule SUBSET_CARDLEQ >> simp[]
893QED
894
895(* getting from F's own bound, which is a set, to an ordinal one *)
896Theorem cardeq_preds_omega:
897  INFINITE B ∧ preds (bd:'g ordinal) ≈ B ⇒ ω ≤ bd
898Proof
899  strip_tac >> irule omega_LEQ_INFINITE_preds >>
900  metis_tac[CARD_FINITE_CONG]
901QED
902
903Theorem cardeq_preds_bound:
904  preds (bd:'g ordinal) ≈ (B:'b set) ∧ (s:'s set) ≼ B ⇒ s ≼ preds bd
905Proof
906  strip_tac >> irule (INST_TYPE [beta |-> “:'b”] cardleq_TRANS) >>
907  qexists_tac ‘B’ >> simp[] >> irule CARDEQ_IMP_CARDLEQ >>
908  simp[Once cardeq_SYM]
909QED
910
911Theorem MINSET_CARDLEQ:
912  bnfMapId (mp_aa : ('a -> 'a) -> 'f -> 'f) ∧ bnfMapCong mp_aa sta ∧
913  bnfNatural (mp_ab : ('a -> 'a + bool) -> 'f -> 'fab) sta stab ∧
914  bnfMapComp mp_ab (mp_ba : ('a + bool -> 'a) -> 'fab -> 'f) mp_aa ∧
915  bnfMapId (mp_bb : ('a + bool -> 'a + bool) -> 'fab -> 'fab) ∧
916  bnfMapCong mp_bb stab ∧
917  bnfNatural (mp_bo : ('a + bool -> 'g ordinal) -> 'fab -> 'fo) stab sto ∧
918  bnfNatural (mp_ob : ('g ordinal -> 'a + bool) -> 'fo -> 'fab) sto stab ∧
919  bnfMapComp mp_bo mp_ob mp_bb ∧
920  bnfNatural (mp_oo : ('g ordinal -> 'g ordinal) -> 'fo -> 'fo) sto sto ∧
921  (∃x : 'fo. sto x ≠ ∅) ∧
922  ω ≤ (bd : 'g ordinal) ∧ (∀x. sta x ≼ preds bd) ∧
923  (∀x. stab x ≼ preds bd) ⇒
924  ∀s. bnfMINSET sta (s : 'f -> 'a) ≼ 𝟚 ** cardSUC (bnfFIN sto (preds bd))
925Proof
926  strip_tac >> gen_tac >>
927  ‘∀C : 'g ordinal set. C ≼ bnfFIN sto C’
928    by (byrule NontrivialBs [‘bnfNatural mp_oo sto sto’] irule >>
929        qpat_assum ‘sto _ ≠ ∅’ (irule_at Any)) >>
930  ‘∀u:'a set. ∀v:('a + bool) set.
931     u ≼ v ⇒ (bnfFIN sta u : 'f set) ≼ (bnfFIN stab v : 'fab set)’
932    by (rpt strip_tac >>
933        byrule FIN_cardleq
934          [‘bnfMapId mp_aa’, ‘bnfMapCong mp_aa sta’, ‘bnfNatural mp_ab sta stab’,
935           ‘bnfMapComp mp_ab mp_ba mp_aa’]
936          irule >> simp[]) >>
937  ‘∀B : ('a + bool) set.
938     𝟚 ≼ B ⇒ (bnfFIN stab B : 'fab set) ≼ B ** cardSUC (bnfFIN sto (preds bd))’
939    by (byrule CBDb
940          [‘bnfNatural mp_bo stab sto’, ‘bnfNatural mp_ob sto stab’,
941           ‘bnfMapComp mp_bo mp_ob mp_bb’, ‘bnfMapId mp_bb’, ‘bnfMapCong mp_bb stab’,
942           ‘∀C : 'g ordinal set. C ≼ bnfFIN sto C’]
943          (fn th => mp_tac th >> simp[])) >>
944  byrule KKbnd_EQ_MINSET [‘bnfMapId mp_aa’]
945    (fn th => ‘bnfKK sta s (csuc bd) = bnfMINSET sta s’ by (irule th >> simp[])) >>
946  pop_assum (SUBST1_TAC o SYM) >>
947  byrule ALG_cardinality_bound
948    [‘∀C : 'g ordinal set. C ≼ bnfFIN sto C’,
949     ‘∀u:'a set. ∀v:('a + bool) set. u ≼ v ⇒ _’,
950     ‘∀B : ('a + bool) set. 𝟚 ≼ B ⇒ _’]
951    (fn th => irule th >> simp[])
952QED
953
954(* ----------------------------------------------------------------------
955    The initial algebra: the minimal sub-algebra of the product of all
956    algebras over the bounded carrier type.
957
958    Both are parameterised by the same data as bnfBIGPROD, so nothing here
959    is specific to a functor.
960   ---------------------------------------------------------------------- *)
961
962Definition ICONS_def:
963  bnfICONS (mp : ((('a set # ('f -> 'a)) -> 'a) -> 'a) -> 'fp -> 'f) sta =
964    SND (bnfBIGPROD mp sta)
965End
966
967Definition IALG_def:
968  bnfIALG stp (mp : ((('a set # ('f -> 'a)) -> 'a) -> 'a) -> 'fp -> 'f) sta =
969    bnfMINSET stp (bnfICONS mp sta)
970End
971
972Theorem BIGPROD_ALG'[simp]:
973  bnfNatural mp stp sta ⇒ bnfALG stp (FST (bnfBIGPROD mp sta), bnfICONS mp sta)
974Proof
975  strip_tac >> drule BIGPROD_ALG >> simp[ICONS_def]
976QED
977
978Theorem BIGPROD_proj':
979  bnfNatural mp stp sta ⇒ bnfALG sta (A,s) ⇒
980  bnfHOM mp stp sta (λff. ff (A,s)) (FST (bnfBIGPROD mp sta), bnfICONS mp sta) (A,s)
981Proof
982  rpt strip_tac >> drule_all BIGPROD_proj >> simp[ICONS_def]
983QED
984
985Theorem IALG_ALG[simp]:
986  bnfALG stp (bnfIALG stp mp sta, bnfICONS mp sta)
987Proof
988  simp[IALG_def]
989QED
990
991Theorem IALG_I_HOM:
992  bnfMapId mp_pp ∧ bnfNatural mp_pa stp sta ⇒
993  bnfHOM mp_pp stp stp I (bnfIALG stp mp_pa sta, bnfICONS mp_pa sta)
994      (FST (bnfBIGPROD mp_pa sta), bnfICONS mp_pa sta)
995Proof
996  strip_tac >> simp[IALG_def] >> irule MINSET_I_HOM >> simp[]
997QED
998
999(* ----------------------------------------------------------------------
1000    Homomorphisms out of the initial algebra are unique only on its
1001    carrier, so pick the representative that is ARB elsewhere.
1002   ---------------------------------------------------------------------- *)
1003
1004Definition ARBIFY_def:
1005  bnfARBIFY A f x = if x ∈ A then f x else ARB
1006End
1007
1008Theorem HOM_ARBIFY:
1009  bnfMapCong mp sta ⇒
1010  (bnfHOM mp sta stb (bnfARBIFY A f) (A,s) (B,t) ⇔ bnfHOM mp sta stb f (A,s) (B,t))
1011Proof
1012  simp[MapCong_def] >> strip_tac >>
1013  simp[HOM_def, ARBIFY_def] >> Cases_on ‘bnfALG sta (A,s)’ >> simp[] >>
1014  ‘∀af. af ∈ bnfFIN sta A ⇒ s af ∈ A’ by gs[ALG_def] >> simp[] >>
1015  rw[EQ_IMP_THM] >> RULE_ASSUM_TAC GSYM >> simp[] >> AP_TERM_TAC >>
1016  first_x_assum irule >> simp[ARBIFY_def] >> gs[SUBSET_DEF]
1017QED
1018
1019Theorem HOM_arbification:
1020  bnfMapCong mp sta ⇒
1021  bnfHOM mp sta stb h (A,s) (B,t) ⇒
1022  ∃j. bnfHOM mp sta stb j (A,s) (B,t) ∧ ∀x. x ∉ A ⇒ j x = ARB
1023Proof
1024  rpt strip_tac >> qexists_tac ‘bnfARBIFY A h’ >>
1025  simp[ARBIFY_def] >> drule (iffRL HOM_ARBIFY) >> simp[]
1026QED
1027
1028(* ----------------------------------------------------------------------
1029    Existence of a homomorphism out of the initial algebra.
1030
1031    The chain is
1032        bnfIALG --I--> bnfBIGPROD --proj--> (B0,s') --hh--> bnfMINSET stc t --I--> G
1033    where (B0,s') is the minimal sub-algebra of (G,t) copied onto the
1034    bounded carrier type 'a, which is what makes it an index of the
1035    product.
1036   ---------------------------------------------------------------------- *)
1037
1038Theorem IALG_HOM_ANY:
1039  bnfNatural (mp_pa : ((('a set # ('f -> 'a)) -> 'a) -> 'a) -> 'fp -> 'f)
1040          stp sta ∧
1041  bnfNatural mp_pp stp stp ∧ bnfMapId mp_pp ∧ bnfMapComp mp_pp mp_pa mp_pa ∧
1042  bnfNatural mp_pc stp (stc : 'fc -> 'c set) ∧ bnfMapComp mp_pa mp_ac mp_pc ∧
1043  bnfMapComp mp_pc mp_cc mp_pc ∧
1044  bnfNatural mp_ac sta stc ∧ bnfNatural mp_ca stc sta ∧
1045  bnfMapComp mp_ca mp_ac mp_cc ∧ bnfMapId mp_cc ∧ bnfMapCong mp_cc stc ∧
1046  (∀t : 'fc -> 'c. bnfMINSET stc t ≼ 𝕌(:'a)) ⇒
1047  ∀t G. bnfALG stc (G,t) ⇒
1048        ∃h. bnfHOM mp_pc stp stc h (bnfIALG stp mp_pa sta, bnfICONS mp_pa sta) (G,t)
1049Proof
1050  strip_tac >> rpt strip_tac >>
1051  (* the minimal sub-algebra of (G,t), copied onto the bounded carrier *)
1052  ‘∃B0 s' hh jj.
1053     bnfHOM mp_ac sta stc hh (B0,s') (bnfMINSET stc t, t) ∧
1054     bnfHOM mp_ca stc sta jj (bnfMINSET stc t, t) (B0,s') ∧
1055     (∀a. a ∈ bnfMINSET stc t ⇒ hh (jj a) = a) ∧
1056     (∀b. b ∈ B0 ⇒ jj (hh b) = b)’
1057    by (irule copy_alg_back >> simp[] >> rpt conj_tac >~
1058        [‘bnfMINSET stc t ≼ _’] >- (qexists_tac ‘𝕌(:'a)’ >> simp[]) >>
1059        qexists_tac ‘mp_cc’ >> simp[]) >>
1060  ‘bnfALG sta (B0,s')’ by gs[HOM_def] >>
1061  (* being an algebra on the bounded carrier, (B0,s') indexes the
1062     product, so the product projects onto it *)
1063  ‘bnfHOM mp_pa stp sta (λff. ff (B0,s'))
1064       (FST (bnfBIGPROD mp_pa sta), bnfICONS mp_pa sta) (B0,s')’
1065    by (irule BIGPROD_proj' >> simp[]) >>
1066  ‘bnfHOM mp_pp stp stp I (bnfIALG stp mp_pa sta, bnfICONS mp_pa sta)
1067       (FST (bnfBIGPROD mp_pa sta), bnfICONS mp_pa sta)’
1068    by (irule IALG_I_HOM >> simp[]) >>
1069  byrule HOMs_compose
1070    [‘bnfMapComp mp_pp mp_pa mp_pa’, ‘bnfNatural mp_pp stp stp’,
1071     ‘bnfHOM mp_pp stp stp I _ _’, ‘bnfHOM mp_pa stp sta _ _ (B0,s')’]
1072    assume_tac >>
1073  byrule HOMs_compose
1074    [‘bnfMapComp mp_pa mp_ac mp_pc’, ‘bnfNatural mp_pa stp sta’,
1075     ‘bnfHOM mp_pa stp sta (_ o I) (bnfIALG stp mp_pa sta, _) _’,
1076     ‘bnfHOM mp_ac sta stc hh _ (bnfMINSET stc t, t)’]
1077    assume_tac >>
1078  ‘bnfHOM mp_cc stc stc I (bnfMINSET stc t, t) (G,t)’
1079    by (irule MINSET_I_HOM >> simp[]) >>
1080  byrule HOMs_compose
1081    [‘bnfMapComp mp_pc mp_cc mp_pc’, ‘bnfNatural mp_pc stp stc’,
1082     ‘bnfHOM mp_pc stp stc _ (bnfIALG stp mp_pa sta, _) (bnfMINSET stc t, t)’,
1083     ‘bnfHOM mp_cc stc stc I _ (G,t)’]
1084    (irule_at Any)
1085QED
1086
1087(* ----------------------------------------------------------------------
1088    A bound stated at one type is a bound at any type in bijection with
1089    it.
1090
1091    The construction states its bound at the type the minimal sets live
1092    in, and that type writes the functor out over the ordinals -- so
1093    every leaf of every law about it carries a type hundreds of times
1094    its own size.  This is what lets the bound be carried onto a type
1095    defined to stand for it, which the laws are then about instead.
1096   ---------------------------------------------------------------------- *)
1097
1098Theorem cardleq_ACROSS_BIJ:
1099  (∀a. (abs:'x -> 'y) (rep a) = a) ∧ (∀r. rep (abs r) = r) ⇒
1100  ∀s. s ≼ univ(:'x) ⇒ s ≼ univ(:'y)
1101Proof
1102  strip_tac >> rw[cardleq_def] >> qexists ‘abs o f’ >>
1103  gs[INJ_DEF] >> metis_tac[]
1104QED
1105
1106(* ----------------------------------------------------------------------
1107    Initiality: the homomorphism out of the initial algebra into any
1108    other algebra exists and, once pinned down off the carrier, is
1109    unique.
1110   ---------------------------------------------------------------------- *)
1111
1112(* the hypotheses are bnfMapCong followed by *exactly* IALG_HOM_ANY's, so
1113   the second conjunct of the bundle can be MATCH_MPed straight into
1114   that theorem with nothing left to guess *)
1115Theorem INITIALITY0:
1116  bnfMapCong mp_pc stp ∧
1117  (bnfNatural (mp_pa : ((('a set # ('f -> 'a)) -> 'a) -> 'a) -> 'fp -> 'f)
1118           stp sta ∧
1119   bnfNatural mp_pp stp stp ∧ bnfMapId mp_pp ∧ bnfMapComp mp_pp mp_pa mp_pa ∧
1120   bnfNatural mp_pc stp (stc : 'fc -> 'c set) ∧ bnfMapComp mp_pa mp_ac mp_pc ∧
1121   bnfMapComp mp_pc mp_cc mp_pc ∧
1122   bnfNatural mp_ac sta stc ∧ bnfNatural mp_ca stc sta ∧
1123   bnfMapComp mp_ca mp_ac mp_cc ∧ bnfMapId mp_cc ∧ bnfMapCong mp_cc stc ∧
1124   (∀t : 'fc -> 'c. bnfMINSET stc t ≼ 𝕌(:'a))) ⇒
1125  ∀t G.
1126    bnfALG stc (G,t) ⇒
1127    ∃!h. bnfHOM mp_pc stp stc h (bnfIALG stp mp_pa sta, bnfICONS mp_pa sta) (G,t) ∧
1128         ∀x. x ∉ bnfIALG stp mp_pa sta ⇒ h x = ARB
1129Proof
1130  (* the bundle is kept whole as well as split: the whole one is what
1131     applies forward to IALG_HOM_ANY *)
1132  disch_then (fn th => strip_assume_tac th >> assume_tac th) >>
1133  rpt strip_tac >> simp[EXISTS_UNIQUE_THM] >> conj_tac
1134  >- (irule HOM_arbification >> simp[] >>
1135      qpat_assum ‘bnfMapCong mp_pc stp ∧ _’
1136        (fn th => irule (MATCH_MP IALG_HOM_ANY (CONJUNCT2 th))) >>
1137      simp[]) >>
1138  rpt strip_tac >> simp[FUN_EQ_THM] >> qx_gen_tac ‘a’ >>
1139  Cases_on ‘a ∈ bnfIALG stp mp_pa sta’ >> simp[] >> gs[IALG_def] >>
1140  byrule MINSET_unique_homs
1141    [‘bnfMapCong mp_pc stp’,
1142     ‘bnfHOM mp_pc stp stc h _ _’, ‘bnfHOM mp_pc stp stc h' _ _’]
1143    (fn th => simp[th])
1144QED
1145
1146(* ----------------------------------------------------------------------
1147    Lambek: an algebra with the initiality property has a bijective
1148    structure map.
1149
1150    F's own carrier is a fourth instance: 'p is the algebra's carrier,
1151    'fp is F['p], and 'ffp is F['fp], the carrier of the algebra
1152    (bnfFIN stp A, mp_Fp s).
1153   ---------------------------------------------------------------------- *)
1154
1155Theorem ALG_FIN:
1156  bnfNatural mp_Fp stF stp ⇒ bnfALG stp (A,s) ⇒ bnfALG stF (bnfFIN stp A, mp_Fp s)
1157Proof
1158  simp[Natural_def] >> rpt strip_tac >>
1159  simp[ALG_def, SUBSET_DEF, PULL_EXISTS] >> rw[] >>
1160  gs[ALG_def, SUBSET_DEF, PULL_EXISTS] >> metis_tac[]
1161QED
1162
1163Theorem HOM_FIN:
1164  bnfNatural mp_Fp stF stp ⇒ bnfALG stp (A,s) ⇒
1165  bnfHOM mp_Fp stF stp s (bnfFIN stp A, mp_Fp s) (A,s)
1166Proof
1167  rpt strip_tac >> drule_all_then assume_tac ALG_FIN >>
1168  simp[HOM_def] >> gs[ALG_def]
1169QED
1170
1171Theorem LAMBEK:
1172  bnfMapCong (mp_pp : ('p -> 'p) -> 'fp -> 'fp) stp ∧ bnfMapId mp_pp ∧
1173  bnfNatural (mp_Fp : ('fp -> 'p) -> 'ffp -> 'fp) stF stp ∧
1174  bnfMapComp (mp_pF : ('p -> 'fp) -> 'fp -> 'ffp) mp_Fp mp_pp ∧
1175  bnfMapCong mp_pF stp ∧ bnfNatural mp_pF stp stF ∧
1176  bnfALG stp (A,s) ∧
1177  (∀t G. bnfALG stF (G,t) ⇒
1178         ∃!h. bnfHOM mp_pF stp stF h (A,s) (G,t) ∧ ∀x. x ∉ A ⇒ h x = ARB) ∧
1179  (∀t G. bnfALG stp (G,t) ⇒
1180         ∃!h. bnfHOM mp_pp stp stp h (A,s) (G,t) ∧ ∀x. x ∉ A ⇒ h x = ARB) ⇒
1181  BIJ s (bnfFIN stp A) A
1182Proof
1183  strip_tac >>
1184  drule_all_then assume_tac ALG_FIN >>
1185  ‘bnfHOM mp_Fp stF stp s (bnfFIN stp A, mp_Fp s) (A,s)’
1186    by (irule HOM_FIN >> simp[]) >>
1187  (* the unique homomorphism into the algebra (bnfFIN stp A, mp_Fp s) *)
1188  qpat_x_assum ‘∀t G. bnfALG stF (G,t) ⇒ _’
1189    (qspecl_then [‘mp_Fp s’, ‘bnfFIN stp A’] mp_tac) >>
1190  simp[EXISTS_UNIQUE_ALT] >> disch_then (qx_choose_then ‘H’ assume_tac) >>
1191  ‘bnfHOM mp_pF stp stF H (A,s) (bnfFIN stp A, mp_Fp s) ∧ ∀x. x ∉ A ⇒ H x = ARB’
1192    by (first_assum (irule o iffRL) >> simp[]) >>
1193  byrule HOMs_compose
1194    [‘bnfMapComp mp_pF mp_Fp mp_pp’, ‘bnfNatural mp_pF stp stF’,
1195     ‘bnfHOM mp_pF stp stF H (A,s) _’, ‘bnfHOM mp_Fp stF stp s _ (A,s)’]
1196    assume_tac >>
1197  (* s o H and I are both endomorphisms of (A,s), so they agree on A *)
1198  ‘bnfHOM mp_pp stp stp (bnfARBIFY A (s o H)) (A,s) (A,s)’
1199    by (byrule HOM_ARBIFY [‘bnfMapCong mp_pp stp’] (fn th => simp[th])) >>
1200  ‘bnfHOM mp_pp stp stp (bnfARBIFY A I) (A,s) (A,s)’
1201    by (byrule HOM_ARBIFY [‘bnfMapCong mp_pp stp’] (fn th => simp[th]) >>
1202        simp[HOM_def] >> gs[MapId_def]) >>
1203  qpat_x_assum ‘∀t G. bnfALG stp (G,t) ⇒ _’
1204    (qspecl_then [‘s’, ‘A’] mp_tac) >>
1205  simp[EXISTS_UNIQUE_ALT] >> disch_then (qx_choose_then ‘K0’ assume_tac) >>
1206  ‘K0 = bnfARBIFY A (s o H) ∧ K0 = bnfARBIFY A I’
1207    by (conj_tac >> first_assum (irule o iffLR) >> simp[ARBIFY_def]) >>
1208  ‘∀a. a ∈ A ⇒ s (H a) = a’
1209    by (rpt strip_tac >> ‘bnfARBIFY A (s o H) a = bnfARBIFY A I a’ by metis_tac[] >>
1210        gs[ARBIFY_def]) >>
1211  simp[BIJ_IFF_INV] >> conj_tac >- gs[ALG_def] >>
1212  qexists_tac ‘H’ >> rpt conj_tac
1213  >- gs[HOM_def]
1214  >- (* H (s af) = af: push s o H through the map and use bnfMapId *)
1215     (qx_gen_tac ‘af’ >> strip_tac >>
1216      ‘mp_Fp s (mp_pF H af) = H (s af)’ by gs[HOM_def] >>
1217      pop_assum (SUBST1_TAC o SYM) >>
1218      ‘mp_Fp s (mp_pF H af) = mp_pp (s o H) af’ by gs[MapComp_def] >>
1219      pop_assum SUBST1_TAC >>
1220      byrule Map_eq_id [‘bnfMapCong mp_pp stp’, ‘bnfMapId mp_pp’] irule >>
1221      gs[SUBSET_DEF]) >>
1222  simp[]
1223QED
1224
1225(* ----------------------------------------------------------------------
1226    What a type definition needs: the carrier is inhabited, and its
1227    elements are reachable, which is the induction principle.
1228   ---------------------------------------------------------------------- *)
1229
1230Theorem IALG_NONEMPTY:
1231  (∃w. stp w = ∅) ⇒ bnfIALG stp mp_pa sta ≠ ∅
1232Proof
1233  strip_tac >> simp[GSYM MEMBER_NOT_EMPTY] >>
1234  qexists_tac ‘bnfICONS mp_pa sta w’ >> irule ALG_closed >>
1235  qexists_tac ‘stp’ >> simp[]
1236QED
1237
1238(* the form new_type_definition wants: the carrier as a predicate *)
1239Theorem IALG_INHABITED:
1240  (∃w. stp w = ∅) ⇒ ∃x. bnfIALG stp mp_pa sta x
1241Proof
1242  strip_tac >>
1243  ‘bnfIALG stp mp_pa sta ≠ ∅’ by (irule IALG_NONEMPTY >> metis_tac[]) >>
1244  gs[GSYM MEMBER_NOT_EMPTY, IN_DEF] >> first_assum (irule_at Any)
1245QED
1246
1247Theorem IALG_ind:
1248  ∀P. (∀x. stp x ⊆ bnfIALG stp mp_pa sta ∧ (∀y. y ∈ stp x ⇒ P y) ⇒
1249           P (bnfICONS mp_pa sta x)) ⇒
1250      ∀x. x ∈ bnfIALG stp mp_pa sta ⇒ P x
1251Proof
1252  simp[IALG_def] >> MATCH_ACCEPT_TAC MINSET_ind
1253QED
1254
1255(* ----------------------------------------------------------------------
1256    Transporting the algebra to a type of its own.
1257
1258    A type definition supplies abs and rep with the three facts below;
1259    nothing here needs to know that they came from one.  'n is the new
1260    type, 'fn is F['n].
1261   ---------------------------------------------------------------------- *)
1262
1263Definition NCONS_def:
1264  bnfNCONS (mp_np : ('n -> 'p) -> 'fn -> 'fp) s rep abs af =
1265    abs (s (mp_np rep af))
1266End
1267
1268Theorem ALG_NCONS[simp]:
1269  bnfALG stn (𝕌(:'n), bnfNCONS mp_np s rep abs)
1270Proof
1271  simp[ALG_def]
1272QED
1273
1274Theorem HOM_ABS:
1275  bnfMapComp (mp_pn : ('p -> 'n) -> 'fp -> 'fn) mp_np mp_pp ∧
1276  bnfMapId mp_pp ∧ bnfMapCong mp_pp stp ∧
1277  (∀p. p ∈ A ⇒ rep (abs p) = p) ∧ bnfALG stp (A,s) ⇒
1278  bnfHOM mp_pn stp stn abs (A,s) (𝕌(:'n), bnfNCONS mp_np s rep abs)
1279Proof
1280  strip_tac >> drule_then (drule_then assume_tac) Map_eq_id >>
1281  simp[HOM_def, NCONS_def] >> rpt strip_tac >>
1282  gs[MapComp_def] >> AP_TERM_TAC >> AP_TERM_TAC >>
1283  first_x_assum irule >> gs[SUBSET_DEF]
1284QED
1285
1286Theorem HOM_REP:
1287  bnfNatural (mp_np : ('n -> 'p) -> 'fn -> 'fp) stn stp ∧
1288  (∀n. rep n ∈ A) ∧ (∀p. p ∈ A ⇒ rep (abs p) = p) ∧ bnfALG stp (A,s) ⇒
1289  bnfHOM mp_np stn stp rep (𝕌(:'n), bnfNCONS mp_np s rep abs) (A,s)
1290Proof
1291  strip_tac >> simp[HOM_def, NCONS_def] >> rpt strip_tac >>
1292  irule EQ_SYM >> first_x_assum irule >> irule ALG_closed >>
1293  qexists_tac ‘stp’ >> gs[Natural_def, SUBSET_DEF, PULL_EXISTS]
1294QED
1295
1296Theorem NEWTYPE_INITIALITY:
1297  bnfMapComp (mp_pn : ('p -> 'n) -> 'fp -> 'fn) mp_np mp_pp ∧
1298  bnfMapId mp_pp ∧ bnfMapCong mp_pp stp ∧
1299  bnfNatural mp_np stn stp ∧ bnfNatural mp_pn stp stn ∧
1300  bnfMapComp mp_np (mp_pc : ('p -> 'c) -> 'fp -> 'fc) mp_nc ∧
1301  bnfMapComp mp_pn mp_nc mp_pc ∧ bnfMapCong mp_pc stp ∧
1302  (∀n. abs (rep n) = n) ∧ (∀p. p ∈ A ⇒ rep (abs p) = p) ∧ (∀n. rep n ∈ A) ∧
1303  bnfALG stp (A,s) ∧
1304  (∀t G. bnfALG stc (G,t) ⇒
1305         ∃!h. bnfHOM mp_pc stp stc h (A,s) (G,t) ∧ ∀x. x ∉ A ⇒ h x = ARB) ⇒
1306  ∀t G. bnfALG stc (G,t) ⇒
1307        ∃!h. bnfHOM mp_nc stn stc h (𝕌(:'n), bnfNCONS mp_np s rep abs) (G,t)
1308Proof
1309  strip_tac >> rpt strip_tac >>
1310  ‘bnfHOM mp_np stn stp rep (𝕌(:'n), bnfNCONS mp_np s rep abs) (A,s)’
1311    by (irule HOM_REP >> simp[]) >>
1312  (* mp_pp appears only in HOM_ABS's hypotheses, so this one is forward *)
1313  byrule HOM_ABS
1314    [‘bnfMapComp mp_pn mp_np mp_pp’, ‘bnfMapId mp_pp’, ‘bnfMapCong mp_pp stp’,
1315     ‘∀p. p ∈ A ⇒ rep (abs p) = p’, ‘bnfALG stp (A,s)’]
1316    assume_tac >>
1317  (* the rewrite goes on the assumption: EXISTS_UNIQUE_ALT on the goal
1318     would put it in a shape the rest of the proof does not expect *)
1319  first_x_assum (qspecl_then [‘t’,‘G’] mp_tac) >> simp[] >>
1320  disch_then (qx_choose_then ‘H’ assume_tac o SRULE[EXISTS_UNIQUE_ALT]) >>
1321  simp[EXISTS_UNIQUE_THM] >> conj_tac
1322  >- (‘bnfHOM mp_pc stp stc H (A,s) (G,t) ∧ ∀x. x ∉ A ⇒ H x = ARB’
1323        by (first_assum (irule o iffRL) >> simp[]) >>
1324      byrule HOMs_compose
1325        [‘bnfMapComp mp_np mp_pc mp_nc’, ‘bnfNatural mp_np stn stp’,
1326         ‘bnfHOM mp_np stn stp rep _ (A,s)’, ‘bnfHOM mp_pc stp stc H (A,s) (G,t)’]
1327        (irule_at Any)) >>
1328  (* uniqueness: both give homomorphisms out of (A,s) once composed
1329     with abs, and those are unique *)
1330  qx_genl_tac [‘h1’, ‘h2’] >> strip_tac >>
1331  ‘∀h. bnfHOM mp_nc stn stc h (𝕌(:'n), bnfNCONS mp_np s rep abs) (G,t) ⇒
1332       H = bnfARBIFY A (h o abs)’
1333    by (rpt strip_tac >> first_assum (irule o iffLR) >>
1334        simp[ARBIFY_def] >>
1335        byrule HOM_ARBIFY [‘bnfMapCong mp_pc stp’] (fn th => simp[th]) >>
1336        byrule HOMs_compose
1337          [‘bnfMapComp mp_pn mp_nc mp_pc’, ‘bnfNatural mp_pn stp stn’,
1338           ‘bnfHOM mp_pn stp stn abs (A,s) _’,
1339           ‘bnfHOM mp_nc stn stc _ _ (G,t)’]
1340          (irule_at Any)) >>
1341  ‘bnfARBIFY A (h1 o abs) = bnfARBIFY A (h2 o abs)’ by metis_tac[] >>
1342  simp[FUN_EQ_THM] >> qx_gen_tac ‘n’ >>
1343  (* stating the instance rather than AP_TERMing a quotation: a rule's
1344     quotation is parsed with no goal context, so rep would come back at
1345     a fresh type *)
1346  ‘bnfARBIFY A (h1 o abs) (rep n) = bnfARBIFY A (h2 o abs) (rep n)’ by simp[] >>
1347  gs[ARBIFY_def]
1348QED
1349
1350(* over the whole type every function is a homomorphism, so initiality
1351   collapses to the recursion equation a datatype package wants *)
1352Theorem NEWTYPE_RECURSION =
1353        NEWTYPE_INITIALITY |> UNDISCH
1354                           |> Q.SPECL [‘t’, ‘UNIV’]
1355                           |> SRULE [HOM_def, ALG_def, SUBSET_UNIV]
1356                           |> GSYM
1357                           |> Q.GEN ‘t’
1358                           |> DISCH_ALL
1359
1360(* ----------------------------------------------------------------------
1361    Primitive recursion from iteration.
1362
1363    The recursion theorem above is an iterator: the function only ever
1364    sees the results of the recursive calls.  HOL's datatype axioms are
1365    primitive recursive — the function sees the constructor's arguments
1366    as well — so the two are bridged by the standard pairing trick, which
1367    needs the iterator at the product carrier 'n # 'c.
1368   ---------------------------------------------------------------------- *)
1369
1370Theorem PRIM_REC_OF_ITER:
1371  bnfMapComp (mp_nq : ('n -> 'n # 'c) -> 'fn -> 'fq) mp_qn mp_nn ∧
1372  bnfMapComp mp_nq (mp_qc : ('n # 'c -> 'c) -> 'fq -> 'fc) mp_nc ∧
1373  bnfMapId mp_nn ∧
1374  (∀t : 'fq -> 'n # 'c. ∃!h. ∀af. h (cons af) = t (mp_nq h af)) ∧
1375  (∀t : 'fn -> 'n. ∃!h. ∀af. h (cons af) = t (mp_nn h af)) ⇒
1376  ∀t : 'fn -> 'fc -> 'c. ∃!h. ∀af. h (cons af) = t af (mp_nc h af)
1377Proof
1378  strip_tac >> gen_tac >>
1379  (* the paired iterator: alongside the answer it rebuilds its own
1380     argument, and rebuilding is the identity *)
1381  qpat_assum ‘∀t. ∃!h. ∀af. h (cons af) = t (mp_nq h af)’
1382    (qspec_then ‘λv. (cons (mp_qn FST v), t (mp_qn FST v) (mp_qc SND v))’
1383       (strip_assume_tac o SRULE[EXISTS_UNIQUE_THM])) >>
1384  rename [‘k (cons _) = _’] >>
1385  ‘FST o k = I’
1386    by (qpat_assum ‘∀t. ∃!h. ∀af. h (cons af) = t (mp_nn h af)’
1387          (qspec_then ‘cons’ (strip_assume_tac o SRULE[EXISTS_UNIQUE_THM])) >>
1388        first_x_assum irule >> rpt conj_tac >~
1389        [‘I (cons _) = _’] >- gs[MapId_def] >>
1390        gen_tac >> simp[] >> gs[MapComp_def]) >>
1391  simp[EXISTS_UNIQUE_THM] >> conj_tac
1392  >- (qexists_tac ‘SND o k’ >> gen_tac >> simp[] >>
1393      gs[MapComp_def, MapId_def]) >>
1394  (* uniqueness: a solution paired with the identity solves the paired
1395     equation, and those solutions are unique *)
1396  qx_genl_tac [‘h1’, ‘h2’] >> strip_tac >>
1397  ‘∀h. (∀af. h (cons af) = t af (mp_nc h af)) ⇒ k = (λx. (x, h x))’
1398    by (rpt strip_tac >>
1399        qpat_assum ‘∀h h'. (∀af. h (cons af) = (cons _, _)) ∧ _ ⇒ _’ irule >>
1400        rpt conj_tac >~ [‘k (cons _) = _’] >- simp[] >>
1401        gen_tac >> simp[] >> gs[MapComp_def] >>
1402        simp[combinTheory.o_DEF, GSYM combinTheory.I_EQ_IDABS, ETA_AX] >>
1403        gs[MapId_def]) >>
1404  ‘(λx. (x, h1 x)) = (λx. (x, h2 x))’ by metis_tac[] >>
1405  gs[FUN_EQ_THM]
1406QED
1407
1408(* ----------------------------------------------------------------------
1409    Induction on the new type.
1410
1411    The hypothesis is "for every sub-term in the set", which is the form
1412    that survives a nested recursion: Prim_rec's derivation counts
1413    recursive arguments by their type, and under another type operator
1414    there are none to count.
1415   ---------------------------------------------------------------------- *)
1416
1417Theorem NEWTYPE_IND:
1418  bnfMapComp (mp_pn : ('p -> 'n) -> 'fp -> 'fn) mp_np mp_pp ∧
1419  bnfMapId mp_pp ∧ bnfMapCong mp_pp stp ∧ bnfNatural mp_pn stp stn ∧
1420  (∀n. abs (rep n) = n) ∧ (∀p. p ∈ bnfMINSET stp s ⇒ rep (abs p) = p) ∧
1421  (∀n. rep n ∈ bnfMINSET stp s) ⇒
1422  ∀P. (∀af. (∀y. y ∈ stn af ⇒ P y) ⇒ P (bnfNCONS mp_np s rep abs af)) ⇒
1423      ∀n. P n
1424Proof
1425  strip_tac >> gen_tac >> strip_tac >>
1426  drule_then (drule_then assume_tac) Map_eq_id >>
1427  ‘∀p. p ∈ bnfMINSET stp s ⇒ P (abs p)’
1428    by (ho_match_mp_tac MINSET_ind' >> qx_gen_tac ‘x’ >> strip_tac >>
1429        first_x_assum (qspec_then ‘mp_pn abs x’ mp_tac) >>
1430        simp[NCONS_def] >>
1431        ‘mp_np rep (mp_pn abs x) = x’
1432          by (gs[MapComp_def] >> first_x_assum irule >> simp[] >>
1433              metis_tac[]) >>
1434        simp[] >> disch_then irule >> gs[Natural_def, PULL_EXISTS]) >>
1435  gen_tac >> first_x_assum (qspec_then ‘rep n’ mp_tac) >> simp[]
1436QED
1437
1438(* ----------------------------------------------------------------------
1439    The degenerate fixed point.
1440
1441    A specification with no recursion — an enumeration, a record, any
1442    sum of products the type itself does not occur in — gives a functor
1443    that does not use the recursive argument at all, and μα. C is C.
1444
1445    The construction above cannot build it: the cardinality argument
1446    needs the recursive argument to be somewhere non-empty, which for a
1447    constant functor it never is.  It does not need to.  A type in
1448    bijection with C satisfies the same three principles, with the map
1449    an identity and the sub-term set empty, and that is all the rest of
1450    the package asks of a fixed point.
1451
1452    The map and the set function are parameters here, as they are
1453    everywhere else, so that a caller instantiates them with the terms
1454    its own functor gives and proves the two degeneracy facts about
1455    those terms.
1456   ---------------------------------------------------------------------- *)
1457
1458Theorem COPY_RECURSION:
1459  (∀n. abs (rep n) = n) ∧ (∀p. rep (abs p) = p) ∧
1460  (∀h:'n -> 'c. ∀af. mp h af = af) ⇒
1461  ∀t. ∃!h. ∀af. h (abs af) = t (mp h af)
1462Proof
1463  strip_tac >> gen_tac >> simp[EXISTS_UNIQUE_THM] >> conj_tac
1464  >- (qexists ‘t o rep’ >> simp[]) >>
1465  ‘∀k. (∀af. k (abs af) = t (mp k af)) ⇒ k = t o rep’
1466    suffices_by metis_tac[] >>
1467  rpt strip_tac >> simp[FUN_EQ_THM, FUN_EQ_THM] >> qx_gen_tac ‘n’ >>
1468  first_x_assum (qspec_then ‘rep n’ mp_tac) >> simp[]
1469QED
1470
1471Theorem COPY_PRIM_REC:
1472  (∀n. abs (rep n) = n) ∧ (∀p. rep (abs p) = p) ∧
1473  (∀h:'n -> 'c. ∀af. mp h af = af) ⇒
1474  ∀t. ∃!h. ∀af. h (abs af) = t af (mp h af)
1475Proof
1476  strip_tac >> gen_tac >> simp[EXISTS_UNIQUE_THM] >> conj_tac
1477  >- (qexists ‘λn. t (rep n) (rep n)’ >> simp[]) >>
1478  ‘∀k. (∀af. k (abs af) = t af (mp k af)) ⇒ k = λn. t (rep n) (rep n)’
1479    suffices_by metis_tac[] >>
1480  rpt strip_tac >> simp[FUN_EQ_THM] >> qx_gen_tac ‘n’ >>
1481  first_x_assum (qspec_then ‘rep n’ mp_tac) >> simp[]
1482QED
1483
1484Theorem COPY_IND:
1485  (∀n. abs (rep n) = n) ∧ (∀af. stn af = ∅) ⇒
1486  ∀P. (∀af. (∀y. y ∈ stn af ⇒ P y) ⇒ P (abs af)) ⇒ ∀n. P n
1487Proof
1488  rpt strip_tac >> first_x_assum (qspec_then ‘rep n’ mp_tac) >> simp[]
1489QED