1structure standardisationScript = 2struct 3 4 (* explicit structure above is necessary if MoscowML is to compile the 5 script file in its standard (not "toplevel") mode, and not be put off 6 by the structure Q = ... line below. 7 8 Poly/ML doesn't have this problem. *) 9 10open HolKernel Parse boolLib bossLib BasicProvers metisLib 11 12open boolSimps 13 14open nomsetTheory binderLib 15 16open pred_setTheory 17open finite_developmentsTheory 18open labelledTermsTheory 19open termTheory chap2Theory chap3Theory 20open term_posnsTheory 21open pathTheory 22open chap11_1Theory 23open head_reductionTheory 24 25local open containerTheory in end 26 27val _ = new_theory "standardisation" 28 29structure NewQ = Q 30structure Q = struct open Q open OldAbbrevTactics end 31 32val _ = set_fixity "=" (Infix(NONASSOC, 100)) 33 34 35val RUNION_def = relationTheory.RUNION 36val ADD1 = arithmeticTheory.ADD1 37 38 39 40fun Store_Thm(n,t,tac) = store_thm(n,t,tac) before export_rewrites [n] 41 42(* Section 11.4 of Barendregt *) 43 44val standard_reduction_def = Define` 45 standard_reduction s = 46 okpath (labelled_redn beta) s /\ 47 !i j. j < i /\ (i + 1) IN PL s ==> 48 !p. p < nth_label j s ==> 49 ~(nth_label i s IN residuals (seg j i s) {p}) 50`; 51 52val better_standard_reduction = store_thm( 53 "better_standard_reduction", 54 ``standard_reduction s = 55 okpath (labelled_redn beta) s /\ 56 !i j. j < i /\ i + 1 IN PL s ==> 57 !p. p IN redex_posns (el j s) /\ p < nth_label j s ==> 58 ~(nth_label i s IN residuals (seg j i s) {p})``, 59 SRW_TAC [][standard_reduction_def] THEN EQ_TAC THEN SRW_TAC [][] THEN 60 Cases_on `p IN redex_posns (el j s)` THENL [ 61 METIS_TAC [], 62 `i IN PL s` by METIS_TAC [PL_downward_closed, DECIDE ``i < i + 1``] THEN 63 `okpath (labelled_redn beta) (seg j i s)` 64 by SRW_TAC [numSimps.ARITH_ss][okpath_seg] THEN 65 `first (seg j i s) = el j s` by SRW_TAC [numSimps.ARITH_ss][first_seg] THEN 66 `{p} INTER redex_posns (el j s) = {}` by SRW_TAC [][EXTENSION] THEN 67 `finite (seg j i s)` by SRW_TAC [numSimps.ARITH_ss][] THEN 68 `residuals (seg j i s) {p} = {}` 69 by METIS_TAC [residuals_can_ignore, residuals_EMPTY] THEN 70 SRW_TAC [][] 71 ]); 72 73val _ = add_infix ("is_head_redex", 760, NONASSOC) 74 75val (is_head_redex_rules, is_head_redex_ind, is_head_redex_cases) = 76 IndDefLib.Hol_reln` 77 (!v (t:term) u. [] is_head_redex (LAM v t @@ u)) /\ 78 (!v t p. p is_head_redex t ==> (In::p) is_head_redex (LAM v t)) /\ 79 (!t u v p. p is_head_redex (t @@ u) ==> 80 (Lt::p) is_head_redex (t @@ u) @@ v) 81 `; 82 83val ihr_bvc_ind = store_thm( 84 "ihr_bvc_ind", 85 ``!P X. FINITE X /\ 86 (!v M N. ~(v IN X) /\ ~(v IN FV N) ==> P [] (LAM v M @@ N)) /\ 87 (!v M p. ~(v IN X) /\ P p M ==> P (In::p) (LAM v M)) /\ 88 (!M N L p. P p (M @@ N) ==> P (Lt::p) ((M @@ N) @@ L)) ==> 89 !p M. p is_head_redex M ==> P p M``, 90 REPEAT GEN_TAC THEN STRIP_TAC THEN 91 Q_TAC SUFF_TAC `!p M. p is_head_redex M ==> !pi. P p (tpm pi M)` 92 THEN1 METIS_TAC [pmact_nil] THEN 93 HO_MATCH_MP_TAC is_head_redex_ind THEN 94 SRW_TAC [][is_head_redex_rules] THENL [ 95 Q.MATCH_ABBREV_TAC `P [] (LAM vv MM @@ NN)` THEN 96 markerLib.RM_ALL_ABBREVS_TAC THEN 97 Q_TAC (NEW_TAC "z") `FV MM UNION FV NN UNION X` THEN 98 `LAM vv MM = LAM z (tpm [(z,vv)] MM)` by SRW_TAC [][tpm_ALPHA] THEN 99 SRW_TAC [][], 100 Q.MATCH_ABBREV_TAC `P (In::p) (LAM vv MM)` THEN 101 Q_TAC (NEW_TAC "z") `FV MM UNION X` THEN 102 `LAM vv MM = LAM z (tpm [(z,vv)] MM)` by SRW_TAC [][tpm_ALPHA] THEN 103 SRW_TAC [][GSYM pmact_decompose, Abbr`MM`] 104 ]); 105 106val is_head_redex_subst_invariant = store_thm( 107 "is_head_redex_subst_invariant", 108 ``!p t u v. p is_head_redex t ==> p is_head_redex [u/v] t``, 109 REPEAT GEN_TAC THEN MAP_EVERY Q.ID_SPEC_TAC [`t`, `p`] THEN 110 HO_MATCH_MP_TAC ihr_bvc_ind THEN Q.EXISTS_TAC `v INSERT FV u` THEN 111 SRW_TAC [][SUB_THM, SUB_VAR, is_head_redex_rules]); 112 113val is_head_redex_tpm_invariant = Store_Thm( 114 "is_head_redex_tpm_invariant", 115 ``p is_head_redex (tpm pi t) = p is_head_redex t``, 116 Q_TAC SUFF_TAC `!p t. p is_head_redex t ==> !pi. p is_head_redex (tpm pi t)` 117 THEN1 METIS_TAC [pmact_inverse] THEN 118 HO_MATCH_MP_TAC is_head_redex_ind THEN SRW_TAC [][is_head_redex_rules]); 119 120val is_head_redex_unique = store_thm( 121 "is_head_redex_unique", 122 ``!t p1 p2. p1 is_head_redex t /\ p2 is_head_redex t ==> (p1 = p2)``, 123 Q_TAC SUFF_TAC 124 `!p1 t. p1 is_head_redex t ==> !p2. p2 is_head_redex t ==> (p1 = p2)` 125 THEN1 PROVE_TAC [] THEN 126 HO_MATCH_MP_TAC is_head_redex_ind THEN REPEAT STRIP_TAC THEN 127 POP_ASSUM MP_TAC THEN ONCE_REWRITE_TAC [is_head_redex_cases] THEN 128 SRW_TAC [][LAM_eq_thm]); 129 130val is_head_redex_thm = store_thm( 131 "is_head_redex_thm", 132 ``(p is_head_redex (LAM v t) = ?p0. (p = In::p0) /\ p0 is_head_redex t) /\ 133 (p is_head_redex (t @@ u) = (p = []) /\ is_abs t \/ 134 ?p0. (p = Lt::p0) /\ is_comb t /\ 135 p0 is_head_redex t) /\ 136 (p is_head_redex (VAR v) = F)``, 137 REPEAT CONJ_TAC THEN 138 SRW_TAC [][Once is_head_redex_cases, SimpLHS, LAM_eq_thm] THEN 139 SRW_TAC [][EQ_IMP_THM] THENL [ 140 PROVE_TAC [], 141 PROVE_TAC [is_abs_thm, term_CASES], 142 METIS_TAC [is_comb_thm, term_CASES] 143 ]); 144 145val head_redex_leftmost = store_thm( 146 "head_redex_leftmost", 147 ``!p t. p is_head_redex t ==> 148 !p'. p' IN redex_posns t ==> (p = p') \/ p < p'``, 149 HO_MATCH_MP_TAC is_head_redex_ind THEN 150 SRW_TAC [][redex_posns_thm, DISJ_IMP_THM]); 151 152val hnf_no_head_redex = store_thm( 153 "hnf_no_head_redex", 154 ``!t. hnf t = !p. ~(p is_head_redex t)``, 155 HO_MATCH_MP_TAC simple_induction THEN 156 SRW_TAC [][hnf_thm, is_head_redex_thm] THEN 157 Q.SPEC_THEN `t` STRUCT_CASES_TAC term_CASES THEN 158 SRW_TAC [][is_head_redex_thm]); 159 160val head_redex_is_redex = store_thm( 161 "head_redex_is_redex", 162 ``!p t. p is_head_redex t ==> p IN redex_posns t``, 163 HO_MATCH_MP_TAC is_head_redex_ind THEN 164 SRW_TAC [][redex_posns_thm]); 165 166val is_head_redex_vsubst_invariant = store_thm( 167 "is_head_redex_vsubst_invariant", 168 ``!t v x p. p is_head_redex ([VAR v/x] t) = p is_head_redex t``, 169 REPEAT GEN_TAC THEN MAP_EVERY Q.ID_SPEC_TAC [`p`, `t`] THEN 170 HO_MATCH_MP_TAC nc_INDUCTION2 THEN Q.EXISTS_TAC `{x;v}` THEN 171 SRW_TAC [][is_head_redex_thm, SUB_THM, SUB_VAR]); 172 173val _ = add_infix("is_internal_redex", 760, NONASSOC) 174(* definition 11.4.2 (i) *) 175val is_internal_redex_def = Define` 176 p is_internal_redex t = ~(p is_head_redex t) /\ p IN redex_posns t 177`; 178 179val NIL_never_internal_redex = Store_Thm( 180 "NIL_never_internal_redex", 181 ``!t. ~([] is_internal_redex t)``, 182 GEN_TAC THEN 183 Q.SPEC_THEN `t` STRUCT_CASES_TAC term_CASES THEN 184 SRW_TAC [][is_internal_redex_def, is_head_redex_thm, redex_posns_thm]); 185 186val _ = add_infix("i_reduces", 760, NONASSOC) 187(* definition 11.4.2 (ii) *) 188val i_reduces_def = Define` 189 M i_reduces N = ?s. okpath (labelled_redn beta) s /\ (first s = M) /\ 190 finite s /\ (last s = N) /\ 191 !i. i + 1 IN PL s ==> 192 (nth_label i s) is_internal_redex (el i s) 193`; 194 195(* single step version of the same *) 196val _ = add_infix("i_reduce1", 760, NONASSOC) 197val i_reduce1_def = Define` 198 M i_reduce1 N = ?r. labelled_redn beta M r N /\ r is_internal_redex M 199`; 200 201val i_reduces_RTC_i_reduce1 = store_thm( 202 "i_reduces_RTC_i_reduce1", 203 ``(i_reduces) = RTC (i_reduce1)``, 204 SIMP_TAC (srw_ss()) [FUN_EQ_THM, EQ_IMP_THM, i_reduces_def, i_reduce1_def, 205 FORALL_AND_THM, GSYM LEFT_FORALL_IMP_THM] THEN 206 CONJ_TAC THENL [ 207 Q_TAC SUFF_TAC 208 `!s. okpath (labelled_redn beta) s /\ finite s ==> 209 (!i. i + 1 IN PL s ==> 210 nth_label i s is_internal_redex el i s) ==> 211 RTC (i_reduce1) (first s) (last s)` THEN1 PROVE_TAC [] THEN 212 HO_MATCH_MP_TAC pathTheory.finite_okpath_ind THEN 213 SIMP_TAC (srw_ss()) 214 [relationTheory.RTC_RULES, GSYM ADD1] THEN 215 MAP_EVERY Q.X_GEN_TAC [`x`,`r`,`p`] THEN REPEAT STRIP_TAC THEN 216 MATCH_MP_TAC (CONJUNCT2 (SPEC_ALL relationTheory.RTC_RULES)) THEN 217 Q.EXISTS_TAC `first p` THEN 218 POP_ASSUM (fn th => 219 MAP_EVERY (MP_TAC o GEN_ALL o C SPEC th) 220 [``0``, ``SUC i``]) THEN 221 SRW_TAC [][i_reduce1_def] THEN PROVE_TAC [], 222 223 HO_MATCH_MP_TAC relationTheory.RTC_INDUCT THEN 224 SRW_TAC [][i_reduce1_def] THENL [ 225 Q.EXISTS_TAC `stopped_at x` THEN SRW_TAC [][], 226 Q.EXISTS_TAC `pcons x r s` THEN 227 SRW_TAC [][GSYM ADD1] THEN 228 Cases_on `i` THEN SRW_TAC [][] THEN 229 FULL_SIMP_TAC (srw_ss()) [ADD1] 230 ] 231 ]); 232 233 234val _ = add_infix("i1_reduces", 760, NONASSOC) 235(* definition 11.4.3 (iii) *) 236val i1_reduces_def = Define` 237 M i1_reduces N = ?s. okpath (labelled_redn beta) s /\ (first s = M) /\ 238 finite s /\ (last s = N) /\ 239 (!i. i + 1 IN PL s ==> 240 (nth_label i s) is_internal_redex (el i s)) /\ 241 ?FS. s IN complete_development M FS 242`; 243 244val head_redex_preserved = store_thm( 245 "head_redex_preserved", 246 ``!M p N. 247 labelled_redn beta M p N ==> 248 !h. h is_head_redex M /\ ~(h = p) ==> h is_head_redex N``, 249 HO_MATCH_MP_TAC strong_labelled_redn_ind THEN 250 SRW_TAC [][is_head_redex_thm, beta_def] THENL [ 251 FULL_SIMP_TAC (srw_ss()) [is_head_redex_thm], 252 `?v t. M = LAM v t` by PROVE_TAC [is_abs_thm, term_CASES] THEN 253 FULL_SIMP_TAC (srw_ss()) [labelled_redn_lam], 254 `?f x. M = f @@ x` by PROVE_TAC [is_comb_APP_EXISTS] THEN 255 SRW_TAC [][] THEN 256 Q.PAT_X_ASSUM `labelled_redn beta _ _ _` MP_TAC THEN 257 ONCE_REWRITE_TAC [labelled_redn_cases] THEN 258 FULL_SIMP_TAC (srw_ss()) [is_head_redex_thm, beta_def] THEN 259 PROVE_TAC [is_comb_thm] 260 ]); 261 262val lemma11_4_3i = store_thm( 263 "lemma11_4_3i", 264 ``!M delta N. 265 labelled_redn beta M delta N /\ delta is_internal_redex M ==> 266 ((?p. p is_head_redex N) ==> (?p. p is_head_redex M))``, 267 METIS_TAC [labelled_redn_cc, hnf_no_head_redex, hnf_ccbeta_preserved]); 268 269val residual1_equal_singletons = store_thm( 270 "residual1_equal_singletons", 271 ``!M N pos. labelled_redn beta M pos N ==> (residual1 M pos N {pos} = {})``, 272 SRW_TAC [][residual1_def] THEN 273 Q.ABBREV_TAC `M' = nlabel 0 M {pos}` THEN 274 `lrcc (beta0 RUNION beta1) M' pos (lift_redn M' pos N) /\ 275 (N = strip_label (lift_redn M' pos N))` 276 by PROVE_TAC [strip_label_nlabel, lift_redn_def] THEN 277 Q.ABBREV_TAC `N' = lift_redn M' pos N` THEN 278 `pos IN redex_posns M` 279 by PROVE_TAC [IN_term_IN_redex_posns, is_redex_occurrence_def] THEN 280 `pos IN n_posns 0 M'` by SRW_TAC [][n_posns_nlabel] THEN 281 IMP_RES_TAC pick_a_beta THENL [ 282 PROVE_TAC [beta0_reduce_at_single_label], 283 PROVE_TAC [] 284 ]) 285 286val nlabel_eq = store_thm( 287 "nlabel_eq", 288 ``!t. ((VAR s = nlabel n t ps) = (t = VAR s)) /\ 289 ((M' @@ N' = nlabel n t ps) = 290 ?M N. (t = M @@ N) /\ (~is_abs M \/ ~([] IN ps)) /\ 291 (M' = nlabel n M { p | Lt::p IN ps}) /\ 292 (N' = nlabel n N { p | Rt::p IN ps})) /\ 293 ((LAM v M' = nlabel n t ps) = 294 ?M. (t = LAM v M) /\ (M' = nlabel n M {p| In::p IN ps})) /\ 295 ((LAMi m v M' N' = nlabel n t ps) = 296 ?M N. (t = LAM v M @@ N) /\ [] IN ps /\ (m = n) /\ 297 (M' = nlabel n M { p | Lt::In::p IN ps}) /\ 298 (N' = nlabel n N { p | Rt::p IN ps}))``, 299 GEN_TAC THEN 300 Q.SPEC_THEN `t` STRUCT_CASES_TAC term_CASES THEN 301 SRW_TAC [][nlabel_thm] THENL [ 302 PROVE_TAC [], 303 Q.SPEC_THEN `t1` STRUCT_CASES_TAC term_CASES THEN 304 SRW_TAC [][nlabel_thm], 305 Q.SPEC_THEN `t1` STRUCT_CASES_TAC term_CASES THEN 306 SRW_TAC [][nlabel_thm], 307 Q.SPEC_THEN `t1` STRUCT_CASES_TAC term_CASES THEN 308 SRW_TAC [][nlabel_thm], 309 Q.SPEC_THEN `t1` STRUCT_CASES_TAC term_CASES THEN 310 SRW_TAC [][nlabel_thm] THEN 311 SRW_TAC [][lLAMi_eq_thm, lLAM_eq_thm, EQ_IMP_THM, LAM_eq_thm] THENL [ 312 SRW_TAC [][tpm_eqr, nlabel_def, pmact_flip_args], 313 SRW_TAC [][nlabel_def, pmact_flip_args] 314 ], 315 SRW_TAC [][LAM_eq_thm, lLAM_eq_thm, EQ_IMP_THM] THENL [ 316 SRW_TAC [][tpm_eqr, nlabel_def, pmact_flip_args], 317 SRW_TAC [][nlabel_def, pmact_flip_args] 318 ] 319 ]); 320 321val IMAGE_EQ_SING = prove( 322 ``!f s x. (!x y. (f x = f y) = (x = y)) ==> 323 ((IMAGE f s = {f x}) = (s = {x}))``, 324 REPEAT STRIP_TAC THEN SRW_TAC [][EXTENSION, EQ_IMP_THM] THEN 325 PROVE_TAC []); 326 327val _ = augment_srw_ss [rewrites [IMAGE_EQ_SING]] 328 329 330 331val residual1_different_singletons = store_thm( 332 "residual1_different_singletons", 333 ``!M N p1 p2. 334 labelled_redn beta M p1 N /\ p2 IN redex_posns M /\ p2 < p1 ==> 335 (residual1 M p1 N {p2} = {p2})``, 336 SRW_TAC [][residual1_def] THEN 337 Q.ABBREV_TAC `M' = nlabel 0 M {p2}` THEN 338 Q.ABBREV_TAC `N' = lift_redn M' p1 N` THEN 339 `lrcc (beta0 RUNION beta1) M' p1 N' /\ (N = strip_label N')` by 340 METIS_TAC [lift_redn_def, strip_label_nlabel] THEN 341 Q_TAC SUFF_TAC 342 `!M' p1 N'. lrcc (beta0 RUNION beta1) M' p1 N' ==> 343 !p2 M. (M' = nlabel 0 M {p2}) /\ p2 < p1 /\ 344 p2 IN redex_posns M ==> 345 (n_posns 0 N' = {p2})` THEN1 METIS_TAC [] THEN 346 POP_ASSUM_LIST (K ALL_TAC) THEN 347 HO_MATCH_MP_TAC strong_lrcc_ind THEN 348 SRW_TAC [][n_posns_def, nlabel_eq] THENL [ 349 FULL_SIMP_TAC (srw_ss()) [n_posns_nlabel, redex_posns_thm] THEN 350 FULL_SIMP_TAC (srw_ss() ++ COND_elim_ss) [] THEN PROVE_TAC [], 351 352 FULL_SIMP_TAC (srw_ss()) [n_posns_nlabel, redex_posns_thm] THEN 353 FULL_SIMP_TAC (srw_ss() ++ COND_elim_ss) [] THEN 354 SRW_TAC [][] THEN TRY (RES_TAC THEN NO_TAC) THEN PROVE_TAC [], 355 356 FULL_SIMP_TAC (srw_ss()) [n_posns_nlabel, redex_posns_thm] THEN 357 FULL_SIMP_TAC (srw_ss() ++ COND_elim_ss) [] THENL [ 358 `n_posns 0 (nlabel 0 N {}) = {}` by SRW_TAC [][n_posns_nlabel] THEN 359 `n_posns 0 N' = {}` by PROVE_TAC [lrcc_new_labels] THEN 360 SRW_TAC [][EXTENSION], 361 PROVE_TAC [] 362 ], 363 364 FULL_SIMP_TAC (srw_ss()) [n_posns_nlabel, redex_posns_thm] THEN 365 FULL_SIMP_TAC (srw_ss() ++ COND_elim_ss) [] THEN 366 SRW_TAC [][] THEN TRY (RES_TAC THEN NO_TAC) THENL [ 367 `n_posns 0 (nlabel 0 N {}) = {}` by SRW_TAC [][n_posns_nlabel] THEN 368 `n_posns 0 N' = {}` by PROVE_TAC [lrcc_new_labels] THEN 369 SRW_TAC [][EXTENSION], 370 PROVE_TAC [] 371 ], 372 373 FULL_SIMP_TAC (srw_ss()) [n_posns_nlabel, redex_posns_thm] THEN 374 FULL_SIMP_TAC (srw_ss() ++ COND_elim_ss) [] THEN PROVE_TAC [], 375 376 FULL_SIMP_TAC (srw_ss()) [n_posns_nlabel, redex_posns_thm] THEN 377 `n_posns 0 (nlabel 0 N {}) = {}` by SRW_TAC [][n_posns_nlabel] THEN 378 `n_posns 0 N' = {}` by PROVE_TAC [lrcc_new_labels] THEN 379 SRW_TAC [][EXTENSION], 380 381 FULL_SIMP_TAC (srw_ss()) [n_posns_nlabel, redex_posns_thm] THEN 382 `n_posns 0 (nlabel 0 M'' {}) = {}` by SRW_TAC [][n_posns_nlabel] THEN 383 `n_posns 0 N' = {}` by PROVE_TAC [lrcc_new_labels] THEN 384 SRW_TAC [][EXTENSION] 385 ]); 386 387val lr_beta_preserves_lefter_redexes = store_thm( 388 "lr_beta_preserves_lefter_redexes", 389 ``!x y r r0. r0 IN redex_posns x /\ r0 < r /\ 390 labelled_redn beta x r y ==> (r0 IN redex_posns y)``, 391 REPEAT STRIP_TAC THEN 392 `residual1 x r y {r0} = {r0}` 393 by SRW_TAC [][residual1_different_singletons] THEN 394 `r0 IN redex_posns y` 395 by (Q_TAC SUFF_TAC `{r0} SUBSET redex_posns y` THEN1 396 SRW_TAC [][] THEN METIS_TAC [residual1_SUBSET])); 397 398val residuals_different_singletons = store_thm( 399 "residuals_different_singletons", 400 ``!p. okpath (labelled_redn beta) p /\ finite p ==> 401 !r. r IN redex_posns (first p) /\ 402 (!n. SUC n IN PL p ==> r < nth_label n p) ==> 403 (residuals p {r} = {r})``, 404 HO_MATCH_MP_TAC finite_okpath_ind THEN 405 SRW_TAC [][residuals_stopped_at, residuals_pcons] THENL [ 406 SRW_TAC [][EXTENSION] THEN METIS_TAC [], 407 FIRST_X_ASSUM 408 (fn th => Q.SPEC_THEN `0` MP_TAC th THEN 409 Q.SPEC_THEN `SUC n` (ASSUME_TAC o SIMP_RULE (srw_ss()) [] o 410 Q.GEN `n`) th) THEN 411 SRW_TAC [][residual1_different_singletons] THEN 412 METIS_TAC [lr_beta_preserves_lefter_redexes] 413 ]); 414 415val _ = set_trace "Unicode" 1 416val standard_coind = store_thm( 417 "standard_coind", 418 ``���Q. (���x r p. Q (pcons x r p) ��� 419 labelled_redn beta x r (first p) ��� 420 (���n r���. r��� ��� redex_posns x ��� r��� < r ��� n + 1 ��� PL p ��� 421 r��� < nth_label n p) ��� 422 Q p) 423 ��� 424 ���p. Q p ��� standard_reduction p``, 425 SRW_TAC [][] THEN 426 `okpath (labelled_redn beta) p` 427 by (Q.UNDISCH_THEN `Q p` MP_TAC THEN Q.ID_SPEC_TAC `p` THEN 428 HO_MATCH_MP_TAC okpath_co_ind THEN METIS_TAC []) THEN 429 SRW_TAC [][better_standard_reduction] THEN 430 `���n pth. Q pth ��� n ��� PL pth ��� Q (drop n pth)` 431 by (Induct THEN SRW_TAC [][] THEN 432 Q.ISPEC_THEN `pth` FULL_STRUCT_CASES_TAC path_cases THEN 433 FULL_SIMP_TAC (srw_ss()) [] THEN METIS_TAC []) THEN 434 `j < i + 1` by DECIDE_TAC THEN 435 `j ��� PL p` by METIS_TAC [PL_downward_closed] THEN 436 `okpath (labelled_redn beta) (drop j p)` 437 by METIS_TAC [okpath_drop] THEN 438 `Q (drop j p)` by METIS_TAC [] THEN 439 SRW_TAC [][seg_def] THEN 440 `el j p = first (drop j p)` by SRW_TAC [][first_drop] THEN 441 POP_ASSUM SUBST_ALL_TAC THEN 442 `nth_label j p = first_label (drop j p)` 443 by SRW_TAC [][first_label_drop] THEN 444 POP_ASSUM SUBST_ALL_TAC THEN 445 `nth_label i p = nth_label (i - j) (drop j p)` 446 by SRW_TAC [ARITH_ss] 447 [nth_label_drop, ADD1] THEN 448 POP_ASSUM SUBST_ALL_TAC THEN 449 NewQ.ABBREV_TAC `pp = drop j p` THEN 450 NewQ.ABBREV_TAC `ii = i - j` THEN 451 `ii + 1 ��� PL pp` by SRW_TAC [ARITH_ss][IN_PL_drop, Abbr`ii`, Abbr`pp`] THEN 452 `���n. n + 1 ��� PL pp ��� p' < nth_label n pp` 453 by (Q.ISPEC_THEN `pp` FULL_STRUCT_CASES_TAC path_cases THEN 454 FULL_SIMP_TAC (srw_ss()) [ADD1] THEN Cases THEN SRW_TAC [][] THEN 455 SRW_TAC [][] THEN METIS_TAC [ADD1]) THEN 456 `ii ��� PL pp` by METIS_TAC [PL_downward_closed, DECIDE ``x < x + 1``] THEN 457 `residuals (take ii pp) {p'} = {p'}` 458 by (MATCH_MP_TAC (SIMP_RULE (srw_ss() ++ DNF_ss) [AND_IMP_INTRO] 459 residuals_different_singletons) THEN 460 SRW_TAC [ARITH_ss][okpath_take,nth_label_take,ADD1] THEN 461 `n + 1 ��� PL pp` by METIS_TAC [PL_downward_closed, 462 arithmeticTheory.LESS_OR_EQ] THEN 463 SRW_TAC [][]) THEN 464 SRW_TAC [][] THEN 465 METIS_TAC [posn_lt_irrefl]); 466 467val cant_create_redexes_to_left1 = store_thm( 468 "cant_create_redexes_to_left1", 469 ``!x r y. labelled_redn beta x r y ==> 470 !r0 r1. r1 IN redex_posns x /\ r0 IN redex_posns y /\ 471 r1 < r /\ r0 < r1 ==> r0 IN redex_posns x``, 472 HO_MATCH_MP_TAC strong_labelled_redn_ind THEN 473 SRW_TAC [][redex_posns_thm] THEN 474 FULL_SIMP_TAC (srw_ss()) [posn_lt_def] THEN TRY (PROVE_TAC []) THEN 475 RULE_ASSUM_TAC (ONCE_REWRITE_RULE [labelled_redn_cases]) THEN 476 FULL_SIMP_TAC (srw_ss()) [] THEN REPEAT VAR_EQ_TAC THEN 477 FULL_SIMP_TAC (srw_ss()) [is_abs_thm, posn_lt_nil]); 478 479val cant_create_redexes_to_left = store_thm( 480 "cant_create_redexes_to_left", 481 ``!p. okpath (labelled_redn beta) p /\ finite p ==> 482 !r. r IN redex_posns (first p) /\ 483 (!n. SUC n IN PL p ==> r < nth_label n p) ==> 484 !r' M. labelled_redn beta (last p) r' M /\ r' < r ==> 485 r' IN redex_posns (first p)``, 486 HO_MATCH_MP_TAC finite_okpath_ind THEN SRW_TAC [][] THENL [ 487 METIS_TAC [labelled_redn_beta_redex_posn], 488 FIRST_X_ASSUM 489 (fn th => Q.SPEC_THEN `0` MP_TAC th THEN 490 Q.SPEC_THEN `SUC n` (ASSUME_TAC o SIMP_RULE (srw_ss()) [] o 491 Q.GEN `n`) th) THEN 492 SRW_TAC [][] THEN 493 `r' IN redex_posns (first p)` 494 by METIS_TAC [lr_beta_preserves_lefter_redexes] THEN 495 `r'' IN redex_posns (first p)` by METIS_TAC [] THEN 496 `r'' < r` by METIS_TAC [posn_lt_trans] THEN 497 METIS_TAC [cant_create_redexes_to_left1] 498 ]); 499 500val lemma11_4_3ii = store_thm( 501 "lemma11_4_3ii", 502 ``!M delta N. 503 labelled_redn beta M delta N /\ delta is_internal_redex M ==> 504 (!delta_h. delta_h is_head_redex M ==> 505 ?p. (residual1 M delta N {delta_h} = {p}) /\ 506 p is_head_redex N)``, 507 REPEAT STRIP_TAC THEN 508 `~(delta = delta_h) /\ delta IN redex_posns M` 509 by PROVE_TAC [is_internal_redex_def] THEN 510 `delta_h < delta` by PROVE_TAC [head_redex_leftmost] THEN 511 `delta_h IN redex_posns M` by PROVE_TAC [head_redex_is_redex] THEN 512 PROVE_TAC [residual1_different_singletons, head_redex_preserved]); 513 514val nil_posn_le = store_thm( 515 "nil_posn_le", 516 ``!p : posn. ([] = p) \/ [] < p``, 517 Induct THEN SRW_TAC [][]); 518 519val lrcc_new_labels' = prove( 520 ``~(lrcc (beta0 RUNION beta1) (nlabel 0 x {}) r y /\ p IN n_posns 0 y)``, 521 PROVE_TAC [NOT_IN_EMPTY, n_posns_nlabel, INTER_EMPTY, lrcc_new_labels]); 522 523val residuals_to_right_of_reduction = store_thm( 524 "residuals_to_right_of_reduction", 525 ``!M p1 N. labelled_redn beta M p1 N ==> 526 !p2. p2 IN redex_posns M /\ p1 < p2 ==> 527 !p. p IN residual1 M p1 N {p2} ==> (p1 = p) \/ (p1 < p)``, 528 SRW_TAC [][residual1_def] THEN 529 Q.ABBREV_TAC `M' = nlabel 0 M {p2}` THEN 530 Q.ABBREV_TAC `N' = lift_redn M' p1 N` THEN 531 `lrcc (beta0 RUNION beta1) M' p1 N' /\ (N = strip_label N')` 532 by METIS_TAC [lift_redn_def, strip_label_nlabel] THEN 533 Q_TAC SUFF_TAC 534 `!M' p1 N'. lrcc (beta0 RUNION beta1) M' p1 N' ==> 535 !p2 M. p1 < p2 /\ p2 IN redex_posns M /\ 536 (M' = nlabel 0 M {p2}) ==> 537 !p. p IN n_posns 0 N' ==> 538 (p1 = p) \/ p1 < p` THEN1 METIS_TAC [] THEN 539 POP_ASSUM_LIST (K ALL_TAC) THEN 540 HO_MATCH_MP_TAC strong_lrcc_ind THEN 541 SRW_TAC [][beta0_def, beta1_def, RUNION_def, nlabel_eq, n_posns_def, 542 n_posns_nlabel, nil_posn_le] THEN 543 FULL_SIMP_TAC (srw_ss()) [redex_posns_thm] THEN 544 FULL_SIMP_TAC (srw_ss() ++ COND_elim_ss) [] THENL [ 545 PROVE_TAC [], 546 PROVE_TAC [lrcc_new_labels'], 547 PROVE_TAC [], 548 PROVE_TAC [lrcc_new_labels'], 549 PROVE_TAC [], 550 FULL_SIMP_TAC (srw_ss()) [n_posns_nlabel] THEN SRW_TAC [][], 551 PROVE_TAC [], 552 FULL_SIMP_TAC (srw_ss()) [n_posns_nlabel] THEN SRW_TAC [][], 553 FULL_SIMP_TAC (srw_ss()) [n_posns_nlabel] THEN SRW_TAC [][], 554 PROVE_TAC [], 555 PROVE_TAC [], 556 PROVE_TAC [] 557 ]); 558 559 560val lemma11_4_3iii = store_thm( 561 "lemma11_4_3iii", 562 ``!M delta N. 563 labelled_redn beta M delta N /\ delta is_internal_redex M ==> 564 !delta_i. delta_i is_internal_redex M ==> 565 !p. p IN residual1 M delta N {delta_i} ==> 566 p is_internal_redex N``, 567 SRW_TAC [][] THEN 568 `delta IN valid_posns M /\ delta_i IN valid_posns M` 569 by PROVE_TAC [is_internal_redex_def, redex_posns_are_valid] THEN 570 Q.SPECL_THEN [`M`, `delta`, `delta_i`] 571 MP_TAC all_valid_posns_comparable THEN 572 SRW_TAC [][] THENL [ 573 `delta_i IN redex_posns M` by PROVE_TAC [is_internal_redex_def] THEN 574 `p IN redex_posns N` by PROVE_TAC [residual1_SUBSET, SUBSET_DEF] THEN 575 Cases_on `?h. h is_head_redex N` THENL [ 576 POP_ASSUM STRIP_ASSUME_TAC THEN 577 Q_TAC SUFF_TAC `~(p = h)` THEN1 578 METIS_TAC [is_internal_redex_def, is_head_redex_unique] THEN 579 DISCH_THEN ASSUME_TAC THEN 580 `delta IN redex_posns M` by PROVE_TAC [is_internal_redex_def] THEN 581 `(delta = p) \/ delta < p` 582 by PROVE_TAC [residuals_to_right_of_reduction] THEN 583 `?h0. h0 is_head_redex M` by PROVE_TAC [lemma11_4_3i] THEN 584 `~(h0 = delta)` by PROVE_TAC [is_internal_redex_def] THEN 585 `h0 = h` 586 by PROVE_TAC [head_redex_preserved, is_head_redex_unique] THEN 587 PROVE_TAC [head_redex_leftmost, posn_lt_antisym, posn_lt_irrefl], 588 PROVE_TAC [is_internal_redex_def] 589 ], 590 PROVE_TAC [residual1_equal_singletons, NOT_IN_EMPTY], 591 `p = delta_i` 592 by PROVE_TAC [residual1_different_singletons, NOT_IN_EMPTY, 593 IN_INSERT, is_internal_redex_def] THEN 594 SRW_TAC [][] THEN 595 `delta_i IN redex_posns N` 596 by PROVE_TAC [residual1_SUBSET, SUBSET_DEF] THEN 597 Cases_on `?h. h is_head_redex N` THENL [ 598 POP_ASSUM STRIP_ASSUME_TAC THEN 599 Q_TAC SUFF_TAC `~(delta_i = h)` THEN1 600 PROVE_TAC [is_internal_redex_def, is_head_redex_unique] THEN 601 DISCH_THEN SUBST_ALL_TAC THEN 602 `?h0. h0 is_head_redex M` by PROVE_TAC [lemma11_4_3i] THEN 603 `~(h0 = delta)` by PROVE_TAC [is_internal_redex_def] THEN 604 `h0 = h` by PROVE_TAC [head_redex_preserved, is_head_redex_unique] THEN 605 PROVE_TAC [is_internal_redex_def], 606 PROVE_TAC [is_internal_redex_def] 607 ] 608 ]); 609 610val is_head_reduction_def = Define` 611 is_head_reduction s = okpath (labelled_redn beta) s /\ 612 !i. i + 1 IN PL s ==> 613 nth_label i s is_head_redex el i s 614`; 615 616val is_head_reduction_thm = store_thm( 617 "is_head_reduction_thm", 618 ``(is_head_reduction (stopped_at x) = T) /\ 619 (is_head_reduction (pcons x r p) = 620 labelled_redn beta x r (first p) /\ r is_head_redex x /\ 621 is_head_reduction p)``, 622 SRW_TAC [][is_head_reduction_def, GSYM ADD1, 623 EQ_IMP_THM] 624 THENL [ 625 POP_ASSUM (Q.SPEC_THEN `0` MP_TAC) THEN SRW_TAC [][], 626 RES_TAC THEN FULL_SIMP_TAC (srw_ss()) [], 627 Cases_on `i` THEN SRW_TAC [][] 628 ]); 629val _ = export_rewrites ["is_head_reduction_thm"] 630 631 632val _ = add_infix ("head_reduces", 760, NONASSOC) 633val head_reduces_def = Define` 634 M head_reduces N = ?s. finite s /\ (first s = M) /\ (last s = N) /\ 635 is_head_reduction s 636`; 637 638 639val head_reduce1_def = store_thm( 640 "head_reduce1_def", 641 ``M -h-> N = (?r. r is_head_redex M /\ labelled_redn beta M r N)``, 642 EQ_TAC THENL [ 643 Q_TAC SUFF_TAC `!M N. M -h-> N ==> 644 ?r. r is_head_redex M /\ labelled_redn beta M r N` 645 THEN1 METIS_TAC [] THEN 646 HO_MATCH_MP_TAC hreduce1_ind THEN SRW_TAC [][] THENL [ 647 METIS_TAC [beta_def, is_head_redex_rules, labelled_redn_rules], 648 METIS_TAC [is_head_redex_rules, labelled_redn_rules], 649 Q.SPEC_THEN `M` FULL_STRUCT_CASES_TAC term_CASES THENL [ 650 FULL_SIMP_TAC (srw_ss()) [Once labelled_redn_cases, beta_def], 651 METIS_TAC [is_head_redex_rules, labelled_redn_rules], 652 FULL_SIMP_TAC (srw_ss()) [] 653 ] 654 ], 655 Q_TAC SUFF_TAC `!M r N. labelled_redn beta M r N ==> 656 r is_head_redex M ==> M -h-> N` 657 THEN1 METIS_TAC [] THEN 658 HO_MATCH_MP_TAC labelled_redn_ind THEN 659 SIMP_TAC (srw_ss() ++ DNF_ss) [beta_def, is_head_redex_thm, 660 Once is_comb_APP_EXISTS, hreduce1_rwts] 661 ]); 662 663val head_reduces_RTC_hreduce1 = store_thm( 664 "head_reduces_RTC_hreduce1", 665 ``(head_reduces) = RTC (-h->)``, 666 SIMP_TAC (srw_ss()) [head_reduces_def, FUN_EQ_THM, GSYM LEFT_FORALL_IMP_THM, 667 FORALL_AND_THM, EQ_IMP_THM] THEN 668 CONJ_TAC THENL [ 669 Q_TAC SUFF_TAC `!s. finite s ==> 670 is_head_reduction s ==> 671 RTC (-h->) (first s) (last s)` THEN1 672 PROVE_TAC [] THEN 673 HO_MATCH_MP_TAC pathTheory.finite_path_ind THEN 674 SIMP_TAC (srw_ss()) [relationTheory.RTC_RULES] THEN 675 MAP_EVERY Q.X_GEN_TAC [`x`,`r`,`p`] THEN REPEAT STRIP_TAC THEN 676 MATCH_MP_TAC (CONJUNCT2 (SPEC_ALL relationTheory.RTC_RULES)) THEN 677 Q.EXISTS_TAC `first p` THEN SRW_TAC [][head_reduce1_def] THEN 678 PROVE_TAC [], 679 HO_MATCH_MP_TAC relationTheory.RTC_INDUCT THEN 680 SRW_TAC [][head_reduce1_def] THENL [ 681 Q.EXISTS_TAC `stopped_at x` THEN SRW_TAC [][], 682 Q.EXISTS_TAC `pcons x r s` THEN SRW_TAC [][] 683 ] 684 ]); 685 686val head_reduces_reduction_beta = store_thm( 687 "head_reduces_reduction_beta", 688 ``!M N. M head_reduces N ==> reduction beta M N``, 689 SIMP_TAC (srw_ss()) [head_reduces_RTC_hreduce1] THEN 690 MATCH_MP_TAC relationTheory.RTC_MONOTONE THEN 691 METIS_TAC [head_reduce1_def, labelled_redn_cc]); 692 693val beta0_induction = 694 REWRITE_RULE [relationTheory.inv_DEF] 695 (MATCH_MP relationTheory.WF_INDUCTION_THM prop11_2_20) 696 697val last_strip_path_label = store_thm( 698 "last_strip_path_label", 699 ``!s. finite s ==> (last (strip_path_label s) = strip_label (last s))``, 700 HO_MATCH_MP_TAC pathTheory.finite_path_ind THEN 701 SRW_TAC [][strip_path_label_thm]); 702 703 704val okpath_monotone = prove( 705 ``!R1 R2 s. (!x r y. R1 x r y ==> R2 x r y) /\ okpath R1 s ==> 706 okpath R2 s``, 707 Q_TAC SUFF_TAC 708 `!R1 R2. (!x r y. R1 x r y ==> R2 x r y) ==> 709 !s. okpath R1 s ==> okpath R2 s` THEN1 PROVE_TAC [] THEN 710 REPEAT GEN_TAC THEN STRIP_TAC THEN 711 HO_MATCH_MP_TAC pathTheory.okpath_co_ind THEN SRW_TAC [][]); 712 713val lrcc_monotone = store_thm( 714 "lrcc_monotone", 715 ``!R1 R2 x r y. (!x y. R1 x y ==> R2 x y) /\ 716 lrcc R1 x r y ==> lrcc R2 x r y``, 717 Q_TAC SUFF_TAC 718 `!R1 R2. (!x y. R1 x y ==> R2 x y) ==> 719 !x r y. lrcc R1 x r y ==> lrcc R2 x r y` THEN1 720 PROVE_TAC [] THEN 721 REPEAT GEN_TAC THEN STRIP_TAC THEN 722 HO_MATCH_MP_TAC lrcc_ind THEN PROVE_TAC [lrcc_rules]); 723 724 725val length_lift_path = Store_Thm( 726 "length_lift_path", 727 ``!M p. length (lift_path M p) = length p``, 728 REPEAT GEN_TAC THEN 729 Cases_on `finite p` THENL [ 730 Q.ID_SPEC_TAC `M` THEN POP_ASSUM MP_TAC THEN 731 Q.ID_SPEC_TAC `p` THEN 732 HO_MATCH_MP_TAC pathTheory.finite_path_ind THEN 733 SRW_TAC [][lift_path_def, pathTheory.length_thm, finite_lift_path], 734 SRW_TAC [][pathTheory.length_def, finite_lift_path] 735 ]); 736 737val PL_lift_path = store_thm( 738 "PL_lift_path", 739 ``!p. PL (lift_path M p) = PL p``, 740 SRW_TAC [][pathTheory.PL_def, finite_lift_path]); 741val _ = export_rewrites ["PL_lift_path"] 742 743val n_posns_are_redex_posns = store_thm( 744 "n_posns_are_redex_posns", 745 ``!p n t. p IN n_posns n t ==> p IN redex_posns (strip_label t)``, 746 SRW_TAC [][] THEN 747 `?u. lrcc beta0 t p u` by PROVE_TAC [n_posns_beta0] THEN 748 `lrcc (beta0 RUNION beta1) t p u` by PROVE_TAC [pick_a_beta] THEN 749 `labelled_redn beta (strip_label t) p (strip_label u)` 750 by PROVE_TAC [lrcc_labelled_redn] THEN 751 PROVE_TAC [is_redex_occurrence_def, IN_term_IN_redex_posns]); 752 753val zero_def = Define` 754 zero n M = nlabel 0 (strip_label M) (n_posns n M) 755`; 756 757val zero_thm = store_thm( 758 "zero_thm", 759 ``(zero n (VAR s) = VAR s) /\ 760 (zero n (M @@ N) = zero n M @@ zero n N) /\ 761 (zero n (LAM v t) = LAM v (zero n t)) /\ 762 (zero n (LAMi m v t u) = 763 if m = n then LAMi 0 v (zero n t) (zero n u) 764 else LAM v (zero n t) @@ zero n u)``, 765 ASM_SIMP_TAC (srw_ss())[zero_def, nlabel_thm, n_posns_def, strip_label_thm, 766 nlabel_app_no_nil] THEN 767 Cases_on `n = m` THEN SRW_TAC [][]); 768 769val n_posns_zero = store_thm( 770 "n_posns_zero", 771 ``!M n. n_posns 0 (zero n M) = n_posns n M``, 772 HO_MATCH_MP_TAC simple_lterm_induction THEN 773 SRW_TAC [][n_posns_def, zero_thm] THEN 774 Cases_on `n = y` THEN SRW_TAC [][n_posns_def] THEN 775 SRW_TAC [][EXTENSION, EQ_IMP_THM]); 776 777val zero_vsubst = store_thm( 778 "zero_vsubst", 779 ``zero n ([VAR u/v] t) = [VAR u/v] (zero n t)``, 780 SRW_TAC [][zero_def, GSYM nlabel_vsubst_commutes, n_posns_vsubst_invariant, 781 strip_label_vsubst_commutes]); 782 783val FV_zero = Store_Thm( 784 "FV_zero", 785 ``FV (zero n t) = FV t``, 786 SRW_TAC [][zero_def, FV_nlabel, FV_strip_label]); 787 788val zero_subst = store_thm( 789 "zero_subst", 790 ``!t. zero n ([u/v] t) = [zero n u/v] (zero n t)``, 791 HO_MATCH_MP_TAC lterm_bvc_induction THEN 792 Q.EXISTS_TAC `v INSERT FV u` THEN SRW_TAC [][zero_thm, lSUB_VAR]); 793 794val lrcc_zero = store_thm( 795 "lrcc_zero", 796 ``!M r N. lrcc (beta0 RUNION beta1) M r N ==> 797 lrcc (beta0 RUNION beta1) (zero n M) r (zero n N)``, 798 HO_MATCH_MP_TAC lrcc_ind THEN 799 SRW_TAC [][zero_thm, RUNION_def, beta0_def, beta1_def] THENL [ 800 SRW_TAC [][zero_thm, zero_subst] THENL [ 801 PROVE_TAC [lrcc_rules, beta0_def, RUNION_def], 802 PROVE_TAC [lrcc_rules, beta1_def, RUNION_def] 803 ], 804 SRW_TAC [][zero_thm, zero_subst] THEN 805 PROVE_TAC [lrcc_rules, beta1_def, RUNION_def], 806 PROVE_TAC [lrcc_rules], 807 PROVE_TAC [lrcc_rules], 808 PROVE_TAC [lrcc_rules], 809 PROVE_TAC [lrcc_rules], 810 PROVE_TAC [lrcc_rules], 811 PROVE_TAC [lrcc_rules], 812 PROVE_TAC [lrcc_rules] 813 ]); 814 815val residuals_have_precursors0 = prove( 816 ``!M' r N'. 817 lrcc (beta0 RUNION beta1) M' r N' ==> 818 !p. p IN n_posns n N' ==> 819 p IN residual1 (strip_label M') r (strip_label N') (n_posns n M')``, 820 SRW_TAC [][residual1_def] THEN 821 `labelled_redn beta (strip_label M') r (strip_label N')` 822 by PROVE_TAC [lrcc_labelled_redn] THEN 823 Q.ABBREV_TAC `M = strip_label M'` THEN 824 Q.ABBREV_TAC `N = strip_label N'` THEN 825 Q.ABBREV_TAC `M'' = nlabel 0 M (n_posns n M')` THEN 826 Q.ABBREV_TAC `N'' = lift_redn M'' r N` THEN 827 `M = strip_label M''` by PROVE_TAC [strip_label_nlabel] THEN 828 `lrcc (beta0 RUNION beta1) M'' r N'' /\ (N = strip_label N'')` 829 by PROVE_TAC [lift_redn_def] THEN 830 `M'' = zero n M'` by PROVE_TAC [zero_def] THEN 831 `N'' = zero n N'` by PROVE_TAC [lrcc_det, lrcc_zero] THEN 832 SRW_TAC [][n_posns_zero]) 833 834val linear_set_fn_lemma = prove( 835 ``(!X Y. f (X UNION Y) = f X UNION f Y) /\ (f {} = {}) ==> 836 !X. FINITE X ==> 837 !x. x IN f X ==> ?y. y IN X /\ x IN f {y}``, 838 STRIP_TAC THEN 839 HO_MATCH_MP_TAC FINITE_INDUCT THEN 840 ONCE_REWRITE_TAC [INSERT_SING_UNION] THEN 841 SRW_TAC [][] THEN PROVE_TAC []); 842 843val residual1_empty = store_thm( 844 "residual1_empty", 845 ``labelled_redn beta M r N ==> (residual1 M r N {} = {})``, 846 STRIP_TAC THEN 847 Q.ABBREV_TAC `s = pcons M r (stopped_at N)` THEN 848 `okpath (labelled_redn beta) s` 849 by SRW_TAC [][pathTheory.okpath_thm] THEN 850 `residuals s {} = {}` by SRW_TAC [][residuals_EMPTY] THEN 851 POP_ASSUM MP_TAC THEN SRW_TAC [][residuals_pcons, residuals_stopped_at] THEN 852 PROVE_TAC [residual1_SUBSET, SUBSET_INTER_ABSORPTION]); 853 854val residuals_have_precursors = store_thm( 855 "residuals_have_precursors", 856 ``lrcc (beta0 RUNION beta1) M' r N' ==> 857 p IN n_posns n N' ==> 858 ?p0. p IN residual1 (strip_label M') r (strip_label N') {p0} /\ 859 p0 IN n_posns n M'``, 860 REPEAT STRIP_TAC THEN 861 `p IN residual1 (strip_label M') r (strip_label N') (n_posns n M')` 862 by PROVE_TAC [residuals_have_precursors0] THEN 863 `labelled_redn beta (strip_label M') r (strip_label N')` 864 by PROVE_TAC [lrcc_labelled_redn] THEN 865 MAP_EVERY IMP_RES_TAC [residual1_pointwise_union, residual1_empty] THEN 866 POP_ASSUM 867 (fn th2 => (POP_ASSUM 868 (fn th1 => ASSUME_TAC 869 (MATCH_MP linear_set_fn_lemma 870 (CONJ (CONV_RULE SWAP_VARS_CONV th1) 871 th2))))) THEN 872 `FINITE (n_posns n M')` by METIS_TAC [n_posns_are_redex_posns, 873 redex_posns_FINITE, SUBSET_DEF, 874 SUBSET_FINITE] THEN 875 METIS_TAC []); 876 877val lemma11_4_4 = store_thm( 878 "lemma11_4_4", 879 ``!M N. fd_grandbeta M N ==> ?M'. M head_reduces M' /\ M' i1_reduces N``, 880 SRW_TAC [][fd_grandbeta_def] THEN 881 `!M'. ?s. okpath (lrcc beta0) s /\ (first s = M') /\ finite s /\ 882 is_head_reduction (strip_path_label s) /\ 883 !p n. p IN n_posns n (last s) ==> 884 ~(p is_head_redex (strip_label (last s)))` 885 by (POP_ASSUM (K ALL_TAC) THEN 886 HO_MATCH_MP_TAC beta0_induction THEN 887 REPEAT STRIP_TAC THEN 888 Cases_on `?p n. p is_head_redex (strip_label M') /\ 889 p IN n_posns n M'` THENL [ 890 POP_ASSUM STRIP_ASSUME_TAC THEN 891 `p IN redex_posns (strip_label M')` 892 by PROVE_TAC [head_redex_is_redex] THEN 893 `?N. labelled_redn beta (strip_label M') p N` 894 by PROVE_TAC [IN_term_IN_redex_posns, 895 is_redex_occurrence_def] THEN 896 Q.ABBREV_TAC `N' = lift_redn M' p N` THEN 897 `lrcc (beta0 RUNION beta1) M' p N' /\ (N = strip_label N')` 898 by PROVE_TAC [lift_redn_def] THEN 899 `lrcc beta0 M' p N'` by PROVE_TAC [pick_a_beta] THEN 900 `lcompat_closure beta0 M' N'` by PROVE_TAC [lrcc_lcc] THEN 901 `?s0. okpath (lrcc beta0) s0 /\ (first s0 = N') /\ 902 finite s0 /\ is_head_reduction (strip_path_label s0) /\ 903 !p n. p IN n_posns n (last s0) ==> 904 ~(p is_head_redex strip_label (last s0))` 905 by METIS_TAC [] THEN 906 Q.EXISTS_TAC `pcons M' p s0` THEN 907 SRW_TAC [] [strip_path_label_thm, first_strip_path_label, 908 development_thm, strip_label_nlabel] THEN 909 PROVE_TAC [], 910 POP_ASSUM (STRIP_ASSUME_TAC o SIMP_RULE bool_ss []) THEN 911 Q.EXISTS_TAC `stopped_at M'` THEN 912 SRW_TAC [][strip_path_label_thm] THEN PROVE_TAC [] 913 ]) THEN 914 POP_ASSUM (Q.SPEC_THEN `nlabel 0 M FS` 915 (Q.X_CHOOSE_THEN `s'` STRIP_ASSUME_TAC)) THEN 916 Q.EXISTS_TAC `strip_label (last s')` THEN 917 Q.ABBREV_TAC `s = strip_path_label s'` THEN 918 ASM_SIMP_TAC (srw_ss()) [head_reduces_def] THEN CONJ_TAC THENL [ 919 Q.EXISTS_TAC `s` THEN 920 SRW_TAC [][finite_strip_path_label, first_strip_path_label, 921 strip_label_nlabel, last_strip_path_label], 922 ALL_TAC 923 ] THEN 924 `okpath (lrcc (beta0 RUNION beta1)) s'` 925 by (MATCH_MP_TAC okpath_monotone THEN 926 Q.EXISTS_TAC `lrcc beta0` THEN SRW_TAC [][] THEN 927 MATCH_MP_TAC lrcc_monotone THEN Q.EXISTS_TAC `beta0` THEN 928 SRW_TAC [][RUNION_def]) THEN 929 `lift_path (first s') (strip_path_label s') = s'` 930 by (MATCH_MP_TAC lift_path_strip_path_label THEN SRW_TAC [][]) THEN 931 `okpath (labelled_redn beta) s` 932 by PROVE_TAC [lemma11_2_1] THEN 933 `first s = M` by SRW_TAC [][first_strip_path_label, strip_label_nlabel] THEN 934 `s IN development M FS` by PROVE_TAC [lemma11_2_12] THEN 935 ASM_SIMP_TAC (srw_ss()) [i1_reduces_def] THEN 936 `finite s` by SRW_TAC [][finite_strip_path_label] THEN 937 `(last s' = nlabel 0 (last s) (residuals s FS)) /\ 938 residuals s FS SUBSET redex_posns (last s)` 939 by PROVE_TAC [residuals_def] THEN 940 `residuals s FS SUBSET (last s)` by PROVE_TAC [redex_occurrences_SUBSET] THEN 941 `n_posns 0 (nlabel 0 (last s) (residuals s FS)) = n_posns 0 (last s')` 942 by SRW_TAC [][] THEN 943 `residuals s FS = n_posns 0 (last s')` 944 by PROVE_TAC [n_posns_nlabel, SUBSET_INTER_ABSORPTION] THEN 945 `?s2. s2 IN complete_development (last s) (residuals s FS)` 946 by PROVE_TAC [complete_developments_always_exist] THEN 947 Q.EXISTS_TAC `s2` THEN 948 `s2 IN development (last s) (residuals s FS)` 949 by PROVE_TAC [complete_development_thm] THEN 950 `first s2 = strip_label (last s')` by 951 PROVE_TAC [last_strip_path_label, wf_development] THEN 952 `okpath (labelled_redn beta) s2` by PROVE_TAC [lemma11_2_12] THEN 953 `finite s2 /\ (residuals s2 (residuals s FS) = {})` 954 by PROVE_TAC [complete_development_thm] THEN 955 `plink s s2 IN development M FS` by PROVE_TAC [linking_developments] THEN 956 `last s = first s2` by PROVE_TAC [last_strip_path_label] THEN 957 `residuals (plink s s2) FS = {}` by METIS_TAC [lemma11_2_6] THEN 958 `finite (plink s s2)` by PROVE_TAC [pathTheory.finite_plink] THEN 959 `plink s s2 IN complete_development M FS` 960 by PROVE_TAC [complete_development_thm] THEN 961 `last (plink s s2) = Cpl(M, FS)` 962 by PROVE_TAC [Cpl_complete_development] THEN 963 `last s2 = Cpl(M, FS)` by PROVE_TAC [pathTheory.last_plink] THEN 964 REPEAT CONJ_TAC THEN TRY (FIRST_ASSUM ACCEPT_TAC) THENL [ 965 `okpath (lrcc beta0) (lift_path (last s') s2)` 966 by METIS_TAC [lemma11_2_12] THEN 967 Q.PAT_X_ASSUM `last u = nlabel x y z` (K ALL_TAC) THEN 968 Q_TAC SUFF_TAC 969 `!s. okpath (lrcc beta0) s /\ finite s ==> 970 (!p n. p IN n_posns n (first s) ==> 971 ~(p is_head_redex strip_label (first s))) ==> 972 !i. i + 1 IN PL s ==> 973 nth_label i (strip_path_label s) is_internal_redex 974 el i (strip_path_label s)` THEN1 975 (DISCH_THEN (Q.SPEC_THEN `lift_path (last s') s2` MP_TAC) THEN 976 ASM_SIMP_TAC (srw_ss()) 977 [finite_lift_path, first_lift_path, 978 strip_path_label_lift_path] THEN 979 DISCH_THEN MATCH_MP_TAC THEN FIRST_ASSUM ACCEPT_TAC) THEN 980 POP_ASSUM_LIST (K ALL_TAC) THEN 981 HO_MATCH_MP_TAC pathTheory.finite_okpath_ind THEN 982 SIMP_TAC (srw_ss())[pathTheory.okpath_thm, strip_path_label_thm, 983 GSYM ADD1] THEN 984 MAP_EVERY Q.X_GEN_TAC [`x`,`r`,`p`] THEN REPEAT STRIP_TAC THEN 985 `?m. r IN n_posns m x` by PROVE_TAC [beta0_n_posns] THEN 986 `r IN redex_posns (strip_label x)` 987 by PROVE_TAC [n_posns_are_redex_posns] THEN 988 `r is_internal_redex (strip_label x)` 989 by (SRW_TAC [][is_internal_redex_def] THEN PROVE_TAC []) THEN 990 Cases_on `i` THEN SRW_TAC [][] THEN 991 Q_TAC SUFF_TAC `!p' n. p' IN n_posns n (first p) ==> 992 ~(p' is_head_redex strip_label (first p))` THEN1 993 PROVE_TAC [] THEN 994 REPEAT STRIP_TAC THEN 995 `labelled_redn beta (strip_label x) r (strip_label (first p))` 996 by PROVE_TAC [pick_a_beta, lrcc_labelled_redn] THEN 997 `lrcc (beta0 RUNION beta1) x r (first p)` 998 by PROVE_TAC [pick_a_beta] THEN 999 `?p0. p' IN residual1 (strip_label x) r (strip_label (first p)) {p0} /\ 1000 p0 IN n_posns n' x` 1001 by PROVE_TAC [residuals_have_precursors] THEN 1002 `p0 is_internal_redex strip_label x` 1003 by PROVE_TAC [is_internal_redex_def, n_posns_are_redex_posns] THEN 1004 `p' is_internal_redex strip_label (first p)` 1005 by PROVE_TAC [lemma11_4_3iii] THEN 1006 PROVE_TAC [is_internal_redex_def], 1007 1008 PROVE_TAC [] 1009 ]); 1010 1011val i_reduce1_i1_reduces = prove( 1012 ``M i_reduce1 N ==> M i1_reduces N``, 1013 SRW_TAC [][i_reduce1_def, i1_reduces_def] THEN 1014 Q.EXISTS_TAC `pcons M r (stopped_at N)` THEN 1015 SRW_TAC [][complete_development_thm, development_thm, residuals_pcons, 1016 residuals_stopped_at, redex_occurrences_SUBSET, 1017 residual1_SUBSET] THEN 1018 Q.EXISTS_TAC `{r}` THEN 1019 SRW_TAC [][residual1_equal_singletons, SUBSET_DEF] THEN 1020 PROVE_TAC [is_redex_occurrence_def, IN_term_IN_redex_posns]); 1021 1022val i1_reduces_i_reduces = prove( 1023 ``M i1_reduces N ==> M i_reduces N``, 1024 SRW_TAC [][i1_reduces_def, i_reduces_def] THEN PROVE_TAC []); 1025 1026val i_reduces_RTC_i_reduce1 = store_thm( 1027 "i_reduces_RTC_i_reduce1", 1028 ``(i_reduces) = RTC (i_reduce1)``, 1029 SIMP_TAC (srw_ss()) [FORALL_AND_THM, GSYM LEFT_FORALL_IMP_THM, 1030 FUN_EQ_THM, i_reduces_def, EQ_IMP_THM] THEN 1031 CONJ_TAC THENL [ 1032 Q_TAC SUFF_TAC 1033 `!s. okpath (labelled_redn beta) s /\ finite s ==> 1034 (!i. i + 1 IN PL s ==> nth_label i s is_internal_redex el i s) ==> 1035 RTC (i_reduce1) (first s) (last s)` THEN1 PROVE_TAC [] THEN 1036 HO_MATCH_MP_TAC pathTheory.finite_okpath_ind THEN 1037 SRW_TAC [][GSYM ADD1, relationTheory.RTC_RULES] THEN 1038 MATCH_MP_TAC (CONJUNCT2 (SPEC_ALL relationTheory.RTC_RULES)) THEN 1039 POP_ASSUM (fn th => 1040 MAP_EVERY (MP_TAC o GEN_ALL o C SPEC th) 1041 [``0``,``SUC i``]) THEN 1042 SRW_TAC [][i_reduce1_def] THEN PROVE_TAC [], 1043 HO_MATCH_MP_TAC relationTheory.RTC_INDUCT THEN 1044 SRW_TAC [][i_reduce1_def, GSYM ADD1] THENL [ 1045 Q.EXISTS_TAC `stopped_at x` THEN SRW_TAC [][], 1046 Q.EXISTS_TAC `pcons x r s` THEN 1047 SRW_TAC [][] THEN Cases_on `i` THEN SRW_TAC [][] 1048 ] 1049 ]); 1050 1051 1052val _ = augment_srw_ss [rewrites [REWRITE_CONV [EMPTY_SUBSET, 1053 redex_occurrences_SUBSET] 1054 ``{} SUBSET (M:term)``]] 1055 1056val head_reduces_TRANS = store_thm( 1057 "head_reduces_TRANS", 1058 ``!M N P. M head_reduces N /\ N head_reduces P ==> M head_reduces P``, 1059 METIS_TAC [relationTheory.RTC_RTC, head_reduces_RTC_hreduce1]); 1060 1061val lemma11_4_5 = store_thm( 1062 "lemma11_4_5", 1063 ``!M M' N'. M i_reduce1 M' /\ M' head_reduces N' ==> 1064 ?N. M head_reduces N /\ N i_reduces N'``, 1065 Q_TAC SUFF_TAC 1066 `!M M' N'. M i1_reduces M' /\ M' -h-> N' ==> 1067 ?N. M head_reduces N /\ N i1_reduces N'` THEN1 1068 (STRIP_TAC THEN 1069 Q_TAC SUFF_TAC 1070 `!M' N'. M' -h->* N' ==> 1071 !M. M i1_reduces M' ==> 1072 ?N. M head_reduces N /\ N i1_reduces N'` 1073 THEN1 METIS_TAC [head_reduces_RTC_hreduce1, 1074 i_reduce1_i1_reduces, i1_reduces_i_reduces] THEN 1075 HO_MATCH_MP_TAC relationTheory.RTC_INDUCT THEN CONJ_TAC THENL [ 1076 MAP_EVERY Q.X_GEN_TAC [`M'`,`M`] THEN STRIP_TAC THEN 1077 Q.EXISTS_TAC `M` THEN 1078 SRW_TAC [][relationTheory.RTC_RULES, head_reduces_RTC_hreduce1], 1079 METIS_TAC [head_reduces_TRANS] 1080 ]) THEN 1081 SIMP_TAC (srw_ss()) [SimpL ``(==>)``, i1_reduces_def, head_reduce1_def] THEN 1082 REPEAT STRIP_TAC THEN 1083 `?r0. r0 is_head_redex M` 1084 by (Q_TAC SUFF_TAC 1085 `!s. okpath (labelled_redn beta) s /\ finite s ==> 1086 (!i. i + 1 IN PL s ==> 1087 nth_label i s is_internal_redex el i s) ==> 1088 !r. r is_head_redex (last s) ==> 1089 ?r0. r0 is_head_redex (first s)` 1090 THEN1 PROVE_TAC [] THEN 1091 POP_ASSUM_LIST (K ALL_TAC) THEN 1092 HO_MATCH_MP_TAC pathTheory.finite_okpath_ind THEN 1093 SRW_TAC [][GSYM ADD1] THENL [ 1094 PROVE_TAC [], 1095 FIRST_X_ASSUM (fn th => 1096 MAP_EVERY (MP_TAC o GEN_ALL o C SPEC th) 1097 [``0``, ``SUC i``]) THEN 1098 SRW_TAC [][] THEN PROVE_TAC [lemma11_4_3i] 1099 ]) THEN 1100 `(residuals s (FS UNION {r0}) = {r}) /\ (r0 = r)` 1101 by (`residuals s FS = {}` by PROVE_TAC [complete_development_thm] THEN 1102 ASM_SIMP_TAC (srw_ss()) [residuals_pointwise_union] THEN 1103 Q_TAC SUFF_TAC 1104 `!s. okpath (labelled_redn beta) s /\ finite s ==> 1105 (!i. i + 1 IN PL s ==> 1106 nth_label i s is_internal_redex el i s) ==> 1107 !r r0. 1108 r0 is_head_redex (first s) /\ 1109 r is_head_redex (last s) ==> 1110 (residuals s {r0} = {r}) /\ (r0 = r)` 1111 THEN1 METIS_TAC [] THEN 1112 POP_ASSUM_LIST (K ALL_TAC) THEN 1113 HO_MATCH_MP_TAC pathTheory.finite_okpath_ind THEN 1114 ASM_SIMP_TAC (srw_ss()) 1115 [GSYM ADD1, residuals_pcons, 1116 residuals_stopped_at] THEN CONJ_TAC 1117 THENL [ 1118 REPEAT STRIP_TAC THEN 1119 `r0 = r` by PROVE_TAC [is_head_redex_unique] THEN 1120 SRW_TAC [][GSYM SUBSET_INTER_ABSORPTION, head_redex_is_redex], 1121 MAP_EVERY Q.X_GEN_TAC [`x`,`r`,`p`] THEN STRIP_TAC THEN 1122 DISCH_THEN (fn th => 1123 MAP_EVERY (MP_TAC o GEN_ALL o C SPEC th) 1124 [``0``, ``SUC i``]) THEN 1125 ASM_SIMP_TAC (srw_ss()) [] THEN NTAC 2 STRIP_TAC THEN 1126 REPEAT GEN_TAC THEN STRIP_TAC THEN 1127 `?hr. (residual1 x r (first p) {r0} = {hr})/\ 1128 hr is_head_redex (first p)` by PROVE_TAC [lemma11_4_3ii] THEN 1129 `r0 is_head_redex (first p)` 1130 by PROVE_TAC [is_internal_redex_def, 1131 head_redex_preserved] THEN 1132 `r0 = hr` by PROVE_TAC [is_head_redex_unique] THEN 1133 ASM_SIMP_TAC (srw_ss()) [] 1134 ]) THEN 1135 VAR_EQ_TAC THEN 1136 `FS SUBSET M` by PROVE_TAC [complete_development_thm, wf_development] THEN 1137 `{r} SUBSET M /\ {r} SUBSET M'` 1138 by SRW_TAC [][redexes_all_occur_def, IN_term_IN_redex_posns, 1139 head_redex_is_redex] THEN 1140 `FS UNION {r} SUBSET M` 1141 by PROVE_TAC [redex_occurrences_SUBSET, UNION_SUBSET] THEN 1142 `plink s (pcons M' r (stopped_at N')) IN 1143 complete_development M (FS UNION {r})` 1144 by (ASM_SIMP_TAC (srw_ss()) [complete_development_thm, 1145 lemma11_2_6, residuals_pcons, 1146 residuals_stopped_at, 1147 residual1_equal_singletons] THEN 1148 MATCH_MP_TAC linking_developments THEN 1149 SRW_TAC [][development_thm, residual1_equal_singletons] THEN 1150 MATCH_MP_TAC development_SUBSET THEN 1151 Q.EXISTS_TAC `FS` THEN 1152 FULL_SIMP_TAC (srw_ss()) [complete_development_thm]) THEN 1153 `?M1. labelled_redn beta M r M1` 1154 by PROVE_TAC [is_redex_occurrence_def, head_redex_is_redex, 1155 IN_term_IN_redex_posns] THEN 1156 Q.ABBREV_TAC `FS' = residual1 M r M1 FS` THEN 1157 `?s'. s' IN complete_development M1 FS'` 1158 by PROVE_TAC [complete_developments_always_exist, 1159 residual1_SUBSET, redex_occurrences_SUBSET] THEN 1160 `finite s'` by PROVE_TAC [complete_development_thm, FD] THEN 1161 `first s' = M1` by PROVE_TAC [complete_development_thm, wf_development] THEN 1162 `okpath (labelled_redn beta) s' /\ s' IN development (first s') FS' /\ 1163 (residuals s' FS' = {})` 1164 by PROVE_TAC [complete_development_thm, lemma11_2_12] THEN 1165 `pcons M r s' IN complete_development M (FS UNION {r})` 1166 by (SRW_TAC [][complete_development_thm, development_thm, 1167 residual1_pointwise_union, residual1_equal_singletons, 1168 residuals_pcons]) THEN 1169 `last s' = N'` 1170 by (`last (pcons M r s') = last (plink s (pcons M' r (stopped_at N')))` 1171 by PROVE_TAC [FDbang] THEN 1172 POP_ASSUM MP_TAC THEN SRW_TAC [][]) THEN 1173 `FS' SUBSET M1` by PROVE_TAC [complete_development_thm, wf_development] THEN 1174 `fd_grandbeta M1 N'` by PROVE_TAC [fd_grandbeta_def, 1175 Cpl_complete_development] THEN 1176 `?P. M1 head_reduces P /\ P i1_reduces N'` by PROVE_TAC [lemma11_4_4] THEN 1177 Q.EXISTS_TAC `P` THEN SRW_TAC [][] THEN 1178 METIS_TAC [head_reduces_RTC_hreduce1, head_reduce1_def, 1179 relationTheory.RTC_RULES]); 1180 1181val lemma11_4_6 = store_thm( 1182 "lemma11_4_6", 1183 ``!M N. reduction beta M N ==> 1184 ?M'. M head_reduces M' /\ M' i_reduces N``, 1185 SIMP_TAC (srw_ss()) [] THEN 1186 HO_MATCH_MP_TAC relationTheory.RTC_INDUCT THEN CONJ_TAC THENL [ 1187 PROVE_TAC [head_reduces_RTC_hreduce1, i_reduces_RTC_i_reduce1, 1188 relationTheory.RTC_RULES], 1189 MAP_EVERY Q.X_GEN_TAC [`M`,`N`,`P`] THEN 1190 SIMP_TAC (srw_ss()) [GSYM LEFT_FORALL_IMP_THM, 1191 GSYM RIGHT_EXISTS_AND_THM] THEN 1192 Q.X_GEN_TAC `M'` THEN STRIP_TAC THEN 1193 `?r. labelled_redn beta M r N` by PROVE_TAC [cc_labelled_redn] THEN 1194 `r IN redex_posns M` by PROVE_TAC [is_redex_occurrence_def, 1195 IN_term_IN_redex_posns] THEN 1196 Cases_on `r is_head_redex M` THENL [ 1197 Q.EXISTS_TAC `M'` THEN SRW_TAC [][] THEN 1198 METIS_TAC [relationTheory.RTC_RULES, head_reduces_RTC_hreduce1, 1199 head_reduce1_def], 1200 `r is_internal_redex M` by PROVE_TAC [is_internal_redex_def] THEN 1201 `M i_reduce1 N` by PROVE_TAC [i_reduce1_def] THEN 1202 `?Q. M head_reduces Q /\ Q i_reduces M'` by PROVE_TAC [lemma11_4_5] THEN 1203 Q.EXISTS_TAC `Q` THEN SRW_TAC [][] THEN 1204 METIS_TAC [relationTheory.RTC_RTC, i_reduces_RTC_i_reduce1] 1205 ] 1206 ]); 1207 1208val foldl_snoc = prove( 1209 ``!l f x y. FOLDL f x (APPEND l [y]) = f (FOLDL f x l) y``, 1210 Induct THEN SRW_TAC [][]); 1211 1212val size_nonzero = prove(``!t:term. 0 < size t``, 1213 HO_MATCH_MP_TAC simple_induction THEN 1214 SRW_TAC [ARITH_ss][]) 1215 1216val size_nz = 1217 REWRITE_RULE [GSYM arithmeticTheory.NOT_ZERO_LT_ZERO] size_nonzero 1218 1219val combs_not_size_1 = prove( 1220 ``(size M = 1) ==> ~is_comb M``, 1221 Q.SPEC_THEN `M` STRUCT_CASES_TAC term_CASES THEN 1222 SRW_TAC [][size_thm, size_nz]); 1223 1224val cant_ireduce_to_atom = prove( 1225 ``!M N. (size N = 1) ==> ~(M i_reduce1 N)``, 1226 Q_TAC SUFF_TAC `!M r N. labelled_redn beta M r N ==> 1227 (size N = 1) ==> ~(r is_internal_redex M)` 1228 THEN1 PROVE_TAC [i_reduce1_def] THEN 1229 HO_MATCH_MP_TAC labelled_redn_ind THEN 1230 SRW_TAC [] [is_internal_redex_def, redex_posns_thm, size_thm, size_nz, 1231 beta_def] THEN 1232 SRW_TAC [][redex_posns_thm, is_head_redex_thm]); 1233 1234val i_reduce_to_LAM_underneath = prove( 1235 ``!M N v. ~(v IN FV M) ==> 1236 (M i_reduce1 (LAM v N) = ?M0. (M = LAM v M0) /\ M0 i_reduce1 N)``, 1237 SRW_TAC [][i_reduce1_def, EQ_IMP_THM, is_internal_redex_def, 1238 redex_posns_thm, is_head_redex_thm] 1239 THENL [ 1240 Cases_on `r` THENL [ 1241 Q.SPEC_THEN `M` (REPEAT_TCL STRIP_THM_THEN SUBST_ALL_TAC) term_CASES THEN 1242 FULL_SIMP_TAC (srw_ss() ++ COND_elim_ss) 1243 [redex_posns_thm, is_head_redex_thm], 1244 RULE_ASSUM_TAC (ONCE_REWRITE_RULE [labelled_redn_cases]) THEN 1245 FULL_SIMP_TAC (srw_ss()) [LAM_eq_thm] THEN SRW_TAC [][] THEN 1246 FULL_SIMP_TAC (srw_ss()) [redex_posns_thm, is_head_redex_thm] THENL [ 1247 PROVE_TAC [], 1248 SRW_TAC [][tpm_eqr, labelled_redn_beta_tpm_eqn, pmact_flip_args] THEN 1249 PROVE_TAC [] 1250 ] 1251 ], 1252 Q.EXISTS_TAC `In :: r` THEN 1253 ASM_SIMP_TAC (srw_ss()) [is_head_redex_thm, redex_posns_thm] THEN 1254 PROVE_TAC [labelled_redn_rules] 1255 ]); 1256 1257val LAMl_def = Define` 1258 LAMl vs (t : term) = FOLDR LAM t vs 1259`; 1260 1261val LAMl_thm = Store_Thm( 1262 "LAMl_thm", 1263 ``(LAMl [] M = M) /\ 1264 (LAMl (h::t) M = LAM h (LAMl t M))``, 1265 SRW_TAC [][LAMl_def]); 1266 1267val LAMl_11 = Store_Thm( 1268 "LAMl_11", 1269 ``!vs. (LAMl vs x = LAMl vs y) = (x = y)``, 1270 Induct THEN SRW_TAC [][]); 1271 1272val size_LAMl = Store_Thm( 1273 "size_LAMl", 1274 ``!vs. size (LAMl vs M) = LENGTH vs + size M``, 1275 Induct THEN SRW_TAC [numSimps.ARITH_ss][size_thm]); 1276 1277val LAMl_vsub = store_thm( 1278 "LAMl_vsub", 1279 ``!vs u v M. 1280 ~MEM u vs /\ ~MEM v vs ==> 1281 ([VAR v/u] (LAMl vs M) = LAMl vs ([VAR v/u] M))``, 1282 Induct THEN SRW_TAC [][] THEN 1283 Q_TAC (NEW_TAC "z") `LIST_TO_SET vs UNION {h;v;u} UNION FV (LAMl vs M) UNION 1284 FV (LAMl vs ([VAR v/u] M))` THEN 1285 `LAM h (LAMl vs M) = LAM z ([VAR z/h] (LAMl vs M))` 1286 by SRW_TAC [][SIMPLE_ALPHA] THEN 1287 `LAM h (LAMl vs ([VAR v/u] M)) = LAM z ([VAR z/h] (LAMl vs ([VAR v/u] M)))` 1288 by SRW_TAC [][SIMPLE_ALPHA] THEN 1289 SRW_TAC [][SUB_THM]); 1290 1291val FV_LAMl = store_thm( 1292 "FV_LAMl", 1293 ``!vs M. FV (LAMl vs M) = FV M DIFF LIST_TO_SET vs``, 1294 Induct THEN SRW_TAC [][] THEN 1295 SIMP_TAC (srw_ss()) [EXTENSION] THEN PROVE_TAC []); 1296 1297val LAMl_vsub_disappears = store_thm( 1298 "LAMl_vsub_disappears", 1299 ``!vs u v M. MEM u vs ==> ([VAR v/u] (LAMl vs M) = LAMl vs M)``, 1300 Induct THEN SRW_TAC [][] THENL [ 1301 SRW_TAC [][SUB_THM, lemma14b], 1302 `~(u IN FV (LAMl vs M))` by SRW_TAC [][FV_LAMl] THEN 1303 `LAM h (LAMl vs M) = LAM u ([VAR u/h] (LAMl vs M))` 1304 by SRW_TAC [][SIMPLE_ALPHA] THEN 1305 SRW_TAC [][SUB_THM, lemma14b] 1306 ]); 1307 1308val SUB_ISUB_SINGLETON = store_thm( 1309 "SUB_ISUB_SINGLETON", 1310 ``!t x u. [t/x]u:term = u ISUB [(t,x)]``, 1311 SRW_TAC [][ISUB_def]); 1312 1313val ISUB_APPEND = store_thm( 1314 "ISUB_APPEND", 1315 ``!R1 R2 t:term. (t ISUB R1) ISUB R2 = t ISUB (APPEND R1 R2)``, 1316 Induct THEN 1317 ASM_SIMP_TAC (srw_ss()) [pairTheory.FORALL_PROD, ISUB_def]); 1318 1319val LAMl_ALPHA = store_thm( 1320 "LAMl_ALPHA", 1321 ``!vs vs' M. 1322 (LENGTH vs = LENGTH vs') /\ ALL_DISTINCT vs' /\ 1323 DISJOINT (LIST_TO_SET vs') (LIST_TO_SET vs UNION FV M) ==> 1324 (LAMl vs M = LAMl vs' (M ISUB REVERSE (ZIP(MAP VAR vs', vs))))``, 1325 Induct THENL [ 1326 SRW_TAC [][] THEN 1327 FULL_SIMP_TAC (srw_ss()) [ISUB_def], 1328 SRW_TAC [][] THEN 1329 Cases_on `vs'` THEN 1330 FULL_SIMP_TAC (srw_ss()) [DISJ_IMP_THM, FORALL_AND_THM] THEN 1331 `~(h' IN LIST_TO_SET vs) /\ ~(h' IN FV M) /\ 1332 DISJOINT (LIST_TO_SET vs) (LIST_TO_SET t) /\ 1333 DISJOINT (FV M) (LIST_TO_SET t)` 1334 by PROVE_TAC [DISJOINT_INSERT, DISJOINT_SYM] THEN 1335 Q_TAC SUFF_TAC `~(h' IN FV (LAMl vs M)) /\ 1336 (LAMl t (M ISUB APPEND (REVERSE (ZIP (MAP VAR t, vs))) 1337 [(VAR h',h)]) = 1338 [VAR h'/h] (LAMl vs M))` THEN1 1339 SRW_TAC [][SIMPLE_ALPHA] THEN 1340 ASM_SIMP_TAC (srw_ss()) [FV_LAMl] THEN 1341 FIRST_X_ASSUM (Q.SPECL_THEN [`t`, `M`] MP_TAC) THEN 1342 ASM_SIMP_TAC (srw_ss()) [] THEN 1343 DISCH_THEN (K ALL_TAC) THEN 1344 SRW_TAC [][LAMl_vsub, SUB_ISUB_SINGLETON, ISUB_APPEND] 1345 ]); 1346 1347val FRESH_lists = store_thm( 1348 "FRESH_lists", 1349 ``!n s : string set. 1350 FINITE s ==> ?l'. ALL_DISTINCT l' /\ DISJOINT (LIST_TO_SET l') s /\ 1351 (LENGTH l' = n)``, 1352 Induct THEN SRW_TAC [][] THENL [ 1353 RES_TAC THEN 1354 Q_TAC (NEW_TAC "z") `LIST_TO_SET l' UNION s` THEN 1355 Q.EXISTS_TAC `z::l'` THEN 1356 FULL_SIMP_TAC (srw_ss()) [] 1357 ]); 1358 1359val RENAMING_def = Define` 1360 (RENAMING [] = T) /\ 1361 (RENAMING (h::t) = (?y x:string. h = (VAR y:term,x)) /\ RENAMING t) 1362`; 1363val _ = export_rewrites ["RENAMING_def"] 1364 1365val RENAMING_APPEND = store_thm( 1366 "RENAMING_APPEND", 1367 ``!l1 l2. RENAMING (APPEND l1 l2) = RENAMING l1 /\ RENAMING l2``, 1368 Induct THEN SRW_TAC [][] THEN METIS_TAC []); 1369 1370val RENAMING_THM = CONJ RENAMING_def RENAMING_APPEND 1371 1372val RENAMING_REVERSE = store_thm( 1373 "RENAMING_REVERSE", 1374 ``!R. RENAMING (REVERSE R) = RENAMING R``, 1375 Induct THEN SRW_TAC [][RENAMING_APPEND, RENAMING_THM] THEN METIS_TAC []); 1376 1377val RENAMING_ZIP = store_thm( 1378 "RENAMING_ZIP", 1379 ``!l1 l2. (LENGTH l1 = LENGTH l2) ==> 1380 (RENAMING (ZIP (l1, l2)) = !e. MEM e l1 ==> ?s. e = VAR s)``, 1381 Induct THEN Cases_on `l2` THEN 1382 SRW_TAC [][RENAMING_THM] THEN PROVE_TAC []); 1383 1384val RENAMING_ZIP_MAP_VAR = store_thm( 1385 "RENAMING_ZIP_MAP_VAR", 1386 ``!l1 l2. (LENGTH l1 = LENGTH l2) ==> RENAMING (ZIP (MAP VAR l1, l2))``, 1387 Induct THEN Cases_on `l2` THEN 1388 SRW_TAC [][RENAMING_ZIP, listTheory.MEM_MAP] THEN 1389 SRW_TAC [][]); 1390 1391val _ = augment_srw_ss [rewrites [RENAMING_REVERSE, RENAMING_ZIP_MAP_VAR]] 1392 1393val is_comb_LAMl = store_thm( 1394 "is_comb_LAMl", 1395 ``is_comb (LAMl vs M) = (vs = []) /\ is_comb M``, 1396 Cases_on `vs` THEN SRW_TAC [][]); 1397val _ = export_rewrites ["is_comb_LAMl"] 1398 1399val strange_cases = prove( 1400 ``!M : term. (?vs M'. (M = LAMl vs M') /\ (size M' = 1)) \/ 1401 (?vs args t. 1402 (M = LAMl vs (FOLDL APP t args)) /\ 1403 ~(args = []) /\ ~is_comb t)``, 1404 HO_MATCH_MP_TAC simple_induction THEN REPEAT CONJ_TAC THENL [ 1405 (* VAR *) GEN_TAC THEN DISJ1_TAC THEN 1406 MAP_EVERY Q.EXISTS_TAC [`[]`, `VAR s`] THEN SRW_TAC [][size_thm], 1407 (* app *) MAP_EVERY Q.X_GEN_TAC [`M`,`N`] THEN 1408 DISCH_THEN (CONJUNCTS_THEN ASSUME_TAC) THEN 1409 DISJ2_TAC THEN Q.EXISTS_TAC `[]` THEN 1410 SIMP_TAC (srw_ss()) [] THEN 1411 `(?vs M'. (M = LAMl vs M') /\ (size M' = 1)) \/ 1412 (?vs args t. 1413 (M = LAMl vs (FOLDL APP t args)) /\ ~(args = []) /\ 1414 ~is_comb t)` by PROVE_TAC [] 1415 THENL [ 1416 MAP_EVERY Q.EXISTS_TAC [`[N]`, `M`] THEN 1417 ASM_SIMP_TAC (srw_ss()) [] THEN 1418 PROVE_TAC [combs_not_size_1], 1419 ASM_SIMP_TAC (srw_ss()) [] THEN 1420 Cases_on `vs` THENL [ 1421 MAP_EVERY Q.EXISTS_TAC [`APPEND args [N]`, `t`] THEN 1422 ASM_SIMP_TAC (srw_ss()) [foldl_snoc], 1423 MAP_EVERY Q.EXISTS_TAC [`[N]`, `M`] THEN 1424 ASM_SIMP_TAC (srw_ss()) [] 1425 ] 1426 ], 1427 (* LAM *) MAP_EVERY Q.X_GEN_TAC [`x`,`M`] THEN STRIP_TAC THENL [ 1428 DISJ1_TAC THEN 1429 MAP_EVERY Q.EXISTS_TAC [`x::vs`, `M'`] THEN 1430 ASM_SIMP_TAC (srw_ss()) [], 1431 DISJ2_TAC THEN 1432 MAP_EVERY Q.EXISTS_TAC [`x::vs`, `args`, `t`] THEN 1433 ASM_SIMP_TAC (srw_ss()) [] 1434 ] 1435 ]); 1436 1437val head_reduction_standard = store_thm( 1438 "head_reduction_standard", 1439 ``!s. is_head_reduction s ==> standard_reduction s``, 1440 HO_MATCH_MP_TAC standard_coind THEN SRW_TAC [][is_head_reduction_thm] THEN 1441 METIS_TAC [head_redex_leftmost, posn_lt_antisym, posn_lt_irrefl]); 1442 1443val i_reduce1_under_lam = prove( 1444 ``M i_reduce1 N ==> LAM v M i_reduce1 LAM v N``, 1445 SRW_TAC [][i_reduce1_def, is_internal_redex_def, 1446 redex_posns_thm, is_head_redex_thm] THEN 1447 Q.EXISTS_TAC `In::r` THEN SRW_TAC [][] THEN 1448 PROVE_TAC [labelled_redn_rules]); 1449 1450val i_reduce1_under_LAMl = prove( 1451 ``!vs. M i_reduce1 N ==> LAMl vs M i_reduce1 LAMl vs N``, 1452 Induct THEN SRW_TAC [][i_reduce1_under_lam]); 1453 1454 1455val i1_reduce_to_LAMl = prove( 1456 ``!vs M N. DISJOINT (LIST_TO_SET vs) (FV M) /\ ALL_DISTINCT vs ==> 1457 (M i_reduce1 LAMl vs N = 1458 ?M0. (M = LAMl vs M0) /\ M0 i_reduce1 N)``, 1459 SIMP_TAC (srw_ss()) [EQ_IMP_THM, IMP_CONJ_THM, FORALL_AND_THM] THEN 1460 CONJ_TAC THENL [ 1461 Induct THEN 1462 SRW_TAC [][i_reduce_to_LAM_underneath] THEN 1463 `DISJOINT (LIST_TO_SET vs) (FV M0)` 1464 by (FULL_SIMP_TAC (srw_ss()) [] THEN 1465 Q.PAT_X_ASSUM `DISJOINT X Y` MP_TAC THEN 1466 SRW_TAC [][DISJOINT_DEF, EXTENSION] THEN PROVE_TAC []) THEN 1467 `?M00. (M0 = LAMl vs M00) /\ M00 i_reduce1 N` by PROVE_TAC [] THEN 1468 PROVE_TAC [], 1469 1470 Q_TAC SUFF_TAC 1471 `!vs M N. M i_reduce1 N ==> LAMl vs M i_reduce1 LAMl vs N` THEN1 1472 PROVE_TAC [] THEN 1473 Induct THEN SRW_TAC [][] THEN 1474 PROVE_TAC [i_reduce1_under_lam] 1475 ]); 1476 1477val SUBSET_DISJOINT = store_thm( 1478 "SUBSET_DISJOINT", 1479 ``!X Y Z. X SUBSET Y /\ DISJOINT Y Z ==> DISJOINT X Z``, 1480 SRW_TAC [][SUBSET_DEF, DISJOINT_DEF, EXTENSION] THEN PROVE_TAC []); 1481 1482val i_reduces_to_LAMl = prove( 1483 ``!vs M N. DISJOINT (LIST_TO_SET vs) (FV M) /\ ALL_DISTINCT vs ==> 1484 (M i_reduces LAMl vs N = 1485 ?M0. (M = LAMl vs M0) /\ M0 i_reduces N)``, 1486 SIMP_TAC (srw_ss()) [i_reduces_RTC_i_reduce1, EQ_IMP_THM, 1487 FORALL_AND_THM, IMP_CONJ_THM] THEN CONJ_TAC 1488 THENL [ 1489 Q_TAC SUFF_TAC 1490 `!M N1. 1491 RTC (i_reduce1) M N1 ==> 1492 !vs N. (N1 = LAMl vs N) /\ DISJOINT (LIST_TO_SET vs) (FV M) /\ 1493 ALL_DISTINCT vs ==> 1494 ?M0. 1495 (M = LAMl vs M0) /\ RTC $i_reduce1 M0 N` 1496 THEN1 PROVE_TAC [] THEN 1497 HO_MATCH_MP_TAC relationTheory.RTC_STRONG_INDUCT_RIGHT1 THEN 1498 SRW_TAC [][] THEN 1499 `DISJOINT (LIST_TO_SET vs) (FV N1)` 1500 by (Q_TAC SUFF_TAC `FV N1 SUBSET FV M` THEN1 1501 PROVE_TAC [DISJOINT_SYM, SUBSET_DISJOINT] THEN 1502 Q_TAC SUFF_TAC 1503 `!M N. RTC (i_reduce1) M N ==> FV N SUBSET FV M` THEN1 1504 PROVE_TAC [] THEN 1505 HO_MATCH_MP_TAC relationTheory.RTC_INDUCT THEN 1506 SRW_TAC [][] THEN 1507 PROVE_TAC [cc_beta_FV_SUBSET, SUBSET_TRANS, labelled_redn_cc, 1508 i_reduce1_def]) THEN 1509 `?N10. (N1 = LAMl vs N10) /\ N10 i_reduce1 N` 1510 by PROVE_TAC [i1_reduce_to_LAMl] THEN 1511 `?M0. (M = LAMl vs M0) /\ RTC (i_reduce1) M0 N10` 1512 by METIS_TAC [] THEN 1513 Q.EXISTS_TAC `M0` THEN 1514 PROVE_TAC [relationTheory.RTC_CASES2], 1515 1516 Q_TAC SUFF_TAC `!M N. RTC $i_reduce1 M N ==> 1517 !vs. RTC (i_reduce1) (LAMl vs M) (LAMl vs N)` 1518 THEN1 PROVE_TAC [] THEN 1519 HO_MATCH_MP_TAC relationTheory.RTC_INDUCT THEN 1520 SRW_TAC [][relationTheory.RTC_RULES] THEN 1521 PROVE_TAC [relationTheory.RTC_RULES, i_reduce1_under_LAMl] 1522 ]); 1523 1524val size_vsubst = Store_Thm( 1525 "size_vsubst", 1526 ``!M:term. size ([VAR v/u] M) = size M``, 1527 HO_MATCH_MP_TAC nc_INDUCTION2 THEN Q.EXISTS_TAC `{u;v}` THEN 1528 SRW_TAC [][SUB_VAR, SUB_THM]); 1529 1530 1531val size_ISUB = prove( 1532 ``!R N:term. RENAMING R ==> (size (N ISUB R) = size N)``, 1533 Induct THEN 1534 ASM_SIMP_TAC (srw_ss())[ISUB_def, pairTheory.FORALL_PROD, 1535 RENAMING_THM] THEN 1536 SRW_TAC [][] THEN SRW_TAC [][]); 1537 1538val _ = augment_srw_ss [rewrites [size_ISUB]] 1539 1540val cant_ireduce_to_lam_atom = prove( 1541 ``!vs M N. (size N = 1) ==> ~(M i_reduce1 LAMl vs N)``, 1542 REPEAT GEN_TAC THEN 1543 Q.SPECL_THEN [`LENGTH vs`, `LIST_TO_SET vs UNION FV M UNION FV N`] 1544 MP_TAC FRESH_lists THEN 1545 SIMP_TAC (srw_ss()) [FINITE_FV] THEN 1546 DISCH_THEN (Q.X_CHOOSE_THEN `vs'` STRIP_ASSUME_TAC) THEN 1547 `LAMl vs N = LAMl vs' (N ISUB REVERSE (ZIP (MAP VAR vs', vs)))` 1548 by SRW_TAC [][LAMl_ALPHA] THEN 1549 FULL_SIMP_TAC (srw_ss()) [DISJOINT_SYM] THEN 1550 SRW_TAC [][i1_reduce_to_LAMl, cant_ireduce_to_atom]); 1551 1552val noncomb_nonabs_doesnt_reduce = store_thm( 1553 "noncomb_nonabs_doesnt_reduce", 1554 ``~is_comb t /\ ~is_abs t ==> ~(labelled_redn beta t r u)``, 1555 Q.SPEC_THEN `t` STRUCT_CASES_TAC term_CASES THEN 1556 SRW_TAC [][is_comb_thm, is_abs_thm] THEN 1557 ONCE_REWRITE_TAC [labelled_redn_cases] THEN 1558 SRW_TAC [][beta_def]); 1559 1560val i_reduce1_to_app = store_thm( 1561 "i_reduce1_to_app", 1562 ``M i_reduce1 (N @@ P) = 1563 (?N0 r. (M = N0 @@ P) /\ ~is_comb N0 /\ labelled_redn beta N0 r N) \/ 1564 (?N0. (M = N0 @@ P) /\ is_comb N0 /\ N0 i_reduce1 N) \/ 1565 (?P0 r. (M = N @@ P0) /\ labelled_redn beta P0 r P)``, 1566 SRW_TAC [][i_reduce1_def, EQ_IMP_THM] THENL [ 1567 RULE_ASSUM_TAC (ONCE_REWRITE_RULE [labelled_redn_cases]) THEN 1568 FULL_SIMP_TAC (srw_ss()) [] THEN SRW_TAC [][] THEN 1569 FULL_SIMP_TAC (srw_ss() ++ SatisfySimps.SATISFY_ss) 1570 [is_internal_redex_def, is_head_redex_thm, 1571 redex_posns_thm, beta_def] 1572 THENL [ 1573 PROVE_TAC [], 1574 FULL_SIMP_TAC (srw_ss()) [COND_RATOR, COND_RAND] 1575 ], 1576 Q.EXISTS_TAC `Lt::r` THEN 1577 SRW_TAC [][labelled_redn_rules, is_internal_redex_def, 1578 redex_posns_thm, is_head_redex_thm] THEN 1579 PROVE_TAC [labelled_redn_beta_redex_posn], 1580 Q.EXISTS_TAC `Lt::r` THEN 1581 FULL_SIMP_TAC (srw_ss())[labelled_redn_rules, is_internal_redex_def, 1582 redex_posns_thm, is_head_redex_thm], 1583 Q.EXISTS_TAC `Rt::r` THEN 1584 SRW_TAC [][labelled_redn_rules, is_internal_redex_def, 1585 redex_posns_thm, is_head_redex_thm] THEN 1586 PROVE_TAC [labelled_redn_beta_redex_posn] 1587 ]); 1588 1589val i_reduce1_to_fold_app = store_thm( 1590 "i_reduce1_to_fold_app", 1591 ``!args t M. 1592 M i_reduce1 FOLDL APP t args = 1593 (?t0 r. (M = FOLDL APP t0 args) /\ labelled_redn beta t0 r t /\ 1594 ~is_comb t0 /\ ~(args = [])) \/ 1595 (?t0. (M = FOLDL APP t0 args) /\ t0 i_reduce1 t) \/ 1596 (?pfx a0 a sfx r. 1597 (M = FOLDL APP t (APPEND pfx (a0 :: sfx))) /\ 1598 (args = (APPEND pfx (a :: sfx))) /\ 1599 labelled_redn beta a0 r a)``, 1600 Induct THEN SRW_TAC [][] THEN 1601 POP_ASSUM (K ALL_TAC) THEN EQ_TAC THEN REPEAT STRIP_TAC THENL [ 1602 `is_abs t0` by PROVE_TAC [noncomb_nonabs_doesnt_reduce] THEN 1603 POP_ASSUM MP_TAC THEN 1604 RULE_ASSUM_TAC (ONCE_REWRITE_RULE [labelled_redn_cases]) THEN 1605 FULL_SIMP_TAC (srw_ss()) [beta_def], 1606 FULL_SIMP_TAC (srw_ss()) [i_reduce1_to_app] THENL [ 1607 PROVE_TAC [], 1608 PROVE_TAC [], 1609 DISJ2_TAC THEN DISJ2_TAC THEN 1610 MAP_EVERY Q.EXISTS_TAC [`[]`,`P0`,`h`,`args`,`r`] THEN SRW_TAC [][] 1611 ], 1612 REPEAT DISJ2_TAC THEN 1613 MAP_EVERY Q.EXISTS_TAC [`h::pfx`,`a0`,`a`, `sfx`,`r`] THEN SRW_TAC [][], 1614 DISJ2_TAC THEN DISJ1_TAC THEN Q.EXISTS_TAC `t0 @@ h` THEN 1615 SRW_TAC [][] THEN 1616 `is_abs t0` by PROVE_TAC [noncomb_nonabs_doesnt_reduce] THEN 1617 SRW_TAC [][i_reduce1_def] THEN 1618 Q.EXISTS_TAC `Lt::r` THEN 1619 SRW_TAC [][is_internal_redex_def, is_head_redex_thm, redex_posns_thm, 1620 labelled_redn_rules] THEN 1621 PROVE_TAC [labelled_redn_beta_redex_posn], 1622 DISJ2_TAC THEN DISJ1_TAC THEN 1623 Q.EXISTS_TAC `t0 @@ h` THEN SRW_TAC [][] THEN 1624 FULL_SIMP_TAC (srw_ss()) [i_reduce1_def, is_head_redex_thm, 1625 is_internal_redex_def, redex_posns_thm] THEN 1626 Q.EXISTS_TAC `Lt::r` THEN SRW_TAC [][labelled_redn_rules] THEN 1627 PROVE_TAC [], 1628 Cases_on `pfx` THEN FULL_SIMP_TAC (srw_ss()) [] THENL [ 1629 DISJ2_TAC THEN DISJ1_TAC THEN Q.EXISTS_TAC `t @@ a0` THEN 1630 SRW_TAC [][i_reduce1_def, is_internal_redex_def] THEN 1631 Q.EXISTS_TAC `Rt::r` THEN 1632 SRW_TAC [][labelled_redn_rules, is_head_redex_thm, redex_posns_thm] THEN 1633 PROVE_TAC [labelled_redn_beta_redex_posn], 1634 REPEAT DISJ2_TAC THEN 1635 MAP_EVERY Q.EXISTS_TAC [`t'`, `a0`, `a`, `sfx`, `r`] THEN 1636 SRW_TAC [][] 1637 ] 1638 ]); 1639 1640val EL_APPEND1 = prove( 1641 ``!l1 l2 n. n < LENGTH l1 ==> (EL n (APPEND l1 l2) = EL n l1)``, 1642 Induct THEN SRW_TAC [][] THEN 1643 Cases_on `n` THEN FULL_SIMP_TAC (srw_ss()) []); 1644 1645val EL_APPEND2 = prove( 1646 ``!l1 l2 n. LENGTH l1 <= n /\ n < LENGTH l1 + LENGTH l2 ==> 1647 (EL n (APPEND l1 l2) = EL (n - LENGTH l1) l2)``, 1648 Induct THEN SRW_TAC [][] THEN 1649 Cases_on `n` THEN FULL_SIMP_TAC (srw_ss()) [arithmeticTheory.ADD_CLAUSES]); 1650 1651val ireduces_to_fold_app = store_thm( 1652 "ireduces_to_fold_app", 1653 ``M i_reduces FOLDL APP t args ��� 1654 ���t0 args0. 1655 (M = FOLDL APP t0 args0) ��� (LENGTH args0 = LENGTH args) ��� 1656 reduction beta t0 t ��� 1657 EVERY (��p. reduction beta (FST p) (SND p)) (ZIP (args0, args))``, 1658 SIMP_TAC (srw_ss()) [i_reduces_RTC_i_reduce1] THEN 1659 Q_TAC SUFF_TAC 1660 `���M N. RTC (i_reduce1) M N ��� 1661 ���t args. (N = FOLDL APP t args) ��� 1662 ���t0 args0. 1663 (M = FOLDL APP t0 args0) ��� 1664 (LENGTH args0 = LENGTH args) ��� 1665 reduction beta t0 t ��� 1666 EVERY (��p. reduction beta (FST p) (SND p)) 1667 (ZIP (args0, args))` 1668 THEN1 PROVE_TAC [] THEN 1669 HO_MATCH_MP_TAC relationTheory.RTC_INDUCT_RIGHT1 THEN 1670 SRW_TAC [][] THENL [ 1671 MAP_EVERY Q.EXISTS_TAC [`t`, `args`] THEN 1672 SIMP_TAC (srw_ss()) [reduction_rules, listTheory.MEM_ZIP, 1673 listTheory.EVERY_MEM, GSYM LEFT_FORALL_IMP_THM], 1674 FULL_SIMP_TAC (srw_ss()) [i_reduce1_to_fold_app] THENL [ 1675 RES_TAC THEN 1676 MAP_EVERY Q.EXISTS_TAC [`t0'`, `args0`] THEN 1677 SRW_TAC [][] THEN 1678 PROVE_TAC [reduction_rules, labelled_redn_cc], 1679 RES_TAC THEN 1680 MAP_EVERY Q.EXISTS_TAC [`t0'`, `args0`] THEN 1681 SRW_TAC [][] THEN 1682 PROVE_TAC [reduction_rules, labelled_redn_cc, i_reduce1_def], 1683 RES_TAC THEN 1684 MAP_EVERY Q.EXISTS_TAC [`t0`, `args0`] THEN SRW_TAC [ARITH_ss][] THEN 1685 Q.PAT_X_ASSUM `EVERY f l` MP_TAC THEN 1686 FULL_SIMP_TAC (srw_ss()) [] THEN 1687 ASM_SIMP_TAC (srw_ss() ++ ARITH_ss) 1688 [listTheory.EVERY_MEM, listTheory.MEM_ZIP, 1689 GSYM LEFT_FORALL_IMP_THM] THEN 1690 STRIP_TAC THEN GEN_TAC THEN STRIP_TAC THEN 1691 Cases_on `n < LENGTH pfx` THENL [ 1692 FIRST_X_ASSUM (Q.SPEC_THEN `n` MP_TAC) THEN 1693 SRW_TAC [numSimps.ARITH_ss][EL_APPEND1], 1694 `LENGTH pfx <= n` by DECIDE_TAC THEN 1695 FIRST_X_ASSUM (Q.SPEC_THEN `n` MP_TAC) THEN 1696 Cases_on `n = LENGTH pfx` THEN 1697 SRW_TAC [numSimps.ARITH_ss][EL_APPEND2, EL_APPEND1] THENL [ 1698 PROVE_TAC [reduction_rules, labelled_redn_cc], 1699 `n ��� LENGTH pfx = SUC (n - (LENGTH pfx +1))` by DECIDE_TAC THEN 1700 FULL_SIMP_TAC (srw_ss()) [] 1701 ] 1702 ] 1703 ] 1704 ]); 1705 1706val standard_reductions_ok = store_thm( 1707 "standard_reductions_ok", 1708 ``!s. standard_reduction s ==> okpath (labelled_redn beta) s``, 1709 PROVE_TAC [standard_reduction_def]); 1710 1711val valid_posns_relate = store_thm( 1712 "valid_posns_relate", 1713 ``!t r1 r2. r1 IN valid_posns t /\ r2 IN valid_posns t ==> 1714 r1 < r2 \/ (r1 = r2) \/ r2 < r1``, 1715 HO_MATCH_MP_TAC simple_induction THEN 1716 SRW_TAC [][valid_posns_thm]); 1717 1718val lefty_relates_to_first_nonless = store_thm( 1719 "lefty_relates_to_first_nonless", 1720 ``!p. okpath (labelled_redn beta) p /\ finite p ==> 1721 !r0 r M. r0 IN redex_posns (first p) /\ 1722 (!n. SUC n IN PL p ==> r0 < nth_label n p) /\ 1723 labelled_redn beta (last p) r M ==> 1724 r0 < r \/ (r0 = r) \/ r < r0``, 1725 HO_MATCH_MP_TAC finite_okpath_ind THEN SRW_TAC [][] THENL [ 1726 `r IN redex_posns x` by METIS_TAC [labelled_redn_beta_redex_posn] THEN 1727 METIS_TAC [valid_posns_relate, redex_posns_are_valid], 1728 FIRST_X_ASSUM MATCH_MP_TAC THEN Q.EXISTS_TAC `M` THEN 1729 SRW_TAC [][] THENL [ 1730 FIRST_X_ASSUM (Q.SPEC_THEN `0` MP_TAC) THEN SRW_TAC [][] THEN 1731 METIS_TAC [lr_beta_preserves_lefter_redexes], 1732 FIRST_X_ASSUM (Q.SPEC_THEN `SUC n` MP_TAC) THEN SRW_TAC [][] 1733 ] 1734 ]); 1735 1736val okpath_every_el_relates = store_thm( 1737 "okpath_every_el_relates", 1738 ``!R p. okpath R p = 1739 !i. SUC i IN PL p ==> R (el i p) (nth_label i p) (el (SUC i) p)``, 1740 GEN_TAC THEN SIMP_TAC (srw_ss()) [EQ_IMP_THM, FORALL_AND_THM] THEN 1741 CONJ_TAC THENL [ 1742 SIMP_TAC (srw_ss()) [GSYM RIGHT_FORALL_IMP_THM] THEN 1743 Induct_on `i`, 1744 HO_MATCH_MP_TAC okpath_co_ind 1745 ] THEN REPEAT GEN_TAC THENL [ 1746 Q.SPEC_THEN `p` STRUCT_CASES_TAC path_cases, 1747 Q.SPEC_THEN `p` STRUCT_CASES_TAC path_cases, 1748 ALL_TAC 1749 ] THEN SRW_TAC [][] THENL [ 1750 POP_ASSUM (Q.SPEC_THEN `0` MP_TAC) THEN SRW_TAC [][], 1751 RES_THEN MP_TAC THEN SIMP_TAC (srw_ss()) [] 1752 ]); 1753 1754val seg_SUC_pcons = store_thm( 1755 "seg_SUC_pcons", 1756 ``!i j p x r. i < j /\ j IN PL p ==> 1757 (seg (SUC i) j (pcons x r p) = seg i (j - 1) p)``, 1758 SRW_TAC [][seg_def] THEN 1759 Q_TAC SUFF_TAC `j - SUC i = j - 1 - i` THEN1 SRW_TAC [][] THEN 1760 DECIDE_TAC); 1761 1762val standard_reduction_thm = store_thm( 1763 "standard_reduction_thm", 1764 ``(standard_reduction (stopped_at x) = T) /\ 1765 (standard_reduction (pcons x r p) = 1766 labelled_redn beta x r (first p) /\ 1767 (!n r0. r0 IN redex_posns x /\ r0 < r /\ n + 1 IN PL p ==> 1768 r0 < nth_label n p) /\ 1769 standard_reduction p)``, 1770 CONJ_TAC THENL [ 1771 SRW_TAC [][standard_reduction_def], 1772 SIMP_TAC (srw_ss()) [EQ_IMP_THM, 1773 GSYM RIGHT_FORALL_IMP_THM, IMP_CONJ_THM] THEN 1774 REPEAT CONJ_TAC THENL [ 1775 SRW_TAC [][standard_reduction_def], 1776 SIMP_TAC (srw_ss())[better_standard_reduction, 1777 GSYM ADD1] THEN 1778 completeInduct_on `n` THEN REPEAT STRIP_TAC THEN 1779 FULL_SIMP_TAC (srw_ss()) [] THEN 1780 FIRST_X_ASSUM (Q.SPECL_THEN [`SUC n`, `0`] MP_TAC) THEN 1781 `n IN PL p` by METIS_TAC [PL_downward_closed, DECIDE ``n < SUC n``] THEN 1782 ASM_SIMP_TAC (srw_ss()) [seg_def, residuals_pcons, 1783 residual1_different_singletons] THEN 1784 `!m. SUC m IN PL (take n p) ==> r0 < nth_label m (take n p)` 1785 by (SRW_TAC [][PL_take] THEN 1786 `m < n` by DECIDE_TAC THEN 1787 SRW_TAC [][nth_label_take] THEN 1788 `SUC m IN PL p` 1789 by METIS_TAC [PL_downward_closed, 1790 DECIDE ``m < n = SUC m < SUC n``] THEN 1791 METIS_TAC []) THEN 1792 `labelled_redn beta (el n p) (nth_label n p) (el (SUC n) p)` 1793 by METIS_TAC [okpath_every_el_relates] THEN 1794 `last (take n p) = el n p` by SRW_TAC [][last_take] THEN 1795 `okpath (labelled_redn beta) (take n p)` by METIS_TAC [okpath_take] THEN 1796 `first (take n p) = first p` by SRW_TAC [][first_take] THEN 1797 `r0 IN redex_posns (first p)` 1798 by METIS_TAC [lr_beta_preserves_lefter_redexes] THEN 1799 `finite (take n p)` by SRW_TAC [][finite_take] THEN 1800 `r0 < nth_label n p \/ (r0 = nth_label n p) \/ nth_label n p < r0` 1801 by METIS_TAC [lefty_relates_to_first_nonless] 1802 THENL [ 1803 SRW_TAC [][], 1804 DISCH_THEN (Q.SPEC_THEN `r0` MP_TAC) THEN SRW_TAC [][] THEN 1805 SRW_TAC [][residuals_different_singletons], 1806 Q.ABBREV_TAC `r00 = nth_label n p` THEN 1807 `r00 IN redex_posns (first p)` 1808 by METIS_TAC [cant_create_redexes_to_left] THEN 1809 `r00 IN redex_posns x` 1810 by METIS_TAC [cant_create_redexes_to_left1] THEN 1811 DISCH_THEN (Q.SPEC_THEN `r00` MP_TAC) THEN 1812 `r00 < r` by METIS_TAC [posn_lt_trans] THEN 1813 `!m. SUC m IN PL (take n p) ==> r00 < nth_label m (take n p)` 1814 by (SRW_TAC [][PL_take] THEN 1815 `m < n` by DECIDE_TAC THEN 1816 SRW_TAC [][nth_label_take] THEN 1817 `SUC m IN PL p` 1818 by METIS_TAC [PL_downward_closed, 1819 DECIDE ``m < n = SUC m < SUC n``] THEN 1820 METIS_TAC []) THEN 1821 SRW_TAC [][residuals_different_singletons] 1822 ], 1823 1824 SRW_TAC [][better_standard_reduction, GSYM ADD1] THEN 1825 FIRST_X_ASSUM (Q.SPECL_THEN [`SUC i`, `SUC j`] MP_TAC) THEN 1826 SRW_TAC [][seg_def], 1827 1828 SRW_TAC [][better_standard_reduction, GSYM ADD1] THEN 1829 Cases_on `j` THENL [ 1830 FULL_SIMP_TAC (srw_ss()) [seg_def] THEN 1831 `?n. i = SUC n` by METIS_TAC [TypeBase.nchotomy_of ``:num``, 1832 DECIDE ``0 < n = ~(n = 0)``] THEN 1833 FULL_SIMP_TAC (srw_ss()) [] THEN 1834 `n IN PL p` by METIS_TAC [PL_downward_closed, 1835 DECIDE ``n < SUC n``] THEN 1836 `okpath (labelled_redn beta) (take n p)` 1837 by SRW_TAC [][okpath_take] THEN 1838 `finite (take n p)` by SRW_TAC [][finite_take] THEN 1839 `first (take n p) = first p` by SRW_TAC [][first_take] THEN 1840 SRW_TAC [][residuals_pcons, residual1_different_singletons] THEN 1841 `p' IN redex_posns (first p)` 1842 by METIS_TAC [lr_beta_preserves_lefter_redexes] THEN 1843 `!m. SUC m IN PL (take n p) ==> p' < nth_label m (take n p)` 1844 by (SRW_TAC [][PL_take] THEN 1845 `m < n` by DECIDE_TAC THEN 1846 SRW_TAC [][nth_label_take] THEN 1847 FIRST_X_ASSUM MATCH_MP_TAC THEN SRW_TAC [][] THEN 1848 METIS_TAC [PL_downward_closed, 1849 arithmeticTheory.LESS_MONO_EQ]) THEN 1850 SRW_TAC [][residuals_different_singletons] THEN 1851 METIS_TAC [posn_lt_irrefl], 1852 1853 FULL_SIMP_TAC (srw_ss()) [] THEN 1854 `?m. i = SUC m` by METIS_TAC [TypeBase.nchotomy_of ``:num``, 1855 DECIDE ``~(SUC n < 0)``] THEN 1856 FULL_SIMP_TAC (srw_ss()) [] THEN 1857 `n < SUC m` by DECIDE_TAC THEN 1858 SRW_TAC [][seg_SUC_pcons] 1859 ] 1860 ] 1861 ]); 1862 1863 1864val PL_plink = prove( 1865 ``!p1. finite p1 ==> 1866 !x p2. x IN PL (plink p1 p2) = 1867 x IN PL p1 \/ 1868 ?n. 0 < n /\ n IN PL p2 /\ (x = n + THE (length p1) - 1)``, 1869 HO_MATCH_MP_TAC pathTheory.finite_path_ind THEN 1870 SRW_TAC [][pathTheory.length_thm] THENL [ 1871 PROVE_TAC [pathTheory.PL_0, DECIDE ``(x = 0) \/ 0 < x``], 1872 SRW_TAC [numSimps.ARITH_ss][LEFT_AND_OVER_OR, EXISTS_OR_THM, 1873 GSYM RIGHT_EXISTS_AND_THM] THEN 1874 `0 < THE (length p1)` 1875 by (`?m. length p1 = SOME m` 1876 by PROVE_TAC [pathTheory.finite_length] THEN 1877 SRW_TAC [][] THEN 1878 Q_TAC SUFF_TAC `~(m = 0)` THEN1 DECIDE_TAC THEN STRIP_TAC THEN 1879 PROVE_TAC [pathTheory.length_never_zero]) THEN 1880 SRW_TAC [numSimps.ARITH_ss][ADD1] THEN PROVE_TAC [] 1881 ]); 1882 1883val el_plink_left = store_thm( 1884 "el_plink_left", 1885 ``!i p1. i IN PL p1 /\ (last p1 = first p2) ==> 1886 (el i (plink p1 p2) = el i p1)``, 1887 Induct THENL [ 1888 SRW_TAC [][first_plink], 1889 GEN_TAC THEN 1890 Q.SPEC_THEN `p1` STRUCT_CASES_TAC path_cases THEN 1891 SRW_TAC [][] 1892 ]); 1893 1894val drop_plink_left = store_thm( 1895 "drop_plink_left", 1896 ``!i p1. i IN PL p1 /\ (last p1 = first p2) ==> 1897 (drop i (plink p1 p2) = plink (drop i p1) p2)``, 1898 Induct THEN SRW_TAC [][] THEN 1899 Q.SPEC_THEN `p1` (REPEAT_TCL STRIP_THM_THEN SUBST_ALL_TAC) path_cases THEN 1900 FULL_SIMP_TAC (srw_ss()) []); 1901 1902val take_plink_left = store_thm( 1903 "take_plink_left", 1904 ``!i p1. i IN PL p1 /\ (last p1 = first p2) ==> 1905 (take i (plink p1 p2) = take i p1)``, 1906 Induct THENL [ 1907 SRW_TAC [][], 1908 GEN_TAC THEN 1909 Q.SPEC_THEN `p1` STRUCT_CASES_TAC path_cases THEN 1910 SRW_TAC [][] 1911 ]); 1912 1913val IN_PL_tail = store_thm( 1914 "IN_PL_tail", 1915 ``!x p1. x + 1 IN PL p1 ==> x IN PL (tail p1)``, 1916 Induct THENL [ 1917 SRW_TAC [][], 1918 GEN_TAC THEN 1919 Q.SPEC_THEN `p1` STRUCT_CASES_TAC path_cases THEN 1920 SRW_TAC [][arithmeticTheory.ADD_CLAUSES, GSYM ADD1] 1921 ]); 1922 1923val last_drop = store_thm( 1924 "last_drop", 1925 ``!i p. i IN PL p ==> (last (drop i p) = last p)``, 1926 Induct THENL [ 1927 SRW_TAC [][], 1928 GEN_TAC THEN Q.SPEC_THEN `p` STRUCT_CASES_TAC path_cases THEN 1929 SRW_TAC [][] 1930 ]); 1931 1932val seg_plink_left = store_thm( 1933 "seg_plink_left", 1934 ``!i j. i <= j /\ j IN PL p1 /\ (last p1 = first p2) ==> 1935 (seg i j (plink p1 p2) = seg i j p1)``, 1936 SRW_TAC [][seg_def] THEN 1937 `i IN PL p1` by METIS_TAC [arithmeticTheory.LESS_OR_EQ, 1938 PL_downward_closed] THEN 1939 SRW_TAC [][drop_plink_left] THEN 1940 `j - i IN PL (drop i p1)` by SRW_TAC [numSimps.ARITH_ss][IN_PL_drop] THEN 1941 SRW_TAC [][take_plink_left, last_drop]); 1942 1943val nth_label_plink_left = store_thm( 1944 "nth_label_plink_left", 1945 ``!i p1. i + 1 IN PL p1 ==> (nth_label i (plink p1 p2) = nth_label i p1)``, 1946 Induct THEN GEN_TAC THEN 1947 Q.SPEC_THEN `p1` STRUCT_CASES_TAC path_cases THEN 1948 SRW_TAC [][arithmeticTheory.ADD_CLAUSES, GSYM ADD1]); 1949 1950val nth_label_plink_right = store_thm( 1951 "nth_label_plink_right", 1952 ``!i p1 p2. finite p1 /\ THE (length p1) <= SUC i /\ (last p1 = first p2) ==> 1953 (nth_label i (plink p1 p2) = 1954 nth_label (SUC i - THE (length p1)) p2)``, 1955 Induct THEN 1956 GEN_TAC THEN Q.SPEC_THEN `p1` STRUCT_CASES_TAC path_cases THEN 1957 SRW_TAC [][length_thm, DECIDE ``y + x <= x = (y = 0)``] THENL [ 1958 FULL_SIMP_TAC (srw_ss()) [finite_length] THEN 1959 Q.PAT_X_ASSUM `length x = SOME y` MP_TAC THEN 1960 DISCH_THEN (fn th => SUBST_ALL_TAC th THEN ASSUME_TAC th) THEN 1961 FULL_SIMP_TAC (srw_ss()) [] THEN VAR_EQ_TAC THEN 1962 FULL_SIMP_TAC (srw_ss()) [length_never_zero], 1963 `THE (length q) <= SUC i` by DECIDE_TAC THEN 1964 SRW_TAC [][GSYM ADD1] 1965 ]); 1966 1967val standard_reductions_join_over_comb = prove( 1968 ``!s1 s2. 1969 standard_reduction s1 /\ standard_reduction s2 /\ 1970 finite s1 /\ finite s2 ==> 1971 standard_reduction (plink (pmap (\t. t @@ first s2) (CONS Lt) s1) 1972 (pmap (APP (last s1)) (CONS Rt) s2))``, 1973 Q_TAC SUFF_TAC 1974 `!s1. 1975 okpath (labelled_redn beta) s1 /\ finite s1 ==> 1976 standard_reduction s1 ==> 1977 !s2. standard_reduction s2 /\ finite s2 ==> 1978 standard_reduction (plink (pmap (\t. t @@ first s2) (CONS Lt) s1) 1979 (pmap (APP (last s1)) (CONS Rt) s2))` 1980 THEN1 METIS_TAC [standard_reductions_ok] THEN 1981 HO_MATCH_MP_TAC finite_okpath_ind THEN 1982 SIMP_TAC (srw_ss()) [standard_reduction_thm] THEN CONJ_TAC THENL [ 1983 Q_TAC SUFF_TAC 1984 `!s. okpath (labelled_redn beta) s /\ finite s ==> 1985 !x. standard_reduction s ==> 1986 standard_reduction (pmap (APP x) (CONS Rt) s)` THEN1 1987 METIS_TAC [standard_reductions_ok] THEN 1988 HO_MATCH_MP_TAC finite_okpath_ind THEN 1989 SRW_TAC [][standard_reduction_thm, labelled_redn_rules] THEN 1990 FULL_SIMP_TAC (srw_ss()) [GSYM ADD1, nth_label_pmap] THEN 1991 FULL_SIMP_TAC (srw_ss()) [redex_posns_thm] THENL [ 1992 REPEAT VAR_EQ_TAC THEN FULL_SIMP_TAC (srw_ss()) [], 1993 FULL_SIMP_TAC (srw_ss() ++ COND_elim_ss) [] THEN RES_TAC 1994 ], 1995 MAP_EVERY Q.X_GEN_TAC [`x`,`r`,`p`] THEN REPEAT STRIP_TAC THEN 1996 Q.ABBREV_TAC `p' = pmap (\t. t @@ first s2) (CONS Lt) p` THEN 1997 Q.ABBREV_TAC `s2' = pmap (APP (last p)) (CONS Rt) s2` THEN 1998 `last p' = first s2'` by SRW_TAC [][] THENL [ 1999 SRW_TAC [][first_plink, labelled_redn_rules], 2000 2001 `finite p'` by SRW_TAC [][] THEN 2002 FULL_SIMP_TAC (srw_ss()) [PL_plink] THENL [ 2003 SRW_TAC [][] THEN 2004 FULL_SIMP_TAC (srw_ss()) [nth_label_plink_left, nth_label_pmap, 2005 GSYM ADD1] THEN 2006 FULL_SIMP_TAC (srw_ss()) [redex_posns_thm] THEN 2007 SRW_TAC [][] THEN FULL_SIMP_TAC (srw_ss()) [] THEN 2008 FULL_SIMP_TAC (srw_ss() ++ COND_elim_ss) [] THEN RES_TAC, 2009 2010 `THE (length p') <= SUC n` by DECIDE_TAC THEN 2011 ASM_SIMP_TAC (srw_ss())[nth_label_plink_right] THEN 2012 `SUC n - THE (length p') = n' - 1` by DECIDE_TAC THEN 2013 `SUC (n' - 1) = n'` by DECIDE_TAC THEN 2014 SRW_TAC [][] THEN 2015 FULL_SIMP_TAC (srw_ss()) [nth_label_pmap] THEN 2016 MATCH_MP_TAC posn_lt_trans THEN Q.EXISTS_TAC `Lt::r` THEN 2017 SRW_TAC [][] 2018 ] 2019 ] 2020 ]); 2021 2022val standard_reductions_join_over_comb = store_thm( 2023 "standard_reductions_join_over_comb", 2024 ``!s1 s2. standard_reduction s1 /\ finite s1 /\ 2025 standard_reduction s2 /\ finite s2 ==> 2026 ?s. 2027 standard_reduction s /\ finite s /\ 2028 (first s = first s1 @@ first s2) /\ 2029 (last s = last s1 @@ last s2)``, 2030 REPEAT STRIP_TAC THEN 2031 Q.ABBREV_TAC `s1' = pmap (\t. t @@ first s2) (CONS Lt) s1` THEN 2032 Q.ABBREV_TAC `s2' = pmap (APP (last s1)) (CONS Rt) s2` THEN 2033 Q.EXISTS_TAC `plink s1' s2'` THEN 2034 `last s1' = first s2'` by SRW_TAC [][] THEN 2035 SRW_TAC [][] THEN 2036 METIS_TAC [standard_reductions_join_over_comb]); 2037 2038val ISUB_APP = prove( 2039 ``!sub M N. (M @@ N) ISUB sub = (M ISUB sub) @@ (N ISUB sub)``, 2040 Induct THEN ASM_SIMP_TAC (srw_ss()) [pairTheory.FORALL_PROD, ISUB_def, 2041 SUB_THM]); 2042 2043val FOLDL_APP_ISUB = prove( 2044 ``!args (t:term) sub. 2045 FOLDL APP t args ISUB sub = 2046 FOLDL APP (t ISUB sub) (MAP (\t. t ISUB sub) args)``, 2047 Induct THEN SRW_TAC [][ISUB_APP]); 2048 2049val size_foldl_app = prove( 2050 ``!args t : term. 2051 size (FOLDL APP t args) = FOLDL (\n t. n + size t + 1) (size t) args``, 2052 Induct THEN SRW_TAC [][size_thm]); 2053 2054val size_foldl_app_lt = prove( 2055 ``!(args : term list) x. x <= FOLDL (\n t. n + size t + 1) x args``, 2056 Induct THEN SRW_TAC [][] THEN 2057 `x + size h + 1 <= FOLDL (\n t. n + size t + 1) (x + size h + 1) args` 2058 by METIS_TAC [] THEN 2059 DECIDE_TAC); 2060 2061val size_args_foldl_app = prove( 2062 ``!args n (t : term) x. n < LENGTH args ==> 2063 size (EL n args) < x + size (FOLDL APP t args)``, 2064 Induct THEN SRW_TAC [][] THEN 2065 Cases_on `n` THEN SRW_TAC [][] THENL [ 2066 SRW_TAC [][size_foldl_app, size_thm] THEN 2067 `size t + size h + 1 <= 2068 FOLDL (\n t. n + size t + 1) (size t + size h + 1) args` 2069 by SRW_TAC [][size_foldl_app_lt] THEN 2070 DECIDE_TAC, 2071 FULL_SIMP_TAC (srw_ss()) [] 2072 ]); 2073 2074val head_standard_is_standard = store_thm( 2075 "head_standard_is_standard", 2076 ``!s1 s2. 2077 is_head_reduction s1 /\ finite s1 /\ (last s1 = first s2) /\ 2078 standard_reduction s2 ==> 2079 standard_reduction (plink s1 s2)``, 2080 Q_TAC SUFF_TAC 2081 `!s1. okpath (labelled_redn beta) s1 /\ finite s1 ==> 2082 is_head_reduction s1 ==> 2083 !s2. standard_reduction s2 /\ (last s1 = first s2) ==> 2084 standard_reduction (plink s1 s2)` THEN1 2085 METIS_TAC [is_head_reduction_def] THEN 2086 HO_MATCH_MP_TAC finite_okpath_ind THEN 2087 SRW_TAC [][standard_reduction_thm, is_head_reduction_thm] THEN 2088 METIS_TAC [head_redex_leftmost, posn_lt_irrefl, posn_lt_antisym]); 2089 2090val collect_standard_reductions = prove( 2091 ``!args0 args s. 2092 (LENGTH args = LENGTH args0) /\ 2093 standard_reduction s /\ finite s /\ 2094 EVERY (\p. ?arg_s. (first arg_s = FST p) /\ 2095 finite arg_s /\ 2096 (last arg_s = SND p) /\ 2097 standard_reduction arg_s) (ZIP (args0, args)) ==> 2098 ?s'. standard_reduction s' /\ finite s' /\ 2099 (first s' = FOLDL APP (first s) args0) /\ 2100 (last s' = FOLDL APP (last s) args)``, 2101 Induct THEN SRW_TAC [][] THENL [ 2102 FULL_SIMP_TAC (srw_ss()) [] THEN METIS_TAC [], 2103 FULL_SIMP_TAC (srw_ss()) [listTheory.LENGTH_CONS] THEN VAR_EQ_TAC THEN 2104 FULL_SIMP_TAC (srw_ss()) [] THEN 2105 `?s0. standard_reduction s0 /\ finite s0 /\ 2106 (first s @@ h = first s0) /\ (last s @@ h' = last s0)` 2107 by (ONCE_REWRITE_TAC [EQ_SYM_EQ] THEN REPEAT VAR_EQ_TAC THEN 2108 MATCH_MP_TAC standard_reductions_join_over_comb THEN 2109 SRW_TAC [][]) THEN 2110 ASM_REWRITE_TAC [] THEN 2111 FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC [] 2112 ]); 2113 2114val standard_reduction_under_LAM = prove( 2115 ``!s. standard_reduction s /\ finite s ==> 2116 standard_reduction (pmap (LAM v) (CONS In) s)``, 2117 Q_TAC SUFF_TAC 2118 `!s. okpath (labelled_redn beta) s /\ finite s ==> 2119 standard_reduction s ==> 2120 standard_reduction (pmap (LAM v) (CONS In) s)` THEN1 2121 METIS_TAC [standard_reductions_ok] THEN 2122 HO_MATCH_MP_TAC finite_okpath_ind THEN 2123 SRW_TAC [][standard_reduction_thm, labelled_redn_rules, 2124 nth_label_pmap, GSYM ADD1, redex_posns_thm] THEN 2125 FULL_SIMP_TAC (srw_ss()) []); 2126 2127val standard_reduction_under_LAMl = prove( 2128 ``!vs s. finite s /\ standard_reduction s ==> 2129 ?s'. (first s' = LAMl vs (first s)) /\ 2130 (last s' = LAMl vs (last s)) /\ finite s' /\ 2131 standard_reduction s'``, 2132 Induct THEN SRW_TAC [][] THENL [ 2133 METIS_TAC [], 2134 `?s0. (first s0 = LAMl vs (first s)) /\ 2135 (last s0 = LAMl vs (last s)) /\ finite s0 /\ standard_reduction s0` 2136 by METIS_TAC [] THEN 2137 Q.EXISTS_TAC `pmap (LAM h) (CONS In) s0` THEN SRW_TAC [][] THEN 2138 METIS_TAC [standard_reduction_under_LAM] 2139 ]); 2140 2141val standardisation_theorem = store_thm( 2142 "standardisation_theorem", 2143 ``!M N. reduction beta M N ==> 2144 ?s. (first s = M) /\ finite s /\ (last s = N) /\ 2145 standard_reduction s``, 2146 CONV_TAC SWAP_VARS_CONV THEN GEN_TAC THEN completeInduct_on `size N` THEN 2147 FULL_SIMP_TAC (srw_ss()) [GSYM RIGHT_FORALL_IMP_THM] THEN 2148 SRW_TAC [][] THEN 2149 `?Z. M head_reduces Z /\ Z i_reduces N` by PROVE_TAC [lemma11_4_6] THEN 2150 Q.SPEC_THEN `N` STRIP_ASSUME_TAC strange_cases THENL [ 2151 `Z = N` by 2152 (FULL_SIMP_TAC (srw_ss()) [i_reduces_RTC_i_reduce1] THEN 2153 RULE_ASSUM_TAC (ONCE_REWRITE_RULE [relationTheory.RTC_CASES2]) THEN 2154 FULL_SIMP_TAC (srw_ss()) [] THEN 2155 PROVE_TAC [cant_ireduce_to_lam_atom]) THEN 2156 PROVE_TAC [head_reduces_def, head_reduction_standard], 2157 Q.SPECL_THEN [`LENGTH vs`, 2158 `LIST_TO_SET vs UNION FV (FOLDL APP t args) UNION FV Z`] 2159 MP_TAC FRESH_lists THEN 2160 SIMP_TAC (srw_ss()) [FINITE_FV] THEN 2161 DISCH_THEN (Q.X_CHOOSE_THEN `vs'` STRIP_ASSUME_TAC) THEN 2162 Q.ABBREV_TAC `sub = REVERSE (ZIP (MAP VAR vs' : term list, vs))` THEN 2163 `LAMl vs (FOLDL APP t args) = LAMl vs' (FOLDL APP t args ISUB sub)` 2164 by SRW_TAC [][LAMl_ALPHA] THEN 2165 Q.ABBREV_TAC `N0 = FOLDL APP t args ISUB sub` THEN 2166 `?Z0. (Z = LAMl vs' Z0) /\ Z0 i_reduces N0` 2167 by METIS_TAC [i_reduces_to_LAMl, DISJOINT_SYM] THEN 2168 `N0 = FOLDL APP (t ISUB sub) (MAP (\t. t ISUB sub) args)` 2169 by SRW_TAC [][FOLDL_APP_ISUB] THEN 2170 Q.ABBREV_TAC `args' = MAP (\t. t ISUB sub) args` THEN 2171 `?t0 args0. 2172 (Z0 = FOLDL APP t0 args0) /\ (LENGTH args0 = LENGTH args') /\ 2173 reduction beta t0 (t ISUB sub) /\ 2174 EVERY (\p. reduction beta (FST p) (SND p)) (ZIP (args0, args'))` 2175 by METIS_TAC [ireduces_to_fold_app] THEN 2176 `!t. size (t ISUB sub) = size t` 2177 by SRW_TAC [][RENAMING_REVERSE, RENAMING_ZIP] THEN 2178 `size (t ISUB sub) < size N` 2179 by (SRW_TAC [][size_foldl_app] THEN 2180 Cases_on `args` THEN FULL_SIMP_TAC (srw_ss()) [] THEN 2181 `size t + size h + 1 <= 2182 FOLDL (\n t. n + size t + 1) (size t + size h + 1) t'` by 2183 METIS_TAC [size_foldl_app_lt] THEN 2184 DECIDE_TAC) THEN 2185 `?ts. (first ts = t0) /\ finite ts /\ (last ts = t ISUB sub) /\ 2186 standard_reduction ts` by METIS_TAC[] THEN 2187 `EVERY (\p. ?arg_s. (first arg_s = FST p) /\ finite arg_s /\ 2188 (last arg_s = SND p) /\ standard_reduction arg_s) 2189 (ZIP (args0, args'))` 2190 by (FULL_SIMP_TAC (srw_ss())[listTheory.EVERY_MEM, listTheory.MEM_ZIP, 2191 GSYM LEFT_FORALL_IMP_THM] THEN 2192 REPEAT STRIP_TAC THEN 2193 FULL_SIMP_TAC (srw_ss()) [AND_IMP_INTRO] THEN 2194 FIRST_X_ASSUM MATCH_MP_TAC THEN 2195 ASM_SIMP_TAC (srw_ss()) [size_args_foldl_app] THEN 2196 Q.PAT_X_ASSUM `LENGTH x = LENGTH y` ASSUME_TAC THEN 2197 FULL_SIMP_TAC (srw_ss()) [listTheory.MEM_ZIP, 2198 GSYM LEFT_FORALL_IMP_THM]) THEN 2199 `?sr. standard_reduction sr /\ finite sr /\ 2200 (first sr = FOLDL APP (first ts) args0) /\ 2201 (last sr = FOLDL APP (last ts) args')` 2202 by (MATCH_MP_TAC collect_standard_reductions THEN 2203 ASM_REWRITE_TAC []) THEN 2204 `?hr. is_head_reduction hr /\ finite hr /\ (first hr = M) /\ 2205 (last hr = Z)` 2206 by METIS_TAC [head_reduces_def] THEN 2207 `?sr2. (first sr2 = LAMl vs' (first sr)) /\ 2208 (last sr2 = LAMl vs' (last sr)) /\ 2209 finite sr2 /\ standard_reduction sr2` 2210 by (MATCH_MP_TAC standard_reduction_under_LAMl THEN 2211 ASM_REWRITE_TAC []) THEN 2212 Q.EXISTS_TAC `plink hr sr2` THEN 2213 SRW_TAC [][head_standard_is_standard] 2214 ]); 2215 2216val has_hnf_def = Define` 2217 has_hnf M = ?N. M == N /\ hnf N 2218`; 2219 2220val has_bnf_hnf = store_thm( 2221 "has_bnf_hnf", 2222 ``has_bnf M ��� has_hnf M``, 2223 SRW_TAC [][has_hnf_def, chap2Theory.has_bnf_def] THEN 2224 METIS_TAC [bnf_hnf]); 2225 2226val head_reduct_def = Define` 2227 head_reduct M = if ?r. r is_head_redex M then 2228 SOME (@N. M -h-> N) 2229 else NONE 2230`; 2231 2232val head_reduct_unique = store_thm( 2233 "head_reduct_unique", 2234 ``!M N. M -h-> N ==> (head_reduct M = SOME N)``, 2235 SRW_TAC [][head_reduce1_def, head_reduct_def] THEN1 METIS_TAC [] THEN 2236 SELECT_ELIM_TAC THEN METIS_TAC [is_head_redex_unique, labelled_redn_det]); 2237 2238val head_reduct_NONE = store_thm( 2239 "head_reduct_NONE", 2240 ``(head_reduct M = NONE) = !N. ~(M -h-> N)``, 2241 SRW_TAC [][head_reduct_def, head_reduce1_def] THEN 2242 METIS_TAC [head_redex_is_redex, IN_term_IN_redex_posns, 2243 is_redex_occurrence_def]); 2244 2245val head_reduct_SOME = store_thm( 2246 "head_reduct_SOME", 2247 ``(head_reduct M = SOME N) = M -h-> N``, 2248 SIMP_TAC (srw_ss()) [EQ_IMP_THM, head_reduct_unique] THEN 2249 SRW_TAC [][head_reduct_def] THEN SELECT_ELIM_TAC THEN 2250 SRW_TAC [][head_reduce1_def] THEN 2251 METIS_TAC [head_redex_is_redex, IN_term_IN_redex_posns, 2252 is_redex_occurrence_def]); 2253 2254val drop_not_stopped = prove( 2255 ``!i p. SUC i IN PL p ==> ?v r q. drop i p = pcons v r q``, 2256 Induct THEN GEN_TAC THEN 2257 Q.SPEC_THEN `p` STRUCT_CASES_TAC path_cases THEN 2258 SRW_TAC [][]); 2259 2260val drop_tail_commute = store_thm( 2261 "drop_tail_commute", 2262 ``!i p. SUC i IN PL p ==> (drop i (tail p) = tail (drop i p))``, 2263 Induct THEN SIMP_TAC (srw_ss()) [Once FORALL_path] THEN 2264 SRW_TAC [][]); 2265 2266val is_head_reduction_coind = store_thm( 2267 "is_head_reduction_coind", 2268 ``(!x r q. P (pcons x r q) ==> 2269 labelled_redn beta x r (first q) /\ 2270 r is_head_redex x /\ P q) ==> 2271 !p. P p ==> is_head_reduction p``, 2272 SIMP_TAC (srw_ss()) [is_head_reduction_def, IMP_CONJ_THM, 2273 FORALL_AND_THM] THEN CONJ_TAC 2274 THENL [ 2275 STRIP_TAC THEN HO_MATCH_MP_TAC okpath_co_ind THEN METIS_TAC [], 2276 STRIP_TAC THEN GEN_TAC THEN STRIP_TAC THEN 2277 Q_TAC SUFF_TAC `!i. i + 1 IN PL p ==> nth_label i p is_head_redex el i p /\ 2278 P (drop (i + 1) p)` THEN1 2279 METIS_TAC [] THEN 2280 Induct THEN FULL_SIMP_TAC (srw_ss()) [GSYM ADD1] THENL [ 2281 Q.ISPEC_THEN `p` FULL_STRUCT_CASES_TAC path_cases THEN 2282 FULL_SIMP_TAC (srw_ss()) [] THEN METIS_TAC [], 2283 STRIP_TAC THEN 2284 `SUC i IN PL p` 2285 by METIS_TAC [PL_downward_closed, DECIDE ``x < SUC x``] THEN 2286 FULL_SIMP_TAC (srw_ss()) [] THEN 2287 Q.ISPEC_THEN `p` FULL_STRUCT_CASES_TAC path_cases THEN 2288 FULL_SIMP_TAC (srw_ss()) [] THEN 2289 `?y s q'. drop i q = pcons y s q'` by METIS_TAC [drop_not_stopped] THEN 2290 `labelled_redn beta y s (first q') /\ s is_head_redex y /\ P q'` 2291 by METIS_TAC [stopped_at_not_pcons, pcons_11] THEN 2292 `el 0 (drop i q) = el i q` by SRW_TAC [][] THEN 2293 `el i q = y` by METIS_TAC [el_def, first_thm] THEN 2294 `nth_label 0 (drop i q) = nth_label i q` by SRW_TAC [][] THEN 2295 `nth_label i q = s` by METIS_TAC [nth_label_def, first_label_def] THEN 2296 SRW_TAC [][drop_tail_commute] 2297 ] 2298 ]); 2299 2300val head_reduction_path_uexists = prove( 2301 ``!M. ?!p. (first p = M) /\ is_head_reduction p /\ 2302 (finite p ==> hnf (last p))``, 2303 GEN_TAC THEN 2304 Q.ISPEC_THEN `\M. (M, OPTION_MAP (\N. ((@r. r is_head_redex M), N)) 2305 (head_reduct M))` 2306 STRIP_ASSUME_TAC path_Axiom THEN 2307 `!M. first (g M) = M` 2308 by (POP_ASSUM (fn th => SRW_TAC [][Once th]) THEN 2309 Cases_on `head_reduct M` THEN SRW_TAC [][]) THEN 2310 `!M. is_head_reduction (g M)` 2311 by (Q_TAC SUFF_TAC 2312 `!p. (?M. p = g M) ==> is_head_reduction p` THEN1 2313 METIS_TAC [] THEN 2314 HO_MATCH_MP_TAC is_head_reduction_coind THEN 2315 Q.PAT_X_ASSUM `!x:term. g x = Z` 2316 (fn th => SIMP_TAC (srw_ss()) 2317 [Once th, SimpL ``(==>)``]) THEN 2318 REPEAT GEN_TAC THEN STRIP_TAC THEN 2319 Cases_on `head_reduct M` THEN 2320 FULL_SIMP_TAC (srw_ss()) [head_reduct_SOME, head_reduce1_def] THEN 2321 REPEAT VAR_EQ_TAC THEN SELECT_ELIM_TAC THEN 2322 METIS_TAC [is_head_redex_unique]) THEN 2323 `!p. finite p ==> !M. (p = g M) ==> hnf (last p)` 2324 by (HO_MATCH_MP_TAC finite_path_ind THEN 2325 SIMP_TAC (srw_ss()) [] THEN CONJ_TAC THEN REPEAT GEN_TAC THENL [ 2326 Q.PAT_X_ASSUM `!x:term. g x = Z` 2327 (fn th => ONCE_REWRITE_TAC [th]) THEN 2328 Cases_on `head_reduct M` THEN SRW_TAC [][] THEN 2329 FULL_SIMP_TAC (srw_ss()) [hnf_no_head_redex, head_reduct_NONE, 2330 head_reduce1_def] THEN 2331 METIS_TAC [head_redex_is_redex, IN_term_IN_redex_posns, 2332 is_redex_occurrence_def], 2333 STRIP_TAC THEN GEN_TAC THEN 2334 Q.PAT_X_ASSUM `!x:term. g x = Z` 2335 (fn th => ONCE_REWRITE_TAC [th]) THEN 2336 Cases_on `head_reduct M` THEN SRW_TAC [][] 2337 ]) THEN 2338 SIMP_TAC (srw_ss()) [EXISTS_UNIQUE_THM] THEN CONJ_TAC THENL [ 2339 Q.EXISTS_TAC `g M` THEN 2340 Q.PAT_X_ASSUM `!x:term. g x = Z` (K ALL_TAC) THEN METIS_TAC [], 2341 REPEAT (POP_ASSUM (K ALL_TAC)) THEN 2342 REPEAT STRIP_TAC THEN 2343 ONCE_REWRITE_TAC [path_bisimulation] THEN 2344 Q.EXISTS_TAC `\p1 p2. is_head_reduction p1 /\ is_head_reduction p2 /\ 2345 (first p1 = first p2) /\ 2346 (finite p1 ==> hnf (last p1)) /\ 2347 (finite p2 ==> hnf (last p2))` THEN 2348 SRW_TAC [][] THEN 2349 Q.ISPEC_THEN `q1` (REPEAT_TCL STRIP_THM_THEN SUBST_ALL_TAC) 2350 path_cases THEN 2351 Q.ISPEC_THEN `q2` (REPEAT_TCL STRIP_THM_THEN SUBST_ALL_TAC) 2352 path_cases THEN FULL_SIMP_TAC (srw_ss()) [] 2353 THENL [ 2354 METIS_TAC [hnf_no_head_redex], 2355 METIS_TAC [hnf_no_head_redex], 2356 METIS_TAC [is_head_redex_unique, labelled_redn_det] 2357 ] 2358 ]); 2359 2360val head_reduction_path_def = new_specification( 2361 "head_reduction_path_def", 2362 ["head_reduction_path"], 2363 CONJUNCT1 ((SIMP_RULE bool_ss [EXISTS_UNIQUE_THM] o 2364 SIMP_RULE bool_ss [UNIQUE_SKOLEM_THM]) 2365 head_reduction_path_uexists)); 2366 2367val head_reduction_path_unique = store_thm( 2368 "head_reduction_path_unique", 2369 ``!M p. (first p = M) /\ is_head_reduction p /\ 2370 (finite p ==> hnf (last p)) ==> 2371 (head_reduction_path M = p)``, 2372 REPEAT STRIP_TAC THEN 2373 Q.SPEC_THEN `M` (ASSUME_TAC o CONJUNCT2 o 2374 SIMP_RULE bool_ss [EXISTS_UNIQUE_THM]) 2375 head_reduction_path_uexists THEN 2376 METIS_TAC [head_reduction_path_def]); 2377 2378val hnf_preserved = store_thm( 2379 "hnf_preserved", 2380 ``!M N. reduction beta M N ==> hnf M ==> hnf N``, 2381 SIMP_TAC (srw_ss())[] THEN 2382 HO_MATCH_MP_TAC relationTheory.RTC_INDUCT THEN 2383 SRW_TAC [][hnf_no_head_redex] THEN 2384 Q_TAC SUFF_TAC `!p. ~(p is_head_redex N)` THEN1 PROVE_TAC [] THEN 2385 `?r. labelled_redn beta M r M'` by METIS_TAC [cc_labelled_redn] THEN 2386 `r is_internal_redex M` by METIS_TAC [is_internal_redex_def, 2387 labelled_redn_beta_redex_posn] THEN 2388 METIS_TAC [lemma11_4_3i]); 2389 2390val hnf_reflected_over_ireduction = store_thm( 2391 "hnf_reflected_over_ireduction", 2392 ``!M N. M i_reduces N ==> hnf N ==> hnf M``, 2393 SIMP_TAC (srw_ss()) [i_reduces_RTC_i_reduce1] THEN 2394 HO_MATCH_MP_TAC relationTheory.RTC_INDUCT THEN 2395 SRW_TAC [][hnf_no_head_redex, i_reduce1_def] THEN 2396 METIS_TAC [lemma11_4_3ii]); 2397 2398val corollary11_4_8 = store_thm( 2399 "corollary11_4_8", 2400 ``!M. has_hnf M = finite (head_reduction_path M)``, 2401 GEN_TAC THEN EQ_TAC THENL [ 2402 SRW_TAC [][has_hnf_def] THEN 2403 `?Z. reduction beta M Z /\ reduction beta N Z` 2404 by METIS_TAC [lameq_betaconversion, theorem3_13, beta_CR] THEN 2405 `hnf Z` by METIS_TAC [hnf_preserved] THEN 2406 `?Z0. M head_reduces Z0 /\ Z0 i_reduces Z` by METIS_TAC [lemma11_4_6] THEN 2407 `hnf Z0` by METIS_TAC [hnf_reflected_over_ireduction] THEN 2408 `?p. finite p /\ (first p = M) /\ (last p = Z0) /\ 2409 is_head_reduction p` by METIS_TAC [head_reduces_def] THEN 2410 METIS_TAC [head_reduction_path_unique], 2411 SRW_TAC [][has_hnf_def, lameq_betaconversion] THEN 2412 `(first (head_reduction_path M) = M) /\ 2413 hnf (last (head_reduction_path M)) /\ 2414 is_head_reduction (head_reduction_path M)` 2415 by METIS_TAC [head_reduction_path_def] THEN 2416 Q.EXISTS_TAC `last (head_reduction_path M)` THEN 2417 METIS_TAC [head_reduces_reduction_beta, conversion_rules, 2418 head_reduces_def] 2419 ]); 2420 2421(* named by analogy with has_bnf_thm in chap3Theory *) 2422val has_hnf_thm = store_thm( 2423 "has_hnf_thm", 2424 ``has_hnf M ��� ���N. M -h->* N ��� hnf N``, 2425 SRW_TAC [][corollary11_4_8, EQ_IMP_THM] THENL [ 2426 Q.EXISTS_TAC `last (head_reduction_path M)` THEN 2427 METIS_TAC [head_reduction_path_def, head_reduces_def, 2428 head_reduces_RTC_hreduce1], 2429 2430 `M head_reduces N` by METIS_TAC [head_reduces_RTC_hreduce1] THEN 2431 `���p. finite p ��� (first p = M) ��� (last p = N) ��� is_head_reduction p` 2432 by METIS_TAC [head_reduces_def] THEN 2433 METIS_TAC [head_reduction_path_unique] 2434 ]); 2435 2436val has_hnf_whnf = store_thm( 2437 "has_hnf_whnf", 2438 ``has_hnf M ��� has_whnf M``, 2439 METIS_TAC [has_hnf_thm, head_reductions_have_weak_prefixes, 2440 has_whnf_def]); 2441 2442val has_bnf_whnf = store_thm( 2443 "has_bnf_whnf", 2444 ``has_bnf M ��� has_whnf M``, 2445 METIS_TAC [has_bnf_hnf, has_hnf_whnf]); 2446 2447val _ = export_theory() 2448 2449end (* struct *) 2450