src/HOL/UNITY/Union.thy
changeset 13805 3786b2fd6808
parent 13798 4c1a53627500
child 13812 91713a1915ee
     1.1 --- a/src/HOL/UNITY/Union.thy	Mon Feb 03 11:45:05 2003 +0100
     1.2 +++ b/src/HOL/UNITY/Union.thy	Tue Feb 04 18:12:40 2003 +0100
     1.3 @@ -12,36 +12,36 @@
     1.4  
     1.5  constdefs
     1.6  
     1.7 -  (*FIXME: conjoin Init F Int Init G ~= {} *) 
     1.8 +  (*FIXME: conjoin Init F \<inter> Init G \<noteq> {} *) 
     1.9    ok :: "['a program, 'a program] => bool"      (infixl "ok" 65)
    1.10 -    "F ok G == Acts F <= AllowedActs G &
    1.11 -               Acts G <= AllowedActs F"
    1.12 +    "F ok G == Acts F \<subseteq> AllowedActs G &
    1.13 +               Acts G \<subseteq> AllowedActs F"
    1.14  
    1.15 -  (*FIXME: conjoin (INT i:I. Init (F i)) ~= {} *) 
    1.16 +  (*FIXME: conjoin (\<Inter>i \<in> I. Init (F i)) \<noteq> {} *) 
    1.17    OK  :: "['a set, 'a => 'b program] => bool"
    1.18 -    "OK I F == (ALL i:I. ALL j: I-{i}. Acts (F i) <= AllowedActs (F j))"
    1.19 +    "OK I F == (\<forall>i \<in> I. \<forall>j \<in> I-{i}. Acts (F i) \<subseteq> AllowedActs (F j))"
    1.20  
    1.21    JOIN  :: "['a set, 'a => 'b program] => 'b program"
    1.22 -    "JOIN I F == mk_program (INT i:I. Init (F i), UN i:I. Acts (F i),
    1.23 -			     INT i:I. AllowedActs (F i))"
    1.24 +    "JOIN I F == mk_program (\<Inter>i \<in> I. Init (F i), \<Union>i \<in> I. Acts (F i),
    1.25 +			     \<Inter>i \<in> I. AllowedActs (F i))"
    1.26  
    1.27    Join :: "['a program, 'a program] => 'a program"      (infixl "Join" 65)
    1.28 -    "F Join G == mk_program (Init F Int Init G, Acts F Un Acts G,
    1.29 -			     AllowedActs F Int AllowedActs G)"
    1.30 +    "F Join G == mk_program (Init F \<inter> Init G, Acts F \<union> Acts G,
    1.31 +			     AllowedActs F \<inter> AllowedActs G)"
    1.32  
    1.33    SKIP :: "'a program"
    1.34      "SKIP == mk_program (UNIV, {}, UNIV)"
    1.35  
    1.36    (*Characterizes safety properties.  Used with specifying AllowedActs*)
    1.37    safety_prop :: "'a program set => bool"
    1.38 -    "safety_prop X == SKIP: X & (ALL G. Acts G <= UNION X Acts --> G : X)"
    1.39 +    "safety_prop X == SKIP: X & (\<forall>G. Acts G \<subseteq> UNION X Acts --> G \<in> X)"
    1.40  
    1.41  syntax
    1.42    "@JOIN1"     :: "[pttrns, 'b set] => 'b set"         ("(3JN _./ _)" 10)
    1.43    "@JOIN"      :: "[pttrn, 'a set, 'b set] => 'b set"  ("(3JN _:_./ _)" 10)
    1.44  
    1.45  translations
    1.46 -  "JN x:A. B"   == "JOIN A (%x. B)"
    1.47 +  "JN x : A. B"   == "JOIN A (%x. B)"
    1.48    "JN x y. B"   == "JN x. JN y. B"
    1.49    "JN x. B"     == "JOIN UNIV (%x. B)"
    1.50  
    1.51 @@ -49,7 +49,7 @@
    1.52    SKIP      :: "'a program"                              ("\<bottom>")
    1.53    "op Join" :: "['a program, 'a program] => 'a program"  (infixl "\<squnion>" 65)
    1.54    "@JOIN1"  :: "[pttrns, 'b set] => 'b set"              ("(3\<Squnion> _./ _)" 10)
    1.55 -  "@JOIN"   :: "[pttrn, 'a set, 'b set] => 'b set"       ("(3\<Squnion> _:_./ _)" 10)
    1.56 +  "@JOIN"   :: "[pttrn, 'a set, 'b set] => 'b set"       ("(3\<Squnion> _\<in>_./ _)" 10)
    1.57  
    1.58  
    1.59  subsection{*SKIP*}
    1.60 @@ -68,13 +68,13 @@
    1.61  
    1.62  subsection{*SKIP and safety properties*}
    1.63  
    1.64 -lemma SKIP_in_constrains_iff [iff]: "(SKIP : A co B) = (A<=B)"
    1.65 +lemma SKIP_in_constrains_iff [iff]: "(SKIP \<in> A co B) = (A \<subseteq> B)"
    1.66  by (unfold constrains_def, auto)
    1.67  
    1.68 -lemma SKIP_in_Constrains_iff [iff]: "(SKIP : A Co B) = (A<=B)"
    1.69 +lemma SKIP_in_Constrains_iff [iff]: "(SKIP \<in> A Co B) = (A \<subseteq> B)"
    1.70  by (unfold Constrains_def, auto)
    1.71  
    1.72 -lemma SKIP_in_stable [iff]: "SKIP : stable A"
    1.73 +lemma SKIP_in_stable [iff]: "SKIP \<in> stable A"
    1.74  by (unfold stable_def, auto)
    1.75  
    1.76  declare SKIP_in_stable [THEN stable_imp_Stable, iff]
    1.77 @@ -82,40 +82,40 @@
    1.78  
    1.79  subsection{*Join*}
    1.80  
    1.81 -lemma Init_Join [simp]: "Init (F Join G) = Init F Int Init G"
    1.82 +lemma Init_Join [simp]: "Init (F Join G) = Init F \<inter> Init G"
    1.83  by (simp add: Join_def)
    1.84  
    1.85 -lemma Acts_Join [simp]: "Acts (F Join G) = Acts F Un Acts G"
    1.86 +lemma Acts_Join [simp]: "Acts (F Join G) = Acts F \<union> Acts G"
    1.87  by (auto simp add: Join_def)
    1.88  
    1.89  lemma AllowedActs_Join [simp]:
    1.90 -     "AllowedActs (F Join G) = AllowedActs F Int AllowedActs G"
    1.91 +     "AllowedActs (F Join G) = AllowedActs F \<inter> AllowedActs G"
    1.92  by (auto simp add: Join_def)
    1.93  
    1.94  
    1.95  subsection{*JN*}
    1.96  
    1.97 -lemma JN_empty [simp]: "(JN i:{}. F i) = SKIP"
    1.98 +lemma JN_empty [simp]: "(\<Squnion>i\<in>{}. F i) = SKIP"
    1.99  by (unfold JOIN_def SKIP_def, auto)
   1.100  
   1.101 -lemma JN_insert [simp]: "(JN i:insert a I. F i) = (F a) Join (JN i:I. F i)"
   1.102 +lemma JN_insert [simp]: "(\<Squnion>i \<in> insert a I. F i) = (F a) Join (\<Squnion>i \<in> I. F i)"
   1.103  apply (rule program_equalityI)
   1.104  apply (auto simp add: JOIN_def Join_def)
   1.105  done
   1.106  
   1.107 -lemma Init_JN [simp]: "Init (JN i:I. F i) = (INT i:I. Init (F i))"
   1.108 +lemma Init_JN [simp]: "Init (\<Squnion>i \<in> I. F i) = (\<Inter>i \<in> I. Init (F i))"
   1.109  by (simp add: JOIN_def)
   1.110  
   1.111 -lemma Acts_JN [simp]: "Acts (JN i:I. F i) = insert Id (UN i:I. Acts (F i))"
   1.112 +lemma Acts_JN [simp]: "Acts (\<Squnion>i \<in> I. F i) = insert Id (\<Union>i \<in> I. Acts (F i))"
   1.113  by (auto simp add: JOIN_def)
   1.114  
   1.115  lemma AllowedActs_JN [simp]:
   1.116 -     "AllowedActs (JN i:I. F i) = (INT i:I. AllowedActs (F i))"
   1.117 +     "AllowedActs (\<Squnion>i \<in> I. F i) = (\<Inter>i \<in> I. AllowedActs (F i))"
   1.118  by (auto simp add: JOIN_def)
   1.119  
   1.120  
   1.121  lemma JN_cong [cong]: 
   1.122 -    "[| I=J;  !!i. i:J ==> F i = G i |] ==> (JN i:I. F i) = (JN i:J. G i)"
   1.123 +    "[| I=J;  !!i. i \<in> J ==> F i = G i |] ==> (\<Squnion>i \<in> I. F i) = (\<Squnion>i \<in> J. G i)"
   1.124  by (simp add: JOIN_def)
   1.125  
   1.126  
   1.127 @@ -156,28 +156,28 @@
   1.128  lemmas Join_ac = Join_assoc Join_left_absorb Join_commute Join_left_commute
   1.129  
   1.130  
   1.131 -subsection{*JN laws*}
   1.132 +subsection{*\<Squnion>laws*}
   1.133  
   1.134  (*Also follows by JN_insert and insert_absorb, but the proof is longer*)
   1.135 -lemma JN_absorb: "k:I ==> F k Join (JN i:I. F i) = (JN i:I. F i)"
   1.136 +lemma JN_absorb: "k \<in> I ==> F k Join (\<Squnion>i \<in> I. F i) = (\<Squnion>i \<in> I. F i)"
   1.137  by (auto intro!: program_equalityI)
   1.138  
   1.139 -lemma JN_Un: "(JN i: I Un J. F i) = ((JN i: I. F i) Join (JN i:J. F i))"
   1.140 +lemma JN_Un: "(\<Squnion>i \<in> I \<union> J. F i) = ((\<Squnion>i \<in> I. F i) Join (\<Squnion>i \<in> J. F i))"
   1.141  by (auto intro!: program_equalityI)
   1.142  
   1.143 -lemma JN_constant: "(JN i:I. c) = (if I={} then SKIP else c)"
   1.144 +lemma JN_constant: "(\<Squnion>i \<in> I. c) = (if I={} then SKIP else c)"
   1.145  by (rule program_equalityI, auto)
   1.146  
   1.147  lemma JN_Join_distrib:
   1.148 -     "(JN i:I. F i Join G i) = (JN i:I. F i)  Join  (JN i:I. G i)"
   1.149 +     "(\<Squnion>i \<in> I. F i Join G i) = (\<Squnion>i \<in> I. F i)  Join  (\<Squnion>i \<in> I. G i)"
   1.150  by (auto intro!: program_equalityI)
   1.151  
   1.152  lemma JN_Join_miniscope:
   1.153 -     "i : I ==> (JN i:I. F i Join G) = ((JN i:I. F i) Join G)"
   1.154 +     "i \<in> I ==> (\<Squnion>i \<in> I. F i Join G) = ((\<Squnion>i \<in> I. F i) Join G)"
   1.155  by (auto simp add: JN_Join_distrib JN_constant)
   1.156  
   1.157  (*Used to prove guarantees_JN_I*)
   1.158 -lemma JN_Join_diff: "i: I ==> F i Join JOIN (I - {i}) F = JOIN I F"
   1.159 +lemma JN_Join_diff: "i \<in> I ==> F i Join JOIN (I - {i}) F = JOIN I F"
   1.160  apply (unfold JOIN_def Join_def)
   1.161  apply (rule program_equalityI, auto)
   1.162  done
   1.163 @@ -185,19 +185,19 @@
   1.164  
   1.165  subsection{*Safety: co, stable, FP*}
   1.166  
   1.167 -(*Fails if I={} because it collapses to SKIP : A co B, i.e. to A<=B.  So an
   1.168 -  alternative precondition is A<=B, but most proofs using this rule require
   1.169 +(*Fails if I={} because it collapses to SKIP \<in> A co B, i.e. to A \<subseteq> B.  So an
   1.170 +  alternative precondition is A \<subseteq> B, but most proofs using this rule require
   1.171    I to be nonempty for other reasons anyway.*)
   1.172  lemma JN_constrains: 
   1.173 -    "i : I ==> (JN i:I. F i) : A co B = (ALL i:I. F i : A co B)"
   1.174 +    "i \<in> I ==> (\<Squnion>i \<in> I. F i) \<in> A co B = (\<forall>i \<in> I. F i \<in> A co B)"
   1.175  by (simp add: constrains_def JOIN_def, blast)
   1.176  
   1.177  lemma Join_constrains [simp]:
   1.178 -     "(F Join G : A co B) = (F : A co B & G : A co B)"
   1.179 +     "(F Join G \<in> A co B) = (F \<in> A co B & G \<in> A co B)"
   1.180  by (auto simp add: constrains_def Join_def)
   1.181  
   1.182  lemma Join_unless [simp]:
   1.183 -     "(F Join G : A unless B) = (F : A unless B & G : A unless B)"
   1.184 +     "(F Join G \<in> A unless B) = (F \<in> A unless B & G \<in> A unless B)"
   1.185  by (simp add: Join_constrains unless_def)
   1.186  
   1.187  (*Analogous weak versions FAIL; see Misra [1994] 5.4.1, Substitution Axiom.
   1.188 @@ -206,100 +206,100 @@
   1.189  
   1.190  
   1.191  lemma Join_constrains_weaken:
   1.192 -     "[| F : A co A';  G : B co B' |]  
   1.193 -      ==> F Join G : (A Int B) co (A' Un B')"
   1.194 +     "[| F \<in> A co A';  G \<in> B co B' |]  
   1.195 +      ==> F Join G \<in> (A \<inter> B) co (A' \<union> B')"
   1.196  by (simp, blast intro: constrains_weaken)
   1.197  
   1.198 -(*If I={}, it degenerates to SKIP : UNIV co {}, which is false.*)
   1.199 +(*If I={}, it degenerates to SKIP \<in> UNIV co {}, which is false.*)
   1.200  lemma JN_constrains_weaken:
   1.201 -     "[| ALL i:I. F i : A i co A' i;  i: I |]  
   1.202 -      ==> (JN i:I. F i) : (INT i:I. A i) co (UN i:I. A' i)"
   1.203 +     "[| \<forall>i \<in> I. F i \<in> A i co A' i;  i \<in> I |]  
   1.204 +      ==> (\<Squnion>i \<in> I. F i) \<in> (\<Inter>i \<in> I. A i) co (\<Union>i \<in> I. A' i)"
   1.205  apply (simp (no_asm_simp) add: JN_constrains)
   1.206  apply (blast intro: constrains_weaken)
   1.207  done
   1.208  
   1.209 -lemma JN_stable: "(JN i:I. F i) : stable A = (ALL i:I. F i : stable A)"
   1.210 +lemma JN_stable: "(\<Squnion>i \<in> I. F i) \<in> stable A = (\<forall>i \<in> I. F i \<in> stable A)"
   1.211  by (simp add: stable_def constrains_def JOIN_def)
   1.212  
   1.213  lemma invariant_JN_I:
   1.214 -     "[| !!i. i:I ==> F i : invariant A;  i : I |]   
   1.215 -       ==> (JN i:I. F i) : invariant A"
   1.216 +     "[| !!i. i \<in> I ==> F i \<in> invariant A;  i \<in> I |]   
   1.217 +       ==> (\<Squnion>i \<in> I. F i) \<in> invariant A"
   1.218  by (simp add: invariant_def JN_stable, blast)
   1.219  
   1.220  lemma Join_stable [simp]:
   1.221 -     "(F Join G : stable A) =  
   1.222 -      (F : stable A & G : stable A)"
   1.223 +     "(F Join G \<in> stable A) =  
   1.224 +      (F \<in> stable A & G \<in> stable A)"
   1.225  by (simp add: stable_def)
   1.226  
   1.227  lemma Join_increasing [simp]:
   1.228 -     "(F Join G : increasing f) =  
   1.229 -      (F : increasing f & G : increasing f)"
   1.230 +     "(F Join G \<in> increasing f) =  
   1.231 +      (F \<in> increasing f & G \<in> increasing f)"
   1.232  by (simp add: increasing_def Join_stable, blast)
   1.233  
   1.234  lemma invariant_JoinI:
   1.235 -     "[| F : invariant A; G : invariant A |]   
   1.236 -      ==> F Join G : invariant A"
   1.237 +     "[| F \<in> invariant A; G \<in> invariant A |]   
   1.238 +      ==> F Join G \<in> invariant A"
   1.239  by (simp add: invariant_def, blast)
   1.240  
   1.241 -lemma FP_JN: "FP (JN i:I. F i) = (INT i:I. FP (F i))"
   1.242 +lemma FP_JN: "FP (\<Squnion>i \<in> I. F i) = (\<Inter>i \<in> I. FP (F i))"
   1.243  by (simp add: FP_def JN_stable INTER_def)
   1.244  
   1.245  
   1.246  subsection{*Progress: transient, ensures*}
   1.247  
   1.248  lemma JN_transient:
   1.249 -     "i : I ==>  
   1.250 -    (JN i:I. F i) : transient A = (EX i:I. F i : transient A)"
   1.251 +     "i \<in> I ==>  
   1.252 +    (\<Squnion>i \<in> I. F i) \<in> transient A = (\<exists>i \<in> I. F i \<in> transient A)"
   1.253  by (auto simp add: transient_def JOIN_def)
   1.254  
   1.255  lemma Join_transient [simp]:
   1.256 -     "F Join G : transient A =  
   1.257 -      (F : transient A | G : transient A)"
   1.258 +     "F Join G \<in> transient A =  
   1.259 +      (F \<in> transient A | G \<in> transient A)"
   1.260  by (auto simp add: bex_Un transient_def Join_def)
   1.261  
   1.262 -lemma Join_transient_I1: "F : transient A ==> F Join G : transient A"
   1.263 +lemma Join_transient_I1: "F \<in> transient A ==> F Join G \<in> transient A"
   1.264  by (simp add: Join_transient)
   1.265  
   1.266 -lemma Join_transient_I2: "G : transient A ==> F Join G : transient A"
   1.267 +lemma Join_transient_I2: "G \<in> transient A ==> F Join G \<in> transient A"
   1.268  by (simp add: Join_transient)
   1.269  
   1.270 -(*If I={} it degenerates to (SKIP : A ensures B) = False, i.e. to ~(A<=B) *)
   1.271 +(*If I={} it degenerates to (SKIP \<in> A ensures B) = False, i.e. to ~(A \<subseteq> B) *)
   1.272  lemma JN_ensures:
   1.273 -     "i : I ==>  
   1.274 -      (JN i:I. F i) : A ensures B =  
   1.275 -      ((ALL i:I. F i : (A-B) co (A Un B)) & (EX i:I. F i : A ensures B))"
   1.276 +     "i \<in> I ==>  
   1.277 +      (\<Squnion>i \<in> I. F i) \<in> A ensures B =  
   1.278 +      ((\<forall>i \<in> I. F i \<in> (A-B) co (A \<union> B)) & (\<exists>i \<in> I. F i \<in> A ensures B))"
   1.279  by (auto simp add: ensures_def JN_constrains JN_transient)
   1.280  
   1.281  lemma Join_ensures: 
   1.282 -     "F Join G : A ensures B =      
   1.283 -      (F : (A-B) co (A Un B) & G : (A-B) co (A Un B) &  
   1.284 -       (F : transient (A-B) | G : transient (A-B)))"
   1.285 +     "F Join G \<in> A ensures B =      
   1.286 +      (F \<in> (A-B) co (A \<union> B) & G \<in> (A-B) co (A \<union> B) &  
   1.287 +       (F \<in> transient (A-B) | G \<in> transient (A-B)))"
   1.288  by (auto simp add: ensures_def Join_transient)
   1.289  
   1.290  lemma stable_Join_constrains: 
   1.291 -    "[| F : stable A;  G : A co A' |]  
   1.292 -     ==> F Join G : A co A'"
   1.293 +    "[| F \<in> stable A;  G \<in> A co A' |]  
   1.294 +     ==> F Join G \<in> A co A'"
   1.295  apply (unfold stable_def constrains_def Join_def)
   1.296  apply (simp add: ball_Un, blast)
   1.297  done
   1.298  
   1.299 -(*Premise for G cannot use Always because  F: Stable A  is weaker than
   1.300 -  G : stable A *)
   1.301 +(*Premise for G cannot use Always because  F \<in> Stable A  is weaker than
   1.302 +  G \<in> stable A *)
   1.303  lemma stable_Join_Always1:
   1.304 -     "[| F : stable A;  G : invariant A |] ==> F Join G : Always A"
   1.305 +     "[| F \<in> stable A;  G \<in> invariant A |] ==> F Join G \<in> Always A"
   1.306  apply (simp (no_asm_use) add: Always_def invariant_def Stable_eq_stable)
   1.307  apply (force intro: stable_Int)
   1.308  done
   1.309  
   1.310  (*As above, but exchanging the roles of F and G*)
   1.311  lemma stable_Join_Always2:
   1.312 -     "[| F : invariant A;  G : stable A |] ==> F Join G : Always A"
   1.313 +     "[| F \<in> invariant A;  G \<in> stable A |] ==> F Join G \<in> Always A"
   1.314  apply (subst Join_commute)
   1.315  apply (blast intro: stable_Join_Always1)
   1.316  done
   1.317  
   1.318  lemma stable_Join_ensures1:
   1.319 -     "[| F : stable A;  G : A ensures B |] ==> F Join G : A ensures B"
   1.320 +     "[| F \<in> stable A;  G \<in> A ensures B |] ==> F Join G \<in> A ensures B"
   1.321  apply (simp (no_asm_simp) add: Join_ensures)
   1.322  apply (simp add: stable_def ensures_def)
   1.323  apply (erule constrains_weaken, auto)
   1.324 @@ -307,7 +307,7 @@
   1.325  
   1.326  (*As above, but exchanging the roles of F and G*)
   1.327  lemma stable_Join_ensures2:
   1.328 -     "[| F : A ensures B;  G : stable A |] ==> F Join G : A ensures B"
   1.329 +     "[| F \<in> A ensures B;  G \<in> stable A |] ==> F Join G \<in> A ensures B"
   1.330  apply (subst Join_commute)
   1.331  apply (blast intro: stable_Join_ensures1)
   1.332  done
   1.333 @@ -344,16 +344,16 @@
   1.334  lemma ok_Join_commute_I: "[| F ok G; (F Join G) ok H |] ==> F ok (G Join H)"
   1.335  by (auto simp add: ok_def)
   1.336  
   1.337 -lemma ok_JN_iff1 [iff]: "F ok (JOIN I G) = (ALL i:I. F ok G i)"
   1.338 +lemma ok_JN_iff1 [iff]: "F ok (JOIN I G) = (\<forall>i \<in> I. F ok G i)"
   1.339  by (auto simp add: ok_def)
   1.340  
   1.341 -lemma ok_JN_iff2 [iff]: "(JOIN I G) ok F =  (ALL i:I. G i ok F)"
   1.342 +lemma ok_JN_iff2 [iff]: "(JOIN I G) ok F =  (\<forall>i \<in> I. G i ok F)"
   1.343  by (auto simp add: ok_def)
   1.344  
   1.345 -lemma OK_iff_ok: "OK I F = (ALL i: I. ALL j: I-{i}. (F i) ok (F j))"
   1.346 +lemma OK_iff_ok: "OK I F = (\<forall>i \<in> I. \<forall>j \<in> I-{i}. (F i) ok (F j))"
   1.347  by (auto simp add: ok_def OK_def)
   1.348  
   1.349 -lemma OK_imp_ok: "[| OK I F; i: I; j: I; i ~= j|] ==> (F i) ok (F j)"
   1.350 +lemma OK_imp_ok: "[| OK I F; i \<in> I; j \<in> I; i \<noteq> j|] ==> (F i) ok (F j)"
   1.351  by (auto simp add: OK_iff_ok)
   1.352  
   1.353  
   1.354 @@ -362,27 +362,27 @@
   1.355  lemma Allowed_SKIP [simp]: "Allowed SKIP = UNIV"
   1.356  by (auto simp add: Allowed_def)
   1.357  
   1.358 -lemma Allowed_Join [simp]: "Allowed (F Join G) = Allowed F Int Allowed G"
   1.359 +lemma Allowed_Join [simp]: "Allowed (F Join G) = Allowed F \<inter> Allowed G"
   1.360  by (auto simp add: Allowed_def)
   1.361  
   1.362 -lemma Allowed_JN [simp]: "Allowed (JOIN I F) = (INT i:I. Allowed (F i))"
   1.363 +lemma Allowed_JN [simp]: "Allowed (JOIN I F) = (\<Inter>i \<in> I. Allowed (F i))"
   1.364  by (auto simp add: Allowed_def)
   1.365  
   1.366 -lemma ok_iff_Allowed: "F ok G = (F : Allowed G & G : Allowed F)"
   1.367 +lemma ok_iff_Allowed: "F ok G = (F \<in> Allowed G & G \<in> Allowed F)"
   1.368  by (simp add: ok_def Allowed_def)
   1.369  
   1.370 -lemma OK_iff_Allowed: "OK I F = (ALL i: I. ALL j: I-{i}. F i : Allowed(F j))"
   1.371 +lemma OK_iff_Allowed: "OK I F = (\<forall>i \<in> I. \<forall>j \<in> I-{i}. F i \<in> Allowed(F j))"
   1.372  by (auto simp add: OK_iff_ok ok_iff_Allowed)
   1.373  
   1.374  subsection{*@{text safety_prop}, for reasoning about
   1.375   given instances of "ok"*}
   1.376  
   1.377  lemma safety_prop_Acts_iff:
   1.378 -     "safety_prop X ==> (Acts G <= insert Id (UNION X Acts)) = (G : X)"
   1.379 +     "safety_prop X ==> (Acts G \<subseteq> insert Id (UNION X Acts)) = (G \<in> X)"
   1.380  by (auto simp add: safety_prop_def)
   1.381  
   1.382  lemma safety_prop_AllowedActs_iff_Allowed:
   1.383 -     "safety_prop X ==> (UNION X Acts <= AllowedActs F) = (X <= Allowed F)"
   1.384 +     "safety_prop X ==> (UNION X Acts \<subseteq> AllowedActs F) = (X \<subseteq> Allowed F)"
   1.385  by (auto simp add: Allowed_def safety_prop_Acts_iff [symmetric])
   1.386  
   1.387  lemma Allowed_eq:
   1.388 @@ -395,27 +395,27 @@
   1.389  by (simp add: Allowed_eq)
   1.390  
   1.391  (*For safety_prop to hold, the property must be satisfiable!*)
   1.392 -lemma safety_prop_constrains [iff]: "safety_prop (A co B) = (A <= B)"
   1.393 +lemma safety_prop_constrains [iff]: "safety_prop (A co B) = (A \<subseteq> B)"
   1.394  by (simp add: safety_prop_def constrains_def, blast)
   1.395  
   1.396  lemma safety_prop_stable [iff]: "safety_prop (stable A)"
   1.397  by (simp add: stable_def)
   1.398  
   1.399  lemma safety_prop_Int [simp]:
   1.400 -     "[| safety_prop X; safety_prop Y |] ==> safety_prop (X Int Y)"
   1.401 +     "[| safety_prop X; safety_prop Y |] ==> safety_prop (X \<inter> Y)"
   1.402  by (simp add: safety_prop_def, blast)
   1.403  
   1.404  lemma safety_prop_INTER1 [simp]:
   1.405 -     "(!!i. safety_prop (X i)) ==> safety_prop (INT i. X i)"
   1.406 +     "(!!i. safety_prop (X i)) ==> safety_prop (\<Inter>i. X i)"
   1.407  by (auto simp add: safety_prop_def, blast)
   1.408  							       
   1.409  lemma safety_prop_INTER [simp]:
   1.410 -     "(!!i. i:I ==> safety_prop (X i)) ==> safety_prop (INT i:I. X i)"
   1.411 +     "(!!i. i \<in> I ==> safety_prop (X i)) ==> safety_prop (\<Inter>i \<in> I. X i)"
   1.412  by (auto simp add: safety_prop_def, blast)
   1.413  
   1.414  lemma def_UNION_ok_iff:
   1.415       "[| F == mk_program(init,acts,UNION X Acts); safety_prop X |]  
   1.416 -      ==> F ok G = (G : X & acts <= AllowedActs G)"
   1.417 +      ==> F ok G = (G \<in> X & acts \<subseteq> AllowedActs G)"
   1.418  by (auto simp add: ok_def safety_prop_Acts_iff)
   1.419  
   1.420  end