src/HOL/UNITY/Guar.thy
 changeset 13805 3786b2fd6808 parent 13798 4c1a53627500 child 13812 91713a1915ee
```     1.1 --- a/src/HOL/UNITY/Guar.thy	Mon Feb 03 11:45:05 2003 +0100
1.2 +++ b/src/HOL/UNITY/Guar.thy	Tue Feb 04 18:12:40 2003 +0100
1.3 @@ -32,57 +32,57 @@
1.4      case, proving equivalence with Chandy and Sanders's n-ary definitions*)
1.5
1.6    ex_prop  :: "'a program set => bool"
1.7 -   "ex_prop X == \<forall>F G. F ok G -->F:X | G: X --> (F Join G) : X"
1.8 +   "ex_prop X == \<forall>F G. F ok G -->F \<in> X | G \<in> X --> (F Join G) \<in> X"
1.9
1.10    strict_ex_prop  :: "'a program set => bool"
1.11 -   "strict_ex_prop X == \<forall>F G.  F ok G --> (F:X | G: X) = (F Join G : X)"
1.12 +   "strict_ex_prop X == \<forall>F G.  F ok G --> (F \<in> X | G \<in> X) = (F Join G \<in> X)"
1.13
1.14    uv_prop  :: "'a program set => bool"
1.15 -   "uv_prop X == SKIP : X & (\<forall>F G. F ok G --> F:X & G: X --> (F Join G) : X)"
1.16 +   "uv_prop X == SKIP \<in> X & (\<forall>F G. F ok G --> F \<in> X & G \<in> X --> (F Join G) \<in> X)"
1.17
1.18    strict_uv_prop  :: "'a program set => bool"
1.19     "strict_uv_prop X ==
1.20 -      SKIP : X & (\<forall>F G. F ok G --> (F:X & G: X) = (F Join G : X))"
1.21 +      SKIP \<in> X & (\<forall>F G. F ok G --> (F \<in> X & G \<in> X) = (F Join G \<in> X))"
1.22
1.23    guar :: "['a program set, 'a program set] => 'a program set"
1.24            (infixl "guarantees" 55)  (*higher than membership, lower than Co*)
1.25 -   "X guarantees Y == {F. \<forall>G. F ok G --> F Join G : X --> F Join G : Y}"
1.26 +   "X guarantees Y == {F. \<forall>G. F ok G --> F Join G \<in> X --> F Join G \<in> Y}"
1.27
1.28
1.29    (* Weakest guarantees *)
1.30     wg :: "['a program, 'a program set] =>  'a program set"
1.31 -  "wg F Y == Union({X. F:X guarantees Y})"
1.32 +  "wg F Y == Union({X. F \<in> X guarantees Y})"
1.33
1.34     (* Weakest existential property stronger than X *)
1.35     wx :: "('a program) set => ('a program)set"
1.36 -   "wx X == Union({Y. Y<=X & ex_prop Y})"
1.37 +   "wx X == Union({Y. Y \<subseteq> X & ex_prop Y})"
1.38
1.39    (*Ill-defined programs can arise through "Join"*)
1.40    welldef :: "'a program set"
1.41 -  "welldef == {F. Init F ~= {}}"
1.42 +  "welldef == {F. Init F \<noteq> {}}"
1.43
1.44    refines :: "['a program, 'a program, 'a program set] => bool"
1.45  			("(3_ refines _ wrt _)" [10,10,10] 10)
1.46    "G refines F wrt X ==
1.47 -     \<forall>H. (F ok H  & G ok H & F Join H : welldef Int X) -->
1.48 -         (G Join H : welldef Int X)"
1.49 +     \<forall>H. (F ok H  & G ok H & F Join H \<in> welldef \<inter> X) -->
1.50 +         (G Join H \<in> welldef \<inter> X)"
1.51
1.52    iso_refines :: "['a program, 'a program, 'a program set] => bool"
1.53                                ("(3_ iso'_refines _ wrt _)" [10,10,10] 10)
1.54    "G iso_refines F wrt X ==
1.55 -   F : welldef Int X --> G : welldef Int X"
1.56 +   F \<in> welldef \<inter> X --> G \<in> welldef \<inter> X"
1.57
1.58
1.59  lemma OK_insert_iff:
1.60       "(OK (insert i I) F) =
1.61 -      (if i:I then OK I F else OK I F & (F i ok JOIN I F))"
1.62 +      (if i \<in> I then OK I F else OK I F & (F i ok JOIN I F))"
1.63  by (auto intro: ok_sym simp add: OK_iff_ok)
1.64
1.65
1.66  (*** existential properties ***)
1.67  lemma ex1 [rule_format]:
1.68   "[| ex_prop X; finite GG |] ==>
1.69 -     GG Int X ~= {}--> OK GG (%G. G) -->(JN G:GG. G) : X"
1.70 +     GG \<inter> X \<noteq> {}--> OK GG (%G. G) --> (\<Squnion>G \<in> GG. G) \<in> X"
1.71  apply (unfold ex_prop_def)
1.72  apply (erule finite_induct)
1.73  apply (auto simp add: OK_insert_iff Int_insert_left)
1.74 @@ -90,7 +90,7 @@
1.75
1.76
1.77  lemma ex2:
1.78 -     "\<forall>GG. finite GG & GG Int X ~= {} --> OK GG (%G. G) -->(JN G:GG. G):X
1.79 +     "\<forall>GG. finite GG & GG \<inter> X \<noteq> {} --> OK GG (%G. G) -->(\<Squnion>G \<in> GG. G):X
1.80        ==> ex_prop X"
1.81  apply (unfold ex_prop_def, clarify)
1.82  apply (drule_tac x = "{F,G}" in spec)
1.83 @@ -101,13 +101,13 @@
1.84  (*Chandy & Sanders take this as a definition*)
1.85  lemma ex_prop_finite:
1.86       "ex_prop X =
1.87 -      (\<forall>GG. finite GG & GG Int X ~= {} & OK GG (%G. G)--> (JN G:GG. G) : X)"
1.88 +      (\<forall>GG. finite GG & GG \<inter> X \<noteq> {} & OK GG (%G. G)--> (\<Squnion>G \<in> GG. G) \<in> X)"
1.89  by (blast intro: ex1 ex2)
1.90
1.91
1.92  (*Their "equivalent definition" given at the end of section 3*)
1.93  lemma ex_prop_equiv:
1.94 -     "ex_prop X = (\<forall>G. G:X = (\<forall>H. (G component_of H) --> H: X))"
1.95 +     "ex_prop X = (\<forall>G. G \<in> X = (\<forall>H. (G component_of H) --> H \<in> X))"
1.96  apply auto
1.97  apply (unfold ex_prop_def component_of_def, safe)
1.98  apply blast
1.99 @@ -120,14 +120,14 @@
1.100  (*** universal properties ***)
1.101  lemma uv1 [rule_format]:
1.102       "[| uv_prop X; finite GG |]
1.103 -      ==> GG <= X & OK GG (%G. G) --> (JN G:GG. G) : X"
1.104 +      ==> GG \<subseteq> X & OK GG (%G. G) --> (\<Squnion>G \<in> GG. G) \<in> X"
1.105  apply (unfold uv_prop_def)
1.106  apply (erule finite_induct)
1.107  apply (auto simp add: Int_insert_left OK_insert_iff)
1.108  done
1.109
1.110  lemma uv2:
1.111 -     "\<forall>GG. finite GG & GG <= X & OK GG (%G. G) --> (JN G:GG. G) : X
1.112 +     "\<forall>GG. finite GG & GG \<subseteq> X & OK GG (%G. G) --> (\<Squnion>G \<in> GG. G) \<in> X
1.113        ==> uv_prop X"
1.114  apply (unfold uv_prop_def)
1.115  apply (rule conjI)
1.116 @@ -141,37 +141,37 @@
1.117  (*Chandy & Sanders take this as a definition*)
1.118  lemma uv_prop_finite:
1.119       "uv_prop X =
1.120 -      (\<forall>GG. finite GG & GG <= X & OK GG (%G. G) --> (JN G:GG. G): X)"
1.121 +      (\<forall>GG. finite GG & GG \<subseteq> X & OK GG (%G. G) --> (\<Squnion>G \<in> GG. G): X)"
1.122  by (blast intro: uv1 uv2)
1.123
1.124  (*** guarantees ***)
1.125
1.126  lemma guaranteesI:
1.127 -     "(!!G. [| F ok G; F Join G : X |] ==> F Join G : Y)
1.128 -      ==> F : X guarantees Y"
1.129 +     "(!!G. [| F ok G; F Join G \<in> X |] ==> F Join G \<in> Y)
1.130 +      ==> F \<in> X guarantees Y"
1.131  by (simp add: guar_def component_def)
1.132
1.133  lemma guaranteesD:
1.134 -     "[| F : X guarantees Y;  F ok G;  F Join G : X |]
1.135 -      ==> F Join G : Y"
1.136 +     "[| F \<in> X guarantees Y;  F ok G;  F Join G \<in> X |]
1.137 +      ==> F Join G \<in> Y"
1.138  by (unfold guar_def component_def, blast)
1.139
1.140  (*This version of guaranteesD matches more easily in the conclusion
1.141 -  The major premise can no longer be  F<=H since we need to reason about G*)
1.142 +  The major premise can no longer be  F \<subseteq> H since we need to reason about G*)
1.143  lemma component_guaranteesD:
1.144 -     "[| F : X guarantees Y;  F Join G = H;  H : X;  F ok G |]
1.145 -      ==> H : Y"
1.146 +     "[| F \<in> X guarantees Y;  F Join G = H;  H \<in> X;  F ok G |]
1.147 +      ==> H \<in> Y"
1.148  by (unfold guar_def, blast)
1.149
1.150  lemma guarantees_weaken:
1.151 -     "[| F: X guarantees X'; Y <= X; X' <= Y' |] ==> F: Y guarantees Y'"
1.152 +     "[| F \<in> X guarantees X'; Y \<subseteq> X; X' \<subseteq> Y' |] ==> F \<in> Y guarantees Y'"
1.153  by (unfold guar_def, blast)
1.154
1.155 -lemma subset_imp_guarantees_UNIV: "X <= Y ==> X guarantees Y = UNIV"
1.156 +lemma subset_imp_guarantees_UNIV: "X \<subseteq> Y ==> X guarantees Y = UNIV"
1.157  by (unfold guar_def, blast)
1.158
1.159  (*Equivalent to subset_imp_guarantees_UNIV but more intuitive*)
1.160 -lemma subset_imp_guarantees: "X <= Y ==> F : X guarantees Y"
1.161 +lemma subset_imp_guarantees: "X \<subseteq> Y ==> F \<in> X guarantees Y"
1.162  by (unfold guar_def, blast)
1.163
1.164  (*Remark at end of section 4.1 *)
1.165 @@ -201,31 +201,31 @@
1.166  (** Distributive laws.  Re-orient to perform miniscoping **)
1.167
1.168  lemma guarantees_UN_left:
1.169 -     "(UN i:I. X i) guarantees Y = (INT i:I. X i guarantees Y)"
1.170 +     "(\<Union>i \<in> I. X i) guarantees Y = (\<Inter>i \<in> I. X i guarantees Y)"
1.171  by (unfold guar_def, blast)
1.172
1.173  lemma guarantees_Un_left:
1.174 -     "(X Un Y) guarantees Z = (X guarantees Z) Int (Y guarantees Z)"
1.175 +     "(X \<union> Y) guarantees Z = (X guarantees Z) \<inter> (Y guarantees Z)"
1.176  by (unfold guar_def, blast)
1.177
1.178  lemma guarantees_INT_right:
1.179 -     "X guarantees (INT i:I. Y i) = (INT i:I. X guarantees Y i)"
1.180 +     "X guarantees (\<Inter>i \<in> I. Y i) = (\<Inter>i \<in> I. X guarantees Y i)"
1.181  by (unfold guar_def, blast)
1.182
1.183  lemma guarantees_Int_right:
1.184 -     "Z guarantees (X Int Y) = (Z guarantees X) Int (Z guarantees Y)"
1.185 +     "Z guarantees (X \<inter> Y) = (Z guarantees X) \<inter> (Z guarantees Y)"
1.186  by (unfold guar_def, blast)
1.187
1.188  lemma guarantees_Int_right_I:
1.189 -     "[| F : Z guarantees X;  F : Z guarantees Y |]
1.190 -     ==> F : Z guarantees (X Int Y)"
1.191 +     "[| F \<in> Z guarantees X;  F \<in> Z guarantees Y |]
1.192 +     ==> F \<in> Z guarantees (X \<inter> Y)"
1.193  by (simp add: guarantees_Int_right)
1.194
1.195  lemma guarantees_INT_right_iff:
1.196 -     "(F : X guarantees (INTER I Y)) = (\<forall>i\<in>I. F : X guarantees (Y i))"
1.197 +     "(F \<in> X guarantees (INTER I Y)) = (\<forall>i\<in>I. F \<in> X guarantees (Y i))"
1.198  by (simp add: guarantees_INT_right)
1.199
1.200 -lemma shunting: "(X guarantees Y) = (UNIV guarantees (-X Un Y))"
1.201 +lemma shunting: "(X guarantees Y) = (UNIV guarantees (-X \<union> Y))"
1.202  by (unfold guar_def, blast)
1.203
1.204  lemma contrapositive: "(X guarantees Y) = -Y guarantees -X"
1.205 @@ -236,35 +236,35 @@
1.206  **)
1.207
1.208  lemma combining1:
1.209 -    "[| F : V guarantees X;  F : (X Int Y) guarantees Z |]
1.210 -     ==> F : (V Int Y) guarantees Z"
1.211 +    "[| F \<in> V guarantees X;  F \<in> (X \<inter> Y) guarantees Z |]
1.212 +     ==> F \<in> (V \<inter> Y) guarantees Z"
1.213
1.214  by (unfold guar_def, blast)
1.215
1.216  lemma combining2:
1.217 -    "[| F : V guarantees (X Un Y);  F : Y guarantees Z |]
1.218 -     ==> F : V guarantees (X Un Z)"
1.219 +    "[| F \<in> V guarantees (X \<union> Y);  F \<in> Y guarantees Z |]
1.220 +     ==> F \<in> V guarantees (X \<union> Z)"
1.221  by (unfold guar_def, blast)
1.222
1.223  (** The following two follow Chandy-Sanders, but the use of object-quantifiers
1.224      does not suit Isabelle... **)
1.225
1.226 -(*Premise should be (!!i. i: I ==> F: X guarantees Y i) *)
1.227 +(*Premise should be (!!i. i \<in> I ==> F \<in> X guarantees Y i) *)
1.228  lemma all_guarantees:
1.229 -     "\<forall>i\<in>I. F : X guarantees (Y i) ==> F : X guarantees (INT i:I. Y i)"
1.230 +     "\<forall>i\<in>I. F \<in> X guarantees (Y i) ==> F \<in> X guarantees (\<Inter>i \<in> I. Y i)"
1.231  by (unfold guar_def, blast)
1.232
1.233 -(*Premises should be [| F: X guarantees Y i; i: I |] *)
1.234 +(*Premises should be [| F \<in> X guarantees Y i; i \<in> I |] *)
1.235  lemma ex_guarantees:
1.236 -     "\<exists>i\<in>I. F : X guarantees (Y i) ==> F : X guarantees (UN i:I. Y i)"
1.237 +     "\<exists>i\<in>I. F \<in> X guarantees (Y i) ==> F \<in> X guarantees (\<Union>i \<in> I. Y i)"
1.238  by (unfold guar_def, blast)
1.239
1.240
1.241  (*** Additional guarantees laws, by lcp ***)
1.242
1.243  lemma guarantees_Join_Int:
1.244 -    "[| F: U guarantees V;  G: X guarantees Y; F ok G |]
1.245 -     ==> F Join G: (U Int X) guarantees (V Int Y)"
1.246 +    "[| F \<in> U guarantees V;  G \<in> X guarantees Y; F ok G |]
1.247 +     ==> F Join G \<in> (U \<inter> X) guarantees (V \<inter> Y)"
1.248  apply (unfold guar_def)
1.249  apply (simp (no_asm))
1.250  apply safe
1.251 @@ -275,8 +275,8 @@
1.252  done
1.253
1.254  lemma guarantees_Join_Un:
1.255 -    "[| F: U guarantees V;  G: X guarantees Y; F ok G |]
1.256 -     ==> F Join G: (U Un X) guarantees (V Un Y)"
1.257 +    "[| F \<in> U guarantees V;  G \<in> X guarantees Y; F ok G |]
1.258 +     ==> F Join G \<in> (U \<union> X) guarantees (V \<union> Y)"
1.259  apply (unfold guar_def)
1.260  apply (simp (no_asm))
1.261  apply safe
1.262 @@ -287,8 +287,8 @@
1.263  done
1.264
1.265  lemma guarantees_JN_INT:
1.266 -     "[| \<forall>i\<in>I. F i : X i guarantees Y i;  OK I F |]
1.267 -      ==> (JOIN I F) : (INTER I X) guarantees (INTER I Y)"
1.268 +     "[| \<forall>i\<in>I. F i \<in> X i guarantees Y i;  OK I F |]
1.269 +      ==> (JOIN I F) \<in> (INTER I X) guarantees (INTER I Y)"
1.270  apply (unfold guar_def, auto)
1.271  apply (drule bspec, assumption)
1.272  apply (rename_tac "i")
1.273 @@ -298,8 +298,8 @@
1.274  done
1.275
1.276  lemma guarantees_JN_UN:
1.277 -    "[| \<forall>i\<in>I. F i : X i guarantees Y i;  OK I F |]
1.278 -     ==> (JOIN I F) : (UNION I X) guarantees (UNION I Y)"
1.279 +    "[| \<forall>i\<in>I. F i \<in> X i guarantees Y i;  OK I F |]
1.280 +     ==> (JOIN I F) \<in> (UNION I X) guarantees (UNION I Y)"
1.281  apply (unfold guar_def, auto)
1.282  apply (drule bspec, assumption)
1.283  apply (rename_tac "i")
1.284 @@ -312,7 +312,7 @@
1.285  (*** guarantees laws for breaking down the program, by lcp ***)
1.286
1.287  lemma guarantees_Join_I1:
1.288 -     "[| F: X guarantees Y;  F ok G |] ==> F Join G: X guarantees Y"
1.289 +     "[| F \<in> X guarantees Y;  F ok G |] ==> F Join G \<in> X guarantees Y"
1.290  apply (unfold guar_def)
1.291  apply (simp (no_asm))
1.292  apply safe
1.293 @@ -320,14 +320,14 @@
1.294  done
1.295
1.296  lemma guarantees_Join_I2:
1.297 -     "[| G: X guarantees Y;  F ok G |] ==> F Join G: X guarantees Y"
1.298 +     "[| G \<in> X guarantees Y;  F ok G |] ==> F Join G \<in> X guarantees Y"
1.299  apply (simp add: Join_commute [of _ G] ok_commute [of _ G])
1.300  apply (blast intro: guarantees_Join_I1)
1.301  done
1.302
1.303  lemma guarantees_JN_I:
1.304 -     "[| i : I;  F i: X guarantees Y;  OK I F |]
1.305 -      ==> (JN i:I. (F i)) : X guarantees Y"
1.306 +     "[| i \<in> I;  F i \<in> X guarantees Y;  OK I F |]
1.307 +      ==> (\<Squnion>i \<in> I. (F i)) \<in> X guarantees Y"
1.308  apply (unfold guar_def, clarify)
1.309  apply (drule_tac x = "JOIN (I-{i}) F Join G" in spec)
1.310  apply (auto intro: OK_imp_ok simp add: JN_Join_diff JN_Join_diff Join_assoc [symmetric])
1.311 @@ -336,10 +336,10 @@
1.312
1.313  (*** well-definedness ***)
1.314
1.315 -lemma Join_welldef_D1: "F Join G: welldef ==> F: welldef"
1.316 +lemma Join_welldef_D1: "F Join G \<in> welldef ==> F \<in> welldef"
1.317  by (unfold welldef_def, auto)
1.318
1.319 -lemma Join_welldef_D2: "F Join G: welldef ==> G: welldef"
1.320 +lemma Join_welldef_D2: "F Join G \<in> welldef ==> G \<in> welldef"
1.321  by (unfold welldef_def, auto)
1.322
1.323  (*** refinement ***)
1.324 @@ -357,14 +357,14 @@
1.325
1.326  lemma strict_ex_refine_lemma:
1.327       "strict_ex_prop X
1.328 -      ==> (\<forall>H. F ok H & G ok H & F Join H : X --> G Join H : X)
1.329 -              = (F:X --> G:X)"
1.330 +      ==> (\<forall>H. F ok H & G ok H & F Join H \<in> X --> G Join H \<in> X)
1.331 +              = (F \<in> X --> G \<in> X)"
1.332  by (unfold strict_ex_prop_def, auto)
1.333
1.334  lemma strict_ex_refine_lemma_v:
1.335       "strict_ex_prop X
1.336 -      ==> (\<forall>H. F ok H & G ok H & F Join H : welldef & F Join H : X --> G Join H : X) =
1.337 -          (F: welldef Int X --> G:X)"
1.338 +      ==> (\<forall>H. F ok H & G ok H & F Join H \<in> welldef & F Join H \<in> X --> G Join H \<in> X) =
1.339 +          (F \<in> welldef \<inter> X --> G \<in> X)"
1.340  apply (unfold strict_ex_prop_def, safe)
1.341  apply (erule_tac x = SKIP and P = "%H. ?PP H --> ?RR H" in allE)
1.342  apply (auto dest: Join_welldef_D1 Join_welldef_D2)
1.343 @@ -372,7 +372,7 @@
1.344
1.345  lemma ex_refinement_thm:
1.346       "[| strict_ex_prop X;
1.347 -         \<forall>H. F ok H & G ok H & F Join H : welldef Int X --> G Join H : welldef |]
1.348 +         \<forall>H. F ok H & G ok H & F Join H \<in> welldef \<inter> X --> G Join H \<in> welldef |]
1.349        ==> (G refines F wrt X) = (G iso_refines F wrt X)"
1.350  apply (rule_tac x = SKIP in allE, assumption)
1.351  apply (simp add: refines_def iso_refines_def strict_ex_refine_lemma_v)
1.352 @@ -381,13 +381,13 @@
1.353
1.354  lemma strict_uv_refine_lemma:
1.355       "strict_uv_prop X ==>
1.356 -      (\<forall>H. F ok H & G ok H & F Join H : X --> G Join H : X) = (F:X --> G:X)"
1.357 +      (\<forall>H. F ok H & G ok H & F Join H \<in> X --> G Join H \<in> X) = (F \<in> X --> G \<in> X)"
1.358  by (unfold strict_uv_prop_def, blast)
1.359
1.360  lemma strict_uv_refine_lemma_v:
1.361       "strict_uv_prop X
1.362 -      ==> (\<forall>H. F ok H & G ok H & F Join H : welldef & F Join H : X --> G Join H : X) =
1.363 -          (F: welldef Int X --> G:X)"
1.364 +      ==> (\<forall>H. F ok H & G ok H & F Join H \<in> welldef & F Join H \<in> X --> G Join H \<in> X) =
1.365 +          (F \<in> welldef \<inter> X --> G \<in> X)"
1.366  apply (unfold strict_uv_prop_def, safe)
1.367  apply (erule_tac x = SKIP and P = "%H. ?PP H --> ?RR H" in allE)
1.368  apply (auto dest: Join_welldef_D1 Join_welldef_D2)
1.369 @@ -395,8 +395,8 @@
1.370
1.371  lemma uv_refinement_thm:
1.372       "[| strict_uv_prop X;
1.373 -         \<forall>H. F ok H & G ok H & F Join H : welldef Int X -->
1.374 -             G Join H : welldef |]
1.375 +         \<forall>H. F ok H & G ok H & F Join H \<in> welldef \<inter> X -->
1.376 +             G Join H \<in> welldef |]
1.377        ==> (G refines F wrt X) = (G iso_refines F wrt X)"
1.378  apply (rule_tac x = SKIP in allE, assumption)
1.379  apply (simp add: refines_def iso_refines_def strict_uv_refine_lemma_v)
1.380 @@ -404,17 +404,17 @@
1.381
1.382  (* Added by Sidi Ehmety from Chandy & Sander, section 6 *)
1.383  lemma guarantees_equiv:
1.384 -    "(F:X guarantees Y) = (\<forall>H. H:X \<longrightarrow> (F component_of H \<longrightarrow> H:Y))"
1.385 +    "(F \<in> X guarantees Y) = (\<forall>H. H \<in> X \<longrightarrow> (F component_of H \<longrightarrow> H \<in> Y))"
1.386  by (unfold guar_def component_of_def, auto)
1.387
1.388 -lemma wg_weakest: "!!X. F:(X guarantees Y) ==> X <= (wg F Y)"
1.389 +lemma wg_weakest: "!!X. F:(X guarantees Y) ==> X \<subseteq> (wg F Y)"
1.390  by (unfold wg_def, auto)
1.391
1.392  lemma wg_guarantees: "F:((wg F Y) guarantees Y)"
1.393  by (unfold wg_def guar_def, blast)
1.394
1.395  lemma wg_equiv:
1.396 -  "(H: wg F X) = (F component_of H --> H:X)"
1.397 +  "(H \<in> wg F X) = (F component_of H --> H \<in> X)"
1.398  apply (unfold wg_def)
1.399  apply (simp (no_asm) add: guarantees_equiv)
1.400  apply (rule iffI)
1.401 @@ -423,21 +423,21 @@
1.402  done
1.403
1.404
1.405 -lemma component_of_wg: "F component_of H ==> (H:wg F X) = (H:X)"
1.406 +lemma component_of_wg: "F component_of H ==> (H \<in> wg F X) = (H \<in> X)"
1.407  by (simp add: wg_equiv)
1.408
1.409  lemma wg_finite:
1.410 -    "\<forall>FF. finite FF & FF Int X ~= {} --> OK FF (%F. F)
1.411 -          --> (\<forall>F\<in>FF. ((JN F:FF. F): wg F X) = ((JN F:FF. F):X))"
1.412 +    "\<forall>FF. finite FF & FF \<inter> X \<noteq> {} --> OK FF (%F. F)
1.413 +          --> (\<forall>F\<in>FF. ((\<Squnion>F \<in> FF. F): wg F X) = ((\<Squnion>F \<in> FF. F):X))"
1.414  apply clarify
1.415 -apply (subgoal_tac "F component_of (JN F:FF. F) ")
1.416 +apply (subgoal_tac "F component_of (\<Squnion>F \<in> FF. F) ")
1.417  apply (drule_tac X = X in component_of_wg, simp)
1.418  apply (simp add: component_of_def)
1.419 -apply (rule_tac x = "JN F: (FF-{F}) . F" in exI)
1.420 +apply (rule_tac x = "\<Squnion>F \<in> (FF-{F}) . F" in exI)
1.421  apply (auto intro: JN_Join_diff dest: ok_sym simp add: OK_iff_ok)
1.422  done
1.423
1.424 -lemma wg_ex_prop: "ex_prop X ==> (F:X) = (\<forall>H. H : wg F X)"
1.425 +lemma wg_ex_prop: "ex_prop X ==> (F \<in> X) = (\<forall>H. H \<in> wg F X)"
1.426  apply (simp (no_asm_use) add: ex_prop_equiv wg_equiv)
1.427  apply blast
1.428  done
1.429 @@ -455,11 +455,11 @@
1.430  apply auto
1.431  done
1.432
1.433 -lemma wx_weakest: "\<forall>Z. Z<= X --> ex_prop Z --> Z <= wx X"
1.434 +lemma wx_weakest: "\<forall>Z. Z<= X --> ex_prop Z --> Z \<subseteq> wx X"
1.435  by (unfold wx_def, auto)
1.436
1.437  (* Proposition 6 *)
1.438 -lemma wx'_ex_prop: "ex_prop({F. \<forall>G. F ok G --> F Join G:X})"
1.439 +lemma wx'_ex_prop: "ex_prop({F. \<forall>G. F ok G --> F Join G \<in> X})"
1.440  apply (unfold ex_prop_def, safe)
1.441  apply (drule_tac x = "G Join Ga" in spec)
1.442  apply (force simp add: ok_Join_iff1 Join_assoc)
1.443 @@ -483,7 +483,7 @@
1.444  apply (drule_tac x = G in spec)
1.445  apply (frule_tac c = "x Join G" in subsetD, safe)
1.446  apply (simp (no_asm))
1.447 -apply (rule_tac x = "{F. \<forall>G. F ok G --> F Join G:X}" in exI, safe)
1.448 +apply (rule_tac x = "{F. \<forall>G. F ok G --> F Join G \<in> X}" in exI, safe)
1.449  apply (rule_tac  wx'_ex_prop)
1.450  apply (rotate_tac 1)
1.451  apply (drule_tac x = SKIP in spec, auto)
1.452 @@ -496,7 +496,7 @@
1.453  (* Proposition 12 *)
1.454  (* Main result of the paper *)
1.455  lemma guarantees_wx_eq:
1.456 -   "(X guarantees Y) = wx(-X Un Y)"
1.457 +   "(X guarantees Y) = wx(-X \<union> Y)"
1.458  apply (unfold guar_def)
1.459  apply (simp (no_asm) add: wx_equiv)
1.460  done
1.461 @@ -511,7 +511,7 @@
1.462      Reasoning About Program composition paper *)
1.463
1.464  lemma stable_guarantees_Always:
1.465 -     "Init F <= A ==> F:(stable A) guarantees (Always A)"
1.466 +     "Init F \<subseteq> A ==> F:(stable A) guarantees (Always A)"
1.467  apply (rule guaranteesI)
1.468  apply (simp (no_asm) add: Join_commute)
1.469  apply (rule stable_Join_Always1)
1.470 @@ -519,7 +519,7 @@
1.471  done
1.472
1.473  (* To be moved to WFair.ML *)
1.474 -lemma leadsTo_Basis': "[| F:A co A Un B; F:transient A |] ==> F:A leadsTo B"
1.475 +lemma leadsTo_Basis': "[| F \<in> A co A \<union> B; F \<in> transient A |] ==> F \<in> A leadsTo B"
1.476  apply (drule_tac B = "A-B" in constrains_weaken_L)
1.477  apply (drule_tac  B = "A-B" in transient_strengthen)
1.478  apply (rule_tac  ensuresI [THEN leadsTo_Basis])
1.479 @@ -529,7 +529,7 @@
1.480
1.481