1open HolKernel Parse boolLib bossLib binderLib 2open nomsetTheory 3 4local open stringTheory in end 5 6fun Store_thm (n,t,tac) = store_thm(n,t,tac) before export_rewrites [n] 7 8val _ = new_theory "MPlambda" 9 10val _ = Hol_datatype `MPterm = Var of string 11 | Parameter of string 12 | App of MPterm => MPterm 13 | Abs of string => MPterm`; 14 15val psub_def = Define` 16 (psub a p (Var s) = Var s) /\ 17 (psub a p (Parameter q) = if p = q then a else Parameter q) /\ 18 (psub a p (App t1 t2) = App (psub a p t1) (psub a p t2)) /\ 19 (psub a p (Abs v t) = Abs v (psub a p t)) 20`; 21val _ = export_rewrites ["psub_def"] 22 23val params_def = Define` 24 (params (Var s) = {}) /\ 25 (params (Parameter p) = {p}) /\ 26 (params (App t1 t2) = params t1 UNION params t2) /\ 27 (params (Abs v t) = params t) 28`; 29val _ = export_rewrites ["params_def"] 30 31val vsub_def = Define` 32 (vsub a v (Var u) = if u = v then a else Var u) /\ 33 (vsub a v (Parameter p) = Parameter p) /\ 34 (vsub a v (App t1 t2) = App (vsub a v t1) (vsub a v t2)) /\ 35 (vsub a v (Abs u t) = if u = v then Abs u t 36 else Abs u (vsub a v t)) 37`; 38val _ = export_rewrites ["vsub_def"] 39 40val allvars_def = Define` 41 (allvars (Parameter p) = {}) /\ 42 (allvars (Var v) = {v}) /\ 43 (allvars (App t1 t2) = allvars t1 UNION allvars t2) /\ 44 (allvars (Abs v t) = v INSERT allvars t) 45`; 46val _= export_rewrites ["allvars_def"] 47 48val FINITE_allvars = Store_thm( 49 "FINITE_allvars", 50 ``!t. FINITE (allvars t)``, 51 Induct THEN SRW_TAC [][]); 52 53val vsub_14a = Store_thm( 54 "vsub_14a", 55 ``~(v IN allvars t) ==> (vsub N v t = t)``, 56 Induct_on `t` THEN SRW_TAC [][]); 57 58val pvsub_vsub_collapse = store_thm( 59 "pvsub_vsub_collapse", 60 ``!M p v1 v2. ~(v2 IN allvars M) ==> 61 (vsub (Parameter p) v2 (vsub (Var v2) v1 M) = 62 vsub (Parameter p) v1 M)``, 63 Induct THEN SRW_TAC [][]); 64 65val params_vvsub = Store_thm( 66 "params_vvsub", 67 ``params (vsub (Var v1) v2 M) = params M``, 68 Induct_on `M` THEN SRW_TAC [][]); 69 70val shape_lemma = store_thm( 71 "shape_lemma", 72 ``!M p. ?v M'. (M = vsub (Parameter p) v M') /\ ~(p IN params M')``, 73 Induct THEN ASM_SIMP_TAC (srw_ss()) []THENL [ 74 Q.X_GEN_TAC `s` THEN SRW_TAC [][] THEN 75 Q_TAC (NEW_TAC "z") `{s}` THEN 76 MAP_EVERY Q.EXISTS_TAC [`z`, `Var s`] THEN SRW_TAC [][], 77 78 Q.X_GEN_TAC `s` THEN SRW_TAC [][] THEN 79 Cases_on `s = p` THENL [ 80 MAP_EVERY Q.EXISTS_TAC [`x`, `Var x`] THEN SRW_TAC [][], 81 MAP_EVERY Q.EXISTS_TAC [`x`, `Parameter s`] THEN SRW_TAC [][] 82 ], 83 84 GEN_TAC THEN 85 `?v1 M1. (M = vsub (Parameter p) v1 M1) /\ ~(p IN params M1)` 86 by METIS_TAC [] THEN 87 `?v2 M2. (M' = vsub (Parameter p) v2 M2) /\ ~(p IN params M2)` 88 by METIS_TAC [] THEN 89 Q_TAC (NEW_TAC "z") `allvars M1 UNION allvars M2 UNION {v1;v2}` THEN 90 `(M = vsub (Parameter p) z (vsub (Var z) v1 M1)) /\ 91 (M' = vsub (Parameter p) z (vsub (Var z) v2 M2))` 92 by METIS_TAC [pvsub_vsub_collapse] THEN 93 MAP_EVERY Q.EXISTS_TAC 94 [`z`, `App (vsub (Var z) v1 M1) (vsub (Var z) v2 M2)`] THEN 95 SRW_TAC [][pvsub_vsub_collapse], 96 97 Q.X_GEN_TAC `s` THEN SRW_TAC [][] THEN 98 FIRST_X_ASSUM (Q.SPEC_THEN `p` STRIP_ASSUME_TAC) THEN 99 REVERSE (Cases_on `s = v`) THEN1 100 (MAP_EVERY Q.EXISTS_TAC [`v`, `Abs s M'`] THEN SRW_TAC [][]) THEN 101 SRW_TAC [][] THEN 102 Q_TAC (NEW_TAC "z") `s INSERT allvars M'` THEN 103 MAP_EVERY Q.EXISTS_TAC [`z`, `Abs s (vsub (Var z) s M')`] THEN 104 SRW_TAC [][pvsub_vsub_collapse] 105 ]); 106 107val (vclosed_rules, vclosed_ind, vclosed_cases) = Hol_reln` 108 (!p. vclosed (Parameter p)) /\ 109 (!p v t. vclosed (vsub (Parameter p) v t) ==> 110 vclosed (Abs v t)) /\ 111 (!t1 t2. vclosed t1 /\ vclosed t2 ==> vclosed (App t1 t2)) 112`; 113 114val FINITE_params = Store_thm( 115 "FINITE_params", 116 ``!t. FINITE (params t)``, 117 Induct THEN SRW_TAC [][]); 118 119val psub_14a = Store_thm( 120 "psub_14a", 121 ``!M p N. ~(p IN params M) ==> (psub N p M = M)``, 122 Induct THEN SRW_TAC [][]); 123 124 125val vsub_is_psub_alpha = store_thm( 126 "vsub_is_psub_alpha", 127 ``!M p N v. ~(p IN params M) ==> 128 (psub N p (vsub (Parameter p) v M) = vsub N v M)``, 129 Induct THEN SRW_TAC [][]); 130 131val vars_def = Define` 132 (vars (Var u) = {u}) /\ 133 (vars (Parameter p) = {}) /\ 134 (vars (App t1 t2) = vars t1 UNION vars t2) /\ 135 (vars (Abs v t) = vars t DIFF {v}) 136`; 137val _ = export_rewrites ["vars_def"] 138 139val vsub_14a = Store_thm( 140 "vsub_14a", 141 ``!M v N. ~(v IN vars M) ==> (vsub N v M = M)``, 142 Induct THEN SRW_TAC [][]); 143 144 145val raw_MPpm_def = Define` 146 (raw_MPpm pi (Parameter s) = Parameter (lswapstr pi s)) /\ 147 (raw_MPpm pi (Var v) = Var v) /\ 148 (raw_MPpm pi (App t1 t2) = App (raw_MPpm pi t1) (raw_MPpm pi t2)) /\ 149 (raw_MPpm pi (Abs v t) = Abs v (raw_MPpm pi t)) 150`; 151val _ = export_rewrites ["raw_MPpm_def"] 152 153val _ = overload_on("MP_pmact",``mk_pmact raw_MPpm``); 154val _ = overload_on("MPpm", ``pmact MP_pmact``); 155 156val MPpm_raw = store_thm( 157 "MPpm_raw", 158 ``MPpm = raw_MPpm``, 159 SRW_TAC [][GSYM pmact_bijections] THEN 160 SRW_TAC [][is_pmact_def] THENL [ 161 Induct_on `x` THEN SRW_TAC [][], 162 Induct_on `x` THEN SRW_TAC [][pmact_decompose], 163 FULL_SIMP_TAC (srw_ss()) [permeq_thm, FUN_EQ_THM] THEN 164 Induct THEN SRW_TAC [][] 165 ]); 166 167val MPpm_thm = save_thm( 168"MPpm_thm", 169raw_MPpm_def |> SUBS [GSYM MPpm_raw]); 170val _ = export_rewrites["MPpm_thm"]; 171 172val MPpm_fresh = Store_thm( 173 "MPpm_fresh", 174 ``!M x y. ~(x IN params M) /\ ~(y IN params M) ==> 175 (MPpm [(x,y)] M = M)``, 176 Induct THEN SRW_TAC [][]); 177 178val MPpm_NIL = Store_thm( 179 "MPpm_NIL", 180 ``MPpm [] t = t``, 181 Induct_on `t` THEN SRW_TAC [][]); 182 183val supp_MPpm = Store_thm( 184 "supp_MPpm", 185 ``supp MP_pmact = params``, 186 ONCE_REWRITE_TAC [FUN_EQ_THM] THEN GEN_TAC THEN 187 MATCH_MP_TAC supp_unique_apart THEN SRW_TAC [][support_def] THEN 188 Induct_on `x` THEN SRW_TAC [][] THEN METIS_TAC []); 189 190val MPpm_vsub = store_thm( 191 "MPpm_vsub", 192 ``!M v pi N. MPpm pi (vsub M v N) = vsub (MPpm pi M) v (MPpm pi N)``, 193 Induct_on `N` THEN SRW_TAC [][]); 194 195val vclosed_MPpm = store_thm( 196 "vclosed_MPpm", 197 ``!M. vclosed M ==> !pi. vclosed (MPpm pi M)``, 198 HO_MATCH_MP_TAC vclosed_ind THEN SRW_TAC [][vclosed_rules, MPpm_vsub] THEN 199 METIS_TAC [vclosed_rules]); 200 201val vars_pvsub = store_thm( 202 "vars_pvsub", 203 ``!p v M. vars (vsub (Parameter p) v M) = vars M DELETE v``, 204 Induct_on `M` THEN SRW_TAC [][] THEN 205 SRW_TAC [][pred_setTheory.EXTENSION] THEN METIS_TAC []); 206 207 208val vclosed_empty_vars = store_thm( 209 "vclosed_empty_vars", 210 ``!t. vclosed t ==> (vars t = {})``, 211 HO_MATCH_MP_TAC vclosed_ind THEN SRW_TAC [][vars_pvsub] THEN 212 FULL_SIMP_TAC (srw_ss()) [pred_setTheory.EXTENSION]); 213 214 215val vclosed_var = Store_thm( 216 "vclosed_var", 217 ``!v. ~(vclosed (Var v))``, 218 ONCE_REWRITE_TAC [vclosed_cases] THEN SRW_TAC [][]); 219 220val vclosed_parameter = Store_thm( 221 "vclosed_parameter", 222 ``vclosed (Parameter p)``, 223 ONCE_REWRITE_TAC [vclosed_cases] THEN SRW_TAC [][]); 224 225val _ = set_fixity "=" (Infix(NONASSOC, 100)) 226 227val vclosed_app = Store_thm( 228 "vclosed_app", 229 ``vclosed (App t1 t2) = vclosed t1 /\ vclosed t2``, 230 CONV_TAC (LAND_CONV (ONCE_REWRITE_CONV [vclosed_cases])) THEN 231 SRW_TAC [][]); 232 233val vclosed_abs = store_thm( 234 "vclosed_abs", 235 ``vclosed (Abs v t) = ?p. vclosed (vsub (Parameter p) v t)``, 236 CONV_TAC (LAND_CONV (ONCE_REWRITE_CONV [vclosed_cases])) THEN 237 SRW_TAC [][]); 238 239val pvsub_eq_app = prove( 240 ``(vsub (Parameter p) v M = App t1 t2) = 241 ?M1 M2. (M = App M1 M2) /\ (vsub (Parameter p) v M1 = t1) /\ 242 (vsub (Parameter p) v M2 = t2)``, 243 Cases_on `M` THEN SRW_TAC [][]); 244 245val pvsub_eq_param = prove( 246 ``(vsub (Parameter p1) v M = Parameter p2) = 247 (M = Var v) /\ (p1 = p2) \/ 248 (M = Parameter p2)``, 249 Cases_on `M` THEN SRW_TAC [][]); 250 251val pvsub_eq_abs = prove( 252 ``(vsub (Parameter p) v M = Abs s t) = 253 (?M0. ~(s = v) /\ (M = Abs s M0) /\ (vsub (Parameter p) v M0 = t)) \/ 254 (v = s) /\ (M = Abs s t)``, 255 Cases_on `M` THEN SRW_TAC [][] THEN METIS_TAC []); 256 257val independent_pvsub = prove( 258 ``!p1 p2 v1 v2 M. 259 ~(v1 = v2) ==> (vsub (Parameter p1) v1 (vsub (Parameter p2) v2 M) = 260 vsub (Parameter p2) v2 (vsub (Parameter p1) v1 M))``, 261 Induct_on `M` THEN SRW_TAC [][]) 262 263val IN_params_MPpm = store_thm( 264 "IN_params_MPpm", 265 ``x IN params (MPpm pi M) = lswapstr (REVERSE pi) x IN params M``, 266 Induct_on `M` THEN SRW_TAC [][pmact_eql]); 267 268val independent_psub_vsub = prove( 269 ``!M v p1 p2 p3. 270 ~(p2 = p3) ==> 271 (psub (Parameter p1) p2 (vsub (Parameter p3) v M) = 272 vsub (Parameter p3) v (psub (Parameter p1) p2 M))``, 273 Induct THEN SRW_TAC [][]); 274 275val (cvclosed_rules, cvclosed_ind, cvclosed_cases) = Hol_reln` 276 (!p. cvclosed (Parameter p)) /\ 277 (!M N. cvclosed M /\ cvclosed N ==> cvclosed (App M N)) /\ 278 (!v p M. ~(p IN params M) /\ cvclosed (vsub (Parameter p) v M) ==> 279 cvclosed (Abs v M)) 280`; 281 282val cvclosed_eqns = prove( 283 ``cvclosed (Parameter p) /\ 284 (cvclosed (App M N) = cvclosed M /\ cvclosed N) /\ 285 (cvclosed (Abs v M) = ?p. ~(p IN params M) /\ 286 cvclosed (vsub (Parameter p) v M))``, 287 REPEAT CONJ_TAC THEN1 288 (ONCE_REWRITE_TAC [cvclosed_cases] THEN SRW_TAC [][]) THEN 289 CONV_TAC (LAND_CONV (ONCE_REWRITE_CONV [cvclosed_cases])) THEN 290 SRW_TAC [][]); 291 292val cvclosed_strongctxt_ind = prove( 293 ``!P f. (!x. FINITE (f x)) /\ 294 (!p x. P (Parameter p) x) /\ 295 (!M N y. (!x. P M x) /\ (!x. P N x) ==> P (App M N) y) /\ 296 (!v p M y. ~(p IN f y) /\ ~(p IN params M) /\ 297 (!x. P (vsub (Parameter p) v M) x) ==> 298 P (Abs v M) y) 299 ==> 300 !M. cvclosed M ==> !x. P M x``, 301 REPEAT GEN_TAC THEN STRIP_TAC THEN 302 Q_TAC SUFF_TAC `!M. cvclosed M ==> !pi x. P (MPpm pi M) x` 303 THEN1 METIS_TAC [MPpm_NIL] THEN 304 HO_MATCH_MP_TAC cvclosed_ind THEN 305 SRW_TAC [][] THEN 306 FIRST_X_ASSUM MATCH_MP_TAC THEN 307 FULL_SIMP_TAC (srw_ss()) [MPpm_vsub] THEN 308 Q_TAC (NEW_TAC "z") `f x UNION params (MPpm pi M)` THEN 309 Q.EXISTS_TAC `z` THEN SRW_TAC [][] THEN 310 FIRST_X_ASSUM (Q.SPECL_THEN [`(stringpm pi p, z) :: pi`, `x'`] MP_TAC) THEN 311 ASM_SIMP_TAC (srw_ss()) [] THEN 312 `MPpm [(stringpm pi p, z)] (MPpm pi M) = MPpm pi M` 313 by SRW_TAC [][MPpm_fresh, IN_params_MPpm, stringpm_raw] THEN 314 FULL_SIMP_TAC (srw_ss()) [GSYM pmact_decompose]); 315 316val cvclosed_strong_ind = 317(Q.GEN `P` o Q.GEN `X` o 318 SIMP_RULE (srw_ss()) [] o 319 Q.SPECL [`\t u. P t`, `\u. X`] o 320 INST_TYPE [alpha |-> ``:one``]) cvclosed_strongctxt_ind 321 322val notin_pvsub_I = prove( 323 ``~(p1 = p2) /\ ~(p1 IN params M) ==> 324 ~(p1 IN params (vsub (Parameter p2) v M))``, 325 Induct_on `M` THEN SRW_TAC [][]); 326 327val cvclosed_p_indep = prove( 328 ``!t. cvclosed t ==> 329 !pp't0 v p p' t0. 330 ((p, p', t0) = pp't0) /\ (t = vsub (Parameter p) v t0) ==> 331 cvclosed (vsub (Parameter p') v t0)``, 332 HO_MATCH_MP_TAC cvclosed_strongctxt_ind THEN 333 Q.EXISTS_TAC `\(p,p',t0). {p;p'} UNION params t0` THEN 334 SIMP_TAC (srw_ss()) [pairTheory.FORALL_PROD] THEN 335 SRW_TAC [][cvclosed_eqns, pvsub_eq_abs, pvsub_eq_param, pvsub_eq_app] THEN 336 SRW_TAC [][cvclosed_eqns] THENL [ 337 METIS_TAC [], 338 METIS_TAC [], 339 FULL_SIMP_TAC (srw_ss()) [] THEN 340 Q.EXISTS_TAC `p` THEN CONJ_TAC THENL [ 341 MATCH_MP_TAC notin_pvsub_I THEN SRW_TAC [][], 342 METIS_TAC [independent_pvsub] 343 ], 344 METIS_TAC [] 345 ]); 346 347val cvclosed_pickany = save_thm( 348 "cvclosed_pickany", 349 SIMP_RULE (srw_ss() ++ boolSimps.DNF_ss) [] cvclosed_p_indep); 350 351val cvclosed_vclosed = prove( 352 ``!t. cvclosed t ==> vclosed t``, 353 HO_MATCH_MP_TAC cvclosed_ind THEN SRW_TAC [][vclosed_rules] THEN 354 METIS_TAC [vclosed_rules]); 355 356val vclosed_cvclosed = prove( 357 ``!t. vclosed t ==> cvclosed t``, 358 HO_MATCH_MP_TAC vclosed_ind THEN SRW_TAC [][cvclosed_rules] THEN 359 MATCH_MP_TAC (last (CONJUNCTS cvclosed_rules)) THEN 360 Q_TAC (NEW_TAC "z") `params t` THEN 361 METIS_TAC [cvclosed_pickany]); 362 363val cv_eq_vclosed = store_thm( 364 "cv_eq_vclosed", 365 ``cvclosed = vclosed``, 366 SRW_TAC [] [FUN_EQ_THM, vclosed_cvclosed, cvclosed_vclosed, EQ_IMP_THM]); 367 368val vclosed_strong_ind = save_thm( 369 "vclosed_strong_ind", 370 REWRITE_RULE [cv_eq_vclosed] cvclosed_strong_ind) 371 372val double_pvsub = Store_thm( 373 "double_pvsub", 374 ``vsub (Parameter p1) v (vsub (Parameter p2) v t) = 375 vsub (Parameter p2) v t``, 376 Induct_on `t` THEN SRW_TAC [][]); 377 378val vclosed_pvsub = store_thm( 379 "vclosed_pvsub", 380 ``!t. vclosed t ==> !p v. vclosed (vsub (Parameter p) v t)``, 381 HO_MATCH_MP_TAC vclosed_ind THEN SRW_TAC [][vclosed_rules] THEN 382 METIS_TAC [vclosed_rules, double_pvsub, independent_pvsub]); 383 384val cofin_vclosed_ind = store_thm( 385 "cofin_vclosed_ind", 386 ``!P. (!p. P (Parameter p)) /\ 387 (!v t X. FINITE X /\ 388 (!p. ~(p IN X) ==> P (vsub (Parameter p) v t)) ==> 389 P (Abs v t)) /\ 390 (!t1 t2. P t1 /\ P t2 ==> P (App t1 t2)) ==> 391 !t. vclosed t ==> P t``, 392 GEN_TAC THEN STRIP_TAC THEN 393 Q_TAC SUFF_TAC `!t. vclosed t ==> !pi. P (MPpm pi t)` 394 THEN1 METIS_TAC [MPpm_NIL] THEN 395 HO_MATCH_MP_TAC vclosed_strong_ind THEN 396 Q.EXISTS_TAC `{}` THEN SRW_TAC [][] THEN 397 FIRST_X_ASSUM MATCH_MP_TAC THEN 398 Q.EXISTS_TAC `params (MPpm pi t)` THEN 399 FULL_SIMP_TAC (srw_ss()) [MPpm_vsub] THEN 400 Q.X_GEN_TAC `p1` THEN STRIP_TAC THEN 401 FIRST_X_ASSUM (Q.SPEC_THEN `[(p1,stringpm pi p)] ++ pi` MP_TAC) THEN 402 ASM_SIMP_TAC (srw_ss()) [] THEN 403 Q_TAC SUFF_TAC `MPpm ((p1,stringpm pi p)::pi) t = MPpm pi t` 404 THEN1 SRW_TAC [][] THEN 405 `MPpm [(p1,stringpm pi p)] (MPpm pi t) = MPpm pi t` 406 by SRW_TAC [][MPpm_fresh, IN_params_MPpm, stringpm_raw] THEN 407 FULL_SIMP_TAC (srw_ss()) [GSYM pmact_decompose]); 408 409val (avclosed_rules, avclosed_ind, avclosed_cases) = Hol_reln` 410 (!p. avclosed (Parameter p)) /\ 411 (!t1 t2. avclosed t1 /\ avclosed t2 ==> avclosed (App t1 t2)) /\ 412 (!v t. (!p. avclosed (vsub (Parameter p) v t)) ==> 413 avclosed (Abs v t)) 414`; 415 416val avclosed_pickany = prove( 417 ``!t. avclosed t ==> 418 !v p p' t0. (t = vsub (Parameter p) v t0) ==> 419 avclosed (vsub (Parameter p') v t0)``, 420 HO_MATCH_MP_TAC avclosed_ind THEN 421 SRW_TAC [][pvsub_eq_app, pvsub_eq_param, pvsub_eq_abs] THEN 422 SRW_TAC [][avclosed_rules] THENL [ 423 METIS_TAC [avclosed_rules], 424 MATCH_MP_TAC (last (CONJUNCTS avclosed_rules)) THEN 425 METIS_TAC [independent_pvsub], 426 MATCH_MP_TAC (last (CONJUNCTS avclosed_rules)) THEN 427 METIS_TAC [] 428 ]); 429 430(* page 12 *) 431val avclosed_alpha = store_thm( 432 "avclosed_alpha", 433 ``avclosed (vsub (Parameter p) v t) ==> 434 !q. avclosed (vsub (Parameter q) v t)``, 435 METIS_TAC [avclosed_pickany]); 436 437val vclosed_avclosed = store_thm( 438 "vclosed_avclosed", 439 ``!t. vclosed t ==> avclosed t``, 440 HO_MATCH_MP_TAC vclosed_strong_ind THEN 441 SRW_TAC [][avclosed_rules] THEN 442 Q.EXISTS_TAC `{}` THEN SRW_TAC [][] THEN 443 MATCH_MP_TAC (last (CONJUNCTS avclosed_rules)) THEN SRW_TAC [][] THEN 444 METIS_TAC [avclosed_pickany]); 445 446val avclosed_vclosed = prove( 447 ``!t. avclosed t ==> vclosed t``, 448 HO_MATCH_MP_TAC avclosed_ind THEN SRW_TAC [][vclosed_abs]); 449 450val avclosed_eq_vclosed = prove( 451 ``avclosed = vclosed``, 452 SRW_TAC [][FUN_EQ_THM, EQ_IMP_THM, vclosed_avclosed, avclosed_vclosed]); 453 454val vclosed_avclosed_ind = save_thm( 455 "vclosed_avclosed_ind", 456 REWRITE_RULE [avclosed_eq_vclosed] avclosed_ind); 457 458val sub = ``\t (p,v). vsub (Parameter p) v t`` 459val FOLDL_Parameter = prove( 460 ``!l. FOLDL ^sub (Parameter p) l = Parameter p``, 461 Induct THEN ASM_SIMP_TAC (srw_ss()) [pairTheory.FORALL_PROD]); 462val FOLDL_Var = prove( 463 ``!l. (?p. FOLDL ^sub (Var s) l = Parameter p) \/ 464 (FOLDL ^sub (Var s) l = Var s)``, 465 Induct THEN ASM_SIMP_TAC (srw_ss()) [pairTheory.FORALL_PROD] THEN 466 FULL_SIMP_TAC (srw_ss()) [] THEN 467 SRW_TAC [][FOLDL_Parameter]); 468 469val FOLDL_App = prove( 470 ``!l t1 t2. FOLDL ^sub (App t1 t2) l = 471 App (FOLDL ^sub t1 l) (FOLDL ^sub t2 l)``, 472 Induct THEN ASM_SIMP_TAC (srw_ss()) [pairTheory.FORALL_PROD]); 473 474val FOLDL_Abs = prove( 475 ``!l v t. FOLDL ^sub (Abs v t) l = 476 Abs v (FOLDL ^sub t (FILTER (\ (p,u). ~(u = v)) l))``, 477 Induct THEN ASM_SIMP_TAC (srw_ss()) [pairTheory.FORALL_PROD] THEN 478 SRW_TAC [][]); 479 480val vsub_FOLDL = prove( 481 ``!l t p s. vsub (Parameter p) s (FOLDL ^sub t l) = 482 FOLDL ^sub t (l ++ [(p,s)])``, 483 Induct THEN ASM_SIMP_TAC (srw_ss()) [pairTheory.FORALL_PROD]); 484 485val vars_pvsub = prove( 486 ``vars (vsub (Parameter p) v t) = vars t DELETE v``, 487 SIMP_TAC (srw_ss()) [pred_setTheory.EXTENSION] THEN 488 Induct_on `t` THEN SRW_TAC [][] THEN 489 METIS_TAC []); 490 491 492val vars_FOLDL = prove( 493 ``!l t. vars (FOLDL ^sub t l) = vars t DIFF set (MAP SND l)``, 494 Induct THEN ASM_SIMP_TAC (srw_ss()) [pairTheory.FORALL_PROD, vars_pvsub] THEN 495 SRW_TAC [][pred_setTheory.EXTENSION] THEN METIS_TAC []); 496 497val empty_vars_vclosed = store_thm( 498 "empty_vars_vclosed", 499 ``!t. (vars t = {}) ==> vclosed t``, 500 Q_TAC SUFF_TAC 501 `!t l. (vars (FOLDL (\t (p,v). vsub (Parameter p) v t) t l) = {}) ==> 502 vclosed (FOLDL (\t (p,v). vsub (Parameter p) v t) t l)` 503 THEN1 METIS_TAC [listTheory.FOLDL] THEN 504 Induct THEN 505 ASM_SIMP_TAC (srw_ss()) [FOLDL_App, FOLDL_Parameter, FOLDL_Abs] THENL [ 506 MAP_EVERY Q.X_GEN_TAC [`s`,`l`] THEN 507 Q.SPEC_THEN `l` STRIP_ASSUME_TAC FOLDL_Var THEN 508 FULL_SIMP_TAC (srw_ss()) [], 509 SRW_TAC [][] THEN 510 MATCH_MP_TAC (List.nth(CONJUNCTS vclosed_rules, 1)) THEN 511 SRW_TAC [][vsub_FOLDL] THEN Q.EXISTS_TAC `p` THEN 512 FIRST_X_ASSUM MATCH_MP_TAC THEN 513 FULL_SIMP_TAC (srw_ss()) [vars_FOLDL, pred_setTheory.EXTENSION] THEN 514 METIS_TAC [] 515 ]); 516 517val (mpbeta_rules, mpbeta_ind, mpbeta_cases) = Hol_reln` 518 (!M N M'. mpbeta M M' ==> mpbeta (App M N) (App M' N)) /\ 519 (!M N N'. mpbeta N N' ==> mpbeta (App M N) (App M N')) /\ 520 (!u v M N p. ~(p IN params M) /\ ~(p IN params N) /\ 521 mpbeta (vsub (Parameter p) u M) (vsub (Parameter p) v N) ==> 522 mpbeta (Abs u M) (Abs v N)) /\ 523 (!x M N. vclosed (Abs x M) /\ vclosed N ==> 524 mpbeta (App (Abs x M) N) (vsub N x M)) 525`; 526 527open chap3Theory 528val (convert_rules, convert_ind, convert_cases) = Hol_reln` 529 (!p. convert (Parameter p) (VAR p)) /\ 530 (!t1 t2 M N. convert t1 M /\ convert t2 N ==> 531 convert (App t1 t2) (M @@ N)) /\ 532 (!u v t M. ~(u IN params t) /\ convert (vsub (Parameter u) v t) M ==> 533 convert (Abs v t) (LAM u M)) 534`; 535 536val convert_param = Store_thm( 537 "convert_param", 538 ``convert (Parameter p) t = (t = VAR p)``, 539 ONCE_REWRITE_TAC [convert_cases] THEN SRW_TAC [][]); 540 541val convert_app = store_thm( 542 "convert_app", 543 ``convert (App M N) t = ?t0 t1. convert M t0 /\ convert N t1 /\ 544 (t = t0 @@ t1)``, 545 CONV_TAC (LAND_CONV (ONCE_REWRITE_CONV [convert_cases])) THEN 546 SRW_TAC [][] THEN METIS_TAC []); 547 548val convert_abs = save_thm( 549 "convert_abs", 550 (SIMP_RULE (srw_ss()) [] o Q.SPEC `Abs v M`) convert_cases) 551 552val UNION_DELETE = prove( 553 ``(s UNION t) DELETE e = (s DELETE e) UNION (t DELETE e)``, 554 SRW_TAC [][pred_setTheory.EXTENSION] THEN METIS_TAC []); 555 556val params_vsub = store_thm( 557 "params_vsub", 558 ``!t p v. ~(p IN params t) ==> 559 (params (vsub (Parameter p) v t) DELETE p = params t)``, 560 Induct THEN SRW_TAC [][UNION_DELETE] THEN 561 SRW_TAC [][pred_setTheory.EXTENSION] THEN METIS_TAC []); 562 563val convert_MPpm = prove( 564 ``!t M. convert t M ==> !pi. convert (MPpm pi t) (tpm pi M)``, 565 HO_MATCH_MP_TAC convert_ind THEN 566 SRW_TAC [][convert_rules, MPpm_vsub] THEN 567 MATCH_MP_TAC (last (CONJUNCTS convert_rules)) THEN 568 SRW_TAC [][IN_params_MPpm]); 569 570val convert_MPpm_E = Store_thm( 571 "convert_MPpm_E", 572 ``convert (MPpm pi t) (tpm pi M) = convert t M``, 573 METIS_TAC [convert_MPpm, pmact_inverse]); 574 575val convert_strong_ind = store_thm( 576 "convert_strong_ind", 577 ``!P f. (!x. FINITE (f x)) /\ 578 (!p c. P (Parameter p) (VAR p) c) /\ 579 (!t1 t2 M N c. 580 (!d1. P t1 M d1) /\ convert t1 M /\ 581 (!d2. P t2 N d2) /\ convert t2 N ==> 582 P (App t1 t2) (M @@ N) c) /\ 583 (!u v t M c. ~(u IN params t) /\ ~(u IN f c) /\ 584 convert (vsub (Parameter u) v t) M /\ 585 (!d. P (vsub (Parameter u) v t) M d) ==> 586 P (Abs v t) (LAM u M) c) 587 ==> 588 !t M. convert t M ==> !c. P t M c``, 589 REPEAT GEN_TAC THEN STRIP_TAC THEN 590 Q_TAC SUFF_TAC `!t M. convert t M ==> 591 convert t M /\ 592 !c pi. P (MPpm pi t) (tpm pi M) c` 593 THEN1 METIS_TAC [pmact_nil] THEN 594 HO_MATCH_MP_TAC convert_ind THEN 595 SRW_TAC [][convert_rules, MPpm_vsub] THEN 596 Q_TAC (NEW_TAC "z") `FV (tpm pi M) UNION f c UNION params (MPpm pi t)` THEN 597 `LAM (lswapstr pi u) (tpm pi M) = LAM z (tpm [(z, lswapstr pi u)] (tpm pi M))` 598 by SRW_TAC [][termTheory.tpm_ALPHA] THEN 599 SRW_TAC [][] THEN 600 `MPpm ((z,lswapstr pi u)::pi) t = MPpm [(z,lswapstr pi u)] (MPpm pi t)` 601 by SRW_TAC [][GSYM pmact_decompose] THEN 602 ` _ = MPpm pi t` 603 by SRW_TAC [][MPpm_fresh, IN_params_MPpm] THEN 604 FIRST_X_ASSUM MATCH_MP_TAC THEN SRW_TAC [][] 605 THEN1 (`convert (MPpm ((z,lswapstr pi u)::pi) (vsub (Parameter u) v t)) 606 (tpm ((z,lswapstr pi u)::pi) M)` 607 by METIS_TAC [convert_MPpm_E] THEN 608 POP_ASSUM MP_TAC THEN 609 ASM_SIMP_TAC bool_ss [MPpm_vsub] THEN 610 SRW_TAC [][GSYM pmact_decompose]) THEN 611 FIRST_X_ASSUM (Q.SPECL_THEN [`d`, `((z,lswapstr pi u)::pi)`] MP_TAC) THEN 612 SRW_TAC [][GSYM pmact_decompose]); 613 614val convert_params = store_thm( 615 "convert_params", 616 ``!t M. convert t M ==> (params t = FV M)``, 617 HO_MATCH_MP_TAC convert_ind THEN 618 SRW_TAC [][] THEN METIS_TAC [params_vsub]); 619 620val vclosed_convert = store_thm( 621 "vclosed_convert", 622 ``!t. vclosed t ==> ?M. convert t M``, 623 HO_MATCH_MP_TAC vclosed_strong_ind THEN Q.EXISTS_TAC `{}` THEN 624 SRW_TAC [][] THEN METIS_TAC [convert_rules]); 625 626val convert_vclosed = store_thm( 627 "convert_vclosed", 628 ``!t M. convert t M ==> vclosed t``, 629 HO_MATCH_MP_TAC convert_ind THEN SRW_TAC [][vclosed_abs] THEN 630 METIS_TAC []); 631 632val convert_vsub = prove( 633 ``!t M. convert t M ==> 634 !t0p1p2 v p1 p2 t0. 635 (t0p1p2 = (t0,p1,p2)) /\ 636 (vsub (Parameter p1) v t0 = t) /\ 637 ~(p1 IN params t0) /\ ~(p2 IN params t0) ==> 638 convert (vsub (Parameter p2) v t0) (tpm [(p1,p2)] M)``, 639 HO_MATCH_MP_TAC convert_strong_ind THEN 640 Q.EXISTS_TAC `\ (t0,p1,p2). {p1;p2} UNION params t0` THEN 641 SIMP_TAC (srw_ss()) [pairTheory.FORALL_PROD] THEN 642 REPEAT CONJ_TAC THENL [ 643 (* parameter case *) 644 SRW_TAC [][pvsub_eq_param] THEN 645 FULL_SIMP_TAC (srw_ss()) [convert_rules], 646 647 (* App case *) 648 SRW_TAC [][pvsub_eq_app] THEN 649 FULL_SIMP_TAC (srw_ss()) [convert_rules], 650 651 (* Abs case *) 652 MAP_EVERY Q.X_GEN_TAC [`u`, `v`, `t`, `M`, `t0`, `p1`, `p2`] THEN 653 STRIP_TAC THEN Q.X_GEN_TAC `v'` THEN STRIP_TAC THEN 654 FULL_SIMP_TAC (srw_ss()) [pvsub_eq_abs] THENL [ 655 SRW_TAC [][] THEN FULL_SIMP_TAC (srw_ss()) [] THEN 656 MATCH_MP_TAC (last (CONJUNCTS convert_rules)) THEN 657 SRW_TAC [][notin_pvsub_I] THEN 658 METIS_TAC [independent_pvsub, notin_pvsub_I], 659 660 MATCH_MP_TAC (last (CONJUNCTS convert_rules)) THEN 661 SRW_TAC [][] THEN 662 FULL_SIMP_TAC (srw_ss()) [] THEN 663 `convert (MPpm [(p1,p2)] (vsub (Parameter u) v t)) 664 (tpm [(p1,p2)] M)` 665 by SRW_TAC [][] THEN 666 Q_TAC SUFF_TAC `MPpm [(p1,p2)] (vsub (Parameter u) v t) = 667 vsub (Parameter u) v t` 668 THEN1 METIS_TAC [] THEN 669 SRW_TAC [][MPpm_vsub] 670 ] 671 ]); 672 673val convert_vsub_thm = save_thm( 674 "convert_vsub_thm", 675 SIMP_RULE (srw_ss() ++ boolSimps.DNF_ss) [] convert_vsub) 676 677val convert_unique = store_thm( 678 "convert_unique", 679 ``!t M. convert t M ==> !N. convert t N ==> (M = N)``, 680 HO_MATCH_MP_TAC convert_ind THEN REPEAT CONJ_TAC THENL [ 681 ONCE_REWRITE_TAC [convert_cases] THEN SRW_TAC [][], 682 REPEAT GEN_TAC THEN STRIP_TAC THEN 683 ONCE_REWRITE_TAC [convert_cases] THEN SRW_TAC [][] THEN 684 SRW_TAC [][], 685 REPEAT GEN_TAC THEN STRIP_TAC THEN 686 ONCE_REWRITE_TAC [convert_cases] THEN SRW_TAC [][] THEN 687 SRW_TAC [][termTheory.LAM_eq_thm] THEN 688 Cases_on `u = u'` THEN1 METIS_TAC [] THEN 689 ASM_SIMP_TAC (srw_ss()) [] THEN 690 `FV M' = params (vsub (Parameter u') v t)` 691 by METIS_TAC [convert_params] THEN 692 SRW_TAC [][notin_pvsub_I] THEN 693 METIS_TAC [convert_vsub_thm, pmact_flip_args] 694 ]); 695 696val convert_onto = store_thm( 697 "convert_onto", 698 ``!M. ?t. convert t M``, 699 HO_MATCH_MP_TAC termTheory.simple_induction THEN REPEAT STRIP_TAC THENL [ 700 Q.EXISTS_TAC `Parameter s` THEN SRW_TAC [][convert_rules], 701 Q.EXISTS_TAC `App t t'` THEN SRW_TAC [][convert_rules], 702 Q.SPECL_THEN [`t`, `v`] 703 (Q.X_CHOOSE_THEN `u` (Q.X_CHOOSE_THEN `t0` STRIP_ASSUME_TAC)) 704 shape_lemma THEN 705 SRW_TAC [][] THEN 706 Q.EXISTS_TAC `Abs u t0` THEN METIS_TAC [convert_rules] 707 ]) 708 709val params_vsub_upperbound = prove( 710 ``p IN params (vsub N v M) ==> p IN params N \/ p IN params M``, 711 Induct_on `M` THEN SRW_TAC [][] THEN METIS_TAC []); 712 713val params_vsub_lowerbound = prove( 714 ``p IN params M ==> p IN params (vsub N v M)``, 715 Induct_on `M` THEN SRW_TAC [][] THEN METIS_TAC []); 716 717val mpbeta_params = store_thm( 718 "mpbeta_params", 719 ``!t u. mpbeta t u ==> !p. p IN params u ==> p IN params t``, 720 HO_MATCH_MP_TAC mpbeta_ind THEN SRW_TAC [][] THENL [ 721 METIS_TAC [], 722 METIS_TAC [], 723 METIS_TAC [], 724 METIS_TAC [], 725 `p' IN params (Parameter p) \/ p' IN params M` 726 by METIS_TAC [params_vsub_lowerbound, params_vsub_upperbound] THEN 727 FULL_SIMP_TAC (srw_ss()) [], 728 METIS_TAC [params_vsub_upperbound] 729 ]); 730 731val vsub_vclosed = store_thm( 732 "vsub_vclosed", 733 ``!t. vclosed t ==> (vsub t' v t = t)``, 734 REPEAT STRIP_TAC THEN IMP_RES_TAC vclosed_empty_vars THEN 735 SRW_TAC [][vsub_14a]); 736 737val general_vsub_commute = store_thm( 738 "general_vsub_commute", 739 ``vclosed t1 /\ vclosed t2 /\ ~(v1 = v2) ==> 740 (vsub t1 v1 (vsub t2 v2 t) = vsub t2 v2 (vsub t1 v1 t))``, 741 Induct_on `t` THEN SRW_TAC [][vsub_vclosed] THEN METIS_TAC []); 742 743val convert_sub = store_thm( 744 "convert_sub", 745 ``~(p IN params t1) /\ 746 convert (vsub (Parameter p) v t1) M /\ 747 convert t2 N ==> 748 convert (vsub t2 v t1) ([N/p] M)``, 749 Q_TAC SUFF_TAC 750 `!t M. convert t M ==> 751 !t1pt2 t1 t2 p v N. 752 (t1pt2 = (t1,p,t2)) /\ 753 ~(p IN params t1) /\ 754 (vsub (Parameter p) v t1 = t) /\ 755 convert t2 N ==> 756 convert (vsub t2 v t1) ([N/p] M)` 757 THEN1 SRW_TAC [][] THEN 758 HO_MATCH_MP_TAC convert_strong_ind THEN 759 Q.EXISTS_TAC `\ (t1,p,t2). {p} UNION params t1 UNION params t2` THEN 760 ASM_SIMP_TAC (srw_ss()) [pairTheory.FORALL_PROD] THEN 761 SRW_TAC [][pvsub_eq_param, pvsub_eq_app, pvsub_eq_abs] THEN 762 FULL_SIMP_TAC (srw_ss()) [termTheory.SUB_THM, convert_rules] THENL [ 763 `FV N = params p_2` by SRW_TAC [][convert_params] THEN 764 SRW_TAC [][termTheory.SUB_THM] THEN 765 MATCH_MP_TAC (last (CONJUNCTS convert_rules)) THEN 766 `~(u IN params (vsub p_2 v' M0))` 767 by METIS_TAC [params_vsub_upperbound] THEN 768 SRW_TAC [][] THEN 769 `vclosed p_2` by METIS_TAC [convert_vclosed] THEN 770 `vsub (Parameter u) v (vsub p_2 v' M0) = 771 vsub p_2 v' (vsub (Parameter u) v M0)` 772 by SRW_TAC [][general_vsub_commute] THEN 773 SRW_TAC [][] THEN FIRST_X_ASSUM MATCH_MP_TAC THEN 774 SRW_TAC [][general_vsub_commute, notin_pvsub_I], 775 776 `FV N = params p_2` by SRW_TAC [][convert_params] THEN 777 SRW_TAC [][termTheory.SUB_THM] THEN 778 MATCH_MP_TAC (last (CONJUNCTS convert_rules)) THEN 779 Q_TAC SUFF_TAC `~(p_1' IN FV M)` THEN1 SRW_TAC [][termTheory.lemma14b] THEN 780 `FV M = params (vsub (Parameter u) v t)` 781 by SRW_TAC [][convert_params] THEN 782 SRW_TAC [][notin_pvsub_I] 783 ]); 784 785 786val mpbeta_MPpm = prove( 787 ``!t u. mpbeta t u ==> !pi. mpbeta (MPpm pi t) (MPpm pi u)``, 788 HO_MATCH_MP_TAC mpbeta_ind THEN 789 SRW_TAC [][mpbeta_rules, MPpm_vsub] THENL [ 790 MATCH_MP_TAC (List.nth(CONJUNCTS mpbeta_rules, 2)) THEN 791 Q.EXISTS_TAC `stringpm pi p` THEN SRW_TAC [][IN_params_MPpm], 792 MATCH_MP_TAC (last (CONJUNCTS mpbeta_rules)) THEN 793 `MPpm pi (Abs x M) = Abs x (MPpm pi M)` by SRW_TAC [][] THEN 794 METIS_TAC [vclosed_MPpm] 795 ]); 796 797val mpbeta_strong_ind = 798 IndDefLib.derive_strong_induction(mpbeta_rules, mpbeta_ind) 799 800val mpbeta_ccbeta = store_thm( 801 "mpbeta_ccbeta", 802 ``!t u. mpbeta t u ==> 803 !M N. convert t M /\ convert u N ==> compat_closure beta M N``, 804 HO_MATCH_MP_TAC mpbeta_strong_ind THEN 805 SRW_TAC [][compat_closure_rules, convert_abs, convert_app] THENL [ 806 METIS_TAC [compat_closure_rules, convert_unique], 807 METIS_TAC [compat_closure_rules, convert_unique], 808 SRW_TAC [boolSimps.DNF_ss][cc_beta_thm, termTheory.LAM_eq_thm, 809 termTheory.tpm_eqr] THEN 810 Cases_on `u' = u''` THEN ASM_SIMP_TAC (srw_ss()) [] THENL [ 811 SRW_TAC [][] THEN 812 `convert (vsub (Parameter p) u M) (tpm [(p,u')] M'') /\ 813 convert (vsub (Parameter p) v N) (tpm [(p,u')] M''')` 814 by METIS_TAC [convert_vsub_thm, pmact_flip_args] THEN 815 METIS_TAC [cc_beta_tpm_eqn, pmact_inverse], 816 `~(u' IN FV M''')` 817 by (`FV M''' = params (vsub (Parameter u'') v N)` 818 by SRW_TAC [][convert_params] THEN 819 SRW_TAC [][] THEN 820 Cases_on `u' = p` THEN1 SRW_TAC [][notin_pvsub_I] THEN 821 `mpbeta (MPpm [(u'',p)] (vsub (Parameter p) u M)) 822 (MPpm [(u'',p)] (vsub (Parameter p) v N))` 823 by SRW_TAC [][mpbeta_MPpm] THEN 824 POP_ASSUM MP_TAC THEN 825 SRW_TAC [][MPpm_vsub, MPpm_fresh] THEN 826 Q_TAC SUFF_TAC 827 `~(u' IN params (vsub (Parameter u'') u (MPpm [(u'',p)] M)))` 828 THEN1 METIS_TAC [mpbeta_params] THEN 829 SRW_TAC [][notin_pvsub_I, IN_params_MPpm]) THEN 830 `convert (vsub (Parameter p) u M) (tpm [(u',p)] M'') /\ 831 convert (vsub (Parameter p) v N) (tpm [(u'',p)] M''')` 832 by METIS_TAC [convert_vsub_thm] THEN 833 `compat_closure beta (tpm [(u',p)] M'') (tpm [(u'',p)] M''')` 834 by METIS_TAC [] THEN 835 `compat_closure beta M'' (tpm [(u',p)] (tpm [(u'',p)] M'''))` 836 by METIS_TAC [cc_beta_tpm, pmact_sing_inv] THEN 837 Q_TAC SUFF_TAC `tpm [(u',p)] (tpm [(u'',p)] M''') = tpm [(u'',u')] M'''` 838 THEN1 METIS_TAC [] THEN 839 Cases_on `p = u'` THEN1 SRW_TAC [][] THEN 840 Cases_on `p = u''` THEN1 SRW_TAC [][pmact_flip_args] THEN 841 ONCE_REWRITE_TAC [GSYM pmact_sing_to_back] THEN 842 SRW_TAC [][] THEN 843 `~(p IN FV M''') /\ ~(u' IN FV M''')` 844 by METIS_TAC [convert_params, notin_pvsub_I] THEN 845 SRW_TAC [][termTheory.tpm_fresh] 846 ], 847 848 `N' = [t1/u]M''` by METIS_TAC [convert_sub, convert_unique] THEN 849 SRW_TAC [][cc_beta_thm] THEN METIS_TAC [] 850 ]); 851 852 853val alpha_def = Define`alpha t1 t2 = ?M. convert t1 M /\ convert t2 M` 854 855val alpha_trans = store_thm( 856 "alpha_trans", 857 ``alpha t1 t2 /\ alpha t2 t3 ==> alpha t1 t3``, 858 SRW_TAC [][alpha_def] THEN METIS_TAC [convert_unique]); 859 860val alpha_sym = store_thm( 861 "alpha_sym", 862 ``alpha t1 t2 ==> alpha t2 t1``, 863 SRW_TAC [][alpha_def] THEN METIS_TAC []); 864 865val alpha_prefl = store_thm( 866 "alpha_prefl", 867 ``alpha t t = vclosed t``, 868 SRW_TAC [][alpha_def] THEN METIS_TAC [convert_vclosed, vclosed_convert]); 869 870val convert_to_app = prove( 871 ``convert t (M1 @@ M2) = ?t1 t2. (t = App t1 t2) /\ convert t1 M1 /\ 872 convert t2 M2``, 873 CONV_TAC (LAND_CONV (ONCE_REWRITE_CONV [convert_cases])) THEN 874 SRW_TAC [][]); 875 876val convert_to_lam = prove( 877 ``convert t (LAM v M) = ?u t0. (t = Abs u t0) /\ ~(v IN params t0) /\ 878 convert (vsub (Parameter v) u t0) M``, 879 CONV_TAC (LAND_CONV (ONCE_REWRITE_CONV [convert_cases])) THEN 880 SRW_TAC [boolSimps.DNF_ss][termTheory.LAM_eq_thm, termTheory.tpm_eqr] THEN 881 SRW_TAC [][EQ_IMP_THM] THEN 882 Q_TAC SUFF_TAC `~(v IN params t')` 883 THEN1 METIS_TAC [convert_vsub_thm, pmact_flip_args, 884 pmact_sing_inv] THEN 885 `~(v IN FV (tpm [(v,u)] M))` by SRW_TAC [][] THEN 886 `~(v IN params (vsub (Parameter u) v' t'))` 887 by METIS_TAC [convert_params] THEN 888 METIS_TAC [params_vsub_lowerbound]); 889 890val alpha_app = prove( 891 ``alpha (App t1 t2) t = ?t1' t2'. (t = App t1' t2') /\ 892 alpha t1 t1' /\ alpha t2 t2'``, 893 SRW_TAC [boolSimps.DNF_ss][alpha_def, convert_app, convert_to_app] THEN 894 METIS_TAC []); 895 896(* Curiously, only need to alpha-convert after a reduction, and not 897 before. *) 898val ccbeta_beta = store_thm( 899 "ccbeta_beta", 900 ``!M N. compat_closure beta M N ==> 901 !t u. convert t M /\ convert u N ==> 902 (alpha O mpbeta) t u``, 903 HO_MATCH_MP_TAC ccbeta_ind THEN Q.EXISTS_TAC `{}` THEN 904 SRW_TAC [][relationTheory.O_DEF, convert_to_app, convert_to_lam] THENL [ 905 IMP_RES_TAC convert_vclosed THEN 906 Q.EXISTS_TAC `vsub t2 u' t0` THEN CONJ_TAC THENL [ 907 MATCH_MP_TAC (last (CONJUNCTS mpbeta_rules)) THEN 908 SRW_TAC [][vclosed_abs] THEN METIS_TAC [], 909 SRW_TAC [][alpha_def] THEN METIS_TAC [convert_sub] 910 ], 911 912 `?y. mpbeta t1 y /\ alpha y t1'` by METIS_TAC [] THEN 913 Q.EXISTS_TAC `App y t2` THEN 914 IMP_RES_TAC convert_vclosed THEN 915 SRW_TAC [][alpha_app, alpha_prefl] THEN 916 SRW_TAC [][mpbeta_rules, alpha_app, alpha_prefl] THEN 917 SRW_TAC [][alpha_def] THEN METIS_TAC [], 918 919 `?y. mpbeta t2 y /\ alpha y t2'` by METIS_TAC [] THEN 920 Q.EXISTS_TAC `App t1 y` THEN 921 IMP_RES_TAC convert_vclosed THEN 922 SRW_TAC [][alpha_app, alpha_prefl] THEN 923 SRW_TAC [][mpbeta_rules, alpha_app, alpha_prefl] THEN 924 SRW_TAC [][alpha_def] THEN METIS_TAC [], 925 926 `?y. mpbeta (vsub (Parameter v) u' t0) y /\ 927 alpha y (vsub (Parameter v) u'' t0')` 928 by METIS_TAC [] THEN 929 `?v1 t1. (y = vsub (Parameter v) v1 t1) /\ ~(v IN params t1)` 930 by METIS_TAC [shape_lemma] THEN 931 Q.EXISTS_TAC `Abs v1 t1` THEN CONJ_TAC THENL [ 932 MATCH_MP_TAC (List.nth(CONJUNCTS mpbeta_rules, 2)) THEN 933 Q.EXISTS_TAC `v` THEN SRW_TAC [][], 934 ALL_TAC 935 ] THEN 936 SRW_TAC [boolSimps.DNF_ss][alpha_def, convert_abs] THEN 937 MAP_EVERY Q.EXISTS_TAC [`v`, `N`, `v`, `N`] THEN 938 FULL_SIMP_TAC (srw_ss()) [alpha_def] THEN METIS_TAC [convert_unique] 939 ]); 940 941 942val _ = export_theory() 943