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