72 (* ------------------------------------------------------------------------ *) |
72 (* ------------------------------------------------------------------------ *) |
73 (* monotone functions map chains to chains *) |
73 (* monotone functions map chains to chains *) |
74 (* ------------------------------------------------------------------------ *) |
74 (* ------------------------------------------------------------------------ *) |
75 |
75 |
76 qed_goal "ch2ch_monofun" Cont.thy |
76 qed_goal "ch2ch_monofun" Cont.thy |
77 "[| monofun(f); is_chain(Y) |] ==> is_chain(%i. f(Y(i)))" |
77 "[| monofun(f); is_chain(Y) |] ==> is_chain(%i. f(Y(i)))" |
78 (fn prems => |
78 (fn prems => |
79 [ |
79 [ |
80 (cut_facts_tac prems 1), |
80 (cut_facts_tac prems 1), |
81 (rtac is_chainI 1), |
81 (rtac is_chainI 1), |
82 (rtac allI 1), |
82 (rtac allI 1), |
83 (etac (monofunE RS spec RS spec RS mp) 1), |
83 (etac (monofunE RS spec RS spec RS mp) 1), |
84 (etac (is_chainE RS spec) 1) |
84 (etac (is_chainE RS spec) 1) |
85 ]); |
85 ]); |
86 |
86 |
87 (* ------------------------------------------------------------------------ *) |
87 (* ------------------------------------------------------------------------ *) |
88 (* monotone functions map upper bound to upper bounds *) |
88 (* monotone functions map upper bound to upper bounds *) |
89 (* ------------------------------------------------------------------------ *) |
89 (* ------------------------------------------------------------------------ *) |
90 |
90 |
91 qed_goal "ub2ub_monofun" Cont.thy |
91 qed_goal "ub2ub_monofun" Cont.thy |
92 "[| monofun(f); range(Y) <| u|] ==> range(%i.f(Y(i))) <| f(u)" |
92 "[| monofun(f); range(Y) <| u|] ==> range(%i.f(Y(i))) <| f(u)" |
93 (fn prems => |
93 (fn prems => |
94 [ |
94 [ |
95 (cut_facts_tac prems 1), |
95 (cut_facts_tac prems 1), |
96 (rtac ub_rangeI 1), |
96 (rtac ub_rangeI 1), |
97 (rtac allI 1), |
97 (rtac allI 1), |
98 (etac (monofunE RS spec RS spec RS mp) 1), |
98 (etac (monofunE RS spec RS spec RS mp) 1), |
99 (etac (ub_rangeE RS spec) 1) |
99 (etac (ub_rangeE RS spec) 1) |
100 ]); |
100 ]); |
101 |
101 |
102 (* ------------------------------------------------------------------------ *) |
102 (* ------------------------------------------------------------------------ *) |
103 (* left to right: monofun(f) & contlub(f) ==> cont(f) *) |
103 (* left to right: monofun(f) & contlub(f) ==> cont(f) *) |
104 (* ------------------------------------------------------------------------ *) |
104 (* ------------------------------------------------------------------------ *) |
105 |
105 |
106 qed_goalw "monocontlub2cont" Cont.thy [cont] |
106 qed_goalw "monocontlub2cont" Cont.thy [cont] |
107 "[|monofun(f);contlub(f)|] ==> cont(f)" |
107 "[|monofun(f);contlub(f)|] ==> cont(f)" |
108 (fn prems => |
108 (fn prems => |
109 [ |
109 [ |
110 (cut_facts_tac prems 1), |
110 (cut_facts_tac prems 1), |
111 (strip_tac 1), |
111 (strip_tac 1), |
112 (rtac thelubE 1), |
112 (rtac thelubE 1), |
113 (etac ch2ch_monofun 1), |
113 (etac ch2ch_monofun 1), |
114 (atac 1), |
114 (atac 1), |
115 (etac (contlubE RS spec RS mp RS sym) 1), |
115 (etac (contlubE RS spec RS mp RS sym) 1), |
116 (atac 1) |
116 (atac 1) |
117 ]); |
117 ]); |
118 |
118 |
119 (* ------------------------------------------------------------------------ *) |
119 (* ------------------------------------------------------------------------ *) |
120 (* first a lemma about binary chains *) |
120 (* first a lemma about binary chains *) |
121 (* ------------------------------------------------------------------------ *) |
121 (* ------------------------------------------------------------------------ *) |
122 |
122 |
123 qed_goal "binchain_cont" Cont.thy |
123 qed_goal "binchain_cont" Cont.thy |
124 "[| cont(f); x << y |] ==> range(%i. f(if i = 0 then x else y)) <<| f(y)" |
124 "[| cont(f); x << y |] ==> range(%i. f(if i = 0 then x else y)) <<| f(y)" |
125 (fn prems => |
125 (fn prems => |
126 [ |
126 [ |
127 (cut_facts_tac prems 1), |
127 (cut_facts_tac prems 1), |
128 (rtac subst 1), |
128 (rtac subst 1), |
129 (etac (contE RS spec RS mp) 2), |
129 (etac (contE RS spec RS mp) 2), |
130 (etac bin_chain 2), |
130 (etac bin_chain 2), |
131 (res_inst_tac [("y","y")] arg_cong 1), |
131 (res_inst_tac [("y","y")] arg_cong 1), |
132 (etac (lub_bin_chain RS thelubI) 1) |
132 (etac (lub_bin_chain RS thelubI) 1) |
133 ]); |
133 ]); |
134 |
134 |
135 (* ------------------------------------------------------------------------ *) |
135 (* ------------------------------------------------------------------------ *) |
136 (* right to left: cont(f) ==> monofun(f) & contlub(f) *) |
136 (* right to left: cont(f) ==> monofun(f) & contlub(f) *) |
137 (* part1: cont(f) ==> monofun(f *) |
137 (* part1: cont(f) ==> monofun(f *) |
138 (* ------------------------------------------------------------------------ *) |
138 (* ------------------------------------------------------------------------ *) |
139 |
139 |
140 qed_goalw "cont2mono" Cont.thy [monofun] |
140 qed_goalw "cont2mono" Cont.thy [monofun] |
141 "cont(f) ==> monofun(f)" |
141 "cont(f) ==> monofun(f)" |
142 (fn prems => |
142 (fn prems => |
143 [ |
143 [ |
144 (cut_facts_tac prems 1), |
144 (cut_facts_tac prems 1), |
145 (strip_tac 1), |
145 (strip_tac 1), |
146 (res_inst_tac [("s","if 0 = 0 then x else y")] subst 1), |
146 (res_inst_tac [("s","if 0 = 0 then x else y")] subst 1), |
147 (rtac (binchain_cont RS is_ub_lub) 2), |
147 (rtac (binchain_cont RS is_ub_lub) 2), |
148 (atac 2), |
148 (atac 2), |
149 (atac 2), |
149 (atac 2), |
150 (Simp_tac 1) |
150 (Simp_tac 1) |
151 ]); |
151 ]); |
152 |
152 |
153 (* ------------------------------------------------------------------------ *) |
153 (* ------------------------------------------------------------------------ *) |
154 (* right to left: cont(f) ==> monofun(f) & contlub(f) *) |
154 (* right to left: cont(f) ==> monofun(f) & contlub(f) *) |
155 (* part2: cont(f) ==> contlub(f) *) |
155 (* part2: cont(f) ==> contlub(f) *) |
156 (* ------------------------------------------------------------------------ *) |
156 (* ------------------------------------------------------------------------ *) |
157 |
157 |
158 qed_goalw "cont2contlub" Cont.thy [contlub] |
158 qed_goalw "cont2contlub" Cont.thy [contlub] |
159 "cont(f) ==> contlub(f)" |
159 "cont(f) ==> contlub(f)" |
160 (fn prems => |
160 (fn prems => |
161 [ |
161 [ |
162 (cut_facts_tac prems 1), |
162 (cut_facts_tac prems 1), |
163 (strip_tac 1), |
163 (strip_tac 1), |
164 (rtac (thelubI RS sym) 1), |
164 (rtac (thelubI RS sym) 1), |
165 (etac (contE RS spec RS mp) 1), |
165 (etac (contE RS spec RS mp) 1), |
166 (atac 1) |
166 (atac 1) |
167 ]); |
167 ]); |
168 |
168 |
169 (* ------------------------------------------------------------------------ *) |
169 (* ------------------------------------------------------------------------ *) |
170 (* The following results are about a curried function that is monotone *) |
170 (* The following results are about a curried function that is monotone *) |
171 (* in both arguments *) |
171 (* in both arguments *) |
172 (* ------------------------------------------------------------------------ *) |
172 (* ------------------------------------------------------------------------ *) |
173 |
173 |
174 qed_goal "ch2ch_MF2L" Cont.thy |
174 qed_goal "ch2ch_MF2L" Cont.thy |
175 "[|monofun(MF2); is_chain(F)|] ==> is_chain(%i. MF2 (F i) x)" |
175 "[|monofun(MF2); is_chain(F)|] ==> is_chain(%i. MF2 (F i) x)" |
176 (fn prems => |
176 (fn prems => |
177 [ |
177 [ |
178 (cut_facts_tac prems 1), |
178 (cut_facts_tac prems 1), |
179 (etac (ch2ch_monofun RS ch2ch_fun) 1), |
179 (etac (ch2ch_monofun RS ch2ch_fun) 1), |
180 (atac 1) |
180 (atac 1) |
181 ]); |
181 ]); |
182 |
182 |
183 |
183 |
184 qed_goal "ch2ch_MF2R" Cont.thy |
184 qed_goal "ch2ch_MF2R" Cont.thy |
185 "[|monofun(MF2(f)); is_chain(Y)|] ==> is_chain(%i. MF2 f (Y i))" |
185 "[|monofun(MF2(f)); is_chain(Y)|] ==> is_chain(%i. MF2 f (Y i))" |
186 (fn prems => |
186 (fn prems => |
187 [ |
187 [ |
188 (cut_facts_tac prems 1), |
188 (cut_facts_tac prems 1), |
189 (etac ch2ch_monofun 1), |
189 (etac ch2ch_monofun 1), |
190 (atac 1) |
190 (atac 1) |
191 ]); |
191 ]); |
192 |
192 |
193 qed_goal "ch2ch_MF2LR" Cont.thy |
193 qed_goal "ch2ch_MF2LR" Cont.thy |
194 "[|monofun(MF2); !f.monofun(MF2(f)); is_chain(F); is_chain(Y)|] ==> \ |
194 "[|monofun(MF2); !f.monofun(MF2(f)); is_chain(F); is_chain(Y)|] ==> \ |
195 \ is_chain(%i. MF2(F(i))(Y(i)))" |
195 \ is_chain(%i. MF2(F(i))(Y(i)))" |
196 (fn prems => |
196 (fn prems => |
197 [ |
197 [ |
198 (cut_facts_tac prems 1), |
198 (cut_facts_tac prems 1), |
199 (rtac is_chainI 1), |
199 (rtac is_chainI 1), |
200 (strip_tac 1 ), |
200 (strip_tac 1 ), |
201 (rtac trans_less 1), |
201 (rtac trans_less 1), |
202 (etac (ch2ch_MF2L RS is_chainE RS spec) 1), |
202 (etac (ch2ch_MF2L RS is_chainE RS spec) 1), |
203 (atac 1), |
203 (atac 1), |
204 ((rtac (monofunE RS spec RS spec RS mp) 1) THEN (etac spec 1)), |
204 ((rtac (monofunE RS spec RS spec RS mp) 1) THEN (etac spec 1)), |
205 (etac (is_chainE RS spec) 1) |
205 (etac (is_chainE RS spec) 1) |
206 ]); |
206 ]); |
207 |
207 |
208 |
208 |
209 qed_goal "ch2ch_lubMF2R" Cont.thy |
209 qed_goal "ch2ch_lubMF2R" Cont.thy |
210 "[|monofun(MF2::('a::po=>'b::po=>'c::pcpo));\ |
210 "[|monofun(MF2::('a::po=>'b::po=>'c::pcpo));\ |
211 \ !f.monofun(MF2(f)::('b::po=>'c::pcpo));\ |
211 \ !f.monofun(MF2(f)::('b::po=>'c::pcpo));\ |
212 \ is_chain(F);is_chain(Y)|] ==> \ |
212 \ is_chain(F);is_chain(Y)|] ==> \ |
213 \ is_chain(%j. lub(range(%i. MF2 (F j) (Y i))))" |
213 \ is_chain(%j. lub(range(%i. MF2 (F j) (Y i))))" |
214 (fn prems => |
214 (fn prems => |
215 [ |
215 [ |
216 (cut_facts_tac prems 1), |
216 (cut_facts_tac prems 1), |
217 (rtac (lub_mono RS allI RS is_chainI) 1), |
217 (rtac (lub_mono RS allI RS is_chainI) 1), |
218 ((rtac ch2ch_MF2R 1) THEN (etac spec 1)), |
218 ((rtac ch2ch_MF2R 1) THEN (etac spec 1)), |
219 (atac 1), |
219 (atac 1), |
220 ((rtac ch2ch_MF2R 1) THEN (etac spec 1)), |
220 ((rtac ch2ch_MF2R 1) THEN (etac spec 1)), |
221 (atac 1), |
221 (atac 1), |
222 (strip_tac 1), |
222 (strip_tac 1), |
223 (rtac (is_chainE RS spec) 1), |
223 (rtac (is_chainE RS spec) 1), |
224 (etac ch2ch_MF2L 1), |
224 (etac ch2ch_MF2L 1), |
225 (atac 1) |
225 (atac 1) |
226 ]); |
226 ]); |
227 |
227 |
228 |
228 |
229 qed_goal "ch2ch_lubMF2L" Cont.thy |
229 qed_goal "ch2ch_lubMF2L" Cont.thy |
230 "[|monofun(MF2::('a::po=>'b::po=>'c::pcpo));\ |
230 "[|monofun(MF2::('a::po=>'b::po=>'c::pcpo));\ |
231 \ !f.monofun(MF2(f)::('b::po=>'c::pcpo));\ |
231 \ !f.monofun(MF2(f)::('b::po=>'c::pcpo));\ |
232 \ is_chain(F);is_chain(Y)|] ==> \ |
232 \ is_chain(F);is_chain(Y)|] ==> \ |
233 \ is_chain(%i. lub(range(%j. MF2 (F j) (Y i))))" |
233 \ is_chain(%i. lub(range(%j. MF2 (F j) (Y i))))" |
234 (fn prems => |
234 (fn prems => |
235 [ |
235 [ |
236 (cut_facts_tac prems 1), |
236 (cut_facts_tac prems 1), |
237 (rtac (lub_mono RS allI RS is_chainI) 1), |
237 (rtac (lub_mono RS allI RS is_chainI) 1), |
238 (etac ch2ch_MF2L 1), |
238 (etac ch2ch_MF2L 1), |
239 (atac 1), |
239 (atac 1), |
240 (etac ch2ch_MF2L 1), |
240 (etac ch2ch_MF2L 1), |
241 (atac 1), |
241 (atac 1), |
242 (strip_tac 1), |
242 (strip_tac 1), |
243 (rtac (is_chainE RS spec) 1), |
243 (rtac (is_chainE RS spec) 1), |
244 ((rtac ch2ch_MF2R 1) THEN (etac spec 1)), |
244 ((rtac ch2ch_MF2R 1) THEN (etac spec 1)), |
245 (atac 1) |
245 (atac 1) |
246 ]); |
246 ]); |
247 |
247 |
248 |
248 |
249 qed_goal "lub_MF2_mono" Cont.thy |
249 qed_goal "lub_MF2_mono" Cont.thy |
250 "[|monofun(MF2::('a::po=>'b::po=>'c::pcpo));\ |
250 "[|monofun(MF2::('a::po=>'b::po=>'c::pcpo));\ |
251 \ !f.monofun(MF2(f)::('b::po=>'c::pcpo));\ |
251 \ !f.monofun(MF2(f)::('b::po=>'c::pcpo));\ |
252 \ is_chain(F)|] ==> \ |
252 \ is_chain(F)|] ==> \ |
253 \ monofun(% x.lub(range(% j.MF2 (F j) (x))))" |
253 \ monofun(% x.lub(range(% j.MF2 (F j) (x))))" |
254 (fn prems => |
254 (fn prems => |
255 [ |
255 [ |
256 (cut_facts_tac prems 1), |
256 (cut_facts_tac prems 1), |
257 (rtac monofunI 1), |
257 (rtac monofunI 1), |
258 (strip_tac 1), |
258 (strip_tac 1), |
259 (rtac lub_mono 1), |
259 (rtac lub_mono 1), |
260 (etac ch2ch_MF2L 1), |
260 (etac ch2ch_MF2L 1), |
261 (atac 1), |
261 (atac 1), |
262 (etac ch2ch_MF2L 1), |
262 (etac ch2ch_MF2L 1), |
263 (atac 1), |
263 (atac 1), |
264 (strip_tac 1), |
264 (strip_tac 1), |
265 ((rtac (monofunE RS spec RS spec RS mp) 1) THEN (etac spec 1)), |
265 ((rtac (monofunE RS spec RS spec RS mp) 1) THEN (etac spec 1)), |
266 (atac 1) |
266 (atac 1) |
267 ]); |
267 ]); |
268 |
268 |
269 qed_goal "ex_lubMF2" Cont.thy |
269 qed_goal "ex_lubMF2" Cont.thy |
270 "[|monofun(MF2::('a::po=>'b::po=>'c::pcpo));\ |
270 "[|monofun(MF2::('a::po=>'b::po=>'c::pcpo));\ |
271 \ !f.monofun(MF2(f)::('b::po=>'c::pcpo));\ |
271 \ !f.monofun(MF2(f)::('b::po=>'c::pcpo));\ |
272 \ is_chain(F); is_chain(Y)|] ==> \ |
272 \ is_chain(F); is_chain(Y)|] ==> \ |
273 \ lub(range(%j. lub(range(%i. MF2(F j) (Y i))))) =\ |
273 \ lub(range(%j. lub(range(%i. MF2(F j) (Y i))))) =\ |
274 \ lub(range(%i. lub(range(%j. MF2(F j) (Y i)))))" |
274 \ lub(range(%i. lub(range(%j. MF2(F j) (Y i)))))" |
275 (fn prems => |
275 (fn prems => |
276 [ |
276 [ |
277 (cut_facts_tac prems 1), |
277 (cut_facts_tac prems 1), |
278 (rtac antisym_less 1), |
278 (rtac antisym_less 1), |
279 (rtac (ub_rangeI RSN (2,is_lub_thelub)) 1), |
279 (rtac (ub_rangeI RSN (2,is_lub_thelub)) 1), |
280 (etac ch2ch_lubMF2R 1), |
280 (etac ch2ch_lubMF2R 1), |
281 (REPEAT (atac 1)), |
281 (REPEAT (atac 1)), |
282 (strip_tac 1), |
282 (strip_tac 1), |
283 (rtac lub_mono 1), |
283 (rtac lub_mono 1), |
284 ((rtac ch2ch_MF2R 1) THEN (etac spec 1)), |
284 ((rtac ch2ch_MF2R 1) THEN (etac spec 1)), |
285 (atac 1), |
285 (atac 1), |
286 (etac ch2ch_lubMF2L 1), |
286 (etac ch2ch_lubMF2L 1), |
287 (REPEAT (atac 1)), |
287 (REPEAT (atac 1)), |
288 (strip_tac 1), |
288 (strip_tac 1), |
289 (rtac is_ub_thelub 1), |
289 (rtac is_ub_thelub 1), |
290 (etac ch2ch_MF2L 1), |
290 (etac ch2ch_MF2L 1), |
291 (atac 1), |
291 (atac 1), |
292 (rtac (ub_rangeI RSN (2,is_lub_thelub)) 1), |
292 (rtac (ub_rangeI RSN (2,is_lub_thelub)) 1), |
293 (etac ch2ch_lubMF2L 1), |
293 (etac ch2ch_lubMF2L 1), |
294 (REPEAT (atac 1)), |
294 (REPEAT (atac 1)), |
295 (strip_tac 1), |
295 (strip_tac 1), |
296 (rtac lub_mono 1), |
296 (rtac lub_mono 1), |
297 (etac ch2ch_MF2L 1), |
297 (etac ch2ch_MF2L 1), |
298 (atac 1), |
298 (atac 1), |
299 (etac ch2ch_lubMF2R 1), |
299 (etac ch2ch_lubMF2R 1), |
300 (REPEAT (atac 1)), |
300 (REPEAT (atac 1)), |
301 (strip_tac 1), |
301 (strip_tac 1), |
302 (rtac is_ub_thelub 1), |
302 (rtac is_ub_thelub 1), |
303 ((rtac ch2ch_MF2R 1) THEN (etac spec 1)), |
303 ((rtac ch2ch_MF2R 1) THEN (etac spec 1)), |
304 (atac 1) |
304 (atac 1) |
305 ]); |
305 ]); |
306 |
306 |
307 |
307 |
308 qed_goal "diag_lubMF2_1" Cont.thy |
308 qed_goal "diag_lubMF2_1" Cont.thy |
309 "[|monofun(MF2::('a::po=>'b::po=>'c::pcpo));\ |
309 "[|monofun(MF2::('a::po=>'b::po=>'c::pcpo));\ |
310 \ !f.monofun(MF2(f)::('b::po=>'c::pcpo));\ |
310 \ !f.monofun(MF2(f)::('b::po=>'c::pcpo));\ |
311 \ is_chain(FY);is_chain(TY)|] ==>\ |
311 \ is_chain(FY);is_chain(TY)|] ==>\ |
312 \ lub(range(%i. lub(range(%j. MF2(FY(j))(TY(i)))))) =\ |
312 \ lub(range(%i. lub(range(%j. MF2(FY(j))(TY(i)))))) =\ |
313 \ lub(range(%i. MF2(FY(i))(TY(i))))" |
313 \ lub(range(%i. MF2(FY(i))(TY(i))))" |
314 (fn prems => |
314 (fn prems => |
315 [ |
315 [ |
316 (cut_facts_tac prems 1), |
316 (cut_facts_tac prems 1), |
317 (rtac antisym_less 1), |
317 (rtac antisym_less 1), |
318 (rtac (ub_rangeI RSN (2,is_lub_thelub)) 1), |
318 (rtac (ub_rangeI RSN (2,is_lub_thelub)) 1), |
319 (etac ch2ch_lubMF2L 1), |
319 (etac ch2ch_lubMF2L 1), |
320 (REPEAT (atac 1)), |
320 (REPEAT (atac 1)), |
321 (strip_tac 1 ), |
321 (strip_tac 1 ), |
322 (rtac lub_mono3 1), |
322 (rtac lub_mono3 1), |
323 (etac ch2ch_MF2L 1), |
323 (etac ch2ch_MF2L 1), |
324 (REPEAT (atac 1)), |
324 (REPEAT (atac 1)), |
325 (etac ch2ch_MF2LR 1), |
325 (etac ch2ch_MF2LR 1), |
326 (REPEAT (atac 1)), |
326 (REPEAT (atac 1)), |
327 (rtac allI 1), |
327 (rtac allI 1), |
328 (res_inst_tac [("m","i"),("n","ia")] nat_less_cases 1), |
328 (res_inst_tac [("m","i"),("n","ia")] nat_less_cases 1), |
329 (res_inst_tac [("x","ia")] exI 1), |
329 (res_inst_tac [("x","ia")] exI 1), |
330 (rtac (chain_mono RS mp) 1), |
330 (rtac (chain_mono RS mp) 1), |
331 (etac allE 1), |
331 (etac allE 1), |
332 (etac ch2ch_MF2R 1), |
332 (etac ch2ch_MF2R 1), |
333 (REPEAT (atac 1)), |
333 (REPEAT (atac 1)), |
334 (hyp_subst_tac 1), |
334 (hyp_subst_tac 1), |
335 (res_inst_tac [("x","ia")] exI 1), |
335 (res_inst_tac [("x","ia")] exI 1), |
336 (rtac refl_less 1), |
336 (rtac refl_less 1), |
337 (res_inst_tac [("x","i")] exI 1), |
337 (res_inst_tac [("x","i")] exI 1), |
338 (rtac (chain_mono RS mp) 1), |
338 (rtac (chain_mono RS mp) 1), |
339 (etac ch2ch_MF2L 1), |
339 (etac ch2ch_MF2L 1), |
340 (REPEAT (atac 1)), |
340 (REPEAT (atac 1)), |
341 (rtac lub_mono 1), |
341 (rtac lub_mono 1), |
342 (etac ch2ch_MF2LR 1), |
342 (etac ch2ch_MF2LR 1), |
343 (REPEAT(atac 1)), |
343 (REPEAT(atac 1)), |
344 (etac ch2ch_lubMF2L 1), |
344 (etac ch2ch_lubMF2L 1), |
345 (REPEAT (atac 1)), |
345 (REPEAT (atac 1)), |
346 (strip_tac 1 ), |
346 (strip_tac 1 ), |
347 (rtac is_ub_thelub 1), |
347 (rtac is_ub_thelub 1), |
348 (etac ch2ch_MF2L 1), |
348 (etac ch2ch_MF2L 1), |
349 (atac 1) |
349 (atac 1) |
350 ]); |
350 ]); |
351 |
351 |
352 qed_goal "diag_lubMF2_2" Cont.thy |
352 qed_goal "diag_lubMF2_2" Cont.thy |
353 "[|monofun(MF2::('a::po=>'b::po=>'c::pcpo));\ |
353 "[|monofun(MF2::('a::po=>'b::po=>'c::pcpo));\ |
354 \ !f.monofun(MF2(f)::('b::po=>'c::pcpo));\ |
354 \ !f.monofun(MF2(f)::('b::po=>'c::pcpo));\ |
355 \ is_chain(FY);is_chain(TY)|] ==>\ |
355 \ is_chain(FY);is_chain(TY)|] ==>\ |
356 \ lub(range(%j. lub(range(%i. MF2(FY(j))(TY(i)))))) =\ |
356 \ lub(range(%j. lub(range(%i. MF2(FY(j))(TY(i)))))) =\ |
357 \ lub(range(%i. MF2(FY(i))(TY(i))))" |
357 \ lub(range(%i. MF2(FY(i))(TY(i))))" |
358 (fn prems => |
358 (fn prems => |
359 [ |
359 [ |
360 (cut_facts_tac prems 1), |
360 (cut_facts_tac prems 1), |
361 (rtac trans 1), |
361 (rtac trans 1), |
362 (rtac ex_lubMF2 1), |
362 (rtac ex_lubMF2 1), |
363 (REPEAT (atac 1)), |
363 (REPEAT (atac 1)), |
364 (etac diag_lubMF2_1 1), |
364 (etac diag_lubMF2_1 1), |
365 (REPEAT (atac 1)) |
365 (REPEAT (atac 1)) |
366 ]); |
366 ]); |
367 |
367 |
368 |
368 |
369 |
369 |
370 |
370 |
371 (* ------------------------------------------------------------------------ *) |
371 (* ------------------------------------------------------------------------ *) |
375 |
375 |
376 qed_goal "contlub_CF2" Cont.thy |
376 qed_goal "contlub_CF2" Cont.thy |
377 "[|cont(CF2);!f.cont(CF2(f));is_chain(FY);is_chain(TY)|] ==>\ |
377 "[|cont(CF2);!f.cont(CF2(f));is_chain(FY);is_chain(TY)|] ==>\ |
378 \ CF2(lub(range(FY)))(lub(range(TY))) = lub(range(%i.CF2(FY(i))(TY(i))))" |
378 \ CF2(lub(range(FY)))(lub(range(TY))) = lub(range(%i.CF2(FY(i))(TY(i))))" |
379 (fn prems => |
379 (fn prems => |
380 [ |
380 [ |
381 (cut_facts_tac prems 1), |
381 (cut_facts_tac prems 1), |
382 (rtac ((hd prems) RS cont2contlub RS contlubE RS spec RS mp RS ssubst) 1), |
382 (rtac ((hd prems) RS cont2contlub RS contlubE RS spec RS mp RS ssubst) 1), |
383 (atac 1), |
383 (atac 1), |
384 (rtac (thelub_fun RS ssubst) 1), |
384 (rtac (thelub_fun RS ssubst) 1), |
385 (rtac ((hd prems) RS cont2mono RS ch2ch_monofun) 1), |
385 (rtac ((hd prems) RS cont2mono RS ch2ch_monofun) 1), |
386 (atac 1), |
386 (atac 1), |
387 (rtac trans 1), |
387 (rtac trans 1), |
388 (rtac (((hd (tl prems)) RS spec RS cont2contlub) RS contlubE RS spec RS mp RS ext RS arg_cong RS arg_cong) 1), |
388 (rtac (((hd (tl prems)) RS spec RS cont2contlub) RS contlubE RS spec RS mp RS ext RS arg_cong RS arg_cong) 1), |
389 (atac 1), |
389 (atac 1), |
390 (rtac diag_lubMF2_2 1), |
390 (rtac diag_lubMF2_2 1), |
391 (etac cont2mono 1), |
391 (etac cont2mono 1), |
392 (rtac allI 1), |
392 (rtac allI 1), |
393 (etac allE 1), |
393 (etac allE 1), |
394 (etac cont2mono 1), |
394 (etac cont2mono 1), |
395 (REPEAT (atac 1)) |
395 (REPEAT (atac 1)) |
396 ]); |
396 ]); |
397 |
397 |
398 (* ------------------------------------------------------------------------ *) |
398 (* ------------------------------------------------------------------------ *) |
399 (* The following results are about application for functions in 'a=>'b *) |
399 (* The following results are about application for functions in 'a=>'b *) |
400 (* ------------------------------------------------------------------------ *) |
400 (* ------------------------------------------------------------------------ *) |
401 |
401 |
402 qed_goal "monofun_fun_fun" Cont.thy |
402 qed_goal "monofun_fun_fun" Cont.thy |
403 "f1 << f2 ==> f1(x) << f2(x)" |
403 "f1 << f2 ==> f1(x) << f2(x)" |
404 (fn prems => |
404 (fn prems => |
405 [ |
405 [ |
406 (cut_facts_tac prems 1), |
406 (cut_facts_tac prems 1), |
407 (etac (less_fun RS iffD1 RS spec) 1) |
407 (etac (less_fun RS iffD1 RS spec) 1) |
408 ]); |
408 ]); |
409 |
409 |
410 qed_goal "monofun_fun_arg" Cont.thy |
410 qed_goal "monofun_fun_arg" Cont.thy |
411 "[|monofun(f); x1 << x2|] ==> f(x1) << f(x2)" |
411 "[|monofun(f); x1 << x2|] ==> f(x1) << f(x2)" |
412 (fn prems => |
412 (fn prems => |
413 [ |
413 [ |
414 (cut_facts_tac prems 1), |
414 (cut_facts_tac prems 1), |
415 (etac (monofunE RS spec RS spec RS mp) 1), |
415 (etac (monofunE RS spec RS spec RS mp) 1), |
416 (atac 1) |
416 (atac 1) |
417 ]); |
417 ]); |
418 |
418 |
419 qed_goal "monofun_fun" Cont.thy |
419 qed_goal "monofun_fun" Cont.thy |
420 "[|monofun(f1); monofun(f2); f1 << f2; x1 << x2|] ==> f1(x1) << f2(x2)" |
420 "[|monofun(f1); monofun(f2); f1 << f2; x1 << x2|] ==> f1(x1) << f2(x2)" |
421 (fn prems => |
421 (fn prems => |
422 [ |
422 [ |
423 (cut_facts_tac prems 1), |
423 (cut_facts_tac prems 1), |
424 (rtac trans_less 1), |
424 (rtac trans_less 1), |
425 (etac monofun_fun_arg 1), |
425 (etac monofun_fun_arg 1), |
426 (atac 1), |
426 (atac 1), |
427 (etac monofun_fun_fun 1) |
427 (etac monofun_fun_fun 1) |
428 ]); |
428 ]); |
429 |
429 |
430 |
430 |
431 (* ------------------------------------------------------------------------ *) |
431 (* ------------------------------------------------------------------------ *) |
432 (* The following results are about the propagation of monotonicity and *) |
432 (* The following results are about the propagation of monotonicity and *) |
433 (* continuity *) |
433 (* continuity *) |
434 (* ------------------------------------------------------------------------ *) |
434 (* ------------------------------------------------------------------------ *) |
435 |
435 |
436 qed_goal "mono2mono_MF1L" Cont.thy |
436 qed_goal "mono2mono_MF1L" Cont.thy |
437 "[|monofun(c1)|] ==> monofun(%x. c1 x y)" |
437 "[|monofun(c1)|] ==> monofun(%x. c1 x y)" |
438 (fn prems => |
438 (fn prems => |
439 [ |
439 [ |
440 (cut_facts_tac prems 1), |
440 (cut_facts_tac prems 1), |
441 (rtac monofunI 1), |
441 (rtac monofunI 1), |
442 (strip_tac 1), |
442 (strip_tac 1), |
443 (etac (monofun_fun_arg RS monofun_fun_fun) 1), |
443 (etac (monofun_fun_arg RS monofun_fun_fun) 1), |
444 (atac 1) |
444 (atac 1) |
445 ]); |
445 ]); |
446 |
446 |
447 qed_goal "cont2cont_CF1L" Cont.thy |
447 qed_goal "cont2cont_CF1L" Cont.thy |
448 "[|cont(c1)|] ==> cont(%x. c1 x y)" |
448 "[|cont(c1)|] ==> cont(%x. c1 x y)" |
449 (fn prems => |
449 (fn prems => |
450 [ |
450 [ |
451 (cut_facts_tac prems 1), |
451 (cut_facts_tac prems 1), |
452 (rtac monocontlub2cont 1), |
452 (rtac monocontlub2cont 1), |
453 (etac (cont2mono RS mono2mono_MF1L) 1), |
453 (etac (cont2mono RS mono2mono_MF1L) 1), |
454 (rtac contlubI 1), |
454 (rtac contlubI 1), |
455 (strip_tac 1), |
455 (strip_tac 1), |
456 (rtac ((hd prems) RS cont2contlub RS |
456 (rtac ((hd prems) RS cont2contlub RS |
457 contlubE RS spec RS mp RS ssubst) 1), |
457 contlubE RS spec RS mp RS ssubst) 1), |
458 (atac 1), |
458 (atac 1), |
459 (rtac (thelub_fun RS ssubst) 1), |
459 (rtac (thelub_fun RS ssubst) 1), |
460 (rtac ch2ch_monofun 1), |
460 (rtac ch2ch_monofun 1), |
461 (etac cont2mono 1), |
461 (etac cont2mono 1), |
462 (atac 1), |
462 (atac 1), |
463 (rtac refl 1) |
463 (rtac refl 1) |
464 ]); |
464 ]); |
465 |
465 |
466 (********* Note "(%x.%y.c1 x y) = c1" ***********) |
466 (********* Note "(%x.%y.c1 x y) = c1" ***********) |
467 |
467 |
468 qed_goal "mono2mono_MF1L_rev" Cont.thy |
468 qed_goal "mono2mono_MF1L_rev" Cont.thy |
469 "!y.monofun(%x.c1 x y) ==> monofun(c1)" |
469 "!y.monofun(%x.c1 x y) ==> monofun(c1)" |
470 (fn prems => |
470 (fn prems => |
471 [ |
471 [ |
472 (cut_facts_tac prems 1), |
472 (cut_facts_tac prems 1), |
473 (rtac monofunI 1), |
473 (rtac monofunI 1), |
474 (strip_tac 1), |
474 (strip_tac 1), |
475 (rtac (less_fun RS iffD2) 1), |
475 (rtac (less_fun RS iffD2) 1), |
476 (strip_tac 1), |
476 (strip_tac 1), |
477 (rtac ((hd prems) RS spec RS monofunE RS spec RS spec RS mp) 1), |
477 (rtac ((hd prems) RS spec RS monofunE RS spec RS spec RS mp) 1), |
478 (atac 1) |
478 (atac 1) |
479 ]); |
479 ]); |
480 |
480 |
481 qed_goal "cont2cont_CF1L_rev" Cont.thy |
481 qed_goal "cont2cont_CF1L_rev" Cont.thy |
482 "!y.cont(%x.c1 x y) ==> cont(c1)" |
482 "!y.cont(%x.c1 x y) ==> cont(c1)" |
483 (fn prems => |
483 (fn prems => |
484 [ |
484 [ |
485 (cut_facts_tac prems 1), |
485 (cut_facts_tac prems 1), |
486 (rtac monocontlub2cont 1), |
486 (rtac monocontlub2cont 1), |
487 (rtac (cont2mono RS allI RS mono2mono_MF1L_rev ) 1), |
487 (rtac (cont2mono RS allI RS mono2mono_MF1L_rev ) 1), |
488 (etac spec 1), |
488 (etac spec 1), |
489 (rtac contlubI 1), |
489 (rtac contlubI 1), |
490 (strip_tac 1), |
490 (strip_tac 1), |
491 (rtac ext 1), |
491 (rtac ext 1), |
492 (rtac (thelub_fun RS ssubst) 1), |
492 (rtac (thelub_fun RS ssubst) 1), |
493 (rtac (cont2mono RS allI RS mono2mono_MF1L_rev RS ch2ch_monofun) 1), |
493 (rtac (cont2mono RS allI RS mono2mono_MF1L_rev RS ch2ch_monofun) 1), |
494 (etac spec 1), |
494 (etac spec 1), |
495 (atac 1), |
495 (atac 1), |
496 (rtac |
496 (rtac |
497 ((hd prems) RS spec RS cont2contlub RS contlubE RS spec RS mp) 1), |
497 ((hd prems) RS spec RS cont2contlub RS contlubE RS spec RS mp) 1), |
498 (atac 1) |
498 (atac 1) |
499 ]); |
499 ]); |
500 |
500 |
501 |
501 |
502 (* ------------------------------------------------------------------------ *) |
502 (* ------------------------------------------------------------------------ *) |
503 (* What D.A.Schmidt calls continuity of abstraction *) |
503 (* What D.A.Schmidt calls continuity of abstraction *) |
504 (* never used here *) |
504 (* never used here *) |
506 |
506 |
507 qed_goal "contlub_abstraction" Cont.thy |
507 qed_goal "contlub_abstraction" Cont.thy |
508 "[|is_chain(Y::nat=>'a);!y.cont(%x.(c::'a=>'b=>'c) x y)|] ==>\ |
508 "[|is_chain(Y::nat=>'a);!y.cont(%x.(c::'a=>'b=>'c) x y)|] ==>\ |
509 \ (%y.lub(range(%i.c (Y i) y))) = (lub(range(%i.%y.c (Y i) y)))" |
509 \ (%y.lub(range(%i.c (Y i) y))) = (lub(range(%i.%y.c (Y i) y)))" |
510 (fn prems => |
510 (fn prems => |
511 [ |
511 [ |
512 (cut_facts_tac prems 1), |
512 (cut_facts_tac prems 1), |
513 (rtac trans 1), |
513 (rtac trans 1), |
514 (rtac (cont2contlub RS contlubE RS spec RS mp) 2), |
514 (rtac (cont2contlub RS contlubE RS spec RS mp) 2), |
515 (atac 3), |
515 (atac 3), |
516 (etac cont2cont_CF1L_rev 2), |
516 (etac cont2cont_CF1L_rev 2), |
517 (rtac ext 1), |
517 (rtac ext 1), |
518 (rtac (cont2contlub RS contlubE RS spec RS mp RS sym) 1), |
518 (rtac (cont2contlub RS contlubE RS spec RS mp RS sym) 1), |
519 (etac spec 1), |
519 (etac spec 1), |
520 (atac 1) |
520 (atac 1) |
521 ]); |
521 ]); |
522 |
522 |
523 |
523 |
524 qed_goal "mono2mono_app" Cont.thy |
524 qed_goal "mono2mono_app" Cont.thy |
525 "[|monofun(ft);!x.monofun(ft(x));monofun(tt)|] ==>\ |
525 "[|monofun(ft);!x.monofun(ft(x));monofun(tt)|] ==>\ |
526 \ monofun(%x.(ft(x))(tt(x)))" |
526 \ monofun(%x.(ft(x))(tt(x)))" |
527 (fn prems => |
527 (fn prems => |
528 [ |
528 [ |
529 (cut_facts_tac prems 1), |
529 (cut_facts_tac prems 1), |
530 (rtac monofunI 1), |
530 (rtac monofunI 1), |
531 (strip_tac 1), |
531 (strip_tac 1), |
532 (res_inst_tac [("f1.0","ft(x)"),("f2.0","ft(y)")] monofun_fun 1), |
532 (res_inst_tac [("f1.0","ft(x)"),("f2.0","ft(y)")] monofun_fun 1), |
533 (etac spec 1), |
533 (etac spec 1), |
534 (etac spec 1), |
534 (etac spec 1), |
535 (etac (monofunE RS spec RS spec RS mp) 1), |
535 (etac (monofunE RS spec RS spec RS mp) 1), |
536 (atac 1), |
536 (atac 1), |
537 (etac (monofunE RS spec RS spec RS mp) 1), |
537 (etac (monofunE RS spec RS spec RS mp) 1), |
538 (atac 1) |
538 (atac 1) |
539 ]); |
539 ]); |
540 |
540 |
541 |
541 |
542 qed_goal "cont2contlub_app" Cont.thy |
542 qed_goal "cont2contlub_app" Cont.thy |
543 "[|cont(ft);!x.cont(ft(x));cont(tt)|] ==> contlub(%x.(ft(x))(tt(x)))" |
543 "[|cont(ft);!x.cont(ft(x));cont(tt)|] ==> contlub(%x.(ft(x))(tt(x)))" |
544 (fn prems => |
544 (fn prems => |
545 [ |
545 [ |
546 (cut_facts_tac prems 1), |
546 (cut_facts_tac prems 1), |
547 (rtac contlubI 1), |
547 (rtac contlubI 1), |
548 (strip_tac 1), |
548 (strip_tac 1), |
549 (res_inst_tac [("f3","tt")] (contlubE RS spec RS mp RS ssubst) 1), |
549 (res_inst_tac [("f3","tt")] (contlubE RS spec RS mp RS ssubst) 1), |
550 (etac cont2contlub 1), |
550 (etac cont2contlub 1), |
551 (atac 1), |
551 (atac 1), |
552 (rtac contlub_CF2 1), |
552 (rtac contlub_CF2 1), |
553 (REPEAT (atac 1)), |
553 (REPEAT (atac 1)), |
554 (etac (cont2mono RS ch2ch_monofun) 1), |
554 (etac (cont2mono RS ch2ch_monofun) 1), |
555 (atac 1) |
555 (atac 1) |
556 ]); |
556 ]); |
557 |
557 |
558 |
558 |
559 qed_goal "cont2cont_app" Cont.thy |
559 qed_goal "cont2cont_app" Cont.thy |
560 "[|cont(ft);!x.cont(ft(x));cont(tt)|] ==>\ |
560 "[|cont(ft);!x.cont(ft(x));cont(tt)|] ==>\ |
561 \ cont(%x.(ft(x))(tt(x)))" |
561 \ cont(%x.(ft(x))(tt(x)))" |
562 (fn prems => |
562 (fn prems => |
563 [ |
563 [ |
564 (rtac monocontlub2cont 1), |
564 (rtac monocontlub2cont 1), |
565 (rtac mono2mono_app 1), |
565 (rtac mono2mono_app 1), |
566 (rtac cont2mono 1), |
566 (rtac cont2mono 1), |
567 (resolve_tac prems 1), |
567 (resolve_tac prems 1), |
568 (strip_tac 1), |
568 (strip_tac 1), |
569 (rtac cont2mono 1), |
569 (rtac cont2mono 1), |
570 (cut_facts_tac prems 1), |
570 (cut_facts_tac prems 1), |
571 (etac spec 1), |
571 (etac spec 1), |
572 (rtac cont2mono 1), |
572 (rtac cont2mono 1), |
573 (resolve_tac prems 1), |
573 (resolve_tac prems 1), |
574 (rtac cont2contlub_app 1), |
574 (rtac cont2contlub_app 1), |
575 (resolve_tac prems 1), |
575 (resolve_tac prems 1), |
576 (resolve_tac prems 1), |
576 (resolve_tac prems 1), |
577 (resolve_tac prems 1) |
577 (resolve_tac prems 1) |
578 ]); |
578 ]); |
579 |
579 |
580 |
580 |
581 val cont2cont_app2 = (allI RSN (2,cont2cont_app)); |
581 val cont2cont_app2 = (allI RSN (2,cont2cont_app)); |
582 (* [| cont ?ft; !!x. cont (?ft x); cont ?tt |] ==> *) |
582 (* [| cont ?ft; !!x. cont (?ft x); cont ?tt |] ==> *) |
583 (* cont (%x. ?ft x (?tt x)) *) |
583 (* cont (%x. ?ft x (?tt x)) *) |