# HG changeset patch
# User huffman
# Date 1200279271 -3600
# Node ID b2d2f1ae5808766866b65885bdcec0dc5995a6dd
# Parent  0eaadfa8889e21322540c5c98f4b28a4eb28e82b
add lemma contI2

diff -r 0eaadfa8889e -r b2d2f1ae5808 src/HOLCF/Cont.thy
--- a/src/HOLCF/Cont.thy	Mon Jan 14 03:49:53 2008 +0100
+++ b/src/HOLCF/Cont.thy	Mon Jan 14 03:54:31 2008 +0100
@@ -150,6 +150,24 @@
 
 lemmas cont2contlubE = cont2contlub [THEN contlubE]
 
+lemma contI2:
+  assumes mono: "monofun f"
+  assumes less: "\<And>Y. \<lbrakk>chain Y; chain (\<lambda>i. f (Y i))\<rbrakk>
+     \<Longrightarrow> f (lub (range Y)) \<sqsubseteq> (\<Squnion>i. f (Y i))"
+  shows "cont f"
+apply (rule monocontlub2cont)
+apply (rule mono)
+apply (rule contlubI)
+apply (rule antisym_less)
+apply (rule less, assumption)
+apply (erule ch2ch_monofun [OF mono])
+apply (rule is_lub_thelub)
+apply (erule ch2ch_monofun [OF mono])
+apply (rule ub2ub_monofun [OF mono])
+apply (rule is_lubD1)
+apply (erule thelubE, rule refl)
+done
+
 subsection {* Continuity of basic functions *}
 
 text {* The identity function is continuous *}