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