author | paulson |
Fri, 21 Aug 1998 16:14:34 +0200 | |
changeset 5359 | bd539b72d484 |
parent 5321 | f8848433d240 |
child 9907 | 473a6604da94 |
permissions | -rw-r--r-- |
1461 | 1 |
(* Title: ZF/fixedpt.ML |
0 | 2 |
ID: $Id$ |
1461 | 3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
0 | 4 |
Copyright 1992 University of Cambridge |
5 |
||
5321 | 6 |
Least and greatest fixed points; the Knaster-Tarski Theorem |
0 | 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 |
||
5321 | 15 |
val prems = Goalw [bnd_mono_def] |
0 | 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)); |
|
760 | 21 |
qed "bnd_monoI"; |
0 | 22 |
|
5321 | 23 |
Goalw [bnd_mono_def] "bnd_mono(D,h) ==> h(D) <= D"; |
24 |
by (etac conjunct1 1); |
|
760 | 25 |
qed "bnd_monoD1"; |
0 | 26 |
|
5321 | 27 |
Goalw [bnd_mono_def] "[| bnd_mono(D,h); W<=X; X<=D |] ==> h(W) <= h(X)"; |
28 |
by (Blast_tac 1); |
|
760 | 29 |
qed "bnd_monoD2"; |
0 | 30 |
|
31 |
val [major,minor] = goal Fixedpt.thy |
|
32 |
"[| bnd_mono(D,h); X<=D |] ==> h(X) <= D"; |
|
33 |
by (rtac (major RS bnd_monoD2 RS subset_trans) 1); |
|
34 |
by (rtac (major RS bnd_monoD1) 3); |
|
35 |
by (rtac minor 1); |
|
36 |
by (rtac subset_refl 1); |
|
760 | 37 |
qed "bnd_mono_subset"; |
0 | 38 |
|
5137 | 39 |
Goal "[| bnd_mono(D,h); A <= D; B <= D |] ==> \ |
0 | 40 |
\ h(A) Un h(B) <= h(A Un B)"; |
41 |
by (REPEAT (ares_tac [Un_upper1, Un_upper2, Un_least] 1 |
|
42 |
ORELSE etac bnd_monoD2 1)); |
|
760 | 43 |
qed "bnd_mono_Un"; |
0 | 44 |
|
45 |
(*Useful??*) |
|
5137 | 46 |
Goal "[| bnd_mono(D,h); A <= D; B <= D |] ==> \ |
0 | 47 |
\ h(A Int B) <= h(A) Int h(B)"; |
48 |
by (REPEAT (ares_tac [Int_lower1, Int_lower2, Int_greatest] 1 |
|
49 |
ORELSE etac bnd_monoD2 1)); |
|
760 | 50 |
qed "bnd_mono_Int"; |
0 | 51 |
|
52 |
(**** Proof of Knaster-Tarski Theorem for the lfp ****) |
|
53 |
||
54 |
(*lfp is contained in each pre-fixedpoint*) |
|
5067 | 55 |
Goalw [lfp_def] |
5147
825877190618
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5137
diff
changeset
|
56 |
"[| h(A) <= A; A<=D |] ==> lfp(D,h) <= A"; |
3016 | 57 |
by (Blast_tac 1); |
744 | 58 |
(*or by (rtac (PowI RS CollectI RS Inter_lower) 1); *) |
760 | 59 |
qed "lfp_lowerbound"; |
0 | 60 |
|
61 |
(*Unfolding the defn of Inter dispenses with the premise bnd_mono(D,h)!*) |
|
5067 | 62 |
Goalw [lfp_def,Inter_def] "lfp(D,h) <= D"; |
3016 | 63 |
by (Blast_tac 1); |
760 | 64 |
qed "lfp_subset"; |
0 | 65 |
|
66 |
(*Used in datatype package*) |
|
67 |
val [rew] = goal Fixedpt.thy "A==lfp(D,h) ==> A <= D"; |
|
68 |
by (rewtac rew); |
|
69 |
by (rtac lfp_subset 1); |
|
760 | 70 |
qed "def_lfp_subset"; |
0 | 71 |
|
5321 | 72 |
val prems = Goalw [lfp_def] |
0 | 73 |
"[| h(D) <= D; !!X. [| h(X) <= X; X<=D |] ==> A<=X |] ==> \ |
74 |
\ A <= lfp(D,h)"; |
|
14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
0
diff
changeset
|
75 |
by (rtac (Pow_top RS CollectI RS Inter_greatest) 1); |
0 | 76 |
by (REPEAT (ares_tac prems 1 ORELSE eresolve_tac [CollectE,PowD] 1)); |
760 | 77 |
qed "lfp_greatest"; |
0 | 78 |
|
79 |
val hmono::prems = goal Fixedpt.thy |
|
80 |
"[| bnd_mono(D,h); h(A)<=A; A<=D |] ==> h(lfp(D,h)) <= A"; |
|
81 |
by (rtac (hmono RS bnd_monoD2 RS subset_trans) 1); |
|
82 |
by (rtac lfp_lowerbound 1); |
|
83 |
by (REPEAT (resolve_tac prems 1)); |
|
760 | 84 |
qed "lfp_lemma1"; |
0 | 85 |
|
5321 | 86 |
Goal "bnd_mono(D,h) ==> h(lfp(D,h)) <= lfp(D,h)"; |
0 | 87 |
by (rtac (bnd_monoD1 RS lfp_greatest) 1); |
88 |
by (rtac lfp_lemma1 2); |
|
5321 | 89 |
by (REPEAT (assume_tac 1)); |
760 | 90 |
qed "lfp_lemma2"; |
0 | 91 |
|
92 |
val [hmono] = goal Fixedpt.thy |
|
93 |
"bnd_mono(D,h) ==> lfp(D,h) <= h(lfp(D,h))"; |
|
94 |
by (rtac lfp_lowerbound 1); |
|
95 |
by (rtac (hmono RS bnd_monoD2) 1); |
|
96 |
by (rtac (hmono RS lfp_lemma2) 1); |
|
97 |
by (rtac (hmono RS bnd_mono_subset) 2); |
|
98 |
by (REPEAT (rtac lfp_subset 1)); |
|
760 | 99 |
qed "lfp_lemma3"; |
0 | 100 |
|
5321 | 101 |
Goal "bnd_mono(D,h) ==> lfp(D,h) = h(lfp(D,h))"; |
102 |
by (REPEAT (ares_tac [equalityI,lfp_lemma2,lfp_lemma3] 1)); |
|
760 | 103 |
qed "lfp_Tarski"; |
0 | 104 |
|
105 |
(*Definition form, to control unfolding*) |
|
106 |
val [rew,mono] = goal Fixedpt.thy |
|
107 |
"[| A==lfp(D,h); bnd_mono(D,h) |] ==> A = h(A)"; |
|
108 |
by (rewtac rew); |
|
109 |
by (rtac (mono RS lfp_Tarski) 1); |
|
760 | 110 |
qed "def_lfp_Tarski"; |
0 | 111 |
|
112 |
(*** General induction rule for least fixedpoints ***) |
|
113 |
||
5321 | 114 |
val [hmono,indstep] = Goal |
0 | 115 |
"[| bnd_mono(D,h); !!x. x : h(Collect(lfp(D,h),P)) ==> P(x) \ |
116 |
\ |] ==> h(Collect(lfp(D,h),P)) <= Collect(lfp(D,h),P)"; |
|
117 |
by (rtac subsetI 1); |
|
118 |
by (rtac CollectI 1); |
|
119 |
by (etac indstep 2); |
|
120 |
by (rtac (hmono RS lfp_lemma2 RS subsetD) 1); |
|
121 |
by (rtac (hmono RS bnd_monoD2 RS subsetD) 1); |
|
122 |
by (REPEAT (ares_tac [Collect_subset, lfp_subset] 1)); |
|
760 | 123 |
qed "Collect_is_pre_fixedpt"; |
0 | 124 |
|
125 |
(*This rule yields an induction hypothesis in which the components of a |
|
126 |
data structure may be assumed to be elements of lfp(D,h)*) |
|
5321 | 127 |
val prems = Goal |
1461 | 128 |
"[| bnd_mono(D,h); a : lfp(D,h); \ |
129 |
\ !!x. x : h(Collect(lfp(D,h),P)) ==> P(x) \ |
|
0 | 130 |
\ |] ==> P(a)"; |
131 |
by (rtac (Collect_is_pre_fixedpt RS lfp_lowerbound RS subsetD RS CollectD2) 1); |
|
132 |
by (rtac (lfp_subset RS (Collect_subset RS subset_trans)) 3); |
|
133 |
by (REPEAT (ares_tac prems 1)); |
|
760 | 134 |
qed "induct"; |
0 | 135 |
|
136 |
(*Definition form, to control unfolding*) |
|
5321 | 137 |
val rew::prems = Goal |
0 | 138 |
"[| A == lfp(D,h); bnd_mono(D,h); a:A; \ |
139 |
\ !!x. x : h(Collect(A,P)) ==> P(x) \ |
|
140 |
\ |] ==> P(a)"; |
|
141 |
by (rtac induct 1); |
|
142 |
by (REPEAT (ares_tac (map (rewrite_rule [rew]) prems) 1)); |
|
760 | 143 |
qed "def_induct"; |
0 | 144 |
|
145 |
(*This version is useful when "A" is not a subset of D; |
|
146 |
second premise could simply be h(D Int A) <= D or !!X. X<=D ==> h(X)<=D *) |
|
147 |
val [hsub,hmono] = goal Fixedpt.thy |
|
148 |
"[| h(D Int A) <= A; bnd_mono(D,h) |] ==> lfp(D,h) <= A"; |
|
149 |
by (rtac (lfp_lowerbound RS subset_trans) 1); |
|
150 |
by (rtac (hmono RS bnd_mono_subset RS Int_greatest) 1); |
|
151 |
by (REPEAT (resolve_tac [hsub,Int_lower1,Int_lower2] 1)); |
|
760 | 152 |
qed "lfp_Int_lowerbound"; |
0 | 153 |
|
154 |
(*Monotonicity of lfp, where h precedes i under a domain-like partial order |
|
155 |
monotonicity of h is not strictly necessary; h must be bounded by D*) |
|
5321 | 156 |
val [hmono,imono,subhi] = Goal |
1461 | 157 |
"[| bnd_mono(D,h); bnd_mono(E,i); \ |
0 | 158 |
\ !!X. X<=D ==> h(X) <= i(X) |] ==> lfp(D,h) <= lfp(E,i)"; |
14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
0
diff
changeset
|
159 |
by (rtac (bnd_monoD1 RS lfp_greatest) 1); |
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
0
diff
changeset
|
160 |
by (rtac imono 1); |
0 | 161 |
by (rtac (hmono RSN (2, lfp_Int_lowerbound)) 1); |
162 |
by (rtac (Int_lower1 RS subhi RS subset_trans) 1); |
|
163 |
by (rtac (imono RS bnd_monoD2 RS subset_trans) 1); |
|
164 |
by (REPEAT (ares_tac [Int_lower2] 1)); |
|
760 | 165 |
qed "lfp_mono"; |
0 | 166 |
|
167 |
(*This (unused) version illustrates that monotonicity is not really needed, |
|
168 |
but both lfp's must be over the SAME set D; Inter is anti-monotonic!*) |
|
5321 | 169 |
val [isubD,subhi] = Goal |
0 | 170 |
"[| i(D) <= D; !!X. X<=D ==> h(X) <= i(X) |] ==> lfp(D,h) <= lfp(D,i)"; |
14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
0
diff
changeset
|
171 |
by (rtac lfp_greatest 1); |
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
0
diff
changeset
|
172 |
by (rtac isubD 1); |
0 | 173 |
by (rtac lfp_lowerbound 1); |
14
1c0926788772
ex/{bin.ML,comb.ML,prop.ML}: replaced NewSext by Syntax.simple_sext
lcp
parents:
0
diff
changeset
|
174 |
by (etac (subhi RS subset_trans) 1); |
0 | 175 |
by (REPEAT (assume_tac 1)); |
760 | 176 |
qed "lfp_mono2"; |
0 | 177 |
|
178 |
||
179 |
(**** Proof of Knaster-Tarski Theorem for the gfp ****) |
|
180 |
||
181 |
(*gfp contains each post-fixedpoint that is contained in D*) |
|
5321 | 182 |
Goalw [gfp_def] "[| A <= h(A); A<=D |] ==> A <= gfp(D,h)"; |
0 | 183 |
by (rtac (PowI RS CollectI RS Union_upper) 1); |
5321 | 184 |
by (REPEAT (assume_tac 1)); |
760 | 185 |
qed "gfp_upperbound"; |
0 | 186 |
|
5067 | 187 |
Goalw [gfp_def] "gfp(D,h) <= D"; |
3016 | 188 |
by (Blast_tac 1); |
760 | 189 |
qed "gfp_subset"; |
0 | 190 |
|
191 |
(*Used in datatype package*) |
|
192 |
val [rew] = goal Fixedpt.thy "A==gfp(D,h) ==> A <= D"; |
|
193 |
by (rewtac rew); |
|
194 |
by (rtac gfp_subset 1); |
|
760 | 195 |
qed "def_gfp_subset"; |
0 | 196 |
|
5321 | 197 |
val hmono::prems = Goalw [gfp_def] |
0 | 198 |
"[| bnd_mono(D,h); !!X. [| X <= h(X); X<=D |] ==> X<=A |] ==> \ |
199 |
\ gfp(D,h) <= A"; |
|
200 |
by (fast_tac (subset_cs addIs ((hmono RS bnd_monoD1)::prems)) 1); |
|
760 | 201 |
qed "gfp_least"; |
0 | 202 |
|
203 |
val hmono::prems = goal Fixedpt.thy |
|
204 |
"[| bnd_mono(D,h); A<=h(A); A<=D |] ==> A <= h(gfp(D,h))"; |
|
205 |
by (rtac (hmono RS bnd_monoD2 RSN (2,subset_trans)) 1); |
|
206 |
by (rtac gfp_subset 3); |
|
207 |
by (rtac gfp_upperbound 2); |
|
208 |
by (REPEAT (resolve_tac prems 1)); |
|
760 | 209 |
qed "gfp_lemma1"; |
0 | 210 |
|
5321 | 211 |
Goal "bnd_mono(D,h) ==> gfp(D,h) <= h(gfp(D,h))"; |
0 | 212 |
by (rtac gfp_least 1); |
213 |
by (rtac gfp_lemma1 2); |
|
5321 | 214 |
by (REPEAT (assume_tac 1)); |
760 | 215 |
qed "gfp_lemma2"; |
0 | 216 |
|
217 |
val [hmono] = goal Fixedpt.thy |
|
218 |
"bnd_mono(D,h) ==> h(gfp(D,h)) <= gfp(D,h)"; |
|
219 |
by (rtac gfp_upperbound 1); |
|
220 |
by (rtac (hmono RS bnd_monoD2) 1); |
|
221 |
by (rtac (hmono RS gfp_lemma2) 1); |
|
222 |
by (REPEAT (rtac ([hmono, gfp_subset] MRS bnd_mono_subset) 1)); |
|
760 | 223 |
qed "gfp_lemma3"; |
0 | 224 |
|
5321 | 225 |
Goal "bnd_mono(D,h) ==> gfp(D,h) = h(gfp(D,h))"; |
226 |
by (REPEAT (ares_tac [equalityI,gfp_lemma2,gfp_lemma3] 1)); |
|
760 | 227 |
qed "gfp_Tarski"; |
0 | 228 |
|
229 |
(*Definition form, to control unfolding*) |
|
230 |
val [rew,mono] = goal Fixedpt.thy |
|
231 |
"[| A==gfp(D,h); bnd_mono(D,h) |] ==> A = h(A)"; |
|
232 |
by (rewtac rew); |
|
233 |
by (rtac (mono RS gfp_Tarski) 1); |
|
760 | 234 |
qed "def_gfp_Tarski"; |
0 | 235 |
|
236 |
||
237 |
(*** Coinduction rules for greatest fixed points ***) |
|
238 |
||
239 |
(*weak version*) |
|
5137 | 240 |
Goal "[| a: X; X <= h(X); X <= D |] ==> a : gfp(D,h)"; |
0 | 241 |
by (REPEAT (ares_tac [gfp_upperbound RS subsetD] 1)); |
760 | 242 |
qed "weak_coinduct"; |
0 | 243 |
|
244 |
val [subs_h,subs_D,mono] = goal Fixedpt.thy |
|
245 |
"[| X <= h(X Un gfp(D,h)); X <= D; bnd_mono(D,h) |] ==> \ |
|
246 |
\ X Un gfp(D,h) <= h(X Un gfp(D,h))"; |
|
247 |
by (rtac (subs_h RS Un_least) 1); |
|
248 |
by (rtac (mono RS gfp_lemma2 RS subset_trans) 1); |
|
249 |
by (rtac (Un_upper2 RS subset_trans) 1); |
|
250 |
by (rtac ([mono, subs_D, gfp_subset] MRS bnd_mono_Un) 1); |
|
760 | 251 |
qed "coinduct_lemma"; |
0 | 252 |
|
253 |
(*strong version*) |
|
5147
825877190618
More tidying and removal of "\!\!... from Goal commands
paulson
parents:
5137
diff
changeset
|
254 |
Goal "[| bnd_mono(D,h); a: X; X <= h(X Un gfp(D,h)); X <= D |] ==> \ |
0 | 255 |
\ a : gfp(D,h)"; |
647
fb7345cccddc
ZF/Fixedpt/coinduct: modified proof to suppress deep unification
lcp
parents:
484
diff
changeset
|
256 |
by (rtac weak_coinduct 1); |
fb7345cccddc
ZF/Fixedpt/coinduct: modified proof to suppress deep unification
lcp
parents:
484
diff
changeset
|
257 |
by (etac coinduct_lemma 2); |
0 | 258 |
by (REPEAT (ares_tac [gfp_subset, UnI1, Un_least] 1)); |
760 | 259 |
qed "coinduct"; |
0 | 260 |
|
261 |
(*Definition form, to control unfolding*) |
|
262 |
val rew::prems = goal Fixedpt.thy |
|
263 |
"[| A == gfp(D,h); bnd_mono(D,h); a: X; X <= h(X Un A); X <= D |] ==> \ |
|
264 |
\ a : A"; |
|
265 |
by (rewtac rew); |
|
266 |
by (rtac coinduct 1); |
|
267 |
by (REPEAT (ares_tac (map (rewrite_rule [rew]) prems) 1)); |
|
760 | 268 |
qed "def_coinduct"; |
0 | 269 |
|
270 |
(*Lemma used immediately below!*) |
|
5321 | 271 |
val [subsA,XimpP] = Goal |
0 | 272 |
"[| X <= A; !!z. z:X ==> P(z) |] ==> X <= Collect(A,P)"; |
273 |
by (rtac (subsA RS subsetD RS CollectI RS subsetI) 1); |
|
274 |
by (assume_tac 1); |
|
275 |
by (etac XimpP 1); |
|
760 | 276 |
qed "subset_Collect"; |
0 | 277 |
|
278 |
(*The version used in the induction/coinduction package*) |
|
5321 | 279 |
val prems = Goal |
0 | 280 |
"[| A == gfp(D, %w. Collect(D,P(w))); bnd_mono(D, %w. Collect(D,P(w))); \ |
281 |
\ a: X; X <= D; !!z. z: X ==> P(X Un A, z) |] ==> \ |
|
282 |
\ a : A"; |
|
283 |
by (rtac def_coinduct 1); |
|
284 |
by (REPEAT (ares_tac (subset_Collect::prems) 1)); |
|
760 | 285 |
qed "def_Collect_coinduct"; |
0 | 286 |
|
287 |
(*Monotonicity of gfp!*) |
|
5321 | 288 |
val [hmono,subde,subhi] = Goal |
1461 | 289 |
"[| bnd_mono(D,h); D <= E; \ |
0 | 290 |
\ !!X. X<=D ==> h(X) <= i(X) |] ==> gfp(D,h) <= gfp(E,i)"; |
291 |
by (rtac gfp_upperbound 1); |
|
292 |
by (rtac (hmono RS gfp_lemma2 RS subset_trans) 1); |
|
293 |
by (rtac (gfp_subset RS subhi) 1); |
|
294 |
by (rtac ([gfp_subset, subde] MRS subset_trans) 1); |
|
760 | 295 |
qed "gfp_mono"; |
0 | 296 |