1open HolKernel Parse boolLib; 2infix THEN THENL THENC ORELSE ORELSEC THEN_TCL ORELSE_TCL ## |->; 3infixr -->; 4 5 6(* --------------------------------------------------------------------- *) 7(* Building the definitions of alpha equivalence for object expressions. *) 8(* --------------------------------------------------------------------- *) 9 10 11val _ = new_theory "alpha"; 12val _ = ParseExtras.temp_loose_equality() 13 14 15open prim_recTheory pairTheory pairLib listTheory; 16open combinTheory; 17open pred_setTheory; 18open numTheory; 19open arithmeticTheory; 20open bossLib; 21open Mutual; 22open ind_rel; 23open dep_rewrite; 24open more_listTheory; 25open more_setTheory; 26open variableTheory; 27open objectTheory; 28 29open tactics; 30 31 32 33val vars = ty_antiq( ==`:var list`== ); 34val subs1 = ty_antiq( ==`:(var # obj1) list`== ); 35val dict1 = ty_antiq( ==`:(string # method1) list`== ); 36val entry1 = ty_antiq( ==`:string # method1`== ); 37 38 39 40(* --------------------------------------------------------------------- *) 41(* Define semantics for objects, methods, and method dictionaries. *) 42(* --------------------------------------------------------------------- *) 43 44(* Here is the syntax, repeated for clarity: 45 46val _ = Hol_datatype 47 48 (* obj1 ::= x | [li=mi] i in 1..n | a.l | a.l:=m *) 49 50 ` obj1 = OVAR1 of var 51 | OBJ1 of (string # method1) list 52 | INVOKE1 of obj1 => string 53 | UPDATE1 of obj1 => string => method1 ; 54 55 (* method ::= sigma(x)b *) 56 57 method1 = SIGMA1 of var => obj1 ` ; 58 59*) 60 61 62(* ---------------------------------------------------------------------- *) 63(* To define alpha equivalence between objects, we first need to define a *) 64(* matching function, that checks if a pair of variables match according *) 65(* to a given pair of lists of variables; the lists are searched, and *) 66(* the variables must each be found at the same place. *) 67(* ---------------------------------------------------------------------- *) 68 69val alpha_match_def = Define 70 `(alpha_match NIL ys x1 y1 = (if ys = [] then (x1 = y1) else F)) /\ 71 (alpha_match (CONS (x:var) xs) ys x1 y1 = 72 (if ys = [] then F else 73 (if x1 = x then (y1 = HD ys) /\ (LENGTH xs = LENGTH (TL ys)) else 74 (if y1 = HD ys then F else 75 alpha_match xs (TL ys) x1 y1))))`; 76 77val alpha_match = store_thm 78 ("alpha_match", 79 ���(!x1 y1. alpha_match [] [] x1 y1 = (x1 = y1)) /\ 80 (!ys y x1 y1. alpha_match [] (CONS y ys) x1 y1 = F) /\ 81 (!xs x x1 y1. alpha_match (CONS x xs) [] x1 y1 = F) /\ 82 (!xs ys x y x1 y1. alpha_match (CONS x xs) (CONS y ys) x1 y1 = 83 (((x1 = x) /\ (y1 = y) 84 /\ (LENGTH xs = LENGTH ys)) \/ 85 (~(x1 = x) /\ ~(y1 = y) 86 /\ alpha_match xs ys x1 y1)))���, 87 REWRITE_TAC[alpha_match_def] 88 THEN REWRITE_TAC[NOT_CONS_NIL] 89 THEN REWRITE_TAC[HD,TL] 90 THEN REPEAT GEN_TAC 91 THEN COND_CASES_TAC 92 THENL 93 [ REWRITE_TAC[], 94 95 COND_CASES_TAC 96 THEN ASM_REWRITE_TAC[] 97 ] 98 ); 99 100val alpha_match_NIL = store_thm 101 ("alpha_match_NIL", 102 ���alpha_match [] [] = $=���, 103 EXT_TAC ���x:var��� 104 THEN GEN_TAC 105 THEN EXT_TAC ���y:var��� 106 THEN GEN_TAC 107 THEN REWRITE_TAC[alpha_match] 108 ); 109 110val alpha_match_REFL = store_thm 111 ("alpha_match_REFL", 112 ���!xs x. alpha_match xs xs x x���, 113 LIST_INDUCT_TAC 114 THEN ASM_REWRITE_TAC[alpha_match] 115 THEN REWRITE_TAC[EXCLUDED_MIDDLE] 116 ); 117 118val alpha_match_SYM = store_thm 119 ("alpha_match_SYM", 120 ���!xs ys x1 y1. alpha_match xs ys x1 y1 = alpha_match ys xs y1 x1���, 121 LIST_INDUCT_TAC 122 THEN REWRITE_TAC[alpha_match] 123 THENL 124 [ LIST_INDUCT_TAC 125 THEN REWRITE_TAC[alpha_match] 126 THEN REPEAT GEN_TAC 127 THEN CONV_TAC (RAND_CONV (ONCE_REWRITE_CONV[EQ_SYM_EQ])) 128 THEN REFL_TAC, 129 130 GEN_TAC 131 THEN LIST_INDUCT_TAC 132 THEN REWRITE_TAC[alpha_match] 133 THEN REPEAT GEN_TAC 134 THEN ASM_REWRITE_TAC[] 135 THEN EQ_TAC 136 THEN STRIP_TAC 137 THEN ASM_REWRITE_TAC[] 138 ] 139 ); 140 141val alpha_match_TRANS = store_thm 142 ("alpha_match_TRANS", 143 ���!xs ys zs x y z. alpha_match xs ys x y /\ alpha_match ys zs y z 144 ==> alpha_match xs zs x z���, 145 LIST_INDUCT_TAC 146 THENL 147 [ LIST_INDUCT_TAC 148 THENL 149 [ LIST_INDUCT_TAC 150 THEN REWRITE_TAC[alpha_match] 151 THEN REWRITE_TAC[EQ_TRANS], 152 153 REWRITE_TAC[alpha_match] 154 ], 155 156 GEN_TAC 157 THEN LIST_INDUCT_TAC 158 THEN REWRITE_TAC[alpha_match] 159 THEN GEN_TAC 160 THEN LIST_INDUCT_TAC 161 THEN REWRITE_TAC[alpha_match] 162 THEN REPEAT GEN_TAC 163 THEN STRIP_TAC 164 THEN ASM_REWRITE_TAC[] 165 THEN RES_TAC 166 ] 167 ); 168 169 170val alpha_match_SUB_var = store_thm 171 ("alpha_match_SUB_var", 172 ���!xs ys x y. alpha_match xs ys x y = 173 ((LENGTH xs = LENGTH ys) /\ 174 (SUB1 (xs // ys) x = OVAR1 y) /\ 175 (SUB1 (ys // xs) y = OVAR1 x))���, 176 LIST_INDUCT_TAC 177 THENL 178 [ LIST_INDUCT_TAC 179 THEN REWRITE_TAC[alpha_match,vsubst1,SUB1,object1_one_one, 180 LENGTH, GSYM NOT_SUC] 181 THEN REPEAT GEN_TAC 182 THEN EQ_TAC 183 THEN REPEAT STRIP_TAC 184 THEN ASM_REWRITE_TAC[], 185 186 GEN_TAC 187 THEN LIST_INDUCT_TAC 188 THEN REWRITE_TAC[alpha_match,vsubst1,SUB1,object1_one_one, 189 LENGTH, NOT_SUC] 190 THEN REPEAT GEN_TAC 191 THEN ASM_REWRITE_TAC[prim_recTheory.INV_SUC_EQ] 192 THEN COND_CASES_TAC (* (x'' = x)? *) 193 THENL 194 [ POP_ASSUM REWRITE_THM 195 THEN REWRITE_TAC[object1_one_one] 196 THEN COND_CASES_TAC (* (x' = y)? *) 197 THENL 198 [ POP_ASSUM REWRITE_THM, 199 200 POP_ASSUM (REWRITE_THM o GSYM) 201 ], 202 203 FIRST_ASSUM (REWRITE_THM o GSYM) 204 THEN COND_CASES_TAC (* (x' = y)? *) 205 THENL 206 [ POP_ASSUM (REWRITE_THM o SYM) 207 THEN REWRITE_TAC[object1_one_one] 208 THEN FIRST_ASSUM (REWRITE_THM o GSYM), 209 210 REWRITE_TAC[] 211 ] 212 ] 213 ] 214 ); 215 216 217val alpha_match_IDENT = store_thm 218 ("alpha_match_IDENT", 219 ���!xs x y. alpha_match xs xs x y = (x = y)���, 220 LIST_INDUCT_TAC 221 THENL 222 [ REWRITE_TAC[alpha_match], 223 224 ASM_REWRITE_TAC[alpha_match] 225 THEN REPEAT GEN_TAC 226 THEN EQ_TAC 227 THENL 228 [ STRIP_TAC 229 THEN ASM_REWRITE_TAC[], 230 231 DISCH_THEN REWRITE_THM 232 THEN REWRITE_TAC[EXCLUDED_MIDDLE] 233 ] 234 ] 235 ); 236 237 238val alpha_match_NOT_EQ = store_thm 239 ("alpha_match_NOT_EQ", 240 ���!xs ys x y x' y'. 241 alpha_match (CONS x xs) (CONS y ys) x' y' /\ ~(x' = x) 242 ==> alpha_match xs ys x' y' /\ ~(y' = y)���, 243 REPEAT GEN_TAC 244 THEN REWRITE_TAC[alpha_match_SUB_var] 245 THEN REWRITE_TAC[LENGTH,INV_SUC_EQ,vsubst1,SUB1] 246 THEN STRIP_TAC 247 THEN ASM_REWRITE_TAC[] 248 THEN POP_ASSUM (fn th => REWRITE_ALL_TAC[th] THEN MP_TAC th) 249 THEN POP_ASSUM MP_TAC 250 THEN COND_CASES_TAC 251 THENL 252 [ REWRITE_TAC[object1_one_one] 253 THEN DISCH_THEN REWRITE_THM, 254 255 DISCH_TAC 256 THEN ASM_REWRITE_TAC[] 257 ] 258 ); 259 260 261val alpha_match_pair = store_thm 262 ("alpha_match_pair", 263 ���!xs ys x1 y1 x2 y2. 264 alpha_match xs ys x1 y1 /\ 265 alpha_match xs ys x2 y2 ==> 266 ((x1 = x2) = (y1 = y2))���, 267 LIST_INDUCT_TAC 268 THENL 269 [ LIST_INDUCT_TAC 270 THEN REWRITE_TAC[alpha_match] 271 THEN REPEAT STRIP_TAC 272 THEN ASM_REWRITE_TAC[], 273 274 GEN_TAC 275 THEN LIST_INDUCT_TAC 276 THEN REWRITE_TAC[alpha_match] 277 THEN POP_ASSUM (fn th => ALL_TAC) 278 THEN REPEAT STRIP_TAC (* 4 subgoals *) 279 THEN ASM_REWRITE_TAC[] 280 THEN ASSUM_LIST (EVERY o (map (REWRITE_THM o GSYM))) 281 THEN RES_TAC 282 ] 283 ); 284 285val alpha_match_LENGTH = store_thm 286 ("alpha_match_LENGTH", 287 ���!xs ys x y. alpha_match xs ys x y ==> (LENGTH xs = LENGTH ys)���, 288 LIST_INDUCT_TAC 289 THENL 290 [ LIST_INDUCT_TAC 291 THEN REWRITE_TAC[alpha_match], 292 293 GEN_TAC 294 THEN LIST_INDUCT_TAC 295 THEN REWRITE_TAC[alpha_match] 296 THEN POP_TAC 297 THEN REPEAT STRIP_TAC (* 2 subgoals *) 298 THEN RES_TAC 299 THEN ASM_REWRITE_TAC[LENGTH] 300 ] 301 ); 302 303 304 305(* --------------------------------------------------------------------- *) 306(* Definition of equivalence between objects. *) 307(* --------------------------------------------------------------------- *) 308 309val ALPHA1_obj = 310���ALPHA1_obj : obj1 -> obj1 -> ^vars -> ^vars -> bool���; 311val ALPHA1_dict = 312���ALPHA1_dict : ^dict1 -> ^dict1 -> ^vars -> ^vars -> bool���; 313val ALPHA1_entry = 314���ALPHA1_entry : ^entry1 -> ^entry1 -> ^vars -> ^vars -> bool���; 315val ALPHA1_method = 316���ALPHA1_method : method1 -> method1 -> ^vars -> ^vars -> bool���; 317 318val ALPHA1_patterns = [���^ALPHA1_obj o1 o2 xs ys���, 319 ���^ALPHA1_dict d1 d2 xs ys���, 320 ���^ALPHA1_entry e1 e2 xs ys���, 321 ���^ALPHA1_method m1 m2 xs ys��� 322 ]; 323 324val ALPHA1_rules_tm = 325��� 326 (alpha_match xs ys x y 327 (* -------------------------------------------- *) ==> 328 (^ALPHA1_obj (OVAR1 x) (OVAR1 y) xs ys)) /\ 329 330 331 ((^ALPHA1_dict d1 d2 xs ys) 332 (* -------------------------------------------- *) ==> 333 (^ALPHA1_obj (OBJ1 d1) (OBJ1 d2) xs ys)) /\ 334 335 336 ((^ALPHA1_obj o1 o2 xs ys) 337 (* -------------------------------------------- *) ==> 338 (^ALPHA1_obj (INVOKE1 o1 l) (INVOKE1 o2 l) xs ys)) /\ 339 340 341 ((^ALPHA1_obj o1 o2 xs ys) /\ (^ALPHA1_method m1 m2 xs ys) 342 (* -------------------------------------------- *) ==> 343 (^ALPHA1_obj (UPDATE1 o1 l m1) (UPDATE1 o2 l m2) xs ys)) /\ 344 345 346 ((^ALPHA1_entry e1 e2 xs ys) /\ (^ALPHA1_dict d1 d2 xs ys) 347 (* -------------------------------------------- *) ==> 348 (^ALPHA1_dict (CONS e1 d1) (CONS e2 d2) xs ys)) /\ 349 350 351 ((LENGTH xs = LENGTH ys) 352 (* -------------------------------------------- *) ==> 353 (^ALPHA1_dict NIL NIL xs ys)) /\ 354 355 356 ((^ALPHA1_method m1 m2 xs ys) 357 (* -------------------------------------------- *) ==> 358 (^ALPHA1_entry (l,m1) (l,m2) xs ys)) /\ 359 360(* Alpha conversion: *) 361 362 ((^ALPHA1_obj o1 o2 (CONS x xs) (CONS y ys)) 363 (* -------------------------------------------- *) ==> 364 (^ALPHA1_method (SIGMA1 x o1) (SIGMA1 y o2) xs ys)) 365���; 366 367val (ALPHA1_rules_sat,ALPHA1_ind_thm) = 368 define_inductive_relations ALPHA1_patterns ALPHA1_rules_tm; 369 370val ALPHA1_inv_thms = prove_inversion_theorems 371 ALPHA1_rules_sat ALPHA1_ind_thm; 372 373val ALPHA1_strong_ind = prove_strong_induction 374 ALPHA1_rules_sat ALPHA1_ind_thm; 375 376val _ = save_thm ("ALPHA1_rules_sat", ALPHA1_rules_sat); 377val _ = save_thm ("ALPHA1_ind_thm", ALPHA1_ind_thm); 378val _ = save_thm ("ALPHA1_inv_thms", LIST_CONJ ALPHA1_inv_thms); 379val _ = save_thm ("ALPHA1_strong_ind", ALPHA1_strong_ind); 380 381 382val [ALPHA1_OVAR1, ALPHA1_OBJ1, ALPHA1_INVOKE1, ALPHA1_UPDATE1, 383 ALPHA1_CONS, ALPHA1_NIL, ALPHA1_PAIR, ALPHA1_SIGMA1] 384 = CONJUNCTS ALPHA1_rules_sat; 385 386 387 388val ALPHA1_REFL = store_thm 389 ("ALPHA1_REFL", 390 ���(!a xs. ALPHA1_obj a a xs xs) /\ 391 (!d xs. ALPHA1_dict d d xs xs) /\ 392 (!e xs. ALPHA1_entry e e xs xs) /\ 393 (!m xs. ALPHA1_method m m xs xs)���, 394 MUTUAL_INDUCT_THEN obj1_induction ASSUME_TAC 395 THEN REPEAT GEN_TAC 396 THENL (* 8 subgoals *) 397 [ MATCH_MP_TAC ALPHA1_OVAR1 398 THEN REWRITE_TAC[alpha_match_REFL], 399 400 MATCH_MP_TAC ALPHA1_OBJ1 401 THEN ASM_REWRITE_TAC[], 402 403 MATCH_MP_TAC ALPHA1_INVOKE1 404 THEN ASM_REWRITE_TAC[], 405 406 MATCH_MP_TAC ALPHA1_UPDATE1 407 THEN ASM_REWRITE_TAC[], 408 409 MATCH_MP_TAC ALPHA1_SIGMA1 410 THEN ASM_REWRITE_TAC[], 411 412 MATCH_MP_TAC ALPHA1_NIL 413 THEN ASM_REWRITE_TAC[], 414 415 MATCH_MP_TAC ALPHA1_CONS 416 THEN ASM_REWRITE_TAC[], 417 418 MATCH_MP_TAC ALPHA1_PAIR 419 THEN ASM_REWRITE_TAC[] 420 ] 421 ); 422 423 424val ALPHA1_IMP_SYM = TAC_PROOF(([], 425 ���(!o1 o2 xs ys. ALPHA1_obj o1 o2 xs ys ==> 426 ALPHA1_obj o2 o1 ys xs) /\ 427 (!d1 d2 xs ys. ALPHA1_dict d1 d2 xs ys ==> 428 ALPHA1_dict d2 d1 ys xs) /\ 429 (!e1 e2 xs ys. ALPHA1_entry e1 e2 xs ys ==> 430 ALPHA1_entry e2 e1 ys xs) /\ 431 (!m1 m2 xs ys. ALPHA1_method m1 m2 xs ys ==> 432 ALPHA1_method m2 m1 ys xs)���), 433 rule_induct ALPHA1_strong_ind 434 THEN REPEAT STRIP_TAC 435 THENL (* 8 subgoals *) 436 [ MATCH_MP_TAC ALPHA1_OVAR1 437 THEN IMP_RES_TAC alpha_match_SYM, 438 439 MATCH_MP_TAC ALPHA1_OBJ1 440 THEN ASM_REWRITE_TAC[], 441 442 MATCH_MP_TAC ALPHA1_INVOKE1 443 THEN ASM_REWRITE_TAC[], 444 445 MATCH_MP_TAC ALPHA1_UPDATE1 446 THEN ASM_REWRITE_TAC[], 447 448 MATCH_MP_TAC ALPHA1_CONS 449 THEN ASM_REWRITE_TAC[], 450 451 MATCH_MP_TAC ALPHA1_NIL 452 THEN ASM_REWRITE_TAC[], 453 454 MATCH_MP_TAC ALPHA1_PAIR 455 THEN ASM_REWRITE_TAC[], 456 457 MATCH_MP_TAC ALPHA1_SIGMA1 458 THEN ASM_REWRITE_TAC[] 459 ] 460 ); 461 462val ALPHA1_SYM = store_thm 463 ("ALPHA1_SYM", 464 ���(!o1 o2 xs ys. ALPHA1_obj o1 o2 xs ys = 465 ALPHA1_obj o2 o1 ys xs) /\ 466 (!d1 d2 xs ys. ALPHA1_dict d1 d2 xs ys = 467 ALPHA1_dict d2 d1 ys xs) /\ 468 (!e1 e2 xs ys. ALPHA1_entry e1 e2 xs ys = 469 ALPHA1_entry e2 e1 ys xs) /\ 470 (!m1 m2 xs ys. ALPHA1_method m1 m2 xs ys = 471 ALPHA1_method m2 m1 ys xs)���, 472 REPEAT STRIP_TAC 473 THEN EQ_TAC 474 THEN STRIP_TAC 475 THEN IMP_RES_TAC ALPHA1_IMP_SYM 476 ); 477 478 479val ALPHA1_TRANS1 = TAC_PROOF(([], 480 ���(!o1 o2 xs ys. ALPHA1_obj o1 o2 xs ys ==> 481 !o3 zs. ALPHA1_obj o2 o3 ys zs ==> 482 ALPHA1_obj o1 o3 xs zs) /\ 483 (!d1 d2 xs ys. ALPHA1_dict d1 d2 xs ys ==> 484 !d3 zs. ALPHA1_dict d2 d3 ys zs ==> 485 ALPHA1_dict d1 d3 xs zs) /\ 486 (!e1 e2 xs ys. ALPHA1_entry e1 e2 xs ys ==> 487 !e3 zs. ALPHA1_entry e2 e3 ys zs ==> 488 ALPHA1_entry e1 e3 xs zs) /\ 489 (!m1 m2 xs ys. ALPHA1_method m1 m2 xs ys ==> 490 !m3 zs. ALPHA1_method m2 m3 ys zs ==> 491 ALPHA1_method m1 m3 xs zs)���), 492 rule_induct ALPHA1_strong_ind 493 THEN REPEAT CONJ_TAC 494 THEN REPEAT GEN_TAC 495 THEN STRIP_TAC 496 THEN ONCE_REWRITE_TAC ALPHA1_inv_thms 497 THEN REWRITE_TAC[object1_one_one,object1_distinct] 498 THEN REPEAT CONJ_TAC 499 THEN REPEAT GEN_TAC 500 THEN STRIP_TAC 501 THENL (* 9 subgoals *) 502 [ UNDISCH_THEN���(y:var) = x'��� REWRITE_ALL_THM 503 THEN UNDISCH_THEN ���o3 = OVAR1 y'��� REWRITE_ALL_THM 504 THEN REWRITE_TAC[object1_one_one] 505 THEN EXISTS_TAC ���x:var��� 506 THEN EXISTS_TAC ���y':var��� 507 THEN REWRITE_TAC[] 508 THEN IMP_RES_TAC alpha_match_TRANS, 509 510 UNDISCH_THEN ���(d2:^dict1) = d1'��� REWRITE_ALL_THM 511 THEN UNDISCH_THEN ���o3 = OBJ1 d2'��� REWRITE_ALL_THM 512 THEN REWRITE_TAC[object1_one_one] 513 THEN EXISTS_TAC ���d1:^dict1��� 514 THEN EXISTS_TAC ���d2':^dict1��� 515 THEN REWRITE_TAC[] 516 THEN RES_TAC, 517 518 UNDISCH_THEN ���(o2:obj1) = o1'��� REWRITE_ALL_THM 519 THEN UNDISCH_THEN ���(l:string) = l'��� REWRITE_ALL_THM 520 THEN UNDISCH_THEN ���o3 = INVOKE1 o2' l'��� REWRITE_ALL_THM 521 THEN REWRITE_TAC[object1_one_one] 522 THEN EXISTS_TAC ���o1:obj1��� 523 THEN EXISTS_TAC ���l':string��� 524 THEN EXISTS_TAC ���o2':obj1��� 525 THEN REWRITE_TAC[] 526 THEN RES_TAC, 527 528 UNDISCH_THEN ���(o2:obj1) = o1'��� REWRITE_ALL_THM 529 THEN UNDISCH_THEN ���(l:string) = l'��� REWRITE_ALL_THM 530 THEN UNDISCH_THEN ���(m2:method1) = m1'��� REWRITE_ALL_THM 531 THEN UNDISCH_THEN ���o3 = UPDATE1 o2' l' m2'��� REWRITE_ALL_THM 532 THEN REWRITE_TAC[object1_one_one] 533 THEN EXISTS_TAC ���o1:obj1��� 534 THEN EXISTS_TAC ���l':string��� 535 THEN EXISTS_TAC ���m1:method1��� 536 THEN EXISTS_TAC ���o2':obj1��� 537 THEN EXISTS_TAC ���m2':method1��� 538 THEN REWRITE_TAC[] 539 THEN RES_TAC 540 THEN ASM_REWRITE_TAC[], 541 542 UNDISCH_THEN ���(e2:^entry1) = e1'��� REWRITE_ALL_THM 543 THEN UNDISCH_THEN ���(d2:^dict1) = d1'��� REWRITE_ALL_THM 544 THEN UNDISCH_THEN ���d3 = CONS (e2':^entry1) d2'��� REWRITE_ALL_THM 545 THEN REWRITE_TAC[object1_one_one] 546 THEN EXISTS_TAC ���e1:^entry1��� 547 THEN EXISTS_TAC ���d1:^dict1��� 548 THEN EXISTS_TAC ���e2':^entry1��� 549 THEN EXISTS_TAC ���d2':^dict1��� 550 THEN REWRITE_TAC[] 551 THEN RES_TAC 552 THEN ASM_REWRITE_TAC[], 553 554 ASM_REWRITE_TAC[], 555 556 UNDISCH_THEN ���(l:string) = l'��� REWRITE_ALL_THM 557 THEN UNDISCH_THEN ���(m2:method1) = m1'��� REWRITE_ALL_THM 558 THEN UNDISCH_THEN ���(e3:^entry1) = (l',m2')��� REWRITE_ALL_THM 559 THEN REWRITE_TAC[object1_one_one] 560 THEN EXISTS_TAC ���l':string��� 561 THEN EXISTS_TAC ���m1:method1��� 562 THEN EXISTS_TAC ���m2':method1��� 563 THEN REWRITE_TAC[] 564 THEN RES_TAC, 565 566 UNDISCH_THEN ���(y:var) = x'��� REWRITE_ALL_THM 567 THEN UNDISCH_THEN ���(o2:obj1) = o1'��� REWRITE_ALL_THM 568 THEN UNDISCH_THEN ���m3 = SIGMA1 y' o2'��� REWRITE_ALL_THM 569 THEN REWRITE_TAC[object1_one_one] 570 THEN EXISTS_TAC ���x:var��� 571 THEN EXISTS_TAC ���o1:obj1��� 572 THEN EXISTS_TAC ���y':var��� 573 THEN EXISTS_TAC ���o2':obj1��� 574 THEN REWRITE_TAC[] 575 THEN RES_TAC 576 ] 577 ); 578 579 580val ALPHA1_TRANS = store_thm 581 ("ALPHA1_TRANS", 582 ���(!o1 o2 o3 xs ys zs. ALPHA1_obj o1 o2 xs ys /\ 583 ALPHA1_obj o2 o3 ys zs ==> 584 ALPHA1_obj o1 o3 xs zs) /\ 585 (!d1 d2 d3 xs ys zs. ALPHA1_dict d1 d2 xs ys /\ 586 ALPHA1_dict d2 d3 ys zs ==> 587 ALPHA1_dict d1 d3 xs zs) /\ 588 (!e1 e2 e3 xs ys zs. ALPHA1_entry e1 e2 xs ys /\ 589 ALPHA1_entry e2 e3 ys zs ==> 590 ALPHA1_entry e1 e3 xs zs) /\ 591 (!m1 m2 m3 xs ys zs. ALPHA1_method m1 m2 xs ys /\ 592 ALPHA1_method m2 m3 ys zs ==> 593 ALPHA1_method m1 m3 xs zs)���, 594 REPEAT STRIP_TAC 595 THEN IMP_RES_TAC ALPHA1_TRANS1 596 ); 597 598 599val ALPHA1_LENGTH = store_thm 600 ("ALPHA1_LENGTH", 601 ���(!o1 o2 xs ys. ALPHA1_obj o1 o2 xs ys ==> 602 (LENGTH xs = LENGTH ys)) /\ 603 (!d1 d2 xs ys. ALPHA1_dict d1 d2 xs ys ==> 604 (LENGTH xs = LENGTH ys)) /\ 605 (!e1 e2 xs ys. ALPHA1_entry e1 e2 xs ys ==> 606 (LENGTH xs = LENGTH ys)) /\ 607 (!m1 m2 xs ys. ALPHA1_method m1 m2 xs ys ==> 608 (LENGTH xs = LENGTH ys))���, 609 rule_induct ALPHA1_ind_thm 610 THEN REWRITE_TAC[LENGTH,INV_SUC_EQ] 611 THEN REPEAT STRIP_TAC 612 THEN IMP_RES_TAC alpha_match_LENGTH 613 ); 614 615 616val ALPHA1_HEIGHT = store_thm 617 ("ALPHA1_HEIGHT", 618 ���(!o1 o2 xs ys. ALPHA1_obj o1 o2 xs ys ==> 619 (HEIGHT_obj1 o1 = HEIGHT_obj1 o2)) /\ 620 (!d1 d2 xs ys. ALPHA1_dict d1 d2 xs ys ==> 621 (HEIGHT_dict1 d1 = HEIGHT_dict1 d2)) /\ 622 (!e1 e2 xs ys. ALPHA1_entry e1 e2 xs ys ==> 623 (HEIGHT_entry1 e1 = HEIGHT_entry1 e2)) /\ 624 (!m1 m2 xs ys. ALPHA1_method m1 m2 xs ys ==> 625 (HEIGHT_method1 m1 = HEIGHT_method1 m2))���, 626 rule_induct ALPHA1_ind_thm 627 THEN REWRITE_TAC[HEIGHT1_def,INV_SUC_EQ] 628 THEN REPEAT STRIP_TAC 629 THEN ASM_REWRITE_TAC[] 630 ); 631 632 633val ALPHA1_object_similar = store_thm 634 ("ALPHA1_object_similar", 635 ���(!x a xs ys. ALPHA1_obj (OVAR1 x) a xs ys ==> (?y. a = OVAR1 y)) /\ 636 (!d1 a xs ys. ALPHA1_obj (OBJ1 d1) a xs ys ==> (?d2. a = OBJ1 d2)) /\ 637 (!o1 l1 a xs ys. ALPHA1_obj (INVOKE1 o1 l1) a xs ys ==> 638 (?o2 l2. a = INVOKE1 o2 l2)) /\ 639 (!o1 l1 m1 a xs ys. ALPHA1_obj (UPDATE1 o1 l1 m1) a xs ys ==> 640 (?o2 l2 m2. a = UPDATE1 o2 l2 m2)) /\ 641 (!e1 d1 d xs ys. ALPHA1_dict (CONS e1 d1) d xs ys ==> 642 (?e2 d2. d = CONS e2 d2)) /\ 643 (!d xs ys. ALPHA1_dict NIL d xs ys ==> (d = NIL)) /\ 644 (!l1 m1 e xs ys. ALPHA1_entry (l1,m1) e xs ys ==> 645 (?l2 m2. e = (l2,m2))) /\ 646 (!x1 o1 m xs ys. ALPHA1_method (SIGMA1 x1 o1) m xs ys ==> 647 (?x2 o2. m = SIGMA1 x2 o2))���, 648 PURE_ONCE_REWRITE_TAC ALPHA1_inv_thms 649 THEN REWRITE_TAC[object1_one_one,object1_distinct] 650 THEN REPEAT STRIP_TAC 651 THENL (* 7 subgoals *) 652 [ EXISTS_TAC ���y:var��� 653 THEN ASM_REWRITE_TAC[], 654 655 EXISTS_TAC ���d2:^dict1��� 656 THEN ASM_REWRITE_TAC[], 657 658 EXISTS_TAC ���o2':obj1��� 659 THEN EXISTS_TAC ���l:string��� 660 THEN ASM_REWRITE_TAC[], 661 662 EXISTS_TAC ���o2':obj1��� 663 THEN EXISTS_TAC ���l:string��� 664 THEN EXISTS_TAC ���m2:method1��� 665 THEN ASM_REWRITE_TAC[], 666 667 EXISTS_TAC ���e2:^entry1��� 668 THEN EXISTS_TAC ���d2':^dict1��� 669 THEN ASM_REWRITE_TAC[], 670 671 EXISTS_TAC ���l:string��� 672 THEN EXISTS_TAC ���m2:method1��� 673 THEN ASM_REWRITE_TAC[], 674 675 EXISTS_TAC ���y:var��� 676 THEN EXISTS_TAC ���o2:obj1��� 677 THEN ASM_REWRITE_TAC[] 678 ] 679 ); 680 681 682val ALPHA1_object_pos = store_thm 683 ("ALPHA1_object_pos", 684 ���(!x y xs ys. ALPHA1_obj (OVAR1 x) (OVAR1 y) xs ys 685 = alpha_match xs ys x y) /\ 686 (!d1 d2 xs ys. ALPHA1_obj (OBJ1 d1) (OBJ1 d2) xs ys 687 = ALPHA1_dict d1 d2 xs ys) /\ 688 (!o1 o2 l1 l2 xs ys. ALPHA1_obj (INVOKE1 o1 l1) (INVOKE1 o2 l2) xs ys 689 = (ALPHA1_obj o1 o2 xs ys /\ (l1 = l2))) /\ 690 (!o1 o2 l1 l2 m1 m2 xs ys. 691 ALPHA1_obj (UPDATE1 o1 l1 m1) (UPDATE1 o2 l2 m2) xs ys 692 = (ALPHA1_obj o1 o2 xs ys /\ (l1 = l2) 693 /\ ALPHA1_method m1 m2 xs ys)) /\ 694 (!e1 e2 d1 d2 xs ys. ALPHA1_dict (CONS e1 d1) (CONS e2 d2) xs ys 695 = (ALPHA1_entry e1 e2 xs ys 696 /\ ALPHA1_dict d1 d2 xs ys)) /\ 697 (ALPHA1_dict NIL NIL xs ys = (LENGTH xs = LENGTH ys)) /\ 698 (!l1 l2 m1 m2 xs ys. ALPHA1_entry (l1,m1) (l2,m2) xs ys 699 = ((l1 = l2) /\ ALPHA1_method m1 m2 xs ys)) /\ 700 (!x1 x2 o1 o2 xs ys. ALPHA1_method (SIGMA1 x1 o1) (SIGMA1 x2 o2) xs ys 701 = ALPHA1_obj o1 o2 (CONS x1 xs) (CONS x2 ys))���, 702 REPEAT CONJ_TAC 703 THEN REPEAT GEN_TAC 704 THEN (EQ_TAC 705 THENL [ DISCH_THEN (STRIP_ASSUME_TAC 706 o REWRITE_RULE[object1_one_one,object1_distinct] 707 o ONCE_REWRITE_RULE ALPHA1_inv_thms) 708 THEN ASM_REWRITE_TAC[], 709 710 REWRITE_TAC[] 711 THEN REPEAT STRIP_TAC 712 THEN FIRST (map (fn th => ASM_REWRITE_TAC[] 713 THEN (MATCH_MP_TAC th 714 handle _ => ALL_TAC) 715 THEN ASM_REWRITE_TAC[th] 716 THEN NO_TAC) 717 (CONJUNCTS ALPHA1_rules_sat)) 718 ]) 719 ); 720 721 722val ALPHA1_object_neg = store_thm 723 ("ALPHA1_object_neg", 724 ���(!x d xs ys. ALPHA1_obj (OVAR1 x) (OBJ1 d) xs ys = F) /\ 725 (!x a l xs ys. ALPHA1_obj (OVAR1 x) (INVOKE1 a l) xs ys = F) /\ 726 (!x a l m xs ys. ALPHA1_obj (OVAR1 x) (UPDATE1 a l m) xs ys = F) /\ 727 (!d x xs ys. ALPHA1_obj (OBJ1 d) (OVAR1 x) xs ys = F) /\ 728 (!d a l xs ys. ALPHA1_obj (OBJ1 d) (INVOKE1 a l) xs ys = F) /\ 729 (!d a l m xs ys. ALPHA1_obj (OBJ1 d) (UPDATE1 a l m) xs ys = F) /\ 730 (!a l x xs ys. ALPHA1_obj (INVOKE1 a l) (OVAR1 x) xs ys = F) /\ 731 (!a l d xs ys. ALPHA1_obj (INVOKE1 a l) (OBJ1 d) xs ys = F) /\ 732 (!o1 l1 o2 l2 m2 xs ys. 733 ALPHA1_obj (INVOKE1 o1 l1) (UPDATE1 o2 l2 m2) xs ys = F) /\ 734 (!a l m x xs ys. ALPHA1_obj (UPDATE1 a l m) (OVAR1 x) xs ys = F) /\ 735 (!a l m d xs ys. ALPHA1_obj (UPDATE1 a l m) (OBJ1 d) xs ys = F) /\ 736 (!o1 l1 m1 o2 l2 xs ys. 737 ALPHA1_obj (UPDATE1 o1 l1 m1) (INVOKE1 o2 l2) xs ys = F) 738 /\ 739 (!e d xs ys. ALPHA1_dict (CONS e d) NIL xs ys = F) /\ 740 (!e d xs ys. ALPHA1_dict NIL (CONS e d) xs ys = F)���, 741 PURE_ONCE_REWRITE_TAC ALPHA1_inv_thms 742 THEN REWRITE_TAC[object1_one_one,object1_distinct] 743 ); 744 745 746(* We have no use for the following induction principle at present, 747 but are keeping it in this comment in case it becomes useful later. 748 749val ALPHA1_height_induct_LEMMA = TAC_PROOF(([], 750 ���!n P_0 P_1 P_2 P_3. 751 (!x y xs ys. 752 alpha_match xs ys x y ==> P_0 (OVAR1 x) (OVAR1 y) xs ys) /\ 753 (!d1 d2 xs ys. 754 P_1 d1 d2 xs ys /\ ALPHA1_dict d1 d2 xs ys ==> 755 P_0 (OBJ1 d1) (OBJ1 d2) xs ys) /\ 756 (!o1 l o2 xs ys. 757 P_0 o1 o2 xs ys /\ ALPHA1_obj o1 o2 xs ys ==> 758 P_0 (INVOKE1 o1 l) (INVOKE1 o2 l) xs ys) /\ 759 (!o1 l m1 o2 m2 xs ys. 760 P_0 o1 o2 xs ys /\ ALPHA1_obj o1 o2 xs ys /\ 761 P_3 m1 m2 xs ys /\ ALPHA1_method m1 m2 xs ys ==> 762 P_0 (UPDATE1 o1 l m1) (UPDATE1 o2 l m2) xs ys) /\ 763 (!e1 d1 e2 d2 xs ys. 764 P_2 e1 e2 xs ys /\ ALPHA1_entry e1 e2 xs ys /\ 765 P_1 d1 d2 xs ys /\ ALPHA1_dict d1 d2 xs ys ==> 766 P_1 (CONS e1 d1) (CONS e2 d2) xs ys) /\ 767 (!xs ys. (LENGTH xs = LENGTH ys) ==> P_1 [] [] xs ys) /\ 768 (!l m1 m2 xs ys. 769 P_3 m1 m2 xs ys /\ ALPHA1_method m1 m2 xs ys ==> 770 P_2 (l,m1) (l,m2) xs ys) /\ 771 (!x o1 y o2 xs ys. 772 (!o' o''. ALPHA1_obj o' o'' (CONS x xs) (CONS y ys) /\ 773 (HEIGHT_obj1 o1 = HEIGHT_obj1 o') /\ 774 (HEIGHT_obj1 o2 = HEIGHT_obj1 o'') ==> 775 P_0 o' o'' (CONS x xs) (CONS y ys)) /\ 776 ALPHA1_obj o1 o2 (CONS x xs) (CONS y ys) ==> 777 P_3 (SIGMA1 x o1) (SIGMA1 y o2) xs ys) ==> 778 (!o1 o2 xs ys. ALPHA1_obj o1 o2 xs ys ==> 779 ((HEIGHT_obj1 o1 <= n) /\ 780 (HEIGHT_obj1 o2 <= n) ==> 781 P_0 o1 o2 xs ys)) /\ 782 (!d1 d2 xs ys. ALPHA1_dict d1 d2 xs ys ==> 783 ((HEIGHT_dict1 d1 <= n) /\ 784 (HEIGHT_dict1 d2 <= n) ==> 785 P_1 d1 d2 xs ys)) /\ 786 (!e1 e2 xs ys. ALPHA1_entry e1 e2 xs ys ==> 787 ((HEIGHT_entry1 e1 <= n) /\ 788 (HEIGHT_entry1 e2 <= n) ==> 789 P_2 e1 e2 xs ys)) /\ 790 (!m1 m2 xs ys. ALPHA1_method m1 m2 xs ys ==> 791 ((HEIGHT_method1 m1 <= n) /\ 792 (HEIGHT_method1 m2 <= n) ==> 793 P_3 m1 m2 xs ys))���), 794 INDUCT_TAC 795 THEN REPEAT GEN_TAC 796 THEN STRIP_TAC 797 THENL 798 [ REWRITE_TAC[HEIGHT_LESS_EQ_ZERO1] 799 THEN REPEAT STRIP_TAC 800 THEN ASM_REWRITE_TAC[] 801 THEN FIRST_ASSUM MATCH_MP_TAC 802 THENL 803 [ UNDISCH_TAC ���ALPHA1_obj o1 o2 xs ys��� 804 THEN ASM_REWRITE_TAC[ALPHA1_object_pos], 805 806 IMP_RES_TAC ALPHA1_LENGTH 807 ], 808 809 UNDISCH_ALL_TAC 810 THEN DISCH_THEN ((fn th => REPEAT DISCH_TAC 811 THEN ASSUME_TAC th) o SPEC_ALL) 812 THEN POP_ASSUM MP_TAC 813 THEN ASM_REWRITE_TAC[] 814 THEN DISCH_THEN (fn th => UNDISCH_ALL_TAC THEN STRIP_ASSUME_TAC th) 815 THEN REPEAT DISCH_TAC 816 THEN rule_induct ALPHA1_strong_ind 817 THEN REWRITE_TAC[HEIGHT1_def] 818 THEN REWRITE_TAC[MAX_SUC,MAX_LESS_EQ,LESS_EQ_MONO,ZERO_LESS_EQ] 819 THEN REPEAT STRIP_TAC 820 THEN ASM_REWRITE_TAC[] 821 THENL (* 8 subgoals *) 822 [ FIRST_ASSUM MATCH_MP_TAC 823 THEN ASM_REWRITE_TAC[], 824 825 FIRST_ASSUM MATCH_MP_TAC 826 THEN ASM_REWRITE_TAC[] 827 THEN FIRST_ASSUM MATCH_MP_TAC 828 THEN IMP_RES_TAC LESS_EQ_IMP_LESS_SUC 829 THEN IMP_RES_TAC LESS_IMP_LESS_OR_EQ 830 THEN ASM_REWRITE_TAC[], 831 832 FIRST_ASSUM MATCH_MP_TAC 833 THEN ASM_REWRITE_TAC[] 834 THEN FIRST_ASSUM MATCH_MP_TAC 835 THEN IMP_RES_TAC LESS_EQ_IMP_LESS_SUC 836 THEN IMP_RES_TAC LESS_IMP_LESS_OR_EQ 837 THEN ASM_REWRITE_TAC[], 838 839 FIRST_ASSUM MATCH_MP_TAC 840 THEN ASM_REWRITE_TAC[] 841 THEN CONJ_TAC 842 THEN FIRST_ASSUM MATCH_MP_TAC 843 THEN IMP_RES_TAC LESS_EQ_IMP_LESS_SUC 844 THEN IMP_RES_TAC LESS_IMP_LESS_OR_EQ 845 THEN ASM_REWRITE_TAC[], 846 847 FIRST_ASSUM MATCH_MP_TAC 848 THEN ASM_REWRITE_TAC[] 849 THEN CONJ_TAC 850 THEN FIRST_ASSUM MATCH_MP_TAC 851 THEN IMP_RES_TAC LESS_EQ_IMP_LESS_SUC 852 THEN IMP_RES_TAC LESS_IMP_LESS_OR_EQ 853 THEN ASM_REWRITE_TAC[], 854 855 FIRST_ASSUM MATCH_MP_TAC 856 THEN ASM_REWRITE_TAC[], 857 858 FIRST_ASSUM MATCH_MP_TAC 859 THEN ASM_REWRITE_TAC[] 860 THEN FIRST_ASSUM MATCH_MP_TAC 861 THEN IMP_RES_TAC LESS_EQ_IMP_LESS_SUC 862 THEN IMP_RES_TAC LESS_IMP_LESS_OR_EQ 863 THEN ASM_REWRITE_TAC[], 864 865 FIRST_ASSUM MATCH_MP_TAC 866 THEN ASM_REWRITE_TAC[] 867 THEN REPEAT STRIP_TAC 868 THEN FIRST_ASSUM (MATCH_MP_TAC o REWRITE_RULE[AND_IMP_INTRO]) 869 THEN POP_ASSUM (REWRITE_THM o SYM) 870 THEN POP_ASSUM (REWRITE_THM o SYM) 871 THEN IMP_RES_TAC LESS_EQ_IMP_LESS_SUC 872 THEN IMP_RES_TAC LESS_IMP_LESS_OR_EQ 873 THEN ASM_REWRITE_TAC[] 874 ] 875 ] 876 ); 877 878 879val ALPHA1_height_induct = store_thm 880 ("ALPHA1_height_induct", 881 ���!P_0 P_1 P_2 P_3. 882 (!x y xs ys. 883 alpha_match xs ys x y ==> P_0 (OVAR1 x) (OVAR1 y) xs ys) /\ 884 (!d1 d2 xs ys. 885 P_1 d1 d2 xs ys /\ ALPHA1_dict d1 d2 xs ys ==> 886 P_0 (OBJ1 d1) (OBJ1 d2) xs ys) /\ 887 (!o1 l o2 xs ys. 888 P_0 o1 o2 xs ys /\ ALPHA1_obj o1 o2 xs ys ==> 889 P_0 (INVOKE1 o1 l) (INVOKE1 o2 l) xs ys) /\ 890 (!o1 l m1 o2 m2 xs ys. 891 P_0 o1 o2 xs ys /\ ALPHA1_obj o1 o2 xs ys /\ 892 P_3 m1 m2 xs ys /\ ALPHA1_method m1 m2 xs ys ==> 893 P_0 (UPDATE1 o1 l m1) (UPDATE1 o2 l m2) xs ys) /\ 894 (!e1 d1 e2 d2 xs ys. 895 P_2 e1 e2 xs ys /\ ALPHA1_entry e1 e2 xs ys /\ 896 P_1 d1 d2 xs ys /\ ALPHA1_dict d1 d2 xs ys ==> 897 P_1 (CONS e1 d1) (CONS e2 d2) xs ys) /\ 898 (!xs ys. (LENGTH xs = LENGTH ys) ==> P_1 [] [] xs ys) /\ 899 (!l m1 m2 xs ys. 900 P_3 m1 m2 xs ys /\ ALPHA1_method m1 m2 xs ys ==> 901 P_2 (l,m1) (l,m2) xs ys) /\ 902 (!x o1 y o2 xs ys. 903 (!o' o''. ALPHA1_obj o' o'' (CONS x xs) (CONS y ys) /\ 904 (HEIGHT_obj1 o1 = HEIGHT_obj1 o') /\ 905 (HEIGHT_obj1 o2 = HEIGHT_obj1 o'') ==> 906 P_0 o' o'' (CONS x xs) (CONS y ys)) /\ 907 ALPHA1_obj o1 o2 (CONS x xs) (CONS y ys) ==> 908 P_3 (SIGMA1 x o1) (SIGMA1 y o2) xs ys) ==> 909 (!o1 o2 xs ys. ALPHA1_obj o1 o2 xs ys ==> P_0 o1 o2 xs ys) /\ 910 (!d1 d2 xs ys. ALPHA1_dict d1 d2 xs ys ==> P_1 d1 d2 xs ys) /\ 911 (!e1 e2 xs ys. ALPHA1_entry e1 e2 xs ys ==> P_2 e1 e2 xs ys) /\ 912 (!m1 m2 xs ys. ALPHA1_method m1 m2 xs ys ==> P_3 m1 m2 xs ys)���, 913 REPEAT STRIP_TAC 914 THENL 915 (map (fn tm => MP_TAC (SPEC_ALL (SPEC tm ALPHA1_height_induct_LEMMA))) 916 [���(HEIGHT_obj1 o1) MAX (HEIGHT_obj1 o2)���, 917 ���(HEIGHT_dict1 d1) MAX (HEIGHT_dict1 d2)���, 918 ���(HEIGHT_entry1 e1) MAX (HEIGHT_entry1 e2)���, 919 ���(HEIGHT_method1 m1) MAX (HEIGHT_method1 m2)���]) 920 THEN ASM_REWRITE_TAC[AND_IMP_INTRO] 921 THEN REPEAT STRIP_TAC 922 THEN FIRST_ASSUM MATCH_MP_TAC 923 THEN ASM_REWRITE_TAC[LESS_EQ_MAX] 924 ); 925 926(* Unfortunately, this induction principle is not that useful yet, because *) 927(* we do not yet have the ability to shift the bound variable of a SIGMA1. *) 928 929 930fun INSTANTIATE_TAC th (asm,gl) = 931 let val {Bvar=x, Body=glb} = Rsyntax.dest_forall gl 932 in 933 (X_GEN_TAC x 934 THEN STRIP_ASSUME_TAC (SPEC x th) 935 (* If disjuncts in th, multiple subgoals here *) 936 THEN POP_ASSUM REWRITE_ALL_THM 937 THEN REWRITE_TAC[ALPHA1_object_pos,ALPHA1_object_neg]) (asm,gl) 938 end; 939 940fun FIND_INSTANTIATION th (asm,gl) = 941 (FIRST (map INSTANTIATE_TAC (CONJUNCTS th)) 942 ORELSE (GEN_TAC THEN FIND_INSTANTIATION th)) (asm,gl); 943*) 944 945 946val ALPHA1_FV = store_thm 947 ("ALPHA1_FV", 948 (���(!o1 o2 xs ys. ALPHA1_obj o1 o2 xs ys ==> 949 (!x. x IN FV_obj1 o1 ==> 950 (?y. y IN FV_obj1 o2 /\ alpha_match xs ys x y))) /\ 951 952 (!d1 d2 xs ys. ALPHA1_dict d1 d2 xs ys ==> 953 (!x. x IN FV_dict1 d1 ==> 954 (?y. y IN FV_dict1 d2 /\ alpha_match xs ys x y))) /\ 955 956 (!e1 e2 xs ys. ALPHA1_entry e1 e2 xs ys ==> 957 (!x. x IN FV_entry1 e1 ==> 958 (?y. y IN FV_entry1 e2 /\ alpha_match xs ys x y))) /\ 959 960 (!m1 m2 xs ys. ALPHA1_method m1 m2 xs ys ==> 961 (!x. x IN FV_method1 m1 ==> 962 (?y. y IN FV_method1 m2 /\ alpha_match xs ys x y)))���), 963 964 rule_induct ALPHA1_strong_ind 965 THEN REWRITE_TAC[FV_object1_def] 966 THEN REWRITE_TAC[IN_INSERT,NOT_IN_EMPTY,IN_UNION,IN_DIFF] 967 THEN REPEAT STRIP_TAC 968 THEN RES_TAC 969 THEN TRY (EXISTS_TAC ���y:var��� 970 THEN ASM_REWRITE_TAC[] 971 THEN NO_TAC) 972 (* only one goal here *) 973 THEN EXISTS_TAC ���y':var��� 974 THEN IMP_RES_TAC alpha_match_NOT_EQ 975 THEN ASM_REWRITE_TAC[] 976 ); 977(* Glory to God! Soli Deo Gloria! *) 978 979 980 981val FORALL_OR_IMP = TAC_PROOF(([], 982 ���!s t (f:'a->'b) g. 983 (!x. x IN s \/ x IN t ==> (f x = g x)) ==> 984 ((!x. x IN s ==> (f x = g x)) /\ 985 (!x. x IN t ==> (f x = g x)))���), 986 PROVE_TAC [] 987 ); 988 989 990val ALPHA1_FREE_CONTEXT = store_thm 991 ("ALPHA1_FREE_CONTEXT", 992 ���(!o1 o2 xs ys xs' ys'. 993 ((LENGTH xs = LENGTH ys) = (LENGTH xs' = LENGTH ys')) /\ 994 (!x. (x IN FV_obj1 o1) ==> 995 (SUB1 (xs // ys) x = SUB1 (xs' // ys') x)) /\ 996 (!y. (y IN FV_obj1 o2) ==> 997 (SUB1 (ys // xs) y = SUB1 (ys' // xs') y)) ==> 998 (ALPHA1_obj o1 o2 xs ys = ALPHA1_obj o1 o2 xs' ys')) /\ 999 (!d1 d2 xs ys xs' ys'. 1000 ((LENGTH xs = LENGTH ys) = (LENGTH xs' = LENGTH ys')) /\ 1001 (!x. (x IN FV_dict1 d1) ==> 1002 (SUB1 (xs // ys) x = SUB1 (xs' // ys') x)) /\ 1003 (!y. (y IN FV_dict1 d2) ==> 1004 (SUB1 (ys // xs) y = SUB1 (ys' // xs') y)) ==> 1005 (ALPHA1_dict d1 d2 xs ys = ALPHA1_dict d1 d2 xs' ys')) /\ 1006 (!e1 e2 xs ys xs' ys'. 1007 ((LENGTH xs = LENGTH ys) = (LENGTH xs' = LENGTH ys')) /\ 1008 (!x. (x IN FV_entry1 e1) ==> 1009 (SUB1 (xs // ys) x = SUB1 (xs' // ys') x)) /\ 1010 (!y. (y IN FV_entry1 e2) ==> 1011 (SUB1 (ys // xs) y = SUB1 (ys' // xs') y)) ==> 1012 (ALPHA1_entry e1 e2 xs ys = ALPHA1_entry e1 e2 xs' ys')) /\ 1013 (!m1 m2 xs ys xs' ys'. 1014 ((LENGTH xs = LENGTH ys) = (LENGTH xs' = LENGTH ys')) /\ 1015 (!x. (x IN FV_method1 m1) ==> 1016 (SUB1 (xs // ys) x = SUB1 (xs' // ys') x)) /\ 1017 (!y. (y IN FV_method1 m2) ==> 1018 (SUB1 (ys // xs) y = SUB1 (ys' // xs') y)) ==> 1019 (ALPHA1_method m1 m2 xs ys = ALPHA1_method m1 m2 xs' ys'))���, 1020 MUTUAL_INDUCT_THEN obj1_induction ASSUME_TAC 1021 THEN REPEAT STRIP_TAC 1022 THEN EQ_TAC 1023 THEN STRIP_TAC 1024 THEN IMP_RES_TAC ALPHA1_object_similar 1025 THEN POP_ASSUM REWRITE_ALL_THM 1026 THEN REWRITE_ALL_TAC[FV_object1_def,IN_DIFF,IN_UNION,IN] 1027 THEN UNDISCH_LAST_TAC 1028 THEN REWRITE_TAC[ALPHA1_object_pos] 1029 THENL 1030 [ 1031 REWRITE_TAC[alpha_match_SUB_var] 1032 THEN POP_ASSUM (MP_TAC o SPEC ���y:var���) 1033 THEN POP_ASSUM (MP_TAC o SPEC ���v:var���) 1034 THEN REWRITE_TAC[] 1035 THEN DISCH_TAC 1036 THEN DISCH_TAC 1037 THEN ASM_REWRITE_TAC[], 1038 1039 REWRITE_TAC[alpha_match_SUB_var] 1040 THEN POP_ASSUM (MP_TAC o SPEC ���y:var���) 1041 THEN POP_ASSUM (MP_TAC o SPEC ���v:var���) 1042 THEN REWRITE_TAC[] 1043 THEN DISCH_TAC 1044 THEN DISCH_TAC 1045 THEN ASM_REWRITE_TAC[], 1046 1047 DISCH_TAC 1048 THEN RES_TAC, 1049 1050 DISCH_TAC 1051 THEN RES_TAC, 1052 1053 STRIP_TAC 1054 THEN ASM_REWRITE_TAC[] 1055 THEN RES_TAC, 1056 1057 STRIP_TAC 1058 THEN ASM_REWRITE_TAC[] 1059 THEN RES_TAC, 1060 1061 IMP_RES_TAC FORALL_OR_IMP 1062 THEN STRIP_TAC 1063 THEN RES_TAC 1064 THEN ASM_REWRITE_TAC[], 1065 1066 IMP_RES_TAC FORALL_OR_IMP 1067 THEN STRIP_TAC 1068 THEN RES_TAC 1069 THEN ASM_REWRITE_TAC[], 1070 1071 FIRST_ASSUM (fn th => 1072 DEP_REWRITE_TAC[ 1073 SPECL [���o2:obj1���,���CONS (v:var) xs���,���CONS (x2:var) ys���, 1074 ���CONS (v:var) xs'���,���CONS (x2:var) ys'���] 1075 th]) 1076 THEN ASM_REWRITE_TAC[LENGTH,INV_SUC_EQ] 1077 THEN CONJ_TAC 1078 THEN GEN_TAC 1079 THEN DISCH_TAC 1080 THEN REWRITE_TAC[vsubst1,SUB1] 1081 THEN COND_CASES_TAC 1082 THEN ASM_REWRITE_TAC[] 1083 THEN FIRST_ASSUM MATCH_MP_TAC 1084 THEN FIRST_ASSUM (REWRITE_THM o GSYM) 1085 THEN ASM_REWRITE_TAC[], 1086 1087 FIRST_ASSUM (fn th => 1088 DEP_ONCE_REWRITE_TAC[ 1089 SPECL [���o2:obj1���,���CONS (v:var) xs'���,���CONS (x2:var) ys'���, 1090 ���CONS (v:var) xs���,���CONS (x2:var) ys���] 1091 th]) 1092 THEN ASM_REWRITE_TAC[LENGTH,INV_SUC_EQ] 1093 THEN CONJ_TAC 1094 THEN GEN_TAC 1095 THEN DISCH_TAC 1096 THEN REWRITE_TAC[vsubst1,SUB1] 1097 THEN COND_CASES_TAC 1098 THEN ASM_REWRITE_TAC[] 1099 THEN ONCE_REWRITE_TAC[EQ_SYM_EQ] 1100 THEN FIRST_ASSUM MATCH_MP_TAC 1101 THEN ASM_REWRITE_TAC[], 1102 1103 POP_TAC 1104 THEN POP_TAC 1105 THEN ASM_REWRITE_TAC[], 1106 1107 POP_TAC 1108 THEN POP_TAC 1109 THEN ASM_REWRITE_TAC[], 1110 1111 IMP_RES_TAC FORALL_OR_IMP 1112 THEN STRIP_TAC 1113 THEN RES_TAC 1114 THEN ASM_REWRITE_TAC[], 1115 1116 IMP_RES_TAC FORALL_OR_IMP 1117 THEN STRIP_TAC 1118 THEN RES_TAC 1119 THEN ASM_REWRITE_TAC[], 1120 1121 STRIP_TAC 1122 THEN ASM_REWRITE_TAC[] 1123 THEN RES_TAC, 1124 1125 STRIP_TAC 1126 THEN ASM_REWRITE_TAC[] 1127 THEN RES_TAC 1128 ] 1129 ); 1130 1131 1132val ALPHA1_EXTRANEOUS_CONTEXT = store_thm 1133 ("ALPHA1_EXTRANEOUS_CONTEXT", 1134 ���(!o1 o2 xs ys x y. 1135 ~(x IN FV_obj1 o1) /\ ~(y IN FV_obj1 o2) ==> 1136 (ALPHA1_obj o1 o2 (CONS x xs) (CONS y ys) = 1137 ALPHA1_obj o1 o2 xs ys)) /\ 1138 (!d1 d2 xs ys x y. 1139 ~(x IN FV_dict1 d1) /\ ~(y IN FV_dict1 d2) ==> 1140 (ALPHA1_dict d1 d2 (CONS x xs) (CONS y ys) = 1141 ALPHA1_dict d1 d2 xs ys)) /\ 1142 (!e1 e2 xs ys x y. 1143 ~(x IN FV_entry1 e1) /\ ~(y IN FV_entry1 e2) ==> 1144 (ALPHA1_entry e1 e2 (CONS x xs) (CONS y ys) = 1145 ALPHA1_entry e1 e2 xs ys)) /\ 1146 (!m1 m2 xs ys x y. 1147 ~(x IN FV_method1 m1) /\ ~(y IN FV_method1 m2) ==> 1148 (ALPHA1_method m1 m2 (CONS x xs) (CONS y ys) = 1149 ALPHA1_method m1 m2 xs ys))���, 1150 REPEAT STRIP_TAC 1151 THEN FIRST (map MATCH_MP_TAC (CONJUNCTS ALPHA1_FREE_CONTEXT)) 1152 THEN REWRITE_TAC[LENGTH,INV_SUC_EQ] 1153 THEN CONJ_TAC 1154 THEN GEN_TAC 1155 THEN DISCH_TAC 1156 THEN REWRITE_TAC[vsubst1,SUB1] 1157 THEN COND_CASES_TAC 1158 THEN ASM_REWRITE_TAC[] 1159 THEN POP_ASSUM REWRITE_ALL_THM 1160 THEN RES_TAC 1161 ); 1162 1163val [ALPHA1_EXTRANEOUS_CONTEXT_obj, ALPHA1_EXTRANEOUS_CONTEXT_dict1, 1164 ALPHA1_EXTRANEOUS_CONTEXT_entry1, ALPHA1_EXTRANEOUS_CONTEXT_method1] = 1165 CONJUNCTS ALPHA1_EXTRANEOUS_CONTEXT; 1166 1167 1168 1169(* ---------------------------------------------------------------------- *) 1170(* Now we prepare to prove ALPHA1_SUB, the key and most important theorem *) 1171(* of this theory. It is difficult, but critical. *) 1172(* ---------------------------------------------------------------------- *) 1173 1174 1175(* define ALPHA1_subst *) 1176 1177val ALPHA1_subst = 1178 new_definition 1179 ("ALPHA1_subst", 1180 ���ALPHA1_subst xs ys xs' ys' t1 t2 s1 s2 = 1181 (LENGTH xs' = LENGTH ys') /\ 1182 (!x y. (x IN t1) /\ (y IN t2) /\ 1183 alpha_match xs ys x y ==> 1184 ALPHA1_obj (SUB1 s1 x) (SUB1 s2 y) xs' ys')���); 1185 1186 1187val ALPHA1_subst_UNION = store_thm 1188 ("ALPHA1_subst_UNION", 1189 ���!xs ys xs' ys' t11 t12 t21 t22 s1 s2. 1190 ALPHA1_subst xs ys xs' ys' (t11 UNION t12) (t21 UNION t22) s1 s2 1191 ==> 1192 (ALPHA1_subst xs ys xs' ys' t11 t21 s1 s2 /\ 1193 ALPHA1_subst xs ys xs' ys' t12 t22 s1 s2)���, 1194 REPEAT GEN_TAC 1195 THEN REWRITE_TAC[ALPHA1_subst] 1196 THEN REWRITE_TAC[IN_UNION] 1197 THEN REPEAT STRIP_TAC 1198 THEN ASM_REWRITE_TAC[] 1199 THEN FIRST_ASSUM MATCH_MP_TAC 1200 THEN ASM_REWRITE_TAC[] 1201 ); 1202 1203val ALPHA1_subst_LENGTH = store_thm 1204 ("ALPHA1_subst_LENGTH", 1205 ���!xs ys xs' ys' t1 t2 s1 s2. 1206 ALPHA1_subst xs ys xs' ys' t1 t2 s1 s2 1207 ==> 1208 (LENGTH xs' = LENGTH ys')���, 1209 REWRITE_TAC[ALPHA1_subst] 1210 THEN REPEAT STRIP_TAC 1211 ); 1212 1213 1214 1215val variant_not_in_sub = store_thm 1216 ("variant_not_in_sub", 1217 ���!v v' s t x. 1218 FINITE t /\ (x IN t) /\ 1219 (v' = variant v (FV_subst1 s t)) 1220 ==> 1221 ~(v' IN FV_obj1 (SUB1 s x))���, 1222 REPEAT GEN_TAC 1223 THEN STRIP_TAC 1224 THEN MP_TAC (SPECL [���v:var���,���FV_subst1 s t���] variant_not_in_set) 1225 THEN IMP_RES_THEN REWRITE_THM FINITE_FV_subst1 1226 THEN FIRST_ASSUM (REWRITE_THM o SYM) 1227 THEN REWRITE_TAC[FV_subst1] 1228 THEN REWRITE_TAC[IN_UNION_SET,IN_IMAGE,combinTheory.o_THM] 1229 THEN CONV_TAC (DEPTH_CONV NOT_EXISTS_CONV) 1230 THEN REWRITE_TAC[DE_MORGAN_THM] 1231 THEN CONV_TAC (DEPTH_CONV NOT_EXISTS_CONV) 1232 THEN REWRITE_TAC[DE_MORGAN_THM] 1233 THEN DISCH_THEN (MP_TAC o SPEC ���FV_obj1 (SUB1 s x)���) 1234 THEN STRIP_TAC 1235 THEN POP_ASSUM (MP_TAC o SPEC ���x:var���) 1236 THEN ASM_REWRITE_TAC[] 1237 ); 1238 1239 1240 1241val ALPHA1_SUB = store_thm 1242 ("ALPHA1_SUB", 1243 ���(!o1 o2 xs ys. ALPHA1_obj o1 o2 xs ys ==> 1244 (!xs' ys' s1 s2. 1245 ALPHA1_subst xs ys xs' ys' (FV_obj1 o1) (FV_obj1 o2) s1 s2 ==> 1246 ALPHA1_obj (o1 <[ s1) (o2 <[ s2) xs' ys')) /\ 1247 (!d1 d2 xs ys. ALPHA1_dict d1 d2 xs ys ==> 1248 (!xs' ys' s1 s2. 1249 ALPHA1_subst xs ys xs' ys' (FV_dict1 d1) (FV_dict1 d2) s1 s2 ==> 1250 ALPHA1_dict (d1 <[ s1) (d2 <[ s2) xs' ys')) /\ 1251 (!e1 e2 xs ys. ALPHA1_entry e1 e2 xs ys ==> 1252 (!xs' ys' s1 s2. 1253 ALPHA1_subst xs ys xs' ys' (FV_entry1 e1) (FV_entry1 e2) s1 s2 ==> 1254 ALPHA1_entry (e1 <[ s1) (e2 <[ s2) xs' ys')) /\ 1255 (!m1 m2 xs ys. ALPHA1_method m1 m2 xs ys ==> 1256 (!xs' ys' s1 s2. 1257 ALPHA1_subst xs ys xs' ys' (FV_method1 m1) (FV_method1 m2) s1 s2 ==> 1258 ALPHA1_method (m1 <[ s1) (m2 <[ s2) xs' ys'))���, 1259 rule_induct ALPHA1_strong_ind 1260 THEN REWRITE_TAC[FV_object1_def] 1261 THEN REPEAT STRIP_TAC 1262 THEN REWRITE_TAC[SUB_object1_def] 1263 THEN CONV_TAC (DEPTH_CONV let_CONV) 1264 THEN REWRITE_TAC[ALPHA1_object_pos] 1265 THEN IMP_RES_TAC ALPHA1_subst_UNION 1266 THEN IMP_RES_TAC ALPHA1_subst_LENGTH 1267 THEN RES_TAC 1268 THEN ASM_REWRITE_TAC[] 1269 (* two subgoals left: *) 1270 THENL 1271 [ UNDISCH_LAST_TAC 1272 THEN UNDISCH_LAST_TAC 1273 THEN REWRITE_TAC[ALPHA1_subst] 1274 THEN REWRITE_TAC[IN] 1275 THEN STRIP_TAC 1276 THEN ASM_REWRITE_TAC[] 1277 THEN POP_ASSUM MATCH_MP_TAC 1278 THEN ASM_REWRITE_TAC[], 1279 1280 POP_TAC 1281 THEN UNDISCH_LAST_TAC 1282 THEN DEFINE_NEW_VAR 1283 ���x' = variant x (FV_subst1 s1 (FV_obj1 o1 DIFF {x}))��� 1284 THEN FIRST_ASSUM (REWRITE_THM o SYM) 1285 THEN DEFINE_NEW_VAR 1286 ���y' = variant y (FV_subst1 s2 (FV_obj1 o2 DIFF {y}))��� 1287 THEN FIRST_ASSUM (REWRITE_THM o SYM) 1288 THEN DISCH_TAC 1289 THEN FIRST_ASSUM MATCH_MP_TAC 1290 THEN UNDISCH_LAST_TAC 1291 THEN REWRITE_TAC[ALPHA1_subst] 1292 THEN STRIP_TAC 1293 THEN UNDISCH_LAST_TAC 1294 THEN REWRITE_TAC[LENGTH] 1295 THEN FIRST_ASSUM REWRITE_THM 1296 THEN DISCH_TAC 1297 THEN REPEAT GEN_TAC 1298 THEN REWRITE_TAC[alpha_match] 1299 THEN REWRITE_TAC[SUB1] 1300 THEN COND_CASES_TAC 1301 THENL 1302 [ POP_ASSUM REWRITE_THM 1303 THEN COND_CASES_TAC 1304 THEN FIRST_ASSUM REWRITE_THM 1305 THEN POP_TAC 1306 THEN STRIP_TAC 1307 THEN REWRITE_TAC[ALPHA1_object_pos] 1308 THEN REWRITE_TAC[alpha_match] 1309 THEN FIRST_ASSUM ACCEPT_TAC, 1310 1311 COND_CASES_TAC 1312 THEN FIRST_ASSUM REWRITE_THM 1313 THEN STRIP_TAC 1314 (* Here the extra x', y' are extraneous *) 1315 THEN DEP_REWRITE_TAC[ALPHA1_EXTRANEOUS_CONTEXT_obj] 1316 THEN FIRST_ASSUM (MP_TAC o SPECL[���x'':var���,���y'':var���]) 1317 THEN REWRITE_TAC[IN_DIFF,IN] 1318 THEN DISCH_THEN IMP_RES_TAC 1319 THEN FIRST_ASSUM REWRITE_THM 1320 THEN CONJ_TAC 1321 THEN MATCH_MP_TAC variant_not_in_sub 1322 THENL 1323 [ EXISTS_TAC ���x:var��� 1324 THEN EXISTS_TAC ���FV_obj1 o1 DIFF {x}��� 1325 THEN ASM_REWRITE_TAC[IN_DIFF,IN] 1326 THEN MATCH_MP_TAC FINITE_DIFF 1327 THEN REWRITE_TAC[FINITE_FV_object1], 1328 1329 EXISTS_TAC ���y:var��� 1330 THEN EXISTS_TAC ���FV_obj1 o2 DIFF {y}��� 1331 THEN ASM_REWRITE_TAC[IN_DIFF,IN] 1332 THEN MATCH_MP_TAC FINITE_DIFF 1333 THEN REWRITE_TAC[FINITE_FV_object1] 1334 ] 1335 ] 1336 ] 1337 ); 1338(* Soli Deo Gloria!!! *) 1339 1340 1341 1342 1343val ALPHA1_CHANGE_VAR = store_thm 1344 ("ALPHA1_CHANGE_VAR", 1345 ���!y x s v a. 1346 ~(x IN FV_subst1 s (FV_obj1 a DIFF {v})) /\ 1347 ~(y IN FV_subst1 s (FV_obj1 a DIFF {v})) ==> 1348 ALPHA1_obj 1349 (a <[ CONS (v, OVAR1 x) s) 1350 (a <[ CONS (v, OVAR1 y) s) 1351 [x] [y]���, 1352 REWRITE_TAC[FV_subst1] 1353 THEN REWRITE_TAC[IN_UNION_SET,IN_IMAGE,o_THM] 1354 THEN CONV_TAC (DEPTH_CONV NOT_EXISTS_CONV) 1355 THEN REWRITE_TAC[DE_MORGAN_THM] 1356 THEN CONV_TAC (DEPTH_CONV NOT_EXISTS_CONV) 1357 THEN REWRITE_TAC[DE_MORGAN_THM,IN_DIFF,IN] 1358 THEN REPEAT STRIP_TAC 1359 THEN MATCH_MP_TAC (REWRITE_RULE[AND_IMP_INTRO] 1360 (CONV_RULE (TOP_DEPTH_CONV RIGHT_IMP_FORALL_CONV) 1361 (CONJUNCT1 ALPHA1_SUB))) 1362 THEN EXISTS_TAC ���[]:var list��� 1363 THEN EXISTS_TAC ���[]:var list��� 1364 THEN REWRITE_TAC[ALPHA1_REFL] 1365 THEN REWRITE_TAC[ALPHA1_subst] 1366 THEN REWRITE_TAC[LENGTH] 1367 THEN REWRITE_TAC[alpha_match] 1368 THEN REWRITE_TAC[SUB1] 1369 THEN REPEAT GEN_TAC 1370 THEN STRIP_TAC 1371 THEN POP_ASSUM (REWRITE_ALL_THM o SYM) 1372 THEN POP_TAC 1373 THEN UNDISCH_LAST_TAC 1374 THEN UNDISCH_LAST_TAC 1375 THEN POP_ASSUM (STRIP_ASSUME_TAC o SPEC ���FV_obj1 (SUB1 s x')���) 1376 THENL 1377 [ POP_ASSUM (STRIP_ASSUME_TAC o SPEC ���x':var���) 1378 THENL (* 3 subgoals *) 1379 [ UNDISCH_LAST_TAC 1380 THEN REWRITE_TAC[], 1381 1382 REPEAT STRIP_TAC 1383 THEN RES_TAC, 1384 1385 POP_ASSUM (REWRITE_THM o SYM) 1386 THEN REPEAT STRIP_TAC 1387 THEN POP_ASSUM REWRITE_THM 1388 THEN REWRITE_TAC[ALPHA1_object_pos,alpha_match] 1389 ], 1390 1391 DISCH_THEN (STRIP_ASSUME_TAC o SPEC ���FV_obj1 (SUB1 s x')���) 1392 THENL 1393 [ POP_ASSUM (STRIP_ASSUME_TAC o SPEC ���x':var���) 1394 THENL (* 3 subgoals *) 1395 [ UNDISCH_LAST_TAC 1396 THEN REWRITE_TAC[], 1397 1398 REPEAT STRIP_TAC 1399 THEN RES_TAC, 1400 1401 POP_ASSUM REWRITE_THM 1402 THEN REPEAT STRIP_TAC 1403 THEN POP_ASSUM REWRITE_THM 1404 THEN REWRITE_TAC[ALPHA1_object_pos,alpha_match] 1405 ], 1406 1407 STRIP_TAC 1408 THEN COND_CASES_TAC 1409 THENL 1410 [ REWRITE_TAC[ALPHA1_object_pos,alpha_match], 1411 1412 REWRITE_TAC[] 1413 THEN DEP_REWRITE_TAC[CONJUNCT1 ALPHA1_EXTRANEOUS_CONTEXT] 1414 THEN ASM_REWRITE_TAC[ALPHA1_REFL] 1415 ] 1416 ] 1417 ] 1418 ); 1419 1420 1421 1422val obj_SUB_distinct = store_thm 1423 ("obj_SUB_distinct", 1424 ���(!d xs ys x. ~(OBJ1 d = SUB1 (xs // ys) x)) /\ 1425 (!o' l xs ys x. ~(INVOKE1 o' l = SUB1 (xs // ys) x)) /\ 1426 (!o' l m xs ys x. ~(UPDATE1 o' l m = SUB1 (xs // ys) x)) /\ 1427 (!d xs ys x. ~(SUB1 (xs // ys) x = OBJ1 d)) /\ 1428 (!o' l xs ys x. ~(SUB1 (xs // ys) x = INVOKE1 o' l)) /\ 1429 (!o' l m xs ys x. ~(SUB1 (xs // ys) x = UPDATE1 o' l m))���, 1430 REPEAT CONJ_TAC 1431 THEN REPEAT GEN_TAC 1432 THEN STRIP_ASSUME_TAC (SPEC_ALL SUB_vsubst_OVAR1) 1433 THEN ASM_REWRITE_TAC[object1_distinct] 1434 ); 1435 1436 1437val FREE_SUBST = store_thm 1438 ("FREE_SUBST", 1439 ���(!a s. 1440 DISJOINT (FV_obj1 a) (BV_subst s) ==> ((a <[ s) = a)) /\ 1441 (!d s. 1442 DISJOINT (FV_dict1 d) (BV_subst s) ==> ((d <[ s) = d)) /\ 1443 (!e s. 1444 DISJOINT (FV_entry1 e) (BV_subst s) ==> ((e <[ s) = e)) /\ 1445 (!m s. 1446 DISJOINT (FV_method1 m) (BV_subst s) ==> ((m <[ s) = m))���, 1447 MUTUAL_INDUCT_THEN obj1_induction ASSUME_TAC 1448 THEN REWRITE_TAC[FV_object1_def,SUB_object1_def] 1449 THEN CONV_TAC (DEPTH_CONV let_CONV) 1450 THEN REWRITE_TAC[DISJOINT_UNION,object1_one_one] 1451 THEN ASM_REWRITE_TAC[] 1452 THEN REPEAT STRIP_TAC 1453 THEN RES_TAC 1454 THENL 1455 [ IMP_RES_TAC FREE_SUB1 1456 THEN POP_ASSUM MATCH_MP_TAC 1457 THEN REWRITE_TAC[IN], 1458 1459 IMP_RES_TAC FREE_IDENT_SUBST1 1460 THEN POP_ASSUM REWRITE_THM 1461 THEN MATCH_MP_TAC variant_ident 1462 THEN REWRITE_TAC[IN_DIFF,IN] 1463 THEN MATCH_MP_TAC FINITE_DIFF 1464 THEN REWRITE_TAC[FINITE_FV_object1], 1465 1466 IMP_RES_TAC FREE_IDENT_SUBST1 1467 THEN POP_ASSUM REWRITE_THM 1468 THEN DEP_REWRITE_TAC[variant_ident] 1469 THEN DEP_REWRITE_TAC[FINITE_DIFF] 1470 THEN REWRITE_TAC[FINITE_FV_object1,IN_DIFF,IN] 1471 THEN MATCH_MP_TAC (CONJUNCT1 subst_IDENT1) 1472 THEN GEN_TAC 1473 THEN DISCH_TAC 1474 THEN REWRITE_TAC[SUB1] 1475 THEN COND_CASES_TAC 1476 THENL 1477 [ ASM_REWRITE_TAC[], 1478 1479 IMP_RES_TAC FREE_SUB1 1480 THEN POP_ASSUM MATCH_MP_TAC 1481 THEN ASM_REWRITE_TAC[IN_DIFF,IN] 1482 THEN FIRST_ASSUM (REWRITE_THM o GSYM) 1483 ] 1484 ] 1485 ); 1486 1487 1488val BLOCKED_SUBST = store_thm 1489 ("BLOCKED_SUBST", 1490 ���!o' x o1. 1491 (SIGMA1 x o' <[ [x,o1]) = SIGMA1 x o'���, 1492 REPEAT GEN_TAC 1493 THEN REWRITE_TAC[SUB_object1_def] 1494 THEN DEP_REWRITE_TAC[variant_ident] 1495 THEN DEP_REWRITE_TAC[FINITE_FV_subst1] 1496 THEN DEP_REWRITE_TAC[FINITE_DIFF] 1497 THEN REWRITE_TAC[FINITE_FV_object1] 1498 THEN DEP_REWRITE_TAC[FV_subst_IDENT1] 1499 THEN REWRITE_TAC[IN_DIFF,IN] 1500 THEN CONJ_TAC 1501 THENL 1502 [ REPEAT STRIP_TAC 1503 THEN REWRITE_TAC[SUB1] 1504 THEN FIRST_ASSUM REWRITE_THM, 1505 1506 CONV_TAC (DEPTH_CONV let_CONV) 1507 THEN REWRITE_TAC[object1_one_one] 1508 THEN DEP_REWRITE_TAC[subst_IDENT1] 1509 THEN REPEAT STRIP_TAC 1510 THEN REWRITE_TAC[SUB1] 1511 THEN COND_CASES_TAC 1512 THEN ASM_REWRITE_TAC[] 1513 ] 1514 ); 1515 1516 1517val PARTIALLY_BLOCKED_SUBST = store_thm 1518 ("PARTIALLY_BLOCKED_SUBST", 1519 ���!xs ys x y o'. 1520 (LENGTH xs = LENGTH ys) ==> 1521 (SIGMA1 x o' <[ (APPEND xs [x] // APPEND ys [y]) = 1522 SIGMA1 x o' <[ (xs // ys))���, 1523 REPEAT STRIP_TAC 1524 THEN MATCH_MP_TAC (hd (rev (CONJUNCTS subst_EQ1))) 1525 THEN REWRITE_TAC[FV_object1_def,IN_DIFF,IN] 1526 THEN REPEAT STRIP_TAC 1527 THEN DEP_REWRITE_TAC[SUB_APPEND_vsubst1] 1528 THEN ASM_REWRITE_TAC[] 1529 THEN COND_CASES_TAC 1530 THENL 1531 [ REFL_TAC, 1532 1533 REWRITE_TAC[vsubst1,SUB1] 1534 THEN EVERY_ASSUM (REWRITE_THM o GSYM) 1535 THEN DEP_REWRITE_TAC[SUB_FREE_vsubst1] 1536 THEN ASM_REWRITE_TAC[] 1537 ] 1538 ); 1539 1540 1541(* THe following two theorems are unnecessary. 1542 1543val ALPHA1_DUPLICATE_CONTEXT = store_thm 1544 ("ALPHA1_DUPLICATE_CONTEXT", 1545 ���(!o1 o2 x y xs ys. 1546 ALPHA1_obj o1 o2 (CONS x (CONS x xs)) (CONS y (CONS y ys)) = 1547 ALPHA1_obj o1 o2 (CONS x xs) (CONS y ys)) /\ 1548 (!d1 d2 x y xs ys. 1549 ALPHA1_dict d1 d2 (CONS x (CONS x xs)) (CONS y (CONS y ys)) = 1550 ALPHA1_dict d1 d2 (CONS x xs) (CONS y ys)) /\ 1551 (!e1 e2 x y xs ys. 1552 ALPHA1_entry e1 e2 (CONS x (CONS x xs)) (CONS y (CONS y ys)) = 1553 ALPHA1_entry e1 e2 (CONS x xs) (CONS y ys)) /\ 1554 (!m1 m2 x y xs ys. 1555 ALPHA1_method m1 m2 (CONS x (CONS x xs)) (CONS y (CONS y ys)) = 1556 ALPHA1_method m1 m2 (CONS x xs) (CONS y ys))���, 1557 REPEAT STRIP_TAC 1558 THENL (map MATCH_MP_TAC (CONJUNCTS ALPHA1_FREE_CONTEXT)) 1559 THEN REWRITE_TAC[LENGTH,INV_SUC_EQ] 1560 THEN REPEAT STRIP_TAC 1561 THEN REWRITE_TAC[vsubst1,SUB1] 1562 THEN COND_CASES_TAC 1563 THEN REWRITE_TAC[] 1564 ); 1565 1566 1567val ALPHA1_INNOCUOUS_SUBST = store_thm 1568 ("ALPHA1_INNOCUOUS_SUBST", 1569 ���(!o' x y xs ys. 1570 ~(x IN SL ys) /\ 1571 ALPHA1_obj (o' <[ (APPEND ys [x] // APPEND xs [y])) o' xs ys ==> 1572 ((x = y) \/ ~(x IN FV_obj1 o'))) /\ 1573 (!d x y xs ys. 1574 ~(x IN SL ys) /\ 1575 ALPHA1_dict (d <[ (APPEND ys [x] // APPEND xs [y])) d xs ys ==> 1576 ((x = y) \/ ~(x IN FV_dict1 d))) /\ 1577 (!e x y xs ys. 1578 ~(x IN SL ys) /\ 1579 ALPHA1_entry (e <[ (APPEND ys [x] // APPEND xs [y])) e xs ys ==> 1580 ((x = y) \/ ~(x IN FV_entry1 e))) /\ 1581 (!m x y xs ys. 1582 ~(x IN SL ys) /\ 1583 ALPHA1_method (m <[ (APPEND ys [x] // APPEND xs [y])) m xs ys ==> 1584 ((x = y) \/ ~(x IN FV_method1 m)))���, 1585 MUTUAL_INDUCT_THEN obj1_induction ASSUME_TAC 1586 THEN REWRITE_TAC[SUB_object1_def,FV_object1_def,IN_UNION,IN] 1587 THEN CONV_TAC (DEPTH_CONV let_CONV) 1588 THEN REWRITE_TAC[ALPHA1_object_pos] 1589 THEN REPEAT STRIP_TAC 1590 THEN RES_TAC 1591 THEN ASM_REWRITE_TAC[] 1592 THENL 1593 [ ASM_CASES_TAC ���(x:var) = v��� 1594 THEN ASM_REWRITE_TAC[] 1595 THEN POP_ASSUM (REWRITE_ALL_THM o SYM) 1596 THEN IMP_RES_TAC ALPHA1_LENGTH 1597 THEN POP_ASSUM (fn th1 => 1598 POP_ASSUM (fn th2 => 1599 ASSUME_TAC th1 THEN MP_TAC th2)) 1600 THEN DEP_REWRITE_TAC[SUB_APPEND_FREE_vsubst1] 1601 THEN ASM_REWRITE_TAC[] 1602 THEN REWRITE_TAC[SUB1,vsubst1] 1603 THEN REWRITE_TAC[ALPHA1_object_pos] 1604 THEN REWRITE_TAC[alpha_match_SUB_var] 1605 THEN STRIP_TAC 1606 THEN UNDISCH_LAST_TAC 1607 THEN DEP_REWRITE_TAC[SUB_FREE_vsubst1] 1608 THEN ASM_REWRITE_TAC[object1_one_one], 1609 1610 POP_TAC 1611 THEN UNDISCH_LAST_TAC 1612 THEN DEFINE_NEW_VAR 1613 ���v' = variant v (FV_subst1 (APPEND ys [x] // APPEND xs [y]) 1614 (FV_obj1 o' DIFF {v}))��� 1615 THEN FIRST_ASSUM (REWRITE_THM o SYM) 1616 THEN DISCH_TAC 1617 THEN ASM_CASES_TAC ���(x:var) = v��� 1618 THENL 1619 [ POP_ASSUM REWRITE_THM 1620 THEN REWRITE_TAC[IN_DIFF,IN], 1621 1622 FIRST_ASSUM (MP_TAC o 1623 REWRITE_RULE[SUB1] o 1624 SPECL[���x:var���,���y:var���, 1625 ���CONS (v':var) xs���,���CONS (v:var) ys���]) 1626 THEN REWRITE_TAC[SL,IN] 1627 THEN FIRST_ASSUM REWRITE_THM 1628 THEN UNDISCH_ALL_TAC 1629 THEN DISCH_TAC 1630 THEN POP_TAC 1631 THEN DISCH_TAC 1632 THEN DISCH_TAC 1633 THEN REWRITE_TAC[APPEND,vsubst1] 1634 THEN DISCH_THEN REWRITE_THM 1635 THEN REWRITE_TAC[IN_DIFF,IN,DE_MORGAN_THM] 1636 THEN DISCH_THEN ASM_REWRITE_THM 1637 ] 1638 ] 1639 ); 1640 1641*) 1642 1643 1644 1645val ALPHA1_SWITCH_OVAR1 = TAC_PROOF(([], 1646 ���!xs xs' ys ys' x y u v. 1647 (LENGTH xs = LENGTH xs') /\ 1648 (LENGTH xs' = LENGTH ys) /\ 1649 (LENGTH ys = LENGTH ys') /\ 1650 ALPHA1_obj (SUB1 (APPEND xs [x] // APPEND xs' [y]) u) 1651 (OVAR1 v) xs' ys /\ 1652 ALPHA1_obj (OVAR1 u) 1653 (SUB1 (APPEND ys [y] // APPEND ys' [x]) v) xs ys' 1654 ==> 1655 ALPHA1_obj (OVAR1 u) (OVAR1 v) (APPEND xs [x]) (APPEND ys [y])���), 1656 LIST_INDUCT_TAC 1657 THENL 1658 [ LIST_INDUCT_TAC 1659 THEN REWRITE_TAC[LENGTH,SUC_NOT] 1660 THEN LIST_INDUCT_TAC 1661 THEN REWRITE_TAC[LENGTH,SUC_NOT] 1662 THEN LIST_INDUCT_TAC 1663 THEN REWRITE_TAC[LENGTH,SUC_NOT] 1664 THEN REWRITE_TAC[APPEND,vsubst1,SUB1] 1665 THEN REPEAT GEN_TAC 1666 THEN COND_CASES_TAC 1667 THEN COND_CASES_TAC 1668 THEN REWRITE_TAC[ALPHA1_object_pos] 1669 THEN REWRITE_TAC[alpha_match_SUB_var] 1670 THEN REWRITE_TAC[vsubst1,SUB1] 1671 THEN ASM_REWRITE_TAC[object1_one_one,LENGTH], 1672 1673 GEN_TAC 1674 THEN LIST_INDUCT_TAC 1675 THEN REWRITE_TAC[LENGTH,NOT_SUC] 1676 THEN POP_TAC 1677 THEN GEN_TAC 1678 THEN LIST_INDUCT_TAC 1679 THEN REWRITE_TAC[LENGTH,NOT_SUC] 1680 THEN POP_TAC 1681 THEN GEN_TAC 1682 THEN LIST_INDUCT_TAC 1683 THEN REWRITE_TAC[LENGTH,NOT_SUC] 1684 THEN POP_TAC 1685 THEN X_GEN_TAC ���x1:var��� 1686 THEN X_GEN_TAC ���x2:var��� 1687 THEN REPEAT GEN_TAC 1688 THEN REWRITE_TAC[INV_SUC_EQ] 1689 THEN STRIP_TAC 1690 THEN UNDISCH_LAST_TAC 1691 THEN UNDISCH_LAST_TAC 1692 THEN REWRITE_TAC[APPEND,vsubst1,SUB1] 1693 THEN COND_CASES_TAC 1694 THEN POP_ASSUM (ASSUME_TAC o GSYM) 1695 THEN COND_CASES_TAC 1696 THEN POP_ASSUM (ASSUME_TAC o GSYM) 1697 THENL (* 4 subgoals *) 1698 [ REWRITE_TAC[ALPHA1_object_pos] 1699 THEN REWRITE_TAC[alpha_match_SUB_var] 1700 THEN ASM_REWRITE_TAC[LENGTH,LENGTH_APPEND,vsubst1,SUB1], 1701 1702 REWRITE_TAC[ALPHA1_object_pos] 1703 THEN REWRITE_TAC[alpha_match_SUB_var] 1704 THEN REWRITE_TAC[vsubst1,SUB1] 1705 THEN ASM_REWRITE_TAC[object1_one_one], 1706 1707 REWRITE_TAC[ALPHA1_object_pos] 1708 THEN REWRITE_TAC[alpha_match_SUB_var] 1709 THEN REWRITE_TAC[vsubst1,SUB1] 1710 THEN ASM_REWRITE_TAC[object1_one_one], 1711 1712 ASM_CASES_TAC 1713 ���SUB1 (APPEND xs [x2] // APPEND xs' [y]) u = OVAR1 x'��� 1714 THEN TRY (POP_ASSUM REWRITE_THM 1715 THEN REWRITE_TAC[ALPHA1_object_pos] 1716 THEN REWRITE_TAC[alpha_match_SUB_var] 1717 THEN REWRITE_TAC[vsubst1,SUB1] 1718 THEN ASM_REWRITE_TAC[object1_one_one] 1719 THEN NO_TAC) 1720 THEN ASM_CASES_TAC 1721 ���SUB1 (APPEND ys [y] // APPEND ys' [x2]) v = OVAR1 x1��� 1722 THEN TRY (FIRST_ASSUM REWRITE_THM 1723 THEN REWRITE_TAC[ALPHA1_object_pos] 1724 THEN REWRITE_TAC[alpha_match_SUB_var] 1725 THEN REWRITE_TAC[vsubst1,SUB1] 1726 THEN ASM_REWRITE_TAC[object1_one_one] 1727 THEN NO_TAC) 1728 THEN DEP_REWRITE_TAC[ALPHA1_EXTRANEOUS_CONTEXT] 1729 THEN ASM_REWRITE_TAC[FV_object1_def,IN,IN_FV_SUB_vsubst1] 1730 THEN REPEAT DISCH_TAC 1731 THEN FIRST_ASSUM MATCH_MP_TAC 1732 THEN EXISTS_TAC ���xs':var list��� 1733 THEN EXISTS_TAC ���ys':var list��� 1734 THEN ASM_REWRITE_TAC[] 1735 ] 1736 ] 1737 ); 1738 1739 1740 1741val ALPHA1_SWITCH_LEMMA = TAC_PROOF(([], 1742 ���(!o3 o2 xs' ys. 1743 ALPHA1_obj o3 o2 xs' ys ==> 1744 (!o1 x y xs ys'. 1745 (LENGTH xs = LENGTH xs') /\ (LENGTH ys = LENGTH ys') /\ 1746 (o3 = (o1 <[ (APPEND xs [x] // APPEND xs' [y]))) /\ 1747 ALPHA1_obj o1 (o2 <[ (APPEND ys [y] // APPEND ys' [x])) xs ys' 1748 ==> 1749 ALPHA1_obj o1 o2 (APPEND xs [x]) (APPEND ys [y]))) /\ 1750 (!d3 d2 xs' ys. 1751 ALPHA1_dict d3 d2 xs' ys ==> 1752 (!d1 x y xs ys'. 1753 (LENGTH xs = LENGTH xs') /\ (LENGTH ys = LENGTH ys') /\ 1754 (d3 = (d1 <[ (APPEND xs [x] // APPEND xs' [y]))) /\ 1755 ALPHA1_dict d1 (d2 <[ (APPEND ys [y] // APPEND ys' [x])) xs ys' 1756 ==> 1757 ALPHA1_dict d1 d2 (APPEND xs [x]) (APPEND ys [y]))) /\ 1758 (!e3 e2 xs' ys. 1759 ALPHA1_entry e3 e2 xs' ys ==> 1760 (!e1 x y xs ys'. 1761 (LENGTH xs = LENGTH xs') /\ (LENGTH ys = LENGTH ys') /\ 1762 (e3 = (e1 <[ (APPEND xs [x] // APPEND xs' [y]))) /\ 1763 ALPHA1_entry e1 (e2 <[ (APPEND ys [y] // APPEND ys' [x])) xs ys' 1764 ==> 1765 ALPHA1_entry e1 e2 (APPEND xs [x]) (APPEND ys [y]))) /\ 1766 (!m3 m2 xs' ys. 1767 ALPHA1_method m3 m2 xs' ys ==> 1768 (!m1 x y xs ys'. 1769 (LENGTH xs = LENGTH xs') /\ (LENGTH ys = LENGTH ys') /\ 1770 (m3 = (m1 <[ (APPEND xs [x] // APPEND xs' [y]))) /\ 1771 ALPHA1_method m1 (m2 <[ (APPEND ys [y] // APPEND ys' [x])) xs ys' 1772 ==> 1773 ALPHA1_method m1 m2 (APPEND xs [x]) (APPEND ys [y])))���), 1774 rule_induct ALPHA1_strong_ind 1775 THEN REPEAT STRIP_TAC 1776 THEN UNDISCH_LAST_TAC 1777 THEN UNDISCH_LAST_TAC 1778 THENL (* 8 subgoals *) 1779 [ STRIP_ASSUME_TAC (SPEC ���o1:obj1��� obj1_cases) 1780 (* four subgoals *) 1781 THEN POP_ASSUM REWRITE_THM 1782 THEN REWRITE_TAC[SUB_object1_def] 1783 THEN REWRITE_TAC[object1_distinct] 1784 (* one subgoal *) 1785 THEN REPEAT DISCH_TAC 1786 THEN MATCH_MP_TAC ALPHA1_SWITCH_OVAR1 1787 THEN EXISTS_TAC ���xs:var list��� 1788 THEN EXISTS_TAC ���ys':var list��� 1789 THEN IMP_RES_TAC alpha_match_LENGTH 1790 THEN ASM_REWRITE_TAC[] 1791 THEN POP_TAC 1792 THEN UNDISCH_LAST_TAC 1793 THEN FIRST_ASSUM (REWRITE_THM o SYM) 1794 THEN ASM_REWRITE_TAC[ALPHA1_object_pos], 1795 1796 1797 STRIP_ASSUME_TAC (SPEC ���o1:obj1��� obj1_cases) 1798 (* four subgoals *) 1799 THEN POP_ASSUM REWRITE_THM 1800 THEN REWRITE_TAC[SUB_object1_def] 1801 THEN REWRITE_TAC[object1_distinct,obj_SUB_distinct] 1802 (* one subgoal *) 1803 THEN REWRITE_TAC[object1_one_one] 1804 THEN DISCH_TAC 1805 THEN REWRITE_TAC[ALPHA1_object_pos] 1806 THEN DISCH_TAC 1807 THEN RES_TAC, 1808 1809 STRIP_ASSUME_TAC (SPEC ���o1':obj1��� obj1_cases) 1810 (* four subgoals *) 1811 THEN POP_ASSUM REWRITE_THM 1812 THEN REWRITE_TAC[SUB_object1_def] 1813 THEN REWRITE_TAC[object1_distinct,obj_SUB_distinct] 1814 (* one subgoal *) 1815 THEN REWRITE_TAC[object1_one_one] 1816 THEN STRIP_TAC 1817 THEN REWRITE_TAC[ALPHA1_object_pos] 1818 THEN STRIP_TAC 1819 THEN POP_ASSUM REWRITE_THM 1820 THEN RES_TAC, 1821 1822 STRIP_ASSUME_TAC (SPEC ���o1':obj1��� obj1_cases) 1823 (* four subgoals *) 1824 THEN POP_ASSUM REWRITE_THM 1825 THEN REWRITE_TAC[SUB_object1_def] 1826 THEN REWRITE_TAC[object1_distinct,obj_SUB_distinct] 1827 (* one subgoal *) 1828 THEN REWRITE_TAC[object1_one_one] 1829 THEN STRIP_TAC 1830 THEN REWRITE_TAC[ALPHA1_object_pos] 1831 THEN STRIP_TAC 1832 THEN FIRST_ASSUM (REWRITE_THM o SYM) 1833 THEN RES_TAC 1834 THEN ASM_REWRITE_TAC[], 1835 1836 STRIP_ASSUME_TAC (SPEC ���d1':^dict1��� dict1_cases) 1837 (* two subgoals *) 1838 THEN POP_ASSUM REWRITE_THM 1839 THEN REWRITE_TAC[SUB_object1_def] 1840 THEN REWRITE_TAC[object1_distinct] 1841 (* one subgoal *) 1842 THEN REWRITE_TAC[object1_one_one] 1843 THEN STRIP_TAC 1844 THEN REWRITE_TAC[ALPHA1_object_pos] 1845 THEN STRIP_TAC 1846 THEN RES_TAC 1847 THEN ASM_REWRITE_TAC[], 1848 1849 STRIP_ASSUME_TAC (SPEC ���d1:^dict1��� dict1_cases) 1850 (* two subgoals *) 1851 THEN POP_ASSUM REWRITE_THM 1852 THEN REWRITE_TAC[SUB_object1_def] 1853 THEN REWRITE_TAC[object1_distinct] 1854 (* one subgoal *) 1855 THEN ASM_REWRITE_TAC[ALPHA1_object_pos,LENGTH,LENGTH_APPEND], 1856 1857 STRIP_ASSUME_TAC (SPEC ���e1:^entry1��� entry1_cases) 1858 THEN POP_ASSUM REWRITE_THM 1859 THEN REWRITE_TAC[SUB_object1_def] 1860 THEN REWRITE_TAC[object1_one_one] 1861 THEN STRIP_TAC 1862 THEN ASM_REWRITE_TAC[ALPHA1_object_pos] 1863 THEN STRIP_TAC 1864 THEN RES_TAC, 1865 1866 STRIP_ASSUME_TAC (SPEC ���m1:method1��� method1_cases) 1867 THEN POP_ASSUM REWRITE_THM 1868 THEN REWRITE_TAC[SUB_object1_def] 1869 THEN CONV_TAC (DEPTH_CONV let_CONV) 1870 THEN REWRITE_TAC[object1_one_one] 1871 THEN STRIP_TAC 1872 THEN REWRITE_TAC[ALPHA1_object_pos] 1873 THEN DISCH_TAC 1874 THEN REWRITE_TAC[GSYM (CONJUNCT2 APPEND)] 1875 THEN FIRST_ASSUM MATCH_MP_TAC 1876 THEN EXISTS_TAC ���CONS 1877 (variant y 1878 (FV_subst1 (APPEND ys [y'] // APPEND ys' [x']) 1879 (FV_obj1 o2 DIFF {y}))) 1880 ys'��� 1881 THEN ASM_REWRITE_TAC[LENGTH,APPEND,vsubst1,SL,IN] 1882 ] 1883 ); 1884 1885 1886val ALPHA1_SWITCH = store_thm 1887 ("ALPHA1_SWITCH", 1888 ���(!o1 o2 xs xs' ys ys' x y. 1889 (LENGTH xs = LENGTH xs') /\ (LENGTH ys = LENGTH ys') /\ 1890 ALPHA1_obj (o1 <[ (APPEND xs [x] // APPEND xs' [y])) o2 xs' ys /\ 1891 ALPHA1_obj o1 (o2 <[ (APPEND ys [y] // APPEND ys' [x])) xs ys' 1892 ==> 1893 ALPHA1_obj o1 o2 (APPEND xs [x]) (APPEND ys [y])) /\ 1894 (!d1 d2 xs xs' ys ys' x y. 1895 (LENGTH xs = LENGTH xs') /\ (LENGTH ys = LENGTH ys') /\ 1896 ALPHA1_dict (d1 <[ (APPEND xs [x] // APPEND xs' [y])) d2 xs' ys /\ 1897 ALPHA1_dict d1 (d2 <[ (APPEND ys [y] // APPEND ys' [x])) xs ys' 1898 ==> 1899 ALPHA1_dict d1 d2 (APPEND xs [x]) (APPEND ys [y])) /\ 1900 (!e1 e2 xs xs' ys ys' x y. 1901 (LENGTH xs = LENGTH xs') /\ (LENGTH ys = LENGTH ys') /\ 1902 ALPHA1_entry (e1 <[ (APPEND xs [x] // APPEND xs' [y])) e2 xs' ys /\ 1903 ALPHA1_entry e1 (e2 <[ (APPEND ys [y] // APPEND ys' [x])) xs ys' 1904 ==> 1905 ALPHA1_entry e1 e2 (APPEND xs [x]) (APPEND ys [y])) /\ 1906 (!m1 m2 xs xs' ys ys' x y. 1907 (LENGTH xs = LENGTH xs') /\ (LENGTH ys = LENGTH ys') /\ 1908 ALPHA1_method (m1 <[ (APPEND xs [x] // APPEND xs' [y])) m2 xs' ys/\ 1909 ALPHA1_method m1 (m2 <[ (APPEND ys [y] // APPEND ys' [x])) xs ys' 1910 ==> 1911 ALPHA1_method m1 m2 (APPEND xs [x]) (APPEND ys [y]))���, 1912 REPEAT STRIP_TAC 1913 THENL (map (MATCH_MP_TAC o 1914 REWRITE_RULE[AND_IMP_INTRO] o 1915 CONV_RULE (TOP_DEPTH_CONV RIGHT_IMP_FORALL_CONV)) 1916 (CONJUNCTS ALPHA1_SWITCH_LEMMA)) 1917 THENL 1918 [ EXISTS_TAC ���(o1: obj1) <[ (APPEND xs [x] // APPEND xs' [y])���, 1919 EXISTS_TAC ���(d1:^dict1) <[ (APPEND xs [x] // APPEND xs' [y])���, 1920 EXISTS_TAC ���(e1:^entry1) <[ (APPEND xs [x] // APPEND xs' [y])���, 1921 EXISTS_TAC ���(m1: method1) <[ (APPEND xs [x] // APPEND xs' [y])��� 1922 ] 1923 THEN EXISTS_TAC ���xs':var list��� 1924 THEN EXISTS_TAC ���ys':var list��� 1925 THEN ASM_REWRITE_TAC[] 1926 ); 1927 1928 1929val ALPHA1_SIGMA_subst = store_thm 1930 ("ALPHA1_SIGMA_subst", 1931 ���!o1 o2 x y a. 1932 ALPHA1_method (SIGMA1 x o1) (SIGMA1 y o2) [] [] ==> 1933 (ALPHA1_obj (o1 <[ [x, a]) (o2 <[ [y, a]) [] [])���, 1934 REWRITE_TAC[ALPHA1_object_pos] 1935 THEN REPEAT GEN_TAC 1936 THEN DISCH_TAC 1937 THEN IMP_RES_TAC (CONJUNCT1 ALPHA1_SUB) 1938 THEN POP_ASSUM MATCH_MP_TAC 1939 THEN REWRITE_TAC[ALPHA1_subst] 1940 THEN REWRITE_TAC[alpha_match] 1941 THEN REWRITE_TAC[SUB1] 1942 THEN REPEAT GEN_TAC 1943 THEN STRIP_TAC 1944 THEN ASM_REWRITE_TAC[ALPHA1_REFL] 1945 ); 1946 1947 1948val ALPHA1_method_one_one = store_thm 1949 ("ALPHA1_method_one_one", 1950 ���!o1 o2 x y. 1951 ALPHA1_method (SIGMA1 x o1) (SIGMA1 y o2) [] [] = 1952 (ALPHA1_obj (o1 <[ [x, OVAR1 y]) o2 [] [] /\ 1953 ALPHA1_obj o1 (o2 <[ [y, OVAR1 x]) [] [])���, 1954 REPEAT GEN_TAC 1955 THEN EQ_TAC 1956 THENL 1957 [ STRIP_TAC 1958 THEN IMP_RES_TAC ALPHA1_SYM 1959 THEN IMP_RES_THEN MP_TAC ALPHA1_SIGMA_subst 1960 THEN DISCH_THEN (ASSUME_TAC o SPEC ���OVAR1 y���) 1961 THEN DISCH_THEN (MP_TAC o SPEC ���OVAR1 x���) 1962 THEN POP_ASSUM MP_TAC 1963 THEN REWRITE_TAC[subst_SAME_ONE1] 1964 THEN REPEAT DISCH_TAC 1965 THEN IMP_RES_TAC ALPHA1_SYM 1966 THEN ASM_REWRITE_TAC[], 1967 1968 REWRITE_TAC[ALPHA1_object_pos] 1969 THEN REPEAT STRIP_TAC 1970 THEN ONCE_REWRITE_TAC[GSYM (CONJUNCT1 APPEND)] 1971 THEN MATCH_MP_TAC (CONJUNCT1 ALPHA1_SWITCH) 1972 THEN EXISTS_TAC ���[]:var list��� 1973 THEN EXISTS_TAC ���[]:var list��� 1974 THEN ASM_REWRITE_TAC[LENGTH,APPEND,vsubst1] 1975 ] 1976 ); 1977 1978 1979 1980(* ========================================================== *) 1981(* Now we define the alpha-equivalence predicates themselves. *) 1982(* ========================================================== *) 1983 1984val ALPHA_obj = 1985 new_definition ("ALPHA_obj", 1986 ���ALPHA_obj o1 o2 = ALPHA1_obj o1 o2 [] []���); 1987 1988val ALPHA_dict = 1989 new_definition ("ALPHA_dict", 1990 ���ALPHA_dict d1 d2 = ALPHA1_dict d1 d2 [] []���); 1991 1992val ALPHA_entry = 1993 new_definition ("ALPHA_entry", 1994 ���ALPHA_entry e1 e2 = ALPHA1_entry e1 e2 [] []���); 1995 1996val ALPHA_method = 1997 new_definition ("ALPHA_method", 1998 ���ALPHA_method m1 m2 = ALPHA1_method m1 m2 [] []���); 1999 2000 2001val ALPHA_object = store_thm 2002 ("ALPHA_object", 2003 ���(!o1 o2. ALPHA_obj o1 o2 = ALPHA1_obj o1 o2 [] []) /\ 2004 (!d1 d2. ALPHA_dict d1 d2 = ALPHA1_dict d1 d2 [] []) /\ 2005 (!e1 e2. ALPHA_entry e1 e2 = ALPHA1_entry e1 e2 [] []) /\ 2006 (!m1 m2. ALPHA_method m1 m2 = ALPHA1_method m1 m2 [] [])���, 2007 REWRITE_TAC[ALPHA_obj,ALPHA_dict,ALPHA_entry,ALPHA_method] 2008 ); 2009 2010 2011val ALPHA_HEIGHT = store_thm 2012 ("ALPHA_HEIGHT", 2013 ���(!o1 o2. ALPHA_obj o1 o2 ==> 2014 (HEIGHT_obj1 o1 = HEIGHT_obj1 o2)) /\ 2015 (!d1 d2. ALPHA_dict d1 d2 ==> 2016 (HEIGHT_dict1 d1 = HEIGHT_dict1 d2)) /\ 2017 (!e1 e2. ALPHA_entry e1 e2 ==> 2018 (HEIGHT_entry1 e1 = HEIGHT_entry1 e2)) /\ 2019 (!m1 m2. ALPHA_method m1 m2 ==> 2020 (HEIGHT_method1 m1 = HEIGHT_method1 m2))���, 2021 REWRITE_TAC[ALPHA_object,ALPHA1_HEIGHT] 2022 ); 2023 2024 2025val ALPHA_object_similar = store_thm 2026 ("ALPHA_object_similar", 2027 ���(!x a. ALPHA_obj (OVAR1 x) a ==> (?y. a = OVAR1 y)) /\ 2028 (!d1 a. ALPHA_obj (OBJ1 d1) a ==> (?d2. a = OBJ1 d2)) /\ 2029 (!o1 l1 a. ALPHA_obj (INVOKE1 o1 l1) a ==> 2030 (?o2 l2. a = INVOKE1 o2 l2)) /\ 2031 (!o1 l1 m1 a. ALPHA_obj (UPDATE1 o1 l1 m1) a ==> 2032 (?o2 l2 m2. a = UPDATE1 o2 l2 m2)) /\ 2033 (!e1 d1 d. ALPHA_dict (CONS e1 d1) d ==> 2034 (?e2 d2. d = CONS e2 d2)) /\ 2035 (!d. ALPHA_dict NIL d ==> (d = NIL)) /\ 2036 (!l1 m1 e. ALPHA_entry (l1,m1) e ==> 2037 (?l2 m2. e = (l2,m2))) /\ 2038 (!x1 o1 m. ALPHA_method (SIGMA1 x1 o1) m ==> 2039 (?x2 o2. m = SIGMA1 x2 o2))���, 2040 REWRITE_TAC[ALPHA_object,ALPHA1_object_similar] 2041 ); 2042 2043 2044val ALPHA_REFL = store_thm 2045 ("ALPHA_REFL", 2046 ���(!a. ALPHA_obj a a) /\ 2047 (!d. ALPHA_dict d d) /\ 2048 (!e. ALPHA_entry e e) /\ 2049 (!m. ALPHA_method m m)���, 2050 REWRITE_TAC[ALPHA_object,ALPHA1_REFL] 2051 ); 2052 2053 2054val ALPHA_SYM = store_thm 2055 ("ALPHA_SYM", 2056 ���(!o1 o2. ALPHA_obj o1 o2 = ALPHA_obj o2 o1) /\ 2057 (!d1 d2. ALPHA_dict d1 d2 = ALPHA_dict d2 d1) /\ 2058 (!e1 e2. ALPHA_entry e1 e2 = ALPHA_entry e2 e1) /\ 2059 (!m1 m2. ALPHA_method m1 m2 = ALPHA_method m2 m1)���, 2060 REWRITE_TAC[ALPHA_object] 2061 THEN REPEAT STRIP_TAC 2062 THEN EQ_TAC 2063 THEN DISCH_THEN (REWRITE_THM o ONCE_REWRITE_RULE[ALPHA1_SYM]) 2064 ); 2065 2066 2067val ALPHA_TRANS = store_thm 2068 ("ALPHA_TRANS", 2069 ���(!o1 o2 o3. ALPHA_obj o1 o2 /\ ALPHA_obj o2 o3 ==> 2070 ALPHA_obj o1 o3) /\ 2071 (!d1 d2 d3. ALPHA_dict d1 d2 /\ ALPHA_dict d2 d3 ==> 2072 ALPHA_dict d1 d3) /\ 2073 (!e1 e2 e3. ALPHA_entry e1 e2 /\ ALPHA_entry e2 e3 ==> 2074 ALPHA_entry e1 e3) /\ 2075 (!m1 m2 m3. ALPHA_method m1 m2 /\ ALPHA_method m2 m3 ==> 2076 ALPHA_method m1 m3)���, 2077 REWRITE_TAC[ALPHA_object,ALPHA1_TRANS] 2078 ); 2079 2080 2081val ALPHA_object_pos = store_thm 2082 ("ALPHA_object_pos", 2083 ���(!x y. 2084 ALPHA_obj (OVAR1 x) (OVAR1 y) = (x = y)) /\ 2085 (!d1 d2. 2086 ALPHA_obj (OBJ1 d1) (OBJ1 d2) = ALPHA_dict d1 d2) /\ 2087 (!o1 o2 l1 l2. 2088 ALPHA_obj (INVOKE1 o1 l1) (INVOKE1 o2 l2) = 2089 ALPHA_obj o1 o2 /\ (l1 = l2)) /\ 2090 (!o1 o2 l1 l2 m1 m2. 2091 ALPHA_obj (UPDATE1 o1 l1 m1) (UPDATE1 o2 l2 m2) = 2092 ALPHA_obj o1 o2 /\ (l1 = l2) /\ ALPHA_method m1 m2) /\ 2093 (!e1 e2 d1 d2. 2094 ALPHA_dict (CONS e1 d1) (CONS e2 d2) = 2095 ALPHA_entry e1 e2 /\ ALPHA_dict d1 d2) /\ 2096 (ALPHA_dict [] [] = T) /\ 2097 (!l1 l2 m1 m2. 2098 ALPHA_entry (l1,m1) (l2,m2) = 2099 (l1 = l2) /\ ALPHA_method m1 m2) (* /\ 2100 (!x1 x2 o1 o2. 2101 ALPHA_method (SIGMA1 x1 o1) (SIGMA1 x2 o2) = 2102 ALPHA1_obj o1 o2 [x1] [x2]) *)���, 2103 REWRITE_TAC[ALPHA_object,ALPHA1_object_pos,alpha_match] 2104 ); 2105 2106 2107val ALPHA_method_SIGMA = store_thm 2108 ("ALPHA_method_SIGMA", 2109 ���!x o1 o2. 2110 ALPHA_method (SIGMA1 x o1) (SIGMA1 x o2) = ALPHA_obj o1 o2���, 2111 REWRITE_TAC[ALPHA_object,ALPHA1_object_pos] 2112 THEN REPEAT GEN_TAC 2113 THEN FIRST (map MATCH_MP_TAC (CONJUNCTS ALPHA1_FREE_CONTEXT)) 2114 THEN REWRITE_TAC[vsubst1,SUB1] 2115 THEN REPEAT STRIP_TAC 2116 THEN COND_CASES_TAC 2117 THEN ASM_REWRITE_TAC[] 2118 ); 2119 2120 2121val ALPHA_object_neg = store_thm 2122 ("ALPHA_object_neg", 2123 ���(!x d. ALPHA_obj (OVAR1 x) (OBJ1 d) = F) /\ 2124 (!x a l. ALPHA_obj (OVAR1 x) (INVOKE1 a l) = F) /\ 2125 (!x a l m. ALPHA_obj (OVAR1 x) (UPDATE1 a l m) = F) /\ 2126 (!d x. ALPHA_obj (OBJ1 d) (OVAR1 x) = F) /\ 2127 (!d a l. ALPHA_obj (OBJ1 d) (INVOKE1 a l) = F) /\ 2128 (!d a l m. ALPHA_obj (OBJ1 d) (UPDATE1 a l m) = F) /\ 2129 (!a l x. ALPHA_obj (INVOKE1 a l) (OVAR1 x) = F) /\ 2130 (!a l d. ALPHA_obj (INVOKE1 a l) (OBJ1 d) = F) /\ 2131 (!o1 l1 o2 l2 m2. 2132 ALPHA_obj (INVOKE1 o1 l1) (UPDATE1 o2 l2 m2) = F) /\ 2133 (!a l m x. ALPHA_obj (UPDATE1 a l m) (OVAR1 x) = F) /\ 2134 (!a l m d. ALPHA_obj (UPDATE1 a l m) (OBJ1 d) = F) /\ 2135 (!o1 l1 m1 o2 l2. 2136 ALPHA_obj (UPDATE1 o1 l1 m1) (INVOKE1 o2 l2) = F) 2137 /\ 2138 (!e d. ALPHA_dict (CONS e d) NIL = F) /\ 2139 (!e d. ALPHA_dict NIL (CONS e d) = F)���, 2140 REWRITE_TAC[ALPHA_object,ALPHA1_object_neg] 2141 ); 2142 2143 2144(* --------------------------------------------------------------------- *) 2145(* We claim that ALPHA is a binary relation on the object/method1 *) 2146(* language which is *) 2147(* 1) reflexive *) 2148(* 2) symmetric *) 2149(* 3) transitive *) 2150(* 4) compatible (in the sense of Barendregt, Definition 3.1.1, pg 50 *) 2151(* --------------------------------------------------------------------- *) 2152 2153 2154val ALPHA_FV = store_thm 2155 ("ALPHA_FV", 2156 ���(!o1 o2. ALPHA_obj o1 o2 ==> (FV_obj1 o1 = FV_obj1 o2)) /\ 2157 (!d1 d2. ALPHA_dict d1 d2 ==> (FV_dict1 d1 = FV_dict1 d2)) /\ 2158 (!e1 e2. ALPHA_entry e1 e2 ==> (FV_entry1 e1 = FV_entry1 e2)) /\ 2159 (!m1 m2. ALPHA_method m1 m2 ==> (FV_method1 m1 = FV_method1 m2))���, 2160 REWRITE_TAC[ALPHA_object] 2161 THEN REPEAT STRIP_TAC 2162 THENL (map IMP_RES_TAC (CONJUNCTS ALPHA1_SYM)) 2163 THENL (map IMP_RES_TAC (CONJUNCTS ALPHA1_FV)) 2164 THEN POP_ASSUM MP_TAC 2165 THEN POP_ASSUM MP_TAC 2166 THEN REWRITE_TAC[alpha_match_NIL] 2167 THEN REPEAT STRIP_TAC 2168 THEN REWRITE_TAC[EXTENSION] 2169 THEN GEN_TAC 2170 THEN EQ_TAC 2171 THEN DISCH_TAC 2172 THEN RES_TAC 2173 THEN ASM_REWRITE_TAC[] 2174 ); 2175 2176 2177 2178(* 2179val ALPHA1_subst = 2180 new_definition 2181 ("ALPHA1_subst", 2182 ���ALPHA1_subst xs ys xs' ys' t1 t2 s1 s2 = 2183 (LENGTH xs' = LENGTH ys') /\ 2184 (!x y. (x IN t1) /\ (y IN t2) /\ 2185 alpha_match xs ys x y ==> 2186 ALPHA1_obj (SUB1 s1 x) (SUB1 s2 y) xs' ys')���); 2187*) 2188 2189val ALPHA_subst = 2190 new_definition 2191 ("ALPHA_subst", 2192 ���ALPHA_subst t s1 s2 = 2193 (!x. (x IN t) ==> 2194 ALPHA_obj (SUB1 s1 x) (SUB1 s2 x))���); 2195 2196 2197val ALPHA_SUB_CONTEXT = store_thm 2198 ("ALPHA_SUB_CONTEXT", 2199 ���(!o1 o2 s1 s2. ALPHA_obj o1 o2 /\ 2200 ALPHA_subst (FV_obj1 o1) s1 s2 ==> 2201 ALPHA_obj (o1 <[ s1) (o2 <[ s2)) /\ 2202 (!d1 d2 s1 s2. ALPHA_dict d1 d2 /\ 2203 ALPHA_subst (FV_dict1 d1) s1 s2 ==> 2204 ALPHA_dict (d1 <[ s1) (d2 <[ s2)) /\ 2205 (!e1 e2 s1 s2. ALPHA_entry e1 e2 /\ 2206 ALPHA_subst (FV_entry1 e1) s1 s2 ==> 2207 ALPHA_entry (e1 <[ s1) (e2 <[ s2)) /\ 2208 (!m1 m2 s1 s2. ALPHA_method m1 m2 /\ 2209 ALPHA_subst (FV_method1 m1) s1 s2 ==> 2210 ALPHA_method (m1 <[ s1) (m2 <[ s2))���, 2211 REPEAT STRIP_TAC 2212 THEN IMP_RES_TAC ALPHA_FV 2213 THEN REWRITE_ALL_TAC[ALPHA_object] 2214 THEN FIRST (map (MATCH_MP_TAC o REWRITE_RULE[AND_IMP_INTRO] o 2215 CONV_RULE (TOP_DEPTH_CONV RIGHT_IMP_FORALL_CONV)) 2216 (CONJUNCTS ALPHA1_SUB)) 2217 THEN EXISTS_TAC ���[]:var list��� 2218 THEN EXISTS_TAC ���[]:var list��� 2219 THEN ASM_REWRITE_TAC[] 2220 THEN UNDISCH_ALL_TAC 2221 THEN REWRITE_TAC[ALPHA_subst,ALPHA1_subst] 2222 THEN REWRITE_TAC[ALPHA_object,alpha_match] 2223 THEN REPEAT STRIP_TAC 2224 THEN ASM_REWRITE_TAC[] 2225 THEN FIRST_ASSUM MATCH_MP_TAC 2226 THEN ASM_REWRITE_TAC[] 2227 ); 2228 2229 2230val ALPHA_SUB = store_thm 2231 ("ALPHA_SUB", 2232 ���(!o1 o2 s. ALPHA_obj o1 o2 ==> 2233 ALPHA_obj (o1 <[ s) (o2 <[ s)) /\ 2234 (!d1 d2 s. ALPHA_dict d1 d2 ==> 2235 ALPHA_dict (d1 <[ s) (d2 <[ s)) /\ 2236 (!e1 e2 s. ALPHA_entry e1 e2 ==> 2237 ALPHA_entry (e1 <[ s) (e2 <[ s)) /\ 2238 (!m1 m2 s. ALPHA_method m1 m2 ==> 2239 ALPHA_method (m1 <[ s) (m2 <[ s))���, 2240 REPEAT STRIP_TAC 2241 THENL (map MATCH_MP_TAC (CONJUNCTS ALPHA_SUB_CONTEXT)) 2242 THEN ASM_REWRITE_TAC[ALPHA_subst,ALPHA_REFL] 2243 ); 2244 2245 2246val ALPHA_CHANGE_VAR = store_thm 2247 ("ALPHA_CHANGE_VAR", 2248 ���!y x s v a. 2249 ~(x IN FV_subst1 s (FV_obj1 a DIFF {v})) /\ 2250 ~(y IN FV_subst1 s (FV_obj1 a DIFF {v})) ==> 2251 ALPHA_method (SIGMA1 x (a <[ CONS (v, OVAR1 x) s)) 2252 (SIGMA1 y (a <[ CONS (v, OVAR1 y) s))���, 2253 REPEAT STRIP_TAC 2254 THEN REWRITE_TAC[ALPHA_object,ALPHA1_object_pos] 2255 THEN MATCH_MP_TAC ALPHA1_CHANGE_VAR 2256 THEN ASM_REWRITE_TAC[] 2257 ); 2258 2259 2260val ALPHA_CHANGE_ONE_VAR = store_thm 2261 ("ALPHA_CHANGE_ONE_VAR", 2262 ���!x v a. 2263 ~(x IN (FV_obj1 a DIFF {v})) ==> 2264 ALPHA_method (SIGMA1 x (a <[ [v, OVAR1 x])) 2265 (SIGMA1 v a)���, 2266 REPEAT STRIP_TAC 2267 THEN MP_TAC (SPECL [���v:var���,���x:var���,���[]:^subs1���, 2268 ���v:var���,���a:obj1���] 2269 ALPHA_CHANGE_VAR) 2270 THEN REWRITE_TAC[FV_subst_NIL1] 2271 THEN UNDISCH_ALL_TAC 2272 THEN REWRITE_TAC[IN_DIFF,IN] 2273 THEN DISCH_THEN REWRITE_THM 2274 THEN DEP_ONCE_REWRITE_TAC[SPECL[���a:obj1���,���[v,OVAR1 v]���] 2275 (CONJUNCT1 subst_IDENT1)] 2276 THEN GEN_TAC 2277 THEN REWRITE_TAC[SUB1] 2278 THEN COND_CASES_TAC 2279 THEN ASM_REWRITE_TAC[] 2280 ); 2281 2282 2283(* The following theorem is unused. 2284 2285val ALPHA_SWITCH = store_thm 2286 ("ALPHA_SWITCH", 2287 ���(!o1 o2 x y. 2288 ALPHA_obj (o1 <[ [x,OVAR1 y]) o2 /\ 2289 ALPHA_obj o1 (o2 <[ [y,OVAR1 x]) 2290 ==> 2291 ALPHA1_obj o1 o2 [x] [y]) /\ 2292 (!d1 d2 x y. 2293 ALPHA_dict (d1 <[ [x,OVAR1 y]) d2 /\ 2294 ALPHA_dict d1 (d2 <[ [y,OVAR1 x]) 2295 ==> 2296 ALPHA1_dict d1 d2 [x] [y]) /\ 2297 (!e1 e2 x y. 2298 ALPHA_entry (e1 <[ [x,OVAR1 y]) e2 /\ 2299 ALPHA_entry e1 (e2 <[ [y,OVAR1 x]) 2300 ==> 2301 ALPHA1_entry e1 e2 [x] [y]) /\ 2302 (!m1 m2 x y. 2303 ALPHA_method (m1 <[ [x,OVAR1 y]) m2 /\ 2304 ALPHA_method m1 (m2 <[ [y,OVAR1 x]) 2305 ==> 2306 ALPHA1_method m1 m2 [x] [y])���, 2307 REWRITE_TAC[ALPHA_object] 2308 THEN REPEAT STRIP_TAC 2309 THEN ONCE_REWRITE_TAC[GSYM (CONJUNCT1 APPEND)] 2310 THENL (map MATCH_MP_TAC (CONJUNCTS ALPHA1_SWITCH)) 2311 THEN EXISTS_TAC ���[]:var list��� 2312 THEN EXISTS_TAC ���[]:var list��� 2313 THEN ASM_REWRITE_TAC[APPEND,vsubst1] 2314 ); 2315 2316*) 2317 2318val ALPHA_method_one_one = store_thm 2319 ("ALPHA_method_one_one", 2320 ���!o1 o2 x y. 2321 ALPHA_method (SIGMA1 x o1) (SIGMA1 y o2) = 2322 (ALPHA_obj (o1 <[ [x, OVAR1 y]) o2 /\ 2323 ALPHA_obj o1 (o2 <[ [y, OVAR1 x]))���, 2324 REWRITE_TAC[ALPHA_object,ALPHA1_method_one_one] 2325 ); 2326 2327val ALPHA_SIGMA_subst = store_thm 2328 ("ALPHA_SIGMA_subst", 2329 ���!o1 o2 x y a. 2330 ALPHA_method (SIGMA1 x o1) (SIGMA1 y o2) ==> 2331 (ALPHA_obj (o1 <[ [x, a]) (o2 <[ [y, a]))���, 2332 REWRITE_TAC[ALPHA_object,ALPHA1_SIGMA_subst] 2333 ); 2334 2335 2336(* --------------------------------------------------------------------- *) 2337(* Primitive semantics of the sigma-calculus: *) 2338(* Abadi/Cardelli, Section 6.1.2, page 58-59 *) 2339(* Here we define the primitive reduction operator of the calculus. *) 2340(* It has two forms, one for method invocation and one for update. *) 2341(* --------------------------------------------------------------------- *) 2342 2343val obj1_0_RSP = store_thm 2344 ("obj1_0_RSP", 2345 ���ALPHA_obj obj1_0 obj1_0���, 2346 REWRITE_TAC[ALPHA_REFL] 2347 ); 2348 2349val method1_0_RSP = store_thm 2350 ("method1_0_RSP", 2351 ���ALPHA_method method1_0 method1_0���, 2352 REWRITE_TAC[ALPHA_REFL] 2353 ); 2354 2355 2356(* --------------------------------------------------------------------- *) 2357(* Definition of method invocation. *) 2358(* --------------------------------------------------------------------- *) 2359 2360val invoke_method1_RSP = store_thm 2361 ("invoke_method1_RSP", 2362 ���!m1 m2 o1 o2. 2363 ALPHA_method m1 m2 /\ ALPHA_obj o1 o2 ==> 2364 ALPHA_obj (invoke_method1 m1 o1) (invoke_method1 m2 o2)���, 2365 MUTUAL_INDUCT_THEN obj1_induction ASSUME_TAC 2366 THEN GEN_TAC 2367 THEN MUTUAL_INDUCT_THEN obj1_induction ASSUME_TAC 2368 THEN REPEAT GEN_TAC 2369 THEN REWRITE_TAC[invoke_method1_def] 2370 THEN REWRITE_TAC[ALPHA_object,ALPHA1_object_pos] 2371 THEN STRIP_TAC 2372 THEN IMP_RES_TAC ALPHA1_SUB 2373 THEN FIRST_ASSUM MATCH_MP_TAC 2374 THEN REWRITE_TAC[ALPHA1_subst] 2375 THEN REWRITE_TAC[alpha_match] 2376 THEN REWRITE_TAC[SUB1] 2377 THEN REPEAT STRIP_TAC 2378 THENL 2379 [ POP_ASSUM (REWRITE_ALL_THM o SYM) 2380 THEN POP_ASSUM (REWRITE_ALL_THM o SYM) 2381 THEN ASM_REWRITE_TAC[], 2382 2383 POP_ASSUM (REWRITE_ALL_THM o SYM) 2384 THEN ASM_REWRITE_TAC[] 2385 THEN REWRITE_TAC[ALPHA1_REFL] 2386 ] 2387 ); 2388 2389val invoke_dict1_RSP = store_thm 2390 ("invoke_dict1_RSP", 2391 ���!d1 d2 o1 o2 lb. 2392 ALPHA_dict d1 d2 /\ ALPHA_obj o1 o2 ==> 2393 ALPHA_obj (invoke_dict1 d1 o1 lb) (invoke_dict1 d2 o2 lb)���, 2394 MUTUAL_INDUCT_THEN obj1_induction ASSUME_TAC 2395 THEN MUTUAL_INDUCT_THEN obj1_induction ASSUME_TAC 2396 THEN REWRITE_TAC[ALPHA_object_neg] 2397 THEN REPEAT GEN_TAC 2398 THEN ONCE_REWRITE_TAC[GSYM PAIR] 2399 THEN PURE_REWRITE_TAC[invoke_dict1] 2400 THEN PURE_REWRITE_TAC[ALPHA_object_pos] 2401 THEN REWRITE_TAC[ALPHA_REFL] 2402 THEN POP_TAC 2403 THEN STRIP_TAC 2404 THEN RES_TAC 2405 THEN POP_ASSUM (ASSUME_TAC o SPEC_ALL) 2406 THEN IMP_RES_TAC invoke_method1_RSP 2407 THEN ASM_REWRITE_TAC[] 2408 THEN COND_CASES_TAC 2409 THEN ASM_REWRITE_TAC[] 2410 ); 2411 2412val invoke1_RSP = store_thm 2413 ("invoke1_RSP", 2414 ���!o1 o2 lb. ALPHA_obj o1 o2 ==> 2415 ALPHA_obj (invoke1 o1 lb) (invoke1 o2 lb)���, 2416 MUTUAL_INDUCT_THEN obj1_induction ASSUME_TAC 2417 THENL [GEN_TAC, ALL_TAC, GEN_TAC, GEN_TAC] 2418 THEN MUTUAL_INDUCT_THEN obj1_induction ASSUME_TAC 2419 THEN REWRITE_TAC[ALPHA_object_neg] 2420 THEN REPEAT GEN_TAC 2421 THEN REWRITE_TAC[invoke1_def] 2422 THEN REWRITE_TAC[ALPHA_REFL] 2423 (* only one subgoal *) 2424 THEN DISCH_TAC 2425 THEN FIRST_ASSUM (ASSUME_TAC o REWRITE_RULE[ALPHA_object_pos]) 2426 THEN IMP_RES_TAC invoke_dict1_RSP 2427 THEN ASM_REWRITE_TAC[] 2428 ); 2429 2430val update_dict1_RSP = store_thm 2431 ("update_dict1_RSP", 2432 ���!d1 d2 lb m1 m2. 2433 ALPHA_dict d1 d2 /\ ALPHA_method m1 m2 ==> 2434 ALPHA_dict (update_dict1 d1 lb m1) (update_dict1 d2 lb m2)���, 2435 MUTUAL_INDUCT_THEN obj1_induction ASSUME_TAC 2436 THEN MUTUAL_INDUCT_THEN obj1_induction ASSUME_TAC 2437 THEN REWRITE_TAC[ALPHA_object_neg] 2438 THEN REPEAT GEN_TAC 2439 THEN ONCE_REWRITE_TAC[GSYM PAIR] 2440 THEN PURE_REWRITE_TAC[update_dict1] 2441 THEN PURE_REWRITE_TAC[ALPHA_object_pos] 2442 THEN REWRITE_TAC[ALPHA_REFL] 2443 THEN POP_TAC 2444 THEN STRIP_TAC 2445 THEN RES_TAC 2446 THEN POP_TAC 2447 THEN POP_ASSUM (ASSUME_TAC o SPEC_ALL) 2448 THEN ASM_REWRITE_TAC[] 2449 THEN COND_CASES_TAC 2450 THEN REWRITE_TAC[] 2451 THEN ONCE_REWRITE_TAC[GSYM PAIR] 2452 THEN PURE_REWRITE_TAC[ALPHA_object_pos] 2453 THEN ASM_REWRITE_TAC[] 2454 ); 2455 2456val update1_RSP = store_thm 2457 ("update1_RSP", 2458 ���!o1 o2 lb m1 m2. 2459 ALPHA_obj o1 o2 /\ ALPHA_method m1 m2 ==> 2460 ALPHA_obj (update1 o1 lb m1) (update1 o2 lb m2)���, 2461 MUTUAL_INDUCT_THEN obj1_induction ASSUME_TAC 2462 THENL [GEN_TAC, ALL_TAC, GEN_TAC, GEN_TAC] 2463 THEN MUTUAL_INDUCT_THEN obj1_induction ASSUME_TAC 2464 THEN REWRITE_TAC[ALPHA_object_neg] 2465 THEN REPEAT GEN_TAC 2466 THEN REWRITE_TAC[update1_def] 2467 THEN REWRITE_TAC[ALPHA_REFL] 2468 (* only one subgoal *) 2469 THEN REWRITE_TAC[ALPHA_object_pos] 2470 THEN STRIP_TAC 2471 THEN IMP_RES_TAC update_dict1_RSP 2472 THEN ASM_REWRITE_TAC[] 2473 ); 2474 2475 2476 2477val _ = export_theory(); 2478 2479val _ = print_theory_to_file "alpha.lst"; 2480 2481val _ = html_theory "alpha"; 2482 2483val _ = print_theory_size(); 2484