src/HOL/UNITY/Token.thy
author paulson
Tue Sep 01 15:07:11 1998 +0200 (1998-09-01)
changeset 5420 b48ab3281944
parent 5277 e4297d03e5d2
child 5608 a82a038a3e7a
permissions -rw-r--r--
New approach, using a locale
     1 (*  Title:      HOL/UNITY/Token
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1998  University of Cambridge
     5 
     6 The Token Ring.
     7 
     8 From Misra, "A Logic for Concurrent Programming" (1994), sections 5.2 and 13.2.
     9 *)
    10 
    11 
    12 Token = WFair + 
    13 
    14 (*process states*)
    15 datatype pstate = Hungry | Eating | Thinking
    16 
    17 record state =
    18   token :: nat
    19   proc  :: nat => pstate
    20 
    21 
    22 constdefs
    23   HasTok :: nat => state set
    24     "HasTok i == {s. token s = i}"
    25 
    26   H :: nat => state set
    27     "H i == {s. proc s i = Hungry}"
    28 
    29   E :: nat => state set
    30     "E i == {s. proc s i = Eating}"
    31 
    32   T :: nat => state set
    33     "T i == {s. proc s i = Thinking}"
    34 
    35 
    36 locale Token =
    37   fixes
    38     N         :: nat	 (*number of nodes in the ring*)
    39     acts      :: "(state*state)set set"
    40     nodeOrder :: "nat => (nat*nat)set"
    41     next      :: nat => nat
    42 
    43   assumes
    44     N_positive "0<N"
    45 
    46     skip "id: acts"
    47 
    48     TR2  "!!i. constrains acts (T i) (T i Un H i)"
    49 
    50     TR3  "!!i. constrains acts (H i) (H i Un E i)"
    51 
    52     TR4  "!!i. constrains acts (H i - HasTok i) (H i)"
    53 
    54     TR5  "!!i. constrains acts (HasTok i) (HasTok i Un Compl(E i))"
    55 
    56     TR6  "!!i. leadsTo acts (H i Int HasTok i) (E i)"
    57 
    58     TR7  "!!i. leadsTo acts (HasTok i) (HasTok (next i))"
    59 
    60   defines
    61     nodeOrder_def
    62       "nodeOrder j == (inv_image less_than (%i. ((j+N)-i) mod N))  Int
    63 		      (lessThan N Times lessThan N)"
    64 
    65     next_def
    66       "next i == (Suc i) mod N"
    67 
    68 end