|
7626
|
1 |
(* Title: HOL/BCV/Fixpoint.thy
|
|
|
2 |
ID: $Id$
|
|
|
3 |
Author: Tobias Nipkow
|
|
|
4 |
Copyright 1999 TUM
|
|
|
5 |
|
|
|
6 |
Searching for a fixpoint.
|
|
|
7 |
*)
|
|
|
8 |
|
|
|
9 |
Fixpoint = SemiLattice +
|
|
|
10 |
|
|
|
11 |
consts fix :: "('a => 'a option) * 'a => bool"
|
|
|
12 |
recdef fix
|
|
|
13 |
"{((nxt,t),(nxs,s)) . nxt=nxs &
|
|
|
14 |
~(? f. f 0 = s & (!i. nxt (f i) = Some(f(i+1)) & f(i+1) ~= f i)) &
|
|
|
15 |
nxs s = Some t & t ~= s}"
|
|
|
16 |
"fix(next,s) =
|
|
|
17 |
(if (? f. f 0 = s & (!i. next (f i) = Some(f(i+1)) & f(i+1) ~= f i))
|
|
|
18 |
then arbitrary
|
|
|
19 |
else case next s of None => False |
|
|
|
20 |
Some t => if t=s then True else fix(next,t))"
|
|
|
21 |
|
|
|
22 |
|
|
|
23 |
end
|