4 Copyright 1998 University of Cambridge |
4 Copyright 1998 University of Cambridge |
5 |
5 |
6 Weak 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 header{*Weak Safety*} |
|
10 |
9 theory Constrains = UNITY: |
11 theory Constrains = UNITY: |
10 |
12 |
11 consts traces :: "['a set, ('a * 'a)set set] => ('a * 'a list) set" |
13 consts traces :: "['a set, ('a * 'a)set set] => ('a * 'a list) set" |
12 |
14 |
13 (*Initial states and program => (final state, reversed trace to it)... |
15 (*Initial states and program => (final state, reversed trace to it)... |
48 (*Polymorphic in both states and the meaning of <= *) |
50 (*Polymorphic in both states and the meaning of <= *) |
49 Increasing :: "['a => 'b::{order}] => 'a program set" |
51 Increasing :: "['a => 'b::{order}] => 'a program set" |
50 "Increasing f == INT z. Stable {s. z <= f s}" |
52 "Increasing f == INT z. Stable {s. z <= f s}" |
51 |
53 |
52 |
54 |
53 (*** traces and reachable ***) |
55 subsection{*traces and reachable*} |
54 |
56 |
55 lemma reachable_equiv_traces: |
57 lemma reachable_equiv_traces: |
56 "reachable F = {s. EX evs. (s,evs): traces (Init F) (Acts F)}" |
58 "reachable F = {s. EX evs. (s,evs): traces (Init F) (Acts F)}" |
57 apply safe |
59 apply safe |
58 apply (erule_tac [2] traces.induct) |
60 apply (erule_tac [2] traces.induct) |
80 apply (erule reachable.induct) |
82 apply (erule reachable.induct) |
81 apply (blast intro: reachable.intros)+ |
83 apply (blast intro: reachable.intros)+ |
82 done |
84 done |
83 |
85 |
84 |
86 |
85 (*** Co ***) |
87 subsection{*Co*} |
86 |
88 |
87 (*F : B co B' ==> F : (reachable F Int B) co (reachable F Int B')*) |
89 (*F : B co B' ==> F : (reachable F Int B) co (reachable F Int B')*) |
88 lemmas constrains_reachable_Int = |
90 lemmas constrains_reachable_Int = |
89 subset_refl [THEN stable_reachable [unfolded stable_def], |
91 subset_refl [THEN stable_reachable [unfolded stable_def], |
90 THEN constrains_Int, standard] |
92 THEN constrains_Int, standard] |
182 lemma Constrains_cancel: |
184 lemma Constrains_cancel: |
183 "[| F : A Co (A' Un B); F : B Co B' |] ==> F : A Co (A' Un B')" |
185 "[| 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) |
186 by (simp add: Constrains_eq_constrains constrains_def, blast) |
185 |
187 |
186 |
188 |
187 (*** Stable ***) |
189 subsection{*Stable*} |
188 |
190 |
189 (*Useful because there's no Stable_weaken. [Tanja Vos]*) |
191 (*Useful because there's no Stable_weaken. [Tanja Vos]*) |
190 lemma Stable_eq: "[| F: Stable A; A = B |] ==> F : Stable B" |
192 lemma Stable_eq: "[| F: Stable A; A = B |] ==> F : Stable B" |
191 by blast |
193 by blast |
192 |
194 |
236 lemma Stable_reachable: "F : Stable (reachable F)" |
238 lemma Stable_reachable: "F : Stable (reachable F)" |
237 by (simp add: Stable_eq_stable) |
239 by (simp add: Stable_eq_stable) |
238 |
240 |
239 |
241 |
240 |
242 |
241 (*** Increasing ***) |
243 subsection{*Increasing*} |
242 |
244 |
243 lemma IncreasingD: |
245 lemma IncreasingD: |
244 "F : Increasing f ==> F : Stable {s. x <= f s}" |
246 "F : Increasing f ==> F : Stable {s. x <= f s}" |
245 by (unfold Increasing_def, blast) |
247 by (unfold Increasing_def, blast) |
246 |
248 |
263 |
265 |
264 lemmas Increasing_constant = |
266 lemmas Increasing_constant = |
265 increasing_constant [THEN increasing_imp_Increasing, standard, iff] |
267 increasing_constant [THEN increasing_imp_Increasing, standard, iff] |
266 |
268 |
267 |
269 |
268 (*** The Elimination Theorem. The "free" m has become universally quantified! |
270 subsection{*The Elimination Theorem*} |
269 Should the premise be !!m instead of ALL m ? Would make it harder to use |
271 |
270 in forward proof. ***) |
272 (*The "free" m has become universally quantified! Should the premise be !!m |
|
273 instead of ALL m ? Would make it harder to use in forward proof.*) |
271 |
274 |
272 lemma Elimination: |
275 lemma Elimination: |
273 "[| ALL m. F : {s. s x = m} Co (B m) |] |
276 "[| ALL m. F : {s. s x = m} Co (B m) |] |
274 ==> F : {s. s x : M} Co (UN m:M. B m)" |
277 ==> F : {s. s x : M} Co (UN m:M. B m)" |
275 |
|
276 by (unfold Constrains_def constrains_def, blast) |
278 by (unfold Constrains_def constrains_def, blast) |
277 |
279 |
278 (*As above, but for the trivial case of a one-variable state, in which the |
280 (*As above, but for the trivial case of a one-variable state, in which the |
279 state is identified with its one variable.*) |
281 state is identified with its one variable.*) |
280 lemma Elimination_sing: |
282 lemma Elimination_sing: |
281 "(ALL m. F : {m} Co (B m)) ==> F : M Co (UN m:M. B m)" |
283 "(ALL m. F : {m} Co (B m)) ==> F : M Co (UN m:M. B m)" |
282 by (unfold Constrains_def constrains_def, blast) |
284 by (unfold Constrains_def constrains_def, blast) |
283 |
285 |
284 |
286 |
285 (*** Specialized laws for handling Always ***) |
287 subsection{*Specialized laws for handling Always*} |
286 |
288 |
287 (** Natural deduction rules for "Always A" **) |
289 (** Natural deduction rules for "Always A" **) |
288 |
290 |
289 lemma AlwaysI: "[| Init F<=A; F : Stable A |] ==> F : Always A" |
291 lemma AlwaysI: "[| Init F<=A; F : Stable A |] ==> F : Always A" |
290 by (simp add: Always_def) |
292 by (simp add: Always_def) |
338 |
340 |
339 lemma Always_weaken: "[| F : Always A; A <= B |] ==> F : Always B" |
341 lemma Always_weaken: "[| F : Always A; A <= B |] ==> F : Always B" |
340 by (auto simp add: Always_eq_includes_reachable) |
342 by (auto simp add: Always_eq_includes_reachable) |
341 |
343 |
342 |
344 |
343 (*** "Co" rules involving Always ***) |
345 subsection{*"Co" rules involving Always*} |
344 |
346 |
345 lemma Always_Constrains_pre: |
347 lemma Always_Constrains_pre: |
346 "F : Always INV ==> (F : (INV Int A) Co A') = (F : A Co A')" |
348 "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 |
349 by (simp add: Always_includes_reachable [THEN Int_absorb2] Constrains_def |
348 Int_assoc [symmetric]) |
350 Int_assoc [symmetric]) |