--- a/src/HOL/UNITY/Alloc.thy Fri Jul 21 17:46:43 2000 +0200
+++ b/src/HOL/UNITY/Alloc.thy Fri Jul 21 18:01:36 2000 +0200
@@ -15,19 +15,19 @@
ask :: nat list (*client's OUTPUT history: tokens REQUESTED*)
rel :: nat list (*client's OUTPUT history: tokens RELEASED*)
-record 'a clientState_u =
+record 'a clientState_d =
clientState +
- extra :: 'a (*dummy field for new variables*)
+ dummy :: 'a (*dummy field for new variables*)
constdefs
(*DUPLICATED FROM Client.thy, but with "tok" removed*)
(*Maybe want a special theory section to declare such maps*)
- non_extra :: 'a clientState_u => clientState
- "non_extra s == (|giv = giv s, ask = ask s, rel = rel s|)"
+ non_dummy :: 'a clientState_d => clientState
+ "non_dummy s == (|giv = giv s, ask = ask s, rel = rel s|)"
(*Renaming map to put a Client into the standard form*)
- client_map :: "'a clientState_u => clientState*'a"
- "client_map == funPair non_extra extra"
+ client_map :: "'a clientState_d => clientState*'a"
+ "client_map == funPair non_dummy dummy"
record allocState =
@@ -35,14 +35,14 @@
allocAsk :: nat => nat list (*INPUT: allocator's copy of "ask" for i*)
allocRel :: nat => nat list (*INPUT: allocator's copy of "rel" for i*)
-record 'a allocState_u =
+record 'a allocState_d =
allocState +
- extra :: 'a (*dummy field for new variables*)
+ dummy :: 'a (*dummy field for new variables*)
record 'a systemState =
allocState +
client :: nat => clientState (*states of all clients*)
- extra :: 'a (*dummy field for new variables*)
+ dummy :: 'a (*dummy field for new variables*)
constdefs
@@ -68,19 +68,19 @@
(** Client specification (required) ***)
(*spec (3)*)
- client_increasing :: 'a clientState_u program set
+ client_increasing :: 'a clientState_d program set
"client_increasing ==
UNIV guarantees[funPair rel ask]
Increasing ask Int Increasing rel"
(*spec (4)*)
- client_bounded :: 'a clientState_u program set
+ client_bounded :: 'a clientState_d program set
"client_bounded ==
UNIV guarantees[ask]
Always {s. ALL elt : set (ask s). elt <= NbT}"
(*spec (5)*)
- client_progress :: 'a clientState_u program set
+ client_progress :: 'a clientState_d program set
"client_progress ==
Increasing giv
guarantees[funPair rel ask]
@@ -88,24 +88,24 @@
LeadsTo {s. tokens h <= (tokens o rel) s})"
(*spec: preserves part*)
- client_preserves :: 'a clientState_u program set
- "client_preserves == preserves (funPair giv clientState_u.extra)"
+ client_preserves :: 'a clientState_d program set
+ "client_preserves == preserves (funPair giv clientState_d.dummy)"
- client_spec :: 'a clientState_u program set
+ client_spec :: 'a clientState_d program set
"client_spec == client_increasing Int client_bounded Int client_progress
Int client_preserves"
(** Allocator specification (required) ***)
(*spec (6)*)
- alloc_increasing :: 'a allocState_u program set
+ alloc_increasing :: 'a allocState_d program set
"alloc_increasing ==
UNIV
guarantees[allocGiv]
(INT i : lessThan Nclients. Increasing (sub i o allocGiv))"
(*spec (7)*)
- alloc_safety :: 'a allocState_u program set
+ alloc_safety :: 'a allocState_d program set
"alloc_safety ==
(INT i : lessThan Nclients. Increasing (sub i o allocRel))
guarantees[allocGiv]
@@ -113,13 +113,13 @@
<= NbT + setsum(%i.(tokens o sub i o allocRel)s) (lessThan Nclients)}"
(*spec (8)*)
- alloc_progress :: 'a allocState_u program set
+ alloc_progress :: 'a allocState_d program set
"alloc_progress ==
(INT i : lessThan Nclients. Increasing (sub i o allocAsk) Int
Increasing (sub i o allocRel))
Int
- Always {s. ALL i. i<Nclients -->
- (ALL elt : set ((sub i o allocAsk) s). elt <= NbT)}
+ Always {s. ALL i<Nclients.
+ ALL elt : set ((sub i o allocAsk) s). elt <= NbT}
Int
(INT i : lessThan Nclients.
INT h. {s. h <= (sub i o allocGiv)s & h pfixGe (sub i o allocAsk)s}
@@ -139,11 +139,11 @@
looked at.*)
(*spec: preserves part*)
- alloc_preserves :: 'a allocState_u program set
+ alloc_preserves :: 'a allocState_d program set
"alloc_preserves == preserves (funPair allocRel
- (funPair allocAsk allocState_u.extra))"
+ (funPair allocAsk allocState_d.dummy))"
- alloc_spec :: 'a allocState_u program set
+ alloc_spec :: 'a allocState_d program set
"alloc_spec == alloc_increasing Int alloc_safety Int alloc_progress Int
alloc_preserves"
@@ -182,25 +182,25 @@
(** State mappings **)
- sysOfAlloc :: "((nat => clientState) * 'a) allocState_u => 'a systemState"
- "sysOfAlloc == %s. let (cl,xtr) = allocState_u.extra s
+ sysOfAlloc :: "((nat => clientState) * 'a) allocState_d => 'a systemState"
+ "sysOfAlloc == %s. let (cl,xtr) = allocState_d.dummy s
in (| allocGiv = allocGiv s,
allocAsk = allocAsk s,
allocRel = allocRel s,
client = cl,
- extra = xtr|)"
+ dummy = xtr|)"
- sysOfClient :: "(nat => clientState) * 'a allocState_u => 'a systemState"
+ sysOfClient :: "(nat => clientState) * 'a allocState_d => 'a systemState"
"sysOfClient == %(cl,al). (| allocGiv = allocGiv al,
allocAsk = allocAsk al,
allocRel = allocRel al,
client = cl,
- systemState.extra = allocState_u.extra al|)"
+ systemState.dummy = allocState_d.dummy al|)"
consts
- Alloc :: 'a allocState_u program
- Client :: 'a clientState_u program
+ Alloc :: 'a allocState_d program
+ Client :: 'a clientState_d program
Network :: 'a systemState program
System :: 'a systemState program
@@ -219,8 +219,8 @@
(**
locale System =
fixes
- Alloc :: 'a allocState_u program
- Client :: 'a clientState_u program
+ Alloc :: 'a allocState_d program
+ Client :: 'a clientState_d program
Network :: 'a systemState program
System :: 'a systemState program