src/HOL/UNITY/Comp.thy
changeset 13805 3786b2fd6808
parent 13798 4c1a53627500
child 13812 91713a1915ee
     1.1 --- a/src/HOL/UNITY/Comp.thy	Mon Feb 03 11:45:05 2003 +0100
     1.2 +++ b/src/HOL/UNITY/Comp.thy	Tue Feb 04 18:12:40 2003 +0100
     1.3 @@ -9,7 +9,7 @@
     1.4  
     1.5  Revised by Sidi Ehmety on January  2001 
     1.6  
     1.7 -Added: a strong form of the <= relation (component_of) and localize 
     1.8 +Added: a strong form of the \<subseteq> relation (component_of) and localize 
     1.9  
    1.10  *)
    1.11  
    1.12 @@ -20,33 +20,32 @@
    1.13  instance program :: (type) ord ..
    1.14  
    1.15  defs
    1.16 -  component_def:          "F <= H == EX G. F Join G = H"
    1.17 -  strict_component_def:   "(F < (H::'a program)) == (F <= H & F ~= H)"
    1.18 +  component_def:          "F \<le> H == \<exists>G. F Join G = H"
    1.19 +  strict_component_def:   "(F < (H::'a program)) == (F \<le> H & F \<noteq> H)"
    1.20  
    1.21  
    1.22  constdefs
    1.23 -  component_of :: "'a program=>'a program=> bool"
    1.24 +  component_of :: "'a program =>'a program=> bool"
    1.25                                      (infixl "component'_of" 50)
    1.26 -  "F component_of H == EX G. F ok G & F Join G = H"
    1.27 +  "F component_of H == \<exists>G. F ok G & F Join G = H"
    1.28  
    1.29    strict_component_of :: "'a program\<Rightarrow>'a program=> bool"
    1.30                                      (infixl "strict'_component'_of" 50)
    1.31 -  "F strict_component_of H == F component_of H & F~=H"
    1.32 +  "F strict_component_of H == F component_of H & F\<noteq>H"
    1.33    
    1.34    preserves :: "('a=>'b) => 'a program set"
    1.35 -    "preserves v == INT z. stable {s. v s = z}"
    1.36 +    "preserves v == \<Inter>z. stable {s. v s = z}"
    1.37  
    1.38    localize  :: "('a=>'b) => 'a program => 'a program"
    1.39    "localize v F == mk_program(Init F, Acts F,
    1.40 -			      AllowedActs F Int (UN G:preserves v. Acts G))"
    1.41 +			      AllowedActs F \<inter> (\<Union>G \<in> preserves v. Acts G))"
    1.42  
    1.43    funPair      :: "['a => 'b, 'a => 'c, 'a] => 'b * 'c"
    1.44    "funPair f g == %x. (f x, g x)"
    1.45  
    1.46  
    1.47  subsection{*The component relation*}
    1.48 -lemma componentI: 
    1.49 -     "H <= F | H <= G ==> H <= (F Join G)"
    1.50 +lemma componentI: "H \<le> F | H \<le> G ==> H \<le> (F Join G)"
    1.51  apply (unfold component_def, auto)
    1.52  apply (rule_tac x = "G Join Ga" in exI)
    1.53  apply (rule_tac [2] x = "G Join F" in exI)
    1.54 @@ -54,61 +53,61 @@
    1.55  done
    1.56  
    1.57  lemma component_eq_subset: 
    1.58 -     "(F <= G) =  
    1.59 -      (Init G <= Init F & Acts F <= Acts G & AllowedActs G <= AllowedActs F)"
    1.60 +     "(F \<le> G) =  
    1.61 +      (Init G \<subseteq> Init F & Acts F \<subseteq> Acts G & AllowedActs G \<subseteq> AllowedActs F)"
    1.62  apply (unfold component_def)
    1.63  apply (force intro!: exI program_equalityI)
    1.64  done
    1.65  
    1.66 -lemma component_SKIP [iff]: "SKIP <= F"
    1.67 +lemma component_SKIP [iff]: "SKIP \<le> F"
    1.68  apply (unfold component_def)
    1.69  apply (force intro: Join_SKIP_left)
    1.70  done
    1.71  
    1.72 -lemma component_refl [iff]: "F <= (F :: 'a program)"
    1.73 +lemma component_refl [iff]: "F \<le> (F :: 'a program)"
    1.74  apply (unfold component_def)
    1.75  apply (blast intro: Join_SKIP_right)
    1.76  done
    1.77  
    1.78 -lemma SKIP_minimal: "F <= SKIP ==> F = SKIP"
    1.79 +lemma SKIP_minimal: "F \<le> SKIP ==> F = SKIP"
    1.80  by (auto intro!: program_equalityI simp add: component_eq_subset)
    1.81  
    1.82 -lemma component_Join1: "F <= (F Join G)"
    1.83 +lemma component_Join1: "F \<le> (F Join G)"
    1.84  by (unfold component_def, blast)
    1.85  
    1.86 -lemma component_Join2: "G <= (F Join G)"
    1.87 +lemma component_Join2: "G \<le> (F Join G)"
    1.88  apply (unfold component_def)
    1.89  apply (simp add: Join_commute, blast)
    1.90  done
    1.91  
    1.92 -lemma Join_absorb1: "F<=G ==> F Join G = G"
    1.93 +lemma Join_absorb1: "F \<le> G ==> F Join G = G"
    1.94  by (auto simp add: component_def Join_left_absorb)
    1.95  
    1.96 -lemma Join_absorb2: "G<=F ==> F Join G = F"
    1.97 +lemma Join_absorb2: "G \<le> F ==> F Join G = F"
    1.98  by (auto simp add: Join_ac component_def)
    1.99  
   1.100 -lemma JN_component_iff: "((JOIN I F) <= H) = (ALL i: I. F i <= H)"
   1.101 +lemma JN_component_iff: "((JOIN I F) \<le> H) = (\<forall>i \<in> I. F i \<le> H)"
   1.102  by (simp add: component_eq_subset, blast)
   1.103  
   1.104 -lemma component_JN: "i : I ==> (F i) <= (JN i:I. (F i))"
   1.105 +lemma component_JN: "i \<in> I ==> (F i) \<le> (\<Squnion>i \<in> I. (F i))"
   1.106  apply (unfold component_def)
   1.107  apply (blast intro: JN_absorb)
   1.108  done
   1.109  
   1.110 -lemma component_trans: "[| F <= G; G <= H |] ==> F <= (H :: 'a program)"
   1.111 +lemma component_trans: "[| F \<le> G; G \<le> H |] ==> F \<le> (H :: 'a program)"
   1.112  apply (unfold component_def)
   1.113  apply (blast intro: Join_assoc [symmetric])
   1.114  done
   1.115  
   1.116 -lemma component_antisym: "[| F <= G; G <= F |] ==> F = (G :: 'a program)"
   1.117 +lemma component_antisym: "[| F \<le> G; G \<le> F |] ==> F = (G :: 'a program)"
   1.118  apply (simp (no_asm_use) add: component_eq_subset)
   1.119  apply (blast intro!: program_equalityI)
   1.120  done
   1.121  
   1.122 -lemma Join_component_iff: "((F Join G) <= H) = (F <= H & G <= H)"
   1.123 +lemma Join_component_iff: "((F Join G) \<le> H) = (F \<le> H & G \<le> H)"
   1.124  by (simp add: component_eq_subset, blast)
   1.125  
   1.126 -lemma component_constrains: "[| F <= G; G : A co B |] ==> F : A co B"
   1.127 +lemma component_constrains: "[| F \<le> G; G \<in> A co B |] ==> F \<in> A co B"
   1.128  by (auto simp add: constrains_def component_eq_subset)
   1.129  
   1.130  (*Used in Guar.thy to show that programs are partially ordered*)
   1.131 @@ -117,34 +116,34 @@
   1.132  
   1.133  subsection{*The preserves property*}
   1.134  
   1.135 -lemma preservesI: "(!!z. F : stable {s. v s = z}) ==> F : preserves v"
   1.136 +lemma preservesI: "(!!z. F \<in> stable {s. v s = z}) ==> F \<in> preserves v"
   1.137  by (unfold preserves_def, blast)
   1.138  
   1.139  lemma preserves_imp_eq: 
   1.140 -     "[| F : preserves v;  act : Acts F;  (s,s') : act |] ==> v s = v s'"
   1.141 +     "[| F \<in> preserves v;  act \<in> Acts F;  (s,s') \<in> act |] ==> v s = v s'"
   1.142  apply (unfold preserves_def stable_def constrains_def, force)
   1.143  done
   1.144  
   1.145  lemma Join_preserves [iff]: 
   1.146 -     "(F Join G : preserves v) = (F : preserves v & G : preserves v)"
   1.147 +     "(F Join G \<in> preserves v) = (F \<in> preserves v & G \<in> preserves v)"
   1.148  apply (unfold preserves_def, auto)
   1.149  done
   1.150  
   1.151  lemma JN_preserves [iff]:
   1.152 -     "(JOIN I F : preserves v) = (ALL i:I. F i : preserves v)"
   1.153 +     "(JOIN I F \<in> preserves v) = (\<forall>i \<in> I. F i \<in> preserves v)"
   1.154  apply (simp add: JN_stable preserves_def, blast)
   1.155  done
   1.156  
   1.157 -lemma SKIP_preserves [iff]: "SKIP : preserves v"
   1.158 +lemma SKIP_preserves [iff]: "SKIP \<in> preserves v"
   1.159  by (auto simp add: preserves_def)
   1.160  
   1.161  lemma funPair_apply [simp]: "(funPair f g) x = (f x, g x)"
   1.162  by (simp add:  funPair_def)
   1.163  
   1.164 -lemma preserves_funPair: "preserves (funPair v w) = preserves v Int preserves w"
   1.165 +lemma preserves_funPair: "preserves (funPair v w) = preserves v \<inter> preserves w"
   1.166  by (auto simp add: preserves_def stable_def constrains_def, blast)
   1.167  
   1.168 -(* (F : preserves (funPair v w)) = (F : preserves v Int preserves w) *)
   1.169 +(* (F \<in> preserves (funPair v w)) = (F \<in> preserves v \<inter> preserves w) *)
   1.170  declare preserves_funPair [THEN eqset_imp_iff, iff]
   1.171  
   1.172  
   1.173 @@ -157,20 +156,20 @@
   1.174  lemma snd_o_funPair [simp]: "snd o (funPair f g) = g"
   1.175  by (simp add: funPair_def o_def)
   1.176  
   1.177 -lemma subset_preserves_o: "preserves v <= preserves (w o v)"
   1.178 +lemma subset_preserves_o: "preserves v \<subseteq> preserves (w o v)"
   1.179  by (force simp add: preserves_def stable_def constrains_def)
   1.180  
   1.181 -lemma preserves_subset_stable: "preserves v <= stable {s. P (v s)}"
   1.182 +lemma preserves_subset_stable: "preserves v \<subseteq> stable {s. P (v s)}"
   1.183  apply (auto simp add: preserves_def stable_def constrains_def)
   1.184  apply (rename_tac s' s)
   1.185  apply (subgoal_tac "v s = v s'")
   1.186  apply (force+)
   1.187  done
   1.188  
   1.189 -lemma preserves_subset_increasing: "preserves v <= increasing v"
   1.190 +lemma preserves_subset_increasing: "preserves v \<subseteq> increasing v"
   1.191  by (auto simp add: preserves_subset_stable [THEN subsetD] increasing_def)
   1.192  
   1.193 -lemma preserves_id_subset_stable: "preserves id <= stable A"
   1.194 +lemma preserves_id_subset_stable: "preserves id \<subseteq> stable A"
   1.195  by (force simp add: preserves_def stable_def constrains_def)
   1.196  
   1.197  
   1.198 @@ -183,27 +182,27 @@
   1.199  (** Some lemmas used only in Client.ML **)
   1.200  
   1.201  lemma stable_localTo_stable2:
   1.202 -     "[| F : stable {s. P (v s) (w s)};    
   1.203 -         G : preserves v;  G : preserves w |]                
   1.204 -      ==> F Join G : stable {s. P (v s) (w s)}"
   1.205 -apply (simp (no_asm_simp))
   1.206 -apply (subgoal_tac "G: preserves (funPair v w) ")
   1.207 +     "[| F \<in> stable {s. P (v s) (w s)};    
   1.208 +         G \<in> preserves v;  G \<in> preserves w |]                
   1.209 +      ==> F Join G \<in> stable {s. P (v s) (w s)}"
   1.210 +apply (simp)
   1.211 +apply (subgoal_tac "G \<in> preserves (funPair v w) ")
   1.212   prefer 2 apply simp 
   1.213 -apply (drule_tac P1 = "split ?Q" in  preserves_subset_stable [THEN subsetD], auto)
   1.214 +apply (drule_tac P1 = "split ?Q" in preserves_subset_stable [THEN subsetD], auto)
   1.215  done
   1.216  
   1.217  lemma Increasing_preserves_Stable:
   1.218 -     "[| F : stable {s. v s <= w s};  G : preserves v;        
   1.219 -         F Join G : Increasing w |]                
   1.220 -      ==> F Join G : Stable {s. v s <= w s}"
   1.221 +     "[| F \<in> stable {s. v s \<le> w s};  G \<in> preserves v;        
   1.222 +         F Join G \<in> Increasing w |]                
   1.223 +      ==> F Join G \<in> Stable {s. v s \<le> w s}"
   1.224  apply (auto simp add: stable_def Stable_def Increasing_def Constrains_def all_conj_distrib)
   1.225  apply (blast intro: constrains_weaken)
   1.226  (*The G case remains*)
   1.227  apply (auto simp add: preserves_def stable_def constrains_def)
   1.228  apply (case_tac "act: Acts F", blast)
   1.229  (*We have a G-action, so delete assumptions about F-actions*)
   1.230 -apply (erule_tac V = "ALL act:Acts F. ?P act" in thin_rl)
   1.231 -apply (erule_tac V = "ALL z. ALL act:Acts F. ?P z act" in thin_rl)
   1.232 +apply (erule_tac V = "\<forall>act \<in> Acts F. ?P act" in thin_rl)
   1.233 +apply (erule_tac V = "\<forall>z. \<forall>act \<in> Acts F. ?P z act" in thin_rl)
   1.234  apply (subgoal_tac "v x = v xa")
   1.235  prefer 2 apply blast
   1.236  apply auto
   1.237 @@ -212,12 +211,12 @@
   1.238  
   1.239  (** component_of **)
   1.240  
   1.241 -(*  component_of is stronger than <= *)
   1.242 -lemma component_of_imp_component: "F component_of H ==> F <= H"
   1.243 +(*  component_of is stronger than \<le> *)
   1.244 +lemma component_of_imp_component: "F component_of H ==> F \<le> H"
   1.245  by (unfold component_def component_of_def, blast)
   1.246  
   1.247  
   1.248 -(* component_of satisfies many of the <='s properties *)
   1.249 +(* component_of satisfies many of the same properties as \<le> *)
   1.250  lemma component_of_refl [simp]: "F component_of F"
   1.251  apply (unfold component_of_def)
   1.252  apply (rule_tac x = SKIP in exI, auto)
   1.253 @@ -243,7 +242,7 @@
   1.254  by (simp add: localize_def)
   1.255  
   1.256  lemma localize_AllowedActs_eq [simp]: 
   1.257 - "AllowedActs (localize v F) = AllowedActs F Int (UN G:(preserves v). Acts G)"
   1.258 + "AllowedActs (localize v F) = AllowedActs F \<inter> (\<Union>G \<in> preserves v. Acts G)"
   1.259  by (unfold localize_def, auto)
   1.260  
   1.261  end