# HG changeset patch
# User paulson
# Date 941022212 -7200
# Node ID b999c1ab932737fca242ee31b6b5b17946551498
# Parent  95e1de322e82efbd182838bba625608b066468ed
working again; new treatment of LocalTo

diff -r 95e1de322e82 -r b999c1ab9327 src/HOL/UNITY/Alloc.ML
--- a/src/HOL/UNITY/Alloc.ML	Wed Oct 27 13:02:23 1999 +0200
+++ b/src/HOL/UNITY/Alloc.ML	Wed Oct 27 13:03:32 1999 +0200
@@ -402,8 +402,35 @@
 by (auto_tac (claset(), simpset() addsimps [o_def]));
 qed "Client_i_Progress";
 
+Goal "extend sysOfAlloc F \
+\       : (v o client) localTo[C] extend sysOfClient (lift_prog i Client)";
+br localTo_UNIV_imp_localTo 1;
+by (simp_tac (simpset() addsimps [LOCALTO_def, Diff_def, extend_def, 
+				  stable_def, constrains_def,
+				  image_eq_UN, extend_act_def,
+				  sysOfAlloc_def, sysOfClient_def]) 1);
+by (Force_tac 1);
+qed "sysOfAlloc_in_client_localTo_xl_Client";
+
+Goal "extend sysOfClient (plam x: I. Client) : ((%z. z i) o client) \
+\     localTo[C] extend sysOfClient (lift_prog i Client)";
+br localTo_UNIV_imp_localTo 1;
+by (rtac (client_export (extend_set_UNIV_eq RS equalityD2 RSN
+			 (2, extend_localTo_extend_I))) 1);
+br (rewrite_rule [sub_def] PLam_sub_localTo) 1;
+qed "sysOfClient_in_client_localTo_xl_Client";
+
 xxxxxxxxxxxxxxxx;
 
+THIS PROOF requires an extra locality specification for Network:
+    Network : rel o sub i o client localTo[C] 
+                     extend sysOfClient (lift_prog i Client)
+and similarly for ask o sub i o client.
+
+The LeadsTo rule must be refined so as not to require the whole of client to
+be local, since giv is written by the Network.
+
+
 Goalw [System_def]
      "i < Nclients \
 \ ==> System : (INT h. {s. h <=  (giv o sub i o client) s & \
@@ -411,17 +438,23 @@
 \            LeadsTo {s. tokens h <= (tokens o rel o sub i o client) s})";
 by (rtac (guarantees_Join_I2 RS guaranteesD) 1);
 by (rtac (guarantees_PLam_I RS project_guarantees) 1);
-by (rtac Client_i_Progress  1);
+by (rtac Client_i_Progress 1);
 by (Force_tac 1);
 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);
-by (rtac projecting_Int 1);
-by (rtac (client_export projecting_Increasing) 1);
-by (rtac (client_export projecting_localTo) 1);
+(*The next step goes wrong: it makes an impossible localTo subgoal*)
+(*blast_tac doesn't use HO unification*)
+by (fast_tac (claset() addIs [projecting_Int,
+			      client_export projecting_Increasing,
+			      component_PLam,
+			      client_export projecting_LocalTo]) 1);
+by (asm_simp_tac
+    (simpset() addsimps [rewrite_rule [System_def] System_Increasing_giv,
+			 LocalTo_def, Join_localTo,
+			 sysOfClient_in_client_localTo_xl_Client,
+			 sysOfAlloc_in_client_localTo_xl_Client]) 2);
+auto();
 
-by (simp_tac (simpset()addsimps [lift_prog_correct]) 1);
 
-by (rtac (client_export ) 1);
 
-Client_Progress;
diff -r 95e1de322e82 -r b999c1ab9327 src/HOL/UNITY/Comp.ML
--- a/src/HOL/UNITY/Comp.ML	Wed Oct 27 13:02:23 1999 +0200
+++ b/src/HOL/UNITY/Comp.ML	Wed Oct 27 13:03:32 1999 +0200
@@ -56,6 +56,11 @@
 by (auto_tac (claset(), simpset() addsimps Join_ac@[component_def]));
 qed "Join_absorb2";
 
+Goal "((JOIN I F) <= H) = (ALL i: I. F i <= H)";
+by (simp_tac (simpset() addsimps [component_eq_subset]) 1);
+by (Blast_tac 1);
+qed "JN_component_iff";
+
 Goalw [component_def] "i : I ==> (F i) <= (JN i:I. (F i))";
 by (blast_tac (claset() addIs [JN_absorb]) 1);
 qed "component_JN";
@@ -84,4 +89,19 @@
 	      simpset() addsimps [constrains_def, component_eq_subset]));
 qed "component_constrains";
 
+(*Used in Guar.thy to show that programs are partially ordered*)
 bind_thm ("program_less_le", strict_component_def RS meta_eq_to_obj_eq);
+
+Goal "F' <= F ==> Diff C G (Acts F) <= Diff C G (Acts F')";
+by (auto_tac (claset(), simpset() addsimps [Diff_def, component_eq_subset]));
+qed "Diff_anti_mono";
+
+(*The LocalTo analogue fails unless 
+    reachable (F Join G) <= reachable (F' Join G),
+  e.g. if the initial condition of F is stronger than that of F'*)
+Goalw [LOCALTO_def, stable_def]
+     "[| G : v localTo[C] F';  F' <= F |] ==> G : v localTo[C] F";
+by (auto_tac (claset() addIs [Diff_anti_mono RS component_constrains], 
+	      simpset()));
+qed "localTo_component";
+
diff -r 95e1de322e82 -r b999c1ab9327 src/HOL/UNITY/Extend.ML
--- a/src/HOL/UNITY/Extend.ML	Wed Oct 27 13:02:23 1999 +0200
+++ b/src/HOL/UNITY/Extend.ML	Wed Oct 27 13:03:32 1999 +0200
@@ -123,6 +123,13 @@
 qed "extend_set_inverse";
 Addsimps [extend_set_inverse];
 
+Goalw [extend_set_def, project_set_def]
+     "C <= extend_set h (project_set h C)";
+by (auto_tac (claset(), 
+	      simpset() addsimps [split_extended_all]));
+by (Blast_tac 1);
+qed "extend_set_project_set";
+
 Goal "inj (extend_set h)";
 by (rtac inj_on_inverseI 1);
 by (rtac extend_set_inverse 1);
@@ -454,6 +461,12 @@
 by (simp_tac (simpset() addsimps [Diff_extend_stable]) 1);
 qed "extend_localTo_extend_eq";
 
+Goal "[| F : v localTo[C] H;  C' <= extend_set h C |] \
+\     ==> extend h F : (v o f) localTo[C'] extend h H";
+by (blast_tac (claset() addDs [extend_localTo_extend_eq RS iffD2,
+			       impOfSubs localTo_anti_mono]) 1);
+qed "extend_localTo_extend_I";
+
 (*USED?? opposite inclusion fails*)
 Goal "Restrict C (extend_act h act) <= \
 \     extend_act h (Restrict (project_set h C) act)";
diff -r 95e1de322e82 -r b999c1ab9327 src/HOL/UNITY/Guar.ML
--- a/src/HOL/UNITY/Guar.ML	Wed Oct 27 13:02:23 1999 +0200
+++ b/src/HOL/UNITY/Guar.ML	Wed Oct 27 13:03:32 1999 +0200
@@ -191,11 +191,6 @@
 by (Blast_tac 1);
 qed "guarantees_Join_Un";
 
-Goal "((JOIN I F) <= H) = (ALL i: I. F i <= H)";
-by (simp_tac (simpset() addsimps [component_eq_subset]) 1);
-by (Blast_tac 1);
-qed "JN_component_iff";
-
 Goalw [guar_def]
     "[| ALL i:I. F i : X i guarantees Y i |] \
 \    ==> (JOIN I F) : (INTER I X) guarantees (INTER I Y)";
diff -r 95e1de322e82 -r b999c1ab9327 src/HOL/UNITY/Lift_prog.ML
--- a/src/HOL/UNITY/Lift_prog.ML	Wed Oct 27 13:02:23 1999 +0200
+++ b/src/HOL/UNITY/Lift_prog.ML	Wed Oct 27 13:03:32 1999 +0200
@@ -30,21 +30,8 @@
 
 Addsimps [Int_lift_set, Un_lift_set, Diff_lift_set];
 
-(*Converse fails*)
-Goalw [drop_set_def] "f : A ==> f i : drop_set i A";
-by Auto_tac;
-qed "drop_set_I";
-
 (** lift_act and drop_act **)
 
-Goalw [lift_act_def] "lift_act i Id = Id";
-by Auto_tac;
-by (etac rev_mp 1);
-by (dtac sym 1);
-by (asm_simp_tac (simpset() addsimps [fun_upd_idem_iff]) 1);
-qed "lift_act_Id";
-Addsimps [lift_act_Id];
-
 (*For compatibility with the original definition and perhaps simpler proofs*)
 Goalw [lift_act_def]
     "((f,f') : lift_act i act) = (EX s'. f' = f(i := s') & (f i, s') : act)";
@@ -54,12 +41,6 @@
 qed "lift_act_eq";
 AddIffs [lift_act_eq];
 
-Goalw [drop_set_def, drop_act_def]
-     "UNIV <= drop_set i C ==> drop_act i (Restrict C Id) = Id";
-by (Blast_tac 1);
-qed "drop_act_Id";
-Addsimps [drop_act_Id];
-
 (** lift_prog and drop_prog **)
 
 Goalw [lift_prog_def] "Init (lift_prog i F) = lift_set i (Init F)";
@@ -86,7 +67,10 @@
 
 (*** sub ***)
 
-Addsimps [sub_def];
+Goal "sub i f = f i";
+by (simp_tac (simpset() addsimps [sub_def]) 1);
+qed "sub_apply";
+Addsimps [sub_apply];
 
 Goal "lift_set i {s. P s} = {s. P (sub i s)}";
 by (asm_simp_tac (simpset() addsimps [lift_set_def]) 1);
@@ -338,8 +322,9 @@
 
 Goal "(lift_prog i F : (lift_set i A) Co (lift_set i B))  =  \
 \     (F : A Co B)";
-by (simp_tac (simpset() addsimps [Constrains_def, reachable_lift_prog,
-				  lift_prog_constrains]) 1);
+by (simp_tac
+    (simpset() addsimps [lift_prog_correct, lift_set_correct, 
+			 lift_export extend_Constrains]) 1);
 qed "lift_prog_Constrains";
 
 Goal "(lift_prog i F : Stable (lift_set i A)) = (F : Stable A)";
@@ -453,14 +438,13 @@
 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 H) guarantees Increasing func;  H <= F |]  \
+\     ==> lift_prog i F : (v o sub i) LocalTo (lift_prog i H)  \
 \                         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);
+by (auto_tac (claset(),
+	      simpset() addsimps [lift_prog_correct, o_def]));
 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 95e1de322e82 -r b999c1ab9327 src/HOL/UNITY/Lift_prog.thy
--- a/src/HOL/UNITY/Lift_prog.thy	Wed Oct 27 13:02:23 1999 +0200
+++ b/src/HOL/UNITY/Lift_prog.thy	Wed Oct 27 13:03:32 1999 +0200
@@ -39,7 +39,7 @@
   (*simplifies the expression of specifications*)
   constdefs
     sub :: ['a, 'a=>'b] => 'b
-      "sub i f == f i"
+      "sub == %i f. f i"
 
 
 end
diff -r 95e1de322e82 -r b999c1ab9327 src/HOL/UNITY/PPROD.ML
--- a/src/HOL/UNITY/PPROD.ML	Wed Oct 27 13:02:23 1999 +0200
+++ b/src/HOL/UNITY/PPROD.ML	Wed Oct 27 13:03:32 1999 +0200
@@ -18,13 +18,14 @@
 Goalw [PLam_def] "Init (PLam I F) = (INT i:I. lift_set i (Init (F i)))";
 by Auto_tac;
 qed "Init_PLam";
-Addsimps [Init_PLam];
 
 Goal "Acts (PLam I F) = insert Id (UN i:I. lift_act i `` Acts (F i))";
 by (auto_tac (claset(),
 	      simpset() addsimps [PLam_def]));
 qed "Acts_PLam";
 
+Addsimps [Init_PLam, Acts_PLam];
+
 Goal "PLam {} F = SKIP";
 by (simp_tac (simpset() addsimps [PLam_def]) 1);
 qed "PLam_empty";
@@ -40,6 +41,10 @@
 by Auto_tac;
 qed "PLam_insert";
 
+Goal "((PLam I F) <= H) = (ALL i: I. lift_prog i (F i) <= H)";
+by (simp_tac (simpset() addsimps [PLam_def, JN_component_iff]) 1);
+qed "PLam_component_iff";
+
 Goalw [PLam_def] "i : I ==> lift_prog i (F i) <= (PLam I F)";
 (*blast_tac doesn't use HO unification*)
 by (fast_tac (claset() addIs [component_JN]) 1);
@@ -121,13 +126,20 @@
 qed "const_PLam_invariant";
 
 
+(** localTo **)
+
+Goal "(PLam I F) : (sub i) localTo[C] lift_prog i (F i)";
+by (simp_tac (simpset() addsimps [LOCALTO_def, Diff_def, extend_def, 
+				  stable_def, constrains_def]) 1);
+by (Force_tac 1);
+qed "PLam_sub_localTo";
+
+
 (** Reachability **)
 
 Goal "[| f : reachable (PLam I F);  i : I |] ==> f i : reachable (F i)";
 by (etac reachable.induct 1);
-by (auto_tac
-    (claset() addIs reachable.intrs,
-     simpset() addsimps [Acts_PLam]));
+by (auto_tac (claset() addIs reachable.intrs, simpset()));
 qed "reachable_PLam";
 
 (*Result to justify a re-organization of this file*)
@@ -149,10 +161,10 @@
 (*Init, Init case*)
 by (force_tac (claset() addIs reachable.intrs, simpset()) 1);
 (*Init of F, action of PLam F case*)
-by (rtac reachable.Acts 1);
+by (res_inst_tac [("act","act")] reachable.Acts 1);
 by (Force_tac 1);
 by (assume_tac 1);
-by (force_tac (claset() addIs [ext], simpset() addsimps [Acts_PLam]) 1);
+by (force_tac (claset() addIs [ext], simpset()) 1);
 (*induction over the 2nd "reachable" assumption*)
 by (eres_inst_tac [("xa","f")] reachable.induct 1);
 (*Init of PLam F, action of F case*)
@@ -161,10 +173,10 @@
 by (force_tac (claset() addIs [reachable.Init], simpset()) 1);
 by (force_tac (claset() addIs [ext], simpset() addsimps [lift_act_def]) 1);
 (*last case: an action of PLam I F*)
-by (rtac reachable.Acts 1);
+by (res_inst_tac [("act","acta")] reachable.Acts 1);
 by (Force_tac 1);
 by (assume_tac 1);
-by (force_tac (claset() addIs [ext], simpset() addsimps [Acts_PLam]) 1);
+by (force_tac (claset() addIs [ext], simpset()) 1);
 qed_spec_mp "reachable_lift_Join_PLam";
 
 
diff -r 95e1de322e82 -r b999c1ab9327 src/HOL/UNITY/Project.ML
--- a/src/HOL/UNITY/Project.ML	Wed Oct 27 13:02:23 1999 +0200
+++ b/src/HOL/UNITY/Project.ML	Wed Oct 27 13:03:32 1999 +0200
@@ -402,7 +402,6 @@
 	       simpset() addsimps [project_set_def]) 1);
 qed "reachable_project_imp_reachable";
 
-
 Goal "project_set h (reachable (extend h F Join G)) = \
 \     reachable (F Join project h (reachable (extend h F Join G)) G)";
 by (auto_tac (claset() addDs [subset_refl RS reachable_imp_reachable_project,
@@ -410,6 +409,13 @@
 	      simpset() addsimps [project_set_def]));
 qed "project_set_reachable_extend_eq";
 
+Goal "reachable (extend h F Join G) <= C  \
+\     ==> reachable (extend h F Join G) <= \
+\         extend_set h (reachable (F Join project h C G))";
+by (auto_tac (claset() addDs [reachable_imp_reachable_project], 
+	      simpset()));
+qed "reachable_extend_Join_subset";
+
 (*Perhaps should replace C by reachable...*)
 Goalw [Constrains_def]
      "[| C <= reachable (extend h F Join G);  \
@@ -472,16 +478,14 @@
 				      Collect_eq_extend_set RS sym]) 1);
 qed "project_Increasing";
 
-(**
-Goal "extend h F Join G : (v o f) LocalTo extend h H \
+Goal "[| H <= F;  extend h F Join G : (v o f) LocalTo extend h H |] \
 \     ==> F Join project h (reachable (extend h F Join G)) G : v LocalTo H";
 by (asm_full_simp_tac 
-    (simpset() addsimps [LocalTo_def, project_set_reachable_extend_eq RS sym,
-			 gen_project_localTo_I,
-			 Join_assoc RS sym]) 1);
-
+    (simpset() delsimps [extend_Join]
+	       addsimps [LocalTo_def, project_set_reachable_extend_eq RS sym,
+			 gen_project_localTo_I, extend_Join RS sym, 
+			 Join_assoc RS sym, Join_absorb1]) 1);
 qed "project_LocalTo_I";
-**)
 
 (** A lot of redundant theorems: all are proved to facilitate reasoning
     about guarantees. **)
@@ -510,13 +514,11 @@
 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)";
+     "H <= F ==> 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' \
@@ -625,32 +627,15 @@
 		       simpset()) 1));
 qed_spec_mp "Join_project_ensures";
 
-Goal "[| ALL D. project h C G : transient D --> F : transient D;  \
-\        extend h F Join G : stable C;  \
-\        F Join project h C G : A leadsTo B |] \
-\     ==> extend h F Join G : (C Int extend_set h A) leadsTo (extend_set h B)";
-by (etac leadsTo_induct 1);
-by (asm_simp_tac (simpset() delsimps UN_simps
-		  addsimps [Int_UN_distrib, leadsTo_UN, extend_set_Union]) 3);
-by (blast_tac (claset() addIs [psp_stable RS leadsTo_weaken, 
-			       leadsTo_Trans]) 2);
-by (blast_tac (claset() addIs [leadsTo_Basis, Join_project_ensures]) 1);
-qed "project_leadsTo_lemma";
+(** Lemma useful for both STRONG and WEAK progress*)
 
-(*Instance of the previous theorem for STRONG progress*)
-Goal "[| ALL D. project h UNIV G : transient D --> F : transient D;  \
-\        F Join project h UNIV G : A leadsTo B |] \
-\     ==> extend h F Join G : (extend_set h A) leadsTo (extend_set h B)";
-by (dtac project_leadsTo_lemma 1);
-by Auto_tac;
-qed "project_UNIV_leadsTo_lemma";
-
-(** Towards the analogous theorem for WEAK progress*)
-
+(*The strange induction formula allows induction over the leadsTo
+  assumption's non-atomic precondition*)
 Goal "[| ALL D. project h C G : transient D --> F : transient D;  \
 \        extend h F Join G : stable C;  \
 \        F Join project h C G : (project_set h C Int A) leadsTo B |] \
-\     ==> extend h F Join G : C Int extend_set h (project_set h C Int A) leadsTo (extend_set h B)";
+\     ==> extend h F Join G : \
+\         C Int extend_set h (project_set h C Int A) leadsTo (extend_set h B)";
 by (etac leadsTo_induct 1);
 by (asm_simp_tac (simpset() delsimps UN_simps
 		  addsimps [Int_UN_distrib, leadsTo_UN, extend_set_Union]) 3);
@@ -665,14 +650,14 @@
 \     ==> extend h F Join G : (C Int extend_set h A) leadsTo (extend_set h B)";
 by (rtac (lemma RS leadsTo_weaken) 1);
 by (auto_tac (claset() addIs [project_set_I], simpset()));
-val lemma2 = result();
+qed "project_leadsTo_lemma";
 
 Goal "[| C = (reachable (extend h F Join G)); \
 \        ALL D. project h C G : transient D --> F : transient D;  \
 \        F Join project h C G : A LeadsTo B |] \
 \     ==> extend h F Join G : (extend_set h A) LeadsTo (extend_set h B)";
 by (asm_full_simp_tac 
-    (simpset() addsimps [LeadsTo_def, lemma2, stable_reachable, 
+    (simpset() addsimps [LeadsTo_def, project_leadsTo_lemma, stable_reachable, 
 			 project_set_reachable_extend_eq]) 1);
 qed "Join_project_LeadsTo";
 
@@ -713,14 +698,12 @@
 val [xguary,project,extend] =
 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 UNIV (extend h F) G |] \
+\        !!G. [| F Join proj G h G : Y; extend h F Join G : X' |] \
 \             ==> extend h F Join G : Y' |] \
 \     ==> extend h F : X' guarantees Y'";
 by (rtac (xguary RS guaranteesD RS extend RS guaranteesI) 1);
 by (etac project 1);
 by (assume_tac 1);
-by (assume_tac 1);
 qed "project_guarantees_lemma";
 
 Goal "[| F : X guarantees Y;  \
@@ -761,16 +744,14 @@
 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 H) guarantees Increasing func;  H <= F |]  \
+\     ==> extend h F : (v o f) LocalTo (extend h H)  \
 \                      guarantees Increasing (func o f)";
 by (etac project_guarantees 1);
 by (rtac extending_Increasing 2);
 by (rtac projecting_LocalTo 1);
 by Auto_tac;
 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)";
@@ -808,9 +789,9 @@
 Goal "[| F Join project h UNIV G : A leadsTo B;    \
 \        G : f localTo[UNIV] extend h F |]  \
 \     ==> extend h F Join G : (extend_set h A) leadsTo (extend_set h B)";
-by (rtac project_UNIV_leadsTo_lemma 1);
+by (res_inst_tac [("C1", "UNIV")] (project_leadsTo_lemma RS leadsTo_weaken) 1);
 by (auto_tac (claset(), 
-         simpset() addsimps [impOfSubs (subset_UNIV RS localTo_anti_mono) RS
+         simpset() addsimps [localTo_UNIV_imp_localTo RS
 			     localTo_project_transient_transient]));
 qed "project_leadsTo_D";
 
diff -r 95e1de322e82 -r b999c1ab9327 src/HOL/UNITY/Project.thy
--- a/src/HOL/UNITY/Project.thy	Wed Oct 27 13:02:23 1999 +0200
+++ b/src/HOL/UNITY/Project.thy	Wed Oct 27 13:03:32 1999 +0200
@@ -19,8 +19,7 @@
   extending :: "['c program => 'c set, 'a*'b => 'c, 'a program, 
 		 'c program set, 'c program set, 'a program set] => bool"
   "extending C h F X' Y' Y ==
-     ALL G. F Join project h (C G) G : Y & extend h F Join G : X' &
-            Disjoint UNIV (extend h F) G
+     ALL G. F Join project h (C G) G : Y & extend h F Join G : X'
             --> extend h F Join G : Y'"
 
 end
diff -r 95e1de322e82 -r b999c1ab9327 src/HOL/UNITY/Union.ML
--- a/src/HOL/UNITY/Union.ML	Wed Oct 27 13:02:23 1999 +0200
+++ b/src/HOL/UNITY/Union.ML	Wed Oct 27 13:03:32 1999 +0200
@@ -325,6 +325,9 @@
 by (blast_tac (claset() addIs [Restrict_eq_mono RSN (2,Restrict_imageI)]) 1);
 qed "localTo_anti_mono";
 
+bind_thm ("localTo_UNIV_imp_localTo", 
+	  impOfSubs (subset_UNIV RS 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);
@@ -355,6 +358,15 @@
 			 Diff_self_eq]) 1);
 qed "self_localTo";
 
+Goal "(F Join G : v localTo[C] F) = (G : v localTo[C] F)";
+by (simp_tac (simpset() addsimps [Join_localTo, self_localTo]) 1);
+qed "self_Join_localTo";
+
+Goal "(F Join G : v LocalTo F) = (G : v LocalTo F)";
+by (simp_tac (simpset() addsimps [self_Join_localTo, LocalTo_def,
+				  Join_left_absorb]) 1);
+qed "self_Join_LocalTo";
+
 
 
 (*** Higher-level rules involving localTo and Join ***)
diff -r 95e1de322e82 -r b999c1ab9327 src/HOL/UNITY/Union.thy
--- a/src/HOL/UNITY/Union.thy	Wed Oct 27 13:02:23 1999 +0200
+++ b/src/HOL/UNITY/Union.thy	Wed Oct 27 13:03:32 1999 +0200
@@ -8,6 +8,8 @@
 Partly from Misra's Chapter 5: Asynchronous Compositions of Programs
 
 Do we need a Meet operator?  (Aka Intersection)
+
+CAN PROBABLY DELETE the "Disjoint" predicate
 *)
 
 Union = SubstAx + FP +