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