bnfFixBNFScript.sml

1Theory bnfFixBNF[bare]
2Ancestors
3  bnfInitial bnfPrelims pred_set cardinalityCore
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”
20
21
22(* ----------------------------------------------------------------------
23    bossLib is not built yet — the package has to be, so that Datatype
24    can use it, and so this is the part of bossLib's environment these
25    proofs need.  The same emulation cardinalScript uses.
26   ---------------------------------------------------------------------- *)
27
28fun simp ths = simpLib.ASM_SIMP_TAC (srw_ss()) ths
29fun csimp ths = simp (SF CONJ_ss :: ths)
30fun dsimp ths = simp (SF DNF_ss :: ths)
31fun gs ths = simpLib.global_simp_tac
32               {elimvars = false, strip = true, droptrues = true,
33                oldestfirst = true} (srw_ss()) ths
34fun gvs ths = simpLib.global_simp_tac
35                {elimvars = true, strip = true, droptrues = true,
36                 oldestfirst = true} (srw_ss()) ths
37fun rw ths = BasicProvers.SRW_TAC [] ths
38val metis_tac = metisLib.METIS_TAC
39fun SRULE ths th = SIMP_RULE (srw_ss()) ths th
40val qexists = Q.EXISTS_TAC
41val op >~ = Q.>~
42val op >>~ = Q.>>~
43
44
45(* ----------------------------------------------------------------------
46    The fixed point is itself a functor, proved once.
47
48    A datatype the package builds is μα. F(α, β⃗), and for a later
49    datatype to recurse through it, it has to go into the BNF database
50    with a map, a set function per parameter, the four laws, a bound and
51    witnesses.  All of that is proved here, over parameters, in the way
52    bnfInitialScript proves the construction itself: F's instances become
53    ordinary type variables and its map and set functions ordinary term
54    variables.
55
56    Two things make the statements below shorter than they look.  First,
57    the map and set functions of the new type are not defined here — the
58    recursion principle defines them per datatype — so they arrive as
59    parameters constrained by the equations they satisfy: bnfFIXMAP for the
60    map, bnfFIXSET for a set function.  Second, F's map is *bundled*: a
61    parameter map term stands for F's n-ary map with a particular tuple
62    of functions already applied to the parameters, so that one binary
63    statement covers a functor with any number of them.  Two bundles at
64    different tuples are two parameters, related by whichever of the laws
65    below needs them related — which is exactly how bnfMapComp already
66    relates three instances of a map.
67
68    Throughout, 'n is the new type and 'fn is F['n]; 'm and 'fm are the
69    same after a map, cn and cm the constructors, stn F's set function
70    for the recursive argument, and sbn one of its parameters'.
71   ---------------------------------------------------------------------- *)
72
73(* ----------------------------------------------------------------------
74    the parameters that are not already in bnfInitialTheory
75   ---------------------------------------------------------------------- *)
76
77(* the new type's induction principle: every element is a cn of one whose
78   sub-terms are covered.  This is what defineFixpoint's set_induction
79   supplies. *)
80Definition FIXIND_def:
81  bnfFIXIND (cn : 'fn -> 'n) stn ⇔
82    ∀P. (∀af. (∀y. y ∈ stn af ⇒ P y) ⇒ P (cn af)) ⇒ ∀n. P n
83End
84
85Theorem FIXIND_thm:
86  bnfFIXIND (cn : 'fn -> 'n) stn ⇒
87  ∀P. (∀af. (∀y. y ∈ stn af ⇒ P y) ⇒ P (cn af)) ⇒ ∀n. P n
88Proof
89  simp[FIXIND_def]
90QED
91
92(* M is the new type's map for one tuple of functions on the parameters:
93   it takes a constructor apart, maps F, and puts it back together *)
94Definition FIXMAP_def:
95  bnfFIXMAP (cn : 'fn -> 'n) (cm : 'fm -> 'm) mp M ⇔
96    ∀af. M (cn af) = cm (mp M af)
97End
98
99(* and S is the set function for one parameter: the atoms F holds at this
100   node, together with those of every sub-term *)
101Definition FIXSET_def:
102  bnfFIXSET (cn : 'fn -> 'n) stn sbn S ⇔
103    ∀af. S (cn af) = sbn af ∪ BIGUNION (IMAGE S (stn af))
104End
105
106(* naturality in a parameter rather than in the recursive argument: what
107   the bundled map does to the parameter's atoms doesn't depend on the
108   function it is given for the recursive argument *)
109Definition NaturalP_def:
110  bnfNaturalP (mp : ('n -> 'm) -> 'fn -> 'fm) sbn sbm p ⇔
111    ∀h af. sbm (mp h af) = IMAGE p (sbn af)
112End
113
114(* and congruence between two bundles that differ in one parameter *)
115Definition MapCongP_def:
116  bnfMapCongP (mp1 : ('n -> 'm) -> 'fn -> 'fm) mp2 stn sbn p q ⇔
117    ∀h1 h2 af.
118      (∀y. y ∈ stn af ⇒ h1 y = h2 y) ∧ (∀b. b ∈ sbn af ⇒ p b = q b) ⇒
119      mp1 h1 af = mp2 h2 af
120End
121
122(* ----------------------------------------------------------------------
123    the map laws
124   ---------------------------------------------------------------------- *)
125
126(* induction on the new type, from the principle the parameters carry.
127   drule would pull the induction variable out in front of P, leaving the
128   conclusion in a shape ho_match_mp_tac cannot use. *)
129val fix_induct =
130    qpat_assum ‘bnfFIXIND _ _’ (ho_match_mp_tac o MATCH_MP FIXIND_thm)
131
132(* bnfMapCong comes first in every hypothesis list below because it fixes
133   both the map and the set function, so drule can resolve it and know
134   what the rest means *)
135Theorem FIXMAP_ID:
136  bnfMapCong mp stn ∧ bnfMapId mp ∧ bnfFIXIND cn stn ∧ bnfFIXMAP cn cn mp M ⇒
137  ∀n. M n = n
138Proof
139  strip_tac >> drule_then (drule_then assume_tac) Map_eq_id >>
140  fix_induct >> rpt strip_tac >> gs[FIXMAP_def]
141QED
142
143Theorem FIXMAP_O:
144  bnfMapCong mp_np stn ∧ bnfMapComp mp_nm mp_mp mp_np ∧ bnfFIXIND cn stn ∧
145  bnfFIXMAP cn cm mp_nm M1 ∧ bnfFIXMAP cm cp mp_mp M2 ∧ bnfFIXMAP cn cp mp_np M12 ⇒
146  ∀n. M2 (M1 n) = M12 n
147Proof
148  strip_tac >> fix_induct >> rpt strip_tac >>
149  gs[FIXMAP_def, MapComp_def] >>
150  (* both sides are cp of a map of af; the maps agree by congruence,
151     since the induction hypothesis covers every sub-term *)
152  AP_TERM_TAC >> gs[MapCong_def] >> first_x_assum irule >> simp[]
153QED
154
155(* ----------------------------------------------------------------------
156    the set function
157   ---------------------------------------------------------------------- *)
158
159Theorem FIXSET_NATURAL:
160  bnfNatural mp stn stm ∧ bnfNaturalP mp sbn sbm p ∧ bnfFIXIND cn stn ∧
161  bnfFIXMAP cn cm mp M ∧ bnfFIXSET cn stn sbn Sn ∧ bnfFIXSET cm stm sbm Sm ⇒
162  ∀n. Sm (M n) = IMAGE p (Sn n)
163Proof
164  strip_tac >> fix_induct >> rpt strip_tac >>
165  gs[FIXMAP_def, FIXSET_def, Natural_def, NaturalP_def] >>
166  (* the atoms of the mapped sub-terms are the images of the sub-terms'
167     atoms, which is the induction hypothesis under an IMAGE *)
168  ‘IMAGE Sm (IMAGE M (stn af)) = IMAGE (IMAGE p o Sn) (stn af)’
169    by (simp[IMAGE_IMAGE] >> irule IMAGE_CONG >> simp[]) >>
170  simp[IMAGE_BIGUNIONo]
171QED
172
173Theorem FIXMAP_CONG:
174  bnfMapCongP mp1 mp2 stn sbn p q ∧ bnfFIXIND cn stn ∧ bnfFIXSET cn stn sbn Sn ∧
175  bnfFIXMAP cn cm mp1 M1 ∧ bnfFIXMAP cn cm mp2 M2 ⇒
176  ∀n. (∀b. b ∈ Sn n ⇒ p b = q b) ⇒ M1 n = M2 n
177Proof
178  strip_tac >> fix_induct >> rpt strip_tac >>
179  gs[FIXMAP_def] >> AP_TERM_TAC >>
180  (* the atoms of cn af are those F holds here and those of the
181     sub-terms, so agreeing on all of them is agreeing on each part *)
182  qpat_x_assum ‘∀b. b ∈ Sn (cn af) ⇒ _’ mp_tac >>
183  gs[FIXSET_def, MapCongP_def, PULL_EXISTS] >> strip_tac >>
184  first_x_assum irule >> rpt strip_tac >>
185  first_x_assum irule >> metis_tac[]
186QED
187
188(* ----------------------------------------------------------------------
189    the bound.
190
191    An atom of a term sits in one of its sub-terms, of which there are no
192    more than F's own bound, and each holds no more than that many atoms;
193    an infinite cardinal absorbs both, so F's bound bounds the new type
194    as well.
195   ---------------------------------------------------------------------- *)
196
197Theorem FIXSET_CARDLEQ:
198  bnfFIXSET cn stn sbn Sn ∧ INFINITE B ∧ (∀af. sbn af ≼ B) ∧
199  (∀af. stn af ≼ B) ∧ bnfFIXIND cn stn ⇒
200  ∀n. Sn n ≼ B
201Proof
202  strip_tac >> fix_induct >> rpt strip_tac >>
203  gs[FIXSET_def] >> irule UNION_CARDLE >> simp[] >>
204  irule CARD_BIGUNION >> simp[PULL_EXISTS] >>
205  irule IMAGE_cardleq_rwt >> simp[]
206QED
207
208(* ----------------------------------------------------------------------
209    Set notation.
210
211    The set functions the component functors are registered with are
212    stated as predicates — sumTheory's setL gives ‘λx. x = a’ — so
213    unfolding a composite's set function at a constructor leaves those
214    where set notation is wanted.
215   ---------------------------------------------------------------------- *)
216
217(* the argument's own set function, as a set: a composite over a bare
218   parameter is the equality predicate at it *)
219Theorem EQUAL_SING:
220  (=) a = {a}
221Proof
222  simp[EXTENSION, bnfPrelimsTheory.IN_equal, EQ_SYM_EQ]
223QED
224
225Theorem LAM_EQ_SING:
226  (λx. x = a) = {a}
227Proof
228  simp[EXTENSION]
229QED
230
231Theorem LAM_F_EMPTY:
232  (λx. F) = ∅
233Proof
234  simp[EXTENSION]
235QED
236
237(* and two laws that put a set term built by nesting one functor inside
238   another into a normal form: the atoms of a union are collected
239   separately, and a set function applied through a collection of
240   sub-terms is applied at each of them *)
241Theorem BIGUNION_IMAGE_UNION:
242  BIGUNION (IMAGE (λx. A x ∪ B x) X) =
243  BIGUNION (IMAGE A X) ∪ BIGUNION (IMAGE B X)
244Proof
245  simp[Once EXTENSION, PULL_EXISTS] >> metis_tac[]
246QED
247
248Theorem BIGUNION_IMAGE_EMPTY:
249  BIGUNION (IMAGE (λx. ∅) X) = ∅
250Proof
251  once_rewrite_tac[EXTENSION] >> simp[PULL_EXISTS]
252QED
253
254Theorem BIGUNION_IMAGE_BIGUNION:
255  BIGUNION (IMAGE h (BIGUNION (IMAGE g X))) =
256  BIGUNION (IMAGE (λx. BIGUNION (IMAGE h (g x))) X)
257Proof
258  simp[Once EXTENSION, PULL_EXISTS] >> metis_tac[]
259QED
260
261(* what a value's sets say after a map: the induction hypothesis for
262   that member, without taking the set function apart *)
263Theorem IMAGE_ALL:
264  (∀b. b ∈ IMAGE f s ⇒ b) ⇔ ∀y. y ∈ s ⇒ f y
265Proof
266  simp[PULL_EXISTS]
267QED
268
269(* and the same when the value is the argument itself: its set function
270   is equality, with no image over it to take apart *)
271Theorem EQ_ALL:
272  (∀b. b ∈ $= a ⇒ b) ⇔ a
273Proof
274  simp[IN_DEF]
275QED
276
277(* an equation the induction principle is read off: a clause of it says
278   the hypothesis implies the conclusion, and what the recursion at the
279   booleans says is that the two are the same disjunction *)
280Theorem IMP_DISJ_EQ:
281  (q ⇒ p) ⇒ (p ⇔ q ∨ p)
282Proof
283  DECIDE_TAC
284QED
285
286(* ----------------------------------------------------------------------
287    witnesses and inhabitation.
288
289    A witness for the new type is a constructor applied to a witness for
290    F that doesn't need the recursive argument — a base case — and its
291    atoms are then exactly the ones F holds there.  Inhabitation is the
292    other half: an atom F holds at a node is an atom of the term.
293   ---------------------------------------------------------------------- *)
294
295Theorem FIXSET_EMPTY:
296  bnfFIXSET cn stn sbn Sn ∧ stn w = ∅ ⇒ Sn (cn w) = sbn w
297Proof
298  simp[FIXSET_def]
299QED
300
301Theorem FIXSET_IN:
302  bnfFIXSET cn stn sbn Sn ⇒ ∀af b. b ∈ sbn af ⇒ b ∈ Sn (cn af)
303Proof
304  simp[FIXSET_def]
305QED