chfin now a subclass of po, proved instance chfin < cpo
authorhuffman
Thu Mar 31 03:01:21 2005 +0200 (2005-03-31 ago)
changeset 156402d1d6ea579a1
parent 15639 99ed5113783b
child 15641 b389f108c485
chfin now a subclass of po, proved instance chfin < cpo
src/HOLCF/Pcpo.thy
     1.1 --- a/src/HOLCF/Pcpo.thy	Thu Mar 31 02:52:49 2005 +0200
     1.2 +++ b/src/HOLCF/Pcpo.thy	Thu Mar 31 03:01:21 2005 +0200
     1.3 @@ -199,7 +199,7 @@
     1.4  
     1.5  text {* further useful classes for HOLCF domains *}
     1.6  
     1.7 -axclass chfin < cpo
     1.8 +axclass chfin < po
     1.9    chfin: 	"!Y. chain Y-->(? n. max_in_chain n Y)"
    1.10  
    1.11  axclass flat < pcpo
    1.12 @@ -207,10 +207,20 @@
    1.13  
    1.14  text {* some properties for chfin and flat *}
    1.15  
    1.16 +text {* chfin types are cpo *}
    1.17 +
    1.18 +lemma chfin_imp_cpo:
    1.19 +  "chain (S::nat=>'a::chfin) ==> EX x. range S <<| x"
    1.20 +apply (frule chfin [rule_format])
    1.21 +apply (blast intro: lub_finch1)
    1.22 +done
    1.23 +
    1.24 +instance chfin < cpo
    1.25 +by intro_classes (rule chfin_imp_cpo)
    1.26 +
    1.27  text {* flat types are chfin *}
    1.28  
    1.29  lemma flat_imp_chfin: 
    1.30 -  -- {*Used only in an "instance" declaration (Fun1.thy)*}
    1.31       "ALL Y::nat=>'a::flat. chain Y --> (EX n. max_in_chain n Y)"
    1.32  apply (unfold max_in_chain_def)
    1.33  apply clarify