1open HolKernel boolLib bossLib Parse stringTheory arithmeticTheory finite_mapTheory pred_setTheory bagTheory pairTheory relationTheory prim_recTheory quotientLib nomsetTheory listTheory ramanaLib ntermTheory nsubstTheory apply_piTheory nwalkTheory nwalkstarTheory nunifDefTheory dis_setTheory monadsyntax ntermLib 2 3val _ = new_theory "nunifProps" 4val _ = metisTools.limit := { time = NONE, infs = SOME 5000 } 5 6val _ = export_permweakening "dis_set.dis_set_eq_perms" 7 8val fresh_q = ` 9 (fresh fe a (Nom b) <=> a ��� b) ��� 10 (fresh fe a (Sus pi v) <=> (lswapstr (REVERSE pi) a, v) ��� fe) ��� 11 (fresh fe a (Tie b t) <=> (a = b) ��� a ��� b ��� fresh fe a t) ��� 12 (fresh fe a (nPair t1 t2) <=> fresh fe a t1 ��� fresh fe a t2) ��� 13 (fresh fe a (nConst c) <=> T)`; 14val def_suffix = !Defn.def_suffix; 15val _ = Defn.def_suffix := "_def_with_choice"; 16val fresh_def_with_choice = Define fresh_q; 17val _ = Defn.def_suffix := def_suffix; 18val fresh_def = Q.store_thm("fresh_def",fresh_q,SIMP_TAC (psrw_ss()) [fresh_def_with_choice]); 19 20val fresh_apply_pi = Q.store_thm( 21"fresh_apply_pi", 22`fresh fcs a t ��� fresh fcs (lswapstr pi a) (apply_pi pi t)`, 23Induct_on `t` THEN ASM_SIMP_TAC (psrw_ss()) [fresh_def] THEN1 ( 24 SRW_TAC [][REVERSE_APPEND,pmact_decompose] ) THEN 25SRW_TAC [][] THEN SRW_TAC [][]) 26 27val lemma27 = Q.store_thm( (* Lemma 2.7 - just consequences of the above, but good for metis *) 28"lemma27", 29`(���t a pi fcs. fresh fcs a (apply_pi pi t) ��� fresh fcs (lswapstr (REVERSE pi) a) t) ��� 30 (���t a pi fcs. fresh fcs (lswapstr pi a) t ��� fresh fcs a (apply_pi (REVERSE pi) t)) ��� 31 (���t a pi fcs. fresh fcs a t ��� fresh fcs (lswapstr pi a) (apply_pi pi t))`, 32SRW_TAC [][] THEN1 ( 33 IMP_RES_TAC fresh_apply_pi THEN 34 POP_ASSUM (Q.SPEC_THEN `REVERSE pi` MP_TAC) THEN 35 SRW_TAC [][] ) 36THEN1 ( 37 IMP_RES_TAC fresh_apply_pi THEN 38 POP_ASSUM (Q.SPEC_THEN `REVERSE pi` MP_TAC) THEN 39 SRW_TAC [][] ) 40THEN METIS_TAC [fresh_apply_pi]) 41 42val (equiv_rules,equiv_ind,equiv_cases) = Hol_reln` 43 (equiv fcs (Nom a) (Nom a)) ��� 44 ((���a. a IN dis_set p1 p2 ��� (a,v) IN fcs) ��� 45 (equiv fcs (Sus p1 v) (Sus p2 v))) ��� 46 (equiv fcs t1 t2 ��� 47 equiv fcs (Tie a t1) (Tie a t2)) ��� 48 (a1 ��� a2 ��� fresh fcs a1 t2 ��� 49 equiv fcs t1 (apply_pi [(a1,a2)] t2) ��� 50 equiv fcs (Tie a1 t1) (Tie a2 t2)) ��� 51 (equiv fcs t1a t2a ��� equiv fcs t1d t2d ��� 52 equiv fcs (nPair t1a t1d) (nPair t2a t2d)) ��� 53 (equiv fcs (nConst c) (nConst c))` 54 55val equiv_refl = RWstore_thm( 56"equiv_refl", 57`equiv fcs t t`, 58Induct_on `t` THEN SRW_TAC [][] 59THEN SRW_TAC [][Once equiv_cases] THEN 60NTAC 2 (Q.EXISTS_TAC `l`) THEN 61SRW_TAC [][dis_set_def]) 62 63val equiv_fresh = Q.store_thm( (* Lemma 2.9 *) 64"equiv_fresh", 65`equiv fe t1 t2 ��� fresh fe a t1 ��� fresh fe a t2`, 66MAP_EVERY Q.ID_SPEC_TAC [`t2`,`t1`] THEN 67SIMP_TAC bool_ss [GSYM AND_IMP_INTRO] THEN 68HO_MATCH_MP_TAC equiv_ind THEN 69SRW_TAC [][] THEN 70IMP_RES_TAC fresh_apply_pi THEN 71FULL_SIMP_TAC (psrw_ss()) [fresh_def] THEN1 ( 72 Cases_on `lswapstr (REVERSE p2) a IN dis_set p1 p2` 73 THEN FULL_SIMP_TAC (srw_ss()) [dis_set_def] THEN 74 `lswapstr (REVERSE p1) (lswapstr p1 (lswapstr (REVERSE p2) a)) = lswapstr (REVERSE p1) a` 75 by METIS_TAC [] THEN 76 FULL_SIMP_TAC bool_ss [GSYM pmact_decompose] THEN 77 FULL_SIMP_TAC (srw_ss()) [pmact_decompose]) THEN 78Cases_on `a = a2` THEN 79Q.PAT_X_ASSUM `a ��� a1` ASSUME_TAC THEN 80FULL_SIMP_TAC (srw_ss()) [] THEN 81IMP_RES_TAC fresh_apply_pi THEN 82POP_ASSUM (Q.SPEC_THEN `REVERSE [(a1,a2)]` MP_TAC) THEN 83ASM_SIMP_TAC (srw_ss()) []) 84 85val equiv_apply_pi = Q.store_thm( (* equation 9, used for Theorem 2.11 *) 86"equiv_apply_pi", 87`equiv fe t1 t2 ��� equiv fe (apply_pi pi t1) (apply_pi pi t2)`, 88Q_TAC SUFF_TAC 89`���t1 t2. equiv fe t1 t2 ��� ���pi. equiv fe (apply_pi pi t1) (apply_pi pi t2)` 90THEN1 METIS_TAC [] THEN 91HO_MATCH_MP_TAC equiv_ind THEN 92SRW_TAC [][] THEN 93ASM_SIMP_TAC (psrw_ss()) [] THEN 94SRW_TAC [][Once equiv_cases] THEN1 ( 95 MAP_EVERY Q.EXISTS_TAC [`pi++p1`,`pi++p2`] THEN 96 SRW_TAC [][] THEN 97 FIRST_X_ASSUM MATCH_MP_TAC THEN 98 (dis_set_app_same_left |> EQ_IMP_RULE |> fst |> MATCH_MP_TAC) THEN 99 SRW_TAC [][] ) 100THEN1 METIS_TAC [fresh_apply_pi] THEN 101FIRST_X_ASSUM (Q.SPEC_THEN `pi` MP_TAC) THEN 102Q.MATCH_ABBREV_TAC `equiv fe X Y1 ��� equiv fe X Y2` THEN 103Q_TAC SUFF_TAC `Y1 = Y2` THEN1 METIS_TAC [] THEN 104MAP_EVERY Q.UNABBREV_TAC [`Y1`,`Y2`] THEN 105SRW_TAC [][pmact_sing_to_back]); 106 107val equiv_sym = Q.store_thm( 108"equiv_sym", 109`equiv fe t1 t2 ��� equiv fe t2 t1`, 110MAP_EVERY Q.ID_SPEC_TAC [`t2`,`t1`] THEN 111HO_MATCH_MP_TAC equiv_ind THEN 112SRW_TAC [][] THEN1 ( 113 SRW_TAC [][Once equiv_cases] THEN 114 MAP_EVERY Q.EXISTS_TAC [`p2`,`p1`] THEN 115 SRW_TAC [][] THEN METIS_TAC [dis_set_comm] ) 116THEN1 ( SRW_TAC [][Once equiv_cases] ) 117THEN1 ( 118 ASM_SIMP_TAC (srw_ss()) [Once equiv_cases] THEN 119 `equiv fe (apply_pi [(a2,a1)] (apply_pi [(a1,a2)] t2)) (apply_pi [(a2,a1)] t1)` 120 by (MATCH_MP_TAC equiv_apply_pi THEN SRW_TAC [][] ) THEN 121 FULL_SIMP_TAC (srw_ss()) [pmact_flip_args] THEN 122 MATCH_MP_TAC (GEN_ALL equiv_fresh) THEN 123 Q.EXISTS_TAC `[(a1,a2)] �� t2` THEN 124 IMP_RES_TAC fresh_apply_pi THEN 125 POP_ASSUM (Q.SPEC_THEN `[(a1,a2)]` MP_TAC) THEN 126 SRW_TAC [][]) THEN 127SRW_TAC [][Once equiv_cases]) 128 129val fresh_ds_equiv = Q.store_thm( (* Lemma 2.8 *) 130"fresh_ds_equiv", 131`(���a. a IN (dis_set pi1 pi2) ��� (fresh fcs a t)) ��� 132 equiv fcs (apply_pi pi1 t) (apply_pi pi2 t)`, 133MAP_EVERY Q.ID_SPEC_TAC [`pi2`,`pi1`,`t`] THEN 134Induct THEN SRW_TAC [][fresh_def] THEN 135FULL_SIMP_TAC (psrw_ss()) [dis_set_def] THEN 136SRW_TAC [][Once equiv_cases] THEN1 ( 137 MAP_EVERY Q.EXISTS_TAC [`pi1 ++ l`,`pi2++l`] THEN 138 SRW_TAC [][dis_set_def,pmact_decompose] THEN 139 RES_TAC THEN FULL_SIMP_TAC (srw_ss()) [] 140) THEN 141Cases_on `lswapstr pi2 s = lswapstr pi1 s` THEN SRW_TAC [][] THENL [ 142 FIRST_ASSUM MATCH_MP_TAC THEN 143 SRW_TAC [][] THEN RES_TAC THEN FULL_SIMP_TAC (srw_ss()) [], 144 (lemma27 |> CONJUNCT2 |> CONJUNCT1 |> Q.SPECL [`t`,`lswapstr pi1 s`,`REVERSE pi2`,`fcs`] 145 |> SIMP_RULE (srw_ss()) [] |> MATCH_MP_TAC) THEN 146 Q.MATCH_ABBREV_TAC `fresh fcs a t` THEN 147 Q_TAC SUFF_TAC `lswapstr pi1 a ��� lswapstr pi2 a ��� a ��� s` THEN1 METIS_TAC [] THEN 148 UNABBREV_ALL_TAC THEN SRW_TAC [][] THEN METIS_TAC [pmact_eql], 149 SRW_TAC [][GSYM apply_pi_decompose] THEN 150 FIRST_X_ASSUM MATCH_MP_TAC THEN SRW_TAC [][] THEN 151 Cases_on `a = s` THEN FULL_SIMP_TAC (srw_ss()) [] THEN 152 REVERSE (Cases_on `lswapstr pi1 a = lswapstr pi2 a`) 153 THEN1 RES_TAC THEN 154 Cases_on `lswapstr pi2 a = lswapstr pi1 s` THEN 155 Cases_on `lswapstr pi2 a = lswapstr pi2 s` THEN 156 FULL_SIMP_TAC (srw_ss()) [] 157]) 158 159val equiv_ds_fresh = Q.store_thm( (* 2.12.3 *) 160"equiv_ds_fresh", 161`equiv fe (apply_pi pi1 t) (apply_pi pi2 t) ��� a IN dis_set pi1 pi2 ��� fresh fe a t`, 162Q_TAC SUFF_TAC 163`!t1 t2. equiv fe t1 t2 ��� 164!pi1 pi2 t a. (apply_pi pi1 t = t1) ��� (apply_pi pi2 t = t2) ��� 165a ��� dis_set pi1 pi2 ��� fresh fe a t` THEN1 METIS_TAC [] THEN 166HO_MATCH_MP_TAC equiv_ind THEN 167STRIP_TAC THEN1 ( 168 ASM_SIMP_TAC (psrw_ss()) [apply_pi_eql,fresh_def,dis_set_def] THEN 169 METIS_TAC [pmact_inverse] ) THEN 170STRIP_TAC THEN1 ( 171 ASM_SIMP_TAC (srw_ss()) [apply_pi_eql,fresh_def] THEN 172 SRW_TAC [][dis_set_def] THEN 173 FIRST_X_ASSUM MATCH_MP_TAC THEN 174 `lswapstr (pi1����� ++ p1)����� = lswapstr (pi2����� ++ p2)�����` 175 by (MATCH_MP_TAC pmact_permeq THEN 176 IMP_RES_TAC permof_REVERSE_monotone) THEN 177 POP_ASSUM (fn th => SIMP_TAC bool_ss [SimpRHS, th]) THEN 178 SRW_TAC [][pmact_decompose]) THEN 179STRIP_TAC THEN1 ( 180 ASM_SIMP_TAC (psrw_ss()) [apply_pi_eql,fresh_def,dis_set_def] THEN 181 SRW_TAC [][] THEN 182 Cases_on `a' = lswapstr (REVERSE pi2) a` THEN SRW_TAC [][] 183 THEN METIS_TAC [] ) THEN 184STRIP_TAC THEN1 ( 185 ASM_SIMP_TAC (psrw_ss()) [apply_pi_eql,fresh_def,dis_set_def] THEN 186 SRW_TAC [][] THEN 187 Cases_on `a = lswapstr (REVERSE pi2) a2` THEN SRW_TAC [][] THEN 188 Q_TAC SUFF_TAC `fresh fe (lswapstr pi2 a) t2` THEN1 METIS_TAC [lemma27] THEN 189 Cases_on `a1 = lswapstr pi2 a` THEN SRW_TAC [][] THEN 190 FIRST_X_ASSUM (Q.SPECL_THEN [`pi1 ++ (REVERSE pi2)`,`[(a1,a2)]`,`lswapstr pi2 a`] MP_TAC) THEN 191 ASM_SIMP_TAC (psrw_ss()) [apply_pi_decompose,pmact_decompose] THEN 192 STRIP_TAC THEN POP_ASSUM MATCH_MP_TAC THEN 193 Cases_on `a2 = lswapstr pi2 a` THEN1 ( 194 SRW_TAC [][] THEN FULL_SIMP_TAC (psrw_ss()) [] ) THEN 195 SRW_TAC [][] ) THEN 196STRIP_TAC THEN1 ( 197 ASM_SIMP_TAC (psrw_ss()) [apply_pi_eql,fresh_def,dis_set_def] THEN 198 METIS_TAC [] ) THEN 199ASM_SIMP_TAC (psrw_ss()) [apply_pi_eql,fresh_def,dis_set_def]) 200 201val equiv_trans_lemma = Q.store_thm( 202"equiv_trans_lemma", 203`equiv fe t1 t2 ��� equiv fe t2 (apply_pi pi t2) ��� equiv fe t1 (apply_pi pi t2)`, 204Q_TAC SUFF_TAC 205`���t1 t2. equiv fe t1 t2 ��� ���pi. equiv fe t2 (apply_pi pi t2) ��� equiv fe t1 (apply_pi pi t2)` 206THEN1 METIS_TAC [] THEN 207HO_MATCH_MP_TAC equiv_ind THEN 208STRIP_TAC THEN1 SRW_TAC [][Once equiv_cases] THEN 209STRIP_TAC THEN1 ( 210 REPEAT STRIP_TAC THEN 211 ASM_SIMP_TAC (psrw_ss()) [Once equiv_cases] THEN 212 POP_ASSUM MP_TAC THEN 213 ASM_SIMP_TAC (psrw_ss()) [Once equiv_cases] THEN 214 STRIP_TAC THEN 215 MAP_EVERY Q.EXISTS_TAC [`p1`,`pi++p2`] THEN 216 SRW_TAC [][] THEN 217 FULL_SIMP_TAC (srw_ss()) [dis_set_def] THEN 218 METIS_TAC [pmact_permeq] ) THEN 219STRIP_TAC THEN1 ( 220 REPEAT STRIP_TAC THEN 221 SRW_TAC [][Once equiv_cases] THEN 222 POP_ASSUM MP_TAC THEN 223 SRW_TAC [][Once equiv_cases] THEN 224 SRW_TAC [][] THEN 225 METIS_TAC [apply_pi_decompose] ) THEN 226STRIP_TAC THEN1 ( 227 REPEAT STRIP_TAC THEN 228 SRW_TAC [][Once equiv_cases] THEN 229 POP_ASSUM MP_TAC THEN 230 SRW_TAC [][Once equiv_cases] THEN 231 SRW_TAC [][] THEN1 ( 232 Cases_on `lswapstr pi a1 = a1` THEN1 METIS_TAC [fresh_apply_pi] THEN 233 Cases_on `lswapstr (REVERSE pi) a1 = a1` THEN1 ( 234 FULL_SIMP_TAC (srw_ss()) [pmact_eql] ) THEN 235 MATCH_MP_TAC (GEN_ALL equiv_ds_fresh) THEN 236 MAP_EVERY Q.EXISTS_TAC [`[]`,`REVERSE pi`] THEN 237 SRW_TAC [][dis_set_def]) 238 THEN1 ( 239 `equiv fe (apply_pi [(a1,a2)] t2) (apply_pi [(a1,a2)] (apply_pi pi t2))` 240 by METIS_TAC [equiv_apply_pi] THEN 241 FIRST_X_ASSUM (Q.SPEC_THEN `(a1,a2)::pi ++ (REVERSE [(a1,a2)])` MP_TAC) THEN 242 SIMP_TAC (srw_ss()) [apply_pi_decompose] THEN 243 FULL_SIMP_TAC (srw_ss()) [GSYM apply_pi_decompose] ) THEN 244 Cases_on `lswapstr pi a2 = a2` THEN 245 Cases_on `lswapstr pi a2 = a1` THEN 246 FULL_SIMP_TAC (srw_ss()) [] THEN1 ( 247 `equiv fe (apply_pi [(a1,a2)] t2) (apply_pi [(a1,a2)] (apply_pi [(a2,a1)] (apply_pi pi t2)))` 248 by METIS_TAC [equiv_apply_pi] THEN 249 FIRST_X_ASSUM (Q.SPEC_THEN `pi ++ (REVERSE [(a1,a2)])` MP_TAC) THEN 250 FULL_SIMP_TAC (srw_ss()) [apply_pi_decompose] THEN 251 FULL_SIMP_TAC (srw_ss()) [pmact_flip_args]) THEN 252 `fresh fe a1 (apply_pi [(a2,lswapstr pi a2)] (apply_pi pi t2))` 253 by METIS_TAC [equiv_fresh] THEN 254 `fresh fe (lswapstr (REVERSE [(a2,lswapstr pi a2)]) a1) (apply_pi pi t2)` 255 by METIS_TAC [lemma27] THEN 256 Q.PAT_X_ASSUM `lswapstr pi a2 ��� a1` ASSUME_TAC THEN 257 Q.PAT_X_ASSUM `a1 ��� a2` ASSUME_TAC THEN 258 FULL_SIMP_TAC (srw_ss()) [] THEN 259 FIRST_X_ASSUM (Q.SPEC_THEN `(a1,lswapstr pi a2)::pi ++ (REVERSE [(a1,a2)])` MP_TAC) THEN 260 SIMP_TAC (srw_ss()) [apply_pi_decompose] THEN 261 FULL_SIMP_TAC (srw_ss()) [GSYM apply_pi_decompose] THEN 262 STRIP_TAC THEN POP_ASSUM MATCH_MP_TAC THEN 263 MATCH_MP_TAC fresh_ds_equiv THEN 264 `���a. a ��� dis_set [] ((a2,lswapstr pi a2)::pi) ��� fresh fe a t2` 265 by (SRW_TAC [][] THEN MATCH_MP_TAC (GEN_ALL equiv_ds_fresh) THEN 266 MAP_EVERY Q.EXISTS_TAC [`[]`,`((a2,lswapstr pi a2)::pi)`] THEN 267 SRW_TAC [][] THEN METIS_TAC [dis_set_comm,equiv_sym] ) THEN 268 FULL_SIMP_TAC (srw_ss()) [dis_set_def] THEN 269 SRW_TAC [][] THEN 270 Cases_on `a = a1` THEN FULL_SIMP_TAC (srw_ss()) [] THEN 271 Cases_on `a = a2` THEN FULL_SIMP_TAC (srw_ss()) [] THEN 272 Cases_on `a1 = lswapstr pi a` THEN FULL_SIMP_TAC (srw_ss()) [] THEN 273 Cases_on `a2 = lswapstr pi a` THEN FULL_SIMP_TAC (srw_ss()) [] THEN 274 Cases_on `lswapstr pi (lswapstr pi a) = a` THEN FULL_SIMP_TAC (srw_ss()) [] THEN 275 Cases_on `lswapstr (REVERSE pi) a = a` THEN 276 FULL_SIMP_TAC (srw_ss()) [pmact_eql] THEN 277 `fresh fe (lswapstr (REVERSE pi) (lswapstr pi a)) (apply_pi (REVERSE pi) (apply_pi pi t2))` 278 by METIS_TAC [lemma27] THEN 279 FULL_SIMP_TAC (srw_ss()) []) THEN 280STRIP_TAC THEN1 ( 281 REPEAT STRIP_TAC THEN 282 SRW_TAC [][Once equiv_cases] THEN 283 POP_ASSUM MP_TAC THEN 284 SRW_TAC [][Once equiv_cases] ) THEN 285SRW_TAC [][Once equiv_cases]) 286 287val equiv_trans = Q.store_thm( 288"equiv_trans", 289`equiv fe t1 t2 ��� equiv fe t2 t3 ��� equiv fe t1 t3`, 290Q_TAC SUFF_TAC 291`���t1 t2. equiv fe t1 t2 ��� ���t3. equiv fe t2 t3 ��� equiv fe t1 t3` 292THEN1 METIS_TAC [] THEN 293HO_MATCH_MP_TAC equiv_ind THEN 294STRIP_TAC THEN1 ( 295 SRW_TAC [][Once equiv_cases] ) THEN 296STRIP_TAC THEN1 ( 297 SRW_TAC [][Once equiv_cases] THEN 298 SRW_TAC [][Once equiv_cases] THEN 299 MAP_EVERY Q.EXISTS_TAC [`p1`,`p2'`] THEN 300 SRW_TAC [][] THEN 301 `dis_set p1' p2' = dis_set p2 p2'` 302 by METIS_TAC [dis_set_eq_perms,permeq_refl,permeq_sym] THEN 303 FULL_SIMP_TAC (srw_ss()) [dis_set_def] THEN 304 Cases_on `lswapstr p1 a ��� lswapstr p2 a` THEN SRW_TAC [][] THEN 305 Cases_on `lswapstr p2 a ��� lswapstr p2' a` THEN SRW_TAC [][] THEN 306 METIS_TAC [] ) THEN 307STRIP_TAC THEN1 ( 308 REPEAT STRIP_TAC THEN 309 SRW_TAC [][Once equiv_cases] THEN 310 POP_ASSUM MP_TAC THEN 311 SRW_TAC [][Once equiv_cases] ) THEN 312STRIP_TAC THEN1 ( 313 REPEAT STRIP_TAC THEN 314 SRW_TAC [][Once equiv_cases] THEN 315 POP_ASSUM MP_TAC THEN 316 SRW_TAC [][Once equiv_cases] THEN1 ( 317 IMP_RES_TAC equiv_fresh THEN 318 SRW_TAC [][] THEN 319 FIRST_X_ASSUM MATCH_MP_TAC THEN 320 MATCH_MP_TAC equiv_apply_pi THEN 321 SRW_TAC [][] ) THEN 322 Cases_on `a2' = a1` THEN ASM_SIMP_TAC (srw_ss()) [] THEN1 ( 323 FIRST_X_ASSUM MATCH_MP_TAC THEN 324 `equiv fe ([(a1,a2)] �� t2) ([(a1,a2)] �� ([(a2,a1)] �� t2'))` 325 by ( MATCH_MP_TAC equiv_apply_pi THEN SRW_TAC [][]) THEN 326 FULL_SIMP_TAC (srw_ss()) [pmact_flip_args]) THEN 327 Q.MATCH_ASSUM_RENAME_TAC `a2 ��� a3` THEN 328 Q.MATCH_ASSUM_RENAME_TAC `fresh fe a2 t3` THEN 329 CONJ1_TAC THEN1 ( 330 `equiv fe (apply_pi (REVERSE [(a2,a3)]) t2) (apply_pi (REVERSE [(a2,a3)]) (apply_pi [(a2,a3)] t3))` 331 by METIS_TAC [equiv_apply_pi] THEN 332 FULL_SIMP_TAC (srw_ss()) [] THEN 333 `fresh fe (lswapstr [(a2,a3)] a1) (apply_pi [(a2,a3)] t2)` 334 by METIS_TAC [lemma27] THEN 335 POP_ASSUM MP_TAC THEN ASM_SIMP_TAC (srw_ss()) [] THEN 336 METIS_TAC [equiv_fresh] ) THEN 337 `equiv fe (apply_pi [(a1,a2)] t2) (apply_pi [(a1,a2)] (apply_pi [(a2,a3)] t3))` 338 by (METIS_TAC [equiv_apply_pi]) THEN 339 `dis_set [(a1,a3)] [(a1,a2);(a2,a3)] = {a1;a2}` 340 by (SRW_TAC [][dis_set_def,EXTENSION] THEN 341 Cases_on `x = a1` THEN SRW_TAC [][] THEN 342 Cases_on `x = a2` THEN SRW_TAC [][] THEN 343 Cases_on `x = a3` THEN SRW_TAC [][] ) THEN 344 FULL_SIMP_TAC (srw_ss()) [EXTENSION] THEN 345 `equiv fe (apply_pi [(a1,a2);(a2,a3)] t3) (apply_pi [(a1,a3)] t3)` 346 by METIS_TAC [fresh_ds_equiv,dis_set_comm] THEN 347 `equiv fe (apply_pi [(a1,a2)] t2) 348 (apply_pi ([(a1,a3)] ++ (REVERSE [(a1,a2);(a2,a3)])) 349 (apply_pi [(a1,a2);(a2,a3)] t3))` by 350 (MATCH_MP_TAC equiv_trans_lemma THEN 351 CONJ_TAC THEN1 FULL_SIMP_TAC (srw_ss()) [GSYM apply_pi_decompose] THEN 352 SRW_TAC [][apply_pi_decompose]) THEN 353 RES_TAC THEN FULL_SIMP_TAC (srw_ss()) [apply_pi_decompose]) THEN 354STRIP_TAC THEN1 ( 355 REPEAT STRIP_TAC THEN 356 SRW_TAC [][Once equiv_cases] THEN 357 POP_ASSUM MP_TAC THEN 358 SRW_TAC [][Once equiv_cases] ) THEN 359SRW_TAC [][Once equiv_cases]) 360 361val fresh_extra_fcs = Q.store_thm( 362"fresh_extra_fcs", 363`fresh fe a t ��� fe SUBSET fex ��� fresh fex a t`, 364Induct_on `t` THEN SRW_TAC [][fresh_def] THEN METIS_TAC [SUBSET_DEF]) 365 366val term_fcs_FINITE = Q.store_thm( 367"term_fcs_FINITE", 368`(term_fcs a t = SOME fe) ��� FINITE fe`, 369Q.ID_SPEC_TAC `fe` THEN 370Induct_on `t` THEN 371ASM_SIMP_TAC (psrw_ss()) [Once term_fcs_def] THEN 372SRW_TAC [][] THEN SRW_TAC [][]) 373 374val term_fcs_fresh = Q.store_thm( 375"term_fcs_fresh", 376`(term_fcs a t = SOME fe) ��� fresh fe a t`, 377Q.ID_SPEC_TAC `fe` THEN Induct_on `t` THEN 378ASM_SIMP_TAC (psrw_ss()) [Once term_fcs_def, fresh_def] THEN 379SRW_TAC [][] THEN METIS_TAC [fresh_extra_fcs,SUBSET_UNION]) 380 381val term_fcs_minimal = Q.store_thm( 382"term_fcs_minimal", 383`(term_fcs a t = SOME fe) ��� fresh fe' a t ��� fe SUBSET fe'`, 384Q.ID_SPEC_TAC `fe` THEN Induct_on `t` THEN 385ASM_SIMP_TAC (psrw_ss()) [Once term_fcs_def, fresh_def] THEN 386SRW_TAC [][] THEN SRW_TAC [][]) 387 388val term_fcs_SOME = LIST_CONJ [term_fcs_FINITE,term_fcs_fresh,term_fcs_minimal] 389 390val term_fcs_NONE = Q.store_thm( 391"term_fcs_NONE", 392`���t fe. (term_fcs a t = NONE) ��� ���fe. ��fresh fe a t`, 393Induct THEN SRW_TAC [][fresh_def] THEN 394TRY (POP_ASSUM MP_TAC) THEN 395SRW_TAC [][Once term_fcs_def] THEN 396METIS_TAC []) 397 398val fcs_acc_RECURSES = Q.store_thm( 399"fcs_acc_RECURSES", 400`FINITE t ��� 401 (ITSET (fcs_acc s) (e INSERT t) b = 402 fcs_acc s e (ITSET (fcs_acc s) (t DELETE e) b))`, 403STRIP_TAC THEN MATCH_MP_TAC COMMUTING_ITSET_RECURSES THEN 404SIMP_TAC (srw_ss()) [FORALL_PROD] THEN 405SRW_TAC [][fcs_acc_def] THEN 406MAP_EVERY Cases_on 407[`z`,`term_fcs p_1 (nwalk* s (Sus [] p_2))`,`term_fcs p_1' (nwalk* s (Sus [] p_2'))`] THEN 408SRW_TAC [][] THEN 409METIS_TAC [UNION_ASSOC,UNION_COMM]) 410 411val unify_eq_vars_extends_fe = Q.store_thm( 412"unify_eq_vars_extends_fe", 413`FINITE ds ��� (unify_eq_vars ds v (s,fe) = SOME (s',fex)) ��� fe SUBSET fex`, 414SRW_TAC [][unify_eq_vars_def] THEN 415SRW_TAC [][SUBSET_UNION]) 416 417val image_lem = Q.prove( 418`e NOTIN t ��� (IMAGE (��a. (a,v:num)) t DELETE (e,v) = IMAGE (��a. (a,v)) t)`, 419SRW_TAC [][EXTENSION,EQ_IMP_THM]) 420 421val unify_eq_vars_FINITE = Q.store_thm( 422"unify_eq_vars_FINITE", 423`FINITE ds ��� (unify_eq_vars ds v (s,fe) = SOME (s',fex)) ��� FINITE fe ��� FINITE fex`, 424Q_TAC SUFF_TAC 425`���ds. FINITE ds ��� ���fe fex. (unify_eq_vars ds v (s,fe) = SOME (s',fex)) ��� FINITE fe ��� FINITE fex` 426THEN1 METIS_TAC [] THEN 427HO_MATCH_MP_TAC FINITE_INDUCT THEN 428SIMP_TAC (srw_ss()) [unify_eq_vars_def,ITSET_EMPTY] THEN 429SRW_TAC [][] THEN SRW_TAC [][] THEN 430Q.PAT_X_ASSUM `X = SOME fex'` MP_TAC THEN 431FULL_SIMP_TAC (srw_ss()) [DELETE_NON_ELEMENT,fcs_acc_RECURSES,fcs_acc_def,image_lem] THEN 432SRW_TAC [][] THEN METIS_TAC [FINITE_UNION,term_fcs_FINITE]) 433 434val unify_eq_vars_fresh = Q.store_thm( 435"unify_eq_vars_fresh", 436`FINITE ds ��� (unify_eq_vars ds v (s,fe) = SOME (s',fex)) ��� a ��� ds ��� 437 fresh fex a (nwalk* s' (Sus [] v))`, 438Q_TAC SUFF_TAC 439`���ds. FINITE ds ��� ���fe fex. (unify_eq_vars ds v (s,fe) = SOME (s',fex)) ��� a ��� ds ��� 440 fresh fex a (nwalk* s' (Sus [] v))` 441THEN1 METIS_TAC [] THEN 442HO_MATCH_MP_TAC FINITE_INDUCT THEN 443SIMP_TAC (srw_ss()) [unify_eq_vars_def,ITSET_EMPTY] THEN 444SRW_TAC [][] THEN SRW_TAC [][] THEN 445Q.PAT_X_ASSUM `X = SOME fex'` MP_TAC THEN 446FULL_SIMP_TAC (srw_ss()) [DELETE_NON_ELEMENT,fcs_acc_RECURSES,fcs_acc_def,image_lem] THEN 447SRW_TAC [][] THEN IMP_RES_TAC term_fcs_fresh THEN 448METIS_TAC [fresh_extra_fcs,SUBSET_UNION,UNION_ASSOC]) 449 450val unify_eq_vars_minimal = Q.store_thm( 451"unify_eq_vars_minimal", 452`FINITE ds ��� (unify_eq_vars ds v (s,fe) = SOME (s',fex)) ��� c ��� fex ��� 453 c ��� fe ��� c ��� fe ��� ���a fcs. (term_fcs a (nwalk* s (Sus [] v)) = SOME fcs) ��� a ��� ds ��� c ��� fcs`, 454Q_TAC SUFF_TAC 455`���ds. FINITE ds ��� ���fe fex. (unify_eq_vars ds v (s,fe) = SOME (s',fex)) ��� c ��� fex ��� 456 c ��� fe ��� c ��� fe ��� ���a fcs. (term_fcs a (nwalk* s (Sus [] v)) = SOME fcs) ��� a ��� ds ��� c ��� fcs` 457THEN1 SRW_TAC [][] THEN 458HO_MATCH_MP_TAC FINITE_INDUCT THEN 459SIMP_TAC (srw_ss()) [unify_eq_vars_def,ITSET_EMPTY] THEN 460SRW_TAC [][] THEN SRW_TAC [][] THEN 461Cases_on `c ��� fe` THEN FULL_SIMP_TAC (srw_ss()) [] THEN 462Q.PAT_X_ASSUM `X = SOME fex'` MP_TAC THEN 463FULL_SIMP_TAC (srw_ss()) [DELETE_NON_ELEMENT,fcs_acc_RECURSES,fcs_acc_def,image_lem] THEN 464SRW_TAC [][] THEN METIS_TAC [UNION_COMM]) 465 466val unify_eq_vars_SOME = LIST_CONJ [unify_eq_vars_FINITE,unify_eq_vars_fresh,unify_eq_vars_minimal] 467 468val unify_eq_vars_NONE = Q.store_thm( 469"unify_eq_vars_NONE", 470`FINITE ds ��� (unify_eq_vars ds v (s,fe) = NONE) ��� 471 ���a. a ��� ds ��� ���fe. �� fresh fe a (nwalk* s (Sus [] v))`, 472Q_TAC SUFF_TAC 473`���t. FINITE t ��� ���fe. (unify_eq_vars t v (s,fe) = NONE) ��� 474 (���a. a IN t ��� ���fex. �� fresh fex a (nwalk* s (Sus [] v)))` 475THEN1 METIS_TAC [] THEN 476HO_MATCH_MP_TAC FINITE_INDUCT THEN 477SRW_TAC [][unify_eq_vars_def,ITSET_EMPTY] THEN 478IMP_RES_TAC image_lem THEN POP_ASSUM (Q.SPEC_THEN `v` MP_TAC) THEN STRIP_TAC THEN 479Q.PAT_X_ASSUM `FINITE t` ASSUME_TAC THEN 480Q.PAT_X_ASSUM `a NOTIN t` ASSUME_TAC THEN 481FULL_SIMP_TAC (srw_ss()) [fcs_acc_RECURSES,DELETE_NON_ELEMENT,fcs_acc_def] THEN 482METIS_TAC [term_fcs_NONE]) 483 484val unify_eq_vars_decompose = Q.store_thm( 485"unify_eq_vars_decompose", 486`(unify_eq_vars (a INSERT ds) v (s,fe) = SOME (sx,fex)) ��� FINITE ds ��� 487 ���fe0 fcs. 488 (unify_eq_vars ds v (s,fe) = SOME (s, fe0)) ��� 489 (term_fcs a (nwalk* s (Sus [] v)) = SOME fcs) ��� 490 (fex = fe0 ��� fcs)`, 491SRW_TAC [][] THEN 492Cases_on `a ��� ds` THEN1 ( 493 FULL_SIMP_TAC (srw_ss()) [ABSORPTION] THEN 494 IMP_RES_TAC unify_eq_vars_preserves_s THEN 495 SRW_TAC [][] THEN 496 IMP_RES_TAC unify_eq_vars_SOME THEN 497 FULL_SIMP_TAC (srw_ss()) [ABSORPTION] THEN 498 RES_TAC THEN 499 Cases_on `term_fcs a (nwalk* s (Sus [] v))` THEN1 ( 500 IMP_RES_TAC term_fcs_NONE ) THEN 501 SRW_TAC [][] THEN 502 IMP_RES_TAC term_fcs_minimal THEN 503 FULL_SIMP_TAC (srw_ss()) [SUBSET_DEF,EXTENSION] THEN METIS_TAC []) THEN 504FULL_SIMP_TAC (srw_ss()) [unify_eq_vars_def,fcs_acc_RECURSES,fcs_acc_def] THEN 505`(a,v) ��� IMAGE (��a. (a,v)) ds` 506by (SRW_TAC [][]) THEN 507FULL_SIMP_TAC (srw_ss()) [DELETE_NON_ELEMENT] THEN 508METIS_TAC [UNION_ASSOC]) 509 510val unify_eq_vars_INSERT = Q.store_thm( 511"unify_eq_vars_INSERT", 512`(unify_eq_vars ds v (s,fe) = SOME (sx,fex)) ��� 513 (term_fcs a (nwalk* s (Sus [] v)) = SOME fcs) ��� 514 FINITE ds ��� 515 (unify_eq_vars (a INSERT ds) v (s,fe) = SOME (s,fex ��� fcs))`, 516SRW_TAC [][unify_eq_vars_def,fcs_acc_RECURSES,fcs_acc_def] THEN 517REVERSE (Cases_on `(a,v) ��� IMAGE (��a. (a,v)) ds`) THEN1 ( 518 FULL_SIMP_TAC (srw_ss()) [DELETE_NON_ELEMENT] THEN 519 METIS_TAC [UNION_ASSOC]) THEN 520`(a,v) INSERT (IMAGE (��a. (a,v)) ds DELETE (a,v)) = IMAGE (��a. (a,v)) ds` 521by SRW_TAC [][] THEN 522(fcs_acc_RECURSES |> Q.INST [`e`|->`(a,v)`,`t`|->`IMAGE (��a. (a,v)) ds DELETE (a,v)`,`b`|->`SOME {}`] 523 |> SIMP_RULE (srw_ss()) [fcs_acc_def] |> MP_TAC) THEN 524SRW_TAC [][] THEN SRW_TAC [][UNION_IDEMPOT,GSYM UNION_ASSOC]) 525 526val equiv_eq_perms = Q.store_thm( 527"equiv_eq_perms", 528`equiv fcs (Sus p1 v1) (Sus p2 v2) ��� p1 == q1 ��� p2 == q2 ��� equiv fcs (Sus q1 v1) (Sus q2 v2)`, 529SRW_TAC [][Once equiv_cases] THEN 530SRW_TAC [][Once equiv_cases] THEN 531FULL_SIMP_TAC (srw_ss()) [dis_set_def] THEN 532METIS_TAC [pmact_permeq,permeq_sym]) 533 534val fresh_eq_perms = Q.store_thm( 535"fresh_eq_perms", 536`fresh fcs a (Sus p v) ��� p == q ��� fresh fcs a (Sus q v)`, 537ASM_SIMP_TAC (psrw_ss()) [fresh_def] THEN 538METIS_TAC [pmact_eql,pmact_permeq]) 539 540val unify_eq_vars_equiv = Q.store_thm( 541"unify_eq_vars_equiv", 542`nwfs s ��� (unify_eq_vars (dis_set pi1 pi2) v (s,fe) = SOME (s,fcs)) ��� 543 equiv fcs (nwalk* s (Sus pi1 v)) (nwalk* s (Sus pi2 v))`, 544STRIP_TAC THEN 545MP_TAC (Q.SPECL [`s`,`pi1`,`v`] (nvwalk_modulo_pi)) THEN 546MP_TAC (Q.SPECL [`s`,`pi2`,`v`] (nvwalk_modulo_pi)) THEN 547SRW_TAC [][] THEN 548Cases_on `nvwalk s [] v` THEN FULL_SIMP_TAC (psrw_ss()) [] THENL [ 549 (fresh_ds_equiv |> Q.GEN `t` |> Q.SPEC `Nom s'` |> SIMP_RULE (srw_ss()) [] |> MATCH_MP_TAC) THEN 550 `FINITE (dis_set pi1 pi2)` by SRW_TAC [][] THEN 551 SRW_TAC [][] THEN 552 IMP_RES_TAC unify_eq_vars_fresh THEN 553 POP_ASSUM MP_TAC THEN SRW_TAC [][], 554 ASM_SIMP_TAC (psrw_ss()) [] THEN 555 Q_TAC SUFF_TAC `equiv fcs (Sus (pi1 ++ l) n) (Sus (pi2 ++ l) n)` 556 THEN1 (STRIP_TAC THEN MATCH_MP_TAC (GEN_ALL equiv_eq_perms) THEN 557 MAP_EVERY Q.EXISTS_TAC [`pi2++l`,`pi1++l`] THEN 558 NTAC 2 SELECT_ELIM_TAC THEN SRW_TAC [][] THEN METIS_TAC [permeq_sym]) THEN 559 (fresh_ds_equiv |> Q.GEN `t` |> Q.SPEC `Sus l n` |> SIMP_RULE (psrw_ss()) [] |> MATCH_MP_TAC) THEN 560 `FINITE (dis_set pi1 pi2)` by SRW_TAC [][] THEN 561 SRW_TAC [][] THEN 562 IMP_RES_TAC unify_eq_vars_fresh THEN 563 POP_ASSUM MP_TAC THEN ASM_SIMP_TAC (psrw_ss()) [], 564 Q.MATCH_ASSUM_RENAME_TAC `nvwalk s [] v = Tie s' C` THEN 565 (fresh_ds_equiv |> GEN_ALL |> Q.SPECL [`nwalkstar s (Tie s' C)`,`pi2`,`pi1`] |> 566 SIMP_RULE (srw_ss()) [] |> MP_TAC) THEN 567 SRW_TAC [][nwalkstar_apply_pi] THEN 568 POP_ASSUM MATCH_MP_TAC THEN 569 `FINITE (dis_set pi1 pi2)` by SRW_TAC [][] THEN 570 SRW_TAC [][] THEN 571 IMP_RES_TAC unify_eq_vars_fresh THEN 572 POP_ASSUM MP_TAC THEN ASM_SIMP_TAC (psrw_ss()) [], 573 Q.MATCH_ASSUM_RENAME_TAC `nvwalk s [] v = nPair C1 C2` THEN 574 (fresh_ds_equiv |> GEN_ALL |> Q.SPECL [`nwalkstar s (nPair C1 C2)`,`pi2`,`pi1`] |> 575 SIMP_RULE (srw_ss()) [] |> MP_TAC) THEN 576 SRW_TAC [][nwalkstar_apply_pi] THEN 577 POP_ASSUM MATCH_MP_TAC THEN 578 `FINITE (dis_set pi1 pi2)` by SRW_TAC [][] THEN 579 SRW_TAC [][] THEN 580 IMP_RES_TAC unify_eq_vars_fresh THEN 581 POP_ASSUM MP_TAC THEN ASM_SIMP_TAC (psrw_ss()) []]) 582 583val nunify_extends_fe = Q.store_thm( 584"nunify_extends_fe", 585`���s fe t1 t2 sx fex. nwfs s ��� (nunify (s,fe) t1 t2 = SOME (sx,fex)) ��� fe SUBSET fex`, 586HO_MATCH_MP_TAC nunify_ind THEN SRW_TAC [][] THEN 587Q.PAT_X_ASSUM `nunify p t1 t2 = SOME px` MP_TAC THEN 588Cases_on `nwalk s t1` THEN Cases_on `nwalk s t2` THEN 589SRW_TAC [][Once nunify_def,LET_THM] THEN SRW_TAC [][] THENL [ 590 METIS_TAC [unify_eq_vars_extends_fe,FINITE_dis_set], 591 FULL_SIMP_TAC (srw_ss()) [UNCURRY] THEN 592 Cases_on `x` THEN 593 `nwfs q` by METIS_TAC [nunify_uP,uP_def] THEN 594 METIS_TAC [SUBSET_TRANS] 595]) 596 597val unify_eq_vars_empty = RWstore_thm( 598"unify_eq_vars_empty", 599`unify_eq_vars {} v (s,fe) = SOME (s,fe)`, 600SRW_TAC [][unify_eq_vars_def,ITSET_EMPTY]) 601 602val verify_fcs_empty = RWstore_thm( 603"verify_fcs_empty", 604`verify_fcs {} s = SOME {}`, 605SRW_TAC [][verify_fcs_def,ITSET_EMPTY]); 606 607val verify_fcs_FINITE = Q.store_thm( 608"verify_fcs_FINITE", 609`FINITE fe ��� (verify_fcs fe s = SOME ve) ��� FINITE ve`, 610Q_TAC SUFF_TAC 611`���fe. FINITE fe ��� ���ve. (verify_fcs fe s = SOME ve) ��� FINITE ve` 612THEN1 METIS_TAC [] THEN 613HO_MATCH_MP_TAC FINITE_INDUCT THEN 614SRW_TAC [] [verify_fcs_def,ITSET_EMPTY] THEN 615SRW_TAC [][] THEN POP_ASSUM MP_TAC THEN 616FULL_SIMP_TAC (srw_ss()) [DELETE_NON_ELEMENT,fcs_acc_RECURSES] THEN 617Cases_on `e` THEN ASM_SIMP_TAC (srw_ss()) [fcs_acc_def] THEN 618SRW_TAC [][] THEN SRW_TAC [][] THEN IMP_RES_TAC term_fcs_FINITE); 619 620val verify_fcs_covers_all = Q.store_thm( 621"verify_fcs_covers_all", 622`FINITE fe ��� (verify_fcs fe s = SOME ve) ��� (a,v) ��� fe ��� 623 ���fcs. (term_fcs a (nwalk* s (Sus [] v)) = SOME fcs) ��� fcs SUBSET ve`, 624Q_TAC SUFF_TAC 625`���fe. FINITE fe ��� ���ve. (verify_fcs fe s = SOME ve) ��� (a,v) ��� fe ��� 626 ���fcs. (term_fcs a (nwalk* s (Sus [] v)) = SOME fcs) ��� fcs SUBSET ve` 627THEN1 METIS_TAC [] THEN 628HO_MATCH_MP_TAC FINITE_INDUCT THEN 629SRW_TAC [] [verify_fcs_def,ITSET_EMPTY] THEN1 ( 630 POP_ASSUM MP_TAC THEN 631 FULL_SIMP_TAC (srw_ss()) [DELETE_NON_ELEMENT,fcs_acc_RECURSES,fcs_acc_def] THEN 632 SRW_TAC [][] THEN FULL_SIMP_TAC (srw_ss()) [] ) THEN 633Q.PAT_X_ASSUM `X = SOME ve` MP_TAC THEN 634FULL_SIMP_TAC (srw_ss()) [DELETE_NON_ELEMENT,fcs_acc_RECURSES] THEN 635Cases_on `e` THEN SRW_TAC [][fcs_acc_def] THEN 636FULL_SIMP_TAC (srw_ss()) [] THEN METIS_TAC [SUBSET_TRANS,SUBSET_UNION]); 637 638val verify_fcs_minimal = Q.store_thm( 639"verify_fcs_minimal", 640`FINITE fe ��� (verify_fcs fe s = SOME ve) ��� (a,v) ��� ve ��� 641 ���b w fcs. (b,w) ��� fe ��� (term_fcs b (nwalk* s (Sus [] w)) = SOME fcs) ��� (a,v) ��� fcs`, 642Q_TAC SUFF_TAC 643`���fe. FINITE fe ��� ���ve. (verify_fcs fe s = SOME ve) ��� (a,v) ��� ve ��� 644 ���b w fcs. (b,w) ��� fe ��� (term_fcs b (nwalk* s (Sus [] w)) = SOME fcs) ��� (a,v) ��� fcs` 645THEN1 METIS_TAC [] THEN 646HO_MATCH_MP_TAC FINITE_INDUCT THEN 647ASM_SIMP_TAC (srw_ss()) [verify_fcs_def,ITSET_EMPTY] THEN 648SRW_TAC [][] THEN 649Q.PAT_X_ASSUM `X = SOME ve` MP_TAC THEN 650FULL_SIMP_TAC (srw_ss()) [DELETE_NON_ELEMENT,fcs_acc_RECURSES] THEN 651Cases_on `e` THEN SRW_TAC [][fcs_acc_def] THEN 652FULL_SIMP_TAC (srw_ss()) [] THEN METIS_TAC []); 653 654val verify_fcs_SOME = LIST_CONJ [verify_fcs_FINITE, verify_fcs_covers_all, verify_fcs_minimal]; 655 656val verify_fcs_NONE = Q.store_thm( 657"verify_fcs_NONE", 658`FINITE fe ��� (verify_fcs fe s = NONE) ��� 659 ���a v. (a,v) ��� fe ��� (term_fcs a (nwalk* s (Sus [] v)) = NONE)`, 660Q_TAC SUFF_TAC 661`���t. FINITE t ��� (verify_fcs t s = NONE) ��� 662 ���a v. (a,v) IN t ��� (term_fcs a (nwalk* s (Sus [] v)) = NONE)` 663THEN1 METIS_TAC [] THEN 664HO_MATCH_MP_TAC FINITE_INDUCT THEN 665SIMP_TAC (srw_ss()) [verify_fcs_def,ITSET_EMPTY] THEN 666SRW_TAC [][] THEN 667Q.PAT_X_ASSUM `FINITE t` ASSUME_TAC THEN 668Q.PAT_X_ASSUM `e NOTIN fcs` ASSUME_TAC THEN 669FULL_SIMP_TAC (srw_ss()) [fcs_acc_RECURSES,DELETE_NON_ELEMENT] THEN 670Cases_on `e` THEN SRW_TAC [][] THEN 671FULL_SIMP_TAC (srw_ss()) [fcs_acc_def] THEN 672METIS_TAC []); 673 674val verify_fcs_INSERT = Q.store_thm( 675"verify_fcs_INSERT", 676`FINITE fe ��� 677 (verify_fcs fe s = SOME ve) ��� 678 (term_fcs a (nwalk* s (Sus [] v)) = SOME fcs) ��� 679 (verify_fcs ((a,v) INSERT fe) s = SOME (ve ��� fcs))`, 680SRW_TAC [][verify_fcs_def,fcs_acc_RECURSES,fcs_acc_def] THEN 681REVERSE (Cases_on `(a,v) ��� fe`) THEN1 ( 682 FULL_SIMP_TAC (srw_ss()) [DELETE_NON_ELEMENT] ) THEN 683`(a,v) INSERT (fe DELETE (a,v)) = fe` by SRW_TAC [][] THEN 684(fcs_acc_RECURSES |> Q.INST [`e`|->`(a,v)`,`t`|->`fe DELETE (a,v)`,`b`|->`SOME {}`] |> 685 SIMP_RULE (srw_ss()) [fcs_acc_def] |> MP_TAC) THEN 686SRW_TAC [][] THEN SRW_TAC [][UNION_IDEMPOT,GSYM UNION_ASSOC]); 687 688val verify_fcs_decompose = Q.store_thm( 689"verify_fcs_decompose", 690`(verify_fcs ((a,v) INSERT fe) s = SOME ve) ��� FINITE fe ��� 691 ���ve0 fcs. 692 (verify_fcs fe s = SOME ve0) ��� 693 (term_fcs a (nwalk* s (Sus [] v)) = SOME fcs) ��� 694 (ve = ve0 ��� fcs)`, 695SRW_TAC [][] THEN 696Cases_on `(a,v) ��� fe` THEN1 ( 697 IMP_RES_TAC verify_fcs_SOME THEN 698 FULL_SIMP_TAC (srw_ss()) [ABSORPTION] THEN 699 RES_TAC THEN Q.EXISTS_TAC `fcs` THEN SRW_TAC [][] THEN 700 FULL_SIMP_TAC (srw_ss()) [SUBSET_DEF,EXTENSION] THEN METIS_TAC []) THEN 701FULL_SIMP_TAC (srw_ss()) [verify_fcs_def,fcs_acc_RECURSES,fcs_acc_def,DELETE_NON_ELEMENT]); 702 703val verify_fcs_UNION_I = Q.store_thm( 704"verify_fcs_UNION_I", 705`FINITE fe1 ��� FINITE fe2 ��� 706 (verify_fcs fe1 s = SOME ve1) ��� (verify_fcs fe2 s = SOME ve2) ��� 707 (verify_fcs (fe1 ��� fe2) s = SOME (ve1 ��� ve2))`, 708Q_TAC SUFF_TAC 709`���fe1. FINITE fe1 ��� 710 ���fe2 ve1 ve2. 711 FINITE fe2 ��� (verify_fcs fe1 s = SOME ve1) ��� (verify_fcs fe2 s = SOME ve2) ==> 712(verify_fcs (fe1 UNION fe2) s = SOME (ve1 ��� ve2))` THEN1 METIS_TAC [] THEN 713HO_MATCH_MP_TAC FINITE_INDUCT THEN SRW_TAC [][] THEN SRW_TAC [][] THEN 714`���ve0 fcs. (verify_fcs fe1 s = SOME ve0) ��� (ve1 = ve0 ��� fcs) ��� 715(term_fcs (FST e) (nwalk* s (Sus [] (SND e))) = SOME fcs)` by 716(Cases_on `e` THEN IMP_RES_TAC verify_fcs_decompose THEN 717 ASM_SIMP_TAC (srw_ss()) []) THEN 718FIRST_X_ASSUM (Q.SPECL_THEN [`fe2`,`ve0`,`ve2`] MP_TAC) THEN 719SRW_TAC [][INSERT_UNION_EQ] THEN 720Q.MATCH_ABBREV_TAC `X = SOME (ve0 ��� fcs ��� ve2)` THEN 721Q_TAC SUFF_TAC `X = SOME (ve0 ��� ve2 ��� fcs)` THEN1 METIS_TAC [UNION_COMM,UNION_ASSOC] THEN 722Q.UNABBREV_TAC `X` THEN 723Cases_on `e` THEN FULL_SIMP_TAC (srw_ss()) [] THEN 724MATCH_MP_TAC verify_fcs_INSERT THEN SRW_TAC [][]); 725 726val verify_fcs_UNION_E = Q.store_thm( 727"verify_fcs_UNION_E", 728`FINITE (fe1 ��� fe2) ��� 729(verify_fcs (fe1 ��� fe2) s = SOME ve) ��� 730 ���ve1 ve2. 731 (verify_fcs fe1 s = SOME ve1) ��� 732 (verify_fcs fe2 s = SOME ve2) ��� 733 (ve = ve1 ��� ve2)`, 734Q_TAC SUFF_TAC 735`���fe1. FINITE fe1 ��� 736 ���fe2 ve. FINITE fe2 ��� (verify_fcs (fe1 ��� fe2) s = SOME ve) ��� 737 ���ve1 ve2. (verify_fcs fe1 s = SOME ve1) ��� 738 (verify_fcs fe2 s = SOME ve2) ��� 739 (ve = ve1 ��� ve2)` THEN1 METIS_TAC [FINITE_UNION] THEN 740HO_MATCH_MP_TAC FINITE_INDUCT THEN SRW_TAC [][] THEN 741`���ve0 fcs. (verify_fcs (fe1 ��� fe2) s = SOME ve0) ��� (ve = ve0 ��� fcs) ��� 742(term_fcs (FST e) (nwalk* s (Sus [] (SND e))) = SOME fcs)` by ( 743 FULL_SIMP_TAC (srw_ss()) [INSERT_UNION_EQ] THEN 744 `FINITE (fe1 ��� fe2)` by METIS_TAC [FINITE_UNION] THEN 745 Cases_on `e` THEN IMP_RES_TAC verify_fcs_decompose THEN 746 ASM_SIMP_TAC (srw_ss()) []) THEN 747FIRST_X_ASSUM (Q.SPECL_THEN [`fe2`,`ve0`] MP_TAC) THEN 748SRW_TAC [][] THEN 749Cases_on `e` THEN FULL_SIMP_TAC (srw_ss()) [] THEN 750Q.EXISTS_TAC `ve1 ��� fcs` THEN SRW_TAC [][] THEN1 ( 751 MATCH_MP_TAC verify_fcs_INSERT THEN SRW_TAC [][] ) THEN 752METIS_TAC [UNION_COMM,UNION_ASSOC]); 753 754val verify_fcs_UNION = Q.store_thm( 755"verify_fcs_UNION", 756`FINITE fe1 ��� FINITE fe2 ��� 757 ((���ve1 ve2. (verify_fcs fe1 s = SOME ve1) ��� (verify_fcs fe2 s = SOME ve2) ��� (ve = ve1 ��� ve2)) ��� 758 (verify_fcs (fe1 ��� fe2) s = SOME ve))`, 759SRW_TAC [][EQ_IMP_THM] THEN1 760METIS_TAC [verify_fcs_UNION_I] THEN 761IMP_RES_TAC FINITE_UNION THEN 762METIS_TAC [verify_fcs_UNION_E]); 763 764val fresh_verify_fcs = Q.store_thm( 765"fresh_verify_fcs", 766`nwfs s ��� fresh fe a t ��� FINITE fe ��� 767 (verify_fcs fe s = SOME fex) 768 ��� fresh fex a (nwalk* s t)`, 769Induct_on `t` THEN SRW_TAC [][] THEN 770FULL_SIMP_TAC (psrw_ss()) [fresh_def] THEN 771`���fcs. fresh fcs a (apply_pi (REVERSE (REVERSE l)) (nwalk* s (Sus [] n))) ��� fcs SUBSET fex` 772by METIS_TAC [verify_fcs_SOME,term_fcs_fresh,term_fcs_minimal,lemma27,verify_fcs_covers_all] THEN 773Q.PAT_X_ASSUM `nwfs s` ASSUME_TAC THEN 774FULL_SIMP_TAC (psrw_ss()) [GSYM nwalkstar_apply_pi] THEN 775Cases_on `nvwalk s l n` THEN FULL_SIMP_TAC (psrw_ss()) [fresh_def] THEN1 ( 776FULL_SIMP_TAC (srw_ss()) [SUBSET_DEF] ) THEN 777METIS_TAC [fresh_extra_fcs]); 778 779val nwalkstar_subterm_exists = Q.store_thm( 780"nwalkstar_subterm_exists", 781`nwfs s ��� ���t. (���a c. (nwalk* s t = Tie a c) ��� 782 ���t2. nwalk* s t2 = c) ��� 783 (���c1 c2. (nwalk* s t = nPair c1 c2) ��� 784 (���t2. nwalk* s t2 = c1) ��� 785 (���t2. nwalk* s t2 = c2))`, 786STRIP_TAC THEN HO_MATCH_MP_TAC nwalkstar_ind THEN SRW_TAC [][] THEN 787Q.PAT_X_ASSUM `nwfs s` ASSUME_TAC THEN Cases_on `t` THEN 788FULL_SIMP_TAC (srw_ss()) [] THENL [ 789 Cases_on `nvwalk s l n` THEN FULL_SIMP_TAC (srw_ss()) [], ALL_TAC, 790 Cases_on `nvwalk s l n` THEN FULL_SIMP_TAC (srw_ss()) [], ALL_TAC, 791 Cases_on `nvwalk s l n` THEN FULL_SIMP_TAC (srw_ss()) [], ALL_TAC 792] THEN METIS_TAC []); 793 794val equiv_verify_fcs = Q.store_thm( 795"equiv_verify_fcs", 796`equiv fe t1 t2 ��� nwfs s ��� FINITE fe ��� (verify_fcs fe s = SOME fex) ��� 797 equiv fex (nwalk* s t1) (nwalk* s t2)`, 798MAP_EVERY Q.ID_SPEC_TAC [`t2`,`t1`] THEN 799SIMP_TAC (srw_ss()) [GSYM AND_IMP_INTRO] THEN 800HO_MATCH_MP_TAC equiv_ind THEN 801SRW_TAC [][] THEN1 ( 802 (nvwalk_modulo_pi |> Q.SPECL_THEN [`s`,`p1`,`v`] MP_TAC) THEN 803 (nvwalk_modulo_pi |> Q.SPECL_THEN [`s`,`p2`,`v`] MP_TAC) THEN 804 SRW_TAC [][] THEN 805 (fresh_ds_equiv |> GEN_ALL |> Q.SPECL [`nwalk* s (Sus [] v)`,`p2`,`p1`,`fex`] |> MP_TAC) THEN 806 ASM_SIMP_TAC (psrw_ss()) [GSYM nwalkstar_apply_pi] THEN 807 STRIP_TAC THEN POP_ASSUM MATCH_MP_TAC THEN 808 SRW_TAC [][] THEN RES_TAC THEN 809 IMP_RES_TAC verify_fcs_SOME THEN 810 IMP_RES_TAC term_fcs_fresh THEN 811 IMP_RES_TAC fresh_extra_fcs THEN 812 POP_ASSUM MP_TAC THEN 813 ASM_SIMP_TAC (srw_ss()) [] ) 814THEN1 ( 815 SRW_TAC [][Once equiv_cases] THEN 816 FIRST_X_ASSUM MATCH_MP_TAC THEN 817 SRW_TAC [][] THEN 818 METIS_TAC [nwalkstar_subterm_exists] ) 819THEN1 ( 820 SRW_TAC [][Once equiv_cases] THEN 821 FULL_SIMP_TAC (srw_ss()) [nwalkstar_apply_pi] THEN 822 IMP_RES_TAC fresh_verify_fcs ) 823THEN1 ( 824 SRW_TAC [][Once equiv_cases] THEN 825 FIRST_X_ASSUM MATCH_MP_TAC THEN 826 SRW_TAC [][] THEN 827 METIS_TAC [nwalkstar_subterm_exists] )) 828 829val nunify_FINITE_fe = Q.store_thm( 830"nunify_FINITE_fe", 831`���s fe t1 t2 sx fex. nwfs s ��� FINITE fe ��� (nunify (s,fe) t1 t2 = SOME (sx,fex)) ��� 832 FINITE fex`, 833HO_MATCH_MP_TAC nunify_ind THEN 834REPEAT STRIP_TAC THEN 835Cases_on `nwalk s t1` THEN Cases_on `nwalk s t2` THEN 836FULL_SIMP_TAC (srw_ss()) [] THEN 837SRW_TAC [][] THEN 838Q.PAT_X_ASSUM `nunify X Y Z = XX` MP_TAC THEN 839ASM_SIMP_TAC (srw_ss()) [Once nunify_def,LET_THM,nvwalk_case_thms] THEN 840SRW_TAC [][] THEN SRW_TAC [][] THENL [ 841 METIS_TAC [unify_eq_vars_SOME,FINITE_dis_set,unify_eq_vars_preserves_s], 842 METIS_TAC [term_fcs_FINITE], 843 Cases_on `x` THEN FULL_SIMP_TAC (srw_ss()) [] THEN 844 METIS_TAC [nunify_uP,uP_def] 845]); 846 847val fresh_SUBMAP = Q.store_thm( 848"fresh_SUBMAP", 849`fresh fcs a (nwalk* s t) ��� nwfs s ��� ���fe. fresh fe a t ��� ���b w. (b,w) ��� fe ��� fresh fcs b (nwalk* s (Sus [] w))`, 850Induct_on `t` THEN SRW_TAC [][] THEN 851FULL_SIMP_TAC (psrw_ss()) [fresh_def] THENL [ 852 Q.EXISTS_TAC `{}` THEN SRW_TAC [][], 853 Q.HO_MATCH_ABBREV_TAC `���fe. X ��� fe ��� Z fe` THEN 854 Q.EXISTS_TAC `{X}` THEN 855 UNABBREV_ALL_TAC THEN 856 SRW_TAC [][] THEN 857 (fresh_apply_pi |> Q.INST [`pi`|->`REVERSE l`,`t`|->`nwalk* s (Sus l n)`] |> MP_TAC) THEN 858 ASM_SIMP_TAC (psrw_ss()) [GSYM nwalkstar_apply_pi], 859 Q.EXISTS_TAC `{}` THEN SRW_TAC [][], 860 Q.EXISTS_TAC `fe ��� fe'` THEN SRW_TAC [][] THEN 861 METIS_TAC [fresh_extra_fcs,SUBSET_UNION], 862 Q.EXISTS_TAC `{}` THEN SRW_TAC [][] ]) 863 864val equiv_SUBSET = Q.store_thm( 865"equiv_SUBSET", 866`equiv fe t1 t2 ��� fe SUBSET fex ��� equiv fex t1 t2`, 867SIMP_TAC (srw_ss()) [GSYM AND_IMP_INTRO] THEN 868MAP_EVERY Q.ID_SPEC_TAC [`t2`,`t1`] THEN 869HO_MATCH_MP_TAC equiv_ind THEN 870SRW_TAC [][] THEN 871SRW_TAC [][Once equiv_cases] THEN1 ( 872MAP_EVERY Q.EXISTS_TAC [`p1`,`p2`] THEN 873SRW_TAC [][] THEN METIS_TAC [SUBSET_DEF] ) THEN 874METIS_TAC [fresh_extra_fcs]) 875 876val fresh_drop_NOTIN_nvars = Q.store_thm( 877"fresh_drop_NOTIN_nvars", 878`fresh fe a t ��� v NOTIN nvars t ��� fresh (fe DIFF {(b,u) | u = v}) a t`, 879Induct_on `t` THEN SRW_TAC [][fresh_def] THEN SRW_TAC [][]) 880 881val term_fcs_IN_nvars = Q.store_thm( 882"term_fcs_IN_nvars", 883`(term_fcs a t = SOME fe) ��� (b,v) IN fe ��� v IN nvars t`, 884SRW_TAC [][] THEN 885`fresh fe a t` by IMP_RES_TAC term_fcs_fresh THEN 886SPOSE_NOT_THEN STRIP_ASSUME_TAC THEN 887IMP_RES_TAC fresh_drop_NOTIN_nvars THEN 888POP_ASSUM (Q.SPEC_THEN `b` STRIP_ASSUME_TAC) THEN 889IMP_RES_TAC term_fcs_minimal THEN 890FULL_SIMP_TAC (srw_ss()) [SUBSET_DEF]) 891 892val fresh_drop_IN_FDOM = Q.store_thm( 893"fresh_drop_IN_FDOM", 894`nwfs s ��� fresh fe a (nwalk* s t) ��� v IN FDOM s ��� fresh (fe DIFF {(b,u) | u = v}) a (nwalk* s t)`, 895SRW_TAC [][] THEN 896Q_TAC SUFF_TAC `v NOTIN nvars (nwalk* s t)` THEN1 SRW_TAC [][fresh_drop_NOTIN_nvars] THEN 897SRW_TAC [][GSYM noc_eq_nvars_nwalkstar,IN_DEF] THEN 898METIS_TAC [noc_NOTIN_FDOM]) 899 900val term_fcs_NOTIN_FDOM = Q.store_thm( 901"term_fcs_NOTIN_FDOM", 902`nwfs s ��� (term_fcs a (nwalk* s t) = SOME fe) ��� (b,v) IN fe ��� v NOTIN FDOM s`, 903SRW_TAC [][] THEN 904`fresh fe a (nwalk* s t)` by IMP_RES_TAC term_fcs_fresh THEN 905SPOSE_NOT_THEN STRIP_ASSUME_TAC THEN 906IMP_RES_TAC fresh_drop_IN_FDOM THEN 907POP_ASSUM (Q.SPEC_THEN `b` STRIP_ASSUME_TAC) THEN 908IMP_RES_TAC term_fcs_minimal THEN 909FULL_SIMP_TAC (srw_ss()) [SUBSET_DEF]) 910 911val verify_fcs_NOTIN_FDOM = Q.store_thm( 912"verify_fcs_NOTIN_FDOM", 913`(verify_fcs fe s = SOME ve) ��� (a,v) ��� ve ��� nwfs s ��� FINITE fe ��� v ��� FDOM s`, 914STRIP_TAC THEN IMP_RES_TAC verify_fcs_SOME THEN 915IMP_RES_TAC term_fcs_NOTIN_FDOM) 916 917val verify_fcs_SUBSET = Q.store_thm( 918"verify_fcs_SUBSET", 919`FINITE fex ��� (verify_fcs fex s = SOME vex) ��� fe SUBSET fex ��� 920 ���ve. (verify_fcs fe s = SOME ve) ��� ve SUBSET vex`, 921SRW_TAC [][] THEN 922IMP_RES_TAC SUBSET_FINITE THEN 923Cases_on `verify_fcs fe s` THEN SRW_TAC [][] THEN1 ( 924 IMP_RES_TAC verify_fcs_NONE THEN 925 IMP_RES_TAC SUBSET_DEF THEN 926 IMP_RES_TAC verify_fcs_covers_all THEN 927 FULL_SIMP_TAC (srw_ss()) []) THEN 928FULL_SIMP_TAC (srw_ss()) [SUBSET_DEF,FORALL_PROD] THEN 929SRW_TAC [][] THEN 930`���b w fcs. (b,w) ��� fe ��� (term_fcs b (nwalk* s (Sus [] w)) = SOME fcs) ��� (p_1,p_2) ��� fcs` 931by METIS_TAC [verify_fcs_minimal] THEN 932`fcs SUBSET vex` by METIS_TAC [verify_fcs_covers_all,optionTheory.SOME_11] THEN 933FULL_SIMP_TAC (srw_ss()) [SUBSET_DEF]) 934 935val term_fcs_apply_pi = Q.store_thm( 936"term_fcs_apply_pi", 937`(term_fcs a t = SOME fcs) ��� 938 (term_fcs (lswapstr pi a) (apply_pi pi t) = SOME fcs)`, 939Q.ID_SPEC_TAC `fcs` THEN 940Induct_on `t` THEN SRW_TAC [][] THEN1 ( 941 FULL_SIMP_TAC (srw_ss()) [term_fcs_def] ) 942THEN1 ( 943 FULL_SIMP_TAC (psrw_ss()) [term_fcs_def, REVERSE_APPEND] THEN 944 SRW_TAC [][GSYM pmact_decompose] THEN 945 SIMP_TAC (psrw_ss()) [] ) 946THEN1 ( 947 SRW_TAC [][Once term_fcs_def] THEN1 ( 948 FULL_SIMP_TAC (srw_ss()) [Once term_fcs_def] ) THEN 949 Q.PAT_X_ASSUM `term_fcs a X = SOME fcs` MP_TAC THEN 950 SRW_TAC [][Once term_fcs_def]) 951THEN1 ( 952 SRW_TAC [][Once term_fcs_def] THEN 953 Q.PAT_X_ASSUM `term_fcs a X = SOME fcs` MP_TAC THEN 954 SRW_TAC [][Once term_fcs_def] THEN 955 FULL_SIMP_TAC (srw_ss()) []) THEN 956FULL_SIMP_TAC (srw_ss()) [term_fcs_def]) 957 958val term_fcs_nwalkstar = Q.store_thm( 959"term_fcs_nwalkstar", 960`nwfs s ��� 961 (term_fcs b t = SOME fcs) ��� 962 (term_fcs b (nwalk* s t) = SOME fcs2) ��� 963 (a,v) ��� fcs ��� 964 ���fcs1. (term_fcs a (nwalk* s (Sus [] v)) = SOME fcs1) ��� 965 fcs1 ��� fcs2`, 966STRIP_TAC THEN 967NTAC 4 (POP_ASSUM MP_TAC) THEN 968SPEC_ALL_TAC [`t`,`s`] THEN 969Q.ID_SPEC_TAC `t` THEN HO_MATCH_MP_TAC nwalkstar_ind THEN 970REPEAT STRIP_TAC THEN 971`nwalk* s t = nwalk* s (nwalk s t)` by METIS_TAC [nwalkstar_nwalk] THEN 972Cases_on `nwalk s t` THEN 973Q.PAT_X_ASSUM `nwfs s` ASSUME_TAC THEN 974FULL_SIMP_TAC (srw_ss()) [] THEN1 ( 975 Q.PAT_X_ASSUM `term_fcs X Y = SOME fcs2` MP_TAC THEN 976 SRW_TAC [][Once term_fcs_def] THEN 977 Cases_on `t` THEN FULL_SIMP_TAC (psrw_ss()) [Once term_fcs_def] THEN 978 SRW_TAC [][] THEN FULL_SIMP_TAC (srw_ss()) [] THEN 979 (nvwalk_modulo_pi |> Q.SPECL [`s`,`l`,`n`] |> GSYM |> MP_TAC) THEN 980 SRW_TAC [][apply_pi_eql] ) 981THEN1 ( 982 `n ��� FDOM s` by METIS_TAC [nwalk_to_var] THEN 983 Cases_on `t` THEN 984 FULL_SIMP_TAC (psrw_ss()) [NOT_FDOM_nvwalk,Once term_fcs_def,EXTENSION] THEN 985 RES_TAC THEN FULL_SIMP_TAC (srw_ss()) [] THEN 986 (nvwalk_modulo_pi |> Q.SPECL [`s`,`l'`,`n'`] |> GSYM |> MP_TAC) THEN 987 ASM_SIMP_TAC (psrw_ss()) [apply_pi_eql] THEN 988 SRW_TAC [][REVERSE_APPEND,pmact_decompose] THEN 989 METIS_TAC [] ) 990THEN1 ( 991 Q.PAT_X_ASSUM `term_fcs X Y = SOME fcs2` MP_TAC THEN 992 SRW_TAC [][Once term_fcs_def] THEN1 ( 993 Cases_on `t` THEN FULL_SIMP_TAC (psrw_ss()) [Once term_fcs_def] THEN 994 SRW_TAC [][] THEN FULL_SIMP_TAC (srw_ss()) [] THEN 995 (nvwalk_modulo_pi |> Q.SPECL [`s`,`l`,`n`] |> GSYM |> MP_TAC) THEN 996 SRW_TAC [][apply_pi_eql] THEN 997 SRW_TAC [][Once term_fcs_def]) THEN 998 Cases_on `t` THEN FULL_SIMP_TAC (psrw_ss()) [] THEN1 ( 999 Q.PAT_X_ASSUM `term_fcs b X = SOME fcs` MP_TAC THEN 1000 ASM_SIMP_TAC (psrw_ss()) [Once term_fcs_def,EXTENSION] THEN 1001 SRW_TAC [][] THEN RES_TAC THEN 1002 FULL_SIMP_TAC (srw_ss()) [] THEN 1003 (nvwalk_modulo_pi |> Q.SPECL [`s`,`l`,`n`] |> GSYM |> MP_TAC) THEN 1004 SRW_TAC [][apply_pi_eql] THEN 1005 SRW_TAC [][Once term_fcs_def,nwalkstar_apply_pi] THEN 1006 Q.EXISTS_TAC `fcs2` THEN SRW_TAC [][] THEN 1007 MATCH_MP_TAC term_fcs_apply_pi THEN SRW_TAC [][] ) THEN 1008 SRW_TAC [][] THEN 1009 Q.PAT_X_ASSUM `term_fcs b X = SOME fcs` MP_TAC THEN 1010 SRW_TAC [] [Once term_fcs_def] THEN 1011 METIS_TAC [] ) 1012THEN1 ( 1013 Q.PAT_X_ASSUM `term_fcs b Y = SOME fcs2` MP_TAC THEN 1014 SRW_TAC [][Once term_fcs_def] THEN 1015 Cases_on `t` THEN FULL_SIMP_TAC (srw_ss()) [] THEN1 ( 1016 Q.PAT_X_ASSUM `term_fcs b X = SOME fcs` MP_TAC THEN 1017 ASM_SIMP_TAC (psrw_ss()) [Once term_fcs_def,EXTENSION] THEN 1018 SRW_TAC [][] THEN RES_TAC THEN 1019 FULL_SIMP_TAC (srw_ss()) [] THEN SRW_TAC [][] THEN 1020 (nvwalk_modulo_pi |> Q.SPECL [`s`,`l`,`n`] |> GSYM |> MP_TAC) THEN 1021 SRW_TAC [][apply_pi_eql] THEN 1022 SRW_TAC [][Once term_fcs_def,nwalkstar_apply_pi] THEN 1023 Q.EXISTS_TAC `x1 ��� x2` THEN SRW_TAC [][] THEN 1024 MAP_EVERY Q.EXISTS_TAC [`x1`,`x2`] THEN SRW_TAC [][] THEN 1025 MATCH_MP_TAC term_fcs_apply_pi THEN SRW_TAC [][] ) THEN 1026 SRW_TAC [][] THEN 1027 Q.PAT_X_ASSUM `term_fcs b X = SOME fcs` MP_TAC THEN 1028 SRW_TAC [] [Once term_fcs_def] THEN 1029 FULL_SIMP_TAC (srw_ss()) [] THEN 1030 RES_TAC THEN METIS_TAC [SUBSET_UNION,SUBSET_TRANS] ) 1031THEN 1032 Q.PAT_X_ASSUM `term_fcs b Y = SOME fcs2` MP_TAC THEN 1033 SRW_TAC [][Once term_fcs_def] THEN 1034 Cases_on `t` THEN FULL_SIMP_TAC (psrw_ss()) [Once term_fcs_def] THEN 1035 SRW_TAC [][] THEN FULL_SIMP_TAC (srw_ss()) [] THEN 1036 (nvwalk_modulo_pi |> Q.SPECL [`s`,`l`,`n`] |> GSYM |> MP_TAC) THEN 1037 SRW_TAC [][apply_pi_eql] ) 1038 1039val verify_fcs_SUBMAP = Q.store_thm( 1040"verify_fcs_SUBMAP", 1041`FINITE fe ��� (verify_fcs fe sx = SOME fex) ��� nwfs sx ��� s SUBMAP sx ��� 1042 ���fe1. (verify_fcs fe s = SOME fe1) ��� 1043 ���a v. (a,v) ��� fe1 ��� 1044���fcs. (term_fcs a (nwalk* sx (Sus [] v)) = SOME fcs) ��� fcs ��� fex`, 1045REPEAT STRIP_TAC THEN 1046Cases_on `verify_fcs fe s` THEN1 ( 1047 IMP_RES_TAC verify_fcs_NONE THEN 1048 IMP_RES_TAC term_fcs_NONE THEN 1049 IMP_RES_TAC verify_fcs_SOME THEN 1050 IMP_RES_TAC term_fcs_fresh THEN 1051 METIS_TAC [nwalkstar_SUBMAP,fresh_SUBMAP] ) THEN 1052Q.EXISTS_TAC `x` THEN SIMP_TAC (srw_ss()) [] THEN 1053REPEAT STRIP_TAC THEN 1054`���b w fcs. (b,w) ��� fe ��� (term_fcs b (nwalk* s (Sus [] w)) = SOME fcs) ��� (a,v) ��� fcs` 1055by METIS_TAC [verify_fcs_minimal] THEN 1056`���fcs2. (term_fcs b (nwalk* sx (Sus [] w)) = SOME fcs2) ��� fcs2 ��� fex` 1057by METIS_TAC[verify_fcs_covers_all] THEN 1058`���fcs. (term_fcs a (nwalk* sx (Sus [] v)) = SOME fcs) ��� fcs ��� fcs2` by ( 1059 MATCH_MP_TAC (GEN_ALL term_fcs_nwalkstar) THEN 1060 MAP_EVERY Q.EXISTS_TAC [`nwalk* s (Sus [] w)`,`fcs`,`b`] THEN 1061 SRW_TAC [][] THEN 1062 METIS_TAC [nwalkstar_SUBMAP] ) THEN 1063METIS_TAC [SUBSET_TRANS]) 1064 1065val verify_fcs_term_fcs = Q.store_thm( 1066"verify_fcs_term_fcs", 1067`(term_fcs a t = SOME fcs) ��� 1068 (term_fcs a (nwalk* s t) = SOME fex) ��� nwfs s ��� 1069 (verify_fcs fcs s = SOME fex)`, 1070MAP_EVERY Q.ID_SPEC_TAC [`fcs`,`fex`] THEN 1071Induct_on `t` THEN SRW_TAC [][] THEN 1072FULL_SIMP_TAC (srw_ss()) [] THEN1 ( 1073 FULL_SIMP_TAC (srw_ss()) [Once term_fcs_def] THEN 1074 SRW_TAC [][] ) 1075THEN1 ( 1076 Q.PAT_X_ASSUM `term_fcs a (Sus X Y) = Z` MP_TAC THEN 1077 ASM_SIMP_TAC (psrw_ss()) [term_fcs_def] THEN 1078 SRW_TAC [][] THEN 1079 SRW_TAC [][verify_fcs_def,fcs_acc_RECURSES,fcs_acc_def,ITSET_EMPTY] THEN 1080 (nwalkstar_apply_pi |> UNDISCH |> 1081 Q.SPEC `Sus [] n` |> Q.INST [`pi`|->`l`] |> 1082 DISCH_ALL |> 1083 SIMP_RULE (psrw_ss()) [] |> MP_TAC) THEN 1084 SRW_TAC [][] THEN FULL_SIMP_TAC (srw_ss()) [] THEN 1085 (term_fcs_apply_pi |> 1086 Q.INST [`t`|->`apply_pi l (nwalk* s (Sus [] n))`,`fcs`|->`fex`,`pi`|->`REVERSE l`] |> 1087 SIMP_RULE (srw_ss()) [] |> MP_TAC) THEN 1088 SRW_TAC [][]) 1089THEN1 ( 1090 Q.PAT_X_ASSUM `term_fcs a (Tie Y X) = SOME fcs` MP_TAC THEN 1091 ASM_SIMP_TAC (srw_ss()) [Once term_fcs_def] THEN 1092 Q.PAT_X_ASSUM `term_fcs a (Tie Y X) = SOME fex` MP_TAC THEN 1093 ASM_SIMP_TAC (srw_ss()) [Once term_fcs_def] THEN 1094 SRW_TAC [][] THEN SRW_TAC [][]) 1095THEN1 ( 1096 Q.PAT_X_ASSUM `term_fcs a X = SOME fcs` MP_TAC THEN 1097 ASM_SIMP_TAC (srw_ss()) [Once term_fcs_def] THEN 1098 Q.PAT_X_ASSUM `term_fcs a X = SOME fex` MP_TAC THEN 1099 ASM_SIMP_TAC (srw_ss()) [Once term_fcs_def] THEN 1100 SRW_TAC [][] THEN 1101 FULL_SIMP_TAC (srw_ss()) [] THEN 1102 IMP_RES_TAC term_fcs_SOME THEN 1103 SRW_TAC [][verify_fcs_UNION_I]) THEN 1104FULL_SIMP_TAC (srw_ss()) [term_fcs_def] THEN 1105SRW_TAC [][]) 1106 1107val verify_fcs_iter_SUBMAP = Q.store_thm( 1108"verify_fcs_iter_SUBMAP", 1109`(verify_fcs fe s = SOME ve0) ��� 1110 (verify_fcs fe sx = SOME ve) ��� 1111 s SUBMAP sx ��� nwfs sx ��� FINITE fe ��� 1112 (verify_fcs ve0 sx = SOME ve)`, 1113Q_TAC SUFF_TAC 1114`���fe. FINITE fe ��� ���ve0 ve. 1115 (verify_fcs fe s = SOME ve0) ��� 1116 (verify_fcs fe sx = SOME ve) ��� 1117 s SUBMAP sx ��� nwfs sx ��� 1118 (verify_fcs ve0 sx = SOME ve)` THEN1 METIS_TAC [] THEN 1119HO_MATCH_MP_TAC FINITE_INDUCT THEN 1120SRW_TAC [][] THEN SRW_TAC [][] THEN 1121Cases_on `e` THEN 1122IMP_RES_TAC verify_fcs_decompose THEN 1123FULL_SIMP_TAC (srw_ss()) [] THEN 1124SRW_TAC [][] THEN 1125Q_TAC SUFF_TAC 1126`verify_fcs fcs' sx = SOME fcs` THEN1 ( 1127 STRIP_TAC THEN 1128 IMP_RES_TAC term_fcs_SOME THEN 1129 IMP_RES_TAC verify_fcs_SOME THEN 1130 SRW_TAC [][verify_fcs_UNION_I]) THEN 1131MATCH_MP_TAC (GEN_ALL verify_fcs_term_fcs) THEN 1132MAP_EVERY Q.EXISTS_TAC [`nwalk* s (Sus [] r)`,`q`] THEN 1133METIS_TAC [nwalkstar_SUBMAP,nwfs_SUBMAP]) 1134 1135val verify_fcs_idem = Q.store_thm( 1136"verify_fcs_idem", 1137`nwfs s ��� FINITE fe ��� (verify_fcs fe s = SOME fex) ��� (verify_fcs fex s = SOME fex)`, 1138METIS_TAC [verify_fcs_iter_SUBMAP, SUBMAP_REFL]) 1139 1140val unify_eq_vars_adds_same_fcs = Q.store_thm( 1141"unify_eq_vars_adds_same_fcs", 1142`���ds. FINITE ds ��� ���fu. ���fe sx fex. (unify_eq_vars ds v (s,fe) = SOME (sx,fex)) ��� (fex = fe ��� fu)`, 1143HO_MATCH_MP_TAC FINITE_INDUCT THEN SRW_TAC [][] 1144THEN1 (Q.EXISTS_TAC `{}` THEN SRW_TAC [][]) THEN 1145Cases_on `term_fcs e (nwalk* s (Sus [] v))` THEN1 ( 1146 Q.EXISTS_TAC `{}` THEN SRW_TAC [][] THEN 1147 IMP_RES_TAC unify_eq_vars_decompose THEN 1148 FULL_SIMP_TAC (srw_ss()) [] ) THEN 1149Q.EXISTS_TAC `fu ��� x` THEN SRW_TAC [][] THEN 1150IMP_RES_TAC unify_eq_vars_decompose THEN 1151RES_TAC THEN FULL_SIMP_TAC (srw_ss()) [] THEN 1152METIS_TAC [UNION_ASSOC]); 1153 1154val unify_eq_vars_ignores_fe = Q.store_thm( 1155"unify_eq_vars_ignores_fe", 1156`(unify_eq_vars ds v (s,fe) = SOME (sx,fex)) ��� FINITE ds ��� 1157 ���fe'.���fex'. (unify_eq_vars ds v (s,fe') = SOME (s,fex'))`, 1158SRW_TAC [][] THEN 1159Cases_on `unify_eq_vars ds v (s,fe')` THEN1 ( 1160 IMP_RES_TAC unify_eq_vars_NONE THEN 1161 IMP_RES_TAC unify_eq_vars_preserves_s THEN 1162 SRW_TAC [][] THEN 1163 IMP_RES_TAC unify_eq_vars_SOME THEN 1164 RES_TAC) THEN 1165Cases_on `x` THEN 1166IMP_RES_TAC unify_eq_vars_preserves_s THEN 1167SRW_TAC [][]); 1168 1169val nunify_ignores_fe = Q.store_thm( 1170"nunify_ignores_fe", 1171`���s fe t1 t2 sx fex. 1172 nwfs s ��� (nunify (s,fe) t1 t2 = SOME (sx,fex)) ��� 1173 ���fe'. ���fex'. nunify (s,fe') t1 t2 = SOME (sx,fex')`, 1174HO_MATCH_MP_TAC nunify_ind THEN SRW_TAC [][] THEN 1175POP_ASSUM MP_TAC THEN 1176MAP_EVERY Cases_on [`nwalk s t1`,`nwalk s t2`] THEN 1177ASM_SIMP_TAC (psrw_ss()) [Once nunify_def,LET_THM] THEN SRW_TAC [][] THEN 1178ASM_SIMP_TAC (psrw_ss()) [Once nunify_def,LET_THM] THEN SRW_TAC [][] THEN1 ( 1179 `FINITE (dis_set l l')` by METIS_TAC [FINITE_dis_set] THEN 1180 IMP_RES_TAC unify_eq_vars_preserves_s THEN SRW_TAC [][] THEN 1181 IMP_RES_TAC unify_eq_vars_adds_same_fcs THEN 1182 POP_ASSUM (Q.SPECL_THEN [`n`,`s`] MP_TAC) THEN 1183 SRW_TAC [][] THEN 1184 Cases_on `unify_eq_vars (dis_set l l') n (s,fe')` THEN1 ( 1185 IMP_RES_TAC unify_eq_vars_ignores_fe THEN 1186 POP_ASSUM (Q.SPEC_THEN `fe'` MP_TAC) THEN SRW_TAC [][] ) THEN 1187 Cases_on `x` THEN FULL_SIMP_TAC (srw_ss()) [] THEN 1188 IMP_RES_TAC unify_eq_vars_preserves_s THEN SRW_TAC [][]) THEN 1189Q.PAT_X_ASSUM `unify X Y Z = Z2` ASSUME_TAC THEN 1190Q.PAT_X_ASSUM `nwfs s` ASSUME_TAC THEN 1191Cases_on `x` THEN FULL_SIMP_TAC (srw_ss()) [] THEN 1192`nwfs q` by METIS_TAC [nunify_uP,uP_def] THEN 1193Q.PAT_X_ASSUM `nunify (q,r) Y Z = X` ASSUME_TAC THEN 1194FULL_SIMP_TAC (srw_ss()) [] THEN 1195Q.MATCH_ASSUM_RENAME_TAC `nunify (s,fe) C2 C2' = SOME (q,r)` THEN 1196`���r'. nunify (s,fe') C2 C2' = SOME (q,r')` by METIS_TAC [] THEN 1197SRW_TAC [][]); 1198 1199val nunify_ignores_fe_NONE = Q.store_thm( 1200"nunify_ignores_fe_NONE", 1201`nwfs s ��� (nunify (s,fe) t1 t2 = NONE) ��� 1202 ���fe'. nunify (s,fe') t1 t2 = NONE`, 1203SRW_TAC [][] THEN 1204Cases_on `nunify (s,fe') t1 t2` THEN 1205SRW_TAC [][] THEN Cases_on `x` THEN 1206SRW_TAC [][] THEN 1207(nunify_ignores_fe |> 1208 Q.SPECL [`s`,`fe'`,`t1`,`t2`,`q`,`r`] |> 1209 MP_TAC) THEN 1210SRW_TAC [][] THEN Q.EXISTS_TAC `fe` THEN 1211SRW_TAC [][]); 1212 1213val nunify_adds_same_fcs = Q.store_thm( 1214"nunify_adds_same_fcs", 1215`nwfs s ��� 1216 ���fu. 1217 ���fe sx fex. 1218 (nunify (s,fe) t1 t2 = SOME (sx,fex)) ��� (fex = fe ��� fu)`, 1219Q_TAC SUFF_TAC 1220`���s (fe:fe) t1 t2. nwfs s ��� ���fu.���fe sx fex. (nunify (s,fe) t1 t2 = SOME (sx,fex)) 1221��� (fex = fe ��� fu)` THEN1 METIS_TAC [] THEN 1222HO_MATCH_MP_TAC nunify_ind THEN SRW_TAC [][] THEN 1223MAP_EVERY Cases_on [`nwalk s t1`,`nwalk s t2`] THEN 1224SRW_TAC [][] THEN SRW_TAC [][Once nunify_def,LET_THM] 1225THEN1 ( Q.EXISTS_TAC `{}` THEN SRW_TAC [][] ) 1226THEN1 ( Q.EXISTS_TAC `{}` THEN SRW_TAC [][] ) 1227THEN1 ( Q.EXISTS_TAC `{}` THEN SRW_TAC [][] ) 1228THEN1 ( 1229 ASM_SIMP_TAC (psrw_ss()) [] THEN 1230 Cases_on `n = n'` THEN SRW_TAC [][] THEN1 ( 1231 (unify_eq_vars_adds_same_fcs |> Q.SPEC `dis_set l l'` |> 1232 Q.INST [`v`|->`n`] |> MP_TAC) THEN 1233 SRW_TAC [][] ) THEN 1234 Q.EXISTS_TAC `{}` THEN SRW_TAC [][] ) 1235THEN1 ( Q.EXISTS_TAC `{}` THEN SRW_TAC [][] ) 1236THEN1 ( Q.EXISTS_TAC `{}` THEN SRW_TAC [][] ) 1237THEN1 ( Q.EXISTS_TAC `{}` THEN SRW_TAC [][] ) 1238THEN1 ( Q.EXISTS_TAC `{}` THEN SRW_TAC [][] ) 1239THEN1 ( 1240 Q.MATCH_ASSUM_RENAME_TAC `nwalk s t1 = Tie s1 C1` THEN 1241 Q.MATCH_ASSUM_RENAME_TAC `nwalk s t2 = Tie s2 C2` THEN 1242 Cases_on `s1 = s2` THEN SRW_TAC [][] THEN 1243 Q.PAT_X_ASSUM `nwfs s` ASSUME_TAC THEN 1244 FULL_SIMP_TAC (srw_ss()) [] THEN 1245 Cases_on `term_fcs s1 (nwalk* s C2)` THEN 1246 FULL_SIMP_TAC (srw_ss()) [] THEN 1247 Q.EXISTS_TAC `fu ��� x` THEN SRW_TAC [][] THEN 1248 METIS_TAC [UNION_ASSOC,UNION_COMM] ) 1249THEN1 (Q.EXISTS_TAC `{}` THEN SRW_TAC [][] ) 1250THEN1 ( 1251 Q.MATCH_ASSUM_RENAME_TAC `nwalk s t1 = nPair t1a t1d` THEN 1252 Q.MATCH_ASSUM_RENAME_TAC `nwalk s t2 = nPair t2a t2d` THEN 1253 Cases_on `nunify (s,fe) t1a t2a` THEN 1254 Q.PAT_X_ASSUM `nwfs s` ASSUME_TAC THEN 1255 FULL_SIMP_TAC (srw_ss()) [] THEN1 ( 1256 IMP_RES_TAC nunify_ignores_fe_NONE THEN 1257 FULL_SIMP_TAC (srw_ss()) [] ) THEN 1258 Cases_on `x` THEN FULL_SIMP_TAC (srw_ss()) [] THEN 1259 `nwfs q` by METIS_TAC [nunify_uP,uP_def] THEN 1260 FULL_SIMP_TAC (srw_ss()) [] THEN 1261 IMP_RES_TAC nunify_ignores_fe THEN 1262 Q.EXISTS_TAC `fu ��� fu'` THEN SRW_TAC [][] THEN 1263 Cases_on `x` THEN FULL_SIMP_TAC (srw_ss()) [] THEN 1264 FIRST_X_ASSUM (Q.SPEC_THEN `fe'` MP_TAC) THEN 1265 SRW_TAC [][] THEN RES_TAC THEN 1266 METIS_TAC [UNION_ASSOC] ) 1267THEN1 (Q.EXISTS_TAC `{}` THEN SRW_TAC [][] ) 1268THEN1 (Q.EXISTS_TAC `{}` THEN SRW_TAC [][] )); 1269 1270val nomunify_unifier = Q.store_thm( 1271"nomunify_unifier", 1272`nwfs s ��� FINITE fe ��� (nomunify (s,fe) t1 t2 = SOME (sx,fex)) ==> 1273 FINITE fex ��� nwfs sx ��� s SUBMAP sx ��� (equiv fex (nwalk* sx t1) (nwalk* sx t2))`, 1274Q_TAC SUFF_TAC 1275`!s fe t1 t2 sx fex. nwfs s ��� FINITE fe ��� (nomunify (s,fe) t1 t2 = SOME (sx,fex)) ==> 1276 (equiv fex (nwalk* sx t1) (nwalk* sx t2))` 1277THEN1 (SIMP_TAC (srw_ss()) [nomunify_def] THEN 1278 STRIP_TAC THEN REPEAT GEN_TAC THEN 1279 STRIP_TAC THEN 1280 Cases_on `x` THEN FULL_SIMP_TAC (srw_ss()) [] THEN 1281 CONJ1_TAC THEN1 METIS_TAC [nunify_FINITE_fe,verify_fcs_SOME] THEN 1282 CONJ1_TAC THEN1 METIS_TAC [nunify_uP,uP_def] THEN 1283 CONJ1_TAC THEN1 METIS_TAC [nunify_uP,uP_def] THEN 1284 FIRST_X_ASSUM (Q.SPEC_THEN `s` (MP_TAC o SPEC_ALL)) THEN 1285 SRW_TAC [][] ) THEN 1286HO_MATCH_MP_TAC nunify_ind THEN SRW_TAC [][nomunify_def,UNCURRY] THEN 1287`���sx fx0. x = (sx,fx0)` by (Cases_on `x` THEN SRW_TAC [][]) THEN SRW_TAC [][] THEN 1288`nwfs sx /\ s SUBMAP sx` by METIS_TAC [nunify_uP,uP_def] THEN 1289FULL_SIMP_TAC (srw_ss()) [EXISTS_PROD] THEN 1290Q.PAT_X_ASSUM `nunify p t1 t2 = SOME px` MP_TAC THEN 1291Cases_on `nwalk s t1` THEN Cases_on `nwalk s t2` THEN 1292ASM_SIMP_TAC (psrw_ss()) [Once nunify_def,nvwalk_case_thms,LET_THM] THEN 1293SRW_TAC [][] THEN1 ( 1294 Q.PAT_X_ASSUM `nwfs s` ASSUME_TAC THEN 1295 Cases_on `t1` THEN Cases_on `t2` THEN 1296 FULL_SIMP_TAC (srw_ss()) [nwalk_def,nvwalk_case_thms,Once equiv_cases]) THEN1 ( 1297 Q.MATCH_ABBREV_TAC `equiv fex (nwalk* sx t1) (nwalk* sx t2)` THEN 1298 `(nwalk* sx t1 = nwalk* sx (nwalk s t1)) /\ 1299 (nwalk* sx t2 = nwalk* sx (nwalk s t2))` 1300 by METIS_TAC [nwalkstar_nwalk_SUBMAP] THEN 1301 Q.PAT_X_ASSUM `nwfs s` MP_TAC THEN 1302 MP_TAC (Q.INST[`t`|->`t1`]nwalk_SUBMAP) THEN 1303 MP_TAC (Q.INST[`t`|->`t2`]nwalk_SUBMAP) THEN 1304 NTAC 2 (POP_ASSUM MP_TAC) THEN SRW_TAC [][] THEN 1305 FIRST_X_ASSUM (Q.SPEC_THEN `l` MP_TAC) THEN SRW_TAC [][] THEN 1306 `nvwalk sx l n = Nom s'` 1307 by (ASM_SIMP_TAC (psrw_ss()) [Once nvwalk_def,Abbr`sx`,FLOOKUP_UPDATE]) THEN 1308 FULL_SIMP_TAC (srw_ss()) []) THEN1 ( 1309 Q.MATCH_ABBREV_TAC `equiv fex (nwalk* sx t1) (nwalk* sx t2)` THEN 1310 `(nwalk* sx t1 = nwalk* sx (nwalk s t1)) /\ 1311 (nwalk* sx t2 = nwalk* sx (nwalk s t2))` 1312 by METIS_TAC [nwalkstar_nwalk_SUBMAP] THEN 1313 Q.PAT_X_ASSUM `nwfs s` MP_TAC THEN 1314 MP_TAC (Q.INST[`t`|->`t1`]nwalk_SUBMAP) THEN 1315 MP_TAC (Q.INST[`t`|->`t2`]nwalk_SUBMAP) THEN 1316 NTAC 2 (POP_ASSUM MP_TAC) THEN SRW_TAC [][] THEN 1317 FIRST_X_ASSUM (Q.SPEC_THEN `l` MP_TAC) THEN SRW_TAC [][] THEN 1318 `nvwalk sx l n = Nom s'` 1319 by (ASM_SIMP_TAC (psrw_ss()) [Once nvwalk_def,Abbr`sx`,FLOOKUP_UPDATE]) THEN 1320 FULL_SIMP_TAC (srw_ss()) []) THEN1 ( 1321 `s = sx` by METIS_TAC [unify_eq_vars_preserves_s,FINITE_dis_set] THEN 1322 SRW_TAC [][] THEN 1323 `equiv fx0 (nwalk* s t1) (nwalk* s t2)` 1324 by (IMP_RES_TAC unify_eq_vars_equiv THEN 1325 METIS_TAC [nwalkstar_nwalk]) THEN 1326 `FINITE fx0` by METIS_TAC [unify_eq_vars_SOME,FINITE_dis_set] THEN 1327 METIS_TAC [verify_fcs_SOME,equiv_verify_fcs,nwalkstar_idempotent]) THEN1 ( 1328 Q.MATCH_ABBREV_TAC `equiv fex (nwalkstar sx t1) (nwalkstar sx t2)` THEN 1329 IMP_RES_TAC nwalk_to_var THEN SRW_TAC [][] THEN 1330 IMP_RES_TAC NOT_FDOM_nvwalk THEN 1331 Q.PAT_X_ASSUM `nwfs s` ASSUME_TAC THEN FULL_SIMP_TAC (srw_ss()) [] THEN 1332 SRW_TAC [][] THEN 1333 Q.MATCH_ASSUM_RENAME_TAC `nvwalk s p1 u1 = Sus l n` THEN 1334 Q.MATCH_ASSUM_RENAME_TAC `nvwalk s p2 u2 = Sus l' n'` THEN 1335 MP_TAC (Q.SPECL [`p1`,`u1`,`s`] (Q.INST [`pu`|->`l`,`u`|->`n`] (UNDISCH nvwalk_SUBMAP_var))) THEN 1336 MP_TAC (Q.SPECL [`p2`,`u2`,`s`] (Q.INST [`pu`|->`l'`,`u`|->`n'`] (UNDISCH nvwalk_SUBMAP_var))) THEN 1337 SRW_TAC [][] THEN 1338 SRW_TAC [][Once nvwalk_def,FLOOKUP_UPDATE,nvwalk_case_thms,Abbr`sx`] THEN 1339 ASM_SIMP_TAC (psrw_ss()) [] ) THEN1 ( 1340 Q.MATCH_ABBREV_TAC `equiv fex (nwalkstar sx t1) (nwalkstar sx t2)` THEN 1341 `(nwalkstar sx t1 = nwalkstar sx (nwalk s t1)) /\ 1342 (nwalkstar sx t2 = nwalkstar sx (nwalk s t2))` 1343 by METIS_TAC [nwalkstar_nwalk_SUBMAP] THEN 1344 Q.PAT_X_ASSUM `nwfs s` MP_TAC THEN 1345 MP_TAC (Q.INST[`t`|->`t1`]nwalk_SUBMAP) THEN 1346 MP_TAC (Q.INST[`t`|->`t2`]nwalk_SUBMAP) THEN 1347 NTAC 2 (POP_ASSUM MP_TAC) THEN SRW_TAC [][] THEN 1348 FIRST_X_ASSUM (Q.SPEC_THEN `l` MP_TAC) THEN SRW_TAC [][] THEN 1349 Cases_on `t1` THEN FULL_SIMP_TAC (srw_ss()) [] THEN 1350 Q.PAT_X_ASSUM `nwfs sx` ASSUME_TAC THEN FULL_SIMP_TAC (psrw_ss()) [] THEN 1351 SRW_TAC [][Abbr`sx`,Once nvwalk_def,FLOOKUP_UPDATE] ) THEN1 ( 1352 Q.MATCH_ABBREV_TAC `equiv fex (nwalkstar sx t1) (nwalkstar sx t2)` THEN 1353 `(nwalkstar sx t1 = nwalkstar sx (nwalk s t1)) /\ 1354 (nwalkstar sx t2 = nwalkstar sx (nwalk s t2))` 1355 by METIS_TAC [nwalkstar_nwalk_SUBMAP] THEN 1356 Q.PAT_X_ASSUM `nwfs s` MP_TAC THEN 1357 MP_TAC (Q.INST[`t`|->`t1`]nwalk_SUBMAP) THEN 1358 MP_TAC (Q.INST[`t`|->`t2`]nwalk_SUBMAP) THEN 1359 NTAC 2 (POP_ASSUM MP_TAC) THEN SRW_TAC [][] THEN 1360 FIRST_X_ASSUM (Q.SPEC_THEN `l` MP_TAC) THEN SRW_TAC [][] THEN 1361 Cases_on `t1` THEN FULL_SIMP_TAC (srw_ss()) [] THEN 1362 Q.PAT_X_ASSUM `nwfs sx` ASSUME_TAC THEN FULL_SIMP_TAC (psrw_ss()) [] THEN 1363 SRW_TAC [][Abbr`sx`,Once nvwalk_def,FLOOKUP_UPDATE] ) THEN1 ( 1364 Q.MATCH_ABBREV_TAC `equiv fex (nwalkstar sx t1) (nwalkstar sx t2)` THEN 1365 `(nwalkstar sx t1 = nwalkstar sx (nwalk s t1)) /\ 1366 (nwalkstar sx t2 = nwalkstar sx (nwalk s t2))` 1367 by METIS_TAC [nwalkstar_nwalk_SUBMAP] THEN 1368 Q.PAT_X_ASSUM `nwfs s` MP_TAC THEN 1369 MP_TAC (Q.INST[`t`|->`t1`]nwalk_SUBMAP) THEN 1370 MP_TAC (Q.INST[`t`|->`t2`]nwalk_SUBMAP) THEN 1371 NTAC 2 (POP_ASSUM MP_TAC) THEN SRW_TAC [][] THEN 1372 FIRST_X_ASSUM (Q.SPEC_THEN `l` MP_TAC) THEN SRW_TAC [][] THEN 1373 Cases_on `t1` THEN FULL_SIMP_TAC (srw_ss()) [] THEN 1374 Q.PAT_X_ASSUM `nwfs sx` ASSUME_TAC THEN FULL_SIMP_TAC (srw_ss()) [] THEN 1375 SRW_TAC [][Abbr`sx`,Once nvwalk_def,FLOOKUP_UPDATE] ) THEN1 ( 1376 Q.MATCH_ABBREV_TAC `equiv fex (nwalkstar sx t1) (nwalkstar sx t2)` THEN 1377 `(nwalkstar sx t1 = nwalkstar sx (nwalk s t1)) /\ 1378 (nwalkstar sx t2 = nwalkstar sx (nwalk s t2))` 1379 by METIS_TAC [nwalkstar_nwalk_SUBMAP] THEN 1380 Q.PAT_X_ASSUM `nwfs s` MP_TAC THEN 1381 MP_TAC (Q.INST[`t`|->`t1`]nwalk_SUBMAP) THEN 1382 MP_TAC (Q.INST[`t`|->`t2`]nwalk_SUBMAP) THEN 1383 NTAC 2 (POP_ASSUM MP_TAC) THEN SRW_TAC [][] THEN 1384 Q.PAT_X_ASSUM `nwalk* sx t2 = Z` MP_TAC THEN 1385 SRW_TAC [][Once nvwalk_def,Abbr`sx`,FLOOKUP_UPDATE] THEN 1386 SIMP_TAC (psrw_ss()) [] ) THEN1 ( 1387 Q.PAT_X_ASSUM `nunify X Y Z = X2` ASSUME_TAC THEN 1388 Q.PAT_X_ASSUM `verify_fcs X Y = Z` ASSUME_TAC THEN 1389 FULL_SIMP_TAC (srw_ss()) [] THEN 1390 `(nwalkstar sx t1 = nwalkstar sx (nwalk s t1)) /\ 1391 (nwalkstar sx t2 = nwalkstar sx (nwalk s t2))` 1392 by METIS_TAC [nwalkstar_nwalk_SUBMAP] THEN 1393 Q.PAT_X_ASSUM `nwfs s` MP_TAC THEN 1394 MP_TAC (Q.INST[`t`|->`t1`]nwalk_SUBMAP) THEN 1395 MP_TAC (Q.INST[`t`|->`t2`]nwalk_SUBMAP) THEN 1396 NTAC 2 (POP_ASSUM MP_TAC) THEN SRW_TAC [][] THEN 1397 SRW_TAC [][Once equiv_cases] ) THEN1 ( 1398 Q.PAT_X_ASSUM `term_fcs X Y = Z` ASSUME_TAC THEN 1399 Q.PAT_X_ASSUM `nunify X Y Z = X2` ASSUME_TAC THEN 1400 Q.PAT_X_ASSUM `X ��� Y` ASSUME_TAC THEN 1401 FULL_SIMP_TAC (srw_ss()) [] THEN 1402 IMP_RES_TAC term_fcs_SOME THEN 1403 Q.PAT_X_ASSUM `verify_fcs X Y = Z` ASSUME_TAC THEN 1404 FULL_SIMP_TAC (srw_ss()) [] THEN 1405 SRW_TAC [][] THEN 1406 `(nwalkstar sx t1 = nwalkstar sx (nwalk s t1)) /\ 1407 (nwalkstar sx t2 = nwalkstar sx (nwalk s t2))` 1408 by METIS_TAC [nwalkstar_nwalk_SUBMAP] THEN 1409 Q.PAT_X_ASSUM `nwfs s` MP_TAC THEN 1410 MP_TAC (Q.INST[`t`|->`t1`]nwalk_SUBMAP) THEN 1411 MP_TAC (Q.INST[`t`|->`t2`]nwalk_SUBMAP) THEN 1412 NTAC 2 (POP_ASSUM MP_TAC) THEN SRW_TAC [][] THEN 1413 REVERSE (SRW_TAC [][Once equiv_cases]) THEN1 1414 METIS_TAC [nwalkstar_apply_pi] THEN 1415 Q.MATCH_RENAME_TAC `fresh fex a (nwalk* sx c)` THEN 1416 Q_TAC SUFF_TAC `fresh fex a (nwalk* sx (nwalk* s c))` 1417 THEN1 METIS_TAC [nwalkstar_SUBMAP] THEN 1418 MATCH_MP_TAC (GEN_ALL fresh_verify_fcs) THEN 1419 Q.EXISTS_TAC `fx0` THEN 1420 SRW_TAC [][] THEN1 ( 1421 MATCH_MP_TAC (GEN_ALL fresh_extra_fcs) THEN 1422 Q.EXISTS_TAC `fcs` THEN SRW_TAC [][] THEN 1423 METIS_TAC [nunify_extends_fe,UNION_SUBSET] ) THEN 1424 MATCH_MP_TAC nunify_FINITE_fe THEN METIS_TAC [FINITE_UNION] ) THEN1 ( 1425 Q.MATCH_ABBREV_TAC `equiv fex (nwalkstar sx t1) (nwalkstar sx t2)` THEN 1426 `(nwalkstar sx t1 = nwalkstar sx (nwalk s t1)) /\ 1427 (nwalkstar sx t2 = nwalkstar sx (nwalk s t2))` 1428 by METIS_TAC [nwalkstar_nwalk_SUBMAP] THEN 1429 Q.PAT_X_ASSUM `nwfs s` MP_TAC THEN 1430 MP_TAC (Q.INST[`t`|->`t1`]nwalk_SUBMAP) THEN 1431 MP_TAC (Q.INST[`t`|->`t2`]nwalk_SUBMAP) THEN 1432 NTAC 2 (POP_ASSUM MP_TAC) THEN SRW_TAC [][] THEN 1433 FIRST_X_ASSUM (Q.SPEC_THEN `l` MP_TAC) THEN SRW_TAC [][] THEN 1434 Cases_on `t2` THEN FULL_SIMP_TAC (psrw_ss()) [] THEN 1435 Q.PAT_X_ASSUM `nwfs sx` ASSUME_TAC THEN FULL_SIMP_TAC (srw_ss()) [] THEN 1436 SRW_TAC [][Abbr`sx`,Once nvwalk_def,FLOOKUP_UPDATE] ) THEN1 ( 1437 `(nwalkstar sx t1 = nwalkstar sx (nwalk s t1)) /\ 1438 (nwalkstar sx t2 = nwalkstar sx (nwalk s t2))` 1439 by METIS_TAC [nwalkstar_nwalk_SUBMAP] THEN 1440 Cases_on `x` THEN FULL_SIMP_TAC (srw_ss()) [] THEN 1441 Q.PAT_X_ASSUM `nunify X Y Z = SOME (q,r)` ASSUME_TAC THEN 1442 Q.PAT_X_ASSUM `nunify X Y Z = SOME (sx,fx0)` ASSUME_TAC THEN 1443 Q.PAT_X_ASSUM `verify_fcs X Y = Z` ASSUME_TAC THEN 1444 FULL_SIMP_TAC (srw_ss()) [] THEN 1445 Q.MATCH_ASSUM_RENAME_TAC `nwalk s t1 = nPair t1a t1d` THEN 1446 Q.MATCH_ASSUM_RENAME_TAC `nwalk s t2 = nPair t2a t2d` THEN 1447 Q.MATCH_ASSUM_RENAME_TAC `nunify (s,fe) t1a t2a = SOME (sa, fea)` THEN 1448 Q.MATCH_ASSUM_RENAME_TAC `nunify (sa,fea) t1d t2d = SOME (sd, fed)` THEN 1449 `nwfs sa ��� sa SUBMAP sd` by METIS_TAC [nunify_uP,uP_def] THEN 1450 `FINITE fea ��� fea SUBSET fed ��� FINITE fed` 1451 by METIS_TAC [nunify_FINITE_fe,nunify_extends_fe] THEN 1452 SRW_TAC [][Once equiv_cases] THEN 1453 `���fad. (verify_fcs fea sd = SOME fad) ��� fad SUBSET fex` 1454 by METIS_TAC [verify_fcs_SUBSET] THEN 1455 `���faa. verify_fcs fea sa = SOME faa` 1456 by (METIS_TAC [verify_fcs_SUBMAP] ) THEN 1457 FULL_SIMP_TAC (srw_ss()) [] THEN 1458 `verify_fcs faa sd = SOME fad` by METIS_TAC [verify_fcs_iter_SUBMAP] THEN 1459 MATCH_MP_TAC (GEN_ALL equiv_SUBSET) THEN 1460 Q.EXISTS_TAC `fad` THEN SRW_TAC [][] THEN 1461 Q_TAC SUFF_TAC `equiv fad (nwalk* sd (nwalk* sa t1a)) (nwalk* sd (nwalk* sa t2a))` 1462 THEN1 METIS_TAC [nwalkstar_SUBMAP] THEN 1463 MATCH_MP_TAC (GEN_ALL equiv_verify_fcs) THEN 1464 MAP_EVERY Q.EXISTS_TAC [`faa`] THEN SRW_TAC [][] THEN 1465 IMP_RES_TAC verify_fcs_SOME) 1466THEN1 ( 1467 Q.MATCH_ABBREV_TAC `equiv fex (nwalkstar sx t1) (nwalkstar sx t2)` THEN 1468 `(nwalkstar sx t1 = nwalkstar sx (nwalk s t1)) /\ 1469 (nwalkstar sx t2 = nwalkstar sx (nwalk s t2))` 1470 by METIS_TAC [nwalkstar_nwalk_SUBMAP] THEN 1471 Q.PAT_X_ASSUM `nwfs s` MP_TAC THEN 1472 MP_TAC (Q.INST[`t`|->`t1`]nwalk_SUBMAP) THEN 1473 MP_TAC (Q.INST[`t`|->`t2`]nwalk_SUBMAP) THEN 1474 NTAC 2 (POP_ASSUM MP_TAC) THEN SRW_TAC [][] THEN 1475 FIRST_X_ASSUM (Q.SPEC_THEN `l` MP_TAC) THEN SRW_TAC [][] THEN 1476 Cases_on `t2` THEN FULL_SIMP_TAC (srw_ss()) [] THEN 1477 Q.PAT_X_ASSUM `nwfs sx` ASSUME_TAC THEN FULL_SIMP_TAC (srw_ss()) [] THEN 1478 SRW_TAC [][Abbr`sx`,Once nvwalk_def,FLOOKUP_UPDATE] ) THEN 1479METIS_TAC [nwalkstar_nwalk,equiv_refl]); 1480 1481val nomunify_fcs_consistent = Q.store_thm( 1482"nomunify_fcs_consistent", 1483`!s fe t1 t2 sx fex. nwfs s ��� FINITE fe ��� (nomunify (s,fe) t1 t2 = SOME (sx,fex)) ��� (a,v) ��� fex ==> 1484 fresh fex a (nwalk* sx (Sus [] v))`, 1485HO_MATCH_MP_TAC nunify_ind THEN SRW_TAC [][nomunify_def,UNCURRY] THEN 1486`���sx fx0. x = (sx,fx0)` by (Cases_on `x` THEN SRW_TAC [][]) THEN SRW_TAC [][] THEN 1487`nwfs sx /\ s SUBMAP sx` by METIS_TAC [nunify_uP,uP_def] THEN 1488FULL_SIMP_TAC (srw_ss()) [EXISTS_PROD] THEN 1489Q.PAT_X_ASSUM `nunify p t1 t2 = SOME px` MP_TAC THEN 1490Cases_on `nwalk s t1` THEN Cases_on `nwalk s t2` THEN 1491ASM_SIMP_TAC (psrw_ss()) [Once nunify_def,nvwalk_case_thms,LET_THM] THEN 1492SRW_TAC [][] THEN1 ( 1493 IMP_RES_TAC verify_fcs_NOTIN_FDOM THEN 1494 ASM_SIMP_TAC (psrw_ss()) [NOT_FDOM_nvwalk,fresh_def]) 1495THEN1 ( 1496 IMP_RES_TAC verify_fcs_NOTIN_FDOM THEN 1497 ASM_SIMP_TAC (psrw_ss()) [NOT_FDOM_nvwalk,fresh_def]) 1498THEN1 ( 1499 IMP_RES_TAC verify_fcs_NOTIN_FDOM THEN 1500 ASM_SIMP_TAC (psrw_ss()) [NOT_FDOM_nvwalk,fresh_def]) 1501THEN1 ( 1502 IMP_RES_TAC unify_eq_vars_preserves_s THEN 1503 IMP_RES_TAC unify_eq_vars_FINITE THEN 1504 FULL_SIMP_TAC (srw_ss()) [] THEN 1505 IMP_RES_TAC verify_fcs_NOTIN_FDOM THEN 1506 SRW_TAC [][] THEN 1507 ASM_SIMP_TAC (psrw_ss()) [NOT_FDOM_nvwalk,fresh_def]) 1508THEN1 ( 1509 IMP_RES_TAC verify_fcs_NOTIN_FDOM THEN 1510 ASM_SIMP_TAC (psrw_ss()) [NOT_FDOM_nvwalk,fresh_def]) 1511THEN1 ( 1512 IMP_RES_TAC verify_fcs_NOTIN_FDOM THEN 1513 ASM_SIMP_TAC (psrw_ss()) [NOT_FDOM_nvwalk,fresh_def]) 1514THEN1 ( 1515 IMP_RES_TAC verify_fcs_NOTIN_FDOM THEN 1516 ASM_SIMP_TAC (psrw_ss()) [NOT_FDOM_nvwalk,fresh_def]) 1517THEN1 ( 1518 IMP_RES_TAC verify_fcs_NOTIN_FDOM THEN 1519 ASM_SIMP_TAC (psrw_ss()) [NOT_FDOM_nvwalk,fresh_def]) 1520THEN1 ( 1521 IMP_RES_TAC verify_fcs_NOTIN_FDOM THEN 1522 ASM_SIMP_TAC (psrw_ss()) [NOT_FDOM_nvwalk,fresh_def]) 1523THEN1 ( 1524 POP_ASSUM MP_TAC THEN ASM_SIMP_TAC (srw_ss()) [] ) 1525THEN1 ( 1526 IMP_RES_TAC term_fcs_FINITE THEN 1527 NTAC 3 ( POP_ASSUM MP_TAC ) 1528 THEN ASM_SIMP_TAC (srw_ss()) [] ) 1529THEN1 ( 1530 IMP_RES_TAC verify_fcs_NOTIN_FDOM THEN 1531 ASM_SIMP_TAC (psrw_ss()) [NOT_FDOM_nvwalk,fresh_def]) 1532THEN1 ( 1533 Cases_on `x` THEN 1534 NTAC 3 (POP_ASSUM MP_TAC) THEN 1535 ASM_SIMP_TAC (srw_ss()) [] THEN 1536 STRIP_TAC THEN 1537 `nwfs q ��� FINITE r` by METIS_TAC [nunify_uP,uP_def,nunify_FINITE_fe] THEN 1538 SRW_TAC [][]) 1539THEN1 ( 1540 IMP_RES_TAC verify_fcs_NOTIN_FDOM THEN 1541 ASM_SIMP_TAC (psrw_ss()) [NOT_FDOM_nvwalk,fresh_def]) 1542THEN1 ( 1543 IMP_RES_TAC verify_fcs_NOTIN_FDOM THEN 1544 ASM_SIMP_TAC (psrw_ss()) [NOT_FDOM_nvwalk,fresh_def])); 1545 1546val nomunify_solves_fe = Q.store_thm( 1547"nomunify_solves_fe", 1548`!s fe t1 t2 sx fex. nwfs s ��� FINITE fe ��� (nomunify (s,fe) t1 t2 = SOME (sx,fex)) ��� (a,v) ��� fe ==> 1549 fresh fex a (nwalk* sx (Sus [] v))`, 1550HO_MATCH_MP_TAC nunify_ind THEN SRW_TAC [][nomunify_def,UNCURRY] THEN 1551`���sx fx0. x = (sx,fx0)` by (Cases_on `x` THEN SRW_TAC [][]) THEN SRW_TAC [][] THEN 1552`nwfs sx /\ s SUBMAP sx` by METIS_TAC [nunify_uP,uP_def] THEN 1553FULL_SIMP_TAC (srw_ss()) [EXISTS_PROD] THEN 1554Q.PAT_X_ASSUM `nunify p t1 t2 = SOME px` MP_TAC THEN 1555Cases_on `nwalk s t1` THEN Cases_on `nwalk s t2` THEN 1556ASM_SIMP_TAC (psrw_ss()) [Once nunify_def,nvwalk_case_thms,LET_THM] THEN 1557SRW_TAC [][] THEN1 ( 1558 IMP_RES_TAC verify_fcs_covers_all THEN 1559 IMP_RES_TAC term_fcs_fresh THEN 1560 IMP_RES_TAC fresh_extra_fcs THEN 1561 POP_ASSUM MP_TAC THEN ASM_SIMP_TAC (srw_ss()) [] ) 1562THEN1 ( 1563 IMP_RES_TAC verify_fcs_covers_all THEN 1564 IMP_RES_TAC term_fcs_fresh THEN 1565 IMP_RES_TAC fresh_extra_fcs THEN 1566 POP_ASSUM MP_TAC THEN ASM_SIMP_TAC (srw_ss()) [] ) 1567THEN1 ( 1568 IMP_RES_TAC verify_fcs_covers_all THEN 1569 IMP_RES_TAC term_fcs_fresh THEN 1570 IMP_RES_TAC fresh_extra_fcs THEN 1571 POP_ASSUM MP_TAC THEN ASM_SIMP_TAC (srw_ss()) [] ) 1572THEN1 ( 1573 IMP_RES_TAC unify_eq_vars_preserves_s THEN 1574 IMP_RES_TAC unify_eq_vars_extends_fe THEN 1575 IMP_RES_TAC unify_eq_vars_FINITE THEN 1576 FULL_SIMP_TAC (srw_ss()) [] THEN 1577 `(a,v) ��� fx0` by METIS_TAC [SUBSET_DEF] THEN 1578 IMP_RES_TAC verify_fcs_covers_all THEN 1579 IMP_RES_TAC term_fcs_fresh THEN 1580 IMP_RES_TAC fresh_extra_fcs THEN 1581 NTAC 2 (POP_ASSUM MP_TAC) THEN ASM_SIMP_TAC (srw_ss()) [] ) 1582THEN1 ( 1583 IMP_RES_TAC verify_fcs_covers_all THEN 1584 IMP_RES_TAC term_fcs_fresh THEN 1585 IMP_RES_TAC fresh_extra_fcs THEN 1586 POP_ASSUM MP_TAC THEN ASM_SIMP_TAC (srw_ss()) [] ) 1587THEN1 ( 1588 IMP_RES_TAC verify_fcs_covers_all THEN 1589 IMP_RES_TAC term_fcs_fresh THEN 1590 IMP_RES_TAC fresh_extra_fcs THEN 1591 POP_ASSUM MP_TAC THEN ASM_SIMP_TAC (srw_ss()) [] ) 1592THEN1 ( 1593 IMP_RES_TAC verify_fcs_covers_all THEN 1594 IMP_RES_TAC term_fcs_fresh THEN 1595 IMP_RES_TAC fresh_extra_fcs THEN 1596 POP_ASSUM MP_TAC THEN ASM_SIMP_TAC (srw_ss()) [] ) 1597THEN1 ( 1598 IMP_RES_TAC verify_fcs_covers_all THEN 1599 IMP_RES_TAC term_fcs_fresh THEN 1600 IMP_RES_TAC fresh_extra_fcs THEN 1601 POP_ASSUM MP_TAC THEN ASM_SIMP_TAC (srw_ss()) [] ) 1602THEN1 ( 1603 IMP_RES_TAC verify_fcs_covers_all THEN 1604 IMP_RES_TAC term_fcs_fresh THEN 1605 IMP_RES_TAC fresh_extra_fcs THEN 1606 POP_ASSUM MP_TAC THEN ASM_SIMP_TAC (srw_ss()) [] ) 1607THEN1 ( 1608 POP_ASSUM MP_TAC THEN SRW_TAC [][] ) 1609THEN1 ( 1610 IMP_RES_TAC term_fcs_FINITE THEN 1611 NTAC 3 (POP_ASSUM MP_TAC) THEN 1612 ASM_SIMP_TAC (srw_ss()) [] ) 1613THEN1 ( 1614 IMP_RES_TAC verify_fcs_covers_all THEN 1615 IMP_RES_TAC term_fcs_fresh THEN 1616 IMP_RES_TAC fresh_extra_fcs THEN 1617 POP_ASSUM MP_TAC THEN ASM_SIMP_TAC (srw_ss()) [] ) 1618THEN1 ( 1619 Cases_on `x` THEN FULL_SIMP_TAC (srw_ss()) [] THEN 1620 NTAC 2 (POP_ASSUM MP_TAC) THEN ASM_SIMP_TAC (srw_ss()) [] THEN 1621 `nwfs q ��� FINITE r ��� fe SUBSET r` 1622 by METIS_TAC [nunify_uP,uP_def,nunify_FINITE_fe,nunify_extends_fe] THEN 1623 `(a,v) ��� r` by METIS_TAC [SUBSET_DEF] THEN 1624 SRW_TAC [][] ) 1625THEN1 ( 1626 IMP_RES_TAC verify_fcs_covers_all THEN 1627 IMP_RES_TAC term_fcs_fresh THEN 1628 IMP_RES_TAC fresh_extra_fcs THEN 1629 POP_ASSUM MP_TAC THEN ASM_SIMP_TAC (srw_ss()) [] ) 1630THEN1 ( 1631 IMP_RES_TAC verify_fcs_covers_all THEN 1632 IMP_RES_TAC term_fcs_fresh THEN 1633 IMP_RES_TAC fresh_extra_fcs THEN 1634 POP_ASSUM MP_TAC THEN ASM_SIMP_TAC (srw_ss()) [] )) 1635 1636val _ = set_fixity "COMPAT" (Infix(NONASSOC,450)) 1637 1638val COMPAT_def = Define` 1639 (sx,fex) COMPAT (s,fe) <=> 1640 nwfs s ��� nwfs sx ��� FINITE fe ��� FINITE fex ��� 1641 ���ve vex. (verify_fcs fe s = SOME ve) ��� 1642 (verify_fcs fex sx = SOME vex) ��� 1643 ���t1 t2. equiv ve (nwalk* s t1) (nwalk* s t2) ��� 1644 equiv vex (nwalk* sx t1) (nwalk* sx t2) 1645`; 1646 1647val COMPAT_REFL = Q.store_thm( 1648"COMPAT_REFL", 1649`nwfs s ��� FINITE fe ��� (verify_fcs fe s = SOME ve) ==> 1650(s,fe) COMPAT (s,fe) ��� 1651(s,ve) COMPAT (s,fe) ��� 1652(s,fe) COMPAT (s,ve) ��� 1653(s,ve) COMPAT (s,ve) 1654`, 1655SRW_TAC [][COMPAT_def] THEN 1656FULL_SIMP_TAC (srw_ss()) [] THEN 1657`FINITE ve` by IMP_RES_TAC verify_fcs_SOME THEN 1658SRW_TAC [][] THEN 1659IMP_RES_TAC verify_fcs_idem THEN 1660FULL_SIMP_TAC (srw_ss()) []) 1661 1662val COMPAT_TRANS = Q.store_thm( 1663"COMPAT_TRANS", 1664`p2 COMPAT p1 /\ p1 COMPAT p0 ==> p2 COMPAT p0`, 1665MAP_EVERY Cases_on [`p0`,`p1`,`p2`] THEN 1666SRW_TAC [][COMPAT_def] THEN 1667FULL_SIMP_TAC (srw_ss()) [] THEN 1668SRW_TAC [][]) 1669 1670val SUBMAP_COMPAT = Q.store_thm( 1671"SUBMAP_COMPAT", 1672`nwfs sx ��� s SUBMAP sx ��� FINITE fe ��� (verify_fcs fe sx = SOME ve) ��� 1673 (sx,fe) COMPAT (s,fe)`, 1674STRIP_TAC THEN 1675IMP_RES_TAC nwfs_SUBMAP THEN 1676SRW_TAC [][COMPAT_def] THEN 1677IMP_RES_TAC verify_fcs_SUBMAP THEN 1678FULL_SIMP_TAC (srw_ss()) [] THEN 1679SRW_TAC [][] THEN 1680Q_TAC SUFF_TAC `equiv ve (nwalk* sx (nwalk* s t1)) (nwalk* sx (nwalk* s t2))` 1681THEN1 METIS_TAC [nwalkstar_SUBMAP] THEN 1682MATCH_MP_TAC (GEN_ALL equiv_verify_fcs) THEN 1683Q.EXISTS_TAC `fe1` THEN 1684SRW_TAC [][] THEN1 1685IMP_RES_TAC verify_fcs_SOME THEN 1686MATCH_MP_TAC verify_fcs_iter_SUBMAP THEN 1687SRW_TAC [][] ) 1688 1689val SUBSET_COMPAT = Q.store_thm( 1690"SUBSET_COMPAT", 1691`nwfs s ��� (verify_fcs fex s = SOME vex) ��� FINITE fex ��� fe SUBSET fex ��� 1692 (s,fex) COMPAT (s,fe)`, 1693SRW_TAC [][COMPAT_def] THEN1 1694METIS_TAC [SUBSET_FINITE] THEN 1695`���ve. ve SUBSET vex ��� (verify_fcs fe s = SOME ve)` 1696by METIS_TAC [verify_fcs_SUBSET] THEN 1697SRW_TAC [][] THEN 1698METIS_TAC [equiv_SUBSET]) 1699 1700val nomunify_COMPAT = Q.store_thm( 1701"nomunify_COMPAT", 1702`nwfs s ��� FINITE fe ��� (nomunify (s,fe) t1 t2 = SOME (su,fu)) ��� (su,fu) COMPAT (s,fe)`, 1703SRW_TAC [][nomunify_def] THEN 1704Cases_on `x` THEN 1705FULL_SIMP_TAC (srw_ss()) [] THEN SRW_TAC [][] THEN 1706Q.MATCH_ASSUM_RENAME_TAC `verify_fcs fu0 su = SOME fu` THEN 1707`s SUBMAP su ��� nwfs su` by METIS_TAC [nunify_uP,uP_def] THEN 1708`fe SUBSET fu0` by METIS_TAC [nunify_extends_fe] THEN 1709`FINITE fu0` by METIS_TAC [nunify_FINITE_fe] THEN 1710MATCH_MP_TAC (GEN_ALL COMPAT_TRANS) THEN 1711Q.EXISTS_TAC `(su,fe)` THEN 1712REVERSE CONJ_TAC THEN1 ( 1713 MATCH_MP_TAC (GEN_ALL SUBMAP_COMPAT) THEN 1714 IMP_RES_TAC verify_fcs_SUBSET THEN 1715 SRW_TAC [][] ) THEN 1716MATCH_MP_TAC (GEN_ALL COMPAT_TRANS) THEN 1717Q.EXISTS_TAC `(su,fu0)` THEN 1718CONJ_TAC THEN1 ( 1719 METIS_TAC [COMPAT_REFL] ) THEN 1720MATCH_MP_TAC (GEN_ALL SUBSET_COMPAT) THEN 1721SRW_TAC [][]) 1722 1723val nvwalk_irrelevant_FUPDATE = Q.store_thm( 1724"nvwalk_irrelevant_FUPDATE", 1725`nwfs (s|+(vx,tx)) /\ vx NOTIN FDOM s ==> 1726 !p v.~(nvR s)^* vx v ==> (nvwalk (s|+(vx,tx)) p v = nvwalk s p v)`, 1727STRIP_TAC THEN 1728`nwfs s` by METIS_TAC [nwfs_SUBMAP,SUBMAP_FUPDATE_EQN] THEN 1729HO_MATCH_MP_TAC nvwalk_ind THEN 1730SRW_TAC [][] THEN 1731`vx <> v` by METIS_TAC [RTC_REFL] THEN 1732Cases_on `FLOOKUP s v` THEN1 ( 1733 `v NOTIN FDOM s /\ v NOTIN FDOM (s|+(vx,tx))` 1734 by (POP_ASSUM MP_TAC THEN SRW_TAC [][FLOOKUP_DEF]) THEN 1735 SRW_TAC [][NOT_FDOM_nvwalk] ) THEN 1736Cases_on `is_Sus x` THEN1 ( 1737 FULL_SIMP_TAC (srw_ss()) [] THEN 1738 `nvR s v' v` by FULL_SIMP_TAC (srw_ss()) [nvR_def] THEN 1739 `~(nvR s)^* vx v'` by METIS_TAC [RTC_SUBSET,RTC_TRANSITIVE,transitive_def] THEN 1740 FULL_SIMP_TAC (srw_ss()) [] THEN 1741 FIRST_X_ASSUM (Q.SPEC_THEN `p'` MP_TAC) THEN 1742 SRW_TAC [][] THEN 1743 ASM_SIMP_TAC (psrw_ss()) [Once nvwalk_def,SimpLHS,FLOOKUP_UPDATE,nvwalk_case_thms] THEN 1744 ASM_SIMP_TAC (psrw_ss()) [Once nvwalk_def,SimpRHS,FLOOKUP_UPDATE,nvwalk_case_thms] ) 1745THEN Cases_on `x` THEN FULL_SIMP_TAC (srw_ss()) [] THEN 1746ASM_SIMP_TAC (psrw_ss()) [Once nvwalk_def,SimpLHS,FLOOKUP_UPDATE,nvwalk_case_thms] THEN 1747ASM_SIMP_TAC (psrw_ss()) [Once nvwalk_def,SimpRHS,FLOOKUP_UPDATE,nvwalk_case_thms]) 1748 1749val nvR_SUBMAP = Q.prove( 1750`s SUBMAP sx ==> nvR s u v ==> nvR sx u v`, 1751Cases_on `FLOOKUP s v` THEN 1752SRW_TAC [][nvR_def] THEN 1753`FLOOKUP sx v = SOME x` by METIS_TAC [FLOOKUP_SUBMAP] THEN 1754SRW_TAC [][]) 1755 1756val TC_nvR_SUBMAP = Q.store_thm( 1757"TC_nvR_SUBMAP", 1758`s SUBMAP sx ==> !u v.(nvR s)^+ u v ==> (nvR sx)^+ u v`, 1759STRIP_TAC THEN HO_MATCH_MP_TAC TC_INDUCT THEN 1760SRW_TAC [][] THEN1 METIS_TAC [TC_SUBSET,nvR_SUBMAP] THEN 1761METIS_TAC [TC_RULES]) 1762 1763val nvwalk_FUPDATE_var = Q.store_thm( 1764"nvwalk_FUPDATE_var", 1765`nwfs (s |+ (vx,tx)) ��� vx ��� FDOM s ��� 1766 (nvwalk (s |+ (vx,tx)) [] vx = nwalk s tx)`, 1767STRIP_TAC THEN 1768`nwfs s` by METIS_TAC [nwfs_SUBMAP,SUBMAP_FUPDATE_EQN] THEN 1769Cases_on `is_Sus tx` THEN1 ( 1770 FULL_SIMP_TAC (srw_ss()) [] THEN SRW_TAC [][] THEN 1771 ASM_SIMP_TAC (psrw_ss()) [Once nvwalk_def,SimpLHS,FLOOKUP_UPDATE,nvwalk_case_thms] THEN 1772 Q_TAC SUFF_TAC `~(nvR s)^* vx v` THEN1 METIS_TAC [nvwalk_irrelevant_FUPDATE] THEN 1773 Cases_on `vx = v` THEN1 ( 1774 `nvR (s|+(vx,Sus p v)) vx v` by FULL_SIMP_TAC (srw_ss()) [nvR_def,FLOOKUP_UPDATE] THEN 1775 SRW_TAC [][] THEN 1776 FULL_SIMP_TAC (srw_ss()) [nwfs_no_cycles] THEN 1777 METIS_TAC [TC_SUBSET] ) THEN 1778 SRW_TAC [][RTC_CASES_TC] THEN 1779 FULL_SIMP_TAC (srw_ss()) [nwfs_no_cycles] THEN 1780 `s SUBMAP (s|+(vx,Sus p v))` by METIS_TAC [SUBMAP_FUPDATE_EQN] THEN 1781 SPOSE_NOT_THEN STRIP_ASSUME_TAC THEN 1782 IMP_RES_TAC TC_nvR_SUBMAP THEN 1783 `nvR (s|+(vx,Sus p v)) v vx` by FULL_SIMP_TAC (srw_ss()) [nvR_def,FLOOKUP_UPDATE] THEN 1784 METIS_TAC [TC_RULES] ) THEN 1785Cases_on `tx` THEN FULL_SIMP_TAC (srw_ss()) [] THEN 1786SRW_TAC [][Once nvwalk_def,SimpLHS,FLOOKUP_UPDATE]) 1787 1788val nwalkstar_irrelevant_FUPDATE = Q.store_thm( 1789"nwalkstar_irrelevant_FUPDATE", 1790`nwfs (s|+(vx,tx)) ��� vx ��� FDOM s ��� �� noc s t vx ��� 1791 (nwalk* (s|+(vx,tx)) t = nwalk* s t)`, 1792Q_TAC SUFF_TAC 1793`nwfs (s|+(vx,tx)) ��� vx ��� FDOM s ��� 1794���t. �� noc s t vx ��� (nwalk* (s|+(vx,tx)) t = nwalk* s t)` 1795THEN1 METIS_TAC [] THEN 1796STRIP_TAC THEN 1797`nwfs s` by METIS_TAC [nwfs_SUBMAP,SUBMAP_FUPDATE_EQN] THEN 1798HO_MATCH_MP_TAC (Q.INST [`s`|->`s|+(vx,tx)`]nwalkstar_ind) THEN 1799SRW_TAC [][] THEN 1800Cases_on `t` THEN FULL_SIMP_TAC (psrw_ss()) [] THEN 1801`vx ��� nvars (nwalk* s (Sus l n))` 1802by (SRW_TAC [][GSYM noc_eq_nvars_nwalkstar,IN_DEF]) THEN 1803(TC_nvR_nvars_nwalkstar |> UNDISCH |> 1804 Q.SPECL [`Sus l n`,`vx`] |> 1805 SIMP_RULE (srw_ss()) [LEFT_FORALL_IMP_THM] |> 1806 CONTRAPOS |> MP_TAC) THEN 1807SRW_TAC [][] THEN 1808`n ��� vx` by ( 1809 SPOSE_NOT_THEN STRIP_ASSUME_TAC THEN 1810 Q.PAT_X_ASSUM `nwfs s` ASSUME_TAC THEN 1811 Q.PAT_X_ASSUM `vx ��� FDOM s` ASSUME_TAC THEN 1812 FULL_SIMP_TAC (srw_ss()) [NOT_FDOM_nvwalk] ) THEN 1813`~(nvR s)^* vx n` by METIS_TAC [RTC_CASES_TC] THEN 1814IMP_RES_TAC nvwalk_irrelevant_FUPDATE THEN 1815Q.PAT_X_ASSUM `nwfs (s|+(vx,tx))` ASSUME_TAC THEN 1816FULL_SIMP_TAC (srw_ss()) [] THEN 1817Cases_on `nvwalk s l n` THEN 1818FULL_SIMP_TAC (srw_ss()) [] THEN 1819Q.PAT_X_ASSUM `nwfs s` ASSUME_TAC THEN 1820FULL_SIMP_TAC (srw_ss()) [noc_eq_nvars_nwalkstar] THEN 1821METIS_TAC [IN_DEF,IN_UNION]) 1822 1823val extension_is_nwfs = Q.store_thm( 1824"extension_is_nwfs", 1825`nwfs (s|+(vx,tx)) ��� vx ��� FDOM s ��� 1826 nwfs s ��� �� noc s tx vx`, 1827STRIP_TAC THEN 1828`s SUBMAP (s|+(vx,tx))` by METIS_TAC [SUBMAP_FUPDATE_EQN] THEN 1829CONJ1_TAC THEN1 ( 1830 METIS_TAC [nwfs_no_cycles,TC_nvR_SUBMAP] ) THEN 1831STRIP_TAC THEN 1832IMP_RES_TAC noc_TC_nvR THEN 1833`nvR (s|+(vx,tx)) u vx` by ( 1834 SRW_TAC [][nvR_def,FLOOKUP_UPDATE] ) THEN 1835IMP_RES_TAC RTC_CASES_TC THEN1 1836 METIS_TAC [nwfs_no_cycles,TC_SUBSET] THEN 1837IMP_RES_TAC TC_nvR_SUBMAP THEN 1838METIS_TAC [nwfs_no_cycles,TC_RULES]); 1839 1840val nwalkstar_FUPDATE_var = Q.store_thm( 1841"nwalkstar_FUPDATE_var", 1842`nwfs (s|+(vx,tx)) ��� vx ��� FDOM s ��� 1843 (nwalk* (s|+(vx,tx)) (Sus [] vx) = nwalk* s tx)`, 1844STRIP_TAC THEN 1845`nwfs s` by METIS_TAC [nwfs_SUBMAP,SUBMAP_FUPDATE_EQN] THEN 1846Q_TAC SUFF_TAC 1847`nwalk* (s|+(vx,tx)) (nwalk s tx) = nwalk* s (nwalk s tx)` 1848THEN1 ( 1849 `nwalk (s|+(vx,tx)) (Sus [] vx) = nwalk s tx` 1850 by (SRW_TAC [][nvwalk_FUPDATE_var]) THEN 1851 METIS_TAC [nwalkstar_nwalk] ) THEN 1852MATCH_MP_TAC nwalkstar_irrelevant_FUPDATE THEN 1853SRW_TAC [][] THEN 1854IMP_RES_TAC extension_is_nwfs THEN 1855POP_ASSUM MP_TAC THEN 1856ASM_SIMP_TAC (srw_ss()) [noc_eq_nvars_nwalkstar] THEN 1857METIS_TAC [nwalkstar_nwalk]); 1858 1859val equiv_extend = Q.store_thm ((* Lemma 3.3 ; nominal version of nwalkstar_extend ?*) 1860"equiv_extend", 1861`nwfs s1 ��� nwfs (s|+(vx,apply_pi (REVERSE pi) tx)) ��� vx ��� FDOM s ��� 1862 equiv fe (nwalk* s1 (Sus pi vx)) (nwalk* s1 (nwalk* s tx)) ��� 1863 ���t. equiv fe (nwalk* s1 (nwalk* (s|+(vx,apply_pi (REVERSE pi) tx)) t)) (nwalk* s1 (nwalk* s t))`, 1864STRIP_TAC THEN 1865Q.ABBREV_TAC `sx = (s|+(vx,apply_pi (REVERSE pi) tx))` THEN 1866`nwfs s ��� s SUBMAP sx` by METIS_TAC [nwfs_SUBMAP,SUBMAP_FUPDATE_EQN] THEN 1867HO_MATCH_MP_TAC nwalkstar_ind THEN SRW_TAC [][] THEN 1868`(nwalk* s t = nwalk* s (nwalk s t)) ��� 1869 (nwalk* sx t = nwalk* sx (nwalk s t))` 1870 by METIS_TAC [nwalkstar_nwalk,nwalkstar_nwalk_SUBMAP] THEN 1871Cases_on `nwalk s t` THEN FULL_SIMP_TAC (srw_ss()) [] THEN1 ( 1872 `n ��� FDOM s` by METIS_TAC [nwalk_to_var] THEN 1873 REVERSE (Cases_on `n = vx`) THEN1 ( 1874 `nwalk* sx (Sus l n) = nwalk* s (Sus l n)` 1875 by (Q.UNABBREV_TAC `sx` THEN 1876 MATCH_MP_TAC nwalkstar_irrelevant_FUPDATE THEN 1877 SRW_TAC [][noc_eq_nvars_nwalkstar,NOT_FDOM_nvwalk] ) THEN 1878 POP_ASSUM MP_TAC THEN ASM_SIMP_TAC (srw_ss()) [] ) THEN 1879 SRW_TAC [][] THEN 1880 Q_TAC SUFF_TAC `equiv fe (nwalk* s1 (nwalk* sx (Sus [] n))) (nwalk* s1 (nwalk* s (Sus [] n)))` 1881 THEN1 ( STRIP_TAC THEN 1882 IMP_RES_TAC equiv_apply_pi THEN 1883 POP_ASSUM (K ALL_TAC) THEN 1884 POP_ASSUM (Q.SPEC_THEN `l` MP_TAC) THEN 1885 ASM_SIMP_TAC (psrw_ss()) [GSYM nwalkstar_apply_pi] ) THEN 1886 MATCH_MP_TAC equiv_sym THEN 1887 `equiv fe (apply_pi (REVERSE pi) (nwalk* s1 (Sus pi n))) 1888 (apply_pi (REVERSE pi) (nwalk* s1 (nwalk* s tx)))` 1889 by (MATCH_MP_TAC equiv_apply_pi THEN SRW_TAC [][]) THEN 1890 POP_ASSUM MP_TAC THEN ASM_SIMP_TAC (psrw_ss()) [GSYM nwalkstar_apply_pi] THEN 1891 ASM_SIMP_TAC (psrw_ss()) [NOT_FDOM_nvwalk] THEN 1892 `nwalk* sx (Sus [] n) = nwalk* s (apply_pi (REVERSE pi) tx)` 1893 by (Q.UNABBREV_TAC `sx` THEN 1894 MATCH_MP_TAC nwalkstar_FUPDATE_var THEN 1895 SRW_TAC [][] ) THEN 1896 POP_ASSUM MP_TAC THEN ASM_SIMP_TAC (srw_ss()) [] ) 1897THEN1 (SRW_TAC [][Once equiv_cases]) 1898THEN1 (SRW_TAC [][Once equiv_cases])); 1899 1900val nvars_nwalkstar_subterm = Q.store_thm( 1901"nvars_nwalkstar_subterm", 1902`nwfs s ��� 1903 ((���v1. v1 ��� nvars t ��� v2 ��� nvars (nwalk* s (Sus [] v1))) ��� v2 ��� nvars (nwalk* s t))`, 1904STRIP_TAC THEN EQ_TAC THEN1 ( 1905 STRIP_TAC THEN 1906 IMP_RES_TAC noc_eq_nvars_nwalkstar THEN 1907 IMP_RES_TAC noc_TC_nvR THEN 1908 IMP_RES_TAC noc_NOTIN_FDOM THEN 1909 FULL_SIMP_TAC (srw_ss()) [RTC_CASES_TC] THEN 1910 SRW_TAC [][] THEN1 1911 IMP_RES_TAC NOT_FDOM_nwalkstar THEN 1912 METIS_TAC [TC_nvR_nvars_nwalkstar]) THEN 1913SPEC_ALL_TAC [`s`,`t`] THEN 1914Q.ID_SPEC_TAC `t` THEN 1915HO_MATCH_MP_TAC nwalkstar_ind THEN 1916SRW_TAC [][] THEN 1917`nwalk* s t = (nwalk* s (nwalk s t))` by METIS_TAC [nwalkstar_nwalk] THEN 1918Cases_on `nwalk s t` THEN 1919Q.PAT_X_ASSUM `nwfs s` ASSUME_TAC THEN 1920FULL_SIMP_TAC (srw_ss()) [] THEN1 ( 1921 Cases_on `t` THEN FULL_SIMP_TAC (psrw_ss()) [] THEN 1922 `n ��� FDOM s` by METIS_TAC [nvwalk_to_var] THEN 1923 FULL_SIMP_TAC (psrw_ss()) [NOT_FDOM_nvwalk] THEN 1924 (nvwalk_modulo_pi |> Q.SPECL [`s`,`l'`,`n'`] |> GSYM |> MP_TAC) THEN 1925 ASM_SIMP_TAC (psrw_ss()) [apply_pi_eql] ) 1926THEN1 ( 1927 Cases_on `t` THEN FULL_SIMP_TAC (srw_ss()) [] THEN 1928 (nvwalk_modulo_pi |> Q.SPECL [`s`,`l`,`n`] |> GSYM |> MP_TAC) THEN 1929 ASM_SIMP_TAC (srw_ss()) [apply_pi_eql,nwalkstar_apply_pi] ) 1930THEN1 ( 1931 Cases_on `t` THEN FULL_SIMP_TAC (srw_ss()) [] THEN 1932 (nvwalk_modulo_pi |> Q.SPECL [`s`,`l`,`n`] |> GSYM |> MP_TAC) THEN 1933 ASM_SIMP_TAC (srw_ss()) [apply_pi_eql,nwalkstar_apply_pi] THEN 1934 SRW_TAC [][] THEN METIS_TAC []) 1935THEN1 ( 1936 Cases_on `t` THEN FULL_SIMP_TAC (srw_ss()) [] THEN 1937 (nvwalk_modulo_pi |> Q.SPECL [`s`,`l`,`n`] |> GSYM |> MP_TAC) THEN 1938 ASM_SIMP_TAC (srw_ss()) [apply_pi_eql,nwalkstar_apply_pi] THEN 1939 SRW_TAC [][] THEN METIS_TAC [])); 1940 1941val equiv_ties_fcs = Q.store_thm( 1942"equiv_ties_fcs", 1943`equiv fe (Tie a1 t1) (Tie a2 t2) ��� a1 ��� a2 ��� 1944 ���fcs. (term_fcs a1 t2 = SOME fcs) ��� fcs SUBSET fe`, 1945SRW_TAC [][Once equiv_cases] THEN 1946Cases_on `term_fcs a1 t2` THEN1 ( 1947 IMP_RES_TAC term_fcs_NONE ) THEN 1948IMP_RES_TAC term_fcs_minimal THEN 1949SRW_TAC [][]) 1950 1951val fresh_FINITE = Q.store_thm( 1952"fresh_FINITE", 1953`fresh fe a t ��� ���fcs. fcs SUBSET fe ��� FINITE fcs ��� fresh fcs a t`, 1954Induct_on `t` THEN ASM_SIMP_TAC (psrw_ss()) [fresh_def] THEN SRW_TAC [][] THEN1 ( 1955 Q.EXISTS_TAC `{}` THEN SRW_TAC [][] ) 1956THEN1 ( 1957 Q.MATCH_ASSUM_RENAME_TAC `x ��� fe` THEN 1958 Q.EXISTS_TAC `{x}` THEN SRW_TAC [][] ) 1959THEN1 ( 1960 Q.EXISTS_TAC `{}` THEN SRW_TAC [][] ) 1961THEN1 ( 1962 RES_TAC THEN METIS_TAC [] ) 1963THEN1 ( 1964 RES_TAC THEN 1965 Q.EXISTS_TAC `fcs ��� fcs'` THEN 1966 SRW_TAC [][] THEN 1967 METIS_TAC [fresh_extra_fcs,SUBSET_UNION] ) 1968THEN Q.EXISTS_TAC `{}` THEN SRW_TAC [][] ); 1969 1970val equiv_FINITE = Q.store_thm( 1971"equiv_FINITE", 1972`���t1 t2. equiv fe t1 t2 ��� ���fcs. fcs SUBSET fe ��� FINITE fcs ��� equiv fcs t1 t2`, 1973HO_MATCH_MP_TAC equiv_ind THEN SRW_TAC [][] THEN1 ( 1974 Q.EXISTS_TAC `{}` THEN SRW_TAC [][] ) 1975THEN1 ( 1976 SRW_TAC [][Once equiv_cases] THEN 1977 Q.EXISTS_TAC `IMAGE (��a. (a,v)) (dis_set p1 p2)` THEN 1978 SRW_TAC [][SUBSET_DEF] THEN1 SRW_TAC [][] THEN 1979 MAP_EVERY Q.EXISTS_TAC [`p1`,`p2`] THEN 1980 SRW_TAC [][] ) 1981THEN1 ( 1982 SRW_TAC [][Once equiv_cases] THEN 1983 Q.EXISTS_TAC `fcs` THEN SRW_TAC [][] ) 1984THEN1 ( 1985 SRW_TAC [][Once equiv_cases] THEN 1986 IMP_RES_TAC fresh_FINITE THEN 1987 Q.EXISTS_TAC `fcs ��� fcs'` THEN 1988 SRW_TAC [][] THEN1 ( 1989 METIS_TAC [fresh_extra_fcs,SUBSET_UNION] ) 1990 THEN METIS_TAC [equiv_SUBSET,SUBSET_UNION] ) 1991THEN1 ( 1992 SRW_TAC [][Once equiv_cases] THEN 1993 Q.EXISTS_TAC `fcs ��� fcs'` THEN 1994 SRW_TAC [][] THEN 1995 METIS_TAC [equiv_SUBSET,SUBSET_UNION] ) 1996THEN Q.EXISTS_TAC `{}` THEN SRW_TAC [][]) 1997 1998val term_fcs_irrelevant_nwalkstar = Q.store_thm( 1999"term_fcs_irrelevant_nwalkstar", 2000`(term_fcs b t = SOME fcs) ��� 2001 (term_fcs b (nwalk* s t) = SOME fcs2) ��� 2002 (a,v) ��� fcs ��� v ��� FDOM s ��� 2003 nwfs s ��� 2004 (a,v) ��� fcs2`, 2005SRW_TAC [][] THEN 2006`���fcs1. (term_fcs a (nwalk* s (Sus [] v)) = SOME fcs1) ��� fcs1 ��� fcs2` 2007by METIS_TAC [term_fcs_nwalkstar] THEN 2008NTAC 2 (POP_ASSUM MP_TAC) THEN 2009ASM_SIMP_TAC (psrw_ss()) [NOT_FDOM_nvwalk] THEN 2010ASM_SIMP_TAC (psrw_ss()) [Once term_fcs_def,EXTENSION] THEN 2011SRW_TAC [][SUBSET_DEF] THEN METIS_TAC []); 2012 2013val ee = equiv_extend |> UNDISCH |> SPEC_ALL |> DISCH_ALL |> Q.GEN `tx` |> Q.GEN `pi` 2014 2015val nomunify_mgu2 = Q.store_thm( 2016"nomunify_mgu2", 2017`���s fe t1 t2 sx fex. 2018(nomunify (s,fe) t1 t2 = SOME (sx,fex)) ��� 2019(equiv fe2 (nwalk* s2 (nwalk* s t1)) (nwalk* s2 (nwalk* s t2))) ��� nwfs s2 ��� nwfs s ��� FINITE fe 2020��� (���t. equiv fe2 (nwalk* s2 (nwalk* sx t)) (nwalk* s2 (nwalk* s t)))`, 2021HO_MATCH_MP_TAC nunify_ind THEN SRW_TAC [][] THEN 2022`nwfs sx ��� s SUBMAP sx ��� FINITE fex ��� equiv fex (nwalk* sx t1) (nwalk* sx t2)` 2023by (IMP_RES_TAC nomunify_unifier THEN SRW_TAC [][]) THEN 2024FULL_SIMP_TAC (srw_ss()) [nomunify_def] THEN 2025Q.PAT_X_ASSUM `nunify p t1 t2 = SOME px` MP_TAC THEN 2026Cases_on `nwalk s t1` THEN Cases_on `nwalk s t2` THEN 2027ASM_SIMP_TAC (psrw_ss()) [Once nunify_def,LET_THM] THEN 2028SRW_TAC [][] THEN FULL_SIMP_TAC (srw_ss()) [] THEN SRW_TAC [][] 2029THEN1 ( 2030 Q.MATCH_ASSUM_RENAME_TAC `nwalk s _ = Sus pi vx` THEN 2031 Q.MATCH_ASSUM_RENAME_TAC `nwalk s _ = Nom a` THEN 2032 MATCH_MP_TAC (ee |> Q.SPECL [`pi`,`Nom a`] |> SIMP_RULE (srw_ss()) []) THEN 2033 `vx ��� FDOM s` by METIS_TAC [nwalk_to_var] THEN 2034 `(nwalk* s t1 = nwalk* s (nwalk s t1)) ��� 2035 (nwalk* s t2 = nwalk* s (nwalk s t2))` by METIS_TAC [nwalkstar_nwalk] THEN 2036 FULL_SIMP_TAC (psrw_ss()) [NOT_FDOM_nvwalk] THEN 2037 METIS_TAC [equiv_sym] ) 2038THEN1 ( 2039 Q.MATCH_ASSUM_RENAME_TAC `nwalk s _ = Sus pi vx` THEN 2040 Q.MATCH_ASSUM_RENAME_TAC `nwalk s _ = Nom a` THEN 2041 MATCH_MP_TAC (ee |> Q.SPECL [`pi`,`Nom a`] |> SIMP_RULE (srw_ss()) []) THEN 2042 `vx ��� FDOM s` by METIS_TAC [nwalk_to_var] THEN 2043 `(nwalk* s t1 = nwalk* s (nwalk s t1)) ��� 2044 (nwalk* s t2 = nwalk* s (nwalk s t2))` by METIS_TAC [nwalkstar_nwalk] THEN 2045 FULL_SIMP_TAC (psrw_ss()) [NOT_FDOM_nvwalk] THEN 2046 METIS_TAC [equiv_sym] ) 2047THEN1 ( 2048 Cases_on `x` THEN 2049 IMP_RES_TAC unify_eq_vars_preserves_s THEN 2050 FULL_SIMP_TAC (srw_ss()) [] ) 2051THEN1 ( 2052 Q.MATCH_ASSUM_RENAME_TAC `nwalk s t1 = Sus pi1 vx` THEN 2053 Q.MATCH_ASSUM_RENAME_TAC `nwalk s t2 = Sus pi2 v2` THEN 2054 MATCH_MP_TAC (ee |> Q.SPECL [`pi1`,`Sus pi2 v2`] |> SIMP_RULE (psrw_ss()) []) THEN 2055 `vx ��� FDOM s` by METIS_TAC [nwalk_to_var] THEN 2056 `(nwalk* s t1 = nwalk* s (nwalk s t1)) ��� 2057 (nwalk* s t2 = nwalk* s (nwalk s t2))` by METIS_TAC [nwalkstar_nwalk] THEN 2058 FULL_SIMP_TAC (psrw_ss()) [NOT_FDOM_nvwalk]) 2059THEN1 ( 2060 Q.MATCH_ASSUM_RENAME_TAC `nwalk s _ = Sus pi vx` THEN 2061 Q.MATCH_ASSUM_RENAME_TAC `nwalk s _ = Tie a c` THEN 2062 MATCH_MP_TAC (ee |> Q.SPECL [`pi`,`Tie a c`] |> SIMP_RULE (srw_ss()) []) THEN 2063 `vx ��� FDOM s` by METIS_TAC [nwalk_to_var] THEN 2064 `(nwalk* s t1 = nwalk* s (nwalk s t1)) ��� 2065 (nwalk* s t2 = nwalk* s (nwalk s t2))` by METIS_TAC [nwalkstar_nwalk] THEN 2066 FULL_SIMP_TAC (psrw_ss()) [NOT_FDOM_nvwalk] ) 2067THEN1 ( 2068 Q.MATCH_ASSUM_RENAME_TAC `nwalk s _ = Sus pi vx` THEN 2069 Q.MATCH_ASSUM_RENAME_TAC `nwalk s _ = nPair c1 c2` THEN 2070 MATCH_MP_TAC (ee |> Q.SPECL [`pi`,`nPair c1 c2`] |> SIMP_RULE (srw_ss()) []) THEN 2071 `vx ��� FDOM s` by METIS_TAC [nwalk_to_var] THEN 2072 `(nwalk* s t1 = nwalk* s (nwalk s t1)) ��� 2073 (nwalk* s t2 = nwalk* s (nwalk s t2))` by METIS_TAC [nwalkstar_nwalk] THEN 2074 FULL_SIMP_TAC (psrw_ss()) [NOT_FDOM_nvwalk] ) 2075THEN1 ( 2076 Q.MATCH_ASSUM_RENAME_TAC `nwalk s _ = Sus pi vx` THEN 2077 Q.MATCH_ASSUM_RENAME_TAC `nwalk s _ = nConst c` THEN 2078 MATCH_MP_TAC (ee |> Q.SPECL [`pi`,`nConst c`] |> SIMP_RULE (srw_ss()) []) THEN 2079 `vx ��� FDOM s` by METIS_TAC [nwalk_to_var] THEN 2080 `(nwalk* s t1 = nwalk* s (nwalk s t1)) ��� 2081 (nwalk* s t2 = nwalk* s (nwalk s t2))` by METIS_TAC [nwalkstar_nwalk] THEN 2082 FULL_SIMP_TAC (psrw_ss()) [NOT_FDOM_nvwalk] ) 2083THEN1 ( 2084 Q.MATCH_ASSUM_RENAME_TAC `nwalk s _ = Sus pi vx` THEN 2085 Q.MATCH_ASSUM_RENAME_TAC `nwalk s _ = Tie a c` THEN 2086 MATCH_MP_TAC (ee |> Q.SPECL [`pi`,`Tie a c`] |> SIMP_RULE (srw_ss()) []) THEN 2087 `vx ��� FDOM s` by METIS_TAC [nwalk_to_var] THEN 2088 `(nwalk* s t1 = nwalk* s (nwalk s t1)) ��� 2089 (nwalk* s t2 = nwalk* s (nwalk s t2))` by METIS_TAC [nwalkstar_nwalk] THEN 2090 FULL_SIMP_TAC (psrw_ss()) [NOT_FDOM_nvwalk] THEN 2091 METIS_TAC [equiv_sym]) 2092THEN1 ( 2093 POP_ASSUM MP_TAC THEN SRW_TAC [][] THEN 2094 POP_ASSUM MATCH_MP_TAC THEN 2095 `(nwalk* s t1 = nwalk* s (nwalk s t1)) ��� 2096 (nwalk* s t2 = nwalk* s (nwalk s t2))` by METIS_TAC [nwalkstar_nwalk] THEN 2097 Q.PAT_X_ASSUM `equiv fe2 X Y` MP_TAC THEN 2098 ASM_SIMP_TAC (srw_ss()) [Once equiv_cases] ) 2099THEN1 ( 2100 NTAC 2 (POP_ASSUM MP_TAC) THEN 2101 `(nwalk* s t1 = nwalk* s (nwalk s t1)) ��� 2102 (nwalk* s t2 = nwalk* s (nwalk s t2))` by METIS_TAC [nwalkstar_nwalk] THEN 2103 `FINITE fcs` by METIS_TAC [term_fcs_FINITE] THEN 2104 Q.PAT_X_ASSUM `equiv fe2 X Y` MP_TAC THEN 2105 ASM_SIMP_TAC (srw_ss()) [Once equiv_cases,nwalkstar_apply_pi] ) 2106THEN1 ( 2107 Q.MATCH_ASSUM_RENAME_TAC `nwalk s _ = Sus pi vx` THEN 2108 Q.MATCH_ASSUM_RENAME_TAC `nwalk s _ = nPair c1 c2` THEN 2109 MATCH_MP_TAC (ee |> Q.SPECL [`pi`,`nPair c1 c2`] |> SIMP_RULE (srw_ss()) []) THEN 2110 `vx ��� FDOM s` by METIS_TAC [nwalk_to_var] THEN 2111 `(nwalk* s t1 = nwalk* s (nwalk s t1)) ��� 2112 (nwalk* s t2 = nwalk* s (nwalk s t2))` by METIS_TAC [nwalkstar_nwalk] THEN 2113 FULL_SIMP_TAC (psrw_ss()) [NOT_FDOM_nvwalk] THEN 2114 METIS_TAC [equiv_sym]) 2115THEN1 ( 2116 Cases_on `x` THEN Cases_on `x'` THEN FULL_SIMP_TAC (srw_ss()) [] THEN 2117 SRW_TAC [][] THEN 2118 Q.MATCH_ASSUM_RENAME_TAC `nunify (s,fe) t1a t2a = SOME (sa,fa)` THEN 2119 Q.MATCH_ASSUM_RENAME_TAC `nunify (sa,fa) t1d t2d = SOME (sd,fd)` THEN 2120 `nwfs sa ��� FINITE fa ��� fa ��� fd ��� FINITE fd ��� sa SUBMAP sd ��� nwfs sd` 2121 by METIS_TAC [nunify_uP,uP_def,nunify_FINITE_fe,nunify_extends_fe] THEN 2122 `���fad. (verify_fcs fa sd = SOME fad)` by METIS_TAC [verify_fcs_SUBSET] THEN 2123 `���faa. (verify_fcs fa sa = SOME faa)` 2124 by METIS_TAC [verify_fcs_SUBMAP] THEN 2125 NTAC 2 (Q.PAT_X_ASSUM `!X.Y` MP_TAC) THEN 2126 SRW_TAC [][] THEN 2127 `(nwalk* s t1 = nwalk* s (nwalk s t1)) ��� 2128 (nwalk* s t2 = nwalk* s (nwalk s t2))` by METIS_TAC [nwalkstar_nwalk] THEN 2129 Q.PAT_X_ASSUM `equiv fe2 X Y` MP_TAC THEN 2130 SRW_TAC [][Once equiv_cases] THEN 2131 METIS_TAC [equiv_trans,equiv_refl,equiv_sym] ) 2132THEN1 ( 2133 Q.MATCH_ASSUM_RENAME_TAC `nwalk s _ = Sus pi vx` THEN 2134 Q.MATCH_ASSUM_RENAME_TAC `nwalk s _ = nConst c` THEN 2135 MATCH_MP_TAC (ee |> Q.SPECL [`pi`,`nConst c`] |> SIMP_RULE (srw_ss()) []) THEN 2136 `vx ��� FDOM s` by METIS_TAC [nwalk_to_var] THEN 2137 `(nwalk* s t1 = nwalk* s (nwalk s t1)) ��� 2138 (nwalk* s t2 = nwalk* s (nwalk s t2))` by METIS_TAC [nwalkstar_nwalk] THEN 2139 FULL_SIMP_TAC (psrw_ss()) [NOT_FDOM_nvwalk] THEN 2140 METIS_TAC [equiv_sym])); 2141 2142val term_fcs_equiv = Q.store_thm( 2143"term_fcs_equiv", 2144`equiv fe t1 t2 ��� (term_fcs a t1 = SOME fcs1) ��� fcs1 ��� fe ��� 2145 ���fcs2. (term_fcs a t2 = SOME fcs2) ��� fcs2 ��� fe`, 2146Q_TAC SUFF_TAC 2147`���t1 t2. equiv fe t1 t2 ��� ���fcs. 2148(term_fcs a t1 = SOME fcs) ��� fcs ��� fe ��� ���fcs2. (term_fcs a t2 = SOME fcs2) ��� fcs2 ��� fe` 2149THEN1 METIS_TAC [] THEN 2150HO_MATCH_MP_TAC equiv_ind THEN 2151STRIP_TAC THEN1 2152 NTAC 2 (SRW_TAC [][Once term_fcs_def]) 2153THEN STRIP_TAC THEN1 ( 2154 NTAC 2 (ASM_SIMP_TAC (psrw_ss()) [Once term_fcs_def]) THEN 2155 SRW_TAC [][dis_set_def,SUBSET_DEF] THEN 2156 FULL_SIMP_TAC (srw_ss()) [] THEN 2157 Cases_on `lswapstr (REVERSE p1) a = lswapstr (REVERSE p2) a` THEN1 METIS_TAC [] THEN 2158 FIRST_ASSUM MATCH_MP_TAC THEN 2159 ASM_SIMP_TAC (srw_ss()) [] THEN 2160 SPOSE_NOT_THEN STRIP_ASSUME_TAC THEN 2161 `lswapstr (REVERSE p1) (lswapstr p1 (lswapstr (REVERSE p2) a)) ��� lswapstr (REVERSE p2) a` 2162 by METIS_TAC [] THEN 2163 POP_ASSUM MP_TAC THEN SIMP_TAC (srw_ss()) []) 2164THEN STRIP_TAC THEN1 ( 2165 SRW_TAC [][] THEN 2166 Q.PAT_X_ASSUM `term_fcs a X = Y` MP_TAC THEN 2167 NTAC 2 (SRW_TAC [][Once term_fcs_def]) ) 2168THEN STRIP_TAC THEN1 ( 2169 SRW_TAC [][] THEN 2170 Q.PAT_X_ASSUM `term_fcs a X = Y` MP_TAC THEN 2171 SRW_TAC [][Once term_fcs_def] THEN1 ( 2172 SRW_TAC [][Once term_fcs_def] THEN 2173 Cases_on `term_fcs a t2` THEN1 2174 IMP_RES_TAC term_fcs_NONE THEN 2175 IMP_RES_TAC term_fcs_minimal THEN 2176 METIS_TAC [] ) THEN 2177 SRW_TAC [][Once term_fcs_def] THEN 2178 FULL_SIMP_TAC (srw_ss()) [] THEN 2179 IMP_RES_TAC term_fcs_apply_pi THEN 2180 POP_ASSUM (Q.SPEC_THEN `REVERSE [(a1,a2)]` MP_TAC) THEN 2181 SIMP_TAC (srw_ss()) [] THEN 2182 ASM_SIMP_TAC (srw_ss()) []) 2183THEN STRIP_TAC THEN1 ( 2184 SRW_TAC [][] THEN 2185 Q.PAT_X_ASSUM `term_fcs a X = Y` MP_TAC THEN 2186 SRW_TAC [][Once term_fcs_def] THEN 2187 SRW_TAC [][Once term_fcs_def] THEN 2188 FULL_SIMP_TAC (srw_ss()) [] ) 2189THEN NTAC 2 (SRW_TAC [][Once term_fcs_def])); 2190 2191val nvwalk_SUBMAP_idem = Q.store_thm( 2192"nvwalk_SUBMAP_idem", 2193`nwfs sx ��� s SUBMAP sx ��� ���pi v. nwalk s (nvwalk sx pi v) = nvwalk sx pi v`, 2194STRIP_TAC THEN IMP_RES_TAC nwfs_SUBMAP THEN 2195HO_MATCH_MP_TAC (Q.INST[`s`|->`sx`]nvwalk_ind) THEN 2196SRW_TAC [][] THEN 2197Cases_on `FLOOKUP sx v` THEN1 ( 2198 Cases_on `FLOOKUP s v` THEN 2199 IMP_RES_TAC FLOOKUP_SUBMAP THEN 2200 FULL_SIMP_TAC (srw_ss()) [] THEN 2201 NTAC 3 (SRW_TAC [][Once nvwalk_def]) ) THEN 2202Cases_on `x` THEN FULL_SIMP_TAC (psrw_ss()) [] THEN 2203TRY ( 2204 NTAC 2 (ASM_SIMP_TAC (psrw_ss()) [Once nvwalk_def]) THEN 2205 NO_TAC ) THEN 2206ASM_SIMP_TAC (srw_ss()) [Once nvwalk_def] THEN 2207ASM_SIMP_TAC (srw_ss()) [Once nvwalk_def,SimpRHS] THEN 2208SELECT_ELIM_TAC THEN 2209SRW_TAC [][] THEN 2210METIS_TAC [nvwalk_eq_perms,permeq_refl,app_permeq_monotone]); 2211 2212val nwalkstar_SUBMAP_idem = Q.store_thm( 2213"nwalkstar_SUBMAP_idem", 2214`nwfs sx ��� s SUBMAP sx ��� ���t.nwalk* s (nwalk* sx t) = nwalk* sx t`, 2215STRIP_TAC THEN IMP_RES_TAC nwfs_SUBMAP THEN 2216HO_MATCH_MP_TAC (Q.INST[`s`|->`sx`]nwalkstar_ind) THEN 2217SRW_TAC [][] THEN 2218`nwalk* sx t = nwalk* sx (nwalk sx t)` by METIS_TAC [nwalkstar_nwalk] THEN 2219Cases_on `nwalk s t` THEN 2220MP_TAC nwalk_SUBMAP THEN SRW_TAC [][] THEN 2221Cases_on `nwalk sx t` THEN FULL_SIMP_TAC (srw_ss()) [] THEN 2222Q.PAT_X_ASSUM `nwfs s` ASSUME_TAC THEN 2223Q.PAT_X_ASSUM `nwfs sx` ASSUME_TAC THEN 2224Cases_on `t` THEN FULL_SIMP_TAC (psrw_ss()) [] THEN 2225Cases_on `nvwalk sx l' n'` THEN FULL_SIMP_TAC (psrw_ss()) [] THEN 2226IMP_RES_TAC nvwalk_to_var THEN 2227Q.MATCH_ASSUM_RENAME_TAC `v ��� FDOM sx` THEN 2228`v ��� FDOM s` by METIS_TAC [SUBMAP_DEF,SUBSET_DEF] THEN 2229SRW_TAC [][] THEN 2230FULL_SIMP_TAC (srw_ss()) [NOT_FDOM_nvwalk]); 2231 2232val unify_eq_vars_NOTIN_FDOM = Q.store_thm( 2233"unify_eq_vars_NOTIN_FDOM", 2234`FINITE ds ��� nwfs s ��� (unify_eq_vars ds v (s,fe) = SOME (s',fex)) ��� (b,w) ��� fe ��� (b,w) ��� fex ��� w ��� FDOM s`, 2235SIMP_TAC (srw_ss()) [GSYM AND_IMP_INTRO] THEN 2236STRIP_TAC THEN 2237SPEC_ALL_TAC [`ds`] THEN 2238POP_ASSUM MP_TAC THEN 2239Q.ID_SPEC_TAC `ds` THEN 2240HO_MATCH_MP_TAC FINITE_INDUCT THEN 2241SIMP_TAC (srw_ss()) [unify_eq_vars_def,ITSET_EMPTY] THEN 2242SRW_TAC [][] THEN SRW_TAC [][] THEN 2243Q.PAT_X_ASSUM `X = SOME fex'` MP_TAC THEN 2244FULL_SIMP_TAC (srw_ss()) [DELETE_NON_ELEMENT,fcs_acc_RECURSES,fcs_acc_def,image_lem] THEN 2245FULL_SIMP_TAC (srw_ss()) [GSYM DELETE_NON_ELEMENT] THEN 2246SRW_TAC [][GSYM DELETE_NON_ELEMENT] THEN 2247SRW_TAC [][] THEN 2248FULL_SIMP_TAC (srw_ss()) [] THEN1 ( 2249 FIRST_X_ASSUM (Q.SPECL_THEN [`s`,`v`,`{}`,`s`,`x1`,`b`,`w`] MP_TAC) 2250 THEN SRW_TAC [][] ) THEN 2251MATCH_MP_TAC (GEN_ALL term_fcs_NOTIN_FDOM) THEN 2252MAP_EVERY Q.EXISTS_TAC [`Sus [] v`,`x2`,`b`,`e`] THEN 2253SRW_TAC [][]); 2254 2255val nunify_fcs_NOTIN_FDOM = Q.store_thm ( 2256"nunify_fcs_NOTIN_FDOM", 2257`���s fe t1 t2 sx fex. nwfs s ��� FINITE fe ��� 2258(nunify (s,fe) t1 t2 = SOME (sx,fex)) ��� (a,v) ��� fe ��� (a,v) ��� fex ��� 2259v ��� FDOM s`, 2260HO_MATCH_MP_TAC nunify_ind THEN SRW_TAC [][] THEN 2261Q.PAT_X_ASSUM `nunify p t1 t2 = SOME px` MP_TAC THEN 2262Cases_on `nwalk s t1` THEN Cases_on `nwalk s t2` THEN 2263ASM_SIMP_TAC (psrw_ss()) [Once nunify_def,LET_THM] THEN 2264SRW_TAC [][] THEN 2265FULL_SIMP_TAC (srw_ss()) [] THEN1 ( 2266 IMP_RES_TAC unify_eq_vars_NOTIN_FDOM THEN 2267 FULL_SIMP_TAC (srw_ss()) [] ) 2268THEN1 ( 2269 NTAC 2 (POP_ASSUM MP_TAC) THEN 2270 SRW_TAC [][] THEN 2271 Cases_on `(a,v) ��� fcs` THEN1 ( 2272 IMP_RES_TAC term_fcs_NOTIN_FDOM ) THEN 2273 IMP_RES_TAC term_fcs_FINITE THEN 2274 FULL_SIMP_TAC (srw_ss()) [] ) THEN 2275NTAC 2 (POP_ASSUM MP_TAC) THEN 2276Cases_on `x` THEN SRW_TAC [][] THEN 2277Q.MATCH_ASSUM_RENAME_TAC `nunify (s,fe) t1a t2a = SOME (sa,fa)` THEN 2278Cases_on `(a,v) ��� fa` THEN FULL_SIMP_TAC (srw_ss()) [] THEN 2279`nwfs sa ��� FINITE fa ��� s SUBMAP sa` by METIS_TAC [nunify_uP,uP_def,nunify_FINITE_fe] THEN 2280METIS_TAC [SUBMAP_DEF,SUBSET_DEF]); 2281 2282val GEN_SUBMAP_FUPDATE_EQN = Q.store_thm( 2283"GEN_SUBMAP_FUPDATE_EQN", 2284`f SUBMAP g |+ (k,v) ��� k ��� FDOM f ��� f SUBMAP g ��� k ��� FDOM f ��� (f \\ k) SUBMAP g ��� (f ' k = v)`, 2285SRW_TAC [][EQ_IMP_THM] THEN1 ( 2286 Cases_on `k ��� FDOM f` THEN SRW_TAC [][] THEN 2287 FULL_SIMP_TAC (srw_ss()) [SUBMAP_DEF] THEN 2288 SRW_TAC [][DOMSUB_FAPPLY_THM,FAPPLY_FUPDATE_THM] THEN 2289 METIS_TAC [] ) THEN 2290FULL_SIMP_TAC (srw_ss()) [SUBMAP_DEF,DOMSUB_FAPPLY_THM,FAPPLY_FUPDATE_THM] THEN 2291SRW_TAC [][]) 2292 2293val fresh_term_fcs = Q.store_thm( 2294"fresh_term_fcs", 2295`fresh fe a t ��� (���fcs. (term_fcs a t = SOME fcs) ��� fcs ��� fe)`, 2296SRW_TAC [][] THEN Cases_on `term_fcs a t` THEN 2297IMP_RES_TAC term_fcs_NONE THEN 2298IMP_RES_TAC term_fcs_minimal THEN 2299SRW_TAC [][]); 2300 2301val equiv_fcs_q = ` 2302 (equiv_fcs (Nom a) (Nom b) = if a = b then SOME {} else NONE) ��� 2303 (equiv_fcs (Sus p1 v1) (Sus p2 v2) = 2304 if v1 = v2 then SOME {(a,v1) | a ��� dis_set p1 p2} else NONE) ��� 2305 (equiv_fcs (Tie a1 t1) (Tie a2 t2) = 2306 if a1 = a2 then equiv_fcs t1 t2 2307 else OPTION_MAP2 $UNION (term_fcs a1 t2) 2308 (equiv_fcs t1 (apply_pi [(a1,a2)] t2))) ��� 2309 (equiv_fcs (nPair t1a t1d) (nPair t2a t2d) = 2310 OPTION_MAP2 $UNION (equiv_fcs t1a t2a) (equiv_fcs t1d t2d)) ��� 2311 (equiv_fcs (nConst c1) (nConst c2) = if c1 = c2 then SOME {} else NONE) ��� 2312 (equiv_fcs t1 t2 = NONE)` 2313 2314val equiv_fcs_def = Define equiv_fcs_q; 2315val _ = export_rewrites ["equiv_fcs_def"] 2316val _ = store_term_thm("equiv_fcs_def_print",TermWithCase equiv_fcs_q); 2317 2318val equiv_fcs_minimal = Q.store_thm( 2319"equiv_fcs_minimal", 2320`���t1 t2. equiv fe t1 t2 ��� ���fe0. (equiv_fcs t1 t2 = SOME fe0) ��� fe0 ��� fe`, 2321HO_MATCH_MP_TAC equiv_ind THEN 2322ASM_SIMP_TAC (psrw_ss()) [] THEN 2323SRW_TAC [][] THEN1 ( 2324 SRW_TAC [][SUBSET_DEF] THEN 2325 RES_TAC ) 2326THEN1 ( 2327 IMP_RES_TAC fresh_term_fcs THEN 2328 SRW_TAC [][] ) THEN 2329SRW_TAC [][]); 2330 2331val equiv_fcs_equiv = Q.store_thm( 2332"equiv_fcs_equiv", 2333`���t1 t2 fe. (equiv_fcs t1 t2 = SOME fe) ��� equiv fe t1 t2`, 2334Induct THEN Cases_on `t2` THEN 2335FULL_SIMP_TAC (psrw_ss()) [] THEN 2336SRW_TAC [][] THEN 2337SRW_TAC [][Once equiv_cases] THEN 2338FULL_SIMP_TAC (srw_ss()) [] THEN 2339METIS_TAC [permeq_refl,equiv_SUBSET,SUBSET_UNION,fresh_extra_fcs,term_fcs_fresh]); 2340 2341val nwalk_apply_pi = Q.store_thm( 2342"nwalk_apply_pi", 2343`nwfs s ��� (nwalk s (apply_pi pi t) = apply_pi pi (nwalk s t))`, 2344Induct_on `t` THEN ASM_SIMP_TAC (psrw_ss()) [] THEN 2345SRW_TAC [][] THEN 2346(nvwalk_modulo_pi |> Q.SPECL [`s`,`l`,`n`] |> MP_TAC) THEN 2347(nvwalk_modulo_pi |> Q.SPECL [`s`,`pi ++ l`,`n`] |> MP_TAC) THEN 2348SRW_TAC [][apply_pi_decompose]); 2349 2350val _ = add_rule { 2351 fixity = Infix(NONASSOC,450), 2352 term_name = "equiv", 2353 block_style = (AroundEachPhrase,(PP.INCONSISTENT,2)), 2354 paren_style = OnlyIfNecessary, 2355 pp_elements = 2356 [BreakSpace(1,2),TOK"���",BreakSpace(1,2),TM,BreakSpace(1,2),TOK"���",BreakSpace(1,2)] } 2357 2358val _ = add_rule { 2359 fixity = Infix(NONASSOC,450), 2360 term_name = "fresh", 2361 block_style = (AroundEachPhrase,(PP.INCONSISTENT,2)), 2362 paren_style = OnlyIfNecessary, 2363 pp_elements = 2364 [BreakSpace(1,2),TOK"���",BreakSpace(1,2),TM,BreakSpace(1,2),TOK"#",BreakSpace(1,2)] } 2365 2366val equiv_fcs_nwalkstar = Q.store_thm( 2367"equiv_fcs_nwalkstar", 2368`(equiv_fcs t1 t2 = SOME fe1) ��� 2369 (equiv_fcs (nwalk* s t1) (nwalk* s t2) = SOME fe2) ��� 2370 (a,v) ��� fe1 ��� nwfs s ��� 2371 ���fcs. (term_fcs a (nwalk* s (Sus [] v)) = SOME fcs) ��� fcs ��� fe2`, 2372MAP_EVERY Q.ID_SPEC_TAC [`fe2`,`fe1`,`t2`,`t1`] THEN 2373Induct THEN Cases_on `t2` THEN FULL_SIMP_TAC (psrw_ss()) [] THEN1 ( 2374 SRW_TAC [][] THEN 2375 Q.MATCH_ASSUM_RENAME_TAC `equiv_fcs (nwalk* s (Sus p1 v)) (nwalk* s (Sus p2 v)) = SOME fe2` THEN 2376 `equiv fe2 (apply_pi p1 (nwalk* s (Sus [] v))) (apply_pi p2 (nwalk* s (Sus [] v)))` by ( 2377 IMP_RES_TAC equiv_fcs_equiv THEN 2378 POP_ASSUM MP_TAC THEN 2379 ASM_SIMP_TAC (psrw_ss()) [GSYM nwalkstar_apply_pi] ) THEN 2380 IMP_RES_TAC equiv_ds_fresh THEN 2381 IMP_RES_TAC fresh_term_fcs THEN 2382 Q.PAT_X_ASSUM `nwfs s` ASSUME_TAC THEN 2383 FULL_SIMP_TAC (srw_ss()) [] ) 2384THEN1 ( 2385 SRW_TAC [][] THEN1 ( 2386 FULL_SIMP_TAC (srw_ss()) [] THEN 2387 METIS_TAC [] ) THEN 2388 Q.PAT_X_ASSUM `a1 ��� a2` ASSUME_TAC THEN 2389 FULL_SIMP_TAC (srw_ss()) [] THEN1 ( 2390 IMP_RES_TAC term_fcs_nwalkstar THEN 2391 Q.PAT_X_ASSUM `nwfs s` ASSUME_TAC THEN 2392 FULL_SIMP_TAC (srw_ss()) [] THEN 2393 METIS_TAC [SUBSET_UNION,SUBSET_TRANS] ) THEN 2394 FULL_SIMP_TAC (srw_ss()) [GSYM nwalkstar_apply_pi] THEN 2395 RES_TAC THEN 2396 METIS_TAC [SUBSET_UNION,SUBSET_TRANS] ) 2397THEN1 ( 2398 SRW_TAC [][] THEN 2399 FULL_SIMP_TAC (srw_ss()) [] THEN 2400 RES_TAC THEN 2401 METIS_TAC [SUBSET_UNION,SUBSET_TRANS] )); 2402 2403val term_fcs_SUBMAP = Q.store_thm( 2404"term_fcs_SUBMAP", 2405`(term_fcs a (nwalk* s t) = SOME fcs) ��� nwfs s ��� 2406 ���fe0. (term_fcs a t = SOME fe0) ��� 2407 ���b w. (b,w) ��� fe0 ��� ���fe1. (term_fcs b (nwalk* s (Sus [] w)) = SOME fe1) ��� fe1 ��� fcs`, 2408REPEAT STRIP_TAC THEN 2409IMP_RES_TAC term_fcs_fresh THEN 2410IMP_RES_TAC fresh_SUBMAP THEN 2411IMP_RES_TAC fresh_term_fcs THEN 2412Q.MATCH_ASSUM_RENAME_TAC `term_fcs a t = SOME fe0` THEN 2413Q.EXISTS_TAC `fe0` THEN CONJ_TAC THEN1 SRW_TAC [][] THEN 2414REPEAT STRIP_TAC THEN 2415`(b,w) ��� fe` by FULL_SIMP_TAC (srw_ss()) [SUBSET_DEF] THEN 2416RES_TAC THEN 2417IMP_RES_TAC fresh_term_fcs THEN 2418SRW_TAC [][]) 2419 2420val term_fcs_nwalkstar_backwards = Q.store_thm( 2421"term_fcs_nwalkstar_backwards", 2422`nwfs s ��� (term_fcs b (nwalk* s t) = SOME fcs) ��� (a,v) ��� fcs ��� 2423 (term_fcs b t = SOME fe0) ��� 2424 ���c w fe1. (c,w) ��� fe0 ��� (term_fcs c (nwalk* s (Sus [] w)) = SOME fe1) ��� (a,v) ��� fe1`, 2425STRIP_TAC THEN 2426NTAC 3 (POP_ASSUM MP_TAC) THEN 2427SPEC_ALL_TAC [`t`,`s`] THEN 2428Q.ID_SPEC_TAC `t` THEN HO_MATCH_MP_TAC nwalkstar_ind THEN 2429REPEAT STRIP_TAC THEN 2430`nwalk* s t = nwalk* s (nwalk s t)` by METIS_TAC [nwalkstar_nwalk] THEN 2431Cases_on `nwalk s t` THEN 2432Q.PAT_X_ASSUM `nwfs s` ASSUME_TAC THEN 2433FULL_SIMP_TAC (srw_ss()) [] THEN1 ( 2434 FULL_SIMP_TAC (srw_ss()) [Once term_fcs_def] THEN 2435 SRW_TAC [][] THEN 2436 FULL_SIMP_TAC (srw_ss()) [] ) 2437THEN1 ( 2438 `n ��� FDOM s` by METIS_TAC [nwalk_to_var] THEN 2439 FULL_SIMP_TAC (psrw_ss()) [NOT_FDOM_nvwalk] THEN 2440 FULL_SIMP_TAC (psrw_ss()) [Once term_fcs_def] THEN 2441 SRW_TAC [][] THEN 2442 Cases_on `t` THEN FULL_SIMP_TAC (psrw_ss()) [] THEN 2443 SRW_TAC [][] THEN 2444 (nvwalk_modulo_pi |> Q.SPECL [`s`,`l'`,`n'`] |> GSYM |> MP_TAC) THEN 2445 ASM_SIMP_TAC (psrw_ss()) [apply_pi_eql] THEN 2446 SRW_TAC [][REVERSE_APPEND,pmact_decompose] ) 2447THEN1 ( 2448 Q.PAT_X_ASSUM `X = SOME fcs` MP_TAC THEN 2449 ASM_SIMP_TAC (srw_ss()) [Once term_fcs_def] THEN 2450 Cases_on `b = s'` THEN FULL_SIMP_TAC (srw_ss()) [] THEN 2451 SRW_TAC [][] THEN FULL_SIMP_TAC (srw_ss()) [] THEN 2452 Cases_on `t` THEN FULL_SIMP_TAC (srw_ss()) [] THEN1 ( 2453 Q.PAT_X_ASSUM `X = SOME fe0` MP_TAC THEN 2454 ASM_SIMP_TAC (psrw_ss()) [Once term_fcs_def] THEN 2455 SRW_TAC [][] THEN SRW_TAC [][] THEN 2456 (nvwalk_modulo_pi |> Q.SPECL [`s`,`l`,`n`] |> GSYM |> MP_TAC) THEN 2457 ASM_SIMP_TAC (psrw_ss()) [apply_pi_eql] THEN 2458 SRW_TAC [][Once term_fcs_def,nwalkstar_apply_pi] THEN 2459 Q.EXISTS_TAC `fcs` THEN SRW_TAC [][] THEN 2460 MATCH_MP_TAC term_fcs_apply_pi THEN 2461 SRW_TAC [][] ) THEN 2462 Q.PAT_X_ASSUM `X = SOME fe0` MP_TAC THEN 2463 SRW_TAC [][Once term_fcs_def] THEN 2464 METIS_TAC [] ) 2465THEN1 ( 2466 Q.PAT_X_ASSUM `X = SOME fcs` MP_TAC THEN 2467 ASM_SIMP_TAC (srw_ss()) [Once term_fcs_def] THEN 2468 Cases_on `t` THEN FULL_SIMP_TAC (srw_ss()) [] THEN1 ( 2469 Q.PAT_X_ASSUM `X = SOME fe0` MP_TAC THEN 2470 ASM_SIMP_TAC (psrw_ss()) [Once term_fcs_def] THEN 2471 SRW_TAC [][] THEN SRW_TAC [][] THEN 2472 (nvwalk_modulo_pi |> Q.SPECL [`s`,`l`,`n`] |> GSYM |> MP_TAC) THEN 2473 ASM_SIMP_TAC (psrw_ss()) [apply_pi_eql] THEN 2474 SRW_TAC [][Once term_fcs_def,nwalkstar_apply_pi] THEN 2475 Q.EXISTS_TAC `x1 ��� x2` THEN SRW_TAC [][] THEN 2476 MAP_EVERY Q.EXISTS_TAC [`x1`,`x2`] THEN 2477 SRW_TAC [][] THEN 2478 MATCH_MP_TAC term_fcs_apply_pi THEN 2479 SRW_TAC [][] ) THEN 2480 Q.PAT_X_ASSUM `X = SOME fe0` MP_TAC THEN 2481 ASM_SIMP_TAC (psrw_ss()) [Once term_fcs_def] THEN 2482 SRW_TAC [][] THEN 2483 FULL_SIMP_TAC (srw_ss()) [] THEN 2484 METIS_TAC []) THEN 2485FULL_SIMP_TAC (srw_ss()) [Once term_fcs_def] THEN 2486SRW_TAC [][] THEN FULL_SIMP_TAC (srw_ss()) []) 2487 2488val nomunify_equiv_fcs = Q.store_thm( 2489"nomunify_equiv_fcs", 2490`(nomunify (s,fe) t1 t2 = SOME (sx,fex)) ��� (a,v) ��� fex ��� nwfs s ��� FINITE fe ��� 2491 (��� b w fcs. (b,w) ��� fe ��� (term_fcs b (nwalk* sx (Sus [] w)) = SOME fcs) ��� (a,v) ��� fcs) ��� 2492 (a,v) ��� THE (equiv_fcs (nwalk* sx t1) (nwalk* sx t2))`, 2493Q_TAC SUFF_TAC 2494`���s fe t1 t2 sx sxx b w fex fcs fem fev. (nunify (s,fe) t1 t2 = SOME (sx,fex)) ��� (b,w) ��� fe ��� (b,w) ��� fex ��� 2495 nwfs sxx ��� sx SUBMAP sxx ��� 2496 (term_fcs b (nwalk* sxx (Sus [] w)) = SOME fcs) ��� (a,v) ��� fcs ��� 2497 nwfs s ��� FINITE fe ��� (equiv_fcs (nwalk* sxx t1) (nwalk* sxx t2) = SOME fem) ��� 2498 (a,v) ��� fem` THEN1 ( 2499 REPEAT STRIP_TAC THEN 2500 IMP_RES_TAC nomunify_unifier THEN 2501 NTAC 3 (Q.PAT_X_ASSUM `!X.Y` (K ALL_TAC)) THEN 2502 IMP_RES_TAC equiv_fcs_minimal THEN 2503 FULL_SIMP_TAC (srw_ss()) [nomunify_def,EXISTS_PROD] THEN 2504 Q.MATCH_ASSUM_RENAME_TAC `nunify (s,fe) t1 t2 = SOME (sx,fx)` THEN 2505 `FINITE fx` by IMP_RES_TAC nunify_FINITE_fe THEN 2506 `���b w fcs. (b,w) ��� fx ��� (term_fcs b (nwalk* sx (Sus [] w)) = SOME fcs) ��� (a,v) ��� fcs` 2507 by (MATCH_MP_TAC (GEN_ALL verify_fcs_minimal) THEN SRW_TAC [][]) THEN 2508 Q.PAT_X_ASSUM `nwfs sx` ASSUME_TAC THEN 2509 FULL_SIMP_TAC (srw_ss()) [] THEN 2510 Cases_on `(b,w) ��� fe` THEN1 METIS_TAC [] THEN 2511 FIRST_X_ASSUM (Q.SPECL_THEN [`s`,`fe`,`t1`,`t2`,`sx`,`sx`,`b`,`w`,`fx`,`fcs`,`fe0`] MP_TAC) THEN 2512 SRW_TAC [][] ) THEN 2513HO_MATCH_MP_TAC nunify_ind THEN REPEAT STRIP_TAC THEN 2514Q.PAT_X_ASSUM `nunify p t1 t2 = SOME px` MP_TAC THEN 2515Q.PAT_X_ASSUM `nwfs s` MP_TAC THEN 2516Cases_on `nwalk s t1` THEN Cases_on `nwalk s t2` THEN 2517NTAC 2 (POP_ASSUM MP_TAC) THEN 2518SIMP_TAC (psrw_ss()) [Once nunify_def,LET_THM] THEN 2519REPEAT STRIP_TAC THEN 2520FULL_SIMP_TAC (srw_ss()) [] THEN1 ( 2521 POP_ASSUM MP_TAC THEN SRW_TAC [][] THEN1 ( 2522 IMP_RES_TAC unify_eq_vars_preserves_s THEN 2523 IMP_RES_TAC unify_eq_vars_minimal THEN 2524 NTAC 2 (FULL_SIMP_TAC (srw_ss()) []) THEN 2525 SRW_TAC [][] THEN 2526 `(nwalk* sxx t1 = nwalk* sxx (nwalk s t1)) ��� 2527 (nwalk* sxx t2 = nwalk* sxx (nwalk s t2))` 2528 by METIS_TAC [nwalkstar_nwalk_SUBMAP] THEN 2529 Q.PAT_X_ASSUM `nwfs s` ASSUME_TAC THEN 2530 `n ��� FDOM s` by METIS_TAC [nwalk_to_var] THEN 2531 FULL_SIMP_TAC (psrw_ss()) [NOT_FDOM_nvwalk] THEN 2532 IMP_RES_TAC equiv_fcs_equiv THEN 2533 `equiv fem (apply_pi l (nwalk* sxx (Sus [] n))) (apply_pi l' (nwalk* sxx (Sus [] n)))` by ( 2534 POP_ASSUM MP_TAC THEN 2535 ASM_SIMP_TAC (psrw_ss()) [GSYM nwalkstar_apply_pi] ) THEN 2536 IMP_RES_TAC equiv_ds_fresh THEN 2537 Q.PAT_X_ASSUM `X = SOME fcs'` MP_TAC THEN 2538 ASM_SIMP_TAC (psrw_ss()) [Once term_fcs_def] THEN 2539 SRW_TAC [][] THEN 2540 FULL_SIMP_TAC (srw_ss()) [] THEN SRW_TAC [][] THEN 2541 IMP_RES_TAC term_fcs_minimal THEN 2542 FULL_SIMP_TAC (srw_ss()) [SUBSET_DEF] ) THEN 2543 FULL_SIMP_TAC (srw_ss()) [] ) 2544THEN1 ( 2545 POP_ASSUM MP_TAC THEN SRW_TAC [][] THEN1 ( 2546 POP_ASSUM MP_TAC THEN 2547 `nwfs sx ��� s SUBMAP sx` by METIS_TAC [nunify_uP,uP_def] THEN 2548 `(nwalk* sxx t1 = nwalk* sxx (nwalk s t1)) ��� 2549 (nwalk* sxx t2 = nwalk* sxx (nwalk s t2))` 2550 by METIS_TAC [nwalkstar_nwalk_SUBMAP,SUBMAP_TRANS] THEN 2551 Q.PAT_X_ASSUM `nwfs sxx` ASSUME_TAC THEN 2552 FULL_SIMP_TAC (srw_ss()) [] THEN 2553 STRIP_TAC THEN POP_ASSUM MATCH_MP_TAC THEN 2554 MAP_EVERY Q.EXISTS_TAC [`sxx`,`b`,`w`] THEN 2555 SRW_TAC [][]) THEN 2556 FULL_SIMP_TAC (srw_ss()) [] THEN 2557 Q.MATCH_ASSUM_RENAME_TAC `nwalk s t1 = Tie a1 c1` THEN 2558 Q.MATCH_ASSUM_RENAME_TAC `nwalk s t2 = Tie a2 c2` THEN 2559 `nwfs sx ��� s SUBMAP sx` by METIS_TAC [nunify_uP,uP_def] THEN 2560 `(nwalk* sxx t1 = nwalk* sxx (nwalk s t1)) ��� 2561 (nwalk* sxx t2 = nwalk* sxx (nwalk s t2))` 2562 by METIS_TAC [nwalkstar_nwalk_SUBMAP,SUBMAP_TRANS] THEN 2563 IMP_RES_TAC equiv_fcs_equiv THEN 2564 POP_ASSUM MP_TAC THEN ASM_SIMP_TAC (srw_ss()) [] THEN 2565 STRIP_TAC THEN IMP_RES_TAC equiv_ties_fcs THEN 2566 Cases_on `(b,w) ��� fcs'` THEN1 ( 2567 (term_fcs_nwalkstar |> 2568 Q.INST [`s`|->`sxx`,`t`|->`nwalk* s c2`,`b`|->`a1`,`a`|->`b`, 2569 `v`|->`w`,`fcs`|->`fcs'`,`fcs2`|->`fcs''`] |> 2570 MP_TAC) THEN 2571 `nwalk* sxx (nwalk* s c2) = nwalk* sxx c2` by METIS_TAC [nwalkstar_SUBMAP,SUBMAP_TRANS] THEN 2572 SRW_TAC [][] THEN FULL_SIMP_TAC (srw_ss()) [] THEN 2573 SRW_TAC [][] THEN FULL_SIMP_TAC (srw_ss()) [SUBSET_DEF] ) THEN 2574 Q.PAT_X_ASSUM `nwfs sxx` ASSUME_TAC THEN 2575 IMP_RES_TAC term_fcs_FINITE THEN 2576 FULL_SIMP_TAC (srw_ss()) [nwalkstar_apply_pi] THEN 2577 DISJ2_TAC THEN 2578 FIRST_X_ASSUM MATCH_MP_TAC THEN 2579 MAP_EVERY Q.EXISTS_TAC [`sxx`,`b`,`w`] THEN 2580 SRW_TAC [][nwalkstar_apply_pi]) 2581THEN1 ( 2582 Cases_on `x` THEN FULL_SIMP_TAC (srw_ss()) [] THEN 2583 Q.MATCH_ASSUM_RENAME_TAC `nunify (s,fe) t1a t2a = SOME (sa,fa)` THEN 2584 Q.MATCH_ASSUM_RENAME_TAC `nunify (sa,fa) t1d t2d = SOME (sd,fd)` THEN 2585 `nwfs sa ��� FINITE fa ��� fa ��� fd ��� FINITE fd ��� s SUBMAP sa ��� sa SUBMAP sd ��� nwfs sd` 2586 by METIS_TAC [nunify_uP,uP_def,nunify_FINITE_fe,nunify_extends_fe] THEN 2587 `(nwalk* sxx t1 = nwalk* sxx (nwalk s t1)) ��� 2588 (nwalk* sxx t2 = nwalk* sxx (nwalk s t2))` 2589 by METIS_TAC [nwalkstar_nwalk_SUBMAP,SUBMAP_TRANS] THEN 2590 Q.PAT_X_ASSUM `nwfs sxx` ASSUME_TAC THEN 2591 FULL_SIMP_TAC (srw_ss()) [] THEN SRW_TAC [][] THEN 2592 REVERSE (Cases_on `(b,w) ��� fa`) THEN1 ( 2593 NTAC 2 (FIRST_X_ASSUM (Q.SPECL_THEN [`sxx`,`b`,`w`] MP_TAC)) THEN 2594 SRW_TAC [][] ) THEN 2595 NTAC 2 (FIRST_X_ASSUM (Q.SPECL_THEN [`sxx`,`b`,`w`] MP_TAC)) THEN 2596 SRW_TAC [][] THEN 2597 DISJ1_TAC THEN POP_ASSUM MATCH_MP_TAC THEN 2598 METIS_TAC [SUBMAP_TRANS] )) 2599 2600val nomunify_mgu1 = Q.store_thm( 2601"nomunify_mgu1", 2602`(nomunify (s,fe) t1 t2 = SOME (sx,fex)) ��� (a,v) ��� fex ��� 2603(equiv fe2 (nwalk* s2 (nwalk* s t1)) (nwalk* s2 (nwalk* s t2))) ��� nwfs s2 ��� nwfs s ��� FINITE fe 2604��� (��� b w fcs. (b,w) ��� fe ��� (term_fcs b (nwalk* sx (Sus [] w)) = SOME fcs) ��� (a,v) ��� fcs) ��� 2605fresh fe2 a (nwalk* s2 (Sus [] v))`, 2606REPEAT STRIP_TAC THEN 2607(nomunify_equiv_fcs |> SIMP_RULE bool_ss [GSYM AND_IMP_INTRO] |> funpow 4 UNDISCH |> STRIP_ASSUME_TAC ) 2608THEN1 METIS_TAC [] THEN DISJ2_TAC THEN 2609`equiv fex (nwalk* sx t1) (nwalk* sx t2)` by METIS_TAC [nomunify_unifier] THEN 2610`���t. equiv fe2 (nwalk* s2 (nwalk* sx t)) (nwalk* s2 (nwalk* s t))` by METIS_TAC [nomunify_mgu2] THEN 2611`equiv fe2 (nwalk* s2 (nwalk* sx t1)) (nwalk* s2 (nwalk* sx t2))` by METIS_TAC [equiv_trans,equiv_sym] THEN 2612IMP_RES_TAC equiv_fcs_minimal THEN 2613Q_TAC SUFF_TAC `���fcs. (term_fcs a (nwalk* s2 (Sus [] v)) = SOME fcs) ��� fcs ��� fe0` 2614THEN1 METIS_TAC [fresh_extra_fcs,term_fcs_fresh,SUBSET_TRANS] THEN 2615MATCH_MP_TAC (GEN_ALL equiv_fcs_nwalkstar) THEN 2616MAP_EVERY Q.EXISTS_TAC [`nwalk* sx t2`,`nwalk* sx t1`,`fe0'`] THEN 2617FULL_SIMP_TAC (srw_ss()) []) 2618 2619val nomunify_mgu = Q.store_thm( 2620"nomunify_mgu", 2621`nwfs s ��� FINITE fe ��� (nomunify (s,fe) t1 t2 = SOME (sx,fex)) ��� 2622 nwfs s2 ��� equiv fe2 (nwalk* s2 (nwalk* s t1)) (nwalk* s2 (nwalk* s t2)) ��� 2623 (���a v. (a,v) ��� fex ��� 2624 (���b w fcs. (b,w) ��� fe ��� (term_fcs b (nwalk* sx (Sus [] w)) = SOME fcs) ��� (a,v) ��� fcs) ��� 2625 fresh fe2 a (nwalk* s2 (Sus [] v))) ��� 2626 (���t. equiv fe2 (nwalk* s2 (nwalk* sx t)) (nwalk* s2 (nwalk* s t)))`, 2627REPEAT STRIP_TAC THEN1 2628(MATCH_MP_TAC nomunify_mgu1 THEN 2629 METIS_TAC []) THEN 2630METIS_TAC [nomunify_mgu2]) 2631 2632val equiv_consistent_exists = Q.store_thm( 2633"equiv_consistent_exists", 2634`equiv fe (nwalk* s t1) (nwalk* s t2) ��� nwfs s ��� ���fec. 2635 FINITE fec ��� 2636 (verify_fcs fec s = SOME fec) ��� 2637 equiv fec (nwalk* s t1) (nwalk* s t2)`, 2638Q_TAC SUFF_TAC 2639`���fe w1 w2. equiv fe w1 w2 ��� 2640���t1 t2 s. FINITE fe ��� nwfs s ��� (nwalk* s t1 = w1) ��� (nwalk* s t2 = w2) ��� 2641 ���fec. FINITE fec ��� verify_fcs fec s ��� NONE ��� equiv fec w1 w2` 2642THEN1 ( 2643 SRW_TAC [][] THEN 2644 IMP_RES_TAC equiv_FINITE THEN 2645 FIRST_X_ASSUM (Q.SPECL_THEN [`fcs`,`nwalk* s t1`,`nwalk* s t2`] MP_TAC) THEN 2646 SRW_TAC [][] THEN 2647 FIRST_X_ASSUM (Q.SPECL_THEN [`t1`,`t2`,`s`] MP_TAC) THEN 2648 SRW_TAC [][] THEN 2649 Cases_on `verify_fcs fec s` THEN FULL_SIMP_TAC (srw_ss()) [] THEN 2650 Q.EXISTS_TAC `x` THEN SRW_TAC [][] THEN1 2651 METIS_TAC [verify_fcs_FINITE] THEN1 2652 METIS_TAC [verify_fcs_idem] THEN 2653 METIS_TAC [equiv_verify_fcs,nwalkstar_idempotent]) THEN 2654STRIP_TAC THEN HO_MATCH_MP_TAC equiv_ind THEN 2655SRW_TAC [][] THEN1 ( 2656 Q.EXISTS_TAC `{}` THEN SRW_TAC [][] ) 2657THEN1 ( 2658 Q.EXISTS_TAC `IMAGE (��a. (a,v)) (dis_set p1 p2)` THEN SRW_TAC [][] THEN1 ( 2659 SPOSE_NOT_THEN STRIP_ASSUME_TAC THEN 2660 IMP_RES_TAC verify_fcs_NONE THEN 2661 FULL_SIMP_TAC (srw_ss()) [] THEN 2662 `v ��� FDOM s` by METIS_TAC [nwalkstar_to_var] THEN 2663 Q.PAT_X_ASSUM `nwfs s` ASSUME_TAC THEN 2664 FULL_SIMP_TAC (psrw_ss()) [NOT_FDOM_nvwalk,Once term_fcs_def] ) THEN 2665 SRW_TAC [][Once equiv_cases] THEN 2666 METIS_TAC [permeq_refl] ) 2667THEN1 ( 2668 IMP_RES_TAC nwalkstar_subterm_exists THEN 2669 SRW_TAC [][] THEN 2670 Q.MATCH_ASSUM_RENAME_TAC `nwalk* s t1 = Tie a (nwalk* s c1)` THEN 2671 Q.MATCH_ASSUM_RENAME_TAC `nwalk* s t2 = Tie a (nwalk* s c2)` THEN 2672 NTAC 2 (POP_ASSUM (K ALL_TAC)) THEN 2673 FIRST_X_ASSUM (Q.SPECL_THEN [`c1`,`c2`,`s`] MP_TAC) THEN 2674 SRW_TAC [][] THEN 2675 SRW_TAC [][Once equiv_cases] THEN 2676 METIS_TAC [] ) 2677THEN1 ( 2678 IMP_RES_TAC nwalkstar_subterm_exists THEN 2679 SRW_TAC [][] THEN 2680 NTAC 2 (POP_ASSUM (K ALL_TAC)) THEN 2681 Q.MATCH_ASSUM_RENAME_TAC `nwalk* s t1 = Tie a1 (nwalk* s c1)` THEN 2682 Q.MATCH_ASSUM_RENAME_TAC `nwalk* s t2' = Tie a2 (nwalk* s c2)` THEN 2683 FIRST_X_ASSUM (Q.SPECL_THEN [`c1`,`apply_pi [(a1,a2)] c2`,`s`] MP_TAC) THEN 2684 SRW_TAC [][nwalkstar_apply_pi] THEN 2685 SRW_TAC [][Once equiv_cases] THEN 2686 IMP_RES_TAC fresh_FINITE THEN 2687 IMP_RES_TAC fresh_term_fcs THEN 2688 IMP_RES_TAC term_fcs_FINITE THEN 2689 Cases_on `verify_fcs fec s` THEN FULL_SIMP_TAC (srw_ss()) [] THEN 2690 SRW_TAC [][] THEN 2691 `verify_fcs (fcs' ��� fec) s = SOME (fcs' ��� x)` by ( 2692 MATCH_MP_TAC verify_fcs_UNION_I THEN 2693 SRW_TAC [][] THEN 2694 MATCH_MP_TAC (GEN_ALL verify_fcs_term_fcs) THEN 2695 MAP_EVERY Q.EXISTS_TAC [`nwalk* s c2`,`a1`] THEN 2696 METIS_TAC [nwalkstar_idempotent] ) THEN 2697 Q.EXISTS_TAC `fcs' ��� fec` THEN SRW_TAC [][] THEN1 2698 METIS_TAC [term_fcs_fresh,fresh_extra_fcs,SUBSET_UNION] THEN 2699 METIS_TAC [equiv_SUBSET,SUBSET_UNION]) 2700THEN1 ( 2701 IMP_RES_TAC nwalkstar_subterm_exists THEN 2702 SRW_TAC [][] THEN 2703 POP_ASSUM (K ALL_TAC) THEN 2704 Q.MATCH_ASSUM_RENAME_TAC `nwalk* s t1 = nPair (nwalk* s t1a) (nwalk* s t1d)` THEN 2705 Q.MATCH_ASSUM_RENAME_TAC `nwalk* s t2 = nPair (nwalk* s t2a) (nwalk* s t2d)` THEN 2706 FIRST_X_ASSUM (Q.SPECL_THEN [`t1d`,`t2d`,`s`] MP_TAC) THEN 2707 FIRST_X_ASSUM (Q.SPECL_THEN [`t1a`,`t2a`,`s`] MP_TAC) THEN 2708 SRW_TAC [][] THEN 2709 SRW_TAC [][Once equiv_cases] THEN 2710 Cases_on `verify_fcs fec s` THEN 2711 Cases_on `verify_fcs fec' s` THEN 2712 FULL_SIMP_TAC (srw_ss()) [] THEN 2713 `verify_fcs (fec ��� fec') s = SOME (x ��� x')` by ( 2714 MATCH_MP_TAC verify_fcs_UNION_I THEN 2715 SRW_TAC [][] ) THEN 2716 Q.EXISTS_TAC `fec ��� fec'` THEN SRW_TAC [][] THEN 2717 METIS_TAC [equiv_SUBSET,SUBSET_UNION] ) THEN 2718Q.EXISTS_TAC `{}` THEN SRW_TAC [][]) 2719 2720val unify_eq_vars_verify_fcs = Q.store_thm( 2721"unify_eq_vars_verify_fcs", 2722`(verify_fcs fe s = SOME ve) ��� nwfs s ��� FINITE ds ��� FINITE fe ��� 2723 (unify_eq_vars ds v (s,fe) = SOME (s',fe')) ��� 2724 (���ve'. verify_fcs fe' s' = SOME ve')`, 2725SRW_TAC [][] THEN 2726Cases_on `verify_fcs fe' s'` THEN SRW_TAC [][] THEN 2727IMP_RES_TAC unify_eq_vars_FINITE THEN 2728IMP_RES_TAC unify_eq_vars_preserves_s THEN 2729IMP_RES_TAC verify_fcs_NONE THEN 2730Cases_on `(a,v') ��� fe` THEN1 ( 2731 IMP_RES_TAC verify_fcs_covers_all THEN 2732 SRW_TAC [][] THEN 2733 FULL_SIMP_TAC (srw_ss()) [] ) THEN 2734`��� b fcs. (term_fcs b (nwalk* s (Sus [] v)) = SOME fcs) ��� (a,v') ��� fcs` 2735by METIS_TAC [unify_eq_vars_minimal] THEN 2736SRW_TAC [][] THEN 2737IMP_RES_TAC term_fcs_NOTIN_FDOM THEN 2738Q.PAT_X_ASSUM `nwfs s` ASSUME_TAC THEN 2739FULL_SIMP_TAC (psrw_ss()) [NOT_FDOM_nvwalk,Once term_fcs_def]) 2740 2741val nwalk_nwalkstar = Q.store_thm( 2742"nwalk_nwalkstar", 2743`nwfs s ��� ���t. nwalk s (nwalk* s t) = nwalk* s t`, 2744STRIP_TAC THEN HO_MATCH_MP_TAC nwalkstar_ind THEN 2745STRIP_TAC THEN 2746`nwalk* s t = nwalk* s (nwalk s t)` by METIS_TAC [nwalkstar_nwalk] THEN 2747Cases_on `nwalk s t` THEN FULL_SIMP_TAC (srw_ss()) [] THEN 2748`n ��� FDOM s` by METIS_TAC [nwalk_to_var] THEN 2749ASM_SIMP_TAC (psrw_ss()) [NOT_FDOM_nvwalk]) 2750 2751val nomunify_eqs = Q.store_thm( 2752"nomunify_eqs", 2753`���s fe t1 t2 q1 q2 t ve. 2754 (nwalk s t1 = apply_pi q1 t) ��� 2755 (nwalk s t2 = apply_pi q2 t) ��� nwfs s ��� 2756 (���a. a ��� dis_set q1 q2 ��� term_fcs a (nwalk* s t) ��� NONE) ��� 2757 (verify_fcs fe s = SOME ve) ��� FINITE fe 2758 ��� 2759 ���fex. nomunify (s,fe) t1 t2 = SOME (s,fex)`, 2760HO_MATCH_MP_TAC nunify_ind THEN 2761SRW_TAC [][nomunify_def,EXISTS_PROD] THEN 2762Q.PAT_X_ASSUM `nwfs s` MP_TAC THEN 2763SIMP_TAC (psrw_ss()) [Once nunify_def,LET_THM] THEN 2764Cases_on `t` THEN ASM_SIMP_TAC (psrw_ss()) [] THEN1 ( 2765 SRW_TAC [][] THEN 2766 FULL_SIMP_TAC (srw_ss()) [dis_set_def] THEN 2767 FULL_SIMP_TAC (srw_ss()) [Once term_fcs_def] ) 2768THEN1 ( 2769 SRW_TAC [][] THEN 2770 Q.ABBREV_TAC `ds = dis_set (q1 ++ l) (q2 ++ l)` THEN 2771 REVERSE (Cases_on `unify_eq_vars ds n (s,fe)`) THEN1 ( 2772 Cases_on `x` THEN 2773 IMP_RES_TAC unify_eq_vars_preserves_s THEN 2774 SRW_TAC [][] THEN 2775 MATCH_MP_TAC (GEN_ALL unify_eq_vars_verify_fcs) THEN 2776 FULL_SIMP_TAC (srw_ss()) [] THEN 2777 METIS_TAC [FINITE_dis_set] ) THEN 2778 IMP_RES_TAC unify_eq_vars_NONE THEN 2779 FULL_SIMP_TAC (psrw_ss()) [Abbr`ds`] THEN 2780 `n ��� FDOM s` by METIS_TAC [nwalk_to_var] THEN 2781 Q.PAT_X_ASSUM `nwfs s` ASSUME_TAC THEN 2782 FULL_SIMP_TAC (psrw_ss()) [NOT_FDOM_nvwalk,fresh_def] THEN 2783 METIS_TAC [IN_SING] ) 2784THEN1 ( 2785 SRW_TAC [][] THEN FULL_SIMP_TAC (srw_ss()) [] THEN1 ( 2786 FIRST_X_ASSUM MATCH_MP_TAC THEN 2787 ASM_SIMP_TAC (srw_ss()) [nwalk_apply_pi] THEN 2788 Q.MATCH_ASSUM_RENAME_TAC `nwalk s t1 = Tie _ (apply_pi _ t)` THEN 2789 MAP_EVERY Q.EXISTS_TAC [`q1`,`q2`,`nwalk s t`] THEN 2790 SRW_TAC [][] THEN 2791 Q.PAT_X_ASSUM `!X.Y` MP_TAC THEN 2792 SRW_TAC [][Once term_fcs_def] THEN 2793 POP_ASSUM (Q.SPEC_THEN `a` MP_TAC) THEN 2794 FULL_SIMP_TAC (srw_ss()) [dis_set_def] THEN 2795 SRW_TAC [][] THEN FULL_SIMP_TAC (srw_ss()) [] THEN 2796 SRW_TAC [][nwalkstar_nwalk] ) THEN 2797 Q.MATCH_ASSUM_RENAME_TAC `nwalk s t1 = Tie (lswapstr q1 a) (apply_pi q1 t)` THEN 2798 `lswapstr (REVERSE q2) (lswapstr q1 a) ��� dis_set q1 q2` by ( 2799 ASM_SIMP_TAC (srw_ss()) [dis_set_def] THEN 2800 FULL_SIMP_TAC (srw_ss())[pmact_eql] ) THEN 2801 Q.PAT_X_ASSUM `!X.Y` MP_TAC THEN 2802 SRW_TAC [][Once term_fcs_def] THEN 2803 `lswapstr (REVERSE q2) (lswapstr q1 a) ��� a` by ( 2804 SPOSE_NOT_THEN STRIP_ASSUME_TAC THEN 2805 METIS_TAC [pmact_inverse] ) THEN 2806 `���fcs. term_fcs (lswapstr q1 a) (apply_pi q2 (nwalk* s t)) = SOME fcs` by ( 2807 FIRST_X_ASSUM (Q.SPEC_THEN `lswapstr (REVERSE q2) (lswapstr q1 a)` MP_TAC) THEN 2808 SRW_TAC [][] THEN 2809 Cases_on `term_fcs (lswapstr (REVERSE q2) (lswapstr q1 a)) (nwalk* s t)` THEN 2810 FULL_SIMP_TAC (srw_ss()) [] THEN 2811 (term_fcs_apply_pi |> 2812 Q.INST [`a`|->`lswapstr (REVERSE q2) (lswapstr q1 a)`,`t`|->`nwalk* s t`, 2813 `pi`|->`q2`,`fcs`|->`x`] |> MP_TAC) THEN 2814 SRW_TAC [][] ) THEN 2815 FULL_SIMP_TAC (srw_ss()) [nwalkstar_apply_pi] THEN 2816 FIRST_X_ASSUM MATCH_MP_TAC THEN 2817 ASM_SIMP_TAC (srw_ss()) [nwalk_apply_pi] THEN 2818 ASM_SIMP_TAC (srw_ss()) [GSYM apply_pi_decompose] THEN 2819 MAP_EVERY Q.EXISTS_TAC [`q1`,`(lswapstr q1 a, lswapstr q2 a)::q2`,`nwalk s t`] THEN 2820 SRW_TAC [][] THEN 2821 `verify_fcs fcs s = SOME fcs` by ( 2822 MATCH_MP_TAC (GEN_ALL verify_fcs_term_fcs) THEN 2823 MAP_EVERY Q.EXISTS_TAC [`nwalk* s (apply_pi q2 t)`,`lswapstr q1 a`] THEN 2824 SRW_TAC [][nwalkstar_apply_pi] THEN 2825 METIS_TAC [nwalkstar_idempotent] ) THEN 2826 Q.EXISTS_TAC `ve ��� fcs` THEN 2827 IMP_RES_TAC term_fcs_FINITE THEN 2828 SRW_TAC [][] THEN1 ( 2829 FULL_SIMP_TAC (srw_ss()) [dis_set_def] THEN 2830 ASM_SIMP_TAC (srw_ss()) [nwalkstar_nwalk] THEN 2831 Cases_on `a = a'` THEN FULL_SIMP_TAC (srw_ss()) [] THEN 2832 Cases_on `lswapstr q1 a' = lswapstr q2 a'` THEN FULL_SIMP_TAC (srw_ss()) [] THEN1 ( 2833 Cases_on `lswapstr q2 a' = lswapstr q2 a` THEN 2834 FULL_SIMP_TAC (srw_ss()) [] THEN 2835 Cases_on `lswapstr q2 a' = lswapstr q1 a` THEN 2836 FULL_SIMP_TAC (srw_ss()) [] ) THEN 2837 FIRST_X_ASSUM (Q.SPEC_THEN `a'` MP_TAC) THEN 2838 SRW_TAC [][] ) THEN 2839 MATCH_MP_TAC verify_fcs_UNION_I THEN 2840 SRW_TAC [][] ) 2841THEN1 ( 2842 SRW_TAC [][EXISTS_PROD] THEN FULL_SIMP_TAC (srw_ss()) [] THEN 2843 FULL_SIMP_TAC (srw_ss()) [nwalk_apply_pi] THEN 2844 Q.MATCH_ASSUM_RENAME_TAC `nwalk s t1 = nPair (apply_pi q1 ta) (apply_pi q1 td)` THEN 2845 FIRST_X_ASSUM (Q.SPECL_THEN [`q1`,`q2`,`nwalk s ta`] MP_TAC) THEN 2846 SRW_TAC [][] THEN 2847 Q.PAT_X_ASSUM `!X.Y` MP_TAC THEN 2848 SRW_TAC [][Once term_fcs_def] THEN 2849 Q.PAT_X_ASSUM `nwfs s` ASSUME_TAC THEN 2850 FULL_SIMP_TAC (srw_ss()) [nwalkstar_nwalk] THEN 2851 Q.MATCH_ASSUM_RENAME_TAC `nunify (s,fe) _ _ = SOME (s,fu)` THEN 2852 FIRST_X_ASSUM (Q.SPECL_THEN [`s`,`fu`] MP_TAC) THEN 2853 SRW_TAC [][] THEN 2854 FIRST_X_ASSUM MATCH_MP_TAC THEN 2855 ASM_SIMP_TAC (srw_ss()) [nwalk_apply_pi] THEN 2856 IMP_RES_TAC nunify_FINITE_fe THEN 2857 MAP_EVERY Q.EXISTS_TAC [`q1`,`q2`,`nwalk s td`] THEN 2858 SRW_TAC [][] THEN 2859 METIS_TAC [nwalkstar_nwalk] ) ) 2860 2861val nvars_measure = Q.store_thm( 2862"nvars_measure", 2863`v ��� nvars t ��� �� is_Sus t ��� nwfs s ��� 2864 measure (npair_count o (nwalk* s)) (Sus [] v) t`, 2865Induct_on `t` THEN SRW_TAC [][] THEN 2866Q.MATCH_ASSUM_RENAME_TAC `v ��� nvars tt` THEN 2867Cases_on `tt` THEN FULL_SIMP_TAC (srw_ss()) [] THEN 2868FULL_SIMP_TAC (srw_ss()++ARITH_ss) [measure_thm] THEN 2869(npair_count_nwalkstar_ignores_pi |> 2870 UNDISCH |> 2871 Q.SPECL [`Sus [] n`,`l`] |> 2872 MP_TAC) THEN 2873ASM_SIMP_TAC (psrw_ss()++ARITH_ss) []) 2874 2875val npair_count_apply_pi = RWstore_thm( 2876"npair_count_apply_pi", 2877`npair_count (apply_pi pi t) = npair_count t`, 2878Induct_on `t` THEN SRW_TAC [][]) 2879 2880val equiv_depth_eq = Q.store_thm( 2881"equiv_depth_eq", 2882`���t1 t2. equiv fe t1 t2 ��� (npair_count t1 = npair_count t2)`, 2883HO_MATCH_MP_TAC equiv_ind THEN SRW_TAC [][]) 2884 2885val noc_subterm_nequiv = Q.store_thm( 2886"noc_subterm_nequiv", 2887`noc s t v ��� �� is_Sus t ��� nwfs s ��� nwfs s2 ��� 2888�� equiv fe (nwalk* s2 (Sus pi v)) (nwalk* s2 (nwalk* s t))`, 2889STRIP_TAC THEN 2890`v ��� nvars (nwalk* s t)` by METIS_TAC [noc_eq_nvars_nwalkstar] THEN 2891`~is_Sus (nwalk* s t)` by (Cases_on `t` THEN FULL_SIMP_TAC (srw_ss()) []) THEN 2892IMP_RES_TAC nvars_measure THEN 2893SPOSE_NOT_THEN STRIP_ASSUME_TAC THEN 2894IMP_RES_TAC noc_NOTIN_FDOM THEN 2895Q.PAT_X_ASSUM `nwfs s` ASSUME_TAC THEN 2896FULL_SIMP_TAC (psrw_ss()) [measure_thm,NOT_FDOM_nvwalk] THEN 2897`npair_count (nwalk* s2 (apply_pi pi (Sus [] v))) < npair_count (nwalk* s2 (nwalk* s t))` 2898by (Q.PAT_X_ASSUM `nwfs s2` ASSUME_TAC THEN FULL_SIMP_TAC (psrw_ss()) [nwalkstar_apply_pi]) THEN 2899FULL_SIMP_TAC (psrw_ss()) [] THEN 2900METIS_TAC [equiv_depth_eq,LESS_NOT_EQ]) 2901 2902val nwalk_to_var_NOT_FDOM = Q.prove( 2903`nwfs s ��� (nwalk s t = Sus p v) ��� v ��� FDOM s`, 2904METIS_TAC [nwalk_to_var]) 2905 2906val term_fcs_equiv_NONE = Q.store_thm( 2907"term_fcs_equiv_NONE", 2908`(term_fcs a t1 = NONE) ��� equiv fe t1 t2 ��� (term_fcs a t2 = SOME fcs) ��� �� (fcs ��� fe)`, 2909SRW_TAC [][] THEN 2910IMP_RES_TAC term_fcs_NONE THEN 2911IMP_RES_TAC term_fcs_fresh THEN 2912IMP_RES_TAC equiv_sym THEN 2913IMP_RES_TAC equiv_fresh THEN 2914SPOSE_NOT_THEN STRIP_ASSUME_TAC THEN 2915`fresh fe a t2` by METIS_TAC [fresh_extra_fcs] THEN 2916RES_TAC THEN RES_TAC) 2917 2918val term_fcs_apply_pi_NONE = Q.store_thm( 2919"term_fcs_apply_pi_NONE", 2920`(term_fcs a t = NONE) ��� (term_fcs (lswapstr pi a) (apply_pi pi t) = NONE)`, 2921Cases_on `term_fcs a t` THEN 2922Cases_on `term_fcs (lswapstr pi a) (apply_pi pi t)` THEN 2923SRW_TAC [][] THEN1 ( 2924 (term_fcs_apply_pi |> 2925 Q.INST [`a`|->`lswapstr pi a`,`t`|->`apply_pi pi t`,`pi`|->`REVERSE pi`,`fcs`|->`x`] |> 2926 MP_TAC) THEN 2927 SRW_TAC [][] ) THEN 2928(term_fcs_apply_pi |> 2929 Q.INST [`fcs`|->`x`] |> 2930 MP_TAC) THEN 2931SRW_TAC [][]) 2932 2933val term_fcs_nwalkstar_NONE = Q.store_thm( 2934"term_fcs_nwalkstar_NONE", 2935`nwfs s ��� (term_fcs a t = SOME fcs) ��� 2936 (term_fcs a (nwalk* s t) = NONE) ��� 2937 (verify_fcs fcs s = NONE)`, 2938STRIP_TAC THEN 2939NTAC 2 (POP_ASSUM MP_TAC) THEN 2940MAP_EVERY Q.ID_SPEC_TAC [`fcs`,`t`] THEN 2941HO_MATCH_MP_TAC nwalkstar_ind THEN 2942SRW_TAC [][] THEN 2943Q.PAT_X_ASSUM `nwfs s` ASSUME_TAC THEN 2944`nwalk* s t = nwalk* s (nwalk s t)` by METIS_TAC [nwalkstar_nwalk] THEN 2945Cases_on `nwalk s t` THEN FULL_SIMP_TAC (srw_ss()) [] THEN1 ( 2946 Q.PAT_X_ASSUM `X = NONE` MP_TAC THEN 2947 SRW_TAC [][Once term_fcs_def] THEN 2948 Q.PAT_X_ASSUM `nwfs s` ASSUME_TAC THEN 2949 Cases_on `t` THEN FULL_SIMP_TAC (psrw_ss()) [Once term_fcs_def] THEN 2950 SRW_TAC [][verify_fcs_def,fcs_acc_RECURSES] THEN 2951 SRW_TAC [][fcs_acc_def,ITSET_EMPTY] THEN 2952 (nvwalk_modulo_pi |> Q.SPECL [`s`,`l`,`n`] |> GSYM |> MP_TAC) THEN 2953 SRW_TAC [][apply_pi_eql,Once term_fcs_def] ) 2954THEN1 ( 2955 Q.PAT_X_ASSUM `nwfs s` ASSUME_TAC THEN 2956 Cases_on `t` THEN FULL_SIMP_TAC (psrw_ss()) [] THEN 2957 `n ��� FDOM s` by METIS_TAC [nvwalk_to_var] THEN 2958 FULL_SIMP_TAC (psrw_ss()) [NOT_FDOM_nvwalk] THEN 2959 FULL_SIMP_TAC (srw_ss()) [Once term_fcs_def] ) 2960THEN1 ( 2961 Q.PAT_X_ASSUM `X = NONE` MP_TAC THEN 2962 SRW_TAC [][Once term_fcs_def] THEN 2963 Q.PAT_X_ASSUM `nwfs s` ASSUME_TAC THEN 2964 Cases_on `t` THEN FULL_SIMP_TAC (srw_ss()) [] THEN 2965 Q.PAT_X_ASSUM `X = SOME fcs` MP_TAC THEN 2966 ASM_SIMP_TAC (psrw_ss()) [Once term_fcs_def] THEN 2967 SRW_TAC [][] THEN 2968 SRW_TAC [][verify_fcs_def,fcs_acc_RECURSES] THEN 2969 SRW_TAC [][fcs_acc_def,ITSET_EMPTY] THEN 2970 (nvwalk_modulo_pi |> Q.SPECL [`s`,`l`,`n`] |> GSYM |> MP_TAC) THEN 2971 SRW_TAC [][apply_pi_eql,Once term_fcs_def,nwalkstar_apply_pi] THEN 2972 METIS_TAC [term_fcs_apply_pi_NONE] ) 2973THEN1 ( 2974 Q.PAT_X_ASSUM `nwfs s` ASSUME_TAC THEN 2975 Cases_on `t` THEN FULL_SIMP_TAC (srw_ss()) [] THEN1 ( 2976 Q.PAT_X_ASSUM `X = SOME fcs` MP_TAC THEN 2977 ASM_SIMP_TAC (psrw_ss()) [Once term_fcs_def] THEN 2978 SRW_TAC [][] THEN 2979 SRW_TAC [][verify_fcs_def,fcs_acc_RECURSES] THEN 2980 SRW_TAC [][fcs_acc_def,ITSET_EMPTY] THEN 2981 (nvwalk_modulo_pi |> Q.SPECL [`s`,`l`,`n`] |> GSYM |> MP_TAC) THEN 2982 SRW_TAC [][apply_pi_eql,Once term_fcs_def,nwalkstar_apply_pi] THEN 2983 Q.PAT_X_ASSUM `X = NONE` MP_TAC THEN 2984 SRW_TAC [][Once term_fcs_def] THEN 2985 METIS_TAC [term_fcs_apply_pi_NONE] ) THEN 2986 SRW_TAC [][] THEN 2987 Q.PAT_X_ASSUM `X = SOME fcs` MP_TAC THEN 2988 ASM_SIMP_TAC (psrw_ss()) [Once term_fcs_def] THEN 2989 Q.PAT_X_ASSUM `X = NONE` MP_TAC THEN 2990 SRW_TAC [][Once term_fcs_def] THEN 2991 Cases_on `verify_fcs (x1 ��� x2) s` THEN SRW_TAC [][] THEN 2992 RES_TAC THEN 2993 METIS_TAC [verify_fcs_UNION,term_fcs_FINITE,optionTheory.NOT_SOME_NONE] ) THEN 2994FULL_SIMP_TAC (srw_ss()) [term_fcs_def]) 2995 2996val verify_fcs_iter_SUBMAP_exists = Q.store_thm( 2997"verify_fcs_iter_SUBMAP_exists", 2998`(verify_fcs fe s = SOME ve) ��� nwfs sx ��� s SUBMAP sx ��� FINITE fe ��� 2999 (verify_fcs ve sx = SOME vex) ��� 3000 (���fex. verify_fcs fe sx = SOME fex)`, 3001STRIP_TAC THEN Cases_on `verify_fcs fe sx` THEN SRW_TAC [][] THEN 3002`���a v. (a,v) ��� fe ��� (term_fcs a (nwalk* sx (Sus [] v)) = NONE)` 3003by METIS_TAC [verify_fcs_NONE] THEN 3004`���fcs. (term_fcs a (nwalk* s (Sus [] v)) = SOME fcs) ��� fcs ��� ve` 3005by METIS_TAC [verify_fcs_covers_all] THEN 3006`nwalk* sx (Sus [] v) = nwalk* sx (nwalk* s (Sus [] v))` 3007by METIS_TAC [nwalkstar_SUBMAP] THEN 3008FULL_SIMP_TAC (srw_ss()) [] THEN 3009IMP_RES_TAC term_fcs_nwalkstar_NONE THEN 3010IMP_RES_TAC verify_fcs_FINITE THEN 3011IMP_RES_TAC verify_fcs_SUBSET THEN 3012FULL_SIMP_TAC (srw_ss()) []) 3013 3014val equiv_nomunify = Q.store_thm( 3015"equiv_nomunify", 3016`equiv fe2 (nwalk* s2 (nwalk* s t1)) (nwalk* s2 (nwalk* s t2)) ��� nwfs s2 ��� nwfs s ��� 3017 ���sx.���fe. FINITE fe ��� (verify_fcs fe sx ��� NONE) ��� 3018 ���fex. (nomunify (s,fe) t1 t2 = SOME (sx,fex))`, 3019Q_TAC SUFF_TAC 3020`���fe2 s fe t1 t2 ve2. equiv fe2 (nwalk* s2 (nwalk* s t1)) (nwalk* s2 (nwalk* s t2)) 3021 ��� nwfs s2 ��� nwfs s ��� FINITE (fe:fe) ��� FINITE fe2 ��� (verify_fcs fe2 s2 = SOME ve2) ��� 3022 ���sx fu fv. (nunify (s,{}) t1 t2 = SOME (sx,fu)) ��� (verify_fcs fu sx = SOME fv)` THEN1 ( 3023 SRW_TAC [][] THEN 3024 `���fcs. FINITE fcs ��� (verify_fcs fcs s2 = SOME fcs) ��� equiv fcs (nwalk* s2 (nwalk* s t1)) (nwalk* s2 (nwalk* s t2))` 3025 by METIS_TAC [equiv_consistent_exists] THEN 3026 FIRST_X_ASSUM (Q.SPECL_THEN [`fcs`,`s`,`{}`,`t1`,`t2`,`fcs`] MP_TAC) THEN 3027 SRW_TAC [][] THEN 3028 FULL_SIMP_TAC (srw_ss()) [nomunify_def,EXISTS_PROD] THEN 3029 Q.EXISTS_TAC `sx` THEN SRW_TAC [][] THEN 3030 `���f2. nunify (s,fe) t1 t2 = SOME (sx,f2)` 3031 by METIS_TAC [nunify_ignores_fe] THEN 3032 SRW_TAC [][] THEN 3033 `���ff.���fe fex. (nunify (s,fe) t1 t2 = SOME (sx,fex)) ��� (fex = fe ��� ff)` 3034 by METIS_TAC [nunify_adds_same_fcs] THEN 3035 RES_TAC THEN SRW_TAC [][] THEN 3036 Cases_on `verify_fcs fe sx` THEN FULL_SIMP_TAC (srw_ss()) [] THEN 3037 Q.EXISTS_TAC `x ��� fv` THEN 3038 MATCH_MP_TAC verify_fcs_UNION_I THEN 3039 IMP_RES_TAC nunify_FINITE_fe THEN 3040 FULL_SIMP_TAC (srw_ss()) []) THEN 3041STRIP_TAC THEN HO_MATCH_MP_TAC nunify_ind THEN 3042SRW_TAC [][nomunify_def,EXISTS_PROD] THEN 3043`(nwalk* s t1 = nwalk* s (nwalk s t1)) ��� 3044 (nwalk* s t2 = nwalk* s (nwalk s t2))` 3045by METIS_TAC [nwalkstar_nwalk] THEN 3046MAP_EVERY Cases_on [`nwalk s t1`,`nwalk s t2`] THEN 3047NTAC 2 (POP_ASSUM MP_TAC) THEN 3048Q.PAT_X_ASSUM `nwfs s` MP_TAC THEN 3049SIMP_TAC (psrw_ss()) [Once nunify_def,LET_THM] THEN 3050REPEAT STRIP_TAC THEN 3051IMP_RES_TAC nwalk_to_var_NOT_FDOM THEN 3052Q.PAT_X_ASSUM `nwfs s` ASSUME_TAC THEN 3053Q.PAT_X_ASSUM `nwfs s2` ASSUME_TAC THEN 3054FULL_SIMP_TAC (psrw_ss()) [NOT_FDOM_nvwalk] THEN 3055TRY ( FULL_SIMP_TAC (srw_ss()) [Once equiv_cases] THEN NO_TAC) 3056THEN1 ( 3057 Cases_on `n = n'` THEN SRW_TAC [][] THEN 3058 Q.EXISTS_TAC `s` THEN 3059 Q.ABBREV_TAC `ds = dis_set l l'` THEN 3060 Cases_on `unify_eq_vars ds n (s,fe)` THEN1 ( 3061 IMP_RES_TAC unify_eq_vars_NONE THEN 3062 FULL_SIMP_TAC (srw_ss()) [Abbr`ds`] THEN 3063 POP_ASSUM (Q.SPEC_THEN `{(a,n)}` MP_TAC) THEN 3064 ASM_SIMP_TAC (psrw_ss()) [NOT_FDOM_nvwalk,fresh_def] ) THEN 3065 Cases_on `x` THEN IMP_RES_TAC unify_eq_vars_preserves_s THEN 3066 SRW_TAC [][] THEN 3067 IMP_RES_TAC unify_eq_vars_ignores_fe THEN 3068 FULL_SIMP_TAC (srw_ss()) [Abbr`ds`] THEN 3069 POP_ASSUM (Q.SPEC_THEN `{}` STRIP_ASSUME_TAC) THEN 3070 SRW_TAC [][] THEN 3071 MATCH_MP_TAC (GEN_ALL unify_eq_vars_verify_fcs) THEN 3072 METIS_TAC [FINITE_dis_set,FINITE_EMPTY,verify_fcs_empty]) 3073THEN1 ( 3074 Q.MATCH_ASSUM_RENAME_TAC `nwalk s _ = Tie a t` THEN 3075 (noc_subterm_nequiv |> CONTRAPOS |> 3076 Q.INST [`v`|->`n`,`t`|->`Tie a t`,`pi`|->`l`,`fe`|->`fe2`] |> 3077 MP_TAC) THEN 3078 FULL_SIMP_TAC (srw_ss()) [noc_ignores_pi]) 3079THEN1 ( 3080 Q.MATCH_ASSUM_RENAME_TAC `nwalk s _ = nPair c1 c2` THEN 3081 (noc_subterm_nequiv |> CONTRAPOS |> 3082 Q.INST [`v`|->`n`,`t`|->`nPair c1 c2`,`pi`|->`l`,`fe`|->`fe2`] |> 3083 MP_TAC) THEN 3084 FULL_SIMP_TAC (srw_ss()) [noc_ignores_pi]) 3085THEN1 ( 3086 Q.MATCH_ASSUM_RENAME_TAC `nwalk s _ = nPair c1 c2` THEN 3087 (noc_subterm_nequiv |> CONTRAPOS |> 3088 Q.INST [`v`|->`n`,`t`|->`nPair c1 c2`,`pi`|->`l`,`fe`|->`fe2`] |> 3089 MP_TAC) THEN 3090 FULL_SIMP_TAC (srw_ss()) [noc_ignores_pi]) 3091THEN1 ( 3092 Q.MATCH_ASSUM_RENAME_TAC `nwalk s _ = Tie a t` THEN 3093 (noc_subterm_nequiv |> CONTRAPOS |> 3094 Q.INST [`v`|->`n`,`t`|->`Tie a t`,`pi`|->`l`,`fe`|->`fe2`] |> 3095 MP_TAC) THEN 3096 FULL_SIMP_TAC (srw_ss()) [noc_ignores_pi,equiv_sym]) 3097THEN1 ( 3098 Q.MATCH_ASSUM_RENAME_TAC `nwalk s t1 = Tie a1 c1` THEN 3099 Q.MATCH_ASSUM_RENAME_TAC `nwalk s t2 = Tie a2 c2` THEN 3100 Cases_on `a1 = a2` THEN SRW_TAC [][] THEN1 ( 3101 POP_ASSUM MATCH_MP_TAC THEN 3102 FULL_SIMP_TAC (srw_ss()) [Once equiv_cases] ) THEN 3103 FULL_SIMP_TAC (srw_ss()) [] THEN 3104 Q.PAT_X_ASSUM `equiv fe2 X Y` MP_TAC THEN 3105 SRW_TAC [][Once equiv_cases] THEN 3106 IMP_RES_TAC fresh_term_fcs THEN 3107 `���fe0. term_fcs a1 (nwalk* s c2) = SOME fe0` 3108 by METIS_TAC [term_fcs_SUBMAP] THEN 3109 IMP_RES_TAC term_fcs_FINITE THEN 3110 FULL_SIMP_TAC (srw_ss()) [nwalkstar_apply_pi] THEN 3111 `���fe1. nunify (s,fe0) c1 (apply_pi [(a1,a2)] c2) = SOME (sx,fe1)` 3112 by METIS_TAC [nunify_ignores_fe] THEN 3113 `fe1 = fe0 ��� fu` by ( 3114 IMP_RES_TAC nunify_adds_same_fcs THEN 3115 POP_ASSUM (Q.SPECL_THEN [`apply_pi [(a1,a2)] c2`,`c1`] STRIP_ASSUME_TAC) THEN 3116 RES_TAC THEN FULL_SIMP_TAC (srw_ss()) [] ) THEN 3117 SRW_TAC [][] THEN 3118 Q_TAC SUFF_TAC `verify_fcs fe0 sx ��� NONE` THEN1 ( 3119 Cases_on `verify_fcs fe0 sx` THEN SRW_TAC [][] THEN 3120 Q.EXISTS_TAC `x ��� fv` THEN 3121 MATCH_MP_TAC verify_fcs_UNION_I THEN 3122 METIS_TAC [nunify_FINITE_fe,FINITE_EMPTY] ) THEN 3123 `���t. equiv fe2 (nwalk* s2 (nwalk* sx t)) (nwalk* s2 (nwalk* s t))` by ( 3124 MATCH_MP_TAC nomunify_mgu2 THEN 3125 MAP_EVERY Q.EXISTS_TAC [`{}`,`c1`,`apply_pi [(a1,a2)] c2`,`fv`] THEN 3126 SRW_TAC [][nomunify_def,EXISTS_PROD,nwalkstar_apply_pi] ) THEN 3127 `fresh fe2 a1 (nwalk* s2 (nwalk* sx c2))` 3128 by METIS_TAC [equiv_fresh,equiv_trans,equiv_sym] THEN 3129 `���fcs4. (term_fcs a1 (nwalk* s2 (nwalk* sx c2)) = SOME fcs4) ��� fcs4 ��� fe2` by 3130 METIS_TAC [fresh_term_fcs] THEN 3131 `s SUBMAP sx ��� nwfs sx` by METIS_TAC [nunify_uP,uP_def] THEN 3132 `���fcs3. (term_fcs a1 (nwalk* sx (nwalk* s c2)) = SOME fcs3)` by 3133 METIS_TAC [term_fcs_SUBMAP,nwalkstar_SUBMAP] THEN 3134 SPOSE_NOT_THEN STRIP_ASSUME_TAC THEN 3135 `���a v. (a,v) ��� fe0 ��� (term_fcs a (nwalk* sx (Sus [] v)) = NONE)` 3136 by METIS_TAC [verify_fcs_NONE] THEN 3137 METIS_TAC [term_fcs_nwalkstar,optionTheory.NOT_SOME_NONE] ) 3138THEN1 ( 3139 Q.MATCH_ASSUM_RENAME_TAC `nwalk s _ = nPair c1 c2` THEN 3140 (noc_subterm_nequiv |> CONTRAPOS |> 3141 Q.INST [`v`|->`n`,`t`|->`nPair c1 c2`,`pi`|->`l`,`fe`|->`fe2`] |> 3142 MP_TAC) THEN 3143 FULL_SIMP_TAC (srw_ss()) [noc_ignores_pi,equiv_sym]) 3144THEN1 ( 3145 Q.MATCH_ASSUM_RENAME_TAC `nwalk s _ = nPair c1 c2` THEN 3146 (noc_subterm_nequiv |> CONTRAPOS |> 3147 Q.INST [`v`|->`n`,`t`|->`nPair c1 c2`,`pi`|->`l`,`fe`|->`fe2`] |> 3148 MP_TAC) THEN 3149 FULL_SIMP_TAC (srw_ss()) [noc_ignores_pi,equiv_sym]) THEN 3150SRW_TAC [][EXISTS_PROD] THEN 3151Q.MATCH_ASSUM_RENAME_TAC `nwalk s t1 = nPair t1a t1d` THEN 3152Q.MATCH_ASSUM_RENAME_TAC `nwalk s t2 = nPair t2a t2d` THEN 3153Q.PAT_X_ASSUM `equiv fe2 X Y` MP_TAC THEN 3154SRW_TAC [][Once equiv_cases] THEN 3155FULL_SIMP_TAC (srw_ss()) [] THEN 3156`���fe1. nunify (s,fe) t1a t2a = SOME (sx,fe1)` 3157by METIS_TAC [nunify_ignores_fe] THEN 3158`fe1 = fe ��� fu` by ( 3159 IMP_RES_TAC nunify_adds_same_fcs THEN 3160 POP_ASSUM (Q.SPECL_THEN [`t2a`,`t1a`] STRIP_ASSUME_TAC) THEN 3161 RES_TAC THEN FULL_SIMP_TAC (srw_ss()) [] ) THEN 3162SRW_TAC [][] THEN 3163FULL_SIMP_TAC (srw_ss()) [] THEN 3164`���t. equiv fe2 (nwalk* s2 (nwalk* sx t)) (nwalk* s2 (nwalk* s t))` by ( 3165 MATCH_MP_TAC nomunify_mgu2 THEN 3166 MAP_EVERY Q.EXISTS_TAC [`{}`,`t1a`,`t2a`,`fv`] THEN 3167 SRW_TAC [][nomunify_def,EXISTS_PROD,nwalkstar_apply_pi] ) THEN 3168`equiv fe2 (nwalk* s2 (nwalk* sx t1d)) (nwalk* s2 (nwalk* sx t2d))` 3169by METIS_TAC [equiv_trans,equiv_sym] THEN 3170`nwfs sx ��� FINITE fu` by METIS_TAC [nunify_uP,uP_def,nunify_FINITE_fe,FINITE_EMPTY] THEN 3171FULL_SIMP_TAC (srw_ss()) [] THEN 3172Q.MATCH_ASSUM_RENAME_TAC `nunify (s,{}) t1a t2a = SOME (sa,fa)` THEN 3173Q.MATCH_ASSUM_RENAME_TAC `nunify (sa,{}) t1d t2d = SOME (sd,fd)` THEN 3174Q.MATCH_ASSUM_RENAME_TAC `verify_fcs fa sa = SOME faa` THEN 3175Q.MATCH_ASSUM_RENAME_TAC `verify_fcs fd sd = SOME fdd` THEN 3176`���fe1. nunify (sa,fa) t1d t2d = SOME (sd,fe1)` 3177by METIS_TAC [nunify_ignores_fe] THEN 3178`fe1 = fa ��� fd` by ( 3179 IMP_RES_TAC nunify_adds_same_fcs THEN 3180 REPEAT (FIRST_X_ASSUM (Q.SPECL_THEN [`t2d`,`t1d`] STRIP_ASSUME_TAC)) THEN 3181 RES_TAC THEN FULL_SIMP_TAC (srw_ss()) [] ) THEN 3182SRW_TAC [][] THEN 3183Q_TAC SUFF_TAC `verify_fcs fa sd ��� NONE` THEN1 ( 3184 Cases_on `verify_fcs fa sd` THEN SRW_TAC [][] THEN 3185 Q.EXISTS_TAC `x ��� fdd` THEN 3186 MATCH_MP_TAC verify_fcs_UNION_I THEN 3187 METIS_TAC [nunify_FINITE_fe,FINITE_EMPTY] ) THEN 3188Q_TAC SUFF_TAC `verify_fcs faa sd ��� NONE` THEN1 ( 3189 Cases_on `verify_fcs faa sd` THEN SRW_TAC [][] THEN 3190 `nwfs sd ��� sa SUBMAP sd ��� FINITE fa` by METIS_TAC [nunify_uP,uP_def,nunify_FINITE_fe,FINITE_EMPTY] THEN 3191 METIS_TAC [verify_fcs_iter_SUBMAP_exists,optionTheory.NOT_SOME_NONE] ) THEN 3192SPOSE_NOT_THEN STRIP_ASSUME_TAC THEN 3193`FINITE faa` by METIS_TAC [verify_fcs_FINITE] THEN 3194`���a v. (a,v) ��� faa ��� (term_fcs a (nwalk* sd (Sus [] v)) = NONE)` by 3195 METIS_TAC [verify_fcs_NONE] THEN 3196(nomunify_mgu1 |> 3197 Q.INST [`fe`|->`{}`,`t1`|->`t1a`,`t2`|->`t2a`,`sx`|->`sa`,`fex`|->`faa`] |> 3198 MP_TAC) THEN 3199SRW_TAC [][nomunify_def] THEN 3200SPOSE_NOT_THEN STRIP_ASSUME_TAC THEN 3201IMP_RES_TAC fresh_term_fcs THEN 3202`���t. equiv fe2 (nwalk* s2 (nwalk* sd t)) (nwalk* s2 (nwalk* sa t))` by ( 3203 MATCH_MP_TAC nomunify_mgu2 THEN 3204 MAP_EVERY Q.EXISTS_TAC [`{}`,`t1d`,`t2d`,`fdd`] THEN 3205 SRW_TAC [][nomunify_def,EXISTS_PROD,nwalkstar_apply_pi] ) THEN 3206`equiv fe2 (nwalk* s2 (nwalk* s (Sus [] v))) (nwalk* s2 (nwalk* sd (Sus [] v)))` 3207by METIS_TAC [equiv_trans,equiv_sym] THEN 3208(term_fcs_equiv |> 3209 Q.INST [`fe`|->`fe2`,`t1`|->`nwalk* s2 (nwalk* s (Sus [] v))`,`t2`|->`nwalk* s2 (nwalk* sd (Sus [] v))`, 3210 `fcs1`|->`fcs`] |> MP_TAC) THEN 3211`v ��� FDOM sa` by METIS_TAC [verify_fcs_NOTIN_FDOM] THEN 3212`s SUBMAP sa` by METIS_TAC [nunify_uP,uP_def] THEN 3213`v ��� FDOM s` by METIS_TAC [SUBMAP_DEF] THEN 3214ASM_SIMP_TAC (psrw_ss()) [NOT_FDOM_nvwalk] THEN 3215SRW_TAC [][] THEN 3216Cases_on `fcs2 ��� fe2` THEN SRW_TAC [][] THEN 3217SPOSE_NOT_THEN STRIP_ASSUME_TAC THEN 3218IMP_RES_TAC term_fcs_SUBMAP THEN 3219FULL_SIMP_TAC (srw_ss()) []) 3220 3221val _ = export_theory (); 3222