# HG changeset patch
# User paulson
# Date 969717721 -7200
# Node ID 1a77667b21ef896ec614df3441063524c50f44ab
# Parent  947ee8608b90c1f3d32774b0dacf302ff34bc61d
added compatibility relation: AllowedActs, Allowed, ok,
OK and changes to "guarantees", etc.

diff -r 947ee8608b90 -r 1a77667b21ef src/HOL/UNITY/Alloc.ML
--- a/src/HOL/UNITY/Alloc.ML	Fri Sep 22 17:25:09 2000 +0200
+++ b/src/HOL/UNITY/Alloc.ML	Sat Sep 23 16:02:01 2000 +0200
@@ -9,7 +9,8 @@
 (*Perhaps equalities.ML shouldn't add this in the first place!*)
 Delsimps [image_Collect];
 
-AddIs [impOfSubs subset_preserves_o];
+AddIs    [impOfSubs subset_preserves_o];
+Addsimps [impOfSubs subset_preserves_o];
 Addsimps [funPair_o_distrib];
 Addsimps [Always_INT_distrib];
 Delsimps [o_apply];
@@ -23,7 +24,7 @@
 	  rename_image_Constrains, rename_image_Stable,
 	  rename_image_Increasing, rename_image_Always,
 	  rename_image_leadsTo, rename_image_LeadsTo,
-	  rename_preserves,
+	  rename_preserves, rename_image_preserves, lift_image_preserves,
 	  bij_image_INT, bij_is_inj RS image_Int, bij_image_Collect_eq];
 
 (*Splits up conjunctions & intersections: like CONJUNCTS in the HOL system*)
@@ -31,6 +32,7 @@
     (list_of_Int (th RS conjunct1) @ list_of_Int (th RS conjunct2))
     handle THM _ => (list_of_Int (th RS IntD1) @ list_of_Int (th RS IntD2))
     handle THM _ => (list_of_Int (th RS INT_D))
+    handle THM _ => (list_of_Int (th RS bspec))
     handle THM _ => [th];
 
 (*Used just once, for Alloc_Increasing*)
@@ -196,7 +198,32 @@
 qed "allocRel_o_sysOfClient_eq";
 Addsimps (make_o_equivs allocRel_o_sysOfClient_eq);
 
+Goal "allocGiv o inv sysOfAlloc = allocGiv";
+by (simp_tac (simpset() addsimps [o_def]) 1); 
+qed "allocGiv_o_inv_sysOfAlloc_eq";
+Addsimps (make_o_equivs allocGiv_o_inv_sysOfAlloc_eq);
 
+Goal "allocAsk o inv sysOfAlloc = allocAsk";
+by (simp_tac (simpset() addsimps [o_def]) 1); 
+qed "allocAsk_o_inv_sysOfAlloc_eq";
+Addsimps (make_o_equivs allocAsk_o_inv_sysOfAlloc_eq);
+
+Goal "allocRel o inv sysOfAlloc = allocRel";
+by (simp_tac (simpset() addsimps [o_def]) 1); 
+qed "allocRel_o_inv_sysOfAlloc_eq";
+Addsimps (make_o_equivs allocRel_o_inv_sysOfAlloc_eq);
+
+Goal "(rel o inv client_map o drop_map i o inv sysOfClient) = \
+\     rel o sub i o client";
+by (simp_tac (simpset() addsimps [o_def, drop_map_def]) 1); 
+qed "rel_inv_client_map_drop_map";
+Addsimps (make_o_equivs rel_inv_client_map_drop_map);
+
+Goal "(ask o inv client_map o drop_map i o inv sysOfClient) = \
+\     ask o sub i o client";
+by (simp_tac (simpset() addsimps [o_def, drop_map_def]) 1); 
+qed "ask_inv_client_map_drop_map";
+Addsimps (make_o_equivs ask_inv_client_map_drop_map);
 
 (**
 Open_locale "System";
@@ -206,55 +233,63 @@
 val Network = thm "Network";
 val System_def = thm "System_def";
 
-(*CANNOT use bind_thm: it puts the theorem into standard form, in effect
-  exporting it from the locale*)
+CANNOT use bind_thm: it puts the theorem into standard form, in effect
+  exporting it from the locale
 **)
 
 AddIffs [finite_lessThan];
 
 (*Client : <unfolded specification> *)
-val Client_Spec =
-    rewrite_rule [client_spec_def, client_increasing_def,
-		  client_bounded_def, client_progress_def,
-		  client_preserves_def] Client;
+val client_spec_simps = 
+    [client_spec_def, client_increasing_def, client_bounded_def, 
+     client_progress_def, client_allowed_acts_def, client_preserves_def, 
+     guarantees_Int_right];
 
 val [Client_Increasing_ask, Client_Increasing_rel,
-     Client_Bounded, Client_Progress, Client_preserves_giv,
-     Client_preserves_dummy] =
-        Client_Spec 
-          |> simplify (simpset() addsimps [guarantees_Int_right]) 
-          |> list_of_Int;
+     Client_Bounded, Client_Progress, Client_AllowedActs, 
+     Client_preserves_giv, Client_preserves_dummy] =
+        Client |> simplify (simpset() addsimps client_spec_simps) 
+               |> list_of_Int;
 
 AddIffs [Client_Increasing_ask, Client_Increasing_rel, Client_Bounded,
 	 Client_preserves_giv, Client_preserves_dummy];
 
 
 (*Network : <unfolded specification> *)
-val Network_Spec =
-    rewrite_rule [network_spec_def, network_ask_def, network_giv_def, 
-		  network_rel_def, network_preserves_def] Network;
+val network_spec_simps = 
+    [network_spec_def, network_ask_def, network_giv_def, 
+     network_rel_def, network_allowed_acts_def, network_preserves_def, 
+     ball_conj_distrib];
 
-val [Network_Ask, Network_Giv, Network_Rel, 
-     Network_preserves_allocGiv, Network_preserves_rel_ask] = 
-    list_of_Int Network_Spec;
+val [Network_Ask, Network_Giv, Network_Rel, Network_AllowedActs,
+     Network_preserves_allocGiv, Network_preserves_rel, 
+     Network_preserves_ask]  =  
+        Network |> simplify (simpset() addsimps network_spec_simps) 
+                |> list_of_Int;
 
 AddIffs  [Network_preserves_allocGiv];
 
-Addsimps (Network_preserves_rel_ask |> simplify (simpset()) |> list_of_Int);
+Addsimps [Network_preserves_rel, Network_preserves_ask];
+Addsimps [o_simp Network_preserves_rel, o_simp Network_preserves_ask];
 
 
 (*Alloc : <unfolded specification> *)
-val Alloc_Spec =
-    rewrite_rule [alloc_spec_def, alloc_increasing_def, alloc_safety_def, 
-		  alloc_progress_def, alloc_preserves_def] Alloc;
+val alloc_spec_simps = 
+    [alloc_spec_def, alloc_increasing_def, alloc_safety_def, 
+		  alloc_progress_def, alloc_allowed_acts_def, 
+                  alloc_preserves_def];
 
-val [Alloc_Increasing_0, Alloc_Safety, 
-     Alloc_Progress, Alloc_preserves] = list_of_Int Alloc_Spec;
+val [Alloc_Increasing_0, Alloc_Safety, Alloc_Progress, Alloc_AllowedActs,
+     Alloc_preserves_allocRel, Alloc_preserves_allocAsk, 
+     Alloc_preserves_dummy] = 
+        Alloc |> simplify (simpset() addsimps alloc_spec_simps) 
+              |> list_of_Int;
 
 (*Strip off the INT in the guarantees postcondition*)
 val Alloc_Increasing = normalize Alloc_Increasing_0;
 
-AddIffs (Alloc_preserves |> simplify (simpset()) |> list_of_Int);
+AddIffs [Alloc_preserves_allocRel, Alloc_preserves_allocAsk, 
+         Alloc_preserves_dummy];
 
 (** Components lemmas [MUST BE AUTOMATED] **)
 
@@ -283,9 +318,37 @@
 
 (** These preservation laws should be generated automatically **)
 
-AddIs    [impOfSubs subset_preserves_o];
-Addsimps [impOfSubs subset_preserves_o];
+Goal "Allowed Client = preserves rel Int preserves ask";
+by (auto_tac (claset(), 
+              simpset() addsimps [Allowed_def, Client_AllowedActs, 
+                                  safety_prop_Acts_iff]));  
+qed "Client_Allowed";
+Addsimps [Client_Allowed];
+
+Goal "Allowed Network =        \
+\       preserves allocRel Int \
+\       (INT i: lessThan Nclients. preserves(giv o sub i o client))";
+by (auto_tac (claset(), 
+              simpset() addsimps [Allowed_def, Network_AllowedActs, 
+                                  safety_prop_Acts_iff]));  
+qed "Network_Allowed";
+Addsimps [Network_Allowed];
 
+Goal "Allowed Alloc = preserves allocGiv";
+by (auto_tac (claset(), 
+              simpset() addsimps [Allowed_def, Alloc_AllowedActs, 
+                                  safety_prop_Acts_iff]));  
+qed "Alloc_Allowed";
+Addsimps [Alloc_Allowed];
+
+Goal "OK I (%i. lift i (rename client_map Client))";
+by (rtac OK_lift_I 1); 
+by Auto_tac;  
+by (dres_inst_tac [("w1", "rel")] (impOfSubs subset_preserves_o) 1);
+by (dres_inst_tac [("w1", "ask")] (impOfSubs subset_preserves_o) 2);
+by (auto_tac (claset(), simpset() addsimps [o_def, split_def]));  
+qed "OK_lift_rename_Client";
+Addsimps [OK_lift_rename_Client]; (*needed in rename_client_map_tac*
 
 (*The proofs of rename_Client_Increasing, rename_Client_Bounded and
   rename_Client_Progress are similar.  All require copying out the original
@@ -321,23 +384,62 @@
     asm_simp_tac
         (simpset() addsimps [o_def, non_dummy_def, guarantees_Int_right]) 1];
 
-
+						     
 (*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)";
+\           UNIV  guarantees  \
+\           Increasing (ask o sub i o client) Int \
+\           Increasing (rel o sub i o client)";
 by rename_client_map_tac;
 qed "rename_Client_Increasing";
 
+Goal "[| F : preserves w; i ~= j |] \
+\     ==> F : preserves (sub i o fst o lift_map j o funPair v w)";
+by (auto_tac (claset(), 
+       simpset() addsimps [lift_map_def, split_def, linorder_neq_iff, o_def]));
+by (ALLGOALS (dtac (impOfSubs subset_preserves_o)));
+by (auto_tac (claset(), simpset() addsimps [o_def]));  
+qed "preserves_sub_fst_lift_map";
+
+Goal "[| i < Nclients; j < Nclients |] \
+\     ==> Client : preserves (giv o sub i o fst o lift_map j o client_map)";
+by (case_tac "i=j" 1);
+by (asm_full_simp_tac (simpset() addsimps [o_def, non_dummy_def]) 1);
+by (dtac (Client_preserves_dummy RS preserves_sub_fst_lift_map) 1);
+by (ALLGOALS (dtac (impOfSubs subset_preserves_o)));
+by (asm_full_simp_tac (simpset() addsimps [o_def, client_map_def]) 1);  
+qed "client_preserves_giv_oo_client_map";
+
+Goal "rename sysOfClient (plam x: lessThan Nclients. rename client_map Client)\
+\     ok Network";
+by (auto_tac (claset(), simpset() addsimps [ok_iff_Allowed,
+        client_preserves_giv_oo_client_map]));  
+qed "rename_sysOfClient_ok_Network";
+
+Goal "rename sysOfClient (plam x: lessThan Nclients. rename client_map Client)\
+\     ok rename sysOfAlloc Alloc";
+by (simp_tac (simpset() addsimps [ok_iff_Allowed]) 1);
+qed "rename_sysOfClient_ok_Alloc";
+
+Goal "rename sysOfAlloc Alloc ok Network";
+by (simp_tac (simpset() addsimps [ok_iff_Allowed]) 1);
+qed "rename_sysOfAlloc_ok_Network";
+
+AddIffs [rename_sysOfClient_ok_Network, rename_sysOfClient_ok_Alloc,
+         rename_sysOfAlloc_ok_Network];
+
+(*The "ok" laws, re-oriented*)
+AddIffs [rename_sysOfClient_ok_Network RS ok_sym,
+         rename_sysOfClient_ok_Alloc RS ok_sym,
+         rename_sysOfAlloc_ok_Network RS ok_sym];
+
 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;
+by Auto_tac;  
 qed "System_Increasing";
 
 bind_thm ("rename_guarantees_sysOfAlloc_I",
@@ -476,9 +578,8 @@
 (*progress (2), step 3: lifting "Client_Bounded" to systemState*)
 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}";
+\         UNIV  guarantees  \
+\         Always {s. ALL elt : set ((ask o sub i o client) s). elt <= NbT}";
 by rename_client_map_tac;
 qed "rename_Client_Bounded";
 
@@ -514,7 +615,7 @@
 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] \
+\         guarantees \
 \         (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})";
@@ -616,3 +717,28 @@
 qed "System_correct";
 
 
+(** Some lemmas no longer used **)
+
+Goal "non_dummy = (% (g,a,r). (| giv = g, ask = a, rel = r |)) o \
+\                             (funPair giv (funPair ask rel))";
+by (rtac ext 1); 
+by (auto_tac (claset(), simpset() addsimps [o_def, non_dummy_def]));  
+qed "non_dummy_eq_o_funPair";
+
+Goal "(preserves non_dummy) = \
+\     (preserves rel Int preserves ask Int preserves giv)";
+by (simp_tac (simpset() addsimps [non_dummy_eq_o_funPair]) 1); 
+by Auto_tac;  
+by (dres_inst_tac [("w1", "rel")] (impOfSubs subset_preserves_o) 1);
+by (dres_inst_tac [("w1", "ask")] (impOfSubs subset_preserves_o) 2);
+by (dres_inst_tac [("w1", "giv")] (impOfSubs subset_preserves_o) 3);
+by (auto_tac (claset(), simpset() addsimps [o_def]));  
+qed "preserves_non_dummy_eq";
+
+(*Could go to Extend.ML*)
+Goal "bij f ==> fst (inv (%(x, u). inv f x) z) = f z";
+by (rtac fst_inv_equalityI 1); 
+by (res_inst_tac [("f","%z. (f z, ?h z)")] surjI 1); 
+by (asm_full_simp_tac (simpset() addsimps [bij_is_inj, inv_f_f]) 1); 
+by (asm_full_simp_tac (simpset() addsimps [bij_is_surj, surj_f_inv_f]) 1); 
+qed "bij_fst_inv_inv_eq";
diff -r 947ee8608b90 -r 1a77667b21ef src/HOL/UNITY/Alloc.thy
--- a/src/HOL/UNITY/Alloc.thy	Fri Sep 22 17:25:09 2000 +0200
+++ b/src/HOL/UNITY/Alloc.thy	Sat Sep 23 16:02:01 2000 +0200
@@ -70,45 +70,47 @@
   (*spec (3)*)
   client_increasing :: 'a clientState_d program set
     "client_increasing ==
-         UNIV guarantees[funPair rel ask]
-         Increasing ask Int Increasing rel"
+         UNIV guarantees  Increasing ask Int Increasing rel"
 
   (*spec (4)*)
   client_bounded :: 'a clientState_d program set
     "client_bounded ==
-         UNIV guarantees[ask]
-         Always {s. ALL elt : set (ask s). elt <= NbT}"
+         UNIV guarantees  Always {s. ALL elt : set (ask s). elt <= NbT}"
 
   (*spec (5)*)
   client_progress :: 'a clientState_d program set
     "client_progress ==
-	 Increasing giv
-	 guarantees[funPair rel ask]
+	 Increasing giv  guarantees
 	 (INT h. {s. h <= giv s & h pfixGe ask s}
 		 LeadsTo {s. tokens h <= (tokens o rel) s})"
 
   (*spec: preserves part*)
-    client_preserves :: 'a clientState_d program set
-    "client_preserves == preserves (funPair giv clientState_d.dummy)"
+  client_preserves :: 'a clientState_d program set
+    "client_preserves == preserves giv Int preserves clientState_d.dummy"
+
+  (*environmental constraints*)
+  client_allowed_acts :: 'a clientState_d program set
+    "client_allowed_acts ==
+       {F. AllowedActs F =
+	    insert Id (UNION (preserves (funPair rel ask)) Acts)}"
 
   client_spec :: 'a clientState_d program set
     "client_spec == client_increasing Int client_bounded Int client_progress
-                    Int client_preserves"
+                    Int client_allowed_acts Int client_preserves"
 
 (** Allocator specification (required) ***)
 
   (*spec (6)*)
   alloc_increasing :: 'a allocState_d program set
     "alloc_increasing ==
-	 UNIV
-         guarantees[allocGiv]
+	 UNIV  guarantees
 	 (INT i : lessThan Nclients. Increasing (sub i o allocGiv))"
 
   (*spec (7)*)
   alloc_safety :: 'a allocState_d program set
     "alloc_safety ==
 	 (INT i : lessThan Nclients. Increasing (sub i o allocRel))
-         guarantees[allocGiv]
+         guarantees
 	 Always {s. setsum(%i.(tokens o sub i o allocGiv)s) (lessThan Nclients)
          <= NbT + setsum(%i.(tokens o sub i o allocRel)s) (lessThan Nclients)}"
 
@@ -125,7 +127,7 @@
 	  INT h. {s. h <= (sub i o allocGiv)s & h pfixGe (sub i o allocAsk)s}
 		 LeadsTo
 	         {s. tokens h <= (tokens o sub i o allocRel)s})
-         guarantees[allocGiv]
+         guarantees
 	     (INT i : lessThan Nclients.
 	      INT h. {s. h <= (sub i o allocAsk) s}
 	             LeadsTo
@@ -139,46 +141,62 @@
     looked at.*)
 
   (*spec: preserves part*)
-    alloc_preserves :: 'a allocState_d program set
-    "alloc_preserves == preserves (funPair allocRel
-				   (funPair allocAsk allocState_d.dummy))"
+  alloc_preserves :: 'a allocState_d program set
+    "alloc_preserves == preserves allocRel Int preserves allocAsk Int
+                        preserves allocState_d.dummy"
   
+  (*environmental constraints*)
+  alloc_allowed_acts :: 'a allocState_d program set
+    "alloc_allowed_acts ==
+       {F. AllowedActs F =
+	    insert Id (UNION (preserves allocGiv) Acts)}"
+
   alloc_spec :: 'a allocState_d program set
     "alloc_spec == alloc_increasing Int alloc_safety Int alloc_progress Int
-                   alloc_preserves"
+                   alloc_allowed_acts Int alloc_preserves"
 
 (** Network specification ***)
 
   (*spec (9.1)*)
   network_ask :: 'a systemState program set
     "network_ask == INT i : lessThan Nclients.
-			Increasing (ask o sub i o client)
-			guarantees[allocAsk]
+			Increasing (ask o sub i o client)  guarantees
 			((sub i o allocAsk) Fols (ask o sub i o client))"
 
   (*spec (9.2)*)
   network_giv :: 'a systemState program set
     "network_giv == INT i : lessThan Nclients.
 			Increasing (sub i o allocGiv)
-			guarantees[giv o sub i o client]
+			guarantees
 			((giv o sub i o client) Fols (sub i o allocGiv))"
 
   (*spec (9.3)*)
   network_rel :: 'a systemState program set
     "network_rel == INT i : lessThan Nclients.
 			Increasing (rel o sub i o client)
-			guarantees[allocRel]
+			guarantees
 			((sub i o allocRel) Fols (rel o sub i o client))"
 
   (*spec: preserves part*)
-    network_preserves :: 'a systemState program set
-    "network_preserves == preserves allocGiv  Int
-                          (INT i : lessThan Nclients.
-                           preserves (funPair rel ask o sub i o client))"
+  network_preserves :: 'a systemState program set
+    "network_preserves ==
+       preserves allocGiv  Int
+       (INT i : lessThan Nclients. preserves (rel o sub i o client)  Int
+                                   preserves (ask o sub i o client))"
   
+  (*environmental constraints*)
+  network_allowed_acts :: 'a systemState program set
+    "network_allowed_acts ==
+       {F. AllowedActs F =
+           insert Id
+	    (UNION (preserves allocRel Int
+		    (INT i: lessThan Nclients. preserves(giv o sub i o client)))
+		  Acts)}"
+
   network_spec :: 'a systemState program set
     "network_spec == network_ask Int network_giv Int
-                     network_rel Int network_preserves"
+                     network_rel Int network_allowed_acts Int
+                     network_preserves"
 
 
 (** State mappings **)
diff -r 947ee8608b90 -r 1a77667b21ef src/HOL/UNITY/AllocImpl.ML
--- a/src/HOL/UNITY/AllocImpl.ML	Fri Sep 22 17:25:09 2000 +0200
+++ b/src/HOL/UNITY/AllocImpl.ML	Sat Sep 23 16:02:01 2000 +0200
@@ -11,21 +11,38 @@
 Addsimps [Always_INT_distrib];
 Delsimps [o_apply];
 
-(*Make a locale for M: merge_spec and G: preserves (funPair merge.Out iOut)?*)
+Open_locale "Merge";
+
+val Merge = thm "Merge_spec";
+
+Goal "Allowed M = (preserves merge.Out) Int (preserves merge.iOut)";
+by (cut_facts_tac [Merge] 1);
+by (auto_tac (claset(), 
+              simpset() addsimps [merge_spec_def, merge_allowed_acts_def, 
+                                  Allowed_def, safety_prop_Acts_iff]));  
+qed "Merge_Allowed";
 
-Goalw [merge_spec_def,merge_eqOut_def]
-     "[| M: merge_spec; G: preserves merge.Out; G: preserves merge.iOut |] \
-\ ==> M Join G : Always {s. length (merge.Out s) = length (merge.iOut s)}";  
-by (force_tac (claset() addDs [guaranteesD], simpset()) 1);
+Goal "M ok G = (G: preserves merge.Out & G: preserves merge.iOut & \
+\                    M : Allowed G)";
+by (auto_tac (claset(), simpset() addsimps [Merge_Allowed, ok_iff_Allowed]));  
+qed "M_ok_iff";
+AddIffs [M_ok_iff];
+
+Goal "[| G: preserves merge.Out; G: preserves merge.iOut; M : Allowed G |] \
+\     ==> M Join G : Always {s. length (merge.Out s) = length (merge.iOut s)}";
+by (cut_facts_tac [Merge] 1);
+by (force_tac (claset() addDs [guaranteesD], 
+               simpset() addsimps [merge_spec_def, merge_eqOut_def]) 1); 
 qed "Merge_Always_Out_eq_iOut";
 
-Goalw [merge_spec_def,merge_bounded_def]
-     "[| M: merge_spec; G: preserves merge.iOut |] \
-\ ==> M Join G : Always {s. ALL elt : set (merge.iOut s). elt < Nclients}";  
-by (force_tac (claset() addDs [guaranteesD], simpset()) 1);
+Goal "[| G: preserves merge.iOut; G: preserves merge.Out; M : Allowed G |] \
+\     ==> M Join G: Always {s. ALL elt : set (merge.iOut s). elt < Nclients}";
+by (cut_facts_tac [Merge] 1);
+by (force_tac (claset() addDs [guaranteesD], 
+               simpset() addsimps [merge_spec_def, merge_bounded_def]) 1); 
 qed "Merge_Bounded";
 
-Goal "[| M : merge_spec;  G : preserves (funPair merge.Out iOut) |] \
+Goal "[| G: preserves merge.iOut; G: preserves merge.Out; M : Allowed G |] \
 \ ==> M Join G : Always \
 \         {s. setsum (%i. bag_of (sublist (merge.Out s) \
 \                                 {k. k < length (iOut s) & iOut s ! k = i})) \
@@ -45,35 +62,44 @@
 by (asm_simp_tac (simpset() addsimps [o_def]) 1); 
 qed "Merge_Bag_Follows_lemma";
 
-Goal "M : merge_spec \
-\ ==> M : (INT i: lessThan Nclients. Increasing (sub i o merge.In)) \
-\             guarantees[funPair merge.Out merge.iOut]  \
-\                (bag_of o merge.Out) Fols \
-\                (%s. setsum (%i. (bag_of o sub i o merge.In) s) \
-\                            (lessThan Nclients))";
+Goal "M : (INT i: lessThan Nclients. Increasing (sub i o merge.In)) \
+\         guarantees  \
+\            (bag_of o merge.Out) Fols \
+\            (%s. setsum (%i. (bag_of o sub i o merge.In) s) \
+\                        (lessThan Nclients))";
 by (rtac (Merge_Bag_Follows_lemma RS Always_Follows1 RS guaranteesI) 1);
-by Auto_tac;
+by Auto_tac;  
 by (rtac Follows_setsum 1);
+by (cut_facts_tac [Merge] 1);
 by (auto_tac (claset(), 
-              simpset() addsimps [merge_spec_def,merge_follows_def, o_def]));
-by (best_tac (claset() addIs [impOfSubs (mono_bag_of RS mono_Follows_apply)]
-                       addDs [guaranteesD]) 1);
+              simpset() addsimps [merge_spec_def, merge_follows_def, o_def]));
+by (dtac guaranteesD 1); 
+by (best_tac
+    (claset() addIs [impOfSubs (mono_bag_of RS mono_Follows_apply)]) 3);
+by Auto_tac;  
 qed "Merge_Bag_Follows";
 
+Close_locale "Merge";
+
 
 (** Distributor **)
-	 
-Goalw [distr_follows_def]
-     "D : distr_follows \
-\ ==> D : Increasing distr.In Int Increasing distr.iIn Int \
-\        Always {s. ALL elt : set (distr.iIn s). elt < Nclients} \
-\        guarantees[distr.Out] \
-\        (INT i : lessThan Nclients. Increasing (sub i o distr.Out))";
+
+Open_locale "Distrib";
+
+val Distrib = thm "Distrib_spec";
+  
+
+Goal "D : Increasing distr.In Int Increasing distr.iIn Int \
+\         Always {s. ALL elt : set (distr.iIn s). elt < Nclients} \
+\         guarantees \
+\         (INT i : lessThan Nclients. Increasing (sub i o distr.Out))";
+by (cut_facts_tac [Distrib] 1);
+by (full_simp_tac (simpset() addsimps [distr_spec_def, distr_follows_def]) 1); 
+by (Clarify_tac 1); 
 by (blast_tac (claset() addIs [guaranteesI, Follows_Increasing1]
                         addDs [guaranteesD]) 1);
 qed "Distr_Increasing_Out";
 
-
 Goal "[| G : preserves distr.Out; \
 \        D Join G : Always {s. ALL elt: set (distr.iIn s). elt < Nclients} |] \
 \ ==> D Join G : Always \
@@ -94,26 +120,37 @@
 by (Asm_simp_tac 1); 
 qed "Distr_Bag_Follows_lemma";
 
+Goal "D ok G = (G: preserves distr.Out & D : Allowed G)";
+by (cut_facts_tac [Distrib] 1);
+by (auto_tac (claset(), 
+     simpset() addsimps [distr_spec_def, distr_allowed_acts_def, 
+                         Allowed_def, safety_prop_Acts_iff, ok_iff_Allowed]));
+qed "D_ok_iff";
+AddIffs [D_ok_iff];
 
-Goal "D : distr_follows \
-\ ==> D : Increasing distr.In Int Increasing distr.iIn Int \
+Goal
+ "D : Increasing distr.In Int Increasing distr.iIn Int \
 \     Always {s. ALL elt : set (distr.iIn s). elt < Nclients} \
-\     guarantees[distr.Out] \
+\     guarantees  \
 \      (INT i : lessThan Nclients. \
 \       (%s. setsum (%i. (bag_of o sub i o distr.Out) s) (lessThan Nclients)) \
 \       Fols \
 \       (%s. bag_of (sublist (distr.In s) (lessThan (length(distr.iIn s))))))";
 by (rtac guaranteesI 1);
-by (Clarify_tac 1);
+by (Clarify_tac 1); 
 by (rtac (Distr_Bag_Follows_lemma RS Always_Follows2) 1);
-by Auto_tac;
+by Auto_tac;  
 by (rtac Follows_setsum 1);
+by (cut_facts_tac [Distrib] 1);
 by (auto_tac (claset(), 
-              simpset() addsimps [distr_follows_def, o_def]));
-by (best_tac (claset() addIs [impOfSubs (mono_bag_of RS mono_Follows_apply)]
-                       addDs [guaranteesD]) 1);
+              simpset() addsimps [distr_spec_def, distr_follows_def, o_def]));
+by (dtac guaranteesD 1); 
+by (best_tac (claset() addIs [impOfSubs (mono_bag_of RS mono_Follows_apply)]) 3);
+by Auto_tac;  
 qed "Distr_Bag_Follows";
 
+Close_locale "Distrib";
+
 
 Goal "!!f::nat=>nat. (INT i:(lessThan n). {s. f i <= g i s})  \
 \     <= {s. setsum f (lessThan n) <= setsum (%i. g i s) (lessThan n)}";
diff -r 947ee8608b90 -r 1a77667b21ef src/HOL/UNITY/AllocImpl.thy
--- a/src/HOL/UNITY/AllocImpl.thy	Fri Sep 22 17:25:09 2000 +0200
+++ b/src/HOL/UNITY/AllocImpl.thy	Sat Sep 23 16:02:01 2000 +0200
@@ -58,38 +58,43 @@
   (*spec (10)*)
   merge_increasing :: ('a,'b) merge_d program set
     "merge_increasing ==
-         UNIV guarantees[funPair merge.Out merge.iOut]
-         (Increasing merge.Out) Int (Increasing merge.iOut)"
+         UNIV guarantees (Increasing merge.Out) Int (Increasing merge.iOut)"
 
   (*spec (11)*)
   merge_eqOut :: ('a,'b) merge_d program set
     "merge_eqOut ==
-         UNIV guarantees[funPair merge.Out merge.iOut]
+         UNIV guarantees
          Always {s. length (merge.Out s) = length (merge.iOut s)}"
 
   (*spec (12)*)
   merge_bounded :: ('a,'b) merge_d program set
     "merge_bounded ==
-         UNIV guarantees[merge.iOut]
+         UNIV guarantees
          Always {s. ALL elt : set (merge.iOut s). elt < Nclients}"
 
   (*spec (13)*)
   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]
+	 guarantees
 	 (INT i : lessThan Nclients. 
 	  (%s. sublist (merge.Out s) 
                        {k. k < size(merge.iOut s) & merge.iOut s! k = i})
 	  Fols (sub i o merge.In))"
 
   (*spec: preserves part*)
-    merge_preserves :: ('a,'b) merge_d program set
-    "merge_preserves == preserves (funPair merge.In merge_d.dummy)"
+  merge_preserves :: ('a,'b) merge_d program set
+    "merge_preserves == preserves merge.In Int preserves merge_d.dummy"
+
+  (*environmental constraints*)
+  merge_allowed_acts :: ('a,'b) merge_d program set
+    "merge_allowed_acts ==
+       {F. AllowedActs F =
+	    insert Id (UNION (preserves (funPair merge.Out merge.iOut)) Acts)}"
 
   merge_spec :: ('a,'b) merge_d program set
     "merge_spec == merge_increasing Int merge_eqOut Int merge_bounded Int
-                   merge_follows Int merge_preserves"
+                   merge_follows Int merge_allowed_acts Int merge_preserves"
 
 (** Distributor specification (the number of outputs is Nclients) ***)
 
@@ -98,24 +103,30 @@
     "distr_follows ==
 	 Increasing distr.In Int Increasing distr.iIn Int
 	 Always {s. ALL elt : set (distr.iIn s). elt < Nclients}
-	 guarantees[distr.Out]
+	 guarantees
 	 (INT i : lessThan Nclients. 
 	  (sub i o distr.Out) Fols
 	  (%s. sublist (distr.In s) 
                        {k. k < size(distr.iIn s) & distr.iIn s ! k = i}))"
 
+  distr_allowed_acts :: ('a,'b) distr_d program set
+    "distr_allowed_acts ==
+       {D. AllowedActs D = insert Id (UNION (preserves distr.Out) Acts)}"
+
+  distr_spec :: ('a,'b) distr_d program set
+    "distr_spec == distr_follows Int distr_allowed_acts"
 
 (** Single-client allocator specification (required) ***)
 
   (*spec (18)*)
   alloc_increasing :: 'a allocState_d program set
-    "alloc_increasing == UNIV guarantees[giv] Increasing giv"
+    "alloc_increasing == UNIV  guarantees  Increasing giv"
 
   (*spec (19)*)
   alloc_safety :: 'a allocState_d program set
     "alloc_safety ==
 	 Increasing rel
-         guarantees[giv] Always {s. tokens (giv s) <= NbT + tokens (rel s)}"
+         guarantees  Always {s. tokens (giv s) <= NbT + tokens (rel s)}"
 
   (*spec (20)*)
   alloc_progress :: 'a allocState_d program set
@@ -126,86 +137,88 @@
          (INT h. {s. h <= giv s & h pfixGe (ask s)}
 		 LeadsTo
 	         {s. tokens h <= tokens (rel s)})
-         guarantees[giv]
-	     (INT h. {s. h <= ask s} LeadsTo {s. h pfixLe giv s})"
+         guarantees  (INT h. {s. h <= ask s} LeadsTo {s. h pfixLe giv s})"
 
   (*spec: preserves part*)
-    alloc_preserves :: 'a allocState_d program set
-    "alloc_preserves == preserves (funPair rel
-				   (funPair ask allocState_d.dummy))"
+  alloc_preserves :: 'a allocState_d program set
+    "alloc_preserves == preserves rel Int
+                        preserves ask Int
+                        preserves allocState_d.dummy"
   
+
+  (*environmental constraints*)
+  alloc_allowed_acts :: 'a allocState_d program set
+    "alloc_allowed_acts ==
+       {F. AllowedActs F = insert Id (UNION (preserves giv) Acts)}"
+
   alloc_spec :: 'a allocState_d program set
     "alloc_spec == alloc_increasing Int alloc_safety Int alloc_progress Int
-                   alloc_preserves"
+                   alloc_allowed_acts Int alloc_preserves"
+
+locale Merge =
+  fixes 
+    M   :: ('a,'b::order) merge_d program
+  assumes
+    Merge_spec  "M  : merge_spec"
+
+locale Distrib =
+  fixes 
+    D   :: ('a,'b::order) distr_d program
+  assumes
+    Distrib_spec  "D : distr_spec"
+
 
 (****
-    (** Network specification ***)
+#  (** Network specification ***)
 
-      (*spec (9.1)*)
-      network_ask :: 'a systemState program set
-	"network_ask == INT i : lessThan Nclients.
-			    Increasing (ask o sub i o client)
-			    guarantees[ask]
-			    (ask  Fols (ask o sub i o client))"
+#    (*spec (9.1)*)
+#    network_ask :: 'a systemState program set
+#	"network_ask == INT i : lessThan Nclients.
+#			    Increasing (ask o sub i o client)
+#			    guarantees[ask]
+#			    (ask  Fols (ask o sub i o client))"
 
-      (*spec (9.2)*)
-      network_giv :: 'a systemState program set
-	"network_giv == INT i : lessThan Nclients.
-			    Increasing giv 
-			    guarantees[giv o sub i o client]
-			    ((giv o sub i o client) Fols giv )"
+#    (*spec (9.2)*)
+#    network_giv :: 'a systemState program set
+#	"network_giv == INT i : lessThan Nclients.
+#			    Increasing giv 
+#			    guarantees[giv o sub i o client]
+#			    ((giv o sub i o client) Fols giv )"
 
-      (*spec (9.3)*)
-      network_rel :: 'a systemState program set
-	"network_rel == INT i : lessThan Nclients.
-			    Increasing (rel o sub i o client)
-			    guarantees[rel]
-			    (rel  Fols (rel o sub i o client))"
+#    (*spec (9.3)*)
+#    network_rel :: 'a systemState program set
+#	"network_rel == INT i : lessThan Nclients.
+#			    Increasing (rel o sub i o client)
+#			    guarantees[rel]
+#			    (rel  Fols (rel o sub i o client))"
 
-      (*spec: preserves part*)
-	network_preserves :: 'a systemState program set
-	"network_preserves == preserves giv  Int
-			      (INT i : lessThan Nclients.
-			       preserves (funPair rel ask o sub i o client))"
+#    (*spec: preserves part*)
+#	network_preserves :: 'a systemState program set
+#	"network_preserves == preserves giv  Int
+#			      (INT i : lessThan Nclients.
+#			       preserves (funPair rel ask o sub i o client))"
 
-      network_spec :: 'a systemState program set
-	"network_spec == network_ask Int network_giv Int
-			 network_rel Int network_preserves"
+#    network_spec :: 'a systemState program set
+#	"network_spec == network_ask Int network_giv Int
+#			 network_rel Int network_preserves"
 
 
-    (** State mappings **)
-      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,
-				 dummy    = xtr|)"
+#  (** State mappings **)
+#    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,
+#				 dummy    = xtr|)"
 
 
-      sysOfClient :: "(nat => merge) * 'a allocState_d => 'a systemState"
-	"sysOfClient == %(cl,al). (| giv = giv al,
-				     ask = ask al,
-				     rel = rel al,
-				     client   = cl,
-				     systemState.dummy = allocState_d.dummy al|)"
+#    sysOfClient :: "(nat => merge) * 'a allocState_d => 'a systemState"
+#	"sysOfClient == %(cl,al). (| giv = giv al,
+#				     ask = ask al,
+#				     rel = rel al,
+#				     client   = cl,
+#				     systemState.dummy = allocState_d.dummy al|)"
 ****)
 
-consts 
-    Alloc  :: 'a allocState_d program
-    Merge  :: ('a,'b) merge_d program
-
-(*    
-    Network :: 'a systemState program
-    System  :: 'a systemState program
-  *)
-  
-rules
-    Alloc   "Alloc   : alloc_spec"
-    Merge  "Merge  : merge_spec"
-
-(**    Network "Network : network_spec"**)
-
-
-
 end
diff -r 947ee8608b90 -r 1a77667b21ef src/HOL/UNITY/Client.ML
--- a/src/HOL/UNITY/Client.ML	Fri Sep 22 17:25:09 2000 +0200
+++ b/src/HOL/UNITY/Client.ML	Sat Sep 23 16:02:01 2000 +0200
@@ -6,15 +6,23 @@
 Distributed Resource Management System: the Client
 *)
 
-Addsimps [Client_def RS def_prg_Init];
+Addsimps [Client_def RS def_prg_Init, 
+          Client_def RS def_prg_AllowedActs];
 program_defs_ref := [Client_def];
 
 Addsimps (map simp_of_act [rel_act_def, tok_act_def, ask_act_def]);
 
+Goal "(Client ok G) = \
+\     (G : preserves rel & G : preserves ask & G : preserves tok &\
+\      Client : Allowed G)";
+by (auto_tac (claset(), 
+      simpset() addsimps [ok_iff_Allowed, Client_def RS def_prg_Allowed]));  
+qed "Client_ok_iff";
+AddIffs [Client_ok_iff];
+
 
 (*Safety property 1: ask, rel are increasing*)
-Goal "Client: UNIV guarantees[funPair rel ask] \
-\             Increasing ask Int Increasing rel";
+Goal "Client: UNIV guarantees Increasing ask Int Increasing rel";
 by (auto_tac
     (claset() addSIs [increasing_imp_Increasing],
      simpset() addsimps [guar_def, impOfSubs preserves_subset_increasing]));
@@ -23,7 +31,6 @@
 by Auto_tac;
 qed "increasing_ask_rel";
 
-
 Addsimps [nth_append, append_one_prefix];
 
 
@@ -31,10 +38,11 @@
       With no Substitution Axiom, we must prove the two invariants 
   simultaneously.
 *)
-Goal "G : preserves (funPair ask tok)  \
+Goal "Client ok G  \
 \     ==> Client Join G :  \
 \             Always ({s. tok s <= NbT}  Int  \
 \                     {s. ALL elt : set (ask s). elt <= NbT})";
+by Auto_tac;  
 by (rtac (invariantI RS stable_Join_Always2) 1);
 by (fast_tac (claset() addSEs [impOfSubs preserves_subset_stable]
 		       addSIs [stable_Int]) 3);
@@ -45,8 +53,7 @@
 
 (*export version, with no mention of tok in the postcondition, but
   unfortunately tok must be declared local.*)
-Goal "Client: UNIV guarantees[funPair ask tok] \
-\             Always {s. ALL elt : set (ask s). elt <= NbT}";
+Goal "Client: UNIV guarantees Always {s. ALL elt : set (ask s). elt <= NbT}";
 by (rtac guaranteesI 1);
 by (etac (ask_bounded_lemma RS Always_weaken) 1);
 by (rtac Int_lower2 1);
@@ -83,7 +90,7 @@
 qed "transient_lemma";
 
 
-Goal "[| Client Join G : Increasing giv;  G : preserves (funPair rel ask) |] \
+Goal "[| Client Join G : Increasing giv;  Client ok G |] \
 \ ==> Client Join G : {s. rel s = k & k<h & h <= giv s & h pfixGe ask s}  \
 \                     LeadsTo {s. k < rel s & rel s <= giv s & \
 \                                 h <= giv s & h pfixGe ask s}";
@@ -105,7 +112,7 @@
 qed "induct_lemma";
 
 
-Goal "[| Client Join G : Increasing giv;  G : preserves (funPair rel ask) |] \
+Goal "[| Client Join G : Increasing giv;  Client ok G |] \
 \ ==> Client Join G : {s. rel s < h & h <= giv s & h pfixGe ask s}  \
 \                     LeadsTo {s. h <= rel s}";
 by (res_inst_tac [("f", "%s. size h - size (rel s)")] LessThan_induct 1);
@@ -120,7 +127,7 @@
 qed "rel_progress_lemma";
 
 
-Goal "[| Client Join G : Increasing giv;  G : preserves (funPair rel ask) |] \
+Goal "[| Client Join G : Increasing giv;  Client ok G |] \
 \ ==> Client Join G : {s. h <= giv s & h pfixGe ask s}  \
 \                     LeadsTo {s. h <= rel s}";
 by (rtac (Join_Always_rel_le_giv RS Always_LeadsToI) 1);
@@ -133,7 +140,7 @@
 
 (*Progress property: all tokens that are given will be released*)
 Goal "Client : \
-\      Increasing giv  guarantees[funPair rel ask]  \
+\      Increasing giv  guarantees  \
 \      (INT h. {s. h <= giv s & h pfixGe ask s} LeadsTo {s. h <= rel s})";
 by (rtac guaranteesI 1);
 by (Clarify_tac 1);
@@ -158,7 +165,7 @@
 qed "stable_size_rel_le_giv";
 
 (*clients return the right number of tokens*)
-Goal "Client : Increasing giv  guarantees[rel]  Always {s. rel s <= giv s}";
+Goal "Client : Increasing giv  guarantees  Always {s. rel s <= giv s}";
 by (rtac guaranteesI 1);
 by (rtac AlwaysI 1);
 by (Force_tac 1);
diff -r 947ee8608b90 -r 1a77667b21ef src/HOL/UNITY/Client.thy
--- a/src/HOL/UNITY/Client.thy	Fri Sep 22 17:25:09 2000 +0200
+++ b/src/HOL/UNITY/Client.thy	Sat Sep 23 16:02:01 2000 +0200
@@ -48,9 +48,12 @@
 		         (s' = s (|ask := ask s @ [tok s]|))}"
 
   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})"
+    "Client ==
+       mk_program ({s. tok s : atMost NbT &
+		    giv s = [] & ask s = [] & rel s = []},
+		   {rel_act, tok_act, ask_act},
+		   UN G: preserves rel Int preserves ask Int preserves tok.
+		   Acts G)"
 
   (*Maybe want a special theory section to declare such maps*)
   non_dummy :: 'a state_d => state
diff -r 947ee8608b90 -r 1a77667b21ef src/HOL/UNITY/Common.ML
--- a/src/HOL/UNITY/Common.ML	Fri Sep 22 17:25:09 2000 +0200
+++ b/src/HOL/UNITY/Common.ML	Sat Sep 23 16:02:01 2000 +0200
@@ -36,21 +36,22 @@
 result();
 
 (*This one is  t := ftime t || t := gtime t*)
-Goal "mk_program (UNIV, {range(%t.(t,ftime t)), range(%t.(t,gtime t))}) \
+Goal "mk_program (UNIV, {range(%t.(t,ftime t)), range(%t.(t,gtime t))}, UNIV) \
 \      : {m} co (maxfg m)";
 by (simp_tac (simpset() addsimps [constrains_def, maxfg_def, 
 				  le_max_iff_disj, fasc]) 1);
 result();
 
 (*This one is  t := max (ftime t) (gtime t)*)
-Goal "mk_program (UNIV, {range(%t.(t, max (ftime t) (gtime t)))}) \
+Goal "mk_program (UNIV, {range(%t.(t, max (ftime t) (gtime t)))}, UNIV) \
 \      : {m} co (maxfg m)";
 by (simp_tac 
     (simpset() addsimps [constrains_def, maxfg_def, max_def, gasc]) 1);
 result();
 
 (*This one is  t := t+1 if t <max (ftime t) (gtime t) *)
-Goal "mk_program (UNIV, { {(t, Suc t) | t. t < max (ftime t) (gtime t)} }) \
+Goal "mk_program  \
+\         (UNIV, { {(t, Suc t) | t. t < max (ftime t) (gtime t)} }, UNIV)  \
 \      : {m} co (maxfg m)";
 by (simp_tac 
     (simpset() addsimps [constrains_def, maxfg_def, max_def, gasc]) 1);
diff -r 947ee8608b90 -r 1a77667b21ef src/HOL/UNITY/Common.thy
--- a/src/HOL/UNITY/Common.thy	Fri Sep 22 17:25:09 2000 +0200
+++ b/src/HOL/UNITY/Common.thy	Sat Sep 23 16:02:01 2000 +0200
@@ -10,7 +10,7 @@
 From Misra, "A Logic for Concurrent Programming" (1994), sections 5.1 and 13.1.
 *)
 
-Common = Union + 
+Common = SubstAx + 
 
 consts
   ftime,gtime :: nat=>nat
diff -r 947ee8608b90 -r 1a77667b21ef src/HOL/UNITY/Comp.ML
--- a/src/HOL/UNITY/Comp.ML	Fri Sep 22 17:25:09 2000 +0200
+++ b/src/HOL/UNITY/Comp.ML	Sat Sep 23 16:02:01 2000 +0200
@@ -19,7 +19,8 @@
 qed "componentI";
 
 Goalw [component_def]
-     "(F <= G) = (Init G <= Init F & Acts F <= Acts G)";
+     "(F <= G) = \
+\     (Init G <= Init F & Acts F <= Acts G & AllowedActs G <= AllowedActs F)";
 by (force_tac (claset() addSIs [exI, program_equalityI], 
 	       simpset()) 1);
 qed "component_eq_subset";
@@ -110,7 +111,11 @@
 by (Blast_tac 1);
 qed "JN_preserves";
 
-AddIffs [Join_preserves, JN_preserves];
+Goal "SKIP : preserves v";
+by (auto_tac (claset(), simpset() addsimps [preserves_def]));
+qed "SKIP_preserves";
+
+AddIffs [Join_preserves, JN_preserves, SKIP_preserves];
 
 Goalw [funPair_def] "(funPair f g) x = (f x, g x)";
 by (Simp_tac 1);
@@ -131,7 +136,6 @@
 by (simp_tac (simpset() addsimps [funPair_def, o_def]) 1);
 qed "funPair_o_distrib";
 
-
 Goal "fst o (funPair f g) = f";
 by (simp_tac (simpset() addsimps [funPair_def, o_def]) 1);
 qed "fst_o_funPair";
@@ -141,11 +145,9 @@
 qed "snd_o_funPair";
 Addsimps [fst_o_funPair, snd_o_funPair];
 
-
 Goal "preserves v <= preserves (w o v)";
 by (force_tac (claset(),
-	       simpset() addsimps [preserves_def, 
-				   stable_def, constrains_def]) 1);
+      simpset() addsimps [preserves_def, stable_def, constrains_def]) 1);
 qed "subset_preserves_o";
 
 Goal "preserves v <= stable {s. P (v s)}";
@@ -168,6 +170,15 @@
 qed "preserves_id_subset_stable";
 
 
+(** For use with def_UNION_ok_iff **)
+
+Goal "safety_prop (preserves v)";
+by (auto_tac (claset() addIs [safety_prop_INTER1], 
+              simpset() addsimps [preserves_def]));
+qed "safety_prop_preserves";
+AddIffs [safety_prop_preserves];
+
+
 (** Some lemmas used only in Client.ML **)
 
 Goal "[| F : stable {s. P (v s) (w s)};   \
diff -r 947ee8608b90 -r 1a77667b21ef src/HOL/UNITY/ELT.ML
--- a/src/HOL/UNITY/ELT.ML	Fri Sep 22 17:25:09 2000 +0200
+++ b/src/HOL/UNITY/ELT.ML	Sat Sep 23 16:02:01 2000 +0200
@@ -76,6 +76,7 @@
      "[| F: A ensures B;  A-B: insert {} CC |] ==> F : A leadsTo[CC] B";
 by (blast_tac (claset() addIs [elt.Basis]) 1);
 qed "leadsETo_Basis";
+AddIs [leadsETo_Basis];
 
 Goalw [leadsETo_def]
      "[| F : A leadsTo[CC] B;  F : B leadsTo[CC] C |] ==> F : A leadsTo[CC] C";
@@ -350,7 +351,7 @@
 by (etac leadsETo_induct 1);
 by (blast_tac (claset() addIs [leadsTo_Union]) 3);
 by (blast_tac (claset() addIs [leadsTo_Trans]) 2);
-by (blast_tac (claset() addIs [leadsTo_Basis]) 1);
+by (Blast_tac 1);
 qed "leadsETo_subset_leadsTo";
 
 Goal "(A leadsTo[UNIV] B) = (A leadsTo B)";
@@ -360,7 +361,7 @@
 by (etac leadsTo_induct 1);
 by (blast_tac (claset() addIs [leadsETo_Union]) 3);
 by (blast_tac (claset() addIs [leadsETo_Trans]) 2);
-by (blast_tac (claset() addIs [leadsETo_Basis]) 1);
+by (Blast_tac 1);
 qed "leadsETo_UNIV_eq_leadsTo";
 
 (**** weak ****)
@@ -595,7 +596,8 @@
 qed "project_LeadsETo_D";
 
 Goalw [extending_def]
-     "extending (v o f) (%G. UNIV) h F \
+     "(ALL G. extend h F ok G --> G : preserves (v o f)) \
+\     ==> extending (%G. UNIV) h F \
 \               (extend_set h A leadsTo[givenBy (v o f)] extend_set h B) \
 \               (A leadsTo[givenBy v] B)";
 by (auto_tac (claset(), simpset() addsimps [project_leadsETo_D]));
@@ -603,7 +605,8 @@
 
 
 Goalw [extending_def]
-     "extending (v o f) (%G. reachable (extend h F Join G)) h F \
+     "(ALL G. extend h F ok G --> G : preserves (v o f)) \
+\     ==> extending (%G. reachable (extend h F Join G)) h F \
 \               (extend_set h A LeadsTo[givenBy (v o f)] extend_set h B) \
 \               (A LeadsTo[givenBy v]  B)";
 by (blast_tac (claset() addIs [project_LeadsETo_D]) 1);
@@ -637,8 +640,7 @@
 by (asm_full_simp_tac 
     (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);
+by (blast_tac (claset() addIs [ensures_extend_set_imp_project_ensures]) 1);
 
 qed "project_leadsETo_I_lemma";
 
diff -r 947ee8608b90 -r 1a77667b21ef src/HOL/UNITY/Extend.ML
--- a/src/HOL/UNITY/Extend.ML	Fri Sep 22 17:25:09 2000 +0200
+++ b/src/HOL/UNITY/Extend.ML	Sat Sep 23 16:02:01 2000 +0200
@@ -288,6 +288,7 @@
      "project_act h (extend_act h act) = act";
 by (Blast_tac 1);
 qed "extend_act_inverse";
+Addsimps [extend_act_inverse];
 
 Goalw [extend_act_def, project_act_def]
      "project_act h (Restrict C (extend_act h act)) = \
@@ -345,7 +346,7 @@
               simpset() addsimps [split_extended_all]) 1);
 qed "Domain_project_act";
 
-Addsimps [extend_act_Id];
+Addsimps [extend_act_Id, project_act_Id];
 
 
 (**** extend ****)
@@ -355,21 +356,43 @@
 Goalw [extend_def] "Init (extend h F) = extend_set h (Init F)";
 by Auto_tac;
 qed "Init_extend";
+Addsimps [Init_extend];
 
 Goalw [project_def] "Init (project h C F) = project_set h (Init F)";
 by Auto_tac;
 qed "Init_project";
+Addsimps [Init_project];
 
 Goal "Acts (extend h F) = (extend_act h `` Acts F)";
 by (simp_tac (simpset() addsimps [extend_def, insert_Id_image_Acts]) 1);
 qed "Acts_extend";
+Addsimps [Acts_extend];
+
+Goal "AllowedActs (extend h F) = project_act h -`` AllowedActs F";
+by (simp_tac (simpset() addsimps [extend_def, insert_absorb]) 1);
+qed "AllowedActs_extend";
+Addsimps [AllowedActs_extend];
 
 Goal "Acts(project h C F) = insert Id (project_act h `` Restrict C `` Acts F)";
 by (auto_tac (claset(), 
 	      simpset() addsimps [project_def, image_iff]));
 qed "Acts_project";
+Addsimps [Acts_project];
 
-Addsimps [Init_extend, Init_project, Acts_extend, Acts_project];
+Goal "AllowedActs(project h C F) = \
+\       {act. Restrict (project_set h C) act \
+\              : project_act h `` Restrict C `` AllowedActs F}";
+by (simp_tac (simpset() addsimps [project_def, image_iff]) 1);
+by (stac insert_absorb 1);
+by (auto_tac (claset() addSIs [inst "x" "Id" bexI], 
+                 simpset() addsimps [project_act_def]));  
+qed "AllowedActs_project";
+Addsimps [AllowedActs_project];
+
+Goal "Allowed (extend h F) = project h UNIV -`` Allowed F";
+by (simp_tac (simpset() addsimps [AllowedActs_extend, Allowed_def]) 1);
+by (Blast_tac 1); 
+qed "Allowed_extend";
 
 Goalw [SKIP_def] "extend h SKIP = SKIP";
 by (rtac program_equalityI 1);
@@ -386,31 +409,51 @@
 by (Blast_tac 1);
 qed "project_set_Union";
 
+(*Converse FAILS: the extended state contributing to project_set h C
+  may not coincide with the one contributing to project_act h act*)
+Goal "project_act h (Restrict C act) <= \
+\     Restrict (project_set h C) (project_act h act)";
+by (auto_tac (claset(), simpset() addsimps [project_act_def]));  
+qed "project_act_Restrict_subset";
+
+
+Goal "project_act h (Restrict C Id) = Restrict (project_set h C) Id";
+by (auto_tac (claset(), simpset() addsimps [project_act_def]));  
+qed "project_act_Restrict_Id_eq";
+
 Goal "project h C (extend h F) = \
-\     mk_program (Init F, Restrict (project_set h C) `` Acts F)";
+\     mk_program (Init F, Restrict (project_set h C) `` Acts F, \
+\                 {act. Restrict (project_set h C) act : project_act h `` Restrict C `` (project_act h -`` AllowedActs F)})";
 by (rtac program_equalityI 1);
 by (asm_simp_tac (simpset() addsimps [image_eq_UN]) 2);
 by (Simp_tac 1);
+by (simp_tac (simpset() addsimps [project_def]) 1);
 qed "project_extend_eq";
 
-(*ALL act: Acts F. Domain act is MUCH TOO STRONG since Domain Id = UNIV!*)
-Goal "UNIV <= project_set h C \
-\     ==> project h C (extend h F) = F";
+Goal "project h UNIV (extend h F) = F";
 by (asm_simp_tac (simpset() addsimps [project_extend_eq, image_eq_UN, 
                    subset_UNIV RS subset_trans RS Restrict_triv]) 1);
+by (rtac program_equalityI 1);
+by (ALLGOALS Simp_tac);
+by (stac insert_absorb 1);
+by (simp_tac (simpset() addsimps [inst "x" "Id" bexI]) 1); 
+by Auto_tac;  
+by (rename_tac "act" 1);
+by (res_inst_tac [("x","extend_act h act")] bexI 1);
+by Auto_tac;  
 qed "extend_inverse";
 Addsimps [extend_inverse];
 
 Goal "inj (extend h)";
 by (rtac inj_on_inverseI 1);
 by (rtac extend_inverse 1);
-by (Force_tac 1);
 qed "inj_extend";
 
 Goal "extend h (F Join G) = extend h F Join extend h G";
 by (rtac program_equalityI 1);
 by (simp_tac (simpset() addsimps [image_Un]) 2);
 by (simp_tac (simpset() addsimps [extend_set_Int_distrib]) 1);
+by Auto_tac;  
 qed "extend_Join";
 Addsimps [extend_Join];
 
@@ -418,6 +461,7 @@
 by (rtac program_equalityI 1);
 by (simp_tac (simpset() addsimps [image_UN]) 2);
 by (simp_tac (simpset() addsimps [extend_set_INT_distrib]) 1);
+by Auto_tac;  
 qed "extend_JN";
 Addsimps [extend_JN];
 
@@ -430,7 +474,7 @@
 
 Goal "F <= G ==> project h C F <= project h C G";
 by (full_simp_tac (simpset() addsimps [component_eq_subset]) 1);
-by Auto_tac;
+by (Blast_tac 1); 
 qed "project_mono";
 
 
@@ -685,9 +729,9 @@
 
 Goal "project h UNIV ((extend h F) Join G) = F Join (project h UNIV G)";
 by (rtac program_equalityI 1);
-by (asm_simp_tac
-    (simpset() addsimps [image_eq_UN, UN_Un, extend_act_inverse]) 2);
+by (simp_tac (simpset() addsimps [image_eq_UN, UN_Un]) 2);
 by (simp_tac (simpset() addsimps [project_set_extend_set_Int]) 1);
+by Auto_tac;  
 qed "project_extend_Join";
 
 Goal "(extend h F) Join G = extend h H ==> H = F Join (project h UNIV G)";
@@ -698,26 +742,44 @@
 (** Strong precondition and postcondition; only useful when
     the old and new state sets are in bijection **)
 
-Goal "F : X guarantees[v] Y ==> \
-\     extend h F : (extend h `` X) guarantees[v o f] (extend h `` Y)";
+
+Goal "extend h F ok G ==> F ok project h UNIV G";
+by (auto_tac (claset(), simpset() addsimps [ok_def]));
+by (dtac subsetD 1);   
+by (auto_tac (claset() addSIs [rev_image_eqI], simpset()));  
+qed "ok_extend_imp_ok_project";
+
+Goal "(extend h F ok extend h G) = (F ok G)";
+by (auto_tac (claset(), simpset() addsimps [ok_def]));  
+qed "ok_extend_iff";
+
+Goal "OK I (%i. extend h (F i)) = (OK I F)";
+by (auto_tac (claset(), simpset() addsimps [OK_def]));  
+by (dres_inst_tac [("x","i")] bspec 1); 
+by (dres_inst_tac [("x","j")] bspec 2); 
+by Auto_tac;  
+qed "OK_extend_iff";
+
+Goal "F : X guarantees Y ==> \
+\     extend h F : (extend h `` X) guarantees (extend h `` Y)";
 by (rtac guaranteesI 1);
-by Auto_tac;
-by (blast_tac (claset() addIs [project_preserves_I]
-			addDs [extend_Join_eq_extend_D, guaranteesD]) 1);
+by (Clarify_tac 1);
+by (blast_tac (claset() addDs [ok_extend_imp_ok_project, 
+                               extend_Join_eq_extend_D, guaranteesD]) 1);
 qed "guarantees_imp_extend_guarantees";
 
-Goal "extend h F : (extend h `` X) guarantees[v o f] (extend h `` Y) \
-\     ==> F : X guarantees[v] Y";
+Goal "extend h F : (extend h `` X) guarantees (extend h `` Y) \
+\     ==> F : X guarantees Y";
 by (auto_tac (claset(), simpset() addsimps [guar_def]));
-by (dres_inst_tac [("x", "extend h G")] bspec 1);
+by (dres_inst_tac [("x", "extend h G")] spec 1);
 by (asm_full_simp_tac 
     (simpset() delsimps [extend_Join] 
-           addsimps [extend_Join RS sym, inj_extend RS inj_image_mem_iff]) 2);
-by (asm_simp_tac (simpset() addsimps [extend_preserves]) 1);
+               addsimps [extend_Join RS sym, ok_extend_iff, 
+                         inj_extend RS inj_image_mem_iff]) 1);
 qed "extend_guarantees_imp_guarantees";
 
-Goal "(extend h F : (extend h `` X) guarantees[v o f] (extend h `` Y)) = \
-\    (F : X guarantees[v] Y)";
+Goal "(extend h F : (extend h `` X) guarantees (extend h `` Y)) = \
+\    (F : X guarantees Y)";
 by (blast_tac (claset() addIs [guarantees_imp_extend_guarantees,
 			       extend_guarantees_imp_guarantees]) 1);
 qed "extend_guarantees_eq";
diff -r 947ee8608b90 -r 1a77667b21ef src/HOL/UNITY/Extend.thy
--- a/src/HOL/UNITY/Extend.thy	Fri Sep 22 17:25:09 2000 +0200
+++ b/src/HOL/UNITY/Extend.thy	Sat Sep 23 16:02:01 2000 +0200
@@ -34,12 +34,16 @@
 
   extend :: "['a*'b => 'c, 'a program] => 'c program"
     "extend h F == mk_program (extend_set h (Init F),
-			       extend_act h `` Acts F)"
+			       extend_act h `` Acts F,
+			       project_act h -`` AllowedActs F)"
 
   (*Argument C allows weak safety laws to be projected*)
   project :: "['a*'b => 'c, 'c set, 'c program] => 'a program"
-    "project h C F == mk_program (project_set h (Init F),
-		  	          project_act h `` Restrict C `` Acts F)"
+    "project h C F ==
+       mk_program (project_set h (Init F),
+		   project_act h `` Restrict C `` Acts F,
+		   {act. Restrict (project_set h C) act :
+		         project_act h `` Restrict C `` AllowedActs F})"
 
 locale Extend =
   fixes 
diff -r 947ee8608b90 -r 1a77667b21ef src/HOL/UNITY/Guar.ML
--- a/src/HOL/UNITY/Guar.ML	Fri Sep 22 17:25:09 2000 +0200
+++ b/src/HOL/UNITY/Guar.ML	Sat Sep 23 16:02:01 2000 +0200
@@ -65,14 +65,14 @@
 (*** guarantees ***)
 
 val prems = Goal
-     "(!!G. [| G : preserves v; F Join G : X |] ==> F Join G : Y) \
-\     ==> F : X guarantees[v] Y";
+     "(!!G. [| F ok G; F Join G : X |] ==> F Join G : Y) \
+\     ==> F : X guarantees Y";
 by (simp_tac (simpset() addsimps [guar_def, component_def]) 1);
 by (blast_tac (claset() addIs prems) 1);
 qed "guaranteesI";
 
 Goalw [guar_def, component_def]
-     "[| F : X guarantees[v] Y;  G : preserves v;  F Join G : X |] \
+     "[| F : X guarantees Y;  F ok G;  F Join G : X |] \
 \     ==> F Join G : Y";
 by (Blast_tac 1);
 qed "guaranteesD";
@@ -80,33 +80,27 @@
 (*This version of guaranteesD matches more easily in the conclusion
   The major premise can no longer be  F<=H since we need to reason about G*)
 Goalw [guar_def]
-     "[| F : X guarantees[v] Y;  F Join G = H;  H : X;  G : preserves v |] \
+     "[| F : X guarantees Y;  F Join G = H;  H : X;  F ok G |] \
 \     ==> H : Y";
 by (Blast_tac 1);
 qed "component_guaranteesD";
 
 Goalw [guar_def]
-     "[| F: X guarantees[v] X'; Y <= X; X' <= Y' |] ==> F: Y guarantees[v] Y'";
+     "[| F: X guarantees X'; Y <= X; X' <= Y' |] ==> F: Y guarantees Y'";
 by (Blast_tac 1);
 qed "guarantees_weaken";
 
-Goalw [guar_def]
-     "[| F: X guarantees[v] Y;  preserves w <= preserves v |] \
-\     ==> F: X guarantees[w] Y";
-by (Blast_tac 1);
-qed "guarantees_weaken_var";
-
-Goalw [guar_def] "X <= Y ==> X guarantees[v] Y = UNIV";
+Goalw [guar_def] "X <= Y ==> X guarantees Y = UNIV";
 by (Blast_tac 1);
 qed "subset_imp_guarantees_UNIV";
 
 (*Equivalent to subset_imp_guarantees_UNIV but more intuitive*)
-Goalw [guar_def] "X <= Y ==> F : X guarantees[v] Y";
+Goalw [guar_def] "X <= Y ==> F : X guarantees Y";
 by (Blast_tac 1);
 qed "subset_imp_guarantees";
 
 (*Remark at end of section 4.1
-Goalw [guar_def] "ex_prop Y = (Y = UNIV guarantees[v] Y)";
+Goalw [guar_def] "ex_prop Y = (Y = UNIV guarantees Y)";
 by (simp_tac (simpset() addsimps [ex_prop_equiv]) 1);
 by (blast_tac (claset() addEs [equalityE]) 1);
 qed "ex_prop_equiv2";
@@ -115,40 +109,40 @@
 (** Distributive laws.  Re-orient to perform miniscoping **)
 
 Goalw [guar_def]
-     "(UN i:I. X i) guarantees[v] Y = (INT i:I. X i guarantees[v] Y)";
+     "(UN i:I. X i) guarantees Y = (INT i:I. X i guarantees Y)";
 by (Blast_tac 1);
 qed "guarantees_UN_left";
 
 Goalw [guar_def]
-     "(X Un Y) guarantees[v] Z = (X guarantees[v] Z) Int (Y guarantees[v] Z)";
+     "(X Un Y) guarantees Z = (X guarantees Z) Int (Y guarantees Z)";
 by (Blast_tac 1);
 qed "guarantees_Un_left";
 
 Goalw [guar_def]
-     "X guarantees[v] (INT i:I. Y i) = (INT i:I. X guarantees[v] Y i)";
+     "X guarantees (INT i:I. Y i) = (INT i:I. X guarantees Y i)";
 by (Blast_tac 1);
 qed "guarantees_INT_right";
 
 Goalw [guar_def]
-     "Z guarantees[v] (X Int Y) = (Z guarantees[v] X) Int (Z guarantees[v] Y)";
+     "Z guarantees (X Int Y) = (Z guarantees X) Int (Z guarantees Y)";
 by (Blast_tac 1);
 qed "guarantees_Int_right";
 
-Goal "[| F : Z guarantees[v] X;  F : Z guarantees[v] Y |] \
-\    ==> F : Z guarantees[v] (X Int Y)";
+Goal "[| F : Z guarantees X;  F : Z guarantees Y |] \
+\    ==> F : Z guarantees (X Int Y)";
 by (asm_simp_tac (simpset() addsimps [guarantees_Int_right]) 1);
 qed "guarantees_Int_right_I";
 
-Goal "(F : X guarantees[v] (INTER I Y)) = \
-\     (ALL i:I. F : X guarantees[v] (Y i))";
+Goal "(F : X guarantees (INTER I Y)) = \
+\     (ALL i:I. F : X guarantees (Y i))";
 by (simp_tac (simpset() addsimps [guarantees_INT_right]) 1);
 qed "guarantees_INT_right_iff";
 
-Goalw [guar_def] "(X guarantees[v] Y) = (UNIV guarantees[v] (-X Un Y))";
+Goalw [guar_def] "(X guarantees Y) = (UNIV guarantees (-X Un Y))";
 by (Blast_tac 1);
 qed "shunting";
 
-Goalw [guar_def] "(X guarantees[v] Y) = -Y guarantees[v] -X";
+Goalw [guar_def] "(X guarantees Y) = -Y guarantees -X";
 by (Blast_tac 1);
 qed "contrapositive";
 
@@ -157,119 +151,115 @@
 **)
 
 Goalw [guar_def]
-    "[| F : V guarantees[v] X;  F : (X Int Y) guarantees[v] Z |]\
-\    ==> F : (V Int Y) guarantees[v] Z";
+    "[| F : V guarantees X;  F : (X Int Y) guarantees Z |]\
+\    ==> F : (V Int Y) guarantees Z";
 by (Blast_tac 1);
 qed "combining1";
 
 Goalw [guar_def]
-    "[| F : V guarantees[v] (X Un Y);  F : Y guarantees[v] Z |]\
-\    ==> F : V guarantees[v] (X Un Z)";
+    "[| F : V guarantees (X Un Y);  F : Y guarantees Z |]\
+\    ==> F : V guarantees (X Un Z)";
 by (Blast_tac 1);
 qed "combining2";
 
 (** The following two follow Chandy-Sanders, but the use of object-quantifiers
     does not suit Isabelle... **)
 
-(*Premise should be (!!i. i: I ==> F: X guarantees[v] Y i) *)
+(*Premise should be (!!i. i: I ==> F: X guarantees Y i) *)
 Goalw [guar_def]
-     "ALL i:I. F : X guarantees[v] (Y i) ==> F : X guarantees[v] (INT i:I. Y i)";
+     "ALL i:I. F : X guarantees (Y i) ==> F : X guarantees (INT i:I. Y i)";
 by (Blast_tac 1);
 qed "all_guarantees";
 
-(*Premises should be [| F: X guarantees[v] Y i; i: I |] *)
+(*Premises should be [| F: X guarantees Y i; i: I |] *)
 Goalw [guar_def]
-     "EX i:I. F : X guarantees[v] (Y i) ==> F : X guarantees[v] (UN i:I. Y i)";
+     "EX i:I. F : X guarantees (Y i) ==> F : X guarantees (UN i:I. Y i)";
 by (Blast_tac 1);
 qed "ex_guarantees";
 
 (*** Additional guarantees laws, by lcp ***)
 
 Goalw [guar_def]
-    "[| F: U guarantees[v] V;  G: X guarantees[v] Y; \
-\       F : preserves v;  G : preserves v |] \
-\    ==> F Join G: (U Int X) guarantees[v] (V Int Y)";
+    "[| F: U guarantees V;  G: X guarantees Y; F ok G |] \
+\    ==> F Join G: (U Int X) guarantees (V Int Y)"; 
 by (Simp_tac 1);
 by Safe_tac;
 by (asm_full_simp_tac (simpset() addsimps [Join_assoc]) 1);
 by (subgoal_tac "F Join G Join Ga = G Join (F Join Ga)" 1);
-by (Asm_full_simp_tac 1);
+by (asm_full_simp_tac (simpset() addsimps [ok_commute]) 1); 
 by (asm_simp_tac (simpset() addsimps Join_ac) 1);
 qed "guarantees_Join_Int";
 
 Goalw [guar_def]
-    "[| F: U guarantees[v] V;  G: X guarantees[v] Y; \
-\       F : preserves v;  G : preserves v |]  \
-\    ==> F Join G: (U Un X) guarantees[v] (V Un Y)";
+    "[| F: U guarantees V;  G: X guarantees Y; F ok G |]  \
+\    ==> F Join G: (U Un X) guarantees (V Un Y)";
 by (Simp_tac 1);
 by Safe_tac;
 by (asm_full_simp_tac (simpset() addsimps [Join_assoc]) 1);
 by (subgoal_tac "F Join G Join Ga = G Join (F Join Ga)" 1);
-by (Asm_full_simp_tac 1);
+by (asm_full_simp_tac (simpset() addsimps [ok_commute]) 1);
 by (asm_simp_tac (simpset() addsimps Join_ac) 1);
 qed "guarantees_Join_Un";
 
 Goalw [guar_def]
-     "[| ALL i:I. F i : X i guarantees[v] Y i;  \
-\        ALL i:I. F i : preserves v |] \
-\     ==> (JOIN I F) : (INTER I X) guarantees[v] (INTER I Y)";
+     "[| ALL i:I. F i : X i guarantees Y i;  OK I F |] \
+\     ==> (JOIN I F) : (INTER I X) guarantees (INTER I Y)";
 by Auto_tac;
 by (ball_tac 1);
-by (dres_inst_tac [("x", "JOIN I F Join G")] bspec 1);
+by (rename_tac "i" 1);
+by (dres_inst_tac [("x", "JOIN (I-{i}) F Join G")] spec 1);
 by (auto_tac
-    (claset(),
-     simpset() addsimps [Join_assoc RS sym, JN_absorb]));
+    (claset() addIs [OK_imp_ok],
+     simpset() addsimps [Join_assoc RS sym, JN_Join_diff, JN_absorb]));
 qed "guarantees_JN_INT";
 
 Goalw [guar_def]
-    "[| ALL i:I. F i : X i guarantees[v] Y i;  \
-\       ALL i:I. F i : preserves v |] \
-\    ==> (JOIN I F) : (INTER I X) guarantees[v] (INTER I Y)";
+    "[| ALL i:I. F i : X i guarantees Y i;  OK I F |] \
+\    ==> (JOIN I F) : (INTER I X) guarantees (INTER I Y)";
 by Auto_tac;
 by (ball_tac 1);
-by (dres_inst_tac [("x", "JOIN I F Join G")] bspec 1);
+by (rename_tac "i" 1);
+by (dres_inst_tac [("x", "JOIN (I-{i}) F Join G")] spec 1);
 by (auto_tac
-    (claset(),
-     simpset() addsimps [Join_assoc RS sym, JN_absorb]));
+    (claset() addIs [OK_imp_ok],
+     simpset() addsimps [Join_assoc RS sym, JN_Join_diff, JN_absorb]));
 qed "guarantees_JN_INT";
 
 Goalw [guar_def]
-    "[| ALL i:I. F i : X i guarantees[v] Y i;  \
-\       ALL i:I. F i : preserves v |] \
-\    ==> (JOIN I F) : (UNION I X) guarantees[v] (UNION I Y)";
+    "[| ALL i:I. F i : X i guarantees Y i;  OK I F |] \
+\    ==> (JOIN I F) : (UNION I X) guarantees (UNION I Y)";
 by Auto_tac;
 by (ball_tac 1);
-by (dres_inst_tac [("x", "JOIN I F Join G")] bspec 1);
+by (rename_tac "i" 1);
+by (dres_inst_tac [("x", "JOIN (I-{i}) F Join G")] spec 1);
 by (auto_tac
-    (claset(),
-     simpset() addsimps [Join_assoc RS sym, JN_absorb]));
+    (claset() addIs [OK_imp_ok],
+     simpset() addsimps [Join_assoc RS sym, JN_Join_diff, JN_absorb]));
 qed "guarantees_JN_UN";
 
 
-(*** guarantees[v] laws for breaking down the program, by lcp ***)
+(*** guarantees laws for breaking down the program, by lcp ***)
 
 Goalw [guar_def]
-     "[| F: X guarantees[v] Y;  G: preserves v |] \
-\     ==> F Join G: X guarantees[v] Y";
+     "[| F: X guarantees Y;  F ok G |] ==> F Join G: X guarantees Y";
 by (Simp_tac 1);
 by Safe_tac;
 by (asm_full_simp_tac (simpset() addsimps [Join_assoc]) 1);
 qed "guarantees_Join_I1";
 
-Goal "[| G: X guarantees[v] Y;  F: preserves v |] \
-\    ==> F Join G: X guarantees[v] Y";
-by (stac Join_commute 1);
+Goal "[| G: X guarantees Y;  F ok G |] ==> F Join G: X guarantees Y";
+by (asm_full_simp_tac (simpset() addsimps [inst "G" "G" Join_commute, 
+                                           inst "G" "G" ok_commute]) 1);
 by (blast_tac (claset() addIs [guarantees_Join_I1]) 1);
 qed "guarantees_Join_I2";
 
 Goalw [guar_def]
-     "[| i : I;  F i: X guarantees[v] Y;  \
-\        ALL j:I. i~=j --> F j : preserves v |] \
-\     ==> (JN i:I. (F i)) : X guarantees[v] Y";
+     "[| i : I;  F i: X guarantees Y;  OK I F |] \
+\     ==> (JN i:I. (F i)) : X guarantees Y";
 by (Clarify_tac 1);
-by (dres_inst_tac [("x", "JOIN (I-{i}) F Join G")] bspec 1);
-by (auto_tac (claset(),
-	      simpset() addsimps [JN_Join_diff, Join_assoc RS sym]));
+by (dres_inst_tac [("x", "JOIN (I-{i}) F Join G")] spec 1);
+by (auto_tac (claset() addIs [OK_imp_ok],
+	      simpset() addsimps [JN_Join_diff, JN_Join_diff, Join_assoc RS sym]));
 qed "guarantees_JN_I";
 
 
diff -r 947ee8608b90 -r 1a77667b21ef src/HOL/UNITY/Guar.thy
--- a/src/HOL/UNITY/Guar.thy	Fri Sep 22 17:25:09 2000 +0200
+++ b/src/HOL/UNITY/Guar.thy	Sat Sep 23 16:02:01 2000 +0200
@@ -35,11 +35,9 @@
   welldef :: 'a program set  
    "welldef == {F. Init F ~= {}}"
 
-  guar :: ['a program set, 'a=>'b, 'a program set] => 'a program set
-   ("(_/ guarantees[_]/ _)" [55,0,55] 55)
-                              (*higher than membership, lower than Co*)
-   "X guarantees[v] Y == {F. ALL G : preserves v. 
-                               F Join G : X --> F Join G : Y}"
+  guar :: ['a program set, 'a program set] => 'a program set
+          (infixl "guarantees" 55)  (*higher than membership, lower than Co*)
+   "X guarantees Y == {F. ALL G. F ok G --> F Join G : X --> F Join G : Y}"
 
   refines :: ['a program, 'a program, 'a program set] => bool
 			("(3_ refines _ wrt _)" [10,10,10] 10)
diff -r 947ee8608b90 -r 1a77667b21ef src/HOL/UNITY/Handshake.thy
--- a/src/HOL/UNITY/Handshake.thy	Fri Sep 22 17:25:09 2000 +0200
+++ b/src/HOL/UNITY/Handshake.thy	Sat Sep 23 16:02:01 2000 +0200
@@ -21,14 +21,14 @@
     "cmdF == {(s,s'). s' = s (|NF:= Suc(NF s), BB:=False|) & BB s}"
 
   F :: "state program"
-    "F == mk_program ({s. NF s = 0 & BB s}, {cmdF})"
+    "F == mk_program ({s. NF s = 0 & BB s}, {cmdF}, UNIV)"
 
   (*G's program*)
   cmdG :: "(state*state) set"
     "cmdG == {(s,s'). s' = s (|NG:= Suc(NG s), BB:=True|) & ~ BB s}"
 
   G :: "state program"
-    "G == mk_program ({s. NG s = 0 & BB s}, {cmdG})"
+    "G == mk_program ({s. NG s = 0 & BB s}, {cmdG}, UNIV)"
 
   (*the joint invariant*)
   invFG :: "state set"
diff -r 947ee8608b90 -r 1a77667b21ef src/HOL/UNITY/Lift.thy
--- a/src/HOL/UNITY/Lift.thy	Fri Sep 22 17:25:09 2000 +0200
+++ b/src/HOL/UNITY/Lift.thy	Sat Sep 23 16:02:01 2000 +0200
@@ -108,6 +108,10 @@
          {(s,s'). s' = s (|floor := floor s - #1|)
 		       & ~ stop s & ~ up s & floor s ~: req s}"
 
+  (*This action is omitted from prior treatments, which therefore are
+    unrealistic: nobody asks the lift to do anything!  But adding this
+    action invalidates many of the existing progress arguments: various
+    "ensures" properties fail.*)
   button_press  :: "(state*state) set"
     "button_press ==
          {(s,s'). EX n. s' = s (|req := insert n (req s)|)
@@ -119,7 +123,8 @@
     "Lift == mk_program ({s. floor s = Min & ~ up s & move s & stop s &
 		          ~ open s & req s = {}},
 			 {request_act, open_act, close_act,
-			  req_up, req_down, move_up, move_down})"
+			  req_up, req_down, move_up, move_down},
+			 UNIV)"
 
 
   (** Invariants **)
diff -r 947ee8608b90 -r 1a77667b21ef src/HOL/UNITY/Lift_prog.ML
--- a/src/HOL/UNITY/Lift_prog.ML	Fri Sep 22 17:25:09 2000 +0200
+++ b/src/HOL/UNITY/Lift_prog.ML	Sat Sep 23 16:02:01 2000 +0200
@@ -133,6 +133,11 @@
 
 (*** the lattice operations ***)
 
+Goal "bij (lift i)";
+by (simp_tac (simpset() addsimps [lift_def]) 1);
+qed "bij_lift";
+AddIffs [bij_lift];
+
 Goalw [lift_def] "lift i SKIP = SKIP";
 by (Asm_simp_tac 1);
 qed "lift_SKIP";
@@ -209,15 +214,14 @@
 (** guarantees **)
 
 Goalw [lift_def]
-     "(lift i F : (lift i `` X) guarantees[v o drop_map i] (lift i `` Y)) = \
-\     (F : X guarantees[v] Y)";
+     "(lift i F : (lift i `` X) guarantees (lift i `` Y)) = \
+\     (F : X guarantees Y)";
 by (stac (bij_lift_map RS rename_rename_guarantees_eq RS sym) 1);
 by (asm_simp_tac (simpset() addsimps [o_def]) 1);
 qed "lift_lift_guarantees_eq";
 
-Goal "(lift i F : X guarantees[v] Y) = \
-\     (F : (rename (drop_map i) `` X) guarantees[v o lift_map i] \
-\          (rename (drop_map i) `` Y))";
+Goal "(lift i F : X guarantees Y) = \
+\     (F : (rename (drop_map i) `` X) guarantees (rename (drop_map i) `` Y))";
 by (asm_simp_tac 
     (simpset() addsimps [bij_lift_map RS rename_guarantees_eq_rename_inv,
 			 lift_def]) 1);
@@ -409,4 +413,74 @@
 Addsimps (make_o_equivs fst_o_lift_map @ make_o_equivs snd_o_lift_map);
 
 
+(*** More lemmas about extend and project 
+     They could be moved to {Extend,Project}.ML, but DON'T need the locale ***)
 
+Goal "extend_act h' (extend_act h act) = \
+\     extend_act (%(x,(y,y')). h'(h(x,y),y')) act";
+by (auto_tac (claset() addSEs [rev_bexI], 
+              simpset() addsimps [extend_act_def]));
+by (ALLGOALS Blast_tac);
+qed "extend_act_extend_act";
+
+Goal "project_act h (project_act h' act) = \
+\     project_act (%(x,(y,y')). h'(h(x,y),y')) act";
+by (auto_tac (claset() addSEs [rev_bexI], 
+              simpset() addsimps [project_act_def]));    
+qed "project_act_project_act";
+
+Goal "project_act h (extend_act h' act) = \
+\       {(x,x'). EX s s' y y' z. (s,s') : act & \
+\                h(x,y) = h'(s,z) & h(x',y') = h'(s',z)}";
+by (simp_tac (simpset() addsimps [extend_act_def, project_act_def]) 1); 
+by (Blast_tac 1); 
+qed "project_act_extend_act";
+
+
+(*** OK and "lift" ***)
+
+Goal "act <= {(x,x'). fst x = fst x'} ==> act : UNION (preserves fst) Acts";
+by (res_inst_tac [("a","mk_program(UNIV,{act},UNIV)")] UN_I 1);
+by (auto_tac (claset(),
+              simpset() addsimps [preserves_def,stable_def,constrains_def]));  
+qed "act_in_UNION_preserves_fst";
+
+Goal "[| ALL i:I. F i : preserves snd;  \
+\        ALL i:I. UNION (preserves fst) Acts <= AllowedActs (F i) |] \
+\     ==> OK I (%i. lift i (F i))";
+by (auto_tac (claset(), 
+      simpset() addsimps [OK_def, lift_def, rename_def, export Acts_extend,
+                export AllowedActs_extend, project_act_extend_act]));
+by (rename_tac "act" 1);
+by (subgoal_tac
+    "{(x, x'). EX s f u s' f' u'.   \
+\                ((s, f, u), s', f', u') : act &   \
+\                lift_map j x  = lift_map i (s, f, u) &   \
+\                lift_map j x' = lift_map i (s', f', u')}   \
+\    <= {(x,x'). fst x = fst x'}" 1);
+by (blast_tac (claset() addIs [act_in_UNION_preserves_fst]) 1);
+by (Clarify_tac 1); 
+by (REPEAT (dres_inst_tac [("x","j")] fun_cong 1) );
+by (dres_inst_tac [("x","i")] bspec 1); 
+by (assume_tac 1); 
+by (ftac preserves_imp_eq 1);
+by Auto_tac;  
+qed "UNION_OK_lift_I";
+
+Goal "[| ALL i:I. F i : preserves snd;  \
+\        ALL i:I. preserves fst <= Allowed (F i) |] \
+\     ==> OK I (%i. lift i (F i))";
+by (asm_full_simp_tac 
+    (simpset() addsimps [safety_prop_AllowedActs_iff_Allowed, 
+                         UNION_OK_lift_I]) 1); 
+qed "OK_lift_I";
+
+Goal "Allowed (lift i F) = lift i `` (Allowed F)";
+by (simp_tac (simpset() addsimps [lift_def, Allowed_rename]) 1); 
+qed "Allowed_lift"; 
+Addsimps [Allowed_lift];
+
+Goal "lift i `` preserves v = preserves (v o drop_map i)";
+by (simp_tac (simpset() addsimps [rename_image_preserves, lift_def, 
+                                  inv_lift_map_eq]) 1); 
+qed "lift_image_preserves";
diff -r 947ee8608b90 -r 1a77667b21ef src/HOL/UNITY/Mutex.thy
--- a/src/HOL/UNITY/Mutex.thy	Fri Sep 22 17:25:09 2000 +0200
+++ b/src/HOL/UNITY/Mutex.thy	Sat Sep 23 16:02:01 2000 +0200
@@ -55,7 +55,8 @@
 
   Mutex :: state program
     "Mutex == mk_program ({s. ~ u s & ~ v s & m s = #0 & n s = #0},
-		 	  {U0, U1, U2, U3, U4, V0, V1, V2, V3, V4})"
+		 	  {U0, U1, U2, U3, U4, V0, V1, V2, V3, V4},
+			  UNIV)"
 
 
   (** The correct invariants **)
diff -r 947ee8608b90 -r 1a77667b21ef src/HOL/UNITY/NSP_Bad.thy
--- a/src/HOL/UNITY/NSP_Bad.thy	Fri Sep 22 17:25:09 2000 +0200
+++ b/src/HOL/UNITY/NSP_Bad.thy	Sat Sep 23 16:02:01 2000 +0200
@@ -54,6 +54,6 @@
 constdefs
   Nprg :: state program
     (*Initial trace is empty*)
-    "Nprg == mk_program({[]}, {Fake, NS1, NS2, NS3})"
+    "Nprg == mk_program({[]}, {Fake, NS1, NS2, NS3}, UNIV)"
 
 end
diff -r 947ee8608b90 -r 1a77667b21ef src/HOL/UNITY/PPROD.ML
--- a/src/HOL/UNITY/PPROD.ML	Fri Sep 22 17:25:09 2000 +0200
+++ b/src/HOL/UNITY/PPROD.ML	Sat Sep 23 16:02:01 2000 +0200
@@ -121,12 +121,21 @@
   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 |]  \
-\    ==> (PLam I F) : X guarantees[v] Y";
+    "[| lift i (F i): X guarantees Y;  i : I;  \
+\       OK I (%i. lift i (F i)) |]  \
+\    ==> (PLam I F) : X guarantees Y"; 
 by (asm_simp_tac (simpset() addsimps [guarantees_JN_I]) 1);
 qed "guarantees_PLam_I";
 
+Goal "Allowed (PLam I F) = (INT i:I. lift i `` Allowed(F i))";
+by (simp_tac (simpset() addsimps [PLam_def]) 1); 
+qed "Allowed_PLam";
+Addsimps [Allowed_PLam];
+
+Goal "(PLam I F) : preserves v = (ALL i:I. F i : preserves (v o lift_map i))";
+by (simp_tac (simpset() addsimps [PLam_def, lift_def, rename_preserves]) 1); 
+qed "PLam_preserves";
+Addsimps [PLam_preserves];
 
 (**UNUSED
     (*The f0 premise ensures that the product is well-defined.*)
diff -r 947ee8608b90 -r 1a77667b21ef src/HOL/UNITY/Project.ML
--- a/src/HOL/UNITY/Project.ML	Fri Sep 22 17:25:09 2000 +0200
+++ b/src/HOL/UNITY/Project.ML	Sat Sep 23 16:02:01 2000 +0200
@@ -120,38 +120,36 @@
 qed "projecting_weaken_L";
 
 Goalw [extending_def]
-     "[| extending v C h F YA' YA;  extending v C h F YB' YB |] \
-\     ==> extending v C h F (YA' Int YB') (YA Int YB)";
+     "[| extending C h F YA' YA;  extending C h F YB' YB |] \
+\     ==> extending C h F (YA' Int YB') (YA Int YB)";
 by (Blast_tac 1);
 qed "extending_Int";
 
 Goalw [extending_def]
-     "[| extending v C h F YA' YA;  extending v C h F YB' YB |] \
-\     ==> extending v C h F (YA' Un YB') (YA Un YB)";
+     "[| extending C h F YA' YA;  extending C h F YB' YB |] \
+\     ==> extending C h F (YA' Un YB') (YA Un YB)";
 by (Blast_tac 1);
 qed "extending_Un";
 
 val [prem] = Goalw [extending_def]
-     "[| !!i. i:I ==> extending v C h F (Y' i) (Y i) |] \
-\     ==> extending v C h F (INT i:I. Y' i) (INT i:I. Y i)";
+     "[| !!i. i:I ==> extending C h F (Y' i) (Y i) |] \
+\     ==> extending C h F (INT i:I. Y' i) (INT i:I. Y i)";
 by (blast_tac (claset() addDs [prem RS spec RS mp]) 1);
 qed "extending_INT";
 
 val [prem] = Goalw [extending_def]
-     "[| !!i. i:I ==> extending v C h F (Y' i) (Y i) |] \
-\     ==> extending v C h F (UN i:I. Y' i) (UN i:I. Y i)";
+     "[| !!i. i:I ==> extending C h F (Y' i) (Y i) |] \
+\     ==> extending C h F (UN i:I. Y' i) (UN i:I. Y i)";
 by (blast_tac (claset() addDs [prem RS spec RS mp]) 1);
 qed "extending_UN";
 
 Goalw [extending_def]
-     "[| extending v C h F Y' Y;  Y'<=V';  V<=Y; \
-\        preserves w <= preserves v |] \
-\     ==> extending w C h F V' V";
+     "[| extending C h F Y' Y;  Y'<=V';  V<=Y |] ==> extending C h F V' V";
 by Auto_tac;
 qed "extending_weaken";
 
 Goalw [extending_def]
-     "[| extending v C h F Y' Y;  Y'<=V' |] ==> extending v C h F V' Y";
+     "[| extending C h F Y' Y;  Y'<=V' |] ==> extending C h F V' Y";
 by Auto_tac;
 qed "extending_weaken_L";
 
@@ -174,22 +172,22 @@
 by (blast_tac (claset() addIs [project_increasing_I]) 1);
 qed "projecting_increasing";
 
-Goal "extending v C h F UNIV Y";
+Goal "extending C h F UNIV Y";
 by (simp_tac (simpset() addsimps [extending_def]) 1);
 qed "extending_UNIV";
 
 Goalw [extending_def]
-     "extending v (%G. UNIV) h F (extend_set h A co extend_set h B) (A co B)";
+     "extending (%G. UNIV) h F (extend_set h A co extend_set h B) (A co B)";
 by (blast_tac (claset() addIs [project_constrains_D]) 1);
 qed "extending_constrains";
 
 Goalw [stable_def]
-     "extending v (%G. UNIV) h F (stable (extend_set h A)) (stable A)";
+     "extending (%G. UNIV) h F (stable (extend_set h A)) (stable A)";
 by (rtac extending_constrains 1);
 qed "extending_stable";
 
 Goalw [extending_def]
-     "extending v (%G. UNIV) h F (increasing (func o f)) (increasing func)";
+     "extending (%G. UNIV) h F (increasing (func o f)) (increasing func)";
 by (simp_tac (HOL_ss addsimps [Join_project_increasing]) 1);
 qed "extending_increasing";
 
@@ -354,25 +352,25 @@
 qed "projecting_Increasing";
 
 Goalw [extending_def]
-     "extending v (%G. reachable (extend h F Join G)) h F \
+     "extending (%G. reachable (extend h F Join G)) h F \
 \                 (extend_set h A Co extend_set h B) (A Co B)";
 by (blast_tac (claset() addIs [project_Constrains_D]) 1);
 qed "extending_Constrains";
 
 Goalw [extending_def]
-     "extending v (%G. reachable (extend h F Join G)) h F \
+     "extending (%G. reachable (extend h F Join G)) h F \
 \                 (Stable (extend_set h A)) (Stable A)";
 by (blast_tac (claset() addIs [project_Stable_D]) 1);
 qed "extending_Stable";
 
 Goalw [extending_def]
-     "extending v (%G. reachable (extend h F Join G)) h F \
+     "extending (%G. reachable (extend h F Join G)) h F \
 \                 (Always (extend_set h A)) (Always A)";
 by (blast_tac (claset() addIs [project_Always_D]) 1);
 qed "extending_Always";
 
 Goalw [extending_def]
-     "extending v (%G. reachable (extend h F Join G)) h F \
+     "extending (%G. reachable (extend h F Join G)) h F \
 \                 (Increasing (func o f)) (Increasing func)";
 by (blast_tac (claset() addIs [project_Increasing_D]) 1);
 qed "extending_Increasing";
@@ -596,31 +594,46 @@
 
 (*** Guarantees ***)
 
+Goal "project_act h (Restrict C act) <= project_act h act";
+by (auto_tac (claset(), simpset() addsimps [project_act_def]));  
+qed "project_act_Restrict_subset_project_act";
+					   
+							   
+Goal "[| extend h F ok G; subset_closed (AllowedActs F) |] \
+\     ==> F ok project h C G";
+by (auto_tac (claset(), simpset() addsimps [ok_def]));
+by (dtac subsetD 1);   
+by (Blast_tac 1); 
+by (force_tac (claset() addSIs [rev_image_eqI], simpset()) 1);
+by (cut_facts_tac [project_act_Restrict_subset_project_act] 1);
+by (auto_tac (claset(), simpset() addsimps [subset_closed_def]));  
+qed "subset_closed_ok_extend_imp_ok_project";
+
+
 (*Weak precondition and postcondition
   Not clear that it has a converse [or that we want one!]*)
 
 (*The raw version; 3rd premise could be weakened by adding the
   precondition extend h F Join G : X' *)
-val [xguary,project,extend] =
-Goal "[| F : X guarantees[v] Y;  \
+val [xguary,closed,project,extend] =
+Goal "[| F : X guarantees Y;  subset_closed (AllowedActs F);  \
 \        !!G. extend h F Join G : X' ==> F Join project h (C G) G : X;  \
-\        !!G. [| F Join project h (C G) G : Y; G : preserves (v o f) |] \
+\        !!G. [| F Join project h (C G) G : Y |] \
 \             ==> extend h F Join G : Y' |] \
-\     ==> extend h F : X' guarantees[v o f] Y'";
+\     ==> extend h F : X' guarantees Y'";
 by (rtac (xguary RS guaranteesD RS extend RS guaranteesI) 1);
-by (etac project_preserves_I 1);
+by (blast_tac (claset() addIs [closed, 
+          subset_closed_ok_extend_imp_ok_project]) 1); 
 by (etac project 1);
-by Auto_tac;
 qed "project_guarantees_raw";
 
-Goal "[| F : X guarantees[v] Y;  \
-\        projecting C h F X' X;  extending w C h F Y' Y; \
-\        preserves w <= preserves (v o f) |] \
-\     ==> extend h F : X' guarantees[w] Y'";
+Goal "[| F : X guarantees Y;  subset_closed (AllowedActs F); \
+\        projecting C h F X' X;  extending C h F Y' Y |] \
+\     ==> extend h F : X' guarantees Y'";
 by (rtac guaranteesI 1);
 by (auto_tac (claset(), 
-        simpset() addsimps [project_preserves_I, guaranteesD, projecting_def,
-			    extending_def]));
+        simpset() addsimps [guaranteesD, projecting_def, 
+                    extending_def, subset_closed_ok_extend_imp_ok_project]));
 qed "project_guarantees";
 
 
@@ -631,28 +644,31 @@
 
 (** Some could be deleted: the required versions are easy to prove **)
 
-Goal "F : UNIV guarantees[v] increasing func \
-\     ==> extend h F : X' guarantees[v o f] increasing (func o f)";
+Goal "[| F : UNIV guarantees increasing func;  \
+\        subset_closed (AllowedActs F) |] \
+\     ==> extend h F : X' guarantees increasing (func o f)";
 by (etac project_guarantees 1);
-by (rtac extending_increasing 2);
-by (rtac projecting_UNIV 1);
+by (rtac extending_increasing 3);
+by (rtac projecting_UNIV 2);
 by Auto_tac;
 qed "extend_guar_increasing";
 
-Goal "F : UNIV guarantees[v] Increasing func \
-\     ==> extend h F : X' guarantees[v o f] Increasing (func o f)";
+Goal "[| F : UNIV guarantees Increasing func;  \
+\        subset_closed (AllowedActs F) |] \
+\     ==> extend h F : X' guarantees Increasing (func o f)";
 by (etac project_guarantees 1);
-by (rtac extending_Increasing 2);
-by (rtac projecting_UNIV 1);
+by (rtac extending_Increasing 3);
+by (rtac projecting_UNIV 2);
 by Auto_tac;
 qed "extend_guar_Increasing";
 
-Goal "F : Always A guarantees[v] Always B \
-\     ==> extend h F : Always(extend_set h A) guarantees[v o f] \
-\                      Always(extend_set h B)";
+Goal "[| F : Always A guarantees Always B;  \
+\        subset_closed (AllowedActs F) |] \
+\     ==> extend h F                   \
+\           : Always(extend_set h A) guarantees Always(extend_set h B)";
 by (etac project_guarantees 1);
-by (rtac extending_Always 2);
-by (rtac projecting_Always 1);
+by (rtac extending_Always 3);
+by (rtac projecting_Always 2);
 by Auto_tac;
 qed "extend_guar_Always";
 
@@ -676,8 +692,8 @@
 	      simpset()));
 qed "project_leadsTo_D";
 
-Goal "[| F Join project h (reachable (extend h F Join G)) G : A LeadsTo B; \
-\         G : preserves f |]  \
+Goal "[| F Join project h (reachable (extend h F Join G)) G : A LeadsTo B;    \
+\        G : preserves f |]  \
 \      ==> extend h F Join G : (extend_set h A) LeadsTo (extend_set h B)";
 by (rtac (refl RS Join_project_LeadsTo) 1);
 by (auto_tac (claset() addDs [preserves_project_transient_empty], 
@@ -685,35 +701,17 @@
 qed "project_LeadsTo_D";
 
 Goalw [extending_def]
-     "extending f (%G. UNIV) h F \
+     "(ALL G. extend h F ok G --> G : preserves f) \
+\     ==> extending (%G. UNIV) h F \
 \                 (extend_set h A leadsTo extend_set h B) (A leadsTo B)";
 by (blast_tac (claset() addIs [project_leadsTo_D]) 1);
 qed "extending_leadsTo";
 
 Goalw [extending_def]
-     "extending f (%G. reachable (extend h F Join G)) h F \
+     "(ALL G. extend h F ok G --> G : preserves f) \
+\     ==> extending (%G. reachable (extend h F Join G)) h F \
 \                 (extend_set h A LeadsTo extend_set h B) (A LeadsTo B)";
 by (blast_tac (claset() addIs [project_LeadsTo_D]) 1);
 qed "extending_LeadsTo";
 
-(*STRONG precondition and postcondition*)
-Goal "F : (A co A') guarantees[v] (B leadsTo B')  \
-\ ==> extend h F : (extend_set h A co extend_set h A') \
-\                  guarantees[f] (extend_set h B leadsTo extend_set h B')";
-by (etac project_guarantees 1);
-by (rtac subset_preserves_o 3);
-by (rtac extending_leadsTo 2);
-by (rtac projecting_constrains 1);
-qed "extend_co_guar_leadsTo";
-
-(*WEAK precondition and postcondition*)
-Goal "F : (A Co A') guarantees[v] (B LeadsTo B')  \
-\ ==> extend h F : (extend_set h A Co extend_set h A') \
-\                  guarantees[f] (extend_set h B LeadsTo extend_set h B')";
-by (etac project_guarantees 1);
-by (rtac subset_preserves_o 3);
-by (rtac extending_LeadsTo 2);
-by (rtac projecting_Constrains 1);
-qed "extend_Co_guar_LeadsTo";
-
 Close_locale "Extend";
diff -r 947ee8608b90 -r 1a77667b21ef src/HOL/UNITY/Project.thy
--- a/src/HOL/UNITY/Project.thy	Fri Sep 22 17:25:09 2000 +0200
+++ b/src/HOL/UNITY/Project.thy	Sat Sep 23 16:02:01 2000 +0200
@@ -13,13 +13,16 @@
 constdefs
   projecting :: "['c program => 'c set, 'a*'b => 'c, 
 		  'a program, 'c program set, 'a program set] => bool"
-  "projecting C h F X' X ==
-     ALL G. extend h F Join G : X' --> F Join project h (C G) G : X"
+    "projecting C h F X' X ==
+       ALL G. extend h F Join G : X' --> F Join project h (C G) G : X"
 
-  extending :: "['c=>'d, 'c program => 'c set, 'a*'b => 'c, 'a program, 
+  extending :: "['c program => 'c set, 'a*'b => 'c, 'a program, 
 		 'c program set, 'a program set] => bool"
-  "extending v C h F Y' Y ==
-     ALL G. G : preserves v --> F Join project h (C G) G : Y
-            --> extend h F Join G : Y'"
+    "extending C h F Y' Y ==
+       ALL G. extend h F  ok G --> F Join project h (C G) G : Y
+	      --> extend h F Join G : Y'"
+
+  subset_closed :: "'a set set => bool"
+    "subset_closed U == ALL A: U. Pow A <= U"  
 
 end
diff -r 947ee8608b90 -r 1a77667b21ef src/HOL/UNITY/Reach.thy
--- a/src/HOL/UNITY/Reach.thy	Fri Sep 22 17:25:09 2000 +0200
+++ b/src/HOL/UNITY/Reach.thy	Sat Sep 23 16:02:01 2000 +0200
@@ -24,7 +24,7 @@
     "asgt u v == {(s,s'). s' = s(v:= s u | s v)}"
 
   Rprg :: state program
-    "Rprg == mk_program ({%v. v=init}, UN (u,v): edges. {asgt u v})"
+    "Rprg == mk_program ({%v. v=init}, UN (u,v): edges. {asgt u v}, UNIV)"
 
   reach_invariant :: state set
     "reach_invariant == {s. (ALL v. s v --> (init, v) : edges^*) & s init}"
diff -r 947ee8608b90 -r 1a77667b21ef src/HOL/UNITY/Rename.ML
--- a/src/HOL/UNITY/Rename.ML	Fri Sep 22 17:25:09 2000 +0200
+++ b/src/HOL/UNITY/Rename.ML	Sat Sep 23 16:02:01 2000 +0200
@@ -13,6 +13,7 @@
 by Auto_tac;
 qed "good_map_bij";
 Addsimps [good_map_bij];
+AddIs    [good_map_bij];
 
 fun bij_export th = good_map_bij RS export th |> simplify (simpset());
 
@@ -57,12 +58,35 @@
 (** for "rename" (programs) **)
 
 Goal "bij h \
-\     ==> extend_act (%(x,u::'c). inv h x) = project_act (%(x,u::'c). h x)";
+\     ==> extend_act (%(x,u::'c). h x) = project_act (%(x,u::'c). inv h x)";
 by (rtac ext 1);
 by (auto_tac (claset() addSIs [image_eqI], 
 	      simpset() addsimps [extend_act_def, project_act_def, bij_def,
 				  surj_f_inv_f]));
-qed "extend_act_inv";
+qed "bij_extend_act_eq_project_act";
+
+Goal "bij h ==> bij (extend_act (%(x,u::'c). h x))";
+by (rtac bijI 1);
+by (rtac (export inj_extend_act) 1);
+by (auto_tac (claset(), simpset() addsimps [bij_extend_act_eq_project_act]));  
+by (blast_tac (claset() addIs [bij_imp_bij_inv, surjI, 
+                               export extend_act_inverse]) 1); 
+qed "bij_extend_act";
+
+Goal "bij h ==> bij (project_act (%(x,u::'c). h x))";
+by (ftac (bij_imp_bij_inv RS bij_extend_act) 1);
+by (asm_full_simp_tac (simpset() addsimps [bij_extend_act_eq_project_act,
+                                    bij_imp_bij_inv, inv_inv_eq]) 1);  
+qed "bij_project_act";
+
+Goal "bij h ==> inv (project_act (%(x,u::'c). inv h x)) = \
+\               project_act (%(x,u::'c). h x)";
+by (asm_simp_tac
+    (simpset() addsimps [bij_extend_act_eq_project_act RS sym]) 1); 
+by (rtac surj_imp_inv_eq 1);
+by (blast_tac (claset() addIs [bij_extend_act, bij_is_surj]) 1);  
+by (asm_simp_tac (simpset() addsimps [export extend_act_inverse]) 1); 
+qed "bij_inv_project_act_eq";
 
 Goal "bij h  \
 \     ==> extend (%(x,u::'c). inv h x) = project (%(x,u::'c). h x) UNIV";
@@ -71,8 +95,14 @@
 by (rtac program_equalityI 1);
 by (asm_simp_tac
     (simpset() addsimps [export project_act_Id, export Acts_extend,
-			 insert_Id_image_Acts, extend_act_inv]) 2);
+			 insert_Id_image_Acts, bij_extend_act_eq_project_act, 
+                         inv_inv_eq]) 2);
 by (asm_simp_tac (simpset() addsimps [extend_set_inv]) 1);
+by (asm_simp_tac
+    (simpset() addsimps [export AllowedActs_extend,
+			 export AllowedActs_project,
+			 bij_project_act, bij_vimage_eq_inv_image,
+                         bij_inv_project_act_eq]) 1);
 qed "extend_inv";
 
 Goal "bij h ==> rename (inv h) (rename h F) = F";
@@ -94,24 +124,45 @@
 
 (** (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);
-qed "inj_rename";
+Goal "bij h ==> bij (extend (%(x,u::'c). h x))";
+by (rtac bijI 1);
+by (blast_tac (claset() addIs [export inj_extend]) 1);
+by (res_inst_tac [("f","extend (%(x,u). inv h x)")] surjI 1); 
+by (stac ((inst "f" "h" inv_inv_eq) RS sym) 1
+    THEN stac extend_inv 2 THEN stac (export extend_inverse) 3);
+by (auto_tac (claset(), simpset() addsimps [bij_imp_bij_inv, inv_inv_eq]));
+qed "bij_extend";
+
+Goal "bij h ==> bij (project (%(x,u::'c). h x) UNIV)";
+by (stac (extend_inv RS sym) 1); 
+by (auto_tac (claset(), simpset() addsimps [bij_imp_bij_inv, bij_extend]));
+qed "bij_project";
 
-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  \
+\     ==> inv (project (%(x,u::'c). h x) UNIV) = extend (%(x,u::'c). h x)";
+by (rtac inj_imp_inv_eq 1); 
+by (etac (bij_project RS bij_is_inj) 1); 
+by (asm_simp_tac (simpset() addsimps [export extend_inverse]) 1); 
+qed "inv_project_eq";
+
+Goal "bij h ==> Allowed (rename h F) = rename h `` Allowed F";
+by (asm_simp_tac (simpset() addsimps [rename_def, export Allowed_extend]) 1);
+by (stac bij_vimage_eq_inv_image 1); 
+by (rtac bij_project 1); 
+by (Blast_tac 1); 
+by (asm_simp_tac (simpset() addsimps [inv_project_eq]) 1);
+qed "Allowed_rename"; 
+Addsimps [Allowed_rename];
 
 Goal "bij h ==> bij (rename h)";
-by (blast_tac (claset() addIs [bijI, inj_rename, surj_rename]) 1);
+by (asm_simp_tac (simpset() addsimps [rename_def, bij_extend]) 1); 
 qed "bij_rename";
+bind_thm ("surj_rename", bij_rename RS bij_is_surj);
 
 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 (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, 
                                   rename_def, extend_def]));
@@ -119,7 +170,7 @@
 
 Goalw [surj_def] "surj (rename h) ==> surj h";
 by Auto_tac;
-by (dres_inst_tac [("x", "mk_program ({y}, {})")] spec 1);
+by (dres_inst_tac [("x", "mk_program ({y}, {}, {})")] spec 1);
 by (auto_tac (claset(), 
 	      simpset() addsimps [program_equality_iff, 
                                   rename_def, extend_def]));
@@ -135,6 +186,7 @@
 qed "bij_rename_iff";
 AddIffs [bij_rename_iff];
 
+
 (*** the lattice operations ***)
 
 Goalw [rename_def] "bij h ==> rename h SKIP = SKIP";
@@ -236,16 +288,16 @@
 qed "rename_LeadsTo";
 
 Goalw [rename_def]
-     "bij h ==> (rename h F : (rename h `` X) guarantees[v o inv h] \
+     "bij h ==> (rename h F : (rename h `` X) guarantees \
 \                             (rename h `` Y)) = \
-\               (F : X guarantees[v] Y)";
+\               (F : X guarantees Y)";
 by (stac (good_map_bij RS export extend_guarantees_eq RS sym) 1);
 by (assume_tac 1);
 by (asm_simp_tac (simpset() addsimps [fst_o_inv_eq_inv, o_def]) 1);
 qed "rename_rename_guarantees_eq";
 
-Goal "bij h ==> (rename h F : X guarantees[v] Y) = \
-\               (F : (rename (inv h) `` X) guarantees[v o h] \
+Goal "bij h ==> (rename h F : X guarantees Y) = \
+\               (F : (rename (inv h) `` X) guarantees \
 \                    (rename (inv h) `` Y))";
 by (stac (rename_rename_guarantees_eq RS sym) 1);
 by (assume_tac 1);
@@ -260,6 +312,16 @@
 				      bij_is_surj RS surj_f_inv_f]) 1);
 qed "rename_preserves";
 
+Goal "bij h ==> (rename h F ok rename h G) = (F ok G)";
+by (asm_simp_tac (simpset() addsimps [export ok_extend_iff, rename_def]) 1); 
+qed "ok_rename_iff";
+Addsimps [ok_rename_iff];
+
+Goal "bij h ==> OK I (%i. rename h (F i)) = (OK I F)";
+by (asm_simp_tac (simpset() addsimps [export OK_extend_iff, rename_def]) 1); 
+qed "OK_rename_iff";
+Addsimps [OK_rename_iff];
+
 
 (*** "image" versions of the rules, for lifting "guarantees" properties ***)
 
@@ -294,6 +356,11 @@
 by (rename_image_tac [rename_Constrains]);
 qed "rename_image_Constrains";
 
+Goal "bij h ==> rename h `` preserves v = preserves (v o inv h)";
+by (asm_simp_tac (simpset() addsimps [o_def, rename_image_stable,
+                    preserves_def, bij_image_INT, bij_image_Collect_eq]) 1); 
+qed "rename_image_preserves";
+
 Goal "bij h ==> rename h `` Stable A = Stable (h `` A)";
 by (rename_image_tac [rename_Stable]);
 qed "rename_image_Stable";
diff -r 947ee8608b90 -r 1a77667b21ef src/HOL/UNITY/TimerArray.thy
--- a/src/HOL/UNITY/TimerArray.thy	Fri Sep 22 17:25:09 2000 +0200
+++ b/src/HOL/UNITY/TimerArray.thy	Sat Sep 23 16:02:01 2000 +0200
@@ -18,6 +18,6 @@
     "decr == UN n uu. {((Suc n, uu), (n,uu))}"
   
   Timer :: 'a state program
-    "Timer == mk_program (UNIV, {decr})"
+    "Timer == mk_program (UNIV, {decr}, UNIV)"
 
 end
diff -r 947ee8608b90 -r 1a77667b21ef src/HOL/UNITY/UNITY.ML
--- a/src/HOL/UNITY/UNITY.ML	Fri Sep 22 17:25:09 2000 +0200
+++ b/src/HOL/UNITY/UNITY.ML	Sat Sep 23 16:02:01 2000 +0200
@@ -8,16 +8,14 @@
 From Misra, "A Logic for Concurrent Programming", 1994
 *)
 
-set timing;
-
 (*Perhaps equalities.ML shouldn't add this in the first place!*)
 Delsimps [image_Collect];
 
-
 (*** The abstract type of programs ***)
 
 val rep_ss = simpset() addsimps 
-                [Init_def, Acts_def, mk_program_def, Program_def, Rep_Program, 
+                [Init_def, Acts_def, AllowedActs_def, 
+		 mk_program_def, Program_def, Rep_Program, 
 		 Rep_Program_inverse, Abs_Program_inverse];
 
 
@@ -32,41 +30,59 @@
 qed "insert_Id_Acts";
 AddIffs [insert_Id_Acts];
 
+Goal "Id : AllowedActs F";
+by (cut_inst_tac [("x", "F")] Rep_Program 1);
+by (auto_tac (claset(), rep_ss));
+qed "Id_in_AllowedActs";
+AddIffs [Id_in_AllowedActs];
+
+Goal "insert Id (AllowedActs F) = AllowedActs F";
+by (simp_tac (simpset() addsimps [insert_absorb, Id_in_AllowedActs]) 1);
+qed "insert_Id_AllowedActs";
+AddIffs [insert_Id_AllowedActs];
+
 (** Inspectors for type "program" **)
 
-Goal "Init (mk_program (init,acts)) = init";
+Goal "Init (mk_program (init,acts,allowed)) = init";
 by (auto_tac (claset(), rep_ss));
 qed "Init_eq";
 
-Goal "Acts (mk_program (init,acts)) = insert Id acts";
+Goal "Acts (mk_program (init,acts,allowed)) = insert Id acts";
 by (auto_tac (claset(), rep_ss));
 qed "Acts_eq";
 
-Addsimps [Acts_eq, Init_eq];
+Goal "AllowedActs (mk_program (init,acts,allowed)) = insert Id allowed";
+by (auto_tac (claset(), rep_ss));
+qed "AllowedActs_eq";
 
+Addsimps [Init_eq, Acts_eq, AllowedActs_eq];
 
 (** Equality for UNITY programs **)
 
-Goal "mk_program (Init F, Acts F) = F";
+Goal "mk_program (Init F, Acts F, AllowedActs F) = F";
 by (cut_inst_tac [("x", "F")] Rep_Program 1);
 by (auto_tac (claset(), rep_ss));
 by (REPEAT (dres_inst_tac [("f", "Abs_Program")] arg_cong 1));
 by (asm_full_simp_tac (rep_ss addsimps [insert_absorb]) 1);
 qed "surjective_mk_program";
 
-Goal "[| Init F = Init G; Acts F = Acts G |] ==> F = G";
+Goal "[| Init F = Init G; Acts F = Acts G; AllowedActs F = AllowedActs G |] \
+\     ==> F = G";
 by (res_inst_tac [("t", "F")] (surjective_mk_program RS subst) 1);
 by (res_inst_tac [("t", "G")] (surjective_mk_program RS subst) 1);
 by (Asm_simp_tac 1);
 qed "program_equalityI";
 
 val [major,minor] =
-Goal "[| F = G; [| Init F = Init G; Acts F = Acts G |] ==> P |] ==> P";
+Goal "[| F = G; \
+\        [| Init F = Init G; Acts F = Acts G; AllowedActs F = AllowedActs G |]\
+\        ==> P |] ==> P";
 by (rtac minor 1);
 by (auto_tac (claset(), simpset() addsimps [major]));
 qed "program_equalityE";
 
-Goal "(F=G) = (Init F = Init G & Acts F = Acts G)";
+Goal "(F=G) =  \
+\     (Init F = Init G & Acts F = Acts G &AllowedActs F = AllowedActs G)";
 by (blast_tac (claset() addIs [program_equalityI, program_equalityE]) 1);
 qed "program_equality_iff";
 
@@ -77,13 +93,22 @@
      They avoid expanding the full program, which is a large expression
 ***)
 
-Goal "F == mk_program (init,acts) ==> Init F = init";
+Goal "F == mk_program (init,acts,allowed) ==> Init F = init";
 by Auto_tac;
 qed "def_prg_Init";
 
+Goal "F == mk_program (init,acts,allowed) ==> Acts F = insert Id acts";
+by Auto_tac;
+qed "def_prg_Acts";
+
+Goal "F == mk_program (init,acts,allowed) \
+\     ==> AllowedActs F = insert Id allowed";
+by Auto_tac;
+qed "def_prg_AllowedActs";
+
 (*The program is not expanded, but its Init and Acts are*)
 val [rew] = goal thy
-    "[| F == mk_program (init,acts) |] \
+    "[| F == mk_program (init,acts,allowed) |] \
 \    ==> Init F = init & Acts F = insert Id acts";
 by (rewtac rew);
 by Auto_tac;
diff -r 947ee8608b90 -r 1a77667b21ef src/HOL/UNITY/UNITY.thy
--- a/src/HOL/UNITY/UNITY.thy	Fri Sep 22 17:25:09 2000 +0200
+++ b/src/HOL/UNITY/UNITY.thy	Sat Sep 23 16:02:01 2000 +0200
@@ -11,21 +11,30 @@
 UNITY = Main + 
 
 typedef (Program)
-  'a program = "{(init:: 'a set, acts :: ('a * 'a)set set). Id:acts}"
+  'a program = "{(init:: 'a set, acts :: ('a * 'a)set set,
+		  allowed :: ('a * 'a)set set). Id:acts & Id: allowed}"
 
 consts
   constrains :: "['a set, 'a set] => 'a program set"  (infixl "co"     60)
   op_unless  :: "['a set, 'a set] => 'a program set"  (infixl "unless" 60)
 
 constdefs
-    mk_program :: "('a set * ('a * 'a)set set) => 'a program"
-    "mk_program == %(init, acts). Abs_Program (init, insert Id acts)"
+    mk_program :: "('a set * ('a * 'a)set set * ('a * 'a)set set)
+		   => 'a program"
+    "mk_program == %(init, acts, allowed).
+                      Abs_Program (init, insert Id acts, insert Id allowed)"
 
   Init :: "'a program => 'a set"
-    "Init F == (%(init, acts). init) (Rep_Program F)"
+    "Init F == (%(init, acts, allowed). init) (Rep_Program F)"
 
   Acts :: "'a program => ('a * 'a)set set"
-    "Acts F == (%(init, acts). acts) (Rep_Program F)"
+    "Acts F == (%(init, acts, allowed). acts) (Rep_Program F)"
+
+  AllowedActs :: "'a program => ('a * 'a)set set"
+    "AllowedActs F == (%(init, acts, allowed). allowed) (Rep_Program F)"
+
+  Allowed :: "'a program => 'a program set"
+    "Allowed F == {G. Acts G <= AllowedActs F}"
 
   stable     :: "'a set => 'a program set"
     "stable A == A co A"
diff -r 947ee8608b90 -r 1a77667b21ef src/HOL/UNITY/Union.ML
--- a/src/HOL/UNITY/Union.ML	Fri Sep 22 17:25:09 2000 +0200
+++ b/src/HOL/UNITY/Union.ML	Sat Sep 23 16:02:01 2000 +0200
@@ -19,7 +19,11 @@
 by (simp_tac (simpset() addsimps [SKIP_def]) 1);
 qed "Acts_SKIP";
 
-Addsimps [Init_SKIP, Acts_SKIP];
+Goal "AllowedActs SKIP = UNIV";
+by (auto_tac (claset(), simpset() addsimps [SKIP_def]));  
+qed "AllowedActs_SKIP";
+
+Addsimps [Init_SKIP, Acts_SKIP, AllowedActs_SKIP];
 
 Goal "reachable SKIP = UNIV";
 by (force_tac (claset() addEs [reachable.induct]
@@ -56,7 +60,11 @@
 by (auto_tac (claset(), simpset() addsimps [Join_def]));
 qed "Acts_Join";
 
-Addsimps [Init_Join, Acts_Join];
+Goal "AllowedActs (F Join G) = AllowedActs F Int AllowedActs G";
+by (auto_tac (claset(), simpset() addsimps [Join_def]));
+qed "AllowedActs_Join";
+
+Addsimps [Init_Join, Acts_Join, AllowedActs_Join];
 
 
 (** JN **)
@@ -68,7 +76,7 @@
 
 Goal "(JN i:insert a I. F i) = (F a) Join (JN i:I. F i)";
 by (rtac program_equalityI 1);
-by (ALLGOALS (simp_tac (simpset() addsimps [JOIN_def, Join_def])));
+by (auto_tac (claset(), simpset() addsimps [JOIN_def, Join_def]));  
 qed "JN_insert";
 Addsimps[JN_empty, JN_insert];
 
@@ -80,7 +88,11 @@
 by (auto_tac (claset(), simpset() addsimps [JOIN_def]));
 qed "Acts_JN";
 
-Addsimps [Init_JN, Acts_JN];
+Goal "AllowedActs (JN i:I. F i) = (INT i:I. AllowedActs (F i))";
+by (auto_tac (claset(), simpset() addsimps [JOIN_def]));
+qed "AllowedActs_JN";
+
+Addsimps [Init_JN, Acts_JN, AllowedActs_JN];
 
 val prems = Goalw [JOIN_def]
     "[| I=J;  !!i. i:J ==> F i = G i |] ==> \
@@ -97,12 +109,14 @@
 by (simp_tac (simpset() addsimps [Join_def, Un_commute, Int_commute]) 1);
 qed "Join_commute";
 
+
 Goal "A Join (B Join C) = B Join (A Join C)";
-by (simp_tac (simpset() addsimps Un_ac@Int_ac@[Join_def]) 1);
+by (simp_tac (simpset() addsimps Un_ac@Int_ac@[Join_def, insert_absorb]) 1);
 qed "Join_left_commute";
 
+
 Goal "(F Join G) Join H = F Join (G Join H)";
-by (simp_tac (simpset() addsimps Un_ac@[Join_def, Int_assoc]) 1);
+by (simp_tac (simpset() addsimps Un_ac@[Join_def, Int_assoc, insert_absorb]) 1);
 qed "Join_assoc";
  
 Goalw [Join_def, SKIP_def] "SKIP Join F = F";
@@ -316,3 +330,142 @@
 qed "stable_Join_ensures2";
 
 
+(*** the ok and OK relations ***)
+
+Goal "SKIP ok F";
+by (auto_tac (claset(), simpset() addsimps [ok_def]));
+qed "ok_SKIP1";  
+
+Goal "F ok SKIP";
+by (auto_tac (claset(), simpset() addsimps [ok_def]));
+qed "ok_SKIP2";
+
+AddIffs [ok_SKIP1, ok_SKIP2];  
+
+Goal "(F ok G & (F Join G) ok H) = (G ok H & F ok (G Join H))";
+by (auto_tac (claset(), simpset() addsimps [ok_def]));
+qed "ok_Join_commute";
+
+Goal "(F ok G) = (G ok F)";
+by (auto_tac (claset(), simpset() addsimps [ok_def]));
+qed "ok_commute";
+
+bind_thm ("ok_sym", ok_commute RS iffD1);
+
+Goal "OK {(0,F),(1,G),(2,H)} snd = (F ok G & (F Join G) ok H)";
+by (asm_full_simp_tac
+    (simpset() addsimps [Ball_def, conj_disj_distribR, ok_def, Join_def, 
+                   OK_def, insert_absorb, all_conj_distrib, eq_commute]) 1); 
+by (Blast_tac 1); 
+qed "ok_iff_OK";
+
+Goal "F ok (G Join H) = (F ok G & F ok H)";
+by (auto_tac (claset(), simpset() addsimps [ok_def]));
+qed "ok_Join_iff1";
+
+Goal "(G Join H) ok F = (G ok F & H ok F)";
+by (auto_tac (claset(), simpset() addsimps [ok_def]));
+qed "ok_Join_iff2";
+AddIffs [ok_Join_iff1, ok_Join_iff2];
+
+(*useful?  Not with the previous two around*)
+Goal "[| F ok G; (F Join G) ok H |] ==> F ok (G Join H)";
+by (auto_tac (claset(), simpset() addsimps [ok_def]));
+qed "ok_Join_commute_I";
+
+Goal "F ok (JOIN I G) = (ALL i:I. F ok G i)";
+by (auto_tac (claset(), simpset() addsimps [ok_def]));
+qed "ok_JN_iff1";
+
+Goal "(JOIN I G) ok F =  (ALL i:I. G i ok F)";
+by (auto_tac (claset(), simpset() addsimps [ok_def]));
+qed "ok_JN_iff2";
+AddIffs [ok_JN_iff1, ok_JN_iff2];
+
+Goal "OK I F = (ALL i: I. ALL j: I-{i}. (F i) ok (F j))"; 
+by (auto_tac (claset(), simpset() addsimps [ok_def, OK_def]));  
+qed "OK_iff_ok";
+
+Goal "[| OK I F; i: I; j: I; i ~= j|] ==> (F i) ok (F j)"; 
+by (auto_tac (claset(), simpset() addsimps [OK_iff_ok]));  
+qed "OK_imp_ok";
+
+
+(*** Allowed ***)
+
+Goal "Allowed SKIP = UNIV";
+by (auto_tac (claset(), simpset() addsimps [Allowed_def]));  
+qed "Allowed_SKIP";
+
+Goal "Allowed (F Join G) = Allowed F Int Allowed G";
+by (auto_tac (claset(), simpset() addsimps [Allowed_def]));  
+qed "Allowed_Join";
+
+Goal "Allowed (JOIN I F) = (INT i:I. Allowed (F i))";
+by (auto_tac (claset(), simpset() addsimps [Allowed_def]));  
+qed "Allowed_JN";
+
+Addsimps [Allowed_SKIP, Allowed_Join, Allowed_JN];
+
+Goal "F ok G = (F : Allowed G & G : Allowed F)";
+by (simp_tac (simpset() addsimps [ok_def, Allowed_def]) 1);
+qed "ok_iff_Allowed";
+
+Goal "OK I F = (ALL i: I. ALL j: I-{i}. F i : Allowed(F j))"; 
+by (auto_tac (claset(), simpset() addsimps [OK_iff_ok, ok_iff_Allowed]));  
+qed "OK_iff_Allowed";
+
+(*** safety_prop, for reasoning about given instances of "ok" ***)
+
+Goal "safety_prop X ==> (Acts G <= insert Id (UNION X Acts)) = (G : X)";
+by (auto_tac (claset(), simpset() addsimps [safety_prop_def]));
+qed "safety_prop_Acts_iff";
+
+Goal "safety_prop X ==> (UNION X Acts <= AllowedActs F) = (X <= Allowed F)";
+by (auto_tac (claset(), 
+      simpset() addsimps [Allowed_def, safety_prop_Acts_iff RS sym]));  
+qed "safety_prop_AllowedActs_iff_Allowed";
+
+Goal "safety_prop X ==> Allowed (mk_program (init, acts, UNION X Acts)) = X";
+by (asm_simp_tac (simpset() addsimps [Allowed_def, safety_prop_Acts_iff]) 1); 
+qed "Allowed_eq";
+
+Goal "[| F == mk_program (init, acts, UNION X Acts) ; safety_prop X |] \
+\     ==> Allowed F = X";
+by (asm_simp_tac (simpset() addsimps [Allowed_eq]) 1); 
+qed "def_prg_Allowed";
+
+(*For safety_prop to hold, the property must be satisfiable!*)
+Goal "safety_prop (A co B) = (A <= B)";
+by (simp_tac (simpset() addsimps [safety_prop_def, constrains_def]) 1);
+by (Blast_tac 1); 
+qed "safety_prop_constrains";
+AddIffs [safety_prop_constrains];
+
+Goal "safety_prop (stable A)";
+by (simp_tac (simpset() addsimps [stable_def]) 1);
+qed "safety_prop_stable";
+AddIffs [safety_prop_stable];
+
+Goal "[| safety_prop X; safety_prop Y |] ==> safety_prop (X Int Y)";
+by (full_simp_tac (simpset() addsimps [safety_prop_def]) 1); 
+by (Blast_tac 1); 
+qed "safety_prop_Int";
+Addsimps [safety_prop_Int];
+
+Goal "(ALL i. safety_prop (X i)) ==> safety_prop (INT i. X i)";
+by (auto_tac (claset(), simpset() addsimps [safety_prop_def]));
+by (Blast_tac 1); 
+bind_thm ("safety_prop_INTER1", allI RS result());
+Addsimps [safety_prop_INTER1];
+							       
+Goal "(ALL i:I. safety_prop (X i)) ==> safety_prop (INT i:I. X i)";
+by (auto_tac (claset(), simpset() addsimps [safety_prop_def]));
+by (Blast_tac 1); 
+bind_thm ("safety_prop_INTER", ballI RS result());
+Addsimps [safety_prop_INTER];
+
+Goal "[| F == mk_program(init,acts,UNION X Acts); safety_prop X |] \
+\     ==> F ok G = (G : X & acts <= AllowedActs G)";
+by (auto_tac (claset(), simpset() addsimps [ok_def, safety_prop_Acts_iff]));  
+qed "def_UNION_ok_iff";
diff -r 947ee8608b90 -r 1a77667b21ef src/HOL/UNITY/Union.thy
--- a/src/HOL/UNITY/Union.thy	Fri Sep 22 17:25:09 2000 +0200
+++ b/src/HOL/UNITY/Union.thy	Sat Sep 23 16:02:01 2000 +0200
@@ -11,14 +11,30 @@
 Union = SubstAx + FP +
 
 constdefs
+
+  (*FIXME: conjoin Init F Int Init G ~= {} *) 
+  ok :: ['a program, 'a program] => bool      (infixl 65)
+    "F ok G == Acts F <= AllowedActs G &
+               Acts G <= AllowedActs F"
+
+  (*FIXME: conjoin (INT i:I. Init (F i)) ~= {} *) 
+  OK  :: ['a set, 'a => 'b program] => bool
+    "OK I F == (ALL i:I. ALL j: I-{i}. Acts (F i) <= AllowedActs (F j))"
+
   JOIN  :: ['a set, 'a => 'b program] => 'b program
-    "JOIN I F == mk_program (INT i:I. Init (F i), UN i:I. Acts (F i))"
+    "JOIN I F == mk_program (INT i:I. Init (F i), UN i:I. Acts (F i),
+			     INT i:I. AllowedActs (F i))"
 
   Join :: ['a program, 'a program] => 'a program      (infixl 65)
-    "F Join G == mk_program (Init F Int Init G, Acts F Un Acts G)"
+    "F Join G == mk_program (Init F Int Init G, Acts F Un Acts G,
+			     AllowedActs F Int AllowedActs G)"
 
   SKIP :: 'a program
-    "SKIP == mk_program (UNIV, {})"
+    "SKIP == mk_program (UNIV, {}, UNIV)"
+
+  (*Characterizes safety properties.  Used with specifying AllowedActs*)
+  safety_prop :: "'a program set => bool"
+    "safety_prop X == SKIP: X & (ALL G. Acts G <= UNION X Acts --> G : X)"
 
 syntax
   "@JOIN1"     :: [pttrns, 'b set] => 'b set         ("(3JN _./ _)" 10)
diff -r 947ee8608b90 -r 1a77667b21ef src/HOL/UNITY/WFair.ML
--- a/src/HOL/UNITY/WFair.ML	Fri Sep 22 17:25:09 2000 +0200
+++ b/src/HOL/UNITY/WFair.ML	Sat Sep 23 16:02:01 2000 +0200
@@ -237,7 +237,7 @@
 qed "leadsTo_weaken";
 
 
-(*Set difference: maybe combine with leadsTo_weaken_L??*)
+(*Set difference: maybe combine with leadsTo_weaken_L?*)
 Goal "[| F : (A-B) leadsTo C; F : B leadsTo C |]   ==> F : A leadsTo C";
 by (blast_tac (claset() addIs [leadsTo_Un, leadsTo_weaken]) 1);
 qed "leadsTo_Diff";
@@ -373,7 +373,7 @@
 val lemma = result();
 
 
-(** Meta or object quantifier ????? **)
+(** Meta or object quantifier ? **)
 Goal "[| wf r;     \
 \        ALL m. F : (A Int f-``{m}) leadsTo                     \
 \                   ((A Int f-``(r^-1 ^^ {m})) Un B) |] \