src/HOL/UNITY/FP.thy
author paulson
Fri Apr 03 12:34:33 1998 +0200 (1998-04-03)
changeset 4776 1f9362e769c1
child 5648 fe887910e32e
permissions -rw-r--r--
New UNITY theory
paulson@4776
     1
(*  Title:      HOL/UNITY/FP
paulson@4776
     2
    ID:         $Id$
paulson@4776
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@4776
     4
    Copyright   1998  University of Cambridge
paulson@4776
     5
paulson@4776
     6
Fixed Point of a Program
paulson@4776
     7
paulson@4776
     8
From Misra, "A Logic for Concurrent Programming", 1994
paulson@4776
     9
*)
paulson@4776
    10
paulson@4776
    11
FP = UNITY +
paulson@4776
    12
paulson@4776
    13
constdefs
paulson@4776
    14
paulson@4776
    15
  FP_Orig :: "('a * 'a)set set => 'a set"
paulson@4776
    16
    "FP_Orig Acts == Union{A. ALL B. stable Acts (A Int B)}"
paulson@4776
    17
paulson@4776
    18
  FP :: "('a * 'a)set set => 'a set"
paulson@4776
    19
    "FP Acts == {s. stable Acts {s}}"
paulson@4776
    20
paulson@4776
    21
end