# HG changeset patch
# User huffman
# Date 1112230881 -7200
# Node ID 2d1d6ea579a1cb6cc283a015e42892434ecb09b6
# Parent  99ed5113783b4a8d67c8a82b3f33a7dbe9924aab
chfin now a subclass of po, proved instance chfin < cpo

diff -r 99ed5113783b -r 2d1d6ea579a1 src/HOLCF/Pcpo.thy
--- a/src/HOLCF/Pcpo.thy	Thu Mar 31 02:52:49 2005 +0200
+++ b/src/HOLCF/Pcpo.thy	Thu Mar 31 03:01:21 2005 +0200
@@ -199,7 +199,7 @@
 
 text {* further useful classes for HOLCF domains *}
 
-axclass chfin < cpo
+axclass chfin < po
   chfin: 	"!Y. chain Y-->(? n. max_in_chain n Y)"
 
 axclass flat < pcpo
@@ -207,10 +207,20 @@
 
 text {* some properties for chfin and flat *}
 
+text {* chfin types are cpo *}
+
+lemma chfin_imp_cpo:
+  "chain (S::nat=>'a::chfin) ==> EX x. range S <<| x"
+apply (frule chfin [rule_format])
+apply (blast intro: lub_finch1)
+done
+
+instance chfin < cpo
+by intro_classes (rule chfin_imp_cpo)
+
 text {* flat types are chfin *}
 
 lemma flat_imp_chfin: 
-  -- {*Used only in an "instance" declaration (Fun1.thy)*}
      "ALL Y::nat=>'a::flat. chain Y --> (EX n. max_in_chain n Y)"
 apply (unfold max_in_chain_def)
 apply clarify