1open HolKernel Parse boolLib; 2infix THEN THENL THENC ORELSE ORELSEC THEN_TCL ORELSE_TCL ## |->; 3infixr -->; 4 5 6 7val _ = new_theory "reduction"; 8 9 10open prim_recTheory pairTheory listTheory rich_listTheory; 11open combinTheory; 12open listLib; 13open pred_setTheory pred_setLib; 14open numTheory; 15open numLib; 16open arithmeticTheory; 17open bossLib; 18open relationTheory; 19open Mutual 20open ind_rel; 21open dep_rewrite; 22open more_listTheory; 23open more_setTheory; 24open variableTheory; 25open termTheory; 26open alphaTheory; 27open liftTheory; 28open barendregt; 29open relationTheory; 30 31 32open tactics; 33 34 35 36val vars = ty_antiq( ==`:var list`== ); 37val term = ty_antiq( ==`:'a term`== ); 38val subs = ty_antiq( ==`:(var # 'a term) list`== ); 39 40 41(* Define the transitive closure of a relation. *) 42(* Wait, it's already done: see file src/relation/relationScript.sml. *) 43(* This defines TC in the logic as TC R is the transitive closure of R, *) 44(* and "transitive R" as the property that R is transitite on 'a. *) 45(* There are also a bunch of theorems in structure TCScript, as well as *) 46(* induction tactics, cases theorems, etc. It's theory "TC". *) 47 48(* copied: *) 49 50val TC_INDUCT_TAC = 51 let val tc_thm = TC_INDUCT 52 fun tac (asl,w) = 53 let open Rsyntax 54 val {Bvar=u,Body} = dest_forall w 55 val {Bvar=v,Body} = dest_forall Body 56 val {ant,conseq} = dest_imp Body 57 val (TC,Ru'v') = strip_comb ant 58 val R = hd Ru'v' 59 val u'v' = tl Ru'v' 60 val u' = hd u'v' 61 val v' = hd (tl u'v') 62 (*val (TC,[R,u',v']) = strip_comb ant*) 63 (*val {Name = "TC",...} = dest_const TC*) 64 val _ = if #Name(dest_const TC) = "TC" then true else raise Match 65 val _ = assert (aconv u) u' 66 val _ = assert (aconv v) v' 67 val P = list_mk_abs([u,v], conseq) 68 val tc_thm' = BETA_RULE(ISPEC P (ISPEC R tc_thm)) 69 in MATCH_MP_TAC tc_thm' (asl,w) 70 end 71 handle _ => raise HOL_ERR{origin_structure = "<top-level>", 72 origin_function = "TC_INDUCT_TAC", 73 message = "Unanticipated term structure"} 74 in tac 75 end; 76 77val TC_TRANS = REWRITE_RULE[transitive_def] TC_TRANSITIVE; 78(* Also see TC_SUBSET, TC_CASES1, TC_CASES2, TC_RC_RED1_IS_RED, TC_MONOTONIC *) 79 80 81 82val HEIGHT_SUB_VAR = store_thm 83 ("HEIGHT_SUB_VAR", 84 ���!t:^term x y. 85 HEIGHT (t <[ [x,Var y]) = HEIGHT t���, 86 MUTUAL_INDUCT_THEN term_height_induct ASSUME_TAC 87 THEN REPEAT GEN_TAC 88 THENL 89 [ REWRITE_TAC[SUB_term], 90 91 REWRITE_TAC[SUB_term,SUB] 92 THEN COND_CASES_TAC 93 THEN REWRITE_TAC[HEIGHT], 94 95 REWRITE_TAC[SUB_term] 96 THEN ASM_REWRITE_TAC[HEIGHT], 97 98 SIMPLE_SUBST_TAC 99 THEN ASM_REWRITE_TAC[HEIGHT] 100 ] 101 ); 102 103 104 105(* Barendregt's Substitution Lemma, 2.1.16, page 27: *) 106 107val BARENDREGT_SUBSTITUTION_LEMMA = store_thm 108 ("BARENDREGT_SUBSTITUTION_LEMMA", 109 ���!N L x y (M:^term). 110 ~(x = y) /\ ~(x IN FV L) ==> 111 (((M <[ [x,N]) <[ [y,L]) = 112 ((M <[ [y,L]) <[ [x, (N <[ [y,L])]))���, 113 GEN_TAC THEN GEN_TAC THEN GEN_TAC THEN GEN_TAC THEN 114 MUTUAL_INDUCT_THEN term_height_induct ASSUME_TAC 115 THENL 116 [ REPEAT STRIP_TAC 117 THEN REWRITE_TAC[SUB_term], 118 119 REPEAT STRIP_TAC 120 THEN REWRITE_TAC[SUB_term,SUB] 121 THEN COND_CASES_TAC 122 THENL 123 [ POP_ASSUM REWRITE_ALL_THM 124 THEN EVERY_ASSUM REWRITE_THM 125 THEN REWRITE_TAC[SUB_term,SUB], 126 127 REWRITE_TAC[SUB_term,SUB] 128 THEN COND_CASES_TAC 129 THENL 130 [ IMP_RES_THEN REWRITE_THM subst_EMPTY, 131 132 ASM_REWRITE_TAC[SUB_term,SUB] 133 ] 134 ], 135 136 REPEAT STRIP_TAC 137 THEN RES_TAC 138 THEN ASM_REWRITE_TAC[SUB_term], 139 140 REPEAT STRIP_TAC 141 THEN SIMPLE_SUBST_TAC 142 THEN DEP_ASM_REWRITE_TAC[] 143 ] 144 ); 145 146 147val COLLAPSE_SUBST = store_thm 148 ("COLLAPSE_SUBST", 149 ���!(M:^term) x y N. 150 ~(y IN FV M) ==> 151 (((M <[ [x,Var y]) <[ [y,N]) = (M <[ [x,N]))���, 152 MUTUAL_INDUCT_THEN term_height_induct ASSUME_TAC 153 THENL 154 [ REWRITE_TAC[FV_term,IN] 155 THEN REPEAT GEN_TAC 156 THEN REWRITE_TAC[SUB_term], 157 158 REWRITE_TAC[FV_term,IN] 159 THEN REPEAT STRIP_TAC 160 THEN REWRITE_TAC[SUB_term,SUB] 161 THEN COND_CASES_TAC 162 THENL 163 [ REWRITE_TAC[SUB_term,SUB], 164 165 REWRITE_TAC[SUB_term,SUB] 166 THEN EVERY_ASSUM (REWRITE_THM o GSYM) 167 ], 168 169 REWRITE_TAC[FV_term,IN,IN_UNION,DE_MORGAN_THM] 170 THEN REPEAT STRIP_TAC 171 THEN RES_TAC 172 THEN ASM_REWRITE_TAC[SUB_term], 173 174 REPEAT GEN_TAC 175 THEN SIMPLE_SUBST_TAC 176 THEN REWRITE_TAC[FV_term,IN,DE_MORGAN_THM] 177 THEN REPEAT STRIP_TAC 178 THEN DEP_ASM_REWRITE_TAC[] 179 THEN UNDISCH_TAC ���~(y IN FV (M':^term) DIFF {z})��� 180 THEN FIRST_ASSUM (REWRITE_THM o REWRITE_RULE[FV_term] o 181 AP_TERM ���FV:^term -> var -> bool���) 182 THEN REWRITE_TAC[IN_DIFF,IN,DE_MORGAN_THM] 183 THEN EVERY_ASSUM (REWRITE_THM o GSYM) 184 ] 185 ); 186 187 188 189(* --------------------------------------------------------------------- *) 190(* General reduction relations and theorems: *) 191(* "Lambda Calculus," Barendregt, Chapter 3, page 50-63 *) 192(* --------------------------------------------------------------------- *) 193 194 195(* Define the reflexive closure of a relation. *) 196 197val RC_DEF = 198 new_definition("RC_DEF", 199 ���RC (R:'a->'a->bool) a b = 200 !P. 201 (!x y. R x y ==> P x y) /\ 202 (!x. P x x) 203 ==> P a b���); 204 205 206val RC_REFLEXIVE = store_thm 207 ("RC_REFLEXIVE", 208 ���!R (x:'a). RC R x x���, 209 REWRITE_TAC[RC_DEF] 210 THEN REPEAT STRIP_TAC 211 THEN ASM_REWRITE_TAC[] 212 ); 213 214val RC_SUBSET = store_thm 215 ("RC_SUBSET", 216 ���!R (x:'a) y. R x y ==> RC R x y���, 217 REWRITE_TAC[RC_DEF] 218 THEN REPEAT STRIP_TAC 219 THEN FIRST_ASSUM MATCH_MP_TAC 220 THEN ASM_REWRITE_TAC[] 221 ); 222 223val RC_INDUCT = store_thm 224 ("RC_INDUCT", 225 ���!(R:'a->'a->bool) P. 226 (!x y. R x y ==> P x y) /\ 227 (!x. P x x) 228 ==> !u v. RC R u v ==> P u v���, 229 REWRITE_TAC[RC_DEF] 230 THEN REPEAT STRIP_TAC 231 THEN FIRST_ASSUM MATCH_MP_TAC 232 THEN ASM_REWRITE_TAC[] 233 ); 234 235 236val RC_INDUCT_TAC = 237 let val rc_thm = RC_INDUCT 238 fun tac (asl,w) = 239 let open Rsyntax 240 val {Bvar=u,Body} = dest_forall w 241 val {Bvar=v,Body} = dest_forall Body 242 val {ant,conseq} = dest_imp Body 243 (*val (RC,[R,u',v']) = strip_comb ant*) 244 val (RC,Ruv) = strip_comb ant 245 val R = hd Ruv and u' = hd (tl Ruv) and v' = hd (tl (tl Ruv)) 246 val _ = assert (curry op = "RC") (#Name (dest_const RC)) 247 val _ = assert (aconv u) u' 248 val _ = assert (aconv v) v' 249 val P = list_mk_abs([u,v], conseq) 250 val rc_thm' = BETA_RULE(ISPEC P (ISPEC R rc_thm)) 251 in MATCH_MP_TAC rc_thm' (asl,w) 252 end 253 handle _ => raise HOL_ERR{origin_structure = "<top-level>", 254 origin_function = "RC_INDUCT_TAC", 255 message = "Unanticipated term structure"} 256 in tac 257 end; 258 259 260val RC_CASES = store_thm 261 ("RC_CASES", 262 ���!R (x:'a) y. RC R x y ==> R x y \/ (x = y)���, 263 GEN_TAC 264 THEN RC_INDUCT_TAC 265 THEN REPEAT STRIP_TAC 266 THEN ASM_REWRITE_TAC[] 267 ); 268 269 270 271(* --------------------------------------------------------------------- *) 272(* Define compatible relations on the term/method language. *) 273(* --------------------------------------------------------------------- *) 274 275val term_rel = ty_antiq ( ==`:'a term -> 'a term -> bool`== ); 276 277val compatible = 278 new_definition ("compatible", 279 ���compatible R = 280 (!t1:^term t2. R t1 t2 ==> (!u. R (App u t1) (App u t2)) /\ 281 (!u. R (App t1 u) (App t2 u)) /\ 282 (!x. R (Lam x t1) (Lam x t2)))���); 283 284val reflexive = 285 new_definition ("reflexive", 286 ���reflexive R = 287 (!t:^term. R t t)���); 288 289val symmetric = 290 new_definition ("symmetric", 291 ���symmetric R = 292 (!t1 t2:^term. R t1 t2 ==> R t2 t1)���); 293 294(* Already defined in relationTheory: 295val transitive_def = 296 new_definition ("transitive_def", 297 ���transitve R = 298 (!t1 t2 t3:^term. R t1 t2 /\ R t2 t3 ==> R t1 t3)���); 299*) 300val transitive = relationTheory.transitive_def; 301 302val equality = 303 new_definition ("equality", 304 ���equality (R:^term_rel) = 305 (compatible R /\ 306 reflexive R /\ 307 symmetric R /\ 308 transitive R)���); 309 310val reduction = 311 new_definition ("reduction", 312 ���reduction (R:^term_rel) = 313 (compatible R /\ 314 reflexive R /\ 315 transitive R)���); 316 317 318val RC_compatible = store_thm 319 ("RC_compatible", 320 ���!R:^term_rel. compatible R ==> compatible (RC R)���, 321 REWRITE_TAC[compatible] 322 THEN REPEAT STRIP_TAC 323 THEN ( IMP_RES_TAC RC_CASES 324 THENL 325 [ MATCH_MP_TAC RC_SUBSET 326 THEN RES_TAC 327 THEN ASM_REWRITE_TAC[], 328 329 ASM_REWRITE_TAC[RC_REFLEXIVE] 330 ] 331 ) 332 ); 333 334val TC_compatible1 = TAC_PROOF(([], 335 ���!(R:^term_rel) t1 t2. TC R t1 t2 ==> 336 compatible R ==> 337 (!u. TC R (App u t1) (App u t2)) /\ 338 (!u. TC R (App t1 u) (App t2 u)) /\ 339 (!x. TC R (Lam x t1) (Lam x t2))���), 340 GEN_TAC 341 THEN TC_INDUCT_TAC 342 THEN CONJ_TAC 343 THENL 344 [ REWRITE_TAC[compatible] 345 THEN REPEAT STRIP_TAC 346 THEN RES_TAC 347 THEN MATCH_MP_TAC TC_SUBSET 348 THEN ASM_REWRITE_TAC[], 349 350 REPEAT STRIP_TAC 351 THEN RES_TAC 352 THEN MATCH_MP_TAC TC_TRANS 353 THENL 354 [ EXISTS_TAC ``App u y :^term``, 355 EXISTS_TAC ``App y u :^term``, 356 EXISTS_TAC ``Lam x' y :^term`` 357 ] 358 THEN ASM_REWRITE_TAC[] 359 ] 360 ); 361 362val TC_compatible = store_thm 363 ("TC_compatible", 364 ���!(R:^term_rel). compatible R ==> compatible (TC R)���, 365 GEN_TAC 366 THEN DISCH_TAC 367 THEN REWRITE_TAC[compatible] 368 THEN REPEAT GEN_TAC 369 THEN DISCH_TAC 370 THEN IMP_RES_TAC TC_compatible1 371 THEN ASM_REWRITE_TAC[] 372 ); 373 374 375 376(* --------------------------------------------------------------------- *) 377(* (RED1 R t1 t2) means that the term t1 reduces to the term t2 *) 378(* in exactly one step, as defined in Barendregt, Definition 3.1.5, *) 379(* page 51. This is the compatible closure of R. *) 380(* --------------------------------------------------------------------- *) 381 382 383val RED1 = 384���RED1 : ^term_rel -> ^term -> ^term -> bool���; 385 386val RED1_patterns = [���^RED1 R t1 t2���]; 387 388val RED1_rules_tm = 389��� 390 ((R t1 t2) 391 (* -------------------------------------------- *) ==> 392 (^RED1 R t1 t2)) /\ 393 394 395 ((^RED1 R t1 t2) 396 (* -------------------------------------------- *) ==> 397 (^RED1 R (App t1 u) (App t2 u))) /\ 398 399 400 ((^RED1 R u1 u2) 401 (* -------------------------------------------- *) ==> 402 (^RED1 R (App t u1) (App t u2))) /\ 403 404 405 ((^RED1 R t1 t2) 406 (* -------------------------------------------- *) ==> 407 (^RED1 R (Lam x t1) (Lam x t2))) 408���; 409 410val (RED1_rules_sat,RED1_ind_thm) = 411 define_inductive_relations RED1_patterns RED1_rules_tm; 412 413val RED1_inv_thms = prove_inversion_theorems 414 RED1_rules_sat RED1_ind_thm; 415 416val RED1_strong_ind = prove_strong_induction 417 RED1_rules_sat RED1_ind_thm; 418 419val _ = save_thm ("RED1_rules_sat", RED1_rules_sat); 420val _ = save_thm ("RED1_ind_thm", RED1_ind_thm); 421val _ = save_thm ("RED1_inv_thms", LIST_CONJ RED1_inv_thms); 422val _ = save_thm ("RED1_strong_ind", RED1_strong_ind); 423 424 425val [RED1_R, RED1_App1, RED1_App2, RED1_Lam] = CONJUNCTS RED1_rules_sat; 426 427 428 429 430val RED1_height_ind_thm_LEMMA = store_thm 431 ("RED1_height_ind_thm_LEMMA", 432 ���!n (P_0:^term_rel -> ^term -> ^term -> bool). 433 (!R t1 t2. R t1 t2 ==> P_0 R t1 t2) /\ 434 (!R t1 u t2. P_0 R t1 t2 ==> P_0 R (App t1 u) (App t2 u)) /\ 435 (!R t u1 u2. P_0 R u1 u2 ==> P_0 R (App t u1) (App t u2)) /\ 436 (!R x t1 t2. 437 (!t1' t2'. RED1 R t1' t2' /\ 438 (HEIGHT t1 = HEIGHT t1') /\ 439 (HEIGHT t2 = HEIGHT t2') ==> P_0 R t1' t2') 440 ==> P_0 R (Lam x t1) (Lam x t2)) ==> 441 (!R t1 t2. RED1 R t1 t2 ==> 442 ((HEIGHT t1 <= n) /\ 443 (HEIGHT t2 <= n) ==> 444 P_0 R t1 t2))���, 445 INDUCT_TAC 446 THEN REPEAT GEN_TAC 447 THEN STRIP_TAC 448 THENL 449 [ REWRITE_TAC[HEIGHT_LESS_EQ_ZERO] 450 THEN REPEAT STRIP_TAC 451 THEN ASM_REWRITE_TAC[] 452 THEN FIRST_ASSUM MATCH_MP_TAC 453 THEN UNDISCH_TAC ���RED1 R (t1:^term) t2��� 454 THEN ONCE_REWRITE_TAC RED1_inv_thms 455 THEN ASM_REWRITE_TAC[term_distinct], 456 457 UNDISCH_ALL_TAC 458 THEN DISCH_THEN ((fn th => REPEAT DISCH_TAC 459 THEN ASSUME_TAC th) o SPEC_ALL) 460 THEN POP_ASSUM MP_TAC 461 THEN ASM_REWRITE_TAC[] 462 THEN DISCH_THEN (fn th => UNDISCH_ALL_TAC THEN STRIP_ASSUME_TAC th) 463 THEN REPEAT DISCH_TAC 464 THEN rule_induct RED1_ind_thm 465 THEN REWRITE_TAC[HEIGHT] 466 THEN REWRITE_TAC[MAX_SUC,MAX_LESS_EQ,LESS_EQ_MONO,ZERO_LESS_EQ] 467 THEN REPEAT STRIP_TAC 468 THEN ASM_REWRITE_TAC[] 469 THENL (* 4 subgoals *) 470 [ FIRST_ASSUM MATCH_MP_TAC 471 THEN ASM_REWRITE_TAC[], 472 473 FIRST_ASSUM MATCH_MP_TAC 474 THEN FIRST_ASSUM MATCH_MP_TAC 475 THEN IMP_RES_TAC LESS_EQ_IMP_LESS_SUC 476 THEN IMP_RES_TAC LESS_IMP_LESS_OR_EQ 477 THEN ASM_REWRITE_TAC[], 478 479 FIRST_ASSUM MATCH_MP_TAC 480 THEN FIRST_ASSUM MATCH_MP_TAC 481 THEN IMP_RES_TAC LESS_EQ_IMP_LESS_SUC 482 THEN IMP_RES_TAC LESS_IMP_LESS_OR_EQ 483 THEN ASM_REWRITE_TAC[], 484 485 FIRST_ASSUM MATCH_MP_TAC 486 THEN REPEAT STRIP_TAC 487 THEN ASSUM_LIST 488 (MATCH_MP_TAC o REWRITE_RULE[AND_IMP_INTRO] o hd o rev) 489 THEN POP_ASSUM (REWRITE_THM o SYM) 490 THEN POP_ASSUM (REWRITE_THM o SYM) 491 THEN ASM_REWRITE_TAC[] 492 ] 493 ] 494 ); 495 496val RED1_height_ind_thm = store_thm 497 ("RED1_height_ind_thm", 498 ���!P_0. 499 (!R (t1:^term) t2. R t1 t2 ==> P_0 R t1 t2) /\ 500 (!R t1 t2 u. P_0 R t1 t2 ==> P_0 R (App t1 u) (App t2 u)) /\ 501 (!R t u1 u2. P_0 R u1 u2 ==> P_0 R (App t u1) (App t u2)) /\ 502 (!R x t1 t2. 503 (!t1' t2'. RED1 R t1' t2' /\ 504 (HEIGHT t1 = HEIGHT t1') /\ 505 (HEIGHT t2 = HEIGHT t2') ==> P_0 R t1' t2') 506 ==> P_0 R (Lam x t1) (Lam x t2)) ==> 507 (!R t1 t2. RED1 R t1 t2 ==> P_0 R t1 t2)���, 508 REPEAT STRIP_TAC 509 THEN MP_TAC (SPEC_ALL 510 (SPEC ���(HEIGHT (t1:^term)) MAX (HEIGHT (t2:^term))��� 511 RED1_height_ind_thm_LEMMA)) 512 THEN ASM_REWRITE_TAC[AND_IMP_INTRO] 513 THEN REPEAT STRIP_TAC 514 THEN FIRST_ASSUM MATCH_MP_TAC 515 THEN ASM_REWRITE_TAC[LESS_EQ_MAX] 516 ); 517 518val RED1_height_strong_ind_LEMMA = store_thm 519 ("RED1_height_strong_ind_LEMMA", 520 ���!n P_0. 521 (!R (t1:^term) t2. R t1 t2 ==> P_0 R t1 t2) /\ 522 (!R t1 t2 u. 523 P_0 R t1 t2 /\ RED1 R t1 t2 ==> 524 P_0 R (App t1 u) (App t2 u)) /\ 525 (!R t u1 u2. 526 P_0 R u1 u2 /\ RED1 R u1 u2 ==> 527 P_0 R (App t u1) (App t u2)) /\ 528 (!R x t1 t2. 529 (!t1' t2'. 530 RED1 R t1' t2' /\ 531 (HEIGHT t1 = HEIGHT t1') /\ 532 (HEIGHT t2 = HEIGHT t2') ==> 533 P_0 R t1' t2') /\ 534 RED1 R t1 t2 ==> 535 P_0 R (Lam x t1) (Lam x t2)) ==> 536 (!R t1 t2. RED1 R t1 t2 ==> 537 ((HEIGHT t1 <= n) /\ 538 (HEIGHT t2 <= n) ==> 539 P_0 R t1 t2))���, 540 INDUCT_TAC 541 THEN REPEAT GEN_TAC 542 THEN STRIP_TAC 543 THENL 544 [ REWRITE_TAC[HEIGHT_LESS_EQ_ZERO] 545 THEN REPEAT STRIP_TAC 546 THEN ASM_REWRITE_TAC[] 547 THEN FIRST_ASSUM MATCH_MP_TAC 548 THEN UNDISCH_TAC ���RED1 R (t1:^term) t2��� 549 THEN ONCE_REWRITE_TAC RED1_inv_thms 550 THEN ASM_REWRITE_TAC[term_distinct], 551 552 UNDISCH_ALL_TAC 553 THEN DISCH_THEN ((fn th => REPEAT DISCH_TAC 554 THEN ASSUME_TAC th) o SPEC_ALL) 555 THEN POP_ASSUM MP_TAC 556 THEN ASM_REWRITE_TAC[] 557 THEN DISCH_THEN (fn th => UNDISCH_ALL_TAC THEN STRIP_ASSUME_TAC th) 558 THEN REPEAT DISCH_TAC 559 THEN rule_induct RED1_strong_ind 560 THEN REWRITE_TAC[HEIGHT] 561 THEN REWRITE_TAC[MAX_SUC,MAX_LESS_EQ,LESS_EQ_MONO,ZERO_LESS_EQ] 562 THEN REPEAT STRIP_TAC 563 THEN ASM_REWRITE_TAC[] 564 THENL (* 4 subgoals *) 565 [ FIRST_ASSUM MATCH_MP_TAC 566 THEN ASM_REWRITE_TAC[], 567 568 FIRST_ASSUM MATCH_MP_TAC 569 THEN ASM_REWRITE_TAC[] 570 THEN FIRST_ASSUM MATCH_MP_TAC 571 THEN IMP_RES_TAC LESS_EQ_IMP_LESS_SUC 572 THEN IMP_RES_TAC LESS_IMP_LESS_OR_EQ 573 THEN ASM_REWRITE_TAC[], 574 575 FIRST_ASSUM MATCH_MP_TAC 576 THEN ASM_REWRITE_TAC[] 577 THEN FIRST_ASSUM MATCH_MP_TAC 578 THEN IMP_RES_TAC LESS_EQ_IMP_LESS_SUC 579 THEN IMP_RES_TAC LESS_IMP_LESS_OR_EQ 580 THEN ASM_REWRITE_TAC[], 581 582 FIRST_ASSUM MATCH_MP_TAC 583 THEN ASM_REWRITE_TAC[] 584 THEN REPEAT STRIP_TAC 585 THEN UNDISCH_THEN 586 ���!(R:^term->^term->bool) t1 t2. R t1 t2 ==> P_0 R t1 t2��� 587 (fn th => ALL_TAC) 588 THEN FIRST_ASSUM (MATCH_MP_TAC o REWRITE_RULE[AND_IMP_INTRO]) 589 THEN POP_ASSUM (REWRITE_THM o SYM) 590 THEN POP_ASSUM (REWRITE_THM o SYM) 591 THEN IMP_RES_TAC LESS_EQ_IMP_LESS_SUC 592 THEN IMP_RES_TAC LESS_IMP_LESS_OR_EQ 593 THEN ASM_REWRITE_TAC[] 594 ] 595 ] 596 ); 597 598val RED1_height_strong_ind = store_thm 599 ("RED1_height_strong_ind", 600 ���!P_0. 601 (!R (t1:^term) t2. R t1 t2 ==> P_0 R t1 t2) /\ 602 (!R t1 t2 u. 603 P_0 R t1 t2 /\ RED1 R t1 t2 ==> P_0 R (App t1 u) (App t2 u)) /\ 604 (!R t u1 u2. 605 P_0 R u1 u2 /\ RED1 R u1 u2 ==> P_0 R (App t u1) (App t u2)) /\ 606 (!R x t1 t2. 607 (!t1' t2'. 608 RED1 R t1' t2' /\ 609 (HEIGHT t1 = HEIGHT t1') /\ 610 (HEIGHT t2 = HEIGHT t2') ==> 611 P_0 R t1' t2') /\ 612 RED1 R t1 t2 ==> 613 P_0 R (Lam x t1) (Lam x t2)) ==> 614 (!R t1 t2. RED1 R t1 t2 ==> P_0 R t1 t2)���, 615 REPEAT STRIP_TAC 616 THEN MP_TAC (SPEC_ALL 617 (SPEC ���(HEIGHT (t1:^term)) MAX (HEIGHT (t2:^term))��� 618 RED1_height_strong_ind_LEMMA)) 619 THEN ASM_REWRITE_TAC[AND_IMP_INTRO] 620 THEN REPEAT STRIP_TAC 621 THEN FIRST_ASSUM MATCH_MP_TAC 622 THEN ASM_REWRITE_TAC[LESS_EQ_MAX] 623 ); 624 625 626 627 628(* --------------------------------------------------------------------- *) 629(* We claim that RED1 is a binary relation on the object/method *) 630(* language which is *) 631(* 1) compatible (in the sense of Barendregt, Definition 3.1.1, pg 50 *) 632(* 2) the compatible closure of the R relation, in the sense of *) 633(* Barendregt, Definition 3.1.4, pg 51 *) 634(* --------------------------------------------------------------------- *) 635 636 637val RED1_compatible = store_thm 638 ("RED1_compatible", 639 ���!R:^term_rel. compatible (RED1 R)���, 640 REWRITE_TAC[compatible] 641 THEN rule_induct RED1_strong_ind 642 THEN REPEAT STRIP_TAC 643 THEN IMP_RES_TAC RED1_R 644 THEN FIRST (map (fn th => MATCH_MP_TAC th 645 THEN ASM_REWRITE_TAC[] 646 THEN NO_TAC) 647 (CONJUNCTS RED1_rules_sat)) 648 ); 649 650val RC_RED1_compatible = store_thm 651 ("RC_RED1_compatible", 652 ���!R:^term_rel. compatible (RC (RED1 R))���, 653 GEN_TAC 654 THEN MATCH_MP_TAC RC_compatible 655 THEN REWRITE_TAC[RED1_compatible] 656 ); 657 658val TC_RC_RED1_compatible = store_thm 659 ("TC_RC_RED1_compatible", 660 ���!R:^term_rel. compatible (TC (RC (RED1 R)))���, 661 GEN_TAC 662 THEN MATCH_MP_TAC TC_compatible 663 THEN REWRITE_TAC[RC_RED1_compatible] 664 ); 665 666 667(* If R is monotonic, then RED1 R is monotonic 668 with respect to free variables. *) 669 670val RED1_FV_LEMMA = TAC_PROOF(([], 671 ���!R (M:^term) M'. 672 RED1 R M M' ==> (!N N'. R N N' ==> (FV N' SUBSET FV N)) ==> 673 (FV M' SUBSET FV M)���), 674 rule_induct RED1_strong_ind (* strong, not weak induction *) 675 THEN REWRITE_TAC[FV_term] 676 THEN REPEAT STRIP_TAC (* 4 subgoals *) 677 THENL 678 [ RES_TAC, 679 680 RES_TAC 681 THEN MATCH_MP_TAC SUBSETS_UNION 682 THEN ASM_REWRITE_TAC[SUBSET_REFL], 683 684 RES_TAC 685 THEN MATCH_MP_TAC SUBSETS_UNION 686 THEN ASM_REWRITE_TAC[SUBSET_REFL], 687 688 RES_TAC 689 THEN MATCH_MP_TAC SUBSET_DIFF 690 THEN ASM_REWRITE_TAC[] 691 ] 692 ); 693 694val RED1_FV = store_thm 695 ("RED1_FV", 696 ���!R. 697 (!(N:^term) N'. R N N' ==> (FV N' SUBSET FV N)) ==> 698 (!M M'. RED1 R M M' ==> (FV M' SUBSET FV M))���, 699 REPEAT STRIP_TAC 700 THEN IMP_RES_TAC RED1_FV_LEMMA 701 ); 702 703 704 705(* We now need to define the reflexive and transitive closure of this. *) 706 707(* --------------------------------------------------------------------- *) 708(* (RED R t1 t2) means that the term t1 reduces to the term t2 *) 709(* in zero or more steps, as defined in Barendregt, Definition 3.1.5, *) 710(* page 51. This is the reflexive and transitive closure of RED1 R. *) 711(* --------------------------------------------------------------------- *) 712 713val RED = 714���RED : ^term_rel -> ^term -> ^term -> bool���; 715 716val RED_patterns = [���^RED R t1 t2���]; 717 718val RED_rules_tm = 719��� 720 721 (RED1 R t1 t2 722 (* -------------------------------------------- *) ==> 723 ^RED R t1 t2) /\ 724 725 726 (* -------------------------------------------- *) 727 (^RED R t1 t1) /\ 728 729 730 (^RED R t1 t2 /\ ^RED R t2 t3 731 (* -------------------------------------------- *) ==> 732 ^RED R t1 t3) 733���; 734 735 736val (RED_rules_sat,RED_ind_thm) = 737 define_inductive_relations RED_patterns RED_rules_tm; 738 739val RED_inv_thms = prove_inversion_theorems 740 RED_rules_sat RED_ind_thm; 741 742val RED_strong_ind = prove_strong_induction 743 RED_rules_sat RED_ind_thm; 744 745val _ = save_thm ("RED_rules_sat", RED_rules_sat); 746val _ = save_thm ("RED_ind_thm", RED_ind_thm); 747val _ = save_thm ("RED_inv_thms", LIST_CONJ RED_inv_thms); 748val _ = save_thm ("RED_strong_ind", RED_strong_ind); 749 750 751(* --------------------------------------------------------------------- *) 752(* We claim that RED is a binary relation on the object/method *) 753(* language which is *) 754(* 1) compatible (in the sense of Barendregt, Definition 3.1.1, pg 50 *) 755(* 2) the reflexive, transitive closure of the REDC relation, in the *) 756(* sense of Barendregt, Definition 3.1.4 and 3.1.5, pg 51 *) 757(* 3) a reduction relation, from 1) and 2). *) 758(* --------------------------------------------------------------------- *) 759 760 761val [RED_RED1, RED_REFL, RED_TRANS] 762 = CONJUNCTS (CONV_RULE (DEPTH_CONV LEFT_IMP_EXISTS_CONV) RED_rules_sat); 763 764 765val [RED_inv] 766 = RED_inv_thms; 767 768 769val RED_reflexive = store_thm 770 ("RED_reflexive", 771 ���!R:^term_rel. reflexive (RED R)���, 772 REWRITE_TAC[reflexive] 773 THEN REWRITE_TAC[RED_REFL] 774 ); 775 776val RED_transitive = store_thm 777 ("RED_transitive", 778 ���!R:^term_rel. transitive (RED R)���, 779 REWRITE_TAC[transitive] 780 THEN REWRITE_TAC[CONV_RULE (DEPTH_CONV LEFT_IMP_EXISTS_CONV) 781 RED_rules_sat] 782 ); 783 784val RED_TRANS = save_thm("RED_TRANS", 785 REWRITE_RULE[transitive] RED_transitive); 786 787val RED_compatible = store_thm 788 ("RED_compatible", 789 ���!R:^term_rel. compatible (RED R)���, 790 REWRITE_TAC[compatible] 791 THEN rule_induct RED_ind_thm (* weak, not strong induction *) 792 THEN REPEAT STRIP_TAC (* 9 subgoals *) 793 THEN REWRITE_TAC[RED_REFL] (* takes care of 3 *) 794 THEN RULE_ASSUM_TAC SPEC_ALL 795 THEN IMP_RES_TAC RED_TRANS (* solves another 3 *) 796 THEN IMP_RES_TAC (REWRITE_RULE[compatible] RED1_compatible) 797 THEN RULE_ASSUM_TAC SPEC_ALL 798 THEN IMP_RES_TAC RED_RED1 (* finishes the last 3 *) 799 ); 800 801val RED_COMPAT = save_thm("RED_COMPAT", 802 (REWRITE_RULE[compatible] RED_compatible)); 803 804 805 806val RED_reduction = store_thm 807 ("RED_reduction", 808 ���!R:^term_rel. reduction (RED R)���, 809 REWRITE_TAC[reduction] 810 THEN REWRITE_TAC[RED_compatible,RED_reflexive,RED_transitive] 811 ); 812 813 814(* Barendregt's Substitution Remark, 3.1.7, page 52: *) 815 816val BARENDREGT_SUBSTITUTION_REMARK = store_thm 817 ("BARENDREGT_SUBSTITUTION_REMARK", 818 ���!(M:^term) N N' x R. 819 RED R N N' ==> 820 RED R (M <[ [x,N]) (M <[ [x,N'])���, 821 MUTUAL_INDUCT_THEN term_height_induct ASSUME_TAC 822 THENL 823 [ REPEAT STRIP_TAC 824 THEN REWRITE_TAC[SUB_term] 825 THEN REWRITE_TAC[RED_REFL], 826 827 REPEAT STRIP_TAC 828 THEN REWRITE_TAC[SUB_term,SUB] 829 THEN COND_CASES_TAC 830 THENL 831 [ ASM_REWRITE_TAC[], 832 833 REWRITE_TAC[RED_REFL] 834 ], 835 836 REPEAT STRIP_TAC 837 THEN RES_TAC 838 THEN REWRITE_TAC[SUB_term] 839 THEN MATCH_MP_TAC RED_TRANS 840 THEN EXISTS_TAC ���App ((M:^term) <[ [x,N']) (M' <[ [x,N])��� 841 THEN RULE_ASSUM_TAC SPEC_ALL 842 THEN IMP_RES_TAC RED_COMPAT 843 THEN ASM_REWRITE_TAC[], 844 845 REPEAT STRIP_TAC 846 THEN SIMPLE_SUBST_TAC 847 THEN RES_TAC 848 THEN POP_ASSUM (ASSUME_TAC o SPEC ���x:var���) 849 THEN IMP_RES_TAC RED_COMPAT 850 THEN ASM_REWRITE_TAC[] 851 ] 852 ); 853 854 855 856 857(* We now need to define the equivalence relation generated by R. *) 858 859(* --------------------------------------------------------------------- *) 860(* (REQUAL R t1 t2) means that the term t1 is R-convertible to the *) 861(* term t2, as defined in Barendregt, Definition 3.1.5, page 51. *) 862(* This is the symmetric and transitive closure of RED R. *) 863(* --------------------------------------------------------------------- *) 864 865val REQUAL = 866���REQUAL : ^term_rel -> ^term -> ^term -> bool���; 867 868val REQUAL_patterns = [���^REQUAL R t1 t2���]; 869 870val REQUAL_rules_tm = 871��� 872 (RED R t1 t2 873 (* -------------------------------------------- *) ==> 874 ^REQUAL R t1 t2) /\ 875 876 (REQUAL R t1 t2 877 (* -------------------------------------------- *) ==> 878 ^REQUAL R t2 t1) /\ 879 880 (^REQUAL R t1 t2 /\ ^REQUAL R t2 t3 881 (* -------------------------------------------- *) ==> 882 ^REQUAL R t1 t3) 883���; 884 885 886val (REQUAL_rules_sat,REQUAL_ind_thm) = 887 define_inductive_relations REQUAL_patterns REQUAL_rules_tm; 888 889val REQUAL_inv_thms = prove_inversion_theorems 890 REQUAL_rules_sat REQUAL_ind_thm; 891 892val REQUAL_strong_ind = prove_strong_induction 893 REQUAL_rules_sat REQUAL_ind_thm; 894 895val _ = save_thm ("REQUAL_rules_sat", REQUAL_rules_sat); 896val _ = save_thm ("REQUAL_ind_thm", REQUAL_ind_thm); 897val _ = save_thm ("REQUAL_inv_thms", LIST_CONJ REQUAL_inv_thms); 898val _ = save_thm ("REQUAL_strong_ind", REQUAL_strong_ind); 899 900 901(* --------------------------------------------------------------------- *) 902(* We claim that REQUAL is a binary relation on the object/method *) 903(* language which is *) 904(* 1) compatible (in the sense of Barendregt, Definition 3.1.1, pg 50 *) 905(* 2) the symmetric, transitive closure of the RED relation, in the *) 906(* sense of Barendregt, Definition 3.1.4 and 3.1.5, pg 51. *) 907(* 3) an equivalence relation, from 2) and that RED is reflexive. *) 908(* 4) an equality relation, as a compatible equivalence relation. *) 909(* --------------------------------------------------------------------- *) 910 911 912val [REQUAL_RED, REQUAL_SYM, REQUAL_TRANS] 913 = CONJUNCTS (CONV_RULE (DEPTH_CONV LEFT_IMP_EXISTS_CONV) REQUAL_rules_sat); 914 915 916val [REQUAL_inv] = REQUAL_inv_thms; 917 918 919val REQUAL_reflexive = store_thm 920 ("REQUAL_reflexive", 921 ���!R:^term_rel. reflexive (REQUAL R)���, 922 REWRITE_TAC[reflexive] 923 THEN REPEAT STRIP_TAC 924 THEN MATCH_MP_TAC REQUAL_RED 925 THEN REWRITE_TAC[RED_REFL] 926 ); 927 928val REQUAL_symmetric = store_thm 929 ("REQUAL_symmetric", 930 ���!R:^term_rel. symmetric (REQUAL R)���, 931 REWRITE_TAC[symmetric] 932 THEN REWRITE_TAC[REQUAL_SYM] 933 ); 934 935val REQUAL_transitive = store_thm 936 ("REQUAL_transitive", 937 ���!R:^term_rel. transitive (REQUAL R)���, 938 REWRITE_TAC[transitive_def] 939 THEN REWRITE_TAC[CONV_RULE (DEPTH_CONV LEFT_IMP_EXISTS_CONV) 940 REQUAL_rules_sat] 941 ); 942 943val REQUAL_TRANS = save_thm("REQUAL_TRANS", 944 REWRITE_RULE[transitive_def] REQUAL_transitive); 945 946val REQUAL_compatible = store_thm 947 ("REQUAL_compatible", 948 ���!R:^term_rel. compatible (REQUAL R)���, 949 REWRITE_TAC[compatible] 950 THEN CONV_TAC (TOP_DEPTH_CONV FORALL_AND_CONV) 951 THEN rule_induct REQUAL_ind_thm (* weak, not strong induction *) 952 THEN REPEAT STRIP_TAC (* 9 subgoals *) 953 THEN RULE_ASSUM_TAC SPEC_ALL 954 THEN IMP_RES_TAC REQUAL_SYM (* takes care of 3 *) 955 THEN IMP_RES_TAC REQUAL_TRANS (* solves another 3 *) 956 THEN IMP_RES_TAC RED_COMPAT 957 THEN RULE_ASSUM_TAC SPEC_ALL 958 THEN IMP_RES_TAC REQUAL_RED (* finishes the last 3 *) 959 ); 960 961val REQUAL_COMPAT = save_thm("REQUAL_COMPAT", 962 REWRITE_RULE[compatible] REQUAL_compatible); 963 964 965val REQUAL_reduction = store_thm 966 ("REQUAL_reduction", 967 ���!R:^term_rel. reduction (REQUAL R)���, 968 REWRITE_TAC[reduction] 969 THEN REWRITE_TAC[REQUAL_compatible,REQUAL_reflexive,REQUAL_transitive] 970 ); 971 972val REQUAL_equality = store_thm 973 ("REQUAL_equality", 974 ���!R:^term_rel. equality (REQUAL R)���, 975 REWRITE_TAC[equality] 976 THEN REWRITE_TAC[REQUAL_compatible,REQUAL_reflexive, 977 REQUAL_symmetric,REQUAL_transitive] 978 ); 979 980 981 982 (* ============ *) 983 (* NORMAL FORMS *) 984 (* ============ *) 985 986 987 988val NORMAL_FORM = 989 new_definition 990 ("NORMAL_FORM", 991 ���NORMAL_FORM R a = (!a':^term. ~(RED1 R a a'))���); 992 993 994val NORMAL_FORM_OF = 995 new_definition 996 ("NORMAL_FORM_OF", 997 ���NORMAL_FORM_OF R (a:^term) b = 998 (NORMAL_FORM R a /\ REQUAL R b a)���); 999 1000 1001val NORMAL_FORM_IDENT_LEMMA = store_thm 1002 ("NORMAL_FORM_IDENT_LEMMA", 1003 ���!R (M:^term) N. RED R M N ==> (NORMAL_FORM R M ==> (M = N))���, 1004 rule_induct RED_ind_thm (* weak, not strong induction *) 1005 THEN REWRITE_TAC[NORMAL_FORM] 1006 THEN REPEAT STRIP_TAC 1007 THEN RES_TAC 1008 THEN POP_ASSUM REWRITE_ALL_THM 1009 THEN RES_TAC 1010 ); 1011 1012val NORMAL_FORM_IDENT = store_thm 1013 ("NORMAL_FORM_IDENT", 1014 ���!R (M:^term). NORMAL_FORM R M ==> (!N. RED R M N ==> (M = N))���, 1015 REPEAT STRIP_TAC 1016 THEN IMP_RES_TAC NORMAL_FORM_IDENT_LEMMA 1017 ); 1018 1019 1020(* THE DIAMOND PROPERTY *) 1021 1022 1023val DIAMOND = 1024 new_definition 1025 ("DIAMOND", 1026 ���DIAMOND R = (!a b c:'a. R a b /\ R a c ==> (?d. R b d /\ R c d))���); 1027 1028 1029(* THE CHURCH-ROSSER PROPERTY *) 1030 1031 1032val CHURCH_ROSSER = 1033 new_definition 1034 ("CHURCH_ROSSER", 1035 ���CHURCH_ROSSER (R:^term_rel) = DIAMOND (RED R)���); 1036 1037 1038 1039val NORMAL_FORM_EXISTS_LEMMA = store_thm 1040 ("NORMAL_FORM_EXISTS_LEMMA", 1041 ���!R M N. REQUAL R M N ==> 1042 (CHURCH_ROSSER R ==> 1043 (?Z:^term. RED R M Z /\ RED R N Z))���, 1044 rule_induct REQUAL_ind_thm (* weak, not strong induction *) 1045 THEN REWRITE_TAC[CHURCH_ROSSER,DIAMOND] 1046 THEN REPEAT STRIP_TAC (* 3 subgoals *) 1047 THENL 1048 [ EXISTS_TAC ���t2:^term��� 1049 THEN ASM_REWRITE_TAC[RED_REFL], 1050 1051 UNDISCH_ALL_TAC 1052 THEN DISCH_THEN (fn th => REPEAT DISCH_TAC THEN MP_TAC th) 1053 THEN ASM_REWRITE_TAC[] 1054 THEN STRIP_TAC 1055 THEN EXISTS_TAC ���Z:^term��� 1056 THEN ASM_REWRITE_TAC[], 1057 1058 UNDISCH_ALL_TAC 1059 THEN DISCH_THEN (fn th1 => 1060 DISCH_THEN (fn th2 => 1061 REPEAT DISCH_TAC THEN MP_TAC th2 THEN MP_TAC th1)) 1062 THEN ASM_REWRITE_TAC[] 1063 THEN REPEAT STRIP_TAC 1064 THEN FIRST_ASSUM (fn imp => STRIP_ASSUME_TAC 1065 (MATCH_MP imp (CONJ (ASSUME ���RED R t2 (Z:^term)���) 1066 (ASSUME ���RED R t2 (Z':^term)���)))) 1067 THEN EXISTS_TAC ���d:^term��� 1068 THEN IMP_RES_TAC RED_TRANS 1069 THEN ASM_REWRITE_TAC[] 1070 ] 1071 ); 1072 1073val NORMAL_FORM_EXISTS = store_thm 1074 ("NORMAL_FORM_EXISTS", 1075 ���!R. CHURCH_ROSSER R ==> 1076 (!M N. REQUAL R M N ==> 1077 (?Z:^term. RED R M Z /\ RED R N Z))���, 1078 REPEAT STRIP_TAC 1079 THEN IMP_RES_TAC NORMAL_FORM_EXISTS_LEMMA 1080 THEN EXISTS_TAC ���Z:^term��� 1081 THEN ASM_REWRITE_TAC[] 1082 ); 1083 1084val NORMAL_FORM_REDUCED_TO = store_thm 1085 ("NORMAL_FORM_REDUCED_TO", 1086 ���!R. CHURCH_ROSSER R ==> 1087 (!(M:^term) N. NORMAL_FORM_OF R N M ==> RED R M N)���, 1088 REWRITE_TAC[NORMAL_FORM_OF] 1089 THEN REPEAT STRIP_TAC 1090 THEN IMP_RES_TAC NORMAL_FORM_EXISTS 1091 THEN IMP_RES_TAC NORMAL_FORM_IDENT 1092 THEN ASM_REWRITE_TAC[] 1093 ); 1094 1095val NORMAL_FORM_UNIQUE = store_thm 1096 ("NORMAL_FORM_UNIQUE", 1097 ���!R. CHURCH_ROSSER R ==> 1098 (!(M:^term) N1 N2. 1099 NORMAL_FORM_OF R N1 M /\ 1100 NORMAL_FORM_OF R N2 M ==> (N1 = N2))���, 1101 REWRITE_TAC[NORMAL_FORM_OF] 1102 THEN REPEAT STRIP_TAC 1103 THEN IMP_RES_TAC REQUAL_SYM 1104 THEN UNDISCH_LAST_TAC 1105 (* THEN POP_TAC *) 1106 THEN DISCH_TAC 1107 THEN IMP_RES_TAC REQUAL_TRANS 1108 (* THEN POP_TAC THEN POP_TAC THEN POP_TAC *) 1109 THEN IMP_RES_TAC NORMAL_FORM_EXISTS 1110 (* THEN POP_TAC THEN POP_TAC THEN POP_TAC 1111 THEN POP_TAC THEN POP_TAC THEN POP_TAC 1112 THEN POP_TAC THEN POP_TAC THEN POP_TAC *) 1113 THEN IMP_RES_TAC NORMAL_FORM_IDENT 1114 THEN ASM_REWRITE_TAC[] 1115 ); 1116 1117 1118(* SUBSTITUTIVE RELATIONS *) 1119 1120 1121val SUBSTITUTIVE = 1122 new_definition 1123 ("SUBSTITUTIVE", 1124 ���SUBSTITUTIVE R = 1125 (!(M:^term) (N:^term) L x. 1126 R M N ==> R (M <[ [x,L]) (N <[ [x,L]))���); 1127 1128 1129val RED1_SUBSTITUTIVE_LEMMA = TAC_PROOF(([], 1130 ���!R (M:^term) N. 1131 RED1 R M N ==> 1132 ((!M N L x. R M N ==> R (M <[ [x,L]) (N <[ [x,L])) ==> 1133 (!L x. RED1 R (M <[ [x,L]) (N <[ [x,L])))���), 1134 rule_induct RED1_height_strong_ind (* strong, not weak induction *) 1135 THEN REPEAT STRIP_TAC (* 4 subgoals *) 1136 THENL 1137 [ RES_TAC 1138 THEN MATCH_MP_TAC RED1_R 1139 THEN ASM_REWRITE_TAC[], 1140 1141 RES_TAC 1142 THEN REWRITE_TAC[SUB_term] 1143 THEN MATCH_MP_TAC RED1_App1 1144 THEN ASM_REWRITE_TAC[], 1145 1146 RES_TAC 1147 THEN REWRITE_TAC[SUB_term] 1148 THEN MATCH_MP_TAC RED1_App2 1149 THEN ASM_REWRITE_TAC[], 1150 1151 SIMPLE_SUBST_TAC 1152 THEN MATCH_MP_TAC RED1_Lam 1153 THEN FIRST_ASSUM 1154 (MATCH_MP_TAC o 1155 REWRITE_RULE[AND_IMP_INTRO] o 1156 CONV_RULE (TOP_DEPTH_CONV RIGHT_IMP_FORALL_CONV)) 1157 THEN ASM_REWRITE_TAC[] 1158 THEN POP_ASSUM (REWRITE_THM o SYM o CONJUNCT1 o 1159 REWRITE_RULE[Lam_one_one]) 1160 THEN POP_ASSUM (REWRITE_THM o SYM o CONJUNCT1 o 1161 REWRITE_RULE[Lam_one_one]) 1162 THEN FIRST_ASSUM 1163 (MATCH_MP_TAC o 1164 REWRITE_RULE[AND_IMP_INTRO] o 1165 CONV_RULE (TOP_DEPTH_CONV RIGHT_IMP_FORALL_CONV)) 1166 THEN ASM_REWRITE_TAC[] 1167 ] 1168 ); 1169 1170 1171val RED1_SUBSTITUTIVE = store_thm 1172 ("RED1_SUBSTITUTIVE", 1173 ���!R:^term_rel. SUBSTITUTIVE R ==> 1174 SUBSTITUTIVE (RED1 R)���, 1175 REWRITE_TAC[SUBSTITUTIVE] 1176 THEN REPEAT STRIP_TAC 1177 THEN IMP_RES_TAC RED1_SUBSTITUTIVE_LEMMA 1178 THEN ASM_REWRITE_TAC[] 1179 ); 1180 1181 1182 1183val RED1_SUBSTITUTIVE_ind_thm_LEMMA = store_thm 1184 ("RED1_SUBSTITUTIVE_ind_thm_LEMMA", 1185 ���!n P_0. 1186 (!R (t1:^term) t2. 1187 SUBSTITUTIVE R /\ 1188 R t1 t2 ==> P_0 R t1 t2) /\ 1189 (!R t1 u t2. 1190 SUBSTITUTIVE R /\ 1191 P_0 R t1 t2 ==> P_0 R (App t1 u) (App t2 u)) /\ 1192 (!R t u1 u2. 1193 SUBSTITUTIVE R /\ 1194 P_0 R u1 u2 ==> P_0 R (App t u1) (App t u2)) /\ 1195 (!R x t1 t2. SUBSTITUTIVE R /\ 1196 (!z. P_0 R (t1 <[ [x,Var z]) (t2 <[ [x,Var z])) 1197 ==> P_0 R (Lam x t1) (Lam x t2)) ==> 1198 (!R t1 t2. RED1 R t1 t2 ==> 1199 (SUBSTITUTIVE R /\ 1200 (HEIGHT t1 <= n) /\ 1201 (HEIGHT t2 <= n) ==> 1202 P_0 R t1 t2))���, 1203 INDUCT_TAC 1204 THEN REPEAT GEN_TAC 1205 THEN STRIP_TAC 1206 THENL 1207 [ REWRITE_TAC[HEIGHT_LESS_EQ_ZERO] 1208 THEN REPEAT STRIP_TAC 1209 THEN ASM_REWRITE_TAC[] 1210 THEN FIRST_ASSUM MATCH_MP_TAC 1211 THEN UNDISCH_TAC ���RED1 R (t1:^term) t2��� 1212 THEN ONCE_REWRITE_TAC RED1_inv_thms 1213 THEN ASM_REWRITE_TAC[term_distinct], 1214 1215 UNDISCH_ALL_TAC 1216 THEN DISCH_THEN ((fn th => REPEAT DISCH_TAC 1217 THEN ASSUME_TAC th) o SPEC_ALL) 1218 THEN POP_ASSUM MP_TAC 1219 THEN ASM_REWRITE_TAC[] 1220 THEN DISCH_THEN (fn th => UNDISCH_ALL_TAC THEN STRIP_ASSUME_TAC th) 1221 THEN REPEAT DISCH_TAC 1222 THEN rule_induct RED1_strong_ind 1223 THEN REWRITE_TAC[HEIGHT] 1224 THEN REWRITE_TAC[MAX_SUC,MAX_LESS_EQ,LESS_EQ_MONO,ZERO_LESS_EQ] 1225 THEN REPEAT STRIP_TAC 1226 THEN ASM_REWRITE_TAC[] 1227 THENL (* 4 subgoals *) 1228 [ FIRST_ASSUM MATCH_MP_TAC 1229 THEN ASM_REWRITE_TAC[], 1230 1231 FIRST_ASSUM MATCH_MP_TAC 1232 THEN ASM_REWRITE_TAC[] 1233 THEN FIRST_ASSUM MATCH_MP_TAC 1234 THEN IMP_RES_TAC LESS_EQ_IMP_LESS_SUC 1235 THEN IMP_RES_TAC LESS_IMP_LESS_OR_EQ 1236 THEN ASM_REWRITE_TAC[], 1237 1238 FIRST_ASSUM MATCH_MP_TAC 1239 THEN ASM_REWRITE_TAC[] 1240 THEN FIRST_ASSUM MATCH_MP_TAC 1241 THEN IMP_RES_TAC LESS_EQ_IMP_LESS_SUC 1242 THEN IMP_RES_TAC LESS_IMP_LESS_OR_EQ 1243 THEN ASM_REWRITE_TAC[], 1244 1245 FIRST_ASSUM MATCH_MP_TAC 1246 THEN ASM_REWRITE_TAC[] 1247 THEN REWRITE_TAC[SUBSTITUTIVE] 1248 THEN REPEAT STRIP_TAC 1249 THEN ASSUM_LIST 1250 (MATCH_MP_TAC o REWRITE_RULE[AND_IMP_INTRO] o hd o rev) 1251 THEN ASM_REWRITE_TAC[HEIGHT_SUB_VAR] 1252 THEN IMP_RES_TAC RED1_SUBSTITUTIVE 1253 THEN REWRITE_ALL_TAC[SUBSTITUTIVE] 1254 THEN FIRST_ASSUM MATCH_MP_TAC 1255 THEN ASM_REWRITE_TAC[] 1256 ] 1257 ] 1258 ); 1259 1260val RED1_SUBSTITUTIVE_ind_thm_LEMMA1 = store_thm 1261 ("RED1_SUBSTITUTIVE_ind_thm_LEMMA1", 1262 ���!P_0. 1263 (!R (t1:^term) t2. SUBSTITUTIVE R /\ R t1 t2 ==> P_0 R t1 t2) /\ 1264 (!R t1 u t2. 1265 SUBSTITUTIVE R /\ P_0 R t1 t2 ==> P_0 R (App t1 u) (App t2 u)) /\ 1266 (!R t u1 u2. 1267 SUBSTITUTIVE R /\ P_0 R u1 u2 ==> P_0 R (App t u1) (App t u2)) /\ 1268 (!R x t1 t2. 1269 SUBSTITUTIVE R /\ 1270 (!z. P_0 R (t1 <[ [(x,Var z)]) (t2 <[ [(x,Var z)])) ==> 1271 P_0 R (Lam x t1) (Lam x t2)) ==> 1272 (!R t1 t2. 1273 RED1 R t1 t2 ==> 1274 SUBSTITUTIVE R ==> 1275 P_0 R t1 t2)���, 1276 REPEAT STRIP_TAC 1277 THEN MP_TAC (SPEC_ALL 1278 (SPEC ���(HEIGHT (t1:^term)) MAX (HEIGHT (t2:^term))��� 1279 RED1_SUBSTITUTIVE_ind_thm_LEMMA)) 1280 THEN ASM_REWRITE_TAC[AND_IMP_INTRO] 1281 THEN REPEAT STRIP_TAC 1282 THEN FIRST_ASSUM MATCH_MP_TAC 1283 THEN ASM_REWRITE_TAC[LESS_EQ_MAX] 1284 ); 1285 1286 1287val RED1_SUBSTITUTIVE_ind_thm = store_thm 1288 ("RED1_SUBSTITUTIVE_ind_thm", 1289 ���!R. SUBSTITUTIVE R ==> 1290 !P_0. 1291 (!R (t1:^term) t2. R t1 t2 ==> P_0 R t1 t2) /\ 1292 (!R t1 u t2. 1293 P_0 R t1 t2 ==> P_0 R (App t1 u) (App t2 u)) /\ 1294 (!R t u1 u2. 1295 P_0 R u1 u2 ==> P_0 R (App t u1) (App t u2)) /\ 1296 (!R x t1 t2. SUBSTITUTIVE R /\ 1297 (!z. P_0 R (t1 <[ [x,Var z]) (t2 <[ [x,Var z])) 1298 ==> P_0 R (Lam x t1) (Lam x t2)) ==> 1299 (!t1 t2. RED1 R t1 t2 ==> P_0 R t1 t2)���, 1300 GEN_TAC 1301 THEN DISCH_TAC 1302 THEN REPEAT GEN_TAC 1303 THEN STRIP_TAC 1304 THEN UNDISCH_TAC ���SUBSTITUTIVE (R:^term_rel)��� 1305 THEN CONV_TAC (TOP_DEPTH_CONV RIGHT_IMP_FORALL_CONV) 1306 THEN REWRITE_TAC[AND_IMP_INTRO] 1307 THEN ONCE_REWRITE_TAC[ISPEC ���SUBSTITUTIVE (R:^term_rel)��� CONJ_SYM] 1308 THEN REWRITE_TAC[GSYM AND_IMP_INTRO] 1309 THEN SPEC_TAC (���R:^term_rel���,���R:^term_rel���) 1310 THEN MATCH_MP_TAC RED1_SUBSTITUTIVE_ind_thm_LEMMA1 1311 THEN REPEAT STRIP_TAC 1312 THEN FIRST_ASSUM MATCH_MP_TAC 1313 THEN ASM_REWRITE_TAC[] 1314 ); 1315 1316 1317 1318val RED_SUBSTITUTIVE_LEMMA = TAC_PROOF(([], 1319 ���!R (M:^term) N. 1320 RED R M N ==> 1321 (SUBSTITUTIVE R ==> 1322 (!L x. RED R (M <[ [x,L]) (N <[ [x,L])))���), 1323 rule_induct RED_ind_thm (* weak, not strong induction *) 1324 THEN REPEAT STRIP_TAC (* 3 subgoals *) 1325 THENL 1326 [ IMP_RES_TAC RED1_SUBSTITUTIVE 1327 THEN REWRITE_ALL_TAC[SUBSTITUTIVE] 1328 THEN RES_TAC 1329 THEN RULE_ASSUM_TAC SPEC_ALL 1330 THEN IMP_RES_TAC RED_RED1, 1331 1332 REWRITE_TAC[RED_REFL], 1333 1334 RES_TAC 1335 THEN RULE_ASSUM_TAC SPEC_ALL 1336 THEN IMP_RES_TAC RED_TRANS 1337 ] 1338 ); 1339 1340 1341val RED_SUBSTITUTIVE = store_thm 1342 ("RED_SUBSTITUTIVE", 1343 ���!R:^term_rel. 1344 SUBSTITUTIVE R ==> 1345 SUBSTITUTIVE (RED R)���, 1346 GEN_TAC THEN DISCH_TAC 1347 THEN REWRITE_TAC[SUBSTITUTIVE] 1348 THEN REPEAT STRIP_TAC 1349 THEN IMP_RES_TAC RED_SUBSTITUTIVE_LEMMA 1350 THEN ASM_REWRITE_TAC[] 1351 ); 1352 1353 1354 1355val REQUAL_SUBSTITUTIVE_LEMMA = TAC_PROOF(([], 1356 ���!R (M:^term) N. 1357 REQUAL R M N ==> 1358 (SUBSTITUTIVE R ==> 1359 (!L x. REQUAL R (M <[ [x,L]) (N <[ [x,L])))���), 1360 rule_induct REQUAL_ind_thm (* weak, not strong induction *) 1361 THEN REPEAT STRIP_TAC (* 3 subgoals *) 1362 THENL 1363 [ IMP_RES_TAC RED_SUBSTITUTIVE 1364 THEN REWRITE_ALL_TAC[SUBSTITUTIVE] 1365 THEN RES_TAC 1366 THEN RULE_ASSUM_TAC SPEC_ALL 1367 THEN IMP_RES_TAC REQUAL_RED, 1368 1369 RES_TAC 1370 THEN RULE_ASSUM_TAC SPEC_ALL 1371 THEN IMP_RES_TAC REQUAL_SYM, 1372 1373 RES_TAC 1374 THEN RULE_ASSUM_TAC SPEC_ALL 1375 THEN IMP_RES_TAC REQUAL_TRANS 1376 ] 1377 ); 1378 1379 1380val REQUAL_SUBSTITUTIVE = store_thm 1381 ("REQUAL_SUBSTITUTIVE", 1382 ���!R:^term_rel. 1383 SUBSTITUTIVE R ==> 1384 SUBSTITUTIVE (REQUAL R)���, 1385 GEN_TAC THEN DISCH_TAC 1386 THEN REWRITE_TAC[SUBSTITUTIVE] 1387 THEN REPEAT STRIP_TAC 1388 THEN IMP_RES_TAC REQUAL_SUBSTITUTIVE_LEMMA 1389 THEN ASM_REWRITE_TAC[] 1390 ); 1391 1392 1393 1394 1395val _ = export_theory(); 1396 1397val _ = print_theory_to_file "-" "reduction.lst"; 1398 1399val _ = html_theory "reduction"; 1400 1401val _ = print_theory_size(); 1402