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