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