author | nipkow |
Sun, 04 Nov 2018 12:07:24 +0100 | |
changeset 69232 | 2b913054a9cf |
parent 63120 | 629a4c5e953e |
child 69587 | 53982d5ec0bb |
permissions | -rw-r--r-- |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32149
diff
changeset
|
1 |
(* Title: ZF/UNITY/SubstAx.thy |
11479 | 2 |
Author: Sidi O Ehmety, Computer Laboratory |
3 |
Copyright 2001 University of Cambridge |
|
4 |
||
5 |
Theory ported from HOL. |
|
6 |
*) |
|
7 |
||
60770 | 8 |
section\<open>Weak LeadsTo relation (restricted to the set of reachable states)\<close> |
15634 | 9 |
|
10 |
theory SubstAx |
|
46953 | 11 |
imports WFair Constrains |
15634 | 12 |
begin |
11479 | 13 |
|
24893 | 14 |
definition |
15 |
(* The definitions below are not `conventional', but yield simpler rules *) |
|
16 |
Ensures :: "[i,i] => i" (infixl "Ensures" 60) where |
|
46953 | 17 |
"A Ensures B == {F \<in> program. F \<in> (reachable(F) \<inter> A) ensures (reachable(F) \<inter> B) }" |
11479 | 18 |
|
24893 | 19 |
definition |
61392 | 20 |
LeadsTo :: "[i, i] => i" (infixl "\<longmapsto>w" 60) where |
21 |
"A \<longmapsto>w B == {F \<in> program. F:(reachable(F) \<inter> A) \<longmapsto> (reachable(F) \<inter> B)}" |
|
15634 | 22 |
|
23 |
||
24 |
(*Resembles the previous definition of LeadsTo*) |
|
25 |
||
26 |
(* Equivalence with the HOL-like definition *) |
|
46953 | 27 |
lemma LeadsTo_eq: |
61392 | 28 |
"st_set(B)==> A \<longmapsto>w B = {F \<in> program. F:(reachable(F) \<inter> A) \<longmapsto> B}" |
15634 | 29 |
apply (unfold LeadsTo_def) |
30 |
apply (blast dest: psp_stable2 leadsToD2 constrainsD2 intro: leadsTo_weaken) |
|
31 |
done |
|
32 |
||
61392 | 33 |
lemma LeadsTo_type: "A \<longmapsto>w B <=program" |
15634 | 34 |
by (unfold LeadsTo_def, auto) |
35 |
||
36 |
(*** Specialized laws for handling invariants ***) |
|
37 |
||
38 |
(** Conjoining an Always property **) |
|
61392 | 39 |
lemma Always_LeadsTo_pre: "F \<in> Always(I) ==> (F:(I \<inter> A) \<longmapsto>w A') \<longleftrightarrow> (F \<in> A \<longmapsto>w A')" |
15634 | 40 |
by (simp add: LeadsTo_def Always_eq_includes_reachable Int_absorb2 Int_assoc [symmetric] leadsToD2) |
41 |
||
61392 | 42 |
lemma Always_LeadsTo_post: "F \<in> Always(I) ==> (F \<in> A \<longmapsto>w (I \<inter> A')) \<longleftrightarrow> (F \<in> A \<longmapsto>w A')" |
15634 | 43 |
apply (unfold LeadsTo_def) |
44 |
apply (simp add: Always_eq_includes_reachable Int_absorb2 Int_assoc [symmetric] leadsToD2) |
|
45 |
done |
|
46 |
||
47 |
(* Like 'Always_LeadsTo_pre RS iffD1', but with premises in the good order *) |
|
61392 | 48 |
lemma Always_LeadsToI: "[| F \<in> Always(C); F \<in> (C \<inter> A) \<longmapsto>w A' |] ==> F \<in> A \<longmapsto>w A'" |
15634 | 49 |
by (blast intro: Always_LeadsTo_pre [THEN iffD1]) |
50 |
||
51 |
(* Like 'Always_LeadsTo_post RS iffD2', but with premises in the good order *) |
|
61392 | 52 |
lemma Always_LeadsToD: "[| F \<in> Always(C); F \<in> A \<longmapsto>w A' |] ==> F \<in> A \<longmapsto>w (C \<inter> A')" |
15634 | 53 |
by (blast intro: Always_LeadsTo_post [THEN iffD2]) |
54 |
||
55 |
(*** Introduction rules \<in> Basis, Trans, Union ***) |
|
56 |
||
61392 | 57 |
lemma LeadsTo_Basis: "F \<in> A Ensures B ==> F \<in> A \<longmapsto>w B" |
15634 | 58 |
by (auto simp add: Ensures_def LeadsTo_def) |
59 |
||
60 |
lemma LeadsTo_Trans: |
|
61392 | 61 |
"[| F \<in> A \<longmapsto>w B; F \<in> B \<longmapsto>w C |] ==> F \<in> A \<longmapsto>w C" |
15634 | 62 |
apply (simp (no_asm_use) add: LeadsTo_def) |
63 |
apply (blast intro: leadsTo_Trans) |
|
64 |
done |
|
65 |
||
66 |
lemma LeadsTo_Union: |
|
61392 | 67 |
"[|(!!A. A \<in> S ==> F \<in> A \<longmapsto>w B); F \<in> program|]==>F \<in> \<Union>(S) \<longmapsto>w B" |
15634 | 68 |
apply (simp add: LeadsTo_def) |
69 |
apply (subst Int_Union_Union2) |
|
70 |
apply (rule leadsTo_UN, auto) |
|
71 |
done |
|
72 |
||
73 |
(*** Derived rules ***) |
|
74 |
||
61392 | 75 |
lemma leadsTo_imp_LeadsTo: "F \<in> A \<longmapsto> B ==> F \<in> A \<longmapsto>w B" |
15634 | 76 |
apply (frule leadsToD2, clarify) |
77 |
apply (simp (no_asm_simp) add: LeadsTo_eq) |
|
78 |
apply (blast intro: leadsTo_weaken_L) |
|
79 |
done |
|
80 |
||
81 |
(*Useful with cancellation, disjunction*) |
|
61392 | 82 |
lemma LeadsTo_Un_duplicate: "F \<in> A \<longmapsto>w (A' \<union> A') ==> F \<in> A \<longmapsto>w A'" |
15634 | 83 |
by (simp add: Un_ac) |
84 |
||
85 |
lemma LeadsTo_Un_duplicate2: |
|
61392 | 86 |
"F \<in> A \<longmapsto>w (A' \<union> C \<union> C) ==> F \<in> A \<longmapsto>w (A' \<union> C)" |
15634 | 87 |
by (simp add: Un_ac) |
88 |
||
89 |
lemma LeadsTo_UN: |
|
61392 | 90 |
"[|(!!i. i \<in> I ==> F \<in> A(i) \<longmapsto>w B); F \<in> program|] |
91 |
==>F:(\<Union>i \<in> I. A(i)) \<longmapsto>w B" |
|
15634 | 92 |
apply (simp add: LeadsTo_def) |
93 |
apply (simp (no_asm_simp) del: UN_simps add: Int_UN_distrib) |
|
94 |
apply (rule leadsTo_UN, auto) |
|
95 |
done |
|
96 |
||
97 |
(*Binary union introduction rule*) |
|
98 |
lemma LeadsTo_Un: |
|
61392 | 99 |
"[| F \<in> A \<longmapsto>w C; F \<in> B \<longmapsto>w C |] ==> F \<in> (A \<union> B) \<longmapsto>w C" |
15634 | 100 |
apply (subst Un_eq_Union) |
101 |
apply (rule LeadsTo_Union) |
|
102 |
apply (auto dest: LeadsTo_type [THEN subsetD]) |
|
103 |
done |
|
104 |
||
105 |
(*Lets us look at the starting state*) |
|
46953 | 106 |
lemma single_LeadsTo_I: |
61392 | 107 |
"[|(!!s. s \<in> A ==> F:{s} \<longmapsto>w B); F \<in> program|]==>F \<in> A \<longmapsto>w B" |
15634 | 108 |
apply (subst UN_singleton [symmetric], rule LeadsTo_UN, auto) |
109 |
done |
|
110 |
||
61392 | 111 |
lemma subset_imp_LeadsTo: "[| A \<subseteq> B; F \<in> program |] ==> F \<in> A \<longmapsto>w B" |
15634 | 112 |
apply (simp (no_asm_simp) add: LeadsTo_def) |
113 |
apply (blast intro: subset_imp_leadsTo) |
|
114 |
done |
|
115 |
||
61392 | 116 |
lemma empty_LeadsTo: "F \<in> 0 \<longmapsto>w A \<longleftrightarrow> F \<in> program" |
15634 | 117 |
by (auto dest: LeadsTo_type [THEN subsetD] |
118 |
intro: empty_subsetI [THEN subset_imp_LeadsTo]) |
|
119 |
declare empty_LeadsTo [iff] |
|
120 |
||
61392 | 121 |
lemma LeadsTo_state: "F \<in> A \<longmapsto>w state \<longleftrightarrow> F \<in> program" |
15634 | 122 |
by (auto dest: LeadsTo_type [THEN subsetD] simp add: LeadsTo_eq) |
123 |
declare LeadsTo_state [iff] |
|
124 |
||
61392 | 125 |
lemma LeadsTo_weaken_R: "[| F \<in> A \<longmapsto>w A'; A'<=B'|] ==> F \<in> A \<longmapsto>w B'" |
15634 | 126 |
apply (unfold LeadsTo_def) |
127 |
apply (auto intro: leadsTo_weaken_R) |
|
128 |
done |
|
129 |
||
61392 | 130 |
lemma LeadsTo_weaken_L: "[| F \<in> A \<longmapsto>w A'; B \<subseteq> A |] ==> F \<in> B \<longmapsto>w A'" |
15634 | 131 |
apply (unfold LeadsTo_def) |
132 |
apply (auto intro: leadsTo_weaken_L) |
|
133 |
done |
|
134 |
||
61392 | 135 |
lemma LeadsTo_weaken: "[| F \<in> A \<longmapsto>w A'; B<=A; A'<=B' |] ==> F \<in> B \<longmapsto>w B'" |
15634 | 136 |
by (blast intro: LeadsTo_weaken_R LeadsTo_weaken_L LeadsTo_Trans) |
137 |
||
46953 | 138 |
lemma Always_LeadsTo_weaken: |
61392 | 139 |
"[| F \<in> Always(C); F \<in> A \<longmapsto>w A'; C \<inter> B \<subseteq> A; C \<inter> A' \<subseteq> B' |] |
140 |
==> F \<in> B \<longmapsto>w B'" |
|
15634 | 141 |
apply (blast dest: Always_LeadsToI intro: LeadsTo_weaken Always_LeadsToD) |
142 |
done |
|
143 |
||
144 |
(** Two theorems for "proof lattices" **) |
|
145 |
||
61392 | 146 |
lemma LeadsTo_Un_post: "F \<in> A \<longmapsto>w B ==> F:(A \<union> B) \<longmapsto>w B" |
15634 | 147 |
by (blast dest: LeadsTo_type [THEN subsetD] |
148 |
intro: LeadsTo_Un subset_imp_LeadsTo) |
|
149 |
||
61392 | 150 |
lemma LeadsTo_Trans_Un: "[| F \<in> A \<longmapsto>w B; F \<in> B \<longmapsto>w C |] |
151 |
==> F \<in> (A \<union> B) \<longmapsto>w C" |
|
15634 | 152 |
apply (blast intro: LeadsTo_Un subset_imp_LeadsTo LeadsTo_weaken_L LeadsTo_Trans dest: LeadsTo_type [THEN subsetD]) |
153 |
done |
|
154 |
||
155 |
(** Distributive laws **) |
|
61392 | 156 |
lemma LeadsTo_Un_distrib: "(F \<in> (A \<union> B) \<longmapsto>w C) \<longleftrightarrow> (F \<in> A \<longmapsto>w C & F \<in> B \<longmapsto>w C)" |
15634 | 157 |
by (blast intro: LeadsTo_Un LeadsTo_weaken_L) |
158 |
||
61392 | 159 |
lemma LeadsTo_UN_distrib: "(F \<in> (\<Union>i \<in> I. A(i)) \<longmapsto>w B) \<longleftrightarrow> (\<forall>i \<in> I. F \<in> A(i) \<longmapsto>w B) & F \<in> program" |
15634 | 160 |
by (blast dest: LeadsTo_type [THEN subsetD] |
161 |
intro: LeadsTo_UN LeadsTo_weaken_L) |
|
162 |
||
61392 | 163 |
lemma LeadsTo_Union_distrib: "(F \<in> \<Union>(S) \<longmapsto>w B) \<longleftrightarrow> (\<forall>A \<in> S. F \<in> A \<longmapsto>w B) & F \<in> program" |
15634 | 164 |
by (blast dest: LeadsTo_type [THEN subsetD] |
165 |
intro: LeadsTo_Union LeadsTo_weaken_L) |
|
166 |
||
167 |
(** More rules using the premise "Always(I)" **) |
|
168 |
||
46823 | 169 |
lemma EnsuresI: "[| F:(A-B) Co (A \<union> B); F \<in> transient (A-B) |] ==> F \<in> A Ensures B" |
15634 | 170 |
apply (simp add: Ensures_def Constrains_eq_constrains) |
171 |
apply (blast intro: ensuresI constrains_weaken transient_strengthen dest: constrainsD2) |
|
172 |
done |
|
173 |
||
46953 | 174 |
lemma Always_LeadsTo_Basis: "[| F \<in> Always(I); F \<in> (I \<inter> (A-A')) Co (A \<union> A'); |
175 |
F \<in> transient (I \<inter> (A-A')) |] |
|
61392 | 176 |
==> F \<in> A \<longmapsto>w A'" |
15634 | 177 |
apply (rule Always_LeadsToI, assumption) |
178 |
apply (blast intro: EnsuresI LeadsTo_Basis Always_ConstrainsD [THEN Constrains_weaken] transient_strengthen) |
|
179 |
done |
|
180 |
||
181 |
(*Set difference: maybe combine with leadsTo_weaken_L?? |
|
182 |
This is the most useful form of the "disjunction" rule*) |
|
183 |
lemma LeadsTo_Diff: |
|
61392 | 184 |
"[| F \<in> (A-B) \<longmapsto>w C; F \<in> (A \<inter> B) \<longmapsto>w C |] ==> F \<in> A \<longmapsto>w C" |
15634 | 185 |
by (blast intro: LeadsTo_Un LeadsTo_weaken) |
186 |
||
46953 | 187 |
lemma LeadsTo_UN_UN: |
61392 | 188 |
"[|(!!i. i \<in> I ==> F \<in> A(i) \<longmapsto>w A'(i)); F \<in> program |] |
189 |
==> F \<in> (\<Union>i \<in> I. A(i)) \<longmapsto>w (\<Union>i \<in> I. A'(i))" |
|
46953 | 190 |
apply (rule LeadsTo_Union, auto) |
15634 | 191 |
apply (blast intro: LeadsTo_weaken_R) |
192 |
done |
|
193 |
||
194 |
(*Binary union version*) |
|
195 |
lemma LeadsTo_Un_Un: |
|
61392 | 196 |
"[| F \<in> A \<longmapsto>w A'; F \<in> B \<longmapsto>w B' |] ==> F:(A \<union> B) \<longmapsto>w (A' \<union> B')" |
15634 | 197 |
by (blast intro: LeadsTo_Un LeadsTo_weaken_R) |
198 |
||
199 |
(** The cancellation law **) |
|
200 |
||
61392 | 201 |
lemma LeadsTo_cancel2: "[| F \<in> A \<longmapsto>w(A' \<union> B); F \<in> B \<longmapsto>w B' |] ==> F \<in> A \<longmapsto>w (A' \<union> B')" |
15634 | 202 |
by (blast intro: LeadsTo_Un_Un subset_imp_LeadsTo LeadsTo_Trans dest: LeadsTo_type [THEN subsetD]) |
203 |
||
46823 | 204 |
lemma Un_Diff: "A \<union> (B - A) = A \<union> B" |
15634 | 205 |
by auto |
206 |
||
61392 | 207 |
lemma LeadsTo_cancel_Diff2: "[| F \<in> A \<longmapsto>w (A' \<union> B); F \<in> (B-A') \<longmapsto>w B' |] ==> F \<in> A \<longmapsto>w (A' \<union> B')" |
15634 | 208 |
apply (rule LeadsTo_cancel2) |
209 |
prefer 2 apply assumption |
|
210 |
apply (simp (no_asm_simp) add: Un_Diff) |
|
211 |
done |
|
212 |
||
61392 | 213 |
lemma LeadsTo_cancel1: "[| F \<in> A \<longmapsto>w (B \<union> A'); F \<in> B \<longmapsto>w B' |] ==> F \<in> A \<longmapsto>w (B' \<union> A')" |
15634 | 214 |
apply (simp add: Un_commute) |
215 |
apply (blast intro!: LeadsTo_cancel2) |
|
216 |
done |
|
217 |
||
46823 | 218 |
lemma Diff_Un2: "(B - A) \<union> A = B \<union> A" |
15634 | 219 |
by auto |
220 |
||
61392 | 221 |
lemma LeadsTo_cancel_Diff1: "[| F \<in> A \<longmapsto>w (B \<union> A'); F \<in> (B-A') \<longmapsto>w B' |] ==> F \<in> A \<longmapsto>w (B' \<union> A')" |
15634 | 222 |
apply (rule LeadsTo_cancel1) |
223 |
prefer 2 apply assumption |
|
224 |
apply (simp (no_asm_simp) add: Diff_Un2) |
|
225 |
done |
|
226 |
||
227 |
(** The impossibility law **) |
|
228 |
||
229 |
(*The set "A" may be non-empty, but it contains no reachable states*) |
|
61392 | 230 |
lemma LeadsTo_empty: "F \<in> A \<longmapsto>w 0 ==> F \<in> Always (state -A)" |
15634 | 231 |
apply (simp (no_asm_use) add: LeadsTo_def Always_eq_includes_reachable) |
232 |
apply (cut_tac reachable_type) |
|
233 |
apply (auto dest!: leadsTo_empty) |
|
234 |
done |
|
235 |
||
236 |
(** PSP \<in> Progress-Safety-Progress **) |
|
237 |
||
238 |
(*Special case of PSP \<in> Misra's "stable conjunction"*) |
|
61392 | 239 |
lemma PSP_Stable: "[| F \<in> A \<longmapsto>w A'; F \<in> Stable(B) |]==> F:(A \<inter> B) \<longmapsto>w (A' \<inter> B)" |
15634 | 240 |
apply (simp add: LeadsTo_def Stable_eq_stable, clarify) |
241 |
apply (drule psp_stable, assumption) |
|
242 |
apply (simp add: Int_ac) |
|
243 |
done |
|
244 |
||
61392 | 245 |
lemma PSP_Stable2: "[| F \<in> A \<longmapsto>w A'; F \<in> Stable(B) |] ==> F \<in> (B \<inter> A) \<longmapsto>w (B \<inter> A')" |
15634 | 246 |
apply (simp (no_asm_simp) add: PSP_Stable Int_ac) |
247 |
done |
|
248 |
||
61392 | 249 |
lemma PSP: "[| F \<in> A \<longmapsto>w A'; F \<in> B Co B'|]==> F \<in> (A \<inter> B') \<longmapsto>w ((A' \<inter> B) \<union> (B' - B))" |
15634 | 250 |
apply (simp (no_asm_use) add: LeadsTo_def Constrains_eq_constrains) |
251 |
apply (blast dest: psp intro: leadsTo_weaken) |
|
252 |
done |
|
253 |
||
61392 | 254 |
lemma PSP2: "[| F \<in> A \<longmapsto>w A'; F \<in> B Co B' |]==> F:(B' \<inter> A) \<longmapsto>w ((B \<inter> A') \<union> (B' - B))" |
15634 | 255 |
by (simp (no_asm_simp) add: PSP Int_ac) |
256 |
||
46953 | 257 |
lemma PSP_Unless: |
61392 | 258 |
"[| F \<in> A \<longmapsto>w A'; F \<in> B Unless B'|]==> F:(A \<inter> B) \<longmapsto>w ((A' \<inter> B) \<union> B')" |
24893 | 259 |
apply (unfold op_Unless_def) |
15634 | 260 |
apply (drule PSP, assumption) |
261 |
apply (blast intro: LeadsTo_Diff LeadsTo_weaken subset_imp_LeadsTo) |
|
262 |
done |
|
263 |
||
264 |
(*** Induction rules ***) |
|
265 |
||
266 |
(** Meta or object quantifier ????? **) |
|
46953 | 267 |
lemma LeadsTo_wf_induct: "[| wf(r); |
61392 | 268 |
\<forall>m \<in> I. F \<in> (A \<inter> f-``{m}) \<longmapsto>w |
46953 | 269 |
((A \<inter> f-``(converse(r) `` {m})) \<union> B); |
270 |
field(r)<=I; A<=f-``I; F \<in> program |] |
|
61392 | 271 |
==> F \<in> A \<longmapsto>w B" |
15634 | 272 |
apply (simp (no_asm_use) add: LeadsTo_def) |
273 |
apply auto |
|
274 |
apply (erule_tac I = I and f = f in leadsTo_wf_induct, safe) |
|
275 |
apply (drule_tac [2] x = m in bspec, safe) |
|
46823 | 276 |
apply (rule_tac [2] A' = "reachable (F) \<inter> (A \<inter> f -`` (converse (r) ``{m}) \<union> B) " in leadsTo_weaken_R) |
46953 | 277 |
apply (auto simp add: Int_assoc) |
15634 | 278 |
done |
279 |
||
280 |
||
61392 | 281 |
lemma LessThan_induct: "[| \<forall>m \<in> nat. F:(A \<inter> f-``{m}) \<longmapsto>w ((A \<inter> f-``m) \<union> B); |
282 |
A<=f-``nat; F \<in> program |] ==> F \<in> A \<longmapsto>w B" |
|
15634 | 283 |
apply (rule_tac A1 = nat and f1 = "%x. x" in wf_measure [THEN LeadsTo_wf_induct]) |
284 |
apply (simp_all add: nat_measure_field) |
|
285 |
apply (simp add: ltI Image_inverse_lessThan vimage_def [symmetric]) |
|
286 |
done |
|
287 |
||
288 |
||
46953 | 289 |
(****** |
15634 | 290 |
To be ported ??? I am not sure. |
291 |
||
292 |
integ_0_le_induct |
|
293 |
LessThan_bounded_induct |
|
294 |
GreaterThan_bounded_induct |
|
295 |
||
296 |
*****) |
|
297 |
||
298 |
(*** Completion \<in> Binary and General Finite versions ***) |
|
299 |
||
61392 | 300 |
lemma Completion: "[| F \<in> A \<longmapsto>w (A' \<union> C); F \<in> A' Co (A' \<union> C); |
301 |
F \<in> B \<longmapsto>w (B' \<union> C); F \<in> B' Co (B' \<union> C) |] |
|
302 |
==> F \<in> (A \<inter> B) \<longmapsto>w ((A' \<inter> B') \<union> C)" |
|
15634 | 303 |
apply (simp (no_asm_use) add: LeadsTo_def Constrains_eq_constrains Int_Un_distrib) |
304 |
apply (blast intro: completion leadsTo_weaken) |
|
305 |
done |
|
306 |
||
307 |
lemma Finite_completion_aux: |
|
46953 | 308 |
"[| I \<in> Fin(X);F \<in> program |] |
61392 | 309 |
==> (\<forall>i \<in> I. F \<in> (A(i)) \<longmapsto>w (A'(i) \<union> C)) \<longrightarrow> |
46953 | 310 |
(\<forall>i \<in> I. F \<in> (A'(i)) Co (A'(i) \<union> C)) \<longrightarrow> |
61392 | 311 |
F \<in> (\<Inter>i \<in> I. A(i)) \<longmapsto>w ((\<Inter>i \<in> I. A'(i)) \<union> C)" |
15634 | 312 |
apply (erule Fin_induct) |
313 |
apply (auto simp del: INT_simps simp add: Inter_0) |
|
46953 | 314 |
apply (rule Completion, auto) |
15634 | 315 |
apply (simp del: INT_simps add: INT_extend_simps) |
316 |
apply (blast intro: Constrains_INT) |
|
317 |
done |
|
318 |
||
46953 | 319 |
lemma Finite_completion: |
61392 | 320 |
"[| I \<in> Fin(X); !!i. i \<in> I ==> F \<in> A(i) \<longmapsto>w (A'(i) \<union> C); |
46953 | 321 |
!!i. i \<in> I ==> F \<in> A'(i) Co (A'(i) \<union> C); |
322 |
F \<in> program |] |
|
61392 | 323 |
==> F \<in> (\<Inter>i \<in> I. A(i)) \<longmapsto>w ((\<Inter>i \<in> I. A'(i)) \<union> C)" |
15634 | 324 |
by (blast intro: Finite_completion_aux [THEN mp, THEN mp]) |
325 |
||
46953 | 326 |
lemma Stable_completion: |
61392 | 327 |
"[| F \<in> A \<longmapsto>w A'; F \<in> Stable(A'); |
328 |
F \<in> B \<longmapsto>w B'; F \<in> Stable(B') |] |
|
329 |
==> F \<in> (A \<inter> B) \<longmapsto>w (A' \<inter> B')" |
|
15634 | 330 |
apply (unfold Stable_def) |
331 |
apply (rule_tac C1 = 0 in Completion [THEN LeadsTo_weaken_R]) |
|
332 |
prefer 5 |
|
46953 | 333 |
apply blast |
334 |
apply auto |
|
15634 | 335 |
done |
336 |
||
46953 | 337 |
lemma Finite_stable_completion: |
338 |
"[| I \<in> Fin(X); |
|
61392 | 339 |
(!!i. i \<in> I ==> F \<in> A(i) \<longmapsto>w A'(i)); |
46953 | 340 |
(!!i. i \<in> I ==>F \<in> Stable(A'(i))); F \<in> program |] |
61392 | 341 |
==> F \<in> (\<Inter>i \<in> I. A(i)) \<longmapsto>w (\<Inter>i \<in> I. A'(i))" |
15634 | 342 |
apply (unfold Stable_def) |
343 |
apply (rule_tac C1 = 0 in Finite_completion [THEN LeadsTo_weaken_R], simp_all) |
|
46953 | 344 |
apply (rule_tac [3] subset_refl, auto) |
15634 | 345 |
done |
346 |
||
60770 | 347 |
ML \<open> |
15634 | 348 |
(*proves "ensures/leadsTo" properties when the program is specified*) |
23894
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
18371
diff
changeset
|
349 |
fun ensures_tac ctxt sact = |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46953
diff
changeset
|
350 |
SELECT_GOAL |
58963
26bf09b95dda
proper context for assume_tac (atac remains as fall-back without context);
wenzelm
parents:
58871
diff
changeset
|
351 |
(EVERY [REPEAT (Always_Int_tac ctxt 1), |
60754 | 352 |
eresolve_tac ctxt @{thms Always_LeadsTo_Basis} 1 |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46953
diff
changeset
|
353 |
ORELSE (*subgoal may involve LeadsTo, leadsTo or ensures*) |
60774 | 354 |
REPEAT (ares_tac ctxt [@{thm LeadsTo_Basis}, @{thm leadsTo_Basis}, |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46953
diff
changeset
|
355 |
@{thm EnsuresI}, @{thm ensuresI}] 1), |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46953
diff
changeset
|
356 |
(*now there are two subgoals: co & transient*) |
57945
cacb00a569e0
prefer 'named_theorems' over Named_Thms, with subtle change of semantics due to visual order vs. internal reverse order;
wenzelm
parents:
55111
diff
changeset
|
357 |
simp_tac (ctxt addsimps (Named_Theorems.get ctxt @{named_theorems program})) 2, |
59780 | 358 |
Rule_Insts.res_inst_tac ctxt |
359 |
[((("act", 0), Position.none), sact)] [] @{thm transientI} 2, |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46953
diff
changeset
|
360 |
(*simplify the command's domain*) |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46953
diff
changeset
|
361 |
simp_tac (ctxt addsimps [@{thm domain_def}]) 3, |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46953
diff
changeset
|
362 |
(* proving the domain part *) |
60754 | 363 |
clarify_tac ctxt 3, |
364 |
dresolve_tac ctxt @{thms swap} 3, force_tac ctxt 4, |
|
365 |
resolve_tac ctxt @{thms ReplaceI} 3, force_tac ctxt 3, force_tac ctxt 4, |
|
366 |
asm_full_simp_tac ctxt 3, resolve_tac ctxt @{thms conjI} 3, simp_tac ctxt 4, |
|
367 |
REPEAT (resolve_tac ctxt @{thms state_update_type} 3), |
|
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46953
diff
changeset
|
368 |
constrains_tac ctxt 1, |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46953
diff
changeset
|
369 |
ALLGOALS (clarify_tac ctxt), |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46953
diff
changeset
|
370 |
ALLGOALS (asm_full_simp_tac (ctxt addsimps [@{thm st_set_def}])), |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46953
diff
changeset
|
371 |
ALLGOALS (clarify_tac ctxt), |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
46953
diff
changeset
|
372 |
ALLGOALS (asm_lr_simp_tac ctxt)]); |
60770 | 373 |
\<close> |
15634 | 374 |
|
60770 | 375 |
method_setup ensures = \<open> |
63120
629a4c5e953e
embedded content may be delimited via cartouches;
wenzelm
parents:
61392
diff
changeset
|
376 |
Args.goal_spec -- Scan.lift Args.embedded_inner_syntax >> |
30549 | 377 |
(fn (quant, s) => fn ctxt => SIMPLE_METHOD'' quant (ensures_tac ctxt s)) |
60770 | 378 |
\<close> "for proving progress properties" |
15634 | 379 |
|
11479 | 380 |
end |