src/HOL/UNITY/Guar.thy
author hoelzl
Thu Sep 02 10:14:32 2010 +0200 (2010-09-02)
changeset 39072 1030b1a166ef
parent 35416 d8d7d1b785af
child 44871 fbfdc5ac86be
permissions -rw-r--r--
Add lessThan_Suc_eq_insert_0
     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 [rule_format]: 
    79  "[| ex_prop X; finite GG |] ==>  
    80      GG \<inter> X \<noteq> {}--> OK GG (%G. G) --> (\<Squnion>G \<in> GG. G) \<in> X"
    81 apply (unfold ex_prop_def)
    82 apply (erule finite_induct)
    83 apply (auto simp add: OK_insert_iff Int_insert_left)
    84 done
    85 
    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 [rule_format]: 
   116      "[| uv_prop X; finite GG |] 
   117       ==> GG \<subseteq> X & OK GG (%G. G) --> (\<Squnion>G \<in> GG. G) \<in> X"
   118 apply (unfold uv_prop_def)
   119 apply (erule finite_induct)
   120 apply (auto simp add: Int_insert_left OK_insert_iff)
   121 done
   122 
   123 lemma uv2: 
   124      "\<forall>GG. finite GG & GG \<subseteq> X & OK GG (%G. G) --> (\<Squnion>G \<in> GG. G) \<in> X  
   125       ==> uv_prop X"
   126 apply (unfold uv_prop_def)
   127 apply (rule conjI)
   128  apply (drule_tac x = "{}" in spec)
   129  prefer 2
   130  apply clarify 
   131  apply (drule_tac x = "{F,G}" in spec)
   132 apply (auto dest: ok_sym simp add: OK_iff_ok)
   133 done
   134 
   135 (*Chandy & Sanders take this as a definition*)
   136 lemma uv_prop_finite:
   137      "uv_prop X = 
   138       (\<forall>GG. finite GG & GG \<subseteq> X & OK GG (%G. G) --> (\<Squnion>G \<in> GG. G): X)"
   139 by (blast intro: uv1 uv2)
   140 
   141 subsection{*Guarantees*}
   142 
   143 lemma guaranteesI:
   144      "(!!G. [| F ok G; F\<squnion>G \<in> X |] ==> F\<squnion>G \<in> Y) ==> F \<in> X guarantees Y"
   145 by (simp add: guar_def component_def)
   146 
   147 lemma guaranteesD: 
   148      "[| F \<in> X guarantees Y;  F ok G;  F\<squnion>G \<in> X |] ==> F\<squnion>G \<in> Y"
   149 by (unfold guar_def component_def, blast)
   150 
   151 (*This version of guaranteesD matches more easily in the conclusion
   152   The major premise can no longer be  F \<subseteq> H since we need to reason about G*)
   153 lemma component_guaranteesD: 
   154      "[| F \<in> X guarantees Y;  F\<squnion>G = H;  H \<in> X;  F ok G |] ==> H \<in> Y"
   155 by (unfold guar_def, blast)
   156 
   157 lemma guarantees_weaken: 
   158      "[| F \<in> X guarantees X'; Y \<subseteq> X; X' \<subseteq> Y' |] ==> F \<in> Y guarantees Y'"
   159 by (unfold guar_def, blast)
   160 
   161 lemma subset_imp_guarantees_UNIV: "X \<subseteq> Y ==> X guarantees Y = UNIV"
   162 by (unfold guar_def, blast)
   163 
   164 (*Equivalent to subset_imp_guarantees_UNIV but more intuitive*)
   165 lemma subset_imp_guarantees: "X \<subseteq> Y ==> F \<in> X guarantees Y"
   166 by (unfold guar_def, blast)
   167 
   168 (*Remark at end of section 4.1 *)
   169 
   170 lemma ex_prop_imp: "ex_prop Y ==> (Y = UNIV guarantees Y)"
   171 apply (simp (no_asm_use) add: guar_def ex_prop_equiv)
   172 apply safe
   173  apply (drule_tac x = x in spec)
   174  apply (drule_tac [2] x = x in spec)
   175  apply (drule_tac [2] sym)
   176 apply (auto simp add: component_of_def)
   177 done
   178 
   179 lemma guarantees_imp: "(Y = UNIV guarantees Y) ==> ex_prop(Y)"
   180 by (auto simp add: guar_def ex_prop_equiv component_of_def dest: sym)
   181 
   182 lemma ex_prop_equiv2: "(ex_prop Y) = (Y = UNIV guarantees Y)"
   183 apply (rule iffI)
   184 apply (rule ex_prop_imp)
   185 apply (auto simp add: guarantees_imp) 
   186 done
   187 
   188 
   189 subsection{*Distributive Laws.  Re-Orient to Perform Miniscoping*}
   190 
   191 lemma guarantees_UN_left: 
   192      "(\<Union>i \<in> I. X i) guarantees Y = (\<Inter>i \<in> I. X i guarantees Y)"
   193 by (unfold guar_def, blast)
   194 
   195 lemma guarantees_Un_left: 
   196      "(X \<union> Y) guarantees Z = (X guarantees Z) \<inter> (Y guarantees Z)"
   197 by (unfold guar_def, blast)
   198 
   199 lemma guarantees_INT_right: 
   200      "X guarantees (\<Inter>i \<in> I. Y i) = (\<Inter>i \<in> I. X guarantees Y i)"
   201 by (unfold guar_def, blast)
   202 
   203 lemma guarantees_Int_right: 
   204      "Z guarantees (X \<inter> Y) = (Z guarantees X) \<inter> (Z guarantees Y)"
   205 by (unfold guar_def, blast)
   206 
   207 lemma guarantees_Int_right_I:
   208      "[| F \<in> Z guarantees X;  F \<in> Z guarantees Y |]  
   209      ==> F \<in> Z guarantees (X \<inter> Y)"
   210 by (simp add: guarantees_Int_right)
   211 
   212 lemma guarantees_INT_right_iff:
   213      "(F \<in> X guarantees (INTER I Y)) = (\<forall>i\<in>I. F \<in> X guarantees (Y i))"
   214 by (simp add: guarantees_INT_right)
   215 
   216 lemma shunting: "(X guarantees Y) = (UNIV guarantees (-X \<union> Y))"
   217 by (unfold guar_def, blast)
   218 
   219 lemma contrapositive: "(X guarantees Y) = -Y guarantees -X"
   220 by (unfold guar_def, blast)
   221 
   222 (** The following two can be expressed using intersection and subset, which
   223     is more faithful to the text but looks cryptic.
   224 **)
   225 
   226 lemma combining1: 
   227     "[| F \<in> V guarantees X;  F \<in> (X \<inter> Y) guarantees Z |] 
   228      ==> F \<in> (V \<inter> Y) guarantees Z"
   229 by (unfold guar_def, blast)
   230 
   231 lemma combining2: 
   232     "[| F \<in> V guarantees (X \<union> Y);  F \<in> Y guarantees Z |] 
   233      ==> F \<in> V guarantees (X \<union> Z)"
   234 by (unfold guar_def, blast)
   235 
   236 (** The following two follow Chandy-Sanders, but the use of object-quantifiers
   237     does not suit Isabelle... **)
   238 
   239 (*Premise should be (!!i. i \<in> I ==> F \<in> X guarantees Y i) *)
   240 lemma all_guarantees: 
   241      "\<forall>i\<in>I. F \<in> X guarantees (Y i) ==> F \<in> X guarantees (\<Inter>i \<in> I. Y i)"
   242 by (unfold guar_def, blast)
   243 
   244 (*Premises should be [| F \<in> X guarantees Y i; i \<in> I |] *)
   245 lemma ex_guarantees: 
   246      "\<exists>i\<in>I. F \<in> X guarantees (Y i) ==> F \<in> X guarantees (\<Union>i \<in> I. Y i)"
   247 by (unfold guar_def, blast)
   248 
   249 
   250 subsection{*Guarantees: Additional Laws (by lcp)*}
   251 
   252 lemma guarantees_Join_Int: 
   253     "[| F \<in> U guarantees V;  G \<in> X guarantees Y; F ok G |]  
   254      ==> F\<squnion>G \<in> (U \<inter> X) guarantees (V \<inter> Y)"
   255 apply (simp add: guar_def, safe)
   256  apply (simp add: Join_assoc)
   257 apply (subgoal_tac "F\<squnion>G\<squnion>Ga = G\<squnion>(F\<squnion>Ga) ")
   258  apply (simp add: ok_commute)
   259 apply (simp add: Join_ac)
   260 done
   261 
   262 lemma guarantees_Join_Un: 
   263     "[| F \<in> U guarantees V;  G \<in> X guarantees Y; F ok G |]   
   264      ==> F\<squnion>G \<in> (U \<union> X) guarantees (V \<union> Y)"
   265 apply (simp add: guar_def, safe)
   266  apply (simp add: Join_assoc)
   267 apply (subgoal_tac "F\<squnion>G\<squnion>Ga = G\<squnion>(F\<squnion>Ga) ")
   268  apply (simp add: ok_commute)
   269 apply (simp add: Join_ac)
   270 done
   271 
   272 lemma guarantees_JN_INT: 
   273      "[| \<forall>i\<in>I. F i \<in> X i guarantees Y i;  OK I F |]  
   274       ==> (JOIN I F) \<in> (INTER I X) guarantees (INTER I Y)"
   275 apply (unfold guar_def, auto)
   276 apply (drule bspec, assumption)
   277 apply (rename_tac "i")
   278 apply (drule_tac x = "JOIN (I-{i}) F\<squnion>G" in spec)
   279 apply (auto intro: OK_imp_ok
   280             simp add: Join_assoc [symmetric] JN_Join_diff JN_absorb)
   281 done
   282 
   283 lemma guarantees_JN_UN: 
   284     "[| \<forall>i\<in>I. F i \<in> X i guarantees Y i;  OK I F |]  
   285      ==> (JOIN I F) \<in> (UNION I X) guarantees (UNION I Y)"
   286 apply (unfold guar_def, auto)
   287 apply (drule bspec, assumption)
   288 apply (rename_tac "i")
   289 apply (drule_tac x = "JOIN (I-{i}) F\<squnion>G" in spec)
   290 apply (auto intro: OK_imp_ok
   291             simp add: Join_assoc [symmetric] JN_Join_diff JN_absorb)
   292 done
   293 
   294 
   295 subsection{*Guarantees Laws for Breaking Down the Program (by lcp)*}
   296 
   297 lemma guarantees_Join_I1: 
   298      "[| F \<in> X guarantees Y;  F ok G |] ==> F\<squnion>G \<in> X guarantees Y"
   299 by (simp add: guar_def Join_assoc)
   300 
   301 lemma guarantees_Join_I2:         
   302      "[| G \<in> X guarantees Y;  F ok G |] ==> F\<squnion>G \<in> X guarantees Y"
   303 apply (simp add: Join_commute [of _ G] ok_commute [of _ G])
   304 apply (blast intro: guarantees_Join_I1)
   305 done
   306 
   307 lemma guarantees_JN_I: 
   308      "[| i \<in> I;  F i \<in> X guarantees Y;  OK I F |]  
   309       ==> (\<Squnion>i \<in> I. (F i)) \<in> X guarantees Y"
   310 apply (unfold guar_def, clarify)
   311 apply (drule_tac x = "JOIN (I-{i}) F\<squnion>G" in spec)
   312 apply (auto intro: OK_imp_ok 
   313             simp add: JN_Join_diff JN_Join_diff Join_assoc [symmetric])
   314 done
   315 
   316 
   317 (*** well-definedness ***)
   318 
   319 lemma Join_welldef_D1: "F\<squnion>G \<in> welldef ==> F \<in> welldef"
   320 by (unfold welldef_def, auto)
   321 
   322 lemma Join_welldef_D2: "F\<squnion>G \<in> welldef ==> G \<in> welldef"
   323 by (unfold welldef_def, auto)
   324 
   325 (*** refinement ***)
   326 
   327 lemma refines_refl: "F refines F wrt X"
   328 by (unfold refines_def, blast)
   329 
   330 (*We'd like transitivity, but how do we get it?*)
   331 lemma refines_trans:
   332      "[| H refines G wrt X;  G refines F wrt X |] ==> H refines F wrt X"
   333 apply (simp add: refines_def) 
   334 oops
   335 
   336 
   337 lemma strict_ex_refine_lemma: 
   338      "strict_ex_prop X  
   339       ==> (\<forall>H. F ok H & G ok H & F\<squnion>H \<in> X --> G\<squnion>H \<in> X)  
   340               = (F \<in> X --> G \<in> X)"
   341 by (unfold strict_ex_prop_def, auto)
   342 
   343 lemma strict_ex_refine_lemma_v: 
   344      "strict_ex_prop X  
   345       ==> (\<forall>H. F ok H & G ok H & F\<squnion>H \<in> welldef & F\<squnion>H \<in> X --> G\<squnion>H \<in> X) =  
   346           (F \<in> welldef \<inter> X --> G \<in> X)"
   347 apply (unfold strict_ex_prop_def, safe)
   348 apply (erule_tac x = SKIP and P = "%H. ?PP H --> ?RR H" in allE)
   349 apply (auto dest: Join_welldef_D1 Join_welldef_D2)
   350 done
   351 
   352 lemma ex_refinement_thm:
   353      "[| strict_ex_prop X;   
   354          \<forall>H. F ok H & G ok H & F\<squnion>H \<in> welldef \<inter> X --> G\<squnion>H \<in> welldef |]  
   355       ==> (G refines F wrt X) = (G iso_refines F wrt X)"
   356 apply (rule_tac x = SKIP in allE, assumption)
   357 apply (simp add: refines_def iso_refines_def strict_ex_refine_lemma_v)
   358 done
   359 
   360 
   361 lemma strict_uv_refine_lemma: 
   362      "strict_uv_prop X ==> 
   363       (\<forall>H. F ok H & G ok H & F\<squnion>H \<in> X --> G\<squnion>H \<in> X) = (F \<in> X --> G \<in> X)"
   364 by (unfold strict_uv_prop_def, blast)
   365 
   366 lemma strict_uv_refine_lemma_v: 
   367      "strict_uv_prop X  
   368       ==> (\<forall>H. F ok H & G ok H & F\<squnion>H \<in> welldef & F\<squnion>H \<in> X --> G\<squnion>H \<in> X) =  
   369           (F \<in> welldef \<inter> X --> G \<in> X)"
   370 apply (unfold strict_uv_prop_def, safe)
   371 apply (erule_tac x = SKIP and P = "%H. ?PP H --> ?RR H" in allE)
   372 apply (auto dest: Join_welldef_D1 Join_welldef_D2)
   373 done
   374 
   375 lemma uv_refinement_thm:
   376      "[| strict_uv_prop X;   
   377          \<forall>H. F ok H & G ok H & F\<squnion>H \<in> welldef \<inter> X --> 
   378              G\<squnion>H \<in> welldef |]  
   379       ==> (G refines F wrt X) = (G iso_refines F wrt X)"
   380 apply (rule_tac x = SKIP in allE, assumption)
   381 apply (simp add: refines_def iso_refines_def strict_uv_refine_lemma_v)
   382 done
   383 
   384 (* Added by Sidi Ehmety from Chandy & Sander, section 6 *)
   385 lemma guarantees_equiv: 
   386     "(F \<in> X guarantees Y) = (\<forall>H. H \<in> X \<longrightarrow> (F component_of H \<longrightarrow> H \<in> Y))"
   387 by (unfold guar_def component_of_def, auto)
   388 
   389 lemma wg_weakest: "!!X. F\<in> (X guarantees Y) ==> X \<subseteq> (wg F Y)"
   390 by (unfold wg_def, auto)
   391 
   392 lemma wg_guarantees: "F\<in> ((wg F Y) guarantees Y)"
   393 by (unfold wg_def guar_def, blast)
   394 
   395 lemma wg_equiv: "(H \<in> wg F X) = (F component_of H --> H \<in> X)"
   396 by (simp add: guarantees_equiv wg_def, blast)
   397 
   398 lemma component_of_wg: "F component_of H ==> (H \<in> wg F X) = (H \<in> X)"
   399 by (simp add: wg_equiv)
   400 
   401 lemma wg_finite: 
   402     "\<forall>FF. finite FF & FF \<inter> X \<noteq> {} --> OK FF (%F. F)  
   403           --> (\<forall>F\<in>FF. ((\<Squnion>F \<in> FF. F): wg F X) = ((\<Squnion>F \<in> FF. F):X))"
   404 apply clarify
   405 apply (subgoal_tac "F component_of (\<Squnion>F \<in> FF. F) ")
   406 apply (drule_tac X = X in component_of_wg, simp)
   407 apply (simp add: component_of_def)
   408 apply (rule_tac x = "\<Squnion>F \<in> (FF-{F}) . F" in exI)
   409 apply (auto intro: JN_Join_diff dest: ok_sym simp add: OK_iff_ok)
   410 done
   411 
   412 lemma wg_ex_prop: "ex_prop X ==> (F \<in> X) = (\<forall>H. H \<in> wg F X)"
   413 apply (simp (no_asm_use) add: ex_prop_equiv wg_equiv)
   414 apply blast
   415 done
   416 
   417 (** From Charpentier and Chandy "Theorems About Composition" **)
   418 (* Proposition 2 *)
   419 lemma wx_subset: "(wx X)<=X"
   420 by (unfold wx_def, auto)
   421 
   422 lemma wx_ex_prop: "ex_prop (wx X)"
   423 apply (simp add: wx_def ex_prop_equiv cong: bex_cong, safe, blast)
   424 apply force 
   425 done
   426 
   427 lemma wx_weakest: "\<forall>Z. Z<= X --> ex_prop Z --> Z \<subseteq> wx X"
   428 by (auto simp add: wx_def)
   429 
   430 (* Proposition 6 *)
   431 lemma wx'_ex_prop: "ex_prop({F. \<forall>G. F ok G --> F\<squnion>G \<in> X})"
   432 apply (unfold ex_prop_def, safe)
   433  apply (drule_tac x = "G\<squnion>Ga" in spec)
   434  apply (force simp add: ok_Join_iff1 Join_assoc)
   435 apply (drule_tac x = "F\<squnion>Ga" in spec)
   436 apply (simp add: ok_Join_iff1 ok_commute  Join_ac) 
   437 done
   438 
   439 text{* Equivalence with the other definition of wx *}
   440 
   441 lemma wx_equiv: "wx X = {F. \<forall>G. F ok G --> (F\<squnion>G) \<in> X}"
   442 apply (unfold wx_def, safe)
   443  apply (simp add: ex_prop_def, blast) 
   444 apply (simp (no_asm))
   445 apply (rule_tac x = "{F. \<forall>G. F ok G --> F\<squnion>G \<in> X}" in exI, safe)
   446 apply (rule_tac [2] wx'_ex_prop)
   447 apply (drule_tac x = SKIP in spec)+
   448 apply auto 
   449 done
   450 
   451 
   452 text{* Propositions 7 to 11 are about this second definition of wx. 
   453    They are the same as the ones proved for the first definition of wx,
   454  by equivalence *}
   455    
   456 (* Proposition 12 *)
   457 (* Main result of the paper *)
   458 lemma guarantees_wx_eq: "(X guarantees Y) = wx(-X \<union> Y)"
   459 by (simp add: guar_def wx_equiv)
   460 
   461 
   462 (* Rules given in section 7 of Chandy and Sander's
   463     Reasoning About Program composition paper *)
   464 lemma stable_guarantees_Always:
   465      "Init F \<subseteq> A ==> F \<in> (stable A) guarantees (Always A)"
   466 apply (rule guaranteesI)
   467 apply (simp add: Join_commute)
   468 apply (rule stable_Join_Always1)
   469  apply (simp_all add: invariant_def Join_stable)
   470 done
   471 
   472 lemma constrains_guarantees_leadsTo:
   473      "F \<in> transient A ==> F \<in> (A co A \<union> B) guarantees (A leadsTo (B-A))"
   474 apply (rule guaranteesI)
   475 apply (rule leadsTo_Basis')
   476  apply (drule constrains_weaken_R)
   477   prefer 2 apply assumption
   478  apply blast
   479 apply (blast intro: Join_transient_I1)
   480 done
   481 
   482 end