src/HOL/UNITY/Channel.thy
author paulson
Wed Aug 05 10:57:25 1998 +0200 (1998-08-05)
changeset 5253 82a5ca6290aa
parent 4776 1f9362e769c1
child 5608 a82a038a3e7a
permissions -rw-r--r--
New record type of programs
paulson@4776
     1
(*  Title:      HOL/UNITY/Channel
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
Unordered Channel
paulson@4776
     7
paulson@4776
     8
From Misra, "A Logic for Concurrent Programming" (1994), section 13.3
paulson@4776
     9
*)
paulson@4776
    10
paulson@4776
    11
Channel = WFair + Option + 
paulson@4776
    12
paulson@4776
    13
types state = nat set
paulson@4776
    14
paulson@4776
    15
constdefs
paulson@4776
    16
  minSet :: nat set => nat option
paulson@4776
    17
    "minSet A == if A={} then None else Some (LEAST x. x:A)"
paulson@4776
    18
paulson@4776
    19
rules
paulson@4776
    20
paulson@5253
    21
  skip "id: acts"
paulson@4776
    22
paulson@5253
    23
  UC1  "constrains acts (minSet -`` {Some x}) (minSet -`` (Some``atLeast x))"
paulson@4776
    24
paulson@5253
    25
  (*  UC1  "constrains acts {s. minSet s = x} {s. x <= minSet s}"  *)
paulson@4776
    26
paulson@5253
    27
  UC2  "leadsTo acts (minSet -`` {Some x}) {s. x ~: s}"
paulson@4776
    28
paulson@4776
    29
end