# HG changeset patch
# User huffman
# Date 1231985105 28800
# Node ID 59bee7985149aad5e55df04c968e74fef7b24449
# Parent  2eb29775b0b699feac0189db4d9234015c8a83c8
add lemmas cont2monofunE, cont2cont_apply

diff -r 2eb29775b0b6 -r 59bee7985149 src/HOLCF/Cont.thy
--- 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]: