# HG changeset patch
# User paulson
# Date 951731382 -3600
# Node ID 6218522253e7534fb6843420078e49214060d73a
# Parent  cc2340c338f0cc3d42c5782ae0e1635689567c20
new mostly working version; Alloc nearly converted to "Rename"

diff -r cc2340c338f0 -r 6218522253e7 src/HOL/UNITY/Alloc.ML
--- a/src/HOL/UNITY/Alloc.ML	Mon Feb 28 10:49:08 2000 +0100
+++ b/src/HOL/UNITY/Alloc.ML	Mon Feb 28 10:49:42 2000 +0100
@@ -13,20 +13,47 @@
 Client :: (clientState * ((nat => clientState) * 'b)) program
 *)
 
-    Goal "(inj f) = (inv f o f = id)";
-    by (asm_simp_tac (simpset() addsimps [o_def, expand_fun_eq]) 1);
-    by (blast_tac (claset() addIs [inj_inverseI, inv_f_f]) 1);
-    qed "inj_iff";
+(***USEFUL??*)
+Goal "surj h ==> h `` {s. P (h s)} = {s. P s}";
+by Auto_tac;
+by (force_tac (claset() addSIs [exI, surj_f_inv_f RS sym], 
+	       simpset() addsimps [surj_f_inv_f]) 1);
+qed "surj_image_Collect_lemma";
+
+(**To Lift_prog.ML???????????????????????????????????????????????????????????*)
+(*Lets us prove one version of a theorem and store others*)
+Goal "f o g = h ==> f' o f o g = f' o h";
+by (asm_full_simp_tac (simpset() addsimps [expand_fun_eq, o_def]) 1);
+qed "o_equiv_assoc";
+
+Goal "f o g = h ==> ALL x. f(g x) = h x";
+by (asm_full_simp_tac (simpset() addsimps [expand_fun_eq, o_def]) 1);
+qed "o_equiv_apply";
 
-    Goal "(surj f) = (f o inv f = id)";
-    by (asm_simp_tac (simpset() addsimps [o_def, expand_fun_eq]) 1);
-    by (blast_tac (claset() addIs [surjI, surj_f_inv_f]) 1);
-    qed "surj_iff";
+fun make_o_equivs th = 
+    [th, 
+     th RS o_equiv_assoc |> simplify (HOL_ss addsimps [o_assoc]), 
+     th RS o_equiv_apply |> simplify (HOL_ss addsimps [o_def, sub_def])];
+
+Addsimps (make_o_equivs fst_o_funPair @ make_o_equivs snd_o_funPair);
 
+Goal "sub i o fst o lift_map i = fst";
+by (rtac ext 1);
+by (auto_tac (claset(), simpset() addsimps [o_def, lift_map_def, sub_def]));
+qed "fst_o_lift_map";
+
+Goal "snd o lift_map i = snd o snd";
+by (rtac ext 1);
+by (auto_tac (claset(), simpset() addsimps [o_def, lift_map_def]));
+qed "snd_o_lift_map";
+
+Addsimps (make_o_equivs fst_o_lift_map @ make_o_equivs snd_o_lift_map);
+(**To Lift_prog.ML???????????????????????????????????????????????????????????*)
 
 
 AddIs [impOfSubs subset_preserves_o];
 Addsimps [funPair_o_distrib];
+Addsimps [rename_preserves];
 
 Delsimps [o_apply];
 
@@ -156,12 +183,95 @@
 AddIffs [bij_sysOfClient];
 
 
+
+
+
+(** o-simprules for client_map **)
+
+Goal "fst o client_map = non_extra";
+by (rtac ext 1);
+by (auto_tac (claset() addSWrapper record_split_wrapper, 
+	      simpset() addsimps [o_def, client_map_def]));
+qed "fst_o_client_map";
+Addsimps (make_o_equivs fst_o_client_map);
+
+Goal "snd o client_map = clientState_u.extra";
+by (rtac ext 1);
+by (auto_tac (claset() addSWrapper record_split_wrapper, 
+	      simpset() addsimps [o_def, client_map_def]));
+qed "snd_o_client_map";
+Addsimps (make_o_equivs snd_o_client_map);
+
+(** o-simprules for sysOfAlloc **)
+
+Goal "client o sysOfAlloc = fst o allocState_u.extra ";
+by (rtac ext 1);
+by (auto_tac (claset() addSWrapper record_split_wrapper, 
+	      simpset() addsimps [o_def, sysOfAlloc_def, Let_def]));
+qed "client_o_sysOfAlloc";
+Addsimps (make_o_equivs client_o_sysOfAlloc);
+
+Goal "allocGiv o sysOfAlloc = allocGiv";
+by (rtac ext 1);
+by (auto_tac (claset() addSWrapper record_split_wrapper, 
+	      simpset() addsimps [sysOfAlloc_def, Let_def, o_def]));
+qed "allocGiv_o_sysOfAlloc_eq";
+Addsimps (make_o_equivs allocGiv_o_sysOfAlloc_eq);
+
+Goal "allocAsk o sysOfAlloc = allocAsk";
+by (rtac ext 1);
+by (auto_tac (claset() addSWrapper record_split_wrapper, 
+	      simpset() addsimps [sysOfAlloc_def, Let_def, o_def]));
+qed "allocAsk_o_sysOfAlloc_eq";
+Addsimps (make_o_equivs allocAsk_o_sysOfAlloc_eq);
+
+Goal "allocRel o sysOfAlloc = allocRel";
+by (rtac ext 1);
+by (auto_tac (claset() addSWrapper record_split_wrapper, 
+	      simpset() addsimps [sysOfAlloc_def, Let_def, o_def]));
+qed "allocRel_o_sysOfAlloc_eq";
+Addsimps (make_o_equivs allocRel_o_sysOfAlloc_eq);
+
+(** o-simprules for sysOfClient **)
+
+Goal "client o sysOfClient = fst";
+by (rtac ext 1);
+by (auto_tac (claset() addSWrapper record_split_wrapper, 
+	      simpset() addsimps [o_def, sysOfClient_def]));
+qed "client_o_sysOfClient";
+Addsimps (make_o_equivs client_o_sysOfClient);
+
+Goal "allocGiv o sysOfClient = allocGiv o snd ";
+by (rtac ext 1);
+by (auto_tac (claset() addSWrapper record_split_wrapper, 
+	      simpset() addsimps [sysOfClient_def, o_def]));
+qed "allocGiv_o_sysOfClient_eq";
+Addsimps (make_o_equivs allocGiv_o_sysOfClient_eq);
+
+Goal "allocAsk o sysOfClient = allocAsk o snd ";
+by (rtac ext 1);
+by (auto_tac (claset() addSWrapper record_split_wrapper, 
+	      simpset() addsimps [sysOfClient_def, o_def]));
+qed "allocAsk_o_sysOfClient_eq";
+Addsimps (make_o_equivs allocAsk_o_sysOfClient_eq);
+
+Goal "allocRel o sysOfClient = allocRel o snd ";
+by (rtac ext 1);
+by (auto_tac (claset() addSWrapper record_split_wrapper, 
+	      simpset() addsimps [sysOfClient_def, o_def]));
+qed "allocRel_o_sysOfClient_eq";
+Addsimps (make_o_equivs allocRel_o_sysOfClient_eq);
+
+
+
+(**
 Open_locale "System";
 
 val Alloc = thm "Alloc";
 val Client = thm "Client";
 val Network = thm "Network";
 val System_def = thm "System_def";
+**)
 
 AddIffs [finite_lessThan];
 
@@ -171,28 +281,33 @@
 		  client_bounded_def, client_progress_def,
 		  client_preserves_def] Client;
 
-Goal "Client : UNIV guarantees[funPair rel ask] Increasing ask";
-by (cut_facts_tac [Client_Spec] 1);
-by (asm_full_simp_tac (simpset() addsimps [guarantees_Int_right]) 1);
-qed "Client_Increasing_ask";
+val [Client_Increasing_ask, Client_Increasing_rel,
+     Client_Bounded, Client_Progress, Client_preserves_giv,
+     Client_preserves_extra] =
+        Client_Spec 
+          |> simplify (simpset() addsimps [guarantees_Int_right]) 
+          |> list_of_Int;
 
-Goal "Client : UNIV guarantees[funPair rel ask] Increasing rel";
-by (cut_facts_tac [Client_Spec] 1);
-by (asm_full_simp_tac (simpset() addsimps [guarantees_Int_right]) 1);
-qed "Client_Increasing_rel";
+(** Showing that a renamed Client is in "preserves snd" **)
 
-AddIffs [Client_Increasing_ask, Client_Increasing_rel];
+Goal "bij client_map";
+by (auto_tac (claset() addSWrapper record_split_wrapper, 
+	      simpset() addsimps [client_map_def, non_extra_def, bij_def, 
+				  inj_on_def, surj_def]));
+by (res_inst_tac 
+    [("x", "(|giv=?a, ask=?b, rel=?c, clientState_u.extra=?e|)")] exI 1);
+by (Force_tac 1);
+qed "bij_client_map";
+AddIffs [bij_client_map];
 
-Goal "Client : UNIV guarantees[ask] \
-\              Always {s. ALL elt : set (ask s). elt <= NbT}";
-by (cut_facts_tac [Client_Spec] 1);
-by Auto_tac;
-qed "Client_Bounded";
+(**no longer needed
+Goal "rename client_map Client : preserves snd";
+by (simp_tac (simpset() addsimps [Client_preserves_extra]) 1);
+qed "rename_Client_preserves_snd";
+**)
 
-(*Client_Progress is cumbersome to state*)
-val [_, _, Client_Progress, Client_preserves_giv] = list_of_Int Client_Spec;
-
-AddIffs [Client_preserves_giv];	    
+AddIffs [Client_Increasing_ask, Client_Increasing_rel, Client_Bounded,
+	 Client_preserves_giv, Client_preserves_extra];
 
 
 (*Network : <unfolded specification> *)
@@ -222,9 +337,11 @@
 (*Strip off the INT in the guarantees postcondition*)
 val Alloc_Increasing = normalize Alloc_Increasing_0;
 
+(*????????????????????????????????????????????????????????????????
 fun alloc_export th = good_map_sysOfAlloc RS export th |> simplify (simpset());
 
 fun client_export th = good_map_sysOfClient RS export th |> simplify (simpset());
+*)
 
 AddIffs (Alloc_preserves |> simplify (simpset()) |> list_of_Int);
 
@@ -232,19 +349,21 @@
 
 (*Alternative is to say that System = Network Join F such that F preserves
   certain state variables*)
-Goal "(extend sysOfClient (plam x: lessThan Nclients. Client)) Join \
-\     (Network Join Alloc)  =  System";
-by (simp_tac (simpset() addsimps System_def::Join_ac) 1);
-qed "Client_component_System";
-
 Goal "Network Join \
-\     ((extend sysOfClient (plam x: lessThan Nclients. Client)) Join Alloc) \
+\     ((rename sysOfClient \
+\       (plam x: lessThan 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 "Alloc Join \
-\      ((extend sysOfClient (plam x: lessThan Nclients. Client)) Join \
+Goal "(rename sysOfClient (plam x: lessThan 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 \
 \       Network)  =  System";
 by (simp_tac (simpset() addsimps System_def::Join_ac) 1);
 qed "Alloc_component_System";
@@ -254,59 +373,103 @@
 
 (** These preservation laws should be generated automatically **)
 
-(*technical lemma*)
-bind_thm ("extend_sysOfClient_preserves_o", 
-	  inj_sysOfClient RS export inj_extend_preserves RS 
-	  impOfSubs subset_preserves_o
-	  |> simplify (simpset() addsimps [o_def]));
+AddIs    [impOfSubs subset_preserves_o];
+Addsimps [impOfSubs subset_preserves_o];
+
+    (*** Lemmas about "preserves" 
+
+    val preserves_imp_preserves_apply = 
+	impOfSubs subset_preserves_o |> simplify (simpset() addsimps [o_def]);
+
+    Goal "F : preserves snd ==> rename sysOfClient F : preserves allocGiv";
+    by (simp_tac (simpset() addsimps [rename_preserves]) 1);
+    by (asm_simp_tac (simpset() addsimps [sysOfClient_def, o_def, split_def, 
+					  preserves_imp_preserves_apply]) 1);
+    qed "rename_sysOfClient_preserves_allocGiv";
+
+    Goal "F : preserves snd ==> rename sysOfClient F : preserves allocAsk";
+    by (simp_tac (simpset() addsimps [rename_preserves]) 1);
+    by (asm_simp_tac (simpset() addsimps [sysOfClient_def, o_def, split_def, 
+					  preserves_imp_preserves_apply]) 1);
+    qed "rename_sysOfClient_preserves_allocAsk";
 
-Goal "extend sysOfClient F : preserves allocGiv";
-by (cut_inst_tac [("w", "allocGiv")] (extend_sysOfClient_preserves_o) 1);
-by Auto_tac;
-qed "extend_sysOfClient_preserves_allocGiv";
+    Goal "F : preserves snd ==> rename sysOfClient F : preserves allocRel";
+    by (simp_tac (simpset() addsimps [rename_preserves]) 1);
+    by (asm_simp_tac (simpset() addsimps [sysOfClient_def, o_def, split_def, 
+					  preserves_imp_preserves_apply]) 1);
+    qed "rename_sysOfClient_preserves_allocRel";
+
+    Addsimps [rename_sysOfClient_preserves_allocGiv,
+	      rename_sysOfClient_preserves_allocAsk,
+	      rename_sysOfClient_preserves_allocRel];
 
-Goal "extend sysOfClient F : preserves allocAsk";
-by (cut_inst_tac [("w", "allocAsk")] (extend_sysOfClient_preserves_o) 1);
-by Auto_tac;
-qed "extend_sysOfClient_preserves_allocAsk";
+    AddIs [rename_sysOfClient_preserves_allocGiv,
+	   rename_sysOfClient_preserves_allocAsk,
+	   rename_sysOfClient_preserves_allocRel];
+
+    Goal "(rename sysOfClient F : preserves (v o client)) = \
+    \     (F : preserves (v o fst))";
+    by (simp_tac (simpset() addsimps [rename_preserves]) 1);
+    by (asm_simp_tac (simpset() addsimps [sysOfClient_def, o_def, split_def]) 1);
+    qed "rename_sysOfClient_preserves_client";
+    AddIffs [rename_sysOfClient_preserves_client];
+
+Goal "rename sysOfAlloc Alloc : preserves client";
+by (simp_tac (simpset() addsimps [rename_preserves]) 1);
+result();
 
-Goal "extend sysOfClient F : preserves allocRel";
-by (cut_inst_tac [("w", "allocRel")] (extend_sysOfClient_preserves_o) 1);
-by Auto_tac;
-qed "extend_sysOfClient_preserves_allocRel";
+    ***)
 
-AddIffs [extend_sysOfClient_preserves_allocGiv,
-	 extend_sysOfClient_preserves_allocAsk,
-	 extend_sysOfClient_preserves_allocRel];
-
+(*Lifting Client_Increasing to systemState*)
+Goal "i : I \
+\     ==> rename sysOfClient (plam x: I. rename client_map Client) : \
+\           UNIV \
+\           guarantees[(funPair rel ask) o sub i o client]  \
+\             Increasing (ask o sub i o client) Int \
+\             Increasing (rel o sub i o client)";
+by (simp_tac (simpset() addsimps [rename_guarantees_eq_rename_inv]) 1);
+by (rtac guarantees_PLam_I 1);
+ba 2;
+(*preserves: routine reasoning*)
+by (asm_simp_tac (simpset() addsimps [lift_preserves_sub]) 2);
+(*the guarantee for  "lift i (rename client_map Client)" *)
+by (asm_simp_tac
+    (simpset() addsimps [lift_guarantees_eq_lift_inv, 
+			 rename_guarantees_eq_rename_inv,
+			 bij_imp_bij_inv, surj_rename RS surj_range,
+			 bij_rename, bij_image_INT, bij_is_inj RS image_Int,
+			 rename_image_Increasing, inv_inv_eq]) 1);
+by (asm_simp_tac
+    (simpset() addsimps [o_def, non_extra_def, guarantees_Int_right]) 1);
+qed "rename_Client_Increasing";
 
-(* (extend sysOfClient F : preserves (v o client)) = (F : preserves v) *)
-bind_thm ("extend_sysOfClient_preserves_o_client",
-	  client_export extend_preserves);
-AddIffs [extend_sysOfClient_preserves_o_client];
+(*Lifting Alloc_Increasing to systemState*)
+Goal "i < Nclients \
+\     ==> rename sysOfAlloc Alloc :  \
+\           UNIV  guarantees[allocGiv]  Increasing (sub i o allocGiv)";
+by (asm_simp_tac
+    (simpset() addsimps [rename_guarantees_eq_rename_inv,
+			 bij_imp_bij_inv, surj_rename RS surj_range,
+			 bij_rename, bij_image_INT, 
+			 rename_image_Increasing, inv_inv_eq,
+			 Alloc_Increasing]) 1);
+qed "rename_Alloc_Increasing";
 
+Goal "i < Nclients \
+\     ==> System : Increasing (ask o sub i o client) Int \
+\                  Increasing (rel o sub i o client)";
+by (rtac ([rename_Client_Increasing,
+	   Client_component_System] MRS component_guaranteesD) 1);
+by Auto_tac;
+qed "System_Increasing";
 
 Goalw [System_def]
      "i < Nclients ==> System : Increasing (sub i o allocGiv)";
-by (rtac (Alloc_Increasing RS guarantees_Join_I1 RS guaranteesD) 1);
+by (rtac (rename_Alloc_Increasing RS guarantees_Join_I1 RS guaranteesD) 1);
 by Auto_tac;
 qed "System_Increasing_allocGiv";
 
-
-Goal "i < Nclients ==> System : Increasing (ask o sub i o client)";
-by (rtac ([client_export extend_guar_Increasing,
-	   Client_component_System] MRS component_guaranteesD) 1);
-by (rtac (lift_prog_guar_Increasing RS guarantees_PLam_I) 1);
-by Auto_tac;
-qed "System_Increasing_ask";
-
-Goal "i < Nclients ==> System : Increasing (rel o sub i o client)";
-by (rtac ([client_export extend_guar_Increasing,
-	   Client_component_System] MRS component_guaranteesD) 1);
-by (rtac (lift_prog_guar_Increasing RS guarantees_PLam_I) 1);
-(*gets Client_Increasing_rel from simpset*)
-by Auto_tac;
-qed "System_Increasing_rel";
+AddSIs (list_of_Int System_Increasing);
 
 (** Follows consequences.
     The "Always (INT ...) formulation expresses the general safety property
@@ -314,23 +477,22 @@
 
 Goal
   "i < Nclients ==> System : ((sub i o allocRel) Fols (rel o sub i o client))";
-by (auto_tac (claset() addSIs [System_Increasing_rel, 
-			       Network_Rel RS component_guaranteesD], 
+by (auto_tac (claset() addSIs [Network_Rel RS component_guaranteesD], 
 	      simpset()));
 qed "System_Follows_rel";
 
 Goal
   "i < Nclients ==> System : ((sub i o allocAsk) Fols (ask o sub i o client))";
-by (auto_tac (claset() addSIs [System_Increasing_ask, 
-			       Network_Ask RS component_guaranteesD], 
+by (auto_tac (claset() addSIs [Network_Ask RS component_guaranteesD], 
 	      simpset()));
 qed "System_Follows_ask";
 
 Goal
   "i < Nclients ==> System : (giv o sub i o client) Fols (sub i o allocGiv)";
 by (auto_tac (claset() addSIs [Network_Giv RS component_guaranteesD, 
-		 Alloc_Increasing RS component_guaranteesD], 
+		 rename_Alloc_Increasing RS component_guaranteesD], 
 	      simpset()));
+by (simp_tac (simpset() addsimps [o_def, non_extra_def]) 1);
 qed "System_Follows_allocGiv";
 
 Goal "System : Always (INT i: lessThan Nclients. \
@@ -363,12 +525,28 @@
 by (etac (System_Follows_rel RS Follows_Increasing1) 1);
 qed "System_Increasing_allocRel";
 
+Goal "rename sysOfAlloc Alloc :  \
+\       (INT i : lessThan 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}";
+by (asm_simp_tac
+    (simpset() addsimps [rename_guarantees_eq_rename_inv,
+			 bij_imp_bij_inv, bij_rename, 
+			 bij_image_INT, 
+			 rename_image_Increasing, rename_image_Always,
+			 inv_inv_eq, bij_image_Collect_eq]) 1);
+by (cut_facts_tac [Alloc_Safety] 1);
+by (full_simp_tac (simpset() addsimps [o_def]) 1);
+qed "rename_Alloc_Safety";
+
 (*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}";
-by (rtac ([Alloc_Safety, Alloc_component_System] MRS component_guaranteesD) 1);
+by (rtac ([rename_Alloc_Safety, Alloc_component_System] MRS 
+	  component_guaranteesD) 1);
 (*preserves*)
-by (asm_full_simp_tac (simpset() addsimps [o_def]) 2);
+by (Simp_tac 2);
 by (force_tac (claset(), simpset() addsimps [System_Increasing_allocRel]) 1);
 qed "System_sum_bounded";
 
@@ -412,32 +590,39 @@
 
 (*progress (2), step 2; see also System_Increasing_allocRel*)
 Goal "i < Nclients ==> System : Increasing (sub i o allocAsk)";
-by (rtac Follows_Increasing1 1);
-by (blast_tac (claset() addIs [Network_Ask RS component_guaranteesD,
-			       System_Increasing_ask]) 1);
+by (etac (System_Follows_ask RS Follows_Increasing1) 1);
 qed "System_Increasing_allocAsk";
 
-val Client_i_Bounded =
-    [Client_Bounded, projecting_UNIV, lift_export extending_Always] 
-    MRS drop_prog_guarantees;
+(*progress (2), step 3*)
+(*All this trouble just to lift "Client_Bounded" to systemState
+  (though it is similar to that for Client_Increasing*)
+Goal "i : I \
+\   ==> rename sysOfClient (plam x: I. rename client_map Client) : \
+\         UNIV \
+\         guarantees[ask o sub i o client]  \
+\           Always {s. ALL elt : set ((ask o sub i o client) s). elt <= NbT}";
+by (simp_tac (simpset() addsimps [rename_guarantees_eq_rename_inv]) 1);
+by (rtac guarantees_PLam_I 1);
+ba 2;
+(*preserves: routine reasoning*)
+by (asm_simp_tac (simpset() addsimps [lift_preserves_sub]) 2);
+(*the guarantee for  "lift i (rename client_map Client)" *)
+by (asm_simp_tac
+    (simpset() addsimps [lift_guarantees_eq_lift_inv, 
+			 rename_guarantees_eq_rename_inv,
+			 bij_imp_bij_inv, surj_rename RS surj_range,
+			 bij_rename, bij_image_INT, bij_is_inj RS image_Int,
+			 rename_image_Always, inv_inv_eq,
+			 bij_image_Collect_eq]) 1);
+by (asm_simp_tac (simpset() addsimps [o_def, non_extra_def]) 1);
+qed "rename_Client_Bounded";
 
-val UNIV_guar_Always =
-    [asm_rl, projecting_UNIV, extending_Always] 
-    MRS project_guarantees;
-
-
-(*progress (2), step 3*)
-(*All this trouble just to lift "Client_Bounded" through two extend ops*)
 Goal "i < Nclients \
 \     ==> System : Always \
 \                   {s. ALL elt : set ((ask o sub i o client) s). elt <= NbT}";
-by (rtac Always_weaken 1);
-by (rtac ([guarantees_PLam_I RS client_export UNIV_guar_Always,
+by (rtac ([rename_Client_Bounded,
 	   Client_component_System] MRS component_guaranteesD) 1);
-by (rtac Client_i_Bounded 1);
-by (auto_tac(claset(),
-	 simpset() addsimps [o_apply, lift_export extend_set_eq_Collect,
-			     client_export extend_set_eq_Collect]));
+by Auto_tac;
 qed "System_Bounded_ask";
 
 (*progress (2), step 4*)
@@ -454,30 +639,62 @@
 
 (*progress (2), step 6*)
 Goal "i < Nclients ==> System : Increasing (giv o sub i o client)";
-by (rtac Follows_Increasing1 1);
-by (auto_tac (claset() addIs [Network_Giv RS component_guaranteesD,
-			       System_Increasing_allocGiv], 
-	      simpset()));
+by (etac (System_Follows_allocGiv RS Follows_Increasing1) 1);
 qed "System_Increasing_giv";
 
+
+xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx;
+
+
+
 (** A LOT of work just to lift "Client_Progress" to the array **)
 
-(*stability lemma for G*)
-Goalw [preserves_def, o_def, stable_def, constrains_def, sub_def]
-     "[| ALL z. G : stable      \
-\                   (reachable (lift_prog i Client Join G) Int      \
-\                    {s. z <= (giv o sub i) s});      \
-\         G : preserves (rel o sub i);  G : preserves (ask o sub i) |]      \
-\      ==> G : stable      \
-\               (reachable (lift_prog i Client Join G) Int      \
-\                {s. h <= (giv o sub i) s & h pfixGe (ask o sub i) s} -      \
-\                {s. tokens h <= tokens ((rel o sub i) s)})";
-by Auto_tac;
-by (REPEAT (dres_inst_tac [("x", "rel (xa i)")] spec 2));
-by (REPEAT (dres_inst_tac [("x", "ask (xa i)")] spec 1));
-by (REPEAT_FIRST ball_tac);
-by Auto_tac;
-qed "G_stable_lift_prog";
+
+Goal "i: I \
+\  ==> rename sysOfClient (plam x: I. rename client_map Client) \
+\       : Increasing (giv o sub i o client)  \
+\         guarantees[funPair rel ask o sub i o client] \
+\         (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})";
+by (simp_tac (simpset() addsimps [rename_guarantees_eq_rename_inv]) 1);
+by (rtac guarantees_PLam_I 1);
+ba 2;
+(*preserves: routine reasoning*)
+by (asm_simp_tac (simpset() addsimps [lift_preserves_sub]) 2);
+(*the guarantee for  "lift i (rename client_map Client)" *)
+by (asm_simp_tac
+    (simpset() addsimps [lift_guarantees_eq_lift_inv, 
+			 rename_guarantees_eq_rename_inv,
+			 bij_imp_bij_inv, surj_rename RS surj_range,
+			 bij_rename, bij_image_INT, bij_is_inj RS image_Int,
+			 (****rename_image_LeadsTo,***) rename_image_Increasing, 
+			 inv_inv_eq,
+			 bij_image_Collect_eq]) 1);
+by (asm_simp_tac (simpset() addsimps [o_def, non_extra_def]) 1);
+
+
+by (rtac (lemma2 RS client_export project_guarantees_raw) 1);
+by (assume_tac 1);
+by (rtac (client_export project_Increasing_I) 1);
+by (Simp_tac 1);
+by (rtac INT_I 1);
+by (simp_tac (simpset() addsimps [o_apply]) 1);
+by (REPEAT (stac (client_export extend_set_eq_Collect RS sym) 1));
+by (rtac (client_export project_Ensures_D) 1);
+by (asm_full_simp_tac (simpset() addsimps [o_apply]) 1);
+by (asm_full_simp_tac
+    (simpset() addsimps [all_conj_distrib,
+			 Increasing_def, Stable_eq_stable, Join_stable,
+			 extend_set_eq_Collect]) 1);
+by (Clarify_tac 1);
+by (dtac G_stable_sysOfClient 1);
+by (auto_tac (claset(), 
+     simpset() addsimps [o_apply, client_export extend_set_eq_Collect]));
+qed "rename_Client_Progress";
+
+
+
 
 Goal "lift_prog i Client \
 \        : Increasing (giv o sub i)  \
@@ -518,53 +735,6 @@
 by Auto_tac;
 val lemma2 = result();
 
-(*another stability lemma for G*)
-Goalw [preserves_def, o_def, stable_def, constrains_def, sub_def]
-     "[| ALL z. G : stable      \
-\                  (reachable (extend sysOfClient  \
-\                              (plam x:lessThan Nclients. Client) Join G) Int \
-\                    {s. z <= (giv o sub i o client) s});      \
-\         G : preserves (rel o sub i o client);  \
-\         G : preserves (ask o sub i o client) |]      \
-\ ==> G : stable      \
-\          (reachable (extend sysOfClient  \
-\                      (plam x:lessThan Nclients. Client) Join G) Int \
-\           {s. h <= (giv o sub i o client) s & \
-\               h pfixGe (ask o sub i o client) s} - \
-\           {s. tokens h <= tokens ((rel o sub i o client) s)})";
-by Auto_tac;
-by (REPEAT (dres_inst_tac [("x", "rel (client xa i)")] spec 2));
-by (REPEAT (dres_inst_tac [("x", "ask (client xa i)")] spec 1));
-by (REPEAT_FIRST ball_tac);
-by Auto_tac;
-qed "G_stable_sysOfClient";
-
-Goal "i < Nclients \
-\  ==> extend sysOfClient (plam x: lessThan Nclients. Client) \
-\       : Increasing (giv o sub i o client)  \
-\         guarantees[funPair rel ask o sub i o client] \
-\         (INT h. {s. h <=  (giv o sub i o client) s & \
-\                            h pfixGe (ask o sub i o client) s}  \
-\                 Ensures {s. tokens h <= (tokens o rel o sub i o client) s})";
-by (rtac (lemma2 RS client_export project_guarantees_raw) 1);
-by (assume_tac 1);
-by (rtac (client_export project_Increasing_I) 1);
-by (Simp_tac 1);
-by (rtac INT_I 1);
-by (simp_tac (simpset() addsimps [o_apply]) 1);
-by (REPEAT (stac (client_export extend_set_eq_Collect RS sym) 1));
-by (rtac (client_export project_Ensures_D) 1);
-by (asm_full_simp_tac (simpset() addsimps [o_apply]) 1);
-by (asm_full_simp_tac
-    (simpset() addsimps [all_conj_distrib,
-			 Increasing_def, Stable_eq_stable, Join_stable,
-			 extend_set_eq_Collect]) 1);
-by (Clarify_tac 1);
-by (dtac G_stable_sysOfClient 1);
-by (auto_tac (claset(), 
-     simpset() addsimps [o_apply, client_export extend_set_eq_Collect]));
-qed "sysOfClient_i_Progress";
-
 
 (*progress (2), step 7*)
 Goal
@@ -574,7 +744,7 @@
 \               Ensures {s. tokens h <= (tokens o rel o sub i o client) s})";
 by (rtac INT_I 1);
 (*Couldn't have just used Auto_tac since the "INT h" must be kept*)
-by (rtac ([sysOfClient_i_Progress,
+by (rtac ([rename_Client_Progress,
 	   Client_component_System] MRS component_guaranteesD) 1);
 by (asm_full_simp_tac
     (simpset() addsimps [System_Increasing_giv]) 2);
diff -r cc2340c338f0 -r 6218522253e7 src/HOL/UNITY/Alloc.thy
--- a/src/HOL/UNITY/Alloc.thy	Mon Feb 28 10:49:08 2000 +0100
+++ b/src/HOL/UNITY/Alloc.thy	Mon Feb 28 10:49:42 2000 +0100
@@ -43,9 +43,17 @@
   clientState +
   extra :: 'a       (*dummy field for new variables*)
 
-consts
-  rClient  :: "(clientState * 'a) program"  (*DUMMY CONSTANT*)
+constdefs
+  (*DUPLICATED FROM Client.thy, but with "tok" removed*)
+  (*Maybe want a special theory section to declare such maps*)
+  non_extra :: 'a clientState_u => clientState
+    "non_extra s == (|giv = giv s, ask = ask s, rel = rel s|)"
 
+  (*Renaming map to put a Client into the standard form*)
+  client_map :: "'a clientState_u => clientState*'a"
+    "client_map == funPair non_extra extra"
+
+  
 record allocState =
   allocGiv :: nat => nat list   (*OUTPUT history: source of "giv" for i*)
   allocAsk :: nat => nat list   (*INPUT: allocator's copy of "ask" for i*)
@@ -105,7 +113,7 @@
 
   (*spec: preserves part*)
     client_preserves :: 'a clientState_u program set
-    "client_preserves == preserves giv"
+    "client_preserves == preserves (funPair giv clientState_u.extra)"
 
   client_spec :: 'a clientState_u program set
     "client_spec == client_increasing Int client_bounded Int client_progress
@@ -149,7 +157,8 @@
 
   (*spec: preserves part*)
     alloc_preserves :: 'a allocState_u program set
-    "alloc_preserves == preserves (funPair allocRel allocAsk)"
+    "alloc_preserves == preserves (funPair allocRel
+				   (funPair allocAsk allocState_u.extra))"
   
   alloc_spec :: 'a allocState_u program set
     "alloc_spec == alloc_increasing Int alloc_safety Int alloc_progress Int
@@ -206,14 +215,32 @@
 			         client   = cl,
 			         systemState.extra = allocState_u.extra al|)"
 
-
-locale System =
-  fixes 
-    Alloc   :: 'a allocState program
-    Client  :: clientState program
+consts 
+    Alloc   :: 'a allocState_u program
+    Client  :: 'a clientState_u program
     Network :: 'a systemState program
     System  :: 'a systemState program
   
+rules
+    Alloc   "Alloc   : alloc_spec"
+    Client  "Client  : client_spec"
+    Network "Network : network_spec"
+
+defs
+    System_def
+      "System == rename sysOfAlloc Alloc Join Network Join
+                 (rename sysOfClient
+		  (plam x: lessThan Nclients. rename client_map Client))"
+
+
+(**
+locale System =
+  fixes 
+    Alloc   :: 'a allocState_u program
+    Client  :: 'a clientState_u program
+    Network :: 'a systemState program
+    System  :: 'a systemState program
+
   assumes
     Alloc   "Alloc   : alloc_spec"
     Client  "Client  : client_spec"
@@ -221,9 +248,13 @@
 
   defines
     System_def
-      "System == rename sysOfAlloc Alloc Join Network Join
-                 (rename sysOfClient (plam x: lessThan Nclients. Client))"
-
+      "System == rename sysOfAlloc Alloc
+                 Join
+                 Network
+                 Join
+                 (rename sysOfClient
+		  (plam x: lessThan Nclients. rename client_map Client))"
+**)
 
 
 end
diff -r cc2340c338f0 -r 6218522253e7 src/HOL/UNITY/Client.ML
--- a/src/HOL/UNITY/Client.ML	Mon Feb 28 10:49:08 2000 +0100
+++ b/src/HOL/UNITY/Client.ML	Mon Feb 28 10:49:42 2000 +0100
@@ -149,6 +149,8 @@
 by (blast_tac (claset() addIs [client_progress_lemma]) 1);
 qed "client_progress";
 
+(*This shows that the Client won't alter other variables in any state
+  that it is combined with*)
 Goal "Client : preserves extra";
 by (rewtac preserves_def);
 by Auto_tac;
@@ -156,21 +158,6 @@
 by Auto_tac;
 qed "client_preserves_extra";
 
-Goal "bij client_map";
-by (auto_tac (claset() addSWrapper record_split_wrapper, 
-	      simpset() addsimps [client_map_def, non_extra_def, bij_def, 
-				  inj_on_def, surj_def]));
-by (res_inst_tac 
-    [("x", "(|giv=?a, ask=?b, rel=?c, tok=?d, extra=?e|)")] exI 1);
-by (Force_tac 1);
-qed "bij_client_map";
-
-Goal "rename client_map Client : preserves snd";
-by (asm_simp_tac (simpset() addsimps [bij_client_map RS rename_preserves]) 1);
-by (asm_simp_tac (simpset() addsimps [client_map_def]) 1);
-by (rtac client_preserves_extra 1);
-qed "client_preserves_extra";
-
 
 (** Obsolete lemmas from first version of the Client **)
 
diff -r cc2340c338f0 -r 6218522253e7 src/HOL/UNITY/Lift_prog.ML
--- a/src/HOL/UNITY/Lift_prog.ML	Mon Feb 28 10:49:08 2000 +0100
+++ b/src/HOL/UNITY/Lift_prog.ML	Mon Feb 28 10:49:42 2000 +0100
@@ -85,6 +85,19 @@
 qed "inv_lift_map_eq";
 Addsimps [inv_lift_map_eq];
 
+Goal "inv (drop_map i) = lift_map i";
+by (rtac inv_equality 1);
+by (rtac drop_map_lift_map_eq 2);
+by (rtac lift_map_drop_map_eq 1);
+qed "inv_drop_map_eq";
+Addsimps [inv_drop_map_eq];
+
+Goal "bij (drop_map i)";
+by (simp_tac (simpset() delsimps [inv_lift_map_eq]
+                        addsimps [inv_lift_map_eq RS sym, bij_imp_bij_inv]) 1);
+qed "bij_drop_map";
+AddIffs [bij_drop_map];
+
 (*** sub ***)
 
 Goal "sub i f = f i";
@@ -108,11 +121,12 @@
 qed "lift_set_iff";
 AddIffs [lift_set_iff];
 
+(*Do we really need both this one and its predecessor?*)
 Goal "((f,uu) : lift_set i A) = ((f i, (delete_map i f, uu)) : A)";
 by (asm_simp_tac (simpset() addsimps [lift_set_def, 
 				      mem_rename_set_iff, drop_map_def]) 1);
-qed "lift_set_iff";
-AddIffs [lift_set_iff];
+qed "lift_set_iff2";
+AddIffs [lift_set_iff2];
 
 Goalw [lift_set_def] "A<=B ==> lift_set i A <= lift_set i B";
 by (etac image_mono 1);
diff -r cc2340c338f0 -r 6218522253e7 src/HOL/UNITY/PPROD.ML
--- a/src/HOL/UNITY/PPROD.ML	Mon Feb 28 10:49:08 2000 +0100
+++ b/src/HOL/UNITY/PPROD.ML	Mon Feb 28 10:49:42 2000 +0100
@@ -111,8 +111,24 @@
 \         (if j: I then F j : preserves (v o fst) else True)";
 by (asm_simp_tac (simpset() addsimps [PLam_def, lift_preserves_sub]) 1);
 by (Blast_tac 1);
-qed "PLam_preserves";
-Addsimps [PLam_preserves];
+qed "PLam_preserves_fst";
+Addsimps [PLam_preserves_fst];
+
+Goal "ALL j. F j : preserves snd ==> PLam I F : preserves snd";
+by (asm_simp_tac (simpset() addsimps [PLam_def, lift_preserves_snd_I]) 1);
+qed "PLam_preserves_snd";
+Addsimps [PLam_preserves_snd];
+AddIs [PLam_preserves_snd];
+
+
+(*** guarantees properties ***)
+
+Goalw [PLam_def]
+    "[| lift i (F i): X guarantees[v] Y;  i : I;  \
+\        ALL j:I. i~=j --> lift j (F j) : preserves v |]  \
+\    ==> (PLam I F) : X guarantees[v] Y";
+by (asm_simp_tac (simpset() addsimps [guarantees_JN_I]) 1);
+qed "guarantees_PLam_I";
 
 
 (**UNUSED
@@ -256,15 +272,5 @@
     by (asm_full_simp_tac
 	(simpset() addsimps [finite_lessThan, const_PLam_Stable]) 1);
     qed "const_PLam_Increasing";
-
-
-    (*** guarantees properties ***)
-
-    Goalw [PLam_def]
-	"[| lift i (F i): X guarantees[v] Y;  i : I;  \
-    \        ALL j:I. i~=j --> lift j (F j) : preserves v |]  \
-    \    ==> (PLam I F) : X guarantees[v] Y";
-    by (asm_simp_tac (simpset() addsimps [guarantees_JN_I]) 1);
-    qed "guarantees_PLam_I";
 **)
 
diff -r cc2340c338f0 -r 6218522253e7 src/HOL/UNITY/Rename.ML
--- a/src/HOL/UNITY/Rename.ML	Mon Feb 28 10:49:08 2000 +0100
+++ b/src/HOL/UNITY/Rename.ML	Mon Feb 28 10:49:42 2000 +0100
@@ -31,7 +31,7 @@
 qed "mem_rename_set_iff";
 
 Goal "bij h ==> h``{s. P s} = {s. P (inv h s)}";
-by (auto_tac (claset() addSIs [exI],
+by (auto_tac (claset() addSIs [image_eqI],
 	      simpset() addsimps [bij_is_inj, bij_is_surj RS surj_f_inv_f]));
 qed "rename_set_eq_Collect";
 
@@ -117,6 +117,20 @@
 by Auto_tac;
 qed "rename_inv_eq";
 
+Goal "bij h ==> inj (rename h)";
+by (asm_simp_tac (simpset() addsimps [inj_iff, expand_fun_eq, o_def, 
+				      rename_inv_eq RS sym]) 1);
+qed "inj_rename";
+
+Goal "bij h ==> surj (rename h)";
+by (asm_simp_tac (simpset() addsimps [surj_iff, expand_fun_eq, o_def, 
+				      rename_inv_eq RS sym]) 1);
+qed "surj_rename";
+
+Goal "bij h ==> bij (rename h)";
+by (blast_tac (claset() addIs [bijI, inj_rename, surj_rename]) 1);
+qed "bij_rename";
+
 
 (*** the lattice operations ***)
 
@@ -140,7 +154,8 @@
 qed "rename_JN";
 Addsimps [rename_JN];
 
-(*** Safety: co, stable ***)
+
+(*** Strong Safety: co, stable ***)
 
 Goalw [rename_def]
      "bij h ==> (rename h F : (h``A) co (h``B)) = (F : A co B)";
@@ -158,6 +173,50 @@
 				      bij_is_inj RS inj_image_subset_iff]) 1);
 qed "rename_invariant";
 
+Goal "bij h ==> (rename h F : increasing func) = (F : increasing (func o h))";
+by (asm_simp_tac 
+    (simpset() addsimps [increasing_def, rename_stable RS sym,
+  		 bij_image_Collect_eq, bij_is_surj RS surj_f_inv_f]) 1);
+qed "rename_increasing";
+
+Goal "bij h ==> rename h `` (A co B) = (h `` A) co (h``B)";
+by Auto_tac;
+by (asm_simp_tac (simpset() addsimps [rename_constrains]) 1);
+by (rtac image_eqI 1);
+by (etac (surj_rename RS surj_f_inv_f RS sym) 1);
+by (asm_simp_tac (simpset() addsimps [rename_constrains RS sym,
+				      surj_rename RS surj_f_inv_f]) 1);
+qed "rename_image_constrains";
+
+Goal "bij h ==> rename h `` stable A = stable (h `` A)";
+by (asm_simp_tac (simpset() addsimps [stable_def, rename_image_constrains]) 1);
+qed "rename_image_stable";
+
+Goal "bij h ==> rename h `` increasing func = increasing (func o inv h)";
+by Auto_tac;
+by (asm_simp_tac (simpset() addsimps [rename_increasing,o_def,bij_is_inj]) 1);
+by (rtac image_eqI 1);
+by (etac (surj_rename RS surj_f_inv_f RS sym) 1);
+by (asm_simp_tac (simpset() addsimps [rename_inv_eq RS sym, rename_increasing,
+				      bij_imp_bij_inv]) 1);
+qed "rename_image_increasing";
+
+Goal "bij h ==> rename h `` {F. Init F <= A} = {F. Init F <= h``A}";
+by (asm_simp_tac 
+    (simpset() addsimps [bij_rename, bij_image_Collect_eq,
+			 rename_inv_eq RS sym, vimage_subset_eq RS sym,
+			 bij_vimage_eq_inv_image]) 1);
+qed "rename_image_Init";
+
+Goal "bij h ==> rename h `` invariant A = invariant (h `` A)";
+by (asm_simp_tac (simpset() addsimps [invariant_def, rename_image_Init,
+				      rename_image_stable,
+				      inj_rename, image_Int]) 1);
+qed "rename_image_invariant";
+
+
+(*** Weak Safety: Co, Stable ***)
+
 Goalw [rename_def]
      "bij h ==> reachable (rename h F) = h `` (reachable F)";
 by (asm_simp_tac (simpset() addsimps [export reachable_extend_eq]) 1);
@@ -179,6 +238,40 @@
 				      bij_is_inj RS inj_image_subset_iff]) 1);
 qed "rename_Always";
 
+Goal "bij h ==> (rename h F : Increasing func) = (F : Increasing (func o h))";
+by (asm_simp_tac 
+    (simpset() addsimps [Increasing_def, rename_Stable RS sym,
+  		 bij_image_Collect_eq, bij_is_surj RS surj_f_inv_f]) 1);
+qed "rename_Increasing";
+
+Goal "bij h ==> rename h `` (A Co B) = (h `` A) Co (h``B)";
+by Auto_tac;
+by (asm_simp_tac (simpset() addsimps [rename_Constrains]) 1);
+by (rtac image_eqI 1);
+by (etac (surj_rename RS surj_f_inv_f RS sym) 1);
+by (asm_simp_tac (simpset() addsimps [rename_Constrains RS sym,
+				      surj_rename RS surj_f_inv_f]) 1);
+qed "rename_image_Constrains";
+
+Goal "bij h ==> rename h `` Stable A = Stable (h `` A)";
+by (asm_simp_tac (simpset() addsimps [Stable_def, rename_image_Constrains]) 1);
+qed "rename_image_Stable";
+
+Goal "bij h ==> rename h `` Increasing func = Increasing (func o inv h)";
+by Auto_tac;
+by (asm_simp_tac (simpset() addsimps [rename_Increasing,o_def,bij_is_inj]) 1);
+by (rtac image_eqI 1);
+by (etac (surj_rename RS surj_f_inv_f RS sym) 1);
+by (asm_simp_tac (simpset() addsimps [rename_inv_eq RS sym, rename_Increasing,
+				      bij_imp_bij_inv]) 1);
+qed "rename_image_Increasing";
+
+Goal "bij h ==> rename h `` Always A = Always (h `` A)";
+by (asm_simp_tac (simpset() addsimps [Always_def, rename_image_Init,
+				      rename_image_Stable,
+				      inj_rename, image_Int]) 1);
+qed "rename_image_Always";
+
 
 (*** Progress: transient, ensures ***)
 
diff -r cc2340c338f0 -r 6218522253e7 src/HOL/UNITY/UNITY.ML
--- a/src/HOL/UNITY/UNITY.ML	Mon Feb 28 10:49:08 2000 +0100
+++ b/src/HOL/UNITY/UNITY.ML	Mon Feb 28 10:49:42 2000 +0100
@@ -10,6 +10,9 @@
 
 set proof_timing;
 
+(*Perhaps equalities.ML shouldn't add this in the first place!*)
+Delsimps [image_Collect];
+
 
 (*** General lemmas ***)