author | paulson |
Thu, 02 Jun 2005 13:17:06 +0200 | |
changeset 16183 | 052d9aba392d |
parent 14077 | 37c964462747 |
child 16417 | 9bc16273c2d4 |
permissions | -rw-r--r-- |
11479 | 1 |
(* Title: ZF/UNITY/UNITY.thy |
2 |
ID: $Id$ |
|
3 |
Author: Sidi O Ehmety, Computer Laboratory |
|
4 |
Copyright 2001 University of Cambridge |
|
5 |
*) |
|
6 |
||
14077 | 7 |
header {*The Basic UNITY Theory*} |
8 |
||
9 |
theory UNITY = State: |
|
16183
052d9aba392d
renamed "constrains" to "safety" to avoid keyword clash
paulson
parents:
14077
diff
changeset
|
10 |
|
052d9aba392d
renamed "constrains" to "safety" to avoid keyword clash
paulson
parents:
14077
diff
changeset
|
11 |
text{*The basic UNITY theory (revised version, based upon the "co" operator) |
052d9aba392d
renamed "constrains" to "safety" to avoid keyword clash
paulson
parents:
14077
diff
changeset
|
12 |
From Misra, "A Logic for Concurrent Programming", 1994. |
052d9aba392d
renamed "constrains" to "safety" to avoid keyword clash
paulson
parents:
14077
diff
changeset
|
13 |
|
052d9aba392d
renamed "constrains" to "safety" to avoid keyword clash
paulson
parents:
14077
diff
changeset
|
14 |
This ZF theory was ported from its HOL equivalent.*} |
052d9aba392d
renamed "constrains" to "safety" to avoid keyword clash
paulson
parents:
14077
diff
changeset
|
15 |
|
11479 | 16 |
consts |
16183
052d9aba392d
renamed "constrains" to "safety" to avoid keyword clash
paulson
parents:
14077
diff
changeset
|
17 |
"constrains" :: "[i, i] => i" (infixl "co" 60) |
052d9aba392d
renamed "constrains" to "safety" to avoid keyword clash
paulson
parents:
14077
diff
changeset
|
18 |
op_unless :: "[i, i] => i" (infixl "unless" 60) |
11479 | 19 |
|
20 |
constdefs |
|
14077 | 21 |
program :: i |
12195 | 22 |
"program == {<init, acts, allowed>: |
14077 | 23 |
Pow(state) * Pow(Pow(state*state)) * Pow(Pow(state*state)). |
24 |
id(state) \<in> acts & id(state) \<in> allowed}" |
|
11479 | 25 |
|
14077 | 26 |
mk_program :: "[i,i,i]=>i" |
27 |
--{* The definition yields a program thanks to the coercions |
|
28 |
init \<inter> state, acts \<inter> Pow(state*state), etc. *} |
|
11479 | 29 |
"mk_program(init, acts, allowed) == |
14077 | 30 |
<init \<inter> state, cons(id(state), acts \<inter> Pow(state*state)), |
31 |
cons(id(state), allowed \<inter> Pow(state*state))>" |
|
11479 | 32 |
|
33 |
SKIP :: i |
|
12195 | 34 |
"SKIP == mk_program(state, 0, Pow(state*state))" |
11479 | 35 |
|
12195 | 36 |
(* Coercion from anything to program *) |
14077 | 37 |
programify :: "i=>i" |
38 |
"programify(F) == if F \<in> program then F else SKIP" |
|
12195 | 39 |
|
14077 | 40 |
RawInit :: "i=>i" |
11479 | 41 |
"RawInit(F) == fst(F)" |
14077 | 42 |
|
43 |
Init :: "i=>i" |
|
11479 | 44 |
"Init(F) == RawInit(programify(F))" |
45 |
||
14077 | 46 |
RawActs :: "i=>i" |
12195 | 47 |
"RawActs(F) == cons(id(state), fst(snd(F)))" |
11479 | 48 |
|
14077 | 49 |
Acts :: "i=>i" |
11479 | 50 |
"Acts(F) == RawActs(programify(F))" |
51 |
||
14077 | 52 |
RawAllowedActs :: "i=>i" |
12195 | 53 |
"RawAllowedActs(F) == cons(id(state), snd(snd(F)))" |
11479 | 54 |
|
14077 | 55 |
AllowedActs :: "i=>i" |
11479 | 56 |
"AllowedActs(F) == RawAllowedActs(programify(F))" |
57 |
||
14077 | 58 |
|
59 |
Allowed :: "i =>i" |
|
60 |
"Allowed(F) == {G \<in> program. Acts(G) \<subseteq> AllowedActs(F)}" |
|
11479 | 61 |
|
14077 | 62 |
initially :: "i=>i" |
63 |
"initially(A) == {F \<in> program. Init(F)\<subseteq>A}" |
|
64 |
||
65 |
stable :: "i=>i" |
|
11479 | 66 |
"stable(A) == A co A" |
67 |
||
14077 | 68 |
strongest_rhs :: "[i, i] => i" |
69 |
"strongest_rhs(F, A) == Inter({B \<in> Pow(state). F \<in> A co B})" |
|
11479 | 70 |
|
14077 | 71 |
invariant :: "i => i" |
72 |
"invariant(A) == initially(A) \<inter> stable(A)" |
|
73 |
||
14046 | 74 |
(* meta-function composition *) |
14077 | 75 |
metacomp :: "[i=>i, i=>i] => (i=>i)" (infixl "comp" 65) |
14046 | 76 |
"f comp g == %x. f(g(x))" |
11479 | 77 |
|
14046 | 78 |
pg_compl :: "i=>i" |
79 |
"pg_compl(X)== program - X" |
|
14077 | 80 |
|
11479 | 81 |
defs |
14077 | 82 |
constrains_def: |
83 |
"A co B == {F \<in> program. (\<forall>act \<in> Acts(F). act``A\<subseteq>B) & st_set(A)}" |
|
84 |
--{* the condition @{term "st_set(A)"} makes the definition slightly |
|
85 |
stronger than the HOL one *} |
|
86 |
||
87 |
unless_def: "A unless B == (A - B) co (A Un B)" |
|
88 |
||
89 |
||
16183
052d9aba392d
renamed "constrains" to "safety" to avoid keyword clash
paulson
parents:
14077
diff
changeset
|
90 |
text{*SKIP*} |
14077 | 91 |
lemma SKIP_in_program [iff,TC]: "SKIP \<in> program" |
92 |
by (force simp add: SKIP_def program_def mk_program_def) |
|
93 |
||
94 |
||
95 |
subsection{*The function @{term programify}, the coercion from anything to |
|
96 |
program*} |
|
97 |
||
98 |
lemma programify_program [simp]: "F \<in> program ==> programify(F)=F" |
|
99 |
by (force simp add: programify_def) |
|
100 |
||
101 |
lemma programify_in_program [iff,TC]: "programify(F) \<in> program" |
|
102 |
by (force simp add: programify_def) |
|
103 |
||
16183
052d9aba392d
renamed "constrains" to "safety" to avoid keyword clash
paulson
parents:
14077
diff
changeset
|
104 |
text{*Collapsing rules: to remove programify from expressions*} |
14077 | 105 |
lemma programify_idem [simp]: "programify(programify(F))=programify(F)" |
106 |
by (force simp add: programify_def) |
|
107 |
||
108 |
lemma Init_programify [simp]: "Init(programify(F)) = Init(F)" |
|
109 |
by (simp add: Init_def) |
|
110 |
||
111 |
lemma Acts_programify [simp]: "Acts(programify(F)) = Acts(F)" |
|
112 |
by (simp add: Acts_def) |
|
113 |
||
114 |
lemma AllowedActs_programify [simp]: |
|
115 |
"AllowedActs(programify(F)) = AllowedActs(F)" |
|
116 |
by (simp add: AllowedActs_def) |
|
117 |
||
118 |
subsection{*The Inspectors for Programs*} |
|
119 |
||
120 |
lemma id_in_RawActs: "F \<in> program ==>id(state) \<in> RawActs(F)" |
|
121 |
by (auto simp add: program_def RawActs_def) |
|
122 |
||
123 |
lemma id_in_Acts [iff,TC]: "id(state) \<in> Acts(F)" |
|
124 |
by (simp add: id_in_RawActs Acts_def) |
|
125 |
||
126 |
lemma id_in_RawAllowedActs: "F \<in> program ==>id(state) \<in> RawAllowedActs(F)" |
|
127 |
by (auto simp add: program_def RawAllowedActs_def) |
|
128 |
||
129 |
lemma id_in_AllowedActs [iff,TC]: "id(state) \<in> AllowedActs(F)" |
|
130 |
by (simp add: id_in_RawAllowedActs AllowedActs_def) |
|
131 |
||
132 |
lemma cons_id_Acts [simp]: "cons(id(state), Acts(F)) = Acts(F)" |
|
133 |
by (simp add: cons_absorb) |
|
134 |
||
135 |
lemma cons_id_AllowedActs [simp]: |
|
136 |
"cons(id(state), AllowedActs(F)) = AllowedActs(F)" |
|
137 |
by (simp add: cons_absorb) |
|
138 |
||
139 |
||
140 |
subsection{*Types of the Inspectors*} |
|
141 |
||
142 |
lemma RawInit_type: "F \<in> program ==> RawInit(F)\<subseteq>state" |
|
143 |
by (auto simp add: program_def RawInit_def) |
|
144 |
||
145 |
lemma RawActs_type: "F \<in> program ==> RawActs(F)\<subseteq>Pow(state*state)" |
|
146 |
by (auto simp add: program_def RawActs_def) |
|
147 |
||
148 |
lemma RawAllowedActs_type: |
|
149 |
"F \<in> program ==> RawAllowedActs(F)\<subseteq>Pow(state*state)" |
|
150 |
by (auto simp add: program_def RawAllowedActs_def) |
|
151 |
||
152 |
lemma Init_type: "Init(F)\<subseteq>state" |
|
153 |
by (simp add: RawInit_type Init_def) |
|
154 |
||
155 |
lemmas InitD = Init_type [THEN subsetD, standard] |
|
156 |
||
157 |
lemma st_set_Init [iff]: "st_set(Init(F))" |
|
158 |
apply (unfold st_set_def) |
|
159 |
apply (rule Init_type) |
|
160 |
done |
|
161 |
||
162 |
lemma Acts_type: "Acts(F)\<subseteq>Pow(state*state)" |
|
163 |
by (simp add: RawActs_type Acts_def) |
|
164 |
||
165 |
lemma AllowedActs_type: "AllowedActs(F) \<subseteq> Pow(state*state)" |
|
166 |
by (simp add: RawAllowedActs_type AllowedActs_def) |
|
167 |
||
16183
052d9aba392d
renamed "constrains" to "safety" to avoid keyword clash
paulson
parents:
14077
diff
changeset
|
168 |
text{*Needed in Behaviors*} |
14077 | 169 |
lemma ActsD: "[| act \<in> Acts(F); <s,s'> \<in> act |] ==> s \<in> state & s' \<in> state" |
170 |
by (blast dest: Acts_type [THEN subsetD]) |
|
171 |
||
172 |
lemma AllowedActsD: |
|
173 |
"[| act \<in> AllowedActs(F); <s,s'> \<in> act |] ==> s \<in> state & s' \<in> state" |
|
174 |
by (blast dest: AllowedActs_type [THEN subsetD]) |
|
175 |
||
176 |
subsection{*Simplification rules involving @{term state}, @{term Init}, |
|
177 |
@{term Acts}, and @{term AllowedActs}*} |
|
178 |
||
179 |
text{*But are they really needed?*} |
|
180 |
||
181 |
lemma state_subset_is_Init_iff [iff]: "state \<subseteq> Init(F) <-> Init(F)=state" |
|
182 |
by (cut_tac F = F in Init_type, auto) |
|
183 |
||
184 |
lemma Pow_state_times_state_is_subset_Acts_iff [iff]: |
|
185 |
"Pow(state*state) \<subseteq> Acts(F) <-> Acts(F)=Pow(state*state)" |
|
186 |
by (cut_tac F = F in Acts_type, auto) |
|
187 |
||
188 |
lemma Pow_state_times_state_is_subset_AllowedActs_iff [iff]: |
|
189 |
"Pow(state*state) \<subseteq> AllowedActs(F) <-> AllowedActs(F)=Pow(state*state)" |
|
190 |
by (cut_tac F = F in AllowedActs_type, auto) |
|
191 |
||
192 |
subsubsection{*Eliminating @{text "\<inter> state"} from expressions*} |
|
193 |
||
194 |
lemma Init_Int_state [simp]: "Init(F) \<inter> state = Init(F)" |
|
195 |
by (cut_tac F = F in Init_type, blast) |
|
196 |
||
197 |
lemma state_Int_Init [simp]: "state \<inter> Init(F) = Init(F)" |
|
198 |
by (cut_tac F = F in Init_type, blast) |
|
199 |
||
200 |
lemma Acts_Int_Pow_state_times_state [simp]: |
|
201 |
"Acts(F) \<inter> Pow(state*state) = Acts(F)" |
|
202 |
by (cut_tac F = F in Acts_type, blast) |
|
203 |
||
204 |
lemma state_times_state_Int_Acts [simp]: |
|
205 |
"Pow(state*state) \<inter> Acts(F) = Acts(F)" |
|
206 |
by (cut_tac F = F in Acts_type, blast) |
|
207 |
||
208 |
lemma AllowedActs_Int_Pow_state_times_state [simp]: |
|
209 |
"AllowedActs(F) \<inter> Pow(state*state) = AllowedActs(F)" |
|
210 |
by (cut_tac F = F in AllowedActs_type, blast) |
|
211 |
||
212 |
lemma state_times_state_Int_AllowedActs [simp]: |
|
213 |
"Pow(state*state) \<inter> AllowedActs(F) = AllowedActs(F)" |
|
214 |
by (cut_tac F = F in AllowedActs_type, blast) |
|
215 |
||
216 |
||
16183
052d9aba392d
renamed "constrains" to "safety" to avoid keyword clash
paulson
parents:
14077
diff
changeset
|
217 |
subsubsection{*The Operator @{term mk_program}*} |
14077 | 218 |
|
219 |
lemma mk_program_in_program [iff,TC]: |
|
220 |
"mk_program(init, acts, allowed) \<in> program" |
|
221 |
by (auto simp add: mk_program_def program_def) |
|
222 |
||
223 |
lemma RawInit_eq [simp]: |
|
224 |
"RawInit(mk_program(init, acts, allowed)) = init \<inter> state" |
|
225 |
by (auto simp add: mk_program_def RawInit_def) |
|
226 |
||
227 |
lemma RawActs_eq [simp]: |
|
228 |
"RawActs(mk_program(init, acts, allowed)) = |
|
229 |
cons(id(state), acts \<inter> Pow(state*state))" |
|
230 |
by (auto simp add: mk_program_def RawActs_def) |
|
231 |
||
232 |
lemma RawAllowedActs_eq [simp]: |
|
233 |
"RawAllowedActs(mk_program(init, acts, allowed)) = |
|
234 |
cons(id(state), allowed \<inter> Pow(state*state))" |
|
235 |
by (auto simp add: mk_program_def RawAllowedActs_def) |
|
236 |
||
237 |
lemma Init_eq [simp]: "Init(mk_program(init, acts, allowed)) = init \<inter> state" |
|
238 |
by (simp add: Init_def) |
|
239 |
||
240 |
lemma Acts_eq [simp]: |
|
241 |
"Acts(mk_program(init, acts, allowed)) = |
|
242 |
cons(id(state), acts \<inter> Pow(state*state))" |
|
243 |
by (simp add: Acts_def) |
|
244 |
||
245 |
lemma AllowedActs_eq [simp]: |
|
246 |
"AllowedActs(mk_program(init, acts, allowed))= |
|
247 |
cons(id(state), allowed \<inter> Pow(state*state))" |
|
248 |
by (simp add: AllowedActs_def) |
|
249 |
||
16183
052d9aba392d
renamed "constrains" to "safety" to avoid keyword clash
paulson
parents:
14077
diff
changeset
|
250 |
text{*Init, Acts, and AlowedActs of SKIP *} |
14077 | 251 |
|
252 |
lemma RawInit_SKIP [simp]: "RawInit(SKIP) = state" |
|
253 |
by (simp add: SKIP_def) |
|
254 |
||
255 |
lemma RawAllowedActs_SKIP [simp]: "RawAllowedActs(SKIP) = Pow(state*state)" |
|
256 |
by (force simp add: SKIP_def) |
|
257 |
||
258 |
lemma RawActs_SKIP [simp]: "RawActs(SKIP) = {id(state)}" |
|
259 |
by (force simp add: SKIP_def) |
|
260 |
||
261 |
lemma Init_SKIP [simp]: "Init(SKIP) = state" |
|
262 |
by (force simp add: SKIP_def) |
|
263 |
||
264 |
lemma Acts_SKIP [simp]: "Acts(SKIP) = {id(state)}" |
|
265 |
by (force simp add: SKIP_def) |
|
266 |
||
267 |
lemma AllowedActs_SKIP [simp]: "AllowedActs(SKIP) = Pow(state*state)" |
|
268 |
by (force simp add: SKIP_def) |
|
269 |
||
16183
052d9aba392d
renamed "constrains" to "safety" to avoid keyword clash
paulson
parents:
14077
diff
changeset
|
270 |
text{*Equality of UNITY programs*} |
14077 | 271 |
|
272 |
lemma raw_surjective_mk_program: |
|
273 |
"F \<in> program ==> mk_program(RawInit(F), RawActs(F), RawAllowedActs(F))=F" |
|
274 |
apply (auto simp add: program_def mk_program_def RawInit_def RawActs_def |
|
275 |
RawAllowedActs_def, blast+) |
|
276 |
done |
|
277 |
||
278 |
lemma surjective_mk_program [simp]: |
|
279 |
"mk_program(Init(F), Acts(F), AllowedActs(F)) = programify(F)" |
|
280 |
by (auto simp add: raw_surjective_mk_program Init_def Acts_def AllowedActs_def) |
|
281 |
||
282 |
lemma program_equalityI: |
|
283 |
"[|Init(F) = Init(G); Acts(F) = Acts(G); |
|
284 |
AllowedActs(F) = AllowedActs(G); F \<in> program; G \<in> program |] ==> F = G" |
|
285 |
apply (subgoal_tac "programify(F) = programify(G)") |
|
286 |
apply simp |
|
287 |
apply (simp only: surjective_mk_program [symmetric]) |
|
288 |
done |
|
289 |
||
290 |
lemma program_equalityE: |
|
291 |
"[|F = G; |
|
292 |
[|Init(F) = Init(G); Acts(F) = Acts(G); AllowedActs(F) = AllowedActs(G) |] |
|
293 |
==> P |] |
|
294 |
==> P" |
|
295 |
by force |
|
296 |
||
297 |
||
298 |
lemma program_equality_iff: |
|
299 |
"[| F \<in> program; G \<in> program |] ==>(F=G) <-> |
|
300 |
(Init(F) = Init(G) & Acts(F) = Acts(G) & AllowedActs(F) = AllowedActs(G))" |
|
301 |
by (blast intro: program_equalityI program_equalityE) |
|
302 |
||
303 |
subsection{*These rules allow "lazy" definition expansion*} |
|
304 |
||
305 |
lemma def_prg_Init: |
|
306 |
"F == mk_program (init,acts,allowed) ==> Init(F) = init \<inter> state" |
|
307 |
by auto |
|
308 |
||
309 |
lemma def_prg_Acts: |
|
310 |
"F == mk_program (init,acts,allowed) |
|
311 |
==> Acts(F) = cons(id(state), acts \<inter> Pow(state*state))" |
|
312 |
by auto |
|
313 |
||
314 |
lemma def_prg_AllowedActs: |
|
315 |
"F == mk_program (init,acts,allowed) |
|
316 |
==> AllowedActs(F) = cons(id(state), allowed \<inter> Pow(state*state))" |
|
317 |
by auto |
|
318 |
||
319 |
lemma def_prg_simps: |
|
320 |
"[| F == mk_program (init,acts,allowed) |] |
|
321 |
==> Init(F) = init \<inter> state & |
|
322 |
Acts(F) = cons(id(state), acts \<inter> Pow(state*state)) & |
|
323 |
AllowedActs(F) = cons(id(state), allowed \<inter> Pow(state*state))" |
|
324 |
by auto |
|
325 |
||
326 |
||
16183
052d9aba392d
renamed "constrains" to "safety" to avoid keyword clash
paulson
parents:
14077
diff
changeset
|
327 |
text{*An action is expanded only if a pair of states is being tested against it*} |
14077 | 328 |
lemma def_act_simp: |
329 |
"[| act == {<s,s'> \<in> A*B. P(s, s')} |] |
|
330 |
==> (<s,s'> \<in> act) <-> (<s,s'> \<in> A*B & P(s, s'))" |
|
331 |
by auto |
|
332 |
||
16183
052d9aba392d
renamed "constrains" to "safety" to avoid keyword clash
paulson
parents:
14077
diff
changeset
|
333 |
text{*A set is expanded only if an element is being tested against it*} |
14077 | 334 |
lemma def_set_simp: "A == B ==> (x \<in> A) <-> (x \<in> B)" |
335 |
by auto |
|
336 |
||
337 |
||
338 |
subsection{*The Constrains Operator*} |
|
339 |
||
340 |
lemma constrains_type: "A co B \<subseteq> program" |
|
341 |
by (force simp add: constrains_def) |
|
342 |
||
343 |
lemma constrainsI: |
|
344 |
"[|(!!act s s'. [| act: Acts(F); <s,s'> \<in> act; s \<in> A|] ==> s' \<in> A'); |
|
345 |
F \<in> program; st_set(A) |] ==> F \<in> A co A'" |
|
346 |
by (force simp add: constrains_def) |
|
347 |
||
348 |
lemma constrainsD: |
|
349 |
"F \<in> A co B ==> \<forall>act \<in> Acts(F). act``A\<subseteq>B" |
|
350 |
by (force simp add: constrains_def) |
|
351 |
||
352 |
lemma constrainsD2: "F \<in> A co B ==> F \<in> program & st_set(A)" |
|
353 |
by (force simp add: constrains_def) |
|
354 |
||
355 |
lemma constrains_empty [iff]: "F \<in> 0 co B <-> F \<in> program" |
|
356 |
by (force simp add: constrains_def st_set_def) |
|
357 |
||
358 |
lemma constrains_empty2 [iff]: "(F \<in> A co 0) <-> (A=0 & F \<in> program)" |
|
359 |
by (force simp add: constrains_def st_set_def) |
|
360 |
||
361 |
lemma constrains_state [iff]: "(F \<in> state co B) <-> (state\<subseteq>B & F \<in> program)" |
|
362 |
apply (cut_tac F = F in Acts_type) |
|
363 |
apply (force simp add: constrains_def st_set_def) |
|
364 |
done |
|
365 |
||
366 |
lemma constrains_state2 [iff]: "F \<in> A co state <-> (F \<in> program & st_set(A))" |
|
367 |
apply (cut_tac F = F in Acts_type) |
|
368 |
apply (force simp add: constrains_def st_set_def) |
|
369 |
done |
|
370 |
||
16183
052d9aba392d
renamed "constrains" to "safety" to avoid keyword clash
paulson
parents:
14077
diff
changeset
|
371 |
text{*monotonic in 2nd argument*} |
14077 | 372 |
lemma constrains_weaken_R: |
373 |
"[| F \<in> A co A'; A'\<subseteq>B' |] ==> F \<in> A co B'" |
|
374 |
apply (unfold constrains_def, blast) |
|
375 |
done |
|
376 |
||
16183
052d9aba392d
renamed "constrains" to "safety" to avoid keyword clash
paulson
parents:
14077
diff
changeset
|
377 |
text{*anti-monotonic in 1st argument*} |
14077 | 378 |
lemma constrains_weaken_L: |
379 |
"[| F \<in> A co A'; B\<subseteq>A |] ==> F \<in> B co A'" |
|
380 |
apply (unfold constrains_def st_set_def, blast) |
|
381 |
done |
|
382 |
||
383 |
lemma constrains_weaken: |
|
384 |
"[| F \<in> A co A'; B\<subseteq>A; A'\<subseteq>B' |] ==> F \<in> B co B'" |
|
385 |
apply (drule constrains_weaken_R) |
|
386 |
apply (drule_tac [2] constrains_weaken_L, blast+) |
|
387 |
done |
|
388 |
||
389 |
||
390 |
subsection{*Constrains and Union*} |
|
391 |
||
392 |
lemma constrains_Un: |
|
393 |
"[| F \<in> A co A'; F \<in> B co B' |] ==> F \<in> (A Un B) co (A' Un B')" |
|
394 |
by (auto simp add: constrains_def st_set_def, force) |
|
395 |
||
396 |
lemma constrains_UN: |
|
397 |
"[|!!i. i \<in> I ==> F \<in> A(i) co A'(i); F \<in> program |] |
|
398 |
==> F \<in> (\<Union>i \<in> I. A(i)) co (\<Union>i \<in> I. A'(i))" |
|
399 |
by (force simp add: constrains_def st_set_def) |
|
400 |
||
401 |
lemma constrains_Un_distrib: |
|
402 |
"(A Un B) co C = (A co C) \<inter> (B co C)" |
|
403 |
by (force simp add: constrains_def st_set_def) |
|
404 |
||
405 |
lemma constrains_UN_distrib: |
|
406 |
"i \<in> I ==> (\<Union>i \<in> I. A(i)) co B = (\<Inter>i \<in> I. A(i) co B)" |
|
407 |
by (force simp add: constrains_def st_set_def) |
|
408 |
||
409 |
||
410 |
subsection{*Constrains and Intersection*} |
|
411 |
||
412 |
lemma constrains_Int_distrib: "C co (A \<inter> B) = (C co A) \<inter> (C co B)" |
|
413 |
by (force simp add: constrains_def st_set_def) |
|
414 |
||
415 |
lemma constrains_INT_distrib: |
|
416 |
"x \<in> I ==> A co (\<Inter>i \<in> I. B(i)) = (\<Inter>i \<in> I. A co B(i))" |
|
417 |
by (force simp add: constrains_def st_set_def) |
|
418 |
||
419 |
lemma constrains_Int: |
|
420 |
"[| F \<in> A co A'; F \<in> B co B' |] ==> F \<in> (A \<inter> B) co (A' \<inter> B')" |
|
421 |
by (force simp add: constrains_def st_set_def) |
|
422 |
||
423 |
lemma constrains_INT [rule_format]: |
|
424 |
"[| \<forall>i \<in> I. F \<in> A(i) co A'(i); F \<in> program|] |
|
425 |
==> F \<in> (\<Inter>i \<in> I. A(i)) co (\<Inter>i \<in> I. A'(i))" |
|
426 |
apply (case_tac "I=0") |
|
427 |
apply (simp add: Inter_def) |
|
428 |
apply (erule not_emptyE) |
|
429 |
apply (auto simp add: constrains_def st_set_def, blast) |
|
430 |
apply (drule bspec, assumption, force) |
|
431 |
done |
|
432 |
||
433 |
(* The rule below simulates the HOL's one for (\<Inter>z. A i) co (\<Inter>z. B i) *) |
|
434 |
lemma constrains_All: |
|
435 |
"[| \<forall>z. F:{s \<in> state. P(s, z)} co {s \<in> state. Q(s, z)}; F \<in> program |]==> |
|
436 |
F:{s \<in> state. \<forall>z. P(s, z)} co {s \<in> state. \<forall>z. Q(s, z)}" |
|
437 |
by (unfold constrains_def, blast) |
|
438 |
||
439 |
lemma constrains_imp_subset: |
|
440 |
"[| F \<in> A co A' |] ==> A \<subseteq> A'" |
|
441 |
by (unfold constrains_def st_set_def, force) |
|
442 |
||
16183
052d9aba392d
renamed "constrains" to "safety" to avoid keyword clash
paulson
parents:
14077
diff
changeset
|
443 |
text{*The reasoning is by subsets since "co" refers to single actions |
052d9aba392d
renamed "constrains" to "safety" to avoid keyword clash
paulson
parents:
14077
diff
changeset
|
444 |
only. So this rule isn't that useful.*} |
14077 | 445 |
|
446 |
lemma constrains_trans: "[| F \<in> A co B; F \<in> B co C |] ==> F \<in> A co C" |
|
447 |
by (unfold constrains_def st_set_def, auto, blast) |
|
448 |
||
449 |
lemma constrains_cancel: |
|
450 |
"[| F \<in> A co (A' Un B); F \<in> B co B' |] ==> F \<in> A co (A' Un B')" |
|
451 |
apply (drule_tac A = B in constrains_imp_subset) |
|
452 |
apply (blast intro: constrains_weaken_R) |
|
453 |
done |
|
454 |
||
455 |
||
456 |
subsection{*The Unless Operator*} |
|
457 |
||
458 |
lemma unless_type: "A unless B \<subseteq> program" |
|
459 |
by (force simp add: unless_def constrains_def) |
|
460 |
||
461 |
lemma unlessI: "[| F \<in> (A-B) co (A Un B) |] ==> F \<in> A unless B" |
|
462 |
apply (unfold unless_def) |
|
463 |
apply (blast dest: constrainsD2) |
|
464 |
done |
|
465 |
||
466 |
lemma unlessD: "F :A unless B ==> F \<in> (A-B) co (A Un B)" |
|
467 |
by (unfold unless_def, auto) |
|
468 |
||
469 |
||
470 |
subsection{*The Operator @{term initially}*} |
|
471 |
||
472 |
lemma initially_type: "initially(A) \<subseteq> program" |
|
473 |
by (unfold initially_def, blast) |
|
474 |
||
475 |
lemma initiallyI: "[| F \<in> program; Init(F)\<subseteq>A |] ==> F \<in> initially(A)" |
|
476 |
by (unfold initially_def, blast) |
|
477 |
||
478 |
lemma initiallyD: "F \<in> initially(A) ==> Init(F)\<subseteq>A" |
|
479 |
by (unfold initially_def, blast) |
|
480 |
||
481 |
||
482 |
subsection{*The Operator @{term stable}*} |
|
483 |
||
484 |
lemma stable_type: "stable(A)\<subseteq>program" |
|
485 |
by (unfold stable_def constrains_def, blast) |
|
486 |
||
487 |
lemma stableI: "F \<in> A co A ==> F \<in> stable(A)" |
|
488 |
by (unfold stable_def, assumption) |
|
489 |
||
490 |
lemma stableD: "F \<in> stable(A) ==> F \<in> A co A" |
|
491 |
by (unfold stable_def, assumption) |
|
492 |
||
493 |
lemma stableD2: "F \<in> stable(A) ==> F \<in> program & st_set(A)" |
|
494 |
by (unfold stable_def constrains_def, auto) |
|
495 |
||
496 |
lemma stable_state [simp]: "stable(state) = program" |
|
497 |
by (auto simp add: stable_def constrains_def dest: Acts_type [THEN subsetD]) |
|
498 |
||
499 |
||
500 |
lemma stable_unless: "stable(A)= A unless 0" |
|
501 |
by (auto simp add: unless_def stable_def) |
|
502 |
||
503 |
||
504 |
subsection{*Union and Intersection with @{term stable}*} |
|
505 |
||
506 |
lemma stable_Un: |
|
507 |
"[| F \<in> stable(A); F \<in> stable(A') |] ==> F \<in> stable(A Un A')" |
|
508 |
apply (unfold stable_def) |
|
509 |
apply (blast intro: constrains_Un) |
|
510 |
done |
|
511 |
||
512 |
lemma stable_UN: |
|
513 |
"[|!!i. i\<in>I ==> F \<in> stable(A(i)); F \<in> program |] |
|
514 |
==> F \<in> stable (\<Union>i \<in> I. A(i))" |
|
515 |
apply (unfold stable_def) |
|
516 |
apply (blast intro: constrains_UN) |
|
517 |
done |
|
518 |
||
519 |
lemma stable_Int: |
|
520 |
"[| F \<in> stable(A); F \<in> stable(A') |] ==> F \<in> stable (A \<inter> A')" |
|
521 |
apply (unfold stable_def) |
|
522 |
apply (blast intro: constrains_Int) |
|
523 |
done |
|
524 |
||
525 |
lemma stable_INT: |
|
526 |
"[| !!i. i \<in> I ==> F \<in> stable(A(i)); F \<in> program |] |
|
527 |
==> F \<in> stable (\<Inter>i \<in> I. A(i))" |
|
528 |
apply (unfold stable_def) |
|
529 |
apply (blast intro: constrains_INT) |
|
530 |
done |
|
531 |
||
532 |
lemma stable_All: |
|
533 |
"[|\<forall>z. F \<in> stable({s \<in> state. P(s, z)}); F \<in> program|] |
|
534 |
==> F \<in> stable({s \<in> state. \<forall>z. P(s, z)})" |
|
535 |
apply (unfold stable_def) |
|
536 |
apply (rule constrains_All, auto) |
|
537 |
done |
|
538 |
||
539 |
lemma stable_constrains_Un: |
|
540 |
"[| F \<in> stable(C); F \<in> A co (C Un A') |] ==> F \<in> (C Un A) co (C Un A')" |
|
541 |
apply (unfold stable_def constrains_def st_set_def, auto) |
|
542 |
apply (blast dest!: bspec) |
|
543 |
done |
|
544 |
||
545 |
lemma stable_constrains_Int: |
|
546 |
"[| F \<in> stable(C); F \<in> (C \<inter> A) co A' |] ==> F \<in> (C \<inter> A) co (C \<inter> A')" |
|
547 |
by (unfold stable_def constrains_def st_set_def, blast) |
|
548 |
||
549 |
(* [| F \<in> stable(C); F \<in> (C \<inter> A) co A |] ==> F \<in> stable(C \<inter> A) *) |
|
550 |
lemmas stable_constrains_stable = stable_constrains_Int [THEN stableI, standard] |
|
551 |
||
552 |
subsection{*The Operator @{term invariant}*} |
|
553 |
||
554 |
lemma invariant_type: "invariant(A) \<subseteq> program" |
|
555 |
apply (unfold invariant_def) |
|
556 |
apply (blast dest: stable_type [THEN subsetD]) |
|
557 |
done |
|
558 |
||
559 |
lemma invariantI: "[| Init(F)\<subseteq>A; F \<in> stable(A) |] ==> F \<in> invariant(A)" |
|
560 |
apply (unfold invariant_def initially_def) |
|
561 |
apply (frule stable_type [THEN subsetD], auto) |
|
562 |
done |
|
563 |
||
564 |
lemma invariantD: "F \<in> invariant(A) ==> Init(F)\<subseteq>A & F \<in> stable(A)" |
|
565 |
by (unfold invariant_def initially_def, auto) |
|
566 |
||
567 |
lemma invariantD2: "F \<in> invariant(A) ==> F \<in> program & st_set(A)" |
|
568 |
apply (unfold invariant_def) |
|
569 |
apply (blast dest: stableD2) |
|
570 |
done |
|
571 |
||
572 |
text{*Could also say |
|
573 |
@{term "invariant(A) \<inter> invariant(B) \<subseteq> invariant (A \<inter> B)"}*} |
|
574 |
lemma invariant_Int: |
|
575 |
"[| F \<in> invariant(A); F \<in> invariant(B) |] ==> F \<in> invariant(A \<inter> B)" |
|
576 |
apply (unfold invariant_def initially_def) |
|
577 |
apply (simp add: stable_Int, blast) |
|
578 |
done |
|
579 |
||
580 |
||
581 |
subsection{*The Elimination Theorem*} |
|
582 |
||
583 |
(** The "free" m has become universally quantified! |
|
584 |
Should the premise be !!m instead of \<forall>m ? Would make it harder |
|
585 |
to use in forward proof. **) |
|
586 |
||
16183
052d9aba392d
renamed "constrains" to "safety" to avoid keyword clash
paulson
parents:
14077
diff
changeset
|
587 |
text{*The general case is easier to prove than the special case!*} |
14077 | 588 |
lemma "elimination": |
589 |
"[| \<forall>m \<in> M. F \<in> {s \<in> A. x(s) = m} co B(m); F \<in> program |] |
|
590 |
==> F \<in> {s \<in> A. x(s) \<in> M} co (\<Union>m \<in> M. B(m))" |
|
591 |
by (auto simp add: constrains_def st_set_def, blast) |
|
592 |
||
16183
052d9aba392d
renamed "constrains" to "safety" to avoid keyword clash
paulson
parents:
14077
diff
changeset
|
593 |
text{*As above, but for the special case of A=state*} |
14077 | 594 |
lemma elimination2: |
595 |
"[| \<forall>m \<in> M. F \<in> {s \<in> state. x(s) = m} co B(m); F \<in> program |] |
|
596 |
==> F:{s \<in> state. x(s) \<in> M} co (\<Union>m \<in> M. B(m))" |
|
597 |
by (rule UNITY.elimination, auto) |
|
598 |
||
599 |
subsection{*The Operator @{term strongest_rhs}*} |
|
600 |
||
601 |
lemma constrains_strongest_rhs: |
|
602 |
"[| F \<in> program; st_set(A) |] ==> F \<in> A co (strongest_rhs(F,A))" |
|
603 |
by (auto simp add: constrains_def strongest_rhs_def st_set_def |
|
604 |
dest: Acts_type [THEN subsetD]) |
|
605 |
||
606 |
lemma strongest_rhs_is_strongest: |
|
607 |
"[| F \<in> A co B; st_set(B) |] ==> strongest_rhs(F,A) \<subseteq> B" |
|
608 |
by (auto simp add: constrains_def strongest_rhs_def st_set_def) |
|
609 |
||
610 |
ML |
|
611 |
{* |
|
612 |
val constrains_def = thm "constrains_def"; |
|
613 |
val stable_def = thm "stable_def"; |
|
614 |
val invariant_def = thm "invariant_def"; |
|
615 |
val unless_def = thm "unless_def"; |
|
616 |
val initially_def = thm "initially_def"; |
|
617 |
val SKIP_def = thm "SKIP_def"; |
|
618 |
val Allowed_def = thm "Allowed_def"; |
|
619 |
val programify_def = thm "programify_def"; |
|
620 |
val metacomp_def = thm "metacomp_def"; |
|
621 |
||
622 |
val id_in_Acts = thm "id_in_Acts"; |
|
623 |
val id_in_RawAllowedActs = thm "id_in_RawAllowedActs"; |
|
624 |
val id_in_AllowedActs = thm "id_in_AllowedActs"; |
|
625 |
val cons_id_Acts = thm "cons_id_Acts"; |
|
626 |
val cons_id_AllowedActs = thm "cons_id_AllowedActs"; |
|
627 |
val Init_type = thm "Init_type"; |
|
628 |
val st_set_Init = thm "st_set_Init"; |
|
629 |
val Acts_type = thm "Acts_type"; |
|
630 |
val AllowedActs_type = thm "AllowedActs_type"; |
|
631 |
val ActsD = thm "ActsD"; |
|
632 |
val AllowedActsD = thm "AllowedActsD"; |
|
633 |
val mk_program_in_program = thm "mk_program_in_program"; |
|
634 |
val Init_eq = thm "Init_eq"; |
|
635 |
val Acts_eq = thm "Acts_eq"; |
|
636 |
val AllowedActs_eq = thm "AllowedActs_eq"; |
|
637 |
val Init_SKIP = thm "Init_SKIP"; |
|
638 |
val Acts_SKIP = thm "Acts_SKIP"; |
|
639 |
val AllowedActs_SKIP = thm "AllowedActs_SKIP"; |
|
640 |
val raw_surjective_mk_program = thm "raw_surjective_mk_program"; |
|
641 |
val surjective_mk_program = thm "surjective_mk_program"; |
|
642 |
val program_equalityI = thm "program_equalityI"; |
|
643 |
val program_equalityE = thm "program_equalityE"; |
|
644 |
val program_equality_iff = thm "program_equality_iff"; |
|
645 |
val def_prg_Init = thm "def_prg_Init"; |
|
646 |
val def_prg_Acts = thm "def_prg_Acts"; |
|
647 |
val def_prg_AllowedActs = thm "def_prg_AllowedActs"; |
|
648 |
val def_prg_simps = thm "def_prg_simps"; |
|
649 |
val def_act_simp = thm "def_act_simp"; |
|
650 |
val def_set_simp = thm "def_set_simp"; |
|
651 |
val constrains_type = thm "constrains_type"; |
|
652 |
val constrainsI = thm "constrainsI"; |
|
653 |
val constrainsD = thm "constrainsD"; |
|
654 |
val constrainsD2 = thm "constrainsD2"; |
|
655 |
val constrains_empty = thm "constrains_empty"; |
|
656 |
val constrains_empty2 = thm "constrains_empty2"; |
|
657 |
val constrains_state = thm "constrains_state"; |
|
658 |
val constrains_state2 = thm "constrains_state2"; |
|
659 |
val constrains_weaken_R = thm "constrains_weaken_R"; |
|
660 |
val constrains_weaken_L = thm "constrains_weaken_L"; |
|
661 |
val constrains_weaken = thm "constrains_weaken"; |
|
662 |
val constrains_Un = thm "constrains_Un"; |
|
663 |
val constrains_UN = thm "constrains_UN"; |
|
664 |
val constrains_Un_distrib = thm "constrains_Un_distrib"; |
|
665 |
val constrains_UN_distrib = thm "constrains_UN_distrib"; |
|
666 |
val constrains_Int_distrib = thm "constrains_Int_distrib"; |
|
667 |
val constrains_INT_distrib = thm "constrains_INT_distrib"; |
|
668 |
val constrains_Int = thm "constrains_Int"; |
|
669 |
val constrains_INT = thm "constrains_INT"; |
|
670 |
val constrains_All = thm "constrains_All"; |
|
671 |
val constrains_imp_subset = thm "constrains_imp_subset"; |
|
672 |
val constrains_trans = thm "constrains_trans"; |
|
673 |
val constrains_cancel = thm "constrains_cancel"; |
|
674 |
val unless_type = thm "unless_type"; |
|
675 |
val unlessI = thm "unlessI"; |
|
676 |
val unlessD = thm "unlessD"; |
|
677 |
val initially_type = thm "initially_type"; |
|
678 |
val initiallyI = thm "initiallyI"; |
|
679 |
val initiallyD = thm "initiallyD"; |
|
680 |
val stable_type = thm "stable_type"; |
|
681 |
val stableI = thm "stableI"; |
|
682 |
val stableD = thm "stableD"; |
|
683 |
val stableD2 = thm "stableD2"; |
|
684 |
val stable_state = thm "stable_state"; |
|
685 |
val stable_unless = thm "stable_unless"; |
|
686 |
val stable_Un = thm "stable_Un"; |
|
687 |
val stable_UN = thm "stable_UN"; |
|
688 |
val stable_Int = thm "stable_Int"; |
|
689 |
val stable_INT = thm "stable_INT"; |
|
690 |
val stable_All = thm "stable_All"; |
|
691 |
val stable_constrains_Un = thm "stable_constrains_Un"; |
|
692 |
val stable_constrains_Int = thm "stable_constrains_Int"; |
|
693 |
val invariant_type = thm "invariant_type"; |
|
694 |
val invariantI = thm "invariantI"; |
|
695 |
val invariantD = thm "invariantD"; |
|
696 |
val invariantD2 = thm "invariantD2"; |
|
697 |
val invariant_Int = thm "invariant_Int"; |
|
698 |
val elimination = thm "elimination"; |
|
699 |
val elimination2 = thm "elimination2"; |
|
700 |
val constrains_strongest_rhs = thm "constrains_strongest_rhs"; |
|
701 |
val strongest_rhs_is_strongest = thm "strongest_rhs_is_strongest"; |
|
702 |
||
703 |
fun simp_of_act def = def RS def_act_simp; |
|
704 |
fun simp_of_set def = def RS def_set_simp; |
|
705 |
*} |
|
706 |
||
11479 | 707 |
end |