494 done |
494 done |
495 |
495 |
496 lemmas flatdom_strict2cont = flatdom2monofun [THEN chfindom_monofun2cont, standard] |
496 lemmas flatdom_strict2cont = flatdom2monofun [THEN chfindom_monofun2cont, standard] |
497 (* f UU = UU ==> cont (f::'a=>'b::pcpo)" *) |
497 (* f UU = UU ==> cont (f::'a=>'b::pcpo)" *) |
498 |
498 |
|
499 text {* the lub of a chain of monotone functions is monotone. *} |
|
500 |
|
501 lemma monofun_lub_fun: |
|
502 "\<lbrakk>chain (F::nat \<Rightarrow> 'a \<Rightarrow> 'b::cpo); \<forall>i. monofun (F i)\<rbrakk> |
|
503 \<Longrightarrow> monofun (\<Squnion>i. F i)" |
|
504 apply (rule monofunI [rule_format]) |
|
505 apply (simp add: thelub_fun) |
|
506 apply (rule lub_mono [rule_format]) |
|
507 apply (erule ch2ch_fun) |
|
508 apply (erule ch2ch_fun) |
|
509 apply (simp add: monofunE) |
|
510 done |
|
511 |
|
512 text {* the lub of a chain of continuous functions is continuous *} |
|
513 |
|
514 lemma cont_lub_fun: |
|
515 "\<lbrakk>chain F; \<forall>i. cont (F i)\<rbrakk> \<Longrightarrow> cont (\<Squnion>i. F i)" |
|
516 apply (rule contI [rule_format]) |
|
517 apply (rule is_lubI) |
|
518 apply (rule ub_rangeI) |
|
519 apply (erule monofun_lub_fun [THEN monofunE [rule_format]]) |
|
520 apply (simp add: cont2mono) |
|
521 apply (erule is_ub_thelub) |
|
522 apply (simp add: thelub_fun) |
|
523 apply (rule is_lub_thelub) |
|
524 apply (erule ch2ch_fun) |
|
525 apply (rule ub_rangeI) |
|
526 apply (drule_tac x=i in spec) |
|
527 apply (simp add: cont2contlub [THEN contlubE]) |
|
528 apply (rule is_lub_thelub) |
|
529 apply (simp add: cont2mono [THEN ch2ch_monofun]) |
|
530 apply (rule ub_rangeI) |
|
531 apply (rule trans_less) |
|
532 apply (erule ch2ch_fun [THEN is_ub_thelub]) |
|
533 apply (erule ub_rangeD) |
|
534 done |
|
535 |
499 end |
536 end |