# HG changeset patch
# User huffman
# Date 1291653000 28800
# Node ID c599955d9806e09f9ae6d2a5bcad1897d681811c
# Parent  83f241623b86632816b570a6e744b4567659ee75
add lemmas lub_APP, lub_LAM

diff -r 83f241623b86 -r c599955d9806 src/HOL/HOLCF/Cfun.thy
--- a/src/HOL/HOLCF/Cfun.thy	Mon Dec 06 13:46:45 2010 +0100
+++ b/src/HOL/HOLCF/Cfun.thy	Mon Dec 06 08:30:00 2010 -0800
@@ -244,28 +244,26 @@
 
 text {* contlub, cont properties of @{term Rep_cfun} in both arguments *}
 
-lemma contlub_cfun: 
-  "\<lbrakk>chain F; chain Y\<rbrakk> \<Longrightarrow> (\<Squnion>i. F i)\<cdot>(\<Squnion>i. Y i) = (\<Squnion>i. F i\<cdot>(Y i))"
+lemma lub_APP:
+  "\<lbrakk>chain F; chain Y\<rbrakk> \<Longrightarrow> (\<Squnion>i. F i\<cdot>(Y i)) = (\<Squnion>i. F i)\<cdot>(\<Squnion>i. Y i)"
 by (simp add: contlub_cfun_fun contlub_cfun_arg diag_lub)
 
-lemma cont_cfun: 
+lemma cont_cfun:
   "\<lbrakk>chain F; chain Y\<rbrakk> \<Longrightarrow> range (\<lambda>i. F i\<cdot>(Y i)) <<| (\<Squnion>i. F i)\<cdot>(\<Squnion>i. Y i)"
 apply (rule thelubE)
 apply (simp only: ch2ch_Rep_cfun)
-apply (simp only: contlub_cfun)
+apply (simp only: lub_APP)
 done
 
-lemma contlub_LAM:
+lemma lub_LAM:
   "\<lbrakk>\<And>x. chain (\<lambda>i. F i x); \<And>i. cont (\<lambda>x. F i x)\<rbrakk>
-    \<Longrightarrow> (\<Lambda> x. \<Squnion>i. F i x) = (\<Squnion>i. \<Lambda> x. F i x)"
+    \<Longrightarrow> (\<Squnion>i. \<Lambda> x. F i x) = (\<Lambda> x. \<Squnion>i. F i x)"
 apply (simp add: lub_cfun)
 apply (simp add: Abs_cfun_inverse2)
 apply (simp add: thelub_fun ch2ch_lambda)
 done
 
-lemmas lub_distribs = 
-  contlub_cfun [symmetric]
-  contlub_LAM [symmetric]
+lemmas lub_distribs = lub_APP lub_LAM
 
 text {* strictness *}
 
@@ -278,7 +276,7 @@
 text {* type @{typ "'a -> 'b"} is chain complete *}
 
 lemma lub_cfun: "chain F \<Longrightarrow> range F <<| (\<Lambda> x. \<Squnion>i. F i\<cdot>x)"
-by (simp only: contlub_cfun_fun [symmetric] eta_cfun thelubE)
+by (simp only: contlub_cfun_fun [symmetric] eta_cfun cpo_lubI)
 
 lemma thelub_cfun: "chain F \<Longrightarrow> (\<Squnion>i. F i) = (\<Lambda> x. \<Squnion>i. F i\<cdot>x)"
 by (rule lub_cfun [THEN lub_eqI])
diff -r 83f241623b86 -r c599955d9806 src/HOL/HOLCF/FOCUS/Fstream.thy
--- a/src/HOL/HOLCF/FOCUS/Fstream.thy	Mon Dec 06 13:46:45 2010 +0100
+++ b/src/HOL/HOLCF/FOCUS/Fstream.thy	Mon Dec 06 08:30:00 2010 -0800
@@ -250,7 +250,7 @@
 apply  (rule_tac x="i+j" in exI)
 apply  (drule fstream_prefix)
 apply  (clarsimp)
-apply  (subst contlub_cfun [symmetric])
+apply  (subst lub_APP)
 apply   (rule chainI)
 apply   (fast)
 apply  (erule chain_shift)
diff -r 83f241623b86 -r c599955d9806 src/HOL/HOLCF/HOLCF.thy
--- a/src/HOL/HOLCF/HOLCF.thy	Mon Dec 06 13:46:45 2010 +0100
+++ b/src/HOL/HOLCF/HOLCF.thy	Mon Dec 06 08:30:00 2010 -0800
@@ -32,8 +32,8 @@
 lemmas cont_Rep_CFun_app_app = cont_APP_app_app
 lemmas cont_cfun_fun = cont_Rep_cfun1 [THEN contE]
 lemmas cont_cfun_arg = cont_Rep_cfun2 [THEN contE]
-(*
+lemmas contlub_cfun = lub_APP [symmetric]
+lemmas contlub_LAM = lub_LAM [symmetric]
 lemmas thelubI = lub_eqI
-*)
 
 end
diff -r 83f241623b86 -r c599955d9806 src/HOL/HOLCF/Library/List_Cpo.thy
--- a/src/HOL/HOLCF/Library/List_Cpo.thy	Mon Dec 06 13:46:45 2010 +0100
+++ b/src/HOL/HOLCF/Library/List_Cpo.thy	Mon Dec 06 08:30:00 2010 -0800
@@ -228,7 +228,7 @@
     apply (induct rule: list_chain_induct)
     apply simp
     apply (simp add: lub_Cons f h)
-    apply (simp add: contlub_cfun [symmetric] ch2ch_monofun [OF mono])
+    apply (simp add: lub_APP ch2ch_monofun [OF mono])
     apply (simp add: monofun_cfun)
     done
 qed