src/HOLCF/Cont.thy

New function read_cterms is a combination of read_def_cterm and
read_cterm. It reads and simultaneously type-checks a list of strings.
cterm_of no longer catches exception TYPE; instead it must be caught later on
and a message printed using Sign.exn_type_msg. More informative messages can
be printed this way.

(*  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 pcpo

*)


default pcpo

consts  
	monofun :: "('a::po => 'b::po) => bool"	(* monotonicity    *)
	contlub	:: "('a => 'b) => bool"		(* first cont. def *)
	cont	:: "('a => 'b) => 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