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
```