1(* standard prelude *)
2open HolKernel boolLib Parse
3
4
5(* extra theorem-proving oomph from libraries *)
6open bossLib metisLib ncLib BasicProvers boolSimps
7
8
9
10(* ancestor theories *)
11open fsubtypesTheory pred_setTheory
12     sortingTheory (* for theorems about permutations *)
13
14val _ = new_theory "full_subtyping"
15
16val _ = add_rule {block_style = (AroundEachPhrase, (PP.INCONSISTENT, 2)),
17                  fixity = Infix(NONASSOC, 425),
18                  paren_style = OnlyIfNecessary,
19                  pp_elements = [HardSpace 1, TOK "|-", BreakSpace(1, 0),
20                                 BeginFinalBlock(PP.INCONSISTENT, 2),
21                                 TM, HardSpace 1, TOK "<:", BreakSpace(1,0)],
22                  term_name = "fsubtyping"}
23
24(* define subtyping rules : figure 26-2 *)
25val (fsubtyping_rules, fsubtyping_ind, fsubtyping_cases) = Hol_reln`
26  (!Gamma ty. wfctxt Gamma /\ ftyFV ty SUBSET cdom Gamma ==>
27              Gamma |- ty <: ty) /\
28  (!Gamma ty1 ty2 ty3. Gamma |- ty1 <: ty2 /\
29                       Gamma |- ty2 <: ty3 ==>
30                       Gamma |- ty1 <: ty3) /\
31  (!Gamma ty. wfctxt Gamma /\ ftyFV ty SUBSET cdom Gamma ==>
32              Gamma |- ty <: Top) /\
33  (!Gamma x ty. wfctxt Gamma /\ MEM (x, ty) Gamma ==>
34                Gamma |- TyVar x <: ty) /\
35  (!Gamma s1 t1 s2 t2.
36          Gamma |- t1 <: s1 /\ Gamma |- s2 <: t2 ==>
37          Gamma |- Fun s1 s2 <: Fun t1 t2) /\
38  (!Gamma x s1 t1 s2 t2.
39          Gamma |- t1 <: s1 /\
40          ((x,t1) :: Gamma) |- s2 <: t2 ==>
41          Gamma |- ForallTy x s1 s2 <: ForallTy x t1 t2)
42`;
43
44val fsubtyping_swap = store_thm(
45  "fsubtyping_swap",
46  ``!G t1 t2. G |- t1 <: t2 ==>
47              !x y. ctxtswap x y G |- fswap x y t1 <: fswap x y t2``,
48  HO_MATCH_MP_TAC fsubtyping_ind THEN REPEAT CONJ_TAC THENL [
49    SRW_TAC [][SUBSET_DEF, fsubtyping_rules],
50    METIS_TAC [fsubtyping_rules],
51    SRW_TAC [][SUBSET_DEF, fsubtyping_rules],
52    SRW_TAC [][fsubtyping_rules],
53    SRW_TAC [][fsubtyping_rules],
54    SRW_TAC [][SUBSET_DEF, fsubtyping_rules]
55  ]);
56
57val fsubtyping_wfctxt = store_thm(
58  "fsubtyping_wfctxt",
59  ``!G t1 t2. G |- t1 <: t2 ==> wfctxt G``,
60  HO_MATCH_MP_TAC fsubtyping_ind THEN SRW_TAC [][]);
61
62(* define algorithmic sub-typing, with a depth of derivation parameter *)
63val (algn_subtyping_rules, algn_subtyping_ind, algn_subtyping_cases) =
64  Hol_reln`
65    (!Gamma s. wfctxt Gamma /\ ftyFV s SUBSET cdom Gamma ==>
66               algn_subtyping 0 Gamma s Top) /\
67    (!Gamma x. wfctxt Gamma /\ x IN cdom Gamma ==>
68               algn_subtyping 0 Gamma (TyVar x) (TyVar x)) /\
69    (!Gamma x u t n. MEM (x, u) Gamma /\ algn_subtyping n Gamma u t ==>
70                     algn_subtyping (n + 1) Gamma (TyVar x) t) /\
71    (!Gamma t1 s1 t2 s2 n m.
72                 algn_subtyping n Gamma t1 s1 /\
73                 algn_subtyping m Gamma s2 t2 ==>
74                 algn_subtyping (MAX n m + 1) Gamma (Fun s1 s2) (Fun t1 t2)) /\
75    (!Gamma x s1 s2 t1 t2 m n.
76                 algn_subtyping m Gamma t1 s1 /\
77                 algn_subtyping n ((x,t1)::Gamma) s2 t2 ==>
78                 algn_subtyping (MAX m n + 1) Gamma (ForallTy x s1 s2)
79                                                    (ForallTy x t1 t2))
80`;
81
82val algn_subtyping_swap = store_thm(
83  "algn_subtyping_swap",
84  ``!n G t1 t2. algn_subtyping n G t1 t2 ==>
85                !x y. algn_subtyping n (ctxtswap x y G)
86                                       (fswap x y t1) (fswap x y t2)``,
87  HO_MATCH_MP_TAC algn_subtyping_ind THEN
88  SRW_TAC [][algn_subtyping_rules, SUBSET_DEF] THEN
89  (* only sa-trans-tvar case remains *)
90  MATCH_MP_TAC (List.nth(CONJUNCTS algn_subtyping_rules, 2)) THEN
91  Q.EXISTS_TAC `fswap x' y t1` THEN SRW_TAC [][]);
92
93val algn_subtyping_swap1_eqn = store_thm(
94  "algn_subtyping_swap1_eqn",
95  ``!n G t1 t2 x y. algn_subtyping n G (fswap x y t1) t2 =
96                    algn_subtyping n (ctxtswap x y G) t1 (fswap x y t2)``,
97  METIS_TAC [algn_subtyping_swap, ctxtswap_inv, fswap_inv]);
98
99val algn_subtyping_wfctxt = store_thm(
100  "algn_subtyping_wfctxt",
101  ``!n G t1 t2. algn_subtyping n G t1 t2 ==> wfctxt G``,
102  HO_MATCH_MP_TAC algn_subtyping_ind THEN SRW_TAC [][]);
103
104val cdom_APPEND = store_thm(
105  "cdom_APPEND",
106  ``cdom (X ++ Y) = cdom X UNION cdom Y``,
107  SRW_TAC [DNF_ss][cdom_MEM, EXTENSION]);
108val _ = export_rewrites ["cdom_APPEND"]
109
110val wfctxt_APPEND = store_thm(
111  "wfctxt_APPEND",
112  ``!X Y. DISJOINT (cdom X) (cdom Y) /\ wfctxt X /\ wfctxt Y ==>
113          wfctxt (X ++ Y)``,
114  Induct THEN
115  ASM_SIMP_TAC (srw_ss()) [pairTheory.FORALL_PROD, SUBSET_DEF]);
116
117val wfctxt_APPEND_down = store_thm(
118  "wfctxt_APPEND_down",
119  ``!X Y x y z. wfctxt (X ++ (x,y)::Y) /\ ftyFV z SUBSET cdom Y ==>
120                wfctxt (X ++ (x,z)::Y)``,
121  Induct THEN ASM_SIMP_TAC (srw_ss()) [pairTheory.FORALL_PROD] THEN
122  METIS_TAC []);
123
124val wfctxt_INSERT = store_thm(
125  "wfctxt_INSERT",
126  ``!D G v ty.
127        wfctxt (D ++ G) /\ ~(v IN cdom D) /\ ~(v IN cdom G) /\
128        ftyFV ty SUBSET cdom G ==>
129        wfctxt (D ++ (v,ty)::G)``,
130  Induct THEN ASM_SIMP_TAC (srw_ss()) [pairTheory.FORALL_PROD] THEN
131  SRW_TAC [][SUBSET_DEF] THEN METIS_TAC []);
132
133val wfctxt_APPEND_DISJOINT = store_thm(
134  "wfctxt_APPEND_DISJOINT",
135  ``!X Y. wfctxt (X ++ Y) ==> DISJOINT (cdom X) (cdom Y)``,
136  Induct THEN ASM_SIMP_TAC (srw_ss()) [pairTheory.FORALL_PROD]);
137
138val ctxtswap_APPEND = store_thm(
139  "ctxtswap_APPEND",
140  ``!X Y. ctxtswap x y (X ++ Y) = ctxtswap x y X ++ ctxtswap x y Y``,
141  Induct THEN SRW_TAC [][]);
142val _ = export_rewrites ["ctxtswap_APPEND"]
143
144val cdom_PERM = store_thm(
145  "cdom_PERM",
146  ``!G1 G2. PERM G1 G2 ==> (cdom G1 = cdom G2)``,
147  HO_MATCH_MP_TAC PERM_IND THEN
148  ASM_SIMP_TAC (srw_ss()) [pairTheory.FORALL_PROD, INSERT_COMM]);
149
150val algn_subtyping_FVs = store_thm(
151  "algn_subtyping_FVs",
152  ``!n G ty1 ty2. algn_subtyping n G ty1 ty2 ==>
153                  ftyFV ty1 SUBSET cdom G /\
154                  ftyFV ty2 SUBSET cdom G``,
155  HO_MATCH_MP_TAC algn_subtyping_ind THEN SRW_TAC [][] THENL [
156    METIS_TAC [cdom_MEM],
157    FULL_SIMP_TAC (srw_ss()) [SUBSET_DEF] THEN METIS_TAC [],
158    FULL_SIMP_TAC (srw_ss()) [SUBSET_DEF] THEN METIS_TAC []
159  ]);
160
161val strong_algn_subtyping_ind =
162    IndDefRules.derive_strong_induction (CONJUNCTS algn_subtyping_rules,
163                                         algn_subtyping_ind)
164
165(* lemma 28.4.1.1 *)
166val algn_subtyping_permutation = store_thm(
167  "algn_subtyping_permutation",
168  ``!n G t1 t2. algn_subtyping n G t1 t2 ==>
169                !D. PERM D G /\ wfctxt D ==>
170                    algn_subtyping n D t1 t2``,
171  HO_MATCH_MP_TAC strong_algn_subtyping_ind THEN REPEAT CONJ_TAC THENL [
172    METIS_TAC [algn_subtyping_rules, cdom_PERM],
173    METIS_TAC [algn_subtyping_rules, cdom_PERM],
174    METIS_TAC [algn_subtyping_rules, PERM_MEM_EQ],
175    METIS_TAC [algn_subtyping_rules],
176    REPEAT STRIP_TAC THEN
177    MATCH_MP_TAC (last (CONJUNCTS algn_subtyping_rules)) THEN
178    `wfctxt ((x,t1')::G)` by METIS_TAC [algn_subtyping_wfctxt] THEN
179    `~(x IN cdom G) /\ ftyFV t1' SUBSET cdom G`
180        by FULL_SIMP_TAC (srw_ss()) [] THEN
181    `~(x IN cdom D) /\ ftyFV t1' SUBSET cdom D`
182        by METIS_TAC [cdom_PERM] THEN
183    CONJ_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN SRW_TAC [][]
184  ]);
185
186(* lemma 28.4.1.2 *)
187val algn_subtyping_weakening = store_thm(
188  "algn_subtyping_weakening",
189  ``!n G t1 t2. algn_subtyping n G t1 t2 ==>
190                !D. wfctxt (D ++ G) ==> algn_subtyping n (D ++ G) t1 t2``,
191  HO_MATCH_MP_TAC strong_algn_subtyping_ind THEN REPEAT CONJ_TAC THENL[
192    SRW_TAC [][SUBSET_DEF, wfctxt_APPEND, algn_subtyping_rules],
193    SRW_TAC [][SUBSET_DEF, wfctxt_APPEND, algn_subtyping_rules],
194    METIS_TAC [listTheory.MEM_APPEND, algn_subtyping_rules],
195    SRW_TAC [][algn_subtyping_rules],
196
197    (* SA-ALL case *)
198    Q_TAC SUFF_TAC
199          `!G x s1 s2 t1 t2 m n.
200              algn_subtyping m G t1 s1 /\
201              (!D. wfctxt (D ++ G) ==> algn_subtyping m (D ++ G) t1 s1) /\
202              algn_subtyping n ((x,t1)::G) s2 t2 /\
203              (!D. wfctxt (D ++ (x,t1)::G) ==>
204                   algn_subtyping n (D ++ (x,t1)::G) s2 t2) ==>
205              !D. wfctxt (D ++ G) ==>
206                  algn_subtyping (MAX m n + 1) (D ++ G)
207                                 (ForallTy x s1 s2)
208                                 (ForallTy x t1 t2)` THEN1
209          SIMP_TAC (srw_ss()) [SUBSET_DEF] THEN
210    REPEAT STRIP_TAC THEN
211    (* generate fresh z *)
212    Q_TAC (NEW_TAC "z") `ftyFV t1 UNION cdom G UNION cdom D UNION ftyFV s2
213                         UNION ftyFV t2 UNION {x}` THEN
214
215    (* state that types have alpha equivalent forms involving z *)
216    `(ForallTy x s1 s2 = ForallTy z s1 (fswap z x s2)) /\
217     (ForallTy x t1 t2 = ForallTy z t1 (fswap z x t2))`
218        by SRW_TAC [][ForallTy_11] THEN
219
220    (* by SA-ALL rule if suffices to show (various side conditions drop
221       out because z is fresh) ... *)
222    Q_TAC SUFF_TAC
223          `algn_subtyping m (D ++ G) t1 s1 /\
224           algn_subtyping n ((z,t1)::(D ++ G)) (fswap z x s2) (fswap z x t2)`
225          THEN1 SRW_TAC [][algn_subtyping_rules, SUBSET_DEF] THEN
226
227    `wfctxt ((x,t1)::G) /\ wfctxt G` by METIS_TAC [algn_subtyping_wfctxt] THEN
228    `~(x IN cdom G) /\ (!v. v IN ftyFV t1 ==> v IN cdom G)`
229       by FULL_SIMP_TAC (srw_ss()) [wfctxt_def, SUBSET_DEF] THEN
230    `~(x IN ftyFV t1)` by METIS_TAC [] THEN
231
232    (* move swaps out, over (z,t1), the z turns into x; the t1 is unchanged
233       because z and x are both fresh wrt it, similarly G *)
234    Q_TAC SUFF_TAC
235          `algn_subtyping n ((x,t1)::ctxtswap z x D ++ G) s2 t2`
236          THEN1 SRW_TAC [][algn_subtyping_swap1_eqn, fswap_fresh,
237                           ctxtswap_fresh, wfctxt_ctxtFV_cdom] THEN
238
239    (* set up appeal to permutation result *)
240    `PERM ((x,t1)::ctxtswap z x D ++ G) (ctxtswap z x D ++ (x,t1)::G)`
241       by (SRW_TAC [][PERM_CONS_EQ_APPEND] THEN
242           METIS_TAC [PERM_REFL]) THEN
243
244    (* the permuted context is well-formed too: *)
245    `wfctxt (ctxtswap z x D ++ G)`
246       by (`ctxtswap z x D ++ G = ctxtswap z x (D ++ G)`
247              by SRW_TAC [][ctxtswap_fresh, wfctxt_ctxtFV_cdom] THEN
248           METIS_TAC [wfctxt_swap]) THEN
249    `wfctxt ((x,t1) :: ctxtswap z x D ++ G)`
250       by SRW_TAC [][SUBSET_DEF, wfctxt_APPEND] THEN
251
252    (* apply permutation result *)
253    Q_TAC SUFF_TAC
254          `algn_subtyping n (ctxtswap z x D ++ (x,t1)::G) s2 t2`
255          THEN1 METIS_TAC [algn_subtyping_permutation] THEN
256
257    (* apply IH  *)
258    Q_TAC SUFF_TAC `wfctxt (ctxtswap z x D ++ (x,t1)::G)`
259          THEN1 SRW_TAC [][] THEN
260
261    `ctxtswap z x D ++ (x,t1)::G = ctxtswap z x (D ++ (z,t1)::G)`
262       by SRW_TAC [][fswap_fresh, ctxtswap_fresh, wfctxt_ctxtFV_cdom] THEN
263    SRW_TAC [][wfctxt_INSERT, SUBSET_DEF]
264  ]);
265
266val algn_subtyping_Top_left = store_thm(
267  "algn_subtyping_Top_left",
268  ``algn_subtyping n G Top t = (t = Top) /\ (n = 0) /\ wfctxt G``,
269  ONCE_REWRITE_TAC [algn_subtyping_cases] THEN
270  SRW_TAC [][] THEN METIS_TAC []);
271val _ = export_rewrites ["algn_subtyping_Top_left"]
272
273val wfctxt_assoc_unique = store_thm(
274  "wfctxt_assoc_unique",
275  ``!G x y z. wfctxt G /\ MEM (x,y) G /\ MEM (x,z) G ==> (z = y)``,
276  Induct THEN ASM_SIMP_TAC (srw_ss()) [pairTheory.FORALL_PROD, cdom_MEM] THEN
277  METIS_TAC []);
278
279val algn_subtyping_foralltyleft_inversion = store_thm(
280  "algn_subtyping_foralltyleft_inversion",
281  ``~(x IN cdom G) /\ ~(x IN ftyFV t1) ==>
282    (algn_subtyping n G (ForallTy x t1 t2) t =
283     wfctxt G /\
284     ((t = Top) /\ (n = 0) /\ ftyFV (ForallTy x t1 t2) SUBSET cdom G \/
285      (?t1' t2' m1 m2. (t = ForallTy x t1' t2') /\
286                       (n = MAX m1 m2 + 1) /\
287                       algn_subtyping m1 G t1' t1 /\
288                       algn_subtyping m2 ((x,t1')::G) t2 t2')))``,
289  SIMP_TAC (srw_ss() ++ DNF_ss ++ SatisfySimps.SATISFY_ss)
290           [EQ_IMP_THM, algn_subtyping_rules, algn_subtyping_wfctxt] THEN
291  STRIP_TAC THEN
292  CONV_TAC (LAND_CONV (ONCE_REWRITE_CONV [algn_subtyping_cases])) THEN
293  SRW_TAC[][] THEN DISJ2_TAC THEN
294  Cases_on `x = x'` THEN FULL_SIMP_TAC (srw_ss()) [ForallTy_11] THENL [
295    METIS_TAC [],
296    Q.EXISTS_TAC `fswap x x' t2'` THEN
297    SRW_TAC [][algn_subtyping_swap1_eqn] THEN
298    `wfctxt G /\ wfctxt ((x',t1')::G)`
299       by METIS_TAC [algn_subtyping_wfctxt] THEN
300    `~(x' IN cdom G) /\ (!v. v IN ftyFV t1' ==> v IN cdom G)`
301       by METIS_TAC [SUBSET_DEF, wfctxt_def] THEN
302    `~(x' IN ftyFV t1') /\ ~(x IN ftyFV t1')` by METIS_TAC [] THEN
303    `ctxtswap x x' G = G`
304       by SRW_TAC [][ctxtswap_fresh, wfctxt_ctxtFV_cdom] THEN
305    SRW_TAC [][fswap_fresh] THEN
306    `ftyFV t2' SUBSET cdom ((x',t1')::G)`
307        by METIS_TAC [algn_subtyping_FVs] THEN
308    `~(x IN ftyFV t2')`
309        by METIS_TAC [SUBSET_DEF, cdom_def, IN_INSERT, pairTheory.FST] THEN
310    METIS_TAC []
311  ]);
312
313val lemma28_4_2_0 = prove(
314  ``!sz q. (fsize q = sz) ==>
315       (!i j G s t. algn_subtyping i G s q /\ algn_subtyping j G q t ==>
316                    ?k. algn_subtyping k G s t) /\
317       (!i j G D p m n x.
318                    algn_subtyping i (D ++ ((x,q) :: G)) m n /\
319                    algn_subtyping j G p q ==>
320                    ?k. algn_subtyping k (D ++ (x,p) :: G) m n)``,
321  HO_MATCH_MP_TAC arithmeticTheory.COMPLETE_INDUCTION THEN
322  GEN_TAC THEN
323  DISCH_THEN (STRIP_ASSUME_TAC o SIMP_RULE (srw_ss() ++ DNF_ss) []) THEN
324  GEN_TAC THEN STRIP_TAC THEN
325  (* part 1 *)
326  `!i j G s t.
327      algn_subtyping i G s q /\ algn_subtyping j G q t ==>
328      ?k. algn_subtyping k G s t`
329      by (HO_MATCH_MP_TAC arithmeticTheory.COMPLETE_INDUCTION THEN
330          GEN_TAC THEN STRIP_TAC THEN REPEAT GEN_TAC THEN
331          CONV_TAC (LAND_CONV
332                    (LAND_CONV
333                       (ONCE_REWRITE_CONV [algn_subtyping_cases]))) THEN
334          SRW_TAC [][] THENL [
335            (* Top case *)
336            FULL_SIMP_TAC (srw_ss()) [] THEN SRW_TAC [][] THEN
337            METIS_TAC [algn_subtyping_rules],
338            (* Tyvar case - 1*)
339            METIS_TAC [],
340            (* Tyvar case - 2*)
341            `?k. algn_subtyping k G u t`
342               by METIS_TAC [DECIDE ``n < n + 1``] THEN
343            METIS_TAC [algn_subtyping_rules],
344            (* Fun case *)
345            Q.PAT_ASSUM `algn_subtyping X Y (Fun t1 t2) Z`
346                        (MP_TAC o
347                         ONCE_REWRITE_RULE [algn_subtyping_cases]) THEN
348            SRW_TAC [][] THENL [
349              METIS_TAC [algn_subtyping_rules, ftyFV_thm, UNION_SUBSET,
350                         algn_subtyping_FVs],
351              `fsize t1 < fsize (Fun t1 t2) /\ fsize t2 < fsize (Fun t1 t2)`
352                 by SRW_TAC [numSimps.ARITH_ss][fsize_thm] THEN
353              `(?k1. algn_subtyping k1 G t1' s1) /\
354               (?k2. algn_subtyping k2 G s2 t2')`
355                 by METIS_TAC [] THEN
356              METIS_TAC [algn_subtyping_rules]
357            ],
358
359            (* ForallTy case *)
360            `wfctxt G /\ wfctxt ((x,t1)::G)`
361               by METIS_TAC [algn_subtyping_wfctxt] THEN
362            `~(x IN cdom G) /\ (!v. v IN ftyFV t1 ==> v IN cdom G)`
363               by FULL_SIMP_TAC (srw_ss()) [SUBSET_DEF] THEN
364            `~(x IN ftyFV t1)` by METIS_TAC [] THEN
365            `ftyFV s1 SUBSET cdom G /\ ftyFV s2 SUBSET cdom ((x,t1)::G)`
366               by METIS_TAC [algn_subtyping_FVs] THEN
367            `~(x IN ftyFV s1)` by METIS_TAC [SUBSET_DEF] THEN
368            Q.PAT_ASSUM `algn_subtyping X Y (ForallTy x t1 t2) Z` MP_TAC THEN
369            SRW_TAC [][algn_subtyping_foralltyleft_inversion] THENL [
370              FULL_SIMP_TAC (srw_ss()) [SUBSET_DEF] THEN
371              METIS_TAC [],
372              SRW_TAC [][ForallTy_11] THEN
373              `fsize t1 < fsize (ForallTy x t1 t2) /\
374               fsize t2 < fsize (ForallTy x t1 t2)`
375                 by SRW_TAC[numSimps.ARITH_ss][fsize_thm] THEN
376              `?k1. algn_subtyping k1 G t1' s1` by METIS_TAC [] THEN
377              Q_TAC SUFF_TAC
378                    `?k2. algn_subtyping k2 ((x,t1')::G) s2 t2'`
379                    THEN1 METIS_TAC [] THEN
380              Q_TAC SUFF_TAC
381                    `?k3. algn_subtyping k3 ((x,t1')::G) s2 t2`
382                    THEN1 METIS_TAC [] THEN
383              METIS_TAC [listTheory.APPEND]
384            ]
385          ]) THEN
386  (* part 2 *)
387  CONJ_TAC THEN1 FIRST_ASSUM ACCEPT_TAC THEN
388  HO_MATCH_MP_TAC arithmeticTheory.COMPLETE_INDUCTION THEN
389  REPEAT STRIP_TAC THEN
390  `ftyFV p SUBSET cdom G` by METIS_TAC [algn_subtyping_FVs] THEN
391  `wfctxt (D ++ (x,q)::G)` by METIS_TAC [algn_subtyping_wfctxt] THEN
392  `wfctxt (D ++ (x,p)::G)` by METIS_TAC [wfctxt_APPEND_down] THEN
393  Q.PAT_ASSUM `algn_subtyping X (D ++ Y :: G) M N` MP_TAC THEN
394  Q.ABBREV_TAC `xqctxt = D ++ (x,q) :: G` THEN
395  Q.ABBREV_TAC `xpctxt = D ++ (x,p) :: G` THEN
396  `cdom xpctxt = cdom xqctxt` by SRW_TAC [][Abbr`xpctxt`, Abbr`xqctxt`] THEN
397  CONV_TAC (LAND_CONV
398              (ONCE_REWRITE_CONV [algn_subtyping_cases])) THEN
399  SRW_TAC [][]THENL [
400    (* Top case *)
401    Q.EXISTS_TAC `0` THEN SRW_TAC [][algn_subtyping_rules],
402
403    (* tyvar refl case  *)
404    Q.EXISTS_TAC `0` THEN SRW_TAC [][algn_subtyping_rules],
405
406    (* tyvar trans case *)
407    Cases_on `x = x'` THENL [
408      `u = q`
409        by (`MEM (x,q) xqctxt` by SRW_TAC [][Abbr`xqctxt`] THEN
410            METIS_TAC [wfctxt_assoc_unique]) THEN
411      REPEAT VAR_EQ_TAC THEN
412      `n' < n' + 1` by DECIDE_TAC THEN
413      `?k. algn_subtyping k xpctxt q n` by METIS_TAC [] THEN
414      `MEM (x,p) xpctxt` by SRW_TAC [][Abbr`xpctxt`] THEN
415      Q_TAC SUFF_TAC
416            `?k1. algn_subtyping k1 xpctxt p n`
417            THEN1 METIS_TAC [algn_subtyping_rules] THEN
418      Q_TAC SUFF_TAC
419            `?k2. algn_subtyping k2 xpctxt p q`
420            THEN1 METIS_TAC [] THEN
421      `xpctxt = (D ++ [(x,p)]) ++ G`
422         by ASM_SIMP_TAC bool_ss [GSYM listTheory.APPEND_ASSOC, Abbr`xpctxt`,
423                                  listTheory.APPEND] THEN
424      METIS_TAC [algn_subtyping_weakening],
425
426      `MEM (x',u) xpctxt`
427         by FULL_SIMP_TAC (srw_ss()) [Abbr`xpctxt`, Abbr`xqctxt`] THEN
428      METIS_TAC [algn_subtyping_rules, DECIDE ``n' < n' + 1``]
429    ],
430
431    (* Fun case *)
432    `n' < MAX n' m' + 1 /\ m' < MAX n' m' + 1`
433       by SRW_TAC [numSimps.ARITH_ss][arithmeticTheory.MAX_DEF] THEN
434    METIS_TAC [algn_subtyping_rules],
435
436    (* Forall case *)
437    `n' < MAX m' n' + 1 /\ m' < MAX m' n' + 1`
438       by SRW_TAC [numSimps.ARITH_ss][arithmeticTheory.MAX_DEF] THEN
439    `?k1. algn_subtyping k1 xpctxt t1 s1` by METIS_TAC [] THEN
440    `((x',t1) :: xqctxt = ((x',t1)::D) ++ ((x,q)::G)) /\
441     ((x',t1) :: xpctxt = ((x',t1)::D) ++ ((x,p)::G))`
442       by SRW_TAC [][Abbr`xqctxt`, Abbr`xpctxt`] THEN
443    `?k2. algn_subtyping k2 ((x',t1)::xpctxt) s2 t2`
444       by METIS_TAC [] THEN
445    METIS_TAC [algn_subtyping_rules]
446  ]);
447
448val _ = remove_rules_for_term "dSUB"
449
450val _ = add_rule {block_style = (AroundEachPhrase, (PP.INCONSISTENT, 2)),
451                  fixity = Infix(NONASSOC, 425),
452                  paren_style = OnlyIfNecessary,
453                  pp_elements = [HardSpace 1, TOK "|->", BreakSpace(1, 0),
454                                 BeginFinalBlock(PP.INCONSISTENT, 2),
455                                 TM, HardSpace 1, TOK "<:", BreakSpace(1,0)],
456                  term_name = "alg_subtyping"}
457
458val alg_subtyping_def = Define`
459  G |-> ty1 <: ty2 = ?n. algn_subtyping n G ty1 ty2
460`;
461
462fun derive_rule th0 = let
463  val (vs, base) = strip_forall (concl th0)
464  val th = UNDISCH_ALL (SPEC_ALL th0)
465  val (f, args) = strip_comb (concl th)
466  val n = mk_var("n", numSyntax.num)
467  val pattern = mk_exists(n, list_mk_comb(f, n::tl args))
468  val witness = hd args
469  val ex_thm = EXISTS (pattern, witness) th
470  val discharged =
471      GENL vs (DISCH_ALL (REWRITE_RULE [GSYM alg_subtyping_def] ex_thm))
472  val exs_in = SIMP_RULE bool_ss [LEFT_FORALL_IMP_THM,
473                                  LEFT_EXISTS_AND_THM,
474                                  RIGHT_EXISTS_AND_THM] discharged
475in
476  REWRITE_RULE [GSYM alg_subtyping_def] exs_in
477end
478
479val alg_subtyping_rules = save_thm(
480  "alg_subtyping_rules",
481  LIST_CONJ (map derive_rule (CONJUNCTS algn_subtyping_rules)));
482
483val alg_subtyping_ind = save_thm(
484  "alg_subtyping_ind",
485    (Q.GEN `P` o
486     SIMP_RULE (srw_ss()) [GSYM alg_subtyping_def] o
487     CONV_RULE (RAND_CONV
488                  (SWAP_VARS_CONV THENC
489                   BINDER_CONV (SWAP_VARS_CONV THENC
490                                BINDER_CONV (SWAP_VARS_CONV THENC
491                                             BINDER_CONV FORALL_IMP_CONV)))) o
492     SIMP_RULE (srw_ss()) [] o
493     Q.SPEC `\n G ty1 ty2. P G ty1 ty2`) algn_subtyping_ind);
494
495val alg_subtyping_cases = save_thm(
496  "alg_subtyping_cases",
497    (REWRITE_CONV [alg_subtyping_def] THENC
498     ONCE_REWRITE_CONV [algn_subtyping_cases] THENC
499     SIMP_CONV (srw_ss()) [EXISTS_OR_THM] THENC
500     SIMP_CONV (srw_ss())
501               (map (INST_TYPE [alpha |-> numSyntax.num])
502                    [LEFT_EXISTS_AND_THM, RIGHT_EXISTS_AND_THM]) THENC
503     REWRITE_CONV [GSYM alg_subtyping_def])
504      ``Gamma |-> ty1 <: ty2``);
505
506val alg_subtyping_swap1_eqn = store_thm(
507  "alg_subtyping_swap1_eqn",
508  ``G |-> fswap x y ty1 <: ty2 = ctxtswap x y G |-> ty1 <: fswap x y ty2``,
509  METIS_TAC [alg_subtyping_def, algn_subtyping_swap1_eqn]);
510
511val alg_subtyping_refl = store_thm(
512  "alg_subtyping_refl",
513  ``!ty G. wfctxt G /\ ftyFV ty SUBSET cdom G ==> G |-> ty <: ty``,
514  HO_MATCH_MP_TAC fsubty_ind THEN
515  SRW_TAC [][alg_subtyping_rules] THEN
516  Q_TAC (NEW_TAC "z") `cdom G UNION ftyFV ty UNION ftyFV ty'` THEN
517  `ForallTy v ty ty' = ForallTy z ty (fswap z v ty')`
518     by SRW_TAC [][ForallTy_11] THEN
519  SRW_TAC [][] THEN
520  MATCH_MP_TAC (last (CONJUNCTS alg_subtyping_rules)) THEN
521  SRW_TAC [][alg_subtyping_swap1_eqn] THEN
522  FIRST_X_ASSUM MATCH_MP_TAC THEN SRW_TAC [][] THEN
523  FULL_SIMP_TAC (srw_ss()) [SUBSET_DEF] THEN
524  METIS_TAC [swapTheory.swapstr_def]);
525
526val alg_subtyping_trans = store_thm(
527  "alg_subtyping_trans",
528  ``G |-> ty1 <: ty2 /\ G |-> ty2 <: ty3 ==> G |-> ty1 <: ty3``,
529  METIS_TAC [alg_subtyping_def, lemma28_4_2_0]);
530
531val alg_soundcomplete = store_thm(
532  "alg_soundcomplete",
533  ``G |- ty1 <: ty2 = G |-> ty1 <: ty2``,
534  EQ_TAC THEN MAP_EVERY Q.ID_SPEC_TAC [`ty2`, `ty1`, `G`] THENL [
535    HO_MATCH_MP_TAC fsubtyping_ind THEN
536    SRW_TAC [][alg_subtyping_rules] THENL [
537      METIS_TAC [alg_subtyping_refl],
538      METIS_TAC [alg_subtyping_trans],
539      METIS_TAC [wfctxt_MEM, SUBSET_DEF, alg_subtyping_refl,
540                 alg_subtyping_rules]
541    ],
542    HO_MATCH_MP_TAC alg_subtyping_ind THEN
543    SRW_TAC [][fsubtyping_rules] THEN
544    METIS_TAC [fsubtyping_rules, fsubtyping_wfctxt]
545  ]);
546
547val _ = export_theory()
548
549