1open HolKernel Parse boolLib bossLib BasicProvers metisLib 2 3local open stringTheory in end 4 5open pred_setTheory binderLib boolSimps relationTheory 6open chap3Theory 7 8(* ---------------------------------------------------------------------- 9 10 This theory demonstrates that the quotiented theory of 11 lambda-calculus in the rest of the development is a good model of 12 the "raw" theory of lambda calculus syntax. 13 14 The raw syntax here and the relations on it are taken from 15 16 "A formalised first-order confluence proof of for the \lambda-calculus 17 using one-sorted variable names" 18 19 by Rene Vestergaard and James Brotherston 20 21 which appeared in Information and Computation, 183:2. 22 (A pre-print of this paper is available at 23 http://www.jaist.ac.jp/~vester/Writings/vestergaard-brotherston-IandC-rta01.ps.gz) 24 25 In this paper, the "real \lambda-calculus" is established by 26 taking a quotient of raw syntax terms, and the notion of 27 beta-reduction in the real type is defined such that 28 29 collapse e_1 -->_\beta collapse e_2 30 31 = (by defn) 32 33 e1 ==_\alpha ; -->_\beta ; ==_\alpha e2 34 35 (Where collapse is written graphically in the paper as the "round 36 down operator". Also, in the theory below, the semi-colon is 37 replaced with the relation composition operator O.) 38 39 I show the above is a theorem of the development. 40 41 The collapse function below has the important property that 42 43 EQC alpha x y = (collapse x = collapse y) 44 45 I.e., two raw syntax terms are alpha-equivalent iff they collapse 46 to the same quotiented term. 47 48 ---------------------------------------------------------------------- *) 49 50val _ = new_theory "raw_syntax" 51 52val _ = Hol_datatype `raw_term = var of string 53 | app of raw_term => raw_term 54 | lam of string => raw_term`; 55 56val fv_def = Define` 57 (fv (var s) = {s}) /\ 58 (fv (app t u) = fv t UNION fv u) /\ 59 (fv (lam v t) = fv t DELETE v)`; 60 61val FINITE_fv = store_thm( 62 "FINITE_fv", 63 ``!t. FINITE (fv t)``, 64 Induct THEN SRW_TAC [][fv_def]); 65val _ = export_rewrites ["FINITE_fv"] 66 67val capt_def = Define` 68 (capt x (var y) = {}) /\ 69 (capt x (app t u) = capt x t UNION capt x u) /\ 70 (capt x (lam y t) = if ~(x = y) /\ x IN fv t then {y} UNION capt x t 71 else {}) 72` 73 74val FINITE_capt = store_thm( 75 "FINITE_capt", 76 ``!t v. FINITE (capt v t)``, 77 Induct THEN SRW_TAC [][capt_def]); 78val _ = export_rewrites ["FINITE_capt"] 79 80val capt_fv = store_thm( 81 "capt_fv", 82 ``!e x. ~(x IN fv e) ==> (capt x e = {})``, 83 Induct THEN SRW_TAC [][capt_def, fv_def]); 84val _ = export_rewrites ["capt_fv"] 85 86val subst_def = Define` 87 (subst x y (var s) = if y = s then x else var s) /\ 88 (subst x y (app t u) = app (subst x y t) (subst x y u)) /\ 89 (subst x y (lam v t) = if ~(y = v) /\ ~(v IN fv x) then lam v (subst x y t) 90 else lam v t) 91`; 92 93val (ialpha_rules, ialpha_ind, ialpha_cases) = Hol_reln` 94 (!x y e. ~(y IN capt x e UNION fv e) ==> 95 ialpha y (lam x e) (lam y (subst (var y) x e))) /\ 96 (!e e' x y. ialpha y e e' ==> ialpha y (lam x e) (lam x e')) /\ 97 (!e1 e1' e2 y. ialpha y e1 e1' ==> ialpha y (app e1 e2) (app e1' e2)) /\ 98 (!e1 e2 e2' y. ialpha y e2 e2' ==> ialpha y (app e1 e2) (app e1 e2')) 99`; 100 101val (beta_rules, beta_ind, beta_cases) = Hol_reln` 102 (!e1 e2 x. (fv e2 INTER capt x e1 = {}) ==> 103 beta (app (lam x e1) e2) (subst e2 x e1)) /\ 104 (!e e' x. beta e e' ==> beta (lam x e) (lam x e')) /\ 105 (!e1 e1' e2. beta e1 e1' ==> beta (app e1 e2) (app e1' e2)) /\ 106 (!e1 e2 e2'. beta e2 e2' ==> beta (app e1 e2) (app e1 e2')) 107`; 108 109val alpha_def = Define`alpha e1 e2 = ?y. ialpha y e1 e2` 110 111val renaming_sanity1 = store_thm( 112 "renaming_sanity1", 113 ``!e x. subst (var x) x e = e``, 114 Induct THEN SRW_TAC [][subst_def]); 115val _ = export_rewrites ["renaming_sanity1"] 116 117val renaming_sanity2 = store_thm( 118 "renaming_sanity2", 119 ``!e x e'. ~(x IN fv e) ==> (subst e' x e = e)``, 120 Induct THEN SRW_TAC [][subst_def, fv_def]); 121val _ = export_rewrites ["renaming_sanity2"] 122 123val RIGHT_INTER_OVER_UNION = prove( 124 ``(x UNION y) INTER z = (x INTER z) UNION (y INTER z)``, 125 SRW_TAC [][EXTENSION] THEN tautLib.TAUT_TAC) 126 127val SING_INTER = prove( 128 ``({x} INTER Y = if x IN Y then {x} else {}) /\ 129 (Y INTER {x} = if x IN Y then {x} else {})``, 130 SRW_TAC [][EXTENSION] THEN PROVE_TAC []); 131 132val renaming_sanity3 = store_thm( 133 "renaming_sanity3", 134 ``!e e' x. ~(x IN fv e') /\ (capt x e INTER fv e' = {}) ==> 135 ~(x IN fv (subst e' x e))``, 136 Induct THEN 137 SRW_TAC [][capt_def, fv_def, subst_def, 138 RIGHT_INTER_OVER_UNION, SING_INTER] THEN 139 FULL_SIMP_TAC (srw_ss()) []); 140 141val renaming_sanity4 = store_thm( 142 "renaming_sanity4", 143 ``!e x y. ~(y IN fv e) ==> (subst (var x) y (subst (var y) x e) = e)``, 144 Induct THEN SRW_TAC [][fv_def, subst_def] THEN 145 SRW_TAC [][]); 146 147val collapse_def = Define` 148 (collapse (var s) = VAR s) /\ 149 (collapse (app t u) = collapse t @@ collapse u) /\ 150 (collapse (lam v t) = LAM v (collapse t))`; 151 152open termTheory 153 154val FV_collapse = store_thm( 155 "FV_collapse", 156 ``!e. FV (collapse e) = fv e``, 157 Induct THEN SRW_TAC [][collapse_def, fv_def]); 158val _ = export_rewrites ["FV_collapse"] 159 160val fv_vsubst = store_thm( 161 "fv_vsubst", 162 ``!e x y. ~(y IN capt x e) ==> 163 (fv (subst (var y) x e) = 164 if x IN fv e then y INSERT (fv e DELETE x) 165 else fv e)``, 166 Induct THEN 167 SRW_TAC [][fv_def, capt_def, subst_def, EXTENSION] THEN 168 FULL_SIMP_TAC (srw_ss()) [] THEN PROVE_TAC []); 169 170val collapse_vsubst = store_thm( 171 "collapse_vsubst", 172 ``!e x y. ~(y IN capt x e) ==> 173 (collapse (subst (var y) x e) = [VAR y/x] (collapse e))``, 174 Induct THEN 175 ASM_SIMP_TAC (srw_ss()) [collapse_def, capt_def, fv_def, subst_def, 176 SUB_VAR, SUB_THM] 177 THENL [ 178 REPEAT GEN_TAC THEN COND_CASES_TAC THEN SRW_TAC [][collapse_def], 179 MAP_EVERY Q.X_GEN_TAC [`s`, `x`, `y`] THEN 180 Cases_on `x = s` THEN ASM_SIMP_TAC (srw_ss()) [collapse_def, SUB_THM] THEN 181 Cases_on `s = y` THEN 182 ASM_SIMP_TAC (srw_ss()) [collapse_def, SUB_THM, lemma14b] THENL [ 183 Cases_on `x IN fv e` THEN 184 ASM_SIMP_TAC (srw_ss()) [] THEN 185 `~(x IN FV (collapse e))` by SRW_TAC [][] THEN 186 `~(x IN FV (LAM y (collapse e)))` by SRW_TAC [][] THEN 187 SRW_TAC [][lemma14b], 188 Cases_on `x IN fv e` THEN ASM_SIMP_TAC (srw_ss()) [] 189 ] 190 ]); 191 192val collapse_subst = store_thm( 193 "collapse_subst", 194 ``!t u v. (capt v t INTER fv u = {}) ==> 195 (collapse (subst u v t) = [collapse u/v] (collapse t))``, 196 Induct THEN 197 ASM_SIMP_TAC (srw_ss()) [collapse_def, capt_def, fv_def, subst_def, 198 SUB_VAR, SUB_THM, RIGHT_INTER_OVER_UNION] 199 THENL [ 200 REPEAT GEN_TAC THEN SRW_TAC [][collapse_def], 201 REPEAT GEN_TAC THEN SRW_TAC [][collapse_def, RIGHT_INTER_OVER_UNION, 202 SUB_THM] THEN 203 FULL_SIMP_TAC (srw_ss() ++ COND_elim_ss) [SING_INTER, SUB_THM, lemma14b] 204 ]); 205 206 207val x_IN_capt_x = store_thm( 208 "x_IN_capt_x", 209 ``!t. ~(x IN capt x t)``, 210 Induct THEN SRW_TAC [][capt_def]); 211 212val capt_subst2 = prove( 213 ``!t. 214 ~(v IN capt x t) /\ ~(v IN fv t) ==> 215 ~(x IN capt v (subst (var v) x t))``, 216 Induct THEN SRW_TAC [][capt_def, subst_def, fv_def, fv_vsubst] THEN 217 FULL_SIMP_TAC (srw_ss()) []); 218 219val ialpha_sym = store_thm( 220 "ialpha_sym", 221 ``!y t1 t2. ialpha y t1 t2 ==> ?z. ialpha z t2 t1``, 222 HO_MATCH_MP_TAC ialpha_ind THEN SRW_TAC [][] THENL [ 223 Cases_on `x = y` THENL [ 224 SRW_TAC [][renaming_sanity1] THEN 225 Q.EXISTS_TAC `x` THEN 226 Q_TAC SUFF_TAC `~(x IN fv (subst (var x) x e))` THEN 227 METIS_TAC [ialpha_rules, renaming_sanity1, 228 pred_setTheory.IN_UNION], 229 `~(x IN fv (subst (var y) x e))` 230 by SRW_TAC [][fv_vsubst] THEN 231 Q_TAC SUFF_TAC `~(x IN capt y (subst (var y) x e))` 232 THEN1 METIS_TAC [renaming_sanity4, ialpha_rules, 233 pred_setTheory.IN_UNION] THEN 234 SRW_TAC [][capt_subst2] 235 ], 236 METIS_TAC [ialpha_rules], 237 METIS_TAC [ialpha_rules], 238 METIS_TAC [ialpha_rules] 239 ]); 240 241val alpha_sym = store_thm( 242 "alpha_sym", 243 ``alpha x y ==> alpha y x``, 244 METIS_TAC [alpha_def, ialpha_sym]); 245 246val alpha_CONG = store_thm( 247 "alpha_CONG", 248 ``!t t'. alpha t t' ==> 249 (!u. alpha (app t u) (app t' u) /\ 250 alpha (app u t) (app u t')) /\ 251 (!v. alpha (lam v t) (lam v t'))``, 252 SRW_TAC [][alpha_def] THEN PROVE_TAC [ialpha_rules]); 253 254val EQC_alpha_CONG = store_thm( 255 "EQC_alpha_CONG", 256 ``!t t'. EQC alpha t t' ==> 257 (!u. EQC alpha (app t u) (app t' u) /\ 258 EQC alpha (app u t) (app u t')) /\ 259 (!v. EQC alpha (lam v t) (lam v t'))``, 260 HO_MATCH_MP_TAC relationTheory.EQC_INDUCTION THEN 261 SRW_TAC [][] THEN 262 PROVE_TAC [alpha_CONG, EQC_R, EQC_SYM, EQC_TRANS]); 263 264 265 266val EQC_alpha_CONG2 = store_thm( 267 "EQC_alpha_CONG2", 268 ``!t t' u u'. EQC alpha t t' /\ EQC alpha u u' ==> 269 EQC alpha (app t u) (app t' u')``, 270 METIS_TAC [EQC_alpha_CONG, EQC_TRANS]); 271 272val ialpha_lam_lemma = prove( 273 ``!y t u. ialpha y t u ==> 274 !v t0 s k t1 t2. 275 ((t = lam v t0) ==> 276 ~(u = var s) /\ ~(u = app t1 t2)) /\ 277 ((u = lam v t0) ==> 278 ~(t = var s) /\ ~(t = app t1 t2))``, 279 HO_MATCH_MP_TAC ialpha_ind THEN SRW_TAC [][]); 280 281val ialpha_lam_thm = save_thm( 282 "ialpha_lam_thm", 283 SIMP_RULE (srw_ss() ++ DNF_ss) [] ialpha_lam_lemma) 284 285val alpha_lam_thm = store_thm( 286 "alpha_lam_thm", 287 ``(!v t0 s. ~alpha (lam v t0) (var s) /\ ~alpha (var s) (lam v t0)) /\ 288 (!v t0 t1 t2. 289 ~alpha (lam v t0) (app t1 t2) /\ ~alpha (app t1 t2) (lam v t0))``, 290 METIS_TAC [alpha_def, ialpha_lam_thm]); 291val _ = export_rewrites ["alpha_lam_thm"] 292 293val EQC_alpha_lam_lemma = prove( 294 ``!t u. EQC alpha t u ==> 295 !v t0 s k t1 t2. 296 ((t = lam v t0) ==> 297 ~(u = var s) /\ ~(u = app t1 t2)) /\ 298 ((u = lam v t0) ==> 299 ~(t = var s) /\ ~(t = app t1 t2))``, 300 HO_MATCH_MP_TAC EQC_INDUCTION THEN REPEAT STRIP_TAC THEN SRW_TAC [][] THEN 301 FULL_SIMP_TAC (srw_ss()) [] THEN Cases_on `t'` THEN 302 FULL_SIMP_TAC (srw_ss()) []); 303 304val EQC_alpha_lam_thm = save_thm( 305 "EQC_alpha_lam_thm", 306 SIMP_RULE (srw_ss() ++ DNF_ss) [] EQC_alpha_lam_lemma) 307val _ = export_rewrites ["EQC_alpha_lam_thm"] 308 309val alpha_collapse = store_thm( 310 "alpha_collapse", 311 ``!t u. EQC alpha t u ==> (collapse t = collapse u)``, 312 HO_MATCH_MP_TAC relationTheory.EQC_INDUCTION THEN 313 SIMP_TAC (srw_ss()) [alpha_def] THEN 314 Q_TAC SUFF_TAC `!y t u. ialpha y t u ==> (collapse t = collapse u)` 315 THEN1 PROVE_TAC [] THEN 316 HO_MATCH_MP_TAC ialpha_ind THEN 317 SIMP_TAC (srw_ss()) [collapse_def, collapse_vsubst] THEN REPEAT STRIP_TAC THEN 318 MATCH_MP_TAC SIMPLE_ALPHA THEN SRW_TAC [][]); 319 320val alpha_fv_invariant = store_thm( 321 "alpha_fv_invariant", 322 ``!t u. EQC alpha t u ==> (fv t = fv u)``, 323 HO_MATCH_MP_TAC EQC_INDUCTION THEN SIMP_TAC (srw_ss()) [alpha_def] THEN 324 Q_TAC SUFF_TAC `!y t u. ialpha y t u ==> (fv t = fv u)` 325 THEN1 PROVE_TAC [] THEN 326 HO_MATCH_MP_TAC ialpha_ind THEN SRW_TAC [][fv_def, fv_vsubst] THEN 327 SRW_TAC [][EXTENSION] THEN PROVE_TAC []); 328 329val capt_subst = store_thm( 330 "capt_subst", 331 ``!t x y z. ~(x = y) /\ ~(y IN capt z t) ==> 332 (capt x (subst (var y) z t) = 333 if x = z then {} else capt x t)``, 334 Induct THEN SRW_TAC [][subst_def, capt_def, fv_def, fv_vsubst] THEN 335 FULL_SIMP_TAC (srw_ss()) []); 336 337val alpha_eq_safe_subst = store_thm( 338 "alpha_eq_safe_subst", 339 ``!t. ?t'. EQC alpha t t' /\ (capt x t' INTER fv u = {})``, 340 Induct THEN FULL_SIMP_TAC (srw_ss()) [] THENL [ 341 Q.X_GEN_TAC `s` THEN Q.EXISTS_TAC `var s` THEN SRW_TAC [][capt_def], 342 Q.EXISTS_TAC `app t'' t'''` THEN 343 SRW_TAC [][capt_def, RIGHT_INTER_OVER_UNION] THEN 344 METIS_TAC [EQC_alpha_CONG2], 345 Q.X_GEN_TAC `s` THEN 346 Cases_on `x IN fv t` THENL [ 347 Cases_on `s IN fv u` THENL [ 348 Q_TAC (NEW_TAC "z") 349 `fv t UNION fv u UNION {s;x} UNION capt s t'` THEN 350 Q.EXISTS_TAC `lam z (subst (var z) s t')` THEN 351 CONJ_TAC THENL [ 352 MATCH_MP_TAC EQC_TRANS THEN 353 Q.EXISTS_TAC `lam s t'` THEN CONJ_TAC THENL [ 354 PROVE_TAC [EQC_alpha_CONG], 355 MATCH_MP_TAC EQC_R THEN 356 SRW_TAC [][alpha_def] THEN Q.EXISTS_TAC `z` THEN 357 MATCH_MP_TAC (hd (CONJUNCTS ialpha_rules)) THEN 358 SRW_TAC [][] THEN PROVE_TAC [alpha_fv_invariant] 359 ], 360 SRW_TAC [][capt_def, capt_subst, RIGHT_INTER_OVER_UNION, SING_INTER] 361 ], 362 Q.EXISTS_TAC `lam s t'` THEN CONJ_TAC THENL [ 363 PROVE_TAC [EQC_alpha_CONG], 364 SRW_TAC [][capt_def, RIGHT_INTER_OVER_UNION, SING_INTER] 365 ] 366 ], 367 Q.EXISTS_TAC `lam s t'` THEN CONJ_TAC THENL [ 368 PROVE_TAC [EQC_alpha_CONG], 369 SRW_TAC [][capt_def] THEN PROVE_TAC [alpha_fv_invariant] 370 ] 371 ] 372 ]); 373 374val LAM_INJ_ALPHA_FV = prove( 375 ``~(v1 = v2) /\ (LAM v1 t1 = LAM v2 t2) ==> 376 ~(v1 IN FV t2) /\ ~(v2 IN FV t1)``, 377 SRW_TAC [][LAM_eq_thm] THEN SRW_TAC [][]); 378val INJECTIVITY_LEMMA1 = prove( 379 ``(LAM v1 t1 = LAM v2 t2) ==> (t1 = [VAR v1/v2]t2)``, 380 SRW_TAC [][LAM_eq_thm] THEN SRW_TAC [][fresh_tpm_subst]); 381 382val collapse_alpha = store_thm( 383 "collapse_alpha", 384 ``!t u. (collapse t = collapse u) ==> EQC alpha t u``, 385 Induct THEN REPEAT GEN_TAC THEN Cases_on `u` THEN 386 SRW_TAC [][collapse_def] THENL [ 387 PROVE_TAC [EQC_alpha_CONG2], 388 REPEAT (POP_ASSUM MP_TAC) THEN 389 Q_TAC SUFF_TAC 390 `!t s s' t'. 391 (!u. (collapse t = collapse u) ==> EQC alpha t u) /\ 392 (LAM s (collapse t) = LAM s' (collapse t')) ==> 393 EQC alpha (lam s t) (lam s' t')` THEN1 METIS_TAC [] THEN 394 REPEAT STRIP_TAC THEN 395 Cases_on `s = s'` THENL [ 396 FULL_SIMP_TAC (srw_ss()) [] THEN 397 METIS_TAC [EQC_alpha_CONG], 398 `collapse t = [VAR s/s'] (collapse t')` 399 by PROVE_TAC [INJECTIVITY_LEMMA1] THEN 400 `~(s IN FV (collapse t')) /\ ~(s' IN FV (collapse t))` 401 by PROVE_TAC [LAM_INJ_ALPHA_FV] THEN 402 MATCH_MP_TAC EQC_TRANS THEN 403 `?t2. EQC alpha t' t2 /\ (capt s' t2 INTER fv (var s) = {})` 404 by PROVE_TAC [alpha_eq_safe_subst] THEN 405 `collapse t' = collapse t2` by PROVE_TAC [alpha_collapse] THEN 406 `~(s IN capt s' t2)` 407 by FULL_SIMP_TAC (srw_ss() ++ COND_elim_ss) [SING_INTER, fv_def] THEN 408 `[VAR s/s'] (collapse t2) = collapse (subst (var s) s' t2)` 409 by METIS_TAC [collapse_vsubst] THEN 410 `EQC alpha t (subst (var s) s' t2)` by METIS_TAC [] THEN 411 `EQC alpha (lam s t) (lam s (subst (var s) s' t2))` 412 by METIS_TAC [EQC_alpha_CONG] THEN 413 `EQC alpha (lam s (subst (var s) s' t2)) (lam s' t2)` 414 by (MATCH_MP_TAC EQC_SYM THEN 415 MATCH_MP_TAC EQC_R THEN REWRITE_TAC [alpha_def] THEN 416 Q.EXISTS_TAC `s` THEN 417 MATCH_MP_TAC (hd (CONJUNCTS ialpha_rules)) THEN 418 FULL_SIMP_TAC (srw_ss()) [] THEN 419 PROVE_TAC [alpha_fv_invariant]) THEN 420 PROVE_TAC [EQC_TRANS, EQC_SYM, EQC_alpha_CONG] 421 ] 422 ]); 423 424val EQC_alpha_collapse_EQ = store_thm( 425 "EQC_alpha_collapse_EQ", 426 ``EQC alpha t u = (collapse t = collapse u)``, 427 PROVE_TAC [collapse_alpha, alpha_collapse]); 428 429val collapse_ONTO = store_thm( 430 "collapse_ONTO", 431 ``!M. ?t. collapse t = M``, 432 HO_MATCH_MP_TAC simple_induction THEN METIS_TAC [collapse_def]); 433 434val beta_ccbeta = store_thm( 435 "beta_ccbeta", 436 ``!t u. beta t u ==> compat_closure beta (collapse t) (collapse u)``, 437 HO_MATCH_MP_TAC beta_ind THEN 438 SRW_TAC [][compat_closure_rules, collapse_def] THEN 439 SRW_TAC [][collapse_subst, INTER_COMM] THEN 440 SRW_TAC [][cc_beta_thm] THEN PROVE_TAC []); 441 442val gmbeta_beta = store_thm( 443 "gmbeta_beta", 444 ``!t u. beta (collapse t) (collapse u) ==> 445 (EQC alpha O beta O EQC alpha) t u``, 446 SIMP_TAC (srw_ss()) [beta_def, O_DEF] THEN REPEAT GEN_TAC THEN 447 DISCH_THEN (Q.X_CHOOSE_THEN `v` 448 (Q.X_CHOOSE_THEN `M` 449 (Q.X_CHOOSE_THEN `N` STRIP_ASSUME_TAC))) THEN 450 `?f x. t = app f x` 451 by (Cases_on `t` THEN FULL_SIMP_TAC (srw_ss()) [collapse_def]) THEN 452 POP_ASSUM SUBST_ALL_TAC THEN FULL_SIMP_TAC (srw_ss()) [collapse_def] THEN 453 `?w t0. f = lam w t0` 454 by (Cases_on `f` THEN FULL_SIMP_TAC (srw_ss()) [collapse_def]) THEN 455 POP_ASSUM SUBST_ALL_TAC THEN FULL_SIMP_TAC (srw_ss()) [collapse_def] THEN 456 `?t1. EQC alpha t0 t1 /\ (capt w t1 INTER fv x = {})` 457 by PROVE_TAC [alpha_eq_safe_subst] THEN 458 `EQC alpha (app (lam w t0) x) (app (lam w t1) x)` 459 by METIS_TAC [EQC_alpha_CONG] THEN 460 `beta (app (lam w t1) x) (subst x w t1)` 461 by (MATCH_MP_TAC (hd (CONJUNCTS beta_rules)) THEN 462 FULL_SIMP_TAC (srw_ss()) [INTER_COMM]) THEN 463 Q_TAC SUFF_TAC `EQC alpha (subst x w t1) u` THEN1 PROVE_TAC [] THEN 464 ASM_SIMP_TAC (srw_ss()) [EQC_alpha_collapse_EQ, collapse_subst] THEN 465 `collapse t0 = collapse t1` by PROVE_TAC [alpha_collapse] THEN 466 POP_ASSUM SUBST_ALL_TAC THEN 467 Cases_on `v = w` THEN1 FULL_SIMP_TAC (srw_ss()) [] THEN 468 `M = [VAR v/w] (collapse t1)` by METIS_TAC [INJECTIVITY_LEMMA1] THEN 469 `~(v IN FV (collapse t1))` by METIS_TAC [LAM_INJ_ALPHA_FV] THEN 470 SRW_TAC [][lemma15a]); 471 472val beta_some_reflected = store_thm( 473 "beta_some_reflected", 474 ``!M N. compat_closure beta M N ==> 475 ?t u. (M = collapse t) /\ (N = collapse u) /\ 476 beta t u``, 477 HO_MATCH_MP_TAC ccbeta_ind THEN Q.EXISTS_TAC `{}` THEN SRW_TAC [][] THENL [ 478 `?m n. (collapse m = M) /\ (collapse n = N)` 479 by METIS_TAC [collapse_ONTO] THEN 480 `?m'. EQC alpha m m' /\ (capt v m' INTER fv n = {})` 481 by METIS_TAC [alpha_eq_safe_subst] THEN 482 MAP_EVERY Q.EXISTS_TAC [`app (lam v m') n`, `subst n v m'`] THEN 483 SRW_TAC [][collapse_def, GSYM EQC_alpha_collapse_EQ, collapse_subst] 484 THENL [ 485 METIS_TAC [EQC_alpha_collapse_EQ], 486 METIS_TAC [INTER_COMM, beta_rules] 487 ], 488 `?n. collapse n = N'` by METIS_TAC [collapse_ONTO] THEN 489 MAP_EVERY Q.EXISTS_TAC [`app t n`, `app u n`] THEN 490 SRW_TAC [][collapse_def, beta_rules], 491 `?m. collapse m = M` by METIS_TAC [collapse_ONTO] THEN 492 MAP_EVERY Q.EXISTS_TAC [`app m t`, `app m u`] THEN 493 SRW_TAC [][collapse_def, beta_rules], 494 MAP_EVERY Q.EXISTS_TAC [`lam v t`, `lam v u`] THEN 495 SRW_TAC [][collapse_def, beta_rules] 496 ]); 497 498val ccbeta_beta_lemma = prove( 499 ``!M N. compat_closure beta M N ==> 500 !t u. (M = collapse t) /\ (N = collapse u) ==> 501 (EQC alpha O beta O EQC alpha) t u``, 502 HO_MATCH_MP_TAC compat_closure_ind THEN 503 REPEAT STRIP_TAC THEN1 METIS_TAC [gmbeta_beta] THEN 504 FULL_SIMP_TAC (srw_ss()) [O_DEF] THENL [ 505 `?z1 m. (t = app z1 m) /\ (collapse z1 = z) /\ (collapse m = M)` 506 by (Cases_on `t` THEN FULL_SIMP_TAC (srw_ss()) [collapse_def]) THEN 507 `?z2 n. (u = app z2 n) /\ (collapse z2 = z) /\ (collapse n = N)` 508 by (Cases_on `u` THEN FULL_SIMP_TAC (srw_ss()) [collapse_def]) THEN 509 `?y1 y2. EQC alpha m y1 /\ beta y1 y2 /\ EQC alpha y2 n` 510 by METIS_TAC [] THEN 511 `EQC alpha (app z1 m) (app z1 y1)` by METIS_TAC [EQC_alpha_CONG] THEN 512 `beta (app z1 y1) (app z1 y2)` by METIS_TAC [beta_rules] THEN 513 METIS_TAC [EQC_alpha_CONG2, EQC_alpha_collapse_EQ], 514 515 `?z1 m. (t = app m z1) /\ (collapse z1 = z) /\ (collapse m = M)` 516 by (Cases_on `t` THEN FULL_SIMP_TAC (srw_ss()) [collapse_def]) THEN 517 `?z2 n. (u = app n z2) /\ (collapse z2 = z) /\ (collapse n = N)` 518 by (Cases_on `u` THEN FULL_SIMP_TAC (srw_ss()) [collapse_def]) THEN 519 `?y1 y2. EQC alpha m y1 /\ beta y1 y2 /\ EQC alpha y2 n` 520 by METIS_TAC [] THEN 521 `EQC alpha (app m z1) (app y1 z1)` by METIS_TAC [EQC_alpha_CONG] THEN 522 `beta (app y1 z1) (app y2 z1)` by METIS_TAC [beta_rules] THEN 523 METIS_TAC [EQC_alpha_CONG2, EQC_alpha_collapse_EQ], 524 525 `?s v'. (t = lam s v')` 526 by (Cases_on `t` THEN FULL_SIMP_TAC (srw_ss()) [collapse_def]) THEN 527 POP_ASSUM SUBST_ALL_TAC THEN FULL_SIMP_TAC (srw_ss()) [collapse_def] THEN 528 `?s' v''. (u = lam s' v'')` 529 by (Cases_on `u` THEN FULL_SIMP_TAC (srw_ss()) [collapse_def]) THEN 530 POP_ASSUM SUBST_ALL_TAC THEN FULL_SIMP_TAC (srw_ss()) [collapse_def] THEN 531 `?w. EQC alpha v' w /\ (capt s w INTER fv (var v) = {})` 532 by PROVE_TAC [alpha_eq_safe_subst] THEN 533 `~(v IN capt s w)` 534 by FULL_SIMP_TAC (srw_ss() ++ COND_elim_ss) [SING_INTER, fv_def] THEN 535 `collapse v' = collapse w` by PROVE_TAC [EQC_alpha_collapse_EQ] THEN 536 `M = [VAR v/s] (collapse w)` by PROVE_TAC [INJECTIVITY_LEMMA1] THEN 537 `M = collapse (subst (var v) s w)` by PROVE_TAC [collapse_vsubst] THEN 538 539 `?z. EQC alpha v'' z /\ (capt s' z INTER fv (var v) = {})` 540 by PROVE_TAC [alpha_eq_safe_subst] THEN 541 `~(v IN capt s' z)` 542 by FULL_SIMP_TAC (srw_ss() ++ COND_elim_ss) [SING_INTER, fv_def] THEN 543 `collapse v'' = collapse z` by PROVE_TAC [EQC_alpha_collapse_EQ] THEN 544 `N = [VAR v/s'] (collapse z)` by PROVE_TAC [INJECTIVITY_LEMMA1] THEN 545 `N = collapse (subst (var v) s' z)` by PROVE_TAC [collapse_vsubst] THEN 546 `?a b. EQC alpha (subst (var v) s w) a /\ beta a b /\ 547 EQC alpha b (subst (var v) s' z)` by PROVE_TAC [] THEN 548 `EQC alpha (lam s w) (lam v (subst (var v) s w))` 549 by (Cases_on `s = v` THEN1 550 SRW_TAC [][renaming_sanity1] THEN 551 MATCH_MP_TAC EQC_R THEN REWRITE_TAC [alpha_def] THEN 552 Q.EXISTS_TAC `v` THEN 553 MATCH_MP_TAC (hd (CONJUNCTS ialpha_rules)) THEN 554 ASM_SIMP_TAC (srw_ss()) [] THEN 555 Q_TAC SUFF_TAC `~(v IN FV (collapse v'))` THEN1 556 PROVE_TAC [alpha_fv_invariant, FV_collapse] THEN 557 PROVE_TAC [LAM_INJ_ALPHA_FV]) THEN 558 `EQC alpha (lam s v') (lam s w)` by PROVE_TAC [EQC_alpha_CONG] THEN 559 `EQC alpha (lam v (subst (var v) s w)) (lam v a)` 560 by PROVE_TAC [EQC_alpha_CONG] THEN 561 `EQC alpha (lam s v') (lam v a)` by PROVE_TAC [EQC_TRANS] THEN 562 `beta (lam v a) (lam v b)` by PROVE_TAC [beta_rules] THEN 563 `EQC alpha (lam v b) (lam v (subst (var v) s' z))` 564 by PROVE_TAC [EQC_alpha_CONG] THEN 565 `EQC alpha (lam v (subst (var v) s' z)) (lam s' z)` 566 by (Cases_on `s' = v` THEN1 SRW_TAC [][renaming_sanity1] THEN 567 MATCH_MP_TAC EQC_SYM THEN 568 MATCH_MP_TAC EQC_R THEN REWRITE_TAC [alpha_def] THEN 569 Q.EXISTS_TAC `v` THEN 570 MATCH_MP_TAC (hd (CONJUNCTS ialpha_rules)) THEN 571 ASM_SIMP_TAC (srw_ss()) [] THEN 572 PROVE_TAC [LAM_INJ_ALPHA_FV, alpha_fv_invariant, FV_collapse]) THEN 573 `EQC alpha (lam s' z) (lam s' v'')` 574 by PROVE_TAC [EQC_alpha_CONG, EQC_SYM] THEN 575 PROVE_TAC [EQC_TRANS] 576 ]); 577 578val ccbeta_beta = store_thm( 579 "ccbeta_beta", 580 ``compat_closure beta (collapse t) (collapse u) ==> 581 (EQC alpha O beta O EQC alpha) t u``, 582 PROVE_TAC [SIMP_RULE (bool_ss ++ DNF_ss) [] ccbeta_beta_lemma]); 583 584val ccbeta_beta_EQ = store_thm( 585 "ccbeta_beta_EQ", 586 ``compat_closure beta (collapse t) (collapse u) = 587 (EQC alpha O beta O EQC alpha) t u``, 588 EQ_TAC THENL [ 589 PROVE_TAC [ccbeta_beta], 590 SRW_TAC [][O_DEF] THEN 591 PROVE_TAC [alpha_collapse, beta_ccbeta] 592 ]); 593 594(* ---------------------------------------------------------------------- 595 having established this much, confluence results about the 596 quotiented type can be transferred to the raw type, using the abstract 597 machinery from diagsTheory 598 ---------------------------------------------------------------------- *) 599 600open diagsTheory 601 602val onto_collapse = store_thm( 603 "onto_collapse", 604 ``onto collapse``, 605 SRW_TAC [][onto_def, collapse_ONTO]); 606 607val kSound_collapse = store_thm( 608 "kSound_collapse", 609 ``kSound alpha collapse``, 610 SIMP_TAC (srw_ss()) [kSound_def] THEN 611 METIS_TAC [EQC_alpha_collapse_EQ, EQC_R]); 612 613val kCompl_collapse = store_thm( 614 "kCompl_collapse", 615 ``kCompl alpha collapse``, 616 SRW_TAC [][kCompl_def] THEN 617 METIS_TAC [EQC_alpha_collapse_EQ, EQC_R]); 618 619val Pres_collapse = store_thm( 620 "Pres_collapse", 621 ``Pres collapse beta (compat_closure beta)``, 622 SRW_TAC [][O_DEF, ccbeta_beta_EQ, Pres_def] THEN 623 METIS_TAC [EQC_REFL]); 624 625val sRefl_collapse = store_thm( 626 "sRefl_collapse", 627 ``sRefl collapse beta (compat_closure beta)``, 628 SRW_TAC [][sRefl_def] THEN 629 `(?a1. b1 = collapse a1) /\ (?a2. b2 = collapse a2)` 630 by METIS_TAC [collapse_ONTO] THEN 631 FULL_SIMP_TAC (srw_ss()) [ccbeta_beta_EQ, O_DEF] THEN 632 METIS_TAC [alpha_collapse]); 633 634 635val ofree_alpha = store_thm( 636 "ofree_alpha", 637 ``ofree alpha``, 638 REWRITE_TAC [ofree_def] THEN 639 HO_MATCH_MP_TAC EQC_INDUCTION THEN REPEAT CONJ_TAC THENL [ 640 METIS_TAC [RTC_RULES], 641 METIS_TAC [RTC_RULES], 642 METIS_TAC [TC_RC_EQNS, alpha_sym, symmetric_RC, symmetric_TC, 643 symmetric_def], 644 METIS_TAC [RTC_RTC] 645 ]); 646 647val aRefl_eq_sRefl_lambda = prove( 648 ``aRefl collapse (RTC (beta RUNION alpha)) (RTC (compat_closure beta)) = 649 sRefl collapse (RTC (beta RUNION alpha)) (RTC (compat_closure beta))``, 650 METIS_TAC [onto_collapse, kCompl_collapse, ofree_alpha, note_lemma9]); 651 652val aRefl_collapse_RTC = prove( 653 ``aRefl collapse (RTC (beta RUNION alpha)) (RTC (compat_closure beta))``, 654 REWRITE_TAC [aRefl_eq_sRefl_lambda] THEN 655 METIS_TAC [note_prop10_1, sRefl_collapse, onto_collapse, kCompl_collapse, 656 ofree_alpha]); 657 658val Pres_collapse_RTC = store_thm( 659 "Pres_collapse_RTC", 660 ``Pres collapse (RTC (beta RUNION alpha)) (RTC (compat_closure beta))``, 661 SRW_TAC [][onto_collapse, Pres_structure_RTC, Pres_collapse, 662 kSound_collapse]); 663 664val collapse_preserves_diagrams = store_thm( 665 "collapse_preserves_diagrams", 666 ``!Fa G. eval Fa G (\i. RTC (beta RUNION alpha)) = 667 eval Fa G (\i. RTC (compat_closure beta))``, 668 MATCH_MP_TAC diagram_preservation THEN Q.EXISTS_TAC `collapse` THEN 669 SRW_TAC [][aRefl_collapse_RTC, Pres_collapse_RTC, onto_collapse]); 670 671val raw_diamond = store_thm( 672 "raw_diamond", 673 ``diamond (RTC (beta RUNION alpha))``, 674 SRW_TAC [][GSYM diamond_eval, collapse_preserves_diagrams] THEN 675 SRW_TAC [][diamond_eval] THEN 676 METIS_TAC [chap3Theory.beta_CR, chap3Theory.CR_def]); 677 678val _ = export_theory(); 679