src/HOLCF/cont.thy
author wenzelm
Thu Aug 27 20:46:36 1998 +0200 (1998-08-27)
changeset 5400 645f46a24c72
parent 243 c22b85994e17
permissions -rw-r--r--
made tutorial first;
nipkow@243
     1
(*  Title: 	HOLCF/cont.thy
nipkow@243
     2
    ID:         $Id$
nipkow@243
     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
nipkow@243
    14
   of default class pcpo
nipkow@243
    15
nipkow@243
    16
*)
nipkow@243
    17
nipkow@243
    18
nipkow@243
    19
default pcpo
nipkow@243
    20
nipkow@243
    21
consts  
nipkow@243
    22
	monofun :: "('a::po => 'b::po) => bool"	(* monotonicity    *)
nipkow@243
    23
	contlub	:: "('a => 'b) => bool"		(* first cont. def *)
nipkow@243
    24
	contX	:: "('a => 'b) => bool"		(* secnd cont. def *)
nipkow@243
    25
nipkow@243
    26
rules 
nipkow@243
    27
nipkow@243
    28
monofun		"monofun(f) == ! x y. x << y --> f(x) << f(y)"
nipkow@243
    29
nipkow@243
    30
contlub		"contlub(f) == ! Y. is_chain(Y) --> \
nipkow@243
    31
\				f(lub(range(Y))) = lub(range(% i.f(Y(i))))"
nipkow@243
    32
nipkow@243
    33
contX		"contX(f)   == ! Y. is_chain(Y) --> \
nipkow@243
    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:                                 *)
nipkow@243
    38
(*              monofun(f) & contlub(f)  <==> contX(f)                      *)
nipkow@243
    39
(* ------------------------------------------------------------------------ *)
nipkow@243
    40
nipkow@243
    41
end