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