1open HolKernel Parse boolLib bossLib metisLib basic_swapTheory 2 relationTheory 3 4val _ = new_theory "chap3"; 5 6local open pred_setLib in end; 7 8open binderLib BasicProvers 9open nomsetTheory termTheory chap2Theory 10 11fun Store_thm (trip as (n,t,tac)) = store_thm trip before export_rewrites [n] 12 13val SUBSET_DEF = pred_setTheory.SUBSET_DEF 14 15val compatible_def = 16 Define`compatible R = !x y c. R x y /\ one_hole_context c ==> 17 R (c x) (c y)`; 18 19val congruence_def = Define`congruence R <=> equivalence R /\ compatible R`; 20 21val is_reduction_def = 22 Define`is_reduction R <=> compatible R /\ transitive R /\ reflexive R`; 23 24val (compat_closure_rules, compat_closure_ind, compat_closure_cases) = 25 Hol_reln`(!x y. R x y ==> compat_closure R x y) /\ 26 (!x y z. compat_closure R x y ==> 27 compat_closure R (z @@ x) (z @@ y)) /\ 28 (!x y z. compat_closure R x y ==> 29 compat_closure R (x @@ z) (y @@ z)) /\ 30 (!x y v. compat_closure R x y ==> 31 compat_closure R (LAM v x) (LAM v y))` 32 33(* Barendregt definition 3.1.14 *) 34val substitutive_def = Define` 35 substitutive R = !M M'. R M M' ==> !N v. R ([N/v]M) ([N/v]M') 36`; 37 38val permutative_def = Define` 39 permutative R = !M M'. R M M' ==> !p. R (tpm p M) (tpm p M') 40`; 41 42val cc_gen_ind = store_thm( 43 "cc_gen_ind", 44 ``!R fv. (!M N p. R M N ==> R (tpm p M) (tpm p N)) /\ 45 (!M N x. R M N ==> P M N x) /\ 46 (!M M' N x. (!y. P M M' y) ==> P (M @@ N) (M' @@ N) x) /\ 47 (!M N N' x. (!y. P N N' y) ==> P (M @@ N) (M @@ N') x) /\ 48 (!v M M' x. ~(v IN fv x) /\ (!y. P M M' y) ==> 49 P (LAM v M) (LAM v M') x) /\ 50 (!x. FINITE (fv x)) ==> 51 !M N. compat_closure R M N ==> !x. P M N x``, 52 REPEAT GEN_TAC THEN STRIP_TAC THEN 53 Q_TAC SUFF_TAC `!M N. compat_closure R M N ==> 54 !x p. P (tpm p M) (tpm p N) x` 55 THEN1 METIS_TAC [pmact_nil] THEN 56 HO_MATCH_MP_TAC compat_closure_ind THEN SRW_TAC [][] THEN 57 Q_TAC (NEW_TAC "z") `fv x UNION {lswapstr p v} UNION FV (tpm p M) UNION 58 FV (tpm p N)` THEN 59 `LAM (lswapstr p v) (tpm p M) = LAM z (tpm ([(z,lswapstr p v)] ++ p) M)` 60 by SRW_TAC [][tpm_ALPHA, pmact_decompose] THEN 61 `LAM (lswapstr p v) (tpm p N) = LAM z (tpm ([(z,lswapstr p v)] ++ p) N)` 62 by SRW_TAC [][tpm_ALPHA, pmact_decompose] THEN 63 SRW_TAC [][]); 64 65val cc_ind = save_thm( 66 "cc_ind", 67 (Q.GEN `P` o Q.GEN `X` o Q.GEN `R` o 68 Q.INST [`P'` |-> `P`] o 69 SIMP_RULE (srw_ss()) [] o 70 Q.INST [`P` |-> `\M N x. P' M N`, `fv` |-> `\x. X`] o 71 SPEC_ALL) cc_gen_ind); 72 73val compat_closure_permutative = store_thm( 74 "compat_closure_permutative", 75 ``permutative R ==> permutative (compat_closure R)``, 76 STRIP_TAC THEN ASM_SIMP_TAC (srw_ss()) [permutative_def] THEN 77 HO_MATCH_MP_TAC compat_closure_ind THEN SRW_TAC [][] THEN 78 METIS_TAC [permutative_def, compat_closure_rules]); 79 80val permutative_compat_closure_eqn = store_thm( 81 "permutative_compat_closure_eqn", 82 ``permutative R ==> 83 (compat_closure R (tpm p M) (tpm p N) = compat_closure R M N)``, 84 STRIP_TAC THEN EQ_TAC THEN STRIP_TAC THENL [ 85 `permutative (compat_closure R)` 86 by METIS_TAC [compat_closure_permutative] THEN 87 `compat_closure R (tpm (REVERSE p) (tpm p M)) 88 (tpm (REVERSE p) (tpm p N))` 89 by METIS_TAC [permutative_def] THEN 90 FULL_SIMP_TAC (srw_ss()) [], 91 METIS_TAC [permutative_def, compat_closure_permutative] 92 ]); 93val _ = export_rewrites ["permutative_compat_closure_eqn"] 94 95val swap_eq_3substs = store_thm( 96 "swap_eq_3substs", 97 ``~(z IN FV M) /\ ~(x = z) /\ ~(y = z) ==> 98 (tpm [(x, y)] M = [VAR y/z] ([VAR x/y] ([VAR z/x] M)))``, 99 SRW_TAC [][GSYM fresh_tpm_subst] THEN 100 `tpm [(x,y)] (tpm [(z,x)] M) = 101 tpm [(swapstr x y z, swapstr x y x)] (tpm [(x,y)] M)` 102 by (SRW_TAC [][Once (GSYM pmact_sing_to_back), SimpLHS] THEN 103 SRW_TAC [][]) THEN 104 POP_ASSUM SUBST_ALL_TAC THEN 105 SRW_TAC [][pmact_flip_args]); 106 107val substitutive_implies_permutative = store_thm( 108 "substitutive_implies_permutative", 109 ``substitutive R ==> permutative R``, 110 SRW_TAC [][substitutive_def, permutative_def] THEN 111 Induct_on `p` THEN SRW_TAC [][] THEN 112 `?x y. h = (x,y)` by METIS_TAC [pairTheory.pair_CASES] THEN 113 SRW_TAC [][] THEN 114 Q_TAC (NEW_TAC "z") `{x; y} UNION FV (tpm p M) UNION FV (tpm p M')` THEN 115 `(tpm ((x,y)::p) M = [VAR y/z] ([VAR x/y] ([VAR z/x] (tpm p M)))) /\ 116 (tpm ((x,y)::p) M'= [VAR y/z] ([VAR x/y] ([VAR z/x] (tpm p M'))))` 117 by (ONCE_REWRITE_TAC [tpm_CONS] THEN 118 SRW_TAC [][swap_eq_3substs]) THEN 119 ASM_SIMP_TAC (srw_ss()) []); 120 121val compat_closure_substitutive = store_thm( 122 "compat_closure_substitutive", 123 ``substitutive R ==> substitutive (compat_closure R)``, 124 STRIP_TAC THEN SIMP_TAC (srw_ss()) [substitutive_def] THEN 125 REPEAT STRIP_TAC THEN 126 Q.UNDISCH_THEN `compat_closure R M M'` MP_TAC THEN 127 MAP_EVERY Q.ID_SPEC_TAC [`M'`, `M`] THEN 128 HO_MATCH_MP_TAC cc_ind THEN Q.EXISTS_TAC `v INSERT FV N` THEN 129 SRW_TAC [][SUB_THM] THENL [ 130 PROVE_TAC [substitutive_implies_permutative, permutative_def], 131 PROVE_TAC [compat_closure_rules, substitutive_def], 132 SRW_TAC [][compat_closure_rules], 133 SRW_TAC [][compat_closure_rules], 134 SRW_TAC [][compat_closure_rules] 135 ]); 136 137val _ = overload_on ("equiv_closure", ``relation$EQC``) 138val _ = overload_on ("EQC", ``relation$EQC``) 139local 140 open relationTheory 141in 142 val equiv_closure_rules = LIST_CONJ [EQC_R, EQC_REFL, EQC_SYM, EQC_TRANS] 143 val equiv_closure_ind = EQC_INDUCTION 144end 145 146val equiv_closure_substitutive = store_thm( 147 "equiv_closure_substitutive", 148 ``substitutive R ==> substitutive (equiv_closure R)``, 149 STRIP_TAC THEN SIMP_TAC (srw_ss()) [substitutive_def] THEN 150 HO_MATCH_MP_TAC equiv_closure_ind THEN SRW_TAC [][] THEN 151 METIS_TAC [substitutive_def, equiv_closure_rules]); 152 153val _ = overload_on ("conversion", ``\R. equiv_closure (compat_closure R)``) 154 155val conversion_substitutive = store_thm( 156 "conversion_substitutive", 157 ``substitutive R ==> substitutive (conversion R)``, 158 METIS_TAC [compat_closure_substitutive, equiv_closure_substitutive]); 159 160val RTC_substitutive = store_thm( 161 "RTC_substitutive", 162 ``substitutive R ==> substitutive (RTC R)``, 163 STRIP_TAC THEN SIMP_TAC (srw_ss()) [substitutive_def] THEN 164 HO_MATCH_MP_TAC RTC_INDUCT THEN 165 METIS_TAC [RTC_RULES, substitutive_def]); 166 167val _ = overload_on ("reduction", ``\R. RTC (compat_closure R)``) 168 169val reduction_substitutive = store_thm( 170 "reduction_substitutive", 171 ``substitutive R ==> substitutive (reduction R)``, 172 METIS_TAC [compat_closure_substitutive, RTC_substitutive]); 173 174val conversion_rules = store_thm( 175 "conversion_rules", 176 ``!R. (!x. conversion R x x) /\ 177 (!x y. conversion R x y ==> conversion R y x) /\ 178 (!x y z. conversion R x y /\ conversion R y z ==> conversion R x z) /\ 179 (!x y. R x y ==> conversion R x y) /\ 180 (!x y. reduction R x y ==> conversion R x y) /\ 181 (!x y. compat_closure R x y ==> conversion R x y)``, 182 SRW_TAC [][equiv_closure_rules] THENL [ 183 PROVE_TAC [equiv_closure_rules], 184 PROVE_TAC [equiv_closure_rules, compat_closure_rules], 185 POP_ASSUM MP_TAC THEN SIMP_TAC (srw_ss()) [] THEN 186 MAP_EVERY Q.ID_SPEC_TAC [`y`,`x`] THEN 187 HO_MATCH_MP_TAC RTC_INDUCT THEN 188 PROVE_TAC [equiv_closure_rules] 189 ]); 190 191val compat_closure_compatible = store_thm( 192 "compat_closure_compatible", 193 ``!R. compatible (compat_closure R)``, 194 GEN_TAC THEN 195 Q_TAC SUFF_TAC `!c. one_hole_context c ==> 196 !x y. compat_closure R x y ==> 197 compat_closure R (c x) (c y)` THEN1 198 SRW_TAC [][compatible_def] THEN 199 HO_MATCH_MP_TAC one_hole_context_ind THEN SRW_TAC [][] THEN 200 PROVE_TAC [compat_closure_rules]); 201 202val reduction_compatible = store_thm( 203 "reduction_compatible", 204 ``!R. compatible (reduction R)``, 205 GEN_TAC THEN 206 Q_TAC SUFF_TAC `!x y. RTC (compat_closure R) x y ==> 207 !c. one_hole_context c ==> 208 RTC (compat_closure R) (c x) (c y)` THEN1 209 SRW_TAC [][compatible_def] THEN 210 HO_MATCH_MP_TAC RTC_INDUCT THEN SRW_TAC [][] THEN 211 PROVE_TAC [compatible_def, compat_closure_compatible, 212 RTC_RULES]); 213 214val reduction_rules = store_thm( 215 "reduction_rules", 216 ``(!x. reduction R x x) /\ 217 (!x y. R x y ==> reduction R x y) /\ 218 (!x y. compat_closure R x y ==> reduction R x y) /\ 219 (!x y z. reduction R x y /\ reduction R y z ==> 220 reduction R x z) /\ 221 (!x y z. reduction R x y ==> reduction R (z @@ x) (z @@ y)) /\ 222 (!x y z. reduction R x y ==> reduction R (x @@ z) (y @@ z)) /\ 223 (!x y v. reduction R x y ==> reduction R (LAM v x) (LAM v y))``, 224 REPEAT STRIP_TAC THENL [ 225 PROVE_TAC [RTC_RULES], 226 PROVE_TAC [RTC_RULES, compat_closure_rules], 227 PROVE_TAC [RTC_RULES], 228 PROVE_TAC [RTC_RTC], 229 PROVE_TAC [leftctxt, compatible_def, reduction_compatible], 230 PROVE_TAC [rightctxt_thm, rightctxt, compatible_def, reduction_compatible], 231 PROVE_TAC [absctxt, compatible_def, reduction_compatible] 232 ]); 233 234val conversion_compatible = store_thm( 235 "conversion_compatible", 236 ``!R. compatible (conversion R)``, 237 GEN_TAC THEN 238 Q_TAC SUFF_TAC `!x y. equiv_closure (compat_closure R) x y ==> 239 !c. one_hole_context c ==> 240 equiv_closure (compat_closure R) (c x) (c y)` THEN1 241 SRW_TAC [][compatible_def] THEN 242 HO_MATCH_MP_TAC equiv_closure_ind THEN SRW_TAC [][] THEN 243 PROVE_TAC [compatible_def, equiv_closure_rules, compat_closure_compatible]); 244 245(* "Follows from an induction on the structure of M, and the 246 compatibility of reduction R" *) 247val lemma3_8 = store_thm( 248 "lemma3_8", 249 ``!M. reduction R N N' ==> reduction R ([N/x] M) ([N'/x] M)``, 250 HO_MATCH_MP_TAC nc_INDUCTION2 THEN 251 Q.EXISTS_TAC `x INSERT FV N UNION FV N'` THEN 252 SRW_TAC [][SUB_THM, SUB_VAR] THEN PROVE_TAC [reduction_rules]); 253 254val redex_def = Define`redex (R:'a -> 'a -> bool) t = ?u. R t u`; 255 256val (can_reduce_rules, can_reduce_ind, can_reduce_cases) = 257 Hol_reln`(!t. redex R t ==> can_reduce R t) /\ 258 (!M N. can_reduce R M ==> can_reduce R (M @@ N)) /\ 259 (!M N. can_reduce R M ==> can_reduce R (N @@ M)) /\ 260 (!v M. can_reduce R M ==> can_reduce R (LAM v M))` 261 262val can_reduce_reduces = store_thm( 263 "can_reduce_reduces", 264 ``!R t. can_reduce R t ==> ?u. compat_closure R t u``, 265 GEN_TAC THEN HO_MATCH_MP_TAC can_reduce_ind THEN SRW_TAC [][redex_def] THEN 266 PROVE_TAC [compat_closure_rules]); 267 268val normal_form_def = Define`normal_form R t = ~can_reduce R t`; 269 270(* definition from p30 *) 271val beta_def = Define`beta M N = ?x body arg. (M = LAM x body @@ arg) /\ 272 (N = [arg/x]body)`; 273val _ = Unicode.unicode_version {u = UnicodeChars.beta, tmnm = "beta"} 274 275val beta_alt = store_thm( 276 "beta_alt", 277 ``!X M N. FINITE X ==> 278 (beta M N = ?x body arg. (M = LAM x body @@ arg) /\ 279 (N = [arg/x] body) /\ 280 ~(x IN X))``, 281 SRW_TAC [][beta_def, EQ_IMP_THM] THENL [ 282 SRW_TAC [][LAM_eq_thm] THEN 283 Q_TAC (NEW_TAC "z") `x INSERT FV body UNION X` THEN 284 MAP_EVERY Q.EXISTS_TAC [`z`, `tpm [(x,z)] body`] THEN 285 SRW_TAC [][] THEN 286 Q_TAC SUFF_TAC `tpm [(x,z)] body = [VAR z/x]body` 287 THEN1 SRW_TAC [][lemma15a] THEN 288 SRW_TAC [][GSYM fresh_tpm_subst, pmact_flip_args], 289 METIS_TAC [] 290 ]); 291 292val strong_bvc_term_ind = store_thm( 293 "strong_bvc_term_ind", 294 ``!P fv. (!s x. P (VAR s) x) /\ 295 (!M N x. (!x. P M x) /\ (!x. P N x) ==> P (M @@ N) x) /\ 296 (!v x M. ~(v IN fv x) /\ (!x. P M x) ==> P (LAM v M) x) /\ 297 (!x. FINITE (fv x)) ==> 298 !t x. P t x``, 299 REPEAT GEN_TAC THEN STRIP_TAC THEN 300 Q_TAC SUFF_TAC `!t p x. P (tpm p t) x` THEN1 METIS_TAC [pmact_nil] THEN 301 HO_MATCH_MP_TAC simple_induction THEN SRW_TAC [][] THEN 302 Q.ABBREV_TAC `u = lswapstr p v` THEN 303 Q.ABBREV_TAC `M = tpm p t` THEN 304 Q_TAC (NEW_TAC "z") `u INSERT FV M UNION fv x` THEN 305 `LAM u M = LAM z (tpm [(z, u)] M)` by SRW_TAC [][tpm_ALPHA] THEN 306 `tpm [(z,u)] M = tpm ((z,u)::p) t` 307 by SRW_TAC [][Abbr`M`, GSYM pmact_decompose] THEN 308 SRW_TAC [][]) 309 310val _ = set_fixity "-b->" (Infix(NONASSOC, 450)) 311val _ = overload_on("-b->", ``compat_closure beta``) 312val _ = set_fixity "-b->*" (Infix(NONASSOC, 450)) 313val _ = overload_on ("-b->*", ``RTC (-b->)``) 314 315val ubeta_arrow = "-" ^ UnicodeChars.beta ^ "->" 316val _ = Unicode.unicode_version {u = ubeta_arrow, tmnm = "-b->"} 317val _ = Unicode.unicode_version {u = ubeta_arrow^"*", tmnm = "-b->*"} 318 319val ccbeta_gen_ind = store_thm( 320 "ccbeta_gen_ind", 321 ``(!v M N X. v NOTIN FV N /\ v NOTIN fv X ==> 322 P ((LAM v M) @@ N) ([N/v]M) X) /\ 323 (!M1 M2 N X. (!X. P M1 M2 X) ==> P (M1 @@ N) (M2 @@ N) X) /\ 324 (!M N1 N2 X. (!X. P N1 N2 X) ==> P (M @@ N1) (M @@ N2) X) /\ 325 (!v M1 M2 X. v NOTIN fv X /\ (!X. P M1 M2 X) ==> 326 P (LAM v M1) (LAM v M2) X) /\ 327 (!X. FINITE (fv X)) ==> 328 !M N. M -b-> N ==> !X. P M N X``, 329 STRIP_TAC THEN 330 Q_TAC SUFF_TAC `!M N. M -b-> N ==> 331 !X p. P (tpm p M) (tpm p N) X` 332 THEN1 METIS_TAC [pmact_nil] THEN 333 HO_MATCH_MP_TAC compat_closure_ind THEN REPEAT STRIP_TAC THENL [ 334 FULL_SIMP_TAC (srw_ss()) [beta_def, tpm_subst] THEN 335 Q.ABBREV_TAC `v = lswapstr p x` THEN 336 Q.ABBREV_TAC `N' = tpm p arg` THEN 337 Q.ABBREV_TAC `M' = tpm p body` THEN 338 Q_TAC (NEW_TAC "z") `v INSERT FV M' UNION FV N' UNION fv X` THEN 339 `LAM v M' = LAM z ([VAR z/v] M')` by SRW_TAC [][SIMPLE_ALPHA] THEN 340 Q_TAC SUFF_TAC `[N'/v]M' = [N'/z]([VAR z/v]M')` THEN1 SRW_TAC [][] THEN 341 SRW_TAC [][lemma15a], 342 SRW_TAC [][], 343 SRW_TAC [][], 344 SRW_TAC [][] THEN 345 Q.ABBREV_TAC `x = lswapstr p v` THEN 346 Q.ABBREV_TAC `M' = tpm p M` THEN 347 Q.ABBREV_TAC `N' = tpm p N` THEN 348 Q_TAC (NEW_TAC "z") `x INSERT FV M' UNION FV N' UNION fv X` THEN 349 `(LAM x M' = LAM z (tpm [(z,x)] M')) /\ (LAM x N' = LAM z (tpm[(z,x)] N'))` 350 by SRW_TAC [][tpm_ALPHA] THEN 351 SRW_TAC [][] THEN 352 FIRST_X_ASSUM MATCH_MP_TAC THEN SRW_TAC [][] THEN 353 `(tpm [(z,x)] M' = tpm ((z,x)::p) M) /\ 354 (tpm [(z,x)] N' = tpm ((z,x)::p) N)` 355 by SRW_TAC [][Abbr`M'`, Abbr`N'`, GSYM pmact_decompose] THEN 356 SRW_TAC [][] 357 ]); 358 359val ccbeta_ind = save_thm( 360 "ccbeta_ind", 361 (Q.GEN `P` o Q.GEN `X` o 362 SIMP_RULE (srw_ss()) [] o 363 Q.INST [`P'` |-> `P`] o 364 Q.INST [`fv` |-> `\x. X`, `P` |-> `\M N X. P' M N`] o 365 SPEC_ALL) ccbeta_gen_ind); 366 367val beta_substitutive = store_thm( 368 "beta_substitutive", 369 ``substitutive beta``, 370 SRW_TAC [][substitutive_def] THEN 371 Q.SPEC_THEN `v INSERT FV N` ASSUME_TAC beta_alt THEN 372 FULL_SIMP_TAC (srw_ss()) [] THEN 373 Q.EXISTS_TAC `x` THEN SRW_TAC [][SUB_THM, GSYM substitution_lemma]); 374 375val cc_beta_subst = store_thm( 376 "cc_beta_subst", 377 ``!M N. M -b-> N ==> !P v. [P/v]M -b-> [P/v]N``, 378 METIS_TAC [beta_substitutive, compat_closure_substitutive, 379 substitutive_def]); 380 381val reduction_beta_subst = store_thm( 382 "reduction_beta_subst", 383 ``!M N. M -b->* N ==> !P v. [P/v]M -b->* [P/v]N``, 384 METIS_TAC [beta_substitutive, reduction_substitutive, substitutive_def]); 385 386val cc_beta_FV_SUBSET = store_thm( 387 "cc_beta_FV_SUBSET", 388 ``!M N. M -b-> N ==> FV N SUBSET FV M``, 389 HO_MATCH_MP_TAC ccbeta_ind THEN Q.EXISTS_TAC `{}` THEN 390 SRW_TAC [][SUBSET_DEF, FV_SUB] THEN PROVE_TAC []); 391 392val cc_beta_tpm = store_thm( 393 "cc_beta_tpm", 394 ``!M N. M -b-> N ==> !p. tpm p M -b-> tpm p N``, 395 HO_MATCH_MP_TAC compat_closure_ind THEN SRW_TAC [][] THENL [ 396 FULL_SIMP_TAC (srw_ss()) [beta_def, tpm_subst] THEN 397 METIS_TAC [compat_closure_rules, beta_def], 398 METIS_TAC [compat_closure_rules], 399 METIS_TAC [compat_closure_rules], 400 METIS_TAC [compat_closure_rules] 401 ]); 402 403val cc_beta_tpm_eqn = store_thm( 404 "cc_beta_tpm_eqn", 405 ``tpm pi M -b-> N <=> M -b-> tpm (REVERSE pi) N``, 406 METIS_TAC [pmact_inverse, cc_beta_tpm]); 407 408val cc_beta_thm = store_thm( 409 "cc_beta_thm", 410 ``(!s t. VAR s -b-> t <=> F) /\ 411 (!M N P. M @@ N -b-> P <=> 412 (?v M0. (M = LAM v M0) /\ (P = [N/v]M0)) \/ 413 (?M'. (P = M' @@ N) /\ M -b-> M') \/ 414 (?N'. (P = M @@ N') /\ N -b-> N')) /\ 415 (!v M N. LAM v M -b-> N <=> ?N0. (N = LAM v N0) /\ M -b-> N0)``, 416 REPEAT CONJ_TAC THEN 417 SIMP_TAC (srw_ss()) [beta_def, SimpLHS, Once compat_closure_cases] THEN 418 REPEAT STRIP_TAC THEN EQ_TAC THEN 419 SRW_TAC [][] THEN SRW_TAC [][] THENL [ 420 PROVE_TAC [], 421 PROVE_TAC [], 422 REPEAT (POP_ASSUM MP_TAC) THEN 423 Q_TAC SUFF_TAC 424 `!v w M N P. 425 (LAM v M = LAM w N) ==> 426 compat_closure beta N P ==> 427 ?M0. (LAM w P = LAM v M0) /\ 428 compat_closure beta M M0` THEN1 PROVE_TAC [] THEN 429 SRW_TAC [][LAM_eq_thm] THEN Q.EXISTS_TAC `tpm [(v,w)] P` THEN 430 SRW_TAC [][pmact_flip_args, cc_beta_tpm_eqn] THEN 431 METIS_TAC [cc_beta_FV_SUBSET, SUBSET_DEF], 432 PROVE_TAC [] 433 ]); 434 435val ccbeta_rwt = store_thm( 436 "ccbeta_rwt", 437 ``(VAR s -b-> N <=> F) /\ 438 (LAM x M -b-> N <=> ?N0. (N = LAM x N0) /\ M -b-> N0) /\ 439 (LAM x M @@ N -b-> P <=> 440 (?M'. (P = LAM x M' @@ N) /\ M -b-> M') \/ 441 (?N'. (P = LAM x M @@ N') /\ N -b-> N') \/ 442 (P = [N/x]M)) /\ 443 (~is_abs M ==> 444 (M @@ N -b-> P <=> 445 (?M'. (P = M' @@ N) /\ M -b-> M') \/ 446 (?N'. (P = M @@ N') /\ N -b-> N')))``, 447 SRW_TAC [][cc_beta_thm] THENL [ 448 SRW_TAC [][EQ_IMP_THM, LAM_eq_thm] THEN SRW_TAC [][] THENL [ 449 METIS_TAC [fresh_tpm_subst, lemma15a], 450 SRW_TAC [boolSimps.DNF_ss][tpm_eqr] 451 ], 452 Q_TAC SUFF_TAC `!v M'. M <> LAM v M'` THEN1 METIS_TAC[] THEN 453 Q.SPEC_THEN `M` FULL_STRUCT_CASES_TAC term_CASES THEN 454 FULL_SIMP_TAC (srw_ss()) [] 455 ]); 456 457val beta_normal_form_bnf = store_thm( 458 "beta_normal_form_bnf", 459 ``normal_form beta = bnf``, 460 SIMP_TAC (srw_ss()) [FUN_EQ_THM, EQ_IMP_THM, normal_form_def, 461 FORALL_AND_THM] THEN 462 CONJ_TAC THENL [ 463 Q_TAC SUFF_TAC `!t. ~bnf t ==> can_reduce beta t` THEN1 PROVE_TAC [] THEN 464 HO_MATCH_MP_TAC nc_INDUCTION2 THEN 465 Q.EXISTS_TAC `{}` THEN SRW_TAC [][] THENL [ 466 PROVE_TAC [can_reduce_rules], 467 PROVE_TAC [can_reduce_rules], 468 Q_TAC SUFF_TAC `redex beta (t @@ t')` THEN1 469 PROVE_TAC [can_reduce_rules] THEN 470 SRW_TAC [][redex_def, beta_def] THEN PROVE_TAC [is_abs_thm, term_CASES], 471 PROVE_TAC [lemma14a, can_reduce_rules] 472 ], 473 Q_TAC SUFF_TAC `!t. can_reduce beta t ==> ~bnf t` THEN1 PROVE_TAC [] THEN 474 HO_MATCH_MP_TAC can_reduce_ind THEN SRW_TAC [][redex_def, beta_def] THEN 475 SRW_TAC [][] 476 ]); 477 478val nf_of_def = Define`nf_of R M N <=> normal_form R N /\ conversion R M N`; 479 480val prop3_10 = store_thm( 481 "prop3_10", 482 ``!R M N. 483 compat_closure R M N = ?P Q c. one_hole_context c /\ (M = c P) /\ 484 (N = c Q) /\ R P Q``, 485 GEN_TAC THEN SIMP_TAC (srw_ss()) [EQ_IMP_THM, FORALL_AND_THM] THEN 486 CONJ_TAC THENL [ 487 HO_MATCH_MP_TAC compat_closure_ind THEN SRW_TAC [][] THENL [ 488 MAP_EVERY Q.EXISTS_TAC [`M`,`N`,`\x.x`] THEN 489 SRW_TAC [][one_hole_context_rules], 490 MAP_EVERY Q.EXISTS_TAC [`P`,`Q`,`\t. z @@ c t`] THEN 491 SRW_TAC [][one_hole_context_rules], 492 MAP_EVERY Q.EXISTS_TAC [`P`,`Q`,`\t. c t @@ z`] THEN 493 SRW_TAC [][one_hole_context_rules], 494 MAP_EVERY Q.EXISTS_TAC [`P`,`Q`,`\t. LAM v (c t)`] THEN 495 SRW_TAC [][one_hole_context_rules] 496 ], 497 PROVE_TAC [compat_closure_compatible, compatible_def, 498 compat_closure_rules] 499 ]); 500 501val corollary3_2_1 = store_thm( 502 "corollary3_2_1", 503 ``!R M. normal_form R M ==> (!N. ~compat_closure R M N) /\ 504 (!N. reduction R M N ==> (M = N))``, 505 SIMP_TAC (srw_ss()) [normal_form_def] THEN REPEAT GEN_TAC THEN 506 STRIP_TAC THEN 507 Q.SUBGOAL_THEN `!N. ~compat_closure R M N` ASSUME_TAC THENL [ 508 GEN_TAC THEN POP_ASSUM MP_TAC THEN 509 CONV_TAC CONTRAPOS_CONV THEN SIMP_TAC (srw_ss())[] THEN 510 MAP_EVERY Q.ID_SPEC_TAC [`N`, `M`] THEN 511 HO_MATCH_MP_TAC compat_closure_ind THEN 512 PROVE_TAC [can_reduce_rules, redex_def], 513 ALL_TAC 514 ] THEN ASM_SIMP_TAC (srw_ss()) [] THEN 515 PROVE_TAC [RTC_CASES1]); 516 517val bnf_reduction_to_self = store_thm( 518 "bnf_reduction_to_self", 519 ``bnf M ==> (M -b->* N <=> (N = M))``, 520 METIS_TAC [corollary3_2_1, beta_normal_form_bnf, RTC_RULES]); 521 522local open relationTheory 523in 524val diamond_property_def = save_thm("diamond_property_def", diamond_def) 525end 526val _ = overload_on("diamond_property", ``relation$diamond``) 527 528(* This is not the same CR as appears in There 529 CR R = diamond (RTC R) 530 Here, 531 CR R = diamond (RTC (compat_closure R)) 532 In other words, this formulation allows us to write 533 CR beta 534 rather than having to write 535 CR (compat_closure beta) 536*) 537val CR_def = Define`CR R = diamond_property (reduction R)`; 538 539val theorem3_13 = store_thm( 540 "theorem3_13", 541 ``!R. CR R ==> 542 !M N. conversion R M N ==> ?Z. reduction R M Z /\ reduction R N Z``, 543 GEN_TAC THEN STRIP_TAC THEN SIMP_TAC (srw_ss()) [] THEN 544 HO_MATCH_MP_TAC equiv_closure_ind THEN REVERSE (SRW_TAC [][]) THEN1 545 (`?Z2. reduction R Z Z2 /\ reduction R Z' Z2` by 546 PROVE_TAC [CR_def, diamond_property_def] THEN 547 PROVE_TAC [reduction_rules]) THEN 548 PROVE_TAC [reduction_rules]); 549 550val corollary3_3_1 = store_thm( 551 "corollary3_3_1", 552 ``!R. CR R ==> (!M N. nf_of R M N ==> reduction R M N) /\ 553 (!M N1 N2. nf_of R M N1 /\ nf_of R M N2 ==> (N1 = N2))``, 554 SRW_TAC [][nf_of_def] THENL [ 555 PROVE_TAC [corollary3_2_1, theorem3_13], 556 `conversion R N1 N2` by 557 (FULL_SIMP_TAC (srw_ss()) [] THEN 558 PROVE_TAC [equiv_closure_rules]) THEN 559 `?Z. reduction R N1 Z /\ reduction R N2 Z` by 560 PROVE_TAC [theorem3_13] THEN 561 PROVE_TAC [corollary3_2_1] 562 ]); 563 564 565val diamond_TC = diamond_TC_diamond 566 567val bvc_cases = store_thm( 568 "bvc_cases", 569 ``!X. FINITE X ==> 570 !t. (?s. t = VAR s) \/ (?t1 t2. t = t1 @@ t2) \/ 571 (?v t0. ~(v IN X) /\ (t = LAM v t0))``, 572 SRW_TAC [][] THEN 573 Q.SPEC_THEN `t` FULL_STRUCT_CASES_TAC term_CASES THEN 574 SRW_TAC [][LAM_eq_thm] THEN 575 SRW_TAC [boolSimps.DNF_ss][] THEN 576 SRW_TAC [][Once tpm_eqr] THEN 577 Q_TAC (NEW_TAC "z") `v INSERT X UNION FV t0` THEN 578 METIS_TAC []); 579 580val (grandbeta_rules, grandbeta_ind, grandbeta_cases) = 581 Hol_reln`(!M. grandbeta M M) /\ 582 (!M M' x. grandbeta M M' ==> grandbeta (LAM x M) (LAM x M')) /\ 583 (!M N M' N'. grandbeta M M' /\ grandbeta N N' ==> 584 grandbeta (M @@ N) (M' @@ N')) /\ 585 (!M N M' N' x. grandbeta M M' /\ grandbeta N N' ==> 586 grandbeta ((LAM x M) @@ N) ([N'/x] M'))`; 587val _ = set_fixity "=b=>" (Infix(NONASSOC,450)) 588val _ = overload_on ("=b=>", ``grandbeta``) 589val _ = set_fixity "=b=>*" (Infix(NONASSOC,450)) 590val _ = overload_on ("=b=>*", ``RTC grandbeta``) 591 592val gbarrow = "=" ^ UnicodeChars.beta ^ "=>" 593val _ = Unicode.unicode_version {u = gbarrow, tmnm = "=b=>"} 594val _ = Unicode.unicode_version {u = gbarrow ^ "*", tmnm = "=b=>*"} 595 596val grandbeta_bvc_gen_ind = store_thm( 597 "grandbeta_bvc_gen_ind", 598 ``!P fv. 599 (!M x. P M M x) /\ 600 (!v M1 M2 x. v NOTIN fv x /\ (!x. P M1 M2 x) ==> 601 P (LAM v M1) (LAM v M2) x) /\ 602 (!M1 M2 N1 N2 x. (!x. P M1 M2 x) /\ (!x. P N1 N2 x) ==> 603 P (M1 @@ N1) (M2 @@ N2) x) /\ 604 (!M1 M2 N1 N2 v x. 605 v NOTIN fv x /\ v NOTIN FV N1 /\ v NOTIN FV N2 /\ 606 (!x. P M1 M2 x) /\ (!x. P N1 N2 x) ==> 607 P ((LAM v M1) @@ N1) ([N2/v]M2) x) /\ 608 (!x. FINITE (fv x)) ==> 609 !M N. M =b=> N ==> !x. P M N x``, 610 REPEAT GEN_TAC THEN STRIP_TAC THEN 611 Q_TAC SUFF_TAC `!M N. grandbeta M N ==> !p x. P (tpm p M) (tpm p N) x` 612 THEN1 METIS_TAC [pmact_nil] THEN 613 HO_MATCH_MP_TAC grandbeta_ind THEN SRW_TAC [][] THENL [ 614 Q.ABBREV_TAC `M' = tpm p M` THEN 615 Q.ABBREV_TAC `N' = tpm p N` THEN 616 Q.ABBREV_TAC `v = lswapstr p x` THEN 617 Q_TAC (NEW_TAC "z") `v INSERT fv x' UNION FV M' UNION FV N'` THEN 618 `(LAM v M' = LAM z (tpm ((z,v)::p) M)) /\ 619 (LAM v N' = LAM z (tpm ((z,v)::p) N))` 620 by (ONCE_REWRITE_TAC [tpm_CONS] THEN 621 SRW_TAC [][Abbr`M'`, Abbr`N'`, tpm_ALPHA]) THEN 622 SRW_TAC [][], 623 Q.MATCH_ABBREV_TAC `P (LAM (lswapstr p v0) (tpm p ML) @@ tpm p MR) 624 (tpm p ([NR/v0] NL)) ctx` THEN 625 markerLib.RM_ALL_ABBREVS_TAC THEN 626 SRW_TAC [][tpm_subst] THEN 627 Q.ABBREV_TAC `v = lswapstr p v0` THEN 628 Q.ABBREV_TAC `M1 = tpm p ML` THEN 629 Q.ABBREV_TAC `N1 = tpm p MR` THEN 630 Q.ABBREV_TAC `M2 = tpm p NL` THEN 631 Q.ABBREV_TAC `N2 = tpm p NR` THEN 632 Q_TAC (NEW_TAC "z") 633 `v INSERT fv ctx UNION FV N1 UNION FV N2 UNION FV M1 UNION 634 FV M2` THEN 635 `LAM v M1 = LAM z (tpm [(z,v)] M1)` by SRW_TAC [][tpm_ALPHA] THEN 636 `[N2/v]M2 = [N2/z](tpm [(z,v)] M2)` 637 by SRW_TAC [][fresh_tpm_subst, lemma15a] THEN 638 SRW_TAC [][] THEN FIRST_X_ASSUM MATCH_MP_TAC THEN 639 SRW_TAC [][Abbr`N1`,Abbr`N2`] THEN 640 `(tpm [(z,v)] M1 = tpm ((z,v)::p) ML) /\ 641 (tpm [(z,v)] M2 = tpm ((z,v)::p) NL)` 642 by SRW_TAC [][GSYM pmact_decompose, Abbr`M1`,Abbr`M2`] THEN 643 SRW_TAC [][] 644 ]); 645 646val grandbeta_bvc_ind = save_thm( 647 "grandbeta_bvc_ind", 648 (Q.GEN `P` o Q.GEN `X` o 649 SIMP_RULE bool_ss [] o 650 SPECL [``(\M:term N:term x:'a. P M N:bool)``, ``\x:'a. X:string -> bool``]) 651 grandbeta_bvc_gen_ind); 652 653val exercise3_3_1 = store_thm( 654 "exercise3_3_1", 655 ``!M N. M -b-> N ==> M =b=> N``, 656 HO_MATCH_MP_TAC compat_closure_ind THEN SRW_TAC [][beta_def] THEN 657 PROVE_TAC [grandbeta_rules]); 658 659val app_grandbeta = store_thm( (* property 3 on p. 37 *) 660 "app_grandbeta", 661 ``!M N L. M @@ N =b=> L <=> 662 (?M' N'. M =b=> M' /\ N =b=> N' /\ (L = M' @@ N')) \/ 663 (?x P P' N'. (M = LAM x P) /\ P =b=> P' /\ 664 N =b=> N' /\ (L = [N'/x]P'))``, 665 REPEAT GEN_TAC THEN EQ_TAC THENL [ 666 SIMP_TAC (srw_ss()) [SimpL ``(==>)``, Once grandbeta_cases] THEN 667 SIMP_TAC (srw_ss()) [DISJ_IMP_THM, GSYM LEFT_FORALL_IMP_THM, 668 grandbeta_rules] THEN PROVE_TAC [], 669 SRW_TAC [][] THEN PROVE_TAC [grandbeta_rules] 670 ]); 671 672val grandbeta_permutative = store_thm( 673 "grandbeta_permutative", 674 ``!M N. M =b=> N ==> !pi. tpm pi M =b=> tpm pi N``, 675 HO_MATCH_MP_TAC grandbeta_ind THEN SRW_TAC [][tpm_subst] THEN 676 METIS_TAC [grandbeta_rules]); 677 678val grandbeta_permutative_eqn = store_thm( 679 "grandbeta_permutative_eqn", 680 ``tpm pi M =b=> tpm pi N <=> M =b=> N``, 681 METIS_TAC [pmact_inverse, grandbeta_permutative]); 682val _ = export_rewrites ["grandbeta_permutative_eqn"] 683 684val grandbeta_substitutive = store_thm( 685 "grandbeta_substitutive", 686 ``!M N. M =b=> N ==> [P/x]M =b=> [P/x]N``, 687 HO_MATCH_MP_TAC grandbeta_bvc_ind THEN 688 Q.EXISTS_TAC `x INSERT FV P` THEN 689 SRW_TAC [][SUB_THM, grandbeta_rules] THEN 690 SRW_TAC [][lemma2_11, grandbeta_rules]); 691 692val grandbeta_FV = store_thm( 693 "grandbeta_FV", 694 ``!M N. M =b=> N ==> FV N SUBSET FV M``, 695 HO_MATCH_MP_TAC grandbeta_ind THEN 696 SRW_TAC [][SUBSET_DEF, FV_SUB] THEN 697 PROVE_TAC []); 698 699val abs_grandbeta = store_thm( 700 "abs_grandbeta", 701 ``!M N v. LAM v M =b=> N <=> ���N0. N = LAM v N0 /\ M =b=> N0``, 702 REPEAT GEN_TAC THEN EQ_TAC THENL [ 703 SIMP_TAC (srw_ss()) [Once grandbeta_cases, SimpL ``(==>)``] THEN 704 SIMP_TAC (srw_ss()) [DISJ_IMP_THM, grandbeta_rules] THEN 705 SRW_TAC [][LAM_eq_thm] THENL [ 706 PROVE_TAC [], 707 SRW_TAC [][LAM_eq_thm, tpm_eqr, pmact_flip_args] THEN 708 PROVE_TAC [SUBSET_DEF, grandbeta_FV] 709 ], 710 PROVE_TAC [grandbeta_rules] 711 ]); 712 713val lemma3_15 = save_thm("lemma3_15", abs_grandbeta); 714 715val redex_grandbeta = store_thm( 716 "redex_grandbeta", 717 ``LAM v M @@ N =b=> L <=> 718 (���M' N'. M =b=> M' /\ N =b=> N' /\ 719 (L = LAM v M' @@ N')) \/ 720 (���M' N'. M =b=> M' /\ N =b=> N' /\ (L = [N'/v]M'))``, 721 SRW_TAC [][app_grandbeta, EQ_IMP_THM] THENL [ 722 PROVE_TAC [abs_grandbeta], 723 FULL_SIMP_TAC (srw_ss()) [LAM_eq_thm] THEN DISJ2_TAC THENL [ 724 METIS_TAC [], 725 SRW_TAC [][] THEN 726 MAP_EVERY Q.EXISTS_TAC [`tpm [(v,x)] P'`, `N'`] THEN 727 SRW_TAC [][] THEN 728 `v NOTIN FV P'` 729 by METIS_TAC [grandbeta_FV, SUBSET_DEF] THEN 730 SRW_TAC [][fresh_tpm_subst, lemma15a] 731 ], 732 METIS_TAC [grandbeta_rules], 733 METIS_TAC [] 734 ]); 735 736val var_grandbeta = store_thm( 737 "var_grandbeta", 738 ``!v N. VAR v =b=> N <=> (N = VAR v)``, 739 REPEAT GEN_TAC THEN ONCE_REWRITE_TAC [grandbeta_cases] THEN 740 SRW_TAC [][]); 741 742val grandbeta_cosubstitutive = store_thm( 743 "grandbeta_cosubstitutive", 744 ``!M. N =b=> N' ==> [N/x] M =b=> [N'/x] M``, 745 HO_MATCH_MP_TAC nc_INDUCTION2 THEN 746 Q.EXISTS_TAC `x INSERT FV N UNION FV N'` THEN 747 SRW_TAC [][grandbeta_rules, SUB_VAR]); 748 749(* property 1 on p37, and Barendregt's lemma 3.2.4 *) 750val grandbeta_subst = store_thm( 751 "grandbeta_subst", 752 ``M =b=> M' /\ N =b=> N' ==> [N/x]M =b=> [N'/x]M'``, 753 Q_TAC SUFF_TAC 754 `!M M'. M =b=> M' ==> N =b=> N' ==> 755 [N/x] M =b=> [N'/x]M'` THEN1 756 METIS_TAC [] THEN 757 HO_MATCH_MP_TAC grandbeta_bvc_ind THEN 758 Q.EXISTS_TAC `x INSERT FV N UNION FV N'` THEN 759 SRW_TAC [][SUB_THM, grandbeta_rules] THENL [ 760 METIS_TAC [grandbeta_cosubstitutive], 761 RES_TAC THEN 762 SRW_TAC [][lemma2_11, grandbeta_rules] 763 ]); 764 765val strong_grandbeta_ind = 766 IndDefLib.derive_strong_induction (grandbeta_rules, grandbeta_ind) 767 768val strong_grandbeta_bvc_gen_ind = 769 (GEN_ALL o 770 SIMP_RULE (srw_ss()) [grandbeta_rules, FORALL_AND_THM, 771 GSYM CONJ_ASSOC] o 772 Q.SPEC `\M N x. P M N x /\ grandbeta M N`) 773 grandbeta_bvc_gen_ind 774 775val lemma3_16 = store_thm( (* p. 37 *) 776 "lemma3_16", 777 ``diamond_property grandbeta``, 778 Q_TAC SUFF_TAC `!M M1. M =b=> M1 ==> 779 !M2. M =b=> M2 ==> 780 ?M3. M1 =b=> M3 /\ M2 =b=> M3` THEN1 781 PROVE_TAC [diamond_property_def] THEN 782 HO_MATCH_MP_TAC strong_grandbeta_bvc_gen_ind THEN Q.EXISTS_TAC `FV` THEN 783 SIMP_TAC (srw_ss()) [] THEN REPEAT CONJ_TAC THENL [ 784 (* reflexive case *) 785 PROVE_TAC [grandbeta_rules], 786 (* lambda case *) 787 MAP_EVERY Q.X_GEN_TAC [`v`, `M`,`M1`, `M2`] THEN REPEAT STRIP_TAC THEN 788 `?P. (M2 = LAM v P) /\ M =b=> P` by PROVE_TAC [abs_grandbeta] THEN 789 SRW_TAC [][] THEN PROVE_TAC [grandbeta_rules], 790 (* app case *) 791 MAP_EVERY Q.X_GEN_TAC [`f`,`g`,`x`,`y`, `fx'`] THEN STRIP_TAC THEN 792 STRIP_TAC THEN 793 `(?f' x'. (fx' = f' @@ x') /\ f =b=> f' /\ x =b=> x') \/ 794 (?v P P' x'. (f = LAM v P) /\ P =b=> P' /\ x =b=> x' /\ 795 (fx' = [x'/v]P'))` by 796 (FULL_SIMP_TAC (srw_ss()) [app_grandbeta] THEN PROVE_TAC []) 797 THENL [ 798 METIS_TAC [grandbeta_rules], 799 `?P2. (g = LAM v P2) /\ P =b=> P2` by 800 PROVE_TAC [abs_grandbeta] THEN 801 SRW_TAC [][] THEN 802 `?ff. LAM v P2 =b=> ff /\ LAM v P' =b=> ff` by 803 PROVE_TAC [grandbeta_rules] THEN 804 `?xx. y =b=> xx /\ x' =b=> xx` by PROVE_TAC [] THEN 805 `?PP. P' =b=> PP /\ (ff = LAM v PP)` by 806 PROVE_TAC [abs_grandbeta] THEN 807 SRW_TAC [][] THEN 808 `P2 =b=> PP` by PROVE_TAC [abs_grandbeta, term_11] THEN 809 PROVE_TAC [grandbeta_rules, grandbeta_subst] 810 ], 811 (* beta-redex case *) 812 MAP_EVERY Q.X_GEN_TAC [`M`, `M'`, `N`, `N'`, `x`, `M2`] THEN 813 SRW_TAC [][redex_grandbeta] THENL [ 814 (* other reduction didn't beta-reduce *) 815 `?Mfin. M' =b=> Mfin /\ M'' =b=> Mfin` by METIS_TAC [] THEN 816 `?Nfin. N' =b=> Nfin /\ N'' =b=> Nfin` by METIS_TAC [] THEN 817 Q.EXISTS_TAC `[Nfin/x]Mfin` THEN 818 METIS_TAC [grandbeta_rules, grandbeta_subst], 819 (* other reduction also beta-reduced *) 820 `?Mfin. M' =b=> Mfin /\ M'' =b=> Mfin` by METIS_TAC [] THEN 821 `?Nfin. N' =b=> Nfin /\ N'' =b=> Nfin` by METIS_TAC [] THEN 822 Q.EXISTS_TAC `[Nfin/x]Mfin` THEN 823 METIS_TAC [grandbeta_rules, grandbeta_subst] 824 ] 825 ]); 826 827val theorem3_17 = store_thm( 828 "theorem3_17", 829 ``TC grandbeta = reduction beta``, 830 Q_TAC SUFF_TAC 831 `(!M N. TC grandbeta M N ==> reduction beta M N) /\ 832 (!M N. RTC (compat_closure beta) M N ==> TC grandbeta M N)` 833 THEN1 SRW_TAC [] [FUN_EQ_THM, EQ_IMP_THM] THEN 834 CONJ_TAC THENL [ 835 Q_TAC SUFF_TAC `!M N. grandbeta M N ==> reduction beta M N` 836 THEN1 (PROVE_TAC [TC_IDEM, TC_RC_EQNS, 837 TC_MONOTONE]) THEN 838 HO_MATCH_MP_TAC grandbeta_ind THEN PROVE_TAC [reduction_rules, beta_def], 839 840 Q_TAC SUFF_TAC `!M N. RC (compat_closure beta) M N ==> grandbeta M N` 841 THEN1 PROVE_TAC [TC_MONOTONE, 842 TC_RC_EQNS] THEN 843 Q_TAC SUFF_TAC `!M N. compat_closure beta M N ==> grandbeta M N` 844 THEN1 PROVE_TAC [RC_DEF, grandbeta_rules] THEN 845 PROVE_TAC [exercise3_3_1] 846 ]); 847 848val beta_CR = store_thm( 849 "beta_CR", 850 ``CR beta``, 851 PROVE_TAC [CR_def, lemma3_16, theorem3_17, diamond_TC]); 852 853val betaCR_square = store_thm( 854 "betaCR_square", 855 ``M -b->* N1 /\ M -b->* N2 ==> ?N. N1 -b->* N /\ N2 -b->* N``, 856 METIS_TAC [beta_CR, diamond_property_def, CR_def]); 857 858val bnf_triangle = store_thm( 859 "bnf_triangle", 860 ``M -b->* N /\ M -b->* N' /\ bnf N ==> N' -b->* N``, 861 METIS_TAC [betaCR_square, bnf_reduction_to_self]); 862 863val Omega_starloops = Store_thm( 864 "Omega_starloops", 865 ``Omega -b->* N <=> (N = Omega)``, 866 Q_TAC SUFF_TAC `!M N. M -b->* N ==> (M = Omega) ==> (N = Omega)` 867 THEN1 METIS_TAC [RTC_RULES] THEN 868 HO_MATCH_MP_TAC RTC_INDUCT THEN SRW_TAC [][] THEN 869 FULL_SIMP_TAC (srw_ss()) [ccbeta_rwt, Omega_def]); 870 871val lameq_betaconversion = store_thm( 872 "lameq_betaconversion", 873 ``!M N. M == N <=> conversion beta M N``, 874 SIMP_TAC (srw_ss()) [EQ_IMP_THM, FORALL_AND_THM] THEN CONJ_TAC THENL [ 875 HO_MATCH_MP_TAC lameq_ind THEN REPEAT STRIP_TAC THENL [ 876 Q_TAC SUFF_TAC `beta (LAM x M @@ N) ([N/x] M)` THEN1 877 PROVE_TAC [conversion_rules] THEN 878 SRW_TAC [][beta_def] THEN PROVE_TAC [], 879 PROVE_TAC [conversion_rules], 880 PROVE_TAC [conversion_rules], 881 PROVE_TAC [conversion_rules], 882 PROVE_TAC [conversion_compatible, compatible_def, rightctxt, 883 rightctxt_thm], 884 PROVE_TAC [conversion_compatible, compatible_def, leftctxt], 885 PROVE_TAC [conversion_compatible, compatible_def, absctxt] 886 ], 887 SIMP_TAC (srw_ss()) [] THEN 888 HO_MATCH_MP_TAC equiv_closure_ind THEN REPEAT CONJ_TAC THEN1 889 (HO_MATCH_MP_TAC compat_closure_ind THEN SRW_TAC [][beta_def] THEN 890 PROVE_TAC [lameq_rules]) THEN 891 PROVE_TAC [lameq_rules] 892 ]); 893 894val prop3_18 = save_thm("prop3_18", lameq_betaconversion); 895 896val ccbeta_lameq = store_thm( 897 "ccbeta_lameq", 898 ``!M N. M -b-> N ==> M == N``, 899 SRW_TAC [][lameq_betaconversion, EQC_R]); 900val betastar_lameq = store_thm( 901 "betastar_lameq", 902 ``!M N. M -b->* N ==> M == N``, 903 SRW_TAC [][lameq_betaconversion, RTC_EQC]); 904 905val betastar_lameq_bnf = store_thm( 906 "betastar_lameq_bnf", 907 ``bnf N ==> (M -b->* N <=> M == N)``, 908 METIS_TAC [theorem3_13, beta_CR, betastar_lameq, bnf_reduction_to_self, 909 lameq_betaconversion]); 910 911val lameq_consistent = store_thm( 912 "lameq_consistent", 913 ``consistent $==``, 914 SRW_TAC [][consistent_def] THEN 915 MAP_EVERY Q.EXISTS_TAC [`S`,`K`] THEN STRIP_TAC THEN 916 `conversion beta S K` by PROVE_TAC [prop3_18] THEN 917 `?Z. reduction beta S Z /\ reduction beta K Z` by 918 PROVE_TAC [theorem3_13, beta_CR] THEN 919 `normal_form beta S` by PROVE_TAC [S_beta_normal, beta_normal_form_bnf] THEN 920 `normal_form beta K` by PROVE_TAC [K_beta_normal, beta_normal_form_bnf] THEN 921 `S = K` by PROVE_TAC [corollary3_2_1] THEN 922 FULL_SIMP_TAC (srw_ss()) [S_def, K_def]); 923 924val has_bnf_thm = store_thm( 925 "has_bnf_thm", 926 ``has_bnf M <=> ?N. M -b->* N /\ bnf N``, 927 EQ_TAC THENL [ 928 METIS_TAC [lameq_betaconversion, chap2Theory.has_bnf_def, theorem3_13, 929 beta_CR, beta_normal_form_bnf, corollary3_2_1], 930 SRW_TAC [][chap2Theory.has_bnf_def, lameq_betaconversion] THEN 931 METIS_TAC [RTC_EQC] 932 ]); 933 934val Omega_reachable_no_bnf = store_thm( 935 "Omega_reachable_no_bnf", 936 ``M -b->* Omega ==> ~has_bnf M``, 937 REPEAT STRIP_TAC THEN 938 FULL_SIMP_TAC (srw_ss()) [has_bnf_thm] THEN 939 `Omega -b->* N` by METIS_TAC [bnf_triangle] THEN 940 `N = Omega` by FULL_SIMP_TAC (srw_ss()) [] THEN 941 FULL_SIMP_TAC (srw_ss()) []); 942 943val weak_diamond_def = 944 save_thm("weak_diamond_def", WCR_def) 945val _ = overload_on("weak_diamond", ``relation$WCR``) 946 947(* likewise, these definitions of WCR and SN, differ from those in 948 relation by wrapping the argument in a call to compat_closure 949*) 950val WCR_def = (* definition 3.20, p39 *) Define` 951 WCR R = weak_diamond (compat_closure R) 952`; 953 954val SN_def = Define`SN R = relation$SN (compat_closure R)`; 955 956val newmans_lemma = store_thm( (* lemma3_22, p39 *) 957 "newmans_lemma", 958 ``!R. SN R /\ WCR R ==> CR R``, 959 SIMP_TAC (srw_ss()) [SN_def, WCR_def, Newmans_lemma, 960 CR_def, 961 GSYM relationTheory.diamond_def, 962 GSYM relationTheory.CR_def]); 963 964val commute_def = (* p43 *) 965 Define`commute R1 R2 = !x x1 x2. R1 x x1 /\ R2 x x2 ==> 966 ?x3. R2 x1 x3 /\ R1 x2 x3`; 967 968val commute_COMM = store_thm( 969 "commute_COMM", 970 ``commute R1 R2 = commute R2 R1``, 971 PROVE_TAC [commute_def]); 972 973val diamond_RC = diamond_RC_diamond 974 (* |- !R. diamond_property R ==> diamond_property (RC R) *) 975 976val diamond_RTC = store_thm( 977 "diamond_RTC", 978 ``!R. diamond_property R ==> diamond_property (RTC R)``, 979 PROVE_TAC [diamond_TC, diamond_RC, TC_RC_EQNS]); 980 981val hr_lemma0 = prove( 982 ``!R1 R2. diamond_property R1 /\ diamond_property R2 /\ commute R1 R2 ==> 983 diamond_property (RTC (R1 RUNION R2))``, 984 REPEAT STRIP_TAC THEN 985 Q_TAC SUFF_TAC `diamond_property (R1 RUNION R2)` THEN1 986 PROVE_TAC [diamond_RTC] THEN 987 FULL_SIMP_TAC (srw_ss()) [diamond_property_def, commute_def, 988 RUNION] THEN 989 PROVE_TAC []); 990 991val RUNION_RTC_MONOTONE = store_thm( 992 "RUNION_RTC_MONOTONE", 993 ``!R1 x y. RTC R1 x y ==> !R2. RTC (R1 RUNION R2) x y``, 994 GEN_TAC THEN HO_MATCH_MP_TAC RTC_INDUCT THEN 995 PROVE_TAC [RTC_RULES, RUNION]); 996 997val RTC_OUT = store_thm( 998 "RTC_OUT", 999 ``!R1 R2. RTC (RTC R1 RUNION RTC R2) = RTC (R1 RUNION R2)``, 1000 REPEAT GEN_TAC THEN 1001 Q_TAC SUFF_TAC 1002 `(!x y. RTC (RTC R1 RUNION RTC R2) x y ==> RTC (R1 RUNION R2) x y) /\ 1003 (!x y. RTC (R1 RUNION R2) x y ==> RTC (RTC R1 RUNION RTC R2) x y)` THEN1 1004 (SIMP_TAC (srw_ss()) [FUN_EQ_THM, EQ_IMP_THM, FORALL_AND_THM] THEN 1005 PROVE_TAC []) THEN CONJ_TAC 1006 THEN HO_MATCH_MP_TAC RTC_INDUCT THENL [ 1007 CONJ_TAC THENL [ 1008 PROVE_TAC [RTC_RULES], 1009 MAP_EVERY Q.X_GEN_TAC [`x`,`y`,`z`] THEN REPEAT STRIP_TAC THEN 1010 `RTC R1 x y \/ RTC R2 x y` by PROVE_TAC [RUNION] THEN 1011 PROVE_TAC [RUNION_RTC_MONOTONE, RTC_RTC, RUNION_COMM] 1012 ], 1013 CONJ_TAC THENL [ 1014 PROVE_TAC [RTC_RULES], 1015 MAP_EVERY Q.X_GEN_TAC [`x`,`y`,`z`] THEN REPEAT STRIP_TAC THEN 1016 `R1 x y \/ R2 x y` by PROVE_TAC [RUNION] THEN 1017 PROVE_TAC [RTC_RULES, RUNION] 1018 ] 1019 ]); 1020 1021 1022val CC_RUNION_MONOTONE = store_thm( 1023 "CC_RUNION_MONOTONE", 1024 ``!R1 x y. compat_closure R1 x y ==> compat_closure (R1 RUNION R2) x y``, 1025 GEN_TAC THEN HO_MATCH_MP_TAC compat_closure_ind THEN 1026 PROVE_TAC [compat_closure_rules, RUNION]); 1027 1028val CC_RUNION_DISTRIB = store_thm( 1029 "CC_RUNION_DISTRIB", 1030 ``!R1 R2. compat_closure (R1 RUNION R2) = 1031 compat_closure R1 RUNION compat_closure R2``, 1032 REPEAT GEN_TAC THEN 1033 Q_TAC SUFF_TAC 1034 `(!x y. compat_closure (R1 RUNION R2) x y ==> 1035 (compat_closure R1 RUNION compat_closure R2) x y) /\ 1036 (!x y. (compat_closure R1 RUNION compat_closure R2) x y ==> 1037 compat_closure (R1 RUNION R2) x y)` THEN1 1038 SIMP_TAC (srw_ss()) [FUN_EQ_THM, EQ_IMP_THM, FORALL_AND_THM] THEN 1039 CONJ_TAC THENL [ 1040 HO_MATCH_MP_TAC compat_closure_ind THEN 1041 PROVE_TAC [compat_closure_rules, RUNION], 1042 SRW_TAC [][RUNION] THEN 1043 PROVE_TAC [RUNION_COMM, CC_RUNION_MONOTONE] 1044 ]); 1045 1046val hindley_rosen_lemma = store_thm( (* p43 *) 1047 "hindley_rosen_lemma", 1048 ``(!R1 R2. diamond_property R1 /\ diamond_property R2 /\ commute R1 R2 ==> 1049 diamond_property (RTC (R1 RUNION R2))) /\ 1050 (!R1 R2. CR R1 /\ CR R2 /\ commute (reduction R1) (reduction R2) ==> 1051 CR (R1 RUNION R2))``, 1052 CONJ_TAC THENL [ 1053 MATCH_ACCEPT_TAC hr_lemma0, 1054 SRW_TAC [][CR_def] THEN 1055 `diamond_property (RTC (RTC (compat_closure R1) RUNION 1056 RTC (compat_closure R2)))` 1057 by PROVE_TAC [hr_lemma0] THEN 1058 FULL_SIMP_TAC (srw_ss()) [RTC_OUT, CC_RUNION_DISTRIB] 1059 ]); 1060 1061val eta_def = 1062 Define`eta M N <=> ���v. M = LAM v (N @@ VAR v) ��� v ��� FV N`; 1063 1064val _ = Unicode.unicode_version {u = UnicodeChars.eta, tmnm = "eta"} 1065 1066val eta_normal_form_enf = store_thm( 1067 "eta_normal_form_enf", 1068 ``normal_form eta = enf``, 1069 Q_TAC SUFF_TAC `(!x. ~enf x ==> can_reduce eta x) /\ 1070 (!x. can_reduce eta x ==> ~enf x)` THEN1 1071 (SIMP_TAC (srw_ss())[normal_form_def, FUN_EQ_THM, EQ_IMP_THM, 1072 FORALL_AND_THM] THEN PROVE_TAC []) THEN 1073 CONJ_TAC THENL [ 1074 HO_MATCH_MP_TAC nc_INDUCTION2 THEN Q.EXISTS_TAC `{}` THEN 1075 SRW_TAC [][] THENL [ 1076 PROVE_TAC [can_reduce_rules], 1077 PROVE_TAC [can_reduce_rules], 1078 PROVE_TAC [can_reduce_rules, lemma14a], 1079 Q_TAC SUFF_TAC `?u. eta (LAM y x) u` THEN1 1080 PROVE_TAC [can_reduce_rules, redex_def] THEN 1081 FULL_SIMP_TAC (srw_ss()) [is_comb_APP_EXISTS, eta_def] THEN 1082 SRW_TAC [][] THEN 1083 FULL_SIMP_TAC (srw_ss()) [rand_thm, rator_thm] THEN PROVE_TAC [] 1084 ], 1085 HO_MATCH_MP_TAC can_reduce_ind THEN 1086 SRW_TAC [][redex_def, eta_def] THEN 1087 SRW_TAC [][] 1088 ]); 1089 1090val no_eta_thm = store_thm( 1091 "no_eta_thm", 1092 ``(!s t. ~(eta (VAR s) t)) /\ 1093 (!t u v. ~(eta (t @@ u) v))``, 1094 SRW_TAC [][eta_def]); 1095 1096val cc_eta_thm = store_thm( 1097 "cc_eta_thm", 1098 ``(!s t. compat_closure eta (VAR s) t <=> F) /\ 1099 (!t u v. compat_closure eta (t @@ u) v <=> 1100 (?t'. (v = t' @@ u) /\ compat_closure eta t t') \/ 1101 (?u'. (v = t @@ u') /\ compat_closure eta u u'))``, 1102 REPEAT CONJ_TAC THEN 1103 SIMP_TAC (srw_ss()) [SimpLHS, Once compat_closure_cases] THEN 1104 SIMP_TAC (srw_ss()) [no_eta_thm, EQ_IMP_THM, DISJ_IMP_THM, 1105 GSYM LEFT_FORALL_IMP_THM, RIGHT_AND_OVER_OR, 1106 LEFT_AND_OVER_OR, FORALL_AND_THM, 1107 is_comb_APP_EXISTS, GSYM LEFT_EXISTS_AND_THM]); 1108 1109val eta_substitutive = store_thm( 1110 "eta_substitutive", 1111 ``substitutive eta``, 1112 SRW_TAC [][substitutive_def, eta_def] THEN 1113 Q_TAC (NEW_TAC "z") `{v;v'} UNION FV M' UNION FV N` THEN 1114 `LAM v (M' @@ VAR v) = LAM z ([VAR z/v] (M' @@ VAR v))` 1115 by SRW_TAC [][SIMPLE_ALPHA] THEN 1116 ` _ = LAM z ([VAR z/v] M' @@ VAR z)` by SRW_TAC [][SUB_THM] THEN 1117 ASM_SIMP_TAC (srw_ss()) [SUB_THM, lemma14b] THEN 1118 Q.EXISTS_TAC `z` THEN SRW_TAC [][FV_SUB]); 1119 1120val cc_eta_subst = store_thm( 1121 "cc_eta_subst", 1122 ``!M N. compat_closure eta M N ==> 1123 !P v. compat_closure eta ([P/v] M) ([P/v] N)``, 1124 METIS_TAC [eta_substitutive, compat_closure_substitutive, substitutive_def]); 1125 1126val cc_eta_tpm = store_thm( 1127 "cc_eta_tpm", 1128 ``!M N. compat_closure eta M N ==> 1129 compat_closure eta (tpm pi M) (tpm pi N)``, 1130 METIS_TAC [compat_closure_permutative, substitutive_implies_permutative, 1131 eta_substitutive, permutative_def]) 1132val cc_eta_tpm_eqn = store_thm( 1133 "cc_eta_tpm_eqn", 1134 ``compat_closure eta (tpm pi M) N = 1135 compat_closure eta M (tpm (REVERSE pi) N)``, 1136 METIS_TAC [cc_eta_tpm, pmact_inverse]); 1137 1138val eta_deterministic = store_thm( 1139 "eta_deterministic", 1140 ``!M N1 N2. eta M N1 /\ eta M N2 ==> (N1 = N2)``, 1141 SIMP_TAC (srw_ss() ++ boolSimps.DNF_ss) [eta_def, LAM_eq_thm, tpm_fresh]); 1142 1143val cc_eta_FV_SUBSET = store_thm( 1144 "cc_eta_FV_SUBSET", 1145 ``!M N. compat_closure eta M N ==> FV N SUBSET FV M``, 1146 HO_MATCH_MP_TAC compat_closure_ind THEN 1147 SIMP_TAC (srw_ss()) [SUBSET_DEF] THEN 1148 Q_TAC SUFF_TAC `!M N. eta M N ==> !s. s IN FV N ==> s IN FV M` THEN1 1149 PROVE_TAC [] THEN 1150 SIMP_TAC (srw_ss()) [eta_def, GSYM LEFT_FORALL_IMP_THM]); 1151 1152val cc_eta_LAM = store_thm( 1153 "cc_eta_LAM", 1154 ``!t v u. compat_closure eta (LAM v t) u <=> 1155 (?t'. (u = LAM v t') /\ compat_closure eta t t') \/ 1156 eta (LAM v t) u``, 1157 SIMP_TAC (srw_ss()) [Once compat_closure_cases, SimpLHS] THEN 1158 SIMP_TAC (srw_ss() ++ boolSimps.DNF_ss)[LAM_eq_thm, EQ_IMP_THM, tpm_eqr, 1159 cc_eta_tpm_eqn, pmact_flip_args] THEN 1160 REPEAT STRIP_TAC THEN DISJ1_TAC THEN 1161 Q_TAC SUFF_TAC `~(v' IN FV (tpm [(v,v')] y))` THEN1 SRW_TAC [][] THEN 1162 METIS_TAC [cc_eta_FV_SUBSET, SUBSET_DEF]); 1163 1164val eta_LAM = store_thm( 1165 "eta_LAM", 1166 ``!v t u. eta (LAM v t) u <=> t = u @@ VAR v ��� v ��� FV u``, 1167 SRW_TAC [][eta_def, LAM_eq_thm, EQ_IMP_THM] THEN SRW_TAC [][tpm_fresh] THEN 1168 SRW_TAC [boolSimps.DNF_ss][]); 1169 1170val CR_eta_lemma = prove( 1171 ``!M M1 M2. eta M M1 /\ compat_closure eta M M2 /\ ~(M1 = M2) ==> 1172 ?M3. compat_closure eta M1 M3 /\ compat_closure eta M2 M3``, 1173 REPEAT STRIP_TAC THEN 1174 `?v. (M = LAM v (M1 @@ VAR v)) /\ ~(v IN FV M1)` by PROVE_TAC [eta_def] THEN 1175 FULL_SIMP_TAC (srw_ss()) [cc_eta_LAM, cc_eta_thm] THENL [ 1176 Q.EXISTS_TAC `rator t'` THEN 1177 SRW_TAC [][eta_LAM] THEN 1178 METIS_TAC [cc_eta_FV_SUBSET, SUBSET_DEF], 1179 FULL_SIMP_TAC (srw_ss()) [eta_LAM] 1180 ]); 1181 1182val cc_strong_ind = 1183 IndDefLib.derive_strong_induction (compat_closure_rules, compat_closure_ind) 1184 1185val eta_diamond = prove( 1186 ``!M M1. compat_closure eta M M1 ==> 1187 !M2. compat_closure eta M M2 /\ ~(M1 = M2) ==> 1188 ?M3. compat_closure eta M1 M3 /\ 1189 compat_closure eta M2 M3``, 1190 HO_MATCH_MP_TAC cc_strong_ind THEN REPEAT CONJ_TAC THENL [ 1191 PROVE_TAC [CR_eta_lemma], 1192 1193 SRW_TAC [][cc_eta_thm] THEN 1194 FULL_SIMP_TAC (srw_ss() ++ boolSimps.DNF_ss) [cc_eta_thm], 1195 1196 SRW_TAC [][cc_eta_thm] THEN 1197 FULL_SIMP_TAC (srw_ss() ++ boolSimps.DNF_ss) [cc_eta_thm], 1198 1199 SRW_TAC [][cc_eta_LAM, eta_LAM] THEN 1200 FULL_SIMP_TAC (srw_ss() ++ boolSimps.DNF_ss) [cc_eta_LAM, cc_eta_thm] THEN 1201 METIS_TAC [cc_eta_FV_SUBSET, SUBSET_DEF] 1202 ]); 1203 1204val eta_CR = store_thm( 1205 "eta_CR", 1206 ``CR eta``, 1207 Q_TAC SUFF_TAC `diamond_property (RC (compat_closure eta))` THEN1 1208 (SRW_TAC [][CR_def] THEN 1209 PROVE_TAC [TC_RC_EQNS, diamond_TC]) THEN 1210 SIMP_TAC (srw_ss()) [diamond_property_def, RC_DEF, 1211 RIGHT_AND_OVER_OR, LEFT_AND_OVER_OR, EXISTS_OR_THM, 1212 DISJ_IMP_THM, FORALL_AND_THM] THEN 1213 PROVE_TAC [eta_diamond]); 1214 1215val wonky_diamond_commutes = store_thm( (* Barendregt, lemma 3.3.6 *) 1216 "wonky_diamond_commutes", 1217 ``!R1 R2. 1218 (!x y z. R1 x y /\ R2 x z ==> ?w. RTC R1 z w /\ RC R2 y w) ==> 1219 commute (RTC R1) (RTC R2)``, 1220 REPEAT STRIP_TAC THEN 1221 `!x y. RTC R1 x y ==> !z. R2 x z ==> ?w. RTC R1 z w /\ RTC R2 y w` by 1222 (HO_MATCH_MP_TAC RTC_STRONG_INDUCT THEN 1223 CONJ_TAC THENL [ 1224 PROVE_TAC [RTC_RULES], 1225 MAP_EVERY Q.X_GEN_TAC [`x`,`y`,`z`] THEN REPEAT STRIP_TAC THEN 1226 `?w. RC R2 y w /\ RTC R1 z' w` by PROVE_TAC [] THEN 1227 FULL_SIMP_TAC (srw_ss()) [RC_DEF] THEN 1228 PROVE_TAC [RTC_RTC, RTC_RULES] 1229 ]) THEN 1230 Q_TAC SUFF_TAC 1231 `!x y. RTC R2 x y ==> !z. RTC R1 x z ==> 1232 ?w. RTC R2 z w /\ RTC R1 y w` THEN1 1233 (SRW_TAC [][commute_def] THEN PROVE_TAC []) THEN 1234 HO_MATCH_MP_TAC RTC_INDUCT THEN 1235 PROVE_TAC [RTC_RULES, RTC_RTC]); 1236 1237val eta_cosubstitutive = store_thm( 1238 "eta_cosubstitutive", 1239 ``!P M N x. compat_closure eta M N ==> reduction eta ([M/x] P) ([N/x] P)``, 1240 REPEAT GEN_TAC THEN Q.ID_SPEC_TAC `P` THEN 1241 HO_MATCH_MP_TAC nc_INDUCTION2 THEN 1242 Q.EXISTS_TAC `x INSERT FV M UNION FV N` THEN 1243 SRW_TAC [][SUB_THM, SUB_VAR] THEN 1244 PROVE_TAC [reduction_rules]); 1245 1246val ccredex = prove( 1247 ``compat_closure beta (LAM v M @@ N) ([N/v]M)``, 1248 SRW_TAC [][cc_beta_thm] THEN METIS_TAC []) 1249 1250val strong_ccbeta_gen_ind = save_thm( 1251 "strong_ccbeta_gen_ind", 1252 (GEN_ALL o 1253 SIMP_RULE (srw_ss() ++ SatisfySimps.SATISFY_ss) 1254 [compat_closure_rules, FORALL_AND_THM, ccredex, 1255 GSYM CONJ_ASSOC] o 1256 Q.INST [`P` |-> `\M N x. P M N x /\ compat_closure beta M N`]) 1257 ccbeta_gen_ind) 1258 1259val eta_beta_commute = store_thm( 1260 "eta_beta_commute", 1261 ``commute (reduction eta) (reduction beta)``, 1262 SIMP_TAC (srw_ss()) [] THEN 1263 MATCH_MP_TAC wonky_diamond_commutes THEN 1264 Q_TAC SUFF_TAC 1265 `!M P. M -b-> P ==> 1266 !N. compat_closure eta M N ==> 1267 ?Q. reduction eta P Q /\ RC (-b->) N Q` 1268 THEN1 PROVE_TAC [] THEN 1269 HO_MATCH_MP_TAC strong_ccbeta_gen_ind THEN 1270 Q.EXISTS_TAC `FV` THEN SRW_TAC [][] THENL [ 1271 FULL_SIMP_TAC (srw_ss()) [cc_eta_thm, cc_eta_LAM] THENL [ 1272 Q.EXISTS_TAC `[P/v]t''` THEN 1273 `compat_closure eta ([P/v]M) ([P/v]t'')` 1274 by METIS_TAC [cc_eta_subst] THEN 1275 `compat_closure beta (LAM v t'' @@ P) ([P/v]t'')` 1276 by METIS_TAC [beta_def, compat_closure_rules] THEN 1277 METIS_TAC [RC_DEF, reduction_rules], 1278 FULL_SIMP_TAC (srw_ss()) [eta_LAM, SUB_THM, lemma14b] THEN 1279 Q.EXISTS_TAC `t' @@ P` THEN 1280 METIS_TAC [reduction_rules, RC_DEF], 1281 Q.EXISTS_TAC `[u'/v]M` THEN 1282 METIS_TAC [RC_DEF, eta_cosubstitutive, beta_def, 1283 compat_closure_rules] 1284 ], 1285 1286 FULL_SIMP_TAC (srw_ss()) [cc_eta_thm] THEN 1287 METIS_TAC [compat_closure_rules, RC_DEF, 1288 reduction_rules], 1289 FULL_SIMP_TAC (srw_ss()) [cc_eta_thm] THEN 1290 METIS_TAC [compat_closure_rules, RC_DEF, 1291 reduction_rules], 1292 1293 FULL_SIMP_TAC (srw_ss()) [cc_eta_LAM, eta_LAM] THENL [ 1294 METIS_TAC [compat_closure_rules, RC_DEF, 1295 reduction_rules], 1296 FULL_SIMP_TAC (srw_ss()) [cc_beta_thm] THENL [ 1297 SRW_TAC [][] THEN FULL_SIMP_TAC (srw_ss()) [] THEN 1298 Cases_on `v = v'` THEN FULL_SIMP_TAC (srw_ss()) [] THENL [ 1299 METIS_TAC [reduction_rules, RC_DEF], 1300 `LAM v ([VAR v/v'] M0) = LAM v' M0` 1301 by METIS_TAC [SIMPLE_ALPHA] THEN 1302 METIS_TAC [reduction_rules, RC_DEF] 1303 ], 1304 `v NOTIN FV M'` by METIS_TAC [cc_beta_FV_SUBSET, SUBSET_DEF] THEN 1305 `compat_closure eta (LAM v (M' @@ VAR v)) M'` 1306 by SRW_TAC [][cc_eta_LAM, eta_LAM] THEN 1307 METIS_TAC [RC_DEF, reduction_rules] 1308 ] 1309 ] 1310 ]) 1311 1312val beta_eta_CR = store_thm( 1313 "beta_eta_CR", 1314 ``CR (beta RUNION eta)``, 1315 MATCH_MP_TAC (CONJUNCT2 hindley_rosen_lemma) THEN 1316 PROVE_TAC [beta_CR, eta_CR, eta_beta_commute, commute_COMM]); 1317 1318val beta_eta_lameta = store_thm( 1319 "beta_eta_lameta", 1320 ``conversion (beta RUNION eta) = lameta``, 1321 SIMP_TAC (srw_ss()) [FUN_EQ_THM, EQ_IMP_THM, FORALL_AND_THM] THEN 1322 CONJ_TAC THENL [ 1323 SIMP_TAC (srw_ss()) [] THEN 1324 HO_MATCH_MP_TAC equiv_closure_ind THEN 1325 REPEAT CONJ_TAC THEN1 1326 (HO_MATCH_MP_TAC compat_closure_ind THEN 1327 REPEAT CONJ_TAC THEN1 1328 (SRW_TAC [][beta_def, eta_def, RUNION] THEN 1329 PROVE_TAC [lameta_rules]) THEN 1330 PROVE_TAC [lameta_rules]) THEN 1331 PROVE_TAC [lameta_rules], 1332 CONV_TAC (RENAME_VARS_CONV ["M", "N"]) THEN HO_MATCH_MP_TAC lameta_ind THEN 1333 REPEAT STRIP_TAC THENL [ 1334 `(beta RUNION eta) (LAM x M @@ N) ([N/x]M)` by 1335 (SRW_TAC [][beta_def, RUNION] THEN PROVE_TAC []) THEN 1336 PROVE_TAC [conversion_rules], 1337 PROVE_TAC [conversion_rules], 1338 PROVE_TAC [conversion_rules], 1339 PROVE_TAC [conversion_rules], 1340 PROVE_TAC [conversion_compatible, compatible_def, rightctxt, 1341 rightctxt_thm], 1342 PROVE_TAC [conversion_compatible, compatible_def, leftctxt], 1343 PROVE_TAC [conversion_compatible, compatible_def, absctxt], 1344 `(beta RUNION eta) (LAM x (N @@ VAR x)) N` by 1345 (SRW_TAC [][eta_def, RUNION] THEN PROVE_TAC []) THEN 1346 PROVE_TAC [conversion_rules] 1347 ] 1348 ]); 1349 1350val beta_eta_normal_form_benf = store_thm( 1351 "beta_eta_normal_form_benf", 1352 ``normal_form (beta RUNION eta) = benf``, 1353 SIMP_TAC (srw_ss()) [FUN_EQ_THM, EQ_IMP_THM, benf_def, FORALL_AND_THM, 1354 normal_form_def] THEN CONJ_TAC 1355 THENL [ 1356 Q_TAC SUFF_TAC `!M. ~bnf M \/ ~enf M ==> can_reduce (beta RUNION eta) M` 1357 THEN1 PROVE_TAC [] THEN 1358 HO_MATCH_MP_TAC simple_induction THEN REPEAT CONJ_TAC THENL [ 1359 SRW_TAC [][bnf_thm, enf_thm], (* var case *) 1360 MAP_EVERY Q.X_GEN_TAC [`f`, `x`] THEN (* app case *) 1361 SRW_TAC [][bnf_thm, enf_thm] THENL [ 1362 PROVE_TAC [can_reduce_rules], 1363 PROVE_TAC [can_reduce_rules], 1364 `redex (beta RUNION eta) (f @@ x)` by 1365 (SRW_TAC [][redex_def, RUNION, beta_def, 1366 EXISTS_OR_THM] THEN 1367 PROVE_TAC [is_abs_thm, term_CASES]) THEN 1368 PROVE_TAC [can_reduce_rules], 1369 PROVE_TAC [can_reduce_rules], 1370 PROVE_TAC [can_reduce_rules] 1371 ], 1372 1373 MAP_EVERY Q.X_GEN_TAC [`x`, `M`] THEN 1374 SRW_TAC [][bnf_thm, enf_thm] THENL [ 1375 PROVE_TAC [can_reduce_rules, lemma14a], 1376 PROVE_TAC [can_reduce_rules, lemma14a], 1377 Q_TAC SUFF_TAC `redex (beta RUNION eta) (LAM x M)` THEN1 1378 PROVE_TAC [can_reduce_rules] THEN 1379 SRW_TAC [][redex_def, RUNION, eta_def] THEN 1380 PROVE_TAC [is_comb_rator_rand] 1381 ] 1382 ], 1383 Q_TAC SUFF_TAC `!x. can_reduce (beta RUNION eta) x ==> ~bnf x \/ ~enf x` 1384 THEN1 PROVE_TAC [] THEN 1385 HO_MATCH_MP_TAC can_reduce_ind THEN 1386 SIMP_TAC (srw_ss()) [bnf_thm, enf_thm, DISJ_IMP_THM, redex_def, 1387 RUNION, GSYM LEFT_FORALL_IMP_THM, 1388 beta_def, eta_def] 1389 ]); 1390 1391val lameta_consistent = store_thm( 1392 "lameta_consistent", 1393 ``consistent lameta``, 1394 SIMP_TAC (srw_ss()) [consistent_def, GSYM beta_eta_lameta] THEN 1395 MAP_EVERY Q.EXISTS_TAC [`S`, `K`] THEN STRIP_TAC THEN 1396 `?Z. reduction (beta RUNION eta) S Z /\ reduction (beta RUNION eta) K Z` by 1397 PROVE_TAC [theorem3_13, beta_eta_CR] THEN 1398 `normal_form (beta RUNION eta) S` by 1399 SRW_TAC [][beta_eta_normal_form_benf, benf_def, bnf_thm, enf_thm, 1400 S_def] THEN 1401 `normal_form (beta RUNION eta) K` by 1402 SRW_TAC [][beta_eta_normal_form_benf, benf_def, bnf_thm, enf_thm, 1403 K_def] THEN 1404 `S = K` by PROVE_TAC [corollary3_2_1] THEN 1405 FULL_SIMP_TAC (srw_ss()) [S_def, K_def]); 1406 1407val is_comb_subst = store_thm( 1408 "is_comb_subst", 1409 ``!t u v. is_comb t ==> is_comb ([u/v]t)``, 1410 SIMP_TAC (srw_ss()) [SUB_THM, is_comb_APP_EXISTS, 1411 GSYM LEFT_FORALL_IMP_THM]); 1412 1413val rator_isub_commutes = store_thm( 1414 "rator_isub_commutes", 1415 ``!R t. is_comb t ==> (rator (t ISUB R) = rator t ISUB R)``, 1416 Induct THEN 1417 ASM_SIMP_TAC (srw_ss()) [ISUB_def, pairTheory.FORALL_PROD, 1418 rator_subst_commutes, is_comb_subst]); 1419 1420(* ---------------------------------------------------------------------- 1421 Congruence and rewrite rules for -b-> and -b->* 1422 ---------------------------------------------------------------------- *) 1423 1424open boolSimps 1425val RTC1_step = CONJUNCT2 (SPEC_ALL RTC_RULES) 1426 1427val betastar_LAM = store_thm( 1428 "betastar_LAM", 1429 ``!M N. LAM x M -b->* LAM x N <=> M -b->* N``, 1430 SIMP_TAC (srw_ss()) [EQ_IMP_THM, FORALL_AND_THM] THEN CONJ_TAC THENL [ 1431 Q_TAC SUFF_TAC `!M N. M -b->* N ==> 1432 !v M0 N0. (M = LAM v M0) /\ (N = LAM v N0) ==> 1433 M0 -b->* N0` THEN1 METIS_TAC [] THEN 1434 HO_MATCH_MP_TAC RTC_INDUCT THEN 1435 SIMP_TAC (srw_ss() ++ DNF_ss) [ccbeta_rwt] THEN 1436 METIS_TAC [RTC_RULES], 1437 1438 HO_MATCH_MP_TAC RTC_INDUCT THEN 1439 SRW_TAC [][] THEN 1440 METIS_TAC [compat_closure_rules, RTC_RULES] 1441 ]); 1442val _ = export_rewrites ["betastar_LAM"] 1443 1444val betastar_LAM_I = store_thm( 1445 "betastar_LAM_I", 1446 ``!v M N. M -b->* N ==> LAM v M -b->* LAM v N``, 1447 METIS_TAC [betastar_LAM]); 1448 1449val betastar_APPr = store_thm( 1450 "betastar_APPr", 1451 ``!M N. M -b->* N ==> P @@ M -b->* P @@ N``, 1452 HO_MATCH_MP_TAC RTC_INDUCT THEN SRW_TAC [][] THEN 1453 METIS_TAC [RTC1_step, compat_closure_rules]); 1454 1455val betastar_APPl = store_thm( 1456 "betastar_APPl", 1457 ``!M N. M -b->* N ==> M @@ P -b->* N @@ P``, 1458 HO_MATCH_MP_TAC RTC_INDUCT THEN SRW_TAC [][] THEN 1459 METIS_TAC [RTC1_step, compat_closure_rules]); 1460 1461val betastar_APPlr = store_thm( 1462 "betastar_APPlr", 1463 ``M -b->* M' ==> N -b->* N' ==> M @@ N -b->* M' @@ N'``, 1464 METIS_TAC [RTC_CASES_RTC_TWICE, betastar_APPl, betastar_APPr]); 1465 1466val beta_betastar = store_thm( 1467 "beta_betastar", 1468 ``LAM v M @@ N -b->* [N/v]M``, 1469 SRW_TAC [][ccbeta_rwt, RTC_SINGLE]); 1470 1471val betastar_eq_cong = store_thm( 1472 "betastar_eq_cong", 1473 ``bnf N ==> M -b->* M' ==> (M -b->* N <=> M' -b->* N)``, 1474 METIS_TAC [bnf_triangle, RTC_CASES_RTC_TWICE]); 1475 1476val _ = export_theory(); 1477 1478