src/HOL/UNITY/UNITY.thy

renamed mutex to Acts

(*  Title:      HOL/UNITY/UNITY
    ID:         $Id$
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1998  University of Cambridge

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

From Misra, "A Logic for Concurrent Programming", 1994
*)

UNITY = LessThan +

constdefs

  constrains :: "[('a * 'a)set set, 'a set, 'a set] => bool"
    "constrains Acts A B == ALL act:Acts. act^^A <= B"

  stable     :: "('a * 'a)set set => 'a set => bool"
    "stable Acts A == constrains Acts A A"

  strongest_rhs :: "[('a * 'a)set set, 'a set] => 'a set"
    "strongest_rhs Acts A == Inter {B. constrains Acts A B}"

  unless :: "[('a * 'a)set set, 'a set, 'a set] => bool"
    "unless Acts A B == constrains Acts (A-B) (A Un B)"

end