1 (* Title: HOLCF/cont.thy |
1 (* Title: HOLCF/cont.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Franz Regensburger |
3 Author: Franz Regensburger |
|
4 License: GPL (GNU GENERAL PUBLIC LICENSE) |
4 |
5 |
5 Results about continuity and monotonicity |
6 Results about continuity and monotonicity |
6 *) |
7 *) |
7 |
8 |
8 Cont = Fun3 + |
9 theory Cont = Fun3: |
9 |
10 |
10 (* |
11 (* |
11 |
12 |
12 Now we change the default class! Form now on all untyped typevariables are |
13 Now we change the default class! Form now on all untyped typevariables are |
13 of default class po |
14 of default class po |
14 |
15 |
15 *) |
16 *) |
16 |
17 |
17 |
18 |
18 default po |
19 defaultsort po |
19 |
20 |
20 consts |
21 consts |
21 monofun :: "('a => 'b) => bool" (* monotonicity *) |
22 monofun :: "('a => 'b) => bool" (* monotonicity *) |
22 contlub :: "('a::cpo => 'b::cpo) => bool" (* first cont. def *) |
23 contlub :: "('a::cpo => 'b::cpo) => bool" (* first cont. def *) |
23 cont :: "('a::cpo => 'b::cpo) => bool" (* secnd cont. def *) |
24 cont :: "('a::cpo => 'b::cpo) => bool" (* secnd cont. def *) |
24 |
25 |
25 defs |
26 defs |
26 |
27 |
27 monofun "monofun(f) == ! x y. x << y --> f(x) << f(y)" |
28 monofun: "monofun(f) == ! x y. x << y --> f(x) << f(y)" |
28 |
29 |
29 contlub "contlub(f) == ! Y. chain(Y) --> |
30 contlub: "contlub(f) == ! Y. chain(Y) --> |
30 f(lub(range(Y))) = lub(range(% i. f(Y(i))))" |
31 f(lub(range(Y))) = lub(range(% i. f(Y(i))))" |
31 |
32 |
32 cont "cont(f) == ! Y. chain(Y) --> |
33 cont: "cont(f) == ! Y. chain(Y) --> |
33 range(% i. f(Y(i))) <<| f(lub(range(Y)))" |
34 range(% i. f(Y(i))) <<| f(lub(range(Y)))" |
34 |
35 |
35 (* ------------------------------------------------------------------------ *) |
36 (* ------------------------------------------------------------------------ *) |
36 (* the main purpose of cont.thy is to show: *) |
37 (* the main purpose of cont.thy is to show: *) |
37 (* monofun(f) & contlub(f) <==> cont(f) *) |
38 (* monofun(f) & contlub(f) <==> cont(f) *) |
38 (* ------------------------------------------------------------------------ *) |
39 (* ------------------------------------------------------------------------ *) |
39 |
40 |
|
41 (* Title: HOLCF/Cont.ML |
|
42 ID: $Id$ |
|
43 Author: Franz Regensburger |
|
44 License: GPL (GNU GENERAL PUBLIC LICENSE) |
|
45 |
|
46 Results about continuity and monotonicity |
|
47 *) |
|
48 |
|
49 (* ------------------------------------------------------------------------ *) |
|
50 (* access to definition *) |
|
51 (* ------------------------------------------------------------------------ *) |
|
52 |
|
53 lemma contlubI: |
|
54 "! Y. chain(Y) --> f(lub(range(Y))) = lub(range(%i. f(Y(i))))==> |
|
55 contlub(f)" |
|
56 apply (unfold contlub) |
|
57 apply assumption |
|
58 done |
|
59 |
|
60 lemma contlubE: |
|
61 " contlub(f)==> |
|
62 ! Y. chain(Y) --> f(lub(range(Y))) = lub(range(%i. f(Y(i))))" |
|
63 apply (unfold contlub) |
|
64 apply assumption |
|
65 done |
|
66 |
|
67 |
|
68 lemma contI: |
|
69 "! Y. chain(Y) --> range(% i. f(Y(i))) <<| f(lub(range(Y))) ==> cont(f)" |
|
70 |
|
71 apply (unfold cont) |
|
72 apply assumption |
|
73 done |
|
74 |
|
75 lemma contE: |
|
76 "cont(f) ==> ! Y. chain(Y) --> range(% i. f(Y(i))) <<| f(lub(range(Y)))" |
|
77 apply (unfold cont) |
|
78 apply assumption |
|
79 done |
|
80 |
|
81 |
|
82 lemma monofunI: |
|
83 "! x y. x << y --> f(x) << f(y) ==> monofun(f)" |
|
84 apply (unfold monofun) |
|
85 apply assumption |
|
86 done |
|
87 |
|
88 lemma monofunE: |
|
89 "monofun(f) ==> ! x y. x << y --> f(x) << f(y)" |
|
90 apply (unfold monofun) |
|
91 apply assumption |
|
92 done |
|
93 |
|
94 (* ------------------------------------------------------------------------ *) |
|
95 (* the main purpose of cont.thy is to show: *) |
|
96 (* monofun(f) & contlub(f) <==> cont(f) *) |
|
97 (* ------------------------------------------------------------------------ *) |
|
98 |
|
99 (* ------------------------------------------------------------------------ *) |
|
100 (* monotone functions map chains to chains *) |
|
101 (* ------------------------------------------------------------------------ *) |
|
102 |
|
103 lemma ch2ch_monofun: |
|
104 "[| monofun(f); chain(Y) |] ==> chain(%i. f(Y(i)))" |
|
105 apply (rule chainI) |
|
106 apply (erule monofunE [THEN spec, THEN spec, THEN mp]) |
|
107 apply (erule chainE) |
|
108 done |
|
109 |
|
110 (* ------------------------------------------------------------------------ *) |
|
111 (* monotone functions map upper bound to upper bounds *) |
|
112 (* ------------------------------------------------------------------------ *) |
|
113 |
|
114 lemma ub2ub_monofun: |
|
115 "[| monofun(f); range(Y) <| u|] ==> range(%i. f(Y(i))) <| f(u)" |
|
116 apply (rule ub_rangeI) |
|
117 apply (erule monofunE [THEN spec, THEN spec, THEN mp]) |
|
118 apply (erule ub_rangeD) |
|
119 done |
|
120 |
|
121 (* ------------------------------------------------------------------------ *) |
|
122 (* left to right: monofun(f) & contlub(f) ==> cont(f) *) |
|
123 (* ------------------------------------------------------------------------ *) |
|
124 |
|
125 lemma monocontlub2cont: |
|
126 "[|monofun(f);contlub(f)|] ==> cont(f)" |
|
127 apply (unfold cont) |
|
128 apply (intro strip) |
|
129 apply (rule thelubE) |
|
130 apply (erule ch2ch_monofun) |
|
131 apply assumption |
|
132 apply (erule contlubE [THEN spec, THEN mp, symmetric]) |
|
133 apply assumption |
|
134 done |
|
135 |
|
136 (* ------------------------------------------------------------------------ *) |
|
137 (* first a lemma about binary chains *) |
|
138 (* ------------------------------------------------------------------------ *) |
|
139 |
|
140 lemma binchain_cont: "[| cont(f); x << y |] |
|
141 ==> range(%i::nat. f(if i = 0 then x else y)) <<| f(y)" |
|
142 apply (rule subst) |
|
143 prefer 2 apply (erule contE [THEN spec, THEN mp]) |
|
144 apply (erule bin_chain) |
|
145 apply (rule_tac y = "y" in arg_cong) |
|
146 apply (erule lub_bin_chain [THEN thelubI]) |
|
147 done |
|
148 |
|
149 (* ------------------------------------------------------------------------ *) |
|
150 (* right to left: cont(f) ==> monofun(f) & contlub(f) *) |
|
151 (* part1: cont(f) ==> monofun(f *) |
|
152 (* ------------------------------------------------------------------------ *) |
|
153 |
|
154 lemma cont2mono: "cont(f) ==> monofun(f)" |
|
155 apply (unfold monofun) |
|
156 apply (intro strip) |
|
157 apply (drule binchain_cont [THEN is_ub_lub]) |
|
158 apply (auto split add: split_if_asm) |
|
159 done |
|
160 |
|
161 (* ------------------------------------------------------------------------ *) |
|
162 (* right to left: cont(f) ==> monofun(f) & contlub(f) *) |
|
163 (* part2: cont(f) ==> contlub(f) *) |
|
164 (* ------------------------------------------------------------------------ *) |
|
165 |
|
166 lemma cont2contlub: "cont(f) ==> contlub(f)" |
|
167 apply (unfold contlub) |
|
168 apply (intro strip) |
|
169 apply (rule thelubI [symmetric]) |
|
170 apply (erule contE [THEN spec, THEN mp]) |
|
171 apply assumption |
|
172 done |
|
173 |
|
174 (* ------------------------------------------------------------------------ *) |
|
175 (* monotone functions map finite chains to finite chains *) |
|
176 (* ------------------------------------------------------------------------ *) |
|
177 |
|
178 lemma monofun_finch2finch: |
|
179 "[| monofun f; finite_chain Y |] ==> finite_chain (%n. f (Y n))" |
|
180 apply (unfold finite_chain_def) |
|
181 apply (force elim!: ch2ch_monofun simp add: max_in_chain_def) |
|
182 done |
|
183 |
|
184 (* ------------------------------------------------------------------------ *) |
|
185 (* The same holds for continuous functions *) |
|
186 (* ------------------------------------------------------------------------ *) |
|
187 |
|
188 lemmas cont_finch2finch = cont2mono [THEN monofun_finch2finch, standard] |
|
189 (* [| cont ?f; finite_chain ?Y |] ==> finite_chain (%n. ?f (?Y n)) *) |
|
190 |
|
191 |
|
192 (* ------------------------------------------------------------------------ *) |
|
193 (* The following results are about a curried function that is monotone *) |
|
194 (* in both arguments *) |
|
195 (* ------------------------------------------------------------------------ *) |
|
196 |
|
197 lemma ch2ch_MF2L: |
|
198 "[|monofun(MF2); chain(F)|] ==> chain(%i. MF2 (F i) x)" |
|
199 apply (erule ch2ch_monofun [THEN ch2ch_fun]) |
|
200 apply assumption |
|
201 done |
|
202 |
|
203 |
|
204 lemma ch2ch_MF2R: |
|
205 "[|monofun(MF2(f)); chain(Y)|] ==> chain(%i. MF2 f (Y i))" |
|
206 apply (erule ch2ch_monofun) |
|
207 apply assumption |
|
208 done |
|
209 |
|
210 lemma ch2ch_MF2LR: |
|
211 "[|monofun(MF2); !f. monofun(MF2(f)); chain(F); chain(Y)|] ==> |
|
212 chain(%i. MF2(F(i))(Y(i)))" |
|
213 apply (rule chainI) |
|
214 apply (rule trans_less) |
|
215 apply (erule ch2ch_MF2L [THEN chainE]) |
|
216 apply assumption |
|
217 apply (rule monofunE [THEN spec, THEN spec, THEN mp], erule spec) |
|
218 apply (erule chainE) |
|
219 done |
|
220 |
|
221 |
|
222 lemma ch2ch_lubMF2R: |
|
223 "[|monofun(MF2::('a::po=>'b::po=>'c::cpo)); |
|
224 !f. monofun(MF2(f)::('b::po=>'c::cpo)); |
|
225 chain(F);chain(Y)|] ==> |
|
226 chain(%j. lub(range(%i. MF2 (F j) (Y i))))" |
|
227 apply (rule lub_mono [THEN chainI]) |
|
228 apply (rule ch2ch_MF2R, erule spec) |
|
229 apply assumption |
|
230 apply (rule ch2ch_MF2R, erule spec) |
|
231 apply assumption |
|
232 apply (intro strip) |
|
233 apply (rule chainE) |
|
234 apply (erule ch2ch_MF2L) |
|
235 apply assumption |
|
236 done |
|
237 |
|
238 |
|
239 lemma ch2ch_lubMF2L: |
|
240 "[|monofun(MF2::('a::po=>'b::po=>'c::cpo)); |
|
241 !f. monofun(MF2(f)::('b::po=>'c::cpo)); |
|
242 chain(F);chain(Y)|] ==> |
|
243 chain(%i. lub(range(%j. MF2 (F j) (Y i))))" |
|
244 apply (rule lub_mono [THEN chainI]) |
|
245 apply (erule ch2ch_MF2L) |
|
246 apply assumption |
|
247 apply (erule ch2ch_MF2L) |
|
248 apply assumption |
|
249 apply (intro strip) |
|
250 apply (rule chainE) |
|
251 apply (rule ch2ch_MF2R, erule spec) |
|
252 apply assumption |
|
253 done |
|
254 |
|
255 |
|
256 lemma lub_MF2_mono: |
|
257 "[|monofun(MF2::('a::po=>'b::po=>'c::cpo)); |
|
258 !f. monofun(MF2(f)::('b::po=>'c::cpo)); |
|
259 chain(F)|] ==> |
|
260 monofun(% x. lub(range(% j. MF2 (F j) (x))))" |
|
261 apply (rule monofunI) |
|
262 apply (intro strip) |
|
263 apply (rule lub_mono) |
|
264 apply (erule ch2ch_MF2L) |
|
265 apply assumption |
|
266 apply (erule ch2ch_MF2L) |
|
267 apply assumption |
|
268 apply (intro strip) |
|
269 apply (rule monofunE [THEN spec, THEN spec, THEN mp], erule spec) |
|
270 apply assumption |
|
271 done |
|
272 |
|
273 lemma ex_lubMF2: |
|
274 "[|monofun(MF2::('a::po=>'b::po=>'c::cpo)); |
|
275 !f. monofun(MF2(f)::('b::po=>'c::cpo)); |
|
276 chain(F); chain(Y)|] ==> |
|
277 lub(range(%j. lub(range(%i. MF2(F j) (Y i))))) = |
|
278 lub(range(%i. lub(range(%j. MF2(F j) (Y i)))))" |
|
279 apply (rule antisym_less) |
|
280 apply (rule is_lub_thelub[OF _ ub_rangeI]) |
|
281 apply (erule ch2ch_lubMF2R) |
|
282 apply (assumption+) |
|
283 apply (rule lub_mono) |
|
284 apply (rule ch2ch_MF2R, erule spec) |
|
285 apply assumption |
|
286 apply (erule ch2ch_lubMF2L) |
|
287 apply (assumption+) |
|
288 apply (intro strip) |
|
289 apply (rule is_ub_thelub) |
|
290 apply (erule ch2ch_MF2L) |
|
291 apply assumption |
|
292 apply (rule is_lub_thelub[OF _ ub_rangeI]) |
|
293 apply (erule ch2ch_lubMF2L) |
|
294 apply (assumption+) |
|
295 apply (rule lub_mono) |
|
296 apply (erule ch2ch_MF2L) |
|
297 apply assumption |
|
298 apply (erule ch2ch_lubMF2R) |
|
299 apply (assumption+) |
|
300 apply (intro strip) |
|
301 apply (rule is_ub_thelub) |
|
302 apply (rule ch2ch_MF2R, erule spec) |
|
303 apply assumption |
|
304 done |
|
305 |
|
306 |
|
307 lemma diag_lubMF2_1: |
|
308 "[|monofun(MF2::('a::po=>'b::po=>'c::cpo)); |
|
309 !f. monofun(MF2(f)::('b::po=>'c::cpo)); |
|
310 chain(FY);chain(TY)|] ==> |
|
311 lub(range(%i. lub(range(%j. MF2(FY(j))(TY(i)))))) = |
|
312 lub(range(%i. MF2(FY(i))(TY(i))))" |
|
313 apply (rule antisym_less) |
|
314 apply (rule is_lub_thelub[OF _ ub_rangeI]) |
|
315 apply (erule ch2ch_lubMF2L) |
|
316 apply (assumption+) |
|
317 apply (rule lub_mono3) |
|
318 apply (erule ch2ch_MF2L) |
|
319 apply (assumption+) |
|
320 apply (erule ch2ch_MF2LR) |
|
321 apply (assumption+) |
|
322 apply (rule allI) |
|
323 apply (rule_tac m = "i" and n = "ia" in nat_less_cases) |
|
324 apply (rule_tac x = "ia" in exI) |
|
325 apply (rule chain_mono) |
|
326 apply (erule allE) |
|
327 apply (erule ch2ch_MF2R) |
|
328 apply (assumption+) |
|
329 apply (erule ssubst) |
|
330 apply (rule_tac x = "ia" in exI) |
|
331 apply (rule refl_less) |
|
332 apply (rule_tac x = "i" in exI) |
|
333 apply (rule chain_mono) |
|
334 apply (erule ch2ch_MF2L) |
|
335 apply (assumption+) |
|
336 apply (rule lub_mono) |
|
337 apply (erule ch2ch_MF2LR) |
|
338 apply (assumption+) |
|
339 apply (erule ch2ch_lubMF2L) |
|
340 apply (assumption+) |
|
341 apply (intro strip) |
|
342 apply (rule is_ub_thelub) |
|
343 apply (erule ch2ch_MF2L) |
|
344 apply assumption |
|
345 done |
|
346 |
|
347 lemma diag_lubMF2_2: |
|
348 "[|monofun(MF2::('a::po=>'b::po=>'c::cpo)); |
|
349 !f. monofun(MF2(f)::('b::po=>'c::cpo)); |
|
350 chain(FY);chain(TY)|] ==> |
|
351 lub(range(%j. lub(range(%i. MF2(FY(j))(TY(i)))))) = |
|
352 lub(range(%i. MF2(FY(i))(TY(i))))" |
|
353 apply (rule trans) |
|
354 apply (rule ex_lubMF2) |
|
355 apply (assumption+) |
|
356 apply (erule diag_lubMF2_1) |
|
357 apply (assumption+) |
|
358 done |
|
359 |
|
360 |
|
361 (* ------------------------------------------------------------------------ *) |
|
362 (* The following results are about a curried function that is continuous *) |
|
363 (* in both arguments *) |
|
364 (* ------------------------------------------------------------------------ *) |
|
365 |
|
366 lemma contlub_CF2: |
|
367 assumes prem1: "cont(CF2)" |
|
368 assumes prem2: "!f. cont(CF2(f))" |
|
369 assumes prem3: "chain(FY)" |
|
370 assumes prem4: "chain(TY)" |
|
371 shows "CF2(lub(range(FY)))(lub(range(TY))) = lub(range(%i. CF2(FY(i))(TY(i))))" |
|
372 apply (subst prem1 [THEN cont2contlub, THEN contlubE, THEN spec, THEN mp]) |
|
373 apply assumption |
|
374 apply (subst thelub_fun) |
|
375 apply (rule prem1 [THEN cont2mono [THEN ch2ch_monofun]]) |
|
376 apply assumption |
|
377 apply (rule trans) |
|
378 apply (rule prem2 [THEN spec, THEN cont2contlub, THEN contlubE, THEN spec, THEN mp, THEN ext, THEN arg_cong, THEN arg_cong]) |
|
379 apply (rule prem4) |
|
380 apply (rule diag_lubMF2_2) |
|
381 apply (auto simp add: cont2mono prems) |
|
382 done |
|
383 |
|
384 (* ------------------------------------------------------------------------ *) |
|
385 (* The following results are about application for functions in 'a=>'b *) |
|
386 (* ------------------------------------------------------------------------ *) |
|
387 |
|
388 lemma monofun_fun_fun: "f1 << f2 ==> f1(x) << f2(x)" |
|
389 apply (erule less_fun [THEN iffD1, THEN spec]) |
|
390 done |
|
391 |
|
392 lemma monofun_fun_arg: "[|monofun(f); x1 << x2|] ==> f(x1) << f(x2)" |
|
393 apply (erule monofunE [THEN spec, THEN spec, THEN mp]) |
|
394 apply assumption |
|
395 done |
|
396 |
|
397 lemma monofun_fun: "[|monofun(f1); monofun(f2); f1 << f2; x1 << x2|] ==> f1(x1) << f2(x2)" |
|
398 apply (rule trans_less) |
|
399 apply (erule monofun_fun_arg) |
|
400 apply assumption |
|
401 apply (erule monofun_fun_fun) |
|
402 done |
|
403 |
|
404 |
|
405 (* ------------------------------------------------------------------------ *) |
|
406 (* The following results are about the propagation of monotonicity and *) |
|
407 (* continuity *) |
|
408 (* ------------------------------------------------------------------------ *) |
|
409 |
|
410 lemma mono2mono_MF1L: "[|monofun(c1)|] ==> monofun(%x. c1 x y)" |
|
411 apply (rule monofunI) |
|
412 apply (intro strip) |
|
413 apply (erule monofun_fun_arg [THEN monofun_fun_fun]) |
|
414 apply assumption |
|
415 done |
|
416 |
|
417 lemma cont2cont_CF1L: "[|cont(c1)|] ==> cont(%x. c1 x y)" |
|
418 apply (rule monocontlub2cont) |
|
419 apply (erule cont2mono [THEN mono2mono_MF1L]) |
|
420 apply (rule contlubI) |
|
421 apply (intro strip) |
|
422 apply (frule asm_rl) |
|
423 apply (erule cont2contlub [THEN contlubE, THEN spec, THEN mp, THEN ssubst]) |
|
424 apply assumption |
|
425 apply (subst thelub_fun) |
|
426 apply (rule ch2ch_monofun) |
|
427 apply (erule cont2mono) |
|
428 apply assumption |
|
429 apply (rule refl) |
|
430 done |
|
431 |
|
432 (********* Note "(%x.%y.c1 x y) = c1" ***********) |
|
433 |
|
434 lemma mono2mono_MF1L_rev: "!y. monofun(%x. c1 x y) ==> monofun(c1)" |
|
435 apply (rule monofunI) |
|
436 apply (intro strip) |
|
437 apply (rule less_fun [THEN iffD2]) |
|
438 apply (blast dest: monofunE) |
|
439 done |
|
440 |
|
441 lemma cont2cont_CF1L_rev: "!y. cont(%x. c1 x y) ==> cont(c1)" |
|
442 apply (rule monocontlub2cont) |
|
443 apply (rule cont2mono [THEN allI, THEN mono2mono_MF1L_rev]) |
|
444 apply (erule spec) |
|
445 apply (rule contlubI) |
|
446 apply (intro strip) |
|
447 apply (rule ext) |
|
448 apply (subst thelub_fun) |
|
449 apply (rule cont2mono [THEN allI, THEN mono2mono_MF1L_rev, THEN ch2ch_monofun]) |
|
450 apply (erule spec) |
|
451 apply assumption |
|
452 apply (blast dest: cont2contlub [THEN contlubE]) |
|
453 done |
|
454 |
|
455 (* ------------------------------------------------------------------------ *) |
|
456 (* What D.A.Schmidt calls continuity of abstraction *) |
|
457 (* never used here *) |
|
458 (* ------------------------------------------------------------------------ *) |
|
459 |
|
460 lemma contlub_abstraction: |
|
461 "[|chain(Y::nat=>'a);!y. cont(%x.(c::'a::cpo=>'b::cpo=>'c::cpo) x y)|] ==> |
|
462 (%y. lub(range(%i. c (Y i) y))) = (lub(range(%i.%y. c (Y i) y)))" |
|
463 apply (rule trans) |
|
464 prefer 2 apply (rule cont2contlub [THEN contlubE, THEN spec, THEN mp]) |
|
465 prefer 2 apply (assumption) |
|
466 apply (erule cont2cont_CF1L_rev) |
|
467 apply (rule ext) |
|
468 apply (rule cont2contlub [THEN contlubE, THEN spec, THEN mp, symmetric]) |
|
469 apply (erule spec) |
|
470 apply assumption |
|
471 done |
|
472 |
|
473 lemma mono2mono_app: "[|monofun(ft);!x. monofun(ft(x));monofun(tt)|] ==> |
|
474 monofun(%x.(ft(x))(tt(x)))" |
|
475 apply (rule monofunI) |
|
476 apply (intro strip) |
|
477 apply (rule_tac ?f1.0 = "ft(x)" and ?f2.0 = "ft(y)" in monofun_fun) |
|
478 apply (erule spec) |
|
479 apply (erule spec) |
|
480 apply (erule monofunE [THEN spec, THEN spec, THEN mp]) |
|
481 apply assumption |
|
482 apply (erule monofunE [THEN spec, THEN spec, THEN mp]) |
|
483 apply assumption |
|
484 done |
|
485 |
|
486 |
|
487 lemma cont2contlub_app: "[|cont(ft);!x. cont(ft(x));cont(tt)|] ==> contlub(%x.(ft(x))(tt(x)))" |
|
488 apply (rule contlubI) |
|
489 apply (intro strip) |
|
490 apply (rule_tac f3 = "tt" in contlubE [THEN spec, THEN mp, THEN ssubst]) |
|
491 apply (erule cont2contlub) |
|
492 apply assumption |
|
493 apply (rule contlub_CF2) |
|
494 apply (assumption+) |
|
495 apply (erule cont2mono [THEN ch2ch_monofun]) |
|
496 apply assumption |
|
497 done |
|
498 |
|
499 |
|
500 lemma cont2cont_app: "[|cont(ft); !x. cont(ft(x)); cont(tt)|] ==> cont(%x.(ft(x))(tt(x)))" |
|
501 apply (blast intro: monocontlub2cont mono2mono_app cont2mono cont2contlub_app) |
|
502 done |
|
503 |
|
504 |
|
505 lemmas cont2cont_app2 = cont2cont_app[OF _ allI] |
|
506 (* [| cont ?ft; !!x. cont (?ft x); cont ?tt |] ==> *) |
|
507 (* cont (%x. ?ft x (?tt x)) *) |
|
508 |
|
509 |
|
510 (* ------------------------------------------------------------------------ *) |
|
511 (* The identity function is continuous *) |
|
512 (* ------------------------------------------------------------------------ *) |
|
513 |
|
514 lemma cont_id: "cont(% x. x)" |
|
515 apply (rule contI) |
|
516 apply (intro strip) |
|
517 apply (erule thelubE) |
|
518 apply (rule refl) |
|
519 done |
|
520 |
|
521 (* ------------------------------------------------------------------------ *) |
|
522 (* constant functions are continuous *) |
|
523 (* ------------------------------------------------------------------------ *) |
|
524 |
|
525 lemma cont_const: "cont(%x. c)" |
|
526 apply (unfold cont) |
|
527 apply (intro strip) |
|
528 apply (blast intro: is_lubI ub_rangeI dest: ub_rangeD) |
|
529 done |
|
530 |
|
531 |
|
532 lemma cont2cont_app3: "[|cont(f); cont(t) |] ==> cont(%x. f(t(x)))" |
|
533 apply (best intro: cont2cont_app2 cont_const) |
|
534 done |
|
535 |
|
536 (* ------------------------------------------------------------------------ *) |
|
537 (* A non-emptyness result for Cfun *) |
|
538 (* ------------------------------------------------------------------------ *) |
|
539 |
|
540 lemma CfunI: "?x:Collect cont" |
|
541 apply (rule CollectI) |
|
542 apply (rule cont_const) |
|
543 done |
|
544 |
|
545 (* ------------------------------------------------------------------------ *) |
|
546 (* some properties of flat *) |
|
547 (* ------------------------------------------------------------------------ *) |
|
548 |
|
549 lemma flatdom2monofun: "f UU = UU ==> monofun (f::'a::flat=>'b::pcpo)" |
|
550 |
|
551 apply (unfold monofun) |
|
552 apply (intro strip) |
|
553 apply (drule ax_flat [THEN spec, THEN spec, THEN mp]) |
|
554 apply auto |
|
555 done |
|
556 |
|
557 declare range_composition [simp del] |
|
558 lemma chfindom_monofun2cont: "monofun f ==> cont(f::'a::chfin=>'b::pcpo)" |
|
559 apply (rule monocontlub2cont) |
|
560 apply assumption |
|
561 apply (rule contlubI) |
|
562 apply (intro strip) |
|
563 apply (frule chfin2finch) |
|
564 apply (rule antisym_less) |
|
565 apply (clarsimp simp add: finite_chain_def maxinch_is_thelub) |
|
566 apply (rule is_ub_thelub) |
|
567 apply (erule ch2ch_monofun) |
|
568 apply assumption |
|
569 apply (drule monofun_finch2finch[COMP swap_prems_rl]) |
|
570 apply assumption |
|
571 apply (simp add: finite_chain_def) |
|
572 apply (erule conjE) |
|
573 apply (erule exE) |
|
574 apply (simp add: maxinch_is_thelub) |
|
575 apply (erule monofunE [THEN spec, THEN spec, THEN mp]) |
|
576 apply (erule is_ub_thelub) |
|
577 done |
|
578 |
|
579 lemmas flatdom_strict2cont = flatdom2monofun [THEN chfindom_monofun2cont, standard] |
|
580 (* f UU = UU ==> cont (f::'a=>'b::pcpo)" *) |
|
581 |
40 end |
582 end |