|
1 (* Title: ZF/fixedpt.ML |
|
2 ID: $Id$ |
|
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 Copyright 1992 University of Cambridge |
|
5 |
|
6 For fixedpt.thy. Least and greatest fixed points; the Knaster-Tarski Theorem |
|
7 |
|
8 Proved in the lattice of subsets of D, namely Pow(D), with Inter as glb |
|
9 *) |
|
10 |
|
11 open Fixedpt; |
|
12 |
|
13 (*** Monotone operators ***) |
|
14 |
|
15 val prems = goalw Fixedpt.thy [bnd_mono_def] |
|
16 "[| h(D)<=D; \ |
|
17 \ !!W X. [| W<=D; X<=D; W<=X |] ==> h(W) <= h(X) \ |
|
18 \ |] ==> bnd_mono(D,h)"; |
|
19 by (REPEAT (ares_tac (prems@[conjI,allI,impI]) 1 |
|
20 ORELSE etac subset_trans 1)); |
|
21 val bnd_monoI = result(); |
|
22 |
|
23 val [major] = goalw Fixedpt.thy [bnd_mono_def] "bnd_mono(D,h) ==> h(D) <= D"; |
|
24 by (rtac (major RS conjunct1) 1); |
|
25 val bnd_monoD1 = result(); |
|
26 |
|
27 val major::prems = goalw Fixedpt.thy [bnd_mono_def] |
|
28 "[| bnd_mono(D,h); W<=X; X<=D |] ==> h(W) <= h(X)"; |
|
29 by (rtac (major RS conjunct2 RS spec RS spec RS mp RS mp) 1); |
|
30 by (REPEAT (resolve_tac prems 1)); |
|
31 val bnd_monoD2 = result(); |
|
32 |
|
33 val [major,minor] = goal Fixedpt.thy |
|
34 "[| bnd_mono(D,h); X<=D |] ==> h(X) <= D"; |
|
35 by (rtac (major RS bnd_monoD2 RS subset_trans) 1); |
|
36 by (rtac (major RS bnd_monoD1) 3); |
|
37 by (rtac minor 1); |
|
38 by (rtac subset_refl 1); |
|
39 val bnd_mono_subset = result(); |
|
40 |
|
41 goal Fixedpt.thy "!!A B. [| bnd_mono(D,h); A <= D; B <= D |] ==> \ |
|
42 \ h(A) Un h(B) <= h(A Un B)"; |
|
43 by (REPEAT (ares_tac [Un_upper1, Un_upper2, Un_least] 1 |
|
44 ORELSE etac bnd_monoD2 1)); |
|
45 val bnd_mono_Un = result(); |
|
46 |
|
47 (*Useful??*) |
|
48 goal Fixedpt.thy "!!A B. [| bnd_mono(D,h); A <= D; B <= D |] ==> \ |
|
49 \ h(A Int B) <= h(A) Int h(B)"; |
|
50 by (REPEAT (ares_tac [Int_lower1, Int_lower2, Int_greatest] 1 |
|
51 ORELSE etac bnd_monoD2 1)); |
|
52 val bnd_mono_Int = result(); |
|
53 |
|
54 (**** Proof of Knaster-Tarski Theorem for the lfp ****) |
|
55 |
|
56 (*lfp is contained in each pre-fixedpoint*) |
|
57 val prems = goalw Fixedpt.thy [lfp_def] |
|
58 "[| h(A) <= A; A<=D |] ==> lfp(D,h) <= A"; |
|
59 by (rtac (PowI RS CollectI RS Inter_lower) 1); |
|
60 by (REPEAT (resolve_tac prems 1)); |
|
61 val lfp_lowerbound = result(); |
|
62 |
|
63 (*Unfolding the defn of Inter dispenses with the premise bnd_mono(D,h)!*) |
|
64 goalw Fixedpt.thy [lfp_def,Inter_def] "lfp(D,h) <= D"; |
|
65 by (fast_tac ZF_cs 1); |
|
66 val lfp_subset = result(); |
|
67 |
|
68 (*Used in datatype package*) |
|
69 val [rew] = goal Fixedpt.thy "A==lfp(D,h) ==> A <= D"; |
|
70 by (rewtac rew); |
|
71 by (rtac lfp_subset 1); |
|
72 val def_lfp_subset = result(); |
|
73 |
|
74 val subset0_cs = FOL_cs |
|
75 addSIs [ballI, InterI, CollectI, PowI, empty_subsetI] |
|
76 addIs [bexI, UnionI, ReplaceI, RepFunI] |
|
77 addSEs [bexE, make_elim PowD, UnionE, ReplaceE, RepFunE, |
|
78 CollectE, emptyE] |
|
79 addEs [rev_ballE, InterD, make_elim InterD, subsetD]; |
|
80 |
|
81 val subset_cs = subset0_cs |
|
82 addSIs [subset_refl,cons_subsetI,subset_consI,Union_least,UN_least,Un_least, |
|
83 Inter_greatest,Int_greatest,RepFun_subset] |
|
84 addSIs [Un_upper1,Un_upper2,Int_lower1,Int_lower2] |
|
85 addIs [Union_upper,Inter_lower] |
|
86 addSEs [cons_subsetE]; |
|
87 |
|
88 val prems = goalw Fixedpt.thy [lfp_def] |
|
89 "[| h(D) <= D; !!X. [| h(X) <= X; X<=D |] ==> A<=X |] ==> \ |
|
90 \ A <= lfp(D,h)"; |
|
91 br (Pow_top RS CollectI RS Inter_greatest) 1; |
|
92 by (REPEAT (ares_tac prems 1 ORELSE eresolve_tac [CollectE,PowD] 1)); |
|
93 val lfp_greatest = result(); |
|
94 |
|
95 val hmono::prems = goal Fixedpt.thy |
|
96 "[| bnd_mono(D,h); h(A)<=A; A<=D |] ==> h(lfp(D,h)) <= A"; |
|
97 by (rtac (hmono RS bnd_monoD2 RS subset_trans) 1); |
|
98 by (rtac lfp_lowerbound 1); |
|
99 by (REPEAT (resolve_tac prems 1)); |
|
100 val lfp_lemma1 = result(); |
|
101 |
|
102 val [hmono] = goal Fixedpt.thy |
|
103 "bnd_mono(D,h) ==> h(lfp(D,h)) <= lfp(D,h)"; |
|
104 by (rtac (bnd_monoD1 RS lfp_greatest) 1); |
|
105 by (rtac lfp_lemma1 2); |
|
106 by (REPEAT (ares_tac [hmono] 1)); |
|
107 val lfp_lemma2 = result(); |
|
108 |
|
109 val [hmono] = goal Fixedpt.thy |
|
110 "bnd_mono(D,h) ==> lfp(D,h) <= h(lfp(D,h))"; |
|
111 by (rtac lfp_lowerbound 1); |
|
112 by (rtac (hmono RS bnd_monoD2) 1); |
|
113 by (rtac (hmono RS lfp_lemma2) 1); |
|
114 by (rtac (hmono RS bnd_mono_subset) 2); |
|
115 by (REPEAT (rtac lfp_subset 1)); |
|
116 val lfp_lemma3 = result(); |
|
117 |
|
118 val prems = goal Fixedpt.thy |
|
119 "bnd_mono(D,h) ==> lfp(D,h) = h(lfp(D,h))"; |
|
120 by (REPEAT (resolve_tac (prems@[equalityI,lfp_lemma2,lfp_lemma3]) 1)); |
|
121 val lfp_Tarski = result(); |
|
122 |
|
123 (*Definition form, to control unfolding*) |
|
124 val [rew,mono] = goal Fixedpt.thy |
|
125 "[| A==lfp(D,h); bnd_mono(D,h) |] ==> A = h(A)"; |
|
126 by (rewtac rew); |
|
127 by (rtac (mono RS lfp_Tarski) 1); |
|
128 val def_lfp_Tarski = result(); |
|
129 |
|
130 (*** General induction rule for least fixedpoints ***) |
|
131 |
|
132 val [hmono,indstep] = goal Fixedpt.thy |
|
133 "[| bnd_mono(D,h); !!x. x : h(Collect(lfp(D,h),P)) ==> P(x) \ |
|
134 \ |] ==> h(Collect(lfp(D,h),P)) <= Collect(lfp(D,h),P)"; |
|
135 by (rtac subsetI 1); |
|
136 by (rtac CollectI 1); |
|
137 by (etac indstep 2); |
|
138 by (rtac (hmono RS lfp_lemma2 RS subsetD) 1); |
|
139 by (rtac (hmono RS bnd_monoD2 RS subsetD) 1); |
|
140 by (REPEAT (ares_tac [Collect_subset, lfp_subset] 1)); |
|
141 val Collect_is_pre_fixedpt = result(); |
|
142 |
|
143 (*This rule yields an induction hypothesis in which the components of a |
|
144 data structure may be assumed to be elements of lfp(D,h)*) |
|
145 val prems = goal Fixedpt.thy |
|
146 "[| bnd_mono(D,h); a : lfp(D,h); \ |
|
147 \ !!x. x : h(Collect(lfp(D,h),P)) ==> P(x) \ |
|
148 \ |] ==> P(a)"; |
|
149 by (rtac (Collect_is_pre_fixedpt RS lfp_lowerbound RS subsetD RS CollectD2) 1); |
|
150 by (rtac (lfp_subset RS (Collect_subset RS subset_trans)) 3); |
|
151 by (REPEAT (ares_tac prems 1)); |
|
152 val induct = result(); |
|
153 |
|
154 (*Definition form, to control unfolding*) |
|
155 val rew::prems = goal Fixedpt.thy |
|
156 "[| A == lfp(D,h); bnd_mono(D,h); a:A; \ |
|
157 \ !!x. x : h(Collect(A,P)) ==> P(x) \ |
|
158 \ |] ==> P(a)"; |
|
159 by (rtac induct 1); |
|
160 by (REPEAT (ares_tac (map (rewrite_rule [rew]) prems) 1)); |
|
161 val def_induct = result(); |
|
162 |
|
163 (*This version is useful when "A" is not a subset of D; |
|
164 second premise could simply be h(D Int A) <= D or !!X. X<=D ==> h(X)<=D *) |
|
165 val [hsub,hmono] = goal Fixedpt.thy |
|
166 "[| h(D Int A) <= A; bnd_mono(D,h) |] ==> lfp(D,h) <= A"; |
|
167 by (rtac (lfp_lowerbound RS subset_trans) 1); |
|
168 by (rtac (hmono RS bnd_mono_subset RS Int_greatest) 1); |
|
169 by (REPEAT (resolve_tac [hsub,Int_lower1,Int_lower2] 1)); |
|
170 val lfp_Int_lowerbound = result(); |
|
171 |
|
172 (*Monotonicity of lfp, where h precedes i under a domain-like partial order |
|
173 monotonicity of h is not strictly necessary; h must be bounded by D*) |
|
174 val [hmono,imono,subhi] = goal Fixedpt.thy |
|
175 "[| bnd_mono(D,h); bnd_mono(E,i); \ |
|
176 \ !!X. X<=D ==> h(X) <= i(X) |] ==> lfp(D,h) <= lfp(E,i)"; |
|
177 br (bnd_monoD1 RS lfp_greatest) 1; |
|
178 br imono 1; |
|
179 by (rtac (hmono RSN (2, lfp_Int_lowerbound)) 1); |
|
180 by (rtac (Int_lower1 RS subhi RS subset_trans) 1); |
|
181 by (rtac (imono RS bnd_monoD2 RS subset_trans) 1); |
|
182 by (REPEAT (ares_tac [Int_lower2] 1)); |
|
183 val lfp_mono = result(); |
|
184 |
|
185 (*This (unused) version illustrates that monotonicity is not really needed, |
|
186 but both lfp's must be over the SAME set D; Inter is anti-monotonic!*) |
|
187 val [isubD,subhi] = goal Fixedpt.thy |
|
188 "[| i(D) <= D; !!X. X<=D ==> h(X) <= i(X) |] ==> lfp(D,h) <= lfp(D,i)"; |
|
189 br lfp_greatest 1; |
|
190 br isubD 1; |
|
191 by (rtac lfp_lowerbound 1); |
|
192 be (subhi RS subset_trans) 1; |
|
193 by (REPEAT (assume_tac 1)); |
|
194 val lfp_mono2 = result(); |
|
195 |
|
196 |
|
197 (**** Proof of Knaster-Tarski Theorem for the gfp ****) |
|
198 |
|
199 (*gfp contains each post-fixedpoint that is contained in D*) |
|
200 val prems = goalw Fixedpt.thy [gfp_def] |
|
201 "[| A <= h(A); A<=D |] ==> A <= gfp(D,h)"; |
|
202 by (rtac (PowI RS CollectI RS Union_upper) 1); |
|
203 by (REPEAT (resolve_tac prems 1)); |
|
204 val gfp_upperbound = result(); |
|
205 |
|
206 goalw Fixedpt.thy [gfp_def] "gfp(D,h) <= D"; |
|
207 by (fast_tac ZF_cs 1); |
|
208 val gfp_subset = result(); |
|
209 |
|
210 (*Used in datatype package*) |
|
211 val [rew] = goal Fixedpt.thy "A==gfp(D,h) ==> A <= D"; |
|
212 by (rewtac rew); |
|
213 by (rtac gfp_subset 1); |
|
214 val def_gfp_subset = result(); |
|
215 |
|
216 val hmono::prems = goalw Fixedpt.thy [gfp_def] |
|
217 "[| bnd_mono(D,h); !!X. [| X <= h(X); X<=D |] ==> X<=A |] ==> \ |
|
218 \ gfp(D,h) <= A"; |
|
219 by (fast_tac (subset_cs addIs ((hmono RS bnd_monoD1)::prems)) 1); |
|
220 val gfp_least = result(); |
|
221 |
|
222 val hmono::prems = goal Fixedpt.thy |
|
223 "[| bnd_mono(D,h); A<=h(A); A<=D |] ==> A <= h(gfp(D,h))"; |
|
224 by (rtac (hmono RS bnd_monoD2 RSN (2,subset_trans)) 1); |
|
225 by (rtac gfp_subset 3); |
|
226 by (rtac gfp_upperbound 2); |
|
227 by (REPEAT (resolve_tac prems 1)); |
|
228 val gfp_lemma1 = result(); |
|
229 |
|
230 val [hmono] = goal Fixedpt.thy |
|
231 "bnd_mono(D,h) ==> gfp(D,h) <= h(gfp(D,h))"; |
|
232 by (rtac gfp_least 1); |
|
233 by (rtac gfp_lemma1 2); |
|
234 by (REPEAT (ares_tac [hmono] 1)); |
|
235 val gfp_lemma2 = result(); |
|
236 |
|
237 val [hmono] = goal Fixedpt.thy |
|
238 "bnd_mono(D,h) ==> h(gfp(D,h)) <= gfp(D,h)"; |
|
239 by (rtac gfp_upperbound 1); |
|
240 by (rtac (hmono RS bnd_monoD2) 1); |
|
241 by (rtac (hmono RS gfp_lemma2) 1); |
|
242 by (REPEAT (rtac ([hmono, gfp_subset] MRS bnd_mono_subset) 1)); |
|
243 val gfp_lemma3 = result(); |
|
244 |
|
245 val prems = goal Fixedpt.thy |
|
246 "bnd_mono(D,h) ==> gfp(D,h) = h(gfp(D,h))"; |
|
247 by (REPEAT (resolve_tac (prems@[equalityI,gfp_lemma2,gfp_lemma3]) 1)); |
|
248 val gfp_Tarski = result(); |
|
249 |
|
250 (*Definition form, to control unfolding*) |
|
251 val [rew,mono] = goal Fixedpt.thy |
|
252 "[| A==gfp(D,h); bnd_mono(D,h) |] ==> A = h(A)"; |
|
253 by (rewtac rew); |
|
254 by (rtac (mono RS gfp_Tarski) 1); |
|
255 val def_gfp_Tarski = result(); |
|
256 |
|
257 |
|
258 (*** Coinduction rules for greatest fixed points ***) |
|
259 |
|
260 (*weak version*) |
|
261 goal Fixedpt.thy "!!X h. [| a: X; X <= h(X); X <= D |] ==> a : gfp(D,h)"; |
|
262 by (REPEAT (ares_tac [gfp_upperbound RS subsetD] 1)); |
|
263 val weak_coinduct = result(); |
|
264 |
|
265 val [subs_h,subs_D,mono] = goal Fixedpt.thy |
|
266 "[| X <= h(X Un gfp(D,h)); X <= D; bnd_mono(D,h) |] ==> \ |
|
267 \ X Un gfp(D,h) <= h(X Un gfp(D,h))"; |
|
268 by (rtac (subs_h RS Un_least) 1); |
|
269 by (rtac (mono RS gfp_lemma2 RS subset_trans) 1); |
|
270 by (rtac (Un_upper2 RS subset_trans) 1); |
|
271 by (rtac ([mono, subs_D, gfp_subset] MRS bnd_mono_Un) 1); |
|
272 val coinduct_lemma = result(); |
|
273 |
|
274 (*strong version*) |
|
275 goal Fixedpt.thy |
|
276 "!!X D. [| bnd_mono(D,h); a: X; X <= h(X Un gfp(D,h)); X <= D |] ==> \ |
|
277 \ a : gfp(D,h)"; |
|
278 by (rtac (coinduct_lemma RSN (2, weak_coinduct)) 1); |
|
279 by (REPEAT (ares_tac [gfp_subset, UnI1, Un_least] 1)); |
|
280 val coinduct = result(); |
|
281 |
|
282 (*Definition form, to control unfolding*) |
|
283 val rew::prems = goal Fixedpt.thy |
|
284 "[| A == gfp(D,h); bnd_mono(D,h); a: X; X <= h(X Un A); X <= D |] ==> \ |
|
285 \ a : A"; |
|
286 by (rewtac rew); |
|
287 by (rtac coinduct 1); |
|
288 by (REPEAT (ares_tac (map (rewrite_rule [rew]) prems) 1)); |
|
289 val def_coinduct = result(); |
|
290 |
|
291 (*Lemma used immediately below!*) |
|
292 val [subsA,XimpP] = goal ZF.thy |
|
293 "[| X <= A; !!z. z:X ==> P(z) |] ==> X <= Collect(A,P)"; |
|
294 by (rtac (subsA RS subsetD RS CollectI RS subsetI) 1); |
|
295 by (assume_tac 1); |
|
296 by (etac XimpP 1); |
|
297 val subset_Collect = result(); |
|
298 |
|
299 (*The version used in the induction/coinduction package*) |
|
300 val prems = goal Fixedpt.thy |
|
301 "[| A == gfp(D, %w. Collect(D,P(w))); bnd_mono(D, %w. Collect(D,P(w))); \ |
|
302 \ a: X; X <= D; !!z. z: X ==> P(X Un A, z) |] ==> \ |
|
303 \ a : A"; |
|
304 by (rtac def_coinduct 1); |
|
305 by (REPEAT (ares_tac (subset_Collect::prems) 1)); |
|
306 val def_Collect_coinduct = result(); |
|
307 |
|
308 (*Monotonicity of gfp!*) |
|
309 val [hmono,subde,subhi] = goal Fixedpt.thy |
|
310 "[| bnd_mono(D,h); D <= E; \ |
|
311 \ !!X. X<=D ==> h(X) <= i(X) |] ==> gfp(D,h) <= gfp(E,i)"; |
|
312 by (rtac gfp_upperbound 1); |
|
313 by (rtac (hmono RS gfp_lemma2 RS subset_trans) 1); |
|
314 by (rtac (gfp_subset RS subhi) 1); |
|
315 by (rtac ([gfp_subset, subde] MRS subset_trans) 1); |
|
316 val gfp_mono = result(); |
|
317 |