1open HolKernel Parse boolLib; 2infix THEN THENL THENC ORELSE ORELSEC THEN_TCL ORELSE_TCL ## |->; 3infixr -->; 4 5 6(* --------------------------------------------------------------------- *) 7(* Embedding the reduction semantaics of objects as a foundational *) 8(* layer, according to Abadi and Cardelli, "A Theory of Objects." *) 9(* --------------------------------------------------------------------- *) 10 11 12val _ = new_theory "reduction"; 13 14 15open listTheory; 16open pred_setTheory; 17open numLib; 18open arithmeticTheory; 19open bossLib; 20open Mutual; 21open ind_rel; 22open dep_rewrite; 23open more_setTheory; 24open objectTheory; 25open alphaTheory; 26open liftTheory; 27open barendregt; 28 29open tactics; 30 31 32 33val vars = ty_antiq( ==`:var list`== ); 34val subs = ty_antiq( ==`:(var # obj) list`== ); 35val dict = ty_antiq( ==`:(string # method) list`== ); 36val entry = ty_antiq( ==`:string # method`== ); 37 38 39val [ALPHA_obj_REFL, ALPHA_dict_REFL, ALPHA_entry_REFL, 40 ALPHA_method_REFL] 41 = CONJUNCTS ALPHA_REFL; 42 43val [ALPHA_obj_SYM, ALPHA_dict_SYM, ALPHA_entry_SYM, 44 ALPHA_method_SYM] 45 = CONJUNCTS ALPHA_SYM; 46 47val [ALPHA_obj_TRANS, ALPHA_dict_TRANS, ALPHA_entry_TRANS, 48 ALPHA_method_TRANS] 49 = CONJUNCTS ALPHA_TRANS; 50 51 52 53val HEIGHT_SUB_VAR = store_thm 54 ("HEIGHT_SUB_VAR", 55 ���(!a x y. 56 HEIGHT_obj (a <[ [x,OVAR y]) = HEIGHT_obj a) /\ 57 (!d x y. 58 HEIGHT_dict (d <[ [x,OVAR y]) = HEIGHT_dict d) /\ 59 (!e x y. 60 HEIGHT_entry (e <[ [x,OVAR y]) = HEIGHT_entry e) /\ 61 (!m x y. 62 HEIGHT_method (m <[ [x,OVAR y]) = HEIGHT_method m)���, 63 MUTUAL_INDUCT_THEN object_height_induct ASSUME_TAC 64 THEN REPEAT GEN_TAC 65 THENL 66 [ REWRITE_TAC[SUB_object,SUB] 67 THEN COND_CASES_TAC 68 THEN REWRITE_TAC[HEIGHT], 69 70 REWRITE_TAC[SUB_object] 71 THEN ASM_REWRITE_TAC[HEIGHT], 72 73 REWRITE_TAC[SUB_object] 74 THEN ASM_REWRITE_TAC[HEIGHT], 75 76 REWRITE_TAC[SUB_object] 77 THEN ASM_REWRITE_TAC[HEIGHT], 78 79 REWRITE_TAC[SUB_object] 80 THEN ASM_REWRITE_TAC[HEIGHT], 81 82 REWRITE_TAC[SUB_object] 83 THEN ASM_REWRITE_TAC[HEIGHT], 84 85 REWRITE_TAC[SUB_object] 86 THEN ASM_REWRITE_TAC[HEIGHT], 87(* 88 SHIFT_SIGMAS_TAC 89 THEN MAKE_SIMPLE_SUBST_TAC 90*) 91 SIMPLE_SUBST_TAC 92 THEN ASM_REWRITE_TAC[HEIGHT] 93 ] 94 ); 95 96 97 98(* Barendregt's Substitution Lemma, 2.1.16, page 27: *) 99 100val BARENDREGT_SUBSTITUTION_LEMMA = store_thm 101 ("BARENDREGT_SUBSTITUTION_LEMMA", 102 ���(!(M:obj) N L x y. 103 ~(x = y) /\ ~(x IN FV_obj L) ==> 104 (((M <[ [x,N]) <[ [y,L]) = 105 ((M <[ [y,L]) <[ [x, (N <[ [y,L])]))) /\ 106 (!(M:^dict) N L x y. 107 ~(x = y) /\ ~(x IN FV_obj L) ==> 108 (((M <[ [x,N]) <[ [y,L]) = 109 ((M <[ [y,L]) <[ [x, (N <[ [y,L])]))) /\ 110 (!(M:^entry) N L x y. 111 ~(x = y) /\ ~(x IN FV_obj L) ==> 112 (((M <[ [x,N]) <[ [y,L]) = 113 ((M <[ [y,L]) <[ [x, (N <[ [y,L])]))) /\ 114 (!(M:method) N L x y. 115 ~(x = y) /\ ~(x IN FV_obj L) ==> 116 (((M <[ [x,N]) <[ [y,L]) = 117 ((M <[ [y,L]) <[ [x, (N <[ [y,L])])))���, 118 MUTUAL_INDUCT_THEN object_height_induct ASSUME_TAC 119 THENL 120 [ REPEAT STRIP_TAC 121 THEN REWRITE_TAC[SUB_object,SUB] 122 THEN COND_CASES_TAC 123 THENL 124 [ POP_ASSUM REWRITE_ALL_THM 125 THEN EVERY_ASSUM REWRITE_THM 126 THEN REWRITE_TAC[SUB_object,SUB], 127 128 REWRITE_TAC[SUB_object,SUB] 129 THEN COND_CASES_TAC 130 THENL 131 [ IMP_RES_THEN REWRITE_THM subst_EMPTY, 132 133 ASM_REWRITE_TAC[SUB_object,SUB] 134 ] 135 ], 136 137 REPEAT STRIP_TAC 138 THEN RES_TAC 139 THEN ASM_REWRITE_TAC[SUB_object], 140 141 REPEAT STRIP_TAC 142 THEN RES_TAC 143 THEN ASM_REWRITE_TAC[SUB_object], 144 145 REPEAT STRIP_TAC 146 THEN RES_TAC 147 THEN ASM_REWRITE_TAC[SUB_object], 148 149 REPEAT STRIP_TAC 150 THEN RES_TAC 151 THEN ASM_REWRITE_TAC[SUB_object], 152 153 REPEAT STRIP_TAC 154 THEN RES_TAC 155 THEN ASM_REWRITE_TAC[SUB_object], 156 157 REPEAT STRIP_TAC 158 THEN RES_TAC 159 THEN ASM_REWRITE_TAC[SUB_object], 160 161 REPEAT STRIP_TAC 162 THEN SIMPLE_SUBST_TAC 163 THEN DEP_ASM_REWRITE_TAC[] 164 ] 165 ); 166 167 168val COLLAPSE_SUBST = store_thm 169 ("COLLAPSE_SUBST", 170 ���(!M x y N. 171 ~(y IN FV_obj M) ==> 172 (((M <[ [x,OVAR y]) <[ [y,N]) = (M <[ [x,N]))) /\ 173 (!M x y N. 174 ~(y IN FV_dict M) ==> 175 (((M <[ [x,OVAR y]) <[ [y,N]) = (M <[ [x,N]))) /\ 176 (!M x y N. 177 ~(y IN FV_entry M) ==> 178 (((M <[ [x,OVAR y]) <[ [y,N]) = (M <[ [x,N]))) /\ 179 (!M x y N. 180 ~(y IN FV_method M) ==> 181 (((M <[ [x,OVAR y]) <[ [y,N]) = (M <[ [x,N])))���, 182 MUTUAL_INDUCT_THEN object_height_induct ASSUME_TAC 183 THENL 184 [ REWRITE_TAC[FV_object,IN] 185 THEN REPEAT STRIP_TAC 186 THEN REWRITE_TAC[SUB_object,SUB] 187 THEN COND_CASES_TAC 188 THENL 189 [ REWRITE_TAC[SUB_object,SUB], 190 191 REWRITE_TAC[SUB_object,SUB] 192 THEN EVERY_ASSUM (REWRITE_THM o GSYM) 193 ], 194 195 REWRITE_TAC[FV_object,IN,IN_UNION,DE_MORGAN_THM] 196 THEN REPEAT STRIP_TAC 197 THEN RES_TAC 198 THEN ASM_REWRITE_TAC[SUB_object], 199 200 REWRITE_TAC[FV_object,IN,IN_UNION,DE_MORGAN_THM] 201 THEN REPEAT STRIP_TAC 202 THEN RES_TAC 203 THEN ASM_REWRITE_TAC[SUB_object], 204 205 REWRITE_TAC[FV_object,IN,IN_UNION,DE_MORGAN_THM] 206 THEN REPEAT STRIP_TAC 207 THEN RES_TAC 208 THEN ASM_REWRITE_TAC[SUB_object], 209 210 REWRITE_TAC[FV_object,IN,IN_UNION,DE_MORGAN_THM] 211 THEN REPEAT STRIP_TAC 212 THEN RES_TAC 213 THEN ASM_REWRITE_TAC[SUB_object], 214 215 REWRITE_TAC[FV_object,IN,IN_UNION,DE_MORGAN_THM] 216 THEN REPEAT STRIP_TAC 217 THEN RES_TAC 218 THEN ASM_REWRITE_TAC[SUB_object], 219 220 REWRITE_TAC[FV_object,IN,IN_UNION,DE_MORGAN_THM] 221 THEN REPEAT STRIP_TAC 222 THEN RES_TAC 223 THEN ASM_REWRITE_TAC[SUB_object], 224 225 REWRITE_TAC[FV_object,IN,DE_MORGAN_THM] 226 THEN REPEAT STRIP_TAC 227 THEN SIMPLE_SUBST_TAC 228 THEN DEP_ASM_REWRITE_TAC[] 229 THEN UNDISCH_TAC ���~(y IN FV_obj M DIFF {x})��� 230 THEN FIRST_ASSUM (REWRITE_THM o REWRITE_RULE[FV_object] o 231 AP_TERM ���FV_method���) 232 THEN REWRITE_TAC[IN_DIFF,IN,DE_MORGAN_THM] 233 THEN EVERY_ASSUM (REWRITE_THM o GSYM) 234 ] 235 ); 236 237 238 239(* --------------------------------------------------------------------- *) 240(* General reduction relations and theorems: *) 241(* "Lambda Calculus," Barendregt, Chapter 3, page 50-63 *) 242(* --------------------------------------------------------------------- *) 243 244 245(* Define the reflexive closure of a relation. *) 246 247(* Wait! Now, this is done in relationTheory! 248 249But the following definition is not the same as that in relationTheory. *) 250 251val RC_DEF = 252 new_definition("RC_DEF", 253 ���RC (R:'a->'a->bool) a b = 254 !P. 255 (!x y. R x y ==> P x y) /\ 256 (!x. P x x) 257 ==> P a b���); 258 259 260val RC_REFLEXIVE = store_thm 261 ("RC_REFLEXIVE", 262 ���!R (x:'a). RC R x x���, 263 REWRITE_TAC[RC_DEF] 264 THEN REPEAT STRIP_TAC 265 THEN ASM_REWRITE_TAC[] 266 ); 267 268val RC_SUBSET = store_thm 269 ("RC_SUBSET", 270 ���!R (x:'a) y. R x y ==> RC R x y���, 271 REWRITE_TAC[RC_DEF] 272 THEN REPEAT STRIP_TAC 273 THEN FIRST_ASSUM MATCH_MP_TAC 274 THEN ASM_REWRITE_TAC[] 275 ); 276 277val RC_INDUCT = store_thm 278 ("RC_INDUCT", 279 ���!(R:'a->'a->bool) P. 280 (!x y. R x y ==> P x y) /\ 281 (!x. P x x) 282 ==> !u v. RC R u v ==> P u v���, 283 REWRITE_TAC[RC_DEF] 284 THEN REPEAT STRIP_TAC 285 THEN FIRST_ASSUM MATCH_MP_TAC 286 THEN ASM_REWRITE_TAC[] 287 ); 288 289 290val RC_INDUCT_TAC = 291 let val rc_thm = RC_INDUCT 292 fun tac (asl,w) = 293 let open Rsyntax 294 val {Bvar=u,Body} = dest_forall w 295 val {Bvar=v,Body} = dest_forall Body 296 val {ant,conseq} = dest_imp Body 297 val (RC,[R,u',v']) = boolSyntax.strip_comb ant 298 val {Name = "RC",...} = dest_const RC 299 val _ = assert (aconv u) u' 300 val _ = assert (aconv v) v' 301 val P = list_mk_abs([u,v], conseq) 302 val rc_thm' = BETA_RULE(ISPEC P (ISPEC R rc_thm)) 303 in MATCH_MP_TAC rc_thm' (asl,w) 304 end 305 handle _ => raise HOL_ERR{origin_structure = "<top-level>", 306 origin_function = "RC_INDUCT_TAC", 307 message = "Unanticipated term structure"} 308 in tac 309 end; 310 311 312val RC_CASES = store_thm 313 ("RC_CASES", 314 ���!R (x:'a) y. RC R x y ==> R x y \/ (x = y)���, 315 GEN_TAC 316 THEN RC_INDUCT_TAC 317 THEN REPEAT STRIP_TAC 318 THEN ASM_REWRITE_TAC[] 319 ); 320 321(* Must use what is provided now in relationTheory. 322*) 323 324 325(* --------------------------------------------------------------------- *) 326(* Define compatible relations on the object/method language. *) 327(* --------------------------------------------------------------------- *) 328 329val compatible = 330 new_definition ("compatible", 331 ���compatible Ro Rd Re Rm = 332 ((!o1 o2. Ro o1 o2 ==> (!l. Ro (INVOKE o1 l) (INVOKE o2 l)) /\ 333 (!l m. Ro (UPDATE o1 l m) (UPDATE o2 l m)) /\ 334 (!x. Rm (SIGMA x o1) (SIGMA x o2))) 335 /\ 336 (!d1 d2. Rd d1 d2 ==> Ro (OBJ d1) (OBJ d2) /\ 337 (!e. Rd (CONS e d1) (CONS e d2))) 338 /\ 339 (!e1 e2. Re e1 e2 ==> (!d. Rd (CONS e1 d) (CONS e2 d))) 340 /\ 341 (!m1 m2. Rm m1 m2 ==> (!o' l. Ro (UPDATE o' l m1) (UPDATE o' l m2)) 342 /\ 343 (!l. Re (l, m1) (l, m2))))���); 344 345val reflexve = 346 new_definition ("reflexve", 347 ���reflexve Ro Rd Re Rm = 348 ((!o1: obj. Ro o1 o1) /\ 349 (!d1:^dict. Rd d1 d1) /\ 350 (!e1:^entry. Re e1 e1) /\ 351 (!m1: method. Rm m1 m1))���); 352 353val _ = hide "symmetric"; 354 355val symmetric = 356 new_definition ("symmetric", 357 ���symmetric Ro Rd Re Rm = 358 ((!o1 o2: obj. Ro o1 o2 ==> Ro o2 o1) /\ 359 (!d1 d2:^dict. Rd d1 d2 ==> Rd d2 d1) /\ 360 (!e1 e2:^entry. Re e1 e2 ==> Re e2 e1) /\ 361 (!m1 m2: method. Rm m1 m2 ==> Rm m2 m1))���); 362 363val transitive = 364 new_definition ("transitve", 365 ���transitve Ro Rd Re Rm = 366 ((!o1 o2 o3: obj. Ro o1 o2 /\ Ro o2 o3 ==> Ro o1 o3) /\ 367 (!d1 d2 d3:^dict. Rd d1 d2 /\ Rd d2 d3 ==> Rd d1 d3) /\ 368 (!e1 e2 e3:^entry. Re e1 e2 /\ Re e2 e3 ==> Re e1 e3) /\ 369 (!m1 m2 m3: method. Rm m1 m2 /\ Rm m2 m3 ==> Rm m1 m3))���); 370 371val equality = 372 new_definition ("equality", 373 ���equality Ro Rd Re Rm = 374 (compatible Ro Rd Re Rm /\ 375 reflexve Ro Rd Re Rm /\ 376 symmetric Ro Rd Re Rm /\ 377 transitve Ro Rd Re Rm)���); 378 379val reduction = 380 new_definition ("reduction", 381 ���reduction Ro Rd Re Rm = 382 (compatible Ro Rd Re Rm /\ 383 reflexve Ro Rd Re Rm /\ 384 transitve Ro Rd Re Rm)���); 385 386 387 388 389(* --------------------------------------------------------------------- *) 390(* (RED1 R o1 o2) means that the object o1 reduces to the object o2 *) 391(* in exactly one step, as defined in Barendregt, Definition 3.1.5, *) 392(* page 51. This is the compatible closure of R. *) 393(* --------------------------------------------------------------------- *) 394 395 396val RED1_obj = 397���RED1_obj : (obj -> obj -> bool) -> obj -> obj -> bool���; 398val RED1_dict = 399���RED1_dict : (obj -> obj -> bool) -> ^dict -> ^dict -> bool���; 400val RED1_entry = 401���RED1_entry : (obj -> obj -> bool) -> ^entry -> ^entry -> bool���; 402val RED1_method = 403���RED1_method : (obj -> obj -> bool) -> method -> method -> bool���; 404 405val RED1_patterns = [���^RED1_obj R o1 o2���, 406 ���^RED1_dict R d1 d2���, 407 ���^RED1_entry R e1 e2���, 408 ���^RED1_method R m1 m2��� 409 ]; 410 411val RED1_rules_tm = 412��� 413 ((R o1 o2) 414 (* -------------------------------------------- *) ==> 415 (^RED1_obj R o1 o2)) /\ 416 417 418 ((^RED1_dict R d1 d2) 419 (* -------------------------------------------- *) ==> 420 (^RED1_obj R (OBJ d1) (OBJ d2))) /\ 421 422 423 ((^RED1_obj R o1 o2) 424 (* -------------------------------------------- *) ==> 425 (^RED1_obj R (INVOKE o1 l) (INVOKE o2 l))) /\ 426 427 428 ((^RED1_obj R o1 o2) 429 (* -------------------------------------------- *) ==> 430 (^RED1_obj R (UPDATE o1 l m) (UPDATE o2 l m))) /\ 431 432 433 ((^RED1_method R m1 m2) 434 (* -------------------------------------------- *) ==> 435 (^RED1_obj R (UPDATE a l m1) (UPDATE a l m2))) /\ 436 437 438 ((^RED1_entry R e1 e2) 439 (* -------------------------------------------- *) ==> 440 (^RED1_dict R (CONS e1 d) (CONS e2 d))) /\ 441 442 443 ((^RED1_dict R d1 d2) 444 (* -------------------------------------------- *) ==> 445 (^RED1_dict R (CONS e d1) (CONS e d2))) /\ 446 447 448 ((^RED1_method R m1 m2) 449 (* -------------------------------------------- *) ==> 450 (^RED1_entry R (l, m1) (l, m2))) /\ 451 452 453 ((^RED1_obj R o1 o2) 454 (* -------------------------------------------- *) ==> 455 (^RED1_method R (SIGMA x o1) (SIGMA x o2))) 456���; 457 458val (RED1_rules_sat,RED1_ind_thm) = 459 define_inductive_relations RED1_patterns RED1_rules_tm; 460 461val RED1_inv_thms = prove_inversion_theorems 462 RED1_rules_sat RED1_ind_thm; 463 464val RED1_strong_ind = prove_strong_induction 465 RED1_rules_sat RED1_ind_thm; 466 467val _ = save_thm ("RED1_rules_sat", RED1_rules_sat); 468val _ = save_thm ("RED1_ind_thm", RED1_ind_thm); 469val _ = save_thm ("RED1_inv_thms", LIST_CONJ RED1_inv_thms); 470val _ = save_thm ("RED1_strong_ind", RED1_strong_ind); 471 472 473val [RED1_R, RED1_OBJ, RED1_INVOKE, RED1_UPDATE1, RED1_UPDATE2, 474 RED1_CONS1, RED1_CONS2, RED1_PAIR, RED1_SIGMA] = CONJUNCTS RED1_rules_sat; 475 476 477 478 479val RED1_height_ind_thm_LEMMA = store_thm 480 ("RED1_height_ind_thm_LEMMA", 481 ���!n P_0 P_1 P_2 P_3. 482 (!R o1 o2. R o1 o2 ==> P_0 R o1 o2) /\ 483 (!R d1 d2. P_1 R d1 d2 ==> P_0 R (OBJ d1) (OBJ d2)) /\ 484 (!R o1 l o2. P_0 R o1 o2 ==> P_0 R (INVOKE o1 l) (INVOKE o2 l)) /\ 485 (!R o1 l m o2. 486 P_0 R o1 o2 ==> P_0 R (UPDATE o1 l m) (UPDATE o2 l m)) /\ 487 (!R a l m1 m2. 488 P_3 R m1 m2 ==> P_0 R (UPDATE a l m1) (UPDATE a l m2)) /\ 489 (!R e1 d e2. P_2 R e1 e2 ==> P_1 R (CONS e1 d) (CONS e2 d)) /\ 490 (!R e d1 d2. P_1 R d1 d2 ==> P_1 R (CONS e d1) (CONS e d2)) /\ 491 (!R l m1 m2. P_3 R m1 m2 ==> P_2 R (l,m1) (l,m2)) /\ 492 (!R x o1 o2. 493 (!o1' o2'. RED1_obj R o1' o2' /\ 494 (HEIGHT_obj o1 = HEIGHT_obj o1') /\ 495 (HEIGHT_obj o2 = HEIGHT_obj o2') ==> P_0 R o1' o2') 496 ==> P_3 R (SIGMA x o1) (SIGMA x o2)) ==> 497 (!R o1 o2. RED1_obj R o1 o2 ==> 498 ((HEIGHT_obj o1 <= n) /\ 499 (HEIGHT_obj o2 <= n) ==> 500 P_0 R o1 o2)) /\ 501 (!R d1 d2. RED1_dict R d1 d2 ==> 502 ((HEIGHT_dict d1 <= n) /\ 503 (HEIGHT_dict d2 <= n) ==> 504 P_1 R d1 d2)) /\ 505 (!R e1 e2. RED1_entry R e1 e2 ==> 506 ((HEIGHT_entry e1 <= n) /\ 507 (HEIGHT_entry e2 <= n) ==> 508 P_2 R e1 e2)) /\ 509 (!R m1 m2. RED1_method R m1 m2 ==> 510 ((HEIGHT_method m1 <= n) /\ 511 (HEIGHT_method m2 <= n) ==> 512 P_3 R m1 m2))���, 513 INDUCT_TAC 514 THEN REPEAT GEN_TAC 515 THEN STRIP_TAC 516 THENL 517 [ REWRITE_TAC[HEIGHT_LESS_EQ_ZERO] 518 THEN REPEAT STRIP_TAC 519 THEN ASM_REWRITE_TAC[] 520 THENL 521 [ FIRST_ASSUM MATCH_MP_TAC 522 THEN UNDISCH_TAC ���RED1_obj R o1 o2��� 523 THEN ONCE_REWRITE_TAC RED1_inv_thms 524 THEN ASM_REWRITE_TAC[object_distinct], 525 526 UNDISCH_TAC ���RED1_dict R d1 d2��� 527 THEN ONCE_REWRITE_TAC RED1_inv_thms 528 THEN ASM_REWRITE_TAC[object_distinct,NOT_NIL_CONS] 529 ], 530 531 UNDISCH_ALL_TAC 532 THEN DISCH_THEN ((fn th => REPEAT DISCH_TAC 533 THEN ASSUME_TAC th) o SPEC_ALL) 534 THEN POP_ASSUM MP_TAC 535 THEN ASM_REWRITE_TAC[] 536 THEN DISCH_THEN (fn th => UNDISCH_ALL_TAC THEN STRIP_ASSUME_TAC th) 537 THEN REPEAT DISCH_TAC 538 THEN rule_induct RED1_ind_thm 539 THEN REWRITE_TAC[HEIGHT] 540 THEN REWRITE_TAC[MAX_SUC,MAX_LESS_EQ,LESS_EQ_MONO,ZERO_LESS_EQ] 541 THEN REPEAT STRIP_TAC 542 THEN ASM_REWRITE_TAC[] 543 THENL (* 9 subgoals *) 544 [ FIRST_ASSUM MATCH_MP_TAC 545 THEN ASM_REWRITE_TAC[], 546 547 FIRST_ASSUM MATCH_MP_TAC 548 THEN FIRST_ASSUM MATCH_MP_TAC 549 THEN IMP_RES_TAC LESS_EQ_IMP_LESS_SUC 550 THEN IMP_RES_TAC LESS_IMP_LESS_OR_EQ 551 THEN ASM_REWRITE_TAC[], 552 553 FIRST_ASSUM MATCH_MP_TAC 554 THEN FIRST_ASSUM MATCH_MP_TAC 555 THEN IMP_RES_TAC LESS_EQ_IMP_LESS_SUC 556 THEN IMP_RES_TAC LESS_IMP_LESS_OR_EQ 557 THEN ASM_REWRITE_TAC[], 558 559 FIRST_ASSUM MATCH_MP_TAC 560 THEN FIRST_ASSUM MATCH_MP_TAC 561 THEN IMP_RES_TAC LESS_EQ_IMP_LESS_SUC 562 THEN IMP_RES_TAC LESS_IMP_LESS_OR_EQ 563 THEN ASM_REWRITE_TAC[], 564 565 FIRST_ASSUM MATCH_MP_TAC 566 THEN FIRST_ASSUM MATCH_MP_TAC 567 THEN IMP_RES_TAC LESS_EQ_IMP_LESS_SUC 568 THEN IMP_RES_TAC LESS_IMP_LESS_OR_EQ 569 THEN ASM_REWRITE_TAC[], 570 571 FIRST_ASSUM MATCH_MP_TAC 572 THEN FIRST_ASSUM MATCH_MP_TAC 573 THEN IMP_RES_TAC LESS_EQ_IMP_LESS_SUC 574 THEN IMP_RES_TAC LESS_IMP_LESS_OR_EQ 575 THEN ASM_REWRITE_TAC[], 576 577 FIRST_ASSUM MATCH_MP_TAC 578 THEN FIRST_ASSUM MATCH_MP_TAC 579 THEN IMP_RES_TAC LESS_EQ_IMP_LESS_SUC 580 THEN IMP_RES_TAC LESS_IMP_LESS_OR_EQ 581 THEN ASM_REWRITE_TAC[], 582 583 FIRST_ASSUM MATCH_MP_TAC 584 THEN FIRST_ASSUM MATCH_MP_TAC 585 THEN IMP_RES_TAC LESS_EQ_IMP_LESS_SUC 586 THEN IMP_RES_TAC LESS_IMP_LESS_OR_EQ 587 THEN ASM_REWRITE_TAC[], 588 589 FIRST_ASSUM MATCH_MP_TAC 590 THEN REPEAT STRIP_TAC 591 THEN ASSUM_LIST 592 (MATCH_MP_TAC o REWRITE_RULE[AND_IMP_INTRO] o hd o rev) 593 THEN POP_ASSUM (REWRITE_THM o SYM) 594 THEN POP_ASSUM (REWRITE_THM o SYM) 595 THEN ASM_REWRITE_TAC[] 596 ] 597 ] 598 ); 599 600val RED1_height_ind_thm = store_thm 601 ("RED1_height_ind_thm", 602 ���!P_0 P_1 P_2 P_3. 603 (!R o1 o2. R o1 o2 ==> P_0 R o1 o2) /\ 604 (!R d1 d2. P_1 R d1 d2 ==> P_0 R (OBJ d1) (OBJ d2)) /\ 605 (!R o1 l o2. P_0 R o1 o2 ==> P_0 R (INVOKE o1 l) (INVOKE o2 l)) /\ 606 (!R o1 l m o2. 607 P_0 R o1 o2 ==> P_0 R (UPDATE o1 l m) (UPDATE o2 l m)) /\ 608 (!R a l m1 m2. 609 P_3 R m1 m2 ==> P_0 R (UPDATE a l m1) (UPDATE a l m2)) /\ 610 (!R e1 d e2. P_2 R e1 e2 ==> P_1 R (CONS e1 d) (CONS e2 d)) /\ 611 (!R e d1 d2. P_1 R d1 d2 ==> P_1 R (CONS e d1) (CONS e d2)) /\ 612 (!R l m1 m2. P_3 R m1 m2 ==> P_2 R (l,m1) (l,m2)) /\ 613 (!R x o1 o2. 614 (!o1' o2'. RED1_obj R o1' o2' /\ 615 (HEIGHT_obj o1 = HEIGHT_obj o1') /\ 616 (HEIGHT_obj o2 = HEIGHT_obj o2') ==> P_0 R o1' o2') 617 ==> P_3 R (SIGMA x o1) (SIGMA x o2)) ==> 618 (!R o1 o2. RED1_obj R o1 o2 ==> P_0 R o1 o2) /\ 619 (!R d1 d2. RED1_dict R d1 d2 ==> P_1 R d1 d2) /\ 620 (!R e1 e2. RED1_entry R e1 e2 ==> P_2 R e1 e2) /\ 621 (!R m1 m2. RED1_method R m1 m2 ==> P_3 R m1 m2)���, 622 REPEAT STRIP_TAC 623 THENL 624 (map (fn tm => MP_TAC (SPEC_ALL (SPEC tm RED1_height_ind_thm_LEMMA))) 625 [���(HEIGHT_obj o1) MAX (HEIGHT_obj o2)���, 626 ���(HEIGHT_dict d1) MAX (HEIGHT_dict d2)���, 627 ���(HEIGHT_entry e1) MAX (HEIGHT_entry e2)���, 628 ���(HEIGHT_method m1) MAX (HEIGHT_method m2)���]) 629 THEN ASM_REWRITE_TAC[AND_IMP_INTRO] 630 THEN REPEAT STRIP_TAC 631 THEN FIRST_ASSUM MATCH_MP_TAC 632 THEN ASM_REWRITE_TAC[LESS_EQ_MAX] 633 ); 634 635 636val RED1_height_strong_ind_LEMMA = store_thm 637 ("RED1_height_strong_ind_LEMMA", 638 ���!n P_0 P_1 P_2 P_3. 639 (!R o1 o2. R o1 o2 ==> P_0 R o1 o2) /\ 640 (!R d1 d2. 641 P_1 R d1 d2 /\ RED1_dict R d1 d2 ==> P_0 R (OBJ d1) (OBJ d2)) /\ 642 (!R o1 l o2. 643 P_0 R o1 o2 /\ RED1_obj R o1 o2 ==> 644 P_0 R (INVOKE o1 l) (INVOKE o2 l)) /\ 645 (!R o1 l m o2. 646 P_0 R o1 o2 /\ RED1_obj R o1 o2 ==> 647 P_0 R (UPDATE o1 l m) (UPDATE o2 l m)) /\ 648 (!R a l m1 m2. 649 P_3 R m1 m2 /\ RED1_method R m1 m2 ==> 650 P_0 R (UPDATE a l m1) (UPDATE a l m2)) /\ 651 (!R e1 d e2. 652 P_2 R e1 e2 /\ RED1_entry R e1 e2 ==> 653 P_1 R (CONS e1 d) (CONS e2 d)) /\ 654 (!R e d1 d2. 655 P_1 R d1 d2 /\ RED1_dict R d1 d2 ==> 656 P_1 R (CONS e d1) (CONS e d2)) /\ 657 (!R l m1 m2. 658 P_3 R m1 m2 /\ RED1_method R m1 m2 ==> P_2 R (l,m1) (l,m2)) /\ 659 (!R x o1 o2. 660 (!o1' o2'. 661 RED1_obj R o1' o2' /\ 662 (HEIGHT_obj o1 = HEIGHT_obj o1') /\ 663 (HEIGHT_obj o2 = HEIGHT_obj o2') ==> 664 P_0 R o1' o2') /\ 665 RED1_obj R o1 o2 ==> 666 P_3 R (SIGMA x o1) (SIGMA x o2)) ==> 667 (!R o1 o2. RED1_obj R o1 o2 ==> 668 ((HEIGHT_obj o1 <= n) /\ 669 (HEIGHT_obj o2 <= n) ==> 670 P_0 R o1 o2)) /\ 671 (!R d1 d2. RED1_dict R d1 d2 ==> 672 ((HEIGHT_dict d1 <= n) /\ 673 (HEIGHT_dict d2 <= n) ==> 674 P_1 R d1 d2)) /\ 675 (!R e1 e2. RED1_entry R e1 e2 ==> 676 ((HEIGHT_entry e1 <= n) /\ 677 (HEIGHT_entry e2 <= n) ==> 678 P_2 R e1 e2)) /\ 679 (!R m1 m2. RED1_method R m1 m2 ==> 680 ((HEIGHT_method m1 <= n) /\ 681 (HEIGHT_method m2 <= n) ==> 682 P_3 R m1 m2))���, 683 INDUCT_TAC 684 THEN REPEAT GEN_TAC 685 THEN STRIP_TAC 686 THENL 687 [ REWRITE_TAC[HEIGHT_LESS_EQ_ZERO] 688 THEN REPEAT STRIP_TAC 689 THEN ASM_REWRITE_TAC[] 690 THENL 691 [ FIRST_ASSUM MATCH_MP_TAC 692 THEN UNDISCH_TAC ���RED1_obj R o1 o2��� 693 THEN ONCE_REWRITE_TAC RED1_inv_thms 694 THEN ASM_REWRITE_TAC[object_distinct], 695 696 UNDISCH_TAC ���RED1_dict R d1 d2��� 697 THEN ONCE_REWRITE_TAC RED1_inv_thms 698 THEN ASM_REWRITE_TAC[object_distinct,NOT_NIL_CONS] 699 ], 700 701 UNDISCH_ALL_TAC 702 THEN DISCH_THEN ((fn th => REPEAT DISCH_TAC 703 THEN ASSUME_TAC th) o SPEC_ALL) 704 THEN POP_ASSUM MP_TAC 705 THEN ASM_REWRITE_TAC[] 706 THEN DISCH_THEN (fn th => UNDISCH_ALL_TAC THEN STRIP_ASSUME_TAC th) 707 THEN REPEAT DISCH_TAC 708 THEN rule_induct RED1_strong_ind 709 THEN REWRITE_TAC[HEIGHT] 710 THEN REWRITE_TAC[MAX_SUC,MAX_LESS_EQ,LESS_EQ_MONO,ZERO_LESS_EQ] 711 THEN REPEAT STRIP_TAC 712 THEN ASM_REWRITE_TAC[] 713 THENL (* 9 subgoals *) 714 [ FIRST_ASSUM MATCH_MP_TAC 715 THEN ASM_REWRITE_TAC[], 716 717 FIRST_ASSUM MATCH_MP_TAC 718 THEN ASM_REWRITE_TAC[] 719 THEN FIRST_ASSUM MATCH_MP_TAC 720 THEN IMP_RES_TAC LESS_EQ_IMP_LESS_SUC 721 THEN IMP_RES_TAC LESS_IMP_LESS_OR_EQ 722 THEN ASM_REWRITE_TAC[], 723 724 FIRST_ASSUM MATCH_MP_TAC 725 THEN ASM_REWRITE_TAC[] 726 THEN FIRST_ASSUM MATCH_MP_TAC 727 THEN IMP_RES_TAC LESS_EQ_IMP_LESS_SUC 728 THEN IMP_RES_TAC LESS_IMP_LESS_OR_EQ 729 THEN ASM_REWRITE_TAC[], 730 731 FIRST_ASSUM MATCH_MP_TAC 732 THEN ASM_REWRITE_TAC[] 733 THEN FIRST_ASSUM MATCH_MP_TAC 734 THEN IMP_RES_TAC LESS_EQ_IMP_LESS_SUC 735 THEN IMP_RES_TAC LESS_IMP_LESS_OR_EQ 736 THEN ASM_REWRITE_TAC[], 737 738 FIRST_ASSUM MATCH_MP_TAC 739 THEN ASM_REWRITE_TAC[] 740 THEN FIRST_ASSUM MATCH_MP_TAC 741 THEN IMP_RES_TAC LESS_EQ_IMP_LESS_SUC 742 THEN IMP_RES_TAC LESS_IMP_LESS_OR_EQ 743 THEN ASM_REWRITE_TAC[], 744 745 FIRST_ASSUM MATCH_MP_TAC 746 THEN ASM_REWRITE_TAC[] 747 THEN FIRST_ASSUM MATCH_MP_TAC 748 THEN IMP_RES_TAC LESS_EQ_IMP_LESS_SUC 749 THEN IMP_RES_TAC LESS_IMP_LESS_OR_EQ 750 THEN ASM_REWRITE_TAC[], 751 752 FIRST_ASSUM MATCH_MP_TAC 753 THEN ASM_REWRITE_TAC[] 754 THEN FIRST_ASSUM MATCH_MP_TAC 755 THEN IMP_RES_TAC LESS_EQ_IMP_LESS_SUC 756 THEN IMP_RES_TAC LESS_IMP_LESS_OR_EQ 757 THEN ASM_REWRITE_TAC[], 758 759 FIRST_ASSUM MATCH_MP_TAC 760 THEN ASM_REWRITE_TAC[] 761 THEN FIRST_ASSUM MATCH_MP_TAC 762 THEN IMP_RES_TAC LESS_EQ_IMP_LESS_SUC 763 THEN IMP_RES_TAC LESS_IMP_LESS_OR_EQ 764 THEN ASM_REWRITE_TAC[], 765 766 FIRST_ASSUM MATCH_MP_TAC 767 THEN ASM_REWRITE_TAC[] 768 THEN REPEAT STRIP_TAC 769 THEN UNDISCH_THEN 770 ���!(R:obj->obj->bool) o1 o2. R o1 o2 ==> P_0 R o1 o2��� 771 (fn th => ALL_TAC) 772 THEN FIRST_ASSUM (MATCH_MP_TAC o REWRITE_RULE[AND_IMP_INTRO]) 773 THEN POP_ASSUM (REWRITE_THM o SYM) 774 THEN POP_ASSUM (REWRITE_THM o SYM) 775 THEN IMP_RES_TAC LESS_EQ_IMP_LESS_SUC 776 THEN IMP_RES_TAC LESS_IMP_LESS_OR_EQ 777 THEN ASM_REWRITE_TAC[] 778 ] 779 ] 780 ); 781 782 783val RED1_height_strong_ind = store_thm 784 ("RED1_height_strong_ind", 785 ���!P_0 P_1 P_2 P_3. 786 (!R o1 o2. R o1 o2 ==> P_0 R o1 o2) /\ 787 (!R d1 d2. 788 P_1 R d1 d2 /\ RED1_dict R d1 d2 ==> P_0 R (OBJ d1) (OBJ d2)) /\ 789 (!R o1 l o2. 790 P_0 R o1 o2 /\ RED1_obj R o1 o2 ==> 791 P_0 R (INVOKE o1 l) (INVOKE o2 l)) /\ 792 (!R o1 l m o2. 793 P_0 R o1 o2 /\ RED1_obj R o1 o2 ==> 794 P_0 R (UPDATE o1 l m) (UPDATE o2 l m)) /\ 795 (!R a l m1 m2. 796 P_3 R m1 m2 /\ RED1_method R m1 m2 ==> 797 P_0 R (UPDATE a l m1) (UPDATE a l m2)) /\ 798 (!R e1 d e2. 799 P_2 R e1 e2 /\ RED1_entry R e1 e2 ==> 800 P_1 R (CONS e1 d) (CONS e2 d)) /\ 801 (!R e d1 d2. 802 P_1 R d1 d2 /\ RED1_dict R d1 d2 ==> 803 P_1 R (CONS e d1) (CONS e d2)) /\ 804 (!R l m1 m2. 805 P_3 R m1 m2 /\ RED1_method R m1 m2 ==> P_2 R (l,m1) (l,m2)) /\ 806 (!R x o1 o2. 807 (!o1' o2'. 808 RED1_obj R o1' o2' /\ 809 (HEIGHT_obj o1 = HEIGHT_obj o1') /\ 810 (HEIGHT_obj o2 = HEIGHT_obj o2') ==> 811 P_0 R o1' o2') /\ 812 RED1_obj R o1 o2 ==> 813 P_3 R (SIGMA x o1) (SIGMA x o2)) ==> 814 (!R o1 o2. RED1_obj R o1 o2 ==> P_0 R o1 o2) /\ 815 (!R d1 d2. RED1_dict R d1 d2 ==> P_1 R d1 d2) /\ 816 (!R e1 e2. RED1_entry R e1 e2 ==> P_2 R e1 e2) /\ 817 (!R m1 m2. RED1_method R m1 m2 ==> P_3 R m1 m2)���, 818 REPEAT STRIP_TAC 819 THENL 820 (map (fn tm => MP_TAC (SPEC_ALL (SPEC tm RED1_height_strong_ind_LEMMA))) 821 [���(HEIGHT_obj o1) MAX (HEIGHT_obj o2)���, 822 ���(HEIGHT_dict d1) MAX (HEIGHT_dict d2)���, 823 ���(HEIGHT_entry e1) MAX (HEIGHT_entry e2)���, 824 ���(HEIGHT_method m1) MAX (HEIGHT_method m2)���]) 825 THEN ASM_REWRITE_TAC[AND_IMP_INTRO] 826 THEN REPEAT STRIP_TAC 827 THEN FIRST_ASSUM MATCH_MP_TAC 828 THEN ASM_REWRITE_TAC[LESS_EQ_MAX] 829 ); 830 831 832 833(* --------------------------------------------------------------------- *) 834(* We claim that RED1 is a binary relation on the object/method *) 835(* language which is *) 836(* 1) compatible (in the sense of Barendregt, Definition 3.1.1, pg 50 *) 837(* 2) the compatible closure of the R relation, in the sense of *) 838(* Barendregt, Definition 3.1.4, pg 51 *) 839(* --------------------------------------------------------------------- *) 840 841 842val RED1_compatible = store_thm 843 ("RED1_compatible", 844 ���!R. compatible 845 (RED1_obj R) (RED1_dict R) (RED1_entry R) (RED1_method R)���, 846 REWRITE_TAC[compatible] 847 THEN CONV_TAC (TOP_DEPTH_CONV FORALL_AND_CONV) 848 THEN rule_induct RED1_strong_ind 849 THEN REPEAT STRIP_TAC 850 THEN IMP_RES_TAC RED1_R 851 THEN FIRST (map (fn th => MATCH_MP_TAC th 852 THEN ASM_REWRITE_TAC[] 853 THEN NO_TAC) 854 (CONJUNCTS RED1_rules_sat)) 855 ); 856 857 858 859(* We now need to define the reflexive and transitive closure of this. *) 860 861(* --------------------------------------------------------------------- *) 862(* (RED R o1 o2) means that the object o1 reduces to the object o2 *) 863(* in zero or more steps, as defined in Barendregt, Definition 3.1.5, *) 864(* page 51. This is the reflexive and transitive closure of RED1 R. *) 865(* --------------------------------------------------------------------- *) 866 867val RED_obj = 868���RED_obj : (obj -> obj -> bool) -> obj -> obj -> bool���; 869val RED_dict = 870���RED_dict : (obj -> obj -> bool) -> ^dict -> ^dict -> bool���; 871val RED_entry = 872���RED_entry : (obj -> obj -> bool) -> ^entry -> ^entry -> bool���; 873val RED_method = 874���RED_method : (obj -> obj -> bool) -> method -> method -> bool���; 875 876val RED_patterns = [���^RED_obj R o1 o2���, 877 ���^RED_dict R d1 d2���, 878 ���^RED_entry R e1 e2���, 879 ���^RED_method R m1 m2��� 880 ]; 881 882val RED_rules_tm = 883��� 884 885 (RED1_obj R o1 o2 886 (* -------------------------------------------- *) ==> 887 ^RED_obj R o1 o2) /\ 888 889 890 (* -------------------------------------------- *) 891 (^RED_obj R o1 o1) /\ 892 893 894 (^RED_obj R o1 o2 /\ ^RED_obj R o2 o3 895 (* -------------------------------------------- *) ==> 896 ^RED_obj R o1 o3) /\ 897 898 899 (RED1_dict R d1 d2 900 (* -------------------------------------------- *) ==> 901 ^RED_dict R d1 d2) /\ 902 903 904 (* -------------------------------------------- *) 905 (^RED_dict R d1 d1) /\ 906 907 908 (^RED_dict R d1 d2 /\ ^RED_dict R d2 d3 909 (* -------------------------------------------- *) ==> 910 ^RED_dict R d1 d3) /\ 911 912 913 (RED1_entry R e1 e2 914 (* -------------------------------------------- *) ==> 915 ^RED_entry R e1 e2) /\ 916 917 918 (* -------------------------------------------- *) 919 (^RED_entry R e1 e1) /\ 920 921 922 (^RED_entry R e1 e2 /\ ^RED_entry R e2 e3 923 (* -------------------------------------------- *) ==> 924 ^RED_entry R e1 e3) /\ 925 926 927 (RED1_method R m1 m2 928 (* -------------------------------------------- *) ==> 929 ^RED_method R m1 m2) /\ 930 931 932 (* -------------------------------------------- *) 933 (^RED_method R m1 m1) /\ 934 935 936 (^RED_method R m1 m2 /\ ^RED_method R m2 m3 937 (* -------------------------------------------- *) ==> 938 ^RED_method R m1 m3) 939���; 940 941 942val (RED_rules_sat,RED_ind_thm) = 943 define_inductive_relations RED_patterns RED_rules_tm; 944 945val RED_inv_thms = prove_inversion_theorems 946 RED_rules_sat RED_ind_thm; 947 948val RED_strong_ind = prove_strong_induction 949 RED_rules_sat RED_ind_thm; 950 951val _ = save_thm ("RED_rules_sat", RED_rules_sat); 952val _ = save_thm ("RED_ind_thm", RED_ind_thm); 953val _ = save_thm ("RED_inv_thms", LIST_CONJ RED_inv_thms); 954val _ = save_thm ("RED_strong_ind", RED_strong_ind); 955 956 957 958(* --------------------------------------------------------------------- *) 959(* We claim that RED is a binary relation on the object/method *) 960(* language which is *) 961(* 1) compatible (in the sense of Barendregt, Definition 3.1.1, pg 50 *) 962(* 2) the reflexive, transitive closure of the REDC relation, in the *) 963(* sense of Barendregt, Definition 3.1.4 and 3.1.5, pg 51 *) 964(* 3) a reduction relation, from 1) and 2). *) 965(* --------------------------------------------------------------------- *) 966 967 968val [RED_obj_RED1, RED_obj_REFL, RED_obj_TRANS, 969 RED_dict_RED1, RED_dict_REFL, RED_dict_TRANS, 970 RED_entry_RED1, RED_entry_REFL, RED_entry_TRANS, 971 RED_method_RED1, RED_method_REFL, RED_method_TRANS] 972 = CONJUNCTS (CONV_RULE (DEPTH_CONV LEFT_IMP_EXISTS_CONV) RED_rules_sat); 973 974val RED_RED1 = save_thm 975 ("RED_RED1", 976 LIST_CONJ [RED_obj_RED1, RED_dict_RED1, 977 RED_entry_RED1, RED_method_RED1]); 978 979val RED_REFL = save_thm 980 ("RED_REFL", 981 LIST_CONJ [RED_obj_REFL, RED_dict_REFL, 982 RED_entry_REFL, RED_method_REFL]); 983 984 985val [RED_obj_inv, RED_dict_inv, RED_entry_inv, RED_method_inv] 986 = RED_inv_thms; 987 988 989val RED_reflexive = store_thm 990 ("RED_reflexive", 991 ���!R. reflexve 992 (RED_obj R) (RED_dict R) (RED_entry R) (RED_method R)���, 993 REWRITE_TAC[reflexve] 994 THEN REWRITE_TAC[RED_REFL] 995 ); 996 997val RED_transitive = store_thm 998 ("RED_transitive", 999 ���!R. transitve 1000 (RED_obj R) (RED_dict R) (RED_entry R) (RED_method R)���, 1001 REWRITE_TAC[transitive] 1002 THEN REWRITE_TAC[CONV_RULE (DEPTH_CONV LEFT_IMP_EXISTS_CONV) 1003 RED_rules_sat] 1004 ); 1005 1006val RED_TRANS = save_thm("RED_TRANS", 1007 CONV_RULE (TOP_DEPTH_CONV FORALL_AND_CONV) 1008 (REWRITE_RULE[transitive] RED_transitive)); 1009 1010val RED_compatible = store_thm 1011 ("RED_compatible", 1012 ���!R. compatible 1013 (RED_obj R) (RED_dict R) (RED_entry R) (RED_method R)���, 1014 REWRITE_TAC[compatible] 1015 THEN CONV_TAC (TOP_DEPTH_CONV FORALL_AND_CONV) 1016 THEN rule_induct RED_ind_thm (* weak, not strong induction *) 1017 THEN REPEAT STRIP_TAC (* 24 subgoals *) 1018 THEN REWRITE_TAC[RED_REFL] (* takes care of 8 *) 1019 THEN RULE_ASSUM_TAC SPEC_ALL 1020 THEN IMP_RES_TAC RED_TRANS (* solves another 8 *) 1021 THEN IMP_RES_TAC (REWRITE_RULE[compatible] RED1_compatible) 1022 THEN RULE_ASSUM_TAC SPEC_ALL 1023 THEN IMP_RES_TAC RED_RED1 (* finishes the last 8 *) 1024 ); 1025 1026val RED_COMPAT = save_thm("RED_COMPAT", 1027 CONV_RULE (TOP_DEPTH_CONV FORALL_AND_CONV) 1028 (REWRITE_RULE[compatible] RED_compatible)); 1029 1030val [RED_obj_COMPAT, RED_dict_COMPAT, RED_entry_COMPAT, RED_method_COMPAT] 1031 = CONJUNCTS RED_COMPAT; 1032 1033 1034 1035val RED_reduction = store_thm 1036 ("RED_reduction", 1037 ���!R. reduction 1038 (RED_obj R) (RED_dict R) (RED_entry R) (RED_method R)���, 1039 REWRITE_TAC[reduction] 1040 THEN REWRITE_TAC[RED_compatible,RED_reflexive,RED_transitive] 1041 ); 1042 1043 1044 1045(* Barendregt's Substitution Remark, 3.1.7, page 52: *) 1046 1047val BARENDREGT_SUBSTITUTION_REMARK = store_thm 1048 ("BARENDREGT_SUBSTITUTION_REMARK", 1049 ���(!M N N' x. 1050 RED_obj R N N' ==> 1051 RED_obj R (M <[ [x,N]) (M <[ [x,N'])) /\ 1052 (!M N N' x. 1053 RED_obj R N N' ==> 1054 RED_dict R (M <[ [x,N]) (M <[ [x,N'])) /\ 1055 (!M N N' x. 1056 RED_obj R N N' ==> 1057 RED_entry R (M <[ [x,N]) (M <[ [x,N'])) /\ 1058 (!M N N' x. 1059 RED_obj R N N' ==> 1060 RED_method R (M <[ [x,N]) (M <[ [x,N']))���, 1061 MUTUAL_INDUCT_THEN object_height_induct ASSUME_TAC 1062 THENL 1063 [ REPEAT STRIP_TAC 1064 THEN REWRITE_TAC[SUB_object,SUB] 1065 THEN COND_CASES_TAC 1066 THENL 1067 [ ASM_REWRITE_TAC[], 1068 1069 REWRITE_TAC[RED_REFL] 1070 ], 1071 1072 REPEAT STRIP_TAC 1073 THEN RES_TAC 1074 THEN REWRITE_TAC[SUB_object] 1075 THEN RULE_ASSUM_TAC SPEC_ALL 1076 THEN IMP_RES_TAC RED_COMPAT, 1077 1078 REPEAT STRIP_TAC 1079 THEN RES_TAC 1080 THEN REWRITE_TAC[SUB_object] 1081 THEN RULE_ASSUM_TAC SPEC_ALL 1082 THEN IMP_RES_TAC RED_COMPAT 1083 THEN ASM_REWRITE_TAC[], 1084 1085 REPEAT STRIP_TAC 1086 THEN RES_TAC 1087 THEN REWRITE_TAC[SUB_object] 1088 THEN MATCH_MP_TAC RED_obj_TRANS 1089 THEN EXISTS_TAC ���UPDATE (M <[ [x,N']) l (M' <[ [x,N])��� 1090 THEN RULE_ASSUM_TAC SPEC_ALL 1091 THEN IMP_RES_TAC RED_COMPAT 1092 THEN ASM_REWRITE_TAC[], 1093 1094 REPEAT STRIP_TAC 1095 THEN RES_TAC 1096 THEN REWRITE_TAC[SUB_object] 1097 THEN MATCH_MP_TAC RED_dict_TRANS 1098 THEN EXISTS_TAC ���CONS ((M:^entry) <[ [x,N']) (M' <[ [x,N])��� 1099 THEN RULE_ASSUM_TAC SPEC_ALL 1100 THEN IMP_RES_TAC RED_COMPAT 1101 THEN ASM_REWRITE_TAC[], 1102 1103 REPEAT STRIP_TAC 1104 THEN REWRITE_TAC[SUB_object,RED_dict_REFL], 1105 1106 REPEAT STRIP_TAC 1107 THEN RES_TAC 1108 THEN REWRITE_TAC[SUB_object] 1109 THEN RULE_ASSUM_TAC SPEC_ALL 1110 THEN IMP_RES_TAC RED_COMPAT 1111 THEN ASM_REWRITE_TAC[], 1112 1113 REPEAT STRIP_TAC 1114 THEN SIMPLE_SUBST_TAC 1115 THEN RES_TAC 1116 THEN POP_ASSUM (ASSUME_TAC o SPEC ���x':var���) 1117 THEN IMP_RES_TAC RED_COMPAT 1118 THEN ASM_REWRITE_TAC[] 1119 ] 1120 ); 1121 1122 1123 1124(* We now need to define the equivalence relation generated by R. *) 1125 1126(* --------------------------------------------------------------------- *) 1127(* (REQUAL R o1 o2) means that the object o1 is R-convertible to the *) 1128(* object o2, as defined in Barendregt, Definition 3.1.5, page 51. *) 1129(* This is the symmetric and transitive closure of RED R. *) 1130(* --------------------------------------------------------------------- *) 1131 1132val REQUAL_obj = 1133���REQUAL_obj : (obj -> obj -> bool) -> obj -> obj -> bool���; 1134val REQUAL_dict = 1135���REQUAL_dict : (obj -> obj -> bool) -> ^dict -> ^dict -> bool���; 1136val REQUAL_entry = 1137���REQUAL_entry : (obj -> obj -> bool) -> ^entry -> ^entry -> bool���; 1138val REQUAL_method = 1139���REQUAL_method : (obj -> obj -> bool) -> method -> method -> bool���; 1140 1141val REQUAL_patterns = [���^REQUAL_obj R o1 o2���, 1142 ���^REQUAL_dict R d1 d2���, 1143 ���^REQUAL_entry R e1 e2���, 1144 ���^REQUAL_method R m1 m2��� 1145 ]; 1146 1147val REQUAL_rules_tm = 1148��� 1149 (RED_obj R o1 o2 1150 (* -------------------------------------------- *) ==> 1151 ^REQUAL_obj R o1 o2) /\ 1152 1153 (REQUAL_obj R o1 o2 1154 (* -------------------------------------------- *) ==> 1155 ^REQUAL_obj R o2 o1) /\ 1156 1157 (^REQUAL_obj R o1 o2 /\ ^REQUAL_obj R o2 o3 1158 (* -------------------------------------------- *) ==> 1159 ^REQUAL_obj R o1 o3) /\ 1160 1161 1162 (RED_dict R d1 d2 1163 (* -------------------------------------------- *) ==> 1164 ^REQUAL_dict R d1 d2) /\ 1165 1166 (^REQUAL_dict R d1 d2 1167 (* -------------------------------------------- *) ==> 1168 ^REQUAL_dict R d2 d1) /\ 1169 1170 (^REQUAL_dict R d1 d2 /\ ^REQUAL_dict R d2 d3 1171 (* -------------------------------------------- *) ==> 1172 ^REQUAL_dict R d1 d3) /\ 1173 1174 1175 (RED_entry R e1 e2 1176 (* -------------------------------------------- *) ==> 1177 ^REQUAL_entry R e1 e2) /\ 1178 1179 (^REQUAL_entry R e1 e2 1180 (* -------------------------------------------- *) ==> 1181 ^REQUAL_entry R e2 e1) /\ 1182 1183 (^REQUAL_entry R e1 e2 /\ ^REQUAL_entry R e2 e3 1184 (* -------------------------------------------- *) ==> 1185 ^REQUAL_entry R e1 e3) /\ 1186 1187 1188 (RED_method R m1 m2 1189 (* -------------------------------------------- *) ==> 1190 ^REQUAL_method R m1 m2) /\ 1191 1192 (REQUAL_method R m1 m2 1193 (* -------------------------------------------- *) ==> 1194 ^REQUAL_method R m2 m1) /\ 1195 1196 1197 (^REQUAL_method R m1 m2 /\ ^REQUAL_method R m2 m3 1198 (* -------------------------------------------- *) ==> 1199 ^REQUAL_method R m1 m3) 1200���; 1201 1202 1203val (REQUAL_rules_sat,REQUAL_ind_thm) = 1204 define_inductive_relations REQUAL_patterns REQUAL_rules_tm; 1205 1206val REQUAL_inv_thms = prove_inversion_theorems 1207 REQUAL_rules_sat REQUAL_ind_thm; 1208 1209val REQUAL_strong_ind = prove_strong_induction 1210 REQUAL_rules_sat REQUAL_ind_thm; 1211 1212val _ = save_thm ("REQUAL_rules_sat", REQUAL_rules_sat); 1213val _ = save_thm ("REQUAL_ind_thm", REQUAL_ind_thm); 1214val _ = save_thm ("REQUAL_inv_thms", LIST_CONJ REQUAL_inv_thms); 1215val _ = save_thm ("REQUAL_strong_ind", REQUAL_strong_ind); 1216 1217 1218 1219(* --------------------------------------------------------------------- *) 1220(* We claim that REQUAL is a binary relation on the object/method *) 1221(* language which is *) 1222(* 1) compatible (in the sense of Barendregt, Definition 3.1.1, pg 50 *) 1223(* 2) the symmetric, transitive closure of the RED relation, in the *) 1224(* sense of Barendregt, Definition 3.1.4 and 3.1.5, pg 51. *) 1225(* 3) an equivalence relation, from 2) and that RED is reflexive. *) 1226(* 4) an equality relation, as a compatible equivalence relation. *) 1227(* --------------------------------------------------------------------- *) 1228 1229 1230val [REQUAL_obj_RED, REQUAL_obj_SYM, REQUAL_obj_TRANS, 1231 REQUAL_dict_RED, REQUAL_dict_SYM, REQUAL_dict_TRANS, 1232 REQUAL_entry_RED, REQUAL_entry_SYM, REQUAL_entry_TRANS, 1233 REQUAL_method_RED, REQUAL_method_SYM, REQUAL_method_TRANS] 1234 = CONJUNCTS (CONV_RULE (DEPTH_CONV LEFT_IMP_EXISTS_CONV) REQUAL_rules_sat); 1235 1236val REQUAL_RED = save_thm 1237 ("REQUAL_RED", 1238 LIST_CONJ [REQUAL_obj_RED, REQUAL_dict_RED, 1239 REQUAL_entry_RED, REQUAL_method_RED]); 1240 1241val REQUAL_SYM = save_thm 1242 ("REQUAL_SYM", 1243 LIST_CONJ [REQUAL_obj_SYM, REQUAL_dict_SYM, 1244 REQUAL_entry_SYM, REQUAL_method_SYM]); 1245 1246 1247val [REQUAL_obj_inv, REQUAL_dict_inv, REQUAL_entry_inv, REQUAL_method_inv] 1248 = REQUAL_inv_thms; 1249 1250 1251val REQUAL_reflexive = store_thm 1252 ("REQUAL_reflexive", 1253 ���!R. reflexve 1254 (REQUAL_obj R) 1255 (REQUAL_dict R) 1256 (REQUAL_entry R) 1257 (REQUAL_method R)���, 1258 REWRITE_TAC[reflexve] 1259 THEN REPEAT STRIP_TAC 1260 THENL (map MATCH_MP_TAC (CONJUNCTS REQUAL_RED)) 1261 THEN REWRITE_TAC[RED_REFL] 1262 ); 1263 1264val REQUAL_symmetric = store_thm 1265 ("REQUAL_symmetric", 1266 ���!R. symmetric 1267 (REQUAL_obj R) 1268 (REQUAL_dict R) 1269 (REQUAL_entry R) 1270 (REQUAL_method R)���, 1271 REWRITE_TAC[symmetric] 1272 THEN REWRITE_TAC[REQUAL_SYM] 1273 ); 1274 1275val REQUAL_transitive = store_thm 1276 ("REQUAL_transitive", 1277 ���!R. transitve 1278 (REQUAL_obj R) 1279 (REQUAL_dict R) 1280 (REQUAL_entry R) 1281 (REQUAL_method R)���, 1282 REWRITE_TAC[transitive] 1283 THEN REWRITE_TAC[CONV_RULE (DEPTH_CONV LEFT_IMP_EXISTS_CONV) 1284 REQUAL_rules_sat] 1285 ); 1286 1287val REQUAL_TRANS = save_thm("REQUAL_TRANS", 1288 CONV_RULE (TOP_DEPTH_CONV FORALL_AND_CONV) 1289 (REWRITE_RULE[transitive] REQUAL_transitive)); 1290 1291val REQUAL_compatible = store_thm 1292 ("REQUAL_compatible", 1293 ���!R. compatible 1294 (REQUAL_obj R) 1295 (REQUAL_dict R) 1296 (REQUAL_entry R) 1297 (REQUAL_method R)���, 1298 REWRITE_TAC[compatible] 1299 THEN CONV_TAC (TOP_DEPTH_CONV FORALL_AND_CONV) 1300 THEN rule_induct REQUAL_ind_thm (* weak, not strong induction *) 1301 THEN REPEAT STRIP_TAC (* 24 subgoals *) 1302 THEN RULE_ASSUM_TAC SPEC_ALL 1303 THEN IMP_RES_TAC REQUAL_SYM (* takes care of 8 *) 1304 THEN IMP_RES_TAC REQUAL_TRANS (* solves another 8 *) 1305 THEN IMP_RES_TAC RED_COMPAT 1306 THEN RULE_ASSUM_TAC SPEC_ALL 1307 THEN IMP_RES_TAC REQUAL_RED (* finishes the last 8 *) 1308 ); 1309 1310val REQUAL_COMPAT = save_thm("REQUAL_COMPAT", 1311 CONV_RULE (TOP_DEPTH_CONV FORALL_AND_CONV) 1312 (REWRITE_RULE[compatible] REQUAL_compatible)); 1313 1314val [REQUAL_obj_COMPAT, REQUAL_dict_COMPAT, 1315 REQUAL_entry_COMPAT, REQUAL_method_COMPAT] 1316 = CONJUNCTS REQUAL_COMPAT; 1317 1318 1319val REQUAL_reduction = store_thm 1320 ("REQUAL_reduction", 1321 ���!R. reduction 1322 (REQUAL_obj R) 1323 (REQUAL_dict R) 1324 (REQUAL_entry R) 1325 (REQUAL_method R)���, 1326 REWRITE_TAC[reduction] 1327 THEN REWRITE_TAC[REQUAL_compatible,REQUAL_reflexive,REQUAL_transitive] 1328 ); 1329 1330val REQUAL_equality = store_thm 1331 ("REQUAL_equality", 1332 ���!R. equality 1333 (REQUAL_obj R) 1334 (REQUAL_dict R) 1335 (REQUAL_entry R) 1336 (REQUAL_method R)���, 1337 REWRITE_TAC[equality] 1338 THEN REWRITE_TAC[REQUAL_compatible,REQUAL_reflexive, 1339 REQUAL_symmetric,REQUAL_transitive] 1340 ); 1341 1342 1343 1344 (* ============ *) 1345 (* NORMAL FORMS *) 1346 (* ============ *) 1347 1348 1349val NORMAL_FORM_obj = 1350 new_definition 1351 ("NORMAL_FORM_obj", 1352 ���NORMAL_FORM_obj R a = (!a'. ~(RED1_obj R a a'))���); 1353 1354val NORMAL_FORM_dict = 1355 new_definition 1356 ("NORMAL_FORM_dict", 1357 ���NORMAL_FORM_dict R a = (!a'. ~(RED1_dict R a a'))���); 1358 1359val NORMAL_FORM_entry = 1360 new_definition 1361 ("NORMAL_FORM_entry", 1362 ���NORMAL_FORM_entry R a = (!a'. ~(RED1_entry R a a'))���); 1363 1364val NORMAL_FORM_method = 1365 new_definition 1366 ("NORMAL_FORM_method", 1367 ���NORMAL_FORM_method R a = (!a'. ~(RED1_method R a a'))���); 1368 1369val NORMAL_FORM = save_thm 1370 ("NORMAL_FORM", 1371 LIST_CONJ [NORMAL_FORM_obj, NORMAL_FORM_dict, 1372 NORMAL_FORM_entry, NORMAL_FORM_method]); 1373 1374 1375val NORMAL_FORM_OF_obj = 1376 new_definition 1377 ("NORMAL_FORM_OF_obj", 1378 ���NORMAL_FORM_OF_obj R a b = 1379 (NORMAL_FORM_obj R a /\ REQUAL_obj R b a)���); 1380 1381val NORMAL_FORM_OF_dict = 1382 new_definition 1383 ("NORMAL_FORM_OF_dict", 1384 ���NORMAL_FORM_OF_dict R a b = 1385 (NORMAL_FORM_dict R a /\ REQUAL_dict R b a)���); 1386 1387val NORMAL_FORM_OF_entry = 1388 new_definition 1389 ("NORMAL_FORM_OF_entry", 1390 ���NORMAL_FORM_OF_entry R a b = 1391 (NORMAL_FORM_entry R a /\ REQUAL_entry R b a)���); 1392 1393val NORMAL_FORM_OF_method = 1394 new_definition 1395 ("NORMAL_FORM_OF_method", 1396 ���NORMAL_FORM_OF_method R a b = 1397 (NORMAL_FORM_method R a /\ REQUAL_method R b a)���); 1398 1399val NORMAL_FORM_OF = save_thm 1400 ("NORMAL_FORM_OF", 1401 LIST_CONJ [NORMAL_FORM_OF_obj, NORMAL_FORM_OF_dict, 1402 NORMAL_FORM_OF_entry, NORMAL_FORM_OF_method]); 1403 1404 1405val NORMAL_FORM_IDENT_LEMMA = store_thm 1406 ("NORMAL_FORM_IDENT_LEMMA", 1407 ���(!R M N. RED_obj R M N ==> (NORMAL_FORM_obj R M ==> (M = N))) /\ 1408 (!R M N. RED_dict R M N ==> (NORMAL_FORM_dict R M ==> (M = N))) /\ 1409 (!R M N. RED_entry R M N ==> (NORMAL_FORM_entry R M ==> (M = N))) /\ 1410 (!R M N. RED_method R M N ==> (NORMAL_FORM_method R M ==> (M = N))) 1411 ���, 1412 rule_induct RED_ind_thm (* weak, not strong induction *) 1413 THEN REWRITE_TAC[NORMAL_FORM] 1414 THEN REPEAT STRIP_TAC 1415 THEN RES_TAC 1416 THEN POP_ASSUM REWRITE_ALL_THM 1417 THEN RES_TAC 1418 ); 1419 1420val NORMAL_FORM_IDENT = store_thm 1421 ("NORMAL_FORM_IDENT", 1422 ���(!R M. NORMAL_FORM_obj R M ==> (!N. RED_obj R M N ==> (M = N))) /\ 1423 (!R M. NORMAL_FORM_dict R M ==> (!N. RED_dict R M N ==> (M = N))) /\ 1424 (!R M. NORMAL_FORM_entry R M ==> (!N. RED_entry R M N ==> (M = N))) /\ 1425 (!R M. NORMAL_FORM_method R M ==> (!N. RED_method R M N ==> (M = N))) 1426 ���, 1427 REPEAT STRIP_TAC 1428 THEN IMP_RES_TAC NORMAL_FORM_IDENT_LEMMA 1429 ); 1430 1431 1432 1433(* THE DIAMOND PROPERTY *) 1434 1435val DIAMOND = 1436 new_definition 1437 ("DIAMOND", 1438 ���DIAMOND R = (!a b c:'a. R a b /\ R a c ==> (?d. R b d /\ R c d))���); 1439 1440 1441 1442(* THE CHURCH-ROSSER PROPERTY *) 1443 1444val CHURCH_ROSSER = 1445 new_definition 1446 ("CHURCH_ROSSER", 1447 ���CHURCH_ROSSER R = 1448 (DIAMOND (RED_obj R) /\ 1449 DIAMOND (RED_dict R) /\ 1450 DIAMOND (RED_entry R) /\ 1451 DIAMOND (RED_method R))���); 1452 1453 1454 1455val NORMAL_FORM_EXISTS_LEMMA = store_thm 1456 ("NORMAL_FORM_EXISTS_LEMMA", 1457 ���(!R M N. REQUAL_obj R M N ==> 1458 (CHURCH_ROSSER R ==> 1459 (?Z. RED_obj R M Z /\ RED_obj R N Z))) /\ 1460 (!R M N. REQUAL_dict R M N ==> 1461 (CHURCH_ROSSER R ==> 1462 (?Z. RED_dict R M Z /\ RED_dict R N Z))) /\ 1463 (!R M N. REQUAL_entry R M N ==> 1464 (CHURCH_ROSSER R ==> 1465 (?Z. RED_entry R M Z /\ RED_entry R N Z))) /\ 1466 (!R M N. REQUAL_method R M N ==> 1467 (CHURCH_ROSSER R ==> 1468 (?Z. RED_method R M Z /\ RED_method R N Z)))���, 1469 rule_induct REQUAL_ind_thm (* weak, not strong induction *) 1470 THEN REWRITE_TAC[CHURCH_ROSSER,DIAMOND] 1471 THEN REPEAT STRIP_TAC (* 12 subgoals *) 1472 THENL 1473 [ EXISTS_TAC ���o2:obj��� 1474 THEN ASM_REWRITE_TAC[RED_REFL], 1475 1476 UNDISCH_ALL_TAC 1477 THEN DISCH_THEN (fn th => REPEAT DISCH_TAC THEN MP_TAC th) 1478 THEN ASM_REWRITE_TAC[] 1479 THEN STRIP_TAC 1480 THEN EXISTS_TAC ���Z:obj��� 1481 THEN ASM_REWRITE_TAC[], 1482 1483 UNDISCH_ALL_TAC 1484 THEN DISCH_THEN (fn th1 => 1485 DISCH_THEN (fn th2 => 1486 REPEAT DISCH_TAC THEN MP_TAC th2 THEN MP_TAC th1)) 1487 THEN ASM_REWRITE_TAC[] 1488 THEN REPEAT STRIP_TAC 1489 THEN FIRST_ASSUM (fn imp => STRIP_ASSUME_TAC 1490 (MATCH_MP imp (CONJ (ASSUME ���RED_obj R o2 Z���) 1491 (ASSUME ���RED_obj R o2 Z'���)))) 1492 THEN EXISTS_TAC ���d:obj��� 1493 THEN IMP_RES_TAC RED_TRANS 1494 THEN ASM_REWRITE_TAC[], 1495 1496 EXISTS_TAC ���d2:^dict��� 1497 THEN ASM_REWRITE_TAC[RED_REFL], 1498 1499 UNDISCH_ALL_TAC 1500 THEN DISCH_THEN (fn th => REPEAT DISCH_TAC THEN MP_TAC th) 1501 THEN ASM_REWRITE_TAC[] 1502 THEN STRIP_TAC 1503 THEN EXISTS_TAC ���Z:^dict��� 1504 THEN ASM_REWRITE_TAC[], 1505 1506 UNDISCH_ALL_TAC 1507 THEN DISCH_THEN (fn th1 => 1508 DISCH_THEN (fn th2 => 1509 REPEAT DISCH_TAC THEN MP_TAC th2 THEN MP_TAC th1)) 1510 THEN ASM_REWRITE_TAC[] 1511 THEN REPEAT STRIP_TAC 1512 THEN FIRST_ASSUM (fn imp => STRIP_ASSUME_TAC 1513 (MATCH_MP imp (CONJ (ASSUME ���RED_dict R d2 Z���) 1514 (ASSUME ���RED_dict R d2 Z'���)))) 1515 THEN EXISTS_TAC ���d:^dict��� 1516 THEN IMP_RES_TAC RED_TRANS 1517 THEN ASM_REWRITE_TAC[], 1518 1519 EXISTS_TAC ���e2:^entry��� 1520 THEN ASM_REWRITE_TAC[RED_REFL], 1521 1522 UNDISCH_ALL_TAC 1523 THEN DISCH_THEN (fn th => REPEAT DISCH_TAC THEN MP_TAC th) 1524 THEN ASM_REWRITE_TAC[] 1525 THEN STRIP_TAC 1526 THEN EXISTS_TAC ���Z:^entry��� 1527 THEN ASM_REWRITE_TAC[], 1528 1529 UNDISCH_ALL_TAC 1530 THEN DISCH_THEN (fn th1 => 1531 DISCH_THEN (fn th2 => 1532 REPEAT DISCH_TAC THEN MP_TAC th2 THEN MP_TAC th1)) 1533 THEN ASM_REWRITE_TAC[] 1534 THEN REPEAT STRIP_TAC 1535 THEN FIRST_ASSUM (fn imp => STRIP_ASSUME_TAC 1536 (MATCH_MP imp (CONJ (ASSUME ���RED_entry R e2 Z���) 1537 (ASSUME ���RED_entry R e2 Z'���)))) 1538 THEN EXISTS_TAC ���d:^entry��� 1539 THEN IMP_RES_TAC RED_TRANS 1540 THEN ASM_REWRITE_TAC[], 1541 1542 EXISTS_TAC ���m2:method��� 1543 THEN ASM_REWRITE_TAC[RED_REFL], 1544 1545 UNDISCH_ALL_TAC 1546 THEN DISCH_THEN (fn th => REPEAT DISCH_TAC THEN MP_TAC th) 1547 THEN ASM_REWRITE_TAC[] 1548 THEN STRIP_TAC 1549 THEN EXISTS_TAC ���Z:method��� 1550 THEN ASM_REWRITE_TAC[], 1551 1552 UNDISCH_ALL_TAC 1553 THEN DISCH_THEN (fn th1 => 1554 DISCH_THEN (fn th2 => 1555 REPEAT DISCH_TAC THEN MP_TAC th2 THEN MP_TAC th1)) 1556 THEN ASM_REWRITE_TAC[] 1557 THEN REPEAT STRIP_TAC 1558 THEN FIRST_ASSUM (fn imp => STRIP_ASSUME_TAC 1559 (MATCH_MP imp (CONJ (ASSUME ���RED_method R m2 Z���) 1560 (ASSUME ���RED_method R m2 Z'���)))) 1561 THEN EXISTS_TAC ���d:method��� 1562 THEN IMP_RES_TAC RED_TRANS 1563 THEN ASM_REWRITE_TAC[] 1564 ] 1565 ); 1566 1567val NORMAL_FORM_EXISTS = store_thm 1568 ("NORMAL_FORM_EXISTS", 1569 ���!R. CHURCH_ROSSER R ==> 1570 (!M N. REQUAL_obj R M N ==> 1571 (?Z. RED_obj R M Z /\ RED_obj R N Z)) /\ 1572 (!M N. REQUAL_dict R M N ==> 1573 (?Z. RED_dict R M Z /\ RED_dict R N Z)) /\ 1574 (!M N. REQUAL_entry R M N ==> 1575 (?Z. RED_entry R M Z /\ RED_entry R N Z)) /\ 1576 (!M N. REQUAL_method R M N ==> 1577 (?Z. RED_method R M Z /\ RED_method R N Z))���, 1578 REPEAT STRIP_TAC 1579 THEN IMP_RES_TAC NORMAL_FORM_EXISTS_LEMMA 1580 THENL 1581 [ EXISTS_TAC ���Z:obj���, 1582 EXISTS_TAC ���Z:^dict���, 1583 EXISTS_TAC ���Z:^entry���, 1584 EXISTS_TAC ���Z:method��� 1585 ] 1586 THEN ASM_REWRITE_TAC[] 1587 ); 1588 1589val NORMAL_FORM_REDUCED_TO = store_thm 1590 ("NORMAL_FORM_REDUCED_TO", 1591 ���!R. CHURCH_ROSSER R ==> 1592 (!M N. NORMAL_FORM_OF_obj R N M ==> RED_obj R M N) /\ 1593 (!M N. NORMAL_FORM_OF_dict R N M ==> RED_dict R M N) /\ 1594 (!M N. NORMAL_FORM_OF_entry R N M ==> RED_entry R M N) /\ 1595 (!M N. NORMAL_FORM_OF_method R N M ==> RED_method R M N)���, 1596 REWRITE_TAC[NORMAL_FORM_OF] 1597 THEN REPEAT STRIP_TAC 1598 THEN IMP_RES_TAC NORMAL_FORM_EXISTS 1599 THEN IMP_RES_TAC NORMAL_FORM_IDENT 1600 THEN ASM_REWRITE_TAC[] 1601 ); 1602 1603val NORMAL_FORM_UNIQUE = store_thm 1604 ("NORMAL_FORM_UNIQUE", 1605 ���!R. CHURCH_ROSSER R ==> 1606 (!M N1 N2. NORMAL_FORM_OF_obj R N1 M /\ 1607 NORMAL_FORM_OF_obj R N2 M ==> (N1 = N2)) /\ 1608 (!M N1 N2. NORMAL_FORM_OF_dict R N1 M /\ 1609 NORMAL_FORM_OF_dict R N2 M ==> (N1 = N2)) /\ 1610 (!M N1 N2. NORMAL_FORM_OF_entry R N1 M /\ 1611 NORMAL_FORM_OF_entry R N2 M ==> (N1 = N2)) /\ 1612 (!M N1 N2. NORMAL_FORM_OF_method R N1 M /\ 1613 NORMAL_FORM_OF_method R N2 M ==> (N1 = N2))���, 1614 REWRITE_TAC[NORMAL_FORM_OF] 1615 THEN REPEAT STRIP_TAC 1616 THEN IMP_RES_TAC REQUAL_SYM 1617 THEN UNDISCH_LAST_TAC 1618 (* THEN POP_TAC *) 1619 THEN DISCH_TAC 1620 THEN IMP_RES_TAC REQUAL_TRANS 1621 (* THEN POP_TAC THEN POP_TAC THEN POP_TAC *) 1622 THEN IMP_RES_TAC NORMAL_FORM_EXISTS 1623 (* THEN POP_TAC THEN POP_TAC THEN POP_TAC 1624 THEN POP_TAC THEN POP_TAC THEN POP_TAC 1625 THEN POP_TAC THEN POP_TAC THEN POP_TAC *) 1626 THEN IMP_RES_TAC NORMAL_FORM_IDENT 1627 THEN ASM_REWRITE_TAC[] 1628 ); 1629 1630 1631 1632(* SUBSTITUTIVE RELATIONS *) 1633 1634 1635val SUBSTITUTIVE_obj = 1636 new_definition 1637 ("SUBSTITUTIVE_obj", 1638 ���SUBSTITUTIVE_obj R = 1639 (!(M:obj) (N:obj) L x. 1640 R M N ==> R (M <[ [x,L]) (N <[ [x,L]))���); 1641 1642val SUBSTITUTIVE_dict = 1643 new_definition 1644 ("SUBSTITUTIVE_dict", 1645 ���SUBSTITUTIVE_dict R = 1646 (!(M:^dict) (N:^dict) L x. 1647 R M N ==> R (M <[ [x,L]) (N <[ [x,L]))���); 1648 1649val SUBSTITUTIVE_entry = 1650 new_definition 1651 ("SUBSTITUTIVE_entry", 1652 ���SUBSTITUTIVE_entry R = 1653 (!(M:^entry) (N:^entry) L x. 1654 R M N ==> R (M <[ [x,L]) (N <[ [x,L]))���); 1655 1656val SUBSTITUTIVE_method = 1657 new_definition 1658 ("SUBSTITUTIVE_method", 1659 ���SUBSTITUTIVE_method R = 1660 (!(M:method) (N:method) L x. 1661 R M N ==> R (M <[ [x,L]) (N <[ [x,L]))���); 1662 1663val SUBSTITUTIVE = save_thm 1664 ("SUBSTITUTIVE", 1665 LIST_CONJ [SUBSTITUTIVE_obj, SUBSTITUTIVE_dict, 1666 SUBSTITUTIVE_entry, SUBSTITUTIVE_method]); 1667 1668 1669val RED1_SUBSTITUTIVE_LEMMA = TAC_PROOF(([], 1670 ���(!R M N. 1671 RED1_obj R M N ==> 1672 ((!M N L x. R M N ==> R (M <[ [x,L]) (N <[ [x,L])) ==> 1673 (!L x. RED1_obj R (M <[ [x,L]) (N <[ [x,L])))) /\ 1674 (!R M N. 1675 RED1_dict R M N ==> 1676 ((!M N L x. R M N ==> R (M <[ [x,L]) (N <[ [x,L])) ==> 1677 (!L x. RED1_dict R (M <[ [x,L]) (N <[ [x,L])))) /\ 1678 (!R M N. 1679 RED1_entry R M N ==> 1680 ((!M N L x. R M N ==> R (M <[ [x,L]) (N <[ [x,L])) ==> 1681 (!L x. RED1_entry R (M <[ [x,L]) (N <[ [x,L])))) /\ 1682 (!R M N. 1683 RED1_method R M N ==> 1684 ((!M N L x. R M N ==> R (M <[ [x,L]) (N <[ [x,L])) ==> 1685 (!L x. RED1_method R (M <[ [x,L]) (N <[ [x,L]))))���), 1686 rule_induct RED1_height_strong_ind (* strong, not weak induction *) 1687 THEN REPEAT STRIP_TAC (* 12 subgoals *) 1688 THENL 1689 [ RES_TAC 1690 THEN MATCH_MP_TAC RED1_R 1691 THEN ASM_REWRITE_TAC[], 1692 1693 RES_TAC 1694 THEN REWRITE_TAC[SUB_object] 1695 THEN MATCH_MP_TAC RED1_OBJ 1696 THEN ASM_REWRITE_TAC[], 1697 1698 RES_TAC 1699 THEN REWRITE_TAC[SUB_object] 1700 THEN MATCH_MP_TAC RED1_INVOKE 1701 THEN ASM_REWRITE_TAC[], 1702 1703 RES_TAC 1704 THEN REWRITE_TAC[SUB_object] 1705 THEN MATCH_MP_TAC RED1_UPDATE1 1706 THEN ASM_REWRITE_TAC[], 1707 1708 RES_TAC 1709 THEN REWRITE_TAC[SUB_object] 1710 THEN MATCH_MP_TAC RED1_UPDATE2 1711 THEN ASM_REWRITE_TAC[], 1712 1713 RES_TAC 1714 THEN REWRITE_TAC[SUB_object] 1715 THEN MATCH_MP_TAC RED1_CONS1 1716 THEN ASM_REWRITE_TAC[], 1717 1718 RES_TAC 1719 THEN REWRITE_TAC[SUB_object] 1720 THEN MATCH_MP_TAC RED1_CONS2 1721 THEN ASM_REWRITE_TAC[], 1722 1723 RES_TAC 1724 THEN REWRITE_TAC[SUB_object] 1725 THEN MATCH_MP_TAC RED1_PAIR 1726 THEN ASM_REWRITE_TAC[], 1727 1728 SIMPLE_SUBST_TAC 1729 THEN MATCH_MP_TAC RED1_SIGMA 1730 THEN FIRST_ASSUM 1731 (MATCH_MP_TAC o 1732 REWRITE_RULE[AND_IMP_INTRO] o 1733 CONV_RULE (TOP_DEPTH_CONV RIGHT_IMP_FORALL_CONV)) 1734 THEN ASM_REWRITE_TAC[] 1735 THEN POP_ASSUM (REWRITE_THM o SYM o CONJUNCT1 o 1736 REWRITE_RULE[SIGMA_one_one]) 1737 THEN POP_ASSUM (REWRITE_THM o SYM o CONJUNCT1 o 1738 REWRITE_RULE[SIGMA_one_one]) 1739 THEN FIRST_ASSUM 1740 (MATCH_MP_TAC o 1741 REWRITE_RULE[AND_IMP_INTRO] o 1742 CONV_RULE (TOP_DEPTH_CONV RIGHT_IMP_FORALL_CONV)) 1743 THEN ASM_REWRITE_TAC[] 1744 ] 1745 ); 1746 1747 1748val RED1_SUBSTITUTIVE = store_thm 1749 ("RED1_SUBSTITUTIVE", 1750 ���!R. SUBSTITUTIVE_obj R ==> 1751 SUBSTITUTIVE_obj (RED1_obj R) /\ 1752 SUBSTITUTIVE_dict (RED1_dict R) /\ 1753 SUBSTITUTIVE_entry (RED1_entry R) /\ 1754 SUBSTITUTIVE_method (RED1_method R)���, 1755 REWRITE_TAC[SUBSTITUTIVE] 1756 THEN REPEAT STRIP_TAC (* 12 subgoals *) 1757 THEN IMP_RES_TAC RED1_SUBSTITUTIVE_LEMMA 1758 THEN ASM_REWRITE_TAC[] 1759 ); 1760 1761 1762val RED1_SUBSTITUTIVE_ind_thm_LEMMA = store_thm 1763 ("RED1_SUBSTITUTIVE_ind_thm_LEMMA", 1764 ���!n P_0 P_1 P_2 P_3. 1765 (!R o1 o2. SUBSTITUTIVE_obj R /\ 1766 R o1 o2 ==> P_0 R o1 o2) /\ 1767 (!R d1 d2. SUBSTITUTIVE_obj R /\ 1768 P_1 R d1 d2 ==> P_0 R (OBJ d1) (OBJ d2)) /\ 1769 (!R o1 l o2. SUBSTITUTIVE_obj R /\ 1770 P_0 R o1 o2 ==> P_0 R (INVOKE o1 l) (INVOKE o2 l)) /\ 1771 (!R o1 l m o2. 1772 SUBSTITUTIVE_obj R /\ 1773 P_0 R o1 o2 ==> P_0 R (UPDATE o1 l m) (UPDATE o2 l m)) /\ 1774 (!R a l m1 m2. 1775 SUBSTITUTIVE_obj R /\ 1776 P_3 R m1 m2 ==> P_0 R (UPDATE a l m1) (UPDATE a l m2)) /\ 1777 (!R e1 d e2. SUBSTITUTIVE_obj R /\ 1778 P_2 R e1 e2 ==> P_1 R (CONS e1 d) (CONS e2 d)) /\ 1779 (!R e d1 d2. SUBSTITUTIVE_obj R /\ 1780 P_1 R d1 d2 ==> P_1 R (CONS e d1) (CONS e d2)) /\ 1781 (!R l m1 m2. SUBSTITUTIVE_obj R /\ 1782 P_3 R m1 m2 ==> P_2 R (l,m1) (l,m2)) /\ 1783 (!R x o1 o2. SUBSTITUTIVE_obj R /\ 1784 (!z. P_0 R (o1 <[ [x,OVAR z]) (o2 <[ [x,OVAR z])) 1785 ==> P_3 R (SIGMA x o1) (SIGMA x o2)) ==> 1786 (!R o1 o2. RED1_obj R o1 o2 ==> 1787 (SUBSTITUTIVE_obj R /\ 1788 (HEIGHT_obj o1 <= n) /\ 1789 (HEIGHT_obj o2 <= n) ==> 1790 P_0 R o1 o2)) /\ 1791 (!R d1 d2. RED1_dict R d1 d2 ==> 1792 (SUBSTITUTIVE_obj R /\ 1793 (HEIGHT_dict d1 <= n) /\ 1794 (HEIGHT_dict d2 <= n) ==> 1795 P_1 R d1 d2)) /\ 1796 (!R e1 e2. RED1_entry R e1 e2 ==> 1797 (SUBSTITUTIVE_obj R /\ 1798 (HEIGHT_entry e1 <= n) /\ 1799 (HEIGHT_entry e2 <= n) ==> 1800 P_2 R e1 e2)) /\ 1801 (!R m1 m2. RED1_method R m1 m2 ==> 1802 (SUBSTITUTIVE_obj R /\ 1803 (HEIGHT_method m1 <= n) /\ 1804 (HEIGHT_method m2 <= n) ==> 1805 P_3 R m1 m2))���, 1806 INDUCT_TAC 1807 THEN REPEAT GEN_TAC 1808 THEN STRIP_TAC 1809 THENL 1810 [ REWRITE_TAC[HEIGHT_LESS_EQ_ZERO] 1811 THEN REPEAT STRIP_TAC 1812 THEN ASM_REWRITE_TAC[] 1813 THENL 1814 [ FIRST_ASSUM MATCH_MP_TAC 1815 THEN UNDISCH_TAC ���RED1_obj R o1 o2��� 1816 THEN ONCE_REWRITE_TAC RED1_inv_thms 1817 THEN ASM_REWRITE_TAC[object_distinct,NOT_NIL_CONS], 1818 1819 UNDISCH_TAC ���RED1_dict R d1 d2��� 1820 THEN ONCE_REWRITE_TAC RED1_inv_thms 1821 THEN ASM_REWRITE_TAC[object_distinct,NOT_NIL_CONS] 1822 ], 1823 1824 UNDISCH_ALL_TAC 1825 THEN DISCH_THEN ((fn th => REPEAT DISCH_TAC 1826 THEN ASSUME_TAC th) o SPEC_ALL) 1827 THEN POP_ASSUM MP_TAC 1828 THEN ASM_REWRITE_TAC[] 1829 THEN DISCH_THEN (fn th => UNDISCH_ALL_TAC THEN STRIP_ASSUME_TAC th) 1830 THEN REPEAT DISCH_TAC 1831 THEN rule_induct RED1_strong_ind 1832 THEN REWRITE_TAC[HEIGHT] 1833 THEN REWRITE_TAC[MAX_SUC,MAX_LESS_EQ,LESS_EQ_MONO,ZERO_LESS_EQ] 1834 THEN REPEAT STRIP_TAC 1835 THEN ASM_REWRITE_TAC[] 1836 THENL (* 9 subgoals *) 1837 [ FIRST_ASSUM MATCH_MP_TAC 1838 THEN ASM_REWRITE_TAC[], 1839 1840 FIRST_ASSUM MATCH_MP_TAC 1841 THEN ASM_REWRITE_TAC[] 1842 THEN FIRST_ASSUM MATCH_MP_TAC 1843 THEN IMP_RES_TAC LESS_EQ_IMP_LESS_SUC 1844 THEN IMP_RES_TAC LESS_IMP_LESS_OR_EQ 1845 THEN ASM_REWRITE_TAC[], 1846 1847 FIRST_ASSUM MATCH_MP_TAC 1848 THEN ASM_REWRITE_TAC[] 1849 THEN FIRST_ASSUM MATCH_MP_TAC 1850 THEN IMP_RES_TAC LESS_EQ_IMP_LESS_SUC 1851 THEN IMP_RES_TAC LESS_IMP_LESS_OR_EQ 1852 THEN ASM_REWRITE_TAC[], 1853 1854 FIRST_ASSUM MATCH_MP_TAC 1855 THEN ASM_REWRITE_TAC[] 1856 THEN FIRST_ASSUM MATCH_MP_TAC 1857 THEN IMP_RES_TAC LESS_EQ_IMP_LESS_SUC 1858 THEN IMP_RES_TAC LESS_IMP_LESS_OR_EQ 1859 THEN ASM_REWRITE_TAC[], 1860 1861 FIRST_ASSUM MATCH_MP_TAC 1862 THEN ASM_REWRITE_TAC[] 1863 THEN FIRST_ASSUM MATCH_MP_TAC 1864 THEN IMP_RES_TAC LESS_EQ_IMP_LESS_SUC 1865 THEN IMP_RES_TAC LESS_IMP_LESS_OR_EQ 1866 THEN ASM_REWRITE_TAC[], 1867 1868 FIRST_ASSUM MATCH_MP_TAC 1869 THEN ASM_REWRITE_TAC[] 1870 THEN FIRST_ASSUM MATCH_MP_TAC 1871 THEN IMP_RES_TAC LESS_EQ_IMP_LESS_SUC 1872 THEN IMP_RES_TAC LESS_IMP_LESS_OR_EQ 1873 THEN ASM_REWRITE_TAC[], 1874 1875 FIRST_ASSUM MATCH_MP_TAC 1876 THEN ASM_REWRITE_TAC[] 1877 THEN FIRST_ASSUM MATCH_MP_TAC 1878 THEN IMP_RES_TAC LESS_EQ_IMP_LESS_SUC 1879 THEN IMP_RES_TAC LESS_IMP_LESS_OR_EQ 1880 THEN ASM_REWRITE_TAC[], 1881 1882 FIRST_ASSUM MATCH_MP_TAC 1883 THEN ASM_REWRITE_TAC[] 1884 THEN FIRST_ASSUM MATCH_MP_TAC 1885 THEN IMP_RES_TAC LESS_EQ_IMP_LESS_SUC 1886 THEN IMP_RES_TAC LESS_IMP_LESS_OR_EQ 1887 THEN ASM_REWRITE_TAC[], 1888 1889 FIRST_ASSUM MATCH_MP_TAC 1890 THEN ASM_REWRITE_TAC[] 1891 THEN REWRITE_TAC[SUBSTITUTIVE] 1892 THEN REPEAT STRIP_TAC 1893 THEN ASSUM_LIST 1894 (MATCH_MP_TAC o REWRITE_RULE[AND_IMP_INTRO] o hd o rev) 1895 THEN ASM_REWRITE_TAC[HEIGHT_SUB_VAR] 1896 THEN IMP_RES_TAC RED1_SUBSTITUTIVE 1897 THEN REWRITE_ALL_TAC[SUBSTITUTIVE] 1898 THEN FIRST_ASSUM MATCH_MP_TAC 1899 THEN ASM_REWRITE_TAC[] 1900 ] 1901 ] 1902 ); 1903 1904 1905val RED1_SUBSTITUTIVE_ind_thm_LEMMA1 = store_thm 1906 ("RED1_SUBSTITUTIVE_ind_thm_LEMMA1", 1907 ���!P_0 P_1 P_2 P_3. 1908 (!R o1 o2. SUBSTITUTIVE_obj R /\ 1909 R o1 o2 ==> P_0 R o1 o2) /\ 1910 (!R d1 d2. SUBSTITUTIVE_obj R /\ 1911 P_1 R d1 d2 ==> P_0 R (OBJ d1) (OBJ d2)) /\ 1912 (!R o1 l o2. SUBSTITUTIVE_obj R /\ 1913 P_0 R o1 o2 ==> P_0 R (INVOKE o1 l) (INVOKE o2 l)) /\ 1914 (!R o1 l m o2. SUBSTITUTIVE_obj R /\ 1915 P_0 R o1 o2 ==> P_0 R (UPDATE o1 l m) (UPDATE o2 l m)) /\ 1916 (!R a l m1 m2. SUBSTITUTIVE_obj R /\ 1917 P_3 R m1 m2 ==> P_0 R (UPDATE a l m1) (UPDATE a l m2)) /\ 1918 (!R e1 d e2. SUBSTITUTIVE_obj R /\ 1919 P_2 R e1 e2 ==> P_1 R (CONS e1 d) (CONS e2 d)) /\ 1920 (!R e d1 d2. SUBSTITUTIVE_obj R /\ 1921 P_1 R d1 d2 ==> P_1 R (CONS e d1) (CONS e d2)) /\ 1922 (!R l m1 m2. SUBSTITUTIVE_obj R /\ 1923 P_3 R m1 m2 ==> P_2 R (l,m1) (l,m2)) /\ 1924 (!R x o1 o2. SUBSTITUTIVE_obj R /\ 1925 (!z. P_0 R (o1 <[ [x,OVAR z]) (o2 <[ [x,OVAR z])) 1926 ==> P_3 R (SIGMA x o1) (SIGMA x o2)) ==> 1927 (!R o1 o2. RED1_obj R o1 o2 ==> 1928 (SUBSTITUTIVE_obj R ==> 1929 P_0 R o1 o2)) /\ 1930 (!R d1 d2. RED1_dict R d1 d2 ==> 1931 (SUBSTITUTIVE_obj R ==> 1932 P_1 R d1 d2)) /\ 1933 (!R e1 e2. RED1_entry R e1 e2 ==> 1934 (SUBSTITUTIVE_obj R ==> 1935 P_2 R e1 e2)) /\ 1936 (!R m1 m2. RED1_method R m1 m2 ==> 1937 (SUBSTITUTIVE_obj R ==> 1938 P_3 R m1 m2))���, 1939 REPEAT STRIP_TAC 1940 THENL 1941 (map (fn tm => MP_TAC (SPEC_ALL 1942 (SPEC tm RED1_SUBSTITUTIVE_ind_thm_LEMMA))) 1943 [���(HEIGHT_obj o1) MAX (HEIGHT_obj o2)���, 1944 ���(HEIGHT_dict d1) MAX (HEIGHT_dict d2)���, 1945 ���(HEIGHT_entry e1) MAX (HEIGHT_entry e2)���, 1946 ���(HEIGHT_method m1) MAX (HEIGHT_method m2)���]) 1947 THEN ASM_REWRITE_TAC[AND_IMP_INTRO] 1948 THEN REPEAT STRIP_TAC 1949 THEN FIRST_ASSUM MATCH_MP_TAC 1950 THEN ASM_REWRITE_TAC[LESS_EQ_MAX] 1951 ); 1952 1953 1954val RED1_SUBSTITUTIVE_ind_thm = store_thm 1955 ("RED1_SUBSTITUTIVE_ind_thm", 1956 ���!R. SUBSTITUTIVE_obj R ==> 1957 !P_0 P_1 P_2 P_3. 1958 (!R o1 o2. R o1 o2 ==> P_0 R o1 o2) /\ 1959 (!R d1 d2. P_1 R d1 d2 ==> P_0 R (OBJ d1) (OBJ d2)) /\ 1960 (!R o1 l o2. P_0 R o1 o2 ==> P_0 R (INVOKE o1 l) (INVOKE o2 l)) /\ 1961 (!R o1 l m o2. 1962 P_0 R o1 o2 ==> P_0 R (UPDATE o1 l m) (UPDATE o2 l m)) /\ 1963 (!R a l m1 m2. 1964 P_3 R m1 m2 ==> P_0 R (UPDATE a l m1) (UPDATE a l m2)) /\ 1965 (!R e1 d e2. P_2 R e1 e2 ==> P_1 R (CONS e1 d) (CONS e2 d)) /\ 1966 (!R e d1 d2. P_1 R d1 d2 ==> P_1 R (CONS e d1) (CONS e d2)) /\ 1967 (!R l m1 m2. P_3 R m1 m2 ==> P_2 R (l,m1) (l,m2)) /\ 1968 (!R x o1 o2. SUBSTITUTIVE_obj R /\ 1969 (!z. P_0 R (o1 <[ [x,OVAR z]) (o2 <[ [x,OVAR z])) 1970 ==> P_3 R (SIGMA x o1) (SIGMA x o2)) ==> 1971 (!o1 o2. RED1_obj R o1 o2 ==> P_0 R o1 o2) /\ 1972 (!d1 d2. RED1_dict R d1 d2 ==> P_1 R d1 d2) /\ 1973 (!e1 e2. RED1_entry R e1 e2 ==> P_2 R e1 e2) /\ 1974 (!m1 m2. RED1_method R m1 m2 ==> P_3 R m1 m2)���, 1975 GEN_TAC 1976 THEN DISCH_TAC 1977 THEN REPEAT GEN_TAC 1978 THEN STRIP_TAC 1979 THEN UNDISCH_TAC ���SUBSTITUTIVE_obj R��� 1980 THEN REWRITE_TAC[tautLib.TAUT_PROVE 1981 ���(a ==> (b /\ c)) = ((a ==> b) /\ (a ==> c))���] 1982 THEN CONV_TAC (TOP_DEPTH_CONV RIGHT_IMP_FORALL_CONV) 1983 THEN REWRITE_TAC[AND_IMP_INTRO] 1984 THEN ONCE_REWRITE_TAC[ISPEC ���SUBSTITUTIVE_obj R��� CONJ_SYM] 1985 THEN REWRITE_TAC[GSYM AND_IMP_INTRO] 1986 THEN SPEC_TAC (���R:obj->obj->bool���,���R:obj->obj->bool���) 1987 THEN CONV_TAC (TOP_DEPTH_CONV FORALL_AND_CONV) 1988 THEN MATCH_MP_TAC RED1_SUBSTITUTIVE_ind_thm_LEMMA1 1989 THEN REPEAT STRIP_TAC 1990 THEN FIRST_ASSUM MATCH_MP_TAC 1991 THEN ASM_REWRITE_TAC[] 1992 ); 1993 1994 1995 1996val RED_SUBSTITUTIVE_LEMMA = TAC_PROOF(([], 1997 ���(!R M N. 1998 RED_obj R M N ==> 1999 (SUBSTITUTIVE_obj R ==> 2000 (!L x. RED_obj R (M <[ [x,L]) (N <[ [x,L])))) /\ 2001 (!R M N. 2002 RED_dict R M N ==> 2003 (SUBSTITUTIVE_obj R ==> 2004 (!L x. RED_dict R (M <[ [x,L]) (N <[ [x,L])))) /\ 2005 (!R M N. 2006 RED_entry R M N ==> 2007 (SUBSTITUTIVE_obj R ==> 2008 (!L x. RED_entry R (M <[ [x,L]) (N <[ [x,L])))) /\ 2009 (!R M N. 2010 RED_method R M N ==> 2011 (SUBSTITUTIVE_obj R ==> 2012 (!L x. RED_method R (M <[ [x,L]) (N <[ [x,L]))))���), 2013 rule_induct RED_ind_thm (* weak, not strong induction *) 2014 THEN REPEAT STRIP_TAC (* 12 subgoals *) 2015 THEN FIRST 2016 [ REWRITE_TAC[RED_REFL] 2017 THEN NO_TAC, 2018 2019 RES_TAC 2020 THEN RULE_ASSUM_TAC SPEC_ALL 2021 THEN IMP_RES_TAC RED_TRANS 2022 THEN NO_TAC, 2023 2024 IMP_RES_TAC RED1_SUBSTITUTIVE 2025 THEN REWRITE_ALL_TAC[SUBSTITUTIVE] 2026 THEN RES_TAC 2027 THEN RULE_ASSUM_TAC SPEC_ALL 2028 THEN IMP_RES_TAC RED_RED1 2029 THEN NO_TAC 2030 ] 2031 ); 2032 2033 2034val RED_SUBSTITUTIVE = store_thm 2035 ("RED_SUBSTITUTIVE", 2036 ���!R. SUBSTITUTIVE_obj R ==> 2037 SUBSTITUTIVE_obj (RED_obj R) /\ 2038 SUBSTITUTIVE_dict (RED_dict R) /\ 2039 SUBSTITUTIVE_entry (RED_entry R) /\ 2040 SUBSTITUTIVE_method (RED_method R)���, 2041 GEN_TAC THEN DISCH_TAC 2042 THEN REWRITE_TAC[SUBSTITUTIVE] 2043 THEN REPEAT STRIP_TAC (* 12 subgoals *) 2044 THEN IMP_RES_TAC RED_SUBSTITUTIVE_LEMMA 2045 THEN ASM_REWRITE_TAC[] 2046 ); 2047 2048 2049 2050val REQUAL_SUBSTITUTIVE_LEMMA = TAC_PROOF(([], 2051 ���(!R M N. 2052 REQUAL_obj R M N ==> 2053 (SUBSTITUTIVE_obj R ==> 2054 (!L x. REQUAL_obj R (M <[ [x,L]) (N <[ [x,L])))) /\ 2055 (!R M N. 2056 REQUAL_dict R M N ==> 2057 (SUBSTITUTIVE_obj R ==> 2058 (!L x. REQUAL_dict R (M <[ [x,L]) (N <[ [x,L])))) /\ 2059 (!R M N. 2060 REQUAL_entry R M N ==> 2061 (SUBSTITUTIVE_obj R ==> 2062 (!L x. REQUAL_entry R (M <[ [x,L]) (N <[ [x,L])))) /\ 2063 (!R M N. 2064 REQUAL_method R M N ==> 2065 (SUBSTITUTIVE_obj R ==> 2066 (!L x. REQUAL_method R (M <[ [x,L]) (N <[ [x,L]))))���), 2067 rule_induct REQUAL_ind_thm (* weak, not strong induction *) 2068 THEN REPEAT STRIP_TAC (* 12 subgoals *) 2069 THEN FIRST 2070 [ RES_TAC 2071 THEN RULE_ASSUM_TAC SPEC_ALL 2072 THEN IMP_RES_TAC REQUAL_SYM 2073 THEN NO_TAC, 2074 2075 RES_TAC 2076 THEN RULE_ASSUM_TAC SPEC_ALL 2077 THEN IMP_RES_TAC REQUAL_TRANS 2078 THEN NO_TAC, 2079 2080 IMP_RES_TAC RED_SUBSTITUTIVE 2081 THEN REWRITE_ALL_TAC[SUBSTITUTIVE] 2082 THEN RES_TAC 2083 THEN RULE_ASSUM_TAC SPEC_ALL 2084 THEN IMP_RES_TAC REQUAL_RED 2085 THEN NO_TAC 2086 ] 2087 ); 2088 2089 2090val REQUAL_SUBSTITUTIVE = store_thm 2091 ("REQUAL_SUBSTITUTIVE", 2092 ���!R. SUBSTITUTIVE_obj R ==> 2093 SUBSTITUTIVE_obj (REQUAL_obj R) /\ 2094 SUBSTITUTIVE_dict (REQUAL_dict R) /\ 2095 SUBSTITUTIVE_entry (REQUAL_entry R) /\ 2096 SUBSTITUTIVE_method (REQUAL_method R)���, 2097 GEN_TAC THEN DISCH_TAC 2098 THEN REWRITE_TAC[SUBSTITUTIVE] 2099 THEN REPEAT STRIP_TAC (* 12 subgoals *) 2100 THEN IMP_RES_TAC REQUAL_SUBSTITUTIVE_LEMMA 2101 THEN ASM_REWRITE_TAC[] 2102 ); 2103 2104 2105 2106val _ = export_theory(); 2107 2108val _ = print_theory_to_file "reduction.lst"; 2109 2110val _ = html_theory "reduction"; 2111 2112val _ = print_theory_size(); 2113