0
|
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();
|