1open HolKernel Parse boolLib 2 3open bossLib metisLib boolSimps 4 5open chap3Theory chap2Theory labelledTermsTheory termTheory binderLib 6open term_posnsTheory chap11_1Theory 7open pathTheory BasicProvers nomsetTheory pred_setTheory 8 9local open pred_setLib in end 10val _ = augment_srw_ss [boolSimps.LET_ss] 11 12val _ = new_theory "finite_developments"; 13 14fun Save_Thm(n, th) = save_thm(n,th) before export_rewrites [n] 15fun Store_Thm(n, t, tac) = store_thm(n, t, tac) before export_rewrites [n] 16 17val _ = hide "set" 18 19val RUNION_COMM = relationTheory.RUNION_COMM 20val RUNION = relationTheory.RUNION 21 22(* finiteness of developments : section 11.2 of Barendregt *) 23 24(* ---------------------------------------------------------------------- 25 substitutivity etc 26 ---------------------------------------------------------------------- *) 27 28val lsubstitutive_def = Define` 29 lsubstitutive R = !M (N:lterm) v L. R M N ==> R ([L/v]M) ([L/v]N) 30`; 31 32val lpermutative_def = Define` 33 lpermutative R = !M (N:lterm) pi. R M N ==> R (ltpm pi M) (ltpm pi N) 34`; 35 36val RUNION_lsubstitutive = store_thm( 37 "RUNION_lsubstitutive", 38 ``!R1 R2. lsubstitutive R1 /\ lsubstitutive R2 ==> 39 lsubstitutive (R1 RUNION R2)``, 40 SRW_TAC [][lsubstitutive_def, relationTheory.RUNION] THEN SRW_TAC [][]); 41 42val lsubstitutive_lpermutative = store_thm( 43 "lsubstitutive_lpermutative", 44 ``lsubstitutive R ==> lpermutative R``, 45 SRW_TAC [][lsubstitutive_def, lpermutative_def] THEN 46 Induct_on `pi` THEN SRW_TAC [][] THEN 47 `?x y. h = (x,y)` by (Cases_on `h` THEN METIS_TAC []) THEN 48 SRW_TAC [][] THEN 49 `(ltpm ((x,y)::pi) M = ltpm [(x,y)] (ltpm pi M)) /\ 50 (ltpm ((x,y)::pi) N = ltpm [(x,y)] (ltpm pi N))` 51 by SRW_TAC [][GSYM pmact_decompose] THEN 52 SRW_TAC [][] THEN 53 Q.MATCH_ABBREV_TAC `R (ltpm [(x,y)] MM) (ltpm [(x,y)] NN)` THEN 54 Q_TAC (NEW_TAC "z") `{x;y} UNION FV MM UNION FV NN` THEN 55 Q_TAC SUFF_TAC `(ltpm [(x,y)] MM = [VAR y/z] ([VAR x/y] ([VAR z/x] MM))) /\ 56 (ltpm [(x,y)] NN = [VAR y/z] ([VAR x/y] ([VAR z/x] NN)))` 57 THEN1 SRW_TAC [][] THEN 58 ASM_SIMP_TAC (srw_ss()) [GSYM fresh_ltpm_subst, GSYM pmact_decompose] THEN 59 Q_TAC SUFF_TAC `[(x,y)] == [(y,z); (x,y); (z,x)]` 60 THEN1 METIS_TAC [nomsetTheory.pmact_permeq] THEN 61 SRW_TAC [][nomsetTheory.permeq_def, FUN_EQ_THM] THEN 62 Cases_on `x' = x` THEN SRW_TAC [][] THEN 63 Cases_on `x' = z` THEN SRW_TAC [][] THEN 64 Cases_on `x' = y` THEN SRW_TAC [][]); 65 66(* ---------------------------------------------------------------------- 67 define redex labelled reduction for unlabelled and labelled terms 68 ---------------------------------------------------------------------- *) 69 70val _ = 71 "Defining redex-labelled reduction for unlabelled and labelled terms\n"; 72 73(* unlabelled terms *) 74val (labelled_redn_rules, labelled_redn_ind, labelled_redn_cases) = 75 Hol_reln`(!x y. R (x:term) y ==> labelled_redn R x [] y) /\ 76 (!z x y pos. 77 labelled_redn R x pos y ==> 78 labelled_redn R (x @@ z) (Lt::pos) (y @@ z)) /\ 79 (!z x y pos. 80 labelled_redn R x pos y ==> 81 labelled_redn R (z @@ x) (Rt::pos) (z @@ y)) /\ 82 (!v x y pos. 83 labelled_redn R x pos y ==> 84 labelled_redn R (LAM v x) (In::pos) (LAM v y))`; 85 86val strong_labelled_redn_ind = save_thm( 87 "strong_labelled_redn_ind", 88 IndDefLib.derive_strong_induction (labelled_redn_rules, labelled_redn_ind)); 89 90val labelled_redn_bvc_ind = store_thm( 91 "labelled_redn_bvc_ind", 92 ``!P X. FINITE X /\ 93 (!v M N. ~(v IN X) /\ ~(v IN FV N) ==> 94 P (LAM v M @@ N) [] ([N/v]M)) /\ 95 (!z x y pos. P x pos y ==> P (x @@ z) (Lt::pos) (y @@ z)) /\ 96 (!z x y pos. P x pos y ==> P (z @@ x) (Rt::pos) (z @@ y)) /\ 97 (!v x y pos. ~(v IN X) /\ P x pos y ==> 98 P (LAM v x) (In::pos) (LAM v y)) ==> 99 !M pos N. labelled_redn beta M pos N ==> P M pos N``, 100 REPEAT GEN_TAC THEN STRIP_TAC THEN 101 Q_TAC SUFF_TAC 102 `!M pos N. labelled_redn beta M pos N ==> 103 !p. P (tpm p M) pos (tpm p N)` 104 THEN1 METIS_TAC [pmact_nil] THEN 105 HO_MATCH_MP_TAC labelled_redn_ind THEN SRW_TAC [][beta_def] THENL [ 106 SRW_TAC [][tpm_subst] THEN 107 Q.MATCH_ABBREV_TAC `P (LAM v M @@ N) [] ([N/v]M)` THEN 108 Q_TAC (NEW_TAC "z") `X UNION FV M UNION FV N` THEN 109 `LAM v M = LAM z (tpm [(z,v)] M)` by SRW_TAC [][tpm_ALPHA] THEN 110 `[N/v] M = [N/z] ([VAR z/v] M)` by SRW_TAC [][lemma15a] THEN 111 SRW_TAC [][GSYM pmact_decompose, GSYM fresh_tpm_subst], 112 113 Q.MATCH_ABBREV_TAC `P (LAM vv MM) (In::pos) (LAM vv NN)` THEN 114 Q_TAC (NEW_TAC "z") `X UNION FV MM UNION FV NN` THEN 115 `(LAM vv MM = LAM z (tpm [(z,vv)] MM)) /\ 116 (LAM vv NN = LAM z (tpm [(z,vv)] NN))` 117 by SRW_TAC [][tpm_ALPHA] THEN 118 SRW_TAC [][Abbr`MM`, Abbr`NN`, GSYM pmact_decompose] 119 ]); 120 121val labelled_redn_beta_tpm_imp = store_thm( 122 "labelled_redn_beta_tpm_imp", 123 ``!M pos N. labelled_redn beta M pos N ==> 124 !pi. labelled_redn beta (tpm pi M) pos (tpm pi N)``, 125 HO_MATCH_MP_TAC labelled_redn_ind THEN 126 SRW_TAC [][beta_def, labelled_redn_rules] THEN 127 SRW_TAC [][tpm_subst] THEN 128 METIS_TAC [beta_def, labelled_redn_rules]); 129 130val labelled_redn_beta_tpm_eqn = store_thm( 131 "labelled_redn_beta_tpm_eqn", 132 ``labelled_redn beta (tpm p M) pos N = 133 labelled_redn beta M pos (tpm (REVERSE p) N)``, 134 METIS_TAC [labelled_redn_beta_tpm_imp, pmact_inverse]); 135 136 137(* relationship to unlabelled reductions *) 138val cc_labelled_redn = store_thm( 139 "cc_labelled_redn", 140 ``!R M N. compat_closure R M N ==> ?pos. labelled_redn R M pos N``, 141 GEN_TAC THEN HO_MATCH_MP_TAC compat_closure_ind THEN 142 PROVE_TAC [labelled_redn_rules]); 143 144val labelled_redn_cc = store_thm( 145 "labelled_redn_cc", 146 ``!R M pos N. labelled_redn R M pos N ==> compat_closure R M N``, 147 GEN_TAC THEN HO_MATCH_MP_TAC labelled_redn_ind THEN 148 PROVE_TAC [compat_closure_rules]); 149 150(* labelled terms *) 151val (lrcc_rules, lrcc_ind, lrcc_cases) = 152 Hol_reln`(!x y. R x y ==> lrcc R x [] y) /\ 153 (!x y z r. lrcc R x r y ==> 154 lrcc R (x @@ z) (Lt::r) (y @@ z)) /\ 155 (!x y z r. lrcc R x r y ==> 156 lrcc R (z @@ x) (Rt::r) (z @@ y)) /\ 157 (!x y v r. lrcc R x r y ==> 158 lrcc R (LAM v x) (In::r) (LAM v y)) /\ 159 (!x y n v z r. 160 lrcc R x r y ==> 161 lrcc R (LAMi n v z x) (Rt::r) (LAMi n v z y)) /\ 162 (!x y n v z r. 163 lrcc R x r y ==> 164 lrcc R (LAMi n v x z) (Lt::In::r) (LAMi n v y z))`; 165 166val strong_lrcc_ind = save_thm( 167 "strong_lrcc_ind", 168 IndDefLib.derive_strong_induction(lrcc_rules, lrcc_ind)); 169 170val lrcc_bvc_b01_ind = store_thm( 171 "lrcc_bvc_b01_ind", 172 ``!P X. 173 FINITE X /\ 174 (!v M N. ~(v IN X) /\ ~(v IN FV N) ==> 175 P (LAM v M @@ N) [] ([N/v]M)) /\ 176 (!n v M N. ~(v IN X) /\ ~(v IN FV N) ==> 177 P (LAMi n v M N) [] ([N/v]M)) /\ 178 (!M M' N pos. P M pos M' ==> P (M @@ N) (Lt::pos) (M' @@ N)) /\ 179 (!M N N' pos. P N pos N' ==> P (M @@ N) (Rt::pos) (M @@ N')) /\ 180 (!v M M' pos. ~(v IN X) /\ P M pos M' ==> 181 P (LAM v M) (In::pos) (LAM v M')) /\ 182 (!n v M M' N pos. ~(v IN FV N) /\ ~(v IN X) /\ P M pos M' ==> 183 P (LAMi n v M N) (Lt::In::pos) (LAMi n v M' N)) /\ 184 (!n v M N N' pos. ~(v IN FV N) /\ ~(v IN X) /\ ~(v IN FV N') /\ 185 P N pos N' ==> 186 P (LAMi n v M N) (Rt::pos) (LAMi n v M N')) ==> 187 !M pos N. lrcc (beta0 RUNION beta1) M pos N ==> P M pos N``, 188 REPEAT GEN_TAC THEN STRIP_TAC THEN 189 Q_TAC SUFF_TAC `!M pos N. lrcc (beta0 RUNION beta1) M pos N ==> 190 !p. P (ltpm p M) pos (ltpm p N)` 191 THEN1 METIS_TAC [pmact_nil] THEN 192 HO_MATCH_MP_TAC lrcc_ind THEN SRW_TAC [][beta0_def, beta1_def, RUNION] 193 THENL [ 194 SRW_TAC [][ltpm_subst] THEN 195 Q.MATCH_ABBREV_TAC `P (LAMi n vv MM NN) [] ([NN/vv]MM)` THEN 196 markerLib.RM_ALL_ABBREVS_TAC THEN 197 Q_TAC (NEW_TAC "z") `X UNION FV MM UNION FV NN` THEN 198 `LAMi n vv MM NN = LAMi n z (ltpm [(z,vv)] MM) NN` 199 by SRW_TAC [][ltpm_ALPHAi] THEN 200 `[NN/vv]MM = [NN/z] ([VAR z/vv] MM)` by SRW_TAC [][l15a] THEN 201 SRW_TAC [][GSYM fresh_ltpm_subst], 202 SRW_TAC [][ltpm_subst] THEN 203 Q.MATCH_ABBREV_TAC `P (LAM vv MM @@ NN) [] ([NN/vv]MM)` THEN 204 markerLib.RM_ALL_ABBREVS_TAC THEN 205 Q_TAC (NEW_TAC "z") `X UNION FV MM UNION FV NN` THEN 206 `LAM vv MM = LAM z (ltpm [(z,vv)] MM)` by SRW_TAC [][ltpm_ALPHA] THEN 207 `[NN/vv]MM = [NN/z] ([VAR z/vv] MM)` by SRW_TAC [][l15a] THEN 208 SRW_TAC [][GSYM fresh_ltpm_subst], 209 Q.MATCH_ABBREV_TAC `P (LAM vv MM) (In::pos) (LAM vv NN)` THEN 210 Q_TAC (NEW_TAC "z") `X UNION FV MM UNION FV NN` THEN 211 `(LAM vv MM = LAM z (ltpm [(z,vv)] MM)) /\ 212 (LAM vv NN = LAM z (ltpm [(z,vv)] NN))` by SRW_TAC [][ltpm_ALPHA] THEN 213 SRW_TAC [][Abbr`MM`, Abbr`NN`, GSYM pmact_decompose], 214 Q.MATCH_ABBREV_TAC `P (LAMi n vv ZZ MM) (Rt::Pos) (LAMi n vv ZZ NN)` THEN 215 Q_TAC (NEW_TAC "z") `FV ZZ UNION FV MM UNION FV NN UNION X` THEN 216 `(LAMi n vv ZZ MM = LAMi n z (ltpm [(z,vv)] ZZ) MM) /\ 217 (LAMi n vv ZZ NN = LAMi n z (ltpm [(z,vv)] ZZ) NN)` 218 by SRW_TAC [][ltpm_ALPHAi] THEN 219 SRW_TAC [][Abbr`MM`, Abbr`NN`, GSYM pmact_decompose], 220 Q.MATCH_ABBREV_TAC 221 `P (LAMi n vv MM ZZ) (Lt::In::pos) (LAMi n vv NN ZZ)` THEN 222 Q_TAC (NEW_TAC "z") `FV ZZ UNION FV MM UNION FV NN UNION X` THEN 223 `(LAMi n vv MM ZZ = LAMi n z (ltpm [(z,vv)] MM) ZZ) /\ 224 (LAMi n vv NN ZZ = LAMi n z (ltpm [(z,vv)] NN) ZZ)` 225 by SRW_TAC [][ltpm_ALPHAi] THEN 226 SRW_TAC [][Abbr`MM`, Abbr`NN`, GSYM pmact_decompose] 227 ]); 228 229val lrcc_bvc_ind = store_thm( 230 "lrcc_bvc_ind", 231 ``!P X. 232 FINITE X /\ 233 lpermutative R /\ 234 (!M N. R M N ==> P M [] N) /\ 235 (!M M' N pos. P M pos M' ==> P (M @@ N) (Lt::pos) (M' @@ N)) /\ 236 (!M N N' pos. P N pos N' ==> P (M @@ N) (Rt::pos) (M @@ N')) /\ 237 (!v M M' pos. ~(v IN X) /\ P M pos M' ==> 238 P (LAM v M) (In::pos) (LAM v M')) /\ 239 (!n v M M' N pos. ~(v IN FV N) /\ ~(v IN X) /\ P M pos M' ==> 240 P (LAMi n v M N) (Lt::In::pos) (LAMi n v M' N)) /\ 241 (!n v M N N' pos. ~(v IN FV N) /\ ~(v IN X) /\ ~(v IN FV N') /\ 242 P N pos N' ==> 243 P (LAMi n v M N) (Rt::pos) (LAMi n v M N')) ==> 244 !M pos N. lrcc R M pos N ==> P M pos N``, 245 REPEAT GEN_TAC THEN STRIP_TAC THEN 246 Q_TAC SUFF_TAC `!M pos N. lrcc R M pos N ==> 247 !p. P (ltpm p M) pos (ltpm p N)` 248 THEN1 METIS_TAC [pmact_nil] THEN 249 HO_MATCH_MP_TAC lrcc_ind THEN SRW_TAC [][] THENL [ 250 METIS_TAC [lpermutative_def], 251 Q.MATCH_ABBREV_TAC `P (LAM vv MM) (In::pos) (LAM vv NN)` THEN 252 Q_TAC (NEW_TAC "z") `X UNION FV MM UNION FV NN` THEN 253 `(LAM vv MM = LAM z (ltpm [(z,vv)] MM)) /\ 254 (LAM vv NN = LAM z (ltpm [(z,vv)] NN))` by SRW_TAC [][ltpm_ALPHA] THEN 255 SRW_TAC [][Abbr`MM`, Abbr`NN`, GSYM pmact_decompose], 256 Q.MATCH_ABBREV_TAC `P (LAMi n vv ZZ MM) (Rt::Pos) (LAMi n vv ZZ NN)` THEN 257 Q_TAC (NEW_TAC "z") `FV ZZ UNION FV MM UNION FV NN UNION X` THEN 258 `(LAMi n vv ZZ MM = LAMi n z (ltpm [(z,vv)] ZZ) MM) /\ 259 (LAMi n vv ZZ NN = LAMi n z (ltpm [(z,vv)] ZZ) NN)` 260 by SRW_TAC [][ltpm_ALPHAi] THEN 261 SRW_TAC [][Abbr`MM`, Abbr`NN`, GSYM pmact_decompose], 262 Q.MATCH_ABBREV_TAC 263 `P (LAMi n vv MM ZZ) (Lt::In::pos) (LAMi n vv NN ZZ)` THEN 264 Q_TAC (NEW_TAC "z") `FV ZZ UNION FV MM UNION FV NN UNION X` THEN 265 `(LAMi n vv MM ZZ = LAMi n z (ltpm [(z,vv)] MM) ZZ) /\ 266 (LAMi n vv NN ZZ = LAMi n z (ltpm [(z,vv)] NN) ZZ)` 267 by SRW_TAC [][ltpm_ALPHAi] THEN 268 SRW_TAC [][Abbr`MM`, Abbr`NN`, GSYM pmact_decompose] 269 ]); 270 271 272val lrcc_labelled_redn = store_thm( 273 "lrcc_labelled_redn", 274 ``!x r y. 275 lrcc (beta0 RUNION beta1) x r y ==> 276 labelled_redn beta (strip_label x) r (strip_label y)``, 277 HO_MATCH_MP_TAC lrcc_bvc_b01_ind THEN Q.EXISTS_TAC `{}` THEN 278 SRW_TAC [][strip_label_subst, labelled_redn_rules] THEN 279 METIS_TAC [beta_def, labelled_redn_rules]); 280 281val strip_path_label_def = Define`strip_path_label = pmap strip_label I`; 282 283val strip_path_label_thm = store_thm( 284 "strip_path_label_thm", 285 ``(!x. strip_path_label (stopped_at x) = stopped_at (strip_label x)) /\ 286 (!x r p. 287 strip_path_label (pcons x r p) = 288 pcons (strip_label x) r (strip_path_label p))``, 289 SRW_TAC [][strip_path_label_def, pmap_thm, combinTheory.I_THM]); 290val _ = export_rewrites ["strip_path_label_thm"] 291 292val first_strip_path_label = store_thm( 293 "first_strip_path_label", 294 ``!p. first (strip_path_label p) = strip_label (first p)``, 295 GEN_TAC THEN 296 Q.ISPEC_THEN `p` STRUCT_CASES_TAC path_cases THEN 297 SRW_TAC [][first_thm, strip_path_label_thm]); 298val _ = export_rewrites ["first_strip_path_label"] 299 300(* ---------------------------------------------------------------------- 301 proofs begin 302 ---------------------------------------------------------------------- *) 303 304val lemma11_2_1 = store_thm( 305 "lemma11_2_1", 306 ``!sigma'. 307 okpath (lrcc (beta0 RUNION beta1)) sigma' ==> 308 okpath (labelled_redn beta) (strip_path_label sigma')``, 309 Q_TAC SUFF_TAC 310 `!sigma. 311 (?sigma'. (sigma = strip_path_label sigma') /\ 312 okpath (lrcc (beta0 RUNION beta1)) sigma') ==> 313 okpath (labelled_redn beta) sigma` THEN1 PROVE_TAC [] THEN 314 HO_MATCH_MP_TAC okpath_co_ind THEN 315 SRW_TAC [][Once EXISTS_path, SimpL ``(==>)``] THEN 316 SRW_TAC [][] THEN PROVE_TAC [lrcc_labelled_redn]); 317 318val beta0_lsubstitutive = store_thm( 319 "beta0_lsubstitutive", 320 ``lsubstitutive beta0``, 321 SRW_TAC [][lsubstitutive_def, beta0_def] THEN 322 Q_TAC (NEW_TAC "z") `{v; v'} UNION FV t UNION FV L` THEN 323 `LAMi n v' t u = LAMi n z (ltpm [(z,v')] t) u` 324 by SRW_TAC [][ltpm_ALPHAi] THEN 325 ASM_SIMP_TAC (srw_ss()) [lSUB_THM] THEN 326 MAP_EVERY Q.EXISTS_TAC [`n`, `z`, `[L/v] ([VAR z/v'] t)`, `[L/v]u`] THEN 327 ASM_SIMP_TAC (srw_ss()) [GSYM lSUBSTITUTION_LEMMA, l15a, 328 fresh_ltpm_subst]); 329 330val beta1_lsubstitutive = store_thm( 331 "beta1_lsubstitutive", 332 ``lsubstitutive beta1``, 333 SIMP_TAC (srw_ss()) [lsubstitutive_def, beta1_def, lSUB_THM, 334 GSYM LEFT_FORALL_IMP_THM] THEN 335 REPEAT GEN_TAC THEN 336 Q_TAC (NEW_TAC "z") `{v; v'} UNION FV t UNION FV L` THEN 337 `LAM v' t = LAM z (ltpm [(z,v')] t)` by SRW_TAC [][ltpm_ALPHA] THEN 338 MAP_EVERY Q.EXISTS_TAC [`z`, `[L/v]([VAR z/v']t)`] THEN 339 ASM_SIMP_TAC (srw_ss()) [GSYM lSUBSTITUTION_LEMMA, l15a, 340 fresh_ltpm_subst]); 341 342val lrcc_lsubstitutive = store_thm( 343 "lrcc_lsubstitutive", 344 ``!R. lsubstitutive R ==> 345 !M pos N. 346 lrcc R M pos N ==> !v L. lrcc R ([L/v]M) pos ([L/v]N)``, 347 GEN_TAC THEN REPEAT STRIP_TAC THEN 348 Q.UNDISCH_THEN `lrcc R M pos N` MP_TAC THEN 349 MAP_EVERY Q.ID_SPEC_TAC [`N`, `pos`, `M`] THEN 350 HO_MATCH_MP_TAC lrcc_bvc_ind THEN Q.EXISTS_TAC `v INSERT FV L` THEN 351 SRW_TAC [][lsubstitutive_lpermutative, lrcc_rules] THEN 352 METIS_TAC [lsubstitutive_def, lrcc_rules]); 353 354val labelled_redn_beta_sub = store_thm( 355 "labelled_redn_beta_sub", 356 ``!M pos N. labelled_redn beta M pos N ==> 357 !t v. labelled_redn beta ([t/v]M) pos ([t/v]N)``, 358 REPEAT STRIP_TAC THEN POP_ASSUM MP_TAC THEN 359 MAP_EVERY Q.ID_SPEC_TAC [`N`, `pos`, `M`] THEN 360 HO_MATCH_MP_TAC labelled_redn_bvc_ind THEN 361 Q.EXISTS_TAC `v INSERT FV t` THEN 362 SRW_TAC [][labelled_redn_rules, SUB_THM] THEN 363 METIS_TAC [substitution_lemma, labelled_redn_rules, beta_def]); 364 365val lrcc_beta_sub = store_thm( 366 "lrcc_beta_sub", 367 ``!M pos N. lrcc (beta0 RUNION beta1) M pos N ==> 368 !v t. lrcc (beta0 RUNION beta1) ([t/v]M) pos ([t/v]N)``, 369 PROVE_TAC [lrcc_lsubstitutive, beta0_lsubstitutive, beta1_lsubstitutive, 370 RUNION_lsubstitutive]); 371 372val lrcc_b01_ltpm_imp = store_thm( 373 "lrcc_b01_ltpm_imp", 374 ``!M pos N. lrcc (beta0 RUNION beta1) M pos N ==> 375 lrcc (beta0 RUNION beta1) (ltpm p M) pos (ltpm p N)``, 376 HO_MATCH_MP_TAC lrcc_ind THEN 377 SRW_TAC [][lrcc_rules, beta0_def, beta1_def, RUNION] THEN 378 SRW_TAC [][ltpm_subst] THEN 379 METIS_TAC [lrcc_rules, RUNION, beta0_def, beta1_def]); 380 381val lrcc_b01_ltpm_eqn = store_thm( 382 "lrcc_b01_ltpm_eqn", 383 ``lrcc (beta0 RUNION beta1) (ltpm p M) pos N = 384 lrcc (beta0 RUNION beta1) M pos (ltpm (REVERSE p) N)``, 385 METIS_TAC [lrcc_b01_ltpm_imp, pmact_inverse]); 386 387val lrcc_lcc = store_thm( 388 "lrcc_lcc", 389 ``!M pos N. lrcc R M pos N ==> lcompat_closure R M N``, 390 HO_MATCH_MP_TAC lrcc_ind THEN PROVE_TAC [lcompat_closure_rules]); 391 392val lrcc_beta_lam = store_thm( 393 "lrcc_beta_lam", 394 ``!pos v t N. 395 lrcc (beta0 RUNION beta1) (LAM v t) pos N = 396 ?pos0 N0. 397 lrcc (beta0 RUNION beta1) t pos0 N0 /\ 398 (pos = In :: pos0) /\ (N = LAM v N0)``, 399 SRW_TAC [][Once lrcc_cases, SimpLHS] THEN 400 SRW_TAC [][relationTheory.RUNION, beta0_def, beta1_def, lLAM_eq_thm, 401 ltpm_eqr, EQ_IMP_THM] THEN 402 FULL_SIMP_TAC (srw_ss()) [lrcc_b01_ltpm_eqn, pmact_flip_args] THENL [ 403 MAP_EVERY IMP_RES_TAC [lrcc_lcc, lcc_beta_FV] THEN 404 FULL_SIMP_TAC (srw_ss()) [] THEN 405 PROVE_TAC [basic_swapTheory.swapstr_def], 406 METIS_TAC [] 407 ]); 408 409val rcc_beta_matched = prove( 410 ``!M pos N. 411 labelled_redn beta M pos N ==> 412 !M'. (M = strip_label M') ==> 413 ?N'. lrcc (beta0 RUNION beta1) M' pos N' /\ 414 (N = strip_label N')``, 415 HO_MATCH_MP_TAC labelled_redn_ind THEN REPEAT STRIP_TAC THENL [ 416 PROVE_TAC [beta_matched, lrcc_rules], 417 POP_ASSUM MP_TAC THEN 418 `���s. (M' = VAR s) ��� (���t1 t2. M' = t1 @@ t2) ��� (���v t. M' = LAM v t) ��� 419 (���n v t1 t2. M' = LAMi n v t1 t2)` 420 by (Q.SPEC_THEN `M'` STRUCT_CASES_TAC lterm_CASES THEN SRW_TAC [][] THEN 421 METIS_TAC []) THEN 422 SRW_TAC [][] THENL [ 423 PROVE_TAC [strip_label_thm, lrcc_rules], 424 POP_ASSUM (Q.SPEC_THEN `LAM v t1` MP_TAC) THEN 425 SRW_TAC [][lrcc_beta_lam] THEN 426 Q.EXISTS_TAC `LAMi n v N0 t2` THEN 427 SRW_TAC [][lrcc_rules] 428 ], 429 POP_ASSUM MP_TAC THEN 430 Q.SPEC_THEN `M'` STRUCT_CASES_TAC lterm_CASES THEN 431 SRW_TAC [][] THEN 432 PROVE_TAC [strip_label_thm, lrcc_rules], 433 POP_ASSUM MP_TAC THEN SRW_TAC [][strip_label_eq_lam] THEN 434 PROVE_TAC [strip_label_thm, lrcc_rules] 435 ]); 436 437val rcc_bmatched = 438 (SIMP_RULE (srw_ss()) [GSYM RIGHT_EXISTS_IMP_THM, SKOLEM_THM] o 439 SIMP_RULE (srw_ss()) [GSYM RIGHT_FORALL_IMP_THM]) rcc_beta_matched 440 441val _ = print "Defining the lifting of reductions and paths\n"; 442 443val lift_redn_def = new_specification ( 444 "lift_redn_def", ["lift_redn"], 445 prove(``?g. 446 !pos N M'. 447 labelled_redn beta (strip_label M') pos N ==> 448 lrcc (beta0 RUNION beta1) M' pos (g M' pos N) /\ 449 (N = strip_label (g M' pos N))``, 450 STRIP_ASSUME_TAC rcc_bmatched THEN 451 Q.EXISTS_TAC `\M' pos N. f pos N M'` THEN 452 ASM_SIMP_TAC (srw_ss()) [] THEN PROVE_TAC [])); 453 454val lift_path0 = 455 ISPEC ``\X : (lterm # (term, redpos list) path). 456 let M' = FST X in 457 let q = SND X in 458 let x = first q in 459 if is_stopped q then (M', NONE) 460 else let r = first_label q in 461 let t = tail q in 462 let y' = lift_redn M' r (first t) in 463 (M', SOME (r, (y', t)))`` path_Axiom 464 465val lift_path_exists = prove( 466 ``?h:lterm -> (term, redpos list) path -> (lterm, redpos list) path. 467 (!M' x. h M' (stopped_at x) = stopped_at M') /\ 468 (!M' x r p. 469 h M' (pcons x r p) = 470 pcons M' r (h (lift_redn M' r (first p)) p))``, 471 STRIP_ASSUME_TAC lift_path0 THEN 472 Q.EXISTS_TAC `\M' p. g (M', p)` THEN 473 REPEAT STRIP_TAC THEN 474 POP_ASSUM (fn th => SIMP_TAC (srw_ss()) [SimpLHS, Once th]) THEN 475 SRW_TAC [][]); 476 477val lift_path_def = new_specification ( 478 "lift_path_def", ["lift_path"], lift_path_exists); 479 480val first_lift_path = store_thm( 481 "first_lift_path", 482 ``!M' p. first (lift_path M' p) = M'``, 483 REPEAT GEN_TAC THEN 484 Q.ISPEC_THEN `p` STRUCT_CASES_TAC path_cases THEN 485 SRW_TAC [][lift_path_def]); 486 487val strip_path_label_lift_path = store_thm( 488 "strip_path_label_lift_path", 489 ``!p M'. okpath (labelled_redn beta) p /\ (strip_label M' = first p) ==> 490 (strip_path_label (lift_path M' p) = p)``, 491 REPEAT STRIP_TAC THEN 492 ONCE_REWRITE_TAC [path_bisimulation] THEN 493 Q.EXISTS_TAC `\x y. ?M'. (x = strip_path_label (lift_path M' y)) /\ 494 okpath (labelled_redn beta) y /\ 495 (strip_label M' = first y)` THEN 496 SRW_TAC [][] THENL [ 497 PROVE_TAC [], 498 `(?x. q2 = stopped_at x) \/ 499 (?x r p'. (q2 = pcons x r p') /\ labelled_redn beta x r (first p') /\ 500 okpath (labelled_redn beta) p')` by PROVE_TAC [okpath_cases] 501 THEN SRW_TAC [][lift_path_def, strip_path_label_thm] THEN 502 FULL_SIMP_TAC (srw_ss()) [] THEN 503 PROVE_TAC [lift_redn_def] 504 ]); 505 506val strip_path_label_okpath = store_thm( 507 "strip_path_label_okpath", 508 ``!M' p. okpath (labelled_redn beta) p /\ (first p = strip_label M') ==> 509 okpath (lrcc (beta0 RUNION beta1)) (lift_path M' p)``, 510 Q_TAC SUFF_TAC 511 `!p'. (?M' p. okpath (labelled_redn beta) p /\ 512 (first p = strip_label M') /\ 513 (p' = lift_path M' p)) ==> 514 okpath (lrcc (beta0 RUNION beta1)) p'` THEN1 PROVE_TAC [] THEN 515 HO_MATCH_MP_TAC okpath_co_ind THEN 516 SIMP_TAC (srw_ss()) [Once okpath_cases, SimpL ``(==>)``] THEN 517 SIMP_TAC (srw_ss() ++ DNF_ss) [lift_path_def, first_lift_path] THEN 518 PROVE_TAC [lift_redn_def]); 519 520val lemma11_2_2 = store_thm( 521 "lemma11_2_2", 522 ``!sigma. 523 okpath (labelled_redn beta) sigma ==> 524 !M'. (strip_label M' = first sigma) ==> 525 ?sigma'. (first sigma' = M') /\ 526 (strip_path_label sigma' = sigma) /\ 527 okpath (lrcc (beta0 RUNION beta1)) sigma'``, 528 REPEAT STRIP_TAC THEN 529 Q.EXISTS_TAC `lift_path M' sigma` THEN 530 SRW_TAC [][first_lift_path, strip_path_label_okpath, 531 strip_path_label_lift_path]); 532 533(* support the notation of saying that a redex position is \in a 534 term *) 535 536val is_redex_occurrence_def = 537 Define`is_redex_occurrence pos M = ?N. labelled_redn beta M pos N`; 538 539val is_redex_occurrence_thm = store_thm( 540 "is_redex_occurrence_thm", 541 ``(!s p. is_redex_occurrence p (VAR s) = F) /\ 542 (!t u p. is_redex_occurrence p (t @@ u) <=> 543 is_abs t /\ (p = []) \/ 544 (p = Lt :: TL p) /\ is_redex_occurrence (TL p) t \/ 545 (p = Rt :: TL p) /\ is_redex_occurrence (TL p) u) /\ 546 (!v t p. is_redex_occurrence p (LAM v t) <=> 547 (p = In :: TL p) /\ is_redex_occurrence (TL p) t)``, 548 SIMP_TAC pureSimps.pure_ss [is_redex_occurrence_def] THEN 549 REPEAT CONJ_TAC THEN 550 SRW_TAC [][SimpLHS, Once labelled_redn_cases] THEN 551 SRW_TAC [][beta_def, EQ_IMP_THM] THENL [ 552 PROVE_TAC [], 553 PROVE_TAC [], 554 PROVE_TAC [is_abs_thm, term_CASES], 555 FIRST_X_ASSUM SUBST_ALL_TAC THEN 556 FULL_SIMP_TAC (srw_ss()) [] THEN PROVE_TAC [], 557 FIRST_X_ASSUM SUBST_ALL_TAC THEN 558 FULL_SIMP_TAC (srw_ss()) [] THEN PROVE_TAC [], 559 FULL_SIMP_TAC (srw_ss()) [LAM_eq_thm] THEN 560 PROVE_TAC [labelled_redn_beta_sub, fresh_tpm_subst], 561 PROVE_TAC [] 562 ]); 563 564val redexes_all_occur_def = 565 Define`redexes_all_occur posS M = 566 !s. s IN posS ==> is_redex_occurrence s M` 567 568val _ = overload_on("IN", ``is_redex_occurrence``); 569val _ = overload_on("SUBSET", ``redexes_all_occur``); 570 571val redex_posns_redex_occurrence = store_thm( 572 "redex_posns_redex_occurrence", 573 ``!t. redex_posns t = {p | p IN t}``, 574 HO_MATCH_MP_TAC simple_induction THEN 575 SRW_TAC [][redex_posns_thm, is_redex_occurrence_thm, EXTENSION] THEN 576 SRW_TAC [][EQ_IMP_THM] THEN PROVE_TAC [lemma14a, listTheory.TL]); 577 578val IN_term_IN_redex_posns = store_thm( 579 "IN_term_IN_redex_posns", 580 ``!x M. x IN M <=> x IN redex_posns M``, 581 SRW_TAC [][redex_posns_redex_occurrence]); 582 583val ordering = prove( 584 ``(?f:lterm -> num -> 'a. P f) = (?f. P (\n t. f t n))``, 585 EQ_TAC THEN SRW_TAC [][] THENL [ 586 Q.EXISTS_TAC `��t n. f n t` THEN SRW_TAC [ETA_ss][], 587 METIS_TAC [] 588 ]); 589val n_posns_exists = 590 parameter_ltm_recursion 591 |> INST_TYPE [alpha |-> ``:posn set``, ``:��`` |-> ``:num``] 592 |> Q.INST [`vr` |-> `\s n. {}`, `A` |-> `{}`, 593 `apm` |-> `discrete_pmact`, 594 `ap` |-> `\r1 r2 t1 t2 n. 595 IMAGE (CONS Lt) (r1 n) ��� IMAGE (CONS Rt) (r2 n)`, 596 `lm` |-> `\r v t n. IMAGE (CONS In) (r n)`, 597 `li` |-> `\r1 r2 m v t1 t2 n. 598 IMAGE (APPEND [Lt; In]) (r1 n) UNION 599 IMAGE (CONS Rt) (r2 n) UNION 600 (if n = m then {[]} else {})`, 601 `ppm` |-> `discrete_pmact`] 602 |> SIMP_RULE (srw_ss()) [fnpm_def, ordering] 603 |> CONV_RULE (DEPTH_CONV (nomdatatype.rename_vars [("p", "n")]) THENC 604 BINDER_CONV (RAND_CONV (ONCE_REWRITE_CONV [EQ_SYM_EQ]))) 605 606val n_posns_def = new_specification("n_posns_def", ["n_posns"], 607 n_posns_exists); 608val _ = export_rewrites ["n_posns_def"] 609 610val n_posns_vsubst_invariant = Store_Thm( 611 "n_posns_vsubst_invariant", 612 ``!M m u w. n_posns m ([VAR u/w] M) = n_posns m M``, 613 REPEAT GEN_TAC THEN Q.ID_SPEC_TAC `M` THEN 614 HO_MATCH_MP_TAC lterm_bvc_induction THEN 615 Q.EXISTS_TAC `{u;w}` THEN SRW_TAC [][lSUB_VAR]); 616 617(* ---------------------------------------------------------------------- 618 n_label : labels (some of) a term's redexes, producing an lterm 619 ---------------------------------------------------------------------- *) 620 621(* first a little constant to apply t2 to t1, creating a LAMi redex, if the 622 left argument t1 is a LAM. *) 623val ordering = prove( 624 ``(?f:lterm -> num # lterm -> lterm. P f) <=> 625 (?f. P (\t1 (n,t2). f n t1 t2))``, 626 SRW_TAC [][EQ_IMP_THM] THENL [ 627 Q.EXISTS_TAC `\n t1 t2. f t1 (n, t2)` THEN SRW_TAC [][] THEN 628 CONV_TAC (DEPTH_CONV pairLib.PAIRED_ETA_CONV) THEN SRW_TAC [ETA_ss][], 629 METIS_TAC [] 630 ]) 631val rAPP_exists = 632 parameter_ltm_recursion 633 |> INST_TYPE [alpha |-> ``:lterm``, 634 ``:��`` |-> ``:num # lterm``] 635 |> Q.INST [`ap` |-> `\rt ru t u (n,p). (t @@ u) @@ p`, 636 `vr` |-> `\s (n,p). VAR s @@ p`, 637 `lm` |-> `\rt v t (n,p). LAMi n v t p`, 638 `li` |-> `\rt ru n v t u (m,p). LAMi n v t u @@ p`, 639 `apm` |-> `lterm_pmact`, `ppm` |-> `pair_pmact discrete_pmact lterm_pmact`, `A` |-> `{}`] 640 |> SIMP_RULE (srw_ss()) [ltpm_ALPHA, ltpm_ALPHAi, ordering, 641 pairTheory.FORALL_PROD] 642 |> CONV_RULE (DEPTH_CONV 643 (nomdatatype.rename_vars [("p_1", "n"), ("p_2", "M")])) 644 |> nomdatatype.elim_unnecessary_atoms 645 {finite_fv = labelledTermsTheory.FINITE_FV} [] 646 647val rAPP_def = new_specification("rAPP_def", ["rAPP"], rAPP_exists) 648val _ = export_rewrites ["rAPP_def"] 649 650val rAPP_LAMs = Store_Thm( 651 "rAPP_LAMs", 652 ``(rAPP n (LAM v t) M = LAMi n v t M) ��� 653 (rAPP m (LAMi n v t1 t2) M = LAMi n v t1 t2 @@ M)``, 654 CONJ_TAC THENL [ 655 Q_TAC (NEW_TAC "z") `FV t ��� FV M` THEN 656 `(LAM v t = LAM z (ltpm [(z,v)] t)) ��� 657 (LAMi n v t M = LAMi n z (ltpm [(z,v)] t) M)` 658 by SRW_TAC [][ltpm_ALPHA, ltpm_ALPHAi] THEN 659 SRW_TAC [][], 660 Q_TAC (NEW_TAC "z") `FV t1 ��� FV M` THEN 661 `(LAMi n v t1 t2 = LAMi n z (ltpm [(z,v)] t1) t2)` 662 by SRW_TAC [][ltpm_ALPHAi] THEN 663 SRW_TAC [][] 664 ]) 665 666val FINITE_UPPERBOUND_SETS = store_thm( 667 "FINITE_UPPERBOUND_SETS", 668 ``!L P. FINITE L /\ (!s. s IN P ==> s SUBSET L) ==> FINITE P``, 669 Q_TAC SUFF_TAC `!L. FINITE L ==> !P. (!s. s IN P ==> s SUBSET L) ==> 670 FINITE P` 671 THEN1 METIS_TAC [] THEN 672 HO_MATCH_MP_TAC FINITE_INDUCT THEN SRW_TAC [][] THENL [ 673 Q_TAC SUFF_TAC `(P = {}) \/ (P = {{}})` THEN1 SRW_TAC [][DISJ_IMP_THM] THEN 674 Q.ISPEC_THEN `P` FULL_STRUCT_CASES_TAC SET_CASES THEN SRW_TAC [][] THEN 675 ONCE_REWRITE_TAC [EXTENSION] THEN SRW_TAC [][] THEN 676 SRW_TAC [][EQ_IMP_THM], 677 `P = {s | s IN P /\ e IN s} UNION {s | s IN P /\ ~(e IN s)}` 678 by (SIMP_TAC (srw_ss()) [EXTENSION] THEN METIS_TAC []) THEN 679 POP_ASSUM SUBST1_TAC THEN SRW_TAC [][] THENL [ 680 `{s | s IN P /\ e IN s} = 681 IMAGE ((INSERT) e) (IMAGE (\s. s DELETE e) {s | s IN P /\ e IN s})` 682 by (ONCE_REWRITE_TAC [EXTENSION] THEN 683 SRW_TAC [DNF_ss][] THEN 684 SRW_TAC [][EQ_IMP_THM] THENL [ 685 Q.EXISTS_TAC `x` THEN SRW_TAC [][EXTENSION] THEN 686 Cases_on `x' = e` THEN SRW_TAC [][], 687 Q.MATCH_ABBREV_TAC `e INSERT (s DELETE e) IN P` THEN 688 `e INSERT s DELETE e = s` 689 by (SRW_TAC [][EXTENSION] THEN 690 Cases_on `x = e` THEN SRW_TAC [][]) THEN 691 SRW_TAC [][], 692 SRW_TAC [][] 693 ]) THEN 694 POP_ASSUM SUBST1_TAC THEN 695 MATCH_MP_TAC IMAGE_FINITE THEN 696 FIRST_X_ASSUM MATCH_MP_TAC THEN SRW_TAC [][] THEN 697 FULL_SIMP_TAC (srw_ss()) [SUBSET_DEF] THEN METIS_TAC [], 698 FIRST_X_ASSUM MATCH_MP_TAC THEN SRW_TAC [][] THEN 699 FULL_SIMP_TAC (srw_ss()) [SUBSET_DEF] THEN METIS_TAC [] 700 ] 701 ]); 702 703val ltpm_if = prove( 704 ``ltpm [(x,y)] (if P then M else N) = 705 if P then ltpm [(x,y)] M else ltpm [(x,y)] N``, 706 SRW_TAC [][]); 707 708open nomdatatype 709val ordering = prove( 710 ``(?f : term -> num # posn set -> lterm. P f) <=> 711 (?f. P (\t (n,ps). f n t ps))``, 712 EQ_TAC THEN STRIP_TAC THENL [ 713 Q.EXISTS_TAC `\n t ps. f t (n, ps)` THEN SRW_TAC [][] THEN 714 CONV_TAC (DEPTH_CONV pairLib.PAIRED_ETA_CONV) THEN 715 SRW_TAC [ETA_ss][], 716 METIS_TAC [] 717 ]) ; 718val nlabel_exists = 719 parameter_tm_recursion 720 |> INST_TYPE [alpha |-> ``:lterm``, ``:��`` |-> ``:num # posn set``] 721 |> Q.INST 722 [`apm` |-> `lterm_pmact`, `A` |-> `{}`, `ppm` |-> `discrete_pmact`, 723 `vr` |-> `\s nps. VAR s`, 724 `ap` |-> `\rt ru t u (n,ps). 725 if [] IN ps then 726 rAPP n 727 (rt (n,{p | Lt::p IN ps})) 728 (ru (n,{p | Rt::p IN ps})) 729 else 730 (rt (n,{p | Lt::p IN ps})) @@ 731 (ru (n,{p | Rt::p IN ps}))`, 732 `lm` |-> `\rt v t (n,ps). 733 LAM v (rt (n, 734 {p | In::p IN ps} INTER redex_posns t))`] 735 |> SIMP_RULE (srw_ss()) [pairTheory.FORALL_PROD, fnpm_def, 736 ltpm_if, ordering] 737 |> prove_alpha_fcbhyp {ppm = ``discrete_pmact : (num # posn set) pmact``, 738 alphas = [ltpm_ALPHA], 739 rwts = []} 740 |> CONV_RULE (DEPTH_CONV 741 (rename_vars [("p_1", "n"), ("p_2", "ps")])) 742 743val nlabel_def = new_specification("nlabel_def", ["nlabel"], nlabel_exists) 744 745val FV_rAPP = Store_Thm( 746 "FV_rAPP", 747 ``!M. FV (rAPP n M N) = FV M UNION FV N``, 748 HO_MATCH_MP_TAC lterm_bvc_induction THEN Q.EXISTS_TAC `FV N` THEN 749 SRW_TAC [][]); 750 751val FV_nlabel = Store_Thm( 752 "FV_nlabel", 753 ``!M n ps. FV (nlabel n M ps) = FV M``, 754 HO_MATCH_MP_TAC simple_induction THEN 755 SRW_TAC [][nlabel_def] THEN SRW_TAC [][]); 756 757val rAPP_vsubst_commutes = store_thm( 758 "rAPP_vsubst_commutes", 759 ``!M. [VAR v/u](rAPP n M N) = rAPP n ([VAR v/u]M) ([VAR v/u]N)``, 760 HO_MATCH_MP_TAC lterm_bvc_induction THEN 761 Q.EXISTS_TAC `FV N UNION {u;v}` THEN SRW_TAC [][lSUB_VAR]); 762 763val nlabel_vsubst_commutes = store_thm( 764 "nlabel_vsubst_commutes", 765 ``!n M w u ps. nlabel n ([VAR w/u] M) ps = [VAR w/u](nlabel n M ps)``, 766 REPEAT GEN_TAC THEN 767 MAP_EVERY Q.ID_SPEC_TAC [`ps`, `M`] THEN 768 HO_MATCH_MP_TAC nc_INDUCTION2 THEN Q.EXISTS_TAC `{u;w}` THEN 769 SRW_TAC [][SUB_THM, nlabel_def, SUB_VAR] THEN 770 SRW_TAC [][rAPP_vsubst_commutes]); 771 772val strip_label_rAPP = Store_Thm( 773 "strip_label_rAPP", 774 ``strip_label (rAPP n M N) = strip_label M @@ strip_label N``, 775 Q.SPEC_THEN `M` STRUCT_CASES_TAC lterm_CASES THEN SRW_TAC [][]); 776val strip_label_nlabel = Store_Thm( 777 "strip_label_nlabel", 778 ``!M ps. strip_label (nlabel n M ps) = M``, 779 HO_MATCH_MP_TAC simple_induction THEN SRW_TAC [][nlabel_def] THEN 780 SRW_TAC [][]); 781 782val not_abs_rAPP_APP = Store_Thm( 783 "not_abs_rAPP_APP", 784 ``~is_abs (strip_label M) ==> (rAPP n M N = M @@ N)``, 785 Q.SPEC_THEN `M` STRUCT_CASES_TAC lterm_CASES THEN SRW_TAC [][]); 786 787val nlabel_eq_inter = store_thm( 788 "nlabel_eq_inter", 789 ``!M m ps. nlabel m M ps = nlabel m M (ps INTER redex_posns M)``, 790 ONCE_REWRITE_TAC [EQ_SYM_EQ] THEN 791 HO_MATCH_MP_TAC simple_induction THEN SRW_TAC [][nlabel_def] THENL [ 792 SRW_TAC [][redex_posns_thm] THEN 793 Cases_on `is_abs M` THEN FULL_SIMP_TAC (srw_ss()) [] THEN 794 SRW_TAC [][GSPEC_AND], 795 SRW_TAC [][redex_posns_thm] THEN SRW_TAC [][GSPEC_AND] 796 ]); 797 798val nlabel_thm = store_thm( 799 "nlabel_thm", 800 ``(!n s ps. nlabel n (VAR s) ps = VAR s) /\ 801 (!b v t u ps. 802 nlabel n (LAM v t @@ u) ps = 803 if [] IN ps then 804 LAMi n v (nlabel n t { p | Lt::In::p IN ps}) 805 (nlabel n u { p | Rt :: p IN ps}) 806 else 807 LAM v (nlabel n t { p | Lt::In::p IN ps}) @@ 808 (nlabel n u { p | Rt :: p IN ps})) /\ 809 (!t u n ps. 810 ~is_abs t ==> (nlabel n (t @@ u) ps = 811 nlabel n t { p | Lt::p IN ps} @@ 812 nlabel n u { p | Rt::p IN ps})) /\ 813 (!v t n ps. nlabel n (LAM v t) ps = 814 LAM v (nlabel n t { p | In::p IN ps }))``, 815 SRW_TAC [][nlabel_def, GSYM nlabel_eq_inter]); 816 817val n_posns_nlabel = store_thm( 818 "n_posns_nlabel", 819 ``!M n ps. (n_posns n (nlabel n M ps) = ps INTER redex_posns M) /\ 820 !m. ~(m = n) ==> (n_posns m (nlabel n M ps) = {})``, 821 HO_MATCH_MP_TAC simple_induction THEN 822 SRW_TAC [][n_posns_def, nlabel_thm, redex_posns_thm] THENL [ 823 `?var b. M = LAM var b` by PROVE_TAC [term_CASES, is_abs_thm] THEN 824 FULL_SIMP_TAC (srw_ss())[nlabel_thm, n_posns_def, redex_posns_thm] THEN 825 SRW_TAC [][n_posns_def] THENL [ 826 `IMAGE (APPEND [Lt; In]) 827 (n_posns n (nlabel n b {p | Lt::In::p IN ps})) = 828 IMAGE (CONS Lt) 829 (IMAGE (CONS In) 830 (n_posns n (nlabel n b 831 { p | In :: p IN { q | Lt :: q IN ps}})))` by 832 SRW_TAC [][EXTENSION, GSYM RIGHT_EXISTS_AND_THM] THEN 833 ASM_SIMP_TAC bool_ss [] THEN 834 SRW_TAC [][EXTENSION, GSYM RIGHT_EXISTS_AND_THM, 835 GSYM LEFT_EXISTS_AND_THM] THEN 836 EQ_TAC THEN SRW_TAC [][] THEN SRW_TAC [][], 837 `nlabel n b { p | Lt::In::p IN ps} = 838 nlabel n b { p | In::p IN { q | Lt :: q IN ps}}` by 839 SRW_TAC [][EXTENSION] THEN 840 ASM_SIMP_TAC bool_ss [] THEN 841 SRW_TAC [][EXTENSION, EQ_IMP_THM] THEN SRW_TAC [][] THEN 842 PROVE_TAC [] 843 ], 844 `?var b. M = LAM var b` by PROVE_TAC [term_CASES, is_abs_thm] THEN 845 FULL_SIMP_TAC (srw_ss()) [nlabel_thm, n_posns_def, redex_posns_thm, 846 IMAGE_EQ_EMPTY] THEN 847 SRW_TAC [][n_posns_def, IMAGE_EQ_EMPTY] THEN 848 `nlabel n b { p | Lt::In::p IN ps} = 849 nlabel n b { p | In::p IN { q | Lt :: q IN ps}}` by 850 SRW_TAC [][EXTENSION] THEN 851 ASM_SIMP_TAC bool_ss [], 852 SRW_TAC [][EXTENSION, EQ_IMP_THM] THEN SRW_TAC [][], 853 SRW_TAC [][EXTENSION, EQ_IMP_THM] THEN SRW_TAC [][] 854 ]); 855 856(* notation (M, S) in 11.2.3 correponds to ``nlabel 0 M S`` *) 857 858(*val _ = add_rule {block_style = (AroundEachPhrase, (PP.INCONSISTENT, 2)), 859 fixity = Infix(NONASSOC, 510), 860 paren_style = OnlyIfNecessary, 861 pp_elements = [HardSpace 1, TOK "from", HardSpace 1, TM, 862 BreakSpace(1,0), TOK "to", HardSpace 1], 863 term_name = "from_to"} 864 865 866val from_to_def = 867 Define`sigma from M to N = 868 finite sigma /\ (first sigma = M) /\ (last sigma = N)`; 869*) 870 871 872val lv_posns_def = Define`lv_posns v t = v_posns v (strip_label t)` 873 874val lv_posns_thm = store_thm( 875 "lv_posns_thm", 876 ``(!v s. lv_posns v (VAR s : lterm) = if s = v then {[]} else {}) /\ 877 (!v M N. lv_posns v (M @@ N : lterm) = 878 IMAGE (CONS Lt) (lv_posns v M) UNION 879 IMAGE (CONS Rt) (lv_posns v N)) /\ 880 (!v M. lv_posns v (LAM v M : lterm) = {}) /\ 881 (!v w M. ~(v = w) ==> 882 (lv_posns v (LAM w M:lterm) = IMAGE (CONS In) (lv_posns v M))) /\ 883 (!v n M N. lv_posns v (LAMi n v M N:lterm) = 884 IMAGE (CONS Rt) (lv_posns v N)) /\ 885 (!v w n M N. 886 ~(v = w) ==> 887 (lv_posns v (LAMi n w M N:lterm) = 888 IMAGE (APPEND [Lt; In]) (lv_posns v M) UNION 889 IMAGE (CONS Rt) (lv_posns v N)))``, 890 SRW_TAC [][lv_posns_def, v_posns_thm, strip_label_thm, 891 GSYM IMAGE_COMPOSE, 892 combinTheory.o_DEF] THEN 893 Q_TAC SUFF_TAC `(\x. Lt::In::x) = APPEND [Lt;In]` THEN1 SRW_TAC [][] THEN 894 SRW_TAC [][FUN_EQ_THM]); 895 896val lv_posns_vsubst = store_thm( 897 "lv_posns_vsubst", 898 ``!M x y z. 899 lv_posns x ([VAR y/z] M) = 900 if x = y then lv_posns x M UNION lv_posns z M 901 else if x = z then {} else lv_posns x M``, 902 SRW_TAC [][lv_posns_def, v_posns_vsubst, strip_label_subst, 903 strip_label_thm]); 904 905val n_posns_sub = store_thm( 906 "n_posns_sub", 907 ``!M t v n. n_posns n ([t/v] M) = 908 n_posns n M UNION 909 { APPEND vp np | vp IN lv_posns v M /\ np IN n_posns n t }``, 910 REPEAT GEN_TAC THEN Q.ID_SPEC_TAC `M` THEN 911 HO_MATCH_MP_TAC lterm_bvc_induction THEN 912 Q.EXISTS_TAC `v INSERT FV t` THEN SRW_TAC [][] THENL [ 913 SRW_TAC [][lv_posns_thm, lSUB_THM, n_posns_def, EXTENSION], 914 915 SRW_TAC [][lv_posns_thm, lSUB_THM, n_posns_def, 916 EXTENSION, EQ_IMP_THM, 917 GSYM RIGHT_EXISTS_AND_THM, GSYM LEFT_EXISTS_AND_THM, 918 RIGHT_AND_OVER_OR, LEFT_AND_OVER_OR, EXISTS_OR_THM] THEN 919 PROVE_TAC [], 920 921 SRW_TAC [][lSUB_THM, n_posns_def, lv_posns_thm] THEN 922 ASM_SIMP_TAC (srw_ss()) [EXTENSION] THEN GEN_TAC THEN 923 EQ_TAC THEN SRW_TAC [][GSYM RIGHT_EXISTS_AND_THM, lv_posns_vsubst, 924 GSYM LEFT_EXISTS_AND_THM] THEN 925 PROVE_TAC [], 926 927 SRW_TAC [][lSUB_THM, n_posns_def, lv_posns_thm, lv_posns_vsubst] THEN 928 SRW_TAC [][EXTENSION, EQ_IMP_THM, 929 GSYM RIGHT_EXISTS_AND_THM, GSYM LEFT_EXISTS_AND_THM, 930 RIGHT_AND_OVER_OR, LEFT_AND_OVER_OR, EXISTS_OR_THM] THEN 931 PROVE_TAC [], 932 933 SRW_TAC [][lSUB_THM, n_posns_def, lv_posns_thm, lv_posns_vsubst] THEN 934 SRW_TAC [][EXTENSION, EQ_IMP_THM, 935 GSYM RIGHT_EXISTS_AND_THM, GSYM LEFT_EXISTS_AND_THM, 936 RIGHT_AND_OVER_OR, LEFT_AND_OVER_OR, EXISTS_OR_THM] THEN 937 PROVE_TAC [] 938 ]); 939 940val lrcc_new_labels = store_thm( 941 "lrcc_new_labels", 942 ``!x r y. 943 lrcc (beta0 RUNION beta1) x r y ==> 944 !n. (n_posns n x = EMPTY) ==> (n_posns n y = EMPTY)``, 945 HO_MATCH_MP_TAC lrcc_ind THEN REPEAT CONJ_TAC THENL [ 946 SIMP_TAC (srw_ss()) [beta0_def, relationTheory.RUNION, beta1_def, 947 DISJ_IMP_THM, FORALL_AND_THM, 948 GSYM LEFT_FORALL_IMP_THM, n_posns_def, 949 EMPTY_UNION, 950 IMAGE_EQ_EMPTY, n_posns_sub] THEN 951 SRW_TAC [][EXTENSION], 952 SIMP_TAC (srw_ss()) [n_posns_def, IMAGE_EQ_EMPTY], 953 SIMP_TAC (srw_ss()) [n_posns_def, IMAGE_EQ_EMPTY], 954 SIMP_TAC (srw_ss()) [n_posns_def, IMAGE_EQ_EMPTY], 955 SIMP_TAC (srw_ss()) [n_posns_def, IMAGE_EQ_EMPTY], 956 SIMP_TAC (srw_ss()) [n_posns_def, IMAGE_EQ_EMPTY] 957 ]); 958 959val nlabel_null_labelling = store_thm( 960 "nlabel_null_labelling", 961 ``!M n. nlabel n M {} = null_labelling M``, 962 HO_MATCH_MP_TAC simple_induction THEN 963 SRW_TAC [][nlabel_thm] THEN 964 Cases_on `is_abs M` THENL [ 965 `?var b. M = LAM var b` by PROVE_TAC [term_CASES, is_abs_thm] THEN 966 FULL_SIMP_TAC (srw_ss()) [nlabel_thm], 967 SRW_TAC [][nlabel_thm] 968 ]); 969 970val n_posns_strip_label = store_thm( 971 "n_posns_strip_label", 972 ``!M' n. n_posns n M' SUBSET (strip_label M')``, 973 HO_MATCH_MP_TAC simple_lterm_induction THEN 974 SRW_TAC [][redexes_all_occur_def, n_posns_def, strip_label_thm, 975 is_redex_occurrence_thm] 976 THENL [ 977 PROVE_TAC [], 978 PROVE_TAC [], 979 SRW_TAC [][] THEN PROVE_TAC [], 980 PROVE_TAC [], 981 PROVE_TAC [], 982 FULL_SIMP_TAC (srw_ss() ++ COND_elim_ss) [] THEN RES_TAC 983 ]); 984 985val rpos_UNION_11 = store_thm( 986 "rpos_UNION_11", 987 ``!s1 s2 t1 t2. 988 (IMAGE (CONS Lt) s1 UNION IMAGE (CONS Rt) s2 = 989 IMAGE (CONS Lt) t1 UNION IMAGE (CONS Rt) t2) <=> 990 (s1 = t1) /\ (s2 = t2)``, 991 SIMP_TAC (srw_ss()) [EQ_IMP_THM, EXTENSION, 992 DISJ_IMP_THM, FORALL_AND_THM, 993 GSYM LEFT_FORALL_IMP_THM] THEN 994 PROVE_TAC []); 995 996val IMAGE_CONS_11 = store_thm( 997 "IMAGE_CONS_11", 998 ``!h s1 s2. (IMAGE (CONS h) s1 = IMAGE (CONS h) s2) = (s1 = s2)``, 999 SIMP_TAC (srw_ss()) [EQ_IMP_THM, EXTENSION, 1000 DISJ_IMP_THM, FORALL_AND_THM, 1001 GSYM LEFT_FORALL_IMP_THM]); 1002 1003val IMAGE_APPEND = prove( 1004 ``!h t s X. IMAGE (APPEND (h::t)) X = IMAGE (CONS h) (IMAGE (APPEND t) X)``, 1005 SIMP_TAC (srw_ss()) [EXTENSION, EQ_IMP_THM, 1006 GSYM LEFT_FORALL_IMP_THM]); 1007 1008val LAMI_partly_11 = prove( 1009 ``!x y z w a b. (LAMi x y z w = LAMi x y a b) <=> (z = a) /\ (w = b)``, 1010 SRW_TAC [][lLAMi_eq_thm]) 1011 1012 1013val stripped_equal = store_thm( 1014 "stripped_equal", 1015 ``!M' N'. (strip_label M' = strip_label N') /\ ~(M' = N') ==> 1016 ?n. ~(n_posns n M' = n_posns n N')``, 1017 HO_MATCH_MP_TAC simple_lterm_induction THEN 1018 ASM_SIMP_TAC (srw_ss()) [strip_label_thm] THEN 1019 REPEAT CONJ_TAC THENL [ 1020 SRW_TAC [][strip_label_thm] THEN 1021 Q.PAT_X_ASSUM `X = strip_label yy` (MP_TAC o SYM) THEN 1022 Q.SPEC_THEN `N'` FULL_STRUCT_CASES_TAC lterm_CASES THEN SRW_TAC [][] THEN 1023 FULL_SIMP_TAC (srw_ss()) [], 1024 SRW_TAC [][strip_label_thm] THEN 1025 Q.PAT_X_ASSUM `X = strip_label yy` (MP_TAC o SYM) THEN 1026 `(���s. N' = VAR s) ��� (���t1 t2. N' = t1 @@ t2) ��� (���v t. N' = LAM v t) ��� 1027 (���n v t1 t2. N' = LAMi n v t1 t2)` 1028 by (Q.SPEC_THEN `N'` FULL_STRUCT_CASES_TAC lterm_CASES THEN 1029 SRW_TAC [][] THEN METIS_TAC []) THEN 1030 SRW_TAC [][] THEN 1031 FULL_SIMP_TAC (srw_ss()) [rpos_UNION_11] THENL [ 1032 METIS_TAC [], 1033 METIS_TAC [], 1034 Q.EXISTS_TAC `n` THEN SRW_TAC [][EXTENSION] THEN 1035 Q.EXISTS_TAC `[]` THEN SRW_TAC [][] 1036 ], 1037 SRW_TAC [][strip_label_thm] THEN 1038 Q.PAT_X_ASSUM `X = strip_label yy` (MP_TAC o SYM) THEN 1039 SRW_TAC [][strip_label_eq_lam] THEN 1040 SRW_TAC [][IMAGE_CONS_11] THEN PROVE_TAC [], 1041 MAP_EVERY Q.X_GEN_TAC [`v`, `n`, `t2`, `t1`] THEN 1042 SRW_TAC [][strip_label_thm] THEN 1043 Q.PAT_X_ASSUM `X = strip_label yy` (MP_TAC o SYM) THEN 1044 SRW_TAC [][strip_label_eq_redex] THENL [ 1045 Q.EXISTS_TAC `n` THEN SRW_TAC [][EXTENSION] THEN 1046 Q.EXISTS_TAC `[]` THEN SRW_TAC [][], 1047 Cases_on `n = n'` THENL [ 1048 FULL_SIMP_TAC (srw_ss()) [] THENL [ 1049 Q.PAT_X_ASSUM `MM:lterm ��� NN` MP_TAC THEN 1050 Q.MATCH_ABBREV_TAC `MM ��� NN ==> GOAL` THEN 1051 Q.UNABBREV_TAC `GOAL` THEN markerLib.RM_ALL_ABBREVS_TAC THEN 1052 STRIP_TAC THEN 1053 `?m. ~(n_posns m MM = n_posns m NN)` by METIS_TAC [] THEN 1054 Q.EXISTS_TAC `m` THEN 1055 FULL_SIMP_TAC (srw_ss()) [EXTENSION] THEN 1056 Q.EXISTS_TAC `Lt::In::x` THEN 1057 SRW_TAC [][] THEN SRW_TAC [][], 1058 1059 Q.PAT_X_ASSUM `MM:lterm ��� NN` MP_TAC THEN 1060 Q.MATCH_ABBREV_TAC `MM ��� NN ==> GOAL` THEN 1061 Q.UNABBREV_TAC `GOAL` THEN markerLib.RM_ALL_ABBREVS_TAC THEN 1062 STRIP_TAC THEN 1063 `?m. ~(n_posns m MM = n_posns m NN)` by METIS_TAC [] THEN 1064 Q.EXISTS_TAC `m` THEN 1065 FULL_SIMP_TAC (srw_ss()) [EXTENSION] THEN 1066 Q.EXISTS_TAC `Rt::x` THEN 1067 SRW_TAC [][] THEN SRW_TAC [][] 1068 ], 1069 Q.EXISTS_TAC `n'` THEN SRW_TAC [][EXTENSION] THEN 1070 Q.EXISTS_TAC `[]` THEN SRW_TAC [][] 1071 ] 1072 ] 1073 ]); 1074 1075val nlabel_app_no_nil = store_thm( 1076 "nlabel_app_no_nil", 1077 ``!t u ps. 1078 ~([] IN ps) ==> 1079 (nlabel n (t @@ u) ps = 1080 nlabel n t { p | Lt::p IN ps} @@ nlabel n u { p | Rt::p IN ps})``, 1081 REPEAT STRIP_TAC THEN 1082 Cases_on `is_abs t` THENL [ 1083 `?var b. t = LAM var b` by PROVE_TAC [term_CASES, is_abs_thm] THEN 1084 SRW_TAC [][nlabel_thm], 1085 SRW_TAC [][nlabel_thm] 1086 ]); 1087 1088val nlabel_n_posns = store_thm( 1089 "nlabel_n_posns", 1090 ``!M' n. (!m. ~(m = n) ==> (n_posns m M' = {})) ==> 1091 (nlabel n (strip_label M') (n_posns n M') = M')``, 1092 HO_MATCH_MP_TAC simple_lterm_induction THEN 1093 REPEAT CONJ_TAC THENL [ 1094 SRW_TAC [][strip_label_thm, nlabel_thm], 1095 SRW_TAC [][n_posns_def, nlabel_thm, strip_label_thm, 1096 IMAGE_EQ_EMPTY, EMPTY_UNION, 1097 nlabel_app_no_nil], 1098 SRW_TAC [][n_posns_def, nlabel_thm, strip_label_thm, 1099 IMAGE_EQ_EMPTY], 1100 SRW_TAC [][n_posns_def, nlabel_thm, strip_label_thm, 1101 IMAGE_EQ_EMPTY, 1102 EMPTY_UNION] THEN 1103 SRW_TAC [][] THENL [ 1104 FULL_SIMP_TAC (srw_ss()) [], 1105 FULL_SIMP_TAC (srw_ss() ++ COND_elim_ss) [] THEN METIS_TAC [] 1106 ] 1107 ]); 1108 1109val labelled_term_component_equality = store_thm( 1110 "labelled_term_component_equality", 1111 ``!M' N'. (M' = N') <=> (strip_label M' = strip_label N') /\ 1112 (!n. n_posns n M' = n_posns n N')``, 1113 SRW_TAC [][EQ_IMP_THM] THEN SPOSE_NOT_THEN ASSUME_TAC THEN 1114 PROVE_TAC [stripped_equal]); 1115 1116val residuals_exist = store_thm( 1117 "residuals_exist", 1118 ``!sigma. okpath (labelled_redn beta) sigma /\ finite sigma ==> 1119 !posS. 1120 ?posS'. 1121 (last (lift_path (nlabel 0 (first sigma) posS) sigma) = 1122 nlabel 0 (last sigma) posS') /\ 1123 posS' SUBSET redex_posns (last sigma)``, 1124 HO_MATCH_MP_TAC finite_okpath_ind THEN 1125 SIMP_TAC (srw_ss()) [first_thm, last_thm, lift_path_def] THEN 1126 REPEAT CONJ_TAC THENL [ 1127 PROVE_TAC [nlabel_eq_inter, IN_INTER, SUBSET_DEF], 1128 MAP_EVERY Q.X_GEN_TAC [`x`,`r`,`p`] THEN REPEAT STRIP_TAC THEN 1129 Q.ABBREV_TAC `y = first p` THEN 1130 Q.ABBREV_TAC `x' = nlabel 0 x posS` THEN 1131 Q.ABBREV_TAC `y' = lift_redn x' r y` THEN 1132 Q_TAC SUFF_TAC `?posS'. (y' = nlabel 0 y posS')` THEN1 1133 PROVE_TAC [] THEN 1134 `strip_label x' = x` by PROVE_TAC [strip_label_nlabel] THEN 1135 `lrcc (beta0 RUNION beta1) x' r y' /\ (strip_label y' = y)` by 1136 PROVE_TAC [lift_redn_def] THEN 1137 `!m. ~(m = 0) ==> (n_posns m x' = {})` by PROVE_TAC [n_posns_nlabel] THEN 1138 `!m. ~(m = 0) ==> (n_posns m y' = {})` by PROVE_TAC [lrcc_new_labels] THEN 1139 Q.EXISTS_TAC `n_posns 0 y'` THEN 1140 PROVE_TAC [n_posns_strip_label, nlabel_n_posns] 1141 ]); 1142 1143val residuals_def = new_specification ( 1144 "residuals_def", ["residuals"], 1145 SIMP_RULE bool_ss [GSYM RIGHT_EXISTS_IMP_THM, 1146 SKOLEM_THM] residuals_exist); 1147 1148val residuals_can_ignore = store_thm( 1149 "residuals_can_ignore", 1150 ``!sigma ps. 1151 okpath (labelled_redn beta) sigma /\ finite sigma ==> 1152 (residuals sigma ps = 1153 residuals sigma (ps INTER redex_posns (first sigma)))``, 1154 REPEAT STRIP_TAC THEN 1155 Q.ABBREV_TAC `M = first sigma` THEN 1156 Q.ABBREV_TAC `N = last sigma` THEN 1157 Q.ABBREV_TAC `r1 = residuals sigma ps` THEN 1158 Q.ABBREV_TAC `r2 = residuals sigma (ps INTER redex_posns M)` THEN 1159 Q.ABBREV_TAC `N1 = nlabel 0 N r1` THEN 1160 Q.ABBREV_TAC `N2 = nlabel 0 N r2` THEN 1161 Q.ABBREV_TAC `M1 = nlabel 0 M ps` THEN 1162 Q.ABBREV_TAC `M2 = nlabel 0 M (ps INTER redex_posns M)` THEN 1163 `(last (lift_path M1 sigma) = N1) /\ (r1 SUBSET redex_posns N) /\ 1164 (last (lift_path M2 sigma) = N2) /\ (r2 SUBSET redex_posns N)` 1165 by METIS_TAC [residuals_def] THEN 1166 `M1 = M2` by PROVE_TAC [nlabel_eq_inter] THEN 1167 `N1 = N2` by PROVE_TAC [] THEN 1168 `r1 INTER (redex_posns N) = r2 INTER (redex_posns N)` 1169 by PROVE_TAC [labelled_term_component_equality, n_posns_nlabel] THEN 1170 PROVE_TAC [SUBSET_INTER_ABSORPTION]); 1171 1172val redex_posns_FINITE = store_thm( 1173 "redex_posns_FINITE", 1174 ``!M. FINITE (redex_posns M)``, 1175 HO_MATCH_MP_TAC simple_induction THEN 1176 SRW_TAC [][redex_posns_thm]); 1177 1178val residuals_FINITE = store_thm( 1179 "residuals_FINITE", 1180 ``!sigma ps. 1181 okpath (labelled_redn beta) sigma /\ finite sigma ==> 1182 FINITE (residuals sigma ps)``, 1183 PROVE_TAC [residuals_def, redex_posns_FINITE, SUBSET_FINITE]); 1184 1185val residuals_EMPTY = store_thm( 1186 "residuals_EMPTY", 1187 ``!p. okpath (labelled_redn beta) p /\ finite p ==> (residuals p {} = {})``, 1188 HO_MATCH_MP_TAC finite_okpath_ind THEN REPEAT STRIP_TAC THENL [ 1189 Q.SPEC_THEN `stopped_at x` (Q.SPEC_THEN `{}` MP_TAC o 1190 REWRITE_RULE [okpath_thm, finite_thm]) 1191 residuals_def THEN 1192 SIMP_TAC (srw_ss())[last_thm, first_thm, lift_path_def, 1193 labelled_term_component_equality, 1194 strip_label_nlabel] THEN 1195 STRIP_TAC THEN 1196 FIRST_X_ASSUM (Q.SPEC_THEN `0` 1197 (ASSUME_TAC o 1198 SIMP_RULE (srw_ss()) [n_posns_nlabel])) THEN 1199 PROVE_TAC [SUBSET_INTER_ABSORPTION], 1200 Q.SPEC_THEN `pcons x r p` MP_TAC residuals_def THEN 1201 ASM_SIMP_TAC (srw_ss())[last_thm, first_thm, lift_path_def, 1202 strip_label_nlabel, finite_thm, okpath_thm] THEN 1203 DISCH_THEN (Q.SPEC_THEN `{}` MP_TAC) THEN 1204 `lift_redn (nlabel 0 x {}) r (first p) = nlabel 0 (first p) {}` by 1205 (SRW_TAC [][labelled_term_component_equality, 1206 strip_label_nlabel] 1207 THENL[ 1208 PROVE_TAC [lift_redn_def, strip_label_nlabel], 1209 Q.ABBREV_TAC `x' = nlabel 0 x {}` THEN 1210 `lrcc (beta0 RUNION beta1) (nlabel 0 x {}) r 1211 (lift_redn x' r (first p))` by 1212 PROVE_TAC [strip_label_nlabel, lift_redn_def] THEN 1213 `!n. n_posns n x' = {}` by 1214 PROVE_TAC [n_posns_nlabel, INTER_EMPTY] THEN 1215 `!n. n_posns n (nlabel 0 (first p) {}) = {}` by 1216 PROVE_TAC [n_posns_nlabel, INTER_EMPTY] THEN 1217 PROVE_TAC [lrcc_new_labels] 1218 ]) THEN 1219 POP_ASSUM SUBST_ALL_TAC THEN 1220 Q.SPEC_THEN `p` MP_TAC residuals_def THEN 1221 ASM_SIMP_TAC bool_ss [] THEN 1222 DISCH_THEN (Q.SPEC_THEN `{}` STRIP_ASSUME_TAC) THEN 1223 SIMP_TAC (srw_ss())[labelled_term_component_equality, 1224 strip_label_nlabel] THEN 1225 STRIP_TAC THEN 1226 `{} INTER redex_posns (last p) = 1227 residuals (pcons x r p) {} INTER redex_posns (last p)` by 1228 PROVE_TAC [n_posns_nlabel] THEN 1229 POP_ASSUM MP_TAC THEN SRW_TAC [][] THEN 1230 PROVE_TAC [SUBSET_INTER_ABSORPTION] 1231 ]); 1232 1233val nlabel_11 = store_thm( 1234 "nlabel_11", 1235 ``!t1 t2 n ps1 ps2. (nlabel n t1 ps1 = nlabel n t2 ps2) ==> 1236 (t1 = t2) /\ 1237 (ps1 INTER redex_posns t1 = ps2 INTER redex_posns t1)``, 1238 REPEAT GEN_TAC THEN STRIP_TAC THEN 1239 `(n_posns n (nlabel n t1 ps1) = n_posns n (nlabel n t2 ps2)) /\ 1240 (strip_label (nlabel n t1 ps1) = strip_label (nlabel n t2 ps2))` by 1241 PROVE_TAC [labelled_term_component_equality] THEN 1242 PROVE_TAC [n_posns_nlabel, strip_label_nlabel]); 1243 1244val residuals_stopped_at = store_thm( 1245 "residuals_stopped_at", 1246 ``!x ps. 1247 residuals (stopped_at x) ps = ps INTER redex_posns x``, 1248 REPEAT GEN_TAC THEN 1249 Q.SPEC_THEN `stopped_at x` MP_TAC residuals_def THEN 1250 SIMP_TAC (srw_ss()) [lift_path_def] THEN 1251 DISCH_THEN (Q.SPEC_THEN `ps` STRIP_ASSUME_TAC) THEN 1252 `ps INTER (redex_posns x) = 1253 residuals (stopped_at x) ps INTER (redex_posns x)` 1254 by PROVE_TAC [nlabel_11] THEN 1255 PROVE_TAC [SUBSET_INTER_ABSORPTION]); 1256 1257val residual1_def = Define` 1258 residual1 x r y ps = n_posns 0 (lift_redn (nlabel 0 x ps) r y) 1259`; 1260 1261val residuals_pcons = store_thm( 1262 "residuals_pcons", 1263 ``!x r p ps. 1264 okpath (labelled_redn beta) p /\ finite p /\ 1265 labelled_redn beta x r (first p) ==> 1266 (residuals (pcons x r p) ps = 1267 residuals p (residual1 x r (first p) ps))``, 1268 REPEAT STRIP_TAC THEN 1269 Q.SPEC_THEN `pcons x r p` MP_TAC residuals_def THEN 1270 ASM_SIMP_TAC (srw_ss()) [lift_path_def, residual1_def] THEN 1271 DISCH_THEN (Q.SPEC_THEN `ps` MP_TAC) THEN 1272 Q.ABBREV_TAC `x' = nlabel 0 x ps` THEN 1273 Q.ABBREV_TAC `y = first p` THEN 1274 Q.ABBREV_TAC `y' = lift_redn x' r y` THEN 1275 `strip_label x' = x` by PROVE_TAC [strip_label_nlabel] THEN 1276 `(strip_label y' = y) /\ lrcc (beta0 RUNION beta1) x' r y'` 1277 by PROVE_TAC [lift_redn_def] THEN 1278 Q.SPEC_THEN `p` MP_TAC residuals_def THEN 1279 ASM_SIMP_TAC (srw_ss()) [] THEN 1280 DISCH_THEN (Q.SPEC_THEN `n_posns 0 y'` MP_TAC) THEN 1281 `!m. ~(m = 0) ==> (n_posns m x' = {})` by PROVE_TAC [n_posns_nlabel] THEN 1282 `!m. ~(m = 0) ==> (n_posns m y' = {})` by PROVE_TAC [lrcc_new_labels] THEN 1283 `nlabel 0 y (n_posns 0 y') = y'` by PROVE_TAC [nlabel_n_posns] THEN 1284 ASM_SIMP_TAC (srw_ss()) [] THEN REPEAT STRIP_TAC THEN 1285 IMP_RES_TAC nlabel_11 THEN 1286 PROVE_TAC [SUBSET_INTER_ABSORPTION]); 1287 1288val residual1_SUBSET = store_thm( 1289 "residual1_SUBSET", 1290 ``!x r y ps. labelled_redn beta x r y ==> 1291 residual1 x r y ps SUBSET redex_posns y``, 1292 SRW_TAC [][residual1_def, redex_posns_redex_occurrence, SUBSET_DEF] THEN 1293 `x = strip_label (nlabel 0 x ps)` by SRW_TAC [][strip_label_nlabel] THEN 1294 `y = strip_label (lift_redn (nlabel 0 x ps) r y)` by 1295 PROVE_TAC [lift_redn_def] THEN 1296 PROVE_TAC [n_posns_strip_label, redexes_all_occur_def]); 1297 1298val labelled_redn_lam = store_thm( 1299 "labelled_redn_lam", 1300 ``!v t r y. 1301 labelled_redn beta (LAM v t) r y = 1302 ?t' r'. labelled_redn beta t r' t' /\ (y = LAM v t') /\ (r = In::r')``, 1303 REPEAT GEN_TAC THEN EQ_TAC THENL [ 1304 SRW_TAC [][beta_def, Once labelled_redn_cases, SimpL ``(==>)``] THEN 1305 FULL_SIMP_TAC (srw_ss()) [LAM_eq_thm, tpm_eqr, pmact_flip_args] THEN 1306 SRW_TAC [][] THEN 1307 FULL_SIMP_TAC (srw_ss()) [labelled_redn_beta_tpm_eqn] THEN 1308 `!a. a IN FV (tpm [(v,v')] y') ==> a IN FV t` 1309 by METIS_TAC [labelled_redn_cc, cc_beta_FV_SUBSET, 1310 SUBSET_DEF] THEN 1311 POP_ASSUM (Q.SPEC_THEN `v'` MP_TAC) THEN SRW_TAC [][], 1312 SRW_TAC [][] THEN SRW_TAC [][labelled_redn_rules] 1313 ]); 1314 1315val labelled_redn_var = store_thm( 1316 "labelled_redn_var", 1317 ``~labelled_redn beta (VAR s) r t``, 1318 SRW_TAC [][Once labelled_redn_cases, beta_def]); 1319val _ = export_rewrites ["labelled_redn_var"] 1320 1321val labelled_redn_vposn_sub = store_thm( 1322 "labelled_redn_vposn_sub", 1323 ``!body v x r y p. 1324 p IN v_posns v body /\ 1325 labelled_redn beta x r y ==> 1326 ?M. labelled_redn beta ([x/v] body) (APPEND p r) M``, 1327 REPEAT GEN_TAC THEN MAP_EVERY Q.ID_SPEC_TAC [`p`, `body`] THEN 1328 HO_MATCH_MP_TAC nc_INDUCTION2 THEN Q.EXISTS_TAC `v INSERT FV x` THEN 1329 SRW_TAC [][SUB_THM, SUB_VAR]THEN REPEAT CONJ_TAC THEN 1330 METIS_TAC [labelled_redn_rules, listTheory.APPEND]); 1331 1332val BIGUNION_IMAGE_SING = prove( 1333 ``!s f. BIGUNION (IMAGE (\x. {f x}) s) = IMAGE f s``, 1334 SRW_TAC [][EXTENSION, EQ_IMP_THM, FORALL_AND_THM] THEN 1335 PROVE_TAC [IN_INSERT, NOT_IN_EMPTY]); 1336 1337val lv_posns_nlabel = store_thm( 1338 "lv_posns_nlabel", 1339 ``!t v ps n. lv_posns v (nlabel n (strip_label t) ps) = lv_posns v t``, 1340 SRW_TAC [][lv_posns_def]); 1341 1342val lv_posns_null_labelling = store_thm( 1343 "lv_posns_null_labelling", 1344 ``!t v ps. lv_posns v (null_labelling (strip_label t)) = lv_posns v t``, 1345 SRW_TAC [][lv_posns_def]); 1346 1347val position_maps_exist = store_thm( 1348 "position_maps_exist", 1349 ``!x r y. 1350 labelled_redn beta x r y ==> 1351 ?f:redpos list -> redpos list set. 1352 !x'. (strip_label x' = x) ==> 1353 !y'. lrcc (beta0 RUNION beta1) x' r y' ==> 1354 (strip_label y' = y) /\ 1355 !n. n_posns n y' = 1356 BIGUNION (IMAGE f (n_posns n x'))``, 1357 HO_MATCH_MP_TAC simple_induction THEN REPEAT CONJ_TAC THENL [ 1358 SRW_TAC [][], 1359 1360 MAP_EVERY Q.X_GEN_TAC [`M`, `N`] THEN STRIP_TAC THEN 1361 SIMP_TAC (srw_ss()) 1362 [Once labelled_redn_cases, beta_def, SimpL ``(==>)``] THEN 1363 SIMP_TAC (srw_ss() ++ DNF_ss) [] THEN 1364 REPEAT CONJ_TAC THENL [ 1365 MAP_EVERY Q.X_GEN_TAC [`bv`, `body`] THEN SRW_TAC [][] THEN 1366 SRW_TAC [][RUNION, beta0_def, beta1_def, DISJ_IMP_THM, 1367 Once lrcc_cases] THEN 1368 SIMP_TAC (srw_ss() ++ DNF_ss) [] THEN 1369 CONV_TAC EXISTS_AND_REORDER_CONV THEN 1370 CONJ_TAC THEN1 1371 (SRW_TAC [][strip_label_subst] THEN 1372 FULL_SIMP_TAC (srw_ss()) [LAM_eq_thm, fresh_tpm_subst, lemma15a]) THEN 1373 SRW_TAC [][Once lrcc_cases, RUNION, beta0_def, beta1_def] THEN 1374 SIMP_TAC (srw_ss() ++ DNF_ss) [n_posns_sub] THEN 1375 1376 Q.EXISTS_TAC `\p. if p = [] then {} 1377 else if (HD p = Lt) /\ (HD (TL p) = In) then 1378 {TL (TL p)} 1379 else IMAGE (\vp. APPEND vp (TL p)) 1380 (v_posns bv body)` THEN 1381 SRW_TAC [][] THEN 1382 REPEAT STRIP_TAC THEN 1383 (`v_posns bv body = lv_posns v t` 1384 by FULL_SIMP_TAC (srw_ss()) [LAM_eq_thm, lv_posns_def] THEN 1385 POP_ASSUM SUBST_ALL_TAC THEN 1386 SRW_TAC [][n_posns_def, GSYM IMAGE_COMPOSE, 1387 combinTheory.o_DEF, BIGUNION_IMAGE_SING] THEN 1388 (SRW_TAC [][EXTENSION, EQ_IMP_THM] THEN 1389 ASM_REWRITE_TAC [] THENL [ 1390 DISJ2_TAC THEN 1391 Q.EXISTS_TAC `IMAGE (\vp. APPEND vp np) (lv_posns v t)` THEN 1392 SRW_TAC [][] THEN Q.EXISTS_TAC `np` THEN PROVE_TAC [], 1393 PROVE_TAC [] 1394 ])), 1395 1396 MAP_EVERY Q.X_GEN_TAC [`M'`, `pos`] THEN STRIP_TAC THEN 1397 RES_TAC THEN 1398 REPEAT (Q.PAT_X_ASSUM `!r y. labelled_redn beta X r y ==> Q X r y` 1399 (K ALL_TAC)) THEN 1400 ONCE_REWRITE_TAC [lrcc_cases] THEN 1401 SIMP_TAC (srw_ss() ++ DNF_ss) [] THEN 1402 CONV_TAC EXISTS_AND_REORDER_CONV THEN 1403 REPEAT STRIP_TAC THENL [ 1404 PROVE_TAC [], 1405 REPEAT VAR_EQ_TAC THEN 1406 FULL_SIMP_TAC (srw_ss() ++ DNF_ss) 1407 [strip_label_eq_lam, labelled_redn_lam, 1408 lrcc_beta_lam] THEN 1409 SRW_TAC [][] THEN FULL_SIMP_TAC (srw_ss()) [] THEN METIS_TAC [], 1410 ALL_TAC 1411 ] THEN 1412 Q.EXISTS_TAC `\p. if p = [] then {[]} 1413 else if HD p = Lt then IMAGE (CONS Lt) (f (TL p)) 1414 else {p}` THEN 1415 SRW_TAC [][n_posns_def, GSYM IMAGE_COMPOSE, 1416 BIGUNION_IMAGE_SING, combinTheory.o_DEF] 1417 THENL [ 1418 FIRST_X_ASSUM (Q.SPEC_THEN `x` (ASSUME_TAC o REWRITE_RULE [])) THEN 1419 RES_TAC THEN 1420 REWRITE_TAC [EXTENSION] THEN 1421 SRW_TAC [ETA_ss][GSYM LEFT_EXISTS_AND_THM, 1422 GSYM RIGHT_EXISTS_AND_THM, 1423 EQ_IMP_THM] THEN PROVE_TAC [], 1424 ALL_TAC, 1425 ALL_TAC 1426 ] THEN 1427 FIRST_X_ASSUM 1428 (Q.SPEC_THEN `LAM v x` (ASSUME_TAC o SIMP_RULE (srw_ss()) [])) THEN 1429 `lrcc (beta0 RUNION beta1) (LAM v x) (In::r) (LAM v y)` 1430 by PROVE_TAC [lrcc_rules] THEN RES_TAC THEN 1431 POP_ASSUM MP_TAC THEN 1432 SIMP_TAC (srw_ss()) [n_posns_def] THEN 1433 REWRITE_TAC [EXTENSION] THEN 1434 SRW_TAC [ETA_ss] 1435 [GSYM LEFT_EXISTS_AND_THM, GSYM RIGHT_EXISTS_AND_THM, 1436 EQ_IMP_THM, FORALL_AND_THM, GSYM LEFT_FORALL_IMP_THM] THEN 1437 PROVE_TAC [], 1438 1439 MAP_EVERY Q.X_GEN_TAC [`N'`,`pos`] THEN STRIP_TAC THEN RES_TAC THEN 1440 REPEAT (Q.PAT_X_ASSUM `!r y. labelled_redn beta X r y ==> Q X r y` 1441 (K ALL_TAC)) THEN 1442 ONCE_REWRITE_TAC [lrcc_cases] THEN SRW_TAC [][] THEN 1443 SRW_TAC [DNF_ss][] THEN CONV_TAC EXISTS_AND_REORDER_CONV THEN 1444 REPEAT STRIP_TAC THENL [ 1445 PROVE_TAC [], 1446 PROVE_TAC [], 1447 ALL_TAC 1448 ] THEN 1449 Q.EXISTS_TAC `\p. if p = [] then {[]} 1450 else if HD p = Rt then IMAGE (CONS Rt) (f (TL p)) 1451 else {p}` THEN 1452 SRW_TAC [][n_posns_def, GSYM IMAGE_COMPOSE, 1453 BIGUNION_IMAGE_SING, combinTheory.o_DEF] THEN 1454 FIRST_X_ASSUM (Q.SPEC_THEN `x` (ASSUME_TAC o REWRITE_RULE [])) THEN 1455 RES_TAC THEN 1456 REWRITE_TAC [EXTENSION] THEN 1457 SRW_TAC [ETA_ss][GSYM LEFT_EXISTS_AND_THM, 1458 GSYM RIGHT_EXISTS_AND_THM, 1459 EQ_IMP_THM] THEN PROVE_TAC [] 1460 ], 1461 1462 MAP_EVERY Q.X_GEN_TAC [`bv`, `body`] THEN 1463 SRW_TAC [][labelled_redn_lam] THEN RES_TAC THEN 1464 Q.PAT_X_ASSUM `!r y. labelled_redn beta X r y ==> Q X r y` 1465 (K ALL_TAC) THEN 1466 Q.EXISTS_TAC `\p. IMAGE (CONS In) (f (TL p))` THEN 1467 SIMP_TAC (srw_ss())[strip_label_eq_lam, GSYM LEFT_FORALL_IMP_THM, 1468 lrcc_beta_lam, n_posns_def] THEN 1469 REPEAT STRIP_TAC THENL [ 1470 PROVE_TAC [], 1471 RES_TAC THEN 1472 REWRITE_TAC [EXTENSION] THEN 1473 SRW_TAC [][GSYM LEFT_EXISTS_AND_THM, GSYM RIGHT_EXISTS_AND_THM, 1474 EQ_IMP_THM] THEN PROVE_TAC [] 1475 ] 1476 ]); 1477 1478val residual1_pointwise_union = store_thm( 1479 "residual1_pointwise_union", 1480 ``!x r y. 1481 labelled_redn beta x r y ==> 1482 !ps1 ps2. 1483 residual1 x r y (ps1 UNION ps2) = 1484 residual1 x r y ps1 UNION residual1 x r y ps2``, 1485 SRW_TAC [][] THEN 1486 Q.ABBREV_TAC `x' = nlabel 0 x (ps1 UNION ps2)` THEN 1487 `strip_label x' = x` by PROVE_TAC [strip_label_nlabel] THEN 1488 Q.ABBREV_TAC `x1' = nlabel 0 x ps1` THEN 1489 Q.ABBREV_TAC `x2' = nlabel 0 x ps2` THEN 1490 `(strip_label x1' = x) /\ (strip_label x2' = x)` 1491 by PROVE_TAC [strip_label_nlabel] THEN 1492 Q.ABBREV_TAC `y' = lift_redn x' r y` THEN 1493 Q.ABBREV_TAC `y1' = lift_redn x1' r y` THEN 1494 Q.ABBREV_TAC `y2' = lift_redn x2' r y` THEN 1495 `lrcc (beta0 RUNION beta1) x' r y' /\ (strip_label y' = y) /\ 1496 lrcc (beta0 RUNION beta1) x1' r y1' /\ (strip_label y1' = y) /\ 1497 lrcc (beta0 RUNION beta1) x2' r y2' /\ (strip_label y2' = y)` 1498 by PROVE_TAC [lift_redn_def] THEN 1499 ASM_SIMP_TAC (srw_ss())[residual1_def] THEN 1500 `?f. !x' y'. (strip_label x' = x) /\ 1501 lrcc (beta0 RUNION beta1) x' r y' ==> 1502 (n_posns 0 y' = BIGUNION (IMAGE f (n_posns 0 x')))` 1503 by PROVE_TAC [position_maps_exist] THEN 1504 `(n_posns 0 y' = BIGUNION (IMAGE f (n_posns 0 x'))) /\ 1505 (n_posns 0 y1' = BIGUNION (IMAGE f (n_posns 0 x1'))) /\ 1506 (n_posns 0 y2' = BIGUNION (IMAGE f (n_posns 0 x2')))` by PROVE_TAC [] THEN 1507 ASM_REWRITE_TAC [] THEN 1508 MAP_EVERY Q.UNABBREV_TAC [`x'`, `x1'`, `x2'`] THEN 1509 SIMP_TAC (srw_ss()) [n_posns_nlabel] THEN 1510 REPEAT (POP_ASSUM (K ALL_TAC)) THEN 1511 REWRITE_TAC [EXTENSION] THEN 1512 SRW_TAC [][EQ_IMP_THM, GSYM LEFT_EXISTS_AND_THM, 1513 GSYM RIGHT_EXISTS_AND_THM] THEN 1514 PROVE_TAC []); 1515 1516val residuals_pointwise_union = store_thm( 1517 "residuals_pointwise_union", 1518 ``!sigma. 1519 okpath (labelled_redn beta) sigma /\ finite sigma ==> 1520 !ps1 ps2. residuals sigma (ps1 UNION ps2) = 1521 residuals sigma ps1 UNION residuals sigma ps2``, 1522 HO_MATCH_MP_TAC finite_okpath_ind THEN REPEAT STRIP_TAC THENL [ 1523 SRW_TAC [][residuals_stopped_at, EXTENSION] THEN 1524 PROVE_TAC [], 1525 SRW_TAC [][residuals_pcons, residuals_pcons, residual1_pointwise_union] 1526 ]); 1527 1528val lemma11_2_5 = store_thm( 1529 "lemma11_2_5", 1530 ``!sigma. 1531 okpath (labelled_redn beta) sigma /\ finite sigma ==> 1532 !r ps. residuals sigma (r INSERT ps) = 1533 residuals sigma {r} UNION residuals sigma ps``, 1534 REPEAT STRIP_TAC THEN 1535 CONV_TAC 1536 (LAND_CONV (ONCE_REWRITE_CONV [INSERT_SING_UNION])) THEN 1537 SRW_TAC [][residuals_pointwise_union]); 1538 1539val lemma11_2_6 = store_thm( 1540 "lemma11_2_6", 1541 ``!sigma tau ps. 1542 finite sigma /\ okpath (labelled_redn beta) sigma /\ 1543 finite tau /\ okpath (labelled_redn beta) tau /\ 1544 (last sigma = first tau) ==> 1545 (residuals (plink sigma tau) ps = residuals tau (residuals sigma ps))``, 1546 Q_TAC SUFF_TAC 1547 `!sigma. okpath (labelled_redn beta) sigma /\ finite sigma ==> 1548 !tau ps. finite tau /\ okpath (labelled_redn beta) tau /\ 1549 (last sigma = first tau) ==> 1550 (residuals (plink sigma tau) ps = 1551 residuals tau (residuals sigma ps))` THEN1 1552 PROVE_TAC [] THEN 1553 HO_MATCH_MP_TAC finite_okpath_ind THEN 1554 SRW_TAC [][residuals_stopped_at, residuals_pcons, first_plink, 1555 okpath_plink] THEN 1556 PROVE_TAC [residuals_can_ignore]); 1557 1558(* skipping lemma11_2_8 because this requires me to invent a multi-label 1559 constant; maybe one that takes a finite map from positions to labels and 1560 labels a term accordingly. *) 1561 1562(* definition 11.2.11 *) 1563val development_f_def = Define` 1564 development_f X = 1565 { (stopped_at x, ps) | T } UNION 1566 { (pcons x r p, ps) | (p, residual1 x r (first p) ps) IN X /\ r IN ps /\ 1567 labelled_redn beta x r (first p) } 1568`; 1569 1570val development_f_monotone = store_thm( 1571 "development_f_monotone", 1572 ``monotone development_f``, 1573 SRW_TAC [][fixedPointTheory.monotone_def, SUBSET_DEF, 1574 development_f_def]); 1575 1576val development0_def = Define` 1577 development0 sigma ps <=> (sigma, ps) IN gfp development_f 1578`; 1579 1580val development0_coinduction = store_thm( 1581 "development0_coinduction", 1582 ``!P. 1583 (!sigma ps. P sigma ps ==> 1584 (?x. (sigma = stopped_at x)) \/ 1585 (?x r p. (sigma = pcons x r p) /\ r IN ps /\ 1586 labelled_redn beta x r (first p) /\ 1587 P p (residual1 x r (first p) ps))) ==> 1588 !sigma ps. P sigma ps ==> development0 sigma ps``, 1589 GEN_TAC THEN STRIP_TAC THEN 1590 Q.SPEC_THEN `{ p | P (FST p) (SND p) }` 1591 (ASSUME_TAC o SIMP_RULE (srw_ss()) [SUBSET_DEF, 1592 pairTheory.FORALL_PROD]) 1593 (MATCH_MP fixedPointTheory.gfp_coinduction 1594 development_f_monotone) THEN 1595 SIMP_TAC (srw_ss()) [development0_def] THEN 1596 FIRST_X_ASSUM MATCH_MP_TAC THEN 1597 SIMP_TAC (srw_ss()) [development_f_def] THEN 1598 REPEAT STRIP_TAC THEN RES_TAC THEN SRW_TAC [][]); 1599 1600val development0_cases = save_thm( 1601 "development0_cases", 1602 (GEN_ALL o CONV_RULE (RENAME_VARS_CONV ["sigma", "ps"]) o 1603 SIMP_RULE (srw_ss()) [pairTheory.FORALL_PROD, 1604 development_f_def, GSYM development0_def] o 1605 CONV_RULE (REWR_CONV EXTENSION) o SYM o 1606 CONJUNCT1) 1607 (MATCH_MP fixedPointTheory.gfp_greatest_fixedpoint 1608 (SPEC_ALL development_f_monotone))); 1609 1610val term_posset_development_def = Define` 1611 term_posset_development M posset sigma <=> 1612 (first sigma = M) /\ posset SUBSET M /\ development0 sigma posset 1613`; 1614 1615val _ = overload_on ("development", ``term_posset_development``); 1616 1617Theorem development_thm: 1618 (stopped_at x IN development M ps <=> (M = x) /\ ps SUBSET M) /\ 1619 (pcons x r p IN development M ps <=> 1620 (M = x) /\ ps SUBSET M /\ 1621 labelled_redn beta x r (first p) /\ r IN ps /\ 1622 p IN development (first p) (residual1 x r (first p) ps)) 1623Proof 1624 REPEAT STRIP_TAC THEN 1625 `!sigma M ps. sigma IN development M ps <=> development M ps sigma` 1626 by SRW_TAC [][SPECIFICATION] THEN 1627 SRW_TAC [][term_posset_development_def] THEN 1628 CONV_TAC (LAND_CONV (ONCE_REWRITE_CONV [development0_cases])) THEN 1629 SRW_TAC [][EQ_IMP_THM, redexes_all_occur_def, IN_term_IN_redex_posns] THEN 1630 PROVE_TAC [residual1_SUBSET, SUBSET_DEF] 1631QED 1632 1633val development_cases = store_thm( 1634 "development_cases", 1635 ``!M ps sigma. 1636 sigma IN development M ps <=> 1637 (sigma = stopped_at M) /\ ps SUBSET M \/ 1638 (?r p. (sigma = pcons M r p) /\ ps SUBSET M /\ r IN ps /\ 1639 labelled_redn beta M r (first p) /\ 1640 p IN development (first p) (residual1 M r (first p) ps))``, 1641 REPEAT GEN_TAC THEN 1642 Q.ISPEC_THEN `sigma` STRUCT_CASES_TAC path_cases THEN 1643 SRW_TAC [][development_thm, EQ_IMP_THM]); 1644 1645val developments_ok = store_thm( 1646 "developments_ok", 1647 ``!M sigma ps. sigma IN development M ps ==> 1648 okpath (labelled_redn beta) sigma``, 1649 Q_TAC SUFF_TAC 1650 `!sigma. (?M ps. sigma IN development M ps) ==> 1651 okpath (labelled_redn beta) sigma` THEN1 PROVE_TAC [] THEN 1652 HO_MATCH_MP_TAC okpath_co_ind THEN 1653 METIS_TAC [development_cases, pcons_11, stopped_at_not_pcons]); 1654 1655val complete_development_def = Define` 1656 complete_development M ps sigma <=> 1657 finite sigma /\ sigma IN development M ps /\ (residuals sigma ps = {}) 1658`; 1659 1660val complete_development_thm = store_thm( 1661 "complete_development_thm", 1662 ``sigma IN complete_development M ps <=> 1663 finite sigma /\ sigma IN development M ps /\ (residuals sigma ps = {})``, 1664 SRW_TAC [][SPECIFICATION, complete_development_def]); 1665 1666val term_development_def = Define` 1667 term_development M sigma = development M (redex_posns M) sigma 1668`; 1669 1670val _ = overload_on ("development", ``term_development``); 1671 1672val term_development_thm = store_thm( 1673 "term_development_thm", 1674 ``sigma IN development M <=> sigma IN development M (redex_posns M)``, 1675 SRW_TAC [][SPECIFICATION, term_development_def]); 1676 1677val first_lift_path = store_thm( 1678 "first_lift_path", 1679 ``!p M. first (lift_path M p) = M``, 1680 SIMP_TAC (srw_ss()) [Once FORALL_path, lift_path_def]); 1681 1682val lrcc_RUNION = store_thm( 1683 "lrcc_RUNION", 1684 ``!R M r N. lrcc R M r N ==> lrcc (R RUNION R') M r N``, 1685 GEN_TAC THEN HO_MATCH_MP_TAC lrcc_ind THEN 1686 PROVE_TAC [lrcc_rules, relationTheory.RUNION]); 1687 1688val pick_a_beta = store_thm( 1689 "pick_a_beta", 1690 ``!M r N. lrcc (beta0 RUNION beta1) M r N <=> 1691 (?n. r IN n_posns n M) /\ lrcc beta0 M r N \/ 1692 (!n. ~(r IN n_posns n M)) /\ lrcc beta1 M r N``, 1693 SIMP_TAC (srw_ss()) [EQ_IMP_THM, FORALL_AND_THM] THEN CONJ_TAC THENL [ 1694 HO_MATCH_MP_TAC lrcc_ind THEN 1695 SRW_TAC [][n_posns_def, beta0_def, relationTheory.RUNION, beta1_def] THEN 1696 SRW_TAC [COND_elim_ss][n_posns_def] THEN 1697 PROVE_TAC [lrcc_rules, beta0_def, beta1_def], 1698 PROVE_TAC [lrcc_RUNION, RUNION_COMM] 1699 ]); 1700 1701val lterm_INJECTIVITY_LEMMA1 = store_thm( 1702 "lterm_INJECTIVITY_LEMMA1", 1703 ``!v1 v2 t1 t2. (LAM v1 t1 = LAM v2 t2) ==> (t2 = [VAR v2/v1] t1)``, 1704 SRW_TAC [][lLAM_eq_thm] THEN SRW_TAC [][fresh_ltpm_subst, l15a]); 1705val lterm_INJECTIVITY_LEMMA1i = store_thm( 1706 "lterm_INJECTIVITY_LEMMA1i", 1707 ``!n1 n2 v1 v2 t1 t2 u1 u2. 1708 (LAMi n1 v1 t1 u1 = LAMi n2 v2 t2 u2) ==> 1709 (n1 = n2) /\ (u1 = u2) /\ (t2 = [VAR v2/v1] t1)``, 1710 SRW_TAC [][lLAMi_eq_thm] THEN SRW_TAC [][fresh_ltpm_subst, l15a]); 1711 1712val lrcc_lpermutative = store_thm( 1713 "lrcc_lpermutative", 1714 ``lpermutative R ==> 1715 !M p N. lrcc R M p N ==> !pi. lrcc R (ltpm pi M) p (ltpm pi N)``, 1716 STRIP_TAC THEN HO_MATCH_MP_TAC lrcc_ind THEN SRW_TAC [][] THEN 1717 METIS_TAC [lrcc_rules, lpermutative_def]); 1718 1719val beta0_lpermutative = store_thm( 1720 "beta0_lpermutative", 1721 ``lpermutative beta0``, 1722 SRW_TAC [][lpermutative_def, beta0_def] THEN 1723 SRW_TAC [][ltpm_subst] THEN METIS_TAC []); 1724 1725val beta1_lpermutative = store_thm( 1726 "beta1_lpermutative", 1727 ``lpermutative beta1``, 1728 SRW_TAC [][lpermutative_def, beta1_def] THEN 1729 SRW_TAC [][ltpm_subst] THEN METIS_TAC []); 1730 1731val lrcc_beta01_exclusive = store_thm( 1732 "lrcc_beta01_exclusive", 1733 ``!M r N. lrcc beta0 M r N ==> ~lrcc beta1 M r N``, 1734 HO_MATCH_MP_TAC lrcc_ind THEN REPEAT CONJ_TAC THEN 1735 SIMP_TAC (srw_ss()) [DECIDE ``(~p ==> ~q) <=> (q ==> p)``] THEN 1736 SIMP_TAC (srw_ss()) [Once lrcc_cases, SimpL ``(==>)``] THEN1 1737 SIMP_TAC (srw_ss() ++ DNF_ss) [beta0_def, beta1_def, Once lrcc_cases] THEN 1738 SIMP_TAC (srw_ss() ++ DNF_ss) [lLAMi_eq_thm, lLAM_eq_thm, 1739 lrcc_lpermutative, beta1_lpermutative]); 1740 1741val lrcc_det = store_thm( 1742 "lrcc_det", 1743 ``!M r N. lrcc (beta0 RUNION beta1) M r N ==> 1744 !N'. lrcc (beta0 RUNION beta1) M r N' = (N' = N)``, 1745 REPEAT STRIP_TAC THEN SRW_TAC [][EQ_IMP_THM] THEN 1746 Q.ABBREV_TAC `M0 = strip_label M` THEN 1747 Q.ABBREV_TAC `N0 = strip_label N` THEN 1748 `labelled_redn beta M0 r N0` by PROVE_TAC [lrcc_labelled_redn] THEN 1749 `?f. !y. lrcc (beta0 RUNION beta1) M r y ==> 1750 (strip_label y = N0) /\ 1751 !n. n_posns n y = BIGUNION (IMAGE f (n_posns n M))` by 1752 PROVE_TAC [position_maps_exist] THEN 1753 REWRITE_TAC [labelled_term_component_equality] THEN PROVE_TAC []); 1754 1755val labelled_redn_det = store_thm( 1756 "labelled_redn_det", 1757 ``!M r N. labelled_redn beta M r N ==> 1758 !L. labelled_redn beta M r L = (L = N)``, 1759 REPEAT STRIP_TAC THEN SRW_TAC [][EQ_IMP_THM] THEN 1760 Q.ABBREV_TAC `M' = null_labelling M` THEN 1761 `M = strip_label M'` by SRW_TAC [][strip_null_labelling, Abbr`M'`] THEN 1762 Q.ABBREV_TAC `N' = lift_redn M' r N` THEN 1763 Q.ABBREV_TAC `L' = lift_redn M' r L` THEN 1764 `lrcc (beta0 RUNION beta1) M' r N' /\ (strip_label N' = N) /\ 1765 lrcc (beta0 RUNION beta1) M' r L' /\ (strip_label L' = L)` by 1766 PROVE_TAC [lift_redn_def] THEN 1767 PROVE_TAC [lrcc_det]); 1768 1769val lemma11_2_12 = store_thm( 1770 "lemma11_2_12", 1771 ``!M sigma ps. 1772 sigma IN development M ps <=> 1773 (M = first sigma) /\ ps SUBSET M /\ 1774 okpath (labelled_redn beta) sigma /\ 1775 okpath (lrcc beta0) (lift_path (nlabel 0 (first sigma) ps) sigma)``, 1776 Q_TAC SUFF_TAC 1777 `(!sigma' : (lterm, redpos list) path. 1778 (?x sigma ps. 1779 sigma IN development x ps /\ 1780 (sigma' = lift_path (nlabel 0 (first sigma) ps) sigma)) ==> 1781 okpath (lrcc beta0) sigma') /\ 1782 (!(sigma : (term, redpos list) path) ps. 1783 okpath (labelled_redn beta) sigma /\ 1784 okpath (lrcc beta0) (lift_path (nlabel 0 (first sigma) ps) sigma) ==> 1785 development0 sigma ps)` THEN1 1786 PROVE_TAC [developments_ok, term_posset_development_def, 1787 SPECIFICATION] THEN 1788 CONJ_TAC THENL [ 1789 HO_MATCH_MP_TAC okpath_co_ind THEN 1790 MAP_EVERY Q.X_GEN_TAC [`x`, `r`, `sigma'`] THEN 1791 CONV_TAC (LAND_CONV (RENAME_VARS_CONV ["M", "sigma", "ps"])) THEN 1792 SIMP_TAC (srw_ss()) [Once development_cases, SimpL ``(==>)``] THEN 1793 SIMP_TAC (srw_ss() ++ DNF_ss) [lift_path_def] THEN SRW_TAC [][] THENL [ 1794 SRW_TAC [][first_lift_path] THEN 1795 Q.ABBREV_TAC `M' = nlabel 0 M ps` THEN 1796 Q.ABBREV_TAC `y = first p` THEN 1797 Q.ABBREV_TAC `y' = lift_redn M' r y` THEN 1798 `strip_label M' = M` by PROVE_TAC [strip_label_nlabel] THEN 1799 `lrcc (beta0 RUNION beta1) M' r y'` by PROVE_TAC [lift_redn_def] THEN 1800 `r IN redex_posns M` 1801 by (ASM_SIMP_TAC (srw_ss())[redex_posns_redex_occurrence, 1802 is_redex_occurrence_def] THEN 1803 PROVE_TAC []) THEN 1804 `r IN n_posns 0 M'` 1805 by PROVE_TAC [n_posns_nlabel, IN_INTER] THEN 1806 PROVE_TAC [pick_a_beta], 1807 Q.ABBREV_TAC `M' = nlabel 0 M ps` THEN 1808 Q.ABBREV_TAC `y = first p` THEN 1809 Q.ABBREV_TAC `y' = lift_redn M' r y` THEN 1810 Q.EXISTS_TAC `y` THEN Q.EXISTS_TAC `p` THEN 1811 Q.EXISTS_TAC `residual1 M r y ps` THEN 1812 ASM_SIMP_TAC (srw_ss()) [residual1_def] THEN 1813 `strip_label M' = M` by PROVE_TAC [strip_label_nlabel] THEN 1814 `(y = strip_label y') /\ lrcc (beta0 RUNION beta1) M' r y'` 1815 by PROVE_TAC [lift_redn_def] THEN 1816 `!n. ~(n = 0) ==> (n_posns n M' = {})` by PROVE_TAC [n_posns_nlabel] THEN 1817 `!n. ~(n = 0) ==> (n_posns n y' = {})` 1818 by PROVE_TAC [lrcc_new_labels] THEN 1819 ASM_SIMP_TAC (srw_ss()) [nlabel_n_posns] 1820 ], 1821 HO_MATCH_MP_TAC development0_coinduction THEN REPEAT GEN_TAC THEN 1822 Q.ISPEC_THEN `sigma` STRUCT_CASES_TAC path_cases THEN 1823 SRW_TAC [][lift_path_def, first_lift_path] THEN 1824 Q.ABBREV_TAC `x' = nlabel 0 x ps` THEN 1825 Q.ABBREV_TAC `y = first q` THEN 1826 Q.ABBREV_TAC `y' = lift_redn x' r y` THENL [ 1827 `lrcc (beta0 RUNION beta1) x' r y'` by PROVE_TAC [lrcc_RUNION] THEN 1828 `?n. r IN n_posns n x'` by PROVE_TAC [lrcc_beta01_exclusive, 1829 pick_a_beta] THEN 1830 `n = 0` by PROVE_TAC [n_posns_nlabel, NOT_IN_EMPTY] THEN 1831 PROVE_TAC [IN_INTER, n_posns_nlabel], 1832 ASM_SIMP_TAC (srw_ss()) [residual1_def] THEN 1833 Q_TAC SUFF_TAC `nlabel 0 y (n_posns 0 y') = y'` THEN1 PROVE_TAC [] THEN 1834 `!n. ~(n = 0) ==> (n_posns n x' = {})` by PROVE_TAC [n_posns_nlabel] THEN 1835 `lrcc (beta0 RUNION beta1) x' r y'` by PROVE_TAC [lrcc_RUNION] THEN 1836 `!n. ~(n = 0) ==> (n_posns n y' = {})` 1837 by PROVE_TAC [lrcc_new_labels] THEN 1838 `strip_label x' = x` by PROVE_TAC [strip_label_nlabel] THEN 1839 `y = strip_label y'` by PROVE_TAC [lift_redn_def] THEN 1840 PROVE_TAC [nlabel_n_posns] 1841 ] 1842 ]); 1843 1844val lvar_posns_def = Define` 1845 lvar_posns t = var_posns (strip_label t) 1846`; 1847 1848val (update_weighing_def, update_weighing_swap) = 1849 define_recursive_term_function` 1850 (update_weighing (t @@ u:term) = 1851 \rp w p. 1852 case rp of 1853 [] => (let vps = IMAGE TL (bv_posns t) 1854 in 1855 if ?vp l. vp IN vps /\ (APPEND vp l = p) then 1856 w (Rt :: @l. ?vp. vp IN vps /\ (APPEND vp l = p)) 1857 else w (Lt :: In :: p)) 1858 | Lt::rp0 => if HD p = Lt then 1859 update_weighing t rp0 (\p. w(Lt::p)) (TL p) 1860 else w p 1861 | Rt::rp0 => if HD p = Rt then 1862 update_weighing u rp0 (\p. w(Rt::p)) (TL p) 1863 else w p) /\ 1864 (update_weighing (LAM v t) = 1865 \rp w p. update_weighing t (TL rp) (\p. w (In::p)) (TL p)) 1866`; 1867 1868val update_weighing_thm = store_thm( 1869 "update_weighing_thm", 1870 ``(update_weighing (t @@ u) [] w = 1871 let vps = IMAGE TL (bv_posns t) 1872 in 1873 \p. if ?vp l. vp IN vps /\ (APPEND vp l = p) then 1874 w (Rt :: @l. ?vp. vp IN vps /\ (APPEND vp l = p)) 1875 else 1876 w (Lt::In::p)) /\ 1877 (update_weighing (LAM v t) (In::pos0) w = 1878 let w0 = update_weighing t pos0 (\p. w (In::p)) 1879 in 1880 \p. w0 (TL p)) /\ 1881 (update_weighing (t @@ u) (Lt::pos0) w = 1882 let w0 = update_weighing t pos0 (\p. w (Lt::p)) 1883 in 1884 \p. if HD p = Lt then w0 (TL p) else w p) /\ 1885 (update_weighing (t @@ u) (Rt::pos0) w = 1886 let w0 = update_weighing u pos0 (\p. w (Rt::p)) 1887 in 1888 \p. if HD p = Rt then w0 (TL p) else w p)``, 1889 SRW_TAC [][update_weighing_def]); 1890 1891val update_weighing_vsubst = store_thm( 1892 "update_weighing_vsubst", 1893 ``!t p u v w. p IN redex_posns t ==> 1894 (update_weighing ([VAR v/u]t) p w = update_weighing t p w)``, 1895 REPEAT GEN_TAC THEN MAP_EVERY Q.ID_SPEC_TAC [`w`, `p`,`t`] THEN 1896 HO_MATCH_MP_TAC nc_INDUCTION2 THEN Q.EXISTS_TAC `{u;v}` THEN 1897 SRW_TAC [][redex_posns_thm, SUB_THM] THEN 1898 SRW_TAC [][update_weighing_thm]); 1899 1900val beta0_redex_posn = store_thm( 1901 "beta0_redex_posn", 1902 ``!x r y. lrcc beta0 x r y ==> r IN redex_posns (strip_label x)``, 1903 HO_MATCH_MP_TAC lrcc_ind THEN 1904 SIMP_TAC (srw_ss() ++ DNF_ss) 1905 [redex_posns_thm, strip_label_thm, beta0_def]); 1906 1907val nonzero_def = Define` 1908 nonzero (t:lterm) w = !p. p IN lvar_posns t ==> 0 < w p 1909`; 1910 1911val term_weight_def = Define` 1912 term_weight (t:term) w = SUM_IMAGE w (var_posns t) 1913`; 1914 1915val lterm_weight_def = Define` 1916 lterm_weight (t: lterm) w = SUM_IMAGE w (lvar_posns t) 1917`; 1918 1919val delete_non_element = 1920 #1 (EQ_IMP_RULE (SPEC_ALL DELETE_NON_ELEMENT)) 1921 1922val SUM_IMAGE_IMAGE = store_thm( 1923 "SUM_IMAGE_IMAGE", 1924 ``!g. (!x y. (g x = g y) = (x = y)) ==> 1925 !s. FINITE s ==> 1926 !f. SUM_IMAGE f (IMAGE g s) = SUM_IMAGE (f o g) s``, 1927 GEN_TAC THEN STRIP_TAC THEN 1928 HO_MATCH_MP_TAC FINITE_INDUCT THEN CONJ_TAC THEN 1929 SRW_TAC [][SUM_IMAGE_THM, delete_non_element]); 1930 1931val inter_images = prove( 1932 ``!s t f g. (!x y. ~(f x = g y)) ==> (IMAGE f s INTER IMAGE g t = {})``, 1933 SRW_TAC [][EXTENSION] THEN PROVE_TAC []); 1934 1935val lterm_weight_thm = store_thm( 1936 "lterm_weight_thm", 1937 ``(lterm_weight (VAR s) w = w []) /\ 1938 (lterm_weight (t1 @@ t2) w = 1939 lterm_weight t1 (\p. w (Lt::p)) + 1940 lterm_weight t2 (\p. w (Rt::p))) /\ 1941 (lterm_weight (LAM v t) w = 1942 lterm_weight t (\p. w (In::p))) /\ 1943 (lterm_weight (LAMi n v t1 t2) w = 1944 lterm_weight t1 (\p. w (Lt::In::p)) + 1945 lterm_weight t2 (\p. w (Rt :: p)))``, 1946 SIMP_TAC (srw_ss()) [lterm_weight_def, lvar_posns_def, var_posns_thm, 1947 strip_label_thm, SUM_IMAGE_SING, 1948 SUM_IMAGE_THM, 1949 SUM_IMAGE_IMAGE, inter_images, 1950 GSYM IMAGE_COMPOSE, 1951 combinTheory.o_DEF, SUM_IMAGE_UNION 1952 ]); 1953 1954val term_weight_thm = store_thm( 1955 "term_weight_thm", 1956 ``(!s. term_weight (VAR s) w = w []) /\ 1957 (!t u. term_weight (t @@ u) w = term_weight t (\p. w (Lt::p)) + 1958 term_weight u (\p. w (Rt::p))) /\ 1959 (!v t. term_weight (LAM v t) w = term_weight t (\p. w (In::p)))``, 1960 SIMP_TAC (srw_ss()) [term_weight_def, var_posns_def, 1961 SUM_IMAGE_SING, 1962 SUM_IMAGE_THM, 1963 SUM_IMAGE_IMAGE, inter_images, 1964 GSYM IMAGE_COMPOSE, 1965 combinTheory.o_DEF, SUM_IMAGE_UNION 1966 ]); 1967 1968val term_weight_vsubst = Store_Thm( 1969 "term_weight_vsubst", 1970 ``!t w u v. term_weight ([VAR v/u] t) w = term_weight t w``, 1971 SIMP_TAC (srw_ss()) [term_weight_def]); 1972 1973val term_weight_swap = Store_Thm( 1974 "term_weight_swap", 1975 ``term_weight (tpm p t) w = term_weight t w``, 1976 SIMP_TAC (srw_ss()) [term_weight_def]); 1977 1978val lterm_term_weight = store_thm( 1979 "lterm_term_weight", 1980 ``!t w. lterm_weight t w = term_weight (strip_label t) w``, 1981 HO_MATCH_MP_TAC simple_lterm_induction THEN 1982 SRW_TAC [][lterm_weight_thm, term_weight_thm, strip_label_thm]); 1983 1984val w_at_exists = 1985 (CONV_RULE (QUANT_CONV (RAND_CONV (ONCE_REWRITE_CONV [EQ_SYM_EQ]))) o 1986 SIMP_RULE (srw_ss()) [term_weight_thm] o 1987 Q.INST [`lm` |-> `\rt v t p w. if p = [] then term_weight (LAM v t) w 1988 else rt (TL p) (\p. w (In::p))`, 1989 `ap` |-> `\rt ru t u p w. 1990 case p of 1991 (Lt::p0) => rt p0 (\p. w (Lt::p)) 1992 | (Rt::p0) => ru p0 (\p. w (Rt::p)) 1993 | _ => term_weight (t @@ u) w`, 1994 `vr` |-> `\s p w. term_weight (VAR s) w`, 1995 `apm` |-> `discrete_pmact`] o SPEC_ALL o 1996 INST_TYPE [alpha |-> ``:redpos list -> (redpos list -> num) -> num``]) 1997 tm_recursion_nosideset 1998 1999val weight_at_def = new_specification( 2000 "weight_at_def", ["weight_at"], 2001 prove( 2002 ``?weight_at. 2003 (!t w. 2004 weight_at [] w t = term_weight t w) /\ 2005 (!p w v t. 2006 weight_at (In::p) w (LAM v t) = weight_at p (\p. w (In::p)) t) /\ 2007 (!p w t u. 2008 weight_at (Lt::p) w (t @@ u) = weight_at p (\p. w (Lt::p)) t) /\ 2009 (!p w t u. 2010 weight_at (Rt::p) w (t @@ u) = weight_at p (\p. w (Rt::p)) u) /\ 2011 (!p w t pi. weight_at p w (tpm pi t) = weight_at p w t)``, 2012 STRIP_ASSUME_TAC w_at_exists THEN 2013 Q.EXISTS_TAC `\p w t. f t p w` THEN SRW_TAC [][] THEN 2014 Q.ISPEC_THEN `t` STRUCT_CASES_TAC term_CASES THEN 2015 SRW_TAC [][term_weight_thm])); 2016 2017val weight_at_swap = Save_Thm( 2018 "weight_at_swap", 2019 last (CONJUNCTS weight_at_def)); 2020 2021val weight_at_vsubst = Store_Thm( 2022 "weight_at_vsubst", 2023 ``!t w v u p. p IN valid_posns t ==> 2024 (weight_at p w ([VAR v/u] t) = weight_at p w t)``, 2025 REPEAT GEN_TAC THEN MAP_EVERY Q.ID_SPEC_TAC [`p`, `w`, `t`] THEN 2026 HO_MATCH_MP_TAC nc_INDUCTION2 THEN Q.EXISTS_TAC `{u;v}` THEN 2027 SRW_TAC [][valid_posns_thm, SUB_THM] THEN 2028 SRW_TAC [][weight_at_def, term_weight_thm]); 2029 2030val weight_at_thm = save_thm( 2031 "weight_at_thm", 2032 LIST_CONJ (butlast (CONJUNCTS weight_at_def))); 2033 2034val decreasing_def = Define` 2035 decreasing t w <=> 2036 !n p1 p2. p1 IN n_posns n t /\ 2037 p2 IN bv_posns_at (APPEND p1 [Lt]) (strip_label t) ==> 2038 weight_at (APPEND p1 [Rt]) w (strip_label t) < 2039 weight_at p2 w (strip_label t) 2040`; 2041 2042val n_posns_lam_posns = store_thm( 2043 "n_posns_lam_posns", 2044 ``!t n p. p IN n_posns n t ==> 2045 (APPEND p [Lt]) IN lam_posns (strip_label t)``, 2046 HO_MATCH_MP_TAC simple_lterm_induction THEN 2047 SRW_TAC [][lam_posns_def, n_posns_def, strip_label_thm] THEN 2048 SRW_TAC [][] THEN TRY (PROVE_TAC []) THEN 2049 FULL_SIMP_TAC (srw_ss() ++ COND_elim_ss) [] THEN RES_TAC); 2050 2051val n_posn_valid_posns = store_thm( 2052 "n_posn_valid_posns", 2053 ``!t n p. p IN n_posns n t ==> 2054 APPEND p [Rt] IN valid_posns (strip_label t) /\ 2055 APPEND p [Lt] IN valid_posns (strip_label t)``, 2056 HO_MATCH_MP_TAC simple_lterm_induction THEN 2057 SRW_TAC [][strip_label_thm, valid_posns_thm, n_posns_def] THEN 2058 SRW_TAC [][] THEN TRY (PROVE_TAC []) THEN 2059 FULL_SIMP_TAC (srw_ss() ++ COND_elim_ss) [] THEN RES_TAC); 2060 2061val decreasing_thm = store_thm( 2062 "decreasing_thm", 2063 ``(!s. decreasing (VAR s : lterm) w <=> T) /\ 2064 (!t u. decreasing (t @@ u : lterm) w <=> 2065 decreasing t (\p. w (Lt::p)) /\ 2066 decreasing u (\p. w (Rt::p))) /\ 2067 (!v t. decreasing (LAM v t : lterm) w = decreasing t (\p. w (In::p))) /\ 2068 (!n v t u. decreasing (LAMi n v t u : lterm) w <=> 2069 decreasing t (\p. w (Lt::In::p)) /\ 2070 decreasing u (\p. w (Rt::p)) /\ 2071 !p. p IN lv_posns v t ==> 2072 lterm_weight u (\p. w (Rt::p)) < 2073 weight_at p (\p. w (Lt::In::p)) (strip_label t))``, 2074 SRW_TAC [][decreasing_def, n_posns_def, strip_label_thm, RIGHT_AND_OVER_OR, 2075 DISJ_IMP_THM, GSYM LEFT_FORALL_IMP_THM, 2076 GSYM LEFT_EXISTS_AND_THM, FORALL_AND_THM] THEN 2077 SIMP_TAC (srw_ss() ++ SatisfySimps.SATISFY_ss) 2078 [GSYM AND_IMP_INTRO, bv_posns_at_thm, n_posns_lam_posns, 2079 GSYM LEFT_FORALL_IMP_THM, GSYM RIGHT_FORALL_IMP_THM, 2080 weight_at_thm, n_posn_valid_posns] THEN 2081 EQ_TAC THEN REPEAT STRIP_TAC THENL [ 2082 RES_TAC, 2083 RES_TAC, 2084 FIRST_X_ASSUM (Q.SPECL_THEN [`n`, `[]`, `Lt::In::p`] MP_TAC) THEN 2085 SIMP_TAC (srw_ss()) [weight_at_thm, bv_posns_thm, lterm_term_weight] THEN 2086 DISCH_THEN MATCH_MP_TAC THEN 2087 FULL_SIMP_TAC (srw_ss()) [lv_posns_def], 2088 RES_TAC, 2089 RES_TAC, 2090 Cases_on `n = n'` THEN FULL_SIMP_TAC (srw_ss()) [] THEN 2091 SRW_TAC [][] THEN 2092 FULL_SIMP_TAC (srw_ss()) [weight_at_thm, bv_posns_thm, lterm_term_weight, 2093 lv_posns_def] 2094 ]); 2095 2096val nonzero_def = Define` 2097 nonzero t w = !p. p IN lvar_posns t ==> 0 < w p 2098`; 2099 2100val nonzero_thm = store_thm( 2101 "nonzero_thm", 2102 ``(!s w. nonzero (VAR s : lterm) w <=> 0 < w []) /\ 2103 (!t u w. nonzero (t @@ u : lterm) w <=> 2104 nonzero t (\p. w (Lt::p)) /\ 2105 nonzero u (\p. w (Rt::p))) /\ 2106 (!v t w. nonzero (LAM v t : lterm) w <=> nonzero t (\p. w (In::p))) /\ 2107 (!n v t u. nonzero (LAMi n v t u : lterm) w <=> 2108 nonzero t (\p. w (Lt::In::p)) /\ 2109 nonzero u (\p. w (Rt::p)))``, 2110 SRW_TAC [][nonzero_def, lvar_posns_def, var_posns_thm, strip_label_thm, 2111 DISJ_IMP_THM, FORALL_AND_THM, GSYM LEFT_FORALL_IMP_THM]); 2112 2113val weight_at_times_constant = store_thm( 2114 "weight_at_times_constant", 2115 ``!t w c p. p IN valid_posns t ==> 2116 (weight_at p ($* c o w) t = c * weight_at p w t)``, 2117 HO_MATCH_MP_TAC simple_induction THEN 2118 SIMP_TAC (srw_ss()) [valid_posns_thm, weight_at_thm, term_weight_thm, 2119 DISJ_IMP_THM, GSYM LEFT_FORALL_IMP_THM, 2120 FORALL_AND_THM, combinTheory.o_DEF] THEN 2121 REPEAT STRIP_TAC THENL [ 2122 Q.PAT_X_ASSUM `!w c p. p IN valid_posns t' ==> Q w p c` 2123 (Q.SPECL_THEN [`\p. w (Rt::p)`, `c`, `[]`] MP_TAC) THEN 2124 SRW_TAC [][weight_at_thm] THEN 2125 Q.PAT_X_ASSUM `!w c p. p IN valid_posns t ==> Q w p c` 2126 (Q.SPECL_THEN [`\p. w (Lt::p)`, `c`, `[]`] MP_TAC) THEN 2127 SRW_TAC [][weight_at_thm, arithmeticTheory.LEFT_ADD_DISTRIB], 2128 POP_ASSUM (Q.SPECL_THEN [`\p. w (In::p)`, `c`, `[]`] MP_TAC) THEN 2129 SRW_TAC [][weight_at_thm] 2130 ]); 2131 2132val decreasing_times_constant = store_thm( 2133 "decreasing_times_constant", 2134 ``!t w. decreasing t w ==> !c. 0 < c ==> decreasing t ($* c o w)``, 2135 SRW_TAC [][decreasing_def] THEN 2136 `APPEND p1 [Rt] IN valid_posns (strip_label t)` 2137 by PROVE_TAC [n_posn_valid_posns] THEN 2138 `APPEND p1 [Lt] IN lam_posns (strip_label t)` 2139 by PROVE_TAC [n_posns_lam_posns] THEN 2140 `p2 IN valid_posns (strip_label t)` 2141 by PROVE_TAC [bv_posns_at_SUBSET_var_posns, 2142 var_posns_SUBSET_valid_posns] THEN RES_TAC THEN 2143 SRW_TAC [numSimps.SUC_FILTER_ss][weight_at_times_constant, 2144 arithmeticTheory.LESS_MULT_MONO]); 2145 2146val weight_at_var_posn = store_thm( 2147 "weight_at_var_posn", 2148 ``!t p w. p IN var_posns t ==> (weight_at p w t = w p)``, 2149 HO_MATCH_MP_TAC simple_induction THEN 2150 SRW_TAC [][var_posns_thm, weight_at_vsubst, 2151 var_posns_SUBSET_valid_posns] THEN 2152 SRW_TAC [][var_posns_SUBSET_valid_posns, weight_at_thm, term_weight_thm]); 2153 2154Theorem decreasing_weights_exist: 2155 ���t. ���w. nonzero t w ��� decreasing t w 2156Proof 2157 HO_MATCH_MP_TAC simple_lterm_induction THEN 2158 SIMP_TAC (srw_ss())[decreasing_thm, nonzero_thm] THEN REPEAT CONJ_TAC THENL [ 2159 Q.EXISTS_TAC `\p. 1` THEN SRW_TAC [][], 2160 2161 REPEAT STRIP_TAC THEN 2162 Q.EXISTS_TAC `\p. if HD p = Lt then w (TL p) else w' (TL p)` THEN 2163 SRW_TAC [ETA_ss][], 2164 2165 REPEAT STRIP_TAC THEN 2166 Q.EXISTS_TAC `w o TL` THEN 2167 SRW_TAC [ETA_ss][combinTheory.o_THM], 2168 2169 Q_TAC SUFF_TAC 2170 `���v t1 t2. 2171 (���w. nonzero t1 w ��� decreasing t1 w) ��� 2172 (���w. nonzero t2 w ��� decreasing t2 w) ==> 2173 ���w. 2174 nonzero t1 (��p. w (Lt::In::p)) ��� nonzero t2 (��p. w (Rt::p)) ��� 2175 decreasing t1 (��p. w (Lt::In::p)) ��� 2176 decreasing t2 (��p. w (Rt::p)) ��� 2177 ���p. p ��� lv_posns v t1 ==> 2178 lterm_weight t2 (��p. w (Rt::p)) < 2179 weight_at p (��p. w (Lt::In::p)) (strip_label t1)` 2180 THEN1 METIS_TAC [] THEN 2181 MAP_EVERY Q.X_GEN_TAC [`v`, `t1`,`t2`] THEN 2182 DISCH_THEN (CONJUNCTS_THEN2 (Q.X_CHOOSE_THEN `w1` STRIP_ASSUME_TAC) 2183 (Q.X_CHOOSE_THEN `w2` STRIP_ASSUME_TAC)) THEN 2184 Q.EXISTS_TAC `\p. if HD p = Lt then 2185 (lterm_weight t2 w2 + 1) * w1 (TL (TL p)) 2186 else w2 (TL p)` THEN 2187 SRW_TAC [ETA_ss][nonzero_def] THENL [ 2188 (* 1 *) `0 < w1 p` by PROVE_TAC [nonzero_def] THEN 2189 ASM_SIMP_TAC (srw_ss() ++ ARITH_ss) 2190 [nonzero_def, arithmeticTheory.RIGHT_ADD_DISTRIB], 2191 (* 2 *) PROVE_TAC [nonzero_def], 2192 (* 3 *) PROVE_TAC [nonzero_def], 2193 (* 4 *) 2194 ASM_SIMP_TAC (srw_ss() ++ ARITH_ss) 2195 [decreasing_times_constant, GSYM combinTheory.o_DEF], 2196 (* 5 *) 2197 `p IN valid_posns (strip_label t1)` 2198 by PROVE_TAC [lv_posns_def, v_posns_SUBSET_var_posns, 2199 var_posns_SUBSET_valid_posns] THEN 2200 ASM_SIMP_TAC (srw_ss() ++ ARITH_ss) 2201 [weight_at_times_constant, GSYM combinTheory.o_DEF] THEN 2202 Q_TAC SUFF_TAC `(!c n. 0 < c ==> n < (n + 1) * c) /\ 2203 0 < weight_at p w1 (strip_label t1)` 2204 THEN1 PROVE_TAC [] THEN 2205 `p IN var_posns (strip_label t1)` 2206 by PROVE_TAC [lv_posns_def, v_posns_SUBSET_var_posns] THEN 2207 ASM_SIMP_TAC (srw_ss()) [weight_at_var_posn] THEN 2208 `0 < w1 p` by PROVE_TAC [nonzero_def, lvar_posns_def] THEN 2209 ASM_SIMP_TAC (srw_ss()) [] THEN 2210 Induct THEN SRW_TAC [ARITH_ss][arithmeticTheory.MULT_CLAUSES] 2211 ] 2212 ] 2213QED 2214 2215val weighted_reduction_def = Define` 2216 weighted_reduction (M', w0) r (N', w) <=> 2217 lrcc beta0 M' r N' /\ (w = update_weighing (strip_label M') r w0) 2218`; 2219 2220 2221val op on = BasicProvers.on; 2222infix 8 on; 2223 2224val lrcc_redex_posn = store_thm( 2225 "lrcc_redex_posn", 2226 ``!M r N. lrcc beta0 M r N ==> r IN redex_posns (strip_label M)``, 2227 HO_MATCH_MP_TAC lrcc_ind THEN 2228 SRW_TAC [][redex_posns_thm, strip_label_thm, beta0_def] THEN 2229 SRW_TAC [][redex_posns_thm, strip_label_thm]); 2230 2231val labelled_redn_beta_redex_posn = store_thm( 2232 "labelled_redn_beta_redex_posn", 2233 ``!M r N. labelled_redn beta M r N ==> r IN redex_posns M``, 2234 HO_MATCH_MP_TAC labelled_redn_ind THEN 2235 SRW_TAC [][redex_posns_thm, beta_def] THEN 2236 SRW_TAC [][redex_posns_thm]); 2237 2238val weighted_reduction_preserves_nonzero_weighing = store_thm( 2239 "weighted_reduction_preserves_nonzero_weighing", 2240 ``!M' w0 r N' w. 2241 weighted_reduction (M', w0) r (N', w) /\ 2242 nonzero M' w0 ==> nonzero N' w``, 2243 Q_TAC SUFF_TAC 2244 `!M' r N'. 2245 lrcc beta0 M' r N' ==> 2246 !w. nonzero M' w ==> 2247 nonzero N' (update_weighing (strip_label M') r w)` THEN1 2248 SRW_TAC [][weighted_reduction_def] THEN 2249 HO_MATCH_MP_TAC strong_lrcc_ind THEN 2250 SIMP_TAC (srw_ss())[update_weighing_thm, strip_label_thm] THEN 2251 REPEAT CONJ_TAC THENL [ 2252 SRW_TAC [] [beta0_def, nonzero_def, lvar_posns_def, var_posns_thm, 2253 strip_label_thm] THEN 2254 FULL_SIMP_TAC (srw_ss() ++ DNF_ss) 2255 [strip_label_thm, var_posns_thm, var_posns_subst, 2256 bv_posns_thm, strip_label_subst, update_weighing_thm] 2257 THENL [ 2258 `!vp l. ~(vp IN v_posns v (strip_label t) /\ (APPEND vp l = p))` 2259 by (REPEAT STRIP_TAC THEN 2260 `vp IN var_posns (strip_label t)` 2261 by PROVE_TAC [v_posns_SUBSET_var_posns] THEN 2262 `l = []` by PROVE_TAC [no_var_posns_in_var_posn_prefix] THEN 2263 FULL_SIMP_TAC (srw_ss()) []) THEN 2264 SRW_TAC [][], 2265 (fn th => REWRITE_TAC [th] THEN STRIP_ASSUME_TAC th) on 2266 (`?vp l. vp IN v_posns v (strip_label t) /\ 2267 (APPEND vp l = APPEND p1 p2)`, PROVE_TAC []) THEN 2268 SELECT_ELIM_TAC THEN CONJ_TAC THEN1 PROVE_TAC [] THEN 2269 GEN_TAC THEN 2270 DISCH_THEN (Q.X_CHOOSE_THEN `vp1` STRIP_ASSUME_TAC) THEN 2271 `vp1 IN var_posns (strip_label t) /\ p1 IN var_posns (strip_label t)` 2272 by PROVE_TAC [v_posns_SUBSET_var_posns] THEN 2273 `vp1 = p1` by 2274 (`APPEND p1 p2 = APPEND vp1 x` by PROVE_TAC [] THEN 2275 POP_ASSUM MP_TAC THEN 2276 SIMP_TAC (srw_ss() ++ DNF_ss) [APPEND_CASES] THEN 2277 SRW_TAC [][] THEN PROVE_TAC [no_var_posns_in_var_posn_prefix]) THEN 2278 FULL_SIMP_TAC (srw_ss()) [] 2279 ], 2280 SIMP_TAC (srw_ss() ++ ETA_ss) [nonzero_thm, strip_label_thm], 2281 SIMP_TAC (srw_ss() ++ ETA_ss) [nonzero_thm, strip_label_thm], 2282 SRW_TAC [][nonzero_thm, strip_label_thm] THEN 2283 IMP_RES_TAC lrcc_redex_posn THEN 2284 SRW_TAC [ETA_ss][update_weighing_vsubst], 2285 SIMP_TAC (srw_ss() ++ ETA_ss) [nonzero_thm, strip_label_thm], 2286 SRW_TAC [][nonzero_thm, strip_label_thm] THEN 2287 IMP_RES_TAC lrcc_redex_posn THEN 2288 SRW_TAC [ETA_ss][] 2289 ]); 2290 2291val wterm_ordering_def = Define` 2292 wterm_ordering (N, w) (M, w0) <=> lterm_weight N w < lterm_weight M w0 2293`; 2294 2295val WF_wterm_ordering = store_thm( 2296 "WF_wterm_ordering", 2297 ``WF wterm_ordering``, 2298 `wterm_ordering = measure (\p. lterm_weight (FST p) (SND p))` 2299 by SIMP_TAC (srw_ss()) [prim_recTheory.measure_def, FUN_EQ_THM, 2300 pairTheory.FORALL_PROD, wterm_ordering_def, 2301 relationTheory.inv_image_def] THEN 2302 SRW_TAC [][prim_recTheory.WF_measure]); 2303 2304val weighing_at_def = Define`weighing_at l w = w o APPEND l`; 2305 2306val CARD_IMAGE = prove( 2307 ``!f s. (!x y. (f x = f y) = (x = y)) /\ FINITE s ==> 2308 (CARD (IMAGE f s) = CARD s)``, 2309 Q_TAC SUFF_TAC 2310 `!f. (!x y. (f x = f y) = (x = y)) ==> 2311 !s. FINITE s ==> (CARD (IMAGE f s) = CARD s)` 2312 THEN1 PROVE_TAC [] THEN 2313 GEN_TAC THEN STRIP_TAC THEN 2314 HO_MATCH_MP_TAC FINITE_INDUCT THEN 2315 SRW_TAC [][]); 2316 2317val CARD_UNION_BETTER = prove( 2318 ``!s. FINITE s ==> 2319 !t. FINITE t ==> 2320 (CARD (s UNION t) = CARD s + CARD t - CARD (s INTER t))``, 2321 REPEAT STRIP_TAC THEN 2322 `CARD (s INTER t) <= CARD s` 2323 by PROVE_TAC [CARD_INTER_LESS_EQ] THEN 2324 `CARD (s UNION t) + CARD (s INTER t) = CARD s + CARD t` 2325 by PROVE_TAC [CARD_UNION] THEN 2326 DECIDE_TAC); 2327 2328val v_posns_LE_term_weight = store_thm( 2329 "v_posns_LE_term_weight", 2330 ``!t v w. SUM_IMAGE w (v_posns v t) <= term_weight t w``, 2331 SIMP_TAC (srw_ss()) [term_weight_def] THEN 2332 REPEAT GEN_TAC THEN MATCH_MP_TAC SUM_IMAGE_SUBSET_LE THEN 2333 PROVE_TAC [SUBSET_DEF, v_posns_SUBSET_var_posns, 2334 var_posns_FINITE]); 2335 2336val size_vsubst = prove( 2337 ``!M:term. size ([VAR v/u] M) = size M``, 2338 HO_MATCH_MP_TAC nc_INDUCTION2 THEN Q.EXISTS_TAC `{u;v}` THEN 2339 SRW_TAC [][SUB_THM, SUB_VAR]); 2340 2341val old_induction = prove( 2342 ``!P. (!x. P (VAR x)) /\ 2343 (!t u. P t /\ P u ==> P (t @@ u)) /\ 2344 (!x u. (!y'. P ([VAR y'/x] u)) ==> P (LAM x u)) ==> 2345 !u:term. P u``, 2346 REPEAT STRIP_TAC THEN 2347 completeInduct_on `size u` THEN GEN_TAC THEN 2348 Q.SPEC_THEN `u` STRUCT_CASES_TAC term_CASES THEN 2349 SRW_TAC [][] THENL [ 2350 FIRST_X_ASSUM MATCH_MP_TAC THEN 2351 FULL_SIMP_TAC (srw_ss()) [GSYM RIGHT_FORALL_IMP_THM] THEN 2352 SRW_TAC [numSimps.ARITH_ss][], 2353 FIRST_X_ASSUM MATCH_MP_TAC THEN 2354 FULL_SIMP_TAC (srw_ss()) [GSYM RIGHT_FORALL_IMP_THM] THEN 2355 SRW_TAC [numSimps.ARITH_ss][size_vsubst] 2356 ]); 2357 2358 2359val weight_at_subst = store_thm( 2360 "weight_at_subst", 2361 ``!t u v p w. 2362 p IN valid_posns ([u/v] t) ==> 2363 (weight_at p (update_weighing ((LAM v t) @@ u) [] w) ([u/v] t) = 2364 if ?vp l. vp IN v_posns v t /\ (APPEND vp l = p) then 2365 weight_at (@l. ?vp. vp IN v_posns v t /\ (APPEND vp l = p)) 2366 (\p. w (Rt::p)) 2367 u 2368 else 2369 let vps = { p' | (?p''. p' = APPEND p p'') /\ 2370 p' IN v_posns v t } 2371 in 2372 weight_at p (\p. w (Lt::In::p)) t - 2373 SUM_IMAGE (\p. w (Lt::In::p)) vps + 2374 CARD vps * term_weight u (\p. w (Rt::p)))``, 2375 2376 HO_MATCH_MP_TAC old_induction THEN REPEAT CONJ_TAC THENL [ 2377 SRW_TAC [ARITH_ss] 2378 [v_posns_thm, term_weight_thm, valid_posns_thm, 2379 SUB_THM, update_weighing_def, bv_posns_thm, 2380 weight_at_thm, SUM_IMAGE_THM] THEN 2381 FULL_SIMP_TAC (srw_ss()) [], 2382 SRW_TAC [][v_posns_thm, valid_posns_thm, SUB_THM] THENL [ 2383 SIMP_TAC (srw_ss() ++ DNF_ss) [weight_at_thm, term_weight_thm] THEN 2384 FIRST_X_ASSUM (Q.SPECL_THEN [`u`,`v`,`[]`] MP_TAC) THEN 2385 SRW_TAC [][weight_at_thm, GSPEC_OR] THEN 2386 FIRST_X_ASSUM (Q.SPECL_THEN [`u`,`v`,`[]`] MP_TAC) THEN 2387 SRW_TAC [][weight_at_thm, GSPEC_OR] THEN 2388 FULL_SIMP_TAC (srw_ss() ++ DNF_ss) [update_weighing_def, bv_posns_thm, 2389 v_posns_thm] THEN 2390 FIRST_X_ASSUM (Q.SPEC_THEN `\q. if HD q = Lt then 2391 w (HD q :: HD (TL q) :: Lt :: 2392 TL (TL q)) 2393 else w q` 2394 (ASSUME_TAC o SIMP_RULE (srw_ss()) [])) THEN 2395 POP_ASSUM (fn th => 2396 REWRITE_TAC [CONV_RULE 2397 (ONCE_DEPTH_CONV (SWAP_VARS_CONV)) th]) THEN 2398 FIRST_X_ASSUM (Q.SPEC_THEN `\q. if HD q = Lt then 2399 w (HD q :: HD (TL q) :: Rt :: 2400 TL (TL q)) 2401 else w q` 2402 (ASSUME_TAC o SIMP_RULE (srw_ss()) [])) THEN 2403 POP_ASSUM (fn th => 2404 REWRITE_TAC [CONV_RULE 2405 (ONCE_DEPTH_CONV (SWAP_VARS_CONV)) th]) THEN 2406 SRW_TAC [][NIL_IN_v_posns] THENL [ 2407 `{[Lt]} UNION {[Rt]} = {[Lt]; [Rt]}` by SRW_TAC [][EXTENSION] THEN 2408 SRW_TAC [ARITH_ss][v_posns_thm, term_weight_thm, GSPEC_EQ, 2409 SUM_IMAGE_THM, 2410 SUM_IMAGE_DELETE], 2411 `{p' | ?x. (p' = Rt::x) /\ x IN v_posns v t'} = 2412 IMAGE (CONS Rt) (v_posns v t')` by SRW_TAC [][EXTENSION] THEN 2413 SRW_TAC [][v_posns_thm, term_weight_thm, GSPEC_EQ, 2414 GSYM INSERT_SING_UNION, 2415 SUM_IMAGE_THM, delete_non_element, 2416 arithmeticTheory.MULT_CLAUSES, SUM_IMAGE_IMAGE, 2417 combinTheory.o_DEF, CARD_IMAGE] THEN 2418 DECIDE_TAC, 2419 `{p' | ?x. (p' = Lt::x) /\ x IN v_posns v t} = 2420 IMAGE (CONS Lt) (v_posns v t)` by SRW_TAC [][EXTENSION] THEN 2421 SRW_TAC [] [v_posns_thm, term_weight_thm, GSPEC_EQ, 2422 SUM_IMAGE_IMAGE, 2423 GSYM (ONCE_REWRITE_RULE [UNION_COMM] 2424 INSERT_SING_UNION), 2425 SUM_IMAGE_THM, delete_non_element, 2426 combinTheory.o_DEF, arithmeticTheory.MULT_CLAUSES, 2427 CARD_IMAGE] THEN DECIDE_TAC, 2428 `{p' | ?x. (p' = Rt::x) /\ x IN v_posns v t'} = 2429 IMAGE (CONS Rt) (v_posns v t')` by SRW_TAC [][EXTENSION] THEN 2430 `{p' | ?x. (p' = Lt::x) /\ x IN v_posns v t} = 2431 IMAGE (CONS Lt) (v_posns v t)` by SRW_TAC [][EXTENSION] THEN 2432 SRW_TAC [] [v_posns_thm, term_weight_thm, GSPEC_EQ, 2433 SUM_IMAGE_IMAGE, 2434 SUM_IMAGE_THM, delete_non_element, 2435 combinTheory.o_DEF, arithmeticTheory.MULT_CLAUSES, 2436 CARD_IMAGE, SUM_IMAGE_UNION] THEN 2437 `!x y. IMAGE (CONS Lt) x INTER IMAGE (CONS Rt) y = {}` by 2438 (SRW_TAC [][EXTENSION] THEN 2439 SPOSE_NOT_THEN STRIP_ASSUME_TAC THEN 2440 FULL_SIMP_TAC (srw_ss()) []) THEN 2441 SRW_TAC [][SUM_IMAGE_THM, CARD_UNION_BETTER, 2442 arithmeticTheory.RIGHT_ADD_DISTRIB, CARD_IMAGE] THEN 2443 Q.SPECL_THEN [`t'`, `v`, `\p. w(Lt::In::Rt::p)`] MP_TAC 2444 v_posns_LE_term_weight THEN 2445 Q.SPECL_THEN [`t`, `v`, `\p. w(Lt::In::Lt::p)`] MP_TAC 2446 v_posns_LE_term_weight THEN 2447 numLib.ARITH_TAC 2448 ], 2449 2450 SIMP_TAC (srw_ss() ++ DNF_ss) [] THEN 2451 `!p p1 p2 r. ~((p = Lt::p1) /\ (p = Rt::p2) /\ r)` 2452 by SIMP_TAC (srw_ss()) [] THEN ASM_REWRITE_TAC [] THEN 2453 POP_ASSUM (K ALL_TAC) THEN RES_THEN MP_TAC THEN 2454 REPEAT (FIRST_X_ASSUM (K ALL_TAC o assert (is_forall o concl))) THEN 2455 ASM_SIMP_TAC (srw_ss()) [weight_at_thm] THEN 2456 CONV_TAC (LAND_CONV (ONCE_DEPTH_CONV SWAP_VARS_CONV)) THEN 2457 DISCH_THEN (Q.SPEC_THEN `\p. if HD p = Lt then 2458 w (Lt::In::Lt::TL (TL p)) 2459 else w p` MP_TAC) THEN 2460 SIMP_TAC (srw_ss()) [] THEN 2461 Cases_on `?l vp. vp IN v_posns v t /\ (APPEND vp l = x)` THENL [ 2462 ASM_SIMP_TAC (srw_ss()) [] THEN 2463 DISCH_THEN (fn th => REWRITE_TAC [SYM th]) THEN 2464 ASM_SIMP_TAC (srw_ss() ++ DNF_ss) 2465 [update_weighing_def, bv_posns_thm, v_posns_thm] THEN 2466 CONV_TAC (LAND_CONV (ONCE_DEPTH_CONV SWAP_VARS_CONV)) THEN 2467 REWRITE_TAC [], 2468 ASM_SIMP_TAC (srw_ss()) [] THEN 2469 `{p | ?a b. (p = Lt::APPEND x a) /\ (p = Lt::b) /\ b IN v_posns v t} = 2470 IMAGE (CONS Lt) {p | ?a. (p = APPEND x a) /\ p IN v_posns v t}` 2471 by SRW_TAC [][EXTENSION, EQ_IMP_THM] THEN 2472 `FINITE {p | ?a. (p = APPEND x a) /\ p IN v_posns v t}` 2473 by (MATCH_MP_TAC (MATCH_MP SUBSET_FINITE 2474 (Q.SPEC `t` var_posns_FINITE)) THEN 2475 SRW_TAC [][SUBSET_DEF] THEN 2476 PROVE_TAC [v_posns_SUBSET_var_posns]) THEN 2477 `x IN valid_posns t` 2478 by (FULL_SIMP_TAC (srw_ss()) [valid_posns_subst] THEN 2479 PROVE_TAC []) THEN 2480 ASM_SIMP_TAC (srw_ss() ++ DNF_ss) [CARD_IMAGE, SUM_IMAGE_IMAGE, 2481 combinTheory.o_DEF, 2482 weight_at_thm] THEN 2483 DISCH_THEN (fn th => REWRITE_TAC [SYM th]) THEN 2484 ASM_SIMP_TAC (srw_ss() ++ DNF_ss) 2485 [update_weighing_def, bv_posns_thm, v_posns_thm] THEN 2486 CONV_TAC (LAND_CONV (ONCE_DEPTH_CONV SWAP_VARS_CONV)) THEN 2487 REWRITE_TAC [] 2488 ], 2489 2490 SIMP_TAC (srw_ss() ++ DNF_ss) [] THEN 2491 `!p p1 p2 r. ~((p = Rt::p1) /\ (p = Lt::p2) /\ r)` 2492 by SIMP_TAC (srw_ss()) [] THEN ASM_REWRITE_TAC [] THEN 2493 POP_ASSUM (K ALL_TAC) THEN RES_THEN MP_TAC THEN 2494 REPEAT (FIRST_X_ASSUM (K ALL_TAC o assert (is_forall o concl))) THEN 2495 ASM_SIMP_TAC (srw_ss()) [weight_at_thm] THEN 2496 CONV_TAC (LAND_CONV (ONCE_DEPTH_CONV SWAP_VARS_CONV)) THEN 2497 DISCH_THEN (Q.SPEC_THEN `\p. if HD p = Lt then 2498 w (Lt::In::Rt::TL (TL p)) 2499 else w p` MP_TAC) THEN 2500 SIMP_TAC (srw_ss()) [] THEN 2501 Cases_on `?l vp. vp IN v_posns v t' /\ (APPEND vp l = x)` THENL [ 2502 ASM_SIMP_TAC (srw_ss()) [] THEN 2503 DISCH_THEN (fn th => REWRITE_TAC [SYM th]) THEN 2504 ASM_SIMP_TAC (srw_ss() ++ DNF_ss) 2505 [update_weighing_def, bv_posns_thm, v_posns_thm] THEN 2506 CONV_TAC (LAND_CONV (ONCE_DEPTH_CONV SWAP_VARS_CONV)) THEN 2507 REWRITE_TAC [], 2508 2509 ASM_SIMP_TAC (srw_ss()) [] THEN 2510 `{p | ?a b. (p = Rt::APPEND x a) /\ (p = Rt::b) /\ b IN v_posns v t'} = 2511 IMAGE (CONS Rt) {p | ?a. (p = APPEND x a) /\ p IN v_posns v t'}` 2512 by SRW_TAC [][EXTENSION, EQ_IMP_THM] THEN 2513 `FINITE {p | ?a. (p = APPEND x a) /\ p IN v_posns v t'}` 2514 by (MATCH_MP_TAC (MATCH_MP SUBSET_FINITE 2515 (Q.SPEC `t'` var_posns_FINITE)) THEN 2516 SRW_TAC [][SUBSET_DEF] THEN 2517 PROVE_TAC [v_posns_SUBSET_var_posns]) THEN 2518 `x IN valid_posns t'` 2519 by (FULL_SIMP_TAC (srw_ss()) [valid_posns_subst] THEN 2520 PROVE_TAC []) THEN 2521 ASM_SIMP_TAC (srw_ss() ++ DNF_ss) [CARD_IMAGE, SUM_IMAGE_IMAGE, 2522 combinTheory.o_DEF, 2523 weight_at_thm] THEN 2524 DISCH_THEN (fn th => REWRITE_TAC [SYM th]) THEN 2525 ASM_SIMP_TAC (srw_ss() ++ DNF_ss) 2526 [update_weighing_def, bv_posns_thm, v_posns_thm] THEN 2527 CONV_TAC (LAND_CONV (ONCE_DEPTH_CONV SWAP_VARS_CONV)) THEN 2528 REWRITE_TAC [] 2529 ] 2530 ], 2531 2532 (* abstraction case *) 2533 REPEAT GEN_TAC THEN STRIP_TAC THEN REPEAT GEN_TAC THEN 2534 Q_TAC (NEW_TAC "z") `{x;v} UNION FV t UNION FV u` THEN 2535 `LAM x t = LAM z ([VAR z/x] t)` by SRW_TAC [][SIMPLE_ALPHA] THEN 2536 ASM_SIMP_TAC (srw_ss() ++ DNF_ss) [SUB_THM, v_posns_thm] THEN 2537 SIMP_TAC (srw_ss()) [valid_posns_thm] THEN STRIP_TAC THENL [ 2538 ASM_SIMP_TAC (srw_ss()) [term_weight_thm, weight_at_thm] THEN 2539 FIRST_X_ASSUM (Q.SPECL_THEN [`z`,`u`,`v`,`[]`] MP_TAC) THEN 2540 ASM_SIMP_TAC (srw_ss()) [weight_at_thm, term_weight_thm] THEN 2541 DISCH_THEN (Q.SPEC_THEN `\p. if HD p = Lt then 2542 w (Lt::In::In::(TL (TL p))) 2543 else w p` MP_TAC) THEN 2544 Cases_on `[] IN v_posns v ([VAR z/x] t)` THENL [ 2545 ASM_SIMP_TAC (srw_ss()) [] THEN 2546 `~(x = v) /\ (t = VAR v)` 2547 by (FULL_SIMP_TAC (srw_ss()) [v_posns_vsubst] THEN 2548 POP_ASSUM MP_TAC THEN SRW_TAC [][NIL_IN_v_posns]) THEN 2549 ASM_SIMP_TAC (srw_ss()) [SUB_THM, term_weight_thm] THEN 2550 ASM_SIMP_TAC (srw_ss() ++ DNF_ss) 2551 [update_weighing_def, bv_posns_thm, v_posns_thm, 2552 GSPEC_EQ, SUM_IMAGE_SING] THEN 2553 DECIDE_TAC, 2554 ASM_SIMP_TAC (srw_ss()) [] THEN 2555 ASM_SIMP_TAC (srw_ss() ++ DNF_ss) 2556 [update_weighing_thm, bv_posns_thm, v_posns_thm] THEN 2557 CONV_TAC (LAND_CONV (ONCE_DEPTH_CONV SWAP_VARS_CONV)) THEN 2558 DISCH_THEN (fn th => REWRITE_TAC [th]) THEN 2559 Cases_on `v = x` THEN 2560 ASM_SIMP_TAC (srw_ss()) [SUM_IMAGE_IMAGE, CARD_IMAGE, 2561 v_posns_FINITE, combinTheory.o_DEF, 2562 v_posns_vsubst, 2563 SUM_IMAGE_THM] 2564 ], 2565 2566 Cases_on `v = x` THENL [ 2567 SRW_TAC [][update_weighing_thm, SUB_TWICE_ONE_VAR, SUB_THM, 2568 bv_posns_thm, v_posns_thm, v_posns_vsubst, 2569 SUM_IMAGE_THM], 2570 ALL_TAC 2571 ] THEN 2572 ASM_SIMP_TAC (srw_ss() ++ DNF_ss) [weight_at_thm] THEN GEN_TAC THEN 2573 FIRST_X_ASSUM (Q.SPECL_THEN [`z`,`u`,`v`,`x'`] MP_TAC) THEN 2574 SIMP_TAC (srw_ss() ++ DNF_ss) [update_weighing_def, bv_posns_thm] THEN 2575 ASM_SIMP_TAC (srw_ss() ++ DNF_ss) [v_posns_thm, v_posns_vsubst] THEN 2576 DISCH_THEN (Q.SPEC_THEN `\p. if HD p = Lt then 2577 w (Lt::In::In::(TL (TL p))) 2578 else w p` MP_TAC) THEN 2579 ASM_SIMP_TAC (srw_ss()) [] THEN 2580 CONV_TAC (LAND_CONV (ONCE_DEPTH_CONV SWAP_VARS_CONV)) THEN 2581 DISCH_THEN (fn th => SIMP_TAC (srw_ss()) [th]) THEN 2582 COND_CASES_TAC THEN SRW_TAC [][] THEN 2583 `{p | ?a b. (p = In::APPEND x' a) /\ (p = In::b) /\ 2584 b IN v_posns v t} = 2585 IMAGE (CONS In) { p | ?a. (p = APPEND x' a) /\ (p IN v_posns v t)}` 2586 by SRW_TAC [][EXTENSION, EQ_IMP_THM] THEN 2587 ASM_SIMP_TAC (srw_ss()) [] THEN 2588 `FINITE {p | ?a. (p = APPEND x' a) /\ (p IN v_posns v t)}` 2589 by (MATCH_MP_TAC (MATCH_MP SUBSET_FINITE 2590 (Q.SPEC `t` var_posns_FINITE)) THEN 2591 ASM_SIMP_TAC (srw_ss() ++ DNF_ss) 2592 [SUBSET_DEF] THEN 2593 PROVE_TAC [v_posns_SUBSET_var_posns]) THEN 2594 ASM_SIMP_TAC (srw_ss() ++ DNF_ss) [SUM_IMAGE_IMAGE, CARD_IMAGE, 2595 combinTheory.o_DEF] 2596 ] 2597 ]); 2598 2599val list_append_lemma = prove( (* thanks be to KG! *) 2600 ``!m n. ((m = APPEND m n) = (n = [])) /\ 2601 ((APPEND m n = m) = (n = [])) /\ 2602 ((m = APPEND n m) = (n = [])) /\ 2603 ((APPEND n m = m) = (n = []))``, 2604 SIMP_TAC (srw_ss() ++ DNF_ss) [EQ_IMP_THM] THEN REPEAT CONJ_TAC THEN 2605 REPEAT GEN_TAC THEN DISCH_THEN (MP_TAC o Q.AP_TERM `LENGTH`) THEN 2606 SRW_TAC [][DECIDE ``((x + y = x) = (y = 0)) /\ ((y + x = x) = (y = 0)) /\ 2607 ((x = x + y) = (y = 0)) /\ ((x = y + x) = (y = 0))``] 2608 THEN PROVE_TAC [listTheory.LENGTH_NIL]); 2609 2610val _ = augment_srw_ss [rewrites [list_append_lemma]] 2611 2612val lv_posns_n_posns = store_thm( 2613 "lv_posns_n_posns", 2614 ``!t p n v. ~(p IN n_posns n t /\ p IN lv_posns v t)``, 2615 REPEAT STRIP_TAC THEN 2616 `APPEND p [Lt] IN lam_posns (strip_label t)` 2617 by PROVE_TAC [n_posns_lam_posns] THEN 2618 `APPEND p [Lt] IN valid_posns (strip_label t)` 2619 by PROVE_TAC [lam_posns_SUBSET_valid_posns] THEN 2620 `p IN var_posns (strip_label t)` 2621 by PROVE_TAC [v_posns_SUBSET_var_posns, lv_posns_def] THEN 2622 PROVE_TAC [cant_be_deeper_than_var_posns, listTheory.NOT_NIL_CONS]); 2623 2624val CARD_SUM_IMAGE_LE = prove( 2625 ``!s. FINITE s /\ 2626 (!e. e IN s ==> c < f e) ==> 2627 CARD s * c <= SUM_IMAGE f s``, 2628 REWRITE_TAC [GSYM AND_IMP_INTRO] THEN 2629 HO_MATCH_MP_TAC FINITE_INDUCT THEN 2630 SRW_TAC [DNF_ss] [arithmeticTheory.MULT_CLAUSES, 2631 SUM_IMAGE_THM, delete_non_element] THEN 2632 FULL_SIMP_TAC (srw_ss() ++ARITH_ss)[]); 2633 2634val CARD_SUM_IMAGE_LT = prove( 2635 ``!s. FINITE s /\ ~(s = {}) /\ (!e. e IN s ==> c < f e) ==> 2636 CARD s * c < SUM_IMAGE f s``, 2637 REWRITE_TAC [GSYM AND_IMP_INTRO] THEN 2638 HO_MATCH_MP_TAC FINITE_INDUCT THEN 2639 SRW_TAC [DNF_ss] [arithmeticTheory.MULT_CLAUSES, 2640 SUM_IMAGE_THM, delete_non_element] THEN 2641 Cases_on `s = {}` THEN FULL_SIMP_TAC (srw_ss() ++ ARITH_ss)[]); 2642 2643 2644val weight_at_SUM_IMAGE = store_thm( 2645 "weight_at_SUM_IMAGE", 2646 ``!t p w. 2647 p IN valid_posns t ==> 2648 (weight_at p w t = SUM_IMAGE w ({ p' | (?p''. APPEND p p'' = p') /\ 2649 p' IN var_posns t}))``, 2650 HO_MATCH_MP_TAC simple_induction THEN 2651 SRW_TAC [][valid_posns_thm, var_posns_thm, GSPEC_EQ, 2652 SUM_IMAGE_THM, weight_at_thm, 2653 term_weight_thm, arithmeticTheory.ADD_CLAUSES] 2654 THENL [ 2655 SRW_TAC [][weight_at_thm, term_weight_def, var_posns_thm] THEN 2656 REPEAT AP_TERM_TAC THEN SRW_TAC [][EXTENSION], 2657 SRW_TAC [CONJ_ss, DNF_ss][weight_at_thm] THEN 2658 `(\p. w (Lt::p)) = w o CONS Lt` by SRW_TAC [][FUN_EQ_THM] THEN 2659 `FINITE {p' | ?p''. (APPEND x p'' = p') /\ p' IN var_posns t}` 2660 by (MATCH_MP_TAC (MATCH_MP SUBSET_FINITE 2661 (Q.SPEC `t` var_posns_FINITE)) THEN 2662 SRW_TAC [][SUBSET_DEF]) THEN 2663 ASM_SIMP_TAC (srw_ss()) [GSYM SUM_IMAGE_IMAGE] THEN 2664 REPEAT AP_TERM_TAC THEN SRW_TAC [DNF_ss][EXTENSION], 2665 SRW_TAC [CONJ_ss, DNF_ss][weight_at_thm] THEN 2666 `(\p. w (Rt::p)) = w o CONS Rt` by SRW_TAC [][FUN_EQ_THM] THEN 2667 `FINITE {p' | ?p''. (APPEND x p'' = p') /\ p' IN var_posns t'}` 2668 by (MATCH_MP_TAC (MATCH_MP SUBSET_FINITE 2669 (Q.SPEC `t'` var_posns_FINITE)) THEN 2670 SRW_TAC [][SUBSET_DEF]) THEN 2671 ASM_SIMP_TAC (srw_ss()) [GSYM SUM_IMAGE_IMAGE] THEN 2672 REPEAT AP_TERM_TAC THEN SRW_TAC [DNF_ss][EXTENSION], 2673 SRW_TAC [][weight_at_thm, term_weight_def, var_posns_thm] THEN 2674 REPEAT AP_TERM_TAC THEN SRW_TAC [DNF_ss][EXTENSION], 2675 SRW_TAC [CONJ_ss, DNF_ss][weight_at_thm] THEN 2676 `(\p. w (In::p)) = w o CONS In` by SRW_TAC [][FUN_EQ_THM] THEN 2677 `FINITE {p' | ?p''. (APPEND x p'' = p') /\ p' IN var_posns t}` 2678 by (MATCH_MP_TAC (MATCH_MP SUBSET_FINITE 2679 (Q.SPEC `t` var_posns_FINITE)) THEN 2680 SRW_TAC [][SUBSET_DEF]) THEN 2681 ASM_SIMP_TAC (srw_ss()) [GSYM SUM_IMAGE_IMAGE] THEN 2682 REPEAT AP_TERM_TAC THEN SRW_TAC [DNF_ss][EXTENSION] 2683 ]); 2684 2685val FV_weights_update_weighing = store_thm( 2686 "FV_weights_update_weighing", 2687 ``!x r y. 2688 labelled_redn beta x r y ==> 2689 !p v. p IN v_posns v y ==> 2690 ?p'. p' IN v_posns v x /\ 2691 (!wf. weight_at p (update_weighing x r wf) y = 2692 weight_at p' wf x)``, 2693 HO_MATCH_MP_TAC strong_labelled_redn_ind THEN 2694 SIMP_TAC (srw_ss())[update_weighing_def, v_posns_thm, beta_def] THEN 2695 REPEAT STRIP_TAC THEN REPEAT VAR_EQ_TAC THENL [ 2696 `p IN var_posns ([arg/x'] body) /\ 2697 p IN valid_posns ([arg/x'] body)` 2698 by PROVE_TAC [v_posns_SUBSET_var_posns, 2699 var_posns_SUBSET_valid_posns] THEN 2700 FULL_SIMP_TAC (srw_ss()) [v_posns_subst, v_posns_thm, rator_thm, 2701 bv_posns_thm] THEN 2702 Cases_on `v = x'` THENL [ 2703 FULL_SIMP_TAC (srw_ss()) [v_posns_thm] THEN 2704 Q.EXISTS_TAC `Rt::p2` THEN 2705 `p2 IN var_posns arg /\ p2 IN valid_posns arg` 2706 by PROVE_TAC [v_posns_SUBSET_var_posns, 2707 var_posns_SUBSET_valid_posns] THEN 2708 REPEAT VAR_EQ_TAC THEN 2709 ASM_SIMP_TAC (srw_ss() ++ DNF_ss) [weight_at_thm, 2710 weight_at_var_posn] THEN 2711 `!vp l. 2712 vp IN v_posns v body /\ (APPEND vp l = APPEND p1 p2) <=> 2713 (vp = p1) /\ (l = p2)` 2714 by (ASM_SIMP_TAC (srw_ss()) [EQ_IMP_THM] THEN STRIP_TAC THEN 2715 PROVE_TAC [APPEND_var_posns, v_posns_SUBSET_var_posns]) THEN 2716 ASM_SIMP_TAC (srw_ss() ++ DNF_ss) [update_weighing_thm, bv_posns_thm], 2717 FULL_SIMP_TAC (srw_ss()) [v_posns_thm] THENL [ 2718 Q.EXISTS_TAC `Lt::In::p` THEN 2719 `p IN var_posns body /\ p IN valid_posns body` 2720 by PROVE_TAC [v_posns_SUBSET_var_posns, 2721 var_posns_SUBSET_valid_posns] THEN 2722 ASM_SIMP_TAC (srw_ss()) [weight_at_thm, valid_posns_thm, 2723 weight_at_var_posn] THEN 2724 ASM_SIMP_TAC (srw_ss() ++ DNF_ss) 2725 [update_weighing_def, bv_posns_thm] THEN 2726 GEN_TAC THEN COND_CASES_TAC THENL [ 2727 POP_ASSUM STRIP_ASSUME_TAC THEN 2728 `l = []` by PROVE_TAC [v_posns_SUBSET_var_posns, 2729 no_var_posns_in_var_posn_prefix] THEN 2730 FULL_SIMP_TAC (srw_ss()) [] THEN 2731 PROVE_TAC [v_posns_injective], 2732 REWRITE_TAC [] 2733 ], 2734 Q.EXISTS_TAC `Rt::p2` THEN 2735 `p2 IN var_posns arg /\ p2 IN valid_posns arg` 2736 by PROVE_TAC [v_posns_SUBSET_var_posns, 2737 var_posns_SUBSET_valid_posns] THEN 2738 ASM_SIMP_TAC (srw_ss()) [weight_at_thm, valid_posns_thm] THEN 2739 REPEAT VAR_EQ_TAC THEN 2740 ASM_SIMP_TAC (srw_ss()) [weight_at_var_posn] THEN 2741 ASM_SIMP_TAC (srw_ss() ++ DNF_ss) 2742 [update_weighing_def, bv_posns_thm] THEN 2743 `!vp l. vp IN v_posns x' body /\ (APPEND vp l = APPEND p1 p2) <=> 2744 (vp = p1) /\ (l = p2)` 2745 by (ASM_SIMP_TAC (srw_ss()) [EQ_IMP_THM] THEN 2746 REPEAT GEN_TAC THEN STRIP_TAC THEN 2747 PROVE_TAC [APPEND_var_posns, v_posns_SUBSET_var_posns]) THEN 2748 ASM_SIMP_TAC (srw_ss()) [] 2749 ] 2750 ], 2751 2752 RES_THEN (Q.X_CHOOSE_THEN `p1` STRIP_ASSUME_TAC) THEN 2753 `x' IN valid_posns y /\ p1 IN valid_posns x` 2754 by PROVE_TAC [v_posns_SUBSET_var_posns, 2755 var_posns_SUBSET_valid_posns] THEN 2756 Q.EXISTS_TAC `Lt::p1` THEN 2757 ASM_SIMP_TAC (srw_ss() ++ ETA_ss) [weight_at_thm], 2758 2759 Q.EXISTS_TAC `Rt::x'` THEN 2760 `x' IN valid_posns z` by PROVE_TAC [v_posns_SUBSET_var_posns, 2761 var_posns_SUBSET_valid_posns] THEN 2762 ASM_SIMP_TAC (srw_ss())[weight_at_thm], 2763 2764 Q.EXISTS_TAC `Lt::x'` THEN 2765 `x' IN valid_posns z` by PROVE_TAC [v_posns_SUBSET_var_posns, 2766 var_posns_SUBSET_valid_posns] THEN 2767 ASM_SIMP_TAC (srw_ss())[weight_at_thm], 2768 2769 RES_THEN (Q.X_CHOOSE_THEN `p1` STRIP_ASSUME_TAC) THEN 2770 `x' IN valid_posns y /\ p1 IN valid_posns x` 2771 by PROVE_TAC [v_posns_SUBSET_var_posns, 2772 var_posns_SUBSET_valid_posns] THEN 2773 Q.EXISTS_TAC `Rt::p1` THEN 2774 ASM_SIMP_TAC (srw_ss() ++ ETA_ss) [weight_at_thm], 2775 2776 `r IN redex_posns x` by PROVE_TAC [labelled_redn_beta_redex_posn] THEN 2777 ASM_SIMP_TAC (srw_ss()) [update_weighing_vsubst] THEN 2778 Cases_on `v = v'` THEN FULL_SIMP_TAC (srw_ss()) [v_posns_thm] THEN 2779 ASM_SIMP_TAC (srw_ss() ++ DNF_ss) [] THEN 2780 RES_THEN (Q.X_CHOOSE_THEN `p1` STRIP_ASSUME_TAC) THEN 2781 `x' IN valid_posns y /\ p1 IN valid_posns x` 2782 by PROVE_TAC [v_posns_SUBSET_var_posns, 2783 var_posns_SUBSET_valid_posns] THEN 2784 Q.EXISTS_TAC `p1` THEN 2785 ASM_SIMP_TAC (srw_ss() ++ ETA_ss) [weight_at_thm] 2786 ]); 2787 2788val nonzero_term_weight = store_thm( 2789 "nonzero_term_weight", 2790 ``!t w. nonzero t w ==> 0 < lterm_weight t w``, 2791 HO_MATCH_MP_TAC simple_lterm_induction THEN 2792 SRW_TAC [][nonzero_thm, lterm_weight_thm] THEN 2793 RES_TAC THEN SRW_TAC [ARITH_ss][]); 2794 2795val weighted_reduction_reduces_ordering = store_thm( 2796 "weighted_reduction_reduces_ordering", 2797 ``!M w0 N w r. weighted_reduction (M, w0) r (N, w) /\ 2798 decreasing M w0 /\ nonzero M w0 ==> 2799 decreasing N w /\ nonzero N w /\ 2800 wterm_ordering (N, w) (M, w0)``, 2801 Q_TAC SUFF_TAC 2802 `!M r N. lrcc beta0 M r N ==> 2803 !w0 w. decreasing M w0 /\ nonzero M w0 /\ 2804 (w = update_weighing (strip_label M) r w0) ==> 2805 decreasing N w /\ wterm_ordering (N, w) (M, w0)` THEN1 2806 (SRW_TAC [][weighted_reduction_def] THEN 2807 PROVE_TAC [weighted_reduction_preserves_nonzero_weighing, 2808 weighted_reduction_def]) THEN 2809 HO_MATCH_MP_TAC strong_lrcc_ind THEN REPEAT CONJ_TAC THENL [ 2810 SIMP_TAC (srw_ss() ++ DNF_ss) 2811 [beta0_def, strip_label_thm, decreasing_thm, 2812 nonzero_thm] THEN REPEAT STRIP_TAC 2813 THENL [ 2814 ASM_SIMP_TAC (srw_ss()) [decreasing_def] THEN 2815 REPEAT STRIP_TAC THEN 2816 `strip_label ([u/v] t) = [strip_label u/v] (strip_label t)` 2817 by SRW_TAC [][strip_label_subst] THEN 2818 FULL_SIMP_TAC bool_ss [] THEN 2819 `p1 ++ [Rt] ��� valid_posns ([strip_label u/v](strip_label t))` 2820 by PROVE_TAC [n_posn_valid_posns] THEN 2821 SRW_TAC [][weight_at_subst] THENL [ 2822 SIMP_TAC (srw_ss() ++ DNF_ss) [bv_posns_thm, update_weighing_def, 2823 v_posns_thm] THEN 2824 (* p1 : the position within t of a marked redex 2825 vp : at least the RHS of this redex was within u, originally and 2826 has been substituted into t. vp is the position of the 2827 variable v within t where the substitution happened. 2828 l : appended onto vp, gives the position of the RHS of the 2829 redex within t. On its own, gives the position within u of 2830 that. 2831 p2 : position of a bound variable within the LHS of the redex *) 2832 `p1 ++ [Lt] ��� lam_posns ([strip_label u/v] (strip_label t))` 2833 by PROVE_TAC [n_posns_lam_posns] THEN 2834 `p2 ��� var_posns ([strip_label u/v] (strip_label t))` 2835 by PROVE_TAC [bv_posns_at_SUBSET_var_posns] THEN 2836 ASM_SIMP_TAC (srw_ss()) [weight_at_var_posn] THEN 2837 Q.ASM_CASES_TAC 2838 `���bvp m. bvp ��� v_posns v (strip_label t) /\ (bvp ++ m = p2)` 2839 THENL [ 2840 (* the bound variable was also within u, meaning that the whole 2841 redex was within u *) 2842 ASM_SIMP_TAC (srw_ss()) [] THEN 2843 `vp ��� var_posns (strip_label t)` 2844 by PROVE_TAC [v_posns_SUBSET_var_posns] THEN 2845 `?p'. (p1 = vp ++ p') /\ (p' ��� n_posns n u)` 2846 by (`p2 IN var_posns (strip_label t) /\ 2847 ~(p2 IN v_posns v (strip_label t)) \/ 2848 ?bvp' m'. (p2 = APPEND bvp' m') /\ 2849 bvp' IN v_posns v (strip_label t) /\ 2850 m' IN var_posns (strip_label u)` 2851 by (FULL_SIMP_TAC (srw_ss()) [var_posns_subst] THEN 2852 PROVE_TAC []) THEN 2853 FULL_SIMP_TAC (srw_ss()) [] THENL [ 2854 (* p2 in var_posns (strip_label t) *) 2855 FULL_SIMP_TAC (srw_ss()) [] THEN 2856 `bvp IN var_posns (strip_label t)` 2857 by PROVE_TAC [v_posns_SUBSET_var_posns] THEN 2858 `m = []` 2859 by PROVE_TAC [no_var_posns_in_var_posn_prefix] THEN 2860 FULL_SIMP_TAC (srw_ss()) [], 2861 2862 `bvp IN var_posns (strip_label t) /\ 2863 bvp' IN var_posns (strip_label t)` 2864 by PROVE_TAC [v_posns_SUBSET_var_posns] THEN 2865 `(bvp' = bvp) /\ (m' = m)` 2866 by PROVE_TAC [APPEND_var_posns] THEN 2867 NTAC 2 (POP_ASSUM SUBST_ALL_TAC) THEN 2868 `(vp = p1) /\ (l = [Rt]) \/ 2869 (?vpplus. (p1 = APPEND vp vpplus) /\ 2870 (l = APPEND vpplus [Rt]) /\ ~(vpplus = [])) \/ 2871 (?p1plus. (vp = APPEND p1 p1plus) /\ 2872 ([Rt] = APPEND p1plus l) /\ ~(p1plus = []))` 2873 by FULL_SIMP_TAC (srw_ss()) [APPEND_CASES] 2874 THENL [ 2875 Q.EXISTS_TAC `[]` THEN 2876 FULL_SIMP_TAC (srw_ss()) [n_posns_sub] THENL [ 2877 PROVE_TAC [lv_posns_n_posns, lv_posns_def], 2878 `vp' IN var_posns (strip_label t) /\ 2879 p1 IN var_posns (strip_label t)` 2880 by PROVE_TAC [v_posns_SUBSET_var_posns, 2881 lv_posns_def] THEN 2882 PROVE_TAC [no_var_posns_in_var_posn_prefix] 2883 ], 2884 Q.EXISTS_TAC `vpplus` THEN 2885 FULL_SIMP_TAC (srw_ss()) [n_posns_sub] THENL [ 2886 `APPEND vp (APPEND vpplus [Lt]) IN 2887 valid_posns (strip_label t)` 2888 by PROVE_TAC [n_posn_valid_posns, 2889 listTheory.APPEND_ASSOC] THEN 2890 PROVE_TAC [cant_be_deeper_than_var_posns, 2891 listTheory.APPEND_eq_NIL], 2892 Q_TAC SUFF_TAC `vpplus = np` THEN1 SRW_TAC [][] THEN 2893 `vp' IN var_posns (strip_label t)` 2894 by PROVE_TAC [v_posns_SUBSET_var_posns, 2895 lv_posns_def] THEN 2896 PROVE_TAC [APPEND_var_posns] 2897 ], 2898 `l = []` by (Cases_on `p1plus` THEN 2899 FULL_SIMP_TAC (srw_ss()) []) THEN 2900 POP_ASSUM SUBST_ALL_TAC THEN 2901 ASM_REWRITE_TAC [list_append_lemma, 2902 GSYM listTheory.APPEND_ASSOC, 2903 listTheory.APPEND_eq_NIL] THEN 2904 FULL_SIMP_TAC (srw_ss()) [lam_posns_subst] THENL [ 2905 FULL_SIMP_TAC (srw_ss()) [bv_posns_at_subst] THEN 2906 `APPEND bvp m IN valid_posns (strip_label t)` 2907 by PROVE_TAC [bv_posns_at_SUBSET_var_posns, 2908 var_posns_SUBSET_valid_posns] THEN 2909 `m = []` 2910 by PROVE_TAC [cant_be_deeper_than_var_posns] THEN 2911 FULL_SIMP_TAC (srw_ss()) [] THEN 2912 PROVE_TAC [v_posns_arent_bv_posns], 2913 FULL_SIMP_TAC (srw_ss()) [APPEND_CASES] THENL [ 2914 REPEAT VAR_EQ_TAC THEN 2915 PROVE_TAC [listTheory.NOT_NIL_CONS, 2916 no_var_posns_in_var_posn_prefix, 2917 v_posns_SUBSET_var_posns], 2918 `!x y z. ([x : redpos] = APPEND y z) <=> 2919 (y = [x]) /\ (z = []) \/ 2920 (y = []) /\ (z = [x])` 2921 by (REPEAT GEN_TAC THEN 2922 Cases_on `y` THEN SRW_TAC [][] THEN 2923 PROVE_TAC []) THEN 2924 FULL_SIMP_TAC (srw_ss()) [] THEN 2925 REPEAT VAR_EQ_TAC THEN 2926 FULL_SIMP_TAC (srw_ss()) [n_posns_sub] THEN 2927 POP_ASSUM (K ALL_TAC) THENL [ 2928 `APPEND p1 [Lt] IN lam_posns (strip_label t)` 2929 by PROVE_TAC [n_posns_lam_posns] THEN 2930 PROVE_TAC [lam_posns_var_posns, 2931 v_posns_SUBSET_var_posns], 2932 `vp IN var_posns (strip_label t)` 2933 by PROVE_TAC [lv_posns_def, 2934 v_posns_SUBSET_var_posns] THEN 2935 VAR_EQ_TAC THEN 2936 `APPEND vp (APPEND np [Lt]) IN 2937 var_posns (strip_label t)` 2938 by PROVE_TAC [listTheory.APPEND_ASSOC, 2939 v_posns_SUBSET_var_posns] THEN 2940 PROVE_TAC [listTheory.NOT_NIL_CONS, 2941 listTheory.APPEND_eq_NIL, 2942 no_var_posns_in_var_posn_prefix] 2943 ], 2944 REPEAT VAR_EQ_TAC THEN 2945 IMP_RES_TAC v_posns_SUBSET_var_posns THEN 2946 FULL_SIMP_TAC bool_ss 2947 [GSYM listTheory.APPEND_ASSOC] THEN 2948 PROVE_TAC [listTheory.APPEND_eq_NIL, 2949 listTheory.NOT_NIL_CONS, 2950 no_var_posns_in_var_posn_prefix] 2951 ] 2952 ] 2953 ] 2954 ]) THEN 2955 SELECT_ELIM_TAC THEN CONJ_TAC THEN1 2956 (ASM_SIMP_TAC bool_ss [GSYM listTheory.APPEND_ASSOC] THEN 2957 PROVE_TAC []) THEN 2958 SRW_TAC [][] THEN 2959 `vp' IN var_posns (strip_label t)` 2960 by PROVE_TAC [v_posns_SUBSET_var_posns] THEN 2961 `(vp' = vp) /\ (x = APPEND p' [Rt])` 2962 by PROVE_TAC [listTheory.APPEND_ASSOC, APPEND_var_posns] THEN 2963 NTAC 2 (POP_ASSUM SUBST_ALL_TAC) THEN 2964 SELECT_ELIM_TAC THEN CONJ_TAC THEN1 PROVE_TAC [] THEN 2965 SRW_TAC [][] THEN 2966 `vp' IN var_posns (strip_label t) /\ 2967 bvp IN var_posns (strip_label t)` 2968 by PROVE_TAC [v_posns_SUBSET_var_posns] THEN 2969 `(vp' = bvp) /\ (x = m)` by PROVE_TAC [APPEND_var_posns] THEN 2970 NTAC 2 (POP_ASSUM SUBST_ALL_TAC) THEN 2971 `APPEND p' [Lt] IN lam_posns (strip_label u)` 2972 by (FULL_SIMP_TAC (srw_ss()) [lam_posns_subst] THENL [ 2973 `APPEND vp (APPEND p' [Lt]) IN 2974 valid_posns (strip_label t)` 2975 by PROVE_TAC [lam_posns_SUBSET_valid_posns, 2976 listTheory.APPEND_ASSOC] THEN 2977 PROVE_TAC [cant_be_deeper_than_var_posns, 2978 listTheory.APPEND_eq_NIL, 2979 listTheory.NOT_NIL_CONS], 2980 PROVE_TAC [listTheory.APPEND_ASSOC, 2981 APPEND_var_posns, 2982 v_posns_SUBSET_var_posns] 2983 ]) THEN 2984 `bvp ++ m ��� 2985 IMAGE (APPEND vp) (bv_posns_at (APPEND p' [Lt]) (strip_label u))` 2986 by PROVE_TAC [bv_posns_at_subst2, listTheory.APPEND_ASSOC] THEN 2987 POP_ASSUM MP_TAC THEN 2988 ASM_SIMP_TAC (srw_ss() ++ SatisfySimps.SATISFY_ss) 2989 [APPEND_var_posns] THEN SRW_TAC [][] THEN 2990 `m ��� var_posns (strip_label u)` 2991 by PROVE_TAC [bv_posns_at_SUBSET_var_posns] THEN 2992 `w0 (Rt::m) = weight_at m (\p. w0 (Rt::p)) (strip_label u)` 2993 by SRW_TAC [][weight_at_var_posn] THEN 2994 SRW_TAC [][] THEN 2995 PROVE_TAC [decreasing_def], 2996 2997 ASM_SIMP_TAC (srw_ss()) [] THEN 2998 SELECT_ELIM_TAC THEN CONJ_TAC THEN1 PROVE_TAC [] THEN 2999 `p1 ��� n_posns n t` 3000 by (FULL_SIMP_TAC (srw_ss()) [n_posns_sub, lv_posns_def] THEN 3001 REPEAT VAR_EQ_TAC THEN 3002 `���m. p2 = vp' ++ np ++ [Lt] ++ m` 3003 by PROVE_TAC [bv_posns_at_prefix_posn, 3004 listTheory.APPEND_ASSOC] THEN 3005 `p2 = vp' ++ (np ++ ([Lt] ++ m))` 3006 by FULL_SIMP_TAC (srw_ss()) [] THEN 3007 PROVE_TAC []) THEN 3008 `p1 ++ [Lt] ��� lam_posns (strip_label t)` 3009 by PROVE_TAC [n_posns_lam_posns] THEN 3010 FULL_SIMP_TAC (srw_ss()) [bv_posns_at_subst] THEN 3011 Q.X_GEN_TAC `m` THEN 3012 DISCH_THEN (Q.X_CHOOSE_THEN `vp1` STRIP_ASSUME_TAC) THEN 3013 `(vp1 = vp) /\ (m = l)` 3014 by PROVE_TAC [APPEND_var_posns, v_posns_SUBSET_var_posns] THEN 3015 NTAC 2 (POP_ASSUM SUBST_ALL_TAC) THEN 3016 `(l = [])` by 3017 (`(vp = p1) /\ (l = [Rt]) \/ 3018 (?m. (vp = APPEND p1 m) /\ ([Rt] = APPEND m l) /\ ~(m = [])) \/ 3019 (?m. (p1 = APPEND vp m) /\ (l = APPEND m [Rt]) /\ ~(m = []))` 3020 by FULL_SIMP_TAC (srw_ss()) [APPEND_CASES] 3021 THENL [ 3022 `APPEND vp [Lt] IN valid_posns (strip_label t)` 3023 by PROVE_TAC [lam_posns_SUBSET_valid_posns] THEN 3024 PROVE_TAC [cant_be_deeper_than_var_posns, 3025 listTheory.NOT_NIL_CONS, 3026 v_posns_SUBSET_var_posns], 3027 Cases_on `m` THEN FULL_SIMP_TAC (srw_ss()) [], 3028 `?p. p2 = p1 ++ [Lt] ++ [In] ++ p` 3029 by PROVE_TAC [bv_posns_at_prefix_posn] THEN 3030 `p2 = vp ++ (m ++ ([Lt] ++ In::p))` 3031 by FULL_SIMP_TAC (srw_ss()) [] THEN 3032 PROVE_TAC [] 3033 ]) THEN 3034 POP_ASSUM SUBST_ALL_TAC THEN 3035 FULL_SIMP_TAC (srw_ss()) [weight_at_def, lterm_term_weight] THEN 3036 MATCH_MP_TAC arithmeticTheory.LESS_TRANS THEN 3037 Q.EXISTS_TAC 3038 `weight_at (APPEND p1 [Rt]) (\p. w0 (Lt::In::p)) (strip_label t)` 3039 THEN 3040 CONJ_TAC THENL [ 3041 FIRST_X_ASSUM MATCH_MP_TAC THEN 3042 ASM_SIMP_TAC (srw_ss()) [lv_posns_def], 3043 ALL_TAC 3044 ] THEN 3045 `p2 IN var_posns (strip_label t)` 3046 by PROVE_TAC [bv_posns_at_SUBSET_var_posns] THEN 3047 Q.ABBREV_TAC `fw = \p. w0 (Lt::In::p)` THEN 3048 `w0 (Lt::In::p2) = fw p2` by SRW_TAC [][Abbr`fw`] THEN 3049 ` _ = weight_at p2 fw (strip_label t)` 3050 by PROVE_TAC [weight_at_var_posn] THEN 3051 POP_ASSUM SUBST_ALL_TAC THEN 3052 PROVE_TAC [decreasing_def] 3053 ], 3054 3055 `p1 IN n_posns n t` 3056 by (FULL_SIMP_TAC (srw_ss()) [n_posns_sub, lv_posns_def] THEN 3057 REPEAT VAR_EQ_TAC THEN PROVE_TAC [listTheory.APPEND_ASSOC]) THEN 3058 `APPEND p1 [Lt] IN lam_posns ([strip_label u/v] (strip_label t)) /\ 3059 APPEND p1 [Lt] IN lam_posns (strip_label t)` 3060 by PROVE_TAC [n_posns_lam_posns] THEN 3061 `p2 IN var_posns ([strip_label u/v] (strip_label t))` 3062 by PROVE_TAC [bv_posns_at_SUBSET_var_posns] THEN 3063 FULL_SIMP_TAC (srw_ss()) [bv_posns_at_subst] THEN 3064 `p2 IN var_posns (strip_label t)` 3065 by PROVE_TAC [bv_posns_at_SUBSET_var_posns] THEN 3066 `p2 IN valid_posns (strip_label t) /\ 3067 p2 IN valid_posns ([strip_label u/v] (strip_label t))` 3068 by PROVE_TAC [var_posns_SUBSET_valid_posns] THEN 3069 ASM_SIMP_TAC (srw_ss()) [weight_at_subst] THEN 3070 `!vp l. vp IN v_posns v (strip_label t) /\ (APPEND vp l = p2) <=> F` 3071 by (REPEAT GEN_TAC THEN 3072 REWRITE_TAC [] THEN STRIP_TAC THEN 3073 `l = []` by PROVE_TAC [no_var_posns_in_var_posn_prefix, 3074 v_posns_SUBSET_var_posns] THEN 3075 FULL_SIMP_TAC (srw_ss()) [] THEN 3076 PROVE_TAC [v_posns_arent_bv_posns]) THEN 3077 ASM_SIMP_TAC (srw_ss()) [] THEN 3078 `{p' | (?p''. p' = APPEND p2 p'') /\ 3079 p' IN v_posns v (strip_label t)} = {}` 3080 by (SRW_TAC [][EXTENSION, GSYM IMP_DISJ_THM] THEN 3081 STRIP_TAC THEN 3082 `p'' = []` by PROVE_TAC [no_var_posns_in_var_posn_prefix, 3083 v_posns_SUBSET_var_posns] THEN 3084 FULL_SIMP_TAC (srw_ss()) [] THEN 3085 PROVE_TAC [v_posns_arent_bv_posns]) THEN 3086 ASM_SIMP_TAC (srw_ss()) [SUM_IMAGE_THM, 3087 arithmeticTheory.ADD_CLAUSES] THEN 3088 Q.ABBREV_TAC 3089 `vpset = {p' | (?p''. p' = APPEND (APPEND p1 [Rt]) p'') /\ 3090 p' IN v_posns v (strip_label t) }` THEN 3091 MATCH_MP_TAC arithmeticTheory.LESS_EQ_LESS_TRANS THEN 3092 Q.EXISTS_TAC 3093 `weight_at (APPEND p1 [Rt]) (\p. w0 (Lt::In::p)) (strip_label t)` 3094 THEN 3095 REVERSE CONJ_TAC THEN1 3096 (Q.ABBREV_TAC `fw = (\p. w0 (Lt::In::p))` THEN 3097 PROVE_TAC [decreasing_def]) THEN 3098 MATCH_MP_TAC (DECIDE``z <= y /\ y <= x ==> x - y + z <= x``) THEN 3099 CONJ_TAC THENL [ 3100 MATCH_MP_TAC CARD_SUM_IMAGE_LE THEN 3101 `vpset SUBSET v_posns v (strip_label t)` 3102 by SRW_TAC [][SUBSET_DEF, Abbr`vpset`] THEN 3103 `FINITE vpset` by PROVE_TAC [SUBSET_FINITE, 3104 v_posns_FINITE] THEN 3105 ASM_REWRITE_TAC [] THEN REPEAT STRIP_TAC THEN 3106 `e IN v_posns v (strip_label t) /\ e IN var_posns (strip_label t)` 3107 by PROVE_TAC [SUBSET_DEF, 3108 v_posns_SUBSET_var_posns] THEN 3109 Q.ABBREV_TAC `fw = \p. w0 (Lt::In::p)` THEN 3110 `fw e = weight_at e fw (strip_label t)` 3111 by PROVE_TAC [weight_at_var_posn] THEN 3112 ASM_SIMP_TAC (srw_ss()) [GSYM lterm_term_weight, lv_posns_def], 3113 Q.ABBREV_TAC `lfw = \p. w0 (Lt::In::p)` THEN 3114 `APPEND p1 [Rt] IN valid_posns (strip_label t)` 3115 by PROVE_TAC [n_posn_valid_posns] THEN 3116 ASM_SIMP_TAC (srw_ss()) [weight_at_SUM_IMAGE] THEN 3117 MATCH_MP_TAC SUM_IMAGE_SUBSET_LE THEN 3118 UNABBREV_ALL_TAC THEN 3119 SRW_TAC [][SUBSET_DEF] THENL [ 3120 MATCH_MP_TAC (MATCH_MP SUBSET_FINITE 3121 (Q.SPEC `strip_label t` 3122 var_posns_FINITE)) THEN 3123 SRW_TAC [][SUBSET_DEF], 3124 PROVE_TAC [], 3125 PROVE_TAC [v_posns_SUBSET_var_posns] 3126 ] 3127 ] 3128 ], 3129 3130 ASM_SIMP_TAC (srw_ss()) [wterm_ordering_def, lterm_term_weight] THEN 3131 `strip_label ([u/v] t) = [strip_label u/v] (strip_label t)` 3132 by SRW_TAC [][strip_label_subst] THEN 3133 ASM_SIMP_TAC (srw_ss()) [GSYM weight_at_def, weight_at_subst, 3134 strip_label_thm] THEN 3135 Cases_on `v_posns v (strip_label t) = {}` THENL [ 3136 SRW_TAC [][SUM_IMAGE_THM, 3137 arithmeticTheory.ADD_CLAUSES] THEN 3138 SRW_TAC [][weight_at_thm, term_weight_def, var_posns_thm, 3139 SUM_IMAGE_UNION] THEN 3140 `!s t. IMAGE (CONS Lt) s INTER IMAGE (CONS Rt) t = {}` 3141 by (SRW_TAC [][EXTENSION, EQ_IMP_THM] THEN 3142 Cases_on `x` THEN SRW_TAC [][] THEN Cases_on `h` THEN 3143 SRW_TAC [][]) THEN 3144 SRW_TAC [][SUM_IMAGE_THM, SUM_IMAGE_IMAGE, 3145 combinTheory.o_DEF] THEN 3146 `~(v IN FV t)` by PROVE_TAC [v_posns_FV_EQ, FV_strip_label] THEN 3147 SRW_TAC [][GSYM lvar_posns_def, GSYM lterm_weight_def] THEN 3148 METIS_TAC [nonzero_term_weight], 3149 ALL_TAC 3150 ] THEN 3151 COND_CASES_TAC THENL [ 3152 `strip_label t = VAR v` by PROVE_TAC [NIL_IN_v_posns] THEN 3153 ASM_SIMP_TAC (srw_ss()) [weight_at_thm, term_weight_thm] THEN 3154 Q_TAC SUFF_TAC `0 < w0 [Lt; In]` THEN1 SRW_TAC [ARITH_ss][] THEN 3155 `!p. p IN var_posns (strip_label t) ==> 0 < w0 (Lt::In::p)` 3156 by FULL_SIMP_TAC (srw_ss()) [nonzero_def, lvar_posns_def] THEN 3157 PROVE_TAC [v_posns_SUBSET_var_posns], 3158 ALL_TAC 3159 ] THEN 3160 ASM_SIMP_TAC (srw_ss()) [weight_at_thm, term_weight_thm] THEN 3161 MATCH_MP_TAC (DECIDE ``x < y ==> x < y + z``) THEN 3162 MATCH_MP_TAC (DECIDE ``z < y /\ y <= x ==> x - y + z < x``) THEN 3163 CONJ_TAC THENL [ 3164 MATCH_MP_TAC CARD_SUM_IMAGE_LT THEN 3165 FULL_SIMP_TAC (srw_ss() ++ SatisfySimps.SATISFY_ss) 3166 [lterm_term_weight, weight_at_var_posn, 3167 v_posns_SUBSET_var_posns, lv_posns_def], 3168 SIMP_TAC (srw_ss()) [term_weight_def] THEN 3169 MATCH_MP_TAC SUM_IMAGE_SUBSET_LE THEN 3170 SRW_TAC [SatisfySimps.SATISFY_ss] 3171 [v_posns_SUBSET_var_posns, SUBSET_DEF] 3172 ] 3173 ], 3174 3175 (* beta reduction on left of application *) 3176 SIMP_TAC (srw_ss() ++ ETA_ss) 3177 [update_weighing_def, strip_label_thm, 3178 decreasing_thm, nonzero_thm, wterm_ordering_def, 3179 lterm_term_weight, term_weight_thm], 3180 (* beta reduction on right of application *) 3181 SIMP_TAC (srw_ss() ++ ETA_ss) 3182 [update_weighing_def, strip_label_thm, 3183 decreasing_thm, nonzero_thm, wterm_ordering_def, 3184 lterm_term_weight, term_weight_thm], 3185 (* beta reduction under lambda abstraction *) 3186 SIMP_TAC (srw_ss() ++ ETA_ss) 3187 [update_weighing_def, strip_label_thm, 3188 decreasing_thm, nonzero_thm, wterm_ordering_def, 3189 lterm_term_weight, term_weight_thm], 3190 3191 (* beta reduction on RHS of marked redex *) 3192 SIMP_TAC (srw_ss() ++ ETA_ss) 3193 [update_weighing_def, strip_label_thm, 3194 decreasing_thm, nonzero_thm, wterm_ordering_def, 3195 lterm_term_weight, term_weight_thm, 3196 lv_posns_def] THEN 3197 REPEAT STRIP_TAC THEN 3198 MATCH_MP_TAC arithmeticTheory.LESS_EQ_LESS_TRANS THEN 3199 Q.EXISTS_TAC `term_weight (strip_label M) (\p. w0 (Rt::p))` THEN 3200 ASM_SIMP_TAC (srw_ss() ++ SatisfySimps.SATISFY_ss) [] THEN 3201 Q.ABBREV_TAC `wf = \p. w0 (Rt::p)` THEN 3202 PROVE_TAC [DECIDE ``x <= y <=> x < y \/ (x = y)``], 3203 3204 (* beta reduction within LHS of marked redex *) 3205 SIMP_TAC (srw_ss() ++ ETA_ss) 3206 [update_weighing_def, strip_label_thm, 3207 decreasing_thm, nonzero_thm, wterm_ordering_def, 3208 lterm_term_weight, term_weight_thm, lv_posns_def] THEN 3209 REPEAT GEN_TAC THEN STRIP_TAC THEN 3210 `r IN redex_posns (strip_label M)` by PROVE_TAC [beta0_redex_posn] THEN 3211 ASM_SIMP_TAC (srw_ss()) [update_weighing_vsubst] THEN 3212 REPEAT STRIP_TAC THEN 3213 `labelled_redn beta (strip_label M) r (strip_label N)` 3214 by PROVE_TAC [lrcc_RUNION, lrcc_labelled_redn] THEN 3215 IMP_RES_THEN (IMP_RES_THEN (Q.X_CHOOSE_THEN `p1` STRIP_ASSUME_TAC)) 3216 FV_weights_update_weighing THEN 3217 ASM_SIMP_TAC (srw_ss()) [] 3218 ]); 3219 3220 3221val WF_path_finite0 = prove( 3222 ``!R P L. WF R /\ (!x r y. P x /\ L x r y ==> P y /\ R y x) ==> 3223 !x p. (x = first p) /\ okpath L p /\ P (first p) ==> 3224 finite p``, 3225 REPEAT GEN_TAC THEN STRIP_TAC THEN 3226 FIRST_ASSUM (HO_MATCH_MP_TAC o 3227 MATCH_MP relationTheory.WF_INDUCTION_THM) THEN 3228 REPEAT STRIP_TAC THEN 3229 Q.SPEC_THEN `p` (REPEAT_TCL STRIP_THM_THEN SUBST_ALL_TAC) 3230 pathTheory.path_cases THEN 3231 FULL_SIMP_TAC (srw_ss()) [] THEN PROVE_TAC []); 3232 3233val WF_path_finite = save_thm("WF_path_finite", 3234 SIMP_RULE bool_ss [] WF_path_finite0); 3235 3236 3237val path_case_def = 3238 Define`path_case f g p = if is_stopped p then f (first p) 3239 else g (first p) (first_label p) (tail p)`; 3240 3241val path_case_thm = store_thm( 3242 "path_case_thm", 3243 ``!f g. (!x. path_case f g (stopped_at x) = f x) /\ 3244 (!x r y. path_case f g (pcons x r y) = g x r y)``, 3245 SRW_TAC [][path_case_def]); 3246 3247 3248(* the lift_weighing function computes (among other things) the weighing 3249 asserted to exist by Barendregt's Lemma 11.2.19 *) 3250val lift_weighing_t = 3251 ``\w_sigma. 3252 path_case (\x. ((x, FST w_sigma), NONE)) 3253 (\x r y. ((x, FST w_sigma), 3254 SOME (r, 3255 (update_weighing (strip_label x) r 3256 (FST w_sigma), y)))) 3257 (SND w_sigma)`` 3258 3259val lift_weighing_def = new_specification( 3260 "lift_weighing_def", ["lift_weighing"], 3261 prove(``?f. (!w x. f w (stopped_at x) = stopped_at (x, w)) /\ 3262 (!w x r y. f w (pcons x r y) = 3263 pcons (x, w) r 3264 (f (update_weighing (strip_label x) r w) y))``, 3265 STRIP_ASSUME_TAC (ISPEC lift_weighing_t pathTheory.path_Axiom) THEN 3266 Q.EXISTS_TAC `\w p. g (w, p)` THEN 3267 SIMP_TAC (srw_ss()) [] THEN 3268 REPEAT STRIP_TAC THEN 3269 POP_ASSUM (fn th => CONV_TAC (LAND_CONV (ONCE_REWRITE_CONV [th]))) THEN 3270 SRW_TAC [][path_case_thm])); 3271 3272val pstrip_weights_def = Define` 3273 pstrip_weights = pmap (FST : lterm # (redpos list -> num) -> lterm) I 3274`; 3275 3276val pstrip_lift_weighing = store_thm( 3277 "pstrip_lift_weighing", 3278 ``!p w. pstrip_weights (lift_weighing w p) = p``, 3279 REPEAT GEN_TAC THEN 3280 ONCE_REWRITE_TAC [pathTheory.path_bisimulation] THEN 3281 Q.EXISTS_TAC `\x y. ?w. x = pstrip_weights (lift_weighing w y)` THEN 3282 SRW_TAC [][] THENL [ 3283 PROVE_TAC [], 3284 Q.ISPEC_THEN `q2` STRUCT_CASES_TAC pathTheory.path_cases THEN 3285 SRW_TAC [][lift_weighing_def, pstrip_weights_def, pathTheory.pmap_thm] THEN 3286 PROVE_TAC [] 3287 ]); 3288 3289val first_lift_weighing = store_thm( 3290 "first_lift_weighing", 3291 ``!p w. first (lift_weighing w p) = (first p, w)``, 3292 REPEAT GEN_TAC THEN 3293 Q.ISPEC_THEN `p` STRUCT_CASES_TAC path_cases THEN 3294 SRW_TAC [][lift_weighing_def]); 3295 3296val finite_lift_weighing = store_thm( 3297 "finite_lift_weighing", 3298 ``!p w : redpos list -> num. finite (lift_weighing w p) = finite p``, 3299 Q_TAC SUFF_TAC 3300 `(!p : (lterm, redpos list) path. 3301 finite p ==> 3302 !w : redpos list -> num. finite (lift_weighing w p)) /\ 3303 (!p. finite p ==> 3304 !(w : redpos list -> num) (p' : (lterm, redpos list) path). 3305 (p = lift_weighing w p') ==> finite p')` 3306 THEN1 PROVE_TAC [] THEN 3307 CONJ_TAC THEN HO_MATCH_MP_TAC finite_path_ind THEN 3308 SIMP_TAC (srw_ss()) [lift_weighing_def] THEN CONJ_TAC THEN 3309 REPEAT GEN_TAC THENL [ ALL_TAC, STRIP_TAC THEN REPEAT GEN_TAC] THEN 3310 Q.ISPEC_THEN `p'` STRUCT_CASES_TAC path_cases THEN 3311 SRW_TAC [][lift_weighing_def] THEN PROVE_TAC []); 3312 3313val beta0_weighted_reduction_lift_weighing = store_thm( 3314 "beta0_weighted_reduction_lift_weighing", 3315 ``!p. okpath (lrcc beta0) p ==> 3316 !w. okpath weighted_reduction (lift_weighing w p)``, 3317 Q_TAC SUFF_TAC 3318 `!p2. (?w p. (p2 = lift_weighing w p) /\ okpath (lrcc beta0) p) ==> 3319 okpath weighted_reduction p2` THEN1 PROVE_TAC [] THEN 3320 HO_MATCH_MP_TAC pathTheory.okpath_co_ind THEN REPEAT GEN_TAC THEN 3321 STRIP_TAC THEN 3322 Q.ISPEC_THEN `p` FULL_STRUCT_CASES_TAC path_cases THEN 3323 FULL_SIMP_TAC (srw_ss()) [lift_weighing_def, first_lift_weighing] THEN 3324 CONJ_TAC THENL [ 3325 SRW_TAC [][weighted_reduction_def], 3326 PROVE_TAC [] 3327 ]); 3328 3329val beta0_paths_finite = store_thm( 3330 "beta0_paths_finite", 3331 ``!p. okpath (lrcc beta0) p ==> finite p``, 3332 REPEAT STRIP_TAC THEN 3333 Q.SPEC_THEN `first p` STRIP_ASSUME_TAC decreasing_weights_exist THEN 3334 `okpath weighted_reduction (lift_weighing w p)` 3335 by PROVE_TAC [beta0_weighted_reduction_lift_weighing] THEN 3336 Q_TAC SUFF_TAC `finite (lift_weighing w p)` 3337 THEN1 PROVE_TAC [finite_lift_weighing] THEN 3338 MATCH_MP_TAC 3339 (SIMP_RULE (srw_ss() ++ DNF_ss) [AND_IMP_INTRO] WF_path_finite) THEN 3340 Q.EXISTS_TAC `wterm_ordering` THEN 3341 REWRITE_TAC [WF_wterm_ordering] THEN 3342 Q.EXISTS_TAC `\tw. decreasing (FST tw) (SND tw) /\ 3343 nonzero (FST tw) (SND tw)` THEN 3344 Q.EXISTS_TAC `weighted_reduction` THEN 3345 ASM_SIMP_TAC (srw_ss()) [pairTheory.FORALL_PROD, first_lift_weighing] THEN 3346 PROVE_TAC [weighted_reduction_reduces_ordering]); 3347 3348val lrcc_lcompat_closure = store_thm( 3349 "lrcc_lcompat_closure", 3350 ``!R x y. lcompat_closure R x y = ?r. lrcc R x r y``, 3351 GEN_TAC THEN 3352 Q_TAC SUFF_TAC `(!x y. lcompat_closure R x y ==> ?r. lrcc R x r y)` 3353 THEN1 PROVE_TAC [lrcc_lcc] THEN 3354 HO_MATCH_MP_TAC lcompat_closure_ind THEN SRW_TAC [][] THEN 3355 PROVE_TAC [lrcc_rules]); 3356 3357val inv_lemma = prove( 3358 ``inv R = \x y. R y x``, 3359 SRW_TAC [][FUN_EQ_THM, relationTheory.inv_DEF]) 3360 3361val TC_inv = GSYM relationTheory.inv_TC 3362 3363val prop11_2_20 = store_thm( 3364 "prop11_2_20", 3365 ``WF (inv (lcompat_closure beta0))``, 3366 REWRITE_TAC [lrcc_lcompat_closure, GSYM pathTheory.SN_def, inv_lemma, 3367 pathTheory.SN_finite_paths_EQ, beta0_paths_finite]); 3368 3369val finite_lift_path = store_thm( 3370 "finite_lift_path", 3371 ``!M p. finite (lift_path M p) = finite p``, 3372 Q_TAC SUFF_TAC 3373 `(!p. finite p ==> !M : lterm. finite (lift_path M p)) /\ 3374 (!p'. finite p' ==> 3375 !M : lterm p. (p' = lift_path M p) ==> finite p)` 3376 THEN1 PROVE_TAC [] THEN CONJ_TAC THEN 3377 HO_MATCH_MP_TAC finite_path_ind THENL [ 3378 SRW_TAC [][lift_path_def], 3379 ALL_TAC 3380 ] THEN 3381 Q_TAC SUFF_TAC 3382 `(!(x : lterm) M p. (stopped_at x = lift_path M p) ==> finite p) /\ 3383 (!(x : lterm) r p. finite p /\ 3384 (!M q. (p = lift_path M q) ==> finite q) ==> 3385 !M q. (pcons x r p = lift_path M q) ==> finite q)` THEN1 3386 PROVE_TAC [] THEN 3387 REPEAT STRIP_TAC THENL [ 3388 Q.ISPEC_THEN `p` (REPEAT_TCL STRIP_THM_THEN SUBST_ALL_TAC) path_cases, 3389 Q.ISPEC_THEN `q` (REPEAT_TCL STRIP_THM_THEN SUBST_ALL_TAC) path_cases 3390 ] THEN FULL_SIMP_TAC (srw_ss()) [lift_path_def] THEN PROVE_TAC []); 3391 3392val theorem11_2_21 = store_thm( 3393 "theorem11_2_21", 3394 ``!M p. p IN development M ==> finite p``, 3395 REWRITE_TAC [term_development_thm] THEN 3396 PROVE_TAC [lemma11_2_12, beta0_paths_finite, finite_lift_path]); 3397 3398val FD = save_thm("FD", theorem11_2_21) 3399 3400val extend_path_maximally = store_thm( 3401 "extend_path_maximally", 3402 ``!R. SN R ==> 3403 !x. ?p. finite p /\ (first p = x) /\ okpath R p /\ 3404 !r y. ~R (last p) r y``, 3405 REWRITE_TAC [SN_def] THEN GEN_TAC THEN 3406 DISCH_THEN (HO_MATCH_MP_TAC o MATCH_MP relationTheory.WF_INDUCTION_THM) THEN 3407 SRW_TAC [][] THEN 3408 Cases_on `?r y. R x r y` THENL [ 3409 POP_ASSUM STRIP_ASSUME_TAC THEN 3410 RES_TAC THEN Q.EXISTS_TAC `pcons x r p` THEN 3411 SRW_TAC [][], 3412 Q.EXISTS_TAC `stopped_at x` THEN 3413 FULL_SIMP_TAC (srw_ss()) [] 3414 ]); 3415 3416val finite_strip_path_label = store_thm ( 3417 "finite_strip_path_label", 3418 ``!p. finite (strip_path_label p) = finite p``, 3419 SIMP_TAC (srw_ss()) [EQ_IMP_THM, FORALL_AND_THM] THEN CONJ_TAC THENL [ 3420 Q_TAC SUFF_TAC 3421 `!q. finite q ==> !p. (q = strip_path_label p) ==> finite p` 3422 THEN1 PROVE_TAC [] THEN 3423 HO_MATCH_MP_TAC finite_path_ind THEN REPEAT STRIP_TAC THEN 3424 Q.ISPEC_THEN `p` (REPEAT_TCL STRIP_THM_THEN SUBST_ALL_TAC) path_cases THEN 3425 FULL_SIMP_TAC (srw_ss()) [strip_path_label_thm], 3426 HO_MATCH_MP_TAC finite_path_ind THEN 3427 SRW_TAC [][strip_path_label_thm] 3428 ]); 3429 3430val okpath_RUNION = store_thm( 3431 "okpath_RUNION", 3432 ``!R1 R2 p. okpath (lrcc R1) p ==> okpath (lrcc (R1 RUNION R2)) p``, 3433 GEN_TAC THEN GEN_TAC THEN HO_MATCH_MP_TAC okpath_co_ind THEN 3434 SRW_TAC [][lrcc_RUNION]); 3435 3436val lift_path_plink = store_thm( 3437 "lift_path_plink", 3438 ``!p1 M p2. 3439 finite p1 /\ (last p1 = first p2) ==> 3440 (lift_path M (plink p1 p2) = 3441 plink (lift_path M p1) (lift_path (last (lift_path M p1)) p2))``, 3442 SIMP_TAC (srw_ss()) [GSYM AND_IMP_INTRO, RIGHT_FORALL_IMP_THM] THEN 3443 HO_MATCH_MP_TAC finite_path_ind THEN 3444 SRW_TAC [][lift_path_def, first_plink]); 3445 3446val lift_path_strip_path_label = store_thm( 3447 "lift_path_strip_path_label", 3448 ``!p. okpath (lrcc (beta0 RUNION beta1)) p ==> 3449 (lift_path (first p) (strip_path_label p) = p)``, 3450 REPEAT STRIP_TAC THEN ONCE_REWRITE_TAC [path_bisimulation] THEN 3451 Q.EXISTS_TAC `\x y. okpath (lrcc (beta0 RUNION beta1)) y /\ 3452 (x = lift_path (first y) (strip_path_label y)) ` THEN 3453 ASM_SIMP_TAC (srw_ss()) [] THEN 3454 GEN_TAC THEN 3455 Q.ISPEC_THEN `q2` STRUCT_CASES_TAC path_cases THEN 3456 SRW_TAC [][lift_path_def, strip_path_label_thm, first_strip_path_label] THEN 3457 Q_TAC SUFF_TAC `lift_redn x r (strip_label (first q)) = first q` 3458 THEN1 SRW_TAC [][] THEN 3459 IMP_RES_TAC lrcc_labelled_redn THEN 3460 IMP_RES_TAC lift_redn_def THEN 3461 PROVE_TAC [lrcc_det]); 3462 3463val n_posns_beta0 = store_thm( 3464 "n_posns_beta0", 3465 ``!M p n. p IN n_posns n M ==> ?N. lrcc beta0 M p N``, 3466 HO_MATCH_MP_TAC simple_lterm_induction THEN 3467 REVERSE (SRW_TAC [][n_posns_def]) THEN1 3468 (FULL_SIMP_TAC (srw_ss() ++ COND_elim_ss) [] THEN RES_TAC THEN 3469 ONCE_REWRITE_TAC [lrcc_cases] THEN SRW_TAC [][beta0_def] THEN 3470 PROVE_TAC []) THEN 3471 PROVE_TAC [lrcc_rules, l14a]); 3472 3473val corollary11_2_22i = store_thm( 3474 "corollary11_2_22i", 3475 ``!M ps p. p IN development M ps ==> 3476 ?p'. (last p = first p') /\ 3477 (plink p p') IN complete_development M ps``, 3478 REWRITE_TAC [lemma11_2_12, complete_development_thm] THEN 3479 REPEAT STRIP_TAC THEN 3480 `SN (lrcc beta0)` by PROVE_TAC [SN_finite_paths_EQ, beta0_paths_finite] THEN 3481 Q.ABBREV_TAC `p' = lift_path (nlabel 0 (first p) ps) p` THEN 3482 `?p2. finite p2 /\ (first p2 = last p') /\ okpath (lrcc beta0) p2 /\ 3483 !r y. ~lrcc beta0 (last p2) r y` 3484 by PROVE_TAC [extend_path_maximally] THEN 3485 `finite p /\ finite p'` 3486 by PROVE_TAC [finite_lift_path, beta0_paths_finite] THEN 3487 `last p = strip_label (last p')` 3488 by PROVE_TAC [strip_label_nlabel, residuals_def] THEN 3489 Q.EXISTS_TAC `strip_path_label p2` THEN 3490 ASM_SIMP_TAC (srw_ss()) [first_strip_path_label, first_plink, 3491 finite_strip_path_label] THEN 3492 `last p = first (strip_path_label p2)` 3493 by PROVE_TAC [first_strip_path_label] THEN 3494 `okpath (labelled_redn beta) (strip_path_label p2)` 3495 by PROVE_TAC [okpath_RUNION, lemma11_2_1] THEN 3496 `okpath (lrcc (beta0 RUNION beta1)) p2` by PROVE_TAC [okpath_RUNION] THEN 3497 REPEAT CONJ_TAC THENL [ 3498 ASM_SIMP_TAC (srw_ss()) [lift_path_plink], 3499 ASM_SIMP_TAC (srw_ss()) [lift_path_plink, first_lift_path] THEN 3500 Q_TAC SUFF_TAC `lift_path (last p') (strip_path_label p2) = p2` 3501 THEN1 SRW_TAC [][] THEN 3502 PROVE_TAC [lift_path_strip_path_label], 3503 `finite (strip_path_label p2)` by SRW_TAC [][finite_strip_path_label] THEN 3504 ASM_SIMP_TAC (srw_ss()) [lemma11_2_6] THEN 3505 Q.SPEC_THEN `strip_path_label p2` MP_TAC residuals_def THEN 3506 ASM_REWRITE_TAC [] THEN 3507 DISCH_THEN (Q.SPEC_THEN `residuals p ps` STRIP_ASSUME_TAC) THEN 3508 `nlabel 0 (first (strip_path_label p2)) (residuals p ps) = first p2` 3509 by (ASM_SIMP_TAC (srw_ss()) [labelled_term_component_equality, 3510 strip_label_nlabel, 3511 first_strip_path_label] THEN 3512 Q.SPEC_THEN `p` MP_TAC residuals_def THEN 3513 ASM_REWRITE_TAC [first_strip_path_label] THEN 3514 DISCH_THEN (Q.SPEC_THEN `ps` STRIP_ASSUME_TAC o GSYM) THEN 3515 ASM_SIMP_TAC bool_ss []) THEN 3516 POP_ASSUM SUBST_ALL_TAC THEN 3517 Q.PAT_X_ASSUM `last x = y` MP_TAC THEN 3518 ASM_SIMP_TAC (srw_ss()) [lift_path_strip_path_label] THEN 3519 DISCH_THEN (MP_TAC o Q.AP_TERM `n_posns 0`) THEN 3520 POP_ASSUM (ASSUME_TAC o 3521 REWRITE_RULE [SUBSET_INTER_ABSORPTION]) THEN 3522 ASM_SIMP_TAC (srw_ss()) [n_posns_nlabel] THEN 3523 DISCH_THEN (fn th => REWRITE_TAC [SYM th]) THEN 3524 SPOSE_NOT_THEN STRIP_ASSUME_TAC THEN 3525 `?p. p IN n_posns 0 (last p2)` 3526 by PROVE_TAC [SET_CASES, IN_INSERT] THEN 3527 PROVE_TAC [n_posns_beta0] 3528 ]); 3529 3530(* corollary11_2_22ii requires a proof of K\"onig's lemma *) 3531 3532val RTC_lcc_rules = store_thm( 3533 "RTC_lcc_rules", 3534 ``!x y. RTC (lcompat_closure R) x y ==> 3535 (!z. RTC (lcompat_closure R) (x @@ z) (y @@ z) /\ 3536 RTC (lcompat_closure R) (z @@ x) (z @@ y)) /\ 3537 !v. RTC (lcompat_closure R) (LAM v x) (LAM v y) /\ 3538 !n w. RTC (lcompat_closure R) (LAMi n v w x) (LAMi n v w y) /\ 3539 RTC (lcompat_closure R) (LAMi n v x w) (LAMi n v y w)``, 3540 HO_MATCH_MP_TAC relationTheory.RTC_INDUCT THEN 3541 PROVE_TAC [relationTheory.RTC_RULES, lcompat_closure_rules]); 3542 3543val lcc_cosubstitutive = store_thm( 3544 "lcc_cosubstitutive", 3545 ``!P M N v. lcompat_closure R M N ==> 3546 RTC (lcompat_closure R) ([M/v] P) ([N/v] P)``, 3547 REPEAT GEN_TAC THEN Q.ID_SPEC_TAC `P` THEN 3548 HO_MATCH_MP_TAC lterm_bvc_induction THEN 3549 Q.EXISTS_TAC `v INSERT FV M UNION FV N` THEN SRW_TAC [][lSUB_VAR] THEN 3550 PROVE_TAC [relationTheory.RTC_RULES, relationTheory.RTC_RTC, 3551 RTC_lcc_rules]); 3552 3553val strong_lcc_ind = 3554 IndDefLib.derive_strong_induction 3555 (lcompat_closure_rules, lcompat_closure_ind) 3556 3557val beta0_LAMi = store_thm( 3558 "beta0_LAMi", 3559 ``beta0 (LAMi n v M N) P = (P = [N/v] M)``, 3560 SRW_TAC [][beta0_def, EQ_IMP_THM, lLAMi_eq_thm] THEN 3561 SRW_TAC [][fresh_ltpm_subst, l15a] THEN 3562 PROVE_TAC []); 3563 3564val lcc_b0_tpm_imp = store_thm( 3565 "lcc_b0_tpm_imp", 3566 ``!M N. lcompat_closure beta0 M N ==> 3567 !p. lcompat_closure beta0 (ltpm p M) (ltpm p N)``, 3568 HO_MATCH_MP_TAC lcompat_closure_ind THEN 3569 SRW_TAC [][lcompat_closure_rules, beta0_def] THEN 3570 SRW_TAC [][ltpm_subst] THEN METIS_TAC [lcompat_closure_rules, beta0_def]); 3571 3572val lcc_beta0_LAMi = store_thm( 3573 "lcc_beta0_LAMi", 3574 ``lcompat_closure beta0 (LAMi n v M N) P <=> 3575 (P = [N/v] M) \/ 3576 (?P0. lcompat_closure beta0 M P0 /\ (P = LAMi n v P0 N)) \/ 3577 (?P0. lcompat_closure beta0 N P0 /\ (P = LAMi n v M P0))``, 3578 CONV_TAC (LAND_CONV (ONCE_REWRITE_CONV [lcompat_closure_cases])) THEN 3579 SRW_TAC [][EQ_IMP_THM, beta0_LAMi] THENL [ 3580 DISJ2_TAC THEN DISJ1_TAC THEN 3581 FULL_SIMP_TAC (srw_ss()) [lLAMi_eq_thm] THEN 3582 Q.EXISTS_TAC `ltpm [(v,v')] y` THEN 3583 SRW_TAC [][pmact_flip_args, lcc_b0_tpm_imp] THEN 3584 PROVE_TAC [lcc_beta_FV, lrcc_RUNION, lrcc_lcompat_closure], 3585 DISJ2_TAC THEN DISJ2_TAC THEN 3586 FULL_SIMP_TAC (srw_ss()) [lLAMi_eq_thm, pmact_flip_args], 3587 PROVE_TAC [], 3588 PROVE_TAC [] 3589 ]); 3590 3591val lcc_beta0_app = store_thm( 3592 "lcc_beta0_app", 3593 ``!M N P. lcompat_closure beta0 (M @@ N) P <=> 3594 (?P0. lcompat_closure beta0 M P0 /\ (P = P0 @@ N)) \/ 3595 (?P0. lcompat_closure beta0 N P0 /\ (P = M @@ P0))``, 3596 REPEAT GEN_TAC THEN 3597 CONV_TAC (LAND_CONV (ONCE_REWRITE_CONV [lcompat_closure_cases])) THEN 3598 SRW_TAC [][beta0_def, EQ_IMP_THM] THEN PROVE_TAC []); 3599 3600val lcc_beta0_LAM = store_thm( 3601 "lcc_beta0_LAM", 3602 ``!v M P. lcompat_closure beta0 (LAM v M) P <=> 3603 ?P0. lcompat_closure beta0 M P0 /\ (P = LAM v P0)``, 3604 REPEAT GEN_TAC THEN 3605 CONV_TAC (LAND_CONV (ONCE_REWRITE_CONV [lcompat_closure_cases])) THEN 3606 SRW_TAC [][beta0_def, EQ_IMP_THM] THENL [ 3607 FULL_SIMP_TAC (srw_ss()) [lLAM_eq_thm] THEN 3608 Q.EXISTS_TAC `ltpm [(v,v')] y` THEN 3609 SRW_TAC [][lcc_b0_tpm_imp, pmact_flip_args] THEN 3610 PROVE_TAC [lcc_beta_FV, lrcc_RUNION, lrcc_lcompat_closure], 3611 3612 PROVE_TAC [] 3613 ]); 3614 3615 3616val beta0_WCR = store_thm( 3617 "beta0_WCR", 3618 ``weak_diamond (lcompat_closure beta0)``, 3619 SIMP_TAC (srw_ss()) [weak_diamond_def, RIGHT_FORALL_IMP_THM, 3620 GSYM AND_IMP_INTRO] THEN 3621 HO_MATCH_MP_TAC strong_lcc_ind THEN REPEAT STRIP_TAC THENL [ 3622 (* beta0 (base) case *) 3623 FULL_SIMP_TAC (srw_ss()) [beta0_def] THEN 3624 REPEAT VAR_EQ_TAC THEN 3625 FULL_SIMP_TAC (srw_ss()) [lcc_beta0_LAMi] THENL [ 3626 PROVE_TAC [relationTheory.RTC_RULES], 3627 `beta0 (LAMi n v P0 u) ([u/v] P0)` by PROVE_TAC [beta0_def] THEN 3628 `lcompat_closure beta0 (LAMi n v P0 u) ([u/v] P0)` 3629 by PROVE_TAC [lcompat_closure_rules] THEN 3630 `RTC (lcompat_closure beta0) (LAMi n v P0 u) ([u/v] P0)` 3631 by PROVE_TAC [relationTheory.RTC_RULES] THEN 3632 Q.EXISTS_TAC `([u/v] P0)` THEN 3633 PROVE_TAC [lrcc_lcompat_closure, lrcc_lsubstitutive, 3634 beta0_lsubstitutive, relationTheory.RTC_RULES], 3635 `beta0 (LAMi n v t P0) ([P0/v] t)` by PROVE_TAC [beta0_def] THEN 3636 `lcompat_closure beta0 (LAMi n v t P0) ([P0/v] t)` 3637 by PROVE_TAC [lcompat_closure_rules] THEN 3638 Q.EXISTS_TAC `[P0/v] t` THEN 3639 PROVE_TAC [lcc_cosubstitutive, relationTheory.RTC_RULES] 3640 ], 3641 3642 (* app right case *) 3643 FULL_SIMP_TAC (srw_ss()) [lcc_beta0_app] THEN 3644 PROVE_TAC [relationTheory.RTC_RULES, RTC_lcc_rules], 3645 3646 (* app left case *) 3647 FULL_SIMP_TAC (srw_ss()) [lcc_beta0_app] THEN 3648 PROVE_TAC [relationTheory.RTC_RULES, RTC_lcc_rules], 3649 3650 (* lam case *) 3651 FULL_SIMP_TAC (srw_ss()) [lcc_beta0_LAM] THEN 3652 PROVE_TAC [RTC_lcc_rules], 3653 3654 (* LAMi body moves case *) 3655 REPEAT (POP_ASSUM MP_TAC) THEN 3656 Q_TAC SUFF_TAC 3657 `!x y z n v z'. 3658 lcompat_closure beta0 x y /\ 3659 (!z. lcompat_closure beta0 x z ==> 3660 ?u. RTC (lcompat_closure beta0) y u /\ 3661 RTC (lcompat_closure beta0) z u) /\ 3662 lcompat_closure beta0 (LAMi n v x z) z' ==> 3663 ?u. RTC (lcompat_closure beta0) (LAMi n v y z) u /\ 3664 RTC (lcompat_closure beta0) z' u` THEN1 METIS_TAC [] THEN 3665 SRW_TAC [][lcc_beta0_LAMi] THENL [ 3666 Q.EXISTS_TAC `[z/v] y` THEN 3667 `beta0 (LAMi n v y z) ([z/v] y)` by PROVE_TAC [beta0_def] THEN 3668 `lcompat_closure beta0 (LAMi n v y z) ([z/v] y)` 3669 by PROVE_TAC [lcompat_closure_rules] THEN 3670 PROVE_TAC [lrcc_lcompat_closure, lrcc_lsubstitutive, 3671 beta0_lsubstitutive, relationTheory.RTC_RULES], 3672 PROVE_TAC [RTC_lcc_rules], 3673 PROVE_TAC [RTC_lcc_rules, relationTheory.RTC_RULES] 3674 ], 3675 3676 (* LAMi argument moves *) 3677 REPEAT (POP_ASSUM MP_TAC) THEN 3678 Q_TAC SUFF_TAC 3679 `!x y z n v z'. 3680 lcompat_closure beta0 x y /\ 3681 (!z. lcompat_closure beta0 x z ==> 3682 ?u. RTC (lcompat_closure beta0) y u /\ 3683 RTC (lcompat_closure beta0) z u) /\ 3684 lcompat_closure beta0 (LAMi n v z x) z' ==> 3685 ?u. RTC (lcompat_closure beta0) (LAMi n v z y) u /\ 3686 RTC (lcompat_closure beta0) z' u` THEN1 METIS_TAC [] THEN 3687 SRW_TAC [][lcc_beta0_LAMi] THENL [ 3688 Q.EXISTS_TAC `[y/v] z` THEN 3689 `beta0 (LAMi n v z y) ([y/v] z)` by PROVE_TAC [beta0_def] THEN 3690 `lcompat_closure beta0 (LAMi n v z y) ([y/v] z)` 3691 by PROVE_TAC [lcompat_closure_rules] THEN 3692 PROVE_TAC [lcc_cosubstitutive, relationTheory.RTC_RULES], 3693 PROVE_TAC [RTC_lcc_rules, relationTheory.RTC_RULES], 3694 PROVE_TAC [RTC_lcc_rules] 3695 ] 3696 ]); 3697 3698val newman_recast = store_thm( 3699 "newman_recast", 3700 ``WF (inv R) /\ weak_diamond R ==> diamond_property (RTC R)``, 3701 SRW_TAC [][relationTheory.Newmans_lemma, 3702 GSYM relationTheory.CR_def, 3703 GSYM relationTheory.SN_def]); 3704 3705val CR_beta0 = store_thm( 3706 "CR_beta0", 3707 ``diamond_property (RTC (lcompat_closure beta0))``, 3708 PROVE_TAC [newman_recast, prop11_2_20, beta0_WCR]); 3709 3710val okpath_RTC = store_thm( 3711 "okpath_RTC", 3712 ``!R p. 3713 okpath R p /\ finite p ==> 3714 RTC (\x y. ?l. R x l y) (first p) (last p)``, 3715 GEN_TAC THEN HO_MATCH_MP_TAC finite_okpath_ind THEN 3716 SRW_TAC [][relationTheory.RTC_RULES] THEN 3717 Q.SPEC_THEN `RR` (MATCH_MP_TAC o CONJUNCT2) relationTheory.RTC_RULES THEN 3718 PROVE_TAC []); 3719 3720val unique_nforms = store_thm( 3721 "unique_nforms", 3722 ``!R x y z. diamond_property (RTC R) /\ 3723 RTC R x y /\ RTC R x z /\ (!u. ~R y u) /\ (!u. ~R z u) ==> 3724 (y = z)``, 3725 REPEAT STRIP_TAC THEN 3726 `?w. RTC R y w /\ RTC R z w` by PROVE_TAC [diamond_property_def] THEN 3727 PROVE_TAC [relationTheory.RTC_CASES1]); 3728 3729val beta0_n_posns = store_thm( 3730 "beta0_n_posns", 3731 ``!M p N. lrcc beta0 M p N ==> ?n. p IN n_posns n M``, 3732 HO_MATCH_MP_TAC lrcc_ind THEN 3733 SRW_TAC [][n_posns_def, beta0_def] THENL [ 3734 SRW_TAC [COND_elim_ss][n_posns_def], 3735 PROVE_TAC [], 3736 PROVE_TAC [] 3737 ]); 3738 3739 3740(* definitions 11_2_26 *) 3741val SN_beta0 = save_thm( 3742 "SN_beta0", 3743 REWRITE_RULE [lrcc_lcompat_closure, inv_lemma, GSYM SN_def] prop11_2_20); 3744 3745val cpl_uexists = store_thm( 3746 "cpl_uexists", 3747 ``!M'. ?!N'. RTC (lcompat_closure beta0) M' N' /\ 3748 !N''. ~ lcompat_closure beta0 N' N''``, 3749 SRW_TAC [][EXISTS_UNIQUE_THM] THENL [ 3750 Q.SPEC_THEN `M'` STRIP_ASSUME_TAC 3751 (MATCH_MP extend_path_maximally SN_beta0) THEN 3752 Q.EXISTS_TAC `last p` THEN 3753 IMP_RES_TAC okpath_RTC THEN 3754 FULL_SIMP_TAC (srw_ss()) [lrcc_lcompat_closure] THEN 3755 FULL_SIMP_TAC (srw_ss() ++ ETA_ss) [GSYM lrcc_lcompat_closure] THEN 3756 PROVE_TAC [], 3757 PROVE_TAC [unique_nforms, CR_beta0] 3758 ]); 3759 3760val cpl_exists = 3761 (CONV_RULE SKOLEM_CONV o 3762 CONJUNCT1 o 3763 CONV_RULE (BINDER_CONV EXISTS_UNIQUE_CONV THENC FORALL_AND_CONV)) 3764 cpl_uexists 3765 3766val lterm_cpl_def = 3767 new_specification("lterm_cpl_def", ["lterm_cpl"], cpl_exists) 3768 3769val term_posset_cpl_def = Define` 3770 term_posset_cpl (M, FS) = strip_label (lterm_cpl (nlabel 0 M FS)) 3771`; 3772 3773val _ = overload_on("Cpl", ``lterm_cpl``); 3774val _ = overload_on("Cpl", ``term_posset_cpl``); 3775 3776val lterm_cpl_unique = store_thm( 3777 "lterm_cpl_unique", 3778 ``!M' N'. RTC (lcompat_closure beta0) M' N' /\ 3779 (!N''. ~lcompat_closure beta0 N' N'') ==> 3780 (N' = Cpl M')``, 3781 REPEAT GEN_TAC THEN 3782 ASSUME_TAC (CONJUNCT2 (CONV_RULE (BINDER_CONV EXISTS_UNIQUE_CONV THENC 3783 FORALL_AND_CONV) cpl_uexists)) THEN 3784 POP_ASSUM (Q.SPECL_THEN [`M'`, `N'`, `Cpl M'`] MP_TAC) THEN 3785 REWRITE_TAC [lterm_cpl_def]); 3786 3787val Cpl_complete_development = store_thm( 3788 "Cpl_complete_development", 3789 ``!M ps s. s IN complete_development M ps ==> (last s = Cpl (M, ps))``, 3790 SRW_TAC [][complete_development_thm, lemma11_2_12] THEN 3791 Q.ABBREV_TAC `M = first s` THEN 3792 Q.ABBREV_TAC `M' = nlabel 0 M ps` THEN 3793 Q.ABBREV_TAC `s' = lift_path M' s` THEN 3794 `finite s'` by PROVE_TAC [finite_lift_path] THEN 3795 `RTC (lcompat_closure beta0) M' (last s')` by 3796 (`M' = first s'` by PROVE_TAC [first_lift_path] THEN 3797 POP_ASSUM SUBST_ALL_TAC THEN 3798 `!R. lcompat_closure R = \x y. ?r. lrcc R x r y` 3799 by SRW_TAC [][lrcc_lcompat_closure, FUN_EQ_THM] THEN 3800 SRW_TAC [][] THEN MATCH_MP_TAC okpath_RTC THEN SRW_TAC [][]) THEN 3801 `(last s' = nlabel 0 (last s) (residuals s ps))` 3802 by PROVE_TAC [residuals_def] THEN 3803 ASM_SIMP_TAC (srw_ss())[term_posset_cpl_def] THEN 3804 `!n. n_posns n (last s') = {}` 3805 by (GEN_TAC THEN Cases_on `n` THEN 3806 SRW_TAC [][n_posns_nlabel]) THEN 3807 `!N''. ~lcompat_closure beta0 (last s') N''` 3808 by PROVE_TAC [beta0_n_posns, lrcc_lcompat_closure, 3809 NOT_IN_EMPTY] THEN 3810 `Cpl M' = last s'` by PROVE_TAC [lterm_cpl_unique] THEN 3811 SRW_TAC [][strip_label_nlabel]); 3812 3813val FDbang = store_thm( 3814 "FDbang", 3815 ``(s IN development M ==> finite s) /\ 3816 (s IN development M ps ==> 3817 ?s'. (last s = first s') /\ plink s s' IN complete_development M ps) /\ 3818 (!s1 s2. 3819 s1 IN complete_development M ps /\ s2 IN complete_development M ps ==> 3820 (last s1 = last s2))``, 3821 PROVE_TAC [FD, corollary11_2_22i, Cpl_complete_development]); 3822 3823(* written as 3824 3825 ---->> 3826 1 3827 3828 in Barendregt *) 3829 3830 3831val fd_grandbeta_def = Define` 3832 fd_grandbeta M N = ?FS. (Cpl(M, FS) = N) /\ FS SUBSET M 3833`; 3834 3835val n_posns_null_labelling = store_thm( 3836 "n_posns_null_labelling", 3837 ``!n t. n_posns n (null_labelling t) = {}``, 3838 SRW_TAC [][GSYM (Q.SPECL [`M`, `0`] nlabel_null_labelling)] THEN 3839 Cases_on `n = 0` THEN SRW_TAC [][n_posns_nlabel]); 3840 3841val lrcc_beta0_LAM = store_thm( 3842 "lrcc_beta0_LAM", 3843 ``!v t p N. lrcc beta0 (LAM v t) p N = 3844 ?t' r. (N = LAM v t') /\ (p = In :: r) /\ lrcc beta0 t r t'``, 3845 SRW_TAC [][EQ_IMP_THM] THENL [ 3846 IMP_RES_TAC beta0_n_posns THEN 3847 `lrcc (beta0 RUNION beta1) (LAM v t) p N` by PROVE_TAC [pick_a_beta] THEN 3848 `?p0 N0. lrcc (beta0 RUNION beta1) t p0 N0 /\ 3849 (N = LAM v N0) /\ (p = In::p0)` by PROVE_TAC [lrcc_beta_lam] THEN 3850 `p0 IN n_posns n t` by FULL_SIMP_TAC (srw_ss()) [n_posns_def] THEN 3851 PROVE_TAC [pick_a_beta], 3852 PROVE_TAC [lrcc_rules] 3853 ]); 3854 3855val lcompat_closure_RUNION_MONOTONE = store_thm( 3856 "lcompat_closure_RUNION_MONOTONE", 3857 ``!R1 x y. lcompat_closure R1 x y ==> lcompat_closure (R1 RUNION R2) x y``, 3858 GEN_TAC THEN HO_MATCH_MP_TAC lcompat_closure_ind THEN 3859 PROVE_TAC [lcompat_closure_rules, relationTheory.RUNION]); 3860 3861val lcompat_closure_RUNION_distrib = store_thm( 3862 "lcompat_closure_RUNION_distrib", 3863 ``!R1 R2. lcompat_closure R1 RUNION lcompat_closure R2 = 3864 lcompat_closure (R1 RUNION R2)``, 3865 ASM_SIMP_TAC (srw_ss())[FUN_EQ_THM, relationTheory.RUNION, EQ_IMP_THM, 3866 DISJ_IMP_THM, FORALL_AND_THM] THEN 3867 REPEAT CONJ_TAC THENL [ 3868 PROVE_TAC [lcompat_closure_RUNION_MONOTONE], 3869 PROVE_TAC [lcompat_closure_RUNION_MONOTONE, RUNION_COMM], 3870 Q_TAC SUFF_TAC 3871 `!R x y. lcompat_closure R x y ==> 3872 !R1 R2. (R = R1 RUNION R2) ==> 3873 lcompat_closure R1 x y \/ lcompat_closure R2 x y` THEN1 3874 PROVE_TAC [] THEN GEN_TAC THEN 3875 HO_MATCH_MP_TAC lcompat_closure_ind THEN SRW_TAC [][] THEN 3876 PROVE_TAC [relationTheory.RUNION, lcompat_closure_rules] 3877 ]); 3878 3879val beta0_reduce_at_single_label = store_thm( 3880 "beta0_reduce_at_single_label", 3881 ``!x pos y. lrcc beta0 (nlabel 0 x {pos}) pos y ==> 3882 (!n. n_posns n y = {})``, 3883 HO_MATCH_MP_TAC simple_induction THEN REPEAT CONJ_TAC THEN 3884 SIMP_TAC (srw_ss()) [nlabel_thm] THENL [ 3885 ONCE_REWRITE_TAC [lrcc_cases] THEN SRW_TAC [][beta0_def], 3886 MAP_EVERY Q.X_GEN_TAC [`f`,`x`] THEN Cases_on `is_abs f` THENL [ 3887 `?v body. f = LAM v body` by PROVE_TAC [is_abs_thm, term_CASES] THEN 3888 ASM_SIMP_TAC (srw_ss()) [nlabel_thm] THEN STRIP_TAC THEN 3889 REPEAT GEN_TAC THEN COND_CASES_TAC THEN 3890 VAR_EQ_TAC THEN 3891 ASM_SIMP_TAC (srw_ss()) [] THEN 3892 ONCE_REWRITE_TAC [lrcc_cases] THENL [ 3893 ASM_SIMP_TAC (srw_ss()) [beta0_LAMi, n_posns_sub, 3894 nlabel_null_labelling, 3895 n_posns_null_labelling, EXTENSION], 3896 SRW_TAC [][beta0_def, n_posns_def, IMAGE_EQ_EMPTY, 3897 nlabel_null_labelling, n_posns_null_labelling] THEN 3898 RES_TAC THEN SRW_TAC [][] 3899 ], 3900 ASM_SIMP_TAC (srw_ss()) [nlabel_thm] THEN 3901 STRIP_TAC THEN 3902 ONCE_REWRITE_TAC [lrcc_cases] THEN 3903 SRW_TAC [][beta0_def, n_posns_def, IMAGE_EQ_EMPTY, 3904 nlabel_null_labelling, n_posns_null_labelling] THEN 3905 RES_TAC THEN SRW_TAC [][] 3906 ], 3907 REPEAT GEN_TAC THEN STRIP_TAC THEN 3908 SRW_TAC [][lrcc_beta0_LAM] THEN 3909 SRW_TAC [][n_posns_def, IMAGE_EQ_EMPTY] THEN 3910 PROVE_TAC [] 3911 ]); 3912 3913val lemma11_2_28i = store_thm( 3914 "lemma11_2_28i", 3915 ``RTC (compat_closure beta) = TC fd_grandbeta``, 3916 SIMP_TAC (srw_ss()) [FUN_EQ_THM, EQ_IMP_THM, FORALL_AND_THM] THEN 3917 CONJ_TAC THENL [ 3918 HO_MATCH_MP_TAC relationTheory.RTC_INDUCT THEN CONJ_TAC THENL [ 3919 (* TC fd_grandbeta is reflexive *) 3920 Q.X_GEN_TAC `x` THEN 3921 Q.ISPEC_THEN `fd_grandbeta` (MATCH_MP_TAC o CONJUNCT1) 3922 relationTheory.TC_RULES THEN 3923 SRW_TAC [][fd_grandbeta_def] THEN Q.EXISTS_TAC `{}` THEN 3924 SRW_TAC [][term_posset_cpl_def, redexes_all_occur_def] THEN 3925 Q.ABBREV_TAC `x' = nlabel 0 x {}` THEN 3926 `RTC (lcompat_closure beta0) x' x'` 3927 by PROVE_TAC [relationTheory.RTC_RULES] THEN 3928 `!n. n_posns n x' = {}` by PROVE_TAC [INTER_EMPTY, 3929 n_posns_nlabel] THEN 3930 `!y'. ~lcompat_closure beta0 x' y'` 3931 by PROVE_TAC [NOT_IN_EMPTY, lrcc_lcompat_closure, 3932 beta0_n_posns] THEN 3933 `Cpl x' = x'` by PROVE_TAC [lterm_cpl_unique] THEN 3934 SRW_TAC [][strip_label_nlabel, Abbr`x'`], 3935 MAP_EVERY Q.X_GEN_TAC [`x`,`y`,`z`] THEN REPEAT STRIP_TAC THEN 3936 Q.ISPEC_THEN `fd_grandbeta` (MATCH_MP_TAC o CONJUNCT2) 3937 relationTheory.TC_RULES THEN 3938 Q.EXISTS_TAC `y` THEN SRW_TAC [][] THEN 3939 Q.ISPEC_THEN `fd_grandbeta` (MATCH_MP_TAC o CONJUNCT1) 3940 relationTheory.TC_RULES THEN 3941 SRW_TAC [][fd_grandbeta_def, term_posset_cpl_def] THEN 3942 IMP_RES_TAC cc_labelled_redn THEN 3943 Q.EXISTS_TAC `{pos}` THEN 3944 Q.ABBREV_TAC `M' = nlabel 0 x {pos}` THEN 3945 Q.ABBREV_TAC `N' = lift_redn M' pos y` THEN 3946 `lrcc (beta0 RUNION beta1) M' pos N' /\ (y = strip_label N')` by 3947 METIS_TAC [lift_redn_def, strip_label_nlabel] THEN 3948 `pos IN redex_posns x` 3949 by (SRW_TAC [][redex_posns_redex_occurrence, 3950 is_redex_occurrence_def] THEN PROVE_TAC []) THEN 3951 `pos IN n_posns 0 M'` by SRW_TAC [][n_posns_nlabel, Abbr`M'`] THEN 3952 `lrcc beta0 M' pos N'` by PROVE_TAC [pick_a_beta] THEN 3953 `!n. n_posns n N' = {}` by PROVE_TAC [beta0_reduce_at_single_label] THEN 3954 `RTC (lcompat_closure beta0) M' N'` 3955 by PROVE_TAC [relationTheory.RTC_RULES, lrcc_lcompat_closure] THEN 3956 `!N''. ~lcompat_closure beta0 N' N''` 3957 by PROVE_TAC [NOT_IN_EMPTY, lrcc_lcompat_closure, 3958 beta0_n_posns] THEN 3959 `Cpl M' = N'` by PROVE_TAC [lterm_cpl_unique] THEN 3960 SRW_TAC [][strip_label_nlabel, redexes_all_occur_def, 3961 IN_term_IN_redex_posns] 3962 ], 3963 HO_MATCH_MP_TAC relationTheory.TC_INDUCT THEN CONJ_TAC THENL [ 3964 MAP_EVERY Q.X_GEN_TAC [`M`, `N`] THEN 3965 SRW_TAC [][fd_grandbeta_def, term_posset_cpl_def] THEN 3966 Q.SPEC_THEN `nlabel 0 M FS` STRIP_ASSUME_TAC lterm_cpl_def THEN 3967 Q.ABBREV_TAC `M' = nlabel 0 M FS` THEN 3968 `RTC (lcompat_closure beta0 RUNION lcompat_closure beta1) M' (Cpl M')` 3969 by PROVE_TAC [RUNION_RTC_MONOTONE] THEN 3970 FULL_SIMP_TAC (srw_ss()) [lcompat_closure_RUNION_distrib] THEN 3971 `RTC (compat_closure beta) (strip_label M') (strip_label (Cpl M'))` by 3972 PROVE_TAC [lemma11_1_6ii] THEN 3973 Q.UNABBREV_TAC `M'` THEN FULL_SIMP_TAC (srw_ss()) [strip_label_nlabel], 3974 PROVE_TAC [relationTheory.RTC_RTC] 3975 ] 3976 ]); 3977 3978val complete_developments_are_developments = store_thm( 3979 "complete_developments_are_developments", 3980 ``!s. s IN complete_development M ps ==> s IN development M ps``, 3981 SRW_TAC [][complete_development_thm]); 3982 3983val complete_developments_always_exist = store_thm( 3984 "complete_developments_always_exist", 3985 ``!M ps. ps SUBSET M ==> ?s. s IN complete_development M ps``, 3986 REPEAT STRIP_TAC THEN 3987 `stopped_at M IN development M ps` by SRW_TAC [][development_thm] THEN 3988 IMP_RES_TAC corollary11_2_22i THEN 3989 FULL_SIMP_TAC (srw_ss()) [] THEN PROVE_TAC []); 3990 3991 3992val development_SUBSET = store_thm( 3993 "development_SUBSET", 3994 ``!s M FS1 FS2. s IN development M FS1 /\ FS1 SUBSET FS2 /\ FS2 SUBSET M ==> 3995 s IN development M FS2``, 3996 REWRITE_TAC [SPECIFICATION] THEN 3997 SIMP_TAC (srw_ss()) [term_posset_development_def] THEN 3998 Q_TAC SUFF_TAC 3999 `!s FS2. (?FS1. FS1 SUBSET FS2 /\ development0 s FS1) ==> 4000 development0 s FS2` THEN1 PROVE_TAC [] THEN 4001 HO_MATCH_MP_TAC development0_coinduction THEN GEN_TAC THEN 4002 Q.ISPEC_THEN `s` STRUCT_CASES_TAC path_cases THEN 4003 SRW_TAC [][] THEN 4004 RULE_ASSUM_TAC (ONCE_REWRITE_RULE [development0_cases]) THEN 4005 FULL_SIMP_TAC (srw_ss()) [] THENL [ 4006 PROVE_TAC [SUBSET_DEF], 4007 `?FS'. FS2 = FS1 UNION FS'` 4008 by (FULL_SIMP_TAC (srw_ss()) [SUBSET_DEF, EXTENSION] THEN 4009 PROVE_TAC []) THEN 4010 POP_ASSUM SUBST_ALL_TAC THEN 4011 ASM_SIMP_TAC (srw_ss()) [residual1_pointwise_union] THEN 4012 PROVE_TAC [SUBSET_UNION] 4013 ]); 4014 4015val redex_occurrences_SUBSET = store_thm( 4016 "redex_occurrences_SUBSET", 4017 ``!s M. s SUBSET M <=> s SUBSET (redex_posns M)``, 4018 SRW_TAC [][redexes_all_occur_def, IN_term_IN_redex_posns, SUBSET_DEF]); 4019 4020val linking_developments = store_thm( 4021 "linking_developments", 4022 ``!s t M FS. 4023 s IN development M FS /\ finite s /\ 4024 t IN development (last s) (residuals s FS) ==> 4025 (plink s t) IN development M FS``, 4026 SRW_TAC [][lemma11_2_12, first_plink, okpath_plink, 4027 lift_path_plink, okpath_plink, first_lift_path, 4028 finite_lift_path] THEN 4029 Q_TAC SUFF_TAC `last (lift_path (nlabel 0 (first s) FS) s) = 4030 nlabel 0 (first t) (residuals s FS)` THEN1 PROVE_TAC [] THEN 4031 PROVE_TAC [residuals_def]); 4032 4033val wf_development = store_thm( 4034 "wf_development", 4035 ``!M FS s. s IN development M FS ==> (first s = M) /\ FS SUBSET M``, 4036 SRW_TAC [][term_posset_development_def, SPECIFICATION]); 4037 4038val lemma11_2_28ii = store_thm( 4039 "lemma11_2_28ii", 4040 ``diamond_property fd_grandbeta``, 4041 Q_TAC SUFF_TAC 4042 `!M M1 M2. fd_grandbeta M M1 /\ fd_grandbeta M M2 ==> 4043 ?N. fd_grandbeta M1 N /\ fd_grandbeta M2 N` 4044 THEN1 SRW_TAC [][diamond_property_def] THEN 4045 REPEAT STRIP_TAC THEN 4046 `?FS1 FS2. (M1 = Cpl(M, FS1)) /\ (M2 = Cpl(M, FS2)) /\ FS1 SUBSET M /\ 4047 FS2 SUBSET M` by 4048 PROVE_TAC [fd_grandbeta_def] THEN 4049 `(FS1 UNION FS2) SUBSET M` by 4050 FULL_SIMP_TAC (srw_ss()) [redex_occurrences_SUBSET] THEN 4051 `?s1 s2. s1 IN complete_development M FS1 /\ (last s1 = M1) /\ 4052 s2 IN complete_development M FS2 /\ (last s2 = M2)` 4053 by METIS_TAC [complete_developments_always_exist, 4054 Cpl_complete_development] THEN 4055 `finite s1 /\ okpath (labelled_redn beta) s1 /\ 4056 finite s2 /\ okpath (labelled_redn beta) s2` 4057 by PROVE_TAC [complete_development_thm, lemma11_2_12] THEN 4058 `residuals s1 FS2 SUBSET M1 /\ residuals s2 FS1 SUBSET M2` 4059 by PROVE_TAC [residuals_def, redex_occurrences_SUBSET] THEN 4060 `?s1' s2'. s1' IN complete_development M1 (residuals s1 FS2) /\ 4061 s2' IN complete_development M2 (residuals s2 FS1)` 4062 by PROVE_TAC [complete_developments_always_exist] THEN 4063 `(residuals s1 FS1 = {}) /\ (residuals s1' (residuals s1 FS2) = {}) /\ 4064 (residuals s2 FS2 = {}) /\ (residuals s2' (residuals s2 FS1) = {})` 4065 by PROVE_TAC [complete_development_thm] THEN 4066 `(residuals s1 (FS1 UNION FS2) = residuals s1 FS2) /\ 4067 (residuals s2 (FS1 UNION FS2) = residuals s2 FS1)` 4068 by SRW_TAC [][residuals_pointwise_union] THEN 4069 `plink s1 s1' IN development M (FS1 UNION FS2) /\ 4070 plink s2 s2' IN development M (FS1 UNION FS2)` 4071 by PROVE_TAC [linking_developments, development_SUBSET, 4072 SUBSET_UNION, 4073 complete_developments_are_developments] THEN 4074 `(first s1' = last s1) /\ (first s2' = last s2) /\ finite s1' /\ finite s2'` 4075 by PROVE_TAC [complete_development_thm, wf_development] THEN 4076 `okpath (labelled_redn beta) s1' /\ okpath (labelled_redn beta) s2'` 4077 by PROVE_TAC [lemma11_2_12, complete_developments_are_developments] THEN 4078 `(residuals (plink s1 s1') (FS1 UNION FS2) = {}) /\ 4079 (residuals (plink s2 s2') (FS1 UNION FS2) = {})` 4080 by SRW_TAC [][lemma11_2_6] THEN 4081 `(plink s1 s1') IN complete_development M (FS1 UNION FS2) /\ 4082 (plink s2 s2') IN complete_development M (FS1 UNION FS2)` 4083 by PROVE_TAC [complete_development_thm, finite_plink] THEN 4084 `(last s1' = Cpl(M, FS1 UNION FS2)) /\ (last s2' = Cpl(M, FS1 UNION FS2))` 4085 by PROVE_TAC [Cpl_complete_development, last_plink] THEN 4086 Q.EXISTS_TAC `Cpl(M, FS1 UNION FS2)` THEN 4087 SIMP_TAC (srw_ss()) [fd_grandbeta_def] THEN 4088 CONJ_TAC THENL [ 4089 Q.EXISTS_TAC `residuals s1 FS2`, 4090 Q.EXISTS_TAC `residuals s2 FS1` 4091 ] THEN PROVE_TAC [Cpl_complete_development]); 4092 4093val corollary11_2_29 = store_thm( 4094 "corollary11_2_29", 4095 ``CR beta``, 4096 SRW_TAC [][CR_def, lemma11_2_28i, lemma11_2_28ii, 4097 relationTheory.diamond_TC_diamond]); 4098 4099val _ = export_theory(); 4100