1(* Title: ZF/UNITY/Guar.thy 2 Author: Sidi O Ehmety, Computer Laboratory 3 Copyright 2001 University of Cambridge 4 5Guarantees, etc. 6 7From Chandy and Sanders, "Reasoning About Program Composition", 8Technical Report 2000-003, University of Florida, 2000. 9 10Revised by Sidi Ehmety on January 2001 11 12Added \<in> Compatibility, weakest guarantees, etc. 13 14and Weakest existential property, 15from Charpentier and Chandy "Theorems about Composition", 16Fifth International Conference on Mathematics of Program, 2000. 17 18Theory ported from HOL. 19*) 20 21 22section\<open>The Chandy-Sanders Guarantees Operator\<close> 23 24theory Guar imports Comp begin 25 26 27(* To be moved to theory WFair???? *) 28lemma leadsTo_Basis': "[| F \<in> A co A \<union> B; F \<in> transient(A); st_set(B) |] ==> F \<in> A \<longmapsto> B" 29apply (frule constrainsD2) 30apply (drule_tac B = "A-B" in constrains_weaken_L, blast) 31apply (drule_tac B = "A-B" in transient_strengthen, blast) 32apply (blast intro: ensuresI [THEN leadsTo_Basis]) 33done 34 35 36 (*Existential and Universal properties. We formalize the two-program 37 case, proving equivalence with Chandy and Sanders's n-ary definitions*) 38 39definition 40 ex_prop :: "i => o" where 41 "ex_prop(X) == X<=program & 42 (\<forall>F \<in> program. \<forall>G \<in> program. F ok G \<longrightarrow> F \<in> X | G \<in> X \<longrightarrow> (F \<squnion> G) \<in> X)" 43 44definition 45 strict_ex_prop :: "i => o" where 46 "strict_ex_prop(X) == X<=program & 47 (\<forall>F \<in> program. \<forall>G \<in> program. F ok G \<longrightarrow> (F \<in> X | G \<in> X) \<longleftrightarrow> (F \<squnion> G \<in> X))" 48 49definition 50 uv_prop :: "i => o" where 51 "uv_prop(X) == X<=program & 52 (SKIP \<in> X & (\<forall>F \<in> program. \<forall>G \<in> program. F ok G \<longrightarrow> F \<in> X & G \<in> X \<longrightarrow> (F \<squnion> G) \<in> X))" 53 54definition 55 strict_uv_prop :: "i => o" where 56 "strict_uv_prop(X) == X<=program & 57 (SKIP \<in> X & (\<forall>F \<in> program. \<forall>G \<in> program. F ok G \<longrightarrow>(F \<in> X & G \<in> X) \<longleftrightarrow> (F \<squnion> G \<in> X)))" 58 59definition 60 guar :: "[i, i] => i" (infixl "guarantees" 55) where 61 (*higher than membership, lower than Co*) 62 "X guarantees Y == {F \<in> program. \<forall>G \<in> program. F ok G \<longrightarrow> F \<squnion> G \<in> X \<longrightarrow> F \<squnion> G \<in> Y}" 63 64definition 65 (* Weakest guarantees *) 66 wg :: "[i,i] => i" where 67 "wg(F,Y) == \<Union>({X \<in> Pow(program). F:(X guarantees Y)})" 68 69definition 70 (* Weakest existential property stronger than X *) 71 wx :: "i =>i" where 72 "wx(X) == \<Union>({Y \<in> Pow(program). Y<=X & ex_prop(Y)})" 73 74definition 75 (*Ill-defined programs can arise through "\<squnion>"*) 76 welldef :: i where 77 "welldef == {F \<in> program. Init(F) \<noteq> 0}" 78 79definition 80 refines :: "[i, i, i] => o" ("(3_ refines _ wrt _)" [10,10,10] 10) where 81 "G refines F wrt X == 82 \<forall>H \<in> program. (F ok H & G ok H & F \<squnion> H \<in> welldef \<inter> X) 83 \<longrightarrow> (G \<squnion> H \<in> welldef \<inter> X)" 84 85definition 86 iso_refines :: "[i,i, i] => o" ("(3_ iso'_refines _ wrt _)" [10,10,10] 10) where 87 "G iso_refines F wrt X == F \<in> welldef \<inter> X \<longrightarrow> G \<in> welldef \<inter> X" 88 89 90(*** existential properties ***) 91 92lemma ex_imp_subset_program: "ex_prop(X) ==> X\<subseteq>program" 93by (simp add: ex_prop_def) 94 95lemma ex1 [rule_format]: 96 "GG \<in> Fin(program) 97 ==> ex_prop(X) \<longrightarrow> GG \<inter> X\<noteq>0 \<longrightarrow> OK(GG, (%G. G)) \<longrightarrow>(\<Squnion>G \<in> GG. G) \<in> X" 98apply (unfold ex_prop_def) 99apply (erule Fin_induct) 100apply (simp_all add: OK_cons_iff) 101apply (safe elim!: not_emptyE, auto) 102done 103 104lemma ex2 [rule_format]: 105"X \<subseteq> program ==> 106 (\<forall>GG \<in> Fin(program). GG \<inter> X \<noteq> 0 \<longrightarrow> OK(GG,(%G. G))\<longrightarrow>(\<Squnion>G \<in> GG. G) \<in> X) 107 \<longrightarrow> ex_prop(X)" 108apply (unfold ex_prop_def, clarify) 109apply (drule_tac x = "{F,G}" in bspec) 110apply (simp_all add: OK_iff_ok) 111apply (auto intro: ok_sym) 112done 113 114(*Chandy & Sanders take this as a definition*) 115 116lemma ex_prop_finite: 117 "ex_prop(X) \<longleftrightarrow> (X\<subseteq>program & 118 (\<forall>GG \<in> Fin(program). GG \<inter> X \<noteq> 0 & OK(GG,(%G. G))\<longrightarrow>(\<Squnion>G \<in> GG. G) \<in> X))" 119apply auto 120apply (blast intro: ex1 ex2 dest: ex_imp_subset_program)+ 121done 122 123(* Equivalent definition of ex_prop given at the end of section 3*) 124lemma ex_prop_equiv: 125"ex_prop(X) \<longleftrightarrow> 126 X\<subseteq>program & (\<forall>G \<in> program. (G \<in> X \<longleftrightarrow> (\<forall>H \<in> program. (G component_of H) \<longrightarrow> H \<in> X)))" 127apply (unfold ex_prop_def component_of_def, safe, force, force, blast) 128apply (subst Join_commute) 129apply (blast intro: ok_sym) 130done 131 132(*** universal properties ***) 133 134lemma uv_imp_subset_program: "uv_prop(X)==> X\<subseteq>program" 135apply (unfold uv_prop_def) 136apply (simp (no_asm_simp)) 137done 138 139lemma uv1 [rule_format]: 140 "GG \<in> Fin(program) ==> 141 (uv_prop(X)\<longrightarrow> GG \<subseteq> X & OK(GG, (%G. G)) \<longrightarrow> (\<Squnion>G \<in> GG. G) \<in> X)" 142apply (unfold uv_prop_def) 143apply (erule Fin_induct) 144apply (auto simp add: OK_cons_iff) 145done 146 147lemma uv2 [rule_format]: 148 "X\<subseteq>program ==> 149 (\<forall>GG \<in> Fin(program). GG \<subseteq> X & OK(GG,(%G. G)) \<longrightarrow> (\<Squnion>G \<in> GG. G) \<in> X) 150 \<longrightarrow> uv_prop(X)" 151apply (unfold uv_prop_def, auto) 152apply (drule_tac x = 0 in bspec, simp+) 153apply (drule_tac x = "{F,G}" in bspec, simp) 154apply (force dest: ok_sym simp add: OK_iff_ok) 155done 156 157(*Chandy & Sanders take this as a definition*) 158lemma uv_prop_finite: 159"uv_prop(X) \<longleftrightarrow> X\<subseteq>program & 160 (\<forall>GG \<in> Fin(program). GG \<subseteq> X & OK(GG, %G. G) \<longrightarrow> (\<Squnion>G \<in> GG. G) \<in> X)" 161apply auto 162apply (blast dest: uv_imp_subset_program) 163apply (blast intro: uv1) 164apply (blast intro!: uv2 dest:) 165done 166 167(*** guarantees ***) 168lemma guaranteesI: 169 "[| (!!G. [| F ok G; F \<squnion> G \<in> X; G \<in> program |] ==> F \<squnion> G \<in> Y); 170 F \<in> program |] 171 ==> F \<in> X guarantees Y" 172by (simp add: guar_def component_def) 173 174lemma guaranteesD: 175 "[| F \<in> X guarantees Y; F ok G; F \<squnion> G \<in> X; G \<in> program |] 176 ==> F \<squnion> G \<in> Y" 177by (simp add: guar_def component_def) 178 179 180(*This version of guaranteesD matches more easily in the conclusion 181 The major premise can no longer be F\<subseteq>H since we need to reason about G*) 182 183lemma component_guaranteesD: 184 "[| F \<in> X guarantees Y; F \<squnion> G = H; H \<in> X; F ok G; G \<in> program |] 185 ==> H \<in> Y" 186by (simp add: guar_def, blast) 187 188lemma guarantees_weaken: 189 "[| F \<in> X guarantees X'; Y \<subseteq> X; X' \<subseteq> Y' |] ==> F \<in> Y guarantees Y'" 190by (simp add: guar_def, auto) 191 192lemma subset_imp_guarantees_program: 193 "X \<subseteq> Y ==> X guarantees Y = program" 194by (unfold guar_def, blast) 195 196(*Equivalent to subset_imp_guarantees_UNIV but more intuitive*) 197lemma subset_imp_guarantees: 198 "[| X \<subseteq> Y; F \<in> program |] ==> F \<in> X guarantees Y" 199by (unfold guar_def, blast) 200 201lemma component_of_Join1: "F ok G ==> F component_of (F \<squnion> G)" 202by (unfold component_of_def, blast) 203 204lemma component_of_Join2: "F ok G ==> G component_of (F \<squnion> G)" 205apply (subst Join_commute) 206apply (blast intro: ok_sym component_of_Join1) 207done 208 209(*Remark at end of section 4.1 *) 210lemma ex_prop_imp: 211 "ex_prop(Y) ==> (Y = (program guarantees Y))" 212apply (simp (no_asm_use) add: ex_prop_equiv guar_def component_of_def) 213apply clarify 214apply (rule equalityI, blast, safe) 215apply (drule_tac x = x in bspec, assumption, force) 216done 217 218lemma guarantees_imp: "(Y = program guarantees Y) ==> ex_prop(Y)" 219apply (unfold guar_def) 220apply (simp (no_asm_simp) add: ex_prop_equiv) 221apply safe 222apply (blast intro: elim: equalityE) 223apply (simp_all (no_asm_use) add: component_of_def) 224apply (force elim: equalityE)+ 225done 226 227lemma ex_prop_equiv2: "(ex_prop(Y)) \<longleftrightarrow> (Y = program guarantees Y)" 228by (blast intro: ex_prop_imp guarantees_imp) 229 230(** Distributive laws. Re-orient to perform miniscoping **) 231 232lemma guarantees_UN_left: 233 "i \<in> I ==>(\<Union>i \<in> I. X(i)) guarantees Y = (\<Inter>i \<in> I. X(i) guarantees Y)" 234apply (unfold guar_def) 235apply (rule equalityI, safe) 236 prefer 2 apply force 237apply blast+ 238done 239 240lemma guarantees_Un_left: 241 "(X \<union> Y) guarantees Z = (X guarantees Z) \<inter> (Y guarantees Z)" 242apply (unfold guar_def) 243apply (rule equalityI, safe, blast+) 244done 245 246lemma guarantees_INT_right: 247 "i \<in> I ==> X guarantees (\<Inter>i \<in> I. Y(i)) = (\<Inter>i \<in> I. X guarantees Y(i))" 248apply (unfold guar_def) 249apply (rule equalityI, safe, blast+) 250done 251 252lemma guarantees_Int_right: 253 "Z guarantees (X \<inter> Y) = (Z guarantees X) \<inter> (Z guarantees Y)" 254by (unfold guar_def, blast) 255 256lemma guarantees_Int_right_I: 257 "[| F \<in> Z guarantees X; F \<in> Z guarantees Y |] 258 ==> F \<in> Z guarantees (X \<inter> Y)" 259by (simp (no_asm_simp) add: guarantees_Int_right) 260 261lemma guarantees_INT_right_iff: 262 "i \<in> I==> (F \<in> X guarantees (\<Inter>i \<in> I. Y(i))) \<longleftrightarrow> 263 (\<forall>i \<in> I. F \<in> X guarantees Y(i))" 264by (simp add: guarantees_INT_right INT_iff, blast) 265 266 267lemma shunting: "(X guarantees Y) = (program guarantees ((program-X) \<union> Y))" 268by (unfold guar_def, auto) 269 270lemma contrapositive: 271 "(X guarantees Y) = (program - Y) guarantees (program -X)" 272by (unfold guar_def, blast) 273 274(** The following two can be expressed using intersection and subset, which 275 is more faithful to the text but looks cryptic. 276**) 277 278lemma combining1: 279 "[| F \<in> V guarantees X; F \<in> (X \<inter> Y) guarantees Z |] 280 ==> F \<in> (V \<inter> Y) guarantees Z" 281by (unfold guar_def, blast) 282 283lemma combining2: 284 "[| F \<in> V guarantees (X \<union> Y); F \<in> Y guarantees Z |] 285 ==> F \<in> V guarantees (X \<union> Z)" 286by (unfold guar_def, blast) 287 288 289(** The following two follow Chandy-Sanders, but the use of object-quantifiers 290 does not suit Isabelle... **) 291 292(*Premise should be (!!i. i \<in> I ==> F \<in> X guarantees Y i) *) 293lemma all_guarantees: 294 "[| \<forall>i \<in> I. F \<in> X guarantees Y(i); i \<in> I |] 295 ==> F \<in> X guarantees (\<Inter>i \<in> I. Y(i))" 296by (unfold guar_def, blast) 297 298(*Premises should be [| F \<in> X guarantees Y i; i \<in> I |] *) 299lemma ex_guarantees: 300 "\<exists>i \<in> I. F \<in> X guarantees Y(i) ==> F \<in> X guarantees (\<Union>i \<in> I. Y(i))" 301by (unfold guar_def, blast) 302 303 304(*** Additional guarantees laws, by lcp ***) 305 306lemma guarantees_Join_Int: 307 "[| F \<in> U guarantees V; G \<in> X guarantees Y; F ok G |] 308 ==> F \<squnion> G: (U \<inter> X) guarantees (V \<inter> Y)" 309 310apply (unfold guar_def) 311apply (simp (no_asm)) 312apply safe 313apply (simp add: Join_assoc) 314apply (subgoal_tac "F \<squnion> G \<squnion> Ga = G \<squnion> (F \<squnion> Ga) ") 315apply (simp add: ok_commute) 316apply (simp (no_asm_simp) add: Join_ac) 317done 318 319lemma guarantees_Join_Un: 320 "[| F \<in> U guarantees V; G \<in> X guarantees Y; F ok G |] 321 ==> F \<squnion> G: (U \<union> X) guarantees (V \<union> Y)" 322apply (unfold guar_def) 323apply (simp (no_asm)) 324apply safe 325apply (simp add: Join_assoc) 326apply (subgoal_tac "F \<squnion> G \<squnion> Ga = G \<squnion> (F \<squnion> Ga) ") 327apply (rotate_tac 4) 328apply (drule_tac x = "F \<squnion> Ga" in bspec) 329apply (simp (no_asm)) 330apply (force simp add: ok_commute) 331apply (simp (no_asm_simp) add: Join_ac) 332done 333 334lemma guarantees_JOIN_INT: 335 "[| \<forall>i \<in> I. F(i) \<in> X(i) guarantees Y(i); OK(I,F); i \<in> I |] 336 ==> (\<Squnion>i \<in> I. F(i)) \<in> (\<Inter>i \<in> I. X(i)) guarantees (\<Inter>i \<in> I. Y(i))" 337apply (unfold guar_def, safe) 338 prefer 2 apply blast 339apply (drule_tac x = xa in bspec) 340apply (simp_all add: INT_iff, safe) 341apply (drule_tac x = "(\<Squnion>x \<in> (I-{xa}) . F (x)) \<squnion> G" and A=program in bspec) 342apply (auto intro: OK_imp_ok simp add: Join_assoc [symmetric] JOIN_Join_diff JOIN_absorb) 343done 344 345lemma guarantees_JOIN_UN: 346 "[| \<forall>i \<in> I. F(i) \<in> X(i) guarantees Y(i); OK(I,F) |] 347 ==> JOIN(I,F) \<in> (\<Union>i \<in> I. X(i)) guarantees (\<Union>i \<in> I. Y(i))" 348apply (unfold guar_def, auto) 349apply (drule_tac x = y in bspec, simp_all, safe) 350apply (rename_tac G y) 351apply (drule_tac x = "JOIN (I-{y}, F) \<squnion> G" and A=program in bspec) 352apply (auto intro: OK_imp_ok simp add: Join_assoc [symmetric] JOIN_Join_diff JOIN_absorb) 353done 354 355(*** guarantees laws for breaking down the program, by lcp ***) 356 357lemma guarantees_Join_I1: 358 "[| F \<in> X guarantees Y; F ok G |] ==> F \<squnion> G \<in> X guarantees Y" 359apply (simp add: guar_def, safe) 360apply (simp add: Join_assoc) 361done 362 363lemma guarantees_Join_I2: 364 "[| G \<in> X guarantees Y; F ok G |] ==> F \<squnion> G \<in> X guarantees Y" 365apply (simp add: Join_commute [of _ G] ok_commute [of _ G]) 366apply (blast intro: guarantees_Join_I1) 367done 368 369lemma guarantees_JOIN_I: 370 "[| i \<in> I; F(i) \<in> X guarantees Y; OK(I,F) |] 371 ==> (\<Squnion>i \<in> I. F(i)) \<in> X guarantees Y" 372apply (unfold guar_def, safe) 373apply (drule_tac x = "JOIN (I-{i},F) \<squnion> G" in bspec) 374apply (simp (no_asm)) 375apply (auto intro: OK_imp_ok simp add: JOIN_Join_diff Join_assoc [symmetric]) 376done 377 378(*** well-definedness ***) 379 380lemma Join_welldef_D1: "F \<squnion> G \<in> welldef ==> programify(F) \<in> welldef" 381by (unfold welldef_def, auto) 382 383lemma Join_welldef_D2: "F \<squnion> G \<in> welldef ==> programify(G) \<in> welldef" 384by (unfold welldef_def, auto) 385 386(*** refinement ***) 387 388lemma refines_refl: "F refines F wrt X" 389by (unfold refines_def, blast) 390 391(* More results on guarantees, added by Sidi Ehmety from Chandy & Sander, section 6 *) 392 393lemma wg_type: "wg(F, X) \<subseteq> program" 394by (unfold wg_def, auto) 395 396lemma guarantees_type: "X guarantees Y \<subseteq> program" 397by (unfold guar_def, auto) 398 399lemma wgD2: "G \<in> wg(F, X) ==> G \<in> program & F \<in> program" 400apply (unfold wg_def, auto) 401apply (blast dest: guarantees_type [THEN subsetD]) 402done 403 404lemma guarantees_equiv: 405"(F \<in> X guarantees Y) \<longleftrightarrow> 406 F \<in> program & (\<forall>H \<in> program. H \<in> X \<longrightarrow> (F component_of H \<longrightarrow> H \<in> Y))" 407by (unfold guar_def component_of_def, force) 408 409lemma wg_weakest: 410 "!!X. [| F \<in> (X guarantees Y); X \<subseteq> program |] ==> X \<subseteq> wg(F,Y)" 411by (unfold wg_def, auto) 412 413lemma wg_guarantees: "F \<in> program ==> F \<in> wg(F,Y) guarantees Y" 414by (unfold wg_def guar_def, blast) 415 416lemma wg_equiv: 417 "H \<in> wg(F,X) \<longleftrightarrow> 418 ((F component_of H \<longrightarrow> H \<in> X) & F \<in> program & H \<in> program)" 419apply (simp add: wg_def guarantees_equiv) 420apply (rule iffI, safe) 421apply (rule_tac [4] x = "{H}" in bexI) 422apply (rule_tac [3] x = "{H}" in bexI, blast+) 423done 424 425lemma component_of_wg: 426 "F component_of H ==> H \<in> wg(F,X) \<longleftrightarrow> (H \<in> X & F \<in> program & H \<in> program)" 427by (simp (no_asm_simp) add: wg_equiv) 428 429lemma wg_finite [rule_format]: 430"\<forall>FF \<in> Fin(program). FF \<inter> X \<noteq> 0 \<longrightarrow> OK(FF, %F. F) 431 \<longrightarrow> (\<forall>F \<in> FF. ((\<Squnion>F \<in> FF. F) \<in> wg(F,X)) \<longleftrightarrow> ((\<Squnion>F \<in> FF. F) \<in> X))" 432apply clarify 433apply (subgoal_tac "F component_of (\<Squnion>F \<in> FF. F) ") 434apply (drule_tac X = X in component_of_wg) 435apply (force dest!: Fin.dom_subset [THEN subsetD, THEN PowD]) 436apply (simp_all add: component_of_def) 437apply (rule_tac x = "\<Squnion>F \<in> (FF-{F}) . F" in exI) 438apply (auto intro: JOIN_Join_diff dest: ok_sym simp add: OK_iff_ok) 439done 440 441lemma wg_ex_prop: 442 "ex_prop(X) ==> (F \<in> X) \<longleftrightarrow> (\<forall>H \<in> program. H \<in> wg(F,X) & F \<in> program)" 443apply (simp (no_asm_use) add: ex_prop_equiv wg_equiv) 444apply blast 445done 446 447(** From Charpentier and Chandy "Theorems About Composition" **) 448(* Proposition 2 *) 449lemma wx_subset: "wx(X)\<subseteq>X" 450by (unfold wx_def, auto) 451 452lemma wx_ex_prop: "ex_prop(wx(X))" 453apply (simp (no_asm_use) add: ex_prop_def wx_def) 454apply safe 455apply blast 456apply (rule_tac x=x in bexI, force, simp)+ 457done 458 459lemma wx_weakest: "\<forall>Z. Z\<subseteq>program \<longrightarrow> Z\<subseteq> X \<longrightarrow> ex_prop(Z) \<longrightarrow> Z \<subseteq> wx(X)" 460by (unfold wx_def, auto) 461 462(* Proposition 6 *) 463lemma wx'_ex_prop: 464 "ex_prop({F \<in> program. \<forall>G \<in> program. F ok G \<longrightarrow> F \<squnion> G \<in> X})" 465apply (unfold ex_prop_def, safe) 466 apply (drule_tac x = "G \<squnion> Ga" in bspec) 467 apply (simp (no_asm)) 468 apply (force simp add: Join_assoc) 469apply (drule_tac x = "F \<squnion> Ga" in bspec) 470 apply (simp (no_asm)) 471apply (simp (no_asm_use)) 472apply safe 473 apply (simp (no_asm_simp) add: ok_commute) 474apply (subgoal_tac "F \<squnion> G = G \<squnion> F") 475 apply (simp (no_asm_simp) add: Join_assoc) 476apply (simp (no_asm) add: Join_commute) 477done 478 479(* Equivalence with the other definition of wx *) 480 481lemma wx_equiv: 482 "wx(X) = {F \<in> program. \<forall>G \<in> program. F ok G \<longrightarrow> (F \<squnion> G) \<in> X}" 483apply (unfold wx_def) 484apply (rule equalityI, safe, blast) 485 apply (simp (no_asm_use) add: ex_prop_def) 486apply blast 487apply (rule_tac B = "{F \<in> program. \<forall>G \<in> program. F ok G \<longrightarrow> F \<squnion> G \<in> X}" 488 in UnionI, 489 safe) 490apply (rule_tac [2] wx'_ex_prop) 491apply (drule_tac x=SKIP in bspec, simp)+ 492apply auto 493done 494 495(* Propositions 7 to 11 are all about this second definition of wx. And 496 by equivalence between the two definition, they are the same as the ones proved *) 497 498 499(* Proposition 12 *) 500(* Main result of the paper *) 501lemma guarantees_wx_eq: "(X guarantees Y) = wx((program-X) \<union> Y)" 502by (auto simp add: guar_def wx_equiv) 503 504(* 505{* Corollary, but this result has already been proved elsewhere *} 506 "ex_prop(X guarantees Y)" 507*) 508 509(* Rules given in section 7 of Chandy and Sander's 510 Reasoning About Program composition paper *) 511 512lemma stable_guarantees_Always: 513 "[| Init(F) \<subseteq> A; F \<in> program |] ==> F \<in> stable(A) guarantees Always(A)" 514apply (rule guaranteesI) 515 prefer 2 apply assumption 516apply (simp (no_asm) add: Join_commute) 517apply (rule stable_Join_Always1) 518apply (simp_all add: invariant_def) 519apply (auto simp add: programify_def initially_def) 520done 521 522lemma constrains_guarantees_leadsTo: 523 "[| F \<in> transient(A); st_set(B) |] 524 ==> F: (A co A \<union> B) guarantees (A \<longmapsto> (B-A))" 525apply (rule guaranteesI) 526 prefer 2 apply (blast dest: transient_type [THEN subsetD]) 527apply (rule leadsTo_Basis') 528 apply (blast intro: constrains_weaken_R) 529 apply (blast intro!: Join_transient_I1, blast) 530done 531 532end 533