11479
|
1 |
(* Title: ZF/UNITY/Constrains.ML
|
|
2 |
ID: $Id$
|
|
3 |
Author: Sidi O Ehmety, Computer Laboratory
|
|
4 |
Copyright 2001 University of Cambridge
|
|
5 |
|
|
6 |
Safety relations: restricted to the set of reachable states.
|
|
7 |
|
|
8 |
Proofs ported from HOL.
|
|
9 |
*)
|
|
10 |
|
|
11 |
(*** traces and reachable ***)
|
|
12 |
|
|
13 |
Goalw [condition_def]
|
|
14 |
"reachable(F):condition";
|
|
15 |
by (auto_tac (claset() addSDs [reachable.dom_subset RS subsetD]
|
|
16 |
addDs [InitD, ActsD], simpset()));
|
|
17 |
qed "reachable_type";
|
|
18 |
Addsimps [reachable_type];
|
|
19 |
AddIs [reachable_type];
|
|
20 |
|
|
21 |
Goal "x:reachable(F) ==> x:state";
|
|
22 |
by (cut_inst_tac [("F", "F")] reachable_type 1);
|
|
23 |
by (auto_tac (claset(), simpset() addsimps [condition_def]));
|
|
24 |
qed "reachableD";
|
|
25 |
|
|
26 |
Goal "F:program ==> \
|
|
27 |
\ reachable(F) = {s:state. EX evs. <s,evs>: traces(Init(F), Acts(F))}";
|
|
28 |
by (rtac equalityI 1);
|
|
29 |
by Safe_tac;
|
|
30 |
by (blast_tac (claset() addDs [reachableD]) 1);
|
|
31 |
by (etac traces.induct 2);
|
|
32 |
by (etac reachable.induct 1);
|
|
33 |
by (ALLGOALS (blast_tac (claset() addIs reachable.intrs @ traces.intrs)));
|
|
34 |
qed "reachable_equiv_traces";
|
|
35 |
|
|
36 |
Goal "Init(F) <= reachable(F)";
|
|
37 |
by (blast_tac (claset() addIs reachable.intrs) 1);
|
|
38 |
qed "Init_into_reachable";
|
|
39 |
|
|
40 |
Goal "[| F:program; G:program; \
|
|
41 |
\ Acts(G) <= Acts(F) |] ==> G:stable(reachable(F))";
|
|
42 |
by (blast_tac (claset()
|
|
43 |
addIs [stableI, constrainsI, reachable_type] @ reachable.intrs) 1);
|
|
44 |
qed "stable_reachable";
|
|
45 |
|
|
46 |
AddSIs [stable_reachable];
|
|
47 |
Addsimps [stable_reachable];
|
|
48 |
|
|
49 |
(*The set of all reachable states is an invariant...*)
|
|
50 |
Goalw [invariant_def, initially_def]
|
|
51 |
"F:program ==> F:invariant(reachable(F))";
|
|
52 |
by (blast_tac (claset() addIs [reachable_type]@reachable.intrs) 1);
|
|
53 |
qed "invariant_reachable";
|
|
54 |
|
|
55 |
(*...in fact the strongest invariant!*)
|
|
56 |
Goal "F : invariant(A) ==> reachable(F) <= A";
|
|
57 |
by (full_simp_tac
|
|
58 |
(simpset() addsimps [stable_def, constrains_def, invariant_def]) 1);
|
|
59 |
by (rtac subsetI 1);
|
|
60 |
by (etac reachable.induct 1);
|
|
61 |
by (REPEAT (blast_tac (claset() addIs reachable.intrs) 1));
|
|
62 |
qed "invariant_includes_reachable";
|
|
63 |
|
|
64 |
(*** Co ***)
|
|
65 |
|
|
66 |
(*F : B co B' ==> F : (reachable F Int B) co (reachable F Int B')*)
|
|
67 |
val lemma = subset_refl RSN (3, rewrite_rule
|
|
68 |
[stable_def] stable_reachable RS constrains_Int);
|
|
69 |
Goal "F:B co B' ==> F: (reachable(F) Int B) co (reachable(F) Int B')";
|
|
70 |
by (blast_tac (claset() addSIs [lemma]
|
|
71 |
addDs [constrainsD2]) 1);
|
|
72 |
qed "constrains_reachable_Int";
|
|
73 |
|
|
74 |
(*Resembles the previous definition of Constrains*)
|
|
75 |
Goalw [Constrains_def]
|
|
76 |
"A Co B = \
|
|
77 |
\ {F:program. F : (reachable(F) Int A) co (reachable(F) Int B) & \
|
|
78 |
\ A:condition & B:condition}";
|
|
79 |
by (rtac equalityI 1);
|
|
80 |
by (ALLGOALS(Clarify_tac));
|
|
81 |
by (subgoal_tac "reachable(x) Int B:condition" 2);
|
|
82 |
by (blast_tac (claset() addDs [constrains_reachable_Int]
|
|
83 |
addIs [constrains_weaken]) 2);
|
|
84 |
by (subgoal_tac "reachable(x) Int B:condition" 1);
|
|
85 |
by (blast_tac (claset() addDs [constrains_reachable_Int]
|
|
86 |
addIs [constrains_weaken]) 1);
|
|
87 |
by (REPEAT(blast_tac (claset() addIs [reachable_type]) 1));
|
|
88 |
qed "Constrains_eq_constrains";
|
|
89 |
|
|
90 |
Goalw [Constrains_def]
|
|
91 |
"F : A co A' ==> F : A Co A'";
|
|
92 |
by (blast_tac (claset() addIs [constrains_weaken_L]
|
|
93 |
addDs [constrainsD2]) 1);
|
|
94 |
qed "constrains_imp_Constrains";
|
|
95 |
|
|
96 |
Goalw [stable_def, Stable_def]
|
|
97 |
"F : stable(A) ==> F : Stable(A)";
|
|
98 |
by (etac constrains_imp_Constrains 1);
|
|
99 |
qed "stable_imp_Stable";
|
|
100 |
|
|
101 |
|
|
102 |
val prems = Goal
|
|
103 |
"[|(!!act s s'. [| act: Acts(F); <s,s'>:act; s:A |] \
|
|
104 |
\ ==> s':A'); F:program; A:condition; A':condition |] ==> F:A Co A'";
|
|
105 |
by (rtac constrains_imp_Constrains 1);
|
|
106 |
by (blast_tac (claset() addIs (constrainsI::prems)) 1);
|
|
107 |
qed "ConstrainsI";
|
|
108 |
|
|
109 |
Goalw [Constrains_def]
|
|
110 |
"F:A Co B ==> F:program & A:condition & B:condition";
|
|
111 |
by (Blast_tac 1);
|
|
112 |
qed "ConstrainsD";
|
|
113 |
|
|
114 |
Goal "[| F:program; B:condition |] ==> F : 0 Co B";
|
|
115 |
by (blast_tac (claset() addIs
|
|
116 |
[constrains_imp_Constrains, constrains_empty]) 1);
|
|
117 |
qed "Constrains_empty";
|
|
118 |
|
|
119 |
Goal "[| F:program; A:condition |] ==> F : A Co state";
|
|
120 |
by (blast_tac (claset() addIs
|
|
121 |
[constrains_imp_Constrains, constrains_state2]) 1);
|
|
122 |
qed "Constrains_state";
|
|
123 |
Addsimps [Constrains_empty, Constrains_state];
|
|
124 |
|
|
125 |
val Constrains_def2 = Constrains_eq_constrains RS eq_reflection;
|
|
126 |
|
|
127 |
Goalw [Constrains_def2]
|
|
128 |
"[| F : A Co A'; A'<=B'; B':condition |] ==> F : A Co B'";
|
|
129 |
by (Clarify_tac 1);
|
|
130 |
by (blast_tac (claset()
|
|
131 |
addIs [reachable_type, constrains_weaken_R]) 1);
|
|
132 |
qed "Constrains_weaken_R";
|
|
133 |
|
|
134 |
|
|
135 |
Goalw [condition_def]
|
|
136 |
"[| A<=B; B:condition |] ==>A:condition";
|
|
137 |
by (Blast_tac 1);
|
|
138 |
qed "condition_subset_mono";
|
|
139 |
|
|
140 |
|
|
141 |
Goalw [Constrains_def2]
|
|
142 |
"[| F : A Co A'; B<=A |] ==> F : B Co A'";
|
|
143 |
by (Clarify_tac 1);
|
|
144 |
by (forward_tac [condition_subset_mono] 1);
|
|
145 |
by (assume_tac 1);
|
|
146 |
by (blast_tac (claset()
|
|
147 |
addIs [reachable_type, constrains_weaken_L]) 1);
|
|
148 |
qed "Constrains_weaken_L";
|
|
149 |
|
|
150 |
Goalw [Constrains_def]
|
|
151 |
"[| F : A Co A'; B<=A; A'<=B'; B':condition |] ==> F : B Co B'";
|
|
152 |
by (Clarify_tac 1);
|
|
153 |
by (forward_tac [condition_subset_mono] 1);
|
|
154 |
by (assume_tac 1);
|
|
155 |
by (blast_tac (claset() addIs [reachable_type, constrains_weaken]) 1);
|
|
156 |
qed "Constrains_weaken";
|
|
157 |
|
|
158 |
(** Union **)
|
|
159 |
|
|
160 |
Goalw [Constrains_def2]
|
|
161 |
"[| F : A Co A'; F : B Co B' |] \
|
|
162 |
\ ==> F : (A Un B) Co (A' Un B')";
|
|
163 |
by Safe_tac;
|
|
164 |
by (asm_full_simp_tac (simpset() addsimps [Int_Un_distrib2 RS sym]) 1);
|
|
165 |
by (blast_tac (claset() addIs [constrains_Un]) 1);
|
|
166 |
qed "Constrains_Un";
|
|
167 |
|
|
168 |
Goalw [Constrains_def2]
|
|
169 |
"[| F:program; \
|
|
170 |
\ ALL i:I. F : A(i) Co A'(i) |] \
|
|
171 |
\ ==> F : (UN i:I. A(i)) Co (UN i:I. A'(i))";
|
|
172 |
by (rtac CollectI 1);
|
|
173 |
by Safe_tac;
|
|
174 |
by (simp_tac (simpset() addsimps [Int_UN_distrib]) 1);
|
|
175 |
by (blast_tac (claset() addIs [constrains_UN, CollectD2 RS conjunct1]) 1);
|
|
176 |
by (rewrite_goals_tac [condition_def]);
|
|
177 |
by (ALLGOALS(Blast_tac));
|
|
178 |
qed "Constrains_UN";
|
|
179 |
|
|
180 |
(** Intersection **)
|
|
181 |
|
|
182 |
Goal "A Int (B Int C) = (A Int B) Int (A Int C)";
|
|
183 |
by (Blast_tac 1);
|
|
184 |
qed "Int_duplicate";
|
|
185 |
|
|
186 |
Goalw [Constrains_def]
|
|
187 |
"[| F : A Co A'; F : B Co B' |] \
|
|
188 |
\ ==> F : (A Int B) Co (A' Int B')";
|
|
189 |
by (Step_tac 1);
|
|
190 |
by (subgoal_tac "reachable(F) Int (A Int B) = \
|
|
191 |
\ (reachable(F) Int A) Int (reachable(F) Int B)" 1);
|
|
192 |
by (Blast_tac 2);
|
|
193 |
by (Asm_simp_tac 1);
|
|
194 |
by (rtac constrains_Int 1);
|
|
195 |
by (ALLGOALS(Asm_simp_tac));
|
|
196 |
qed "Constrains_Int";
|
|
197 |
|
|
198 |
Goal
|
|
199 |
"[| F:program; \
|
|
200 |
\ ALL i:I. F: A(i) Co A'(i) |] \
|
|
201 |
\ ==> F : (INT i:I. A(i)) Co (INT i:I. A'(i))";
|
|
202 |
by (case_tac "I=0" 1);
|
|
203 |
by (asm_full_simp_tac (simpset() addsimps [Inter_def]) 1);
|
|
204 |
by (subgoal_tac "reachable(F) Int Inter(RepFun(I, A)) = (INT i:I. reachable(F) Int A(i))" 1);
|
|
205 |
by (asm_full_simp_tac (simpset() addsimps [Inter_def]) 2);
|
|
206 |
by (Blast_tac 2);
|
|
207 |
by (asm_full_simp_tac (simpset() addsimps [Constrains_def]) 1);
|
|
208 |
by (Step_tac 1);
|
|
209 |
by (rtac constrains_INT 1);
|
|
210 |
by (ALLGOALS(Asm_full_simp_tac));
|
|
211 |
by (ALLGOALS(Blast_tac));
|
|
212 |
qed "Constrains_INT";
|
|
213 |
|
|
214 |
Goal "F : A Co A' ==> reachable(F) Int A <= A'";
|
|
215 |
by (asm_full_simp_tac (simpset() addsimps
|
|
216 |
[Constrains_def, reachable_type]) 1);
|
|
217 |
by (blast_tac (claset() addDs [constrains_imp_subset]) 1);
|
|
218 |
qed "Constrains_imp_subset";
|
|
219 |
|
|
220 |
Goal "[| F : A Co B; F : B Co C |] ==> F : A Co C";
|
|
221 |
by (full_simp_tac (simpset() addsimps [Constrains_eq_constrains]) 1);
|
|
222 |
by (blast_tac (claset() addIs [constrains_trans, constrains_weaken]) 1);
|
|
223 |
qed "Constrains_trans";
|
|
224 |
|
|
225 |
Goal "[| F : A Co (A' Un B); F : B Co B' |] ==> F : A Co (A' Un B')";
|
|
226 |
by (full_simp_tac (simpset()
|
|
227 |
addsimps [Constrains_eq_constrains, Int_Un_distrib2 RS sym]) 1);
|
|
228 |
by (Step_tac 1);
|
|
229 |
by (blast_tac (claset() addIs [constrains_cancel]) 1);
|
|
230 |
qed "Constrains_cancel";
|
|
231 |
|
|
232 |
(*** Stable ***)
|
|
233 |
|
|
234 |
(*Useful because there's no Stable_weaken. [Tanja Vos]*)
|
|
235 |
Goal "[| F: Stable(A); A = B |] ==> F : Stable(B)";
|
|
236 |
by (Blast_tac 1);
|
|
237 |
qed "Stable_eq";
|
|
238 |
|
|
239 |
Goal "A:condition ==> F : Stable(A) <-> (F : stable(reachable(F) Int A))";
|
|
240 |
by (simp_tac (simpset() addsimps [Stable_def, Constrains_eq_constrains,
|
|
241 |
stable_def]) 1);
|
|
242 |
by (blast_tac (claset() addDs [constrainsD2]) 1);
|
|
243 |
qed "Stable_eq_stable";
|
|
244 |
|
|
245 |
Goalw [Stable_def] "F : A Co A ==> F : Stable(A)";
|
|
246 |
by (assume_tac 1);
|
|
247 |
qed "StableI";
|
|
248 |
|
|
249 |
Goalw [Stable_def] "F : Stable(A) ==> F : A Co A";
|
|
250 |
by (assume_tac 1);
|
|
251 |
qed "StableD";
|
|
252 |
|
|
253 |
Goalw [Stable_def]
|
|
254 |
"[| F : Stable(A); F : Stable(A') |] ==> F : Stable(A Un A')";
|
|
255 |
by (blast_tac (claset() addIs [Constrains_Un]) 1);
|
|
256 |
qed "Stable_Un";
|
|
257 |
|
|
258 |
Goalw [Stable_def]
|
|
259 |
"[| F : Stable(A); F : Stable(A') |] ==> F : Stable (A Int A')";
|
|
260 |
by (blast_tac (claset() addIs [Constrains_Int]) 1);
|
|
261 |
qed "Stable_Int";
|
|
262 |
|
|
263 |
Goalw [Stable_def]
|
|
264 |
"[| F : Stable(C); F : A Co (C Un A') |] \
|
|
265 |
\ ==> F : (C Un A) Co (C Un A')";
|
|
266 |
by (subgoal_tac "C Un A' :condition & C Un A:condition" 1);
|
|
267 |
by (blast_tac (claset() addIs [Constrains_Un RS Constrains_weaken_R]) 1);
|
|
268 |
by (blast_tac (claset() addDs [ConstrainsD]) 1);
|
|
269 |
qed "Stable_Constrains_Un";
|
|
270 |
|
|
271 |
|
|
272 |
Goalw [Stable_def]
|
|
273 |
"[| F : Stable(C); F : (C Int A) Co A' |] \
|
|
274 |
\ ==> F : (C Int A) Co (C Int A')";
|
|
275 |
by (blast_tac (claset() addDs [ConstrainsD]
|
|
276 |
addIs [Constrains_Int RS Constrains_weaken]) 1);
|
|
277 |
qed "Stable_Constrains_Int";
|
|
278 |
|
|
279 |
val [major, prem] = Goalw [Stable_def]
|
|
280 |
"[| F:program; \
|
|
281 |
\ (!!i. i:I ==> F : Stable(A(i))) |]==> F : Stable (UN i:I. A(i))";
|
|
282 |
by (cut_facts_tac [major] 1);
|
|
283 |
by (blast_tac (claset() addIs [major, Constrains_UN, prem]) 1);
|
|
284 |
qed "Stable_UN";
|
|
285 |
|
|
286 |
val [major, prem] = Goalw [Stable_def]
|
|
287 |
"[| F:program; \
|
|
288 |
\ (!!i. i:I ==> F:Stable(A(i))) |]==> F : Stable (INT i:I. A(i))";
|
|
289 |
by (cut_facts_tac [major] 1);
|
|
290 |
by (blast_tac (claset() addIs [major, Constrains_INT, prem]) 1);
|
|
291 |
qed "Stable_INT";
|
|
292 |
|
|
293 |
Goal "F:program ==>F : Stable (reachable(F))";
|
|
294 |
by (asm_simp_tac (simpset()
|
|
295 |
addsimps [Stable_eq_stable, Int_absorb, subset_refl]) 1);
|
|
296 |
qed "Stable_reachable";
|
|
297 |
|
|
298 |
Goalw [Stable_def]
|
|
299 |
"F:Stable(A) ==> F:program & A:condition";
|
|
300 |
by (blast_tac (claset() addDs [ConstrainsD]) 1);
|
|
301 |
qed "StableD2";
|
|
302 |
|
|
303 |
(*** The Elimination Theorem. The "free" m has become universally quantified!
|
|
304 |
Should the premise be !!m instead of ALL m ? Would make it harder to use
|
|
305 |
in forward proof. ***)
|
|
306 |
|
|
307 |
Goalw [condition_def]
|
|
308 |
"Collect(state,P):condition";
|
|
309 |
by Auto_tac;
|
|
310 |
qed "Collect_in_condition";
|
|
311 |
AddIffs [Collect_in_condition];
|
|
312 |
|
|
313 |
Goalw [Constrains_def]
|
|
314 |
"[| ALL m:M. F : {s:S. x(s) = m} Co B(m); F:program |] \
|
|
315 |
\ ==> F : {s:S. x(s):M} Co (UN m:M. B(m))";
|
|
316 |
by Safe_tac;
|
|
317 |
by (res_inst_tac [("S1", "reachable(F) Int S")]
|
|
318 |
(elimination RS constrains_weaken_L) 1);
|
|
319 |
by Auto_tac;
|
|
320 |
by (rtac constrains_weaken_L 1);
|
|
321 |
by (auto_tac (claset(), simpset() addsimps [condition_def]));
|
|
322 |
qed "Elimination";
|
|
323 |
|
|
324 |
(* As above, but for the special case of S=state *)
|
|
325 |
|
|
326 |
Goal
|
|
327 |
"[| ALL m:M. F : {s:state. x(s) = m} Co B(m); F:program |] \
|
|
328 |
\ ==> F : {s:state. x(s):M} Co (UN m:M. B(m))";
|
|
329 |
by (blast_tac (claset() addIs [Elimination]) 1);
|
|
330 |
qed "Elimination2";
|
|
331 |
|
|
332 |
(** Unless **)
|
|
333 |
|
|
334 |
Goalw [Unless_def]
|
|
335 |
"F:A Unless B ==> F:program & A:condition & B:condition";
|
|
336 |
by (blast_tac (claset() addDs [ConstrainsD]) 1);
|
|
337 |
qed "UnlessD";
|
|
338 |
|
|
339 |
(*** Specialized laws for handling Always ***)
|
|
340 |
|
|
341 |
(** Natural deduction rules for "Always A" **)
|
|
342 |
Goalw [Always_def, initially_def]
|
|
343 |
"Always(A) = initially(A) Int Stable(A)";
|
|
344 |
by (blast_tac (claset() addDs [StableD2]) 1);
|
|
345 |
qed "Always_eq";
|
|
346 |
|
|
347 |
val Always_def2 = Always_eq RS eq_reflection;
|
|
348 |
|
|
349 |
Goalw [Always_def]
|
|
350 |
"[| Init(F)<=A; F : Stable(A) |] ==> F : Always(A)";
|
|
351 |
by (asm_simp_tac (simpset() addsimps [StableD2]) 1);
|
|
352 |
qed "AlwaysI";
|
|
353 |
|
|
354 |
Goal "F : Always(A) ==> Init(F)<=A & F : Stable(A)";
|
|
355 |
by (asm_full_simp_tac (simpset() addsimps [Always_def]) 1);
|
|
356 |
qed "AlwaysD";
|
|
357 |
|
|
358 |
bind_thm ("AlwaysE", AlwaysD RS conjE);
|
|
359 |
bind_thm ("Always_imp_Stable", AlwaysD RS conjunct2);
|
|
360 |
|
|
361 |
|
|
362 |
(*The set of all reachable states is Always*)
|
|
363 |
Goal "F : Always(A) ==> reachable(F) <= A";
|
|
364 |
by (full_simp_tac
|
|
365 |
(simpset() addsimps [Stable_def, Constrains_def, constrains_def,
|
|
366 |
Always_def]) 1);
|
|
367 |
by (rtac subsetI 1);
|
|
368 |
by (etac reachable.induct 1);
|
|
369 |
by (REPEAT (blast_tac (claset() addIs reachable.intrs) 1));
|
|
370 |
qed "Always_includes_reachable";
|
|
371 |
|
|
372 |
Goalw [Always_def2, invariant_def2, Stable_def, stable_def]
|
|
373 |
"F : invariant(A) ==> F : Always(A)";
|
|
374 |
by (blast_tac (claset() addIs [constrains_imp_Constrains]) 1);
|
|
375 |
qed "invariant_imp_Always";
|
|
376 |
|
|
377 |
bind_thm ("Always_reachable", invariant_reachable RS invariant_imp_Always);
|
|
378 |
|
|
379 |
Goal "Always(A) = {F:program. F : invariant(reachable(F) Int A) & A:condition}";
|
|
380 |
by (simp_tac (simpset() addsimps [Always_def, invariant_def, Stable_def,
|
|
381 |
Constrains_eq_constrains, stable_def]) 1);
|
|
382 |
by (rtac equalityI 1);
|
|
383 |
by (ALLGOALS(Clarify_tac));
|
|
384 |
by (REPEAT(blast_tac (claset() addDs [constrainsD]
|
|
385 |
addIs reachable.intrs@[reachable_type]) 1));
|
|
386 |
qed "Always_eq_invariant_reachable";
|
|
387 |
|
|
388 |
(*the RHS is the traditional definition of the "always" operator*)
|
|
389 |
Goal "Always(A) = {F:program. reachable(F) <= A & A:condition}";
|
|
390 |
br equalityI 1;
|
|
391 |
by (ALLGOALS(Clarify_tac));
|
|
392 |
by (auto_tac (claset() addDs [invariant_includes_reachable],
|
|
393 |
simpset() addsimps [subset_Int_iff, invariant_reachable,
|
|
394 |
Always_eq_invariant_reachable]));
|
|
395 |
qed "Always_eq_includes_reachable";
|
|
396 |
|
|
397 |
Goalw [Always_def]
|
|
398 |
"F:Always(A)==> F:program & A:condition";
|
|
399 |
by (blast_tac (claset() addDs [StableD2]) 1);
|
|
400 |
qed "AlwaysD2";
|
|
401 |
|
|
402 |
Goal "Always(state) = program";
|
|
403 |
br equalityI 1;
|
|
404 |
by (ALLGOALS(Clarify_tac));
|
|
405 |
by (blast_tac (claset() addDs [AlwaysD2]) 1);
|
|
406 |
by (auto_tac (claset() addDs [reachableD],
|
|
407 |
simpset() addsimps [Always_eq_includes_reachable]));
|
|
408 |
qed "Always_state_eq";
|
|
409 |
Addsimps [Always_state_eq];
|
|
410 |
|
|
411 |
Goal "[| state <= A; F:program; A:condition |] ==> F : Always(A)";
|
|
412 |
by (auto_tac (claset(), simpset()
|
|
413 |
addsimps [Always_eq_includes_reachable]));
|
|
414 |
by (auto_tac (claset() addSDs [reachableD],
|
|
415 |
simpset() addsimps [condition_def]));
|
|
416 |
qed "state_AlwaysI";
|
|
417 |
|
|
418 |
Goal "A:condition ==> Always(A) = (UN I: Pow(A). invariant(I))";
|
|
419 |
by (simp_tac (simpset() addsimps [Always_eq_includes_reachable]) 1);
|
|
420 |
by (rtac equalityI 1);
|
|
421 |
by (ALLGOALS(Clarify_tac));
|
|
422 |
by (REPEAT(blast_tac (claset()
|
|
423 |
addIs [invariantI, impOfSubs Init_into_reachable,
|
|
424 |
impOfSubs invariant_includes_reachable]
|
|
425 |
addDs [invariantD2]) 1));
|
|
426 |
qed "Always_eq_UN_invariant";
|
|
427 |
|
|
428 |
Goal "[| F : Always(A); A <= B; B:condition |] ==> F : Always(B)";
|
|
429 |
by (auto_tac (claset(), simpset() addsimps [Always_eq_includes_reachable]));
|
|
430 |
qed "Always_weaken";
|
|
431 |
|
|
432 |
|
|
433 |
(*** "Co" rules involving Always ***)
|
|
434 |
val Int_absorb2 = rewrite_rule [iff_def] subset_Int_iff RS conjunct1 RS mp;
|
|
435 |
|
|
436 |
Goal "[| F:Always(INV); A:condition |] \
|
|
437 |
\ ==> (F:(INV Int A) Co A') <-> (F : A Co A')";
|
|
438 |
by (asm_simp_tac
|
|
439 |
(simpset() addsimps [Always_includes_reachable RS Int_absorb2,
|
|
440 |
Constrains_def, Int_assoc RS sym]) 1);
|
|
441 |
by (blast_tac (claset() addDs [AlwaysD2]) 1);
|
|
442 |
qed "Always_Constrains_pre";
|
|
443 |
|
|
444 |
Goal "[| F : Always(INV); A':condition |] \
|
|
445 |
\ ==> (F : A Co (INV Int A')) <->(F : A Co A')";
|
|
446 |
by (asm_simp_tac
|
|
447 |
(simpset() addsimps [Always_includes_reachable RS Int_absorb2,
|
|
448 |
Constrains_eq_constrains, Int_assoc RS sym]) 1);
|
|
449 |
by (blast_tac (claset() addDs [AlwaysD2]) 1);
|
|
450 |
qed "Always_Constrains_post";
|
|
451 |
|
|
452 |
(* [| F : Always INV; F : (INV Int A) Co A' |] ==> F : A Co A' *)
|
|
453 |
bind_thm ("Always_ConstrainsI", Always_Constrains_pre RS iffD1);
|
|
454 |
|
|
455 |
(* [| F : Always INV; F : A Co A' |] ==> F : A Co (INV Int A') *)
|
|
456 |
bind_thm ("Always_ConstrainsD", Always_Constrains_post RS iffD2);
|
|
457 |
|
|
458 |
(*The analogous proof of Always_LeadsTo_weaken doesn't terminate*)
|
|
459 |
Goal "[| F : Always(C); F : A Co A'; \
|
|
460 |
\ C Int B <= A; C Int A' <= B'; B:condition; B':condition |] \
|
|
461 |
\ ==> F : B Co B'";
|
|
462 |
by (rtac Always_ConstrainsI 1);
|
|
463 |
by (assume_tac 1);
|
|
464 |
by (assume_tac 1);
|
|
465 |
by (dtac Always_ConstrainsD 1);
|
|
466 |
by (assume_tac 2);
|
|
467 |
by (blast_tac (claset() addDs [ConstrainsD]) 1);
|
|
468 |
by (blast_tac (claset() addIs [Constrains_weaken]) 1);
|
|
469 |
qed "Always_Constrains_weaken";
|
|
470 |
|
|
471 |
|
|
472 |
(** Conjoining Always properties **)
|
|
473 |
|
|
474 |
Goal "[| A:condition; B:condition |] ==> \
|
|
475 |
\ Always(A Int B) = Always(A) Int Always(B)";
|
|
476 |
by (auto_tac (claset(), simpset() addsimps [Always_eq_includes_reachable]));
|
|
477 |
qed "Always_Int_distrib";
|
|
478 |
|
|
479 |
(* the premise i:I is need since INT is formally not defined for I=0 *)
|
|
480 |
Goal "[| i:I; ALL i:I. A(i):condition |] \
|
|
481 |
\ ==>Always(INT i:I. A(i)) = (INT i:I. Always(A(i)))";
|
|
482 |
by (rtac equalityI 1);
|
|
483 |
by (auto_tac (claset(), simpset() addsimps [Always_eq_includes_reachable]));
|
|
484 |
qed "Always_INT_distrib";
|
|
485 |
|
|
486 |
|
|
487 |
Goal "[| F : Always(A); F : Always(B) |] ==> F : Always(A Int B)";
|
|
488 |
by (asm_simp_tac (simpset() addsimps
|
|
489 |
[Always_Int_distrib,AlwaysD2]) 1);
|
|
490 |
qed "Always_Int_I";
|
|
491 |
|
|
492 |
(*Allows a kind of "implication introduction"*)
|
|
493 |
Goal "F : Always(A) ==> (F : Always (state-A Un B)) <-> (F : Always(B))";
|
|
494 |
by (auto_tac (claset(), simpset() addsimps [Always_eq_includes_reachable]));
|
|
495 |
qed "Always_Compl_Un_eq";
|
|
496 |
|
|
497 |
(*Delete the nearest invariance assumption (which will be the second one
|
|
498 |
used by Always_Int_I) *)
|
|
499 |
val Always_thin =
|
|
500 |
read_instantiate_sg (sign_of thy)
|
|
501 |
[("V", "?F : Always(?A)")] thin_rl;
|
|
502 |
|
|
503 |
(*Combines two invariance ASSUMPTIONS into one. USEFUL??*)
|
|
504 |
val Always_Int_tac = dtac Always_Int_I THEN' assume_tac THEN' etac Always_thin;
|
|
505 |
|
|
506 |
(*Combines a list of invariance THEOREMS into one.*)
|
|
507 |
val Always_Int_rule = foldr1 (fn (th1,th2) => [th1,th2] MRS Always_Int_I);
|
|
508 |
|
|
509 |
(*** Increasing ***)
|
|
510 |
|
|
511 |
Goalw [Increasing_on_def]
|
|
512 |
"[| F:Increasing_on(A, f, r); a:A |] ==> F: Stable({s:state. <a,f`s>:r})";
|
|
513 |
by (Blast_tac 1);
|
|
514 |
qed "Increasing_onD";
|
|
515 |
|
|
516 |
Goalw [Increasing_on_def]
|
|
517 |
"F:Increasing_on(A, f, r) ==> F:program & f:state->A & part_order(A,r)";
|
|
518 |
by (auto_tac (claset(), simpset() addsimps [INT_iff]));
|
|
519 |
qed "Increasing_onD2";
|
|
520 |
|
|
521 |
Goalw [Increasing_on_def, Stable_def, Constrains_def, stable_def, constrains_def, part_order_def]
|
|
522 |
"!!f. g:mono_map(A,r,A,r) \
|
|
523 |
\ ==> Increasing_on(A, f, r) <= Increasing_on(A, g O f, r)";
|
|
524 |
by (asm_full_simp_tac (simpset() addsimps [INT_iff,condition_def, mono_map_def]) 1);
|
|
525 |
by (auto_tac (claset() addIs [comp_fun], simpset() addsimps [mono_map_def]));
|
|
526 |
by (force_tac (claset() addSDs [bspec, ActsD], simpset()) 1);
|
|
527 |
by (subgoal_tac "xd:state" 1);
|
|
528 |
by (blast_tac (claset() addSDs [ActsD]) 2);
|
|
529 |
by (subgoal_tac "f`xe:A & f`xd:A" 1);
|
|
530 |
by (blast_tac (claset() addDs [apply_type]) 2);
|
|
531 |
by (rotate_tac 3 1);
|
|
532 |
by (dres_inst_tac [("x", "f`xe")] bspec 1);
|
|
533 |
by (Asm_simp_tac 1);
|
|
534 |
by (REPEAT(etac conjE 1));
|
|
535 |
by (rotate_tac ~3 1);
|
|
536 |
by (dres_inst_tac [("x", "xc")] bspec 1);
|
|
537 |
by (Asm_simp_tac 1);
|
|
538 |
by (dres_inst_tac [("c", "xd")] subsetD 1);
|
|
539 |
by (rtac imageI 1);
|
|
540 |
by Auto_tac;
|
|
541 |
by (asm_full_simp_tac (simpset() addsimps [refl_def]) 1);
|
|
542 |
by (dres_inst_tac [("x", "f`xe")] bspec 1);
|
|
543 |
by (dres_inst_tac [("x", "f`xd")] bspec 2);
|
|
544 |
by (ALLGOALS(Asm_simp_tac));
|
|
545 |
by (dres_inst_tac [("b", "g`(f`xe)")] trans_onD 1);
|
|
546 |
by Auto_tac;
|
|
547 |
qed "mono_Increasing_on_comp";
|
|
548 |
|
|
549 |
Goalw [increasing_on_def, Increasing_on_def]
|
|
550 |
"F : increasing_on(A, f,r) ==> F : Increasing_on(A, f,r)";
|
|
551 |
by (Clarify_tac 1);
|
|
552 |
by (asm_full_simp_tac (simpset() addsimps [INT_iff]) 1);
|
|
553 |
by (blast_tac (claset() addIs [stable_imp_Stable]) 1);
|
|
554 |
qed "increasing_on_imp_Increasing_on";
|
|
555 |
|
|
556 |
bind_thm("Increasing_on_constant", increasing_on_constant RS increasing_on_imp_Increasing_on);
|
|
557 |
Addsimps [Increasing_on_constant];
|
|
558 |
|
|
559 |
Goalw [Increasing_on_def, nat_order_def]
|
|
560 |
"[| F:Increasing_on(nat,f, nat_order); z:nat |] \
|
|
561 |
\ ==> F: Stable({s:state. z < f`s})";
|
|
562 |
by (Clarify_tac 1);
|
|
563 |
by (asm_full_simp_tac (simpset() addsimps [INT_iff]) 1);
|
|
564 |
by Safe_tac;
|
|
565 |
by (dres_inst_tac [("x", "succ(z)")] bspec 1);
|
|
566 |
by (auto_tac (claset(), simpset() addsimps [apply_type, Collect_conj_eq]));
|
|
567 |
by (subgoal_tac "{x: state . f ` x : nat} = state" 1);
|
|
568 |
by Auto_tac;
|
|
569 |
qed "strict_Increasing_onD";
|
|
570 |
|
|
571 |
(*To allow expansion of the program's definition when appropriate*)
|
|
572 |
val program_defs_ref = ref ([] : thm list);
|
|
573 |
|
|
574 |
(*proves "co" properties when the program is specified*)
|
|
575 |
|
|
576 |
fun constrains_tac i =
|
|
577 |
SELECT_GOAL
|
|
578 |
(EVERY [REPEAT (Always_Int_tac 1),
|
|
579 |
REPEAT (etac Always_ConstrainsI 1
|
|
580 |
ORELSE
|
|
581 |
resolve_tac [StableI, stableI,
|
|
582 |
constrains_imp_Constrains] 1),
|
|
583 |
rtac constrainsI 1,
|
|
584 |
full_simp_tac (simpset() addsimps !program_defs_ref) 1,
|
|
585 |
ALLGOALS Clarify_tac,
|
|
586 |
REPEAT (FIRSTGOAL (etac disjE)),
|
|
587 |
ALLGOALS Clarify_tac,
|
|
588 |
REPEAT (FIRSTGOAL (etac disjE)),
|
|
589 |
ALLGOALS Clarify_tac,
|
|
590 |
ALLGOALS Asm_full_simp_tac,
|
|
591 |
ALLGOALS Clarify_tac]) i;
|
|
592 |
|
|
593 |
(*For proving invariants*)
|
|
594 |
fun always_tac i =
|
|
595 |
rtac AlwaysI i THEN Force_tac i THEN constrains_tac i;
|