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