polished version of the Allocator using Rename

--- a/src/HOL/UNITY/Alloc.ML	Thu Mar 02 10:26:22 2000 +0100
+++ b/src/HOL/UNITY/Alloc.ML	Thu Mar 02 10:29:29 2000 +0100
@@ -5,8 +5,6 @@
 
 Specification of Chandy and Charpentier's Allocator
 
-guarantees_PLam_I looks wrong: refers to lift_prog
-
 Goal "(plam x: lessThan Nclients. Client) = x";
 Client :: (clientState * ((nat => clientState) * 'b)) program
 *)
@@ -21,8 +19,7 @@
 
 AddIs [impOfSubs subset_preserves_o];
 Addsimps [funPair_o_distrib];
-Addsimps [rename_preserves];
-
+Addsimps [Always_INT_distrib];
 Delsimps [o_apply];
 
 (*Eliminate the "o" operator*)
@@ -33,7 +30,9 @@
 	  rename_image_increasing, rename_image_invariant,
 	  rename_image_Constrains, rename_image_Stable,
 	  rename_image_Increasing, rename_image_Always,
-	  rename_image_leadsTo, rename_image_LeadsTo];
+	  rename_image_leadsTo, rename_image_LeadsTo,
+	  rename_preserves,
+	  bij_image_INT, bij_is_inj RS image_Int, bij_image_Collect_eq];
 
 (*Splits up conjunctions & intersections: like CONJUNCTS in the HOL system*)
 fun list_of_Int th = 
@@ -91,7 +90,7 @@
 Addsimps [inv_sysOfAlloc_eq];
 
 Goal "surj sysOfAlloc";
-by (simp_tac (simpset() addsimps [surj_iff, expand_fun_eq, o_def]) 1);
+by (simp_tac (simpset() addsimps [surj_iff, expand_fun_eq, o_apply]) 1);
 by (auto_tac (claset() addSWrapper record_split_wrapper, 
 	      simpset() addsimps [sysOfAlloc_def, Let_def]));
 qed "surj_sysOfAlloc";
@@ -124,7 +123,7 @@
 Addsimps [inv_sysOfClient_eq];
 
 Goal "surj sysOfClient";
-by (simp_tac (simpset() addsimps [surj_iff, expand_fun_eq, o_def]) 1);
+by (simp_tac (simpset() addsimps [surj_iff, expand_fun_eq, o_apply]) 1);
 by (auto_tac (claset() addSWrapper record_split_wrapper, 
 	      simpset() addsimps [sysOfClient_def]));
 qed "surj_sysOfClient";
@@ -154,7 +153,7 @@
 Addsimps [inv_client_map_eq];
 
 Goal "surj client_map";
-by (simp_tac (simpset() addsimps [surj_iff, expand_fun_eq, o_def]) 1);
+by (simp_tac (simpset() addsimps [surj_iff, expand_fun_eq, o_apply]) 1);
 by (auto_tac (claset() addSWrapper record_split_wrapper, 
 	      simpset() addsimps [client_map_def, non_extra_def]));
 qed "surj_client_map";
@@ -168,77 +167,73 @@
 
 (** 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]));
+Goalw [client_map_def] "fst o client_map = non_extra";
+by (rtac fst_o_funPair 1);
 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]));
+Goalw [client_map_def] "snd o client_map = clientState_u.extra";
+by (rtac snd_o_funPair 1);
 qed "snd_o_client_map";
 Addsimps (make_o_equivs snd_o_client_map);
 
-(** o-simprules for sysOfAlloc **)
+(** o-simprules for sysOfAlloc [MUST BE AUTOMATED] **)
 
 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]));
+	      simpset() addsimps [o_apply, 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]));
+	      simpset() addsimps [sysOfAlloc_def, Let_def, o_apply]));
 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]));
+	      simpset() addsimps [sysOfAlloc_def, Let_def, o_apply]));
 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]));
+	      simpset() addsimps [sysOfAlloc_def, Let_def, o_apply]));
 qed "allocRel_o_sysOfAlloc_eq";
 Addsimps (make_o_equivs allocRel_o_sysOfAlloc_eq);
 
-(** o-simprules for sysOfClient **)
+(** o-simprules for sysOfClient [MUST BE AUTOMATED] **)
 
 Goal "client o sysOfClient = fst";
 by (rtac ext 1);
 by (auto_tac (claset() addSWrapper record_split_wrapper, 
-	      simpset() addsimps [o_def, sysOfClient_def]));
+	      simpset() addsimps [o_apply, 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]));
+	      simpset() addsimps [sysOfClient_def, o_apply]));
 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]));
+	      simpset() addsimps [sysOfClient_def, o_apply]));
 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]));
+	      simpset() addsimps [sysOfClient_def, o_apply]));
 qed "allocRel_o_sysOfClient_eq";
 Addsimps (make_o_equivs allocRel_o_sysOfClient_eq);
 
@@ -302,10 +297,8 @@
 
 AddIffs (Alloc_preserves |> simplify (simpset()) |> list_of_Int);
 
-(** Components lemmas **)
+(** Components lemmas [MUST BE AUTOMATED] **)
 
-(*Alternative is to say that System = Network Join F such that F preserves
-  certain state variables*)
 Goal "Network Join \
 \     ((rename sysOfClient \
 \       (plam x: lessThan Nclients. rename client_map Client)) Join \
@@ -348,15 +341,30 @@
 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, 
+    (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,
 			 inv_inv_eq]) 1);
 by (asm_simp_tac
     (simpset() addsimps [o_def, non_extra_def, guarantees_Int_right]) 1);
 qed "rename_Client_Increasing";
 
+(*The proofs of rename_Client_Bounded and rename_Client_Progress are 
+  similar to the one above.  All require copying out the original Client
+  property.  A forward proof can be constructed as follows:
+
+  Client_Increasing_ask RS
+      (bij_client_map RS rename_rename_guarantees_eq RS iffD2)
+  RS (lift_lift_guarantees_eq RS iffD2)
+  RS guarantees_PLam_I
+  RS (bij_sysOfClient RS rename_rename_guarantees_eq RS iffD2)
+  |> simplify (simpset() addsimps [lift_image_eq_rename, o_def, split_def, 
+				   surj_rename RS surj_range]);
+
+However, the "preserves" property remains to be discharged, and the unfolding
+of "o" and "sub" complicates subsequent reasoning.
+*)
+
 Goal "i < Nclients \
 \     ==> System : Increasing (ask o sub i o client) Int \
 \                  Increasing (rel o sub i o client)";
@@ -365,13 +373,14 @@
 by Auto_tac;
 qed "System_Increasing";
 
+bind_thm ("rename_guarantees_sysOfAlloc_I",
+	  bij_sysOfAlloc RS rename_rename_guarantees_eq RS iffD2);
+
+
 (*Lifting Alloc_Increasing up to the level of systemState*)
 val rename_Alloc_Increasing = 
-    [bij_sysOfAlloc RS rename_rename_guarantees_eq, Alloc_Increasing] MRS iffD2
-     |> simplify
-	 (simpset() addsimps [bij_rename, surj_rename RS surj_range,
-			      bij_image_INT, 
-			      bij_image_Collect_eq, o_def]);
+    Alloc_Increasing RS rename_guarantees_sysOfAlloc_I
+     |> simplify (simpset() addsimps [surj_rename RS surj_range, o_def]);
 
 Goalw [System_def]
      "i < Nclients ==> System : Increasing (sub i o allocGiv)";
@@ -411,22 +420,20 @@
 
 Goal "System : Always (INT i: lessThan Nclients. \
 \                      {s. (giv o sub i o client) s <= (sub i o allocGiv) s})";
-by (auto_tac (claset(), 
-	      simpset() addsimps [Always_INT_distrib]));
+by Auto_tac;
 by (etac (System_Follows_allocGiv RS Follows_Bounded) 1);
 qed "Always_giv_le_allocGiv";
 
 Goal "System : Always (INT i: lessThan Nclients. \
 \                      {s. (sub i o allocAsk) s <= (ask o sub i o client) s})";
-by (auto_tac (claset(), 
-	      simpset() addsimps [Always_INT_distrib]));
+by Auto_tac;
 by (etac (System_Follows_ask RS Follows_Bounded) 1);
 qed "Always_allocAsk_le_ask";
 
 Goal "System : Always (INT i: lessThan 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() addsimps [Always_INT_distrib]));
+	      simpset()));
 qed "Always_allocRel_le_rel";
 
 
@@ -441,22 +448,16 @@
 
 (*Lifting Alloc_safety up to the level of systemState*)
 val rename_Alloc_Safety = 
-    [bij_sysOfAlloc RS rename_rename_guarantees_eq, Alloc_Safety] MRS iffD2
-     |> simplify
-	 (simpset() addsimps [bij_rename, 
-			      bij_image_INT, 
-			      bij_image_Collect_eq, o_def]);
+    Alloc_Safety RS rename_guarantees_sysOfAlloc_I
+     |> 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}";
-by (simp_tac (simpset() addsimps [o_def]) 1);
-by (rtac ([rename_Alloc_Safety, Alloc_component_System] MRS 
-	  component_guaranteesD) 1);
-(*preserves*)
-by (Simp_tac 2);
-by (force_tac (claset(), 
-	       simpset() addsimps [o_simp System_Increasing_allocRel]) 1);
+by (simp_tac (simpset() addsimps [o_apply]) 1);
+by (rtac (rename_Alloc_Safety RS component_guaranteesD) 1);
+by (auto_tac (claset(), 
+	       simpset() addsimps [o_simp System_Increasing_allocRel]));
 qed "System_sum_bounded";
 
 
@@ -518,12 +519,10 @@
 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, 
+    (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);
+			 inv_inv_eq]) 1);
 by (asm_simp_tac (simpset() addsimps [o_def, non_extra_def]) 1);
 qed "rename_Client_Bounded";
 
@@ -539,7 +538,7 @@
 Goal "System : Always {s. ALL i : lessThan Nclients. \
 \                          ALL elt : set ((sub i o allocAsk) s). elt <= NbT}";
 by (auto_tac (claset(), 
-	      simpset() addsimps [Collect_ball_eq, Always_INT_distrib]));
+	      simpset() addsimps [Collect_ball_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()));
@@ -567,13 +566,9 @@
 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, 
+    (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);
+			 bij_imp_bij_inv, inv_inv_eq]) 1);
 by (asm_simp_tac (simpset() addsimps [o_def, non_extra_def,
 				  rewrite_rule [o_def] Client_Progress]) 1);
 qed "rename_Client_Progress";
@@ -589,8 +584,7 @@
 (*Couldn't have just used Auto_tac since the "INT h" must be kept*)
 by (rtac ([rename_Client_Progress,
 	   Client_component_System] MRS component_guaranteesD) 1);
-by (asm_full_simp_tac
-    (simpset() addsimps [System_Increasing_giv]) 2);
+by (asm_full_simp_tac (simpset() addsimps [System_Increasing_giv]) 2);
 by Auto_tac;
 qed "System_Client_Progress";
 
@@ -640,11 +634,8 @@
 
 (*Lifting Alloc_Progress up to the level of systemState*)
 val rename_Alloc_Progress = 
-    [bij_sysOfAlloc RS rename_rename_guarantees_eq, Alloc_Progress] MRS iffD2
-     |> simplify
-	 (simpset() addsimps [bij_rename, surj_rename RS surj_range,
-			      bij_image_INT, bij_is_inj RS image_Int,
-			      bij_image_Collect_eq, o_def]);
+    Alloc_Progress RS rename_guarantees_sysOfAlloc_I
+     |> simplify (simpset() addsimps [o_def]);
 
 (*progress (2), step 9*)
 Goal
@@ -652,12 +643,8 @@
 \           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*)
-by (simp_tac (HOL_ss addsimps [o_def, sub_def]) 1);
-by (rtac ([rename_Alloc_Progress, Alloc_component_System] MRS 
-	  component_guaranteesD) 1);
-(*preserves*)
-by (Simp_tac 2);
-(*the guarantees precondition*)
+by (simp_tac (HOL_ss addsimps [o_apply, sub_def]) 1);
+by (rtac (rename_Alloc_Progress RS component_guaranteesD) 1);
 by (auto_tac (claset(), 
 	      simpset() addsimps [o_simp System_Increasing_allocRel,
 				  o_simp System_Increasing_allocAsk,

--- a/src/HOL/UNITY/Lift_prog.ML	Thu Mar 02 10:26:22 2000 +0100
+++ b/src/HOL/UNITY/Lift_prog.ML	Thu Mar 02 10:29:29 2000 +0100
@@ -360,6 +360,8 @@
 by (simp_tac (simpset() addsimps [lift_def, rename_preserves]) 1);
 qed "lift_preserves_eq";
 
+(*A useful rewrite.  If o, sub have been rewritten out already then can also
+  use it as   rewrite_rule [sub_def, o_def] lift_preserves_sub*)
 Goal "F : preserves snd \
 \     ==> lift i F : preserves (v o sub j o fst) = \
 \         (if i=j then F : preserves (v o fst) else True)";

--- a/src/HOL/UNITY/PPROD.ML	Thu Mar 02 10:26:22 2000 +0100
+++ b/src/HOL/UNITY/PPROD.ML	Thu Mar 02 10:29:29 2000 +0100
@@ -123,6 +123,10 @@
 
 (*** guarantees properties ***)
 
+(*This rule looks unsatisfactory because it refers to "lift".  One must use
+  lift_guarantees_eq_lift_inv to rewrite the first subgoal and
+  something like lift_preserves_sub to rewrite the third.  However there's
+  no obvious way to alternative for the third premise.*)
 Goalw [PLam_def]
     "[| lift i (F i): X guarantees[v] Y;  i : I;  \
 \        ALL j:I. i~=j --> lift j (F j) : preserves v |]  \

--- a/src/HOL/UNITY/Rename.ML	Thu Mar 02 10:26:22 2000 +0100
+++ b/src/HOL/UNITY/Rename.ML	Thu Mar 02 10:29:29 2000 +0100
@@ -52,6 +52,12 @@
 
 Addsimps [Init_rename, Acts_rename];
 
+(*Useful if we don't assume bij h*)
+Goalw [rename_def, rename_act_def, extend_def]
+     "Acts (rename h F) = insert Id (rename_act h `` Acts F)";
+by (asm_simp_tac (simpset() addsimps [export Acts_extend]) 1);
+qed "raw_Acts_rename";
+
 Goalw [rename_act_def, extend_act_def]
      "(s,s') : act ==> (h s, h s') : rename_act h act";
 by Auto_tac;
@@ -117,6 +123,8 @@
 by Auto_tac;
 qed "rename_inv_eq";
 
+(** (rename h) is bijective <=> h is bijective **)
+
 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);
@@ -131,6 +139,30 @@
 by (blast_tac (claset() addIs [bijI, inj_rename, surj_rename]) 1);
 qed "bij_rename";
 
+Goalw [inj_on_def] "inj (rename h) ==> inj h";
+by Auto_tac;
+by (dres_inst_tac [("x", "mk_program ({x}, {})")] spec 1);
+by (dres_inst_tac [("x", "mk_program ({y}, {})")] spec 1);
+by (auto_tac (claset(), 
+	      simpset() addsimps [program_equality_iff, raw_Acts_rename]));
+qed "inj_rename_imp_inj";
+
+Goalw [surj_def] "surj (rename h) ==> surj h";
+by Auto_tac;
+by (dres_inst_tac [("x", "mk_program ({y}, {})")] spec 1);
+by (auto_tac (claset() addSEs [equalityE], 
+	      simpset() addsimps [program_equality_iff, raw_Acts_rename]));
+qed "surj_rename_imp_surj";
+
+Goalw [bij_def] "bij (rename h) ==> bij h";
+by (asm_simp_tac
+    (simpset() addsimps [inj_rename_imp_inj, surj_rename_imp_surj]) 1);
+qed "bij_rename_imp_bij";
+
+Goal "bij (rename h) = bij h";
+by (blast_tac (claset() addIs [bij_rename, bij_rename_imp_bij]) 1);
+qed "bij_rename_iff";
+AddIffs [bij_rename_iff];
 
 (*** the lattice operations ***)
 
@@ -139,10 +171,6 @@
 qed "rename_SKIP";
 Addsimps [rename_SKIP];
 
-Goalw [rename_def] "bij h ==> inj (rename h)";
-by (asm_simp_tac (simpset() addsimps [export inj_extend]) 1);
-qed "inj_rename";
-
 Goalw [rename_def]
      "bij h ==> rename h (F Join G) = rename h F Join rename h G";
 by (asm_simp_tac (simpset() addsimps [export extend_Join]) 1);

--- a/src/HOL/UNITY/UNITY.ML	Thu Mar 02 10:26:22 2000 +0100
+++ b/src/HOL/UNITY/UNITY.ML	Thu Mar 02 10:29:29 2000 +0100
@@ -63,8 +63,7 @@
 Addsimps [Acts_eq, Init_eq];
 
 
-(** The notation of equality for type "program" **)
-
+(** Equality for UNITY programs **)
 
 Goal "mk_program (Init F, Acts F) = F";
 by (cut_inst_tac [("x", "F")] Rep_Program 1);
@@ -84,6 +83,10 @@
 by (auto_tac (claset(), simpset() addsimps [major]));
 qed "program_equalityE";
 
+Goal "(F=G) = (Init F = Init G & Acts F = Acts G)";
+by (blast_tac (claset() addIs [program_equalityI, program_equalityE]) 1);
+qed "program_equality_iff";
+
 Addsimps [surjective_mk_program];