|
1478
|
1 |
(* Title: ZF/fixedpt.thy
|
|
0
|
2 |
ID: $Id$
|
|
1478
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
|
|
0
|
4 |
Copyright 1992 University of Cambridge
|
|
|
5 |
|
|
|
6 |
Least and greatest fixed points
|
|
|
7 |
*)
|
|
|
8 |
|
|
2469
|
9 |
Fixedpt = domrange +
|
|
3923
|
10 |
|
|
|
11 |
global
|
|
|
12 |
|
|
0
|
13 |
consts
|
|
1401
|
14 |
bnd_mono :: [i,i=>i]=>o
|
|
|
15 |
lfp, gfp :: [i,i=>i]=>i
|
|
0
|
16 |
|
|
3923
|
17 |
path Fixedpt
|
|
|
18 |
|
|
753
|
19 |
defs
|
|
0
|
20 |
(*monotone operator from Pow(D) to itself*)
|
|
|
21 |
bnd_mono_def
|
|
|
22 |
"bnd_mono(D,h) == h(D)<=D & (ALL W X. W<=X --> X<=D --> h(W) <= h(X))"
|
|
|
23 |
|
|
|
24 |
lfp_def "lfp(D,h) == Inter({X: Pow(D). h(X) <= X})"
|
|
|
25 |
|
|
|
26 |
gfp_def "gfp(D,h) == Union({X: Pow(D). X <= h(X)})"
|
|
|
27 |
|
|
|
28 |
end
|