src/HOL/UNITY/Channel.thy
author paulson
Fri Apr 03 12:34:33 1998 +0200 (1998-04-03)
changeset 4776 1f9362e769c1
child 5253 82a5ca6290aa
permissions -rw-r--r--
New UNITY theory
     1 (*  Title:      HOL/UNITY/Channel
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1998  University of Cambridge
     5 
     6 Unordered Channel
     7 
     8 From Misra, "A Logic for Concurrent Programming" (1994), section 13.3
     9 *)
    10 
    11 Channel = WFair + Option + 
    12 
    13 types state = nat set
    14 
    15 constdefs
    16   minSet :: nat set => nat option
    17     "minSet A == if A={} then None else Some (LEAST x. x:A)"
    18 
    19 rules
    20 
    21   skip "id: Acts"
    22 
    23   UC1  "constrains Acts (minSet -`` {Some x}) (minSet -`` (Some``atLeast x))"
    24 
    25   (*  UC1  "constrains Acts {s. minSet s = x} {s. x <= minSet s}"  *)
    26 
    27   UC2  "leadsTo Acts (minSet -`` {Some x}) {s. x ~: s}"
    28 
    29 end