working snapshot with new theory "Project"
authorpaulson
Wed Sep 29 13:13:06 1999 +0200 (1999-09-29)
changeset 7630d0e4a6f1f05c
parent 7629 68e155f81f88
child 7631 1b6b51b17c4a
working snapshot with new theory "Project"
src/HOL/UNITY/Alloc.thy
src/HOL/UNITY/Extend.ML
src/HOL/UNITY/Lift_prog.thy
src/HOL/UNITY/Project.ML
src/HOL/UNITY/Project.thy
src/HOL/UNITY/UNITY.ML
src/HOL/UNITY/Union.ML
     1.1 --- a/src/HOL/UNITY/Alloc.thy	Tue Sep 28 22:17:05 1999 +0200
     1.2 +++ b/src/HOL/UNITY/Alloc.thy	Wed Sep 29 13:13:06 1999 +0200
     1.3 @@ -10,7 +10,7 @@
     1.4    --but need invariants that values are non-negative
     1.5  *)
     1.6  
     1.7 -Alloc = Follows + Extend + PPROD +
     1.8 +Alloc = Follows + Project + PPROD +
     1.9  
    1.10  (*Duplicated from HOL/ex/NatSum.thy.
    1.11    Maybe type should be  [nat=>int, nat] => int**)
     2.1 --- a/src/HOL/UNITY/Extend.ML	Tue Sep 28 22:17:05 1999 +0200
     2.2 +++ b/src/HOL/UNITY/Extend.ML	Wed Sep 29 13:13:06 1999 +0200
     2.3 @@ -290,21 +290,6 @@
     2.4  qed "extend_JN";
     2.5  Addsimps [extend_JN];
     2.6  
     2.7 -Goal "UNIV <= project_set h C \
     2.8 -\     ==> project C h ((extend h F) Join G) = F Join (project C h G)";
     2.9 -by (rtac program_equalityI 1);
    2.10 -by (asm_simp_tac (simpset() addsimps [image_Un, image_image_eq_UN,
    2.11 -                   subset_UNIV RS subset_trans RS extend_act_inverse]) 2);
    2.12 -by (simp_tac (simpset() addsimps [project_set_extend_set_Int]) 1);
    2.13 -qed "project_extend_Join";
    2.14 -
    2.15 -Goal "UNIV <= project_set h C \
    2.16 -\     ==> (extend h F) Join G = extend h H ==> H = F Join (project C h G)";
    2.17 -by (dres_inst_tac [("f", "project C h")] arg_cong 1);
    2.18 -by (asm_full_simp_tac (simpset() addsimps [project_extend_Join]) 1);
    2.19 -qed "extend_Join_eq_extend_D";
    2.20 -
    2.21 -
    2.22  (*** Safety: co, stable ***)
    2.23  
    2.24  Goal "(extend h F : (extend_set h A) co (extend_set h B)) = \
    2.25 @@ -320,88 +305,9 @@
    2.26  by (asm_simp_tac (simpset() addsimps [invariant_def, extend_stable]) 1);
    2.27  qed "extend_invariant";
    2.28  
    2.29 -(** Safety and project **)
    2.30 -
    2.31 -Goalw [constrains_def]
    2.32 -     "(project C h F : A co B)  =  \
    2.33 -\     (F : (C Int extend_set h A) co (extend_set h B) & A <= B)";
    2.34 -by (auto_tac (claset() addSIs [project_act_I], simpset() addsimps [ball_Un]));
    2.35 -by (force_tac (claset() addSIs [project_act_I] addSDs [subsetD], simpset()) 1);
    2.36 -(*the <== direction*)
    2.37 -by (rewtac project_act_def);
    2.38 -by (force_tac (claset() addSDs [subsetD], simpset()) 1);
    2.39 -qed "project_constrains";
    2.40 -
    2.41 -Goalw [stable_def]
    2.42 -     "(project UNIV h F : stable A) = (F : stable (extend_set h A))";
    2.43 -by (simp_tac (simpset() addsimps [project_constrains]) 1);
    2.44 -qed "project_stable";
    2.45 -
    2.46 -(*This form's useful with guarantees reasoning*)
    2.47 -Goal "(F Join project C h G : A co B)  =  \
    2.48 -\       (extend h F Join G : (C Int extend_set h A) co (extend_set h B) &  \
    2.49 -\        F : A co B)";
    2.50 -by (simp_tac (simpset() addsimps [Join_constrains, project_constrains]) 1);
    2.51 -by (blast_tac (claset() addIs [extend_constrains RS iffD2 RS constrains_weaken]
    2.52 -                        addDs [constrains_imp_subset]) 1);
    2.53 -qed "Join_project_constrains";
    2.54 -
    2.55 -(*The condition is required to prove the left-to-right direction;
    2.56 -  could weaken it to G : (C Int extend_set h A) co C*)
    2.57 -Goalw [stable_def]
    2.58 -     "extend h F Join G : stable C \
    2.59 -\     ==> (F Join project C h G : stable A)  =  \
    2.60 -\         (extend h F Join G : stable (C Int extend_set h A) &  \
    2.61 -\          F : stable A)";
    2.62 -by (simp_tac (simpset() addsimps [Join_project_constrains]) 1);
    2.63 -by (blast_tac (claset() addIs [constrains_weaken] addDs [constrains_Int]) 1);
    2.64 -qed "Join_project_stable";
    2.65 -
    2.66 -Goal "(F Join project UNIV h G : increasing func)  =  \
    2.67 -\     (extend h F Join G : increasing (func o f))";
    2.68 -by (simp_tac (simpset() addsimps [increasing_def, Join_project_stable]) 1);
    2.69 -by (auto_tac (claset(),
    2.70 -	      simpset() addsimps [Join_stable, Collect_eq_extend_set RS sym,
    2.71 -				  extend_stable RS iffD1]));
    2.72 -qed "Join_project_increasing";
    2.73 -
    2.74  
    2.75  (*** Diff, needed for localTo ***)
    2.76  
    2.77 -(** project versions **)
    2.78 -
    2.79 -(*Opposite direction fails because Diff in the extended state may remove
    2.80 -  fewer actions, i.e. those that affect other state variables.*)
    2.81 -Goal "(UN act:acts. Domain act) <= project_set h C \
    2.82 -\     ==> Diff (project C h G) acts <= \
    2.83 -\         project C h (Diff G (extend_act h `` acts))";
    2.84 -by (asm_full_simp_tac (simpset() addsimps [component_eq_subset, Diff_def,
    2.85 -					   UN_subset_iff]) 1);
    2.86 -by (force_tac (claset() addSIs [image_diff_subset RS subsetD], 
    2.87 -	       simpset() addsimps [image_image_eq_UN]) 1);
    2.88 -qed "Diff_project_component_project_Diff";
    2.89 -
    2.90 -Goal
    2.91 -   "[| (UN act:acts. Domain act) <= project_set h C; \
    2.92 -\      Diff G (extend_act h `` acts) : (extend_set h A) co (extend_set h B) |]\
    2.93 -\   ==> Diff (project C h G) acts : A co B";
    2.94 -by (etac (Diff_project_component_project_Diff RS component_constrains) 1);
    2.95 -by (rtac (project_constrains RS iffD2) 1);
    2.96 -by (ftac constrains_imp_subset 1);
    2.97 -by (Asm_full_simp_tac 1);
    2.98 -by (blast_tac (claset() addIs [constrains_weaken]) 1);
    2.99 -qed "Diff_project_co";
   2.100 -
   2.101 -Goalw [stable_def]
   2.102 -     "[| (UN act:acts. Domain act) <= project_set h C; \
   2.103 -\        Diff G (extend_act h `` acts) : stable (extend_set h A) |] \
   2.104 -\     ==> Diff (project C h G) acts : stable A";
   2.105 -by (etac Diff_project_co 1);
   2.106 -by (assume_tac 1);
   2.107 -qed "Diff_project_stable";
   2.108 -
   2.109 -(** extend versions **)
   2.110 -
   2.111  Goal "(Diff (extend h G) (extend_act h `` acts)) = extend h (Diff G acts)";
   2.112  by (auto_tac (claset() addSIs [program_equalityI],
   2.113  	      simpset() addsimps [Diff_def,
   2.114 @@ -419,17 +325,6 @@
   2.115  by (simp_tac (simpset() addsimps [Diff_extend_co, stable_def]) 1);
   2.116  qed "Diff_extend_stable";
   2.117  
   2.118 -(*Converse appears to fail*)
   2.119 -Goal "[| UNIV <= project_set h C;  (H : (func o f) localTo extend h G) |] \
   2.120 -\     ==> (project C h H : func localTo G)";
   2.121 -by (asm_full_simp_tac 
   2.122 -    (simpset() addsimps [localTo_def, 
   2.123 -			 project_extend_Join RS sym,
   2.124 -			 subset_UNIV RS subset_trans RS Diff_project_stable,
   2.125 -			 Collect_eq_extend_set RS sym]) 1);
   2.126 -qed "project_localTo_I";
   2.127 -
   2.128 -
   2.129  (*** Weak safety primitives: Co, Stable ***)
   2.130  
   2.131  Goal "p : reachable (extend h F) ==> f p : reachable F";
   2.132 @@ -471,125 +366,6 @@
   2.133  qed "extend_Always";
   2.134  
   2.135  
   2.136 -(** Reachability and project **)
   2.137 -
   2.138 -Goal "[| reachable (extend h F Join G) <= C;  \
   2.139 -\        z : reachable (extend h F Join G) |] \
   2.140 -\     ==> f z : reachable (F Join project C h G)";
   2.141 -by (etac reachable.induct 1);
   2.142 -by (force_tac (claset() addIs [reachable.Init, project_set_I],
   2.143 -	       simpset()) 1);
   2.144 -by Auto_tac;
   2.145 -by (force_tac (claset() addIs [project_act_I RSN (3,reachable.Acts)],
   2.146 -	       simpset()) 2);
   2.147 -by (res_inst_tac [("act","x")] reachable.Acts 1);
   2.148 -by Auto_tac;
   2.149 -by (etac extend_act_D 1);
   2.150 -qed "reachable_imp_reachable_project";
   2.151 -
   2.152 -Goalw [Constrains_def]
   2.153 -     "[| reachable (extend h F Join G) <= C;    \
   2.154 -\        F Join project C h G : A Co B |] \
   2.155 -\     ==> extend h F Join G : (extend_set h A) Co (extend_set h B)";
   2.156 -by (full_simp_tac (simpset() addsimps [Join_project_constrains]) 1);
   2.157 -by (Clarify_tac 1);
   2.158 -by (etac constrains_weaken 1);
   2.159 -by (auto_tac (claset() addDs [reachable_imp_reachable_project], simpset()));
   2.160 -qed "project_Constrains_D";
   2.161 -
   2.162 -Goalw [Stable_def]
   2.163 -     "[| reachable (extend h F Join G) <= C;  \
   2.164 -\        F Join project C h G : Stable A |]   \
   2.165 -\     ==> extend h F Join G : Stable (extend_set h A)";
   2.166 -by (asm_simp_tac (simpset() addsimps [project_Constrains_D]) 1);
   2.167 -qed "project_Stable_D";
   2.168 -
   2.169 -Goalw [Always_def]
   2.170 -     "[| reachable (extend h F Join G) <= C;  \
   2.171 -\        F Join project C h G : Always A |]   \
   2.172 -\     ==> extend h F Join G : Always (extend_set h A)";
   2.173 -by (force_tac (claset() addIs [reachable.Init, project_set_I],
   2.174 -	       simpset() addsimps [project_Stable_D]) 1);
   2.175 -qed "project_Always_D";
   2.176 -
   2.177 -Goalw [Increasing_def]
   2.178 -     "[| reachable (extend h F Join G) <= C;  \
   2.179 -\        F Join project C h G : Increasing func |] \
   2.180 -\     ==> extend h F Join G : Increasing (func o f)";
   2.181 -by Auto_tac;
   2.182 -by (stac Collect_eq_extend_set 1);
   2.183 -by (asm_simp_tac (simpset() addsimps [project_Stable_D]) 1); 
   2.184 -qed "project_Increasing_D";
   2.185 -
   2.186 -
   2.187 -(** Converse results for weak safety: benefits of the argument C *)
   2.188 -
   2.189 -Goal "[| C <= reachable(extend h F Join G);   \
   2.190 -\        x : reachable (F Join project C h G) |] \
   2.191 -\     ==> EX y. h(x,y) : reachable (extend h F Join G)";
   2.192 -by (etac reachable.induct 1);
   2.193 -by (ALLGOALS Asm_full_simp_tac);
   2.194 -(*SLOW: 6.7s*)
   2.195 -by (force_tac (claset() delrules [Id_in_Acts]
   2.196 -		        addIs [reachable.Acts, extend_act_D],
   2.197 -	       simpset() addsimps [project_act_def]) 2);
   2.198 -by (force_tac (claset() addIs [reachable.Init],
   2.199 -	       simpset() addsimps [project_set_def]) 1);
   2.200 -qed "reachable_project_imp_reachable";
   2.201 -
   2.202 -Goalw [Constrains_def]
   2.203 -     "[| C <= reachable (extend h F Join G);  \
   2.204 -\        extend h F Join G : (extend_set h A) Co (extend_set h B) |] \
   2.205 -\     ==> F Join project C h G : A Co B";
   2.206 -by (full_simp_tac (simpset() addsimps [Join_project_constrains, 
   2.207 -				       extend_set_Int_distrib]) 1);
   2.208 -by (rtac conjI 1);
   2.209 -by (etac constrains_weaken 1);
   2.210 -by Auto_tac;
   2.211 -by (asm_full_simp_tac (simpset() addsimps [Join_constrains]) 1);
   2.212 -(*Some generalization of constrains_weaken_L would be better, but what is it?*)
   2.213 -by (rewtac constrains_def);
   2.214 -by Auto_tac;
   2.215 -by (thin_tac "ALL act : Acts G. ?P act" 1);
   2.216 -by (force_tac (claset() addSDs [reachable_project_imp_reachable], 
   2.217 -	       simpset()) 1);
   2.218 -qed "project_Constrains_I";
   2.219 -
   2.220 -Goalw [Stable_def]
   2.221 -     "[| C <= reachable (extend h F Join G);  \
   2.222 -\        extend h F Join G : Stable (extend_set h A) |] \
   2.223 -\     ==> F Join project C h G : Stable A";
   2.224 -by (asm_simp_tac (simpset() addsimps [project_Constrains_I]) 1);
   2.225 -qed "project_Stable_I";
   2.226 -
   2.227 -Goalw [Increasing_def]
   2.228 -     "[| C <= reachable (extend h F Join G);  \
   2.229 -\        extend h F Join G : Increasing (func o f) |] \
   2.230 -\     ==> F Join project C h G : Increasing func";
   2.231 -by Auto_tac;
   2.232 -by (asm_simp_tac (simpset() addsimps [Collect_eq_extend_set RS sym,
   2.233 -				      project_Stable_I]) 1); 
   2.234 -qed "project_Increasing_I";
   2.235 -
   2.236 -Goal "(F Join project (reachable (extend h F Join G)) h G : A Co B)  =  \
   2.237 -\     (extend h F Join G : (extend_set h A) Co (extend_set h B))";
   2.238 -by (blast_tac (claset() addIs [project_Constrains_I, project_Constrains_D]) 1);
   2.239 -qed "project_Constrains";
   2.240 -
   2.241 -Goalw [Stable_def]
   2.242 -     "(F Join project (reachable (extend h F Join G)) h G : Stable A)  =  \
   2.243 -\     (extend h F Join G : Stable (extend_set h A))";
   2.244 -by (rtac project_Constrains 1);
   2.245 -qed "project_Stable";
   2.246 -
   2.247 -Goal
   2.248 -   "(F Join project (reachable (extend h F Join G)) h G : Increasing func)  = \
   2.249 -\   (extend h F Join G : Increasing (func o f))";
   2.250 -by (asm_simp_tac (simpset() addsimps [Increasing_def, project_Stable,
   2.251 -				      Collect_eq_extend_set RS sym]) 1);
   2.252 -qed "project_Increasing";
   2.253 -
   2.254 -
   2.255  (*** Progress: transient, ensures ***)
   2.256  
   2.257  Goal "(extend h F : transient (extend_set h A)) = (F : transient A)";
   2.258 @@ -687,221 +463,6 @@
   2.259  qed "extend_LeadsTo";
   2.260  
   2.261  
   2.262 -(** Progress includes safety in the definition of ensures **)
   2.263 -
   2.264 -(*** Progress for (project C h F) ***)
   2.265 -
   2.266 -(** transient **)
   2.267 -
   2.268 -(*Premise is that C includes the domains of all actions that could be the
   2.269 -  transient one.  Could have C=UNIV of course*)
   2.270 -Goalw [transient_def]
   2.271 -     "[| ALL act: Acts F. act ^^ extend_set h A <= - extend_set h A --> \
   2.272 -\                      Domain act <= C;    \
   2.273 -\        F : transient (extend_set h A) |] \
   2.274 -\     ==> project C h F : transient A";
   2.275 -by (auto_tac (claset() delrules [ballE],
   2.276 -              simpset() addsimps [Domain_project_act, Int_absorb2]));
   2.277 -by (REPEAT (ball_tac 1));
   2.278 -by (auto_tac (claset(),
   2.279 -              simpset() addsimps [extend_set_def, project_set_def, 
   2.280 -				  project_act_def]));
   2.281 -by (ALLGOALS Blast_tac);
   2.282 -qed "transient_extend_set_imp_project_transient";
   2.283 -
   2.284 -
   2.285 -(*Converse of the above...it requires a strong assumption about actions
   2.286 -  being enabled for all possible values of the new variables.*)
   2.287 -Goalw [transient_def]
   2.288 -     "[| project C h F : transient A;  \
   2.289 -\        ALL act: Acts F. project_act C h act ^^ A <= - A --> \
   2.290 -\                         Domain act <= C \
   2.291 -\             & extend_set h (project_set h (Domain act)) <= Domain act |]  \
   2.292 -\     ==> F : transient (extend_set h A)";
   2.293 -by (auto_tac (claset() delrules [ballE],
   2.294 -	      simpset() addsimps [Domain_project_act]));
   2.295 -by (ball_tac 1);
   2.296 -by (rtac bexI 1);
   2.297 -by (assume_tac 2);
   2.298 -by Auto_tac;
   2.299 -by (eres_inst_tac [("P", "A <= ?B")] rev_mp 1);
   2.300 -by (force_tac (claset(), simpset() addsimps [Int_absorb2]) 1);
   2.301 -(*The Domain requirement's proved; must prove the Image requirement*)
   2.302 -by (res_inst_tac [("y1", "x")] (surj_h RS surjD RS exE) 1);
   2.303 -by (res_inst_tac [("y1", "xa")] (surj_h RS surjD RS exE) 1);
   2.304 -by Auto_tac;
   2.305 -by (thin_tac "A <= ?B" 1);
   2.306 -by (force_tac (claset() addSIs [ImageI, project_act_I], simpset()) 1);
   2.307 -qed "project_transient_imp_transient_extend_set";
   2.308 -
   2.309 -
   2.310 -(** ensures **)
   2.311 -
   2.312 -(*For simplicity, the complicated condition on C is eliminated
   2.313 -  NOT SURE THIS IS GOOD FOR ANYTHING: CAN'T PROVE LEADSTO THEOREM*)
   2.314 -Goal "F : (extend_set h A) ensures (extend_set h B) \
   2.315 -\     ==> project UNIV h F : A ensures B";
   2.316 -by (asm_full_simp_tac
   2.317 -    (simpset() addsimps [ensures_def, project_constrains, 
   2.318 -			 transient_extend_set_imp_project_transient,
   2.319 -			 extend_set_Un_distrib RS sym, 
   2.320 -			 extend_set_Diff_distrib RS sym]) 1);
   2.321 -by (Blast_tac 1);
   2.322 -qed "ensures_extend_set_imp_project_ensures";
   2.323 -
   2.324 -(*A super-strong condition: G is not allowed to affect the
   2.325 -  shared variables at all.*)
   2.326 -Goal "[| ALL x. project UNIV h G ~: transient {x};  \
   2.327 -\        F Join project UNIV h G : A ensures B |] \
   2.328 -\     ==> extend h F Join G : (extend_set h A) ensures (extend_set h B)";
   2.329 -by (case_tac "A <= B" 1);
   2.330 -by (etac (extend_set_mono RS subset_imp_ensures) 1);
   2.331 -by (asm_full_simp_tac
   2.332 -    (simpset() addsimps [ensures_def, extend_constrains, extend_transient, 
   2.333 -			 extend_set_Un_distrib RS sym, 
   2.334 -			 extend_set_Diff_distrib RS sym,
   2.335 -			 Join_transient, Join_constrains,
   2.336 -			 project_constrains, Int_absorb1]) 1);
   2.337 -(*otherwise PROOF FAILED*)
   2.338 -by Auto_tac;
   2.339 -by (blast_tac (claset() addIs [transient_strengthen]) 1);
   2.340 -qed_spec_mp "Join_project_ensures";
   2.341 -
   2.342 -Goal "[| ALL x. project UNIV h G ~: transient {x};  \
   2.343 -\        F Join project UNIV h G : A leadsTo B |] \
   2.344 -\     ==> extend h F Join G : (extend_set h A) leadsTo (extend_set h B)";
   2.345 -by (etac leadsTo_induct 1);
   2.346 -by (asm_simp_tac (simpset() addsimps [leadsTo_UN, extend_set_Union]) 3);
   2.347 -by (blast_tac (claset() addIs [leadsTo_Trans]) 2);
   2.348 -by (blast_tac (claset() addIs [leadsTo_Basis, Join_project_ensures]) 1);
   2.349 -qed "Join_project_leadsTo_I";
   2.350 -
   2.351 -
   2.352 -
   2.353 -Goal "F : stable{s} ==> F ~: transient {s}";
   2.354 -by (auto_tac (claset(), 
   2.355 -	      simpset() addsimps [FP_def, transient_def,
   2.356 -				  stable_def, constrains_def]));
   2.357 -qed "stable_sing_imp_not_transient";
   2.358 -
   2.359 -
   2.360 -(** Strong precondition and postcondition; doesn't seem very useful. **)
   2.361 -
   2.362 -Goal "F : X guarantees Y ==> \
   2.363 -\     extend h F : (extend h `` X) guarantees (extend h `` Y)";
   2.364 -by (rtac guaranteesI 1);
   2.365 -by Auto_tac;
   2.366 -by (blast_tac (claset() addDs [project_set_UNIV RS extend_Join_eq_extend_D, 
   2.367 -			       guaranteesD]) 1);
   2.368 -qed "guarantees_imp_extend_guarantees";
   2.369 -
   2.370 -Goal "extend h F : (extend h `` X) guarantees (extend h `` Y) \
   2.371 -\    ==> F : X guarantees Y";
   2.372 -by (rtac guaranteesI 1);
   2.373 -by (auto_tac (claset(), simpset() addsimps [guar_def, component_def]));
   2.374 -by (dtac spec 1);
   2.375 -by (dtac (mp RS mp) 1);
   2.376 -by (Blast_tac 2);
   2.377 -by (blast_tac (claset() addSDs [inj_extend RS inj_image_mem_iff RS iffD1]) 2);
   2.378 -by Auto_tac;
   2.379 -qed "extend_guarantees_imp_guarantees";
   2.380 -
   2.381 -Goal "(extend h F : (extend h `` X) guarantees (extend h `` Y)) = \
   2.382 -\    (F : X guarantees Y)";
   2.383 -by (blast_tac (claset() addIs [guarantees_imp_extend_guarantees,
   2.384 -			       extend_guarantees_imp_guarantees]) 1);
   2.385 -qed "extend_guarantees_eq";
   2.386 -
   2.387 -(*Weak precondition and postcondition; this is the good one!
   2.388 -  Not clear that it has a converse [or that we want one!]*)
   2.389 -val [xguary,project,extend] =
   2.390 -Goal "[| F : X guarantees Y;  \
   2.391 -\        !!G. extend h F Join G : X' ==> F Join proj G h G : X;  \
   2.392 -\        !!G. [| F Join proj G h G : Y; extend h F Join G : X'; \
   2.393 -\                Disjoint (extend h F) G |] \
   2.394 -\             ==> extend h F Join G : Y' |] \
   2.395 -\     ==> extend h F : X' guarantees Y'";
   2.396 -by (rtac (xguary RS guaranteesD RS extend RS guaranteesI) 1);
   2.397 -by (etac project 1);
   2.398 -by (assume_tac 1);
   2.399 -by (assume_tac 1);
   2.400 -qed "project_guarantees";
   2.401 -
   2.402 -(** It seems that neither "guarantees" law can be proved from the other. **)
   2.403 -
   2.404 -
   2.405 -(*** guarantees corollaries ***)
   2.406 -
   2.407 -Goal "F : UNIV guarantees increasing func \
   2.408 -\     ==> extend h F : UNIV guarantees increasing (func o f)";
   2.409 -by (etac project_guarantees 1);
   2.410 -by (ALLGOALS
   2.411 -    (asm_simp_tac (simpset() addsimps [Join_project_increasing RS sym])));
   2.412 -qed "extend_guar_increasing";
   2.413 -
   2.414 -Goal "F : UNIV guarantees Increasing func \
   2.415 -\     ==> extend h F : UNIV guarantees Increasing (func o f)";
   2.416 -by (etac project_guarantees 1);
   2.417 -by (rtac (subset_UNIV RS project_Increasing_D) 2);
   2.418 -by Auto_tac;
   2.419 -qed "extend_guar_Increasing";
   2.420 -
   2.421 -Goal "F : (func localTo G) guarantees increasing func  \
   2.422 -\     ==> extend h F : (func o f) localTo (extend h G)  \
   2.423 -\                      guarantees increasing (func o f)";
   2.424 -by (etac project_guarantees 1);
   2.425 -(*the "increasing" guarantee*)
   2.426 -by (asm_simp_tac
   2.427 -    (simpset() addsimps [Join_project_increasing RS sym]) 2);
   2.428 -(*the "localTo" requirement*)
   2.429 -by (stac (project_set_UNIV RS project_extend_Join RS sym) 1);
   2.430 -by (asm_simp_tac 
   2.431 -    (simpset() addsimps [project_set_UNIV RS project_localTo_I]) 1);
   2.432 -qed "extend_localTo_guar_increasing";
   2.433 -
   2.434 -Goal "F : (func localTo G) guarantees Increasing func  \
   2.435 -\     ==> extend h F : (func o f) localTo (extend h G)  \
   2.436 -\                      guarantees Increasing (func o f)";
   2.437 -by (etac project_guarantees 1);
   2.438 -(*the "Increasing" guarantee*)
   2.439 -by (etac (subset_UNIV RS project_Increasing_D) 2);
   2.440 -(*the "localTo" requirement*)
   2.441 -by (stac (project_set_UNIV RS project_extend_Join RS sym) 1);
   2.442 -by (asm_simp_tac 
   2.443 -    (simpset() addsimps [project_set_UNIV RS project_localTo_I]) 1);
   2.444 -qed "extend_localTo_guar_Increasing";
   2.445 -
   2.446 -
   2.447 -(** Guarantees with a leadsTo postcondition **)
   2.448 -
   2.449 -Goal "[| G : f localTo extend h F; \
   2.450 -\        Disjoint (extend h F) G |] ==> project UNIV h G : stable {x}";
   2.451 -by (asm_full_simp_tac
   2.452 -    (simpset() addsimps [localTo_imp_stable,
   2.453 -			 extend_set_sing, project_stable]) 1);
   2.454 -qed "localTo_imp_project_stable";
   2.455 -
   2.456 -
   2.457 -Goal "F : (A co A') guarantees (B leadsTo B')  \
   2.458 -\ ==> extend h F : ((extend_set h A) co (extend_set h A'))  \
   2.459 -\                   Int (f localTo (extend h F)) \
   2.460 -\                  guarantees ((extend_set h B) leadsTo (extend_set h B'))";
   2.461 -by (etac project_guarantees 1);
   2.462 -(*the safety precondition*)
   2.463 -by (stac (project_set_UNIV RS project_extend_Join RS sym) 1);
   2.464 -by (asm_full_simp_tac
   2.465 -    (simpset() addsimps [project_constrains, Join_constrains, 
   2.466 -			 extend_constrains]) 1);
   2.467 -by (fast_tac (claset() addDs [constrains_imp_subset]) 1);
   2.468 -(*the liveness postcondition*)
   2.469 -by (rtac Join_project_leadsTo_I 1);
   2.470 -by Auto_tac;
   2.471 -by (asm_full_simp_tac
   2.472 -    (simpset() addsimps [Join_localTo, self_localTo,
   2.473 -			 localTo_imp_project_stable, stable_sing_imp_not_transient]) 1);
   2.474 -qed "extend_co_guar_leadsTo";
   2.475 -
   2.476 -
   2.477  Close_locale "Extend";
   2.478  
   2.479  (*Close_locale should do this!
     3.1 --- a/src/HOL/UNITY/Lift_prog.thy	Tue Sep 28 22:17:05 1999 +0200
     3.2 +++ b/src/HOL/UNITY/Lift_prog.thy	Wed Sep 29 13:13:06 1999 +0200
     3.3 @@ -6,7 +6,7 @@
     3.4  lift_prog, etc: replication of components
     3.5  *)
     3.6  
     3.7 -Lift_prog = Guar + Extend +
     3.8 +Lift_prog = Project +
     3.9  
    3.10  constdefs
    3.11  
     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/HOL/UNITY/Project.ML	Wed Sep 29 13:13:06 1999 +0200
     4.3 @@ -0,0 +1,501 @@
     4.4 +(*  Title:      HOL/UNITY/Project.ML
     4.5 +    ID:         $Id$
     4.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4.7 +    Copyright   1999  University of Cambridge
     4.8 +
     4.9 +Projections of state sets (also of actions and programs)
    4.10 +
    4.11 +Inheritance of GUARANTEES properties under extension
    4.12 +*)
    4.13 +
    4.14 +Open_locale "Extend";
    4.15 +
    4.16 +Goalw [restr_def] "Init (restr C h F) = Init F";
    4.17 +by Auto_tac;
    4.18 +qed "Init_restr";
    4.19 +
    4.20 +Goalw [restr_act_def, extend_act_def, project_act_def]
    4.21 +     "((x,x') : restr_act C h act) = ((x,x') : act & (EX y. h(x,y) : C))";
    4.22 +by (Blast_tac 1);
    4.23 +qed "restr_act_iff";
    4.24 +Addsimps [restr_act_iff];
    4.25 +
    4.26 +Goal "Acts (restr C h F) = insert Id (restr_act C h `` Acts F)";
    4.27 +by (auto_tac (claset(), 
    4.28 +	      simpset() addsimps [restr_def, symmetric restr_act_def, 
    4.29 +				  image_image_eq_UN]));
    4.30 +qed "Acts_restr";
    4.31 +
    4.32 +Addsimps [Init_restr, Acts_restr];
    4.33 +
    4.34 +(*The definitions are RE-ORIENTED*)
    4.35 +Addsimps [symmetric restr_act_def, symmetric restr_def];
    4.36 +
    4.37 +Goal "project C h ((extend h F) Join G) = (restr C h F) Join (project C h G)";
    4.38 +by (rtac program_equalityI 1);
    4.39 +by (asm_simp_tac (simpset() addsimps [symmetric restr_act_def,
    4.40 +				      image_Un, image_image]) 2);
    4.41 +by (simp_tac (simpset() addsimps [project_set_extend_set_Int]) 1);
    4.42 +qed "project_extend_Join_restr";
    4.43 +
    4.44 +Goalw [project_set_def]
    4.45 + "Domain act <= project_set h C ==> restr_act C h act = act";
    4.46 +by (Force_tac 1);
    4.47 +qed "restr_act_ident";
    4.48 +Addsimps [restr_act_ident];
    4.49 +
    4.50 +Goal "F : A co B ==> restr C h F : A co B";
    4.51 +by (auto_tac (claset(), simpset() addsimps [constrains_def]));
    4.52 +by (Blast_tac 1);
    4.53 +qed "restr_constrains";
    4.54 +
    4.55 +Goal "F : stable A ==> restr C h F : stable A";
    4.56 +by (asm_full_simp_tac (simpset() addsimps [stable_def, restr_constrains]) 1);
    4.57 +qed "restr_stable";
    4.58 +
    4.59 +Goal "UNIV <= project_set h C ==> restr C h F = F";
    4.60 +by (rtac program_equalityI 1);
    4.61 +by (force_tac (claset(),
    4.62 +	       simpset() addsimps [image_def,
    4.63 +                   subset_UNIV RS subset_trans RS restr_act_ident]) 2);
    4.64 +by (Simp_tac 1);
    4.65 +qed "restr_ident";
    4.66 +
    4.67 +(*Ideally, uses of this should be eliminated.  But often we see it re-oriented
    4.68 +  as project_extend_Join RS sym*)
    4.69 +Goal "UNIV <= project_set h C \
    4.70 +\     ==> project C h ((extend h F) Join G) = F Join (project C h G)";
    4.71 +by (asm_simp_tac (simpset() addsimps [project_extend_Join_restr, 
    4.72 +				      restr_ident]) 1);
    4.73 +qed "project_extend_Join";
    4.74 +
    4.75 +Goal "UNIV <= project_set h C \
    4.76 +\     ==> (extend h F) Join G = extend h H ==> H = F Join (project C h G)";
    4.77 +by (dres_inst_tac [("f", "project C h")] arg_cong 1);
    4.78 +by (asm_full_simp_tac (simpset() addsimps [project_extend_Join_restr, 
    4.79 +					   restr_ident]) 1);
    4.80 +qed "extend_Join_eq_extend_D";
    4.81 +
    4.82 +
    4.83 +(** Safety **)
    4.84 +
    4.85 +Goalw [constrains_def]
    4.86 +     "(project C h F : A co B)  =  \
    4.87 +\     (F : (C Int extend_set h A) co (extend_set h B) & A <= B)";
    4.88 +by (auto_tac (claset() addSIs [project_act_I], simpset() addsimps [ball_Un]));
    4.89 +by (force_tac (claset() addSIs [project_act_I] addSDs [subsetD], simpset()) 1);
    4.90 +(*the <== direction*)
    4.91 +by (rewtac project_act_def);
    4.92 +by (force_tac (claset() addSDs [subsetD], simpset()) 1);
    4.93 +qed "project_constrains";
    4.94 +
    4.95 +Goalw [stable_def]
    4.96 +     "(project UNIV h F : stable A) = (F : stable (extend_set h A))";
    4.97 +by (simp_tac (simpset() addsimps [project_constrains]) 1);
    4.98 +qed "project_stable";
    4.99 +
   4.100 +(*This form's useful with guarantees reasoning*)
   4.101 +Goal "(F Join project C h G : A co B)  =  \
   4.102 +\       (extend h F Join G : (C Int extend_set h A) co (extend_set h B) &  \
   4.103 +\        F : A co B)";
   4.104 +by (simp_tac (simpset() addsimps [Join_constrains, project_constrains]) 1);
   4.105 +by (blast_tac (claset() addIs [extend_constrains RS iffD2 RS constrains_weaken]
   4.106 +                        addDs [constrains_imp_subset]) 1);
   4.107 +qed "Join_project_constrains";
   4.108 +
   4.109 +(*The condition is required to prove the left-to-right direction;
   4.110 +  could weaken it to G : (C Int extend_set h A) co C*)
   4.111 +Goalw [stable_def]
   4.112 +     "extend h F Join G : stable C \
   4.113 +\     ==> (F Join project C h G : stable A)  =  \
   4.114 +\         (extend h F Join G : stable (C Int extend_set h A) &  \
   4.115 +\          F : stable A)";
   4.116 +by (simp_tac (simpset() addsimps [Join_project_constrains]) 1);
   4.117 +by (blast_tac (claset() addIs [constrains_weaken] addDs [constrains_Int]) 1);
   4.118 +qed "Join_project_stable";
   4.119 +
   4.120 +Goal "(F Join project UNIV h G : increasing func)  =  \
   4.121 +\     (extend h F Join G : increasing (func o f))";
   4.122 +by (simp_tac (simpset() addsimps [increasing_def, Join_project_stable]) 1);
   4.123 +by (auto_tac (claset(),
   4.124 +	      simpset() addsimps [Join_stable, Collect_eq_extend_set RS sym,
   4.125 +				  extend_stable RS iffD1]));
   4.126 +qed "Join_project_increasing";
   4.127 +
   4.128 +
   4.129 +(*** Diff, needed for localTo ***)
   4.130 +
   4.131 +(*Opposite direction fails because Diff in the extended state may remove
   4.132 +  fewer actions, i.e. those that affect other state variables.*)
   4.133 +Goal "(UN act:acts. Domain act) <= project_set h C \
   4.134 +\     ==> Diff (project C h G) acts <= \
   4.135 +\         project C h (Diff G (extend_act h `` acts))";
   4.136 +by (asm_full_simp_tac (simpset() addsimps [component_eq_subset, Diff_def,
   4.137 +					   UN_subset_iff]) 1);
   4.138 +by (force_tac (claset() addSIs [image_diff_subset RS subsetD], 
   4.139 +	       simpset() addsimps [image_image_eq_UN]) 1);
   4.140 +qed "Diff_project_component_project_Diff";
   4.141 +
   4.142 +Goal
   4.143 +   "[| (UN act:acts. Domain act) <= project_set h C; \
   4.144 +\      Diff G (extend_act h `` acts) : (extend_set h A) co (extend_set h B) |]\
   4.145 +\   ==> Diff (project C h G) acts : A co B";
   4.146 +by (etac (Diff_project_component_project_Diff RS component_constrains) 1);
   4.147 +by (rtac (project_constrains RS iffD2) 1);
   4.148 +by (ftac constrains_imp_subset 1);
   4.149 +by (Asm_full_simp_tac 1);
   4.150 +by (blast_tac (claset() addIs [constrains_weaken]) 1);
   4.151 +qed "Diff_project_co";
   4.152 +
   4.153 +Goalw [stable_def]
   4.154 +     "[| (UN act:acts. Domain act) <= project_set h C; \
   4.155 +\        Diff G (extend_act h `` acts) : stable (extend_set h A) |] \
   4.156 +\     ==> Diff (project C h G) acts : stable A";
   4.157 +by (etac Diff_project_co 1);
   4.158 +by (assume_tac 1);
   4.159 +qed "Diff_project_stable";
   4.160 +
   4.161 +(*Converse appears to fail*)
   4.162 +Goal "[| UNIV <= project_set h C;  (H : (func o f) localTo extend h G) |] \
   4.163 +\     ==> (project C h H : func localTo G)";
   4.164 +by (asm_full_simp_tac 
   4.165 +    (simpset() addsimps [localTo_def, 
   4.166 +			 project_extend_Join RS sym,
   4.167 +			 subset_UNIV RS subset_trans RS Diff_project_stable,
   4.168 +			 Collect_eq_extend_set RS sym]) 1);
   4.169 +qed "project_localTo_I";
   4.170 +
   4.171 +
   4.172 +(** Reachability and project **)
   4.173 +
   4.174 +Goal "[| reachable (extend h F Join G) <= C;  \
   4.175 +\        z : reachable (extend h F Join G) |] \
   4.176 +\     ==> f z : reachable (F Join project C h G)";
   4.177 +by (etac reachable.induct 1);
   4.178 +by (force_tac (claset() addIs [reachable.Init, project_set_I],
   4.179 +	       simpset()) 1);
   4.180 +by Auto_tac;
   4.181 +by (force_tac (claset() addIs [project_act_I RSN (3,reachable.Acts)],
   4.182 +	       simpset()) 2);
   4.183 +by (res_inst_tac [("act","x")] reachable.Acts 1);
   4.184 +by Auto_tac;
   4.185 +by (etac extend_act_D 1);
   4.186 +qed "reachable_imp_reachable_project";
   4.187 +
   4.188 +Goalw [Constrains_def]
   4.189 +     "[| reachable (extend h F Join G) <= C;    \
   4.190 +\        F Join project C h G : A Co B |] \
   4.191 +\     ==> extend h F Join G : (extend_set h A) Co (extend_set h B)";
   4.192 +by (full_simp_tac (simpset() addsimps [Join_project_constrains]) 1);
   4.193 +by (Clarify_tac 1);
   4.194 +by (etac constrains_weaken 1);
   4.195 +by (auto_tac (claset() addDs [reachable_imp_reachable_project], simpset()));
   4.196 +qed "project_Constrains_D";
   4.197 +
   4.198 +Goalw [Stable_def]
   4.199 +     "[| reachable (extend h F Join G) <= C;  \
   4.200 +\        F Join project C h G : Stable A |]   \
   4.201 +\     ==> extend h F Join G : Stable (extend_set h A)";
   4.202 +by (asm_simp_tac (simpset() addsimps [project_Constrains_D]) 1);
   4.203 +qed "project_Stable_D";
   4.204 +
   4.205 +Goalw [Always_def]
   4.206 +     "[| reachable (extend h F Join G) <= C;  \
   4.207 +\        F Join project C h G : Always A |]   \
   4.208 +\     ==> extend h F Join G : Always (extend_set h A)";
   4.209 +by (force_tac (claset() addIs [reachable.Init, project_set_I],
   4.210 +	       simpset() addsimps [project_Stable_D]) 1);
   4.211 +qed "project_Always_D";
   4.212 +
   4.213 +Goalw [Increasing_def]
   4.214 +     "[| reachable (extend h F Join G) <= C;  \
   4.215 +\        F Join project C h G : Increasing func |] \
   4.216 +\     ==> extend h F Join G : Increasing (func o f)";
   4.217 +by Auto_tac;
   4.218 +by (stac Collect_eq_extend_set 1);
   4.219 +by (asm_simp_tac (simpset() addsimps [project_Stable_D]) 1); 
   4.220 +qed "project_Increasing_D";
   4.221 +
   4.222 +
   4.223 +(** Converse results for weak safety: benefits of the argument C *)
   4.224 +
   4.225 +Goal "[| C <= reachable(extend h F Join G);   \
   4.226 +\        x : reachable (F Join project C h G) |] \
   4.227 +\     ==> EX y. h(x,y) : reachable (extend h F Join G)";
   4.228 +by (etac reachable.induct 1);
   4.229 +by (ALLGOALS Asm_full_simp_tac);
   4.230 +(*SLOW: 6.7s*)
   4.231 +by (force_tac (claset() delrules [Id_in_Acts]
   4.232 +		        addIs [reachable.Acts, extend_act_D],
   4.233 +	       simpset() addsimps [project_act_def]) 2);
   4.234 +by (force_tac (claset() addIs [reachable.Init],
   4.235 +	       simpset() addsimps [project_set_def]) 1);
   4.236 +qed "reachable_project_imp_reachable";
   4.237 +
   4.238 +Goalw [Constrains_def]
   4.239 +     "[| C <= reachable (extend h F Join G);  \
   4.240 +\        extend h F Join G : (extend_set h A) Co (extend_set h B) |] \
   4.241 +\     ==> F Join project C h G : A Co B";
   4.242 +by (full_simp_tac (simpset() addsimps [Join_project_constrains, 
   4.243 +				       extend_set_Int_distrib]) 1);
   4.244 +by (rtac conjI 1);
   4.245 +by (etac constrains_weaken 1);
   4.246 +by Auto_tac;
   4.247 +by (asm_full_simp_tac (simpset() addsimps [Join_constrains]) 1);
   4.248 +(*Some generalization of constrains_weaken_L would be better, but what is it?*)
   4.249 +by (rewtac constrains_def);
   4.250 +by Auto_tac;
   4.251 +by (thin_tac "ALL act : Acts G. ?P act" 1);
   4.252 +by (force_tac (claset() addSDs [reachable_project_imp_reachable], 
   4.253 +	       simpset()) 1);
   4.254 +qed "project_Constrains_I";
   4.255 +
   4.256 +Goalw [Stable_def]
   4.257 +     "[| C <= reachable (extend h F Join G);  \
   4.258 +\        extend h F Join G : Stable (extend_set h A) |] \
   4.259 +\     ==> F Join project C h G : Stable A";
   4.260 +by (asm_simp_tac (simpset() addsimps [project_Constrains_I]) 1);
   4.261 +qed "project_Stable_I";
   4.262 +
   4.263 +Goalw [Increasing_def]
   4.264 +     "[| C <= reachable (extend h F Join G);  \
   4.265 +\        extend h F Join G : Increasing (func o f) |] \
   4.266 +\     ==> F Join project C h G : Increasing func";
   4.267 +by Auto_tac;
   4.268 +by (asm_simp_tac (simpset() addsimps [Collect_eq_extend_set RS sym,
   4.269 +				      project_Stable_I]) 1); 
   4.270 +qed "project_Increasing_I";
   4.271 +
   4.272 +Goal "(F Join project (reachable (extend h F Join G)) h G : A Co B)  =  \
   4.273 +\     (extend h F Join G : (extend_set h A) Co (extend_set h B))";
   4.274 +by (blast_tac (claset() addIs [project_Constrains_I, project_Constrains_D]) 1);
   4.275 +qed "project_Constrains";
   4.276 +
   4.277 +Goalw [Stable_def]
   4.278 +     "(F Join project (reachable (extend h F Join G)) h G : Stable A)  =  \
   4.279 +\     (extend h F Join G : Stable (extend_set h A))";
   4.280 +by (rtac project_Constrains 1);
   4.281 +qed "project_Stable";
   4.282 +
   4.283 +Goal
   4.284 +   "(F Join project (reachable (extend h F Join G)) h G : Increasing func)  = \
   4.285 +\   (extend h F Join G : Increasing (func o f))";
   4.286 +by (asm_simp_tac (simpset() addsimps [Increasing_def, project_Stable,
   4.287 +				      Collect_eq_extend_set RS sym]) 1);
   4.288 +qed "project_Increasing";
   4.289 +
   4.290 +
   4.291 +(** Progress includes safety in the definition of ensures **)
   4.292 +
   4.293 +(*** Progress for (project C h F) ***)
   4.294 +
   4.295 +(** transient **)
   4.296 +
   4.297 +(*Premise is that C includes the domains of all actions that could be the
   4.298 +  transient one.  Could have C=UNIV of course*)
   4.299 +Goalw [transient_def]
   4.300 +     "[| ALL act: Acts F. act ^^ extend_set h A <= - extend_set h A --> \
   4.301 +\                      Domain act <= C;    \
   4.302 +\        F : transient (extend_set h A) |] \
   4.303 +\     ==> project C h F : transient A";
   4.304 +by (auto_tac (claset() delrules [ballE],
   4.305 +              simpset() addsimps [Domain_project_act, Int_absorb2]));
   4.306 +by (REPEAT (ball_tac 1));
   4.307 +by (auto_tac (claset(),
   4.308 +              simpset() addsimps [extend_set_def, project_set_def, 
   4.309 +				  project_act_def]));
   4.310 +by (ALLGOALS Blast_tac);
   4.311 +qed "transient_extend_set_imp_project_transient";
   4.312 +
   4.313 +
   4.314 +(*UNUSED.  WHY??
   4.315 +  Converse of the above...it requires a strong assumption about actions
   4.316 +  being enabled for all possible values of the new variables.*)
   4.317 +Goalw [transient_def]
   4.318 +     "[| project C h F : transient A;  \
   4.319 +\        ALL act: Acts F. project_act C h act ^^ A <= - A --> \
   4.320 +\                         Domain act <= C \
   4.321 +\             & extend_set h (project_set h (Domain act)) <= Domain act |]  \
   4.322 +\     ==> F : transient (extend_set h A)";
   4.323 +by (auto_tac (claset() delrules [ballE],
   4.324 +	      simpset() addsimps [Domain_project_act]));
   4.325 +by (ball_tac 1);
   4.326 +by (rtac bexI 1);
   4.327 +by (assume_tac 2);
   4.328 +by Auto_tac;
   4.329 +by (eres_inst_tac [("P", "A <= ?B")] rev_mp 1);
   4.330 +by (force_tac (claset(), simpset() addsimps [Int_absorb2]) 1);
   4.331 +(*The Domain requirement's proved; must prove the Image requirement*)
   4.332 +by (res_inst_tac [("y1", "x")] (surj_h RS surjD RS exE) 1);
   4.333 +by (res_inst_tac [("y1", "xa")] (surj_h RS surjD RS exE) 1);
   4.334 +by Auto_tac;
   4.335 +by (thin_tac "A <= ?B" 1);
   4.336 +by (force_tac (claset() addSIs [ImageI, project_act_I], simpset()) 1);
   4.337 +qed "project_transient_imp_transient_extend_set";
   4.338 +
   4.339 +
   4.340 +(** ensures **)
   4.341 +
   4.342 +(*For simplicity, the complicated condition on C is eliminated
   4.343 +  NOT SURE THIS IS GOOD FOR ANYTHING: CAN'T PROVE LEADSTO THEOREM*)
   4.344 +Goal "F : (extend_set h A) ensures (extend_set h B) \
   4.345 +\     ==> project UNIV h F : A ensures B";
   4.346 +by (asm_full_simp_tac
   4.347 +    (simpset() addsimps [ensures_def, project_constrains, 
   4.348 +			 transient_extend_set_imp_project_transient,
   4.349 +			 extend_set_Un_distrib RS sym, 
   4.350 +			 extend_set_Diff_distrib RS sym]) 1);
   4.351 +by (Blast_tac 1);
   4.352 +qed "ensures_extend_set_imp_project_ensures";
   4.353 +
   4.354 +(*A super-strong condition: G is not allowed to affect the
   4.355 +  shared variables at all.*)
   4.356 +Goal "[| ALL x. project UNIV h G ~: transient {x};  \
   4.357 +\        F Join project UNIV h G : A ensures B |] \
   4.358 +\     ==> extend h F Join G : (extend_set h A) ensures (extend_set h B)";
   4.359 +by (case_tac "A <= B" 1);
   4.360 +by (etac (extend_set_mono RS subset_imp_ensures) 1);
   4.361 +by (asm_full_simp_tac
   4.362 +    (simpset() addsimps [ensures_def, extend_constrains, extend_transient, 
   4.363 +			 extend_set_Un_distrib RS sym, 
   4.364 +			 extend_set_Diff_distrib RS sym,
   4.365 +			 Join_transient, Join_constrains,
   4.366 +			 project_constrains, Int_absorb1]) 1);
   4.367 +by (blast_tac (claset() addIs [transient_strengthen]) 1);
   4.368 +qed_spec_mp "Join_project_ensures";
   4.369 +
   4.370 +Goal "[| ALL x. project UNIV h G ~: transient {x};  \
   4.371 +\        F Join project UNIV h G : A leadsTo B |] \
   4.372 +\     ==> extend h F Join G : (extend_set h A) leadsTo (extend_set h B)";
   4.373 +by (etac leadsTo_induct 1);
   4.374 +by (asm_simp_tac (simpset() addsimps [leadsTo_UN, extend_set_Union]) 3);
   4.375 +by (blast_tac (claset() addIs [leadsTo_Trans]) 2);
   4.376 +by (blast_tac (claset() addIs [leadsTo_Basis, Join_project_ensures]) 1);
   4.377 +qed "Join_project_leadsTo_I";
   4.378 +
   4.379 +
   4.380 +(** Strong precondition and postcondition; doesn't seem very useful. **)
   4.381 +
   4.382 +Goal "F : X guarantees Y ==> \
   4.383 +\     extend h F : (extend h `` X) guarantees (extend h `` Y)";
   4.384 +by (rtac guaranteesI 1);
   4.385 +by Auto_tac;
   4.386 +by (blast_tac (claset() addDs [project_set_UNIV RS extend_Join_eq_extend_D, 
   4.387 +			       guaranteesD]) 1);
   4.388 +qed "guarantees_imp_extend_guarantees";
   4.389 +
   4.390 +Goal "extend h F : (extend h `` X) guarantees (extend h `` Y) \
   4.391 +\    ==> F : X guarantees Y";
   4.392 +by (rtac guaranteesI 1);
   4.393 +by (auto_tac (claset(), simpset() addsimps [guar_def, component_def]));
   4.394 +by (dtac spec 1);
   4.395 +by (dtac (mp RS mp) 1);
   4.396 +by (Blast_tac 2);
   4.397 +by (blast_tac (claset() addSDs [inj_extend RS inj_image_mem_iff RS iffD1]) 2);
   4.398 +by Auto_tac;
   4.399 +qed "extend_guarantees_imp_guarantees";
   4.400 +
   4.401 +Goal "(extend h F : (extend h `` X) guarantees (extend h `` Y)) = \
   4.402 +\    (F : X guarantees Y)";
   4.403 +by (blast_tac (claset() addIs [guarantees_imp_extend_guarantees,
   4.404 +			       extend_guarantees_imp_guarantees]) 1);
   4.405 +qed "extend_guarantees_eq";
   4.406 +
   4.407 +
   4.408 +(*Weak precondition and postcondition; this is the good one!
   4.409 +  Not clear that it has a converse [or that we want one!]*)
   4.410 +val [xguary,project,extend] =
   4.411 +Goal "[| F : X guarantees Y;  \
   4.412 +\        !!G. extend h F Join G : X' ==> F Join proj G h G : X;  \
   4.413 +\        !!G. [| F Join proj G h G : Y; extend h F Join G : X'; \
   4.414 +\                Disjoint (extend h F) G |] \
   4.415 +\             ==> extend h F Join G : Y' |] \
   4.416 +\     ==> extend h F : X' guarantees Y'";
   4.417 +by (rtac (xguary RS guaranteesD RS extend RS guaranteesI) 1);
   4.418 +by (etac project 1);
   4.419 +by (assume_tac 1);
   4.420 +by (assume_tac 1);
   4.421 +qed "project_guarantees";
   4.422 +
   4.423 +(** It seems that neither "guarantees" law can be proved from the other. **)
   4.424 +
   4.425 +
   4.426 +(*** guarantees corollaries ***)
   4.427 +
   4.428 +Goal "F : UNIV guarantees increasing func \
   4.429 +\     ==> extend h F : UNIV guarantees increasing (func o f)";
   4.430 +by (etac project_guarantees 1);
   4.431 +by (ALLGOALS
   4.432 +    (asm_simp_tac (simpset() addsimps [Join_project_increasing RS sym])));
   4.433 +qed "extend_guar_increasing";
   4.434 +
   4.435 +Goal "F : UNIV guarantees Increasing func \
   4.436 +\     ==> extend h F : UNIV guarantees Increasing (func o f)";
   4.437 +by (etac project_guarantees 1);
   4.438 +by (rtac (subset_UNIV RS project_Increasing_D) 2);
   4.439 +by Auto_tac;
   4.440 +qed "extend_guar_Increasing";
   4.441 +
   4.442 +Goal "F : (func localTo G) guarantees increasing func  \
   4.443 +\     ==> extend h F : (func o f) localTo (extend h G)  \
   4.444 +\                      guarantees increasing (func o f)";
   4.445 +by (etac project_guarantees 1);
   4.446 +(*the "increasing" guarantee*)
   4.447 +by (asm_simp_tac
   4.448 +    (simpset() addsimps [Join_project_increasing RS sym]) 2);
   4.449 +(*the "localTo" requirement*)
   4.450 +by (stac (project_set_UNIV RS project_extend_Join RS sym) 1);
   4.451 +by (asm_simp_tac 
   4.452 +    (simpset() addsimps [project_set_UNIV RS project_localTo_I]) 1);
   4.453 +qed "extend_localTo_guar_increasing";
   4.454 +
   4.455 +Goal "F : (func localTo G) guarantees Increasing func  \
   4.456 +\     ==> extend h F : (func o f) localTo (extend h G)  \
   4.457 +\                      guarantees Increasing (func o f)";
   4.458 +by (etac project_guarantees 1);
   4.459 +(*the "Increasing" guarantee*)
   4.460 +by (etac (subset_UNIV RS project_Increasing_D) 2);
   4.461 +(*the "localTo" requirement*)
   4.462 +by (stac (project_set_UNIV RS project_extend_Join RS sym) 1);
   4.463 +by (asm_simp_tac 
   4.464 +    (simpset() addsimps [project_set_UNIV RS project_localTo_I]) 1);
   4.465 +qed "extend_localTo_guar_Increasing";
   4.466 +
   4.467 +
   4.468 +(** Guarantees with a leadsTo postcondition **)
   4.469 +
   4.470 +Goal "[| G : f localTo extend h F; \
   4.471 +\        Disjoint (extend h F) G |] ==> project UNIV h G : stable {x}";
   4.472 +by (asm_full_simp_tac
   4.473 +    (simpset() addsimps [localTo_imp_stable,
   4.474 +			 extend_set_sing, project_stable]) 1);
   4.475 +qed "localTo_imp_project_stable";
   4.476 +
   4.477 +
   4.478 +Goal "F : stable{s} ==> F ~: transient {s}";
   4.479 +by (auto_tac (claset(), 
   4.480 +	      simpset() addsimps [FP_def, transient_def,
   4.481 +				  stable_def, constrains_def]));
   4.482 +qed "stable_sing_imp_not_transient";
   4.483 +
   4.484 +Goal "F : (A co A') guarantees (B leadsTo B')  \
   4.485 +\ ==> extend h F : ((extend_set h A) co (extend_set h A'))  \
   4.486 +\                   Int (f localTo (extend h F)) \
   4.487 +\                  guarantees ((extend_set h B) leadsTo (extend_set h B'))";
   4.488 +by (etac project_guarantees 1);
   4.489 +(*the safety precondition*)
   4.490 +by (stac (project_set_UNIV RS project_extend_Join RS sym) 1);
   4.491 +by (asm_full_simp_tac
   4.492 +    (simpset() addsimps [project_constrains, Join_constrains, 
   4.493 +			 extend_constrains]) 1);
   4.494 +by (fast_tac (claset() addDs [constrains_imp_subset]) 1);
   4.495 +(*the liveness postcondition*)
   4.496 +by (rtac Join_project_leadsTo_I 1);
   4.497 +by Auto_tac;
   4.498 +by (asm_full_simp_tac
   4.499 +    (simpset() addsimps [Join_localTo, self_localTo,
   4.500 +			 localTo_imp_project_stable, 
   4.501 +			 stable_sing_imp_not_transient]) 1);
   4.502 +qed "extend_co_guar_leadsTo";
   4.503 +
   4.504 +Close_locale "Extend";
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/HOL/UNITY/Project.thy	Wed Sep 29 13:13:06 1999 +0200
     5.3 @@ -0,0 +1,22 @@
     5.4 +(*  Title:      HOL/UNITY/Project.ML
     5.5 +    ID:         $Id$
     5.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     5.7 +    Copyright   1999  University of Cambridge
     5.8 +
     5.9 +Projections of state sets (also of actions and programs)
    5.10 +
    5.11 +Inheritance of GUARANTEES properties under extension
    5.12 +*)
    5.13 +
    5.14 +Project = Extend +
    5.15 +
    5.16 +
    5.17 +constdefs
    5.18 +
    5.19 +  restr_act :: "['c set, 'a*'b => 'c, ('a*'a) set] => ('a*'a) set"
    5.20 +    "restr_act C h act == project_act C h (extend_act h act)"
    5.21 +
    5.22 +  restr :: "['c set, 'a*'b => 'c, 'a program] => 'a program"
    5.23 +    "restr C h F == project C h (extend h F)"
    5.24 +
    5.25 +end
     6.1 --- a/src/HOL/UNITY/UNITY.ML	Tue Sep 28 22:17:05 1999 +0200
     6.2 +++ b/src/HOL/UNITY/UNITY.ML	Wed Sep 29 13:13:06 1999 +0200
     6.3 @@ -197,6 +197,17 @@
     6.4  qed "constrains_cancel";
     6.5  
     6.6  
     6.7 +(*** unless ***)
     6.8 +
     6.9 +Goalw [unless_def] "F : (A-B) co (A Un B) ==> F : A unless B";
    6.10 +by (assume_tac 1);
    6.11 +qed "unlessI";
    6.12 +
    6.13 +Goalw [unless_def] "F : A unless B ==> F : (A-B) co (A Un B)";
    6.14 +by (assume_tac 1);
    6.15 +qed "unlessD";
    6.16 +
    6.17 +
    6.18  (*** stable ***)
    6.19  
    6.20  Goalw [stable_def] "F : A co A ==> F : stable A";
     7.1 --- a/src/HOL/UNITY/Union.ML	Tue Sep 28 22:17:05 1999 +0200
     7.2 +++ b/src/HOL/UNITY/Union.ML	Wed Sep 29 13:13:06 1999 +0200
     7.3 @@ -250,9 +250,8 @@
     7.4  
     7.5  Goalw [ensures_def]
     7.6       "F Join G : A ensures B =     \
     7.7 -\     (F : (A-B) co (A Un B) & \
     7.8 -\      G : (A-B) co (A Un B) & \
     7.9 -\      (F : A ensures B | G : A ensures B))";
    7.10 +\     (F : (A-B) co (A Un B) & G : (A-B) co (A Un B) & \
    7.11 +\      (F : transient (A-B) | G : transient (A-B)))";
    7.12  by (auto_tac (claset(),
    7.13  	      simpset() addsimps [Join_constrains, Join_transient]));
    7.14  qed "Join_ensures";