src/HOL/Lfp.thy
changeset 15140 322485b816ac
parent 15131 c69542757a4d
child 15386 06757406d8cf
equal deleted inserted replaced
15139:58cd3404cf75 15140:322485b816ac
     5 
     5 
     6 The Knaster-Tarski Theorem
     6 The Knaster-Tarski Theorem
     7 *)
     7 *)
     8 
     8 
     9 theory Lfp
     9 theory Lfp
    10 import Product_Type
    10 imports Product_Type
    11 begin
    11 begin
    12 
    12 
    13 constdefs
    13 constdefs
    14   lfp :: "['a set \<Rightarrow> 'a set] \<Rightarrow> 'a set"
    14   lfp :: "['a set \<Rightarrow> 'a set] \<Rightarrow> 'a set"
    15   "lfp(f) == Inter({u. f(u) <= u})"    (*least fixed point*)
    15   "lfp(f) == Inter({u. f(u) <= u})"    (*least fixed point*)