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