1open HolKernel boolLib bossLib Parse stringTheory arithmeticTheory 2 finite_mapTheory pred_setTheory bagTheory pairTheory relationTheory 3 prim_recTheory apply_piTheory ntermTheory nsubstTheory nwalkTheory 4 nwalkstarTheory nomsetTheory listTheory dis_setTheory ramanaLib 5 ntermLib 6 7val _ = new_theory "nunifDef" 8val _ = monadsyntax.temp_add_monadsyntax() 9val _ = monadsyntax.enable_monad "option"; 10val _ = metisTools.limit := { time = NONE, infs = SOME 5000 } 11 12Triviality nvR_update: 13 v NOTIN FDOM s /\ x <> v ==> (nvR (s |+ (v,t)) y x <=> nvR s y x) 14Proof 15 SRW_TAC [][nvR_def] THEN 16 Cases_on `x IN FDOM s` THEN 17 SRW_TAC [][FLOOKUP_DEF,FAPPLY_FUPDATE_THM] 18QED 19 20Triviality TC_nvR_update: 21 !y x. (nvR (s |+ (v,t)))^+ y x ==> v NOTIN FDOM s ==> 22 (nvR s)^+ y x \/ ?u. (nvR s)^* v x /\ u IN nvars t /\ (nvR s)^* y u 23Proof 24HO_MATCH_MP_TAC TC_STRONG_INDUCT THEN CONJ_TAC THENL [ 25 MAP_EVERY Q.X_GEN_TAC [`y`,`x`] THEN SRW_TAC [][] THEN 26 Cases_on `x = v` THENL [ 27 DISJ2_TAC THEN 28 FULL_SIMP_TAC (srw_ss()) [nvR_def,FLOOKUP_DEF] THEN 29 Q.EXISTS_TAC `y` THEN SRW_TAC [][], 30 METIS_TAC [nvR_update,TC_RULES] 31 ], 32 SRW_TAC [][] THEN FULL_SIMP_TAC (srw_ss()) [] 33 THEN1 METIS_TAC [TC_RULES] THEN 34 DISJ2_TAC THEN Q.EXISTS_TAC `u` THEN 35 METIS_TAC [TC_RTC,RTC_TRANSITIVE,transitive_def] 36] 37QED 38 39Theorem nwfs_extend: 40 nwfs s /\ v NOTIN FDOM s /\ v NOTIN nvars (nwalkstar s t) ==> 41 nwfs (s |+ (v, t)) 42Proof 43 SRW_TAC [boolSimps.CONJ_ss][noc_eq_nvars_nwalkstar, nwfs_no_cycles] THEN 44 STRIP_TAC THEN 45 `!u. u IN nvars t ==> ~(nvR s)^+ v u` 46 by METIS_TAC [TC_nvR_nvars_nwalkstar, nwfs_no_cycles] THEN 47 `?u. (nvR s)^* v v' /\ u IN nvars t /\ (nvR s)^* v' u` 48 by METIS_TAC [TC_nvR_update] THEN 49 FULL_SIMP_TAC (srw_ss()) [RTC_CASES_TC] THEN 50 METIS_TAC [NOT_FDOM_nwalkstar,nwfs_no_cycles,TC_RULES] 51QED 52 53Type fe = ``:(string # num) set`` 54Type pkg[pp] = ``:('a nsubst # fe)`` 55 56Definition term_fcs_def: 57 term_fcs a t = 58 case t 59 of Nom b => if a = b then NONE else SOME {} 60 | Sus p v => SOME {(lswapstr (REVERSE p) a, v)} 61 | Tie b tt => if a = b then SOME {} else term_fcs a tt 62 | nPair t1 t2 => OPTION_MAP2 $UNION (term_fcs a t1) (term_fcs a t2) 63 | nConst _ => SOME {} 64Termination 65 WF_REL_TAC `measure (npair_count o SND)` THEN SRW_TAC [ARITH_ss][] 66End 67 68Theorem term_fcs_monadic_thm: 69 term_fcs a t = 70 case t 71 of Nom b => if a = b then NONE else SOME {} 72 | Sus p v => SOME {(lswapstr (REVERSE p) a, v)} 73 | Tie b tt => if a = b then SOME {} else term_fcs a tt 74 | nPair t1 t2 => do fe1 <- term_fcs a t1; 75 fe2 <- term_fcs a t2; 76 return (fe1 ��� fe2) 77 od 78 | nConst _ => SOME {} 79Proof 80Cases_on `t` THEN SRW_TAC [][Once term_fcs_def] THEN 81Q.MATCH_RENAME_TAC `OPTION_MAP2 $UNION x1 x2 = _` THEN 82Cases_on `x1` THEN SRW_TAC [][] THEN 83Cases_on `x2` THEN SRW_TAC [][] 84QED 85 86Definition fcs_acc_def: 87 fcs_acc s (a,v) ac = OPTION_MAP2 $UNION ac (term_fcs a (nwalk* s (Sus [] v))) 88End 89 90Definition unify_eq_vars_def: 91 unify_eq_vars ds v (s,fe) = 92 do fex <- ITSET (fcs_acc s) (IMAGE (��a. (a,v)) ds) (SOME {}); 93 SOME (s,fe UNION fex) 94 od 95End 96 97Definition add_bdg_def[simp]: 98 add_bdg pi v t0 (s,fe) = 99 let t = (apply_pi (REVERSE pi) t0) in 100 if noc s t v then NONE else SOME ((s|+(v,t)),fe) 101End 102 103val ntunify_defn_q = ` 104 ntunify (s,fe) t1 t2 = 105 if nwfs s then 106 case (nwalk s t1, nwalk s t2) 107 of (Nom a1, Nom a2) => if a1 = a2 then SOME (s,fe) else NONE 108 | (Sus pi1 v1, Sus pi2 v2) => 109 if v1 = v2 110 then unify_eq_vars (dis_set pi1 pi2) v1 (s,fe) 111 else add_bdg pi1 v1 (Sus pi2 v2) (s,fe) 112 | (Sus pi1 v1, t2) => add_bdg pi1 v1 t2 (s,fe) 113 | (t1, Sus pi2 v2) => add_bdg pi2 v2 t1 (s,fe) 114 | (Tie a1 t1, Tie a2 t2) => 115 if a1 = a2 then ntunify (s,fe) t1 t2 116 else do fcs <- term_fcs a1 (nwalk* s t2); 117 ntunify (s, fe UNION fcs) t1 (apply_pi [(a1,a2)] t2) 118 od 119 | (nPair t1a t1d, nPair t2a t2d) => 120 do (sx,fex) <- ntunify (s,fe) t1a t2a; 121 ntunify (sx,fex) t1d t2d 122 od 123 | (nConst c1, nConst c2) => if c1 = c2 then SOME (s,fe) else NONE 124 | _ => NONE 125 else ARB` 126 127val ntunify_defn = Hol_defn "ntunify" ntunify_defn_q 128 129val _ = store_term_thm("ntunify_defn", TermWithCase ntunify_defn_q) 130 131val SOME ntunify_aux_defn = Defn.aux_defn ntunify_defn 132 133Definition sysvars_def: 134 sysvars s (t1:'a nterm) (t2:'a nterm) = 135 nvars t1 UNION nvars t2 UNION 136 FDOM s UNION BIGUNION (FRANGE (nvars o_f s)) 137End 138 139Theorem FINITE_sysvars[simp]: FINITE (sysvars s t1 t2) 140Proof 141 SRW_TAC [][sysvars_def] THEN 142 FULL_SIMP_TAC (srw_ss()) [FRANGE_DEF] THEN 143 Cases_on `s ' x'` THEN SRW_TAC [][o_f_DEF] 144QED 145 146Theorem sysvars_comm: sysvars s t1 t2 = sysvars s t2 t1 147Proof SRW_TAC [][sysvars_def] THEN METIS_TAC [UNION_COMM] 148QED 149 150Theorem sysvars_apply_pi: (sysvars s t1 t2 = sysvars s (apply_pi pi t1) t2) 151Proof SRW_TAC [][sysvars_def] 152QED 153 154Definition uR_def: 155 uR = ��((sx,fex:fe),c,c2) ((s,fe:fe),t,t2). 156 nwfs sx 157 /\ s SUBMAP sx 158 /\ sysvars sx c c2 SUBSET sysvars s t t2 159 /\ measure (npair_count o (nwalkstar sx)) c t 160End 161 162Theorem WF_uR: WF nunifDef$uR 163Proof 164SRW_TAC [][WF_IFF_WELLFOUNDED,wellfounded_def,uR_def,UNCURRY] THEN 165SPOSE_NOT_THEN STRIP_ASSUME_TAC THEN 166Q.ABBREV_TAC `f1 = \n. FST (FST (f n))` THEN 167`!n. FST (FST (f n)) = f1 n` by SRW_TAC [][Abbr`f1`] THEN 168Q.ABBREV_TAC `f2 = \n. FST (SND (f n))` THEN 169`!n. FST (SND (f n)) = f2 n` by SRW_TAC [][Abbr`f2`] THEN 170Q.ABBREV_TAC `f3 = \n. SND (SND (f n))` THEN 171`!n. SND (SND (f n)) = f3 n` by SRW_TAC [][Abbr`f3`] THEN 172FULL_SIMP_TAC (srw_ss()) [] THEN 173REPEAT (Q.PAT_X_ASSUM `Abbrev B` (K ALL_TAC)) THEN 174`!m n. m < n ==> 175 sysvars (f1 n) (f2 n) (f3 n) ��� sysvars (f1 m) (f2 m) (f3 m)` 176 by (Induct THENL 177 [Induct THEN1 SRW_TAC [][] THEN 178 Cases_on `n` THEN METIS_TAC [SUBSET_TRANS,LESS_0], 179 Induct THEN1 SRW_TAC [][] THEN STRIP_TAC THEN 180 `SUC m < n \/ (SUC m = n)` by (SRW_TAC [ARITH_ss] [LESS_EQ]) THEN 181 METIS_TAC [SUBSET_TRANS] 182 ]) THEN 183`!m n. m < n ==> f1 m SUBMAP f1 n` 184 by (Induct THENL 185 [Induct THEN1 SRW_TAC [][] THEN 186 Cases_on `n` THEN METIS_TAC [SUBMAP_TRANS,LESS_0], 187 Induct THEN1 SRW_TAC [][] THEN STRIP_TAC THEN 188 `SUC m < n \/ (SUC m = n)` by (SRW_TAC [ARITH_ss] [LESS_EQ]) THEN 189 METIS_TAC [SUBMAP_TRANS] 190 ]) THEN 191`?m.!n. m < n ==> 192 (sysvars (f1 n) (f2 n) (f3 n) = sysvars (f1 m) (f2 m) (f3 m))` 193 by (SPOSE_NOT_THEN STRIP_ASSUME_TAC THEN 194 FULL_SIMP_TAC (srw_ss()) [SKOLEM_THM] THEN 195 `!m. m < f' m /\ 196 sysvars (f1 (f' m)) (f2 (f' m)) (f3 (f' m)) 197 PSUBSET 198 sysvars (f1 m) (f2 m) (f3 m)` 199 by (METIS_TAC [PSUBSET_DEF]) THEN 200 `!m.measure CARD 201 (sysvars (f1 (f' m)) (f2 (f' m)) (f3 (f' m))) 202 (sysvars (f1 m) (f2 m) (f3 m))` 203 by (METIS_TAC [measure_thm,FINITE_sysvars,CARD_PSUBSET]) 204 THEN 205 `WF (measure (CARD:((num -> bool) -> num)))` by SRW_TAC [][] THEN 206 FULL_SIMP_TAC bool_ss [WF_IFF_WELLFOUNDED,wellfounded_def] THEN 207 POP_ASSUM (Q.SPEC_THEN 208 `\n. let t = FUNPOW f' n 0 209 in sysvars (f1 t) (f2 t) (f3 t)` 210 MP_TAC) THEN 211 FULL_SIMP_TAC (srw_ss()) [LET_THM,FUNPOW_SUC]) THEN 212`?m. !n. m < n ==> (f1 m = f1 n)` 213by (Q.ISPECL_THEN 214 [`f1`, `\n. sysvars (f1 n) (f2 n) (f3 n) DIFF (FDOM(f1 n))`, `m`] 215 (MATCH_MP_TAC o GSYM o SIMP_RULE (srw_ss()) [Excl"UNION_DIFF_EQ"]) 216 commonUnifTheory.extension_chain THEN 217 SRW_TAC [][DISJOINT_DEF,Excl"UNION_DIFF_EQ"] THENL [ 218 SRW_TAC [][EXTENSION] THEN METIS_TAC [], 219 METIS_TAC [UNION_DIFF,sysvars_def,SUBSET_UNION,SUBSET_TRANS] 220 ]) THEN 221Q.ABBREV_TAC `z = MAX m m'` THEN 222`!n. z < n ==> (f1 n = f1 m')` 223 by (METIS_TAC [MAX_LT]) THEN 224`!n. z < n ==> npair_count (nwalkstar (f1 m') (f2 (SUC n))) < 225 npair_count (nwalkstar (f1 m') (f2 n))` 226 by (METIS_TAC [LESS_SUC]) THEN 227`WF (measure (npair_count o (nwalkstar (f1 m'))))` 228 by SRW_TAC [][] THEN 229FULL_SIMP_TAC bool_ss [WF_IFF_WELLFOUNDED,wellfounded_def] THEN 230POP_ASSUM (Q.SPEC_THEN `\n. f2(z+n+1)` MP_TAC) THEN 231SRW_TAC [][ADD_CLAUSES] THEN 232SRW_TAC [ARITH_ss][] 233QED 234 235val nwalkstar_subpair = Q.store_thm( 236"nwalkstar_subpair", 237`nwfs s /\ (nwalk s t1 = nPair t1a t1d) ==> 238 npair_count (nwalkstar s t1a) < npair_count (nwalkstar s t1) /\ 239 npair_count (nwalkstar s t1d) < npair_count (nwalkstar s t1)`, 240SRW_TAC [][nwalk_def] THEN 241Cases_on `t1` THEN 242Q.PAT_X_ASSUM `nwfs s` ASSUME_TAC THEN 243FULL_SIMP_TAC (srw_ss()) [nvwalk_case_thms] THEN 244FULL_SIMP_TAC (srw_ss() ++ ARITH_ss) []) 245 246val nwalkstar_subtie = Q.store_thm( 247"nwalkstar_subtie", 248`nwfs s /\ (nwalk s t1 = Tie a1 t1a) ==> 249 npair_count (nwalkstar s t1a) < npair_count (nwalkstar s t1)`, 250SRW_TAC [][nwalk_def] THEN 251Cases_on `t1` THEN 252Q.PAT_X_ASSUM `nwfs s` ASSUME_TAC THEN 253FULL_SIMP_TAC (srw_ss()) [nvwalk_case_thms] THEN 254FULL_SIMP_TAC (srw_ss() ++ ARITH_ss) []) 255 256val lemp = Q.prove( 257`(nwfs s ��� (nvwalk s p v = nPair ta td) ��� v IN FDOM s) ��� 258 ���ta td. nvars ta SUBSET nvars (nPair ta td) ��� 259 nvars td SUBSET nvars (nPair ta td)`, 260SRW_TAC [][] THEN METIS_TAC [NOT_FDOM_nvwalk,ntermeq_thm]) 261 262val sysvars_SUBSET_pairs = Q.store_thm( 263"sysvars_SUBSET_pairs", 264`nwfs s /\ 265 (nwalk s t1 = nPair t1a t1d) /\ 266 (nwalk s t2 = nPair t2a t2d) ==> 267 sysvars s t1a t2a SUBSET sysvars s t1 t2 /\ 268 sysvars s t1d t2d SUBSET sysvars s t1 t2`, 269SRW_TAC [][nwalk_def,sysvars_def] THEN 270Cases_on `t1` THEN Cases_on `t2` THEN 271Q.PAT_X_ASSUM `nwfs s` ASSUME_TAC THEN 272FULL_SIMP_TAC (srw_ss()) [nvwalk_case_thms] THEN 273METIS_TAC [nvars_nvwalk_SUBSET_FRANGE, lemp, SUBSET_TRANS,SUBSET_UNION]) 274 275val lemt = Q.prove( 276`(nwfs s ��� (nvwalk s p v = Tie ta td) ��� v IN FDOM s) ��� 277 ���ta td. nvars td SUBSET nvars (Tie ta td)`, 278SRW_TAC [][] THEN METIS_TAC [NOT_FDOM_nvwalk,ntermeq_thm]) 279 280val sysvars_SUBSET_ties = Q.store_thm( 281"sysvars_SUBSET_ties", 282`nwfs s ��� 283 (nwalk s t1 = Tie a1 t1a) ��� 284 (nwalk s t2 = Tie a2 t2a) ��� 285 sysvars s t1a t2a SUBSET sysvars s t1 t2`, 286SRW_TAC [][nwalk_def,sysvars_def] THEN 287Cases_on `t1` THEN Cases_on `t2` THEN 288Q.PAT_X_ASSUM `nwfs s` ASSUME_TAC THEN 289FULL_SIMP_TAC (srw_ss()) [nvwalk_case_thms] THEN 290METIS_TAC [nvars_nvwalk_SUBSET_FRANGE,lemt,SUBSET_TRANS,SUBSET_UNION]); 291 292val tca_thm = Q.store_thm( 293"tca_thm", 294`nwfs (FST p) /\ 295 (nwalk (FST p) t1 = nPair t1a t1d) /\ 296 (nwalk (FST p) t2 = nPair t2a t2d) ==> 297 uR (p,t1a,t2a) (p,t1,t2)`, 298Cases_on `p` THEN 299SRW_TAC [][uR_def,SUBMAP_REFL] THEN1 300METIS_TAC [sysvars_SUBSET_pairs] THEN 301METIS_TAC [nwalkstar_subpair]); 302 303val tctie_thm = Q.store_thm( 304"tctie_thm", 305`nwfs (FST p) ��� 306 (nwalk (FST p) t1 = Tie a1 t1a) ��� 307 (nwalk (FST p) t2 = Tie a2 t2a) ��� 308 uR ((FST p,fex),t1a,apply_pi pi t2a) (p,t1,t2)`, 309Cases_on `p` THEN 310SRW_TAC [][uR_def,SUBMAP_REFL] THEN1 311METIS_TAC [sysvars_SUBSET_ties,sysvars_apply_pi,sysvars_comm] THEN 312METIS_TAC [nwalkstar_subtie]); 313 314val aux_def = 315SIMP_RULE std_ss [] 316(MATCH_MP 317 (MATCH_MP WFREC_COROLLARY 318 (Q.SPEC`nunifDef$uR`(definition"ntunify_tupled_AUX_def"))) 319 WF_uR); 320 321val uR_ind = WF_INDUCTION_THM |> Q.ISPEC `nunifDef$uR` |> SIMP_RULE (srw_ss()) [WF_uR] 322|> Q.SPEC `\(a,b,c).P (FST a) (SND a) b c` 323|> SIMP_RULE std_ss [FORALL_PROD] |> Q.GEN`P`; 324 325val FRANGE_DOMSUB_SUBSET = Q.store_thm( 326"FRANGE_DOMSUB_SUBSET", 327`BIGUNION (FRANGE (f \\ x)) SUBSET BIGUNION (FRANGE f)`, 328SRW_TAC [][BIGUNION,SUBSET_DEF,FRANGE_DEF] THEN 329METIS_TAC [DOMSUB_FAPPLY_THM]); 330 331val met1 = 332[nvars_nvwalk_SUBSET_FRANGE,lemp,lemt, 333SUBSET_TRANS,SUBSET_UNION,FRANGE_DOMSUB_SUBSET,o_f_DOMSUB]; 334 335val met2 = 336[nvars_apply_pi,FRANGE_FLOOKUP,o_f_FRANGE, 337 SUBSET_UNION,SUBSET_BIGUNION_I,SUBSET_TRANS]; 338 339val lem1 = Q.prove( 340`nwfs s ��� (nvwalk s pv v = Sus py y) ��� 341 ((nvwalk s px x = nPair (Sus pv v) t2) ��� 342 (nvwalk s px x = nPair t2 (Sus pv v))) ��� 343 ���vs. y IN vs ��� vs IN FRANGE (nvars o_f s)`, 344SRW_TAC [][] THENL [ 345 MP_TAC (Q.SPECL [`v`,`nvwalk s pv v`,`s`,`pv`] (GEN_ALL nvwalk_FDOM)) THEN 346 MP_TAC (Q.SPECL [`x`,`nvwalk s px x`,`s`,`px`] (GEN_ALL nvwalk_FDOM)) THEN 347 SRW_TAC [][] THENL [ 348 `v IN nvars (nPair (Sus pv v) t2)` by SRW_TAC [][] THEN 349 METIS_TAC [FRANGE_FLOOKUP,o_f_FRANGE,nvars_apply_pi], 350 `y IN nvars (Sus py y)` by SRW_TAC [][] THEN 351 METIS_TAC [FRANGE_FLOOKUP,o_f_FRANGE,nvars_apply_pi] 352 ], 353 MP_TAC (Q.SPECL [`v`,`nvwalk s pv v`,`s`,`pv`] (GEN_ALL nvwalk_FDOM)) THEN 354 MP_TAC (Q.SPECL [`x`,`nvwalk s px x`,`s`,`px`] (GEN_ALL nvwalk_FDOM)) THEN 355 SRW_TAC [][] THENL [ 356 `v IN nvars (nPair t2 (Sus pv v))` by SRW_TAC [][] THEN 357 METIS_TAC [FRANGE_FLOOKUP,o_f_FRANGE,nvars_apply_pi], 358 `y IN nvars (Sus py y)` by SRW_TAC [][] THEN 359 METIS_TAC [FRANGE_FLOOKUP,o_f_FRANGE,nvars_apply_pi] 360 ] 361]); 362 363val lem2 = Q.prove( 364`nwfs s ��� ((nvwalk s px x = nPair (Sus pv v) t2) ��� 365 (nvwalk s px x = nPair t2 (Sus pv v))) ��� 366 nvars (nvwalk s pv v) SUBSET BIGUNION (FRANGE (nvars o_f s))`, 367Cases_on `nvwalk s pv v` THEN SRW_TAC [][] THENL [ 368 METIS_TAC [lem1], 369 METIS_TAC [lem1], 370 MP_TAC (Q.SPECL [`v`,`nvwalk s pv v`,`s`,`pv`] (GEN_ALL nvwalk_FDOM)) THEN SRW_TAC [][] THEN 371 `nvars C SUBSET (nvars (Tie s' C))` by SRW_TAC [][] THEN METIS_TAC met1, 372 MP_TAC (Q.SPECL [`v`,`nvwalk s pv v`,`s`,`pv`] (GEN_ALL nvwalk_FDOM)) THEN SRW_TAC [][] THEN 373 `nvars C SUBSET (nvars (Tie s' C))` by SRW_TAC [][] THEN METIS_TAC met1, 374 MP_TAC (Q.SPECL [`v`,`nvwalk s pv v`,`s`,`pv`] (GEN_ALL nvwalk_FDOM)) THEN SRW_TAC [][] THEN 375 `nvars C SUBSET (nvars (nPair C C0))` by SRW_TAC [][] THEN METIS_TAC met1, 376 MP_TAC (Q.SPECL [`v`,`nvwalk s pv v`,`s`,`pv`] (GEN_ALL nvwalk_FDOM)) THEN SRW_TAC [][] THEN 377 `nvars C SUBSET (nvars (nPair C C0))` by SRW_TAC [][] THEN METIS_TAC met1, 378 MP_TAC (Q.SPECL [`v`,`nvwalk s pv v`,`s`,`pv`] (GEN_ALL nvwalk_FDOM)) THEN SRW_TAC [][] THEN 379 `nvars C SUBSET (nvars (nPair C C0))` by SRW_TAC [][] THEN METIS_TAC met1, 380 MP_TAC (Q.SPECL [`v`,`nvwalk s pv v`,`s`,`pv`] (GEN_ALL nvwalk_FDOM)) THEN SRW_TAC [][] THEN 381 `nvars C0 SUBSET (nvars (nPair C C0))` by SRW_TAC [][] THEN METIS_TAC met1 382]); 383 384val lem3 = Q.prove( 385`nwfs s ��� (nvwalk s px x = nPair t1 t2) ��� 386 (vs SUBSET (nvars t1) ��� 387 vs SUBSET (nvars t2)) ��� 388 vs SUBSET BIGUNION (FRANGE (nvars o_f s))`, 389SRW_TAC [][] THENL [ 390 MP_TAC (Q.SPECL [`x`,`nvwalk s px x`,`s`,`px`] (GEN_ALL nvwalk_FDOM)) THEN SRW_TAC [][] THEN 391 METIS_TAC met1, 392 MP_TAC (Q.SPECL [`x`,`nvwalk s px x`,`s`,`px`] (GEN_ALL nvwalk_FDOM)) THEN SRW_TAC [][] THEN 393 METIS_TAC met1 394]); 395 396fun tac1 t1a t2a = 397Cases_on t1a THEN 398Q.PAT_X_ASSUM `nwfs s` ASSUME_TAC THEN 399FULL_SIMP_TAC (srw_ss()) [nvwalk_case_thms] THEN 400SRW_TAC [][sysvars_def] THENL [ 401 METIS_TAC met1, METIS_TAC met1, METIS_TAC [lem1], METIS_TAC met1, 402 Cases_on t2a THEN FULL_SIMP_TAC (srw_ss()) [nvwalk_case_thms] THENL [ 403 METIS_TAC (lem2::met1), 404 Q.MATCH_ABBREV_TAC `X SUBSET Y` THEN 405 `X SUBSET BIGUNION (FRANGE (nvars o_f s))` by METIS_TAC (lem3::met1) THEN 406 METIS_TAC met1, 407 Q.MATCH_ABBREV_TAC `X1 SUBSET Y1 ��� X2 SUBSET Y2` THEN 408 `X1 SUBSET BIGUNION (FRANGE (nvars o_f s)) ��� 409 X2 SUBSET BIGUNION (FRANGE (nvars o_f s))` by 410 METIS_TAC (lem3::met1) THEN 411 METIS_TAC met1 412 ], 413 METIS_TAC met1 414]; 415 416val lem4 = Q.prove( 417`nwfs s ��� nvars (nvwalk s px x) SUBSET {x} ��� nvars (nvwalk s px x) SUBSET BIGUNION (FRANGE (nvars o_f s))`, 418MP_TAC (Q.SPECL [`x`,`nvwalk s px x`,`s`,`px`] (GEN_ALL nvwalk_FDOM)) THEN SRW_TAC [][] THEN 419FULL_SIMP_TAC (srw_ss()) [] THEN 420METIS_TAC ([FRANGE_FLOOKUP,o_f_FRANGE,nvars_apply_pi]@met2)); 421 422fun tac2 t = 423Cases_on t THEN 424Q.PAT_X_ASSUM `nwfs s` ASSUME_TAC THEN 425FULL_SIMP_TAC (srw_ss()) [nvwalk_case_thms] THEN 426SRW_TAC [][sysvars_def] THENL [ 427 METIS_TAC met1, METIS_TAC met1, METIS_TAC [lem1], METIS_TAC met1, 428 Cases_on `C` THEN FULL_SIMP_TAC (srw_ss()) [nvwalk_case_thms] THENL [ 429 METIS_TAC (lem4::met1), 430 METIS_TAC met1, 431 METIS_TAC met1 432 ], 433 METIS_TAC met1 434]; 435 436fun tac3 t = 437Cases_on `C` THEN 438Q.PAT_X_ASSUM `nwfs s` ASSUME_TAC THEN 439FULL_SIMP_TAC (srw_ss()) [nvwalk_case_thms] THEN 440SRW_TAC [][sysvars_def] THENL [ 441 `nvars t1d SUBSET (nvars (nPair t1a t1d))` by SRW_TAC [][] THEN 442 METIS_TAC (lem4::met1), 443 METIS_TAC met1, 444 MP_TAC (Q.SPECL [`n'`,`nvwalk s l' n'`,`s`,`l'`] (GEN_ALL nvwalk_FDOM)) THEN SRW_TAC [][] THEN 445 `v IN nvars (Sus p v)` by SRW_TAC [][] THEN 446 METIS_TAC [FRANGE_FLOOKUP,o_f_FRANGE,nvars_apply_pi], 447 METIS_TAC met1, 448 Cases_on t THEN FULL_SIMP_TAC (srw_ss()) [nvwalk_case_thms] THENL [ 449 METIS_TAC (lem2::met1), 450 Q.MATCH_ABBREV_TAC `X SUBSET Y` THEN 451 `X SUBSET BIGUNION (FRANGE (nvars o_f s))` by METIS_TAC (lem3::met1) THEN 452 METIS_TAC met1, 453 Q.MATCH_ABBREV_TAC `X1 SUBSET Y1 ��� X2 SUBSET Y2` THEN 454 `X1 SUBSET BIGUNION (FRANGE (nvars o_f s)) ��� 455 X2 SUBSET BIGUNION (FRANGE (nvars o_f s))` by 456 METIS_TAC (lem3::met1) THEN 457 METIS_TAC met1 458 ], 459 METIS_TAC met1 460]; 461 462fun tac5 t1 t2 = 463Cases_on t1 THEN 464Q.PAT_X_ASSUM `nwfs s` ASSUME_TAC THEN 465FULL_SIMP_TAC (srw_ss()) [nvwalk_case_thms] THEN 466SRW_TAC [][sysvars_def] THENL [ 467 METIS_TAC met1, METIS_TAC met1, 468 MP_TAC (Q.SPECL [`n`,`nvwalk s l n`,`s`,`l`] (GEN_ALL nvwalk_FDOM)) THEN SRW_TAC [][] THEN 469 `v IN nvars (Sus p v)` by SRW_TAC [][] THEN 470 METIS_TAC [FRANGE_FLOOKUP,o_f_FRANGE,nvars_apply_pi], 471 METIS_TAC met1, 472 Cases_on t2 THEN FULL_SIMP_TAC (srw_ss()) [nvwalk_case_thms] THENL [ 473 METIS_TAC (lem4::met1), 474 METIS_TAC met1, 475 METIS_TAC met1 476 ], 477 METIS_TAC met1 478]; 479 480val sysvars_SUBSET_FUPDATE_pairs = Q.store_thm( 481"sysvars_SUBSET_FUPDATE_pairs", 482`nwfs (s |+ (v,apply_pi pi t)) /\ v NOTIN FDOM s /\ 483 (nwalk s t1 = nPair t1a t1d) /\ 484 (nwalk s t2 = nPair t2a t2d) /\ 485 (((���p.nwalk s t1a = Sus p v) /\ (nwalk s t2a = t)) \/ 486 ((���p.nwalk s t2a = Sus p v) /\ (nwalk s t1a = t))) ==> 487 sysvars (s |+ (v,apply_pi pi t)) t1d t2d SUBSET sysvars s t1 t2`, 488SIMP_TAC (srw_ss()) [nwalk_def,GSYM AND_IMP_INTRO] THEN 489NTAC 2 STRIP_TAC THEN 490`nwfs s` by METIS_TAC [nwfs_SUBMAP,SUBMAP_FUPDATE_EQN] THEN 491Q.MATCH_ABBREV_TAC `X1 ��� X2 ��� Y` THEN 492MAP_EVERY Q.UNABBREV_TAC [`X1`,`X2`] THEN 493Cases_on `t1` THEN Cases_on `t2` THEN 494SRW_TAC [][nvwalk_case_thms] THEN 495Q.UNABBREV_TAC `Y` THENL [ 496 STRIP_TAC THENL [ tac1 `t1a` `t2a`, tac1 `t2a` `t1a`], 497 Q.MATCH_ABBREV_TAC `X ��� Y SUBSET sysvars s Z (nPair C C0)` THEN 498 TRY (Q.RM_ABBREV_TAC `C`) THEN UNABBREV_ALL_TAC THEN 499 STRIP_TAC THENL [ tac2 `t1a`, tac3 `t1a`], 500 Q.MATCH_ABBREV_TAC `X ��� Y SUBSET sysvars s (nPair C C0) Z` THEN 501 TRY (Q.RM_ABBREV_TAC `C`) THEN UNABBREV_ALL_TAC THEN 502 STRIP_TAC THENL [ tac3 `t2a`, tac2 `t2a`], 503 Q.MATCH_ABBREV_TAC `X ��� Y SUBSET sysvars s (nPair C1 D1) (nPair C2 D2)` THEN 504 MAP_EVERY Q.RM_ABBREV_TAC [`C1`,`C2`] THEN UNABBREV_ALL_TAC THEN 505 STRIP_TAC THENL [ tac5 `C1` `C2`, tac5 `C2` `C1`] 506]); 507 508val nwalkstar_subpair_FUPDATE = Q.store_thm( 509"nwalkstar_subpair_FUPDATE", 510`nwfs s /\ v NOTIN FDOM s /\ v NOTIN nvars (nwalkstar s t) /\ 511 (nwalk s t1 = nPair t1a t1d) ==> 512 npair_count (nwalkstar (s |+ (v,apply_pi pi t)) t1d) < 513 npair_count (nwalkstar (s |+ (v,apply_pi pi t)) t1)`, 514SRW_TAC [][] THEN 515`nwfs (s |+ (v,apply_pi pi t))` by METIS_TAC [nwfs_extend,nvars_nwalkstar_ignores_pi] THEN 516`s SUBMAP (s |+ (v,apply_pi pi t))` by METIS_TAC [SUBMAP_FUPDATE_EQN] THEN 517Q.PAT_X_ASSUM `nwfs s` ASSUME_TAC THEN 518`nwalk (s |+ (v,apply_pi pi t)) t1 = nPair t1a t1d` 519 by (Cases_on `t1` THEN FULL_SIMP_TAC (srw_ss()) [] THEN 520 (Q.MATCH_ABBREV_TAC `nvwalk sx pn n = nPair t1a t1d` THEN 521 Q_TAC SUFF_TAC `nvwalk s pn n = nvwalk sx pn n` THEN1 SRW_TAC [][] THEN 522 MATCH_MP_TAC (SIMP_RULE (srw_ss()) [AND_IMP_INTRO] (UNDISCH nvwalk_SUBMAP)) THEN 523 SRW_TAC [][Abbr`sx`])) THEN 524Q.PAT_X_ASSUM `nwfs (s|+x)` ASSUME_TAC THEN 525Cases_on `t1` THEN FULL_SIMP_TAC (srw_ss()) [nwalk_def,nvwalk_case_thms] THEN 526SRW_TAC [ARITH_ss][nwalkstar_thm] 527) 528 529val uR_subpair_FUPDATE = Q.prove( 530`nwfs s /\ v NOTIN FDOM s /\ v NOTIN nvars (nwalkstar s t) /\ 531 (nwalk s t1 = nPair t1a t1d) /\ 532 (nwalk s t2 = nPair t2a t2d) /\ 533 (((���l. nwalk s t1a = Sus l v) /\ (nwalk s t2a = t)) \/ 534 ((���l. nwalk s t2a = Sus l v) /\ (nwalk s t1a = t))) ==> 535 uR ((s |+ (v,apply_pi pi t),fe), t1d, t2d) ((s,fe),t1,t2)`, 536STRIP_TAC THEN 537`nwfs (s |+ (v,apply_pi pi t))` by METIS_TAC [nwfs_extend,nvars_nwalkstar_ignores_pi] THEN 538`s SUBMAP (s|+(v,apply_pi pi t))` by METIS_TAC [SUBMAP_FUPDATE_EQN] THEN 539(SRW_TAC [][uR_def] THEN1 540 METIS_TAC [sysvars_SUBSET_FUPDATE_pairs] THEN 541 METIS_TAC [nwalkstar_subpair_FUPDATE]) 542) 543 544val uR_subpair = Q.prove( 545`nwfs s /\ 546 (nwalk s t1 = nPair t1a t1d) /\ 547 (nwalk s t2 = nPair t2a t2d) ==> 548 uR ((s,fe),t1a,t2a) ((s,fe),t1,t2) /\ 549 uR ((s,fe),t1d,t2d) ((s,fe),t1,t2)`, 550REPEAT STRIP_TAC THEN 551SRW_TAC [][uR_def,SUBMAP_REFL] THEN 552METIS_TAC [sysvars_SUBSET_pairs,nwalkstar_subpair] 553) 554 555val uR_subtie = Q.prove( 556`nwfs s ��� 557 (nwalk s t1 = Tie a1 t1a) ��� 558 (nwalk s t2 = Tie a2 t2a) ��� 559 uR ((s,fe),t1a,t2a) ((s,fe),t1,t2)`, 560SRW_TAC [][uR_def,SUBMAP_REFL] THEN 561METIS_TAC [sysvars_SUBSET_ties,nwalkstar_subtie]) 562 563val uP_def = Define` 564 uP sx s t1 t2 <=> nwfs sx ��� s SUBMAP sx ��� 565 FDOM sx ��� BIGUNION (FRANGE (nvars o_f sx)) ��� sysvars s t1 t2 566`; 567 568val lem5 = Q.prove( 569`nwfs s ��� (nvwalk s l n = Sus p v ) ��� 570 (v = n) ��� (���vs. v IN vs ��� vs IN FRANGE (nvars o_f s))`, 571MP_TAC (Q.SPECL [`n`,`nvwalk s l n`,`s`,`l`] (GEN_ALL nvwalk_FDOM)) THEN SRW_TAC [][] THEN 572FULL_SIMP_TAC (srw_ss()) [] THEN 573DISJ2_TAC THEN Q.EXISTS_TAC `nvars (Sus p v)` THEN 574CONJ_TAC THEN1 SRW_TAC [][] THEN 575METIS_TAC [o_f_FRANGE,nvars_apply_pi,FRANGE_FLOOKUP]) 576 577val uP_subterm_FUPDATE = Q.prove( 578`nwfs s /\ v NOTIN FDOM s /\ v NOTIN nvars (nwalkstar s t) /\ 579 (((���p. nwalk s t1 = Sus p v) /\ (nwalk s t2 = t)) \/ 580 ((���p. nwalk s t2 = Sus p v) /\ (nwalk s t1 = t))) ==> 581 uP (s |+ (v,apply_pi pi t)) s t1 t2`, 582STRIP_TAC THEN 583`nwfs (s |+ (v,apply_pi pi t))` by METIS_TAC [nwfs_extend,nvars_nwalkstar_ignores_pi] THEN 584`s SUBMAP (s|+(v,apply_pi pi t))` by METIS_TAC [SUBMAP_FUPDATE_EQN] THEN 585Q.MATCH_ASSUM_RENAME_TAC `nwalk s tt = Sus p v` THEN 586Q.PAT_X_ASSUM `nwalk s tt = Sus p v` MP_TAC THEN 587Cases_on `tt` THEN SRW_TAC [][nwalk_def] THENL [ 588 Cases_on `nwalk s t2` THEN Cases_on `t2`, 589 Cases_on `nwalk s t1` THEN Cases_on `t1` ] THEN 590Q.PAT_X_ASSUM `nwfs s` ASSUME_TAC THEN 591FULL_SIMP_TAC (srw_ss()) [nwalk_def,nvwalk_case_thms] THEN 592ASM_SIMP_TAC (srw_ss()) [uP_def,sysvars_def] THEN 593METIS_TAC (lem5::met1)) 594 595val uR_ignores_fe = Q.store_thm( 596"uR_ignores_fe", 597`uR ((s1,fe1),x1,y1) ((s2,fe2),x2,y2) ��� 598 uR ((s1,fe3),x1,y1) ((s2,fe4),x2,y2)`, 599SRW_TAC [][uR_def]) 600 601val npair_count_nwalkstar_ignores_pi = Q.store_thm( 602"npair_count_nwalkstar_ignores_pi", 603`nwfs s ��� !t pi. npair_count (nwalk* s t) = npair_count (nwalk* s (apply_pi pi t))`, 604STRIP_TAC THEN HO_MATCH_MP_TAC nwalkstar_ind THEN 605STRIP_TAC THEN REVERSE (Cases_on `t`) THEN FULL_SIMP_TAC (psrw_ss()) [] THEN1 606(SRW_TAC [][] THEN REPEAT (FIRST_X_ASSUM (Q.SPEC_THEN `pi` MP_TAC)) THEN 607 SRW_TAC [ARITH_ss][]) THEN 608Cases_on `nvwalk s l n` THEN FULL_SIMP_TAC (psrw_ss()) [Sus_case1] THEN 609REPEAT STRIP_TAC THEN 610(nvwalk_modulo_pi |> Q.SPECL_THEN [`s`,`l`,`n`] MP_TAC) THEN 611(nvwalk_modulo_pi |> Q.SPECL_THEN [`s`,`pi++l`,`n`] MP_TAC) THEN SRW_TAC [][] THEN 612Cases_on `nvwalk s [] n` THEN FULL_SIMP_TAC (srw_ss()) [Sus_case1] THEN 613REPEAT( FIRST_X_ASSUM (Q.SPEC_THEN `pi` MP_TAC)) THEN 614SRW_TAC [][apply_pi_decompose]) 615 616val uR_ignores_pi = Q.store_thm( 617"uR_ignores_pi", 618`uR ((s1,fe1),x1,y1) ((s2,fe2),x2,y2) ��� 619 uR ((s1,fe1),apply_pi px1 x1,apply_pi py1 y1) ((s2,fe2),apply_pi px2 x2,apply_pi py2 y2)`, 620SRW_TAC [][uR_def] THENL [ 621 METIS_TAC [sysvars_apply_pi,sysvars_comm], 622 FULL_SIMP_TAC (srw_ss()) [] THEN 623 METIS_TAC [npair_count_nwalkstar_ignores_pi] 624]) 625 626val uP_ignores_pi = Q.store_thm( 627"uP_ignores_pi", 628`uP s1 s2 x y ��� 629 uP s1 s2 (apply_pi px1 x) (apply_pi py2 y)`, 630SRW_TAC [][uP_def] THEN 631METIS_TAC [sysvars_apply_pi,sysvars_comm]) 632 633val uR_IMP_uP = Q.store_thm( 634"uR_IMP_uP", 635`uR ((sx,fex),c1,c2) ((s,fe),t1,t2) ==> uP sx s t1 t2`, 636SRW_TAC [][uR_def,uP_def,sysvars_def]) 637 638val nwalkstar_nwalk_SUBMAP = Q.store_thm( 639"nwalkstar_nwalk_SUBMAP", 640`s SUBMAP sx /\ nwfs sx ==> 641 (nwalk* sx t = nwalk* sx (nwalk s t))`, 642METIS_TAC [nwalkstar_SUBMAP,nwalkstar_nwalk,nwfs_SUBMAP]) 643 644val uP_IMP_subtie_uR = Q.store_thm( 645"uP_IMP_subtie_uR", 646`nwfs s ��� 647 (nwalk s t1 = Tie a1 t1a) ��� 648 (nwalk s t2 = Tie a2 t2a) ��� 649 uP sx s t1a t2a ��� 650 uR ((sx,fex),t1a,t2a) ((s,fe),t1,t2)`, 651SRW_TAC [][] THEN 652`sysvars s t1a t2a SUBSET sysvars s t1 t2` 653by METIS_TAC [sysvars_SUBSET_ties] THEN 654FULL_SIMP_TAC (srw_ss()) [uR_def,uP_def] THEN 655`FDOM sx SUBSET sysvars s t1 t2 ��� 656 BIGUNION (FRANGE (nvars o_f sx)) SUBSET sysvars s t1 t2` 657by METIS_TAC [SUBSET_TRANS] THEN 658SRW_TAC [][] THEN1 659FULL_SIMP_TAC (srw_ss()) [sysvars_def] THEN 660SRW_TAC [][measure_thm] THEN 661IMP_RES_TAC nwalkstar_nwalk_SUBMAP THEN 662FIRST_X_ASSUM (Q.SPEC_THEN `t1` MP_TAC) THEN 663SRW_TAC [][]) 664 665val uP_IMP_subpair_uR = Q.store_thm( 666"uP_IMP_subpair_uR", 667`nwfs s /\ 668 (nwalk s t1 = nPair t1a t1d) /\ 669 (nwalk s t2 = nPair t2a t2d) /\ 670 (uP sx s t1a t2a \/ uP sx s t1d t2d) ==> 671 uR ((sx,fex),t1d,t2d) ((s,fe),t1,t2)`, 672SRW_TAC [][] THEN ( 673`sysvars s t1a t2a SUBSET sysvars s t1 t2 /\ 674 sysvars s t1d t2d SUBSET sysvars s t1 t2` 675 by METIS_TAC [sysvars_SUBSET_pairs] THEN 676FULL_SIMP_TAC (srw_ss()) [uR_def,uP_def] THEN 677`FDOM sx SUBSET sysvars s t1 t2 /\ 678 BIGUNION (FRANGE (nvars o_f sx)) SUBSET sysvars s t1 t2` 679 by METIS_TAC [SUBSET_TRANS] THEN 680SRW_TAC [][] THEN1 681FULL_SIMP_TAC (srw_ss()) [sysvars_def] THEN 682SRW_TAC [][] THEN 683IMP_RES_TAC nwalkstar_nwalk_SUBMAP THEN 684FIRST_X_ASSUM (Q.SPEC_THEN `t1` MP_TAC) THEN 685SRW_TAC [ARITH_ss][])) 686 687val unify_eq_vars_preserves_s = Q.store_thm( 688"unify_eq_vars_preserves_s", 689`(unify_eq_vars x y (s,fe) = SOME (s',fe')) ��� (s = s')`, 690SRW_TAC [][unify_eq_vars_def]) 691 692val aux_uP = Q.prove( 693`!s fe t1 t2 sx fex. 694 nwfs s /\ (ntunify_tupled_aux uR ((s,fe),t1,t2) = SOME (sx,fex)) ==> 695 uP sx s t1 t2`, 696HO_MATCH_MP_TAC uR_ind THEN 697REPEAT (GEN_TAC ORELSE (DISCH_THEN STRIP_ASSUME_TAC)) THEN 698POP_ASSUM MP_TAC THEN 699ASM_SIMP_TAC (srw_ss()) [aux_def,LET_THM] THEN 700Cases_on `nwalk s t1` THEN Cases_on `nwalk s t2` 701THEN ASM_SIMP_TAC (srw_ss()) [] THENL [ 702 SRW_TAC [][uP_def,SUBMAP_REFL,sysvars_def] THEN 703 METIS_TAC [SUBSET_UNION,SUBSET_TRANS], 704 SRW_TAC [][] THEN 705 MATCH_MP_TAC (SIMP_RULE (srw_ss()) [] (Q.INST[`t`|->`Nom s'`] uP_subterm_FUPDATE)) THEN 706 SRW_TAC [][] THEN METIS_TAC [nwalk_to_var], 707 SRW_TAC [][] THEN 708 MATCH_MP_TAC (SIMP_RULE (srw_ss()) [] (Q.INST[`t`|->`Nom s'`] uP_subterm_FUPDATE)) THEN 709 SRW_TAC [][] THEN METIS_TAC [nwalk_to_var], 710 SRW_TAC [][] THENL [ 711 IMP_RES_TAC unify_eq_vars_preserves_s THEN 712 SRW_TAC [][uP_def,sysvars_def,SUBMAP_REFL] THEN 713 METIS_TAC [SUBSET_UNION,SUBSET_TRANS], 714 MATCH_MP_TAC (SIMP_RULE (srw_ss()) [] (Q.INST[`t`|->`Sus l' n'`] uP_subterm_FUPDATE)) THEN 715 SRW_TAC [][] THENL [ 716 METIS_TAC [nwalk_to_var], 717 Q.PAT_X_ASSUM `nwfs s` ASSUME_TAC THEN 718 Cases_on `t2` THEN 719 FULL_SIMP_TAC (srw_ss()) [nwalk_def] THEN 720 IMP_RES_TAC nvwalk_to_var THEN 721 SRW_TAC [][NOT_FDOM_nvwalk], 722 SELECT_ELIM_TAC THEN SRW_TAC [][permeq_sym] 723 ] 724 ], 725 SRW_TAC [][] THEN 726 MATCH_MP_TAC (SIMP_RULE (srw_ss()) [] (Q.INST[`t`|->`Tie s' C`] uP_subterm_FUPDATE)) THEN 727 SRW_TAC [][] THEN1 METIS_TAC [nwalk_to_var] THEN 728 METIS_TAC [noc_eq_nvars_nwalkstar,IN_DEF,nvars_nwalkstar_ignores_pi], 729 SRW_TAC [][] THEN 730 MATCH_MP_TAC (SIMP_RULE (srw_ss()) [] (Q.INST[`t`|->`nPair C C0`] uP_subterm_FUPDATE)) THEN 731 SRW_TAC [][] THEN1 METIS_TAC [nwalk_to_var] THEN 732 METIS_TAC [noc_eq_nvars_nwalkstar,IN_DEF,nvars_nwalkstar_ignores_pi], 733 SRW_TAC [][] THEN 734 MATCH_MP_TAC (SIMP_RULE (srw_ss()) [] (Q.INST[`t`|->`nConst s'`] uP_subterm_FUPDATE)) THEN 735 SRW_TAC [][] THEN METIS_TAC [nwalk_to_var], 736 SRW_TAC [][] THEN 737 MATCH_MP_TAC (SIMP_RULE (srw_ss()) [] (Q.INST[`t`|->`Tie s' C`] uP_subterm_FUPDATE)) THEN 738 SRW_TAC [][] THEN1 METIS_TAC [nwalk_to_var] THEN 739 METIS_TAC [noc_eq_nvars_nwalkstar,IN_DEF,nvars_nwalkstar_ignores_pi], 740 Q.MATCH_ABBREV_TAC `((if P then RESTRICT f R X ((s,fe),D,D') else Y) = Z) ==> 741 Z2` THEN 742 MAP_EVERY Q.RM_ABBREV_TAC [`D`, `D'`] THEN 743 UNABBREV_ALL_TAC THEN 744 SRW_TAC [][RESTRICT_LEMMA,uR_subtie] THENL [ 745 METIS_TAC [uR_subtie,uP_IMP_subtie_uR,uR_IMP_uP], 746 `���fex. uR ((s,fex),D,apply_pi [(s',s'')] D') ((s,fe),t1,t2)` 747 by METIS_TAC [uR_ignores_fe, uR_ignores_pi, 748 pmact_nil |> Q.ISPEC `nterm_pmact`, uR_subtie] THEN 749 Cases_on `term_fcs s' (nwalk* s D')` THEN 750 FULL_SIMP_TAC (srw_ss()) [RESTRICT_LEMMA] THEN 751 `uP sx s D (apply_pi [(s',s'')] D')` by METIS_TAC [] THEN 752 `uP sx s D D'` by METIS_TAC [uP_ignores_pi,apply_pi_inverse, pmact_nil] THEN 753 MATCH_MP_TAC (GEN_ALL uR_IMP_uP) THEN 754 METIS_TAC [uP_IMP_subtie_uR] 755 ], 756 SRW_TAC [][] THEN 757 MATCH_MP_TAC (SIMP_RULE (srw_ss()) [] (Q.INST[`t`|->`nPair C C0`] uP_subterm_FUPDATE)) THEN 758 SRW_TAC [][] THEN1 METIS_TAC [nwalk_to_var] THEN 759 METIS_TAC [noc_eq_nvars_nwalkstar,IN_DEF,nvars_nwalkstar_ignores_pi], 760 Q.MATCH_ASSUM_RENAME_TAC `nwalk s t1 = nPair D1a D1b` THEN 761 Q.MATCH_ASSUM_RENAME_TAC `nwalk s t2 = nPair D2a D2b` THEN 762 `uR ((s,fe),D1a,D2a) ((s,fe),t1,t2)` by METIS_TAC [uR_subpair] THEN 763 SRW_TAC [][RESTRICT_LEMMA] THEN 764 Cases_on `x` THEN 765 `uP q s D1a D2a` by METIS_TAC [] THEN 766 FULL_SIMP_TAC (srw_ss()) [UNCURRY] THEN 767 `uR ((q,r),D1b,D2b) ((s,fe),t1,t2)` by METIS_TAC [uP_IMP_subpair_uR] THEN 768 FULL_SIMP_TAC (srw_ss()) [RESTRICT_LEMMA,UNCURRY] THEN 769 `uP sx q D1b D2b` by METIS_TAC [uP_def] THEN 770 FULL_SIMP_TAC (srw_ss()) [uP_def,uR_def] THEN 771 METIS_TAC [SUBSET_TRANS,SUBMAP_TRANS], 772 SRW_TAC [][] THEN 773 MATCH_MP_TAC (SIMP_RULE (srw_ss()) [] (Q.INST[`t`|->`nConst s'`] uP_subterm_FUPDATE)) THEN 774 SRW_TAC [][] THEN METIS_TAC [nwalk_to_var], 775 SRW_TAC [][uP_def,sysvars_def,SUBMAP_REFL] THEN 776 METIS_TAC [SUBSET_TRANS,SUBSET_UNION] 777]) 778 779val nvars_nwalk = Q.store_thm( 780"nvars_nwalk", 781`nwfs s ��� (nwalk s t1 = t2) ��� 782 (nvars t2 SUBSET nvars t1) ��� 783 (nvars t2 SUBSET BIGUNION (FRANGE (nvars o_f s)))`, 784SRW_TAC [][] THEN 785Cases_on `t1` THEN SRW_TAC [][] THEN 786METIS_TAC [lem4]) 787 788val lem = Q.prove( 789`���s t1 t2 t3. s SUBSET t1 UNION t2 UNION t3 ��� t1 SUBSET t4 ��� t2 SUBSET t4 ��� t3 SUBSET t4 ��� s SUBSET t4`, 790SRW_TAC [][] THEN METIS_TAC [UNION_SUBSET,SUBSET_TRANS]) 791 792val sysvars_pairtie = Q.store_thm( 793"sysvars_pairtie", 794`nwfs sx ��� s SUBMAP sx ��� 795 (nwalk s t1 = nPair t1a t1d) ��� 796 (nwalk s t2 = nPair t2a t2d) ��� 797 (nwalk s t1a = Tie a1 c1) ��� 798 (nwalk s t2a = Tie a2 c2) ��� 799 sysvars sx c1 c2 SUBSET sysvars s t1a t2a ��� 800 sysvars sx t1d t2d SUBSET sysvars s t1 t2`, 801STRIP_TAC THEN IMP_RES_TAC nwfs_SUBMAP THEN 802SRW_TAC [][sysvars_def] THENL [ 803 Cases_on `t1` THEN FULL_SIMP_TAC (srw_ss()) [] THEN 804 METIS_TAC (lem4::met1), 805 Cases_on `t2` THEN FULL_SIMP_TAC (srw_ss()) [] THEN 806 METIS_TAC (lem4::met1), 807 `sysvars s t1a t2a SUBSET sysvars s t1 t2` 808 by METIS_TAC[ sysvars_SUBSET_pairs] THEN 809 FULL_SIMP_TAC (srw_ss()) [sysvars_def] THEN 810 MATCH_MP_TAC lem THEN 811 MAP_EVERY Q.EXISTS_TAC [`nvars t1a`,`nvars t2a`,`FDOM s UNION BIGUNION (FRANGE (nvars o_f s))`] THEN 812 SRW_TAC [][] THEN METIS_TAC [UNION_ASSOC], 813 `sysvars s t1a t2a SUBSET sysvars s t1 t2` 814 by METIS_TAC[ sysvars_SUBSET_pairs] THEN 815 FULL_SIMP_TAC (srw_ss()) [sysvars_def] THEN 816 MATCH_MP_TAC lem THEN 817 MAP_EVERY Q.EXISTS_TAC [`nvars t1a`,`nvars t2a`,`FDOM s UNION BIGUNION (FRANGE (nvars o_f s))`] THEN 818 SRW_TAC [][] THEN METIS_TAC [UNION_ASSOC] 819]) 820 821val tcd_thm = Q.store_thm( 822"tcd_thm", 823`nwfs (FST p) /\ 824 (nwalk (FST p) t1 = nPair t1a t1d) /\ 825 (nwalk (FST p) t2 = nPair t2a t2d) /\ 826 (ntunify_tupled_aux uR (p,t1a,t2a) = SOME px) ==> 827 uR (px,t1d,t2d) (p,t1,t2)`, 828MAP_EVERY Cases_on [`p`,`px`] THEN SRW_TAC [][] THEN 829METIS_TAC [aux_uP, uP_IMP_subpair_uR]) 830 831val [tctie_thm,tcd_thm,tca_thm] = map ((SIMP_RULE (srw_ss()) [FORALL_PROD]) o GEN_ALL) [tctie_thm,tcd_thm,tca_thm] 832 833val (ntunify_def,ntunify_ind) = Defn.tprove ( 834ntunify_defn, 835WF_REL_TAC `uR` THEN 836SRW_TAC [][WF_uR] THENL [ 837 SRW_TAC [][tctie_thm], 838 METIS_TAC [pmact_nil,tctie_thm], 839 SRW_TAC [][tcd_thm], 840 SRW_TAC [][tca_thm] 841]) 842 843val aux_eqn = 844hd(Defn.eqns_of ntunify_aux_defn) |> 845Q.INST[`R`|->`uR`] |> 846PROVE_HYP WF_uR |> 847(fn th => PROVE_HYP (prove(hd(hyp th),SRW_TAC[][tctie_thm])) th) |> 848(fn th => PROVE_HYP (prove(hd(hyp th),SRW_TAC[][] THEN METIS_TAC[pmact_nil,tctie_thm,PAIR])) th) |> 849(fn th => PROVE_HYP (prove(hd(hyp th),SRW_TAC[][tcd_thm])) th) |> 850(fn th => PROVE_HYP (prove(hd(hyp th),SRW_TAC[][tca_thm])) th); 851 852Theorem aux_eq_ntunify: 853 !s fe t1 t2. ntunify_tupled_aux uR ((s,fe),t1,t2) = ntunify (s,fe) t1 t2 854Proof 855HO_MATCH_MP_TAC ntunify_ind THEN 856REPEAT STRIP_TAC THEN 857FULL_SIMP_TAC (srw_ss()) [] THEN 858reverse (SRW_TAC [][Once aux_eqn]) 859>- simp[Once ntunify_def] >> 860SRW_TAC [][Once ntunify_def,SimpRHS] THEN 861Cases_on `nwalk s t1` THEN Cases_on `nwalk s t2` THEN 862SRW_TAC [][] THENL [ 863 Q.MATCH_ASSUM_RENAME_TAC `nwalk q t2 = Tie a2 c2` THEN 864 Cases_on `term_fcs s' (nwalk* q c2)` THEN SRW_TAC [][], 865 Q.MATCH_ASSUM_RENAME_TAC `nwalk q t1 = nPair t1a t1d` THEN 866 Q.MATCH_ASSUM_RENAME_TAC `nwalk q t2 = nPair t2a t2d` THEN 867 Cases_on `ntunify (q,fe) t1a t2a` THEN SRW_TAC [][UNCURRY] 868] 869QED 870 871val nunify_exists = prove( 872``���nunify.���s fe t1 t2. nwfs s ��� (nunify (s,fe) t1 t2 = 873 case (nwalk s t1, nwalk s t2) 874 of (Nom a1, Nom a2) => if a1 = a2 then SOME (s,fe) else NONE 875 | (Sus pi1 v1, Sus pi2 v2) => 876 if v1 = v2 877 then unify_eq_vars (dis_set pi1 pi2) v1 (s,fe) 878 else add_bdg pi1 v1 (Sus pi2 v2) (s,fe) 879 | (Sus pi1 v1, t2) => add_bdg pi1 v1 t2 (s,fe) 880 | (t1, Sus pi2 v2) => add_bdg pi2 v2 t1 (s,fe) 881 | (Tie a1 t1, Tie a2 t2) => 882 if a1 = a2 then nunify (s,fe) t1 t2 883 else do fcs <- term_fcs a1 (nwalk* s t2); 884 nunify (s, fe UNION fcs) t1 (apply_pi [(a1,a2)] t2) 885 od 886 | (nPair t1a t1d, nPair t2a t2d) => 887 do (sx,fex) <- nunify (s,fe) t1a t2a; 888 nunify (sx,fex) t1d t2d 889 od 890 | (nConst c1, nConst c2) => if c1 = c2 then SOME (s,fe) else NONE 891 | _ => NONE)``, 892Q.EXISTS_TAC `ntunify` THEN 893SRW_TAC [][Once ntunify_def,SimpLHS] THEN 894Cases_on `nwalk s t1` THEN Cases_on `nwalk s t2` THEN 895SRW_TAC [][]); 896 897val nunify_def = new_specification("nunify_def",["nunify"],nunify_exists); 898 899val nunify_eq_ntunify = Q.store_thm( 900"nunify_eq_ntunify", 901`!s fe t1 t2. nwfs (FST (s,fe)) ==> (nunify (s,fe) t1 t2 = ntunify (s,fe) t1 t2)`, 902HO_MATCH_MP_TAC ntunify_ind THEN 903REPEAT STRIP_TAC THEN 904FULL_SIMP_TAC (srw_ss()) [] THEN 905SRW_TAC [][Once ntunify_def,SimpRHS] THEN 906SRW_TAC [][Once nunify_def,SimpLHS] THEN 907Cases_on `nwalk s t1` THEN Cases_on `nwalk s t2` THEN 908SRW_TAC [][] THENL [ 909 Q.MATCH_ASSUM_RENAME_TAC `nwalk s t2 = Tie a2 c2` THEN 910 Cases_on `term_fcs s' (nwalk* s c2)` THEN SRW_TAC [][], 911 Q.MATCH_ASSUM_RENAME_TAC `nwalk s t1 = nPair t1a t1d` THEN 912 Q.MATCH_ASSUM_RENAME_TAC `nwalk s t2 = nPair t2a t2d` THEN 913 Cases_on `ntunify (s,fe) t1a t2a` THEN SRW_TAC [][] THEN 914 `nwfs (FST x)` by METIS_TAC [aux_eq_ntunify,uP_def,aux_uP,PAIR] THEN 915 SRW_TAC [][UNCURRY] 916]); 917 918val _ = Q.store_thm( 919"nunify_uP", 920`nwfs s /\ (nunify (s,fe) t1 t2 = SOME (sx,fex)) ==> 921 uP sx s t1 t2`, 922METIS_TAC [FST,nunify_eq_ntunify,aux_eq_ntunify,aux_uP]); 923 924val _ = save_thm ("nunify_ind", 925ntunify_ind |> 926SIMP_RULE (srw_ss()) [GSYM nunify_eq_ntunify,GSYM AND_IMP_INTRO] |> 927Q.SPEC `UNCURRY P` |> SIMP_RULE (srw_ss()) [AND_IMP_INTRO] |> Q.GEN `P`); 928 929val verify_fcs = Define` 930 verify_fcs fcs s = ITSET (fcs_acc s) fcs (SOME {})`; 931 932val nomunify_def = Define` 933 nomunify (s,fe) t1 t2 = 934 do (sx,feu) <- nunify (s,fe) t1 t2; 935 fex <- verify_fcs feu sx; 936 SOME (sx,fex) 937 od`; 938 939val _ = export_theory (); 940