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 

124

9 
Fixedpt = ZF + "domrange" +

0

10 
consts

1401

11 
bnd_mono :: [i,i=>i]=>o


12 
lfp, gfp :: [i,i=>i]=>i

0

13 

753

14 
defs

0

15 
(*monotone operator from Pow(D) to itself*)


16 
bnd_mono_def


17 
"bnd_mono(D,h) == h(D)<=D & (ALL W X. W<=X > X<=D > h(W) <= h(X))"


18 


19 
lfp_def "lfp(D,h) == Inter({X: Pow(D). h(X) <= X})"


20 


21 
gfp_def "gfp(D,h) == Union({X: Pow(D). X <= h(X)})"


22 


23 
end
