1open HolKernel boolLib Parse bossLib BasicProvers 2 3open pred_setTheory 4 5open binderLib 6 7open nomsetTheory labelledTermsTheory termTheory chap3Theory 8 9val _ = new_theory "chap11_1"; 10 11fun Store_Thm(n,t,tac) = store_thm(n,t,tac) before export_rewrites [n] 12 13(* ---------------------------------------------------------------------- 14 phi function for reducing all labelled redexes 15 ---------------------------------------------------------------------- *) 16 17val (phi_thm, _) = 18 define_recursive_term_function' 19 (SIMP_CONV (srw_ss()) [tpm_subst, fresh_tpm_subst, GSYM SIMPLE_ALPHA, 20 lemma15a]) 21 `(phi (VAR s) = VAR s : term) /\ 22 (phi (M @@ N) = phi M @@ phi N) /\ 23 (phi (LAM v M) = LAM v (phi M)) /\ 24 (phi (LAMi n v M N) = [phi N/v] (phi M))` 25val _ = export_rewrites ["phi_thm"] 26 27val FV_phi = store_thm( 28 "FV_phi", 29 ``!M. v IN FV (phi M) ==> v IN FV M``, 30 HO_MATCH_MP_TAC lterm_bvc_induction THEN 31 Q.EXISTS_TAC `{v}` THEN SRW_TAC [][] THENL [ 32 METIS_TAC [], 33 METIS_TAC [], 34 FULL_SIMP_TAC (srw_ss()) [FV_SUB] THEN METIS_TAC [IN_UNION, IN_DELETE] 35 ]); 36 37val NOT_IN_lSUB_I = Store_Thm( 38 "NOT_IN_lSUB_I", 39 ``���M:lterm. v ��� FV N ��� v ��� u ��� v ��� FV M ==> v ��� FV ([N/u]M)``, 40 HO_MATCH_MP_TAC lterm_bvc_induction THEN Q.EXISTS_TAC `FV N ��� {u;v}` THEN 41 SRW_TAC [][lSUB_VAR]); 42 43val phi_vsubst_commutes = store_thm( 44 "phi_vsubst_commutes", 45 ``!M. phi ([VAR v/u] M) = [VAR v/u] (phi M)``, 46 HO_MATCH_MP_TAC lterm_bvc_induction THEN Q.EXISTS_TAC `{u;v}` THEN 47 SRW_TAC [][SUB_THM, SUB_VAR] THEN 48 SRW_TAC [][chap2Theory.substitution_lemma]); 49 50 51(* ---------------------------------------------------------------------- 52 strip_label : removing all labels and dropping into :term 53 ---------------------------------------------------------------------- *) 54 55val _ = augment_srw_ss [ 56 simpLib.name_ss "alphas" (rewrites [GSYM tpm_ALPHA, GSYM ltpm_ALPHA]) 57] 58 59val (strip_label_thm,_) = define_recursive_term_function 60 `(strip_label (VAR s) = VAR s : term) /\ 61 (strip_label (M @@ N) = strip_label M @@ strip_label N) /\ 62 (strip_label (LAM v M) = LAM v (strip_label M)) /\ 63 (strip_label (LAMi n v M N) = (LAM v (strip_label M) @@ strip_label N))` 64val _ = export_rewrites ["strip_label_thm"] 65 66val FV_strip_label = Store_Thm( 67 "FV_strip_label", 68 ``!M. FV (strip_label M) = FV M``, 69 HO_MATCH_MP_TAC simple_lterm_induction THEN SRW_TAC [][]); 70 71val strip_label_vsubst_commutes = store_thm( 72 "strip_label_vsubst_commutes", 73 ``!M. [VAR u/v] (strip_label M) = strip_label ([VAR u/v] M)``, 74 HO_MATCH_MP_TAC lterm_bvc_induction THEN 75 Q.EXISTS_TAC `{u;v}` THEN SRW_TAC [][SUB_THM, SUB_VAR]); 76 77val strip_label_eq_lam = store_thm( 78 "strip_label_eq_lam", 79 ``(strip_label M = LAM v t) = 80 ?t'. (M = LAM v t') /\ (strip_label t' = t)``, 81 Q.SPEC_THEN `M` STRUCT_CASES_TAC lterm_CASES THEN 82 SRW_TAC [][LAM_eq_thm, lLAM_eq_thm, EQ_IMP_THM, 83 tpm_eqr, ltpm_eqr] THEN 84 FULL_SIMP_TAC (srw_ss()) [tpm_eqr, ltpm_eqr]); 85 86val strip_label_eq_redex = store_thm( 87 "strip_label_eq_redex", 88 ``(strip_label M = LAM v t @@ u) <=> 89 (?t' u'. (M = LAM v t' @@ u') /\ (strip_label t' = t) /\ 90 (strip_label u' = u)) \/ 91 (?n t' u'. (M = LAMi n v t' u') /\ 92 (strip_label t' = t) /\ 93 (strip_label u' = u))``, 94 Q.SPEC_THEN `M` STRUCT_CASES_TAC lterm_CASES THEN 95 SRW_TAC [][strip_label_eq_lam] THENL [ 96 METIS_TAC [], 97 SRW_TAC [][lLAMi_eq_thm, EQ_IMP_THM, LAM_eq_thm] THENL [ 98 FULL_SIMP_TAC (srw_ss()) [ltpm_eqr, tpm_eqr] THEN 99 SRW_TAC [][] THEN FULL_SIMP_TAC (srw_ss()) [], 100 SRW_TAC [][tpm_eqr] 101 ] 102 ]); 103 104val strip_label_subst = store_thm( 105 "strip_label_subst", 106 ``!M. strip_label ([N/v] M) = [strip_label N/v] (strip_label M)``, 107 HO_MATCH_MP_TAC lterm_bvc_induction THEN Q.EXISTS_TAC `v INSERT FV N` THEN 108 SRW_TAC [][SUB_THM, SUB_VAR]); 109 110(* ---------------------------------------------------------------------- 111 null_labelling, from :term to :lterm 112 ---------------------------------------------------------------------- *) 113 114val (null_labelling_thm,_) = define_recursive_term_function` 115 (null_labelling (VAR s : term) = VAR s : lterm) /\ 116 (null_labelling (M @@ N) = null_labelling M @@ null_labelling N) /\ 117 (null_labelling (LAM v M) = LAM v (null_labelling M))` 118val _ = export_rewrites ["null_labelling_thm"] 119 120val _ = diminish_srw_ss ["alphas"] 121 122val FV_null_labelling = Store_Thm( 123 "FV_null_labelling", 124 ``!M. FV (null_labelling M) = FV M``, 125 HO_MATCH_MP_TAC simple_induction THEN SRW_TAC [][]); 126 127val null_labelling_subst = store_thm( 128 "null_labelling_subst", 129 ``!M. null_labelling ([N/v] M) = [null_labelling N/v] (null_labelling M)``, 130 HO_MATCH_MP_TAC nc_INDUCTION2 THEN Q.EXISTS_TAC `v INSERT FV N` THEN 131 SRW_TAC [][SUB_THM, SUB_VAR]); 132 133val strip_null_labelling = Store_Thm( 134 "strip_null_labelling", 135 ``!M. strip_label (null_labelling M) = M``, 136 HO_MATCH_MP_TAC simple_induction THEN SRW_TAC [][]); 137 138val phi_null_labelling = Store_Thm( 139 "phi_null_labelling", 140 ``!M. phi (null_labelling M) = M``, 141 HO_MATCH_MP_TAC simple_induction THEN SRW_TAC [][]); 142 143(* ---------------------------------------------------------------------- 144 substitution lemma 145 ---------------------------------------------------------------------- *) 146 147val christians_lemma = prove( 148 ``!L: lterm. ~(x IN FV L) /\ ~(x IN FV N) ==> ~(x IN FV ([N/v] L))``, 149 HO_MATCH_MP_TAC lterm_bvc_induction THEN 150 Q.EXISTS_TAC `{x;v} UNION FV N` THEN 151 SRW_TAC [][lSUB_VAR]); 152 153 154val lSUBSTITUTION_LEMMA = store_thm( 155 "lSUBSTITUTION_LEMMA", 156 ``!M:lterm. ~(v = x) /\ ~(v IN FV L) ==> 157 ([L/x] ([N/v] M) = [[L/x] N/v] ([L/x] M))``, 158 HO_MATCH_MP_TAC lterm_bvc_induction THEN 159 Q.EXISTS_TAC `{v;x} UNION FV L UNION FV N` THEN 160 SRW_TAC [][lSUB_VAR, l14b, FV_SUB, christians_lemma]); 161 162val ltpm_subst = store_thm( 163 "ltpm_subst", 164 ``!M. ltpm p ([N/v]M) = [ltpm p N/lswapstr p v] (ltpm p M)``, 165 HO_MATCH_MP_TAC lterm_bvc_induction THEN Q.EXISTS_TAC `v INSERT FV N` THEN 166 SRW_TAC [][lSUB_VAR]); 167 168val l14c = store_thm( 169 "l14c", 170 ``!M:lterm. x IN FV M ==> (FV ([N/x]M) = FV N UNION (FV M DELETE x))``, 171 HO_MATCH_MP_TAC lterm_bvc_induction THEN Q.EXISTS_TAC `x INSERT FV N` THEN 172 SRW_TAC [][] THEN FULL_SIMP_TAC (srw_ss()) [] THENL [ 173 Cases_on `x IN FV M'` THEN SRW_TAC [][l14b, EXTENSION, EQ_IMP_THM] THEN 174 SRW_TAC [][] THEN METIS_TAC [], 175 Cases_on `x IN FV M` THEN SRW_TAC [][l14b, EXTENSION, EQ_IMP_THM] THEN 176 SRW_TAC [][] THEN METIS_TAC [], 177 SRW_TAC [][EXTENSION, EQ_IMP_THM] THEN SRW_TAC [][] THEN METIS_TAC [], 178 Cases_on `x IN FV M'` THEN SRW_TAC [][l14b, EXTENSION, EQ_IMP_THM] THEN 179 SRW_TAC [][] THEN METIS_TAC [], 180 Cases_on `x IN FV M` THEN SRW_TAC [][l14b, EXTENSION, EQ_IMP_THM] THEN 181 SRW_TAC [][] THEN METIS_TAC [] 182 ]); 183 184val lFV_SUB = store_thm( 185 "lFV_SUB", 186 ``FV ([N/v]M:lterm) = if v IN FV M then FV N UNION (FV M DELETE v) 187 else FV M``, 188 METIS_TAC [l14c, l14b]); 189 190 191(* ---------------------------------------------------------------------- 192 compatible closure for labelled terms 193 ---------------------------------------------------------------------- *) 194 195val (lcompat_closure_rules, lcompat_closure_ind, lcompat_closure_cases) = 196 Hol_reln`(!x y. R x y ==> lcompat_closure R x y) /\ 197 (!z x y. lcompat_closure R x y ==> 198 lcompat_closure R (z @@ x) (z @@ y)) /\ 199 (!z x y. lcompat_closure R x y ==> 200 lcompat_closure R (x @@ z) (y @@ z)) /\ 201 (!v x y. lcompat_closure R x y ==> 202 lcompat_closure R (LAM v x) (LAM v y)) /\ 203 (!v n z x y. 204 lcompat_closure R x y ==> 205 lcompat_closure R (LAMi n v x z) (LAMi n v y z)) /\ 206 (!v n z x y. 207 lcompat_closure R x y ==> 208 lcompat_closure R (LAMi n v z x) (LAMi n v z y))`; 209 210(* reduction on lterms *) 211val beta0_def = 212 Define`beta0 M N = ?n v t u. (M = LAMi n v t u) /\ (N = [u/v]t)`; 213 214val beta1_def = 215 Define`beta1 (M: lterm) N = 216 ?v t u. (M = (LAM v t) @@ u) /\ (N = [u/v]t)`; 217 218val lcc_beta_bvc_ind = store_thm( 219 "lcc_beta_bvc_ind", 220 ``!P X. FINITE X /\ 221 (!v M N. ~(v IN FV N) /\ ~(v IN X) ==> 222 P (LAM v M @@ N) ([N/v]M)) /\ 223 (!n v M N. ~(v IN FV N) /\ ~(v IN X) ==> 224 P (LAMi n v M N) ([N/v]M)) /\ 225 (!M M' N. P M M' ==> P (M @@ N) (M' @@ N)) /\ 226 (!M N N'. P N N' ==> P (M @@ N) (M @@ N')) /\ 227 (!v M M'. ~(v IN X) /\ P M M' ==> P (LAM v M) (LAM v M')) /\ 228 (!n v M M' N. ~(v IN X) /\ ~(v IN FV N) /\ P M M' ==> 229 P (LAMi n v M N) (LAMi n v M' N)) /\ 230 (!n v M N N'. 231 ~(v IN X) /\ ~(v IN FV N) /\ ~(v IN FV N') /\ P N N' ==> 232 P (LAMi n v M N) (LAMi n v M N')) 233 ==> 234 !M N. lcompat_closure (beta0 RUNION beta1) M N ==> P M N``, 235 REPEAT GEN_TAC THEN STRIP_TAC THEN 236 Q_TAC SUFF_TAC `!M N. lcompat_closure(beta0 RUNION beta1) M N ==> 237 !p. P (ltpm p M) (ltpm p N)` 238 THEN1 METIS_TAC [pmact_nil] THEN 239 HO_MATCH_MP_TAC lcompat_closure_ind THEN 240 SRW_TAC [][relationTheory.RUNION, beta0_def, beta1_def] THENL [ 241 (* beta0 reduction *) 242 SRW_TAC [][ltpm_subst] THEN 243 Q_TAC (NEW_TAC "z") `X UNION FV (ltpm p t) UNION FV (ltpm p u)` THEN 244 `LAMi n (lswapstr p v) (ltpm p t) (ltpm p u) = 245 LAMi n z (ltpm [(z,lswapstr p v)] (ltpm p t)) (ltpm p u)` 246 by SRW_TAC [][ltpm_ALPHAi] THEN 247 `[ltpm p u/lswapstr p v] (ltpm p t) = 248 [ltpm p u/z] (ltpm [(z,lswapstr p v)] (ltpm p t))` 249 by SRW_TAC [][fresh_ltpm_subst, l15a] THEN 250 SRW_TAC [][], 251 (* beta1 reduction *) 252 SRW_TAC [][ltpm_subst] THEN 253 Q_TAC (NEW_TAC "z") `X UNION FV (ltpm p t) UNION FV (ltpm p u)` THEN 254 `LAM (lswapstr p v) (ltpm p t) = 255 LAM z (ltpm [(z,lswapstr p v)] (ltpm p t))` 256 by SRW_TAC [][ltpm_ALPHA] THEN 257 `[ltpm p u/lswapstr p v] (ltpm p t) = 258 [ltpm p u/z] (ltpm [(z,lswapstr p v)] (ltpm p t))` 259 by SRW_TAC [][fresh_ltpm_subst, l15a] THEN 260 SRW_TAC [][], 261 262 Q_TAC (NEW_TAC "z") `X UNION FV (ltpm p M) UNION FV (ltpm p N)` THEN 263 Q_TAC SUFF_TAC `(LAM (lswapstr p v) (ltpm p M) = 264 LAM z (ltpm [(z,lswapstr p v)] (ltpm p M))) /\ 265 (LAM (lswapstr p v) (ltpm p N) = 266 LAM z (ltpm [(z,lswapstr p v)] (ltpm p N)))` 267 THEN1 SRW_TAC [][GSYM pmact_decompose] THEN 268 SRW_TAC [][ltpm_ALPHA], 269 270 Q_TAC (NEW_TAC "w") 271 `X UNION FV (ltpm p M) UNION FV (ltpm p N) UNION FV (ltpm p z)` THEN 272 `(LAMi n (lswapstr p v) (ltpm p M) (ltpm p z) = 273 LAMi n w (ltpm [(w,lswapstr p v)] (ltpm p M)) (ltpm p z)) /\ 274 (LAMi n (lswapstr p v) (ltpm p N) (ltpm p z) = 275 LAMi n w (ltpm [(w,lswapstr p v)] (ltpm p N)) (ltpm p z))` 276 by SRW_TAC [][ltpm_ALPHAi] THEN 277 SRW_TAC [][GSYM pmact_decompose], 278 279 Q_TAC (NEW_TAC "w") 280 `X UNION FV (ltpm p z) UNION FV (ltpm p M) UNION FV (ltpm p N)` THEN 281 `!N. LAMi n (lswapstr p v) (ltpm p z) N = 282 LAMi n w (ltpm [(w,lswapstr p v)] (ltpm p z)) N` 283 by SRW_TAC [][ltpm_ALPHAi] THEN 284 SRW_TAC [][GSYM pmact_decompose] 285 ]); 286 287open boolSimps 288val beta_matched = store_thm( 289 "beta_matched", 290 ``!M' N. beta (strip_label M') N ==> 291 ?N'. (beta0 RUNION beta1) M' N' /\ (N = strip_label N')``, 292 SIMP_TAC (srw_ss()) [beta_def] THEN 293 REPEAT GEN_TAC THEN 294 Q.SPEC_THEN `M'` STRUCT_CASES_TAC lterm_CASES THEN 295 SRW_TAC [][] THENL [ 296 FULL_SIMP_TAC (srw_ss()) [strip_label_eq_lam] THEN 297 SRW_TAC [DNF_ss][strip_label_subst, beta1_def, beta0_def, 298 relationTheory.RUNION, lLAM_eq_thm] THEN METIS_TAC [], 299 FULL_SIMP_TAC (srw_ss()) [LAM_eq_thm, relationTheory.RUNION, beta0_def, 300 beta1_def] THEN 301 SRW_TAC [DNF_ss][lLAMi_eq_thm, strip_label_subst, 302 fresh_tpm_subst, lemma15a] 303 ]); 304 305val lcc_beta_FV = store_thm( 306 "lcc_beta_FV", 307 ``!M N. lcompat_closure (beta0 RUNION beta1) M N ==> 308 !x. x IN FV N ==> x IN FV M``, 309 HO_MATCH_MP_TAC lcompat_closure_ind THEN 310 SRW_TAC [][relationTheory.RUNION, beta0_def, beta1_def] THEN 311 TRY (PROVE_TAC []) THEN 312 FULL_SIMP_TAC (srw_ss() ++ boolSimps.COND_elim_ss) [lFV_SUB] THEN 313 PROVE_TAC []); 314 315val lcc_beta_subst = store_thm( 316 "lcc_beta_subst", 317 ``!M N P v. lcompat_closure (beta0 RUNION beta1) M N ==> 318 lcompat_closure (beta0 RUNION beta1) ([P/v]M) ([P/v]N)``, 319 REPEAT GEN_TAC THEN MAP_EVERY Q.ID_SPEC_TAC [`N`, `M`] THEN 320 HO_MATCH_MP_TAC lcc_beta_bvc_ind THEN 321 Q.EXISTS_TAC `v INSERT FV P` THEN SRW_TAC [][lcompat_closure_rules] THENL [ 322 Q_TAC SUFF_TAC `beta1 (LAM v' ([P/v]M) @@ [P/v] N) ([P/v]([N/v']M))` 323 THEN1 METIS_TAC [lcompat_closure_rules, relationTheory.RUNION] THEN 324 SRW_TAC [][beta1_def] THEN 325 MAP_EVERY Q.EXISTS_TAC [`v'`, `[P/v]M`] THEN 326 SRW_TAC [][lSUBSTITUTION_LEMMA], 327 Q_TAC SUFF_TAC `beta0 (LAMi n v' ([P/v]M) ([P/v]N)) ([P/v]([N/v']M))` 328 THEN1 METIS_TAC [lcompat_closure_rules, relationTheory.RUNION] THEN 329 SRW_TAC [][beta0_def] THEN 330 MAP_EVERY Q.EXISTS_TAC [`n`,`v'`, `[P/v]M`, `[P/v]N`] THEN 331 SRW_TAC [][lSUBSTITUTION_LEMMA] 332 ]); 333 334val lcc_beta_ltpm_imp = store_thm( 335 "lcc_beta_ltpm_imp", 336 ``!M N. lcompat_closure (beta0 RUNION beta1) M N ==> 337 !pi. lcompat_closure (beta0 RUNION beta1) (ltpm pi M) (ltpm pi N)``, 338 HO_MATCH_MP_TAC lcompat_closure_ind THEN 339 SRW_TAC [][lcompat_closure_rules] THEN 340 FULL_SIMP_TAC (srw_ss()) [beta0_def, beta1_def, relationTheory.RUNION] THEN 341 SRW_TAC [][ltpm_subst] THEN 342 METIS_TAC [relationTheory.RUNION, beta0_def, beta1_def, 343 lcompat_closure_rules]); 344 345val lcc_beta_ltpm_eqn = store_thm( 346 "lcc_beta_ltpm_eqn", 347 ``lcompat_closure (beta0 RUNION beta1) (ltpm pi M) N = 348 lcompat_closure (beta0 RUNION beta1) M (ltpm (REVERSE pi) N)``, 349 METIS_TAC [lcc_beta_ltpm_imp, pmact_inverse]); 350 351val lcc_beta_LAM = store_thm( 352 "lcc_beta_LAM", 353 ``!v t N. lcompat_closure (beta0 RUNION beta1) (LAM v t) N = 354 ?N0. (N = LAM v N0) /\ 355 lcompat_closure (beta0 RUNION beta1) t N0``, 356 REPEAT GEN_TAC THEN 357 CONV_TAC (LAND_CONV (REWR_CONV lcompat_closure_cases)) THEN 358 SRW_TAC [][beta0_def, beta1_def, relationTheory.RUNION] THEN EQ_TAC THEN 359 STRIP_TAC THENL [ 360 FULL_SIMP_TAC (srw_ss()) [lLAM_eq_thm] THEN 361 SRW_TAC [][ltpm_eqr, lcc_beta_ltpm_eqn, pmact_flip_args] THEN 362 METIS_TAC [lcc_beta_FV], 363 METIS_TAC [] 364 ]); 365 366val cc_beta_matched = store_thm( 367 "cc_beta_matched", 368 ``!M N. compat_closure beta M N ==> 369 !M'. (M = strip_label M') ==> 370 ?N'. lcompat_closure (beta0 RUNION beta1) M' N' /\ 371 (N = strip_label N')``, 372 HO_MATCH_MP_TAC compat_closure_ind THEN REPEAT CONJ_TAC THENL [ 373 SIMP_TAC (srw_ss() ++ boolSimps.DNF_ss) 374 [beta_def, strip_label_eq_redex] THEN 375 SRW_TAC [][] THEN 376 Q.EXISTS_TAC `[u'/x]t'` THEN SRW_TAC [][strip_label_subst] THENL [ 377 METIS_TAC [lcompat_closure_rules, beta1_def, relationTheory.RUNION], 378 METIS_TAC [lcompat_closure_rules, beta0_def, relationTheory.RUNION] 379 ], 380 REPEAT GEN_TAC THEN STRIP_TAC THEN GEN_TAC THEN 381 `(���s. M' = VAR s) ��� (���t1 t2. M' = t1 @@ t2) ��� (���v t. M' = LAM v t) ��� 382 (���n v t1 t2. M' = LAMi n v t1 t2)` 383 by (Q.SPEC_THEN `M'` STRUCT_CASES_TAC lterm_CASES THEN SRW_TAC [][] THEN 384 METIS_TAC []) THEN 385 SRW_TAC [][] THENL [ 386 FIRST_X_ASSUM (Q.SPEC_THEN `t2` MP_TAC) THEN SRW_TAC [][] THEN 387 Q.EXISTS_TAC `t1 @@ N'` THEN SRW_TAC [][lcompat_closure_rules], 388 FIRST_X_ASSUM (Q.SPEC_THEN `t2` MP_TAC) THEN SRW_TAC [][] THEN 389 Q.EXISTS_TAC `LAMi n v t1 N'` THEN SRW_TAC [][lcompat_closure_rules] 390 ], 391 REPEAT GEN_TAC THEN STRIP_TAC THEN GEN_TAC THEN 392 `(���s. M' = VAR s) ��� (���t1 t2. M' = t1 @@ t2) ��� (���v t. M' = LAM v t) ��� 393 (���n v t1 t2. M' = LAMi n v t1 t2)` 394 by (Q.SPEC_THEN `M'` STRUCT_CASES_TAC lterm_CASES THEN SRW_TAC [][] THEN 395 METIS_TAC []) THEN 396 SRW_TAC [][] THENL [ 397 FIRST_X_ASSUM (Q.SPEC_THEN `t1` MP_TAC) THEN SRW_TAC [][] THEN 398 Q.EXISTS_TAC `N' @@ t2` THEN SRW_TAC [][lcompat_closure_rules], 399 FIRST_X_ASSUM (Q.SPEC_THEN `LAM v t1` MP_TAC) THEN 400 SRW_TAC [][lcc_beta_LAM] THEN 401 Q.EXISTS_TAC `LAMi n v N0 t2` THEN SRW_TAC [][lcompat_closure_rules] 402 ], 403 SRW_TAC [][strip_label_eq_lam] THEN 404 FIRST_X_ASSUM (Q.SPEC_THEN `t'` MP_TAC) THEN SRW_TAC [][] THEN 405 Q.EXISTS_TAC `LAM v N'` THEN SRW_TAC [][lcompat_closure_rules] THEN 406 METIS_TAC [] 407 ]); 408 409val lemma11_1_6i = store_thm( 410 "lemma11_1_6i", 411 ``!M' N. reduction beta (strip_label M') N ==> 412 ?N'. RTC (lcompat_closure (beta0 RUNION beta1)) M' N' /\ 413 (N = strip_label N')``, 414 SIMP_TAC (srw_ss()) [] THEN 415 Q_TAC SUFF_TAC 416 `!M N. RTC (compat_closure beta) M N ==> 417 !M'. (M = strip_label M') ==> 418 ?N'. RTC (lcompat_closure (beta0 RUNION beta1)) M' N' /\ 419 (N = strip_label N')` THEN1 PROVE_TAC [] THEN 420 HO_MATCH_MP_TAC relationTheory.RTC_INDUCT THEN CONJ_TAC THEN 421 PROVE_TAC [relationTheory.RTC_RULES, cc_beta_matched]); 422 423val lcc_beta_matching_beta = store_thm( 424 "lcc_beta_matching_beta", 425 ``!M' N'. lcompat_closure (beta0 RUNION beta1) M' N' ==> 426 compat_closure beta (strip_label M') (strip_label N')``, 427 HO_MATCH_MP_TAC lcompat_closure_ind THEN 428 SRW_TAC [][strip_label_thm] THEN1 429 (Q_TAC SUFF_TAC `beta (strip_label M') (strip_label N')` THEN1 430 PROVE_TAC [compat_closure_rules] THEN 431 FULL_SIMP_TAC (srw_ss()) [beta0_def, beta1_def, relationTheory.RUNION, 432 strip_label_thm, beta_def, 433 strip_label_subst] THEN PROVE_TAC []) THEN 434 PROVE_TAC [compat_closure_rules]); 435 436val lemma11_1_6ii = store_thm( 437 "lemma11_1_6ii", 438 ``!M' N'. 439 RTC (lcompat_closure (beta0 RUNION beta1)) M' N' ==> 440 reduction beta (strip_label M') (strip_label N')``, 441 HO_MATCH_MP_TAC relationTheory.RTC_INDUCT THEN 442 PROVE_TAC [reduction_rules, lcc_beta_matching_beta]); 443 444val coFV_phi = prove( 445 ``~(v IN FV M) ==> ~(v IN FV (phi M))``, 446 METIS_TAC [FV_phi]); 447 448val lemma11_1_7i = store_thm( 449 "lemma11_1_7i", 450 ``!M. phi ([N/x]M) = [phi N/x] (phi M)``, 451 HO_MATCH_MP_TAC lterm_bvc_induction THEN Q.EXISTS_TAC `x INSERT FV N` THEN 452 SRW_TAC [][SUB_THM, coFV_phi, lSUB_VAR, SUB_VAR] THEN 453 SRW_TAC [][chap2Theory.substitution_lemma, coFV_phi]); 454 455val lcc_beta_phi_matched = store_thm( 456 "lcc_beta_phi_matched", 457 ``!M N. lcompat_closure (beta0 RUNION beta1) M N ==> 458 reduction beta (phi M) (phi N)``, 459 HO_MATCH_MP_TAC lcompat_closure_ind THEN 460 SRW_TAC [][] THENL [ 461 FULL_SIMP_TAC (srw_ss()) [beta0_def, beta1_def, relationTheory.RUNION] 462 THENL [ 463 SRW_TAC [][lemma11_1_7i, reduction_rules], 464 Q_TAC SUFF_TAC `beta (LAM v (phi t) @@ phi u) (phi ([u/v] t))` THEN1 465 PROVE_TAC [reduction_rules] THEN 466 SRW_TAC [][lemma11_1_7i, beta_def] THEN PROVE_TAC [] 467 ], 468 469 PROVE_TAC [reduction_rules], 470 PROVE_TAC [reduction_rules], 471 PROVE_TAC [reduction_beta_subst], 472 PROVE_TAC [lemma3_8] 473 ]); 474 475val lemma11_1_7ii = store_thm( 476 "lemma11_1_7ii", 477 ``!M N. RTC (lcompat_closure (beta0 RUNION beta1)) M N ==> 478 reduction beta (phi M) (phi N)``, 479 HO_MATCH_MP_TAC relationTheory.RTC_INDUCT THEN 480 PROVE_TAC [reduction_rules, lcc_beta_phi_matched]); 481 482val lemma11_1_8 = store_thm( 483 "lemma11_1_8", 484 ``!M. reduction beta (strip_label M) (phi M)``, 485 HO_MATCH_MP_TAC lterm_bvc_induction THEN Q.EXISTS_TAC `{}` THEN 486 SIMP_TAC (srw_ss()) [strip_label_thm, reduction_rules] THEN CONJ_TAC THENL [ 487 PROVE_TAC [reduction_rules], 488 MAP_EVERY Q.X_GEN_TAC [`s`, `M`, `M'`] THEN STRIP_TAC THEN 489 `beta (LAM s (strip_label M) @@ strip_label M') 490 ([strip_label M'/s] (strip_label M))` by PROVE_TAC [beta_def] THEN 491 `reduction beta ([strip_label M'/s] (strip_label M)) 492 ([phi M'/s] (strip_label M))` by PROVE_TAC [lemma3_8] THEN 493 `reduction beta ([phi M'/s] (strip_label M)) 494 ([phi M'/s] (phi M))` by 495 PROVE_TAC [reduction_beta_subst, l14a] THEN 496 PROVE_TAC [reduction_rules] 497 ]); 498 499val can_index_redex = store_thm( 500 "can_index_redex", 501 ``!M N. compat_closure beta M N ==> 502 ?M'. (strip_label M' = M) /\ (phi M' = N)``, 503 HO_MATCH_MP_TAC compat_closure_ind THEN REPEAT CONJ_TAC THENL [ 504 MAP_EVERY Q.X_GEN_TAC [`M`,`N`] THEN 505 SIMP_TAC (srw_ss()) [beta_def, GSYM LEFT_FORALL_IMP_THM] THEN 506 MAP_EVERY Q.X_GEN_TAC [`x`,`body`,`arg`] THEN SRW_TAC [][] THEN 507 Q.EXISTS_TAC `LAMi 0 x (null_labelling body) (null_labelling arg)` THEN 508 SIMP_TAC (srw_ss()) [], 509 MAP_EVERY Q.X_GEN_TAC [`M`,`N`,`z`] THEN SRW_TAC [][] THEN 510 Q.EXISTS_TAC `null_labelling z @@ M'` THEN SRW_TAC [][], 511 MAP_EVERY Q.X_GEN_TAC [`M`,`N`,`z`] THEN SRW_TAC [][] THEN 512 Q.EXISTS_TAC `M' @@ null_labelling z` THEN SRW_TAC [][], 513 MAP_EVERY Q.X_GEN_TAC [`M`,`N`,`v`] THEN SRW_TAC [][] THEN 514 Q.EXISTS_TAC `LAM v M'` THEN 515 ASM_SIMP_TAC (srw_ss()) [] 516 ]); 517 518val strip_lemma = store_thm( 519 "strip_lemma", 520 ``!M M' N. compat_closure beta M M' /\ 521 reduction beta M N ==> 522 ?N'. reduction beta M' N' /\ reduction beta N N'``, 523 REPEAT STRIP_TAC THEN 524 `?Mtilde. (strip_label Mtilde = M) /\ (phi Mtilde = M')` by 525 PROVE_TAC [can_index_redex] THEN 526 `?Ntilde. (N = strip_label Ntilde) /\ 527 RTC (lcompat_closure (beta0 RUNION beta1)) Mtilde Ntilde` by 528 PROVE_TAC [lemma11_1_6i] THEN 529 `reduction beta M' (phi Ntilde)` by PROVE_TAC [lemma11_1_7ii] THEN 530 `reduction beta N (phi Ntilde)` by PROVE_TAC [lemma11_1_8] THEN 531 PROVE_TAC []); 532 533val beta_CR_2 = store_thm( 534 "beta_CR_2", 535 ``CR beta``, 536 SIMP_TAC (srw_ss())[CR_def, diamond_property_def] THEN 537 Q_TAC SUFF_TAC 538 `!M M1. RTC (compat_closure beta) M M1 ==> 539 !M2. reduction beta M M2 ==> 540 ?M3. reduction beta M1 M3 /\ reduction beta M2 M3` 541 THEN1 PROVE_TAC [] THEN 542 HO_MATCH_MP_TAC relationTheory.RTC_INDUCT THEN 543 PROVE_TAC [reduction_rules, strip_lemma]); 544 545val _ = export_theory() 546