# HG changeset patch
# User paulson
# Date 945784982 -3600
# Node ID 19b9f92ca503f522e508ebfd071bcf6b0c5b4a89
# Parent  72d783f7313ab7d950b2093b3770da8b4733690d
working with weak LeadsTo in guarantees precondition\!

diff -r 72d783f7313a -r 19b9f92ca503 src/HOL/UNITY/Alloc.ML
--- a/src/HOL/UNITY/Alloc.ML	Tue Dec 21 11:27:32 1999 +0100
+++ b/src/HOL/UNITY/Alloc.ML	Tue Dec 21 15:03:02 1999 +0100
@@ -28,8 +28,8 @@
                      handle THM _ => (list_of_Int (th RS INT_D))
                      handle THM _ => [th];
 
+(*useful??*)
 val lessThanBspec = lessThan_iff RS iffD2 RSN (2, bspec);
-
 fun normalize th = 
      normalize (th RS spec
 		handle THM _ => th RS lessThanBspec
@@ -223,8 +223,7 @@
 		  alloc_progress_def, alloc_preserves_def] Alloc;
 
 val [Alloc_Increasing, Alloc_Safety, 
-     Alloc_Progress, Alloc_preserves] = 
-    map normalize (list_of_Int Alloc_Spec);
+     Alloc_Progress, Alloc_preserves] = list_of_Int Alloc_Spec;
 
 
 fun alloc_export th = good_map_sysOfAlloc RS export th |> simplify (simpset());
@@ -283,14 +282,21 @@
 AddIffs [extend_sysOfClient_preserves_o_client];
 
 
-(*NEED AUTOMATIC PROPAGATION of Alloc_Increasing*)
+(*NEED AUTOMATIC PROPAGATION of Alloc_Increasing
+  (the form changes slightly, though, removing the INT) *)
 Goal "i < Nclients \
 \     ==> extend sysOfAlloc Alloc : \
 \           UNIV guarantees[allocGiv] Increasing (sub i o allocGiv)";
-by (dtac (Alloc_Increasing RS alloc_export extend_guar_Increasing) 1);
-by (auto_tac (claset(), simpset() addsimps [o_def]));
+(* Alternative is something like
+by (dtac (Alloc_Increasing RS (guarantees_INT_right_iff RS iffD1)
+          RS lessThanBspec RS alloc_export extend_guar_Increasing) 1);
+*)
+by (cut_facts_tac [Alloc_Increasing] 1);
+by (auto_tac (claset() addSDs [alloc_export extend_guar_Increasing], 
+	      simpset() addsimps [guarantees_INT_right_iff, o_def]));
 qed "extend_Alloc_Increasing_allocGiv";
 
+
 Goalw [System_def]
      "i < Nclients ==> System : Increasing (sub i o allocGiv)";
 by (rtac (extend_Alloc_Increasing_allocGiv RS 
@@ -393,25 +399,31 @@
 by (etac (System_Follows_rel RS Follows_Increasing1) 1);
 qed "System_Increasing_allocRel";
 
+(*NEED AUTOMATIC PROPAGATION of Alloc_Safety.  The text is identical.*)
+Goal "extend sysOfAlloc Alloc :  \
+\  (INT i : lessThan Nclients. Increasing (sub i o allocRel))  \
+\  guarantees[allocGiv]  \
+\    Always {s. sum (%i. (tokens o sub i o allocGiv) s) Nclients  \
+\               <= NbT + sum (%i. (tokens o sub i o allocRel) s) Nclients}";
+by (rtac (Alloc_Safety RS alloc_export project_guarantees) 1);
+(*2: Always postcondition*)
+by (rtac ((alloc_export extending_Always RS extending_weaken)) 2);
+(*1: Increasing precondition*)
+by (rtac (alloc_export projecting_Increasing RS projecting_weaken RS 
+	  projecting_INT) 1);
+by (auto_tac (claset(),
+	      simpset() addsimps [alloc_export Collect_eq_extend_set RS sym,
+				  o_def]));
+qed "extend_Alloc_Safety";
+
 (*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 
-    [("X", "(INT i : lessThan Nclients. Increasing (sub i o allocRel))")] 
-    component_guaranteesD 1);
-by (rtac Alloc_component_System 3);
-by (force_tac (claset(), simpset() addsimps [System_Increasing_allocRel]) 2);
-by (rtac (Alloc_Safety RS alloc_export project_guarantees) 1);
-(*1: Increasing precondition*)
-by (rtac (alloc_export projecting_Increasing RS projecting_weaken RS 
-	  projecting_INT) 1);
-by Auto_tac;
-by (asm_full_simp_tac (simpset() addsimps [o_def]) 1);
-(*2: Always postcondition*)
-by (rtac ((alloc_export extending_Always RS extending_weaken)) 1);
-by (auto_tac (claset(),
-	      simpset() addsimps [alloc_export Collect_eq_extend_set RS sym,
-				  o_def]));
+by (rtac (extend_Alloc_Safety RS component_guaranteesD) 1);
+by (rtac Alloc_component_System 2);
+(*preserves*)
+by (asm_full_simp_tac (simpset() addsimps [o_def]) 2);
+by (force_tac (claset(), simpset() addsimps [System_Increasing_allocRel]) 1);
 qed "System_sum_bounded";
 
 (** Follows reasoning **)
@@ -545,7 +557,8 @@
 by (rtac (client_export extending_LeadsETo RS extending_weaken RS 
 	  extending_INT) 1);
 by (auto_tac (claset(), 
-  simpset() addsimps [o_apply, client_export Collect_eq_extend_set RS sym]));
+	      simpset() addsimps [o_apply, 
+				client_export Collect_eq_extend_set RS sym]));
 qed "System_Client_Progress";
 
 val lemma =
@@ -586,6 +599,57 @@
 by (rtac (impOfSubs LeadsETo_subset_LeadsTo) 2);
 by (cut_facts_tac [System_Client_Progress] 2);
 by (Force_tac 2);
-by (simp_tac (simpset() addsimps [Collect_conj_eq]) 1); 
 by (etac lemma3 1);
 qed "System_Alloc_Progress";
+
+
+xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx;
+
+(*NEED AUTOMATIC PROPAGATION of Alloc_Progress.  The text is identical.*)
+Goal "extend sysOfAlloc Alloc :  \
+\  (INT i : lessThan Nclients. Increasing (sub i o allocAsk) Int   \
+\                              Increasing (sub i o allocRel))   \
+\  Int   \
+\  Always {s. ALL i : lessThan Nclients.   \
+\             ALL k : lessThan (length (allocAsk s i)).   \
+\             allocAsk s i ! k <= NbT}   \
+\  Int   \
+\  (INT i : lessThan Nclients.    \
+\   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]   \
+\      (INT i : lessThan Nclients.   \
+\       INT h. {s. h <= (sub i o allocAsk) s}    \
+ \             LeadsTo[givenBy allocGiv]   \
+\              {s. h pfixLe (sub i o allocGiv) s})";
+by (rtac (Alloc_Progress RS alloc_export project_guarantees) 1);
+(*preserves*)
+by (simp_tac (simpset() addsimps [o_def]) 3);
+(*2: LeadsTo postcondition*)
+by (rtac (extending_INT RS extending_INT) 2);
+by (rtac ((alloc_export extending_LeadsETo RS extending_weaken)) 2);
+by (rtac subset_refl 3);
+by (simp_tac (simpset() addsimps [o_def]) 3);
+by (simp_tac (simpset() addsimps [alloc_export Collect_eq_extend_set RS sym,
+				  o_def]) 2);
+(*1: Increasing precondition*)
+by (rtac (alloc_export projecting_Increasing RS projecting_weaken RS 
+	  projecting_INT) 1);
+by (auto_tac (claset(),
+	      simpset() addsimps [alloc_export Collect_eq_extend_set RS sym,
+				  o_def]));
+qed "extend_Alloc_Progress";
+
+
+(*progress (2), step 9*)
+Goal
+ "System : (INT i : lessThan Nclients. \
+\           INT h. {s. h <= (sub i o allocAsk) s}  \
+\                  LeadsTo {s. h pfixLe (sub i o allocGiv) s})";
+by (res_inst_tac 
+    [("X", "(INT i : lessThan Nclients. Increasing (sub i o allocRel))")] 
+    component_guaranteesD 1);
+by (rtac Alloc_component_System 3);
+by (force_tac (claset(), simpset() addsimps [System_Increasing_allocRel]) 2);
+by (rtac (Alloc_Safety RS alloc_export project_guarantees) 1);
+
diff -r 72d783f7313a -r 19b9f92ca503 src/HOL/UNITY/Alloc.thy
--- a/src/HOL/UNITY/Alloc.thy	Tue Dec 21 11:27:32 1999 +0100
+++ b/src/HOL/UNITY/Alloc.thy	Tue Dec 21 15:03:02 1999 +0100
@@ -131,7 +131,8 @@
 		  LeadsTo {s. tokens h <= (tokens o sub i o allocRel)s})
          guarantees[allocGiv]
 	     (INT i : lessThan Nclients.
-	      INT h. {s. h <= (sub i o allocAsk) s} LeadsTo
+	      INT h. {s. h <= (sub i o allocAsk) s}
+	             LeadsTo[givenBy allocGiv]
 	             {s. h pfixLe (sub i o allocGiv) s})"
 
   (*spec: preserves part*)
diff -r 72d783f7313a -r 19b9f92ca503 src/HOL/UNITY/Constrains.ML
--- a/src/HOL/UNITY/Constrains.ML	Tue Dec 21 11:27:32 1999 +0100
+++ b/src/HOL/UNITY/Constrains.ML	Tue Dec 21 15:03:02 1999 +0100
@@ -24,11 +24,13 @@
 by (blast_tac (claset() addIs [stableI, constrainsI] @ reachable.intrs) 1);
 qed "stable_reachable";
 
+AddSIs [stable_reachable];
+Addsimps [stable_reachable];
 
 (*The set of all reachable states is an invariant...*)
 Goal "F : invariant (reachable F)";
 by (simp_tac (simpset() addsimps [invariant_def]) 1);
-by (blast_tac (claset() addIs (stable_reachable::reachable.intrs)) 1);
+by (blast_tac (claset() addIs reachable.intrs) 1);
 qed "invariant_reachable";
 
 (*...in fact the strongest invariant!*)
@@ -194,7 +196,7 @@
 qed "ball_Stable_INT";
 
 Goal "F : Stable (reachable F)";
-by (simp_tac (simpset() addsimps [Stable_eq_stable, stable_reachable]) 1);
+by (simp_tac (simpset() addsimps [Stable_eq_stable]) 1);
 qed "Stable_reachable";
 
 
@@ -291,7 +293,6 @@
 Goal "Always A = (UN I: Pow A. invariant I)";
 by (simp_tac (simpset() addsimps [Always_eq_includes_reachable]) 1);
 by (blast_tac (claset() addIs [invariantI, impOfSubs Init_subset_reachable, 
-                               stable_reachable,
 			       impOfSubs invariant_includes_reachable]) 1);
 qed "Always_eq_UN_invariant";
 
diff -r 72d783f7313a -r 19b9f92ca503 src/HOL/UNITY/ELT.ML
--- a/src/HOL/UNITY/ELT.ML	Tue Dec 21 11:27:32 1999 +0100
+++ b/src/HOL/UNITY/ELT.ML	Tue Dec 21 15:03:02 1999 +0100
@@ -26,7 +26,7 @@
 qed "givenBy_eq_Collect";
 
 val prems =
-Goal "(!!x y. [|  x:A;  v x = v y |] ==> y: A) ==> A: givenBy v";
+Goal "(!!x y. [| x:A;  v x = v y |] ==> y: A) ==> A: givenBy v";
 by (stac givenBy_eq_all 1);
 by (blast_tac (claset() addIs prems) 1);
 qed "givenByI";
@@ -63,6 +63,11 @@
 				   givenBy_eq_Collect]) 1);
 qed "preserves_givenBy_imp_stable";
 
+Goal "givenBy (w o v) <= givenBy v";
+by (simp_tac (simpset() addsimps [givenBy_eq_Collect]) 1);
+by (Deepen_tac 0 1);
+qed "givenBy_o_subset";
+
 
 (** Standard leadsTo rules **)
 
@@ -380,7 +385,7 @@
 (*Postcondition can be strengthened to (reachable F Int B) *)
 Goal "F : A ensures B ==> F : (reachable F Int A) ensures B";
 by (rtac (stable_ensures_Int RS ensures_weaken_R) 1);
-by (auto_tac (claset(), simpset() addsimps [stable_reachable]));
+by Auto_tac;
 qed "reachable_ensures";
 
 Goal "F : A leadsTo B ==> F : (reachable F Int A) leadsTo[Pow(reachable F)] B";
@@ -388,8 +393,7 @@
 by (stac Int_Union 3);
 by (blast_tac (claset() addIs [leadsETo_UN]) 3);
 by (blast_tac (claset() addDs [e_psp_stable2] 
-                        addIs [leadsETo_Trans, stable_reachable, 
-			       leadsETo_weaken_L]) 2);
+                        addIs [leadsETo_Trans, leadsETo_weaken_L]) 2);
 by (blast_tac (claset() addIs [reachable_ensures, leadsETo_Basis]) 1);
 val lemma = result();
 
@@ -406,11 +410,15 @@
 
 Open_locale "Extend";
 
-(*Here h and f are locale constants*)
-Goal "extend_set h `` (givenBy v) <= (givenBy (v o f))";
-by (simp_tac (simpset() addsimps [givenBy_eq_all]) 1);
-by (Blast_tac 1);
-qed "extend_set_givenBy_subset";
+Goal "givenBy (v o f) = extend_set h `` (givenBy v)";
+by (simp_tac (simpset() addsimps [givenBy_eq_Collect]) 1);
+by (Deepen_tac 0 1);
+qed "givenBy_o_eq_extend_set";
+
+Goal "givenBy f = range (extend_set h)";
+by (simp_tac (simpset() addsimps [givenBy_eq_Collect]) 1);
+by (Deepen_tac 0 1);
+qed "givenBy_eq_extend_set";
 
 Goal "D : givenBy v ==> extend_set h D : givenBy (v o f)";
 by (full_simp_tac (simpset() addsimps [givenBy_eq_all]) 1);
@@ -428,20 +436,19 @@
 				      extend_set_Diff_distrib RS sym]) 1);
 qed "leadsETo_imp_extend_leadsETo";
 
-(*NEEDED?? THEN MOVE TO EXTEND.ML??*)
+(*MOVE to Extend.ML?*)
 Goal "A Int extend_set h ((project_set h A) Int B) = A Int extend_set h B";
-by (auto_tac (claset() addIs [project_set_I], 
-	      simpset()));
+by (auto_tac (claset(), simpset() addsimps [split_extended_all]));
 qed "Int_extend_set_lemma";
 
-(*NEEDED?? THEN MOVE TO EXTEND.ML??*)
+(*MOVE to extend.ML??*)
 Goal "G : C co B ==> project h C G : project_set h C co project_set h B";
 by (full_simp_tac (simpset() addsimps [constrains_def, project_def, 
-				       project_act_def, project_set_def]) 1);
+				       project_act_def]) 1);
 by (Blast_tac 1);
 qed "project_constrains_project_set";
 
-(*NEEDED?? THEN MOVE TO EXTEND.ML??*)
+(*MOVE to extend.ML??*)
 Goal "G : stable C ==> project h C G : stable (project_set h C)";
 by (asm_full_simp_tac (simpset() addsimps [stable_def, 
 					   project_constrains_project_set]) 1);
@@ -518,18 +525,19 @@
 \     ==> extend h F Join G : (C Int extend_set h A) \
 \           leadsTo[(%D. C Int extend_set h D)``givenBy v] (extend_set h B)";
 by (rtac (lemma RS leadsETo_weaken) 1);
-by (auto_tac (claset() addIs [project_set_I], simpset()));
-qed "project_leadsETo_lemma";
+by (auto_tac (claset(), 
+	      simpset() addsimps [split_extended_all]));
+qed "project_leadsETo_D_lemma";
 
 Goal "[| F Join project h UNIV G : A leadsTo[givenBy v] B;  \
 \        G : preserves (v o f) |]  \
 \     ==> extend h F Join G : (extend_set h A) \
 \           leadsTo[givenBy (v o f)] (extend_set h B)";
-by (rtac (make_elim project_leadsETo_lemma) 1);
+by (rtac (make_elim project_leadsETo_D_lemma) 1);
 by (stac stable_UNIV 1);
 by Auto_tac;
 by (etac leadsETo_givenBy 1);
-by (rtac extend_set_givenBy_subset 1);
+by (rtac (givenBy_o_eq_extend_set RS equalityD2) 1);
 qed "project_leadsETo_D";
 
 Goal "[| F Join project h (reachable (extend h F Join G)) G \
@@ -538,7 +546,7 @@
 \     ==> extend h F Join G : \
 \           (extend_set h A) LeadsTo[givenBy (v o f)] (extend_set h B)";
 by (rtac (make_elim (subset_refl RS stable_reachable RS 
-		     project_leadsETo_lemma)) 1);
+		     project_leadsETo_D_lemma)) 1);
 by (auto_tac (claset(), 
 	      simpset() addsimps [LeadsETo_def]));
 by (asm_full_simp_tac 
@@ -563,6 +571,133 @@
 qed "extending_LeadsETo";
 
 
+(*** leadsETo in the precondition ***)
+
+Goalw [transient_def]
+     "[| G : transient (C Int extend_set h A);  G : stable C |]  \
+\     ==> project h C G : transient (project_set h C Int A)";
+by (auto_tac (claset(), simpset() addsimps [Domain_project_act]));
+by (subgoal_tac "act ^^ (C Int extend_set h A) <= - extend_set h A" 1);
+by (asm_full_simp_tac 
+    (simpset() addsimps [stable_def, constrains_def]) 2);
+by (Blast_tac 2);
+(*back to main goal*)
+by (thin_tac "?AA <= -C Un ?BB" 1);
+by (ball_tac 1);
+by (asm_full_simp_tac 
+    (simpset() addsimps [extend_set_def, project_act_def]) 1);
+by (Blast_tac 1);
+qed "transient_extend_set_imp_project_transient";
+
+(*converse might hold too?*)
+Goalw [transient_def]
+     "project h C (extend h F) : transient (project_set h C Int D) \
+\     ==> F : transient (project_set h C Int D)";
+by (auto_tac (claset(), simpset() addsimps [Domain_project_act]));
+by (rtac bexI 1);
+by (assume_tac 2);
+by Auto_tac;
+by (rewtac extend_act_def);
+by (Blast_tac 1);
+qed "project_extend_transient_D";
+
+
+Goal "[| extend h F : stable C;  G : stable C;  \
+\        extend h F Join G : A ensures B;  A-B = C Int extend_set h D |]  \
+\     ==> F Join project h C G  \
+\           : (project_set h C Int project_set h A) ensures (project_set h B)";
+by (asm_full_simp_tac
+    (simpset() addsimps [ensures_def, Join_constrains, project_constrains, 
+			 Join_transient, extend_transient]) 1);
+by (Clarify_tac 1);
+by (REPEAT_FIRST (rtac conjI));
+(*first subgoal*)
+by (blast_tac (claset() addIs [extend_stable_project_set RS stableD RS 
+			       constrains_Int RS constrains_weaken]
+	                addSDs [extend_constrains_project_set]
+			addSEs [equalityE]) 1);
+(*2nd subgoal*)
+by (etac (stableD RS constrains_Int RS constrains_weaken) 1);
+by (assume_tac 1);
+by (Blast_tac 3);
+by (full_simp_tac (simpset() addsimps [extend_set_Int_distrib,
+				       extend_set_Un_distrib]) 2);
+by (blast_tac (claset() addSIs [impOfSubs extend_set_project_set]) 2);
+by (full_simp_tac (simpset() addsimps [extend_set_def]) 1);
+by (blast_tac (claset() addSEs [equalityE]) 1);
+(*The transient part*)
+by Auto_tac;
+by (force_tac (claset() addSEs [equalityE]
+	                addIs [transient_extend_set_imp_project_transient RS
+			       transient_strengthen], 
+              simpset()) 2);
+by (full_simp_tac (simpset() addsimps [Int_Diff]) 1);
+by (force_tac (claset() addSEs [equalityE]
+	                addIs [transient_extend_set_imp_project_transient RS 
+			 project_extend_transient_D RS transient_strengthen], 
+              simpset()) 1);
+qed "ensures_extend_set_imp_project_ensures";
+
+
+(*Lemma for the Trans case*)
+Goal "[| extend h F Join G : stable C;    \
+\        F Join project h C G    \
+\          : project_set h C Int project_set h A leadsTo project_set h B |] \
+\     ==> F Join project h C G    \
+\           : project_set h C Int project_set h A leadsTo    \
+\             project_set h C Int project_set h B";
+by (rtac (psp_stable2 RS leadsTo_weaken_L) 1);
+by (auto_tac (claset(),
+	      simpset() addsimps [project_stable_project_set, Join_stable, 
+				  extend_stable_project_set]));
+val lemma = result();
+
+Goal "[| extend h F Join G : stable C;  \
+\        extend h F Join G : \
+\          (C Int A) leadsTo[(%D. C Int D)``givenBy f]  B |]  \
+\ ==> F Join project h C G  \
+\   : (project_set h C Int project_set h (C Int A)) leadsTo (project_set h B)";
+by (etac leadsETo_induct 1);
+by (asm_simp_tac (HOL_ss addsimps [Int_UN_distrib, project_set_Union]) 3);
+by (blast_tac (claset() addIs [leadsTo_UN]) 3);
+by (blast_tac (claset() addIs [leadsTo_Trans, lemma]) 2);
+by (asm_full_simp_tac 
+    (simpset() addsimps [givenBy_eq_extend_set, Join_stable]) 1);
+by (rtac leadsTo_Basis 1);
+by (blast_tac (claset() addIs [leadsTo_Basis,
+			       ensures_extend_set_imp_project_ensures]) 1);
+
+qed "project_leadsETo_I_lemma";
+
+Goal "extend h F Join G : (extend_set h A) leadsTo[givenBy f] (extend_set h B)\
+\     ==> F Join project h UNIV G : A leadsTo B";
+by (rtac (project_leadsETo_I_lemma RS leadsTo_weaken) 1);
+by Auto_tac;
+qed "project_leadsETo_I";
+
+Goal "extend h F Join G : (extend_set h A) LeadsTo[givenBy f] (extend_set h B)\
+\     ==> F Join project h (reachable (extend h F Join G)) G  \
+\          : A LeadsTo B";
+by (full_simp_tac (simpset() addsimps [LeadsTo_def, LeadsETo_def]) 1);
+by (rtac (project_leadsETo_I_lemma RS leadsTo_weaken) 1);
+by (auto_tac (claset(), 
+	      simpset() addsimps [project_set_reachable_extend_eq RS sym]));
+qed "project_LeadsETo_I";
+
+Goalw [projecting_def]
+     "projecting (%G. UNIV) h F \
+\                (extend_set h A leadsTo[givenBy f] extend_set h B) \
+\                (A leadsTo B)";
+by (force_tac (claset() addDs [project_leadsETo_I], simpset()) 1);
+qed "projecting_leadsTo";
+
+Goalw [projecting_def]
+     "projecting (%G. reachable (extend h F Join G)) h F \
+\                (extend_set h A LeadsTo[givenBy f] extend_set h B) \
+\                (A LeadsTo B)";
+by (force_tac (claset() addDs [project_LeadsETo_I], simpset()) 1);
+qed "projecting_LeadsTo";
+
 Close_locale "Extend";
 
 
diff -r 72d783f7313a -r 19b9f92ca503 src/HOL/UNITY/Extend.ML
--- a/src/HOL/UNITY/Extend.ML	Tue Dec 21 11:27:32 1999 +0100
+++ b/src/HOL/UNITY/Extend.ML	Tue Dec 21 15:03:02 1999 +0100
@@ -94,6 +94,12 @@
 
 (*** extend_set: basic properties ***)
 
+Goal "(x : project_set h C) = (EX y. h(x,y) : C)";
+by (simp_tac (simpset() addsimps [project_set_def]) 1);
+qed "project_set_iff";
+
+AddIffs [project_set_iff];
+
 Goalw [extend_set_def] "A<=B ==> extend_set h A <= extend_set h B";
 by (Blast_tac 1);
 qed "extend_set_mono";
@@ -101,10 +107,10 @@
 Goalw [extend_set_def] "z : extend_set h A = (f z : A)";
 by (force_tac (claset() addIs  [h_f_g_eq RS sym], simpset()) 1);
 qed "mem_extend_set_iff";
-AddIffs [mem_extend_set_iff]; 
 
-Goalw [extend_set_def]
-    "(extend_set h A <= extend_set h B) = (A <= B)";
+AddIffs [mem_extend_set_iff];
+
+Goalw [extend_set_def] "(extend_set h A <= extend_set h B) = (A <= B)";
 by (Force_tac 1);
 qed "extend_set_strict_mono";
 AddIffs [extend_set_strict_mono];
@@ -117,13 +123,13 @@
 by Auto_tac;
 qed "extend_set_sing";
 
-Goalw [extend_set_def, project_set_def]
+Goalw [extend_set_def]
      "project_set h (extend_set h C) = C";
 by Auto_tac;
 qed "extend_set_inverse";
 Addsimps [extend_set_inverse];
 
-Goalw [extend_set_def, project_set_def]
+Goalw [extend_set_def]
      "C <= extend_set h (project_set h C)";
 by (auto_tac (claset(), 
 	      simpset() addsimps [split_extended_all]));
@@ -144,13 +150,13 @@
 (*** project_set: basic properties ***)
 
 (*project_set is simply image!*)
-Goalw [project_set_def] "project_set h C = f `` C";
+Goal "project_set h C = f `` C";
 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. z : C ==> f z : project_set h C";
+Goal "!!z. z : C ==> f z : project_set h C";
 by (auto_tac (claset(), 
 	      simpset() addsimps [split_extended_all]));
 qed "project_set_I";
@@ -162,13 +168,11 @@
    cannot generalize to 
       project_set h (A Int B) = project_set h A Int project_set h B
 *)
-Goalw [project_set_def]
-     "project_set h ((extend_set h A) Int B) = A Int (project_set h B)";
+Goal "project_set h ((extend_set h A) Int B) = A Int (project_set h B)";
 by Auto_tac;
 qed "project_set_extend_set_Int";
 
-Goalw [project_set_def]
-     "project_set h (A Int B) <= (project_set h A) Int (project_set h B)";
+Goal "project_set h (A Int B) <= (project_set h A) Int (project_set h B)";
 by Auto_tac;
 qed "project_set_Int_subset";
 
@@ -211,25 +215,18 @@
 by Auto_tac;
 qed "extend_act_D";
 
-Goalw [extend_act_def, project_act_def, project_set_def]
+Goalw [extend_act_def, project_act_def]
      "project_act h (extend_act h act) = act";
 by (Blast_tac 1);
 qed "project_act_extend_act";
 
-Goalw [extend_act_def, project_act_def, project_set_def]
+Goalw [extend_act_def, project_act_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.*)
 Goal "Domain act <= project_set h C \
@@ -245,7 +242,7 @@
 Goal "inj (extend_act h)";
 by (rtac inj_on_inverseI 1);
 by (rtac extend_act_inverse 1);
-by (force_tac (claset(), simpset() addsimps [project_set_def]) 1);
+by (Force_tac 1);
 qed "inj_extend_act";
 
 Goalw [extend_set_def, extend_act_def]
@@ -277,12 +274,12 @@
               simpset() addsimps [split_extended_all]) 1);
 qed "project_act_I";
 
-Goalw [project_set_def, project_act_def]
+Goalw [project_act_def]
     "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]
+Goalw [project_act_def]
   "Domain (project_act h act) = project_set h (Domain act)";
 by (force_tac (claset(), 
               simpset() addsimps [split_extended_all]) 1);
@@ -331,11 +328,16 @@
 by Auto_tac;
 qed "extend_SKIP";
 
-Goalw [project_set_def] "project_set h UNIV = UNIV";
+Goal "project_set h UNIV = UNIV";
 by Auto_tac;
 qed "project_set_UNIV";
 Addsimps [project_set_UNIV];
 
+Goal "project_set h (Union A) = (UN X:A. project_set h X)";
+by (Blast_tac 1);
+qed "project_set_Union";
+
+
 Goal "project h C (extend h F) = \
 \     mk_program (Init F, Restrict (project_set h C) `` Acts F)";
 by (rtac program_equalityI 1);
@@ -355,7 +357,7 @@
 Goal "inj (extend h)";
 by (rtac inj_on_inverseI 1);
 by (rtac extend_inverse 1);
-by (force_tac (claset(), simpset() addsimps [project_set_def]) 1);
+by (Force_tac 1);
 qed "inj_extend";
 
 Goal "extend h (F Join G) = extend h F Join extend h G";
@@ -381,8 +383,7 @@
 qed "extend_mono";
 
 Goal "F <= G ==> project h C F <= project h C G";
-by (full_simp_tac
-    (simpset() addsimps [component_eq_subset, project_set_def]) 1);
+by (full_simp_tac (simpset() addsimps [component_eq_subset]) 1);
 by Auto_tac;
 qed "project_mono";
 
@@ -404,8 +405,7 @@
 
 (*Converse fails: A and B may differ in their extra variables*)
 Goal "extend h F : A co B ==> F : (project_set h A) co (project_set h B)";
-by (auto_tac (claset(), 
-	      simpset() addsimps [constrains_def, project_set_def]));
+by (auto_tac (claset(), simpset() addsimps [constrains_def]));
 by (Force_tac 1);
 qed "extend_constrains_project_set";
 
@@ -490,7 +490,7 @@
 by Auto_tac;
 qed "slice_extend_set";
 
-Goalw [slice_def, project_set_def] "project_set h A = (UN y. slice A y)";
+Goalw [slice_def] "project_set h A = (UN y. slice A y)";
 by Auto_tac;
 qed "project_set_is_UN_slice";
 
diff -r 72d783f7313a -r 19b9f92ca503 src/HOL/UNITY/Project.ML
--- a/src/HOL/UNITY/Project.ML	Tue Dec 21 11:27:32 1999 +0100
+++ b/src/HOL/UNITY/Project.ML	Tue Dec 21 15:03:02 1999 +0100
@@ -101,14 +101,6 @@
 by (blast_tac (claset() addIs [constrains_weaken] addDs [constrains_Int]) 1);
 qed "Join_project_stable";
 
-Goal "(F Join project h UNIV G : increasing func)  =  \
-\     (extend h F Join G : increasing (func o f))";
-by (simp_tac (simpset() addsimps [increasing_def, Join_project_stable]) 1);
-by (auto_tac (claset(),
-	      simpset() addsimps [Join_stable, Collect_eq_extend_set RS sym,
-				  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 h C G : A co B";
@@ -119,6 +111,24 @@
 			addDs [constrains_imp_subset]) 1);
 qed "project_constrains_I";
 
+Goalw [increasing_def, stable_def]
+     "extend h F Join G : increasing (func o f) \
+\     ==> F Join project h C G : increasing func";
+by (asm_full_simp_tac (simpset() addsimps [project_constrains_I, 
+					   Collect_eq_extend_set RS sym]) 1);
+qed "project_increasing_I";
+
+Goal "(F Join project h UNIV G : increasing func)  =  \
+\     (extend h F Join G : increasing (func o f))";
+by (rtac iffI 1);
+by (etac project_increasing_I 2);
+by (asm_full_simp_tac 
+    (simpset() addsimps [increasing_def, Join_project_stable]) 1);
+by (auto_tac (claset(),
+	      simpset() addsimps [Join_stable, Collect_eq_extend_set RS sym,
+				  extend_stable RS iffD1]));
+qed "Join_project_increasing";
+
 (*The UNIV argument is essential*)
 Goal "F Join project h UNIV G : A co B \
 \     ==> extend h F Join G : extend_set h A co extend_set h B";
@@ -127,7 +137,7 @@
 			 extend_constrains]) 1);
 qed "project_constrains_D";
 
-(** "projecting" and union/intersection **)
+(** "projecting" and union/intersection (no converses) **)
 
 Goalw [projecting_def]
      "[| projecting C h F XA' XA;  projecting C h F XB' XB |] \
@@ -183,7 +193,9 @@
 qed "extending_UN";
 
 Goalw [extending_def]
-     "[| extending v C h F Y' Y;  Y'<=V';  V<=Y |] ==> extending v C h F V' V";
+     "[| extending v C h F Y' Y;  Y'<=V';  V<=Y; \
+\        preserves w <= preserves v |] \
+\     ==> extending w C h F V' V";
 by Auto_tac;
 qed "extending_weaken";
 
@@ -202,8 +214,8 @@
 qed "projecting_stable";
 
 Goalw [projecting_def]
-     "projecting (%G. UNIV) h F (increasing (func o f)) (increasing func)";
-by (simp_tac (simpset() addsimps [Join_project_increasing]) 1);
+     "projecting C h F (increasing (func o f)) (increasing func)";
+by (blast_tac (claset() addIs [project_increasing_I]) 1);
 qed "projecting_increasing";
 
 Goal "extending v C h F UNIV Y";
@@ -225,19 +237,6 @@
 by (simp_tac (simpset() addsimps [Join_project_increasing]) 1);
 qed "extending_increasing";
 
-(*UNUSED*)
-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";
-
-(*UNUSED*)
-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";
-
 
 (** Reachability and project **)
 
@@ -245,8 +244,8 @@
 \        z : reachable (extend h F Join G) |] \
 \     ==> f z : reachable (F Join project h C G)";
 by (etac reachable.induct 1);
-by (force_tac (claset() addIs [reachable.Init, project_set_I],
-	       simpset()) 1);
+by (force_tac (claset() addSIs [reachable.Init],
+	       simpset() addsimps [split_extended_all]) 1);
 by Auto_tac;
 by (force_tac (claset() addIs [project_act_I RSN (3,reachable.Acts)],
 	       simpset()) 2);
@@ -279,8 +278,8 @@
      "[| reachable (extend h F Join G) <= C;  \
 \        F Join project h C 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);
+by (force_tac (claset() addIs [reachable.Init],
+               simpset() addsimps [project_Stable_D, split_extended_all]) 1);
 qed "project_Always_D";
 
 Goalw [Increasing_def]
@@ -305,14 +304,14 @@
 		        addIs [reachable.Acts, extend_act_D],
 	       simpset() addsimps [project_act_def]) 2);
 by (force_tac (claset() addIs [reachable.Init],
-	       simpset() addsimps [project_set_def]) 1);
+	       simpset()) 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,
 			      subset_refl RS reachable_project_imp_reachable], 
-	      simpset() addsimps [project_set_def]));
+	      simpset()));
 qed "project_set_reachable_extend_eq";
 
 Goal "reachable (extend h F Join G) <= C  \
@@ -353,7 +352,7 @@
 \        extend h F Join G : Always (extend_set h A) |]   \
 \     ==> F Join project h C G : Always A";
 by (auto_tac (claset(), simpset() addsimps [project_Stable_I]));
-by (rewrite_goals_tac [project_set_def, extend_set_def]);
+by (rewtac extend_set_def);
 by (Blast_tac 1);
 qed "project_Always_I";
 
@@ -454,8 +453,7 @@
               simpset() addsimps [Domain_project_act, Int_absorb1]));
 by (REPEAT (ball_tac 1));
 by (auto_tac (claset(),
-              simpset() addsimps [extend_set_def, project_set_def, 
-				  project_act_def]));
+              simpset() addsimps [extend_set_def, project_act_def]));
 by (ALLGOALS Blast_tac);
 qed "transient_extend_set_imp_project_transient";
 
@@ -510,7 +508,7 @@
 \        F Join project h C 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)";
 by (rtac (lemma RS leadsTo_weaken) 1);
-by (auto_tac (claset() addIs [project_set_I], simpset()));
+by (auto_tac (claset(), simpset() addsimps [split_extended_all]));
 qed "project_leadsTo_lemma";
 
 Goal "[| C = (reachable (extend h F Join G)); \
@@ -518,12 +516,11 @@
 \        F Join project h C G : A LeadsTo B |] \
 \     ==> extend h F Join G : (extend_set h A) LeadsTo (extend_set h B)";
 by (asm_full_simp_tac 
-    (simpset() addsimps [LeadsTo_def, project_leadsTo_lemma, stable_reachable, 
+    (simpset() addsimps [LeadsTo_def, project_leadsTo_lemma, 
 			 project_set_reachable_extend_eq]) 1);
 qed "Join_project_LeadsTo";
 
 
-
 (*** GUARANTEES and EXTEND ***)
 
 (** preserves **)
@@ -647,7 +644,8 @@
 qed "preserves_project_transient_empty";
 
 
-(** Guarantees with a leadsTo postcondition **)
+(** Guarantees with a leadsTo postcondition 
+    THESE ARE ALL TOO WEAK because G can't affect F's variables at all**)
 
 Goal "[| F Join project h UNIV G : A leadsTo B;    \
 \        G : preserves f |]  \
diff -r 72d783f7313a -r 19b9f92ca503 src/HOL/UNITY/SubstAx.ML
--- a/src/HOL/UNITY/SubstAx.ML	Tue Dec 21 11:27:32 1999 +0100
+++ b/src/HOL/UNITY/SubstAx.ML	Tue Dec 21 15:03:02 1999 +0100
@@ -12,8 +12,7 @@
 (*Resembles the previous definition of LeadsTo*)
 Goalw [LeadsTo_def]
      "A LeadsTo B = {F. F : (reachable F Int A) leadsTo (reachable F Int B)}";
-by (blast_tac (claset() addDs [psp_stable2] 
-                        addIs [leadsTo_weaken, stable_reachable]) 1);
+by (blast_tac (claset() addDs [psp_stable2] addIs [leadsTo_weaken]) 1);
 qed "LeadsTo_eq_leadsTo";
 
 
diff -r 72d783f7313a -r 19b9f92ca503 src/HOL/UNITY/UNITY.ML
--- a/src/HOL/UNITY/UNITY.ML	Tue Dec 21 11:27:32 1999 +0100
+++ b/src/HOL/UNITY/UNITY.ML	Tue Dec 21 15:03:02 1999 +0100
@@ -269,7 +269,7 @@
 (** Intersection **)
 
 Goalw [stable_def]
-    "[| F : stable A; F : stable A' |] ==> F : stable (A Int A')";
+    "[| F : stable A;  F : stable A' |] ==> F : stable (A Int A')";
 by (blast_tac (claset() addIs [constrains_Int]) 1);
 qed "stable_Int";
 
@@ -284,11 +284,11 @@
 qed "stable_constrains_Un";
 
 Goalw [stable_def, constrains_def]
-  "[| F : stable C; F :  (C Int A) co  A' |] ==> F : (C Int A) co (C Int A')";
+  "[| F : stable C; F :  (C Int A) co A' |] ==> F : (C Int A) co (C Int A')";
 by (Blast_tac 1);
 qed "stable_constrains_Int";
 
-(*[| F : stable C; F :  co (C Int A) A |] ==> F : stable (C Int A)*)
+(*[| F : stable C; F :  (C Int A) co A |] ==> F : stable (C Int A) *)
 bind_thm ("stable_constrains_stable", stable_constrains_Int RS stableI);
 
 
diff -r 72d783f7313a -r 19b9f92ca503 src/HOL/UNITY/Union.ML
--- a/src/HOL/UNITY/Union.ML	Tue Dec 21 11:27:32 1999 +0100
+++ b/src/HOL/UNITY/Union.ML	Tue Dec 21 15:03:02 1999 +0100
@@ -274,8 +274,7 @@
 Goal "[| F : stable A;  G : invariant A |] ==> F Join G : Always A";
 by (full_simp_tac (simpset() addsimps [Always_def, invariant_def, 
 				       Stable_eq_stable, Join_stable]) 1);
-by (force_tac(claset() addIs [stable_reachable, stable_Int],
-	      simpset()) 1);
+by (force_tac(claset() addIs [stable_Int], simpset()) 1);
 qed "stable_Join_Always";
 
 Goal "[| F : stable A;  G : A ensures B |] ==> F Join G : A ensures B";