1structure chap2Script = 2struct 3(* This structure bracketting is necessary for Moscow ML because of rebinding of 4 structure Q below 5*) 6 7open HolKernel Parse boolLib 8 9open bossLib binderLib 10 11open pred_setTheory pred_setLib 12open termTheory BasicProvers nomsetTheory 13 14val _ = augment_srw_ss [rewrites [LET_THM]] 15val std_ss = std_ss ++ rewrites [LET_THM] 16 17fun Store_thm(s, t, tac) = (store_thm(s,t,tac) before 18 export_rewrites [s]) 19 20structure Q = struct open Q open OldAbbrevTactics end; 21 22 23val _ = new_theory "chap2"; 24 25val (ctxt_rules, ctxt_indn, ctxt_cases) = (* p. 10 *) 26 Hol_reln`(!s. ctxt (\x. VAR s)) /\ 27 ctxt (\x. x) /\ 28 (!c1 c2. ctxt c1 /\ ctxt c2 ==> 29 ctxt (\x. c1 x @@ c2 x)) /\ 30 (!v c. ctxt c ==> ctxt (\x. LAM v (c x)))`; 31 32val constant_contexts_exist = store_thm( 33 "constant_contexts_exist", 34 ``!t. ctxt (\x. t)``, 35 HO_MATCH_MP_TAC simple_induction THEN REPEAT STRIP_TAC THEN 36 SRW_TAC [][ctxt_rules]); 37 38val (one_hole_context_rules, one_hole_context_ind, one_hole_context_cases) = 39 Hol_reln`one_hole_context (\x.x) /\ 40 (!x c. one_hole_context c ==> one_hole_context (\t. x @@ c t)) /\ 41 (!x c. one_hole_context c ==> one_hole_context (\t. c t @@ x)) /\ 42 (!v c. one_hole_context c ==> one_hole_context (\t. LAM v (c t)))`; 43 44val leftctxt = store_thm( 45 "leftctxt", 46 ``!z. one_hole_context (APP z)``, 47 Q_TAC SUFF_TAC `!z. one_hole_context (\t. z @@ (\x. x) t)` THEN1 48 SRW_TAC [boolSimps.ETA_ss][] THEN 49 SRW_TAC [][one_hole_context_rules]); 50 51val rightctxt_def = Define`rightctxt z = \t. t @@ z`; 52val rightctxt_thm = store_thm( 53 "rightctxt_thm", 54 ``!t z. rightctxt z t = t @@ z``, 55 SRW_TAC [][rightctxt_def]); 56 57val rightctxt = store_thm( 58 "rightctxt", 59 ``!z. one_hole_context (rightctxt z)``, 60 Q_TAC SUFF_TAC `!z. one_hole_context (\t. (\x. x) t @@ z)` THEN1 61 SRW_TAC [boolSimps.ETA_ss][rightctxt_def] THEN 62 SRW_TAC [][one_hole_context_rules]); 63 64val absctxt = store_thm( 65 "absctxt", 66 ``!v. one_hole_context (LAM v)``, 67 Q_TAC SUFF_TAC `!v. one_hole_context (\t. LAM v ((\x. x) t))` THEN1 68 SRW_TAC [boolSimps.ETA_ss][] THEN 69 SRW_TAC [][one_hole_context_rules]); 70 71val one_hole_is_normal = store_thm( 72 "one_hole_is_normal", 73 ``!c. one_hole_context c ==> ctxt c``, 74 MATCH_MP_TAC one_hole_context_ind THEN SRW_TAC [][ctxt_rules] THEN 75 `ctxt (\y. x)` by Q.SPEC_THEN `x` ACCEPT_TAC constant_contexts_exist THEN 76 `!c1 c2. ctxt c1 /\ ctxt c2 ==> ctxt (\t. c1 t @@ c2 t)` by 77 SRW_TAC [][ctxt_rules] THEN 78 POP_ASSUM 79 (fn imp => 80 POP_ASSUM (fn cth => 81 POP_ASSUM (fn th => 82 MP_TAC (MATCH_MP imp (CONJ th cth)) THEN 83 MP_TAC (MATCH_MP imp (CONJ cth th))))) THEN 84 SIMP_TAC std_ss []); 85 86val (lameq_rules, lameq_indn, lameq_cases) = (* p. 13 *) 87 IndDefLib.xHol_reln "lameq" 88 `(!x M N. (LAM x M) @@ N == [N/x]M) /\ 89 (!M. M == M) /\ 90 (!M N. M == N ==> N == M) /\ 91 (!M N L. M == N /\ N == L ==> M == L) /\ 92 (!M N Z. M == N ==> M @@ Z == N @@ Z) /\ 93 (!M N Z. M == N ==> Z @@ M == Z @@ N) /\ 94 (!M N x. M == N ==> LAM x M == LAM x N)`; 95 96val lameq_refl = Store_thm( 97 "lameq_refl", 98 ``M:term == M``, 99 SRW_TAC [][lameq_rules]); 100 101val lameq_app_cong = store_thm( 102 "lameq_app_cong", 103 ``M1 == M2 ==> N1 == N2 ==> M1 @@ N1 == M2 @@ N2``, 104 METIS_TAC [lameq_rules]); 105 106val lameq_weaken_cong = store_thm( 107 "lameq_weaken_cong", 108 ``(M1:term) == M2 ==> N1 == N2 ==> (M1 == N1 <=> M2 == N2)``, 109 METIS_TAC [lameq_rules]); 110 111Theorem lameq_SYM = List.nth(CONJUNCTS lameq_rules, 2) 112 113val fixed_point_thm = store_thm( (* p. 14 *) 114 "fixed_point_thm", 115 ``!f. ?x. f @@ x == x``, 116 GEN_TAC THEN Q_TAC (NEW_TAC "x") `FV f` THEN 117 Q.ABBREV_TAC `w = (LAM x (f @@ (VAR x @@ VAR x)))` THEN 118 Q.EXISTS_TAC `w @@ w` THEN 119 `w @@ w == [w/x] (f @@ (VAR x @@ VAR x))` by PROVE_TAC [lameq_rules] THEN 120 POP_ASSUM MP_TAC THEN 121 ASM_SIMP_TAC (srw_ss())[SUB_THM, lemma14b, lameq_rules]); 122 123(* properties of substitution - p19 *) 124 125val SUB_TWICE_ONE_VAR = store_thm( 126 "SUB_TWICE_ONE_VAR", 127 ``!body. [x/v] ([y/v] body) = [[x/v]y / v] body``, 128 HO_MATCH_MP_TAC nc_INDUCTION2 THEN SRW_TAC [][SUB_THM, SUB_VAR] THEN 129 Q.EXISTS_TAC `v INSERT FV x UNION FV y` THEN 130 SRW_TAC [][SUB_THM] THEN 131 Cases_on `v IN FV y` THEN SRW_TAC [][SUB_THM, lemma14c, lemma14b]); 132 133val lemma2_11 = store_thm( 134 "lemma2_11", 135 ``!t. ~(v = u) /\ ~(v IN FV M) ==> 136 ([M/u] ([N/v] t) = [[M/u]N/v] ([M/u] t))``, 137 HO_MATCH_MP_TAC nc_INDUCTION2 THEN 138 Q.EXISTS_TAC `{u;v} UNION FV M UNION FV N` THEN 139 SRW_TAC [][SUB_THM, SUB_VAR, lemma14b] THEN 140 Cases_on `u IN FV N` THEN SRW_TAC [][SUB_THM, lemma14b, lemma14c]); 141 142val substitution_lemma = save_thm("substitution_lemma", lemma2_11); 143 144val NOT_IN_FV_SUB = store_thm( 145 "NOT_IN_FV_SUB", 146 ``!x t u v. x NOTIN FV u /\ (x <> v ==> x NOTIN FV t) ==> 147 x NOTIN FV ([t/v]u)``, 148 SRW_TAC [][FV_SUB] THEN METIS_TAC []); 149 150val lemma2_12 = store_thm( (* p. 19 *) 151 "lemma2_12", 152 ``(M == M' ==> [N/x]M == [N/x]M') /\ 153 (N == N' ==> [N/x]M == [N'/x]M) /\ 154 (M == M' /\ N == N' ==> [N/x]M == [N'/x]M')``, 155 Q.SUBGOAL_THEN `(!M M'. M == M' ==> !N x. [N/x]M == [N/x]M') /\ 156 (!N N'. N == N' ==> !M x. [N/x]M == [N'/x]M)` 157 (fn th => STRIP_ASSUME_TAC th THEN SRW_TAC[][]) 158 THENL [ 159 CONJ_TAC THENL [ 160 REPEAT STRIP_TAC THEN 161 `LAM x M == LAM x M'` by PROVE_TAC [lameq_rules] THEN 162 `LAM x M @@ N == LAM x M' @@ N` by PROVE_TAC [lameq_rules] THEN 163 PROVE_TAC [lameq_rules], 164 Q_TAC SUFF_TAC `!N N' x M. N == N' ==> [N/x] M == [N'/x]M` THEN1 165 SRW_TAC [][] THEN 166 NTAC 3 GEN_TAC THEN HO_MATCH_MP_TAC nc_INDUCTION2 THEN 167 Q.EXISTS_TAC `x INSERT FV N UNION FV N'` THEN 168 SRW_TAC [][SUB_THM, SUB_VAR] THEN PROVE_TAC [lameq_rules] 169 ], 170 PROVE_TAC [lameq_rules] 171 ]); 172 173val lameq_sub_cong = save_thm( 174 "lameq_sub_cong", 175 REWRITE_RULE [GSYM AND_IMP_INTRO] (last (CONJUNCTS lemma2_12))); 176 177val lemma2_13 = store_thm( (* p.20 *) 178 "lemma2_13", 179 ``!c n n'. ctxt c ==> (n == n') ==> (c n == c n')``, 180 REPEAT GEN_TAC THEN STRIP_TAC THEN 181 MAP_EVERY Q.ID_SPEC_TAC [`n`, `n'`] THEN 182 POP_ASSUM MP_TAC THEN Q.ID_SPEC_TAC `c` THEN 183 HO_MATCH_MP_TAC ctxt_indn THEN PROVE_TAC [lameq_rules]); 184 185val (lamext_rules, lamext_indn, lamext_cases) = (* p. 21 *) 186 Hol_reln`(!x M N. lamext ((LAM x M) @@ N) ([N/x]M)) /\ 187 (!M. lamext M M) /\ 188 (!M N. lamext M N ==> lamext N M) /\ 189 (!M N L. lamext M N /\ lamext N L ==> lamext M L) /\ 190 (!M N Z. lamext M N ==> lamext (M @@ Z) (N @@ Z)) /\ 191 (!M N Z. lamext M N ==> lamext (Z @@ M) (Z @@ N)) /\ 192 (!M N x. lamext M N ==> lamext (LAM x M) (LAM x N)) /\ 193 (!M N x. ~(x IN FV (M @@ N)) /\ 194 lamext (M @@ VAR x) (N @@ VAR x) ==> 195 lamext M N)` 196 197val (lameta_rules, lameta_ind, lameta_cases) = (* p. 21 *) 198 Hol_reln`(!x M N. lameta ((LAM x M) @@ N) ([N/x]M)) /\ 199 (!M. lameta M M) /\ 200 (!M N. lameta M N ==> lameta N M) /\ 201 (!M N L. lameta M N /\ lameta N L ==> lameta M L) /\ 202 (!M N Z. lameta M N ==> lameta (M @@ Z) (N @@ Z)) /\ 203 (!M N Z. lameta M N ==> lameta (Z @@ M) (Z @@ N)) /\ 204 (!M N x. lameta M N ==> lameta (LAM x M) (LAM x N)) /\ 205 (!M x. ~(x IN FV M) ==> lameta (LAM x (M @@ VAR x)) M)`; 206 207val lemma2_14 = store_thm( 208 "lemma2_14", 209 ``!M N. lameta M N = lamext M N``, 210 REPEAT GEN_TAC THEN EQ_TAC THEN 211 MAP_EVERY Q.ID_SPEC_TAC [`N`, `M`] THENL [ 212 (* eta ==> ext *) 213 HO_MATCH_MP_TAC lameta_ind THEN REVERSE (REPEAT STRIP_TAC) THEN1 214 (MATCH_MP_TAC (last (CONJUNCTS lamext_rules)) THEN 215 Q.EXISTS_TAC `x` THEN 216 ASM_SIMP_TAC (srw_ss()) [] THEN 217 PROVE_TAC [lemma14a, lamext_rules]) THEN 218 PROVE_TAC [lamext_rules], 219 (* ext ==> eta *) 220 HO_MATCH_MP_TAC lamext_indn THEN REVERSE (REPEAT STRIP_TAC) THEN1 221 (`lameta (LAM x (M @@ VAR x)) (LAM x (N @@ VAR x))` by 222 PROVE_TAC [lameta_rules] THEN 223 FULL_SIMP_TAC (srw_ss()) [] THEN 224 PROVE_TAC [lameta_rules]) THEN 225 PROVE_TAC [lameta_rules] 226 ]); 227 228val consistent_def = 229 Define`consistent (thy:term -> term -> bool) = ?M N. ~thy M N`; 230 231val (asmlam_rules, asmlam_ind, asmlam_cases) = Hol_reln` 232 (!M N. (M,N) IN eqns ==> asmlam eqns M N) /\ 233 (!x M N. asmlam eqns (LAM x M @@ N) ([N/x]M)) /\ 234 (!M. asmlam eqns M M) /\ 235 (!M N. asmlam eqns M N ==> asmlam eqns N M) /\ 236 (!M N P. asmlam eqns M N /\ asmlam eqns N P ==> asmlam eqns M P) /\ 237 (!M M' N. asmlam eqns M M' ==> asmlam eqns (M @@ N) (M' @@ N)) /\ 238 (!M N N'. asmlam eqns N N' ==> asmlam eqns (M @@ N) (M @@ N')) /\ 239 (!x M M'. asmlam eqns M M' ==> asmlam eqns (LAM x M) (LAM x M')) 240`; 241 242val incompatible_def = 243 Define`incompatible x y = ~consistent (asmlam {(x,y)})` 244 245val S_def = 246 Define`S = LAM "x" (LAM "y" (LAM "z" 247 ((VAR "x" @@ VAR "z") @@ 248 (VAR "y" @@ VAR "z"))))`; 249val FV_S = Store_thm( 250 "FV_S", 251 ``FV S = {}``, 252 SRW_TAC [][S_def, EXTENSION] THEN METIS_TAC []); 253 254val K_def = Define`K = LAM "x" (LAM "y" (VAR "x"))`; 255val FV_K = Store_thm( 256 "FV_K", 257 ``FV K = {}``, 258 SRW_TAC [][K_def, EXTENSION]) 259 260val I_def = Define`I = LAM "x" (VAR "x")`; 261val FV_I = Store_thm("FV_I", ``FV I = {}``, SRW_TAC [][I_def]); 262 263val Omega_def = 264 Define`Omega = (LAM "x" (VAR "x" @@ VAR "x")) @@ 265 (LAM "x" (VAR "x" @@ VAR "x"))` 266val _ = Unicode.unicode_version {tmnm = "Omega", u = UnicodeChars.Omega} 267val FV_Omega = Store_thm( 268 "FV_Omega", 269 ``FV Omega = {}``, 270 SRW_TAC [][Omega_def, EXTENSION]); 271 272val SUB_LAM_RWT = store_thm( 273 "SUB_LAM_RWT", 274 ``!x y v body. [x/y] (LAM v body) = 275 let n = NEW (y INSERT FV x UNION FV body) 276 in 277 LAM n ([x/y]([VAR n/v] body))``, 278 SIMP_TAC std_ss [] THEN REPEAT GEN_TAC THEN 279 NEW_ELIM_TAC THEN Q.X_GEN_TAC `z` THEN STRIP_TAC THEN 280 `LAM v body = LAM z ([VAR z/v] body)` by SRW_TAC [][SIMPLE_ALPHA] THEN 281 SRW_TAC [][]); 282 283val lameq_asmlam = store_thm( 284 "lameq_asmlam", 285 ``!M N. M == N ==> asmlam eqns M N``, 286 HO_MATCH_MP_TAC lameq_indn THEN METIS_TAC [asmlam_rules]); 287 288fun betafy ss = 289 simpLib.add_relsimp {refl = GEN_ALL lameq_refl, 290 trans = List.nth(CONJUNCTS lameq_rules, 3), 291 weakenings = [lameq_weaken_cong], 292 subsets = [], 293 rewrs = [hd (CONJUNCTS lameq_rules)]} ss ++ 294 simpLib.SSFRAG {rewrs = [], 295 ac = [], convs = [], 296 congs = [lameq_app_cong, 297 SPEC_ALL (last (CONJUNCTS lameq_rules)), 298 lameq_sub_cong], 299 dprocs = [], filter = NONE, name = NONE} 300 301val lameq_S = store_thm( 302 "lameq_S", 303 ``S @@ A @@ B @@ C == (A @@ C) @@ (B @@ C)``, 304 SIMP_TAC (srw_ss()) [S_def] THEN FRESH_TAC THEN 305 ASM_SIMP_TAC (betafy (srw_ss())) [lemma14b]); 306 307val lameq_K = store_thm( 308 "lameq_K", 309 ``K @@ A @@ B == A``, 310 REWRITE_TAC [K_def] THEN FRESH_TAC THEN 311 ASM_SIMP_TAC (betafy (srw_ss())) [lemma14b]); 312 313val lameq_I = store_thm( 314 "lameq_I", 315 ``I @@ A == A``, 316 PROVE_TAC [lameq_rules, I_def, SUB_THM]); 317 318val B_def = Define`B = S @@ (K @@ S) @@ K`; 319val FV_B = Store_thm( 320 "FV_B", 321 ``FV B = {}``, 322 SRW_TAC [][B_def]); 323 324val lameq_B = store_thm( 325 "lameq_B", 326 ``B @@ f @@ g @@ x == f @@ (g @@ x)``, 327 SIMP_TAC (betafy (srw_ss())) [lameq_S, lameq_K, B_def]); 328 329val C_def = Define` 330 C = S @@ (B @@ B @@ S) @@ (K @@ K) 331`; 332val FV_C = Store_thm( 333 "FV_C", 334 ``FV C = {}``, 335 SRW_TAC [][C_def]); 336 337val lameq_C = store_thm( 338 "lameq_C", 339 ``C @@ f @@ x @@ y == f @@ y @@ x``, 340 SIMP_TAC (betafy (srw_ss())) [C_def, lameq_S, lameq_K, lameq_B]); 341 342val Y_def = Define` 343 Y = LAM "f" (LAM "x" (VAR "f" @@ (VAR "x" @@ VAR "x")) @@ 344 LAM "x" (VAR "f" @@ (VAR "x" @@ VAR "x"))) 345`; 346val FV_Y = Store_thm( 347 "FV_Y", 348 ``FV Y = {}``, 349 SRW_TAC [][Y_def, EXTENSION] THEN METIS_TAC []); 350 351val Yf_def = Define` 352 Yf f = let x = NEW (FV f) 353 in 354 LAM x (f @@ (VAR x @@ VAR x)) @@ 355 LAM x (f @@ (VAR x @@ VAR x)) 356`; 357 358val YYf = store_thm( 359 "YYf", 360 ``Y @@ f == Yf f``, 361 ONCE_REWRITE_TAC [lameq_cases] THEN DISJ1_TAC THEN 362 SRW_TAC [boolSimps.DNF_ss][Yf_def, Y_def, LAM_eq_thm] THEN 363 DISJ1_TAC THEN NEW_ELIM_TAC THEN SRW_TAC [][SUB_LAM_RWT] THEN 364 NEW_ELIM_TAC THEN SRW_TAC [][LAM_eq_thm, supp_fresh]); 365 366val YffYf = store_thm( 367 "YffYf", 368 ``Yf f == f @@ Yf f``, 369 SRW_TAC [][Yf_def] THEN NEW_ELIM_TAC THEN SRW_TAC [][Once lameq_cases] THEN 370 DISJ1_TAC THEN MAP_EVERY Q.EXISTS_TAC [`v`, `f @@ (VAR v @@ VAR v)`] THEN 371 SRW_TAC [][lemma14b]); 372 373val lameq_Y = store_thm( 374 "lameq_Y", 375 ``Y @@ f == f @@ (Y @@ f)``, 376 METIS_TAC [lameq_rules, YYf, YffYf]); 377 378val Yf_fresh = store_thm( 379 "Yf_fresh", 380 ``v ��� FV f ��� 381 (Yf f = LAM v (f @@ (VAR v @@ VAR v)) @@ LAM v (f @@ (VAR v @@ VAR v)))``, 382 SRW_TAC [][Yf_def, LET_THM] THEN 383 binderLib.NEW_ELIM_TAC THEN SRW_TAC [][LAM_eq_thm, supp_fresh]); 384 385val Yf_SUB = Store_thm( 386 "Yf_SUB", 387 ``[N/x] (Yf f) = Yf ([N/x] f)``, 388 Q_TAC (NEW_TAC "v") `FV f ��� FV N ��� {x}` THEN 389 `Yf f = LAM v (f @@ (VAR v @@ VAR v)) @@ LAM v (f @@ (VAR v @@ VAR v))` 390 by SRW_TAC [][Yf_fresh] THEN 391 `Yf ([N/x]f) = 392 LAM v ([N/x]f @@ (VAR v @@ VAR v)) @@ LAM v ([N/x]f @@ (VAR v @@ VAR v))` 393 by SRW_TAC [][Yf_fresh, NOT_IN_FV_SUB] THEN 394 SRW_TAC [][]); 395 396val Yf_11 = Store_thm( 397 "Yf_11", 398 ``(Yf f = Yf g) = (f = g)``, 399 SRW_TAC [][Yf_def, LET_THM] THEN 400 NTAC 2 (binderLib.NEW_ELIM_TAC THEN REPEAT STRIP_TAC) THEN 401 SRW_TAC [][LAM_eq_thm, EQ_IMP_THM] THEN 402 SRW_TAC [][supp_fresh]); 403 404val FV_Yf = Store_thm( 405 "FV_Yf", 406 ``FV (Yf t) = FV t``, 407 SRW_TAC [boolSimps.CONJ_ss][Yf_def, EXTENSION, LET_THM] THEN 408 NEW_ELIM_TAC THEN METIS_TAC []); 409 410val Yf_cong = store_thm( 411 "Yf_cong", 412 ``f == g ��� Yf f == Yf g``, 413 Q_TAC (NEW_TAC "fv") `FV f ��� FV g` THEN 414 `(Yf f = LAM fv (f @@ (VAR fv @@ VAR fv)) @@ 415 LAM fv (f @@ (VAR fv @@ VAR fv))) ��� 416 (Yf g = LAM fv (g @@ (VAR fv @@ VAR fv)) @@ 417 LAM fv (g @@ (VAR fv @@ VAR fv)))` 418 by SRW_TAC [][Yf_fresh] THEN 419 STRIP_TAC THEN ASM_SIMP_TAC (srw_ss()) [] THEN 420 METIS_TAC [lameq_rules]); 421 422val SK_incompatible = store_thm( (* example 2.18, p23 *) 423 "SK_incompatible", 424 ``incompatible S K``, 425 Q_TAC SUFF_TAC `!M N. asmlam {(S,K)} M N` 426 THEN1 SRW_TAC [][incompatible_def, consistent_def] THEN 427 REPEAT GEN_TAC THEN 428 `asmlam {(S,K)} S K` by PROVE_TAC [asmlam_rules, IN_INSERT] THEN 429 `!D. asmlam {(S,K)} (S @@ I @@ (K @@ D) @@ I) (K @@ I @@ (K @@ D) @@ I)` 430 by PROVE_TAC [asmlam_rules] THEN 431 `!D. asmlam {(S,K)} (S @@ I @@ (K @@ D) @@ I) I` 432 by PROVE_TAC [lameq_K, asmlam_rules, lameq_asmlam, lameq_I] THEN 433 `!D. asmlam {(S,K)} ((I @@ I) @@ (K @@ D @@ I)) I` 434 by PROVE_TAC [lameq_S, asmlam_rules, lameq_asmlam] THEN 435 `!D. asmlam {(S,K)} D I` 436 by PROVE_TAC [lameq_I, lameq_K, asmlam_rules, lameq_asmlam] THEN 437 PROVE_TAC [asmlam_rules]); 438 439val [asmlam_eqn, asmlam_beta, asmlam_refl, asmlam_sym, asmlam_trans, 440 asmlam_lcong, asmlam_rcong, asmlam_abscong] = 441 CONJUNCTS (SPEC_ALL asmlam_rules) 442 443val xx_xy_incompatible = store_thm( (* example 2.20, p24 *) 444 "xx_xy_incompatible", 445 ``~(x = y) ==> incompatible (VAR x @@ VAR x) (VAR x @@ VAR y)``, 446 STRIP_TAC THEN 447 Q_TAC SUFF_TAC 448 `!M N. 449 asmlam {(VAR x @@ VAR x, VAR x @@ VAR y)} M N` 450 THEN1 SIMP_TAC std_ss [incompatible_def, consistent_def] THEN 451 REPEAT GEN_TAC THEN 452 Q.ABBREV_TAC `xx_xy = asmlam {(VAR x @@ VAR x, VAR x @@ VAR y)}` THEN 453 `xx_xy (VAR x @@ VAR x) (VAR x @@ VAR y)` 454 by PROVE_TAC [asmlam_rules, IN_INSERT] THEN 455 `xx_xy (LAM x (LAM y (VAR x @@ VAR x))) (LAM x (LAM y (VAR x @@ VAR y)))` 456 by PROVE_TAC [asmlam_rules] THEN 457 `xx_xy ((LAM x (LAM y (VAR x @@ VAR x))) @@ I) 458 ((LAM x (LAM y (VAR x @@ VAR y))) @@ I)` 459 by PROVE_TAC [asmlam_rules] THEN 460 `xx_xy (LAM y (I @@ I)) ((LAM x (LAM y (VAR x @@ VAR x))) @@ I)` 461 by (Q_TAC SUFF_TAC `[I/x] (LAM y (VAR x @@ VAR x)) = LAM y (I @@ I)` THEN1 462 PROVE_TAC [asmlam_rules] THEN 463 ASM_SIMP_TAC std_ss [SUB_THM, FV_I, NOT_IN_EMPTY]) THEN 464 `xx_xy (LAM y (I @@ I)) (LAM y I)` 465 by PROVE_TAC [asmlam_rules, lameq_I, lameq_asmlam] THEN 466 `xx_xy (LAM y I) ((LAM x (LAM y (VAR x @@ VAR y))) @@ I)` 467 by METIS_TAC [asmlam_trans, asmlam_sym] THEN 468 `[I/x](LAM y (VAR x @@ VAR y)) = LAM y (I @@ VAR y)` by 469 ASM_SIMP_TAC (srw_ss()) [SUB_THM, FV_I] THEN 470 `xx_xy (LAM x (LAM y (VAR x @@ VAR y)) @@ I) (LAM y (I @@ VAR y))` 471 by PROVE_TAC [asmlam_beta] THEN 472 `xx_xy (LAM y (I @@ VAR y)) (LAM y I)` 473 by METIS_TAC [asmlam_trans, asmlam_sym] THEN 474 `xx_xy (LAM y (VAR y)) (LAM y I)` 475 by (Q.UNABBREV_TAC `xx_xy` THEN MATCH_MP_TAC asmlam_trans THEN 476 Q.EXISTS_TAC `LAM y (I @@ VAR y)` THEN 477 METIS_TAC [asmlam_abscong, lameq_I, asmlam_sym, lameq_asmlam]) THEN 478 `!D. xx_xy ((LAM y (VAR y)) @@ D) ((LAM y I) @@ D)` 479 by PROVE_TAC [asmlam_lcong] THEN 480 `!D. [D/y](VAR y) = D` by SRW_TAC [][SUB_THM] THEN 481 `!D. xx_xy D ((LAM y I) @@ D)` 482 by METIS_TAC [asmlam_beta, asmlam_trans, asmlam_sym] THEN 483 `!D. [D/y]I = I` by SRW_TAC [][lemma14b, FV_I] THEN 484 `!D. xx_xy D I` 485 by PROVE_TAC [asmlam_beta, asmlam_trans, asmlam_sym] THEN 486 METIS_TAC [asmlam_trans, asmlam_sym]); 487 488val (is_abs_thm, _) = define_recursive_term_function 489 `(is_abs (VAR s) = F) /\ 490 (is_abs (t1 @@ t2) = F) /\ 491 (is_abs (LAM v t) = T)`; 492val _ = export_rewrites ["is_abs_thm"] 493 494val is_abs_vsubst_invariant = Store_thm( 495 "is_abs_vsubst_invariant", 496 ``!t. is_abs ([VAR v/u] t) = is_abs t``, 497 HO_MATCH_MP_TAC nc_INDUCTION2 THEN Q.EXISTS_TAC `{u;v}` THEN 498 SRW_TAC [][SUB_THM, SUB_VAR]); 499 500val (is_comb_thm, _) = define_recursive_term_function 501 `(is_comb (VAR s) = F) /\ 502 (is_comb (t1 @@ t2) = T) /\ 503 (is_comb (LAM v t) = F)`; 504val _ = export_rewrites ["is_comb_thm"] 505 506val is_comb_vsubst_invariant = Store_thm( 507 "is_comb_vsubst_invariant", 508 ``!t. is_comb ([VAR v/u] t) = is_comb t``, 509 HO_MATCH_MP_TAC nc_INDUCTION2 THEN Q.EXISTS_TAC `{u;v}` THEN 510 SRW_TAC [][SUB_THM, SUB_VAR]); 511 512val (is_var_thm, _) = define_recursive_term_function 513 `(is_var (VAR s) = T) /\ 514 (is_var (t1 @@ t2) = F) /\ 515 (is_var (LAM v t) = F)`; 516val _ = export_rewrites ["is_var_thm"] 517 518val is_var_vsubst_invariant = Store_thm( 519 "is_var_vsubst_invariant", 520 ``!t. is_var ([VAR v/u] t) = is_var t``, 521 HO_MATCH_MP_TAC nc_INDUCTION2 THEN Q.EXISTS_TAC `{u;v}` THEN 522 SRW_TAC [][SUB_THM, SUB_VAR]); 523 524val (bnf_thm, _) = define_recursive_term_function 525 `(bnf (VAR s) <=> T) /\ 526 (bnf (t1 @@ t2) <=> bnf t1 /\ bnf t2 /\ ~is_abs t1) /\ 527 (bnf (LAM v t) <=> bnf t)`; 528val _ = export_rewrites ["bnf_thm"] 529 530val bnf_Omega = Store_thm( 531 "bnf_Omega", 532 ``~bnf Omega``, 533 SRW_TAC [][Omega_def]); 534val I_beta_normal = Store_thm( 535 "I_beta_normal", 536 ``bnf I``, 537 SRW_TAC [][I_def]); 538val K_beta_normal = Store_thm("K_beta_normal", ``bnf K``, SRW_TAC [][K_def]); 539val S_beta_normal = Store_thm("S_beta_normal", ``bnf S``, SRW_TAC [][S_def]); 540(* because I have defined them in terms of applications of S and K, C and B 541 are not in bnf *) 542 543val Yf_bnf = Store_thm( 544 "Yf_bnf", 545 ``��bnf (Yf f)``, 546 SRW_TAC [][Yf_def] THEN SRW_TAC [][]); 547 548val bnf_vsubst_invariant = Store_thm( 549 "bnf_vsubst_invariant", 550 ``!t. bnf ([VAR v/u] t) = bnf t``, 551 HO_MATCH_MP_TAC nc_INDUCTION2 THEN Q.EXISTS_TAC `{u;v}` THEN 552 SRW_TAC [][SUB_THM, SUB_VAR]); 553 554val _ = augment_srw_ss [rewrites [LAM_eq_thm]] 555val (rand_thm, _) = define_recursive_term_function `rand (t1 @@ t2) = t2`; 556val _ = export_rewrites ["rand_thm"] 557 558val (rator_thm, _) = define_recursive_term_function `rator (t1 @@ t2) = t1`; 559val _ = export_rewrites ["rator_thm"] 560 561val is_comb_APP_EXISTS = store_thm( 562 "is_comb_APP_EXISTS", 563 ``!t. is_comb t = (?u v. t = u @@ v)``, 564 PROVE_TAC [term_CASES, is_comb_thm]); 565 566val is_comb_rator_rand = store_thm( 567 "is_comb_rator_rand", 568 ``!t. is_comb t ==> (rator t @@ rand t = t)``, 569 SIMP_TAC (srw_ss()) [is_comb_APP_EXISTS, GSYM LEFT_FORALL_IMP_THM, 570 rator_thm, rand_thm]); 571 572val rand_subst_commutes = store_thm( 573 "rand_subst_commutes", 574 ``!t u v. is_comb t ==> ([u/v] (rand t) = rand ([u/v] t))``, 575 REPEAT STRIP_TAC THEN 576 FULL_SIMP_TAC (srw_ss()) [is_comb_APP_EXISTS, SUB_THM, rand_thm]); 577 578val rator_subst_commutes = store_thm( 579 "rator_subst_commutes", 580 ``!t u x. is_comb t ==> ([u/v] (rator t) = rator ([u/v] t))``, 581 SRW_TAC [][is_comb_APP_EXISTS, rator_thm, SUB_THM] THEN 582 SRW_TAC [][is_comb_APP_EXISTS, rator_thm, SUB_THM]); 583 584 585val extra_LAM_DISJOINT = store_thm( 586 "extra_LAM_DISJOINT", 587 ``(!t v u b t1 t2. ~(t1 @@ t2 = [t/v] (LAM u b))) /\ 588 (!R u b t1 t2. ~(t1 @@ t2 = (LAM u b) ISUB R)) /\ 589 (!t v u b s. ~(VAR s = [t/v] (LAM u b))) /\ 590 (!R u b s. ~(VAR s = (LAM u b) ISUB R))``, 591 REPEAT (GEN_TAC ORELSE CONJ_TAC) THENL [ 592 Q_TAC (NEW_TAC "z") `{u;v} UNION FV t UNION FV b`, 593 Q_TAC (NEW_TAC "z") `{u} UNION DOM R UNION FV b UNION FVS R`, 594 Q_TAC (NEW_TAC "z") `{s;u;v} UNION FV b UNION FV t`, 595 Q_TAC (NEW_TAC "z") `{s;u} UNION DOM R UNION FV b UNION FVS R` 596 ] THEN 597 `LAM u b = LAM z ([VAR z/u] b)` by SRW_TAC [][SIMPLE_ALPHA] THEN 598 SRW_TAC [][SUB_THM, ISUB_LAM]); 599val _ = export_rewrites ["extra_LAM_DISJOINT"] 600 601val tpm_eq_var = prove( 602 ``(tpm pi t = VAR s) <=> (t = VAR (lswapstr pi����� s))``, 603 SRW_TAC [][pmact_eql]); 604val _ = augment_srw_ss [rewrites [tpm_eq_var]] 605 606val (enf_thm, _) = define_recursive_term_function 607 `(enf (VAR s) <=> T) /\ 608 (enf (t @@ u) <=> enf t /\ enf u) /\ 609 (enf (LAM v t) <=> enf t /\ (is_comb t /\ rand t = VAR v ==> 610 v IN FV (rator t)))` 611val _ = export_rewrites ["enf_thm"] 612 613val subst_eq_var = store_thm( 614 "subst_eq_var", 615 ``[v/u] t = VAR s <=> t = VAR u ��� v = VAR s ��� t = VAR s ��� u ��� s``, 616 Q.SPEC_THEN `t` STRUCT_CASES_TAC term_CASES THEN 617 SRW_TAC [][SUB_VAR, SUB_THM] THEN PROVE_TAC []); 618 619val enf_vsubst_invariant = Store_thm( 620 "enf_vsubst_invariant", 621 ``!t. enf ([VAR v/u] t) = enf t``, 622 HO_MATCH_MP_TAC nc_INDUCTION2 THEN 623 Q.EXISTS_TAC `{u;v}` THEN 624 SRW_TAC [][SUB_THM, SUB_VAR, enf_thm] THEN 625 SRW_TAC [boolSimps.CONJ_ss][GSYM rand_subst_commutes, subst_eq_var] THEN 626 SRW_TAC [][GSYM rator_subst_commutes, FV_SUB]); 627 628val benf_def = Define`benf t <=> bnf t /\ enf t`; 629 630 631val has_bnf_def = Define`has_bnf t = ?t'. t == t' /\ bnf t'`; 632 633val has_benf_def = Define`has_benf t = ?t'. t == t' /\ benf t'`; 634 635val _ = remove_ovl_mapping "Y" {Thy = "chap2", Name = "Y"} 636 637val _ = export_theory() 638end; (* struct *) 639