| author | skalberg |
| Wed, 27 Aug 2003 18:13:59 +0200 | |
| changeset 14169 | 0590de71a016 |
| parent 11609 | 3f3d1add4d94 |
| child 15131 | c69542757a4d |
| permissions | -rw-r--r-- |
| clasohm@1475 | 1 |
(* Title: HOL/Lfp.thy |
| clasohm@923 | 2 |
ID: $Id$ |
| clasohm@1475 | 3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
| clasohm@923 | 4 |
Copyright 1992 University of Cambridge |
| clasohm@923 | 5 |
|
| clasohm@923 | 6 |
The Knaster-Tarski Theorem |
| clasohm@923 | 7 |
*) |
| clasohm@923 | 8 |
|
| skalberg@14169 | 9 |
theory Lfp = Product_Type: |
| clasohm@1558 | 10 |
|
| clasohm@1558 | 11 |
constdefs |
| skalberg@14169 | 12 |
lfp :: "['a set \<Rightarrow> 'a set] \<Rightarrow> 'a set" |
| clasohm@1558 | 13 |
"lfp(f) == Inter({u. f(u) <= u})" (*least fixed point*)
|
| clasohm@1558 | 14 |
|
| clasohm@923 | 15 |
end |