1 (* Title: HOL/UNITY/Constrains |
1 (* Title: HOL/UNITY/Constrains |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
4 Copyright 1998 University of Cambridge |
4 Copyright 1998 University of Cambridge |
5 |
5 |
6 Safety relations: restricted to the set of reachable states. |
6 Weak safety relations: restricted to the set of reachable states. |
7 *) |
7 *) |
8 |
8 |
9 Constrains = UNITY + |
9 theory Constrains = UNITY: |
10 |
10 |
11 consts traces :: "['a set, ('a * 'a)set set] => ('a * 'a list) set" |
11 consts traces :: "['a set, ('a * 'a)set set] => ('a * 'a list) set" |
12 |
12 |
13 (*Initial states and program => (final state, reversed trace to it)... |
13 (*Initial states and program => (final state, reversed trace to it)... |
14 Arguments MUST be curried in an inductive definition*) |
14 Arguments MUST be curried in an inductive definition*) |
15 |
15 |
16 inductive "traces init acts" |
16 inductive "traces init acts" |
17 intrs |
17 intros |
18 (*Initial trace is empty*) |
18 (*Initial trace is empty*) |
19 Init "s: init ==> (s,[]) : traces init acts" |
19 Init: "s: init ==> (s,[]) : traces init acts" |
20 |
20 |
21 Acts "[| act: acts; (s,evs) : traces init acts; (s,s'): act |] |
21 Acts: "[| act: acts; (s,evs) : traces init acts; (s,s'): act |] |
22 ==> (s', s#evs) : traces init acts" |
22 ==> (s', s#evs) : traces init acts" |
23 |
23 |
24 |
24 |
25 consts reachable :: "'a program => 'a set" |
25 consts reachable :: "'a program => 'a set" |
26 |
26 |
27 inductive "reachable F" |
27 inductive "reachable F" |
28 intrs |
28 intros |
29 Init "s: Init F ==> s : reachable F" |
29 Init: "s: Init F ==> s : reachable F" |
30 |
30 |
31 Acts "[| act: Acts F; s : reachable F; (s,s'): act |] |
31 Acts: "[| act: Acts F; s : reachable F; (s,s'): act |] |
32 ==> s' : reachable F" |
32 ==> s' : reachable F" |
33 |
33 |
34 consts |
34 constdefs |
35 Constrains :: "['a set, 'a set] => 'a program set" (infixl "Co" 60) |
35 Constrains :: "['a set, 'a set] => 'a program set" (infixl "Co" 60) |
36 op_Unless :: "['a set, 'a set] => 'a program set" (infixl "Unless" 60) |
|
37 |
|
38 defs |
|
39 Constrains_def |
|
40 "A Co B == {F. F : (reachable F Int A) co B}" |
36 "A Co B == {F. F : (reachable F Int A) co B}" |
41 |
37 |
42 Unless_def |
38 Unless :: "['a set, 'a set] => 'a program set" (infixl "Unless" 60) |
43 "A Unless B == (A-B) Co (A Un B)" |
39 "A Unless B == (A-B) Co (A Un B)" |
44 |
|
45 constdefs |
|
46 |
40 |
47 Stable :: "'a set => 'a program set" |
41 Stable :: "'a set => 'a program set" |
48 "Stable A == A Co A" |
42 "Stable A == A Co A" |
49 |
43 |
50 (*Always is the weak form of "invariant"*) |
44 (*Always is the weak form of "invariant"*) |
53 |
47 |
54 (*Polymorphic in both states and the meaning of <= *) |
48 (*Polymorphic in both states and the meaning of <= *) |
55 Increasing :: "['a => 'b::{order}] => 'a program set" |
49 Increasing :: "['a => 'b::{order}] => 'a program set" |
56 "Increasing f == INT z. Stable {s. z <= f s}" |
50 "Increasing f == INT z. Stable {s. z <= f s}" |
57 |
51 |
|
52 |
|
53 (*** traces and reachable ***) |
|
54 |
|
55 lemma reachable_equiv_traces: |
|
56 "reachable F = {s. EX evs. (s,evs): traces (Init F) (Acts F)}" |
|
57 apply safe |
|
58 apply (erule_tac [2] traces.induct) |
|
59 apply (erule reachable.induct) |
|
60 apply (blast intro: reachable.intros traces.intros)+ |
|
61 done |
|
62 |
|
63 lemma Init_subset_reachable: "Init F <= reachable F" |
|
64 by (blast intro: reachable.intros) |
|
65 |
|
66 lemma stable_reachable [intro!,simp]: |
|
67 "Acts G <= Acts F ==> G : stable (reachable F)" |
|
68 by (blast intro: stableI constrainsI reachable.intros) |
|
69 |
|
70 (*The set of all reachable states is an invariant...*) |
|
71 lemma invariant_reachable: "F : invariant (reachable F)" |
|
72 apply (simp add: invariant_def) |
|
73 apply (blast intro: reachable.intros) |
|
74 done |
|
75 |
|
76 (*...in fact the strongest invariant!*) |
|
77 lemma invariant_includes_reachable: "F : invariant A ==> reachable F <= A" |
|
78 apply (simp add: stable_def constrains_def invariant_def) |
|
79 apply (rule subsetI) |
|
80 apply (erule reachable.induct) |
|
81 apply (blast intro: reachable.intros)+ |
|
82 done |
|
83 |
|
84 |
|
85 (*** Co ***) |
|
86 |
|
87 (*F : B co B' ==> F : (reachable F Int B) co (reachable F Int B')*) |
|
88 lemmas constrains_reachable_Int = |
|
89 subset_refl [THEN stable_reachable [unfolded stable_def], |
|
90 THEN constrains_Int, standard] |
|
91 |
|
92 (*Resembles the previous definition of Constrains*) |
|
93 lemma Constrains_eq_constrains: |
|
94 "A Co B = {F. F : (reachable F Int A) co (reachable F Int B)}" |
|
95 apply (unfold Constrains_def) |
|
96 apply (blast dest: constrains_reachable_Int intro: constrains_weaken) |
|
97 done |
|
98 |
|
99 lemma constrains_imp_Constrains: "F : A co A' ==> F : A Co A'" |
|
100 apply (unfold Constrains_def) |
|
101 apply (blast intro: constrains_weaken_L) |
|
102 done |
|
103 |
|
104 lemma stable_imp_Stable: "F : stable A ==> F : Stable A" |
|
105 apply (unfold stable_def Stable_def) |
|
106 apply (erule constrains_imp_Constrains) |
|
107 done |
|
108 |
|
109 lemma ConstrainsI: |
|
110 "(!!act s s'. [| act: Acts F; (s,s') : act; s: A |] ==> s': A') |
|
111 ==> F : A Co A'" |
|
112 apply (rule constrains_imp_Constrains) |
|
113 apply (blast intro: constrainsI) |
|
114 done |
|
115 |
|
116 lemma Constrains_empty [iff]: "F : {} Co B" |
|
117 by (unfold Constrains_def constrains_def, blast) |
|
118 |
|
119 lemma Constrains_UNIV [iff]: "F : A Co UNIV" |
|
120 by (blast intro: ConstrainsI) |
|
121 |
|
122 lemma Constrains_weaken_R: |
|
123 "[| F : A Co A'; A'<=B' |] ==> F : A Co B'" |
|
124 apply (unfold Constrains_def) |
|
125 apply (blast intro: constrains_weaken_R) |
|
126 done |
|
127 |
|
128 lemma Constrains_weaken_L: |
|
129 "[| F : A Co A'; B<=A |] ==> F : B Co A'" |
|
130 apply (unfold Constrains_def) |
|
131 apply (blast intro: constrains_weaken_L) |
|
132 done |
|
133 |
|
134 lemma Constrains_weaken: |
|
135 "[| F : A Co A'; B<=A; A'<=B' |] ==> F : B Co B'" |
|
136 apply (unfold Constrains_def) |
|
137 apply (blast intro: constrains_weaken) |
|
138 done |
|
139 |
|
140 (** Union **) |
|
141 |
|
142 lemma Constrains_Un: |
|
143 "[| F : A Co A'; F : B Co B' |] ==> F : (A Un B) Co (A' Un B')" |
|
144 apply (unfold Constrains_def) |
|
145 apply (blast intro: constrains_Un [THEN constrains_weaken]) |
|
146 done |
|
147 |
|
148 lemma Constrains_UN: |
|
149 assumes Co: "!!i. i:I ==> F : (A i) Co (A' i)" |
|
150 shows "F : (UN i:I. A i) Co (UN i:I. A' i)" |
|
151 apply (unfold Constrains_def) |
|
152 apply (rule CollectI) |
|
153 apply (rule Co [unfolded Constrains_def, THEN CollectD, THEN constrains_UN, |
|
154 THEN constrains_weaken], auto) |
|
155 done |
|
156 |
|
157 (** Intersection **) |
|
158 |
|
159 lemma Constrains_Int: |
|
160 "[| F : A Co A'; F : B Co B' |] ==> F : (A Int B) Co (A' Int B')" |
|
161 apply (unfold Constrains_def) |
|
162 apply (blast intro: constrains_Int [THEN constrains_weaken]) |
|
163 done |
|
164 |
|
165 lemma Constrains_INT: |
|
166 assumes Co: "!!i. i:I ==> F : (A i) Co (A' i)" |
|
167 shows "F : (INT i:I. A i) Co (INT i:I. A' i)" |
|
168 apply (unfold Constrains_def) |
|
169 apply (rule CollectI) |
|
170 apply (rule Co [unfolded Constrains_def, THEN CollectD, THEN constrains_INT, |
|
171 THEN constrains_weaken], auto) |
|
172 done |
|
173 |
|
174 lemma Constrains_imp_subset: "F : A Co A' ==> reachable F Int A <= A'" |
|
175 by (simp add: constrains_imp_subset Constrains_def) |
|
176 |
|
177 lemma Constrains_trans: "[| F : A Co B; F : B Co C |] ==> F : A Co C" |
|
178 apply (simp add: Constrains_eq_constrains) |
|
179 apply (blast intro: constrains_trans constrains_weaken) |
|
180 done |
|
181 |
|
182 lemma Constrains_cancel: |
|
183 "[| F : A Co (A' Un B); F : B Co B' |] ==> F : A Co (A' Un B')" |
|
184 by (simp add: Constrains_eq_constrains constrains_def, blast) |
|
185 |
|
186 |
|
187 (*** Stable ***) |
|
188 |
|
189 (*Useful because there's no Stable_weaken. [Tanja Vos]*) |
|
190 lemma Stable_eq: "[| F: Stable A; A = B |] ==> F : Stable B" |
|
191 by blast |
|
192 |
|
193 lemma Stable_eq_stable: "(F : Stable A) = (F : stable (reachable F Int A))" |
|
194 by (simp add: Stable_def Constrains_eq_constrains stable_def) |
|
195 |
|
196 lemma StableI: "F : A Co A ==> F : Stable A" |
|
197 by (unfold Stable_def, assumption) |
|
198 |
|
199 lemma StableD: "F : Stable A ==> F : A Co A" |
|
200 by (unfold Stable_def, assumption) |
|
201 |
|
202 lemma Stable_Un: |
|
203 "[| F : Stable A; F : Stable A' |] ==> F : Stable (A Un A')" |
|
204 apply (unfold Stable_def) |
|
205 apply (blast intro: Constrains_Un) |
|
206 done |
|
207 |
|
208 lemma Stable_Int: |
|
209 "[| F : Stable A; F : Stable A' |] ==> F : Stable (A Int A')" |
|
210 apply (unfold Stable_def) |
|
211 apply (blast intro: Constrains_Int) |
|
212 done |
|
213 |
|
214 lemma Stable_Constrains_Un: |
|
215 "[| F : Stable C; F : A Co (C Un A') |] |
|
216 ==> F : (C Un A) Co (C Un A')" |
|
217 apply (unfold Stable_def) |
|
218 apply (blast intro: Constrains_Un [THEN Constrains_weaken]) |
|
219 done |
|
220 |
|
221 lemma Stable_Constrains_Int: |
|
222 "[| F : Stable C; F : (C Int A) Co A' |] |
|
223 ==> F : (C Int A) Co (C Int A')" |
|
224 apply (unfold Stable_def) |
|
225 apply (blast intro: Constrains_Int [THEN Constrains_weaken]) |
|
226 done |
|
227 |
|
228 lemma Stable_UN: |
|
229 "(!!i. i:I ==> F : Stable (A i)) ==> F : Stable (UN i:I. A i)" |
|
230 by (simp add: Stable_def Constrains_UN) |
|
231 |
|
232 lemma Stable_INT: |
|
233 "(!!i. i:I ==> F : Stable (A i)) ==> F : Stable (INT i:I. A i)" |
|
234 by (simp add: Stable_def Constrains_INT) |
|
235 |
|
236 lemma Stable_reachable: "F : Stable (reachable F)" |
|
237 by (simp add: Stable_eq_stable) |
|
238 |
|
239 |
|
240 |
|
241 (*** Increasing ***) |
|
242 |
|
243 lemma IncreasingD: |
|
244 "F : Increasing f ==> F : Stable {s. x <= f s}" |
|
245 by (unfold Increasing_def, blast) |
|
246 |
|
247 lemma mono_Increasing_o: |
|
248 "mono g ==> Increasing f <= Increasing (g o f)" |
|
249 apply (simp add: Increasing_def Stable_def Constrains_def stable_def |
|
250 constrains_def) |
|
251 apply (blast intro: monoD order_trans) |
|
252 done |
|
253 |
|
254 lemma strict_IncreasingD: |
|
255 "!!z::nat. F : Increasing f ==> F: Stable {s. z < f s}" |
|
256 by (simp add: Increasing_def Suc_le_eq [symmetric]) |
|
257 |
|
258 lemma increasing_imp_Increasing: |
|
259 "F : increasing f ==> F : Increasing f" |
|
260 apply (unfold increasing_def Increasing_def) |
|
261 apply (blast intro: stable_imp_Stable) |
|
262 done |
|
263 |
|
264 lemmas Increasing_constant = |
|
265 increasing_constant [THEN increasing_imp_Increasing, standard, iff] |
|
266 |
|
267 |
|
268 (*** The Elimination Theorem. The "free" m has become universally quantified! |
|
269 Should the premise be !!m instead of ALL m ? Would make it harder to use |
|
270 in forward proof. ***) |
|
271 |
|
272 lemma Elimination: |
|
273 "[| ALL m. F : {s. s x = m} Co (B m) |] |
|
274 ==> F : {s. s x : M} Co (UN m:M. B m)" |
|
275 |
|
276 by (unfold Constrains_def constrains_def, blast) |
|
277 |
|
278 (*As above, but for the trivial case of a one-variable state, in which the |
|
279 state is identified with its one variable.*) |
|
280 lemma Elimination_sing: |
|
281 "(ALL m. F : {m} Co (B m)) ==> F : M Co (UN m:M. B m)" |
|
282 by (unfold Constrains_def constrains_def, blast) |
|
283 |
|
284 |
|
285 (*** Specialized laws for handling Always ***) |
|
286 |
|
287 (** Natural deduction rules for "Always A" **) |
|
288 |
|
289 lemma AlwaysI: "[| Init F<=A; F : Stable A |] ==> F : Always A" |
|
290 by (simp add: Always_def) |
|
291 |
|
292 lemma AlwaysD: "F : Always A ==> Init F<=A & F : Stable A" |
|
293 by (simp add: Always_def) |
|
294 |
|
295 lemmas AlwaysE = AlwaysD [THEN conjE, standard] |
|
296 lemmas Always_imp_Stable = AlwaysD [THEN conjunct2, standard] |
|
297 |
|
298 |
|
299 (*The set of all reachable states is Always*) |
|
300 lemma Always_includes_reachable: "F : Always A ==> reachable F <= A" |
|
301 apply (simp add: Stable_def Constrains_def constrains_def Always_def) |
|
302 apply (rule subsetI) |
|
303 apply (erule reachable.induct) |
|
304 apply (blast intro: reachable.intros)+ |
|
305 done |
|
306 |
|
307 lemma invariant_imp_Always: |
|
308 "F : invariant A ==> F : Always A" |
|
309 apply (unfold Always_def invariant_def Stable_def stable_def) |
|
310 apply (blast intro: constrains_imp_Constrains) |
|
311 done |
|
312 |
|
313 lemmas Always_reachable = |
|
314 invariant_reachable [THEN invariant_imp_Always, standard] |
|
315 |
|
316 lemma Always_eq_invariant_reachable: |
|
317 "Always A = {F. F : invariant (reachable F Int A)}" |
|
318 apply (simp add: Always_def invariant_def Stable_def Constrains_eq_constrains |
|
319 stable_def) |
|
320 apply (blast intro: reachable.intros) |
|
321 done |
|
322 |
|
323 (*the RHS is the traditional definition of the "always" operator*) |
|
324 lemma Always_eq_includes_reachable: "Always A = {F. reachable F <= A}" |
|
325 by (auto dest: invariant_includes_reachable simp add: Int_absorb2 invariant_reachable Always_eq_invariant_reachable) |
|
326 |
|
327 lemma Always_UNIV_eq [simp]: "Always UNIV = UNIV" |
|
328 by (auto simp add: Always_eq_includes_reachable) |
|
329 |
|
330 lemma UNIV_AlwaysI: "UNIV <= A ==> F : Always A" |
|
331 by (auto simp add: Always_eq_includes_reachable) |
|
332 |
|
333 lemma Always_eq_UN_invariant: "Always A = (UN I: Pow A. invariant I)" |
|
334 apply (simp add: Always_eq_includes_reachable) |
|
335 apply (blast intro: invariantI Init_subset_reachable [THEN subsetD] |
|
336 invariant_includes_reachable [THEN subsetD]) |
|
337 done |
|
338 |
|
339 lemma Always_weaken: "[| F : Always A; A <= B |] ==> F : Always B" |
|
340 by (auto simp add: Always_eq_includes_reachable) |
|
341 |
|
342 |
|
343 (*** "Co" rules involving Always ***) |
|
344 |
|
345 lemma Always_Constrains_pre: |
|
346 "F : Always INV ==> (F : (INV Int A) Co A') = (F : A Co A')" |
|
347 by (simp add: Always_includes_reachable [THEN Int_absorb2] Constrains_def |
|
348 Int_assoc [symmetric]) |
|
349 |
|
350 lemma Always_Constrains_post: |
|
351 "F : Always INV ==> (F : A Co (INV Int A')) = (F : A Co A')" |
|
352 by (simp add: Always_includes_reachable [THEN Int_absorb2] |
|
353 Constrains_eq_constrains Int_assoc [symmetric]) |
|
354 |
|
355 (* [| F : Always INV; F : (INV Int A) Co A' |] ==> F : A Co A' *) |
|
356 lemmas Always_ConstrainsI = Always_Constrains_pre [THEN iffD1, standard] |
|
357 |
|
358 (* [| F : Always INV; F : A Co A' |] ==> F : A Co (INV Int A') *) |
|
359 lemmas Always_ConstrainsD = Always_Constrains_post [THEN iffD2, standard] |
|
360 |
|
361 (*The analogous proof of Always_LeadsTo_weaken doesn't terminate*) |
|
362 lemma Always_Constrains_weaken: |
|
363 "[| F : Always C; F : A Co A'; |
|
364 C Int B <= A; C Int A' <= B' |] |
|
365 ==> F : B Co B'" |
|
366 apply (rule Always_ConstrainsI, assumption) |
|
367 apply (drule Always_ConstrainsD, assumption) |
|
368 apply (blast intro: Constrains_weaken) |
|
369 done |
|
370 |
|
371 |
|
372 (** Conjoining Always properties **) |
|
373 |
|
374 lemma Always_Int_distrib: "Always (A Int B) = Always A Int Always B" |
|
375 by (auto simp add: Always_eq_includes_reachable) |
|
376 |
|
377 lemma Always_INT_distrib: "Always (INTER I A) = (INT i:I. Always (A i))" |
|
378 by (auto simp add: Always_eq_includes_reachable) |
|
379 |
|
380 lemma Always_Int_I: |
|
381 "[| F : Always A; F : Always B |] ==> F : Always (A Int B)" |
|
382 by (simp add: Always_Int_distrib) |
|
383 |
|
384 (*Allows a kind of "implication introduction"*) |
|
385 lemma Always_Compl_Un_eq: |
|
386 "F : Always A ==> (F : Always (-A Un B)) = (F : Always B)" |
|
387 by (auto simp add: Always_eq_includes_reachable) |
|
388 |
|
389 (*Delete the nearest invariance assumption (which will be the second one |
|
390 used by Always_Int_I) *) |
|
391 lemmas Always_thin = thin_rl [of "F : Always A", standard] |
|
392 |
58 end |
393 end |