# HG changeset patch
# User paulson
# Date 957950221 -7200
# Node ID f1933a670ae4fe49074ac3ff30c9fb2b4eebe397
# Parent  b06d183df34d991b2c3c56fde24e2b8744c40e80
tidied

diff -r b06d183df34d -r f1933a670ae4 src/HOL/UNITY/Alloc.ML
--- a/src/HOL/UNITY/Alloc.ML	Wed May 10 01:13:43 2000 +0200
+++ b/src/HOL/UNITY/Alloc.ML	Wed May 10 11:17:01 2000 +0200
@@ -4,19 +4,8 @@
     Copyright   1998  University of Cambridge
 
 Specification of Chandy and Charpentier's Allocator
-
-Goal "(plam x: lessThan Nclients. Client) = x";
-Client :: (clientState * ((nat => clientState) * 'b)) program
 *)
 
-(***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";
-
-
 AddIs [impOfSubs subset_preserves_o];
 Addsimps [funPair_o_distrib];
 Addsimps [Always_INT_distrib];
@@ -71,9 +60,16 @@
 
 (*** bijectivity of sysOfAlloc [MUST BE AUTOMATED] ***)
 
+val record_auto_tac =
+    auto_tac (claset() addIs [ext] addSWrapper record_split_wrapper, 
+	      simpset() addsimps [sysOfAlloc_def, sysOfClient_def,
+				  client_map_def, non_extra_def, funPair_def,
+				  o_apply, Let_def]);
+
+
 Goalw [sysOfAlloc_def, Let_def] "inj sysOfAlloc";
 by (rtac injI 1);
-by (auto_tac (claset() addSWrapper record_split_wrapper, simpset()));
+by record_auto_tac;
 qed "inj_sysOfAlloc";
 AddIffs [inj_sysOfAlloc];
 
@@ -84,15 +80,13 @@
 \               allocRel = allocRel s,   \
 \               allocState_u.extra = (client s, extra s) |)";
 by (rtac (inj_sysOfAlloc RS inv_f_eq) 1);
-by (auto_tac (claset() addSWrapper record_split_wrapper, 
-	      simpset() addsimps [sysOfAlloc_def, Let_def]));
+by record_auto_tac;
 qed "inv_sysOfAlloc_eq";
 Addsimps [inv_sysOfAlloc_eq];
 
 Goal "surj sysOfAlloc";
 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]));
+by record_auto_tac;
 qed "surj_sysOfAlloc";
 AddIffs [surj_sysOfAlloc];
 
@@ -106,7 +100,7 @@
 
 Goalw [sysOfClient_def] "inj sysOfClient";
 by (rtac injI 1);
-by (auto_tac (claset() addSWrapper record_split_wrapper, simpset()));
+by record_auto_tac;
 qed "inj_sysOfClient";
 AddIffs [inj_sysOfClient];
 
@@ -117,15 +111,13 @@
 \                allocRel = allocRel s, \
 \                allocState_u.extra = systemState.extra s|) )";
 by (rtac (inj_sysOfClient RS inv_f_eq) 1);
-by (auto_tac (claset() addSWrapper record_split_wrapper, 
-	      simpset() addsimps [sysOfClient_def]));
+by record_auto_tac;
 qed "inv_sysOfClient_eq";
 Addsimps [inv_sysOfClient_eq];
 
 Goal "surj sysOfClient";
 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]));
+by record_auto_tac;
 qed "surj_sysOfClient";
 AddIffs [surj_sysOfClient];
 
@@ -137,9 +129,8 @@
 
 (*** bijectivity of client_map ***)
 
-Goal "inj client_map";
-by (auto_tac (claset() addSWrapper record_split_wrapper, 
-	      simpset() addsimps [client_map_def, non_extra_def, inj_on_def]));
+Goalw [inj_on_def] "inj client_map";
+by record_auto_tac;
 qed "inj_client_map";
 AddIffs [inj_client_map];
 
@@ -147,15 +138,13 @@
 \            (%(x,y).(|giv = giv x, ask = ask x, rel = rel x, \
 \                      clientState_u.extra = y|)) s";
 by (rtac (inj_client_map RS inv_f_eq) 1);
-by (auto_tac (claset() addSWrapper record_split_wrapper, 
-      simpset() addsimps [client_map_def, funPair_def, non_extra_def]));
+by record_auto_tac;
 qed "inv_client_map_eq";
 Addsimps [inv_client_map_eq];
 
 Goal "surj client_map";
 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]));
+by record_auto_tac;
 qed "surj_client_map";
 AddIffs [surj_client_map];
 
@@ -180,60 +169,44 @@
 (** 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_apply, sysOfAlloc_def, Let_def]));
+by record_auto_tac;
 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_apply]));
+by record_auto_tac;
 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_apply]));
+by record_auto_tac;
 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_apply]));
+by record_auto_tac;
 qed "allocRel_o_sysOfAlloc_eq";
 Addsimps (make_o_equivs allocRel_o_sysOfAlloc_eq);
 
 (** 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_apply, sysOfClient_def]));
+by record_auto_tac;
 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_apply]));
+by record_auto_tac;
 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_apply]));
+by record_auto_tac;
 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_apply]));
+by record_auto_tac;
 qed "allocRel_o_sysOfClient_eq";
 Addsimps (make_o_equivs allocRel_o_sysOfClient_eq);