242 "\<lbrakk>\<And>x. chain (\<lambda>i. S i x); \<And>i. cont (\<lambda>x. S i x)\<rbrakk> \<Longrightarrow> chain (\<lambda>i. \<Lambda> x. S i x)" |
242 "\<lbrakk>\<And>x. chain (\<lambda>i. S i x); \<And>i. cont (\<lambda>x. S i x)\<rbrakk> \<Longrightarrow> chain (\<lambda>i. \<Lambda> x. S i x)" |
243 by (simp add: chain_def cfun_below_iff) |
243 by (simp add: chain_def cfun_below_iff) |
244 |
244 |
245 text {* contlub, cont properties of @{term Rep_cfun} in both arguments *} |
245 text {* contlub, cont properties of @{term Rep_cfun} in both arguments *} |
246 |
246 |
247 lemma contlub_cfun: |
247 lemma lub_APP: |
248 "\<lbrakk>chain F; chain Y\<rbrakk> \<Longrightarrow> (\<Squnion>i. F i)\<cdot>(\<Squnion>i. Y i) = (\<Squnion>i. F i\<cdot>(Y i))" |
248 "\<lbrakk>chain F; chain Y\<rbrakk> \<Longrightarrow> (\<Squnion>i. F i\<cdot>(Y i)) = (\<Squnion>i. F i)\<cdot>(\<Squnion>i. Y i)" |
249 by (simp add: contlub_cfun_fun contlub_cfun_arg diag_lub) |
249 by (simp add: contlub_cfun_fun contlub_cfun_arg diag_lub) |
250 |
250 |
251 lemma cont_cfun: |
251 lemma cont_cfun: |
252 "\<lbrakk>chain F; chain Y\<rbrakk> \<Longrightarrow> range (\<lambda>i. F i\<cdot>(Y i)) <<| (\<Squnion>i. F i)\<cdot>(\<Squnion>i. Y i)" |
252 "\<lbrakk>chain F; chain Y\<rbrakk> \<Longrightarrow> range (\<lambda>i. F i\<cdot>(Y i)) <<| (\<Squnion>i. F i)\<cdot>(\<Squnion>i. Y i)" |
253 apply (rule thelubE) |
253 apply (rule thelubE) |
254 apply (simp only: ch2ch_Rep_cfun) |
254 apply (simp only: ch2ch_Rep_cfun) |
255 apply (simp only: contlub_cfun) |
255 apply (simp only: lub_APP) |
256 done |
256 done |
257 |
257 |
258 lemma contlub_LAM: |
258 lemma lub_LAM: |
259 "\<lbrakk>\<And>x. chain (\<lambda>i. F i x); \<And>i. cont (\<lambda>x. F i x)\<rbrakk> |
259 "\<lbrakk>\<And>x. chain (\<lambda>i. F i x); \<And>i. cont (\<lambda>x. F i x)\<rbrakk> |
260 \<Longrightarrow> (\<Lambda> x. \<Squnion>i. F i x) = (\<Squnion>i. \<Lambda> x. F i x)" |
260 \<Longrightarrow> (\<Squnion>i. \<Lambda> x. F i x) = (\<Lambda> x. \<Squnion>i. F i x)" |
261 apply (simp add: lub_cfun) |
261 apply (simp add: lub_cfun) |
262 apply (simp add: Abs_cfun_inverse2) |
262 apply (simp add: Abs_cfun_inverse2) |
263 apply (simp add: thelub_fun ch2ch_lambda) |
263 apply (simp add: thelub_fun ch2ch_lambda) |
264 done |
264 done |
265 |
265 |
266 lemmas lub_distribs = |
266 lemmas lub_distribs = lub_APP lub_LAM |
267 contlub_cfun [symmetric] |
|
268 contlub_LAM [symmetric] |
|
269 |
267 |
270 text {* strictness *} |
268 text {* strictness *} |
271 |
269 |
272 lemma strictI: "f\<cdot>x = \<bottom> \<Longrightarrow> f\<cdot>\<bottom> = \<bottom>" |
270 lemma strictI: "f\<cdot>x = \<bottom> \<Longrightarrow> f\<cdot>\<bottom> = \<bottom>" |
273 apply (rule UU_I) |
271 apply (rule UU_I) |
276 done |
274 done |
277 |
275 |
278 text {* type @{typ "'a -> 'b"} is chain complete *} |
276 text {* type @{typ "'a -> 'b"} is chain complete *} |
279 |
277 |
280 lemma lub_cfun: "chain F \<Longrightarrow> range F <<| (\<Lambda> x. \<Squnion>i. F i\<cdot>x)" |
278 lemma lub_cfun: "chain F \<Longrightarrow> range F <<| (\<Lambda> x. \<Squnion>i. F i\<cdot>x)" |
281 by (simp only: contlub_cfun_fun [symmetric] eta_cfun thelubE) |
279 by (simp only: contlub_cfun_fun [symmetric] eta_cfun cpo_lubI) |
282 |
280 |
283 lemma thelub_cfun: "chain F \<Longrightarrow> (\<Squnion>i. F i) = (\<Lambda> x. \<Squnion>i. F i\<cdot>x)" |
281 lemma thelub_cfun: "chain F \<Longrightarrow> (\<Squnion>i. F i) = (\<Lambda> x. \<Squnion>i. F i\<cdot>x)" |
284 by (rule lub_cfun [THEN lub_eqI]) |
282 by (rule lub_cfun [THEN lub_eqI]) |
285 |
283 |
286 subsection {* Continuity simplification procedure *} |
284 subsection {* Continuity simplification procedure *} |