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;
clasohm@1479
     1
(*  Title:      HOLCF/cont.thy
nipkow@243
     2
    ID:         $Id$
clasohm@1479
     3
    Author:     Franz Regensburger
nipkow@243
     4
    Copyright   1993 Technische Universitaet Muenchen
nipkow@243
     5
nipkow@243
     6
    Results about continuity and monotonicity
nipkow@243
     7
*)
nipkow@243
     8
nipkow@243
     9
Cont = Fun3 +
nipkow@243
    10
nipkow@243
    11
(* 
nipkow@243
    12
nipkow@243
    13
   Now we change the default class! Form now on all untyped typevariables are
slotosch@3323
    14
   of default class po
nipkow@243
    15
nipkow@243
    16
*)
nipkow@243
    17
nipkow@243
    18
slotosch@2838
    19
default po
nipkow@243
    20
nipkow@243
    21
consts  
slotosch@2838
    22
        monofun :: "('a => 'b) => bool" (* monotonicity    *)
slotosch@2838
    23
        contlub :: "('a::cpo => 'b::cpo) => bool"         (* first cont. def *)
slotosch@2838
    24
        cont    :: "('a::cpo => 'b::cpo) => bool"         (* secnd cont. def *)
nipkow@243
    25
regensbu@1168
    26
defs 
nipkow@243
    27
clasohm@1479
    28
monofun         "monofun(f) == ! x y. x << y --> f(x) << f(y)"
nipkow@243
    29
oheimb@4721
    30
contlub         "contlub(f) == ! Y. chain(Y) --> 
wenzelm@3842
    31
                                f(lub(range(Y))) = lub(range(% i. f(Y(i))))"
nipkow@243
    32
oheimb@4721
    33
cont            "cont(f)   == ! Y. chain(Y) --> 
wenzelm@3842
    34
                                range(% i. f(Y(i))) <<| f(lub(range(Y)))"
nipkow@243
    35
nipkow@243
    36
(* ------------------------------------------------------------------------ *)
nipkow@243
    37
(* the main purpose of cont.thy is to show:                                 *)
regensbu@1274
    38
(*              monofun(f) & contlub(f)  <==> cont(f)                       *)
nipkow@243
    39
(* ------------------------------------------------------------------------ *)
nipkow@243
    40
nipkow@243
    41
end