author | berghofe |
Mon, 12 Nov 2001 10:37:36 +0100 | |
changeset 12152 | 46f128d8133c |
parent 11479 | 697dcaaf478f |
child 12195 | ed2893765a08 |
permissions | -rw-r--r-- |
11479 | 1 |
(* Title: ZF/UNITY/UNITY.ML |
2 |
ID: $Id$ |
|
3 |
Author: Sidi O Ehmety, Computer Laboratory |
|
4 |
Copyright 2001 University of Cambridge |
|
5 |
||
6 |
The basic UNITY theory (revised version, based upon the "co" operator) |
|
7 |
From Misra, "A Logic for Concurrent Programming", 1994 |
|
8 |
||
9 |
Proofs ported from HOL |
|
10 |
*) |
|
11 |
||
12 |
(** SKIP **) |
|
13 |
Goal "SKIP:program"; |
|
14 |
by (auto_tac (claset(), simpset() addsimps |
|
15 |
[SKIP_def, program_def, mk_program_def, actionSet_def, cons_absorb])); |
|
16 |
qed "SKIP_type"; |
|
17 |
AddIffs [SKIP_type]; |
|
18 |
AddTCs [SKIP_type]; |
|
19 |
||
20 |
(** programify: coersion from anything to program **) |
|
21 |
||
22 |
Goalw [programify_def] |
|
23 |
"F:program ==> programify(F)=F"; |
|
24 |
by Auto_tac; |
|
25 |
qed "programify_program"; |
|
26 |
Addsimps [programify_program]; |
|
27 |
||
28 |
Goalw [programify_def] |
|
29 |
"programify(F):program"; |
|
30 |
by Auto_tac; |
|
31 |
qed "programify_in_program"; |
|
32 |
AddIffs [programify_in_program]; |
|
33 |
AddTCs [programify_in_program]; |
|
34 |
||
35 |
(** Collapsing rules: to remove programify from expressions **) |
|
36 |
Goalw [programify_def] |
|
37 |
"programify(programify(F))=programify(F)"; |
|
38 |
by Auto_tac; |
|
39 |
qed "programify_idem"; |
|
40 |
Addsimps [programify_idem]; |
|
41 |
||
42 |
Goal |
|
43 |
"Init(programify(F)) = Init(F)"; |
|
44 |
by (simp_tac (simpset() addsimps [Init_def]) 1); |
|
45 |
qed "Init_programify"; |
|
46 |
||
47 |
Goal |
|
48 |
"Acts(programify(F)) = Acts(F)"; |
|
49 |
by (simp_tac (simpset() addsimps [Acts_def]) 1); |
|
50 |
qed "Acts_programify"; |
|
51 |
||
52 |
Goal |
|
53 |
"AllowedActs(programify(F)) = AllowedActs(F)"; |
|
54 |
by (simp_tac (simpset() addsimps [AllowedActs_def]) 1); |
|
55 |
qed "AllowedActs_programify"; |
|
56 |
||
57 |
Addsimps [Init_programify,Acts_programify,AllowedActs_programify]; |
|
58 |
||
59 |
(** program inspectors **) |
|
60 |
||
61 |
Goal "F:program ==>Id:RawActs(F)"; |
|
62 |
by (auto_tac (claset(), simpset() |
|
63 |
addsimps [program_def, RawActs_def])); |
|
64 |
qed "Id_in_RawActs"; |
|
65 |
||
66 |
Goal "Id:Acts(F)"; |
|
67 |
by (simp_tac (simpset() |
|
68 |
addsimps [Id_in_RawActs, Acts_def]) 1); |
|
69 |
qed "Id_in_Acts"; |
|
70 |
||
71 |
Goal "F:program ==>Id:RawAllowedActs(F)"; |
|
72 |
by (auto_tac (claset(), simpset() |
|
73 |
addsimps [program_def, RawAllowedActs_def])); |
|
74 |
qed "Id_in_RawAllowedActs"; |
|
75 |
||
76 |
Goal "Id:AllowedActs(F)"; |
|
77 |
by (simp_tac (simpset() |
|
78 |
addsimps [Id_in_RawAllowedActs, AllowedActs_def]) 1); |
|
79 |
qed "Id_in_AllowedActs"; |
|
80 |
||
81 |
AddIffs [Id_in_Acts, Id_in_AllowedActs]; |
|
82 |
AddTCs [Id_in_Acts, Id_in_AllowedActs]; |
|
83 |
||
84 |
Goal "cons(Id, Acts(F)) = Acts(F)"; |
|
85 |
by (simp_tac (simpset() addsimps [cons_absorb]) 1); |
|
86 |
qed "cons_Id_Acts"; |
|
87 |
||
88 |
Goal "cons(Id, AllowedActs(F)) = AllowedActs(F)"; |
|
89 |
by (simp_tac (simpset() addsimps [cons_absorb]) 1); |
|
90 |
qed "cons_Id_AllowedActs"; |
|
91 |
||
92 |
Addsimps [cons_Id_Acts, cons_Id_AllowedActs]; |
|
93 |
||
94 |
(** inspectors's types **) |
|
95 |
Goal |
|
96 |
"F:program ==> RawInit(F):condition"; |
|
97 |
by (auto_tac (claset(), simpset() |
|
98 |
addsimps [program_def, RawInit_def])); |
|
99 |
qed "RawInit_type"; |
|
100 |
||
101 |
Goal "Init(F):condition"; |
|
102 |
by (simp_tac (simpset() |
|
103 |
addsimps [RawInit_type, Init_def]) 1); |
|
104 |
qed "Init_type"; |
|
105 |
||
106 |
Goal |
|
107 |
"F:program ==> RawActs(F):actionSet"; |
|
108 |
by (auto_tac (claset(), simpset() |
|
109 |
addsimps [program_def, RawActs_def, actionSet_def])); |
|
110 |
qed "RawActs_type"; |
|
111 |
||
112 |
Goal |
|
113 |
"Acts(F):actionSet"; |
|
114 |
by (simp_tac (simpset() |
|
115 |
addsimps [RawActs_type, Acts_def]) 1); |
|
116 |
qed "Acts_type"; |
|
117 |
||
118 |
Goal |
|
119 |
"F:program ==> RawAllowedActs(F):actionSet"; |
|
120 |
by (auto_tac (claset(), simpset() |
|
121 |
addsimps [program_def, RawAllowedActs_def, actionSet_def])); |
|
122 |
qed "RawAllowedActs_type"; |
|
123 |
||
124 |
Goal |
|
125 |
"AllowedActs(F): actionSet"; |
|
126 |
by (simp_tac (simpset() |
|
127 |
addsimps [RawAllowedActs_type, AllowedActs_def]) 1); |
|
128 |
qed "AllowedActs_type"; |
|
129 |
||
130 |
AddIffs [Init_type, Acts_type, AllowedActs_type]; |
|
131 |
AddTCs [Init_type, Acts_type, AllowedActs_type]; |
|
132 |
||
133 |
Goal "x:Init(F) ==> x:state"; |
|
134 |
by (cut_inst_tac [("F", "F")] Init_type 1); |
|
135 |
by (auto_tac (claset(), simpset() addsimps [condition_def])); |
|
136 |
qed "InitD"; |
|
137 |
||
138 |
Goal "act:Acts(F) ==> act<=state*state"; |
|
139 |
by (cut_inst_tac [("F", "F")] Acts_type 1); |
|
140 |
by (rewrite_goals_tac [actionSet_def]); |
|
141 |
by Auto_tac; |
|
142 |
qed "ActsD"; |
|
143 |
||
144 |
||
145 |
Goal "act:AllowedActs(F) ==> act<=state*state"; |
|
146 |
by (cut_inst_tac [("F", "F")] AllowedActs_type 1); |
|
147 |
by (rewrite_goals_tac [actionSet_def]); |
|
148 |
by Auto_tac; |
|
149 |
qed "AllowedActsD"; |
|
150 |
||
151 |
(** More simplification rules involving state |
|
152 |
and Init, Acts, and AllowedActs **) |
|
153 |
||
154 |
Goal "state <= Init(F) <-> Init(F)=state"; |
|
155 |
by (cut_inst_tac [("F", "F")] Init_type 1); |
|
156 |
by (auto_tac (claset(), |
|
157 |
simpset() addsimps [condition_def])); |
|
158 |
qed "Init_state_eq"; |
|
159 |
||
160 |
Goal "action <= Acts(F) <-> Acts(F)=action"; |
|
161 |
by (cut_inst_tac [("F", "F")] Acts_type 1); |
|
162 |
by (auto_tac (claset(), |
|
163 |
simpset() addsimps [actionSet_def])); |
|
164 |
qed "Acts_action_eq"; |
|
165 |
||
166 |
Goal "action <= AllowedActs(F) <-> AllowedActs(F)=action"; |
|
167 |
by (cut_inst_tac [("F", "F")] AllowedActs_type 1); |
|
168 |
by (auto_tac (claset(), |
|
169 |
simpset() addsimps [actionSet_def])); |
|
170 |
qed "AllowedActs_action_eq"; |
|
171 |
||
172 |
(** Eliminating `Int state' from expressions **) |
|
173 |
Goal |
|
174 |
"Init(F) Int state = Init(F)"; |
|
175 |
by (cut_inst_tac [("F", "F")] Init_type 1); |
|
176 |
by (auto_tac (claset(), |
|
177 |
simpset() addsimps [condition_def])); |
|
178 |
qed "Init_Int_state"; |
|
179 |
||
180 |
Goal |
|
181 |
"state Int Init(F) = Init(F)"; |
|
182 |
by (stac (Int_commute) 1); |
|
183 |
by (simp_tac (simpset() |
|
184 |
addsimps [Init_Int_state]) 1); |
|
185 |
qed "Init_Int_state2"; |
|
186 |
||
187 |
Goal |
|
188 |
"Acts(F) Int action = Acts(F)"; |
|
189 |
by (cut_inst_tac [("F", "F")] Acts_type 1); |
|
190 |
by (auto_tac (claset(), |
|
191 |
simpset() addsimps [actionSet_def])); |
|
192 |
qed "Acts_Int_action"; |
|
193 |
||
194 |
Goal |
|
195 |
"action Int Acts(F) = Acts(F)"; |
|
196 |
by (simp_tac (simpset() addsimps |
|
197 |
[Int_commute, Acts_Int_action]) 1); |
|
198 |
qed "Acts_Int_action2"; |
|
199 |
||
200 |
Goal |
|
201 |
"AllowedActs(F) Int action = AllowedActs(F)"; |
|
202 |
by (cut_inst_tac [("F", "F")] AllowedActs_type 1); |
|
203 |
by (auto_tac (claset(), |
|
204 |
simpset() addsimps [actionSet_def])); |
|
205 |
qed "AllowedActs_Int_action"; |
|
206 |
||
207 |
Goal |
|
208 |
"action Int AllowedActs(F) = AllowedActs(F)"; |
|
209 |
by (simp_tac (simpset() addsimps |
|
210 |
[Int_commute, AllowedActs_Int_action]) 1); |
|
211 |
qed "AllowedActs_Int_action2"; |
|
212 |
||
213 |
Addsimps |
|
214 |
[Init_state_eq, Acts_action_eq, AllowedActs_action_eq, |
|
215 |
Init_Int_state, Init_Int_state2, Acts_Int_action, Acts_Int_action2, |
|
216 |
AllowedActs_Int_action,AllowedActs_Int_action2]; |
|
217 |
||
218 |
(** mk_program **) |
|
219 |
||
220 |
Goal "mk_program(init, acts, allowed):program"; |
|
221 |
by (auto_tac (claset(), simpset() |
|
222 |
addsimps [program_def, mk_program_def, condition_def, actionSet_def])); |
|
223 |
qed "mk_program_type"; |
|
224 |
AddIffs [mk_program_type]; |
|
225 |
AddTCs [mk_program_type]; |
|
226 |
||
227 |
Goal "RawInit(mk_program(init, acts, allowed)) = init Int state"; |
|
228 |
by (auto_tac (claset(), simpset() |
|
229 |
addsimps [RawInit_def, mk_program_def])); |
|
230 |
qed "RawInit_eq"; |
|
231 |
||
232 |
Goal "Init(mk_program(init, acts, allowed)) = init Int state"; |
|
233 |
by (auto_tac (claset(), simpset() |
|
234 |
addsimps [Init_def, RawInit_eq])); |
|
235 |
qed "Init_eq"; |
|
236 |
Addsimps [Init_eq]; |
|
237 |
||
238 |
Goalw [RawActs_def] |
|
239 |
"RawActs(mk_program(init, acts, allowed)) \ |
|
240 |
\ = cons(Id, acts Int Pow(state*state))"; |
|
241 |
by (auto_tac (claset(), simpset() |
|
242 |
addsimps [mk_program_def])); |
|
243 |
qed "RawActs_eq"; |
|
244 |
||
245 |
Goalw [Acts_def] |
|
246 |
"Acts(mk_program(init, acts, allowed)) \ |
|
247 |
\ = cons(Id, acts Int Pow(state*state))"; |
|
248 |
by (auto_tac (claset(), |
|
249 |
simpset() addsimps [RawActs_eq])); |
|
250 |
qed "Acts_eq"; |
|
251 |
Addsimps [Acts_eq]; |
|
252 |
||
253 |
Goalw [RawAllowedActs_def] |
|
254 |
"RawAllowedActs(mk_program(init, acts, allowed)) \ |
|
255 |
\ = cons(Id, allowed Int action)"; |
|
256 |
by (auto_tac (claset(), |
|
257 |
simpset() addsimps [mk_program_def])); |
|
258 |
qed "RawAllowedActs_eq"; |
|
259 |
||
260 |
Goalw [AllowedActs_def] |
|
261 |
"AllowedActs(mk_program(init, acts, allowed)) \ |
|
262 |
\ = cons(Id, allowed Int action)"; |
|
263 |
by (auto_tac (claset(), |
|
264 |
simpset() addsimps [RawAllowedActs_eq])); |
|
265 |
qed "AllowedActs_eq"; |
|
266 |
Addsimps [AllowedActs_eq]; |
|
267 |
||
268 |
||
269 |
(**Init, Acts, and AlowedActs of SKIP **) |
|
270 |
||
271 |
Goal "RawInit(SKIP) = state"; |
|
272 |
by (auto_tac (claset(), simpset() |
|
273 |
addsimps [SKIP_def, RawInit_eq])); |
|
274 |
qed "RawInit_SKIP"; |
|
275 |
||
276 |
Goal "Init(SKIP) = state"; |
|
277 |
by (simp_tac (simpset() |
|
278 |
addsimps [Init_def, RawInit_SKIP]) 1); |
|
279 |
qed "Init_SKIP"; |
|
280 |
Addsimps [Init_SKIP]; |
|
281 |
||
282 |
Goal "RawActs(SKIP) = {Id}"; |
|
283 |
by (auto_tac (claset(), simpset() |
|
284 |
addsimps [SKIP_def, RawActs_eq])); |
|
285 |
qed "RawActs_SKIP"; |
|
286 |
||
287 |
||
288 |
Goal "Acts(SKIP) = {Id}"; |
|
289 |
by (simp_tac (simpset() |
|
290 |
addsimps [Acts_def, RawActs_SKIP]) 1); |
|
291 |
qed "Acts_SKIP"; |
|
292 |
Addsimps [Acts_SKIP]; |
|
293 |
||
294 |
Goal "RawAllowedActs(SKIP) = action"; |
|
295 |
by (auto_tac (claset(), simpset() |
|
296 |
addsimps [SKIP_def, RawAllowedActs_eq])); |
|
297 |
qed "RawAllowedActs_SKIP"; |
|
298 |
||
299 |
Goal "AllowedActs(SKIP) = action"; |
|
300 |
by (simp_tac (simpset() |
|
301 |
addsimps [AllowedActs_def, RawAllowedActs_SKIP]) 1); |
|
302 |
qed "AllowedActs_SKIP"; |
|
303 |
Addsimps [AllowedActs_SKIP]; |
|
304 |
||
305 |
(** Equality for UNITY programs **) |
|
306 |
||
307 |
Goal |
|
308 |
"F:program ==> mk_program(RawInit(F), RawActs(F), RawAllowedActs(F))=F"; |
|
309 |
by (auto_tac (claset(), simpset() addsimps |
|
310 |
[program_def, mk_program_def, RawInit_def, |
|
311 |
RawActs_def, RawAllowedActs_def, actionSet_def, condition_def])); |
|
312 |
by (REPEAT(Blast_tac 1)); |
|
313 |
qed "raw_surjective_mk_program"; |
|
314 |
||
315 |
Goal |
|
316 |
"mk_program(Init(F), Acts(F), AllowedActs(F)) = programify(F)"; |
|
317 |
by (auto_tac (claset(), simpset() addsimps |
|
318 |
[Init_def, Acts_def, AllowedActs_def, |
|
319 |
raw_surjective_mk_program])); |
|
320 |
qed "surjective_mk_program"; |
|
321 |
||
322 |
||
323 |
Goal "[|Init(F) = Init(G); Acts(F) = Acts(G); \ |
|
324 |
\ AllowedActs(F) = AllowedActs(G); F:program; G:program |] ==> F = G"; |
|
325 |
by (stac (programify_program RS sym) 1); |
|
326 |
by (rtac sym 2); |
|
327 |
by (stac (programify_program RS sym) 2); |
|
328 |
by (stac (surjective_mk_program RS sym) 3); |
|
329 |
by (stac (surjective_mk_program RS sym) 3); |
|
330 |
by (ALLGOALS(Asm_simp_tac)); |
|
331 |
qed "program_equalityI"; |
|
332 |
||
333 |
val [major,minor] = |
|
334 |
Goal "[| F = G; \ |
|
335 |
\ [| Init(F) = Init(G); Acts(F) = Acts(G); AllowedActs(F) = AllowedActs(G) |]\ |
|
336 |
\ ==> P |] ==> P"; |
|
337 |
by (rtac minor 1); |
|
338 |
by (auto_tac (claset(), simpset() addsimps [major])); |
|
339 |
qed "program_equalityE"; |
|
340 |
||
341 |
||
342 |
Goal "[| F:program; G:program |] ==>(F=G) <-> \ |
|
343 |
\ (Init(F) = Init(G) & Acts(F) = Acts(G) & AllowedActs(F) = AllowedActs(G))"; |
|
344 |
by (blast_tac (claset() addIs [program_equalityI, program_equalityE]) 1); |
|
345 |
qed "program_equality_iff"; |
|
346 |
||
347 |
Addsimps [surjective_mk_program]; |
|
348 |
||
349 |
(*** These rules allow "lazy" definition expansion |
|
350 |
||
351 |
...skipping 1 line |
|
352 |
||
353 |
***) |
|
354 |
||
355 |
Goal "F == mk_program (init,acts,allowed) ==> Init(F) = init Int state"; |
|
356 |
by Auto_tac; |
|
357 |
qed "def_prg_Init"; |
|
358 |
||
359 |
||
360 |
Goal "F == mk_program (init,acts,allowed) ==> Acts(F) = cons(Id, acts Int action)"; |
|
361 |
by Auto_tac; |
|
362 |
qed "def_prg_Acts"; |
|
363 |
||
364 |
||
365 |
Goal "F == mk_program (init,acts,allowed) ==> \ |
|
366 |
\ AllowedActs(F) = cons(Id, allowed Int action)"; |
|
367 |
by Auto_tac; |
|
368 |
qed "def_prg_AllowedActs"; |
|
369 |
||
370 |
||
371 |
val [rew] = goal thy |
|
372 |
"[| F == mk_program (init,acts,allowed) |] \ |
|
373 |
\ ==> Init(F) = init Int state & Acts(F) = cons(Id, acts Int action)"; |
|
374 |
by (rewtac rew); |
|
375 |
by Auto_tac; |
|
376 |
qed "def_prg_simps"; |
|
377 |
||
378 |
||
379 |
(*An action is expanded only if a pair of states is being tested against it*) |
|
380 |
Goal "[| act == {<s,s'>:A*B. P(s, s')} |] ==> \ |
|
381 |
\ (<s,s'>:act) <-> (<s,s'>:A*B & P(s, s'))"; |
|
382 |
by Auto_tac; |
|
383 |
qed "def_act_simp"; |
|
384 |
||
385 |
fun simp_of_act def = def RS def_act_simp; |
|
386 |
||
387 |
(*A set is expanded only if an element is being tested against it*) |
|
388 |
Goal "A == B ==> (x : A) <-> (x : B)"; |
|
389 |
by Auto_tac; |
|
390 |
qed "def_set_simp"; |
|
391 |
||
392 |
fun simp_of_set def = def RS def_set_simp; |
|
393 |
||
394 |
(*** co ***) |
|
395 |
||
396 |
val prems = Goalw [constrains_def] |
|
397 |
"[|(!!act s s'. [| act: Acts(F); <s,s'>:act; s:A|] ==> s':A'); \ |
|
398 |
\ F:program; A:condition; A':condition |] ==> F:A co A'"; |
|
399 |
by (blast_tac(claset() addIs prems) 1); |
|
400 |
qed "constrainsI"; |
|
401 |
||
402 |
Goalw [constrains_def] |
|
403 |
"F:A co B ==> ALL act:Acts(F). act``A<=B"; |
|
404 |
by (Blast_tac 1); |
|
405 |
qed "constrainsD"; |
|
406 |
||
407 |
Goalw [constrains_def] |
|
408 |
"F:A co B ==> F:program & A:condition & B:condition"; |
|
409 |
by (Blast_tac 1); |
|
410 |
qed "constrainsD2"; |
|
411 |
||
412 |
Goalw [constrains_def] |
|
413 |
"[| F:program; B:condition |] ==> F : 0 co B"; |
|
414 |
by (Blast_tac 1); |
|
415 |
qed "constrains_empty"; |
|
416 |
||
417 |
Goalw [constrains_def] |
|
418 |
"[| F:program; A:condition |] ==>(F : A co 0) <-> (A=0)"; |
|
419 |
by (auto_tac (claset() addSDs [bspec], |
|
420 |
simpset() addsimps [condition_def])); |
|
421 |
qed "constrains_empty2"; |
|
422 |
||
423 |
Goalw [constrains_def] |
|
424 |
"[| F:program; B:condition |] ==> (F: state co B) <-> (B = state)"; |
|
425 |
by (auto_tac (claset() addSDs [bspec] addDs [ActsD], |
|
426 |
simpset() addsimps [condition_def])); |
|
427 |
qed "constrains_state"; |
|
428 |
||
429 |
||
430 |
Goalw [constrains_def] |
|
431 |
"[| F:program; A:condition |] ==> F : A co state"; |
|
432 |
by (auto_tac (claset() addDs [ActsD], simpset())); |
|
433 |
qed "constrains_state2"; |
|
434 |
||
435 |
Addsimps [constrains_empty, constrains_empty2, |
|
436 |
constrains_state, constrains_state2]; |
|
437 |
||
438 |
(*monotonic in 2nd argument*) |
|
439 |
Goalw [constrains_def] |
|
440 |
"[| F:A co A'; A'<=B'; B':condition |] ==> F : A co B'"; |
|
441 |
by (Blast_tac 1); |
|
442 |
qed "constrains_weaken_R"; |
|
443 |
||
444 |
(*anti-monotonic in 1st argument*) |
|
445 |
Goalw [constrains_def, condition_def] |
|
446 |
"[| F : A co A'; B<=A |] ==> F : B co A'"; |
|
447 |
by (Blast_tac 1); |
|
448 |
qed "constrains_weaken_L"; |
|
449 |
||
450 |
Goal |
|
451 |
"[| F : A co A'; B<=A; A'<=B'; B':condition |] ==> F : B co B'"; |
|
452 |
by (dtac constrains_weaken_R 1); |
|
453 |
by (dtac constrains_weaken_L 3); |
|
454 |
by (REPEAT(Blast_tac 1)); |
|
455 |
qed "constrains_weaken"; |
|
456 |
||
457 |
(** Union **) |
|
458 |
||
459 |
Goalw [constrains_def] |
|
460 |
"[| F : A co A'; F:B co B' |] ==> F:(A Un B) co (A' Un B')"; |
|
461 |
by (Asm_full_simp_tac 1); |
|
462 |
by (Blast_tac 1); |
|
463 |
qed "constrains_Un"; |
|
464 |
||
465 |
Goalw [constrains_def] |
|
466 |
"[| F : A co A'; F:B co B' |] ==> F:(A Un B) co (A' Un B')"; |
|
467 |
by Auto_tac; |
|
468 |
by (asm_full_simp_tac |
|
469 |
(simpset() addsimps [condition_def]) 1); |
|
470 |
by (Blast_tac 1); |
|
471 |
qed "constrains_Un"; |
|
472 |
||
473 |
Goalw [constrains_def] |
|
474 |
"[| ALL i:I. F:A(i) co A'(i); F:program |] ==> \ |
|
475 |
\ F:(UN i:I. A(i)) co (UN i:I. A'(i))"; |
|
476 |
by (Clarify_tac 1); |
|
477 |
by (Blast_tac 1); |
|
478 |
bind_thm ("constrains_UN", ballI RS result()); |
|
479 |
||
480 |
||
481 |
Goalw [constrains_def] |
|
482 |
"(A Un B) co C = (A co C) Int (B co C)"; |
|
483 |
by (rtac equalityI 1); |
|
484 |
by (ALLGOALS(Asm_full_simp_tac)); |
|
485 |
by (ALLGOALS(Blast_tac)); |
|
486 |
qed "constrains_Un_distrib"; |
|
487 |
||
488 |
||
489 |
Goalw [constrains_def] |
|
490 |
"i:I ==> (UN i:I. A(i)) co B = (INT i:I. A(i) co B)"; |
|
491 |
by (rtac equalityI 1); |
|
492 |
by Safe_tac; |
|
493 |
by (ALLGOALS(Asm_full_simp_tac)); |
|
494 |
by (ALLGOALS(Blast_tac)); |
|
495 |
qed "constrains_UN_distrib"; |
|
496 |
||
497 |
Goalw [constrains_def] |
|
498 |
"[| A:condition; B:condition |] \ |
|
499 |
\ ==> C co (A Int B) = (C co A) Int (C co B)"; |
|
500 |
by (rtac equalityI 1); |
|
501 |
by (ALLGOALS(Clarify_tac)); |
|
502 |
by (ALLGOALS(Blast_tac)); |
|
503 |
qed "constrains_Int_distrib"; |
|
504 |
||
505 |
Goalw [constrains_def] "[| i:I; ALL i:I. B(i):condition |] ==> \ |
|
506 |
\ A co (INT i:I. B(i)) = (INT i:I. A co B(i))"; |
|
507 |
by (rtac equalityI 1); |
|
508 |
by Safe_tac; |
|
509 |
by (ALLGOALS(Blast_tac)); |
|
510 |
qed "constrains_INT_distrib"; |
|
511 |
||
512 |
(** Intersection **) |
|
513 |
||
514 |
Goalw [constrains_def] |
|
515 |
"[| F : A co A'; F : B co B' |] ==> F : (A Int B) co (A' Int B')"; |
|
516 |
by (Clarify_tac 1); |
|
517 |
by (Blast_tac 1); |
|
518 |
qed "constrains_Int"; |
|
519 |
||
520 |
Goalw [constrains_def] |
|
521 |
"[| ALL i:I. F : A(i) co A'(i); F:program |] \ |
|
522 |
\ ==> F : (INT i:I. A(i)) co (INT i:I. A'(i))"; |
|
523 |
by (case_tac "I=0" 1); |
|
524 |
by (asm_full_simp_tac (simpset() addsimps [Inter_def]) 1); |
|
525 |
by (etac not_emptyE 1); |
|
526 |
by Safe_tac; |
|
527 |
by (dres_inst_tac [("x", "xd")] bspec 1); |
|
528 |
by (ALLGOALS(Blast_tac)); |
|
529 |
bind_thm ("constrains_INT", ballI RS result()); |
|
530 |
||
531 |
||
532 |
(* This rule simulates the HOL's one for (INT z. A i) co (INT z. B i) *) |
|
533 |
||
534 |
Goalw [constrains_def, condition_def] |
|
535 |
"[| ALL z. F: {s:state. P(s, z)} co {s:state. Q(s, z)}; F:program |] ==> \ |
|
536 |
\ F: {s:state. ALL z. P(s, z)} co {s:state. ALL z. Q(s, z)}"; |
|
537 |
by (auto_tac (claset() addSDs [bspec] addDs [ActsD], |
|
538 |
simpset() addsimps [condition_def])); |
|
539 |
by (Blast_tac 1); |
|
540 |
bind_thm ("constrains_All", allI RS result()); |
|
541 |
||
542 |
Goalw [constrains_def] |
|
543 |
"F : A co A' ==> A <= A'"; |
|
544 |
by (auto_tac (claset() addSDs [bspec], simpset())); |
|
545 |
qed "constrains_imp_subset"; |
|
546 |
||
547 |
(*The reasoning is by subsets since "co" refers to single actions |
|
548 |
only. So this rule isn't that useful.*) |
|
549 |
||
550 |
Goalw [constrains_def] |
|
551 |
"[| F : A co B; F : B co C |] ==> F : A co C"; |
|
552 |
by Auto_tac; |
|
12152
46f128d8133c
Renamed some bound variables due to changes in simplifier.
berghofe
parents:
11479
diff
changeset
|
553 |
by (dres_inst_tac [("x", "act")] bspec 1); |
11479 | 554 |
by (dres_inst_tac [("x", "Id")] bspec 2); |
555 |
by (auto_tac (claset() addDs [ActsD], |
|
556 |
simpset() addsimps [condition_def])); |
|
557 |
qed "constrains_trans"; |
|
558 |
||
559 |
Goalw [constrains_def] |
|
560 |
"[| F : A co (A' Un B); F : B co B' |] ==> F : A co (A' Un B')"; |
|
561 |
by Auto_tac; |
|
562 |
by (dres_inst_tac [("x", "Id")] bspec 1); |
|
12152
46f128d8133c
Renamed some bound variables due to changes in simplifier.
berghofe
parents:
11479
diff
changeset
|
563 |
by (dres_inst_tac [("x", "act")] bspec 2); |
11479 | 564 |
by (auto_tac (claset(), simpset() addsimps [condition_def])); |
565 |
qed "constrains_cancel"; |
|
566 |
||
567 |
(*** unless ***) |
|
568 |
||
569 |
Goalw [unless_def] "F : (A-B) co (A Un B) ==> F : A unless B"; |
|
570 |
by (assume_tac 1); |
|
571 |
qed "unlessI"; |
|
572 |
||
573 |
Goalw [unless_def] "F :A unless B ==> F : (A-B) co (A Un B)"; |
|
574 |
by (assume_tac 1); |
|
575 |
qed "unlessD"; |
|
576 |
||
577 |
Goalw [unless_def, constrains_def] |
|
578 |
"F: A unless B ==> F:program & A:condition & B:condition"; |
|
579 |
by Auto_tac; |
|
580 |
qed "unlessD2"; |
|
581 |
||
582 |
(*** initially ***) |
|
583 |
||
584 |
Goalw [initially_def] |
|
585 |
"[| Init(F)<=A; F:program; A:condition |] ==> F:initially(A)"; |
|
586 |
by (Blast_tac 1); |
|
587 |
qed "initiallyI"; |
|
588 |
||
589 |
Goalw [initially_def] |
|
590 |
"F:initially(A) ==> Init(F)<=A"; |
|
591 |
by (Blast_tac 1); |
|
592 |
qed "initiallyD"; |
|
593 |
||
594 |
Goalw [initially_def] |
|
595 |
"F:initially(A) ==> F:program & A:condition"; |
|
596 |
by (Blast_tac 1); |
|
597 |
qed "initiallyD2"; |
|
598 |
||
599 |
(*** stable ***) |
|
600 |
||
601 |
Goalw [stable_def] |
|
602 |
"F : A co A ==> F : stable(A)"; |
|
603 |
by (assume_tac 1); |
|
604 |
qed "stableI"; |
|
605 |
||
606 |
Goalw [stable_def] "F : stable(A) ==> F : A co A"; |
|
607 |
by (assume_tac 1); |
|
608 |
qed "stableD"; |
|
609 |
||
610 |
Goalw [stable_def, constrains_def] |
|
611 |
"F:stable(A)==> F:program & A:condition"; |
|
612 |
by (Blast_tac 1); |
|
613 |
qed "stableD2"; |
|
614 |
||
615 |
Goalw [stable_def, constrains_def] |
|
616 |
"stable(state) = program"; |
|
617 |
by (auto_tac (claset() addDs [ActsD], simpset())); |
|
618 |
qed "stable_state"; |
|
619 |
Addsimps [stable_state]; |
|
620 |
||
621 |
(** Union **) |
|
622 |
||
623 |
Goalw [stable_def] |
|
624 |
"[| F : stable(A); F : stable(A') |] ==> F : stable(A Un A')"; |
|
625 |
by (blast_tac (claset() addIs [constrains_Un]) 1); |
|
626 |
qed "stable_Un"; |
|
627 |
||
628 |
val [major, minor] = Goalw [stable_def] |
|
629 |
"[| (!!i. i:I ==> F : stable(A(i))); F:program |] ==> F:stable (UN i:I. A(i))"; |
|
630 |
by (cut_facts_tac [minor] 1); |
|
631 |
by (blast_tac (claset() addIs [constrains_UN, major]) 1); |
|
632 |
qed "stable_UN"; |
|
633 |
||
634 |
Goalw [stable_def] |
|
635 |
"[| F : stable(A); F : stable(A') |] ==> F : stable (A Int A')"; |
|
636 |
by (blast_tac (claset() addIs [constrains_Int]) 1); |
|
637 |
qed "stable_Int"; |
|
638 |
||
639 |
val [major, minor] = Goalw [stable_def] |
|
640 |
"[| (!!i. i:I ==> F : stable(A(i))); F:program |] \ |
|
641 |
\ ==> F : stable (INT i:I. A(i))"; |
|
642 |
by (cut_facts_tac [minor] 1); |
|
643 |
by (blast_tac (claset() addIs [constrains_INT, major]) 1); |
|
644 |
qed "stable_INT"; |
|
645 |
||
646 |
Goalw [stable_def] |
|
647 |
"[| ALL z. F: stable({s:state. P(s, z)}); F:program |] ==> \ |
|
648 |
\ F: stable({s:state. ALL z. P(s, z)})"; |
|
649 |
by (rtac constrains_All 1); |
|
650 |
by Auto_tac; |
|
651 |
bind_thm("stable_All", allI RS result()); |
|
652 |
||
653 |
||
654 |
Goalw [stable_def, constrains_def] |
|
655 |
"[| F : stable(C); F : A co (C Un A') |] ==> F : (C Un A) co (C Un A')"; |
|
656 |
by (Clarify_tac 1); |
|
657 |
by (Blast_tac 1); |
|
658 |
qed "stable_constrains_Un"; |
|
659 |
||
660 |
||
661 |
Goalw [stable_def, constrains_def] |
|
662 |
"[| F : stable(C); F : (C Int A) co A' |] ==> F : (C Int A) co (C Int A')"; |
|
663 |
by (Clarify_tac 1); |
|
664 |
by (Blast_tac 1); |
|
665 |
qed "stable_constrains_Int"; |
|
666 |
||
667 |
(*[| F : stable(C); F : (C Int A) co A |] ==> F : stable (C Int A) *) |
|
668 |
bind_thm ("stable_constrains_stable", stable_constrains_Int RS stableI); |
|
669 |
||
670 |
(** invariant **) |
|
671 |
||
672 |
Goalw [invariant_def, initially_def] |
|
673 |
"invariant(A) = initially(A) Int stable(A)"; |
|
674 |
by (blast_tac (claset() addDs [stableD2]) 1); |
|
675 |
qed "invariant_eq"; |
|
676 |
||
677 |
val invariant_def2 = invariant_eq RS eq_reflection; |
|
678 |
||
679 |
Goalw [invariant_def] |
|
680 |
"[| Init(F)<=A; F:stable(A) |] ==> F : invariant(A)"; |
|
681 |
by (blast_tac (claset() addDs [stableD2]) 1); |
|
682 |
qed "invariantI"; |
|
683 |
||
684 |
Goalw [invariant_def] |
|
685 |
"F:invariant(A) ==> Init(F)<=A & F:stable(A)"; |
|
686 |
by Auto_tac; |
|
687 |
qed "invariantD"; |
|
688 |
||
689 |
Goalw [invariant_def] |
|
690 |
"F:invariant(A) ==> F:program & A:condition"; |
|
691 |
by (blast_tac (claset() addDs [stableD2]) 1); |
|
692 |
qed "invariantD2"; |
|
693 |
||
694 |
(*Could also say "invariant A Int invariant B <= invariant (A Int B)"*) |
|
695 |
Goalw [invariant_def] |
|
696 |
"[| F : invariant(A); F : invariant(B) |] ==> F : invariant(A Int B)"; |
|
697 |
by (asm_full_simp_tac (simpset() addsimps [stable_Int]) 1); |
|
698 |
by (Blast_tac 1); |
|
699 |
qed "invariant_Int"; |
|
700 |
||
701 |
(** The Elimination Theorem. The "free" m has become universally quantified! |
|
702 |
Should the premise be !!m instead of ALL m ? Would make it harder to use |
|
703 |
in forward proof. **) |
|
704 |
||
705 |
Goalw [constrains_def] |
|
706 |
"[| ALL m:M. F : {s:S. x(s) = m} co B(m); F:program |] \ |
|
707 |
\ ==> F:{s:S. x(s):M} co (UN m:M. B(m))"; |
|
708 |
by Safe_tac; |
|
709 |
by (Blast_tac 1); |
|
710 |
by (auto_tac (claset(), simpset() addsimps [condition_def])); |
|
711 |
qed "elimination"; |
|
712 |
||
713 |
(* As above, but for the special case of S=state *) |
|
714 |
Goal "[| ALL m:M. F : {s:state. x(s) = m} co B(m); F:program |] \ |
|
715 |
\ ==> F:{s:state. x(s):M} co (UN m:M. B(m))"; |
|
716 |
by (rtac elimination 1); |
|
717 |
by (ALLGOALS(Clarify_tac)); |
|
718 |
qed "eliminiation2"; |
|
719 |
||
720 |
||
721 |
Goalw [constrains_def, strongest_rhs_def] |
|
722 |
"[| F:program; A:condition |] ==>F : A co (strongest_rhs(F,A))"; |
|
723 |
by (auto_tac (claset() addDs [ActsD], simpset())); |
|
724 |
qed "constrains_strongest_rhs"; |
|
725 |
||
726 |
Goalw [constrains_def, strongest_rhs_def] |
|
727 |
"F : A co B ==> strongest_rhs(F,A) <=B"; |
|
728 |
by Safe_tac; |
|
729 |
by (dtac InterD 1); |
|
730 |
by (auto_tac (claset(), |
|
731 |
simpset() addsimps [condition_def])); |
|
732 |
qed "strongest_rhs_is_strongest"; |
|
733 |
||
734 |
(*** increasing ***) |
|
735 |
Goalw [increasing_on_def] |
|
736 |
"[| F:increasing[A](f, r); z:A |] ==> F:stable({s:state. <z, f`s>:r})"; |
|
737 |
by (Blast_tac 1); |
|
738 |
qed "increasing_onD"; |
|
739 |
||
740 |
Goalw [increasing_on_def] |
|
741 |
"F:increasing[A](f, r) ==> F:program & f:state->A & part_order(A,r)"; |
|
742 |
by (auto_tac (claset(), simpset() addsimps [INT_iff])); |
|
743 |
qed "increasing_onD2"; |
|
744 |
||
745 |
Goalw [increasing_on_def, stable_def] |
|
746 |
"[| part_order(A,r); c:A; F:program |] ==> F : increasing[A](lam s:state. c, r)"; |
|
747 |
by (auto_tac (claset(), simpset() addsimps [INT_iff])); |
|
748 |
by (force_tac (claset() addSDs [bspec, ActsD], |
|
749 |
simpset() addsimps [constrains_def, condition_def]) 1); |
|
750 |
qed "increasing_on_constant"; |
|
751 |
Addsimps [increasing_on_constant]; |
|
752 |
||
753 |
Goalw [increasing_on_def, stable_def, constrains_def, part_order_def] |
|
754 |
"!!f. g:mono_map(A,r,A,r) \ |
|
755 |
\ ==> increasing[A](f, r) <= increasing[A](g O f, r)"; |
|
756 |
by (asm_full_simp_tac (simpset() addsimps [INT_iff,condition_def, mono_map_def]) 1); |
|
757 |
by (auto_tac (claset() addIs [comp_fun], simpset() addsimps [mono_map_def])); |
|
758 |
by (force_tac (claset() addSDs [bspec, ActsD], simpset()) 1); |
|
12152
46f128d8133c
Renamed some bound variables due to changes in simplifier.
berghofe
parents:
11479
diff
changeset
|
759 |
by (subgoal_tac "xc:state" 1); |
11479 | 760 |
by (force_tac (claset() addSDs [ActsD], simpset()) 2); |
12152
46f128d8133c
Renamed some bound variables due to changes in simplifier.
berghofe
parents:
11479
diff
changeset
|
761 |
by (subgoal_tac "f`xd:A & f`xc:A" 1); |
11479 | 762 |
by (blast_tac (claset() addDs [apply_type]) 2); |
763 |
by (rotate_tac 3 1); |
|
12152
46f128d8133c
Renamed some bound variables due to changes in simplifier.
berghofe
parents:
11479
diff
changeset
|
764 |
by (dres_inst_tac [("x", "f`xd")] bspec 1); |
11479 | 765 |
by (Asm_simp_tac 1); |
766 |
by (REPEAT(etac conjE 1)); |
|
767 |
by (rotate_tac ~2 1); |
|
12152
46f128d8133c
Renamed some bound variables due to changes in simplifier.
berghofe
parents:
11479
diff
changeset
|
768 |
by (dres_inst_tac [("x", "act")] bspec 1); |
11479 | 769 |
by (Asm_simp_tac 1); |
12152
46f128d8133c
Renamed some bound variables due to changes in simplifier.
berghofe
parents:
11479
diff
changeset
|
770 |
by (dres_inst_tac [("c", "xc")] subsetD 1); |
11479 | 771 |
by (rtac imageI 1); |
772 |
by Auto_tac; |
|
773 |
by (asm_full_simp_tac (simpset() addsimps [refl_def]) 1); |
|
12152
46f128d8133c
Renamed some bound variables due to changes in simplifier.
berghofe
parents:
11479
diff
changeset
|
774 |
by (dres_inst_tac [("x", "f`xd")] bspec 1); |
46f128d8133c
Renamed some bound variables due to changes in simplifier.
berghofe
parents:
11479
diff
changeset
|
775 |
by (dres_inst_tac [("x", "f`xc")] bspec 2); |
11479 | 776 |
by (ALLGOALS(Asm_simp_tac)); |
12152
46f128d8133c
Renamed some bound variables due to changes in simplifier.
berghofe
parents:
11479
diff
changeset
|
777 |
by (dres_inst_tac [("b", "g`(f`xd)")] trans_onD 1); |
11479 | 778 |
by Auto_tac; |
779 |
qed "mono_increasing_on_comp"; |
|
780 |
||
781 |
(*Holds by the theorem (succ(m) le n) = (m < n) *) |
|
782 |
Goalw [increasing_on_def, nat_order_def] |
|
783 |
"[| F:increasing[nat](f, nat_order); z:nat |] \ |
|
784 |
\ ==> F: stable({s:state. z < f`s})"; |
|
785 |
by (Clarify_tac 1); |
|
786 |
by (asm_full_simp_tac (simpset() addsimps [INT_iff]) 1); |
|
787 |
by Safe_tac; |
|
788 |
by (dres_inst_tac [("x", "succ(z)")] bspec 1); |
|
789 |
by (auto_tac (claset(), simpset() addsimps [apply_type, Collect_conj_eq])); |
|
790 |
by (subgoal_tac "{x: state . f ` x : nat} = state" 1); |
|
791 |
by Auto_tac; |
|
792 |
qed "strict_increasing_onD"; |