src/HOL/UNITY/Constrains.thy
changeset 13797 baefae13ad37
parent 6823 97babc436a41
child 13798 4c1a53627500
     1.1 --- a/src/HOL/UNITY/Constrains.thy	Thu Jan 30 10:35:56 2003 +0100
     1.2 +++ b/src/HOL/UNITY/Constrains.thy	Thu Jan 30 18:08:09 2003 +0100
     1.3 @@ -3,10 +3,10 @@
     1.4      Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.5      Copyright   1998  University of Cambridge
     1.6  
     1.7 -Safety relations: restricted to the set of reachable states.
     1.8 +Weak safety relations: restricted to the set of reachable states.
     1.9  *)
    1.10  
    1.11 -Constrains = UNITY + 
    1.12 +theory Constrains = UNITY:
    1.13  
    1.14  consts traces :: "['a set, ('a * 'a)set set] => ('a * 'a list) set"
    1.15  
    1.16 @@ -14,36 +14,30 @@
    1.17      Arguments MUST be curried in an inductive definition*)
    1.18  
    1.19  inductive "traces init acts"  
    1.20 -  intrs 
    1.21 +  intros 
    1.22           (*Initial trace is empty*)
    1.23 -    Init  "s: init ==> (s,[]) : traces init acts"
    1.24 +    Init:  "s: init ==> (s,[]) : traces init acts"
    1.25  
    1.26 -    Acts  "[| act: acts;  (s,evs) : traces init acts;  (s,s'): act |]
    1.27 -	   ==> (s', s#evs) : traces init acts"
    1.28 +    Acts:  "[| act: acts;  (s,evs) : traces init acts;  (s,s'): act |]
    1.29 +	    ==> (s', s#evs) : traces init acts"
    1.30  
    1.31  
    1.32  consts reachable :: "'a program => 'a set"
    1.33  
    1.34  inductive "reachable F"
    1.35 -  intrs 
    1.36 -    Init  "s: Init F ==> s : reachable F"
    1.37 -
    1.38 -    Acts  "[| act: Acts F;  s : reachable F;  (s,s'): act |]
    1.39 -	   ==> s' : reachable F"
    1.40 +  intros 
    1.41 +    Init:  "s: Init F ==> s : reachable F"
    1.42  
    1.43 -consts
    1.44 -  Constrains :: "['a set, 'a set] => 'a program set"  (infixl "Co"     60)
    1.45 -  op_Unless  :: "['a set, 'a set] => 'a program set"  (infixl "Unless" 60)
    1.46 +    Acts:  "[| act: Acts F;  s : reachable F;  (s,s'): act |]
    1.47 +	    ==> s' : reachable F"
    1.48  
    1.49 -defs
    1.50 -  Constrains_def
    1.51 +constdefs
    1.52 +  Constrains :: "['a set, 'a set] => 'a program set"  (infixl "Co" 60)
    1.53      "A Co B == {F. F : (reachable F Int A)  co  B}"
    1.54  
    1.55 -  Unless_def
    1.56 +  Unless  :: "['a set, 'a set] => 'a program set"     (infixl "Unless" 60)
    1.57      "A Unless B == (A-B) Co (A Un B)"
    1.58  
    1.59 -constdefs
    1.60 -
    1.61    Stable     :: "'a set => 'a program set"
    1.62      "Stable A == A Co A"
    1.63  
    1.64 @@ -55,4 +49,345 @@
    1.65    Increasing :: "['a => 'b::{order}] => 'a program set"
    1.66      "Increasing f == INT z. Stable {s. z <= f s}"
    1.67  
    1.68 +
    1.69 +(*** traces and reachable ***)
    1.70 +
    1.71 +lemma reachable_equiv_traces:
    1.72 +     "reachable F = {s. EX evs. (s,evs): traces (Init F) (Acts F)}"
    1.73 +apply safe
    1.74 +apply (erule_tac [2] traces.induct)
    1.75 +apply (erule reachable.induct)
    1.76 +apply (blast intro: reachable.intros traces.intros)+
    1.77 +done
    1.78 +
    1.79 +lemma Init_subset_reachable: "Init F <= reachable F"
    1.80 +by (blast intro: reachable.intros)
    1.81 +
    1.82 +lemma stable_reachable [intro!,simp]:
    1.83 +     "Acts G <= Acts F ==> G : stable (reachable F)"
    1.84 +by (blast intro: stableI constrainsI reachable.intros)
    1.85 +
    1.86 +(*The set of all reachable states is an invariant...*)
    1.87 +lemma invariant_reachable: "F : invariant (reachable F)"
    1.88 +apply (simp add: invariant_def)
    1.89 +apply (blast intro: reachable.intros)
    1.90 +done
    1.91 +
    1.92 +(*...in fact the strongest invariant!*)
    1.93 +lemma invariant_includes_reachable: "F : invariant A ==> reachable F <= A"
    1.94 +apply (simp add: stable_def constrains_def invariant_def)
    1.95 +apply (rule subsetI)
    1.96 +apply (erule reachable.induct)
    1.97 +apply (blast intro: reachable.intros)+
    1.98 +done
    1.99 +
   1.100 +
   1.101 +(*** Co ***)
   1.102 +
   1.103 +(*F : B co B' ==> F : (reachable F Int B) co (reachable F Int B')*)
   1.104 +lemmas constrains_reachable_Int =  
   1.105 +    subset_refl [THEN stable_reachable [unfolded stable_def], 
   1.106 +                 THEN constrains_Int, standard]
   1.107 +
   1.108 +(*Resembles the previous definition of Constrains*)
   1.109 +lemma Constrains_eq_constrains: 
   1.110 +     "A Co B = {F. F : (reachable F  Int  A) co (reachable F  Int  B)}"
   1.111 +apply (unfold Constrains_def)
   1.112 +apply (blast dest: constrains_reachable_Int intro: constrains_weaken)
   1.113 +done
   1.114 +
   1.115 +lemma constrains_imp_Constrains: "F : A co A' ==> F : A Co A'"
   1.116 +apply (unfold Constrains_def)
   1.117 +apply (blast intro: constrains_weaken_L)
   1.118 +done
   1.119 +
   1.120 +lemma stable_imp_Stable: "F : stable A ==> F : Stable A"
   1.121 +apply (unfold stable_def Stable_def)
   1.122 +apply (erule constrains_imp_Constrains)
   1.123 +done
   1.124 +
   1.125 +lemma ConstrainsI: 
   1.126 +    "(!!act s s'. [| act: Acts F;  (s,s') : act;  s: A |] ==> s': A')  
   1.127 +     ==> F : A Co A'"
   1.128 +apply (rule constrains_imp_Constrains)
   1.129 +apply (blast intro: constrainsI)
   1.130 +done
   1.131 +
   1.132 +lemma Constrains_empty [iff]: "F : {} Co B"
   1.133 +by (unfold Constrains_def constrains_def, blast)
   1.134 +
   1.135 +lemma Constrains_UNIV [iff]: "F : A Co UNIV"
   1.136 +by (blast intro: ConstrainsI)
   1.137 +
   1.138 +lemma Constrains_weaken_R: 
   1.139 +    "[| F : A Co A'; A'<=B' |] ==> F : A Co B'"
   1.140 +apply (unfold Constrains_def)
   1.141 +apply (blast intro: constrains_weaken_R)
   1.142 +done
   1.143 +
   1.144 +lemma Constrains_weaken_L: 
   1.145 +    "[| F : A Co A'; B<=A |] ==> F : B Co A'"
   1.146 +apply (unfold Constrains_def)
   1.147 +apply (blast intro: constrains_weaken_L)
   1.148 +done
   1.149 +
   1.150 +lemma Constrains_weaken: 
   1.151 +   "[| F : A Co A'; B<=A; A'<=B' |] ==> F : B Co B'"
   1.152 +apply (unfold Constrains_def)
   1.153 +apply (blast intro: constrains_weaken)
   1.154 +done
   1.155 +
   1.156 +(** Union **)
   1.157 +
   1.158 +lemma Constrains_Un: 
   1.159 +    "[| F : A Co A'; F : B Co B' |] ==> F : (A Un B) Co (A' Un B')"
   1.160 +apply (unfold Constrains_def)
   1.161 +apply (blast intro: constrains_Un [THEN constrains_weaken])
   1.162 +done
   1.163 +
   1.164 +lemma Constrains_UN: 
   1.165 +  assumes Co: "!!i. i:I ==> F : (A i) Co (A' i)"
   1.166 +  shows "F : (UN i:I. A i) Co (UN i:I. A' i)"
   1.167 +apply (unfold Constrains_def)
   1.168 +apply (rule CollectI)
   1.169 +apply (rule Co [unfolded Constrains_def, THEN CollectD, THEN constrains_UN, 
   1.170 +                THEN constrains_weaken],   auto)
   1.171 +done
   1.172 +
   1.173 +(** Intersection **)
   1.174 +
   1.175 +lemma Constrains_Int: 
   1.176 +    "[| F : A Co A'; F : B Co B' |] ==> F : (A Int B) Co (A' Int B')"
   1.177 +apply (unfold Constrains_def)
   1.178 +apply (blast intro: constrains_Int [THEN constrains_weaken])
   1.179 +done
   1.180 +
   1.181 +lemma Constrains_INT: 
   1.182 +  assumes Co: "!!i. i:I ==> F : (A i) Co (A' i)"
   1.183 +  shows "F : (INT i:I. A i) Co (INT i:I. A' i)"
   1.184 +apply (unfold Constrains_def)
   1.185 +apply (rule CollectI)
   1.186 +apply (rule Co [unfolded Constrains_def, THEN CollectD, THEN constrains_INT, 
   1.187 +                THEN constrains_weaken],   auto)
   1.188 +done
   1.189 +
   1.190 +lemma Constrains_imp_subset: "F : A Co A' ==> reachable F Int A <= A'"
   1.191 +by (simp add: constrains_imp_subset Constrains_def)
   1.192 +
   1.193 +lemma Constrains_trans: "[| F : A Co B; F : B Co C |] ==> F : A Co C"
   1.194 +apply (simp add: Constrains_eq_constrains)
   1.195 +apply (blast intro: constrains_trans constrains_weaken)
   1.196 +done
   1.197 +
   1.198 +lemma Constrains_cancel:
   1.199 +     "[| F : A Co (A' Un B); F : B Co B' |] ==> F : A Co (A' Un B')"
   1.200 +by (simp add: Constrains_eq_constrains constrains_def, blast)
   1.201 +
   1.202 +
   1.203 +(*** Stable ***)
   1.204 +
   1.205 +(*Useful because there's no Stable_weaken.  [Tanja Vos]*)
   1.206 +lemma Stable_eq: "[| F: Stable A; A = B |] ==> F : Stable B"
   1.207 +by blast
   1.208 +
   1.209 +lemma Stable_eq_stable: "(F : Stable A) = (F : stable (reachable F Int A))"
   1.210 +by (simp add: Stable_def Constrains_eq_constrains stable_def)
   1.211 +
   1.212 +lemma StableI: "F : A Co A ==> F : Stable A"
   1.213 +by (unfold Stable_def, assumption)
   1.214 +
   1.215 +lemma StableD: "F : Stable A ==> F : A Co A"
   1.216 +by (unfold Stable_def, assumption)
   1.217 +
   1.218 +lemma Stable_Un: 
   1.219 +    "[| F : Stable A; F : Stable A' |] ==> F : Stable (A Un A')"
   1.220 +apply (unfold Stable_def)
   1.221 +apply (blast intro: Constrains_Un)
   1.222 +done
   1.223 +
   1.224 +lemma Stable_Int: 
   1.225 +    "[| F : Stable A; F : Stable A' |] ==> F : Stable (A Int A')"
   1.226 +apply (unfold Stable_def)
   1.227 +apply (blast intro: Constrains_Int)
   1.228 +done
   1.229 +
   1.230 +lemma Stable_Constrains_Un: 
   1.231 +    "[| F : Stable C; F : A Co (C Un A') |]    
   1.232 +     ==> F : (C Un A) Co (C Un A')"
   1.233 +apply (unfold Stable_def)
   1.234 +apply (blast intro: Constrains_Un [THEN Constrains_weaken])
   1.235 +done
   1.236 +
   1.237 +lemma Stable_Constrains_Int: 
   1.238 +    "[| F : Stable C; F : (C Int A) Co A' |]    
   1.239 +     ==> F : (C Int A) Co (C Int A')"
   1.240 +apply (unfold Stable_def)
   1.241 +apply (blast intro: Constrains_Int [THEN Constrains_weaken])
   1.242 +done
   1.243 +
   1.244 +lemma Stable_UN: 
   1.245 +    "(!!i. i:I ==> F : Stable (A i)) ==> F : Stable (UN i:I. A i)"
   1.246 +by (simp add: Stable_def Constrains_UN) 
   1.247 +
   1.248 +lemma Stable_INT: 
   1.249 +    "(!!i. i:I ==> F : Stable (A i)) ==> F : Stable (INT i:I. A i)"
   1.250 +by (simp add: Stable_def Constrains_INT) 
   1.251 +
   1.252 +lemma Stable_reachable: "F : Stable (reachable F)"
   1.253 +by (simp add: Stable_eq_stable)
   1.254 +
   1.255 +
   1.256 +
   1.257 +(*** Increasing ***)
   1.258 +
   1.259 +lemma IncreasingD: 
   1.260 +     "F : Increasing f ==> F : Stable {s. x <= f s}"
   1.261 +by (unfold Increasing_def, blast)
   1.262 +
   1.263 +lemma mono_Increasing_o: 
   1.264 +     "mono g ==> Increasing f <= Increasing (g o f)"
   1.265 +apply (simp add: Increasing_def Stable_def Constrains_def stable_def 
   1.266 +                 constrains_def)
   1.267 +apply (blast intro: monoD order_trans)
   1.268 +done
   1.269 +
   1.270 +lemma strict_IncreasingD: 
   1.271 +     "!!z::nat. F : Increasing f ==> F: Stable {s. z < f s}"
   1.272 +by (simp add: Increasing_def Suc_le_eq [symmetric])
   1.273 +
   1.274 +lemma increasing_imp_Increasing: 
   1.275 +     "F : increasing f ==> F : Increasing f"
   1.276 +apply (unfold increasing_def Increasing_def)
   1.277 +apply (blast intro: stable_imp_Stable)
   1.278 +done
   1.279 +
   1.280 +lemmas Increasing_constant =  
   1.281 +    increasing_constant [THEN increasing_imp_Increasing, standard, iff]
   1.282 +
   1.283 +
   1.284 +(*** The Elimination Theorem.  The "free" m has become universally quantified!
   1.285 +     Should the premise be !!m instead of ALL m ?  Would make it harder to use
   1.286 +     in forward proof. ***)
   1.287 +
   1.288 +lemma Elimination: 
   1.289 +    "[| ALL m. F : {s. s x = m} Co (B m) |]  
   1.290 +     ==> F : {s. s x : M} Co (UN m:M. B m)"
   1.291 +
   1.292 +by (unfold Constrains_def constrains_def, blast)
   1.293 +
   1.294 +(*As above, but for the trivial case of a one-variable state, in which the
   1.295 +  state is identified with its one variable.*)
   1.296 +lemma Elimination_sing: 
   1.297 +    "(ALL m. F : {m} Co (B m)) ==> F : M Co (UN m:M. B m)"
   1.298 +by (unfold Constrains_def constrains_def, blast)
   1.299 +
   1.300 +
   1.301 +(*** Specialized laws for handling Always ***)
   1.302 +
   1.303 +(** Natural deduction rules for "Always A" **)
   1.304 +
   1.305 +lemma AlwaysI: "[| Init F<=A;  F : Stable A |] ==> F : Always A"
   1.306 +by (simp add: Always_def)
   1.307 +
   1.308 +lemma AlwaysD: "F : Always A ==> Init F<=A & F : Stable A"
   1.309 +by (simp add: Always_def)
   1.310 +
   1.311 +lemmas AlwaysE = AlwaysD [THEN conjE, standard]
   1.312 +lemmas Always_imp_Stable = AlwaysD [THEN conjunct2, standard]
   1.313 +
   1.314 +
   1.315 +(*The set of all reachable states is Always*)
   1.316 +lemma Always_includes_reachable: "F : Always A ==> reachable F <= A"
   1.317 +apply (simp add: Stable_def Constrains_def constrains_def Always_def)
   1.318 +apply (rule subsetI)
   1.319 +apply (erule reachable.induct)
   1.320 +apply (blast intro: reachable.intros)+
   1.321 +done
   1.322 +
   1.323 +lemma invariant_imp_Always: 
   1.324 +     "F : invariant A ==> F : Always A"
   1.325 +apply (unfold Always_def invariant_def Stable_def stable_def)
   1.326 +apply (blast intro: constrains_imp_Constrains)
   1.327 +done
   1.328 +
   1.329 +lemmas Always_reachable =
   1.330 +    invariant_reachable [THEN invariant_imp_Always, standard]
   1.331 +
   1.332 +lemma Always_eq_invariant_reachable:
   1.333 +     "Always A = {F. F : invariant (reachable F Int A)}"
   1.334 +apply (simp add: Always_def invariant_def Stable_def Constrains_eq_constrains
   1.335 +                 stable_def)
   1.336 +apply (blast intro: reachable.intros)
   1.337 +done
   1.338 +
   1.339 +(*the RHS is the traditional definition of the "always" operator*)
   1.340 +lemma Always_eq_includes_reachable: "Always A = {F. reachable F <= A}"
   1.341 +by (auto dest: invariant_includes_reachable simp add: Int_absorb2 invariant_reachable Always_eq_invariant_reachable)
   1.342 +
   1.343 +lemma Always_UNIV_eq [simp]: "Always UNIV = UNIV"
   1.344 +by (auto simp add: Always_eq_includes_reachable)
   1.345 +
   1.346 +lemma UNIV_AlwaysI: "UNIV <= A ==> F : Always A"
   1.347 +by (auto simp add: Always_eq_includes_reachable)
   1.348 +
   1.349 +lemma Always_eq_UN_invariant: "Always A = (UN I: Pow A. invariant I)"
   1.350 +apply (simp add: Always_eq_includes_reachable)
   1.351 +apply (blast intro: invariantI Init_subset_reachable [THEN subsetD] 
   1.352 +                    invariant_includes_reachable [THEN subsetD])
   1.353 +done
   1.354 +
   1.355 +lemma Always_weaken: "[| F : Always A; A <= B |] ==> F : Always B"
   1.356 +by (auto simp add: Always_eq_includes_reachable)
   1.357 +
   1.358 +
   1.359 +(*** "Co" rules involving Always ***)
   1.360 +
   1.361 +lemma Always_Constrains_pre:
   1.362 +     "F : Always INV ==> (F : (INV Int A) Co A') = (F : A Co A')"
   1.363 +by (simp add: Always_includes_reachable [THEN Int_absorb2] Constrains_def 
   1.364 +              Int_assoc [symmetric])
   1.365 +
   1.366 +lemma Always_Constrains_post:
   1.367 +     "F : Always INV ==> (F : A Co (INV Int A')) = (F : A Co A')"
   1.368 +by (simp add: Always_includes_reachable [THEN Int_absorb2] 
   1.369 +              Constrains_eq_constrains Int_assoc [symmetric])
   1.370 +
   1.371 +(* [| F : Always INV;  F : (INV Int A) Co A' |] ==> F : A Co A' *)
   1.372 +lemmas Always_ConstrainsI = Always_Constrains_pre [THEN iffD1, standard]
   1.373 +
   1.374 +(* [| F : Always INV;  F : A Co A' |] ==> F : A Co (INV Int A') *)
   1.375 +lemmas Always_ConstrainsD = Always_Constrains_post [THEN iffD2, standard]
   1.376 +
   1.377 +(*The analogous proof of Always_LeadsTo_weaken doesn't terminate*)
   1.378 +lemma Always_Constrains_weaken:
   1.379 +     "[| F : Always C;  F : A Co A';    
   1.380 +         C Int B <= A;   C Int A' <= B' |]  
   1.381 +      ==> F : B Co B'"
   1.382 +apply (rule Always_ConstrainsI, assumption)
   1.383 +apply (drule Always_ConstrainsD, assumption)
   1.384 +apply (blast intro: Constrains_weaken)
   1.385 +done
   1.386 +
   1.387 +
   1.388 +(** Conjoining Always properties **)
   1.389 +
   1.390 +lemma Always_Int_distrib: "Always (A Int B) = Always A Int Always B"
   1.391 +by (auto simp add: Always_eq_includes_reachable)
   1.392 +
   1.393 +lemma Always_INT_distrib: "Always (INTER I A) = (INT i:I. Always (A i))"
   1.394 +by (auto simp add: Always_eq_includes_reachable)
   1.395 +
   1.396 +lemma Always_Int_I:
   1.397 +     "[| F : Always A;  F : Always B |] ==> F : Always (A Int B)"
   1.398 +by (simp add: Always_Int_distrib)
   1.399 +
   1.400 +(*Allows a kind of "implication introduction"*)
   1.401 +lemma Always_Compl_Un_eq:
   1.402 +     "F : Always A ==> (F : Always (-A Un B)) = (F : Always B)"
   1.403 +by (auto simp add: Always_eq_includes_reachable)
   1.404 +
   1.405 +(*Delete the nearest invariance assumption (which will be the second one
   1.406 +  used by Always_Int_I) *)
   1.407 +lemmas Always_thin = thin_rl [of "F : Always A", standard]
   1.408 +
   1.409  end