# HG changeset patch
# User huffman
# Date 1291663362 28800
# Node ID 9883d1417ce1c4ef6fce0354309cd1746c242b9d
# Parent  ff7d177128ef0da39e48e27747dd333fcd9eac14
remove lemma cont_cfun;
rename thelub_cfun to lub_cfun

diff -r ff7d177128ef -r 9883d1417ce1 NEWS
--- a/NEWS	Mon Dec 06 10:08:33 2010 -0800
+++ b/NEWS	Mon Dec 06 11:22:42 2010 -0800
@@ -526,6 +526,7 @@
   lub_bin_chain   ~> is_lub_bin_chain
   lub_fun         ~> is_lub_fun
   thelub_fun      ~> lub_fun
+  thelub_cfun     ~> lub_cfun
   thelub_Pair     ~> lub_Pair
   lub_cprod       ~> is_lub_prod
   thelub_cprod    ~> lub_prod
diff -r ff7d177128ef -r 9883d1417ce1 src/HOL/HOLCF/Cfun.thy
--- a/src/HOL/HOLCF/Cfun.thy	Mon Dec 06 10:08:33 2010 -0800
+++ b/src/HOL/HOLCF/Cfun.thy	Mon Dec 06 11:22:42 2010 -0800
@@ -248,13 +248,6 @@
   "\<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:
-  "\<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: lub_APP)
-done
-
 lemma lub_LAM:
   "\<lbrakk>\<And>x. chain (\<lambda>i. F i x); \<And>i. cont (\<lambda>x. F i x)\<rbrakk>
     \<Longrightarrow> (\<Squnion>i. \<Lambda> x. F i x) = (\<Lambda> x. \<Squnion>i. F i x)"
@@ -275,11 +268,8 @@
 
 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 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])
+lemma lub_cfun: "chain F \<Longrightarrow> (\<Squnion>i. F i) = (\<Lambda> x. \<Squnion>i. F i\<cdot>x)"
+by (simp add: lub_cfun lub_fun ch2ch_lambda)
 
 subsection {* Continuity simplification procedure *}