# 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: "\Y. chain Y \ (\n. max_in_chain n Y)" axclass flat < pcpo ax_flat: "\x y. x \ y \ (x = \) \ (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 *}