author  wenzelm 
Wed, 27 Mar 2013 16:38:25 +0100  
changeset 51553  63327f679cff 
parent 46823  57bf0cecb366 
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/Constrains.thy 
11479  2 
Author: Sidi O Ehmety, Computer Laboratory 
3 
Copyright 2001 University of Cambridge 

4 
*) 

5 

15634  6 
header{*Weak Safety Properties*} 
7 

8 
theory Constrains 

9 
imports UNITY 

24893  10 
begin 
15634  11 

11479  12 
consts traces :: "[i, i] => i" 
13 
(* Initial states and program => (final state, reversed trace to it)... 

12195  14 
the domain may also be state*list(state) *) 
11479  15 
inductive 
16 
domains 

17 
"traces(init, acts)" <= 

46823  18 
"(init \<union> (\<Union>act\<in>acts. field(act)))*list(\<Union>act\<in>acts. field(act))" 
15634  19 
intros 
11479  20 
(*Initial trace is empty*) 
46823  21 
Init: "s: init ==> <s,[]> \<in> traces(init,acts)" 
11479  22 

46823  23 
Acts: "[ act:acts; <s,evs> \<in> traces(init,acts); <s,s'>: act ] 
24 
==> <s', Cons(s,evs)> \<in> traces(init, acts)" 

11479  25 

15634  26 
type_intros list.intros UnI1 UnI2 UN_I fieldI2 fieldI1 
11479  27 

28 

15634  29 
consts reachable :: "i=>i" 
11479  30 
inductive 
31 
domains 

46823  32 
"reachable(F)" \<subseteq> "Init(F) \<union> (\<Union>act\<in>Acts(F). field(act))" 
15634  33 
intros 
34 
Init: "s:Init(F) ==> s:reachable(F)" 

11479  35 

15634  36 
Acts: "[ act: Acts(F); s:reachable(F); <s,s'>: act ] 
11479  37 
==> s':reachable(F)" 
38 

15634  39 
type_intros UnI1 UnI2 fieldI2 UN_I 
11479  40 

41 

24893  42 
definition 
43 
Constrains :: "[i,i] => i" (infixl "Co" 60) where 

46823  44 
"A Co B == {F:program. F:(reachable(F) \<inter> A) co B}" 
11479  45 

24893  46 
definition 
47 
op_Unless :: "[i, i] => i" (infixl "Unless" 60) where 

46823  48 
"A Unless B == (AB) Co (A \<union> B)" 
11479  49 

24893  50 
definition 
51 
Stable :: "i => i" where 

52 
"Stable(A) == A Co A" 

11479  53 

24893  54 
definition 
11479  55 
(*Always is the weak form of "invariant"*) 
24893  56 
Always :: "i => i" where 
46823  57 
"Always(A) == initially(A) \<inter> Stable(A)" 
11479  58 

15634  59 

60 
(*** traces and reachable ***) 

61 

46823  62 
lemma reachable_type: "reachable(F) \<subseteq> state" 
15634  63 
apply (cut_tac F = F in Init_type) 
64 
apply (cut_tac F = F in Acts_type) 

65 
apply (cut_tac F = F in reachable.dom_subset, blast) 

66 
done 

67 

68 
lemma st_set_reachable: "st_set(reachable(F))" 

69 
apply (unfold st_set_def) 

70 
apply (rule reachable_type) 

71 
done 

72 
declare st_set_reachable [iff] 

73 

46823  74 
lemma reachable_Int_state: "reachable(F) \<inter> state = reachable(F)" 
15634  75 
by (cut_tac reachable_type, auto) 
76 
declare reachable_Int_state [iff] 

77 

46823  78 
lemma state_Int_reachable: "state \<inter> reachable(F) = reachable(F)" 
15634  79 
by (cut_tac reachable_type, auto) 
80 
declare state_Int_reachable [iff] 

81 

82 
lemma reachable_equiv_traces: 

83 
"F \<in> program ==> reachable(F)={s \<in> state. \<exists>evs. <s,evs>:traces(Init(F), Acts(F))}" 

84 
apply (rule equalityI, safe) 

85 
apply (blast dest: reachable_type [THEN subsetD]) 

86 
apply (erule_tac [2] traces.induct) 

87 
apply (erule reachable.induct) 

88 
apply (blast intro: reachable.intros traces.intros)+ 

89 
done 

90 

46823  91 
lemma Init_into_reachable: "Init(F) \<subseteq> reachable(F)" 
15634  92 
by (blast intro: reachable.intros) 
93 

94 
lemma stable_reachable: "[ F \<in> program; G \<in> program; 

46823  95 
Acts(G) \<subseteq> Acts(F) ] ==> G \<in> stable(reachable(F))" 
15634  96 
apply (blast intro: stableI constrainsI st_setI 
97 
reachable_type [THEN subsetD] reachable.intros) 

98 
done 

99 

100 
declare stable_reachable [intro!] 

101 
declare stable_reachable [simp] 

102 

103 
(*The set of all reachable states is an invariant...*) 

104 
lemma invariant_reachable: 

105 
"F \<in> program ==> F \<in> invariant(reachable(F))" 

106 
apply (unfold invariant_def initially_def) 

107 
apply (blast intro: reachable_type [THEN subsetD] reachable.intros) 

108 
done 

109 

110 
(*...in fact the strongest invariant!*) 

46823  111 
lemma invariant_includes_reachable: "F \<in> invariant(A) ==> reachable(F) \<subseteq> A" 
15634  112 
apply (cut_tac F = F in Acts_type) 
113 
apply (cut_tac F = F in Init_type) 

114 
apply (cut_tac F = F in reachable_type) 

115 
apply (simp (no_asm_use) add: stable_def constrains_def invariant_def initially_def) 

116 
apply (rule subsetI) 

117 
apply (erule reachable.induct) 

118 
apply (blast intro: reachable.intros)+ 

119 
done 

120 

121 
(*** Co ***) 

122 

46823  123 
lemma constrains_reachable_Int: "F \<in> B co B'==>F:(reachable(F) \<inter> B) co (reachable(F) \<inter> B')" 
15634  124 
apply (frule constrains_type [THEN subsetD]) 
125 
apply (frule stable_reachable [OF _ _ subset_refl]) 

126 
apply (simp_all add: stable_def constrains_Int) 

127 
done 

128 

129 
(*Resembles the previous definition of Constrains*) 

130 
lemma Constrains_eq_constrains: 

46823  131 
"A Co B = {F \<in> program. F:(reachable(F) \<inter> A) co (reachable(F) \<inter> B)}" 
15634  132 
apply (unfold Constrains_def) 
133 
apply (blast dest: constrains_reachable_Int constrains_type [THEN subsetD] 

134 
intro: constrains_weaken) 

135 
done 

136 

137 
lemmas Constrains_def2 = Constrains_eq_constrains [THEN eq_reflection] 

138 

139 
lemma constrains_imp_Constrains: "F \<in> A co A' ==> F \<in> A Co A'" 

140 
apply (unfold Constrains_def) 

141 
apply (blast intro: constrains_weaken_L dest: constrainsD2) 

142 
done 

143 

144 
lemma ConstrainsI: 

145 
"[!!act s s'. [ act \<in> Acts(F); <s,s'>:act; s \<in> A ] ==> s':A'; 

146 
F \<in> program] 

147 
==> F \<in> A Co A'" 

148 
apply (auto simp add: Constrains_def constrains_def st_set_def) 

149 
apply (blast dest: reachable_type [THEN subsetD]) 

150 
done 

151 

152 
lemma Constrains_type: 

46823  153 
"A Co B \<subseteq> program" 
15634  154 
apply (unfold Constrains_def, blast) 
155 
done 

156 

46823  157 
lemma Constrains_empty: "F \<in> 0 Co B \<longleftrightarrow> F \<in> program" 
15634  158 
by (auto dest: Constrains_type [THEN subsetD] 
159 
intro: constrains_imp_Constrains) 

160 
declare Constrains_empty [iff] 

161 

46823  162 
lemma Constrains_state: "F \<in> A Co state \<longleftrightarrow> F \<in> program" 
15634  163 
apply (unfold Constrains_def) 
164 
apply (auto dest: Constrains_type [THEN subsetD] intro: constrains_imp_Constrains) 

165 
done 

166 
declare Constrains_state [iff] 

167 

168 
lemma Constrains_weaken_R: 

169 
"[ F \<in> A Co A'; A'<=B' ] ==> F \<in> A Co B'" 

170 
apply (unfold Constrains_def2) 

171 
apply (blast intro: constrains_weaken_R) 

172 
done 

173 

174 
lemma Constrains_weaken_L: 

175 
"[ F \<in> A Co A'; B<=A ] ==> F \<in> B Co A'" 

176 
apply (unfold Constrains_def2) 

177 
apply (blast intro: constrains_weaken_L st_set_subset) 

178 
done 

179 

180 
lemma Constrains_weaken: 

181 
"[ F \<in> A Co A'; B<=A; A'<=B' ] ==> F \<in> B Co B'" 

182 
apply (unfold Constrains_def2) 

183 
apply (blast intro: constrains_weaken st_set_subset) 

184 
done 

185 

186 
(** Union **) 

187 
lemma Constrains_Un: 

46823  188 
"[ F \<in> A Co A'; F \<in> B Co B' ] ==> F \<in> (A \<union> B) Co (A' \<union> B')" 
15634  189 
apply (unfold Constrains_def2, auto) 
190 
apply (simp add: Int_Un_distrib) 

191 
apply (blast intro: constrains_Un) 

192 
done 

193 

194 
lemma Constrains_UN: 

195 
"[(!!i. i \<in> I==>F \<in> A(i) Co A'(i)); F \<in> program] 

196 
==> F:(\<Union>i \<in> I. A(i)) Co (\<Union>i \<in> I. A'(i))" 

197 
by (auto intro: constrains_UN simp del: UN_simps 

198 
simp add: Constrains_def2 Int_UN_distrib) 

199 

200 

201 
(** Intersection **) 

202 

203 
lemma Constrains_Int: 

46823  204 
"[ F \<in> A Co A'; F \<in> B Co B']==> F:(A \<inter> B) Co (A' \<inter> B')" 
15634  205 
apply (unfold Constrains_def) 
46823  206 
apply (subgoal_tac "reachable (F) \<inter> (A \<inter> B) = (reachable (F) \<inter> A) \<inter> (reachable (F) \<inter> B) ") 
15634  207 
apply (auto intro: constrains_Int) 
208 
done 

209 

210 
lemma Constrains_INT: 

211 
"[ (!!i. i \<in> I ==>F \<in> A(i) Co A'(i)); F \<in> program ] 

212 
==> F:(\<Inter>i \<in> I. A(i)) Co (\<Inter>i \<in> I. A'(i))" 

213 
apply (simp (no_asm_simp) del: INT_simps add: Constrains_def INT_extend_simps) 

214 
apply (rule constrains_INT) 

215 
apply (auto simp add: Constrains_def) 

216 
done 

217 

46823  218 
lemma Constrains_imp_subset: "F \<in> A Co A' ==> reachable(F) \<inter> A \<subseteq> A'" 
15634  219 
apply (unfold Constrains_def) 
220 
apply (blast dest: constrains_imp_subset) 

221 
done 

222 

223 
lemma Constrains_trans: 

224 
"[ F \<in> A Co B; F \<in> B Co C ] ==> F \<in> A Co C" 

225 
apply (unfold Constrains_def2) 

226 
apply (blast intro: constrains_trans constrains_weaken) 

227 
done 

228 

229 
lemma Constrains_cancel: 

46823  230 
"[ F \<in> A Co (A' \<union> B); F \<in> B Co B' ] ==> F \<in> A Co (A' \<union> B')" 
15634  231 
apply (unfold Constrains_def2) 
232 
apply (simp (no_asm_use) add: Int_Un_distrib) 

233 
apply (blast intro: constrains_cancel) 

234 
done 

235 

236 
(*** Stable ***) 

237 
(* Useful because there's no Stable_weaken. [Tanja Vos] *) 

238 

239 
lemma stable_imp_Stable: 

240 
"F \<in> stable(A) ==> F \<in> Stable(A)" 

241 

242 
apply (unfold stable_def Stable_def) 

243 
apply (erule constrains_imp_Constrains) 

244 
done 

245 

246 
lemma Stable_eq: "[ F \<in> Stable(A); A = B ] ==> F \<in> Stable(B)" 

247 
by blast 

248 

249 
lemma Stable_eq_stable: 

46823  250 
"F \<in> Stable(A) \<longleftrightarrow> (F \<in> stable(reachable(F) \<inter> A))" 
15634  251 
apply (auto dest: constrainsD2 simp add: Stable_def stable_def Constrains_def2) 
252 
done 

253 

254 
lemma StableI: "F \<in> A Co A ==> F \<in> Stable(A)" 

255 
by (unfold Stable_def, assumption) 

256 

257 
lemma StableD: "F \<in> Stable(A) ==> F \<in> A Co A" 

258 
by (unfold Stable_def, assumption) 

259 

260 
lemma Stable_Un: 

46823  261 
"[ F \<in> Stable(A); F \<in> Stable(A') ] ==> F \<in> Stable(A \<union> A')" 
15634  262 
apply (unfold Stable_def) 
263 
apply (blast intro: Constrains_Un) 

264 
done 

265 

266 
lemma Stable_Int: 

46823  267 
"[ F \<in> Stable(A); F \<in> Stable(A') ] ==> F \<in> Stable (A \<inter> A')" 
15634  268 
apply (unfold Stable_def) 
269 
apply (blast intro: Constrains_Int) 

270 
done 

271 

272 
lemma Stable_Constrains_Un: 

46823  273 
"[ F \<in> Stable(C); F \<in> A Co (C \<union> A') ] 
274 
==> F \<in> (C \<union> A) Co (C \<union> A')" 

15634  275 
apply (unfold Stable_def) 
276 
apply (blast intro: Constrains_Un [THEN Constrains_weaken_R]) 

277 
done 

278 

279 
lemma Stable_Constrains_Int: 

46823  280 
"[ F \<in> Stable(C); F \<in> (C \<inter> A) Co A' ] 
281 
==> F \<in> (C \<inter> A) Co (C \<inter> A')" 

15634  282 
apply (unfold Stable_def) 
283 
apply (blast intro: Constrains_Int [THEN Constrains_weaken]) 

284 
done 

285 

286 
lemma Stable_UN: 

287 
"[ (!!i. i \<in> I ==> F \<in> Stable(A(i))); F \<in> program ] 

288 
==> F \<in> Stable (\<Union>i \<in> I. A(i))" 

289 
apply (simp add: Stable_def) 

290 
apply (blast intro: Constrains_UN) 

291 
done 

292 

293 
lemma Stable_INT: 

294 
"[(!!i. i \<in> I ==> F \<in> Stable(A(i))); F \<in> program ] 

295 
==> F \<in> Stable (\<Inter>i \<in> I. A(i))" 

296 
apply (simp add: Stable_def) 

297 
apply (blast intro: Constrains_INT) 

298 
done 

299 

300 
lemma Stable_reachable: "F \<in> program ==>F \<in> Stable (reachable(F))" 

301 
apply (simp (no_asm_simp) add: Stable_eq_stable Int_absorb) 

302 
done 

303 

46823  304 
lemma Stable_type: "Stable(A) \<subseteq> program" 
15634  305 
apply (unfold Stable_def) 
306 
apply (rule Constrains_type) 

307 
done 

308 

309 
(*** The Elimination Theorem. The "free" m has become universally quantified! 

310 
Should the premise be !!m instead of \<forall>m ? Would make it harder to use 

311 
in forward proof. ***) 

312 

313 
lemma Elimination: 

314 
"[ \<forall>m \<in> M. F \<in> ({s \<in> A. x(s) = m}) Co (B(m)); F \<in> program ] 

315 
==> F \<in> ({s \<in> A. x(s):M}) Co (\<Union>m \<in> M. B(m))" 

316 
apply (unfold Constrains_def, auto) 

46823  317 
apply (rule_tac A1 = "reachable (F) \<inter> A" 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32149
diff
changeset

318 
in UNITY.elimination [THEN constrains_weaken_L]) 
15634  319 
apply (auto intro: constrains_weaken_L) 
320 
done 

321 

322 
(* As above, but for the special case of A=state *) 

323 
lemma Elimination2: 

324 
"[ \<forall>m \<in> M. F \<in> {s \<in> state. x(s) = m} Co B(m); F \<in> program ] 

325 
==> F \<in> {s \<in> state. x(s):M} Co (\<Union>m \<in> M. B(m))" 

326 
apply (blast intro: Elimination) 

327 
done 

328 

329 
(** Unless **) 

330 

331 
lemma Unless_type: "A Unless B <=program" 

24893  332 
apply (unfold op_Unless_def) 
15634  333 
apply (rule Constrains_type) 
334 
done 

335 

336 
(*** Specialized laws for handling Always ***) 

337 

338 
(** Natural deduction rules for "Always A" **) 

339 

340 
lemma AlwaysI: 

341 
"[ Init(F)<=A; F \<in> Stable(A) ] ==> F \<in> Always(A)" 

342 

343 
apply (unfold Always_def initially_def) 

344 
apply (frule Stable_type [THEN subsetD], auto) 

345 
done 

346 

347 
lemma AlwaysD: "F \<in> Always(A) ==> Init(F)<=A & F \<in> Stable(A)" 

348 
by (simp add: Always_def initially_def) 

349 

45602  350 
lemmas AlwaysE = AlwaysD [THEN conjE] 
351 
lemmas Always_imp_Stable = AlwaysD [THEN conjunct2] 

15634  352 

353 
(*The set of all reachable states is Always*) 

46823  354 
lemma Always_includes_reachable: "F \<in> Always(A) ==> reachable(F) \<subseteq> A" 
15634  355 
apply (simp (no_asm_use) add: Stable_def Constrains_def constrains_def Always_def initially_def) 
356 
apply (rule subsetI) 

357 
apply (erule reachable.induct) 

358 
apply (blast intro: reachable.intros)+ 

359 
done 

360 

361 
lemma invariant_imp_Always: 

362 
"F \<in> invariant(A) ==> F \<in> Always(A)" 

363 
apply (unfold Always_def invariant_def Stable_def stable_def) 

364 
apply (blast intro: constrains_imp_Constrains) 

365 
done 

366 

45602  367 
lemmas Always_reachable = invariant_reachable [THEN invariant_imp_Always] 
15634  368 

46823  369 
lemma Always_eq_invariant_reachable: "Always(A) = {F \<in> program. F \<in> invariant(reachable(F) \<inter> A)}" 
15634  370 
apply (simp (no_asm) add: Always_def invariant_def Stable_def Constrains_def2 stable_def initially_def) 
371 
apply (rule equalityI, auto) 

372 
apply (blast intro: reachable.intros reachable_type) 

373 
done 

374 

375 
(*the RHS is the traditional definition of the "always" operator*) 

46823  376 
lemma Always_eq_includes_reachable: "Always(A) = {F \<in> program. reachable(F) \<subseteq> A}" 
15634  377 
apply (rule equalityI, safe) 
378 
apply (auto dest: invariant_includes_reachable 

379 
simp add: subset_Int_iff invariant_reachable Always_eq_invariant_reachable) 

380 
done 

381 

46823  382 
lemma Always_type: "Always(A) \<subseteq> program" 
15634  383 
by (unfold Always_def initially_def, auto) 
384 

385 
lemma Always_state_eq: "Always(state) = program" 

386 
apply (rule equalityI) 

387 
apply (auto dest: Always_type [THEN subsetD] reachable_type [THEN subsetD] 

388 
simp add: Always_eq_includes_reachable) 

389 
done 

390 
declare Always_state_eq [simp] 

391 

392 
lemma state_AlwaysI: "F \<in> program ==> F \<in> Always(state)" 

393 
by (auto dest: reachable_type [THEN subsetD] 

394 
simp add: Always_eq_includes_reachable) 

395 

396 
lemma Always_eq_UN_invariant: "st_set(A) ==> Always(A) = (\<Union>I \<in> Pow(A). invariant(I))" 

397 
apply (simp (no_asm) add: Always_eq_includes_reachable) 

398 
apply (rule equalityI, auto) 

399 
apply (blast intro: invariantI rev_subsetD [OF _ Init_into_reachable] 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32149
diff
changeset

400 
rev_subsetD [OF _ invariant_includes_reachable] 
15634  401 
dest: invariant_type [THEN subsetD])+ 
402 
done 

403 

46823  404 
lemma Always_weaken: "[ F \<in> Always(A); A \<subseteq> B ] ==> F \<in> Always(B)" 
15634  405 
by (auto simp add: Always_eq_includes_reachable) 
406 

407 

408 
(*** "Co" rules involving Always ***) 

409 
lemmas Int_absorb2 = subset_Int_iff [unfolded iff_def, THEN conjunct1, THEN mp] 

410 

46823  411 
lemma Always_Constrains_pre: "F \<in> Always(I) ==> (F:(I \<inter> A) Co A') \<longleftrightarrow> (F \<in> A Co A')" 
15634  412 
apply (simp (no_asm_simp) add: Always_includes_reachable [THEN Int_absorb2] Constrains_def Int_assoc [symmetric]) 
413 
done 

414 

46823  415 
lemma Always_Constrains_post: "F \<in> Always(I) ==> (F \<in> A Co (I \<inter> A')) \<longleftrightarrow>(F \<in> A Co A')" 
15634  416 
apply (simp (no_asm_simp) add: Always_includes_reachable [THEN Int_absorb2] Constrains_eq_constrains Int_assoc [symmetric]) 
417 
done 

418 

46823  419 
lemma Always_ConstrainsI: "[ F \<in> Always(I); F \<in> (I \<inter> A) Co A' ] ==> F \<in> A Co A'" 
15634  420 
by (blast intro: Always_Constrains_pre [THEN iffD1]) 
421 

46823  422 
(* [ F \<in> Always(I); F \<in> A Co A' ] ==> F \<in> A Co (I \<inter> A') *) 
45602  423 
lemmas Always_ConstrainsD = Always_Constrains_post [THEN iffD2] 
15634  424 

425 
(*The analogous proof of Always_LeadsTo_weaken doesn't terminate*) 

426 
lemma Always_Constrains_weaken: 

46823  427 
"[F \<in> Always(C); F \<in> A Co A'; C \<inter> B<=A; C \<inter> A'<=B']==>F \<in> B Co B'" 
15634  428 
apply (rule Always_ConstrainsI) 
429 
apply (drule_tac [2] Always_ConstrainsD, simp_all) 

430 
apply (blast intro: Constrains_weaken) 

431 
done 

432 

433 
(** Conjoining Always properties **) 

46823  434 
lemma Always_Int_distrib: "Always(A \<inter> B) = Always(A) \<inter> Always(B)" 
15634  435 
by (auto simp add: Always_eq_includes_reachable) 
436 

437 
(* the premise i \<in> I is need since \<Inter>is formally not defined for I=0 *) 

438 
lemma Always_INT_distrib: "i \<in> I==>Always(\<Inter>i \<in> I. A(i)) = (\<Inter>i \<in> I. Always(A(i)))" 

439 
apply (rule equalityI) 

440 
apply (auto simp add: Inter_iff Always_eq_includes_reachable) 

441 
done 

442 

443 

46823  444 
lemma Always_Int_I: "[ F \<in> Always(A); F \<in> Always(B) ] ==> F \<in> Always(A \<inter> B)" 
15634  445 
apply (simp (no_asm_simp) add: Always_Int_distrib) 
446 
done 

447 

448 
(*Allows a kind of "implication introduction"*) 

46823  449 
lemma Always_Diff_Un_eq: "[ F \<in> Always(A) ] ==> (F \<in> Always(CA \<union> B)) \<longleftrightarrow> (F \<in> Always(B))" 
15634  450 
by (auto simp add: Always_eq_includes_reachable) 
451 

452 
(*Delete the nearest invariance assumption (which will be the second one 

453 
used by Always_Int_I) *) 

45602  454 
lemmas Always_thin = thin_rl [of "F \<in> Always(A)"] 
15634  455 

456 
ML 

457 
{* 

458 
(*Combines two invariance ASSUMPTIONS into one. USEFUL??*) 

24893  459 
val Always_Int_tac = dtac @{thm Always_Int_I} THEN' assume_tac THEN' etac @{thm Always_thin}; 
15634  460 

461 
(*Combines a list of invariance THEOREMS into one.*) 

24893  462 
val Always_Int_rule = foldr1 (fn (th1,th2) => [th1,th2] MRS @{thm Always_Int_I}); 
15634  463 

464 
(*To allow expansion of the program's definition when appropriate*) 

31902  465 
structure Program_Defs = Named_Thms 
466 
( 

45294  467 
val name = @{binding program} 
31902  468 
val description = "program definitions" 
469 
); 

15634  470 

471 
(*proves "co" properties when the program is specified*) 

472 

23894
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23543
diff
changeset

473 
fun constrains_tac ctxt = 
42793  474 
let val ss = simpset_of ctxt in 
15634  475 
SELECT_GOAL 
476 
(EVERY [REPEAT (Always_Int_tac 1), 

24893  477 
REPEAT (etac @{thm Always_ConstrainsI} 1 
15634  478 
ORELSE 
24893  479 
resolve_tac [@{thm StableI}, @{thm stableI}, 
480 
@{thm constrains_imp_Constrains}] 1), 

481 
rtac @{thm constrainsI} 1, 

15634  482 
(* Three subgoals *) 
24893  483 
rewrite_goal_tac [@{thm st_set_def}] 3, 
42793  484 
REPEAT (force_tac ctxt 2), 
31902  485 
full_simp_tac (ss addsimps (Program_Defs.get ctxt)) 1, 
42793  486 
ALLGOALS (clarify_tac ctxt), 
35409  487 
REPEAT (FIRSTGOAL (etac @{thm disjE})), 
42793  488 
ALLGOALS (clarify_tac ctxt), 
35409  489 
REPEAT (FIRSTGOAL (etac @{thm disjE})), 
42793  490 
ALLGOALS (clarify_tac ctxt), 
15634  491 
ALLGOALS (asm_full_simp_tac ss), 
42793  492 
ALLGOALS (clarify_tac ctxt)]) 
23894
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23543
diff
changeset

493 
end; 
15634  494 

495 
(*For proving invariants*) 

42793  496 
fun always_tac ctxt i = 
497 
rtac @{thm AlwaysI} i THEN force_tac ctxt i THEN constrains_tac ctxt i; 

15634  498 
*} 
499 

31902  500 
setup Program_Defs.setup 
24051
896fb015079c
replaced program_defs_ref by proper context data (via attribute "program");
wenzelm
parents:
23894
diff
changeset

501 

16183
052d9aba392d
renamed "constrains" to "safety" to avoid keyword clash
paulson
parents:
15634
diff
changeset

502 
method_setup safety = {* 
30549  503 
Scan.succeed (SIMPLE_METHOD' o constrains_tac) *} 
21588  504 
"for proving safety properties" 
15634  505 

23894
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23543
diff
changeset

506 
method_setup always = {* 
30549  507 
Scan.succeed (SIMPLE_METHOD' o always_tac) *} 
23894
1a4167d761ac
tactics: avoid dynamic reference to accidental theory context (via ML_Context.the_context etc.);
wenzelm
parents:
23543
diff
changeset

508 
"for proving invariants" 
15634  509 

11479  510 
end 