# HG changeset patch
# User paulson
# Date 940252704 -7200
# Node ID 43b03d412b82b1d886b71bd5f16d325606287073
# Parent  e5e019d60f71faccb544587086d4bbb2d7eb7402
working version with localTo[C] instead of localTo

diff -r e5e019d60f71 -r 43b03d412b82 src/HOL/UNITY/Alloc.ML
--- a/src/HOL/UNITY/Alloc.ML	Mon Oct 18 15:17:35 1999 +0200
+++ b/src/HOL/UNITY/Alloc.ML	Mon Oct 18 15:18:24 1999 +0200
@@ -388,35 +388,37 @@
 
 (*A LOT of work just to lift "Client_Progress" to the array*)
 Goal "lift_prog i Client \
-\  : Increasing (giv o sub i) Int ((%z. z i) localTo (lift_prog i Client)) \
+\  : Increasing (giv o sub i) Int ((%z. z i) localTo[UNIV] (lift_prog i Client)) \
 \    guarantees \
 \    (INT h. {s. h <=  (giv o sub i) s & \
 \                       h pfixGe (ask o sub i) s}  \
 \            LeadsTo {s. tokens h <= (tokens o rel o sub i) s})";
-br (Client_Progress RS drop_prog_guarantees) 1;
-br (lift_export extending_LeadsTo RS extending_weaken RS extending_INT) 2;
-br subset_refl 4;
+by (rtac (Client_Progress RS drop_prog_guarantees) 1);
+by (rtac (lift_export extending_LeadsTo RS extending_weaken RS extending_INT) 2);
+by (rtac subset_refl 4);
 by (simp_tac (simpset()addsimps [lift_export Collect_eq_extend_set RS sym]) 3);
 by (force_tac (claset(), simpset() addsimps [lift_prog_correct]) 2);
 by (rtac (lift_export projecting_Increasing RS projecting_weaken) 1);
 by (auto_tac (claset(), simpset() addsimps [o_def]));
 qed "Client_i_Progress";
 
+xxxxxxxxxxxxxxxx;
+
 Goalw [System_def]
      "i < Nclients \
 \ ==> System : (INT h. {s. h <=  (giv o sub i o client) s & \
 \                       h pfixGe (ask o sub i o client) s}  \
 \            LeadsTo {s. tokens h <= (tokens o rel o sub i o client) s})";
 by (rtac (guarantees_Join_I2 RS guaranteesD) 1);
-br (guarantees_PLam_I RS project_guarantees) 1;
-br Client_i_Progress  1;
+by (rtac (guarantees_PLam_I RS project_guarantees) 1);
+by (rtac Client_i_Progress  1);
 by (Force_tac 1);
-br (client_export extending_LeadsTo RS extending_weaken RS extending_INT) 2;
-br subset_refl 4;
+by (rtac (client_export extending_LeadsTo RS extending_weaken RS extending_INT) 2);
+by (rtac subset_refl 4);
 by (simp_tac (simpset()addsimps [client_export Collect_eq_extend_set RS sym]) 3);
-br projecting_Int 1;
-br (client_export projecting_Increasing) 1;
-br (client_export projecting_localTo) 1;
+by (rtac projecting_Int 1);
+by (rtac (client_export projecting_Increasing) 1);
+by (rtac (client_export projecting_localTo) 1);
 
 by (simp_tac (simpset()addsimps [lift_prog_correct]) 1);
 
diff -r e5e019d60f71 -r 43b03d412b82 src/HOL/UNITY/Client.ML
--- a/src/HOL/UNITY/Client.ML	Mon Oct 18 15:17:35 1999 +0200
+++ b/src/HOL/UNITY/Client.ML	Mon Oct 18 15:18:24 1999 +0200
@@ -73,7 +73,7 @@
 program_defs_ref := [];
 
 (*Safety property 2: clients return the right number of tokens*)
-Goal "Cli_prg : (Increasing giv Int (rel localTo Cli_prg))  \
+Goal "Cli_prg : (Increasing giv Int (rel localTo[UNIV] Cli_prg))  \
 \               guarantees Always {s. rel s <= giv s}";
 by (rtac guaranteesI 1);
 by (rtac AlwaysI 1);
@@ -101,7 +101,7 @@
 val Increasing_length = mono_length RS mono_Increasing_o;
 
 Goal "Cli_prg : \
-\      (Increasing giv Int (rel localTo Cli_prg) Int (ask localTo Cli_prg)) \
+\      (Increasing giv Int (rel localTo[UNIV] Cli_prg) Int (ask localTo[UNIV] Cli_prg)) \
 \      guarantees Always ({s. size (ask s) <= Suc (size (rel s))} Int \
 \                            {s. size (rel s) <= size (giv s)})";
 by (rtac guaranteesI 1);
@@ -122,7 +122,7 @@
 
 
 Goal "Cli_prg : \
-\      (Increasing giv Int (rel localTo Cli_prg) Int (ask localTo Cli_prg) \
+\      (Increasing giv Int (rel localTo[UNIV] Cli_prg) Int (ask localTo[UNIV] Cli_prg) \
 \                 Int Always giv_meets_ask) \
 \      guarantees ({s. k < size (giv s)} LeadsTo {s. k < size (rel s)})";
 by (rtac guaranteesI 1);
diff -r e5e019d60f71 -r 43b03d412b82 src/HOL/UNITY/Comp.ML
--- a/src/HOL/UNITY/Comp.ML	Mon Oct 18 15:17:35 1999 +0200
+++ b/src/HOL/UNITY/Comp.ML	Mon Oct 18 15:18:24 1999 +0200
@@ -62,7 +62,7 @@
 qed "component_antisym";
 
 Goalw [component_def]
-      "F <= H = (EX G. F Join G = H & Disjoint F G)";
+      "F <= H = (EX G. F Join G = H & Disjoint UNIV F G)";
 by (blast_tac (claset() addSIs [Diff_Disjoint, Join_Diff2]) 1);
 qed "component_eq";
 
@@ -77,8 +77,3 @@
 qed "component_constrains";
 
 bind_thm ("program_less_le", strict_component_def RS meta_eq_to_obj_eq);
-
-Goal "Diff F (Acts G) <= F";
-by (auto_tac (claset() addSIs [program_equalityI],
-	      simpset() addsimps [Diff_def, component_eq_subset]));
-qed "Diff_component";
diff -r e5e019d60f71 -r 43b03d412b82 src/HOL/UNITY/Extend.ML
--- a/src/HOL/UNITY/Extend.ML	Mon Oct 18 15:17:35 1999 +0200
+++ b/src/HOL/UNITY/Extend.ML	Mon Oct 18 15:18:24 1999 +0200
@@ -8,6 +8,17 @@
   function g (forgotten) maps the extended state to the "extending part"
 *)
 
+
+
+		Goal "(A Int B = {}) = (ALL x:A. ALL y:B. x ~= y)";
+		by  (Blast_tac 1);
+		qed "disjoint_iff_not_equal";
+
+		Goal "ff -`` (ff `` A) = {y. EX x:A. ff x = ff y}";
+		by (blast_tac (claset() addIs [sym]) 1);
+		qed "vimage_image_eq";
+
+
 (** These we prove OUTSIDE the locale. **)
 
 (*Possibly easier than reasoning about "inv h"*)
@@ -57,13 +68,41 @@
 (*FIXME: If locales worked properly we could put just "f" above*)
 by (full_simp_tac (simpset() addsimps [f_def, good_h RS conjunct2]) 1);
 qed "h_inject1";
-AddSDs [h_inject1];
+AddDs [h_inject1];
 
 Goal "h(f z, g z) = z";
 by (simp_tac (simpset() addsimps [f_def, g_def, surjective_pairing RS sym,
 				  surj_h RS surj_f_inv_f]) 1);
 qed "h_f_g_eq";
 
+
+(** A sequence of proof steps borrowed from Provers/split_paired_all.ML **)
+
+val cT = TFree ("'c", ["term"]);
+
+(* "PROP P x == PROP P (h (f x, g x))" *)
+val lemma1 = Thm.combination
+  (Thm.reflexive (cterm_of (sign_of thy) (Free ("P", cT --> propT))))
+  (Drule.unvarify (h_f_g_eq RS sym RS eq_reflection));
+
+val prems = Goalw [lemma1] "(!!u y. PROP P (h (u, y))) ==> PROP P x";
+by (resolve_tac prems 1);
+val lemma2 = result();
+
+val prems = Goal "(!!u y. PROP P (h (u, y))) ==> (!!z. PROP P z)";
+by (rtac lemma2 1);
+by (resolve_tac prems 1);
+val lemma3 = result();
+
+val prems = Goal "(!!z. PROP P z) ==> (!!u y. PROP P (h (u, y)))";
+(*not needed for proof, but prevents generalization over h, 'c, etc.*)
+by (cut_facts_tac [surj_h] 1);
+by (resolve_tac prems 1);
+val lemma4 = result();
+
+val split_extended_all = Thm.equal_intr lemma4 lemma3;
+
+
 (*** extend_set: basic properties ***)
 
 Goalw [extend_set_def] "A<=B ==> extend_set h A <= extend_set h B";
@@ -101,9 +140,8 @@
 qed "inj_extend_set";
 
 Goalw [extend_set_def] "extend_set h UNIV = UNIV";
-by Auto_tac;
-by (res_inst_tac [("y1", "x")] (surj_h RS surjD RS exE) 1);
-by Auto_tac;
+by (auto_tac (claset(), 
+	      simpset() addsimps [split_extended_all]));
 qed "extend_set_UNIV_eq";
 Addsimps [standard extend_set_UNIV_eq];
 
@@ -111,14 +149,14 @@
 
 (*project_set is simply image!*)
 Goalw [project_set_def] "project_set h C = f `` C";
-by (auto_tac (claset() addIs [f_h_eq RS sym, h_f_g_eq RS ssubst], 
-	      simpset()));
+by (auto_tac (claset() addIs [f_h_eq RS sym], 
+	      simpset() addsimps [split_extended_all]));
 qed "project_set_eq";
 
 (*Converse appears to fail*)
-Goalw [project_set_def] "z : C ==> f z : project_set h C";
-by (auto_tac (claset() addIs [h_f_g_eq RS ssubst], 
-	      simpset()));
+Goalw [project_set_def] "!!z. z : C ==> f z : project_set h C";
+by (auto_tac (claset(), 
+	      simpset() addsimps [split_extended_all]));
 qed "project_set_I";
 
 
@@ -160,31 +198,41 @@
 
 (*** extend_act ***)
 
-(*Actions could affect the g-part, so result Cannot be strengthened to
-   ((z, z') : extend_act h act) = ((f z, f z') : act)
-*)
 Goalw [extend_act_def]
      "((h(s,y), h(s',y)) : extend_act h act) = ((s, s') : act)";
 by Auto_tac;
 qed "mem_extend_act_iff";
 AddIffs [mem_extend_act_iff]; 
 
+(*Converse fails: (z,z') would include actions that changed the g-part*)
 Goalw [extend_act_def]
      "(z, z') : extend_act h act ==> (f z, f z') : act";
 by Auto_tac;
 qed "extend_act_D";
 
+Goalw [extend_act_def, project_act_def, project_set_def]
+     "project_act h (Restrict C (extend_act h act)) = \
+\     Restrict (project_set h C) act";
+by (Blast_tac 1);
+qed "project_act_extend_act_restrict";
+Addsimps [project_act_extend_act_restrict];
+
+Goalw [extend_act_def, project_act_def, project_set_def]
+     "(Restrict C (extend_act h act) = Restrict C (extend_act h act')) \
+\     = (Restrict (project_set h C) act = Restrict (project_set h C) act')";
+by Auto_tac;
+by (ALLGOALS (blast_tac (claset() addSEs [equalityE])));
+qed "Restrict_extend_act_eq_Restrict_project_act";
+
 (*Premise is still undesirably strong, since Domain act can include
   non-reachable states, but it seems necessary for this result.*)
-Goalw [extend_act_def, project_set_def, project_act_def]
- "Domain act <= project_set h C ==> project_act C h (extend_act h act) = act";
-by (Force_tac 1);
+Goal "Domain act <= project_set h C \
+\     ==> project_act h (Restrict C (extend_act h act)) = act";
+by (asm_simp_tac (simpset() addsimps [Restrict_triv]) 1);
 qed "extend_act_inverse";
-Addsimps [extend_act_inverse];
 
-(*By subset_refl, a corollary is project_act C h (extend_act h act) <= act*)
 Goalw [extend_act_def, project_act_def]
-     "act' <= extend_act h act ==> project_act C h act' <= act";
+     "act' <= extend_act h act ==> project_act h act' <= act";
 by (Force_tac 1);
 qed "subset_extend_act_D";
 
@@ -218,22 +266,20 @@
 qed "extend_act_Id";
 
 Goalw [project_act_def]
-     "[| (z, z') : act;  z: C |] \
-\     ==> (f z, f z') : project_act C h act";
-by (auto_tac (claset() addSIs [exI] addIs [h_f_g_eq RS ssubst], 
-	      simpset()));
+     "!!z z'. (z, z') : act ==> (f z, f z') : project_act h act";
+by (force_tac (claset(), 
+              simpset() addsimps [split_extended_all]) 1);
 qed "project_act_I";
 
 Goalw [project_set_def, project_act_def]
-    "UNIV <= project_set h C ==> project_act C h Id = Id";
+    "UNIV <= project_set h C ==> project_act h (Restrict C Id) = Id";
 by (Force_tac 1);
 qed "project_act_Id";
 
 Goalw [project_set_def, project_act_def]
-    "Domain (project_act C h act) = project_set h (Domain act Int C)";
-by Auto_tac;
-by (res_inst_tac [("y1", "ya")] (surj_h RS surjD RS exE) 1);
-by Auto_tac;
+  "Domain (project_act h (Restrict C act)) = project_set h (Domain act Int C)";
+by (force_tac (claset(), 
+              simpset() addsimps [split_extended_all]) 1);
 qed "Domain_project_act";
 
 Addsimps [extend_act_Id, project_act_Id];
@@ -267,7 +313,7 @@
 	      simpset() addsimps [extend_def, image_iff]));
 qed "Acts_extend";
 
-Goal "Acts (project C h F) = insert Id (project_act C h `` Acts F)";
+Goal "Acts (project C h F) = insert Id (project_act h `` Restrict C `` Acts F)";
 by (auto_tac (claset(), 
 	      simpset() addsimps [project_def, image_iff]));
 qed "Acts_project";
@@ -279,17 +325,18 @@
 by Auto_tac;
 qed "extend_SKIP";
 
-Goalw [project_set_def] "UNIV <= project_set h UNIV";
+Goalw [project_set_def] "project_set h UNIV = UNIV";
 by Auto_tac;
 qed "project_set_UNIV";
+Addsimps [project_set_UNIV];
 
 (*ALL act: Acts F. Domain act is MUCH TOO STRONG since Domain Id = UNIV!*)
 Goal "UNIV <= project_set h C \
 \     ==> project C h (extend h F) = F";
 by (simp_tac (simpset() addsimps [extend_def, project_def]) 1);
 by (rtac program_equalityI 1);
-by (asm_simp_tac (simpset() addsimps [image_image_eq_UN,
-                   subset_UNIV RS subset_trans RS extend_act_inverse]) 2);
+by (asm_simp_tac (simpset() addsimps [image_image_eq_UN, image_UN, 
+                   subset_UNIV RS subset_trans RS Restrict_triv]) 2);
 by (Simp_tac 1);
 qed "extend_inverse";
 Addsimps [extend_inverse];
@@ -354,43 +401,84 @@
 
 (*** Diff, needed for localTo ***)
 
-Goal "(Diff (extend h G) (extend_act h `` acts)) = extend h (Diff G acts)";
+Goal "Restrict (extend_set h C) (extend_act h act) = \
+\     extend_act h (Restrict C act)";
+by (auto_tac (claset(), 
+              simpset() addsimps [split_extended_all]));
+by (auto_tac (claset(), 
+              simpset() addsimps [extend_act_def]));
+qed "Restrict_extend_set";
+
+Goal "(Diff (extend_set h C) (extend h G) (extend_act h `` acts)) = \
+\     extend h (Diff C G acts)";
 by (auto_tac (claset() addSIs [program_equalityI],
-	      simpset() addsimps [Diff_def,
+	      simpset() addsimps [Diff_def, image_image_eq_UN,
+				  Restrict_extend_set,
 				  inj_extend_act RS image_set_diff]));
 qed "Diff_extend_eq";
 
-Goal "(Diff (extend h G) (extend_act h `` acts) \
+(*Opposite inclusion fails; this inclusion's more general than that of
+  Diff_extend_eq*)     
+Goal "Diff (project_set h C) G acts \
+\     <= project C h (Diff C (extend h G) (extend_act h `` acts))";
+by (simp_tac
+    (simpset() addsimps [component_eq_subset, Diff_def,image_UN,
+			 image_image, image_Diff_image_eq,
+			 Restrict_extend_act_eq_Restrict_project_act,
+			 vimage_image_eq]) 1);
+by  (blast_tac (claset() addSEs [equalityE])1);
+qed "Diff_project_set_component";
+
+Goal "(Diff (extend_set h C) (extend h G) (extend_act h `` acts) \
 \         : (extend_set h A) co (extend_set h B)) \
-\     = (Diff G acts : A co B)";
+\     = (Diff C G acts : A co B)";
 by (simp_tac (simpset() addsimps [Diff_extend_eq, extend_constrains]) 1);
 qed "Diff_extend_constrains";
 
-Goal "(Diff (extend h G) (extend_act h `` acts) : stable (extend_set h A)) \
-\     = (Diff G acts : stable A)";
+Goal "(Diff (extend_set h C) (extend h G) (extend_act h `` acts) \
+\       : stable (extend_set h A)) \
+\     = (Diff C G acts : stable A)";
 by (simp_tac (simpset() addsimps [Diff_extend_constrains, stable_def]) 1);
 qed "Diff_extend_stable";
 
-Goal "Diff (extend h G) (extend_act h `` acts) : A co B \
-\     ==> Diff G acts : (project_set h A) co (project_set h B)";
+(*UNUSED!!*)
+Goal "Diff (extend_set h C) (extend h G) (extend_act h `` acts) : A co B \
+\     ==> Diff C G acts : (project_set h A) co (project_set h B)";
 by (asm_full_simp_tac (simpset() addsimps [Diff_extend_eq, 
 					   extend_constrains_project_set]) 1);
 qed "Diff_extend_constrains_project_set";
 
-Goalw [localTo_def]
-     "(extend h F : (v o f) localTo extend h H) = (F : v localTo H)";
-by (simp_tac (simpset() addsimps []) 1);
+Goalw [LOCALTO_def]
+     "(extend h F : (v o f) localTo[extend_set h C] extend h H) = \
+\     (F : v localTo[C] H)";
+by (Simp_tac 1);
 (*A trick to strip both quantifiers*)
 by (res_inst_tac [("f", "All")] (ext RS arg_cong) 1);
 by (stac Collect_eq_extend_set 1);
 by (simp_tac (simpset() addsimps [Diff_extend_stable]) 1);
 qed "extend_localTo_extend_eq";
 
-Goal "Disjoint (extend h F) (extend h G) = Disjoint F G";
-by (simp_tac (simpset() addsimps [Disjoint_def,
-				  inj_extend_act RS image_Int RS sym]) 1);
-by (simp_tac (simpset() addsimps [image_subset_iff, extend_act_Id_iff]) 1);
-by (blast_tac (claset() addEs [equalityE]) 1);
+(*USED?? opposite inclusion fails*)
+Goal "Restrict C (extend_act h act) <= \
+\     extend_act h (Restrict (project_set h C) act)";
+by (auto_tac (claset(), 
+              simpset() addsimps [split_extended_all]));
+by (auto_tac (claset(), 
+              simpset() addsimps [extend_act_def, project_set_def]));
+qed "Restrict_extend_set_subset";
+
+
+Goal "(extend_act h `` Acts F) - {Id} = extend_act h `` (Acts F - {Id})";
+by (stac (extend_act_Id RS sym) 1);
+by (simp_tac (simpset() addsimps [inj_extend_act RS image_set_diff]) 1);
+qed "extend_act_image_Id_eq";
+
+Goal "Disjoint C (extend h F) (extend h G) = Disjoint (project_set h C) F G";
+by (simp_tac
+    (simpset() addsimps [Disjoint_def, disjoint_iff_not_equal,
+			 image_Diff_image_eq,
+			 Restrict_extend_act_eq_Restrict_project_act,
+			 extend_act_Id_iff, vimage_def]) 1);
 qed "Disjoint_extend_eq";
 Addsimps [Disjoint_extend_eq];
 
diff -r e5e019d60f71 -r 43b03d412b82 src/HOL/UNITY/Extend.thy
--- a/src/HOL/UNITY/Extend.thy	Mon Oct 18 15:17:35 1999 +0200
+++ b/src/HOL/UNITY/Extend.thy	Mon Oct 18 15:18:24 1999 +0200
@@ -25,18 +25,17 @@
   extend_act :: "['a*'b => 'c, ('a*'a) set] => ('c*'c) set"
     "extend_act h == %act. UN (s,s'): act. UN y. {(h(s,y), h(s',y))}"
 
-  (*Argument C allows weak safety laws to be projected*)
-  project_act :: "['c set, 'a*'b => 'c, ('c*'c) set] => ('a*'a) set"
-    "project_act C h act ==
-         {(x,x'). EX y y'. (h(x,y), h(x',y')) : act & (h(x,y) : C)}"
+  project_act :: "['a*'b => 'c, ('c*'c) set] => ('a*'a) set"
+    "project_act h act == {(x,x'). EX y y'. (h(x,y), h(x',y')) : act}"
 
   extend :: "['a*'b => 'c, 'a program] => 'c program"
     "extend h F == mk_program (extend_set h (Init F),
 			       extend_act h `` Acts F)"
 
+  (*Argument C allows weak safety laws to be projected*)
   project :: "['c set, 'a*'b => 'c, 'c program] => 'a program"
     "project C h F == mk_program (project_set h (Init F),
-		  	          project_act C h `` Acts F)"
+		  	          project_act h `` Restrict C `` Acts F)"
 
 locale Extend =
   fixes 
diff -r e5e019d60f71 -r 43b03d412b82 src/HOL/UNITY/Guar.ML
--- a/src/HOL/UNITY/Guar.ML	Mon Oct 18 15:17:35 1999 +0200
+++ b/src/HOL/UNITY/Guar.ML	Mon Oct 18 15:18:24 1999 +0200
@@ -65,7 +65,7 @@
 (*** guarantees ***)
 
 val prems = Goal
-     "(!!G. [| F Join G : X;  Disjoint F G |] ==> F Join G : Y) \
+     "(!!G. [| F Join G : X;  Disjoint UNIV F G |] ==> F Join G : Y) \
 \     ==> F : X guarantees Y";
 by (simp_tac (simpset() addsimps [guar_def, component_eq]) 1);
 by (blast_tac (claset() addIs prems) 1);
@@ -84,7 +84,7 @@
 
 (*This equation is more intuitive than the official definition*)
 Goal "(F : X guarantees Y) = \
-\     (ALL G. F Join G : X & Disjoint F G --> F Join G : Y)";
+\     (ALL G. F Join G : X & Disjoint UNIV F G --> F Join G : Y)";
 by (simp_tac (simpset() addsimps [guar_def, component_eq]) 1);
 by (Blast_tac 1);
 qed "guarantees_eq";
diff -r e5e019d60f71 -r 43b03d412b82 src/HOL/UNITY/LessThan.ML
--- a/src/HOL/UNITY/LessThan.ML	Mon Oct 18 15:17:35 1999 +0200
+++ b/src/HOL/UNITY/LessThan.ML	Mon Oct 18 15:18:24 1999 +0200
@@ -7,6 +7,61 @@
 *)
 
 
+(*** Restrict [MOVE TO RELATION.THY??] ***)
+
+Goalw [Restrict_def] "((x,y): Restrict A r) = ((x,y): r & x: A)";
+by (Blast_tac 1);
+qed "Restrict_iff";
+AddIffs [Restrict_iff];
+
+Goal "Restrict UNIV = id";
+by (rtac ext 1);
+by (auto_tac (claset(), simpset() addsimps [Restrict_def]));
+qed "Restrict_UNIV";
+Addsimps [Restrict_UNIV];
+
+Goal "Restrict {} r = {}";
+by (auto_tac (claset(), simpset() addsimps [Restrict_def]));
+qed "Restrict_empty";
+Addsimps [Restrict_empty];
+
+Goalw [Restrict_def] "Restrict A (Restrict B r) = Restrict (A Int B) r";
+by (Blast_tac 1);
+qed "Restrict_Int";
+Addsimps [Restrict_Int];
+
+Goalw [Restrict_def] "Domain r <= A ==> Restrict A r = r";
+by Auto_tac;
+qed "Restrict_triv";
+
+Goalw [Restrict_def] "Restrict A r <= r";
+by Auto_tac;
+qed "Restrict_subset";
+
+Goalw [Restrict_def]
+     "[| A <= B;  Restrict B r = Restrict B s |] \
+\     ==> Restrict A r = Restrict A s";
+by (blast_tac (claset() addSEs [equalityE]) 1);
+qed "Restrict_eq_mono";
+
+Goalw [Restrict_def, image_def]
+     "[| s : RR;  Restrict A r = Restrict A s |] \
+\     ==> Restrict A r : Restrict A `` RR";
+by Auto_tac;
+qed "Restrict_imageI";
+
+Goal "(Restrict A `` (Restrict A `` r - s)) = (Restrict A `` r - s)";
+by Auto_tac;
+by (rewrite_goals_tac [image_def, Restrict_def]);
+by (Blast_tac 1);
+qed "Restrict_image_Diff";
+
+(*Nothing to do with Restrict, but to specialized for Fun.ML?*)
+Goal "f``(g``A - B) = (UN x: (A - g-`` B). {f(g(x))})";
+by (Blast_tac 1);
+qed "image_Diff_image_eq";
+
+
 (*** lessThan ***)
 
 Goalw [lessThan_def] "(i: lessThan k) = (i<k)";
diff -r e5e019d60f71 -r 43b03d412b82 src/HOL/UNITY/LessThan.thy
--- a/src/HOL/UNITY/LessThan.thy	Mon Oct 18 15:17:35 1999 +0200
+++ b/src/HOL/UNITY/LessThan.thy	Mon Oct 18 15:18:24 1999 +0200
@@ -12,6 +12,10 @@
 
 constdefs
 
+  (*MOVE TO RELATION.THY??*)
+  Restrict :: "[ 'a set, ('a*'b) set] => ('a*'b) set"
+    "Restrict A r == r Int (A Times UNIV)"
+
   lessThan   :: "nat => nat set"
      "lessThan n == {i. i<n}"
 
diff -r e5e019d60f71 -r 43b03d412b82 src/HOL/UNITY/Lift_prog.ML
--- a/src/HOL/UNITY/Lift_prog.ML	Mon Oct 18 15:17:35 1999 +0200
+++ b/src/HOL/UNITY/Lift_prog.ML	Mon Oct 18 15:18:24 1999 +0200
@@ -54,13 +54,8 @@
 qed "lift_act_eq";
 AddIffs [lift_act_eq];
 
-Goalw [drop_act_def]
-     "[| (s, s') : act;  s : C |] ==> (s i, s' i) : drop_act C i act";
-by Auto_tac;
-qed "drop_act_I";
-
 Goalw [drop_set_def, drop_act_def]
-     "UNIV <= drop_set i C ==> drop_act C i Id = Id";
+     "UNIV <= drop_set i C ==> drop_act i (Restrict C Id) = Id";
 by (Blast_tac 1);
 qed "drop_act_Id";
 Addsimps [drop_act_Id];
@@ -82,7 +77,7 @@
 qed "Init_drop_prog";
 Addsimps [Init_drop_prog];
 
-Goal "Acts (drop_prog C i F) = insert Id (drop_act C i `` Acts F)";
+Goal "Acts (drop_prog C i F) = insert Id (drop_act i `` Restrict C `` Acts F)";
 by (auto_tac (claset() addIs [Id_in_Acts RSN (2,image_eqI)], 
 	      simpset() addsimps [drop_prog_def]));
 qed "Acts_drop_prog";
@@ -169,7 +164,7 @@
 by (auto_tac (claset() addSIs [exI], simpset()));
 qed "lift_act_correct";
 
-Goal "drop_act C i = project_act C (lift_map i)";
+Goal "drop_act i = project_act (lift_map i)";
 by (rtac ext 1);
 by (rewrite_goals_tac [project_act_def, drop_act_def, lift_map_def]);
 by Auto_tac;
@@ -230,12 +225,14 @@
 qed "lift_set_UNIV_eq";
 Addsimps [lift_set_UNIV_eq];
 
-Goal "Domain act <= drop_set i C ==> drop_act C i (lift_act i act) = act";
+(*
+Goal "Domain act <= drop_set i C ==> drop_act i (Restrict C (lift_act i act)) = act";
 by (asm_full_simp_tac
     (simpset() addsimps [drop_set_correct, drop_act_correct, 
 			 lift_act_correct, lift_export extend_act_inverse]) 1);
 qed "lift_act_inverse";
 Addsimps [lift_act_inverse];
+*)
 
 Goal "UNIV <= drop_set i C ==> drop_prog C i (lift_prog i F) = F";
 by (asm_full_simp_tac
@@ -314,9 +311,8 @@
 
 (*** Diff, needed for localTo ***)
 
-Goal "[| (UN act:acts. Domain act) <= drop_set i C; \
-\        Diff G (lift_act i `` acts) : (lift_set i A) co (lift_set i B) |]  \
-\     ==> Diff (drop_prog C i G) acts : A co B";
+Goal "[| Diff C G (lift_act i `` acts) : (lift_set i A) co (lift_set i B) |] \
+\     ==> Diff (drop_set i C) (drop_prog C i G) acts : A co B";
 by (asm_full_simp_tac
     (simpset() addsimps [drop_set_correct, drop_prog_correct, 
 			 lift_set_correct, lift_act_correct, 
@@ -324,27 +320,11 @@
 qed "Diff_drop_prog_constrains";
 
 Goalw [stable_def]
-     "[| (UN act:acts. Domain act) <= drop_set i C; \
-\        Diff G (lift_act i `` acts) : stable (lift_set i A) |]  \
-\     ==> Diff (drop_prog C i G) acts : stable A";
-by (etac Diff_drop_prog_constrains 1);
-by (assume_tac 1);
+     "[| Diff C G (lift_act i `` acts) : stable (lift_set i A) |]  \
+\     ==> Diff (drop_set i C) (drop_prog C i G) acts : stable A";
+by (blast_tac (claset() addIs [Diff_drop_prog_constrains]) 1);
 qed "Diff_drop_prog_stable";
 
-Goalw [constrains_def, Diff_def]
-     "Diff G acts : A co B  \
-\     ==> Diff (lift_prog i G) (lift_act i `` acts) \
-\         : (lift_set i A) co (lift_set i B)";
-by Auto_tac;
-by (Blast_tac 1);
-qed "Diff_lift_prog_co";
-
-Goalw [stable_def]
-     "Diff G acts : stable A  \
-\     ==> Diff (lift_prog i G) (lift_act i `` acts) : stable (lift_set i A)";
-by (etac Diff_lift_prog_co 1);
-qed "Diff_lift_prog_stable";
-
 
 (*** Weak safety primitives: Co, Stable ***)
 
@@ -466,19 +446,19 @@
 by (asm_full_simp_tac (simpset() addsimps [lift_prog_correct, o_def]) 1);
 qed "lift_prog_guar_Increasing";
 
-Goal "F : (v localTo G) guarantees increasing func  \
-\     ==> lift_prog i F : (v o sub i) localTo (lift_prog i G)  \
+Goal "F : (v localTo[UNIV] G) guarantees increasing func  \
+\     ==> lift_prog i F : (v o sub i) localTo[UNIV] (lift_prog i G)  \
 \                         guarantees increasing (func o sub i)";
 by (dtac (lift_export extend_localTo_guar_increasing) 1);
 by (asm_full_simp_tac (simpset() addsimps [lift_prog_correct, o_def]) 1);
 qed "lift_prog_localTo_guar_increasing";
 
-Goal "F : (v localTo G) guarantees Increasing func  \
-\     ==> lift_prog i F : (v o sub i) localTo (lift_prog i G)  \
+Goal "F : (v LocalTo G) guarantees Increasing func  \
+\     ==> lift_prog i F : (v o sub i) LocalTo (lift_prog i G)  \
 \                         guarantees Increasing (func o sub i)";
-by (dtac (lift_export extend_localTo_guar_Increasing) 1);
+by (dtac (lift_export extend_LocalTo_guar_Increasing) 1);
 by (asm_full_simp_tac (simpset() addsimps [lift_prog_correct, o_def]) 1);
-qed "lift_prog_localTo_guar_Increasing";
+qed "lift_prog_LocalTo_guar_Increasing";
 
 Goal "F : Always A guarantees Always B \
 \ ==> lift_prog i F : Always(lift_set i A) guarantees Always (lift_set i B)";
diff -r e5e019d60f71 -r 43b03d412b82 src/HOL/UNITY/Lift_prog.thy
--- a/src/HOL/UNITY/Lift_prog.thy	Mon Oct 18 15:17:35 1999 +0200
+++ b/src/HOL/UNITY/Lift_prog.thy	Mon Oct 18 15:18:24 1999 +0200
@@ -22,19 +22,19 @@
   lift_act :: "['a, ('b*'b) set] => (('a=>'b) * ('a=>'b)) set"
     "lift_act i act == {(f,f'). f(i:= f' i) = f' & (f i, f' i) : act}"
 
-  (*Argument C allows weak safety laws to be projected*)
-  drop_act :: "[('a=>'b) set, 'a, (('a=>'b) * ('a=>'b)) set] => ('b*'b) set"
-    "drop_act C i act == {(f i, f' i) | f f'. (f,f'): act & f: C}"
+  drop_act :: "['a, (('a=>'b) * ('a=>'b)) set] => ('b*'b) set"
+    "drop_act i act == {(f i, f' i) | f f'. (f,f'): act}"
 
   lift_prog :: "['a, 'b program] => ('a => 'b) program"
     "lift_prog i F ==
        mk_program (lift_set i (Init F),
 		   lift_act i `` Acts F)"
 
+  (*Argument C allows weak safety laws to be projected*)
   drop_prog :: "[('a=>'b) set, 'a, ('a=>'b) program] => 'b program"
     "drop_prog C i F ==
        mk_program (drop_set i (Init F),
-		   drop_act C i `` (Acts F))"
+		   drop_act i `` Restrict C `` (Acts F))"
 
   (*simplifies the expression of specifications*)
   constdefs
diff -r e5e019d60f71 -r 43b03d412b82 src/HOL/UNITY/Project.ML
--- a/src/HOL/UNITY/Project.ML	Mon Oct 18 15:17:35 1999 +0200
+++ b/src/HOL/UNITY/Project.ML	Mon Oct 18 15:18:24 1999 +0200
@@ -12,7 +12,7 @@
 
 (** projection: monotonicity for safety **)
 
-Goal "D <= C ==> project_act D h act <= project_act C h act";
+Goal "D <= C ==> project_act h (Restrict D act) <= project_act h (Restrict C act)";
 by (auto_tac (claset(), simpset() addsimps [project_act_def]));
 qed "project_act_mono";
 
@@ -35,8 +35,8 @@
 Goal "UNIV <= project_set h C \
 \     ==> project C h ((extend h F) Join G) = F Join (project C h G)";
 by (rtac program_equalityI 1);
-by (asm_simp_tac (simpset() addsimps [image_Un, image_image,
-			subset_UNIV RS subset_trans RS extend_act_inverse]) 2);
+by (asm_simp_tac (simpset() addsimps [image_Un, image_image_eq_UN, image_UN,
+			subset_UNIV RS subset_trans RS Restrict_triv]) 2);
 by (simp_tac (simpset() addsimps [project_set_extend_set_Int]) 1);
 qed "project_extend_Join";
 
@@ -231,61 +231,106 @@
 (*Opposite direction fails because Diff in the extended state may remove
   fewer actions, i.e. those that affect other state variables.*)
 
-Goal "Diff (project C h G) (project_act C h `` acts) <= \
-\         project C h (Diff G acts)";
-by (auto_tac (claset(), simpset() addsimps [component_eq_subset, Diff_def,
-					    UN_subset_iff]));
+Goalw [project_set_def, project_act_def]
+     "Restrict (project_set h C) (project_act h (Restrict C act)) = \
+\     project_act h (Restrict C act)";
+by (Blast_tac 1);
+qed "Restrict_project_act";
+
+Goalw [project_set_def, project_act_def]
+     "project_act h (Restrict C Id) = Restrict (project_set h C) Id";
+by (Blast_tac 1);
+qed "project_act_Restrict_Id";
+
+Goal
+  "Diff(project_set h C)(project C h G)(project_act h `` Restrict C `` acts) \
+\  <= project C h (Diff C G acts)";
+by (simp_tac 
+    (simpset() addsimps [component_eq_subset, Diff_def,
+			 Restrict_project_act, project_act_Restrict_Id, 
+			 image_image_eq_UN, image_UN, Restrict_image_Diff]) 1);
+by (Force_tac 1);
 qed "Diff_project_project_component_project_Diff";
 
-Goal "(UN act:acts. Domain act) <= project_set h C \
-\     ==> Diff (project C h G) acts <= \
-\         project C h (Diff G (extend_act h `` acts))";
-by (asm_full_simp_tac (simpset() addsimps [component_eq_subset, Diff_def,
-					   UN_subset_iff]) 1);
-by (force_tac (claset() addSIs [image_diff_subset RS subsetD], 
-	       simpset() addsimps [image_image_eq_UN]) 1);
+Goal "Diff (project_set h C) (project C h G) acts <= \
+\         project C h (Diff C G (extend_act h `` acts))";
+by (rtac component_trans 1);
+by (rtac Diff_project_project_component_project_Diff 2);
+by (simp_tac 
+    (simpset() addsimps [component_eq_subset, Diff_def,
+			 Restrict_project_act, project_act_Restrict_Id, 
+			 image_image_eq_UN, image_UN, Restrict_image_Diff]) 1);
+by (Blast_tac 1);
 qed "Diff_project_component_project_Diff";
 
-Goal
-   "[| (UN act:acts. Domain act) <= project_set h C; \
-\      Diff G (extend_act h `` acts) : (extend_set h A) co (extend_set h B) |]\
-\   ==> Diff (project C h G) acts : A co B";
-by (etac (Diff_project_component_project_Diff RS component_constrains) 1);
+Goal "Diff C G (extend_act h `` acts) : (extend_set h A) co (extend_set h B) \
+\     ==> Diff (project_set h C) (project C h G) acts : A co B";
+by (rtac (Diff_project_component_project_Diff RS component_constrains) 1);
 by (rtac (project_constrains RS iffD2) 1);
 by (ftac constrains_imp_subset 1);
-by (Asm_full_simp_tac 1);
 by (blast_tac (claset() addIs [constrains_weaken]) 1);
 qed "Diff_project_constrains";
 
 Goalw [stable_def]
-     "[| (UN act:acts. Domain act) <= project_set h C; \
-\        Diff G (extend_act h `` acts) : stable (extend_set h A) |] \
-\     ==> Diff (project C h G) acts : stable A";
+     "Diff C G (extend_act h `` acts) : stable (extend_set h A) \
+\     ==> Diff (project_set h C) (project C h G) acts : stable A";
 by (etac Diff_project_constrains 1);
-by (assume_tac 1);
 qed "Diff_project_stable";
 
+(** Some results for Diff, extend and project_set **)
+
+Goal "Diff C (extend h G) (extend_act h `` acts) \
+\         : (extend_set h A) co (extend_set h B) \
+\     ==> Diff (project_set h C) G acts : A co B";
+br (Diff_project_set_component RS component_constrains) 1;
+by (forward_tac [constrains_imp_subset] 1);
+by (asm_full_simp_tac
+    (simpset() addsimps [project_constrains, extend_set_strict_mono]) 1);
+by (blast_tac (claset() addIs [constrains_weaken]) 1);
+qed "Diff_project_set_constrains_I";
+
+Goalw [stable_def]
+     "Diff C (extend h G) (extend_act h `` acts) : stable (extend_set h A) \
+\     ==> Diff (project_set h C) G acts : stable A";
+by (asm_simp_tac (simpset() addsimps [Diff_project_set_constrains_I]) 1);
+qed "Diff_project_set_stable_I";
+
+Goalw [LOCALTO_def]
+     "extend h F : (v o f) localTo[C] extend h H \
+\     ==> F : v localTo[project_set h C] H";
+by Auto_tac;
+br Diff_project_set_stable_I 1;
+by (asm_simp_tac (simpset() addsimps [Collect_eq_extend_set RS sym]) 1);
+qed "localTo_project_set_I";
+
 (*Converse fails: even if the conclusion holds, H could modify (v o f) 
   simultaneously with other variables, and this action would not be 
   superseded by anything in (extend h G) *)
-Goal "[| UNIV <= project_set h C;  H : (func o f) localTo extend h G |] \
-\     ==> project C h H : func localTo G";
+Goal "H : (v o f) localTo[C] extend h G \
+\     ==> project C h H : v localTo[project_set h C] G";
 by (asm_full_simp_tac 
-    (simpset() addsimps [localTo_def, 
+    (simpset() addsimps [LOCALTO_def, 
 			 project_extend_Join RS sym,
-			 subset_UNIV RS subset_trans RS Diff_project_stable,
+			 Diff_project_stable,
 			 Collect_eq_extend_set RS sym]) 1);
 qed "project_localTo_lemma";
 
-Goal "extend h F Join G : (v o f) localTo extend h H \
-\     ==> F Join project UNIV h G : v localTo H";
-by (stac (project_set_UNIV RS project_extend_Join RS sym) 1);
-by (asm_simp_tac 
-    (simpset() addsimps [project_set_UNIV RS project_localTo_lemma]) 1);
+Goal "extend h F Join G : (v o f) localTo[C] extend h H \
+\     ==> F Join project C h G : v localTo[project_set h C] H";
+by (asm_full_simp_tac 
+    (simpset() addsimps [Join_localTo, localTo_project_set_I,
+			 project_localTo_lemma]) 1);
+qed "gen_project_localTo_I";
+
+Goal "extend h F Join G : (v o f) localTo[UNIV] extend h H \
+\     ==> F Join project UNIV h G : v localTo[UNIV] H";
+bd gen_project_localTo_I 1;
+by (Asm_full_simp_tac 1);
 qed "project_localTo_I";
 
 Goalw [projecting_def]
-     "projecting (%G. UNIV) h F ((v o f) localTo extend h H) (v localTo H)";
+     "projecting (%G. UNIV) h F \
+\         ((v o f) localTo[UNIV] extend h H)  (v localTo[UNIV] H)";
 by (blast_tac (claset() addIs [project_localTo_I]) 1);
 qed "projecting_localTo";
 
@@ -428,6 +473,13 @@
 				      Collect_eq_extend_set RS sym]) 1);
 qed "project_Increasing";
 
+Goal "extend h F Join G : (v o f) LocalTo extend h H \
+\     ==> F Join project (reachable (extend h F Join G)) h G : v LocalTo H";
+by (asm_full_simp_tac 
+    (simpset() addsimps [LocalTo_def, project_set_reachable_extend_eq RS sym,
+			 gen_project_localTo_I]) 1);
+qed "project_LocalTo_I";
+
 (** A lot of redundant theorems: all are proved to facilitate reasoning
     about guarantees. **)
 
@@ -455,6 +507,12 @@
 by (blast_tac (claset() addIs [project_Increasing_I]) 1);
 qed "projecting_Increasing";
 
+Goalw [projecting_def]
+     "projecting (%G. reachable (extend h F Join G)) h F \
+\         ((v o f) LocalTo extend h H)  (v LocalTo H)";
+by (blast_tac (claset() addIs [project_LocalTo_I]) 1);
+qed "projecting_LocalTo";
+
 Goalw [extending_def]
      "extending (%G. reachable (extend h F Join G)) h F X' \
 \               (extend_set h A Co extend_set h B) (A Co B)";
@@ -510,7 +568,7 @@
   being enabled for all possible values of the new variables.*)
 Goalw [transient_def]
      "[| project C h F : transient A;  \
-\        ALL act: Acts F. project_act C h act ^^ A <= - A --> \
+\        ALL act: Acts F. project_act h (Restrict C act) ^^ A <= - A --> \
 \                         Domain act <= C \
 \             & extend_set h (project_set h (Domain act)) <= Domain act |]  \
 \     ==> F : transient (extend_set h A)";
@@ -622,7 +680,8 @@
 \     extend h F : (extend h `` X) guarantees (extend h `` Y)";
 by (rtac guaranteesI 1);
 by Auto_tac;
-by (blast_tac (claset() addDs [project_set_UNIV RS extend_Join_eq_extend_D, 
+by (blast_tac (claset() addDs [project_set_UNIV RS equalityD2 RS 
+			         extend_Join_eq_extend_D, 
 			       guaranteesD]) 1);
 qed "guarantees_imp_extend_guarantees";
 
@@ -650,7 +709,7 @@
 Goal "[| F : X guarantees Y;  \
 \        !!G. extend h F Join G : X' ==> F Join proj G h G : X;  \
 \        !!G. [| F Join proj G h G : Y; extend h F Join G : X'; \
-\                Disjoint (extend h F) G |] \
+\                Disjoint UNIV (extend h F) G |] \
 \             ==> extend h F Join G : Y' |] \
 \     ==> extend h F : X' guarantees Y'";
 by (rtac (xguary RS guaranteesD RS extend RS guaranteesI) 1);
@@ -689,22 +748,22 @@
 by Auto_tac;
 qed "extend_guar_Increasing";
 
-Goal "F : (v localTo G) guarantees increasing func  \
-\     ==> extend h F : (v o f) localTo (extend h G)  \
+Goal "F : (v localTo[UNIV] G) guarantees increasing func  \
+\     ==> extend h F : (v o f) localTo[UNIV] (extend h G)  \
 \                      guarantees increasing (func o f)";
 by (etac project_guarantees 1);
 by (rtac extending_increasing 2);
 by (rtac projecting_localTo 1);
 qed "extend_localTo_guar_increasing";
 
-Goal "F : (v localTo G) guarantees Increasing func  \
-\     ==> extend h F : (v o f) localTo (extend h G)  \
+Goal "F : (v LocalTo G) guarantees Increasing func  \
+\     ==> extend h F : (v o f) LocalTo (extend h G)  \
 \                      guarantees Increasing (func o f)";
 by (etac project_guarantees 1);
 by (rtac extending_Increasing 2);
-by (rtac projecting_localTo 1);
+by (rtac projecting_LocalTo 1);
 by Auto_tac;
-qed "extend_localTo_guar_Increasing";
+qed "extend_LocalTo_guar_Increasing";
 
 Goal "F : Always A guarantees Always B \
 \ ==> extend h F : Always(extend_set h A) guarantees Always(extend_set h B)";
@@ -729,8 +788,15 @@
 but it can fail if C removes some parts of an action of G.*)
 
 
-Goal "[| G : f localTo extend h F; \
-\        Disjoint (extend h F) G |] ==> project C h G : stable {x}";
+Goal "[| G : v localTo[UNIV] F;  Disjoint UNIV F G |] ==> G : stable {s. v s = z}";
+by (asm_full_simp_tac 
+    (simpset() addsimps [LOCALTO_def, Diff_def, Disjoint_def,
+			 stable_def, constrains_def]) 1);
+by (Blast_tac 1);
+qed "localTo_imp_stable";
+
+Goal "[| G : f localTo[UNIV] extend h F; \
+\        Disjoint UNIV (extend h F) G |] ==> project C h G : stable {x}";
 by (asm_full_simp_tac
     (simpset() addsimps [localTo_imp_stable,
 			 extend_set_sing, project_stable_I]) 1);
@@ -742,14 +808,9 @@
 				  stable_def, constrains_def]));
 qed "stable_sing_imp_not_transient";
 
-by (auto_tac (claset(), 
-	      simpset() addsimps [FP_def, transient_def,
-				  stable_def, constrains_def]));
-qed "stable_sing_imp_not_transient";
-
 Goal "[| F Join project UNIV h G : A leadsTo B;    \
-\        G : f localTo extend h F; \
-\        Disjoint (extend h F) G |]  \
+\        G : f localTo[UNIV] extend h F; \
+\        Disjoint UNIV (extend h F) G |]  \
 \     ==> extend h F Join G : (extend_set h A) leadsTo (extend_set h B)";
 by (rtac project_UNIV_leadsTo_lemma 1);
 by (Clarify_tac 1);
@@ -760,8 +821,8 @@
 qed "project_leadsTo_D";
 
 Goal "[| F Join project (reachable (extend h F Join G)) h G : A LeadsTo B; \
-\         G : f localTo extend h F; \
-\         Disjoint (extend h F) G |]  \
+\         G : f localTo[UNIV] extend h F; \
+\         Disjoint UNIV (extend h F) G |]  \
 \      ==> extend h F Join G : (extend_set h A) LeadsTo (extend_set h B)";
 by (rtac (refl RS Join_project_LeadsTo) 1);
 by (Clarify_tac 1);
@@ -773,7 +834,7 @@
 
 Goalw [extending_def]
      "extending (%G. UNIV) h F \
-\                (f localTo extend h F) \
+\                (f localTo[UNIV] extend h F) \
 \                (extend_set h A leadsTo extend_set h B) (A leadsTo B)";
 by (blast_tac (claset() addSDs [Join_localTo RS iffD1]
 			addIs [project_leadsTo_D]) 1);
@@ -781,7 +842,7 @@
 
 Goalw [extending_def]
      "extending (%G. reachable (extend h F Join G)) h F \
-\               (f localTo extend h F) \
+\               (f localTo[UNIV] extend h F) \
 \               (extend_set h A LeadsTo extend_set h B) (A LeadsTo B)";
 by (blast_tac (claset() addSDs [Join_localTo RS iffD1]
 			addIs [project_LeadsTo_D]) 1);
@@ -790,7 +851,7 @@
 (*STRONG precondition and postcondition*)
 Goal "F : (A co A') guarantees (B leadsTo B')  \
 \ ==> extend h F : ((extend_set h A) co (extend_set h A'))  \
-\                   Int (f localTo (extend h F)) \
+\                   Int (f localTo[UNIV] (extend h F)) \
 \                  guarantees ((extend_set h B) leadsTo (extend_set h B'))";
 by (etac project_guarantees 1);
 by (rtac (extending_leadsTo RS extending_weaken) 2);
@@ -801,7 +862,7 @@
 (*WEAK precondition and postcondition*)
 Goal "F : (A Co A') guarantees (B LeadsTo B')  \
 \ ==> extend h F : ((extend_set h A) Co (extend_set h A'))  \
-\                   Int (f localTo (extend h F)) \
+\                   Int (f localTo[UNIV] (extend h F)) \
 \                  guarantees ((extend_set h B) LeadsTo (extend_set h B'))";
 by (etac project_guarantees 1);
 by (rtac (extending_LeadsTo RS extending_weaken) 2);
diff -r e5e019d60f71 -r 43b03d412b82 src/HOL/UNITY/Project.thy
--- a/src/HOL/UNITY/Project.thy	Mon Oct 18 15:17:35 1999 +0200
+++ b/src/HOL/UNITY/Project.thy	Mon Oct 18 15:18:24 1999 +0200
@@ -20,7 +20,7 @@
 		 'c program set, 'c program set, 'a program set] => bool"
   "extending C h F X' Y' Y ==
      ALL G. F Join project (C G) h G : Y & extend h F Join G : X' &
-            Disjoint (extend h F) G
+            Disjoint UNIV (extend h F) G
             --> extend h F Join G : Y'"
 
 end
diff -r e5e019d60f71 -r 43b03d412b82 src/HOL/UNITY/Union.ML
--- a/src/HOL/UNITY/Union.ML	Mon Oct 18 15:17:35 1999 +0200
+++ b/src/HOL/UNITY/Union.ML	Mon Oct 18 15:18:24 1999 +0200
@@ -288,98 +288,122 @@
 
 (** Diff and localTo **)
 
-Goalw [Diff_def] "F Join (Diff G (Acts F)) = F Join G";
+Goalw [Diff_def] "F Join (Diff UNIV G (Acts F)) = F Join G";
 by (rtac program_equalityI 1);
 by Auto_tac;
 qed "Join_Diff2";
 
 Goalw [Diff_def]
-     "Diff (F Join G) (Acts H) = (Diff F (Acts H)) Join (Diff G (Acts H))";
+   "Diff C (F Join G) (Acts H) = (Diff C F (Acts H)) Join (Diff C G (Acts H))";
 by (rtac program_equalityI 1);
 by Auto_tac;
 qed "Diff_Join_distrib";
 
-Goalw [Diff_def, constrains_def] "(Diff F (Acts F) : A co B) = (A <= B)";
+Goalw [Diff_def] "Diff C F (Acts F) = mk_program(Init F, {})";
 by Auto_tac;
-qed "Diff_self_constrains";
+qed "Diff_self_eq";
 
-Goalw [Diff_def, Disjoint_def] "Disjoint F (Diff G (Acts F))";
-by Auto_tac;
+Goalw [Diff_def, Disjoint_def] "Disjoint C F (Diff C G (Acts F))";
+by (force_tac (claset(), 
+	       simpset() addsimps [Restrict_imageI, 
+				   sym RSN (2,Restrict_imageI)]) 1);
 qed "Diff_Disjoint";
 
-Goal "[| G : v localTo F;  Disjoint F G |] ==> G : stable {s. v s = z}";
-by (asm_full_simp_tac 
-    (simpset() addsimps [localTo_def, Diff_def, Disjoint_def,
-			 stable_def, constrains_def]) 1);
-by (Blast_tac 1);
-qed "localTo_imp_stable";
+Goalw [Disjoint_def]
+     "[| A <= B; Disjoint A F G |] ==> Disjoint B F G";
+by (blast_tac (claset() addIs [Restrict_eq_mono RSN (2,Restrict_imageI)]) 1);
+qed "Disjoint_mono";
+
+(*** localTo ***)
 
-Goalw [localTo_def, stable_def, constrains_def]
-     "v localTo F <= (f o v) localTo F";
+Goalw [LOCALTO_def, Diff_def, stable_def, constrains_def]
+     "A <= B ==> v localTo[B] F <= v localTo[A] F";
+by Auto_tac;
+by (dres_inst_tac [("x", "v xc")] spec 1);
+by (dres_inst_tac [("x", "Restrict B xa")] bspec 1);
+by Auto_tac;
+by (blast_tac (claset() addIs [Restrict_eq_mono RSN (2,Restrict_imageI)]) 1);
+qed "localTo_anti_mono";
+
+Goalw [LocalTo_def]
+     "G : v localTo[UNIV] F ==> G : v LocalTo F";
+by (blast_tac (claset() addDs [impOfSubs localTo_anti_mono]) 1);
+qed "localTo_imp_LocalTo";
+
+Goalw [LOCALTO_def, stable_def, constrains_def]
+     "v localTo[C] F <= (f o v) localTo[C] F";
 by (Clarify_tac 1);
 by (force_tac (claset() addSEs [allE, ballE], simpset()) 1);
 qed "localTo_imp_o_localTo";
 
-Goalw [localTo_def, stable_def, constrains_def]
-     "(%s. x) localTo F = UNIV";
+Goalw [LOCALTO_def, stable_def, constrains_def]
+     "(%s. x) localTo[C] F = UNIV";
 by (Blast_tac 1);
 qed "triv_localTo_eq_UNIV";
 
-Goal "(F Join G : v localTo H) = (F : v localTo H  &  G : v localTo H)";
+Goal "(F Join G : v localTo[C] H) = (F : v localTo[C] H  &  G : v localTo[C] H)";
 by (asm_full_simp_tac 
-    (simpset() addsimps [localTo_def, Diff_Join_distrib,
+    (simpset() addsimps [LOCALTO_def, Diff_Join_distrib,
 			 stable_def, Join_constrains]) 1);
 by (Blast_tac 1);
 qed "Join_localTo";
 
-Goal "F : v localTo F";
+Goal "F : v localTo[C] F";
 by (simp_tac 
-    (simpset() addsimps [localTo_def, stable_def, Diff_self_constrains]) 1);
+    (simpset() addsimps [LOCALTO_def, stable_def, constrains_def, 
+			 Diff_self_eq]) 1);
 qed "self_localTo";
 
 
 
 (*** Higher-level rules involving localTo and Join ***)
 
-Goal "[| F : {s. P (v s)} co {s. P' (v s)};  G : v localTo F |]  \
-\     ==> F Join G : {s. P (v s)} co {s. P' (v s)}";
-by (asm_simp_tac (simpset() addsimps [Join_constrains]) 1);
+Goal "[| F : {s. P (v s)} co {s. P' (v s)};  G : v localTo[C] F |]  \
+\     ==> G : C Int {s. P (v s)} co {s. P' (v s)}";
+by (ftac constrains_imp_subset 1);
 by (auto_tac (claset(), 
-	      simpset() addsimps [localTo_def, stable_def, constrains_def,
+	      simpset() addsimps [LOCALTO_def, stable_def, constrains_def,
 				  Diff_def]));
-by (case_tac "act: Acts F" 1);
-by (Blast_tac 1);
-by (dtac bspec 1 THEN rtac Id_in_Acts 1);
+by (case_tac "Restrict C act: Restrict C `` Acts F" 1);
+by (blast_tac (claset() addSEs [equalityE]) 1);
 by (subgoal_tac "v x = v xa" 1);
+by (Force_tac 1);
+by (thin_tac "ALL act: ?A. ?P act" 1);
+by (dtac spec 1);
+by (dres_inst_tac [("x", "Restrict C act")] bspec 1);
 by Auto_tac;
 qed "constrains_localTo_constrains";
 
-Goalw [localTo_def, stable_def, constrains_def, Diff_def]
-     "[| G : v localTo F;  G : w localTo F |]  \
-\     ==> G : (%s. (v s, w s)) localTo F";
+Goalw [LOCALTO_def, stable_def, constrains_def, Diff_def]
+     "[| G : v localTo[C] F;  G : w localTo[C] F |]  \
+\     ==> G : (%s. (v s, w s)) localTo[C] F";
 by (Blast_tac 1);
 qed "localTo_pairfun";
 
 Goal "[| F : {s. P (v s) (w s)} co {s. P' (v s) (w s)};   \
-\        G : v localTo F;       \
-\        G : w localTo F |]               \
-\     ==> F Join G : {s. P (v s) (w s)} co {s. P' (v s) (w s)}";
-by (res_inst_tac [("A", "{s. (%(x,y). P x y) (v s, w s)}"),
+\        G : v localTo[C] F;       \
+\        G : w localTo[C] F |]               \
+\     ==> G : C Int {s. P (v s) (w s)} co {s. P' (v s) (w s)}";
+by (res_inst_tac [("A", "C Int {s. (%(x,y). P x y) (v s, w s)}"),
 		  ("A'", "{s. (%(x,y). P' x y) (v s, w s)}")] 
     constrains_weaken 1);
 by (rtac (localTo_pairfun RSN (2, constrains_localTo_constrains)) 1);
 by Auto_tac;
 qed "constrains_localTo_constrains2";
 
+(*Used just once, in Client.ML.  Having F in the conclusion is silly.*)
 Goalw [stable_def]
      "[| F : stable {s. P (v s) (w s)};   \
-\        G : v localTo F;  G : w localTo F |]               \
+\        G : v localTo[UNIV] F;  G : w localTo[UNIV] F |]               \
 \     ==> F Join G : stable {s. P (v s) (w s)}";
-by (blast_tac (claset() addIs [constrains_localTo_constrains2]) 1);
+by (asm_simp_tac (simpset() addsimps [Join_constrains]) 1);
+by (blast_tac (claset() addIs [constrains_localTo_constrains2 RS 
+			       constrains_weaken]) 1);
 qed "stable_localTo_stable2";
 
+(*Used just in Client.ML.  Generalize to arbitrary C?*)
 Goal "[| F : stable {s. v s <= w s};   \
-\        G : v localTo F;       \
+\        G : v localTo[UNIV] F;       \
 \        F Join G : Increasing w |]               \
 \     ==> F Join G : Stable {s. v s <= w s}";
 by (auto_tac (claset(), 
@@ -388,8 +412,8 @@
 by (blast_tac (claset() addIs [constrains_weaken]) 1);
 (*The G case remains; proved like constrains_localTo_constrains*)
 by (auto_tac (claset(), 
-	      simpset() addsimps [localTo_def, stable_def, constrains_def,
-				  Diff_def]));
+              simpset() addsimps [LOCALTO_def, stable_def, constrains_def,
+                                  Diff_def]));
 by (case_tac "act: Acts F" 1);
 by (Blast_tac 1);
 by (thin_tac "ALL act:Acts F. ?P act" 1);
diff -r e5e019d60f71 -r 43b03d412b82 src/HOL/UNITY/Union.thy
--- a/src/HOL/UNITY/Union.thy	Mon Oct 18 15:17:35 1999 +0200
+++ b/src/HOL/UNITY/Union.thy	Mon Oct 18 15:18:24 1999 +0200
@@ -22,17 +22,25 @@
   SKIP :: 'a program
     "SKIP == mk_program (UNIV, {})"
 
-  Diff :: "['a program, ('a * 'a)set set] => 'a program"
-    "Diff F acts == mk_program (Init F, Acts F - acts)"
+  Diff :: "['a set, 'a program, ('a * 'a)set set] => 'a program"
+    "Diff C G acts ==
+       mk_program (Init G, (Restrict C `` Acts G) - (Restrict C `` acts))"
 
   (*The set of systems that regard "v" as local to F*)
-  localTo :: ['a => 'b, 'a program] => 'a program set  (infixl 80)
-    "v localTo F == {G. ALL z. Diff G (Acts F) : stable {s. v s = z}}"
+  LOCALTO :: ['a => 'b, 'a set, 'a program] => 'a program set
+                                           ("(_/ localTo[_]/ _)" [80,0,80] 80)
+    "v localTo[C] F == {G. ALL z. Diff C G (Acts F) : stable {s. v s = z}}"
+
+  (*The weak version of localTo, considering only G's reachable states*)
+  LocalTo :: ['a => 'b, 'a program] => 'a program set  (infixl 80)
+    "v LocalTo F == {G. G : v localTo[reachable G] F}"
 
   (*Two programs with disjoint actions, except for identity actions.
     It's a weak property but still useful.*)
-  Disjoint :: ['a program, 'a program] => bool
-    "Disjoint F G == Acts F Int Acts G <= {Id}"
+  Disjoint :: ['a set, 'a program, 'a program] => bool
+    "Disjoint C F G ==
+       (Restrict C `` (Acts F - {Id})) Int (Restrict C `` (Acts G - {Id}))
+       <= {}"
 
 syntax
   "@JOIN1"     :: [pttrns, 'b set] => 'b set         ("(3JN _./ _)" 10)