src/HOLCF/Cont.thy

eliminated the constant less by the introduction of the axclass sq_ord
added explicit type ::'a::po in the following theorems:
minimal2UU,antisym_less_inverse,box_less,not_less2not_eq,monofun_pair
and dist_eqI (in domain-package)
added instances
instance fun :: (term,sq_ord)sq_ord
instance "->" :: (term,sq_ord)sq_ord
instance "**" :: (sq_ord,sq_ord)sq_ord
instance "*" :: (sq_ord,sq_ord)sq_ord
instance "++" :: (pcpo,pcpo)sq_ord
instance u :: (sq_ord)sq_ord
instance lift :: (term)sq_ord
instance discr :: (term)sq_ord

(*  Title:      HOLCF/cont.thy
    ID:         $Id$
    Author:     Franz Regensburger
    Copyright   1993 Technische Universitaet Muenchen

    Results about continuity and monotonicity
*)

Cont = Fun3 +

(* 

   Now we change the default class! Form now on all untyped typevariables are
   of default class po

*)


default po

consts  
        monofun :: "('a => 'b) => bool" (* monotonicity    *)
        contlub :: "('a::cpo => 'b::cpo) => bool"         (* first cont. def *)
        cont    :: "('a::cpo => 'b::cpo) => bool"         (* secnd cont. def *)

defs 

monofun         "monofun(f) == ! x y. x << y --> f(x) << f(y)"

contlub         "contlub(f) == ! Y. is_chain(Y) --> 
                                f(lub(range(Y))) = lub(range(% i.f(Y(i))))"

cont            "cont(f)   == ! Y. is_chain(Y) --> 
                                range(% i.f(Y(i))) <<| f(lub(range(Y)))"

(* ------------------------------------------------------------------------ *)
(* the main purpose of cont.thy is to show:                                 *)
(*              monofun(f) & contlub(f)  <==> cont(f)                       *)
(* ------------------------------------------------------------------------ *)

end