sum_below f n -> setsum f (lessThan n)
authorpaulson
Fri Jun 23 10:33:11 2000 +0200 (2000-06-23)
changeset 91090085c32a533b
parent 9108 9fff97d29837
child 9110 40d759b9725f
sum_below f n -> setsum f (lessThan n)
src/HOL/UNITY/Alloc.ML
src/HOL/UNITY/Alloc.thy
src/HOL/UNITY/AllocBase.ML
src/HOL/UNITY/AllocBase.thy
     1.1 --- a/src/HOL/UNITY/Alloc.ML	Thu Jun 22 23:04:34 2000 +0200
     1.2 +++ b/src/HOL/UNITY/Alloc.ML	Fri Jun 23 10:33:11 2000 +0200
     1.3 @@ -420,8 +420,10 @@
     1.4  
     1.5  (*safety (1), step 3*)
     1.6  Goal
     1.7 -  "System : Always {s. sum_below (%i. (tokens o sub i o allocGiv) s) Nclients \
     1.8 -\           <= NbT + sum_below (%i. (tokens o sub i o allocRel) s) Nclients}";
     1.9 +  "System : Always {s. setsum (%i. (tokens o sub i o allocGiv) s) \
    1.10 +\                             (lessThan Nclients)                 \
    1.11 +\           <= NbT + setsum (%i. (tokens o sub i o allocRel) s)   \
    1.12 +\                           (lessThan Nclients)}";
    1.13  by (simp_tac (simpset() addsimps [o_apply]) 1);
    1.14  by (rtac (rename_Alloc_Safety RS component_guaranteesD) 1);
    1.15  by (auto_tac (claset(), 
    1.16 @@ -452,9 +454,9 @@
    1.17  by (rtac (Always_Int_rule [System_sum_bounded, Always_tokens_giv_le_allocGiv, 
    1.18  			   Always_tokens_allocRel_le_rel] RS Always_weaken) 1);
    1.19  by Auto_tac;
    1.20 -by (rtac (sum_mono RS order_trans) 1);
    1.21 +by (rtac (setsum_fun_mono RS order_trans) 1);
    1.22  by (dtac order_trans 2);
    1.23 -by (rtac ([order_refl, sum_mono] MRS add_le_mono) 2);
    1.24 +by (rtac ([order_refl, setsum_fun_mono] MRS add_le_mono) 2);
    1.25  by (assume_tac 3);
    1.26  by Auto_tac;
    1.27  qed "System_safety";
     2.1 --- a/src/HOL/UNITY/Alloc.thy	Thu Jun 22 23:04:34 2000 +0200
     2.2 +++ b/src/HOL/UNITY/Alloc.thy	Fri Jun 23 10:33:11 2000 +0200
     2.3 @@ -52,8 +52,8 @@
     2.4    (*spec (1)*)
     2.5    system_safety :: 'a systemState program set
     2.6      "system_safety ==
     2.7 -     Always {s. sum_below (%i. (tokens o giv o sub i o client) s) Nclients
     2.8 -        <= NbT + sum_below (%i. (tokens o rel o sub i o client) s) Nclients}"
     2.9 +     Always {s. setsum(%i.(tokens o giv o sub i o client)s) (lessThan Nclients)
    2.10 +     <= NbT + setsum(%i.(tokens o rel o sub i o client)s) (lessThan Nclients)}"
    2.11  
    2.12    (*spec (2)*)
    2.13    system_progress :: 'a systemState program set
    2.14 @@ -109,8 +109,8 @@
    2.15      "alloc_safety ==
    2.16  	 (INT i : lessThan Nclients. Increasing (sub i o allocRel))
    2.17           guarantees[allocGiv]
    2.18 -	 Always {s. sum_below (%i. (tokens o sub i o allocGiv) s) Nclients
    2.19 -	      <= NbT + sum_below (%i. (tokens o sub i o allocRel) s) Nclients}"
    2.20 +	 Always {s. setsum(%i.(tokens o sub i o allocGiv)s) (lessThan Nclients)
    2.21 +         <= NbT + setsum(%i.(tokens o sub i o allocRel)s) (lessThan Nclients)}"
    2.22  
    2.23    (*spec (8)*)
    2.24    alloc_progress :: 'a allocState_u program set
    2.25 @@ -131,6 +131,13 @@
    2.26  	             LeadsTo
    2.27  	             {s. h pfixLe (sub i o allocGiv) s})"
    2.28  
    2.29 +  (*NOTE: to follow the original paper, the formula above should have had
    2.30 +	INT h. {s. h i <= (sub i o allocGiv)s & h i pfixGe (sub i o allocAsk)s}
    2.31 +	       LeadsTo
    2.32 +	       {s. tokens h i <= (tokens o sub i o allocRel)s})
    2.33 +    thus h should have been a function variable.  However, only h i is ever
    2.34 +    looked at.*)
    2.35 +
    2.36    (*spec: preserves part*)
    2.37      alloc_preserves :: 'a allocState_u program set
    2.38      "alloc_preserves == preserves (funPair allocRel
     3.1 --- a/src/HOL/UNITY/AllocBase.ML	Thu Jun 22 23:04:34 2000 +0200
     3.2 +++ b/src/HOL/UNITY/AllocBase.ML	Fri Jun 23 10:33:11 2000 +0200
     3.3 @@ -9,13 +9,14 @@
     3.4  time_use_thy "AllocBase";
     3.5  *)
     3.6  
     3.7 -Goal "(ALL i. i<n --> f i <= (g i :: nat)) --> sum_below f n <= sum_below g n";
     3.8 +Goal "!!f :: nat=>nat. \
     3.9 +\     (ALL i. i<n --> f i <= g i) --> \
    3.10 +\     setsum f (lessThan n) <= setsum g (lessThan n)";
    3.11  by (induct_tac "n" 1);
    3.12 -by Auto_tac;
    3.13 +by (auto_tac (claset(), simpset() addsimps [lessThan_Suc]));
    3.14  by (dres_inst_tac [("x","n")] spec 1);
    3.15 -by Auto_tac;
    3.16  by (arith_tac 1);
    3.17 -qed_spec_mp "sum_mono";
    3.18 +qed_spec_mp "setsum_fun_mono";
    3.19  
    3.20  Goal "ALL xs. xs <= ys --> tokens xs <= tokens ys";
    3.21  by (induct_tac "ys" 1);
     4.1 --- a/src/HOL/UNITY/AllocBase.thy	Thu Jun 22 23:04:34 2000 +0200
     4.2 +++ b/src/HOL/UNITY/AllocBase.thy	Fri Jun 23 10:33:11 2000 +0200
     4.3 @@ -24,12 +24,6 @@
     4.4    "tokens [] = 0"
     4.5    "tokens (x#xs) = x + tokens xs"
     4.6  
     4.7 -(*Or could be setsum...(lessThan n)*)
     4.8 -consts sum_below :: "[nat=>'a, nat] => ('a::plus_ac0)"
     4.9 -primrec 
    4.10 -  sum_below_0    "sum_below f 0 = 0"
    4.11 -  sum_below_Suc  "sum_below f (Suc n) = f(n) + sum_below f n"
    4.12 -
    4.13  constdefs sublist :: "['a list, nat set] => 'a list"
    4.14      "sublist l A == map fst (filter (%p. snd p : A) (zip l [0..size l(]))"
    4.15