78 apply (rule is_lub_thelub) |
83 apply (rule is_lub_thelub) |
79 apply (erule ch2ch_fun) |
84 apply (erule ch2ch_fun) |
80 apply (erule ub2ub_fun) |
85 apply (erule ub2ub_fun) |
81 done |
86 done |
82 |
87 |
|
88 lemma lub_fun': |
|
89 fixes S :: "('a::type \<Rightarrow> 'b::dcpo) set" |
|
90 assumes S: "directed S" |
|
91 shows "S <<| (\<lambda>x. \<Squnion>f\<in>S. f x)" |
|
92 apply (rule is_lubI) |
|
93 apply (rule is_ubI) |
|
94 apply (rule less_fun_ext) |
|
95 apply (rule is_ub_thelub') |
|
96 apply (rule dir2dir_monofun [OF monofun_app S]) |
|
97 apply (erule imageI) |
|
98 apply (rule less_fun_ext) |
|
99 apply (rule is_lub_thelub') |
|
100 apply (rule dir2dir_monofun [OF monofun_app S]) |
|
101 apply (erule ub2ub_monofun' [OF monofun_app]) |
|
102 done |
|
103 |
83 lemma thelub_fun: |
104 lemma thelub_fun: |
84 "chain (S::nat \<Rightarrow> 'a::type \<Rightarrow> 'b::cpo) |
105 "chain (S::nat \<Rightarrow> 'a::type \<Rightarrow> 'b::cpo) |
85 \<Longrightarrow> lub (range S) = (\<lambda>x. \<Squnion>i. S i x)" |
106 \<Longrightarrow> lub (range S) = (\<lambda>x. \<Squnion>i. S i x)" |
86 by (rule lub_fun [THEN thelubI]) |
107 by (rule lub_fun [THEN thelubI]) |
87 |
108 |
|
109 lemma thelub_fun': |
|
110 "directed (S::('a::type \<Rightarrow> 'b::dcpo) set) |
|
111 \<Longrightarrow> lub S = (\<lambda>x. \<Squnion>f\<in>S. f x)" |
|
112 by (rule lub_fun' [THEN thelubI]) |
|
113 |
88 lemma cpo_fun: |
114 lemma cpo_fun: |
89 "chain (S::nat \<Rightarrow> 'a::type \<Rightarrow> 'b::cpo) \<Longrightarrow> \<exists>x. range S <<| x" |
115 "chain (S::nat \<Rightarrow> 'a::type \<Rightarrow> 'b::cpo) \<Longrightarrow> \<exists>x. range S <<| x" |
90 by (rule exI, erule lub_fun) |
116 by (rule exI, erule lub_fun) |
91 |
117 |
92 instance "fun" :: (type, cpo) cpo |
118 instance "fun" :: (type, cpo) cpo |
93 by intro_classes (rule cpo_fun) |
119 by intro_classes (rule cpo_fun) |
94 |
120 |
|
121 lemma dcpo_fun: |
|
122 "directed (S::('a::type \<Rightarrow> 'b::dcpo) set) \<Longrightarrow> \<exists>x. S <<| x" |
|
123 by (rule exI, erule lub_fun') |
|
124 |
|
125 instance "fun" :: (type, dcpo) dcpo |
|
126 by intro_classes (rule dcpo_fun) |
|
127 |
95 subsection {* Full function space is pointed *} |
128 subsection {* Full function space is pointed *} |
96 |
129 |
97 lemma minimal_fun: "(\<lambda>x. \<bottom>) \<sqsubseteq> f" |
130 lemma minimal_fun: "(\<lambda>x. \<bottom>) \<sqsubseteq> f" |
98 by (simp add: less_fun_def) |
131 by (simp add: less_fun_def) |
99 |
132 |
100 lemma least_fun: "\<exists>x::'a \<Rightarrow> 'b::pcpo. \<forall>y. x \<sqsubseteq> y" |
133 lemma least_fun: "\<exists>x::'a::type \<Rightarrow> 'b::pcpo. \<forall>y. x \<sqsubseteq> y" |
101 apply (rule_tac x = "\<lambda>x. \<bottom>" in exI) |
134 apply (rule_tac x = "\<lambda>x. \<bottom>" in exI) |
102 apply (rule minimal_fun [THEN allI]) |
135 apply (rule minimal_fun [THEN allI]) |
103 done |
136 done |
104 |
137 |
105 instance "fun" :: (type, pcpo) pcpo |
138 instance "fun" :: (type, pcpo) pcpo |
111 |
144 |
112 text {* function application is strict in the left argument *} |
145 text {* function application is strict in the left argument *} |
113 lemma app_strict [simp]: "\<bottom> x = \<bottom>" |
146 lemma app_strict [simp]: "\<bottom> x = \<bottom>" |
114 by (simp add: inst_fun_pcpo) |
147 by (simp add: inst_fun_pcpo) |
115 |
148 |
|
149 text {* |
|
150 The following results are about application for functions in @{typ "'a=>'b"} |
|
151 *} |
|
152 |
|
153 lemma monofun_fun_fun: "f \<sqsubseteq> g \<Longrightarrow> f x \<sqsubseteq> g x" |
|
154 by (simp add: less_fun_def) |
|
155 |
|
156 lemma monofun_fun_arg: "\<lbrakk>monofun f; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> f x \<sqsubseteq> f y" |
|
157 by (rule monofunE) |
|
158 |
|
159 lemma monofun_fun: "\<lbrakk>monofun f; monofun g; f \<sqsubseteq> g; x \<sqsubseteq> y\<rbrakk> \<Longrightarrow> f x \<sqsubseteq> g y" |
|
160 by (rule trans_less [OF monofun_fun_arg monofun_fun_fun]) |
|
161 |
|
162 subsection {* Propagation of monotonicity and continuity *} |
|
163 |
|
164 text {* the lub of a chain of monotone functions is monotone *} |
|
165 |
|
166 lemma monofun_lub_fun: |
|
167 "\<lbrakk>chain (F::nat \<Rightarrow> 'a \<Rightarrow> 'b::cpo); \<forall>i. monofun (F i)\<rbrakk> |
|
168 \<Longrightarrow> monofun (\<Squnion>i. F i)" |
|
169 apply (rule monofunI) |
|
170 apply (simp add: thelub_fun) |
|
171 apply (rule lub_mono [rule_format]) |
|
172 apply (erule ch2ch_fun) |
|
173 apply (erule ch2ch_fun) |
|
174 apply (simp add: monofunE) |
|
175 done |
|
176 |
|
177 text {* the lub of a chain of continuous functions is continuous *} |
|
178 |
|
179 declare range_composition [simp del] |
|
180 |
|
181 lemma contlub_lub_fun: |
|
182 "\<lbrakk>chain F; \<forall>i. cont (F i)\<rbrakk> \<Longrightarrow> contlub (\<Squnion>i. F i)" |
|
183 apply (rule contlubI) |
|
184 apply (simp add: thelub_fun) |
|
185 apply (simp add: cont2contlubE) |
|
186 apply (rule ex_lub) |
|
187 apply (erule ch2ch_fun) |
|
188 apply (simp add: ch2ch_cont) |
|
189 done |
|
190 |
|
191 lemma cont_lub_fun: |
|
192 "\<lbrakk>chain F; \<forall>i. cont (F i)\<rbrakk> \<Longrightarrow> cont (\<Squnion>i. F i)" |
|
193 apply (rule monocontlub2cont) |
|
194 apply (erule monofun_lub_fun) |
|
195 apply (simp add: cont2mono) |
|
196 apply (erule (1) contlub_lub_fun) |
|
197 done |
|
198 |
|
199 lemma cont2cont_lub: |
|
200 "\<lbrakk>chain F; \<And>i. cont (F i)\<rbrakk> \<Longrightarrow> cont (\<lambda>x. \<Squnion>i. F i x)" |
|
201 by (simp add: thelub_fun [symmetric] cont_lub_fun) |
|
202 |
|
203 lemma mono2mono_fun: "monofun f \<Longrightarrow> monofun (\<lambda>x. f x y)" |
|
204 apply (rule monofunI) |
|
205 apply (erule (1) monofun_fun_arg [THEN monofun_fun_fun]) |
|
206 done |
|
207 |
|
208 lemma cont2cont_fun: "cont f \<Longrightarrow> cont (\<lambda>x. f x y)" |
|
209 apply (rule monocontlub2cont) |
|
210 apply (erule cont2mono [THEN mono2mono_fun]) |
|
211 apply (rule contlubI) |
|
212 apply (simp add: cont2contlubE) |
|
213 apply (simp add: thelub_fun ch2ch_cont) |
|
214 done |
|
215 |
|
216 text {* Note @{text "(\<lambda>x. \<lambda>y. f x y) = f"} *} |
|
217 |
|
218 lemma mono2mono_lambda: "(\<And>y. monofun (\<lambda>x. f x y)) \<Longrightarrow> monofun f" |
|
219 apply (rule monofunI) |
|
220 apply (rule less_fun_ext) |
|
221 apply (blast dest: monofunE) |
|
222 done |
|
223 |
|
224 lemma cont2cont_lambda: "(\<And>y. cont (\<lambda>x. f x y)) \<Longrightarrow> cont f" |
|
225 apply (subgoal_tac "monofun f") |
|
226 apply (rule monocontlub2cont) |
|
227 apply assumption |
|
228 apply (rule contlubI) |
|
229 apply (rule ext) |
|
230 apply (simp add: thelub_fun ch2ch_monofun) |
|
231 apply (blast dest: cont2contlubE) |
|
232 apply (simp add: mono2mono_lambda cont2mono) |
|
233 done |
|
234 |
|
235 text {* What D.A.Schmidt calls continuity of abstraction; never used here *} |
|
236 |
|
237 lemma contlub_lambda: |
|
238 "(\<And>x::'a::type. chain (\<lambda>i. S i x::'b::cpo)) |
|
239 \<Longrightarrow> (\<lambda>x. \<Squnion>i. S i x) = (\<Squnion>i. (\<lambda>x. S i x))" |
|
240 by (simp add: thelub_fun ch2ch_lambda) |
|
241 |
|
242 lemma contlub_abstraction: |
|
243 "\<lbrakk>chain Y; \<forall>y. cont (\<lambda>x.(c::'a::cpo\<Rightarrow>'b::type\<Rightarrow>'c::cpo) x y)\<rbrakk> \<Longrightarrow> |
|
244 (\<lambda>y. \<Squnion>i. c (Y i) y) = (\<Squnion>i. (\<lambda>y. c (Y i) y))" |
|
245 apply (rule thelub_fun [symmetric]) |
|
246 apply (rule ch2ch_cont) |
|
247 apply (simp add: cont2cont_lambda) |
|
248 apply assumption |
|
249 done |
|
250 |
|
251 lemma mono2mono_app: |
|
252 "\<lbrakk>monofun f; \<forall>x. monofun (f x); monofun t\<rbrakk> \<Longrightarrow> monofun (\<lambda>x. (f x) (t x))" |
|
253 apply (rule monofunI) |
|
254 apply (simp add: monofun_fun monofunE) |
|
255 done |
|
256 |
|
257 lemma cont2contlub_app: |
|
258 "\<lbrakk>cont f; \<forall>x. cont (f x); cont t\<rbrakk> \<Longrightarrow> contlub (\<lambda>x. (f x) (t x))" |
|
259 apply (rule contlubI) |
|
260 apply (subgoal_tac "chain (\<lambda>i. f (Y i))") |
|
261 apply (subgoal_tac "chain (\<lambda>i. t (Y i))") |
|
262 apply (simp add: cont2contlubE thelub_fun) |
|
263 apply (rule diag_lub) |
|
264 apply (erule ch2ch_fun) |
|
265 apply (drule spec) |
|
266 apply (erule (1) ch2ch_cont) |
|
267 apply (erule (1) ch2ch_cont) |
|
268 apply (erule (1) ch2ch_cont) |
|
269 done |
|
270 |
|
271 lemma cont2cont_app: |
|
272 "\<lbrakk>cont f; \<forall>x. cont (f x); cont t\<rbrakk> \<Longrightarrow> cont (\<lambda>x. (f x) (t x))" |
|
273 by (blast intro: monocontlub2cont mono2mono_app cont2mono cont2contlub_app) |
|
274 |
|
275 lemmas cont2cont_app2 = cont2cont_app [rule_format] |
|
276 |
|
277 lemma cont2cont_app3: "\<lbrakk>cont f; cont t\<rbrakk> \<Longrightarrow> cont (\<lambda>x. f (t x))" |
|
278 by (rule cont2cont_app2 [OF cont_const]) |
|
279 |
116 end |
280 end |
117 |
281 |