author | kleing |
Mon, 12 May 2003 15:07:11 +0200 | |
changeset 14014 | f3f16f9f2030 |
parent 12195 | ed2893765a08 |
child 14092 | 68da54626309 |
permissions | -rw-r--r-- |
11479 | 1 |
(* Title: ZF/UNITY/FP.thy |
2 |
ID: $Id$ |
|
3 |
Author: Sidi O Ehmety, Computer Laboratory |
|
4 |
Copyright 2001 University of Cambridge |
|
5 |
||
6 |
Fixed Point of a Program |
|
7 |
||
8 |
From Misra, "A Logic for Concurrent Programming", 1994 |
|
9 |
||
10 |
Theory ported from HOL. |
|
11 |
*) |
|
12 |
||
13 |
FP = UNITY + |
|
14 |
||
15 |
constdefs |
|
16 |
FP_Orig :: i=>i |
|
12195 | 17 |
"FP_Orig(F) == Union({A:Pow(state). ALL B. F : stable(A Int B)})" |
11479 | 18 |
|
19 |
FP :: i=>i |
|
20 |
"FP(F) == {s:state. F : stable({s})}" |
|
21 |
||
22 |
end |