src/HOLCF/Cont.thy
author wenzelm
Thu Aug 27 20:46:36 1998 +0200 (1998-08-27)
changeset 5400 645f46a24c72
parent 4721 c8a8482a8124
child 12030 46d57d0290a2
permissions -rw-r--r--
made tutorial first;
     1 (*  Title:      HOLCF/cont.thy
     2     ID:         $Id$
     3     Author:     Franz Regensburger
     4     Copyright   1993 Technische Universitaet Muenchen
     5 
     6     Results about continuity and monotonicity
     7 *)
     8 
     9 Cont = Fun3 +
    10 
    11 (* 
    12 
    13    Now we change the default class! Form now on all untyped typevariables are
    14    of default class po
    15 
    16 *)
    17 
    18 
    19 default po
    20 
    21 consts  
    22         monofun :: "('a => 'b) => bool" (* monotonicity    *)
    23         contlub :: "('a::cpo => 'b::cpo) => bool"         (* first cont. def *)
    24         cont    :: "('a::cpo => 'b::cpo) => bool"         (* secnd cont. def *)
    25 
    26 defs 
    27 
    28 monofun         "monofun(f) == ! x y. x << y --> f(x) << f(y)"
    29 
    30 contlub         "contlub(f) == ! Y. chain(Y) --> 
    31                                 f(lub(range(Y))) = lub(range(% i. f(Y(i))))"
    32 
    33 cont            "cont(f)   == ! Y. chain(Y) --> 
    34                                 range(% i. f(Y(i))) <<| f(lub(range(Y)))"
    35 
    36 (* ------------------------------------------------------------------------ *)
    37 (* the main purpose of cont.thy is to show:                                 *)
    38 (*              monofun(f) & contlub(f)  <==> cont(f)                       *)
    39 (* ------------------------------------------------------------------------ *)
    40 
    41 end