src/HOL/HOLCF/Cfun.thy
changeset 41031 9883d1417ce1
parent 41030 ff7d177128ef
child 41322 43a5b9a0ee8a
equal deleted inserted replaced
41030:ff7d177128ef 41031:9883d1417ce1
   246 
   246 
   247 lemma lub_APP:
   247 lemma lub_APP:
   248   "\<lbrakk>chain F; chain Y\<rbrakk> \<Longrightarrow> (\<Squnion>i. F i\<cdot>(Y i)) = (\<Squnion>i. F i)\<cdot>(\<Squnion>i. 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:
       
   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)
       
   254 apply (simp only: ch2ch_Rep_cfun)
       
   255 apply (simp only: lub_APP)
       
   256 done
       
   257 
       
   258 lemma lub_LAM:
   251 lemma lub_LAM:
   259   "\<lbrakk>\<And>x. chain (\<lambda>i. F i x); \<And>i. cont (\<lambda>x. F i x)\<rbrakk>
   252   "\<lbrakk>\<And>x. chain (\<lambda>i. F i x); \<And>i. cont (\<lambda>x. F i x)\<rbrakk>
   260     \<Longrightarrow> (\<Squnion>i. \<Lambda> x. F i x) = (\<Lambda> x. \<Squnion>i. F i x)"
   253     \<Longrightarrow> (\<Squnion>i. \<Lambda> x. F i x) = (\<Lambda> x. \<Squnion>i. F i x)"
   261 apply (simp add: lub_cfun)
   254 apply (simp add: lub_cfun)
   262 apply (simp add: Abs_cfun_inverse2)
   255 apply (simp add: Abs_cfun_inverse2)
   273 apply (rule minimal [THEN monofun_cfun_arg])
   266 apply (rule minimal [THEN monofun_cfun_arg])
   274 done
   267 done
   275 
   268 
   276 text {* type @{typ "'a -> 'b"} is chain complete *}
   269 text {* type @{typ "'a -> 'b"} is chain complete *}
   277 
   270 
   278 lemma lub_cfun: "chain F \<Longrightarrow> range F <<| (\<Lambda> x. \<Squnion>i. F i\<cdot>x)"
   271 lemma lub_cfun: "chain F \<Longrightarrow> (\<Squnion>i. F i) = (\<Lambda> x. \<Squnion>i. F i\<cdot>x)"
   279 by (simp only: contlub_cfun_fun [symmetric] eta_cfun cpo_lubI)
   272 by (simp add: lub_cfun lub_fun ch2ch_lambda)
   280 
       
   281 lemma thelub_cfun: "chain F \<Longrightarrow> (\<Squnion>i. F i) = (\<Lambda> x. \<Squnion>i. F i\<cdot>x)"
       
   282 by (rule lub_cfun [THEN lub_eqI])
       
   283 
   273 
   284 subsection {* Continuity simplification procedure *}
   274 subsection {* Continuity simplification procedure *}
   285 
   275 
   286 text {* cont2cont lemma for @{term Rep_cfun} *}
   276 text {* cont2cont lemma for @{term Rep_cfun} *}
   287 
   277