1228731Smavopen HolKernel Parse boolLib; 2247463Smavinfix THEN THENL THENC ORELSE ORELSEC THEN_TCL ORELSE_TCL ## |->; 3228731Smavinfixr -->; 4228731Smav 5228731Smav 6228731Smav 7228731Smavval _ = new_theory "eta"; 8228731Smav 9228731Smav 10228731Smav(* In interactive sessions, do: 11228731Smav 12228731Smavapp load ["pairTheory", 13228731Smav "listTheory", "listLib", "numTheory", "numLib", 14228731Smav "pred_setTheory", "pred_setLib", 15228731Smav "MutualIndThen", "bossLib", "relationTheory", 16228731Smav "ind_rel", "dep_rewrite", "quotient", 17228731Smav "more_listTheory", "more_setTheory", "variableTheory", 18228731Smav "termTheory", "alphaTheory", "liftTheory", 19228731Smav "barendregt", "reductionTheory", "betaTheory" 20228731Smav ]; 21228731Smav 22228731Smav*) 23228731Smav 24228731Smavopen prim_recTheory pairTheory listTheory rich_listTheory; 25228731Smavopen combinTheory; 26228731Smavopen listLib; 27266347Sianopen pred_setTheory pred_setLib; 28228731Smavopen numTheory; 29228731Smavopen numLib; 30228731Smavopen arithmeticTheory; 31228731Smavopen bossLib; 32228731Smavopen relationTheory; 33228731Smavopen Mutual; 34228731Smavopen ind_rel; 35228731Smavopen dep_rewrite; 36228731Smavopen quotient; 37228731Smavopen more_listTheory; 38228731Smavopen more_setTheory; 39247463Smavopen variableTheory; 40228731Smavopen termTheory; 41228731Smavopen alphaTheory; 42228731Smavopen liftTheory; 43228731Smavopen barendregt; 44228731Smavopen reductionTheory; 45228731Smavopen betaTheory; 46228731Smav 47228731Smav 48228731Smavopen tactics; 49228731Smav 50228731Smav 51228731Smavval term = ty_antiq ( ==`:'a term`== ); 52228731Smavval subs = ty_antiq ( ==`:(var # 'a term) list`== ); 53228731Smavval term_rel = ty_antiq ( ==`:'a term -> 'a term -> bool`== ); 54228731Smav 55231564Sed 56247463Smav(* Reflexive closure of a relation. *) 57247463Smav(* copied from relationScript.sml: *) 58228731Smav 59228731Smavval RC_INDUCT_TAC = 60228731Smav let val rc_thm = RC_INDUCT 61228731Smav fun tac (asl,w) = 62228731Smav let open Rsyntax 63228731Smav val {Bvar=u,Body} = dest_forall w 64228731Smav val {Bvar=v,Body} = dest_forall Body 65228731Smav val {ant,conseq} = dest_imp Body 66228731Smav val (RC,Ru'v') = strip_comb ant 67228731Smav val R = hd Ru'v' 68228731Smav val u'v' = tl Ru'v' 69228731Smav val u' = hd u'v' 70228731Smav val v' = hd (tl u'v') 71266347Sian (*val (RC,[R,u',v']) = strip_comb ant*) 72266347Sian (*val {Name = "RC",...} = dest_const RC*) 73228731Smav val _ = if #Name(dest_const RC) = "RC" then true else raise Match 74228731Smav val _ = assert (aconv u) u' 75228731Smav val _ = assert (aconv v) v' 76228731Smav val P = list_mk_abs([u,v], conseq) 77228731Smav val rc_thm' = BETA_RULE(ISPEC P (ISPEC R rc_thm)) 78228731Smav in MATCH_MP_TAC rc_thm' (asl,w) 79228731Smav end 80247463Smav handle _ => raise HOL_ERR{origin_structure = "<top-level>", 81228731Smav origin_function = "RC_INDUCT_TAC", 82228731Smav message = "Unanticipated term structure"} 83228731Smav in tac 84228731Smav end; 85228731Smav 86228731Smav(* Also see RC_REFLEXIVE, RC_SUBSET, RC_INDUCT, RC_CASES. *) 87228731Smav 88228731Smav 89228731Smav(* Define the transitive closure of a relation. *) 90228731Smav(* Wait, it's already done: see file src/relation/relationScript.sml. *) 91235373Sgjb(* This defines TC in the logic as TC R is the transitive closure of R, *) 92228731Smav(* and "transitive R" as the property that R is transitite on 'a. *) 93228731Smav(* There are also a bunch of theorems in structure TCScript, as well as *) 94228731Smav(* induction tactics, cases theorems, etc. It's theory "TC". *) 95228731Smav 96228731Smav(* copied: *) 97228731Smav 98228731Smavval TC_INDUCT_TAC = 99228731Smav let val tc_thm = TC_INDUCT 100228731Smav fun tac (asl,w) = 101228731Smav let open Rsyntax 102228731Smav val {Bvar=u,Body} = dest_forall w 103228731Smav val {Bvar=v,Body} = dest_forall Body 104228731Smav val {ant,conseq} = dest_imp Body 105228731Smav val (TC,Ru'v') = strip_comb ant 106228731Smav val R = hd Ru'v' 107228731Smav val u'v' = tl Ru'v' 108228731Smav val u' = hd u'v' 109228731Smav val v' = hd (tl u'v') 110228731Smav (*val (TC,[R,u',v']) = strip_comb ant*) 111228731Smav (*val {Name = "TC",...} = dest_const TC*) 112235373Sgjb val _ = if #Name(dest_const TC) = "TC" then true else raise Match 113228731Smav val _ = assert (aconv u) u' 114228731Smav val _ = assert (aconv v) v' 115228731Smav val P = list_mk_abs([u,v], conseq) 116228731Smav val tc_thm' = BETA_RULE(ISPEC P (ISPEC R tc_thm)) 117228731Smav in MATCH_MP_TAC tc_thm' (asl,w) 118228731Smav end 119228731Smav handle _ => raise HOL_ERR{origin_structure = "<top-level>", 120228731Smav origin_function = "TC_INDUCT_TAC", 121228731Smav message = "Unanticipated term structure"} 122228731Smav in tac 123228731Smav end; 124228731Smav 125228731Smavval TC_TRANS = REWRITE_RULE[transitive_def] TC_TRANSITIVE; 126228731Smav(* Also see TC_SUBSET, TC_CASES1, TC_CASES2, TC_RC_RED1_IS_RED, TC_MONOTONIC *) 127228731Smav 128228731Smav 129228731Smav 130228731Smav(* --------------------------------------------------------------------- *) 131228731Smav(* Definition of the relation of eta reduction. *) 132228731Smav(* This is simple, but we define it by rule induction. *) 133228731Smav(* --------------------------------------------------------------------- *) 134228731Smav 135228731Smav(* --------------------------------------------------------------------- *) 136228731Smav(* (ETA_R t1 t2) means that the term t1 reduces entirely to the term t2 *) 137228731Smav(* in exactly one eta-reduction step, as defined in Barendregt, *) 138228731Smav(* Section 3.3.1, page 63. Note that this is true ONLY on t1 of *) 139228731Smav(* the form (Lam x (App t (Var x))). *) 140228731Smav(* --------------------------------------------------------------------- *) 141228731Smav 142228731Smav 143228731Smavval ETA_R = 144228731Smav���ETA_R : ^term_rel���; 145228731Smav 146228731Smavval ETA_R_patterns = [���^ETA_R t1 t2���]; 147228731Smav 148228731Smavval ETA_R_rules_tm = 149228731Smav��� (~(x IN FV t) 150228731Smav (* -------------------------------------------- *) ==> 151228731Smav (^ETA_R (Lam x (App t (Var x))) t)) 152228731Smav���; 153228731Smav 154228731Smavval (ETA_R_rules_sat,ETA_R_ind_thm) = 155228731Smav define_inductive_relations ETA_R_patterns ETA_R_rules_tm; 156228731Smav 157228731Smavval ETA_R_inv_thms = prove_inversion_theorems 158228731Smav ETA_R_rules_sat ETA_R_ind_thm; 159228731Smav 160228731Smavval ETA_R_strong_ind = prove_strong_induction 161228731Smav ETA_R_rules_sat ETA_R_ind_thm; 162228731Smav 163228731Smavval _ = save_thm ("ETA_R_rules_sat", ETA_R_rules_sat); 164228731Smavval _ = save_thm ("ETA_R_ind_thm", ETA_R_ind_thm); 165228731Smavval _ = save_thm ("ETA_R_inv_thms", LIST_CONJ ETA_R_inv_thms); 166228731Smavval _ = save_thm ("ETA_R_strong_ind", ETA_R_strong_ind); 167228731Smav 168228731Smav 169228731Smav 170228731Smav 171228731Smav(* --------------------------------------------------------------------- *) 172228731Smav(* We claim that ETA_R is a binary relation on the lambda calculus *) 173228731Smav(* language which is *) 174228731Smav(* 1) a notion of reduction on the sigma calculus, in the sense of *) 175228731Smav(* Berendregt, Definition 3.1.2, pg 51 (trivial, since a relation) *) 176228731Smav(* 2) deterministic *) 177228731Smav(* --------------------------------------------------------------------- *) 178228731Smav 179228731Smav 180228731Smav(* ETA_R is a deterministic relation. *) 181266347Sian 182266347Sianval ETA_R_deterministic = store_thm 183266347Sian ("ETA_R_deterministic", 184266347Sian ���!t:^term u1 u2. 185266347Sian ETA_R t u1 /\ ETA_R t u2 ==> (u1 = u2)���, 186266347Sian REWRITE_TAC ETA_R_inv_thms 187266347Sian THEN REPEAT STRIP_TAC 188266347Sian THEN UNDISCH_TAC ``(t:^term) = Lam x' (App u2 (Var x'))`` 189266347Sian THEN ASM_REWRITE_TAC[] 190266347Sian THEN REWRITE_TAC[Lam_one_one] 191266347Sian THEN REWRITE_TAC[SUB_term] 192266347Sian THEN REWRITE_TAC[SUB] 193266347Sian THEN REWRITE_TAC[term_one_one] 194266347Sian THEN REWRITE_TAC[GSYM Lam_one_one] 195266347Sian THEN STRIP_TAC 196228731Smav THEN IMP_RES_TAC SUB_RENAME_TERM 197228731Smav THEN POP_ASSUM (MP_TAC o SPEC ���Var x:^term���) 198228731Smav THEN IMP_RES_THEN REWRITE_THM subst_EMPTY 199228731Smav ); 200228731Smav 201228731Smav(* Note that ETA_R is not reflexive, symmetric, or transitive. *) 202228731Smav 203228731Smav(* ETA_R is monotonically decreasing with respect to free variables. *) 204228731Smav 205228731Smavval ETA_FV = store_thm 206228731Smav ("ETA_FV", 207228731Smav ���!t1:^term t2. ETA_R t1 t2 ==> 208228731Smav (FV t2 SUBSET FV t1)���, 209228731Smav rule_induct ETA_R_strong_ind 210228731Smav THEN REWRITE_TAC[FV_term] 211228731Smav THEN REPEAT STRIP_TAC 212228731Smav THEN REWRITE_TAC[SUBSET_DEF] 213228731Smav THEN REPEAT STRIP_TAC 214228731Smav THEN IMP_RES_TAC IN_NOT_IN 215228731Smav THEN REWRITE_TAC[IN_UNION,IN_DIFF] 216228731Smav THEN ASM_REWRITE_TAC[IN] 217228731Smav ); 218228731Smav 219228731Smav 220228731Smav 221228731Smav(* --------------------------------------------------------------- *) 222228731Smav(* If substituting one variable for another across a term does not *) 223228731Smav(* change the term, then either the variables were the same, or *) 224228731Smav(* the substitution never happened because the target variable did *) 225228731Smav(* not appear free in the term. *) 226228731Smav(* --------------------------------------------------------------- *) 227228731Smav 228228731Smavval SUBST_IS_SAME = store_thm 229228731Smav ("SUBST_IS_SAME", 230228731Smav ���!t:^term x y. ((t <[ [x,Var y]) = t) ==> 231228731Smav ((x = y) \/ ~(x IN FV t))���, 232228731Smav MUTUAL_INDUCT_THEN term_height_induct ASSUME_TAC 233233648Seadler THEN REPEAT GEN_TAC 234228731Smav THENL (* 4 subgoals *) 235228731Smav [ REWRITE_TAC[SUB_term,term_one_one,FV_term,IN], 236228731Smav 237228731Smav REWRITE_TAC[SUB_term,SUB] 238228731Smav THEN COND_CASES_TAC 239228731Smav THENL 240228731Smav [ REWRITE_TAC[term_one_one] 241228731Smav THEN DISCH_TAC 242228731Smav THEN ASM_REWRITE_TAC[], 243228731Smav 244228731Smav REWRITE_TAC[FV_term,IN] 245228731Smav THEN FIRST_ASSUM (REWRITE_THM o GSYM) 246228731Smav ], 247228731Smav 248228731Smav REWRITE_TAC[SUB_term,term_one_one,FV_term,IN_UNION] 249228731Smav THEN STRIP_TAC 250228731Smav THEN RES_TAC 251228731Smav THEN ASM_REWRITE_TAC[], 252228731Smav 253228731Smav SIMPLE_SUBST_TAC 254 THEN REWRITE_TAC[term_one_one,FV_term,IN_DIFF,IN] 255 THEN REWRITE_TAC[GSYM (ASSUME ���~((z:var) = x')���)] 256 THEN STRIP_TAC 257 THEN RES_TAC 258 THEN ASM_REWRITE_TAC[] 259 ] 260 ); 261 262 263(* -------------------------------------------------------------------- *) 264(* The following is remarkably simple, given that Lam x u = Lam x' u' *) 265(* for many choices of x', u'. *) 266(* -------------------------------------------------------------------- *) 267 268val ETA_R_equals = store_thm 269 ("ETA_R_equals", 270 ���(!x t:^term. ETA_R (Var x) t = F) /\ 271 (!t u t':^term. ETA_R (App t u) t' = F) /\ 272 (!x u t:^term. ETA_R (Lam x u) t = 273 ~(x IN FV t) /\ (u = App t (Var x)))���, 274 REWRITE_TAC ETA_R_inv_thms 275 THEN REWRITE_TAC[term_distinct,term_one_one] 276 THEN REPEAT STRIP_TAC 277 THEN EQ_TAC 278 THEN STRIP_TAC 279 THENL 280 [ IMP_RES_TAC Lam_one_one 281 THEN POP_ASSUM (REWRITE_ALL_THM o SYM) 282 THEN UNDISCH_LAST_TAC 283 THEN REWRITE_TAC[SUB_term] 284 THEN IMP_RES_THEN REWRITE_THM subst_EMPTY 285 THEN REWRITE_TAC[SUB_term,SUB] 286 THEN REWRITE_TAC[term_one_one] 287 THEN DISCH_TAC 288 THEN IMP_RES_TAC SUBST_IS_SAME 289 THEN ASM_REWRITE_TAC[], 290 291 EXISTS_TAC ���x:var��� 292 THEN ASM_REWRITE_TAC[] 293 ] 294 ); 295 296 297(* --------------------------------------------------------------------- *) 298(* Now we claim that using the results of theory "reduction", that *) 299(* 1) RED1 ETA_R, RED ETA_R, and REQ ETA_R are compatible, *) 300(* 2) RED ETA_R is a reduction relation, *) 301(* 3) REQ ETA_R is an equality relation, *) 302(* 4) various theorems and relations hold (see the theory "reduction") *) 303(* --------------------------------------------------------------------- *) 304 305 306(* --------------------------------------------------------------------- *) 307(* Now we begin to prove the Church-Rosser theorem for ETA_R. *) 308(* --------------------------------------------------------------------- *) 309 310 311(* Barendregt Proposition 3.3.3, ETA_R is substitutive. *) 312 313val ETA_R_SUBSTITUTIVE = store_thm 314 ("ETA_R_SUBSTITUTIVE", 315 ���SUBSTITUTIVE (ETA_R:^term_rel)���, 316 REWRITE_TAC[SUBSTITUTIVE] 317 THEN REPEAT GEN_TAC 318 THEN DISCH_THEN (STRIP_ASSUME_TAC o REWRITE_RULE ETA_R_inv_thms) 319 THEN ASM_REWRITE_TAC[] 320 THEN DEFINE_NEW_VAR ���(Nx:^term) = App N (Var x')��� 321 THEN FIRST_ASSUM (REWRITE_THM o SYM) 322 THEN SIMPLE_SUBST_TAC 323 THEN REWRITE_TAC[ETA_R_equals] 324 THEN REWRITE_TAC[FV_term_subst] 325 THEN DEP_REWRITE_TAC[NOT_IN_FV_subst] 326 THEN ASM_REWRITE_TAC[] 327 THEN IMP_RES_TAC Lam_one_one 328 THEN POP_TAC 329 THEN POP_ASSUM (REWRITE_THM o GSYM) 330 THEN ASM_REWRITE_TAC[SUB_term,SUB] 331 THEN REWRITE_TAC[term_one_one] 332 THEN IMP_RES_THEN REWRITE_THM subst_EMPTY 333 ); 334 335(* --------------------------------------------------------------- *) 336(* Much of the following development could be moved to the theory *) 337(* "reduction", as it is general for all notions of reduction. *) 338(* --------------------------------------------------------------- *) 339 340(* ----------------------------------------------------- *) 341(* We define what it means for two relations to commute. *) 342(* ----------------------------------------------------- *) 343 344val COMMUTE = 345 new_infixl_definition 346 ("COMMUTE", 347 ���$COMMUTE R1 R2 = 348 (!a b c:'a. R1 a b /\ R2 a c ==> (?d. R2 b d /\ R1 c d))���, 349 250); 350 351(* Define the infix substitution operator, <[, with higher precedence *) 352(* than the substitution-creation operator //, but lower than CONS: *) 353 354val _ = add_infix("<=>",250,LEFT); 355 356(* Now overload the operator <=> to refer to COMMUTE: *) 357 358val _ = overload_on("<=>", 359 ���$COMMUTE:('a->'a->bool)->('a->'a->bool)->bool���) 360handle e => (Raise e); 361 362 363(* Now R |= <> iff R <=> R. *) 364 365val DIAMOND_COMMUTES_SELF = store_thm 366 ("DIAMOND_COMMUTES_SELF", 367 ���!R:'a->'a->bool. DIAMOND R = R <=> R���, 368 REWRITE_TAC[DIAMOND,COMMUTE] 369 ); 370 371 372(* ------------------------------------- *) 373(* We define the union of two relations. *) 374(* ------------------------------------- *) 375 376val UNION_R = 377 new_infixl_definition 378 ("UNION_R", 379 ���$UNION_R R1 R2 = 380 (\(a:'a) (b:'b). R1 a b \/ R2 a b)���, 381 500); 382 383val IN_UNION_R = store_thm 384 ("IN_UNION_R", 385 ���!(R1:'a->'b->bool) R2 x y. (R1 UNION_R R2) x y = R1 x y \/ R2 x y���, 386 REWRITE_TAC[UNION_R] 387 THEN BETA_TAC 388 THEN REWRITE_TAC[] 389 ); 390 391 392(* --------------------------------------------------------- *) 393(* We prove the Hindley-Rosen Lemma on the Diamond property. *) 394(* --------------------------------------------------------- *) 395 396val DIAMOND_TC_UNION1 = TAC_PROOF(([], 397 ���!R1 R2 (a:'a) b. TC (R1 UNION_R R2) a b ==> 398 (DIAMOND R1 /\ DIAMOND R2 /\ (R1 <=> R2) ==> 399 (!c. (R1 UNION_R R2) a c ==> 400 (?d. (R1 UNION_R R2) b d /\ TC (R1 UNION_R R2) c d)))���), 401 GEN_TAC 402 THEN GEN_TAC 403 THEN TC_INDUCT_TAC 404 THEN CONJ_TAC 405 THENL 406 [ REWRITE_TAC[IN_UNION_R] 407 THEN REPEAT STRIP_TAC 408 THEN REWRITE_ALL_TAC[DIAMOND,COMMUTE] 409 THEN RES_TAC 410 THEN EXISTS_TAC ���d':'a��� 411 THEN ASM_REWRITE_TAC[] 412 THEN MATCH_MP_TAC TC_SUBSET 413 THEN REWRITE_TAC[IN_UNION_R] 414 THEN ASM_REWRITE_TAC[], 415 416 REPEAT GEN_TAC 417 THEN STRIP_TAC 418 THEN DISCH_THEN REWRITE_ALL_THM 419 THEN GEN_TAC 420 THEN DISCH_TAC 421 THEN RES_TAC 422 THEN RES_TAC 423 THEN EXISTS_TAC ���d':'a��� 424 THEN ASM_REWRITE_TAC[] 425 THEN IMP_RES_TAC TC_TRANS 426 ] 427 ); 428 429val DIAMOND_TC_UNION2 = TAC_PROOF(([], 430 ���!R1 R2 (a:'a) b. TC (R1 UNION_R R2) a b ==> 431 (DIAMOND R1 /\ DIAMOND R2 /\ (R1 <=> R2) ==> 432 (!c. TC (R1 UNION_R R2) a c ==> 433 (?d. TC (R1 UNION_R R2) b d /\ TC (R1 UNION_R R2) c d)))���), 434 GEN_TAC 435 THEN GEN_TAC 436 THEN TC_INDUCT_TAC 437 THEN CONJ_TAC 438 THENL 439 [ REPEAT STRIP_TAC 440 THEN IMP_RES_TAC DIAMOND_TC_UNION1 441 THEN EXISTS_TAC ���d:'a��� 442 THEN ASM_REWRITE_TAC[] 443 THEN IMP_RES_TAC TC_SUBSET, 444 445 REPEAT GEN_TAC 446 THEN STRIP_TAC 447 THEN DISCH_THEN REWRITE_ALL_THM 448 THEN GEN_TAC 449 THEN DISCH_TAC 450 THEN RES_TAC 451 THEN RES_TAC 452 THEN EXISTS_TAC ���d':'a��� 453 THEN ASM_REWRITE_TAC[] 454 THEN IMP_RES_TAC TC_TRANS 455 ] 456 ); 457 458(* -------------------------------------------- *) 459(* Hindley-Rosen Lemma on the Diamond property. *) 460(* Barendregt Proposition 3.3.5(i) (page 64): *) 461(* -------------------------------------------- *) 462 463val DIAMOND_TC_UNION = store_thm 464 ("DIAMOND_TC_UNION", 465 ���!(R1:'a->'a->bool) R2. 466 DIAMOND R1 /\ DIAMOND R2 /\ (R1 <=> R2) ==> 467 DIAMOND (TC (R1 UNION_R R2))���, 468 REPEAT STRIP_TAC 469 THEN REWRITE_TAC[DIAMOND] 470 THEN REPEAT STRIP_TAC 471 THEN IMP_RES_TAC DIAMOND_TC_UNION2 472 THEN EXISTS_TAC ``d'':'a`` 473 THEN ASM_REWRITE_TAC[] 474 ); 475 476 477val RED1_COMPAT = REWRITE_RULE[compatible] RED1_compatible; 478 479 480(* -------------------------------------------------------------- *) 481(* We now prove that the reduction based on a notion which is the *) 482(* union of two notions of reduction, is itself a union of the *) 483(* reductions of the two notions. *) 484(* -------------------------------------------------------------- *) 485 486val RED1_UNION1 = TAC_PROOF(([], 487 ���!R1 R2 R t1:^term t2. 488 RED1 R t1 t2 ==> 489 (R = R1 UNION_R R2) ==> 490 (RED1 R1 UNION_R RED1 R2) t1 t2���), 491 GEN_TAC THEN GEN_TAC 492 THEN rule_induct RED1_ind_thm 493 THEN REPEAT STRIP_TAC (* 4 subgoals *) 494 THEN POP_ASSUM REWRITE_ALL_THM 495 THEN REWRITE_ALL_TAC[IN_UNION_R] 496 THEN POP_ASSUM STRIP_ASSUME_TAC 497 THEN IMP_RES_TAC RED1_rules_sat 498 THEN ASM_REWRITE_TAC[] 499 ); 500 501val RED1_UNION2 = TAC_PROOF(([], 502 ���!R2 R1 t1:^term t2. RED1 R1 t1 t2 ==> 503 RED1 (R1 UNION_R R2) t1 t2���), 504 GEN_TAC 505 THEN rule_induct RED1_ind_thm 506 THEN REPEAT STRIP_TAC (* 4 subgoals *) 507 THENL 508 [ DEP_REWRITE_TAC[RED1_rules_sat] 509 THEN ASM_REWRITE_TAC[IN_UNION_R], 510 511 IMP_RES_TAC RED1_rules_sat 512 THEN ASM_REWRITE_TAC[], 513 514 IMP_RES_TAC RED1_rules_sat 515 THEN ASM_REWRITE_TAC[], 516 517 IMP_RES_TAC RED1_rules_sat 518 THEN ASM_REWRITE_TAC[] 519 ] 520 ); 521 522val RED1_UNION3 = TAC_PROOF(([], 523 ���!R1 R2 t1:^term t2. RED1 R2 t1 t2 ==> 524 RED1 (R1 UNION_R R2) t1 t2���), 525 GEN_TAC 526 THEN rule_induct RED1_ind_thm 527 THEN REPEAT STRIP_TAC (* 4 subgoals *) 528 THENL 529 [ DEP_REWRITE_TAC[RED1_rules_sat] 530 THEN ASM_REWRITE_TAC[IN_UNION_R], 531 532 IMP_RES_TAC RED1_rules_sat 533 THEN ASM_REWRITE_TAC[], 534 535 IMP_RES_TAC RED1_rules_sat 536 THEN ASM_REWRITE_TAC[], 537 538 IMP_RES_TAC RED1_rules_sat 539 THEN ASM_REWRITE_TAC[] 540 ] 541 ); 542 543val RED1_UNION = store_thm 544 ("RED1_UNION", 545 ���!R1:^term_rel R2. RED1 (R1 UNION_R R2) = (RED1 R1 UNION_R RED1 R2)���, 546 CONV_TAC (TOP_DEPTH_CONV FUN_EQ_CONV) 547 THEN REPEAT GEN_TAC 548 THEN EQ_TAC 549 THEN REPEAT STRIP_TAC 550 THENL 551 [ MATCH_MP_TAC (IMP2AND RED1_UNION1) 552 THEN EXISTS_TAC ���(R1:^term_rel) UNION_R R2��� 553 THEN ASM_REWRITE_TAC[], 554 555 POP_ASSUM (STRIP_ASSUME_TAC o REWRITE_RULE[IN_UNION_R]) 556 THENL 557 [ MATCH_MP_TAC RED1_UNION2, 558 MATCH_MP_TAC RED1_UNION3 559 ] 560 THEN FIRST_ASSUM ACCEPT_TAC 561 ] 562 ); 563 564(* --------------------------------------------------------------------- *) 565(* The above was for one-step reduction, RED1. We now prove the *) 566(* corresponding property for the reflexive, transitive closure, RED. *) 567(* --------------------------------------------------------------------- *) 568 569val RED_UNION1 = TAC_PROOF(([], 570 ���!R1 R2 R t1:^term t2. RED R t1 t2 ==> 571 (R = R1 UNION_R R2) ==> 572 TC (RED R1 UNION_R RED R2) t1 t2���), 573 GEN_TAC THEN GEN_TAC 574 THEN rule_induct RED_ind_thm 575 THEN REPEAT STRIP_TAC (* 3 subgoals *) 576 THEN POP_ASSUM REWRITE_ALL_THM 577 THENL 578 [ MATCH_MP_TAC TC_SUBSET 579 THEN REWRITE_ALL_TAC[RED1_UNION] 580 THEN REWRITE_ALL_TAC[IN_UNION_R] 581 THEN POP_ASSUM STRIP_ASSUME_TAC 582 THEN IMP_RES_TAC RED_rules_sat 583 THEN ASM_REWRITE_TAC[], 584 585 MATCH_MP_TAC TC_SUBSET 586 THEN REWRITE_TAC[IN_UNION_R] 587 THEN REWRITE_TAC[RED_rules_sat], 588 589 IMP_RES_TAC TC_TRANS 590 ] 591 ); 592 593val RED_UNION2 = TAC_PROOF(([], 594 ���!R2 R1 t1:^term t2. RED R1 t1 t2 ==> 595 RED (R1 UNION_R R2) t1 t2���), 596 GEN_TAC 597 THEN rule_induct RED_ind_thm 598 THEN REPEAT STRIP_TAC (* 3 subgoals *) 599 THENL 600 [ DEP_REWRITE_TAC[RED_rules_sat] 601 THEN REWRITE_TAC[RED1_UNION] 602 THEN ASM_REWRITE_TAC[IN_UNION_R], 603 604 REWRITE_TAC[RED_rules_sat], 605 606 IMP_RES_TAC RED_rules_sat 607 ] 608 ); 609 610val RED_UNION3 = TAC_PROOF(([], 611 ���!R1 R2 t1:^term t2. RED R2 t1 t2 ==> 612 RED (R1 UNION_R R2) t1 t2���), 613 GEN_TAC 614 THEN rule_induct RED_ind_thm 615 THEN REPEAT STRIP_TAC (* 3 subgoals *) 616 THENL 617 [ DEP_REWRITE_TAC[RED_rules_sat] 618 THEN REWRITE_TAC[RED1_UNION] 619 THEN ASM_REWRITE_TAC[IN_UNION_R], 620 621 REWRITE_TAC[RED_rules_sat], 622 623 IMP_RES_TAC RED_rules_sat 624 ] 625 ); 626 627val RED_UNION4 = TAC_PROOF(([], 628 ���!R1 R2 t1:^term t2. TC (RED R1 UNION_R RED R2) t1 t2 ==> 629 RED (R1 UNION_R R2) t1 t2���), 630 GEN_TAC 631 THEN GEN_TAC 632 THEN TC_INDUCT_TAC 633 THEN CONJ_TAC 634 THENL 635 [ REWRITE_TAC[IN_UNION_R] 636 THEN REPEAT STRIP_TAC 637 THENL 638 [ MATCH_MP_TAC RED_UNION2, 639 MATCH_MP_TAC RED_UNION3 640 ] 641 THEN FIRST_ASSUM ACCEPT_TAC, 642 643 REPEAT STRIP_TAC 644 THEN IMP_RES_TAC RED_rules_sat 645 ] 646 ); 647 648(* Remark of Barendregt at bottom of page 64. *) 649 650val RED_UNION = store_thm 651 ("RED_UNION", 652 ���!R1:^term_rel R2. RED (R1 UNION_R R2) = TC (RED R1 UNION_R RED R2)���, 653 CONV_TAC (TOP_DEPTH_CONV FUN_EQ_CONV) 654 THEN REPEAT GEN_TAC 655 THEN EQ_TAC 656 THEN REPEAT STRIP_TAC 657 THENL 658 [ IMP_RES_TAC RED_UNION1 659 THEN POP_ASSUM MATCH_MP_TAC 660 THEN REFL_TAC, 661 662 IMP_RES_TAC RED_UNION4 663 ] 664 ); 665 666 667(* Barendregt Proposition 3.3.5(ii) (page 64): *) 668 669val COMMUTE_CHURCH_ROSSER = store_thm 670 ("COMMUTE_CHURCH_ROSSER", 671 ���!R1:^term_rel R2. 672 CHURCH_ROSSER R1 /\ CHURCH_ROSSER R2 /\ 673 (RED R1 <=> RED R2) ==> 674 CHURCH_ROSSER (R1 UNION_R R2)���, 675 REWRITE_TAC[CHURCH_ROSSER] 676 THEN REWRITE_TAC[RED_UNION] 677 THEN REWRITE_TAC[DIAMOND_TC_UNION] 678 ); 679 680 681(* -------------------------------------------------------------- *) 682(* We now prove Barendregt's Lemma 3.3.6, as a way to prove that *) 683(* the reflexive, transitive closures of two relations commute. *) 684(* -------------------------------------------------------------- *) 685 686val COMMUTE_TC_RC1 = TAC_PROOF(([], 687 ���!R2 a b. 688 RC R2 a b ==> 689 !R1. 690 (!a b c:'a. R1 a b /\ R2 a c ==> 691 ?d. TC (RC R2) b d /\ RC R1 c d) ==> 692 (!c. R1 a c ==> 693 ?d. RC R1 b d /\ TC (RC R2) c d)���), 694 GEN_TAC 695 THEN RC_INDUCT_TAC 696 THEN REPEAT STRIP_TAC 697 THENL 698 [ RES_TAC 699 THEN EXISTS_TAC ���d:'a��� 700 THEN ASM_REWRITE_TAC[], 701 702 EXISTS_TAC ``c:'a`` 703 THEN DEP_REWRITE_TAC[TC_SUBSET] 704 THEN REWRITE_TAC[RC_REFLEXIVE] 705 THEN MATCH_MP_TAC RC_SUBSET 706 THEN ASM_REWRITE_TAC[] 707 ] 708 ); 709 710val COMMUTE_TC_RC2 = TAC_PROOF(([], 711 ���!R1 a b. 712 RC R1 a b ==> 713 !R2. 714 (!a b c:'a. R1 a b /\ R2 a c ==> 715 ?d. TC (RC R2) b d /\ RC R1 c d) ==> 716 (!c. RC R2 a c ==> 717 ?d. TC (RC R2) b d /\ RC R1 c d)���), 718 GEN_TAC 719 THEN RC_INDUCT_TAC 720 THEN REPEAT STRIP_TAC 721 THENL 722 [ IMP_RES_TAC COMMUTE_TC_RC1 723 THEN EXISTS_TAC ���d:'a��� 724 THEN ASM_REWRITE_TAC[], 725 726 EXISTS_TAC ``c:'a`` 727 THEN DEP_REWRITE_TAC[TC_SUBSET] 728 THEN ASM_REWRITE_TAC[RC_REFLEXIVE] 729 ] 730 ); 731 732val COMMUTE_TC_RC3 = TAC_PROOF(([], 733 ���!R2 a b. 734 TC (RC R2) a b ==> 735 !R1. 736 (!a b c:'a. R1 a b /\ R2 a c ==> 737 ?d. TC (RC R2) b d /\ RC R1 c d) ==> 738 (!c. RC R1 a c ==> 739 ?d. RC R1 b d /\ TC (RC R2) c d)���), 740 GEN_TAC 741 THEN TC_INDUCT_TAC 742 THEN REPEAT STRIP_TAC 743 THENL 744 [ IMP_RES_TAC COMMUTE_TC_RC2 745 THEN EXISTS_TAC ���d:'a��� 746 THEN ASM_REWRITE_TAC[], 747 748 RES_TAC 749 THEN RES_TAC 750 THEN EXISTS_TAC ``d':'a`` 751 THEN ASM_REWRITE_TAC[] 752 THEN IMP_RES_TAC TC_TRANS 753 ] 754 ); 755 756val COMMUTE_TC_RC4 = TAC_PROOF(([], 757 ���!R1 a b. 758 TC (RC R1) a b ==> 759 !R2. 760 (!a b c:'a. R1 a b /\ R2 a c ==> 761 ?d. TC (RC R2) b d /\ RC R1 c d) ==> 762 (!c. TC (RC R2) a c ==> 763 ?d. TC (RC R2) b d /\ TC (RC R1) c d)���), 764 GEN_TAC 765 THEN TC_INDUCT_TAC 766 THEN REPEAT STRIP_TAC 767 THENL 768 [ IMP_RES_TAC COMMUTE_TC_RC3 769 THEN EXISTS_TAC ���d:'a��� 770 THEN ASM_REWRITE_TAC[] 771 THEN MATCH_MP_TAC TC_SUBSET 772 THEN ASM_REWRITE_TAC[], 773 774 RES_TAC 775 THEN RES_TAC 776 THEN EXISTS_TAC ``d':'a`` 777 THEN ASM_REWRITE_TAC[] 778 THEN IMP_RES_TAC TC_TRANS 779 ] 780 ); 781 782(* Barendregt Lemma 3.3.6, page 65. *) 783 784val COMMUTE_TC_RC = store_thm 785 ("COMMUTE_TC_RC", 786 ���!R1 R2. 787 (!a b c:'a. R1 a b /\ R2 a c ==> 788 ?d. TC (RC R2) b d /\ RC R1 c d) ==> 789 (TC (RC R1) <=> TC (RC R2))���, 790 REWRITE_TAC[COMMUTE] 791 THEN REPEAT STRIP_TAC 792 THEN IMP_RES_TAC COMMUTE_TC_RC4 793 THEN EXISTS_TAC ���d:'a��� 794 THEN ASM_REWRITE_TAC[] 795 ); 796 797 798val RED1_ETA_FV = MATCH_MP RED1_FV ETA_FV; 799val RED1_BETA_FV = MATCH_MP RED1_FV BETA_FV; 800 801 802val RED1_ETA_RENAME = store_thm 803 ("RED1_ETA_RENAME", 804 ���!t1:^term t2 t1' x y. 805 RED1 ETA_R t1 t2 /\ (Lam x t1 = Lam y t1') ==> 806 (Lam x t2 = Lam y (t2 <[ [x, Var y]))���, 807 REPEAT STRIP_TAC 808 THEN IMP_RES_TAC RED1_ETA_FV 809 THEN IMP_RES_TAC LAMBDA_RENAME 810 ); 811 812 813val [RED1_R, RED1_App1, RED1_App2, RED1_Lam] = CONJUNCTS RED1_rules_sat; 814 815val RED1_ETA_SUBSTITUTIVE = REWRITE_RULE[SUBSTITUTIVE] 816 (MATCH_MP RED1_SUBSTITUTIVE ETA_R_SUBSTITUTIVE); 817 818(* This is necessary for when we change a bound variable: *) 819 820val RED1_ETA_CHANGE_VAR = store_thm 821 ("RED1_ETA_CHANGE_VAR", 822 ���!t1:^term t2 x y t1'. 823 RED1 ETA_R t1 t2 /\ (Lam x t1 = Lam y t1') ==> 824 RED1 ETA_R t1' (t2 <[ [x, Var y])���, 825 REPEAT STRIP_TAC 826 THEN IMP_RES_THEN REWRITE_THM Lam_one_one_RENAME 827 THEN MATCH_MP_TAC RED1_ETA_SUBSTITUTIVE 828 THEN ASM_REWRITE_TAC[] 829 ); 830 831 832val RED1_ETA_cases = store_thm 833 ("RED1_ETA_cases", 834 ���(!a t2:^term. 835 RED1 ETA_R (Con a) t2 ==> F) /\ 836 (!x t2:^term. 837 RED1 ETA_R (Var x) t2 ==> F) /\ 838 (!t u t2:^term. 839 RED1 ETA_R (App t u) t2 ==> 840 ((?t'. RED1 ETA_R t t' /\ (t2 = App t' u)) \/ 841 (?u'. RED1 ETA_R u u' /\ (t2 = App t u')))) /\ 842 (!x t t2:^term. 843 RED1 ETA_R (Lam x t) t2 ==> 844 ((~(x IN FV t2) /\ (t = App t2 (Var x)))) \/ 845 (?t'. RED1 ETA_R t t' /\ (t2 = Lam x t')))���, 846 REPEAT CONJ_TAC 847 THEN REPEAT GEN_TAC THEN DISCH_THEN (STRIP_ASSUME_TAC o 848 REWRITE_RULE[term_distinct,term_one_one] o 849 ONCE_REWRITE_RULE[RED1_inv_thms]) 850 THENL (* 7 subgoals *) 851 [ UNDISCH_LAST_TAC 852 THEN REWRITE_TAC ETA_R_inv_thms 853 THEN REWRITE_TAC[term_distinct], 854 855 UNDISCH_LAST_TAC 856 THEN REWRITE_TAC ETA_R_inv_thms 857 THEN REWRITE_TAC[term_distinct], 858 859 UNDISCH_LAST_TAC 860 THEN REWRITE_TAC ETA_R_inv_thms 861 THEN REWRITE_TAC[term_distinct], 862 863 DISJ1_TAC 864 THEN EXISTS_TAC ���t2':^term��� 865 THEN ASM_REWRITE_TAC[], 866 867 DISJ2_TAC 868 THEN EXISTS_TAC ���u2:^term��� 869 THEN ASM_REWRITE_TAC[], 870 871 IMP_RES_TAC ETA_R_equals 872 THEN ASM_REWRITE_TAC[], 873 874 DISJ2_TAC 875 THEN EXISTS_TAC ���(t2':^term) <[ [x', Var x]��� 876 THEN ASSUM_LIST (ASSUME_TAC o SYM o hd o rev) 877 THEN IMP_RES_THEN IMP_RES_TAC RED1_ETA_RENAME 878 THEN IMP_RES_TAC RED1_ETA_CHANGE_VAR 879 THEN ASM_REWRITE_TAC[] 880 ] 881 ); 882 883val [RED1_ETA_Con_case, RED1_ETA_Var_case, 884 RED1_ETA_App_case, RED1_ETA_Lam_case] 885 = CONJUNCTS RED1_ETA_cases; 886 887val RED1_ETA_App_Var_case = store_thm 888 ("RED1_ETA_App_Var_case", 889 ���!t x t2:^term. 890 RED1 ETA_R (App t (Var x)) t2 ==> 891 (?t'. RED1 ETA_R t t' /\ (t2 = App t' (Var x)))���, 892 REPEAT GEN_TAC THEN DISCH_THEN (STRIP_ASSUME_TAC o 893 REWRITE_RULE[term_distinct,term_one_one] o 894 ONCE_REWRITE_RULE[RED1_inv_thms]) 895 THENL (* 3 subgoals *) 896 [ UNDISCH_LAST_TAC 897 THEN REWRITE_TAC[ETA_R_equals], 898 899 EXISTS_TAC ���t2':^term��� 900 THEN ASM_REWRITE_TAC[], 901 902 UNDISCH_LAST_TAC 903 THEN POP_TAC 904 THEN POP_ASSUM (REWRITE_THM o SYM) 905 THEN DISCH_TAC 906 THEN IMP_RES_TAC RED1_ETA_Var_case 907 ] 908 ); 909 910 911val RC_RED1_COMPAT = REWRITE_RULE[compatible] RC_RED1_compatible; 912val TC_RC_RED1_COMPAT = REWRITE_RULE[compatible] TC_RC_RED1_compatible; 913 914 915(* RC -->eta satisfies the diamond property. *) 916 917(* Barendregt Lemma 3.3.7, page 65. *) 918 919val DIAMOND_RED1_ETA_LEMMA = store_thm 920 ("DIAMOND_RED1_ETA_LEMMA", 921 ���!R (M:^term) M1. RED1 R M M1 ==> 922 !M2. RED1 ETA_R M M2 /\ (R = ETA_R) ==> 923 ?M3. RC (RED1 ETA_R) M1 M3 /\ RC (RED1 ETA_R) M2 M3���, 924 rule_induct RED1_strong_ind 925 THEN REPEAT STRIP_TAC (* 4 subgoals *) 926 THEN POP_ASSUM REWRITE_ALL_THM 927 THENL 928 [ (* Case 1: M --> M1 is \x.Px --> P, and M=t1, M1 = P = t2. *) 929 IMP_RES_TAC (hd ETA_R_inv_thms) 930 THEN UNDISCH_LAST_TAC 931 THEN POP_ASSUM REWRITE_ALL_THM 932 THEN IMP_RES_TAC RED1_ETA_Lam_case 933 THENL 934 [ (* Case 1.1: M2 = t2 (= M1). *) 935 POP_ASSUM (REWRITE_ALL_THM o REWRITE_RULE[term_one_one]) 936 THEN STRIP_TAC 937 THEN EXISTS_TAC ``M2:^term`` 938 THEN REWRITE_TAC[RC_REFLEXIVE], 939 940 (* Case 1.2: M2 = \x.t' = \x.P'x and P --> P'. *) 941 IMP_RES_TAC RED1_ETA_App_Var_case (* t'' = P'. *) 942 THEN POP_ASSUM REWRITE_ALL_THM 943 THEN DISCH_TAC 944 THEN EXISTS_TAC ``t'':^term`` (* Take M3 = P'. *) 945 THEN DEP_REWRITE_TAC[RC_SUBSET] 946 THEN ASM_REWRITE_TAC[] 947 THEN MATCH_MP_TAC RED1_R 948 THEN MATCH_MP_TAC ETA_R_rules_sat 949 THEN IMP_RES_THEN MATCH_MP_TAC NOT_IN_SUBSET 950 THEN IMP_RES_TAC RED1_ETA_FV 951 ], 952 953 (* Case 3: M --> M1 is PZ --> P'Z and is conseq of P --> P'. *) 954 (* P = t1, Z = u, P' = t2. *) 955 IMP_RES_TAC RED1_ETA_App_case 956 THENL 957 [ (* Case 3.1: P --> P'', M2 = P''Z. P'' = t'. *) 958 POP_ASSUM REWRITE_ALL_THM 959 THEN RES_TAC 960 (* By ind. hyp, ?P'''. P' -->= P''' /\ P'' -->= P'''. 961 P''' appears as M3. *) 962 THEN EXISTS_TAC ``App M3 u:^term`` (* Take M3 = P'''Z. *) 963 THEN IMP_RES_THEN REWRITE_THM RC_RED1_COMPAT, 964 965 (* Case 3.2: Z --> Z', M2 = P'Z'. Z' = u'. *) 966 POP_ASSUM REWRITE_ALL_THM 967 THEN EXISTS_TAC ``App t2 u':^term`` (* Take M3 = P'Z'. *) 968 THEN DEP_REWRITE_TAC[RC_SUBSET] 969 THEN IMP_RES_THEN REWRITE_THM RED1_COMPAT 970 ], 971 972 (* Case 2: M --> M1 is ZP --> ZP' and is conseq of P --> P'. *) 973 (* Z = t, P = u1, P' = u2. *) 974 IMP_RES_TAC RED1_ETA_App_case 975 THENL 976 [ (* Case 2.1: Z --> Z', M2 = Z'P'. Z' = t'. *) 977 POP_ASSUM REWRITE_ALL_THM 978 THEN EXISTS_TAC ``App t' u2:^term`` (* Take M3 = Z'P'. *) 979 THEN DEP_REWRITE_TAC[RC_SUBSET] 980 THEN IMP_RES_THEN REWRITE_THM RED1_COMPAT, 981 982 (* Case 2.2: P --> P'', M2 = ZP''. P'' = u'. *) 983 POP_ASSUM REWRITE_ALL_THM 984 THEN RES_TAC 985 (* By ind. hyp, ?P'''. P' -->= P''' /\ P'' -->= P'''. 986 P''' appears as M3. *) 987 THEN EXISTS_TAC ``App t M3:^term`` (* Take M3 = ZP'''. *) 988 THEN IMP_RES_THEN REWRITE_THM RC_RED1_COMPAT 989 ], 990 991 (* Case 4: M --> M1 is \x.P --> \x.P' and is conseq of P --> P'. *) 992 (* P = t1, P' = t2. *) 993 IMP_RES_TAC RED1_ETA_Lam_case 994 THENL 995 [ (* Case 4.2: P = P0 x, P0=M2, and so M --> M2 is \x.P0 x --> P0. *) 996 POP_ASSUM REWRITE_ALL_THM 997 THEN IMP_RES_TAC RED1_ETA_App_Var_case (* t' = P0'. *) 998 THEN POP_ASSUM REWRITE_ALL_THM 999 THEN EXISTS_TAC ``t':^term`` (* Take M3 = P0'. *) 1000 THEN DEP_REWRITE_TAC[RC_SUBSET] 1001 THEN ASM_REWRITE_TAC[] 1002 THEN MATCH_MP_TAC RED1_R 1003 THEN MATCH_MP_TAC ETA_R_rules_sat 1004 THEN IMP_RES_THEN MATCH_MP_TAC NOT_IN_SUBSET 1005 THEN MATCH_MP_TAC RED1_ETA_FV 1006 THEN ASM_REWRITE_TAC[], 1007 1008 (* Case 4.1: M2 = \x.P'' with P --> P''. P'' = t'. *) 1009 POP_ASSUM REWRITE_ALL_THM 1010 THEN RES_TAC 1011 (* By ind. hyp, ?P'''. P' -->= P''' /\ P'' -->= P'''. 1012 P''' appears as M3. *) 1013 THEN EXISTS_TAC ``Lam x M3:^term`` (* Take M3 = \x.P'''. *) 1014 THEN IMP_RES_THEN REWRITE_THM RC_RED1_COMPAT 1015 ] 1016 ] 1017 ); 1018 1019val DIAMOND_RED1_ETA_LEMMA1 = 1020 REWRITE_RULE[] (SPEC ``ETA_R:^term_rel`` DIAMOND_RED1_ETA_LEMMA); 1021 1022val DIAMOND_RC_RED1_ETA1 = TAC_PROOF(([], 1023 ���!(M:^term) M1. 1024 RC (RED1 ETA_R) M M1 ==> 1025 !M2. RED1 ETA_R M M2 ==> 1026 ?M3. RC (RED1 ETA_R) M1 M3 /\ RC (RED1 ETA_R) M2 M3���), 1027 RC_INDUCT_TAC 1028 THEN REPEAT STRIP_TAC 1029 THENL 1030 [ IMP_RES_TAC DIAMOND_RED1_ETA_LEMMA1 1031 THEN EXISTS_TAC ���M3':^term��� 1032 THEN ASM_REWRITE_TAC[], 1033 1034 EXISTS_TAC ``M2:^term`` 1035 THEN REWRITE_TAC[RC_REFLEXIVE] 1036 THEN MATCH_MP_TAC RC_SUBSET 1037 THEN ASM_REWRITE_TAC[] 1038 ] 1039 ); 1040 1041val DIAMOND_RC_RED1_ETA2 = TAC_PROOF(([], 1042 ���!(M:^term) M1. 1043 RC (RED1 ETA_R) M M1 ==> 1044 !M2. RC (RED1 ETA_R) M M2 ==> 1045 ?M3. RC (RED1 ETA_R) M1 M3 /\ RC (RED1 ETA_R) M2 M3���), 1046 RC_INDUCT_TAC 1047 THEN REPEAT STRIP_TAC 1048 THENL 1049 [ IMP_RES_TAC DIAMOND_RC_RED1_ETA1 1050 THEN EXISTS_TAC ���M3:^term��� 1051 THEN ASM_REWRITE_TAC[], 1052 1053 EXISTS_TAC ``M2:^term`` 1054 THEN ASM_REWRITE_TAC[RC_REFLEXIVE] 1055 ] 1056 ); 1057 1058val DIAMOND_RC_RED1_ETA_LEMMA = store_thm 1059 ("DIAMOND_RC_RED1_ETA_LEMMA", 1060 ���!(M:^term) M1 M2. 1061 RC (RED1 ETA_R) M M1 /\ RC (RED1 ETA_R) M M2 ==> 1062 ?M3. RC (RED1 ETA_R) M1 M3 /\ RC (RED1 ETA_R) M2 M3���, 1063 REPEAT STRIP_TAC 1064 THEN IMP_RES_TAC DIAMOND_RC_RED1_ETA2 1065 THEN EXISTS_TAC ���M3':^term��� 1066 THEN ASM_REWRITE_TAC[] 1067 ); 1068 1069val DIAMOND_RC_RED1_ETA = store_thm 1070 ("DIAMOND_RC_RED1_ETA", 1071 ���DIAMOND (RC (RED1 (ETA_R:^term_rel)))���, 1072 REWRITE_TAC[DIAMOND] 1073 THEN REWRITE_TAC[DIAMOND_RC_RED1_ETA_LEMMA] 1074 ); 1075 1076 1077 1078val ETA_R_CHURCH_ROSSER = store_thm 1079 ("ETA_R_CHURCH_ROSSER", 1080 ���CHURCH_ROSSER (ETA_R:^term_rel)���, 1081 REWRITE_TAC[CHURCH_ROSSER] 1082 THEN REWRITE_TAC[GSYM TC_RC_RED1_IS_RED] 1083 THEN MATCH_MP_TAC TC_DIAMOND 1084 THEN REWRITE_TAC[DIAMOND_RC_RED1_ETA] 1085 ); 1086 1087 1088 1089val [RED_RED1, RED_REFL, RED_TRANS] 1090 = CONJUNCTS (CONV_RULE (DEPTH_CONV LEFT_IMP_EXISTS_CONV) RED_rules_sat); 1091 1092 1093val RED1_BETA_Var_case = store_thm 1094 ("RED1_BETA_Var_case", 1095 ���!x t2:^term. 1096 RED1 BETA_R (Var x) t2 ==> F���, 1097 REPEAT GEN_TAC THEN DISCH_THEN (STRIP_ASSUME_TAC o 1098 REWRITE_RULE[term_distinct,term_one_one] o 1099 ONCE_REWRITE_RULE[RED1_inv_thms]) 1100 THEN UNDISCH_ALL_TAC 1101 THEN REWRITE_TAC[BETA_R_inv_thms] 1102 THEN REWRITE_TAC[term_distinct] 1103 ); 1104 1105 1106val RED1_BETA_App_case = store_thm 1107 ("RED1_BETA_App_case", 1108 ���!(t:^term) u t2. 1109 RED1 BETA_R (App t u) t2 ==> 1110 ((?t'. RED1 BETA_R t t' /\ (t2 = App t' u)) \/ 1111 (?u'. RED1 BETA_R u u' /\ (t2 = App t u')) \/ 1112 (?x t'. (t = Lam x t') /\ (t2 = t' <[ [x,u])))���, 1113 REPEAT GEN_TAC THEN DISCH_THEN (STRIP_ASSUME_TAC o 1114 REWRITE_RULE[term_distinct,term_one_one] o 1115 ONCE_REWRITE_RULE[RED1_inv_thms]) 1116 THENL (* 3 subgoals *) 1117 [ DISJ2_TAC 1118 THEN DISJ2_TAC 1119 THEN UNDISCH_LAST_TAC 1120 THEN REWRITE_TAC[BETA_R_inv_thms] 1121 THEN REWRITE_TAC[term_one_one] 1122 THEN STRIP_TAC 1123 THEN EXISTS_TAC ``x:var`` 1124 THEN EXISTS_TAC ``u':^term`` 1125 THEN ASM_REWRITE_TAC[], 1126 1127 DISJ1_TAC 1128 THEN EXISTS_TAC ``t2':^term`` 1129 THEN ASM_REWRITE_TAC[], 1130 1131 DISJ2_TAC 1132 THEN DISJ1_TAC 1133 THEN EXISTS_TAC ``u2:^term`` 1134 THEN ASM_REWRITE_TAC[] 1135 ] 1136 ); 1137 1138 1139val TC_RC_RED1_SUBSTITUTION_REMARK = 1140 REWRITE_RULE[GSYM TC_RC_RED1_IS_RED] BARENDREGT_SUBSTITUTION_REMARK; 1141 1142 1143val RED1_BETA_COMMUTES_RED1_ETA_LEMMA1 = store_thm 1144 ("RED1_BETA_COMMUTES_RED1_ETA_LEMMA1", 1145 ���!R (M:^term) M1. 1146 RED1 R M M1 ==> !M2. BETA_R M M2 /\ (R = ETA_R) ==> 1147 ?M3. RC (RED1 BETA_R) M1 M3 /\ TC (RC (RED1 ETA_R)) M2 M3���, 1148 rule_induct RED1_height_strong_ind 1149 THEN REPEAT STRIP_TAC (* 4 subgoals *) 1150 THEN POP_ASSUM REWRITE_ALL_THM 1151 THENL 1152 [ (* Case 1: ETA M M1, BETA M M2, impossible. *) 1153 UNDISCH_ALL_TAC 1154 THEN REWRITE_TAC (BETA_R_inv_thms :: ETA_R_inv_thms) 1155 THEN STRIP_TAC 1156 THEN ASM_REWRITE_TAC[term_distinct], 1157 1158 (* Case 2: t1 -->e t2, BETA (t1 u) M2. *) 1159 IMP_RES_TAC BETA_R_inv_thms 1160 THEN POP_ASSUM REWRITE_ALL_THM 1161 THEN POP_ASSUM (REWRITE_ALL_THM o REWRITE_RULE[term_one_one]) 1162 THEN IMP_RES_TAC RED1_ETA_Lam_case 1163 THENL 1164 [ (* Case 2.1: u' = t2 x, x not in FV t2. *) 1165 POP_ASSUM REWRITE_ALL_THM 1166 THEN EXISTS_TAC ``App t2 t:^term`` (* Take M3 = P0 Q, = t2 t. *) 1167 THEN REWRITE_TAC[SUB_term,SUB] 1168 THEN IMP_RES_THEN REWRITE_THM subst_EMPTY 1169 THEN DEP_REWRITE_TAC[TC_SUBSET] 1170 THEN REWRITE_TAC[RC_REFLEXIVE], 1171 1172 (* Case 2.2: \x.u' -->e \x.t', u' -->e t', BETA ((\x.u') t) M2. *) 1173 POP_ASSUM REWRITE_ALL_THM 1174 THEN EXISTS_TAC ``(t':^term) <[ [x,t]`` (* Take M3 = P'[x:=Q]. *) 1175 THEN DEP_REWRITE_TAC[TC_SUBSET,RC_SUBSET] 1176 THEN IMP_RES_THEN REWRITE_THM 1177 (REWRITE_RULE[SUBSTITUTIVE] RED1_ETA_SUBSTITUTIVE) 1178 THEN MATCH_MP_TAC RED1_R 1179 THEN REWRITE_TAC[BETA_R_rules_sat] 1180 ], 1181 1182 (* Case 3: t' -->e u2, BETA (t u1) M2. *) 1183 IMP_RES_TAC BETA_R_inv_thms 1184 THEN POP_ASSUM REWRITE_ALL_THM 1185 THEN POP_ASSUM (REWRITE_ALL_THM o REWRITE_RULE[term_one_one]) 1186 THEN EXISTS_TAC ``(u:^term) <[ [x,u2]`` (* Take M3 = P[x:=Q']. *) 1187 THEN DEP_REWRITE_TAC[TC_RC_RED1_SUBSTITUTION_REMARK] 1188 THEN DEP_REWRITE_TAC[TC_SUBSET,RC_SUBSET] 1189 THEN ASM_REWRITE_TAC[] 1190 THEN MATCH_MP_TAC RED1_R 1191 THEN REWRITE_TAC[BETA_R_rules_sat], 1192 1193 (* Case 4: t1 -->e u2, BETA (t u1) M2. *) 1194 IMP_RES_TAC BETA_R_inv_thms 1195 THEN POP_ASSUM REWRITE_ALL_THM 1196 THEN UNDISCH_LAST_TAC 1197 THEN REWRITE_TAC[term_distinct] 1198 ] 1199 ); 1200 1201 1202 1203val RED1_BETA_COMMUTES_RED1_ETA_LEMMA2 = store_thm 1204 ("RED1_BETA_COMMUTES_RED1_ETA_LEMMA2", 1205 ���!R (M:^term) M1. 1206 RED1 R M M1 ==> !M2. RED1 ETA_R M M2 /\ (R = BETA_R) ==> 1207 ?M3. TC (RC (RED1 ETA_R)) M1 M3 /\ RC (RED1 BETA_R) M2 M3���, 1208 rule_induct RED1_height_strong_ind 1209 THEN REPEAT STRIP_TAC (* 4 subgoals *) 1210 THEN POP_ASSUM REWRITE_ALL_THM 1211 THENL 1212 [ (* Case 1: *) 1213 IMP_RES_TAC RED1_BETA_COMMUTES_RED1_ETA_LEMMA1 1214 THEN POP_TAC 1215 THEN REWRITE_ALL_TAC[] 1216 THEN POP_ASSUM STRIP_ASSUME_TAC 1217 THEN EXISTS_TAC ``M3:^term`` 1218 THEN ASM_REWRITE_TAC[], 1219 1220 (* Case 2: *) 1221 IMP_RES_TAC RED1_ETA_App_case 1222 THENL 1223 [ POP_ASSUM REWRITE_ALL_THM 1224 THEN RES_TAC 1225 THEN EXISTS_TAC ``App M3 u:^term`` 1226 THEN IMP_RES_THEN REWRITE_THM TC_RC_RED1_COMPAT 1227 THEN IMP_RES_THEN REWRITE_THM RC_RED1_COMPAT, 1228 1229 POP_ASSUM REWRITE_ALL_THM 1230 THEN EXISTS_TAC ``App t2 u':^term`` 1231 THEN DEP_REWRITE_TAC[TC_SUBSET,RC_SUBSET] 1232 THEN IMP_RES_THEN REWRITE_THM RED1_COMPAT 1233 ], 1234 1235 (* Case 3: *) 1236 IMP_RES_TAC RED1_ETA_App_case 1237 THENL 1238 [ POP_ASSUM REWRITE_ALL_THM 1239 THEN EXISTS_TAC ``App t' u2:^term`` 1240 THEN DEP_REWRITE_TAC[TC_SUBSET,RC_SUBSET] 1241 THEN IMP_RES_THEN REWRITE_THM RED1_COMPAT, 1242 1243 POP_ASSUM REWRITE_ALL_THM 1244 THEN RES_TAC 1245 THEN EXISTS_TAC ``App t M3:^term`` 1246 THEN IMP_RES_THEN REWRITE_THM TC_RC_RED1_COMPAT 1247 THEN IMP_RES_THEN REWRITE_THM RC_RED1_COMPAT 1248 ], 1249 1250 (* Case 4: *) 1251 IMP_RES_TAC RED1_ETA_Lam_case 1252 THENL 1253 [ POP_ASSUM REWRITE_ALL_THM 1254 THEN IMP_RES_TAC RED1_BETA_App_case 1255 THENL (* 3 subgoals *) 1256 [ (* Case 4.1: *) 1257 POP_ASSUM REWRITE_ALL_THM 1258 THEN EXISTS_TAC ``t':^term`` 1259 THEN DEP_REWRITE_TAC[TC_SUBSET,RC_SUBSET] 1260 THEN ASM_REWRITE_TAC[] 1261 THEN MATCH_MP_TAC RED1_R 1262 THEN MATCH_MP_TAC ETA_R_rules_sat 1263 THEN IMP_RES_THEN MATCH_MP_TAC NOT_IN_SUBSET 1264 THEN IMP_RES_TAC RED1_BETA_FV, 1265 1266 (* Case 4.2: *) 1267 POP_ASSUM REWRITE_ALL_THM 1268 THEN IMP_RES_TAC RED1_BETA_Var_case, 1269 1270 (* Case 4.3: *) 1271 POP_ASSUM REWRITE_ALL_THM 1272 THEN POP_ASSUM REWRITE_ALL_THM 1273 THEN EXISTS_TAC ``Lam x' t':^term`` 1274 THEN REWRITE_TAC[RC_REFLEXIVE] 1275 THEN DEP_REWRITE_TAC[ 1276 ONCE_REWRITE_RULE[EQ_SYM_EQ] LAMBDA_CHANGE_BOUND_VAR] 1277 THEN ASM_REWRITE_TAC[GSYM FV_term] 1278 THEN MATCH_MP_TAC TC_SUBSET 1279 THEN REWRITE_TAC[RC_REFLEXIVE] 1280 ], 1281 1282 POP_ASSUM REWRITE_ALL_THM 1283 THEN RES_THEN (STRIP_ASSUME_TAC o REWRITE_RULE[]) 1284 THEN POP_ASSUM IMP_RES_TAC 1285 THEN EXISTS_TAC ``Lam x M3:^term`` 1286 THEN IMP_RES_THEN REWRITE_THM TC_RC_RED1_COMPAT 1287 THEN IMP_RES_THEN REWRITE_THM RC_RED1_COMPAT 1288 ] 1289 ] 1290 ); 1291 1292 1293val RED_BETA_COMMUTES_RED_ETA = store_thm 1294 ("RED_BETA_COMMUTES_RED_ETA", 1295 ���RED (BETA_R:^term_rel) <=> RED ETA_R���, 1296 REWRITE_TAC[GSYM TC_RC_RED1_IS_RED] 1297 THEN MATCH_MP_TAC COMMUTE_TC_RC 1298 THEN REPEAT STRIP_TAC 1299 THEN IMP_RES_TAC RED1_BETA_COMMUTES_RED1_ETA_LEMMA2 1300 THEN FIRST_ASSUM MATCH_MP_TAC 1301 THEN REFL_TAC 1302 ); 1303 1304 1305(* ====================================== *) 1306(* Beta-eta reduction is Church-Rosser. *) 1307(* Barendregt Theorem 3.3.9(i), page 66. *) 1308(* ====================================== *) 1309 1310val BETA_ETA_R_CHURCH_ROSSER = store_thm 1311 ("BETA_ETA_R_CHURCH_ROSSER", 1312 ���CHURCH_ROSSER ((BETA_R:^term_rel) UNION_R ETA_R)���, 1313 MATCH_MP_TAC COMMUTE_CHURCH_ROSSER 1314 THEN REWRITE_TAC[BETA_R_CHURCH_ROSSER,ETA_R_CHURCH_ROSSER, 1315 RED_BETA_COMMUTES_RED_ETA] 1316 ); 1317(* Soli Deo Gloria!!! To God Alone Be The Glory!!! *) 1318 1319 1320(* Barendregt Theorem 3.3.9 (ii), page 66. *) 1321 1322val BETA_ETA_R_NORMAL_FORM_EXISTS = store_thm 1323 ("BETA_ETA_R_NORMAL_FORM_EXISTS", 1324 ���!(M:^term) N. 1325 REQUAL (BETA_R UNION_R ETA_R) M N ==> 1326 (?Z. RED (BETA_R UNION_R ETA_R) M Z /\ 1327 RED (BETA_R UNION_R ETA_R) N Z)���, 1328 MATCH_MP_TAC NORMAL_FORM_EXISTS 1329 THEN REWRITE_TAC[BETA_ETA_R_CHURCH_ROSSER] 1330 ); 1331 1332(* Barendregt Corollary 3.3.10 (i), page 67. *) 1333 1334val BETA_ETA_R_NORMAL_FORM_REDUCED_TO = store_thm 1335 ("BETA_ETA_R_NORMAL_FORM_REDUCED_TO", 1336 ���!(M:^term) N. 1337 NORMAL_FORM_OF (BETA_R UNION_R ETA_R) N M ==> 1338 RED (BETA_R UNION_R ETA_R) M N���, 1339 MATCH_MP_TAC NORMAL_FORM_REDUCED_TO 1340 THEN REWRITE_TAC[BETA_ETA_R_CHURCH_ROSSER] 1341 ); 1342 1343(* Barendregt Corollary 3.3.10 (ii), page 67. *) 1344 1345val BETA_ETA_R_NORMAL_FORM_UNIQUE = store_thm 1346 ("BETA_ETA_R_NORMAL_FORM_UNIQUE", 1347 ���!(M:^term) N1 N2. 1348 NORMAL_FORM_OF (BETA_R UNION_R ETA_R) N1 M /\ 1349 NORMAL_FORM_OF (BETA_R UNION_R ETA_R) N2 M ==> 1350 (N1 = N2)���, 1351 MATCH_MP_TAC NORMAL_FORM_UNIQUE 1352 THEN REWRITE_TAC[BETA_ETA_R_CHURCH_ROSSER] 1353 ); 1354 1355 1356 1357 1358 1359val _ = export_theory(); 1360 1361val _ = print_theory_to_file "-" "eta.lst"; 1362 1363val _ = html_theory "eta"; 1364 1365val _ = print_theory_size(); 1366