src/HOLCF/cont.thy
author nipkow
Wed Jan 19 17:35:01 1994 +0100 (1994-01-19)
changeset 243 c22b85994e17
permissions -rw-r--r--
Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF
in HOL.
     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 pcpo
    15 
    16 *)
    17 
    18 
    19 default pcpo
    20 
    21 consts  
    22 	monofun :: "('a::po => 'b::po) => bool"	(* monotonicity    *)
    23 	contlub	:: "('a => 'b) => bool"		(* first cont. def *)
    24 	contX	:: "('a => 'b) => bool"		(* secnd cont. def *)
    25 
    26 rules 
    27 
    28 monofun		"monofun(f) == ! x y. x << y --> f(x) << f(y)"
    29 
    30 contlub		"contlub(f) == ! Y. is_chain(Y) --> \
    31 \				f(lub(range(Y))) = lub(range(% i.f(Y(i))))"
    32 
    33 contX		"contX(f)   == ! Y. is_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)  <==> contX(f)                      *)
    39 (* ------------------------------------------------------------------------ *)
    40 
    41 end