1open HolKernel Parse boolLib
2
3open simpLib boolSimps bossLib BasicProvers metisLib
4
5val _ = new_theory "swap"
6
7val _ = augment_srw_ss [rewrites [LET_THM]]
8
9open basic_swapTheory ncTheory NEWLib pred_setTheory markerLib;
10
11(* ----------------------------------------------------------------------
12    Swapping over sets of strings
13   ---------------------------------------------------------------------- *)
14
15val swapset_def = Define`
16  swapset x y ss = IMAGE (swapstr x y) ss
17`;
18
19val swapset_inverse = store_thm(
20  "swapset_inverse",
21  ``(swapset x y (swapset x y s) = s) /\
22    (swapset x y (swapset y x s) = s)``,
23  SRW_TAC [][swapset_def, EXTENSION, GSYM RIGHT_EXISTS_AND_THM]);
24val _ = export_rewrites ["swapset_inverse"]
25
26val swapset_comm = store_thm(
27  "swapset_comm",
28  ``swapset x y s = swapset y x s``,
29  METIS_TAC [swapset_def, swapstr_comm]);
30
31val swapset_id = store_thm(
32  "swapset_id",
33  ``swapset x x s = s``,
34  SRW_TAC [][swapset_def, EXTENSION]);
35val _ = export_rewrites ["swapset_id"]
36
37val swapset_UNION = store_thm(
38  "swapset_UNION",
39  ``swapset x y (P UNION Q) = swapset x y P UNION swapset x y Q``,
40  SRW_TAC [][swapset_def]);
41
42val swapset_EMPTY = store_thm(
43  "swapset_EMPTY",
44  ``swapset u v {} = {}``,
45  SRW_TAC [][swapset_def]);
46val _ = export_rewrites ["swapset_EMPTY"]
47
48val swapset_INSERT = store_thm(
49  "swapset_INSERT",
50  ``swapset u v (x INSERT s) = swapstr u v x INSERT swapset u v s``,
51  SRW_TAC [][swapset_def]);
52val _ = export_rewrites ["swapset_INSERT"]
53
54val swapset_DELETE = store_thm(
55  "swapset_DELETE",
56  ``swapset u v (s DELETE x) = swapset u v s DELETE swapstr u v x``,
57  SRW_TAC [][swapset_def, EXTENSION, GSYM swapstr_eq_left]);
58val _ = export_rewrites ["swapset_DELETE"]
59
60val swapset_FINITE = store_thm(
61  "swapset_FINITE",
62  ``FINITE (swapset x y s) = FINITE s``,
63  SRW_TAC [][swapset_def, EQ_IMP_THM]);
64val _ = export_rewrites ["swapset_FINITE"]
65
66val IN_swapset_lemma = prove(
67  ``x ��� swapset y z s ��� if x = y then z IN s
68                        else if x = z then y IN s
69                        else x IN s``,
70  SRW_TAC [][swapset_def, swapstr_def] THEN METIS_TAC []);
71
72val swapstr_IN_swapset0 = prove(
73  ``swapstr x y s IN swapset x y Set ��� s IN Set``,
74  SIMP_TAC (srw_ss()) [IN_swapset_lemma] THEN
75  MAP_EVERY Cases_on [`s = x`, `s = y`] THEN SRW_TAC [][] THEN
76  SRW_TAC [][swapstr_def]);
77
78val IN_swapset = store_thm(
79  "IN_swapset",
80  ``s IN swapset x y t ��� swapstr x y s IN t``,
81  METIS_TAC [swapstr_inverse, swapstr_IN_swapset0]);
82val _ = export_rewrites ["IN_swapset"]
83
84val swapset_11 = store_thm(
85  "swapset_11",
86  ``((swapset x y s1 = swapset x y s2) = (s1 = s2)) /\
87    ((swapset x y s1 = swapset y x s2) = (s1 = s2))``,
88  SRW_TAC [][EXTENSION] THEN
89  METIS_TAC [swapstr_inverse]);
90val _ = export_rewrites ["swapset_11"]
91
92(* ----------------------------------------------------------------------
93    Swapping over terms
94   ---------------------------------------------------------------------- *)
95
96
97val con_case_t = ``\c:'a. CON c``
98val var_case_t = ``\s:string. VAR (swapstr x y s)``
99val app_case_t = ``\(old1 : 'a nc) (old2 : 'a nc) t1:'a nc t2 . t1 @@ t2``
100val abs_case_t = ``\(tf: string -> 'a nc) (rf : string -> 'a nc).
101                      let nv = NEW ({x;y} UNION FV (ABS tf))
102                      in LAM nv (rf nv)``
103
104val thm0 =
105  GENL [``x:string``, ``y:string``]
106       (BETA_RULE
107          (ISPECL [con_case_t, var_case_t, app_case_t, abs_case_t]
108                  nc_RECURSION_WEAK))
109
110val thm1 = SIMP_RULE bool_ss [SKOLEM_THM, FORALL_AND_THM, ABS_DEF] thm0
111
112val swap_def = new_specification("swap_def", ["swap"], thm1);
113
114val swap_id = store_thm(
115  "swap_id",
116  ``!t. swap x x t = t``,
117  HO_MATCH_MP_TAC nc_INDUCTION THEN SRW_TAC [][swap_def] THEN
118  MATCH_MP_TAC (GSYM ALPHA) THEN NEW_ELIM_TAC);
119val _ = export_rewrites ["swap_id"]
120
121val swap_comm = store_thm(
122  "swap_comm",
123  ``!t. swap x y t = swap y x t``,
124  HO_MATCH_MP_TAC nc_INDUCTION THEN SRW_TAC [][swap_def] THEN
125  POP_ASSUM (Q.SPEC_THEN `NEW ({x;y} UNION (FV t DELETE x'))` SUBST1_TAC) THEN
126  Q_TAC SUFF_TAC `{x;y} = {y;x}` THEN1 PROVE_TAC [] THEN
127  SRW_TAC [][EXTENSION] THEN PROVE_TAC []);
128
129val fresh_var_swap = store_thm(
130  "fresh_var_swap",
131  ``!t. ~(v IN FV t) ==> ([VAR v/u] t = swap v u t)``,
132  HO_MATCH_MP_TAC nc_INDUCTION THEN REPEAT CONJ_TAC THENL [
133    SRW_TAC [][SUB_THM, swap_def],
134    SRW_TAC [][SUB_VAR, swap_def] THEN SRW_TAC [][swapstr_def],
135    SRW_TAC [][SUB_THM, swap_def],
136    REPEAT STRIP_TAC THEN SRW_TAC [][swap_def] THEN
137    NEW_ELIM_TAC THEN Q.X_GEN_TAC `w` THEN STRIP_TAC THENL [
138      (* w different from the bound variable of the lambda abstraction *)
139      `~(w IN FV (LAM x t))` by SRW_TAC [][] THEN
140      `LAM x t = LAM w ([VAR w/x] t)` by SRW_TAC [][ALPHA] THEN
141      SRW_TAC [][SUB_THM] THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
142      SRW_TAC [][FV_SUB] THEN FULL_SIMP_TAC (srw_ss()) [],
143      (* w equal to bound variable of lambda abstraction *)
144      SRW_TAC [][SUB_THM, lemma14a] THEN
145      FIRST_X_ASSUM (Q.SPEC_THEN `w` MP_TAC) THEN SRW_TAC [][lemma14a] THEN
146      FIRST_X_ASSUM MATCH_MP_TAC THEN FULL_SIMP_TAC (srw_ss()) []
147    ]
148  ]);
149
150val delete_non_element = prove(
151  ``~(x IN s) ==> (s DELETE x = s)``,
152  PROVE_TAC [DELETE_NON_ELEMENT]);
153
154val FV_swap = store_thm(
155  "FV_swap",
156  ``!t u v. FV (swap u v t) = swapset u v (FV t)``,
157  HO_MATCH_MP_TAC nc_INDUCTION THEN REPEAT CONJ_TAC THEN
158  SRW_TAC [][swap_def, swapset_UNION] THEN
159  NEW_ELIM_TAC THEN Q.X_GEN_TAC `w` THEN SRW_TAC [][] THENL [
160    SRW_TAC [][FV_SUB, swapset_UNION, dBTheory.UNION_DELETE,
161               delete_non_element],
162    SRW_TAC [][lemma14a]
163  ]);
164val _ = export_rewrites ["FV_swap"]
165
166val size_swap = store_thm(
167  "size_swap",
168  ``!t x y. size (swap x y t) = size t``,
169  HO_MATCH_MP_TAC nc_INDUCTION THEN SRW_TAC [][swap_def, size_thm]);
170val _ = export_rewrites ["size_swap"]
171
172val pvh_induction = store_thm(
173  "pvh_induction",
174  ``!P. (!s. P (VAR s)) /\ (!k. P (CON k)) /\
175        (!t u. P t /\ P u ==> P (t @@ u)) /\
176        (!v t. (!t'. (size t' = size t) ==> P t') ==> P (LAM v t)) ==>
177        (!t. P t)``,
178  GEN_TAC THEN STRIP_TAC THEN
179  completeInduct_on `size t` THEN
180  FULL_SIMP_TAC (srw_ss()) [GSYM RIGHT_FORALL_IMP_THM] THEN
181  GEN_TAC THEN
182  Q.SPEC_THEN `t` STRUCT_CASES_TAC nc_CASES THEN
183  SRW_TAC [numSimps.ARITH_ss][size_thm]);
184
185val swap_vsubst = store_thm(
186  "swap_vsubst",
187  ``!t u v x y. swap u v ([VAR x/y] t) =
188                [VAR (swapstr u v x)/swapstr u v y] (swap u v t)``,
189  HO_MATCH_MP_TAC pvh_induction THEN REPEAT STRIP_TAC THENL [
190    SRW_TAC [][SUB_VAR, swap_def],
191    SRW_TAC [][SUB_THM, swap_def],
192    SRW_TAC [][SUB_THM, swap_def],
193    Q_TAC (NEW_TAC "z") `{u; v; v'; x; y} UNION FV t` THEN
194    `LAM v t = LAM z ([VAR z/v] t)` by SRW_TAC [][ALPHA] THEN
195    Q.ABBREV_TAC `M = [VAR z/v] t` THEN
196    `size M = size t` by SRW_TAC [][Abbr`M`] THEN
197    ASM_SIMP_TAC (srw_ss()) [SUB_THM] THEN
198    `swap u v' (LAM z ([VAR x/y] M)) =
199       LAM z ([VAR (swapstr u v' x)/swapstr u v' y] (swap u v' M))`
200      by (CONV_TAC (LAND_CONV (REWRITE_CONV [swap_def])) THEN
201          NEW_ELIM_TAC THEN Q.X_GEN_TAC `a` THEN
202          STRIP_TAC THENL [
203            ASM_SIMP_TAC (srw_ss()) [] THEN
204            MATCH_MP_TAC (GSYM SIMPLE_ALPHA) THEN
205            `[VAR (swapstr u v' x)/swapstr u v' y] (swap u v' M) =
206             swap u v' ([VAR x/y] M)`
207               by SRW_TAC [][] THEN
208            POP_ASSUM SUBST_ALL_TAC THEN
209            SIMP_TAC (srw_ss()) [] THEN
210            SRW_TAC [][],
211            ASM_SIMP_TAC (srw_ss()) [lemma14a]
212          ]) THEN
213    POP_ASSUM SUBST_ALL_TAC THEN
214    ASM_SIMP_TAC (srw_ss()) [swap_def] THEN NEW_ELIM_TAC THEN
215    Q.X_GEN_TAC `a` THEN STRIP_TAC THENL [
216      `~(a IN FV (swap u v' M))` by ASM_SIMP_TAC (srw_ss()) [] THEN
217      ASM_SIMP_TAC (srw_ss())[GSYM SIMPLE_ALPHA] THEN
218      MATCH_MP_TAC (GSYM (last (CONJUNCTS SUB_THM))) THEN
219      SRW_TAC [][GSYM swapstr_eq_left],
220      ASM_SIMP_TAC (srw_ss()) [lemma14a] THEN
221      MATCH_MP_TAC (GSYM (last (CONJUNCTS SUB_THM))) THEN
222      SRW_TAC [][GSYM swapstr_eq_left]
223    ]
224  ]);
225
226val swap_LAM = prove(
227  ``swap x y (LAM v t) = LAM (swapstr x y v) (swap x y t)``,
228  SRW_TAC [][swap_def] THEN NEW_ELIM_TAC THEN Q.X_GEN_TAC `a` THEN
229  STRIP_TAC THENL [
230    SRW_TAC [][swap_vsubst] THEN
231    MATCH_MP_TAC (GSYM SIMPLE_ALPHA) THEN
232    SRW_TAC [][],
233    SRW_TAC [][lemma14a]
234  ]);
235
236val swap_thm = store_thm(
237  "swap_thm",
238  ``(swap x y (VAR s) = VAR (swapstr x y s)) /\
239    (swap x y (CON k) = CON k) /\
240    (swap x y (t @@ u) = swap x y t @@ swap x y u) /\
241    (swap x y (LAM v t) = LAM (swapstr x y v) (swap x y t))``,
242  SRW_TAC [][swap_LAM] THEN SRW_TAC [][swap_def]);
243val _ = export_rewrites ["swap_thm"]
244
245val swap_swap = store_thm(
246  "swap_swap",
247  ``!t u v x y. swap (swapstr x y u) (swapstr x y v) (swap x y t) =
248                swap x y (swap u v t)``,
249  HO_MATCH_MP_TAC nc_INDUCTION THEN REPEAT CONJ_TAC THENL [
250    SRW_TAC [][],
251    SRW_TAC [][],
252    REPEAT STRIP_TAC THEN SIMP_TAC (srw_ss()) [] THEN
253    CONJ_TAC THEN FIRST_ASSUM MATCH_ACCEPT_TAC,
254    SRW_TAC [][] THEN
255    METIS_TAC [lemma14a]
256  ]);
257val _ = export_rewrites ["swap_swap"]
258
259val swap_swap2 = store_thm(
260  "swap_swap2",
261  ``swap x y (swap (swapstr x y a) (swapstr x y b) t) =
262    swap a b (swap x y t)``,
263  CONV_TAC (LAND_CONV (ONCE_REWRITE_CONV [GSYM swap_swap])) THEN
264  REWRITE_TAC [swapstr_inverse]);
265val _ = export_rewrites ["swap_swap2"]
266
267val swap_inverse_lemma = prove(
268  ``!t. swap x y (swap x y t) = t``,
269  HO_MATCH_MP_TAC pvh_induction THEN SRW_TAC [][swap_thm]);
270
271val swap_inverse = store_thm(
272  "swap_inverse",
273  ``(swap x y (swap x y t) = t) /\ (swap y x (swap x y t) = t)``,
274  METIS_TAC [swap_inverse_lemma, swap_comm]);
275val _ = export_rewrites ["swap_inverse"]
276
277val swap_ALPHA = store_thm(
278  "swap_ALPHA",
279  ``~(v IN FV M) ==> (LAM v (swap v u M) = LAM u M)``,
280  SRW_TAC [][GSYM fresh_var_swap, GSYM SIMPLE_ALPHA]);
281
282Theorem LAM_INJ_swap:
283    (LAM v1 t1 = LAM v2 t2) ��� v1 ��� FV (LAM v2 t2) ��� (t1 = swap v1 v2 t2)
284Proof
285  SRW_TAC [][EQ_IMP_THM] THENL [
286    Cases_on `v1 IN FV t2` THEN ASM_SIMP_TAC (srw_ss()) [] THEN
287    FIRST_X_ASSUM (MP_TAC o Q.AP_TERM `FV`) THEN
288    ASM_SIMP_TAC (srw_ss()) [EXTENSION] THEN
289    DISCH_THEN (Q.SPEC_THEN `v1` MP_TAC) THEN
290    ASM_REWRITE_TAC [],
291    Cases_on `v1 = v2` THEN FULL_SIMP_TAC (srw_ss()) [] THEN
292    IMP_RES_TAC LAM_INJ_ALPHA_FV THEN
293    IMP_RES_TAC INJECTIVITY_LEMMA1 THEN
294    METIS_TAC [fresh_var_swap],
295    METIS_TAC [swap_ALPHA],
296    SRW_TAC [][]
297  ]
298QED
299
300val swap_subst = store_thm(
301  "swap_subst",
302  ``!M N v x y.
303      swap x y ([N/v] M) = [swap x y N / swapstr x y v] (swap x y M)``,
304  REPEAT GEN_TAC THEN Q.ID_SPEC_TAC `M` THEN
305  HO_MATCH_MP_TAC nc_INDUCTION2 THEN Q.EXISTS_TAC `{x;y;v} UNION FV N` THEN
306  SRW_TAC [][SUB_VAR, SUB_THM] THEN
307  `~(y' = swapstr x y v)` by SRW_TAC [][swapstr_def] THEN
308  SRW_TAC [][SUB_THM]);
309
310val swap_subst_out = store_thm(
311  "swap_subst_out",
312  ``[N/v] (swap x y M) = swap x y ([swap x y N/swapstr x y v] M)``,
313  METIS_TAC [swap_subst, swap_inverse]);
314
315val swap_11 = store_thm(
316  "swap_11",
317  ``((swap x y t1 = swap x y t2) = (t1 = t2)) /\
318    ((swap x y t1 = swap y x t2) = (t1 = t2))``,
319  METIS_TAC [swap_comm, swap_inverse]);
320val _ = export_rewrites ["swap_11"]
321
322val swap_eql = store_thm(
323  "swap_eql",
324  ``(swap x y t = u) = (t = swap x y u)``,
325  METIS_TAC [swap_inverse]);
326
327val swap_eq_var = store_thm(
328  "swap_eq_var",
329  ``((swap x y t = VAR s) = (t = VAR (swapstr x y s))) /\
330    ((VAR s = swap x y t) = (VAR (swapstr x y s) = t))``,
331  SRW_TAC [][swap_eql] THEN SRW_TAC [][GSYM swap_eql]);
332val swap_eq_app = store_thm(
333  "swap_eq_app",
334  ``((swap x y t = M @@ N) = (t = swap x y M @@ swap x y N)) /\
335    ((M @@ N = swap x y t) = (swap x y M @@ swap x y N = t))``,
336  SRW_TAC [][swap_eql] THEN SRW_TAC [][GSYM swap_eql]);
337val swap_eq_con = store_thm(
338  "swap_eq_con",
339  ``((swap x y t = CON k) = (t = CON k)) /\
340    ((CON k = swap x y t) = (CON k = t))``,
341  SRW_TAC [][swap_eql] THEN SRW_TAC [][GSYM swap_eql]);
342val swap_eq_lam = store_thm(
343  "swap_eq_lam",
344  ``((swap x y t = LAM v M) = (t = LAM (swapstr x y v) (swap x y M))) /\
345    ((LAM v M = swap x y t) = (LAM (swapstr x y v) (swap x y M) = t))``,
346  SRW_TAC [][swap_eql] THEN SRW_TAC [][GSYM swap_eql]);
347val _ = export_rewrites ["swap_eq_var", "swap_eq_con", "swap_eq_app",
348                         "swap_eq_lam"]
349
350(* ----------------------------------------------------------------------
351    supporting recursion over lambda calculus terms using swap
352   ---------------------------------------------------------------------- *)
353
354val swapping_def = Define`
355  swapping f fv ���
356    (!x z. f x x z = z) /\
357    (!x y z. f x y (f x y z) = z) /\
358    (!x y z. ~(x IN fv z) /\ ~(y IN fv z) ==> (f x y z = z)) /\
359    (!x y z s. s IN fv (f x y z) ��� swapstr x y s IN fv z)
360`
361
362val LET_NEW_congruence = store_thm(
363  "LET_NEW_congruence",
364  ``(X = Y:string set) ==> FINITE Y ==> (!v. ~(v IN Y) ==> (P v = Q v)) ==>
365    (LET P (NEW X)  = LET Q (NEW Y))``,
366  SRW_TAC [][] THEN NEW_ELIM_TAC THEN SRW_TAC [][]);
367
368val null_swapping = store_thm(
369  "null_swapping",
370  ``swapping (\x y z. z) (K {})``,
371  (* can't write \x. {} for second argument above; it tweaks a bug in
372     HO_PART_MATCH *)
373  SRW_TAC [][swapping_def]);
374val _ = export_rewrites ["null_swapping"]
375
376val swap_identity = store_thm(
377  "swap_identity",
378  ``!t x y. ~(x IN FV t) /\ ~(y IN FV t) ==> (swap x y t = t)``,
379  HO_MATCH_MP_TAC nc_INDUCTION THEN SIMP_TAC (srw_ss()) [swap_thm] THEN
380  MAP_EVERY Q.X_GEN_TAC [`v`, `t`] THEN STRIP_TAC THEN
381  MAP_EVERY Q.X_GEN_TAC [`x`, `y`] THEN STRIP_TAC THENL [
382    `swap x y t = t` by METIS_TAC [lemma14a] THEN
383    Cases_on `v = x` THEN SRW_TAC [][swapstr_def] THEN
384    MATCH_MP_TAC INJECTIVITY_LEMMA3 THEN Q.EXISTS_TAC `v` THEN
385    SRW_TAC [][lemma14b],
386    SRW_TAC [][] THEN METIS_TAC [swap_ALPHA, swap_comm],
387    SRW_TAC [][] THEN METIS_TAC [swap_ALPHA, swap_comm],
388    SRW_TAC [][]
389  ]);
390
391val nc_swapping = store_thm(
392  "nc_swapping",
393  ``swapping swap FV``,
394  SIMP_TAC (srw_ss()) [swap_swap, swapping_def, swap_identity]);
395
396val str_swapping = store_thm(
397  "str_swapping",
398  ``swapping swapstr (\s. {s})``,
399  REWRITE_TAC [swapping_def] THEN SRW_TAC [][swapstr_eq_left]);
400
401val swapping_implies_empty_swap = store_thm(
402  "swapping_implies_empty_swap",
403  ``swapping sw fv /\ (fv t = {}) ==> !x y. sw x y t = t``,
404  SRW_TAC [][swapping_def]);
405
406val swapping_implies_identity_swap = store_thm(
407  "swapping_implies_identity_swap",
408  ``!sw fv x y t. swapping sw fv /\ ~(x IN fv t) /\ ~(y IN fv t) ==>
409                  (sw x y t = t)``,
410  SRW_TAC [][swapping_def]);
411
412
413val swapfn_def = Define`
414  swapfn (dswap:string -> string -> 'a -> 'a)
415         (rswap:string -> string -> 'b -> 'b)
416         x y f d = rswap x y (f (dswap x y d))
417`;
418
419val fresh_new_subst0 = prove(
420  ``FINITE X /\ (!p. FINITE (pFV p)) ==>
421    ((let v = NEW (FV (LAM x u) UNION pFV p UNION X) in f v ([VAR v/x] u)) =
422     (let v = NEW (FV (LAM x u) UNION pFV p UNION X) in f v (swap v x u)))``,
423  STRIP_TAC THEN NEW_ELIM_TAC THEN REPEAT STRIP_TAC THEN
424  SRW_TAC [][fresh_var_swap, lemma14a]);
425
426
427val lemma =
428    (SIMP_RULE bool_ss [FUN_EQ_THM, ABS_DEF, fresh_new_subst0,
429                        ASSUME ``FINITE (X:string set)``,
430                        ASSUME ``!p:'b. FINITE (pFV p : string set)``] o
431     Q.INST [`lam'` |-> `lam`] o
432     Q.INST [`lam` |->
433             `\r t p.
434                 let v = NEW (FV (ABS t) UNION pFV p UNION X)
435                 in
436                   lam' (r v) v (t v) p`] o
437     INST_TYPE [beta |-> (beta --> gamma)] o
438     CONJUNCT1 o
439     CONV_RULE EXISTS_UNIQUE_CONV o
440     SPEC_ALL)
441    nc_RECURSION
442
443val swap_RECURSION_pgeneric = store_thm(
444  "swap_RECURSION_pgeneric",
445  ``swapping rswap rFV /\ swapping pswap pFV /\
446
447    FINITE X /\ (!p. FINITE (pFV p)) /\
448
449    (!k p. rFV (con k p) SUBSET (X UNION pFV p)) /\
450    (!s p. rFV (var s p) SUBSET (s INSERT pFV p UNION X)) /\
451    (!t' u' t u p.
452        (!p. rFV (t' p) SUBSET (FV t UNION pFV p UNION X)) /\
453        (!p. rFV (u' p) SUBSET (FV u UNION pFV p UNION X)) ==>
454        rFV (app t' u' t u p) SUBSET FV t UNION FV u UNION pFV p UNION X) /\
455    (!t' v t p.
456        (!p. rFV (t' p) SUBSET (FV t UNION pFV p UNION X)) ==>
457        rFV (lam t' v t p) SUBSET (FV (LAM v t) UNION pFV p UNION X)) /\
458
459    (!k x y p. ~(x IN X) /\ ~(y IN X) ==>
460               (rswap x y (con k p) = con k (pswap x y p))) /\
461    (!s x y p. ~(x IN X) /\ ~(y IN X) ==>
462               (rswap x y (var s p) = var (swapstr x y s) (pswap x y p))) /\
463    (!t t' u u' x y p.
464         ~(x IN X) /\ ~(y IN X) ==>
465         (rswap x y (app t' u' t u p) =
466          app (swapfn pswap rswap x y t') (swapfn pswap rswap x y u')
467              (swap x y t) (swap x y u)
468              (pswap x y p))) /\
469    (!t' t x y v p.
470         ~(x IN X) /\ ~(y IN X) ==>
471         (rswap x y (lam t' v t p) =
472          lam (swapfn pswap rswap x y t')
473              (swapstr x y v) (swap x y t) (pswap x y p))) ==>
474    ?hom : 'a nc -> 'b -> 'c.
475      ((!k p. hom (CON k) p = con k p) /\
476       (!s p. hom (VAR s) p = var s p) /\
477       (!t u p. hom (t @@ u) p = app (hom t) (hom u) t u p) /\
478       (!v t p. ~(v IN X UNION pFV p) ==>
479                (hom (LAM v t) p = lam (hom t) v t p))) /\
480      (!t p x y. ~(x IN X) /\ ~(y IN X) ==>
481                 (hom (swap x y t) p = rswap x y (hom t (pswap x y p)))) /\
482      (!t p. rFV (hom t p) SUBSET FV t UNION pFV p UNION X)``,
483  REPEAT STRIP_TAC THEN
484  STRIP_ASSUME_TAC lemma THEN
485  Q.EXISTS_TAC `hom` THEN ASM_SIMP_TAC bool_ss [] THEN
486  `!t p. rFV (hom t p) SUBSET FV t UNION pFV p UNION X`
487     by (HO_MATCH_MP_TAC nc_INDUCTION THEN ASM_SIMP_TAC (srw_ss()) [] THEN
488         REPEAT CONJ_TAC THENL [
489           PROVE_TAC [UNION_COMM],
490           ASM_SIMP_TAC (srw_ss()) [GSYM INSERT_SING_UNION, INSERT_UNION_EQ],
491           REPEAT STRIP_TAC THEN NEW_ELIM_TAC THEN
492           ASM_SIMP_TAC bool_ss [] THEN
493           Q.X_GEN_TAC `u` THEN REPEAT STRIP_TAC THENL [
494             `FV t DELETE x = FV (LAM x t)` by SRW_TAC [][] THEN
495             POP_ASSUM SUBST_ALL_TAC THEN
496             `LAM x t = LAM u (swap u x t)` by SRW_TAC [][swap_ALPHA] THEN
497             POP_ASSUM SUBST_ALL_TAC THEN
498             FIRST_ASSUM MATCH_MP_TAC THEN
499             `swap u x t = [VAR u/x] t` by SRW_TAC [][fresh_var_swap] THEN
500             ASM_SIMP_TAC bool_ss [],
501             SRW_TAC [][] THEN
502             `FV t DELETE u = FV (LAM u t)` by SRW_TAC [][] THEN
503             POP_ASSUM SUBST_ALL_TAC THEN
504             FIRST_ASSUM MATCH_MP_TAC THEN SRW_TAC [][] THEN
505             METIS_TAC [lemma14a]
506           ]
507         ]) THEN
508  ASM_SIMP_TAC bool_ss [] THEN
509  `(!x y p. pswap x y (pswap x y p) = p) /\ (!x p. pswap x x p = p) /\
510   (!x r. rswap x x r = r)`
511     by FULL_SIMP_TAC (srw_ss()) [swapping_def] THEN
512  `!t p x y. ~(x IN X) /\ ~(y IN X) ==>
513             (hom (swap x y t) p = rswap x y (hom t (pswap x y p)))`
514      by (HO_MATCH_MP_TAC pvh_induction THEN REPEAT CONJ_TAC THEN
515          TRY (SRW_TAC [][swap_thm] THEN NO_TAC) THENL [
516            MAP_EVERY Q.X_GEN_TAC [`t`,`u`] THEN
517            SRW_TAC [][swap_thm] THEN
518            `(hom (swap x y t) = swapfn pswap rswap x y (hom t)) /\
519             (hom (swap x y u) = swapfn pswap rswap x y (hom u))`
520               by SRW_TAC [][FUN_EQ_THM, swapfn_def] THEN
521            SRW_TAC [][],
522            REPEAT STRIP_TAC THEN
523            Cases_on `x = y` THEN1 SRW_TAC [][] THEN
524            Q_TAC (NEW_TAC "z") `{x;y;v} UNION FV t UNION X UNION pFV p` THEN
525            `LAM v t = LAM z ([VAR z/v] t)` by SRW_TAC [][SIMPLE_ALPHA] THEN
526            Q.ABBREV_TAC `M = [VAR z/v] t` THEN
527            `size t = size M` by SRW_TAC [][Abbr`M`] THEN
528            RM_ABBREV_TAC "M" THEN
529            POP_ASSUM SUBST_ALL_TAC THEN
530            POP_ASSUM SUBST_ALL_TAC THEN
531            `hom (swap x y (LAM z M)) p =
532               rswap x y (lam (hom M) z M (pswap x y p))`
533               by (SRW_TAC [][swap_thm] THEN
534                   NEW_ELIM_TAC THEN ASM_SIMP_TAC bool_ss [] THEN
535                   Q.X_GEN_TAC `a` THEN
536                   REVERSE (SRW_TAC [][]) THEN1
537                           (SRW_TAC [][] THEN
538                            REPEAT (AP_TERM_TAC ORELSE AP_THM_TAC) THEN
539                            SRW_TAC [][FUN_EQ_THM, swapfn_def]) THEN
540                   `hom (swap a z (swap x y M)) =
541                      swapfn pswap rswap a z (hom (swap x y M))`
542                        by SRW_TAC [][swapfn_def, FUN_EQ_THM] THEN
543                   `pswap a z p = p`
544                      by PROVE_TAC [swapping_implies_identity_swap] THEN
545                   `lam (hom (swap a z (swap x y M))) a
546                        (swap a z (swap x y M)) p =
547                      rswap a z
548                          (lam (hom (swap x y M)) z (swap x y M) p)`
549                      by SRW_TAC [][] THEN
550                   POP_ASSUM SUBST_ALL_TAC THEN
551                   `swapfn pswap rswap x y (hom M) = hom (swap x y M)`
552                       by SRW_TAC [][FUN_EQ_THM, swapfn_def] THEN
553                   POP_ASSUM SUBST_ALL_TAC THEN
554                   MATCH_MP_TAC swapping_implies_identity_swap THEN
555                   Q.EXISTS_TAC `rFV` THEN ASM_REWRITE_TAC [] THEN
556                   `rFV (lam (hom (swap x y M)) z (swap x y M) p)
557                        SUBSET
558                    FV (LAM z (swap x y M)) UNION pFV p UNION X`
559                       by SRW_TAC [][] THEN
560                   POP_ASSUM MP_TAC THEN SIMP_TAC (srw_ss()) [SUBSET_DEF] THEN
561                   METIS_TAC []) THEN
562            POP_ASSUM SUBST_ALL_TAC THEN REPEAT AP_TERM_TAC THEN
563            ASM_SIMP_TAC bool_ss [] THEN
564            NEW_ELIM_TAC THEN ASM_REWRITE_TAC [] THEN
565            Q.X_GEN_TAC `a` THEN
566            REVERSE (SRW_TAC [][]) THEN1 REWRITE_TAC [swap_id] THEN
567            `~(z IN pFV (pswap x y p))`
568               by FULL_SIMP_TAC (srw_ss()) [swapping_def] THEN
569            `pswap a z (pswap x y p) = pswap x y p`
570               by (MATCH_MP_TAC swapping_implies_identity_swap THEN
571                   Q.EXISTS_TAC `pFV` THEN ASM_REWRITE_TAC []) THEN
572            MATCH_MP_TAC EQ_TRANS THEN
573            Q.EXISTS_TAC `rswap a z (lam (hom M) z M (pswap x y p))` THEN
574            CONJ_TAC THENL [
575              ONCE_REWRITE_TAC [EQ_SYM_EQ] THEN
576              MATCH_MP_TAC swapping_implies_identity_swap THEN
577              Q.EXISTS_TAC `rFV` THEN ASM_REWRITE_TAC [] THEN
578              `rFV (lam (hom M) z M (pswap x y p)) SUBSET
579               FV (LAM z M) UNION pFV (pswap x y p) UNION X`
580                  by SRW_TAC [][] THEN
581              POP_ASSUM MP_TAC THEN SIMP_TAC (srw_ss()) [SUBSET_DEF] THEN
582              PROVE_TAC [],
583              SRW_TAC [][] THEN REPEAT (AP_TERM_TAC ORELSE AP_THM_TAC) THEN
584              SRW_TAC [][FUN_EQ_THM, swapfn_def]
585            ]
586          ]) THEN
587  ASM_SIMP_TAC bool_ss [] THEN SRW_TAC [][] THEN
588  NEW_ELIM_TAC THEN ASM_SIMP_TAC bool_ss [] THEN
589  Q.X_GEN_TAC `u` THEN STRIP_TAC THENL [
590    `hom (swap u v t) = swapfn pswap rswap u v (hom t)`
591       by SRW_TAC [][FUN_EQ_THM, swapfn_def] THEN
592    `pswap u v p = p` by PROVE_TAC [swapping_implies_identity_swap] THEN
593    `lam (hom (swap u v t)) u (swap u v t) p = rswap u v (lam (hom t) v t p)`
594       by SRW_TAC [][] THEN
595    POP_ASSUM SUBST_ALL_TAC THEN
596    MATCH_MP_TAC swapping_implies_identity_swap THEN
597    Q.EXISTS_TAC `rFV` THEN
598    ASM_REWRITE_TAC [] THEN
599    `rFV (lam (hom t) v t p) SUBSET FV (LAM v t) UNION pFV p UNION X`
600       by SRW_TAC [][] THEN
601    POP_ASSUM MP_TAC THEN REWRITE_TAC [SUBSET_DEF] THEN SRW_TAC [][] THEN
602    METIS_TAC [],
603    SRW_TAC [][]
604  ]);
605
606val one_eta = prove(
607  ``(\u. f ()) = f``,
608  SRW_TAC [][FUN_EQ_THM] THEN Cases_on `u` THEN SRW_TAC [][]);
609val exists_fn_dom_one = prove(
610  ``(?f: 'a -> one -> 'b. P f) = (?f: 'a -> 'b. P (\x u. f x))``,
611  EQ_TAC THEN STRIP_TAC THENL [
612    Q.EXISTS_TAC `\a. f a ()` THEN BETA_TAC THEN REWRITE_TAC [one_eta] THEN
613    SRW_TAC [ETA_ss][],
614    METIS_TAC []
615  ]);
616
617val forall_fn_dom_one = prove(
618  ``(!f : one -> 'b. P f) = (!f: 'b. P (K f))``,
619  SRW_TAC [][EQ_IMP_THM] THEN
620  `f = K (f ())` by SRW_TAC [][combinTheory.K_DEF, one_eta] THEN
621  POP_ASSUM SUBST_ALL_TAC THEN ASM_REWRITE_TAC []);
622val forall_one_one = prove(
623  ``(!p:one. P p) = P ()``,
624  SRW_TAC [][EQ_IMP_THM] THEN Cases_on `p` THEN SRW_TAC [][]);
625
626
627val swap_RECURSION_generic = save_thm(
628  "swap_RECURSION_generic",
629  (SIMP_RULE (srw_ss()) [null_swapping, exists_fn_dom_one, swapfn_def,
630                         forall_fn_dom_one, forall_one_one] o
631   Q.INST [`var'` |-> `var`, `con'` |-> `con`, `app'` |-> `app`,
632           `lam'` |-> `lam`] o
633   Q.INST [`pFV` |-> `K {}`,
634           `pswap` |-> `\x y u. u`,
635           `var` |-> `\s p. var' s`,
636           `con` |-> `\k p. con' k`,
637           `app` |-> `\rt ru t u p. app' (rt()) (ru()) t u`,
638           `lam` |-> `\rt v t p. lam' (rt()) v t`] o
639   INST_TYPE [beta |-> ``:one``, gamma |-> beta])
640  swap_RECURSION_pgeneric);
641
642val ex = (UNDISCH o
643          SIMP_RULE (srw_ss()) [] o
644          Q.INST [`X` |-> `{}`]) swap_RECURSION_generic
645val bod = #2 (dest_exists (concl ex))
646val (eqns, swfv) = CONJ_PAIR (ASSUME bod)
647val bodth' = CONJ eqns (CONJUNCT1 swfv)
648val hom_t = ``hom:'a nc -> 'b``
649
650val better = (DISCH_ALL o
651              CHOOSE (hom_t, ex) o
652              EXISTS (mk_exists(hom_t, concl bodth'), hom_t)) bodth'
653val swap_RECURSION_nosideset = save_thm("swap_RECURSION_nosideset", better)
654
655val swap_RECURSION_simple = save_thm(
656  "swap_RECURSION_simple",
657  (SIMP_RULE (srw_ss()) [null_swapping] o
658   Q.INST [`rswap` |-> `\x y z. z`, `rFV` |-> `K {}`])
659    swap_RECURSION_nosideset);
660
661(* ----------------------------------------------------------------------
662    list swap
663   ---------------------------------------------------------------------- *)
664
665val lswap_def = Define`
666  (lswap [] t = t) /\
667  (lswap (h::hs) t = swap (FST h) (SND h) (lswap hs t))
668`;
669
670val lswap_thm = store_thm(
671  "lswap_thm",
672  ``(lswap p (VAR s) = VAR (raw_lswapstr p s)) /\
673    (lswap p (CON k) = CON k) /\
674    (lswap p (M @@ N) = lswap p M @@ lswap p N) /\
675    (lswap p (LAM v M) = LAM (raw_lswapstr p v) (lswap p M))``,
676  Induct_on `p` THEN SRW_TAC [][lswap_def, raw_lswapstr_def, swap_thm]);
677val _ = export_rewrites ["lswap_thm"]
678
679val lswap_inverse = store_thm(
680  "lswap_inverse",
681  ``!t. (lswap (REVERSE p) (lswap p t) = t) /\
682        (lswap p (lswap (REVERSE p) t) = t)``,
683  HO_MATCH_MP_TAC simple_induction THEN SRW_TAC [][])
684val _ = export_rewrites ["lswap_inverse"]
685
686val lswap_NIL = store_thm(
687  "lswap_NIL",
688  ``lswap [] t = t``,
689  SRW_TAC [][lswap_def]);
690val _ = export_rewrites ["lswap_NIL"]
691
692val _ = export_theory();
693