diff -r f7f812034707 -r f363e6e080e7 src/HOLCF/Porder.thy --- a/src/HOLCF/Porder.thy Mon Mar 07 23:30:06 2005 +0100 +++ b/src/HOLCF/Porder.thy Mon Mar 07 23:54:01 2005 +0100 @@ -7,16 +7,18 @@ Conservative extension of theory Porder0 by constant definitions *) -header {* Type class of partial orders *} +header {* Partial orders *} theory Porder imports Main begin - (* introduce a (syntactic) class for the constant << *) +subsection {* Type class for partial orders *} + + -- {* introduce a (syntactic) class for the constant @{text "<<"} *} axclass sq_ord < type - (* characteristic constant << for po *) + -- {* characteristic constant @{text "<<"} for po *} consts "<<" :: "['a,'a::sq_ord] => bool" (infixl 55) @@ -24,7 +26,7 @@ "op <<" :: "['a,'a::sq_ord] => bool" (infixl "\" 55) axclass po < sq_ord - (* class axioms: *) + -- {* class axioms: *} refl_less [iff]: "x << x" antisym_less: "[|x << y; y << x |] ==> x = y" trans_less: "[|x << y; y << z |] ==> x << z" @@ -51,7 +53,7 @@ apply (fast elim!: antisym_less_inverse intro!: antisym_less) done -subsection {* Constant definitions *} +subsection {* Chains and least upper bounds *} consts "<|" :: "['a set,'a::po] => bool" (infixl 55) @@ -73,17 +75,17 @@ defs -(* class definitions *) +-- {* class definitions *} is_ub_def: "S <| x == ! y. y:S --> y< x << u)" -(* Arbitrary chains are total orders *) +-- {* Arbitrary chains are total orders *} tord_def: "tord S == !x y. x:S & y:S --> (x< C(i) = C(j)" finite_chain_def: "finite_chain C == chain(C) & (? i. max_in_chain i C)" @@ -187,7 +189,7 @@ done lemmas is_ub_lub = is_lubD1 [THEN ub_rangeD, standard] -(* range(?S1) <<| ?x1 ==> ?S1(?x) << ?x1 *) + -- {* @{thm is_ub_lub} *} (* range(?S1) <<| ?x1 ==> ?S1(?x) << ?x1 *) text {* results about finite chains *}