9 |
9 |
10 Theory ported form HOL.. |
10 Theory ported form HOL.. |
11 |
11 |
12 *) |
12 *) |
13 |
13 |
14 Union = SubstAx + FP + |
14 theory Union = SubstAx + FP: |
|
15 |
|
16 declare Inter_0 [simp] |
15 |
17 |
16 constdefs |
18 constdefs |
17 |
19 |
18 (*FIXME: conjoin Init(F) Int Init(G) ~= 0 *) |
20 (*FIXME: conjoin Init(F) Int Init(G) \<noteq> 0 *) |
19 ok :: [i, i] => o (infixl 65) |
21 ok :: "[i, i] => o" (infixl "ok" 65) |
20 "F ok G == Acts(F) <= AllowedActs(G) & |
22 "F ok G == Acts(F) \<subseteq> AllowedActs(G) & |
21 Acts(G) <= AllowedActs(F)" |
23 Acts(G) \<subseteq> AllowedActs(F)" |
22 |
24 |
23 (*FIXME: conjoin (INT i:I. Init(F(i))) ~= 0 *) |
25 (*FIXME: conjoin (\<Inter>i \<in> I. Init(F(i))) \<noteq> 0 *) |
24 OK :: [i, i=>i] => o |
26 OK :: "[i, i=>i] => o" |
25 "OK(I,F) == (ALL i:I. ALL j: I-{i}. Acts(F(i)) <= AllowedActs(F(j)))" |
27 "OK(I,F) == (\<forall>i \<in> I. \<forall>j \<in> I-{i}. Acts(F(i)) \<subseteq> AllowedActs(F(j)))" |
26 |
28 |
27 JOIN :: [i, i=>i] => i |
29 JOIN :: "[i, i=>i] => i" |
28 "JOIN(I,F) == if I = 0 then SKIP else |
30 "JOIN(I,F) == if I = 0 then SKIP else |
29 mk_program(INT i:I. Init(F(i)), UN i:I. Acts(F(i)), |
31 mk_program(\<Inter>i \<in> I. Init(F(i)), \<Union>i \<in> I. Acts(F(i)), |
30 INT i:I. AllowedActs(F(i)))" |
32 \<Inter>i \<in> I. AllowedActs(F(i)))" |
31 |
33 |
32 Join :: [i, i] => i (infixl 65) |
34 Join :: "[i, i] => i" (infixl "Join" 65) |
33 "F Join G == mk_program (Init(F) Int Init(G), Acts(F) Un Acts(G), |
35 "F Join G == mk_program (Init(F) Int Init(G), Acts(F) Un Acts(G), |
34 AllowedActs(F) Int AllowedActs(G))" |
36 AllowedActs(F) Int AllowedActs(G))" |
35 (*Characterizes safety properties. Used with specifying AllowedActs*) |
37 (*Characterizes safety properties. Used with specifying AllowedActs*) |
36 safety_prop :: "i => o" |
38 safety_prop :: "i => o" |
37 "safety_prop(X) == X<=program & |
39 "safety_prop(X) == X\<subseteq>program & |
38 SKIP:X & (ALL G:program. Acts(G) <= (UN F:X. Acts(F)) --> G:X)" |
40 SKIP \<in> X & (\<forall>G \<in> program. Acts(G) \<subseteq> (\<Union>F \<in> X. Acts(F)) --> G \<in> X)" |
39 |
41 |
40 syntax |
42 syntax |
41 "@JOIN1" :: [pttrns, i] => i ("(3JN _./ _)" 10) |
43 "@JOIN1" :: "[pttrns, i] => i" ("(3JN _./ _)" 10) |
42 "@JOIN" :: [pttrn, i, i] => i ("(3JN _:_./ _)" 10) |
44 "@JOIN" :: "[pttrn, i, i] => i" ("(3JN _:_./ _)" 10) |
43 |
45 |
44 translations |
46 translations |
45 "JN x:A. B" == "JOIN(A, (%x. B))" |
47 "JN x:A. B" == "JOIN(A, (%x. B))" |
46 "JN x y. B" == "JN x. JN y. B" |
48 "JN x y. B" == "JN x. JN y. B" |
47 "JN x. B" == "JOIN(state,(%x. B))" |
49 "JN x. B" == "JOIN(state,(%x. B))" |
48 |
50 |
49 syntax (symbols) |
51 syntax (symbols) |
50 SKIP :: i ("\\<bottom>") |
52 SKIP :: i ("\<bottom>") |
51 "op Join" :: [i, i] => i (infixl "\\<squnion>" 65) |
53 Join :: "[i, i] => i" (infixl "\<squnion>" 65) |
52 "@JOIN1" :: [pttrns, i] => i ("(3\\<Squnion> _./ _)" 10) |
54 "@JOIN1" :: "[pttrns, i] => i" ("(3\<Squnion> _./ _)" 10) |
53 "@JOIN" :: [pttrn, i, i] => i ("(3\\<Squnion> _:_./ _)" 10) |
55 "@JOIN" :: "[pttrn, i, i] => i" ("(3\<Squnion> _ \<in> _./ _)" 10) |
|
56 |
|
57 |
|
58 subsection{*SKIP*} |
|
59 |
|
60 lemma reachable_SKIP [simp]: "reachable(SKIP) = state" |
|
61 by (force elim: reachable.induct intro: reachable.intros) |
|
62 |
|
63 text{*Elimination programify from ok and Join*} |
|
64 |
|
65 lemma ok_programify_left [iff]: "programify(F) ok G <-> F ok G" |
|
66 by (simp add: ok_def) |
|
67 |
|
68 lemma ok_programify_right [iff]: "F ok programify(G) <-> F ok G" |
|
69 by (simp add: ok_def) |
|
70 |
|
71 lemma Join_programify_left [simp]: "programify(F) Join G = F Join G" |
|
72 by (simp add: Join_def) |
|
73 |
|
74 lemma Join_programify_right [simp]: "F Join programify(G) = F Join G" |
|
75 by (simp add: Join_def) |
|
76 |
|
77 subsection{*SKIP and safety properties*} |
|
78 |
|
79 lemma SKIP_in_constrains_iff [iff]: "(SKIP \<in> A co B) <-> (A\<subseteq>B & st_set(A))" |
|
80 by (unfold constrains_def st_set_def, auto) |
|
81 |
|
82 lemma SKIP_in_Constrains_iff [iff]: "(SKIP \<in> A Co B)<-> (state Int A\<subseteq>B)" |
|
83 by (unfold Constrains_def, auto) |
|
84 |
|
85 lemma SKIP_in_stable [iff]: "SKIP \<in> stable(A) <-> st_set(A)" |
|
86 by (auto simp add: stable_def) |
|
87 |
|
88 lemma SKIP_in_Stable [iff]: "SKIP \<in> Stable(A)" |
|
89 by (unfold Stable_def, auto) |
|
90 |
|
91 subsection{*Join and JOIN types*} |
|
92 |
|
93 lemma Join_in_program [iff,TC]: "F Join G \<in> program" |
|
94 by (unfold Join_def, auto) |
|
95 |
|
96 lemma JOIN_in_program [iff,TC]: "JOIN(I,F) \<in> program" |
|
97 by (unfold JOIN_def, auto) |
|
98 |
|
99 subsection{*Init, Acts, and AllowedActs of Join and JOIN*} |
|
100 lemma Init_Join [simp]: "Init(F Join G) = Init(F) Int Init(G)" |
|
101 by (simp add: Int_assoc Join_def) |
|
102 |
|
103 lemma Acts_Join [simp]: "Acts(F Join G) = Acts(F) Un Acts(G)" |
|
104 by (simp add: Int_Un_distrib2 cons_absorb Join_def) |
|
105 |
|
106 lemma AllowedActs_Join [simp]: "AllowedActs(F Join G) = |
|
107 AllowedActs(F) Int AllowedActs(G)" |
|
108 apply (simp add: Int_assoc cons_absorb Join_def) |
|
109 done |
|
110 |
|
111 subsection{*Join's algebraic laws*} |
|
112 |
|
113 lemma Join_commute: "F Join G = G Join F" |
|
114 by (simp add: Join_def Un_commute Int_commute) |
|
115 |
|
116 lemma Join_left_commute: "A Join (B Join C) = B Join (A Join C)" |
|
117 apply (simp add: Join_def Int_Un_distrib2 cons_absorb) |
|
118 apply (simp add: Un_ac Int_ac Int_Un_distrib2 cons_absorb) |
|
119 done |
|
120 |
|
121 lemma Join_assoc: "(F Join G) Join H = F Join (G Join H)" |
|
122 by (simp add: Un_ac Join_def cons_absorb Int_assoc Int_Un_distrib2) |
|
123 |
|
124 subsection{*Needed below*} |
|
125 lemma cons_id [simp]: "cons(id(state), Pow(state * state)) = Pow(state*state)" |
|
126 by auto |
|
127 |
|
128 lemma Join_SKIP_left [simp]: "SKIP Join F = programify(F)" |
|
129 apply (unfold Join_def SKIP_def) |
|
130 apply (auto simp add: Int_absorb cons_eq) |
|
131 done |
|
132 |
|
133 lemma Join_SKIP_right [simp]: "F Join SKIP = programify(F)" |
|
134 apply (subst Join_commute) |
|
135 apply (simp add: Join_SKIP_left) |
|
136 done |
|
137 |
|
138 lemma Join_absorb [simp]: "F Join F = programify(F)" |
|
139 by (rule program_equalityI, auto) |
|
140 |
|
141 lemma Join_left_absorb: "F Join (F Join G) = F Join G" |
|
142 by (simp add: Join_assoc [symmetric]) |
|
143 |
|
144 subsection{*Join is an AC-operator*} |
|
145 lemmas Join_ac = Join_assoc Join_left_absorb Join_commute Join_left_commute |
|
146 |
|
147 subsection{*Eliminating programify form JN and OK expressions*} |
|
148 |
|
149 lemma OK_programify [iff]: "OK(I, %x. programify(F(x))) <-> OK(I, F)" |
|
150 by (simp add: OK_def) |
|
151 |
|
152 lemma JN_programify [iff]: "JOIN(I, %x. programify(F(x))) = JOIN(I, F)" |
|
153 by (simp add: JOIN_def) |
|
154 |
|
155 |
|
156 subsection{*JN*} |
|
157 |
|
158 lemma JN_empty [simp]: "JOIN(0, F) = SKIP" |
|
159 by (unfold JOIN_def, auto) |
|
160 |
|
161 lemma Init_JN [simp]: |
|
162 "Init(\<Squnion>i \<in> I. F(i)) = (if I=0 then state else (\<Inter>i \<in> I. Init(F(i))))" |
|
163 apply (simp add: JOIN_def) |
|
164 apply (auto elim!: not_emptyE simp add: INT_extend_simps simp del: INT_simps) |
|
165 done |
|
166 |
|
167 lemma Acts_JN [simp]: |
|
168 "Acts(JOIN(I,F)) = cons(id(state), \<Union>i \<in> I. Acts(F(i)))" |
|
169 apply (unfold JOIN_def) |
|
170 apply (auto simp del: INT_simps UN_simps) |
|
171 apply (rule equalityI) |
|
172 apply (auto dest: Acts_type [THEN subsetD]) |
|
173 done |
|
174 |
|
175 lemma AllowedActs_JN [simp]: |
|
176 "AllowedActs(\<Squnion>i \<in> I. F(i)) = |
|
177 (if I=0 then Pow(state*state) else (\<Inter>i \<in> I. AllowedActs(F(i))))" |
|
178 apply (unfold JOIN_def, auto) |
|
179 apply (rule equalityI) |
|
180 apply (auto elim!: not_emptyE dest: AllowedActs_type [THEN subsetD]) |
|
181 done |
|
182 |
|
183 lemma JN_cons [simp]: "(\<Squnion>i \<in> cons(a,I). F(i)) = F(a) Join (\<Squnion>i \<in> I. F(i))" |
|
184 by (rule program_equalityI, auto) |
|
185 |
|
186 lemma JN_cong [cong]: |
|
187 "[| I=J; !!i. i \<in> J ==> F(i) = G(i) |] ==> |
|
188 (\<Squnion>i \<in> I. F(i)) = (\<Squnion>i \<in> J. G(i))" |
|
189 by (simp add: JOIN_def) |
|
190 |
|
191 |
|
192 |
|
193 subsection{*JN laws*} |
|
194 lemma JN_absorb: "k \<in> I ==>F(k) Join (\<Squnion>i \<in> I. F(i)) = (\<Squnion>i \<in> I. F(i))" |
|
195 apply (subst JN_cons [symmetric]) |
|
196 apply (auto simp add: cons_absorb) |
|
197 done |
|
198 |
|
199 lemma JN_Un: "(\<Squnion>i \<in> I Un J. F(i)) = ((\<Squnion>i \<in> I. F(i)) Join (\<Squnion>i \<in> J. F(i)))" |
|
200 apply (rule program_equalityI) |
|
201 apply (simp_all add: UN_Un INT_Un) |
|
202 apply (simp_all del: INT_simps add: INT_extend_simps, blast) |
|
203 done |
|
204 |
|
205 lemma JN_constant: "(\<Squnion>i \<in> I. c) = (if I=0 then SKIP else programify(c))" |
|
206 by (rule program_equalityI, auto) |
|
207 |
|
208 lemma JN_Join_distrib: |
|
209 "(\<Squnion>i \<in> I. F(i) Join G(i)) = (\<Squnion>i \<in> I. F(i)) Join (\<Squnion>i \<in> I. G(i))" |
|
210 apply (rule program_equalityI) |
|
211 apply (simp_all add: Int_absorb) |
|
212 apply (safe elim!: not_emptyE) |
|
213 apply (simp_all add: INT_Int_distrib Int_absorb, force) |
|
214 done |
|
215 |
|
216 lemma JN_Join_miniscope: "(\<Squnion>i \<in> I. F(i) Join G) = ((\<Squnion>i \<in> I. F(i) Join G))" |
|
217 by (simp add: JN_Join_distrib JN_constant) |
|
218 |
|
219 text{*Used to prove guarantees_JN_I*} |
|
220 lemma JN_Join_diff: "i \<in> I==>F(i) Join JOIN(I - {i}, F) = JOIN(I, F)" |
|
221 apply (rule program_equalityI) |
|
222 apply (auto elim!: not_emptyE) |
|
223 done |
|
224 |
|
225 subsection{*Safety: co, stable, FP*} |
|
226 |
|
227 |
|
228 (*Fails if I=0 because it collapses to SKIP \<in> A co B, i.e. to A\<subseteq>B. So an |
|
229 alternative precondition is A\<subseteq>B, but most proofs using this rule require |
|
230 I to be nonempty for other reasons anyway.*) |
|
231 |
|
232 lemma JN_constrains: |
|
233 "i \<in> I==>(\<Squnion>i \<in> I. F(i)) \<in> A co B <-> (\<forall>i \<in> I. programify(F(i)) \<in> A co B)" |
|
234 |
|
235 apply (unfold constrains_def JOIN_def st_set_def, auto) |
|
236 prefer 2 apply blast |
|
237 apply (rename_tac j act y z) |
|
238 apply (cut_tac F = "F (j) " in Acts_type) |
|
239 apply (drule_tac x = act in bspec, auto) |
|
240 done |
|
241 |
|
242 lemma Join_constrains [iff]: |
|
243 "(F Join G \<in> A co B) <-> (programify(F) \<in> A co B & programify(G) \<in> A co B)" |
|
244 by (auto simp add: constrains_def) |
|
245 |
|
246 lemma Join_unless [iff]: |
|
247 "(F Join G \<in> A unless B) <-> |
|
248 (programify(F) \<in> A unless B & programify(G) \<in> A unless B)" |
|
249 by (simp add: Join_constrains unless_def) |
|
250 |
|
251 |
|
252 (*Analogous weak versions FAIL; see Misra [1994] 5.4.1, Substitution Axiom. |
|
253 reachable (F Join G) could be much bigger than reachable F, reachable G |
|
254 *) |
|
255 |
|
256 lemma Join_constrains_weaken: |
|
257 "[| F \<in> A co A'; G \<in> B co B' |] |
|
258 ==> F Join G \<in> (A Int B) co (A' Un B')" |
|
259 apply (subgoal_tac "st_set (A) & st_set (B) & F \<in> program & G \<in> program") |
|
260 prefer 2 apply (blast dest: constrainsD2, simp) |
|
261 apply (blast intro: constrains_weaken) |
|
262 done |
|
263 |
|
264 (*If I=0, it degenerates to SKIP \<in> state co 0, which is false.*) |
|
265 lemma JN_constrains_weaken: |
|
266 assumes major: "(!!i. i \<in> I ==> F(i) \<in> A(i) co A'(i))" |
|
267 and minor: "i \<in> I" |
|
268 shows "(\<Squnion>i \<in> I. F(i)) \<in> (\<Inter>i \<in> I. A(i)) co (\<Union>i \<in> I. A'(i))" |
|
269 apply (cut_tac minor) |
|
270 apply (simp (no_asm_simp) add: JN_constrains) |
|
271 apply clarify |
|
272 apply (rename_tac "j") |
|
273 apply (frule_tac i = j in major) |
|
274 apply (frule constrainsD2, simp) |
|
275 apply (blast intro: constrains_weaken) |
|
276 done |
|
277 |
|
278 lemma JN_stable: |
|
279 "(\<Squnion>i \<in> I. F(i)) \<in> stable(A) <-> ((\<forall>i \<in> I. programify(F(i)) \<in> stable(A)) & st_set(A))" |
|
280 apply (auto simp add: stable_def constrains_def JOIN_def) |
|
281 apply (cut_tac F = "F (i) " in Acts_type) |
|
282 apply (drule_tac x = act in bspec, auto) |
|
283 done |
|
284 |
|
285 lemma initially_JN_I: |
|
286 assumes major: "(!!i. i \<in> I ==>F(i) \<in> initially(A))" |
|
287 and minor: "i \<in> I" |
|
288 shows "(\<Squnion>i \<in> I. F(i)) \<in> initially(A)" |
|
289 apply (cut_tac minor) |
|
290 apply (auto elim!: not_emptyE simp add: Inter_iff initially_def) |
|
291 apply (frule_tac i = x in major) |
|
292 apply (auto simp add: initially_def) |
|
293 done |
|
294 |
|
295 lemma invariant_JN_I: |
|
296 assumes major: "(!!i. i \<in> I ==> F(i) \<in> invariant(A))" |
|
297 and minor: "i \<in> I" |
|
298 shows "(\<Squnion>i \<in> I. F(i)) \<in> invariant(A)" |
|
299 apply (cut_tac minor) |
|
300 apply (auto intro!: initially_JN_I dest: major simp add: invariant_def JN_stable) |
|
301 apply (erule_tac V = "i \<in> I" in thin_rl) |
|
302 apply (frule major) |
|
303 apply (drule_tac [2] major) |
|
304 apply (auto simp add: invariant_def) |
|
305 apply (frule stableD2, force)+ |
|
306 done |
|
307 |
|
308 lemma Join_stable [iff]: |
|
309 " (F Join G \<in> stable(A)) <-> |
|
310 (programify(F) \<in> stable(A) & programify(G) \<in> stable(A))" |
|
311 by (simp add: stable_def) |
|
312 |
|
313 lemma initially_JoinI [intro!]: |
|
314 "[| F \<in> initially(A); G \<in> initially(A) |] ==> F Join G \<in> initially(A)" |
|
315 by (unfold initially_def, auto) |
|
316 |
|
317 lemma invariant_JoinI: |
|
318 "[| F \<in> invariant(A); G \<in> invariant(A) |] |
|
319 ==> F Join G \<in> invariant(A)" |
|
320 apply (subgoal_tac "F \<in> program&G \<in> program") |
|
321 prefer 2 apply (blast dest: invariantD2) |
|
322 apply (simp add: invariant_def) |
|
323 apply (auto intro: Join_in_program) |
|
324 done |
|
325 |
|
326 |
|
327 (* Fails if I=0 because \<Inter>i \<in> 0. A(i) = 0 *) |
|
328 lemma FP_JN: "i \<in> I ==> FP(\<Squnion>i \<in> I. F(i)) = (\<Inter>i \<in> I. FP (programify(F(i))))" |
|
329 by (auto simp add: FP_def Inter_def st_set_def JN_stable) |
|
330 |
|
331 subsection{*Progress: transient, ensures*} |
|
332 |
|
333 lemma JN_transient: |
|
334 "i \<in> I ==> |
|
335 (\<Squnion>i \<in> I. F(i)) \<in> transient(A) <-> (\<exists>i \<in> I. programify(F(i)) \<in> transient(A))" |
|
336 apply (auto simp add: transient_def JOIN_def) |
|
337 apply (unfold st_set_def) |
|
338 apply (drule_tac [2] x = act in bspec) |
|
339 apply (auto dest: Acts_type [THEN subsetD]) |
|
340 done |
|
341 |
|
342 lemma Join_transient [iff]: |
|
343 "F Join G \<in> transient(A) <-> |
|
344 (programify(F) \<in> transient(A) | programify(G) \<in> transient(A))" |
|
345 apply (auto simp add: transient_def Join_def Int_Un_distrib2) |
|
346 done |
|
347 |
|
348 lemma Join_transient_I1: "F \<in> transient(A) ==> F Join G \<in> transient(A)" |
|
349 by (simp add: Join_transient transientD2) |
|
350 |
|
351 |
|
352 lemma Join_transient_I2: "G \<in> transient(A) ==> F Join G \<in> transient(A)" |
|
353 by (simp add: Join_transient transientD2) |
|
354 |
|
355 (*If I=0 it degenerates to (SKIP \<in> A ensures B) = False, i.e. to ~(A\<subseteq>B) *) |
|
356 lemma JN_ensures: |
|
357 "i \<in> I ==> |
|
358 (\<Squnion>i \<in> I. F(i)) \<in> A ensures B <-> |
|
359 ((\<forall>i \<in> I. programify(F(i)) \<in> (A-B) co (A Un B)) & |
|
360 (\<exists>i \<in> I. programify(F(i)) \<in> A ensures B))" |
|
361 by (auto simp add: ensures_def JN_constrains JN_transient) |
|
362 |
|
363 |
|
364 lemma Join_ensures: |
|
365 "F Join G \<in> A ensures B <-> |
|
366 (programify(F) \<in> (A-B) co (A Un B) & programify(G) \<in> (A-B) co (A Un B) & |
|
367 (programify(F) \<in> transient (A-B) | programify(G) \<in> transient (A-B)))" |
|
368 |
|
369 apply (unfold ensures_def) |
|
370 apply (auto simp add: Join_transient) |
|
371 done |
|
372 |
|
373 lemma stable_Join_constrains: |
|
374 "[| F \<in> stable(A); G \<in> A co A' |] |
|
375 ==> F Join G \<in> A co A'" |
|
376 apply (unfold stable_def constrains_def Join_def st_set_def) |
|
377 apply (cut_tac F = F in Acts_type) |
|
378 apply (cut_tac F = G in Acts_type, force) |
|
379 done |
|
380 |
|
381 (*Premise for G cannot use Always because F \<in> Stable A is |
|
382 weaker than G \<in> stable A *) |
|
383 lemma stable_Join_Always1: |
|
384 "[| F \<in> stable(A); G \<in> invariant(A) |] ==> F Join G \<in> Always(A)" |
|
385 apply (subgoal_tac "F \<in> program & G \<in> program & st_set (A) ") |
|
386 prefer 2 apply (blast dest: invariantD2 stableD2) |
|
387 apply (simp add: Always_def invariant_def initially_def Stable_eq_stable) |
|
388 apply (force intro: stable_Int) |
|
389 done |
|
390 |
|
391 (*As above, but exchanging the roles of F and G*) |
|
392 lemma stable_Join_Always2: |
|
393 "[| F \<in> invariant(A); G \<in> stable(A) |] ==> F Join G \<in> Always(A)" |
|
394 apply (subst Join_commute) |
|
395 apply (blast intro: stable_Join_Always1) |
|
396 done |
|
397 |
|
398 |
|
399 |
|
400 lemma stable_Join_ensures1: |
|
401 "[| F \<in> stable(A); G \<in> A ensures B |] ==> F Join G \<in> A ensures B" |
|
402 apply (subgoal_tac "F \<in> program & G \<in> program & st_set (A) ") |
|
403 prefer 2 apply (blast dest: stableD2 ensures_type [THEN subsetD]) |
|
404 apply (simp (no_asm_simp) add: Join_ensures) |
|
405 apply (simp add: stable_def ensures_def) |
|
406 apply (erule constrains_weaken, auto) |
|
407 done |
|
408 |
|
409 |
|
410 (*As above, but exchanging the roles of F and G*) |
|
411 lemma stable_Join_ensures2: |
|
412 "[| F \<in> A ensures B; G \<in> stable(A) |] ==> F Join G \<in> A ensures B" |
|
413 apply (subst Join_commute) |
|
414 apply (blast intro: stable_Join_ensures1) |
|
415 done |
|
416 |
|
417 subsection{*The ok and OK relations*} |
|
418 |
|
419 lemma ok_SKIP1 [iff]: "SKIP ok F" |
|
420 by (auto dest: Acts_type [THEN subsetD] simp add: ok_def) |
|
421 |
|
422 lemma ok_SKIP2 [iff]: "F ok SKIP" |
|
423 by (auto dest: Acts_type [THEN subsetD] simp add: ok_def) |
|
424 |
|
425 lemma ok_Join_commute: |
|
426 "(F ok G & (F Join G) ok H) <-> (G ok H & F ok (G Join H))" |
|
427 by (auto simp add: ok_def) |
|
428 |
|
429 lemma ok_commute: "(F ok G) <->(G ok F)" |
|
430 by (auto simp add: ok_def) |
|
431 |
|
432 lemmas ok_sym = ok_commute [THEN iffD1, standard] |
|
433 |
|
434 lemma ok_iff_OK: "OK({<0,F>,<1,G>,<2,H>}, snd) <-> (F ok G & (F Join G) ok H)" |
|
435 by (simp add: ok_def Join_def OK_def Int_assoc cons_absorb |
|
436 Int_Un_distrib2 Ball_def, safe, force+) |
|
437 |
|
438 lemma ok_Join_iff1 [iff]: "F ok (G Join H) <-> (F ok G & F ok H)" |
|
439 by (auto simp add: ok_def) |
|
440 |
|
441 lemma ok_Join_iff2 [iff]: "(G Join H) ok F <-> (G ok F & H ok F)" |
|
442 by (auto simp add: ok_def) |
|
443 |
|
444 (*useful? Not with the previous two around*) |
|
445 lemma ok_Join_commute_I: "[| F ok G; (F Join G) ok H |] ==> F ok (G Join H)" |
|
446 by (auto simp add: ok_def) |
|
447 |
|
448 lemma ok_JN_iff1 [iff]: "F ok JOIN(I,G) <-> (\<forall>i \<in> I. F ok G(i))" |
|
449 by (force dest: Acts_type [THEN subsetD] elim!: not_emptyE simp add: ok_def) |
|
450 |
|
451 lemma ok_JN_iff2 [iff]: "JOIN(I,G) ok F <-> (\<forall>i \<in> I. G(i) ok F)" |
|
452 apply (auto elim!: not_emptyE simp add: ok_def) |
|
453 apply (blast dest: Acts_type [THEN subsetD]) |
|
454 done |
|
455 |
|
456 lemma OK_iff_ok: "OK(I,F) <-> (\<forall>i \<in> I. \<forall>j \<in> I-{i}. F(i) ok (F(j)))" |
|
457 by (auto simp add: ok_def OK_def) |
|
458 |
|
459 lemma OK_imp_ok: "[| OK(I,F); i \<in> I; j \<in> I; i\<noteq>j|] ==> F(i) ok F(j)" |
|
460 by (auto simp add: OK_iff_ok) |
|
461 |
|
462 |
|
463 subsection{*Allowed*} |
|
464 |
|
465 lemma Allowed_SKIP [simp]: "Allowed(SKIP) = program" |
|
466 by (auto dest: Acts_type [THEN subsetD] simp add: Allowed_def) |
|
467 |
|
468 lemma Allowed_Join [simp]: |
|
469 "Allowed(F Join G) = |
|
470 Allowed(programify(F)) Int Allowed(programify(G))" |
|
471 apply (auto simp add: Allowed_def) |
|
472 done |
|
473 |
|
474 lemma Allowed_JN [simp]: |
|
475 "i \<in> I ==> |
|
476 Allowed(JOIN(I,F)) = (\<Inter>i \<in> I. Allowed(programify(F(i))))" |
|
477 apply (auto simp add: Allowed_def, blast) |
|
478 done |
|
479 |
|
480 lemma ok_iff_Allowed: |
|
481 "F ok G <-> (programify(F) \<in> Allowed(programify(G)) & |
|
482 programify(G) \<in> Allowed(programify(F)))" |
|
483 by (simp add: ok_def Allowed_def) |
|
484 |
|
485 |
|
486 lemma OK_iff_Allowed: |
|
487 "OK(I,F) <-> |
|
488 (\<forall>i \<in> I. \<forall>j \<in> I-{i}. programify(F(i)) \<in> Allowed(programify(F(j))))" |
|
489 apply (auto simp add: OK_iff_ok ok_iff_Allowed) |
|
490 done |
|
491 |
|
492 subsection{*safety_prop, for reasoning about given instances of "ok"*} |
|
493 |
|
494 lemma safety_prop_Acts_iff: |
|
495 "safety_prop(X) ==> (Acts(G) \<subseteq> cons(id(state), (\<Union>F \<in> X. Acts(F)))) <-> (programify(G) \<in> X)" |
|
496 apply (simp (no_asm_use) add: safety_prop_def) |
|
497 apply clarify |
|
498 apply (case_tac "G \<in> program", simp_all, blast, safe) |
|
499 prefer 2 apply force |
|
500 apply (force simp add: programify_def) |
|
501 done |
|
502 |
|
503 lemma safety_prop_AllowedActs_iff_Allowed: |
|
504 "safety_prop(X) ==> |
|
505 (\<Union>G \<in> X. Acts(G)) \<subseteq> AllowedActs(F) <-> (X \<subseteq> Allowed(programify(F)))" |
|
506 apply (simp add: Allowed_def safety_prop_Acts_iff [THEN iff_sym] |
|
507 safety_prop_def, blast) |
|
508 done |
|
509 |
|
510 |
|
511 lemma Allowed_eq: |
|
512 "safety_prop(X) ==> Allowed(mk_program(init, acts, \<Union>F \<in> X. Acts(F))) = X" |
|
513 apply (subgoal_tac "cons (id (state), Union (RepFun (X, Acts)) Int Pow (state * state)) = Union (RepFun (X, Acts))") |
|
514 apply (rule_tac [2] equalityI) |
|
515 apply (simp del: UN_simps add: Allowed_def safety_prop_Acts_iff safety_prop_def, auto) |
|
516 apply (force dest: Acts_type [THEN subsetD] simp add: safety_prop_def)+ |
|
517 done |
|
518 |
|
519 lemma def_prg_Allowed: |
|
520 "[| F == mk_program (init, acts, \<Union>F \<in> X. Acts(F)); safety_prop(X) |] |
|
521 ==> Allowed(F) = X" |
|
522 by (simp add: Allowed_eq) |
|
523 |
|
524 (*For safety_prop to hold, the property must be satisfiable!*) |
|
525 lemma safety_prop_constrains [iff]: |
|
526 "safety_prop(A co B) <-> (A \<subseteq> B & st_set(A))" |
|
527 by (simp add: safety_prop_def constrains_def st_set_def, blast) |
|
528 |
|
529 (* To be used with resolution *) |
|
530 lemma safety_prop_constrainsI [iff]: |
|
531 "[| A\<subseteq>B; st_set(A) |] ==>safety_prop(A co B)" |
|
532 by auto |
|
533 |
|
534 lemma safety_prop_stable [iff]: "safety_prop(stable(A)) <-> st_set(A)" |
|
535 by (simp add: stable_def) |
|
536 |
|
537 lemma safety_prop_stableI: "st_set(A) ==> safety_prop(stable(A))" |
|
538 by auto |
|
539 |
|
540 lemma safety_prop_Int [simp]: |
|
541 "[| safety_prop(X) ; safety_prop(Y) |] ==> safety_prop(X Int Y)" |
|
542 apply (simp add: safety_prop_def, safe, blast) |
|
543 apply (drule_tac [2] B = "Union (RepFun (X Int Y, Acts))" and C = "Union (RepFun (Y, Acts))" in subset_trans) |
|
544 apply (drule_tac B = "Union (RepFun (X Int Y, Acts))" and C = "Union (RepFun (X, Acts))" in subset_trans) |
|
545 apply blast+ |
|
546 done |
|
547 |
|
548 (* If I=0 the conclusion becomes safety_prop(0) which is false *) |
|
549 lemma safety_prop_Inter: |
|
550 assumes major: "(!!i. i \<in> I ==>safety_prop(X(i)))" |
|
551 and minor: "i \<in> I" |
|
552 shows "safety_prop(\<Inter>i \<in> I. X(i))" |
|
553 apply (simp add: safety_prop_def) |
|
554 apply (cut_tac minor, safe) |
|
555 apply (simp (no_asm_use) add: Inter_iff) |
|
556 apply clarify |
|
557 apply (frule major) |
|
558 apply (drule_tac [2] i = xa in major) |
|
559 apply (frule_tac [4] i = xa in major) |
|
560 apply (auto simp add: safety_prop_def) |
|
561 apply (drule_tac B = "Union (RepFun (Inter (RepFun (I, X)), Acts))" and C = "Union (RepFun (X (xa), Acts))" in subset_trans) |
|
562 apply blast+ |
|
563 done |
|
564 |
|
565 lemma def_UNION_ok_iff: |
|
566 "[| F == mk_program(init,acts, \<Union>G \<in> X. Acts(G)); safety_prop(X) |] |
|
567 ==> F ok G <-> (programify(G) \<in> X & acts Int Pow(state*state) \<subseteq> AllowedActs(G))" |
|
568 apply (unfold ok_def) |
|
569 apply (drule_tac G = G in safety_prop_Acts_iff) |
|
570 apply (cut_tac F = G in AllowedActs_type) |
|
571 apply (cut_tac F = G in Acts_type, auto) |
|
572 done |
|
573 |
|
574 |
|
575 ML |
|
576 {* |
|
577 val safety_prop_def = thm "safety_prop_def"; |
|
578 |
|
579 val reachable_SKIP = thm "reachable_SKIP"; |
|
580 val ok_programify_left = thm "ok_programify_left"; |
|
581 val ok_programify_right = thm "ok_programify_right"; |
|
582 val Join_programify_left = thm "Join_programify_left"; |
|
583 val Join_programify_right = thm "Join_programify_right"; |
|
584 val SKIP_in_constrains_iff = thm "SKIP_in_constrains_iff"; |
|
585 val SKIP_in_Constrains_iff = thm "SKIP_in_Constrains_iff"; |
|
586 val SKIP_in_stable = thm "SKIP_in_stable"; |
|
587 val SKIP_in_Stable = thm "SKIP_in_Stable"; |
|
588 val Join_in_program = thm "Join_in_program"; |
|
589 val JOIN_in_program = thm "JOIN_in_program"; |
|
590 val Init_Join = thm "Init_Join"; |
|
591 val Acts_Join = thm "Acts_Join"; |
|
592 val AllowedActs_Join = thm "AllowedActs_Join"; |
|
593 val Join_commute = thm "Join_commute"; |
|
594 val Join_left_commute = thm "Join_left_commute"; |
|
595 val Join_assoc = thm "Join_assoc"; |
|
596 val cons_id = thm "cons_id"; |
|
597 val Join_SKIP_left = thm "Join_SKIP_left"; |
|
598 val Join_SKIP_right = thm "Join_SKIP_right"; |
|
599 val Join_absorb = thm "Join_absorb"; |
|
600 val Join_left_absorb = thm "Join_left_absorb"; |
|
601 val OK_programify = thm "OK_programify"; |
|
602 val JN_programify = thm "JN_programify"; |
|
603 val JN_empty = thm "JN_empty"; |
|
604 val Init_JN = thm "Init_JN"; |
|
605 val Acts_JN = thm "Acts_JN"; |
|
606 val AllowedActs_JN = thm "AllowedActs_JN"; |
|
607 val JN_cons = thm "JN_cons"; |
|
608 val JN_cong = thm "JN_cong"; |
|
609 val JN_absorb = thm "JN_absorb"; |
|
610 val JN_Un = thm "JN_Un"; |
|
611 val JN_constant = thm "JN_constant"; |
|
612 val JN_Join_distrib = thm "JN_Join_distrib"; |
|
613 val JN_Join_miniscope = thm "JN_Join_miniscope"; |
|
614 val JN_Join_diff = thm "JN_Join_diff"; |
|
615 val JN_constrains = thm "JN_constrains"; |
|
616 val Join_constrains = thm "Join_constrains"; |
|
617 val Join_unless = thm "Join_unless"; |
|
618 val Join_constrains_weaken = thm "Join_constrains_weaken"; |
|
619 val JN_constrains_weaken = thm "JN_constrains_weaken"; |
|
620 val JN_stable = thm "JN_stable"; |
|
621 val initially_JN_I = thm "initially_JN_I"; |
|
622 val invariant_JN_I = thm "invariant_JN_I"; |
|
623 val Join_stable = thm "Join_stable"; |
|
624 val initially_JoinI = thm "initially_JoinI"; |
|
625 val invariant_JoinI = thm "invariant_JoinI"; |
|
626 val FP_JN = thm "FP_JN"; |
|
627 val JN_transient = thm "JN_transient"; |
|
628 val Join_transient = thm "Join_transient"; |
|
629 val Join_transient_I1 = thm "Join_transient_I1"; |
|
630 val Join_transient_I2 = thm "Join_transient_I2"; |
|
631 val JN_ensures = thm "JN_ensures"; |
|
632 val Join_ensures = thm "Join_ensures"; |
|
633 val stable_Join_constrains = thm "stable_Join_constrains"; |
|
634 val stable_Join_Always1 = thm "stable_Join_Always1"; |
|
635 val stable_Join_Always2 = thm "stable_Join_Always2"; |
|
636 val stable_Join_ensures1 = thm "stable_Join_ensures1"; |
|
637 val stable_Join_ensures2 = thm "stable_Join_ensures2"; |
|
638 val ok_SKIP1 = thm "ok_SKIP1"; |
|
639 val ok_SKIP2 = thm "ok_SKIP2"; |
|
640 val ok_Join_commute = thm "ok_Join_commute"; |
|
641 val ok_commute = thm "ok_commute"; |
|
642 val ok_sym = thm "ok_sym"; |
|
643 val ok_iff_OK = thm "ok_iff_OK"; |
|
644 val ok_Join_iff1 = thm "ok_Join_iff1"; |
|
645 val ok_Join_iff2 = thm "ok_Join_iff2"; |
|
646 val ok_Join_commute_I = thm "ok_Join_commute_I"; |
|
647 val ok_JN_iff1 = thm "ok_JN_iff1"; |
|
648 val ok_JN_iff2 = thm "ok_JN_iff2"; |
|
649 val OK_iff_ok = thm "OK_iff_ok"; |
|
650 val OK_imp_ok = thm "OK_imp_ok"; |
|
651 val Allowed_SKIP = thm "Allowed_SKIP"; |
|
652 val Allowed_Join = thm "Allowed_Join"; |
|
653 val Allowed_JN = thm "Allowed_JN"; |
|
654 val ok_iff_Allowed = thm "ok_iff_Allowed"; |
|
655 val OK_iff_Allowed = thm "OK_iff_Allowed"; |
|
656 val safety_prop_Acts_iff = thm "safety_prop_Acts_iff"; |
|
657 val safety_prop_AllowedActs_iff_Allowed = thm "safety_prop_AllowedActs_iff_Allowed"; |
|
658 val Allowed_eq = thm "Allowed_eq"; |
|
659 val def_prg_Allowed = thm "def_prg_Allowed"; |
|
660 val safety_prop_constrains = thm "safety_prop_constrains"; |
|
661 val safety_prop_constrainsI = thm "safety_prop_constrainsI"; |
|
662 val safety_prop_stable = thm "safety_prop_stable"; |
|
663 val safety_prop_stableI = thm "safety_prop_stableI"; |
|
664 val safety_prop_Int = thm "safety_prop_Int"; |
|
665 val safety_prop_Inter = thm "safety_prop_Inter"; |
|
666 val def_UNION_ok_iff = thm "def_UNION_ok_iff"; |
|
667 |
|
668 val Join_ac = thms "Join_ac"; |
|
669 *} |
|
670 |
54 |
671 |
55 end |
672 end |