src/HOL/UNITY/UNITY.thy
author paulson
Fri, 03 Apr 1998 12:34:33 +0200
changeset 4776 1f9362e769c1
child 5135 c12a6eb09574
permissions -rw-r--r--
New UNITY theory
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
     1
(*  Title:      HOL/UNITY/UNITY
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
     2
    ID:         $Id$
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
     4
    Copyright   1998  University of Cambridge
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
     5
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
     6
The basic UNITY theory (revised version, based upon the "co" operator)
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
     7
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
     8
From Misra, "A Logic for Concurrent Programming", 1994
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
     9
*)
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    10
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    11
UNITY = LessThan +
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    12
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    13
constdefs
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    14
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    15
  constrains :: "[('a * 'a)set set, 'a set, 'a set] => bool"
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    16
    "constrains Acts A B == ALL act:Acts. act^^A <= B"
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    17
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    18
  stable     :: "('a * 'a)set set => 'a set => bool"
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    19
    "stable Acts A == constrains Acts A A"
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    20
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    21
  strongest_rhs :: "[('a * 'a)set set, 'a set] => 'a set"
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    22
    "strongest_rhs Acts A == Inter {B. constrains Acts A B}"
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    23
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    24
  unless :: "[('a * 'a)set set, 'a set, 'a set] => bool"
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    25
    "unless mutex A B == constrains mutex (A-B) (A Un B)"
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    26
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    27
end