|
1 (* Title: HOL/Wellfounded_Recursion.ML |
|
2 ID: $Id$ |
|
3 Author: Tobias Nipkow, with minor changes by Konrad Slind |
|
4 Copyright 1992 University of Cambridge/1995 TU Munich |
|
5 |
|
6 Wellfoundedness, induction, and recursion |
|
7 *) |
|
8 |
|
9 Goal "x = y ==> H x z = H y z"; |
|
10 by (Asm_simp_tac 1); |
|
11 val H_cong2 = (*freeze H!*) |
|
12 read_instantiate [("H","H")] (result()); |
|
13 |
|
14 val [prem] = Goalw [wf_def] |
|
15 "(!!P x. (ALL x. (ALL y. (y,x) : r --> P(y)) --> P(x)) ==> P(x)) ==> wf(r)"; |
|
16 by (Clarify_tac 1); |
|
17 by (rtac prem 1); |
|
18 by (assume_tac 1); |
|
19 qed "wfUNIVI"; |
|
20 |
|
21 (*Restriction to domain A. If r is well-founded over A then wf(r)*) |
|
22 val [prem1,prem2] = Goalw [wf_def] |
|
23 "[| r <= A <*> A; \ |
|
24 \ !!x P. [| ALL x. (ALL y. (y,x) : r --> P y) --> P x; x:A |] ==> P x |] \ |
|
25 \ ==> wf r"; |
|
26 by (cut_facts_tac [prem1] 1); |
|
27 by (blast_tac (claset() addIs [prem2]) 1); |
|
28 qed "wfI"; |
|
29 |
|
30 val major::prems = Goalw [wf_def] |
|
31 "[| wf(r); \ |
|
32 \ !!x.[| ALL y. (y,x): r --> P(y) |] ==> P(x) \ |
|
33 \ |] ==> P(a)"; |
|
34 by (rtac (major RS spec RS mp RS spec) 1); |
|
35 by (blast_tac (claset() addIs prems) 1); |
|
36 qed "wf_induct"; |
|
37 |
|
38 (*Perform induction on i, then prove the wf(r) subgoal using prems. *) |
|
39 fun wf_ind_tac a prems i = |
|
40 EVERY [res_inst_tac [("a",a)] wf_induct i, |
|
41 rename_last_tac a ["1"] (i+1), |
|
42 ares_tac prems i]; |
|
43 |
|
44 Goal "wf(r) ==> ALL x. (a,x):r --> (x,a)~:r"; |
|
45 by (wf_ind_tac "a" [] 1); |
|
46 by (Blast_tac 1); |
|
47 qed_spec_mp "wf_not_sym"; |
|
48 |
|
49 (* [| wf r; ~Z ==> (a,x) : r; (x,a) ~: r ==> Z |] ==> Z *) |
|
50 bind_thm ("wf_asym", cla_make_elim wf_not_sym); |
|
51 |
|
52 Goal "wf(r) ==> (a,a) ~: r"; |
|
53 by (blast_tac (claset() addEs [wf_asym]) 1); |
|
54 qed "wf_not_refl"; |
|
55 |
|
56 (* [| wf r; (a,a) ~: r ==> PROP W |] ==> PROP W *) |
|
57 bind_thm ("wf_irrefl", make_elim wf_not_refl); |
|
58 |
|
59 (*transitive closure of a wf relation is wf! *) |
|
60 Goal "wf(r) ==> wf(r^+)"; |
|
61 by (stac wf_def 1); |
|
62 by (Clarify_tac 1); |
|
63 (*must retain the universal formula for later use!*) |
|
64 by (rtac allE 1 THEN assume_tac 1); |
|
65 by (etac mp 1); |
|
66 by (eres_inst_tac [("a","x")] wf_induct 1); |
|
67 by (blast_tac (claset() addEs [tranclE]) 1); |
|
68 qed "wf_trancl"; |
|
69 |
|
70 Goal "wf (r^-1) ==> wf ((r^+)^-1)"; |
|
71 by (stac (trancl_converse RS sym) 1); |
|
72 by (etac wf_trancl 1); |
|
73 qed "wf_converse_trancl"; |
|
74 |
|
75 |
|
76 (*---------------------------------------------------------------------------- |
|
77 * Minimal-element characterization of well-foundedness |
|
78 *---------------------------------------------------------------------------*) |
|
79 |
|
80 Goalw [wf_def] "wf r ==> x:Q --> (EX z:Q. ALL y. (y,z):r --> y~:Q)"; |
|
81 by (dtac spec 1); |
|
82 by (etac (mp RS spec) 1); |
|
83 by (Blast_tac 1); |
|
84 val lemma1 = result(); |
|
85 |
|
86 Goalw [wf_def] "(ALL Q x. x:Q --> (EX z:Q. ALL y. (y,z):r --> y~:Q)) ==> wf r"; |
|
87 by (Clarify_tac 1); |
|
88 by (dres_inst_tac [("x", "{x. ~ P x}")] spec 1); |
|
89 by (Blast_tac 1); |
|
90 val lemma2 = result(); |
|
91 |
|
92 Goal "wf r = (ALL Q x. x:Q --> (EX z:Q. ALL y. (y,z):r --> y~:Q))"; |
|
93 by (blast_tac (claset() addSIs [lemma1, lemma2]) 1); |
|
94 qed "wf_eq_minimal"; |
|
95 |
|
96 (*--------------------------------------------------------------------------- |
|
97 * Wellfoundedness of subsets |
|
98 *---------------------------------------------------------------------------*) |
|
99 |
|
100 Goal "[| wf(r); p<=r |] ==> wf(p)"; |
|
101 by (full_simp_tac (simpset() addsimps [wf_eq_minimal]) 1); |
|
102 by (Fast_tac 1); |
|
103 qed "wf_subset"; |
|
104 |
|
105 (*--------------------------------------------------------------------------- |
|
106 * Wellfoundedness of the empty relation. |
|
107 *---------------------------------------------------------------------------*) |
|
108 |
|
109 Goal "wf({})"; |
|
110 by (simp_tac (simpset() addsimps [wf_def]) 1); |
|
111 qed "wf_empty"; |
|
112 AddIffs [wf_empty]; |
|
113 |
|
114 (*--------------------------------------------------------------------------- |
|
115 * Wellfoundedness of `insert' |
|
116 *---------------------------------------------------------------------------*) |
|
117 |
|
118 Goal "wf(insert (y,x) r) = (wf(r) & (x,y) ~: r^*)"; |
|
119 by (rtac iffI 1); |
|
120 by (blast_tac (claset() addEs [wf_trancl RS wf_irrefl] |
|
121 addIs [rtrancl_into_trancl1,wf_subset,impOfSubs rtrancl_mono]) 1); |
|
122 by (asm_full_simp_tac (simpset() addsimps [wf_eq_minimal]) 1); |
|
123 by Safe_tac; |
|
124 by (EVERY1[rtac allE, assume_tac, etac impE, Blast_tac]); |
|
125 by (etac bexE 1); |
|
126 by (rename_tac "a" 1); |
|
127 by (case_tac "a = x" 1); |
|
128 by (res_inst_tac [("x","a")]bexI 2); |
|
129 by (assume_tac 3); |
|
130 by (Blast_tac 2); |
|
131 by (case_tac "y:Q" 1); |
|
132 by (Blast_tac 2); |
|
133 by (res_inst_tac [("x","{z. z:Q & (z,y) : r^*}")] allE 1); |
|
134 by (assume_tac 1); |
|
135 by (thin_tac "ALL Q. (EX x. x : Q) --> ?P Q" 1); (*essential for speed*) |
|
136 (*Blast_tac with new substOccur fails*) |
|
137 by (best_tac (claset() addIs [rtrancl_into_rtrancl2]) 1); |
|
138 qed "wf_insert"; |
|
139 AddIffs [wf_insert]; |
|
140 |
|
141 (*--------------------------------------------------------------------------- |
|
142 * Wellfoundedness of `disjoint union' |
|
143 *---------------------------------------------------------------------------*) |
|
144 |
|
145 (*Intuition behind this proof for the case of binary union: |
|
146 |
|
147 Goal: find an (R u S)-min element of a nonempty subset A. |
|
148 by case distinction: |
|
149 1. There is a step a -R-> b with a,b : A. |
|
150 Pick an R-min element z of the (nonempty) set {a:A | EX b:A. a -R-> b}. |
|
151 By definition, there is z':A s.t. z -R-> z'. Because z is R-min in the |
|
152 subset, z' must be R-min in A. Because z' has an R-predecessor, it cannot |
|
153 have an S-successor and is thus S-min in A as well. |
|
154 2. There is no such step. |
|
155 Pick an S-min element of A. In this case it must be an R-min |
|
156 element of A as well. |
|
157 |
|
158 *) |
|
159 |
|
160 Goal "[| ALL i:I. wf(r i); \ |
|
161 \ ALL i:I. ALL j:I. r i ~= r j --> Domain(r i) Int Range(r j) = {} & \ |
|
162 \ Domain(r j) Int Range(r i) = {} \ |
|
163 \ |] ==> wf(UN i:I. r i)"; |
|
164 by (asm_full_simp_tac (HOL_basic_ss addsimps [wf_eq_minimal]) 1); |
|
165 by (Clarify_tac 1); |
|
166 by (rename_tac "A a" 1); |
|
167 by (case_tac "EX i:I. EX a:A. EX b:A. (b,a) : r i" 1); |
|
168 by (Asm_full_simp_tac 2); |
|
169 by (Best_tac 2); (*much faster than Blast_tac*) |
|
170 by (Clarify_tac 1); |
|
171 by (EVERY1[dtac bspec, assume_tac, |
|
172 eres_inst_tac [("x","{a. a:A & (EX b:A. (b,a) : r i)}")] allE]); |
|
173 by (EVERY1[etac allE, etac impE]); |
|
174 by (ALLGOALS Blast_tac); |
|
175 qed "wf_UN"; |
|
176 |
|
177 Goalw [Union_def] |
|
178 "[| ALL r:R. wf r; \ |
|
179 \ ALL r:R. ALL s:R. r ~= s --> Domain r Int Range s = {} & \ |
|
180 \ Domain s Int Range r = {} \ |
|
181 \ |] ==> wf(Union R)"; |
|
182 by (blast_tac (claset() addIs [wf_UN]) 1); |
|
183 qed "wf_Union"; |
|
184 |
|
185 Goal "[| wf r; wf s; Domain r Int Range s = {}; Domain s Int Range r = {} \ |
|
186 \ |] ==> wf(r Un s)"; |
|
187 by (rtac (simplify (simpset()) (read_instantiate[("R","{r,s}")]wf_Union)) 1); |
|
188 by (Blast_tac 1); |
|
189 by (Blast_tac 1); |
|
190 qed "wf_Un"; |
|
191 |
|
192 (*--------------------------------------------------------------------------- |
|
193 * Wellfoundedness of `image' |
|
194 *---------------------------------------------------------------------------*) |
|
195 |
|
196 Goal "[| wf r; inj f |] ==> wf(prod_fun f f `` r)"; |
|
197 by (asm_full_simp_tac (HOL_basic_ss addsimps [wf_eq_minimal]) 1); |
|
198 by (Clarify_tac 1); |
|
199 by (case_tac "EX p. f p : Q" 1); |
|
200 by (eres_inst_tac [("x","{p. f p : Q}")]allE 1); |
|
201 by (fast_tac (claset() addDs [injD]) 1); |
|
202 by (Blast_tac 1); |
|
203 qed "wf_prod_fun_image"; |
|
204 |
|
205 (*** acyclic ***) |
|
206 |
|
207 Goalw [acyclic_def] "ALL x. (x, x) ~: r^+ ==> acyclic r"; |
|
208 by (assume_tac 1); |
|
209 qed "acyclicI"; |
|
210 |
|
211 Goalw [acyclic_def] "wf r ==> acyclic r"; |
|
212 by (blast_tac (claset() addEs [wf_trancl RS wf_irrefl]) 1); |
|
213 qed "wf_acyclic"; |
|
214 |
|
215 Goalw [acyclic_def] "acyclic(insert (y,x) r) = (acyclic r & (x,y) ~: r^*)"; |
|
216 by (simp_tac (simpset() addsimps [trancl_insert]) 1); |
|
217 by (blast_tac (claset() addIs [rtrancl_trans]) 1); |
|
218 qed "acyclic_insert"; |
|
219 AddIffs [acyclic_insert]; |
|
220 |
|
221 Goalw [acyclic_def] "acyclic(r^-1) = acyclic r"; |
|
222 by (simp_tac (simpset() addsimps [trancl_converse]) 1); |
|
223 qed "acyclic_converse"; |
|
224 AddIffs [acyclic_converse]; |
|
225 |
|
226 Goalw [acyclic_def,antisym_def] "acyclic r ==> antisym(r^*)"; |
|
227 by(blast_tac (claset() addEs [rtranclE] |
|
228 addIs [rtrancl_into_trancl1,rtrancl_trancl_trancl]) 1); |
|
229 qed "acyclic_impl_antisym_rtrancl"; |
|
230 |
|
231 (* Other direction: |
|
232 acyclic = no loops |
|
233 antisym = only self loops |
|
234 Goalw [acyclic_def,antisym_def] "antisym(r^* ) ==> acyclic(r - Id)"; |
|
235 ==> "antisym(r^* ) = acyclic(r - Id)"; |
|
236 *) |
|
237 |
|
238 Goalw [acyclic_def] "[| acyclic s; r <= s |] ==> acyclic r"; |
|
239 by (blast_tac (claset() addIs [trancl_mono]) 1); |
|
240 qed "acyclic_subset"; |
|
241 |
|
242 (** cut **) |
|
243 |
|
244 (*This rewrite rule works upon formulae; thus it requires explicit use of |
|
245 H_cong to expose the equality*) |
|
246 Goalw [cut_def] "(cut f r x = cut g r x) = (ALL y. (y,x):r --> f(y)=g(y))"; |
|
247 by (simp_tac (HOL_ss addsimps [expand_fun_eq]) 1); |
|
248 qed "cuts_eq"; |
|
249 |
|
250 Goalw [cut_def] "(x,a):r ==> (cut f r a)(x) = f(x)"; |
|
251 by (asm_simp_tac HOL_ss 1); |
|
252 qed "cut_apply"; |
|
253 |
|
254 (*** is_recfun ***) |
|
255 |
|
256 Goalw [is_recfun_def,cut_def] |
|
257 "[| is_recfun r H a f; ~(b,a):r |] ==> f(b) = arbitrary"; |
|
258 by (etac ssubst 1); |
|
259 by (asm_simp_tac HOL_ss 1); |
|
260 qed "is_recfun_undef"; |
|
261 |
|
262 (*** NOTE! some simplifications need a different Solver!! ***) |
|
263 fun indhyp_tac hyps = |
|
264 (cut_facts_tac hyps THEN' |
|
265 DEPTH_SOLVE_1 o (ares_tac [TrueI] ORELSE' |
|
266 eresolve_tac [transD, mp, allE])); |
|
267 val wf_super_ss = HOL_ss addSolver (mk_solver "WF" indhyp_tac); |
|
268 |
|
269 Goalw [is_recfun_def,cut_def] |
|
270 "[| wf(r); trans(r); is_recfun r H a f; is_recfun r H b g |] ==> \ |
|
271 \ (x,a):r --> (x,b):r --> f(x)=g(x)"; |
|
272 by (etac wf_induct 1); |
|
273 by (REPEAT (rtac impI 1 ORELSE etac ssubst 1)); |
|
274 by (asm_simp_tac (wf_super_ss addcongs [if_cong]) 1); |
|
275 qed_spec_mp "is_recfun_equal"; |
|
276 |
|
277 |
|
278 val prems as [wfr,transr,recfa,recgb,_] = goalw (the_context ()) [cut_def] |
|
279 "[| wf(r); trans(r); \ |
|
280 \ is_recfun r H a f; is_recfun r H b g; (b,a):r |] ==> \ |
|
281 \ cut f r b = g"; |
|
282 val gundef = recgb RS is_recfun_undef |
|
283 and fisg = recgb RS (recfa RS (transr RS (wfr RS is_recfun_equal))); |
|
284 by (cut_facts_tac prems 1); |
|
285 by (rtac ext 1); |
|
286 by (asm_simp_tac (wf_super_ss addsimps [gundef,fisg]) 1); |
|
287 qed "is_recfun_cut"; |
|
288 |
|
289 (*** Main Existence Lemma -- Basic Properties of the_recfun ***) |
|
290 |
|
291 Goalw [the_recfun_def] |
|
292 "is_recfun r H a f ==> is_recfun r H a (the_recfun r H a)"; |
|
293 by (eres_inst_tac [("P", "is_recfun r H a")] someI 1); |
|
294 qed "is_the_recfun"; |
|
295 |
|
296 Goal "[| wf(r); trans(r) |] ==> is_recfun r H a (the_recfun r H a)"; |
|
297 by (wf_ind_tac "a" [] 1); |
|
298 by (res_inst_tac [("f","cut (%y. H (the_recfun r H y) y) r a1")] |
|
299 is_the_recfun 1); |
|
300 by (rewtac is_recfun_def); |
|
301 by (stac cuts_eq 1); |
|
302 by (Clarify_tac 1); |
|
303 by (rtac H_cong2 1); |
|
304 by (subgoal_tac |
|
305 "the_recfun r H y = cut(%x. H(cut(the_recfun r H y) r x) x) r y" 1); |
|
306 by (Blast_tac 2); |
|
307 by (etac ssubst 1); |
|
308 by (simp_tac (HOL_ss addsimps [cuts_eq]) 1); |
|
309 by (Clarify_tac 1); |
|
310 by (stac cut_apply 1); |
|
311 by (fast_tac (claset() addDs [transD]) 1); |
|
312 by (fold_tac [is_recfun_def]); |
|
313 by (asm_simp_tac (wf_super_ss addsimps[is_recfun_cut]) 1); |
|
314 qed "unfold_the_recfun"; |
|
315 |
|
316 Goal "[| wf r; trans r; (x,a) : r; (x,b) : r |] \ |
|
317 \ ==> the_recfun r H a x = the_recfun r H b x"; |
|
318 by (best_tac (claset() addIs [is_recfun_equal, unfold_the_recfun]) 1); |
|
319 qed "the_recfun_equal"; |
|
320 |
|
321 (** Removal of the premise trans(r) **) |
|
322 val th = rewrite_rule[is_recfun_def] |
|
323 (trans_trancl RSN (2,(wf_trancl RS unfold_the_recfun))); |
|
324 |
|
325 Goalw [wfrec_def] |
|
326 "wf(r) ==> wfrec r H a = H (cut (wfrec r H) r a) a"; |
|
327 by (rtac H_cong2 1); |
|
328 by (simp_tac (HOL_ss addsimps [cuts_eq]) 1); |
|
329 by (rtac allI 1); |
|
330 by (rtac impI 1); |
|
331 by (res_inst_tac [("a1","a")] (th RS ssubst) 1); |
|
332 by (assume_tac 1); |
|
333 by (ftac wf_trancl 1); |
|
334 by (ftac r_into_trancl 1); |
|
335 by (asm_simp_tac (HOL_ss addsimps [cut_apply]) 1); |
|
336 by (rtac H_cong2 1); (*expose the equality of cuts*) |
|
337 by (simp_tac (HOL_ss addsimps [cuts_eq, cut_apply, r_into_trancl]) 1); |
|
338 by (blast_tac (claset() addIs [the_recfun_equal, transD, trans_trancl, |
|
339 r_into_trancl]) 1); |
|
340 qed "wfrec"; |
|
341 |
|
342 (*--------------------------------------------------------------------------- |
|
343 * This form avoids giant explosions in proofs. NOTE USE OF == |
|
344 *---------------------------------------------------------------------------*) |
|
345 Goal "[| f==wfrec r H; wf(r) |] ==> f(a) = H (cut f r a) a"; |
|
346 by Auto_tac; |
|
347 by (blast_tac (claset() addIs [wfrec]) 1); |
|
348 qed "def_wfrec"; |
|
349 |
|
350 |
|
351 (**** TFL variants ****) |
|
352 |
|
353 Goal "ALL R. wf R --> \ |
|
354 \ (ALL P. (ALL x. (ALL y. (y,x):R --> P y) --> P x) --> (ALL x. P x))"; |
|
355 by (Clarify_tac 1); |
|
356 by (res_inst_tac [("r","R"),("P","P"), ("a","x")] wf_induct 1); |
|
357 by (assume_tac 1); |
|
358 by (Blast_tac 1); |
|
359 qed"tfl_wf_induct"; |
|
360 |
|
361 Goal "ALL f R. (x,a):R --> (cut f R a)(x) = f(x)"; |
|
362 by (Clarify_tac 1); |
|
363 by (rtac cut_apply 1); |
|
364 by (assume_tac 1); |
|
365 qed"tfl_cut_apply"; |
|
366 |
|
367 Goal "ALL M R f. (f=wfrec R M) --> wf R --> (ALL x. f x = M (cut f R x) x)"; |
|
368 by (Clarify_tac 1); |
|
369 by (etac wfrec 1); |
|
370 qed "tfl_wfrec"; |