1(* Title: HOL/UNITY/Project.thy 2 Author: Lawrence C Paulson, Cambridge University Computer Laboratory 3 Copyright 1999 University of Cambridge 4 5Projections of state sets (also of actions and programs). 6 7Inheritance of GUARANTEES properties under extension. 8*) 9 10section\<open>Projections of State Sets\<close> 11 12theory Project imports Extend begin 13 14definition projecting :: "['c program => 'c set, 'a*'b => 'c, 15 'a program, 'c program set, 'a program set] => bool" where 16 "projecting C h F X' X == 17 \<forall>G. extend h F\<squnion>G \<in> X' --> F\<squnion>project h (C G) G \<in> X" 18 19definition extending :: "['c program => 'c set, 'a*'b => 'c, 'a program, 20 'c program set, 'a program set] => bool" where 21 "extending C h F Y' Y == 22 \<forall>G. extend h F ok G --> F\<squnion>project h (C G) G \<in> Y 23 --> extend h F\<squnion>G \<in> Y'" 24 25definition subset_closed :: "'a set set => bool" where 26 "subset_closed U == \<forall>A \<in> U. Pow A \<subseteq> U" 27 28 29context Extend 30begin 31 32lemma project_extend_constrains_I: 33 "F \<in> A co B ==> project h C (extend h F) \<in> A co B" 34apply (auto simp add: extend_act_def project_act_def constrains_def) 35done 36 37 38subsection\<open>Safety\<close> 39 40(*used below to prove Join_project_ensures*) 41lemma project_unless: 42 "[| G \<in> stable C; project h C G \<in> A unless B |] 43 ==> G \<in> (C \<inter> extend_set h A) unless (extend_set h B)" 44apply (simp add: unless_def project_constrains) 45apply (blast dest: stable_constrains_Int intro: constrains_weaken) 46done 47 48(*Generalizes project_constrains to the program F\<squnion>project h C G 49 useful with guarantees reasoning*) 50lemma Join_project_constrains: 51 "(F\<squnion>project h C G \<in> A co B) = 52 (extend h F\<squnion>G \<in> (C \<inter> extend_set h A) co (extend_set h B) & 53 F \<in> A co B)" 54apply (simp (no_asm) add: project_constrains) 55apply (blast intro: extend_constrains [THEN iffD2, THEN constrains_weaken] 56 dest: constrains_imp_subset) 57done 58 59(*The condition is required to prove the left-to-right direction 60 could weaken it to G \<in> (C \<inter> extend_set h A) co C*) 61lemma Join_project_stable: 62 "extend h F\<squnion>G \<in> stable C 63 ==> (F\<squnion>project h C G \<in> stable A) = 64 (extend h F\<squnion>G \<in> stable (C \<inter> extend_set h A) & 65 F \<in> stable A)" 66apply (unfold stable_def) 67apply (simp only: Join_project_constrains) 68apply (blast intro: constrains_weaken dest: constrains_Int) 69done 70 71(*For using project_guarantees in particular cases*) 72lemma project_constrains_I: 73 "extend h F\<squnion>G \<in> extend_set h A co extend_set h B 74 ==> F\<squnion>project h C G \<in> A co B" 75apply (simp add: project_constrains extend_constrains) 76apply (blast intro: constrains_weaken dest: constrains_imp_subset) 77done 78 79lemma project_increasing_I: 80 "extend h F\<squnion>G \<in> increasing (func o f) 81 ==> F\<squnion>project h C G \<in> increasing func" 82apply (unfold increasing_def stable_def) 83apply (simp del: Join_constrains 84 add: project_constrains_I extend_set_eq_Collect) 85done 86 87lemma Join_project_increasing: 88 "(F\<squnion>project h UNIV G \<in> increasing func) = 89 (extend h F\<squnion>G \<in> increasing (func o f))" 90apply (rule iffI) 91apply (erule_tac [2] project_increasing_I) 92apply (simp del: Join_stable 93 add: increasing_def Join_project_stable) 94apply (auto simp add: extend_set_eq_Collect extend_stable [THEN iffD1]) 95done 96 97(*The UNIV argument is essential*) 98lemma project_constrains_D: 99 "F\<squnion>project h UNIV G \<in> A co B 100 ==> extend h F\<squnion>G \<in> extend_set h A co extend_set h B" 101by (simp add: project_constrains extend_constrains) 102 103end 104 105 106subsection\<open>"projecting" and union/intersection (no converses)\<close> 107 108lemma projecting_Int: 109 "[| projecting C h F XA' XA; projecting C h F XB' XB |] 110 ==> projecting C h F (XA' \<inter> XB') (XA \<inter> XB)" 111by (unfold projecting_def, blast) 112 113lemma projecting_Un: 114 "[| projecting C h F XA' XA; projecting C h F XB' XB |] 115 ==> projecting C h F (XA' \<union> XB') (XA \<union> XB)" 116by (unfold projecting_def, blast) 117 118lemma projecting_INT: 119 "[| !!i. i \<in> I ==> projecting C h F (X' i) (X i) |] 120 ==> projecting C h F (\<Inter>i \<in> I. X' i) (\<Inter>i \<in> I. X i)" 121by (unfold projecting_def, blast) 122 123lemma projecting_UN: 124 "[| !!i. i \<in> I ==> projecting C h F (X' i) (X i) |] 125 ==> projecting C h F (\<Union>i \<in> I. X' i) (\<Union>i \<in> I. X i)" 126by (unfold projecting_def, blast) 127 128lemma projecting_weaken: 129 "[| projecting C h F X' X; U'<=X'; X \<subseteq> U |] ==> projecting C h F U' U" 130by (unfold projecting_def, auto) 131 132lemma projecting_weaken_L: 133 "[| projecting C h F X' X; U'<=X' |] ==> projecting C h F U' X" 134by (unfold projecting_def, auto) 135 136lemma extending_Int: 137 "[| extending C h F YA' YA; extending C h F YB' YB |] 138 ==> extending C h F (YA' \<inter> YB') (YA \<inter> YB)" 139by (unfold extending_def, blast) 140 141lemma extending_Un: 142 "[| extending C h F YA' YA; extending C h F YB' YB |] 143 ==> extending C h F (YA' \<union> YB') (YA \<union> YB)" 144by (unfold extending_def, blast) 145 146lemma extending_INT: 147 "[| !!i. i \<in> I ==> extending C h F (Y' i) (Y i) |] 148 ==> extending C h F (\<Inter>i \<in> I. Y' i) (\<Inter>i \<in> I. Y i)" 149by (unfold extending_def, blast) 150 151lemma extending_UN: 152 "[| !!i. i \<in> I ==> extending C h F (Y' i) (Y i) |] 153 ==> extending C h F (\<Union>i \<in> I. Y' i) (\<Union>i \<in> I. Y i)" 154by (unfold extending_def, blast) 155 156lemma extending_weaken: 157 "[| extending C h F Y' Y; Y'<=V'; V \<subseteq> Y |] ==> extending C h F V' V" 158by (unfold extending_def, auto) 159 160lemma extending_weaken_L: 161 "[| extending C h F Y' Y; Y'<=V' |] ==> extending C h F V' Y" 162by (unfold extending_def, auto) 163 164lemma projecting_UNIV: "projecting C h F X' UNIV" 165by (simp add: projecting_def) 166 167context Extend 168begin 169 170lemma projecting_constrains: 171 "projecting C h F (extend_set h A co extend_set h B) (A co B)" 172apply (unfold projecting_def) 173apply (blast intro: project_constrains_I) 174done 175 176lemma projecting_stable: 177 "projecting C h F (stable (extend_set h A)) (stable A)" 178apply (unfold stable_def) 179apply (rule projecting_constrains) 180done 181 182lemma projecting_increasing: 183 "projecting C h F (increasing (func o f)) (increasing func)" 184apply (unfold projecting_def) 185apply (blast intro: project_increasing_I) 186done 187 188lemma extending_UNIV: "extending C h F UNIV Y" 189apply (simp (no_asm) add: extending_def) 190done 191 192lemma extending_constrains: 193 "extending (%G. UNIV) h F (extend_set h A co extend_set h B) (A co B)" 194apply (unfold extending_def) 195apply (blast intro: project_constrains_D) 196done 197 198lemma extending_stable: 199 "extending (%G. UNIV) h F (stable (extend_set h A)) (stable A)" 200apply (unfold stable_def) 201apply (rule extending_constrains) 202done 203 204lemma extending_increasing: 205 "extending (%G. UNIV) h F (increasing (func o f)) (increasing func)" 206by (force simp only: extending_def Join_project_increasing) 207 208 209subsection\<open>Reachability and project\<close> 210 211(*In practice, C = reachable(...): the inclusion is equality*) 212lemma reachable_imp_reachable_project: 213 "[| reachable (extend h F\<squnion>G) \<subseteq> C; 214 z \<in> reachable (extend h F\<squnion>G) |] 215 ==> f z \<in> reachable (F\<squnion>project h C G)" 216apply (erule reachable.induct) 217apply (force intro!: reachable.Init simp add: split_extended_all, auto) 218 apply (rule_tac act = x in reachable.Acts) 219 apply auto 220 apply (erule extend_act_D) 221apply (rule_tac act1 = "Restrict C act" 222 in project_act_I [THEN [3] reachable.Acts], auto) 223done 224 225lemma project_Constrains_D: 226 "F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> A Co B 227 ==> extend h F\<squnion>G \<in> (extend_set h A) Co (extend_set h B)" 228apply (unfold Constrains_def) 229apply (simp del: Join_constrains 230 add: Join_project_constrains, clarify) 231apply (erule constrains_weaken) 232apply (auto intro: reachable_imp_reachable_project) 233done 234 235lemma project_Stable_D: 236 "F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> Stable A 237 ==> extend h F\<squnion>G \<in> Stable (extend_set h A)" 238apply (unfold Stable_def) 239apply (simp (no_asm_simp) add: project_Constrains_D) 240done 241 242lemma project_Always_D: 243 "F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> Always A 244 ==> extend h F\<squnion>G \<in> Always (extend_set h A)" 245apply (unfold Always_def) 246apply (force intro: reachable.Init simp add: project_Stable_D split_extended_all) 247done 248 249lemma project_Increasing_D: 250 "F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> Increasing func 251 ==> extend h F\<squnion>G \<in> Increasing (func o f)" 252apply (unfold Increasing_def, auto) 253apply (subst extend_set_eq_Collect [symmetric]) 254apply (simp (no_asm_simp) add: project_Stable_D) 255done 256 257 258subsection\<open>Converse results for weak safety: benefits of the argument C\<close> 259 260(*In practice, C = reachable(...): the inclusion is equality*) 261lemma reachable_project_imp_reachable: 262 "[| C \<subseteq> reachable(extend h F\<squnion>G); 263 x \<in> reachable (F\<squnion>project h C G) |] 264 ==> \<exists>y. h(x,y) \<in> reachable (extend h F\<squnion>G)" 265apply (erule reachable.induct) 266apply (force intro: reachable.Init) 267apply (auto simp add: project_act_def) 268apply (force del: Id_in_Acts intro: reachable.Acts extend_act_D)+ 269done 270 271lemma project_set_reachable_extend_eq: 272 "project_set h (reachable (extend h F\<squnion>G)) = 273 reachable (F\<squnion>project h (reachable (extend h F\<squnion>G)) G)" 274by (auto dest: subset_refl [THEN reachable_imp_reachable_project] 275 subset_refl [THEN reachable_project_imp_reachable]) 276 277(*UNUSED*) 278lemma reachable_extend_Join_subset: 279 "reachable (extend h F\<squnion>G) \<subseteq> C 280 ==> reachable (extend h F\<squnion>G) \<subseteq> 281 extend_set h (reachable (F\<squnion>project h C G))" 282apply (auto dest: reachable_imp_reachable_project) 283done 284 285lemma project_Constrains_I: 286 "extend h F\<squnion>G \<in> (extend_set h A) Co (extend_set h B) 287 ==> F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> A Co B" 288apply (unfold Constrains_def) 289apply (simp del: Join_constrains 290 add: Join_project_constrains extend_set_Int_distrib) 291apply (rule conjI) 292 prefer 2 293 apply (force elim: constrains_weaken_L 294 dest!: extend_constrains_project_set 295 subset_refl [THEN reachable_project_imp_reachable]) 296apply (blast intro: constrains_weaken_L) 297done 298 299lemma project_Stable_I: 300 "extend h F\<squnion>G \<in> Stable (extend_set h A) 301 ==> F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> Stable A" 302apply (unfold Stable_def) 303apply (simp (no_asm_simp) add: project_Constrains_I) 304done 305 306lemma project_Always_I: 307 "extend h F\<squnion>G \<in> Always (extend_set h A) 308 ==> F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> Always A" 309apply (unfold Always_def) 310apply (auto simp add: project_Stable_I) 311apply (unfold extend_set_def, blast) 312done 313 314lemma project_Increasing_I: 315 "extend h F\<squnion>G \<in> Increasing (func o f) 316 ==> F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> Increasing func" 317apply (unfold Increasing_def, auto) 318apply (simp (no_asm_simp) add: extend_set_eq_Collect project_Stable_I) 319done 320 321lemma project_Constrains: 322 "(F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> A Co B) = 323 (extend h F\<squnion>G \<in> (extend_set h A) Co (extend_set h B))" 324apply (blast intro: project_Constrains_I project_Constrains_D) 325done 326 327lemma project_Stable: 328 "(F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> Stable A) = 329 (extend h F\<squnion>G \<in> Stable (extend_set h A))" 330apply (unfold Stable_def) 331apply (rule project_Constrains) 332done 333 334lemma project_Increasing: 335 "(F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> Increasing func) = 336 (extend h F\<squnion>G \<in> Increasing (func o f))" 337apply (simp (no_asm_simp) add: Increasing_def project_Stable extend_set_eq_Collect) 338done 339 340subsection\<open>A lot of redundant theorems: all are proved to facilitate reasoning 341 about guarantees.\<close> 342 343lemma projecting_Constrains: 344 "projecting (%G. reachable (extend h F\<squnion>G)) h F 345 (extend_set h A Co extend_set h B) (A Co B)" 346 347apply (unfold projecting_def) 348apply (blast intro: project_Constrains_I) 349done 350 351lemma projecting_Stable: 352 "projecting (%G. reachable (extend h F\<squnion>G)) h F 353 (Stable (extend_set h A)) (Stable A)" 354apply (unfold Stable_def) 355apply (rule projecting_Constrains) 356done 357 358lemma projecting_Always: 359 "projecting (%G. reachable (extend h F\<squnion>G)) h F 360 (Always (extend_set h A)) (Always A)" 361apply (unfold projecting_def) 362apply (blast intro: project_Always_I) 363done 364 365lemma projecting_Increasing: 366 "projecting (%G. reachable (extend h F\<squnion>G)) h F 367 (Increasing (func o f)) (Increasing func)" 368apply (unfold projecting_def) 369apply (blast intro: project_Increasing_I) 370done 371 372lemma extending_Constrains: 373 "extending (%G. reachable (extend h F\<squnion>G)) h F 374 (extend_set h A Co extend_set h B) (A Co B)" 375apply (unfold extending_def) 376apply (blast intro: project_Constrains_D) 377done 378 379lemma extending_Stable: 380 "extending (%G. reachable (extend h F\<squnion>G)) h F 381 (Stable (extend_set h A)) (Stable A)" 382apply (unfold extending_def) 383apply (blast intro: project_Stable_D) 384done 385 386lemma extending_Always: 387 "extending (%G. reachable (extend h F\<squnion>G)) h F 388 (Always (extend_set h A)) (Always A)" 389apply (unfold extending_def) 390apply (blast intro: project_Always_D) 391done 392 393lemma extending_Increasing: 394 "extending (%G. reachable (extend h F\<squnion>G)) h F 395 (Increasing (func o f)) (Increasing func)" 396apply (unfold extending_def) 397apply (blast intro: project_Increasing_D) 398done 399 400 401subsection\<open>leadsETo in the precondition (??)\<close> 402 403subsubsection\<open>transient\<close> 404 405lemma transient_extend_set_imp_project_transient: 406 "[| G \<in> transient (C \<inter> extend_set h A); G \<in> stable C |] 407 ==> project h C G \<in> transient (project_set h C \<inter> A)" 408apply (auto simp add: transient_def Domain_project_act) 409apply (subgoal_tac "act `` (C \<inter> extend_set h A) \<subseteq> - extend_set h A") 410 prefer 2 411 apply (simp add: stable_def constrains_def, blast) 412(*back to main goal*) 413apply (erule_tac V = "AA \<subseteq> -C \<union> BB" for AA BB in thin_rl) 414apply (drule bspec, assumption) 415apply (simp add: extend_set_def project_act_def, blast) 416done 417 418(*converse might hold too?*) 419lemma project_extend_transient_D: 420 "project h C (extend h F) \<in> transient (project_set h C \<inter> D) 421 ==> F \<in> transient (project_set h C \<inter> D)" 422apply (simp add: transient_def Domain_project_act, safe) 423apply blast+ 424done 425 426 427subsubsection\<open>ensures -- a primitive combining progress with safety\<close> 428 429(*Used to prove project_leadsETo_I*) 430lemma ensures_extend_set_imp_project_ensures: 431 "[| extend h F \<in> stable C; G \<in> stable C; 432 extend h F\<squnion>G \<in> A ensures B; A-B = C \<inter> extend_set h D |] 433 ==> F\<squnion>project h C G 434 \<in> (project_set h C \<inter> project_set h A) ensures (project_set h B)" 435apply (simp add: ensures_def project_constrains extend_transient, 436 clarify) 437apply (intro conjI) 438(*first subgoal*) 439apply (blast intro: extend_stable_project_set 440 [THEN stableD, THEN constrains_Int, THEN constrains_weaken] 441 dest!: extend_constrains_project_set equalityD1) 442(*2nd subgoal*) 443apply (erule stableD [THEN constrains_Int, THEN constrains_weaken]) 444 apply assumption 445 apply (simp (no_asm_use) add: extend_set_def) 446 apply blast 447 apply (simp add: extend_set_Int_distrib extend_set_Un_distrib) 448 apply (blast intro!: extend_set_project_set [THEN subsetD], blast) 449(*The transient part*) 450apply auto 451 prefer 2 452 apply (force dest!: equalityD1 453 intro: transient_extend_set_imp_project_transient 454 [THEN transient_strengthen]) 455apply (simp (no_asm_use) add: Int_Diff) 456apply (force dest!: equalityD1 457 intro: transient_extend_set_imp_project_transient 458 [THEN project_extend_transient_D, THEN transient_strengthen]) 459done 460 461text\<open>Transferring a transient property upwards\<close> 462lemma project_transient_extend_set: 463 "project h C G \<in> transient (project_set h C \<inter> A - B) 464 ==> G \<in> transient (C \<inter> extend_set h A - extend_set h B)" 465apply (simp add: transient_def project_set_def extend_set_def project_act_def) 466apply (elim disjE bexE) 467 apply (rule_tac x=Id in bexI) 468 apply (blast intro!: rev_bexI )+ 469done 470 471lemma project_unless2: 472 "[| G \<in> stable C; project h C G \<in> (project_set h C \<inter> A) unless B |] 473 ==> G \<in> (C \<inter> extend_set h A) unless (extend_set h B)" 474by (auto dest: stable_constrains_Int intro: constrains_weaken 475 simp add: unless_def project_constrains Diff_eq Int_assoc 476 Int_extend_set_lemma) 477 478 479lemma extend_unless: 480 "[|extend h F \<in> stable C; F \<in> A unless B|] 481 ==> extend h F \<in> C \<inter> extend_set h A unless extend_set h B" 482apply (simp add: unless_def stable_def) 483apply (drule constrains_Int) 484apply (erule extend_constrains [THEN iffD2]) 485apply (erule constrains_weaken, blast) 486apply blast 487done 488 489(*Used to prove project_leadsETo_D*) 490lemma Join_project_ensures: 491 "[| extend h F\<squnion>G \<in> stable C; 492 F\<squnion>project h C G \<in> A ensures B |] 493 ==> extend h F\<squnion>G \<in> (C \<inter> extend_set h A) ensures (extend_set h B)" 494apply (auto simp add: ensures_eq extend_unless project_unless) 495apply (blast intro: extend_transient [THEN iffD2] transient_strengthen) 496apply (blast intro: project_transient_extend_set transient_strengthen) 497done 498 499text\<open>Lemma useful for both STRONG and WEAK progress, but the transient 500 condition's very strong\<close> 501 502(*The strange induction formula allows induction over the leadsTo 503 assumption's non-atomic precondition*) 504lemma PLD_lemma: 505 "[| extend h F\<squnion>G \<in> stable C; 506 F\<squnion>project h C G \<in> (project_set h C \<inter> A) leadsTo B |] 507 ==> extend h F\<squnion>G \<in> 508 C \<inter> extend_set h (project_set h C \<inter> A) leadsTo (extend_set h B)" 509apply (erule leadsTo_induct) 510 apply (blast intro: Join_project_ensures) 511 apply (blast intro: psp_stable2 [THEN leadsTo_weaken_L] leadsTo_Trans) 512apply (simp del: UN_simps add: Int_UN_distrib leadsTo_UN extend_set_Union) 513done 514 515lemma project_leadsTo_D_lemma: 516 "[| extend h F\<squnion>G \<in> stable C; 517 F\<squnion>project h C G \<in> (project_set h C \<inter> A) leadsTo B |] 518 ==> extend h F\<squnion>G \<in> (C \<inter> extend_set h A) leadsTo (extend_set h B)" 519apply (rule PLD_lemma [THEN leadsTo_weaken]) 520apply (auto simp add: split_extended_all) 521done 522 523lemma Join_project_LeadsTo: 524 "[| C = (reachable (extend h F\<squnion>G)); 525 F\<squnion>project h C G \<in> A LeadsTo B |] 526 ==> extend h F\<squnion>G \<in> (extend_set h A) LeadsTo (extend_set h B)" 527by (simp del: Join_stable add: LeadsTo_def project_leadsTo_D_lemma 528 project_set_reachable_extend_eq) 529 530 531subsection\<open>Towards the theorem \<open>project_Ensures_D\<close>\<close> 532 533lemma project_ensures_D_lemma: 534 "[| G \<in> stable ((C \<inter> extend_set h A) - (extend_set h B)); 535 F\<squnion>project h C G \<in> (project_set h C \<inter> A) ensures B; 536 extend h F\<squnion>G \<in> stable C |] 537 ==> extend h F\<squnion>G \<in> (C \<inter> extend_set h A) ensures (extend_set h B)" 538(*unless*) 539apply (auto intro!: project_unless2 [unfolded unless_def] 540 intro: project_extend_constrains_I 541 simp add: ensures_def) 542(*transient*) 543(*A G-action cannot occur*) 544 prefer 2 545 apply (blast intro: project_transient_extend_set) 546(*An F-action*) 547apply (force elim!: extend_transient [THEN iffD2, THEN transient_strengthen] 548 simp add: split_extended_all) 549done 550 551lemma project_ensures_D: 552 "[| F\<squnion>project h UNIV G \<in> A ensures B; 553 G \<in> stable (extend_set h A - extend_set h B) |] 554 ==> extend h F\<squnion>G \<in> (extend_set h A) ensures (extend_set h B)" 555apply (rule project_ensures_D_lemma [of _ UNIV, elim_format], auto) 556done 557 558lemma project_Ensures_D: 559 "[| F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> A Ensures B; 560 G \<in> stable (reachable (extend h F\<squnion>G) \<inter> extend_set h A - 561 extend_set h B) |] 562 ==> extend h F\<squnion>G \<in> (extend_set h A) Ensures (extend_set h B)" 563apply (unfold Ensures_def) 564apply (rule project_ensures_D_lemma [elim_format]) 565apply (auto simp add: project_set_reachable_extend_eq [symmetric]) 566done 567 568 569subsection\<open>Guarantees\<close> 570 571lemma project_act_Restrict_subset_project_act: 572 "project_act h (Restrict C act) \<subseteq> project_act h act" 573apply (auto simp add: project_act_def) 574done 575 576 577lemma subset_closed_ok_extend_imp_ok_project: 578 "[| extend h F ok G; subset_closed (AllowedActs F) |] 579 ==> F ok project h C G" 580apply (auto simp add: ok_def) 581apply (rename_tac act) 582apply (drule subsetD, blast) 583apply (rule_tac x = "Restrict C (extend_act h act)" in rev_image_eqI) 584apply simp + 585apply (cut_tac project_act_Restrict_subset_project_act) 586apply (auto simp add: subset_closed_def) 587done 588 589 590(*Weak precondition and postcondition 591 Not clear that it has a converse [or that we want one!]*) 592 593(*The raw version; 3rd premise could be weakened by adding the 594 precondition extend h F\<squnion>G \<in> X' *) 595lemma project_guarantees_raw: 596 assumes xguary: "F \<in> X guarantees Y" 597 and closed: "subset_closed (AllowedActs F)" 598 and project: "!!G. extend h F\<squnion>G \<in> X' 599 ==> F\<squnion>project h (C G) G \<in> X" 600 and extend: "!!G. [| F\<squnion>project h (C G) G \<in> Y |] 601 ==> extend h F\<squnion>G \<in> Y'" 602 shows "extend h F \<in> X' guarantees Y'" 603apply (rule xguary [THEN guaranteesD, THEN extend, THEN guaranteesI]) 604apply (blast intro: closed subset_closed_ok_extend_imp_ok_project) 605apply (erule project) 606done 607 608lemma project_guarantees: 609 "[| F \<in> X guarantees Y; subset_closed (AllowedActs F); 610 projecting C h F X' X; extending C h F Y' Y |] 611 ==> extend h F \<in> X' guarantees Y'" 612apply (rule guaranteesI) 613apply (auto simp add: guaranteesD projecting_def extending_def 614 subset_closed_ok_extend_imp_ok_project) 615done 616 617 618(*It seems that neither "guarantees" law can be proved from the other.*) 619 620 621subsection\<open>guarantees corollaries\<close> 622 623subsubsection\<open>Some could be deleted: the required versions are easy to prove\<close> 624 625lemma extend_guar_increasing: 626 "[| F \<in> UNIV guarantees increasing func; 627 subset_closed (AllowedActs F) |] 628 ==> extend h F \<in> X' guarantees increasing (func o f)" 629apply (erule project_guarantees) 630apply (rule_tac [3] extending_increasing) 631apply (rule_tac [2] projecting_UNIV, auto) 632done 633 634lemma extend_guar_Increasing: 635 "[| F \<in> UNIV guarantees Increasing func; 636 subset_closed (AllowedActs F) |] 637 ==> extend h F \<in> X' guarantees Increasing (func o f)" 638apply (erule project_guarantees) 639apply (rule_tac [3] extending_Increasing) 640apply (rule_tac [2] projecting_UNIV, auto) 641done 642 643lemma extend_guar_Always: 644 "[| F \<in> Always A guarantees Always B; 645 subset_closed (AllowedActs F) |] 646 ==> extend h F 647 \<in> Always(extend_set h A) guarantees Always(extend_set h B)" 648apply (erule project_guarantees) 649apply (rule_tac [3] extending_Always) 650apply (rule_tac [2] projecting_Always, auto) 651done 652 653 654subsubsection\<open>Guarantees with a leadsTo postcondition\<close> 655 656lemma project_leadsTo_D: 657 "F\<squnion>project h UNIV G \<in> A leadsTo B 658 ==> extend h F\<squnion>G \<in> (extend_set h A) leadsTo (extend_set h B)" 659apply (rule_tac C1 = UNIV in project_leadsTo_D_lemma [THEN leadsTo_weaken], auto) 660done 661 662lemma project_LeadsTo_D: 663 "F\<squnion>project h (reachable (extend h F\<squnion>G)) G \<in> A LeadsTo B 664 ==> extend h F\<squnion>G \<in> (extend_set h A) LeadsTo (extend_set h B)" 665apply (rule refl [THEN Join_project_LeadsTo], auto) 666done 667 668lemma extending_leadsTo: 669 "extending (%G. UNIV) h F 670 (extend_set h A leadsTo extend_set h B) (A leadsTo B)" 671apply (unfold extending_def) 672apply (blast intro: project_leadsTo_D) 673done 674 675lemma extending_LeadsTo: 676 "extending (%G. reachable (extend h F\<squnion>G)) h F 677 (extend_set h A LeadsTo extend_set h B) (A LeadsTo B)" 678apply (unfold extending_def) 679apply (blast intro: project_LeadsTo_D) 680done 681 682end 683 684end 685