# HG changeset patch
# User paulson
# Date 939037648 -7200
# Node ID affe0c2fdfbff141c309e512778b8ef995fc5153
# Parent  d106cad8f51565fd667f0cbe1404b9eb9cc09903
working snapshot (even Alloc)

diff -r d106cad8f515 -r affe0c2fdfbf src/HOL/UNITY/Alloc.ML
--- a/src/HOL/UNITY/Alloc.ML	Mon Oct 04 13:45:31 1999 +0200
+++ b/src/HOL/UNITY/Alloc.ML	Mon Oct 04 13:47:28 1999 +0200
@@ -6,19 +6,11 @@
 Specification of Chandy and Charpentier's Allocator
 
 STOP USING o (COMPOSITION), since function application is naturally associative
+
+guarantees_PLam_I looks wrong: refers to lift_prog
 *)
 
 
-Goal "~ f #2 ==> ~ (!t::nat. (#0 <= t & t <= #10) --> f t)";
-
-(*Useful examples:  singletonI RS subst_elem,  subst_elem RSN (2,IntI) *)
-Goal "[| b:A;  a=b |] ==> a:A";
-by (etac ssubst 1);
-by (assume_tac 1);
-qed "subst_elem";
-
-
-
 Goal "(ALL i: lessThan n. f i <= g i) --> sum f n <= sum g n";
 by (induct_tac "n" 1);
 by Auto_tac;
@@ -65,6 +57,7 @@
 Goalw [good_map_def] "good_map sysOfAlloc";
 by Auto_tac;
 qed "good_map_sysOfAlloc";
+Addsimps [good_map_sysOfAlloc];
 
 (*MUST BE AUTOMATED: even the statement of such results*)
 Goal "!!s. inv sysOfAlloc s = \
@@ -76,7 +69,6 @@
 by (auto_tac (claset() addSWrapper record_split_wrapper, 
 	      simpset() addsimps [sysOfAlloc_def]));
 qed "inv_sysOfAlloc_eq";
-
 Addsimps [inv_sysOfAlloc_eq];
 
 (**SHOULD NOT BE NECESSARY: The various injections into the system
@@ -99,6 +91,7 @@
 Goalw [good_map_def] "good_map sysOfClient";
 by Auto_tac;
 qed "good_map_sysOfClient";
+Addsimps [good_map_sysOfClient];
 
 (*MUST BE AUTOMATED: even the statement of such results*)
 Goal "!!s. inv sysOfClient s = \
@@ -110,6 +103,7 @@
 by (auto_tac (claset() addSWrapper record_split_wrapper, 
 	      simpset() addsimps [sysOfAlloc_def, sysOfClient_def]));
 qed "inv_sysOfClient_eq";
+Addsimps [inv_sysOfClient_eq];
 
 
 Open_locale "System";
@@ -154,7 +148,7 @@
 
 (*CANNOT use bind_thm: it puts the theorem into standard form, in effect
   exporting it from the locale*)
-val Network_Ask = Network_Spec RS IntD1 RS IntD1;
+val Network_Ask = Network_Spec RS IntD1 RS IntD1 RS INT_D;
 val Network_Giv = Network_Spec RS IntD1 RS IntD2 RS INT_D;
 val Network_Rel = Network_Spec RS IntD2 RS INT_D;
 
@@ -189,14 +183,16 @@
 AddIffs [Network_component_System, Alloc_component_System];
 
 
+fun alloc_export th = good_map_sysOfAlloc RS export th;
+
+fun client_export th = good_map_sysOfClient RS export th;
+
 (* F : UNIV guarantees Increasing func
    ==> extend sysOfClient F : UNIV guarantees Increasing (func o client) *)
 val extend_Client_guar_Increasing =
-  good_map_sysOfClient RS export extend_guar_Increasing
+  client_export extend_guar_Increasing
   |> simplify (simpset() addsimps [inv_sysOfClient_eq]);
 
-fun alloc_export th = good_map_sysOfAlloc RS export th;
-
 (*NEED AUTOMATIC PROPAGATION of Alloc_Increasing*)
 Goal "i < Nclients \
 \ ==> extend sysOfAlloc Alloc : UNIV guarantees Increasing (sub i o allocGiv)";
@@ -205,31 +201,27 @@
 qed "extend_Alloc_Increasing_allocGiv";
 
 
-(** Proof of property (1) **)
+(*** Proof of the safety property (1) ***)
 
-(*step 1*)
+(*safety (1), step 1*)
 Goalw [System_def]
      "i < Nclients ==> System : Increasing (rel o sub i o client)";
-by (rtac ([guaranteesI RS disjI2 RS guarantees_Join_I, UNIV_I] 
-	  MRS guaranteesD) 1);
-by (asm_simp_tac 
-    (simpset() addsimps [guarantees_PLam_I, 
-			 extend_Client_guar_Increasing RS guaranteesD,
-			 lift_prog_guar_Increasing]) 1);
+by (rtac (extend_Client_guar_Increasing RS guarantees_Join_I2 
+	  RS guaranteesD) 1);
+by (rtac (lift_prog_guar_Increasing RS guarantees_PLam_I) 1);
+(*gets Client_Increasing_rel from simpset*)
+by Auto_tac;
 qed "System_Increasing_rel";
 
-(*Note: the first step above performs simple quantifier reasoning.  It could
-  be replaced by a proof mentioning no guarantees primitives*)
 
-
-(*step 2*)
+(*safety (1), step 2*)
 Goal "i < Nclients ==> System : Increasing (sub i o allocRel)";
 by (rtac Follows_Increasing1 1);
 by (blast_tac (claset() addIs [Network_Rel RS component_guaranteesD,
 			       System_Increasing_rel]) 1);
 qed "System_Increasing_allocRel";
 
-(*step 2*)
+(*safety (1), step 3*)
 Goal "System : Always {s. sum (%i. (tokens o sub i o allocGiv) s) Nclients \
 \                  <= NbT + sum (%i. (tokens o sub i o allocRel) s) Nclients}";
 by (res_inst_tac 
@@ -250,7 +242,7 @@
      (simpset() addsimps [alloc_export Collect_eq_extend_set RS sym]) 1);
 qed "System_sum_bounded";
 
-(*step 3*)
+(*safety (1), step 4*)
 Goal "System : Always (INT i: lessThan Nclients. \
 \                         {s. (tokens o giv o sub i o client) s \
 \                          <= (tokens o sub i o allocGiv) s})";
@@ -266,6 +258,7 @@
 qed "System_Always_giv_le_allocGiv";
 
 
+(*safety (1), step 5*)
 Goal "System : Always (INT i: lessThan Nclients. \
 \                         {s. (tokens o sub i o allocRel) s \
 \                          <= (tokens o rel o sub i o client) s})";
@@ -281,6 +274,7 @@
 qed "System_Always_allocRel_le_rel";
 
 
+(*safety (1), step 6*)
 Goal "System : Always {s. sum (%i. (tokens o giv o sub i o client)s) Nclients \
 \              <= NbT + sum (%i. (tokens o rel o sub i o client)s) Nclients}";
 by (rtac (Always_Int_rule [System_sum_bounded, System_Always_giv_le_allocGiv, 
@@ -293,3 +287,40 @@
 by Auto_tac;
 qed "System_safety";
 
+
+
+(*** Proof of the progress property (2) ***)
+
+(*we begin with proofs identical to System_Increasing_rel and
+  System_Increasing_allocRel: tactics needed!*)
+
+(*progress (2), step 1*)
+Goalw [System_def]
+     "i < Nclients ==> System : Increasing (ask o sub i o client)";
+by (rtac (extend_Client_guar_Increasing RS guarantees_Join_I2 
+	  RS guaranteesD) 1);
+by (rtac (lift_prog_guar_Increasing RS guarantees_PLam_I) 1);
+by Auto_tac;
+qed "System_Increasing_ask";
+
+(*progress (2), step 2*)
+Goal "i < Nclients ==> System : Increasing (sub i o allocAsk)";
+by (rtac Follows_Increasing1 1);
+by (blast_tac (claset() addIs [Network_Ask RS component_guaranteesD,
+			       System_Increasing_ask]) 1);
+qed "System_Increasing_allocAsk";
+
+(*progress (2), step 3*)
+(*All this trouble just to lift "Client_Bounded" through two extemd ops*)
+Goalw [System_def]
+     "i < Nclients \
+\   ==> System : Always \
+\                 {s. ALL elt : set ((ask o sub i o client) s). elt <= NbT}";
+by (rtac (lift_prog_guar_Always RS 
+	  guarantees_PLam_I RS client_export extend_guar_Always RS
+	  guarantees_Join_I2 RS guaranteesD RS Always_weaken) 1);
+by (stac Always_UNIV_eq 1 THEN rtac Client_Bounded 1);
+by (auto_tac(claset(),
+	 simpset() addsimps [Collect_eq_lift_set RS sym,
+			     client_export Collect_eq_extend_set RS sym]));
+qed "System_Bounded";
diff -r d106cad8f515 -r affe0c2fdfbf src/HOL/UNITY/Constrains.ML
--- a/src/HOL/UNITY/Constrains.ML	Mon Oct 04 13:45:31 1999 +0200
+++ b/src/HOL/UNITY/Constrains.ML	Mon Oct 04 13:47:28 1999 +0200
@@ -282,6 +282,11 @@
 				  Always_eq_invariant_reachable]));
 qed "Always_eq_includes_reachable";
 
+Goal "Always UNIV = UNIV";
+by (auto_tac (claset(),
+	      simpset() addsimps [Always_eq_includes_reachable]));
+qed "Always_UNIV_eq";
+Addsimps [Always_UNIV_eq];
 
 Goal "Always A = (UN I: Pow A. invariant I)";
 by (simp_tac (simpset() addsimps [Always_eq_includes_reachable]) 1);
diff -r d106cad8f515 -r affe0c2fdfbf src/HOL/UNITY/Extend.ML
--- a/src/HOL/UNITY/Extend.ML	Mon Oct 04 13:45:31 1999 +0200
+++ b/src/HOL/UNITY/Extend.ML	Mon Oct 04 13:47:28 1999 +0200
@@ -95,6 +95,13 @@
 by (rtac extend_set_inverse 1);
 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;
+qed "extend_set_UNIV_eq";
+Addsimps [standard extend_set_UNIV_eq];
+
 (*** project_set: basic properties ***)
 
 (*project_set is simply image!*)
@@ -164,7 +171,7 @@
 
 (*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]
+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);
 qed "extend_act_inverse";
@@ -206,8 +213,7 @@
 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 C h Id = Id";
 by (Force_tac 1);
 qed "project_act_Id";
 
@@ -290,6 +296,21 @@
 qed "extend_JN";
 Addsimps [extend_JN];
 
+
+(** These monotonicity results look natural but are UNUSED **)
+
+Goal "F <= G ==> extend h F <= extend h G";
+by (full_simp_tac (simpset() addsimps [component_eq_subset]) 1);
+by Auto_tac;
+qed "extend_mono";
+
+Goal "F <= G ==> project C h F <= project C h G";
+by (full_simp_tac
+    (simpset() addsimps [component_eq_subset, project_set_def]) 1);
+by Auto_tac;
+qed "project_mono";
+
+
 (*** Safety: co, stable ***)
 
 Goal "(extend h F : (extend_set h A) co (extend_set h B)) = \
diff -r d106cad8f515 -r affe0c2fdfbf src/HOL/UNITY/Guar.ML
--- a/src/HOL/UNITY/Guar.ML	Mon Oct 04 13:45:31 1999 +0200
+++ b/src/HOL/UNITY/Guar.ML	Mon Oct 04 13:47:28 1999 +0200
@@ -219,6 +219,9 @@
 by (Blast_tac 1);
 qed "guarantees_Join_I";
 
+bind_thm ("guarantees_Join_I1", disjI1 RS guarantees_Join_I);
+bind_thm ("guarantees_Join_I2", disjI2 RS guarantees_Join_I);
+
 Goalw [guar_def]
      "[| i : I;  F i: X guarantees Y |] ==> (JN i:I. (F i)) : X guarantees Y";
 by (simp_tac (simpset() addsimps [JN_component_iff]) 1);
diff -r d106cad8f515 -r affe0c2fdfbf src/HOL/UNITY/PPROD.ML
--- a/src/HOL/UNITY/PPROD.ML	Mon Oct 04 13:45:31 1999 +0200
+++ b/src/HOL/UNITY/PPROD.ML	Mon Oct 04 13:47:28 1999 +0200
@@ -271,21 +271,7 @@
 (*** guarantees properties ***)
 
 Goalw [PLam_def]
-    "[| i : I;  lift_prog i (F i): X guarantees Y |]  \
+    "[| lift_prog i (F i): X guarantees Y;  i : I |]  \
 \    ==> (PLam I F) : X guarantees Y";
 by (asm_simp_tac (simpset() addsimps [guarantees_JN_I]) 1);
 qed "guarantees_PLam_I";
-
-Goalw [PLam_def]
-    "[| ALL i:I. F i : X guarantees Y |] \
-\    ==> (PLam I F) : (INT i: I. lift_prog i `` X) \
-\                 guarantees (INT i: I. lift_prog i `` Y)";
-by (blast_tac (claset() addIs [guarantees_JN_INT, lift_prog_guarantees]) 1);
-bind_thm ("guarantees_PLam_INT", ballI RS result());
-
-Goalw [PLam_def]
-    "[| ALL i:I. F i : X guarantees Y |] \
-\    ==> (PLam I F) : (UN i: I. lift_prog i `` X) \
-\                 guarantees (UN i: I. lift_prog i `` Y)";
-by (blast_tac (claset() addIs [guarantees_JN_UN, lift_prog_guarantees]) 1);
-bind_thm ("guarantees_PLam_UN", ballI RS result());
diff -r d106cad8f515 -r affe0c2fdfbf src/HOL/UNITY/Project.ML
--- a/src/HOL/UNITY/Project.ML	Mon Oct 04 13:45:31 1999 +0200
+++ b/src/HOL/UNITY/Project.ML	Mon Oct 04 13:47:28 1999 +0200
@@ -18,7 +18,7 @@
 
 Goal "[| D <= C; project C h F : A co B |] ==> project D h F : A co B";
 by (auto_tac (claset(), simpset() addsimps [constrains_def]));
-bd project_act_mono 1;
+by (dtac project_act_mono 1);
 by (Blast_tac 1);
 qed "project_constrains_mono";
 
@@ -65,7 +65,7 @@
 qed "project_stable";
 
 Goal "F : stable (extend_set h A) ==> project C h F : stable A";
-bd (project_stable RS iffD2) 1;
+by (dtac (project_stable RS iffD2) 1);
 by (blast_tac (claset() addIs [project_stable_mono]) 1);
 qed "project_stable_I";
 
@@ -106,6 +106,16 @@
 				  extend_stable RS iffD1]));
 qed "Join_project_increasing";
 
+(*For using project_guarantees in particular cases*)
+Goal "extend h F Join G : extend_set h A co extend_set h B \
+\     ==> F Join project UNIV h G : A co B";
+by (stac (project_set_UNIV RS project_extend_Join RS sym) 1);
+by (asm_full_simp_tac
+    (simpset() addsimps [project_constrains, Join_constrains, 
+			 extend_constrains]) 1);
+by (fast_tac (claset() addDs [constrains_imp_subset]) 1);
+qed "project_constrains_I";
+
 
 (*** Diff, needed for localTo ***)
 
@@ -140,13 +150,20 @@
 qed "Diff_project_stable";
 
 (*Converse appears to fail*)
-Goal "[| UNIV <= project_set h C;  (H : (func o f) localTo extend h G) |] \
-\     ==> (project C h H : func localTo G)";
+Goal "[| UNIV <= project_set h C;  H : (func o f) localTo extend h G |] \
+\     ==> project C h H : func localTo G";
 by (asm_full_simp_tac 
     (simpset() addsimps [localTo_def, 
 			 project_extend_Join RS sym,
 			 subset_UNIV RS subset_trans RS 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);
 qed "project_localTo_I";
 
 
@@ -166,6 +183,8 @@
 by (etac extend_act_D 1);
 qed "reachable_imp_reachable_project";
 
+(*The extra generality in the first premise allows guarantees with STRONG
+  preconditions (localTo) and WEAK postconditions.*)
 Goalw [Constrains_def]
      "[| reachable (extend h F Join G) <= C;    \
 \        F Join project C h G : A Co B |] \
@@ -188,7 +207,7 @@
 \        F Join project C h G : Always A |]   \
 \     ==> extend h F Join G : Always (extend_set h A)";
 by (force_tac (claset() addIs [reachable.Init, project_set_I],
-	       simpset() addsimps [project_Stable_D]) 1);
+               simpset() addsimps [project_Stable_D]) 1);
 qed "project_Always_D";
 
 Goalw [Increasing_def]
@@ -250,6 +269,15 @@
 by (asm_simp_tac (simpset() addsimps [project_Constrains_I]) 1);
 qed "project_Stable_I";
 
+Goalw [Always_def]
+     "[| C <= reachable (extend h F Join G);  \
+\        extend h F Join G : Always (extend_set h A) |]   \
+\     ==> F Join project C h G : Always A";
+by (auto_tac (claset(), simpset() addsimps [project_Stable_I]));
+bws [project_set_def, extend_set_def];
+by (Blast_tac 1);
+qed "project_Always_I";
+
 Goalw [Increasing_def]
      "[| C <= reachable (extend h F Join G);  \
 \        extend h F Join G : Increasing (func o f) |] \
@@ -369,15 +397,15 @@
 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 "Join_project_leadsTo_I";
+qed "project_leadsTo_lemma";
 
 (*Instance of the previous theorem for STRONG progress*)
 Goal "[| ALL x. project UNIV h G ~: transient {x};  \
 \        F Join project UNIV h G : A leadsTo B |] \
 \     ==> extend h F Join G : (extend_set h A) leadsTo (extend_set h B)";
-by (dtac Join_project_leadsTo_I 1);
+by (dtac project_leadsTo_lemma 1);
 by Auto_tac;
-qed "Join_project_UNIV_leadsTo_I";
+qed "project_UNIV_leadsTo_lemma";
 
 (** Towards the analogous theorem for WEAK progress*)
 
@@ -397,7 +425,7 @@
 \        extend h F Join G : stable C;  \
 \        F Join project C h G : (project_set h C Int A) leadsTo B |] \
 \     ==> extend h F Join G : (C Int extend_set h A) leadsTo (extend_set h B)";
-br (lemma RS leadsTo_weaken) 1;
+by (rtac (lemma RS leadsTo_weaken) 1);
 by (auto_tac (claset() addIs [project_set_I], simpset()));
 val lemma2 = result();
 
@@ -475,31 +503,31 @@
 by Auto_tac;
 qed "extend_guar_Increasing";
 
-Goal "F : (func localTo G) guarantees increasing func  \
-\     ==> extend h F : (func 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);
 (*the "increasing" guarantee*)
-by (asm_simp_tac
-    (simpset() addsimps [Join_project_increasing RS sym]) 2);
-(*the "localTo" requirement*)
-by (stac (project_set_UNIV RS project_extend_Join RS sym) 1);
-by (asm_simp_tac 
-    (simpset() addsimps [project_set_UNIV RS project_localTo_I]) 1);
+by (asm_simp_tac (simpset() addsimps [Join_project_increasing RS sym]) 2);
+by (etac project_localTo_I 1);
 qed "extend_localTo_guar_increasing";
 
-Goal "F : (func localTo G) guarantees Increasing func  \
-\     ==> extend h F : (func 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);
 (*the "Increasing" guarantee*)
 by (etac (subset_UNIV RS project_Increasing_D) 2);
-(*the "localTo" requirement*)
-by (stac (project_set_UNIV RS project_extend_Join RS sym) 1);
-by (asm_simp_tac 
-    (simpset() addsimps [project_set_UNIV RS project_localTo_I]) 1);
+by (etac project_localTo_I 1);
 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)";
+by (etac project_guarantees 1);
+by (etac (subset_refl RS project_Always_D) 2);
+by (etac (subset_refl RS project_Always_I) 1);
+qed "extend_guar_Always";
+
 
 (** Guarantees with a leadsTo postcondition **)
 
@@ -510,13 +538,38 @@
 			 extend_set_sing, project_stable_I]) 1);
 qed "localTo_imp_project_stable";
 
-
 Goal "F : stable{s} ==> F ~: transient {s}";
 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;    \
+\        extend h F Join G : f localTo extend h F; \
+\        Disjoint (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 Auto_tac;
+by (asm_full_simp_tac
+    (simpset() addsimps [Join_localTo, self_localTo,
+			 localTo_imp_project_stable, 
+			 stable_sing_imp_not_transient]) 1);
+qed "project_leadsTo_D";
+
+
+Goal "[| F Join project (reachable (extend h F Join G)) h G : A LeadsTo B; \
+\         extend h F Join G : f localTo extend h F; \
+\         Disjoint (extend h F) G  |]  \
+\      ==> extend h F Join G : (extend_set h A) LeadsTo (extend_set h B)";
+by (rtac Join_project_LeadsTo 1);
+by Auto_tac;
+by (asm_full_simp_tac
+    (simpset() addsimps [Join_localTo, self_localTo,
+			 localTo_imp_project_stable, 
+			 stable_sing_imp_not_transient]) 1);
+qed "project_LeadsTo_D";
+
+
 (*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'))  \
@@ -524,18 +577,9 @@
 \                  guarantees ((extend_set h B) leadsTo (extend_set h B'))";
 by (etac project_guarantees 1);
 (*the safety precondition*)
-by (stac (project_set_UNIV RS project_extend_Join RS sym) 1);
-by (asm_full_simp_tac
-    (simpset() addsimps [project_constrains, Join_constrains, 
-			 extend_constrains]) 1);
-by (fast_tac (claset() addDs [constrains_imp_subset]) 1);
+by (fast_tac (claset() addIs [project_constrains_I]) 1);
 (*the liveness postcondition*)
-by (rtac Join_project_UNIV_leadsTo_I 1);
-by Auto_tac;
-by (asm_full_simp_tac
-    (simpset() addsimps [Join_localTo, self_localTo,
-			 localTo_imp_project_stable, 
-			 stable_sing_imp_not_transient]) 1);
+by (fast_tac (claset() addIs [project_leadsTo_D]) 1);
 qed "extend_co_guar_leadsTo";
 
 (*WEAK precondition and postcondition*)
@@ -547,13 +591,7 @@
 (*the safety precondition*)
 by (fast_tac (claset() addIs [project_Constrains_I]) 1);
 (*the liveness postcondition*)
-by (rtac Join_project_LeadsTo 1);
-by Auto_tac;
-by (asm_full_simp_tac
-    (simpset() addsimps [Join_localTo, self_localTo,
-			 localTo_imp_project_stable, 
-			 stable_sing_imp_not_transient]) 1);
+by (fast_tac (claset() addIs [project_LeadsTo_D]) 1);
 qed "extend_Co_guar_LeadsTo";
 
-
 Close_locale "Extend";
diff -r d106cad8f515 -r affe0c2fdfbf src/HOL/UNITY/Project.thy
--- a/src/HOL/UNITY/Project.thy	Mon Oct 04 13:45:31 1999 +0200
+++ b/src/HOL/UNITY/Project.thy	Mon Oct 04 13:47:28 1999 +0200
@@ -8,15 +8,4 @@
 Inheritance of GUARANTEES properties under extension
 *)
 
-Project = Extend +
-
-
-constdefs
-
-  restr_act :: "['c set, 'a*'b => 'c, ('a*'a) set] => ('a*'a) set"
-    "restr_act C h act == project_act C h (extend_act h act)"
-
-  restr :: "['c set, 'a*'b => 'c, 'a program] => 'a program"
-    "restr C h F == project C h (extend h F)"
-
-end
+Project = Extend
diff -r d106cad8f515 -r affe0c2fdfbf src/HOL/UNITY/Union.ML
--- a/src/HOL/UNITY/Union.ML	Mon Oct 04 13:45:31 1999 +0200
+++ b/src/HOL/UNITY/Union.ML	Mon Oct 04 13:47:28 1999 +0200
@@ -329,6 +329,11 @@
 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";
+by (Blast_tac 1);
+qed "triv_localTo_eq_UNIV";
+
 Goal "(F Join G : v localTo H) = (F : v localTo H  &  G : v localTo H)";
 by (asm_full_simp_tac 
     (simpset() addsimps [localTo_def, Diff_Join_distrib,