4776

1 
(* Title: HOL/UNITY/UNITY


2 
ID: $Id$


3 
Author: Lawrence C Paulson, Cambridge University Computer Laboratory


4 
Copyright 1998 University of Cambridge


5 


6 
The basic UNITY theory (revised version, based upon the "co" operator)


7 


8 
From Misra, "A Logic for Concurrent Programming", 1994


9 
*)


10 


11 
UNITY = LessThan +


12 


13 
constdefs


14 


15 
constrains :: "[('a * 'a)set set, 'a set, 'a set] => bool"


16 
"constrains Acts A B == ALL act:Acts. act^^A <= B"


17 


18 
stable :: "('a * 'a)set set => 'a set => bool"


19 
"stable Acts A == constrains Acts A A"


20 


21 
strongest_rhs :: "[('a * 'a)set set, 'a set] => 'a set"


22 
"strongest_rhs Acts A == Inter {B. constrains Acts A B}"


23 


24 
unless :: "[('a * 'a)set set, 'a set, 'a set] => bool"


25 
"unless mutex A B == constrains mutex (AB) (A Un B)"


26 


27 
end
