src/HOLCF/Cont.thy
author kleing
Mon Jun 21 10:25:57 2004 +0200 (2004-06-21)
changeset 14981 e73f8140af78
parent 12030 46d57d0290a2
child 15565 2454493bd77b
permissions -rw-r--r--
Merged in license change from Isabelle2004
     1 (*  Title:      HOLCF/cont.thy
     2     ID:         $Id$
     3     Author:     Franz Regensburger
     4 
     5     Results about continuity and monotonicity
     6 *)
     7 
     8 Cont = Fun3 +
     9 
    10 (* 
    11 
    12    Now we change the default class! Form now on all untyped typevariables are
    13    of default class po
    14 
    15 *)
    16 
    17 
    18 default po
    19 
    20 consts  
    21         monofun :: "('a => 'b) => bool" (* monotonicity    *)
    22         contlub :: "('a::cpo => 'b::cpo) => bool"         (* first cont. def *)
    23         cont    :: "('a::cpo => 'b::cpo) => bool"         (* secnd cont. def *)
    24 
    25 defs 
    26 
    27 monofun         "monofun(f) == ! x y. x << y --> f(x) << f(y)"
    28 
    29 contlub         "contlub(f) == ! Y. chain(Y) --> 
    30                                 f(lub(range(Y))) = lub(range(% i. f(Y(i))))"
    31 
    32 cont            "cont(f)   == ! Y. chain(Y) --> 
    33                                 range(% i. f(Y(i))) <<| f(lub(range(Y)))"
    34 
    35 (* ------------------------------------------------------------------------ *)
    36 (* the main purpose of cont.thy is to show:                                 *)
    37 (*              monofun(f) & contlub(f)  <==> cont(f)                       *)
    38 (* ------------------------------------------------------------------------ *)
    39 
    40 end