# HG changeset patch
# User huffman
# Date 1201810923 -3600
# Node ID d5129e6872908d47fee1a6f44c461048db491797
# Parent  29c1e3e98276a446822724c7f63b049b96d03492
new lemma cont_discrete_cpo

diff -r 29c1e3e98276 -r d5129e687290 src/HOLCF/Cont.thy
--- a/src/HOLCF/Cont.thy	Thu Jan 31 21:21:22 2008 +0100
+++ b/src/HOLCF/Cont.thy	Thu Jan 31 21:22:03 2008 +0100
@@ -229,4 +229,12 @@
 lemma flatdom_strict2cont: "f \<bottom> = \<bottom> \<Longrightarrow> cont (f::'a::flat \<Rightarrow> 'b::pcpo)"
 by (rule flatdom_strict2mono [THEN chfindom_monofun2cont])
 
+text {* functions with discrete domain *}
+
+lemma cont_discrete_cpo [simp]: "cont (f::'a::discrete_cpo \<Rightarrow> 'b::cpo)"
+apply (rule contI)
+apply (drule discrete_chain_const, clarify)
+apply (simp add: lub_const)
+done
+
 end