# HG changeset patch
# User paulson
# Date 945879601 -3600
# Node ID 93b62f856af7e44d4446cf636a45f6385c445fb8
# Parent  36a6c38e0eca9fd9d521cef40e3bd1640fae89ff
tidied, with a bit more progress

diff -r 36a6c38e0eca -r 93b62f856af7 src/HOL/UNITY/Alloc.ML
--- a/src/HOL/UNITY/Alloc.ML	Wed Dec 22 17:18:03 1999 +0100
+++ b/src/HOL/UNITY/Alloc.ML	Wed Dec 22 17:20:01 1999 +0100
@@ -407,9 +407,9 @@
 \               <= NbT + sum (%i. (tokens o sub i o allocRel) s) Nclients}";
 by (rtac (Alloc_Safety RS alloc_export project_guarantees) 1);
 (*2: Always postcondition*)
-by (rtac ((alloc_export extending_Always RS extending_weaken)) 2);
+by (rtac ((alloc_export extending_Always RS extending_weaken_L)) 2);
 (*1: Increasing precondition*)
-by (rtac (alloc_export projecting_Increasing RS projecting_weaken RS 
+by (rtac (alloc_export projecting_Increasing RS projecting_weaken_L RS 
 	  projecting_INT) 1);
 by (auto_tac (claset(),
 	      simpset() addsimps [alloc_export Collect_eq_extend_set RS sym,
@@ -525,12 +525,11 @@
 \                  LeadsTo[givenBy (funPair rel ask o sub i)] \
 \                  {s. tokens h <= (tokens o rel o sub i) s})";
 by (rtac (Client_Progress RS drop_prog_guarantees) 1);
-by (rtac (lift_export extending_LeadsETo RS extending_weaken RS
+by (rtac (lift_export extending_LeadsETo RS extending_weaken_L RS
 	  extending_INT) 2);
-by (rtac subset_refl 3);
-by (simp_tac (simpset() addsimps [lift_export Collect_eq_extend_set RS sym,
-				  sub_def]) 2);
-by (rtac (lift_export projecting_Increasing RS projecting_weaken) 1);
+by (asm_simp_tac (simpset() addsimps [lift_export Collect_eq_extend_set RS sym,
+				  sub_def, o_def]) 2);
+by (rtac (lift_export projecting_Increasing) 1);
 by (auto_tac (claset(), simpset() addsimps [o_def]));
 qed "Client_i_Progress";
 
@@ -554,7 +553,7 @@
 			      client_export projecting_Increasing]) 1);
 by (asm_full_simp_tac
     (simpset() addsimps [rewrite_rule [System_def] System_Increasing_giv]) 5);
-by (rtac (client_export extending_LeadsETo RS extending_weaken RS 
+by (rtac (client_export extending_LeadsETo RS extending_weaken_L RS 
 	  extending_INT) 1);
 by (auto_tac (claset(), 
 	      simpset() addsimps [o_apply, 
@@ -584,13 +583,17 @@
 val lemma3 = result();
 
 
+(*NOT GOOD ENOUGH.  Needs givenBy restriction
+     (funPair allocGiv (funPair allocAsk allocRel))
+  in LeadsTo!   But System_Client_Progress has
+     (funPair rel ask o sub i o client)*)
+  The mention of client's rel, ask must be replaced by allocRel, allocAsk
+*)
 (*progress (2), step 8*)
-Goal
- "System : (INT i : lessThan Nclients. \
-\           INT h. {s. h <= (sub i o allocGiv) s & \
+Goal "i < Nclients  \
+\     ==> System : {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})";
-by Auto_tac;
+\                  LeadsTo {s. tokens h <= (tokens o sub i o allocRel) s}";
 by (rtac LeadsTo_Trans 1);
 by (dtac (System_Follows_rel RS impOfSubs (mono_tokens RS mono_Follows_o) RS 
     Follows_LeadsTo) 2);
@@ -602,21 +605,18 @@
 by (etac lemma3 1);
 qed "System_Alloc_Progress";
 
-
-xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx;
-
 (*NEED AUTOMATIC PROPAGATION of Alloc_Progress.  The text is identical.*)
 Goal "extend sysOfAlloc Alloc :  \
 \  (INT i : lessThan Nclients. Increasing (sub i o allocAsk) Int   \
 \                              Increasing (sub i o allocRel))   \
 \  Int   \
 \  Always {s. ALL i : lessThan Nclients.   \
-\             ALL k : lessThan (length (allocAsk s i)).   \
-\             allocAsk s i ! k <= NbT}   \
+\             ALL elt : set ((sub i o allocAsk) s). elt <= NbT}   \
 \  Int   \
 \  (INT i : lessThan 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})   \
+\          LeadsTo[givenBy (funPair allocGiv (funPair allocAsk allocRel))]  \
+\          {s. tokens h <= (tokens o sub i o allocRel)s})   \
 \  guarantees[allocGiv]   \
 \      (INT i : lessThan Nclients.   \
 \       INT h. {s. h <= (sub i o allocAsk) s}    \
@@ -632,23 +632,48 @@
 by (simp_tac (simpset() addsimps [o_def]) 3);
 by (simp_tac (simpset() addsimps [alloc_export Collect_eq_extend_set RS sym,
 				  o_def]) 2);
-(*1: Increasing precondition*)
-by (rtac (alloc_export projecting_Increasing RS projecting_weaken RS 
-	  projecting_INT) 1);
+(*1: Complex precondition*)
+by (rtac (projecting_Int RS projecting_INT RS projecting_Int RS 
+	  projecting_Int) 1);
+by (rtac (alloc_export projecting_Increasing RS projecting_weaken_L) 1);
+by (asm_simp_tac (simpset() addsimps [o_def]) 1);
+by (rtac (alloc_export projecting_Increasing RS projecting_weaken_L) 1);
+by (asm_simp_tac (simpset() addsimps [o_def]) 1);
+by (rtac (alloc_export projecting_Always RS projecting_weaken_L) 1);
+by (asm_simp_tac
+    (simpset() addsimps [alloc_export Collect_eq_extend_set RS sym, o_def]) 1);
+(*LeadsTo precondition*)
+by (rtac (projecting_INT RS projecting_INT) 1);
+by (rtac (alloc_export projecting_LeadsTo RS projecting_weaken_L) 1);
 by (auto_tac (claset(),
 	      simpset() addsimps [alloc_export Collect_eq_extend_set RS sym,
 				  o_def]));
+by (auto_tac (claset() addSIs [givenByI]
+		       addEs [LeadsETo_weaken, givenByD]
+		       addSWrapper record_split_wrapper, 
+	      simpset() addsimps [funPair_def]));
 qed "extend_Alloc_Progress";
 
 
+xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx;
+
 (*progress (2), step 9*)
 Goal
  "System : (INT i : lessThan Nclients. \
 \           INT h. {s. h <= (sub i o allocAsk) s}  \
-\                  LeadsTo {s. h pfixLe (sub i o allocGiv) s})";
-by (res_inst_tac 
-    [("X", "(INT i : lessThan Nclients. Increasing (sub i o allocRel))")] 
-    component_guaranteesD 1);
+\                  LeadsTo[givenBy allocGiv] \
+\                  {s. h pfixLe (sub i o allocGiv) s})";
+by (rtac (extend_Alloc_Progress RS component_guaranteesD) 1);
+by (rtac Alloc_component_System 2);
+(*preserves*)
+by (asm_full_simp_tac (simpset() addsimps [o_def]) 2);
+(*the guarantees precondition*)
+by (auto_tac (claset(), 
+	      simpset() addsimps [System_Increasing_allocRel,
+				  System_Increasing_allocAsk]));
+br System_Bounded_allocAsk 1;
+br System_Alloc_Progress 1;
+
 by (rtac Alloc_component_System 3);
 by (force_tac (claset(), simpset() addsimps [System_Increasing_allocRel]) 2);
 by (rtac (Alloc_Safety RS alloc_export project_guarantees) 1);
diff -r 36a6c38e0eca -r 93b62f856af7 src/HOL/UNITY/Alloc.thy
--- a/src/HOL/UNITY/Alloc.thy	Wed Dec 22 17:18:03 1999 +0100
+++ b/src/HOL/UNITY/Alloc.thy	Wed Dec 22 17:20:01 1999 +0100
@@ -123,12 +123,12 @@
 	                             Increasing (sub i o allocRel))
          Int
          Always {s. ALL i : lessThan Nclients.
-		    ALL k : lessThan (length (allocAsk s i)).
-		    allocAsk s i ! k <= NbT}
+		     ALL elt : set ((sub i o allocAsk) s). elt <= NbT}
          Int
          (INT i : lessThan 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})
+		 LeadsTo
+	         {s. tokens h <= (tokens o sub i o allocRel)s})
          guarantees[allocGiv]
 	     (INT i : lessThan Nclients.
 	      INT h. {s. h <= (sub i o allocAsk) s}
@@ -148,28 +148,27 @@
   (*spec (9.1)*)
   network_ask :: systemState program set
     "network_ask == INT i : lessThan Nclients.
-                    Increasing (ask o sub i o client)
-                    guarantees[allocAsk]
-                    ((sub i o allocAsk) Fols (ask o sub i o client))"
+			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 :: systemState program set
     "network_giv == INT i : lessThan Nclients.
-                    Increasing (sub i o allocGiv)
-                    guarantees[giv o sub i o client]
-                    ((giv o sub i o client) Fols (sub i o allocGiv))"
+			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 :: systemState program set
     "network_rel == INT i : lessThan Nclients.
-                    Increasing (rel o sub i o client)
-                    guarantees[allocRel]
-                    ((sub i o allocRel) Fols (rel o sub i o client))"
+			Increasing (rel o sub i o client)
+			guarantees[allocRel]
+			((sub i o allocRel) Fols (rel o sub i o client))"
 
   (*spec: preserves part*)
     network_preserves :: systemState program set
-    "network_preserves == preserves allocGiv
-                          Int
+    "network_preserves == preserves allocGiv  Int
                           (INT i : lessThan Nclients.
                            preserves (funPair rel ask o sub i o client))"