|
1 |
|
2 header {* \section{Generation of Verification Conditions} *} |
|
3 |
|
4 theory OG_Tactics = OG_Hoare: |
|
5 |
|
6 lemmas ann_hoare_intros=AnnBasic AnnSeq AnnCond1 AnnCond2 AnnWhile AnnAwait AnnConseq |
|
7 lemmas oghoare_intros=Parallel Basic Seq Cond While Conseq |
|
8 |
|
9 lemma ParallelConseqRule: |
|
10 "\<lbrakk> p \<subseteq> (\<Inter>i\<in>{i. i<length Ts}. pre(the(com(Ts ! i)))); |
|
11 \<parallel>- (\<Inter>i\<in>{i. i<length Ts}. pre(the(com(Ts ! i)))) |
|
12 (Parallel Ts) |
|
13 (\<Inter>i\<in>{i. i<length Ts}. post(Ts ! i)); |
|
14 (\<Inter>i\<in>{i. i<length Ts}. post(Ts ! i)) \<subseteq> q \<rbrakk> |
|
15 \<Longrightarrow> \<parallel>- p (Parallel Ts) q" |
|
16 apply (rule Conseq) |
|
17 prefer 2 |
|
18 apply fast |
|
19 apply assumption+ |
|
20 done |
|
21 |
|
22 lemma SkipRule: "p \<subseteq> q \<Longrightarrow> \<parallel>- p (Basic id) q" |
|
23 apply(rule oghoare_intros) |
|
24 prefer 2 apply(rule Basic) |
|
25 prefer 2 apply(rule subset_refl) |
|
26 apply(simp add:Id_def) |
|
27 done |
|
28 |
|
29 lemma BasicRule: "p \<subseteq> {s. (f s)\<in>q} \<Longrightarrow> \<parallel>- p (Basic f) q" |
|
30 apply(rule oghoare_intros) |
|
31 prefer 2 apply(rule oghoare_intros) |
|
32 prefer 2 apply(rule subset_refl) |
|
33 apply assumption |
|
34 done |
|
35 |
|
36 lemma SeqRule: "\<lbrakk> \<parallel>- p c1 r; \<parallel>- r c2 q \<rbrakk> \<Longrightarrow> \<parallel>- p (Seq c1 c2) q" |
|
37 apply(rule Seq) |
|
38 apply fast+ |
|
39 done |
|
40 |
|
41 lemma CondRule: |
|
42 "\<lbrakk> p \<subseteq> {s. (s\<in>b \<longrightarrow> s\<in>w) \<and> (s\<notin>b \<longrightarrow> s\<in>w')}; \<parallel>- w c1 q; \<parallel>- w' c2 q \<rbrakk> |
|
43 \<Longrightarrow> \<parallel>- p (Cond b c1 c2) q" |
|
44 apply(rule Cond) |
|
45 apply(rule Conseq) |
|
46 prefer 4 apply(rule Conseq) |
|
47 apply simp_all |
|
48 apply force+ |
|
49 done |
|
50 |
|
51 lemma WhileRule: "\<lbrakk> p \<subseteq> i; \<parallel>- (i \<inter> b) c i ; (i \<inter> (-b)) \<subseteq> q \<rbrakk> |
|
52 \<Longrightarrow> \<parallel>- p (While b i c) q" |
|
53 apply(rule Conseq) |
|
54 prefer 2 apply(rule While) |
|
55 apply assumption+ |
|
56 done |
|
57 |
|
58 text {* Three new proof rules for special instances of the @{text |
|
59 AnnBasic} and the @{text AnnAwait} commands when the transformation |
|
60 performed on the state is the identity, and for an @{text AnnAwait} |
|
61 command where the boolean condition is @{text "{s. True}"}: *} |
|
62 |
|
63 lemma AnnatomRule: |
|
64 "\<lbrakk> atom_com(c); \<parallel>- r c q \<rbrakk> \<Longrightarrow> \<turnstile> (AnnAwait r {s. True} c) q" |
|
65 apply(rule AnnAwait) |
|
66 apply simp_all |
|
67 done |
|
68 |
|
69 lemma AnnskipRule: |
|
70 "r \<subseteq> q \<Longrightarrow> \<turnstile> (AnnBasic r id) q" |
|
71 apply(rule AnnBasic) |
|
72 apply simp |
|
73 done |
|
74 |
|
75 lemma AnnwaitRule: |
|
76 "\<lbrakk> (r \<inter> b) \<subseteq> q \<rbrakk> \<Longrightarrow> \<turnstile> (AnnAwait r b (Basic id)) q" |
|
77 apply(rule AnnAwait) |
|
78 apply simp |
|
79 apply(rule BasicRule) |
|
80 apply simp |
|
81 done |
|
82 |
|
83 text {* Lemmata to avoid using the definition of @{text |
|
84 map_ann_hoare}, @{text interfree_aux}, @{text interfree_swap} and |
|
85 @{text interfree} by splitting it into different cases: *} |
|
86 |
|
87 lemma interfree_aux_rule1: "interfree_aux(co, q, None)" |
|
88 by(simp add:interfree_aux_def) |
|
89 |
|
90 lemma interfree_aux_rule2: |
|
91 "\<forall>(R,r)\<in>(atomics a). \<parallel>- (q \<inter> R) r q \<Longrightarrow> interfree_aux(None, q, Some a)" |
|
92 apply(simp add:interfree_aux_def) |
|
93 apply(force elim:oghoare_sound) |
|
94 done |
|
95 |
|
96 lemma interfree_aux_rule3: |
|
97 "(\<forall>(R, r)\<in>(atomics a). \<parallel>- (q \<inter> R) r q \<and> (\<forall>p\<in>(assertions c). \<parallel>- (p \<inter> R) r p)) |
|
98 \<Longrightarrow> interfree_aux(Some c, q, Some a)" |
|
99 apply(simp add:interfree_aux_def) |
|
100 apply(force elim:oghoare_sound) |
|
101 done |
|
102 |
|
103 lemma AnnBasic_assertions: |
|
104 "\<lbrakk>interfree_aux(None, r, Some a); interfree_aux(None, q, Some a)\<rbrakk> \<Longrightarrow> |
|
105 interfree_aux(Some (AnnBasic r f), q, Some a)" |
|
106 apply(simp add: interfree_aux_def) |
|
107 by force |
|
108 |
|
109 lemma AnnSeq_assertions: |
|
110 "\<lbrakk> interfree_aux(Some c1, q, Some a); interfree_aux(Some c2, q, Some a)\<rbrakk>\<Longrightarrow> |
|
111 interfree_aux(Some (AnnSeq c1 c2), q, Some a)" |
|
112 apply(simp add: interfree_aux_def) |
|
113 by force |
|
114 |
|
115 lemma AnnCond1_assertions: |
|
116 "\<lbrakk> interfree_aux(None, r, Some a); interfree_aux(Some c1, q, Some a); |
|
117 interfree_aux(Some c2, q, Some a)\<rbrakk>\<Longrightarrow> |
|
118 interfree_aux(Some(AnnCond1 r b c1 c2), q, Some a)" |
|
119 apply(simp add: interfree_aux_def) |
|
120 by force |
|
121 |
|
122 lemma AnnCond2_assertions: |
|
123 "\<lbrakk> interfree_aux(None, r, Some a); interfree_aux(Some c, q, Some a)\<rbrakk>\<Longrightarrow> |
|
124 interfree_aux(Some (AnnCond2 r b c), q, Some a)" |
|
125 apply(simp add: interfree_aux_def) |
|
126 by force |
|
127 |
|
128 lemma AnnWhile_assertions: |
|
129 "\<lbrakk> interfree_aux(None, r, Some a); interfree_aux(None, i, Some a); |
|
130 interfree_aux(Some c, q, Some a)\<rbrakk>\<Longrightarrow> |
|
131 interfree_aux(Some (AnnWhile r b i c), q, Some a)" |
|
132 apply(simp add: interfree_aux_def) |
|
133 by force |
|
134 |
|
135 lemma AnnAwait_assertions: |
|
136 "\<lbrakk> interfree_aux(None, r, Some a); interfree_aux(None, q, Some a)\<rbrakk>\<Longrightarrow> |
|
137 interfree_aux(Some (AnnAwait r b c), q, Some a)" |
|
138 apply(simp add: interfree_aux_def) |
|
139 by force |
|
140 |
|
141 lemma AnnBasic_atomics: |
|
142 "\<parallel>- (q \<inter> r) (Basic f) q \<Longrightarrow> interfree_aux(None, q, Some (AnnBasic r f))" |
|
143 by(simp add: interfree_aux_def oghoare_sound) |
|
144 |
|
145 lemma AnnSeq_atomics: |
|
146 "\<lbrakk> interfree_aux(Any, q, Some a1); interfree_aux(Any, q, Some a2)\<rbrakk>\<Longrightarrow> |
|
147 interfree_aux(Any, q, Some (AnnSeq a1 a2))" |
|
148 apply(simp add: interfree_aux_def) |
|
149 by force |
|
150 |
|
151 lemma AnnCond1_atomics: |
|
152 "\<lbrakk> interfree_aux(Any, q, Some a1); interfree_aux(Any, q, Some a2)\<rbrakk>\<Longrightarrow> |
|
153 interfree_aux(Any, q, Some (AnnCond1 r b a1 a2))" |
|
154 apply(simp add: interfree_aux_def) |
|
155 by force |
|
156 |
|
157 lemma AnnCond2_atomics: |
|
158 "interfree_aux (Any, q, Some a)\<Longrightarrow> interfree_aux(Any, q, Some (AnnCond2 r b a))" |
|
159 by(simp add: interfree_aux_def) |
|
160 |
|
161 lemma AnnWhile_atomics: "interfree_aux (Any, q, Some a) |
|
162 \<Longrightarrow> interfree_aux(Any, q, Some (AnnWhile r b i a))" |
|
163 by(simp add: interfree_aux_def) |
|
164 |
|
165 lemma Annatom_atomics: |
|
166 "\<parallel>- (q \<inter> r) a q \<Longrightarrow> interfree_aux (None, q, Some (AnnAwait r {x. True} a))" |
|
167 by(simp add: interfree_aux_def oghoare_sound) |
|
168 |
|
169 lemma AnnAwait_atomics: |
|
170 "\<parallel>- (q \<inter> (r \<inter> b)) a q \<Longrightarrow> interfree_aux (None, q, Some (AnnAwait r b a))" |
|
171 by(simp add: interfree_aux_def oghoare_sound) |
|
172 |
|
173 constdefs |
|
174 interfree_swap :: "('a ann_triple_op * ('a ann_triple_op) list) \<Rightarrow> bool" |
|
175 "interfree_swap == \<lambda>(x, xs). \<forall>y\<in>set xs. interfree_aux (com x, post x, com y) |
|
176 \<and> interfree_aux(com y, post y, com x)" |
|
177 |
|
178 lemma interfree_swap_Empty: "interfree_swap (x, [])" |
|
179 by(simp add:interfree_swap_def) |
|
180 |
|
181 lemma interfree_swap_List: |
|
182 "\<lbrakk> interfree_aux (com x, post x, com y); |
|
183 interfree_aux (com y, post y ,com x); interfree_swap (x, xs) \<rbrakk> |
|
184 \<Longrightarrow> interfree_swap (x, y#xs)" |
|
185 by(simp add:interfree_swap_def) |
|
186 |
|
187 lemma interfree_swap_Map: "\<forall>k. i\<le>k \<and> k<j \<longrightarrow> interfree_aux (com x, post x, c k) |
|
188 \<and> interfree_aux (c k, Q k, com x) |
|
189 \<Longrightarrow> interfree_swap (x, map (\<lambda>k. (c k, Q k)) [i..j(])" |
|
190 by(force simp add: interfree_swap_def less_diff_conv) |
|
191 |
|
192 lemma interfree_Empty: "interfree []" |
|
193 by(simp add:interfree_def) |
|
194 |
|
195 lemma interfree_List: |
|
196 "\<lbrakk> interfree_swap(x, xs); interfree xs \<rbrakk> \<Longrightarrow> interfree (x#xs)" |
|
197 apply(simp add:interfree_def interfree_swap_def) |
|
198 apply clarify |
|
199 apply(case_tac i) |
|
200 apply(case_tac j) |
|
201 apply simp_all |
|
202 apply(case_tac j,simp+) |
|
203 done |
|
204 |
|
205 lemma interfree_Map: |
|
206 "(\<forall>i j. a\<le>i \<and> i<b \<and> a\<le>j \<and> j<b \<and> i\<noteq>j \<longrightarrow> interfree_aux (c i, Q i, c j)) |
|
207 \<Longrightarrow> interfree (map (\<lambda>k. (c k, Q k)) [a..b(])" |
|
208 by(force simp add: interfree_def less_diff_conv) |
|
209 |
|
210 constdefs map_ann_hoare :: "(('a ann_com_op * 'a assn) list) \<Rightarrow> bool " ("[\<turnstile>] _" [0] 45) |
|
211 "[\<turnstile>] Ts == (\<forall>i<length Ts. \<exists>c q. Ts!i=(Some c, q) \<and> \<turnstile> c q)" |
|
212 |
|
213 lemma MapAnnEmpty: "[\<turnstile>] []" |
|
214 by(simp add:map_ann_hoare_def) |
|
215 |
|
216 lemma MapAnnList: "\<lbrakk> \<turnstile> c q ; [\<turnstile>] xs \<rbrakk> \<Longrightarrow> [\<turnstile>] (Some c,q)#xs" |
|
217 apply(simp add:map_ann_hoare_def) |
|
218 apply clarify |
|
219 apply(case_tac i,simp+) |
|
220 done |
|
221 |
|
222 lemma MapAnnMap: |
|
223 "\<forall>k. i\<le>k \<and> k<j \<longrightarrow> \<turnstile> (c k) (Q k) \<Longrightarrow> [\<turnstile>] map (\<lambda>k. (Some (c k), Q k)) [i..j(]" |
|
224 apply(simp add: map_ann_hoare_def less_diff_conv) |
|
225 done |
|
226 |
|
227 lemma ParallelRule:"\<lbrakk> [\<turnstile>] Ts ; interfree Ts \<rbrakk> |
|
228 \<Longrightarrow> \<parallel>- (\<Inter>i\<in>{i. i<length Ts}. pre(the(com(Ts!i)))) |
|
229 Parallel Ts |
|
230 (\<Inter>i\<in>{i. i<length Ts}. post(Ts!i))" |
|
231 apply(rule Parallel) |
|
232 apply(simp add:map_ann_hoare_def) |
|
233 apply simp |
|
234 done |
|
235 (* |
|
236 lemma ParamParallelRule: |
|
237 "\<lbrakk> \<forall>k<n. \<turnstile> (c k) (Q k); |
|
238 \<forall>k l. k<n \<and> l<n \<and> k\<noteq>l \<longrightarrow> interfree_aux (Some(c k), Q k, Some(c l)) \<rbrakk> |
|
239 \<Longrightarrow> \<parallel>- (\<Inter>i\<in>{i. i<n} . pre(c i)) COBEGIN SCHEME [0\<le>i<n] (c i) (Q i) COEND (\<Inter>i\<in>{i. i<n} . Q i )" |
|
240 apply(rule ParallelConseqRule) |
|
241 apply simp |
|
242 apply clarify |
|
243 apply force |
|
244 apply(rule ParallelRule) |
|
245 apply(rule MapAnnMap) |
|
246 apply simp |
|
247 apply(rule interfree_Map) |
|
248 apply simp |
|
249 apply simp |
|
250 apply clarify |
|
251 apply force |
|
252 done |
|
253 *) |
|
254 |
|
255 text {* The following are some useful lemmas and simplification |
|
256 tactics to control which theorems are used to simplify at each moment, |
|
257 so that the original input does not suffer any unexpected |
|
258 transformation. *} |
|
259 |
|
260 lemma Compl_Collect: "-(Collect b) = {x. \<not>(b x)}" |
|
261 by fast |
|
262 lemma list_length: "length []=0 \<and> length (x#xs) = Suc(length xs)" |
|
263 by simp |
|
264 lemma list_lemmas: "length []=0 \<and> length (x#xs) = Suc(length xs) |
|
265 \<and> (x#xs) ! 0=x \<and> (x#xs) ! Suc n = xs ! n" |
|
266 by simp |
|
267 lemma le_Suc_eq_insert: "{i. i <Suc n} = insert n {i. i< n}" |
|
268 apply auto |
|
269 by arith |
|
270 lemmas primrecdef_list = "pre.simps" "assertions.simps" "atomics.simps" "atom_com.simps" |
|
271 lemmas my_simp_list = list_lemmas fst_conv snd_conv |
|
272 not_less0 refl le_Suc_eq_insert Suc_not_Zero Zero_not_Suc Suc_Suc_eq |
|
273 Collect_mem_eq ball_simps option.simps primrecdef_list |
|
274 lemmas ParallelConseq_list = INTER_def Collect_conj_eq length_map length_upt length_append list_length |
|
275 |
|
276 ML {* |
|
277 val before_interfree_simp_tac = (simp_tac (HOL_basic_ss addsimps [thm "com.simps", thm "post.simps"])) |
|
278 |
|
279 val interfree_simp_tac = (asm_simp_tac (HOL_ss addsimps [thm "split", thm "ball_Un", thm "ball_empty"]@(thms "my_simp_list"))) |
|
280 |
|
281 val ParallelConseq = (simp_tac (HOL_basic_ss addsimps (thms "ParallelConseq_list")@(thms "my_simp_list"))) |
|
282 *} |
|
283 |
|
284 text {* The following tactic applies @{text tac} to each conjunct in a |
|
285 subgoal of the form @{text "A \<Longrightarrow> a1 \<and> a2 \<and> .. \<and> an"} returning |
|
286 @{text n} subgoals, one for each conjunct: *} |
|
287 |
|
288 ML {* |
|
289 fun conjI_Tac tac i st = st |> |
|
290 ( (EVERY [rtac conjI i, |
|
291 conjI_Tac tac (i+1), |
|
292 tac i]) ORELSE (tac i) ) |
|
293 *} |
|
294 |
|
295 |
|
296 subsubsection {* Tactic for the generation of the verification conditions *} |
|
297 |
|
298 text {* The tactic basically uses two subtactics: |
|
299 |
|
300 \begin{description} |
|
301 |
|
302 \item[HoareRuleTac] is called at the level of parallel programs, it |
|
303 uses the ParallelTac to solve parallel composition of programs. |
|
304 This verification has two parts, namely, (1) all component programs are |
|
305 correct and (2) they are interference free. @{text HoareRuleTac} is |
|
306 also called at the level of atomic regions, i.e. @{text "\<langle> \<rangle>"} and |
|
307 @{text "AWAIT b THEN _ END"}, and at each interference freedom test. |
|
308 |
|
309 \item[AnnHoareRuleTac] is for component programs which |
|
310 are annotated programs and so, there are not unknown assertions |
|
311 (no need to use the parameter precond, see NOTE). |
|
312 |
|
313 NOTE: precond(::bool) informs if the subgoal has the form @{text "\<parallel>- ?p c q"}, |
|
314 in this case we have precond=False and the generated verification |
|
315 condition would have the form @{text "?p \<subseteq> \<dots>"} which can be solved by |
|
316 @{text "rtac subset_refl"}, if True we proceed to simplify it using |
|
317 the simplification tactics above. |
|
318 |
|
319 \end{description} |
|
320 *} |
|
321 |
|
322 ML {* |
|
323 |
|
324 fun WlpTac i = (rtac (thm "SeqRule") i) THEN (HoareRuleTac false (i+1)) |
|
325 and HoareRuleTac precond i st = st |> |
|
326 ( (WlpTac i THEN HoareRuleTac precond i) |
|
327 ORELSE |
|
328 (FIRST[rtac (thm "SkipRule") i, |
|
329 rtac (thm "BasicRule") i, |
|
330 EVERY[rtac (thm "ParallelConseqRule") i, |
|
331 ParallelConseq (i+2), |
|
332 ParallelTac (i+1), |
|
333 ParallelConseq i], |
|
334 EVERY[rtac (thm "CondRule") i, |
|
335 HoareRuleTac false (i+2), |
|
336 HoareRuleTac false (i+1)], |
|
337 EVERY[rtac (thm "WhileRule") i, |
|
338 HoareRuleTac true (i+1)], |
|
339 K all_tac i ] |
|
340 THEN (if precond then (K all_tac i) else (rtac (thm "subset_refl") i)))) |
|
341 |
|
342 and AnnWlpTac i = (rtac (thm "AnnSeq") i) THEN (AnnHoareRuleTac (i+1)) |
|
343 and AnnHoareRuleTac i st = st |> |
|
344 ( (AnnWlpTac i THEN AnnHoareRuleTac i ) |
|
345 ORELSE |
|
346 (FIRST[(rtac (thm "AnnskipRule") i), |
|
347 EVERY[rtac (thm "AnnatomRule") i, |
|
348 HoareRuleTac true (i+1)], |
|
349 (rtac (thm "AnnwaitRule") i), |
|
350 rtac (thm "AnnBasic") i, |
|
351 EVERY[rtac (thm "AnnCond1") i, |
|
352 AnnHoareRuleTac (i+3), |
|
353 AnnHoareRuleTac (i+1)], |
|
354 EVERY[rtac (thm "AnnCond2") i, |
|
355 AnnHoareRuleTac (i+1)], |
|
356 EVERY[rtac (thm "AnnWhile") i, |
|
357 AnnHoareRuleTac (i+2)], |
|
358 EVERY[rtac (thm "AnnAwait") i, |
|
359 HoareRuleTac true (i+1)], |
|
360 K all_tac i])) |
|
361 |
|
362 and ParallelTac i = EVERY[rtac (thm "ParallelRule") i, |
|
363 interfree_Tac (i+1), |
|
364 MapAnn_Tac i] |
|
365 |
|
366 and MapAnn_Tac i st = st |> |
|
367 (FIRST[rtac (thm "MapAnnEmpty") i, |
|
368 EVERY[rtac (thm "MapAnnList") i, |
|
369 MapAnn_Tac (i+1), |
|
370 AnnHoareRuleTac i], |
|
371 EVERY[rtac (thm "MapAnnMap") i, |
|
372 rtac (thm "allI") i,rtac (thm "impI") i, |
|
373 AnnHoareRuleTac i]]) |
|
374 |
|
375 and interfree_swap_Tac i st = st |> |
|
376 (FIRST[rtac (thm "interfree_swap_Empty") i, |
|
377 EVERY[rtac (thm "interfree_swap_List") i, |
|
378 interfree_swap_Tac (i+2), |
|
379 interfree_aux_Tac (i+1), |
|
380 interfree_aux_Tac i ], |
|
381 EVERY[rtac (thm "interfree_swap_Map") i, |
|
382 rtac (thm "allI") i,rtac (thm "impI") i, |
|
383 conjI_Tac (interfree_aux_Tac) i]]) |
|
384 |
|
385 and interfree_Tac i st = st |> |
|
386 (FIRST[rtac (thm "interfree_Empty") i, |
|
387 EVERY[rtac (thm "interfree_List") i, |
|
388 interfree_Tac (i+1), |
|
389 interfree_swap_Tac i], |
|
390 EVERY[rtac (thm "interfree_Map") i, |
|
391 rtac (thm "allI") i,rtac (thm "allI") i,rtac (thm "impI") i, |
|
392 interfree_aux_Tac i ]]) |
|
393 |
|
394 and interfree_aux_Tac i = (before_interfree_simp_tac i ) THEN |
|
395 (FIRST[rtac (thm "interfree_aux_rule1") i, |
|
396 dest_assertions_Tac i]) |
|
397 |
|
398 and dest_assertions_Tac i st = st |> |
|
399 (FIRST[EVERY[rtac (thm "AnnBasic_assertions") i, |
|
400 dest_atomics_Tac (i+1), |
|
401 dest_atomics_Tac i], |
|
402 EVERY[rtac (thm "AnnSeq_assertions") i, |
|
403 dest_assertions_Tac (i+1), |
|
404 dest_assertions_Tac i], |
|
405 EVERY[rtac (thm "AnnCond1_assertions") i, |
|
406 dest_assertions_Tac (i+2), |
|
407 dest_assertions_Tac (i+1), |
|
408 dest_atomics_Tac i], |
|
409 EVERY[rtac (thm "AnnCond2_assertions") i, |
|
410 dest_assertions_Tac (i+1), |
|
411 dest_atomics_Tac i], |
|
412 EVERY[rtac (thm "AnnWhile_assertions") i, |
|
413 dest_assertions_Tac (i+2), |
|
414 dest_atomics_Tac (i+1), |
|
415 dest_atomics_Tac i], |
|
416 EVERY[rtac (thm "AnnAwait_assertions") i, |
|
417 dest_atomics_Tac (i+1), |
|
418 dest_atomics_Tac i], |
|
419 dest_atomics_Tac i]) |
|
420 |
|
421 and dest_atomics_Tac i st = st |> |
|
422 (FIRST[EVERY[rtac (thm "AnnBasic_atomics") i, |
|
423 HoareRuleTac true i], |
|
424 EVERY[rtac (thm "AnnSeq_atomics") i, |
|
425 dest_atomics_Tac (i+1), |
|
426 dest_atomics_Tac i], |
|
427 EVERY[rtac (thm "AnnCond1_atomics") i, |
|
428 dest_atomics_Tac (i+1), |
|
429 dest_atomics_Tac i], |
|
430 EVERY[rtac (thm "AnnCond2_atomics") i, |
|
431 dest_atomics_Tac i], |
|
432 EVERY[rtac (thm "AnnWhile_atomics") i, |
|
433 dest_atomics_Tac i], |
|
434 EVERY[rtac (thm "Annatom_atomics") i, |
|
435 HoareRuleTac true i], |
|
436 EVERY[rtac (thm "AnnAwait_atomics") i, |
|
437 HoareRuleTac true i], |
|
438 K all_tac i]) |
|
439 *} |
|
440 |
|
441 |
|
442 text {* The final tactic is given the name @{text oghoare}: *} |
|
443 |
|
444 ML {* |
|
445 fun oghoare_tac i thm = SUBGOAL (fn (term, _) => |
|
446 (HoareRuleTac true i)) i thm |
|
447 *} |
|
448 |
|
449 text {* Notice that the tactic for parallel programs @{text |
|
450 "oghoare_tac"} is initially invoked with the value @{text true} for |
|
451 the parameter @{text precond}. |
|
452 |
|
453 Parts of the tactic can be also individually used to generate the |
|
454 verification conditions for annotated sequential programs and to |
|
455 generate verification conditions out of interference freedom tests: *} |
|
456 |
|
457 ML {* fun annhoare_tac i thm = SUBGOAL (fn (term, _) => |
|
458 (AnnHoareRuleTac i)) i thm |
|
459 |
|
460 fun interfree_aux_tac i thm = SUBGOAL (fn (term, _) => |
|
461 (interfree_aux_Tac i)) i thm |
|
462 *} |
|
463 |
|
464 text {* The so defined ML tactics are then ``exported'' to be used in |
|
465 Isabelle proofs. *} |
|
466 |
|
467 method_setup oghoare = {* |
|
468 Method.no_args |
|
469 (Method.SIMPLE_METHOD' HEADGOAL (oghoare_tac)) *} |
|
470 "verification condition generator for the oghoare logic" |
|
471 |
|
472 method_setup annhoare = {* |
|
473 Method.no_args |
|
474 (Method.SIMPLE_METHOD' HEADGOAL (annhoare_tac)) *} |
|
475 "verification condition generator for the ann_hoare logic" |
|
476 |
|
477 method_setup interfree_aux = {* |
|
478 Method.no_args |
|
479 (Method.SIMPLE_METHOD' HEADGOAL (interfree_aux_tac)) *} |
|
480 "verification condition generator for interference freedom tests" |
|
481 |
|
482 text {* Tactics useful for dealing with the generated verification conditions: *} |
|
483 |
|
484 method_setup conjI_tac = {* |
|
485 Method.no_args |
|
486 (Method.SIMPLE_METHOD' HEADGOAL (conjI_Tac (K all_tac))) *} |
|
487 "verification condition generator for interference freedom tests" |
|
488 |
|
489 ML {* |
|
490 fun disjE_Tac tac i st = st |> |
|
491 ( (EVERY [etac disjE i, |
|
492 disjE_Tac tac (i+1), |
|
493 tac i]) ORELSE (tac i) ) |
|
494 *} |
|
495 |
|
496 method_setup disjE_tac = {* |
|
497 Method.no_args |
|
498 (Method.SIMPLE_METHOD' HEADGOAL (disjE_Tac (K all_tac))) *} |
|
499 "verification condition generator for interference freedom tests" |
|
500 |
|
501 end |