working version, with Alloc now working on the same state space as the whole
authorpaulson
Thu Jan 13 17:30:23 2000 +0100 (2000-01-13)
changeset 8122b43ad07660b9
parent 8121 4a53041acb28
child 8123 a71686059be0
working version, with Alloc now working on the same state space as the whole
system. Partial removal of ELT.
src/HOL/UNITY/Alloc.ML
src/HOL/UNITY/Alloc.thy
src/HOL/UNITY/Comp.ML
src/HOL/UNITY/Comp.thy
src/HOL/UNITY/ELT.ML
src/HOL/UNITY/ELT.thy
src/HOL/UNITY/Extend.ML
src/HOL/UNITY/Follows.thy
src/HOL/UNITY/Guar.ML
src/HOL/UNITY/Lift_prog.ML
src/HOL/UNITY/Lift_prog.thy
src/HOL/UNITY/Project.ML
src/HOL/UNITY/SubstAx.ML
src/HOL/UNITY/SubstAx.thy
src/HOL/UNITY/Union.ML
src/HOL/UNITY/WFair.ML
     1.1 --- a/src/HOL/UNITY/Alloc.ML	Thu Jan 13 17:29:04 2000 +0100
     1.2 +++ b/src/HOL/UNITY/Alloc.ML	Thu Jan 13 17:30:23 2000 +0100
     1.3 @@ -23,10 +23,12 @@
     1.4  by (asm_full_simp_tac (simpset() addsimps [o_def]) 1);
     1.5  qed "sub_fold";
     1.6  
     1.7 -(*Splits up an intersection: like CONJUNCTS in the HOL system*)
     1.8 -fun list_of_Int th = (list_of_Int (th RS IntD1) @ list_of_Int (th RS IntD2))
     1.9 -                     handle THM _ => (list_of_Int (th RS INT_D))
    1.10 -                     handle THM _ => [th];
    1.11 +(*Splits up conjunctions & intersections: like CONJUNCTS in the HOL system*)
    1.12 +fun list_of_Int th = 
    1.13 +    (list_of_Int (th RS conjunct1) @ list_of_Int (th RS conjunct2))
    1.14 +    handle THM _ => (list_of_Int (th RS IntD1) @ list_of_Int (th RS IntD2))
    1.15 +    handle THM _ => (list_of_Int (th RS INT_D))
    1.16 +    handle THM _ => [th];
    1.17  
    1.18  (*useful??*)
    1.19  val lessThanBspec = lessThan_iff RS iffD2 RSN (2, bspec);
    1.20 @@ -75,17 +77,6 @@
    1.21  by (blast_tac (claset() addIs [tokens_mono_prefix]) 1);
    1.22  qed "mono_tokens";
    1.23  
    1.24 -(*Generalized version allowing different clients*)
    1.25 -Goal "[| Alloc : alloc_spec;  \
    1.26 -\        Client : (lessThan Nclients) funcset client_spec;  \
    1.27 -\        Network : network_spec |] \
    1.28 -\     ==> (extend sysOfAlloc Alloc) \
    1.29 -\         Join (extend sysOfClient (PLam (lessThan Nclients) Client)) \
    1.30 -\         Join Network : system_spec";
    1.31 -
    1.32 -Goal "System : system_spec";
    1.33 -
    1.34 -
    1.35  Goalw [sysOfAlloc_def] "inj sysOfAlloc";
    1.36  by (rtac injI 1);
    1.37  by (auto_tac (claset() addSWrapper record_split_wrapper, simpset()));
    1.38 @@ -206,15 +197,7 @@
    1.39  
    1.40  AddIffs  [Network_preserves_allocGiv];
    1.41  
    1.42 -
    1.43 -Goal "i < Nclients ==> Network : preserves (ask o sub i o client) & \
    1.44 -\                      Network : preserves (rel o sub i o client)";
    1.45 -by (rtac (Network_preserves_rel_ask RS revcut_rl) 1);
    1.46 -by (auto_tac (claset(), 
    1.47 -	      simpset() addsimps [funPair_o_distrib]));
    1.48 -qed "Network_preserves_rel_conj_ask";
    1.49 -
    1.50 -Addsimps [Network_preserves_rel_conj_ask];
    1.51 +Addsimps (Network_preserves_rel_ask |> simplify (simpset()) |> list_of_Int);
    1.52  
    1.53  
    1.54  (*Alloc : <unfolded specification> *)
    1.55 @@ -222,31 +205,41 @@
    1.56      rewrite_rule [alloc_spec_def, alloc_increasing_def, alloc_safety_def, 
    1.57  		  alloc_progress_def, alloc_preserves_def] Alloc;
    1.58  
    1.59 -val [Alloc_Increasing, Alloc_Safety, 
    1.60 +val [Alloc_Increasing_0, Alloc_Safety, 
    1.61       Alloc_Progress, Alloc_preserves] = list_of_Int Alloc_Spec;
    1.62  
    1.63 +(*Strip off the INT in the guarantees postcondition*)
    1.64 +val Alloc_Increasing = normalize Alloc_Increasing_0;
    1.65  
    1.66  fun alloc_export th = good_map_sysOfAlloc RS export th |> simplify (simpset());
    1.67  
    1.68  fun client_export th = good_map_sysOfClient RS export th |> simplify (simpset());
    1.69  
    1.70 -(*extend sysOfAlloc G : preserves client
    1.71 -  alloc_export isn't needed!*)
    1.72 -bind_thm ("extend_sysOfAlloc_preserves_client",
    1.73 -	  inj_sysOfAlloc RS export inj_extend_preserves  
    1.74 -	  |> simplify (simpset()));
    1.75 +AddIffs (Alloc_preserves |> simplify (simpset()) |> list_of_Int);
    1.76 +
    1.77 +(** Components lemmas **)
    1.78  
    1.79 -AddIffs [extend_sysOfAlloc_preserves_client];
    1.80 +(*Alternative is to say that System = Network Join F such that F preserves
    1.81 +  certain state variables*)
    1.82 +Goal "(extend sysOfClient (plam x: lessThan Nclients. Client)) Join \
    1.83 +\     (Network Join Alloc)  =  System";
    1.84 +by (simp_tac (simpset() addsimps System_def::Join_ac) 1);
    1.85 +qed "Client_component_System";
    1.86  
    1.87 -Goal "extend sysOfAlloc Alloc : preserves allocRel & \
    1.88 -\     extend sysOfAlloc Alloc : preserves allocAsk";
    1.89 -by (cut_facts_tac [Alloc_preserves] 1);
    1.90 -by (auto_tac (claset() addSDs [alloc_export extend_preserves RS iffD2],
    1.91 -	      simpset() addsimps [o_def]));
    1.92 -qed "extend_sysOfAlloc_preserves_Rel_Ask";
    1.93 +Goal "Network Join \
    1.94 +\     ((extend sysOfClient (plam x: lessThan Nclients. Client)) Join Alloc) \
    1.95 +\     = System";
    1.96 +by (simp_tac (simpset() addsimps System_def::Join_ac) 1);
    1.97 +qed "Network_component_System";
    1.98  
    1.99 -AddIffs [extend_sysOfAlloc_preserves_Rel_Ask RS conjunct1,
   1.100 -	 extend_sysOfAlloc_preserves_Rel_Ask RS conjunct2];
   1.101 +Goal "Alloc Join \
   1.102 +\      ((extend sysOfClient (plam x: lessThan Nclients. Client)) Join \
   1.103 +\       Network)  =  System";
   1.104 +by (simp_tac (simpset() addsimps System_def::Join_ac) 1);
   1.105 +qed "Alloc_component_System";
   1.106 +
   1.107 +AddIffs [Client_component_System, Network_component_System, 
   1.108 +	 Alloc_component_System];
   1.109  
   1.110  (** These preservation laws should be generated automatically **)
   1.111  
   1.112 @@ -282,68 +275,28 @@
   1.113  AddIffs [extend_sysOfClient_preserves_o_client];
   1.114  
   1.115  
   1.116 -(*NEED AUTOMATIC PROPAGATION of Alloc_Increasing
   1.117 -  (the form changes slightly, though, removing the INT) *)
   1.118 -Goal "i < Nclients \
   1.119 -\     ==> extend sysOfAlloc Alloc : \
   1.120 -\           UNIV guarantees[allocGiv] Increasing (sub i o allocGiv)";
   1.121 -(* Alternative is something like
   1.122 -by (dtac (Alloc_Increasing RS (guarantees_INT_right_iff RS iffD1)
   1.123 -          RS lessThanBspec RS alloc_export extend_guar_Increasing) 1);
   1.124 -*)
   1.125 -by (cut_facts_tac [Alloc_Increasing] 1);
   1.126 -by (auto_tac (claset() addSDs [alloc_export extend_guar_Increasing], 
   1.127 -	      simpset() addsimps [guarantees_INT_right_iff, o_def]));
   1.128 -qed "extend_Alloc_Increasing_allocGiv";
   1.129 -
   1.130 -
   1.131  Goalw [System_def]
   1.132       "i < Nclients ==> System : Increasing (sub i o allocGiv)";
   1.133 -by (rtac (extend_Alloc_Increasing_allocGiv RS 
   1.134 -	  guarantees_Join_I1 RS guaranteesD) 1);
   1.135 +by (rtac (Alloc_Increasing RS guarantees_Join_I1 RS guaranteesD) 1);
   1.136  by Auto_tac;
   1.137  qed "System_Increasing_allocGiv";
   1.138  
   1.139  
   1.140 -Goalw [System_def]
   1.141 -     "i < Nclients ==> System : Increasing (ask o sub i o client)";
   1.142 -by (rtac (client_export extend_guar_Increasing RS guarantees_Join_I2 
   1.143 -	  RS guaranteesD) 1);
   1.144 +Goal "i < Nclients ==> System : Increasing (ask o sub i o client)";
   1.145 +by (rtac ([client_export extend_guar_Increasing,
   1.146 +	   Client_component_System] MRS component_guaranteesD) 1);
   1.147  by (rtac (lift_prog_guar_Increasing RS guarantees_PLam_I) 1);
   1.148 -by (auto_tac (claset(), 
   1.149 -	      simpset() addsimps [Network_preserves_rel_ask]));
   1.150 +by Auto_tac;
   1.151  qed "System_Increasing_ask";
   1.152  
   1.153 -Goalw [System_def]
   1.154 -     "i < Nclients ==> System : Increasing (rel o sub i o client)";
   1.155 -by (rtac (client_export extend_guar_Increasing RS guarantees_Join_I2 
   1.156 -	  RS guaranteesD) 1);
   1.157 +Goal "i < Nclients ==> System : Increasing (rel o sub i o client)";
   1.158 +by (rtac ([client_export extend_guar_Increasing,
   1.159 +	   Client_component_System] MRS component_guaranteesD) 1);
   1.160  by (rtac (lift_prog_guar_Increasing RS guarantees_PLam_I) 1);
   1.161  (*gets Client_Increasing_rel from simpset*)
   1.162 -by (auto_tac (claset(), 
   1.163 -	      simpset() addsimps [Network_preserves_rel_ask]));
   1.164 +by Auto_tac;
   1.165  qed "System_Increasing_rel";
   1.166  
   1.167 -(** Components lemmas **)
   1.168 -
   1.169 -(*Alternative is to say that System = Network Join F such that F preserves
   1.170 -  certain state variables*)
   1.171 -Goal "Network Join \
   1.172 -\     ((extend sysOfClient (plam x: lessThan Nclients. Client)) Join \
   1.173 -\      (extend sysOfAlloc Alloc)) \
   1.174 -\     = System";
   1.175 -by (simp_tac (simpset() addsimps System_def::Join_ac) 1);
   1.176 -qed "Network_component_System";
   1.177 -
   1.178 -Goal "(extend sysOfAlloc Alloc) Join \
   1.179 -\      ((extend sysOfClient (plam x: lessThan Nclients. Client)) Join \
   1.180 -\       Network) \
   1.181 -\     = System";
   1.182 -by (simp_tac (simpset() addsimps System_def::Join_ac) 1);
   1.183 -qed "Alloc_component_System";
   1.184 -
   1.185 -AddIffs [Network_component_System, Alloc_component_System];
   1.186 -
   1.187  (** Follows consequences.
   1.188      The "Always (INT ...) formulation expresses the general safety property
   1.189      and allows it to be combined using Always_Int_rule below. **)
   1.190 @@ -365,7 +318,7 @@
   1.191  Goal
   1.192    "i < Nclients ==> System : (giv o sub i o client) Fols (sub i o allocGiv)";
   1.193  by (auto_tac (claset() addSIs [Network_Giv RS component_guaranteesD, 
   1.194 -		 extend_Alloc_Increasing_allocGiv RS component_guaranteesD], 
   1.195 +		 Alloc_Increasing RS component_guaranteesD], 
   1.196  	      simpset()));
   1.197  qed "System_Follows_allocGiv";
   1.198  
   1.199 @@ -399,28 +352,10 @@
   1.200  by (etac (System_Follows_rel RS Follows_Increasing1) 1);
   1.201  qed "System_Increasing_allocRel";
   1.202  
   1.203 -(*NEED AUTOMATIC PROPAGATION of Alloc_Safety.  The text is identical.*)
   1.204 -Goal "extend sysOfAlloc Alloc :  \
   1.205 -\  (INT i : lessThan Nclients. Increasing (sub i o allocRel))  \
   1.206 -\  guarantees[allocGiv]  \
   1.207 -\    Always {s. sum (%i. (tokens o sub i o allocGiv) s) Nclients  \
   1.208 -\               <= NbT + sum (%i. (tokens o sub i o allocRel) s) Nclients}";
   1.209 -by (rtac (Alloc_Safety RS alloc_export project_guarantees) 1);
   1.210 -(*2: Always postcondition*)
   1.211 -by (rtac (alloc_export extending_Always RS extending_weaken_L) 2);
   1.212 -(*1: Increasing precondition*)
   1.213 -by (rtac (alloc_export projecting_Increasing RS projecting_weaken_L RS 
   1.214 -	  projecting_INT) 1);
   1.215 -by (auto_tac (claset(),
   1.216 -	      simpset() addsimps [alloc_export Collect_eq_extend_set RS sym,
   1.217 -				  o_def]));
   1.218 -qed "extend_Alloc_Safety";
   1.219 -
   1.220  (*safety (1), step 3*)
   1.221  Goal "System : Always {s. sum (%i. (tokens o sub i o allocGiv) s) Nclients \
   1.222  \                  <= NbT + sum (%i. (tokens o sub i o allocRel) s) Nclients}";
   1.223 -by (rtac (extend_Alloc_Safety RS component_guaranteesD) 1);
   1.224 -by (rtac Alloc_component_System 2);
   1.225 +by (rtac ([Alloc_Safety, Alloc_component_System] MRS component_guaranteesD) 1);
   1.226  (*preserves*)
   1.227  by (asm_full_simp_tac (simpset() addsimps [o_def]) 2);
   1.228  by (force_tac (claset(), simpset() addsimps [System_Increasing_allocRel]) 1);
   1.229 @@ -484,12 +419,12 @@
   1.230  
   1.231  (*progress (2), step 3*)
   1.232  (*All this trouble just to lift "Client_Bounded" through two extend ops*)
   1.233 -Goalw [System_def]
   1.234 -     "i < Nclients \
   1.235 -\   ==> System : Always \
   1.236 -\                 {s. ALL elt : set ((ask o sub i o client) s). elt <= NbT}";
   1.237 -by (rtac (guarantees_PLam_I RS client_export UNIV_guar_Always RS
   1.238 -	  guarantees_Join_I2 RS guaranteesD RS Always_weaken) 1);
   1.239 +Goal "i < Nclients \
   1.240 +\     ==> System : Always \
   1.241 +\                   {s. ALL elt : set ((ask o sub i o client) s). elt <= NbT}";
   1.242 +br Always_weaken 1;
   1.243 +by (rtac ([guarantees_PLam_I RS client_export UNIV_guar_Always,
   1.244 +	   Client_component_System] MRS component_guaranteesD) 1);
   1.245  by (rtac Client_i_Bounded 1);
   1.246  by (auto_tac(claset(),
   1.247  	 simpset() addsimps [o_apply, lift_export Collect_eq_extend_set RS sym,
   1.248 @@ -516,48 +451,126 @@
   1.249  	      simpset()));
   1.250  qed "System_Increasing_giv";
   1.251  
   1.252 -(*Lemma.  A LOT of work just to lift "Client_Progress" to the array*)
   1.253 +(** A LOT of work just to lift "Client_Progress" to the array **)
   1.254 +
   1.255 +(*stability lemma for G*)
   1.256 +Goalw [preserves_def, o_def, stable_def, constrains_def, sub_def]
   1.257 +     "[| ALL z. G : stable      \
   1.258 +\                   (reachable (lift_prog i Client Join G) Int      \
   1.259 +\                    {s. z <= (giv o sub i) s});      \
   1.260 +\         G : preserves (rel o sub i);  G : preserves (ask o sub i) |]      \
   1.261 +\      ==> G : stable      \
   1.262 +\               (reachable (lift_prog i Client Join G) Int      \
   1.263 +\                {s. h <= (giv o sub i) s & h pfixGe (ask o sub i) s} -      \
   1.264 +\                {s. tokens h <= tokens ((rel o sub i) s)})";
   1.265 +auto();
   1.266 +by (REPEAT (dres_inst_tac [("x", "rel (xa i)")] spec 2));
   1.267 +by (REPEAT (dres_inst_tac [("x", "ask (xa i)")] spec 1));
   1.268 +by (REPEAT_FIRST ball_tac);
   1.269 +auto();
   1.270 +qed "G_stable_lift_prog";
   1.271 +
   1.272  Goal "lift_prog i Client \
   1.273  \        : Increasing (giv o sub i)  \
   1.274  \          guarantees[funPair rel ask o sub i] \
   1.275  \          (INT h. {s. h <=  (giv o sub i) s & \
   1.276  \                             h pfixGe (ask o sub i) s}  \
   1.277 -\                  LeadsTo[givenBy (funPair rel ask o sub i)] \
   1.278 -\                  {s. tokens h <= (tokens o rel o sub i) s})";
   1.279 -by (rtac (Client_Progress RS drop_prog_guarantees) 1);
   1.280 -by (rtac (lift_export extending_LeadsETo RS extending_weaken_L RS
   1.281 -	  extending_INT) 2);
   1.282 -by (asm_simp_tac (simpset() addsimps [lift_export Collect_eq_extend_set RS sym,
   1.283 -				  sub_def, o_def]) 2);
   1.284 -by (rtac (lift_export projecting_Increasing) 1);
   1.285 -by (auto_tac (claset(), simpset() addsimps [o_def]));
   1.286 +\                  Ensures {s. tokens h <= (tokens o rel o sub i) s})";
   1.287 +by (rtac (Client_Progress RS drop_prog_guarantees_raw) 1);
   1.288 +br (lift_export (subset_refl RS project_Increasing_I)) 1;
   1.289 +by (full_simp_tac (simpset() addsimps [fold_o_sub, lift_prog_correct]) 1);
   1.290 +br INT_I 1;
   1.291 +by (simp_tac (simpset() addsimps [o_apply]) 1);
   1.292 +by (REPEAT (stac (lift_export Collect_eq_extend_set) 1));
   1.293 +br (lift_export project_Ensures_D) 1;
   1.294 +by (asm_full_simp_tac (simpset() addsimps [o_apply, lift_prog_correct, 
   1.295 +					   drop_prog_correct]) 1);
   1.296 +by (asm_full_simp_tac
   1.297 +    (simpset() addsimps [all_conj_distrib,
   1.298 +			 Increasing_def, Stable_eq_stable, Join_stable,
   1.299 +			 lift_set_correct RS sym,
   1.300 +			 Collect_eq_lift_set RS sym,
   1.301 +			 lift_prog_correct RS sym]) 1);
   1.302 +by (Clarify_tac 1);
   1.303 +bd G_stable_lift_prog 1;
   1.304 +by (auto_tac (claset(), 
   1.305 +	      simpset() addsimps [o_apply]));
   1.306  qed "Client_i_Progress";
   1.307  
   1.308 +Goal "i < Nclients \
   1.309 +\   ==> (plam x: lessThan Nclients. Client) \
   1.310 +\        : Increasing (giv o sub i)  \
   1.311 +\          guarantees[funPair rel ask o sub i] \
   1.312 +\          (INT h. {s. h <=  (giv o sub i) s & \
   1.313 +\                             h pfixGe (ask o sub i) s}  \
   1.314 +\                  Ensures {s. tokens h <= (tokens o rel o sub i) s})";
   1.315 +by (rtac guarantees_PLam_I 1);
   1.316 +br Client_i_Progress 1;
   1.317 +by Auto_tac;
   1.318 +val lemma2 = result();
   1.319 +
   1.320 +(*another stability lemma for G*)
   1.321 +Goalw [preserves_def, o_def, stable_def, constrains_def, sub_def]
   1.322 +     "[| ALL z. G : stable      \
   1.323 +\                  (reachable (extend sysOfClient  \
   1.324 +\                              (plam x:lessThan Nclients. Client) Join G) Int \
   1.325 +\                    {s. z <= (giv o sub i o client) s});      \
   1.326 +\         G : preserves (rel o sub i o client);  \
   1.327 +\         G : preserves (ask o sub i o client) |]      \
   1.328 +\ ==> G : stable      \
   1.329 +\          (reachable (extend sysOfClient  \
   1.330 +\                      (plam x:lessThan Nclients. Client) Join G) Int \
   1.331 +\           {s. h <= (giv o sub i o client) s & \
   1.332 +\               h pfixGe (ask o sub i o client) s} - \
   1.333 +\           {s. tokens h <= tokens ((rel o sub i o client) s)})";
   1.334 +auto();
   1.335 +by (REPEAT (dres_inst_tac [("x", "rel (client xa i)")] spec 2));
   1.336 +by (REPEAT (dres_inst_tac [("x", "ask (client xa i)")] spec 1));
   1.337 +by (REPEAT_FIRST ball_tac);
   1.338 +auto();
   1.339 +qed "G_stable_sysOfClient";
   1.340 +
   1.341 +Goal "i < Nclients \
   1.342 +\  ==> extend sysOfClient (plam x: lessThan Nclients. Client) \
   1.343 +\       : Increasing (giv o sub i o client)  \
   1.344 +\         guarantees[funPair rel ask o sub i o client] \
   1.345 +\         (INT h. {s. h <=  (giv o sub i o client) s & \
   1.346 +\                            h pfixGe (ask o sub i o client) s}  \
   1.347 +\                 Ensures {s. tokens h <= (tokens o rel o sub i o client) s})";
   1.348 +by (rtac (lemma2 RS client_export project_guarantees_raw) 1);
   1.349 +ba 1;
   1.350 +br (client_export (subset_refl RS project_Increasing_I)) 1;
   1.351 +by (Simp_tac 1);
   1.352 +br INT_I 1;
   1.353 +by (simp_tac (simpset() addsimps [o_apply]) 1);
   1.354 +by (REPEAT (stac (client_export Collect_eq_extend_set) 1));
   1.355 +br (client_export project_Ensures_D) 1;
   1.356 +by (asm_full_simp_tac (simpset() addsimps [o_apply]) 1);
   1.357 +by (asm_full_simp_tac
   1.358 +    (simpset() addsimps [all_conj_distrib,
   1.359 +			 Increasing_def, Stable_eq_stable, Join_stable,
   1.360 +			 Collect_eq_extend_set RS sym]) 1);
   1.361 +by (Clarify_tac 1);
   1.362 +bd G_stable_sysOfClient 1;
   1.363 +by (auto_tac (claset(), 
   1.364 +	      simpset() addsimps [o_apply,
   1.365 +				client_export Collect_eq_extend_set RS sym]));
   1.366 +qed "sysOfClient_i_Progress";
   1.367 +
   1.368 +
   1.369  (*progress (2), step 7*)
   1.370 -Goalw [System_def]
   1.371 +Goal
   1.372   "System : (INT i : lessThan Nclients. \
   1.373  \           INT h. {s. h <= (giv o sub i o client) s & \
   1.374  \                      h pfixGe (ask o sub i o client) s}  \
   1.375 -\                  LeadsTo[givenBy (funPair rel ask o sub i o client)] \
   1.376 -\                  {s. tokens h <= (tokens o rel o sub i o client) s})";
   1.377 -by (stac INT_iff 1);
   1.378 -by (rtac ballI 1);
   1.379 +\               Ensures {s. tokens h <= (tokens o rel o sub i o client) s})";
   1.380 +by (rtac INT_I 1);
   1.381  (*Couldn't have just used Auto_tac since the "INT h" must be kept*)
   1.382 -by (rtac (guarantees_Join_I2 RS guaranteesD) 1);
   1.383 -by (rtac (Client_i_Progress RS
   1.384 -	  (guarantees_PLam_I RS client_export project_guarantees)) 1);
   1.385 -by (Blast_tac 1);
   1.386 -by (Asm_simp_tac 1);
   1.387 -by (fast_tac (claset() addIs [projecting_Int,
   1.388 -			      component_PLam,
   1.389 -			      client_export projecting_Increasing]) 1);
   1.390 +by (rtac ([sysOfClient_i_Progress,
   1.391 +	   Client_component_System] MRS component_guaranteesD) 1);
   1.392  by (asm_full_simp_tac
   1.393 -    (simpset() addsimps [rewrite_rule [System_def] System_Increasing_giv]) 5);
   1.394 -by (rtac (client_export extending_LeadsETo RS extending_weaken_L RS 
   1.395 -	  extending_INT) 1);
   1.396 -by (auto_tac (claset(), 
   1.397 -	      simpset() addsimps [o_apply, 
   1.398 -				client_export Collect_eq_extend_set RS sym]));
   1.399 +    (simpset() addsimps [System_Increasing_giv]) 2);
   1.400 +auto();
   1.401  qed "System_Client_Progress";
   1.402  
   1.403  val lemma =
   1.404 @@ -583,11 +596,7 @@
   1.405  val lemma3 = result();
   1.406  
   1.407  
   1.408 -(*NOT GOOD ENOUGH.  Needs givenBy restriction
   1.409 -     (funPair allocGiv (funPair allocAsk allocRel))
   1.410 -  in LeadsTo!   But System_Client_Progress has the wrong restriction (below)
   1.411 -*)
   1.412 -(*progress (2), step 8*)
   1.413 +(*progress (2), step 8: Client i's "release" action is visible system-wide*)
   1.414  Goal "i < Nclients  \
   1.415  \     ==> System : {s. h <= (sub i o allocGiv) s & \
   1.416  \                      h pfixGe (sub i o allocAsk) s}  \
   1.417 @@ -597,75 +606,20 @@
   1.418  	  Follows_LeadsTo) 2);
   1.419  by (asm_full_simp_tac (simpset() addsimps [o_assoc]) 2);
   1.420  by (rtac LeadsTo_Trans 1);
   1.421 -by (rtac (impOfSubs LeadsETo_subset_LeadsTo) 2);
   1.422 -(*Here we have givenBy (funPair rel ask o sub i o client)]
   1.423 -  when we need givenBy (funPair allocRel allocAsk) ?? *)
   1.424  by (cut_facts_tac [System_Client_Progress] 2);
   1.425 -by (Force_tac 2);
   1.426 +by (blast_tac (claset() addIs [LeadsTo_Basis]) 2);
   1.427  by (etac lemma3 1);
   1.428 -qed "System_Alloc_Progress";
   1.429 -
   1.430 -(*NEED AUTOMATIC PROPAGATION of Alloc_Progress.  The text is identical
   1.431 -  except in the LeadsTo precondition.*)
   1.432 -Goal "extend sysOfAlloc Alloc :  \
   1.433 -\  (INT i : lessThan Nclients. Increasing (sub i o allocAsk) Int   \
   1.434 -\                              Increasing (sub i o allocRel))   \
   1.435 -\  Int   \
   1.436 -\  Always {s. ALL i : lessThan Nclients.   \
   1.437 -\             ALL elt : set ((sub i o allocAsk) s). elt <= NbT}   \
   1.438 -\  Int   \
   1.439 -\  (INT i : lessThan Nclients.    \
   1.440 -\   INT h. {s. h <= (sub i o allocGiv)s & h pfixGe (sub i o allocAsk)s}   \
   1.441 -\          LeadsTo[givenBy (funPair allocGiv (funPair allocAsk allocRel))]  \
   1.442 -\          {s. tokens h <= (tokens o sub i o allocRel)s})   \
   1.443 -\  guarantees[allocGiv]   \
   1.444 -\      (INT i : lessThan Nclients.   \
   1.445 -\       INT h. {s. h <= (sub i o allocAsk) s}    \
   1.446 - \             LeadsTo[givenBy allocGiv]   \
   1.447 -\              {s. h pfixLe (sub i o allocGiv) s})";
   1.448 -by (rtac (Alloc_Progress RS alloc_export project_guarantees) 1);
   1.449 -(*preserves*)
   1.450 -by (simp_tac (simpset() addsimps [o_def]) 3);
   1.451 -(*2: LeadsTo postcondition*)
   1.452 -by (rtac (extending_INT RS extending_INT) 2);
   1.453 -by (rtac (alloc_export extending_LeadsETo RS extending_weaken) 2);
   1.454 -by (rtac subset_refl 3);
   1.455 -by (simp_tac (simpset() addsimps [o_def]) 3);
   1.456 -by (simp_tac (simpset() addsimps [alloc_export Collect_eq_extend_set RS sym,
   1.457 -				  o_def]) 2);
   1.458 -(*1: Complex precondition*)
   1.459 -by (rtac (projecting_Int RS projecting_INT RS projecting_Int RS 
   1.460 -	  projecting_Int) 1);
   1.461 -by (rtac (alloc_export projecting_Increasing RS projecting_weaken_L) 1);
   1.462 -by (asm_simp_tac (simpset() addsimps [o_def]) 1);
   1.463 -by (rtac (alloc_export projecting_Increasing RS projecting_weaken_L) 1);
   1.464 -by (asm_simp_tac (simpset() addsimps [o_def]) 1);
   1.465 -by (rtac (alloc_export projecting_Always RS projecting_weaken_L) 1);
   1.466 -by (asm_simp_tac
   1.467 -    (simpset() addsimps [alloc_export Collect_eq_extend_set RS sym, o_def]) 1);
   1.468 -(*LeadsTo precondition*)
   1.469 -by (rtac (projecting_INT RS projecting_INT) 1);
   1.470 -by (rtac (alloc_export projecting_LeadsTo RS projecting_weaken_L) 1);
   1.471 -by (auto_tac (claset(),
   1.472 -	      simpset() addsimps [alloc_export Collect_eq_extend_set RS sym,
   1.473 -				  o_def]));
   1.474 -by (auto_tac (claset() addSIs [givenByI]
   1.475 -		       addEs [LeadsETo_weaken, givenByD]
   1.476 -		       addSWrapper record_split_wrapper, 
   1.477 -	      simpset() addsimps [funPair_def]));
   1.478 -qed "extend_Alloc_Progress";
   1.479 +qed "System_Alloc_Client_Progress";
   1.480  
   1.481  
   1.482 -xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx;
   1.483  
   1.484  (*progress (2), step 9*)
   1.485  Goal
   1.486   "System : (INT i : lessThan Nclients. \
   1.487  \           INT h. {s. h <= (sub i o allocAsk) s}  \
   1.488 -\                  LeadsTo[givenBy allocGiv] \
   1.489 -\                  {s. h pfixLe (sub i o allocGiv) s})";
   1.490 -by (rtac (extend_Alloc_Progress RS component_guaranteesD) 1);
   1.491 -by (rtac Alloc_component_System 2);
   1.492 +\                  LeadsTo {s. h pfixLe (sub i o allocGiv) s})";
   1.493 +by (rtac ([Alloc_Progress, Alloc_component_System] 
   1.494 +	  MRS component_guaranteesD) 1);
   1.495  (*preserves*)
   1.496  by (asm_full_simp_tac (simpset() addsimps [o_def]) 2);
   1.497  (*the guarantees precondition*)
   1.498 @@ -673,8 +627,50 @@
   1.499  	      simpset() addsimps [System_Increasing_allocRel,
   1.500  				  System_Increasing_allocAsk]));
   1.501  by (rtac System_Bounded_allocAsk 1);
   1.502 -by (rtac System_Alloc_Progress 1);
   1.503 +by (etac System_Alloc_Progress 1);
   1.504 +qed "System_Alloc_Progress";
   1.505 +
   1.506 +
   1.507 +
   1.508 +(*Ultimate goal*)
   1.509 +Goal "System : system_spec";
   1.510 +
   1.511 +xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx;
   1.512 +
   1.513 +
   1.514 +(*progress (2), step 10*)
   1.515 +Goal
   1.516 + "System : (INT i : lessThan Nclients. \
   1.517 +\           INT h. {s. h <= (ask o sub i o client) s}  \
   1.518 +\                  LeadsTo {s. h pfixLe (giv o sub i o client) s})";
   1.519 +by (Clarify_tac 1);
   1.520 +by (rtac LeadsTo_Trans 1);
   1.521 +by (dtac (System_Follows_allocGiv RS Follows_LeadsTo) 2);
   1.522 +by (blast_tac (claset() addIs [prefix_imp_pfixLe, LeadsTo_weaken_R]) 2);
   1.523 +
   1.524 +prefix_imp_pfixLe
   1.525 +
   1.526  
   1.527 -by (rtac Alloc_component_System 3);
   1.528 -by (force_tac (claset(), simpset() addsimps [System_Increasing_allocRel]) 2);
   1.529 -by (rtac (Alloc_Safety RS alloc_export project_guarantees) 1);
   1.530 +System_Follows_ask
   1.531 +
   1.532 +by (dtac (System_Follows_rel RS impOfSubs (mono_tokens RS mono_Follows_o) RS 
   1.533 +	  Follows_LeadsTo) 2);
   1.534 +
   1.535 +by (asm_full_simp_tac (simpset() addsimps [o_assoc]) 2);
   1.536 +by (rtac LeadsTo_Trans 1);
   1.537 +by (cut_facts_tac [System_Client_Progress] 2);
   1.538 +by (blast_tac (claset() addIs [LeadsTo_Basis]) 2);
   1.539 +by (etac lemma3 1);
   1.540 +
   1.541 +by (rtac ([Alloc_Progress, Alloc_component_System] 
   1.542 +	  MRS component_guaranteesD) 1);
   1.543 +(*preserves*)
   1.544 +by (asm_full_simp_tac (simpset() addsimps [o_def]) 2);
   1.545 +(*the guarantees precondition*)
   1.546 +by (auto_tac (claset(), 
   1.547 +	      simpset() addsimps [System_Increasing_allocRel,
   1.548 +				  System_Increasing_allocAsk]));
   1.549 +by (rtac System_Bounded_allocAsk 1);
   1.550 +by (etac System_Alloc_Progress 1);
   1.551 +qed "System_Alloc_Progress";
   1.552 +
     2.1 --- a/src/HOL/UNITY/Alloc.thy	Thu Jan 13 17:29:04 2000 +0100
     2.2 +++ b/src/HOL/UNITY/Alloc.thy	Thu Jan 13 17:30:23 2000 +0100
     2.3 @@ -88,8 +88,7 @@
     2.4  	 Increasing giv
     2.5  	 guarantees[funPair rel ask]
     2.6  	 (INT h. {s. h <= giv s & h pfixGe ask s}
     2.7 -		 LeadsTo[givenBy (funPair rel ask)]
     2.8 -		 {s. tokens h <= (tokens o rel) s})"
     2.9 +		 Ensures {s. tokens h <= (tokens o rel) s})"
    2.10  
    2.11    (*spec: preserves part*)
    2.12      client_preserves :: clientState program set
    2.13 @@ -101,15 +100,18 @@
    2.14  
    2.15  (** Allocator specification (required) ***)
    2.16  
    2.17 +  (*Specified over the systemState, not the allocState, since then the
    2.18 +    leads-to properties could not be transferred to  extend sysOfAlloc Alloc*)
    2.19 +  
    2.20    (*spec (6)*)
    2.21 -  alloc_increasing :: allocState program set
    2.22 +  alloc_increasing :: systemState program set
    2.23      "alloc_increasing ==
    2.24  	 UNIV
    2.25           guarantees[allocGiv]
    2.26  	 (INT i : lessThan Nclients. Increasing (sub i o allocGiv))"
    2.27  
    2.28    (*spec (7)*)
    2.29 -  alloc_safety :: allocState program set
    2.30 +  alloc_safety :: systemState program set
    2.31      "alloc_safety ==
    2.32  	 (INT i : lessThan Nclients. Increasing (sub i o allocRel))
    2.33           guarantees[allocGiv]
    2.34 @@ -117,7 +119,7 @@
    2.35  	         <= NbT + sum (%i. (tokens o sub i o allocRel) s) Nclients}"
    2.36  
    2.37    (*spec (8)*)
    2.38 -  alloc_progress :: allocState program set
    2.39 +  alloc_progress :: systemState program set
    2.40      "alloc_progress ==
    2.41  	 (INT i : lessThan Nclients. Increasing (sub i o allocAsk) Int
    2.42  	                             Increasing (sub i o allocRel))
    2.43 @@ -132,14 +134,14 @@
    2.44           guarantees[allocGiv]
    2.45  	     (INT i : lessThan Nclients.
    2.46  	      INT h. {s. h <= (sub i o allocAsk) s}
    2.47 -	             LeadsTo[givenBy allocGiv]
    2.48 +	             LeadsTo
    2.49  	             {s. h pfixLe (sub i o allocGiv) s})"
    2.50  
    2.51    (*spec: preserves part*)
    2.52 -    alloc_preserves :: allocState program set
    2.53 -    "alloc_preserves == preserves (funPair allocRel allocAsk)"
    2.54 +    alloc_preserves :: systemState program set
    2.55 +    "alloc_preserves == preserves (funPair client (funPair allocRel allocAsk))"
    2.56    
    2.57 -  alloc_spec :: allocState program set
    2.58 +  alloc_spec :: systemState program set
    2.59      "alloc_spec == alloc_increasing Int alloc_safety Int alloc_progress Int
    2.60                     alloc_preserves"
    2.61  
    2.62 @@ -190,7 +192,7 @@
    2.63  
    2.64  locale System =
    2.65    fixes 
    2.66 -    Alloc   :: allocState program
    2.67 +    Alloc   :: systemState program
    2.68      Client  :: clientState program
    2.69      Network :: systemState program
    2.70      System  :: systemState program
    2.71 @@ -202,9 +204,6 @@
    2.72  
    2.73    defines
    2.74      System_def
    2.75 -      "System == (extend sysOfAlloc Alloc)
    2.76 -                 Join
    2.77 -                 (extend sysOfClient (plam x: lessThan Nclients. Client))
    2.78 -                 Join
    2.79 -                 Network"
    2.80 +      "System == Alloc Join Network Join
    2.81 +                 (extend sysOfClient (plam x: lessThan Nclients. Client))"
    2.82  end
     3.1 --- a/src/HOL/UNITY/Comp.ML	Thu Jan 13 17:29:04 2000 +0100
     3.2 +++ b/src/HOL/UNITY/Comp.ML	Thu Jan 13 17:30:23 2000 +0100
     3.3 @@ -172,3 +172,75 @@
     3.4  by (etac order_trans 1);
     3.5  by (Blast_tac 1);
     3.6  qed "Increasing_preserves_Stable";
     3.7 +
     3.8 +
     3.9 +(*** givenBy ***)
    3.10 +
    3.11 +Goalw [givenBy_def] "givenBy id = UNIV";
    3.12 +by Auto_tac;
    3.13 +qed "givenBy_id";
    3.14 +Addsimps [givenBy_id];
    3.15 +
    3.16 +Goalw [givenBy_def] "(givenBy v) = {A. ALL x:A. ALL y. v x = v y --> y: A}";
    3.17 +by Safe_tac;
    3.18 +by (res_inst_tac [("x", "v `` ?u")] image_eqI 2);
    3.19 +by Auto_tac;
    3.20 +qed "givenBy_eq_all";
    3.21 +
    3.22 +Goal "givenBy v = {A. EX P. A = {s. P(v s)}}";
    3.23 +by (simp_tac (simpset() addsimps [givenBy_eq_all]) 1);
    3.24 +by Safe_tac;
    3.25 +by (res_inst_tac [("x", "%n. EX s. v s = n & s : ?A")] exI 1);
    3.26 +by (Blast_tac 1);
    3.27 +by Auto_tac;
    3.28 +qed "givenBy_eq_Collect";
    3.29 +
    3.30 +val prems =
    3.31 +Goal "(!!x y. [| x:A;  v x = v y |] ==> y: A) ==> A: givenBy v";
    3.32 +by (stac givenBy_eq_all 1);
    3.33 +by (blast_tac (claset() addIs prems) 1);
    3.34 +qed "givenByI";
    3.35 +
    3.36 +Goalw [givenBy_def] "[| A: givenBy v;  x:A;  v x = v y |] ==> y: A";
    3.37 +by Auto_tac;
    3.38 +qed "givenByD";
    3.39 +
    3.40 +Goal "{} : givenBy v";
    3.41 +by (blast_tac (claset() addSIs [givenByI]) 1);
    3.42 +qed "empty_mem_givenBy";
    3.43 +
    3.44 +AddIffs [empty_mem_givenBy];
    3.45 +
    3.46 +Goal "A: givenBy v ==> EX P. A = {s. P(v s)}";
    3.47 +by (res_inst_tac [("x", "%n. EX s. v s = n & s : A")] exI 1);
    3.48 +by (full_simp_tac (simpset() addsimps [givenBy_eq_all]) 1);
    3.49 +by (Blast_tac 1);
    3.50 +qed "givenBy_imp_eq_Collect";
    3.51 +
    3.52 +Goalw [givenBy_def] "{s. P(v s)} : givenBy v";
    3.53 +by (Best_tac 1);
    3.54 +qed "Collect_mem_givenBy";
    3.55 +
    3.56 +Goal "givenBy v = {A. EX P. A = {s. P(v s)}}";
    3.57 +by (blast_tac (claset() addIs [Collect_mem_givenBy,
    3.58 +			       givenBy_imp_eq_Collect]) 1);
    3.59 +qed "givenBy_eq_eq_Collect";
    3.60 +
    3.61 +(*preserving v preserves properties given by v*)
    3.62 +Goal "[| F : preserves v;  D : givenBy v |] ==> F : stable D";
    3.63 +by (force_tac (claset(), 
    3.64 +	       simpset() addsimps [impOfSubs preserves_subset_stable, 
    3.65 +				   givenBy_eq_Collect]) 1);
    3.66 +qed "preserves_givenBy_imp_stable";
    3.67 +
    3.68 +Goal "givenBy (w o v) <= givenBy v";
    3.69 +by (simp_tac (simpset() addsimps [givenBy_eq_Collect]) 1);
    3.70 +by (Deepen_tac 0 1);
    3.71 +qed "givenBy_o_subset";
    3.72 +
    3.73 +Goal "[| A : givenBy v;  B : givenBy v |] ==> A-B : givenBy v";
    3.74 +by (full_simp_tac (simpset() addsimps [givenBy_eq_Collect]) 1);
    3.75 +by Safe_tac;
    3.76 +by (res_inst_tac [("x", "%z. ?R z & ~ ?Q z")] exI 1);
    3.77 +by (deepen_tac (set_cs addSIs [equalityI]) 0 1);
    3.78 +qed "givenBy_DiffI";
     4.1 --- a/src/HOL/UNITY/Comp.thy	Thu Jan 13 17:29:04 2000 +0100
     4.2 +++ b/src/HOL/UNITY/Comp.thy	Thu Jan 13 17:30:23 2000 +0100
     4.3 @@ -26,4 +26,8 @@
     4.4    funPair      :: "['a => 'b, 'a => 'c, 'a] => 'b * 'c"
     4.5      "funPair f g == %x. (f x, g x)"
     4.6  
     4.7 +  (*the set of all sets determined by f alone*)
     4.8 +  givenBy :: "['a => 'b] => 'a set set"
     4.9 +    "givenBy f == range (%B. f-`` B)"
    4.10 +
    4.11  end
     5.1 --- a/src/HOL/UNITY/ELT.ML	Thu Jan 13 17:29:04 2000 +0100
     5.2 +++ b/src/HOL/UNITY/ELT.ML	Thu Jan 13 17:30:23 2000 +0100
     5.3 @@ -6,69 +6,6 @@
     5.4  leadsTo strengthened with a specification of the allowable sets transient parts
     5.5  *)
     5.6  
     5.7 -Goalw [givenBy_def] "givenBy id = UNIV";
     5.8 -by Auto_tac;
     5.9 -qed "givenBy_id";
    5.10 -Addsimps [givenBy_id];
    5.11 -
    5.12 -Goalw [givenBy_def] "(givenBy v) = {A. ALL x:A. ALL y. v x = v y --> y: A}";
    5.13 -by Safe_tac;
    5.14 -by (res_inst_tac [("x", "v `` ?u")] image_eqI 2);
    5.15 -by Auto_tac;
    5.16 -qed "givenBy_eq_all";
    5.17 -
    5.18 -Goal "givenBy v = {A. EX P. A = {s. P(v s)}}";
    5.19 -by (simp_tac (simpset() addsimps [givenBy_eq_all]) 1);
    5.20 -by Safe_tac;
    5.21 -by (res_inst_tac [("x", "%n. EX s. v s = n & s : ?A")] exI 1);
    5.22 -by (Blast_tac 1);
    5.23 -by Auto_tac;
    5.24 -qed "givenBy_eq_Collect";
    5.25 -
    5.26 -val prems =
    5.27 -Goal "(!!x y. [| x:A;  v x = v y |] ==> y: A) ==> A: givenBy v";
    5.28 -by (stac givenBy_eq_all 1);
    5.29 -by (blast_tac (claset() addIs prems) 1);
    5.30 -qed "givenByI";
    5.31 -
    5.32 -Goalw [givenBy_def] "[| A: givenBy v;  x:A;  v x = v y |] ==> y: A";
    5.33 -by Auto_tac;
    5.34 -qed "givenByD";
    5.35 -
    5.36 -Goal "{} : givenBy v";
    5.37 -by (blast_tac (claset() addSIs [givenByI]) 1);
    5.38 -qed "empty_mem_givenBy";
    5.39 -
    5.40 -AddIffs [empty_mem_givenBy];
    5.41 -
    5.42 -Goal "A: givenBy v ==> EX P. A = {s. P(v s)}";
    5.43 -by (res_inst_tac [("x", "%n. EX s. v s = n & s : A")] exI 1);
    5.44 -by (full_simp_tac (simpset() addsimps [givenBy_eq_all]) 1);
    5.45 -by (Blast_tac 1);
    5.46 -qed "givenBy_imp_eq_Collect";
    5.47 -
    5.48 -Goalw [givenBy_def] "EX P. A = {s. P(v s)} ==> A: givenBy v";
    5.49 -by (Best_tac 1);
    5.50 -qed "eq_Collect_imp_givenBy";
    5.51 -
    5.52 -Goal "givenBy v = {A. EX P. A = {s. P(v s)}}";
    5.53 -by (blast_tac (claset() addIs [eq_Collect_imp_givenBy,
    5.54 -			       givenBy_imp_eq_Collect]) 1);
    5.55 -qed "givenBy_eq_eq_Collect";
    5.56 -
    5.57 -(*preserving v preserves properties given by v*)
    5.58 -Goal "[| F : preserves v;  D : givenBy v |] ==> F : stable D";
    5.59 -by (force_tac (claset(), 
    5.60 -	       simpset() addsimps [impOfSubs preserves_subset_stable, 
    5.61 -				   givenBy_eq_Collect]) 1);
    5.62 -qed "preserves_givenBy_imp_stable";
    5.63 -
    5.64 -Goal "givenBy (w o v) <= givenBy v";
    5.65 -by (simp_tac (simpset() addsimps [givenBy_eq_Collect]) 1);
    5.66 -by (Deepen_tac 0 1);
    5.67 -qed "givenBy_o_subset";
    5.68 -
    5.69 -
    5.70  (** Standard leadsTo rules **)
    5.71  
    5.72  Goalw [leadsETo_def]
    5.73 @@ -81,6 +18,7 @@
    5.74  by (blast_tac (claset() addIs [elt.Trans]) 1);
    5.75  qed "leadsETo_Trans";
    5.76  
    5.77 +
    5.78  (*Useful with cancellation, disjunction*)
    5.79  Goal "F : A leadsTo[CC] (A' Un A') ==> F : A leadsTo[CC] A'";
    5.80  by (asm_full_simp_tac (simpset() addsimps Un_ac) 1);
    5.81 @@ -126,6 +64,11 @@
    5.82  by (blast_tac (claset() addIs [leadsETo_Basis]) 1);
    5.83  qed "leadsETo_mono";
    5.84  
    5.85 +Goal "[| F : A leadsTo[CC] B;  F : B leadsTo[DD] C |] \
    5.86 +\     ==> F : A leadsTo[CC Un DD] C";
    5.87 +by (blast_tac (claset() addIs [impOfSubs leadsETo_mono, leadsETo_Trans]) 1);
    5.88 +qed "leadsETo_Trans_Un";
    5.89 +
    5.90  val prems = Goalw [leadsETo_def]
    5.91   "(!!A. A : S ==> F : (A Int C) leadsTo[CC] B) ==> F : (Union S Int C) leadsTo[CC] B";
    5.92  by (simp_tac (HOL_ss addsimps [Int_Union_Union]) 1);
    5.93 @@ -154,6 +97,7 @@
    5.94  Addsimps [empty_leadsETo];
    5.95  
    5.96  
    5.97 +
    5.98  (** Weakening laws **)
    5.99  
   5.100  Goal "[| F : A leadsTo[CC] A';  A'<=B' |] ==> F : A leadsTo[CC] B'";
   5.101 @@ -478,22 +422,6 @@
   5.102  
   5.103  Open_locale "Extend";
   5.104  
   5.105 -Goal "givenBy (v o f) = extend_set h `` (givenBy v)";
   5.106 -by (simp_tac (simpset() addsimps [givenBy_eq_Collect]) 1);
   5.107 -by (Deepen_tac 0 1);
   5.108 -qed "givenBy_o_eq_extend_set";
   5.109 -
   5.110 -Goal "givenBy f = range (extend_set h)";
   5.111 -by (simp_tac (simpset() addsimps [givenBy_eq_Collect]) 1);
   5.112 -by (Deepen_tac 0 1);
   5.113 -qed "givenBy_eq_extend_set";
   5.114 -
   5.115 -Goal "D : givenBy v ==> extend_set h D : givenBy (v o f)";
   5.116 -by (full_simp_tac (simpset() addsimps [givenBy_eq_all]) 1);
   5.117 -by (Blast_tac 1);
   5.118 -qed "extend_set_givenBy_I";
   5.119 -
   5.120 -
   5.121  Goal "F : A leadsTo[CC] B \
   5.122  \     ==> extend h F : (extend_set h A) leadsTo[extend_set h `` CC] \
   5.123  \                      (extend_set h B)";
   5.124 @@ -505,24 +433,6 @@
   5.125  				   extend_set_Diff_distrib RS sym]) 1);
   5.126  qed "leadsETo_imp_extend_leadsETo";
   5.127  
   5.128 -(*MOVE to Extend.ML?*)
   5.129 -Goal "A Int extend_set h ((project_set h A) Int B) = A Int extend_set h B";
   5.130 -by (auto_tac (claset(), simpset() addsimps [split_extended_all]));
   5.131 -qed "Int_extend_set_lemma";
   5.132 -
   5.133 -(*MOVE to extend.ML??*)
   5.134 -Goal "G : C co B ==> project h C G : project_set h C co project_set h B";
   5.135 -by (full_simp_tac (simpset() addsimps [constrains_def, project_def, 
   5.136 -				       project_act_def]) 1);
   5.137 -by (Blast_tac 1);
   5.138 -qed "project_constrains_project_set";
   5.139 -
   5.140 -(*MOVE to extend.ML??*)
   5.141 -Goal "G : stable C ==> project h C G : stable (project_set h C)";
   5.142 -by (asm_full_simp_tac (simpset() addsimps [stable_def, 
   5.143 -					   project_constrains_project_set]) 1);
   5.144 -qed "project_stable_project_set";
   5.145 -
   5.146  
   5.147  
   5.148  (*NOT USED, but analogous to preserves_project_transient_empty in Project.ML*)
   5.149 @@ -535,18 +445,6 @@
   5.150  				project_preserves_I]) 1);
   5.151  result();
   5.152  
   5.153 -(*GENERALIZES the version proved in Project.ML*)
   5.154 -Goal "[| G : preserves (v o f);  \
   5.155 -\        project h C G : transient (C' Int D);  \
   5.156 -\        project h C G : stable C';  D : givenBy v |]    \
   5.157 -\     ==> C' Int D = {}";
   5.158 -by (rtac stable_transient_empty 1);
   5.159 -by (assume_tac 2);
   5.160 -(*If addIs then PROOF FAILED at depth 3*)
   5.161 -by (blast_tac (claset() addSIs [stable_Int, preserves_givenBy_imp_stable,
   5.162 -				project_preserves_I]) 1);
   5.163 -qed "preserves_o_project_transient_empty";
   5.164 -
   5.165  
   5.166  (*This version's stronger in the "ensures" precondition
   5.167    BUT there's no ensures_weaken_L*)
     6.1 --- a/src/HOL/UNITY/ELT.thy	Thu Jan 13 17:29:04 2000 +0100
     6.2 +++ b/src/HOL/UNITY/ELT.thy	Thu Jan 13 17:30:23 2000 +0100
     6.3 @@ -4,6 +4,22 @@
     6.4      Copyright   1999  University of Cambridge
     6.5  
     6.6  leadsTo strengthened with a specification of the allowable sets transient parts
     6.7 +
     6.8 +TRY INSTEAD (to get rid of the {} and to gain strong induction)
     6.9 +
    6.10 +  elt :: "['a set set, 'a program, 'a set] => ('a set) set"
    6.11 +
    6.12 +inductive "elt CC F B"
    6.13 +  intrs 
    6.14 +
    6.15 +    Weaken  "A <= B ==> A : elt CC F B"
    6.16 +
    6.17 +    ETrans  "[| F : A ensures A';  A-A' : CC;  A' : elt CC F B |]
    6.18 +	     ==> A : elt CC F B"
    6.19 +
    6.20 +    Union  "{A. A: S} : Pow (elt CC F B) ==> (Union S) : elt CC F B"
    6.21 +
    6.22 +  monos Pow_mono
    6.23  *)
    6.24  
    6.25  ELT = Project +
    6.26 @@ -28,10 +44,6 @@
    6.27  
    6.28  constdefs
    6.29  
    6.30 -  (*the set of all sets determined by f alone*)
    6.31 -  givenBy :: "['a => 'b] => 'a set set"
    6.32 -    "givenBy f == range (%B. f-`` B)"
    6.33 -
    6.34    (*visible version of the LEADS-TO relation*)
    6.35    leadsETo :: "['a set, 'a set set, 'a set] => 'a program set"
    6.36                                          ("(3_/ leadsTo[_]/ _)" [80,0,80] 80)
     7.1 --- a/src/HOL/UNITY/Extend.ML	Thu Jan 13 17:29:04 2000 +0100
     7.2 +++ b/src/HOL/UNITY/Extend.ML	Thu Jan 13 17:30:23 2000 +0100
     7.3 @@ -327,6 +327,7 @@
     7.4  by (rtac program_equalityI 1);
     7.5  by Auto_tac;
     7.6  qed "extend_SKIP";
     7.7 +Addsimps [export extend_SKIP];
     7.8  
     7.9  Goal "project_set h UNIV = UNIV";
    7.10  by Auto_tac;
    7.11 @@ -456,6 +457,24 @@
    7.12  qed "extend_Always";
    7.13  
    7.14  
    7.15 +(** Further lemmas **)
    7.16 +
    7.17 +Goal "A Int extend_set h ((project_set h A) Int B) = A Int extend_set h B";
    7.18 +by (auto_tac (claset(), simpset() addsimps [split_extended_all]));
    7.19 +qed "Int_extend_set_lemma";
    7.20 +
    7.21 +Goal "G : C co B ==> project h C G : project_set h C co project_set h B";
    7.22 +by (full_simp_tac (simpset() addsimps [constrains_def, project_def, 
    7.23 +				       project_act_def]) 1);
    7.24 +by (Blast_tac 1);
    7.25 +qed "project_constrains_project_set";
    7.26 +
    7.27 +Goal "G : stable C ==> project h C G : stable (project_set h C)";
    7.28 +by (asm_full_simp_tac (simpset() addsimps [stable_def, 
    7.29 +					   project_constrains_project_set]) 1);
    7.30 +qed "project_stable_project_set";
    7.31 +
    7.32 +
    7.33  (*** Progress: transient, ensures ***)
    7.34  
    7.35  Goal "(extend h F : transient (extend_set h A)) = (F : transient A)";
    7.36 @@ -550,6 +569,24 @@
    7.37  qed "extend_LeadsTo";
    7.38  
    7.39  
    7.40 +(*** givenBy: USEFUL??? ***)
    7.41 +
    7.42 +Goal "givenBy (v o f) = extend_set h `` (givenBy v)";
    7.43 +by (simp_tac (simpset() addsimps [givenBy_eq_Collect]) 1);
    7.44 +by (Deepen_tac 0 1);
    7.45 +qed "givenBy_o_eq_extend_set";
    7.46 +
    7.47 +Goal "givenBy f = range (extend_set h)";
    7.48 +by (simp_tac (simpset() addsimps [givenBy_eq_Collect]) 1);
    7.49 +by (Deepen_tac 0 1);
    7.50 +qed "givenBy_eq_extend_set";
    7.51 +
    7.52 +Goal "D : givenBy v ==> extend_set h D : givenBy (v o f)";
    7.53 +by (full_simp_tac (simpset() addsimps [givenBy_eq_all]) 1);
    7.54 +by (Blast_tac 1);
    7.55 +qed "extend_set_givenBy_I";
    7.56 +
    7.57 +
    7.58  Close_locale "Extend";
    7.59  
    7.60  (*Close_locale should do this!
     8.1 --- a/src/HOL/UNITY/Follows.thy	Thu Jan 13 17:29:04 2000 +0100
     8.2 +++ b/src/HOL/UNITY/Follows.thy	Thu Jan 13 17:30:23 2000 +0100
     8.3 @@ -9,7 +9,7 @@
     8.4    progress part: g cannot do anything silly.
     8.5  *)
     8.6  
     8.7 -Follows = ELT +
     8.8 +Follows = Project +
     8.9  
    8.10  constdefs
    8.11  
     9.1 --- a/src/HOL/UNITY/Guar.ML	Thu Jan 13 17:29:04 2000 +0100
     9.2 +++ b/src/HOL/UNITY/Guar.ML	Thu Jan 13 17:30:23 2000 +0100
     9.3 @@ -80,7 +80,7 @@
     9.4  (*This version of guaranteesD matches more easily in the conclusion
     9.5    The major premise can no longer be  F<=H since we need to reason about G*)
     9.6  Goalw [guar_def]
     9.7 -     "[| F : X guarantees[v] Y;  H : X;  F Join G = H;  G : preserves v |] \
     9.8 +     "[| F : X guarantees[v] Y;  F Join G = H;  H : X;  G : preserves v |] \
     9.9  \     ==> H : Y";
    9.10  by (Blast_tac 1);
    9.11  qed "component_guaranteesD";
    10.1 --- a/src/HOL/UNITY/Lift_prog.ML	Thu Jan 13 17:29:04 2000 +0100
    10.2 +++ b/src/HOL/UNITY/Lift_prog.ML	Thu Jan 13 17:30:23 2000 +0100
    10.3 @@ -120,7 +120,7 @@
    10.4  by Auto_tac;
    10.5  qed "good_map_lift_map";
    10.6  
    10.7 -fun lift_export th = 
    10.8 +fun lift_export0 th = 
    10.9      good_map_lift_map RS export th 
   10.10         |> simplify (simpset() addsimps [fold_o_sub]);;
   10.11  
   10.12 @@ -133,7 +133,7 @@
   10.13  
   10.14  Goal "lift_set i A = extend_set (lift_map i) A";
   10.15  by (auto_tac (claset(), 
   10.16 -     simpset() addsimps [lift_export mem_extend_set_iff]));
   10.17 +     simpset() addsimps [lift_export0 mem_extend_set_iff]));
   10.18  qed "lift_set_correct";
   10.19  
   10.20  Goalw [drop_set_def, project_set_def, lift_map_def]
   10.21 @@ -148,7 +148,7 @@
   10.22  Goal "lift_act i = extend_act (lift_map i)";
   10.23  by (rtac ext 1);
   10.24  by Auto_tac;
   10.25 -by (forward_tac [lift_export extend_act_D] 2);
   10.26 +by (forward_tac [lift_export0 extend_act_D] 2);
   10.27  by (auto_tac (claset(), simpset() addsimps [extend_act_def]));
   10.28  by (auto_tac (claset(), simpset() addsimps [extend_act_def, lift_map_def]));
   10.29  by (rtac bexI 1);
   10.30 @@ -168,7 +168,7 @@
   10.31  by (rtac (program_equalityI RS ext) 1);
   10.32  by (simp_tac (simpset() addsimps [lift_set_correct]) 1);
   10.33  by (simp_tac (simpset() 
   10.34 -	      addsimps [lift_export Acts_extend, 
   10.35 +	      addsimps [lift_export0 Acts_extend, 
   10.36  			lift_act_correct]) 1);
   10.37  qed "lift_prog_correct";
   10.38  
   10.39 @@ -212,7 +212,7 @@
   10.40  
   10.41  Goal "lift_set i UNIV = UNIV";
   10.42  by (simp_tac
   10.43 -    (simpset() addsimps [lift_set_correct, lift_export extend_set_UNIV_eq]) 1);
   10.44 +    (simpset() addsimps [lift_set_correct, lift_export0 extend_set_UNIV_eq]) 1);
   10.45  qed "lift_set_UNIV_eq";
   10.46  Addsimps [lift_set_UNIV_eq];
   10.47  
   10.48 @@ -220,7 +220,7 @@
   10.49  Goal "Domain act <= drop_set i C ==> drop_act i (Restrict C (lift_act i act)) = act";
   10.50  by (asm_full_simp_tac
   10.51      (simpset() addsimps [drop_set_correct, drop_act_correct, 
   10.52 -			 lift_act_correct, lift_export extend_act_inverse]) 1);
   10.53 +			 lift_act_correct, lift_export0 extend_act_inverse]) 1);
   10.54  qed "lift_act_inverse";
   10.55  Addsimps [lift_act_inverse];
   10.56  *)
   10.57 @@ -228,13 +228,13 @@
   10.58  Goal "UNIV <= drop_set i C ==> drop_prog i C (lift_prog i F) = F";
   10.59  by (asm_full_simp_tac
   10.60      (simpset() addsimps [drop_set_correct, drop_prog_correct, 
   10.61 -			 lift_prog_correct, lift_export extend_inverse]) 1);
   10.62 +			 lift_prog_correct, lift_export0 extend_inverse]) 1);
   10.63  qed "lift_prog_inverse";
   10.64  Addsimps [lift_prog_inverse];
   10.65  
   10.66  Goal "inj (lift_prog i)";
   10.67  by (simp_tac
   10.68 -    (simpset() addsimps [lift_prog_correct, lift_export inj_extend]) 1);
   10.69 +    (simpset() addsimps [lift_prog_correct, lift_export0 inj_extend]) 1);
   10.70  qed "inj_lift_prog";
   10.71  
   10.72  
   10.73 @@ -242,7 +242,7 @@
   10.74  
   10.75  Goal "lift_act i act ^^ lift_set i A = lift_set i (act^^A)";
   10.76  by (asm_simp_tac (simpset() addsimps [lift_set_correct, lift_act_correct,
   10.77 -				      lift_export extend_act_Image]) 1);
   10.78 +				      lift_export0 extend_act_Image]) 1);
   10.79  qed "lift_act_Image";
   10.80  Addsimps [lift_act_Image];
   10.81  
   10.82 @@ -272,7 +272,7 @@
   10.83  \     ==> F : (drop_set i A) co (drop_set i B)";
   10.84  by (asm_full_simp_tac
   10.85      (simpset() addsimps [drop_set_correct, lift_prog_correct, 
   10.86 -			 lift_export extend_constrains_project_set]) 1);
   10.87 +			 lift_export0 extend_constrains_project_set]) 1);
   10.88  qed "lift_prog_constrains_drop_set";
   10.89  
   10.90  (*This one looks strange!  Proof probably is by case analysis on i=j.
   10.91 @@ -292,7 +292,7 @@
   10.92  \     (F : (C Int lift_set i A) co (lift_set i B) & A <= B)";
   10.93  by (simp_tac
   10.94      (simpset() addsimps [drop_prog_correct, 
   10.95 -			 lift_set_correct, lift_export project_constrains]) 1);
   10.96 +			 lift_set_correct, lift_export0 project_constrains]) 1);
   10.97  qed "drop_prog_constrains";
   10.98  
   10.99  Goal "(drop_prog i UNIV F : stable A)  =  (F : stable (lift_set i A))";
  10.100 @@ -307,14 +307,14 @@
  10.101  Goal "reachable (lift_prog i F) = lift_set i (reachable F)";
  10.102  by (simp_tac
  10.103      (simpset() addsimps [lift_prog_correct, lift_set_correct, 
  10.104 -			 lift_export reachable_extend_eq]) 1);
  10.105 +			 lift_export0 reachable_extend_eq]) 1);
  10.106  qed "reachable_lift_prog";
  10.107  
  10.108  Goal "(lift_prog i F : (lift_set i A) Co (lift_set i B))  =  \
  10.109  \     (F : A Co B)";
  10.110  by (simp_tac
  10.111      (simpset() addsimps [lift_prog_correct, lift_set_correct, 
  10.112 -			 lift_export extend_Constrains]) 1);
  10.113 +			 lift_export0 extend_Constrains]) 1);
  10.114  qed "lift_prog_Constrains";
  10.115  
  10.116  Goal "(lift_prog i F : Stable (lift_set i A)) = (F : Stable A)";
  10.117 @@ -326,7 +326,7 @@
  10.118  \     ==> lift_prog i F Join G : (lift_set i A) Co (lift_set i B)";
  10.119  by (asm_full_simp_tac
  10.120      (simpset() addsimps [lift_prog_correct, drop_prog_correct, 
  10.121 -		     lift_set_correct, lift_export project_Constrains_D]) 1);
  10.122 +		     lift_set_correct, lift_export0 project_Constrains_D]) 1);
  10.123  qed "drop_prog_Constrains_D";
  10.124  
  10.125  Goalw [Stable_def]
  10.126 @@ -341,7 +341,7 @@
  10.127  \     ==> lift_prog i F Join G : Always (lift_set i A)";
  10.128  by (asm_full_simp_tac
  10.129      (simpset() addsimps [lift_prog_correct, drop_prog_correct, 
  10.130 -		     lift_set_correct, lift_export project_Always_D]) 1);
  10.131 +		     lift_set_correct, lift_export0 project_Always_D]) 1);
  10.132  qed "drop_prog_Always_D";
  10.133  
  10.134  Goalw [Increasing_def]
  10.135 @@ -359,7 +359,7 @@
  10.136  \     ==> drop_prog i C ((lift_prog i F) Join G) = F Join (drop_prog i C G)";
  10.137  by (asm_full_simp_tac
  10.138      (simpset() addsimps [lift_prog_correct, drop_prog_correct, 
  10.139 -		     drop_set_correct, lift_export project_extend_Join]) 1);
  10.140 +		     drop_set_correct, lift_export0 project_extend_Join]) 1);
  10.141  qed "drop_prog_lift_prog_Join";
  10.142  
  10.143  
  10.144 @@ -367,7 +367,7 @@
  10.145  
  10.146  Goal "(lift_prog i F : transient (lift_set i A)) = (F : transient A)";
  10.147  by (simp_tac (simpset() addsimps [lift_set_correct, lift_prog_correct,
  10.148 -			  lift_export extend_transient]) 1);
  10.149 +			  lift_export0 extend_transient]) 1);
  10.150  qed "lift_prog_transient";
  10.151  
  10.152  Goal "(lift_prog i F : transient (lift_set j A)) = \
  10.153 @@ -384,7 +384,7 @@
  10.154  Goal "lift_prog i F : preserves (v o sub j) = \
  10.155  \     (if i=j then F : preserves v else True)";
  10.156  by (simp_tac (simpset() addsimps [lift_prog_correct,
  10.157 -				  lift_export extend_preserves]) 1);
  10.158 +				  lift_export0 extend_preserves]) 1);
  10.159  by (auto_tac (claset(),
  10.160  	      simpset() addsimps [preserves_def, extend_def, extend_act_def, 
  10.161  				  stable_def, constrains_def, lift_map_def]));
  10.162 @@ -395,20 +395,21 @@
  10.163  Goal "G : preserves (v o sub i) ==> drop_prog i C G : preserves v";
  10.164  by (asm_simp_tac
  10.165      (simpset() addsimps [drop_prog_correct, fold_o_sub,
  10.166 -			 lift_export project_preserves_I]) 1);
  10.167 +			 lift_export0 project_preserves_I]) 1);
  10.168  qed "drop_prog_preserves_I";
  10.169  
  10.170  (*The raw version*)
  10.171  val [xguary,drop_prog,lift_prog] =
  10.172  Goal "[| F : X guarantees[v] Y;  \
  10.173 -\        !!G. lift_prog i F Join G : X' ==> F Join drop_prog i C G : X;  \
  10.174 -\        !!G. [| F Join drop_prog i C G : Y; lift_prog i F Join G : X' |] \
  10.175 +\        !!G. lift_prog i F Join G : X' ==> F Join drop_prog i (C G) G : X;  \
  10.176 +\        !!G. [| F Join drop_prog i (C G) G : Y; lift_prog i F Join G : X'; \
  10.177 +\                G : preserves (v o sub i) |] \
  10.178  \             ==> lift_prog i F Join G : Y' |] \
  10.179  \     ==> lift_prog i F : X' guarantees[v o sub i] Y'";
  10.180  by (rtac (xguary RS guaranteesD RS lift_prog RS guaranteesI) 1);
  10.181  by (etac drop_prog_preserves_I 1);
  10.182  by (etac drop_prog 1);
  10.183 -by (assume_tac 1);
  10.184 +by Auto_tac;
  10.185  qed "drop_prog_guarantees_raw";
  10.186  
  10.187  Goal "[| F : X guarantees[v] Y;  \
  10.188 @@ -418,7 +419,7 @@
  10.189  \     ==> lift_prog i F : X' guarantees[w] Y'";
  10.190  by (asm_simp_tac
  10.191      (simpset() addsimps [lift_prog_correct, fold_o_sub,
  10.192 -			 lift_export project_guarantees]) 1);
  10.193 +			 lift_export0 project_guarantees]) 1);
  10.194  qed "drop_prog_guarantees";
  10.195  
  10.196  
  10.197 @@ -443,13 +444,13 @@
  10.198  
  10.199  Goal "F : UNIV guarantees[v] increasing func \
  10.200  \   ==> lift_prog i F : UNIV guarantees[v o sub i] increasing (func o sub i)";
  10.201 -by (dtac (lift_export extend_guar_increasing) 1);
  10.202 +by (dtac (lift_export0 extend_guar_increasing) 1);
  10.203  by (asm_full_simp_tac (simpset() addsimps [lift_prog_correct, o_def]) 1);
  10.204  qed "lift_prog_guar_increasing";
  10.205  
  10.206  Goal "F : UNIV guarantees[v] Increasing func \
  10.207  \   ==> lift_prog i F : UNIV guarantees[v o sub i] Increasing (func o sub i)";
  10.208 -by (dtac (lift_export extend_guar_Increasing) 1);
  10.209 +by (dtac (lift_export0 extend_guar_Increasing) 1);
  10.210  by (asm_full_simp_tac (simpset() addsimps [lift_prog_correct, o_def]) 1);
  10.211  qed "lift_prog_guar_Increasing";
  10.212  
  10.213 @@ -458,5 +459,16 @@
  10.214  \       Always(lift_set i A) guarantees[v o sub i] Always (lift_set i B)";
  10.215  by (asm_simp_tac
  10.216      (simpset() addsimps [lift_set_correct, lift_prog_correct, 
  10.217 -			 lift_export extend_guar_Always]) 1);
  10.218 +			 lift_export0 extend_guar_Always]) 1);
  10.219  qed "lift_prog_guar_Always";
  10.220 +
  10.221 +(*version for outside use*)
  10.222 +fun lift_export th = 
  10.223 +    good_map_lift_map RS export th 
  10.224 +       |> simplify
  10.225 +             (simpset() addsimps [fold_o_sub, 
  10.226 +				  drop_set_correct RS sym, 
  10.227 +				  lift_set_correct RS sym, 
  10.228 +				  drop_prog_correct RS sym, 
  10.229 +				  lift_prog_correct RS sym]);;
  10.230 +
    11.1 --- a/src/HOL/UNITY/Lift_prog.thy	Thu Jan 13 17:29:04 2000 +0100
    11.2 +++ b/src/HOL/UNITY/Lift_prog.thy	Thu Jan 13 17:30:23 2000 +0100
    11.3 @@ -6,7 +6,7 @@
    11.4  lift_prog, etc: replication of components
    11.5  *)
    11.6  
    11.7 -Lift_prog = ELT +
    11.8 +Lift_prog = Project +
    11.9  
   11.10  constdefs
   11.11  
    12.1 --- a/src/HOL/UNITY/Project.ML	Thu Jan 13 17:29:04 2000 +0100
    12.2 +++ b/src/HOL/UNITY/Project.ML	Thu Jan 13 17:30:23 2000 +0100
    12.3 @@ -10,6 +10,12 @@
    12.4  POSSIBLY CAN DELETE Restrict_image_Diff
    12.5  *)
    12.6  
    12.7 +(*EQUALITIES.ML*)
    12.8 +		Goal "(A <= -A) = (A = {})";
    12.9 +		by (Blast_tac 1);
   12.10 +		qed "subset_Compl_self_eq";
   12.11 +
   12.12 +
   12.13  Open_locale "Extend";
   12.14  
   12.15  (** projection: monotonicity for safety **)
   12.16 @@ -137,7 +143,34 @@
   12.17  			 extend_constrains]) 1);
   12.18  qed "project_constrains_D";
   12.19  
   12.20 -(** "projecting" and union/intersection (no converses) **)
   12.21 +
   12.22 +(*** preserves ***)
   12.23 +
   12.24 +Goal "G : preserves (v o f) ==> project h C G : preserves v";
   12.25 +by (auto_tac (claset(),
   12.26 +	      simpset() addsimps [preserves_def, project_stable_I,
   12.27 +				  Collect_eq_extend_set RS sym]));
   12.28 +qed "project_preserves_I";
   12.29 +
   12.30 +(*to preserve f is to preserve the whole original state*)
   12.31 +Goal "G : preserves f ==> project h C G : preserves id";
   12.32 +by (asm_simp_tac (simpset() addsimps [project_preserves_I]) 1);
   12.33 +qed "project_preserves_id_I";
   12.34 +
   12.35 +Goal "(extend h G : preserves (v o f)) = (G : preserves v)";
   12.36 +by (auto_tac (claset(),
   12.37 +	      simpset() addsimps [preserves_def, extend_stable RS sym,
   12.38 +				  Collect_eq_extend_set RS sym]));
   12.39 +qed "extend_preserves";
   12.40 +
   12.41 +Goal "inj h ==> (extend h G : preserves g)";
   12.42 +by (auto_tac (claset(),
   12.43 +	      simpset() addsimps [preserves_def, extend_def, extend_act_def, 
   12.44 +				  stable_def, constrains_def, g_def]));
   12.45 +qed "inj_extend_preserves";
   12.46 +
   12.47 +
   12.48 +(*** "projecting" and union/intersection (no converses) ***)
   12.49  
   12.50  Goalw [projecting_def]
   12.51       "[| projecting C h F XA' XA;  projecting C h F XB' XB |] \
   12.52 @@ -446,7 +479,7 @@
   12.53  qed "extending_Increasing";
   12.54  
   12.55  
   12.56 -(*** leadsETo in the precondition ***)
   12.57 +(*** leadsETo in the precondition (??) ***)
   12.58  
   12.59  (** transient **)
   12.60  
   12.61 @@ -533,7 +566,8 @@
   12.62  				  Join_stable, Join_transient]));
   12.63  qed_spec_mp "Join_project_ensures";
   12.64  
   12.65 -(** Lemma useful for both STRONG and WEAK progress*)
   12.66 +(** Lemma useful for both STRONG and WEAK progress, but the transient
   12.67 +    condition's very strong **)
   12.68  
   12.69  (*The strange induction formula allows induction over the leadsTo
   12.70    assumption's non-atomic precondition*)
   12.71 @@ -568,32 +602,91 @@
   12.72  qed "Join_project_LeadsTo";
   12.73  
   12.74  
   12.75 -(*** GUARANTEES and EXTEND ***)
   12.76 +(*** Towards project_Ensures_D ***)
   12.77 +
   12.78 +
   12.79  
   12.80 -(** preserves **)
   12.81 +Goalw [project_set_def, extend_set_def, project_act_def]
   12.82 +     "act ^^ (C Int extend_set h A) <= B \
   12.83 +\     ==> project_act h (Restrict C act) ^^ (project_set h C Int A) \
   12.84 +\         <= project_set h B";
   12.85 +by (Blast_tac 1);
   12.86 +qed "act_subset_imp_project_act_subset";
   12.87 +
   12.88  
   12.89 -Goal "G : preserves (v o f) ==> project h C G : preserves v";
   12.90 -by (auto_tac (claset(),
   12.91 -	      simpset() addsimps [preserves_def, project_stable_I,
   12.92 -				  Collect_eq_extend_set RS sym]));
   12.93 -qed "project_preserves_I";
   12.94 +Goal "[| G : stable ((C Int extend_set h A) - (extend_set h B));  \
   12.95 +\        project h C G : transient (project_set h C Int A - B) |]  \
   12.96 +\     ==> G : transient (C Int extend_set h A - extend_set h B)";
   12.97 +by (case_tac "C Int extend_set h A <= extend_set h B" 1);
   12.98 +by (asm_simp_tac (simpset() addsimps [Diff_eq_empty_iff RS iffD2]) 1);
   12.99 +by (auto_tac (claset(), 
  12.100 +	      simpset() addsimps [transient_def, subset_Compl_self_eq,
  12.101 +				  Domain_project_act, split_extended_all]));
  12.102 +by (Blast_tac 1);
  12.103 +by (auto_tac (claset(), 
  12.104 +	      simpset() addsimps [stable_def, constrains_def]));
  12.105 +by (ball_tac 1);
  12.106 +by (thin_tac "ALL act: Acts G. ?P act" 1);
  12.107 +by (auto_tac (claset(), 
  12.108 +	      simpset() addsimps [Int_Diff,
  12.109 +				  extend_set_Diff_distrib RS sym]));
  12.110 +bd act_subset_imp_project_act_subset 1;
  12.111 +by (subgoal_tac
  12.112 +    "project_act h (Restrict C act) ^^ (project_set h C Int (A - B)) <= {}" 1);
  12.113 +bws [Restrict_def, project_set_def, extend_set_def, project_act_def];
  12.114 +(*using Int_greatest actually slows the next step!*)
  12.115 +by (Blast_tac 2);
  12.116 +by (force_tac (claset(), 
  12.117 +	      simpset() addsimps [split_extended_all]) 1);
  12.118 +qed "stable_project_transient";
  12.119 +
  12.120  
  12.121 -(*to preserve f is to preserve the whole original state*)
  12.122 -Goal "G : preserves f ==> project h C G : preserves id";
  12.123 -by (asm_simp_tac (simpset() addsimps [project_preserves_I]) 1);
  12.124 -qed "project_preserves_id_I";
  12.125 +Goal "[| G : stable C;  project h C G : (project_set h C Int A) unless B |] \
  12.126 +\     ==> G : (C Int extend_set h A) unless (extend_set h B)";
  12.127 +by (auto_tac
  12.128 +    (claset() addDs [stable_constrains_Int]
  12.129 +              addIs [constrains_weaken],
  12.130 +     simpset() addsimps [unless_def, project_constrains, Diff_eq, 
  12.131 +			 Int_assoc, Int_extend_set_lemma]));
  12.132 +qed_spec_mp "project_unless2";
  12.133  
  12.134 -Goal "(extend h G : preserves (v o f)) = (G : preserves v)";
  12.135 -by (auto_tac (claset(),
  12.136 -	      simpset() addsimps [preserves_def, extend_stable RS sym,
  12.137 -				  Collect_eq_extend_set RS sym]));
  12.138 -qed "extend_preserves";
  12.139 +Goal "[| G : stable ((C Int extend_set h A) - (extend_set h B));  \
  12.140 +\        F Join project h C G : (project_set h C Int A) ensures B;  \
  12.141 +\        extend h F Join G : stable C |] \
  12.142 +\     ==> extend h F Join G : (C Int extend_set h A) ensures (extend_set h B)";
  12.143 +(*unless*)
  12.144 +by (auto_tac (claset() addSIs [rewrite_rule [unless_def] project_unless2] 
  12.145 +                       addIs [project_extend_constrains_I], 
  12.146 +	      simpset() addsimps [ensures_def, Join_constrains,
  12.147 +				  Join_stable]));
  12.148 +(*transient*)
  12.149 +by (auto_tac (claset(), simpset() addsimps [Join_transient]));
  12.150 +by (blast_tac (claset() addIs [stable_project_transient]) 2);
  12.151 +by (force_tac (claset() addSEs [extend_transient RS iffD2 RS 
  12.152 +				transient_strengthen], 
  12.153 +	       simpset() addsimps [Join_transient, split_extended_all]) 1);
  12.154 +qed "project_ensures_D_lemma";
  12.155  
  12.156 -Goal "inj h ==> (extend h G : preserves g)";
  12.157 -by (auto_tac (claset(),
  12.158 -	      simpset() addsimps [preserves_def, extend_def, extend_act_def, 
  12.159 -				  stable_def, constrains_def, g_def]));
  12.160 -qed "inj_extend_preserves";
  12.161 +Goal "[| F Join project h UNIV G : A ensures B;  \
  12.162 +\        G : stable (extend_set h A - extend_set h B) |] \
  12.163 +\     ==> extend h F Join G : (extend_set h A) ensures (extend_set h B)";
  12.164 +br (project_ensures_D_lemma RS revcut_rl) 1;
  12.165 +by (stac stable_UNIV 3);
  12.166 +auto();
  12.167 +qed "project_ensures_D";
  12.168 +
  12.169 +Goalw [Ensures_def]
  12.170 +     "[| F Join project h (reachable (extend h F Join G)) G : A Ensures B;  \
  12.171 +\        G : stable (reachable (extend h F Join G) Int extend_set h A - \
  12.172 +\                    extend_set h B) |] \
  12.173 +\     ==> extend h F Join G : (extend_set h A) Ensures (extend_set h B)";
  12.174 +br (project_ensures_D_lemma RS revcut_rl) 1;
  12.175 +by (auto_tac (claset(), 
  12.176 +	      simpset() addsimps [project_set_reachable_extend_eq RS sym]));
  12.177 +qed "project_Ensures_D";
  12.178 +
  12.179 +
  12.180 +(*** GUARANTEES and EXTEND ***)
  12.181  
  12.182  (** Strong precondition and postcondition; doesn't seem very useful. **)
  12.183  
  12.184 @@ -630,14 +723,15 @@
  12.185  (*The raw version*)
  12.186  val [xguary,project,extend] =
  12.187  Goal "[| F : X guarantees[v] Y;  \
  12.188 -\        !!G. extend h F Join G : X' ==> F Join project h C G : X;  \
  12.189 -\        !!G. [| F Join project h C G : Y; extend h F Join G : X' |] \
  12.190 +\        !!G. extend h F Join G : X' ==> F Join project h (C G) G : X;  \
  12.191 +\        !!G. [| F Join project h (C G) G : Y; extend h F Join G : X'; \
  12.192 +\                G : preserves (v o f) |] \
  12.193  \             ==> extend h F Join G : Y' |] \
  12.194  \     ==> extend h F : X' guarantees[v o f] Y'";
  12.195  by (rtac (xguary RS guaranteesD RS extend RS guaranteesI) 1);
  12.196  by (etac project_preserves_I 1);
  12.197  by (etac project 1);
  12.198 -by (assume_tac 1);
  12.199 +by Auto_tac;
  12.200  qed "project_guarantees_raw";
  12.201  
  12.202  Goal "[| F : X guarantees[v] Y;  \
    13.1 --- a/src/HOL/UNITY/SubstAx.ML	Thu Jan 13 17:29:04 2000 +0100
    13.2 +++ b/src/HOL/UNITY/SubstAx.ML	Thu Jan 13 17:30:23 2000 +0100
    13.3 @@ -157,24 +157,28 @@
    13.4  
    13.5  (** More rules using the premise "Always INV" **)
    13.6  
    13.7 -Goal "[| F : (A-A') Co (A Un A');  F : transient (A-A') |]   \
    13.8 -\     ==> F : A LeadsTo A'";
    13.9 +Goal "F : A Ensures B ==> F : A LeadsTo B";
   13.10  by (asm_full_simp_tac
   13.11 -    (simpset() addsimps [LeadsTo_def, Constrains_eq_constrains]) 1);
   13.12 -by (rtac (ensuresI RS leadsTo_Basis) 1);
   13.13 -by (blast_tac (claset() addIs [transient_strengthen]) 2);
   13.14 -by (blast_tac (claset() addIs [constrains_weaken]) 1);
   13.15 +    (simpset() addsimps [Ensures_def, LeadsTo_def, leadsTo_Basis]) 1);
   13.16  qed "LeadsTo_Basis";
   13.17  
   13.18 +Goal "[| F : (A-B) Co (A Un B);  F : transient (A-B) |]   \
   13.19 +\     ==> F : A Ensures B";
   13.20 +by (asm_full_simp_tac
   13.21 +    (simpset() addsimps [Ensures_def, Constrains_eq_constrains]) 1);
   13.22 +by (blast_tac (claset() addIs [ensuresI, constrains_weaken, 
   13.23 +			       transient_strengthen]) 1);
   13.24 +qed "EnsuresI";
   13.25 +
   13.26  Goal "[| F : Always INV;      \
   13.27  \        F : (INV Int (A-A')) Co (A Un A'); \
   13.28  \        F : transient (INV Int (A-A')) |]   \
   13.29  \ ==> F : A LeadsTo A'";
   13.30  by (rtac Always_LeadsToI 1);
   13.31  by (assume_tac 1);
   13.32 -by (rtac LeadsTo_Basis 1);
   13.33 -by (blast_tac (claset() addIs [transient_strengthen]) 2);
   13.34 -by (blast_tac (claset() addIs [Always_ConstrainsD RS Constrains_weaken]) 1);
   13.35 +by (blast_tac (claset() addIs [EnsuresI, LeadsTo_Basis,
   13.36 +			       Always_ConstrainsD RS Constrains_weaken, 
   13.37 +			       transient_strengthen]) 1);
   13.38  qed "Always_LeadsTo_Basis";
   13.39  
   13.40  (*Set difference: maybe combine with leadsTo_weaken_L??
   13.41 @@ -420,7 +424,7 @@
   13.42  	      etac Always_LeadsTo_Basis 1 
   13.43  	          ORELSE   (*subgoal may involve LeadsTo, leadsTo or ensures*)
   13.44  		  REPEAT (ares_tac [LeadsTo_Basis, leadsTo_Basis,
   13.45 -				    ensuresI] 1),
   13.46 +				    EnsuresI, ensuresI] 1),
   13.47  	      (*now there are two subgoals: co & transient*)
   13.48  	      simp_tac (simpset() addsimps !program_defs_ref) 2,
   13.49  	      res_inst_tac [("act", sact)] transientI 2,
    14.1 --- a/src/HOL/UNITY/SubstAx.thy	Thu Jan 13 17:29:04 2000 +0100
    14.2 +++ b/src/HOL/UNITY/SubstAx.thy	Thu Jan 13 17:30:23 2000 +0100
    14.3 @@ -9,6 +9,9 @@
    14.4  SubstAx = WFair + Constrains + 
    14.5  
    14.6  constdefs
    14.7 +   Ensures :: "['a set, 'a set] => 'a program set"            (infixl 60)
    14.8 +    "A Ensures B == {F. F : (reachable F Int A) ensures B}"
    14.9 +
   14.10     LeadsTo :: "['a set, 'a set] => 'a program set"            (infixl 60)
   14.11      "A LeadsTo B == {F. F : (reachable F Int A) leadsTo B}"
   14.12  
    15.1 --- a/src/HOL/UNITY/Union.ML	Thu Jan 13 17:29:04 2000 +0100
    15.2 +++ b/src/HOL/UNITY/Union.ML	Thu Jan 13 17:30:23 2000 +0100
    15.3 @@ -181,6 +181,10 @@
    15.4       simpset() addsimps [constrains_def, Join_def]));
    15.5  qed "Join_constrains";
    15.6  
    15.7 +Goal "(F Join G : A unless B) = (F : A unless B & G : A unless B)";
    15.8 +by (simp_tac (simpset() addsimps [Join_constrains, unless_def]) 1);
    15.9 +qed "Join_unless";
   15.10 +
   15.11  (*Analogous weak versions FAIL; see Misra [1994] 5.4.1, Substitution Axiom.
   15.12    reachable (F Join G) could be much bigger than reachable F, reachable G
   15.13  *)
    16.1 --- a/src/HOL/UNITY/WFair.ML	Thu Jan 13 17:29:04 2000 +0100
    16.2 +++ b/src/HOL/UNITY/WFair.ML	Thu Jan 13 17:30:23 2000 +0100
    16.3 @@ -79,12 +79,15 @@
    16.4  by (blast_tac (claset() addIs [stable_constrains_Int, constrains_weaken]) 1);
    16.5  qed "stable_ensures_Int";
    16.6  
    16.7 -(*NEVER USED*)
    16.8  Goal "[| F : stable A;  F : transient C;  A <= B Un C |] ==> F : A ensures B";
    16.9  by (asm_full_simp_tac (simpset() addsimps [ensures_def, stable_def]) 1);
   16.10  by (blast_tac (claset() addIs [constrains_weaken, transient_strengthen]) 1);
   16.11  qed "stable_transient_ensures";
   16.12  
   16.13 +Goal "(A ensures B) = (A unless B) Int transient (A-B)";
   16.14 +by (simp_tac (simpset() addsimps [ensures_def, unless_def]) 1);
   16.15 +qed "ensures_eq";
   16.16 +
   16.17  
   16.18  (*** leadsTo ***)
   16.19