author  wenzelm 
Wed, 27 Mar 2013 16:38:25 +0100  
changeset 51553  63327f679cff 
parent 46953  2b6e55924af3 
child 51717  9e7d1c139569 
permissions  rwrr 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
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 

15634  8 
header{*Weak LeadsTo relation (restricted to the set of reachable states)*} 
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 
20 
LeadsTo :: "[i, i] => i" (infixl "LeadsTo" 60) where 

46953  21 
"A LeadsTo B == {F \<in> program. F:(reachable(F) \<inter> A) leadsTo (reachable(F) \<inter> 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 HOLlike definition *) 

46953  31 
lemma LeadsTo_eq: 
46823  32 
"st_set(B)==> A LeadsTo B = {F \<in> program. F:(reachable(F) \<inter> A) leadsTo B}" 
15634  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 **) 

46823  43 
lemma Always_LeadsTo_pre: "F \<in> Always(I) ==> (F:(I \<inter> A) LeadsTo A') \<longleftrightarrow> (F \<in> A LeadsTo A')" 
15634  44 
by (simp add: LeadsTo_def Always_eq_includes_reachable Int_absorb2 Int_assoc [symmetric] leadsToD2) 
45 

46823  46 
lemma Always_LeadsTo_post: "F \<in> Always(I) ==> (F \<in> A LeadsTo (I \<inter> A')) \<longleftrightarrow> (F \<in> A LeadsTo A')" 
15634  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 *) 

46823  52 
lemma Always_LeadsToI: "[ F \<in> Always(C); F \<in> (C \<inter> A) LeadsTo A' ] ==> F \<in> A LeadsTo A'" 
15634  53 
by (blast intro: Always_LeadsTo_pre [THEN iffD1]) 
54 

55 
(* Like 'Always_LeadsTo_post RS iffD2', but with premises in the good order *) 

46823  56 
lemma Always_LeadsToD: "[ F \<in> Always(C); F \<in> A LeadsTo A' ] ==> F \<in> A LeadsTo (C \<inter> A')" 
15634  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: 

46823  71 
"[(!!A. A \<in> S ==> F \<in> A LeadsTo B); F \<in> program]==>F \<in> \<Union>(S) LeadsTo B" 
15634  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*) 

46823  86 
lemma LeadsTo_Un_duplicate: "F \<in> A LeadsTo (A' \<union> A') ==> F \<in> A LeadsTo A'" 
15634  87 
by (simp add: Un_ac) 
88 

89 
lemma LeadsTo_Un_duplicate2: 

46823  90 
"F \<in> A LeadsTo (A' \<union> C \<union> C) ==> F \<in> A LeadsTo (A' \<union> C)" 
15634  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: 

46823  103 
"[ F \<in> A LeadsTo C; F \<in> B LeadsTo C ] ==> F \<in> (A \<union> B) LeadsTo C" 
15634  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*) 

46953  110 
lemma single_LeadsTo_I: 
15634  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 

46823  115 
lemma subset_imp_LeadsTo: "[ A \<subseteq> B; F \<in> program ] ==> F \<in> A LeadsTo B" 
15634  116 
apply (simp (no_asm_simp) add: LeadsTo_def) 
117 
apply (blast intro: subset_imp_leadsTo) 

118 
done 

119 

46953  120 
lemma empty_LeadsTo: "F \<in> 0 LeadsTo A \<longleftrightarrow> F \<in> program" 
15634  121 
by (auto dest: LeadsTo_type [THEN subsetD] 
122 
intro: empty_subsetI [THEN subset_imp_LeadsTo]) 

123 
declare empty_LeadsTo [iff] 

124 

46823  125 
lemma LeadsTo_state: "F \<in> A LeadsTo state \<longleftrightarrow> F \<in> program" 
15634  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 

46823  134 
lemma LeadsTo_weaken_L: "[ F \<in> A LeadsTo A'; B \<subseteq> A ] ==> F \<in> B LeadsTo A'" 
15634  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 

46953  142 
lemma Always_LeadsTo_weaken: 
143 
"[ F \<in> Always(C); F \<in> A LeadsTo A'; C \<inter> B \<subseteq> A; C \<inter> A' \<subseteq> B' ] 

15634  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 

46823  150 
lemma LeadsTo_Un_post: "F \<in> A LeadsTo B ==> F:(A \<union> B) LeadsTo B" 
15634  151 
by (blast dest: LeadsTo_type [THEN subsetD] 
152 
intro: LeadsTo_Un subset_imp_LeadsTo) 

153 

46953  154 
lemma LeadsTo_Trans_Un: "[ F \<in> A LeadsTo B; F \<in> B LeadsTo C ] 
46823  155 
==> F \<in> (A \<union> B) LeadsTo C" 
15634  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 **) 

46823  160 
lemma LeadsTo_Un_distrib: "(F \<in> (A \<union> B) LeadsTo C) \<longleftrightarrow> (F \<in> A LeadsTo C & F \<in> B LeadsTo C)" 
15634  161 
by (blast intro: LeadsTo_Un LeadsTo_weaken_L) 
162 

46823  163 
lemma LeadsTo_UN_distrib: "(F \<in> (\<Union>i \<in> I. A(i)) LeadsTo B) \<longleftrightarrow> (\<forall>i \<in> I. F \<in> A(i) LeadsTo B) & F \<in> program" 
15634  164 
by (blast dest: LeadsTo_type [THEN subsetD] 
165 
intro: LeadsTo_UN LeadsTo_weaken_L) 

166 

46823  167 
lemma LeadsTo_Union_distrib: "(F \<in> \<Union>(S) LeadsTo B) \<longleftrightarrow> (\<forall>A \<in> S. F \<in> A LeadsTo B) & F \<in> program" 
15634  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 

46823  173 
lemma EnsuresI: "[ F:(AB) Co (A \<union> B); F \<in> transient (AB) ] ==> F \<in> A Ensures B" 
15634  174 
apply (simp add: Ensures_def Constrains_eq_constrains) 
175 
apply (blast intro: ensuresI constrains_weaken transient_strengthen dest: constrainsD2) 

176 
done 

177 

46953  178 
lemma Always_LeadsTo_Basis: "[ F \<in> Always(I); F \<in> (I \<inter> (AA')) Co (A \<union> A'); 
179 
F \<in> transient (I \<inter> (AA')) ] 

15634  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: 

46823  188 
"[ F \<in> (AB) LeadsTo C; F \<in> (A \<inter> B) LeadsTo C ] ==> F \<in> A LeadsTo C" 
15634  189 
by (blast intro: LeadsTo_Un LeadsTo_weaken) 
190 

46953  191 
lemma LeadsTo_UN_UN: 
192 
"[(!!i. i \<in> I ==> F \<in> A(i) LeadsTo A'(i)); F \<in> program ] 

15634  193 
==> F \<in> (\<Union>i \<in> I. A(i)) LeadsTo (\<Union>i \<in> I. A'(i))" 
46953  194 
apply (rule LeadsTo_Union, auto) 
15634  195 
apply (blast intro: LeadsTo_weaken_R) 
196 
done 

197 

198 
(*Binary union version*) 

199 
lemma LeadsTo_Un_Un: 

46823  200 
"[ F \<in> A LeadsTo A'; F \<in> B LeadsTo B' ] ==> F:(A \<union> B) LeadsTo (A' \<union> B')" 
15634  201 
by (blast intro: LeadsTo_Un LeadsTo_weaken_R) 
202 

203 
(** The cancellation law **) 

204 

46823  205 
lemma LeadsTo_cancel2: "[ F \<in> A LeadsTo(A' \<union> B); F \<in> B LeadsTo B' ] ==> F \<in> A LeadsTo (A' \<union> B')" 
15634  206 
by (blast intro: LeadsTo_Un_Un subset_imp_LeadsTo LeadsTo_Trans dest: LeadsTo_type [THEN subsetD]) 
207 

46823  208 
lemma Un_Diff: "A \<union> (B  A) = A \<union> B" 
15634  209 
by auto 
210 

46823  211 
lemma LeadsTo_cancel_Diff2: "[ F \<in> A LeadsTo (A' \<union> B); F \<in> (BA') LeadsTo B' ] ==> F \<in> A LeadsTo (A' \<union> B')" 
15634  212 
apply (rule LeadsTo_cancel2) 
213 
prefer 2 apply assumption 

214 
apply (simp (no_asm_simp) add: Un_Diff) 

215 
done 

216 

46823  217 
lemma LeadsTo_cancel1: "[ F \<in> A LeadsTo (B \<union> A'); F \<in> B LeadsTo B' ] ==> F \<in> A LeadsTo (B' \<union> A')" 
15634  218 
apply (simp add: Un_commute) 
219 
apply (blast intro!: LeadsTo_cancel2) 

220 
done 

221 

46823  222 
lemma Diff_Un2: "(B  A) \<union> A = B \<union> A" 
15634  223 
by auto 
224 

46823  225 
lemma LeadsTo_cancel_Diff1: "[ F \<in> A LeadsTo (B \<union> A'); F \<in> (BA') LeadsTo B' ] ==> F \<in> A LeadsTo (B' \<union> A')" 
15634  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 nonempty, 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> ProgressSafetyProgress **) 

241 

242 
(*Special case of PSP \<in> Misra's "stable conjunction"*) 

46823  243 
lemma PSP_Stable: "[ F \<in> A LeadsTo A'; F \<in> Stable(B) ]==> F:(A \<inter> B) LeadsTo (A' \<inter> B)" 
15634  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 

46823  249 
lemma PSP_Stable2: "[ F \<in> A LeadsTo A'; F \<in> Stable(B) ] ==> F \<in> (B \<inter> A) LeadsTo (B \<inter> A')" 
15634  250 
apply (simp (no_asm_simp) add: PSP_Stable Int_ac) 
251 
done 

252 

46823  253 
lemma PSP: "[ F \<in> A LeadsTo A'; F \<in> B Co B']==> F \<in> (A \<inter> B') LeadsTo ((A' \<inter> B) \<union> (B'  B))" 
15634  254 
apply (simp (no_asm_use) add: LeadsTo_def Constrains_eq_constrains) 
255 
apply (blast dest: psp intro: leadsTo_weaken) 

256 
done 

257 

46823  258 
lemma PSP2: "[ F \<in> A LeadsTo A'; F \<in> B Co B' ]==> F:(B' \<inter> A) LeadsTo ((B \<inter> A') \<union> (B'  B))" 
15634  259 
by (simp (no_asm_simp) add: PSP Int_ac) 
260 

46953  261 
lemma PSP_Unless: 
46823  262 
"[ F \<in> A LeadsTo A'; F \<in> B Unless B']==> F:(A \<inter> B) LeadsTo ((A' \<inter> B) \<union> 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 ????? **) 

46953  271 
lemma LeadsTo_wf_induct: "[ wf(r); 
272 
\<forall>m \<in> I. F \<in> (A \<inter> f``{m}) LeadsTo 

273 
((A \<inter> f``(converse(r) `` {m})) \<union> B); 

274 
field(r)<=I; A<=f``I; F \<in> program ] 

15634  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) 

46823  280 
apply (rule_tac [2] A' = "reachable (F) \<inter> (A \<inter> f `` (converse (r) ``{m}) \<union> B) " in leadsTo_weaken_R) 
46953  281 
apply (auto simp add: Int_assoc) 
15634  282 
done 
283 

284 

46953  285 
lemma LessThan_induct: "[ \<forall>m \<in> nat. F:(A \<inter> f``{m}) LeadsTo ((A \<inter> f``m) \<union> B); 
15634  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 

46953  293 
(****** 
15634  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 

46953  304 
lemma Completion: "[ F \<in> A LeadsTo (A' \<union> C); F \<in> A' Co (A' \<union> C); 
305 
F \<in> B LeadsTo (B' \<union> C); F \<in> B' Co (B' \<union> C) ] 

46823  306 
==> F \<in> (A \<inter> B) LeadsTo ((A' \<inter> B') \<union> C)" 
15634  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: 

46953  312 
"[ I \<in> Fin(X);F \<in> program ] 
313 
==> (\<forall>i \<in> I. F \<in> (A(i)) LeadsTo (A'(i) \<union> C)) \<longrightarrow> 

314 
(\<forall>i \<in> I. F \<in> (A'(i)) Co (A'(i) \<union> C)) \<longrightarrow> 

46823  315 
F \<in> (\<Inter>i \<in> I. A(i)) LeadsTo ((\<Inter>i \<in> I. A'(i)) \<union> C)" 
15634  316 
apply (erule Fin_induct) 
317 
apply (auto simp del: INT_simps simp add: Inter_0) 

46953  318 
apply (rule Completion, auto) 
15634  319 
apply (simp del: INT_simps add: INT_extend_simps) 
320 
apply (blast intro: Constrains_INT) 

321 
done 

322 

46953  323 
lemma Finite_completion: 
324 
"[ I \<in> Fin(X); !!i. i \<in> I ==> F \<in> A(i) LeadsTo (A'(i) \<union> C); 

325 
!!i. i \<in> I ==> F \<in> A'(i) Co (A'(i) \<union> C); 

326 
F \<in> program ] 

46823  327 
==> F \<in> (\<Inter>i \<in> I. A(i)) LeadsTo ((\<Inter>i \<in> I. A'(i)) \<union> C)" 
15634  328 
by (blast intro: Finite_completion_aux [THEN mp, THEN mp]) 
329 

46953  330 
lemma Stable_completion: 
331 
"[ F \<in> A LeadsTo A'; F \<in> Stable(A'); 

332 
F \<in> B LeadsTo B'; F \<in> Stable(B') ] 

46823  333 
==> F \<in> (A \<inter> B) LeadsTo (A' \<inter> B')" 
15634  334 
apply (unfold Stable_def) 
335 
apply (rule_tac C1 = 0 in Completion [THEN LeadsTo_weaken_R]) 

336 
prefer 5 

46953  337 
apply blast 
338 
apply auto 

15634  339 
done 
340 

46953  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 ] 

15634  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) 

46953  348 
apply (rule_tac [3] subset_refl, auto) 
15634  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 = 
42793  354 
let val ss = simpset_of ctxt in 
15634  355 
SELECT_GOAL 
356 
(EVERY [REPEAT (Always_Int_tac 1), 

46953  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*) 
31902  362 
simp_tac (ss addsimps (Program_Defs.get ctxt)) 2, 
27239  363 
res_inst_tac ctxt [(("act", 0), sact)] @{thm transientI} 2, 
15634  364 
(*simplify the command's domain*) 
46953  365 
simp_tac (ss addsimps [@{thm domain_def}]) 3, 
15634  366 
(* proving the domain part *) 
42793  367 
clarify_tac ctxt 3, dtac @{thm swap} 3, force_tac ctxt 4, 
368 
rtac @{thm ReplaceI} 3, force_tac ctxt 3, force_tac ctxt 4, 

35409  369 
asm_full_simp_tac ss 3, rtac @{thm 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, 
42793  372 
ALLGOALS (clarify_tac ctxt), 
24893  373 
ALLGOALS (asm_full_simp_tac (ss addsimps [@{thm st_set_def}])), 
42793  374 
ALLGOALS (clarify_tac ctxt), 
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 

42814  379 
method_setup ensures = {* 
30549  380 
Args.goal_spec  Scan.lift Args.name_source >> 
381 
(fn (quant, s) => fn ctxt => SIMPLE_METHOD'' quant (ensures_tac ctxt s)) 

382 
*} "for proving progress properties" 

15634  383 

11479  384 
end 