# HG changeset patch
# User huffman
# Date 1286887695 25200
# Node ID 9f6ed6840e8d66d45e4ddd342ebf97522d7490c9
# Parent  427106657e044712433dd2cc3f5a172f5b17e7e3
reformulate lemma cont2cont_lub and move to Cont.thy

diff -r 427106657e04 -r 9f6ed6840e8d src/HOLCF/Cont.thy
--- a/src/HOLCF/Cont.thy	Tue Oct 12 05:25:21 2010 -0700
+++ b/src/HOLCF/Cont.thy	Tue Oct 12 05:48:15 2010 -0700
@@ -22,12 +22,6 @@
   monofun :: "('a \<Rightarrow> 'b) \<Rightarrow> bool"  -- "monotonicity"  where
   "monofun f = (\<forall>x y. x \<sqsubseteq> y \<longrightarrow> f x \<sqsubseteq> f y)"
 
-(*
-definition
-  contlub :: "('a::cpo \<Rightarrow> 'b::cpo) \<Rightarrow> bool"  -- "first cont. def" where
-  "contlub f = (\<forall>Y. chain Y \<longrightarrow> f (\<Squnion>i. Y i) = (\<Squnion>i. f (Y i)))"
-*)
-
 definition
   cont :: "('a::cpo \<Rightarrow> 'b::cpo) \<Rightarrow> bool"
 where
@@ -176,6 +170,17 @@
   "\<lbrakk>cont c; cont (\<lambda>x. f x)\<rbrakk> \<Longrightarrow> cont (\<lambda>x. c (f x))"
 by (rule cont_apply [OF _ _ cont_const])
 
+text {* Least upper bounds preserve continuity *}
+
+lemma cont2cont_lub [simp]:
+  assumes chain: "\<And>x. chain (\<lambda>i. F i x)" and cont: "\<And>i. cont (\<lambda>x. F i x)"
+  shows "cont (\<lambda>x. \<Squnion>i. F i x)"
+apply (rule contI2)
+apply (simp add: monofunI cont2monofunE [OF cont] lub_mono chain)
+apply (simp add: cont2contlubE [OF cont])
+apply (simp add: diag_lub ch2ch_cont [OF cont] chain)
+done
+
 text {* if-then-else is continuous *}
 
 lemma cont_if [simp, cont2cont]:
diff -r 427106657e04 -r 9f6ed6840e8d src/HOLCF/Fix.thy
--- a/src/HOLCF/Fix.thy	Tue Oct 12 05:25:21 2010 -0700
+++ b/src/HOLCF/Fix.thy	Tue Oct 12 05:48:15 2010 -0700
@@ -60,13 +60,7 @@
 text {* direct connection between @{term fix} and iteration *}
 
 lemma fix_def2: "fix\<cdot>F = (\<Squnion>i. iterate i\<cdot>F\<cdot>\<bottom>)"
-apply (unfold fix_def)
-apply (rule beta_cfun)
-apply (rule cont2cont_lub)
-apply (rule ch2ch_lambda)
-apply (rule chain_iterate)
-apply simp
-done
+unfolding fix_def by simp
 
 lemma iterate_below_fix: "iterate n\<cdot>f\<cdot>\<bottom> \<sqsubseteq> fix\<cdot>f"
   unfolding fix_def2
diff -r 427106657e04 -r 9f6ed6840e8d src/HOLCF/Fun_Cpo.thy
--- a/src/HOLCF/Fun_Cpo.thy	Tue Oct 12 05:25:21 2010 -0700
+++ b/src/HOLCF/Fun_Cpo.thy	Tue Oct 12 05:48:15 2010 -0700
@@ -204,10 +204,6 @@
 apply (simp add: diag_lub ch2ch_fun ch2ch_cont)
 done
 
-lemma cont2cont_lub:
-  "\<lbrakk>chain F; \<And>i. cont (F i)\<rbrakk> \<Longrightarrow> cont (\<lambda>x. \<Squnion>i. F i x)"
-by (simp add: thelub_fun [symmetric] cont_lub_fun)
-
 lemma mono2mono_fun: "monofun f \<Longrightarrow> monofun (\<lambda>x. f x y)"
 apply (rule monofunI)
 apply (erule (1) monofun_fun_arg [THEN monofun_fun_fun])