1open HolKernel Parse boolLib bossLib ramanaLib relationTheory pairTheory bagTheory prim_recTheory finite_mapTheory substTheory termTheory walkTheory 2 3val _ = new_theory "walkstar" 4 5val pre_walkstar_def = TotalDefn.xDefineSchema "pre_walkstar" 6 `walkstar t = 7 case walk s t 8 of Pair t1 t2 => Pair (walkstar t1) (walkstar t2) 9 | w => w`; 10 11val _ = overload_on("walk*",``walkstar``) 12 13val _ = add_rule {block_style = (AroundEachPhrase, (PP.CONSISTENT, 0)), 14 paren_style = OnlyIfNecessary, 15 pp_elements = [HardSpace 1, TOK "���", BreakSpace(1,0)], 16 term_name = "walk*", 17 fixity = Infixr 700} 18 19val walkstarR_def = Define 20`walkstarR s = inv_image ((LEX) (mlt1 (vR s)^+)^+ (measure pair_count)) (\t. (varb t, t))`; 21 22val [h2,h1,hWF] = hyp pre_walkstar_def; 23val _ = store_term_thm ("walkstar_hWF", hWF); 24val _ = store_term_thm ("walkstar_h1", h1); 25val _ = store_term_thm ("walkstar_h2", h2); 26val _ = store_term_thm ("walkstar_def_print", 27TermWithCase` 28wfs s ��� 29(walk* s t = 30 case walk s t 31 of Pair t1 t2 => Pair (walk* s t1) (walk* s t2) 32 | t' => t')`) 33 34val inst_walkstar = Q.INST [`R` |-> `walkstarR s`] 35 36val [h2,h1,h3] = hyp (inst_walkstar pre_walkstar_def) 37 38val th1 = Q.store_thm("walkstar_th1",`wfs s ��� ^h1`, 39SRW_TAC [][inv_image_def,LEX_DEF,walkstarR_def] THEN 40Q.PAT_X_ASSUM `wfs s` ASSUME_TAC THEN 41Cases_on `t` THEN FULL_SIMP_TAC (srw_ss()) [] THENL [ 42 MATCH_MP_TAC TC_SUBSET THEN 43 SRW_TAC [][mlt1_def] THEN 44 MAP_EVERY Q.EXISTS_TAC [`n`,`varb t1`,`{||}`] THEN 45 SRW_TAC [][vwalk_vR], 46 REPEAT (Q.PAT_X_ASSUM `X = Y` (K ALL_TAC)) THEN 47 Cases_on `varb t2 = {||}` THEN1 48 SRW_TAC [ARITH_ss][measure_thm] THEN 49 DISJ1_TAC THEN MATCH_MP_TAC TC_mlt1_UNION2_I THEN 50 SRW_TAC [][] 51]); 52 53val th2 = Q.store_thm("walkstar_th2",`wfs s ��� ^h2`, 54SRW_TAC [][inv_image_def,LEX_DEF,walkstarR_def] THEN 55Q.PAT_X_ASSUM `wfs s` ASSUME_TAC THEN 56Cases_on `t` THEN FULL_SIMP_TAC (srw_ss()) [] THENL [ 57 MATCH_MP_TAC TC_SUBSET THEN 58 SRW_TAC [][mlt1_def] THEN 59 MAP_EVERY Q.EXISTS_TAC [`n`,`varb t2`,`{||}`] THEN 60 SRW_TAC [][vwalk_vR], 61 REPEAT (Q.PAT_X_ASSUM `X = Y` (K ALL_TAC)) THEN 62 Cases_on `varb t1 = {||}` THEN1 63 SRW_TAC [ARITH_ss][measure_thm] THEN 64 DISJ1_TAC THEN 65 Q.MATCH_ABBREV_TAC `(mlt1 R)^+ b2 (b1 + b2)` THEN 66 Q_TAC SUFF_TAC `(mlt1 R)^+ b2 (b2 + b1)` THEN1 67 METIS_TAC [COMM_BAG_UNION] THEN 68 MATCH_MP_TAC TC_mlt1_UNION2_I THEN 69 UNABBREV_ALL_TAC THEN 70 SRW_TAC [][] 71]); 72 73val th3 = Q.store_thm("walkstar_thWF",`wfs s ��� ^h3`, 74SRW_TAC [][wfs_def,walkstarR_def] THEN 75MATCH_MP_TAC WF_inv_image THEN 76SRW_TAC [][WF_TC, WF_LEX, WF_mlt1]); 77 78fun walkstar_wfs_hyp th = 79 th |> 80 PROVE_HYP (UNDISCH th1) |> 81 PROVE_HYP (UNDISCH th2) |> 82 PROVE_HYP (UNDISCH th3); 83 84val walkstar_def = save_thm("walkstar_def",DISCH_ALL(walkstar_wfs_hyp (inst_walkstar pre_walkstar_def))); 85val walkstar_ind = save_thm("walkstar_ind",walkstar_wfs_hyp (inst_walkstar (theorem "pre_walkstar_ind"))); 86 87val walkstar_thm = RWsave_thm( 88 "walkstar_thm", 89[walkstar_def |> UNDISCH |> Q.SPEC `Var v` |> SIMP_RULE (srw_ss()) [], 90 walkstar_def |> UNDISCH |> Q.SPEC `Pair t1 t2` |> SIMP_RULE (srw_ss()) [], 91 walkstar_def |> UNDISCH |> Q.SPEC `Const c` |> SIMP_RULE (srw_ss()) []] 92|> LIST_CONJ |> DISCH_ALL); 93 94val walkstar_FEMPTY = RWstore_thm( 95"walkstar_FEMPTY", 96`!t.(walk* FEMPTY t = t)`, 97ASSUME_TAC wfs_FEMPTY THEN 98HO_MATCH_MP_TAC (Q.INST[`s`|->`FEMPTY`]walkstar_ind) THEN 99Cases_on `t` THEN SRW_TAC [][]); 100 101val NOT_FDOM_walkstar = Q.store_thm( 102"NOT_FDOM_walkstar", 103`wfs s ==> !t. v NOTIN FDOM s ==> v IN vars t ==> v IN vars (walk* s t)`, 104DISCH_TAC THEN HO_MATCH_MP_TAC walkstar_ind THEN SRW_TAC [][] THEN Cases_on `t` THENL [ 105 Q.PAT_X_ASSUM `wfs s` ASSUME_TAC THEN 106 FULL_SIMP_TAC (srw_ss()) [Once vwalk_def, vars_def, FLOOKUP_DEF], 107 Q.PAT_X_ASSUM `wfs s` ASSUME_TAC THEN FULL_SIMP_TAC (srw_ss()) [], 108 FULL_SIMP_TAC (srw_ss()) [vars_def]]); 109 110val vwalk_EQ_var_vR = prove( 111 ``wfs s ==> !u v1 v2. (vwalk s u = Var v1) /\ (vR s)^+ v2 u /\ 112 v2 NOTIN FDOM s ==> (v1 = v2)``, 113 STRIP_TAC THEN HO_MATCH_MP_TAC vwalk_ind THEN SRW_TAC [][] THEN 114 IMP_RES_TAC TC_CASES2 THEN 115 FULL_SIMP_TAC (srw_ss()) [vR_def] THEN 116 Cases_on `FLOOKUP s u` THEN FULL_SIMP_TAC (srw_ss()) [] THEN 117 Q.PAT_X_ASSUM `vwalk s u = UU` MP_TAC THEN 118 SRW_TAC [][Once vwalk_def] THEN 119 Cases_on `x` THEN FULL_SIMP_TAC (srw_ss()) [] THEN 120 POP_ASSUM MP_TAC THEN SRW_TAC [][NOT_FDOM_vwalk]); 121 122val vwalk_EQ_const_vR = prove( 123 ``!v u. (vR s)^+ v u ==> v NOTIN FDOM s /\ wfs s ==> 124 !c. vwalk s u <> Const c``, 125 HO_MATCH_MP_TAC TC_INDUCT_RIGHT1 THEN SRW_TAC [][] THENL [ 126 FULL_SIMP_TAC (srw_ss()) [vR_def] THEN 127 Cases_on `FLOOKUP s u` THEN FULL_SIMP_TAC (srw_ss()) [] THEN 128 SRW_TAC [][Once vwalk_def] THEN Cases_on `x` THEN 129 FULL_SIMP_TAC (srw_ss()) [] THEN SRW_TAC [][NOT_FDOM_vwalk], 130 FULL_SIMP_TAC (srw_ss()) [vR_def] THEN 131 Cases_on `FLOOKUP s u'` THEN FULL_SIMP_TAC (srw_ss()) [] THEN 132 SRW_TAC [][Once vwalk_def] THEN Cases_on `x` THEN 133 FULL_SIMP_TAC (srw_ss()) [] THEN SRW_TAC [][NOT_FDOM_vwalk] 134 ]); 135 136val vwalk_EQ_pair_vR = prove( 137 ``!v u. (vR s)^+ v u ==> 138 !t1 t2. v NOTIN FDOM s /\ wfs s /\ (vwalk s u = Pair t1 t2) ==> 139 ?u. (u IN vars t1 \/ u IN vars t2) /\ (vR s)^* v u``, 140 HO_MATCH_MP_TAC TC_STRONG_INDUCT_RIGHT1 THEN SRW_TAC [][] THEN 141 FULL_SIMP_TAC (srw_ss()) [vR_def] THENL [ 142 Cases_on `FLOOKUP s u` THEN FULL_SIMP_TAC (srw_ss()) [] THEN 143 Q.PAT_X_ASSUM `vwalk s u = XXX` MP_TAC THEN 144 SRW_TAC [][Once vwalk_def] THEN 145 Cases_on `x` THEN FULL_SIMP_TAC (srw_ss()) [] THENL [ 146 POP_ASSUM MP_TAC THEN SRW_TAC [][NOT_FDOM_vwalk], 147 Q.EXISTS_TAC `v` THEN SRW_TAC [][], 148 Q.EXISTS_TAC `v` THEN SRW_TAC [][] 149 ], 150 Cases_on `FLOOKUP s u'` THEN FULL_SIMP_TAC (srw_ss()) [] THEN 151 Q.PAT_X_ASSUM `vwalk s u' = XXX` MP_TAC THEN 152 SRW_TAC [][Once vwalk_def] THEN 153 Cases_on `x` THEN FULL_SIMP_TAC (srw_ss()) [] THEN METIS_TAC [TC_RTC] 154 ]); 155 156val TC_vR_vars_walkstar = store_thm( 157 "TC_vR_vars_walkstar", 158 ``wfs s /\ u IN vars t /\ (vR s)^+ v u /\ v NOTIN FDOM s ==> 159 v IN vars (walk* s t)``, 160 Q_TAC SUFF_TAC 161 `wfs s ==> 162 !t v u. (vR s)^+ v u /\ v NOTIN FDOM s /\ u IN vars t ==> 163 v IN vars (walk* s t)` 164 THEN1 METIS_TAC [] THEN 165 STRIP_TAC THEN HO_MATCH_MP_TAC walkstar_ind THEN 166 SRW_TAC [][] THEN Cases_on `t` THENL [ 167 Q.MATCH_ABBREV_TAC `v IN vars (walk* s (Var s'))` THEN 168 FULL_SIMP_TAC (srw_ss()) [] THEN SRW_TAC [][] THEN 169 Cases_on `vwalk s s'` THEN SRW_TAC [][] THENL [ 170 METIS_TAC [vwalk_EQ_var_vR], 171 `?u. u IN vars (Pair t t0) /\ (vR s)^* v u` 172 by (SRW_TAC [][] THEN METIS_TAC [vwalk_EQ_pair_vR]) THEN 173 `(u = v) \/ (vR s)^+ v u` 174 by METIS_TAC [EXTEND_RTC_TC_EQN, RTC_CASES1] THEN1 175 FULL_SIMP_TAC (srw_ss()) [NOT_FDOM_walkstar] THEN 176 FULL_SIMP_TAC (srw_ss()) [] THEN METIS_TAC [], 177 METIS_TAC [vwalk_EQ_const_vR] 178 ], 179 FULL_SIMP_TAC (srw_ss()) [] THEN METIS_TAC [], 180 FULL_SIMP_TAC (srw_ss()) [] 181 ]); 182 183val walkstar_SUBMAP = Q.store_thm( 184"walkstar_SUBMAP", 185`s SUBMAP sx ��� wfs sx ��� (walk* sx t = walk* sx (walk* s t))`, 186STRIP_TAC THEN IMP_RES_TAC wfs_SUBMAP THEN 187Q.ID_SPEC_TAC `t` THEN 188HO_MATCH_MP_TAC walkstar_ind THEN 189SRW_TAC [][] THEN 190Q.PAT_X_ASSUM `wfs s` ASSUME_TAC THEN 191FULL_SIMP_TAC (srw_ss()) [] THEN 192Cases_on `t` THEN SRW_TAC [][] THEN 193Q.SPECL_THEN [`n`,`s`] MP_TAC (UNDISCH vwalk_SUBMAP) THEN 194Cases_on `vwalk s n` THEN SRW_TAC [][]) 195 196val walkstar_idempotent = Q.store_thm( 197"walkstar_idempotent", 198`wfs s ==> !t.(walk* s t = walk* s (walk* s t))`, 199METIS_TAC [walkstar_SUBMAP,SUBMAP_REFL]) 200 201val walkstar_subterm_idem = Q.store_thm( 202"walkstar_subterm_idem", 203`(walk* s t1 = Pair t1a t1d) ��� wfs s ��� 204 (walk* s t1a = t1a) ��� 205 (walk* s t1d = t1d)`, 206SRW_TAC [][] THEN 207IMP_RES_TAC walkstar_idempotent THEN 208POP_ASSUM (Q.SPEC_THEN `t1` MP_TAC) THEN 209FULL_SIMP_TAC (srw_ss()) []) 210 211val walkstar_walk = Q.store_thm( 212"walkstar_walk", 213`wfs s ==> (walk* s (walk s t) = walk* s t)`, 214Cases_on `t` THEN SRW_TAC [][] THEN SRW_TAC [][] THEN 215Cases_on `vwalk s n` THEN SRW_TAC [][] THEN 216`vwalk s n' = Var n'` by METIS_TAC [vwalk_to_var,NOT_FDOM_vwalk] THEN 217SRW_TAC [][]) 218 219val walkstar_to_var = Q.store_thm( 220"walkstar_to_var", 221`(walk* s t = (Var v)) ��� wfs s ��� v NOTIN (FDOM s) ��� ���u.t = Var u`, 222REVERSE (SRW_TAC [][]) THEN1 223(Cases_on `t` THEN FULL_SIMP_TAC (srw_ss()) []) THEN 224IMP_RES_TAC walkstar_idempotent THEN 225POP_ASSUM (Q.SPEC_THEN `t` MP_TAC) THEN 226ASM_SIMP_TAC (srw_ss()) [] THEN 227Cases_on `vwalk s v` THEN SRW_TAC [][] THEN 228METIS_TAC [vwalk_to_var]) 229 230open pred_setTheory; 231 232(* direct version of walkstar that does the walk itself *) 233 234val apply_ts_thm = Q.store_thm( 235"apply_ts_thm", 236`wfs s ��� 237 (walk* s (Var v) = 238 case FLOOKUP s v of NONE => (Var v) 239 | SOME t => walk* s t) ��� 240 (walk* s (Pair t1 t2) = Pair (walk* s t1) (walk* s t2)) ��� 241 (walk* s (Const c) = Const c)`, 242SIMP_TAC (srw_ss()) [] THEN STRIP_TAC THEN 243Q.ID_SPEC_TAC `v` THEN 244HO_MATCH_MP_TAC vwalk_ind THEN 245SRW_TAC [][] THEN 246Cases_on `FLOOKUP s v` THEN SRW_TAC [][Once vwalk_def] THEN 247Cases_on `x` THEN SRW_TAC [][]); 248 249val apply_ts_ind = save_thm( 250"apply_ts_ind", 251UNDISCH (Q.prove( 252`wfs s ��� 253 ���P. (���v. (���t. (FLOOKUP s v = SOME t) ��� P t) ��� P (Var v)) ��� 254 (���t1 t2. P t1 ��� P t2 ��� P (Pair t1 t2)) ��� (���c. P (Const c)) ��� 255 ���v. P v`, 256SRW_TAC [][] THEN 257Q.ID_SPEC_TAC `v` THEN 258HO_MATCH_MP_TAC walkstar_ind THEN 259STRIP_TAC THEN Cases_on `t` THEN 260SRW_TAC [][] THEN 261NTAC 2 (POP_ASSUM MP_TAC) THEN 262Q.ID_SPEC_TAC `n` THEN 263HO_MATCH_MP_TAC vwalk_ind THEN 264SRW_TAC [][] THEN 265Cases_on `FLOOKUP s n` THEN FULL_SIMP_TAC (srw_ss()) [] THEN 266Q.PAT_X_ASSUM `wfs s` ASSUME_TAC THEN 267FULL_SIMP_TAC (srw_ss()) [Once vwalk_def] THEN 268Cases_on `x` THEN FULL_SIMP_TAC (srw_ss()) [] THEN 269Q_TAC SUFF_TAC `���t. (FLOOKUP s n = SOME t) ��� P t` THEN1 METIS_TAC [] THEN 270SRW_TAC [][] THEN 271Q.PAT_X_ASSUM `���t1 t2. X ��� P t2` MP_TAC THEN 272SRW_TAC [][Once vwalk_def]))); 273 274val vars_walkstar = Q.store_thm( 275"vars_walkstar", 276`wfs s ��� ���t. vars (walkstar s t) SUBSET vars t UNION BIGUNION (FRANGE (vars o_f s))`, 277STRIP_TAC THEN HO_MATCH_MP_TAC apply_ts_ind THEN 278SRW_TAC [][apply_ts_thm] THENL [ 279 Cases_on `FLOOKUP s t` THEN SRW_TAC [][] THEN 280 `vars x SUBSET BIGUNION (FRANGE (vars o_f s))` 281 by (MATCH_MP_TAC SUBSET_BIGUNION_I THEN 282 MATCH_MP_TAC o_f_FRANGE THEN 283 METIS_TAC [FRANGE_FLOOKUP]) THEN 284 MATCH_MP_TAC SUBSET_TRANS THEN 285 Q.EXISTS_TAC `vars x UNION BIGUNION (FRANGE (vars o_f s))` THEN SRW_TAC [][] THEN 286 MATCH_MP_TAC SUBSET_TRANS THEN 287 Q.EXISTS_TAC `BIGUNION (FRANGE (vars o_f s))` THEN SRW_TAC [][], 288 MATCH_MP_TAC SUBSET_TRANS THEN 289 Q.EXISTS_TAC `vars t UNION BIGUNION (FRANGE (vars o_f s))` THEN 290 SRW_TAC [][] THEN 291 METIS_TAC [SUBSET_UNION,UNION_ASSOC], 292 MATCH_MP_TAC SUBSET_TRANS THEN 293 Q.EXISTS_TAC `vars t' UNION BIGUNION (FRANGE (vars o_f s))` THEN 294 SRW_TAC [][] THEN 295 METIS_TAC [SUBSET_UNION,UNION_ASSOC,UNION_COMM] 296]); 297 298(* occurs check, which is (proved) equivalent to vars o walkstar *) 299 300val (oc_rules, oc_ind, oc_cases) = Hol_reln` 301 (!t v. v IN vars t /\ v NOTIN FDOM s ==> oc s t v) /\ 302 (!t v u t'. u IN vars t /\ (vwalk s u = t') /\ oc s t' v ==> 303 oc s t v)`; 304 305val oc_strong_ind = 306 save_thm("oc_strong_ind",IndDefLib.derive_strong_induction(oc_rules, oc_ind)); 307 308val oc_pair_E0 = prove( 309 ``!t v. oc s t v ==> 310 !t1 t2. (t = Pair t1 t2) ==> oc s t1 v \/ oc s t2 v``, 311 HO_MATCH_MP_TAC oc_strong_ind THEN CONJ_TAC THENL [ 312 METIS_TAC [IN_UNION, vars_def, oc_rules], 313 ALL_TAC 314 ] THEN 315 SRW_TAC [][] THEN FULL_SIMP_TAC (srw_ss()) [] THEN 316 METIS_TAC [oc_rules]); 317 318val oc_pair_E = SIMP_RULE (srw_ss() ++ boolSimps.DNF_ss) [] oc_pair_E0; 319 320val oc_pair_I = Q.prove( 321 `(!t1. oc s t1 v ==> oc s (Pair t1 t2) v) /\ 322 (!t2. oc s t2 v ==> oc s (Pair t1 t2) v)`, 323 REPEAT STRIP_TAC THEN 324 POP_ASSUM (MP_TAC o ONCE_REWRITE_RULE [oc_cases]) THEN 325 SRW_TAC [][] THEN 326 METIS_TAC [vars_def, IN_UNION, oc_rules]); 327 328val oc_pair = Q.prove( 329 `oc s (Pair t1 t2) v = oc s t1 v \/ oc s t2 v`, 330 METIS_TAC [oc_pair_E, oc_pair_I]); 331 332val oc_const = Q.prove( 333 `~oc s (Const c) v`, 334 ONCE_REWRITE_TAC [oc_cases] THEN SRW_TAC [][]); 335 336val oc_var1 = Q.prove( 337 `!t v. oc s t v ==> 338 !u. (t = Var u) /\ wfs s ==> 339 case vwalk s u of 340 Var u => (v = u) 341 | Pair t1 t2 => oc s t1 v \/ oc s t2 v 342 | _ => F`, 343 HO_MATCH_MP_TAC oc_strong_ind THEN SRW_TAC [][] 344 THEN1 (FULL_SIMP_TAC (srw_ss())[] THEN SRW_TAC [][Once vwalk_def,FLOOKUP_DEF]) THEN 345 FULL_SIMP_TAC (srw_ss()) [] THEN SRW_TAC [][] THEN 346 Cases_on `vwalk s u` THEN FULL_SIMP_TAC (srw_ss()) [oc_pair,oc_const] THEN 347 Q.MATCH_ABBREV_TAC `v = n` THEN 348 `vwalk s n = Var n` by METIS_TAC [vwalk_to_var,NOT_FDOM_vwalk] THEN 349 FULL_SIMP_TAC (srw_ss()) []); 350 351val oc2 = CONJUNCT2 (SIMP_RULE bool_ss [FORALL_AND_THM] oc_rules); 352 353val oc_var2 = Q.prove( 354 `wfs s ==> !v u. 355 (case vwalk s v of 356 Var u => (x = u) 357 | Pair t1 t2 => oc s t1 x \/ oc s t2 x 358 | _ => F) ==> oc s (Var v) x`, 359 DISCH_TAC THEN HO_MATCH_MP_TAC vwalk_ind THEN SRW_TAC [][] THEN 360 Cases_on `vwalk s v` THEN 361 FULL_SIMP_TAC (srw_ss()) [] THENL [ 362 MATCH_MP_TAC oc2 THEN SRW_TAC [][] THEN 363 Q.MATCH_ABBREV_TAC `oc s (Var n) n` THEN 364 `n NOTIN FDOM s` by METIS_TAC [vwalk_to_var,NOT_FDOM_vwalk] THEN 365 METIS_TAC [oc_rules, vars_def, IN_INSERT], 366 MATCH_MP_TAC oc2 THEN SRW_TAC [][oc_pair], 367 MATCH_MP_TAC oc2 THEN SRW_TAC [][oc_pair]]); 368 369val oc_var = Q.prove( 370 `wfs s ==> (oc s (Var v) x = 371 case vwalk s v of 372 Var u => (x = u) 373 | Pair t1 t2 => oc s t1 x \/ oc s t2 x 374 | _ => F)`, 375 METIS_TAC [oc_var2, oc_var1]); 376 377val oc_thm = RWsave_thm("oc_thm", LIST_CONJ [oc_var, oc_pair, oc_const]); 378 379val oc_def_q = 380`wfs s ��� 381 (oc s t v = 382 case walk s t of 383 Var u => (v = u) 384 | Pair t1 t2 => oc s t1 v ��� oc s t2 v 385 | _ => F)`; 386 387val oc_walking = Q.store_thm( 388"oc_walking", oc_def_q, 389Induct_on `t` THEN SRW_TAC [][]) 390 391val _ = store_term_thm("oc_def_print",TermWithCase oc_def_q); 392 393val oc_if_vars_walkstar = Q.prove( 394`wfs s ==> !t. vars (walk* s t) v ==> oc s t v`, 395DISCH_TAC THEN HO_MATCH_MP_TAC walkstar_ind THEN SRW_TAC [] [] THEN 396Cases_on `t` THENL [ 397 Cases_on `walk* s (Var n)` THEN Q.PAT_X_ASSUM `wfs s` ASSUME_TAC 398 THENL [ 399 `v = n'` by METIS_TAC [vars_def,IN_DEF,IN_INSERT,NOT_IN_EMPTY] THEN 400 Cases_on `vwalk s n` THEN FULL_SIMP_TAC (srw_ss()) [], 401 Cases_on `vwalk s n` THEN FULL_SIMP_TAC (srw_ss()) [] THEN 402 METIS_TAC [IN_UNION,IN_DEF], 403 FULL_SIMP_TAC (srw_ss()) [] THEN `v IN {}` by METIS_TAC [IN_DEF] 404 THEN FULL_SIMP_TAC (srw_ss()) [NOT_IN_EMPTY] 405 ], 406 Q.PAT_X_ASSUM `vars (walkstar s t) v` MP_TAC THEN SRW_TAC [][] THEN 407 Q.PAT_X_ASSUM `wfs s` ASSUME_TAC THEN FULL_SIMP_TAC (srw_ss()) [] THEN 408 METIS_TAC [IN_DEF,IN_UNION], 409 Q.PAT_X_ASSUM `wfs s` ASSUME_TAC THEN 410 FULL_SIMP_TAC (srw_ss()) [] THEN 411 METIS_TAC [IN_DEF,NOT_IN_EMPTY]]); 412 413val oc_NOTIN_FDOM = Q.store_thm( 414 "oc_NOTIN_FDOM", 415 `wfs s ==> !t v. oc s t v ==> v NOTIN FDOM s`, 416 STRIP_TAC THEN HO_MATCH_MP_TAC oc_ind THEN SRW_TAC [] []); 417 418val vars_walkstar_if_oc = Q.prove( 419`wfs s ==> !t v. oc s t v ==> v IN vars (walkstar s t)`, 420STRIP_TAC THEN HO_MATCH_MP_TAC oc_strong_ind THEN SRW_TAC [] [] THEN1 421 METIS_TAC [NOT_FDOM_walkstar] THEN 422Induct_on `t` THEN SRW_TAC [][] THENL [ 423 Cases_on `vwalk s n` THEN SRW_TAC [][] THEN 424 Q.PAT_X_ASSUM `Y IN vars X` MP_TAC THEN 425 ASM_SIMP_TAC (srw_ss()) [] THEN 426 `vwalk s n' = Var n'` by METIS_TAC [vwalk_to_var,NOT_FDOM_vwalk] THEN 427 SRW_TAC [][], 428 METIS_TAC [], 429 METIS_TAC [] 430]); 431 432val oc_eq_vars_walkstar = Q.store_thm( 433 "oc_eq_vars_walkstar", 434 `wfs s ==> (oc s t v ��� v ��� vars (walkstar s t))`, 435 SRW_TAC [][FUN_EQ_THM] THEN 436 METIS_TAC [vars_walkstar_if_oc,oc_if_vars_walkstar,IN_DEF]); 437 438val _ = export_theory (); 439