--- a/src/HOL/UNITY/Client.thy Fri Jul 21 17:46:43 2000 +0200
+++ b/src/HOL/UNITY/Client.thy Fri Jul 21 18:01:36 2000 +0200
@@ -17,9 +17,9 @@
rel :: tokbag list (*output history: tokens released*)
tok :: tokbag (*current token request*)
-record 'a state_u =
+record 'a state_d =
state +
- extra :: 'a (*new variables*)
+ dummy :: 'a (*new variables*)
(*Array indexing is translated to list indexing as A[n] == A!(n-1). *)
@@ -28,7 +28,7 @@
(** Release some tokens **)
- rel_act :: "('a state_u * 'a state_u) set"
+ rel_act :: "('a state_d * 'a state_d) set"
"rel_act == {(s,s').
EX nrel. nrel = size (rel s) &
s' = s (| rel := rel s @ [giv s!nrel] |) &
@@ -40,24 +40,24 @@
(** Including s'=s suppresses fairness, allowing the non-trivial part
of the action to be ignored **)
- tok_act :: "('a state_u * 'a state_u) set"
+ tok_act :: "('a state_d * 'a state_d) set"
"tok_act == {(s,s'). s'=s | s' = s (|tok := Suc (tok s mod NbT) |)}"
- ask_act :: "('a state_u * 'a state_u) set"
+ ask_act :: "('a state_d * 'a state_d) set"
"ask_act == {(s,s'). s'=s |
(s' = s (|ask := ask s @ [tok s]|))}"
- Client :: 'a state_u program
+ Client :: 'a state_d program
"Client == mk_program ({s. tok s : atMost NbT &
giv s = [] & ask s = [] & rel s = []},
{rel_act, tok_act, ask_act})"
(*Maybe want a special theory section to declare such maps*)
- non_extra :: 'a state_u => state
- "non_extra s == (|giv = giv s, ask = ask s, rel = rel s, tok = tok s|)"
+ non_dummy :: 'a state_d => state
+ "non_dummy s == (|giv = giv s, ask = ask s, rel = rel s, tok = tok s|)"
(*Renaming map to put a Client into the standard form*)
- client_map :: "'a state_u => state*'a"
- "client_map == funPair non_extra extra"
+ client_map :: "'a state_d => state*'a"
+ "client_map == funPair non_dummy dummy"
end