# HG changeset patch
# User paulson
# Date 947781023 -3600
# Node ID b43ad07660b970e0e1388ec5d96fbd783892c8c8
# Parent  4a53041acb281fe737b581ae4521d8ec5d353d50
working version, with Alloc now working on the same state space as the whole
system.  Partial removal of ELT.

diff -r 4a53041acb28 -r b43ad07660b9 src/HOL/UNITY/Alloc.ML
--- a/src/HOL/UNITY/Alloc.ML	Thu Jan 13 17:29:04 2000 +0100
+++ b/src/HOL/UNITY/Alloc.ML	Thu Jan 13 17:30:23 2000 +0100
@@ -23,10 +23,12 @@
 by (asm_full_simp_tac (simpset() addsimps [o_def]) 1);
 qed "sub_fold";
 
-(*Splits up an intersection: like CONJUNCTS in the HOL system*)
-fun list_of_Int th = (list_of_Int (th RS IntD1) @ list_of_Int (th RS IntD2))
-                     handle THM _ => (list_of_Int (th RS INT_D))
-                     handle THM _ => [th];
+(*Splits up conjunctions & intersections: like CONJUNCTS in the HOL system*)
+fun list_of_Int th = 
+    (list_of_Int (th RS conjunct1) @ list_of_Int (th RS conjunct2))
+    handle THM _ => (list_of_Int (th RS IntD1) @ list_of_Int (th RS IntD2))
+    handle THM _ => (list_of_Int (th RS INT_D))
+    handle THM _ => [th];
 
 (*useful??*)
 val lessThanBspec = lessThan_iff RS iffD2 RSN (2, bspec);
@@ -75,17 +77,6 @@
 by (blast_tac (claset() addIs [tokens_mono_prefix]) 1);
 qed "mono_tokens";
 
-(*Generalized version allowing different clients*)
-Goal "[| Alloc : alloc_spec;  \
-\        Client : (lessThan Nclients) funcset client_spec;  \
-\        Network : network_spec |] \
-\     ==> (extend sysOfAlloc Alloc) \
-\         Join (extend sysOfClient (PLam (lessThan Nclients) Client)) \
-\         Join Network : system_spec";
-
-Goal "System : system_spec";
-
-
 Goalw [sysOfAlloc_def] "inj sysOfAlloc";
 by (rtac injI 1);
 by (auto_tac (claset() addSWrapper record_split_wrapper, simpset()));
@@ -206,15 +197,7 @@
 
 AddIffs  [Network_preserves_allocGiv];
 
-
-Goal "i < Nclients ==> Network : preserves (ask o sub i o client) & \
-\                      Network : preserves (rel o sub i o client)";
-by (rtac (Network_preserves_rel_ask RS revcut_rl) 1);
-by (auto_tac (claset(), 
-	      simpset() addsimps [funPair_o_distrib]));
-qed "Network_preserves_rel_conj_ask";
-
-Addsimps [Network_preserves_rel_conj_ask];
+Addsimps (Network_preserves_rel_ask |> simplify (simpset()) |> list_of_Int);
 
 
 (*Alloc : <unfolded specification> *)
@@ -222,31 +205,41 @@
     rewrite_rule [alloc_spec_def, alloc_increasing_def, alloc_safety_def, 
 		  alloc_progress_def, alloc_preserves_def] Alloc;
 
-val [Alloc_Increasing, Alloc_Safety, 
+val [Alloc_Increasing_0, Alloc_Safety, 
      Alloc_Progress, Alloc_preserves] = list_of_Int Alloc_Spec;
 
+(*Strip off the INT in the guarantees postcondition*)
+val Alloc_Increasing = normalize Alloc_Increasing_0;
 
 fun alloc_export th = good_map_sysOfAlloc RS export th |> simplify (simpset());
 
 fun client_export th = good_map_sysOfClient RS export th |> simplify (simpset());
 
-(*extend sysOfAlloc G : preserves client
-  alloc_export isn't needed!*)
-bind_thm ("extend_sysOfAlloc_preserves_client",
-	  inj_sysOfAlloc RS export inj_extend_preserves  
-	  |> simplify (simpset()));
+AddIffs (Alloc_preserves |> simplify (simpset()) |> list_of_Int);
+
+(** Components lemmas **)
 
-AddIffs [extend_sysOfAlloc_preserves_client];
+(*Alternative is to say that System = Network Join F such that F preserves
+  certain state variables*)
+Goal "(extend sysOfClient (plam x: lessThan Nclients. Client)) Join \
+\     (Network Join Alloc)  =  System";
+by (simp_tac (simpset() addsimps System_def::Join_ac) 1);
+qed "Client_component_System";
 
-Goal "extend sysOfAlloc Alloc : preserves allocRel & \
-\     extend sysOfAlloc Alloc : preserves allocAsk";
-by (cut_facts_tac [Alloc_preserves] 1);
-by (auto_tac (claset() addSDs [alloc_export extend_preserves RS iffD2],
-	      simpset() addsimps [o_def]));
-qed "extend_sysOfAlloc_preserves_Rel_Ask";
+Goal "Network Join \
+\     ((extend sysOfClient (plam x: lessThan Nclients. Client)) Join Alloc) \
+\     = System";
+by (simp_tac (simpset() addsimps System_def::Join_ac) 1);
+qed "Network_component_System";
 
-AddIffs [extend_sysOfAlloc_preserves_Rel_Ask RS conjunct1,
-	 extend_sysOfAlloc_preserves_Rel_Ask RS conjunct2];
+Goal "Alloc Join \
+\      ((extend sysOfClient (plam x: lessThan Nclients. Client)) Join \
+\       Network)  =  System";
+by (simp_tac (simpset() addsimps System_def::Join_ac) 1);
+qed "Alloc_component_System";
+
+AddIffs [Client_component_System, Network_component_System, 
+	 Alloc_component_System];
 
 (** These preservation laws should be generated automatically **)
 
@@ -282,68 +275,28 @@
 AddIffs [extend_sysOfClient_preserves_o_client];
 
 
-(*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)";
-(* 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 
-	  guarantees_Join_I1 RS guaranteesD) 1);
+by (rtac (Alloc_Increasing RS guarantees_Join_I1 RS guaranteesD) 1);
 by Auto_tac;
 qed "System_Increasing_allocGiv";
 
 
-Goalw [System_def]
-     "i < Nclients ==> System : Increasing (ask o sub i o client)";
-by (rtac (client_export extend_guar_Increasing RS guarantees_Join_I2 
-	  RS guaranteesD) 1);
+Goal "i < Nclients ==> System : Increasing (ask o sub i o client)";
+by (rtac ([client_export extend_guar_Increasing,
+	   Client_component_System] MRS component_guaranteesD) 1);
 by (rtac (lift_prog_guar_Increasing RS guarantees_PLam_I) 1);
-by (auto_tac (claset(), 
-	      simpset() addsimps [Network_preserves_rel_ask]));
+by Auto_tac;
 qed "System_Increasing_ask";
 
-Goalw [System_def]
-     "i < Nclients ==> System : Increasing (rel o sub i o client)";
-by (rtac (client_export extend_guar_Increasing RS guarantees_Join_I2 
-	  RS guaranteesD) 1);
+Goal "i < Nclients ==> System : Increasing (rel o sub i o client)";
+by (rtac ([client_export extend_guar_Increasing,
+	   Client_component_System] MRS component_guaranteesD) 1);
 by (rtac (lift_prog_guar_Increasing RS guarantees_PLam_I) 1);
 (*gets Client_Increasing_rel from simpset*)
-by (auto_tac (claset(), 
-	      simpset() addsimps [Network_preserves_rel_ask]));
+by Auto_tac;
 qed "System_Increasing_rel";
 
-(** Components lemmas **)
-
-(*Alternative is to say that System = Network Join F such that F preserves
-  certain state variables*)
-Goal "Network Join \
-\     ((extend sysOfClient (plam x: lessThan Nclients. Client)) Join \
-\      (extend sysOfAlloc Alloc)) \
-\     = System";
-by (simp_tac (simpset() addsimps System_def::Join_ac) 1);
-qed "Network_component_System";
-
-Goal "(extend sysOfAlloc Alloc) Join \
-\      ((extend sysOfClient (plam x: lessThan Nclients. Client)) Join \
-\       Network) \
-\     = System";
-by (simp_tac (simpset() addsimps System_def::Join_ac) 1);
-qed "Alloc_component_System";
-
-AddIffs [Network_component_System, Alloc_component_System];
-
 (** Follows consequences.
     The "Always (INT ...) formulation expresses the general safety property
     and allows it to be combined using Always_Int_rule below. **)
@@ -365,7 +318,7 @@
 Goal
   "i < Nclients ==> System : (giv o sub i o client) Fols (sub i o allocGiv)";
 by (auto_tac (claset() addSIs [Network_Giv RS component_guaranteesD, 
-		 extend_Alloc_Increasing_allocGiv RS component_guaranteesD], 
+		 Alloc_Increasing RS component_guaranteesD], 
 	      simpset()));
 qed "System_Follows_allocGiv";
 
@@ -399,28 +352,10 @@
 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_L) 2);
-(*1: Increasing precondition*)
-by (rtac (alloc_export projecting_Increasing RS projecting_weaken_L 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 (rtac (extend_Alloc_Safety RS component_guaranteesD) 1);
-by (rtac Alloc_component_System 2);
+by (rtac ([Alloc_Safety, Alloc_component_System] MRS component_guaranteesD) 1);
 (*preserves*)
 by (asm_full_simp_tac (simpset() addsimps [o_def]) 2);
 by (force_tac (claset(), simpset() addsimps [System_Increasing_allocRel]) 1);
@@ -484,12 +419,12 @@
 
 (*progress (2), step 3*)
 (*All this trouble just to lift "Client_Bounded" through two extend ops*)
-Goalw [System_def]
-     "i < Nclients \
-\   ==> System : Always \
-\                 {s. ALL elt : set ((ask o sub i o client) s). elt <= NbT}";
-by (rtac (guarantees_PLam_I RS client_export UNIV_guar_Always RS
-	  guarantees_Join_I2 RS guaranteesD RS Always_weaken) 1);
+Goal "i < Nclients \
+\     ==> System : Always \
+\                   {s. ALL elt : set ((ask o sub i o client) s). elt <= NbT}";
+br Always_weaken 1;
+by (rtac ([guarantees_PLam_I RS client_export UNIV_guar_Always,
+	   Client_component_System] MRS component_guaranteesD) 1);
 by (rtac Client_i_Bounded 1);
 by (auto_tac(claset(),
 	 simpset() addsimps [o_apply, lift_export Collect_eq_extend_set RS sym,
@@ -516,48 +451,126 @@
 	      simpset()));
 qed "System_Increasing_giv";
 
-(*Lemma.  A LOT of work just to lift "Client_Progress" to the array*)
+(** A LOT of work just to lift "Client_Progress" to the array **)
+
+(*stability lemma for G*)
+Goalw [preserves_def, o_def, stable_def, constrains_def, sub_def]
+     "[| ALL z. G : stable      \
+\                   (reachable (lift_prog i Client Join G) Int      \
+\                    {s. z <= (giv o sub i) s});      \
+\         G : preserves (rel o sub i);  G : preserves (ask o sub i) |]      \
+\      ==> G : stable      \
+\               (reachable (lift_prog i Client Join G) Int      \
+\                {s. h <= (giv o sub i) s & h pfixGe (ask o sub i) s} -      \
+\                {s. tokens h <= tokens ((rel o sub i) s)})";
+auto();
+by (REPEAT (dres_inst_tac [("x", "rel (xa i)")] spec 2));
+by (REPEAT (dres_inst_tac [("x", "ask (xa i)")] spec 1));
+by (REPEAT_FIRST ball_tac);
+auto();
+qed "G_stable_lift_prog";
+
 Goal "lift_prog i Client \
 \        : Increasing (giv o sub i)  \
 \          guarantees[funPair rel ask o sub i] \
 \          (INT h. {s. h <=  (giv o sub i) s & \
 \                             h pfixGe (ask o sub i) s}  \
-\                  LeadsTo[givenBy (funPair rel ask o sub i)] \
-\                  {s. tokens h <= (tokens o rel o sub i) s})";
-by (rtac (Client_Progress RS drop_prog_guarantees) 1);
-by (rtac (lift_export extending_LeadsETo RS extending_weaken_L RS
-	  extending_INT) 2);
-by (asm_simp_tac (simpset() addsimps [lift_export Collect_eq_extend_set RS sym,
-				  sub_def, o_def]) 2);
-by (rtac (lift_export projecting_Increasing) 1);
-by (auto_tac (claset(), simpset() addsimps [o_def]));
+\                  Ensures {s. tokens h <= (tokens o rel o sub i) s})";
+by (rtac (Client_Progress RS drop_prog_guarantees_raw) 1);
+br (lift_export (subset_refl RS project_Increasing_I)) 1;
+by (full_simp_tac (simpset() addsimps [fold_o_sub, lift_prog_correct]) 1);
+br INT_I 1;
+by (simp_tac (simpset() addsimps [o_apply]) 1);
+by (REPEAT (stac (lift_export Collect_eq_extend_set) 1));
+br (lift_export project_Ensures_D) 1;
+by (asm_full_simp_tac (simpset() addsimps [o_apply, lift_prog_correct, 
+					   drop_prog_correct]) 1);
+by (asm_full_simp_tac
+    (simpset() addsimps [all_conj_distrib,
+			 Increasing_def, Stable_eq_stable, Join_stable,
+			 lift_set_correct RS sym,
+			 Collect_eq_lift_set RS sym,
+			 lift_prog_correct RS sym]) 1);
+by (Clarify_tac 1);
+bd G_stable_lift_prog 1;
+by (auto_tac (claset(), 
+	      simpset() addsimps [o_apply]));
 qed "Client_i_Progress";
 
+Goal "i < Nclients \
+\   ==> (plam x: lessThan Nclients. Client) \
+\        : Increasing (giv o sub i)  \
+\          guarantees[funPair rel ask o sub i] \
+\          (INT h. {s. h <=  (giv o sub i) s & \
+\                             h pfixGe (ask o sub i) s}  \
+\                  Ensures {s. tokens h <= (tokens o rel o sub i) s})";
+by (rtac guarantees_PLam_I 1);
+br Client_i_Progress 1;
+by Auto_tac;
+val lemma2 = result();
+
+(*another stability lemma for G*)
+Goalw [preserves_def, o_def, stable_def, constrains_def, sub_def]
+     "[| ALL z. G : stable      \
+\                  (reachable (extend sysOfClient  \
+\                              (plam x:lessThan Nclients. Client) Join G) Int \
+\                    {s. z <= (giv o sub i o client) s});      \
+\         G : preserves (rel o sub i o client);  \
+\         G : preserves (ask o sub i o client) |]      \
+\ ==> G : stable      \
+\          (reachable (extend sysOfClient  \
+\                      (plam x:lessThan Nclients. Client) Join G) Int \
+\           {s. h <= (giv o sub i o client) s & \
+\               h pfixGe (ask o sub i o client) s} - \
+\           {s. tokens h <= tokens ((rel o sub i o client) s)})";
+auto();
+by (REPEAT (dres_inst_tac [("x", "rel (client xa i)")] spec 2));
+by (REPEAT (dres_inst_tac [("x", "ask (client xa i)")] spec 1));
+by (REPEAT_FIRST ball_tac);
+auto();
+qed "G_stable_sysOfClient";
+
+Goal "i < Nclients \
+\  ==> extend sysOfClient (plam x: lessThan Nclients. Client) \
+\       : Increasing (giv o sub i o client)  \
+\         guarantees[funPair rel ask o sub i o client] \
+\         (INT h. {s. h <=  (giv o sub i o client) s & \
+\                            h pfixGe (ask o sub i o client) s}  \
+\                 Ensures {s. tokens h <= (tokens o rel o sub i o client) s})";
+by (rtac (lemma2 RS client_export project_guarantees_raw) 1);
+ba 1;
+br (client_export (subset_refl RS project_Increasing_I)) 1;
+by (Simp_tac 1);
+br INT_I 1;
+by (simp_tac (simpset() addsimps [o_apply]) 1);
+by (REPEAT (stac (client_export Collect_eq_extend_set) 1));
+br (client_export project_Ensures_D) 1;
+by (asm_full_simp_tac (simpset() addsimps [o_apply]) 1);
+by (asm_full_simp_tac
+    (simpset() addsimps [all_conj_distrib,
+			 Increasing_def, Stable_eq_stable, Join_stable,
+			 Collect_eq_extend_set RS sym]) 1);
+by (Clarify_tac 1);
+bd G_stable_sysOfClient 1;
+by (auto_tac (claset(), 
+	      simpset() addsimps [o_apply,
+				client_export Collect_eq_extend_set RS sym]));
+qed "sysOfClient_i_Progress";
+
+
 (*progress (2), step 7*)
-Goalw [System_def]
+Goal
  "System : (INT i : lessThan Nclients. \
 \           INT h. {s. h <= (giv o sub i o client) s & \
 \                      h pfixGe (ask o sub i o client) s}  \
-\                  LeadsTo[givenBy (funPair rel ask o sub i o client)] \
-\                  {s. tokens h <= (tokens o rel o sub i o client) s})";
-by (stac INT_iff 1);
-by (rtac ballI 1);
+\               Ensures {s. tokens h <= (tokens o rel o sub i o client) s})";
+by (rtac INT_I 1);
 (*Couldn't have just used Auto_tac since the "INT h" must be kept*)
-by (rtac (guarantees_Join_I2 RS guaranteesD) 1);
-by (rtac (Client_i_Progress RS
-	  (guarantees_PLam_I RS client_export project_guarantees)) 1);
-by (Blast_tac 1);
-by (Asm_simp_tac 1);
-by (fast_tac (claset() addIs [projecting_Int,
-			      component_PLam,
-			      client_export projecting_Increasing]) 1);
+by (rtac ([sysOfClient_i_Progress,
+	   Client_component_System] MRS component_guaranteesD) 1);
 by (asm_full_simp_tac
-    (simpset() addsimps [rewrite_rule [System_def] System_Increasing_giv]) 5);
-by (rtac (client_export extending_LeadsETo RS extending_weaken_L RS 
-	  extending_INT) 1);
-by (auto_tac (claset(), 
-	      simpset() addsimps [o_apply, 
-				client_export Collect_eq_extend_set RS sym]));
+    (simpset() addsimps [System_Increasing_giv]) 2);
+auto();
 qed "System_Client_Progress";
 
 val lemma =
@@ -583,11 +596,7 @@
 val lemma3 = result();
 
 
-(*NOT GOOD ENOUGH.  Needs givenBy restriction
-     (funPair allocGiv (funPair allocAsk allocRel))
-  in LeadsTo!   But System_Client_Progress has the wrong restriction (below)
-*)
-(*progress (2), step 8*)
+(*progress (2), step 8: Client i's "release" action is visible system-wide*)
 Goal "i < Nclients  \
 \     ==> System : {s. h <= (sub i o allocGiv) s & \
 \                      h pfixGe (sub i o allocAsk) s}  \
@@ -597,75 +606,20 @@
 	  Follows_LeadsTo) 2);
 by (asm_full_simp_tac (simpset() addsimps [o_assoc]) 2);
 by (rtac LeadsTo_Trans 1);
-by (rtac (impOfSubs LeadsETo_subset_LeadsTo) 2);
-(*Here we have givenBy (funPair rel ask o sub i o client)]
-  when we need givenBy (funPair allocRel allocAsk) ?? *)
 by (cut_facts_tac [System_Client_Progress] 2);
-by (Force_tac 2);
+by (blast_tac (claset() addIs [LeadsTo_Basis]) 2);
 by (etac lemma3 1);
-qed "System_Alloc_Progress";
-
-(*NEED AUTOMATIC PROPAGATION of Alloc_Progress.  The text is identical
-  except in the LeadsTo precondition.*)
-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 elt : set ((sub i o allocAsk) s). elt <= NbT}   \
-\  Int   \
-\  (INT i : lessThan Nclients.    \
-\   INT h. {s. h <= (sub i o allocGiv)s & h pfixGe (sub i o allocAsk)s}   \
-\          LeadsTo[givenBy (funPair allocGiv (funPair allocAsk allocRel))]  \
-\          {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: Complex precondition*)
-by (rtac (projecting_Int RS projecting_INT RS projecting_Int RS 
-	  projecting_Int) 1);
-by (rtac (alloc_export projecting_Increasing RS projecting_weaken_L) 1);
-by (asm_simp_tac (simpset() addsimps [o_def]) 1);
-by (rtac (alloc_export projecting_Increasing RS projecting_weaken_L) 1);
-by (asm_simp_tac (simpset() addsimps [o_def]) 1);
-by (rtac (alloc_export projecting_Always RS projecting_weaken_L) 1);
-by (asm_simp_tac
-    (simpset() addsimps [alloc_export Collect_eq_extend_set RS sym, o_def]) 1);
-(*LeadsTo precondition*)
-by (rtac (projecting_INT RS projecting_INT) 1);
-by (rtac (alloc_export projecting_LeadsTo RS projecting_weaken_L) 1);
-by (auto_tac (claset(),
-	      simpset() addsimps [alloc_export Collect_eq_extend_set RS sym,
-				  o_def]));
-by (auto_tac (claset() addSIs [givenByI]
-		       addEs [LeadsETo_weaken, givenByD]
-		       addSWrapper record_split_wrapper, 
-	      simpset() addsimps [funPair_def]));
-qed "extend_Alloc_Progress";
+qed "System_Alloc_Client_Progress";
 
 
-xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx;
 
 (*progress (2), step 9*)
 Goal
  "System : (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 (extend_Alloc_Progress RS component_guaranteesD) 1);
-by (rtac Alloc_component_System 2);
+\                  LeadsTo {s. h pfixLe (sub i o allocGiv) s})";
+by (rtac ([Alloc_Progress, Alloc_component_System] 
+	  MRS component_guaranteesD) 1);
 (*preserves*)
 by (asm_full_simp_tac (simpset() addsimps [o_def]) 2);
 (*the guarantees precondition*)
@@ -673,8 +627,50 @@
 	      simpset() addsimps [System_Increasing_allocRel,
 				  System_Increasing_allocAsk]));
 by (rtac System_Bounded_allocAsk 1);
-by (rtac System_Alloc_Progress 1);
+by (etac System_Alloc_Progress 1);
+qed "System_Alloc_Progress";
+
+
+
+(*Ultimate goal*)
+Goal "System : system_spec";
+
+xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx;
+
+
+(*progress (2), step 10*)
+Goal
+ "System : (INT i : lessThan Nclients. \
+\           INT h. {s. h <= (ask o sub i o client) s}  \
+\                  LeadsTo {s. h pfixLe (giv o sub i o client) s})";
+by (Clarify_tac 1);
+by (rtac LeadsTo_Trans 1);
+by (dtac (System_Follows_allocGiv RS Follows_LeadsTo) 2);
+by (blast_tac (claset() addIs [prefix_imp_pfixLe, LeadsTo_weaken_R]) 2);
+
+prefix_imp_pfixLe
+
 
-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);
+System_Follows_ask
+
+by (dtac (System_Follows_rel RS impOfSubs (mono_tokens RS mono_Follows_o) RS 
+	  Follows_LeadsTo) 2);
+
+by (asm_full_simp_tac (simpset() addsimps [o_assoc]) 2);
+by (rtac LeadsTo_Trans 1);
+by (cut_facts_tac [System_Client_Progress] 2);
+by (blast_tac (claset() addIs [LeadsTo_Basis]) 2);
+by (etac lemma3 1);
+
+by (rtac ([Alloc_Progress, Alloc_component_System] 
+	  MRS component_guaranteesD) 1);
+(*preserves*)
+by (asm_full_simp_tac (simpset() addsimps [o_def]) 2);
+(*the guarantees precondition*)
+by (auto_tac (claset(), 
+	      simpset() addsimps [System_Increasing_allocRel,
+				  System_Increasing_allocAsk]));
+by (rtac System_Bounded_allocAsk 1);
+by (etac System_Alloc_Progress 1);
+qed "System_Alloc_Progress";
+
diff -r 4a53041acb28 -r b43ad07660b9 src/HOL/UNITY/Alloc.thy
--- a/src/HOL/UNITY/Alloc.thy	Thu Jan 13 17:29:04 2000 +0100
+++ b/src/HOL/UNITY/Alloc.thy	Thu Jan 13 17:30:23 2000 +0100
@@ -88,8 +88,7 @@
 	 Increasing giv
 	 guarantees[funPair rel ask]
 	 (INT h. {s. h <= giv s & h pfixGe ask s}
-		 LeadsTo[givenBy (funPair rel ask)]
-		 {s. tokens h <= (tokens o rel) s})"
+		 Ensures {s. tokens h <= (tokens o rel) s})"
 
   (*spec: preserves part*)
     client_preserves :: clientState program set
@@ -101,15 +100,18 @@
 
 (** Allocator specification (required) ***)
 
+  (*Specified over the systemState, not the allocState, since then the
+    leads-to properties could not be transferred to  extend sysOfAlloc Alloc*)
+  
   (*spec (6)*)
-  alloc_increasing :: allocState program set
+  alloc_increasing :: systemState program set
     "alloc_increasing ==
 	 UNIV
          guarantees[allocGiv]
 	 (INT i : lessThan Nclients. Increasing (sub i o allocGiv))"
 
   (*spec (7)*)
-  alloc_safety :: allocState program set
+  alloc_safety :: systemState program set
     "alloc_safety ==
 	 (INT i : lessThan Nclients. Increasing (sub i o allocRel))
          guarantees[allocGiv]
@@ -117,7 +119,7 @@
 	         <= NbT + sum (%i. (tokens o sub i o allocRel) s) Nclients}"
 
   (*spec (8)*)
-  alloc_progress :: allocState program set
+  alloc_progress :: systemState program set
     "alloc_progress ==
 	 (INT i : lessThan Nclients. Increasing (sub i o allocAsk) Int
 	                             Increasing (sub i o allocRel))
@@ -132,14 +134,14 @@
          guarantees[allocGiv]
 	     (INT i : lessThan Nclients.
 	      INT h. {s. h <= (sub i o allocAsk) s}
-	             LeadsTo[givenBy allocGiv]
+	             LeadsTo
 	             {s. h pfixLe (sub i o allocGiv) s})"
 
   (*spec: preserves part*)
-    alloc_preserves :: allocState program set
-    "alloc_preserves == preserves (funPair allocRel allocAsk)"
+    alloc_preserves :: systemState program set
+    "alloc_preserves == preserves (funPair client (funPair allocRel allocAsk))"
   
-  alloc_spec :: allocState program set
+  alloc_spec :: systemState program set
     "alloc_spec == alloc_increasing Int alloc_safety Int alloc_progress Int
                    alloc_preserves"
 
@@ -190,7 +192,7 @@
 
 locale System =
   fixes 
-    Alloc   :: allocState program
+    Alloc   :: systemState program
     Client  :: clientState program
     Network :: systemState program
     System  :: systemState program
@@ -202,9 +204,6 @@
 
   defines
     System_def
-      "System == (extend sysOfAlloc Alloc)
-                 Join
-                 (extend sysOfClient (plam x: lessThan Nclients. Client))
-                 Join
-                 Network"
+      "System == Alloc Join Network Join
+                 (extend sysOfClient (plam x: lessThan Nclients. Client))"
 end
diff -r 4a53041acb28 -r b43ad07660b9 src/HOL/UNITY/Comp.ML
--- a/src/HOL/UNITY/Comp.ML	Thu Jan 13 17:29:04 2000 +0100
+++ b/src/HOL/UNITY/Comp.ML	Thu Jan 13 17:30:23 2000 +0100
@@ -172,3 +172,75 @@
 by (etac order_trans 1);
 by (Blast_tac 1);
 qed "Increasing_preserves_Stable";
+
+
+(*** givenBy ***)
+
+Goalw [givenBy_def] "givenBy id = UNIV";
+by Auto_tac;
+qed "givenBy_id";
+Addsimps [givenBy_id];
+
+Goalw [givenBy_def] "(givenBy v) = {A. ALL x:A. ALL y. v x = v y --> y: A}";
+by Safe_tac;
+by (res_inst_tac [("x", "v `` ?u")] image_eqI 2);
+by Auto_tac;
+qed "givenBy_eq_all";
+
+Goal "givenBy v = {A. EX P. A = {s. P(v s)}}";
+by (simp_tac (simpset() addsimps [givenBy_eq_all]) 1);
+by Safe_tac;
+by (res_inst_tac [("x", "%n. EX s. v s = n & s : ?A")] exI 1);
+by (Blast_tac 1);
+by Auto_tac;
+qed "givenBy_eq_Collect";
+
+val prems =
+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";
+
+Goalw [givenBy_def] "[| A: givenBy v;  x:A;  v x = v y |] ==> y: A";
+by Auto_tac;
+qed "givenByD";
+
+Goal "{} : givenBy v";
+by (blast_tac (claset() addSIs [givenByI]) 1);
+qed "empty_mem_givenBy";
+
+AddIffs [empty_mem_givenBy];
+
+Goal "A: givenBy v ==> EX P. A = {s. P(v s)}";
+by (res_inst_tac [("x", "%n. EX s. v s = n & s : A")] exI 1);
+by (full_simp_tac (simpset() addsimps [givenBy_eq_all]) 1);
+by (Blast_tac 1);
+qed "givenBy_imp_eq_Collect";
+
+Goalw [givenBy_def] "{s. P(v s)} : givenBy v";
+by (Best_tac 1);
+qed "Collect_mem_givenBy";
+
+Goal "givenBy v = {A. EX P. A = {s. P(v s)}}";
+by (blast_tac (claset() addIs [Collect_mem_givenBy,
+			       givenBy_imp_eq_Collect]) 1);
+qed "givenBy_eq_eq_Collect";
+
+(*preserving v preserves properties given by v*)
+Goal "[| F : preserves v;  D : givenBy v |] ==> F : stable D";
+by (force_tac (claset(), 
+	       simpset() addsimps [impOfSubs preserves_subset_stable, 
+				   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";
+
+Goal "[| A : givenBy v;  B : givenBy v |] ==> A-B : givenBy v";
+by (full_simp_tac (simpset() addsimps [givenBy_eq_Collect]) 1);
+by Safe_tac;
+by (res_inst_tac [("x", "%z. ?R z & ~ ?Q z")] exI 1);
+by (deepen_tac (set_cs addSIs [equalityI]) 0 1);
+qed "givenBy_DiffI";
diff -r 4a53041acb28 -r b43ad07660b9 src/HOL/UNITY/Comp.thy
--- a/src/HOL/UNITY/Comp.thy	Thu Jan 13 17:29:04 2000 +0100
+++ b/src/HOL/UNITY/Comp.thy	Thu Jan 13 17:30:23 2000 +0100
@@ -26,4 +26,8 @@
   funPair      :: "['a => 'b, 'a => 'c, 'a] => 'b * 'c"
     "funPair f g == %x. (f x, g x)"
 
+  (*the set of all sets determined by f alone*)
+  givenBy :: "['a => 'b] => 'a set set"
+    "givenBy f == range (%B. f-`` B)"
+
 end
diff -r 4a53041acb28 -r b43ad07660b9 src/HOL/UNITY/ELT.ML
--- a/src/HOL/UNITY/ELT.ML	Thu Jan 13 17:29:04 2000 +0100
+++ b/src/HOL/UNITY/ELT.ML	Thu Jan 13 17:30:23 2000 +0100
@@ -6,69 +6,6 @@
 leadsTo strengthened with a specification of the allowable sets transient parts
 *)
 
-Goalw [givenBy_def] "givenBy id = UNIV";
-by Auto_tac;
-qed "givenBy_id";
-Addsimps [givenBy_id];
-
-Goalw [givenBy_def] "(givenBy v) = {A. ALL x:A. ALL y. v x = v y --> y: A}";
-by Safe_tac;
-by (res_inst_tac [("x", "v `` ?u")] image_eqI 2);
-by Auto_tac;
-qed "givenBy_eq_all";
-
-Goal "givenBy v = {A. EX P. A = {s. P(v s)}}";
-by (simp_tac (simpset() addsimps [givenBy_eq_all]) 1);
-by Safe_tac;
-by (res_inst_tac [("x", "%n. EX s. v s = n & s : ?A")] exI 1);
-by (Blast_tac 1);
-by Auto_tac;
-qed "givenBy_eq_Collect";
-
-val prems =
-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";
-
-Goalw [givenBy_def] "[| A: givenBy v;  x:A;  v x = v y |] ==> y: A";
-by Auto_tac;
-qed "givenByD";
-
-Goal "{} : givenBy v";
-by (blast_tac (claset() addSIs [givenByI]) 1);
-qed "empty_mem_givenBy";
-
-AddIffs [empty_mem_givenBy];
-
-Goal "A: givenBy v ==> EX P. A = {s. P(v s)}";
-by (res_inst_tac [("x", "%n. EX s. v s = n & s : A")] exI 1);
-by (full_simp_tac (simpset() addsimps [givenBy_eq_all]) 1);
-by (Blast_tac 1);
-qed "givenBy_imp_eq_Collect";
-
-Goalw [givenBy_def] "EX P. A = {s. P(v s)} ==> A: givenBy v";
-by (Best_tac 1);
-qed "eq_Collect_imp_givenBy";
-
-Goal "givenBy v = {A. EX P. A = {s. P(v s)}}";
-by (blast_tac (claset() addIs [eq_Collect_imp_givenBy,
-			       givenBy_imp_eq_Collect]) 1);
-qed "givenBy_eq_eq_Collect";
-
-(*preserving v preserves properties given by v*)
-Goal "[| F : preserves v;  D : givenBy v |] ==> F : stable D";
-by (force_tac (claset(), 
-	       simpset() addsimps [impOfSubs preserves_subset_stable, 
-				   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 **)
 
 Goalw [leadsETo_def]
@@ -81,6 +18,7 @@
 by (blast_tac (claset() addIs [elt.Trans]) 1);
 qed "leadsETo_Trans";
 
+
 (*Useful with cancellation, disjunction*)
 Goal "F : A leadsTo[CC] (A' Un A') ==> F : A leadsTo[CC] A'";
 by (asm_full_simp_tac (simpset() addsimps Un_ac) 1);
@@ -126,6 +64,11 @@
 by (blast_tac (claset() addIs [leadsETo_Basis]) 1);
 qed "leadsETo_mono";
 
+Goal "[| F : A leadsTo[CC] B;  F : B leadsTo[DD] C |] \
+\     ==> F : A leadsTo[CC Un DD] C";
+by (blast_tac (claset() addIs [impOfSubs leadsETo_mono, leadsETo_Trans]) 1);
+qed "leadsETo_Trans_Un";
+
 val prems = Goalw [leadsETo_def]
  "(!!A. A : S ==> F : (A Int C) leadsTo[CC] B) ==> F : (Union S Int C) leadsTo[CC] B";
 by (simp_tac (HOL_ss addsimps [Int_Union_Union]) 1);
@@ -154,6 +97,7 @@
 Addsimps [empty_leadsETo];
 
 
+
 (** Weakening laws **)
 
 Goal "[| F : A leadsTo[CC] A';  A'<=B' |] ==> F : A leadsTo[CC] B'";
@@ -478,22 +422,6 @@
 
 Open_locale "Extend";
 
-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);
-by (Blast_tac 1);
-qed "extend_set_givenBy_I";
-
-
 Goal "F : A leadsTo[CC] B \
 \     ==> extend h F : (extend_set h A) leadsTo[extend_set h `` CC] \
 \                      (extend_set h B)";
@@ -505,24 +433,6 @@
 				   extend_set_Diff_distrib RS sym]) 1);
 qed "leadsETo_imp_extend_leadsETo";
 
-(*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(), simpset() addsimps [split_extended_all]));
-qed "Int_extend_set_lemma";
-
-(*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]) 1);
-by (Blast_tac 1);
-qed "project_constrains_project_set";
-
-(*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);
-qed "project_stable_project_set";
-
 
 
 (*NOT USED, but analogous to preserves_project_transient_empty in Project.ML*)
@@ -535,18 +445,6 @@
 				project_preserves_I]) 1);
 result();
 
-(*GENERALIZES the version proved in Project.ML*)
-Goal "[| G : preserves (v o f);  \
-\        project h C G : transient (C' Int D);  \
-\        project h C G : stable C';  D : givenBy v |]    \
-\     ==> C' Int D = {}";
-by (rtac stable_transient_empty 1);
-by (assume_tac 2);
-(*If addIs then PROOF FAILED at depth 3*)
-by (blast_tac (claset() addSIs [stable_Int, preserves_givenBy_imp_stable,
-				project_preserves_I]) 1);
-qed "preserves_o_project_transient_empty";
-
 
 (*This version's stronger in the "ensures" precondition
   BUT there's no ensures_weaken_L*)
diff -r 4a53041acb28 -r b43ad07660b9 src/HOL/UNITY/ELT.thy
--- a/src/HOL/UNITY/ELT.thy	Thu Jan 13 17:29:04 2000 +0100
+++ b/src/HOL/UNITY/ELT.thy	Thu Jan 13 17:30:23 2000 +0100
@@ -4,6 +4,22 @@
     Copyright   1999  University of Cambridge
 
 leadsTo strengthened with a specification of the allowable sets transient parts
+
+TRY INSTEAD (to get rid of the {} and to gain strong induction)
+
+  elt :: "['a set set, 'a program, 'a set] => ('a set) set"
+
+inductive "elt CC F B"
+  intrs 
+
+    Weaken  "A <= B ==> A : elt CC F B"
+
+    ETrans  "[| F : A ensures A';  A-A' : CC;  A' : elt CC F B |]
+	     ==> A : elt CC F B"
+
+    Union  "{A. A: S} : Pow (elt CC F B) ==> (Union S) : elt CC F B"
+
+  monos Pow_mono
 *)
 
 ELT = Project +
@@ -28,10 +44,6 @@
 
 constdefs
 
-  (*the set of all sets determined by f alone*)
-  givenBy :: "['a => 'b] => 'a set set"
-    "givenBy f == range (%B. f-`` B)"
-
   (*visible version of the LEADS-TO relation*)
   leadsETo :: "['a set, 'a set set, 'a set] => 'a program set"
                                         ("(3_/ leadsTo[_]/ _)" [80,0,80] 80)
diff -r 4a53041acb28 -r b43ad07660b9 src/HOL/UNITY/Extend.ML
--- a/src/HOL/UNITY/Extend.ML	Thu Jan 13 17:29:04 2000 +0100
+++ b/src/HOL/UNITY/Extend.ML	Thu Jan 13 17:30:23 2000 +0100
@@ -327,6 +327,7 @@
 by (rtac program_equalityI 1);
 by Auto_tac;
 qed "extend_SKIP";
+Addsimps [export extend_SKIP];
 
 Goal "project_set h UNIV = UNIV";
 by Auto_tac;
@@ -456,6 +457,24 @@
 qed "extend_Always";
 
 
+(** Further lemmas **)
+
+Goal "A Int extend_set h ((project_set h A) Int B) = A Int extend_set h B";
+by (auto_tac (claset(), simpset() addsimps [split_extended_all]));
+qed "Int_extend_set_lemma";
+
+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]) 1);
+by (Blast_tac 1);
+qed "project_constrains_project_set";
+
+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);
+qed "project_stable_project_set";
+
+
 (*** Progress: transient, ensures ***)
 
 Goal "(extend h F : transient (extend_set h A)) = (F : transient A)";
@@ -550,6 +569,24 @@
 qed "extend_LeadsTo";
 
 
+(*** givenBy: USEFUL??? ***)
+
+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);
+by (Blast_tac 1);
+qed "extend_set_givenBy_I";
+
+
 Close_locale "Extend";
 
 (*Close_locale should do this!
diff -r 4a53041acb28 -r b43ad07660b9 src/HOL/UNITY/Follows.thy
--- a/src/HOL/UNITY/Follows.thy	Thu Jan 13 17:29:04 2000 +0100
+++ b/src/HOL/UNITY/Follows.thy	Thu Jan 13 17:30:23 2000 +0100
@@ -9,7 +9,7 @@
   progress part: g cannot do anything silly.
 *)
 
-Follows = ELT +
+Follows = Project +
 
 constdefs
 
diff -r 4a53041acb28 -r b43ad07660b9 src/HOL/UNITY/Guar.ML
--- a/src/HOL/UNITY/Guar.ML	Thu Jan 13 17:29:04 2000 +0100
+++ b/src/HOL/UNITY/Guar.ML	Thu Jan 13 17:30:23 2000 +0100
@@ -80,7 +80,7 @@
 (*This version of guaranteesD matches more easily in the conclusion
   The major premise can no longer be  F<=H since we need to reason about G*)
 Goalw [guar_def]
-     "[| F : X guarantees[v] Y;  H : X;  F Join G = H;  G : preserves v |] \
+     "[| F : X guarantees[v] Y;  F Join G = H;  H : X;  G : preserves v |] \
 \     ==> H : Y";
 by (Blast_tac 1);
 qed "component_guaranteesD";
diff -r 4a53041acb28 -r b43ad07660b9 src/HOL/UNITY/Lift_prog.ML
--- a/src/HOL/UNITY/Lift_prog.ML	Thu Jan 13 17:29:04 2000 +0100
+++ b/src/HOL/UNITY/Lift_prog.ML	Thu Jan 13 17:30:23 2000 +0100
@@ -120,7 +120,7 @@
 by Auto_tac;
 qed "good_map_lift_map";
 
-fun lift_export th = 
+fun lift_export0 th = 
     good_map_lift_map RS export th 
        |> simplify (simpset() addsimps [fold_o_sub]);;
 
@@ -133,7 +133,7 @@
 
 Goal "lift_set i A = extend_set (lift_map i) A";
 by (auto_tac (claset(), 
-     simpset() addsimps [lift_export mem_extend_set_iff]));
+     simpset() addsimps [lift_export0 mem_extend_set_iff]));
 qed "lift_set_correct";
 
 Goalw [drop_set_def, project_set_def, lift_map_def]
@@ -148,7 +148,7 @@
 Goal "lift_act i = extend_act (lift_map i)";
 by (rtac ext 1);
 by Auto_tac;
-by (forward_tac [lift_export extend_act_D] 2);
+by (forward_tac [lift_export0 extend_act_D] 2);
 by (auto_tac (claset(), simpset() addsimps [extend_act_def]));
 by (auto_tac (claset(), simpset() addsimps [extend_act_def, lift_map_def]));
 by (rtac bexI 1);
@@ -168,7 +168,7 @@
 by (rtac (program_equalityI RS ext) 1);
 by (simp_tac (simpset() addsimps [lift_set_correct]) 1);
 by (simp_tac (simpset() 
-	      addsimps [lift_export Acts_extend, 
+	      addsimps [lift_export0 Acts_extend, 
 			lift_act_correct]) 1);
 qed "lift_prog_correct";
 
@@ -212,7 +212,7 @@
 
 Goal "lift_set i UNIV = UNIV";
 by (simp_tac
-    (simpset() addsimps [lift_set_correct, lift_export extend_set_UNIV_eq]) 1);
+    (simpset() addsimps [lift_set_correct, lift_export0 extend_set_UNIV_eq]) 1);
 qed "lift_set_UNIV_eq";
 Addsimps [lift_set_UNIV_eq];
 
@@ -220,7 +220,7 @@
 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);
+			 lift_act_correct, lift_export0 extend_act_inverse]) 1);
 qed "lift_act_inverse";
 Addsimps [lift_act_inverse];
 *)
@@ -228,13 +228,13 @@
 Goal "UNIV <= drop_set i C ==> drop_prog i C (lift_prog i F) = F";
 by (asm_full_simp_tac
     (simpset() addsimps [drop_set_correct, drop_prog_correct, 
-			 lift_prog_correct, lift_export extend_inverse]) 1);
+			 lift_prog_correct, lift_export0 extend_inverse]) 1);
 qed "lift_prog_inverse";
 Addsimps [lift_prog_inverse];
 
 Goal "inj (lift_prog i)";
 by (simp_tac
-    (simpset() addsimps [lift_prog_correct, lift_export inj_extend]) 1);
+    (simpset() addsimps [lift_prog_correct, lift_export0 inj_extend]) 1);
 qed "inj_lift_prog";
 
 
@@ -242,7 +242,7 @@
 
 Goal "lift_act i act ^^ lift_set i A = lift_set i (act^^A)";
 by (asm_simp_tac (simpset() addsimps [lift_set_correct, lift_act_correct,
-				      lift_export extend_act_Image]) 1);
+				      lift_export0 extend_act_Image]) 1);
 qed "lift_act_Image";
 Addsimps [lift_act_Image];
 
@@ -272,7 +272,7 @@
 \     ==> F : (drop_set i A) co (drop_set i B)";
 by (asm_full_simp_tac
     (simpset() addsimps [drop_set_correct, lift_prog_correct, 
-			 lift_export extend_constrains_project_set]) 1);
+			 lift_export0 extend_constrains_project_set]) 1);
 qed "lift_prog_constrains_drop_set";
 
 (*This one looks strange!  Proof probably is by case analysis on i=j.
@@ -292,7 +292,7 @@
 \     (F : (C Int lift_set i A) co (lift_set i B) & A <= B)";
 by (simp_tac
     (simpset() addsimps [drop_prog_correct, 
-			 lift_set_correct, lift_export project_constrains]) 1);
+			 lift_set_correct, lift_export0 project_constrains]) 1);
 qed "drop_prog_constrains";
 
 Goal "(drop_prog i UNIV F : stable A)  =  (F : stable (lift_set i A))";
@@ -307,14 +307,14 @@
 Goal "reachable (lift_prog i F) = lift_set i (reachable F)";
 by (simp_tac
     (simpset() addsimps [lift_prog_correct, lift_set_correct, 
-			 lift_export reachable_extend_eq]) 1);
+			 lift_export0 reachable_extend_eq]) 1);
 qed "reachable_lift_prog";
 
 Goal "(lift_prog i F : (lift_set i A) Co (lift_set i B))  =  \
 \     (F : A Co B)";
 by (simp_tac
     (simpset() addsimps [lift_prog_correct, lift_set_correct, 
-			 lift_export extend_Constrains]) 1);
+			 lift_export0 extend_Constrains]) 1);
 qed "lift_prog_Constrains";
 
 Goal "(lift_prog i F : Stable (lift_set i A)) = (F : Stable A)";
@@ -326,7 +326,7 @@
 \     ==> lift_prog i F Join G : (lift_set i A) Co (lift_set i B)";
 by (asm_full_simp_tac
     (simpset() addsimps [lift_prog_correct, drop_prog_correct, 
-		     lift_set_correct, lift_export project_Constrains_D]) 1);
+		     lift_set_correct, lift_export0 project_Constrains_D]) 1);
 qed "drop_prog_Constrains_D";
 
 Goalw [Stable_def]
@@ -341,7 +341,7 @@
 \     ==> lift_prog i F Join G : Always (lift_set i A)";
 by (asm_full_simp_tac
     (simpset() addsimps [lift_prog_correct, drop_prog_correct, 
-		     lift_set_correct, lift_export project_Always_D]) 1);
+		     lift_set_correct, lift_export0 project_Always_D]) 1);
 qed "drop_prog_Always_D";
 
 Goalw [Increasing_def]
@@ -359,7 +359,7 @@
 \     ==> drop_prog i C ((lift_prog i F) Join G) = F Join (drop_prog i C G)";
 by (asm_full_simp_tac
     (simpset() addsimps [lift_prog_correct, drop_prog_correct, 
-		     drop_set_correct, lift_export project_extend_Join]) 1);
+		     drop_set_correct, lift_export0 project_extend_Join]) 1);
 qed "drop_prog_lift_prog_Join";
 
 
@@ -367,7 +367,7 @@
 
 Goal "(lift_prog i F : transient (lift_set i A)) = (F : transient A)";
 by (simp_tac (simpset() addsimps [lift_set_correct, lift_prog_correct,
-			  lift_export extend_transient]) 1);
+			  lift_export0 extend_transient]) 1);
 qed "lift_prog_transient";
 
 Goal "(lift_prog i F : transient (lift_set j A)) = \
@@ -384,7 +384,7 @@
 Goal "lift_prog i F : preserves (v o sub j) = \
 \     (if i=j then F : preserves v else True)";
 by (simp_tac (simpset() addsimps [lift_prog_correct,
-				  lift_export extend_preserves]) 1);
+				  lift_export0 extend_preserves]) 1);
 by (auto_tac (claset(),
 	      simpset() addsimps [preserves_def, extend_def, extend_act_def, 
 				  stable_def, constrains_def, lift_map_def]));
@@ -395,20 +395,21 @@
 Goal "G : preserves (v o sub i) ==> drop_prog i C G : preserves v";
 by (asm_simp_tac
     (simpset() addsimps [drop_prog_correct, fold_o_sub,
-			 lift_export project_preserves_I]) 1);
+			 lift_export0 project_preserves_I]) 1);
 qed "drop_prog_preserves_I";
 
 (*The raw version*)
 val [xguary,drop_prog,lift_prog] =
 Goal "[| F : X guarantees[v] Y;  \
-\        !!G. lift_prog i F Join G : X' ==> F Join drop_prog i C G : X;  \
-\        !!G. [| F Join drop_prog i C G : Y; lift_prog i F Join G : X' |] \
+\        !!G. lift_prog i F Join G : X' ==> F Join drop_prog i (C G) G : X;  \
+\        !!G. [| F Join drop_prog i (C G) G : Y; lift_prog i F Join G : X'; \
+\                G : preserves (v o sub i) |] \
 \             ==> lift_prog i F Join G : Y' |] \
 \     ==> lift_prog i F : X' guarantees[v o sub i] Y'";
 by (rtac (xguary RS guaranteesD RS lift_prog RS guaranteesI) 1);
 by (etac drop_prog_preserves_I 1);
 by (etac drop_prog 1);
-by (assume_tac 1);
+by Auto_tac;
 qed "drop_prog_guarantees_raw";
 
 Goal "[| F : X guarantees[v] Y;  \
@@ -418,7 +419,7 @@
 \     ==> lift_prog i F : X' guarantees[w] Y'";
 by (asm_simp_tac
     (simpset() addsimps [lift_prog_correct, fold_o_sub,
-			 lift_export project_guarantees]) 1);
+			 lift_export0 project_guarantees]) 1);
 qed "drop_prog_guarantees";
 
 
@@ -443,13 +444,13 @@
 
 Goal "F : UNIV guarantees[v] increasing func \
 \   ==> lift_prog i F : UNIV guarantees[v o sub i] increasing (func o sub i)";
-by (dtac (lift_export extend_guar_increasing) 1);
+by (dtac (lift_export0 extend_guar_increasing) 1);
 by (asm_full_simp_tac (simpset() addsimps [lift_prog_correct, o_def]) 1);
 qed "lift_prog_guar_increasing";
 
 Goal "F : UNIV guarantees[v] Increasing func \
 \   ==> lift_prog i F : UNIV guarantees[v o sub i] Increasing (func o sub i)";
-by (dtac (lift_export extend_guar_Increasing) 1);
+by (dtac (lift_export0 extend_guar_Increasing) 1);
 by (asm_full_simp_tac (simpset() addsimps [lift_prog_correct, o_def]) 1);
 qed "lift_prog_guar_Increasing";
 
@@ -458,5 +459,16 @@
 \       Always(lift_set i A) guarantees[v o sub i] Always (lift_set i B)";
 by (asm_simp_tac
     (simpset() addsimps [lift_set_correct, lift_prog_correct, 
-			 lift_export extend_guar_Always]) 1);
+			 lift_export0 extend_guar_Always]) 1);
 qed "lift_prog_guar_Always";
+
+(*version for outside use*)
+fun lift_export th = 
+    good_map_lift_map RS export th 
+       |> simplify
+             (simpset() addsimps [fold_o_sub, 
+				  drop_set_correct RS sym, 
+				  lift_set_correct RS sym, 
+				  drop_prog_correct RS sym, 
+				  lift_prog_correct RS sym]);;
+
diff -r 4a53041acb28 -r b43ad07660b9 src/HOL/UNITY/Lift_prog.thy
--- a/src/HOL/UNITY/Lift_prog.thy	Thu Jan 13 17:29:04 2000 +0100
+++ b/src/HOL/UNITY/Lift_prog.thy	Thu Jan 13 17:30:23 2000 +0100
@@ -6,7 +6,7 @@
 lift_prog, etc: replication of components
 *)
 
-Lift_prog = ELT +
+Lift_prog = Project +
 
 constdefs
 
diff -r 4a53041acb28 -r b43ad07660b9 src/HOL/UNITY/Project.ML
--- a/src/HOL/UNITY/Project.ML	Thu Jan 13 17:29:04 2000 +0100
+++ b/src/HOL/UNITY/Project.ML	Thu Jan 13 17:30:23 2000 +0100
@@ -10,6 +10,12 @@
 POSSIBLY CAN DELETE Restrict_image_Diff
 *)
 
+(*EQUALITIES.ML*)
+		Goal "(A <= -A) = (A = {})";
+		by (Blast_tac 1);
+		qed "subset_Compl_self_eq";
+
+
 Open_locale "Extend";
 
 (** projection: monotonicity for safety **)
@@ -137,7 +143,34 @@
 			 extend_constrains]) 1);
 qed "project_constrains_D";
 
-(** "projecting" and union/intersection (no converses) **)
+
+(*** preserves ***)
+
+Goal "G : preserves (v o f) ==> project h C G : preserves v";
+by (auto_tac (claset(),
+	      simpset() addsimps [preserves_def, project_stable_I,
+				  Collect_eq_extend_set RS sym]));
+qed "project_preserves_I";
+
+(*to preserve f is to preserve the whole original state*)
+Goal "G : preserves f ==> project h C G : preserves id";
+by (asm_simp_tac (simpset() addsimps [project_preserves_I]) 1);
+qed "project_preserves_id_I";
+
+Goal "(extend h G : preserves (v o f)) = (G : preserves v)";
+by (auto_tac (claset(),
+	      simpset() addsimps [preserves_def, extend_stable RS sym,
+				  Collect_eq_extend_set RS sym]));
+qed "extend_preserves";
+
+Goal "inj h ==> (extend h G : preserves g)";
+by (auto_tac (claset(),
+	      simpset() addsimps [preserves_def, extend_def, extend_act_def, 
+				  stable_def, constrains_def, g_def]));
+qed "inj_extend_preserves";
+
+
+(*** "projecting" and union/intersection (no converses) ***)
 
 Goalw [projecting_def]
      "[| projecting C h F XA' XA;  projecting C h F XB' XB |] \
@@ -446,7 +479,7 @@
 qed "extending_Increasing";
 
 
-(*** leadsETo in the precondition ***)
+(*** leadsETo in the precondition (??) ***)
 
 (** transient **)
 
@@ -533,7 +566,8 @@
 				  Join_stable, Join_transient]));
 qed_spec_mp "Join_project_ensures";
 
-(** Lemma useful for both STRONG and WEAK progress*)
+(** Lemma useful for both STRONG and WEAK progress, but the transient
+    condition's very strong **)
 
 (*The strange induction formula allows induction over the leadsTo
   assumption's non-atomic precondition*)
@@ -568,32 +602,91 @@
 qed "Join_project_LeadsTo";
 
 
-(*** GUARANTEES and EXTEND ***)
+(*** Towards project_Ensures_D ***)
+
+
 
-(** preserves **)
+Goalw [project_set_def, extend_set_def, project_act_def]
+     "act ^^ (C Int extend_set h A) <= B \
+\     ==> project_act h (Restrict C act) ^^ (project_set h C Int A) \
+\         <= project_set h B";
+by (Blast_tac 1);
+qed "act_subset_imp_project_act_subset";
+
 
-Goal "G : preserves (v o f) ==> project h C G : preserves v";
-by (auto_tac (claset(),
-	      simpset() addsimps [preserves_def, project_stable_I,
-				  Collect_eq_extend_set RS sym]));
-qed "project_preserves_I";
+Goal "[| G : stable ((C Int extend_set h A) - (extend_set h B));  \
+\        project h C G : transient (project_set h C Int A - B) |]  \
+\     ==> G : transient (C Int extend_set h A - extend_set h B)";
+by (case_tac "C Int extend_set h A <= extend_set h B" 1);
+by (asm_simp_tac (simpset() addsimps [Diff_eq_empty_iff RS iffD2]) 1);
+by (auto_tac (claset(), 
+	      simpset() addsimps [transient_def, subset_Compl_self_eq,
+				  Domain_project_act, split_extended_all]));
+by (Blast_tac 1);
+by (auto_tac (claset(), 
+	      simpset() addsimps [stable_def, constrains_def]));
+by (ball_tac 1);
+by (thin_tac "ALL act: Acts G. ?P act" 1);
+by (auto_tac (claset(), 
+	      simpset() addsimps [Int_Diff,
+				  extend_set_Diff_distrib RS sym]));
+bd act_subset_imp_project_act_subset 1;
+by (subgoal_tac
+    "project_act h (Restrict C act) ^^ (project_set h C Int (A - B)) <= {}" 1);
+bws [Restrict_def, project_set_def, extend_set_def, project_act_def];
+(*using Int_greatest actually slows the next step!*)
+by (Blast_tac 2);
+by (force_tac (claset(), 
+	      simpset() addsimps [split_extended_all]) 1);
+qed "stable_project_transient";
+
 
-(*to preserve f is to preserve the whole original state*)
-Goal "G : preserves f ==> project h C G : preserves id";
-by (asm_simp_tac (simpset() addsimps [project_preserves_I]) 1);
-qed "project_preserves_id_I";
+Goal "[| G : stable C;  project h C G : (project_set h C Int A) unless B |] \
+\     ==> G : (C Int extend_set h A) unless (extend_set h B)";
+by (auto_tac
+    (claset() addDs [stable_constrains_Int]
+              addIs [constrains_weaken],
+     simpset() addsimps [unless_def, project_constrains, Diff_eq, 
+			 Int_assoc, Int_extend_set_lemma]));
+qed_spec_mp "project_unless2";
 
-Goal "(extend h G : preserves (v o f)) = (G : preserves v)";
-by (auto_tac (claset(),
-	      simpset() addsimps [preserves_def, extend_stable RS sym,
-				  Collect_eq_extend_set RS sym]));
-qed "extend_preserves";
+Goal "[| G : stable ((C Int extend_set h A) - (extend_set h B));  \
+\        F Join project h C G : (project_set h C Int A) ensures B;  \
+\        extend h F Join G : stable C |] \
+\     ==> extend h F Join G : (C Int extend_set h A) ensures (extend_set h B)";
+(*unless*)
+by (auto_tac (claset() addSIs [rewrite_rule [unless_def] project_unless2] 
+                       addIs [project_extend_constrains_I], 
+	      simpset() addsimps [ensures_def, Join_constrains,
+				  Join_stable]));
+(*transient*)
+by (auto_tac (claset(), simpset() addsimps [Join_transient]));
+by (blast_tac (claset() addIs [stable_project_transient]) 2);
+by (force_tac (claset() addSEs [extend_transient RS iffD2 RS 
+				transient_strengthen], 
+	       simpset() addsimps [Join_transient, split_extended_all]) 1);
+qed "project_ensures_D_lemma";
 
-Goal "inj h ==> (extend h G : preserves g)";
-by (auto_tac (claset(),
-	      simpset() addsimps [preserves_def, extend_def, extend_act_def, 
-				  stable_def, constrains_def, g_def]));
-qed "inj_extend_preserves";
+Goal "[| F Join project h UNIV G : A ensures B;  \
+\        G : stable (extend_set h A - extend_set h B) |] \
+\     ==> extend h F Join G : (extend_set h A) ensures (extend_set h B)";
+br (project_ensures_D_lemma RS revcut_rl) 1;
+by (stac stable_UNIV 3);
+auto();
+qed "project_ensures_D";
+
+Goalw [Ensures_def]
+     "[| F Join project h (reachable (extend h F Join G)) G : A Ensures B;  \
+\        G : stable (reachable (extend h F Join G) Int extend_set h A - \
+\                    extend_set h B) |] \
+\     ==> extend h F Join G : (extend_set h A) Ensures (extend_set h B)";
+br (project_ensures_D_lemma RS revcut_rl) 1;
+by (auto_tac (claset(), 
+	      simpset() addsimps [project_set_reachable_extend_eq RS sym]));
+qed "project_Ensures_D";
+
+
+(*** GUARANTEES and EXTEND ***)
 
 (** Strong precondition and postcondition; doesn't seem very useful. **)
 
@@ -630,14 +723,15 @@
 (*The raw version*)
 val [xguary,project,extend] =
 Goal "[| F : X guarantees[v] Y;  \
-\        !!G. extend h F Join G : X' ==> F Join project h C G : X;  \
-\        !!G. [| F Join project h C G : Y; extend h F Join G : X' |] \
+\        !!G. extend h F Join G : X' ==> F Join project h (C G) G : X;  \
+\        !!G. [| F Join project h (C G) G : Y; extend h F Join G : X'; \
+\                G : preserves (v o f) |] \
 \             ==> extend h F Join G : Y' |] \
 \     ==> extend h F : X' guarantees[v o f] Y'";
 by (rtac (xguary RS guaranteesD RS extend RS guaranteesI) 1);
 by (etac project_preserves_I 1);
 by (etac project 1);
-by (assume_tac 1);
+by Auto_tac;
 qed "project_guarantees_raw";
 
 Goal "[| F : X guarantees[v] Y;  \
diff -r 4a53041acb28 -r b43ad07660b9 src/HOL/UNITY/SubstAx.ML
--- a/src/HOL/UNITY/SubstAx.ML	Thu Jan 13 17:29:04 2000 +0100
+++ b/src/HOL/UNITY/SubstAx.ML	Thu Jan 13 17:30:23 2000 +0100
@@ -157,24 +157,28 @@
 
 (** More rules using the premise "Always INV" **)
 
-Goal "[| F : (A-A') Co (A Un A');  F : transient (A-A') |]   \
-\     ==> F : A LeadsTo A'";
+Goal "F : A Ensures B ==> F : A LeadsTo B";
 by (asm_full_simp_tac
-    (simpset() addsimps [LeadsTo_def, Constrains_eq_constrains]) 1);
-by (rtac (ensuresI RS leadsTo_Basis) 1);
-by (blast_tac (claset() addIs [transient_strengthen]) 2);
-by (blast_tac (claset() addIs [constrains_weaken]) 1);
+    (simpset() addsimps [Ensures_def, LeadsTo_def, leadsTo_Basis]) 1);
 qed "LeadsTo_Basis";
 
+Goal "[| F : (A-B) Co (A Un B);  F : transient (A-B) |]   \
+\     ==> F : A Ensures B";
+by (asm_full_simp_tac
+    (simpset() addsimps [Ensures_def, Constrains_eq_constrains]) 1);
+by (blast_tac (claset() addIs [ensuresI, constrains_weaken, 
+			       transient_strengthen]) 1);
+qed "EnsuresI";
+
 Goal "[| F : Always INV;      \
 \        F : (INV Int (A-A')) Co (A Un A'); \
 \        F : transient (INV Int (A-A')) |]   \
 \ ==> F : A LeadsTo A'";
 by (rtac Always_LeadsToI 1);
 by (assume_tac 1);
-by (rtac LeadsTo_Basis 1);
-by (blast_tac (claset() addIs [transient_strengthen]) 2);
-by (blast_tac (claset() addIs [Always_ConstrainsD RS Constrains_weaken]) 1);
+by (blast_tac (claset() addIs [EnsuresI, LeadsTo_Basis,
+			       Always_ConstrainsD RS Constrains_weaken, 
+			       transient_strengthen]) 1);
 qed "Always_LeadsTo_Basis";
 
 (*Set difference: maybe combine with leadsTo_weaken_L??
@@ -420,7 +424,7 @@
 	      etac Always_LeadsTo_Basis 1 
 	          ORELSE   (*subgoal may involve LeadsTo, leadsTo or ensures*)
 		  REPEAT (ares_tac [LeadsTo_Basis, leadsTo_Basis,
-				    ensuresI] 1),
+				    EnsuresI, ensuresI] 1),
 	      (*now there are two subgoals: co & transient*)
 	      simp_tac (simpset() addsimps !program_defs_ref) 2,
 	      res_inst_tac [("act", sact)] transientI 2,
diff -r 4a53041acb28 -r b43ad07660b9 src/HOL/UNITY/SubstAx.thy
--- a/src/HOL/UNITY/SubstAx.thy	Thu Jan 13 17:29:04 2000 +0100
+++ b/src/HOL/UNITY/SubstAx.thy	Thu Jan 13 17:30:23 2000 +0100
@@ -9,6 +9,9 @@
 SubstAx = WFair + Constrains + 
 
 constdefs
+   Ensures :: "['a set, 'a set] => 'a program set"            (infixl 60)
+    "A Ensures B == {F. F : (reachable F Int A) ensures B}"
+
    LeadsTo :: "['a set, 'a set] => 'a program set"            (infixl 60)
     "A LeadsTo B == {F. F : (reachable F Int A) leadsTo B}"
 
diff -r 4a53041acb28 -r b43ad07660b9 src/HOL/UNITY/Union.ML
--- a/src/HOL/UNITY/Union.ML	Thu Jan 13 17:29:04 2000 +0100
+++ b/src/HOL/UNITY/Union.ML	Thu Jan 13 17:30:23 2000 +0100
@@ -181,6 +181,10 @@
      simpset() addsimps [constrains_def, Join_def]));
 qed "Join_constrains";
 
+Goal "(F Join G : A unless B) = (F : A unless B & G : A unless B)";
+by (simp_tac (simpset() addsimps [Join_constrains, unless_def]) 1);
+qed "Join_unless";
+
 (*Analogous weak versions FAIL; see Misra [1994] 5.4.1, Substitution Axiom.
   reachable (F Join G) could be much bigger than reachable F, reachable G
 *)
diff -r 4a53041acb28 -r b43ad07660b9 src/HOL/UNITY/WFair.ML
--- a/src/HOL/UNITY/WFair.ML	Thu Jan 13 17:29:04 2000 +0100
+++ b/src/HOL/UNITY/WFair.ML	Thu Jan 13 17:30:23 2000 +0100
@@ -79,12 +79,15 @@
 by (blast_tac (claset() addIs [stable_constrains_Int, constrains_weaken]) 1);
 qed "stable_ensures_Int";
 
-(*NEVER USED*)
 Goal "[| F : stable A;  F : transient C;  A <= B Un C |] ==> F : A ensures B";
 by (asm_full_simp_tac (simpset() addsimps [ensures_def, stable_def]) 1);
 by (blast_tac (claset() addIs [constrains_weaken, transient_strengthen]) 1);
 qed "stable_transient_ensures";
 
+Goal "(A ensures B) = (A unless B) Int transient (A-B)";
+by (simp_tac (simpset() addsimps [ensures_def, unless_def]) 1);
+qed "ensures_eq";
+
 
 (*** leadsTo ***)