--- a/src/HOL/UNITY/Alloc.ML Thu Jun 22 23:04:34 2000 +0200
+++ b/src/HOL/UNITY/Alloc.ML Fri Jun 23 10:33:11 2000 +0200
@@ -420,8 +420,10 @@
(*safety (1), step 3*)
Goal
- "System : Always {s. sum_below (%i. (tokens o sub i o allocGiv) s) Nclients \
-\ <= NbT + sum_below (%i. (tokens o sub i o allocRel) s) Nclients}";
+ "System : Always {s. setsum (%i. (tokens o sub i o allocGiv) s) \
+\ (lessThan Nclients) \
+\ <= NbT + setsum (%i. (tokens o sub i o allocRel) s) \
+\ (lessThan Nclients)}";
by (simp_tac (simpset() addsimps [o_apply]) 1);
by (rtac (rename_Alloc_Safety RS component_guaranteesD) 1);
by (auto_tac (claset(),
@@ -452,9 +454,9 @@
by (rtac (Always_Int_rule [System_sum_bounded, Always_tokens_giv_le_allocGiv,
Always_tokens_allocRel_le_rel] RS Always_weaken) 1);
by Auto_tac;
-by (rtac (sum_mono RS order_trans) 1);
+by (rtac (setsum_fun_mono RS order_trans) 1);
by (dtac order_trans 2);
-by (rtac ([order_refl, sum_mono] MRS add_le_mono) 2);
+by (rtac ([order_refl, setsum_fun_mono] MRS add_le_mono) 2);
by (assume_tac 3);
by Auto_tac;
qed "System_safety";
--- a/src/HOL/UNITY/Alloc.thy Thu Jun 22 23:04:34 2000 +0200
+++ b/src/HOL/UNITY/Alloc.thy Fri Jun 23 10:33:11 2000 +0200
@@ -52,8 +52,8 @@
(*spec (1)*)
system_safety :: 'a systemState program set
"system_safety ==
- Always {s. sum_below (%i. (tokens o giv o sub i o client) s) Nclients
- <= NbT + sum_below (%i. (tokens o rel o sub i o client) s) Nclients}"
+ Always {s. setsum(%i.(tokens o giv o sub i o client)s) (lessThan Nclients)
+ <= NbT + setsum(%i.(tokens o rel o sub i o client)s) (lessThan Nclients)}"
(*spec (2)*)
system_progress :: 'a systemState program set
@@ -109,8 +109,8 @@
"alloc_safety ==
(INT i : lessThan Nclients. Increasing (sub i o allocRel))
guarantees[allocGiv]
- Always {s. sum_below (%i. (tokens o sub i o allocGiv) s) Nclients
- <= NbT + sum_below (%i. (tokens o sub i o allocRel) s) Nclients}"
+ Always {s. setsum(%i.(tokens o sub i o allocGiv)s) (lessThan Nclients)
+ <= NbT + setsum(%i.(tokens o sub i o allocRel)s) (lessThan Nclients)}"
(*spec (8)*)
alloc_progress :: 'a allocState_u program set
@@ -131,6 +131,13 @@
LeadsTo
{s. h pfixLe (sub i o allocGiv) s})"
+ (*NOTE: to follow the original paper, the formula above should have had
+ INT h. {s. h i <= (sub i o allocGiv)s & h i pfixGe (sub i o allocAsk)s}
+ LeadsTo
+ {s. tokens h i <= (tokens o sub i o allocRel)s})
+ thus h should have been a function variable. However, only h i is ever
+ looked at.*)
+
(*spec: preserves part*)
alloc_preserves :: 'a allocState_u program set
"alloc_preserves == preserves (funPair allocRel
--- a/src/HOL/UNITY/AllocBase.ML Thu Jun 22 23:04:34 2000 +0200
+++ b/src/HOL/UNITY/AllocBase.ML Fri Jun 23 10:33:11 2000 +0200
@@ -9,13 +9,14 @@
time_use_thy "AllocBase";
*)
-Goal "(ALL i. i<n --> f i <= (g i :: nat)) --> sum_below f n <= sum_below g n";
+Goal "!!f :: nat=>nat. \
+\ (ALL i. i<n --> f i <= g i) --> \
+\ setsum f (lessThan n) <= setsum g (lessThan n)";
by (induct_tac "n" 1);
-by Auto_tac;
+by (auto_tac (claset(), simpset() addsimps [lessThan_Suc]));
by (dres_inst_tac [("x","n")] spec 1);
-by Auto_tac;
by (arith_tac 1);
-qed_spec_mp "sum_mono";
+qed_spec_mp "setsum_fun_mono";
Goal "ALL xs. xs <= ys --> tokens xs <= tokens ys";
by (induct_tac "ys" 1);
--- a/src/HOL/UNITY/AllocBase.thy Thu Jun 22 23:04:34 2000 +0200
+++ b/src/HOL/UNITY/AllocBase.thy Fri Jun 23 10:33:11 2000 +0200
@@ -24,12 +24,6 @@
"tokens [] = 0"
"tokens (x#xs) = x + tokens xs"
-(*Or could be setsum...(lessThan n)*)
-consts sum_below :: "[nat=>'a, nat] => ('a::plus_ac0)"
-primrec
- sum_below_0 "sum_below f 0 = 0"
- sum_below_Suc "sum_below f (Suc n) = f(n) + sum_below f n"
-
constdefs sublist :: "['a list, nat set] => 'a list"
"sublist l A == map fst (filter (%p. snd p : A) (zip l [0..size l(]))"