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