19 |
19 |
20 syntax (xsymbols) |
20 syntax (xsymbols) |
21 "op LeadsTo" :: "['a set, 'a set] => 'a program set" (infixl " \<longmapsto>w " 60) |
21 "op LeadsTo" :: "['a set, 'a set] => 'a program set" (infixl " \<longmapsto>w " 60) |
22 |
22 |
23 |
23 |
24 (*Resembles the previous definition of LeadsTo*) |
24 text{*Resembles the previous definition of LeadsTo*} |
25 lemma LeadsTo_eq_leadsTo: |
25 lemma LeadsTo_eq_leadsTo: |
26 "A LeadsTo B = {F. F \<in> (reachable F \<inter> A) leadsTo (reachable F \<inter> B)}" |
26 "A LeadsTo B = {F. F \<in> (reachable F \<inter> A) leadsTo (reachable F \<inter> B)}" |
27 apply (unfold LeadsTo_def) |
27 apply (unfold LeadsTo_def) |
28 apply (blast dest: psp_stable2 intro: leadsTo_weaken) |
28 apply (blast dest: psp_stable2 intro: leadsTo_weaken) |
29 done |
29 done |
74 subsection{*Derived rules*} |
74 subsection{*Derived rules*} |
75 |
75 |
76 lemma LeadsTo_UNIV [simp]: "F \<in> A LeadsTo UNIV" |
76 lemma LeadsTo_UNIV [simp]: "F \<in> A LeadsTo UNIV" |
77 by (simp add: LeadsTo_def) |
77 by (simp add: LeadsTo_def) |
78 |
78 |
79 (*Useful with cancellation, disjunction*) |
79 text{*Useful with cancellation, disjunction*} |
80 lemma LeadsTo_Un_duplicate: |
80 lemma LeadsTo_Un_duplicate: |
81 "F \<in> A LeadsTo (A' \<union> A') ==> F \<in> A LeadsTo A'" |
81 "F \<in> A LeadsTo (A' \<union> A') ==> F \<in> A LeadsTo A'" |
82 by (simp add: Un_ac) |
82 by (simp add: Un_ac) |
83 |
83 |
84 lemma LeadsTo_Un_duplicate2: |
84 lemma LeadsTo_Un_duplicate2: |
89 "(!!i. i \<in> I ==> F \<in> (A i) LeadsTo B) ==> F \<in> (\<Union>i \<in> I. A i) LeadsTo B" |
89 "(!!i. i \<in> I ==> F \<in> (A i) LeadsTo B) ==> F \<in> (\<Union>i \<in> I. A i) LeadsTo B" |
90 apply (simp only: Union_image_eq [symmetric]) |
90 apply (simp only: Union_image_eq [symmetric]) |
91 apply (blast intro: LeadsTo_Union) |
91 apply (blast intro: LeadsTo_Union) |
92 done |
92 done |
93 |
93 |
94 (*Binary union introduction rule*) |
94 text{*Binary union introduction rule*} |
95 lemma LeadsTo_Un: |
95 lemma LeadsTo_Un: |
96 "[| F \<in> A LeadsTo C; F \<in> B LeadsTo C |] ==> F \<in> (A \<union> B) LeadsTo C" |
96 "[| F \<in> A LeadsTo C; F \<in> B LeadsTo C |] ==> F \<in> (A \<union> B) LeadsTo C" |
97 apply (subst Un_eq_Union) |
97 apply (subst Un_eq_Union) |
98 apply (blast intro: LeadsTo_Union) |
98 apply (blast intro: LeadsTo_Union) |
99 done |
99 done |
100 |
100 |
101 (*Lets us look at the starting state*) |
101 text{*Lets us look at the starting state*} |
102 lemma single_LeadsTo_I: |
102 lemma single_LeadsTo_I: |
103 "(!!s. s \<in> A ==> F \<in> {s} LeadsTo B) ==> F \<in> A LeadsTo B" |
103 "(!!s. s \<in> A ==> F \<in> {s} LeadsTo B) ==> F \<in> A LeadsTo B" |
104 by (subst UN_singleton [symmetric], rule LeadsTo_UN, blast) |
104 by (subst UN_singleton [symmetric], rule LeadsTo_UN, blast) |
105 |
105 |
106 lemma subset_imp_LeadsTo: "A \<subseteq> B ==> F \<in> A LeadsTo B" |
106 lemma subset_imp_LeadsTo: "A \<subseteq> B ==> F \<in> A LeadsTo B" |
180 ==> F \<in> A LeadsTo A'" |
180 ==> F \<in> A LeadsTo A'" |
181 apply (rule Always_LeadsToI, assumption) |
181 apply (rule Always_LeadsToI, assumption) |
182 apply (blast intro: EnsuresI LeadsTo_Basis Always_ConstrainsD [THEN Constrains_weaken] transient_strengthen) |
182 apply (blast intro: EnsuresI LeadsTo_Basis Always_ConstrainsD [THEN Constrains_weaken] transient_strengthen) |
183 done |
183 done |
184 |
184 |
185 (*Set difference: maybe combine with leadsTo_weaken_L?? |
185 text{*Set difference: maybe combine with leadsTo_weaken_L?? |
186 This is the most useful form of the "disjunction" rule*) |
186 This is the most useful form of the "disjunction" rule*} |
187 lemma LeadsTo_Diff: |
187 lemma LeadsTo_Diff: |
188 "[| F \<in> (A-B) LeadsTo C; F \<in> (A \<inter> B) LeadsTo C |] |
188 "[| F \<in> (A-B) LeadsTo C; F \<in> (A \<inter> B) LeadsTo C |] |
189 ==> F \<in> A LeadsTo C" |
189 ==> F \<in> A LeadsTo C" |
190 by (blast intro: LeadsTo_Un LeadsTo_weaken) |
190 by (blast intro: LeadsTo_Un LeadsTo_weaken) |
191 |
191 |
196 apply (simp only: Union_image_eq [symmetric]) |
196 apply (simp only: Union_image_eq [symmetric]) |
197 apply (blast intro: LeadsTo_Union LeadsTo_weaken_R) |
197 apply (blast intro: LeadsTo_Union LeadsTo_weaken_R) |
198 done |
198 done |
199 |
199 |
200 |
200 |
201 (*Version with no index set*) |
201 text{*Version with no index set*} |
202 lemma LeadsTo_UN_UN_noindex: |
202 lemma LeadsTo_UN_UN_noindex: |
203 "(!!i. F \<in> (A i) LeadsTo (A' i)) ==> F \<in> (\<Union>i. A i) LeadsTo (\<Union>i. A' i)" |
203 "(!!i. F \<in> (A i) LeadsTo (A' i)) ==> F \<in> (\<Union>i. A i) LeadsTo (\<Union>i. A' i)" |
204 by (blast intro: LeadsTo_UN_UN) |
204 by (blast intro: LeadsTo_UN_UN) |
205 |
205 |
206 (*Version with no index set*) |
206 text{*Version with no index set*} |
207 lemma all_LeadsTo_UN_UN: |
207 lemma all_LeadsTo_UN_UN: |
208 "\<forall>i. F \<in> (A i) LeadsTo (A' i) |
208 "\<forall>i. F \<in> (A i) LeadsTo (A' i) |
209 ==> F \<in> (\<Union>i. A i) LeadsTo (\<Union>i. A' i)" |
209 ==> F \<in> (\<Union>i. A i) LeadsTo (\<Union>i. A' i)" |
210 by (blast intro: LeadsTo_UN_UN) |
210 by (blast intro: LeadsTo_UN_UN) |
211 |
211 |
212 (*Binary union version*) |
212 text{*Binary union version*} |
213 lemma LeadsTo_Un_Un: |
213 lemma LeadsTo_Un_Un: |
214 "[| F \<in> A LeadsTo A'; F \<in> B LeadsTo B' |] |
214 "[| F \<in> A LeadsTo A'; F \<in> B LeadsTo B' |] |
215 ==> F \<in> (A \<union> B) LeadsTo (A' \<union> B')" |
215 ==> F \<in> (A \<union> B) LeadsTo (A' \<union> B')" |
216 by (blast intro: LeadsTo_Un LeadsTo_weaken_R) |
216 by (blast intro: LeadsTo_Un LeadsTo_weaken_R) |
217 |
217 |
245 prefer 2 apply assumption |
245 prefer 2 apply assumption |
246 apply (simp_all (no_asm_simp)) |
246 apply (simp_all (no_asm_simp)) |
247 done |
247 done |
248 |
248 |
249 |
249 |
250 (** The impossibility law **) |
250 text{*The impossibility law*} |
251 |
251 |
252 (*The set "A" may be non-empty, but it contains no reachable states*) |
252 text{*The set "A" may be non-empty, but it contains no reachable states*} |
253 lemma LeadsTo_empty: "F \<in> A LeadsTo {} ==> F \<in> Always (-A)" |
253 lemma LeadsTo_empty: "[|F \<in> A LeadsTo {}; all_total F|] ==> F \<in> Always (-A)" |
254 apply (simp add: LeadsTo_def Always_eq_includes_reachable) |
254 apply (simp add: LeadsTo_def Always_eq_includes_reachable) |
255 apply (drule leadsTo_empty, auto) |
255 apply (drule leadsTo_empty, auto) |
256 done |
256 done |
257 |
257 |
258 |
258 |
259 (** PSP: Progress-Safety-Progress **) |
259 subsection{*PSP: Progress-Safety-Progress*} |
260 |
260 |
261 (*Special case of PSP: Misra's "stable conjunction"*) |
261 text{*Special case of PSP: Misra's "stable conjunction"*} |
262 lemma PSP_Stable: |
262 lemma PSP_Stable: |
263 "[| F \<in> A LeadsTo A'; F \<in> Stable B |] |
263 "[| F \<in> A LeadsTo A'; F \<in> Stable B |] |
264 ==> F \<in> (A \<inter> B) LeadsTo (A' \<inter> B)" |
264 ==> F \<in> (A \<inter> B) LeadsTo (A' \<inter> B)" |
265 apply (simp add: LeadsTo_eq_leadsTo Stable_eq_stable) |
265 apply (simp add: LeadsTo_eq_leadsTo Stable_eq_stable) |
266 apply (drule psp_stable, assumption) |
266 apply (drule psp_stable, assumption) |
334 lemma LessThan_induct: |
334 lemma LessThan_induct: |
335 "(!!m::nat. F \<in> (A \<inter> f-`{m}) LeadsTo ((A \<inter> f-`(lessThan m)) \<union> B)) |
335 "(!!m::nat. F \<in> (A \<inter> f-`{m}) LeadsTo ((A \<inter> f-`(lessThan m)) \<union> B)) |
336 ==> F \<in> A LeadsTo B" |
336 ==> F \<in> A LeadsTo B" |
337 by (rule wf_less_than [THEN LeadsTo_wf_induct], auto) |
337 by (rule wf_less_than [THEN LeadsTo_wf_induct], auto) |
338 |
338 |
339 (*Integer version. Could generalize from 0 to any lower bound*) |
339 text{*Integer version. Could generalize from 0 to any lower bound*} |
340 lemma integ_0_le_induct: |
340 lemma integ_0_le_induct: |
341 "[| F \<in> Always {s. (0::int) \<le> f s}; |
341 "[| F \<in> Always {s. (0::int) \<le> f s}; |
342 !! z. F \<in> (A \<inter> {s. f s = z}) LeadsTo |
342 !! z. F \<in> (A \<inter> {s. f s = z}) LeadsTo |
343 ((A \<inter> {s. f s < z}) \<union> B) |] |
343 ((A \<inter> {s. f s < z}) \<union> B) |] |
344 ==> F \<in> A LeadsTo B" |
344 ==> F \<in> A LeadsTo B" |