|
1 (* Title: ZF/wf.ML |
|
2 ID: $Id$ |
|
3 Author: Tobias Nipkow and Lawrence C Paulson |
|
4 Copyright 1992 University of Cambridge |
|
5 |
|
6 For wf.thy. 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 open WF; |
|
21 |
|
22 val [H_cong] = mk_typed_congs WF.thy[("H","[i,i]=>i")]; |
|
23 |
|
24 val wf_ss = ZF_ss addcongs [H_cong]; |
|
25 |
|
26 |
|
27 (*** Well-founded relations ***) |
|
28 |
|
29 (*Are these two theorems at all useful??*) |
|
30 |
|
31 (*If every subset of field(r) possesses an r-minimal element then wf(r). |
|
32 Seems impossible to prove this for domain(r) or range(r) instead... |
|
33 Consider in particular finite wf relations!*) |
|
34 val [prem1,prem2] = goalw WF.thy [wf_def] |
|
35 "[| field(r)<=A; \ |
|
36 \ !!Z u. [| Z<=A; u:Z; ALL x:Z. EX y:Z. <y,x>:r |] ==> False |] \ |
|
37 \ ==> wf(r)"; |
|
38 by (rtac (equals0I RS disjCI RS allI) 1); |
|
39 by (rtac prem2 1); |
|
40 by (res_inst_tac [ ("B1", "Z") ] (prem1 RS (Int_lower1 RS subset_trans)) 1); |
|
41 by (fast_tac ZF_cs 1); |
|
42 by (fast_tac ZF_cs 1); |
|
43 val wfI = result(); |
|
44 |
|
45 (*If r allows well-founded induction then wf(r)*) |
|
46 val [prem1,prem2] = goal WF.thy |
|
47 "[| field(r)<=A; \ |
|
48 \ !!B. ALL x:A. (ALL y. <y,x>: r --> y:B) --> x:B ==> A<=B |] \ |
|
49 \ ==> wf(r)"; |
|
50 by (rtac (prem1 RS wfI) 1); |
|
51 by (res_inst_tac [ ("B", "A-Z") ] (prem2 RS subsetCE) 1); |
|
52 by (fast_tac ZF_cs 3); |
|
53 by (fast_tac ZF_cs 2); |
|
54 by (fast_tac ZF_cs 1); |
|
55 val wfI2 = result(); |
|
56 |
|
57 |
|
58 (** Well-founded Induction **) |
|
59 |
|
60 (*Consider the least z in domain(r) Un {a} such that P(z) does not hold...*) |
|
61 val major::prems = goalw WF.thy [wf_def] |
|
62 "[| wf(r); \ |
|
63 \ !!x.[| ALL y. <y,x>: r --> P(y) |] ==> P(x) \ |
|
64 \ |] ==> P(a)"; |
|
65 by (res_inst_tac [ ("x", "{z:domain(r) Un {a}. ~P(z)}") ] (major RS allE) 1); |
|
66 by (etac disjE 1); |
|
67 by (rtac classical 1); |
|
68 by (etac equals0D 1); |
|
69 by (etac (singletonI RS UnI2 RS CollectI) 1); |
|
70 by (etac bexE 1); |
|
71 by (etac CollectE 1); |
|
72 by (etac swap 1); |
|
73 by (resolve_tac prems 1); |
|
74 by (fast_tac ZF_cs 1); |
|
75 val wf_induct = result(); |
|
76 |
|
77 (*Perform induction on i, then prove the wf(r) subgoal using prems. *) |
|
78 fun wf_ind_tac a prems i = |
|
79 EVERY [res_inst_tac [("a",a)] wf_induct i, |
|
80 rename_last_tac a ["1"] (i+1), |
|
81 ares_tac prems i]; |
|
82 |
|
83 (*The form of this rule is designed to match wfI2*) |
|
84 val wfr::amem::prems = goal WF.thy |
|
85 "[| wf(r); a:A; field(r)<=A; \ |
|
86 \ !!x.[| x: A; ALL y. <y,x>: r --> P(y) |] ==> P(x) \ |
|
87 \ |] ==> P(a)"; |
|
88 by (rtac (amem RS rev_mp) 1); |
|
89 by (wf_ind_tac "a" [wfr] 1); |
|
90 by (rtac impI 1); |
|
91 by (eresolve_tac prems 1); |
|
92 by (fast_tac (ZF_cs addIs (prems RL [subsetD])) 1); |
|
93 val wf_induct2 = result(); |
|
94 |
|
95 val prems = goal WF.thy "[| wf(r); <a,x>:r; <x,a>:r |] ==> False"; |
|
96 by (subgoal_tac "ALL x. <a,x>:r --> <x,a>:r --> False" 1); |
|
97 by (wf_ind_tac "a" prems 2); |
|
98 by (fast_tac ZF_cs 2); |
|
99 by (fast_tac (FOL_cs addIs prems) 1); |
|
100 val wf_anti_sym = result(); |
|
101 |
|
102 (*transitive closure of a WF relation is WF!*) |
|
103 val [prem] = goal WF.thy "wf(r) ==> wf(r^+)"; |
|
104 by (rtac (trancl_type RS field_rel_subset RS wfI2) 1); |
|
105 by (rtac subsetI 1); |
|
106 (*must retain the universal formula for later use!*) |
|
107 by (rtac (bspec RS mp) 1 THEN assume_tac 1 THEN assume_tac 1); |
|
108 by (eres_inst_tac [("a","x")] (prem RS wf_induct2) 1); |
|
109 by (rtac subset_refl 1); |
|
110 by (rtac (impI RS allI) 1); |
|
111 by (etac tranclE 1); |
|
112 by (etac (bspec RS mp) 1); |
|
113 by (etac fieldI1 1); |
|
114 by (fast_tac ZF_cs 1); |
|
115 by (fast_tac ZF_cs 1); |
|
116 val wf_trancl = result(); |
|
117 |
|
118 (** r-``{a} is the set of everything under a in r **) |
|
119 |
|
120 val underI = standard (vimage_singleton_iff RS iffD2); |
|
121 val underD = standard (vimage_singleton_iff RS iffD1); |
|
122 |
|
123 (** is_recfun **) |
|
124 |
|
125 val [major] = goalw WF.thy [is_recfun_def] |
|
126 "is_recfun(r,a,H,f) ==> f: r-``{a} -> range(f)"; |
|
127 by (rtac (major RS ssubst) 1); |
|
128 by (rtac (lamI RS rangeI RS lam_type) 1); |
|
129 by (assume_tac 1); |
|
130 val is_recfun_type = result(); |
|
131 |
|
132 val [isrec,rel] = goalw WF.thy [is_recfun_def] |
|
133 "[| is_recfun(r,a,H,f); <x,a>:r |] ==> f`x = H(x, restrict(f,r-``{x}))"; |
|
134 by (res_inst_tac [("P", "%x.?t(x) = ?u::i")] (isrec RS ssubst) 1); |
|
135 by (rtac (rel RS underI RS beta) 1); |
|
136 val apply_recfun = result(); |
|
137 |
|
138 (*eresolve_tac transD solves <a,b>:r using transitivity AT MOST ONCE |
|
139 spec RS mp instantiates induction hypotheses*) |
|
140 fun indhyp_tac hyps = |
|
141 ares_tac (TrueI::hyps) ORELSE' |
|
142 (cut_facts_tac hyps THEN' |
|
143 DEPTH_SOLVE_1 o (ares_tac [TrueI, ballI] ORELSE' |
|
144 eresolve_tac [underD, transD, spec RS mp])); |
|
145 |
|
146 (*** NOTE! some simplifications need a different auto_tac!! ***) |
|
147 val wf_super_ss = wf_ss setauto indhyp_tac; |
|
148 |
|
149 val prems = goalw WF.thy [is_recfun_def] |
|
150 "[| wf(r); trans(r); is_recfun(r,a,H,f); is_recfun(r,b,H,g) |] ==> \ |
|
151 \ <x,a>:r --> <x,b>:r --> f`x=g`x"; |
|
152 by (cut_facts_tac prems 1); |
|
153 by (wf_ind_tac "x" prems 1); |
|
154 by (REPEAT (rtac impI 1 ORELSE etac ssubst 1)); |
|
155 by (rewtac restrict_def); |
|
156 by (ASM_SIMP_TAC (wf_super_ss addrews [vimage_singleton_iff]) 1); |
|
157 val is_recfun_equal_lemma = result(); |
|
158 val is_recfun_equal = standard (is_recfun_equal_lemma RS mp RS mp); |
|
159 |
|
160 val prems as [wfr,transr,recf,recg,_] = goal WF.thy |
|
161 "[| wf(r); trans(r); \ |
|
162 \ is_recfun(r,a,H,f); is_recfun(r,b,H,g); <b,a>:r |] ==> \ |
|
163 \ restrict(f, r-``{b}) = g"; |
|
164 by (cut_facts_tac prems 1); |
|
165 by (rtac (consI1 RS restrict_type RS fun_extension) 1); |
|
166 by (etac is_recfun_type 1); |
|
167 by (ALLGOALS |
|
168 (ASM_SIMP_TAC (wf_super_ss addrews |
|
169 [ [wfr,transr,recf,recg] MRS is_recfun_equal ]))); |
|
170 val is_recfun_cut = result(); |
|
171 |
|
172 (*** Main Existence Lemma ***) |
|
173 |
|
174 val prems = goal WF.thy |
|
175 "[| wf(r); trans(r); is_recfun(r,a,H,f); is_recfun(r,a,H,g) |] ==> f=g"; |
|
176 by (cut_facts_tac prems 1); |
|
177 by (rtac fun_extension 1); |
|
178 by (REPEAT (ares_tac [is_recfun_equal] 1 |
|
179 ORELSE eresolve_tac [is_recfun_type,underD] 1)); |
|
180 val is_recfun_functional = result(); |
|
181 |
|
182 (*If some f satisfies is_recfun(r,a,H,-) then so does the_recfun(r,a,H) *) |
|
183 val prems = goalw WF.thy [the_recfun_def] |
|
184 "[| is_recfun(r,a,H,f); wf(r); trans(r) |] \ |
|
185 \ ==> is_recfun(r, a, H, the_recfun(r,a,H))"; |
|
186 by (rtac (ex1I RS theI) 1); |
|
187 by (REPEAT (ares_tac (prems@[is_recfun_functional]) 1)); |
|
188 val is_the_recfun = result(); |
|
189 |
|
190 val prems = goal WF.thy |
|
191 "[| wf(r); trans(r) |] ==> is_recfun(r, a, H, the_recfun(r,a,H))"; |
|
192 by (cut_facts_tac prems 1); |
|
193 by (wf_ind_tac "a" prems 1); |
|
194 by (res_inst_tac [("f", "lam y: r-``{a1}. wftrec(r,y,H)")] is_the_recfun 1); |
|
195 by (REPEAT (assume_tac 2)); |
|
196 by (rewrite_goals_tac [is_recfun_def, wftrec_def]); |
|
197 (*Applying the substitution: must keep the quantified assumption!!*) |
|
198 by (REPEAT (dtac underD 1 ORELSE resolve_tac [refl, lam_cong, H_cong] 1)); |
|
199 by (fold_tac [is_recfun_def]); |
|
200 by (rtac (consI1 RS restrict_type RSN (2,fun_extension)) 1); |
|
201 by (rtac is_recfun_type 1); |
|
202 by (ALLGOALS |
|
203 (ASM_SIMP_TAC |
|
204 (wf_super_ss addrews [underI RS beta, apply_recfun, is_recfun_cut]))); |
|
205 val unfold_the_recfun = result(); |
|
206 |
|
207 |
|
208 (*** Unfolding wftrec ***) |
|
209 |
|
210 val prems = goal WF.thy |
|
211 "[| wf(r); trans(r); <b,a>:r |] ==> \ |
|
212 \ restrict(the_recfun(r,a,H), r-``{b}) = the_recfun(r,b,H)"; |
|
213 by (REPEAT (ares_tac (prems @ [is_recfun_cut, unfold_the_recfun]) 1)); |
|
214 val the_recfun_cut = result(); |
|
215 |
|
216 (*NOT SUITABLE FOR REWRITING since it is recursive!*) |
|
217 val prems = goalw WF.thy [wftrec_def] |
|
218 "[| wf(r); trans(r) |] ==> \ |
|
219 \ wftrec(r,a,H) = H(a, lam x: r-``{a}. wftrec(r,x,H))"; |
|
220 by (rtac (rewrite_rule [is_recfun_def] unfold_the_recfun RS ssubst) 1); |
|
221 by (ALLGOALS (ASM_SIMP_TAC |
|
222 (wf_ss addrews (prems@[vimage_singleton_iff RS iff_sym, |
|
223 the_recfun_cut])))); |
|
224 val wftrec = result(); |
|
225 |
|
226 (** Removal of the premise trans(r) **) |
|
227 |
|
228 (*NOT SUITABLE FOR REWRITING since it is recursive!*) |
|
229 val [wfr] = goalw WF.thy [wfrec_def] |
|
230 "wf(r) ==> wfrec(r,a,H) = H(a, lam x:r-``{a}. wfrec(r,x,H))"; |
|
231 by (rtac (wfr RS wf_trancl RS wftrec RS ssubst) 1); |
|
232 by (rtac trans_trancl 1); |
|
233 by (rtac (refl RS H_cong) 1); |
|
234 by (rtac (vimage_pair_mono RS restrict_lam_eq) 1); |
|
235 by (etac r_into_trancl 1); |
|
236 by (rtac subset_refl 1); |
|
237 val wfrec = result(); |
|
238 |
|
239 (*This form avoids giant explosions in proofs. NOTE USE OF == *) |
|
240 val rew::prems = goal WF.thy |
|
241 "[| !!x. h(x)==wfrec(r,x,H); wf(r) |] ==> \ |
|
242 \ h(a) = H(a, lam x: r-``{a}. h(x))"; |
|
243 by (rewtac rew); |
|
244 by (REPEAT (resolve_tac (prems@[wfrec]) 1)); |
|
245 val def_wfrec = result(); |
|
246 |
|
247 val prems = goal WF.thy |
|
248 "[| wf(r); a:A; field(r)<=A; \ |
|
249 \ !!x u. [| x: A; u: Pi(r-``{x}, B) |] ==> H(x,u) : B(x) \ |
|
250 \ |] ==> wfrec(r,a,H) : B(a)"; |
|
251 by (res_inst_tac [("a","a")] wf_induct2 1); |
|
252 by (rtac (wfrec RS ssubst) 4); |
|
253 by (REPEAT (ares_tac (prems@[lam_type]) 1 |
|
254 ORELSE eresolve_tac [spec RS mp, underD] 1)); |
|
255 val wfrec_type = result(); |
|
256 |
|
257 val prems = goalw WF.thy [wfrec_def,wftrec_def,the_recfun_def,is_recfun_def] |
|
258 "[| r=r'; !!x u. H(x,u)=H'(x,u); a=a' |] \ |
|
259 \ ==> wfrec(r,a,H)=wfrec(r',a',H')"; |
|
260 by (EVERY1 (map rtac (prems RL [subst]))); |
|
261 by (SIMP_TAC (wf_ss addrews (prems RL [sym])) 1); |
|
262 val wfrec_cong = result(); |