author huffman Wed Oct 13 10:27:26 2010 -0700 (2010-10-13) changeset 40010 d7fdd84b959f parent 40009 f2c78550c0b7 child 40011 b974cf829099
 src/HOLCF/Cont.thy file | annotate | diff | revisions
```     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)
```