--- a/src/HOLCF/Cont.thy Tue Oct 12 09:32:21 2010 -0700
+++ b/src/HOLCF/Cont.thy Wed Oct 13 10:27:26 2010 -0700
@@ -189,7 +189,7 @@
subsection {* Finite chains and flat pcpos *}
-text {* monotone functions map finite chains to finite chains *}
+text {* Monotone functions map finite chains to finite chains. *}
lemma monofun_finch2finch:
"\<lbrakk>monofun f; finite_chain Y\<rbrakk> \<Longrightarrow> finite_chain (\<lambda>n. f (Y n))"
@@ -198,12 +198,14 @@
apply (force simp add: max_in_chain_def)
done
-text {* The same holds for continuous functions *}
+text {* The same holds for continuous functions. *}
lemma cont_finch2finch:
"\<lbrakk>cont f; finite_chain Y\<rbrakk> \<Longrightarrow> finite_chain (\<lambda>n. f (Y n))"
by (rule cont2mono [THEN monofun_finch2finch])
+text {* All monotone functions with chain-finite domain are continuous. *}
+
lemma chfindom_monofun2cont: "monofun f \<Longrightarrow> cont (f::'a::chfin \<Rightarrow> 'b::cpo)"
apply (erule contI2)
apply (frule chfin2finch)
@@ -213,7 +215,7 @@
apply (force simp add: max_in_chain_def)
done
-text {* some properties of flat *}
+text {* All strict functions with flat domain are continuous. *}
lemma flatdom_strict2mono: "f \<bottom> = \<bottom> \<Longrightarrow> monofun (f::'a::flat \<Rightarrow> 'b::pcpo)"
apply (rule monofunI)
@@ -224,7 +226,7 @@
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 *}
+text {* All functions with discrete domain are continuous. *}
lemma cont_discrete_cpo [simp, cont2cont]: "cont (f::'a::discrete_cpo \<Rightarrow> 'b::cpo)"
apply (rule contI)