--- a/src/HOL/UNITY/Guar.thy Mon Feb 03 11:45:05 2003 +0100
+++ b/src/HOL/UNITY/Guar.thy Tue Feb 04 18:12:40 2003 +0100
@@ -32,57 +32,57 @@
case, proving equivalence with Chandy and Sanders's n-ary definitions*)
ex_prop :: "'a program set => bool"
- "ex_prop X == \<forall>F G. F ok G -->F:X | G: X --> (F Join G) : X"
+ "ex_prop X == \<forall>F G. F ok G -->F \<in> X | G \<in> X --> (F Join G) \<in> X"
strict_ex_prop :: "'a program set => bool"
- "strict_ex_prop X == \<forall>F G. F ok G --> (F:X | G: X) = (F Join G : X)"
+ "strict_ex_prop X == \<forall>F G. F ok G --> (F \<in> X | G \<in> X) = (F Join G \<in> X)"
uv_prop :: "'a program set => bool"
- "uv_prop X == SKIP : X & (\<forall>F G. F ok G --> F:X & G: X --> (F Join G) : X)"
+ "uv_prop X == SKIP \<in> X & (\<forall>F G. F ok G --> F \<in> X & G \<in> X --> (F Join G) \<in> X)"
strict_uv_prop :: "'a program set => bool"
"strict_uv_prop X ==
- SKIP : X & (\<forall>F G. F ok G --> (F:X & G: X) = (F Join G : X))"
+ SKIP \<in> X & (\<forall>F G. F ok G --> (F \<in> X & G \<in> X) = (F Join G \<in> X))"
guar :: "['a program set, 'a program set] => 'a program set"
(infixl "guarantees" 55) (*higher than membership, lower than Co*)
- "X guarantees Y == {F. \<forall>G. F ok G --> F Join G : X --> F Join G : Y}"
+ "X guarantees Y == {F. \<forall>G. F ok G --> F Join G \<in> X --> F Join G \<in> Y}"
(* Weakest guarantees *)
wg :: "['a program, 'a program set] => 'a program set"
- "wg F Y == Union({X. F:X guarantees Y})"
+ "wg F Y == Union({X. F \<in> X guarantees Y})"
(* Weakest existential property stronger than X *)
wx :: "('a program) set => ('a program)set"
- "wx X == Union({Y. Y<=X & ex_prop Y})"
+ "wx X == Union({Y. Y \<subseteq> X & ex_prop Y})"
(*Ill-defined programs can arise through "Join"*)
welldef :: "'a program set"
- "welldef == {F. Init F ~= {}}"
+ "welldef == {F. Init F \<noteq> {}}"
refines :: "['a program, 'a program, 'a program set] => bool"
("(3_ refines _ wrt _)" [10,10,10] 10)
"G refines F wrt X ==
- \<forall>H. (F ok H & G ok H & F Join H : welldef Int X) -->
- (G Join H : welldef Int X)"
+ \<forall>H. (F ok H & G ok H & F Join H \<in> welldef \<inter> X) -->
+ (G Join H \<in> welldef \<inter> X)"
iso_refines :: "['a program, 'a program, 'a program set] => bool"
("(3_ iso'_refines _ wrt _)" [10,10,10] 10)
"G iso_refines F wrt X ==
- F : welldef Int X --> G : welldef Int X"
+ F \<in> welldef \<inter> X --> G \<in> welldef \<inter> X"
lemma OK_insert_iff:
"(OK (insert i I) F) =
- (if i:I then OK I F else OK I F & (F i ok JOIN I F))"
+ (if i \<in> I then OK I F else OK I F & (F i ok JOIN I F))"
by (auto intro: ok_sym simp add: OK_iff_ok)
(*** existential properties ***)
lemma ex1 [rule_format]:
"[| ex_prop X; finite GG |] ==>
- GG Int X ~= {}--> OK GG (%G. G) -->(JN G:GG. G) : X"
+ GG \<inter> X \<noteq> {}--> OK GG (%G. G) --> (\<Squnion>G \<in> GG. G) \<in> X"
apply (unfold ex_prop_def)
apply (erule finite_induct)
apply (auto simp add: OK_insert_iff Int_insert_left)
@@ -90,7 +90,7 @@
lemma ex2:
- "\<forall>GG. finite GG & GG Int X ~= {} --> OK GG (%G. G) -->(JN G:GG. G):X
+ "\<forall>GG. finite GG & GG \<inter> X \<noteq> {} --> OK GG (%G. G) -->(\<Squnion>G \<in> GG. G):X
==> ex_prop X"
apply (unfold ex_prop_def, clarify)
apply (drule_tac x = "{F,G}" in spec)
@@ -101,13 +101,13 @@
(*Chandy & Sanders take this as a definition*)
lemma ex_prop_finite:
"ex_prop X =
- (\<forall>GG. finite GG & GG Int X ~= {} & OK GG (%G. G)--> (JN G:GG. G) : X)"
+ (\<forall>GG. finite GG & GG \<inter> X \<noteq> {} & OK GG (%G. G)--> (\<Squnion>G \<in> GG. G) \<in> X)"
by (blast intro: ex1 ex2)
(*Their "equivalent definition" given at the end of section 3*)
lemma ex_prop_equiv:
- "ex_prop X = (\<forall>G. G:X = (\<forall>H. (G component_of H) --> H: X))"
+ "ex_prop X = (\<forall>G. G \<in> X = (\<forall>H. (G component_of H) --> H \<in> X))"
apply auto
apply (unfold ex_prop_def component_of_def, safe)
apply blast
@@ -120,14 +120,14 @@
(*** universal properties ***)
lemma uv1 [rule_format]:
"[| uv_prop X; finite GG |]
- ==> GG <= X & OK GG (%G. G) --> (JN G:GG. G) : X"
+ ==> GG \<subseteq> X & OK GG (%G. G) --> (\<Squnion>G \<in> GG. G) \<in> X"
apply (unfold uv_prop_def)
apply (erule finite_induct)
apply (auto simp add: Int_insert_left OK_insert_iff)
done
lemma uv2:
- "\<forall>GG. finite GG & GG <= X & OK GG (%G. G) --> (JN G:GG. G) : X
+ "\<forall>GG. finite GG & GG \<subseteq> X & OK GG (%G. G) --> (\<Squnion>G \<in> GG. G) \<in> X
==> uv_prop X"
apply (unfold uv_prop_def)
apply (rule conjI)
@@ -141,37 +141,37 @@
(*Chandy & Sanders take this as a definition*)
lemma uv_prop_finite:
"uv_prop X =
- (\<forall>GG. finite GG & GG <= X & OK GG (%G. G) --> (JN G:GG. G): X)"
+ (\<forall>GG. finite GG & GG \<subseteq> X & OK GG (%G. G) --> (\<Squnion>G \<in> GG. G): X)"
by (blast intro: uv1 uv2)
(*** guarantees ***)
lemma guaranteesI:
- "(!!G. [| F ok G; F Join G : X |] ==> F Join G : Y)
- ==> F : X guarantees Y"
+ "(!!G. [| F ok G; F Join G \<in> X |] ==> F Join G \<in> Y)
+ ==> F \<in> X guarantees Y"
by (simp add: guar_def component_def)
lemma guaranteesD:
- "[| F : X guarantees Y; F ok G; F Join G : X |]
- ==> F Join G : Y"
+ "[| F \<in> X guarantees Y; F ok G; F Join G \<in> X |]
+ ==> F Join G \<in> Y"
by (unfold guar_def component_def, blast)
(*This version of guaranteesD matches more easily in the conclusion
- The major premise can no longer be F<=H since we need to reason about G*)
+ The major premise can no longer be F \<subseteq> H since we need to reason about G*)
lemma component_guaranteesD:
- "[| F : X guarantees Y; F Join G = H; H : X; F ok G |]
- ==> H : Y"
+ "[| F \<in> X guarantees Y; F Join G = H; H \<in> X; F ok G |]
+ ==> H \<in> Y"
by (unfold guar_def, blast)
lemma guarantees_weaken:
- "[| F: X guarantees X'; Y <= X; X' <= Y' |] ==> F: Y guarantees Y'"
+ "[| F \<in> X guarantees X'; Y \<subseteq> X; X' \<subseteq> Y' |] ==> F \<in> Y guarantees Y'"
by (unfold guar_def, blast)
-lemma subset_imp_guarantees_UNIV: "X <= Y ==> X guarantees Y = UNIV"
+lemma subset_imp_guarantees_UNIV: "X \<subseteq> Y ==> X guarantees Y = UNIV"
by (unfold guar_def, blast)
(*Equivalent to subset_imp_guarantees_UNIV but more intuitive*)
-lemma subset_imp_guarantees: "X <= Y ==> F : X guarantees Y"
+lemma subset_imp_guarantees: "X \<subseteq> Y ==> F \<in> X guarantees Y"
by (unfold guar_def, blast)
(*Remark at end of section 4.1 *)
@@ -201,31 +201,31 @@
(** Distributive laws. Re-orient to perform miniscoping **)
lemma guarantees_UN_left:
- "(UN i:I. X i) guarantees Y = (INT i:I. X i guarantees Y)"
+ "(\<Union>i \<in> I. X i) guarantees Y = (\<Inter>i \<in> I. X i guarantees Y)"
by (unfold guar_def, blast)
lemma guarantees_Un_left:
- "(X Un Y) guarantees Z = (X guarantees Z) Int (Y guarantees Z)"
+ "(X \<union> Y) guarantees Z = (X guarantees Z) \<inter> (Y guarantees Z)"
by (unfold guar_def, blast)
lemma guarantees_INT_right:
- "X guarantees (INT i:I. Y i) = (INT i:I. X guarantees Y i)"
+ "X guarantees (\<Inter>i \<in> I. Y i) = (\<Inter>i \<in> I. X guarantees Y i)"
by (unfold guar_def, blast)
lemma guarantees_Int_right:
- "Z guarantees (X Int Y) = (Z guarantees X) Int (Z guarantees Y)"
+ "Z guarantees (X \<inter> Y) = (Z guarantees X) \<inter> (Z guarantees Y)"
by (unfold guar_def, blast)
lemma guarantees_Int_right_I:
- "[| F : Z guarantees X; F : Z guarantees Y |]
- ==> F : Z guarantees (X Int Y)"
+ "[| F \<in> Z guarantees X; F \<in> Z guarantees Y |]
+ ==> F \<in> Z guarantees (X \<inter> Y)"
by (simp add: guarantees_Int_right)
lemma guarantees_INT_right_iff:
- "(F : X guarantees (INTER I Y)) = (\<forall>i\<in>I. F : X guarantees (Y i))"
+ "(F \<in> X guarantees (INTER I Y)) = (\<forall>i\<in>I. F \<in> X guarantees (Y i))"
by (simp add: guarantees_INT_right)
-lemma shunting: "(X guarantees Y) = (UNIV guarantees (-X Un Y))"
+lemma shunting: "(X guarantees Y) = (UNIV guarantees (-X \<union> Y))"
by (unfold guar_def, blast)
lemma contrapositive: "(X guarantees Y) = -Y guarantees -X"
@@ -236,35 +236,35 @@
**)
lemma combining1:
- "[| F : V guarantees X; F : (X Int Y) guarantees Z |]
- ==> F : (V Int Y) guarantees Z"
+ "[| F \<in> V guarantees X; F \<in> (X \<inter> Y) guarantees Z |]
+ ==> F \<in> (V \<inter> Y) guarantees Z"
by (unfold guar_def, blast)
lemma combining2:
- "[| F : V guarantees (X Un Y); F : Y guarantees Z |]
- ==> F : V guarantees (X Un Z)"
+ "[| F \<in> V guarantees (X \<union> Y); F \<in> Y guarantees Z |]
+ ==> F \<in> V guarantees (X \<union> Z)"
by (unfold guar_def, blast)
(** The following two follow Chandy-Sanders, but the use of object-quantifiers
does not suit Isabelle... **)
-(*Premise should be (!!i. i: I ==> F: X guarantees Y i) *)
+(*Premise should be (!!i. i \<in> I ==> F \<in> X guarantees Y i) *)
lemma all_guarantees:
- "\<forall>i\<in>I. F : X guarantees (Y i) ==> F : X guarantees (INT i:I. Y i)"
+ "\<forall>i\<in>I. F \<in> X guarantees (Y i) ==> F \<in> X guarantees (\<Inter>i \<in> I. Y i)"
by (unfold guar_def, blast)
-(*Premises should be [| F: X guarantees Y i; i: I |] *)
+(*Premises should be [| F \<in> X guarantees Y i; i \<in> I |] *)
lemma ex_guarantees:
- "\<exists>i\<in>I. F : X guarantees (Y i) ==> F : X guarantees (UN i:I. Y i)"
+ "\<exists>i\<in>I. F \<in> X guarantees (Y i) ==> F \<in> X guarantees (\<Union>i \<in> I. Y i)"
by (unfold guar_def, blast)
(*** Additional guarantees laws, by lcp ***)
lemma guarantees_Join_Int:
- "[| F: U guarantees V; G: X guarantees Y; F ok G |]
- ==> F Join G: (U Int X) guarantees (V Int Y)"
+ "[| F \<in> U guarantees V; G \<in> X guarantees Y; F ok G |]
+ ==> F Join G \<in> (U \<inter> X) guarantees (V \<inter> Y)"
apply (unfold guar_def)
apply (simp (no_asm))
apply safe
@@ -275,8 +275,8 @@
done
lemma guarantees_Join_Un:
- "[| F: U guarantees V; G: X guarantees Y; F ok G |]
- ==> F Join G: (U Un X) guarantees (V Un Y)"
+ "[| F \<in> U guarantees V; G \<in> X guarantees Y; F ok G |]
+ ==> F Join G \<in> (U \<union> X) guarantees (V \<union> Y)"
apply (unfold guar_def)
apply (simp (no_asm))
apply safe
@@ -287,8 +287,8 @@
done
lemma guarantees_JN_INT:
- "[| \<forall>i\<in>I. F i : X i guarantees Y i; OK I F |]
- ==> (JOIN I F) : (INTER I X) guarantees (INTER I Y)"
+ "[| \<forall>i\<in>I. F i \<in> X i guarantees Y i; OK I F |]
+ ==> (JOIN I F) \<in> (INTER I X) guarantees (INTER I Y)"
apply (unfold guar_def, auto)
apply (drule bspec, assumption)
apply (rename_tac "i")
@@ -298,8 +298,8 @@
done
lemma guarantees_JN_UN:
- "[| \<forall>i\<in>I. F i : X i guarantees Y i; OK I F |]
- ==> (JOIN I F) : (UNION I X) guarantees (UNION I Y)"
+ "[| \<forall>i\<in>I. F i \<in> X i guarantees Y i; OK I F |]
+ ==> (JOIN I F) \<in> (UNION I X) guarantees (UNION I Y)"
apply (unfold guar_def, auto)
apply (drule bspec, assumption)
apply (rename_tac "i")
@@ -312,7 +312,7 @@
(*** guarantees laws for breaking down the program, by lcp ***)
lemma guarantees_Join_I1:
- "[| F: X guarantees Y; F ok G |] ==> F Join G: X guarantees Y"
+ "[| F \<in> X guarantees Y; F ok G |] ==> F Join G \<in> X guarantees Y"
apply (unfold guar_def)
apply (simp (no_asm))
apply safe
@@ -320,14 +320,14 @@
done
lemma guarantees_Join_I2:
- "[| G: X guarantees Y; F ok G |] ==> F Join G: X guarantees Y"
+ "[| G \<in> X guarantees Y; F ok G |] ==> F Join G \<in> X guarantees Y"
apply (simp add: Join_commute [of _ G] ok_commute [of _ G])
apply (blast intro: guarantees_Join_I1)
done
lemma guarantees_JN_I:
- "[| i : I; F i: X guarantees Y; OK I F |]
- ==> (JN i:I. (F i)) : X guarantees Y"
+ "[| i \<in> I; F i \<in> X guarantees Y; OK I F |]
+ ==> (\<Squnion>i \<in> I. (F i)) \<in> X guarantees Y"
apply (unfold guar_def, clarify)
apply (drule_tac x = "JOIN (I-{i}) F Join G" in spec)
apply (auto intro: OK_imp_ok simp add: JN_Join_diff JN_Join_diff Join_assoc [symmetric])
@@ -336,10 +336,10 @@
(*** well-definedness ***)
-lemma Join_welldef_D1: "F Join G: welldef ==> F: welldef"
+lemma Join_welldef_D1: "F Join G \<in> welldef ==> F \<in> welldef"
by (unfold welldef_def, auto)
-lemma Join_welldef_D2: "F Join G: welldef ==> G: welldef"
+lemma Join_welldef_D2: "F Join G \<in> welldef ==> G \<in> welldef"
by (unfold welldef_def, auto)
(*** refinement ***)
@@ -357,14 +357,14 @@
lemma strict_ex_refine_lemma:
"strict_ex_prop X
- ==> (\<forall>H. F ok H & G ok H & F Join H : X --> G Join H : X)
- = (F:X --> G:X)"
+ ==> (\<forall>H. F ok H & G ok H & F Join H \<in> X --> G Join H \<in> X)
+ = (F \<in> X --> G \<in> X)"
by (unfold strict_ex_prop_def, auto)
lemma strict_ex_refine_lemma_v:
"strict_ex_prop X
- ==> (\<forall>H. F ok H & G ok H & F Join H : welldef & F Join H : X --> G Join H : X) =
- (F: welldef Int X --> G:X)"
+ ==> (\<forall>H. F ok H & G ok H & F Join H \<in> welldef & F Join H \<in> X --> G Join H \<in> X) =
+ (F \<in> welldef \<inter> X --> G \<in> X)"
apply (unfold strict_ex_prop_def, safe)
apply (erule_tac x = SKIP and P = "%H. ?PP H --> ?RR H" in allE)
apply (auto dest: Join_welldef_D1 Join_welldef_D2)
@@ -372,7 +372,7 @@
lemma ex_refinement_thm:
"[| strict_ex_prop X;
- \<forall>H. F ok H & G ok H & F Join H : welldef Int X --> G Join H : welldef |]
+ \<forall>H. F ok H & G ok H & F Join H \<in> welldef \<inter> X --> G Join H \<in> welldef |]
==> (G refines F wrt X) = (G iso_refines F wrt X)"
apply (rule_tac x = SKIP in allE, assumption)
apply (simp add: refines_def iso_refines_def strict_ex_refine_lemma_v)
@@ -381,13 +381,13 @@
lemma strict_uv_refine_lemma:
"strict_uv_prop X ==>
- (\<forall>H. F ok H & G ok H & F Join H : X --> G Join H : X) = (F:X --> G:X)"
+ (\<forall>H. F ok H & G ok H & F Join H \<in> X --> G Join H \<in> X) = (F \<in> X --> G \<in> X)"
by (unfold strict_uv_prop_def, blast)
lemma strict_uv_refine_lemma_v:
"strict_uv_prop X
- ==> (\<forall>H. F ok H & G ok H & F Join H : welldef & F Join H : X --> G Join H : X) =
- (F: welldef Int X --> G:X)"
+ ==> (\<forall>H. F ok H & G ok H & F Join H \<in> welldef & F Join H \<in> X --> G Join H \<in> X) =
+ (F \<in> welldef \<inter> X --> G \<in> X)"
apply (unfold strict_uv_prop_def, safe)
apply (erule_tac x = SKIP and P = "%H. ?PP H --> ?RR H" in allE)
apply (auto dest: Join_welldef_D1 Join_welldef_D2)
@@ -395,8 +395,8 @@
lemma uv_refinement_thm:
"[| strict_uv_prop X;
- \<forall>H. F ok H & G ok H & F Join H : welldef Int X -->
- G Join H : welldef |]
+ \<forall>H. F ok H & G ok H & F Join H \<in> welldef \<inter> X -->
+ G Join H \<in> welldef |]
==> (G refines F wrt X) = (G iso_refines F wrt X)"
apply (rule_tac x = SKIP in allE, assumption)
apply (simp add: refines_def iso_refines_def strict_uv_refine_lemma_v)
@@ -404,17 +404,17 @@
(* Added by Sidi Ehmety from Chandy & Sander, section 6 *)
lemma guarantees_equiv:
- "(F:X guarantees Y) = (\<forall>H. H:X \<longrightarrow> (F component_of H \<longrightarrow> H:Y))"
+ "(F \<in> X guarantees Y) = (\<forall>H. H \<in> X \<longrightarrow> (F component_of H \<longrightarrow> H \<in> Y))"
by (unfold guar_def component_of_def, auto)
-lemma wg_weakest: "!!X. F:(X guarantees Y) ==> X <= (wg F Y)"
+lemma wg_weakest: "!!X. F:(X guarantees Y) ==> X \<subseteq> (wg F Y)"
by (unfold wg_def, auto)
lemma wg_guarantees: "F:((wg F Y) guarantees Y)"
by (unfold wg_def guar_def, blast)
lemma wg_equiv:
- "(H: wg F X) = (F component_of H --> H:X)"
+ "(H \<in> wg F X) = (F component_of H --> H \<in> X)"
apply (unfold wg_def)
apply (simp (no_asm) add: guarantees_equiv)
apply (rule iffI)
@@ -423,21 +423,21 @@
done
-lemma component_of_wg: "F component_of H ==> (H:wg F X) = (H:X)"
+lemma component_of_wg: "F component_of H ==> (H \<in> wg F X) = (H \<in> X)"
by (simp add: wg_equiv)
lemma wg_finite:
- "\<forall>FF. finite FF & FF Int X ~= {} --> OK FF (%F. F)
- --> (\<forall>F\<in>FF. ((JN F:FF. F): wg F X) = ((JN F:FF. F):X))"
+ "\<forall>FF. finite FF & FF \<inter> X \<noteq> {} --> OK FF (%F. F)
+ --> (\<forall>F\<in>FF. ((\<Squnion>F \<in> FF. F): wg F X) = ((\<Squnion>F \<in> FF. F):X))"
apply clarify
-apply (subgoal_tac "F component_of (JN F:FF. F) ")
+apply (subgoal_tac "F component_of (\<Squnion>F \<in> FF. F) ")
apply (drule_tac X = X in component_of_wg, simp)
apply (simp add: component_of_def)
-apply (rule_tac x = "JN F: (FF-{F}) . F" in exI)
+apply (rule_tac x = "\<Squnion>F \<in> (FF-{F}) . F" in exI)
apply (auto intro: JN_Join_diff dest: ok_sym simp add: OK_iff_ok)
done
-lemma wg_ex_prop: "ex_prop X ==> (F:X) = (\<forall>H. H : wg F X)"
+lemma wg_ex_prop: "ex_prop X ==> (F \<in> X) = (\<forall>H. H \<in> wg F X)"
apply (simp (no_asm_use) add: ex_prop_equiv wg_equiv)
apply blast
done
@@ -455,11 +455,11 @@
apply auto
done
-lemma wx_weakest: "\<forall>Z. Z<= X --> ex_prop Z --> Z <= wx X"
+lemma wx_weakest: "\<forall>Z. Z<= X --> ex_prop Z --> Z \<subseteq> wx X"
by (unfold wx_def, auto)
(* Proposition 6 *)
-lemma wx'_ex_prop: "ex_prop({F. \<forall>G. F ok G --> F Join G:X})"
+lemma wx'_ex_prop: "ex_prop({F. \<forall>G. F ok G --> F Join G \<in> X})"
apply (unfold ex_prop_def, safe)
apply (drule_tac x = "G Join Ga" in spec)
apply (force simp add: ok_Join_iff1 Join_assoc)
@@ -483,7 +483,7 @@
apply (drule_tac x = G in spec)
apply (frule_tac c = "x Join G" in subsetD, safe)
apply (simp (no_asm))
-apply (rule_tac x = "{F. \<forall>G. F ok G --> F Join G:X}" in exI, safe)
+apply (rule_tac x = "{F. \<forall>G. F ok G --> F Join G \<in> X}" in exI, safe)
apply (rule_tac [2] wx'_ex_prop)
apply (rotate_tac 1)
apply (drule_tac x = SKIP in spec, auto)
@@ -496,7 +496,7 @@
(* Proposition 12 *)
(* Main result of the paper *)
lemma guarantees_wx_eq:
- "(X guarantees Y) = wx(-X Un Y)"
+ "(X guarantees Y) = wx(-X \<union> Y)"
apply (unfold guar_def)
apply (simp (no_asm) add: wx_equiv)
done
@@ -511,7 +511,7 @@
Reasoning About Program composition paper *)
lemma stable_guarantees_Always:
- "Init F <= A ==> F:(stable A) guarantees (Always A)"
+ "Init F \<subseteq> A ==> F:(stable A) guarantees (Always A)"
apply (rule guaranteesI)
apply (simp (no_asm) add: Join_commute)
apply (rule stable_Join_Always1)
@@ -519,7 +519,7 @@
done
(* To be moved to WFair.ML *)
-lemma leadsTo_Basis': "[| F:A co A Un B; F:transient A |] ==> F:A leadsTo B"
+lemma leadsTo_Basis': "[| F \<in> A co A \<union> B; F \<in> transient A |] ==> F \<in> A leadsTo B"
apply (drule_tac B = "A-B" in constrains_weaken_L)
apply (drule_tac [2] B = "A-B" in transient_strengthen)
apply (rule_tac [3] ensuresI [THEN leadsTo_Basis])
@@ -529,7 +529,7 @@
lemma constrains_guarantees_leadsTo:
- "F : transient A ==> F: (A co A Un B) guarantees (A leadsTo (B-A))"
+ "F \<in> transient A ==> F \<in> (A co A \<union> B) guarantees (A leadsTo (B-A))"
apply (rule guaranteesI)
apply (rule leadsTo_Basis')
apply (drule constrains_weaken_R)