1(*
2
3   fsubty ::= TyVar of string | Top | Fun of fsubty => fsubty
4          |   ForallTy of string => fsubty => fsubty
5
6   where the string in ForallTy binds in the second fsubty argument, but
7   not the first
8
9   Inductively characterise a subset of the lambda calculus terms that
10   can stand in for these types.  The encoding is
11
12     CON T                    -->  Top
13     CON F @@ t @@ LAM v t'   -->  ForallTy v t t'
14     VAR s                    -->  TyVar s
15     t @@ u                   -->  Fun t u
16
17   This theory establishes the type, along with swap functions for the type
18   and the type of "contexts", which are of type (string * type) list
19
20*)
21
22open HolKernel boolLib Parse
23
24open binderLib bossLib metisLib BasicProvers boolSimps
25
26val SUBSET_DEF = pred_setTheory.SUBSET_DEF
27
28val _ = new_theory "fsubtypes"
29
30(* establish the inductive characterisation of the encoding above *)
31val (fsubrep_rules, fsubrep_ind, fsubrep_cases) = Hol_reln`
32  fsubrep (CON T) /\
33  (!v t t'. fsubrep t /\ fsubrep t' ==> fsubrep (CON F @@ t @@ LAM v t')) /\
34  (!s. fsubrep (VAR s)) /\
35  (!t u. fsubrep t /\ fsubrep u ==> fsubrep (t @@ u))
36`;
37
38val strong_fsubrep_ind = save_thm(
39  "strong_fsubrep_ind",
40  IndDefLib.derive_strong_induction (fsubrep_rules, fsubrep_ind));
41
42(* because this is not obviously non-overlapping, we need to prove that
43   certain patterns aren't in fsubrep by induction *)
44
45val lam_not_fsubrep0 = prove(
46  ``!t0. fsubrep t0 ==> !v t. (t0 = LAM v t) ==> F``,
47  HO_MATCH_MP_TAC fsubrep_ind THEN SRW_TAC [][]);
48val lam_not_fsubrep = save_thm(
49  "lam_not_fsubrep",
50  SIMP_RULE (srw_ss() ++ DNF_ss) [] lam_not_fsubrep0)
51val _ = export_rewrites ["lam_not_fsubrep"]
52
53val CONF_not_fsubrep = store_thm(
54  "CONF_not_fsubrep",
55  ``~(fsubrep (CON F))``,
56  ONCE_REWRITE_TAC [fsubrep_cases] THEN SRW_TAC [][]);
57val _ = export_rewrites ["CONF_not_fsubrep"]
58
59(* type can be established by showing that fsubrep is non-empty; CON T is
60   the witness *)
61val fsubty_def = new_type_definition (
62  "fsubty",
63  prove(``?x. fsubrep x``, Q.EXISTS_TAC `CON T` THEN
64                           SRW_TAC [][fsubrep_rules])
65);
66
67val bijections_exist =
68    define_new_type_bijections {name = "bijections_exist",
69                                ABS = "term2fsubty",
70                                REP = "fsubty2term",
71                                tyax = fsubty_def};
72
73(* obvious facts about the bijections *)
74val fsubty2term_11 = store_thm(
75  "fsubty2term_11",
76  ``(fsubty2term ty1 = fsubty2term ty2) = (ty1 = ty2)``,
77  SRW_TAC [][EQ_IMP_THM] THEN
78  METIS_TAC [bijections_exist]);
79val _ = export_rewrites ["fsubty2term_11"]
80
81val term2fsubty_11 = store_thm(
82  "term2fsubty_11",
83  ``fsubrep t1 /\ fsubrep t2 ==>
84    ((term2fsubty t1 = term2fsubty t2) = (t1 = t2))``,
85  SRW_TAC [][EQ_IMP_THM] THEN METIS_TAC [bijections_exist]);
86
87val fsubrep_fsubty2term = store_thm(
88  "fsubrep_fsubty2term",
89  ``fsubrep (fsubty2term ty1)``,
90  METIS_TAC [bijections_exist]);
91val _ = export_rewrites ["fsubrep_fsubty2term"]
92
93
94(* define constructors *)
95val Top_def = Define`Top = term2fsubty (CON T)`;
96val TyVar_def = Define`TyVar s = term2fsubty (VAR s)`;
97val Fun_def = Define`
98  Fun ty1 ty2 = term2fsubty (fsubty2term ty1 @@ fsubty2term ty2)
99`;
100val ForallTy_def = Define`
101  ForallTy v boundty ty =
102    term2fsubty (CON F @@ fsubty2term boundty @@ LAM v (fsubty2term ty))
103`;
104
105(* prove injectivity for the non-binder constructors *)
106val Fun_11 = store_thm(
107  "Fun_11",
108  ``(Fun ty1 ty2 = Fun ty3 ty4) = (ty1 = ty3) /\ (ty2 = ty4)``,
109  SIMP_TAC (srw_ss()) [Fun_def, EQ_IMP_THM, fsubrep_rules, term2fsubty_11]);
110val _ = export_rewrites ["Fun_11"]
111
112val TyVar_11 = store_thm(
113  "TyVar_11",
114  ``(TyVar s1 = TyVar s2) = (s1 = s2)``,
115  SIMP_TAC (srw_ss()) [TyVar_def, fsubrep_rules, term2fsubty_11]);
116val _ = export_rewrites ["TyVar_11"]
117
118(* prove distinctness *)
119val fsubty_distinct = store_thm(
120  "fsubty_distinct",
121  ``~(Top = TyVar s) /\ ~(Top = Fun ty1 ty2) /\ ~(Top = ForallTy v bnd ty) /\
122    ~(TyVar s = Fun ty1 ty2) /\ ~(TyVar s = ForallTy v bnd ty) /\
123    ~(Fun ty1 ty2 = ForallTy v bnd ty)``,
124  SRW_TAC [][Top_def, TyVar_def, Fun_def, ForallTy_def,
125             fsubrep_rules, term2fsubty_11] THEN
126  DISJ2_TAC THEN STRIP_TAC THEN
127  POP_ASSUM (MP_TAC o Q.AP_TERM `fsubrep`) THEN
128  SRW_TAC [][]);
129val _ = export_rewrites ["fsubty_distinct"]
130
131val forall_fsubty = prove(
132  ``(!ty. P ty) = (!t. fsubrep t ==> P (term2fsubty t))``,
133  SRW_TAC [][EQ_IMP_THM] THEN
134  `?t. (ty = term2fsubty t) /\ fsubrep t`
135       by METIS_TAC [bijections_exist] THEN
136  METIS_TAC []);
137
138val rep_abs_lemma = prove(
139  ``fsubrep t ==> (fsubty2term (term2fsubty t) = t)``,
140  METIS_TAC [bijections_exist])
141
142(* induction principle *)
143val fsubty_ind = store_thm(
144  "fsubty_ind",
145  ``!P.
146        P Top /\
147        (!ty1 ty2. P ty1 /\ P ty2 ==> P (Fun ty1 ty2)) /\
148        (!s. P (TyVar s)) /\
149        (!v bnd ty. P bnd /\ P ty ==> P (ForallTy v bnd ty)) ==>
150        !ty. P ty``,
151  SIMP_TAC (srw_ss())
152           [forall_fsubty, Top_def, TyVar_def, Fun_def, ForallTy_def,
153            rep_abs_lemma] THEN
154  GEN_TAC THEN STRIP_TAC THEN
155  HO_MATCH_MP_TAC strong_fsubrep_ind THEN
156  METIS_TAC []);
157
158(* definition of swap *)
159val fswap_def = Define`
160  fswap x y ty = term2fsubty (swap x y (fsubty2term ty))
161`;
162
163val fsubrep_swap = store_thm(
164  "fsubrep_swap",
165  ``!t. fsubrep t ==> !x y. fsubrep (swap x y t)``,
166  HO_MATCH_MP_TAC fsubrep_ind THEN
167  SRW_TAC [][swapTheory.swap_thm, fsubrep_rules]);
168
169val fswap_thm = store_thm(
170  "fswap_thm",
171  ``(!s. fswap x y (TyVar s) = TyVar (swapstr x y s)) /\
172    (!ty1 ty2. fswap x y (Fun ty1 ty2) =
173                 Fun (fswap x y ty1) (fswap x y ty2)) /\
174    (fswap x y Top = Top) /\
175    (!v bnd ty. fswap x y (ForallTy v bnd ty) =
176       ForallTy (swapstr x y v) (fswap x y bnd) (fswap x y ty))``,
177  SRW_TAC [][fswap_def, Top_def, ForallTy_def, Fun_def, TyVar_def,
178             rep_abs_lemma, fsubrep_rules, swapTheory.swap_thm,
179             fsubrep_swap]);
180val _ = export_rewrites ["fswap_thm"]
181
182val fswap_inv = store_thm(
183  "fswap_inv",
184  ``!ty x y. fswap x y (fswap x y ty) = ty``,
185  HO_MATCH_MP_TAC fsubty_ind THEN SRW_TAC [][]);
186val _ = export_rewrites ["fswap_inv"]
187
188val fswap_id = store_thm(
189  "fswap_id",
190  ``fswap x x ty = ty``,
191  SRW_TAC [][fswap_def, bijections_exist]);
192val _ = export_rewrites ["fswap_id"]
193
194val fswap_comm = store_thm(
195  "fswap_comm",
196  ``fswap y x = fswap x y``,
197  SRW_TAC [][FUN_EQ_THM, fswap_def, swapTheory.swap_comm]);
198val _ = export_rewrites ["fswap_comm"]
199
200(* define swap over contexts *)
201val ctxtswap_def = Define`
202  (ctxtswap x y [] = []) /\
203  (ctxtswap x y (h::t) = (swapstr x y (FST h), fswap x y (SND h)) ::
204                         ctxtswap x y t)
205`;
206val _ = export_rewrites ["ctxtswap_def"]
207
208val ctxtswap_inv = store_thm(
209  "ctxtswap_inv",
210  ``!G x y. ctxtswap x y (ctxtswap x y G) = G``,
211  Induct THEN SRW_TAC [][]);
212val _ = export_rewrites ["ctxtswap_inv"]
213
214val ctxtswap_id = store_thm(
215  "ctxtswap_id",
216  ``!G x y. ctxtswap x x G = G``,
217  Induct THEN SRW_TAC [][ctxtswap_def]);
218val _ = export_rewrites ["ctxtswap_id"]
219
220val MEM_ctxtswap = store_thm(
221  "MEM_ctxtswap",
222  ``!G x y v ty. MEM (v,ty) (ctxtswap x y G) =
223                 MEM (swapstr x y v, fswap x y ty) G``,
224  Induct THEN ASM_SIMP_TAC (srw_ss()) [pairTheory.FORALL_PROD] THEN
225  METIS_TAC [fswap_inv]);
226val _ = export_rewrites ["MEM_ctxtswap"]
227
228val cdom_def = Define`
229  (cdom ([]: (string # fsubty) list)  = {}) /\
230  (cdom (h::t) = FST h INSERT cdom t)
231`;
232val _ = export_rewrites ["cdom_def"]
233
234val FINITE_cdom = store_thm(
235  "FINITE_cdom",
236  ``!G. FINITE (cdom G)``,
237  Induct THEN SRW_TAC [][]);
238val _ = export_rewrites ["FINITE_cdom"]
239
240val cdom_MEM = store_thm(
241  "cdom_MEM",
242  ``x IN cdom G = ?ty. MEM (x,ty) G``,
243  Induct_on `G` THEN ASM_SIMP_TAC (srw_ss()) [pairTheory.FORALL_PROD] THEN
244  METIS_TAC []);
245
246(* define fv for types *)
247val ftyFV_def = Define`
248  ftyFV ty = FV (fsubty2term ty)
249`;
250
251val ftyFV_thm = store_thm(
252  "ftyFV_thm",
253  ``(ftyFV Top = {}) /\
254    (ftyFV (Fun ty1 ty2) = ftyFV ty1 UNION ftyFV ty2) /\
255    (ftyFV (TyVar s) = {s}) /\
256    (ftyFV (ForallTy v bnd ty) = ftyFV bnd UNION (ftyFV ty DELETE v))``,
257  SRW_TAC [][ftyFV_def, Top_def, Fun_def, ForallTy_def, TyVar_def,
258             rep_abs_lemma, fsubrep_rules]);
259val _ = export_rewrites ["ftyFV_thm"]
260
261(* the following is not really an injectivity result, but it seems the best
262   possible for ForallTy *)
263val ForallTy_11 = store_thm(
264  "ForallTy_11",
265  ``(ForallTy v1 bnd1 bod1 = ForallTy v2 bnd2 bod2) =
266      (bnd1 = bnd2) /\ ((v1 = v2) \/ ~(v1 IN ftyFV bod2)) /\
267      (bod1 = fswap v1 v2 bod2)``,
268  SRW_TAC [][ftyFV_def, ftyFV_thm, fswap_def, ForallTy_def,
269             term2fsubty_11, fsubrep_rules, swapTheory.LAM_INJ_swap,
270             EQ_IMP_THM] THEN
271  ASM_SIMP_TAC (srw_ss()) [] THENL [
272    FIRST_X_ASSUM (MP_TAC o Q.AP_TERM `term2fsubty`) THEN
273    SRW_TAC [][bijections_exist],
274    FIRST_X_ASSUM (MP_TAC o Q.AP_TERM `term2fsubty`) THEN
275    SRW_TAC [][bijections_exist],
276    SRW_TAC [][bijections_exist],
277    SRW_TAC [][rep_abs_lemma, fsubrep_fsubty2term, fsubrep_swap]
278  ]);
279
280val ForallTy_injectivity_lemma1 = store_thm(
281  "ForallTy_injectivity_lemma1",
282  ``(ForallTy x bnd1 ty1 = ForallTy y bnd2 ty2) ==>
283    (bnd1 = bnd2) /\ (ty2 = fswap x y ty1)``,
284  METIS_TAC [ForallTy_11, fswap_inv]);
285
286val ForallTy_INJ_ALPHA_FV = store_thm(
287  "ForallTy_INJ_ALPHA_FV",
288  ``(ForallTy x bnd ty1 = ForallTy y bnd ty2) /\ ~(x = y) ==>
289    ~(x IN ftyFV ty2) /\ ~(y IN ftyFV ty1)``,
290  METIS_TAC [ForallTy_11]);
291
292val ForallTy_ALPHA = store_thm(
293  "ForallTy_ALPHA",
294  ``~(u IN ftyFV ty) ==>
295    (ForallTy u bnd (fswap u v ty) = ForallTy v bnd ty)``,
296  METIS_TAC [ForallTy_11]);
297
298val fswap_fresh = store_thm(
299  "fswap_fresh",
300  ``!ty x y. ~(x IN ftyFV ty) /\ ~(y IN ftyFV ty) ==>
301             (fswap x y ty = ty)``,
302  SRW_TAC [][fswap_def, ftyFV_def, swapTheory.swap_identity,
303             bijections_exist]);
304
305val swapset_DELETE = store_thm(
306  "swapset_DELETE",
307  ``swapset x y (s1 DELETE s) = swapset x y s1 DELETE swapstr x y s``,
308  SRW_TAC [][swapTheory.swapset_def, pred_setTheory.EXTENSION]);
309
310val swapset_SUBSET = store_thm(
311  "swapset_SUBSET",
312  ``s1 SUBSET swapset x y s2 = swapset x y s1 SUBSET s2``,
313  SRW_TAC [][swapTheory.swapset_def, SUBSET_DEF] THEN
314  METIS_TAC [swapTheory.swapstr_inverse]);
315val _ = export_rewrites ["swapset_SUBSET"]
316
317val ftyFV_fswap = store_thm(
318  "ftyFV_fswap",
319  ``!ty x y. ftyFV (fswap x y ty) = swapset x y (ftyFV ty)``,
320  HO_MATCH_MP_TAC fsubty_ind THEN
321  SRW_TAC [][swapTheory.swapset_UNION, swapset_DELETE]);
322val _ = export_rewrites ["ftyFV_fswap"]
323
324val ftyFV_FINITE = store_thm(
325  "ftyFV_FINITE",
326  ``!ty. FINITE (ftyFV ty)``,
327  HO_MATCH_MP_TAC fsubty_ind THEN
328  SRW_TAC [][]);
329val _ = export_rewrites ["ftyFV_FINITE"]
330
331(* define FV for ctxts *)
332val ctxtFV_def = Define`
333  (ctxtFV [] = {}) /\
334  (ctxtFV (h::t) = {FST h} UNION ftyFV (SND h) UNION ctxtFV t)
335`;
336val _ = export_rewrites ["ctxtFV_def"]
337
338val ctxtFV_ctxtswap = store_thm(
339  "ctxtFV_ctxtswap",
340  ``!G x y. ctxtFV (ctxtswap x y G) = swapset x y (ctxtFV G)``,
341  Induct THEN SRW_TAC [][swapTheory.swapset_UNION]);
342val _ = export_rewrites ["ctxtFV_ctxtswap"]
343
344val ctxtFV_FINITE = store_thm(
345  "ctxtFV_FINITE",
346  ``!G. FINITE (ctxtFV G)``,
347  Induct THEN SRW_TAC [][]);
348val _ = export_rewrites ["ctxtFV_FINITE"]
349
350val cdom_SUBSET_ctxtFV = store_thm(
351  "cdom_SUBSET_ctxtFV",
352  ``!G. cdom G SUBSET ctxtFV G``,
353  Induct THEN
354  FULL_SIMP_TAC (srw_ss()) [cdom_def, SUBSET_DEF] THEN
355  METIS_TAC []);
356
357val cdom_ctxtswap = store_thm(
358  "cdom_ctxtswap",
359  ``!G x y. cdom (ctxtswap x y G) = swapset x y (cdom G)``,
360  Induct THEN SRW_TAC[][]);
361val _ = export_rewrites ["cdom_ctxtswap"]
362
363val ctxtswap_fresh = store_thm(
364  "ctxtswap_fresh",
365  ``!G x y.
366       ~(x IN ctxtFV G) /\ ~(y IN ctxtFV G) ==>
367       (ctxtswap x y G = G)``,
368  Induct THEN SRW_TAC [][fswap_fresh]);
369
370(* wfctxt implements the restrictions defined on pp393-4 *)
371val wfctxt_def = Define`
372  (wfctxt [] = T) /\
373  (wfctxt ((x,ty) :: t) = ~(x IN cdom t) /\
374                          ftyFV ty SUBSET cdom t /\
375                          wfctxt t)
376`;
377val _ = export_rewrites ["wfctxt_def"]
378
379val wfctxt_swap = store_thm(
380  "wfctxt_swap",
381  ``!G x y. wfctxt (ctxtswap x y G) = wfctxt G``,
382  Induct THEN ASM_SIMP_TAC (srw_ss()) [pairTheory.FORALL_PROD]);
383val _ = export_rewrites ["wfctxt_swap"]
384
385val wfctxt_ctxtFV_cdom = store_thm(
386  "wfctxt_ctxtFV_cdom",
387  ``!G. wfctxt G ==> (ctxtFV G = cdom G)``,
388  SIMP_TAC (srw_ss()) [pred_setTheory.EXTENSION] THEN
389  Induct THEN ASM_SIMP_TAC (srw_ss()) [pairTheory.FORALL_PROD, SUBSET_DEF] THEN
390  METIS_TAC []);
391
392val wfctxt_MEM = store_thm(
393  "wfctxt_MEM",
394  ``!G. wfctxt G /\ MEM (x,ty) G ==>
395        x IN cdom G /\ !y. y IN ftyFV ty ==> y IN cdom G``,
396  Induct THEN ASM_SIMP_TAC (srw_ss()) [pairTheory.FORALL_PROD,
397                                       SUBSET_DEF] THEN
398  METIS_TAC []);
399
400val fsize_def = Define`
401  fsize (t:fsubty) = size (fsubty2term t)
402`;
403
404val fsize_thm = store_thm(
405  "fsize_thm",
406  ``(fsize Top = 1) /\
407    (fsize (TyVar s) = 1) /\
408    (fsize (ForallTy x ty1 ty2) = fsize ty1 + fsize ty2 + 4) /\
409    (fsize (Fun ty1 ty2) = fsize ty1 + fsize ty2 + 1)``,
410  SRW_TAC [numSimps.ARITH_ss]
411          [fsize_def,Fun_def,Top_def,ForallTy_def,TyVar_def,
412           rep_abs_lemma, fsubrep_rules, ncTheory.size_thm]);
413
414
415val _ = export_theory();
416
417