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 [2] 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 [2] B = "A-B" in transient_strengthen)
   1.478  apply (rule_tac [3] ensuresI [THEN leadsTo_Basis])
   1.479 @@ -529,7 +529,7 @@
   1.480  
   1.481  
   1.482  lemma constrains_guarantees_leadsTo:
   1.483 -     "F : transient A ==> F: (A co A Un B) guarantees (A leadsTo (B-A))"
   1.484 +     "F \<in> transient A ==> F \<in> (A co A \<union> B) guarantees (A leadsTo (B-A))"
   1.485  apply (rule guaranteesI)
   1.486  apply (rule leadsTo_Basis')
   1.487  apply (drule constrains_weaken_R)