# HG changeset patch
# User huffman
# Date 1199394584 -3600
# Node ID eb181909e7a4aa7c9a57c12689f0f0be784106ff
# Parent  641b4da8eb9d18aeda2e1f79ea7e36d6b4b36987
new axclass finite_po < finite, po

diff -r 641b4da8eb9d -r eb181909e7a4 src/HOLCF/Pcpo.thy
--- a/src/HOLCF/Pcpo.thy	Thu Jan 03 22:08:54 2008 +0100
+++ b/src/HOLCF/Pcpo.thy	Thu Jan 03 22:09:44 2008 +0100
@@ -272,12 +272,30 @@
 
 text {* further useful classes for HOLCF domains *}
 
+axclass finite_po < finite, po
+
 axclass chfin < po
   chfin: "\<forall>Y. chain Y \<longrightarrow> (\<exists>n. max_in_chain n Y)"
 
 axclass flat < pcpo
   ax_flat: "\<forall>x y. x \<sqsubseteq> y \<longrightarrow> (x = \<bottom>) \<or> (x = y)"
 
+text {* finite partial orders are chain-finite and directed-complete *}
+
+instance finite_po < chfin
+apply (intro_classes, clarify)
+apply (drule finite_range_imp_finch)
+apply (rule finite)
+apply (simp add: finite_chain_def)
+done
+
+instance finite_po < dcpo
+apply intro_classes
+apply (drule directed_finiteD [OF _ finite subset_refl])
+apply (erule bexE, rule exI)
+apply (erule (1) is_lub_maximal)
+done
+
 text {* some properties for chfin and flat *}
 
 text {* chfin types are cpo *}