1open HolKernel Parse boolLib bossLib 2 3open boolSimps pred_setTheory pathTheory binderLib 4open chap3Theory standardisationTheory term_posnsTheory termTheory 5 finite_developmentsTheory appFOLDLTheory nomsetTheory 6 7val _ = new_theory "normal_order" 8 9val _ = set_trace "Unicode" 1 10 11fun Store_thm(trip as (n,t,tac)) = store_thm trip before export_rewrites [n] 12 13(* ---------------------------------------------------------------------- 14 Normal order reduction 15 16 This relation is a bit monstrous really. In particular, nice 17 properties of ��-reduction don't necessarily translate across. For 18 example, substitutivity doesn't hold. This would have that 19 20 M -n-> N ��� [P/v]M -n-> [P/v]N 21 22 but this isn't true because the variable v might be at the head 23 position in M, and P might contain a redex. Then the reduction 24 that was OK on the left has to be deferred for the reduction in P 25 on the right. 26 ---------------------------------------------------------------------- *) 27 28val (normorder_rules, normorder_ind, normorder_cases) = Hol_reln` 29 (���v M N. normorder (LAM v M @@ N) ([N/v]M)) ��� 30 (���v M1 M2. normorder M1 M2 ��� normorder (LAM v M1) (LAM v M2)) ��� 31 (���M1 M2 N. normorder M1 M2 ��� ��is_abs M1 ��� normorder (M1 @@ N) (M2 @@ N)) ��� 32 (���M N1 N2. normorder N1 N2 ��� bnf M ��� ��is_abs M ��� 33 normorder (M @@ N1) (M @@ N2)) 34`; 35 36val _ = set_fixity "-n->" (Infix(NONASSOC,450)) 37val _ = overload_on ("-n->", ``normorder``) 38val _ = set_fixity "-n->*" (Infix(NONASSOC,450)) 39val _ = overload_on ("-n->*", ``RTC normorder``) 40 41val tpm_normorder_I = store_thm( 42 "tpm_normorder_I", 43 ``���M N. M -n-> N ��� ���pi. tpm pi M -n-> tpm pi N``, 44 HO_MATCH_MP_TAC normorder_ind THEN SRW_TAC [][normorder_rules, tpm_subst]); 45 46val tpm_normorder_eqn = store_thm( 47 "tpm_normorder_eqn", 48 ``tpm pi M -n-> tpm pi N ��� M -n-> N``, 49 METIS_TAC [pmact_inverse, tpm_normorder_I]); 50val _ = export_rewrites ["tpm_normorder_eqn"] 51 52val normorder_bvc_gen_ind = store_thm( 53 "normorder_bvc_gen_ind", 54 ``���P f. 55 (���x. FINITE (f x)) ��� 56 (���v M N x. v ��� FV N ��� v ��� f x ��� P (LAM v M @@ N) ([N/v]M) x) ��� 57 (���v M N x. v ��� f x ��� (���y. P M N y) ��� P (LAM v M) (LAM v N) x) ��� 58 (���M1 M2 N x. (���y. P M1 M2 y) ��� ��is_abs M1 ��� P (M1 @@ N) (M2 @@ N) x) ��� 59 (���M N1 N2 x. 60 (���y. P N1 N2 y) ��� bnf M ��� ��is_abs M ��� P (M @@ N1) (M @@ N2) x) 61 ��� 62 ���M N. M -n-> N ��� ���x. P M N x``, 63 REPEAT GEN_TAC THEN STRIP_TAC THEN 64 Q_TAC SUFF_TAC 65 `���M N. M -n-> N ��� ����� x. P (tpm �� M) (tpm �� N) x` 66 THEN1 METIS_TAC [pmact_nil] THEN 67 HO_MATCH_MP_TAC normorder_ind THEN SRW_TAC [][] THENL [ 68 SRW_TAC [][tpm_subst] THEN 69 Q_TAC (NEW_TAC "z") 70 `{lswapstr �� v} ��� FV (tpm �� N) ��� f x ��� FV (tpm �� M)` THEN 71 `LAM (lswapstr �� v) (tpm �� M) = LAM z ([VAR z/lswapstr �� v] (tpm �� M))` 72 by SRW_TAC [][SIMPLE_ALPHA] THEN 73 POP_ASSUM SUBST_ALL_TAC THEN 74 `[tpm �� N/lswapstr �� v](tpm �� M) = 75 [tpm �� N/z] ([VAR z/lswapstr �� v](tpm �� M))` 76 by SRW_TAC [][lemma15a] THEN 77 POP_ASSUM SUBST_ALL_TAC THEN 78 FIRST_X_ASSUM MATCH_MP_TAC THEN SRW_TAC [][], 79 80 Q_TAC (NEW_TAC "z") 81 `{lswapstr �� v} ��� FV (tpm �� M) ��� FV (tpm �� N) ��� f x` THEN 82 `(LAM (lswapstr �� v) (tpm �� M) = LAM z (tpm [(z, lswapstr �� v)] (tpm �� M))) 83 ��� 84 (LAM (lswapstr �� v) (tpm �� N) = LAM z (tpm [(z, lswapstr �� v)] (tpm �� N)))` 85 by SRW_TAC [][tpm_ALPHA] THEN 86 NTAC 2 (POP_ASSUM SUBST_ALL_TAC) THEN 87 SRW_TAC [][GSYM pmact_decompose] 88 ]); 89 90infix |> fun x |> f = f x 91val normorder_bvc_ind = save_thm( 92 "normorder_bvc_ind", 93 normorder_bvc_gen_ind |> SPEC_ALL 94 |> Q.INST [`P` |-> `��M N x. P1 M N`, `f` |-> `��x. X`] 95 |> SIMP_RULE (srw_ss()) [] 96 |> Q.INST [`P1` |-> `P`] 97 |> Q.GEN `X` |> Q.GEN `P`); 98 99val normorder_ccbeta = store_thm( 100 "normorder_ccbeta", 101 ``���M N. M -n-> N ��� M -��-> N``, 102 HO_MATCH_MP_TAC normorder_ind THEN SRW_TAC [][compat_closure_rules] THEN 103 METIS_TAC [compat_closure_rules, beta_def]); 104 105val normorder_lameq = store_thm( 106 "normorder_lameq", 107 ``���M N. M -n-> N ��� M == N``, 108 SRW_TAC [][normorder_ccbeta, ccbeta_lameq]); 109 110val normorder_FV = store_thm( 111 "normorder_FV", 112 ``M -n-> N ��� v ��� FV N ��� v ��� FV M``, 113 METIS_TAC [normorder_ccbeta, cc_beta_FV_SUBSET, SUBSET_DEF]); 114 115val normorder_rwts = store_thm( 116 "normorder_rwts", 117 ``(VAR s -n-> N ��� F) ��� 118 (LAM v M -n-> N ��� ���M'. (N = LAM v M') ��� M -n-> M') ��� 119 (LAM v M @@ N -n-> P ��� (P = [N/v]M)) ��� 120 (��is_abs M ��� (M @@ N -n-> P ��� 121 (bnf M ��� ���N'. (P = M @@ N') ��� N -n-> N') ��� 122 ���M'. (P = M' @@ N) ��� M -n-> M'))``, 123 SRW_TAC [][] THENL [ 124 SRW_TAC [][Once normorder_cases], 125 126 CONV_TAC (LAND_CONV (ONCE_REWRITE_CONV [normorder_cases])) THEN 127 SIMP_TAC (srw_ss() ++ DNF_ss) [LAM_eq_thm, tpm_eqr] THEN 128 SRW_TAC [][EQ_IMP_THM] THEN1 SRW_TAC [][] THEN 129 Q.EXISTS_TAC `tpm [(v,v')] M2` THEN 130 `v ��� FV (tpm [(v,v')] M)` by SRW_TAC [][] THEN 131 `v ��� FV M2` by METIS_TAC [normorder_FV] THEN 132 SRW_TAC [][LAM_eq_thm, pmact_flip_args] THEN 133 METIS_TAC [pmact_sing_inv, tpm_normorder_I], 134 135 CONV_TAC (LAND_CONV (ONCE_REWRITE_CONV [normorder_cases])) THEN 136 SIMP_TAC (srw_ss() ++ DNF_ss) [LAM_eq_thm, tpm_eqr] THEN 137 SRW_TAC [][EQ_IMP_THM] THEN 138 METIS_TAC [fresh_tpm_subst, lemma15a, pmact_flip_args], 139 140 CONV_TAC (LAND_CONV (ONCE_REWRITE_CONV [normorder_cases])) THEN 141 SRW_TAC [][EQ_IMP_THM] THEN SRW_TAC [][] THEN 142 FULL_SIMP_TAC (srw_ss()) [] 143 ]); 144 145 146val normorder_bnf = store_thm( 147 "normorder_bnf", 148 ``bnf M ��� ���N. ��(M -n-> N)``, 149 Q.ID_SPEC_TAC `M` THEN HO_MATCH_MP_TAC simple_induction THEN 150 SRW_TAC [][normorder_rwts] THEN 151 SIMP_TAC (srw_ss()) [EQ_IMP_THM, normorder_rwts] THEN 152 Cases_on `is_abs M` THENL [ 153 `���v M0. M = LAM v M0` 154 by (Q.SPEC_THEN `M` FULL_STRUCT_CASES_TAC term_CASES THEN 155 FULL_SIMP_TAC (srw_ss()) [normorder_rwts] THEN 156 METIS_TAC []) THEN 157 SRW_TAC [][normorder_rwts], 158 159 SRW_TAC [][normorder_rwts] THEN 160 METIS_TAC [simpLib.SIMP_PROVE (srw_ss()) [] 161 ``���M1 M2 N1 N2. (M1 @@ N1:term = M2 @@ N2) ��� 162 (M1 = M2) ��� (N1 = N2)``] 163 ]); 164 165val strong_normorder_ind = 166 IndDefLib.derive_strong_induction (normorder_rules, normorder_ind) 167 168val normorder_det = store_thm( 169 "normorder_det", 170 ``���M N. M -n-> N ��� ���N'. M -n-> N' ��� (N' = N)``, 171 HO_MATCH_MP_TAC strong_normorder_ind THEN 172 SRW_TAC [][normorder_rwts] THEN 173 METIS_TAC [normorder_bnf]); 174 175val noposn_def = define_recursive_term_function` 176 (noposn (VAR s) = NONE) ��� 177 (noposn (M @@ N) = if is_abs M then SOME [] 178 else case noposn M of 179 NONE => OPTION_MAP (CONS Rt) (noposn N) 180 | SOME p => SOME (Lt::p)) ��� 181 (noposn (LAM v M) = OPTION_MAP (CONS In) (noposn M)) 182`; 183val _ = export_rewrites ["noposn_def"] 184 185val bnf_noposn = store_thm( 186 "bnf_noposn", 187 ``���M. bnf M ��� (noposn M = NONE)``, 188 HO_MATCH_MP_TAC simple_induction THEN 189 SRW_TAC [][] THEN Cases_on `noposn M` THEN SRW_TAC [][]) 190 191val normorder_noposn = store_thm( 192 "normorder_noposn", 193 ``M -n-> N ��� ���p. (noposn M = SOME p) ��� labelled_redn beta M p N``, 194 EQ_TAC THENL [ 195 Q_TAC SUFF_TAC 196 `���M N. M -n-> N ��� ���p. (noposn M = SOME p) ��� labelled_redn beta M p N` 197 THEN1 METIS_TAC [] THEN 198 HO_MATCH_MP_TAC normorder_ind THEN SRW_TAC [][bnf_noposn] THEN 199 SRW_TAC [][labelled_redn_rules] THEN 200 METIS_TAC [labelled_redn_rules, beta_def], 201 202 Q_TAC SUFF_TAC 203 `���M p N. labelled_redn beta M p N ��� 204 (noposn M = SOME p) ��� M -n-> N` THEN1 METIS_TAC [] THEN 205 HO_MATCH_MP_TAC labelled_redn_ind THEN 206 SIMP_TAC (srw_ss() ++ DNF_ss) [beta_def, normorder_rules] THEN 207 SRW_TAC [][] THENL [ 208 Cases_on `noposn M` THEN FULL_SIMP_TAC (srw_ss()) [normorder_rules], 209 Cases_on `noposn z` THEN FULL_SIMP_TAC (srw_ss()) [] THEN 210 METIS_TAC [bnf_noposn, normorder_rules] 211 ] 212 ]); 213 214val noposn_least = store_thm( 215 "noposn_least", 216 ``���M p. 217 (noposn M = SOME p) ��� p ��� redex_posns M ��� 218 ���p'. p' ��� redex_posns M ��� 219 (p' = p) ��� p < p'``, 220 HO_MATCH_MP_TAC simple_induction THEN SRW_TAC [][redex_posns_def] THENL [ 221 Cases_on `noposn M` THEN FULL_SIMP_TAC (srw_ss()) [] THEN 222 SRW_TAC [][], 223 Cases_on `noposn M` THEN FULL_SIMP_TAC (srw_ss()) [] THENL [ 224 `���N. labelled_redn beta M x N` 225 by METIS_TAC [is_redex_occurrence_def, IN_term_IN_redex_posns] THEN 226 `bnf M` by METIS_TAC [bnf_noposn] THEN 227 METIS_TAC [labelled_redn_cc, beta_normal_form_bnf, corollary3_2_1], 228 SRW_TAC [][] 229 ], 230 231 Cases_on `noposn M` THEN FULL_SIMP_TAC (srw_ss()) [] THEN 232 SRW_TAC [][] 233 ]); 234 235val normorder_reduction_def = Define` 236 normorder_reduction p = 237 okpath (��M r N. (noposn M = SOME r) ��� labelled_redn beta M r N) p 238` 239val normorder_is_standard = store_thm( 240 "normorder_is_standard", 241 ``���p. normorder_reduction p ��� standard_reduction p``, 242 HO_MATCH_MP_TAC standard_coind THEN 243 SRW_TAC [][normorder_reduction_def] THEN 244 METIS_TAC [posn_lt_antisym, posn_lt_irrefl, noposn_least]); 245 246val ihr_noposn = store_thm( 247 "ihr_noposn", 248 ``���r M. r is_head_redex M ��� (noposn M = SOME r)``, 249 HO_MATCH_MP_TAC is_head_redex_ind THEN SRW_TAC [][]); 250 251val head_is_normorder = store_thm( 252 "head_is_normorder", 253 ``���p. is_head_reduction p ��� normorder_reduction p``, 254 SIMP_TAC (srw_ss()) [normorder_reduction_def] THEN 255 HO_MATCH_MP_TAC okpath_co_ind THEN 256 SRW_TAC [][is_head_reduction_thm, ihr_noposn]); 257 258val ADD1 = arithmeticTheory.ADD1 259 260val last_el = store_thm( 261 "last_el", 262 ``���p. finite p ��� 263 (last p = el (THE (length p) - 1) p)``, 264 HO_MATCH_MP_TAC finite_path_ind THEN SRW_TAC [][length_thm] THEN 265 Q_TAC SUFF_TAC `���n. length p = SOME (SUC n)` 266 THEN1 SIMP_TAC (srw_ss() ++ DNF_ss ++ ARITH_ss) [] THEN 267 METIS_TAC [finite_length, length_never_zero, arithmeticTheory.num_CASES]); 268 269val standard_to_bnf_is_normal = store_thm( 270 "standard_to_bnf_is_normal", 271 ``���p. standard_reduction p ��� finite p ��� bnf (last p) ��� 272 normorder_reduction p``, 273 SIMP_TAC (srw_ss()) [normorder_reduction_def] THEN 274 HO_MATCH_MP_TAC okpath_co_ind THEN 275 SRW_TAC [][standard_reduction_thm] THEN 276 `���r���. noposn M = SOME r���` 277 by (Cases_on `noposn M` THEN SRW_TAC [][] THEN 278 `bnf M` by METIS_TAC [bnf_noposn] THEN 279 METIS_TAC [labelled_redn_cc, beta_normal_form_bnf, 280 corollary3_2_1]) THEN 281 `r��� ��� redex_posns M ��� ���r'. r' ��� redex_posns M ��� (r' = r���) ��� r��� < r'` 282 by METIS_TAC [noposn_least] THEN 283 `r ��� redex_posns M` by METIS_TAC [labelled_redn_beta_redex_posn] THEN 284 `(r = r���) ��� r��� < r` by METIS_TAC [] THEN1 SRW_TAC [][] THEN 285 `okpath (labelled_redn beta) p` by METIS_TAC [standard_reductions_ok] THEN 286 `���n. n ��� PL p ��� r��� ��� redex_posns (el n p)` 287 by (Induct THEN SRW_TAC [][] THENL [ 288 METIS_TAC [lr_beta_preserves_lefter_redexes], 289 `labelled_redn beta (el n p) (nth_label n p) (el (SUC n) p)` 290 by METIS_TAC [okpath_every_el_relates] THEN 291 `n ��� PL p` 292 by METIS_TAC [PL_downward_closed, DECIDE ``x < SUC x``] THEN 293 METIS_TAC [lr_beta_preserves_lefter_redexes, ADD1, el_def] 294 ]) THEN 295 `���m. 0 < m ��� (length p = SOME m)` 296 by METIS_TAC [finite_length, length_never_zero, 297 DECIDE ``0 < x ��� x ��� 0``] THEN 298 `last p = el (m - 1) p` 299 by METIS_TAC [last_el, optionTheory.option_CLAUSES] THEN 300 `m - 1 ��� PL p` by SRW_TAC [][PL_def] THEN 301 `r��� ��� redex_posns (last p)` by METIS_TAC [] THEN 302 `���N. labelled_redn beta (last p) r��� N` 303 by METIS_TAC [is_redex_occurrence_def, IN_term_IN_redex_posns] THEN 304 METIS_TAC [labelled_redn_cc, beta_normal_form_bnf, corollary3_2_1]); 305 306val finite_normorder_RTC = store_thm( 307 "finite_normorder_RTC", 308 ``���p. normorder_reduction p ��� finite p ��� first p -n->* last p``, 309 REWRITE_TAC [normorder_reduction_def] THEN 310 HO_MATCH_MP_TAC finite_okpath_ind THEN SRW_TAC [][] THEN 311 METIS_TAC [normorder_noposn, relationTheory.RTC_RULES]); 312 313 314val normal_finds_bnf = store_thm( 315 "normal_finds_bnf", 316 ``M -��->* N /\ bnf N ��� M -n->* N``, 317 SRW_TAC [][] THEN 318 `���p. (first p = M) ��� finite p ��� (last p = N) ��� standard_reduction p` 319 by METIS_TAC [standardisation_theorem] THEN 320 METIS_TAC [standard_to_bnf_is_normal, finite_normorder_RTC]); 321 322val nstar_betastar = store_thm( 323 "nstar_betastar", 324 ``���M N. M -n->* N ��� M -��->* N``, 325 HO_MATCH_MP_TAC relationTheory.RTC_INDUCT THEN 326 METIS_TAC [relationTheory.RTC_RULES, normorder_ccbeta]); 327 328val nstar_lameq = store_thm( 329 "nstar_lameq", 330 ``���M N. M -n->* N ��� M == N``, 331 SRW_TAC [][nstar_betastar, betastar_lameq]); 332 333val nstar_betastar_bnf = store_thm( 334 "nstar_betastar_bnf", 335 ``bnf N ��� (M -n->* N ��� M -��->* N)``, 336 METIS_TAC [normal_finds_bnf, nstar_betastar]); 337 338 339val nstar_bnf_triangle = store_thm( 340 "nstar_bnf_triangle", 341 ``���M N. M -n->* N ��� 342 bnf N ��� ���M'. M -n->* M' ��� M' -n->* N``, 343 HO_MATCH_MP_TAC relationTheory.RTC_STRONG_INDUCT THEN SRW_TAC [][] THENL [ 344 METIS_TAC [relationTheory.RTC_RULES, bnf_reduction_to_self, 345 nstar_betastar], 346 POP_ASSUM MP_TAC THEN REWRITE_TAC [Once relationTheory.RTC_CASES1] THEN 347 STRIP_TAC THENL [ 348 METIS_TAC [relationTheory.RTC_RULES], 349 METIS_TAC [normorder_det] 350 ] 351 ]); 352 353 354 355val normstar_LAM = store_thm( 356 "normstar_LAM", 357 ``���M N. LAM x M -n->* LAM x N ��� M -n->* N``, 358 SIMP_TAC (srw_ss()) [EQ_IMP_THM, FORALL_AND_THM] THEN CONJ_TAC THENL [ 359 Q_TAC SUFF_TAC `���M N. M -n->* N ��� 360 ���v M0 N0. (M = LAM v M0) ��� (N = LAM v N0) ��� 361 M0 -n->* N0` THEN1 METIS_TAC [] THEN 362 HO_MATCH_MP_TAC relationTheory.RTC_INDUCT THEN 363 SIMP_TAC (srw_ss() ++ DNF_ss) [normorder_rwts] THEN 364 METIS_TAC [relationTheory.RTC_RULES], 365 366 HO_MATCH_MP_TAC relationTheory.RTC_INDUCT THEN 367 SRW_TAC [][] THEN 368 METIS_TAC [normorder_rules, relationTheory.RTC_RULES] 369 ]); 370val _ = export_rewrites ["normstar_LAM"] 371 372val normstar_APPr = store_thm( 373 "normstar_APPr", 374 ``bnf M ��� ��is_abs M ��� 375 (M @@ N -n->* P ��� ���N'. (P = M @@ N') ��� N -n->* N')``, 376 SIMP_TAC (srw_ss() ++ DNF_ss) [EQ_IMP_THM] THEN CONJ_TAC THENL [ 377 Q_TAC SUFF_TAC `���M��� P. M��� -n->* P ��� 378 ���M N. (M��� = M @@ N) ��� bnf M ��� ��is_abs M ��� 379 ���N'. (P = M @@ N') ��� N -n->* N'` 380 THEN1 METIS_TAC [] THEN 381 HO_MATCH_MP_TAC relationTheory.RTC_INDUCT THEN 382 SRW_TAC [][] THEN FULL_SIMP_TAC (srw_ss()) [normorder_rwts] THEN 383 SRW_TAC [][] THEN FULL_SIMP_TAC (srw_ss()) [] THENL [ 384 METIS_TAC [relationTheory.RTC_RULES], 385 METIS_TAC [normorder_bnf] 386 ], 387 388 Q_TAC SUFF_TAC `���N N'. N -n->* N' ��� 389 ���M. bnf M ��� ��is_abs M ��� M @@ N -n->* M @@ N'` 390 THEN1 METIS_TAC [] THEN 391 HO_MATCH_MP_TAC relationTheory.RTC_INDUCT THEN 392 METIS_TAC [normorder_rules, relationTheory.RTC_RULES] 393 ]); 394 395(* ---------------------------------------------------------------------- 396 -n->* congruences 397 ---------------------------------------------------------------------- *) 398 399val nstar_LAM_I = store_thm( 400 "nstar_LAM_I", 401 ``M -n->* N ��� LAM v M -n->* LAM v N``, 402 SRW_TAC [][]); 403 404val normstar_APPr_I = store_thm( 405 "normstar_APPr_I", 406 ``bnf M ��� ��is_abs M ��� N -n->* N' ��� M @@ N -n->* M @@ N'``, 407 SRW_TAC [][normstar_APPr]); 408 409(* ---------------------------------------------------------------------- 410 Calculating normal order reducts 411 ---------------------------------------------------------------------- *) 412 413val noreduct_def = Define` 414 noreduct t = if bnf t then NONE else SOME (@t'. t -n-> t') 415`; 416 417val noreduct_thm = store_thm( 418 "noreduct_thm", 419 ``(noreduct (LAM v M) = OPTION_MAP (LAM v) (noreduct M)) ��� 420 (noreduct (LAM v M @@ N) = SOME ([N/v]M)) ��� 421 (��is_abs M ��� (noreduct (M @@ N) = 422 if bnf M then OPTION_MAP (APP M) (noreduct N) 423 else OPTION_MAP (��M'. M' @@ N) (noreduct M))) ��� 424 (noreduct (VAR s) = NONE)``, 425 SRW_TAC [][noreduct_def] THENL [ 426 SRW_TAC [][normorder_rwts] THEN 427 `���N. M -n-> N` by METIS_TAC [normorder_bnf] THEN 428 `���N'. M -n-> N' ��� (N' = N)` by METIS_TAC [normorder_det] THEN 429 SRW_TAC [][], 430 431 SRW_TAC [][normorder_rwts], 432 FULL_SIMP_TAC (srw_ss()) [], 433 434 SRW_TAC [][normorder_rwts] THEN 435 `(���N. M -n-> N ��� F) ��� ���N'. N -n-> N'` by METIS_TAC [normorder_bnf] THEN 436 SRW_TAC [][] THEN 437 `���N���. N -n-> N��� ��� (N��� = N')` by METIS_TAC [normorder_det] THEN 438 SRW_TAC [][], 439 440 SRW_TAC [][normorder_rwts] THEN 441 `���M'. M -n-> M'` by METIS_TAC [normorder_bnf] THEN 442 `���M���. M -n-> M��� ��� (M��� = M')` by METIS_TAC [normorder_det] THEN 443 SRW_TAC [][] 444 ]); 445 446val noreduct_Yf = Store_thm( 447 "noreduct_Yf", 448 ``(noreduct (Yf f) = SOME (f @@ Yf f)) ��� 449 (noreduct (Yf f @@ x) = SOME (f @@ Yf f @@ x))``, 450 Q_TAC (NEW_TAC "z") `FV f` THEN 451 `Yf f = LAM z (f @@ (VAR z @@ VAR z)) @@ LAM z (f @@ (VAR z @@ VAR z))` 452 by SRW_TAC [][chap2Theory.Yf_fresh] THEN 453 SRW_TAC [][noreduct_thm, termTheory.lemma14b]); 454 455val noreduct_characterisation = store_thm( 456 "noreduct_characterisation", 457 ``M -n-> N ��� (noreduct M = SOME N)``, 458 SRW_TAC [][noreduct_def] THEN Cases_on `bnf M` THEN SRW_TAC [][] THENL [ 459 METIS_TAC [normorder_bnf], 460 `���N���. M -n-> N���` by METIS_TAC [normorder_bnf] THEN 461 `���N���. M -n-> N��� ��� (N��� = N���)` by METIS_TAC [normorder_det] THEN 462 SRW_TAC [][] THEN METIS_TAC [] 463 ]); 464 465val noreduct_bnf = store_thm( 466 "noreduct_bnf", 467 ``(noreduct M = NONE) = bnf M``, 468 SRW_TAC [][noreduct_def]); 469 470 471val noreduct_vsubst = store_thm( 472 "noreduct_vsubst", 473 ``���t. noreduct ([VAR v/u] t) = OPTION_MAP (SUB (VAR v) u) (noreduct t)``, 474 HO_MATCH_MP_TAC nc_INDUCTION2 THEN Q.EXISTS_TAC `{u;v}` THEN 475 SRW_TAC [][noreduct_thm, SUB_VAR] THENL [ 476 Cases_on `is_abs t` THENL [ 477 `���z t0. (t = LAM z t0) ��� z ��� u ��� z ��� v` 478 by (Q.SPEC_THEN `t` FULL_STRUCT_CASES_TAC term_CASES THEN 479 FULL_SIMP_TAC (srw_ss()) [] THEN 480 SRW_TAC [boolSimps.DNF_ss][LAM_eq_thm, tpm_eqr] THEN 481 DISJ2_TAC THEN 482 Q_TAC (NEW_TAC "z") `{v';u;v} ��� FV t0` THEN METIS_TAC []) THEN 483 SRW_TAC [][noreduct_thm] THEN 484 SRW_TAC [][GSYM chap2Theory.substitution_lemma], 485 486 SRW_TAC [][noreduct_thm] THENL [ 487 Cases_on `noreduct t'` THEN SRW_TAC [][], 488 Cases_on `noreduct t` THEN SRW_TAC [][] 489 ] 490 ], 491 492 Cases_on `noreduct t` THEN SRW_TAC [][] 493 ]); 494 495val noreduct_tpm = store_thm( 496 "noreduct_tpm", 497 ``���t. noreduct (tpm �� t) = OPTION_MAP (tpm ��) (noreduct t)``, 498 HO_MATCH_MP_TAC simple_induction THEN 499 SRW_TAC [][noreduct_thm] THENL [ 500 Cases_on `is_abs t` THENL [ 501 `���z t0. t = LAM z t0` 502 by (Q.SPEC_THEN `t` FULL_STRUCT_CASES_TAC term_CASES THEN 503 FULL_SIMP_TAC (srw_ss()) [] THEN METIS_TAC []) THEN 504 SRW_TAC [][noreduct_thm, tpm_subst], 505 506 SRW_TAC [][noreduct_thm] THENL [ 507 Cases_on `noreduct t'` THEN SRW_TAC [][], 508 Cases_on `noreduct t` THEN SRW_TAC [][] 509 ] 510 ], 511 512 Cases_on `noreduct t` THEN SRW_TAC [][] 513 ]); 514 515 516val noredAPP' = store_thm( 517 "noredAPP'", 518 ``~is_abs M ==> (noreduct (M @@ N) = 519 case noreduct M of 520 NONE => OPTION_MAP (APP M) (noreduct N) 521 | SOME M' => SOME (M' @@ N))``, 522 SRW_TAC [][noreduct_thm, GSYM noreduct_bnf] THEN 523 Cases_on `noreduct M` THEN FULL_SIMP_TAC (srw_ss()) []); 524 525val _ = overload_on ("upcons", ``��x y. pcons x () y``) 526 527 528 529val pair_case_unit = prove( 530 ``pair_CASE v (f : unit -> 'a -> 'b) = f () (SND v)``, 531 Cases_on `v` THEN SRW_TAC [][oneTheory.one]); 532 533val option_case_unit = prove( 534 ``option_CASE (OPTION_MAP ($, ()) x) n (f : unit # 'a -> 'b) = 535 option_CASE x n (��x. f ((), x))``, 536 Cases_on `x` THEN SRW_TAC [][]); 537 538val nopath_def = new_specification( 539 "nopath_def", 540 ["nopath"], 541 path_Axiom |> ISPEC ``��M. (M, OPTION_MAP ((,) ()) (noreduct M))`` 542 |> SIMP_RULE (srw_ss()) [oneTheory.one, pair_case_unit, 543 option_case_unit]); 544 545val first_nopath = Store_thm( 546 "first_nopath", 547 ``first (nopath M) = M``, 548 ONCE_REWRITE_TAC [nopath_def] THEN Cases_on `noreduct M` THEN 549 SRW_TAC [][]); 550 551val mem_nopath = Store_thm( 552 "mem_nopath", 553 ``mem M (nopath M)``, 554 ONCE_REWRITE_TAC [nopath_def] THEN Cases_on `noreduct M` THEN 555 SRW_TAC [][]); 556 557val mem_nopath_expanded = Store_thm( 558 "mem_nopath_expanded", 559 ``mem M (case v of NONE => stopped_at M 560 | SOME y => pcons M l (f y))``, 561 Cases_on `v` THEN SRW_TAC [][]); 562 563val nopath_okpath = store_thm( 564 "nopath_okpath", 565 ``okpath (��M u N. M -n-> N) (nopath M)``, 566 Q_TAC SUFF_TAC `���p. (���M. p = nopath M) ��� okpath (��M u N. M -n-> N) p` 567 THEN1 METIS_TAC [] THEN 568 HO_MATCH_MP_TAC okpath_co_ind THEN REPEAT GEN_TAC THEN 569 CONV_TAC (LAND_CONV (ONCE_REWRITE_CONV [nopath_def])) THEN 570 CONV_TAC LEFT_IMP_EXISTS_CONV THEN GEN_TAC THEN 571 Cases_on `noreduct M'` THEN SRW_TAC [][] THEN 572 METIS_TAC [noreduct_characterisation]); 573 574val option_case_CONG = store_thm( 575 "option_case_CONG", 576 ``(x = x') ��� (option_CASE x n f = option_CASE x' n f)``, 577 SRW_TAC [][]); 578 579val normstar_nopath = store_thm( 580 "normstar_nopath", 581 ``M -n->* N ��� mem N (nopath M)``, 582 EQ_TAC THENL [ 583 Q_TAC SUFF_TAC `���M N. M -n->* N ��� mem N (nopath M)` THEN1 METIS_TAC []THEN 584 HO_MATCH_MP_TAC relationTheory.RTC_INDUCT THEN SRW_TAC [][] THEN 585 FULL_SIMP_TAC (srw_ss()) [noreduct_characterisation, 586 nopath_def, Cong option_case_CONG], 587 588 SIMP_TAC (srw_ss())[mem_def, GSYM LEFT_FORALL_IMP_THM] THEN 589 Q.ID_SPEC_TAC `N` THEN Q.ID_SPEC_TAC `M` THEN 590 SIMP_TAC (srw_ss()) [] THEN Induct_on`i` THEN SRW_TAC [][] THEN 591 Q.SPEC_THEN `M` ASSUME_TAC nopath_def THEN 592 POP_ASSUM SUBST_ALL_TAC THEN 593 Cases_on `noreduct M` THEN 594 FULL_SIMP_TAC (srw_ss()) [] THEN 595 METIS_TAC [relationTheory.RTC_RULES, noreduct_characterisation] 596 ]); 597 598val bnf_posn_is_length = store_thm( 599 "bnf_posn_is_length", 600 ``���i M. i ��� PL (nopath M) ��� bnf (el i (nopath M)) ��� 601 (length (nopath M) = SOME (i + 1))``, 602 Induct THEN SRW_TAC [][] THENL [ 603 ONCE_REWRITE_TAC [nopath_def] THEN 604 `noreduct M = NONE` by METIS_TAC [noreduct_bnf] THEN 605 SRW_TAC [][length_thm], 606 607 Q.SPEC_THEN `M` SUBST_ALL_TAC nopath_def THEN 608 Cases_on `noreduct M` THEN FULL_SIMP_TAC (srw_ss()) [] THEN 609 `length (nopath x) = SOME (i + 1)` by METIS_TAC [] THEN 610 `finite (nopath x)` by METIS_TAC [finite_length] THEN 611 SRW_TAC [][length_thm, arithmeticTheory.ADD1] 612 ]); 613 614val has_bnf_finite_nopath = store_thm( 615 "has_bnf_finite_nopath", 616 ``has_bnf M ��� finite (nopath M)``, 617 SRW_TAC [][has_bnf_thm, EQ_IMP_THM] THENL [ 618 `M -n->* N` by METIS_TAC [nstar_betastar_bnf] THEN 619 `mem N (nopath M)` by METIS_TAC [normstar_nopath] THEN 620 `���i. i ��� PL (nopath M) ��� (el i (nopath M) = N)` 621 by METIS_TAC [mem_def] THEN 622 `length (nopath M) = SOME (i + 1)` 623 by METIS_TAC [bnf_posn_is_length] THEN 624 METIS_TAC [finite_length], 625 626 POP_ASSUM MP_TAC THEN 627 Q_TAC SUFF_TAC 628 `���p. finite p ��� ���M. (p = nopath M) ��� ���N. M -��->* N ��� bnf N` 629 THEN1 METIS_TAC [] THEN 630 HO_MATCH_MP_TAC finite_path_ind THEN SRW_TAC [][] THENL [ 631 Q.SPEC_THEN `M` SUBST_ALL_TAC nopath_def THEN 632 Cases_on `noreduct M` THEN FULL_SIMP_TAC (srw_ss()) [] THEN 633 METIS_TAC [noreduct_bnf, relationTheory.RTC_RULES], 634 635 Q.SPEC_THEN `M` SUBST_ALL_TAC nopath_def THEN 636 Cases_on `noreduct M` THEN FULL_SIMP_TAC (srw_ss()) [] THEN 637 SRW_TAC [][] THEN 638 METIS_TAC [normorder_ccbeta, noreduct_characterisation, 639 relationTheory.RTC_RULES] 640 ] 641 ]); 642 643val nopath_el = store_thm( 644 "nopath_el", 645 ``���i M. i ��� PL (nopath M) ��� 646 (nopath (el i (nopath M)) = drop i (nopath M))``, 647 Induct THEN SRW_TAC [][] THEN 648 POP_ASSUM MP_TAC THEN 649 Q.SPEC_THEN `M` ASSUME_TAC nopath_def THEN 650 POP_ASSUM (fn th => REWRITE_TAC [th]) THEN 651 Cases_on `noreduct M` THEN SRW_TAC [][]); 652 653val nopath_smaller = store_thm( 654 "nopath_smaller", 655 ``���M N. M -n->* N ��� 656 M ��� N ��� finite (nopath M) ��� 657 THE (length (nopath N)) < THE (length (nopath M))``, 658 REPEAT STRIP_TAC THEN 659 `mem N (nopath M)` by METIS_TAC [normstar_nopath] THEN 660 `���i. i ��� PL (nopath M) ��� (N = el i (nopath M))` 661 by METIS_TAC [mem_def] THEN 662 `0 < i` 663 by (SPOSE_NOT_THEN ASSUME_TAC THEN 664 `i = 0` by DECIDE_TAC THEN 665 FULL_SIMP_TAC (srw_ss()) []) THEN 666 Q_TAC SUFF_TAC `nopath N = drop i (nopath M)` THEN1 667 (SRW_TAC [][] THEN 668 `���m. (length (nopath M) = SOME m) ��� m ��� 0` 669 by METIS_TAC [finite_length, 670 length_never_zero] THEN 671 SRW_TAC [ARITH_ss][length_drop]) THEN 672 SRW_TAC [][nopath_el]); 673 674 675val Omega_def = chap2Theory.Omega_def 676val noreduct_omega = Store_thm( 677 "noreduct_omega", 678 ``noreduct �� = SOME ��``, 679 SRW_TAC [][noreduct_thm, Omega_def]); 680 681val Omega_loops = store_thm( 682 "Omega_loops", 683 ``�� -n-> ��``, 684 SRW_TAC [][noreduct_characterisation] THEN 685 SRW_TAC [][noreduct_thm, Omega_def]); 686 687val Omega_path_infinite = store_thm( 688 "Omega_path_infinite", 689 ``��finite (nopath ��)``, 690 Q_TAC SUFF_TAC `���p. finite p ��� p ��� nopath ��` THEN1 METIS_TAC [] THEN 691 HO_MATCH_MP_TAC finite_path_ind THEN SRW_TAC [][] THEN 692 ONCE_REWRITE_TAC [nopath_def] THEN SRW_TAC [][]); 693 694 695val Omega_has_no_bnf = Store_thm( 696 "Omega_has_no_bnf", 697 ``��has_bnf ��``, 698 SRW_TAC [][has_bnf_finite_nopath, Omega_path_infinite]); 699 700val last_of_finite_nopath = store_thm( 701 "last_of_finite_nopath", 702 ``finite (nopath M) ��� bnf (last (nopath M))``, 703 Q_TAC SUFF_TAC 704 `���p. finite p ��� ���M. (nopath M = p) ��� bnf (last (nopath M))` 705 THEN1 METIS_TAC [] THEN 706 HO_MATCH_MP_TAC finite_path_ind THEN SRW_TAC [][] THENL [ 707 Q.SPEC_THEN `M` ASSUME_TAC nopath_def THEN 708 Cases_on `noreduct M` THEN FULL_SIMP_TAC (srw_ss()) [noreduct_bnf] THEN 709 SRW_TAC [][], 710 711 Q.SPEC_THEN `M` ASSUME_TAC nopath_def THEN 712 Cases_on `noreduct M` THEN FULL_SIMP_TAC (srw_ss()) [] THEN 713 SRW_TAC [][] THEN METIS_TAC [] 714 ]); 715 716 717(* ---------------------------------------------------------------------- 718 bnf_of : term -> term option 719 720 "Calculating" the ��-normal form of a term (if it exists) with a while 721 loop. 722 ---------------------------------------------------------------------- *) 723 724val bnf_of_def = Define` 725 bnf_of M = OWHILE ((~) o bnf) (THE o noreduct) M 726`; 727 728val lemma1 = prove( 729 ``���p. okpath (��M u N. M -n-> N) p ��� finite p ��� 730 bnf (last p) ��� (bnf_of (first p) = SOME (last p))``, 731 HO_MATCH_MP_TAC finite_okpath_ind THEN SRW_TAC [][] THENL [ 732 SRW_TAC [][Once whileTheory.OWHILE_THM, bnf_of_def], 733 FULL_SIMP_TAC (srw_ss()) [] THEN 734 SRW_TAC [][Once whileTheory.OWHILE_THM, bnf_of_def] THENL [ 735 SRW_TAC [][GSYM bnf_of_def] THEN 736 METIS_TAC [noreduct_characterisation, optionTheory.THE_DEF], 737 METIS_TAC [normorder_bnf] 738 ] 739 ]); 740 741val lemma2 = prove( 742 ``���N. (OWHILE ($~ o bnf) (THE o noreduct) M = SOME N) ��� 743 M -n->* N``, 744 HO_MATCH_MP_TAC whileTheory.OWHILE_INV_IND THEN SRW_TAC [][] THEN 745 Cases_on `noreduct N` THENL [ 746 FULL_SIMP_TAC (srw_ss()) [noreduct_bnf], 747 METIS_TAC [noreduct_characterisation, relationTheory.RTC_RULES_RIGHT1, 748 optionTheory.THE_DEF] 749 ]); 750 751val bnf_of_SOME = store_thm( 752 "bnf_of_SOME", 753 ``(bnf_of M = SOME N) ��� M -n->* N ��� bnf N``, 754 SRW_TAC [][bnf_of_def] THEN 755 IMP_RES_TAC whileTheory.OWHILE_ENDCOND THEN 756 FULL_SIMP_TAC (srw_ss()) [] THEN 757 METIS_TAC [lemma2]); 758 759val has_bnf_of = store_thm( 760 "has_bnf_of", 761 ``has_bnf M ��� ���N. bnf_of M = SOME N``, 762 EQ_TAC THENL [ 763 SRW_TAC [][has_bnf_finite_nopath] THEN 764 ASSUME_TAC nopath_okpath THEN 765 METIS_TAC [lemma1, last_of_finite_nopath, first_nopath], 766 767 METIS_TAC [chap2Theory.has_bnf_def, bnf_of_SOME, nstar_lameq] 768 ]); 769 770val bnf_of_NONE = store_thm( 771 "bnf_of_NONE", 772 ``(bnf_of M = NONE) ��� ��has_bnf M``, 773 REWRITE_TAC [has_bnf_of] THEN 774 Cases_on `bnf_of M` THEN SRW_TAC [][]); 775 776val bnf_of_thm = store_thm( 777 "bnf_of_thm", 778 ``bnf_of M = if bnf M then SOME M else bnf_of (THE (noreduct M))``, 779 SRW_TAC [][bnf_of_def] THEN1 780 SRW_TAC [][Once whileTheory.OWHILE_THM] THEN 781 SRW_TAC [][SimpLHS, Once whileTheory.OWHILE_THM]); 782 783val nstar_bnf_of_SOME_I = store_thm( 784 "nstar_bnf_of_SOME_I", 785 ``M -n->* N ��� bnf N ��� (bnf_of M = SOME N)``, 786 Q_TAC SUFF_TAC `���M N. M -n->* N ��� bnf N ��� (bnf_of M = SOME N)` 787 THEN1 METIS_TAC [] THEN 788 HO_MATCH_MP_TAC relationTheory.RTC_INDUCT THEN SRW_TAC [][] THEN 789 SRW_TAC [][Once bnf_of_thm] THEN1 METIS_TAC [normorder_bnf] THEN 790 FULL_SIMP_TAC (srw_ss()) [noreduct_characterisation]); 791 792val betastar_bnf_of_SOME_I = store_thm( 793 "betastar_bnf_of_SOME_I", 794 ``M -��->* N ��� bnf N ��� (bnf_of M = SOME N)``, 795 METIS_TAC [nstar_bnf_of_SOME_I, normal_finds_bnf]); 796 797val lameq_bnf_of_SOME_I = store_thm( 798 "lameq_bnf_of_SOME_I", 799 ``M == N ��� bnf N ��� (bnf_of M = SOME N)``, 800 METIS_TAC [betastar_bnf_of_SOME_I, betastar_lameq_bnf]); 801 802val lameq_bnf_of_cong = store_thm( 803 "lameq_bnf_of_cong", 804 ``M == N ��� (bnf_of M = bnf_of N)``, 805 Cases_on `bnf_of N` THENL [ 806 FULL_SIMP_TAC (srw_ss()) [bnf_of_NONE, chap2Theory.has_bnf_def] THEN 807 METIS_TAC [chap2Theory.lameq_rules], 808 IMP_RES_TAC bnf_of_SOME THEN STRIP_TAC THEN 809 `M == x` by METIS_TAC [chap2Theory.lameq_rules, nstar_lameq] THEN 810 METIS_TAC [lameq_bnf_of_SOME_I] 811 ]); 812 813val lameq_has_bnf_cong = store_thm( 814 "lameq_has_bnf_cong", 815 ``M == N ��� (has_bnf M = has_bnf N)``, 816 SRW_TAC [][has_bnf_of] THEN 817 METIS_TAC [lameq_bnf_of_cong, chap2Theory.lameq_rules]); 818 819val bnf_bnf_of = store_thm( 820 "bnf_bnf_of", 821 ``bnf M ��� (bnf_of M = SOME M)``, 822 SRW_TAC [][Once bnf_of_thm]); 823 824val bnf_of_Omega = Store_thm( 825 "bnf_of_Omega", 826 ``bnf_of �� = NONE``, 827 METIS_TAC [Omega_has_no_bnf, bnf_of_NONE]); 828 829(* ---------------------------------------------------------------------- 830 weak head reduction gives a congruence rule for -n->* of sorts 831 ---------------------------------------------------------------------- *) 832 833open head_reductionTheory 834val head_normorder = store_thm( 835 "head_normorder", 836 ``���M N. M -h-> N ��� M -n-> N``, 837 HO_MATCH_MP_TAC hreduce1_ind THEN 838 SRW_TAC [][normorder_rules]); 839 840val whstar_nstar = store_thm( 841 "whstar_nstar", 842 ``���M N. M -w->* N ��� M -n->* N``, 843 HO_MATCH_MP_TAC relationTheory.RTC_INDUCT THEN 844 METIS_TAC [relationTheory.RTC_RULES, wh_head, head_normorder]); 845 846val whead_normorder = store_thm( 847 "whead_normorder", 848 ``���M N. M -w-> N ��� M -n-> N``, 849 METIS_TAC [wh_head, head_normorder]); 850 851val whead_norm_congL = store_thm( 852 "whead_norm_congL", 853 ``���M��� M���. M��� -w->* M��� ��� ���N. M��� @@ N -n->* M��� @@ N``, 854 HO_MATCH_MP_TAC relationTheory.RTC_INDUCT_RIGHT1 THEN SRW_TAC [][] THEN 855 MATCH_MP_TAC (CONJUNCT2 (SPEC_ALL relationTheory.RTC_RULES_RIGHT1)) THEN 856 Q.EXISTS_TAC `M��� @@ N` THEN SRW_TAC [][] THEN 857 IMP_RES_TAC whead_normorder THEN 858 IMP_RES_TAC wh_is_abs THEN 859 SRW_TAC [][normorder_rules]); 860 861val normwhnf_is_abs_rpreserved = store_thm( 862 "normwhnf_is_abs_rpreserved", 863 ``���M N. M -n-> N ��� whnf M ��� is_abs N ��� is_abs M``, 864 HO_MATCH_MP_TAC normorder_ind THEN SRW_TAC [][]); 865 866 867val whnf_is_abs_appstr = store_thm( 868 "whnf_is_abs_appstr", 869 ``���t. whnf t ��� is_abs t ��� ���v args. t = VAR v ���� args``, 870 HO_MATCH_MP_TAC simple_induction THEN SRW_TAC [][] THENL [ 871 MAP_EVERY Q.EXISTS_TAC [`s`, `[]`] THEN SRW_TAC [][], 872 SRW_TAC [][EQ_IMP_THM] THENL [ 873 MAP_EVERY Q.EXISTS_TAC [`v`, `args ++ [t']`] THEN 874 SRW_TAC [][rich_listTheory.FOLDL_APPEND], 875 876 FULL_SIMP_TAC (srw_ss()) [app_eq_varappstar] THEN 877 Q.SPEC_THEN `VAR v ���� FRONT args` MP_TAC term_CASES THEN 878 STRIP_TAC THEN SRW_TAC [][] THEN 879 FULL_SIMP_TAC (srw_ss()) [lam_eq_appstar], 880 881 FULL_SIMP_TAC (srw_ss()) [app_eq_varappstar] THEN METIS_TAC [] 882 ] 883 ]); 884 885val normorder_strong_ind = 886 IndDefLib.derive_strong_induction (normorder_rules,normorder_ind) 887 888Theorem bnf_appstar[simp]: 889 ���args f. 890 bnf (f ���� args) ��� bnf f ��� EVERY bnf args ��� (is_abs f ��� (args = [])) 891Proof Induct THEN SRW_TAC [][] THEN METIS_TAC [] 892QED 893 894val norm_varhead0 = prove( 895 ``���M N. M -n-> N ��� 896 ���v Ms. (M = VAR v ���� Ms) ��� 897 ���p s M0 N0. 898 (Ms = p ++ [M0] ++ s) ��� 899 (N = VAR v ���� (p ++ [N0] ++ s)) ��� 900 EVERY bnf p ��� 901 M0 -n-> N0``, 902 HO_MATCH_MP_TAC normorder_strong_ind THEN 903 SRW_TAC [][lam_eq_appstar, app_eq_varappstar] THENL [ 904 FIRST_X_ASSUM (Q.SPECL_THEN [`v`, `FRONT Ms`] MP_TAC) THEN 905 SRW_TAC [][] THEN 906 MAP_EVERY Q.EXISTS_TAC [`p`, `s ++ [LAST Ms]`, `M0`, `N0`] THEN 907 SRW_TAC [][rich_listTheory.FRONT_APPEND, listTheory.FRONT_DEF, 908 rich_listTheory.LAST_APPEND, listTheory.LAST_DEF] THEN 909 IMP_RES_TAC listTheory.APPEND_FRONT_LAST THEN 910 POP_ASSUM (fn th => REWRITE_TAC [Once (GSYM th)]) THEN 911 SRW_TAC [][] THEN 912 REWRITE_TAC [GSYM listTheory.APPEND_ASSOC, listTheory.APPEND], 913 914 MAP_EVERY Q.EXISTS_TAC [`FRONT Ms`, `[]`, `LAST Ms`, `N`] THEN 915 SRW_TAC [][listTheory.APPEND_FRONT_LAST, rich_listTheory.FRONT_APPEND, 916 rich_listTheory.LAST_APPEND] THEN 917 FULL_SIMP_TAC (srw_ss()) [] 918 ]); 919 920val norm_varhead = save_thm( 921 "norm_varhead", 922 SIMP_RULE (srw_ss() ++ DNF_ss) [] norm_varhead0); 923 924val normstar_varhead0 = prove( 925 ``���M N. M -n->* N ��� 926 ���v Ms. (M = VAR v ���� Ms) ��� 927 ���Ns. (N = VAR v ���� Ns) ��� (LENGTH Ns = LENGTH Ms) ��� 928 ���i. i < LENGTH Ms ��� EL i Ms -n->* EL i Ns``, 929 HO_MATCH_MP_TAC relationTheory.RTC_STRONG_INDUCT THEN SRW_TAC [][] THEN 930 `���p s M0 N0. (Ms = p ++ [M0] ++ s) ��� 931 (M' = VAR v ���� (p ++ [N0] ++ s)) ��� 932 M0 -n-> N0` 933 by METIS_TAC [norm_varhead] THEN 934 `���Ns. (N = VAR v ���� Ns) ��� (LENGTH Ns = LENGTH (p ++ [N0] ++ s)) ��� 935 ���i. i < LENGTH (p ++ [N0] ++ s) ��� EL i (p ++ [N0] ++ s) -n->* EL i Ns` 936 by METIS_TAC [] THEN 937 Q.EXISTS_TAC `Ns` THEN SRW_TAC [][] THEN 938 Cases_on `i < LENGTH p` THEN1 939 (SRW_TAC [ARITH_ss][rich_listTheory.EL_APPEND1] THEN 940 FIRST_X_ASSUM (Q.SPEC_THEN `i` MP_TAC) THEN 941 SRW_TAC [ARITH_ss][rich_listTheory.EL_APPEND1]) THEN 942 Cases_on `i = LENGTH p` THENL [ 943 FIRST_X_ASSUM (Q.SPEC_THEN `LENGTH p` MP_TAC) THEN 944 SRW_TAC [ARITH_ss][rich_listTheory.EL_APPEND2, 945 rich_listTheory.EL_APPEND1] THEN 946 METIS_TAC [relationTheory.RTC_RULES], 947 FIRST_X_ASSUM (Q.SPEC_THEN `i` MP_TAC) THEN 948 ASM_SIMP_TAC (srw_ss() ++ ARITH_ss) [rich_listTheory.EL_APPEND2] 949 ]); 950 951val normstar_varhead = save_thm( 952 "normstar_varhead", 953 SIMP_RULE (srw_ss() ++ DNF_ss) [] normstar_varhead0); 954 955val normstar_to_abs_wstar0 = prove( 956 ``���M N. M -n->* N ��� 957 ���v N0. (N = LAM v N0) ��� v ��� FV M ��� 958 ���M0. M -w->* LAM v M0 ��� M0 -n->* N0``, 959 HO_MATCH_MP_TAC relationTheory.RTC_STRONG_INDUCT THEN SRW_TAC [][] THEN 960 Cases_on `whnf M` THENL [ 961 Cases_on `is_abs M` THENL [ 962 `���M0. M = LAM v M0` 963 by (Q.SPEC_THEN `M` FULL_STRUCT_CASES_TAC term_CASES THEN 964 FULL_SIMP_TAC (srw_ss()) [] THEN 965 SRW_TAC [DNF_ss][LAM_eq_thm, tpm_eqr] THEN METIS_TAC []) THEN 966 SRW_TAC [][] THEN FULL_SIMP_TAC (srw_ss()) [normorder_rwts] THEN 967 SRW_TAC [][] THEN FULL_SIMP_TAC (srw_ss()) [] THEN 968 METIS_TAC [relationTheory.RTC_RULES], 969 970 `���var args. LAM v N0 = VAR var ���� args` 971 by METIS_TAC [whnf_is_abs_appstr, normstar_varhead, 972 norm_varhead] THEN 973 FULL_SIMP_TAC (srw_ss()) [lam_eq_appstar] 974 ], 975 976 `���M���. M -w-> M���` by METIS_TAC [whnf_def] THEN 977 `M��� = M'` by METIS_TAC [wh_head, head_normorder, normorder_det] THEN 978 `v ��� FV M'` by METIS_TAC [normorder_FV] THEN 979 `���M'���. M' -w->* LAM v M'��� ��� M'��� -n->* N0` by METIS_TAC [] THEN 980 METIS_TAC [relationTheory.RTC_RULES] 981 ]); 982 983val normstar_to_abs_wstar = save_thm( 984 "normstar_to_abs_wstar", 985 SIMP_RULE (srw_ss() ++ DNF_ss) [AND_IMP_INTRO] normstar_to_abs_wstar0); 986 987val varappstar_not_is_abs = store_thm( 988 "varappstar_not_is_abs", 989 ``��is_abs (VAR v ���� a)``, 990 Q.SPEC_THEN `VAR v ���� a` STRIP_ASSUME_TAC term_CASES THEN SRW_TAC [][] THEN 991 FULL_SIMP_TAC (srw_ss()) [lam_eq_appstar]); 992 993val normorder_preserves_is_abs = store_thm( 994 "normorder_preserves_is_abs", 995 ``���M N. M -n-> N ��� is_abs M ��� is_abs N``, 996 HO_MATCH_MP_TAC normorder_ind THEN SRW_TAC [][]); 997val nstar_preserves_is_abs = store_thm( 998 "nstar_preserves_is_abs", 999 ``���M N. M -n->* N ��� is_abs M ��� is_abs N``, 1000 HO_MATCH_MP_TAC relationTheory.RTC_STRONG_INDUCT THEN 1001 METIS_TAC [relationTheory.RTC_RULES, normorder_preserves_is_abs]); 1002 1003 1004val normstar_to_vhead_wstar0 = prove( 1005 ``���M N. M -n->* N ��� 1006 ���f Ns. (N = VAR f ���� Ns) ��� 1007 ���Ms. M -w->* VAR f ���� Ms ��� 1008 (LENGTH Ms = LENGTH Ns) ��� 1009 ���i. i < LENGTH Ms ��� EL i Ms -n->* EL i Ns``, 1010 HO_MATCH_MP_TAC relationTheory.RTC_STRONG_INDUCT THEN SRW_TAC [][] THENL [ 1011 Q.EXISTS_TAC `Ns` THEN SRW_TAC [][], 1012 FULL_SIMP_TAC (srw_ss()) [] THEN Cases_on `whnf M` THENL [ 1013 `is_abs M ��� ���v M0s. M = VAR v ���� M0s` 1014 by METIS_TAC [whnf_is_abs_appstr] 1015 THEN1 1016 METIS_TAC [normorder_preserves_is_abs, nstar_preserves_is_abs, 1017 varappstar_not_is_abs] THEN 1018 `���Ns'. (VAR f ���� Ns = VAR v ���� Ns') ��� (LENGTH M0s = LENGTH Ns') ��� 1019 ���i. i < LENGTH Ns' ��� EL i M0s -n->* EL i Ns'` 1020 by METIS_TAC [normstar_varhead, relationTheory.RTC_RULES] THEN 1021 FULL_SIMP_TAC (srw_ss()) [] THEN METIS_TAC [relationTheory.RTC_RULES], 1022 1023 `���M''. M -w-> M''` by METIS_TAC [whnf_def] THEN 1024 `M'' = M'` by METIS_TAC [wh_head, head_normorder, normorder_det] THEN 1025 METIS_TAC [relationTheory.RTC_RULES] 1026 ] 1027 ]); 1028 1029val normstar_to_vhead_wstar = save_thm( 1030 "normstar_to_vhead_wstar", 1031 SIMP_RULE (srw_ss() ++ DNF_ss) [] normstar_to_vhead_wstar0); 1032 1033val leneq1 = prove( 1034 ``(LENGTH list = 1) ��� ���e. list = [e]``, 1035 Cases_on `list` THEN SRW_TAC [][listTheory.LENGTH_NIL]); 1036val leneq2 = prove( 1037 ``(LENGTH list = 2) ��� ���e��� e���. list = [e���; e���]``, 1038 Cases_on `list` THEN SRW_TAC [][leneq1]); 1039 1040val normstar_to_vheadnullary_wstar = save_thm( 1041 "normstar_to_vheadnullary_wstar", 1042 normstar_to_vhead_wstar 1043 |> SPEC_ALL |> Q.INST [`Ns` |-> `[]`] 1044 |> SIMP_RULE (srw_ss()) [listTheory.LENGTH_NIL]); 1045 1046val normstar_to_vheadunary_wstar = save_thm( 1047 "normstar_to_vheadunary_wstar", 1048 normstar_to_vhead_wstar 1049 |> SPEC_ALL |> Q.INST [`Ns` |-> `[N]`] 1050 |> SIMP_RULE (srw_ss() ++ DNF_ss) [leneq1, DECIDE ``x < 1 ��� (x = 0)``]); 1051 1052val normstar_to_vheadbinary_wstar = save_thm( 1053 "normstar_to_vheadbinary_wstar", 1054 normstar_to_vhead_wstar 1055 |> SPEC_ALL |> Q.INST [`Ns` |-> `[N���; N���]`] 1056 |> SIMP_RULE (srw_ss() ++ DNF_ss) 1057 [leneq2, DECIDE ``x < 2 ��� (x = 0) ��� (x = 1)``]); 1058 1059val _ = export_theory() 1060