--- a/src/HOL/TLA/Buffer/Buffer.thy Mon Feb 08 13:02:42 1999 +0100
+++ b/src/HOL/TLA/Buffer/Buffer.thy Mon Feb 08 13:02:56 1999 +0100
@@ -9,16 +9,11 @@
A simple FIFO buffer (synchronous communication, interleaving)
*)
-Buffer = TLA + List +
+Buffer = TLA +
consts
- (* infix syntax for list operations *)
- "IntNil" :: 'w::world => 'a list (".[]")
- "IntCons" :: ['w::world => 'a, 'w => 'a list] => ('w => 'a list) ("(_ .#/ _)" [65,66] 65)
- "IntApp" :: ['w::world => 'a list, 'w => 'a list] => ('w => 'a list) ("(_ .@/ _)" [65,66] 65)
-
(* actions *)
- BInit :: "'a stfun => 'a list stfun => 'a stfun => action"
+ BInit :: "'a stfun => 'a list stfun => 'a stfun => stpred"
Enq :: "'a stfun => 'a list stfun => 'a stfun => action"
Deq :: "'a stfun => 'a list stfun => 'a stfun => action"
Next :: "'a stfun => 'a list stfun => 'a stfun => action"
@@ -27,30 +22,20 @@
IBuffer :: "'a stfun => 'a list stfun => 'a stfun => temporal"
Buffer :: "'a stfun => 'a stfun => temporal"
-syntax
- "@listInt" :: args => ('a list, 'w) term (".[(_)]")
-
-translations
- ".[]" == "con []"
- "x .# xs" == "lift2 (op #) x xs"
- "xs .@ ys" == "lift2 (op @) xs ys"
- ".[ x, xs ]" == "x .# .[xs]"
- ".[ x ]" == "x .# .[]"
-
rules
- BInit_def "BInit ic q oc == $q .= .[]"
- Enq_def "Enq ic q oc == (ic$ .~= $ic)
- .& (q$ .= $q .@ .[ ic$ ])
- .& (oc$ .= $oc)"
- Deq_def "Deq ic q oc == ($q .~= .[])
- .& (oc$ .= hd[ $q ])
- .& (q$ .= tl[ $q ])
- .& (ic$ .= $ic)"
- Next_def "Next ic q oc == Enq ic q oc .| Deq ic q oc"
- IBuffer_def "IBuffer ic q oc == Init (BInit ic q oc)
- .& [][Next ic q oc]_<ic,q,oc>
- .& WF(Deq ic q oc)_<ic,q,oc>"
- Buffer_def "Buffer ic oc == EEX q. IBuffer ic q oc"
+ BInit_def "BInit ic q oc == PRED q = #[]"
+ Enq_def "Enq ic q oc == ACT (ic$ ~= $ic)
+ & (q$ = $q @ [ ic$ ])
+ & (oc$ = $oc)"
+ Deq_def "Deq ic q oc == ACT ($q ~= #[])
+ & (oc$ = hd< $q >)
+ & (q$ = tl< $q >)
+ & (ic$ = $ic)"
+ Next_def "Next ic q oc == ACT (Enq ic q oc | Deq ic q oc)"
+ IBuffer_def "IBuffer ic q oc == TEMP Init (BInit ic q oc)
+ & [][Next ic q oc]_(ic,q,oc)
+ & WF(Deq ic q oc)_(ic,q,oc)"
+ Buffer_def "Buffer ic oc == TEMP (EEX q. IBuffer ic q oc)"
end