src/HOL/BCV/Fixpoint.thy

updated;

(*  Title:      HOL/BCV/Fixpoint.thy
    ID:         $Id$
    Author:     Tobias Nipkow
    Copyright   1999 TUM

Searching for a fixpoint.
*)

Fixpoint = SemiLattice +

consts fix :: "('a => 'a option) * 'a => bool"
recdef fix
 "{((nxt,t),(nxs,s)) . nxt=nxs &
      ~(? f. f 0 = s & (!i. nxt (f i) = Some(f(i+1)) & f(i+1) ~= f i)) &
      nxs s = Some t & t ~= s}"
"fix(next,s) =
  (if (? f. f 0 = s & (!i. next (f i) = Some(f(i+1)) & f(i+1) ~= f i))
   then arbitrary
   else case next s of None => False |
                       Some t => if t=s then True else fix(next,t))"


end