src/HOL/UNITY/UNITY.thy
changeset 13805 3786b2fd6808
parent 13798 4c1a53627500
child 13812 91713a1915ee
     1.1 --- a/src/HOL/UNITY/UNITY.thy	Mon Feb 03 11:45:05 2003 +0100
     1.2 +++ b/src/HOL/UNITY/UNITY.thy	Tue Feb 04 18:12:40 2003 +0100
     1.3 @@ -14,15 +14,15 @@
     1.4  
     1.5  typedef (Program)
     1.6    'a program = "{(init:: 'a set, acts :: ('a * 'a)set set,
     1.7 -		   allowed :: ('a * 'a)set set). Id:acts & Id: allowed}" 
     1.8 +		   allowed :: ('a * 'a)set set). Id \<in> acts & Id: allowed}" 
     1.9    by blast
    1.10  
    1.11  constdefs
    1.12    constrains :: "['a set, 'a set] => 'a program set"  (infixl "co"     60)
    1.13 -    "A co B == {F. ALL act: Acts F. act``A <= B}"
    1.14 +    "A co B == {F. \<forall>act \<in> Acts F. act``A \<subseteq> B}"
    1.15  
    1.16    unless  :: "['a set, 'a set] => 'a program set"  (infixl "unless" 60)
    1.17 -    "A unless B == (A-B) co (A Un B)"
    1.18 +    "A unless B == (A-B) co (A \<union> B)"
    1.19  
    1.20    mk_program :: "('a set * ('a * 'a)set set * ('a * 'a)set set)
    1.21  		   => 'a program"
    1.22 @@ -39,20 +39,20 @@
    1.23      "AllowedActs F == (%(init, acts, allowed). allowed) (Rep_Program F)"
    1.24  
    1.25    Allowed :: "'a program => 'a program set"
    1.26 -    "Allowed F == {G. Acts G <= AllowedActs F}"
    1.27 +    "Allowed F == {G. Acts G \<subseteq> AllowedActs F}"
    1.28  
    1.29    stable     :: "'a set => 'a program set"
    1.30      "stable A == A co A"
    1.31  
    1.32    strongest_rhs :: "['a program, 'a set] => 'a set"
    1.33 -    "strongest_rhs F A == Inter {B. F : A co B}"
    1.34 +    "strongest_rhs F A == Inter {B. F \<in> A co B}"
    1.35  
    1.36    invariant :: "'a set => 'a program set"
    1.37 -    "invariant A == {F. Init F <= A} Int stable A"
    1.38 +    "invariant A == {F. Init F \<subseteq> A} \<inter> stable A"
    1.39  
    1.40 -  (*Polymorphic in both states and the meaning of <= *)
    1.41 +  (*Polymorphic in both states and the meaning of \<le> *)
    1.42    increasing :: "['a => 'b::{order}] => 'a program set"
    1.43 -    "increasing f == INT z. stable {s. z <= f s}"
    1.44 +    "increasing f == \<Inter>z. stable {s. z \<le> f s}"
    1.45  
    1.46  
    1.47  (*Perhaps equalities.ML shouldn't add this in the first place!*)
    1.48 @@ -64,7 +64,7 @@
    1.49       Rep_Program Rep_Program_inverse Abs_Program_inverse 
    1.50       Program_def Init_def Acts_def AllowedActs_def mk_program_def
    1.51  
    1.52 -lemma Id_in_Acts [iff]: "Id : Acts F"
    1.53 +lemma Id_in_Acts [iff]: "Id \<in> Acts F"
    1.54  apply (cut_tac x = F in Rep_Program)
    1.55  apply (auto simp add: program_typedef) 
    1.56  done
    1.57 @@ -72,7 +72,7 @@
    1.58  lemma insert_Id_Acts [iff]: "insert Id (Acts F) = Acts F"
    1.59  by (simp add: insert_absorb Id_in_Acts)
    1.60  
    1.61 -lemma Id_in_AllowedActs [iff]: "Id : AllowedActs F"
    1.62 +lemma Id_in_AllowedActs [iff]: "Id \<in> AllowedActs F"
    1.63  apply (cut_tac x = F in Rep_Program)
    1.64  apply (auto simp add: program_typedef) 
    1.65  done
    1.66 @@ -145,114 +145,114 @@
    1.67  
    1.68  (*An action is expanded only if a pair of states is being tested against it*)
    1.69  lemma def_act_simp:
    1.70 -     "[| act == {(s,s'). P s s'} |] ==> ((s,s') : act) = P s s'"
    1.71 +     "[| act == {(s,s'). P s s'} |] ==> ((s,s') \<in> act) = P s s'"
    1.72  by auto
    1.73  
    1.74  (*A set is expanded only if an element is being tested against it*)
    1.75 -lemma def_set_simp: "A == B ==> (x : A) = (x : B)"
    1.76 +lemma def_set_simp: "A == B ==> (x \<in> A) = (x \<in> B)"
    1.77  by auto
    1.78  
    1.79  
    1.80  (*** co ***)
    1.81  
    1.82  lemma constrainsI: 
    1.83 -    "(!!act s s'. [| act: Acts F;  (s,s') : act;  s: A |] ==> s': A')  
    1.84 -     ==> F : A co A'"
    1.85 +    "(!!act s s'. [| act: Acts F;  (s,s') \<in> act;  s \<in> A |] ==> s': A')  
    1.86 +     ==> F \<in> A co A'"
    1.87  by (simp add: constrains_def, blast)
    1.88  
    1.89  lemma constrainsD: 
    1.90 -    "[| F : A co A'; act: Acts F;  (s,s'): act;  s: A |] ==> s': A'"
    1.91 +    "[| F \<in> A co A'; act: Acts F;  (s,s'): act;  s \<in> A |] ==> s': A'"
    1.92  by (unfold constrains_def, blast)
    1.93  
    1.94 -lemma constrains_empty [iff]: "F : {} co B"
    1.95 +lemma constrains_empty [iff]: "F \<in> {} co B"
    1.96  by (unfold constrains_def, blast)
    1.97  
    1.98 -lemma constrains_empty2 [iff]: "(F : A co {}) = (A={})"
    1.99 +lemma constrains_empty2 [iff]: "(F \<in> A co {}) = (A={})"
   1.100  by (unfold constrains_def, blast)
   1.101  
   1.102 -lemma constrains_UNIV [iff]: "(F : UNIV co B) = (B = UNIV)"
   1.103 +lemma constrains_UNIV [iff]: "(F \<in> UNIV co B) = (B = UNIV)"
   1.104  by (unfold constrains_def, blast)
   1.105  
   1.106 -lemma constrains_UNIV2 [iff]: "F : A co UNIV"
   1.107 +lemma constrains_UNIV2 [iff]: "F \<in> A co UNIV"
   1.108  by (unfold constrains_def, blast)
   1.109  
   1.110  (*monotonic in 2nd argument*)
   1.111  lemma constrains_weaken_R: 
   1.112 -    "[| F : A co A'; A'<=B' |] ==> F : A co B'"
   1.113 +    "[| F \<in> A co A'; A'<=B' |] ==> F \<in> A co B'"
   1.114  by (unfold constrains_def, blast)
   1.115  
   1.116  (*anti-monotonic in 1st argument*)
   1.117  lemma constrains_weaken_L: 
   1.118 -    "[| F : A co A'; B<=A |] ==> F : B co A'"
   1.119 +    "[| F \<in> A co A'; B \<subseteq> A |] ==> F \<in> B co A'"
   1.120  by (unfold constrains_def, blast)
   1.121  
   1.122  lemma constrains_weaken: 
   1.123 -   "[| F : A co A'; B<=A; A'<=B' |] ==> F : B co B'"
   1.124 +   "[| F \<in> A co A'; B \<subseteq> A; A'<=B' |] ==> F \<in> B co B'"
   1.125  by (unfold constrains_def, blast)
   1.126  
   1.127  (** Union **)
   1.128  
   1.129  lemma constrains_Un: 
   1.130 -    "[| F : A co A'; F : B co B' |] ==> F : (A Un B) co (A' Un B')"
   1.131 +    "[| F \<in> A co A'; F \<in> B co B' |] ==> F \<in> (A \<union> B) co (A' \<union> B')"
   1.132  by (unfold constrains_def, blast)
   1.133  
   1.134  lemma constrains_UN: 
   1.135 -    "(!!i. i:I ==> F : (A i) co (A' i)) 
   1.136 -     ==> F : (UN i:I. A i) co (UN i:I. A' i)"
   1.137 +    "(!!i. i \<in> I ==> F \<in> (A i) co (A' i)) 
   1.138 +     ==> F \<in> (\<Union>i \<in> I. A i) co (\<Union>i \<in> I. A' i)"
   1.139  by (unfold constrains_def, blast)
   1.140  
   1.141 -lemma constrains_Un_distrib: "(A Un B) co C = (A co C) Int (B co C)"
   1.142 +lemma constrains_Un_distrib: "(A \<union> B) co C = (A co C) \<inter> (B co C)"
   1.143  by (unfold constrains_def, blast)
   1.144  
   1.145 -lemma constrains_UN_distrib: "(UN i:I. A i) co B = (INT i:I. A i co B)"
   1.146 +lemma constrains_UN_distrib: "(\<Union>i \<in> I. A i) co B = (\<Inter>i \<in> I. A i co B)"
   1.147  by (unfold constrains_def, blast)
   1.148  
   1.149 -lemma constrains_Int_distrib: "C co (A Int B) = (C co A) Int (C co B)"
   1.150 +lemma constrains_Int_distrib: "C co (A \<inter> B) = (C co A) \<inter> (C co B)"
   1.151  by (unfold constrains_def, blast)
   1.152  
   1.153 -lemma constrains_INT_distrib: "A co (INT i:I. B i) = (INT i:I. A co B i)"
   1.154 +lemma constrains_INT_distrib: "A co (\<Inter>i \<in> I. B i) = (\<Inter>i \<in> I. A co B i)"
   1.155  by (unfold constrains_def, blast)
   1.156  
   1.157  (** Intersection **)
   1.158  
   1.159  lemma constrains_Int: 
   1.160 -    "[| F : A co A'; F : B co B' |] ==> F : (A Int B) co (A' Int B')"
   1.161 +    "[| F \<in> A co A'; F \<in> B co B' |] ==> F \<in> (A \<inter> B) co (A' \<inter> B')"
   1.162  by (unfold constrains_def, blast)
   1.163  
   1.164  lemma constrains_INT: 
   1.165 -    "(!!i. i:I ==> F : (A i) co (A' i)) 
   1.166 -     ==> F : (INT i:I. A i) co (INT i:I. A' i)"
   1.167 +    "(!!i. i \<in> I ==> F \<in> (A i) co (A' i)) 
   1.168 +     ==> F \<in> (\<Inter>i \<in> I. A i) co (\<Inter>i \<in> I. A' i)"
   1.169  by (unfold constrains_def, blast)
   1.170  
   1.171 -lemma constrains_imp_subset: "F : A co A' ==> A <= A'"
   1.172 +lemma constrains_imp_subset: "F \<in> A co A' ==> A \<subseteq> A'"
   1.173  by (unfold constrains_def, auto)
   1.174  
   1.175  (*The reasoning is by subsets since "co" refers to single actions
   1.176    only.  So this rule isn't that useful.*)
   1.177  lemma constrains_trans: 
   1.178 -    "[| F : A co B; F : B co C |] ==> F : A co C"
   1.179 +    "[| F \<in> A co B; F \<in> B co C |] ==> F \<in> A co C"
   1.180  by (unfold constrains_def, blast)
   1.181  
   1.182  lemma constrains_cancel: 
   1.183 -   "[| F : A co (A' Un B); F : B co B' |] ==> F : A co (A' Un B')"
   1.184 +   "[| F \<in> A co (A' \<union> B); F \<in> B co B' |] ==> F \<in> A co (A' \<union> B')"
   1.185  by (unfold constrains_def, clarify, blast)
   1.186  
   1.187  
   1.188  (*** unless ***)
   1.189  
   1.190 -lemma unlessI: "F : (A-B) co (A Un B) ==> F : A unless B"
   1.191 +lemma unlessI: "F \<in> (A-B) co (A \<union> B) ==> F \<in> A unless B"
   1.192  by (unfold unless_def, assumption)
   1.193  
   1.194 -lemma unlessD: "F : A unless B ==> F : (A-B) co (A Un B)"
   1.195 +lemma unlessD: "F \<in> A unless B ==> F \<in> (A-B) co (A \<union> B)"
   1.196  by (unfold unless_def, assumption)
   1.197  
   1.198  
   1.199  (*** stable ***)
   1.200  
   1.201 -lemma stableI: "F : A co A ==> F : stable A"
   1.202 +lemma stableI: "F \<in> A co A ==> F \<in> stable A"
   1.203  by (unfold stable_def, assumption)
   1.204  
   1.205 -lemma stableD: "F : stable A ==> F : A co A"
   1.206 +lemma stableD: "F \<in> stable A ==> F \<in> A co A"
   1.207  by (unfold stable_def, assumption)
   1.208  
   1.209  lemma stable_UNIV [simp]: "stable UNIV = UNIV"
   1.210 @@ -261,14 +261,14 @@
   1.211  (** Union **)
   1.212  
   1.213  lemma stable_Un: 
   1.214 -    "[| F : stable A; F : stable A' |] ==> F : stable (A Un A')"
   1.215 +    "[| F \<in> stable A; F \<in> stable A' |] ==> F \<in> stable (A \<union> A')"
   1.216  
   1.217  apply (unfold stable_def)
   1.218  apply (blast intro: constrains_Un)
   1.219  done
   1.220  
   1.221  lemma stable_UN: 
   1.222 -    "(!!i. i:I ==> F : stable (A i)) ==> F : stable (UN i:I. A i)"
   1.223 +    "(!!i. i \<in> I ==> F \<in> stable (A i)) ==> F \<in> stable (\<Union>i \<in> I. A i)"
   1.224  apply (unfold stable_def)
   1.225  apply (blast intro: constrains_UN)
   1.226  done
   1.227 @@ -276,75 +276,75 @@
   1.228  (** Intersection **)
   1.229  
   1.230  lemma stable_Int: 
   1.231 -    "[| F : stable A;  F : stable A' |] ==> F : stable (A Int A')"
   1.232 +    "[| F \<in> stable A;  F \<in> stable A' |] ==> F \<in> stable (A \<inter> A')"
   1.233  apply (unfold stable_def)
   1.234  apply (blast intro: constrains_Int)
   1.235  done
   1.236  
   1.237  lemma stable_INT: 
   1.238 -    "(!!i. i:I ==> F : stable (A i)) ==> F : stable (INT i:I. A i)"
   1.239 +    "(!!i. i \<in> I ==> F \<in> stable (A i)) ==> F \<in> stable (\<Inter>i \<in> I. A i)"
   1.240  apply (unfold stable_def)
   1.241  apply (blast intro: constrains_INT)
   1.242  done
   1.243  
   1.244  lemma stable_constrains_Un: 
   1.245 -    "[| F : stable C; F : A co (C Un A') |] ==> F : (C Un A) co (C Un A')"
   1.246 +    "[| F \<in> stable C; F \<in> A co (C \<union> A') |] ==> F \<in> (C \<union> A) co (C \<union> A')"
   1.247  by (unfold stable_def constrains_def, blast)
   1.248  
   1.249  lemma stable_constrains_Int: 
   1.250 -  "[| F : stable C; F :  (C Int A) co A' |] ==> F : (C Int A) co (C Int A')"
   1.251 +  "[| F \<in> stable C; F \<in>  (C \<inter> A) co A' |] ==> F \<in> (C \<inter> A) co (C \<inter> A')"
   1.252  by (unfold stable_def constrains_def, blast)
   1.253  
   1.254 -(*[| F : stable C; F :  (C Int A) co A |] ==> F : stable (C Int A) *)
   1.255 +(*[| F \<in> stable C; F \<in>  (C \<inter> A) co A |] ==> F \<in> stable (C \<inter> A) *)
   1.256  lemmas stable_constrains_stable = stable_constrains_Int [THEN stableI, standard]
   1.257  
   1.258  
   1.259  (*** invariant ***)
   1.260  
   1.261 -lemma invariantI: "[| Init F<=A;  F: stable A |] ==> F : invariant A"
   1.262 +lemma invariantI: "[| Init F \<subseteq> A;  F \<in> stable A |] ==> F \<in> invariant A"
   1.263  by (simp add: invariant_def)
   1.264  
   1.265 -(*Could also say "invariant A Int invariant B <= invariant (A Int B)"*)
   1.266 +(*Could also say "invariant A \<inter> invariant B \<subseteq> invariant (A \<inter> B)"*)
   1.267  lemma invariant_Int:
   1.268 -     "[| F : invariant A;  F : invariant B |] ==> F : invariant (A Int B)"
   1.269 +     "[| F \<in> invariant A;  F \<in> invariant B |] ==> F \<in> invariant (A \<inter> B)"
   1.270  by (auto simp add: invariant_def stable_Int)
   1.271  
   1.272  
   1.273  (*** increasing ***)
   1.274  
   1.275  lemma increasingD: 
   1.276 -     "F : increasing f ==> F : stable {s. z <= f s}"
   1.277 +     "F \<in> increasing f ==> F \<in> stable {s. z \<subseteq> f s}"
   1.278  
   1.279  by (unfold increasing_def, blast)
   1.280  
   1.281 -lemma increasing_constant [iff]: "F : increasing (%s. c)"
   1.282 +lemma increasing_constant [iff]: "F \<in> increasing (%s. c)"
   1.283  by (unfold increasing_def stable_def, auto)
   1.284  
   1.285  lemma mono_increasing_o: 
   1.286 -     "mono g ==> increasing f <= increasing (g o f)"
   1.287 +     "mono g ==> increasing f \<subseteq> increasing (g o f)"
   1.288  apply (unfold increasing_def stable_def constrains_def, auto)
   1.289  apply (blast intro: monoD order_trans)
   1.290  done
   1.291  
   1.292 -(*Holds by the theorem (Suc m <= n) = (m < n) *)
   1.293 +(*Holds by the theorem (Suc m \<subseteq> n) = (m < n) *)
   1.294  lemma strict_increasingD: 
   1.295 -     "!!z::nat. F : increasing f ==> F: stable {s. z < f s}"
   1.296 +     "!!z::nat. F \<in> increasing f ==> F \<in> stable {s. z < f s}"
   1.297  by (simp add: increasing_def Suc_le_eq [symmetric])
   1.298  
   1.299  
   1.300  (** The Elimination Theorem.  The "free" m has become universally quantified!
   1.301 -    Should the premise be !!m instead of ALL m ?  Would make it harder to use
   1.302 +    Should the premise be !!m instead of \<forall>m ?  Would make it harder to use
   1.303      in forward proof. **)
   1.304  
   1.305  lemma elimination: 
   1.306 -    "[| ALL m:M. F : {s. s x = m} co (B m) |]  
   1.307 -     ==> F : {s. s x : M} co (UN m:M. B m)"
   1.308 +    "[| \<forall>m \<in> M. F \<in> {s. s x = m} co (B m) |]  
   1.309 +     ==> F \<in> {s. s x \<in> M} co (\<Union>m \<in> M. B m)"
   1.310  by (unfold constrains_def, blast)
   1.311  
   1.312  (*As above, but for the trivial case of a one-variable state, in which the
   1.313    state is identified with its one variable.*)
   1.314  lemma elimination_sing: 
   1.315 -    "(ALL m:M. F : {m} co (B m)) ==> F : M co (UN m:M. B m)"
   1.316 +    "(\<forall>m \<in> M. F \<in> {m} co (B m)) ==> F \<in> M co (\<Union>m \<in> M. B m)"
   1.317  by (unfold constrains_def, blast)
   1.318  
   1.319  
   1.320 @@ -352,20 +352,20 @@
   1.321  (*** Theoretical Results from Section 6 ***)
   1.322  
   1.323  lemma constrains_strongest_rhs: 
   1.324 -    "F : A co (strongest_rhs F A )"
   1.325 +    "F \<in> A co (strongest_rhs F A )"
   1.326  by (unfold constrains_def strongest_rhs_def, blast)
   1.327  
   1.328  lemma strongest_rhs_is_strongest: 
   1.329 -    "F : A co B ==> strongest_rhs F A <= B"
   1.330 +    "F \<in> A co B ==> strongest_rhs F A \<subseteq> B"
   1.331  by (unfold constrains_def strongest_rhs_def, blast)
   1.332  
   1.333  
   1.334  (** Ad-hoc set-theory rules **)
   1.335  
   1.336 -lemma Un_Diff_Diff [simp]: "A Un B - (A - B) = B"
   1.337 +lemma Un_Diff_Diff [simp]: "A \<union> B - (A - B) = B"
   1.338  by blast
   1.339  
   1.340 -lemma Int_Union_Union: "Union(B) Int A = Union((%C. C Int A)`B)"
   1.341 +lemma Int_Union_Union: "Union(B) \<inter> A = Union((%C. C \<inter> A)`B)"
   1.342  by blast
   1.343  
   1.344  (** Needed for WF reasoning in WFair.ML **)