1open HolKernel Parse boolLib; 2infix THEN THENL THENC ORELSE ORELSEC THEN_TCL ORELSE_TCL ## |->; 3infixr -->; 4 5 6 7val _ = new_theory "beta"; 8 9 10(* In interactive sessions, do: 11 12app load ["barendregt", "tactics" 13 ]; 14 15*) 16 17open prim_recTheory pairTheory listTheory rich_listTheory; 18open combinTheory; 19(* open listLib; *) 20open more_listTheory; 21open pred_setTheory pred_setLib; 22open numTheory; 23open numLib; 24open arithmeticTheory; 25open bossLib; 26open relationTheory; 27open Mutual; 28open ind_rel; 29open dep_rewrite; 30open quotient; 31open more_setTheory; 32open variableTheory; 33open termTheory; 34open alphaTheory; 35open liftTheory; 36open barendregt; 37open reductionTheory; 38 39 40open tactics; 41 42 43val term = ty_antiq ( ==`:'a term`== ); 44val subs = ty_antiq ( ==`:(var # 'a term) list`== ); 45val term_rel = ty_antiq ( ==`:'a term -> 'a term -> bool`== ); 46 47 48(* Define the transitive closure of a relation. *) 49(* Wait, it's already done: see file src/relation/relationScript.sml. *) 50(* This defines TC in the logic as TC R is the transitive closure of R, *) 51(* and "transitive R" as the property that R is transitite on 'a. *) 52(* There are also a bunch of theorems in structure TCScript, as well as *) 53(* induction tactics, cases theorems, etc. It's theory "TC". *) 54 55(* copied: *) 56 57val TC_INDUCT_TAC = 58 let val tc_thm = TC_INDUCT 59 fun tac (asl,w) = 60 let open Rsyntax 61 val {Bvar=u,Body} = dest_forall w 62 val {Bvar=v,Body} = dest_forall Body 63 val {ant,conseq} = dest_imp Body 64 val (TC,Ru'v') = strip_comb ant 65 val R = hd Ru'v' 66 val u'v' = tl Ru'v' 67 val u' = hd u'v' 68 val v' = hd (tl u'v') 69 (*val (TC,[R,u',v']) = strip_comb ant*) 70 (*val {Name = "TC",...} = dest_const TC*) 71 val _ = if #Name(dest_const TC) = "TC" then true else raise Match 72 val _ = assert (aconv u) u' 73 val _ = assert (aconv v) v' 74 val P = list_mk_abs([u,v], conseq) 75 val tc_thm' = BETA_RULE(ISPEC P (ISPEC R tc_thm)) 76 in MATCH_MP_TAC tc_thm' (asl,w) 77 end 78 handle _ => raise HOL_ERR{origin_structure = "<top-level>", 79 origin_function = "TC_INDUCT_TAC", 80 message = "Unanticipated term structure"} 81 in tac 82 end; 83 84 85 86(* Barendregt's Lemma 3.2.2: *) 87 88 89val TC_DIAMOND1 = store_thm 90 ("TC_DIAMOND1", 91 ���!R (a:'a) b. TC R a b ==> 92 (DIAMOND R ==> (!c. R a c ==> 93 (?d. R b d /\ TC R c d)))���, 94 GEN_TAC 95 THEN TC_INDUCT_TAC 96 THEN REPEAT STRIP_TAC 97 THENL 98 [ REWRITE_ALL_TAC[DIAMOND] 99 THEN RES_TAC 100 THEN EXISTS_TAC ���d':'a��� 101 THEN IMP_RES_TAC TC_SUBSET 102 THEN ASM_REWRITE_TAC[], 103 104 RES_TAC 105 THEN FIRST_ASSUM (IMP_RES_TAC o SPEC ``d:'a``) 106 THEN EXISTS_TAC ``d':'a`` 107 THEN ASM_REWRITE_TAC[] 108 THEN IMP_RES_TAC (REWRITE_RULE[transitive_def] TC_TRANSITIVE) 109 ] 110 ); 111 112val TC_DIAMOND2 = store_thm 113 ("TC_DIAMOND2", 114 ���!R (a:'a) b. TC R a b ==> 115 (DIAMOND R ==> (!c. TC R a c ==> 116 (?d. TC R b d /\ TC R c d)))���, 117 GEN_TAC 118 THEN TC_INDUCT_TAC 119 THEN REPEAT STRIP_TAC 120 THENL 121 [ IMP_RES_TAC TC_DIAMOND1 122 THEN EXISTS_TAC ���d:'a��� 123 THEN IMP_RES_TAC TC_SUBSET 124 THEN ASM_REWRITE_TAC[], 125 126 RES_TAC 127 THEN FIRST_ASSUM (IMP_RES_TAC o SPEC ``d:'a``) 128 THEN EXISTS_TAC ``d':'a`` 129 THEN ASM_REWRITE_TAC[] 130 THEN IMP_RES_TAC (REWRITE_RULE[transitive_def] TC_TRANSITIVE) 131 ] 132 ); 133 134val TC_DIAMOND = store_thm 135 ("TC_DIAMOND", 136 ���!R:'a->'a->bool. DIAMOND R ==> DIAMOND (TC R)���, 137 REPEAT STRIP_TAC 138 THEN REWRITE_TAC[DIAMOND] 139 THEN REPEAT STRIP_TAC 140 THEN IMP_RES_TAC TC_DIAMOND2 141 THEN EXISTS_TAC ``d'':'a`` 142 THEN ASM_REWRITE_TAC[] 143 ); 144 145 146 147 148(* --------------------------------------------------------------------- *) 149(* Primitive semantics of the lambda-calculus: *) 150(* Barendregt, Definition 3.1.2, page 51 *) 151(* Here we define the primitive reduction operator of the calculus. *) 152(* It corresponds to applying a function to an argument. *) 153(* --------------------------------------------------------------------- *) 154 155 156 157(* --------------------------------------------------------------------- *) 158(* Definition of the relation of beta reduction. *) 159(* This is simple, but we define it by rule induction. *) 160(* --------------------------------------------------------------------- *) 161 162(* --------------------------------------------------------------------- *) 163(* (BETA_R t1 t2) means that the term t1 reduces entirely to the *) 164(* term t2 in exactly one beta-reduction step, as defined in Barendregt, *) 165(* Section 3.1.3, page 51. Note that this is true ONLY on t1 of *) 166(* the form (App (Lam x u) t). *) 167(* --------------------------------------------------------------------- *) 168 169 170val BETA_R = 171���BETA_R : ^term_rel���; 172 173val BETA_R_patterns = [���^BETA_R t1 t2���]; 174 175val BETA_R_rules_tm = 176��� 177 (* -------------------------------------------- *) 178 (^BETA_R (App (Lam x u) t) (u <[ [x,t])) 179���; 180 181val (BETA_R_rules_sat,BETA_R_ind_thm) = 182 define_inductive_relations BETA_R_patterns BETA_R_rules_tm; 183 184val BETA_R_inv_thms = prove_inversion_theorems 185 BETA_R_rules_sat BETA_R_ind_thm; 186 187val BETA_R_strong_ind = prove_strong_induction 188 BETA_R_rules_sat BETA_R_ind_thm; 189 190val _ = save_thm ("BETA_R_rules_sat", BETA_R_rules_sat); 191val _ = save_thm ("BETA_R_ind_thm", BETA_R_ind_thm); 192val _ = save_thm ("BETA_R_inv_thms", LIST_CONJ BETA_R_inv_thms); 193val _ = save_thm ("BETA_R_strong_ind", BETA_R_strong_ind); 194 195 196 197 198(* --------------------------------------------------------------------- *) 199(* We claim that BETA_R is a binary relation on the lambda calculus *) 200(* language which is *) 201(* 1) a notion of reduction on the sigma calculus, in the sense of *) 202(* Berendregt, Definition 3.1.2, pg 51 (trivial, since a relation) *) 203(* 2) deterministic *) 204(* --------------------------------------------------------------------- *) 205 206 207(* BETA_R is a deterministic relation. *) 208 209val SUB_RENAME_SUB = store_thm 210 ("SUB_RENAME_SUB", 211 ���!a:^term x y t. ((a <[ [(x,Var y)]) <[ [(y,Var x)] = a) ==> 212 (((a <[ [(x,Var y)]) <[ [y,t]) = (a <[ [x,t]))���, 213 MUTUAL_INDUCT_THEN term_height_induct ASSUME_TAC 214 THEN REPEAT GEN_TAC 215 THENL 216 [ (* Con case *) 217 REWRITE_TAC[SUB_term], 218 219 (* Var case *) 220 REWRITE_TAC[SUB_term,SUB] 221 THEN COND_CASES_TAC 222 THEN REWRITE_TAC[SUB_term,SUB] 223 THEN COND_CASES_TAC 224 THEN REWRITE_TAC[term_one_one] 225 THEN DISCH_THEN (ASSUME_TAC o SYM) 226 THEN RES_TAC, 227 228 (* App case *) 229 REWRITE_TAC[SUB_term] 230 THEN REWRITE_TAC[term_one_one] 231 THEN STRIP_TAC 232 THEN RES_TAC 233 THEN ASM_REWRITE_TAC[], 234 235 (* Lam case *) 236 SIMPLE_SUBST_TAC 237 THEN REWRITE_TAC[Lam_one_one] 238 THEN REWRITE_TAC[subst_SAME_ONE] 239 THEN STRIP_TAC 240 THEN POP_TAC 241 THEN RES_TAC 242 THEN ASM_REWRITE_TAC[] 243 ] 244 ); 245 246val SUB_RENAME_TERM = store_thm 247 ("SUB_RENAME_TERM", 248 ���!a:^term b x y t. (Lam x a = Lam y b) ==> 249 ((a <[ [x,t]) = (b <[ [y,t]))���, 250 REWRITE_TAC[Lam_one_one] 251 THEN REPEAT STRIP_TAC 252 THEN FIRST_ASSUM (REWRITE_THM o SYM) 253 THEN MATCH_MP_TAC SUB_RENAME_SUB 254 THEN ASM_REWRITE_TAC[] 255 ); 256 257val BETA_R_deterministic = store_thm 258 ("BETA_R_deterministic", 259 ���!t1:^term t2. 260 BETA_R t1 t2 ==> !t3. BETA_R t1 t3 ==> (t2 = t3)���, 261 rule_induct BETA_R_strong_ind 262 THEN REPEAT GEN_TAC 263 THEN REWRITE_TAC BETA_R_inv_thms 264 THEN REWRITE_TAC[term_one_one] 265 THEN STRIP_TAC 266 THEN IMP_RES_TAC SUB_RENAME_TERM 267 THEN ASM_REWRITE_TAC[] 268 ); 269 270(* Note that BETA_R is not reflexive, symmetric, or transitive. *) 271 272val FV_SUB = store_thm 273 ("FV_SUB", 274 ���!u:^term x t. FV (u <[ [(x,t)]) SUBSET FV u DIFF {x} UNION FV t���, 275 MUTUAL_INDUCT_THEN term_height_induct ASSUME_TAC 276 THEN REPEAT GEN_TAC 277 THENL 278 [ (* Con case *) 279 REWRITE_TAC[SUB_term,FV_term] 280 THEN REWRITE_TAC[EMPTY_SUBSET], 281 282 (* Var case *) 283 REWRITE_TAC[SUB_term,SUB] 284 THEN COND_CASES_TAC 285 THEN REWRITE_TAC[SUBSET_UNION] 286 THEN REWRITE_TAC[SUBSET_DEF] 287 THEN REWRITE_TAC[FV_term,IN_UNION,IN] 288 THEN REPEAT STRIP_TAC 289 THEN DISJ1_TAC 290 THEN POP_ASSUM REWRITE_THM 291 THEN DEP_REWRITE_TAC[IN_DIFF] 292 THEN ASM_REWRITE_TAC[IN], 293 294 (* App case *) 295 REWRITE_TAC[SUB_term,FV_term] 296 THEN REWRITE_TAC[UNION_DIFF,UNION_SUBSET] 297 THEN REWRITE_ALL_TAC[SUBSET_DEF,IN_UNION] 298 THEN REPEAT STRIP_TAC 299 THEN RES_TAC 300 THEN ASM_REWRITE_TAC[], 301 302 (* Lam case *) 303 SIMPLE_SUBST_TAC 304 THEN REWRITE_TAC[FV_term] 305 THEN POP_TAC 306 THEN POP_TAC 307 THEN UNDISCH_LAST_TAC 308 THEN REWRITE_TAC[SUBSET_DEF,IN_UNION,IN_DIFF,IN] 309 THEN REPEAT STRIP_TAC 310 THEN RES_TAC(* 2 subgoals *) 311 THEN ASM_REWRITE_TAC[] 312 ] 313 ); 314 315val BETA_FV = store_thm 316 ("BETA_FV", 317 ���!t1:^term t2. BETA_R t1 t2 ==> 318 (FV t2 SUBSET FV t1)���, 319 rule_induct BETA_R_strong_ind 320 THEN REWRITE_TAC[FV_term] 321 THEN REWRITE_TAC[FV_SUB] 322 ); 323 324 325val BETA_R_equals = store_thm 326 ("BETA_R_equals", 327 ���(!a t:^term. BETA_R (Con a) t = F) /\ 328 (!x t:^term. BETA_R (Var x) t = F) /\ 329 (!t u t':^term. BETA_R (App t u) t' = 330 (?x u'. (t = Lam x u') /\ (t' = u' <[ [x,u]))) /\ 331 (!x u t:^term. BETA_R (Lam x u) t = F)���, 332 REWRITE_TAC BETA_R_inv_thms 333 THEN REWRITE_TAC[term_distinct,term_one_one] 334 THEN REPEAT STRIP_TAC 335 THEN EQ_TAC 336 THEN STRIP_TAC 337 THENL 338 [ EXISTS_TAC ���x:var��� 339 THEN EXISTS_TAC ���u':^term��� 340 THEN ASM_REWRITE_TAC[], 341 342 EXISTS_TAC ���x:var��� 343 THEN EXISTS_TAC ���u':^term��� 344 THEN EXISTS_TAC ���u:^term��� 345 THEN ASM_REWRITE_TAC[] 346 ] 347 ); 348 349 350(* --------------------------------------------------------------------- *) 351(* Now we claim that using the results of theory "reduction", that *) 352(* 1) RED1 BETA_R, RED BETA_R, and REQ BETA_R are compatible, *) 353(* 2) RED BETA_R is a reduction relation, *) 354(* 3) REQ BETA_R is an equality relation, *) 355(* 4) various theorems and relations hold (see the theory "reduction") *) 356(* --------------------------------------------------------------------- *) 357 358 359(* --------------------------------------------------------------------- *) 360(* Now we begin to prove the Church-Rosser theorem for BETA_R. *) 361(* --------------------------------------------------------------------- *) 362 363 364(* Barendregt Proposition 3.1.16, BETA_R is substitutive. *) 365 366val BETA_R_SUBSTITUTIVE = store_thm 367 ("BETA_R_SUBSTITUTIVE", 368 ���SUBSTITUTIVE (BETA_R:^term_rel)���, 369 REWRITE_TAC[SUBSTITUTIVE] 370 THEN REPEAT GEN_TAC 371 THEN DISCH_THEN (STRIP_ASSUME_TAC o REWRITE_RULE BETA_R_inv_thms) 372 THEN ASM_REWRITE_TAC[] 373 THEN ONCE_REWRITE_TAC[SUB_term] 374 THEN SIMPLE_SUBST_TAC 375 THEN IMP_RES_THEN REWRITE_THM SUB_RENAME_TERM 376 THEN REWRITE_TAC BETA_R_inv_thms 377 THEN REWRITE_TAC[term_one_one] 378 THEN EXISTS_TAC ���z:var��� 379 THEN EXISTS_TAC ���(u':^term) <[ [x,L]��� 380 THEN EXISTS_TAC ���(t:^term) <[ [x,L]��� 381 THEN REWRITE_TAC[] 382 THEN MATCH_MP_TAC BARENDREGT_SUBSTITUTION_LEMMA 383 THEN ASM_REWRITE_TAC[] 384 ); 385 386 387 388 389 390(* --------------------------------------------------------------------- *) 391(* (REDL o1 o2) will now be defined on the sigma calculus such that *) 392(* 1) REDL satisfies the diamond property, and *) 393(* 2) the transitive closure of REDL is RED BETA_R. *) 394(* Then it follows by TC_DIAMOND that RED BETA_R satifies the diamond *) 395(* property, i.e., that BETA_R is Church-Rosser. *) 396(* --------------------------------------------------------------------- *) 397 398 399val REDL = 400���REDL : ^term_rel���; 401 402val REDL_patterns = [���^REDL t1 t2���]; 403 404val REDL_rules_tm = 405��� 406 407 (* -------------------------------------------- *) 408 (^REDL t t) /\ 409 410 411 ((^REDL t1 t2) 412 (* -------------------------------------------- *) ==> 413 (^REDL (Lam x t1) (Lam x t2))) /\ 414 415 416 ((^REDL t1 t2) /\ (^REDL u1 u2) 417 (* -------------------------------------------- *) ==> 418 (^REDL (App t1 u1) (App t2 u2))) /\ 419 420 421 ((^REDL t1 t2) /\ (^REDL u1 u2) 422 (* -------------------------------------------- *) ==> 423 (^REDL (App (Lam x t1) u1) (t2 <[ [x,u2]))) 424���; 425 426val (REDL_rules_sat,REDL_ind_thm) = 427 define_inductive_relations REDL_patterns REDL_rules_tm; 428 429val REDL_inv_thms = prove_inversion_theorems 430 REDL_rules_sat REDL_ind_thm; 431 432val REDL_strong_ind = prove_strong_induction 433 REDL_rules_sat REDL_ind_thm; 434 435val _ = save_thm ("REDL_rules_sat", REDL_rules_sat); 436val _ = save_thm ("REDL_ind_thm", REDL_ind_thm); 437val _ = save_thm ("REDL_inv_thms", LIST_CONJ REDL_inv_thms); 438val _ = save_thm ("REDL_strong_ind", REDL_strong_ind); 439 440 441val [REDL_REFL, REDL_Lam, REDL_App, REDL_BETA] 442 = CONJUNCTS REDL_rules_sat; 443 444 445 446 447val REDL_height_ind_thm_LEMMA = store_thm 448 ("REDL_height_ind_thm_LEMMA", 449 ���!n P_0:^term_rel. 450 (!t. P_0 t t) /\ 451 (!x t1 t2. P_0 t1 t2 ==> P_0 (Lam x t1) (Lam x t2)) /\ 452 (!t1 u1 t2 u2. 453 P_0 t1 t2 /\ P_0 u1 u2 ==> 454 P_0 (App t1 u1) (App t2 u2)) /\ 455 (!x t1 u1 t2 u2. 456 (!t1' t2'. REDL t1' t2' /\ 457 (HEIGHT t1 = HEIGHT t1') ==> P_0 t1' t2') /\ 458 P_0 u1 u2 ==> 459 P_0 (App (Lam x t1) u1) (t2 <[ [x,u2])) /\ 460 (!x t1 t2. 461 (!t1' t2'. REDL t1' t2' /\ 462 (HEIGHT t1 = HEIGHT t1') ==> P_0 t1' t2') 463 ==> P_0 (Lam x t1) (Lam x t2)) ==> 464 (!t1 t2. REDL t1 t2 ==> 465 ((HEIGHT t1 <= n) ==> 466 P_0 t1 t2))���, 467 INDUCT_TAC 468 THEN REPEAT GEN_TAC 469 THEN STRIP_TAC 470 THENL 471 [ REWRITE_TAC[HEIGHT_LESS_EQ_ZERO] 472 THEN REPEAT STRIP_TAC 473 THEN ASM_REWRITE_TAC[] 474 THEN UNDISCH_TAC ���REDL (t1:^term) t2��� 475 THEN ONCE_REWRITE_TAC REDL_inv_thms 476 THEN ASM_REWRITE_TAC[term_distinct,term_one_one] 477 THEN DISCH_TAC 478 THEN ASM_REWRITE_TAC[], 479 480 UNDISCH_ALL_TAC 481 THEN DISCH_THEN ((fn th => REPEAT DISCH_TAC 482 THEN ASSUME_TAC th) o SPEC_ALL) 483 THEN POP_ASSUM MP_TAC 484 THEN ASM_REWRITE_TAC[] 485 THEN DISCH_THEN (fn th => UNDISCH_ALL_TAC THEN STRIP_ASSUME_TAC th) 486 THEN REPEAT DISCH_TAC 487 THEN rule_induct REDL_ind_thm 488 THEN REWRITE_TAC[HEIGHT] 489 THEN REWRITE_TAC[MAX_SUC,MAX_LESS_EQ,LESS_EQ_MONO,ZERO_LESS_EQ] 490 THEN REPEAT STRIP_TAC 491 THEN ASM_REWRITE_TAC[] 492 THENL (* 3 subgoals *) 493 [ FIRST_ASSUM MATCH_MP_TAC 494 THEN REPEAT STRIP_TAC 495 THEN ASSUM_LIST 496 (MATCH_MP_TAC o REWRITE_RULE[AND_IMP_INTRO] o hd o rev) 497 THEN POP_ASSUM (REWRITE_THM o SYM) 498 THEN ASM_REWRITE_TAC[], 499 500 FIRST_ASSUM MATCH_MP_TAC 501 THEN CONJ_TAC 502 THEN FIRST_ASSUM MATCH_MP_TAC 503 THEN IMP_RES_TAC LESS_EQ_IMP_LESS_SUC 504 THEN IMP_RES_TAC LESS_IMP_LESS_OR_EQ, 505 506 FIRST_ASSUM MATCH_MP_TAC 507 THEN CONJ_TAC 508 THENL 509 [ REPEAT STRIP_TAC 510 THEN ASSUM_LIST 511 (MATCH_MP_TAC o REWRITE_RULE[AND_IMP_INTRO] o hd o rev) 512 THEN POP_ASSUM (REWRITE_THM o SYM) 513 THEN IMP_RES_TAC LESS_EQ_IMP_LESS_SUC 514 THEN IMP_RES_TAC LESS_MONO_EQ 515 THEN IMP_RES_TAC LESS_IMP_LESS_OR_EQ 516 THEN ASM_REWRITE_TAC[], 517 518 FIRST_ASSUM MATCH_MP_TAC 519 THEN IMP_RES_TAC LESS_EQ_IMP_LESS_SUC 520 THEN IMP_RES_TAC LESS_IMP_LESS_OR_EQ 521 ] 522 ] 523 ] 524 ); 525 526val REDL_height_ind_thm = store_thm 527 ("REDL_height_ind_thm", 528 ���!P_0:^term_rel. 529 (!t. P_0 t t) /\ 530 (!x t1 t2. P_0 t1 t2 ==> P_0 (Lam x t1) (Lam x t2)) /\ 531 (!t1 u1 t2 u2. 532 P_0 t1 t2 /\ P_0 u1 u2 ==> P_0 (App t1 u1) (App t2 u2)) /\ 533 (!x t1 u1 t2 u2. 534 (!t1' t2'. 535 REDL t1' t2' /\ (HEIGHT t1 = HEIGHT t1') ==> P_0 t1' t2') /\ 536 P_0 u1 u2 ==> 537 P_0 (App (Lam x t1) u1) (t2 <[ [(x,u2)])) /\ 538 (!x t1 t2. 539 (!t1' t2'. 540 REDL t1' t2' /\ (HEIGHT t1 = HEIGHT t1') ==> P_0 t1' t2') ==> 541 P_0 (Lam x t1) (Lam x t2)) ==> 542 !t1 t2. REDL t1 t2 ==> P_0 t1 t2���, 543 REPEAT STRIP_TAC 544 THEN MP_TAC (SPEC_ALL 545 (SPEC ���HEIGHT (t1:^term)��� REDL_height_ind_thm_LEMMA)) 546 THEN ASM_REWRITE_TAC[AND_IMP_INTRO] 547 THEN REPEAT STRIP_TAC 548 THEN FIRST_ASSUM MATCH_MP_TAC 549 THEN ASM_REWRITE_TAC[LESS_EQ_REFL] 550 ); 551 552val REDL_height_strong_ind_LEMMA = store_thm 553 ("REDL_height_strong_ind_LEMMA", 554 ���!n P_0:^term_rel. 555 (!t. P_0 t t) /\ 556 (!t1 u1 t2 u2. 557 P_0 t1 t2 /\ REDL t1 t2 /\ P_0 u1 u2 /\ REDL u1 u2 ==> 558 P_0 (App t1 u1) (App t2 u2)) /\ 559 (!x t1 u1 t2 u2. 560 (!t1' t2'. 561 REDL t1' t2' /\ (HEIGHT t1 = HEIGHT t1') ==> 562 P_0 t1' t2') /\ REDL t1 t2 /\ 563 P_0 u1 u2 /\ REDL u1 u2 ==> 564 P_0 (App (Lam x t1) u1) (t2 <[ [(x,u2)])) /\ 565 (!x t1 t2. 566 (!t1' t2'. 567 REDL t1' t2' /\ (HEIGHT t1 = HEIGHT t1') ==> 568 P_0 t1' t2') /\ REDL t1 t2 ==> 569 P_0 (Lam x t1) (Lam x t2)) ==> 570 !t1 t2. REDL t1 t2 ==> HEIGHT t1 <= n ==> P_0 t1 t2 571 ���, 572 INDUCT_TAC 573 THEN REPEAT GEN_TAC 574 THEN STRIP_TAC 575 THENL 576 [ REWRITE_TAC[HEIGHT_LESS_EQ_ZERO] 577 THEN REPEAT STRIP_TAC 578 THEN ASM_REWRITE_TAC[] 579 THEN UNDISCH_TAC ���REDL (t1:^term) t2��� 580 THEN ONCE_REWRITE_TAC REDL_inv_thms 581 THEN ASM_REWRITE_TAC[term_distinct] 582 THEN DISCH_TAC 583 THEN ASM_REWRITE_TAC[], 584 585 UNDISCH_ALL_TAC 586 THEN DISCH_THEN ((fn th => REPEAT DISCH_TAC 587 THEN ASSUME_TAC th) o SPEC_ALL) 588 THEN POP_ASSUM MP_TAC 589 THEN ASM_REWRITE_TAC[] 590 THEN DISCH_THEN (fn th => UNDISCH_ALL_TAC THEN STRIP_ASSUME_TAC th) 591 THEN REPEAT DISCH_TAC 592 THEN rule_induct REDL_strong_ind 593 THEN REWRITE_TAC[HEIGHT] 594 THEN REWRITE_TAC[MAX_SUC,MAX_LESS_EQ,LESS_EQ_MONO,ZERO_LESS_EQ] 595 THEN REPEAT STRIP_TAC 596 THEN ASM_REWRITE_TAC[] 597 THENL (* 3 subgoals *) 598 [ FIRST_ASSUM MATCH_MP_TAC 599 THEN ASM_REWRITE_TAC[] 600 THEN REPEAT STRIP_TAC 601 THEN ASSUM_LIST 602 (MATCH_MP_TAC o REWRITE_RULE[AND_IMP_INTRO] o hd o rev) 603 THEN POP_ASSUM (REWRITE_THM o SYM) 604 THEN ASM_REWRITE_TAC[], 605 606 FIRST_ASSUM MATCH_MP_TAC 607 THEN ASM_REWRITE_TAC[] 608 THEN CONJ_TAC 609 THEN FIRST_ASSUM MATCH_MP_TAC 610 THEN IMP_RES_TAC LESS_EQ_IMP_LESS_SUC 611 THEN IMP_RES_TAC LESS_IMP_LESS_OR_EQ, 612 613 FIRST_ASSUM MATCH_MP_TAC 614 THEN ASM_REWRITE_TAC[] 615 THEN REPEAT STRIP_TAC 616 THENL 617 [ ASSUM_LIST 618 (MATCH_MP_TAC o REWRITE_RULE[AND_IMP_INTRO] o hd o rev) 619 THEN ASM_REWRITE_TAC[] 620 THEN POP_ASSUM (REWRITE_THM o SYM) 621 THEN IMP_RES_TAC LESS_EQ_IMP_LESS_SUC 622 THEN IMP_RES_TAC LESS_MONO_EQ 623 THEN IMP_RES_TAC LESS_IMP_LESS_OR_EQ, 624 625 FIRST_ASSUM MATCH_MP_TAC 626 THEN IMP_RES_TAC LESS_EQ_IMP_LESS_SUC 627 THEN IMP_RES_TAC LESS_IMP_LESS_OR_EQ 628 ] 629 ] 630 ] 631 ); 632 633val REDL_height_strong_ind = store_thm 634 ("REDL_height_strong_ind", 635 ���!P_0. 636 (!t:^term. P_0 t t) /\ 637 (!t1 u1 t2 u2. 638 P_0 t1 t2 /\ REDL t1 t2 /\ P_0 u1 u2 /\ REDL u1 u2 ==> 639 P_0 (App t1 u1) (App t2 u2)) /\ 640 (!x t1 u1 t2 u2. 641 (!t1' t2'. 642 REDL t1' t2' /\ (HEIGHT t1 = HEIGHT t1') ==> 643 P_0 t1' t2') /\ REDL t1 t2 /\ 644 P_0 u1 u2 /\ REDL u1 u2 ==> 645 P_0 (App (Lam x t1) u1) (t2 <[ [(x,u2)])) /\ 646 (!x t1 t2. 647 (!t1' t2'. 648 REDL t1' t2' /\ (HEIGHT t1 = HEIGHT t1') ==> 649 P_0 t1' t2') /\ REDL t1 t2 ==> 650 P_0 (Lam x t1) (Lam x t2)) ==> 651 !t1 t2. REDL t1 t2 ==> P_0 t1 t2���, 652 REPEAT STRIP_TAC 653 THEN MP_TAC (SPEC_ALL (SPEC ���HEIGHT (t1:^term)��� 654 REDL_height_strong_ind_LEMMA)) 655 THEN ASM_REWRITE_TAC[AND_IMP_INTRO] 656 THEN REPEAT STRIP_TAC 657 THEN FIRST_ASSUM MATCH_MP_TAC 658 THEN ASM_REWRITE_TAC[LESS_EQ_REFL] 659 ); 660 661 662val REDL_FV = store_thm 663 ("REDL_FV", 664 ���!(M:^term) M'. 665 REDL M M' ==> (FV M' SUBSET FV M)���, 666 rule_induct REDL_strong_ind (* strong, not weak induction *) 667 THEN REWRITE_TAC[FV_term,SUBSET_REFL] 668 THEN REPEAT STRIP_TAC (* 3 subgoals *) 669 THENL 670 [ MATCH_MP_TAC SUBSET_DIFF 671 THEN ASM_REWRITE_TAC[], 672 673 IMP_RES_TAC SUBSETS_UNION, 674 675 MATCH_MP_TAC SUBSET_TRANS 676 THEN EXISTS_TAC ���FV (t2:^term) DIFF {x} UNION FV (u2:^term)��� 677 THEN REWRITE_TAC[FV_SUB,FV_term] 678 THEN MATCH_MP_TAC SUBSETS_UNION 679 THEN ASM_REWRITE_TAC[] 680 THEN MATCH_MP_TAC SUBSET_DIFF 681 THEN ASM_REWRITE_TAC[] 682 ] 683 ); 684 685 686val REDL_RENAME = store_thm 687 ("REDL_RENAME", 688 ���!t1:^term t2 t1' x y. 689 REDL t1 t2 /\ (Lam x t1 = Lam y t1') ==> 690 (Lam x t2 = Lam y (t2 <[ [x, Var y]))���, 691 REPEAT STRIP_TAC 692 THEN IMP_RES_TAC REDL_FV 693 THEN IMP_RES_TAC LAMBDA_RENAME 694 ); 695 696 697 698val REDL_SUBSTITUTIVE_BASE = store_thm 699 ("REDL_SUBSTITUTIVE_BASE", 700 ���!(M:^term) N. 701 REDL M N ==> 702 !L x. REDL (M <[ [x,L]) (N <[ [x,L])���, 703 rule_induct REDL_height_strong_ind (* strong, not weak induction *) 704 THEN REPEAT STRIP_TAC (* 4 subgoals *) 705 THENL 706 [ REWRITE_TAC[REDL_REFL], 707 708 REWRITE_TAC[SUB_term] 709 THEN MATCH_MP_TAC REDL_App 710 THEN ASM_REWRITE_TAC[], 711 712 ONCE_REWRITE_TAC[SUB_term] 713 THEN SIMPLE_SUBST_TAC 714 THEN IMP_RES_THEN IMP_RES_TAC REDL_RENAME 715 THEN IMP_RES_THEN ONCE_REWRITE_THM SUB_RENAME_TERM 716 THEN POP_TAC 717 THEN DEP_ONCE_REWRITE_TAC[BARENDREGT_SUBSTITUTION_LEMMA] 718 THEN ASM_REWRITE_TAC[] 719 THEN MATCH_MP_TAC REDL_BETA 720 THEN ASM_REWRITE_TAC[] 721 THEN FIRST_ASSUM MATCH_MP_TAC 722 THEN ASM_REWRITE_TAC[] 723 THEN IMP_RES_THEN REWRITE_THM Lam_one_one_RENAME 724 THEN FIRST_ASSUM MATCH_MP_TAC 725 THEN ASM_REWRITE_TAC[], 726 727 SIMPLE_SUBST_TAC 728 THEN MATCH_MP_TAC REDL_Lam 729 THEN FIRST_ASSUM MATCH_MP_TAC 730 THEN ASM_REWRITE_TAC[] 731 THEN IMP_RES_THEN REWRITE_THM Lam_one_one_RENAME 732 THEN FIRST_ASSUM MATCH_MP_TAC 733 THEN ASM_REWRITE_TAC[] 734 ] 735 ); 736 737(* This is necessary for when we change a bound variable: *) 738 739val REDL_CHANGE_VAR = store_thm 740 ("REDL_CHANGE_VAR", 741 ���!t1:^term t2 x y t1'. 742 REDL t1 t2 /\ (Lam x t1 = Lam y t1') ==> 743 REDL t1' (t2 <[ [x, Var y])���, 744 REPEAT STRIP_TAC 745 THEN IMP_RES_THEN REWRITE_THM Lam_one_one_RENAME 746 THEN MATCH_MP_TAC REDL_SUBSTITUTIVE_BASE 747 THEN FIRST_ASSUM ACCEPT_TAC 748 ); 749 750 751(* This is Barendregt's Lemma 3.2.4 Case 1. *) 752val REDL_SUBSTITUTIVE_SAME = store_thm 753 ("REDL_SUBSTITUTIVE_SAME", 754 ���!M:^term. 755 (!N N' x. REDL N N' ==> 756 REDL (M <[ [x,N]) (M <[ [x,N']))���, 757 MUTUAL_INDUCT_THEN term_height_induct ASSUME_TAC 758 THEN REPEAT STRIP_TAC 759 THENL (* 3 subgoals *) 760 [ REWRITE_TAC[SUB_term] 761 THEN REWRITE_TAC[REDL_REFL], 762 763 REWRITE_TAC[SUB_term,SUB] 764 THEN COND_CASES_TAC 765 THEN ASM_REWRITE_TAC[REDL_REFL], 766 767 REWRITE_TAC[SUB_term] 768 THEN DEP_ASM_REWRITE_TAC[REDL_rules_sat], 769 770 SIMPLE_SUBST_TAC 771 THEN DEP_ASM_REWRITE_TAC[REDL_rules_sat] 772 ] 773 ); 774 775 776 777 778 779(* This is Barendregt's Lemma 3.2.4. *) 780val REDL_SUBSTITUTIVE = store_thm 781 ("REDL_SUBSTITUTIVE", 782 ���!M:^term M'. 783 REDL M M' ==> 784 (!N N' x. REDL N N' ==> 785 REDL (M <[ [x,N]) (M' <[ [x,N']))���, 786 rule_induct REDL_height_strong_ind (* strong, not weak induction *) 787 THEN REPEAT STRIP_TAC (* 4 subgoals *) 788 THENL 789 [ (* Case 1 *) 790 DEP_ASM_REWRITE_TAC[REDL_SUBSTITUTIVE_SAME], 791 792 (* Case 3 *) 793 REWRITE_TAC[SUB_term] 794 THEN DEP_ASM_REWRITE_TAC[REDL_rules_sat], 795 796 (* Case 4 *) 797 ONCE_REWRITE_TAC[SUB_term] 798 THEN SIMPLE_SUBST_TAC 799 THEN IMP_RES_THEN IMP_RES_TAC REDL_CHANGE_VAR 800 THEN IMP_RES_THEN IMP_RES_TAC REDL_RENAME 801 THEN IMP_RES_THEN ONCE_REWRITE_THM SUB_RENAME_TERM 802 THEN DEP_ONCE_REWRITE_TAC[BARENDREGT_SUBSTITUTION_LEMMA] 803 THEN ASM_REWRITE_TAC[] 804 THEN MATCH_MP_TAC REDL_BETA 805 THEN DEP_ONCE_ASM_REWRITE_TAC[] 806 THEN ASM_REWRITE_TAC[], 807 808 (* Case 2 *) 809 SIMPLE_SUBST_TAC 810 THEN IMP_RES_THEN IMP_RES_TAC REDL_CHANGE_VAR 811 THEN MATCH_MP_TAC REDL_Lam 812 THEN DEP_ONCE_ASM_REWRITE_TAC[] 813 THEN UNDISCH_LAST_TAC 814 THEN IMP_RES_THEN REWRITE_THM Lam_one_one 815 THEN ASM_REWRITE_TAC[] 816 ] 817 ); 818 819 820 821(* Barendregt lemma 3.2.5 (expanded) *) 822 823val REDL_cases = store_thm 824 ("REDL_cases", 825 ���(!a t2:^term. 826 REDL (Con a) t2 ==> 827 (t2 = Con a)) /\ 828 (!x t2:^term. 829 REDL (Var x) t2 ==> 830 (t2 = Var x)) /\ 831 (!t u t2:^term. 832 REDL (App t u) t2 ==> 833 ((?t' u'. (t2 = (App t' u')) /\ REDL t t' /\ REDL u u') \/ 834 (?x t' t'' u'. (t = Lam x t') /\ 835 (t2 = (t'' <[ [x,u'])) /\ 836 REDL t' t'' /\ 837 REDL u u'))) /\ 838 (!x t t2:^term. 839 REDL (Lam x t) t2 ==> 840 (?t'. (t2 = Lam x t') /\ REDL t t'))���, 841 REPEAT CONJ_TAC 842 THEN REPEAT GEN_TAC THEN DISCH_THEN (STRIP_ASSUME_TAC o 843 REWRITE_RULE[term_distinct,term_one_one] o 844 ONCE_REWRITE_RULE REDL_inv_thms) 845 THENL (* 5 subgoals *) 846 [ POP_ASSUM REWRITE_THM 847 THEN DISJ1_TAC 848 THEN EXISTS_TAC ���t:^term��� 849 THEN EXISTS_TAC ���u:^term��� 850 THEN REWRITE_TAC[REDL_REFL], 851 852 DISJ1_TAC 853 THEN EXISTS_TAC ���t2':^term��� 854 THEN EXISTS_TAC ���u2:^term��� 855 THEN ASM_REWRITE_TAC[], 856 857 DISJ2_TAC 858 THEN EXISTS_TAC ���x:var��� 859 THEN EXISTS_TAC ���t1':^term��� 860 THEN EXISTS_TAC ���t2':^term��� 861 THEN EXISTS_TAC ���u2:^term��� 862 THEN ASM_REWRITE_TAC[], 863 864 EXISTS_TAC ���t:^term��� 865 THEN ASM_REWRITE_TAC[REDL_REFL], 866 867 EXISTS_TAC ���(t2':^term) <[ [x', Var x]��� 868 THEN ASSUM_LIST (ASSUME_TAC o SYM o hd o rev) 869 THEN IMP_RES_THEN IMP_RES_TAC REDL_RENAME 870 THEN IMP_RES_TAC REDL_CHANGE_VAR 871 THEN ASM_REWRITE_TAC[] 872 ] 873 ); 874 875val [REDL_Con_case, REDL_Var_case, REDL_App_case, REDL_Lam_case] 876 = CONJUNCTS REDL_cases; 877 878 879val REDL_Lam_CONF = store_thm 880 ("REDL_Lam_CONF", 881 ���!t1:^term t2 t3 x. 882 REDL (Lam x t1) t3 /\ REDL (Lam x t2) t3 ==> 883 (?t4. t3 = Lam x t4)���, 884 REPEAT STRIP_TAC 885 THEN IMP_RES_TAC REDL_Lam_case 886 THEN ASM_REWRITE_TAC[term_one_one] 887 THEN EXISTS_TAC ���t'':^term��� 888 THEN REFL_TAC 889 ); 890 891val REDL_Lam_MONO = store_thm 892 ("REDL_Lam_MONO", 893 ���!x t1:^term t2. 894 REDL (Lam x t1) (Lam x t2) ==> 895 REDL t1 t2���, 896 REPEAT STRIP_TAC 897 THEN IMP_RES_TAC REDL_Lam_case 898 THEN REWRITE_ALL_TAC[term_one_one] 899 THEN ASM_REWRITE_TAC[] 900 ); 901 902 903 904(* Barendregt Lemma 3.2.6. *) 905 906val REDL_DIAMOND_LEMMA = store_thm 907 ("REDL_DIAMOND_LEMMA", 908 ���!t1:^term t2. 909 REDL t1 t2 ==> 910 (!t3. REDL t1 t3 ==> 911 (?t4. REDL t2 t4 /\ REDL t3 t4))���, 912 rule_induct REDL_strong_ind (* strong, not weak induction *) 913 THEN REPEAT STRIP_TAC 914 THENL (* 4 subgoals *) 915 [ (* Case 1. *) 916 EXISTS_TAC ���t3:^term��� 917 THEN ASM_REWRITE_TAC[REDL_rules_sat], 918 919 (* Case 4. *) 920 IMP_RES_TAC REDL_cases 921 THEN RES_TAC 922 THEN EXISTS_TAC ���Lam x (t4:^term)��� 923 THEN DEP_ASM_REWRITE_TAC[REDL_rules_sat], 924 925 (* Case 3. *) 926 IMP_RES_TAC REDL_cases 927 THENL 928 [ (* Subcase 3.1 *) 929 RES_TAC 930 THEN EXISTS_TAC ���App t4'' (t4:^term)��� 931 THEN DEP_ASM_REWRITE_TAC[REDL_rules_sat], 932 933 (* Subcase 3.2 *) 934 UNDISCH_THEN ���t1 = Lam x (t':^term)��� REWRITE_ALL_THM 935 THEN UNDISCH_THEN ���(t3:^term) = t'' <[ [x,u']��� 936 REWRITE_ALL_THM 937 THEN IMP_RES_TAC REDL_Lam_case 938 THEN UNDISCH_THEN ���t2 = Lam x (t''':^term)��� REWRITE_ALL_THM 939 THEN ASSUME_TAC (SPEC_ALL (MATCH_MP REDL_Lam 940 (ASSUME ���REDL t' (t'':^term)���))) 941 THEN RES_TAC 942 THEN POP_TAC 943 THEN ASSUM_LIST (fn asl => 944 STRIP_ASSUME_TAC (MATCH_MP REDL_Lam_CONF 945 (CONJ (hd asl) (hd (tl asl))))) 946 THEN POP_ASSUM REWRITE_ALL_THM 947 THEN EXISTS_TAC ���(t4''':^term) <[ [x,t4]��� 948 THEN IMP_RES_TAC REDL_Lam_MONO 949 THEN DEP_ASM_REWRITE_TAC[REDL_BETA] 950 THEN DEP_ASM_REWRITE_TAC[REDL_SUBSTITUTIVE] 951 ], 952 953 (* Case 2. *) 954 IMP_RES_TAC REDL_cases 955 THENL 956 [ (* Subcase 2.1 *) 957 IMP_RES_TAC REDL_Lam_case 958 THEN UNDISCH_THEN ���(t':^term) = Lam x t''��� REWRITE_ALL_THM 959 THEN RES_TAC 960 THEN EXISTS_TAC ���(t4'':^term) <[ [x, t4]��� 961 THEN DEP_ASM_REWRITE_TAC[REDL_rules_sat,REDL_SUBSTITUTIVE], 962 963 (* Subcase 2.2 *) 964 UNDISCH_THEN ���(t3:^term) = t'' <[ [x',u']��� REWRITE_ALL_THM 965 THEN FIRST_ASSUM (fn th => 966 (UNDISCH_THEN (concl th) (ASSUME_TAC o SYM))) 967 THEN IMP_RES_THEN IMP_RES_TAC REDL_CHANGE_VAR 968 THEN IMP_RES_THEN IMP_RES_TAC REDL_RENAME 969 THEN RES_TAC 970 THEN POP_TAC 971 THEN EXISTS_TAC ���(t4'':^term) <[ [x,t4]��� 972 THEN IMP_RES_THEN ONCE_REWRITE_THM SUB_RENAME_TERM 973 THEN DEP_ASM_REWRITE_TAC[REDL_SUBSTITUTIVE] 974 ] 975 ] 976 ); 977 978 979 980val REDL_DIAMOND = store_thm 981 ("REDL_DIAMOND", 982 ���DIAMOND (REDL:^term_rel)���, 983 REWRITE_TAC[DIAMOND] 984 THEN REPEAT STRIP_TAC 985 THEN IMP_RES_TAC REDL_DIAMOND_LEMMA 986 THEN EXISTS_TAC ���t4'':^term��� 987 THEN ASM_REWRITE_TAC[] 988 ); 989 990 991 992 993 994(* --------------------------------------------------------------------- *) 995(* (REDC t1 t2) will now be defined on the sigma calculus such that *) 996(* 1) REDC provides the maximal parallel reduction step, that *) 997(* contracts all redexes in t1. *) 998(* 2) We can close any diamond and prove the diamond lemma for REDL *) 999(* by closing the left and right triangles independently. *) 1000(* --------------------------------------------------------------------- *) 1001 1002val REDC = 1003���REDC : ^term_rel���; 1004 1005val REDC_patterns = [���^REDC t1 t2���]; 1006 1007val REDC_rules_tm = 1008��� 1009 1010 (* -------------------------------------------- *) 1011 (^REDC (Con a) (Con a)) /\ 1012 1013 1014 (* -------------------------------------------- *) 1015 (^REDC (Var x) (Var x)) /\ 1016 1017 1018 ((^REDC t1 t2) 1019 (* -------------------------------------------- *) ==> 1020 (^REDC (Lam x t1) (Lam x t2))) /\ 1021 1022 1023 ((^REDC t1 t2) /\ (^REDC u1 u2) /\ (!t x. ~(t1 = Lam x t)) 1024 (* -------------------------------------------- *) ==> 1025 (^REDC (App t1 u1) (App t2 u2))) /\ 1026 1027 1028 ((^REDC t1 t2) /\ (^REDC u1 u2) 1029 (* -------------------------------------------- *) ==> 1030 (^REDC (App (Lam x t1) u1) (t2 <[ [x,u2]))) 1031���; 1032 1033val (REDC_rules_sat,REDC_ind_thm) = 1034 define_inductive_relations REDC_patterns REDC_rules_tm; 1035 1036val REDC_inv_thms = prove_inversion_theorems 1037 REDC_rules_sat REDC_ind_thm; 1038 1039val REDC_strong_ind = prove_strong_induction 1040 REDC_rules_sat REDC_ind_thm; 1041 1042val _ = save_thm ("REDC_rules_sat", REDC_rules_sat); 1043val _ = save_thm ("REDC_ind_thm", REDC_ind_thm); 1044val _ = save_thm ("REDC_inv_thms", LIST_CONJ REDC_inv_thms); 1045val _ = save_thm ("REDC_strong_ind", REDC_strong_ind); 1046 1047 1048val [REDC_Con, REDC_Var, REDC_Lam, REDC_App, REDC_BETA] 1049 = CONJUNCTS REDC_rules_sat; 1050 1051 1052 1053val REDC_height_ind_thm_LEMMA = store_thm 1054 ("REDC_height_ind_thm_LEMMA", 1055 ���!n P_0. 1056 (!a. P_0 (Con a) (Con a)) /\ 1057 (!x. P_0 (Var x) (Var x)) /\ 1058 (!x t1 t2. 1059 (!t1' t2'. REDC t1' t2' /\ 1060 (HEIGHT t1 = HEIGHT t1') ==> P_0 t1' t2') 1061 ==> P_0 (Lam x t1) (Lam x t2)) /\ 1062 (!t1 u1 t2 u2. 1063 P_0 t1 t2 /\ P_0 u1 u2 /\ (!t x. ~(t1 = Lam x t)) ==> 1064 P_0 (App t1 u1) (App t2 u2)) /\ 1065 (!x t1 u1 t2 u2. 1066 (!t1' t2'. REDC t1' t2' /\ 1067 (HEIGHT t1 = HEIGHT t1') ==> P_0 t1' t2') /\ 1068 P_0 u1 u2 ==> 1069 P_0 (App (Lam x t1) u1) (t2 <[ [x,u2])) 1070 ==> 1071 (!t1:^term t2. REDC t1 t2 ==> 1072 ((HEIGHT t1 <= n) ==> 1073 P_0 t1 t2))���, 1074 INDUCT_TAC 1075 THEN REPEAT GEN_TAC 1076 THEN STRIP_TAC 1077 THENL 1078 [ REWRITE_TAC[HEIGHT_LESS_EQ_ZERO] 1079 THEN REPEAT STRIP_TAC 1080 THEN ASM_REWRITE_TAC[] 1081 THEN UNDISCH_TAC ���REDC (t1:^term) t2��� 1082 THEN ONCE_REWRITE_TAC REDC_inv_thms 1083 THEN ASM_REWRITE_TAC[term_distinct,term_one_one] 1084 THEN STRIP_TAC 1085 THEN ASM_REWRITE_TAC[], 1086 1087 UNDISCH_ALL_TAC 1088 THEN DISCH_THEN ((fn th => REPEAT DISCH_TAC 1089 THEN ASSUME_TAC th) o SPEC_ALL) 1090 THEN POP_ASSUM MP_TAC 1091 THEN ASM_REWRITE_TAC[] 1092 THEN DISCH_THEN (fn th => UNDISCH_ALL_TAC THEN STRIP_ASSUME_TAC th) 1093 THEN REPEAT DISCH_TAC 1094 THEN rule_induct REDC_ind_thm 1095 THEN REWRITE_TAC[HEIGHT] 1096 THEN REWRITE_TAC[MAX_SUC,MAX_LESS_EQ,LESS_EQ_MONO,ZERO_LESS_EQ] 1097 THEN REPEAT STRIP_TAC 1098 THEN ASM_REWRITE_TAC[] 1099 THENL (* 3 subgoals *) 1100 [ FIRST_ASSUM MATCH_MP_TAC 1101 THEN REPEAT STRIP_TAC 1102 THEN ASSUM_LIST 1103 (MATCH_MP_TAC o REWRITE_RULE[AND_IMP_INTRO] o hd o rev) 1104 THEN POP_ASSUM (REWRITE_THM o SYM) 1105 THEN ASM_REWRITE_TAC[], 1106 1107 FIRST_ASSUM MATCH_MP_TAC 1108 THEN ASM_REWRITE_TAC[] 1109 THEN CONJ_TAC 1110 THEN FIRST_ASSUM MATCH_MP_TAC 1111 THEN IMP_RES_TAC LESS_EQ_IMP_LESS_SUC 1112 THEN IMP_RES_TAC LESS_IMP_LESS_OR_EQ, 1113 1114 FIRST_ASSUM MATCH_MP_TAC 1115 THEN CONJ_TAC 1116 THENL 1117 [ REPEAT STRIP_TAC 1118 THEN ASSUM_LIST 1119 (MATCH_MP_TAC o REWRITE_RULE[AND_IMP_INTRO] o hd o rev) 1120 THEN POP_ASSUM (REWRITE_THM o SYM) 1121 THEN IMP_RES_TAC LESS_EQ_IMP_LESS_SUC 1122 THEN IMP_RES_TAC LESS_MONO_EQ 1123 THEN IMP_RES_TAC LESS_IMP_LESS_OR_EQ 1124 THEN ASM_REWRITE_TAC[], 1125 1126 FIRST_ASSUM MATCH_MP_TAC 1127 THEN IMP_RES_TAC LESS_EQ_IMP_LESS_SUC 1128 THEN IMP_RES_TAC LESS_IMP_LESS_OR_EQ 1129 ] 1130 ] 1131 ] 1132 ); 1133 1134val REDC_height_ind_thm = store_thm 1135 ("REDC_height_ind_thm", 1136 ���!P_0. 1137 (!a. P_0 (Con a) (Con a)) /\ 1138 (!x. P_0 (Var x) (Var x)) /\ 1139 (!x t1 t2. 1140 (!t1' t2'. REDC t1' t2' /\ 1141 (HEIGHT t1 = HEIGHT t1') ==> P_0 t1' t2') 1142 ==> P_0 (Lam x t1) (Lam x t2)) /\ 1143 (!t1 u1 t2 u2. 1144 P_0 t1 t2 /\ P_0 u1 u2 /\ (!t x. ~(t1 = Lam x t)) ==> 1145 P_0 (App t1 u1) (App t2 u2)) /\ 1146 (!x t1 u1 t2 u2. 1147 (!t1' t2'. 1148 REDC t1' t2' /\ (HEIGHT t1 = HEIGHT t1') ==> P_0 t1' t2') /\ 1149 P_0 u1 u2 ==> 1150 P_0 (App (Lam x t1) u1) (t2 <[ [(x,u2)])) ==> 1151 !t1:^term t2. REDC t1 t2 ==> P_0 t1 t2���, 1152 REPEAT STRIP_TAC 1153 THEN MP_TAC (SPEC_ALL (SPEC ���HEIGHT (t1:^term)��� 1154 REDC_height_ind_thm_LEMMA)) 1155 THEN ASM_REWRITE_TAC[AND_IMP_INTRO] 1156 THEN REPEAT STRIP_TAC 1157 THEN FIRST_ASSUM MATCH_MP_TAC 1158 THEN ASM_REWRITE_TAC[LESS_EQ_REFL] 1159 ); 1160 1161val REDC_height_strong_ind_LEMMA = store_thm 1162 ("REDC_height_strong_ind_LEMMA", 1163 ���!n P_0. 1164 (!a. P_0 (Con a) (Con a)) /\ 1165 (!x. P_0 (Var x) (Var x)) /\ 1166 (!t1 u1 t2 u2. 1167 P_0 t1 t2 /\ REDC t1 t2 /\ P_0 u1 u2 /\ REDC u1 u2 /\ 1168 (!t x. ~(t1 = Lam x t)) ==> 1169 P_0 (App t1 u1) (App t2 u2)) /\ 1170 (!x t1 u1 t2 u2. 1171 (!t1' t2'. 1172 REDC t1' t2' /\ (HEIGHT t1 = HEIGHT t1') ==> 1173 P_0 t1' t2') /\ REDC t1 t2 /\ 1174 P_0 u1 u2 /\ REDC u1 u2 ==> 1175 P_0 (App (Lam x t1) u1) (t2 <[ [(x,u2)])) /\ 1176 (!x t1 t2. 1177 (!t1' t2'. 1178 REDC t1' t2' /\ (HEIGHT t1 = HEIGHT t1') ==> 1179 P_0 t1' t2') /\ REDC t1 t2 ==> 1180 P_0 (Lam x t1) (Lam x t2)) ==> 1181 !t1:^term t2. REDC t1 t2 ==> HEIGHT t1 <= n ==> P_0 t1 t2 1182 ���, 1183 INDUCT_TAC 1184 THEN REPEAT GEN_TAC 1185 THEN STRIP_TAC 1186 THENL 1187 [ REWRITE_TAC[HEIGHT_LESS_EQ_ZERO] 1188 THEN REPEAT STRIP_TAC 1189 THEN ASM_REWRITE_TAC[] 1190 THEN UNDISCH_TAC ���REDC (t1:^term) t2��� 1191 THEN ONCE_REWRITE_TAC REDC_inv_thms 1192 THEN ASM_REWRITE_TAC[term_distinct] 1193 THEN STRIP_TAC 1194 THEN ASM_REWRITE_TAC[], 1195 1196 UNDISCH_ALL_TAC 1197 THEN DISCH_THEN ((fn th => REPEAT DISCH_TAC 1198 THEN ASSUME_TAC th) o SPEC_ALL) 1199 THEN POP_ASSUM MP_TAC 1200 THEN ASM_REWRITE_TAC[] 1201 THEN DISCH_THEN (fn th => UNDISCH_ALL_TAC THEN STRIP_ASSUME_TAC th) 1202 THEN REPEAT DISCH_TAC 1203 THEN rule_induct REDC_strong_ind 1204 THEN REWRITE_TAC[HEIGHT] 1205 THEN REWRITE_TAC[MAX_SUC,MAX_LESS_EQ,LESS_EQ_MONO,ZERO_LESS_EQ] 1206 THEN REPEAT STRIP_TAC 1207 THEN ASM_REWRITE_TAC[] 1208 THENL (* 3 subgoals *) 1209 [ FIRST_ASSUM MATCH_MP_TAC 1210 THEN ASM_REWRITE_TAC[] 1211 THEN REPEAT STRIP_TAC 1212 THEN ASSUM_LIST 1213 (MATCH_MP_TAC o REWRITE_RULE[AND_IMP_INTRO] o hd o rev) 1214 THEN POP_ASSUM (REWRITE_THM o SYM) 1215 THEN ASM_REWRITE_TAC[], 1216 1217 FIRST_ASSUM MATCH_MP_TAC 1218 THEN ASM_REWRITE_TAC[] 1219 THEN CONJ_TAC 1220 THEN FIRST_ASSUM MATCH_MP_TAC 1221 THEN IMP_RES_TAC LESS_EQ_IMP_LESS_SUC 1222 THEN IMP_RES_TAC LESS_IMP_LESS_OR_EQ, 1223 1224 FIRST_ASSUM MATCH_MP_TAC 1225 THEN ASM_REWRITE_TAC[] 1226 THEN REPEAT STRIP_TAC 1227 THENL 1228 [ ASSUM_LIST 1229 (MATCH_MP_TAC o REWRITE_RULE[AND_IMP_INTRO] o hd o rev) 1230 THEN ASM_REWRITE_TAC[] 1231 THEN POP_ASSUM (REWRITE_THM o SYM) 1232 THEN IMP_RES_TAC LESS_EQ_IMP_LESS_SUC 1233 THEN IMP_RES_TAC LESS_MONO_EQ 1234 THEN IMP_RES_TAC LESS_IMP_LESS_OR_EQ, 1235 1236 FIRST_ASSUM MATCH_MP_TAC 1237 THEN IMP_RES_TAC LESS_EQ_IMP_LESS_SUC 1238 THEN IMP_RES_TAC LESS_IMP_LESS_OR_EQ 1239 ] 1240 ] 1241 ] 1242 ); 1243 1244val REDC_height_strong_ind = store_thm 1245 ("REDC_height_strong_ind", 1246 ���!P_0. 1247 (!a. P_0 (Con a) (Con a)) /\ 1248 (!x. P_0 (Var x) (Var x)) /\ 1249 (!t1 u1 t2 u2. 1250 P_0 t1 t2 /\ REDC t1 t2 /\ P_0 u1 u2 /\ REDC u1 u2 /\ 1251 (!t x. ~(t1 = Lam x t)) ==> 1252 P_0 (App t1 u1) (App t2 u2)) /\ 1253 (!x t1 u1 t2 u2. 1254 (!t1' t2'. 1255 REDC t1' t2' /\ (HEIGHT t1 = HEIGHT t1') ==> 1256 P_0 t1' t2') /\ REDC t1 t2 /\ 1257 P_0 u1 u2 /\ REDC u1 u2 ==> 1258 P_0 (App (Lam x t1) u1) (t2 <[ [(x,u2)])) /\ 1259 (!x t1 t2. 1260 (!t1' t2'. 1261 REDC t1' t2' /\ (HEIGHT t1 = HEIGHT t1') ==> 1262 P_0 t1' t2') /\ REDC t1 t2 ==> 1263 P_0 (Lam x t1) (Lam x t2)) ==> 1264 !(t1:^term) t2. REDC t1 t2 ==> P_0 t1 t2���, 1265 REPEAT STRIP_TAC 1266 THEN MP_TAC (SPEC_ALL (SPEC ���HEIGHT (t1:^term)��� 1267 REDC_height_strong_ind_LEMMA)) 1268 THEN ASM_REWRITE_TAC[AND_IMP_INTRO] 1269 THEN REPEAT STRIP_TAC 1270 THEN FIRST_ASSUM MATCH_MP_TAC 1271 THEN ASM_REWRITE_TAC[LESS_EQ_REFL] 1272 ); 1273 1274 1275val REDC_FV = store_thm 1276 ("REDC_FV", 1277 ���!(M:^term) M'. 1278 REDC M M' ==> (FV M' SUBSET FV M)���, 1279 rule_induct REDC_strong_ind (* strong, not weak induction *) 1280 THEN REWRITE_TAC[FV_term,SUBSET_REFL] 1281 THEN REPEAT STRIP_TAC (* 3 subgoals *) 1282 THENL 1283 [ MATCH_MP_TAC SUBSET_DIFF 1284 THEN ASM_REWRITE_TAC[], 1285 1286 IMP_RES_TAC SUBSETS_UNION, 1287 1288 MATCH_MP_TAC SUBSET_TRANS 1289 THEN EXISTS_TAC ���FV (t2:^term) DIFF {x} UNION FV (u2:^term)��� 1290 THEN REWRITE_TAC[FV_SUB,FV_term] 1291 THEN MATCH_MP_TAC SUBSETS_UNION 1292 THEN ASM_REWRITE_TAC[] 1293 THEN MATCH_MP_TAC SUBSET_DIFF 1294 THEN ASM_REWRITE_TAC[] 1295 ] 1296 ); 1297 1298 1299val REDC_RENAME = store_thm 1300 ("REDC_RENAME", 1301 ���!(t1:^term) t2 t1' x y. 1302 REDC t1 t2 /\ (Lam x t1 = Lam y t1') ==> 1303 (Lam x t2 = Lam y (t2 <[ [x, Var y]))���, 1304 REPEAT STRIP_TAC 1305 THEN IMP_RES_TAC REDC_FV 1306 THEN IMP_RES_TAC LAMBDA_RENAME 1307 ); 1308 1309(* NOT TRUE for REDC! REDC (Var x) (Var x), but not REDC ((\x.x)N) ((\x.x)N) ! 1310 1311val REDC_SUBSTITUTIVE_BASE = store_thm 1312 ("REDC_SUBSTITUTIVE_BASE", 1313 ���!(M:^term) N. 1314 REDC M N ==> 1315 !L x. REDC (M <[ [x,L]) (N <[ [x,L])���, 1316 rule_induct REDC_height_strong_ind (* strong, not weak induction *) 1317 THEN REPEAT STRIP_TAC (* 4 subgoals *) 1318 THENL 1319 [ REWRITE_TAC[SUB_term,REDC_Var], 1320 1321 REWRITE_TAC[SUB_term] 1322 THEN MATCH_MP_TAC REDC_App 1323 THEN ASM_REWRITE_TAC[], 1324 1325 ONCE_REWRITE_TAC[SUB_term] 1326 THEN SIMPLE_SUBST_TAC 1327 THEN IMP_RES_THEN IMP_RES_TAC REDC_RENAME 1328 THEN IMP_RES_THEN ONCE_REWRITE_THM SUB_RENAME_TERM 1329 THEN POP_TAC 1330 THEN DEP_ONCE_REWRITE_TAC[BARENDREGT_SUBSTITUTION_LEMMA] 1331 THEN ASM_REWRITE_TAC[] 1332 THEN MATCH_MP_TAC REDC_BETA 1333 THEN ASM_REWRITE_TAC[] 1334 THEN FIRST_ASSUM MATCH_MP_TAC 1335 THEN ASM_REWRITE_TAC[] 1336 THEN IMP_RES_THEN REWRITE_THM Lam_one_one_RENAME 1337 THEN FIRST_ASSUM MATCH_MP_TAC 1338 THEN ASM_REWRITE_TAC[], 1339 1340 SIMPLE_SUBST_TAC 1341 THEN MATCH_MP_TAC REDC_Lam 1342 THEN FIRST_ASSUM MATCH_MP_TAC 1343 THEN ASM_REWRITE_TAC[] 1344 THEN IMP_RES_THEN REWRITE_THM Lam_one_one_RENAME 1345 THEN FIRST_ASSUM MATCH_MP_TAC 1346 THEN ASM_REWRITE_TAC[] 1347 ] 1348 ); 1349 1350*) 1351 1352val NOT_LAMBDA_SUBSTITUTIVE = store_thm 1353 ("NOT_LAMBDA_SUBSTITUTIVE", 1354 ���!(t1:^term) y z. 1355 (!t x. ~(t1 = Lam x t)) ==> 1356 (!t x. ~(t1 <[ [y,Var z] = Lam x t))���, 1357 MUTUAL_INDUCT_THEN term_height_induct ASSUME_TAC (* 4 subgoals *) 1358 THEN REPEAT GEN_TAC 1359 THEN DISCH_TAC 1360 THEN REPEAT GEN_TAC 1361 THEN REWRITE_TAC[SUB_term] 1362 THENL (* 4 subgoals *) 1363 [ REWRITE_TAC[term_distinct], 1364 1365 REWRITE_TAC[SUB] 1366 THEN COND_CASES_TAC 1367 THEN REWRITE_TAC[term_distinct], 1368 1369 REWRITE_TAC[term_distinct], 1370 1371 POP_ASSUM (MP_TAC o SPECL[``t1:^term``,``v:var``]) 1372 THEN REWRITE_TAC[] 1373 ] 1374 ); 1375 1376val REDC_SUBSTITUTIVE_VAR = store_thm 1377 ("REDC_SUBSTITUTIVE_VAR", 1378 ���!(M:^term) N. 1379 REDC M N ==> 1380 !y x. REDC (M <[ [x,Var y]) (N <[ [x,Var y])���, 1381 rule_induct REDC_height_strong_ind (* strong, not weak induction *) 1382 THEN REPEAT STRIP_TAC (* 5 subgoals *) 1383 THENL 1384 [ REWRITE_TAC[SUB_term] 1385 THEN REWRITE_TAC[REDC_Con], 1386 1387 REWRITE_TAC[SUB_term,SUB] 1388 THEN COND_CASES_TAC 1389 THEN REWRITE_TAC[REDC_Var], 1390 1391 REWRITE_TAC[SUB_term] 1392 THEN MATCH_MP_TAC REDC_App 1393 THEN ASM_REWRITE_TAC[] 1394 THEN MATCH_MP_TAC NOT_LAMBDA_SUBSTITUTIVE 1395 THEN ASM_REWRITE_TAC[], 1396 1397 ONCE_REWRITE_TAC[SUB_term] 1398 THEN SIMPLE_SUBST_TAC 1399 THEN IMP_RES_THEN IMP_RES_TAC REDC_RENAME 1400 THEN IMP_RES_THEN ONCE_REWRITE_THM SUB_RENAME_TERM 1401 THEN POP_TAC 1402 THEN DEP_ONCE_REWRITE_TAC[BARENDREGT_SUBSTITUTION_LEMMA] 1403 THEN ASM_REWRITE_TAC[FV_term,IN] 1404 THEN MATCH_MP_TAC REDC_BETA 1405 THEN ASM_REWRITE_TAC[] 1406 THEN FIRST_ASSUM MATCH_MP_TAC 1407 THEN ASM_REWRITE_TAC[] 1408 THEN IMP_RES_THEN REWRITE_THM Lam_one_one_RENAME 1409 THEN FIRST_ASSUM MATCH_MP_TAC 1410 THEN ASM_REWRITE_TAC[], 1411 1412 SIMPLE_SUBST_TAC 1413 THEN MATCH_MP_TAC REDC_Lam 1414 THEN FIRST_ASSUM MATCH_MP_TAC 1415 THEN ASM_REWRITE_TAC[] 1416 THEN IMP_RES_THEN REWRITE_THM Lam_one_one_RENAME 1417 THEN FIRST_ASSUM MATCH_MP_TAC 1418 THEN ASM_REWRITE_TAC[] 1419 ] 1420 ); 1421 1422(* This is for when we change a bound variable: *) 1423 1424val REDC_CHANGE_VAR = store_thm 1425 ("REDC_CHANGE_VAR", 1426 ���!(t1:^term) t2 x y t1'. 1427 REDC t1 t2 /\ (Lam x t1 = Lam y t1') ==> 1428 REDC t1' (t2 <[ [x, Var y])���, 1429 REPEAT STRIP_TAC 1430 THEN IMP_RES_THEN REWRITE_THM Lam_one_one_RENAME 1431 THEN MATCH_MP_TAC REDC_SUBSTITUTIVE_VAR 1432 THEN FIRST_ASSUM ACCEPT_TAC 1433 ); 1434 1435 1436(* Takahashi's trick, an alternative way to prove the diamond lemma. *) 1437 1438 1439(* Complete developments exist. *) 1440 1441val REDC_EXISTS = store_thm 1442 ("REDC_EXISTS", 1443 ���!t:^term. ?t'. REDC t t'���, 1444 MUTUAL_INDUCT_THEN term_induct STRIP_ASSUME_TAC (* 3 subgoals *) 1445 THEN REPEAT GEN_TAC 1446 THENL (* 4 subgoals *) 1447 [ EXISTS_TAC ``Con a :^term`` 1448 THEN REWRITE_TAC[REDC_Con], 1449 1450 EXISTS_TAC ``Var v :^term`` 1451 THEN REWRITE_TAC[REDC_Var], 1452 1453 ASM_CASES_TAC ``?(M:^term) x. t = Lam x M`` 1454 THENL 1455 [ POP_ASSUM STRIP_ASSUME_TAC 1456 THEN POP_ASSUM REWRITE_ALL_THM 1457 THEN UNDISCH_ALL_TAC 1458 THEN DISCH_THEN (MP_TAC o ONCE_REWRITE_RULE REDC_inv_thms) 1459 THEN REWRITE_TAC[term_distinct] 1460 THEN REPEAT STRIP_TAC 1461 THEN EXISTS_TAC ``(t2':^term) <[ [x',t''']`` 1462 THEN ASM_REWRITE_TAC[] 1463 THEN MATCH_MP_TAC REDC_BETA 1464 THEN ASM_REWRITE_TAC[], 1465 1466 UNDISCH_LAST_TAC 1467 THEN CONV_TAC (TOP_DEPTH_CONV NOT_EXISTS_CONV) 1468 THEN DISCH_TAC 1469 THEN EXISTS_TAC ``App t'' t''' :^term`` 1470 THEN MATCH_MP_TAC REDC_App 1471 THEN ASM_REWRITE_TAC[] 1472 ], 1473 1474 EXISTS_TAC ``Lam v t' :^term`` 1475 THEN MATCH_MP_TAC REDC_Lam 1476 THEN ASM_REWRITE_TAC[] 1477 ] 1478 ); 1479 1480val TAKAHASHI_TRIANGLE = store_thm 1481 ("TAKAHASHI_TRIANGLE", 1482 ���!(a:^term) d. REDC a d ==> 1483 !b. REDL a b ==> REDL b d���, 1484 rule_induct REDC_ind_thm (* strong, not weak induction *) 1485 THEN REPEAT STRIP_TAC 1486 THENL (* 5 subgoals *) 1487 [ IMP_RES_TAC REDL_Con_case 1488 THEN ASM_REWRITE_TAC[REDL_REFL], 1489 1490 IMP_RES_TAC REDL_Var_case 1491 THEN ASM_REWRITE_TAC[REDL_REFL], 1492 1493 IMP_RES_TAC REDL_Lam_case 1494 THEN ASM_REWRITE_TAC[] 1495 THEN MATCH_MP_TAC REDL_Lam 1496 THEN RES_TAC, 1497 1498 IMP_RES_TAC REDL_App_case 1499 THENL 1500 [ ASM_REWRITE_TAC[] 1501 THEN MATCH_MP_TAC REDL_App 1502 THEN RES_TAC 1503 THEN ASM_REWRITE_TAC[], 1504 1505 RES_TAC 1506 ], 1507 1508 IMP_RES_TAC REDL_App_case 1509 THENL 1510 [ IMP_RES_TAC REDL_Lam_case 1511 THEN ASM_REWRITE_TAC[] 1512 THEN MATCH_MP_TAC REDL_BETA 1513 THEN RES_TAC 1514 THEN ASM_REWRITE_TAC[], 1515 1516 ASM_REWRITE_TAC[] 1517 THEN UNDISCH_THEN ``Lam x t1 = Lam x' t':^term`` (ASSUME_TAC o SYM) 1518 THEN IMP_RES_THEN IMP_RES_TAC REDL_CHANGE_VAR 1519 THEN IMP_RES_THEN IMP_RES_TAC REDL_RENAME 1520 THEN IMP_RES_THEN ONCE_REWRITE_THM SUB_RENAME_TERM 1521 THEN DEP_REWRITE_TAC[REDL_SUBSTITUTIVE] 1522 THEN RES_TAC 1523 THEN ASM_REWRITE_TAC[] 1524 ] 1525 ] 1526 ); 1527 1528 1529val REDL_DIAMOND_TAKAHASHI = store_thm 1530 ("REDL_DIAMOND_TAKAHASHI", 1531 ���DIAMOND (REDL:^term_rel)���, 1532 REWRITE_TAC[DIAMOND] 1533 THEN REPEAT STRIP_TAC 1534 THEN STRIP_ASSUME_TAC (SPEC ``a:^term`` REDC_EXISTS) 1535 THEN IMP_RES_TAC TAKAHASHI_TRIANGLE 1536 THEN EXISTS_TAC ���t':^term��� 1537 THEN ASM_REWRITE_TAC[] 1538 ); 1539 1540 1541 1542 1543(* copied: *) 1544 1545val RC_INDUCT_TAC = 1546 let val rc_thm = RC_INDUCT 1547 fun tac (asl,w) = 1548 let open Rsyntax 1549 val {Bvar=u,Body} = dest_forall w 1550 val {Bvar=v,Body} = dest_forall Body 1551 val {ant,conseq} = dest_imp Body 1552 val (RC,Ru'v') = strip_comb ant 1553 val R = hd Ru'v' 1554 val u'v' = tl Ru'v' 1555 val u' = hd u'v' 1556 val v' = hd (tl u'v') 1557 (*val (RC,[R,u',v']) = strip_comb ant*) 1558 (*val {Name = "RC",...} = dest_const RC*) 1559 val _ = if #Name(dest_const RC) = "RC" then true else raise Match 1560 val _ = assert (aconv u) u' 1561 val _ = assert (aconv v) v' 1562 val P = list_mk_abs([u,v], conseq) 1563 val rc_thm' = BETA_RULE(ISPEC P (ISPEC R rc_thm)) 1564 in MATCH_MP_TAC rc_thm' (asl,w) 1565 end 1566 handle _ => raise HOL_ERR{origin_structure = "<top-level>", 1567 origin_function = "RC_INDUCT_TAC", 1568 message = "Unanticipated term structure"} 1569 in tac 1570 end; 1571 1572 1573(* 1574Barendregt Lemma 3.2.7, page 62, the proof begins with the note that 1575 1576 --->B SUBSET -->> SUBSET -->>B 1577 = l 1578 1579which in our notation corresponds to 1580 1581 RC (RED1 BETA_R) SUBSET REDL SUBSET RED BETA_R 1582 1583We first deal with the first (left) subset relation. 1584 1585Remember, 1586 1587Hol prf = Barendregt = Description 1588----------------------------------------- 1589RED1 R = --->R = one-step R-reduction 1590RED R = -->>R = R-reduction 1591REQ R = === R = R-equality (also called R-convertibility) 1592RC R = R-arrow with "=" underneath = reflexive closure 1593TC R = R-arrow with "*" superscript after = transitive closure 1594*) 1595 1596(* 1597val RC_BETA_IMP_REDL = store_thm 1598 ("RC_BETA_IMP_REDL", 1599 ���!t1:^term t2. RC BETA_R t1 t2 ==> REDL t1 t2���, 1600 RC_INDUCT_TAC 1601 THEN ONCE_REWRITE_TAC BETA_R_inv_thms 1602 THEN REPEAT STRIP_TAC 1603 THEN DEP_ASM_REWRITE_TAC[REDL_rules_sat] 1604 ); 1605*) 1606 1607val RED1_BETA_IMP_REDL_LEMMA = TAC_PROOF(([], 1608 ���!R (t1:^term) t2. 1609 RED1 R t1 t2 ==> (R = BETA_R) ==> REDL t1 t2���), 1610 rule_induct RED1_ind_thm 1611 THEN REPEAT STRIP_TAC 1612 THEN POP_ASSUM REWRITE_ALL_THM 1613 THENL 1614 [ POP_ASSUM (STRIP_ASSUME_TAC o ONCE_REWRITE_RULE BETA_R_inv_thms) 1615 THEN DEP_ASM_REWRITE_TAC[REDL_rules_sat], 1616 1617 DEP_ASM_REWRITE_TAC[REDL_rules_sat], 1618 1619 DEP_ASM_REWRITE_TAC[REDL_rules_sat], 1620 1621 DEP_ASM_REWRITE_TAC[REDL_rules_sat] 1622 ] 1623 ); 1624 1625val RED1_BETA_IMP_REDL = store_thm 1626 ("RED1_BETA_IMP_REDL", 1627 ���!t1:^term t2. 1628 RED1 BETA_R t1 t2 ==> REDL t1 t2���, 1629 REPEAT STRIP_TAC 1630 THEN IMP_RES_TAC RED1_BETA_IMP_REDL_LEMMA 1631 THEN POP_ASSUM (STRIP_ASSUME_TAC o REWRITE_RULE[]) 1632 ); 1633 1634val RC_RED1_BETA_IMP_REDL = store_thm 1635 ("RC_RED1_BETA_IMP_REDL", 1636 ���!t1:^term t2. RC (RED1 BETA_R) t1 t2 ==> REDL t1 t2���, 1637 RC_INDUCT_TAC 1638 THEN REWRITE_TAC[REDL_rules_sat] 1639 THEN REWRITE_TAC[RED1_BETA_IMP_REDL] 1640 ); 1641 1642val [RED1_R, RED1_App1, RED1_App2, RED1_Lam] = CONJUNCTS RED1_rules_sat; 1643 1644 1645val [RED_RED1, RED_REFL, RED_TRANS] 1646 = CONJUNCTS (CONV_RULE (DEPTH_CONV LEFT_IMP_EXISTS_CONV) RED_rules_sat); 1647 1648 1649val RED1_BETA_R = store_thm 1650 ("RED1_BETA_R", 1651 ���!x t:^term u. 1652 RED1 BETA_R (App (Lam x t) u) (t <[ [x,u])���, 1653 REPEAT STRIP_TAC 1654 THEN MATCH_MP_TAC RED1_R 1655 THEN REWRITE_TAC[BETA_R_rules_sat] 1656 ); 1657 1658val RED_BETA_R = store_thm 1659 ("RED_BETA_R", 1660 ���!x t1:^term t2 u1 u2. 1661 RED BETA_R t1 t2 /\ 1662 RED BETA_R u1 u2 ==> 1663 RED BETA_R (App (Lam x t1) u1) (t2 <[ [x,u2]) 1664 ���, 1665 REPEAT STRIP_TAC 1666 THEN MATCH_MP_TAC RED_TRANS 1667 THEN EXISTS_TAC ���App (Lam x t2) u2:^term��� 1668 THEN CONJ_TAC 1669 THENL 1670 [ MATCH_MP_TAC RED_TRANS 1671 THEN EXISTS_TAC ���App (Lam x t2) u1:^term��� 1672 THEN IMP_RES_TAC RED_COMPAT 1673 THEN RULE_ASSUM_TAC SPEC_ALL 1674 THEN IMP_RES_TAC RED_COMPAT 1675 THEN ASM_REWRITE_TAC[], 1676 1677 DEP_ASM_REWRITE_TAC[RED_RED1] 1678 THEN REWRITE_TAC[RED1_BETA_R] 1679 ] 1680 ); 1681 1682 1683val REDL_IMP_RED_BETA = store_thm 1684 ("REDL_IMP_RED_BETA", 1685 ���!t1:^term t2. REDL t1 t2 ==> RED BETA_R t1 t2���, 1686 rule_induct REDL_ind_thm 1687 THEN REPEAT STRIP_TAC 1688 THENL (* 4 subgoals *) 1689 [ REWRITE_TAC[RED_REFL], 1690 1691 IMP_RES_TAC RED_COMPAT 1692 THEN ASM_REWRITE_TAC[], 1693 1694 IMP_RES_TAC RED_COMPAT 1695 THEN MATCH_MP_TAC RED_TRANS 1696 THEN EXISTS_TAC ���App t2 u1:^term��� 1697 THEN ASM_REWRITE_TAC[], 1698 1699 MATCH_MP_TAC RED_BETA_R 1700 THEN ASM_REWRITE_TAC[] 1701 ] 1702 ); 1703 1704 1705val RC_RED1_IMP_RED = store_thm 1706 ("RC_RED1_IMP_RED", 1707 ���!R t1:^term t2. RC (RED1 R) t1 t2 1708 ==> RED R t1 t2���, 1709 GEN_TAC 1710 THEN RC_INDUCT_TAC 1711 THEN REPEAT STRIP_TAC 1712 THEN REWRITE_TAC[RED_REFL] 1713 THEN IMP_RES_TAC RED_RED1 1714 ); 1715 1716val TC_RC_RED1_IMP_RED = store_thm 1717 ("TC_RC_RED1_IMP_RED", 1718 ���!R t1:^term t2. TC (RC (RED1 R)) t1 t2 1719 ==> RED R t1 t2���, 1720 GEN_TAC 1721 THEN TC_INDUCT_TAC 1722 THEN REPEAT STRIP_TAC 1723 THEN IMP_RES_TAC RC_RED1_IMP_RED 1724 THEN IMP_RES_TAC RED_TRANS 1725 ); 1726 1727(* 1728val TC_RC_BETA_IMP_RED_BETA = store_thm 1729 ("TC_RC_BETA_IMP_RED_BETA", 1730 ���!t1:^term t2. TC (RC (RED1 BETA_R)) t1 t2 1731 ==> RED BETA_R t1 t2���, 1732 TC_INDUCT_TAC 1733 THEN REPEAT STRIP_TAC 1734 THEN IMP_RES_TAC RC_RED1_BETA_IMP_REDL 1735 THEN IMP_RES_TAC REDL_IMP_RED_BETA 1736 THEN IMP_RES_TAC RED_TRANS 1737 ); 1738*) 1739 1740val RED_IMP_TC_RC_RED1 = store_thm 1741 ("RED_IMP_TC_RC_RED1", 1742 ���!R t1:^term t2. RED R t1 t2 1743 ==> TC (RC (RED1 R)) t1 t2���, 1744 rule_induct RED_ind_thm 1745 THEN REPEAT STRIP_TAC 1746 THEN IMP_RES_TAC (REWRITE_RULE[transitive_def] TC_TRANSITIVE) 1747 THEN MATCH_MP_TAC TC_SUBSET 1748 THEN REWRITE_TAC[RC_REFLEXIVE] 1749 THEN IMP_RES_TAC RC_SUBSET 1750 ); 1751 1752val TC_RC_RED1_IS_RED = store_thm 1753 ("TC_RC_RED1_IS_RED", 1754 ���!R:^term_rel. TC (RC (RED1 R)) = RED R���, 1755 CONV_TAC (TOP_DEPTH_CONV FUN_EQ_CONV) 1756 THEN REPEAT GEN_TAC 1757 THEN EQ_TAC 1758 THEN STRIP_TAC 1759 THENL 1760 [ IMP_RES_TAC TC_RC_RED1_IMP_RED, 1761 1762 IMP_RES_TAC RED_IMP_TC_RC_RED1 1763 ] 1764 ); 1765 1766 1767val TC_REDL_IMP_RED_BETA = store_thm 1768 ("TC_REDL_IMP_RED_BETA", 1769 ���!t1:^term t2. TC REDL t1 t2 ==> RED BETA_R t1 t2���, 1770 TC_INDUCT_TAC 1771 THEN REPEAT STRIP_TAC 1772 THEN IMP_RES_TAC REDL_IMP_RED_BETA 1773 THEN IMP_RES_TAC RED_TRANS 1774 ); 1775 1776 1777val TC_MONOTONIC_LEMMA = TAC_PROOF(([], 1778 ���!R1 R2 (a:'a) b. 1779 TC R1 a b ==> (!x y. R1 x y ==> R2 x y) ==> TC R2 a b���), 1780 GEN_TAC THEN GEN_TAC 1781 THEN TC_INDUCT_TAC 1782 THEN REPEAT STRIP_TAC 1783 THENL 1784 [ RES_TAC 1785 THEN IMP_RES_TAC TC_SUBSET, 1786 1787 RES_TAC 1788 THEN IMP_RES_TAC (REWRITE_RULE[transitive_def] TC_TRANSITIVE) 1789 ] 1790 ); 1791 1792val TC_MONOTONIC = store_thm 1793 ("TC_MONOTONIC", 1794 ���!R1 R2 (a:'a) b. 1795 (!x y. R1 x y ==> R2 x y) ==> 1796 (TC R1 a b ==> TC R2 a b)���, 1797 REPEAT STRIP_TAC 1798 THEN IMP_RES_TAC TC_MONOTONIC_LEMMA 1799 ); 1800 1801 1802(* Barendregt Lemma 3.2.7. *) 1803 1804val TC_REDL_IS_RED_BETA = store_thm 1805 ("TC_REDL_IS_RED_BETA", 1806 ���TC (REDL:^term_rel) = RED BETA_R���, 1807 CONV_TAC (TOP_DEPTH_CONV FUN_EQ_CONV) 1808 THEN REPEAT GEN_TAC 1809 THEN EQ_TAC 1810 THENL 1811 [ REWRITE_TAC[TC_REDL_IMP_RED_BETA], 1812 1813 REWRITE_TAC[GSYM TC_RC_RED1_IS_RED] 1814 THEN MATCH_MP_TAC TC_MONOTONIC 1815 THEN REWRITE_TAC[RC_RED1_BETA_IMP_REDL] 1816 ] 1817 ); 1818 1819 1820(* The Church-Rosser Theorem! 1821 Barendregt Theorem 3.2.8 (i) 1822*) 1823 1824val BETA_R_CHURCH_ROSSER = store_thm 1825 ("BETA_R_CHURCH_ROSSER", 1826 ���CHURCH_ROSSER (BETA_R:^term_rel)���, 1827 REWRITE_TAC[CHURCH_ROSSER] 1828 THEN REWRITE_TAC[GSYM TC_REDL_IS_RED_BETA] 1829 THEN REPEAT CONJ_TAC 1830 THEN MATCH_MP_TAC TC_DIAMOND 1831 THEN REWRITE_TAC[REDL_DIAMOND] 1832 ); 1833(* Soli Deo Gloria!!! To God Alone Be The Glory!!! *) 1834 1835 1836(* Barendregt Theorem 3.2.8 (ii). *) 1837 1838val BETA_R_NORMAL_FORM_EXISTS = store_thm 1839 ("BETA_R_NORMAL_FORM_EXISTS", 1840 ���!M:^term N. REQUAL BETA_R M N ==> 1841 (?Z. RED BETA_R M Z /\ RED BETA_R N Z)���, 1842 MATCH_MP_TAC NORMAL_FORM_EXISTS 1843 THEN REWRITE_TAC[BETA_R_CHURCH_ROSSER] 1844 ); 1845 1846(* Barendregt Corollary 3.2.9 (i). *) 1847 1848val BETA_R_NORMAL_FORM_REDUCED_TO = store_thm 1849 ("BETA_R_NORMAL_FORM_REDUCED_TO", 1850 ���!M:^term N. NORMAL_FORM_OF BETA_R N M ==> 1851 RED BETA_R M N���, 1852 MATCH_MP_TAC NORMAL_FORM_REDUCED_TO 1853 THEN REWRITE_TAC[BETA_R_CHURCH_ROSSER] 1854 ); 1855 1856(* Barendregt Corollary 3.2.9 (ii). *) 1857 1858val BETA_R_NORMAL_FORM_UNIQUE = store_thm 1859 ("BETA_R_NORMAL_FORM_UNIQUE", 1860 ���!M:^term N1 N2. NORMAL_FORM_OF BETA_R N1 M /\ 1861 NORMAL_FORM_OF BETA_R N2 M ==> (N1 = N2)���, 1862 MATCH_MP_TAC NORMAL_FORM_UNIQUE 1863 THEN REWRITE_TAC[BETA_R_CHURCH_ROSSER] 1864 ); 1865 1866 1867val _ = export_theory(); 1868 1869val _ = print_theory_to_file "-" "beta.lst"; 1870 1871val _ = html_theory "beta"; 1872 1873val _ = print_theory_size(); 1874