| changeset 116 | ab4328bbff70 |
| parent 0 | 7949f97df77a |
| child 178 | 12dd5d2e266b |
| 115:0ec63df3ae04 | 116:ab4328bbff70 |
|---|---|
4 Copyright 1992 University of Cambridge |
4 Copyright 1992 University of Cambridge |
5 |
5 |
6 The Knaster-Tarski Theorem |
6 The Knaster-Tarski Theorem |
7 *) |
7 *) |
8 |
8 |
9 Lfp = Sum + |
9 Lfp = mono + |
10 consts lfp :: "['a set=>'a set] => 'a set" |
10 consts lfp :: "['a set=>'a set] => 'a set" |
11 rules |
11 rules |
12 (*least fixed point*) |
12 (*least fixed point*) |
13 lfp_def "lfp(f) == Inter({u. f(u) <= u})" |
13 lfp_def "lfp(f) == Inter({u. f(u) <= u})" |
14 end |
14 end |