src/HOL/UNITY/Project.ML
changeset 7826 c6a8b73b6c2a
parent 7689 affe0c2fdfbf
child 7841 65d91d13fc13
     1.1 --- a/src/HOL/UNITY/Project.ML	Mon Oct 11 10:52:51 1999 +0200
     1.2 +++ b/src/HOL/UNITY/Project.ML	Mon Oct 11 10:53:39 1999 +0200
     1.3 @@ -108,13 +108,95 @@
     1.4  
     1.5  (*For using project_guarantees in particular cases*)
     1.6  Goal "extend h F Join G : extend_set h A co extend_set h B \
     1.7 -\     ==> F Join project UNIV h G : A co B";
     1.8 -by (stac (project_set_UNIV RS project_extend_Join RS sym) 1);
     1.9 +\     ==> F Join project C h G : A co B";
    1.10 +by (asm_full_simp_tac
    1.11 +    (simpset() addsimps [project_constrains, Join_constrains, 
    1.12 +			 extend_constrains]) 1);
    1.13 +by (blast_tac (claset() addIs [constrains_weaken]
    1.14 +			addDs [constrains_imp_subset]) 1);
    1.15 +qed "project_constrains_I";
    1.16 +
    1.17 +(*The UNIV argument is essential*)
    1.18 +Goal "F Join project UNIV h G : A co B \
    1.19 +\     ==> extend h F Join G : extend_set h A co extend_set h B";
    1.20  by (asm_full_simp_tac
    1.21      (simpset() addsimps [project_constrains, Join_constrains, 
    1.22  			 extend_constrains]) 1);
    1.23 -by (fast_tac (claset() addDs [constrains_imp_subset]) 1);
    1.24 -qed "project_constrains_I";
    1.25 +qed "project_constrains_D";
    1.26 +
    1.27 +Goalw [projecting_def]
    1.28 +     "[| ALL i:I. projecting C h F (X' i) (X i) |] \
    1.29 +\     ==> projecting C h F (INT i:I. X' i) (INT i:I. X i)";
    1.30 +by Auto_tac;
    1.31 +qed "projecting_INT";
    1.32 +
    1.33 +Goalw [projecting_def]
    1.34 +     "[| ALL i:I. projecting C h F (X' i) (X i) |] \
    1.35 +\     ==> projecting C h F (UN i:I. X' i) (UN i:I. X i)";
    1.36 +by Auto_tac;
    1.37 +qed "projecting_UN";
    1.38 +
    1.39 +Goalw [projecting_def]
    1.40 +     "[| projecting C h F X' X;  U'<=X';  X<=U |] ==> projecting C h F U' U";
    1.41 +by Auto_tac;
    1.42 +qed "projecting_weaken";
    1.43 +
    1.44 +(*Is this the right way to handle the X' argument?*)
    1.45 +Goalw [extending_def]
    1.46 +     "[| ALL i:I. extending C h F (X' i) (Y' i) (Y i) |] \
    1.47 +\     ==> extending C h F (INT i:I. X' i) (INT i:I. Y' i) (INT i:I. Y i)";
    1.48 +by Auto_tac;
    1.49 +qed "extending_INT";
    1.50 +
    1.51 +Goalw [extending_def]
    1.52 +     "[| ALL i:I. extending C h F X' (Y' i) (Y i) |] \
    1.53 +\     ==> extending C h F X' (UN i:I. Y' i) (UN i:I. Y i)";
    1.54 +by Auto_tac;
    1.55 +qed "extending_UN";
    1.56 +
    1.57 +Goalw [extending_def]
    1.58 +     "[| extending C h F X' Y' Y;  U'<= X';  Y'<=V';  V<=Y |] \
    1.59 +\     ==> extending C h F U' V' V";
    1.60 +by Auto_tac;
    1.61 +qed "extending_weaken";
    1.62 +
    1.63 +Goal "projecting C h F X' UNIV";
    1.64 +by (simp_tac (simpset() addsimps [projecting_def]) 1);
    1.65 +qed "projecting_UNIV";
    1.66 +
    1.67 +Goalw [projecting_def]
    1.68 +     "projecting C h F (extend_set h A co extend_set h B) (A co B)";
    1.69 +by (blast_tac (claset() addIs [project_constrains_I]) 1);
    1.70 +qed "projecting_constrains";
    1.71 +
    1.72 +Goalw [stable_def]
    1.73 +     "projecting C h F (stable (extend_set h A)) (stable A)";
    1.74 +by (rtac projecting_constrains 1);
    1.75 +qed "projecting_stable";
    1.76 +
    1.77 +Goalw [projecting_def]
    1.78 +     "projecting (%G. UNIV) h F (increasing (func o f)) (increasing func)";
    1.79 +by (simp_tac (simpset() addsimps [Join_project_increasing]) 1);
    1.80 +qed "projecting_increasing";
    1.81 +
    1.82 +Goal "extending C h F X' UNIV Y";
    1.83 +by (simp_tac (simpset() addsimps [extending_def]) 1);
    1.84 +qed "extending_UNIV";
    1.85 +
    1.86 +Goalw [extending_def]
    1.87 +     "extending (%G. UNIV) h F X' (extend_set h A co extend_set h B) (A co B)";
    1.88 +by (blast_tac (claset() addIs [project_constrains_D]) 1);
    1.89 +qed "extending_constrains";
    1.90 +
    1.91 +Goalw [stable_def]
    1.92 +     "extending (%G. UNIV) h F X' (stable (extend_set h A)) (stable A)";
    1.93 +by (rtac extending_constrains 1);
    1.94 +qed "extending_stable";
    1.95 +
    1.96 +Goalw [extending_def]
    1.97 +     "extending (%G. UNIV) h F X' (increasing (func o f)) (increasing func)";
    1.98 +by (simp_tac (simpset() addsimps [Join_project_increasing]) 1);
    1.99 +qed "extending_increasing";
   1.100  
   1.101  
   1.102  (*** Diff, needed for localTo ***)
   1.103 @@ -139,17 +221,19 @@
   1.104  by (ftac constrains_imp_subset 1);
   1.105  by (Asm_full_simp_tac 1);
   1.106  by (blast_tac (claset() addIs [constrains_weaken]) 1);
   1.107 -qed "Diff_project_co";
   1.108 +qed "Diff_project_constrains";
   1.109  
   1.110  Goalw [stable_def]
   1.111       "[| (UN act:acts. Domain act) <= project_set h C; \
   1.112  \        Diff G (extend_act h `` acts) : stable (extend_set h A) |] \
   1.113  \     ==> Diff (project C h G) acts : stable A";
   1.114 -by (etac Diff_project_co 1);
   1.115 +by (etac Diff_project_constrains 1);
   1.116  by (assume_tac 1);
   1.117  qed "Diff_project_stable";
   1.118  
   1.119 -(*Converse appears to fail*)
   1.120 +(*Converse fails: even if the conclusion holds, H could modify (v o f) 
   1.121 +  simultaneously with other variables, and this action would not be 
   1.122 +  superseded by anything in (extend h G) *)
   1.123  Goal "[| UNIV <= project_set h C;  H : (func o f) localTo extend h G |] \
   1.124  \     ==> project C h H : func localTo G";
   1.125  by (asm_full_simp_tac 
   1.126 @@ -166,6 +250,11 @@
   1.127      (simpset() addsimps [project_set_UNIV RS project_localTo_lemma]) 1);
   1.128  qed "project_localTo_I";
   1.129  
   1.130 +Goalw [projecting_def]
   1.131 +     "projecting (%G. UNIV) h F ((v o f) localTo extend h H) (v localTo H)";
   1.132 +by (blast_tac (claset() addIs [project_localTo_I]) 1);
   1.133 +qed "projecting_localTo";
   1.134 +
   1.135  
   1.136  (** Reachability and project **)
   1.137  
   1.138 @@ -243,7 +332,7 @@
   1.139  	      simpset() addsimps [project_set_def]));
   1.140  qed "project_set_reachable_extend_eq";
   1.141  
   1.142 -
   1.143 +(*Perhaps should replace C by reachable...*)
   1.144  Goalw [Constrains_def]
   1.145       "[| C <= reachable (extend h F Join G);  \
   1.146  \        extend h F Join G : (extend_set h A) Co (extend_set h B) |] \
   1.147 @@ -274,7 +363,7 @@
   1.148  \        extend h F Join G : Always (extend_set h A) |]   \
   1.149  \     ==> F Join project C h G : Always A";
   1.150  by (auto_tac (claset(), simpset() addsimps [project_Stable_I]));
   1.151 -bws [project_set_def, extend_set_def];
   1.152 +by (rewrite_goals_tac [project_set_def, extend_set_def]);
   1.153  by (Blast_tac 1);
   1.154  qed "project_Always_I";
   1.155  
   1.156 @@ -305,6 +394,59 @@
   1.157  				      Collect_eq_extend_set RS sym]) 1);
   1.158  qed "project_Increasing";
   1.159  
   1.160 +(** A lot of redundant theorems: all are proved to facilitate reasoning
   1.161 +    about guarantees. **)
   1.162 +
   1.163 +Goalw [projecting_def]
   1.164 +     "projecting (%G. reachable (extend h F Join G)) h F \
   1.165 +\                (extend_set h A Co extend_set h B) (A Co B)";
   1.166 +by (blast_tac (claset() addIs [project_Constrains_I]) 1);
   1.167 +qed "projecting_Constrains";
   1.168 +
   1.169 +Goalw [Stable_def]
   1.170 +     "projecting (%G. reachable (extend h F Join G)) h F \
   1.171 +\                (Stable (extend_set h A)) (Stable A)";
   1.172 +by (rtac projecting_Constrains 1);
   1.173 +qed "projecting_Stable";
   1.174 +
   1.175 +Goalw [projecting_def]
   1.176 +     "projecting (%G. reachable (extend h F Join G)) h F \
   1.177 +\                (Always (extend_set h A)) (Always A)";
   1.178 +by (blast_tac (claset() addIs [project_Always_I]) 1);
   1.179 +qed "projecting_Always";
   1.180 +
   1.181 +Goalw [projecting_def]
   1.182 +     "projecting (%G. reachable (extend h F Join G)) h F \
   1.183 +\                (Increasing (func o f)) (Increasing func)";
   1.184 +by (blast_tac (claset() addIs [project_Increasing_I]) 1);
   1.185 +qed "projecting_Increasing";
   1.186 +
   1.187 +Goalw [extending_def]
   1.188 +     "extending (%G. reachable (extend h F Join G)) h F X' \
   1.189 +\               (extend_set h A Co extend_set h B) (A Co B)";
   1.190 +by (blast_tac (claset() addIs [project_Constrains_D]) 1);
   1.191 +qed "extending_Constrains";
   1.192 +
   1.193 +Goalw [extending_def]
   1.194 +     "extending (%G. reachable (extend h F Join G)) h F X' \
   1.195 +\               (Stable (extend_set h A)) (Stable A)";
   1.196 +by (blast_tac (claset() addIs [project_Stable_D]) 1);
   1.197 +qed "extending_Stable";
   1.198 +
   1.199 +Goalw [extending_def]
   1.200 +     "extending (%G. reachable (extend h F Join G)) h F X' \
   1.201 +\               (Always (extend_set h A)) (Always A)";
   1.202 +by (blast_tac (claset() addIs [project_Always_D]) 1);
   1.203 +qed "extending_Always";
   1.204 +
   1.205 +val [prem] = 
   1.206 +Goalw [extending_def]
   1.207 +     "(!!G. reachable (extend h F Join G) <= C G)  \
   1.208 +\     ==> extending C h F X' \
   1.209 +\                   (Increasing (func o f)) (Increasing func)";
   1.210 +by (blast_tac (claset() addIs [prem RS project_Increasing_D]) 1);
   1.211 +qed "extending_Increasing";
   1.212 +
   1.213  
   1.214  (** Progress includes safety in the definition of ensures **)
   1.215  
   1.216 @@ -369,9 +511,8 @@
   1.217  by (Blast_tac 1);
   1.218  qed "ensures_extend_set_imp_project_ensures";
   1.219  
   1.220 -(*A super-strong condition: G is not allowed to affect the
   1.221 -  shared variables at all.*)
   1.222 -Goal "[| ALL x. project C h G ~: transient {x};  \
   1.223 +(*A strong condition: F can do anything that project G can.*)
   1.224 +Goal "[| ALL D. project C h G : transient D --> F : transient D;  \
   1.225  \        extend h F Join G : stable C;  \
   1.226  \        F Join project C h G : A ensures B |] \
   1.227  \     ==> extend h F Join G : (C Int extend_set h A) ensures (extend_set h B)";
   1.228 @@ -387,7 +528,7 @@
   1.229  		       simpset()) 1));
   1.230  qed_spec_mp "Join_project_ensures";
   1.231  
   1.232 -Goal "[| ALL x. project C h G ~: transient {x};  \
   1.233 +Goal "[| ALL D. project C h G : transient D --> F : transient D;  \
   1.234  \        extend h F Join G : stable C;  \
   1.235  \        F Join project C h G : A leadsTo B |] \
   1.236  \     ==> extend h F Join G : (C Int extend_set h A) leadsTo (extend_set h B)";
   1.237 @@ -400,7 +541,7 @@
   1.238  qed "project_leadsTo_lemma";
   1.239  
   1.240  (*Instance of the previous theorem for STRONG progress*)
   1.241 -Goal "[| ALL x. project UNIV h G ~: transient {x};  \
   1.242 +Goal "[| ALL D. project UNIV h G : transient D --> F : transient D;  \
   1.243  \        F Join project UNIV h G : A leadsTo B |] \
   1.244  \     ==> extend h F Join G : (extend_set h A) leadsTo (extend_set h B)";
   1.245  by (dtac project_leadsTo_lemma 1);
   1.246 @@ -409,7 +550,7 @@
   1.247  
   1.248  (** Towards the analogous theorem for WEAK progress*)
   1.249  
   1.250 -Goal "[| ALL x. project C h G ~: transient {x};  \
   1.251 +Goal "[| ALL D. project C h G : transient D --> F : transient D;  \
   1.252  \        extend h F Join G : stable C;  \
   1.253  \        F Join project C h G : (project_set h C Int A) leadsTo B |] \
   1.254  \     ==> extend h F Join G : C Int extend_set h (project_set h C Int A) leadsTo (extend_set h B)";
   1.255 @@ -421,7 +562,7 @@
   1.256  by (blast_tac (claset() addIs [leadsTo_Basis, Join_project_ensures]) 1);
   1.257  val lemma = result();
   1.258  
   1.259 -Goal "[| ALL x. project C h G ~: transient {x};  \
   1.260 +Goal "[| ALL D. project C h G : transient D --> F : transient D;  \
   1.261  \        extend h F Join G : stable C;  \
   1.262  \        F Join project C h G : (project_set h C Int A) leadsTo B |] \
   1.263  \     ==> extend h F Join G : (C Int extend_set h A) leadsTo (extend_set h B)";
   1.264 @@ -430,7 +571,7 @@
   1.265  val lemma2 = result();
   1.266  
   1.267  Goal "[| C = (reachable (extend h F Join G)); \
   1.268 -\        ALL x. project C h G ~: transient {x};  \
   1.269 +\        ALL D. project C h G : transient D --> F : transient D;  \
   1.270  \        F Join project C h G : A LeadsTo B |] \
   1.271  \     ==> extend h F Join G : (extend_set h A) LeadsTo (extend_set h B)";
   1.272  by (asm_full_simp_tac 
   1.273 @@ -453,13 +594,11 @@
   1.274  
   1.275  Goal "extend h F : (extend h `` X) guarantees (extend h `` Y) \
   1.276  \    ==> F : X guarantees Y";
   1.277 -by (rtac guaranteesI 1);
   1.278 -by (auto_tac (claset(), simpset() addsimps [guar_def, component_def]));
   1.279 -by (dtac spec 1);
   1.280 -by (dtac (mp RS mp) 1);
   1.281 -by (Blast_tac 2);
   1.282 -by (blast_tac (claset() addSDs [inj_extend RS inj_image_mem_iff RS iffD1]) 2);
   1.283 -by Auto_tac;
   1.284 +by (auto_tac (claset(), simpset() addsimps [guarantees_eq]));
   1.285 +by (dres_inst_tac [("x", "extend h G")] spec 1);
   1.286 +by (asm_full_simp_tac 
   1.287 +    (simpset() delsimps [extend_Join] 
   1.288 +           addsimps [extend_Join RS sym, inj_extend RS inj_image_mem_iff]) 1);
   1.289  qed "extend_guarantees_imp_guarantees";
   1.290  
   1.291  Goal "(extend h F : (extend h `` X) guarantees (extend h `` Y)) = \
   1.292 @@ -471,17 +610,12 @@
   1.293  
   1.294  (*Weak precondition and postcondition; this is the good one!
   1.295    Not clear that it has a converse [or that we want one!]*)
   1.296 -val [xguary,project,extend] =
   1.297  Goal "[| F : X guarantees Y;  \
   1.298 -\        !!G. extend h F Join G : X' ==> F Join proj G h G : X;  \
   1.299 -\        !!G. [| F Join proj G h G : Y; extend h F Join G : X'; \
   1.300 -\                Disjoint (extend h F) G |] \
   1.301 -\             ==> extend h F Join G : Y' |] \
   1.302 +\        projecting C h F X' X;  extending C h F X' Y' Y |] \
   1.303  \     ==> extend h F : X' guarantees Y'";
   1.304 -by (rtac (xguary RS guaranteesD RS extend RS guaranteesI) 1);
   1.305 -by (etac project 1);
   1.306 -by (assume_tac 1);
   1.307 -by (assume_tac 1);
   1.308 +by (rtac guaranteesI 1);
   1.309 +by (auto_tac (claset(), 
   1.310 +        simpset() addsimps [guaranteesD, projecting_def, extending_def]));
   1.311  qed "project_guarantees";
   1.312  
   1.313  (** It seems that neither "guarantees" law can be proved from the other. **)
   1.314 @@ -489,17 +623,20 @@
   1.315  
   1.316  (*** guarantees corollaries ***)
   1.317  
   1.318 +(** Most could be deleted: the required versions are easy to prove **)
   1.319 +
   1.320  Goal "F : UNIV guarantees increasing func \
   1.321 -\     ==> extend h F : UNIV guarantees increasing (func o f)";
   1.322 +\     ==> extend h F : X' guarantees increasing (func o f)";
   1.323  by (etac project_guarantees 1);
   1.324 -by (ALLGOALS
   1.325 -    (asm_simp_tac (simpset() addsimps [Join_project_increasing RS sym])));
   1.326 +by (rtac extending_increasing 2);
   1.327 +by (rtac projecting_UNIV 1);
   1.328  qed "extend_guar_increasing";
   1.329  
   1.330  Goal "F : UNIV guarantees Increasing func \
   1.331 -\     ==> extend h F : UNIV guarantees Increasing (func o f)";
   1.332 +\     ==> extend h F : X' guarantees Increasing (func o f)";
   1.333  by (etac project_guarantees 1);
   1.334 -by (rtac (subset_UNIV RS project_Increasing_D) 2);
   1.335 +by (rtac extending_Increasing 2);
   1.336 +by (rtac projecting_UNIV 1);
   1.337  by Auto_tac;
   1.338  qed "extend_guar_Increasing";
   1.339  
   1.340 @@ -507,30 +644,42 @@
   1.341  \     ==> extend h F : (v o f) localTo (extend h G)  \
   1.342  \                      guarantees increasing (func o f)";
   1.343  by (etac project_guarantees 1);
   1.344 -(*the "increasing" guarantee*)
   1.345 -by (asm_simp_tac (simpset() addsimps [Join_project_increasing RS sym]) 2);
   1.346 -by (etac project_localTo_I 1);
   1.347 +by (rtac extending_increasing 2);
   1.348 +by (rtac projecting_localTo 1);
   1.349  qed "extend_localTo_guar_increasing";
   1.350  
   1.351  Goal "F : (v localTo G) guarantees Increasing func  \
   1.352  \     ==> extend h F : (v o f) localTo (extend h G)  \
   1.353  \                      guarantees Increasing (func o f)";
   1.354  by (etac project_guarantees 1);
   1.355 -(*the "Increasing" guarantee*)
   1.356 -by (etac (subset_UNIV RS project_Increasing_D) 2);
   1.357 -by (etac project_localTo_I 1);
   1.358 +by (rtac extending_Increasing 2);
   1.359 +by (rtac projecting_localTo 1);
   1.360 +by Auto_tac;
   1.361  qed "extend_localTo_guar_Increasing";
   1.362  
   1.363  Goal "F : Always A guarantees Always B \
   1.364  \ ==> extend h F : Always(extend_set h A) guarantees Always(extend_set h B)";
   1.365  by (etac project_guarantees 1);
   1.366 -by (etac (subset_refl RS project_Always_D) 2);
   1.367 -by (etac (subset_refl RS project_Always_I) 1);
   1.368 +by (rtac extending_Always 2);
   1.369 +by (rtac projecting_Always 1);
   1.370  qed "extend_guar_Always";
   1.371  
   1.372  
   1.373  (** Guarantees with a leadsTo postcondition **)
   1.374  
   1.375 +(*Bridges the gap between the "old" and "new" condition of the leadsTo rules*)
   1.376 +Goal "[| ALL x. project C h G ~: transient {x}; project C h G: transient D |] \
   1.377 +\     ==> F : transient D";
   1.378 +by (case_tac "D={}" 1);
   1.379 +by (auto_tac (claset() addIs [transient_strengthen], simpset()));
   1.380 +qed "transient_lemma";
   1.381 +
   1.382 +
   1.383 +(*Previously tried to prove
   1.384 +[| G : f localTo extend h F; project C h G : transient D |] ==> F : transient D
   1.385 +but it can fail if C removes some parts of an action of G.*)
   1.386 +
   1.387 +
   1.388  Goal "[| G : f localTo extend h F; \
   1.389  \        Disjoint (extend h F) G |] ==> project C h G : stable {x}";
   1.390  by (asm_full_simp_tac
   1.391 @@ -544,31 +693,50 @@
   1.392  				  stable_def, constrains_def]));
   1.393  qed "stable_sing_imp_not_transient";
   1.394  
   1.395 +by (auto_tac (claset(), 
   1.396 +	      simpset() addsimps [FP_def, transient_def,
   1.397 +				  stable_def, constrains_def]));
   1.398 +qed "stable_sing_imp_not_transient";
   1.399 +
   1.400  Goal "[| F Join project UNIV h G : A leadsTo B;    \
   1.401 -\        extend h F Join G : f localTo extend h F; \
   1.402 +\        G : f localTo extend h F; \
   1.403  \        Disjoint (extend h F) G |]  \
   1.404  \     ==> extend h F Join G : (extend_set h A) leadsTo (extend_set h B)";
   1.405  by (rtac project_UNIV_leadsTo_lemma 1);
   1.406 -by Auto_tac;
   1.407 -by (asm_full_simp_tac
   1.408 -    (simpset() addsimps [Join_localTo, self_localTo,
   1.409 -			 localTo_imp_project_stable, 
   1.410 -			 stable_sing_imp_not_transient]) 1);
   1.411 +by (Clarify_tac 1);
   1.412 +by (rtac transient_lemma 1);
   1.413 +by (auto_tac (claset(), 
   1.414 +	      simpset() addsimps [localTo_imp_project_stable, 
   1.415 +				  stable_sing_imp_not_transient]));
   1.416  qed "project_leadsTo_D";
   1.417  
   1.418 -
   1.419  Goal "[| F Join project (reachable (extend h F Join G)) h G : A LeadsTo B; \
   1.420 -\         extend h F Join G : f localTo extend h F; \
   1.421 -\         Disjoint (extend h F) G  |]  \
   1.422 +\         G : f localTo extend h F; \
   1.423 +\         Disjoint (extend h F) G |]  \
   1.424  \      ==> extend h F Join G : (extend_set h A) LeadsTo (extend_set h B)";
   1.425 -by (rtac Join_project_LeadsTo 1);
   1.426 -by Auto_tac;
   1.427 -by (asm_full_simp_tac
   1.428 -    (simpset() addsimps [Join_localTo, self_localTo,
   1.429 -			 localTo_imp_project_stable, 
   1.430 -			 stable_sing_imp_not_transient]) 1);
   1.431 +by (rtac (refl RS Join_project_LeadsTo) 1);
   1.432 +by (Clarify_tac 1);
   1.433 +by (rtac transient_lemma 1);
   1.434 +by (auto_tac (claset(), 
   1.435 +	      simpset() addsimps [localTo_imp_project_stable, 
   1.436 +				  stable_sing_imp_not_transient]));
   1.437  qed "project_LeadsTo_D";
   1.438  
   1.439 +Goalw [extending_def]
   1.440 +     "extending (%G. UNIV) h F \
   1.441 +\                (f localTo extend h F) \
   1.442 +\                (extend_set h A leadsTo extend_set h B) (A leadsTo B)";
   1.443 +by (blast_tac (claset() addSDs [Join_localTo RS iffD1]
   1.444 +			addIs [project_leadsTo_D]) 1);
   1.445 +qed "extending_leadsTo";
   1.446 +
   1.447 +Goalw [extending_def]
   1.448 +     "extending (%G. reachable (extend h F Join G)) h F \
   1.449 +\                (f localTo extend h F) \
   1.450 +\                (extend_set h A LeadsTo extend_set h B) (A LeadsTo B)";
   1.451 +by (blast_tac (claset() addSDs [Join_localTo RS iffD1]
   1.452 +			addIs [project_LeadsTo_D]) 1);
   1.453 +qed "extending_LeadsTo";
   1.454  
   1.455  (*STRONG precondition and postcondition*)
   1.456  Goal "F : (A co A') guarantees (B leadsTo B')  \
   1.457 @@ -576,10 +744,9 @@
   1.458  \                   Int (f localTo (extend h F)) \
   1.459  \                  guarantees ((extend_set h B) leadsTo (extend_set h B'))";
   1.460  by (etac project_guarantees 1);
   1.461 -(*the safety precondition*)
   1.462 -by (fast_tac (claset() addIs [project_constrains_I]) 1);
   1.463 -(*the liveness postcondition*)
   1.464 -by (fast_tac (claset() addIs [project_leadsTo_D]) 1);
   1.465 +by (rtac (extending_leadsTo RS extending_weaken) 2);
   1.466 +by (rtac (projecting_constrains RS projecting_weaken) 1);
   1.467 +by Auto_tac;
   1.468  qed "extend_co_guar_leadsTo";
   1.469  
   1.470  (*WEAK precondition and postcondition*)
   1.471 @@ -588,10 +755,9 @@
   1.472  \                   Int (f localTo (extend h F)) \
   1.473  \                  guarantees ((extend_set h B) LeadsTo (extend_set h B'))";
   1.474  by (etac project_guarantees 1);
   1.475 -(*the safety precondition*)
   1.476 -by (fast_tac (claset() addIs [project_Constrains_I]) 1);
   1.477 -(*the liveness postcondition*)
   1.478 -by (fast_tac (claset() addIs [project_LeadsTo_D]) 1);
   1.479 +by (rtac (extending_LeadsTo RS extending_weaken) 2);
   1.480 +by (rtac (projecting_Constrains RS projecting_weaken) 1);
   1.481 +by Auto_tac;
   1.482  qed "extend_Co_guar_LeadsTo";
   1.483  
   1.484  Close_locale "Extend";