src/HOL/HOLCF/Cfun.thy
changeset 41031 9883d1417ce1
parent 41030 ff7d177128ef
child 41322 43a5b9a0ee8a
     1.1 --- a/src/HOL/HOLCF/Cfun.thy	Mon Dec 06 10:08:33 2010 -0800
     1.2 +++ b/src/HOL/HOLCF/Cfun.thy	Mon Dec 06 11:22:42 2010 -0800
     1.3 @@ -248,13 +248,6 @@
     1.4    "\<lbrakk>chain F; chain Y\<rbrakk> \<Longrightarrow> (\<Squnion>i. F i\<cdot>(Y i)) = (\<Squnion>i. F i)\<cdot>(\<Squnion>i. Y i)"
     1.5  by (simp add: contlub_cfun_fun contlub_cfun_arg diag_lub)
     1.6  
     1.7 -lemma cont_cfun:
     1.8 -  "\<lbrakk>chain F; chain Y\<rbrakk> \<Longrightarrow> range (\<lambda>i. F i\<cdot>(Y i)) <<| (\<Squnion>i. F i)\<cdot>(\<Squnion>i. Y i)"
     1.9 -apply (rule thelubE)
    1.10 -apply (simp only: ch2ch_Rep_cfun)
    1.11 -apply (simp only: lub_APP)
    1.12 -done
    1.13 -
    1.14  lemma lub_LAM:
    1.15    "\<lbrakk>\<And>x. chain (\<lambda>i. F i x); \<And>i. cont (\<lambda>x. F i x)\<rbrakk>
    1.16      \<Longrightarrow> (\<Squnion>i. \<Lambda> x. F i x) = (\<Lambda> x. \<Squnion>i. F i x)"
    1.17 @@ -275,11 +268,8 @@
    1.18  
    1.19  text {* type @{typ "'a -> 'b"} is chain complete *}
    1.20  
    1.21 -lemma lub_cfun: "chain F \<Longrightarrow> range F <<| (\<Lambda> x. \<Squnion>i. F i\<cdot>x)"
    1.22 -by (simp only: contlub_cfun_fun [symmetric] eta_cfun cpo_lubI)
    1.23 -
    1.24 -lemma thelub_cfun: "chain F \<Longrightarrow> (\<Squnion>i. F i) = (\<Lambda> x. \<Squnion>i. F i\<cdot>x)"
    1.25 -by (rule lub_cfun [THEN lub_eqI])
    1.26 +lemma lub_cfun: "chain F \<Longrightarrow> (\<Squnion>i. F i) = (\<Lambda> x. \<Squnion>i. F i\<cdot>x)"
    1.27 +by (simp add: lub_cfun lub_fun ch2ch_lambda)
    1.28  
    1.29  subsection {* Continuity simplification procedure *}
    1.30