--- a/src/HOLCF/Cont.thy Wed Jan 14 17:12:21 2009 -0800
+++ b/src/HOLCF/Cont.thy Wed Jan 14 18:05:05 2009 -0800
@@ -104,6 +104,8 @@
apply simp
done
+lemmas cont2monofunE = cont2mono [THEN monofunE]
+
lemmas ch2ch_cont = cont2mono [THEN ch2ch_monofun]
text {* right to left: @{prop "cont f \<Longrightarrow> monofun f \<and> contlub f"} *}
@@ -183,6 +185,34 @@
apply (rule lub_const)
done
+text {* application of functions is continuous *}
+
+lemma cont2cont_apply:
+ fixes f :: "'a::cpo \<Rightarrow> 'b::cpo \<Rightarrow> 'c::cpo" and t :: "'a \<Rightarrow> 'b"
+ assumes f1: "\<And>y. cont (\<lambda>x. f x y)"
+ assumes f2: "\<And>x. cont (\<lambda>y. f x y)"
+ assumes t: "cont (\<lambda>x. t x)"
+ shows "cont (\<lambda>x. (f x) (t x))"
+proof (rule monocontlub2cont [OF monofunI contlubI])
+ fix x y :: "'a" assume "x \<sqsubseteq> y"
+ then show "f x (t x) \<sqsubseteq> f y (t y)"
+ by (auto intro: cont2monofunE [OF f1]
+ cont2monofunE [OF f2]
+ cont2monofunE [OF t]
+ trans_less)
+next
+ fix Y :: "nat \<Rightarrow> 'a" assume "chain Y"
+ then show "f (\<Squnion>i. Y i) (t (\<Squnion>i. Y i)) = (\<Squnion>i. f (Y i) (t (Y i)))"
+ by (simp only: cont2contlubE [OF t] ch2ch_cont [OF t]
+ cont2contlubE [OF f1] ch2ch_cont [OF f1]
+ cont2contlubE [OF f2] ch2ch_cont [OF f2]
+ diag_lub)
+qed
+
+lemma cont2cont_compose:
+ "\<lbrakk>cont c; cont (\<lambda>x. f x)\<rbrakk> \<Longrightarrow> cont (\<lambda>x. c (f x))"
+by (rule cont2cont_apply [OF cont_const])
+
text {* if-then-else is continuous *}
lemma cont_if [simp]: