author | paulson |
Thu, 30 Jan 2003 18:08:09 +0100 | |
changeset 13797 | baefae13ad37 |
parent 6823 | 97babc436a41 |
child 13798 | 4c1a53627500 |
permissions | -rw-r--r-- |
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset
|
1 |
(* Title: HOL/UNITY/Constrains |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset
|
2 |
ID: $Id$ |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset
|
4 |
Copyright 1998 University of Cambridge |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset
|
5 |
|
13797 | 6 |
Weak safety relations: restricted to the set of reachable states. |
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset
|
7 |
*) |
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset
|
8 |
|
13797 | 9 |
theory Constrains = UNITY: |
6535 | 10 |
|
11 |
consts traces :: "['a set, ('a * 'a)set set] => ('a * 'a list) set" |
|
12 |
||
13 |
(*Initial states and program => (final state, reversed trace to it)... |
|
14 |
Arguments MUST be curried in an inductive definition*) |
|
15 |
||
16 |
inductive "traces init acts" |
|
13797 | 17 |
intros |
6535 | 18 |
(*Initial trace is empty*) |
13797 | 19 |
Init: "s: init ==> (s,[]) : traces init acts" |
6535 | 20 |
|
13797 | 21 |
Acts: "[| act: acts; (s,evs) : traces init acts; (s,s'): act |] |
22 |
==> (s', s#evs) : traces init acts" |
|
6535 | 23 |
|
24 |
||
25 |
consts reachable :: "'a program => 'a set" |
|
26 |
||
27 |
inductive "reachable F" |
|
13797 | 28 |
intros |
29 |
Init: "s: Init F ==> s : reachable F" |
|
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset
|
30 |
|
13797 | 31 |
Acts: "[| act: Acts F; s : reachable F; (s,s'): act |] |
32 |
==> s' : reachable F" |
|
6536 | 33 |
|
13797 | 34 |
constdefs |
35 |
Constrains :: "['a set, 'a set] => 'a program set" (infixl "Co" 60) |
|
6575 | 36 |
"A Co B == {F. F : (reachable F Int A) co B}" |
6536 | 37 |
|
13797 | 38 |
Unless :: "['a set, 'a set] => 'a program set" (infixl "Unless" 60) |
6536 | 39 |
"A Unless B == (A-B) Co (A Un B)" |
40 |
||
5648 | 41 |
Stable :: "'a set => 'a program set" |
6536 | 42 |
"Stable A == A Co A" |
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset
|
43 |
|
6570 | 44 |
(*Always is the weak form of "invariant"*) |
45 |
Always :: "'a set => 'a program set" |
|
46 |
"Always A == {F. Init F <= A} Int Stable A" |
|
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset
|
47 |
|
5784 | 48 |
(*Polymorphic in both states and the meaning of <= *) |
6705 | 49 |
Increasing :: "['a => 'b::{order}] => 'a program set" |
5784 | 50 |
"Increasing f == INT z. Stable {s. z <= f s}" |
51 |
||
13797 | 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 |
||
5313
1861a564d7e2
Constrains, Stable, Invariant...more of the substitution axiom, but Union
paulson
parents:
diff
changeset
|
393 |
end |