src/HOL/UNITY/Project.thy
changeset 13790 8d7e9fce8c50
parent 10064 1a77667b21ef
child 13798 4c1a53627500
     1.1 --- a/src/HOL/UNITY/Project.thy	Tue Jan 28 22:53:39 2003 +0100
     1.2 +++ b/src/HOL/UNITY/Project.thy	Wed Jan 29 11:02:08 2003 +0100
     1.3 @@ -8,7 +8,7 @@
     1.4  Inheritance of GUARANTEES properties under extension
     1.5  *)
     1.6  
     1.7 -Project = Extend +
     1.8 +theory Project = Extend:
     1.9  
    1.10  constdefs
    1.11    projecting :: "['c program => 'c set, 'a*'b => 'c, 
    1.12 @@ -25,4 +25,713 @@
    1.13    subset_closed :: "'a set set => bool"
    1.14      "subset_closed U == ALL A: U. Pow A <= U"  
    1.15  
    1.16 +
    1.17 +lemma (in Extend) project_extend_constrains_I:
    1.18 +     "F : A co B ==> project h C (extend h F) : A co B"
    1.19 +apply (auto simp add: extend_act_def project_act_def constrains_def)
    1.20 +done
    1.21 +
    1.22 +
    1.23 +(** Safety **)
    1.24 +
    1.25 +(*used below to prove Join_project_ensures*)
    1.26 +lemma (in Extend) project_unless [rule_format (no_asm)]:
    1.27 +     "[| G : stable C;  project h C G : A unless B |]  
    1.28 +      ==> G : (C Int extend_set h A) unless (extend_set h B)"
    1.29 +apply (simp add: unless_def project_constrains)
    1.30 +apply (blast dest: stable_constrains_Int intro: constrains_weaken)
    1.31 +done
    1.32 +
    1.33 +(*Generalizes project_constrains to the program F Join project h C G
    1.34 +  useful with guarantees reasoning*)
    1.35 +lemma (in Extend) Join_project_constrains:
    1.36 +     "(F Join project h C G : A co B)  =   
    1.37 +        (extend h F Join G : (C Int extend_set h A) co (extend_set h B) &   
    1.38 +         F : A co B)"
    1.39 +apply (simp (no_asm) add: project_constrains)
    1.40 +apply (blast intro: extend_constrains [THEN iffD2, THEN constrains_weaken] 
    1.41 +             dest: constrains_imp_subset)
    1.42 +done
    1.43 +
    1.44 +(*The condition is required to prove the left-to-right direction
    1.45 +  could weaken it to G : (C Int extend_set h A) co C*)
    1.46 +lemma (in Extend) Join_project_stable: 
    1.47 +     "extend h F Join G : stable C  
    1.48 +      ==> (F Join project h C G : stable A)  =   
    1.49 +          (extend h F Join G : stable (C Int extend_set h A) &   
    1.50 +           F : stable A)"
    1.51 +apply (unfold stable_def)
    1.52 +apply (simp only: Join_project_constrains)
    1.53 +apply (blast intro: constrains_weaken dest: constrains_Int)
    1.54 +done
    1.55 +
    1.56 +(*For using project_guarantees in particular cases*)
    1.57 +lemma (in Extend) project_constrains_I:
    1.58 +     "extend h F Join G : extend_set h A co extend_set h B  
    1.59 +      ==> F Join project h C G : A co B"
    1.60 +apply (simp add: project_constrains extend_constrains)
    1.61 +apply (blast intro: constrains_weaken dest: constrains_imp_subset)
    1.62 +done
    1.63 +
    1.64 +lemma (in Extend) project_increasing_I: 
    1.65 +     "extend h F Join G : increasing (func o f)  
    1.66 +      ==> F Join project h C G : increasing func"
    1.67 +apply (unfold increasing_def stable_def)
    1.68 +apply (simp del: Join_constrains
    1.69 +            add: project_constrains_I extend_set_eq_Collect)
    1.70 +done
    1.71 +
    1.72 +lemma (in Extend) Join_project_increasing:
    1.73 +     "(F Join project h UNIV G : increasing func)  =   
    1.74 +      (extend h F Join G : increasing (func o f))"
    1.75 +apply (rule iffI)
    1.76 +apply (erule_tac [2] project_increasing_I)
    1.77 +apply (simp del: Join_stable
    1.78 +            add: increasing_def Join_project_stable)
    1.79 +apply (auto simp add: extend_set_eq_Collect extend_stable [THEN iffD1])
    1.80 +done
    1.81 +
    1.82 +(*The UNIV argument is essential*)
    1.83 +lemma (in Extend) project_constrains_D:
    1.84 +     "F Join project h UNIV G : A co B  
    1.85 +      ==> extend h F Join G : extend_set h A co extend_set h B"
    1.86 +by (simp add: project_constrains extend_constrains)
    1.87 +
    1.88 +
    1.89 +(*** "projecting" and union/intersection (no converses) ***)
    1.90 +
    1.91 +lemma projecting_Int: 
    1.92 +     "[| projecting C h F XA' XA;  projecting C h F XB' XB |]  
    1.93 +      ==> projecting C h F (XA' Int XB') (XA Int XB)"
    1.94 +by (unfold projecting_def, blast)
    1.95 +
    1.96 +lemma projecting_Un: 
    1.97 +     "[| projecting C h F XA' XA;  projecting C h F XB' XB |]  
    1.98 +      ==> projecting C h F (XA' Un XB') (XA Un XB)"
    1.99 +by (unfold projecting_def, blast)
   1.100 +
   1.101 +lemma projecting_INT: 
   1.102 +     "[| !!i. i:I ==> projecting C h F (X' i) (X i) |]  
   1.103 +      ==> projecting C h F (INT i:I. X' i) (INT i:I. X i)"
   1.104 +by (unfold projecting_def, blast)
   1.105 +
   1.106 +lemma projecting_UN: 
   1.107 +     "[| !!i. i:I ==> projecting C h F (X' i) (X i) |]  
   1.108 +      ==> projecting C h F (UN i:I. X' i) (UN i:I. X i)"
   1.109 +by (unfold projecting_def, blast)
   1.110 +
   1.111 +lemma projecting_weaken: 
   1.112 +     "[| projecting C h F X' X;  U'<=X';  X<=U |] ==> projecting C h F U' U"
   1.113 +by (unfold projecting_def, auto)
   1.114 +
   1.115 +lemma projecting_weaken_L: 
   1.116 +     "[| projecting C h F X' X;  U'<=X' |] ==> projecting C h F U' X"
   1.117 +by (unfold projecting_def, auto)
   1.118 +
   1.119 +lemma extending_Int: 
   1.120 +     "[| extending C h F YA' YA;  extending C h F YB' YB |]  
   1.121 +      ==> extending C h F (YA' Int YB') (YA Int YB)"
   1.122 +by (unfold extending_def, blast)
   1.123 +
   1.124 +lemma extending_Un: 
   1.125 +     "[| extending C h F YA' YA;  extending C h F YB' YB |]  
   1.126 +      ==> extending C h F (YA' Un YB') (YA Un YB)"
   1.127 +by (unfold extending_def, blast)
   1.128 +
   1.129 +lemma extending_INT: 
   1.130 +     "[| !!i. i:I ==> extending C h F (Y' i) (Y i) |]  
   1.131 +      ==> extending C h F (INT i:I. Y' i) (INT i:I. Y i)"
   1.132 +by (unfold extending_def, blast)
   1.133 +
   1.134 +lemma extending_UN: 
   1.135 +     "[| !!i. i:I ==> extending C h F (Y' i) (Y i) |]  
   1.136 +      ==> extending C h F (UN i:I. Y' i) (UN i:I. Y i)"
   1.137 +by (unfold extending_def, blast)
   1.138 +
   1.139 +lemma extending_weaken: 
   1.140 +     "[| extending C h F Y' Y;  Y'<=V';  V<=Y |] ==> extending C h F V' V"
   1.141 +by (unfold extending_def, auto)
   1.142 +
   1.143 +lemma extending_weaken_L: 
   1.144 +     "[| extending C h F Y' Y;  Y'<=V' |] ==> extending C h F V' Y"
   1.145 +by (unfold extending_def, auto)
   1.146 +
   1.147 +lemma projecting_UNIV: "projecting C h F X' UNIV"
   1.148 +by (simp add: projecting_def)
   1.149 +
   1.150 +lemma (in Extend) projecting_constrains: 
   1.151 +     "projecting C h F (extend_set h A co extend_set h B) (A co B)"
   1.152 +apply (unfold projecting_def)
   1.153 +apply (blast intro: project_constrains_I)
   1.154 +done
   1.155 +
   1.156 +lemma (in Extend) projecting_stable: 
   1.157 +     "projecting C h F (stable (extend_set h A)) (stable A)"
   1.158 +apply (unfold stable_def)
   1.159 +apply (rule projecting_constrains)
   1.160 +done
   1.161 +
   1.162 +lemma (in Extend) projecting_increasing: 
   1.163 +     "projecting C h F (increasing (func o f)) (increasing func)"
   1.164 +apply (unfold projecting_def)
   1.165 +apply (blast intro: project_increasing_I)
   1.166 +done
   1.167 +
   1.168 +lemma (in Extend) extending_UNIV: "extending C h F UNIV Y"
   1.169 +apply (simp (no_asm) add: extending_def)
   1.170 +done
   1.171 +
   1.172 +lemma (in Extend) extending_constrains: 
   1.173 +     "extending (%G. UNIV) h F (extend_set h A co extend_set h B) (A co B)"
   1.174 +apply (unfold extending_def)
   1.175 +apply (blast intro: project_constrains_D)
   1.176 +done
   1.177 +
   1.178 +lemma (in Extend) extending_stable: 
   1.179 +     "extending (%G. UNIV) h F (stable (extend_set h A)) (stable A)"
   1.180 +apply (unfold stable_def)
   1.181 +apply (rule extending_constrains)
   1.182 +done
   1.183 +
   1.184 +lemma (in Extend) extending_increasing: 
   1.185 +     "extending (%G. UNIV) h F (increasing (func o f)) (increasing func)"
   1.186 +by (force simp only: extending_def Join_project_increasing)
   1.187 +
   1.188 +
   1.189 +(** Reachability and project **)
   1.190 +
   1.191 +(*In practice, C = reachable(...): the inclusion is equality*)
   1.192 +lemma (in Extend) reachable_imp_reachable_project:
   1.193 +     "[| reachable (extend h F Join G) <= C;   
   1.194 +         z : reachable (extend h F Join G) |]  
   1.195 +      ==> f z : reachable (F Join project h C G)"
   1.196 +apply (erule reachable.induct)
   1.197 +apply (force intro!: reachable.Init simp add: split_extended_all, auto)
   1.198 + apply (rule_tac act = x in reachable.Acts)
   1.199 + apply auto
   1.200 + apply (erule extend_act_D)
   1.201 +apply (rule_tac act1 = "Restrict C act"
   1.202 +       in project_act_I [THEN [3] reachable.Acts], auto) 
   1.203 +done
   1.204 +
   1.205 +lemma (in Extend) project_Constrains_D: 
   1.206 +     "F Join project h (reachable (extend h F Join G)) G : A Co B   
   1.207 +      ==> extend h F Join G : (extend_set h A) Co (extend_set h B)"
   1.208 +apply (unfold Constrains_def)
   1.209 +apply (simp del: Join_constrains
   1.210 +            add: Join_project_constrains, clarify)
   1.211 +apply (erule constrains_weaken)
   1.212 +apply (auto intro: reachable_imp_reachable_project)
   1.213 +done
   1.214 +
   1.215 +lemma (in Extend) project_Stable_D: 
   1.216 +     "F Join project h (reachable (extend h F Join G)) G : Stable A   
   1.217 +      ==> extend h F Join G : Stable (extend_set h A)"
   1.218 +apply (unfold Stable_def)
   1.219 +apply (simp (no_asm_simp) add: project_Constrains_D)
   1.220 +done
   1.221 +
   1.222 +lemma (in Extend) project_Always_D: 
   1.223 +     "F Join project h (reachable (extend h F Join G)) G : Always A   
   1.224 +      ==> extend h F Join G : Always (extend_set h A)"
   1.225 +apply (unfold Always_def)
   1.226 +apply (force intro: reachable.Init simp add: project_Stable_D split_extended_all)
   1.227 +done
   1.228 +
   1.229 +lemma (in Extend) project_Increasing_D: 
   1.230 +     "F Join project h (reachable (extend h F Join G)) G : Increasing func   
   1.231 +      ==> extend h F Join G : Increasing (func o f)"
   1.232 +apply (unfold Increasing_def, auto)
   1.233 +apply (subst extend_set_eq_Collect [symmetric])
   1.234 +apply (simp (no_asm_simp) add: project_Stable_D)
   1.235 +done
   1.236 +
   1.237 +
   1.238 +(** Converse results for weak safety: benefits of the argument C *)
   1.239 +
   1.240 +(*In practice, C = reachable(...): the inclusion is equality*)
   1.241 +lemma (in Extend) reachable_project_imp_reachable:
   1.242 +     "[| C <= reachable(extend h F Join G);    
   1.243 +         x : reachable (F Join project h C G) |]  
   1.244 +      ==> EX y. h(x,y) : reachable (extend h F Join G)"
   1.245 +apply (erule reachable.induct)
   1.246 +apply  (force intro: reachable.Init)
   1.247 +apply (auto simp add: project_act_def)
   1.248 +apply (force del: Id_in_Acts intro: reachable.Acts extend_act_D)+
   1.249 +done
   1.250 +
   1.251 +lemma (in Extend) project_set_reachable_extend_eq:
   1.252 +     "project_set h (reachable (extend h F Join G)) =  
   1.253 +      reachable (F Join project h (reachable (extend h F Join G)) G)"
   1.254 +by (auto dest: subset_refl [THEN reachable_imp_reachable_project] 
   1.255 +               subset_refl [THEN reachable_project_imp_reachable])
   1.256 +
   1.257 +(*UNUSED*)
   1.258 +lemma (in Extend) reachable_extend_Join_subset:
   1.259 +     "reachable (extend h F Join G) <= C   
   1.260 +      ==> reachable (extend h F Join G) <=  
   1.261 +          extend_set h (reachable (F Join project h C G))"
   1.262 +apply (auto dest: reachable_imp_reachable_project)
   1.263 +done
   1.264 +
   1.265 +lemma (in Extend) project_Constrains_I: 
   1.266 +     "extend h F Join G : (extend_set h A) Co (extend_set h B)   
   1.267 +      ==> F Join project h (reachable (extend h F Join G)) G : A Co B"
   1.268 +apply (unfold Constrains_def)
   1.269 +apply (simp del: Join_constrains
   1.270 +            add: Join_project_constrains extend_set_Int_distrib)
   1.271 +apply (rule conjI)
   1.272 + prefer 2 
   1.273 + apply (force elim: constrains_weaken_L
   1.274 +              dest!: extend_constrains_project_set
   1.275 +                     subset_refl [THEN reachable_project_imp_reachable])
   1.276 +apply (blast intro: constrains_weaken_L)
   1.277 +done
   1.278 +
   1.279 +lemma (in Extend) project_Stable_I: 
   1.280 +     "extend h F Join G : Stable (extend_set h A)   
   1.281 +      ==> F Join project h (reachable (extend h F Join G)) G : Stable A"
   1.282 +apply (unfold Stable_def)
   1.283 +apply (simp (no_asm_simp) add: project_Constrains_I)
   1.284 +done
   1.285 +
   1.286 +lemma (in Extend) project_Always_I: 
   1.287 +     "extend h F Join G : Always (extend_set h A)   
   1.288 +      ==> F Join project h (reachable (extend h F Join G)) G : Always A"
   1.289 +apply (unfold Always_def)
   1.290 +apply (auto simp add: project_Stable_I)
   1.291 +apply (unfold extend_set_def, blast)
   1.292 +done
   1.293 +
   1.294 +lemma (in Extend) project_Increasing_I: 
   1.295 +    "extend h F Join G : Increasing (func o f)   
   1.296 +     ==> F Join project h (reachable (extend h F Join G)) G : Increasing func"
   1.297 +apply (unfold Increasing_def, auto)
   1.298 +apply (simp (no_asm_simp) add: extend_set_eq_Collect project_Stable_I)
   1.299 +done
   1.300 +
   1.301 +lemma (in Extend) project_Constrains:
   1.302 +     "(F Join project h (reachable (extend h F Join G)) G : A Co B)  =   
   1.303 +      (extend h F Join G : (extend_set h A) Co (extend_set h B))"
   1.304 +apply (blast intro: project_Constrains_I project_Constrains_D)
   1.305 +done
   1.306 +
   1.307 +lemma (in Extend) project_Stable: 
   1.308 +     "(F Join project h (reachable (extend h F Join G)) G : Stable A)  =   
   1.309 +      (extend h F Join G : Stable (extend_set h A))"
   1.310 +apply (unfold Stable_def)
   1.311 +apply (rule project_Constrains)
   1.312 +done
   1.313 +
   1.314 +lemma (in Extend) project_Increasing: 
   1.315 +   "(F Join project h (reachable (extend h F Join G)) G : Increasing func)  =  
   1.316 +    (extend h F Join G : Increasing (func o f))"
   1.317 +apply (simp (no_asm_simp) add: Increasing_def project_Stable extend_set_eq_Collect)
   1.318 +done
   1.319 +
   1.320 +(** A lot of redundant theorems: all are proved to facilitate reasoning
   1.321 +    about guarantees. **)
   1.322 +
   1.323 +lemma (in Extend) projecting_Constrains: 
   1.324 +     "projecting (%G. reachable (extend h F Join G)) h F  
   1.325 +                 (extend_set h A Co extend_set h B) (A Co B)"
   1.326 +
   1.327 +apply (unfold projecting_def)
   1.328 +apply (blast intro: project_Constrains_I)
   1.329 +done
   1.330 +
   1.331 +lemma (in Extend) projecting_Stable: 
   1.332 +     "projecting (%G. reachable (extend h F Join G)) h F  
   1.333 +                 (Stable (extend_set h A)) (Stable A)"
   1.334 +apply (unfold Stable_def)
   1.335 +apply (rule projecting_Constrains)
   1.336 +done
   1.337 +
   1.338 +lemma (in Extend) projecting_Always: 
   1.339 +     "projecting (%G. reachable (extend h F Join G)) h F  
   1.340 +                 (Always (extend_set h A)) (Always A)"
   1.341 +apply (unfold projecting_def)
   1.342 +apply (blast intro: project_Always_I)
   1.343 +done
   1.344 +
   1.345 +lemma (in Extend) projecting_Increasing: 
   1.346 +     "projecting (%G. reachable (extend h F Join G)) h F  
   1.347 +                 (Increasing (func o f)) (Increasing func)"
   1.348 +apply (unfold projecting_def)
   1.349 +apply (blast intro: project_Increasing_I)
   1.350 +done
   1.351 +
   1.352 +lemma (in Extend) extending_Constrains: 
   1.353 +     "extending (%G. reachable (extend h F Join G)) h F  
   1.354 +                  (extend_set h A Co extend_set h B) (A Co B)"
   1.355 +apply (unfold extending_def)
   1.356 +apply (blast intro: project_Constrains_D)
   1.357 +done
   1.358 +
   1.359 +lemma (in Extend) extending_Stable: 
   1.360 +     "extending (%G. reachable (extend h F Join G)) h F  
   1.361 +                  (Stable (extend_set h A)) (Stable A)"
   1.362 +apply (unfold extending_def)
   1.363 +apply (blast intro: project_Stable_D)
   1.364 +done
   1.365 +
   1.366 +lemma (in Extend) extending_Always: 
   1.367 +     "extending (%G. reachable (extend h F Join G)) h F  
   1.368 +                  (Always (extend_set h A)) (Always A)"
   1.369 +apply (unfold extending_def)
   1.370 +apply (blast intro: project_Always_D)
   1.371 +done
   1.372 +
   1.373 +lemma (in Extend) extending_Increasing: 
   1.374 +     "extending (%G. reachable (extend h F Join G)) h F  
   1.375 +                  (Increasing (func o f)) (Increasing func)"
   1.376 +apply (unfold extending_def)
   1.377 +apply (blast intro: project_Increasing_D)
   1.378 +done
   1.379 +
   1.380 +
   1.381 +(*** leadsETo in the precondition (??) ***)
   1.382 +
   1.383 +(** transient **)
   1.384 +
   1.385 +lemma (in Extend) transient_extend_set_imp_project_transient: 
   1.386 +     "[| G : transient (C Int extend_set h A);  G : stable C |]   
   1.387 +      ==> project h C G : transient (project_set h C Int A)"
   1.388 +
   1.389 +apply (unfold transient_def)
   1.390 +apply (auto simp add: Domain_project_act)
   1.391 +apply (subgoal_tac "act `` (C Int extend_set h A) <= - extend_set h A")
   1.392 +prefer 2
   1.393 + apply (simp add: stable_def constrains_def, blast) 
   1.394 +(*back to main goal*)
   1.395 +apply (erule_tac V = "?AA <= -C Un ?BB" in thin_rl)
   1.396 +apply (drule bspec, assumption) 
   1.397 +apply (simp add: extend_set_def project_act_def, blast)
   1.398 +done
   1.399 +
   1.400 +(*converse might hold too?*)
   1.401 +lemma (in Extend) project_extend_transient_D: 
   1.402 +     "project h C (extend h F) : transient (project_set h C Int D)  
   1.403 +      ==> F : transient (project_set h C Int D)"
   1.404 +apply (unfold transient_def)
   1.405 +apply (auto simp add: Domain_project_act)
   1.406 +apply (rule bexI)
   1.407 +prefer 2 apply assumption
   1.408 +apply auto
   1.409 +apply (unfold extend_act_def, blast)
   1.410 +done
   1.411 +
   1.412 +
   1.413 +(** ensures -- a primitive combining progress with safety **)
   1.414 +
   1.415 +(*Used to prove project_leadsETo_I*)
   1.416 +lemma (in Extend) ensures_extend_set_imp_project_ensures:
   1.417 +     "[| extend h F : stable C;  G : stable C;   
   1.418 +         extend h F Join G : A ensures B;  A-B = C Int extend_set h D |]   
   1.419 +      ==> F Join project h C G   
   1.420 +            : (project_set h C Int project_set h A) ensures (project_set h B)"
   1.421 +apply (simp add: ensures_def project_constrains Join_transient extend_transient, clarify)
   1.422 +apply (intro conjI) 
   1.423 +(*first subgoal*)
   1.424 +apply (blast intro: extend_stable_project_set 
   1.425 +                  [THEN stableD, THEN constrains_Int, THEN constrains_weaken] 
   1.426 +             dest!: extend_constrains_project_set equalityD1)
   1.427 +(*2nd subgoal*)
   1.428 +apply (erule stableD [THEN constrains_Int, THEN constrains_weaken])
   1.429 +    apply assumption
   1.430 +   apply (simp (no_asm_use) add: extend_set_def)
   1.431 +   apply blast
   1.432 + apply (simp add: extend_set_Int_distrib extend_set_Un_distrib)
   1.433 + apply (blast intro!: extend_set_project_set [THEN subsetD], blast)
   1.434 +(*The transient part*)
   1.435 +apply auto
   1.436 + prefer 2
   1.437 + apply (force dest!: equalityD1
   1.438 +              intro: transient_extend_set_imp_project_transient
   1.439 +                         [THEN transient_strengthen])
   1.440 +apply (simp (no_asm_use) add: Int_Diff)
   1.441 +apply (force dest!: equalityD1 
   1.442 +             intro: transient_extend_set_imp_project_transient 
   1.443 +               [THEN project_extend_transient_D, THEN transient_strengthen])
   1.444 +done
   1.445 +
   1.446 +(*Used to prove project_leadsETo_D*)
   1.447 +lemma (in Extend) Join_project_ensures [rule_format (no_asm)]:
   1.448 +     "[| project h C G ~: transient (A-B) | A<=B;   
   1.449 +         extend h F Join G : stable C;   
   1.450 +         F Join project h C G : A ensures B |]  
   1.451 +      ==> extend h F Join G : (C Int extend_set h A) ensures (extend_set h B)"
   1.452 +apply (erule disjE)
   1.453 +prefer 2 apply (blast intro: subset_imp_ensures)
   1.454 +apply (auto dest: extend_transient [THEN iffD2]
   1.455 +            intro: transient_strengthen project_set_I
   1.456 +                   project_unless [THEN unlessD] unlessI 
   1.457 +                   project_extend_constrains_I 
   1.458 +            simp add: ensures_def Join_transient)
   1.459 +done
   1.460 +
   1.461 +(** Lemma useful for both STRONG and WEAK progress, but the transient
   1.462 +    condition's very strong **)
   1.463 +
   1.464 +(*The strange induction formula allows induction over the leadsTo
   1.465 +  assumption's non-atomic precondition*)
   1.466 +lemma (in Extend) PLD_lemma:
   1.467 +     "[| ALL D. project h C G : transient D --> D={};   
   1.468 +         extend h F Join G : stable C;   
   1.469 +         F Join project h C G : (project_set h C Int A) leadsTo B |]  
   1.470 +      ==> extend h F Join G :  
   1.471 +          C Int extend_set h (project_set h C Int A) leadsTo (extend_set h B)"
   1.472 +apply (erule leadsTo_induct)
   1.473 +  apply (blast intro: leadsTo_Basis Join_project_ensures)
   1.474 + apply (blast intro: psp_stable2 [THEN leadsTo_weaken_L] leadsTo_Trans)
   1.475 +apply (simp del: UN_simps add: Int_UN_distrib leadsTo_UN extend_set_Union)
   1.476 +done
   1.477 +
   1.478 +lemma (in Extend) project_leadsTo_D_lemma:
   1.479 +     "[| ALL D. project h C G : transient D --> D={};   
   1.480 +         extend h F Join G : stable C;   
   1.481 +         F Join project h C G : (project_set h C Int A) leadsTo B |]  
   1.482 +      ==> extend h F Join G : (C Int extend_set h A) leadsTo (extend_set h B)"
   1.483 +apply (rule PLD_lemma [THEN leadsTo_weaken])
   1.484 +apply (auto simp add: split_extended_all)
   1.485 +done
   1.486 +
   1.487 +lemma (in Extend) Join_project_LeadsTo:
   1.488 +     "[| C = (reachable (extend h F Join G));  
   1.489 +         ALL D. project h C G : transient D --> D={};   
   1.490 +         F Join project h C G : A LeadsTo B |]  
   1.491 +      ==> extend h F Join G : (extend_set h A) LeadsTo (extend_set h B)"
   1.492 +by (simp del: Join_stable    add: LeadsTo_def project_leadsTo_D_lemma
   1.493 +                                  project_set_reachable_extend_eq)
   1.494 +
   1.495 +
   1.496 +(*** Towards project_Ensures_D ***)
   1.497 +
   1.498 +
   1.499 +lemma (in Extend) act_subset_imp_project_act_subset: 
   1.500 +     "act `` (C Int extend_set h A) <= B  
   1.501 +      ==> project_act h (Restrict C act) `` (project_set h C Int A)  
   1.502 +          <= project_set h B"
   1.503 +apply (unfold project_set_def extend_set_def project_act_def, blast)
   1.504 +done
   1.505 +
   1.506 +(*This trivial proof is the complementation part of transferring a transient
   1.507 +  property upwards.  The hard part would be to 
   1.508 +  show that G's action has a big enough domain.*)
   1.509 +lemma (in Extend) 
   1.510 +     "[| act: Acts G;        
   1.511 +         (project_act h (Restrict C act))``  
   1.512 +              (project_set h C Int A - B) <= -(project_set h C Int A - B) |]  
   1.513 +      ==> act``(C Int extend_set h A - extend_set h B)  
   1.514 +            <= -(C Int extend_set h A - extend_set h B)"
   1.515 +by (auto simp add: project_set_def extend_set_def project_act_def)
   1.516 +
   1.517 +lemma (in Extend) stable_project_transient:
   1.518 +     "[| G : stable ((C Int extend_set h A) - (extend_set h B));   
   1.519 +         project h C G : transient (project_set h C Int A - B) |]   
   1.520 +      ==> (C Int extend_set h A) - extend_set h B = {}"
   1.521 +apply (auto simp add: transient_def subset_Compl_self_eq Domain_project_act split_extended_all, blast)
   1.522 +apply (auto simp add: stable_def constrains_def)
   1.523 +apply (drule bspec, assumption) 
   1.524 +apply (auto simp add: Int_Diff extend_set_Diff_distrib [symmetric])
   1.525 +apply (drule act_subset_imp_project_act_subset)
   1.526 +apply (subgoal_tac "project_act h (Restrict C act) `` (project_set h C Int (A - B)) = {}")
   1.527 +apply (erule_tac V = "?r``?A <= ?B" in thin_rl)+
   1.528 +apply (unfold project_set_def extend_set_def project_act_def)
   1.529 +prefer 2 apply blast
   1.530 +apply (rule ccontr)
   1.531 +apply (drule subsetD, blast)
   1.532 +apply (force simp add: split_extended_all)
   1.533 +done
   1.534 +
   1.535 +lemma (in Extend) project_unless2 [rule_format (no_asm)]:
   1.536 +     "[| G : stable C;  project h C G : (project_set h C Int A) unless B |]  
   1.537 +      ==> G : (C Int extend_set h A) unless (extend_set h B)"
   1.538 +by (auto dest: stable_constrains_Int intro: constrains_weaken
   1.539 +         simp add: unless_def project_constrains Diff_eq Int_assoc 
   1.540 +                   Int_extend_set_lemma)
   1.541 +
   1.542 +lemma (in Extend) project_ensures_D_lemma:
   1.543 +     "[| G : stable ((C Int extend_set h A) - (extend_set h B));   
   1.544 +         F Join project h C G : (project_set h C Int A) ensures B;   
   1.545 +         extend h F Join G : stable C |]  
   1.546 +      ==> extend h F Join G : (C Int extend_set h A) ensures (extend_set h B)"
   1.547 +(*unless*)
   1.548 +apply (auto intro!: project_unless2 [unfolded unless_def] 
   1.549 +            intro: project_extend_constrains_I 
   1.550 +            simp add: ensures_def)
   1.551 +(*transient*)
   1.552 +(*A G-action cannot occur*)
   1.553 + prefer 2
   1.554 + apply (force dest: stable_project_transient 
   1.555 +              simp del: Diff_eq_empty_iff
   1.556 +              simp add: Diff_eq_empty_iff [symmetric])
   1.557 +(*An F-action*)
   1.558 +apply (force elim!: extend_transient [THEN iffD2, THEN transient_strengthen]
   1.559 +             simp add: split_extended_all)
   1.560 +done
   1.561 +
   1.562 +lemma (in Extend) project_ensures_D:
   1.563 +     "[| F Join project h UNIV G : A ensures B;   
   1.564 +         G : stable (extend_set h A - extend_set h B) |]  
   1.565 +      ==> extend h F Join G : (extend_set h A) ensures (extend_set h B)"
   1.566 +apply (rule project_ensures_D_lemma [of _ UNIV, THEN revcut_rl], auto)
   1.567 +done
   1.568 +
   1.569 +lemma (in Extend) project_Ensures_D: 
   1.570 +     "[| F Join project h (reachable (extend h F Join G)) G : A Ensures B;   
   1.571 +         G : stable (reachable (extend h F Join G) Int extend_set h A -  
   1.572 +                     extend_set h B) |]  
   1.573 +      ==> extend h F Join G : (extend_set h A) Ensures (extend_set h B)"
   1.574 +apply (unfold Ensures_def)
   1.575 +apply (rule project_ensures_D_lemma [THEN revcut_rl])
   1.576 +apply (auto simp add: project_set_reachable_extend_eq [symmetric])
   1.577 +done
   1.578 +
   1.579 +
   1.580 +(*** Guarantees ***)
   1.581 +
   1.582 +lemma (in Extend) project_act_Restrict_subset_project_act:
   1.583 +     "project_act h (Restrict C act) <= project_act h act"
   1.584 +apply (auto simp add: project_act_def)
   1.585 +done
   1.586 +					   
   1.587 +							   
   1.588 +lemma (in Extend) subset_closed_ok_extend_imp_ok_project:
   1.589 +     "[| extend h F ok G; subset_closed (AllowedActs F) |]  
   1.590 +      ==> F ok project h C G"
   1.591 +apply (auto simp add: ok_def)
   1.592 +apply (rename_tac act) 
   1.593 +apply (drule subsetD, blast)
   1.594 +apply (rule_tac x = "Restrict C  (extend_act h act)" in rev_image_eqI)
   1.595 +apply simp +
   1.596 +apply (cut_tac project_act_Restrict_subset_project_act)
   1.597 +apply (auto simp add: subset_closed_def)
   1.598 +done
   1.599 +
   1.600 +
   1.601 +(*Weak precondition and postcondition
   1.602 +  Not clear that it has a converse [or that we want one!]*)
   1.603 +
   1.604 +(*The raw version; 3rd premise could be weakened by adding the
   1.605 +  precondition extend h F Join G : X' *)
   1.606 +lemma (in Extend) project_guarantees_raw:
   1.607 + assumes xguary:  "F : X guarantees Y"
   1.608 +     and closed:  "subset_closed (AllowedActs F)"
   1.609 +     and project: "!!G. extend h F Join G : X' 
   1.610 +                        ==> F Join project h (C G) G : X"
   1.611 +     and extend:  "!!G. [| F Join project h (C G) G : Y |]  
   1.612 +                        ==> extend h F Join G : Y'"
   1.613 + shows "extend h F : X' guarantees Y'"
   1.614 +apply (rule xguary [THEN guaranteesD, THEN extend, THEN guaranteesI])
   1.615 +apply (blast intro: closed subset_closed_ok_extend_imp_ok_project)
   1.616 +apply (erule project)
   1.617 +done
   1.618 +
   1.619 +lemma (in Extend) project_guarantees:
   1.620 +     "[| F : X guarantees Y;  subset_closed (AllowedActs F);  
   1.621 +         projecting C h F X' X;  extending C h F Y' Y |]  
   1.622 +      ==> extend h F : X' guarantees Y'"
   1.623 +apply (rule guaranteesI)
   1.624 +apply (auto simp add: guaranteesD projecting_def extending_def
   1.625 +                      subset_closed_ok_extend_imp_ok_project)
   1.626 +done
   1.627 +
   1.628 +
   1.629 +(*It seems that neither "guarantees" law can be proved from the other.*)
   1.630 +
   1.631 +
   1.632 +(*** guarantees corollaries ***)
   1.633 +
   1.634 +(** Some could be deleted: the required versions are easy to prove **)
   1.635 +
   1.636 +lemma (in Extend) extend_guar_increasing:
   1.637 +     "[| F : UNIV guarantees increasing func;   
   1.638 +         subset_closed (AllowedActs F) |]  
   1.639 +      ==> extend h F : X' guarantees increasing (func o f)"
   1.640 +apply (erule project_guarantees)
   1.641 +apply (rule_tac [3] extending_increasing)
   1.642 +apply (rule_tac [2] projecting_UNIV, auto)
   1.643 +done
   1.644 +
   1.645 +lemma (in Extend) extend_guar_Increasing:
   1.646 +     "[| F : UNIV guarantees Increasing func;   
   1.647 +         subset_closed (AllowedActs F) |]  
   1.648 +      ==> extend h F : X' guarantees Increasing (func o f)"
   1.649 +apply (erule project_guarantees)
   1.650 +apply (rule_tac [3] extending_Increasing)
   1.651 +apply (rule_tac [2] projecting_UNIV, auto)
   1.652 +done
   1.653 +
   1.654 +lemma (in Extend) extend_guar_Always:
   1.655 +     "[| F : Always A guarantees Always B;   
   1.656 +         subset_closed (AllowedActs F) |]  
   1.657 +      ==> extend h F                    
   1.658 +            : Always(extend_set h A) guarantees Always(extend_set h B)"
   1.659 +apply (erule project_guarantees)
   1.660 +apply (rule_tac [3] extending_Always)
   1.661 +apply (rule_tac [2] projecting_Always, auto)
   1.662 +done
   1.663 +
   1.664 +lemma (in Extend) preserves_project_transient_empty:
   1.665 +     "[| G : preserves f;  project h C G : transient D |] ==> D={}"
   1.666 +apply (rule stable_transient_empty)
   1.667 + prefer 2 apply assumption
   1.668 +apply (blast intro: project_preserves_id_I 
   1.669 +                    preserves_id_subset_stable [THEN subsetD])
   1.670 +done
   1.671 +
   1.672 +
   1.673 +(** Guarantees with a leadsTo postcondition 
   1.674 +    THESE ARE ALL TOO WEAK because G can't affect F's variables at all**)
   1.675 +
   1.676 +lemma (in Extend) project_leadsTo_D:
   1.677 +     "[| F Join project h UNIV G : A leadsTo B;     
   1.678 +         G : preserves f |]   
   1.679 +      ==> extend h F Join G : (extend_set h A) leadsTo (extend_set h B)"
   1.680 +apply (rule_tac C1 = UNIV in project_leadsTo_D_lemma [THEN leadsTo_weaken])
   1.681 +apply (auto dest: preserves_project_transient_empty)
   1.682 +done
   1.683 +
   1.684 +lemma (in Extend) project_LeadsTo_D:
   1.685 +     "[| F Join project h (reachable (extend h F Join G)) G : A LeadsTo B;
   1.686 +         G : preserves f |]   
   1.687 +       ==> extend h F Join G : (extend_set h A) LeadsTo (extend_set h B)"
   1.688 +apply (rule refl [THEN Join_project_LeadsTo])
   1.689 +apply (auto dest: preserves_project_transient_empty)
   1.690 +done
   1.691 +
   1.692 +lemma (in Extend) extending_leadsTo: 
   1.693 +     "(ALL G. extend h F ok G --> G : preserves f)  
   1.694 +      ==> extending (%G. UNIV) h F  
   1.695 +                  (extend_set h A leadsTo extend_set h B) (A leadsTo B)"
   1.696 +apply (unfold extending_def)
   1.697 +apply (blast intro: project_leadsTo_D)
   1.698 +done
   1.699 +
   1.700 +lemma (in Extend) extending_LeadsTo: 
   1.701 +     "(ALL G. extend h F ok G --> G : preserves f)  
   1.702 +      ==> extending (%G. reachable (extend h F Join G)) h F  
   1.703 +                  (extend_set h A LeadsTo extend_set h B) (A LeadsTo B)"
   1.704 +apply (unfold extending_def)
   1.705 +apply (blast intro: project_LeadsTo_D)
   1.706 +done
   1.707 +
   1.708 +ML
   1.709 +{*
   1.710 +val projecting_Int = thm "projecting_Int";
   1.711 +val projecting_Un = thm "projecting_Un";
   1.712 +val projecting_INT = thm "projecting_INT";
   1.713 +val projecting_UN = thm "projecting_UN";
   1.714 +val projecting_weaken = thm "projecting_weaken";
   1.715 +val projecting_weaken_L = thm "projecting_weaken_L";
   1.716 +val extending_Int = thm "extending_Int";
   1.717 +val extending_Un = thm "extending_Un";
   1.718 +val extending_INT = thm "extending_INT";
   1.719 +val extending_UN = thm "extending_UN";
   1.720 +val extending_weaken = thm "extending_weaken";
   1.721 +val extending_weaken_L = thm "extending_weaken_L";
   1.722 +val projecting_UNIV = thm "projecting_UNIV";
   1.723 +*}
   1.724 +
   1.725  end