edit comments
authorhuffman
Wed Oct 13 10:27:26 2010 -0700 (2010-10-13)
changeset 40010d7fdd84b959f
parent 40009 f2c78550c0b7
child 40011 b974cf829099
edit comments
src/HOLCF/Cont.thy
     1.1 --- a/src/HOLCF/Cont.thy	Tue Oct 12 09:32:21 2010 -0700
     1.2 +++ b/src/HOLCF/Cont.thy	Wed Oct 13 10:27:26 2010 -0700
     1.3 @@ -189,7 +189,7 @@
     1.4  
     1.5  subsection {* Finite chains and flat pcpos *}
     1.6  
     1.7 -text {* monotone functions map finite chains to finite chains *}
     1.8 +text {* Monotone functions map finite chains to finite chains. *}
     1.9  
    1.10  lemma monofun_finch2finch:
    1.11    "\<lbrakk>monofun f; finite_chain Y\<rbrakk> \<Longrightarrow> finite_chain (\<lambda>n. f (Y n))"
    1.12 @@ -198,12 +198,14 @@
    1.13  apply (force simp add: max_in_chain_def)
    1.14  done
    1.15  
    1.16 -text {* The same holds for continuous functions *}
    1.17 +text {* The same holds for continuous functions. *}
    1.18  
    1.19  lemma cont_finch2finch:
    1.20    "\<lbrakk>cont f; finite_chain Y\<rbrakk> \<Longrightarrow> finite_chain (\<lambda>n. f (Y n))"
    1.21  by (rule cont2mono [THEN monofun_finch2finch])
    1.22  
    1.23 +text {* All monotone functions with chain-finite domain are continuous. *}
    1.24 +
    1.25  lemma chfindom_monofun2cont: "monofun f \<Longrightarrow> cont (f::'a::chfin \<Rightarrow> 'b::cpo)"
    1.26  apply (erule contI2)
    1.27  apply (frule chfin2finch)
    1.28 @@ -213,7 +215,7 @@
    1.29  apply (force simp add: max_in_chain_def)
    1.30  done
    1.31  
    1.32 -text {* some properties of flat *}
    1.33 +text {* All strict functions with flat domain are continuous. *}
    1.34  
    1.35  lemma flatdom_strict2mono: "f \<bottom> = \<bottom> \<Longrightarrow> monofun (f::'a::flat \<Rightarrow> 'b::pcpo)"
    1.36  apply (rule monofunI)
    1.37 @@ -224,7 +226,7 @@
    1.38  lemma flatdom_strict2cont: "f \<bottom> = \<bottom> \<Longrightarrow> cont (f::'a::flat \<Rightarrow> 'b::pcpo)"
    1.39  by (rule flatdom_strict2mono [THEN chfindom_monofun2cont])
    1.40  
    1.41 -text {* functions with discrete domain *}
    1.42 +text {* All functions with discrete domain are continuous. *}
    1.43  
    1.44  lemma cont_discrete_cpo [simp, cont2cont]: "cont (f::'a::discrete_cpo \<Rightarrow> 'b::cpo)"
    1.45  apply (rule contI)