1(* Thoughts about how to define alpha equivalence for types with sets
2of names as binders.  This is important for type schemas, where the
3model is apparently that you can have sets of binders so that things
4like
5
6  \forall \alpha \beta. \alpha -> \beta
7
8is the same thing as
9
10  \forall \beta \alpha. \alpha -> \beta
11
12not to mention \forall \alpha \beta. \beta -> \alpha
13and even       \forall \alpha \beta \gamma. \beta -> \alpha
14
15Christian Urban and I talked to Peter Homeier about this in September
162007, while in Munich, and PH suggested that we drop the idea of being
17able to do this by an Andy Pitts style definition, and that we instead
18define a relation that embodied some sort of constraint satisfaction
19routine.  This seems plausible, but in an alpha-equivalence test on a
20binary operator (a function space in the type example, say), the
21relation would have to "return" an updated context of equality
22bindings after having checked the match in one argument, so that this
23updated context could be passed onto the next argument.  There would
24also have to be stacks of pairs of sets, recording at which level
25names had occurred.  All told there'd be far too many parameters.
26
27I did try this approach, but it became rather gruesome.  The eventual,
28successful approach instead is very much in the style of Andy Pitts'
29original after all.
30*)
31
32open HolKernel boolLib Parse bossLib
33
34open binderLib boolSimps BasicProvers
35
36open nomsetTheory
37open pred_setTheory
38
39val _ = new_theory "type_schemas"
40
41val _ = Hol_datatype`
42  type = tyvar of string
43       | tyfun of type => type
44       | tyforall of string set => type
45`;
46
47val fv_def = Define`
48  (fv (tyvar s) = {s}) /\
49  (fv (tyfun ty1 ty2) = fv ty1 UNION fv ty2) /\
50  (fv (tyforall vs ty) = fv ty DIFF vs)
51`;
52val _ = export_rewrites ["fv_def"]
53
54val FINITE_fv = store_thm(
55  "FINITE_fv",
56  ``!ty. FINITE (fv ty)``,
57  Induct THEN SRW_TAC [][pred_setTheory.FINITE_DIFF]);
58val _ = export_rewrites ["FINITE_fv"]
59
60val raw_rtypm_def = Define`
61  (raw_rtypm pi (tyvar s) = tyvar (stringpm pi s)) /\
62  (raw_rtypm pi (tyfun ty1 ty2) = tyfun (raw_rtypm pi ty1) (raw_rtypm pi ty2)) /\
63  (raw_rtypm pi (tyforall vs ty) = tyforall (ssetpm pi vs) (raw_rtypm pi ty))
64`;
65val _ = export_rewrites["raw_rtypm_def"];
66
67val _ = overload_on("rty_pmact", ``mk_pmact raw_rtypm``);
68val _ = overload_on("rtypm", ``pmact rty_pmact``);
69
70val rtypm_raw = store_thm(
71  "rtypm_raw",
72  ``rtypm = raw_rtypm``,
73  SRW_TAC [][GSYM pmact_bijections] THEN
74  SRW_TAC [][is_pmact_def] THENL [
75    Induct_on `x` THEN SRW_TAC [][],
76    Induct_on `x` THEN SRW_TAC [][pmact_decompose],
77    FULL_SIMP_TAC (srw_ss()) [FUN_EQ_THM] THEN
78    Induct THEN SRW_TAC [][] THEN
79    METIS_TAC [pmact_permeq]
80  ]);
81
82val rtypm_thm = save_thm(
83"rtypm_thm",
84raw_rtypm_def |> SUBS [GSYM rtypm_raw]);
85val _ = export_rewrites["rtypm_thm"];
86
87val fv_rtypm = prove(
88  ``fv (rtypm pi ty) = ssetpm pi (fv ty)``,
89  Induct_on `ty` THEN SRW_TAC [][pmact_INSERT, pmact_UNION, pmact_DIFF]);
90
91val okpm_def = Define`
92  okpm pi bvs avds t ���
93     (!s. s IN bvs /\ s IN fv t ==> ~(stringpm pi s IN avds)) /\
94     (!s. ~(s IN bvs) /\ s IN fv t ==> (stringpm pi s = s))
95`;
96
97fun Prove(t,tac) = let val th = prove(t,tac)
98                   in
99                     BasicProvers.augment_srw_ss [rewrites [th]] ;
100                     th
101                   end
102
103val (aeq_rules, aeq_ind, aeq_cases) = Hol_reln`
104  (!s. aeq (tyvar s) (tyvar s)) /\
105  (!a b t u. aeq a t /\ aeq b u ==> aeq (tyfun a b) (tyfun t u)) /\
106  (!us vs t u pi1 pi2. okpm pi1 vs (fv t UNION fv u) t /\
107                       okpm pi2 us (fv t UNION fv u) u /\
108                       aeq (rtypm pi1 t) (rtypm pi2 u)
109                     ==>
110                       aeq (tyforall vs t) (tyforall us u))
111`;
112
113val aeq_forall = last (CONJUNCTS aeq_rules)
114
115val aeq_example1 = prove(
116  ``aeq (tyforall {x} (tyvar x)) (tyforall {y} (tyvar y))``,
117  MATCH_MP_TAC aeq_forall THEN
118  Q_TAC (NEW_TAC "z") `{x;y}` THEN
119  MAP_EVERY Q.EXISTS_TAC [`[(x,z)]`, `[(y,z)]`] THEN
120  SRW_TAC [][aeq_rules, okpm_def]);
121
122val aeq_example2 = prove(
123  ``aeq (tyforall {x} (tyvar x)) (tyforall {y} (tyvar a)) = (a = y)``,
124  ONCE_REWRITE_TAC [aeq_cases] THEN SRW_TAC [][okpm_def] THEN
125  SRW_TAC [][Once aeq_cases] THEN Cases_on `a = y` THEN SRW_TAC [][] THENL [
126    Q_TAC (NEW_TAC "z") `{x;a}` THEN
127    MAP_EVERY Q.EXISTS_TAC [`[(x, z)]`, `[(a, z)]`] THEN
128    SRW_TAC [][],
129    Cases_on `lswapstr pi2 a = a` THEN SRW_TAC [][] THEN
130    Cases_on `lswapstr pi1 x = a` THEN SRW_TAC [][stringpm_raw]
131  ]);
132
133val aeq_example3 = prove(
134  ``aeq (tyforall {x} (tyfun (tyvar x) (tyforall {x} (tyvar x))))
135        (tyforall {a} (tyfun (tyvar a) (tyforall {c;d} (tyvar d))))``,
136  MATCH_MP_TAC aeq_forall THEN SRW_TAC [][] THEN
137  Q_TAC (NEW_TAC "z") `{x;a}` THEN
138  MAP_EVERY Q.EXISTS_TAC [`[(x, z)]`, `[(a, z)]`] THEN
139  SRW_TAC [][Once aeq_cases, okpm_def] THEN
140  SRW_TAC [][aeq_rules] THEN
141  MATCH_MP_TAC aeq_forall THEN SRW_TAC [][] THEN
142  Q_TAC (NEW_TAC "q") `{swapstr a z d; z}` THEN
143  MAP_EVERY Q.EXISTS_TAC [`[(z, q)]`, `[(swapstr a z d, q)]`] THEN
144  SRW_TAC [][aeq_rules, okpm_def]);
145
146val aeq_example4 = prove(
147  ``~(a = c) ==> ~aeq (tyforall {x} (tyfun (tyvar x) (tyvar x)))
148                      (tyforall {a;c} (tyfun (tyvar a) (tyvar c)))``,
149  SRW_TAC [][Once aeq_cases] THEN SRW_TAC [][Once aeq_cases] THEN
150  SRW_TAC [][Once aeq_cases] THEN SRW_TAC [][Once aeq_cases] THEN
151  SRW_TAC [][okpm_def] THEN
152  SRW_TAC [DNF_ss][] THEN
153  METIS_TAC [pmact_injective]);
154
155fun find_small_cond t = let
156  fun recurse t k =
157    case dest_term t of
158      COMB(t1,t2) => if is_cond t then
159                       recurse t1 (fn () => recurse t2 (fn () => t))
160                     else
161                       recurse t1 (fn () => recurse t2 k)
162    | LAMB(_, bod) => recurse bod k
163    | _ => k()
164in
165  recurse t (fn () => raise raise mk_HOL_ERR "type_schemas" "find_small_cond"
166                                             "No cond in term")
167end
168
169fun mCOND_CASES_TAC (asl, g) = let
170  val c = find_small_cond g
171in
172  ASM_CASES_TAC (hd (#2 (strip_comb c))) THEN ASM_SIMP_TAC (srw_ss()) []
173end (asl, g)
174
175val rtypm_cpmpm = (SIMP_RULE (srw_ss()) []  o
176                   Q.INST [`pm` |-> `rty_pmact`] o
177                   INST_TYPE [alpha |-> ``:type``])
178                  pm_pm_cpmpm
179
180val lswapstr_lswapstr_cpmpm = stringpm_stringpm_cpmpm
181
182val rtypm_okpm = prove(
183  ``okpm (cpmpm pi pi0)
184             (setpm string_pmact pi bvs)
185             (setpm string_pmact pi avds)
186             (rtypm pi t) =
187    okpm pi0 bvs avds t``,
188  SRW_TAC [][okpm_def, fv_rtypm, pmact_IN, EQ_IMP_THM] THENL [
189    FULL_SIMP_TAC (srw_ss()) [Once lswapstr_lswapstr_cpmpm,
190                              pmact_inverse] THEN
191    FIRST_ASSUM (Q.SPEC_THEN `lswapstr pi s`
192                             (MATCH_MP_TAC o SIMP_RULE (srw_ss()) [])) THEN
193    SRW_TAC [][],
194
195    FIRST_X_ASSUM (Q.SPEC_THEN `lswapstr pi s` MP_TAC) THEN
196    SRW_TAC [][pmact_eqr] THEN
197    FULL_SIMP_TAC (srw_ss()) [Once lswapstr_lswapstr_cpmpm],
198
199    FULL_SIMP_TAC (srw_ss()) [Once lswapstr_lswapstr_cpmpm],
200
201    `lswapstr pi0 (lswapstr (REVERSE pi) s) = lswapstr (REVERSE pi) s`
202       by SRW_TAC [][] THEN
203    POP_ASSUM MP_TAC THEN
204    SIMP_TAC (srw_ss()) [pmact_eqr] THEN
205    SRW_TAC [][Once lswapstr_lswapstr_cpmpm]
206  ]);
207
208val aeq_rtypm = prove(
209  ``!t u. aeq t u ==> !pi. aeq (rtypm pi t) (rtypm pi u)``,
210  HO_MATCH_MP_TAC aeq_ind THEN SRW_TAC [][aeq_rules] THEN
211  MATCH_MP_TAC (last (CONJUNCTS aeq_rules))  THEN
212  MAP_EVERY Q.EXISTS_TAC [`cpmpm pi pi1`, `cpmpm pi pi2`] THEN
213  ASM_SIMP_TAC bool_ss [rtypm_okpm, fv_rtypm, GSYM pmact_UNION] THEN
214  ASM_SIMP_TAC (srw_ss()) [GSYM rtypm_cpmpm]);
215
216
217val INTER_INSERT = prove(
218  ``s INTER (e INSERT t) = if e IN s then e INSERT (s INTER t)
219                           else s INTER t``,
220  SRW_TAC [][EXTENSION] THEN METIS_TAC []);
221
222val avoid_finite_set0 = prove(
223  ``!s1. FINITE s1 ==>
224         FINITE ub /\ s1 SUBSET ub ==>
225         ?pi. (!x. x IN ub /\ ~(x IN s1) ==> ~(x IN patoms pi)) /\
226              (!x. x IN s2 /\ x IN s1 ==> ~(lswapstr pi x IN s1)) /\
227              (!x. ~(x IN s2) /\ x IN s1 ==> (lswapstr pi x = x)) ``,
228  HO_MATCH_MP_TAC FINITE_INDUCT THEN SRW_TAC [DNF_ss][] THEN1
229    (Q.EXISTS_TAC `[]` THEN SRW_TAC [][]) THEN
230  FULL_SIMP_TAC (srw_ss()) [] THEN
231  Cases_on `e IN s2` THENL [
232    Q_TAC (NEW_TAC "z") `e INSERT (patoms pi) UNION ub` THEN
233    Q.EXISTS_TAC `(z,e)::pi` THEN SRW_TAC [][] THENL [
234      METIS_TAC [],
235      SRW_TAC [][basic_swapTheory.swapstr_eq_left, pmact_eql,
236                 listsupp_REVERSE, lswapstr_unchanged],
237
238      SRW_TAC [][lswapstr_unchanged] THEN METIS_TAC [SUBSET_DEF],
239
240      SRW_TAC [][basic_swapTheory.swapstr_eq_left] THEN
241      SPOSE_NOT_THEN STRIP_ASSUME_TAC THEN SRW_TAC [][] THEN
242      `lswapstr pi x = x` by (
243        IMP_RES_TAC lswapstr_unchanged THEN
244        FULL_SIMP_TAC (srw_ss()) [] ) THEN
245      FULL_SIMP_TAC (srw_ss()) [SUBSET_DEF] THEN
246      METIS_TAC [],
247
248      `~(e IN patoms pi)` by SRW_TAC [][] THEN
249      `swapstr e z (lswapstr pi x) = lswapstr [(e,z)] (lswapstr pi x)`
250         by SRW_TAC [][] THEN
251      ` _ = lswapstr (cpmpm [(e,z)] pi) (lswapstr [(e,z)] x)`
252         by METIS_TAC [lswapstr_lswapstr_cpmpm] THEN
253      ` _ = lswapstr (cpmpm [(e,z)] pi) x`
254         by METIS_TAC [basic_swapTheory.swapstr_def, SUBSET_DEF,
255                       stringpm_thm, pairTheory.FST,
256                       pairTheory.SND] THEN
257      ` _ = lswapstr pi x` by SRW_TAC [][supp_fresh] THEN
258      METIS_TAC [],
259      METIS_TAC [SUBSET_DEF, basic_swapTheory.swapstr_def]
260    ],
261    Q.EXISTS_TAC `pi` THEN SRW_TAC [][] THENL [
262      SPOSE_NOT_THEN STRIP_ASSUME_TAC THEN SRW_TAC [][] THEN
263      `lswapstr pi x NOTIN patoms (REVERSE pi)` by (
264        RES_TAC THEN SRW_TAC [][listsupp_REVERSE] ) THEN
265      IMP_RES_TAC lswapstr_unchanged THEN
266      FULL_SIMP_TAC (srw_ss()) [] THEN POP_ASSUM (ASSUME_TAC o SYM) THEN
267      FULL_SIMP_TAC (srw_ss()) [],
268      SRW_TAC [][lswapstr_unchanged]
269    ]
270  ]);
271
272val avoid_finite_set =
273  (SIMP_RULE (srw_ss()) [] (Q.SPEC `ub` avoid_finite_set0))
274
275val aeq_refl = prove(
276  ``!t. aeq t t``,
277  Induct THEN SRW_TAC [][aeq_rules] THEN
278  MATCH_MP_TAC (last (CONJUNCTS aeq_rules)) THEN
279  Q_TAC SUFF_TAC `?pi. okpm pi f (fv t) t`
280        THEN1 METIS_TAC [UNION_IDEMPOT, aeq_rtypm] THEN
281  SRW_TAC [][okpm_def] THEN
282  METIS_TAC [FINITE_fv, avoid_finite_set]);
283
284val aeq_fv = prove(
285  ``!t1 t2. aeq t1 t2 ==> (fv t1 = fv t2)``,
286  HO_MATCH_MP_TAC aeq_ind THEN SRW_TAC [][EXTENSION, fv_rtypm] THEN
287  Cases_on `x IN vs` THEN SRW_TAC [][] THENL [
288    Cases_on `x IN us` THEN SRW_TAC [][] THEN
289    STRIP_TAC THEN
290    `stringpm pi2 x = x` by METIS_TAC [okpm_def] THEN
291    `stringpm (REVERSE pi2) x = x`
292       by METIS_TAC [pmact_eql] THEN
293    `stringpm (REVERSE pi1) x IN fv t` by METIS_TAC [] THEN
294    Cases_on `stringpm (REVERSE pi1) x IN vs` THENL [
295      `~(stringpm pi1 (stringpm (REVERSE pi1) x) IN fv u)`
296         by PROVE_TAC [okpm_def, IN_UNION] THEN
297      FULL_SIMP_TAC (srw_ss()) [],
298      `stringpm pi1 (stringpm (REVERSE pi1) x) = stringpm (REVERSE pi1) x`
299         by PROVE_TAC [okpm_def] THEN
300      FULL_SIMP_TAC (srw_ss()) [] THEN METIS_TAC []
301    ],
302    Cases_on `x IN us` THEN SRW_TAC [][] THENL [
303      STRIP_TAC THEN
304      `stringpm pi1 x = x` by PROVE_TAC [okpm_def] THEN
305      `stringpm (REVERSE pi1) x = x`
306         by METIS_TAC [pmact_eql] THEN
307      `stringpm (REVERSE pi2) x IN fv u` by METIS_TAC [] THEN
308      Cases_on `stringpm (REVERSE pi2) x IN us` THEN
309      PROVE_TAC [okpm_def, IN_UNION, pmact_inverse],
310
311      Cases_on `x IN fv t` THENL [
312        `stringpm pi1 x = x` by PROVE_TAC [okpm_def] THEN
313        `stringpm (REVERSE pi1) x = x`
314           by METIS_TAC [pmact_eql] THEN
315        `stringpm (REVERSE pi2) x IN fv u` by METIS_TAC [] THEN
316        Cases_on `stringpm (REVERSE pi2) x IN us` THEN
317        PROVE_TAC [okpm_def, IN_UNION, pmact_inverse],
318
319        SRW_TAC [][] THEN STRIP_TAC THEN
320        `stringpm pi2 x = x` by PROVE_TAC [okpm_def] THEN
321        `stringpm (REVERSE pi2) x = x`
322           by METIS_TAC [pmact_eql] THEN
323        `stringpm (REVERSE pi1) x IN fv t` by METIS_TAC [] THEN
324        Cases_on `stringpm (REVERSE pi1) x IN vs` THEN
325        PROVE_TAC [okpm_def, IN_UNION, pmact_inverse]
326      ]
327    ]
328  ]);
329
330val aeq_tyvar = prove(
331  ``aeq (tyvar s) t = (t = tyvar s)``,
332  ONCE_REWRITE_TAC [aeq_cases] THEN SRW_TAC [][]);
333
334val aeq_tyfun = prove(
335  ``aeq (tyfun ty1 ty2) ty = ?ty1' ty2'. (ty = tyfun ty1' ty2') /\
336                                         aeq ty1 ty1' /\ aeq ty2 ty2'``,
337  CONV_TAC (LAND_CONV (ONCE_REWRITE_CONV [aeq_cases])) THEN
338  SRW_TAC [][]);
339
340
341val aeq_sym = prove(
342  ``!t1 t2. aeq t1 t2 ==> aeq t2 t1``,
343  HO_MATCH_MP_TAC aeq_ind THEN SRW_TAC [][aeq_rules] THEN
344  MATCH_MP_TAC aeq_forall THEN METIS_TAC [UNION_COMM]);
345
346val strong_aeq_ind = theorem "aeq_strongind"
347
348val aeq_rtypm_eqn = prove(
349  ``aeq (rtypm pi ty1) (rtypm pi ty2) = aeq ty1 ty2``,
350  METIS_TAC [pmact_inverse, aeq_rtypm])
351
352val okpm_exists = store_thm(
353  "okpm_exists",
354  ``!s. FINITE s ==> ?pi. okpm pi bvs s ty``,
355  SIMP_TAC (srw_ss()) [okpm_def] THEN
356  HO_MATCH_MP_TAC FINITE_INDUCT THEN SRW_TAC [][] THENL [
357    Q.EXISTS_TAC `[]` THEN SRW_TAC [][],
358    Cases_on `e IN fv ty` THENL [
359      Cases_on `e IN bvs` THENL [
360        Q_TAC (NEW_TAC "z") `patoms pi UNION fv ty UNION {e} UNION s` THEN
361        Q.EXISTS_TAC `(z,e) :: pi` THEN SRW_TAC [][] THENL [
362          SRW_TAC [][basic_swapTheory.swapstr_eq_left, pmact_eql] THEN
363          SPOSE_NOT_THEN STRIP_ASSUME_TAC THEN SRW_TAC [][] THEN
364          METIS_TAC [lswapstr_unchanged,listsupp_REVERSE],
365          SRW_TAC [][basic_swapTheory.swapstr_def],
366          `~(z = s')` by METIS_TAC [] THEN
367          `~(e = s')` by METIS_TAC [] THEN SRW_TAC [][]
368        ],
369        Q.EXISTS_TAC `pi` THEN SRW_TAC [][] THEN
370        `stringpm pi e = e` by METIS_TAC [] THEN
371        `stringpm (REVERSE pi) e = e` by METIS_TAC [pmact_eql] THEN
372        SRW_TAC [][pmact_eql] THEN METIS_TAC []
373      ],
374      Q_TAC (NEW_TAC "z") `patoms pi UNION fv ty UNION {e} UNION s` THEN
375      Q.EXISTS_TAC `(z,e) :: pi` THEN SRW_TAC [][] THENL [
376        SRW_TAC [][basic_swapTheory.swapstr_eq_left, pmact_eql] THEN
377        METIS_TAC [lswapstr_unchanged,listsupp_REVERSE,stringpm_raw],
378        SRW_TAC [][basic_swapTheory.swapstr_def],
379        `~(z = s')` by METIS_TAC [] THEN
380        `~(e = s')` by METIS_TAC [] THEN SRW_TAC [][]
381      ]
382    ]
383  ]);
384
385val aeq_trans = prove(
386  ``!t1 t2. aeq t1 t2 ==> !t3. aeq t2 t3 ==> aeq t1 t3``,
387  HO_MATCH_MP_TAC strong_aeq_ind THEN SRW_TAC [][aeq_tyvar, aeq_tyfun] THEN
388  POP_ASSUM MP_TAC THEN
389  CONV_TAC (LAND_CONV (ONCE_REWRITE_CONV [aeq_cases])) THEN
390  SRW_TAC [][] THEN
391  MATCH_MP_TAC aeq_forall THEN
392  `!pi t3. aeq (rtypm pi (rtypm pi2 u)) (rtypm pi t3) ==>
393           aeq (rtypm pi (rtypm pi1 t)) (rtypm pi t3)`
394     by SRW_TAC [][aeq_rtypm_eqn] THEN
395  POP_ASSUM (Q.SPECL_THEN [`pi`, `rtypm (REVERSE pi) t3`]
396                          (ASSUME_TAC o GEN_ALL o
397                           SIMP_RULE (srw_ss()) [pmact_inverse])) THEN
398  `?pi. okpm pi us (fv t UNION fv u UNION fv u') u`
399     by SRW_TAC [][okpm_exists] THEN
400
401  MAP_EVERY Q.EXISTS_TAC [`pi ++ REVERSE pi2 ++ pi1`,
402                          `pi ++ REVERSE pi1' ++ pi2'`] THEN
403  FULL_SIMP_TAC (srw_ss()) [pmact_decompose] THEN
404  SRW_TAC [][okpm_def, pmact_decompose] THENL [
405    `~(stringpm pi1 s IN fv t) /\ ~(stringpm pi1 s IN fv u)`
406       by FULL_SIMP_TAC (srw_ss()) [okpm_def] THEN
407    `stringpm pi1 s IN fv (rtypm pi1 t)` by SRW_TAC [][fv_rtypm] THEN
408    `fv (rtypm pi1 t) = fv (rtypm pi2 u)` by METIS_TAC [aeq_fv] THEN
409    `stringpm pi1 s IN fv (rtypm pi2 u)` by METIS_TAC [] THEN
410    `stringpm (REVERSE pi2) (stringpm pi1 s) IN fv u`
411       by FULL_SIMP_TAC (srw_ss()) [fv_rtypm] THEN
412    `stringpm (REVERSE pi2) (stringpm pi1 s) IN us`
413       by (SPOSE_NOT_THEN ASSUME_TAC THEN
414           `stringpm (REVERSE pi2) (stringpm pi1 s) =
415            stringpm pi2 (stringpm (REVERSE pi2) (stringpm pi1 s))`
416              by METIS_TAC [okpm_def] THEN
417           ` _ = stringpm pi1 s` by SRW_TAC [][pmact_inverse] THEN
418           METIS_TAC []) THEN
419    FULL_SIMP_TAC (srw_ss()) [okpm_def],
420
421    `~(stringpm pi1 s IN fv t) /\ ~(stringpm pi1 s IN fv u)`
422       by FULL_SIMP_TAC (srw_ss()) [okpm_def] THEN
423    `stringpm pi1 s IN fv (rtypm pi1 t)` by SRW_TAC [][fv_rtypm] THEN
424    `fv (rtypm pi1 t) = fv (rtypm pi2 u)` by METIS_TAC [aeq_fv] THEN
425    `stringpm pi1 s IN fv (rtypm pi2 u)` by METIS_TAC [] THEN
426    `stringpm (REVERSE pi2) (stringpm pi1 s) IN fv u`
427       by FULL_SIMP_TAC (srw_ss()) [fv_rtypm] THEN
428    `stringpm (REVERSE pi2) (stringpm pi1 s) IN us`
429       by (SPOSE_NOT_THEN ASSUME_TAC THEN
430           `stringpm (REVERSE pi2) (stringpm pi1 s) =
431            stringpm pi2 (stringpm (REVERSE pi2) (stringpm pi1 s))`
432              by METIS_TAC [okpm_def] THEN
433           ` _ = stringpm pi1 s` by SRW_TAC [][pmact_inverse] THEN
434           METIS_TAC []) THEN
435    FULL_SIMP_TAC (srw_ss()) [okpm_def],
436
437    `stringpm pi1 s = s` by METIS_TAC [okpm_def] THEN
438    SRW_TAC [][] THEN
439    `s IN fv (rtypm pi1 t)` by (SRW_TAC [][fv_rtypm] THEN
440                                METIS_TAC [pmact_eql]) THEN
441    `fv (rtypm pi1 t) = fv (rtypm pi2 u)` by METIS_TAC [aeq_fv] THEN
442    `s IN fv (rtypm pi2 u)` by METIS_TAC [] THEN
443    `stringpm (REVERSE pi2) s IN fv u`
444       by FULL_SIMP_TAC (srw_ss()) [fv_rtypm] THEN
445    `~(stringpm (REVERSE pi2) s IN us)`
446       by (STRIP_TAC THEN
447           `~(stringpm pi2 (stringpm (REVERSE pi2) s) IN fv t)`
448              by METIS_TAC [okpm_def, IN_UNION] THEN
449           FULL_SIMP_TAC (srw_ss()) []) THEN
450    `stringpm pi2 (stringpm (REVERSE pi2) s) = stringpm (REVERSE pi2) s`
451       by METIS_TAC [okpm_def] THEN
452    FULL_SIMP_TAC (srw_ss()) [] THEN
453    POP_ASSUM (ASSUME_TAC o SYM) THEN FULL_SIMP_TAC (srw_ss()) [] THEN
454    FULL_SIMP_TAC (srw_ss()) [okpm_def],
455
456    `~(stringpm pi2' s IN fv u) /\ ~(stringpm pi2' s IN fv u')`
457       by FULL_SIMP_TAC (srw_ss()) [okpm_def] THEN
458    `stringpm pi2' s IN fv (rtypm pi2' u')` by SRW_TAC [][fv_rtypm] THEN
459    `fv (rtypm pi1' u) = fv (rtypm pi2' u')` by METIS_TAC [aeq_fv] THEN
460    `stringpm pi2' s IN fv (rtypm pi1' u)` by METIS_TAC [] THEN
461    `stringpm (REVERSE pi1') (stringpm pi2' s) IN fv u`
462       by FULL_SIMP_TAC (srw_ss()) [fv_rtypm] THEN
463    `stringpm (REVERSE pi1') (stringpm pi2' s) IN us`
464       by (SPOSE_NOT_THEN ASSUME_TAC THEN
465           `stringpm (REVERSE pi1') (stringpm pi2' s) =
466            stringpm pi1' (stringpm (REVERSE pi1') (stringpm pi2' s))`
467              by METIS_TAC [okpm_def] THEN
468           ` _ = stringpm pi2' s` by SRW_TAC [][] THEN
469           METIS_TAC []) THEN
470    FULL_SIMP_TAC (srw_ss()) [okpm_def],
471
472    `~(stringpm pi2' s IN fv u) /\ ~(stringpm pi2' s IN fv u')`
473       by FULL_SIMP_TAC (srw_ss()) [okpm_def] THEN
474    `stringpm pi2' s IN fv (rtypm pi2' u')` by SRW_TAC [][fv_rtypm] THEN
475    `fv (rtypm pi1' u) = fv (rtypm pi2' u')` by METIS_TAC [aeq_fv] THEN
476    `stringpm pi2' s IN fv (rtypm pi1' u)` by METIS_TAC [] THEN
477    `stringpm (REVERSE pi1') (stringpm pi2' s) IN fv u`
478       by FULL_SIMP_TAC (srw_ss()) [fv_rtypm] THEN
479    `stringpm (REVERSE pi1') (stringpm pi2' s) IN us`
480       by (SPOSE_NOT_THEN ASSUME_TAC THEN
481           `stringpm (REVERSE pi1') (stringpm pi2' s) =
482            stringpm pi1' (stringpm (REVERSE pi1') (stringpm pi2' s))`
483              by METIS_TAC [okpm_def] THEN
484           ` _ = stringpm pi2' s` by SRW_TAC [][] THEN
485           METIS_TAC []) THEN
486    FULL_SIMP_TAC (srw_ss()) [okpm_def],
487
488    `stringpm pi2' s = s` by METIS_TAC [okpm_def] THEN
489    SRW_TAC [][] THEN
490    `s IN fv (rtypm pi2' u')` by (SRW_TAC [][fv_rtypm] THEN
491                                  METIS_TAC [pmact_eql]) THEN
492    `fv (rtypm pi1' u) = fv (rtypm pi2' u')` by METIS_TAC [aeq_fv] THEN
493    `s IN fv (rtypm pi1' u)` by METIS_TAC [] THEN
494    `stringpm (REVERSE pi1') s IN fv u`
495       by FULL_SIMP_TAC (srw_ss()) [fv_rtypm] THEN
496    `~(stringpm (REVERSE pi1') s IN us)`
497       by (STRIP_TAC THEN
498           `~(stringpm pi1' (stringpm (REVERSE pi1') s) IN fv u')`
499              by METIS_TAC [okpm_def, IN_UNION] THEN
500           FULL_SIMP_TAC (srw_ss()) []) THEN
501    `stringpm pi1' (stringpm (REVERSE pi1') s) = stringpm (REVERSE pi1') s`
502       by METIS_TAC [okpm_def] THEN
503    FULL_SIMP_TAC (srw_ss()) [] THEN
504    POP_ASSUM (ASSUME_TAC o SYM) THEN FULL_SIMP_TAC (srw_ss()) [] THEN
505    FULL_SIMP_TAC (srw_ss()) [okpm_def],
506
507    Q_TAC SUFF_TAC `aeq (rtypm (pi ++ REVERSE pi2) (rtypm pi1 t))
508                        (rtypm (pi ++ REVERSE pi1') (rtypm pi2' u'))`
509          THEN1 SRW_TAC [][pmact_decompose] THEN
510    FIRST_X_ASSUM MATCH_MP_TAC THEN
511    SRW_TAC [][pmact_decompose, pmact_inverse] THEN
512    SRW_TAC [][aeq_rtypm_eqn] THEN
513    METIS_TAC [aeq_rtypm_eqn, pmact_inverse]
514  ]);
515
516val aeq_equiv = prove(
517  ``!t1 t2. aeq t1 t2 = (aeq t1 = aeq t2)``,
518  SRW_TAC [][FUN_EQ_THM] THEN METIS_TAC [aeq_trans, aeq_refl, aeq_sym]);
519
520val forall_respects_aeq = prove(
521  ``!vs t1 t2. aeq t1 t2 ==> aeq (tyforall vs t1) (tyforall vs t2)``,
522  SRW_TAC [][] THEN MATCH_MP_TAC aeq_forall THEN
523  `fv t1 = fv t2` by METIS_TAC [aeq_fv] THEN
524  SRW_TAC [][okpm_def] THEN
525  METIS_TAC [avoid_finite_set, FINITE_fv, aeq_rtypm]);
526
527val tyfun_respects_aeq = List.nth(CONJUNCTS aeq_rules, 1)
528fun mk_def (n,t) = {def_name = n ^ "_def", fname = n, func = t, fixity = NONE}
529
530val okpm_respects = prove(
531  ``!t1 t2. aeq t1 t2 ==> (okpm pi vs avoids t1 =
532                           okpm pi vs avoids t2)``,
533  SRW_TAC [][okpm_def] THEN METIS_TAC [aeq_fv]);
534
535val liftrule = quotientLib.define_quotient_types_std_rule {
536  types = [{name = "tyschema", equiv = aeq_equiv}],
537  defs = [mk_def ("raw_tyspm", ``raw_rtypm``),
538          mk_def ("tysFV", ``fv``),
539          mk_def ("TYALL", ``tyforall``),
540          mk_def ("TYFUN", ``tyfun``),
541          mk_def ("TYV", ``tyvar``),
542          mk_def ("OKpm", ``okpm``)],
543  respects = [SIMP_RULE (bool_ss ++ DNF_ss) [rtypm_raw] aeq_rtypm,
544              forall_respects_aeq, tyfun_respects_aeq,
545              aeq_fv, okpm_respects]}
546
547fun Save_thm(s,th) = save_thm(s,th) before export_rewrites [s]
548fun Store_thm(s,t,tac) = store_thm(s,t,tac) before export_rewrites [s]
549val tysFV_thm = Save_thm("tysFV_thm", liftrule fv_def)
550val tysFV_FINITE = Save_thm("tysFV_FINITE", liftrule FINITE_fv)
551val is_pmact_raw_tyspm = is_pmact_pmact |> Q.ISPEC `rty_pmact`
552                         |> REWRITE_RULE [rtypm_raw,is_pmact_def] |> liftrule
553val _ = overload_on("tys_pmact",``mk_pmact raw_tyspm``);
554val _ = overload_on("tyspm",``pmact tys_pmact``);
555val tyspm_raw = store_thm("tyspm_raw",``tyspm = raw_tyspm``,
556  SRW_TAC [][GSYM pmact_bijections,is_pmact_def,is_pmact_raw_tyspm])
557fun liftrule' th = th |> SUBS [rtypm_raw] |> liftrule |> SUBS [GSYM tyspm_raw]
558val tyspm_thm = Save_thm("tyspm_thm", liftrule' rtypm_thm)
559val tys_ind = save_thm("tys_ind", liftrule (TypeBase.induction_of ``:type``))
560val OKpm_thm = save_thm("OKpm_thm", liftrule okpm_def)
561val OKpm_eqvt = save_thm("OKpm_eqvt", liftrule' rtypm_okpm)
562val tysFV_tyspm = save_thm("tysFV_tyspm", liftrule' fv_rtypm)
563val tyseq_rule = liftrule' aeq_rules
564
565val OKpm_exists = save_thm("OKpm_exists", liftrule okpm_exists)
566
567val OKpm_increase = store_thm(
568  "OKpm_increase",
569  ``s1 SUBSET s2 /\ OKpm pi bvs s2 ty ==> OKpm pi bvs s1 ty``,
570  SRW_TAC [][OKpm_thm] THEN METIS_TAC [SUBSET_DEF]);
571
572val OKpm_avoids = prove(
573  ``!Set. FINITE Set  ==>
574          DISJOINT Set (tysFV ty) ==>
575          ?pi. DISJOINT (patoms pi) Set /\ OKpm pi bvs (tysFV ty) ty``,
576  SIMP_TAC (srw_ss()) [OKpm_thm] THEN
577  HO_MATCH_MP_TAC FINITE_INDUCT THEN SRW_TAC [][] THENL [
578    SRW_TAC [][avoid_finite_set],
579    FULL_SIMP_TAC (srw_ss()) [] THEN
580    SRW_TAC [][] THEN
581    Cases_on `e IN patoms pi` THENL [
582      Q_TAC (NEW_TAC "z") `patoms pi UNION tysFV ty UNION {e} UNION Set` THEN
583      Q.EXISTS_TAC `cpmpm [(z,e)] pi` THEN
584      SRW_TAC [][patoms_cpmpm] THENL [
585        SRW_TAC [][DISJOINT_DEF, EXTENSION] THEN
586        Cases_on `x IN Set` THEN SRW_TAC [][] THEN
587        `~(e = x) /\ ~(z = x)` by METIS_TAC [] THEN
588        SRW_TAC [][] THEN
589        FULL_SIMP_TAC (srw_ss()) [DISJOINT_DEF, EXTENSION] THEN
590        METIS_TAC [],
591        `stringpm (cpmpm [(z,e)] pi) s = stringpm [(z,e)] (stringpm pi s)`
592           by (ONCE_REWRITE_TAC [stringpm_stringpm_cpmpm] THEN
593               `~(e = s) /\ ~(z = s)` by METIS_TAC [] THEN
594               SRW_TAC [][]) THEN
595        SRW_TAC [][] THEN SRW_TAC [][basic_swapTheory.swapstr_def],
596        `~(e = s) /\ ~(z = s)` by METIS_TAC [] THEN
597        `stringpm (cpmpm [(z,e)] pi) s = stringpm [(z,e)] (stringpm pi s)`
598           by (ONCE_REWRITE_TAC [stringpm_stringpm_cpmpm] THEN
599               `~(e = s) /\ ~(z = s)` by METIS_TAC [] THEN
600               SRW_TAC [][]) THEN
601        SRW_TAC [][]
602      ],
603      Q.EXISTS_TAC `pi` THEN SRW_TAC [][]
604    ]
605  ]);
606
607val tys_fresh = store_thm(
608  "tys_fresh",
609  ``!ty a b. ~(a IN tysFV ty) /\ ~(b IN tysFV ty) ==> (tyspm [(a,b)] ty = ty)``,
610  HO_MATCH_MP_TAC tys_ind THEN SRW_TAC [][] THENL [
611    SRW_TAC [][] THEN MATCH_MP_TAC (last (CONJUNCTS tyseq_rule)) THEN
612    SRW_TAC [][] THEN
613    `setpm string_pmact [(a,b)] (tysFV ty) = tysFV ty`
614       by SRW_TAC [][GSYM tysFV_tyspm] THEN
615    `DISJOINT {a;b} (tysFV ty)` by SRW_TAC [][DISJOINT_DEF, EXTENSION] THEN
616    `?pi. DISJOINT (patoms pi) {a;b} /\ OKpm pi f (tysFV ty) ty `
617       by SRW_TAC [][OKpm_avoids] THEN
618    `~(a IN patoms pi) /\ ~(b IN patoms pi)`
619       by (FULL_SIMP_TAC (srw_ss()) [DISJOINT_DEF, EXTENSION] THEN
620           METIS_TAC []) THEN
621    `cpmpm [(a,b)] pi = pi`
622       by (MATCH_MP_TAC supp_fresh THEN SRW_TAC [][]) THEN
623    METIS_TAC [OKpm_eqvt],
624
625    MATCH_MP_TAC (last (CONJUNCTS tyseq_rule)) THEN
626    `FINITE (tysFV (tyspm [(a,b)] ty) UNION tysFV ty)` by SRW_TAC [][] THEN
627    `?pi. OKpm pi f (tysFV (tyspm [(a,b)] ty) UNION tysFV ty) ty`
628        by METIS_TAC [OKpm_exists] THEN
629    MAP_EVERY Q.EXISTS_TAC [`pi ++ [(a,b)]`, `pi`] THEN SRW_TAC [][] THENL [
630      SRW_TAC [][OKpm_thm, tysFV_tyspm] THENL [
631        SRW_TAC [][pmact_decompose] THEN
632        `~(stringpm pi (swapstr a b s) IN tysFV (tyspm [(a,b)] ty))`
633           by FULL_SIMP_TAC (srw_ss()) [OKpm_thm] THEN
634        FULL_SIMP_TAC (srw_ss()) [tysFV_tyspm],
635
636        SRW_TAC [][pmact_decompose] THEN
637        FULL_SIMP_TAC (srw_ss()) [OKpm_thm],
638
639        SRW_TAC [][pmact_decompose] THEN
640        `~(s = a)` by (STRIP_TAC THEN FULL_SIMP_TAC (srw_ss()) []) THEN
641        `~(s = b)` by (STRIP_TAC THEN FULL_SIMP_TAC (srw_ss()) []) THEN
642        FULL_SIMP_TAC (srw_ss()) [OKpm_thm]
643      ],
644      SRW_TAC [][pmact_decompose, pmact_sing_inv]
645    ],
646
647    MATCH_MP_TAC (last (CONJUNCTS tyseq_rule)) THEN
648    `FINITE (tysFV (tyspm [(a,b)] ty) UNION tysFV ty)` by SRW_TAC [][] THEN
649    `?pi. OKpm pi f (tysFV (tyspm [(a,b)] ty) UNION tysFV ty) ty`
650        by METIS_TAC [OKpm_exists] THEN
651    MAP_EVERY Q.EXISTS_TAC [`pi ++ [(a,b)]`, `pi`] THEN SRW_TAC [][] THENL [
652      SRW_TAC [][OKpm_thm, tysFV_tyspm] THENL [
653        SRW_TAC [][pmact_decompose] THEN
654        `~(stringpm pi (swapstr a b s) IN tysFV (tyspm [(a,b)] ty))`
655           by FULL_SIMP_TAC (srw_ss()) [OKpm_thm] THEN
656        FULL_SIMP_TAC (srw_ss()) [tysFV_tyspm],
657
658        SRW_TAC [][pmact_decompose] THEN
659        FULL_SIMP_TAC (srw_ss()) [OKpm_thm],
660
661        SRW_TAC [][pmact_decompose] THEN
662        `~(s = a)` by (STRIP_TAC THEN FULL_SIMP_TAC (srw_ss()) []) THEN
663        `~(s = b)` by (STRIP_TAC THEN FULL_SIMP_TAC (srw_ss()) []) THEN
664        FULL_SIMP_TAC (srw_ss()) [OKpm_thm]
665      ],
666      SRW_TAC [][pmact_decompose]
667    ],
668
669    MATCH_MP_TAC (last (CONJUNCTS tyseq_rule)) THEN
670    `FINITE (tysFV (tyspm [(a,b)] ty) UNION tysFV ty)` by SRW_TAC [][] THEN
671    `?pi. OKpm pi f (tysFV (tyspm [(a,b)] ty) UNION tysFV ty) ty`
672        by METIS_TAC [OKpm_exists] THEN
673    MAP_EVERY Q.EXISTS_TAC [`pi ++ [(a,b)]`, `pi`] THEN
674    SRW_TAC [][] THENL [
675      SRW_TAC [][OKpm_thm, tysFV_tyspm, pmact_decompose] THENL [
676        `~(stringpm pi (swapstr a b s) IN tysFV (tyspm [(a,b)] ty))`
677           by FULL_SIMP_TAC (srw_ss()) [OKpm_thm] THEN
678        FULL_SIMP_TAC (srw_ss()) [tysFV_tyspm, pmact_decompose],
679        FULL_SIMP_TAC (srw_ss()) [OKpm_thm],
680        `~(a = s)` by (STRIP_TAC THEN FULL_SIMP_TAC (srw_ss()) []) THEN
681        `~(b = s)` by (STRIP_TAC THEN FULL_SIMP_TAC (srw_ss()) []) THEN
682        FULL_SIMP_TAC (srw_ss()) [OKpm_thm]
683      ],
684      SRW_TAC [][pmact_decompose]
685    ]
686  ]);
687
688val _ = export_theory ();
689