95 apply (rule thelubI [symmetric]) |
95 apply (rule thelubI [symmetric]) |
96 apply (erule (1) contE) |
96 apply (erule (1) contE) |
97 done |
97 done |
98 |
98 |
99 lemma contI2: |
99 lemma contI2: |
|
100 fixes f :: "'a::cpo \<Rightarrow> 'b::cpo" |
100 assumes mono: "monofun f" |
101 assumes mono: "monofun f" |
101 assumes below: "\<And>Y. \<lbrakk>chain Y; chain (\<lambda>i. f (Y i))\<rbrakk> |
102 assumes below: "\<And>Y. \<lbrakk>chain Y; chain (\<lambda>i. f (Y i))\<rbrakk> |
102 \<Longrightarrow> f (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. f (Y i))" |
103 \<Longrightarrow> f (\<Squnion>i. Y i) \<sqsubseteq> (\<Squnion>i. f (Y i))" |
103 shows "cont f" |
104 shows "cont f" |
104 apply (rule contI) |
105 proof (rule contI) |
105 apply (rule thelubE) |
106 fix Y :: "nat \<Rightarrow> 'a" |
106 apply (erule ch2ch_monofun [OF mono]) |
107 assume Y: "chain Y" |
107 apply (rule below_antisym) |
108 with mono have fY: "chain (\<lambda>i. f (Y i))" |
108 apply (rule is_lub_thelub) |
109 by (rule ch2ch_monofun) |
109 apply (erule ch2ch_monofun [OF mono]) |
110 have "(\<Squnion>i. f (Y i)) = f (\<Squnion>i. Y i)" |
110 apply (rule ub2ub_monofun [OF mono]) |
111 apply (rule below_antisym) |
111 apply (rule is_lubD1) |
112 apply (rule lub_below [OF fY]) |
112 apply (erule cpo_lubI) |
113 apply (rule monofunE [OF mono]) |
113 apply (rule below, assumption) |
114 apply (rule is_ub_thelub [OF Y]) |
114 apply (erule ch2ch_monofun [OF mono]) |
115 apply (rule below [OF Y fY]) |
115 done |
116 done |
|
117 with fY show "range (\<lambda>i. f (Y i)) <<| f (\<Squnion>i. Y i)" |
|
118 by (rule thelubE) |
|
119 qed |
116 |
120 |
117 subsection {* Collection of continuity rules *} |
121 subsection {* Collection of continuity rules *} |
118 |
122 |
119 ML {* |
123 ML {* |
120 structure Cont2ContData = Named_Thms |
124 structure Cont2ContData = Named_Thms |