src/HOL/UNITY/Token.thy
author paulson
Fri, 31 Jul 1998 18:46:55 +0200
changeset 5232 e5a7cdd07ea5
parent 4776 1f9362e769c1
child 5253 82a5ca6290aa
permissions -rw-r--r--
Tidied; uses records
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
     1
(*  Title:      HOL/UNITY/Token
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 Token Ring.
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), sections 5.2 and 13.2.
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
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    12
Token = WFair +
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    13
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    14
(*process states*)
5232
e5a7cdd07ea5 Tidied; uses records
paulson
parents: 4776
diff changeset
    15
datatype pstate = Hungry | Eating | Thinking
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    16
5232
e5a7cdd07ea5 Tidied; uses records
paulson
parents: 4776
diff changeset
    17
record state =
e5a7cdd07ea5 Tidied; uses records
paulson
parents: 4776
diff changeset
    18
  token :: nat
e5a7cdd07ea5 Tidied; uses records
paulson
parents: 4776
diff changeset
    19
  proc  :: nat => pstate
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    20
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    21
consts
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    22
  N :: nat	(*number of nodes in the ring*)
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    23
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    24
constdefs
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    25
  nodeOrder :: "nat => (nat*nat)set"
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    26
    "nodeOrder j == (inv_image less_than (%i. ((j+N)-i) mod N))  Int
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    27
                    (lessThan N Times lessThan N)"
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    28
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    29
  next      :: nat => nat
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    30
    "next i == (Suc i) mod N"
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    31
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    32
  HasTok :: nat => state set
5232
e5a7cdd07ea5 Tidied; uses records
paulson
parents: 4776
diff changeset
    33
    "HasTok i == {s. token s = i}"
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    34
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    35
  H :: nat => state set
5232
e5a7cdd07ea5 Tidied; uses records
paulson
parents: 4776
diff changeset
    36
    "H i == {s. proc s i = Hungry}"
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    37
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    38
  E :: nat => state set
5232
e5a7cdd07ea5 Tidied; uses records
paulson
parents: 4776
diff changeset
    39
    "E i == {s. proc s i = Eating}"
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    40
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    41
  T :: nat => state set
5232
e5a7cdd07ea5 Tidied; uses records
paulson
parents: 4776
diff changeset
    42
    "T i == {s. proc s i = Thinking}"
4776
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    43
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    44
rules
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    45
  N_positive "0<N"
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    46
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    47
  skip "id: Acts"
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    48
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    49
  TR2  "constrains Acts (T i) (T i Un H i)"
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    50
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    51
  TR3  "constrains Acts (H i) (H i Un E i)"
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    52
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    53
  TR4  "constrains Acts (H i - HasTok i) (H i)"
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    54
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    55
  TR5  "constrains Acts (HasTok i) (HasTok i Un Compl(E i))"
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    56
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    57
  TR6  "leadsTo Acts (H i Int HasTok i) (E i)"
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    58
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    59
  TR7  "leadsTo Acts (HasTok i) (HasTok (next i))"
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    60
1f9362e769c1 New UNITY theory
paulson
parents:
diff changeset
    61
end