# HG changeset patch
# User paulson
# Date 964195296 -7200
# Node ID aad13b59b8d9351e7862a049e71f1e7daeba04b9
# Parent  480a1b40fdd6980e3dcd053e127eedcf6e9374fc
much tidying in connection with the 2nd UNITY paper

diff -r 480a1b40fdd6 -r aad13b59b8d9 src/HOL/UNITY/Alloc.ML
--- a/src/HOL/UNITY/Alloc.ML	Fri Jul 21 17:46:43 2000 +0200
+++ b/src/HOL/UNITY/Alloc.ML	Fri Jul 21 18:01:36 2000 +0200
@@ -49,7 +49,7 @@
 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,
+				  client_map_def, non_dummy_def, funPair_def,
 				  o_apply, Let_def]);
 
 
@@ -64,7 +64,7 @@
 \            (| allocGiv = allocGiv s,   \
 \               allocAsk = allocAsk s,   \
 \               allocRel = allocRel s,   \
-\               allocState_u.extra = (client s, extra s) |)";
+\               allocState_d.dummy = (client s, dummy s) |)";
 by (rtac (inj_sysOfAlloc RS inv_f_eq) 1);
 by record_auto_tac;
 qed "inv_sysOfAlloc_eq";
@@ -95,7 +95,7 @@
 \             (| allocGiv = allocGiv s, \
 \                allocAsk = allocAsk s, \
 \                allocRel = allocRel s, \
-\                allocState_u.extra = systemState.extra s|) )";
+\                allocState_d.dummy = systemState.dummy s|) )";
 by (rtac (inj_sysOfClient RS inv_f_eq) 1);
 by record_auto_tac;
 qed "inv_sysOfClient_eq";
@@ -122,7 +122,7 @@
 
 Goal "!!s. inv client_map s = \
 \            (%(x,y).(|giv = giv x, ask = ask x, rel = rel x, \
-\                      clientState_u.extra = y|)) s";
+\                      clientState_d.dummy = y|)) s";
 by (rtac (inj_client_map RS inv_f_eq) 1);
 by record_auto_tac;
 qed "inv_client_map_eq";
@@ -142,19 +142,19 @@
 
 (** o-simprules for client_map **)
 
-Goalw [client_map_def] "fst o client_map = non_extra";
+Goalw [client_map_def] "fst o client_map = non_dummy";
 by (rtac fst_o_funPair 1);
 qed "fst_o_client_map";
 Addsimps (make_o_equivs fst_o_client_map);
 
-Goalw [client_map_def] "snd o client_map = clientState_u.extra";
+Goalw [client_map_def] "snd o client_map = clientState_d.dummy";
 by (rtac snd_o_funPair 1);
 qed "snd_o_client_map";
 Addsimps (make_o_equivs snd_o_client_map);
 
 (** o-simprules for sysOfAlloc [MUST BE AUTOMATED] **)
 
-Goal "client o sysOfAlloc = fst o allocState_u.extra ";
+Goal "client o sysOfAlloc = fst o allocState_d.dummy ";
 by record_auto_tac;
 qed "client_o_sysOfAlloc";
 Addsimps (make_o_equivs client_o_sysOfAlloc);
@@ -220,13 +220,13 @@
 
 val [Client_Increasing_ask, Client_Increasing_rel,
      Client_Bounded, Client_Progress, Client_preserves_giv,
-     Client_preserves_extra] =
+     Client_preserves_dummy] =
         Client_Spec 
           |> simplify (simpset() addsimps [guarantees_Int_right]) 
           |> list_of_Int;
 
 AddIffs [Client_Increasing_ask, Client_Increasing_rel, Client_Bounded,
-	 Client_preserves_giv, Client_preserves_extra];
+	 Client_preserves_giv, Client_preserves_dummy];
 
 
 (*Network : <unfolded specification> *)
@@ -319,7 +319,7 @@
 			     bij_imp_bij_inv, surj_rename RS surj_range,
 			     inv_inv_eq]) 1,
     asm_simp_tac
-        (simpset() addsimps [o_def, non_extra_def, guarantees_Int_right]) 1];
+        (simpset() addsimps [o_def, non_dummy_def, guarantees_Int_right]) 1];
 
 
 (*Lifting Client_Increasing to systemState*)
@@ -379,7 +379,7 @@
 by (auto_tac (claset() addSIs [Network_Giv RS component_guaranteesD, 
 		 rename_Alloc_Increasing RS component_guaranteesD], 
 	      simpset()));
-by (ALLGOALS (simp_tac (simpset() addsimps [o_def, non_extra_def])));
+by (ALLGOALS (simp_tac (simpset() addsimps [o_def, non_dummy_def])));
 by (auto_tac
     (claset() addSIs [rename_Alloc_Increasing RS component_guaranteesD],
      simpset()));
@@ -406,14 +406,16 @@
 
 (*** Proof of the safety property (1) ***)
 
-(*safety (1), step 1 is System_Increasing_rel*)
+(*safety (1), step 1 is System_Follows_rel*)
 
 (*safety (1), step 2*)
-Goal "i < Nclients ==> System : Increasing (sub i o allocRel)";
-by (etac (System_Follows_rel RS Follows_Increasing1) 1);
-qed "System_Increasing_allocRel";
+(* i < Nclients ==> System : Increasing (sub i o allocRel) *)
+bind_thm ("System_Increasing_allocRel", 
+          System_Follows_rel RS Follows_Increasing1);
 
-(*Lifting Alloc_safety up to the level of systemState*)
+(*Lifting Alloc_safety up to the level of systemState.
+  Simplififying with o_def gets rid of the translations but it unfortunately
+  gets rid of the other "o"s too.*)
 val rename_Alloc_Safety = 
     Alloc_Safety RS rename_guarantees_sysOfAlloc_I
      |> simplify (simpset() addsimps [o_def]);
@@ -427,7 +429,7 @@
 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]));
+              simpset() addsimps [o_simp System_Increasing_allocRel]));
 qed "System_sum_bounded";
 
 
@@ -464,19 +466,14 @@
 
 (*** Proof of the progress property (2) ***)
 
-(*Now there are proofs identical to System_Increasing_rel and
-  System_Increasing_allocRel: tactics needed!*)
-
-(*progress (2), step 1 is System_Increasing_ask and System_Increasing_rel*)
+(*progress (2), step 1 is System_Follows_ask and System_Follows_rel*)
 
 (*progress (2), step 2; see also System_Increasing_allocRel*)
-Goal "i < Nclients ==> System : Increasing (sub i o allocAsk)";
-by (etac (System_Follows_ask RS Follows_Increasing1) 1);
-qed "System_Increasing_allocAsk";
+(* i < Nclients ==> System : Increasing (sub i o allocAsk) *)
+bind_thm ("System_Increasing_allocAsk",
+          System_Follows_ask RS Follows_Increasing1);
 
-(*progress (2), step 3*)
-(*All this trouble just to lift "Client_Bounded" to systemState
-  (though it is similar to that for Client_Increasing*)
+(*progress (2), step 3: lifting "Client_Bounded" to systemState*)
 Goal "i : I \
 \   ==> rename sysOfClient (plam x: I. rename client_map Client) : \
 \         UNIV \
@@ -498,10 +495,9 @@
 qed "Collect_all_imp_eq";
 
 (*progress (2), step 4*)
-Goal "System : Always {s. ALL i. i<Nclients --> \
-\                         (ALL elt : set ((sub i o allocAsk) s). elt <= NbT)}";
-by (auto_tac (claset(), 
-	      simpset() addsimps [Collect_all_imp_eq]));
+Goal "System : Always {s. ALL i<Nclients. \
+\                         ALL elt : set ((sub i o allocAsk) s). elt <= NbT}";
+by (auto_tac (claset(),  simpset() addsimps [Collect_all_imp_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()));
@@ -510,9 +506,9 @@
 (*progress (2), step 5 is System_Increasing_allocGiv*)
 
 (*progress (2), step 6*)
-Goal "i < Nclients ==> System : Increasing (giv o sub i o client)";
-by (etac (System_Follows_allocGiv RS Follows_Increasing1) 1);
-qed "System_Increasing_giv";
+(* i < Nclients ==> System : Increasing (giv o sub i o client) *)
+bind_thm ("System_Increasing_giv",
+          System_Follows_allocGiv RS Follows_Increasing1);
 
 
 Goal "i: I \
@@ -523,8 +519,7 @@
 \                           h pfixGe (ask o sub i o client) s}  \
 \                 LeadsTo {s. tokens h <= (tokens o rel o sub i o client) s})";
 by rename_client_map_tac;
-by (asm_simp_tac
-    (simpset() addsimps [rewrite_rule [o_def] Client_Progress]) 1);
+by (asm_simp_tac (simpset() addsimps [o_simp Client_Progress]) 1);
 qed "rename_Client_Progress";
 
 
@@ -538,8 +533,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 Auto_tac;
+by (auto_tac (claset(), simpset() addsimps [System_Increasing_giv]));  
 qed "System_Client_Progress";
 
 (*Concludes
@@ -609,13 +603,10 @@
 
 (*progress (2), step 10 (final result!) *)
 Goalw [system_progress_def] "System : system_progress";
-by (Clarify_tac 1);
-by (rtac LeadsTo_Trans 1);
-by (etac (System_Follows_allocGiv RS Follows_LeadsTo_pfixLe) 2);
-by (rtac LeadsTo_Trans 1);
-by (cut_facts_tac [System_Alloc_Progress] 2);
-by (Blast_tac 2);
-by (etac (System_Follows_ask RS Follows_LeadsTo) 1);
+by (cut_facts_tac [System_Alloc_Progress] 1);
+by (blast_tac (claset() addIs [LeadsTo_Trans, 
+                System_Follows_allocGiv RS Follows_LeadsTo_pfixLe, 
+                System_Follows_ask RS Follows_LeadsTo]) 1);
 qed "System_Progress";
 
 
diff -r 480a1b40fdd6 -r aad13b59b8d9 src/HOL/UNITY/Alloc.thy
--- a/src/HOL/UNITY/Alloc.thy	Fri Jul 21 17:46:43 2000 +0200
+++ b/src/HOL/UNITY/Alloc.thy	Fri Jul 21 18:01:36 2000 +0200
@@ -15,19 +15,19 @@
   ask :: nat list   (*client's OUTPUT history: tokens REQUESTED*)
   rel :: nat list   (*client's OUTPUT history: tokens RELEASED*)
 
-record 'a clientState_u =
+record 'a clientState_d =
   clientState +
-  extra :: 'a       (*dummy field for new variables*)
+  dummy :: 'a       (*dummy field for new variables*)
 
 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|)"
+  non_dummy :: 'a clientState_d => clientState
+    "non_dummy 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"
+  client_map :: "'a clientState_d => clientState*'a"
+    "client_map == funPair non_dummy dummy"
 
   
 record allocState =
@@ -35,14 +35,14 @@
   allocAsk :: nat => nat list   (*INPUT: allocator's copy of "ask" for i*)
   allocRel :: nat => nat list   (*INPUT: allocator's copy of "rel" for i*)
 
-record 'a allocState_u =
+record 'a allocState_d =
   allocState +
-  extra    :: 'a                (*dummy field for new variables*)
+  dummy    :: 'a                (*dummy field for new variables*)
 
 record 'a systemState =
   allocState +
   client :: nat => clientState  (*states of all clients*)
-  extra  :: 'a                  (*dummy field for new variables*)
+  dummy  :: 'a                  (*dummy field for new variables*)
 
 
 constdefs
@@ -68,19 +68,19 @@
 (** Client specification (required) ***)
 
   (*spec (3)*)
-  client_increasing :: 'a clientState_u program set
+  client_increasing :: 'a clientState_d program set
     "client_increasing ==
          UNIV guarantees[funPair rel ask]
          Increasing ask Int Increasing rel"
 
   (*spec (4)*)
-  client_bounded :: 'a clientState_u program set
+  client_bounded :: 'a clientState_d program set
     "client_bounded ==
          UNIV guarantees[ask]
          Always {s. ALL elt : set (ask s). elt <= NbT}"
 
   (*spec (5)*)
-  client_progress :: 'a clientState_u program set
+  client_progress :: 'a clientState_d program set
     "client_progress ==
 	 Increasing giv
 	 guarantees[funPair rel ask]
@@ -88,24 +88,24 @@
 		 LeadsTo {s. tokens h <= (tokens o rel) s})"
 
   (*spec: preserves part*)
-    client_preserves :: 'a clientState_u program set
-    "client_preserves == preserves (funPair giv clientState_u.extra)"
+    client_preserves :: 'a clientState_d program set
+    "client_preserves == preserves (funPair giv clientState_d.dummy)"
 
-  client_spec :: 'a clientState_u program set
+  client_spec :: 'a clientState_d program set
     "client_spec == client_increasing Int client_bounded Int client_progress
                     Int client_preserves"
 
 (** Allocator specification (required) ***)
 
   (*spec (6)*)
-  alloc_increasing :: 'a allocState_u program set
+  alloc_increasing :: 'a allocState_d program set
     "alloc_increasing ==
 	 UNIV
          guarantees[allocGiv]
 	 (INT i : lessThan Nclients. Increasing (sub i o allocGiv))"
 
   (*spec (7)*)
-  alloc_safety :: 'a allocState_u program set
+  alloc_safety :: 'a allocState_d program set
     "alloc_safety ==
 	 (INT i : lessThan Nclients. Increasing (sub i o allocRel))
          guarantees[allocGiv]
@@ -113,13 +113,13 @@
          <= NbT + setsum(%i.(tokens o sub i o allocRel)s) (lessThan Nclients)}"
 
   (*spec (8)*)
-  alloc_progress :: 'a allocState_u program set
+  alloc_progress :: 'a allocState_d program set
     "alloc_progress ==
 	 (INT i : lessThan Nclients. Increasing (sub i o allocAsk) Int
 	                             Increasing (sub i o allocRel))
          Int
-         Always {s. ALL i. i<Nclients -->
-		     (ALL elt : set ((sub i o allocAsk) s). elt <= NbT)}
+         Always {s. ALL i<Nclients.
+		     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}
@@ -139,11 +139,11 @@
     looked at.*)
 
   (*spec: preserves part*)
-    alloc_preserves :: 'a allocState_u program set
+    alloc_preserves :: 'a allocState_d program set
     "alloc_preserves == preserves (funPair allocRel
-				   (funPair allocAsk allocState_u.extra))"
+				   (funPair allocAsk allocState_d.dummy))"
   
-  alloc_spec :: 'a allocState_u program set
+  alloc_spec :: 'a allocState_d program set
     "alloc_spec == alloc_increasing Int alloc_safety Int alloc_progress Int
                    alloc_preserves"
 
@@ -182,25 +182,25 @@
 
 
 (** State mappings **)
-  sysOfAlloc :: "((nat => clientState) * 'a) allocState_u => 'a systemState"
-    "sysOfAlloc == %s. let (cl,xtr) = allocState_u.extra s
+  sysOfAlloc :: "((nat => clientState) * 'a) allocState_d => 'a systemState"
+    "sysOfAlloc == %s. let (cl,xtr) = allocState_d.dummy s
                        in (| allocGiv = allocGiv s,
 			     allocAsk = allocAsk s,
 			     allocRel = allocRel s,
 			     client   = cl,
-			     extra    = xtr|)"
+			     dummy    = xtr|)"
 
 
-  sysOfClient :: "(nat => clientState) * 'a allocState_u => 'a systemState"
+  sysOfClient :: "(nat => clientState) * 'a allocState_d => 'a systemState"
     "sysOfClient == %(cl,al). (| allocGiv = allocGiv al,
 			         allocAsk = allocAsk al,
 			         allocRel = allocRel al,
 			         client   = cl,
-			         systemState.extra = allocState_u.extra al|)"
+			         systemState.dummy = allocState_d.dummy al|)"
 
 consts 
-    Alloc   :: 'a allocState_u program
-    Client  :: 'a clientState_u program
+    Alloc   :: 'a allocState_d program
+    Client  :: 'a clientState_d program
     Network :: 'a systemState program
     System  :: 'a systemState program
   
@@ -219,8 +219,8 @@
 (**
 locale System =
   fixes 
-    Alloc   :: 'a allocState_u program
-    Client  :: 'a clientState_u program
+    Alloc   :: 'a allocState_d program
+    Client  :: 'a clientState_d program
     Network :: 'a systemState program
     System  :: 'a systemState program
 
diff -r 480a1b40fdd6 -r aad13b59b8d9 src/HOL/UNITY/AllocImpl.ML
--- a/src/HOL/UNITY/AllocImpl.ML	Fri Jul 21 17:46:43 2000 +0200
+++ b/src/HOL/UNITY/AllocImpl.ML	Fri Jul 21 18:01:36 2000 +0200
@@ -4,9 +4,6 @@
     Copyright   2000  University of Cambridge
 
 Implementation of a multiple-client allocator from a single-client allocator
-
-add_path "../Induct";
-time_use_thy "AllocImpl";
 *)
 
 AddIs [impOfSubs subset_preserves_o];
diff -r 480a1b40fdd6 -r aad13b59b8d9 src/HOL/UNITY/AllocImpl.thy
--- a/src/HOL/UNITY/AllocImpl.thy	Fri Jul 21 17:46:43 2000 +0200
+++ b/src/HOL/UNITY/AllocImpl.thy	Fri Jul 21 18:01:36 2000 +0200
@@ -4,9 +4,6 @@
     Copyright   1998  University of Cambridge
 
 Implementation of a multiple-client allocator from a single-client allocator
-
-add_path "../Induct";
-with_path "../Induct" time_use_thy "AllocImpl";
 *)
 
 AllocImpl = AllocBase + Follows + PPROD + 
@@ -20,38 +17,38 @@
   Out  :: 'b list          (*merge's OUTPUT history: merged items*)
   iOut :: nat list         (*merge's OUTPUT history: origins of merged items*)
 
-record ('a,'b) merge_u =
+record ('a,'b) merge_d =
   'b merge +
-  extra :: 'a       (*dummy field for new variables*)
+  dummy :: 'a       (*dummy field for new variables*)
 
 constdefs
-  non_extra :: ('a,'b) merge_u => 'b merge
-    "non_extra s == (|In = In s, Out = Out s, iOut = iOut s|)"
+  non_dummy :: ('a,'b) merge_d => 'b merge
+    "non_dummy s == (|In = In s, Out = Out s, iOut = iOut s|)"
 
 record 'b distr =
   In  :: 'b list          (*items to distribute*)
   iIn :: nat list         (*destinations of items to distribute*)
   Out :: nat => 'b list   (*distributed items*)
 
-record ('a,'b) distr_u =
+record ('a,'b) distr_d =
   'b distr +
-  extra :: 'a       (*dummy field for new variables*)
+  dummy :: 'a       (*dummy field for new variables*)
 
 record allocState =
   giv :: nat list   (*OUTPUT history: source of tokens*)
   ask :: nat list   (*INPUT: tokens requested from allocator*)
   rel :: nat list   (*INPUT: tokens released to allocator*)
 
-record 'a allocState_u =
+record 'a allocState_d =
   allocState +
-  extra    :: 'a                (*dummy field for new variables*)
+  dummy    :: 'a                (*dummy field for new variables*)
 
 record 'a systemState =
   allocState +
   mergeRel :: nat merge
   mergeAsk :: nat merge
   distr    :: nat distr
-  extra    :: 'a                  (*dummy field for new variables*)
+  dummy    :: 'a                  (*dummy field for new variables*)
 
 
 constdefs
@@ -59,25 +56,25 @@
 (** Merge specification (the number of inputs is Nclients) ***)
 
   (*spec (10)*)
-  merge_increasing :: ('a,'b) merge_u program set
+  merge_increasing :: ('a,'b) merge_d program set
     "merge_increasing ==
          UNIV guarantees[funPair merge.Out merge.iOut]
          (Increasing merge.Out) Int (Increasing merge.iOut)"
 
   (*spec (11)*)
-  merge_eqOut :: ('a,'b) merge_u program set
+  merge_eqOut :: ('a,'b) merge_d program set
     "merge_eqOut ==
          UNIV guarantees[funPair merge.Out merge.iOut]
          Always {s. length (merge.Out s) = length (merge.iOut s)}"
 
   (*spec (12)*)
-  merge_bounded :: ('a,'b) merge_u program set
+  merge_bounded :: ('a,'b) merge_d program set
     "merge_bounded ==
          UNIV guarantees[merge.iOut]
          Always {s. ALL elt : set (merge.iOut s). elt < Nclients}"
 
   (*spec (13)*)
-  merge_follows :: ('a,'b) merge_u program set
+  merge_follows :: ('a,'b) merge_d program set
     "merge_follows ==
 	 (INT i : lessThan Nclients. Increasing (sub i o merge.In))
 	 guarantees[funPair merge.Out merge.iOut]
@@ -87,17 +84,17 @@
 	  Fols (sub i o merge.In))"
 
   (*spec: preserves part*)
-    merge_preserves :: ('a,'b) merge_u program set
-    "merge_preserves == preserves (funPair merge.In merge_u.extra)"
+    merge_preserves :: ('a,'b) merge_d program set
+    "merge_preserves == preserves (funPair merge.In merge_d.dummy)"
 
-  merge_spec :: ('a,'b) merge_u program set
+  merge_spec :: ('a,'b) merge_d program set
     "merge_spec == merge_increasing Int merge_eqOut Int merge_bounded Int
                    merge_follows Int merge_preserves"
 
 (** Distributor specification (the number of outputs is Nclients) ***)
 
   (*spec (14)*)
-  distr_follows :: ('a,'b) distr_u program set
+  distr_follows :: ('a,'b) distr_d program set
     "distr_follows ==
 	 Increasing distr.In Int Increasing distr.iIn Int
 	 Always {s. ALL elt : set (distr.iIn s). elt < Nclients}
@@ -111,17 +108,17 @@
 (** Single-client allocator specification (required) ***)
 
   (*spec (18)*)
-  alloc_increasing :: 'a allocState_u program set
+  alloc_increasing :: 'a allocState_d program set
     "alloc_increasing == UNIV guarantees[giv] Increasing giv"
 
   (*spec (19)*)
-  alloc_safety :: 'a allocState_u program set
+  alloc_safety :: 'a allocState_d program set
     "alloc_safety ==
 	 Increasing rel
          guarantees[giv] Always {s. tokens (giv s) <= NbT + tokens (rel s)}"
 
   (*spec (20)*)
-  alloc_progress :: 'a allocState_u program set
+  alloc_progress :: 'a allocState_d program set
     "alloc_progress ==
 	 Increasing ask Int Increasing rel Int
          Always {s. ALL elt : set (ask s). elt <= NbT}
@@ -133,11 +130,11 @@
 	     (INT h. {s. h <= ask s} LeadsTo {s. h pfixLe giv s})"
 
   (*spec: preserves part*)
-    alloc_preserves :: 'a allocState_u program set
+    alloc_preserves :: 'a allocState_d program set
     "alloc_preserves == preserves (funPair rel
-				   (funPair ask allocState_u.extra))"
+				   (funPair ask allocState_d.dummy))"
   
-  alloc_spec :: 'a allocState_u program set
+  alloc_spec :: 'a allocState_d program set
     "alloc_spec == alloc_increasing Int alloc_safety Int alloc_progress Int
                    alloc_preserves"
 
@@ -177,26 +174,27 @@
 
 
     (** State mappings **)
-      sysOfAlloc :: "((nat => merge) * 'a) allocState_u => 'a systemState"
-	"sysOfAlloc == %s. let (cl,xtr) = allocState_u.extra s
+      sysOfAlloc :: "((nat => merge) * 'a) allocState_d => 'a systemState"
+	"sysOfAlloc == %s. let (cl,xtr) = allocState_d.dummy s
 			   in (| giv = giv s,
 				 ask = ask s,
 				 rel = rel s,
 				 client   = cl,
-				 extra    = xtr|)"
+				 dummy    = xtr|)"
 
 
-      sysOfClient :: "(nat => merge) * 'a allocState_u => 'a systemState"
+      sysOfClient :: "(nat => merge) * 'a allocState_d => 'a systemState"
 	"sysOfClient == %(cl,al). (| giv = giv al,
 				     ask = ask al,
 				     rel = rel al,
 				     client   = cl,
-				     systemState.extra = allocState_u.extra al|)"
+				     systemState.dummy = allocState_d.dummy al|)"
 ****)
 
 consts 
-    Alloc  :: 'a allocState_u program
-    Merge  :: ('a,'b) merge_u program
+    Alloc  :: 'a allocState_d program
+    Merge  :: ('a,'b) merge_d program
+
 (*    
     Network :: 'a systemState program
     System  :: 'a systemState program
@@ -205,17 +203,9 @@
 rules
     Alloc   "Alloc   : alloc_spec"
     Merge  "Merge  : merge_spec"
+
 (**    Network "Network : network_spec"**)
 
 
 
-(**
-defs
-    System_def
-      "System == rename sysOfAlloc Alloc Join Network Join
-                 (rename sysOfMerge
-		  (plam x: lessThan Nclients. rename merge_map Merge))"
-**)
-
-
 end
diff -r 480a1b40fdd6 -r aad13b59b8d9 src/HOL/UNITY/Client.ML
--- a/src/HOL/UNITY/Client.ML	Fri Jul 21 17:46:43 2000 +0200
+++ b/src/HOL/UNITY/Client.ML	Fri Jul 21 18:01:36 2000 +0200
@@ -15,11 +15,9 @@
 (*Safety property 1: ask, rel are increasing*)
 Goal "Client: UNIV guarantees[funPair rel ask] \
 \             Increasing ask Int Increasing rel";
-by (safe_tac (claset() addSIs [guaranteesI,increasing_imp_Increasing]));
 by (auto_tac
-    (claset(),
-     simpset() addsimps [impOfSubs preserves_subset_increasing,
-			 Join_increasing]));
+    (claset() addSIs [increasing_imp_Increasing],
+     simpset() addsimps [guar_def, impOfSubs preserves_subset_increasing]));
 by (auto_tac (claset(), simpset() addsimps [increasing_def]));
 by (ALLGOALS constrains_tac);
 by Auto_tac;
@@ -70,9 +68,7 @@
 
 Goal "[| Client Join G : Increasing giv;  G : preserves rel |] \
 \     ==> Client Join G : Always {s. rel s <= giv s}";
-by (rtac AlwaysI 1);
-by (rtac Join_Stable_rel_le_giv 2);
-by Auto_tac;
+by (force_tac (claset() addIs [AlwaysI, Join_Stable_rel_le_giv], simpset()) 1);
 qed "Join_Always_rel_le_giv";
 
 Goal "Client : transient {s. rel s = k & k<h & h <= giv s & h pfixGe ask s}";
@@ -146,12 +142,12 @@
 
 (*This shows that the Client won't alter other variables in any state
   that it is combined with*)
-Goal "Client : preserves extra";
+Goal "Client : preserves dummy";
 by (rewtac preserves_def);
 by Auto_tac;
 by (constrains_tac 1);
 by Auto_tac;
-qed "client_preserves_extra";
+qed "client_preserves_dummy";
 
 
 (** Obsolete lemmas from first version of the Client **)
diff -r 480a1b40fdd6 -r aad13b59b8d9 src/HOL/UNITY/Client.thy
--- a/src/HOL/UNITY/Client.thy	Fri Jul 21 17:46:43 2000 +0200
+++ b/src/HOL/UNITY/Client.thy	Fri Jul 21 18:01:36 2000 +0200
@@ -17,9 +17,9 @@
   rel :: tokbag list   (*output history: tokens released*)
   tok :: tokbag	       (*current token request*)
 
-record 'a state_u =
+record 'a state_d =
   state +  
-  extra :: 'a          (*new variables*)
+  dummy :: 'a          (*new variables*)
 
 
 (*Array indexing is translated to list indexing as A[n] == A!(n-1). *)
@@ -28,7 +28,7 @@
   
   (** Release some tokens **)
   
-  rel_act :: "('a state_u * 'a state_u) set"
+  rel_act :: "('a state_d * 'a state_d) set"
     "rel_act == {(s,s').
 		  EX nrel. nrel = size (rel s) &
 		           s' = s (| rel := rel s @ [giv s!nrel] |) &
@@ -40,24 +40,24 @@
   (** Including s'=s suppresses fairness, allowing the non-trivial part
       of the action to be ignored **)
 
-  tok_act :: "('a state_u * 'a state_u) set"
+  tok_act :: "('a state_d * 'a state_d) set"
      "tok_act == {(s,s'). s'=s | s' = s (|tok := Suc (tok s mod NbT) |)}"
   
-  ask_act :: "('a state_u * 'a state_u) set"
+  ask_act :: "('a state_d * 'a state_d) set"
     "ask_act == {(s,s'). s'=s |
 		         (s' = s (|ask := ask s @ [tok s]|))}"
 
-  Client :: 'a state_u program
+  Client :: 'a state_d program
     "Client == mk_program ({s. tok s : atMost NbT &
 		               giv s = [] & ask s = [] & rel s = []},
 			   {rel_act, tok_act, ask_act})"
 
   (*Maybe want a special theory section to declare such maps*)
-  non_extra :: 'a state_u => state
-    "non_extra s == (|giv = giv s, ask = ask s, rel = rel s, tok = tok s|)"
+  non_dummy :: 'a state_d => state
+    "non_dummy s == (|giv = giv s, ask = ask s, rel = rel s, tok = tok s|)"
 
   (*Renaming map to put a Client into the standard form*)
-  client_map :: "'a state_u => state*'a"
-    "client_map == funPair non_extra extra"
+  client_map :: "'a state_d => state*'a"
+    "client_map == funPair non_dummy dummy"
 
 end
diff -r 480a1b40fdd6 -r aad13b59b8d9 src/HOL/UNITY/Comp.ML
--- a/src/HOL/UNITY/Comp.ML	Fri Jul 21 17:46:43 2000 +0200
+++ b/src/HOL/UNITY/Comp.ML	Fri Jul 21 18:01:36 2000 +0200
@@ -100,9 +100,9 @@
 by (Force_tac 1);
 qed "preserves_imp_eq";
 
-Goal "(F Join G : preserves v) = (F : preserves v & G : preserves v)";
-by (simp_tac (simpset() addsimps [Join_stable, preserves_def]) 1);
-by (Blast_tac 1);
+Goalw [preserves_def]
+     "(F Join G : preserves v) = (F : preserves v & G : preserves v)";
+by Auto_tac;
 qed "Join_preserves";
 
 Goal "(JOIN I F : preserves v) = (ALL i:I. F i : preserves v)";
@@ -173,7 +173,7 @@
 Goal "[| F : stable {s. P (v s) (w s)};   \
 \        G : preserves v;  G : preserves w |]               \
 \     ==> F Join G : stable {s. P (v s) (w s)}";
-by (asm_simp_tac (simpset() addsimps [Join_stable]) 1);
+by (Asm_simp_tac 1);
 by (subgoal_tac "G: preserves (funPair v w)" 1);
 by (Asm_simp_tac 2);
 by (dres_inst_tac [("P1", "split ?Q")]  
@@ -186,7 +186,7 @@
 \     ==> F Join G : Stable {s. v s <= w s}";
 by (auto_tac (claset(), 
 	      simpset() addsimps [stable_def, Stable_def, Increasing_def, 
-		    Constrains_def, Join_constrains, all_conj_distrib]));
+				  Constrains_def, all_conj_distrib]));
 by (blast_tac (claset() addIs [constrains_weaken]) 1);
 (*The G case remains*)
 by (auto_tac (claset(), 
diff -r 480a1b40fdd6 -r aad13b59b8d9 src/HOL/UNITY/ELT.ML
--- a/src/HOL/UNITY/ELT.ML	Fri Jul 21 17:46:43 2000 +0200
+++ b/src/HOL/UNITY/ELT.ML	Fri Jul 21 18:01:36 2000 +0200
@@ -316,8 +316,7 @@
 by (auto_tac (claset(),
 	      simpset() addsimps [Diff_eq_empty_iff RS iffD2,
 				  Int_Diff, ensures_def,
-				  givenBy_eq_Collect, Join_stable,
-				  Join_constrains, Join_transient]));
+				  givenBy_eq_Collect, Join_transient]));
 by (blast_tac (claset() addIs [transient_strengthen]) 3);
 by (ALLGOALS (dres_inst_tac [("P1","P")] (impOfSubs preserves_subset_stable)));
 by (rewtac stable_def);
@@ -335,8 +334,7 @@
 by (case_tac "A <= B" 1);
 by (etac subset_imp_ensures 1);
 by (auto_tac (claset() addIs [constrains_weaken],
-              simpset() addsimps [stable_def, ensures_def, 
-                                  Join_constrains, Join_transient]));
+              simpset() addsimps [stable_def, ensures_def, Join_transient]));
 by (REPEAT (thin_tac "?F : ?A co ?B" 1));
 by (etac transientE 1);
 by (rewtac constrains_def);
@@ -551,11 +549,11 @@
 by (rtac Join_project_ensures_strong 1);
 by (auto_tac (claset() addDs [preserves_o_project_transient_empty]
 		       addIs [project_stable_project_set], 
-	      simpset() addsimps [Int_left_absorb, Join_stable]));
+	      simpset() addsimps [Int_left_absorb]));
 by (asm_simp_tac
     (simpset() addsimps [stable_ensures_Int RS ensures_weaken_R,
 			 Int_lower2, project_stable_project_set,
-			 Join_stable, extend_stable_project_set]) 1);
+			 extend_stable_project_set]) 1);
 val lemma = result();
 
 Goal "[| extend h F Join G : stable C;  \
@@ -623,7 +621,7 @@
 \             project_set h C Int project_set h B";
 by (rtac (psp_stable2 RS leadsTo_weaken_L) 1);
 by (auto_tac (claset(),
-	      simpset() addsimps [project_stable_project_set, Join_stable, 
+	      simpset() addsimps [project_stable_project_set, 
 				  extend_stable_project_set]));
 val lemma = result();
 
@@ -637,7 +635,7 @@
 by (blast_tac (claset() addIs [leadsTo_UN]) 3);
 by (blast_tac (claset() addIs [leadsTo_Trans, lemma]) 2);
 by (asm_full_simp_tac 
-    (simpset() addsimps [givenBy_eq_extend_set, Join_stable]) 1);
+    (simpset() addsimps [givenBy_eq_extend_set]) 1);
 by (rtac leadsTo_Basis 1);
 by (blast_tac (claset() addIs [leadsTo_Basis,
 			       ensures_extend_set_imp_project_ensures]) 1);
diff -r 480a1b40fdd6 -r aad13b59b8d9 src/HOL/UNITY/Extend.ML
--- a/src/HOL/UNITY/Extend.ML	Fri Jul 21 17:46:43 2000 +0200
+++ b/src/HOL/UNITY/Extend.ML	Fri Jul 21 18:01:36 2000 +0200
@@ -384,8 +384,7 @@
 Goal "project h C (extend h F) = \
 \     mk_program (Init F, Restrict (project_set h C) `` Acts F)";
 by (rtac program_equalityI 1);
-by (asm_simp_tac (simpset() addsimps [image_eq_UN, 
-                   project_act_extend_act_restrict]) 2);
+by (asm_simp_tac (simpset() addsimps [image_eq_UN]) 2);
 by (Simp_tac 1);
 qed "project_extend_eq";
 
diff -r 480a1b40fdd6 -r aad13b59b8d9 src/HOL/UNITY/Handshake.ML
--- a/src/HOL/UNITY/Handshake.ML	Fri Jul 21 17:46:43 2000 +0200
+++ b/src/HOL/UNITY/Handshake.ML	Fri Jul 21 18:01:36 2000 +0200
@@ -19,7 +19,7 @@
 by (rtac AlwaysI 1);
 by (Force_tac 1);
 by (rtac (constrains_imp_Constrains RS StableI) 1);
-by (auto_tac (claset(), simpset() addsimps [Join_constrains]));
+by Auto_tac;
 by (constrains_tac 2);
 by (auto_tac (claset() addIs [order_antisym] addSEs [le_SucE], simpset()));
 by (constrains_tac 1);
diff -r 480a1b40fdd6 -r aad13b59b8d9 src/HOL/UNITY/Lift_prog.ML
--- a/src/HOL/UNITY/Lift_prog.ML	Fri Jul 21 17:46:43 2000 +0200
+++ b/src/HOL/UNITY/Lift_prog.ML	Fri Jul 21 18:01:36 2000 +0200
@@ -46,6 +46,7 @@
 Goalw [lift_map_def, drop_map_def] "!!s. drop_map i (lift_map i s) = s";
 by (force_tac (claset() addIs [insert_map_inverse], simpset()) 1);
 qed "drop_map_lift_map_eq";
+Addsimps [drop_map_lift_map_eq];
 
 Goalw [lift_map_def] "inj (lift_map i)";
 by (rtac injI 1);
@@ -57,10 +58,11 @@
 Goalw [lift_map_def, drop_map_def] "!!s. lift_map i (drop_map i s) = s";
 by (force_tac (claset(), simpset() addsimps [insert_map_delete_map_eq]) 1);
 qed "lift_map_drop_map_eq";
+Addsimps [lift_map_drop_map_eq];
 
 Goal "(drop_map i s) = (drop_map i s') ==> s=s'";
 by (dres_inst_tac [("f", "lift_map i")] arg_cong 1);
-by (full_simp_tac (simpset() addsimps [lift_map_drop_map_eq]) 1);
+by (Full_simp_tac 1);
 qed "drop_map_inject";
 AddSDs [drop_map_inject];
 
@@ -74,19 +76,15 @@
 qed "bij_lift_map";
 AddIffs [bij_lift_map];
 
-AddIffs [bij_lift_map RS mem_rename_act_iff];
-
 Goal "inv (lift_map i) = drop_map i";
 by (rtac inv_equality 1);
-by (rtac lift_map_drop_map_eq 2);
-by (rtac drop_map_lift_map_eq 1);
+by Auto_tac;  
 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);
+by Auto_tac;  
 qed "inv_drop_map_eq";
 Addsimps [inv_drop_map_eq];
 
@@ -96,18 +94,13 @@
 qed "bij_drop_map";
 AddIffs [bij_drop_map];
 
-(*** sub ***)
-
+(*sub's main property!*)
 Goal "sub i f = f i";
 by (simp_tac (simpset() addsimps [sub_def]) 1);
 qed "sub_apply";
 Addsimps [sub_apply];
 
-Goal "lift_set i {s. P s} = {s. P (drop_map i s)}";
-by (rtac set_ext 1);
-by (asm_simp_tac (simpset() delsimps [image_Collect]
-			    addsimps [lift_set_def, bij_image_Collect_eq]) 1);
-qed "lift_set_eq_Collect";
+(*** lift_set ***)
 
 Goalw [lift_set_def] "lift_set i {} = {}";
 by Auto_tac;
@@ -117,7 +110,6 @@
 Goalw [lift_set_def] "(lift_map i x : lift_set i A) = (x : A)";
 by (rtac (inj_lift_map RS inj_image_mem_iff) 1);
 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)";
@@ -232,6 +224,11 @@
 qed "lift_guarantees_eq_lift_inv";
 
 
+(*** We devote an ENORMOUS effort to proving lift_transient_eq_disj, 
+     which is used only in TimerArray and perhaps isn't even essential
+     there!
+***)
+
 (*To preserve snd means that the second component is there just to allow
   guarantees properties to be stated.  Converse fails, for lift i F can 
   change function components other than i*)
@@ -264,12 +261,21 @@
 
 Addsimps [vimage_o_fst_eq, vimage_sub_eq_lift_set];
 
+Goalw [extend_act_def]
+     "((s,s') : extend_act (%(x,u::unit). lift_map i x) act) = \
+\     ((drop_map i s, drop_map i s') : act)";
+by Auto_tac;  
+by (rtac bexI 1);
+by Auto_tac;  
+qed "mem_lift_act_iff";
+AddIffs [mem_lift_act_iff];
+
 Goal "[| F : preserves snd;  i~=j |] \
 \     ==> lift j F : stable (lift_set i (A <*> UNIV))";
 by (auto_tac (claset(),
 	      simpset() addsimps [lift_def, lift_set_def, 
-				  stable_def, constrains_def, 
-				  mem_rename_act_iff, mem_rename_set_iff]));
+				  stable_def, constrains_def, rename_def,
+                                  extend_def, mem_rename_set_iff]));
 by (auto_tac (claset() addSDs [preserves_imp_eq],
 	      simpset() addsimps [lift_map_def, drop_map_def]));
 by (dres_inst_tac [("x", "i")] fun_cong 1);
@@ -326,8 +332,8 @@
 by (case_tac "i=j" 1);
 by (auto_tac (claset(), simpset() addsimps [lift_transient]));
 by (auto_tac (claset(),
-	      simpset() addsimps [lift_def, transient_def,
-				  Domain_rename_act]));
+	      simpset() addsimps [lift_set_def, lift_def, transient_def, 
+                              rename_def, extend_def, Domain_extend_act]));
 by (dtac subsetD 1);
 by (Blast_tac 1);
 by Auto_tac;
@@ -338,12 +344,11 @@
 by (dtac sym 1);
 by (dtac subsetD 1);
 by (rtac ImageI 1);
-by (etac rename_actI 1);
-by (force_tac (claset(), simpset() addsimps [lift_set_def]) 1);
+by (etac 
+    (bij_lift_map RS good_map_bij RS export (mem_extend_act_iff RS iffD2)) 1);
+by (Force_tac 1);
 by (etac (lift_map_eq_diff RS exE) 1);
-by (assume_tac 1);
-by (dtac ComplD 1);
-by (etac notE 1 THEN etac ssubst 1 THEN Fast_tac 1);
+by Auto_tac;  
 qed "lift_transient_eq_disj";
 
 (*USELESS??*)
diff -r 480a1b40fdd6 -r aad13b59b8d9 src/HOL/UNITY/PPROD.ML
--- a/src/HOL/UNITY/PPROD.ML	Fri Jul 21 17:46:43 2000 +0200
+++ b/src/HOL/UNITY/PPROD.ML	Fri Jul 21 18:01:36 2000 +0200
@@ -15,12 +15,7 @@
 by (simp_tac (simpset() addsimps [PLam_def, lift_def, lift_set_def]) 1);
 qed "Init_PLam";
 
-(*The "insert Id" is needed if I={}, since otherwise the RHS would be {} too*)
-Goal "Acts (PLam I F) = \
-\     insert Id (UN i:I. rename_act (lift_map i) `` Acts (F i))";
-by (simp_tac (simpset() addsimps [PLam_def, lift_def]) 1);
-qed "Acts_PLam";
-Addsimps [Init_PLam, Acts_PLam];
+Addsimps [Init_PLam];
 
 Goal "PLam {} F = SKIP";
 by (simp_tac (simpset() addsimps [PLam_def]) 1);
@@ -46,14 +41,13 @@
 qed "component_PLam";
 
 
-(** Safety & Progress **)
+(** Safety & Progress: but are they used anywhere? **)
 
 Goal "[| i : I;  ALL j. F j : preserves snd |] ==>  \
 \     (PLam I F : (lift_set i (A <*> UNIV)) co \
 \                 (lift_set i (B <*> UNIV)))  =  \
 \     (F i : (A <*> UNIV) co (B <*> UNIV))";
-by (asm_simp_tac (simpset() addsimps [PLam_def, JN_constrains,
-				      Join_constrains]) 1);
+by (asm_simp_tac (simpset() addsimps [PLam_def, JN_constrains]) 1);
 by (stac (insert_Diff RS sym) 1 THEN assume_tac 1);
 by (asm_simp_tac (simpset() addsimps [lift_constrains]) 1);
 by (blast_tac (claset() addIs [constrains_imp_lift_constrains]) 1);
@@ -70,18 +64,17 @@
 by (asm_simp_tac (simpset() addsimps [JN_transient, PLam_def]) 1);
 qed "PLam_transient";
 
-Addsimps [PLam_constrains, PLam_stable, PLam_transient];
-
 (*This holds because the F j cannot change (lift_set i)*)
 Goal "[| i : I;  F i : (A <*> UNIV) ensures (B <*> UNIV);  \
 \        ALL j. F j : preserves snd |] ==>  \
 \     PLam I F : lift_set i (A <*> UNIV) ensures lift_set i (B <*> UNIV)";
 by (auto_tac (claset(), 
-	      simpset() addsimps [ensures_def, lift_transient_eq_disj,
-				  lift_set_Un_distrib RS sym,
-				  lift_set_Diff_distrib RS sym,
-				  Times_Un_distrib1 RS sym,
-				  Times_Diff_distrib1 RS sym]));
+    simpset() addsimps [ensures_def, PLam_constrains, PLam_transient,
+	                lift_transient_eq_disj,
+			lift_set_Un_distrib RS sym,
+			lift_set_Diff_distrib RS sym,
+			Times_Un_distrib1 RS sym,
+			Times_Diff_distrib1 RS sym]));
 qed "PLam_ensures";
 
 Goal "[| i : I;  \
@@ -102,7 +95,7 @@
 \        ALL j. F j : preserves snd |] \
 \     ==> PLam I F : invariant (lift_set i (A <*> UNIV))";
 by (auto_tac (claset(),
-	      simpset() addsimps [invariant_def]));
+	      simpset() addsimps [PLam_stable, invariant_def]));
 qed "invariant_imp_PLam_invariant";
 
 
diff -r 480a1b40fdd6 -r aad13b59b8d9 src/HOL/UNITY/Project.ML
--- a/src/HOL/UNITY/Project.ML	Fri Jul 21 17:46:43 2000 +0200
+++ b/src/HOL/UNITY/Project.ML	Fri Jul 21 18:01:36 2000 +0200
@@ -32,7 +32,7 @@
 Goal "(F Join project h C G : A co B)  =  \
 \       (extend h F Join G : (C Int extend_set h A) co (extend_set h B) &  \
 \        F : A co B)";
-by (simp_tac (simpset() addsimps [Join_constrains, project_constrains]) 1);
+by (simp_tac (simpset() addsimps [project_constrains]) 1);
 by (blast_tac (claset() addIs [extend_constrains RS iffD2 RS constrains_weaken]
                         addDs [constrains_imp_subset]) 1);
 qed "Join_project_constrains";
@@ -44,7 +44,7 @@
 \     ==> (F Join project h C G : stable A)  =  \
 \         (extend h F Join G : stable (C Int extend_set h A) &  \
 \          F : stable A)";
-by (simp_tac (simpset() addsimps [Join_project_constrains]) 1);
+by (simp_tac (HOL_ss addsimps [Join_project_constrains]) 1);
 by (blast_tac (claset() addIs [constrains_weaken] addDs [constrains_Int]) 1);
 qed "Join_project_stable";
 
@@ -52,8 +52,7 @@
 Goal "extend h F Join G : extend_set h A co extend_set h B \
 \     ==> F Join project h C G : A co B";
 by (asm_full_simp_tac
-    (simpset() addsimps [project_constrains, Join_constrains, 
-			 extend_constrains]) 1);
+    (simpset() addsimps [project_constrains, extend_constrains]) 1);
 by (blast_tac (claset() addIs [constrains_weaken]
 			addDs [constrains_imp_subset]) 1);
 qed "project_constrains_I";
@@ -61,18 +60,18 @@
 Goalw [increasing_def, stable_def]
      "extend h F Join G : increasing (func o f) \
 \     ==> F Join project h C G : increasing func";
-by (asm_full_simp_tac (simpset() addsimps [project_constrains_I, 
-					   extend_set_eq_Collect]) 1);
+by (asm_full_simp_tac (simpset_of SubstAx.thy
+		 addsimps [project_constrains_I, extend_set_eq_Collect]) 1);
 qed "project_increasing_I";
 
 Goal "(F Join project h UNIV G : increasing func)  =  \
 \     (extend h F Join G : increasing (func o f))";
 by (rtac iffI 1);
 by (etac project_increasing_I 2);
-by (asm_full_simp_tac 
-    (simpset() addsimps [increasing_def, Join_project_stable]) 1);
+by (asm_full_simp_tac (simpset_of SubstAx.thy
+		         addsimps [increasing_def, Join_project_stable]) 1);
 by (auto_tac (claset(),
-	      simpset() addsimps [Join_stable, extend_set_eq_Collect,
+	      simpset() addsimps [extend_set_eq_Collect,
 				  extend_stable RS iffD1]));
 qed "Join_project_increasing";
 
@@ -80,8 +79,7 @@
 Goal "F Join project h UNIV G : A co B \
 \     ==> extend h F Join G : extend_set h A co extend_set h B";
 by (asm_full_simp_tac
-    (simpset() addsimps [project_constrains, Join_constrains, 
-			 extend_constrains]) 1);
+    (simpset() addsimps [project_constrains, extend_constrains]) 1);
 qed "project_constrains_D";
 
 
@@ -192,7 +190,7 @@
 
 Goalw [extending_def]
      "extending v (%G. UNIV) h F (increasing (func o f)) (increasing func)";
-by (simp_tac (simpset() addsimps [Join_project_increasing]) 1);
+by (simp_tac (HOL_ss addsimps [Join_project_increasing]) 1);
 qed "extending_increasing";
 
 
@@ -216,7 +214,7 @@
 Goalw [Constrains_def]
      "F Join project h (reachable (extend h F Join G)) G : A Co B  \
 \     ==> extend h F Join G : (extend_set h A) Co (extend_set h B)";
-by (full_simp_tac (simpset() addsimps [Join_project_constrains]) 1);
+by (full_simp_tac (simpset_of SubstAx.thy addsimps [Join_project_constrains]) 1);
 by (Clarify_tac 1);
 by (etac constrains_weaken 1);
 by (auto_tac (claset() addIs [reachable_imp_reachable_project], simpset()));
@@ -277,14 +275,14 @@
 Goalw [Constrains_def]
      "extend h F Join G : (extend_set h A) Co (extend_set h B)  \
 \     ==> F Join project h (reachable (extend h F Join G)) G : A Co B";
-by (full_simp_tac (simpset() addsimps [Join_project_constrains, 
+by (full_simp_tac (simpset_of SubstAx.thy addsimps [Join_project_constrains, 
 				       extend_set_Int_distrib]) 1);
 by (rtac conjI 1);
 by (force_tac
     (claset() addEs [constrains_weaken_L]
               addSDs [extend_constrains_project_set,
 		      subset_refl RS reachable_project_imp_reachable], 
-     simpset() addsimps [Join_constrains]) 2);
+     simpset()) 2);
 by (blast_tac (claset() addIs [constrains_weaken_L]) 1);
 qed "project_Constrains_I";
 
@@ -421,7 +419,7 @@
 \     ==> F Join project h C G  \
 \           : (project_set h C Int project_set h A) ensures (project_set h B)";
 by (asm_full_simp_tac
-    (simpset() addsimps [ensures_def, Join_constrains, project_constrains, 
+    (simpset() addsimps [ensures_def, project_constrains, 
 			 Join_transient, extend_transient]) 1);
 by (Clarify_tac 1);
 by (REPEAT_FIRST (rtac conjI));
@@ -463,8 +461,7 @@
                        addIs [transient_strengthen, project_set_I,
 			      project_unless RS unlessD, unlessI, 
 			      project_extend_constrains_I], 
-	      simpset() addsimps [ensures_def, Join_constrains,
-				  Join_stable, Join_transient]));
+	      simpset() addsimps [ensures_def, Join_transient]));
 qed_spec_mp "Join_project_ensures";
 
 (** Lemma useful for both STRONG and WEAK progress, but the transient
@@ -498,7 +495,7 @@
 \        F Join project h C G : A LeadsTo B |] \
 \     ==> extend h F Join G : (extend_set h A) LeadsTo (extend_set h B)";
 by (asm_full_simp_tac 
-    (simpset() addsimps [LeadsTo_def, project_leadsTo_D_lemma, 
+    (simpset_of SubstAx.thy addsimps [LeadsTo_def, project_leadsTo_D_lemma, 
 			 project_set_reachable_extend_eq]) 1);
 qed "Join_project_LeadsTo";
 
@@ -506,7 +503,6 @@
 (*** Towards project_Ensures_D ***)
 
 
-
 Goalw [project_set_def, extend_set_def, project_act_def]
      "act ^^ (C Int extend_set h A) <= B \
 \     ==> project_act h (Restrict C act) ^^ (project_set h C Int A) \
@@ -560,8 +556,7 @@
 (*unless*)
 by (auto_tac (claset() addSIs [rewrite_rule [unless_def] project_unless2] 
                        addIs [project_extend_constrains_I], 
-	      simpset() addsimps [ensures_def, Join_constrains,
-				  Join_stable]));
+	      simpset() addsimps [ensures_def]));
 (*transient*)
 by (auto_tac (claset(), simpset() addsimps [Join_transient]));
 by (blast_tac (claset() addIs [stable_project_transient]) 2);
diff -r 480a1b40fdd6 -r aad13b59b8d9 src/HOL/UNITY/Rename.ML
--- a/src/HOL/UNITY/Rename.ML	Fri Jul 21 17:46:43 2000 +0200
+++ b/src/HOL/UNITY/Rename.ML	Fri Jul 21 18:01:36 2000 +0200
@@ -40,34 +40,8 @@
 by (Simp_tac 1);
 qed "Init_rename";
 
-Goalw [rename_def, rename_act_def]
-     "bij h ==> Acts (rename h F) = (rename_act h `` Acts F)";
-by (asm_simp_tac (simpset() addsimps [export Acts_extend]) 1);
-qed "Acts_rename";
-
-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";
+Addsimps [Init_rename];
 
-Goalw [rename_act_def, extend_act_def]
-     "(s,s') : act ==> (h s, h s') : rename_act h act";
-by Auto_tac;
-qed "rename_actI";
-
-Goalw [rename_act_def]
-     "bij h ==> ((s,s') : rename_act h act) = ((inv h s, inv h s') : act)";
-by (rtac trans 1);
-by (etac (bij_export mem_extend_act_iff) 2);
-by (asm_simp_tac (simpset() addsimps [bij_is_surj RS surj_f_inv_f]) 1);
-qed "mem_rename_act_iff";
-
-Goalw [rename_act_def] "Domain (rename_act h act) = h``(Domain act)";
-by (asm_simp_tac (simpset() addsimps [export Domain_extend_act]) 1);
-qed "Domain_rename_act"; 
 
 (*** inverse properties ***)
 
@@ -139,14 +113,16 @@
 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]));
+	      simpset() addsimps [program_equality_iff, 
+                                  rename_def, extend_def]));
 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(), 
-	      simpset() addsimps [program_equality_iff, raw_Acts_rename]));
+	      simpset() addsimps [program_equality_iff, 
+                                  rename_def, extend_def]));
 qed "surj_rename_imp_surj";
 
 Goalw [bij_def] "bij (rename h) ==> bij h";
@@ -337,41 +313,3 @@
 Goal "bij h ==> rename h `` (A LeadsTo B) = (h `` A) LeadsTo (h``B)";
 by (rename_image_tac [rename_LeadsTo]);
 qed "rename_image_LeadsTo";
-
-
-
-
-(** junk
-
-
-Goalw [extend_act_def, project_act_def, surj_def]
- "surj h ==> extend_act (%(x,u). h x) (project_act (%(x,u). h x) act) = act";
-by Auto_tac;
-by (forw_inst_tac [("x", "a")] spec 1);
-by (dres_inst_tac [("x", "b")] spec 1);
-by Auto_tac;
-qed "project_act_inverse";
-
-Goal "bij h ==> rename h (rename (inv h) F) = F";
-by (rtac program_equalityI 1);
-by (Asm_simp_tac 1);
-by (asm_simp_tac
-    (simpset() addsimps [rename_def, inverse_def, export Acts_extend,
-			 image_eq_UN, export extend_act_Id,
-			 bij_is_surj RS project_act_inverse]) 1);
-qed "rename_rename_inv";
-Addsimps [rename_rename_inv];
-
-
-
-Goalw [bij_def]
-     "bij h \
-\     ==> extend_set (%(x,u::'c). inv h x) = inv (extend_set (%(x,u::'c). h x))";
-by (rtac ext 1);
-by (auto_tac (claset() addSIs [image_eqI], 
-	      simpset() addsimps [extend_set_def, project_set_def,
-				  surj_f_inv_f]));
-qed "extend_set_inv";
-
-
-***)
diff -r 480a1b40fdd6 -r aad13b59b8d9 src/HOL/UNITY/Rename.thy
--- a/src/HOL/UNITY/Rename.thy	Fri Jul 21 17:46:43 2000 +0200
+++ b/src/HOL/UNITY/Rename.thy	Fri Jul 21 18:01:36 2000 +0200
@@ -9,13 +9,6 @@
 Rename = Extend +
 
 constdefs
-  rename_act :: "['a => 'b, ('a*'a) set] => ('b*'b) set"
-    "rename_act h == extend_act (%(x,u::unit). h x)"
-
-(**OR
-      "rename_act h == %act. UN (s,s'): act.  {(h s, h s')}"
-      "rename_act h == %act. (prod_fun h h) `` act"
-**)
   
   rename :: "['a => 'b, 'a program] => 'b program"
     "rename h == extend (%(x,u::unit). h x)"
diff -r 480a1b40fdd6 -r aad13b59b8d9 src/HOL/UNITY/TimerArray.ML
--- a/src/HOL/UNITY/TimerArray.ML	Fri Jul 21 17:46:43 2000 +0200
+++ b/src/HOL/UNITY/TimerArray.ML	Fri Jul 21 18:01:36 2000 +0200
@@ -26,6 +26,7 @@
 qed "Timer_preserves_snd";
 AddIffs [Timer_preserves_snd];
 
+Addsimps [PLam_stable];
 
 Goal "finite I \
 \     ==> (plam i: I. Timer) : UNIV leadsTo {(s,uu). ALL i:I. s i = 0}";
diff -r 480a1b40fdd6 -r aad13b59b8d9 src/HOL/UNITY/Union.ML
--- a/src/HOL/UNITY/Union.ML	Fri Jul 21 17:46:43 2000 +0200
+++ b/src/HOL/UNITY/Union.ML	Fri Jul 21 18:01:36 2000 +0200
@@ -188,6 +188,8 @@
 by (simp_tac (simpset() addsimps [Join_constrains, unless_def]) 1);
 qed "Join_unless";
 
+Addsimps [Join_constrains, Join_unless];
+
 (*Analogous weak versions FAIL; see Misra [1994] 5.4.1, Substitution Axiom.
   reachable (F Join G) could be much bigger than reachable F, reachable G
 *)
@@ -195,7 +197,7 @@
 
 Goal "[| F : A co A';  G : B co B' |] \
 \     ==> F Join G : (A Int B) co (A' Un B')";
-by (simp_tac (simpset() addsimps [Join_constrains]) 1);
+by (Simp_tac 1);
 by (blast_tac (claset() addIs [constrains_weaken]) 1);
 qed "Join_constrains_weaken";
 
@@ -219,7 +221,7 @@
 
 Goal "(F Join G : stable A) = \
 \     (F : stable A & G : stable A)";
-by (simp_tac (simpset() addsimps [stable_def, Join_constrains]) 1);
+by (simp_tac (simpset() addsimps [stable_def]) 1);
 qed "Join_stable";
 
 Goal "(F Join G : increasing f) = \
@@ -228,9 +230,11 @@
 by (Blast_tac 1);
 qed "Join_increasing";
 
+Addsimps [Join_stable, Join_increasing];
+
 Goal "[| F : invariant A; G : invariant A |]  \
 \     ==> F Join G : invariant A";
-by (full_simp_tac (simpset() addsimps [invariant_def, Join_stable]) 1);
+by (full_simp_tac (simpset() addsimps [invariant_def]) 1);
 by (Blast_tac 1);
 qed "invariant_JoinI";
 
@@ -254,6 +258,8 @@
 				  Join_def]));
 qed "Join_transient";
 
+Addsimps [Join_transient];
+
 Goal "F : transient A ==> F Join G : transient A";
 by (asm_simp_tac (simpset() addsimps [Join_transient]) 1);
 qed "Join_transient_I1";
@@ -274,8 +280,7 @@
      "F Join G : A ensures B =     \
 \     (F : (A-B) co (A Un B) & G : (A-B) co (A Un B) & \
 \      (F : transient (A-B) | G : transient (A-B)))";
-by (auto_tac (claset(),
-	      simpset() addsimps [Join_constrains, Join_transient]));
+by (auto_tac (claset(), simpset() addsimps [Join_transient]));
 qed "Join_ensures";
 
 Goalw [stable_def, constrains_def, Join_def]
@@ -289,7 +294,7 @@
   G : stable A *)
 Goal "[| F : stable A;  G : invariant A |] ==> F Join G : Always A";
 by (full_simp_tac (simpset() addsimps [Always_def, invariant_def, 
-				       Stable_eq_stable, Join_stable]) 1);
+				       Stable_eq_stable]) 1);
 by (force_tac(claset() addIs [stable_Int], simpset()) 1);
 qed "stable_Join_Always1";