src/HOLCF/Cont.thy
author nipkow
Tue, 13 Aug 2002 22:01:53 +0200
changeset 13501 79242cccaddc
parent 12030 46d57d0290a2
child 14981 e73f8140af78
permissions -rw-r--r--
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