author | clasohm |
Tue, 30 Jan 1996 13:42:57 +0100 | |
changeset 1461 | 6bcb44e4d6e5 |
parent 782 | 200a16083201 |
child 2033 | 639de962ded4 |
permissions | -rw-r--r-- |
1461 | 1 |
(* Title: ZF/wf.ML |
0 | 2 |
ID: $Id$ |
1461 | 3 |
Author: Tobias Nipkow and Lawrence C Paulson |
0 | 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 |
||
23 |
(*** Well-founded relations ***) |
|
24 |
||
435 | 25 |
(** Equivalences between wf and wf_on **) |
26 |
||
27 |
goalw WF.thy [wf_def, wf_on_def] "!!A r. wf(r) ==> wf[A](r)"; |
|
28 |
by (fast_tac ZF_cs 1); |
|
760 | 29 |
qed "wf_imp_wf_on"; |
435 | 30 |
|
31 |
goalw WF.thy [wf_def, wf_on_def] "!!r. wf[field(r)](r) ==> wf(r)"; |
|
32 |
by (fast_tac ZF_cs 1); |
|
760 | 33 |
qed "wf_on_field_imp_wf"; |
435 | 34 |
|
35 |
goal WF.thy "wf(r) <-> wf[field(r)](r)"; |
|
36 |
by (fast_tac (ZF_cs addSEs [wf_imp_wf_on, wf_on_field_imp_wf]) 1); |
|
760 | 37 |
qed "wf_iff_wf_on_field"; |
0 | 38 |
|
435 | 39 |
goalw WF.thy [wf_on_def, wf_def] "!!A B r. [| wf[A](r); B<=A |] ==> wf[B](r)"; |
40 |
by (fast_tac ZF_cs 1); |
|
760 | 41 |
qed "wf_on_subset_A"; |
435 | 42 |
|
43 |
goalw WF.thy [wf_on_def, wf_def] "!!A r s. [| wf[A](r); s<=r |] ==> wf[A](s)"; |
|
44 |
by (fast_tac ZF_cs 1); |
|
760 | 45 |
qed "wf_on_subset_r"; |
435 | 46 |
|
47 |
(** Introduction rules for wf_on **) |
|
48 |
||
49 |
(*If every non-empty subset of A has an r-minimal element then wf[A](r).*) |
|
50 |
val [prem] = goalw WF.thy [wf_on_def, wf_def] |
|
51 |
"[| !!Z u. [| Z<=A; u:Z; ALL x:Z. EX y:Z. <y,x>:r |] ==> False |] \ |
|
52 |
\ ==> wf[A](r)"; |
|
0 | 53 |
by (rtac (equals0I RS disjCI RS allI) 1); |
435 | 54 |
by (res_inst_tac [ ("Z", "Z") ] prem 1); |
55 |
by (ALLGOALS (fast_tac ZF_cs)); |
|
760 | 56 |
qed "wf_onI"; |
0 | 57 |
|
435 | 58 |
(*If r allows well-founded induction over A then wf[A](r) |
59 |
Premise is equivalent to |
|
60 |
!!B. ALL x:A. (ALL y. <y,x>: r --> y:B) --> x:B ==> A<=B *) |
|
61 |
val [prem] = goal WF.thy |
|
62 |
"[| !!y B. [| ALL x:A. (ALL y:A. <y,x>:r --> y:B) --> x:B; y:A \ |
|
63 |
\ |] ==> y:B |] \ |
|
64 |
\ ==> wf[A](r)"; |
|
437 | 65 |
by (rtac wf_onI 1); |
435 | 66 |
by (res_inst_tac [ ("c", "u") ] (prem RS DiffE) 1); |
67 |
by (contr_tac 3); |
|
0 | 68 |
by (fast_tac ZF_cs 2); |
69 |
by (fast_tac ZF_cs 1); |
|
760 | 70 |
qed "wf_onI2"; |
0 | 71 |
|
72 |
||
73 |
(** Well-founded Induction **) |
|
74 |
||
75 |
(*Consider the least z in domain(r) Un {a} such that P(z) does not hold...*) |
|
494 | 76 |
val [major,minor] = goalw WF.thy [wf_def] |
0 | 77 |
"[| wf(r); \ |
78 |
\ !!x.[| ALL y. <y,x>: r --> P(y) |] ==> P(x) \ |
|
79 |
\ |] ==> P(a)"; |
|
80 |
by (res_inst_tac [ ("x", "{z:domain(r) Un {a}. ~P(z)}") ] (major RS allE) 1); |
|
81 |
by (etac disjE 1); |
|
494 | 82 |
by (fast_tac (ZF_cs addEs [equalityE]) 1); |
83 |
by (asm_full_simp_tac (ZF_ss addsimps [domainI]) 1); |
|
0 | 84 |
by (etac bexE 1); |
494 | 85 |
by (dtac minor 1); |
0 | 86 |
by (fast_tac ZF_cs 1); |
760 | 87 |
qed "wf_induct"; |
0 | 88 |
|
89 |
(*Perform induction on i, then prove the wf(r) subgoal using prems. *) |
|
90 |
fun wf_ind_tac a prems i = |
|
91 |
EVERY [res_inst_tac [("a",a)] wf_induct i, |
|
1461 | 92 |
rename_last_tac a ["1"] (i+1), |
93 |
ares_tac prems i]; |
|
0 | 94 |
|
485 | 95 |
(*The form of this rule is designed to match wfI*) |
0 | 96 |
val wfr::amem::prems = goal WF.thy |
97 |
"[| wf(r); a:A; field(r)<=A; \ |
|
98 |
\ !!x.[| x: A; ALL y. <y,x>: r --> P(y) |] ==> P(x) \ |
|
99 |
\ |] ==> P(a)"; |
|
100 |
by (rtac (amem RS rev_mp) 1); |
|
101 |
by (wf_ind_tac "a" [wfr] 1); |
|
102 |
by (rtac impI 1); |
|
103 |
by (eresolve_tac prems 1); |
|
104 |
by (fast_tac (ZF_cs addIs (prems RL [subsetD])) 1); |
|
760 | 105 |
qed "wf_induct2"; |
0 | 106 |
|
435 | 107 |
goal ZF.thy "!!r A. field(r Int A*A) <= A"; |
108 |
by (fast_tac ZF_cs 1); |
|
760 | 109 |
qed "field_Int_square"; |
435 | 110 |
|
111 |
val wfr::amem::prems = goalw WF.thy [wf_on_def] |
|
1461 | 112 |
"[| wf[A](r); a:A; \ |
113 |
\ !!x.[| x: A; ALL y:A. <y,x>: r --> P(y) |] ==> P(x) \ |
|
435 | 114 |
\ |] ==> P(a)"; |
115 |
by (rtac ([wfr, amem, field_Int_square] MRS wf_induct2) 1); |
|
116 |
by (REPEAT (ares_tac prems 1)); |
|
117 |
by (fast_tac ZF_cs 1); |
|
760 | 118 |
qed "wf_on_induct"; |
435 | 119 |
|
120 |
fun wf_on_ind_tac a prems i = |
|
121 |
EVERY [res_inst_tac [("a",a)] wf_on_induct i, |
|
1461 | 122 |
rename_last_tac a ["1"] (i+2), |
123 |
REPEAT (ares_tac prems i)]; |
|
435 | 124 |
|
125 |
(*If r allows well-founded induction then wf(r)*) |
|
126 |
val [subs,indhyp] = goal WF.thy |
|
127 |
"[| field(r)<=A; \ |
|
128 |
\ !!y B. [| ALL x:A. (ALL y:A. <y,x>:r --> y:B) --> x:B; y:A \ |
|
129 |
\ |] ==> y:B |] \ |
|
130 |
\ ==> wf(r)"; |
|
437 | 131 |
by (rtac ([wf_onI2, subs] MRS (wf_on_subset_A RS wf_on_field_imp_wf)) 1); |
435 | 132 |
by (REPEAT (ares_tac [indhyp] 1)); |
760 | 133 |
qed "wfI"; |
435 | 134 |
|
135 |
||
136 |
(*** Properties of well-founded relations ***) |
|
137 |
||
138 |
goal WF.thy "!!r. wf(r) ==> <a,a> ~: r"; |
|
139 |
by (wf_ind_tac "a" [] 1); |
|
140 |
by (fast_tac ZF_cs 1); |
|
760 | 141 |
qed "wf_not_refl"; |
435 | 142 |
|
143 |
goal WF.thy "!!r. [| wf(r); <a,x>:r; <x,a>:r |] ==> P"; |
|
144 |
by (subgoal_tac "ALL x. <a,x>:r --> <x,a>:r --> P" 1); |
|
145 |
by (wf_ind_tac "a" [] 2); |
|
0 | 146 |
by (fast_tac ZF_cs 2); |
435 | 147 |
by (fast_tac FOL_cs 1); |
760 | 148 |
qed "wf_asym"; |
0 | 149 |
|
435 | 150 |
goal WF.thy "!!r. [| wf[A](r); a: A |] ==> <a,a> ~: r"; |
151 |
by (wf_on_ind_tac "a" [] 1); |
|
152 |
by (fast_tac ZF_cs 1); |
|
760 | 153 |
qed "wf_on_not_refl"; |
435 | 154 |
|
155 |
goal WF.thy "!!r. [| wf[A](r); <a,b>:r; <b,a>:r; a:A; b:A |] ==> P"; |
|
156 |
by (subgoal_tac "ALL y:A. <a,y>:r --> <y,a>:r --> P" 1); |
|
157 |
by (wf_on_ind_tac "a" [] 2); |
|
158 |
by (fast_tac ZF_cs 2); |
|
159 |
by (fast_tac ZF_cs 1); |
|
760 | 160 |
qed "wf_on_asym"; |
435 | 161 |
|
162 |
(*Needed to prove well_ordI. Could also reason that wf[A](r) means |
|
163 |
wf(r Int A*A); thus wf( (r Int A*A)^+ ) and use wf_not_refl *) |
|
164 |
goal WF.thy |
|
165 |
"!!r. [| wf[A](r); <a,b>:r; <b,c>:r; <c,a>:r; a:A; b:A; c:A |] ==> P"; |
|
166 |
by (subgoal_tac |
|
167 |
"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 (fast_tac ZF_cs 2); |
|
170 |
by (fast_tac ZF_cs 1); |
|
760 | 171 |
qed "wf_on_chain3"; |
435 | 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 WF.thy |
|
179 |
"[| wf[A](r); r-``A <= A |] ==> wf[A](r^+)"; |
|
437 | 180 |
by (rtac wf_onI2 1); |
435 | 181 |
by (bchain_tac 1); |
182 |
by (eres_inst_tac [("a","y")] (wfr RS wf_on_induct) 1); |
|
183 |
by (rtac (impI RS ballI) 1); |
|
0 | 184 |
by (etac tranclE 1); |
435 | 185 |
by (etac (bspec RS mp) 1 THEN assume_tac 1); |
0 | 186 |
by (fast_tac ZF_cs 1); |
435 | 187 |
by (cut_facts_tac [subs] 1); |
188 |
(*astar_tac is slightly faster*) |
|
189 |
by (best_tac ZF_cs 1); |
|
760 | 190 |
qed "wf_on_trancl"; |
435 | 191 |
|
192 |
goal WF.thy "!!r. wf(r) ==> wf(r^+)"; |
|
193 |
by (asm_full_simp_tac (ZF_ss addsimps [wf_iff_wf_on_field]) 1); |
|
437 | 194 |
by (rtac (trancl_type RS field_rel_subset RSN (2, wf_on_subset_A)) 1); |
195 |
by (etac wf_on_trancl 1); |
|
0 | 196 |
by (fast_tac ZF_cs 1); |
760 | 197 |
qed "wf_trancl"; |
0 | 198 |
|
435 | 199 |
|
200 |
||
0 | 201 |
(** r-``{a} is the set of everything under a in r **) |
202 |
||
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
203 |
bind_thm ("underI", (vimage_singleton_iff RS iffD2)); |
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
204 |
bind_thm ("underD", (vimage_singleton_iff RS iffD1)); |
0 | 205 |
|
206 |
(** is_recfun **) |
|
207 |
||
208 |
val [major] = goalw WF.thy [is_recfun_def] |
|
209 |
"is_recfun(r,a,H,f) ==> f: r-``{a} -> range(f)"; |
|
210 |
by (rtac (major RS ssubst) 1); |
|
211 |
by (rtac (lamI RS rangeI RS lam_type) 1); |
|
212 |
by (assume_tac 1); |
|
760 | 213 |
qed "is_recfun_type"; |
0 | 214 |
|
215 |
val [isrec,rel] = goalw WF.thy [is_recfun_def] |
|
216 |
"[| is_recfun(r,a,H,f); <x,a>:r |] ==> f`x = H(x, restrict(f,r-``{x}))"; |
|
443
10884e64c241
added parentheses made necessary by new constrain precedence
clasohm
parents:
437
diff
changeset
|
217 |
by (res_inst_tac [("P", "%x.?t(x) = (?u::i)")] (isrec RS ssubst) 1); |
0 | 218 |
by (rtac (rel RS underI RS beta) 1); |
760 | 219 |
qed "apply_recfun"; |
0 | 220 |
|
221 |
(*eresolve_tac transD solves <a,b>:r using transitivity AT MOST ONCE |
|
222 |
spec RS mp instantiates induction hypotheses*) |
|
223 |
fun indhyp_tac hyps = |
|
6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset
|
224 |
resolve_tac (TrueI::refl::hyps) ORELSE' |
0 | 225 |
(cut_facts_tac hyps THEN' |
226 |
DEPTH_SOLVE_1 o (ares_tac [TrueI, ballI] ORELSE' |
|
1461 | 227 |
eresolve_tac [underD, transD, spec RS mp])); |
0 | 228 |
|
6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset
|
229 |
(*** NOTE! some simplifications need a different solver!! ***) |
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset
|
230 |
val wf_super_ss = ZF_ss setsolver indhyp_tac; |
0 | 231 |
|
232 |
val prems = goalw WF.thy [is_recfun_def] |
|
233 |
"[| wf(r); trans(r); is_recfun(r,a,H,f); is_recfun(r,b,H,g) |] ==> \ |
|
234 |
\ <x,a>:r --> <x,b>:r --> f`x=g`x"; |
|
235 |
by (cut_facts_tac prems 1); |
|
236 |
by (wf_ind_tac "x" prems 1); |
|
237 |
by (REPEAT (rtac impI 1 ORELSE etac ssubst 1)); |
|
238 |
by (rewtac restrict_def); |
|
6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset
|
239 |
by (asm_simp_tac (wf_super_ss addsimps [vimage_singleton_iff]) 1); |
760 | 240 |
qed "is_recfun_equal_lemma"; |
782
200a16083201
added bind_thm for theorems defined by "standard ..."
clasohm
parents:
760
diff
changeset
|
241 |
bind_thm ("is_recfun_equal", (is_recfun_equal_lemma RS mp RS mp)); |
0 | 242 |
|
243 |
val prems as [wfr,transr,recf,recg,_] = goal WF.thy |
|
244 |
"[| wf(r); trans(r); \ |
|
245 |
\ is_recfun(r,a,H,f); is_recfun(r,b,H,g); <b,a>:r |] ==> \ |
|
246 |
\ restrict(f, r-``{b}) = g"; |
|
247 |
by (cut_facts_tac prems 1); |
|
248 |
by (rtac (consI1 RS restrict_type RS fun_extension) 1); |
|
249 |
by (etac is_recfun_type 1); |
|
250 |
by (ALLGOALS |
|
6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset
|
251 |
(asm_simp_tac (wf_super_ss addsimps |
1461 | 252 |
[ [wfr,transr,recf,recg] MRS is_recfun_equal ]))); |
760 | 253 |
qed "is_recfun_cut"; |
0 | 254 |
|
255 |
(*** Main Existence Lemma ***) |
|
256 |
||
257 |
val prems = goal WF.thy |
|
258 |
"[| wf(r); trans(r); is_recfun(r,a,H,f); is_recfun(r,a,H,g) |] ==> f=g"; |
|
259 |
by (cut_facts_tac prems 1); |
|
260 |
by (rtac fun_extension 1); |
|
261 |
by (REPEAT (ares_tac [is_recfun_equal] 1 |
|
262 |
ORELSE eresolve_tac [is_recfun_type,underD] 1)); |
|
760 | 263 |
qed "is_recfun_functional"; |
0 | 264 |
|
265 |
(*If some f satisfies is_recfun(r,a,H,-) then so does the_recfun(r,a,H) *) |
|
266 |
val prems = goalw WF.thy [the_recfun_def] |
|
267 |
"[| is_recfun(r,a,H,f); wf(r); trans(r) |] \ |
|
268 |
\ ==> is_recfun(r, a, H, the_recfun(r,a,H))"; |
|
269 |
by (rtac (ex1I RS theI) 1); |
|
270 |
by (REPEAT (ares_tac (prems@[is_recfun_functional]) 1)); |
|
760 | 271 |
qed "is_the_recfun"; |
0 | 272 |
|
273 |
val prems = goal WF.thy |
|
274 |
"[| wf(r); trans(r) |] ==> is_recfun(r, a, H, the_recfun(r,a,H))"; |
|
275 |
by (cut_facts_tac prems 1); |
|
276 |
by (wf_ind_tac "a" prems 1); |
|
277 |
by (res_inst_tac [("f", "lam y: r-``{a1}. wftrec(r,y,H)")] is_the_recfun 1); |
|
278 |
by (REPEAT (assume_tac 2)); |
|
279 |
by (rewrite_goals_tac [is_recfun_def, wftrec_def]); |
|
280 |
(*Applying the substitution: must keep the quantified assumption!!*) |
|
6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset
|
281 |
by (REPEAT (dtac underD 1 ORELSE resolve_tac [refl, lam_cong] 1)); |
0 | 282 |
by (fold_tac [is_recfun_def]); |
6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset
|
283 |
by (rtac (consI1 RS restrict_type RSN (2,fun_extension) RS subst_context) 1); |
0 | 284 |
by (rtac is_recfun_type 1); |
285 |
by (ALLGOALS |
|
6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset
|
286 |
(asm_simp_tac |
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset
|
287 |
(wf_super_ss addsimps [underI RS beta, apply_recfun, is_recfun_cut]))); |
760 | 288 |
qed "unfold_the_recfun"; |
0 | 289 |
|
290 |
||
291 |
(*** Unfolding wftrec ***) |
|
292 |
||
293 |
val prems = goal WF.thy |
|
294 |
"[| wf(r); trans(r); <b,a>:r |] ==> \ |
|
295 |
\ restrict(the_recfun(r,a,H), r-``{b}) = the_recfun(r,b,H)"; |
|
296 |
by (REPEAT (ares_tac (prems @ [is_recfun_cut, unfold_the_recfun]) 1)); |
|
760 | 297 |
qed "the_recfun_cut"; |
0 | 298 |
|
299 |
(*NOT SUITABLE FOR REWRITING since it is recursive!*) |
|
6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset
|
300 |
goalw WF.thy [wftrec_def] |
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset
|
301 |
"!!r. [| wf(r); trans(r) |] ==> \ |
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset
|
302 |
\ wftrec(r,a,H) = H(a, lam x: r-``{a}. wftrec(r,x,H))"; |
0 | 303 |
by (rtac (rewrite_rule [is_recfun_def] unfold_the_recfun RS ssubst) 1); |
6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset
|
304 |
by (ALLGOALS (asm_simp_tac |
1461 | 305 |
(ZF_ss addsimps [vimage_singleton_iff RS iff_sym, the_recfun_cut]))); |
760 | 306 |
qed "wftrec"; |
0 | 307 |
|
308 |
(** Removal of the premise trans(r) **) |
|
309 |
||
310 |
(*NOT SUITABLE FOR REWRITING since it is recursive!*) |
|
311 |
val [wfr] = goalw WF.thy [wfrec_def] |
|
312 |
"wf(r) ==> wfrec(r,a,H) = H(a, lam x:r-``{a}. wfrec(r,x,H))"; |
|
313 |
by (rtac (wfr RS wf_trancl RS wftrec RS ssubst) 1); |
|
314 |
by (rtac trans_trancl 1); |
|
6
8ce8c4d13d4d
Installation of new simplifier for ZF. Deleted all congruence rules not
lcp
parents:
0
diff
changeset
|
315 |
by (rtac (vimage_pair_mono RS restrict_lam_eq RS subst_context) 1); |
0 | 316 |
by (etac r_into_trancl 1); |
317 |
by (rtac subset_refl 1); |
|
760 | 318 |
qed "wfrec"; |
0 | 319 |
|
320 |
(*This form avoids giant explosions in proofs. NOTE USE OF == *) |
|
321 |
val rew::prems = goal WF.thy |
|
322 |
"[| !!x. h(x)==wfrec(r,x,H); wf(r) |] ==> \ |
|
323 |
\ h(a) = H(a, lam x: r-``{a}. h(x))"; |
|
324 |
by (rewtac rew); |
|
325 |
by (REPEAT (resolve_tac (prems@[wfrec]) 1)); |
|
760 | 326 |
qed "def_wfrec"; |
0 | 327 |
|
328 |
val prems = goal WF.thy |
|
329 |
"[| wf(r); a:A; field(r)<=A; \ |
|
330 |
\ !!x u. [| x: A; u: Pi(r-``{x}, B) |] ==> H(x,u) : B(x) \ |
|
331 |
\ |] ==> wfrec(r,a,H) : B(a)"; |
|
332 |
by (res_inst_tac [("a","a")] wf_induct2 1); |
|
333 |
by (rtac (wfrec RS ssubst) 4); |
|
334 |
by (REPEAT (ares_tac (prems@[lam_type]) 1 |
|
335 |
ORELSE eresolve_tac [spec RS mp, underD] 1)); |
|
760 | 336 |
qed "wfrec_type"; |
435 | 337 |
|
338 |
||
339 |
goalw WF.thy [wf_on_def, wfrec_on_def] |
|
340 |
"!!A r. [| wf[A](r); a: A |] ==> \ |
|
341 |
\ wfrec[A](r,a,H) = H(a, lam x: (r-``{a}) Int A. wfrec[A](r,x,H))"; |
|
437 | 342 |
by (etac (wfrec RS trans) 1); |
435 | 343 |
by (asm_simp_tac (ZF_ss addsimps [vimage_Int_square, cons_subset_iff]) 1); |
760 | 344 |
qed "wfrec_on"; |
435 | 345 |