1open HolKernel Parse boolLib bossLib 2 3open chap3Theory pred_setTheory termTheory boolSimps 4open nomsetTheory binderLib 5 6val _ = new_theory "head_reduction" 7 8val _ = ParseExtras.temp_loose_equality() 9 10fun Store_thm(trip as (n,t,tac)) = store_thm trip before export_rewrites [n] 11 12val _ = set_trace "Unicode" 1 13 14val (hreduce1_rules, hreduce1_ind, hreduce1_cases) = Hol_reln` 15 (���v M N. hreduce1 (LAM v M @@ N) ([N/v]M)) ��� 16 (���v M1 M2. hreduce1 M1 M2 ��� hreduce1 (LAM v M1) (LAM v M2)) ��� 17 (���M1 M2 N. hreduce1 M1 M2 ��� ��is_abs M1 ��� hreduce1 (M1 @@ N) (M2 @@ N)) 18`; 19 20val _ = set_fixity "-h->" (Infix(NONASSOC, 450)) 21val _ = overload_on ("-h->", ``hreduce1``) 22 23val _ = set_fixity "-h->*" (Infix(NONASSOC, 450)) 24val _ = overload_on ("-h->*", ``hreduce1^*``) 25 26val hreduce_ccbeta = store_thm( 27 "hreduce_ccbeta", 28 ``���M N. M -h-> N ��� M -��-> N``, 29 HO_MATCH_MP_TAC hreduce1_ind THEN SRW_TAC [][cc_beta_thm] THEN 30 METIS_TAC []); 31 32val hreduce1_FV = store_thm( 33 "hreduce1_FV", 34 ``���M N. M -h-> N ��� ���v. v ��� FV N ��� v ��� FV M``, 35 METIS_TAC [SUBSET_DEF, hreduce_ccbeta, cc_beta_FV_SUBSET]); 36 37 38val _ = temp_add_rule {block_style = (AroundEachPhrase, (PP.INCONSISTENT,2)), 39 fixity = Infix(NONASSOC, 950), 40 paren_style = OnlyIfNecessary, 41 pp_elements = [TOK "��", BreakSpace(0,0)], 42 term_name = "apply_perm"} 43val _ = temp_overload_on ("apply_perm", ``��p M. tpm [p] M``) 44val _ = temp_overload_on ("apply_perm", ``tpm``) 45val _ = temp_overload_on ("#", ``��v t. v ��� FV t``) 46val _ = temp_set_fixity "#" (Infix(NONASSOC, 450)) 47 48val tpm_hreduce_I = store_thm( 49 "tpm_hreduce_I", 50 ``���M N. M -h-> N ��� �����. ����M -h-> ����N``, 51 HO_MATCH_MP_TAC hreduce1_ind THEN SRW_TAC [][tpm_subst, hreduce1_rules]); 52 53val tpm_hreduce = store_thm( 54 "tpm_hreduce", 55 ``���M N ��. ����M -h-> ����N ��� M -h-> N``, 56 METIS_TAC [pmact_inverse, tpm_hreduce_I]); 57 58val hreduce1_rwts = store_thm( 59 "hreduce1_rwts", 60 ``(VAR s -h-> M ��� F) ��� 61 (��is_abs M ��� (M @@ N -h-> P ��� ���M'. (P = M' @@ N) ��� M -h-> M')) ��� 62 (LAM v M -h-> N ��� ���M'. (N = LAM v M') ��� M -h-> M') ��� 63 (LAM v M @@ N -h-> P ��� (P = [N/v]M))``, 64 REPEAT STRIP_TAC THENL [ 65 SRW_TAC [][Once hreduce1_cases], 66 CONV_TAC (LAND_CONV (ONCE_REWRITE_CONV [hreduce1_cases])) THEN 67 SRW_TAC [][] THEN 68 Q_TAC SUFF_TAC `���v N. M ��� LAM v N` THEN1 METIS_TAC [] THEN 69 SPOSE_NOT_THEN STRIP_ASSUME_TAC THEN 70 FULL_SIMP_TAC (srw_ss()) [], 71 CONV_TAC (LAND_CONV (ONCE_REWRITE_CONV [hreduce1_cases])) THEN 72 SRW_TAC [DNF_ss][LAM_eq_thm, tpm_eqr] THEN EQ_TAC THEN 73 SRW_TAC [][] THEN1 SRW_TAC [][] THEN 74 Q.EXISTS_TAC `(v,v')��M2` THEN 75 SRW_TAC [][] THENL [ 76 `v # (v,v')��M` by SRW_TAC [][] THEN 77 `v # M2` by METIS_TAC [hreduce1_FV] THEN 78 SRW_TAC [][GSYM tpm_ALPHA], 79 80 METIS_TAC [pmact_sing_inv, tpm_hreduce_I] 81 ], 82 83 SRW_TAC [DNF_ss][Once hreduce1_cases, LAM_eq_thm] THEN 84 SRW_TAC [][EQ_IMP_THM, tpm_eqr] THEN 85 METIS_TAC [lemma15a, pmact_flip_args, fresh_tpm_subst] 86 ]); 87 88val hnf_def = Define`hnf M = ���N. ��(M -h-> N)`; 89val hnf_thm = Store_thm( 90 "hnf_thm", 91 ``(hnf (VAR s) ��� T) ��� 92 (hnf (M @@ N) ��� hnf M ��� ��is_abs M) ��� 93 (hnf (LAM v M) ��� hnf M)``, 94 SRW_TAC [][hnf_def, hreduce1_rwts] THEN 95 Cases_on `is_abs M` THEN SRW_TAC [][hreduce1_rwts] THEN 96 Q.SPEC_THEN `M` FULL_STRUCT_CASES_TAC term_CASES THEN 97 FULL_SIMP_TAC (srw_ss()) [hreduce1_rwts]); 98 99val hnf_tpm = Store_thm( 100 "hnf_tpm", 101 ``���M ��. hnf (����M) = hnf M``, 102 HO_MATCH_MP_TAC simple_induction THEN SRW_TAC [][]); 103 104val hreduce1_unique = store_thm( 105 "hreduce1_unique", 106 ``���M N1 N2. M -h-> N1 ��� M -h-> N2 ��� (N1 = N2)``, 107 Q_TAC SUFF_TAC `���M N. M -h-> N ��� ���P. M -h-> P ��� (N = P)` 108 THEN1 METIS_TAC [] THEN 109 HO_MATCH_MP_TAC hreduce1_ind THEN 110 SIMP_TAC (srw_ss() ++ DNF_ss) [hreduce1_rwts]); 111 112val strong_cc_ind = IndDefLib.derive_strong_induction (compat_closure_rules, 113 compat_closure_ind) 114 115val hnf_ccbeta_preserved = store_thm( 116 "hnf_ccbeta_preserved", 117 ``���M N. compat_closure beta M N ��� hnf M ��� hnf N``, 118 Q_TAC SUFF_TAC 119 `���M N. compat_closure beta M N ��� hnf M ��� hnf N` 120 THEN1 METIS_TAC [] THEN 121 HO_MATCH_MP_TAC strong_cc_ind THEN SRW_TAC [][] THENL [ 122 FULL_SIMP_TAC (srw_ss()) [beta_def] THEN 123 SRW_TAC [][] THEN FULL_SIMP_TAC (srw_ss()) [], 124 125 Q.SPEC_THEN `M` FULL_STRUCT_CASES_TAC term_CASES THEN 126 FULL_SIMP_TAC (srw_ss()) [cc_beta_thm] THEN 127 SRW_TAC [][] THEN FULL_SIMP_TAC (srw_ss()) [] 128 ]); 129 130val (weak_head_rules, weak_head_ind, weak_head_cases) = Hol_reln` 131 (���v M N. weak_head (LAM v M @@ N) ([N/v]M)) ��� 132 (���M��� M��� N. weak_head M��� M��� ��� weak_head (M��� @@ N) (M��� @@ N)) 133`; 134val _ = set_fixity "-w->" (Infix(NONASSOC, 450)) 135val _ = overload_on ("-w->", ``weak_head``) 136 137val strong_weak_ind = IndDefLib.derive_strong_induction(weak_head_rules, 138 weak_head_ind) 139 140val wh_is_abs = store_thm( 141 "wh_is_abs", 142 ``���M N. M -w-> N ��� ��is_abs M``, 143 HO_MATCH_MP_TAC weak_head_ind THEN SRW_TAC [][]); 144 145val wh_lam = Store_thm( 146 "wh_lam", 147 ``���v M N. ��(LAM v M -w-> N)``, 148 ONCE_REWRITE_TAC [weak_head_cases] THEN SRW_TAC [][]); 149 150val wh_head = store_thm( 151 "wh_head", 152 ``���M N. M -w-> N ��� M -h-> N``, 153 HO_MATCH_MP_TAC strong_weak_ind THEN METIS_TAC [wh_is_abs, hreduce1_rules]); 154 155 156 157val _ = set_fixity "-w->*" (Infix(NONASSOC, 450)) 158val _ = overload_on ("-w->*", ``RTC (-w->)``) 159 160val whead_FV = store_thm( 161 "whead_FV", 162 ``���M N. M -w-> N ��� v ��� FV N ��� v ��� FV M``, 163 HO_MATCH_MP_TAC weak_head_ind THEN SRW_TAC [][FV_SUB] THEN 164 METIS_TAC []); 165val whstar_FV = store_thm( 166 "whstar_FV", 167 ``���M N. M -w->* N ��� v ��� FV N ��� v ��� FV M``, 168 HO_MATCH_MP_TAC relationTheory.RTC_INDUCT THEN 169 METIS_TAC [relationTheory.RTC_RULES, whead_FV]); 170 171 172val _ = reveal "Y" 173val whY1 = store_thm( 174 "whY1", 175 ``Y @@ f -w-> Yf f``, 176 SRW_TAC [][chap2Theory.Y_def, chap2Theory.Yf_def, LET_THM, 177 Once weak_head_cases] THEN 178 NEW_ELIM_TAC THEN REPEAT STRIP_TAC THEN 179 SRW_TAC [DNF_ss][LAM_eq_thm] THEN DISJ1_TAC THEN 180 SRW_TAC [][chap2Theory.SUB_LAM_RWT, LET_THM] THEN NEW_ELIM_TAC THEN 181 SRW_TAC [][LAM_eq_thm, tpm_fresh]); 182 183val whY2 = store_thm( 184 "whY2", 185 ``Yf f -w-> f @@ Yf f``, 186 SRW_TAC [][chap2Theory.Yf_def, LET_THM, Once weak_head_cases] THEN 187 NEW_ELIM_TAC THEN SRW_TAC [DNF_ss][LAM_eq_thm, lemma14b]); 188 189val wh_unique = store_thm( 190 "wh_unique", 191 ``M -w-> N��� ��� M -w-> N��� ��� (N��� = N���)``, 192 METIS_TAC [hreduce1_unique, wh_head]); 193 194val whnf_def = Define` 195 whnf M = ���N. ��(M -w-> N) 196`; 197 198val hnf_whnf = store_thm( 199 "hnf_whnf", 200 ``hnf M ��� whnf M``, 201 METIS_TAC [hnf_def, whnf_def, wh_head]); 202 203val bnf_hnf = store_thm( 204 "bnf_hnf", 205 ``bnf M ��� hnf M``, 206 METIS_TAC [hnf_def, beta_normal_form_bnf, corollary3_2_1, hreduce_ccbeta]); 207 208val bnf_whnf = store_thm( 209 "bnf_whnf", 210 ``bnf M ��� whnf M``, 211 METIS_TAC [hnf_whnf, bnf_hnf]); 212 213val whnf_thm = Store_thm( 214 "whnf_thm", 215 ``whnf (VAR s) ��� 216 (whnf (M @@ N) ��� ��is_abs M ��� whnf M) ��� 217 whnf (LAM v M)``, 218 REPEAT CONJ_TAC THEN SRW_TAC [][whnf_def, Once weak_head_cases] THEN 219 EQ_TAC THEN SRW_TAC [][FORALL_AND_THM] THENL [ 220 Q.SPEC_THEN `M` FULL_STRUCT_CASES_TAC term_CASES THEN SRW_TAC [][] THEN 221 METIS_TAC [], 222 Q.SPEC_THEN `M` FULL_STRUCT_CASES_TAC term_CASES THEN 223 FULL_SIMP_TAC (srw_ss()) [] 224 ]); 225 226val wh_weaken_cong = store_thm( 227 "wh_weaken_cong", 228 ``whnf N ��� M��� -w->* M��� ��� (M��� -w->* N = M��� -w->* N)``, 229 SIMP_TAC (srw_ss()) [EQ_IMP_THM, IMP_CONJ_THM] THEN CONJ_TAC THENL [ 230 Q_TAC SUFF_TAC `���M N. M -w->* N ��� ���N'. M -w->* N' ��� whnf N' ��� N -w->* N'` 231 THEN1 METIS_TAC [] THEN 232 HO_MATCH_MP_TAC relationTheory.RTC_INDUCT THEN SRW_TAC [][] THEN 233 METIS_TAC [relationTheory.RTC_CASES1, whnf_def, wh_unique], 234 235 METIS_TAC [relationTheory.RTC_CASES_RTC_TWICE] 236 ]); 237 238val wh_app_congL = store_thm( 239 "wh_app_congL", 240 ``M -w->* M' ==> M @@ N -w->* M' @@ N``, 241 STRIP_TAC THEN Q.ID_SPEC_TAC `N` THEN POP_ASSUM MP_TAC THEN 242 MAP_EVERY Q.ID_SPEC_TAC [`M'`, `M`] THEN 243 HO_MATCH_MP_TAC relationTheory.RTC_INDUCT THEN SRW_TAC [][] THEN 244 METIS_TAC [relationTheory.RTC_RULES, weak_head_rules]); 245 246val tpm_whead_I = store_thm( 247 "tpm_whead_I", 248 ``���M N. M -w-> N ��� ����M -w-> ����N``, 249 HO_MATCH_MP_TAC weak_head_ind THEN SRW_TAC [][weak_head_rules, tpm_subst]); 250 251val whead_gen_bvc_ind = store_thm( 252 "whead_gen_bvc_ind", 253 ``���P f. (���x. FINITE (f x)) ��� 254 (���v M N x. v ��� f x ��� P (LAM v M @@ N) ([N/v]M) x) ��� 255 (���M��� M��� N x. (���z. P M��� M��� z) ��� P (M��� @@ N) (M��� @@ N) x) 256 ��� 257 ���M N. M -w-> N ��� ���x. P M N x``, 258 REPEAT GEN_TAC THEN STRIP_TAC THEN 259 Q_TAC SUFF_TAC `���M N. M -w-> N ��� ����� x. P (����M) (����N) x` 260 THEN1 METIS_TAC [pmact_nil] THEN 261 HO_MATCH_MP_TAC weak_head_ind THEN SRW_TAC [][tpm_subst] THEN 262 Q_TAC (NEW_TAC "z") `{lswapstr �� v} ��� FV (����M) ��� FV (����N) ��� f x` THEN 263 `LAM (lswapstr �� v) (����M) = LAM z ([VAR z/lswapstr �� v](����M))` 264 by SRW_TAC [][SIMPLE_ALPHA] THEN 265 `[����N/lswapstr �� v](����M) = [����N/z] ([VAR z/lswapstr �� v](����M))` 266 by SRW_TAC [][lemma15a] THEN 267 SRW_TAC [][]); 268 269val whead_bvcX_ind = save_thm( 270 "whead_bvcX_ind", 271 whead_gen_bvc_ind |> Q.SPECL [`��M N x. P' M N`, `��x. X`] 272 |> SIMP_RULE (srw_ss()) [] 273 |> Q.INST [`P'` |-> `P`] 274 |> Q.GEN `X` |> Q.GEN `P`); 275 276val wh_substitutive = store_thm( 277 "wh_substitutive", 278 ``���M N. M -w-> N ��� [P/v]M -w-> [P/v]N``, 279 HO_MATCH_MP_TAC whead_bvcX_ind THEN Q.EXISTS_TAC `FV P ��� {v}` THEN 280 SRW_TAC [][weak_head_rules] THEN 281 METIS_TAC [chap2Theory.substitution_lemma, weak_head_rules]); 282 283val whstar_substitutive = store_thm( 284 "whstar_substitutive", 285 ``���M N. M -w->* N ��� [P/v]M -w->* [P/v]N``, 286 HO_MATCH_MP_TAC relationTheory.RTC_INDUCT THEN SRW_TAC [][] THEN 287 METIS_TAC [relationTheory.RTC_RULES, wh_substitutive]); 288 289val whstar_betastar = store_thm( 290 "whstar_betastar", 291 ``���M N. M -w->* N ��� M -��->* N``, 292 HO_MATCH_MP_TAC relationTheory.RTC_INDUCT THEN SRW_TAC [][] THEN 293 METIS_TAC [relationTheory.RTC_RULES, wh_head, hreduce_ccbeta]); 294 295val whstar_lameq = store_thm( 296 "whstar_lameq", 297 ``M -w->* N ��� M == N``, 298 METIS_TAC [betastar_lameq, whstar_betastar]); 299 300val whstar_abs = Store_thm( 301 "whstar_abs", 302 ``LAM v M -w->* N ��� (N = LAM v M)``, 303 SRW_TAC [][EQ_IMP_THM] THEN 304 FULL_SIMP_TAC (srw_ss()) [Once relationTheory.RTC_CASES1, 305 Once weak_head_cases]); 306 307(* ---------------------------------------------------------------------- 308 has_whnf 309 ---------------------------------------------------------------------- *) 310 311(* definition of has_hnf in standardisationScript has == rather than -h->* 312 as the relation on the RHS. This means that has_bnf automatically implies 313 has_hnf, but makes the corollary to the standardisation theorem interesting 314 to prove... *) 315val has_whnf_def = Define` 316 has_whnf M = ���N. M -w->* N ��� whnf N 317`; 318 319val has_whnf_APP_E = store_thm( 320 "has_whnf_APP_E", 321 ``has_whnf (M @@ N) ��� has_whnf M``, 322 simp_tac (srw_ss())[has_whnf_def] >> 323 Q_TAC SUFF_TAC 324 `���M N. M -w->* N ��� ���M0 M1. (M = M0 @@ M1) ��� whnf N ��� 325 ���N'. M0 -w->* N' ��� whnf N'` 326 >- metis_tac [] >> 327 ho_match_mp_tac relationTheory.RTC_INDUCT >> conj_tac 328 >- (simp_tac (srw_ss()) [] >> metis_tac [relationTheory.RTC_RULES]) >> 329 srw_tac [][] >> Cases_on `is_abs M0` 330 >- (Q.SPEC_THEN `M0` FULL_STRUCT_CASES_TAC term_CASES >> 331 full_simp_tac (srw_ss()) [] >> 332 metis_tac [relationTheory.RTC_RULES, whnf_thm]) >> 333 full_simp_tac (srw_ss()) [Once weak_head_cases] >> 334 metis_tac [relationTheory.RTC_RULES]) 335 336val hreduce_weak_or_strong = store_thm( 337 "hreduce_weak_or_strong", 338 ``���M N. M -h-> N ��� whnf M ��� M -w-> N``, 339 ho_match_mp_tac simple_induction >> simp_tac (srw_ss()) [] >> 340 rpt gen_tac >> strip_tac >> rpt gen_tac >> 341 simp_tac (srw_ss()) [Once hreduce1_cases] >> 342 simp_tac (srw_ss() ++ DNF_ss) [] >> conj_tac 343 >- metis_tac [weak_head_rules] >> 344 srw_tac [][] >> metis_tac [weak_head_rules]); 345 346val head_reductions_have_weak_prefixes = store_thm( 347 "head_reductions_have_weak_prefixes", 348 ``���M N. M -h->* N ��� hnf N ��� 349 ���N0. M -w->* N0 ��� whnf N0 ��� N0 -h->* N``, 350 ho_match_mp_tac relationTheory.RTC_STRONG_INDUCT >> conj_tac 351 >- metis_tac [hnf_whnf, relationTheory.RTC_RULES] >> 352 metis_tac [relationTheory.RTC_RULES, hreduce_weak_or_strong]); 353 354val _ = export_theory() 355