1open HolKernel Parse boolLib; 2 3(* --------------------------------------------------------------------- *) 4(* Building the definitions of alpha equivalence for object expressions. *) 5(* --------------------------------------------------------------------- *) 6 7 8val _ = new_theory "alpha"; 9 10 11open prim_recTheory pairTheory pairLib listTheory rich_listTheory; 12open combinTheory; 13open listLib; 14open pred_setTheory pred_setLib; 15open numTheory; 16open numLib; 17open arithmeticTheory; 18open bossLib; 19open ind_rel; 20open dep_rewrite; 21open more_listTheory; 22open more_setTheory; 23open variableTheory; 24open termTheory; 25 26 27open tactics; 28 29 30 31val vars = ty_antiq( ==`:var list`== ); 32val subs = ty_antiq( ==`:(var # 'a term1) list`== ); 33 34 35 36(* --------------------------------------------------------------------- *) 37(* Define alpha equivalence for lambda expressions. *) 38(* --------------------------------------------------------------------- *) 39 40(* Here is the syntax, repeated for clarity: 41 42val _ = Hol_datatype 43 44 ` term1 = Con1 of 'a 45 | Var1 of var 46 | App1 of term1 => term1 47 | Lam1 of var => term1 ` ; 48 49*) 50 51 52(* ---------------------------------------------------------------------- *) 53(* To define alpha equivalence between objects, we first need to define a *) 54(* matching function, that checks if a pair of variables match according *) 55(* to a given pair of lists of variables; the lists are searched, and *) 56(* the variables must each be found at the same place. *) 57(* ---------------------------------------------------------------------- *) 58 59val alpha_match_def = Define 60 `(alpha_match NIL ys x1 y1 = (if ys = [] then (x1 = y1) else F)) /\ 61 (alpha_match (CONS (x:var) xs) ys x1 y1 = 62 (if ys = [] then F else 63 (if x1 = x then (y1 = HD ys) /\ (LENGTH xs = LENGTH (TL ys)) else 64 (if y1 = HD ys then F else 65 alpha_match xs (TL ys) x1 y1))))`; 66 67val alpha_match = store_thm 68 ("alpha_match", 69 ���(!x1 y1. alpha_match [] [] x1 y1 = (x1 = y1)) /\ 70 (!ys y x1 y1. alpha_match [] (CONS y ys) x1 y1 = F) /\ 71 (!xs x x1 y1. alpha_match (CONS x xs) [] x1 y1 = F) /\ 72 (!xs ys x y x1 y1. alpha_match (CONS x xs) (CONS y ys) x1 y1 = 73 (((x1 = x) /\ (y1 = y) 74 /\ (LENGTH xs = LENGTH ys)) \/ 75 (~(x1 = x) /\ ~(y1 = y) 76 /\ alpha_match xs ys x1 y1)))���, 77 REWRITE_TAC[alpha_match_def] 78 THEN REWRITE_TAC[NOT_CONS_NIL] 79 THEN REWRITE_TAC[HD,TL] 80 THEN REPEAT GEN_TAC 81 THEN COND_CASES_TAC 82 THENL 83 [ REWRITE_TAC[], 84 85 COND_CASES_TAC 86 THEN ASM_REWRITE_TAC[] 87 ] 88 ); 89 90val alpha_match_NIL = store_thm 91 ("alpha_match_NIL", 92 ���alpha_match [] [] = $=���, 93 EXT_TAC ���x:var��� 94 THEN GEN_TAC 95 THEN EXT_TAC ���y:var��� 96 THEN GEN_TAC 97 THEN REWRITE_TAC[alpha_match] 98 ); 99 100val alpha_match_REFL = store_thm 101 ("alpha_match_REFL", 102 ���!xs x. alpha_match xs xs x x���, 103 LIST_INDUCT_TAC 104 THEN ASM_REWRITE_TAC[alpha_match] 105 THEN REWRITE_TAC[EXCLUDED_MIDDLE] 106 ); 107 108val alpha_match_SYM = store_thm 109 ("alpha_match_SYM", 110 ���!xs ys x1 y1. alpha_match xs ys x1 y1 = alpha_match ys xs y1 x1���, 111 LIST_INDUCT_TAC 112 THEN REWRITE_TAC[alpha_match] 113 THENL 114 [ LIST_INDUCT_TAC 115 THEN REWRITE_TAC[alpha_match] 116 THEN REPEAT GEN_TAC 117 THEN CONV_TAC (RAND_CONV (ONCE_REWRITE_CONV[EQ_SYM_EQ])) 118 THEN REFL_TAC, 119 120 GEN_TAC 121 THEN LIST_INDUCT_TAC 122 THEN REWRITE_TAC[alpha_match] 123 THEN REPEAT GEN_TAC 124 THEN ASM_REWRITE_TAC[] 125 THEN EQ_TAC 126 THEN STRIP_TAC 127 THEN ASM_REWRITE_TAC[] 128 ] 129 ); 130 131val alpha_match_TRANS = store_thm 132 ("alpha_match_TRANS", 133 ���!xs ys zs x y z. alpha_match xs ys x y /\ alpha_match ys zs y z 134 ==> alpha_match xs zs x z���, 135 LIST_INDUCT_TAC 136 THENL 137 [ LIST_INDUCT_TAC 138 THENL 139 [ LIST_INDUCT_TAC 140 THEN REWRITE_TAC[alpha_match] 141 THEN REWRITE_TAC[EQ_TRANS], 142 143 REWRITE_TAC[alpha_match] 144 ], 145 146 GEN_TAC 147 THEN LIST_INDUCT_TAC 148 THEN REWRITE_TAC[alpha_match] 149 THEN GEN_TAC 150 THEN LIST_INDUCT_TAC 151 THEN REWRITE_TAC[alpha_match] 152 THEN REPEAT GEN_TAC 153 THEN STRIP_TAC 154 THEN ASM_REWRITE_TAC[] 155 THEN RES_TAC 156 ] 157 ); 158 159 160val alpha_match_SUB_var = store_thm 161 ("alpha_match_SUB_var", 162 ���!xs ys x y. alpha_match xs ys x y = 163 ((LENGTH xs = LENGTH ys) /\ 164 (SUB1 (xs // ys) x = Var1 y:'a term1) /\ 165 (SUB1 (ys // xs) y = Var1 x:'a term1))���, 166 LIST_INDUCT_TAC 167 THENL 168 [ LIST_INDUCT_TAC 169 THEN REWRITE_TAC[alpha_match,vsubst1,SUB1,term1_one_one, 170 LENGTH, GSYM NOT_SUC] 171 THEN REPEAT GEN_TAC 172 THEN EQ_TAC 173 THEN REPEAT STRIP_TAC 174 THEN ASM_REWRITE_TAC[], 175 176 GEN_TAC 177 THEN LIST_INDUCT_TAC 178 THEN REWRITE_TAC[alpha_match,vsubst1,SUB1,term1_one_one, 179 LENGTH, NOT_SUC] 180 THEN REPEAT GEN_TAC 181 THEN ASM_REWRITE_TAC[prim_recTheory.INV_SUC_EQ] 182 THEN COND_CASES_TAC (* (x'' = x)? *) 183 THENL 184 [ POP_ASSUM REWRITE_THM 185 THEN REWRITE_TAC[term1_one_one] 186 THEN COND_CASES_TAC (* (x' = y)? *) 187 THENL 188 [ POP_ASSUM REWRITE_THM, 189 190 POP_ASSUM (REWRITE_THM o GSYM) 191 ], 192 193 FIRST_ASSUM (REWRITE_THM o GSYM) 194 THEN COND_CASES_TAC (* (x' = y)? *) 195 THENL 196 [ POP_ASSUM (REWRITE_THM o SYM) 197 THEN REWRITE_TAC[term1_one_one] 198 THEN FIRST_ASSUM (REWRITE_THM o GSYM), 199 200 REWRITE_TAC[] 201 ] 202 ] 203 ] 204 ); 205 206 207val alpha_match_IDENT = store_thm 208 ("alpha_match_IDENT", 209 ���!xs x y. alpha_match xs xs x y = (x = y)���, 210 LIST_INDUCT_TAC 211 THENL 212 [ REWRITE_TAC[alpha_match], 213 214 ASM_REWRITE_TAC[alpha_match] 215 THEN REPEAT GEN_TAC 216 THEN EQ_TAC 217 THENL 218 [ STRIP_TAC 219 THEN ASM_REWRITE_TAC[], 220 221 DISCH_THEN REWRITE_THM 222 THEN REWRITE_TAC[EXCLUDED_MIDDLE] 223 ] 224 ] 225 ); 226 227 228val alpha_match_NOT_EQ = store_thm 229 ("alpha_match_NOT_EQ", 230 ���!xs ys x y x' y'. 231 alpha_match (CONS x xs) (CONS y ys) x' y' /\ ~(x' = x) 232 ==> alpha_match xs ys x' y' /\ ~(y' = y)���, 233 REPEAT GEN_TAC 234 THEN REWRITE_TAC[alpha_match_SUB_var] 235 THEN REWRITE_TAC[LENGTH,INV_SUC_EQ,vsubst1,SUB1] 236 THEN STRIP_TAC 237 THEN ASM_REWRITE_TAC[] 238 THEN POP_ASSUM (fn th => REWRITE_ALL_TAC[th] THEN MP_TAC th) 239 THEN POP_ASSUM MP_TAC 240 THEN COND_CASES_TAC 241 THENL 242 [ REWRITE_TAC[term1_one_one] 243 THEN DISCH_THEN REWRITE_THM, 244 245 DISCH_TAC 246 THEN ASM_REWRITE_TAC[] 247 ] 248 ); 249 250 251val alpha_match_pair = store_thm 252 ("alpha_match_pair", 253 ���!xs ys x1 y1 x2 y2. 254 alpha_match xs ys x1 y1 /\ 255 alpha_match xs ys x2 y2 ==> 256 ((x1 = x2) = (y1 = y2))���, 257 LIST_INDUCT_TAC 258 THENL 259 [ LIST_INDUCT_TAC 260 THEN REWRITE_TAC[alpha_match] 261 THEN REPEAT STRIP_TAC 262 THEN ASM_REWRITE_TAC[], 263 264 GEN_TAC 265 THEN LIST_INDUCT_TAC 266 THEN REWRITE_TAC[alpha_match] 267 THEN POP_ASSUM (fn th => ALL_TAC) 268 THEN REPEAT STRIP_TAC (* 4 subgoals *) 269 THEN ASM_REWRITE_TAC[] 270 THEN ASSUM_LIST (EVERY o (map (REWRITE_THM o GSYM))) 271 THEN RES_TAC 272 ] 273 ); 274 275val alpha_match_LENGTH = store_thm 276 ("alpha_match_LENGTH", 277 ���!xs ys x y. alpha_match xs ys x y ==> (LENGTH xs = LENGTH ys)���, 278 LIST_INDUCT_TAC 279 THENL 280 [ LIST_INDUCT_TAC 281 THEN REWRITE_TAC[alpha_match], 282 283 GEN_TAC 284 THEN LIST_INDUCT_TAC 285 THEN REWRITE_TAC[alpha_match] 286 THEN POP_TAC 287 THEN REPEAT STRIP_TAC (* 2 subgoals *) 288 THEN RES_TAC 289 THEN ASM_REWRITE_TAC[LENGTH] 290 ] 291 ); 292 293 294 295(* --------------------------------------------------------------------- *) 296(* Definition of equivalence between objects. *) 297(* --------------------------------------------------------------------- *) 298 299val ALPHA1 = 300���ALPHA1 : 'a term1 -> 'a term1 -> ^vars -> ^vars -> bool���; 301 302val ALPHA1_patterns = [���^ALPHA1 t1 t2 xs ys���]; 303 304val ALPHA1_rules_tm = 305��� 306 307 (* -------------------------------------------- *) 308 (^ALPHA1 (Con1 a) (Con1 a) xs ys) /\ 309 310 311 (alpha_match xs ys x y 312 (* -------------------------------------------- *) ==> 313 (^ALPHA1 (Var1 x) (Var1 y) xs ys)) /\ 314 315 316 ((^ALPHA1 t1 t2 xs ys) /\ (^ALPHA1 u1 u2 xs ys) 317 (* -------------------------------------------- *) ==> 318 (^ALPHA1 (App1 t1 u1) (App1 t2 u2) xs ys)) /\ 319 320(* Alpha conversion: *) 321 322 ((^ALPHA1 u1 u2 (CONS x xs) (CONS y ys)) 323 (* -------------------------------------------- *) ==> 324 (^ALPHA1 (Lam1 x u1) (Lam1 y u2) xs ys)) 325���; 326 327val (ALPHA1_rules_sat,ALPHA1_ind_thm) = 328 define_inductive_relations ALPHA1_patterns ALPHA1_rules_tm; 329 330val ALPHA1_inv_thms = prove_inversion_theorems 331 ALPHA1_rules_sat ALPHA1_ind_thm; 332 333val ALPHA1_strong_ind = prove_strong_induction 334 ALPHA1_rules_sat ALPHA1_ind_thm; 335 336val _ = save_thm ("ALPHA1_rules_sat", ALPHA1_rules_sat); 337val _ = save_thm ("ALPHA1_ind_thm", ALPHA1_ind_thm); 338val _ = save_thm ("ALPHA1_inv_thms", LIST_CONJ ALPHA1_inv_thms); 339val _ = save_thm ("ALPHA1_strong_ind", ALPHA1_strong_ind); 340 341 342val [ALPHA1_Con1, ALPHA1_Var1, ALPHA1_App1, ALPHA1_Lam1] 343 = CONJUNCTS ALPHA1_rules_sat; 344 345 346 347val ALPHA1_REFL = store_thm 348 ("ALPHA1_REFL", 349 ���!t:'a term1 xs. ALPHA1 t t xs xs���, 350 Induct 351 THEN REPEAT GEN_TAC 352 THENL (* 4 subgoals *) 353 [ REWRITE_TAC[ALPHA1_Con1], 354 355 MATCH_MP_TAC ALPHA1_Var1 356 THEN REWRITE_TAC[alpha_match_REFL], 357 358 MATCH_MP_TAC ALPHA1_App1 359 THEN ASM_REWRITE_TAC[], 360 361 MATCH_MP_TAC ALPHA1_Lam1 362 THEN ASM_REWRITE_TAC[] 363 ] 364 ); 365 366 367val ALPHA1_IMP_SYM = TAC_PROOF(([], 368 ���!t1 t2:'a term1 xs ys. ALPHA1 t1 t2 xs ys ==> ALPHA1 t2 t1 ys xs���), 369 rule_induct ALPHA1_strong_ind 370 THEN REPEAT STRIP_TAC 371 THENL (* 4 subgoals *) 372 [ ASM_REWRITE_TAC[ALPHA1_Con1], 373 374 MATCH_MP_TAC ALPHA1_Var1 375 THEN IMP_RES_TAC alpha_match_SYM, 376 377 MATCH_MP_TAC ALPHA1_App1 378 THEN ASM_REWRITE_TAC[], 379 380 MATCH_MP_TAC ALPHA1_Lam1 381 THEN ASM_REWRITE_TAC[] 382 ] 383 ); 384 385val ALPHA1_SYM = store_thm 386 ("ALPHA1_SYM", 387 ���!t1 t2 :'a term1 xs ys. ALPHA1 t1 t2 xs ys = ALPHA1 t2 t1 ys xs���, 388 REPEAT STRIP_TAC 389 THEN EQ_TAC 390 THEN STRIP_TAC 391 THEN IMP_RES_TAC ALPHA1_IMP_SYM 392 ); 393 394 395val ALPHA1_TRANS1 = TAC_PROOF(([], 396 ���!t1 t2 :'a term1 xs ys. 397 ALPHA1 t1 t2 xs ys ==> 398 !t3 zs. ALPHA1 t2 t3 ys zs ==> 399 ALPHA1 t1 t3 xs zs���), 400 rule_induct ALPHA1_strong_ind 401 THEN REPEAT STRIP_TAC 402 THEN POP_ASSUM MP_TAC 403 THEN ONCE_REWRITE_TAC ALPHA1_inv_thms 404 THEN REWRITE_TAC[term1_one_one,term1_distinct2] 405 THEN REPEAT GEN_TAC 406 THEN STRIP_TAC 407 THEN PROVE_TAC[alpha_match_TRANS] 408 ); 409 410 411val ALPHA1_TRANS = store_thm 412 ("ALPHA1_TRANS", 413 ���!t1 t2 t3 :'a term1 xs ys zs. 414 ALPHA1 t1 t2 xs ys /\ 415 ALPHA1 t2 t3 ys zs ==> 416 ALPHA1 t1 t3 xs zs���, 417 REPEAT STRIP_TAC 418 THEN IMP_RES_TAC ALPHA1_TRANS1 419 ); 420 421 422val ALPHA1_HEIGHT = store_thm 423 ("ALPHA1_HEIGHT", 424 ���!t1 t2 :'a term1 xs ys. 425 ALPHA1 t1 t2 xs ys ==> (HEIGHT1 t1 = HEIGHT1 t2)���, 426 rule_induct ALPHA1_ind_thm 427 THEN REWRITE_TAC[HEIGHT1_def,INV_SUC_EQ] 428 THEN REPEAT STRIP_TAC 429 THEN ASM_REWRITE_TAC[] 430 ); 431 432 433val ALPHA1_term_similar = store_thm 434 ("ALPHA1_term_similar", 435 ���(!a t xs ys. ALPHA1 (Con1 a) t xs ys ==> (t = Con1 a :'a term1)) /\ 436 (!x t xs ys. ALPHA1 (Var1 x) t xs ys ==> (?y. t = Var1 y :'a term1)) /\ 437 (!t1 u1 t xs ys. ALPHA1 (App1 t1 u1) t xs ys ==> 438 (?t2 u2. t = App1 t2 u2 :'a term1)) /\ 439 (!x1 u1 t xs ys. ALPHA1 (Lam1 x1 u1) t xs ys ==> 440 (?x2 u2. t = Lam1 x2 u2 :'a term1))���, 441 PURE_ONCE_REWRITE_TAC ALPHA1_inv_thms 442 THEN REWRITE_TAC[term1_one_one,term1_distinct2] 443 THEN REPEAT STRIP_TAC 444 THEN PROVE_TAC[] 445 ); 446 447 448val ALPHA1_term_pos = store_thm 449 ("ALPHA1_term_pos", 450 ���(!a b xs ys. ALPHA1 (Con1 a :'a term1) (Con1 b) xs ys 451 = ((a = b) (*/\ (LENGTH xs = LENGTH ys)*) )) /\ 452 (!x y xs ys. ALPHA1 (Var1 x :'a term1) (Var1 y) xs ys 453 = alpha_match xs ys x y) /\ 454 (!t1 t2 u1 u2 :'a term1 xs ys. ALPHA1 (App1 t1 u1) (App1 t2 u2) xs ys 455 = (ALPHA1 t1 t2 xs ys /\ ALPHA1 u1 u2 xs ys)) /\ 456 (!x1 x2 u1 u2 :'a term1 xs ys. ALPHA1 (Lam1 x1 u1) (Lam1 x2 u2) xs ys 457 = ALPHA1 u1 u2 (CONS x1 xs) (CONS x2 ys))���, 458 REPEAT CONJ_TAC 459 THEN REPEAT GEN_TAC 460 THEN (EQ_TAC 461 THENL [ DISCH_THEN (STRIP_ASSUME_TAC 462 o REWRITE_RULE[term1_one_one,term1_distinct2] 463 o ONCE_REWRITE_RULE ALPHA1_inv_thms) 464 THEN ASM_REWRITE_TAC[], 465 466 REWRITE_TAC[] 467 THEN REPEAT STRIP_TAC 468 THEN FIRST (map (fn th => ASM_REWRITE_TAC[] 469 THEN TRY (MATCH_MP_TAC th) 470 THEN ASM_REWRITE_TAC[th] 471 THEN NO_TAC) 472 (CONJUNCTS ALPHA1_rules_sat)) 473 ]) 474 ); 475 476 477val ALPHA1_term_neg = store_thm 478 ("ALPHA1_term_neg", 479 ���(!a x xs ys. ALPHA1 (Con1 a :'a term1) (Var1 x) xs ys = F) /\ 480 (!a t u xs ys. ALPHA1 (Con1 a :'a term1) (App1 t u) xs ys = F) /\ 481 (!a y u xs ys. ALPHA1 (Con1 a :'a term1) (Lam1 y u) xs ys = F) /\ 482 (!x a xs ys. ALPHA1 (Var1 x :'a term1) (Con1 a) xs ys = F) /\ 483 (!x t u xs ys. ALPHA1 (Var1 x :'a term1) (App1 t u) xs ys = F) /\ 484 (!x y u xs ys. ALPHA1 (Var1 x :'a term1) (Lam1 y u) xs ys = F) /\ 485 (!t u a xs ys. ALPHA1 (App1 t u :'a term1) (Con1 a) xs ys = F) /\ 486 (!t u x xs ys. ALPHA1 (App1 t u :'a term1) (Var1 x) xs ys = F) /\ 487 (!t u y v xs ys. ALPHA1 (App1 t u :'a term1) (Lam1 y v) xs ys = F) /\ 488 (!y u a xs ys. ALPHA1 (Lam1 y u :'a term1) (Con1 a) xs ys = F) /\ 489 (!y u x xs ys. ALPHA1 (Lam1 y u :'a term1) (Var1 x) xs ys = F) /\ 490 (!y v t u xs ys. ALPHA1 (Lam1 y v :'a term1) (App1 t u) xs ys = F)���, 491 PURE_ONCE_REWRITE_TAC ALPHA1_inv_thms 492 THEN REWRITE_TAC[term1_one_one,term1_distinct2] 493 ); 494 495 496 497val ALPHA1_FV = store_thm 498 ("ALPHA1_FV", 499 ���!t1 t2 :'a term1 xs ys. 500 ALPHA1 t1 t2 xs ys ==> 501 (!x. x IN FV1 t1 ==> 502 (?y. y IN FV1 t2 /\ alpha_match xs ys x y))���, 503 504 rule_induct ALPHA1_strong_ind 505 THEN REWRITE_TAC[FV1_def] 506 THEN REWRITE_TAC[IN_INSERT,NOT_IN_EMPTY,IN_UNION,IN_DIFF] 507 THEN REPEAT STRIP_TAC 508 THEN RES_TAC 509 THEN TRY (EXISTS_TAC ���y:var��� 510 THEN ASM_REWRITE_TAC[] 511 THEN NO_TAC) 512 (* only one goal here *) 513 THEN EXISTS_TAC ���y':var��� 514 THEN IMP_RES_TAC alpha_match_NOT_EQ 515 THEN ASM_REWRITE_TAC[] 516 ); 517(* Glory to God! Soli Deo Gloria! *) 518 519 520 521val FORALL_OR_IMP = TAC_PROOF(([], 522 ���!s t (f:'a->'b) g. 523 (!x. x IN s \/ x IN t ==> (f x = g x)) ==> 524 ((!x. x IN s ==> (f x = g x)) /\ 525 (!x. x IN t ==> (f x = g x)))���), 526 PROVE_TAC [] 527 ); 528 529 530val ALPHA1_FREE_CONTEXT = store_thm 531 ("ALPHA1_FREE_CONTEXT", 532 ���!t1:'a term1 t2 xs ys xs' ys'. 533 ((LENGTH xs = LENGTH ys) = (LENGTH xs' = LENGTH ys')) /\ 534 (!x. (x IN FV1 t1) ==> 535 (SUB1 ((xs // ys):^subs) x = SUB1 (xs' // ys') x)) /\ 536 (!y. (y IN FV1 t2) ==> 537 (SUB1 ((ys // xs):^subs) y = SUB1 (ys' // xs') y)) ==> 538 (ALPHA1 t1 t2 xs ys = ALPHA1 t1 t2 xs' ys')���, 539 Induct 540 THENL [GEN_TAC, GEN_TAC, ALL_TAC, GEN_TAC] 541 THEN Cases 542 THEN REWRITE_TAC[ALPHA1_term_neg] 543 THEN REPEAT STRIP_TAC 544 THEN REWRITE_TAC[ALPHA1_term_pos] 545 THEN REWRITE_ALL_TAC[FV1_def,IN_DIFF,IN_UNION,IN] 546 THEN EQ_TAC 547 THENL (* 8 subgoals *) 548 [ 549 (*FIRST_ASSUM (REWRITE_THM o SYM), 550 551 FIRST_ASSUM (REWRITE_THM o SYM),*) 552 553 REWRITE_TAC[alpha_match_SUB_var] 554 THEN RW_TAC list_ss [], 555 556 REWRITE_TAC[alpha_match_SUB_var] 557 THEN RW_TAC list_ss [], 558 559 IMP_RES_TAC FORALL_OR_IMP 560 THEN STRIP_TAC 561 THEN RES_TAC 562 THEN ASM_REWRITE_TAC[], 563 564 IMP_RES_TAC FORALL_OR_IMP 565 THEN STRIP_TAC 566 THEN RES_TAC 567 THEN ASM_REWRITE_TAC[], 568 569 FIRST_ASSUM (fn th => 570 DEP_REWRITE_TAC[ 571 SPECL [���t:'a term1���, 572 ���CONS (v:var) xs ���,���CONS (v':var) ys ���, 573 ���CONS (v:var) xs'���,���CONS (v':var) ys'���] 574 th]) 575 THEN ASM_REWRITE_TAC[LENGTH,INV_SUC_EQ] 576 THEN CONJ_TAC 577 THEN GEN_TAC 578 THEN DISCH_TAC 579 THEN REWRITE_TAC[vsubst1,SUB1] 580 THEN COND_CASES_TAC 581 THEN ASM_REWRITE_TAC[] 582 THEN FIRST_ASSUM MATCH_MP_TAC 583 THEN ASM_REWRITE_TAC[], 584 585 FIRST_ASSUM (fn th => 586 DEP_REWRITE_TAC[ 587 SPECL [���t:'a term1���, 588 ���CONS (v:var) xs'���,���CONS (v':var) ys'���, 589 ���CONS (v:var) xs ���,���CONS (v':var) ys ���] 590 th]) 591 THEN ASM_REWRITE_TAC[LENGTH,INV_SUC_EQ] 592 THEN ONCE_REWRITE_TAC[EQ_SYM_EQ] 593 THEN CONJ_TAC 594 THEN GEN_TAC 595 THEN DISCH_TAC 596 THEN REWRITE_TAC[vsubst1,SUB1] 597 THEN COND_CASES_TAC 598 THEN ASM_REWRITE_TAC[] 599 THEN FIRST_ASSUM MATCH_MP_TAC 600 THEN ASM_REWRITE_TAC[] 601 ] 602 ); 603 604 605 606val ALPHA1_EXTRANEOUS_CONTEXT = store_thm 607 ("ALPHA1_EXTRANEOUS_CONTEXT", 608 ���!t1 t2 :'a term1 xs ys x y. 609 ~(x IN FV1 t1) /\ ~(y IN FV1 t2) ==> 610 (ALPHA1 t1 t2 (CONS x xs) (CONS y ys) = 611 ALPHA1 t1 t2 xs ys)���, 612 REPEAT STRIP_TAC 613 THEN MATCH_MP_TAC ALPHA1_FREE_CONTEXT 614 THEN REWRITE_TAC[LENGTH,INV_SUC_EQ] 615 THEN CONJ_TAC 616 THEN GEN_TAC 617 THEN DISCH_TAC 618 THEN REWRITE_TAC[vsubst1,SUB1] 619 THEN COND_CASES_TAC 620 THEN ASM_REWRITE_TAC[] 621 THEN POP_ASSUM REWRITE_ALL_THM 622 THEN RES_TAC 623 ); 624 625 626(* ---------------------------------------------------------------------- *) 627(* Now we prepare to prove ALPHA1_SUB, the key and most important theorem *) 628(* of this theory. It is difficult, but critical. *) 629(* ---------------------------------------------------------------------- *) 630 631 632(* define ALPHA1_subst *) 633 634val ALPHA1_subst = 635 new_definition 636 ("ALPHA1_subst", 637 ���ALPHA1_subst xs ys xs' ys' t1 t2 s1 (s2:^subs) <=> 638 (LENGTH xs' = LENGTH ys') /\ 639 (!x y. (x IN t1) /\ (y IN t2) /\ 640 alpha_match xs ys x y ==> 641 ALPHA1 (SUB1 s1 x) (SUB1 s2 y) xs' ys')���); 642 643 644val ALPHA1_subst_UNION = store_thm 645 ("ALPHA1_subst_UNION", 646 ���!xs ys xs' ys' t11 t12 t21 t22 s1 (s2:^subs). 647 ALPHA1_subst xs ys xs' ys' (t11 UNION t12) (t21 UNION t22) s1 s2 648 ==> 649 (ALPHA1_subst xs ys xs' ys' t11 t21 s1 s2 /\ 650 ALPHA1_subst xs ys xs' ys' t12 t22 s1 s2)���, 651 REPEAT GEN_TAC 652 THEN REWRITE_TAC[ALPHA1_subst] 653 THEN REWRITE_TAC[IN_UNION] 654 THEN REPEAT STRIP_TAC 655 THEN ASM_REWRITE_TAC[] 656 THEN FIRST_ASSUM MATCH_MP_TAC 657 THEN ASM_REWRITE_TAC[] 658 ); 659 660val ALPHA1_subst_LENGTH = store_thm 661 ("ALPHA1_subst_LENGTH", 662 ���!xs ys xs' ys' t1 t2 s1 (s2:^subs). 663 ALPHA1_subst xs ys xs' ys' t1 t2 s1 s2 664 ==> 665 (LENGTH xs' = LENGTH ys')���, 666 REWRITE_TAC[ALPHA1_subst] 667 THEN REPEAT STRIP_TAC 668 ); 669 670 671 672val variant_not_in_sub = store_thm 673 ("variant_not_in_sub", 674 ���!v v' (s:^subs) t x. 675 FINITE t /\ (x IN t) /\ 676 (v' = variant v (FV_subst1 s t)) 677 ==> 678 ~(v' IN FV1 (SUB1 s x))���, 679 REPEAT GEN_TAC 680 THEN STRIP_TAC 681 THEN MP_TAC (SPECL [���v:var���,���FV_subst1 (s:^subs) t���] 682 variant_not_in_set) 683 THEN IMP_RES_THEN REWRITE_THM FINITE_FV_subst1 684 THEN FIRST_ASSUM (REWRITE_THM o SYM) 685 THEN REWRITE_TAC[FV_subst1] 686 THEN REWRITE_TAC[IN_UNION_SET,IN_IMAGE,combinTheory.o_THM] 687 THEN CONV_TAC (DEPTH_CONV NOT_EXISTS_CONV) 688 THEN REWRITE_TAC[DE_MORGAN_THM] 689 THEN CONV_TAC (DEPTH_CONV NOT_EXISTS_CONV) 690 THEN REWRITE_TAC[DE_MORGAN_THM] 691 THEN DISCH_THEN (MP_TAC o SPEC ���FV1 (SUB1 (s:^subs) x)���) 692 THEN STRIP_TAC 693 THEN POP_ASSUM (MP_TAC o SPEC ���x:var���) 694 THEN ASM_REWRITE_TAC[] 695 ); 696 697 698 699(* This next IS TRUE!!! *) 700 701val ALPHA1_SUB = store_thm 702 ("ALPHA1_SUB", 703 ���!t1 t2:'a term1 xs ys. ALPHA1 t1 t2 xs ys ==> 704 (!xs' ys' s1 s2. 705 ALPHA1_subst xs ys xs' ys' (FV1 t1) (FV1 t2) s1 s2 ==> 706 ALPHA1 (t1 <[ s1) (t2 <[ s2) xs' ys')���, 707 rule_induct ALPHA1_strong_ind 708 THEN REWRITE_TAC[FV1_def] 709 THEN REPEAT STRIP_TAC 710 THEN REWRITE_TAC[SUB_term1_def] 711 THEN CONV_TAC (DEPTH_CONV let_CONV) 712 THEN REWRITE_TAC[ALPHA1_term_pos] 713 THEN IMP_RES_TAC ALPHA1_subst_UNION 714 THEN IMP_RES_TAC ALPHA1_subst_LENGTH 715 THEN RES_TAC 716 THEN ASM_REWRITE_TAC[] 717 (* two subgoals left: *) 718 THENL 719 [ UNDISCH_LAST_TAC 720 THEN UNDISCH_LAST_TAC 721 THEN REWRITE_TAC[ALPHA1_subst] 722 THEN REWRITE_TAC[IN] 723 THEN STRIP_TAC 724 THEN ASM_REWRITE_TAC[] 725 THEN POP_ASSUM MATCH_MP_TAC 726 THEN ASM_REWRITE_TAC[], 727 728 POP_TAC 729 THEN UNDISCH_LAST_TAC 730 THEN DEFINE_NEW_VAR 731 ���x' = variant x (FV_subst1 (s1:^subs) 732 (FV1 (u1:'a term1) DIFF {x}))��� 733 THEN FIRST_ASSUM (REWRITE_THM o SYM) 734 THEN DEFINE_NEW_VAR 735 ���y' = variant y (FV_subst1 (s2:^subs) 736 (FV1 (u2:'a term1) DIFF {y}))��� 737 THEN FIRST_ASSUM (REWRITE_THM o SYM) 738 THEN DISCH_TAC 739 THEN FIRST_ASSUM MATCH_MP_TAC 740 THEN UNDISCH_LAST_TAC 741 THEN REWRITE_TAC[ALPHA1_subst] 742 THEN STRIP_TAC 743 THEN UNDISCH_LAST_TAC 744 THEN REWRITE_TAC[LENGTH] 745 THEN FIRST_ASSUM REWRITE_THM 746 THEN DISCH_TAC 747 THEN REPEAT GEN_TAC 748 THEN REWRITE_TAC[alpha_match] 749 THEN REWRITE_TAC[SUB1] 750 THEN COND_CASES_TAC 751 THENL 752 [ POP_ASSUM REWRITE_THM 753 THEN COND_CASES_TAC 754 THEN FIRST_ASSUM REWRITE_THM 755 THEN POP_TAC 756 THEN STRIP_TAC 757 THEN REWRITE_TAC[ALPHA1_term_pos] 758 THEN REWRITE_TAC[alpha_match] 759 THEN FIRST_ASSUM ACCEPT_TAC, 760 761 COND_CASES_TAC 762 THEN FIRST_ASSUM REWRITE_THM (* proves one goal *) 763 THEN STRIP_TAC 764 (* Here the extra x', y' are extraneous *) 765 THEN DEP_REWRITE_TAC[ALPHA1_EXTRANEOUS_CONTEXT] 766 THEN FIRST_ASSUM (MP_TAC o SPECL[���x'':var���,���y'':var���]) 767 THEN REWRITE_TAC[IN_DIFF,IN] 768 THEN DISCH_THEN IMP_RES_TAC 769 THEN FIRST_ASSUM REWRITE_THM 770 THEN CONJ_TAC 771 THEN MATCH_MP_TAC variant_not_in_sub 772 THENL 773 [ EXISTS_TAC ���x:var��� 774 THEN EXISTS_TAC ���FV1 (u1:'a term1) DIFF {x}��� 775 THEN ASM_REWRITE_TAC[IN_DIFF,IN] 776 THEN MATCH_MP_TAC FINITE_DIFF 777 THEN REWRITE_TAC[FINITE_FV1], 778 779 EXISTS_TAC ���y:var��� 780 THEN EXISTS_TAC ���FV1 (u2:'a term1) DIFF {y}��� 781 THEN ASM_REWRITE_TAC[IN_DIFF,IN] 782 THEN MATCH_MP_TAC FINITE_DIFF 783 THEN REWRITE_TAC[FINITE_FV1] 784 ] 785 ] 786 ] 787 ); 788(* Soli Deo Gloria!!! *) 789 790 791 792 793val ALPHA1_CHANGE_VAR = store_thm 794 ("ALPHA1_CHANGE_VAR", 795 ���!y x s v t:'a term1. 796 ~(x IN FV_subst1 s (FV1 t DIFF {v})) /\ 797 ~(y IN FV_subst1 s (FV1 t DIFF {v})) ==> 798 ALPHA1 799 (t <[ CONS (v, Var1 x) s) 800 (t <[ CONS (v, Var1 y) s) 801 [x] [y]���, 802 REWRITE_TAC[FV_subst1] 803 THEN REWRITE_TAC[IN_UNION_SET,IN_IMAGE,o_THM] 804 THEN CONV_TAC (DEPTH_CONV NOT_EXISTS_CONV) 805 THEN REWRITE_TAC[DE_MORGAN_THM] 806 THEN CONV_TAC (DEPTH_CONV NOT_EXISTS_CONV) 807 THEN REWRITE_TAC[DE_MORGAN_THM,IN_DIFF,IN] 808 THEN REPEAT STRIP_TAC 809 THEN MATCH_MP_TAC (REWRITE_RULE[AND_IMP_INTRO] 810 (CONV_RULE (TOP_DEPTH_CONV RIGHT_IMP_FORALL_CONV) 811 ALPHA1_SUB)) 812 THEN EXISTS_TAC ���[]:var list��� 813 THEN EXISTS_TAC ���[]:var list��� 814 THEN REWRITE_TAC[ALPHA1_REFL] 815 THEN REWRITE_TAC[ALPHA1_subst] 816 THEN REWRITE_TAC[LENGTH] 817 THEN REWRITE_TAC[alpha_match] 818 THEN REWRITE_TAC[SUB1] 819 THEN REPEAT GEN_TAC 820 THEN STRIP_TAC 821 THEN POP_ASSUM (REWRITE_ALL_THM o SYM) 822 THEN POP_TAC 823 THEN UNDISCH_LAST_TAC 824 THEN UNDISCH_LAST_TAC 825 THEN POP_ASSUM (STRIP_ASSUME_TAC o SPEC ���FV1 (SUB1 (s:^subs) x')���) 826 THENL 827 [ POP_ASSUM (STRIP_ASSUME_TAC o SPEC ���x':var���) 828 THENL (* 3 subgoals *) 829 [ UNDISCH_LAST_TAC 830 THEN REWRITE_TAC[], 831 832 ASM_REWRITE_TAC[], 833 834 POP_ASSUM (REWRITE_THM o SYM) 835 THEN REPEAT STRIP_TAC 836 THEN REWRITE_TAC[ALPHA1_term_pos,alpha_match] 837 ], 838 839 DISCH_THEN (STRIP_ASSUME_TAC o SPEC ���FV1 (SUB1 (s:^subs) x')���) 840 THENL 841 [ POP_ASSUM (STRIP_ASSUME_TAC o SPEC ���x':var���) 842 THENL (* 3 subgoals *) 843 [ UNDISCH_LAST_TAC 844 THEN REWRITE_TAC[], 845 846 ASM_REWRITE_TAC[], 847 848 POP_ASSUM REWRITE_THM 849 THEN STRIP_TAC 850 THEN REWRITE_TAC[ALPHA1_term_pos,alpha_match] 851 ], 852 853 STRIP_TAC 854 THEN COND_CASES_TAC 855 THENL 856 [ REWRITE_TAC[ALPHA1_term_pos,alpha_match], 857 858 REWRITE_TAC[] 859 THEN DEP_REWRITE_TAC[ALPHA1_EXTRANEOUS_CONTEXT] 860 THEN ASM_REWRITE_TAC[ALPHA1_REFL] 861 ] 862 ] 863 ] 864 ); 865 866 867 868val obj_SUB_distinct = store_thm 869 ("obj_SUB_distinct", 870 ���(!a xs ys x. ~(Con1 a = SUB1 ((xs // ys):^subs) x)) /\ 871 (!t u:'a term1 xs ys x. ~(App1 t u = SUB1 (xs // ys) x)) /\ 872 (!y u:'a term1 xs ys x. ~(Lam1 y u = SUB1 (xs // ys) x)) /\ 873 (!a xs ys x. ~(SUB1 ((xs // ys):^subs) x = Con1 a)) /\ 874 (!t u:'a term1 xs ys x. ~(SUB1 (xs // ys) x = App1 t u)) /\ 875 (!y u:'a term1 xs ys x. ~(SUB1 (xs // ys) x = Lam1 y u))���, 876 REPEAT CONJ_TAC 877 THEN REPEAT GEN_TAC 878 THEN STRIP_ASSUME_TAC (SPEC_ALL SUB_vsubst_Var1) 879 THEN ASM_REWRITE_TAC[term1_distinct2] 880 ); 881 882 883val FREE_SUBST = store_thm 884 ("FREE_SUBST", 885 ���!(t:'a term1) s. DISJOINT (FV1 t) (BV_subst s) ==> ((t <[ s) = t)���, 886 Induct 887 THEN REWRITE_TAC[FV1_def,SUB_term1_def] 888 THEN CONV_TAC (DEPTH_CONV let_CONV) 889 THEN REWRITE_TAC[DISJOINT_UNION,term1_one_one] 890 THEN ASM_REWRITE_TAC[] 891 THEN REPEAT STRIP_TAC 892 THEN RES_TAC 893 THENL 894 [ IMP_RES_TAC FREE_SUB1 895 THEN POP_ASSUM MATCH_MP_TAC 896 THEN REWRITE_TAC[IN], 897 898 IMP_RES_TAC FREE_IDENT_SUBST1 899 THEN POP_ASSUM REWRITE_THM 900 THEN MATCH_MP_TAC variant_ident 901 THEN REWRITE_TAC[IN_DIFF,IN] 902 THEN MATCH_MP_TAC FINITE_DIFF 903 THEN REWRITE_TAC[FINITE_FV1], 904 905 IMP_RES_TAC FREE_IDENT_SUBST1 906 THEN POP_ASSUM REWRITE_THM 907 THEN DEP_REWRITE_TAC[variant_ident] 908 THEN DEP_REWRITE_TAC[FINITE_DIFF] 909 THEN REWRITE_TAC[FINITE_FV1,IN_DIFF,IN] 910 THEN MATCH_MP_TAC subst_IDENT1 911 THEN GEN_TAC 912 THEN DISCH_TAC 913 THEN REWRITE_TAC[SUB1] 914 THEN COND_CASES_TAC 915 THENL 916 [ ASM_REWRITE_TAC[], 917 918 IMP_RES_TAC FREE_SUB1 919 THEN POP_ASSUM MATCH_MP_TAC 920 THEN ASM_REWRITE_TAC[IN_DIFF,IN] 921 ] 922 ] 923 ); 924 925 926val BLOCKED_SUBST = store_thm 927 ("BLOCKED_SUBST", 928 ���!t:'a term1 x u. 929 (Lam1 x u <[ [x,t]) = Lam1 x u���, 930 REPEAT GEN_TAC 931 THEN REWRITE_TAC[SUB_term1_def] 932 THEN DEP_REWRITE_TAC[variant_ident] 933 THEN DEP_REWRITE_TAC[FINITE_FV_subst1] 934 THEN DEP_REWRITE_TAC[FINITE_DIFF] 935 THEN REWRITE_TAC[FINITE_FV1] 936 THEN DEP_REWRITE_TAC[FV_subst_IDENT1] 937 THEN REWRITE_TAC[IN_DIFF,IN] 938 THEN CONJ_TAC 939 THENL 940 [ REPEAT STRIP_TAC 941 THEN REWRITE_TAC[SUB1] 942 THEN FIRST_ASSUM REWRITE_THM, 943 944 CONV_TAC (DEPTH_CONV let_CONV) 945 THEN REWRITE_TAC[term1_one_one] 946 THEN DEP_REWRITE_TAC[subst_IDENT1] 947 THEN REPEAT STRIP_TAC 948 THEN REWRITE_TAC[SUB1] 949 THEN COND_CASES_TAC 950 THEN ASM_REWRITE_TAC[] 951 ] 952 ); 953 954 955val PARTIALLY_BLOCKED_SUBST = store_thm 956 ("PARTIALLY_BLOCKED_SUBST", 957 ���!xs ys x y u:'a term1. 958 (LENGTH xs = LENGTH ys) ==> 959 (Lam1 x u <[ (APPEND xs [x] // APPEND ys [y]) = 960 Lam1 x u <[ (xs // ys))���, 961 REPEAT STRIP_TAC 962 THEN MATCH_MP_TAC (hd (rev (CONJUNCTS subst_EQ1))) 963 THEN REWRITE_TAC[FV1_def,IN_DIFF,IN] 964 THEN REPEAT STRIP_TAC 965 THEN DEP_REWRITE_TAC[SUB_APPEND_vsubst1] 966 THEN ASM_REWRITE_TAC[] 967 THEN COND_CASES_TAC 968 THENL 969 [ REFL_TAC, 970 971 REWRITE_TAC[vsubst1,SUB1] 972 THEN EVERY_ASSUM (REWRITE_THM o GSYM) 973 THEN DEP_REWRITE_TAC[SUB_FREE_vsubst1] 974 THEN ASM_REWRITE_TAC[] 975 ] 976 ); 977 978(* THe following two theorems are unnecessary. 979 980val ALPHA1_DUPLICATE_CONTEXT = store_thm 981 ("ALPHA1_DUPLICATE_CONTEXT", 982 ���!t1 t2:'a term1 x y xs ys. 983 ALPHA1 t1 t2 (CONS x (CONS x xs)) (CONS y (CONS y ys)) = 984 ALPHA1 t1 t2 (CONS x xs) (CONS y ys)���, 985 REPEAT STRIP_TAC 986 THEN MATCH_MP_TAC ALPHA1_FREE_CONTEXT 987 THEN REWRITE_TAC[LENGTH,INV_SUC_EQ] 988 THEN REPEAT STRIP_TAC 989 THEN REWRITE_TAC[vsubst1,SUB1] 990 THEN COND_CASES_TAC 991 THEN REWRITE_TAC[] 992 ); 993 994 995val ALPHA1_INNOCUOUS_SUBST = store_thm 996 ("ALPHA1_INNOCUOUS_SUBST", 997 ���!t:'a term1 x y xs ys. 998 ~(x IN SL ys) /\ 999 ALPHA1 (t <[ (APPEND ys [x] // APPEND xs [y])) t xs ys ==> 1000 ((x = y) \/ ~(x IN FV1 t))���, 1001 Induct 1002 THEN REWRITE_TAC[SUB_term1_def,FV1_def,IN_UNION,IN] 1003 THEN CONV_TAC (DEPTH_CONV let_CONV) 1004 THEN REWRITE_TAC[ALPHA1_term_pos] 1005 THEN REPEAT STRIP_TAC 1006 THEN RES_TAC 1007 THEN ASM_REWRITE_TAC[] 1008 THENL 1009 [ ASM_CASES_TAC ���(x:var) = v��� 1010 THEN ASM_REWRITE_TAC[] 1011 THEN POP_ASSUM (REWRITE_ALL_THM o SYM) 1012 THEN IMP_RES_TAC ALPHA1_LENGTH 1013 THEN POP_ASSUM (fn th1 => 1014 POP_ASSUM (fn th2 => 1015 ASSUME_TAC th1 THEN MP_TAC th2)) 1016 THEN DEP_REWRITE_TAC[SUB_APPEND_FREE_vsubst1] 1017 THEN ASM_REWRITE_TAC[] 1018 THEN REWRITE_TAC[SUB1,vsubst1] 1019 THEN REWRITE_TAC[ALPHA1_term_pos] 1020 THEN REWRITE_TAC[alpha_match_SUB_var] 1021 THEN STRIP_TAC 1022 THEN UNDISCH_LAST_TAC 1023 THEN DEP_REWRITE_TAC[SUB_FREE_vsubst1] 1024 THEN ASM_REWRITE_TAC[term1_one_one], 1025 1026 POP_TAC 1027 THEN UNDISCH_LAST_TAC 1028 THEN DEFINE_NEW_VAR 1029 ���v' = variant v 1030 (FV_subst1 ((APPEND ys [x] // APPEND xs [y]):^subs) 1031 (FV1 (t:'a term1) DIFF {v}))��� 1032 THEN FIRST_ASSUM (REWRITE_THM o SYM) 1033 THEN DISCH_TAC 1034 THEN ASM_CASES_TAC ���(x:var) = v��� 1035 THENL 1036 [ POP_ASSUM REWRITE_THM 1037 THEN REWRITE_TAC[IN_DIFF,IN], 1038 1039 FIRST_ASSUM (MP_TAC o 1040 REWRITE_RULE[SUB1] o 1041 SPECL[���x:var���,���y:var���, 1042 ���CONS (v':var) xs���,���CONS (v:var) ys���]) 1043 THEN REWRITE_TAC[SL,IN] 1044 THEN FIRST_ASSUM REWRITE_THM 1045 THEN UNDISCH_ALL_TAC 1046 THEN DISCH_TAC 1047 THEN POP_TAC 1048 THEN DISCH_TAC 1049 THEN DISCH_TAC 1050 THEN REWRITE_TAC[APPEND,vsubst1] 1051 THEN DISCH_THEN REWRITE_THM 1052 THEN REWRITE_TAC[IN_DIFF,IN,DE_MORGAN_THM] 1053 THEN DISCH_THEN ASM_REWRITE_THM 1054 ] 1055 ] 1056 ); 1057 1058*) 1059 1060 1061 1062val ALPHA1_Var1_pos1 = TAC_PROOF(([], 1063 ���!xs ys x y t:'a term1 v. 1064 ~(x = v) /\ ALPHA1 (Var1 v) t (x::xs) (y::ys) 1065 ==> 1066 ~(t = Var1 y) /\ 1067 ALPHA1 (Var1 v) t xs ys���), 1068 REPEAT GEN_TAC 1069 THEN STRIP_TAC 1070 THEN IMP_RES_TAC ALPHA1_term_similar 1071 THEN POP_ASSUM REWRITE_ALL_THM 1072 THEN UNDISCH_LAST_TAC 1073 THEN POP_ASSUM (ASSUME_TAC o GSYM) 1074 THEN REWRITE_TAC[ALPHA1_term_pos] 1075 THEN REWRITE_TAC[alpha_match] 1076 THEN ASM_REWRITE_TAC[] 1077 THEN REWRITE_TAC[term1_one_one] 1078 ); 1079 1080val ALPHA1_Var1_pos2 = TAC_PROOF(([], 1081 ���!xs ys x y t:'a term1 v. 1082 ~(y = v) /\ ALPHA1 t (Var1 v) (x::xs) (y::ys) 1083 ==> 1084 ~(t = Var1 x) /\ 1085 ALPHA1 t (Var1 v) xs ys���), 1086 ONCE_REWRITE_TAC[ALPHA1_SYM] 1087 THEN REWRITE_TAC[ALPHA1_Var1_pos1] 1088 ); 1089 1090 1091val ALPHA1_SWITCH_Var1 = TAC_PROOF(([], 1092 ���!xs xs' ys ys' x y u v. 1093 (LENGTH xs = LENGTH xs') /\ 1094 (LENGTH xs' = LENGTH ys) /\ 1095 (LENGTH ys = LENGTH ys') /\ 1096 ALPHA1 (SUB1 ((APPEND xs [x] // APPEND xs' [y]) :^subs) u) 1097 (Var1 v) xs' ys /\ 1098 ALPHA1 (Var1 u) 1099 (SUB1 ((APPEND ys [y] // APPEND ys' [x]) :^subs) v) xs ys' 1100 ==> 1101 ALPHA1 ((Var1 u):'a term1) 1102 (Var1 v) (APPEND xs [x]) (APPEND ys [y])���), 1103 LIST_INDUCT_TAC 1104 THENL 1105 [ LIST_INDUCT_TAC 1106 THEN REWRITE_TAC[LENGTH,SUC_NOT] 1107 THEN LIST_INDUCT_TAC 1108 THEN REWRITE_TAC[LENGTH,SUC_NOT] 1109 THEN LIST_INDUCT_TAC 1110 THEN REWRITE_TAC[LENGTH,SUC_NOT] 1111 THEN REWRITE_TAC[APPEND,vsubst1,SUB1] 1112 THEN REPEAT GEN_TAC 1113 THEN COND_CASES_TAC 1114 THEN COND_CASES_TAC 1115 THEN REWRITE_TAC[ALPHA1_term_pos] 1116 THEN REWRITE_TAC[alpha_match_SUB_var] 1117 THEN REWRITE_TAC[vsubst1,SUB1] 1118 THEN ASM_REWRITE_TAC[term1_one_one,LENGTH], 1119 1120 GEN_TAC 1121 THEN LIST_INDUCT_TAC 1122 THEN REWRITE_TAC[LENGTH,NOT_SUC] 1123 THEN POP_TAC 1124 THEN GEN_TAC 1125 THEN LIST_INDUCT_TAC 1126 THEN REWRITE_TAC[LENGTH,NOT_SUC] 1127 THEN POP_TAC 1128 THEN GEN_TAC 1129 THEN LIST_INDUCT_TAC 1130 THEN REWRITE_TAC[LENGTH,NOT_SUC] 1131 THEN POP_TAC 1132 THEN X_GEN_TAC ���x1:var��� 1133 THEN X_GEN_TAC ���x2:var��� 1134 THEN REPEAT GEN_TAC 1135 THEN REWRITE_TAC[INV_SUC_EQ] 1136 THEN STRIP_TAC 1137 THEN UNDISCH_LAST_TAC 1138 THEN UNDISCH_LAST_TAC 1139 THEN REWRITE_TAC[APPEND,vsubst1,SUB1] 1140 THEN COND_CASES_TAC 1141 THEN POP_ASSUM (ASSUME_TAC o GSYM) 1142 THEN COND_CASES_TAC 1143 THEN POP_ASSUM (ASSUME_TAC o GSYM) 1144 THENL (* 4 subgoals *) 1145 [ REWRITE_TAC[ALPHA1_term_pos] 1146 THEN REWRITE_TAC[alpha_match_SUB_var] 1147 THEN ASM_REWRITE_TAC[LENGTH,LENGTH_APPEND,vsubst1,SUB1], 1148 1149 REWRITE_TAC[ALPHA1_term_pos] 1150 THEN REWRITE_TAC[alpha_match_SUB_var] 1151 THEN REWRITE_TAC[vsubst1,SUB1] 1152 THEN ASM_REWRITE_TAC[term1_one_one], 1153 1154 REWRITE_TAC[ALPHA1_term_pos] 1155 THEN REWRITE_TAC[alpha_match_SUB_var] 1156 THEN REWRITE_TAC[vsubst1,SUB1] 1157 THEN ASM_REWRITE_TAC[term1_one_one], 1158 1159 REPEAT STRIP_TAC 1160 THEN IMP_RES_THEN IMP_RES_TAC ALPHA1_Var1_pos1 1161 THEN IMP_RES_THEN IMP_RES_TAC ALPHA1_Var1_pos2 1162 THEN REWRITE_TAC[ALPHA1_term_pos] 1163 THEN REWRITE_TAC[alpha_match] 1164 THEN EVERY_ASSUM (REWRITE_THM o GSYM) 1165 THEN REWRITE_TAC[GSYM ALPHA1_term_pos] 1166 THEN FIRST_ASSUM MATCH_MP_TAC 1167 THEN EXISTS_TAC ���xs':var list��� 1168 THEN EXISTS_TAC ���ys':var list��� 1169 THEN ASM_REWRITE_TAC[] 1170 ] 1171 ] 1172 ); 1173 1174 1175 1176 1177val ALPHA1_SWITCH_LEMMA = TAC_PROOF(([], 1178 ���!t3 t2:'a term1 xs' ys. 1179 ALPHA1 t3 t2 xs' ys ==> 1180 (!t1 x y xs ys'. 1181 (LENGTH xs = LENGTH xs') /\ (LENGTH ys = LENGTH ys') /\ 1182 (t3 = (t1 <[ (APPEND xs [x] // APPEND xs' [y]))) /\ 1183 ALPHA1 t1 (t2 <[ (APPEND ys [y] // APPEND ys' [x])) xs ys' 1184 ==> 1185 ALPHA1 t1 t2 (APPEND xs [x]) (APPEND ys [y]))���), 1186 rule_induct ALPHA1_strong_ind 1187 THEN REPEAT STRIP_TAC 1188 THEN UNDISCH_LAST_TAC 1189 THEN UNDISCH_LAST_TAC 1190 THENL (* 4 subgoals *) 1191 [ STRIP_ASSUME_TAC (SPEC ���t1:'a term1��� term1_cases) 1192 (* four subgoals *) 1193 THEN POP_ASSUM REWRITE_THM 1194 THEN REWRITE_TAC[SUB_term1_def] 1195 THEN CONV_TAC (DEPTH_CONV let_CONV) 1196 THEN REWRITE_TAC[term1_distinct2,obj_SUB_distinct] 1197 (* one subgoal *) 1198 THEN REWRITE_TAC[term1_one_one] 1199 THEN DISCH_THEN (REWRITE_THM o SYM) 1200 THEN REWRITE_TAC[ALPHA1_term_pos] 1201 THEN DISCH_TAC 1202 THEN ASM_REWRITE_TAC[LENGTH_APPEND,LENGTH], 1203 1204 1205 STRIP_ASSUME_TAC (SPEC ���t1:'a term1��� term1_cases) 1206 (* four subgoals *) 1207 THEN POP_ASSUM REWRITE_THM 1208 THEN REWRITE_TAC[SUB_term1_def] 1209 THEN CONV_TAC (DEPTH_CONV let_CONV) 1210 THEN REWRITE_TAC[term1_distinct2] 1211 (* one subgoal *) 1212 THEN REPEAT DISCH_TAC 1213 THEN MATCH_MP_TAC ALPHA1_SWITCH_Var1 1214 THEN EXISTS_TAC ���xs:var list��� 1215 THEN EXISTS_TAC ���ys':var list��� 1216 THEN IMP_RES_TAC alpha_match_LENGTH 1217 THEN ASM_REWRITE_TAC[] 1218 THEN POP_TAC 1219 THEN UNDISCH_LAST_TAC 1220 THEN FIRST_ASSUM (REWRITE_THM o SYM) 1221 THEN ASM_REWRITE_TAC[ALPHA1_term_pos], 1222 1223 1224 STRIP_ASSUME_TAC (SPEC ���t1':'a term1��� term1_cases) 1225 (* four subgoals *) 1226 THEN POP_ASSUM REWRITE_THM 1227 THEN REWRITE_TAC[SUB_term1_def] 1228 THEN CONV_TAC (DEPTH_CONV let_CONV) 1229 THEN REWRITE_TAC[term1_distinct2,obj_SUB_distinct] 1230 (* one subgoal *) 1231 THEN REWRITE_TAC[term1_one_one] 1232 THEN STRIP_TAC 1233 THEN REWRITE_TAC[ALPHA1_term_pos] 1234 THEN STRIP_TAC 1235 THEN RES_TAC 1236 THEN ASM_REWRITE_TAC[], 1237 1238 STRIP_ASSUME_TAC (SPEC ���t1:'a term1��� term1_cases) 1239 (* four subgoals *) 1240 THEN POP_ASSUM REWRITE_THM 1241 THEN REWRITE_TAC[SUB_term1_def] 1242 THEN CONV_TAC (DEPTH_CONV let_CONV) 1243 THEN REWRITE_TAC[term1_distinct2,obj_SUB_distinct] 1244 (* one subgoal *) 1245 THEN REWRITE_TAC[term1_one_one] 1246 THEN STRIP_TAC 1247 THEN REWRITE_TAC[ALPHA1_term_pos] 1248 THEN DISCH_TAC 1249 THEN REWRITE_TAC[GSYM (CONJUNCT2 APPEND)] 1250 THEN FIRST_ASSUM MATCH_MP_TAC 1251 THEN EXISTS_TAC 1252 ���CONS (variant y 1253 (FV_subst1 ((APPEND ys [y'] // APPEND ys' [x']):^subs) 1254 (FV1 (u2:'a term1) DIFF {y}))) 1255 ys'��� 1256 THEN ASM_REWRITE_TAC[LENGTH,APPEND,vsubst1,SL,IN] 1257 ] 1258 ); 1259 1260 1261val ALPHA1_SWITCH = store_thm 1262 ("ALPHA1_SWITCH", 1263 ���!t1 t2:'a term1 xs xs' ys ys' x y. 1264 (LENGTH xs = LENGTH xs') /\ (LENGTH ys = LENGTH ys') /\ 1265 ALPHA1 (t1 <[ (APPEND xs [x] // APPEND xs' [y])) t2 xs' ys /\ 1266 ALPHA1 t1 (t2 <[ (APPEND ys [y] // APPEND ys' [x])) xs ys' 1267 ==> 1268 ALPHA1 t1 t2 (APPEND xs [x]) (APPEND ys [y])���, 1269 REPEAT STRIP_TAC 1270 THEN (MATCH_MP_TAC o 1271 REWRITE_RULE[AND_IMP_INTRO] o 1272 CONV_RULE (TOP_DEPTH_CONV RIGHT_IMP_FORALL_CONV)) 1273 ALPHA1_SWITCH_LEMMA 1274 THEN EXISTS_TAC ���(t1:'a term1) <[ (APPEND xs [x] // APPEND xs' [y])��� 1275 THEN EXISTS_TAC ���xs':var list��� 1276 THEN EXISTS_TAC ���ys':var list��� 1277 THEN ASM_REWRITE_TAC[] 1278 ); 1279 1280 1281val ALPHA1_Lam_subst = store_thm 1282 ("ALPHA1_Lam_subst", 1283 ���!t:'a term1 t1 t2 x y. 1284 ALPHA1 (Lam1 x t1) (Lam1 y t2) [] [] ==> 1285 ALPHA1 (t1 <[ [x, t]) (t2 <[ [y, t]) [] []���, 1286 REWRITE_TAC[ALPHA1_term_pos] 1287 THEN REPEAT GEN_TAC 1288 THEN DISCH_TAC 1289 THEN IMP_RES_TAC ALPHA1_SUB 1290 THEN POP_ASSUM MATCH_MP_TAC 1291 THEN REWRITE_TAC[ALPHA1_subst] 1292 THEN REWRITE_TAC[alpha_match] 1293 THEN REWRITE_TAC[SUB1] 1294 THEN REPEAT GEN_TAC 1295 THEN STRIP_TAC 1296 THEN ASM_REWRITE_TAC[ALPHA1_REFL] 1297 ); 1298 1299 1300val ALPHA1_Lam_one_one = store_thm 1301 ("ALPHA1_Lam_one_one", 1302 ���!t1 t2:'a term1 x y. 1303 ALPHA1 (Lam1 x t1) (Lam1 y t2) [] [] = 1304 (ALPHA1 (t1 <[ [x, Var1 y]) t2 [] [] /\ 1305 ALPHA1 t1 (t2 <[ [y, Var1 x]) [] [])���, 1306 REPEAT GEN_TAC 1307 THEN EQ_TAC 1308 THENL 1309 [ STRIP_TAC 1310 THEN IMP_RES_THEN (MP_TAC o SPEC ���Var1 x :'a term1���) 1311 ALPHA1_Lam_subst 1312 THEN IMP_RES_THEN (MP_TAC o SPEC ���Var1 y :'a term1���) 1313 ALPHA1_Lam_subst 1314 THEN REWRITE_TAC[subst_SAME_ONE1] 1315 THEN REPEAT (DISCH_THEN REWRITE_THM), 1316 1317 REWRITE_TAC[ALPHA1_term_pos] 1318 THEN REPEAT STRIP_TAC 1319 THEN ONCE_REWRITE_TAC[GSYM (CONJUNCT1 APPEND)] 1320 THEN MATCH_MP_TAC ALPHA1_SWITCH 1321 THEN EXISTS_TAC ���[]:var list��� 1322 THEN EXISTS_TAC ���[]:var list��� 1323 THEN ASM_REWRITE_TAC[LENGTH,APPEND,vsubst1] 1324 ] 1325 ); 1326 1327 1328 1329(* ========================================================== *) 1330(* Now we define the alpha-equivalence predicates themselves. *) 1331(* ========================================================== *) 1332 1333 1334val ALPHA = 1335 new_definition ("ALPHA", 1336 ���ALPHA (t1:'a term1) t2 = ALPHA1 t1 t2 [] []���); 1337 1338 1339val ALPHA_term = store_thm 1340 ("ALPHA_term", 1341 ���!t1 t2:'a term1. ALPHA t1 t2 = ALPHA1 t1 t2 [] []���, 1342 REWRITE_TAC[ALPHA] 1343 ); 1344 1345 1346val ALPHA_HEIGHT = store_thm 1347 ("ALPHA_HEIGHT", 1348 ���!t1 t2:'a term1. ALPHA t1 t2 ==> 1349 (HEIGHT1 t1 = HEIGHT1 t2)���, 1350 REWRITE_TAC[ALPHA_term,ALPHA1_HEIGHT] 1351 ); 1352 1353 1354val ALPHA_term_similar = store_thm 1355 ("ALPHA_term_similar", 1356 ���(!a t. ALPHA (Con1 a) t ==> (t = Con1 a :'a term1)) /\ 1357 (!x t. ALPHA (Var1 x) t ==> (?y. t = Var1 y :'a term1)) /\ 1358 (!t1 u1 t. ALPHA (App1 t1 u1) t ==> 1359 (?t2 u2. t = App1 t2 u2 :'a term1)) /\ 1360 (!x1 u1 t. ALPHA (Lam1 x1 u1) t ==> 1361 (?x2 u2. t = Lam1 x2 u2 :'a term1))���, 1362 REWRITE_TAC[ALPHA_term,ALPHA1_term_similar] 1363 ); 1364 1365 1366 1367val ALPHA_REFL = store_thm 1368 ("ALPHA_REFL", 1369 ���!t:'a term1. ALPHA t t���, 1370 REWRITE_TAC[ALPHA_term,ALPHA1_REFL] 1371 ); 1372 1373 1374val ALPHA_SYM = store_thm 1375 ("ALPHA_SYM", 1376 ���!t1 t2:'a term1. ALPHA t1 t2 = ALPHA t2 t1���, 1377 REWRITE_TAC[ALPHA_term] 1378 THEN REPEAT STRIP_TAC 1379 THEN CONV_TAC (RAND_CONV (ONCE_REWRITE_CONV[ALPHA1_SYM])) 1380 THEN REFL_TAC 1381 ); 1382 1383 1384val ALPHA_TRANS = store_thm 1385 ("ALPHA_TRANS", 1386 ���!t1 t2 t3:'a term1. ALPHA t1 t2 /\ ALPHA t2 t3 ==> ALPHA t1 t3���, 1387 REWRITE_TAC[ALPHA_term,ALPHA1_TRANS] 1388 ); 1389 1390 1391val ALPHA_term_pos = store_thm 1392 ("ALPHA_term_pos", 1393 ���(!a b. 1394 ALPHA (Con1 a:'a term1) (Con1 b) = (a = b)) /\ 1395 (!x y. 1396 ALPHA (Var1 x:'a term1) (Var1 y) = (x = y)) /\ 1397 (!t1 t2 u1 u2. 1398 ALPHA (App1 t1 u1:'a term1) (App1 t2 u2) <=> 1399 ALPHA t1 t2 /\ ALPHA u1 u2) (* /\ 1400 (!x1 x2 u1 u2. 1401 ALPHA (Lam1 x1 u1:'a term1) (Lam1 x2 u2) = 1402 ALPHA1 u1 u2 [x1] [x2]) *)���, 1403 REWRITE_TAC[ALPHA_term,ALPHA1_term_pos,alpha_match] 1404 ); 1405 1406 1407val ALPHA_Lam = store_thm 1408 ("ALPHA_Lam", 1409 ���!x u1 u2:'a term1. 1410 ALPHA (Lam1 x u1) (Lam1 x u2) = ALPHA u1 u2���, 1411 REWRITE_TAC[ALPHA_term,ALPHA1_term_pos] 1412 THEN REPEAT GEN_TAC 1413 THEN MATCH_MP_TAC ALPHA1_FREE_CONTEXT 1414 THEN REWRITE_TAC[vsubst1,SUB1] 1415 THEN REPEAT STRIP_TAC 1416 THEN COND_CASES_TAC 1417 THEN ASM_REWRITE_TAC[] 1418 ); 1419 1420 1421val ALPHA_term_neg = store_thm 1422 ("ALPHA_term_neg", 1423 ���(!a x. ALPHA (Con1 a) (Var1 x :'a term1) = F) /\ 1424 (!a t u. ALPHA (Con1 a) (App1 t u :'a term1) = F) /\ 1425 (!a y u. ALPHA (Con1 a) (Lam1 y u :'a term1) = F) /\ 1426 (!x a. ALPHA (Var1 x) (Con1 a :'a term1) = F) /\ 1427 (!x t u. ALPHA (Var1 x) (App1 t u :'a term1) = F) /\ 1428 (!x y u. ALPHA (Var1 x) (Lam1 y u :'a term1) = F) /\ 1429 (!t u a. ALPHA (App1 t u) (Con1 a :'a term1) = F) /\ 1430 (!t u x. ALPHA (App1 t u) (Var1 x :'a term1) = F) /\ 1431 (!t u y v. ALPHA (App1 t u) (Lam1 y v :'a term1) = F) /\ 1432 (!y u a. ALPHA (Lam1 y u) (Con1 a :'a term1) = F) /\ 1433 (!y u x. ALPHA (Lam1 y u) (Var1 x :'a term1) = F) /\ 1434 (!y v t u. ALPHA (Lam1 y v) (App1 t u :'a term1) = F)���, 1435 REWRITE_TAC[ALPHA_term,ALPHA1_term_neg] 1436 ); 1437 1438 1439(* --------------------------------------------------------------------- *) 1440(* We claim that ALPHA is a binary relation on the term language *) 1441(* which is *) 1442(* 1) reflexive *) 1443(* 2) symmetric *) 1444(* 3) transitive *) 1445(* 4) compatible (in the sense of Barendregt, Definition 3.1.1, pg 50 *) 1446(* --------------------------------------------------------------------- *) 1447 1448 1449 1450val ALPHA_FV = store_thm 1451 ("ALPHA_FV", 1452 ���!t1 t2:'a term1. ALPHA t1 t2 ==> (FV1 t1 = FV1 t2)���, 1453 REWRITE_TAC[ALPHA_term] 1454 THEN REPEAT STRIP_TAC 1455 THEN IMP_RES_TAC ALPHA1_SYM 1456 THEN IMP_RES_TAC ALPHA1_FV 1457 THEN POP_ASSUM MP_TAC 1458 THEN POP_ASSUM MP_TAC 1459 THEN REWRITE_TAC[alpha_match_NIL] 1460 THEN REPEAT STRIP_TAC 1461 THEN REWRITE_TAC[EXTENSION] 1462 THEN GEN_TAC 1463 THEN EQ_TAC 1464 THEN DISCH_TAC 1465 THEN RES_TAC 1466 THEN ASM_REWRITE_TAC[] 1467 ); 1468 1469 1470 1471(* 1472val ALPHA1_subst = 1473 new_definition 1474 ("ALPHA1_subst", 1475 ���ALPHA1_subst xs ys xs' ys' t1 t2 s1 (s2:^subs) = 1476 (LENGTH xs' = LENGTH ys') /\ 1477 (!x y. (x IN t1) /\ (y IN t2) /\ 1478 alpha_match xs ys x y ==> 1479 ALPHA1 (SUB1 s1 x) (SUB1 s2 y) xs' ys')���; 1480*) 1481 1482val ALPHA_subst = 1483 new_definition 1484 ("ALPHA_subst", 1485 ���ALPHA_subst t s1 (s2:^subs) = 1486 (!x. (x IN t) ==> 1487 ALPHA (SUB1 s1 x) (SUB1 s2 x))���); 1488 1489 1490val ALPHA_SUB_CONTEXT = store_thm 1491 ("ALPHA_SUB_CONTEXT", 1492 ���!t1 t2:'a term1 s1 s2. 1493 ALPHA t1 t2 /\ 1494 ALPHA_subst (FV1 t1) s1 s2 ==> 1495 ALPHA (t1 <[ s1) (t2 <[ s2)���, 1496 REPEAT STRIP_TAC 1497 THEN IMP_RES_TAC ALPHA_FV 1498 THEN REWRITE_ALL_TAC[ALPHA_term] 1499 THEN (MATCH_MP_TAC o REWRITE_RULE[AND_IMP_INTRO] o 1500 CONV_RULE (TOP_DEPTH_CONV RIGHT_IMP_FORALL_CONV)) 1501 ALPHA1_SUB 1502 THEN EXISTS_TAC ���[]:var list��� 1503 THEN EXISTS_TAC ���[]:var list��� 1504 THEN ASM_REWRITE_TAC[] 1505 THEN UNDISCH_ALL_TAC 1506 THEN REWRITE_TAC[ALPHA_subst,ALPHA1_subst] 1507 THEN REWRITE_TAC[ALPHA_term,alpha_match] 1508 THEN REPEAT STRIP_TAC 1509 THEN ASM_REWRITE_TAC[] 1510 THEN FIRST_ASSUM MATCH_MP_TAC 1511 THEN ASM_REWRITE_TAC[] 1512 ); 1513 1514 1515val ALPHA_SUB = store_thm 1516 ("ALPHA_SUB", 1517 ���!t1 t2 s:^subs. ALPHA t1 t2 ==> 1518 ALPHA (t1 <[ s) (t2 <[ s)���, 1519 REPEAT STRIP_TAC 1520 THEN MATCH_MP_TAC ALPHA_SUB_CONTEXT 1521 THEN ASM_REWRITE_TAC[ALPHA_subst,ALPHA_REFL] 1522 ); 1523 1524 1525 1526val ALPHA_CHANGE_VAR = store_thm 1527 ("ALPHA_CHANGE_VAR", 1528 ���!y x s:^subs v t:'a term1. 1529 ~(x IN FV_subst1 s (FV1 t DIFF {v})) /\ 1530 ~(y IN FV_subst1 s (FV1 t DIFF {v})) ==> 1531 ALPHA (Lam1 x (t <[ CONS (v, Var1 x) s)) 1532 (Lam1 y (t <[ CONS (v, Var1 y) s))���, 1533 REPEAT STRIP_TAC 1534 THEN REWRITE_TAC[ALPHA_term,ALPHA1_term_pos] 1535 THEN MATCH_MP_TAC ALPHA1_CHANGE_VAR 1536 THEN ASM_REWRITE_TAC[] 1537 ); 1538 1539 1540val ALPHA_CHANGE_ONE_VAR = store_thm 1541 ("ALPHA_CHANGE_ONE_VAR", 1542 ���!x v t:'a term1. 1543 ~(x IN (FV1 t DIFF {v})) ==> 1544 ALPHA (Lam1 x (t <[ [v, Var1 x])) 1545 (Lam1 v t)���, 1546 REPEAT STRIP_TAC 1547 THEN MP_TAC (SPECL [���v:var���,���x:var���,���[]:^subs���, 1548 ���v:var���,���t:'a term1���] 1549 ALPHA_CHANGE_VAR) 1550 THEN REWRITE_TAC[FV_subst_NIL1] 1551 THEN UNDISCH_ALL_TAC 1552 THEN REWRITE_TAC[IN_DIFF,IN] 1553 THEN DISCH_THEN REWRITE_THM 1554 THEN DEP_ONCE_REWRITE_TAC[SPECL[���t:'a term1���,���[v,Var1 v:'a term1]���] 1555 subst_IDENT1] 1556 THEN GEN_TAC 1557 THEN REWRITE_TAC[SUB1] 1558 THEN COND_CASES_TAC 1559 THEN ASM_REWRITE_TAC[] 1560 ); 1561 1562 1563val ALPHA_SWITCH = store_thm 1564 ("ALPHA_SWITCH", 1565 ���!t1 t2:'a term1 x y. 1566 ALPHA (t1 <[ [x,Var1 y]) t2 /\ 1567 ALPHA t1 (t2 <[ [y,Var1 x]) 1568 ==> 1569 ALPHA1 t1 t2 [x] [y]���, 1570 REWRITE_TAC[ALPHA_term] 1571 THEN REPEAT STRIP_TAC 1572 THEN ONCE_REWRITE_TAC[GSYM (CONJUNCT1 APPEND)] 1573 THEN MATCH_MP_TAC ALPHA1_SWITCH 1574 THEN EXISTS_TAC ���[]:var list��� 1575 THEN EXISTS_TAC ���[]:var list��� 1576 THEN ASM_REWRITE_TAC[APPEND,vsubst1] 1577 ); 1578 1579 1580val ALPHA_Lam_one_one = store_thm 1581 ("ALPHA_Lam_one_one", 1582 ���!t1 t2:'a term1 x y. 1583 ALPHA (Lam1 x t1) (Lam1 y t2) = 1584 (ALPHA (t1 <[ [x, Var1 y]) t2 /\ 1585 ALPHA t1 (t2 <[ [y, Var1 x]))���, 1586 REWRITE_TAC[ALPHA_term,ALPHA1_Lam_one_one] 1587 ); 1588 1589val ALPHA_Lam_subst = store_thm 1590 ("ALPHA_Lam_subst", 1591 ���!t1 t2 x y t:'a term1. 1592 ALPHA (Lam1 x t1) (Lam1 y t2) ==> 1593 (ALPHA (t1 <[ [x, t]) (t2 <[ [y, t]))���, 1594 REWRITE_TAC[ALPHA_term,ALPHA1_Lam_subst] 1595 ); 1596 1597 1598 1599val _ = export_theory(); 1600 1601val _ = print_theory_to_file "-" "alpha.lst"; 1602 1603val _ = html_theory "alpha"; 1604 1605val _ = print_theory_size(); 1606