1(* Fun and games with the "locally nameless" approach to language meta-theory
2   as done in the POPL paper "Engineering Formal Metatheory" by Brian
3   Aydemir, Arthur Chargu��raud, Benjamin Pierce, Randy Pollack and Stephanie
4   Weirich.
5
6   Contribution below is to show that it's as easy to prove the
7   cofinite introduction rule and the cofinite induction principle of
8   the original relations directly, rather than bothering to define a
9   whole new cofinite relation and to then show that this is
10   equivalent to the original.
11*)
12
13open HolKernel boolLib bossLib Parse
14
15open binderLib
16
17open nomsetTheory pred_setTheory
18
19fun Store_thm (p as (n,t,tac)) = store_thm p before export_rewrites [n]
20
21val _ = new_theory "lnameless"
22
23val _ = Datatype`lnt = var string | bnd num | app lnt lnt | abs lnt`;
24
25val open_def = Define`
26  (open k u (bnd i) = if i = k then u else bnd i) /\
27  (open k u (var s) = var s) /\
28  (open k u (app t1 t2) = app (open k u t1) (open k u t2)) /\
29  (open k u (abs t) = abs (open (k + 1) u t))
30`;
31val _ = export_rewrites ["open_def"]
32
33val raw_lnpm_def = Define`
34  (raw_lnpm pi (var s) = var (lswapstr pi s)) /\
35  (raw_lnpm pi (bnd i) = bnd i) /\
36  (raw_lnpm pi (app t1 t2) = app (raw_lnpm pi t1) (raw_lnpm pi t2)) /\
37  (raw_lnpm pi (abs t) = abs (raw_lnpm pi t))
38`;
39val _ = export_rewrites ["raw_lnpm_def"]
40
41val _ = overload_on("ln_pmact",``mk_pmact raw_lnpm``);
42val _ = overload_on("lnpm",``pmact ln_pmact``);
43
44val lnpm_raw = store_thm(
45  "lnpm_raw",
46  ``lnpm = raw_lnpm``,
47  SRW_TAC [][GSYM pmact_bijections] THEN
48  SRW_TAC [][is_pmact_def, permeq_thm, FUN_EQ_THM] THENL [
49    Induct_on `x` THEN SRW_TAC [][],
50    Induct_on `x` THEN SRW_TAC [][pmact_decompose],
51    Induct_on `x` THEN SRW_TAC [][]
52  ]);
53
54val lnpm_thm = save_thm(
55"lnpm_thm",
56raw_lnpm_def |> SUBS [GSYM lnpm_raw]);
57val _ = export_rewrites["lnpm_thm"];
58
59val lnpm_open = prove(
60  ``!i. lnpm pi (open i t1 t2) = open i (lnpm pi t1) (lnpm pi t2)``,
61  Induct_on `t2` THEN SRW_TAC [][]);
62
63val fv_def = Define`
64  (fv (var s) = {s}) /\
65  (fv (bnd i) = {}) /\
66  (fv (app t u) = fv t UNION fv u) /\
67  (fv (abs t) = fv t)
68`;
69val _ = export_rewrites ["fv_def"]
70
71val fv_lnpm = prove(
72  ``!t. fv (lnpm pi t) = ssetpm pi (fv t)``,
73  Induct THEN SRW_TAC [][pmact_INSERT, pmact_UNION]);
74
75val FINITE_fv = Store_thm(
76  "FINITE_fv",
77  ``!t. FINITE (fv t)``,
78  Induct THEN SRW_TAC [][]);
79
80val lnpm_fresh = store_thm(
81  "lnpm_fresh",
82  ``~(a IN fv t) /\ ~(b IN fv t) ==> (lnpm [(a,b)] t = t)``,
83  Induct_on `t` THEN SRW_TAC [][]);
84
85val (lclosed_rules, lclosed_ind, lclosed_cases) = Hol_reln`
86  (!s. lclosed (var s)) /\
87  (!t1 t2. lclosed t1 /\ lclosed t2 ==> lclosed (app t1 t2)) /\
88  (!s t. ~(s IN fv t) /\ lclosed (open 0 (var s) t) ==>
89         lclosed (abs t))
90`;
91
92val lclosed_eqvt = prove(
93  ``!t. lclosed t ==> !pi. lclosed (lnpm pi t)``,
94  HO_MATCH_MP_TAC lclosed_ind THEN SRW_TAC [][lclosed_rules, lnpm_open] THEN
95  MATCH_MP_TAC (last (CONJUNCTS lclosed_rules)) THEN
96  Q.EXISTS_TAC `lswapstr pi s` THEN
97  SRW_TAC [][fv_lnpm]);
98
99val lclosed_gen_bvc_ind = store_thm(
100  "lclosed_gen_bvc_ind",
101  ``!P f. (!c. FINITE (f c)) /\
102           (!s c. P (var s) c) /\
103           (!t1 t2 c. (!d. P t1 d) /\ (!d. P t2 d) ==> P (app t1 t2) c) /\
104           (!s t c. ~(s IN f c) /\ ~(s IN fv t) /\
105                    (!d. P (open 0 (var s) t) d) ==>
106                    P (abs t) c) ==>
107           !t. lclosed t ==> !c. P t c``,
108  REPEAT GEN_TAC THEN STRIP_TAC THEN
109  Q_TAC SUFF_TAC `!t. lclosed t ==> !pi c. P (lnpm pi t) c`
110        THEN1 METIS_TAC [pmact_nil] THEN
111  HO_MATCH_MP_TAC lclosed_ind THEN SRW_TAC [][lnpm_open] THEN
112  FIRST_X_ASSUM MATCH_MP_TAC THEN
113  Q_TAC (NEW_TAC "z") `fv (lnpm pi t) UNION f c` THEN
114  FIRST_X_ASSUM (Q.SPEC_THEN `(stringpm pi s, z) :: pi` MP_TAC) THEN
115  ASM_SIMP_TAC (srw_ss()) [] THEN
116  `lnpm [(stringpm pi s, z)] (lnpm pi t) = lnpm pi t`
117     by SRW_TAC [][lnpm_fresh, fv_lnpm] THEN
118  FULL_SIMP_TAC (srw_ss()) [GSYM pmact_decompose] THEN
119  STRIP_TAC THEN Q.EXISTS_TAC `z` THEN SRW_TAC [][]);
120
121val all_fnone = prove(
122  ``(!(f:one -> 'a). P f) = !x:'a. P (K x)``,
123  SRW_TAC [][EQ_IMP_THM] THEN
124  Q_TAC SUFF_TAC `f = K (f())`
125        THEN1 (DISCH_THEN SUBST1_TAC THEN SRW_TAC [][]) THEN
126  SRW_TAC [][FUN_EQ_THM, oneTheory.one]);
127
128val lclosed_bvc_ind = save_thm(
129  "lclosed_bvc_ind",
130  (Q.GEN `P` o Q.GEN `X` o
131   SIMP_RULE bool_ss [] o
132   SPECL [``(\M:lnt x:one. P M:bool)``,
133          ``X:string -> bool``] o
134   SIMP_RULE (srw_ss()) [all_fnone, oneTheory.one] o
135   INST_TYPE [alpha |-> ``:one``] o
136   GEN_ALL) lclosed_gen_bvc_ind);
137
138val lclosed_cofin_ind = store_thm(
139  "lclosed_cofin_ind",
140  ``!P. (!s. P (var s)) /\
141        (!t1 t2. P t1 /\ P t2 ==> P (app t1 t2)) /\
142        (!t X. FINITE X /\
143               (!s. ~(s IN X) ==> P (open 0 (var s) t)) ==>
144               P (abs t)) ==>
145        !t. lclosed t ==> P t``,
146  GEN_TAC THEN STRIP_TAC THEN
147  Q_TAC SUFF_TAC `!t. lclosed t ==> !pi. P (lnpm pi t)`
148        THEN1 METIS_TAC [pmact_nil] THEN
149  HO_MATCH_MP_TAC lclosed_bvc_ind THEN SRW_TAC [][lnpm_open] THEN
150  Q.EXISTS_TAC `{}` THEN SRW_TAC [][] THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
151  Q.EXISTS_TAC `fv (lnpm pi t)` THEN SRW_TAC [][] THEN
152  `lnpm [(s',stringpm pi s)] (lnpm pi t) = lnpm pi t`
153      by SRW_TAC [][lnpm_fresh, fv_lnpm] THEN
154  FIRST_X_ASSUM (Q.SPEC_THEN `[(s',stringpm pi s)] ++ pi` MP_TAC) THEN
155  SRW_TAC [][pmact_decompose]);
156
157val abs_lclosed_I = store_thm(
158  "abs_lclosed_I",
159  ``FINITE X /\ (!s. ~(s IN X) ==> lclosed (open 0 (var s) t)) ==>
160    lclosed (abs t)``,
161  STRIP_TAC THEN MATCH_MP_TAC (last (CONJUNCTS lclosed_rules)) THEN
162  Q_TAC (NEW_TAC "z") `fv t UNION X` THEN Q.EXISTS_TAC `z` THEN
163  SRW_TAC [][]);
164
165val strong_lclosed_cofin_ind = store_thm(
166  "strong_lclosed_cofin_ind",
167  ``!P. (!s. P (var s)) /\
168        (!t1 t2. P t1 /\ P t2 /\ lclosed t1 /\ lclosed t2 ==>
169                 P (app t1 t2)) /\
170        (!t X. FINITE X /\
171               (!s. ~(s IN X) ==> P (open 0 (var s) t) /\
172                                  lclosed (open 0 (var s) t)) ==>
173               P (abs t))
174      ==>
175        !t. lclosed t ==> P t``,
176  GEN_TAC THEN STRIP_TAC THEN
177  Q_TAC SUFF_TAC `!t. lclosed t ==> P t /\ lclosed t` THEN1 SRW_TAC [][] THEN
178  HO_MATCH_MP_TAC lclosed_cofin_ind THEN
179  METIS_TAC [abs_lclosed_I, lclosed_rules]);
180
181val lclosed_E = store_thm(
182  "lclosed_E",
183  ``!t.
184      lclosed t ==>
185        (?s. (t = var s)) \/
186        (?t1 t2. (t = app t1 t2) /\ lclosed t1 /\ lclosed t2) \/
187        (?X u. (t = abs u) /\ FINITE X /\
188               !s. ~(s IN X) ==> lclosed (open 0 (var s) u))``,
189  HO_MATCH_MP_TAC strong_lclosed_cofin_ind THEN
190  SIMP_TAC (srw_ss()) [] THEN REPEAT STRIP_TAC THEN
191  METIS_TAC [lclosed_rules, abs_lclosed_I]);
192
193val lclosed_abs_cofin = store_thm(
194  "lclosed_abs_cofin",
195  ``lclosed (abs t) = ?X. FINITE X /\
196                          !s. ~(s IN X) ==> lclosed (open 0 (var s) t)``,
197  EQ_TAC THEN STRIP_TAC THENL [
198    IMP_RES_TAC lclosed_E THEN
199    FULL_SIMP_TAC (srw_ss()) [] THEN METIS_TAC [],
200    METIS_TAC [abs_lclosed_I]
201  ]);
202
203val _ = Datatype `ltype = tyOne | tyFun ltype ltype`;
204
205val _ = set_fixity "-->" (Infixr 700)
206val _ = overload_on ("-->", ``tyFun``);
207
208val valid_ctxt_def = Define`
209  (valid_ctxt [] = T) /\
210  (valid_ctxt ((x,A) :: G) = (!A'. ~MEM (x, A') G) /\ valid_ctxt G)
211`;
212val _ = export_rewrites ["valid_ctxt_def"]
213
214(* permutation over contexts swaps the strings and leaves the types alone *)
215val ctxtswap_def = Define`
216  (ctxtswap pi [] = []) /\
217  (ctxtswap pi (sA :: G) = (lswapstr pi (FST sA), SND sA) :: ctxtswap pi G)
218`;
219val _ = export_rewrites ["ctxtswap_def"]
220
221val ctxtswap_NIL = store_thm(
222  "ctxtswap_NIL",
223  ``ctxtswap [] G = G``,
224  Induct_on `G` THEN SRW_TAC [][]);
225val _ = export_rewrites ["ctxtswap_NIL"]
226
227val ctxtswap_inverse = store_thm(
228  "ctxtswap_inverse",
229  ``(ctxtswap pi (ctxtswap (REVERSE pi) G) = G) /\
230    (ctxtswap (REVERSE pi) (ctxtswap pi G) = G)``,
231  Induct_on `G` THEN SRW_TAC [][]);
232val _ = export_rewrites ["ctxtswap_inverse"]
233
234val ctxtswap_sing_inv = store_thm(
235  "ctxtswap_sing_inv",
236  ``ctxtswap [(x,y)] (ctxtswap [(x,y)] G) = G``,
237  METIS_TAC [listTheory.APPEND, listTheory.REVERSE_DEF, ctxtswap_inverse]);
238val _ = export_rewrites ["ctxtswap_sing_inv"]
239
240val ctxtswap_APPEND = store_thm(
241  "ctxtswap_APPEND",
242  ``!p1 p2. ctxtswap (p1 ++ p2) G = ctxtswap p1 (ctxtswap p2 G)``,
243  Induct_on `G` THEN SRW_TAC [][pmact_decompose]);
244
245(* context membership "respects" permutation *)
246val MEM_ctxtswap = store_thm(
247  "MEM_ctxtswap",
248  ``!G pi x A. MEM (lswapstr pi x, A) (ctxtswap pi G) = MEM (x,A) G``,
249  Induct THEN ASM_SIMP_TAC (srw_ss()) [pairTheory.FORALL_PROD]);
250val _ = export_rewrites ["MEM_ctxtswap"]
251
252(* valid_ctxt also respects permutation *)
253val valid_ctxt_swap0 = prove(
254  ``!G. valid_ctxt G ==> !x y. valid_ctxt (ctxtswap pi G)``,
255  Induct THEN ASM_SIMP_TAC (srw_ss()) [pairTheory.FORALL_PROD]);
256val valid_ctxt_swap = store_thm(
257  "valid_ctxt_swap",
258  ``valid_ctxt (ctxtswap pi G) = valid_ctxt G``,
259  METIS_TAC [valid_ctxt_swap0, ctxtswap_inverse]);
260val _ = export_rewrites ["valid_ctxt_swap"]
261
262(* the free variables of a context, defined with primitive recursion to
263   give us nice rewrites *)
264val ctxtFV_def = Define`
265  (ctxtFV [] = {}) /\
266  (ctxtFV (h::t) = FST h INSERT ctxtFV t)
267`;
268val _ = export_rewrites ["ctxtFV_def"]
269
270(* contexts have finitely many free variables *)
271val FINITE_ctxtFV = store_thm(
272  "FINITE_ctxtFV",
273  ``FINITE (ctxtFV G)``,
274  Induct_on `G` THEN SRW_TAC [][]);
275val _ = export_rewrites ["FINITE_ctxtFV"]
276
277val ctxtswap_fresh = store_thm(
278  "ctxtswap_fresh",
279  ``~(x IN ctxtFV G) /\ ~(y IN ctxtFV G) ==> (ctxtswap [(x,y)] G = G)``,
280  Induct_on `G` THEN ASM_SIMP_TAC (srw_ss()) [pairTheory.FORALL_PROD]);
281
282val ctxtFV_ctxtswap = store_thm(
283  "ctxtFV_ctxtswap",
284  ``ctxtFV (ctxtswap pi G) = ssetpm pi (ctxtFV G)``,
285  Induct_on `G` THEN SRW_TAC [][pmact_INSERT, stringpm_raw]);
286val _ = export_rewrites ["ctxtFV_ctxtswap"]
287
288(* more direct characterisation of ctxtFV *)
289val ctxtFV_MEM = store_thm(
290  "ctxtFV_MEM",
291  ``x IN ctxtFV G = (?A. MEM (x,A) G)``,
292  Induct_on `G` THEN
293  ASM_SIMP_TAC (srw_ss() ++ boolSimps.DNF_ss) [pairTheory.FORALL_PROD]);
294
295
296val valid_ctxt_CONS = prove(
297  ``!z ty. valid_ctxt ((z,ty) :: G) = ~(z IN ctxtFV G) /\ valid_ctxt G``,
298  Induct_on `G` THEN1 SRW_TAC [][] THEN
299  ASM_SIMP_TAC bool_ss [pairTheory.FORALL_PROD, Once valid_ctxt_def] THEN
300  SRW_TAC [][ctxtFV_MEM]);
301
302
303val (typing_rules, typing_ind, typing_cases) = Hol_reln`
304  (!G s ty. valid_ctxt G /\ MEM (s,ty) G ==> typing G (var s) ty) /\
305  (!G t1 t2 ty1 ty2.
306           typing G t1 (ty1 --> ty2) /\ typing G t2 ty1 ==>
307           typing G (app t1 t2) ty2) /\
308  (!G t s ty1 ty2.
309           typing ((s,ty1)::G) (open 0 (var s) t) ty2 /\
310           ~(s IN fv t)
311         ==>
312           typing G (abs t) (ty1 --> ty2))
313`;
314
315val typing_eqvt = store_thm(
316  "typing_eqvt",
317  ``!G t ty. typing G t ty ==> !pi. typing (ctxtswap pi G) (lnpm pi t) ty``,
318  HO_MATCH_MP_TAC typing_ind THEN SRW_TAC [][typing_rules, lnpm_open] THENL [
319    METIS_TAC [typing_rules],
320    MATCH_MP_TAC (last (CONJUNCTS typing_rules)) THEN
321    Q.EXISTS_TAC `lswapstr pi s` THEN
322    SRW_TAC [][fv_lnpm]
323  ]);
324
325
326val typing_valid_ctxt = store_thm(
327  "typing_valid_ctxt",
328  ``!G t ty. typing G t ty ==> valid_ctxt G``,
329  HO_MATCH_MP_TAC typing_ind THEN SRW_TAC [][]);
330
331val typing_lclosed = store_thm(
332  "typing_lclosed",
333  ``!G t ty. typing G t ty ==> lclosed t``,
334  HO_MATCH_MP_TAC typing_ind THEN SRW_TAC [][lclosed_rules] THEN
335  METIS_TAC [lclosed_rules]);
336
337val typing_bvc_ind = store_thm(
338  "typing_bvc_ind",
339  ``!P X. FINITE X /\
340          (!G s ty. valid_ctxt G /\ MEM (s,ty) G ==> P G (var s) ty) /\
341          (!G t1 t2 ty1 ty2.
342               P G t1 (ty1 --> ty2) /\ P G t2 ty1 /\
343               typing G t1 (ty1 --> ty2) /\ typing G t2 ty1 ==>
344               P G (app t1 t2) ty2) /\
345          (!G s t ty1 ty2.
346               ~(s IN X) /\ ~(s IN fv t) /\
347               P ((s,ty1)::G) (open 0 (var s) t) ty2 /\
348               typing ((s,ty1)::G) (open 0 (var s) t) ty2
349             ==>
350               P G (abs t) (ty1 --> ty2))
351        ==>
352          !G t ty. typing G t ty ==> P G t ty``,
353  REPEAT GEN_TAC THEN STRIP_TAC THEN
354  Q_TAC SUFF_TAC `!G t ty. typing G t ty ==>
355                           !pi. typing (ctxtswap pi G) (lnpm pi t) ty /\
356                                P (ctxtswap pi G) (lnpm pi t) ty`
357        THEN1 METIS_TAC [pmact_nil, ctxtswap_NIL] THEN
358  HO_MATCH_MP_TAC typing_ind THEN SRW_TAC [][lnpm_open, typing_rules] THENL [
359    METIS_TAC [typing_rules],
360    METIS_TAC [],
361    MATCH_MP_TAC (last (CONJUNCTS typing_rules)) THEN
362    Q.EXISTS_TAC `lswapstr pi s` THEN SRW_TAC [][fv_lnpm],
363
364    Q_TAC (NEW_TAC "z") `fv (lnpm pi t) UNION X UNION
365                         ctxtFV (ctxtswap pi G) UNION
366                         {lswapstr pi s}` THEN
367    FIRST_X_ASSUM MATCH_MP_TAC THEN Q.EXISTS_TAC `z` THEN
368    ASM_SIMP_TAC (srw_ss()) [] THEN
369    FIRST_X_ASSUM (Q.SPEC_THEN `(lswapstr pi s, z) :: pi` MP_TAC) THEN
370    ASM_SIMP_TAC (srw_ss()) [] THEN
371    STRIP_TAC THEN
372    `lnpm [(lswapstr pi s, z)] (lnpm pi t) = lnpm pi t`
373       by SRW_TAC [][lnpm_fresh, fv_lnpm] THEN
374    `~(s IN ctxtFV G)`
375       by (IMP_RES_TAC typing_valid_ctxt THEN
376           FULL_SIMP_TAC bool_ss [valid_ctxt_CONS] THEN
377           FULL_SIMP_TAC (srw_ss()) [ctxtFV_ctxtswap, pmact_decompose] THEN
378           FULL_SIMP_TAC (srw_ss()) []) THEN
379    `ctxtswap [(lswapstr pi s,z)] (ctxtswap pi G) = ctxtswap pi G`
380       by SRW_TAC [][ctxtswap_fresh] THEN
381    FULL_SIMP_TAC (srw_ss()) [GSYM pmact_decompose,
382                              GSYM ctxtswap_APPEND]
383  ]);
384
385val strong_typing_ind = IndDefLib.derive_strong_induction(typing_rules,
386                                                          typing_ind)
387
388val typing_cofin_ind = store_thm(
389  "typing_cofin_ind",
390  ``!P. (!G s ty. valid_ctxt G /\ MEM (s,ty) G ==> P G (var s) ty) /\
391        (!G t1 t2 ty1 ty2.
392            P G t1 (ty1 --> ty2) /\ P G t2 ty1  ==>
393            P G (app t1 t2) ty2) /\
394        (!G X t ty1 ty2.
395            FINITE X /\
396            (!s. ~(s IN X) ==> P ((s,ty1)::G) (open 0 (var s) t) ty2) ==>
397            P G (abs t) (ty1 --> ty2))
398      ==>
399        !G t ty. typing G t ty ==> P G t ty``,
400  GEN_TAC THEN STRIP_TAC THEN
401  Q_TAC SUFF_TAC `!G t ty. typing G t ty ==>
402                           !pi. P (ctxtswap pi G) (lnpm pi t) ty`
403        THEN1 METIS_TAC [pmact_nil, ctxtswap_NIL] THEN
404  HO_MATCH_MP_TAC strong_typing_ind THEN
405  SRW_TAC [][lnpm_open] THEN1 METIS_TAC [] THEN
406  FIRST_X_ASSUM MATCH_MP_TAC THEN
407  Q.EXISTS_TAC `fv (lnpm pi t) UNION ctxtFV (ctxtswap pi G)` THEN
408  SRW_TAC [][] THEN
409  FIRST_X_ASSUM (Q.SPEC_THEN `[(s',lswapstr pi s)] ++ pi` MP_TAC) THEN
410  ASM_SIMP_TAC (srw_ss()) [] THEN
411  Q_TAC SUFF_TAC `(lnpm ((s', lswapstr pi s)::pi) t = lnpm pi t) /\
412                  (ctxtswap ((s',lswapstr pi s)::pi) G = ctxtswap pi G)`
413        THEN1 SRW_TAC [][] THEN
414  `lnpm [(s',lswapstr pi s)] (lnpm pi t) = lnpm pi t`
415      by SRW_TAC [][lnpm_fresh, fv_lnpm] THEN
416  FULL_SIMP_TAC (srw_ss()) [GSYM pmact_decompose] THEN
417  `~(s IN ctxtFV G)`
418      by (IMP_RES_TAC typing_valid_ctxt THEN
419          FULL_SIMP_TAC bool_ss [valid_ctxt_CONS]) THEN
420  `ctxtswap ((s',lswapstr pi s)::pi) G =
421      ctxtswap ([(s',lswapstr pi s)] ++ pi) G`
422     by SRW_TAC [][] THEN
423  ` _ = ctxtswap [(s',lswapstr pi s)] (ctxtswap pi G)`
424     by SRW_TAC [][ctxtswap_APPEND] THEN
425  ` _ = ctxtswap pi G`
426     by SRW_TAC [][ctxtswap_fresh] THEN
427  SRW_TAC [][]);
428
429(* The approach in "Engineering Formal Metatheory" is to define a separate
430   "cofinite" relation, to prove the desired properties of this relation, and
431   to finish up by showing that it and the original correspond.  *)
432
433val (cotyping_rules, cotyping_ind, cotyping_cases) = Hol_reln`
434  (!G s ty. valid_ctxt G /\ MEM (s, ty) G ==> cotyping G (var s) ty) /\
435  (!G t1 t2 ty1 ty2.
436      cotyping G t1 (ty1 --> ty2) /\ cotyping G t2 ty1 ==>
437      cotyping G (app t1 t2) ty2) /\
438  (!G X t ty1 ty2.
439      FINITE X /\
440      (!s. ~(s IN X) ==> cotyping ((s,ty1)::G) (open 0 (var s) t) ty2) ==>
441      cotyping G (abs t) (ty1 --> ty2))
442`;
443
444val cotyping_typing = store_thm(
445  "cotyping_typing",
446  ``!G t ty. cotyping G t ty ==> typing G t ty``,
447  HO_MATCH_MP_TAC cotyping_ind THEN SRW_TAC [][typing_rules]
448    THEN1 METIS_TAC [typing_rules] THEN
449  MATCH_MP_TAC (last (CONJUNCTS typing_rules)) THEN
450  Q_TAC (NEW_TAC "z") `fv t UNION X` THEN METIS_TAC []);
451
452val typing_cotyping = store_thm(
453  "typing_cotyping",
454  ``!G t ty. typing G t ty ==> cotyping G t ty``,
455  HO_MATCH_MP_TAC typing_cofin_ind THEN SRW_TAC [][cotyping_rules] THEN
456  METIS_TAC [cotyping_rules]);
457
458val _ = export_theory();
459