--- a/src/ZF/UNITY/AllocImpl.thy Sun Oct 07 15:49:25 2007 +0200
+++ b/src/ZF/UNITY/AllocImpl.thy Sun Oct 07 21:19:31 2007 +0200
@@ -24,8 +24,7 @@
alloc_default_val_assumes [simp]:
"default_val(NbR) = 0 & default_val(available_tok)=0"
-constdefs
- alloc_giv_act :: i
+definition
"alloc_giv_act ==
{<s, t> \<in> state*state.
\<exists>k. k = length(s`giv) &
@@ -33,16 +32,16 @@
available_tok := s`available_tok #- nth(k, s`ask)) &
k < length(s`ask) & nth(k, s`ask) le s`available_tok}"
- alloc_rel_act :: i
+definition
"alloc_rel_act ==
{<s, t> \<in> state*state.
t = s(available_tok := s`available_tok #+ nth(s`NbR, s`rel),
NbR := succ(s`NbR)) &
s`NbR < length(s`rel)}"
+definition
(*The initial condition s`giv=[] is missing from the
original definition: S. O. Ehmety *)
- alloc_prog :: i
"alloc_prog ==
mk_program({s:state. s`available_tok=NbT & s`NbR=0 & s`giv=Nil},
{alloc_giv_act, alloc_rel_act},
@@ -659,6 +658,4 @@
apply (auto simp add: alloc_progress_def)
done
-
-
end