# HG changeset patch
# User paulson
# Date 959078066 -7200
# Node ID cb419b8498e5477251d596d1f0b2126772b52058
# Parent  4829556a56f898dfcc0f3d4daf84c003949a75b8
removal of lessThan; use of AllocBase

diff -r 4829556a56f8 -r cb419b8498e5 src/HOL/UNITY/Alloc.ML
--- a/src/HOL/UNITY/Alloc.ML	Tue May 23 12:32:24 2000 +0200
+++ b/src/HOL/UNITY/Alloc.ML	Tue May 23 12:34:26 2000 +0200
@@ -40,23 +40,6 @@
      handle THM _ => th;
 
 
-Goal "(ALL i: lessThan n. f i <= g i) --> sum f n <= sum g n";
-by (induct_tac "n" 1);
-by Auto_tac;
-by (dres_inst_tac [("x","n")] bspec 1);
-by Auto_tac;
-by (arith_tac 1);
-qed_spec_mp "sum_mono";
-
-Goal "ALL xs. xs <= ys --> tokens xs <= tokens ys";
-by (induct_tac "ys" 1);
-by (auto_tac (claset(), simpset() addsimps [prefix_Cons]));
-qed_spec_mp "tokens_mono_prefix";
-
-Goalw [mono_def] "mono tokens";
-by (blast_tac (claset() addIs [tokens_mono_prefix]) 1);
-qed "mono_tokens";
-
 
 (*** bijectivity of sysOfAlloc [MUST BE AUTOMATED] ***)
 
@@ -274,20 +257,20 @@
 
 Goal "Network Join \
 \     ((rename sysOfClient \
-\       (plam x: lessThan Nclients. rename client_map Client)) Join \
+\       (plam x: {x. x<Nclients}. rename client_map Client)) Join \
 \      rename sysOfAlloc Alloc) \
 \     = System";
 by (simp_tac (simpset() addsimps System_def::Join_ac) 1);
 qed "Network_component_System";
 
 Goal "(rename sysOfClient \
-\      (plam x: lessThan Nclients. rename client_map Client)) Join \
+\      (plam x: {x. x<Nclients}. rename client_map Client)) Join \
 \     (Network Join rename sysOfAlloc Alloc)  =  System";
 by (simp_tac (simpset() addsimps System_def::Join_ac) 1);
 qed "Client_component_System";
 
 Goal "rename sysOfAlloc Alloc Join \
-\      ((rename sysOfClient (plam x: lessThan Nclients. rename client_map Client)) Join \
+\      ((rename sysOfClient (plam x: {x. x<Nclients}. rename client_map Client)) Join \
 \       Network)  =  System";
 by (simp_tac (simpset() addsimps System_def::Join_ac) 1);
 qed "Alloc_component_System";
@@ -399,19 +382,19 @@
      simpset()));
 qed "System_Follows_allocGiv";
 
-Goal "System : Always (INT i: lessThan Nclients. \
+Goal "System : Always (INT i: {x. x<Nclients}. \
 \                      {s. (giv o sub i o client) s <= (sub i o allocGiv) s})";
 by Auto_tac;
 by (etac (System_Follows_allocGiv RS Follows_Bounded) 1);
 qed "Always_giv_le_allocGiv";
 
-Goal "System : Always (INT i: lessThan Nclients. \
+Goal "System : Always (INT i: {x. x<Nclients}. \
 \                      {s. (sub i o allocAsk) s <= (ask o sub i o client) s})";
 by Auto_tac;
 by (etac (System_Follows_ask RS Follows_Bounded) 1);
 qed "Always_allocAsk_le_ask";
 
-Goal "System : Always (INT i: lessThan Nclients. \
+Goal "System : Always (INT i: {x. x<Nclients}. \
 \                      {s. (sub i o allocRel) s <= (rel o sub i o client) s})";
 by (auto_tac (claset() addSIs [Follows_Bounded, System_Follows_rel], 
 	      simpset()));
@@ -433,8 +416,9 @@
      |> simplify (simpset() addsimps [o_def]);
 
 (*safety (1), step 3*)
-Goal "System : Always {s. sum (%i. (tokens o sub i o allocGiv) s) Nclients \
-\                  <= NbT + sum (%i. (tokens o sub i o allocRel) s) Nclients}";
+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}";
 by (simp_tac (simpset() addsimps [o_apply]) 1);
 by (rtac (rename_Alloc_Safety RS component_guaranteesD) 1);
 by (auto_tac (claset(), 
@@ -444,7 +428,7 @@
 
 (** Follows reasoning **)
 
-Goal "System : Always (INT i: lessThan Nclients. \
+Goal "System : Always (INT i: {x. x<Nclients}. \
 \                         {s. (tokens o giv o sub i o client) s \
 \                          <= (tokens o sub i o allocGiv) s})";
 by (rtac (Always_giv_le_allocGiv RS Always_weaken) 1);
@@ -452,7 +436,7 @@
 	      simpset() addsimps [o_apply]));
 qed "Always_tokens_giv_le_allocGiv";
 
-Goal "System : Always (INT i: lessThan Nclients. \
+Goal "System : Always (INT i: {x. x<Nclients}. \
 \                         {s. (tokens o sub i o allocRel) s \
 \                          <= (tokens o rel o sub i o client) s})";
 by (rtac (Always_allocRel_le_rel RS Always_weaken) 1);
@@ -504,11 +488,15 @@
 by Auto_tac;
 qed "System_Bounded_ask";
 
+Goal "{x. ALL y. P y --> Q x y} = (INT y: {y. P y}. {x. Q x y})";
+by (Blast_tac 1);
+qed "Collect_all_imp_eq";
+
 (*progress (2), step 4*)
-Goal "System : Always {s. ALL i : lessThan Nclients. \
-\                          ALL elt : set ((sub i o allocAsk) s). elt <= NbT}";
+Goal "System : Always {s. ALL i. i<Nclients --> \
+\                         (ALL elt : set ((sub i o allocAsk) s). elt <= NbT)}";
 by (auto_tac (claset(), 
-	      simpset() addsimps [Collect_ball_eq]));
+	      simpset() addsimps [Collect_all_imp_eq]));
 by (rtac (Always_Int_rule [Always_allocAsk_le_ask, System_Bounded_ask] 
     RS Always_weaken) 1);
 by (auto_tac (claset() addDs [set_mono], simpset()));
@@ -537,7 +525,7 @@
 
 (*progress (2), step 7*)
 Goal
- "System : (INT i : lessThan Nclients. \
+ "System : (INT i : {x. x<Nclients}. \
 \           INT h. {s. h <= (giv o sub i o client) s & \
 \                      h pfixGe (ask o sub i o client) s}  \
 \               LeadsTo {s. tokens h <= (tokens o rel o sub i o client) s})";
@@ -600,7 +588,7 @@
 
 (*progress (2), step 9*)
 Goal
- "System : (INT i : lessThan Nclients. \
+ "System : (INT i : {x. x<Nclients}. \
 \           INT h. {s. h <= (sub i o allocAsk) s}  \
 \                  LeadsTo {s. h pfixLe (sub i o allocGiv) s})";
 (*Can't use simpset(): the "INT h" must be kept*)
diff -r 4829556a56f8 -r cb419b8498e5 src/HOL/UNITY/Alloc.thy
--- a/src/HOL/UNITY/Alloc.thy	Tue May 23 12:32:24 2000 +0200
+++ b/src/HOL/UNITY/Alloc.thy	Tue May 23 12:34:26 2000 +0200
@@ -4,33 +4,9 @@
     Copyright   1998  University of Cambridge
 
 Specification of Chandy and Charpentier's Allocator
-
-CONSIDER CHANGING "sum" to work on type "int", not "nat"
-  --then can use subtraction in spec (1),
-  --but need invariants that values are non-negative
 *)
 
-Alloc = Follows + PPROD +
-
-(*Duplicated from HOL/ex/NatSum.thy.
-  Maybe type should be  [nat=>int, nat] => int**)
-consts sum     :: [nat=>nat, nat] => nat
-primrec 
-  "sum f 0 = 0"
-  "sum f (Suc n) = f(n) + sum f n"
-
-
-(*This function merely sums the elements of a list*)
-consts tokens     :: nat list => nat
-primrec 
-  "tokens [] = 0"
-  "tokens (x#xs) = x + tokens xs"
-
-
-consts
-  NbT      :: nat       (*Number of tokens in system*)
-  Nclients :: nat       (*Number of clients*)
-
+Alloc = AllocBase + PPROD +
 
 (** State definitions.  OUTPUT variables are locals **)
 
@@ -76,12 +52,12 @@
   (*spec (1)*)
   system_safety :: 'a systemState program set
     "system_safety ==
-     Always {s. sum (%i. (tokens o giv o sub i o client) s) Nclients
-	        <= NbT + sum (%i. (tokens o rel o sub i o client) s) Nclients}"
+     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}"
 
   (*spec (2)*)
   system_progress :: 'a systemState program set
-    "system_progress == INT i : lessThan Nclients.
+    "system_progress == INT i : {x. x<Nclients}.
 			INT h. 
 			  {s. h <= (ask o sub i o client)s} LeadsTo
 			  {s. h pfixLe (giv o sub i o client) s}"
@@ -126,31 +102,31 @@
     "alloc_increasing ==
 	 UNIV
          guarantees[allocGiv]
-	 (INT i : lessThan Nclients. Increasing (sub i o allocGiv))"
+	 (INT i : {x. x<Nclients}. Increasing (sub i o allocGiv))"
 
   (*spec (7)*)
   alloc_safety :: 'a allocState_u program set
     "alloc_safety ==
-	 (INT i : lessThan Nclients. Increasing (sub i o allocRel))
+	 (INT i : {x. x<Nclients}. Increasing (sub i o allocRel))
          guarantees[allocGiv]
-	 Always {s. sum (%i. (tokens o sub i o allocGiv) s) Nclients
-	         <= NbT + sum (%i. (tokens o sub i o allocRel) s) Nclients}"
+	 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}"
 
   (*spec (8)*)
   alloc_progress :: 'a allocState_u program set
     "alloc_progress ==
-	 (INT i : lessThan Nclients. Increasing (sub i o allocAsk) Int
+	 (INT i : {x. x<Nclients}. Increasing (sub i o allocAsk) Int
 	                             Increasing (sub i o allocRel))
          Int
-         Always {s. ALL i : lessThan Nclients.
-		     ALL elt : set ((sub i o allocAsk) s). elt <= NbT}
+         Always {s. ALL i. i<Nclients -->
+		     (ALL elt : set ((sub i o allocAsk) s). elt <= NbT)}
          Int
-         (INT i : lessThan Nclients. 
+         (INT i : {x. x<Nclients}. 
 	  INT h. {s. h <= (sub i o allocGiv)s & h pfixGe (sub i o allocAsk)s}
 		 LeadsTo
 	         {s. tokens h <= (tokens o sub i o allocRel)s})
          guarantees[allocGiv]
-	     (INT i : lessThan Nclients.
+	     (INT i : {x. x<Nclients}.
 	      INT h. {s. h <= (sub i o allocAsk) s}
 	             LeadsTo
 	             {s. h pfixLe (sub i o allocGiv) s})"
@@ -168,21 +144,21 @@
 
   (*spec (9.1)*)
   network_ask :: 'a systemState program set
-    "network_ask == INT i : lessThan Nclients.
+    "network_ask == INT i : {x. x<Nclients}.
 			Increasing (ask o sub i o client)
 			guarantees[allocAsk]
 			((sub i o allocAsk) Fols (ask o sub i o client))"
 
   (*spec (9.2)*)
   network_giv :: 'a systemState program set
-    "network_giv == INT i : lessThan Nclients.
+    "network_giv == INT i : {x. x<Nclients}.
 			Increasing (sub i o allocGiv)
 			guarantees[giv o sub i o client]
 			((giv o sub i o client) Fols (sub i o allocGiv))"
 
   (*spec (9.3)*)
   network_rel :: 'a systemState program set
-    "network_rel == INT i : lessThan Nclients.
+    "network_rel == INT i : {x. x<Nclients}.
 			Increasing (rel o sub i o client)
 			guarantees[allocRel]
 			((sub i o allocRel) Fols (rel o sub i o client))"
@@ -190,7 +166,7 @@
   (*spec: preserves part*)
     network_preserves :: 'a systemState program set
     "network_preserves == preserves allocGiv  Int
-                          (INT i : lessThan Nclients.
+                          (INT i : {x. x<Nclients}.
                            preserves (funPair rel ask o sub i o client))"
   
   network_spec :: 'a systemState program set
@@ -230,7 +206,7 @@
     System_def
       "System == rename sysOfAlloc Alloc Join Network Join
                  (rename sysOfClient
-		  (plam x: lessThan Nclients. rename client_map Client))"
+		  (plam x: {x. x<Nclients}. rename client_map Client))"
 
 
 (**
@@ -253,7 +229,7 @@
                  Network
                  Join
                  (rename sysOfClient
-		  (plam x: lessThan Nclients. rename client_map Client))"
+		  (plam x: {x. x<Nclients}. rename client_map Client))"
 **)