src/HOL/UNITY/Token.thy

added option_map_eq_Some via AddIffs

(*  Title:      HOL/UNITY/Token
    ID:         $Id$
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
    Copyright   1998  University of Cambridge

The Token Ring.

From Misra, "A Logic for Concurrent Programming" (1994), sections 5.2 and 13.2.
*)


Token = WFair +

(*process states*)
datatype pstate = Hungry | Eating | Thinking | Pnum nat

types state = nat => pstate

consts
  N :: nat	(*number of nodes in the ring*)

constdefs
  nodeOrder :: "nat => (nat*nat)set"
    "nodeOrder j == (inv_image less_than (%i. ((j+N)-i) mod N))  Int
                    (lessThan N Times lessThan N)"

  next      :: nat => nat
    "next i == (Suc i) mod N"

  WellTyped :: state set
    "WellTyped == {s. ALL i j. s (Suc i) ~= Pnum j}"

  Token :: state => nat
    "Token s == case s 0 of 
                    Hungry => 0
                  | Eating => 0
                  | Thinking => 0
                  | Pnum i => i"

  HasTok :: nat => state set
    "HasTok i == Token -`` {i}"

  H :: nat => state set
    "H i == {s. s (Suc i) = Hungry}"

  E :: nat => state set
    "E i == {s. s (Suc i) = Eating}"

  T :: nat => state set
    "T i == {s. s (Suc i) = Thinking}"

rules
  N_positive "0<N"

  stable_WT  "stable Acts WellTyped"

  skip "id: Acts"

  TR2  "constrains Acts (T i) (T i Un H i)"

  TR3  "constrains Acts (H i) (H i Un E i)"

  TR4  "constrains Acts (H i - HasTok i) (H i)"

  TR5  "constrains Acts (HasTok i) (HasTok i Un Compl(E i))"

  TR6  "leadsTo Acts (H i Int HasTok i) (E i)"

  TR7  "leadsTo Acts (HasTok i) (HasTok (next i))"

end