# HG changeset patch
# User paulson
# Date 961749191 -7200
# Node ID 0085c32a533b815dbd8a9b0ac7f22c613b3f9f99
# Parent  9fff97d298374ddb92a68130cfd4e58316c21c19
sum_below f n  ->  setsum f (lessThan n)

diff -r 9fff97d29837 -r 0085c32a533b src/HOL/UNITY/Alloc.ML
--- 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";
diff -r 9fff97d29837 -r 0085c32a533b src/HOL/UNITY/Alloc.thy
--- 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
diff -r 9fff97d29837 -r 0085c32a533b src/HOL/UNITY/AllocBase.ML
--- 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);
diff -r 9fff97d29837 -r 0085c32a533b src/HOL/UNITY/AllocBase.thy
--- 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(]))"