1open HolKernel boolLib bossLib Parse pred_setTheory finite_mapTheory 2prim_recTheory relationTheory pairTheory bagTheory apply_piTheory 3ntermTheory nsubstTheory nwalkTheory nomsetTheory listTheory 4ramanaLib ntermLib 5 6val _ = new_theory "nwalkstar" 7 8val (noc_rules, noc_ind, noc_cases) = Hol_reln` 9 (v IN nvars t /\ v NOTIN FDOM s ==> noc s t v) /\ 10 (u IN nvars t /\ (nvwalk s [] u = t') /\ noc s t' v ==> 11 noc s t v)` 12 13val noc2 = CONJUNCT2 (SIMP_RULE bool_ss [FORALL_AND_THM] noc_rules) 14 15val noc_strong_ind = 16 save_thm("noc_strong_ind",IndDefLib.derive_strong_induction(noc_rules, noc_ind)) 17 18val noc_pair_E0 = Q.prove( 19 `!t v. noc s t v ==> 20 !t1 t2. (t = nPair t1 t2) ==> noc s t1 v \/ noc s t2 v`, 21 HO_MATCH_MP_TAC noc_strong_ind THEN 22 SRW_TAC [][] THEN FULL_SIMP_TAC (srw_ss()) [noc_rules] THEN 23 METIS_TAC [noc_rules]) 24 25val noc_pair_E = SIMP_RULE (srw_ss() ++ boolSimps.DNF_ss) [] noc_pair_E0 26 27val noc_pair_I = Q.prove( 28 `(!t1. noc s t1 v ==> noc s (nPair t1 t2) v) /\ 29 (!t2. noc s t2 v ==> noc s (nPair t1 t2) v)`, 30 REPEAT STRIP_TAC THEN 31 POP_ASSUM (MP_TAC o ONCE_REWRITE_RULE [noc_cases]) THEN 32 SRW_TAC [][] THEN 33 METIS_TAC [nvars_def, IN_UNION, noc_rules]) 34 35val noc_pair = Q.prove( 36 `noc s (nPair t1 t2) v = noc s t1 v \/ noc s t2 v`, 37 METIS_TAC [noc_pair_E, noc_pair_I]) 38 39val noc_const = Q.prove( 40 `~noc s (nConst c) v`, 41 ONCE_REWRITE_TAC [noc_cases] THEN SRW_TAC [][]) 42 43val noc_nom = Q.prove( 44 `~noc s (Nom a) v`, 45 ONCE_REWRITE_TAC [noc_cases] THEN SRW_TAC [][]) 46 47val noc_tie = Q.prove( 48 `noc s (Tie a t) v = noc s t v`, 49 ONCE_REWRITE_TAC [noc_cases] THEN SRW_TAC [][]) 50 51val noc_var1 = Q.prove( 52 `!t v. noc s t v ==> 53 !p u. (t = Sus p u) /\ nwfs s ==> 54 case nvwalk s [] u 55 of Sus p v1 => (v1 = v) 56 | Tie a t => noc s t v 57 | nPair t1 t2 => noc s t1 v ��� noc s t2 v 58 | _ => F`, 59 HO_MATCH_MP_TAC noc_strong_ind THEN SRW_TAC [][] 60 THEN1 (FULL_SIMP_TAC (srw_ss())[] THEN 61 SRW_TAC [][Once nvwalk_def,FLOOKUP_DEF]) THEN 62 FULL_SIMP_TAC (srw_ss()) [] THEN SRW_TAC [][] THEN 63 Cases_on `nvwalk s [] u` THEN 64 FULL_SIMP_TAC (srw_ss()) [noc_pair,noc_const,noc_nom,noc_tie] THEN 65 `nvwalk s [] n = Sus [] n` by METIS_TAC [nvwalk_to_var,NOT_FDOM_nvwalk] THEN 66 FULL_SIMP_TAC (srw_ss()) []) 67 68val noc_var2 = Q.prove( 69 `nwfs s ==> !pn v. (pn = []) ��� 70 (case nvwalk s pn v 71 of Sus p u => (x = u) 72 | Tie a t => noc s t x 73 | nPair t1 t2 => noc s t1 x ��� noc s t2 x 74 | _ => F) ��� 75 noc s (Sus p v) x`, 76 DISCH_TAC THEN HO_MATCH_MP_TAC nvwalk_ind THEN SRW_TAC [][] THEN 77 Cases_on `nvwalk s [] v` THEN FULL_SIMP_TAC (srw_ss()) [] THENL [ 78 MATCH_MP_TAC noc2 THEN SRW_TAC [][] THEN 79 `n NOTIN FDOM s` by METIS_TAC [nvwalk_to_var,NOT_FDOM_nvwalk] THEN 80 METIS_TAC [noc_rules, nvars_def, IN_INSERT], 81 MATCH_MP_TAC noc2 THEN SRW_TAC [][noc_tie], 82 MATCH_MP_TAC noc2 THEN SRW_TAC [][noc_pair], 83 MATCH_MP_TAC noc2 THEN SRW_TAC [][noc_pair]]) 84 85val noc_var = Q.prove( 86 `nwfs s ==> (noc s (Sus p v) x = 87 case nvwalk s [] v 88 of Sus p u => (x = u) 89 | Tie a t => noc s t x 90 | nPair t1 t2 => noc s t1 x ��� noc s t2 x 91 | _ => F)`, 92SRW_TAC [][EQ_IMP_THM] THENL [ 93 (noc_var1 |> 94 Q.SPECL [`Sus p v`,`x`] |> 95 SIMP_RULE (srw_ss()) [] |> 96 UNDISCH |> 97 Q.SPEC `p` |> 98 SIMP_RULE (srw_ss()) [] |> 99 DISCH_ALL |> 100 ASSUME_TAC) THEN 101 Cases_on `nvwalk s [] v` THEN FULL_SIMP_TAC (srw_ss()) [], 102 (noc_var2 |> 103 UNDISCH |> 104 Q.SPECL [`[]`,`v`] |> 105 SIMP_RULE (srw_ss()) [] |> 106 MATCH_MP_TAC) THEN 107 Cases_on `nvwalk s [] v` THEN FULL_SIMP_TAC (srw_ss()) [] 108]) 109 110val noc_thm = RWsave_thm("noc_thm", LIST_CONJ [noc_nom, noc_var, noc_tie, noc_pair, noc_const]) 111 112val pre_nwalkstar_def = TotalDefn.xDefineSchema "pre_nwalkstar" 113`nwalkstar t = case nwalk s t 114 of Tie a t => Tie a (nwalkstar t) 115 | nPair t1 t2 => nPair (nwalkstar t1) (nwalkstar t2) 116 | t => t`; 117 118val _ = overload_on("nwalk*",``nwalkstar``) 119 120val _ = add_rule {block_style = (AroundEachPhrase, (PP.CONSISTENT, 0)), 121 paren_style = OnlyIfNecessary, 122 pp_elements = [HardSpace 1, TOK "n���", BreakSpace(1,0)], 123 term_name = "nwalk*", 124 fixity = Infixr 700}; 125 126val _ = store_term_thm("nwalkstar_def_print", TermWithCase 127`nwfs s ��� 128(nwalk* s t = case nwalk s t 129 of Tie a t => Tie a (nwalk* s t) 130 | nPair t1 t2 => nPair (nwalk* s t1) (nwalk* s t2) 131 | t => t)`); 132 133val _ = overload_on("npair_count", ``nterm_size ARB``) 134 135fun inst_nwalkstar th = 136Q.INST [`R` |-> `inv_image ((LEX) (mlt1 (nvR s)^+)^+ (measure npair_count)) 137 (��t. (nvarb t, t))`] th 138 139val [h3,h1,h2,h4] = hyp (inst_nwalkstar pre_nwalkstar_def) 140 141val th1 = Q.prove(`nwfs s ��� ^(h1)`, 142STRIP_TAC THEN REPEAT GEN_TAC THEN 143SIMP_TAC (srw_ss()) [inv_image_def,LEX_DEF] THEN 144Cases_on `t` THEN SRW_TAC [][] THENL [ 145 `���u. u IN nvars (nPair t1 t2) ��� (nvR s)^+ u n` 146 by METIS_TAC [nvwalk_nvR,ntermeq_thm] THEN 147 MATCH_MP_TAC TC_SUBSET THEN 148 SRW_TAC [][mlt1_def] THEN 149 MAP_EVERY Q.EXISTS_TAC [`n`,`nvarb t2`,`{||}`] THEN 150 SRW_TAC [][], 151 Q.MATCH_RENAME_TAC `_ ��� _ ��� 0 < 1 + npair_count t1` THEN 152 Cases_on `nvarb t1 = {||}` THEN1 153 SRW_TAC [ARITH_ss][] THEN 154 DISJ1_TAC THEN Q.MATCH_ABBREV_TAC `(mlt1 R)^+ b2 (b1 + b2)` THEN 155 Q_TAC SUFF_TAC `(mlt1 R)^+ b2 (b2 + b1)` THEN1 156 METIS_TAC [COMM_BAG_UNION] THEN 157 MATCH_MP_TAC TC_mlt1_UNION2_I THEN 158 UNABBREV_ALL_TAC THEN 159 SRW_TAC [][] 160]) 161 162val th2 = Q.prove(`nwfs s ��� ^(h2)`, 163STRIP_TAC THEN REPEAT GEN_TAC THEN 164SIMP_TAC (srw_ss()) [inv_image_def,LEX_DEF] THEN 165Cases_on `t` THEN SRW_TAC [][] THENL [ 166 `���u. u IN nvars (nPair t1 t2) ��� (nvR s)^+ u n` 167 by METIS_TAC [nvwalk_nvR,ntermeq_thm] THEN 168 MATCH_MP_TAC TC_SUBSET THEN 169 SRW_TAC [][mlt1_def] THEN 170 MAP_EVERY Q.EXISTS_TAC [`n`,`nvarb t1`,`{||}`] THEN 171 SRW_TAC [][], 172 Q.MATCH_RENAME_TAC 173 `_ ��� _ ��� npair_count t1 < 1 + npair_count t1 + npair_count t2` THEN 174 Cases_on `nvarb t2 = {||}` THEN1 175 SRW_TAC [ARITH_ss][] THEN 176 DISJ1_TAC THEN MATCH_MP_TAC TC_mlt1_UNION2_I THEN 177 SRW_TAC [][] 178]) 179 180val th3 = prove(``nwfs s ��� ^(h3)``, 181STRIP_TAC THEN REPEAT GEN_TAC THEN 182SIMP_TAC (srw_ss()) [inv_image_def,LEX_DEF] THEN 183Cases_on `t` THEN SRW_TAC [][] THEN 184`���u. u IN nvars (Tie a t') ��� (nvR s)^+ u n` 185 by METIS_TAC [nvwalk_nvR,ntermeq_thm] THEN 186MATCH_MP_TAC TC_SUBSET THEN 187SRW_TAC [][mlt1_def] THEN 188MAP_EVERY Q.EXISTS_TAC [`n`,`nvarb t'`,`{||}`] THEN 189SRW_TAC [][]) 190 191val th4 = prove(``nwfs s ��� ^(h4)``, 192SRW_TAC [][nwfs_def] THEN 193MATCH_MP_TAC WF_inv_image THEN 194SRW_TAC [][WF_measure,WF_TC,WF_LEX,WF_mlt1]) 195 196fun nwalkstar_nwfs_hyp th = 197 th |> 198 PROVE_HYP (UNDISCH th1) |> 199 PROVE_HYP (UNDISCH th2) |> 200 PROVE_HYP (UNDISCH th3) |> 201 PROVE_HYP (UNDISCH th4) 202 203val nwalkstar_def = save_thm("nwalkstar_def",DISCH_ALL(nwalkstar_nwfs_hyp (inst_nwalkstar pre_nwalkstar_def))) 204val nwalkstar_ind = save_thm("nwalkstar_ind",nwalkstar_nwfs_hyp (inst_nwalkstar (theorem "pre_nwalkstar_ind"))) 205 206val nwalkstar_nom = nwalkstar_def |> UNDISCH |> Q.SPEC `Nom a` |> DISCH_ALL |> SIMP_RULE (srw_ss()) [] 207val nwalkstar_var = nwalkstar_def |> UNDISCH |> Q.SPEC `Sus p v` |> DISCH_ALL |> SIMP_RULE (srw_ss()) [] 208val nwalkstar_tie = nwalkstar_def |> UNDISCH |> Q.SPEC `Tie a t` |> DISCH_ALL |> SIMP_RULE (srw_ss()) [] 209val nwalkstar_pair = nwalkstar_def |> UNDISCH |> Q.SPEC `nPair t1 t2` |> DISCH_ALL |> SIMP_RULE (srw_ss()) [] 210val nwalkstar_const = nwalkstar_def |> UNDISCH |> Q.SPEC `nConst c` |> DISCH_ALL |> SIMP_RULE (srw_ss()) [] 211val nwalkstar_thm = RWsave_thm( 212 "nwalkstar_thm", 213 LIST_CONJ [nwalkstar_nom,nwalkstar_var,nwalkstar_tie,nwalkstar_pair,nwalkstar_const] 214 |> SIMP_RULE bool_ss [GSYM IMP_CONJ_THM]) 215 216val noc_ignores_pi = Q.store_thm( 217"noc_ignores_pi", 218`nwfs s ��� ���t. (noc s (apply_pi pi t) v ��� noc s t v)`, 219STRIP_TAC THEN Induct THEN SRW_TAC [][]) 220 221val noc_if_nvars_nwalkstar = Q.prove( 222`nwfs s ==> !t. v IN nvars (nwalk* s t) ==> noc s t v`, 223DISCH_TAC THEN HO_MATCH_MP_TAC nwalkstar_ind THEN SRW_TAC [][] THEN 224Q.PAT_X_ASSUM `nwfs s` ASSUME_TAC THEN 225Cases_on `t` THEN FULL_SIMP_TAC (srw_ss()) [] THEN 226Cases_on `nvwalk s l n` THEN FULL_SIMP_TAC (srw_ss()) [] THENL [ 227 (nvwalk_modulo_pi |> Q.SPECL_THEN [`s`,`l`,`n`] MP_TAC) THEN 228 SRW_TAC [][] THEN Cases_on `nvwalk s [] n` THEN FULL_SIMP_TAC (srw_ss()) [], 229 (nvwalk_modulo_pi |> Q.SPECL_THEN [`s`,`l`,`n`] MP_TAC) THEN 230 Cases_on `nvwalk s [] n` THEN FULL_SIMP_TAC (srw_ss()) [] THEN 231 SRW_TAC [][] THEN METIS_TAC [noc_ignores_pi], 232 (nvwalk_modulo_pi |> Q.SPECL_THEN [`s`,`l`,`n`] MP_TAC) THEN 233 SRW_TAC [][] THEN 234 Cases_on `nvwalk s [] n` THEN FULL_SIMP_TAC (srw_ss()) [] THEN 235 METIS_TAC [noc_ignores_pi], 236 (nvwalk_modulo_pi |> Q.SPECL_THEN [`s`,`l`,`n`] MP_TAC) THEN 237 SRW_TAC [][] THEN 238 Cases_on `nvwalk s [] n` THEN FULL_SIMP_TAC (srw_ss()) [] THEN 239 METIS_TAC [noc_ignores_pi] 240]) 241 242val NOT_FDOM_nwalkstar = Q.store_thm( 243"NOT_FDOM_nwalkstar", 244`nwfs s ==> !t. v NOTIN FDOM s ==> v IN nvars t ==> v IN nvars (nwalk* s t)`, 245DISCH_TAC THEN HO_MATCH_MP_TAC nwalkstar_ind THEN SRW_TAC [][] THEN 246Cases_on `t` THEN Cases_on `nvwalk s l n` THEN 247Q.PAT_X_ASSUM `nwfs s` ASSUME_TAC THEN 248FULL_SIMP_TAC (srw_ss()) [] THEN 249SRW_TAC [][] THEN 250Q.PAT_X_ASSUM `n NOTIN FDOM s` ASSUME_TAC THEN 251FULL_SIMP_TAC (srw_ss()) [Once nvwalk_def,FLOOKUP_DEF] THEN 252SRW_TAC [][]) 253 254val noc_NOTIN_FDOM = Q.store_thm( 255 "noc_NOTIN_FDOM", 256 `nwfs s ==> !t v. noc s t v ==> v NOTIN FDOM s`, 257 STRIP_TAC THEN HO_MATCH_MP_TAC noc_ind THEN SRW_TAC [] []) 258 259val nvars_nwalkstar_ignores_pi = Q.store_thm( 260"nvars_nwalkstar_ignores_pi", 261`nwfs s ��� ���t pi. nvars (nwalkstar s t) = nvars (nwalkstar s (apply_pi pi t))`, 262STRIP_TAC THEN HO_MATCH_MP_TAC nwalkstar_ind THEN 263SRW_TAC [][] THEN 264REVERSE (Cases_on `t`) THEN 265Q.PAT_X_ASSUM `nwfs s` ASSUME_TAC THEN 266FULL_SIMP_TAC (psrw_ss()) [] THEN1 METIS_TAC [] THEN 267(nvwalk_modulo_pi |> Q.SPECL_THEN [`s`,`l`,`n`] MP_TAC) THEN 268(nvwalk_modulo_pi |> Q.SPECL_THEN [`s`,`pi++l`,`n`] MP_TAC) THEN 269SRW_TAC [][] THEN 270Cases_on `nvwalk s [] n` THEN FULL_SIMP_TAC (srw_ss()) [] THEN 271FULL_SIMP_TAC (srw_ss()) [apply_pi_decompose] THEN 272METIS_TAC []) 273 274val nvars_nwalkstar_if_noc = Q.prove( 275`nwfs s ==> !t v. noc s t v ==> v IN nvars (nwalkstar s t)`, 276STRIP_TAC THEN HO_MATCH_MP_TAC noc_strong_ind THEN SRW_TAC [] [] THEN1 277 METIS_TAC [NOT_FDOM_nwalkstar] THEN 278REPEAT (POP_ASSUM MP_TAC) THEN 279SPEC_ALL_TAC [] THEN 280Induct_on `t` THEN SRW_TAC [][] THEN1 ( 281 (nvwalk_modulo_pi |> Q.SPECL_THEN [`s`,`l`,`n`] MP_TAC) THEN 282 STRIP_TAC THEN 283 Cases_on `nvwalk s [] n` THEN 284 Q.PAT_X_ASSUM `nwfs s` ASSUME_TAC THEN FULL_SIMP_TAC (srw_ss()) [] THEN1 ( 285 IMP_RES_TAC nvwalk_to_var THEN 286 IMP_RES_TAC NOT_FDOM_nvwalk THEN 287 FULL_SIMP_TAC (srw_ss()) []) THEN 288 METIS_TAC [nvars_nwalkstar_ignores_pi] ) THEN 289METIS_TAC [] 290) 291 292val noc_eq_nvars_nwalkstar = Q.store_thm( 293 "noc_eq_nvars_nwalkstar", 294 `nwfs s ==> (noc s t v ��� v ��� nvars (nwalk* s t))`, 295 SRW_TAC [][FUN_EQ_THM] THEN 296 METIS_TAC [nvars_nwalkstar_if_noc,noc_if_nvars_nwalkstar,IN_DEF]) 297 298val nvwalk_EQ_nom_nvR = Q.prove( 299`!v u. (nvR s)^+ v u ��� v NOTIN FDOM s ��� nwfs s ��� 300 !p a. nvwalk s p u ��� Nom a`, 301HO_MATCH_MP_TAC TC_INDUCT_RIGHT1 THEN SRW_TAC [][] THEN 302FULL_SIMP_TAC (srw_ss()) [nvR_def] THENL [ 303 Cases_on `FLOOKUP s u`, 304 Cases_on `FLOOKUP s u'` 305] THEN 306FULL_SIMP_TAC (srw_ss()) [] THEN 307SRW_TAC [][Once nvwalk_def] THEN Cases_on `x` THEN 308FULL_SIMP_TAC (srw_ss()) [] THEN 309SRW_TAC [][NOT_FDOM_nvwalk,nvwalk_case_thms]) 310 311val nvwalk_EQ_var_nvR = Q.prove( 312 `nwfs s ==> !p u p1 v1 v2. (nvwalk s p u = Sus p1 v1) /\ (nvR s)^+ v2 u /\ 313 v2 NOTIN FDOM s ==> (v1 = v2)`, 314 STRIP_TAC THEN HO_MATCH_MP_TAC nvwalk_ind THEN SRW_TAC [][] THEN 315 IMP_RES_TAC TC_CASES2 THEN 316 FULL_SIMP_TAC (srw_ss()) [nvR_def] THEN 317 Cases_on `FLOOKUP s u` THEN FULL_SIMP_TAC (srw_ss()) [] THEN 318 Q.PAT_X_ASSUM `nvwalk s p u = UU` MP_TAC THEN 319 SRW_TAC [][Once nvwalk_def] THEN 320 Cases_on `x` THEN 321 POP_ASSUM MP_TAC THEN 322 FULL_SIMP_TAC (srw_ss()) [NOT_FDOM_nvwalk] THEN 323 SELECT_ELIM_TAC THEN SRW_TAC [][] THEN 324 METIS_TAC [permeq_sym]) 325 326val nvwalk_EQ_const_nvR = prove( 327 ``!v u. (nvR s)^+ v u ==> v NOTIN FDOM s /\ nwfs s ==> 328 !p c. nvwalk s p u <> nConst c``, 329 HO_MATCH_MP_TAC TC_INDUCT_RIGHT1 THEN SRW_TAC [][] THENL [ 330 FULL_SIMP_TAC (srw_ss()) [nvR_def] THEN 331 Cases_on `FLOOKUP s u` THEN FULL_SIMP_TAC (srw_ss()) [] THEN 332 SRW_TAC [][Once nvwalk_def] THEN Cases_on `x` THEN 333 FULL_SIMP_TAC (srw_ss()) [] THEN 334 SRW_TAC [][NOT_FDOM_nvwalk,nvwalk_case_thms], 335 FULL_SIMP_TAC (srw_ss()) [nvR_def] THEN 336 Cases_on `FLOOKUP s u'` THEN FULL_SIMP_TAC (srw_ss()) [] THEN 337 SRW_TAC [][Once nvwalk_def] THEN Cases_on `x` THEN 338 FULL_SIMP_TAC (srw_ss()) [] THEN 339 SRW_TAC [][NOT_FDOM_nvwalk,nvwalk_case_thms] 340 ]) 341 342val nvwalk_EQ_tie_nvR = Q.prove( 343`!v u. (nvR s)^+ v u ��� 344 !a t p. v NOTIN FDOM s ��� nwfs s ��� (nvwalk s p u = Tie a t) ��� 345 ���u. (u IN nvars t) ��� (nvR s)^* v u`, 346HO_MATCH_MP_TAC TC_STRONG_INDUCT_RIGHT1 THEN SRW_TAC [][] THEN 347FULL_SIMP_TAC (srw_ss()) [nvR_def] THENL [ 348 Cases_on `FLOOKUP s u` THEN FULL_SIMP_TAC (srw_ss()) [] THEN 349 Q.PAT_X_ASSUM `nvwalk s p u = XXX` MP_TAC THEN 350 SRW_TAC [][Once nvwalk_def] THEN 351 Cases_on `x` THEN FULL_SIMP_TAC (srw_ss()) [] THENL [ 352 POP_ASSUM MP_TAC THEN 353 SRW_TAC [][NOT_FDOM_nvwalk,nvwalk_case_thms], 354 Q.EXISTS_TAC `v` THEN SRW_TAC [][] 355 ], 356 Cases_on `FLOOKUP s u'` THEN FULL_SIMP_TAC (srw_ss()) [] THEN 357 Q.PAT_X_ASSUM `nvwalk s p u' = XXX` MP_TAC THEN 358 SRW_TAC [][Once nvwalk_def] THEN 359 POP_ASSUM MP_TAC THEN 360 Cases_on `x` THEN SRW_TAC [][nvwalk_case_thms] 361 THEN FULL_SIMP_TAC (srw_ss()) [] THEN 362 METIS_TAC [TC_RTC] 363]) 364 365val nvwalk_EQ_pair_nvR = prove( 366 ``!v u. (nvR s)^+ v u ==> 367 !t1 t2 p. v NOTIN FDOM s /\ nwfs s /\ (nvwalk s p u = nPair t1 t2) ==> 368 ?u. (u IN nvars t1 \/ u IN nvars t2) /\ (nvR s)^* v u``, 369 HO_MATCH_MP_TAC TC_STRONG_INDUCT_RIGHT1 THEN SRW_TAC [][] THEN 370 FULL_SIMP_TAC (srw_ss()) [nvR_def] THENL [ 371 Cases_on `FLOOKUP s u` THEN FULL_SIMP_TAC (srw_ss()) [] THEN 372 Q.PAT_X_ASSUM `nvwalk s p u = XXX` MP_TAC THEN 373 SRW_TAC [][Once nvwalk_def] THEN 374 Cases_on `x` THEN FULL_SIMP_TAC (srw_ss()) [] THENL [ 375 POP_ASSUM MP_TAC THEN 376 SRW_TAC [][NOT_FDOM_nvwalk,nvwalk_case_thms], 377 Q.EXISTS_TAC `v` THEN SRW_TAC [][], 378 Q.EXISTS_TAC `v` THEN SRW_TAC [][] 379 ], 380 Cases_on `FLOOKUP s u'` THEN FULL_SIMP_TAC (srw_ss()) [] THEN 381 Q.PAT_X_ASSUM `nvwalk s p u' = XXX` MP_TAC THEN 382 SRW_TAC [][Once nvwalk_def] THEN 383 POP_ASSUM MP_TAC THEN 384 Cases_on `x` THEN SRW_TAC [][nvwalk_case_thms] 385 THEN FULL_SIMP_TAC (srw_ss()) [] THEN 386 METIS_TAC [TC_RTC] 387 ]) 388 389val TC_nvR_nvars_nwalkstar = Q.store_thm( 390 "TC_nvR_nvars_nwalkstar", 391 `nwfs s ==> 392 !t v u. (nvR s)^+ v u /\ v NOTIN FDOM s /\ u IN nvars t ==> 393 v IN nvars (nwalkstar s t)`, 394 STRIP_TAC THEN HO_MATCH_MP_TAC nwalkstar_ind THEN SRW_TAC [][] THEN 395 REVERSE (Cases_on `t`) THEN Q.PAT_X_ASSUM `nwfs s` ASSUME_TAC THEN 396 FULL_SIMP_TAC (srw_ss()) [] THEN SRW_TAC [][] 397 THEN1 METIS_TAC [] THEN1 METIS_TAC [] THEN1 METIS_TAC [] THEN 398 Cases_on `nvwalk s l n` THEN SRW_TAC [][] THENL [ 399 METIS_TAC [nvwalk_EQ_nom_nvR], 400 IMP_RES_TAC nvwalk_EQ_var_nvR THEN 401 SRW_TAC [][], 402 IMP_RES_TAC nvwalk_EQ_tie_nvR THEN 403 `(u = v) ��� (nvR s)^+ v u` 404 by METIS_TAC [EXTEND_RTC_TC_EQN,RTC_CASES1] THEN 405 FULL_SIMP_TAC (srw_ss()) [NOT_FDOM_nwalkstar] THEN 406 METIS_TAC [], 407 Q.MATCH_RENAME_TAC `v IN nvars (nwalkstar s t1) ��� v IN nvars (nwalkstar s t2)` THEN 408 `?u. u IN nvars (nPair t1 t2) /\ (nvR s)^* v u` 409 by (SRW_TAC [][] THEN METIS_TAC [nvwalk_EQ_pair_nvR]) THEN 410 `(u = v) \/ (nvR s)^+ v u` 411 by METIS_TAC [EXTEND_RTC_TC_EQN, RTC_CASES1] THEN 412 FULL_SIMP_TAC (srw_ss()) [NOT_FDOM_nwalkstar] THEN 413 METIS_TAC [], 414 METIS_TAC [nvwalk_EQ_const_nvR] 415 ]) 416 417val noc_TC_nvR = Q.store_thm( 418"noc_TC_nvR", 419`���t v. noc s t v ��� nwfs s ��� ���u. u ��� nvars t ��� (nvR s)^* v u`, 420HO_MATCH_MP_TAC noc_ind THEN SRW_TAC [][] THEN1 ( 421 Q.EXISTS_TAC `v` THEN SRW_TAC [][RTC_REFL] ) THEN 422RES_TAC THEN 423Cases_on `u = u'` THEN1 METIS_TAC [] THEN 424Q_TAC SUFF_TAC `(nvR s)^+ u' u` THEN1 ( 425 SRW_TAC [][] THEN Q.EXISTS_TAC `u` THEN SRW_TAC [][] THEN 426 FULL_SIMP_TAC (srw_ss()) [RTC_CASES_TC] THEN SRW_TAC [][] THEN 427 METIS_TAC [TC_RULES] ) THEN 428MATCH_MP_TAC (UNDISCH nvwalk_nvR) THEN 429`nvwalk s [] u ��� Sus [] u` by ( 430 SPOSE_NOT_THEN STRIP_ASSUME_TAC THEN 431 FULL_SIMP_TAC (srw_ss()) [] ) THEN 432METIS_TAC []) 433 434val nwalkstar_SUBMAP = Q.store_thm( 435"nwalkstar_SUBMAP", 436`s ��� sx ��� nwfs sx ��� (nwalk* sx t = nwalk* sx (nwalk* s t))`, 437SRW_TAC [][] THEN 438`nwfs s` by METIS_TAC [nwfs_SUBMAP] THEN 439Q.ID_SPEC_TAC `t` THEN 440HO_MATCH_MP_TAC nwalkstar_ind THEN 441SRW_TAC [][] THEN 442Q.PAT_X_ASSUM `nwfs s` ASSUME_TAC THEN 443Cases_on `nwalk s t` THEN 444FULL_SIMP_TAC (srw_ss()) [] THEN 445Q.MATCH_ABBREV_TAC `X = Y (nwalk* s t)` THEN 446SRW_TAC [][Once nwalkstar_def] THEN 447UNABBREV_ALL_TAC THEN 448SRW_TAC [][Once nwalkstar_def,SimpLHS] THEN 449MP_TAC nwalk_SUBMAP THEN 450SRW_TAC [][] THEN 451POP_ASSUM (Q.SPEC_THEN `l` MP_TAC) THEN SRW_TAC [][] THEN 452ASM_SIMP_TAC (psrw_ss()) []) 453 454val nwalkstar_idempotent = Q.store_thm( 455"nwalkstar_idempotent", 456`nwfs s ==> !t.(nwalkstar s t = nwalkstar s (nwalkstar s t))`, 457METIS_TAC [nwalkstar_SUBMAP,SUBMAP_REFL]) 458 459val nwalkstar_FEMPTY = RWstore_thm( 460"nwalkstar_FEMPTY", 461`nwalk* (FEMPTY) t = t`, 462Induct_on `t` THEN ASM_SIMP_TAC (psrw_ss()) []) 463 464val NOT_FDOM_nwalkstar = Q.store_thm( 465"NOT_FDOM_nwalkstar", 466`nwfs s ==> !t. v NOTIN FDOM s ==> v IN nvars t ==> v IN nvars (nwalk* s t)`, 467DISCH_TAC THEN HO_MATCH_MP_TAC nwalkstar_ind THEN 468SRW_TAC [][] THEN Cases_on `t` THEN 469FULL_SIMP_TAC (srw_ss()) [] THEN 470Q.PAT_X_ASSUM `nwfs s` ASSUME_TAC THEN 471FULL_SIMP_TAC (srw_ss()) [Once nvwalk_def, nvars_def, FLOOKUP_DEF]) 472 473val nwalkstar_nwalk = Q.store_thm( 474"nwalkstar_nwalk", 475`nwfs s ==> (nwalk* s (nwalk s t) = nwalk* s t)`, 476Cases_on `t` THEN SRW_TAC [][] THEN 477Cases_on `nvwalk s l n` THEN ASM_SIMP_TAC (psrw_ss()) [] THEN 478`nvwalk s l' n' = Sus l' n'` by METIS_TAC [nvwalk_to_var,NOT_FDOM_nvwalk] THEN 479ASM_SIMP_TAC (psrw_ss()) []) 480 481val nwalkstar_to_var = Q.store_thm( 482"nwalkstar_to_var", 483`(nwalk* s t = Sus pi v) ��� nwfs s ��� v NOTIN FDOM s ��� ���pu u. t = Sus pu u`, 484STRIP_TAC THEN 485IMP_RES_TAC (GSYM nwalkstar_nwalk) THEN 486POP_ASSUM (Q.SPEC_THEN `t` ASSUME_TAC) THEN 487Cases_on `nwalk s t` THEN 488FULL_SIMP_TAC (srw_ss()) [] THEN 489IMP_RES_TAC nwalk_to_var THEN 490IMP_RES_TAC NOT_FDOM_nvwalk THEN 491FULL_SIMP_TAC (srw_ss()) [] THEN SRW_TAC [][]) 492 493val nwalkstar_apply_pi = Q.store_thm( 494"nwalkstar_apply_pi", (* Lemma 2.14.0*) 495`nwfs s ��� ���t.nwalk* s (apply_pi pi t) = apply_pi pi (nwalk* s t)`, 496STRIP_TAC THEN HO_MATCH_MP_TAC nwalkstar_ind THEN 497STRIP_TAC THEN Cases_on `t` THEN 498ASM_SIMP_TAC (psrw_ss()) [] THEN 499SRW_TAC [][] THEN 500(nvwalk_modulo_pi |> Q.SPECL [`s`,`l`,`n`] |> MP_TAC) THEN 501(nvwalk_modulo_pi |> Q.SPECL [`s`,`pi++l`,`n`] |> MP_TAC) THEN 502SRW_TAC [][] THEN Cases_on `nvwalk s [] n` THEN 503FULL_SIMP_TAC (psrw_ss()) [pmact_decompose]); 504 505val _ = export_theory () 506