author | paulson |
Tue, 04 Feb 2003 18:12:40 +0100 | |
changeset 13805 | 3786b2fd6808 |
parent 13798 | 4c1a53627500 |
child 13812 | 91713a1915ee |
permissions | -rw-r--r-- |
5252 | 1 |
(* Title: HOL/UNITY/Union.thy |
2 |
ID: $Id$ |
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 1998 University of Cambridge |
|
5 |
||
5804
8e0a4c4fd67b
Revising the Client proof as suggested by Michel Charpentier. New lemmas
paulson
parents:
5648
diff
changeset
|
6 |
Partly from Misra's Chapter 5: Asynchronous Compositions of Programs |
5252 | 7 |
*) |
8 |
||
13798 | 9 |
header{*Unions of Programs*} |
10 |
||
13792 | 11 |
theory Union = SubstAx + FP: |
5252 | 12 |
|
13 |
constdefs |
|
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9685
diff
changeset
|
14 |
|
13805 | 15 |
(*FIXME: conjoin Init F \<inter> Init G \<noteq> {} *) |
13792 | 16 |
ok :: "['a program, 'a program] => bool" (infixl "ok" 65) |
13805 | 17 |
"F ok G == Acts F \<subseteq> AllowedActs G & |
18 |
Acts G \<subseteq> AllowedActs F" |
|
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9685
diff
changeset
|
19 |
|
13805 | 20 |
(*FIXME: conjoin (\<Inter>i \<in> I. Init (F i)) \<noteq> {} *) |
13792 | 21 |
OK :: "['a set, 'a => 'b program] => bool" |
13805 | 22 |
"OK I F == (\<forall>i \<in> I. \<forall>j \<in> I-{i}. Acts (F i) \<subseteq> AllowedActs (F j))" |
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9685
diff
changeset
|
23 |
|
13792 | 24 |
JOIN :: "['a set, 'a => 'b program] => 'b program" |
13805 | 25 |
"JOIN I F == mk_program (\<Inter>i \<in> I. Init (F i), \<Union>i \<in> I. Acts (F i), |
26 |
\<Inter>i \<in> I. AllowedActs (F i))" |
|
5252 | 27 |
|
13792 | 28 |
Join :: "['a program, 'a program] => 'a program" (infixl "Join" 65) |
13805 | 29 |
"F Join G == mk_program (Init F \<inter> Init G, Acts F \<union> Acts G, |
30 |
AllowedActs F \<inter> AllowedActs G)" |
|
5252 | 31 |
|
13792 | 32 |
SKIP :: "'a program" |
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9685
diff
changeset
|
33 |
"SKIP == mk_program (UNIV, {}, UNIV)" |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9685
diff
changeset
|
34 |
|
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9685
diff
changeset
|
35 |
(*Characterizes safety properties. Used with specifying AllowedActs*) |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9685
diff
changeset
|
36 |
safety_prop :: "'a program set => bool" |
13805 | 37 |
"safety_prop X == SKIP: X & (\<forall>G. Acts G \<subseteq> UNION X Acts --> G \<in> X)" |
5259 | 38 |
|
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
39 |
syntax |
13792 | 40 |
"@JOIN1" :: "[pttrns, 'b set] => 'b set" ("(3JN _./ _)" 10) |
41 |
"@JOIN" :: "[pttrn, 'a set, 'b set] => 'b set" ("(3JN _:_./ _)" 10) |
|
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
42 |
|
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
43 |
translations |
13805 | 44 |
"JN x : A. B" == "JOIN A (%x. B)" |
7359 | 45 |
"JN x y. B" == "JN x. JN y. B" |
46 |
"JN x. B" == "JOIN UNIV (%x. B)" |
|
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
47 |
|
12114
a8e860c86252
eliminated old "symbols" syntax, use "xsymbols" instead;
wenzelm
parents:
10064
diff
changeset
|
48 |
syntax (xsymbols) |
13792 | 49 |
SKIP :: "'a program" ("\<bottom>") |
50 |
"op Join" :: "['a program, 'a program] => 'a program" (infixl "\<squnion>" 65) |
|
51 |
"@JOIN1" :: "[pttrns, 'b set] => 'b set" ("(3\<Squnion> _./ _)" 10) |
|
13805 | 52 |
"@JOIN" :: "[pttrn, 'a set, 'b set] => 'b set" ("(3\<Squnion> _\<in>_./ _)" 10) |
13792 | 53 |
|
54 |
||
13798 | 55 |
subsection{*SKIP*} |
13792 | 56 |
|
57 |
lemma Init_SKIP [simp]: "Init SKIP = UNIV" |
|
58 |
by (simp add: SKIP_def) |
|
59 |
||
60 |
lemma Acts_SKIP [simp]: "Acts SKIP = {Id}" |
|
61 |
by (simp add: SKIP_def) |
|
62 |
||
63 |
lemma AllowedActs_SKIP [simp]: "AllowedActs SKIP = UNIV" |
|
64 |
by (auto simp add: SKIP_def) |
|
65 |
||
66 |
lemma reachable_SKIP [simp]: "reachable SKIP = UNIV" |
|
67 |
by (force elim: reachable.induct intro: reachable.intros) |
|
68 |
||
13798 | 69 |
subsection{*SKIP and safety properties*} |
13792 | 70 |
|
13805 | 71 |
lemma SKIP_in_constrains_iff [iff]: "(SKIP \<in> A co B) = (A \<subseteq> B)" |
13792 | 72 |
by (unfold constrains_def, auto) |
73 |
||
13805 | 74 |
lemma SKIP_in_Constrains_iff [iff]: "(SKIP \<in> A Co B) = (A \<subseteq> B)" |
13792 | 75 |
by (unfold Constrains_def, auto) |
76 |
||
13805 | 77 |
lemma SKIP_in_stable [iff]: "SKIP \<in> stable A" |
13792 | 78 |
by (unfold stable_def, auto) |
79 |
||
80 |
declare SKIP_in_stable [THEN stable_imp_Stable, iff] |
|
81 |
||
82 |
||
13798 | 83 |
subsection{*Join*} |
13792 | 84 |
|
13805 | 85 |
lemma Init_Join [simp]: "Init (F Join G) = Init F \<inter> Init G" |
13792 | 86 |
by (simp add: Join_def) |
87 |
||
13805 | 88 |
lemma Acts_Join [simp]: "Acts (F Join G) = Acts F \<union> Acts G" |
13792 | 89 |
by (auto simp add: Join_def) |
90 |
||
91 |
lemma AllowedActs_Join [simp]: |
|
13805 | 92 |
"AllowedActs (F Join G) = AllowedActs F \<inter> AllowedActs G" |
13792 | 93 |
by (auto simp add: Join_def) |
94 |
||
95 |
||
13798 | 96 |
subsection{*JN*} |
13792 | 97 |
|
13805 | 98 |
lemma JN_empty [simp]: "(\<Squnion>i\<in>{}. F i) = SKIP" |
13792 | 99 |
by (unfold JOIN_def SKIP_def, auto) |
100 |
||
13805 | 101 |
lemma JN_insert [simp]: "(\<Squnion>i \<in> insert a I. F i) = (F a) Join (\<Squnion>i \<in> I. F i)" |
13792 | 102 |
apply (rule program_equalityI) |
103 |
apply (auto simp add: JOIN_def Join_def) |
|
104 |
done |
|
105 |
||
13805 | 106 |
lemma Init_JN [simp]: "Init (\<Squnion>i \<in> I. F i) = (\<Inter>i \<in> I. Init (F i))" |
13792 | 107 |
by (simp add: JOIN_def) |
108 |
||
13805 | 109 |
lemma Acts_JN [simp]: "Acts (\<Squnion>i \<in> I. F i) = insert Id (\<Union>i \<in> I. Acts (F i))" |
13792 | 110 |
by (auto simp add: JOIN_def) |
111 |
||
112 |
lemma AllowedActs_JN [simp]: |
|
13805 | 113 |
"AllowedActs (\<Squnion>i \<in> I. F i) = (\<Inter>i \<in> I. AllowedActs (F i))" |
13792 | 114 |
by (auto simp add: JOIN_def) |
115 |
||
116 |
||
117 |
lemma JN_cong [cong]: |
|
13805 | 118 |
"[| I=J; !!i. i \<in> J ==> F i = G i |] ==> (\<Squnion>i \<in> I. F i) = (\<Squnion>i \<in> J. G i)" |
13792 | 119 |
by (simp add: JOIN_def) |
120 |
||
121 |
||
13798 | 122 |
subsection{*Algebraic laws*} |
13792 | 123 |
|
124 |
lemma Join_commute: "F Join G = G Join F" |
|
125 |
by (simp add: Join_def Un_commute Int_commute) |
|
126 |
||
127 |
lemma Join_assoc: "(F Join G) Join H = F Join (G Join H)" |
|
128 |
by (simp add: Un_ac Join_def Int_assoc insert_absorb) |
|
129 |
||
130 |
lemma Join_left_commute: "A Join (B Join C) = B Join (A Join C)" |
|
131 |
by (simp add: Un_ac Int_ac Join_def insert_absorb) |
|
132 |
||
133 |
lemma Join_SKIP_left [simp]: "SKIP Join F = F" |
|
134 |
apply (unfold Join_def SKIP_def) |
|
135 |
apply (rule program_equalityI) |
|
136 |
apply (simp_all (no_asm) add: insert_absorb) |
|
137 |
done |
|
138 |
||
139 |
lemma Join_SKIP_right [simp]: "F Join SKIP = F" |
|
140 |
apply (unfold Join_def SKIP_def) |
|
141 |
apply (rule program_equalityI) |
|
142 |
apply (simp_all (no_asm) add: insert_absorb) |
|
143 |
done |
|
144 |
||
145 |
lemma Join_absorb [simp]: "F Join F = F" |
|
146 |
apply (unfold Join_def) |
|
147 |
apply (rule program_equalityI, auto) |
|
148 |
done |
|
149 |
||
150 |
lemma Join_left_absorb: "F Join (F Join G) = F Join G" |
|
151 |
apply (unfold Join_def) |
|
152 |
apply (rule program_equalityI, auto) |
|
153 |
done |
|
154 |
||
155 |
(*Join is an AC-operator*) |
|
156 |
lemmas Join_ac = Join_assoc Join_left_absorb Join_commute Join_left_commute |
|
157 |
||
158 |
||
13805 | 159 |
subsection{*\<Squnion>laws*} |
13792 | 160 |
|
161 |
(*Also follows by JN_insert and insert_absorb, but the proof is longer*) |
|
13805 | 162 |
lemma JN_absorb: "k \<in> I ==> F k Join (\<Squnion>i \<in> I. F i) = (\<Squnion>i \<in> I. F i)" |
13792 | 163 |
by (auto intro!: program_equalityI) |
164 |
||
13805 | 165 |
lemma JN_Un: "(\<Squnion>i \<in> I \<union> J. F i) = ((\<Squnion>i \<in> I. F i) Join (\<Squnion>i \<in> J. F i))" |
13792 | 166 |
by (auto intro!: program_equalityI) |
167 |
||
13805 | 168 |
lemma JN_constant: "(\<Squnion>i \<in> I. c) = (if I={} then SKIP else c)" |
13792 | 169 |
by (rule program_equalityI, auto) |
170 |
||
171 |
lemma JN_Join_distrib: |
|
13805 | 172 |
"(\<Squnion>i \<in> I. F i Join G i) = (\<Squnion>i \<in> I. F i) Join (\<Squnion>i \<in> I. G i)" |
13792 | 173 |
by (auto intro!: program_equalityI) |
174 |
||
175 |
lemma JN_Join_miniscope: |
|
13805 | 176 |
"i \<in> I ==> (\<Squnion>i \<in> I. F i Join G) = ((\<Squnion>i \<in> I. F i) Join G)" |
13792 | 177 |
by (auto simp add: JN_Join_distrib JN_constant) |
178 |
||
179 |
(*Used to prove guarantees_JN_I*) |
|
13805 | 180 |
lemma JN_Join_diff: "i \<in> I ==> F i Join JOIN (I - {i}) F = JOIN I F" |
13792 | 181 |
apply (unfold JOIN_def Join_def) |
182 |
apply (rule program_equalityI, auto) |
|
183 |
done |
|
184 |
||
185 |
||
13798 | 186 |
subsection{*Safety: co, stable, FP*} |
13792 | 187 |
|
13805 | 188 |
(*Fails if I={} because it collapses to SKIP \<in> A co B, i.e. to A \<subseteq> B. So an |
189 |
alternative precondition is A \<subseteq> B, but most proofs using this rule require |
|
13792 | 190 |
I to be nonempty for other reasons anyway.*) |
191 |
lemma JN_constrains: |
|
13805 | 192 |
"i \<in> I ==> (\<Squnion>i \<in> I. F i) \<in> A co B = (\<forall>i \<in> I. F i \<in> A co B)" |
13792 | 193 |
by (simp add: constrains_def JOIN_def, blast) |
194 |
||
195 |
lemma Join_constrains [simp]: |
|
13805 | 196 |
"(F Join G \<in> A co B) = (F \<in> A co B & G \<in> A co B)" |
13792 | 197 |
by (auto simp add: constrains_def Join_def) |
198 |
||
199 |
lemma Join_unless [simp]: |
|
13805 | 200 |
"(F Join G \<in> A unless B) = (F \<in> A unless B & G \<in> A unless B)" |
13792 | 201 |
by (simp add: Join_constrains unless_def) |
202 |
||
203 |
(*Analogous weak versions FAIL; see Misra [1994] 5.4.1, Substitution Axiom. |
|
204 |
reachable (F Join G) could be much bigger than reachable F, reachable G |
|
205 |
*) |
|
206 |
||
207 |
||
208 |
lemma Join_constrains_weaken: |
|
13805 | 209 |
"[| F \<in> A co A'; G \<in> B co B' |] |
210 |
==> F Join G \<in> (A \<inter> B) co (A' \<union> B')" |
|
13792 | 211 |
by (simp, blast intro: constrains_weaken) |
212 |
||
13805 | 213 |
(*If I={}, it degenerates to SKIP \<in> UNIV co {}, which is false.*) |
13792 | 214 |
lemma JN_constrains_weaken: |
13805 | 215 |
"[| \<forall>i \<in> I. F i \<in> A i co A' i; i \<in> I |] |
216 |
==> (\<Squnion>i \<in> I. F i) \<in> (\<Inter>i \<in> I. A i) co (\<Union>i \<in> I. A' i)" |
|
13792 | 217 |
apply (simp (no_asm_simp) add: JN_constrains) |
218 |
apply (blast intro: constrains_weaken) |
|
219 |
done |
|
220 |
||
13805 | 221 |
lemma JN_stable: "(\<Squnion>i \<in> I. F i) \<in> stable A = (\<forall>i \<in> I. F i \<in> stable A)" |
13792 | 222 |
by (simp add: stable_def constrains_def JOIN_def) |
223 |
||
224 |
lemma invariant_JN_I: |
|
13805 | 225 |
"[| !!i. i \<in> I ==> F i \<in> invariant A; i \<in> I |] |
226 |
==> (\<Squnion>i \<in> I. F i) \<in> invariant A" |
|
13792 | 227 |
by (simp add: invariant_def JN_stable, blast) |
228 |
||
229 |
lemma Join_stable [simp]: |
|
13805 | 230 |
"(F Join G \<in> stable A) = |
231 |
(F \<in> stable A & G \<in> stable A)" |
|
13792 | 232 |
by (simp add: stable_def) |
233 |
||
234 |
lemma Join_increasing [simp]: |
|
13805 | 235 |
"(F Join G \<in> increasing f) = |
236 |
(F \<in> increasing f & G \<in> increasing f)" |
|
13792 | 237 |
by (simp add: increasing_def Join_stable, blast) |
238 |
||
239 |
lemma invariant_JoinI: |
|
13805 | 240 |
"[| F \<in> invariant A; G \<in> invariant A |] |
241 |
==> F Join G \<in> invariant A" |
|
13792 | 242 |
by (simp add: invariant_def, blast) |
243 |
||
13805 | 244 |
lemma FP_JN: "FP (\<Squnion>i \<in> I. F i) = (\<Inter>i \<in> I. FP (F i))" |
13792 | 245 |
by (simp add: FP_def JN_stable INTER_def) |
246 |
||
247 |
||
13798 | 248 |
subsection{*Progress: transient, ensures*} |
13792 | 249 |
|
250 |
lemma JN_transient: |
|
13805 | 251 |
"i \<in> I ==> |
252 |
(\<Squnion>i \<in> I. F i) \<in> transient A = (\<exists>i \<in> I. F i \<in> transient A)" |
|
13792 | 253 |
by (auto simp add: transient_def JOIN_def) |
254 |
||
255 |
lemma Join_transient [simp]: |
|
13805 | 256 |
"F Join G \<in> transient A = |
257 |
(F \<in> transient A | G \<in> transient A)" |
|
13792 | 258 |
by (auto simp add: bex_Un transient_def Join_def) |
259 |
||
13805 | 260 |
lemma Join_transient_I1: "F \<in> transient A ==> F Join G \<in> transient A" |
13792 | 261 |
by (simp add: Join_transient) |
262 |
||
13805 | 263 |
lemma Join_transient_I2: "G \<in> transient A ==> F Join G \<in> transient A" |
13792 | 264 |
by (simp add: Join_transient) |
265 |
||
13805 | 266 |
(*If I={} it degenerates to (SKIP \<in> A ensures B) = False, i.e. to ~(A \<subseteq> B) *) |
13792 | 267 |
lemma JN_ensures: |
13805 | 268 |
"i \<in> I ==> |
269 |
(\<Squnion>i \<in> I. F i) \<in> A ensures B = |
|
270 |
((\<forall>i \<in> I. F i \<in> (A-B) co (A \<union> B)) & (\<exists>i \<in> I. F i \<in> A ensures B))" |
|
13792 | 271 |
by (auto simp add: ensures_def JN_constrains JN_transient) |
272 |
||
273 |
lemma Join_ensures: |
|
13805 | 274 |
"F Join G \<in> A ensures B = |
275 |
(F \<in> (A-B) co (A \<union> B) & G \<in> (A-B) co (A \<union> B) & |
|
276 |
(F \<in> transient (A-B) | G \<in> transient (A-B)))" |
|
13792 | 277 |
by (auto simp add: ensures_def Join_transient) |
278 |
||
279 |
lemma stable_Join_constrains: |
|
13805 | 280 |
"[| F \<in> stable A; G \<in> A co A' |] |
281 |
==> F Join G \<in> A co A'" |
|
13792 | 282 |
apply (unfold stable_def constrains_def Join_def) |
283 |
apply (simp add: ball_Un, blast) |
|
284 |
done |
|
285 |
||
13805 | 286 |
(*Premise for G cannot use Always because F \<in> Stable A is weaker than |
287 |
G \<in> stable A *) |
|
13792 | 288 |
lemma stable_Join_Always1: |
13805 | 289 |
"[| F \<in> stable A; G \<in> invariant A |] ==> F Join G \<in> Always A" |
13792 | 290 |
apply (simp (no_asm_use) add: Always_def invariant_def Stable_eq_stable) |
291 |
apply (force intro: stable_Int) |
|
292 |
done |
|
293 |
||
294 |
(*As above, but exchanging the roles of F and G*) |
|
295 |
lemma stable_Join_Always2: |
|
13805 | 296 |
"[| F \<in> invariant A; G \<in> stable A |] ==> F Join G \<in> Always A" |
13792 | 297 |
apply (subst Join_commute) |
298 |
apply (blast intro: stable_Join_Always1) |
|
299 |
done |
|
300 |
||
301 |
lemma stable_Join_ensures1: |
|
13805 | 302 |
"[| F \<in> stable A; G \<in> A ensures B |] ==> F Join G \<in> A ensures B" |
13792 | 303 |
apply (simp (no_asm_simp) add: Join_ensures) |
304 |
apply (simp add: stable_def ensures_def) |
|
305 |
apply (erule constrains_weaken, auto) |
|
306 |
done |
|
307 |
||
308 |
(*As above, but exchanging the roles of F and G*) |
|
309 |
lemma stable_Join_ensures2: |
|
13805 | 310 |
"[| F \<in> A ensures B; G \<in> stable A |] ==> F Join G \<in> A ensures B" |
13792 | 311 |
apply (subst Join_commute) |
312 |
apply (blast intro: stable_Join_ensures1) |
|
313 |
done |
|
314 |
||
315 |
||
13798 | 316 |
subsection{*the ok and OK relations*} |
13792 | 317 |
|
318 |
lemma ok_SKIP1 [iff]: "SKIP ok F" |
|
319 |
by (auto simp add: ok_def) |
|
320 |
||
321 |
lemma ok_SKIP2 [iff]: "F ok SKIP" |
|
322 |
by (auto simp add: ok_def) |
|
323 |
||
324 |
lemma ok_Join_commute: |
|
325 |
"(F ok G & (F Join G) ok H) = (G ok H & F ok (G Join H))" |
|
326 |
by (auto simp add: ok_def) |
|
327 |
||
328 |
lemma ok_commute: "(F ok G) = (G ok F)" |
|
329 |
by (auto simp add: ok_def) |
|
330 |
||
331 |
lemmas ok_sym = ok_commute [THEN iffD1, standard] |
|
332 |
||
333 |
lemma ok_iff_OK: |
|
334 |
"OK {(0::int,F),(1,G),(2,H)} snd = (F ok G & (F Join G) ok H)" |
|
335 |
by (simp add: Ball_def conj_disj_distribR ok_def Join_def OK_def insert_absorb all_conj_distrib eq_commute, blast) |
|
336 |
||
337 |
lemma ok_Join_iff1 [iff]: "F ok (G Join H) = (F ok G & F ok H)" |
|
338 |
by (auto simp add: ok_def) |
|
339 |
||
340 |
lemma ok_Join_iff2 [iff]: "(G Join H) ok F = (G ok F & H ok F)" |
|
341 |
by (auto simp add: ok_def) |
|
342 |
||
343 |
(*useful? Not with the previous two around*) |
|
344 |
lemma ok_Join_commute_I: "[| F ok G; (F Join G) ok H |] ==> F ok (G Join H)" |
|
345 |
by (auto simp add: ok_def) |
|
346 |
||
13805 | 347 |
lemma ok_JN_iff1 [iff]: "F ok (JOIN I G) = (\<forall>i \<in> I. F ok G i)" |
13792 | 348 |
by (auto simp add: ok_def) |
349 |
||
13805 | 350 |
lemma ok_JN_iff2 [iff]: "(JOIN I G) ok F = (\<forall>i \<in> I. G i ok F)" |
13792 | 351 |
by (auto simp add: ok_def) |
352 |
||
13805 | 353 |
lemma OK_iff_ok: "OK I F = (\<forall>i \<in> I. \<forall>j \<in> I-{i}. (F i) ok (F j))" |
13792 | 354 |
by (auto simp add: ok_def OK_def) |
355 |
||
13805 | 356 |
lemma OK_imp_ok: "[| OK I F; i \<in> I; j \<in> I; i \<noteq> j|] ==> (F i) ok (F j)" |
13792 | 357 |
by (auto simp add: OK_iff_ok) |
358 |
||
359 |
||
13798 | 360 |
subsection{*Allowed*} |
13792 | 361 |
|
362 |
lemma Allowed_SKIP [simp]: "Allowed SKIP = UNIV" |
|
363 |
by (auto simp add: Allowed_def) |
|
364 |
||
13805 | 365 |
lemma Allowed_Join [simp]: "Allowed (F Join G) = Allowed F \<inter> Allowed G" |
13792 | 366 |
by (auto simp add: Allowed_def) |
367 |
||
13805 | 368 |
lemma Allowed_JN [simp]: "Allowed (JOIN I F) = (\<Inter>i \<in> I. Allowed (F i))" |
13792 | 369 |
by (auto simp add: Allowed_def) |
370 |
||
13805 | 371 |
lemma ok_iff_Allowed: "F ok G = (F \<in> Allowed G & G \<in> Allowed F)" |
13792 | 372 |
by (simp add: ok_def Allowed_def) |
373 |
||
13805 | 374 |
lemma OK_iff_Allowed: "OK I F = (\<forall>i \<in> I. \<forall>j \<in> I-{i}. F i \<in> Allowed(F j))" |
13792 | 375 |
by (auto simp add: OK_iff_ok ok_iff_Allowed) |
376 |
||
13798 | 377 |
subsection{*@{text safety_prop}, for reasoning about |
378 |
given instances of "ok"*} |
|
13792 | 379 |
|
380 |
lemma safety_prop_Acts_iff: |
|
13805 | 381 |
"safety_prop X ==> (Acts G \<subseteq> insert Id (UNION X Acts)) = (G \<in> X)" |
13792 | 382 |
by (auto simp add: safety_prop_def) |
383 |
||
384 |
lemma safety_prop_AllowedActs_iff_Allowed: |
|
13805 | 385 |
"safety_prop X ==> (UNION X Acts \<subseteq> AllowedActs F) = (X \<subseteq> Allowed F)" |
13792 | 386 |
by (auto simp add: Allowed_def safety_prop_Acts_iff [symmetric]) |
387 |
||
388 |
lemma Allowed_eq: |
|
389 |
"safety_prop X ==> Allowed (mk_program (init, acts, UNION X Acts)) = X" |
|
390 |
by (simp add: Allowed_def safety_prop_Acts_iff) |
|
391 |
||
392 |
lemma def_prg_Allowed: |
|
393 |
"[| F == mk_program (init, acts, UNION X Acts) ; safety_prop X |] |
|
394 |
==> Allowed F = X" |
|
395 |
by (simp add: Allowed_eq) |
|
396 |
||
397 |
(*For safety_prop to hold, the property must be satisfiable!*) |
|
13805 | 398 |
lemma safety_prop_constrains [iff]: "safety_prop (A co B) = (A \<subseteq> B)" |
13792 | 399 |
by (simp add: safety_prop_def constrains_def, blast) |
400 |
||
401 |
lemma safety_prop_stable [iff]: "safety_prop (stable A)" |
|
402 |
by (simp add: stable_def) |
|
403 |
||
404 |
lemma safety_prop_Int [simp]: |
|
13805 | 405 |
"[| safety_prop X; safety_prop Y |] ==> safety_prop (X \<inter> Y)" |
13792 | 406 |
by (simp add: safety_prop_def, blast) |
407 |
||
408 |
lemma safety_prop_INTER1 [simp]: |
|
13805 | 409 |
"(!!i. safety_prop (X i)) ==> safety_prop (\<Inter>i. X i)" |
13792 | 410 |
by (auto simp add: safety_prop_def, blast) |
411 |
||
412 |
lemma safety_prop_INTER [simp]: |
|
13805 | 413 |
"(!!i. i \<in> I ==> safety_prop (X i)) ==> safety_prop (\<Inter>i \<in> I. X i)" |
13792 | 414 |
by (auto simp add: safety_prop_def, blast) |
415 |
||
416 |
lemma def_UNION_ok_iff: |
|
417 |
"[| F == mk_program(init,acts,UNION X Acts); safety_prop X |] |
|
13805 | 418 |
==> F ok G = (G \<in> X & acts \<subseteq> AllowedActs G)" |
13792 | 419 |
by (auto simp add: ok_def safety_prop_Acts_iff) |
9685 | 420 |
|
5252 | 421 |
end |