src/HOLCF/Cont.thy

arith_tac should not produce counter example

(*  Title:      HOLCF/cont.thy
    ID:         $Id$
    Author:     Franz Regensburger
    License:    GPL (GNU GENERAL PUBLIC LICENSE)

    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. chain(Y) --> 
                                f(lub(range(Y))) = lub(range(% i. f(Y(i))))"

cont            "cont(f)   == ! Y. 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