|
1 |
|
2 header {* \section{The Proof System} *} |
|
3 |
|
4 theory OG_Hoare = OG_Tran: |
|
5 |
|
6 consts assertions :: "'a ann_com \<Rightarrow> ('a assn) set" |
|
7 primrec |
|
8 "assertions (AnnBasic r f) = {r}" |
|
9 "assertions (AnnSeq c1 c2) = assertions c1 \<union> assertions c2" |
|
10 "assertions (AnnCond1 r b c1 c2) = {r} \<union> assertions c1 \<union> assertions c2" |
|
11 "assertions (AnnCond2 r b c) = {r} \<union> assertions c" |
|
12 "assertions (AnnWhile r b i c) = {r, i} \<union> assertions c" |
|
13 "assertions (AnnAwait r b c) = {r}" |
|
14 |
|
15 consts atomics :: "'a ann_com \<Rightarrow> ('a assn \<times> 'a com) set" |
|
16 primrec |
|
17 "atomics (AnnBasic r f) = {(r, Basic f)}" |
|
18 "atomics (AnnSeq c1 c2) = atomics c1 \<union> atomics c2" |
|
19 "atomics (AnnCond1 r b c1 c2) = atomics c1 \<union> atomics c2" |
|
20 "atomics (AnnCond2 r b c) = atomics c" |
|
21 "atomics (AnnWhile r b i c) = atomics c" |
|
22 "atomics (AnnAwait r b c) = {(r \<inter> b, c)}" |
|
23 |
|
24 consts com :: "'a ann_triple_op \<Rightarrow> 'a ann_com_op" |
|
25 primrec "com (c, q) = c" |
|
26 |
|
27 consts post :: "'a ann_triple_op \<Rightarrow> 'a assn" |
|
28 primrec "post (c, q) = q" |
|
29 |
|
30 constdefs interfree_aux :: "('a ann_com_op \<times> 'a assn \<times> 'a ann_com_op) \<Rightarrow> bool" |
|
31 "interfree_aux \<equiv> \<lambda>(co, q, co'). co'= None \<or> |
|
32 (\<forall>(r,a) \<in> atomics (the co'). \<parallel>= (q \<inter> r) a q \<and> |
|
33 (co = None \<or> (\<forall>p \<in> assertions (the co). \<parallel>= (p \<inter> r) a p)))" |
|
34 |
|
35 constdefs interfree :: "(('a ann_triple_op) list) \<Rightarrow> bool" |
|
36 "interfree Ts \<equiv> \<forall>i j. i < length Ts \<and> j < length Ts \<and> i \<noteq> j \<longrightarrow> |
|
37 interfree_aux (com (Ts!i), post (Ts!i), com (Ts!j)) " |
|
38 |
|
39 consts ann_hoare :: "('a ann_com \<times> 'a assn) set" |
|
40 syntax "_ann_hoare" :: "'a ann_com \<Rightarrow> 'a assn \<Rightarrow> bool" ("(2\<turnstile> _// _)" [60,90] 45) |
|
41 translations "\<turnstile> c q" \<rightleftharpoons> "(c, q) \<in> ann_hoare" |
|
42 |
|
43 consts oghoare :: "('a assn \<times> 'a com \<times> 'a assn) set" |
|
44 syntax "_oghoare" :: "'a assn \<Rightarrow> 'a com \<Rightarrow> 'a assn \<Rightarrow> bool" ("(3\<parallel>- _//_//_)" [90,55,90] 50) |
|
45 translations "\<parallel>- p c q" \<rightleftharpoons> "(p, c, q) \<in> oghoare" |
|
46 |
|
47 inductive oghoare ann_hoare |
|
48 intros |
|
49 AnnBasic: "r \<subseteq> {s. f s \<in> q} \<Longrightarrow> \<turnstile> (AnnBasic r f) q" |
|
50 |
|
51 AnnSeq: "\<lbrakk> \<turnstile> c0 pre c1; \<turnstile> c1 q \<rbrakk> \<Longrightarrow> \<turnstile> (AnnSeq c0 c1) q" |
|
52 |
|
53 AnnCond1: "\<lbrakk> r \<inter> b \<subseteq> pre c1; \<turnstile> c1 q; r \<inter> -b \<subseteq> pre c2; \<turnstile> c2 q\<rbrakk> |
|
54 \<Longrightarrow> \<turnstile> (AnnCond1 r b c1 c2) q" |
|
55 AnnCond2: "\<lbrakk> r \<inter> b \<subseteq> pre c; \<turnstile> c q; r \<inter> -b \<subseteq> q \<rbrakk> \<Longrightarrow> \<turnstile> (AnnCond2 r b c) q" |
|
56 |
|
57 AnnWhile: "\<lbrakk> r \<subseteq> i; i \<inter> b \<subseteq> pre c; \<turnstile> c i; i \<inter> -b \<subseteq> q \<rbrakk> |
|
58 \<Longrightarrow> \<turnstile> (AnnWhile r b i c) q" |
|
59 |
|
60 AnnAwait: "\<lbrakk> atom_com c; \<parallel>- (r \<inter> b) c q \<rbrakk> \<Longrightarrow> \<turnstile> (AnnAwait r b c) q" |
|
61 |
|
62 AnnConseq: "\<lbrakk>\<turnstile> c q; q \<subseteq> q' \<rbrakk> \<Longrightarrow> \<turnstile> c q'" |
|
63 |
|
64 |
|
65 Parallel: "\<lbrakk> \<forall>i<length Ts. \<exists>c q. Ts!i = (Some c, q) \<and> \<turnstile> c q; interfree Ts \<rbrakk> |
|
66 \<Longrightarrow> \<parallel>- (\<Inter>i\<in>{i. i<length Ts}. pre(the(com(Ts!i)))) |
|
67 Parallel Ts |
|
68 (\<Inter>i\<in>{i. i<length Ts}. post(Ts!i))" |
|
69 |
|
70 Basic: "\<parallel>- {s. f s \<in>q} (Basic f) q" |
|
71 |
|
72 Seq: "\<lbrakk> \<parallel>- p c1 r; \<parallel>- r c2 q \<rbrakk> \<Longrightarrow> \<parallel>- p (Seq c1 c2) q " |
|
73 |
|
74 Cond: "\<lbrakk> \<parallel>- (p \<inter> b) c1 q; \<parallel>- (p \<inter> -b) c2 q \<rbrakk> \<Longrightarrow> \<parallel>- p (Cond b c1 c2) q" |
|
75 |
|
76 While: "\<lbrakk> \<parallel>- (p \<inter> b) c p \<rbrakk> \<Longrightarrow> \<parallel>- p (While b i c) (p \<inter> -b)" |
|
77 |
|
78 Conseq: "\<lbrakk> p' \<subseteq> p; \<parallel>- p c q ; q \<subseteq> q' \<rbrakk> \<Longrightarrow> \<parallel>- p' c q'" |
|
79 |
|
80 section {* Soundness *} |
|
81 (* In the version Isabelle-10-Sep-1999: HOL: The THEN and ELSE |
|
82 parts of conditional expressions (if P then x else y) are no longer |
|
83 simplified. (This allows the simplifier to unfold recursive |
|
84 functional programs.) To restore the old behaviour, we declare |
|
85 @{text "lemmas [cong del] = if_weak_cong"}. *) |
|
86 |
|
87 lemmas [cong del] = if_weak_cong |
|
88 |
|
89 lemmas ann_hoare_induct = oghoare_ann_hoare.induct [THEN conjunct2] |
|
90 lemmas oghoare_induct = oghoare_ann_hoare.induct [THEN conjunct1] |
|
91 |
|
92 lemmas AnnBasic = oghoare_ann_hoare.AnnBasic |
|
93 lemmas AnnSeq = oghoare_ann_hoare.AnnSeq |
|
94 lemmas AnnCond1 = oghoare_ann_hoare.AnnCond1 |
|
95 lemmas AnnCond2 = oghoare_ann_hoare.AnnCond2 |
|
96 lemmas AnnWhile = oghoare_ann_hoare.AnnWhile |
|
97 lemmas AnnAwait = oghoare_ann_hoare.AnnAwait |
|
98 lemmas AnnConseq = oghoare_ann_hoare.AnnConseq |
|
99 |
|
100 lemmas Parallel = oghoare_ann_hoare.Parallel |
|
101 lemmas Basic = oghoare_ann_hoare.Basic |
|
102 lemmas Seq = oghoare_ann_hoare.Seq |
|
103 lemmas Cond = oghoare_ann_hoare.Cond |
|
104 lemmas While = oghoare_ann_hoare.While |
|
105 lemmas Conseq = oghoare_ann_hoare.Conseq |
|
106 |
|
107 subsection {* Soundness of the System for Atomic Programs *} |
|
108 |
|
109 lemma Basic_ntran [rule_format]: |
|
110 "(Basic f, s) -Pn\<rightarrow> (Parallel Ts, t) \<longrightarrow> All_None Ts \<longrightarrow> t = f s" |
|
111 apply(induct "n") |
|
112 apply(simp (no_asm)) |
|
113 apply(fast dest: rel_pow_Suc_D2 Parallel_empty_lemma elim: transition_cases) |
|
114 done |
|
115 |
|
116 lemma SEM_fwhile: "SEM S (p \<inter> b) \<subseteq> p \<Longrightarrow> SEM (fwhile b S k) p \<subseteq> (p \<inter> -b)" |
|
117 apply (induct "k") |
|
118 apply(simp (no_asm) add: L3_5v_lemma3) |
|
119 apply(simp (no_asm) add: L3_5iv L3_5ii Parallel_empty) |
|
120 apply(rule Un_least) |
|
121 apply(rule subset_trans) |
|
122 prefer 2 apply simp |
|
123 apply(erule L3_5i) |
|
124 apply(simp add: SEM_def sem_def id_def) |
|
125 apply clarify |
|
126 apply(drule rtrancl_imp_UN_rel_pow) |
|
127 apply clarify |
|
128 apply(drule Basic_ntran) |
|
129 apply fast+ |
|
130 done |
|
131 |
|
132 lemma atom_hoare_sound [rule_format (no_asm)]: |
|
133 " \<parallel>- p c q \<longrightarrow> atom_com(c) \<longrightarrow> \<parallel>= p c q" |
|
134 apply (unfold com_validity_def) |
|
135 apply(rule oghoare_induct) |
|
136 apply simp_all |
|
137 --{*Basic*} |
|
138 apply(simp add: SEM_def sem_def) |
|
139 apply(fast dest: rtrancl_imp_UN_rel_pow Basic_ntran) |
|
140 --{* Seq *} |
|
141 apply(rule impI) |
|
142 apply(rule subset_trans) |
|
143 prefer 2 apply simp |
|
144 apply(simp add: L3_5ii L3_5i) |
|
145 --{* Cond *} |
|
146 apply(rule impI) |
|
147 apply(simp add: L3_5iv) |
|
148 apply(erule Un_least) |
|
149 apply assumption |
|
150 --{* While *} |
|
151 apply(rule impI) |
|
152 apply(simp add: L3_5v) |
|
153 apply(rule UN_least) |
|
154 apply(drule SEM_fwhile) |
|
155 apply assumption |
|
156 --{* Conseq *} |
|
157 apply(simp add: SEM_def sem_def) |
|
158 apply force |
|
159 done |
|
160 |
|
161 subsection {* Soundness of the System for Component Programs *} |
|
162 |
|
163 inductive_cases ann_transition_cases: |
|
164 "(None,s) -1\<rightarrow> t" |
|
165 "(Some (AnnBasic r f),s) -1\<rightarrow> t" |
|
166 "(Some (AnnSeq c1 c2), s) -1\<rightarrow> t" |
|
167 "(Some (AnnCond1 r b c1 c2), s) -1\<rightarrow> t" |
|
168 "(Some (AnnCond2 r b c), s) -1\<rightarrow> t" |
|
169 "(Some (AnnWhile r b I c), s) -1\<rightarrow> t" |
|
170 "(Some (AnnAwait r b c),s) -1\<rightarrow> t" |
|
171 |
|
172 text {* Strong Soundness for Component Programs:*} |
|
173 |
|
174 lemma ann_hoare_case_analysis [rule_format]: "\<turnstile> C q' \<longrightarrow> |
|
175 ((\<forall>r f. C = AnnBasic r f \<longrightarrow> (\<exists>q. r \<subseteq> {s. f s \<in> q} \<and> q \<subseteq> q')) \<and> |
|
176 (\<forall>c0 c1. C = AnnSeq c0 c1 \<longrightarrow> (\<exists>q. q \<subseteq> q' \<and> \<turnstile> c0 pre c1 \<and> \<turnstile> c1 q)) \<and> |
|
177 (\<forall>r b c1 c2. C = AnnCond1 r b c1 c2 \<longrightarrow> (\<exists>q. q \<subseteq> q' \<and> |
|
178 r \<inter> b \<subseteq> pre c1 \<and> \<turnstile> c1 q \<and> r \<inter> -b \<subseteq> pre c2 \<and> \<turnstile> c2 q)) \<and> |
|
179 (\<forall>r b c. C = AnnCond2 r b c \<longrightarrow> |
|
180 (\<exists>q. q \<subseteq> q' \<and> r \<inter> b \<subseteq> pre c \<and> \<turnstile> c q \<and> r \<inter> -b \<subseteq> q)) \<and> |
|
181 (\<forall>r i b c. C = AnnWhile r b i c \<longrightarrow> |
|
182 (\<exists>q. q \<subseteq> q' \<and> r \<subseteq> i \<and> i \<inter> b \<subseteq> pre c \<and> \<turnstile> c i \<and> i \<inter> -b \<subseteq> q)) \<and> |
|
183 (\<forall>r b c. C = AnnAwait r b c \<longrightarrow> (\<exists>q. q \<subseteq> q' \<and> \<parallel>- (r \<inter> b) c q)))" |
|
184 apply(rule ann_hoare_induct) |
|
185 apply simp_all |
|
186 apply(rule_tac x=q in exI,simp)+ |
|
187 apply(rule conjI,clarify,simp,clarify,rule_tac x=qa in exI,fast)+ |
|
188 apply(clarify,simp,clarify,rule_tac x=qa in exI,fast) |
|
189 done |
|
190 |
|
191 lemma Help: "(transition \<inter> {(v,v,u). True}) = (transition)" |
|
192 apply force |
|
193 done |
|
194 |
|
195 lemma Strong_Soundness_aux_aux [rule_format]: |
|
196 "(co, s) -1\<rightarrow> (co', t) \<longrightarrow> (\<forall>c. co = Some c \<longrightarrow> s\<in> pre c \<longrightarrow> |
|
197 (\<forall>q. \<turnstile> c q \<longrightarrow> (if co' = None then t\<in>q else t \<in> pre(the co') \<and> \<turnstile> (the co') q )))" |
|
198 apply(rule ann_transition_transition.induct [THEN conjunct1]) |
|
199 apply simp_all |
|
200 --{* Basic *} |
|
201 apply clarify |
|
202 apply(frule ann_hoare_case_analysis) |
|
203 apply force |
|
204 --{* Seq *} |
|
205 apply clarify |
|
206 apply(frule ann_hoare_case_analysis,simp) |
|
207 apply(fast intro: AnnConseq) |
|
208 apply clarify |
|
209 apply(frule ann_hoare_case_analysis,simp) |
|
210 apply clarify |
|
211 apply(rule conjI) |
|
212 apply force |
|
213 apply(rule AnnSeq,simp) |
|
214 apply(fast intro: AnnConseq) |
|
215 --{* Cond1 *} |
|
216 apply clarify |
|
217 apply(frule ann_hoare_case_analysis,simp) |
|
218 apply(fast intro: AnnConseq) |
|
219 apply clarify |
|
220 apply(frule ann_hoare_case_analysis,simp) |
|
221 apply(fast intro: AnnConseq) |
|
222 --{* Cond2 *} |
|
223 apply clarify |
|
224 apply(frule ann_hoare_case_analysis,simp) |
|
225 apply(fast intro: AnnConseq) |
|
226 apply clarify |
|
227 apply(frule ann_hoare_case_analysis,simp) |
|
228 apply(fast intro: AnnConseq) |
|
229 --{* While *} |
|
230 apply clarify |
|
231 apply(frule ann_hoare_case_analysis,simp) |
|
232 apply force |
|
233 apply clarify |
|
234 apply(frule ann_hoare_case_analysis,simp) |
|
235 apply auto |
|
236 apply(rule AnnSeq) |
|
237 apply simp |
|
238 apply(rule AnnWhile) |
|
239 apply simp_all |
|
240 apply(fast) |
|
241 --{* Await *} |
|
242 apply(frule ann_hoare_case_analysis,simp) |
|
243 apply clarify |
|
244 apply(drule atom_hoare_sound) |
|
245 apply simp |
|
246 apply(simp add: com_validity_def SEM_def sem_def) |
|
247 apply(simp add: Help All_None_def) |
|
248 apply force |
|
249 done |
|
250 |
|
251 lemma Strong_Soundness_aux: "\<lbrakk> (Some c, s) -*\<rightarrow> (co, t); s \<in> pre c; \<turnstile> c q \<rbrakk> |
|
252 \<Longrightarrow> if co = None then t \<in> q else t \<in> pre (the co) \<and> \<turnstile> (the co) q" |
|
253 apply(erule rtrancl_induct2) |
|
254 apply simp |
|
255 apply(case_tac "a") |
|
256 apply(fast elim: ann_transition_cases) |
|
257 apply(erule Strong_Soundness_aux_aux) |
|
258 apply simp |
|
259 apply simp_all |
|
260 done |
|
261 |
|
262 lemma Strong_Soundness: "\<lbrakk> (Some c, s)-*\<rightarrow>(co, t); s \<in> pre c; \<turnstile> c q \<rbrakk> |
|
263 \<Longrightarrow> if co = None then t\<in>q else t \<in> pre (the co)" |
|
264 apply(force dest:Strong_Soundness_aux) |
|
265 done |
|
266 |
|
267 lemma ann_hoare_sound: "\<turnstile> c q \<Longrightarrow> \<Turnstile> c q" |
|
268 apply (unfold ann_com_validity_def ann_SEM_def ann_sem_def) |
|
269 apply clarify |
|
270 apply(drule Strong_Soundness) |
|
271 apply simp_all |
|
272 done |
|
273 |
|
274 subsection {* Soundness of the System for Parallel Programs *} |
|
275 |
|
276 lemma Parallel_length_post_P1: "(Parallel Ts,s) -P1\<rightarrow> (R', t) \<Longrightarrow> |
|
277 (\<exists>Rs. R' = (Parallel Rs) \<and> (length Rs) = (length Ts) \<and> |
|
278 (\<forall>i. i<length Ts \<longrightarrow> post(Rs ! i) = post(Ts ! i)))" |
|
279 apply(erule transition_cases) |
|
280 apply simp |
|
281 apply clarify |
|
282 apply(case_tac "i=ia") |
|
283 apply simp+ |
|
284 done |
|
285 |
|
286 lemma Parallel_length_post_PStar: "(Parallel Ts,s) -P*\<rightarrow> (R',t) \<Longrightarrow> |
|
287 (\<exists>Rs. R' = (Parallel Rs) \<and> (length Rs) = (length Ts) \<and> |
|
288 (\<forall>i. i<length Ts \<longrightarrow> post(Ts ! i) = post(Rs ! i)))" |
|
289 apply(erule rtrancl_induct2) |
|
290 apply(simp_all) |
|
291 apply clarify |
|
292 apply simp |
|
293 apply(drule Parallel_length_post_P1) |
|
294 apply auto |
|
295 done |
|
296 |
|
297 lemma assertions_lemma: "pre c \<in> assertions c" |
|
298 apply(rule ann_com_com.induct [THEN conjunct1]) |
|
299 apply auto |
|
300 done |
|
301 |
|
302 lemma interfree_aux1 [rule_format]: |
|
303 "(c,s) -1\<rightarrow> (r,t) \<longrightarrow> (interfree_aux(c1, q1, c) \<longrightarrow> interfree_aux(c1, q1, r))" |
|
304 apply (rule ann_transition_transition.induct [THEN conjunct1]) |
|
305 apply(safe) |
|
306 prefer 13 |
|
307 apply (rule TrueI) |
|
308 apply (simp_all add:interfree_aux_def) |
|
309 apply force+ |
|
310 done |
|
311 |
|
312 lemma interfree_aux2 [rule_format]: |
|
313 "(c,s) -1\<rightarrow> (r,t) \<longrightarrow> (interfree_aux(c, q, a) \<longrightarrow> interfree_aux(r, q, a) )" |
|
314 apply (rule ann_transition_transition.induct [THEN conjunct1]) |
|
315 apply(force simp add:interfree_aux_def)+ |
|
316 done |
|
317 |
|
318 lemma interfree_lemma: "\<lbrakk> (Some c, s) -1\<rightarrow> (r, t);interfree Ts ; i<length Ts; |
|
319 Ts!i = (Some c, q) \<rbrakk> \<Longrightarrow> interfree (Ts[i:= (r, q)])" |
|
320 apply(simp add: interfree_def) |
|
321 apply clarify |
|
322 apply(case_tac "i=j") |
|
323 apply(drule_tac t = "ia" in not_sym) |
|
324 apply simp_all |
|
325 apply(force elim: interfree_aux1) |
|
326 apply(force elim: interfree_aux2 simp add:nth_list_update) |
|
327 done |
|
328 |
|
329 text {* Strong Soundness Theorem for Parallel Programs:*} |
|
330 |
|
331 lemma Parallel_Strong_Soundness_Seq_aux: |
|
332 "\<lbrakk>interfree Ts; i<length Ts; com(Ts ! i) = Some(AnnSeq c0 c1) \<rbrakk> |
|
333 \<Longrightarrow> interfree (Ts[i:=(Some c0, pre c1)])" |
|
334 apply(simp add: interfree_def) |
|
335 apply clarify |
|
336 apply(case_tac "i=j") |
|
337 apply(force simp add: nth_list_update interfree_aux_def) |
|
338 apply(case_tac "i=ia") |
|
339 apply(erule_tac x=ia in allE) |
|
340 apply(force simp add:interfree_aux_def assertions_lemma) |
|
341 apply simp |
|
342 done |
|
343 |
|
344 lemma Parallel_Strong_Soundness_Seq [rule_format (no_asm)]: |
|
345 "\<lbrakk> \<forall>i<length Ts. (if com(Ts!i) = None then b \<in> post(Ts!i) |
|
346 else b \<in> pre(the(com(Ts!i))) \<and> \<turnstile> the(com(Ts!i)) post(Ts!i)); |
|
347 com(Ts ! i) = Some(AnnSeq c0 c1); i<length Ts; interfree Ts \<rbrakk> \<Longrightarrow> |
|
348 (\<forall>ia<length Ts. (if com(Ts[i:=(Some c0, pre c1)]! ia) = None |
|
349 then b \<in> post(Ts[i:=(Some c0, pre c1)]! ia) |
|
350 else b \<in> pre(the(com(Ts[i:=(Some c0, pre c1)]! ia))) \<and> |
|
351 \<turnstile> the(com(Ts[i:=(Some c0, pre c1)]! ia)) post(Ts[i:=(Some c0, pre c1)]! ia))) |
|
352 \<and> interfree (Ts[i:= (Some c0, pre c1)])" |
|
353 apply(rule conjI) |
|
354 apply safe |
|
355 apply(case_tac "i=ia") |
|
356 apply simp |
|
357 apply(force dest: ann_hoare_case_analysis) |
|
358 apply simp |
|
359 apply(fast elim: Parallel_Strong_Soundness_Seq_aux) |
|
360 done |
|
361 |
|
362 lemma Parallel_Strong_Soundness_aux_aux [rule_format]: |
|
363 "(Some c, b) -1\<rightarrow> (co, t) \<longrightarrow> |
|
364 (\<forall>Ts. i<length Ts \<longrightarrow> com(Ts ! i) = Some c \<longrightarrow> |
|
365 (\<forall>i<length Ts. (if com(Ts ! i) = None then b\<in>post(Ts!i) |
|
366 else b\<in>pre(the(com(Ts!i))) \<and> \<turnstile> the(com(Ts!i)) post(Ts!i))) \<longrightarrow> |
|
367 interfree Ts \<longrightarrow> |
|
368 (\<forall>j. j<length Ts \<and> i\<noteq>j \<longrightarrow> (if com(Ts!j) = None then t\<in>post(Ts!j) |
|
369 else t\<in>pre(the(com(Ts!j))) \<and> \<turnstile> the(com(Ts!j)) post(Ts!j))) )" |
|
370 apply(rule ann_transition_transition.induct [THEN conjunct1]) |
|
371 apply safe |
|
372 prefer 11 |
|
373 apply(rule TrueI) |
|
374 apply simp_all |
|
375 --{* Basic *} |
|
376 apply(erule_tac x = "i" in all_dupE, erule (1) notE impE) |
|
377 apply(erule_tac x = "j" in allE , erule (1) notE impE) |
|
378 apply(simp add: interfree_def) |
|
379 apply(erule_tac x = "j" in allE,simp) |
|
380 apply(erule_tac x = "i" in allE,simp) |
|
381 apply(drule_tac t = "i" in not_sym) |
|
382 apply(case_tac "com(Ts ! j)=None") |
|
383 apply(force intro: converse_rtrancl_into_rtrancl |
|
384 simp add: interfree_aux_def com_validity_def SEM_def sem_def All_None_def) |
|
385 apply(simp add:interfree_aux_def) |
|
386 apply clarify |
|
387 apply simp |
|
388 apply clarify |
|
389 apply(erule_tac x="pre y" in ballE) |
|
390 apply(force intro: converse_rtrancl_into_rtrancl |
|
391 simp add: com_validity_def SEM_def sem_def All_None_def) |
|
392 apply(simp add:assertions_lemma) |
|
393 --{* Seqs *} |
|
394 apply(erule_tac x = "Ts[i:=(Some c0, pre c1)]" in allE) |
|
395 apply(drule Parallel_Strong_Soundness_Seq,simp+) |
|
396 apply(erule_tac x = "Ts[i:=(Some c0, pre c1)]" in allE) |
|
397 apply(drule Parallel_Strong_Soundness_Seq,simp+) |
|
398 --{* Await *} |
|
399 apply(rule_tac x = "i" in allE , assumption , erule (1) notE impE) |
|
400 apply(erule_tac x = "j" in allE , erule (1) notE impE) |
|
401 apply(simp add: interfree_def) |
|
402 apply(erule_tac x = "j" in allE,simp) |
|
403 apply(erule_tac x = "i" in allE,simp) |
|
404 apply(drule_tac t = "i" in not_sym) |
|
405 apply(case_tac "com(Ts ! j)=None") |
|
406 apply(force intro: converse_rtrancl_into_rtrancl simp add: interfree_aux_def |
|
407 com_validity_def SEM_def sem_def All_None_def Help) |
|
408 apply(simp add:interfree_aux_def) |
|
409 apply clarify |
|
410 apply simp |
|
411 apply clarify |
|
412 apply(erule_tac x="pre y" in ballE) |
|
413 apply(force intro: converse_rtrancl_into_rtrancl |
|
414 simp add: com_validity_def SEM_def sem_def All_None_def Help) |
|
415 apply(simp add:assertions_lemma) |
|
416 done |
|
417 |
|
418 lemma Parallel_Strong_Soundness_aux [rule_format]: |
|
419 "\<lbrakk>(Ts',s) -P*\<rightarrow> (Rs',t); Ts' = (Parallel Ts); interfree Ts; |
|
420 \<forall>i. i<length Ts \<longrightarrow> (\<exists>c q. (Ts ! i) = (Some c, q) \<and> s\<in>(pre c) \<and> \<turnstile> c q ) \<rbrakk> \<Longrightarrow> |
|
421 \<forall>Rs. Rs' = (Parallel Rs) \<longrightarrow> (\<forall>j. j<length Rs \<longrightarrow> |
|
422 (if com(Rs ! j) = None then t\<in>post(Ts ! j) |
|
423 else t\<in>pre(the(com(Rs ! j))) \<and> \<turnstile> the(com(Rs ! j)) post(Ts ! j))) \<and> interfree Rs" |
|
424 apply(erule rtrancl_induct2) |
|
425 apply clarify |
|
426 --{* Base *} |
|
427 apply force |
|
428 --{* Induction step *} |
|
429 apply clarify |
|
430 apply(drule Parallel_length_post_PStar) |
|
431 apply clarify |
|
432 apply (ind_cases "(Parallel Ts, s) -P1\<rightarrow> (Parallel Rs, t)") |
|
433 apply(rule conjI) |
|
434 apply clarify |
|
435 apply(case_tac "i=j") |
|
436 apply(simp split del:split_if) |
|
437 apply(erule Strong_Soundness_aux_aux,simp+) |
|
438 apply force |
|
439 apply force |
|
440 apply(simp split del: split_if) |
|
441 apply(erule Parallel_Strong_Soundness_aux_aux) |
|
442 apply(simp_all add: split del:split_if) |
|
443 apply force |
|
444 apply(rule interfree_lemma) |
|
445 apply simp_all |
|
446 done |
|
447 |
|
448 lemma Parallel_Strong_Soundness: |
|
449 "\<lbrakk>(Parallel Ts, s) -P*\<rightarrow> (Parallel Rs, t); interfree Ts; j<length Rs; |
|
450 \<forall>i. i<length Ts \<longrightarrow> (\<exists>c q. Ts ! i = (Some c, q) \<and> s\<in>pre c \<and> \<turnstile> c q) \<rbrakk> \<Longrightarrow> |
|
451 if com(Rs ! j) = None then t\<in>post(Ts ! j) else t\<in>pre (the(com(Rs ! j)))" |
|
452 apply(drule Parallel_Strong_Soundness_aux) |
|
453 apply simp+ |
|
454 done |
|
455 |
|
456 lemma oghoare_sound [rule_format (no_asm)]: "\<parallel>- p c q \<longrightarrow> \<parallel>= p c q" |
|
457 apply (unfold com_validity_def) |
|
458 apply(rule oghoare_induct) |
|
459 apply(rule TrueI)+ |
|
460 --{* Parallel *} |
|
461 apply(simp add: SEM_def sem_def) |
|
462 apply clarify |
|
463 apply(frule Parallel_length_post_PStar) |
|
464 apply clarify |
|
465 apply(drule_tac j=i in Parallel_Strong_Soundness) |
|
466 apply clarify |
|
467 apply simp |
|
468 apply force |
|
469 apply simp |
|
470 apply(erule_tac V = "\<forall>i. ?P i" in thin_rl) |
|
471 apply(drule_tac s = "length Rs" in sym) |
|
472 apply(erule allE, erule impE, assumption) |
|
473 apply(force dest: nth_mem simp add: All_None_def) |
|
474 --{* Basic *} |
|
475 apply(simp add: SEM_def sem_def) |
|
476 apply(force dest: rtrancl_imp_UN_rel_pow Basic_ntran) |
|
477 --{* Seq *} |
|
478 apply(rule subset_trans) |
|
479 prefer 2 apply assumption |
|
480 apply(simp add: L3_5ii L3_5i) |
|
481 --{* Cond *} |
|
482 apply(simp add: L3_5iv) |
|
483 apply(erule Un_least) |
|
484 apply assumption |
|
485 --{* While *} |
|
486 apply(simp add: L3_5v) |
|
487 apply(rule UN_least) |
|
488 apply(drule SEM_fwhile) |
|
489 apply assumption |
|
490 --{* Conseq *} |
|
491 apply(simp add: SEM_def sem_def) |
|
492 apply auto |
|
493 done |
|
494 |
|
495 end |