remove lemma cont_cfun;
authorhuffman
Mon Dec 06 11:22:42 2010 -0800 (2010-12-06)
changeset 410319883d1417ce1
parent 41030 ff7d177128ef
child 41032 75b4ff66781c
remove lemma cont_cfun;
rename thelub_cfun to lub_cfun
NEWS
src/HOL/HOLCF/Cfun.thy
     1.1 --- a/NEWS	Mon Dec 06 10:08:33 2010 -0800
     1.2 +++ b/NEWS	Mon Dec 06 11:22:42 2010 -0800
     1.3 @@ -526,6 +526,7 @@
     1.4    lub_bin_chain   ~> is_lub_bin_chain
     1.5    lub_fun         ~> is_lub_fun
     1.6    thelub_fun      ~> lub_fun
     1.7 +  thelub_cfun     ~> lub_cfun
     1.8    thelub_Pair     ~> lub_Pair
     1.9    lub_cprod       ~> is_lub_prod
    1.10    thelub_cprod    ~> lub_prod
     2.1 --- a/src/HOL/HOLCF/Cfun.thy	Mon Dec 06 10:08:33 2010 -0800
     2.2 +++ b/src/HOL/HOLCF/Cfun.thy	Mon Dec 06 11:22:42 2010 -0800
     2.3 @@ -248,13 +248,6 @@
     2.4    "\<lbrakk>chain F; chain Y\<rbrakk> \<Longrightarrow> (\<Squnion>i. F i\<cdot>(Y i)) = (\<Squnion>i. F i)\<cdot>(\<Squnion>i. Y i)"
     2.5  by (simp add: contlub_cfun_fun contlub_cfun_arg diag_lub)
     2.6  
     2.7 -lemma cont_cfun:
     2.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)"
     2.9 -apply (rule thelubE)
    2.10 -apply (simp only: ch2ch_Rep_cfun)
    2.11 -apply (simp only: lub_APP)
    2.12 -done
    2.13 -
    2.14  lemma lub_LAM:
    2.15    "\<lbrakk>\<And>x. chain (\<lambda>i. F i x); \<And>i. cont (\<lambda>x. F i x)\<rbrakk>
    2.16      \<Longrightarrow> (\<Squnion>i. \<Lambda> x. F i x) = (\<Lambda> x. \<Squnion>i. F i x)"
    2.17 @@ -275,11 +268,8 @@
    2.18  
    2.19  text {* type @{typ "'a -> 'b"} is chain complete *}
    2.20  
    2.21 -lemma lub_cfun: "chain F \<Longrightarrow> range F <<| (\<Lambda> x. \<Squnion>i. F i\<cdot>x)"
    2.22 -by (simp only: contlub_cfun_fun [symmetric] eta_cfun cpo_lubI)
    2.23 -
    2.24 -lemma thelub_cfun: "chain F \<Longrightarrow> (\<Squnion>i. F i) = (\<Lambda> x. \<Squnion>i. F i\<cdot>x)"
    2.25 -by (rule lub_cfun [THEN lub_eqI])
    2.26 +lemma lub_cfun: "chain F \<Longrightarrow> (\<Squnion>i. F i) = (\<Lambda> x. \<Squnion>i. F i\<cdot>x)"
    2.27 +by (simp add: lub_cfun lub_fun ch2ch_lambda)
    2.28  
    2.29  subsection {* Continuity simplification procedure *}
    2.30