src/HOL/HOLCF/Cfun.thy
changeset 41027 c599955d9806
parent 40834 a1249aeff5b6
child 41030 ff7d177128ef
     1.1 --- a/src/HOL/HOLCF/Cfun.thy	Mon Dec 06 13:46:45 2010 +0100
     1.2 +++ b/src/HOL/HOLCF/Cfun.thy	Mon Dec 06 08:30:00 2010 -0800
     1.3 @@ -244,28 +244,26 @@
     1.4  
     1.5  text {* contlub, cont properties of @{term Rep_cfun} in both arguments *}
     1.6  
     1.7 -lemma contlub_cfun: 
     1.8 -  "\<lbrakk>chain F; chain Y\<rbrakk> \<Longrightarrow> (\<Squnion>i. F i)\<cdot>(\<Squnion>i. Y i) = (\<Squnion>i. F i\<cdot>(Y i))"
     1.9 +lemma lub_APP:
    1.10 +  "\<lbrakk>chain F; chain Y\<rbrakk> \<Longrightarrow> (\<Squnion>i. F i\<cdot>(Y i)) = (\<Squnion>i. F i)\<cdot>(\<Squnion>i. Y i)"
    1.11  by (simp add: contlub_cfun_fun contlub_cfun_arg diag_lub)
    1.12  
    1.13 -lemma cont_cfun: 
    1.14 +lemma cont_cfun:
    1.15    "\<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.16  apply (rule thelubE)
    1.17  apply (simp only: ch2ch_Rep_cfun)
    1.18 -apply (simp only: contlub_cfun)
    1.19 +apply (simp only: lub_APP)
    1.20  done
    1.21  
    1.22 -lemma contlub_LAM:
    1.23 +lemma lub_LAM:
    1.24    "\<lbrakk>\<And>x. chain (\<lambda>i. F i x); \<And>i. cont (\<lambda>x. F i x)\<rbrakk>
    1.25 -    \<Longrightarrow> (\<Lambda> x. \<Squnion>i. F i x) = (\<Squnion>i. \<Lambda> x. F i x)"
    1.26 +    \<Longrightarrow> (\<Squnion>i. \<Lambda> x. F i x) = (\<Lambda> x. \<Squnion>i. F i x)"
    1.27  apply (simp add: lub_cfun)
    1.28  apply (simp add: Abs_cfun_inverse2)
    1.29  apply (simp add: thelub_fun ch2ch_lambda)
    1.30  done
    1.31  
    1.32 -lemmas lub_distribs = 
    1.33 -  contlub_cfun [symmetric]
    1.34 -  contlub_LAM [symmetric]
    1.35 +lemmas lub_distribs = lub_APP lub_LAM
    1.36  
    1.37  text {* strictness *}
    1.38  
    1.39 @@ -278,7 +276,7 @@
    1.40  text {* type @{typ "'a -> 'b"} is chain complete *}
    1.41  
    1.42  lemma lub_cfun: "chain F \<Longrightarrow> range F <<| (\<Lambda> x. \<Squnion>i. F i\<cdot>x)"
    1.43 -by (simp only: contlub_cfun_fun [symmetric] eta_cfun thelubE)
    1.44 +by (simp only: contlub_cfun_fun [symmetric] eta_cfun cpo_lubI)
    1.45  
    1.46  lemma thelub_cfun: "chain F \<Longrightarrow> (\<Squnion>i. F i) = (\<Lambda> x. \<Squnion>i. F i\<cdot>x)"
    1.47  by (rule lub_cfun [THEN lub_eqI])