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