add lemmas lub_APP, lub_LAM
authorhuffman
Mon Dec 06 08:30:00 2010 -0800 (2010-12-06)
changeset 41027c599955d9806
parent 41018 83f241623b86
child 41028 0acff85f95c7
add lemmas lub_APP, lub_LAM
src/HOL/HOLCF/Cfun.thy
src/HOL/HOLCF/FOCUS/Fstream.thy
src/HOL/HOLCF/HOLCF.thy
src/HOL/HOLCF/Library/List_Cpo.thy
     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])
     2.1 --- a/src/HOL/HOLCF/FOCUS/Fstream.thy	Mon Dec 06 13:46:45 2010 +0100
     2.2 +++ b/src/HOL/HOLCF/FOCUS/Fstream.thy	Mon Dec 06 08:30:00 2010 -0800
     2.3 @@ -250,7 +250,7 @@
     2.4  apply  (rule_tac x="i+j" in exI)
     2.5  apply  (drule fstream_prefix)
     2.6  apply  (clarsimp)
     2.7 -apply  (subst contlub_cfun [symmetric])
     2.8 +apply  (subst lub_APP)
     2.9  apply   (rule chainI)
    2.10  apply   (fast)
    2.11  apply  (erule chain_shift)
     3.1 --- a/src/HOL/HOLCF/HOLCF.thy	Mon Dec 06 13:46:45 2010 +0100
     3.2 +++ b/src/HOL/HOLCF/HOLCF.thy	Mon Dec 06 08:30:00 2010 -0800
     3.3 @@ -32,8 +32,8 @@
     3.4  lemmas cont_Rep_CFun_app_app = cont_APP_app_app
     3.5  lemmas cont_cfun_fun = cont_Rep_cfun1 [THEN contE]
     3.6  lemmas cont_cfun_arg = cont_Rep_cfun2 [THEN contE]
     3.7 -(*
     3.8 +lemmas contlub_cfun = lub_APP [symmetric]
     3.9 +lemmas contlub_LAM = lub_LAM [symmetric]
    3.10  lemmas thelubI = lub_eqI
    3.11 -*)
    3.12  
    3.13  end
     4.1 --- a/src/HOL/HOLCF/Library/List_Cpo.thy	Mon Dec 06 13:46:45 2010 +0100
     4.2 +++ b/src/HOL/HOLCF/Library/List_Cpo.thy	Mon Dec 06 08:30:00 2010 -0800
     4.3 @@ -228,7 +228,7 @@
     4.4      apply (induct rule: list_chain_induct)
     4.5      apply simp
     4.6      apply (simp add: lub_Cons f h)
     4.7 -    apply (simp add: contlub_cfun [symmetric] ch2ch_monofun [OF mono])
     4.8 +    apply (simp add: lub_APP ch2ch_monofun [OF mono])
     4.9      apply (simp add: monofun_cfun)
    4.10      done
    4.11  qed