src/HOL/UNITY/Guar.thy
author paulson
Tue Feb 01 18:01:57 2005 +0100 (2005-02-01)
changeset 15481 fc075ae929e4
parent 14112 95d51043d2a3
child 16417 9bc16273c2d4
permissions -rw-r--r--
the new subst tactic, by Lucas Dixon
     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 text{*Existential and Universal properties.  I formalize the two-program
    30       case, proving equivalence with Chandy and Sanders's n-ary definitions*}
    31 
    32 constdefs
    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\<squnion>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\<squnion>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\<squnion>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\<squnion>G \<in> X))"
    46 
    47 
    48 text{*Guarantees properties*}
    49 
    50 constdefs
    51 
    52   guar :: "['a program set, 'a program set] => 'a program set"
    53           (infixl "guarantees" 55)  (*higher than membership, lower than Co*)
    54    "X guarantees Y == {F. \<forall>G. F ok G --> F\<squnion>G \<in> X --> F\<squnion>G \<in> Y}"
    55   
    56 
    57   (* Weakest guarantees *)
    58    wg :: "['a program, 'a program set] =>  'a program set"
    59   "wg F Y == Union({X. F \<in> X guarantees Y})"
    60 
    61    (* Weakest existential property stronger than X *)
    62    wx :: "('a program) set => ('a program)set"
    63    "wx X == Union({Y. Y \<subseteq> X & ex_prop Y})"
    64   
    65   (*Ill-defined programs can arise through "Join"*)
    66   welldef :: "'a program set"
    67   "welldef == {F. Init F \<noteq> {}}"
    68   
    69   refines :: "['a program, 'a program, 'a program set] => bool"
    70 			("(3_ refines _ wrt _)" [10,10,10] 10)
    71   "G refines F wrt X ==
    72      \<forall>H. (F ok H & G ok H & F\<squnion>H \<in> welldef \<inter> X) --> 
    73          (G\<squnion>H \<in> welldef \<inter> X)"
    74 
    75   iso_refines :: "['a program, 'a program, 'a program set] => bool"
    76                               ("(3_ iso'_refines _ wrt _)" [10,10,10] 10)
    77   "G iso_refines F wrt X ==
    78    F \<in> welldef \<inter> X --> G \<in> welldef \<inter> X"
    79 
    80 
    81 lemma OK_insert_iff:
    82      "(OK (insert i I) F) = 
    83       (if i \<in> I then OK I F else OK I F & (F i ok JOIN I F))"
    84 by (auto intro: ok_sym simp add: OK_iff_ok)
    85 
    86 
    87 subsection{*Existential Properties*}
    88 
    89 lemma ex1 [rule_format]: 
    90  "[| ex_prop X; finite GG |] ==>  
    91      GG \<inter> X \<noteq> {}--> OK GG (%G. G) --> (\<Squnion>G \<in> GG. G) \<in> X"
    92 apply (unfold ex_prop_def)
    93 apply (erule finite_induct)
    94 apply (auto simp add: OK_insert_iff Int_insert_left)
    95 done
    96 
    97 
    98 lemma ex2: 
    99      "\<forall>GG. finite GG & GG \<inter> X \<noteq> {} --> OK GG (%G. G) -->(\<Squnion>G \<in> GG. G):X 
   100       ==> ex_prop X"
   101 apply (unfold ex_prop_def, clarify)
   102 apply (drule_tac x = "{F,G}" in spec)
   103 apply (auto dest: ok_sym simp add: OK_iff_ok)
   104 done
   105 
   106 
   107 (*Chandy & Sanders take this as a definition*)
   108 lemma ex_prop_finite:
   109      "ex_prop X = 
   110       (\<forall>GG. finite GG & GG \<inter> X \<noteq> {} & OK GG (%G. G)--> (\<Squnion>G \<in> GG. G) \<in> X)"
   111 by (blast intro: ex1 ex2)
   112 
   113 
   114 (*Their "equivalent definition" given at the end of section 3*)
   115 lemma ex_prop_equiv: 
   116      "ex_prop X = (\<forall>G. G \<in> X = (\<forall>H. (G component_of H) --> H \<in> X))"
   117 apply auto
   118 apply (unfold ex_prop_def component_of_def, safe, blast, blast) 
   119 apply (subst Join_commute) 
   120 apply (drule ok_sym, blast) 
   121 done
   122 
   123 
   124 subsection{*Universal Properties*}
   125 
   126 lemma uv1 [rule_format]: 
   127      "[| uv_prop X; finite GG |] 
   128       ==> GG \<subseteq> X & OK GG (%G. G) --> (\<Squnion>G \<in> GG. G) \<in> X"
   129 apply (unfold uv_prop_def)
   130 apply (erule finite_induct)
   131 apply (auto simp add: Int_insert_left OK_insert_iff)
   132 done
   133 
   134 lemma uv2: 
   135      "\<forall>GG. finite GG & GG \<subseteq> X & OK GG (%G. G) --> (\<Squnion>G \<in> GG. G) \<in> X  
   136       ==> uv_prop X"
   137 apply (unfold uv_prop_def)
   138 apply (rule conjI)
   139  apply (drule_tac x = "{}" in spec)
   140  prefer 2
   141  apply clarify 
   142  apply (drule_tac x = "{F,G}" in spec)
   143 apply (auto dest: ok_sym simp add: OK_iff_ok)
   144 done
   145 
   146 (*Chandy & Sanders take this as a definition*)
   147 lemma uv_prop_finite:
   148      "uv_prop X = 
   149       (\<forall>GG. finite GG & GG \<subseteq> X & OK GG (%G. G) --> (\<Squnion>G \<in> GG. G): X)"
   150 by (blast intro: uv1 uv2)
   151 
   152 subsection{*Guarantees*}
   153 
   154 lemma guaranteesI:
   155      "(!!G. [| F ok G; F\<squnion>G \<in> X |] ==> F\<squnion>G \<in> Y) ==> F \<in> X guarantees Y"
   156 by (simp add: guar_def component_def)
   157 
   158 lemma guaranteesD: 
   159      "[| F \<in> X guarantees Y;  F ok G;  F\<squnion>G \<in> X |] ==> F\<squnion>G \<in> Y"
   160 by (unfold guar_def component_def, blast)
   161 
   162 (*This version of guaranteesD matches more easily in the conclusion
   163   The major premise can no longer be  F \<subseteq> H since we need to reason about G*)
   164 lemma component_guaranteesD: 
   165      "[| F \<in> X guarantees Y;  F\<squnion>G = H;  H \<in> X;  F ok G |] ==> H \<in> Y"
   166 by (unfold guar_def, blast)
   167 
   168 lemma guarantees_weaken: 
   169      "[| F \<in> X guarantees X'; Y \<subseteq> X; X' \<subseteq> Y' |] ==> F \<in> Y guarantees Y'"
   170 by (unfold guar_def, blast)
   171 
   172 lemma subset_imp_guarantees_UNIV: "X \<subseteq> Y ==> X guarantees Y = UNIV"
   173 by (unfold guar_def, blast)
   174 
   175 (*Equivalent to subset_imp_guarantees_UNIV but more intuitive*)
   176 lemma subset_imp_guarantees: "X \<subseteq> Y ==> F \<in> X guarantees Y"
   177 by (unfold guar_def, blast)
   178 
   179 (*Remark at end of section 4.1 *)
   180 
   181 lemma ex_prop_imp: "ex_prop Y ==> (Y = UNIV guarantees Y)"
   182 apply (simp (no_asm_use) add: guar_def ex_prop_equiv)
   183 apply safe
   184  apply (drule_tac x = x in spec)
   185  apply (drule_tac [2] x = x in spec)
   186  apply (drule_tac [2] sym)
   187 apply (auto simp add: component_of_def)
   188 done
   189 
   190 lemma guarantees_imp: "(Y = UNIV guarantees Y) ==> ex_prop(Y)"
   191 by (auto simp add: guar_def ex_prop_equiv component_of_def dest: sym)
   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 subsection{*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 by (unfold guar_def, blast)
   241 
   242 lemma combining2: 
   243     "[| F \<in> V guarantees (X \<union> Y);  F \<in> Y guarantees Z |] 
   244      ==> F \<in> V guarantees (X \<union> Z)"
   245 by (unfold guar_def, blast)
   246 
   247 (** The following two follow Chandy-Sanders, but the use of object-quantifiers
   248     does not suit Isabelle... **)
   249 
   250 (*Premise should be (!!i. i \<in> I ==> F \<in> X guarantees Y i) *)
   251 lemma all_guarantees: 
   252      "\<forall>i\<in>I. F \<in> X guarantees (Y i) ==> F \<in> X guarantees (\<Inter>i \<in> I. Y i)"
   253 by (unfold guar_def, blast)
   254 
   255 (*Premises should be [| F \<in> X guarantees Y i; i \<in> I |] *)
   256 lemma ex_guarantees: 
   257      "\<exists>i\<in>I. F \<in> X guarantees (Y i) ==> F \<in> X guarantees (\<Union>i \<in> I. Y i)"
   258 by (unfold guar_def, blast)
   259 
   260 
   261 subsection{*Guarantees: Additional Laws (by lcp)*}
   262 
   263 lemma guarantees_Join_Int: 
   264     "[| F \<in> U guarantees V;  G \<in> X guarantees Y; F ok G |]  
   265      ==> F\<squnion>G \<in> (U \<inter> X) guarantees (V \<inter> Y)"
   266 apply (simp add: guar_def, safe)
   267  apply (simp add: Join_assoc)
   268 apply (subgoal_tac "F\<squnion>G\<squnion>Ga = G\<squnion>(F\<squnion>Ga) ")
   269  apply (simp add: ok_commute)
   270 apply (simp add: Join_ac)
   271 done
   272 
   273 lemma guarantees_Join_Un: 
   274     "[| F \<in> U guarantees V;  G \<in> X guarantees Y; F ok G |]   
   275      ==> F\<squnion>G \<in> (U \<union> X) guarantees (V \<union> Y)"
   276 apply (simp add: guar_def, safe)
   277  apply (simp add: Join_assoc)
   278 apply (subgoal_tac "F\<squnion>G\<squnion>Ga = G\<squnion>(F\<squnion>Ga) ")
   279  apply (simp add: ok_commute)
   280 apply (simp add: Join_ac)
   281 done
   282 
   283 lemma guarantees_JN_INT: 
   284      "[| \<forall>i\<in>I. F i \<in> X i guarantees Y i;  OK I F |]  
   285       ==> (JOIN I F) \<in> (INTER I X) guarantees (INTER 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 lemma guarantees_JN_UN: 
   295     "[| \<forall>i\<in>I. F i \<in> X i guarantees Y i;  OK I F |]  
   296      ==> (JOIN I F) \<in> (UNION I X) guarantees (UNION I Y)"
   297 apply (unfold guar_def, auto)
   298 apply (drule bspec, assumption)
   299 apply (rename_tac "i")
   300 apply (drule_tac x = "JOIN (I-{i}) F\<squnion>G" in spec)
   301 apply (auto intro: OK_imp_ok
   302             simp add: Join_assoc [symmetric] JN_Join_diff JN_absorb)
   303 done
   304 
   305 
   306 subsection{*Guarantees Laws for Breaking Down the Program (by lcp)*}
   307 
   308 lemma guarantees_Join_I1: 
   309      "[| F \<in> X guarantees Y;  F ok G |] ==> F\<squnion>G \<in> X guarantees Y"
   310 by (simp add: guar_def Join_assoc)
   311 
   312 lemma guarantees_Join_I2:         
   313      "[| G \<in> X guarantees Y;  F ok G |] ==> F\<squnion>G \<in> X guarantees Y"
   314 apply (simp add: Join_commute [of _ G] ok_commute [of _ G])
   315 apply (blast intro: guarantees_Join_I1)
   316 done
   317 
   318 lemma guarantees_JN_I: 
   319      "[| i \<in> I;  F i \<in> X guarantees Y;  OK I F |]  
   320       ==> (\<Squnion>i \<in> I. (F i)) \<in> X guarantees Y"
   321 apply (unfold guar_def, clarify)
   322 apply (drule_tac x = "JOIN (I-{i}) F\<squnion>G" in spec)
   323 apply (auto intro: OK_imp_ok 
   324             simp add: JN_Join_diff JN_Join_diff Join_assoc [symmetric])
   325 done
   326 
   327 
   328 (*** well-definedness ***)
   329 
   330 lemma Join_welldef_D1: "F\<squnion>G \<in> welldef ==> F \<in> welldef"
   331 by (unfold welldef_def, auto)
   332 
   333 lemma Join_welldef_D2: "F\<squnion>G \<in> welldef ==> G \<in> welldef"
   334 by (unfold welldef_def, auto)
   335 
   336 (*** refinement ***)
   337 
   338 lemma refines_refl: "F refines F wrt X"
   339 by (unfold refines_def, blast)
   340 
   341 (*We'd like transitivity, but how do we get it?*)
   342 lemma refines_trans:
   343      "[| H refines G wrt X;  G refines F wrt X |] ==> H refines F wrt X"
   344 apply (simp add: refines_def) 
   345 oops
   346 
   347 
   348 lemma strict_ex_refine_lemma: 
   349      "strict_ex_prop X  
   350       ==> (\<forall>H. F ok H & G ok H & F\<squnion>H \<in> X --> G\<squnion>H \<in> X)  
   351               = (F \<in> X --> G \<in> X)"
   352 by (unfold strict_ex_prop_def, auto)
   353 
   354 lemma strict_ex_refine_lemma_v: 
   355      "strict_ex_prop X  
   356       ==> (\<forall>H. F ok H & G ok H & F\<squnion>H \<in> welldef & F\<squnion>H \<in> X --> G\<squnion>H \<in> X) =  
   357           (F \<in> welldef \<inter> X --> G \<in> X)"
   358 apply (unfold strict_ex_prop_def, safe)
   359 apply (erule_tac x = SKIP and P = "%H. ?PP H --> ?RR H" in allE)
   360 apply (auto dest: Join_welldef_D1 Join_welldef_D2)
   361 done
   362 
   363 lemma ex_refinement_thm:
   364      "[| strict_ex_prop X;   
   365          \<forall>H. F ok H & G ok H & F\<squnion>H \<in> welldef \<inter> X --> G\<squnion>H \<in> welldef |]  
   366       ==> (G refines F wrt X) = (G iso_refines F wrt X)"
   367 apply (rule_tac x = SKIP in allE, assumption)
   368 apply (simp add: refines_def iso_refines_def strict_ex_refine_lemma_v)
   369 done
   370 
   371 
   372 lemma strict_uv_refine_lemma: 
   373      "strict_uv_prop X ==> 
   374       (\<forall>H. F ok H & G ok H & F\<squnion>H \<in> X --> G\<squnion>H \<in> X) = (F \<in> X --> G \<in> X)"
   375 by (unfold strict_uv_prop_def, blast)
   376 
   377 lemma strict_uv_refine_lemma_v: 
   378      "strict_uv_prop X  
   379       ==> (\<forall>H. F ok H & G ok H & F\<squnion>H \<in> welldef & F\<squnion>H \<in> X --> G\<squnion>H \<in> X) =  
   380           (F \<in> welldef \<inter> X --> G \<in> X)"
   381 apply (unfold strict_uv_prop_def, safe)
   382 apply (erule_tac x = SKIP and P = "%H. ?PP H --> ?RR H" in allE)
   383 apply (auto dest: Join_welldef_D1 Join_welldef_D2)
   384 done
   385 
   386 lemma uv_refinement_thm:
   387      "[| strict_uv_prop X;   
   388          \<forall>H. F ok H & G ok H & F\<squnion>H \<in> welldef \<inter> X --> 
   389              G\<squnion>H \<in> welldef |]  
   390       ==> (G refines F wrt X) = (G iso_refines F wrt X)"
   391 apply (rule_tac x = SKIP in allE, assumption)
   392 apply (simp add: refines_def iso_refines_def strict_uv_refine_lemma_v)
   393 done
   394 
   395 (* Added by Sidi Ehmety from Chandy & Sander, section 6 *)
   396 lemma guarantees_equiv: 
   397     "(F \<in> X guarantees Y) = (\<forall>H. H \<in> X \<longrightarrow> (F component_of H \<longrightarrow> H \<in> Y))"
   398 by (unfold guar_def component_of_def, auto)
   399 
   400 lemma wg_weakest: "!!X. F\<in> (X guarantees Y) ==> X \<subseteq> (wg F Y)"
   401 by (unfold wg_def, auto)
   402 
   403 lemma wg_guarantees: "F\<in> ((wg F Y) guarantees Y)"
   404 by (unfold wg_def guar_def, blast)
   405 
   406 lemma wg_equiv: "(H \<in> wg F X) = (F component_of H --> H \<in> X)"
   407 by (simp add: guarantees_equiv wg_def, blast)
   408 
   409 lemma component_of_wg: "F component_of H ==> (H \<in> wg F X) = (H \<in> X)"
   410 by (simp add: wg_equiv)
   411 
   412 lemma wg_finite: 
   413     "\<forall>FF. finite FF & FF \<inter> X \<noteq> {} --> OK FF (%F. F)  
   414           --> (\<forall>F\<in>FF. ((\<Squnion>F \<in> FF. F): wg F X) = ((\<Squnion>F \<in> FF. F):X))"
   415 apply clarify
   416 apply (subgoal_tac "F component_of (\<Squnion>F \<in> FF. F) ")
   417 apply (drule_tac X = X in component_of_wg, simp)
   418 apply (simp add: component_of_def)
   419 apply (rule_tac x = "\<Squnion>F \<in> (FF-{F}) . F" in exI)
   420 apply (auto intro: JN_Join_diff dest: ok_sym simp add: OK_iff_ok)
   421 done
   422 
   423 lemma wg_ex_prop: "ex_prop X ==> (F \<in> X) = (\<forall>H. H \<in> wg F X)"
   424 apply (simp (no_asm_use) add: ex_prop_equiv wg_equiv)
   425 apply blast
   426 done
   427 
   428 (** From Charpentier and Chandy "Theorems About Composition" **)
   429 (* Proposition 2 *)
   430 lemma wx_subset: "(wx X)<=X"
   431 by (unfold wx_def, auto)
   432 
   433 lemma wx_ex_prop: "ex_prop (wx X)"
   434 apply (simp add: wx_def ex_prop_equiv, safe, blast)
   435 apply force 
   436 done
   437 
   438 lemma wx_weakest: "\<forall>Z. Z<= X --> ex_prop Z --> Z \<subseteq> wx X"
   439 by (auto simp add: wx_def)
   440 
   441 (* Proposition 6 *)
   442 lemma wx'_ex_prop: "ex_prop({F. \<forall>G. F ok G --> F\<squnion>G \<in> X})"
   443 apply (unfold ex_prop_def, safe)
   444  apply (drule_tac x = "G\<squnion>Ga" in spec)
   445  apply (force simp add: ok_Join_iff1 Join_assoc)
   446 apply (drule_tac x = "F\<squnion>Ga" in spec)
   447 apply (simp add: ok_Join_iff1 ok_commute  Join_ac) 
   448 done
   449 
   450 text{* Equivalence with the other definition of wx *}
   451 
   452 lemma wx_equiv: "wx X = {F. \<forall>G. F ok G --> (F\<squnion>G) \<in> X}"
   453 apply (unfold wx_def, safe)
   454  apply (simp add: ex_prop_def, blast) 
   455 apply (simp (no_asm))
   456 apply (rule_tac x = "{F. \<forall>G. F ok G --> F\<squnion>G \<in> X}" in exI, safe)
   457 apply (rule_tac [2] wx'_ex_prop)
   458 apply (drule_tac x = SKIP in spec)+
   459 apply auto 
   460 done
   461 
   462 
   463 text{* Propositions 7 to 11 are about this second definition of wx. 
   464    They are the same as the ones proved for the first definition of wx,
   465  by equivalence *}
   466    
   467 (* Proposition 12 *)
   468 (* Main result of the paper *)
   469 lemma guarantees_wx_eq: "(X guarantees Y) = wx(-X \<union> Y)"
   470 by (simp add: guar_def wx_equiv)
   471 
   472 
   473 (* Rules given in section 7 of Chandy and Sander's
   474     Reasoning About Program composition paper *)
   475 lemma stable_guarantees_Always:
   476      "Init F \<subseteq> A ==> F \<in> (stable A) guarantees (Always A)"
   477 apply (rule guaranteesI)
   478 apply (simp add: Join_commute)
   479 apply (rule stable_Join_Always1)
   480  apply (simp_all add: invariant_def Join_stable)
   481 done
   482 
   483 lemma constrains_guarantees_leadsTo:
   484      "F \<in> transient A ==> F \<in> (A co A \<union> B) guarantees (A leadsTo (B-A))"
   485 apply (rule guaranteesI)
   486 apply (rule leadsTo_Basis')
   487  apply (drule constrains_weaken_R)
   488   prefer 2 apply assumption
   489  apply blast
   490 apply (blast intro: Join_transient_I1)
   491 done
   492 
   493 end