equal
deleted
inserted
replaced
|
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 |