1 (* Title: ZF/WF.ML |
|
2 ID: $Id$ |
|
3 Author: Tobias Nipkow and Lawrence C Paulson |
|
4 Copyright 1998 University of Cambridge |
|
5 |
|
6 Well-founded Recursion |
|
7 |
|
8 Derived first for transitive relations, and finally for arbitrary WF relations |
|
9 via wf_trancl and trans_trancl. |
|
10 |
|
11 It is difficult to derive this general case directly, using r^+ instead of |
|
12 r. In is_recfun, the two occurrences of the relation must have the same |
|
13 form. Inserting r^+ in the_recfun or wftrec yields a recursion rule with |
|
14 r^+ -`` {a} instead of r-``{a}. This recursion rule is stronger in |
|
15 principle, but harder to use, especially to prove wfrec_eclose_eq in |
|
16 epsilon.ML. Expanding out the definition of wftrec in wfrec would yield |
|
17 a mess. |
|
18 *) |
|
19 |
|
20 |
|
21 (*** Well-founded relations ***) |
|
22 |
|
23 (** Equivalences between wf and wf_on **) |
|
24 |
|
25 Goalw [wf_def, wf_on_def] "wf(r) ==> wf[A](r)"; |
|
26 by (Clarify_tac 1); (*essential for Blast_tac's efficiency*) |
|
27 by (Blast_tac 1); |
|
28 qed "wf_imp_wf_on"; |
|
29 |
|
30 Goalw [wf_def, wf_on_def] "wf[field(r)](r) ==> wf(r)"; |
|
31 by (Fast_tac 1); |
|
32 qed "wf_on_field_imp_wf"; |
|
33 |
|
34 Goal "wf(r) <-> wf[field(r)](r)"; |
|
35 by (blast_tac (claset() addIs [wf_imp_wf_on, wf_on_field_imp_wf]) 1); |
|
36 qed "wf_iff_wf_on_field"; |
|
37 |
|
38 Goalw [wf_on_def, wf_def] "[| wf[A](r); B<=A |] ==> wf[B](r)"; |
|
39 by (Fast_tac 1); |
|
40 qed "wf_on_subset_A"; |
|
41 |
|
42 Goalw [wf_on_def, wf_def] "[| wf[A](r); s<=r |] ==> wf[A](s)"; |
|
43 by (Fast_tac 1); |
|
44 qed "wf_on_subset_r"; |
|
45 |
|
46 (** Introduction rules for wf_on **) |
|
47 |
|
48 (*If every non-empty subset of A has an r-minimal element then wf[A](r).*) |
|
49 val [prem] = Goalw [wf_on_def, wf_def] |
|
50 "[| !!Z u. [| Z<=A; u:Z; ALL x:Z. EX y:Z. <y,x>:r |] ==> False |] \ |
|
51 \ ==> wf[A](r)"; |
|
52 by (rtac (equals0I RS disjCI RS allI) 1); |
|
53 by (res_inst_tac [ ("Z", "Z") ] prem 1); |
|
54 by (ALLGOALS Blast_tac); |
|
55 qed "wf_onI"; |
|
56 |
|
57 (*If r allows well-founded induction over A then wf[A](r) |
|
58 Premise is equivalent to |
|
59 !!B. ALL x:A. (ALL y. <y,x>: r --> y:B) --> x:B ==> A<=B *) |
|
60 val [prem] = Goal |
|
61 "[| !!y B. [| ALL x:A. (ALL y:A. <y,x>:r --> y:B) --> x:B; y:A |] \ |
|
62 \ ==> y:B |] \ |
|
63 \ ==> wf[A](r)"; |
|
64 by (rtac wf_onI 1); |
|
65 by (res_inst_tac [ ("c", "u") ] (prem RS DiffE) 1); |
|
66 by (contr_tac 3); |
|
67 by (Blast_tac 2); |
|
68 by (Fast_tac 1); |
|
69 qed "wf_onI2"; |
|
70 |
|
71 |
|
72 (** Well-founded Induction **) |
|
73 |
|
74 (*Consider the least z in domain(r) Un {a} such that P(z) does not hold...*) |
|
75 val [major,minor] = Goalw [wf_def] |
|
76 "[| wf(r); \ |
|
77 \ !!x.[| ALL y. <y,x>: r --> P(y) |] ==> P(x) \ |
|
78 \ |] ==> P(a)"; |
|
79 by (res_inst_tac [ ("x", "{z:domain(r) Un {a}. ~P(z)}") ] (major RS allE) 1); |
|
80 by (etac disjE 1); |
|
81 by (blast_tac (claset() addEs [equalityE]) 1); |
|
82 by (asm_full_simp_tac (simpset() addsimps [domainI]) 1); |
|
83 by (blast_tac (claset() addSDs [minor]) 1); |
|
84 qed "wf_induct"; |
|
85 |
|
86 (*Perform induction on i, then prove the wf(r) subgoal using prems. *) |
|
87 fun wf_ind_tac a prems i = |
|
88 EVERY [res_inst_tac [("a",a)] wf_induct i, |
|
89 rename_last_tac a ["1"] (i+1), |
|
90 ares_tac prems i]; |
|
91 |
|
92 (*The form of this rule is designed to match wfI*) |
|
93 val wfr::amem::prems = Goal |
|
94 "[| wf(r); a:A; field(r)<=A; \ |
|
95 \ !!x.[| x: A; ALL y. <y,x>: r --> P(y) |] ==> P(x) \ |
|
96 \ |] ==> P(a)"; |
|
97 by (rtac (amem RS rev_mp) 1); |
|
98 by (wf_ind_tac "a" [wfr] 1); |
|
99 by (rtac impI 1); |
|
100 by (eresolve_tac prems 1); |
|
101 by (blast_tac (claset() addIs (prems RL [subsetD])) 1); |
|
102 qed "wf_induct2"; |
|
103 |
|
104 Goal "field(r Int A*A) <= A"; |
|
105 by (Blast_tac 1); |
|
106 qed "field_Int_square"; |
|
107 |
|
108 val wfr::amem::prems = Goalw [wf_on_def] |
|
109 "[| wf[A](r); a:A; \ |
|
110 \ !!x.[| x: A; ALL y:A. <y,x>: r --> P(y) |] ==> P(x) \ |
|
111 \ |] ==> P(a)"; |
|
112 by (rtac ([wfr, amem, field_Int_square] MRS wf_induct2) 1); |
|
113 by (REPEAT (ares_tac prems 1)); |
|
114 by (Blast_tac 1); |
|
115 qed "wf_on_induct"; |
|
116 |
|
117 fun wf_on_ind_tac a prems i = |
|
118 EVERY [res_inst_tac [("a",a)] wf_on_induct i, |
|
119 rename_last_tac a ["1"] (i+2), |
|
120 REPEAT (ares_tac prems i)]; |
|
121 |
|
122 (*If r allows well-founded induction then wf(r)*) |
|
123 val [subs,indhyp] = Goal |
|
124 "[| field(r)<=A; \ |
|
125 \ !!y B. [| ALL x:A. (ALL y:A. <y,x>:r --> y:B) --> x:B; y:A|] \ |
|
126 \ ==> y:B |] \ |
|
127 \ ==> wf(r)"; |
|
128 by (rtac ([wf_onI2, subs] MRS (wf_on_subset_A RS wf_on_field_imp_wf)) 1); |
|
129 by (REPEAT (ares_tac [indhyp] 1)); |
|
130 qed "wfI"; |
|
131 |
|
132 |
|
133 (*** Properties of well-founded relations ***) |
|
134 |
|
135 Goal "wf(r) ==> <a,a> ~: r"; |
|
136 by (wf_ind_tac "a" [] 1); |
|
137 by (Blast_tac 1); |
|
138 qed "wf_not_refl"; |
|
139 |
|
140 Goal "wf(r) ==> ALL x. <a,x>:r --> <x,a> ~: r"; |
|
141 by (wf_ind_tac "a" [] 1); |
|
142 by (Blast_tac 1); |
|
143 qed_spec_mp "wf_not_sym"; |
|
144 |
|
145 (* [| wf(r); <a,x> : r; ~P ==> <x,a> : r |] ==> P *) |
|
146 bind_thm ("wf_asym", wf_not_sym RS swap); |
|
147 |
|
148 Goal "[| wf[A](r); a: A |] ==> <a,a> ~: r"; |
|
149 by (wf_on_ind_tac "a" [] 1); |
|
150 by (Blast_tac 1); |
|
151 qed "wf_on_not_refl"; |
|
152 |
|
153 Goal "[| wf[A](r); a:A; b:A |] ==> <a,b>:r --> <b,a>~:r"; |
|
154 by (res_inst_tac [("x","b")] bspec 1); |
|
155 by (assume_tac 2); |
|
156 by (wf_on_ind_tac "a" [] 1); |
|
157 by (Blast_tac 1); |
|
158 qed_spec_mp "wf_on_not_sym"; |
|
159 |
|
160 (* [| wf[A](r); ~Z ==> <a,b> : r; |
|
161 <b,a> ~: r ==> Z; ~Z ==> a : A; ~Z ==> b : A |] ==> Z *) |
|
162 bind_thm ("wf_on_asym", permute_prems 1 2 (cla_make_elim wf_on_not_sym)); |
|
163 |
|
164 (*Needed to prove well_ordI. Could also reason that wf[A](r) means |
|
165 wf(r Int A*A); thus wf( (r Int A*A)^+ ) and use wf_not_refl *) |
|
166 Goal "[| wf[A](r); <a,b>:r; <b,c>:r; <c,a>:r; a:A; b:A; c:A |] ==> P"; |
|
167 by (subgoal_tac "ALL y:A. ALL z:A. <a,y>:r --> <y,z>:r --> <z,a>:r --> P" 1); |
|
168 by (wf_on_ind_tac "a" [] 2); |
|
169 by (Blast_tac 2); |
|
170 by (Blast_tac 1); |
|
171 qed "wf_on_chain3"; |
|
172 |
|
173 |
|
174 (*retains the universal formula for later use!*) |
|
175 val bchain_tac = EVERY' [rtac (bspec RS mp), assume_tac, assume_tac ]; |
|
176 |
|
177 (*transitive closure of a WF relation is WF provided A is downwards closed*) |
|
178 val [wfr,subs] = goal (the_context ()) |
|
179 "[| wf[A](r); r-``A <= A |] ==> wf[A](r^+)"; |
|
180 by (rtac wf_onI2 1); |
|
181 by (bchain_tac 1); |
|
182 by (eres_inst_tac [("a","y")] (wfr RS wf_on_induct) 1); |
|
183 by (cut_facts_tac [subs] 1); |
|
184 by (blast_tac (claset() addEs [tranclE]) 1); |
|
185 qed "wf_on_trancl"; |
|
186 |
|
187 Goal "wf(r) ==> wf(r^+)"; |
|
188 by (asm_full_simp_tac (simpset() addsimps [wf_iff_wf_on_field]) 1); |
|
189 by (rtac (trancl_type RS field_rel_subset RSN (2, wf_on_subset_A)) 1); |
|
190 by (etac wf_on_trancl 1); |
|
191 by (Blast_tac 1); |
|
192 qed "wf_trancl"; |
|
193 |
|
194 |
|
195 |
|
196 (** r-``{a} is the set of everything under a in r **) |
|
197 |
|
198 bind_thm ("underI", vimage_singleton_iff RS iffD2); |
|
199 bind_thm ("underD", vimage_singleton_iff RS iffD1); |
|
200 |
|
201 (** is_recfun **) |
|
202 |
|
203 Goalw [is_recfun_def] "is_recfun(r,a,H,f) ==> f: r-``{a} -> range(f)"; |
|
204 by (etac ssubst 1); |
|
205 by (rtac (lamI RS rangeI RS lam_type) 1); |
|
206 by (assume_tac 1); |
|
207 qed "is_recfun_type"; |
|
208 |
|
209 val [isrec,rel] = goalw (the_context ()) [is_recfun_def] |
|
210 "[| is_recfun(r,a,H,f); <x,a>:r |] ==> f`x = H(x, restrict(f,r-``{x}))"; |
|
211 by (res_inst_tac [("P", "%x.?t(x) = (?u::i)")] (isrec RS ssubst) 1); |
|
212 by (rtac (rel RS underI RS beta) 1); |
|
213 qed "apply_recfun"; |
|
214 |
|
215 Goal "[| wf(r); trans(r); is_recfun(r,a,H,f); is_recfun(r,b,H,g) |] \ |
|
216 \ ==> <x,a>:r --> <x,b>:r --> f`x=g`x"; |
|
217 by (forw_inst_tac [("f","f")] is_recfun_type 1); |
|
218 by (forw_inst_tac [("f","g")] is_recfun_type 1); |
|
219 by (asm_full_simp_tac (simpset() addsimps [is_recfun_def]) 1); |
|
220 by (wf_ind_tac "x" [] 1); |
|
221 by (REPEAT (rtac impI 1 ORELSE etac ssubst 1)); |
|
222 by (asm_simp_tac (simpset() addsimps [vimage_singleton_iff, restrict_def]) 1); |
|
223 by (res_inst_tac [("t","%z. H(?x,z)")] subst_context 1); |
|
224 by (subgoal_tac "ALL y : r-``{x1}. ALL z. <y,z>:f <-> <y,z>:g" 1); |
|
225 by (blast_tac (claset() addDs [transD]) 1); |
|
226 by (asm_full_simp_tac (simpset() addsimps [apply_iff]) 1); |
|
227 by (blast_tac (claset() addDs [transD] addIs [sym]) 1); |
|
228 qed_spec_mp "is_recfun_equal"; |
|
229 |
|
230 Goal "[| wf(r); trans(r); \ |
|
231 \ is_recfun(r,a,H,f); is_recfun(r,b,H,g); <b,a>:r |] \ |
|
232 \ ==> restrict(f, r-``{b}) = g"; |
|
233 by (forw_inst_tac [("f","f")] is_recfun_type 1); |
|
234 by (rtac fun_extension 1); |
|
235 by (blast_tac (claset() addDs [transD] addIs [restrict_type2]) 1); |
|
236 by (etac is_recfun_type 1); |
|
237 by (Asm_full_simp_tac 1); |
|
238 by (blast_tac (claset() addDs [transD] |
|
239 addIs [is_recfun_equal]) 1); |
|
240 qed "is_recfun_cut"; |
|
241 |
|
242 (*** Main Existence Lemma ***) |
|
243 |
|
244 Goal "[| wf(r); trans(r); is_recfun(r,a,H,f); is_recfun(r,a,H,g) |] ==> f=g"; |
|
245 by (blast_tac (claset() addIs [fun_extension, is_recfun_type, |
|
246 is_recfun_equal]) 1); |
|
247 qed "is_recfun_functional"; |
|
248 |
|
249 (*If some f satisfies is_recfun(r,a,H,-) then so does the_recfun(r,a,H) *) |
|
250 Goalw [the_recfun_def] |
|
251 "[| is_recfun(r,a,H,f); wf(r); trans(r) |] \ |
|
252 \ ==> is_recfun(r, a, H, the_recfun(r,a,H))"; |
|
253 by (rtac (ex1I RS theI) 1); |
|
254 by (REPEAT (ares_tac [is_recfun_functional] 1)); |
|
255 qed "is_the_recfun"; |
|
256 |
|
257 Goal "[| wf(r); trans(r) |] ==> is_recfun(r, a, H, the_recfun(r,a,H))"; |
|
258 by (wf_ind_tac "a" [] 1); |
|
259 by (res_inst_tac [("f", "lam y: r-``{a1}. wftrec(r,y,H)")] is_the_recfun 1); |
|
260 by (REPEAT (assume_tac 2)); |
|
261 by (rewrite_goals_tac [is_recfun_def, wftrec_def]); |
|
262 (*Applying the substitution: must keep the quantified assumption!!*) |
|
263 by (REPEAT (dtac underD 1 ORELSE resolve_tac [refl, lam_cong] 1)); |
|
264 by (fold_tac [is_recfun_def]); |
|
265 by (res_inst_tac [("t","%z. H(?x,z)")] subst_context 1); |
|
266 by (rtac fun_extension 1); |
|
267 by (blast_tac (claset() addIs [is_recfun_type]) 1); |
|
268 by (rtac (lam_type RS restrict_type2) 1); |
|
269 by (Blast_tac 1); |
|
270 by (blast_tac (claset() addDs [transD]) 1); |
|
271 by (ftac (spec RS mp) 1 THEN assume_tac 1); |
|
272 by (subgoal_tac "<xa,a1> : r" 1); |
|
273 by (dres_inst_tac [("x1","xa")] (spec RS mp) 1 THEN assume_tac 1); |
|
274 by (asm_full_simp_tac |
|
275 (simpset() addsimps [vimage_singleton_iff, underI RS beta, apply_recfun, |
|
276 is_recfun_cut]) 1); |
|
277 by (blast_tac (claset() addDs [transD]) 1); |
|
278 qed "unfold_the_recfun"; |
|
279 |
|
280 |
|
281 (*** Unfolding wftrec ***) |
|
282 |
|
283 Goal "[| wf(r); trans(r); <b,a>:r |] ==> \ |
|
284 \ restrict(the_recfun(r,a,H), r-``{b}) = the_recfun(r,b,H)"; |
|
285 by (REPEAT (ares_tac [is_recfun_cut, unfold_the_recfun] 1)); |
|
286 qed "the_recfun_cut"; |
|
287 |
|
288 (*NOT SUITABLE FOR REWRITING: it is recursive!*) |
|
289 Goalw [wftrec_def] |
|
290 "[| wf(r); trans(r) |] ==> \ |
|
291 \ wftrec(r,a,H) = H(a, lam x: r-``{a}. wftrec(r,x,H))"; |
|
292 by (stac (rewrite_rule [is_recfun_def] unfold_the_recfun) 1); |
|
293 by (ALLGOALS |
|
294 (asm_simp_tac |
|
295 (simpset() addsimps [vimage_singleton_iff RS iff_sym, the_recfun_cut]))); |
|
296 qed "wftrec"; |
|
297 |
|
298 (** Removal of the premise trans(r) **) |
|
299 |
|
300 (*NOT SUITABLE FOR REWRITING: it is recursive!*) |
|
301 val [wfr] = goalw (the_context ()) [wfrec_def] |
|
302 "wf(r) ==> wfrec(r,a,H) = H(a, lam x:r-``{a}. wfrec(r,x,H))"; |
|
303 by (stac (wfr RS wf_trancl RS wftrec) 1); |
|
304 by (rtac trans_trancl 1); |
|
305 by (rtac (vimage_pair_mono RS restrict_lam_eq RS subst_context) 1); |
|
306 by (etac r_into_trancl 1); |
|
307 by (rtac subset_refl 1); |
|
308 qed "wfrec"; |
|
309 |
|
310 (*This form avoids giant explosions in proofs. NOTE USE OF == *) |
|
311 val rew::prems = Goal |
|
312 "[| !!x. h(x)==wfrec(r,x,H); wf(r) |] ==> \ |
|
313 \ h(a) = H(a, lam x: r-``{a}. h(x))"; |
|
314 by (rewtac rew); |
|
315 by (REPEAT (resolve_tac (prems@[wfrec]) 1)); |
|
316 qed "def_wfrec"; |
|
317 |
|
318 val prems = Goal |
|
319 "[| wf(r); a:A; field(r)<=A; \ |
|
320 \ !!x u. [| x: A; u: Pi(r-``{x}, B) |] ==> H(x,u) : B(x) \ |
|
321 \ |] ==> wfrec(r,a,H) : B(a)"; |
|
322 by (res_inst_tac [("a","a")] wf_induct2 1); |
|
323 by (stac wfrec 4); |
|
324 by (REPEAT (ares_tac (prems@[lam_type]) 1 |
|
325 ORELSE eresolve_tac [spec RS mp, underD] 1)); |
|
326 qed "wfrec_type"; |
|
327 |
|
328 |
|
329 Goalw [wf_on_def, wfrec_on_def] |
|
330 "[| wf[A](r); a: A |] ==> \ |
|
331 \ wfrec[A](r,a,H) = H(a, lam x: (r-``{a}) Int A. wfrec[A](r,x,H))"; |
|
332 by (etac (wfrec RS trans) 1); |
|
333 by (asm_simp_tac (simpset() addsimps [vimage_Int_square, cons_subset_iff]) 1); |
|
334 qed "wfrec_on"; |
|
335 |
|
336 (*Minimal-element characterization of well-foundedness*) |
|
337 Goalw [wf_def] |
|
338 "wf(r) <-> (ALL Q x. x:Q --> (EX z:Q. ALL y. <y,z>:r --> y~:Q))"; |
|
339 by (Blast_tac 1); |
|
340 qed "wf_eq_minimal"; |
|
341 |
|