--- a/src/HOL/UNITY/Token.thy Tue Sep 01 15:05:59 1998 +0200
+++ b/src/HOL/UNITY/Token.thy Tue Sep 01 15:07:11 1998 +0200
@@ -18,17 +18,8 @@
token :: nat
proc :: 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"
-
HasTok :: nat => state set
"HasTok i == {s. token s = i}"
@@ -41,21 +32,37 @@
T :: nat => state set
"T i == {s. proc s i = Thinking}"
-rules
- N_positive "0<N"
- skip "id: acts"
+locale Token =
+ fixes
+ N :: nat (*number of nodes in the ring*)
+ acts :: "(state*state)set set"
+ nodeOrder :: "nat => (nat*nat)set"
+ next :: nat => nat
- TR2 "constrains acts (T i) (T i Un H i)"
+ assumes
+ N_positive "0<N"
+
+ skip "id: acts"
+
+ TR2 "!!i. constrains acts (T i) (T i Un H i)"
- TR3 "constrains acts (H i) (H i Un E i)"
+ TR3 "!!i. constrains acts (H i) (H i Un E i)"
+
+ TR4 "!!i. constrains acts (H i - HasTok i) (H i)"
- TR4 "constrains acts (H i - HasTok i) (H i)"
+ TR5 "!!i. constrains acts (HasTok i) (HasTok i Un Compl(E i))"
+
+ TR6 "!!i. leadsTo acts (H i Int HasTok i) (E i)"
- TR5 "constrains acts (HasTok i) (HasTok i Un Compl(E i))"
+ TR7 "!!i. leadsTo acts (HasTok i) (HasTok (next i))"
- TR6 "leadsTo acts (H i Int HasTok i) (E i)"
+ defines
+ nodeOrder_def
+ "nodeOrder j == (inv_image less_than (%i. ((j+N)-i) mod N)) Int
+ (lessThan N Times lessThan N)"
- TR7 "leadsTo acts (HasTok i) (HasTok (next i))"
+ next_def
+ "next i == (Suc i) mod N"
end