# HG changeset patch
# User paulson
# Date 947239455 -3600
# Node ID 7110358acdedfd151a3050728d5bfec3c894cdf2
# Parent  efbe50e2bef920824ae2c04abf62de40086c0168
tidied

diff -r efbe50e2bef9 -r 7110358acded src/HOL/UNITY/Alloc.ML
--- a/src/HOL/UNITY/Alloc.ML	Fri Jan 07 11:00:56 2000 +0100
+++ b/src/HOL/UNITY/Alloc.ML	Fri Jan 07 11:04:15 2000 +0100
@@ -407,7 +407,7 @@
 \               <= 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_L)) 2);
+by (rtac (alloc_export extending_Always RS extending_weaken_L) 2);
 (*1: Increasing precondition*)
 by (rtac (alloc_export projecting_Increasing RS projecting_weaken_L RS 
 	  projecting_INT) 1);
@@ -585,9 +585,7 @@
 
 (*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
+  in LeadsTo!   But System_Client_Progress has the wrong restriction (below)
 *)
 (*progress (2), step 8*)
 Goal "i < Nclients  \
@@ -596,16 +594,19 @@
 \                  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);
+	  Follows_LeadsTo) 2);
 by (asm_full_simp_tac (simpset() addsimps [o_assoc]) 2);
 by (rtac LeadsTo_Trans 1);
 by (rtac (impOfSubs LeadsETo_subset_LeadsTo) 2);
+(*Here we have givenBy (funPair rel ask o sub i o client)]
+  when we need givenBy (funPair allocRel allocAsk) ?? *)
 by (cut_facts_tac [System_Client_Progress] 2);
 by (Force_tac 2);
 by (etac lemma3 1);
 qed "System_Alloc_Progress";
 
-(*NEED AUTOMATIC PROPAGATION of Alloc_Progress.  The text is identical.*)
+(*NEED AUTOMATIC PROPAGATION of Alloc_Progress.  The text is identical
+  except in the LeadsTo precondition.*)
 Goal "extend sysOfAlloc Alloc :  \
 \  (INT i : lessThan Nclients. Increasing (sub i o allocAsk) Int   \
 \                              Increasing (sub i o allocRel))   \
@@ -627,7 +628,7 @@
 by (simp_tac (simpset() addsimps [o_def]) 3);
 (*2: LeadsTo postcondition*)
 by (rtac (extending_INT RS extending_INT) 2);
-by (rtac ((alloc_export extending_LeadsETo RS extending_weaken)) 2);
+by (rtac (alloc_export extending_LeadsETo RS extending_weaken) 2);
 by (rtac subset_refl 3);
 by (simp_tac (simpset() addsimps [o_def]) 3);
 by (simp_tac (simpset() addsimps [alloc_export Collect_eq_extend_set RS sym,
@@ -671,10 +672,9 @@
 by (auto_tac (claset(), 
 	      simpset() addsimps [System_Increasing_allocRel,
 				  System_Increasing_allocAsk]));
-br System_Bounded_allocAsk 1;
-br System_Alloc_Progress 1;
+by (rtac System_Bounded_allocAsk 1);
+by (rtac 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 efbe50e2bef9 -r 7110358acded src/HOL/UNITY/Follows.ML
--- a/src/HOL/UNITY/Follows.ML	Fri Jan 07 11:00:56 2000 +0100
+++ b/src/HOL/UNITY/Follows.ML	Fri Jan 07 11:04:15 2000 +0100
@@ -47,13 +47,13 @@
 (*
 try:
 by (asm_full_simp_tac (simpset() addsimps [Always_eq_includes_reachable]) 1);
-auto();
+by Auto_tac;
 by (blast_tac (claset() addIs [order_trans, LeadsETo_Trans]) 1);
-br LeadsETo_Trans 1;
+by (rtac LeadsETo_Trans 1);
 by (Blast_tac 2);
-bd spec 1;
-be LeadsETo_weaken 1;
-auto();
+by (dtac spec 1);
+by (etac LeadsETo_weaken 1);
+by Auto_tac;
 by (thin_tac "All ?P" 1);
 by (full_simp_tac (simpset() addsimps [givenBy_eq_Collect]) 1);
 by Safe_tac;