author | paulson |
Fri, 31 Jan 2003 20:12:44 +0100 | |
changeset 13798 | 4c1a53627500 |
parent 13792 | d1811693899c |
child 13805 | 3786b2fd6808 |
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 |
|
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9685
diff
changeset
|
15 |
(*FIXME: conjoin Init F Int Init G ~= {} *) |
13792 | 16 |
ok :: "['a program, 'a program] => bool" (infixl "ok" 65) |
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9685
diff
changeset
|
17 |
"F ok G == Acts F <= AllowedActs G & |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9685
diff
changeset
|
18 |
Acts G <= AllowedActs F" |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9685
diff
changeset
|
19 |
|
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9685
diff
changeset
|
20 |
(*FIXME: conjoin (INT i:I. Init (F i)) ~= {} *) |
13792 | 21 |
OK :: "['a set, 'a => 'b program] => bool" |
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9685
diff
changeset
|
22 |
"OK I F == (ALL i:I. ALL j: I-{i}. Acts (F i) <= AllowedActs (F j))" |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9685
diff
changeset
|
23 |
|
13792 | 24 |
JOIN :: "['a set, 'a => 'b program] => 'b program" |
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9685
diff
changeset
|
25 |
"JOIN I F == mk_program (INT i:I. Init (F i), UN i:I. Acts (F i), |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9685
diff
changeset
|
26 |
INT i:I. AllowedActs (F i))" |
5252 | 27 |
|
13792 | 28 |
Join :: "['a program, 'a program] => 'a program" (infixl "Join" 65) |
10064
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9685
diff
changeset
|
29 |
"F Join G == mk_program (Init F Int Init G, Acts F Un Acts G, |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9685
diff
changeset
|
30 |
AllowedActs F Int 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" |
1a77667b21ef
added compatibility relation: AllowedActs, Allowed, ok,
paulson
parents:
9685
diff
changeset
|
37 |
"safety_prop X == SKIP: X & (ALL G. Acts G <= UNION X Acts --> G : 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 |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
5259
diff
changeset
|
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) |
|
52 |
"@JOIN" :: "[pttrn, 'a set, 'b set] => 'b set" ("(3\<Squnion> _:_./ _)" 10) |
|
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 |
|
71 |
lemma SKIP_in_constrains_iff [iff]: "(SKIP : A co B) = (A<=B)" |
|
72 |
by (unfold constrains_def, auto) |
|
73 |
||
74 |
lemma SKIP_in_Constrains_iff [iff]: "(SKIP : A Co B) = (A<=B)" |
|
75 |
by (unfold Constrains_def, auto) |
|
76 |
||
77 |
lemma SKIP_in_stable [iff]: "SKIP : stable A" |
|
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 |
|
85 |
lemma Init_Join [simp]: "Init (F Join G) = Init F Int Init G" |
|
86 |
by (simp add: Join_def) |
|
87 |
||
88 |
lemma Acts_Join [simp]: "Acts (F Join G) = Acts F Un Acts G" |
|
89 |
by (auto simp add: Join_def) |
|
90 |
||
91 |
lemma AllowedActs_Join [simp]: |
|
92 |
"AllowedActs (F Join G) = AllowedActs F Int AllowedActs G" |
|
93 |
by (auto simp add: Join_def) |
|
94 |
||
95 |
||
13798 | 96 |
subsection{*JN*} |
13792 | 97 |
|
98 |
lemma JN_empty [simp]: "(JN i:{}. F i) = SKIP" |
|
99 |
by (unfold JOIN_def SKIP_def, auto) |
|
100 |
||
101 |
lemma JN_insert [simp]: "(JN i:insert a I. F i) = (F a) Join (JN i:I. F i)" |
|
102 |
apply (rule program_equalityI) |
|
103 |
apply (auto simp add: JOIN_def Join_def) |
|
104 |
done |
|
105 |
||
106 |
lemma Init_JN [simp]: "Init (JN i:I. F i) = (INT i:I. Init (F i))" |
|
107 |
by (simp add: JOIN_def) |
|
108 |
||
109 |
lemma Acts_JN [simp]: "Acts (JN i:I. F i) = insert Id (UN i:I. Acts (F i))" |
|
110 |
by (auto simp add: JOIN_def) |
|
111 |
||
112 |
lemma AllowedActs_JN [simp]: |
|
113 |
"AllowedActs (JN i:I. F i) = (INT i:I. AllowedActs (F i))" |
|
114 |
by (auto simp add: JOIN_def) |
|
115 |
||
116 |
||
117 |
lemma JN_cong [cong]: |
|
118 |
"[| I=J; !!i. i:J ==> F i = G i |] ==> (JN i:I. F i) = (JN i:J. G i)" |
|
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 |
||
13798 | 159 |
subsection{*JN laws*} |
13792 | 160 |
|
161 |
(*Also follows by JN_insert and insert_absorb, but the proof is longer*) |
|
162 |
lemma JN_absorb: "k:I ==> F k Join (JN i:I. F i) = (JN i:I. F i)" |
|
163 |
by (auto intro!: program_equalityI) |
|
164 |
||
165 |
lemma JN_Un: "(JN i: I Un J. F i) = ((JN i: I. F i) Join (JN i:J. F i))" |
|
166 |
by (auto intro!: program_equalityI) |
|
167 |
||
168 |
lemma JN_constant: "(JN i:I. c) = (if I={} then SKIP else c)" |
|
169 |
by (rule program_equalityI, auto) |
|
170 |
||
171 |
lemma JN_Join_distrib: |
|
172 |
"(JN i:I. F i Join G i) = (JN i:I. F i) Join (JN i:I. G i)" |
|
173 |
by (auto intro!: program_equalityI) |
|
174 |
||
175 |
lemma JN_Join_miniscope: |
|
176 |
"i : I ==> (JN i:I. F i Join G) = ((JN i:I. F i) Join G)" |
|
177 |
by (auto simp add: JN_Join_distrib JN_constant) |
|
178 |
||
179 |
(*Used to prove guarantees_JN_I*) |
|
180 |
lemma JN_Join_diff: "i: I ==> F i Join JOIN (I - {i}) F = JOIN I F" |
|
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 |
|
188 |
(*Fails if I={} because it collapses to SKIP : A co B, i.e. to A<=B. So an |
|
189 |
alternative precondition is A<=B, but most proofs using this rule require |
|
190 |
I to be nonempty for other reasons anyway.*) |
|
191 |
lemma JN_constrains: |
|
192 |
"i : I ==> (JN i:I. F i) : A co B = (ALL i:I. F i : A co B)" |
|
193 |
by (simp add: constrains_def JOIN_def, blast) |
|
194 |
||
195 |
lemma Join_constrains [simp]: |
|
196 |
"(F Join G : A co B) = (F : A co B & G : A co B)" |
|
197 |
by (auto simp add: constrains_def Join_def) |
|
198 |
||
199 |
lemma Join_unless [simp]: |
|
200 |
"(F Join G : A unless B) = (F : A unless B & G : A unless B)" |
|
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: |
|
209 |
"[| F : A co A'; G : B co B' |] |
|
210 |
==> F Join G : (A Int B) co (A' Un B')" |
|
211 |
by (simp, blast intro: constrains_weaken) |
|
212 |
||
213 |
(*If I={}, it degenerates to SKIP : UNIV co {}, which is false.*) |
|
214 |
lemma JN_constrains_weaken: |
|
215 |
"[| ALL i:I. F i : A i co A' i; i: I |] |
|
216 |
==> (JN i:I. F i) : (INT i:I. A i) co (UN i:I. A' i)" |
|
217 |
apply (simp (no_asm_simp) add: JN_constrains) |
|
218 |
apply (blast intro: constrains_weaken) |
|
219 |
done |
|
220 |
||
221 |
lemma JN_stable: "(JN i:I. F i) : stable A = (ALL i:I. F i : stable A)" |
|
222 |
by (simp add: stable_def constrains_def JOIN_def) |
|
223 |
||
224 |
lemma invariant_JN_I: |
|
225 |
"[| !!i. i:I ==> F i : invariant A; i : I |] |
|
226 |
==> (JN i:I. F i) : invariant A" |
|
227 |
by (simp add: invariant_def JN_stable, blast) |
|
228 |
||
229 |
lemma Join_stable [simp]: |
|
230 |
"(F Join G : stable A) = |
|
231 |
(F : stable A & G : stable A)" |
|
232 |
by (simp add: stable_def) |
|
233 |
||
234 |
lemma Join_increasing [simp]: |
|
235 |
"(F Join G : increasing f) = |
|
236 |
(F : increasing f & G : increasing f)" |
|
237 |
by (simp add: increasing_def Join_stable, blast) |
|
238 |
||
239 |
lemma invariant_JoinI: |
|
240 |
"[| F : invariant A; G : invariant A |] |
|
241 |
==> F Join G : invariant A" |
|
242 |
by (simp add: invariant_def, blast) |
|
243 |
||
244 |
lemma FP_JN: "FP (JN i:I. F i) = (INT i:I. FP (F i))" |
|
245 |
by (simp add: FP_def JN_stable INTER_def) |
|
246 |
||
247 |
||
13798 | 248 |
subsection{*Progress: transient, ensures*} |
13792 | 249 |
|
250 |
lemma JN_transient: |
|
251 |
"i : I ==> |
|
252 |
(JN i:I. F i) : transient A = (EX i:I. F i : transient A)" |
|
253 |
by (auto simp add: transient_def JOIN_def) |
|
254 |
||
255 |
lemma Join_transient [simp]: |
|
256 |
"F Join G : transient A = |
|
257 |
(F : transient A | G : transient A)" |
|
258 |
by (auto simp add: bex_Un transient_def Join_def) |
|
259 |
||
260 |
lemma Join_transient_I1: "F : transient A ==> F Join G : transient A" |
|
261 |
by (simp add: Join_transient) |
|
262 |
||
263 |
lemma Join_transient_I2: "G : transient A ==> F Join G : transient A" |
|
264 |
by (simp add: Join_transient) |
|
265 |
||
266 |
(*If I={} it degenerates to (SKIP : A ensures B) = False, i.e. to ~(A<=B) *) |
|
267 |
lemma JN_ensures: |
|
268 |
"i : I ==> |
|
269 |
(JN i:I. F i) : A ensures B = |
|
270 |
((ALL i:I. F i : (A-B) co (A Un B)) & (EX i:I. F i : A ensures B))" |
|
271 |
by (auto simp add: ensures_def JN_constrains JN_transient) |
|
272 |
||
273 |
lemma Join_ensures: |
|
274 |
"F Join G : A ensures B = |
|
275 |
(F : (A-B) co (A Un B) & G : (A-B) co (A Un B) & |
|
276 |
(F : transient (A-B) | G : transient (A-B)))" |
|
277 |
by (auto simp add: ensures_def Join_transient) |
|
278 |
||
279 |
lemma stable_Join_constrains: |
|
280 |
"[| F : stable A; G : A co A' |] |
|
281 |
==> F Join G : A co A'" |
|
282 |
apply (unfold stable_def constrains_def Join_def) |
|
283 |
apply (simp add: ball_Un, blast) |
|
284 |
done |
|
285 |
||
286 |
(*Premise for G cannot use Always because F: Stable A is weaker than |
|
287 |
G : stable A *) |
|
288 |
lemma stable_Join_Always1: |
|
289 |
"[| F : stable A; G : invariant A |] ==> F Join G : Always A" |
|
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: |
|
296 |
"[| F : invariant A; G : stable A |] ==> F Join G : Always A" |
|
297 |
apply (subst Join_commute) |
|
298 |
apply (blast intro: stable_Join_Always1) |
|
299 |
done |
|
300 |
||
301 |
lemma stable_Join_ensures1: |
|
302 |
"[| F : stable A; G : A ensures B |] ==> F Join G : A ensures B" |
|
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: |
|
310 |
"[| F : A ensures B; G : stable A |] ==> F Join G : A ensures B" |
|
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 |
||
347 |
lemma ok_JN_iff1 [iff]: "F ok (JOIN I G) = (ALL i:I. F ok G i)" |
|
348 |
by (auto simp add: ok_def) |
|
349 |
||
350 |
lemma ok_JN_iff2 [iff]: "(JOIN I G) ok F = (ALL i:I. G i ok F)" |
|
351 |
by (auto simp add: ok_def) |
|
352 |
||
353 |
lemma OK_iff_ok: "OK I F = (ALL i: I. ALL j: I-{i}. (F i) ok (F j))" |
|
354 |
by (auto simp add: ok_def OK_def) |
|
355 |
||
356 |
lemma OK_imp_ok: "[| OK I F; i: I; j: I; i ~= j|] ==> (F i) ok (F j)" |
|
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 |
||
365 |
lemma Allowed_Join [simp]: "Allowed (F Join G) = Allowed F Int Allowed G" |
|
366 |
by (auto simp add: Allowed_def) |
|
367 |
||
368 |
lemma Allowed_JN [simp]: "Allowed (JOIN I F) = (INT i:I. Allowed (F i))" |
|
369 |
by (auto simp add: Allowed_def) |
|
370 |
||
371 |
lemma ok_iff_Allowed: "F ok G = (F : Allowed G & G : Allowed F)" |
|
372 |
by (simp add: ok_def Allowed_def) |
|
373 |
||
374 |
lemma OK_iff_Allowed: "OK I F = (ALL i: I. ALL j: I-{i}. F i : Allowed(F j))" |
|
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: |
|
381 |
"safety_prop X ==> (Acts G <= insert Id (UNION X Acts)) = (G : X)" |
|
382 |
by (auto simp add: safety_prop_def) |
|
383 |
||
384 |
lemma safety_prop_AllowedActs_iff_Allowed: |
|
385 |
"safety_prop X ==> (UNION X Acts <= AllowedActs F) = (X <= Allowed F)" |
|
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!*) |
|
398 |
lemma safety_prop_constrains [iff]: "safety_prop (A co B) = (A <= B)" |
|
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]: |
|
405 |
"[| safety_prop X; safety_prop Y |] ==> safety_prop (X Int Y)" |
|
406 |
by (simp add: safety_prop_def, blast) |
|
407 |
||
408 |
lemma safety_prop_INTER1 [simp]: |
|
409 |
"(!!i. safety_prop (X i)) ==> safety_prop (INT i. X i)" |
|
410 |
by (auto simp add: safety_prop_def, blast) |
|
411 |
||
412 |
lemma safety_prop_INTER [simp]: |
|
413 |
"(!!i. i:I ==> safety_prop (X i)) ==> safety_prop (INT i:I. X i)" |
|
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 |] |
|
418 |
==> F ok G = (G : X & acts <= AllowedActs G)" |
|
419 |
by (auto simp add: ok_def safety_prop_Acts_iff) |
|
9685 | 420 |
|
5252 | 421 |
end |