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