1open HolKernel Parse boolLib bossLib termTheory binderLib chap2Theory 2 3open BasicProvers pred_setTheory boolSimps 4 5val _ = new_theory "term_posns"; 6 7fun Store_Thm(n,t,tac) = store_thm(n,t,tac) before export_rewrites [n] 8fun Save_Thm(n,th) = save_thm(n,th) before export_rewrites [n] 9 10 11(* ---------------------------------------------------------------------- 12 type of (term) positions 13 ---------------------------------------------------------------------- *) 14 15val _ = Hol_datatype `redpos = Lt | Rt | In`; 16 17val _ = type_abbrev ("posn", ``:redpos list``) 18 19val APPEND_CASES = store_thm( 20 "APPEND_CASES", 21 ``!l1 l2 m1 m2. 22 (APPEND l1 l2 = APPEND m1 m2) <=> 23 (l1 = m1) /\ (l2 = m2) \/ 24 (?n. (m1 = APPEND l1 n) /\ (l2 = APPEND n m2) /\ ~(n = [])) \/ 25 (?n. (l1 = APPEND m1 n) /\ (m2 = APPEND n l2) /\ ~(n = []))``, 26 Induct THENL [ 27 SRW_TAC [][EQ_IMP_THM] THEN SRW_TAC [][] THEN 28 PROVE_TAC [listTheory.APPEND], 29 SRW_TAC [][] THEN Cases_on `m1` THENL [ 30 SRW_TAC [][] THEN PROVE_TAC [], 31 SRW_TAC [][EQ_IMP_THM] THEN PROVE_TAC [listTheory.APPEND_ASSOC] 32 ] 33 ]); 34 35(* ---------------------------------------------------------------------- 36 ordering positions 37 ---------------------------------------------------------------------- *) 38 39val posn_lt_def = Define` 40 (posn_lt _ [] = F) /\ 41 (posn_lt [] _ = T) /\ 42 (posn_lt (In::ps1) (In::ps2) = posn_lt ps1 ps2) /\ 43 (posn_lt (In::_) _ = F) /\ 44 (posn_lt (Lt::ps1) (Lt::ps2) = posn_lt ps1 ps2) /\ 45 (posn_lt (Lt::_) (In::_) = F) /\ 46 (posn_lt (Lt::_) (Rt::_) = T) /\ 47 (posn_lt (Rt::ps1) (Rt::ps2) = posn_lt ps1 ps2) /\ 48 (posn_lt (Rt::_) _ = F) 49`; 50val _ = export_rewrites ["posn_lt_def"] 51 52 53val _ = overload_on ("<", ``posn_lt``); 54 55val posn_lt_inj = Store_Thm( 56 "posn_lt_inj", 57 ``!h p1 p2. (h::p1) < (h::p2) <=> p1 < p2``, 58 Cases THEN SRW_TAC [][]); 59 60val posn_lt_nil = Store_Thm( 61 "posn_lt_nil", 62 ``!p : posn. ~(p < [])``, 63 Cases THEN SRW_TAC [][] THEN Cases_on `h` THEN SRW_TAC [][]); 64 65val posn_lt_trans = store_thm( 66 "posn_lt_trans", 67 ``!p1 p2 p3 : posn. p1 < p2 /\ p2 < p3 ==> p1 < p3``, 68 Induct THENL [ 69 NTAC 2 (Cases THEN SIMP_TAC (srw_ss()) [posn_lt_def]), 70 Cases THEN Induct THEN 71 SIMP_TAC (srw_ss()) [posn_lt_def] THEN 72 Cases THEN SIMP_TAC (srw_ss()) [posn_lt_def] THEN 73 Induct THEN TRY Cases THEN ASM_SIMP_TAC (srw_ss()) [posn_lt_def] THEN 74 PROVE_TAC [] 75 ]); 76 77val posn_lt_irrefl = Store_Thm( 78 "posn_lt_irrefl", 79 ``!p : posn. ~(p < p)``, 80 Induct THEN SRW_TAC [][]); 81 82val posn_lt_antisym = store_thm( 83 "posn_lt_antisym", 84 ``!p1 p2. p1 < p2 ==> ~(p2 < p1)``, 85 HO_MATCH_MP_TAC (theorem "posn_lt_ind") THEN 86 SRW_TAC [][]); 87 88val posn_lt_Lt = Store_Thm( 89 "posn_lt_Lt", 90 ``!h p1 p2. ((h::p1) < (Lt::p2) <=> (h = Lt) /\ p1 < p2) /\ 91 ((Lt::p1) < (h::p2) <=> (h = Rt) \/ (h = Lt) /\ p1 < p2)``, 92 Cases THEN SRW_TAC [][]); 93 94val posn_lt_In = Store_Thm( 95 "posn_lt_In", 96 ``!h p1 p2. ((h::p1) < (In::p2) <=> (h = In) /\ p1 < p2) /\ 97 ((In::p1) < (h::p2) <=> (h = In) /\ p1 < p2)``, 98 Cases THEN SRW_TAC [][]); 99 100val posn_lt_Rt = Store_Thm( 101 "posn_lt_Rt", 102 ``!h p1 p2. ((h::p1) < (Rt::p2) <=> (h = Lt) \/ (h = Rt) /\ p1 < p2) /\ 103 ((Rt::p1) < (h::p2) <=> (h = Rt) /\ p1 < p2)``, 104 Cases THEN SRW_TAC [][]); 105 106(* ---------------------------------------------------------------------- 107 all of a term's positions (valid_posns) 108 ---------------------------------------------------------------------- *) 109 110val (valid_posns_thm, _) = define_recursive_term_function` 111 (valid_posns (VAR s) = {[]}) /\ 112 (valid_posns (t @@ u) = [] INSERT IMAGE (CONS Lt) (valid_posns t) UNION 113 IMAGE (CONS Rt) (valid_posns u)) /\ 114 (valid_posns (LAM v t) = [] INSERT IMAGE (CONS In) (valid_posns t)) 115`; 116val _ = export_rewrites ["valid_posns_thm"] 117 118val valid_posns_vsubst = Store_Thm( 119 "valid_posns_vsubst", 120 ``!M. valid_posns ([VAR v/u] M) = valid_posns M``, 121 HO_MATCH_MP_TAC nc_INDUCTION2 THEN Q.EXISTS_TAC `{u;v}` THEN 122 SRW_TAC [][SUB_THM, SUB_VAR]); 123 124 125val NIL_always_valid = Store_Thm( 126 "NIL_always_valid", 127 ``!t. [] IN valid_posns t``, 128 GEN_TAC THEN Q.SPEC_THEN `t` STRUCT_CASES_TAC term_CASES THEN 129 SRW_TAC [][]); 130 131val valid_posns_FINITE = Store_Thm( 132 "valid_posns_FINITE", 133 ``!t : term. FINITE (valid_posns t)``, 134 HO_MATCH_MP_TAC simple_induction THEN SIMP_TAC (srw_ss()) []); 135 136val all_valid_posns_comparable = store_thm( 137 "all_valid_posns_comparable", 138 ``!t p1 p2. p1 IN valid_posns t /\ p2 IN valid_posns t ==> 139 p1 < p2 \/ (p1 = p2) \/ p2 < p1``, 140 HO_MATCH_MP_TAC simple_induction THEN SRW_TAC [][]); 141 142(* ---------------------------------------------------------------------- 143 positions of all of a term's variables, free or bound. (var_posns) 144 ---------------------------------------------------------------------- *) 145 146val (var_posns_thm, _) = define_recursive_term_function` 147 (var_posns (VAR s) = {[]}) /\ 148 (var_posns (t @@ u) = IMAGE (CONS Lt) (var_posns t) UNION 149 IMAGE (CONS Rt) (var_posns u)) /\ 150 (var_posns (LAM v t) = IMAGE (CONS In) (var_posns t))`; 151val _ = export_rewrites ["var_posns_thm"] 152 153val var_posns_vsubst_invariant = Store_Thm( 154 "var_posns_vsubst_invariant", 155 ``!M. var_posns ([VAR v/u]M) = var_posns M``, 156 HO_MATCH_MP_TAC nc_INDUCTION2 THEN Q.EXISTS_TAC `{u;v}` THEN 157 SRW_TAC [][SUB_THM, SUB_VAR]); 158 159val var_posns_FINITE = Store_Thm( 160 "var_posns_FINITE", 161 ``!t:term. FINITE (var_posns t)``, 162 HO_MATCH_MP_TAC simple_induction THEN SIMP_TAC (srw_ss()) []); 163 164val var_posns_SUBSET_valid_posns = store_thm( 165 "var_posns_SUBSET_valid_posns", 166 ``!t p. p IN var_posns t ==> p IN valid_posns t``, 167 HO_MATCH_MP_TAC simple_induction THEN 168 SRW_TAC [][]); 169 170(* ---------------------------------------------------------------------- 171 positions with a term of a particular free variable (v_posns) 172 ---------------------------------------------------------------------- *) 173 174val vp'_var = ``\(s : string) v. if v = s then {[]: redpos list} else {}`` 175val vp'_lam = ``\rt (w:string) t:term (v:string). IMAGE (CONS In) (rt v)`` 176 177val lemma = prove( 178 ``fnpm dact discrete_pmact pi f x = f (pmact dact pi����� x)``, 179 SRW_TAC [][nomsetTheory.fnpm_def]); 180 181val flip_args = prove( 182 ``(?f: 'a -> 'b -> 'c. P f) <=> (?f : 'b -> 'a -> 'c. P (��a b. f b a))``, 183 SRW_TAC [][EQ_IMP_THM] THEN1 (Q.EXISTS_TAC `��b a. f a b` THEN SRW_TAC [ETA_ss][]) THEN 184 METIS_TAC []); 185 186val v_posns_exists = 187 termTheory.parameter_tm_recursion 188 |> INST_TYPE [alpha |-> ``:posn set``, ``:��`` |-> ``:string``] 189 |> SPEC_ALL 190 |> Q.INST [`apm` |-> `discrete_pmact`, `ppm` |-> `string_pmact`, 191 `A` |-> `{}`, 192 `vr` |-> `^vp'_var`, 193 `ap` |-> `\rt ru t u v. IMAGE (CONS Lt) (rt v) ��� IMAGE (CONS Rt) (ru v)`, 194 `lm` |-> `^vp'_lam`] 195 |> SIMP_RULE (srw_ss()) [GSYM basic_swapTheory.swapstr_eq_left, 196 lemma] 197 |> SIMP_RULE (srw_ss()) [Once flip_args] 198 199val v_posns_def = new_specification("v_posns_def", ["v_posns"], 200 v_posns_exists); 201 202val lemma = v_posns_def |> CONJUNCT2 |> SPEC_ALL |> Q.INST [`p` |-> `swapstr x y p`] 203 |> SIMP_RULE (srw_ss()) [] 204 205val v_posns_tpm_invariant = Store_Thm( 206 "v_posns_tpm_invariant", 207 ``!M v. v_posns v (tpm pi M) = v_posns (lswapstr (REVERSE pi) v) M``, 208 Induct_on `pi` THEN 209 ASM_SIMP_TAC (srw_ss()) [pairTheory.FORALL_PROD, nomsetTheory.pmact_decompose] THEN 210 POP_ASSUM (fn th => REWRITE_TAC [GSYM th]) THEN 211 SRW_TAC [][lemma, GSYM nomsetTheory.pmact_decompose]); 212 213val v_posns_FV = store_thm( 214 "v_posns_FV", 215 ``!t. ~(v IN FV t) ==> (v_posns v t = {})``, 216 HO_MATCH_MP_TAC nc_INDUCTION2 THEN Q.EXISTS_TAC `{v}` THEN 217 SRW_TAC [][v_posns_def]); 218 219val v_posns_LAM = prove( 220 ``v_posns v (LAM u t) = if v = u then {} 221 else IMAGE (CONS In) (v_posns v t)``, 222 SRW_TAC [][v_posns_FV, v_posns_def]); 223 224val v_posns_thm = Save_Thm( 225 "v_posns_thm", 226 LIST_CONJ (butlast (CONJUNCTS (CONJUNCT1 v_posns_def)) @ 227 [GEN_ALL v_posns_LAM])) 228 229val v_posns_vsubst = store_thm( 230 "v_posns_vsubst", 231 ``!M x y z. 232 v_posns x ([VAR y/z] M) = 233 if x = y then v_posns x M UNION v_posns z M 234 else if x = z then {} 235 else v_posns x M``, 236 REPEAT GEN_TAC THEN Q.ID_SPEC_TAC `M` THEN 237 HO_MATCH_MP_TAC nc_INDUCTION2 THEN 238 Q.EXISTS_TAC `{x;y;z}` THEN 239 SIMP_TAC (srw_ss()) [v_posns_thm, SUB_THM, SUB_VAR] THEN 240 REPEAT CONJ_TAC THENL [ 241 REPEAT GEN_TAC THEN REPEAT COND_CASES_TAC THEN SRW_TAC [][v_posns_thm], 242 REPEAT GEN_TAC THEN DISCH_THEN (K ALL_TAC) THEN 243 REPEAT GEN_TAC THEN REPEAT COND_CASES_TAC THEN 244 SRW_TAC [][] THEN REWRITE_TAC [EXTENSION] THEN 245 METIS_TAC [IN_UNION], 246 247 REPEAT GEN_TAC THEN STRIP_TAC THEN REPEAT GEN_TAC THEN 248 REPEAT COND_CASES_TAC THEN SRW_TAC [][] 249 ]); 250 251val v_posns_FV_EQ = store_thm( 252 "v_posns_FV_EQ", 253 ``!t v. (v_posns v t = {}) = ~(v IN FV t)``, 254 SIMP_TAC (srw_ss() ++ DNF_ss) [EQ_IMP_THM, v_posns_FV] THEN 255 HO_MATCH_MP_TAC simple_induction THEN 256 SRW_TAC [][v_posns_thm, IMAGE_EQ_EMPTY] THEN 257 PROVE_TAC [IMAGE_EQ_EMPTY]); 258 259val v_posns_LAM_COND = save_thm("v_posns_LAM_COND", v_posns_LAM); 260 261val v_posns_SUBSET_var_posns = store_thm( 262 "v_posns_SUBSET_var_posns", 263 ``!t v p. p IN v_posns v t ==> p IN var_posns t``, 264 HO_MATCH_MP_TAC simple_induction THEN 265 SRW_TAC [][v_posns_thm, var_posns_thm] THENL [ 266 PROVE_TAC [], 267 PROVE_TAC [], 268 Cases_on `v = v'` THEN FULL_SIMP_TAC (srw_ss()) [] THEN 269 PROVE_TAC [] 270 ]); 271 272val IMAGE_DIFF = prove( 273 ``(!x y. (f x = f y) = (x = y)) ==> 274 (IMAGE f (P DIFF Q) = IMAGE f P DIFF IMAGE f Q)``, 275 SRW_TAC [][EXTENSION] THEN PROVE_TAC []); 276 277val IMAGE_CONS_APPEND = prove( 278 ``IMAGE (CONS v) {APPEND x y | P x /\ Q y} = 279 {APPEND x y | (?x'. (x = v::x') /\ P x') /\ Q y}``, 280 SRW_TAC [][EXTENSION, EQ_IMP_THM, GSYM RIGHT_EXISTS_AND_THM, 281 GSYM LEFT_EXISTS_AND_THM] THEN PROVE_TAC []); 282 283val var_posns_subst = store_thm( 284 "var_posns_subst", 285 ``!x v t. var_posns ([t/v] x) = 286 (var_posns x DIFF v_posns v x) UNION 287 {APPEND p1 p2 | p1 IN v_posns v x /\ p2 IN var_posns t}``, 288 REPEAT GEN_TAC THEN Q.ID_SPEC_TAC `x` THEN 289 HO_MATCH_MP_TAC nc_INDUCTION2 THEN 290 Q.EXISTS_TAC `v INSERT FV t` THEN REPEAT CONJ_TAC THENL [ 291 SIMP_TAC (srw_ss() ++ boolSimps.COND_elim_ss ++ DNF_ss) 292 [var_posns_thm, v_posns_thm, SUB_THM, SUB_VAR, 293 EXTENSION, EQ_IMP_THM], 294 SRW_TAC [][var_posns_thm, v_posns_thm, SUB_THM] THEN 295 SIMP_TAC (srw_ss() ++ DNF_ss) [EXTENSION, EQ_IMP_THM] THEN 296 REPEAT CONJ_TAC THEN PROVE_TAC [], 297 SRW_TAC [][SUB_THM, var_posns_thm, v_posns_thm] THEN 298 SRW_TAC [][IMAGE_DIFF, IMAGE_CONS_APPEND], 299 SRW_TAC [][] 300 ]); 301 302(* ---------------------------------------------------------------------- 303 positions of the bound variables underneath an abstraction 304 ---------------------------------------------------------------------- *) 305 306val (bv_posns_thm, _) = define_recursive_term_function 307 `(bv_posns (LAM v t : term) = IMAGE (CONS In) (v_posns v t)) /\ 308 (bv_posns (VAR s) = {}) /\ 309 (bv_posns (t @@ u) = {})`; 310val _ = export_rewrites ["bv_posns_thm"] 311 312val bv_posns_vsubst = Store_Thm( 313 "bv_posns_vsubst", 314 ``!M. bv_posns ([VAR v/u] M) = bv_posns M``, 315 HO_MATCH_MP_TAC nc_INDUCTION2 THEN Q.EXISTS_TAC `{u;v}` THEN 316 SRW_TAC [][SUB_THM, SUB_VAR, v_posns_vsubst]); 317 318(* ---------------------------------------------------------------------- 319 positions of all a term's abstractions 320 ---------------------------------------------------------------------- *) 321 322val (lam_posns_thm, _) = define_recursive_term_function` 323 (lam_posns (VAR s : term) = {}) /\ 324 (lam_posns (t @@ u) = IMAGE (CONS Lt) (lam_posns t) UNION 325 IMAGE (CONS Rt) (lam_posns u)) /\ 326 (lam_posns (LAM v t) = [] INSERT IMAGE (CONS In) (lam_posns t)) 327`; 328val _ = export_rewrites ["lam_posns_thm"] 329 330val lam_posns_vsubst = Store_Thm( 331 "lam_posns_vsubst", 332 ``!M. lam_posns ([VAR v/u]M) = lam_posns M``, 333 HO_MATCH_MP_TAC nc_INDUCTION2 THEN Q.EXISTS_TAC `{u;v}` THEN 334 SRW_TAC [][SUB_THM, SUB_VAR]); 335 336val lam_posns_SUBSET_valid_posns = store_thm( 337 "lam_posns_SUBSET_valid_posns", 338 ``!t p. p IN lam_posns t ==> p IN valid_posns t``, 339 HO_MATCH_MP_TAC simple_induction THEN 340 SRW_TAC [][]); 341 342val lam_posns_var_posns = store_thm( 343 "lam_posns_var_posns", 344 ``!t p. ~(p IN lam_posns t /\ p IN var_posns t)``, 345 Q_TAC SUFF_TAC `!t p. p IN lam_posns t ==> ~(p IN var_posns t)` 346 THEN1 METIS_TAC [] THEN 347 HO_MATCH_MP_TAC simple_induction THEN 348 SRW_TAC [][var_posns_thm, lam_posns_thm] THEN 349 METIS_TAC []); 350 351(* ---------------------------------------------------------------------- 352 positions of all a term's redexes 353 ---------------------------------------------------------------------- *) 354 355val (redex_posns_thm, _) = define_recursive_term_function` 356 (redex_posns (VAR s : term) = {}) /\ 357 (redex_posns (t @@ u) = 358 IMAGE (CONS Lt) (redex_posns t) UNION 359 IMAGE (CONS Rt) (redex_posns u) UNION 360 (if is_abs t then {[]} else {})) /\ 361 (redex_posns (LAM v t) = IMAGE (CONS In) (redex_posns t)) 362`; 363 364val redex_posns_vsubst_invariant = Store_Thm( 365 "redex_posns_vsubst_invariant", 366 ``!M. redex_posns ([VAR v/u]M) = redex_posns M``, 367 HO_MATCH_MP_TAC nc_INDUCTION2 THEN Q.EXISTS_TAC `{u;v}` THEN 368 SRW_TAC [][SUB_THM, SUB_VAR, redex_posns_thm]); 369 370val redex_posns_are_valid = store_thm( 371 "redex_posns_are_valid", 372 ``!t p. p IN redex_posns t ==> p IN valid_posns t``, 373 HO_MATCH_MP_TAC simple_induction THEN 374 SRW_TAC [][valid_posns_thm, redex_posns_thm]); 375 376(* ---------------------------------------------------------------------- 377 bv_posns_at : posn -> term -> posn set 378 assuming posn is the position of an abstraction within the term, 379 return the set of positions of its bound variables. Otherwise, 380 return {} 381 ---------------------------------------------------------------------- *) 382 383val bv_posns_at_exists0 = 384 tm_recursion_nosideset 385 |> SPEC_ALL 386 |> INST_TYPE [alpha |-> ``:redpos list -> redpos list set``] 387 |> Q.INST [`apm` |-> `discrete_pmact`, 388 `vr` |-> `\s l. {}`, 389 `ap` |-> `\rt ru t u l. 390 case l of 391 Lt::rest => IMAGE (CONS Lt) (rt rest) 392 | Rt::rest => IMAGE (CONS Rt) (ru rest) 393 | _ => {}`, 394 `lm` |-> `\rt v t l. 395 case l of 396 [] => bv_posns (LAM v t) 397 | In::rest => IMAGE (CONS In) (rt rest) 398 | _ => {}`] 399 |> SIMP_RULE (srw_ss()) [] 400 |> CONV_RULE (QUANT_CONV (RAND_CONV (ONCE_REWRITE_CONV [EQ_SYM_EQ]))) 401 402val bv_posns_at_exists = prove( 403 ``?bv_posns_at. 404 ((!s l. bv_posns_at l (VAR s) = {}) /\ 405 (!t u l. bv_posns_at l (t @@ u) = 406 case l of 407 (Lt::rest) => IMAGE (CONS Lt) (bv_posns_at rest t) 408 | (Rt::rest) => IMAGE (CONS Rt) (bv_posns_at rest u) 409 | _ => {}) /\ 410 (!v t l. bv_posns_at l (LAM v t) = 411 case l of 412 [] => bv_posns (LAM v t) 413 | In::rest => IMAGE (CONS In) (bv_posns_at rest t) 414 | _ => {})) /\ 415 !t l p. bv_posns_at l (tpm p t) = bv_posns_at l t``, 416 Q.X_CHOOSE_THEN `f` STRIP_ASSUME_TAC bv_posns_at_exists0 THEN 417 Q.EXISTS_TAC `\l t. f t l` THEN SRW_TAC [][]); 418 419val bv_posns_at_def = new_specification("bv_posns_at_def", ["bv_posns_at"], 420 bv_posns_at_exists) 421 422val bv_posns_at_thm = save_thm("bv_posns_at_thm", CONJUNCT1 bv_posns_at_def) 423 424val bv_posns_at_swap_invariant = Save_Thm( 425 "bv_posns_at_swap_invariant", 426 CONJUNCT2 bv_posns_at_def); 427 428val bv_posns_at_vsubst = Store_Thm( 429 "bv_posns_at_vsubst", 430 ``!t p. bv_posns_at p ([VAR v/u] t) = bv_posns_at p t``, 431 HO_MATCH_MP_TAC nc_INDUCTION2 THEN Q.EXISTS_TAC `{u;v}` THEN 432 SRW_TAC [][SUB_THM, SUB_VAR, v_posns_vsubst, bv_posns_at_thm, 433 bv_posns_thm]) 434 435val bv_posns_at_SUBSET_var_posns = store_thm( 436 "bv_posns_at_SUBSET_var_posns", 437 ``!t p1 p2. p1 IN lam_posns t /\ p2 IN bv_posns_at p1 t ==> 438 p2 IN var_posns t``, 439 HO_MATCH_MP_TAC simple_induction THEN 440 SIMP_TAC (srw_ss()) [lam_posns_thm, var_posns_thm, bv_posns_at_thm, 441 DISJ_IMP_THM, GSYM LEFT_FORALL_IMP_THM, 442 FORALL_AND_THM, RIGHT_AND_OVER_OR, 443 GSYM LEFT_EXISTS_AND_THM, 444 GSYM RIGHT_EXISTS_AND_THM, bv_posns_thm] THEN 445 PROVE_TAC [v_posns_SUBSET_var_posns]); 446 447val lam_posns_subst = store_thm( 448 "lam_posns_subst", 449 ``!t u v. lam_posns ([u/v] t) = lam_posns t UNION 450 {APPEND p1 p2 | p1 IN v_posns v t /\ 451 p2 IN lam_posns u}``, 452 REPEAT GEN_TAC THEN Q.ID_SPEC_TAC `t` THEN 453 HO_MATCH_MP_TAC nc_INDUCTION2 THEN Q.EXISTS_TAC `v INSERT FV u` THEN 454 SIMP_TAC (srw_ss()) [SUB_THM, SUB_VAR, lam_posns_thm, v_posns_thm] THEN 455 REPEAT CONJ_TAC THENL [ 456 SRW_TAC [][EXTENSION], 457 SIMP_TAC (srw_ss() ++ DNF_ss) [EXTENSION] THEN PROVE_TAC [], 458 SRW_TAC [DNF_ss][lam_posns_thm, v_posns_thm, EXTENSION, 459 v_posns_FV] THEN 460 PROVE_TAC [] 461 ]); 462 463val v_posns_subst = store_thm( 464 "v_posns_subst", 465 ``!t u v w. v_posns v ([u/w] t) = 466 if v = w then { APPEND p1 p2 | p1 IN v_posns v t /\ 467 p2 IN v_posns v u} 468 else v_posns v t UNION 469 { APPEND p1 p2 | p1 IN v_posns w t /\ p2 IN v_posns v u}``, 470 REPEAT GEN_TAC THEN Q.ID_SPEC_TAC `t` THEN 471 HO_MATCH_MP_TAC nc_INDUCTION2 THEN Q.EXISTS_TAC `{v;w} UNION FV u` THEN 472 SIMP_TAC (srw_ss()) [SUB_VAR, SUB_THM, v_posns_thm, EXTENSION] THEN 473 REPEAT CONJ_TAC THENL [ 474 REPEAT GEN_TAC THEN REPEAT COND_CASES_TAC THEN 475 REPEAT VAR_EQ_TAC THEN ASM_SIMP_TAC (srw_ss()) [v_posns_thm] THEN 476 FULL_SIMP_TAC (srw_ss()) [], 477 SRW_TAC [DNF_ss][] THEN PROVE_TAC [], 478 SRW_TAC [DNF_ss][] THEN PROVE_TAC [] 479 ]); 480 481val bv_posns_at_subst = store_thm( 482 "bv_posns_at_subst", 483 ``!t u v p. p IN lam_posns t ==> 484 (bv_posns_at p ([v/u] t) = bv_posns_at p t)``, 485 REPEAT GEN_TAC THEN MAP_EVERY Q.ID_SPEC_TAC [`p`, `t`] THEN 486 HO_MATCH_MP_TAC nc_INDUCTION2 THEN Q.EXISTS_TAC `u INSERT FV v` THEN 487 SRW_TAC [][lam_posns_thm, SUB_THM, SUB_VAR, bv_posns_at_thm] THEN 488 SRW_TAC [][lam_posns_thm, SUB_THM, SUB_VAR, bv_posns_at_thm, 489 lam_posns_subst, bv_posns_thm, v_posns_subst, v_posns_FV] THEN 490 SRW_TAC [][EXTENSION]); 491 492val bv_posns_at_subst2 = store_thm( 493 "bv_posns_at_subst2", 494 ``!t u v vp m. 495 vp IN v_posns v t /\ m IN lam_posns u ==> 496 (bv_posns_at (APPEND vp m) ([u/v] t) = 497 IMAGE (APPEND vp) (bv_posns_at m u))``, 498 REPEAT GEN_TAC THEN 499 MAP_EVERY Q.ID_SPEC_TAC [`m`, `vp`, `t`] THEN 500 HO_MATCH_MP_TAC nc_INDUCTION2 THEN 501 Q.EXISTS_TAC `v INSERT FV u` THEN 502 ASM_SIMP_TAC (srw_ss()) [v_posns_thm, SUB_THM, SUB_VAR] THEN 503 REPEAT CONJ_TAC THENL [ 504 SRW_TAC [][EXTENSION], 505 REPEAT STRIP_TAC THENL [ 506 `APPEND x m IN lam_posns ([u/v] t)` 507 by (SRW_TAC [][lam_posns_subst] THEN PROVE_TAC []) THEN 508 SRW_TAC [DNF_ss][bv_posns_at_thm, EXTENSION], 509 `APPEND x m IN lam_posns ([u/v] t')` 510 by (SRW_TAC [][lam_posns_subst] THEN PROVE_TAC []) THEN 511 SRW_TAC [DNF_ss][bv_posns_at_thm, EXTENSION] 512 ], 513 SRW_TAC [][bv_posns_at_thm] THEN SRW_TAC [DNF_ss][EXTENSION] 514 ]); 515 516val bv_posns_at_prefix_posn = store_thm( 517 "bv_posns_at_prefix_posn", 518 ``���p t bvp. p ��� lam_posns t /\ bvp ��� bv_posns_at p t ==> 519 ���m. bvp = p ++ [In] ++ m``, 520 Induct THEN 521 REPEAT GEN_TAC THEN SIMP_TAC (srw_ss()) [bv_posns_at_def] THEN 522 Q.SPEC_THEN `t` STRUCT_CASES_TAC term_CASES THEN 523 ASM_SIMP_TAC (srw_ss() ++ DNF_ss ++ boolSimps.CONJ_ss) 524 [lam_posns_thm, bv_posns_thm, bv_posns_at_thm] THEN 525 PROVE_TAC []); 526 527val v_posns_injective = store_thm( 528 "v_posns_injective", 529 ``!t v1 p. p IN v_posns v1 t ==> (p IN v_posns v2 t <=> (v1 = v2))``, 530 SIMP_TAC (srw_ss() ++ DNF_ss) [EQ_IMP_THM] THEN 531 REPEAT GEN_TAC THEN MAP_EVERY Q.ID_SPEC_TAC [`p`, `t`] THEN 532 HO_MATCH_MP_TAC nc_INDUCTION2 THEN Q.EXISTS_TAC `{v1;v2}` THEN 533 SRW_TAC [][v_posns_thm] THEN PROVE_TAC []); 534 535val v_posns_arent_bv_posns = store_thm( 536 "v_posns_arent_bv_posns", 537 ``!t lp p. lp IN lam_posns t /\ p IN bv_posns_at lp t ==> 538 !v. ~(p IN v_posns v t)``, 539 HO_MATCH_MP_TAC simple_induction THEN 540 SRW_TAC [] [lam_posns_thm, bv_posns_at_thm, v_posns_thm, 541 bv_posns_thm] THEN 542 POP_ASSUM MP_TAC THEN SRW_TAC [][bv_posns_at_thm] THEN 543 PROVE_TAC [v_posns_injective]); 544 545val no_var_posns_in_var_posn_prefix = store_thm( 546 "no_var_posns_in_var_posn_prefix", 547 ``!t p1 l. 548 p1 IN var_posns t /\ APPEND p1 l IN var_posns t ==> (l = [])``, 549 HO_MATCH_MP_TAC simple_induction THEN 550 REWRITE_TAC[var_posns_thm, theorem "var_posns_vsubst_invariant"] THEN 551 REPEAT CONJ_TAC THENL [ 552 SIMP_TAC (srw_ss()) [], 553 REPEAT GEN_TAC THEN STRIP_TAC THEN 554 SIMP_TAC (srw_ss() ++ DNF_ss) [] THEN ASM_REWRITE_TAC [], 555 REPEAT GEN_TAC THEN STRIP_TAC THEN 556 SIMP_TAC (srw_ss() ++ DNF_ss) [] THEN ASM_REWRITE_TAC [] 557 ]); 558 559val APPEND_var_posns = store_thm( 560 "APPEND_var_posns", 561 ``!vp1 vp2 t. 562 vp1 IN var_posns t /\ vp2 IN var_posns t ==> 563 !x y. (APPEND vp1 x = APPEND vp2 y) <=> (vp1 = vp2) /\ (x = y)``, 564 SRW_TAC [][APPEND_CASES, EQ_IMP_THM] THEN 565 PROVE_TAC [no_var_posns_in_var_posn_prefix]); 566 567val valid_posns_subst = store_thm( 568 "valid_posns_subst", 569 ``!t u v. valid_posns ([u/v] t) = 570 valid_posns t UNION 571 {APPEND p1 p2 | p1 IN v_posns v t /\ p2 IN valid_posns u}``, 572 REPEAT GEN_TAC THEN Q.ID_SPEC_TAC `t` THEN 573 HO_MATCH_MP_TAC nc_INDUCTION2 THEN Q.EXISTS_TAC `v INSERT FV u` THEN 574 SRW_TAC [][valid_posns_thm, v_posns_thm, SUB_THM] THENL [ 575 SIMP_TAC (srw_ss() ++ DNF_ss)[EXTENSION, EQ_IMP_THM], 576 SRW_TAC [][EXTENSION] THEN REPEAT (POP_ASSUM (K ALL_TAC)) THEN 577 SRW_TAC [DNF_ss][] THEN PROVE_TAC [], 578 SRW_TAC [DNF_ss][EXTENSION] THEN PROVE_TAC [] 579 ]); 580 581val cant_be_deeper_than_var_posns = store_thm( 582 "cant_be_deeper_than_var_posns", 583 ``!t p1 p. p1 IN var_posns t /\ APPEND p1 p IN valid_posns t ==> 584 (p = [])``, 585 HO_MATCH_MP_TAC simple_induction THEN REPEAT CONJ_TAC THENL [ 586 SRW_TAC [][var_posns_thm, valid_posns_thm], 587 REPEAT GEN_TAC THEN STRIP_TAC THEN 588 SIMP_TAC (srw_ss() ++ DNF_ss) [var_posns_thm, valid_posns_thm] THEN 589 ASM_REWRITE_TAC [], 590 REPEAT GEN_TAC THEN STRIP_TAC THEN 591 SIMP_TAC (srw_ss() ++ DNF_ss) [var_posns_thm, valid_posns_thm] THEN 592 PROVE_TAC [lemma14a] 593 ]); 594 595val NIL_IN_v_posns = store_thm( 596 "NIL_IN_v_posns", 597 ``!t v. [] IN v_posns v t <=> (t = VAR v)``, 598 GEN_TAC THEN 599 Q.SPEC_THEN `t` STRUCT_CASES_TAC term_CASES THEN 600 SRW_TAC [][v_posns_thm, v_posns_LAM_COND]); 601 602val v_posns_FINITE = Store_Thm( 603 "v_posns_FINITE", 604 ``!v t. FINITE (v_posns v t)``, 605 PROVE_TAC [v_posns_SUBSET_var_posns, var_posns_FINITE, 606 pred_setTheory.SUBSET_FINITE, pred_setTheory.SUBSET_DEF]); 607 608val _ = export_theory() 609 610