src/HOL/UNITY/Token.thy
changeset 5420 b48ab3281944
parent 5277 e4297d03e5d2
child 5608 a82a038a3e7a
     1.1 --- a/src/HOL/UNITY/Token.thy	Tue Sep 01 15:05:59 1998 +0200
     1.2 +++ b/src/HOL/UNITY/Token.thy	Tue Sep 01 15:07:11 1998 +0200
     1.3 @@ -18,17 +18,8 @@
     1.4    token :: nat
     1.5    proc  :: nat => pstate
     1.6  
     1.7 -consts
     1.8 -  N :: nat	(*number of nodes in the ring*)
     1.9  
    1.10  constdefs
    1.11 -  nodeOrder :: "nat => (nat*nat)set"
    1.12 -    "nodeOrder j == (inv_image less_than (%i. ((j+N)-i) mod N))  Int
    1.13 -                    (lessThan N Times lessThan N)"
    1.14 -
    1.15 -  next      :: nat => nat
    1.16 -    "next i == (Suc i) mod N"
    1.17 -
    1.18    HasTok :: nat => state set
    1.19      "HasTok i == {s. token s = i}"
    1.20  
    1.21 @@ -41,21 +32,37 @@
    1.22    T :: nat => state set
    1.23      "T i == {s. proc s i = Thinking}"
    1.24  
    1.25 -rules
    1.26 -  N_positive "0<N"
    1.27  
    1.28 -  skip "id: acts"
    1.29 +locale Token =
    1.30 +  fixes
    1.31 +    N         :: nat	 (*number of nodes in the ring*)
    1.32 +    acts      :: "(state*state)set set"
    1.33 +    nodeOrder :: "nat => (nat*nat)set"
    1.34 +    next      :: nat => nat
    1.35  
    1.36 -  TR2  "constrains acts (T i) (T i Un H i)"
    1.37 +  assumes
    1.38 +    N_positive "0<N"
    1.39 +
    1.40 +    skip "id: acts"
    1.41 +
    1.42 +    TR2  "!!i. constrains acts (T i) (T i Un H i)"
    1.43  
    1.44 -  TR3  "constrains acts (H i) (H i Un E i)"
    1.45 +    TR3  "!!i. constrains acts (H i) (H i Un E i)"
    1.46 +
    1.47 +    TR4  "!!i. constrains acts (H i - HasTok i) (H i)"
    1.48  
    1.49 -  TR4  "constrains acts (H i - HasTok i) (H i)"
    1.50 +    TR5  "!!i. constrains acts (HasTok i) (HasTok i Un Compl(E i))"
    1.51 +
    1.52 +    TR6  "!!i. leadsTo acts (H i Int HasTok i) (E i)"
    1.53  
    1.54 -  TR5  "constrains acts (HasTok i) (HasTok i Un Compl(E i))"
    1.55 +    TR7  "!!i. leadsTo acts (HasTok i) (HasTok (next i))"
    1.56  
    1.57 -  TR6  "leadsTo acts (H i Int HasTok i) (E i)"
    1.58 +  defines
    1.59 +    nodeOrder_def
    1.60 +      "nodeOrder j == (inv_image less_than (%i. ((j+N)-i) mod N))  Int
    1.61 +		      (lessThan N Times lessThan N)"
    1.62  
    1.63 -  TR7  "leadsTo acts (HasTok i) (HasTok (next i))"
    1.64 +    next_def
    1.65 +      "next i == (Suc i) mod N"
    1.66  
    1.67  end