1open HolKernel boolLib bossLib Parse pred_setTheory relationTheory
2finite_mapTheory termTheory ramanaLib whileTheory
3prim_recTheory arithmeticTheory bagTheory listTheory;
4
5val _ = new_theory "subst";
6
7val FUNPOW_extends_mono = Q.store_thm(
8"FUNPOW_extends_mono",
9`���P f. (���x. P x ��� P (f x)) ��� P x ��� P (FUNPOW f n x)`,
10STRIP_TAC THEN Induct_on `n` THEN SRW_TAC [][FUNPOW_SUC]);
11
12val _ = type_abbrev ("subst", ``:(num |-> 'a term)``);
13
14val rangevars_def = Define`
15  rangevars s = BIGUNION (IMAGE vars (FRANGE s))`;
16
17val FINITE_rangevars = RWstore_thm(
18"FINITE_rangevars",
19`FINITE (rangevars s)`,
20SRW_TAC [][rangevars_def] THEN SRW_TAC [][]);
21
22val IN_FRANGE_rangevars = Q.store_thm(
23"IN_FRANGE_rangevars",
24`t ��� FRANGE s ��� vars t SUBSET rangevars s`,
25SRW_TAC [][rangevars_def,SUBSET_DEF] THEN METIS_TAC []);
26
27val rangevars_FUPDATE = Q.store_thm(
28"rangevars_FUPDATE",
29`v ��� FDOM s ��� (rangevars (s |+ (v,t)) = rangevars s UNION vars t)`,
30SRW_TAC [][rangevars_def,DOMSUB_NOT_IN_DOM,UNION_COMM]);
31
32val substvars_def = Define`
33  substvars s = FDOM s UNION rangevars s`;
34
35val FINITE_substvars = RWstore_thm(
36"FINITE_substvars",
37`FINITE (substvars s)`,
38SRW_TAC [][substvars_def]);
39
40val vR_def = Define`
41  vR s y x = case FLOOKUP s x of SOME t => y IN vars t | _ => F`;
42
43val wfs_def = Define`wfs s = WF (vR s)`;
44
45val wfs_FEMPTY = RWstore_thm(
46"wfs_FEMPTY",
47`wfs FEMPTY`,
48SRW_TAC [][wfs_def] THEN
49Q_TAC SUFF_TAC `vR FEMPTY = EMPTY_REL` THEN1 METIS_TAC [WF_EMPTY_REL] THEN
50SRW_TAC [][FUN_EQ_THM,vR_def]);
51
52val wfs_SUBMAP = Q.store_thm(
53"wfs_SUBMAP",
54`wfs sx /\ s SUBMAP sx ==> wfs s`,
55SRW_TAC [][wfs_def,SUBMAP_DEF] THEN
56Q_TAC SUFF_TAC `!y x.vR s y x ==> vR sx y x`
57  THEN1 METIS_TAC [WF_SUBSET] THEN
58SRW_TAC [][vR_def,FLOOKUP_DEF] THEN
59METIS_TAC []);
60
61val wfs_no_cycles = Q.store_thm(
62  "wfs_no_cycles",
63  `wfs s <=> !v. ~(vR s)^+ v v`,
64  EQ_TAC THEN1 METIS_TAC [WF_TC,wfs_def,WF_NOT_REFL] THEN
65  SRW_TAC [] [wfs_def,WF_IFF_WELLFOUNDED,wellfounded_def] THEN
66  SPOSE_NOT_THEN STRIP_ASSUME_TAC THEN
67  `!n. (f n) IN FDOM s /\ f (SUC n) IN vars (s ' (f n))` by
68    (STRIP_TAC THEN Q.PAT_X_ASSUM `!n.vR s (f (SUC n)) (f n)` (Q.SPEC_THEN `n` MP_TAC)
69     THEN FULL_SIMP_TAC (srw_ss()) [vR_def] THEN Cases_on `FLOOKUP s (f n)` THEN
70     Q.PAT_X_ASSUM `FLOOKUP s (f n) = Z` MP_TAC THEN SRW_TAC [] [FLOOKUP_DEF])
71  THEN
72  `!n m. (vR s)^+ (f (SUC (n + m))) (f n)` by
73    (REPEAT STRIP_TAC THEN Induct_on `m` THEN1
74       (SRW_TAC [] [] THEN METIS_TAC [TC_SUBSET]) THEN
75     Q.PAT_X_ASSUM `!n. f n IN FDOM s /\ Z` (Q.SPEC_THEN `SUC (n + m)` MP_TAC)
76     THEN SRW_TAC [] [] THEN
77     `(vR s) (f (SUC (SUC (n + m)))) (f (SUC (n + m)))` by METIS_TAC
78     [vR_def,FLOOKUP_DEF] THEN METIS_TAC [TC_RULES,ADD_SUC])
79  THEN
80  `?n m. f (SUC (n + m)) = f n` by
81    (`~INJ f (count (SUC (CARD (FDOM s)))) (FDOM s)`
82         by (SRW_TAC [] [PHP,CARD_COUNT,COUNT_SUC,CARD_DEF]) THEN
83     FULL_SIMP_TAC (srw_ss()) [INJ_DEF] THEN1 METIS_TAC [] THEN
84     ASSUME_TAC (Q.SPECL [`x`,`y`] LESS_LESS_CASES) THEN
85     FULL_SIMP_TAC (srw_ss()) [] THEN1 METIS_TAC [] THENL [
86       Q.EXISTS_TAC `x` THEN Q.EXISTS_TAC `y - x - 1`,
87       Q.EXISTS_TAC `y` THEN Q.EXISTS_TAC `x - y - 1`
88     ] THEN SRW_TAC [ARITH_ss] [ADD1])
89  THEN METIS_TAC []);
90
91val subst_APPLY_def = Define`
92  (subst_APPLY s (Var v) = case FLOOKUP s v of NONE => Var v | SOME t => t) /\
93  (subst_APPLY s (Pair t1 t2) = Pair (subst_APPLY s t1) (subst_APPLY s t2)) /\
94  (subst_APPLY s (Const c) = Const c)`;
95val _ = set_fixity "���" (Infixr 700);
96val _ = overload_on ("���", ``subst_APPLY``)
97val _ = export_rewrites["subst_APPLY_def"];
98
99val subst_APPLY_FAPPLY = Q.store_thm(
100"subst_APPLY_FAPPLY",
101`v IN FDOM s ==> (s ' v = s ��� (Var v))`,
102SRW_TAC [][subst_APPLY_def,FLOOKUP_DEF]);
103
104val noids_def = Define`
105  noids s = ���v. FLOOKUP s v ��� SOME (Var v)`;
106
107val subst_APPLY_id = Q.store_thm(
108"subst_APPLY_id",
109`(s ��� t = t) <=> !v.v IN (vars t) ��� v IN FDOM s ��� (s ' v = Var v)`,
110EQ_TAC THEN
111Induct_on `t` THEN SRW_TAC [][FLOOKUP_DEF] THEN
112FULL_SIMP_TAC (srw_ss()) []);
113
114val idempotent_def = Define`
115  idempotent s = !t.s ��� (s ��� t) = s ��� t`;
116
117val wfs_noids = Q.store_thm(
118"wfs_noids",
119`wfs s ��� noids s`,
120SRW_TAC [][wfs_no_cycles,noids_def] THEN
121SPOSE_NOT_THEN STRIP_ASSUME_TAC THEN
122FIRST_X_ASSUM (Q.SPEC_THEN `v` MP_TAC) THEN
123SRW_TAC [][] THEN MATCH_MP_TAC TC_SUBSET THEN
124SRW_TAC [][vR_def]);
125
126val idempotent_rangevars = Q.store_thm(
127"idempotent_rangevars",
128`idempotent s ��� noids s <=> DISJOINT (FDOM s) (rangevars s)`,
129EQ_TAC THEN1 (
130  SRW_TAC [][DISJOINT_BIGUNION,idempotent_def,noids_def,FLOOKUP_DEF,rangevars_def] THEN
131  `���v. v IN FDOM s ��� (s ' v = x)`
132  by (POP_ASSUM MP_TAC THEN SRW_TAC [][FRANGE_DEF]) THEN
133  FIRST_X_ASSUM (Q.SPEC_THEN `Var v` MP_TAC) THEN
134  SRW_TAC [][FLOOKUP_DEF] THEN
135  IMP_RES_TAC subst_APPLY_id THEN
136  SRW_TAC [][IN_DISJOINT] THEN
137  METIS_TAC [] ) THEN
138SRW_TAC [][noids_def,IN_DISJOINT,FLOOKUP_DEF,idempotent_def,subst_APPLY_id,rangevars_def] THEN1 (
139  Induct_on `t` THEN SRW_TAC [][FLOOKUP_DEF] THEN FULL_SIMP_TAC (srw_ss()) [] THEN
140  `s ' n IN FRANGE s` by (SRW_TAC [][FRANGE_DEF] THEN METIS_TAC []) THEN
141  METIS_TAC [] ) THEN
142Cases_on `v IN FDOM s` THEN SRW_TAC [][] THEN
143`s ' v IN FRANGE s` by (SRW_TAC [][FRANGE_DEF] THEN METIS_TAC []) THEN
144`v NOTIN (vars (s ' v))` by METIS_TAC [] THEN
145Cases_on `s ' v` THEN FULL_SIMP_TAC (srw_ss()) []);
146
147val wfs_FAPPLY_var = Q.store_thm(
148"wfs_FAPPLY_var",
149`wfs s ==> !v.v IN FDOM s ==> s ' v <> (Var v)`,
150SRW_TAC [][wfs_no_cycles] THEN
151`~vR s v v` by METIS_TAC [TC_SUBSET] THEN
152POP_ASSUM MP_TAC THEN
153Cases_on `s ' v` THEN
154SRW_TAC [][vR_def,FLOOKUP_DEF]);
155
156val TC_vR_vars_FRANGE = Q.store_thm(
157"TC_vR_vars_FRANGE",
158`���u v. (vR s)^+ u v ��� v IN FDOM s ��� u IN BIGUNION (IMAGE vars (FRANGE s))`,
159HO_MATCH_MP_TAC TC_STRONG_INDUCT_RIGHT1 THEN
160SRW_TAC [][vR_def] THEN1 (
161  Cases_on `FLOOKUP s v` THEN FULL_SIMP_TAC (srw_ss()) [FLOOKUP_DEF] THEN
162  Q.EXISTS_TAC `vars x` THEN SRW_TAC [][] THEN SRW_TAC [][FRANGE_DEF] THEN
163  Q.EXISTS_TAC `s ' v` THEN SRW_TAC [][] THEN
164  Q.EXISTS_TAC `v` THEN SRW_TAC [][] ) THEN
165FIRST_X_ASSUM MATCH_MP_TAC THEN
166IMP_RES_TAC TC_CASES2_E THEN
167FULL_SIMP_TAC (srw_ss()) [vR_def] THEN
168FULL_SIMP_TAC (srw_ss()) [FLOOKUP_DEF] THEN
169Cases_on `v IN FDOM s` THEN FULL_SIMP_TAC (srw_ss()) []);
170
171val wfs_idempotent = Q.store_thm(
172"wfs_idempotent",
173`idempotent s ��� noids s ��� wfs s`,
174STRIP_TAC THEN IMP_RES_TAC idempotent_rangevars THEN
175FULL_SIMP_TAC (srw_ss()) [rangevars_def] THEN
176SRW_TAC [][wfs_no_cycles] THEN
177SPOSE_NOT_THEN STRIP_ASSUME_TAC THEN
178IMP_RES_TAC TC_vR_vars_FRANGE THEN
179IMP_RES_TAC TC_CASES2_E THEN
180FULL_SIMP_TAC (srw_ss()) [vR_def,FLOOKUP_DEF] THEN
181Cases_on `v IN FDOM s` THEN FULL_SIMP_TAC (srw_ss()) [] THEN
182RES_TAC THEN SRW_TAC [][] THEN
183METIS_TAC [IN_DISJOINT]);
184
185val _ = set_fixity "s_o_s"(Infixl 740);
186
187val s_o_s_def = Define`
188  s1 s_o_s s2 = FUN_FMAP (($��� s1) o ($��� s2 o Var)) (FDOM s1 ��� FDOM s2)`;
189
190val selfapp_def = Define`
191  (selfapp s = ($��� s) o_f s)`;
192
193val selfapp_eq_iter_APPLY = Q.store_thm(
194"selfapp_eq_iter_APPLY",
195`���t. (selfapp s) ��� t = s ��� (s ��� t)`,
196Induct THEN SRW_TAC [][selfapp_def,FLOOKUP_DEF]);
197
198val FDOM_selfapp = RWstore_thm(
199"FDOM_selfapp",
200`FDOM (selfapp s) = FDOM s`,
201SRW_TAC [][selfapp_def]);
202
203val selfapp_eq_s_o_s = Q.store_thm(
204"selfapp_eq_s_o_s",
205`selfapp s = s s_o_s s`,
206SRW_TAC [][GSYM fmap_EQ,selfapp_def,s_o_s_def,FUN_FMAP_DEF,FUN_EQ_THM] THEN
207Cases_on `x ��� FDOM s` THEN SRW_TAC [][FUN_FMAP_DEF,NOT_FDOM_FAPPLY_FEMPTY,FLOOKUP_DEF]);
208
209val IN_vars_APPLY = Q.store_thm(
210"IN_vars_APPLY",
211`���t v. v IN vars (s ��� t) ��� v NOTIN FDOM s ��� v IN vars t ��� ���x. vR s v x ��� x IN vars t`,
212Induct THEN SRW_TAC [][vR_def] THEN
213SRW_TAC [][FLOOKUP_DEF] THEN EQ_TAC THEN
214FULL_SIMP_TAC (srw_ss()) [] THEN SRW_TAC [][] THEN
215SRW_TAC [][] THEN METIS_TAC []);
216
217val vR1_def = Define`
218  vR1 s y x = vR s y x ��� y NOTIN FDOM s`;
219
220val vR_selfapp = Q.store_thm(
221"vR_selfapp",
222`vR (selfapp s) = vR1 s RUNION NRC (vR s) 2`,
223SRW_TAC [][RUNION,FUN_EQ_THM,vR1_def,selfapp_def,vR_def,
224           FLOOKUP_DEF,EQ_IMP_THM] THEN
225FULL_SIMP_TAC bool_ss [TWO,ONE,NRC] THEN
226Cases_on `x' IN FDOM s` THEN
227FULL_SIMP_TAC (srw_ss()) [IN_vars_APPLY,vR_def,FLOOKUP_DEF] THEN
228METIS_TAC []);
229
230val vR1_selfapp = Q.store_thm(
231"vR1_selfapp",
232`vR1 (selfapp s) = vR1 s RUNION (vR s O vR1 s)`,
233SRW_TAC [][FUN_EQ_THM,EQ_IMP_THM,vR1_def] THEN
234FULL_SIMP_TAC (srw_ss()) [vR_selfapp,RUNION,O_DEF] THEN
235FULL_SIMP_TAC bool_ss [TWO,ONE,NRC,vR1_def] THEN METIS_TAC []);
236
237val FDOM_FUNPOW_selfapp = RWstore_thm(
238"FDOM_FUNPOW_selfapp",
239`FDOM (FUNPOW selfapp n s) = FDOM s`,
240(FUNPOW_extends_mono |> Q.ISPEC `��s'. FDOM s' = FDOM s` |>
241      SIMP_RULE (srw_ss()) [] |> MATCH_MP_TAC ) THEN
242SRW_TAC [][]);
243
244val NRC_2_IMP_TC_vR_selfapp = Q.store_thm(
245"NRC_2_IMP_TC_vR_selfapp",
246`���n v u. NRC (vR s) (2* SUC n) v u ��� (vR (selfapp s))^+ v u`,
247Induct THEN SRW_TAC [][] THEN1 (
248  MATCH_MP_TAC TC_SUBSET THEN
249  SRW_TAC [][vR_selfapp,RUNION] ) THEN
250Cases_on `2 * SUC (SUC n)` THEN
251FULL_SIMP_TAC (srw_ss()++ARITH_ss) [NRC_SUC_RECURSE_LEFT,MULT_SUC,ADD1] THEN
252Cases_on `n'` THEN
253FULL_SIMP_TAC (srw_ss()++ARITH_ss) [NRC_SUC_RECURSE_LEFT,ADD1] THEN
254`2*n + 2 = n''` by DECIDE_TAC THEN
255FULL_SIMP_TAC (srw_ss()) [] THEN
256RES_TAC THEN
257`vR (selfapp s) z' u` by (
258  SRW_TAC [][vR_selfapp,RUNION] THEN
259  SIMP_TAC bool_ss [TWO,ONE,NRC] THEN
260  METIS_TAC [] ) THEN
261METIS_TAC [TC_RULES]);
262
263val NRC_2_1_IMP_TC_vR_selfapp = Q.store_thm(
264"NRC_2_1_IMP_TC_vR_selfapp",
265`���n v u. NRC (vR s) (2 * n) v u ��� vR1 s w v ��� (vR (selfapp s))^+ w u`,
266Induct THEN SRW_TAC [][] THEN1 (
267  MATCH_MP_TAC TC_SUBSET THEN
268  SRW_TAC [][vR_selfapp,RUNION] ) THEN
269Cases_on `2 * SUC n` THEN
270FULL_SIMP_TAC (srw_ss()++ARITH_ss) [NRC_SUC_RECURSE_LEFT,ADD1] THEN
271Cases_on `n'` THEN
272FULL_SIMP_TAC (srw_ss()++ARITH_ss) [NRC_SUC_RECURSE_LEFT,ADD1] THEN
273`2*n = n''` by DECIDE_TAC THEN
274FULL_SIMP_TAC (srw_ss()) [] THEN
275RES_TAC THEN
276`vR (selfapp s) z' u` by (
277  SRW_TAC [][vR_selfapp,RUNION] THEN
278  SIMP_TAC bool_ss [TWO,ONE,NRC] THEN
279  METIS_TAC [] ) THEN
280IMP_RES_TAC TC_RULES);
281
282val TC_vR_selfapp = Q.store_thm(
283"TC_vR_selfapp",
284`(vR (selfapp s))^+ v u ��� (���n. NRC (vR s) (2 * (SUC n)) v u) ��� (���n u'. NRC (vR s) (2 * n) u' u ��� vR1 s v u')`,
285EQ_TAC THEN1 (
286  MAP_EVERY Q.ID_SPEC_TAC [`u`,`v`] THEN
287  HO_MATCH_MP_TAC TC_INDUCT THEN
288  SRW_TAC [][vR_selfapp,RUNION] THENL [
289    DISJ2_TAC THEN
290    MAP_EVERY Q.EXISTS_TAC [`0`,`u`] THEN
291    SRW_TAC [][],
292    DISJ1_TAC THEN Q.EXISTS_TAC `0` THEN
293    SRW_TAC [][],
294    IMP_RES_TAC NRC_ADD_I THEN
295    FULL_SIMP_TAC (srw_ss()++ARITH_ss) [GSYM LEFT_ADD_DISTRIB,GSYM ADD_SUC] THEN
296    METIS_TAC [],
297    Cases_on `2 * SUC n` THEN
298    FULL_SIMP_TAC (srw_ss()) [NRC_SUC_RECURSE_LEFT,vR1_def,vR_def,FLOOKUP_DEF],
299    IMP_RES_TAC NRC_ADD_I THEN
300    FULL_SIMP_TAC (srw_ss()++ARITH_ss) [GSYM LEFT_ADD_DISTRIB,GSYM ADD_SUC] THEN
301    METIS_TAC [],
302    Cases_on `2 * n` THEN
303    FULL_SIMP_TAC (srw_ss()) [NRC_SUC_RECURSE_LEFT,vR1_def,vR_def,FLOOKUP_DEF] THEN
304    SRW_TAC [][] THEN FULL_SIMP_TAC (srw_ss()) []
305  ] ) THEN
306SRW_TAC [][] THEN1
307IMP_RES_TAC NRC_2_IMP_TC_vR_selfapp THEN
308IMP_RES_TAC NRC_2_1_IMP_TC_vR_selfapp);
309
310val wfs_selfapp = Q.store_thm(
311"wfs_selfapp",
312`wfs s ��� wfs (selfapp s)`,
313SRW_TAC [][wfs_no_cycles,EQ_IMP_THM,TC_vR_selfapp] THEN
314SPOSE_NOT_THEN STRIP_ASSUME_TAC THENL [
315  Cases_on `2 * SUC n` THEN FULL_SIMP_TAC (srw_ss()) [] THEN
316  IMP_RES_TAC TC_eq_NRC THEN METIS_TAC [],
317  Cases_on `2 * n` THEN FULL_SIMP_TAC (srw_ss()) [NRC_SUC_RECURSE_LEFT] THEN
318  SRW_TAC [][] THEN
319  FULL_SIMP_TAC (srw_ss()) [vR1_def,vR_def,FLOOKUP_DEF] THEN
320  FULL_SIMP_TAC (srw_ss()) [],
321  IMP_RES_TAC TC_eq_NRC THEN
322  IMP_RES_TAC NRC_ADD_I THEN
323  FULL_SIMP_TAC (srw_ss()++ARITH_ss) [] THEN
324  METIS_TAC []
325]);
326
327val vR_LRC_ALL_DISTINCT = Q.store_thm(
328"vR_LRC_ALL_DISTINCT",
329`wfs s ��� ���ls v u. LRC (vR s) ls v u ��� ALL_DISTINCT ls`,
330STRIP_TAC THEN Induct THEN SRW_TAC [][LRC_def] THEN1 (
331  SPOSE_NOT_THEN STRIP_ASSUME_TAC THEN
332  IMP_RES_TAC LRC_MEM_right THEN
333  Cases_on `ls` THEN FULL_SIMP_TAC (srw_ss()) [LRC_def,wfs_no_cycles] THEN
334  SRW_TAC [][] THEN1 (
335    IMP_RES_TAC TC_SUBSET THEN RES_TAC) THEN
336  RES_TAC THEN
337  IMP_RES_TAC NRC_LRC THEN
338  `NRC (vR s) (LENGTH p) h z` by METIS_TAC [] THEN
339  Cases_on `p` THEN FULL_SIMP_TAC (srw_ss()) [LRC_def] THEN
340  SRW_TAC [][] THEN1 (
341    NTAC 2 (IMP_RES_TAC TC_RULES) THEN
342    RES_TAC ) THEN
343  IMP_RES_TAC TC_eq_NRC THEN
344  SRW_TAC [][] THEN
345  NTAC 2 (IMP_RES_TAC TC_RULES) THEN
346  RES_TAC) THEN RES_TAC);
347
348val vR_LRC_FDOM = Q.store_thm(
349"vR_LRC_FDOM",
350`LRC (vR s) (h::t) v u ��� MEM e t ��� e IN FDOM s`,
351SRW_TAC [][] THEN IMP_RES_TAC LRC_MEM_right THEN
352Cases_on `e IN FDOM s` THEN
353FULL_SIMP_TAC (srw_ss()) [LRC_def,vR_def,FLOOKUP_DEF]);
354
355val vR_LRC_bound = Q.store_thm(
356"vR_LRC_bound",
357`wfs s ��� LRC (vR s) ls v u ��� LENGTH ls ��� CARD (FDOM s) + 1`,
358Cases_on `ls` THEN SRW_TAC [ARITH_ss][ADD1] THEN
359IMP_RES_TAC vR_LRC_ALL_DISTINCT THEN
360IMP_RES_TAC vR_LRC_FDOM THEN
361FULL_SIMP_TAC (srw_ss()) [] THEN
362IMP_RES_TAC ALL_DISTINCT_CARD_LIST_TO_SET THEN
363`set t SUBSET FDOM s` by SRW_TAC [][SUBSET_DEF] THEN
364METIS_TAC [CARD_SUBSET,FDOM_FINITE]);
365
366val idempotent_selfapp = Q.store_thm(
367"idempotent_selfapp",
368`idempotent s ��� (selfapp s = s)`,
369SRW_TAC [][idempotent_def,EQ_IMP_THM,GSYM fmap_EQ,FUN_EQ_THM] THEN1 (
370  Cases_on `x IN FDOM s` THEN1 (
371    FIRST_X_ASSUM (Q.SPEC_THEN `Var x` MP_TAC) THEN
372    SRW_TAC [][FLOOKUP_DEF,selfapp_def] ) THEN
373  ASSUME_TAC FDOM_selfapp THEN
374  SRW_TAC [][NOT_FDOM_FAPPLY_FEMPTY] ) THEN
375Induct_on `t` THEN SRW_TAC [][] THEN
376Cases_on `n IN FDOM s` THEN SRW_TAC [][FLOOKUP_DEF] THEN
377FIRST_X_ASSUM (Q.SPEC_THEN `n` MP_TAC) THEN
378SRW_TAC [][selfapp_def,o_f_DEF]);
379
380val fixpoint_IMP_wfs = Q.store_thm(
381"fixpoint_IMP_wfs",
382`idempotent (FUNPOW selfapp n s) ��� noids (FUNPOW selfapp n s) ��� wfs s`,
383SRW_TAC [][] THEN IMP_RES_TAC wfs_idempotent THEN
384POP_ASSUM MP_TAC THEN
385REPEAT (POP_ASSUM (K ALL_TAC)) THEN
386Induct_on `n` THEN SRW_TAC [][] THEN
387FULL_SIMP_TAC (srw_ss()) [FUNPOW_SUC] THEN
388IMP_RES_TAC wfs_selfapp THEN
389RES_TAC);
390
391val idempotent_substeq = Q.store_thm(
392"idempotent_substeq",
393`($��� s1 = $��� s2) ��� (idempotent s1 ��� idempotent s2)`,
394SRW_TAC [][idempotent_def,EQ_IMP_THM]);
395
396val vR_FUNPOW_selfapp_bound = Q.store_thm(
397"vR_FUNPOW_selfapp_bound",
398`���n v u. vR (FUNPOW selfapp n s) v u ��� ���m. 1 ��� m ��� NRC (vR s) m v u ��� (v IN FDOM s ��� n ��� m)`,
399Induct THEN SRW_TAC [][] THEN1 (
400  Q.EXISTS_TAC `1` THEN SRW_TAC [][] ) THEN
401FULL_SIMP_TAC (srw_ss()) [FUNPOW_SUC,vR_selfapp,RUNION,vR1_def] THEN1 (
402  RES_TAC THEN Q.EXISTS_TAC `m` THEN SRW_TAC [][] ) THEN
403FULL_SIMP_TAC bool_ss [TWO,ONE,NRC] THEN
404RES_TAC THEN IMP_RES_TAC NRC_ADD_I THEN
405Q.EXISTS_TAC `m' + m` THEN SRW_TAC [][] THEN1
406  DECIDE_TAC THEN
407FULL_SIMP_TAC (srw_ss()) [vR_def,FLOOKUP_DEF] THEN
408Cases_on `z IN FDOM s` THEN FULL_SIMP_TAC (srw_ss()) [] THEN
409DECIDE_TAC);
410
411val idempotent_or_vR = Q.store_thm(
412"idempotent_or_vR",
413`idempotent s ��� ���u v. vR s v u ��� v IN FDOM s`,
414Cases_on `idempotent s` THEN SRW_TAC [][] THEN
415FULL_SIMP_TAC (srw_ss()) [idempotent_def] THEN
416Induct_on `t` THEN SRW_TAC [][] THENL [
417  Cases_on `FLOOKUP s n` THEN FULL_SIMP_TAC (srw_ss()) [] THEN
418  Q.EXISTS_TAC `n` THEN SRW_TAC [][vR_def] THEN
419  (subst_APPLY_id |> Q.INST [`t`|->`x`] |> EQ_IMP_RULE |> snd |>
420   CONTRAPOS |> IMP_RES_TAC) THEN
421  FULL_SIMP_TAC (srw_ss()) [] THEN METIS_TAC [],
422  METIS_TAC [],
423  METIS_TAC []
424]);
425
426val wfs_IMP_fixpoint = Q.store_thm(
427"wfs_IMP_fixpoint",
428`wfs s ��� ���n. idempotent (FUNPOW selfapp n s) ��� noids (FUNPOW selfapp n s)`,
429STRIP_TAC THEN
430`���n. wfs (FUNPOW selfapp n s)`
431by (MATCH_MP_TAC FUNPOW_extends_mono THEN
432    SRW_TAC [][Once wfs_selfapp]) THEN
433`���n. noids (FUNPOW selfapp n s)`
434by METIS_TAC [wfs_noids] THEN
435SRW_TAC [][] THEN
436SPOSE_NOT_THEN STRIP_ASSUME_TAC THEN
437`���n. ���u v. vR (FUNPOW selfapp n s) v u ��� v IN FDOM (FUNPOW selfapp n s)`
438by METIS_TAC [idempotent_or_vR] THEN
439FULL_SIMP_TAC (srw_ss()) [] THEN
440`���n. ���m v u. 1 ��� m ��� NRC (vR s) m v u ��� n ��� m`
441by METIS_TAC [vR_FUNPOW_selfapp_bound] THEN
442`���n. ���ls v u. LRC (vR s) ls v u ��� n ��� LENGTH ls`
443by METIS_TAC [NRC_LRC] THEN
444POP_ASSUM (Q.SPEC_THEN `CARD (FDOM s) + 2` STRIP_ASSUME_TAC) THEN
445IMP_RES_TAC vR_LRC_bound THEN
446DECIDE_TAC);
447
448val wfs_iff_fixpoint = Q.store_thm(
449"wfs_iff_fixpoint",
450`wfs s ��� ���n. idempotent (FUNPOW selfapp n s) ��� noids (FUNPOW selfapp n s)`,
451METIS_TAC [wfs_IMP_fixpoint,fixpoint_IMP_wfs]);
452
453(*
454val BIG_BAG_UNION_def = Define`
455  BIG_BAG_UNION sob = ��x. SIGMA (��b. b x) sob`;
456
457val BIG_BAG_UNION_EMPTY = RWstore_thm(
458"BIG_BAG_UNION_EMPTY",
459`BIG_BAG_UNION {} = {||}`,
460SRW_TAC [][BIG_BAG_UNION_def,SUM_IMAGE_THM,EMPTY_BAG,FUN_EQ_THM]);
461
462val BIG_BAG_UNION_INSERT = Q.store_thm(
463"BIG_BAG_UNION_INSERT",
464`FINITE sob ��� (BIG_BAG_UNION (b INSERT sob) = b + BIG_BAG_UNION (sob DELETE b))`,
465SRW_TAC [][BIG_BAG_UNION_def,SUM_IMAGE_THM,BAG_UNION,FUN_EQ_THM]);
466
467val FINITE_BIG_BAG_UNION = Q.store_thm(
468"FINITE_BIG_BAG_UNION",
469`���sob. FINITE sob ��� (���b. b IN sob ��� FINITE_BAG b) ��� FINITE_BAG (BIG_BAG_UNION sob)`,
470SIMP_TAC bool_ss [GSYM AND_IMP_INTRO] THEN
471HO_MATCH_MP_TAC FINITE_INDUCT THEN
472SRW_TAC [][BIG_BAG_UNION_INSERT] THEN
473FULL_SIMP_TAC (srw_ss()) [DELETE_NON_ELEMENT]);
474
475val EMPTY_BIG_BAG_UNION = Q.store_thm(
476"EMPTY_BIG_BAG_UNION",
477`FINITE sob ��� ((BIG_BAG_UNION sob = {||}) ��� (���b. b IN sob ��� (b = {||})))`,
478Q.ID_SPEC_TAC `sob` THEN HO_MATCH_MP_TAC FINITE_INDUCT THEN
479SRW_TAC [][BIG_BAG_UNION_INSERT,DELETE_NON_ELEMENT] THEN
480SRW_TAC [][EQ_IMP_THM] THEN SRW_TAC [][]);
481
482val BAG_IN_BIG_BAG_UNION = Q.store_thm(
483"BAG_IN_BIG_BAG_UNION",
484`���sob. FINITE sob ��� (e <: BIG_BAG_UNION sob ��� ���b. b IN sob ��� e <: b)`,
485HO_MATCH_MP_TAC FINITE_INDUCT THEN
486SRW_TAC [][BIG_BAG_UNION_INSERT,DELETE_NON_ELEMENT,EQ_IMP_THM] THEN
487METIS_TAC []);
488
489val IMAGE_FAPPLY_FDOM = Q.store_thm(
490"IMAGE_FAPPLY_FDOM",
491`IMAGE ($' s) (FDOM s) = FRANGE s`,
492SRW_TAC [][EXTENSION,FRANGE_DEF,EQ_IMP_THM] THEN METIS_TAC []);
493
494val rangevarb_def = Define`
495  rangevarb s = BIG_BAG_UNION (IMAGE varb (FRANGE s))`;
496
497val FINITE_rangevarb = RWstore_thm(
498"FINITE_rangevarb",
499`FINITE_BAG (rangevarb s)`,
500SRW_TAC [][rangevarb_def] THEN
501HO_MATCH_MP_TAC FINITE_BIG_BAG_UNION THEN
502SRW_TAC [][] THEN SRW_TAC [][]);
503
504val domrangevarb_def = Define`
505  domrangevarb s = BAG_FILTER (��v. v IN FDOM s) (rangevarb s)`;
506
507val BAG_FILTER_EQ_EMPTY = Q.store_thm(
508"BAG_FILTER_EQ_EMPTY",
509`(BAG_FILTER P b = {||}) ��� ���e. e <: b ��� ��P e`,
510SRW_TAC [][BAG_EXTENSION,BAG_INN_BAG_FILTER,BAG_IN,EQ_IMP_THM] THEN1 (
511  FIRST_X_ASSUM (Q.SPECL_THEN [`1`,`e`] MP_TAC)
512  THEN SRW_TAC [][] ) THEN
513FIRST_X_ASSUM (Q.SPEC_THEN `e` MP_TAC) THEN
514SRW_TAC [][] THEN
515Cases_on `n < 1` THEN1 DECIDE_TAC THEN
516(BAG_INN_LESS |> Q.SPECL [`b`,`e`,`n`,`1`] |> CONTRAPOS |> IMP_RES_TAC) THEN
517FULL_SIMP_TAC (srw_ss()) [] THEN
518`n = 1` by DECIDE_TAC THEN
519SRW_TAC [][] THEN FULL_SIMP_TAC (srw_ss()) []);
520
521val domrangevarb_idempotent = Q.store_thm(
522"domrangevarb_idempotent",
523`idempotent s ��� noids s ��� (domrangevarb s = {||})`,
524SRW_TAC []
525[idempotent_rangevars,domrangevarb_def,rangevarb_def,
526 BAG_FILTER_EQ_EMPTY,BAG_IN_BIG_BAG_UNION,EQ_IMP_THM] THEN1 (
527 IMP_RES_TAC IN_varb_vars THEN
528 RES_TAC THEN POP_ASSUM (Q.SPEC_THEN `vars x` MP_TAC) THEN
529 SRW_TAC [][DISJOINT_DEF,EXTENSION] THEN METIS_TAC [] ) THEN
530SRW_TAC [][DISJOINT_DEF,EXTENSION] THEN
531Cases_on `x' IN vars x` THEN SRW_TAC [][] THEN
532IMP_RES_TAC IN_varb_vars THEN
533RES_TAC THEN FULL_SIMP_TAC (srw_ss()) []);
534*)
535
536(*
537
538val selfapp_preserves_idempotent = Q.store_thm(
539"selfapp_preserves_idempotent",
540`idempotent s ��� noids s ��� idempotent (selfapp s) ��� noids (selfapp s)`,
541SRW_TAC [][idempotent_def,noids_def,selfapp_eq_iter_APPLY] THEN
542Cases_on `FLOOKUP (selfapp s) v` THEN
543FULL_SIMP_TAC (srw_ss()) [FLOOKUP_DEF,selfapp_def] THEN
544FIRST_X_ASSUM (Q.SPEC_THEN `Var v` MP_TAC) THEN
545SRW_TAC [][FLOOKUP_DEF] THEN
546FIRST_X_ASSUM (Q.SPEC_THEN `v` MP_TAC) THEN
547SRW_TAC [][]);
548
549this will be a consequence of wfs_IMP_fixpoint above ? ...
550val repeated_selfapp_eq_apply_ts = Q.store_thm(
551"repeated_selfapp_eq_apply_ts", MAYBE n HAS TO DEPEND ON THE TERM !!
552`���n. apply_ts s = subst_APPLY (FUNPOW selfapp n s)`,
553Q_TAC SUFF_TAC `���t.���n. apply_ts s t = (FUNPOW selfapp n s) ��� t`
554THEN1 (
555  SRW_TAC [][FUN_EQ_THM,SKOLEM_THM]
556  SKOLEM_THM
557
558FDOM s INTER BIGUNION (IMAGE vars (FRANGE s))
559
560val wfs_IMP_fixpoint = Q.store_thm(
561"wfs_IMP_fixpoint",
562`wfs s ��� ���t.���n. (FUNPOW selfapp n s) ��� t = apply_ts s t`
563
564val FUNPOW_APPLY_apply_ts = Q.store_thm(
565"FUNPOW_APPLY_apply_ts",
566`(FUNPOW ($��� s) n t = apply_ts s t) ��� m >= n ��� wfs s ���
567 (FUNPOW ($��� s) m t = apply_ts s t)`,
568Induct_on `m` THEN SRW_TAC [][] THEN1 (
569  Cases_on `n` THEN FULL_SIMP_TAC (srw_ss()++ARITH_ss) [] ) THEN
570Cases_on `SUC m = n` THEN1 SRW_TAC [][] THEN
571`m >= n` by FULL_SIMP_TAC (srw_ss()++ARITH_ss) [] THEN
572SRW_TAC [][FUNPOW_SUC] THEN
573SRW_TAC [][apply_ts_eq_walkstar,subst_APPLY_walkstar]);
574
575val FUNPOW_APPLY_pair = Q.store_thm(
576"FUNPOW_APPLY_pair",
577`FUNPOW ($��� s) n (Pair t1 t2) = Pair (FUNPOW ($��� s) n t1) (FUNPOW ($��� s) n t2)`,
578Induct_on `n` THEN SRW_TAC [][FUNPOW_SUC] );
579
580val wfs_IMP_fixpoint = Q.store_thm(
581"wfs_IMP_fixpoint",
582`wfs s ��� ���n. idempotent (FUNPOW ($��� s) n)`
583`wfs s ��� ���t.���n. FUNPOW ($��� s) n t = apply_ts s t`,
584STRIP_TAC THEN HO_MATCH_MP_TAC apply_ts_ind THEN
585SRW_TAC [][] THEN1 (
586  Cases_on `FLOOKUP s t` THEN SRW_TAC [][] THENL [
587    Q.EXISTS_TAC `0` THEN SRW_TAC [][],
588    Q.EXISTS_TAC `SUC n` THEN SRW_TAC [][FUNPOW]
589  ] ) THEN1 (
590  SRW_TAC [][FUNPOW_APPLY_pair] THEN
591  Q.EXISTS_TAC `MAX n n'` THEN
592  SRW_TAC [][] THEN
593  MATCH_MP_TAC (GEN_ALL FUNPOW_APPLY_apply_ts) THENL [
594    Q.EXISTS_TAC `n`, Q.EXISTS_TAC `n'` ] THEN
595  SRW_TAC [ARITH_ss][MAX_DEF] ) THEN
596Q.EXISTS_TAC `0` THEN SRW_TAC [][]);
597
598val fixpoint_IMP_wfs = Q.store_thm(
599"fixpoint_IMP_wfs",
600`(���t.���n. FUNPOW ($��� s) n t = FUNPOW ($��� s) (SUC n) t) ��� noids s ��� wfs s`,
601SRW_TAC [][] THEN
602MATCH_MP_TAC wfs_idempotent THEN
603SRW_TAC [][] THEN
604SRW_TAC [][idempotent_def]
605
606SRW_TAC [][wfs_no_cycles,noids_def] THEN
607SPOSE_NOT_THEN STRIP_ASSUME_TAC THEN
608TC_vR_vars_walkstar
609FIRST_X_ASSUM (Q.SPEC_THEN `Var v` MP_TAC) THEN
610SRW_TAC [][FUNPOW] THEN
611IMP_RES_TAC TC_CASES1 THEN
612FULL_SIMP_TAC (srw_ss()) [vR_def] THEN
613Cases_on `FLOOKUP s v` THEN FULL_SIMP_TAC (srw_ss()) []
614
615val FUNPOW_APPLY_term_depth = Q.store_thm(
616"FUNPOW_APPLY_term_depth",
617`���n t. term_depth (FUNPOW ($��� s) n t) ��� term_depth (FUNPOW ($��� s) (SUC n) t)`,
618Induct THEN SRW_TAC [][] THEN1 (
619  Induct_on `t` THEN SRW_TAC [ARITH_ss][] ) THEN
620FULL_SIMP_TAC (srw_ss()) [FUNPOW]);
621
622val FUNPOW_APPLY_NOT_FDOM = Q.store_thm(
623"FUNPOW_APPLY_NOT_FDOM",
624`v NOTIN FDOM s ��� (FUNPOW ($��� s) n (Var v) = Var v)`,
625STRIP_TAC THEN Induct_on `n` THEN SRW_TAC [][FUNPOW,FLOOKUP_DEF]);
626
627val NOT_FDOM_vars_APPLY = Q.store_thm(
628"NOT_FDOM_vars_APPLY",
629`v NOTIN FDOM s ��� v IN vars t ��� v IN vars (s ��� t)`,
630Induct_on `t` THEN SRW_TAC [][FLOOKUP_DEF] THEN
631FULL_SIMP_TAC (srw_ss()) []);
632
633val term_depth_APPLY = Q.store_thm(
634"term_depth_APPLY",
635`term_depth t ��� term_depth (s ��� t)`,
636Induct_on `t` THEN SRW_TAC [ARITH_ss][]);
637
638val APPLY_subterm = Q.store_thm(
639"APPLY_subterm",
640`v IN vars t ��� t ��� Var v ��� measure term_depth (s ��� (Var v)) (s ��� t)`,
641Induct_on `t` THEN SRW_TAC [ARITH_ss][measure_thm] THEN
642Cases_on `FLOOKUP s v` THEN SRW_TAC [ARITH_ss][] THEN
643FULL_SIMP_TAC (srw_ss()) [measure_thm] THEN
644Cases_on `t` THEN FULL_SIMP_TAC (srw_ss()) []
645THEN SRW_TAC [ARITH_ss][] THEN
646Cases_on `t'` THEN FULL_SIMP_TAC (srw_ss()) []
647THEN SRW_TAC [ARITH_ss][]);
648
649val wfs_iff_fixpoint_exists = Q.store_thm(
650"wfs_iff_fixpoint_exists",
651`wfs s ��� noids s ��� ���t.���tt. OWHILE (��t. (s ��� t) ��� t) (subst_APPLY s) t = SOME tt`,
652SRW_TAC [][EQ_IMP_THM] THEN1 METIS_TAC [wfs_noids] THENL [
653  Q.EXISTS_TAC `walk* s t` THEN SRW_TAC [][OWHILE_def]
654
655val substeq_def = Define`
656  substeq s1 s2 = noids s1 ��� noids s2 ��� (���t. s1 ��� t = s2 ��� t)`;
657
658val substeq_refl = Q.store_thm(
659"substeq_refl",
660`noids s ��� substeq s s`,
661SRW_TAC [][substeq_def]);
662
663val substeq_sym = Q.store_thm(
664"substeq_sym",
665`substeq s1 s2 ��� substeq s2 s1`,
666SRW_TAC [][substeq_def]);
667
668val substeq_trans = Q.store_thm(
669"substeq_trans",
670`substeq s1 s2 ��� substeq s2 s3 ��� substeq s1 s3`,
671SRW_TAC [][substeq_def]);
672
673val vR_substeq_mono = Q.store_thm(
674"vR_substeq_mono",
675`vR s1 u v ��� substeq s1 s2 ��� vR s2 u v`,
676SRW_TAC [][vR_def,substeq_def] THEN
677Cases_on `FLOOKUP s1 v` THEN FULL_SIMP_TAC (srw_ss()) [] THEN
678FIRST_X_ASSUM (Q.SPEC_THEN `Var v` MP_TAC) THEN
679SRW_TAC [][] THEN
680Cases_on `FLOOKUP s2 v` THEN FULL_SIMP_TAC (srw_ss()) [noids_def] THEN
681METIS_TAC []);
682
683val wfs_substeq_mono = Q.store_thm(
684"wfs_substeq_mono",
685`wfs s1 ��� substeq s1 s2 ��� wfs s2`,
686SRW_TAC [][wfs_def] THEN
687Q_TAC SUFF_TAC `vR s1 = vR s2` THEN1 METIS_TAC [] THEN
688SRW_TAC [][FUN_EQ_THM,EQ_IMP_THM] THEN
689METIS_TAC [vR_substeq_mono,substeq_sym]);
690
691val wfs_noids = Q.store_thm(
692"wfs_noids",
693`wfs s ��� noids s`,
694SRW_TAC [][wfs_no_cycles,noids_def] THEN
695SPOSE_NOT_THEN STRIP_ASSUME_TAC THEN
696`vR s v v` by SRW_TAC [][vR_def] THEN
697METIS_TAC [TC_SUBSET]);
698
699val collapsable_eq_wfs = Q.store_thm(
700"collapsable_eq_wfs", FALSE
701`(���si. idempotent si ��� substeq si s) ��� wfs s`,
702SRW_TAC [][EQ_IMP_THM] THEN1 (
703  IMP_RES_TAC wfs_idempotent THEN
704  METIS_TAC [wfs_substeq_mono,substeq_def] ) THEN
705Q.EXISTS_TAC `collapse s` THEN
706IMP_RES_TAC collapse_idempotent THEN
707
708val FUNPOW_exists = Q.store_thm( (* similar to WHILE_INDUCTION *)
709"FUNPOW_exists",
710`���R. WF R ��� (���n. ��(P (FUNPOW f n x)) ��� R (FUNPOW f (SUC n) x) (FUNPOW f n x)) ��� ���n. P (FUNPOW f n x)`,
711SRW_TAC [][] THEN POP_ASSUM MP_TAC THEN Q.ID_SPEC_TAC `x` THEN
712HO_MATCH_MP_TAC (WF_INDUCTION_THM |> Q.SPEC `R` |> UNDISCH) THEN
713SRW_TAC [][] THEN
714Cases_on `P (FUNPOW f 0 x)` THEN1 METIS_TAC [] THEN
715RES_TAC THEN FULL_SIMP_TAC (srw_ss()) [] THEN RES_TAC THEN
716Q_TAC SUFF_TAC `���n. P (FUNPOW f n (f x))` THEN1 (
717  STRIP_TAC THEN Q.EXISTS_TAC `SUC n` THEN SRW_TAC [][FUNPOW] ) THEN
718POP_ASSUM MATCH_MP_TAC THEN SRW_TAC [][] THEN
719FIRST_X_ASSUM (Q.SPEC_THEN `SUC n` MP_TAC) THEN
720SRW_TAC [][FUNPOW]);
721
722val NRC_MUL_I = Q.store_thm(
723"NRC_MUL_I",
724`���m n x y. NRC (NRC R m) n x y ��� NRC R (m * n) x y`,
725Induct THEN Induct THEN SRW_TAC [][NRC] THEN1 (
726  RES_TAC THEN FULL_SIMP_TAC (srw_ss()) [] ) THEN
727RES_TAC THEN
728IMP_RES_TAC NRC_1 THEN
729IMP_RES_TAC NRC_ADD_I THEN
730Q_TAC SUFF_TAC `SUC m * SUC n = 1 + m + SUC m * n`
731THEN1 METIS_TAC [] THEN
732SRW_TAC [ARITH_ss][MULT,ADD1]);
733*)
734
735(*
736val collapsable_IMP_wfs = Q.store_thm(
737"collapsable_IMP_wfs",
738`���s.(���si. idempotent si ��� (���t. si ��� t = s ��� t)) ��� wfs s`,
739SRW_TAC [][wfs_no_cycles]
740
741val wfs_collapse = Q.store_thm(
742"wfs_collapse",
743`wfs s ==> wfs (collapse s)`,
744SIMP_TAC (srw_ss()) [wfs_no_cycles] THEN
745STRIP_TAC THEN
746Q_TAC SUFF_TAC `!v u.(vR (collapse s))^+ v u ==> v <> u`
747THEN1 METIS_TAC [] THEN
748HO_MATCH_MP_TAC TC_STRONG_INDUCT THEN
749SRW_TAC [][] THENL [
750  Cases_on `u IN FDOM (collapse s)` THEN
751  FULL_SIMP_TAC (srw_ss()) [vR_def,FLOOKUP_DEF] THEN
752  `wfs s` by METIS_TAC [wfs_no_cycles] THEN
753  `u IN FDOM s` by FULL_SIMP_TAC (srw_ss()) [collapse_def,FUN_FMAP_DEF] THEN
754  FULL_SIMP_TAC (srw_ss()) [collapse_FAPPLY_eq_walkstar]
755
756val subst_compose_exists = Q.prove(
757`!s2 s1.?comp.!x.(subst_APPLY comp x = (subst_APPLY s2 (subst_APPLY s1 x)))`,
758GEN_TAC THEN INDUCT_THEN fmap_INDUCT STRIP_ASSUME_TAC THENL [
759  Q.EXISTS_TAC `s2` THEN Induct THEN SRW_TAC [][],
760  SRW_TAC [][] THEN
761  Q.EXISTS_TAC `comp |+ (x,s2 ��� y)` THEN
762  SRW_TAC [][] THEN
763  Induct_on `x'` THEN SRW_TAC [][] THEN
764  SRW_TAC [][FLOOKUP_UPDATE] THEN
765  Q.PAT_X_ASSUM `!x.Z` (Q.SPEC_THEN `Var s` MP_TAC) THEN
766  SRW_TAC [][]
767]);
768
769val subst_compose_def = new_specification
770  ("subst_compose_def", ["subst_compose"],
771   CONV_RULE (ONCE_DEPTH_CONV SKOLEM_CONV) subst_compose_exists);
772set_fixity "oo" (Infixl 2000);
773overload_on ("oo", ``subst_compose``);
774
775val sunify_def = Define`
776  (sunify (Var x) (Var y) = SOME if x = y then FEMPTY else (FEMPTY |+ (x, Var y))) /\
777  (sunify (Var x) t2 = if x IN vars t2 then NONE else SOME (FEMPTY |+ (x,t2))) /\
778  (sunify t1 (Var y) = if y IN vars t1 then NONE else SOME (FEMPTY |+ (y,t1))) /\
779  (sunify (Pair t1a t1d) (Pair t2a t2d) =
780    case sunify t1a t2a of NONE => NONE |
781      SOME sa => case sunify t1d t2d of NONE => NONE |
782                   SOME sd => SOME (sa oo sd)) /\
783  (sunify (Const c1) (Const c2) = if c1 = c2 then SOME FEMPTY else NONE) /\
784  (sunify _ _ = NONE)`;
785
786val collapse_unify_eq_sunify = Q.store_thm(
787"collapse_unify_eq_sunify",
788`!s t1 t2 sx.wfs s /\ (unify s t1 t2 = SOME sx) ==>
789   ?ss.(sunify t1 t2 = SOME ss) /\
790       !t.((collapse sx) ��� t = (ss oo s) ��� t)`,
791HO_MATCH_MP_TAC unify_ind THEN SRW_TAC [][] THEN
792`wfs sx` by METIS_TAC [unify_uP,uP_def] THEN
793Cases_on `walk s t1` THEN Cases_on `walk s t2` THEN
794Q.PAT_X_ASSUM `unify X Y Z = D` MP_TAC THEN
795SRW_TAC [][Once unify_def] THENL
796
797`���t1 t2. (s ��� t1 = s ��� t2) ��� (t1 = t2)`,
798Induct THEN SRW_TAC [][] THENL [ false - x -> 3 and y -> 3
799  Induct_on `t2` THEN FULL_SIMP_TAC (srw_ss()) []
800Induct_on `t1` THEN SRW_TAC [][] THENL [
801  Cases_on `FLOOKUP s n` THEN FULL_SIMP_TAC (srw_ss()) [] THENL [
802    Cases_on `t2` THEN FULL_SIMP_TAC (srw_ss()) []
803
804val FUNPOW_extends_mono_cond = Q.store_thm(
805"FUNPOW_extends_mono_cond",
806`(���x y. P x y ��� Q x y ��� P (f x) (f y)) ��� ���x y. (P x y ��� Q x y ��� P (FUNPOW f n x) (FUNPOW f n y))`,
807STRIP_TAC THEN Induct_on `n` THEN SRW_TAC [][FUNPOW_SUC]
808);
809
810`���t1 t2. (��t1 t2. ���v. (t1  = Var v) ��� v IN vars t2 ��� measure term_depth t1 t2) t1 t2 ���
811(��t1 t2. ���v. (t1  = Var v) ��� v IN vars t2 ��� measure term_depth t1 t2)
812(FUNPOW ($��� s) n t1) (FUNPOW ($��� s) n t2)`,
813
814val tmp =
815FUNPOW_extends_mono |>
816Q.INST_TYPE[`:'a`|->`:term`] |>
817Q.INST[`P`|->`(��t1 t2. v IN vars t2 ��� measure term_depth t1 t2)`,
818       `f`|->`$��� s`]
819|> SIMP_RULE (srw_ss()) [] |>
820UNDISCH;
821
822val [rtp] = hyp tmp;
823val th = prove(rtp,
824Induct THEN SRW_TAC [][] THEN
825Cases_on `FLOOKUP s n` THEN SRW_TAC [][] THENL [
826  FULL_SIMP_TAC (srw_ss()) [FLOOKUP_DEF] THEN
827  METIS_TAC [NOT_FDOM_vars_APPLY],
828  FULL_SIMP_TAC (srw_ss()) [measure_thm] THEN
829  (term_depth_APPLY |> Q.GEN `t` |> Q.SPEC `y` |> MP_TAC) THEN
830  SRW_TAC [ARITH_ss][],
831
832
833`���n. v IN vars t ��� t ��� Var v ��� (measure term_depth) (FUNPOW ($��� s) n (Var v)) (FUNPOW ($��� s) n t)`,
834Induct THEN SRW_TAC [][] THEN1 (
835  Induct_on `t` THEN FULL_SIMP_TAC (srw_ss()++ARITH_ss) [measure_thm] ) THEN
836SRW_TAC [][FUNPOW] THEN
837Cases_on `FLOOKUP s v` THEN SRW_TAC [][] THEN1 (
838  FULL_SIMP_TAC (srw_ss()) [measure_thm] THEN
839  SRW_TAC [][GSYM FUNPOW] THEN
840  SRW_TAC [][FUNPOW_SUC] THEN
841  Q.MATCH_ABBREV_TAC `a < b` THEN
842  Q_TAC SUFF_TAC `term_depth (FUNPOW ($��� s) n t) ��� b` THEN1 (
843    FULL_SIMP_TAC (srw_ss()++ARITH_ss) [Abbr`a`,Abbr`b`] ) THEN
844  METIS_TAC [term_depth_APPLY] ) THEN
845Q_TAC SUFF_TAC `x = (s ��� (Var v))`
846THEN1 METIS_TAC [APPLY_subterm]
847SRW_TAC [][FUNPOW]
848
849
850
851HO_MATCH_MP_TAC FUNPOW_extends_mono THEN
852Induct THEN SRW_TAC [][]
853
854���t1 t2.(��t1 t2. ���v. (t1 = Var v) ��� v IN vars t2 ��� term_depth) t1 t2 ��� (measure term_depth) (FUNPOW ($��� s) n t1) (FUNPOW ($��� s) n t2)`
855HO_MATCH_MP_TAC FUNPOW_extends_mono THEN
856Induct THEN SRW_TAC [][]
857
858`(FUNPOW ($��� s) n (Var v) = FUNPOW ($��� s) n t) ��� (t ��� Var v) ��� v NOTIN vars t`,
859STRIP_TAC THEN SPOSE_NOT_THEN STRIP_ASSUME_TAC THEN
860Cases_on `n` THEN FULL_SIMP_TAC (srw_ss()) [] THEN
861`term_depth (Var v) < term_depth t`
862by (Induct_on `t` THEN FULL_SIMP_TAC (srw_ss()++ARITH_ss) []) THEN
863
864
865
866Induct_on `n` THEN SRW_TAC [][] THEN
867FIRST_X_ASSUM MATCH_MP_TAC THEN
868SRW_TAC [][] THEN
869HR
870FULL_SIMP_TAC (srw_ss()) [FUNPOW] THEN
871Cases_on `FLOOKUP s v` THEN FULL_SIMP_TAC (srw_ss()) [] THENL [
872
873
874val FUNPOW_APPLY_preserves_type = Q.store_thm(
875"FUNPOW_APPLY_preserves_type",
876`���FUNPOW ($��� s) n (Var v)
877
878val rangevarb_recurses = save_thm(
879"rangevarb_recurses",
880COMMUTING_ITSET_RECURSES |> Q.ISPEC `rangevarb_acc` |>
881SIMP_RULE (srw_ss()) [rangevarb_acc_def,ASSOC_BAG_UNION] |>
882SIMP_RULE (srw_ss()) [COMM_BAG_UNION]);
883
884val RELPOW_def = Define`
885  (RELPOW R 0 = REMPTY) ���
886  (RELPOW R (SUC n) = R O (RELPOW R n))`;
887
888val RELPOW1 = RWstore_thm(
889"RELPOW1",
890`RELPOW R 1 = R`,
891SRW_TAC [][FUN_EQ_THM] THEN Cases_on `1` THEN
892FULL_SIMP_TAC (srw_ss()) [RELPOW_def]);
893
894val selfapp_rangevarb = Q.store_thm(
895"selfapp_rangevarb",
896`rangevarb s = rangevarb (selfapp s)`,
897SRW_TAC [][rangevarb_def,selfapp_def,IMAGE_FAPPLY_FDOM]);
898
899(���b2. b2 IN sob2 ��� ���b1. b1 IN sob1 ��� mlt1 R b2 b1) ��� (mlt1 R)^+ (BIG_BAG_UNION sob2) (BIG_BAG_UNION sob1)
900
901val TC_vR_selfapp = Q.store_thm(
902"TC_vR_selfapp",
903`(vR (selfapp s))^+ v u ��� vR s v u ��� v NOTIN FDOM s ��� (���n. NRC (vR s) (SUC (SUC n)) v u)`,
904EQ_TAC THEN1 (
905  MAP_EVERY Q.ID_SPEC_TAC [`u`,`v`] THEN
906  HO_MATCH_MP_TAC TC_INDUCT THEN
907  SRW_TAC [][vR_selfapp]
908  THEN1 SRW_TAC [][]
909  THEN1 (
910    DISJ2_TAC THEN Q.EXISTS_TAC `0` THEN
911    ASM_SIMP_TAC (srw_ss()) [] )
912  THEN1 (
913    DISJ2_TAC THEN Q.EXISTS_TAC `0` THEN
914    ASM_SIMP_TAC (srw_ss()) [NRC] THEN
915    METIS_TAC [] )
916  THEN1 (
917    IMP_RES_TAC NRC_1 THEN
918    IMP_RES_TAC NRC_ADD_I THEN
919    FULL_SIMP_TAC (srw_ss()++ARITH_ss) [GSYM ADD_SUC] THEN
920    METIS_TAC [] )
921  THEN1 (
922    IMP_RES_TAC NRC_1 THEN
923    IMP_RES_TAC NRC_ADD_I THEN
924    FULL_SIMP_TAC (srw_ss()++ARITH_ss) [GSYM ADD_SUC,ADD_SYM] THEN
925    METIS_TAC [] )
926  THEN1 (
927    IMP_RES_TAC NRC_ADD_I THEN
928    FULL_SIMP_TAC (srw_ss()++ARITH_ss) [GSYM ADD_SUC] THEN
929    METIS_TAC [] ) ) THEN
930SRW_TAC [][] THEN1 (
931  MATCH_MP_TAC TC_SUBSET THEN
932  SRW_TAC [][vR_selfapp] ) THEN
933
934
935SIMP_TAC (srw_ss()) [GSYM AND_IMP_INTRO] THEN
936HO_MATCH_MP_TAC TC_INDUCT THEN
937SRW_TAC [][] THEN1 (
938  Cases_on `���n. NRC (vR s) (SUC (SUC n)) y x'` THEN1 (
939    FULL_SIMP_TAC (srw_ss()) [] THEN
940    MATCH_MP_TAC TC_SUBSET THEN
941    SRW_TAC [][vR_selfapp] THEN
942    METIS_TAC [] ) THEN
943  RES_TAC
944
945
946  SRW_TAC [][] THEN
947  IMP_RES_TAC TC_RULES THEN
948  IMP_RES_TAC TC_RULES THEN
949  `NRC (vR s) 2 y x'`
950  by (Cases_on `2` THEN FULL_SIMP_TAC (srw_ss()) [NRC] THEN METIS_TAC []) THEN
951  RES_TAC THEN FULL_SIMP_TAC (srw_ss()) []
952  (Q.MATCH_ABBREV_TAC `R^+ a b` THEN
953   METIS_TAC [TC_RULES]) ORELSE
954  (`NRC (vR s) 2 y x'`
955   by (Cases_on `2` THEN FULL_SIMP_TAC (srw_ss()) [NRC] THEN METIS_TAC []) THEN
956   RES_TAC THEN FULL_SIMP_TAC (srw_ss()) []))
957  SRW_TAC [][vR_selfapp] THEN
958  SRW_TAC [][] THEN ((
959    `NRC (vR s) 2 y x'`
960    by (Cases_on `2` THEN FULL_SIMP_TAC (srw_ss()) [NRC] THEN METIS_TAC []) THEN
961    RES_TAC THEN FULL_SIMP_TAC (srw_ss()) []) ORELSE
962    METIS_TAC [TC_RULES]))
963
964  ((
965    Cases_on `y IN FDOM s` THEN
966    FULL_SIMP_TAC (srw_ss()) [vR_def,FLOOKUP_DEF] THEN
967    NO_TAC ) ORELSE
968    METIS_TAC [TC_RULES])) THEN
969SIMP_TAC (srw_ss()) [GSYM AND_IMP_INTRO] THEN
970HO_MATCH_MP_TAC TC_INDUCT THEN
971SRW_TAC [][]
972STRIP_TAC
973Q_TAC SUFF_TAC `(���x y. (vR (selfapp s))^+ x y ��� (vR s)^+ x y) ���
974                (���x y. (vR s)^+ x y ��� (vR (selfapp s))^+ x y)`
975THEN1 (SRW_TAC [][FUN_EQ_THM] THEN METIS_TAC []) THEN
976CONJ_TAC THEN1 (
977  HO_MATCH_MP_TAC TC_INDUCT THEN
978  SRW_TAC [][vR_selfapp] THEN
979  METIS_TAC [TC_RULES]) THEN
980HO_MATCH_MP_TAC TC_INDUCT THEN
981SRW_TAC [][]
982  ;
983
984
985`(vR1 s RUNION NRC (vR s) (SUC (SUC 0))) y x ��� vR1 s y x ��� ���n. NRC (vR s) (SUC (SUC n)) y x`,
986SRW_TAC [][vR1_def,RUNION,NRC,EQ_IMP_THM] THENL [
987  SRW_TAC [][],
988  DISJ2_TAC THEN
989  Q.EXISTS_TAC `0` THEN
990  Q.EXISTS_TAC `z` THEN
991  SRW_TAC [][],
992  SRW_TAC [][],
993  false
994
995
996val selfapp_rangevarb_mlt = Q.store_thm(
997"selfapp_rangevarb_mlt",
998`��idempotent s ��� noids s ��� (mlt1 (vR s))^+ (rangevarb (selfapp s)) (rangevarb s)`,
999Q_TAC SUFF_TAC
1000`���b. FINITE_BAG b ��� ���s. (rangevarb s = b) ��� ��idempotent s ��� noids s ���
1001     (mlt1 (vR s))^+ (rangevarb (selfapp s)) (rangevarb s)`
1002THEN1 SRW_TAC [][] THEN
1003HO_MATCH_MP_TAC FINITE_BAG_INDUCT THEN
1004CONJ_TAC THEN1 (
1005  SRW_TAC [][rangevarb_def,EMPTY_BIG_BAG_UNION] THEN
1006  `~(DISJOINT (FDOM s) (BIGUNION (IMAGE vars (FRANGE s))))`
1007  by METIS_TAC [idempotent_rangevars] THEN
1008  FULL_SIMP_TAC (srw_ss()) [FRANGE_DEF] THEN
1009  Q_TAC SUFF_TAC `varb x = {||}` THEN1 (
1010    STRIP_TAC THEN
1011    `vars x = {}`
1012    by (SetCases_on `vars x` THEN FULL_SIMP_TAC (srw_ss()) [] THEN
1013        METIS_TAC [IN_varb_vars,NOT_IN_EMPTY_BAG,IN_INSERT]) THEN
1014    FULL_SIMP_TAC (srw_ss()) [] THEN SRW_TAC [][] THEN
1015    FULL_SIMP_TAC (srw_ss()) [DISJOINT_EMPTY]) THEN
1016  FIRST_X_ASSUM MATCH_MP_TAC THEN
1017  Q.EXISTS_TAC `x` THEN SRW_TAC [][] THEN
1018  Q.EXISTS_TAC `x���` THEN SRW_TAC [][]) THEN
1019SRW_TAC [][]
1020
1021  `varb b = {||}
1022  FIRST_X_ASSUM (Q.SPEC_THEN `varb b` MP_TAC) THEN
1023  SRW_TAC [][]
1024  SIMP_TAC (srw_ss()) [rangevarb_def,BIG_BAG_UNION_def,IMAGE_EMPTY] THEN
1025HO_MATCH_MP_TAC FINITE_INDUCT THEN
1026CONJ_TAC THEN1 (
1027  SRW_TAC [][] THEN
1028  `~(DISJOINT (FDOM s) (BIGUNION (IMAGE vars (FRANGE s))))`
1029  by METIS_TAC [idempotent_rangevars] THEN
1030  FULL_SIMP_TAC (srw_ss()) [FRANGE_DEF] THEN
1031  METIS_TAC [NOT_IN_EMPTY]) THEN
1032SRW_TAC [][]
1033
1034  SRW_TAC [][idempotent_def,FRANGE_DEF,EXTENSION] THEN
1035  Induct_on `t` THEN FULL_SIMP_TAC (srw_ss()) [FLOOKUP_DEF]
1036SRW_TAC [][rangevarb_def,selfapp_def,IMAGE_FAPPLY_FDOM,IMAGE_COMPOSE] THEN
1037o_f_FRANGE
1038FULL_SIMP_TAC (srw_ss()) []
1039
1040`���s. wfs s ��� ���n. idempotent (FUNPOW selfapp n s) ��� noids (FUNPOW selfapp n s)`,
1041WHILE_INDUCTION |> Q.ISPECL [
1042`��s. �� idempotent s`,
1043`selfapp`,
1044`��ss s. (mlt1 (vR s))^+ (domrangevarb ss) (domrangevarb s)`] |>
1045SIMP_RULE (srw_ss()) []
1046
1047Q.EXISTS_TAC `��ss s. (mlt1 (vR s))^+ (domrangevarb ss) (domrangevarb s)` THEN
1048SRW_TAC [][] THEN1 (
1049  SRW_TAC [][WF_EQ_WFP] THEN
1050  MATCH_MP_TAC WFP_RULES THEN
1051  SRW_TAC [][]
1052Q.EXISTS_TAC `inv_image (mlt1 (vR s))^+ domrangevarb` THEN
1053SRW_TAC [][] THEN1 (
1054  MATCH_MP_TAC WF_inv_image THEN
1055  MATCH_MP_TAC WF_TC THEN
1056  MATCH_MP_TAC WF_mlt1 THEN
1057  FULL_SIMP_TAC (srw_ss()) [wfs_def] ) THEN
1058SRW_TAC [][inv_image_def] THEN
1059SRW_TAC [][FUNPOW_SUC] THEN
1060
1061Q_TAC SUFF_TAC
1062`���s. ��idempotent s ��� noids s ��� (mlt1 (vR s))^+ (domrangevarb (selfapp s)) (domrangevarb s)`
1063METIS_TAC [FUNPOW_exists]
1064METIS_TAC [selfapp_rangevarb_mlt]);
1065
1066val selfappR_def = Define`
1067  selfappR ss s = (mlt1 (vR s)^+)^+
1068
1069
1070val selfapp_rangevarb_mlt = Q.store_thm(
1071"selfapp_rangevarb_mlt",
1072`��idempotent s ��� noids s ��� (mlt1 (vR s))^+ (domrangevarb (selfapp s)) (domrangevarb s)`,
1073
1074val sources_def = Define`
1075  sources s = {v | v IN FDOM s ��� ���u. (vR s)^+ v u }`;
1076
1077val sources_SUBSET_FDOM = Q.store_thm(
1078"sources_SUBSET_FDOM",
1079`sources s SUBSET FDOM s`,
1080SRW_TAC [][SUBSET_DEF,sources_def]);
1081
1082val sources_selfapp = Q.store_thm(
1083"sources_selfapp",
1084`wfs s ��� sources s ��� {} ��� (sources (selfapp s) PSUBSET sources s)`,
1085SRW_TAC [][sources_def,PSUBSET_DEF,SUBSET_DEF] THEN1 (
1086  IMP_RES_TAC TC_vR_selfapp THEN1 (
1087    Cases_on `2 * SUC n` THEN FULL_SIMP_TAC (srw_ss()) [] THEN
1088    IMP_RES_TAC TC_eq_NRC THEN METIS_TAC [] ) THEN
1089  FULL_SIMP_TAC (srw_ss()) [vR1_def]) THEN
1090FULL_SIMP_TAC (srw_ss()) [EXTENSION,EQ_IMP_THM] THEN
1091Q.EXISTS_TAC `x` THEN SRW_TAC [][] THEN
1092SRW_TAC [][TC_vR_selfapp]
1093
1094val (RTC_path_rules,RTC_path_ind,RTC_path_cases) = Hol_reln`
1095  (RTC_path R []) ���
1096  (RTC_path R [y]) ���
1097  (RTC_path R t ��� R x y ���
1098   RTC_path R (x::y::t))`;
1099
1100val RTC_path_strong_ind = save_thm(
1101"RTC_path_strong_ind",
1102IndDefLib.derive_strong_induction(RTC_path_rules, RTC_path_ind));
1103
1104val vR_path_bound = Q.store_thm(
1105"vR_path_bound",
1106`wfs s ��� ���ls. RTC_path (vR s) ls ��� LENGTH ls > 1 ��� LENGTH ls ��� CARD (FDOM s)`,
1107STRIP_TAC THEN HO_MATCH_MP_TAC RTC_path_strong_ind THEN
1108SRW_TAC [][] THEN
1109Cases_on `ls` THEN FULL_SIMP_TAC (srw_ss()) []
1110
1111val longest_path_def = Define`
1112  longest_path s = MAX_SET {n | ���v u. NRC (vR s) n v u}`;
1113
1114val NRC_vR_set = Q.store_thm(
1115"NRC_vR_set",
1116`wfs s ��� ���n v u. NRC (vR s) n v u ��� ���vs. vs SUBSET FDOM s ��� (CARD vs = n) ��� v NOTIN vs`,
1117STRIP_TAC THEN Induct THEN SRW_TAC [][] THEN1 (
1118  Q.EXISTS_TAC `{}` THEN SRW_TAC [][] ) THEN
1119FULL_SIMP_TAC (srw_ss()) [NRC] THEN
1120RES_TAC THEN
1121Q.EXISTS_TAC `z INSERT vs` THEN
1122FULL_SIMP_TAC (srw_ss()) [wfs_no_cycles] THEN
1123Cases_on `v = z` THEN1 (
1124  FULL_SIMP_TAC (srw_ss()) [] THEN
1125  IMP_RES_TAC TC_SUBSET THEN
1126  RES_TAC ) THEN
1127
1128SRW_TAC [][] THENL [
1129  Cases_on `z IN FDOM s` THEN
1130  FULL_SIMP_TAC (srw_ss()) [vR_def,FLOOKUP_DEF],
1131  IMP_RES_TAC FDOM_FINITE THEN
1132  IMP_RES_TAC SUBSET_FINITE
1133  SRW_TAC [][CARD_INSERT]
1134FULL_SIMP_TAC (srw_ss()) [vR_def,wfs_no_cycles,FLOOKUP_DEF]
1135
1136
1137val wfs_max_path = Q.store_thm(
1138"wfs_max_path",
1139`wfs s ��� ���n v u. NRC (vR s) n v u ��� n ��� CARD (FDOM s)`,
1140STRIP_TAC THEN Induct THEN SRW_TAC [][] THEN
1141FULL_SIMP_TAC (srw_ss()) [NRC] THEN
1142RES_TAC THEN
1143Cases_on `n = CARD (FDOM s)` THEN
1144FULL_SIMP_TAC (srw_ss()++ARITH_ss) []
1145
1146val vR_FUNPOW_selfapp = Q.store_thm(
1147"vR_FUNPOW_selfapp",
1148`���n s v u. vR (FUNPOW selfapp n s) v u ��� ���m. 1 ��� m ��� m ��� n + 1 ��� NRC (vR s) m v u ���
1149                                            (m ��� n ��� v NOTIN FDOM s)`,
1150Induct THEN SRW_TAC [][] THEN1 (
1151  SRW_TAC [][EQ_IMP_THM] THEN1 (
1152    Q.EXISTS_TAC `1` THEN SRW_TAC [][] ) THEN
1153  `m = 1` by DECIDE_TAC THEN
1154  FULL_SIMP_TAC (srw_ss()) [] ) THEN
1155SRW_TAC [][EQ_IMP_THM,FUNPOW_SUC,vR_selfapp,RUNION] THENL [
1156  FULL_SIMP_TAC (srw_ss()) [vR1_def] THEN
1157  RES_TAC THEN Q.EXISTS_TAC `m` THEN SRW_TAC [][] THEN
1158  DECIDE_TAC,
1159  ...,
1160  Cases_on `m ��� SUC n` THENL [
1161    SRW_TAC [][vR1_def] THEN
1162    DISJ1_TAC THEN
1163    Q.EXISTS_TAC `m` THEN FULL_SIMP_TAC (srw_ss()) [] THEN
1164    DECIDE_TAC,
1165    `m = SUC (SUC n)` by DECIDE_TAC THEN
1166    SRW_TAC [][] THEN
1167    FULL_SIMP_TAC (srw_ss()) [NRC] THEN
1168    SIMP_TAC bool_ss [TWO,ONE,NRC] THEN
1169
1170
1171    FULL_SIMP_TAC (srw_ss()) []
1172  RES_TAC
1173  FULL_SIMP_TAC bool_ss [TWO,ONE,NRC] THEN
1174  Cases_on `n` THEN FULL_SIMP_TAC (srw_ss()) [] THEN1 (
1175    Q.EXISTS_TAC `2` THEN SRW_TAC [][] THEN
1176    SIMP_TAC bool_ss [TWO,ONE,NRC] THEN
1177    METIS_TAC [] ) THEN
1178  FULL_SIMP_TAC (srw_ss()) [FUNPOW_SUC] THEN
1179  FULL_SIMP_TAC (srw_ss()) [vR_selfapp,RUNION]
1180  RES_TAC THEN IMP_RES_TAC NRC_ADD_I THEN
1181  Q.EXISTS_TAC `m' + m` THEN SRW_TAC [][] THENL [
1182    DECIDE_TAC,
1183    FULL_SIMP_TAC (srw_ss()) [ADD1]
1184
1185
1186completeInduct_on `n` THEN SRW_TAC [][EQ_IMP_THM] THENL [
1187  Cases_on `n` THEN FULL_SIMP_TAC (srw_ss()) [] THEN1 (
1188    Q.EXISTS_TAC `1` THEN SRW_TAC [][] ) THEN
1189  FIRST_X_ASSUM (Q.SPEC_THEN `n'` MP_TAC) THEN
1190  SRW_TAC [][] THEN
1191  FULL_SIMP_TAC (srw_ss()) [FUNPOW_SUC,vR_selfapp,RUNION] THEN1 (
1192    FULL_SIMP_TAC (srw_ss()) [vR1_def] THEN
1193    Q.EXISTS_TAC `m'` THEN SRW_TAC [][] THEN
1194    DECIDE_TAC ) THEN
1195  FULL_SIMP_TAC bool_ss [TWO,ONE,NRC] THEN
1196  RES_TAC
1197`���n. vR (FUNPOW selfapp (SUC n) s) = vR1 s RUNION NRC (vR s) (2 * (SUC n))`,
1198Induct THEN SRW_TAC [][vR_selfapp] THEN
1199FULL_SIMP_TAC (srw_ss()) [vR_selfapp,FUNPOW_SUC,vR1_selfapp] THEN
1200FULL_SIMP_TAC (srw_ss()) [RUNION,FUN_EQ_THM,vR1_def,EQ_IMP_THM,vR_selfapp,O_DEF] THEN
1201SRW_TAC [][] THENL [
1202  RES_TAC THEN SRW_TAC [][] THEN
1203
1204`��idempotent (selfapp s) ��� ���v u. NRC (vR s) 2 v u`,
1205SRW_TAC [][idempotent_def,selfapp_eq_iter_APPLY] THEN
1206Induct_on `t` THEN SRW_TAC [][] THEN1 (
1207
1208`��idempotent s ��� ���v u. vR s v u ��� v IN FDOM s`,
1209SRW_TAC [][idempotent_def,vR_def] THEN
1210REVERSE (Induct_on `t`) THEN SRW_TAC [][] THEN RES_TAC
1211THEN1 METIS_TAC [] THEN1 METIS_TAC [] THEN
1212Cases_on `FLOOKUP s n` THEN FULL_SIMP_TAC (srw_ss()) [] THEN
1213POP_ASSUM (K ALL_TAC) THEN
1214Induct_on `x` THEN SRW_TAC [][] THEN1 (
1215  MAP_EVERY Q.EXISTS_TAC [`n'`,`n`] THEN
1216  SRW_TAC [][] THEN
1217  Cases_on `FLOOKUP s n'` THEN
1218  FULL_SIMP_TAC (srw_ss()) [FLOOKUP_DEF] ) THEN
1219Cases_on `n IN FDOM s` THEN FULL_SIMP_TAC (srw_ss()) []
1220
1221`idempotent (FUNPOW selfapp n s) ��� ���v u. NRC (vR s) n v u`,
1222
1223`���n. idempotent (FUNPOW selfapp n s) ��� ���v u. NRC (vR s) n v u`,
1224Induct THEN SRW_TAC [][] THEN1 (
1225  IMP_RES_TAC idempotent_selfapp THEN
1226  SRW_TAC [][FUNPOW_SUC] ) THEN
1227Cases_on `idempotent (FUNPOW selfapp (SUC n) s)` THEN
1228SRW_TAC [][NRC,idempotent_def,FUNPOW_SUC,selfapp_eq_iter_APPLY]
1229
1230val vRn_def = Define`
1231  vRn s n y x = NRC (vR s) n y x ��� y NOTIN FDOM s`;
1232
1233val wfs_IMP_fixpoint = Q.store_thm(
1234"wfs_IMP_fixpoint",
1235`wfs s ��� ���n. idempotent (FUNPOW selfapp n s) ��� noids (FUNPOW selfapp n s)`,
1236
1237SRW_TAC [][wfs_no_cycles,domrangevarb_idempotent] THEN
1238SPOSE_NOT_THEN STRIP_ASSUME_TAC THEN
1239FULL_SIMP_TAC (srw_ss()) [domrangevarb_def,BAG_FILTER_EQ_EMPTY,rangevarb_def,BAG_IN_BIG_BAG_UNION] THEN
1240`���n. wfs (FUNPOW selfapp n s)`
1241by (MATCH_MP_TAC FUNPOW_extends_mono THEN
1242    SRW_TAC [][Once wfs_selfapp]) THEN
1243`���n. FDOM (FUNPOW selfapp n s) = FDOM s`
1244by ( (FUNPOW_extends_mono |> Q.ISPEC `��s'. FDOM s' = FDOM s` |>
1245      SIMP_RULE (srw_ss()) [] |> MATCH_MP_TAC ) THEN
1246     SRW_TAC [][]) THEN
1247FULL_SIMP_TAC (srw_ss()) [SKOLEM_THM,FORALL_AND_THM] THEN
1248TC_vR_selfapp
1249TC_vR_vars_FRANGE
1250SRW_TAC [][wfs_def,domrangevarb_idempotent] THEN
1251SRW_TAC [][BAG_EXTENSION]
1252WF_INDUCTION_THM |> Q.ISPEC `vR (s:subst)` |> UNDISCH |> HO_MATCH_MP_TAC
1253SRW_TAC [][domrangevarb_idempotent]
1254
1255STRIP_TAC THEN
1256`���n. wfs (FUNPOW selfapp n s)`
1257by (MATCH_MP_TAC FUNPOW_extends_mono THEN
1258    SRW_TAC [][Once wfs_selfapp]) THEN
1259`���n. noids (FUNPOW selfapp n s)`
1260by METIS_TAC [wfs_noids] THEN
1261`���n. FDOM (FUNPOW selfapp n s) = FDOM s`
1262by ( (FUNPOW_extends_mono |> Q.ISPEC `��s'. FDOM s' = FDOM s` |>
1263      SIMP_RULE (srw_ss()) [] |> MATCH_MP_TAC ) THEN
1264     SRW_TAC [][]) THEN
1265SRW_TAC [][] THEN HO_MATCH_MP_TAC FUNPOW_exists THEN
1266Q.EXISTS_TAC `inv_image (mlt1 (vR s)^+)^+ domrangevarb` THEN
1267CONJ_TAC THEN1 (
1268  MATCH_MP_TAC WF_inv_image THEN
1269  MATCH_MP_TAC WF_TC THEN
1270  MATCH_MP_TAC WF_mlt1 THEN
1271  MATCH_MP_TAC WF_TC THEN
1272  FULL_SIMP_TAC (srw_ss()) [wfs_def] ) THEN
1273Induct THEN FULL_SIMP_TAC (srw_ss()) [inv_image_def] THEN1 (
1274  STRIP_TAC THEN
1275  (domrangevarb_idempotent |> EQ_IMP_RULE |> snd |> CONTRAPOS |>
1276   SIMP_RULE (srw_ss()) [] |> IMP_RES_TAC)
1277
1278*)
1279
1280val _ = export_theory ();
1281