1open HolKernel boolLib bossLib ramanaLib Parse stringTheory arithmeticTheory finite_mapTheory pred_setTheory bagTheory pairTheory termTheory relationTheory prim_recTheory unifDefTheory substTheory walkTheory walkstarTheory 2 3val _ = new_theory "unifProps" 4val _ = metisTools.limit := { time = NONE, infs = SOME 5000 } 5 6val vwalk_irrelevant_FUPDATE = Q.store_thm( 7"vwalk_irrelevant_FUPDATE", 8`wfs (s|+(vx,tx)) /\ vx NOTIN FDOM s ==> 9 !v.~(vR s)^* vx v ==> (vwalk (s|+(vx,tx)) v = vwalk s v)`, 10STRIP_TAC THEN 11`wfs s` by METIS_TAC [wfs_SUBMAP,SUBMAP_FUPDATE_EQN] THEN 12HO_MATCH_MP_TAC vwalk_ind THEN 13SRW_TAC [][] THEN 14`vx <> v` by METIS_TAC [RTC_REFL] THEN 15Cases_on `FLOOKUP s v` THENL [ 16 `v NOTIN FDOM s /\ v NOTIN FDOM (s|+(vx,tx))` 17 by (POP_ASSUM MP_TAC THEN SRW_TAC [][FLOOKUP_DEF]) THEN 18 METIS_TAC [DISCH_ALL NOT_FDOM_vwalk,term_11], 19 Cases_on `x` THEN FULL_SIMP_TAC (srw_ss()) [] THENL [ 20 `vR s n v` by FULL_SIMP_TAC (srw_ss()) [vR_def] THEN 21 `~(vR s)^* vx n` 22 by METIS_TAC [RTC_SUBSET,RTC_TRANSITIVE,transitive_def] THEN 23 FULL_SIMP_TAC (srw_ss()) [] THEN 24 SRW_TAC [][Once vwalk_def,SimpLHS,FLOOKUP_UPDATE] THEN 25 SRW_TAC [][Once vwalk_def,SimpRHS], 26 SRW_TAC [][Once vwalk_def,SimpLHS,FLOOKUP_UPDATE] THEN 27 SRW_TAC [][Once vwalk_def,SimpRHS], 28 SRW_TAC [][Once vwalk_def,SimpLHS,FLOOKUP_UPDATE] THEN 29 SRW_TAC [][Once vwalk_def,SimpRHS] 30 ] 31]); 32 33val vR_SUBMAP = Q.prove( 34`s SUBMAP sx ==> vR s u v ==> vR sx u v`, 35Cases_on `FLOOKUP s v` THEN 36SRW_TAC [][vR_def] THEN 37`FLOOKUP sx v = SOME x` by METIS_TAC [FLOOKUP_SUBMAP] THEN 38SRW_TAC [][]); 39 40val TC_vR_SUBMAP = Q.store_thm( 41"TC_vR_SUBMAP", 42`s SUBMAP sx ==> !u v.(vR s)^+ u v ==> (vR sx)^+ u v`, 43STRIP_TAC THEN HO_MATCH_MP_TAC TC_INDUCT THEN 44SRW_TAC [][] THEN1 METIS_TAC [TC_SUBSET,vR_SUBMAP] THEN 45METIS_TAC [TC_RULES]); 46 47val vwalk_FUPDATE_var = Q.store_thm( 48"vwalk_FUPDATE_var", 49`wfs (s|+(v1,Var v2)) /\ v1 NOTIN FDOM s ==> 50 (vwalk (s|+(v1,Var v2)) v2 = vwalk s v2)`, 51SRW_TAC [][] THEN 52Q_TAC SUFF_TAC `~(vR s)^* v1 v2` 53 THEN1 METIS_TAC [vwalk_irrelevant_FUPDATE] THEN 54SRW_TAC [][RTC_CASES_TC] THENL [ 55 SPOSE_NOT_THEN STRIP_ASSUME_TAC THEN 56 `vR (s|+(v1,Var v2)) v1 v1` by SRW_TAC [] [vR_def,FLOOKUP_UPDATE] THEN 57 METIS_TAC [wfs_no_cycles,TC_SUBSET], 58 `s SUBMAP (s|+(v1,Var v2))` by METIS_TAC [SUBMAP_FUPDATE_EQN] THEN 59 Q.PAT_X_ASSUM `wfs Z` MP_TAC THEN 60 SRW_TAC [][wfs_no_cycles] THEN 61 POP_ASSUM (Q.SPEC_THEN `v2` MP_TAC) THEN 62 SPOSE_NOT_THEN STRIP_ASSUME_TAC THEN 63 `(vR (s|+(v1,Var v2)))^+ v1 v2` by METIS_TAC [TC_vR_SUBMAP] THEN 64 `vR (s|+(v1,Var v2)) v2 v1` by SRW_TAC [][vR_def,FLOOKUP_UPDATE] THEN 65 METIS_TAC [TC_RULES] 66]); 67 68val walkstar_extend = Q.store_thm( 69"walkstar_extend", 70`wfs s1 /\ wfs (s|+(vx,tx)) /\ vx NOTIN FDOM s /\ 71 (walkstar s1 (Var vx) = walkstar s1 (walkstar s tx)) ==> 72 !t.(walkstar s1 (walkstar (s|+(vx,tx)) t) = walkstar s1 (walkstar s t))`, 73STRIP_TAC THEN 74`s SUBMAP (s|+(vx,tx)) /\ wfs s` by METIS_TAC [wfs_SUBMAP,SUBMAP_FUPDATE_EQN] THEN 75HO_MATCH_MP_TAC (Q.INST[`s`|->`s|+(vx,tx)`]walkstar_ind) THEN 76SRW_TAC [][] THEN 77Cases_on `t` THEN SRW_TAC [][] THEN 78Q.SPECL_THEN [`n`,`s`] MP_TAC 79 (Q.INST[`sx`|->`s|+(vx,tx)`] (UNDISCH vwalk_SUBMAP)) THEN 80Cases_on `vwalk s n` THEN SRW_TAC [][] THEN 81Q.PAT_X_ASSUM `!v5 v6.Z` MP_TAC THEN 82Cases_on `vwalk (s|+(vx,tx)) n'` THEN 83SRW_TAC [][] THENL [ 84 Cases_on `n' = vx` THENL [ 85 Q.PAT_X_ASSUM `vwalk (s|+(vx,tx)) n' = Var n''` MP_TAC THEN 86 SRW_TAC [][Once(DISCH_ALL vwalk_def),SimpLHS,FLOOKUP_UPDATE] THEN 87 POP_ASSUM MP_TAC THEN 88 Cases_on `tx` THEN SRW_TAC [][] THEN 89 `vwalk s n''' = Var n''` by METIS_TAC [vwalk_FUPDATE_var] THEN 90 Q.PAT_X_ASSUM `walkstar s1 X = walkstar s1 Y` MP_TAC THEN 91 SRW_TAC [][NOT_FDOM_vwalk], 92 `n' NOTIN FDOM s` by METIS_TAC [vwalk_to_var] THEN 93 Q.PAT_X_ASSUM `vwalk (s|+(vx,tx)) n' = Var n''` MP_TAC THEN 94 SRW_TAC [][Once(DISCH_ALL vwalk_def),SimpLHS,FLOOKUP_UPDATE,FLOOKUP_DEF] 95 ], 96 `walkstar s (Var vx) = Var vx` by SRW_TAC [][NOT_FDOM_vwalk] THEN 97 `n' NOTIN FDOM s` by METIS_TAC [vwalk_to_var] THEN 98 `n' = vx` 99 by (Q.PAT_X_ASSUM `vwalk (s|+(vx,tx)) n' = Z` MP_TAC THEN 100 SRW_TAC [][Once(DISCH_ALL vwalk_def),SimpLHS, 101 FLOOKUP_UPDATE,FLOOKUP_DEF]) THEN 102 Q.PAT_X_ASSUM `vwalk (s|+(vx,tx)) n' = Z` MP_TAC THEN 103 SRW_TAC [][Once(DISCH_ALL vwalk_def),SimpLHS,FLOOKUP_UPDATE] THEN 104 FULL_SIMP_TAC (srw_ss()) [] THEN 105 POP_ASSUM MP_TAC THEN 106 Cases_on `tx` THEN SRW_TAC [][] THEN 107 Q.PAT_X_ASSUM `walkstar s1 (Var X) = walkstar s1 Y` MP_TAC 108 THEN SRW_TAC [][] THEN 109 `vwalk s n'' = Pair t t0` by METIS_TAC [vwalk_FUPDATE_var] THEN 110 SRW_TAC [][], 111 `walkstar s (Var vx) = Var vx` by SRW_TAC [][NOT_FDOM_vwalk] THEN 112 `n' NOTIN FDOM s` by METIS_TAC [vwalk_to_var] THEN 113 `n' = vx` 114 by (Q.PAT_X_ASSUM `vwalk (s|+(vx,tx)) n' = Z` MP_TAC THEN 115 SRW_TAC [][Once(DISCH_ALL vwalk_def),SimpLHS, 116 FLOOKUP_UPDATE,FLOOKUP_DEF]) THEN 117 Q.PAT_X_ASSUM `vwalk (s|+(vx,tx)) n' = Z` MP_TAC THEN 118 SRW_TAC [][Once(DISCH_ALL vwalk_def),SimpLHS,FLOOKUP_UPDATE] THEN 119 FULL_SIMP_TAC (srw_ss()) [] THEN 120 POP_ASSUM MP_TAC THEN 121 Cases_on `tx` THEN SRW_TAC [][] THEN 122 Q.PAT_X_ASSUM `walkstar s1 (Var X) = walkstar s1 Y` MP_TAC 123 THEN SRW_TAC [][] THEN 124 Q.MATCH_ASSUM_RENAME_TAC `vwalk _ n'' = Const c` THEN 125 `vwalk s n'' = Const c` by METIS_TAC [vwalk_FUPDATE_var] THEN 126 Q.SPECL_THEN [`n''`,`s`] MP_TAC 127 (Q.INST[`sx`|->`s1`] (UNDISCH vwalk_SUBMAP)) THEN 128 SRW_TAC [][] 129]); 130 131val unify_same_lemma = prove( 132 ``���s t1 t2. wfs s ��� (t1 = t2) ��� (unify s t1 t2 = SOME s)``, 133 ho_match_mp_tac unify_ind >> rw[] >> 134 pop_assum mp_tac >> 135 simp_tac std_ss [Once unify_def] >> 136 Cases_on `walk s t1` >> rw[]) 137val unify_same = store_thm("unify_same", 138 ``���s. wfs s ��� ���t. unify s t t = SOME s``, 139 PROVE_TAC[unify_same_lemma]) 140val _ = export_rewrites["unify_same"] 141 142val wex = Q.prove( 143`wfs s1 /\ wfs (s|+(vx,tx)) /\ 144 (walkstar s1 (walk* s (Var vx)) = walkstar s1 (walkstar s tx)) /\ vx NOTIN FDOM s 145 ==> !t.(walkstar s1 (walkstar (s|+(vx,tx)) t) = walkstar s1 (walkstar s t))`, 146STRIP_TAC THEN 147`wfs s` by METIS_TAC [wfs_SUBMAP,SUBMAP_FUPDATE_EQN] THEN 148FULL_SIMP_TAC (srw_ss()) [NOT_FDOM_vwalk] THEN 149METIS_TAC [walkstar_extend]) 150 151val unify_mgu = Q.store_thm( 152"unify_mgu", 153`!s t1 t2 sx s2. wfs s ��� (unify s t1 t2 = SOME sx) ��� 154 wfs s2 /\ (walk* s2 (walk* s t1) = walk* s2 (walk* s t2)) ==> 155 !t.(walk* s2 (walk* sx t) = walk* s2 (walk* s t))`, 156HO_MATCH_MP_TAC unify_ind THEN SRW_TAC [][] THEN 157`wfs sx` by METIS_TAC [unify_uP,uP_def] THEN 158Cases_on `walk s t1` THEN Cases_on `walk s t2` THEN 159Q.PAT_X_ASSUM `unify X Y Z = D` MP_TAC THEN 160SRW_TAC [][Once unify_def] THENL [ 161 METIS_TAC [walkstar_walk,wex,walk_to_var], 162 METIS_TAC [walkstar_walk,wex,walk_to_var], 163 METIS_TAC [walkstar_walk,wex,walk_to_var], 164 METIS_TAC [walkstar_walk,wex,walk_to_var], 165 `walk* s2 (walk* s (walk s t1)) = walk* s2 (walk* s (walk s t2))` 166 by METIS_TAC [walkstar_walk] THEN 167 Cases_on `unify s t' t''` THEN FULL_SIMP_TAC (srw_ss()) [] THEN 168 `wfs x` by METIS_TAC [unify_uP,uP_def] THEN SRW_TAC [][] THEN 169 MAP_EVERY (fn x => Q.PAT_X_ASSUM x ASSUME_TAC) 170 [`wfs s`,`unify x Y Z = SOME sx`,`wfs s2`,`walk s t1 = X`,`walk s t2 = X`] THEN 171 FULL_SIMP_TAC (srw_ss()) [], 172 METIS_TAC [walkstar_walk,wex,walk_to_var] 173]) 174 175val unify_mgu_FEMPTY = Q.store_thm( 176"unify_mgu_FEMPTY", 177`(unify FEMPTY t1 t2 = SOME sx) ==> 178 !s.wfs s /\ (walkstar s t1 = walkstar s t2) ==> 179 ?s'.!t.(walkstar s' (walkstar sx t) = walkstar s t)`, 180METIS_TAC [unify_mgu,wfs_FEMPTY,walkstar_FEMPTY]) 181 182val walkstar_walk_SUBMAP = Q.store_thm( 183"walkstar_walk_SUBMAP", 184`s SUBMAP sx /\ wfs sx ==> 185 (walkstar sx t = walkstar sx (walk s t))`, 186METIS_TAC [walkstar_SUBMAP,walkstar_walk,wfs_SUBMAP]) 187 188val unify_unifier = Q.store_thm( 189"unify_unifier", 190`wfs s ��� (unify s t1 t2 = SOME sx) ��� 191 wfs sx ��� s SUBMAP sx ��� (walk* sx t1 = walk* sx t2)`, 192Q_TAC SUFF_TAC 193`!s t1 t2 sx.wfs s /\ (unify s t1 t2 = SOME sx) ==> 194 wfs sx ��� s SUBMAP sx ��� (walk* sx t1 = (walk* sx t2))` 195THEN1 METIS_TAC [] THEN 196HO_MATCH_MP_TAC unify_ind THEN SRW_TAC [][] THEN 197`wfs sx /\ s SUBMAP sx` by METIS_TAC [unify_uP,uP_def] THEN 198Q.PAT_X_ASSUM `unify s t1 t2 = SOME sx` MP_TAC THEN 199Cases_on `walk s t1` THEN Cases_on `walk s t2` THEN 200SRW_TAC [][Once unify_def] THENL [ 201 Cases_on `t1` THEN Cases_on `t2` THEN 202 FULL_SIMP_TAC (srw_ss()) [walk_def], 203 Q.MATCH_ABBREV_TAC `walkstar sx t1 = walkstar sx t2` THEN 204 `(walkstar sx t1 = walkstar sx (walk s t1)) /\ 205 (walkstar sx t2 = walkstar sx (walk s t2))` 206 by METIS_TAC [walkstar_walk_SUBMAP] THEN 207 MP_TAC (Q.INST[`t`|->`t1`]walk_SUBMAP) THEN 208 MP_TAC (Q.INST[`t`|->`t2`]walk_SUBMAP) THEN 209 Q.UNABBREV_TAC `sx` THEN 210 REPEAT(SRW_TAC [][Once vwalk_def,FLOOKUP_UPDATE]), 211 Q.MATCH_ABBREV_TAC `walkstar sx t1 = walkstar sx t2` THEN 212 `(walkstar sx t1 = walkstar sx (walk s t1)) /\ 213 (walkstar sx t2 = walkstar sx (walk s t2))` 214 by METIS_TAC [walkstar_walk_SUBMAP] THEN 215 MP_TAC (Q.INST[`t`|->`t1`]walk_SUBMAP) THEN 216 MP_TAC (Q.INST[`t`|->`t2`]walk_SUBMAP) THEN 217 Q.UNABBREV_TAC `sx` THEN 218 REPEAT(SRW_TAC [][Once vwalk_def,FLOOKUP_UPDATE]), 219 Q.MATCH_ABBREV_TAC `walkstar sx t1 = walkstar sx t2` THEN 220 `(walkstar sx t1 = walkstar sx (walk s t1)) /\ 221 (walkstar sx t2 = walkstar sx (walk s t2))` 222 by METIS_TAC [walkstar_walk_SUBMAP] THEN 223 MP_TAC (Q.INST[`t`|->`t1`]walk_SUBMAP) THEN 224 MP_TAC (Q.INST[`t`|->`t2`]walk_SUBMAP) THEN 225 Q.UNABBREV_TAC `sx` THEN 226 REPEAT(SRW_TAC [][Once(DISCH_ALL vwalk_def),FLOOKUP_UPDATE]), 227 Q.MATCH_ABBREV_TAC `walkstar sx t1 = walkstar sx t2` THEN 228 `(walkstar sx t1 = walkstar sx (walk s t1)) /\ 229 (walkstar sx t2 = walkstar sx (walk s t2))` 230 by METIS_TAC [walkstar_walk_SUBMAP] THEN 231 MP_TAC (Q.INST[`t`|->`t1`]walk_SUBMAP) THEN 232 MP_TAC (Q.INST[`t`|->`t2`]walk_SUBMAP) THEN 233 Q.UNABBREV_TAC `sx` THEN 234 REPEAT(SRW_TAC [][Once(DISCH_ALL vwalk_def),FLOOKUP_UPDATE]), 235 `(walkstar sx t1 = walkstar sx (walk s t1)) /\ 236 (walkstar sx t2 = walkstar sx (walk s t2))` 237 by METIS_TAC [walkstar_walk_SUBMAP] THEN 238 Cases_on `unify s t t'` THEN 239 FULL_SIMP_TAC (srw_ss()) [] THEN 240 `wfs x /\ x SUBMAP sx` by METIS_TAC [unify_uP,uP_def] THEN 241 FULL_SIMP_TAC (srw_ss()) [] THEN 242 METIS_TAC [walkstar_SUBMAP], 243 Q.MATCH_ABBREV_TAC `walkstar sx t1 = walkstar sx t2` THEN 244 `(walkstar sx t1 = walkstar sx (walk s t1)) /\ 245 (walkstar sx t2 = walkstar sx (walk s t2))` 246 by METIS_TAC [walkstar_walk_SUBMAP] THEN 247 MP_TAC (Q.INST[`t`|->`t1`]walk_SUBMAP) THEN 248 MP_TAC (Q.INST[`t`|->`t2`]walk_SUBMAP) THEN 249 Q.UNABBREV_TAC `sx` THEN 250 REPEAT(SRW_TAC [][Once(DISCH_ALL vwalk_def),FLOOKUP_UPDATE]), 251 Cases_on `t1` THEN Cases_on `t2` THEN 252 FULL_SIMP_TAC (srw_ss()) [walk_def] 253]) 254 255val walk_to_var_NOT_FDOM = Q.prove( 256`wfs s ��� (walk s t = Var v) ��� v ��� FDOM s`, 257METIS_TAC [walk_to_var]) 258 259val vars_measure = Q.store_thm( 260"vars_measure", 261`v ��� vars t ��� (���w. t ��� Var w) ��� wfs s ��� 262 measure (pair_count o (walk* s)) (Var v) t`, 263Induct_on `t` THEN SRW_TAC [][] THEN 264Q.MATCH_ASSUM_RENAME_TAC `v ��� vars tt` THEN 265Q.PAT_X_ASSUM `wfs s` ASSUME_TAC THEN 266Cases_on `tt` THEN FULL_SIMP_TAC (srw_ss()) [] THEN 267FULL_SIMP_TAC (srw_ss()++ARITH_ss) [measure_thm]) 268 269val oc_subterm_neq = Q.store_thm( 270"oc_subterm_neq", 271`oc s t v ��� (���w. t ��� Var w) ��� wfs s ��� wfs s2 ��� 272 walk* s2 (Var v) ��� walk* s2 (walk* s t)`, 273STRIP_TAC THEN 274`v ��� vars (walk* s t)` by METIS_TAC [oc_eq_vars_walkstar,IN_DEF] THEN 275`���w. (walk* s t) ��� Var w` by (Cases_on `t` THEN FULL_SIMP_TAC (srw_ss()) []) THEN 276IMP_RES_TAC vars_measure THEN 277SPOSE_NOT_THEN STRIP_ASSUME_TAC THEN 278FULL_SIMP_TAC (srw_ss()) [measure_thm]) 279 280val eqs_unify = Q.store_thm( 281"eqs_unify", 282`wfs s ��� wfs s2 ��� (walk* s2 (walk* s t1) = walk* s2 (walk* s t2)) ��� 283 ���sx. unify s t1 t2 = SOME sx`, 284Q_TAC SUFF_TAC 285`���s t1 t2. wfs s ��� wfs s2 ��� (walk* s2 (walk* s t1) = walk* s2 (walk* s t2)) ��� 286 ���sx. unify s t1 t2 = SOME sx` THEN1 METIS_TAC [] THEN 287HO_MATCH_MP_TAC unify_ind THEN SRW_TAC [][] THEN 288`(walk* s t1 = walk* s (walk s t1)) ��� 289 (walk* s t2 = walk* s (walk s t2))` 290by METIS_TAC [walkstar_walk] THEN 291MAP_EVERY Cases_on [`walk s t1`,`walk s t2`] THEN 292Q.PAT_X_ASSUM `wfs s2` ASSUME_TAC THEN 293Q.PAT_X_ASSUM `wfs s` ASSUME_TAC THEN 294IMP_RES_TAC walk_to_var_NOT_FDOM THEN 295FULL_SIMP_TAC (srw_ss()) [NOT_FDOM_vwalk] THEN 296ASM_SIMP_TAC (srw_ss()) [Once unify_def] THEN1 ( 297 Q.MATCH_ASSUM_RENAME_TAC `walk s _ = Pair c1 c2` THEN 298 (oc_subterm_neq |> CONTRAPOS |> 299 Q.INST [`v`|->`n`,`t`|->`Pair c1 c2`] |> 300 MP_TAC) THEN 301 ASM_SIMP_TAC (srw_ss()) [] ) 302THEN1 ( 303 Q.MATCH_ASSUM_RENAME_TAC `walk s _ = Pair c1 c2` THEN 304 (oc_subterm_neq |> CONTRAPOS |> 305 Q.INST [`v`|->`n`,`t`|->`Pair c1 c2`] |> 306 MP_TAC) THEN 307 ASM_SIMP_TAC (srw_ss()) [] ) 308THEN1 ( 309 FULL_SIMP_TAC (srw_ss()) [] THEN 310 `wfs sx` by METIS_TAC [unify_unifier] THEN 311 Q.MATCH_ASSUM_RENAME_TAC `walk s t1 = Pair t1a t1d` THEN 312 Q.MATCH_ASSUM_RENAME_TAC `walk s t2 = Pair t2a t2d` THEN 313 (unify_mgu |> Q.SPECL [`s`,`t1a`,`t2a`,`sx`,`s2`] |> MP_TAC) THEN 314 SRW_TAC [][] ) 315THEN1 ( 316 Cases_on `vwalk s2 n` THEN FULL_SIMP_TAC (srw_ss()) [] )) 317 318val _ = set_fixity "COMPAT" (Infix(NONASSOC,450)) 319val COMPAT_def = Define` 320 s COMPAT s0 = wfs s /\ wfs s0 /\ 321 (!t.walkstar s (walkstar s0 t) = walkstar s t)` 322val _ = TeX_notation {hol = "COMPAT", TeX = ("\\ensuremath{\\Supset}",1)} 323 324val SUBMAP_COMPAT = Q.store_thm( 325"SUBMAP_COMPAT", 326`wfs sx /\ s SUBMAP sx ==> sx COMPAT s`, 327STRIP_TAC THEN 328`wfs s` by METIS_TAC [wfs_SUBMAP] THEN 329SRW_TAC [][COMPAT_def,walkstar_SUBMAP]) 330 331val COMPAT_REFL = Q.store_thm( 332"COMPAT_REFL", 333`wfs s ==> s COMPAT s`, 334SRW_TAC [][COMPAT_def] THEN 335METIS_TAC [walkstar_idempotent]) 336 337val COMPAT_TRANS = Q.store_thm( 338"COMPAT_TRANS", 339`s2 COMPAT s1 /\ s1 COMPAT s0 ==> s2 COMPAT s0`, 340SRW_TAC [][COMPAT_def] THEN 341METIS_TAC []) 342 343val COMPAT_extend = Q.store_thm( 344"COMPAT_extend", 345`sx COMPAT s /\ wfs (s|+(vx,tx)) /\ vx NOTIN FDOM s /\ 346 (walkstar sx (Var vx) = walkstar sx tx) ==> 347 sx COMPAT (s|+(vx,tx))`, 348SRW_TAC [][COMPAT_def] THEN 349METIS_TAC [walkstar_extend]) 350 351val COMPAT_eqs_unify = Q.store_thm( 352"COMPAT_eqs_unify", 353`!s t1 t2 sx.sx COMPAT s /\ 354 (walkstar sx t1 = walkstar sx t2) ==> 355 ?si.(unify s t1 t2 = SOME si) /\ sx COMPAT si`, 356SRW_TAC [][COMPAT_def] THEN 357(eqs_unify |> Q.INST [`s2`|->`sx`] |> MP_TAC) THEN 358SRW_TAC [][] THEN 359Q.EXISTS_TAC `sx'` THEN 360SRW_TAC [][] THEN1 361METIS_TAC [unify_unifier] THEN 362(unify_mgu |> Q.SPECL [`s`,`t1`,`t2`,`sx'`,`sx`] |> MP_TAC) THEN 363SRW_TAC [][]) 364 365val COMPAT_more_specific = Q.store_thm( 366"COMPAT_more_specific", 367`(s COMPAT s0) ��� 368 wfs s ��� wfs s0 ��� 369 (���t1 t2. (walk* s0 t1 = walk* s0 t2) ��� (walk* s t1 = walk* s t2))`, 370SRW_TAC [][COMPAT_def,EQ_IMP_THM] THEN1 ( 371 FIRST_ASSUM (Q.SPEC_THEN `t1` MP_TAC) THEN 372 FIRST_X_ASSUM (Q.SPEC_THEN `t2` MP_TAC) THEN 373 SRW_TAC [][] ) THEN 374FIRST_X_ASSUM (Q.SPECL_THEN [`walk* s0 t`,`t`] MP_TAC) THEN 375SRW_TAC [][walkstar_idempotent]); 376 377val _ = export_theory (); 378