1 (* ========================================================================= *)
2 (* Theory of wellfounded relations. *)
4 (* John Harrison, University of Cambridge Computer Laboratory *)
6 (* (c) Copyright, University of Cambridge 1998 *)
7 (* (c) Copyright, John Harrison 1998-2007 *)
8 (* ========================================================================= *)
12 (* ------------------------------------------------------------------------- *)
13 (* Definition of wellfoundedness for arbitrary (infix) relation << *)
14 (* ------------------------------------------------------------------------- *)
16 parse_as_infix("<<",(12,"right"));;
18 let WF = new_definition
19 `WF(<<) <=> !P:A->bool. (?x. P(x)) ==> (?x. P(x) /\ !y. y << x ==> ~P(y))`;;
21 (* ------------------------------------------------------------------------- *)
22 (* Strengthen it to equality. *)
23 (* ------------------------------------------------------------------------- *)
26 (`WF(<<) <=> !P:A->bool. (?x. P(x)) <=> (?x. P(x) /\ !y. y << x ==> ~P(y))`,
27 REWRITE_TAC[WF] THEN MESON_TAC[]);;
29 (* ------------------------------------------------------------------------- *)
30 (* Equivalence of wellfounded induction. *)
31 (* ------------------------------------------------------------------------- *)
34 (`WF(<<) <=> !P:A->bool. (!x. (!y. y << x ==> P(y)) ==> P(x)) ==> !x. P(x)`,
35 REWRITE_TAC[WF] THEN EQ_TAC THEN DISCH_TAC THEN GEN_TAC THEN
36 POP_ASSUM(MP_TAC o SPEC `\x:A. ~P(x)`) THEN REWRITE_TAC[] THEN MESON_TAC[]);;
38 (* ------------------------------------------------------------------------- *)
39 (* Equivalence of the "infinite descending chains" version. *)
40 (* ------------------------------------------------------------------------- *)
43 (`WF(<<) <=> ~(?s:num->A. !n. s(SUC n) << s(n))`,
44 REWRITE_TAC[WF; TAUT `(a <=> ~b) <=> (~a <=> b)`; NOT_FORALL_THM] THEN
45 EQ_TAC THEN DISCH_THEN CHOOSE_TAC THENL
46 [POP_ASSUM(MP_TAC o REWRITE_RULE[NOT_IMP]) THEN
47 DISCH_THEN(CONJUNCTS_THEN2 (X_CHOOSE_TAC `a:A`) ASSUME_TAC) THEN
48 SUBGOAL_THEN `!x:A. ?y. P(x) ==> P(y) /\ y << x` MP_TAC THENL
49 [ASM_MESON_TAC[]; REWRITE_TAC[SKOLEM_THM]] THEN
50 DISCH_THEN(X_CHOOSE_THEN `f:A->A` STRIP_ASSUME_TAC) THEN
51 CHOOSE_TAC(prove_recursive_functions_exist num_RECURSION
52 `(s(0) = a:A) /\ (!n. s(SUC n) = f(s n))`) THEN
53 EXISTS_TAC `s:num->A` THEN ASM_REWRITE_TAC[] THEN
54 SUBGOAL_THEN `!n. P(s n) /\ s(SUC n):A << s(n)`
55 (fun th -> ASM_MESON_TAC[th]) THEN
56 INDUCT_TAC THEN ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[];
57 EXISTS_TAC `\y:A. ?n:num. y = s(n)` THEN REWRITE_TAC[] THEN
60 (* ------------------------------------------------------------------------- *)
61 (* Equivalent to just *uniqueness* part of recursion. *)
62 (* ------------------------------------------------------------------------- *)
66 !H. (!f g x. (!z. z << x ==> (f z = g z)) ==> (H f x = H g x))
67 ==> !(f:A->B) g. (!x. f x = H f x) /\ (!x. g x = H g x)
69 REWRITE_TAC[WF_IND] THEN REPEAT STRIP_TAC THEN REWRITE_TAC[FUN_EQ_THM] THEN
70 FIRST_ASSUM MATCH_MP_TAC THEN GEN_TAC THEN
71 DISCH_THEN(ANTE_RES_THEN MP_TAC) THEN ASM_REWRITE_TAC[]);;
73 let WF_UREC_WF = prove
74 (`(!H. (!f g x. (!z. z << x ==> (f z = g z)) ==> (H f x = H g x))
75 ==> !(f:A->bool) g. (!x. f x = H f x) /\ (!x. g x = H g x)
78 REWRITE_TAC[WF_IND] THEN DISCH_TAC THEN GEN_TAC THEN DISCH_TAC THEN
79 FIRST_X_ASSUM(MP_TAC o SPEC `\f x. P(x:A) \/ !z:A. z << x ==> f(z)`) THEN
81 W(C SUBGOAL_THEN (fun t -> REWRITE_TAC[t]) o funpow 2 lhand o snd) THENL
82 [MESON_TAC[]; DISCH_THEN(MP_TAC o SPECL [`P:A->bool`; `\x:A. T`]) THEN
83 REWRITE_TAC[FUN_EQ_THM] THEN ASM_MESON_TAC[]]);;
85 (* ------------------------------------------------------------------------- *)
86 (* Stronger form of recursion with "inductive invariant" (Krstic/Matthews). *)
87 (* ------------------------------------------------------------------------- *)
89 let WF_REC_INVARIANT = prove
91 ==> !H S. (!f g x. (!z. z << x ==> (f z = g z) /\ S z (f z))
92 ==> (H f x = H g x) /\ S x (H f x))
93 ==> ?f:A->B. !x. (f x = H f x)`,
94 let lemma = prove_inductive_relations_exist
95 `!f:A->B x. (!z. z << x ==> R z (f z)) ==> R x (H f x)` in
96 REWRITE_TAC[WF_IND] THEN REPEAT STRIP_TAC THEN
97 X_CHOOSE_THEN `R:A->B->bool` STRIP_ASSUME_TAC lemma THEN
98 SUBGOAL_THEN `!x:A. ?!y:B. R x y` (fun th -> ASM_MESON_TAC[th]) THEN
99 FIRST_X_ASSUM MATCH_MP_TAC THEN REPEAT STRIP_TAC THEN
100 FIRST_X_ASSUM(fun th -> GEN_REWRITE_TAC BINDER_CONV [th]) THEN
101 SUBGOAL_THEN `!x:A y:B. R x y ==> S x y` MP_TAC THEN ASM_MESON_TAC[]);;
103 (* ------------------------------------------------------------------------- *)
104 (* Equivalent to just *existence* part of recursion. *)
105 (* ------------------------------------------------------------------------- *)
109 ==> !H. (!f g x. (!z. z << x ==> (f z = g z)) ==> (H f x = H g x))
110 ==> ?f:A->B. !x. f x = H f x`,
111 REPEAT STRIP_TAC THEN
112 FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP WF_REC_INVARIANT) THEN
113 EXISTS_TAC `\x:A y:B. T` THEN ASM_REWRITE_TAC[]);;
115 let WF_REC_WF = prove
116 (`(!H. (!f g x. (!z. z << x ==> (f z = g z)) ==> (H f x = H g x))
117 ==> ?f:A->num. !x. f x = H f x)
119 DISCH_TAC THEN REWRITE_TAC[WF_DCHAIN] THEN
120 DISCH_THEN(X_CHOOSE_TAC `x:num->A`) THEN
121 SUBGOAL_THEN `!n. (x:num->A)(@m. x(m) << x(n)) << x(n)` ASSUME_TAC THENL
122 [CONV_TAC(BINDER_CONV SELECT_CONV) THEN ASM_MESON_TAC[]; ALL_TAC] THEN
123 FIRST_ASSUM(MP_TAC o SPEC
124 `\f:A->num. \y:A. if ?p:num. y = x(p)
125 then SUC(f(x(@m. x(m) << y)))
127 REWRITE_TAC[NOT_IMP] THEN CONJ_TAC THENL
128 [REPEAT STRIP_TAC THEN COND_CASES_TAC THEN REWRITE_TAC[] THEN
129 FIRST_ASSUM(X_CHOOSE_THEN `p:num` SUBST_ALL_TAC) THEN
130 AP_TERM_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN
131 FIRST_ASSUM MATCH_ACCEPT_TAC; ALL_TAC] THEN
132 DISCH_THEN(X_CHOOSE_THEN `f:A->num` MP_TAC) THEN
133 DISCH_THEN(MP_TAC o GEN `n:num` o SPEC `(x:num->A) n`) THEN
134 SUBGOAL_THEN `!n. ?p. (x:num->A) n = x p` (fun th -> REWRITE_TAC[th]) THENL
135 [MESON_TAC[]; DISCH_TAC] THEN
136 SUBGOAL_THEN `!n:num. ?k. f(x(k):A) < f(x(n))` ASSUME_TAC THENL
137 [GEN_TAC THEN EXISTS_TAC `@m:num. x(m):A << x(n)` THEN
138 FIRST_ASSUM(fun th -> GEN_REWRITE_TAC RAND_CONV [th]) THEN REWRITE_TAC[LT];
139 MP_TAC(SPEC `\n:num. ?i:num. n = f(x(i):A)` num_WOP) THEN
140 REWRITE_TAC[] THEN ASM_MESON_TAC[]]);;
142 (* ------------------------------------------------------------------------- *)
143 (* Combine the two versions of the recursion theorem. *)
144 (* ------------------------------------------------------------------------- *)
148 !H. (!f g x. (!z. z << x ==> (f z = g z)) ==> (H f x = H g x))
149 ==> ?!f:A->B. !x. f x = H f x`,
150 MESON_TAC[WF_REC; WF_UREC]);;
152 (* ------------------------------------------------------------------------- *)
153 (* Some preservation theorems for wellfoundedness. *)
154 (* ------------------------------------------------------------------------- *)
156 parse_as_infix("<<<",(12,"right"));;
158 let WF_SUBSET = prove
159 (`(!(x:A) y. x << y ==> x <<< y) /\ WF(<<<) ==> WF(<<)`,
160 DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN REWRITE_TAC[WF] THEN
161 DISCH_TAC THEN GEN_TAC THEN DISCH_THEN(ANTE_RES_THEN MP_TAC) THEN
162 UNDISCH_TAC `!(x:A) (y:A). x << y ==> x <<< y` THEN MESON_TAC[]);;
164 let WF_MEASURE_GEN = prove
165 (`!m:A->B. WF(<<) ==> WF(\x x'. m x << m x')`,
166 GEN_TAC THEN REWRITE_TAC[WF_IND] THEN REPEAT STRIP_TAC THEN
167 FIRST_ASSUM(MP_TAC o SPEC `\y:B. !x:A. (m(x) = y) ==> P x`) THEN
168 UNDISCH_TAC `!x. (!y. (m:A->B) y << m x ==> P y) ==> P x` THEN
169 REWRITE_TAC[] THEN MESON_TAC[]);;
171 let WF_LEX_DEPENDENT = prove
172 (`!R:A->A->bool S:A->B->B->bool. WF(R) /\ (!a. WF(S a))
173 ==> WF(\(r1,s1) (r2,s2). R r1 r2 \/ (r1 = r2) /\ S r1 s1 s2)`,
174 REPEAT GEN_TAC THEN REWRITE_TAC[WF] THEN STRIP_TAC THEN
175 X_GEN_TAC `P:A#B->bool` THEN REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
176 GEN_REWRITE_TAC I [FORALL_PAIR_THM] THEN
177 MAP_EVERY X_GEN_TAC [`a0:A`; `b0:B`] THEN DISCH_TAC THEN
178 FIRST_X_ASSUM(MP_TAC o SPEC `\a:A. ?b:B. P(a,b)`) THEN
179 REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
180 DISCH_THEN(MP_TAC o SPECL [`a0:A`; `b0:B`]) THEN ASM_REWRITE_TAC[] THEN
181 DISCH_THEN(X_CHOOSE_THEN `a:A` (CONJUNCTS_THEN2 MP_TAC ASSUME_TAC)) THEN
182 DISCH_THEN(X_CHOOSE_TAC `b1:B`) THEN
183 FIRST_X_ASSUM(MP_TAC o SPECL [`a:A`; `\b. (P:A#B->bool) (a,b)`]) THEN
184 REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN
185 DISCH_THEN(MP_TAC o SPEC `b1:B`) THEN ASM_REWRITE_TAC[] THEN
186 DISCH_THEN(X_CHOOSE_THEN `b:B` (CONJUNCTS_THEN2 MP_TAC ASSUME_TAC)) THEN
187 DISCH_TAC THEN EXISTS_TAC `(a:A,b:B)` THEN ASM_REWRITE_TAC[] THEN
188 REWRITE_TAC[FORALL_PAIR_THM] THEN ASM_MESON_TAC[]);;
191 (`!R:A->A->bool S:B->B->bool. WF(R) /\ WF(S)
192 ==> WF(\(r1,s1) (r2,s2). R r1 r2 \/ (r1 = r2) /\ S s1 s2)`,
193 SIMP_TAC[WF_LEX_DEPENDENT; ETA_AX]);;
195 let WF_POINTWISE = prove
196 (`WF((<<) :A->A->bool) /\ WF((<<<) :B->B->bool)
197 ==> WF(\(x1,y1) (x2,y2). x1 << x2 /\ y1 <<< y2)`,
198 STRIP_TAC THEN MATCH_MP_TAC(GEN_ALL WF_SUBSET) THEN EXISTS_TAC
199 `\(x1,y1) (x2,y2). x1 << x2 \/ (x1:A = x2) /\ (y1:B) <<< (y2:B)` THEN
201 [REWRITE_TAC[FORALL_PAIR_THM] THEN CONV_TAC TAUT;
202 MATCH_MP_TAC WF_LEX THEN ASM_REWRITE_TAC[]]);;
204 (* ------------------------------------------------------------------------- *)
205 (* Wellfoundedness properties of natural numbers. *)
206 (* ------------------------------------------------------------------------- *)
210 REWRITE_TAC[WF_IND; num_WF]);;
212 let WF_REC_num = prove
213 (`!H. (!f g n. (!m. m < n ==> (f m = g m)) ==> (H f n = H g n))
214 ==> ?f:num->A. !n. f n = H f n`,
215 MATCH_ACCEPT_TAC(MATCH_MP WF_REC WF_num));;
217 (* ------------------------------------------------------------------------- *)
218 (* Natural number measures (useful in program verification). *)
219 (* ------------------------------------------------------------------------- *)
221 let MEASURE = new_definition
222 `MEASURE m = \x y. m(x) < m(y)`;;
224 let WF_MEASURE = prove
225 (`!m:A->num. WF(MEASURE m)`,
226 REPEAT GEN_TAC THEN REWRITE_TAC[MEASURE] THEN
227 MATCH_MP_TAC WF_MEASURE_GEN THEN
228 MATCH_ACCEPT_TAC WF_num);;
230 let MEASURE_LE = prove
231 (`(!y. MEASURE m y a ==> MEASURE m y b) <=> m(a) <= m(b)`,
232 REWRITE_TAC[MEASURE] THEN MESON_TAC[NOT_LE; LTE_TRANS; LT_REFL]);;
234 (* ------------------------------------------------------------------------- *)
235 (* Trivially, a WF relation is irreflexive. *)
236 (* ------------------------------------------------------------------------- *)
239 (`!x:A. WF(<<) ==> ~(x << x)`,
240 GEN_TAC THEN REWRITE_TAC[WF] THEN
241 DISCH_THEN(MP_TAC o SPEC `\y:A. y = x`) THEN
242 REWRITE_TAC[] THEN MESON_TAC[]);;
244 (* ------------------------------------------------------------------------- *)
245 (* Even more trivially, the everywhere-false relation is wellfounded. *)
246 (* ------------------------------------------------------------------------- *)
252 (* ------------------------------------------------------------------------- *)
253 (* Tail recursion. *)
254 (* ------------------------------------------------------------------------- *)
256 let WF_REC_TAIL = prove
257 (`!P g h. ?f:A->B. !x. f x = if P(x) then f(g x) else h x`,
259 (`~(P 0) ==> ((?n. P(SUC n)) <=> (?n. P(n)))`,
260 MESON_TAC[num_CASES; NOT_SUC])
262 (`(P 0) ==> ((!m. m < n ==> P(SUC m)) <=> (!m. m < SUC n ==> P(m)))`,
263 REPEAT(DISCH_TAC ORELSE EQ_TAC) THEN INDUCT_TAC THEN
264 ASM_MESON_TAC[LT_SUC; LT_0]) in
266 MP_TAC(GEN `x:A` (ISPECL [`x:A`; `\y:A n:num. g(y):A`] num_RECURSION)) THEN
267 REWRITE_TAC[SKOLEM_THM; FORALL_AND_THM] THEN
268 DISCH_THEN(X_CHOOSE_THEN `s:A->num->A` STRIP_ASSUME_TAC) THEN
269 EXISTS_TAC `\x:A. if ?n:num. ~P(s x n)
270 then (h:A->B)(@y. ?n. (y = s x n) /\ ~P(s x n) /\
271 !m. m < n ==> P(s x m))
272 else something_arbitrary:B` THEN
274 SUBGOAL_THEN `!n x:A. s (g x) n :A = s x (SUC n)` ASSUME_TAC THENL
275 [INDUCT_TAC THEN ASM_REWRITE_TAC[];
276 UNDISCH_THEN `!x:A n. s x (SUC n) :A = g (s x n)` (K ALL_TAC)] THEN
277 ASM_CASES_TAC `(P:A->bool) x` THEN ASM_REWRITE_TAC[] THENL
278 [ASM_SIMP_TAC[lemma1] THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN
279 CONV_TAC SYM_CONV THEN ASM_SIMP_TAC[lemma2; lemma1];
280 COND_CASES_TAC THENL [ALL_TAC; ASM_MESON_TAC[]] THEN
281 AP_TERM_TAC THEN MATCH_MP_TAC SELECT_UNIQUE THEN
282 REWRITE_TAC[] THEN X_GEN_TAC `y:A` THEN EQ_TAC THENL
283 [SIMP_TAC[LEFT_IMP_EXISTS_THM] THEN
284 INDUCT_TAC THEN ASM_REWRITE_TAC[] THEN ASM_MESON_TAC[LT_0];
285 ASM_MESON_TAC[LT]]]);;
287 (* ------------------------------------------------------------------------- *)
288 (* A more general mix of tail and wellfounded recursion. *)
289 (* ------------------------------------------------------------------------- *)
291 let WF_REC_TAIL_GENERAL = prove
293 (!f g x. (!z. z << x ==> (f z = g z))
294 ==> (P f x <=> P g x) /\ G f x = G g x /\ H f x = H g x) /\
295 (!f g x. (!z. z << x ==> (f z = g z)) ==> (H f x = H g x)) /\
296 (!f x y. P f x /\ y << G f x ==> y << x)
297 ==> ?f:A->B. !x. f x = if P f x then f(G f x) else H f x`,
298 REPEAT STRIP_TAC THEN
300 (prove_inductive_relations_exist
301 `(!x:A. ~(P f x) ==> terminates f x) /\
302 (!x. P (f:A->B) x /\ terminates f (G f x) ==> terminates f x)`) THEN
303 REWRITE_TAC[FORALL_AND_THM] THEN
304 DISCH_THEN(STRIP_ASSUME_TAC o GSYM) THEN
306 `?while. !f:A->B x:A. while f x = if P f x then while f (G f x) else x`
307 (STRIP_ASSUME_TAC o GSYM)
308 THENL [REWRITE_TAC[GSYM SKOLEM_THM; WF_REC_TAIL]; ALL_TAC] THEN
310 `?f:A->B. !x. f x = if terminates f x then H f (while f x :A) else anything`
312 [FIRST_ASSUM(MATCH_MP_TAC o MATCH_MP WF_REC) THEN
313 REPEAT STRIP_TAC THEN MATCH_MP_TAC(MESON[]
314 `(a = b) /\ (a /\ b ==> (x = y) /\ (f x = g x))
315 ==> ((if a then f x else d) = (if b then g y else d))`) THEN
316 REPEAT STRIP_TAC THENL
319 (!x y. P f x /\ y << G (f:A->B) x ==> y << x) /\
320 (!y:A. (!z:A. z << y ==> z << x)
321 ==> (P f y = P g y) /\ (G f y = G g y))
322 ==> terminates f x ==> terminates g x`
323 (fun th -> EQ_TAC THEN MATCH_MP_TAC th THEN ASM_MESON_TAC[]) THEN
324 GEN_TAC THEN GEN_TAC THEN
325 REWRITE_TAC[RIGHT_FORALL_IMP_THM; IMP_CONJ] THEN DISCH_TAC THEN
326 ONCE_REWRITE_TAC[TAUT `a ==> b ==> c <=> b ==> a ==> c`] THEN
327 FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_MESON_TAC[];
329 `!x:A. terminates (f:A->B) x /\
330 (!y:A. (!z:A. z << y ==> z << x)
331 ==> (P f y <=> P g y) /\ (G f y :A = G g y))
332 ==> (while f x :A = while g x)`
333 (fun th -> MATCH_MP_TAC th THEN ASM_MESON_TAC[]) THEN
334 REWRITE_TAC[IMP_CONJ] THEN
335 FIRST_X_ASSUM MATCH_MP_TAC THEN ASM_MESON_TAC[];
336 FIRST_X_ASSUM MATCH_MP_TAC THEN
338 `!f:A->B. (!x:A y:A. P f x /\ y << G f x ==> y << x)
339 ==> !x. terminates f x ==> !y. y << while f x ==> y << x`
340 (fun th -> ASM_MESON_TAC[th]) THEN
341 GEN_TAC THEN DISCH_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
343 MATCH_MP_TAC MONO_EXISTS THEN GEN_TAC THEN
344 DISCH_THEN(fun th -> ASSUME_TAC(GSYM th) THEN MP_TAC th) THEN
345 MATCH_MP_TAC MONO_FORALL THEN X_GEN_TAC `x:A` THEN
346 ASM_CASES_TAC `P (f:A->B) (x:A) :bool` THEN ASM_MESON_TAC[]]);;
348 (* ------------------------------------------------------------------------- *)
349 (* Tactic to apply WF induction on a free "measured" term in the goal. *)
350 (* ------------------------------------------------------------------------- *)
355 (`(!x. P x ==> !y. Q x y) <=> !y x. P x ==> Q x y`, MESON_TAC[]) in
356 GEN_REWRITE_CONV I [pth]
359 (`(!m. P m ==> (m = e) ==> Q) <=> (P e ==> Q)`, MESON_TAC[]) in
362 try (qqconv THENC BINDER_CONV qqconvs) tm
363 with Failure _ -> eqconv tm in
364 fun tm (asl,w as gl) ->
366 and gv = genvar(type_of tm) in
367 let pat = list_mk_forall(gv::fvs,mk_imp(mk_eq(gv,tm),w)) in
368 let th0 = UNDISCH(PART_MATCH rand num_WF pat) in
369 let th1 = MP (SPECL (tm::fvs) th0) (REFL tm) in
370 let th2 = CONV_RULE(LAND_CONV qqconvs) (DISCH_ALL th1) in
371 (MATCH_MP_TAC th2 THEN MAP_EVERY X_GEN_TAC fvs THEN
372 CONV_TAC(LAND_CONV qqconvs) THEN DISCH_THEN ASSUME_TAC) gl;;