src/HOLCF/Cont.thy
 changeset 40010 d7fdd84b959f parent 40004 9f6ed6840e8d child 40736 72857de90621
```--- 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 @@
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 @@
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)```