13020
|
1 |
|
|
2 |
header {* \section{The Proof System} *}
|
|
3 |
|
16417
|
4 |
theory OG_Hoare imports OG_Tran begin
|
13020
|
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)
|
15102
|
120 |
apply(rule conjI)
|
|
121 |
apply (blast dest: L3_5i)
|
13020
|
122 |
apply(simp add: SEM_def sem_def id_def)
|
15102
|
123 |
apply (blast dest: Basic_ntran rtrancl_imp_UN_rel_pow)
|
13020
|
124 |
done
|
|
125 |
|
15102
|
126 |
lemma atom_hoare_sound [rule_format]:
|
13020
|
127 |
" \<parallel>- p c q \<longrightarrow> atom_com(c) \<longrightarrow> \<parallel>= p c q"
|
|
128 |
apply (unfold com_validity_def)
|
|
129 |
apply(rule oghoare_induct)
|
|
130 |
apply simp_all
|
|
131 |
--{*Basic*}
|
|
132 |
apply(simp add: SEM_def sem_def)
|
|
133 |
apply(fast dest: rtrancl_imp_UN_rel_pow Basic_ntran)
|
|
134 |
--{* Seq *}
|
|
135 |
apply(rule impI)
|
|
136 |
apply(rule subset_trans)
|
|
137 |
prefer 2 apply simp
|
|
138 |
apply(simp add: L3_5ii L3_5i)
|
|
139 |
--{* Cond *}
|
|
140 |
apply(simp add: L3_5iv)
|
|
141 |
--{* While *}
|
15102
|
142 |
apply (force simp add: L3_5v dest: SEM_fwhile)
|
13020
|
143 |
--{* Conseq *}
|
15102
|
144 |
apply(force simp add: SEM_def sem_def)
|
13020
|
145 |
done
|
|
146 |
|
|
147 |
subsection {* Soundness of the System for Component Programs *}
|
|
148 |
|
|
149 |
inductive_cases ann_transition_cases:
|
|
150 |
"(None,s) -1\<rightarrow> t"
|
|
151 |
"(Some (AnnBasic r f),s) -1\<rightarrow> t"
|
|
152 |
"(Some (AnnSeq c1 c2), s) -1\<rightarrow> t"
|
|
153 |
"(Some (AnnCond1 r b c1 c2), s) -1\<rightarrow> t"
|
|
154 |
"(Some (AnnCond2 r b c), s) -1\<rightarrow> t"
|
|
155 |
"(Some (AnnWhile r b I c), s) -1\<rightarrow> t"
|
|
156 |
"(Some (AnnAwait r b c),s) -1\<rightarrow> t"
|
|
157 |
|
|
158 |
text {* Strong Soundness for Component Programs:*}
|
|
159 |
|
|
160 |
lemma ann_hoare_case_analysis [rule_format]: "\<turnstile> C q' \<longrightarrow>
|
|
161 |
((\<forall>r f. C = AnnBasic r f \<longrightarrow> (\<exists>q. r \<subseteq> {s. f s \<in> q} \<and> q \<subseteq> q')) \<and>
|
|
162 |
(\<forall>c0 c1. C = AnnSeq c0 c1 \<longrightarrow> (\<exists>q. q \<subseteq> q' \<and> \<turnstile> c0 pre c1 \<and> \<turnstile> c1 q)) \<and>
|
|
163 |
(\<forall>r b c1 c2. C = AnnCond1 r b c1 c2 \<longrightarrow> (\<exists>q. q \<subseteq> q' \<and>
|
|
164 |
r \<inter> b \<subseteq> pre c1 \<and> \<turnstile> c1 q \<and> r \<inter> -b \<subseteq> pre c2 \<and> \<turnstile> c2 q)) \<and>
|
|
165 |
(\<forall>r b c. C = AnnCond2 r b c \<longrightarrow>
|
|
166 |
(\<exists>q. q \<subseteq> q' \<and> r \<inter> b \<subseteq> pre c \<and> \<turnstile> c q \<and> r \<inter> -b \<subseteq> q)) \<and>
|
|
167 |
(\<forall>r i b c. C = AnnWhile r b i c \<longrightarrow>
|
|
168 |
(\<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>
|
|
169 |
(\<forall>r b c. C = AnnAwait r b c \<longrightarrow> (\<exists>q. q \<subseteq> q' \<and> \<parallel>- (r \<inter> b) c q)))"
|
|
170 |
apply(rule ann_hoare_induct)
|
|
171 |
apply simp_all
|
|
172 |
apply(rule_tac x=q in exI,simp)+
|
|
173 |
apply(rule conjI,clarify,simp,clarify,rule_tac x=qa in exI,fast)+
|
|
174 |
apply(clarify,simp,clarify,rule_tac x=qa in exI,fast)
|
|
175 |
done
|
|
176 |
|
|
177 |
lemma Help: "(transition \<inter> {(v,v,u). True}) = (transition)"
|
|
178 |
apply force
|
|
179 |
done
|
|
180 |
|
|
181 |
lemma Strong_Soundness_aux_aux [rule_format]:
|
|
182 |
"(co, s) -1\<rightarrow> (co', t) \<longrightarrow> (\<forall>c. co = Some c \<longrightarrow> s\<in> pre c \<longrightarrow>
|
|
183 |
(\<forall>q. \<turnstile> c q \<longrightarrow> (if co' = None then t\<in>q else t \<in> pre(the co') \<and> \<turnstile> (the co') q )))"
|
|
184 |
apply(rule ann_transition_transition.induct [THEN conjunct1])
|
|
185 |
apply simp_all
|
|
186 |
--{* Basic *}
|
|
187 |
apply clarify
|
|
188 |
apply(frule ann_hoare_case_analysis)
|
|
189 |
apply force
|
|
190 |
--{* Seq *}
|
|
191 |
apply clarify
|
|
192 |
apply(frule ann_hoare_case_analysis,simp)
|
|
193 |
apply(fast intro: AnnConseq)
|
|
194 |
apply clarify
|
|
195 |
apply(frule ann_hoare_case_analysis,simp)
|
|
196 |
apply clarify
|
|
197 |
apply(rule conjI)
|
|
198 |
apply force
|
|
199 |
apply(rule AnnSeq,simp)
|
|
200 |
apply(fast intro: AnnConseq)
|
|
201 |
--{* Cond1 *}
|
|
202 |
apply clarify
|
|
203 |
apply(frule ann_hoare_case_analysis,simp)
|
|
204 |
apply(fast intro: AnnConseq)
|
|
205 |
apply clarify
|
|
206 |
apply(frule ann_hoare_case_analysis,simp)
|
|
207 |
apply(fast intro: AnnConseq)
|
|
208 |
--{* Cond2 *}
|
|
209 |
apply clarify
|
|
210 |
apply(frule ann_hoare_case_analysis,simp)
|
|
211 |
apply(fast intro: AnnConseq)
|
|
212 |
apply clarify
|
|
213 |
apply(frule ann_hoare_case_analysis,simp)
|
|
214 |
apply(fast intro: AnnConseq)
|
|
215 |
--{* While *}
|
|
216 |
apply clarify
|
|
217 |
apply(frule ann_hoare_case_analysis,simp)
|
|
218 |
apply force
|
|
219 |
apply clarify
|
|
220 |
apply(frule ann_hoare_case_analysis,simp)
|
|
221 |
apply auto
|
|
222 |
apply(rule AnnSeq)
|
|
223 |
apply simp
|
|
224 |
apply(rule AnnWhile)
|
|
225 |
apply simp_all
|
|
226 |
--{* Await *}
|
|
227 |
apply(frule ann_hoare_case_analysis,simp)
|
|
228 |
apply clarify
|
|
229 |
apply(drule atom_hoare_sound)
|
|
230 |
apply simp
|
|
231 |
apply(simp add: com_validity_def SEM_def sem_def)
|
|
232 |
apply(simp add: Help All_None_def)
|
|
233 |
apply force
|
|
234 |
done
|
|
235 |
|
|
236 |
lemma Strong_Soundness_aux: "\<lbrakk> (Some c, s) -*\<rightarrow> (co, t); s \<in> pre c; \<turnstile> c q \<rbrakk>
|
|
237 |
\<Longrightarrow> if co = None then t \<in> q else t \<in> pre (the co) \<and> \<turnstile> (the co) q"
|
|
238 |
apply(erule rtrancl_induct2)
|
|
239 |
apply simp
|
|
240 |
apply(case_tac "a")
|
|
241 |
apply(fast elim: ann_transition_cases)
|
|
242 |
apply(erule Strong_Soundness_aux_aux)
|
|
243 |
apply simp
|
|
244 |
apply simp_all
|
|
245 |
done
|
|
246 |
|
|
247 |
lemma Strong_Soundness: "\<lbrakk> (Some c, s)-*\<rightarrow>(co, t); s \<in> pre c; \<turnstile> c q \<rbrakk>
|
|
248 |
\<Longrightarrow> if co = None then t\<in>q else t \<in> pre (the co)"
|
|
249 |
apply(force dest:Strong_Soundness_aux)
|
|
250 |
done
|
|
251 |
|
|
252 |
lemma ann_hoare_sound: "\<turnstile> c q \<Longrightarrow> \<Turnstile> c q"
|
|
253 |
apply (unfold ann_com_validity_def ann_SEM_def ann_sem_def)
|
|
254 |
apply clarify
|
|
255 |
apply(drule Strong_Soundness)
|
|
256 |
apply simp_all
|
|
257 |
done
|
|
258 |
|
|
259 |
subsection {* Soundness of the System for Parallel Programs *}
|
|
260 |
|
|
261 |
lemma Parallel_length_post_P1: "(Parallel Ts,s) -P1\<rightarrow> (R', t) \<Longrightarrow>
|
|
262 |
(\<exists>Rs. R' = (Parallel Rs) \<and> (length Rs) = (length Ts) \<and>
|
|
263 |
(\<forall>i. i<length Ts \<longrightarrow> post(Rs ! i) = post(Ts ! i)))"
|
|
264 |
apply(erule transition_cases)
|
|
265 |
apply simp
|
|
266 |
apply clarify
|
|
267 |
apply(case_tac "i=ia")
|
|
268 |
apply simp+
|
|
269 |
done
|
|
270 |
|
|
271 |
lemma Parallel_length_post_PStar: "(Parallel Ts,s) -P*\<rightarrow> (R',t) \<Longrightarrow>
|
|
272 |
(\<exists>Rs. R' = (Parallel Rs) \<and> (length Rs) = (length Ts) \<and>
|
|
273 |
(\<forall>i. i<length Ts \<longrightarrow> post(Ts ! i) = post(Rs ! i)))"
|
|
274 |
apply(erule rtrancl_induct2)
|
|
275 |
apply(simp_all)
|
|
276 |
apply clarify
|
|
277 |
apply simp
|
|
278 |
apply(drule Parallel_length_post_P1)
|
|
279 |
apply auto
|
|
280 |
done
|
|
281 |
|
|
282 |
lemma assertions_lemma: "pre c \<in> assertions c"
|
|
283 |
apply(rule ann_com_com.induct [THEN conjunct1])
|
|
284 |
apply auto
|
|
285 |
done
|
|
286 |
|
|
287 |
lemma interfree_aux1 [rule_format]:
|
|
288 |
"(c,s) -1\<rightarrow> (r,t) \<longrightarrow> (interfree_aux(c1, q1, c) \<longrightarrow> interfree_aux(c1, q1, r))"
|
|
289 |
apply (rule ann_transition_transition.induct [THEN conjunct1])
|
|
290 |
apply(safe)
|
|
291 |
prefer 13
|
|
292 |
apply (rule TrueI)
|
|
293 |
apply (simp_all add:interfree_aux_def)
|
|
294 |
apply force+
|
|
295 |
done
|
|
296 |
|
|
297 |
lemma interfree_aux2 [rule_format]:
|
|
298 |
"(c,s) -1\<rightarrow> (r,t) \<longrightarrow> (interfree_aux(c, q, a) \<longrightarrow> interfree_aux(r, q, a) )"
|
|
299 |
apply (rule ann_transition_transition.induct [THEN conjunct1])
|
|
300 |
apply(force simp add:interfree_aux_def)+
|
|
301 |
done
|
|
302 |
|
|
303 |
lemma interfree_lemma: "\<lbrakk> (Some c, s) -1\<rightarrow> (r, t);interfree Ts ; i<length Ts;
|
|
304 |
Ts!i = (Some c, q) \<rbrakk> \<Longrightarrow> interfree (Ts[i:= (r, q)])"
|
|
305 |
apply(simp add: interfree_def)
|
|
306 |
apply clarify
|
|
307 |
apply(case_tac "i=j")
|
|
308 |
apply(drule_tac t = "ia" in not_sym)
|
|
309 |
apply simp_all
|
|
310 |
apply(force elim: interfree_aux1)
|
|
311 |
apply(force elim: interfree_aux2 simp add:nth_list_update)
|
|
312 |
done
|
|
313 |
|
|
314 |
text {* Strong Soundness Theorem for Parallel Programs:*}
|
|
315 |
|
|
316 |
lemma Parallel_Strong_Soundness_Seq_aux:
|
|
317 |
"\<lbrakk>interfree Ts; i<length Ts; com(Ts ! i) = Some(AnnSeq c0 c1) \<rbrakk>
|
|
318 |
\<Longrightarrow> interfree (Ts[i:=(Some c0, pre c1)])"
|
|
319 |
apply(simp add: interfree_def)
|
|
320 |
apply clarify
|
|
321 |
apply(case_tac "i=j")
|
|
322 |
apply(force simp add: nth_list_update interfree_aux_def)
|
|
323 |
apply(case_tac "i=ia")
|
|
324 |
apply(erule_tac x=ia in allE)
|
|
325 |
apply(force simp add:interfree_aux_def assertions_lemma)
|
|
326 |
apply simp
|
|
327 |
done
|
|
328 |
|
|
329 |
lemma Parallel_Strong_Soundness_Seq [rule_format (no_asm)]:
|
|
330 |
"\<lbrakk> \<forall>i<length Ts. (if com(Ts!i) = None then b \<in> post(Ts!i)
|
|
331 |
else b \<in> pre(the(com(Ts!i))) \<and> \<turnstile> the(com(Ts!i)) post(Ts!i));
|
|
332 |
com(Ts ! i) = Some(AnnSeq c0 c1); i<length Ts; interfree Ts \<rbrakk> \<Longrightarrow>
|
|
333 |
(\<forall>ia<length Ts. (if com(Ts[i:=(Some c0, pre c1)]! ia) = None
|
|
334 |
then b \<in> post(Ts[i:=(Some c0, pre c1)]! ia)
|
|
335 |
else b \<in> pre(the(com(Ts[i:=(Some c0, pre c1)]! ia))) \<and>
|
|
336 |
\<turnstile> the(com(Ts[i:=(Some c0, pre c1)]! ia)) post(Ts[i:=(Some c0, pre c1)]! ia)))
|
|
337 |
\<and> interfree (Ts[i:= (Some c0, pre c1)])"
|
|
338 |
apply(rule conjI)
|
|
339 |
apply safe
|
|
340 |
apply(case_tac "i=ia")
|
|
341 |
apply simp
|
|
342 |
apply(force dest: ann_hoare_case_analysis)
|
|
343 |
apply simp
|
|
344 |
apply(fast elim: Parallel_Strong_Soundness_Seq_aux)
|
|
345 |
done
|
|
346 |
|
|
347 |
lemma Parallel_Strong_Soundness_aux_aux [rule_format]:
|
|
348 |
"(Some c, b) -1\<rightarrow> (co, t) \<longrightarrow>
|
|
349 |
(\<forall>Ts. i<length Ts \<longrightarrow> com(Ts ! i) = Some c \<longrightarrow>
|
|
350 |
(\<forall>i<length Ts. (if com(Ts ! i) = None then b\<in>post(Ts!i)
|
|
351 |
else b\<in>pre(the(com(Ts!i))) \<and> \<turnstile> the(com(Ts!i)) post(Ts!i))) \<longrightarrow>
|
|
352 |
interfree Ts \<longrightarrow>
|
|
353 |
(\<forall>j. j<length Ts \<and> i\<noteq>j \<longrightarrow> (if com(Ts!j) = None then t\<in>post(Ts!j)
|
|
354 |
else t\<in>pre(the(com(Ts!j))) \<and> \<turnstile> the(com(Ts!j)) post(Ts!j))) )"
|
|
355 |
apply(rule ann_transition_transition.induct [THEN conjunct1])
|
|
356 |
apply safe
|
|
357 |
prefer 11
|
|
358 |
apply(rule TrueI)
|
|
359 |
apply simp_all
|
|
360 |
--{* Basic *}
|
|
361 |
apply(erule_tac x = "i" in all_dupE, erule (1) notE impE)
|
|
362 |
apply(erule_tac x = "j" in allE , erule (1) notE impE)
|
|
363 |
apply(simp add: interfree_def)
|
|
364 |
apply(erule_tac x = "j" in allE,simp)
|
|
365 |
apply(erule_tac x = "i" in allE,simp)
|
|
366 |
apply(drule_tac t = "i" in not_sym)
|
|
367 |
apply(case_tac "com(Ts ! j)=None")
|
|
368 |
apply(force intro: converse_rtrancl_into_rtrancl
|
|
369 |
simp add: interfree_aux_def com_validity_def SEM_def sem_def All_None_def)
|
|
370 |
apply(simp add:interfree_aux_def)
|
|
371 |
apply clarify
|
|
372 |
apply simp
|
|
373 |
apply(erule_tac x="pre y" in ballE)
|
|
374 |
apply(force intro: converse_rtrancl_into_rtrancl
|
|
375 |
simp add: com_validity_def SEM_def sem_def All_None_def)
|
|
376 |
apply(simp add:assertions_lemma)
|
|
377 |
--{* Seqs *}
|
|
378 |
apply(erule_tac x = "Ts[i:=(Some c0, pre c1)]" in allE)
|
|
379 |
apply(drule Parallel_Strong_Soundness_Seq,simp+)
|
|
380 |
apply(erule_tac x = "Ts[i:=(Some c0, pre c1)]" in allE)
|
|
381 |
apply(drule Parallel_Strong_Soundness_Seq,simp+)
|
|
382 |
--{* Await *}
|
|
383 |
apply(rule_tac x = "i" in allE , assumption , erule (1) notE impE)
|
|
384 |
apply(erule_tac x = "j" in allE , erule (1) notE impE)
|
|
385 |
apply(simp add: interfree_def)
|
|
386 |
apply(erule_tac x = "j" in allE,simp)
|
|
387 |
apply(erule_tac x = "i" in allE,simp)
|
|
388 |
apply(drule_tac t = "i" in not_sym)
|
|
389 |
apply(case_tac "com(Ts ! j)=None")
|
|
390 |
apply(force intro: converse_rtrancl_into_rtrancl simp add: interfree_aux_def
|
|
391 |
com_validity_def SEM_def sem_def All_None_def Help)
|
|
392 |
apply(simp add:interfree_aux_def)
|
|
393 |
apply clarify
|
|
394 |
apply simp
|
|
395 |
apply(erule_tac x="pre y" in ballE)
|
|
396 |
apply(force intro: converse_rtrancl_into_rtrancl
|
|
397 |
simp add: com_validity_def SEM_def sem_def All_None_def Help)
|
|
398 |
apply(simp add:assertions_lemma)
|
|
399 |
done
|
|
400 |
|
|
401 |
lemma Parallel_Strong_Soundness_aux [rule_format]:
|
|
402 |
"\<lbrakk>(Ts',s) -P*\<rightarrow> (Rs',t); Ts' = (Parallel Ts); interfree Ts;
|
|
403 |
\<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>
|
|
404 |
\<forall>Rs. Rs' = (Parallel Rs) \<longrightarrow> (\<forall>j. j<length Rs \<longrightarrow>
|
|
405 |
(if com(Rs ! j) = None then t\<in>post(Ts ! j)
|
|
406 |
else t\<in>pre(the(com(Rs ! j))) \<and> \<turnstile> the(com(Rs ! j)) post(Ts ! j))) \<and> interfree Rs"
|
|
407 |
apply(erule rtrancl_induct2)
|
|
408 |
apply clarify
|
|
409 |
--{* Base *}
|
|
410 |
apply force
|
|
411 |
--{* Induction step *}
|
|
412 |
apply clarify
|
|
413 |
apply(drule Parallel_length_post_PStar)
|
|
414 |
apply clarify
|
|
415 |
apply (ind_cases "(Parallel Ts, s) -P1\<rightarrow> (Parallel Rs, t)")
|
|
416 |
apply(rule conjI)
|
|
417 |
apply clarify
|
|
418 |
apply(case_tac "i=j")
|
|
419 |
apply(simp split del:split_if)
|
|
420 |
apply(erule Strong_Soundness_aux_aux,simp+)
|
|
421 |
apply force
|
|
422 |
apply force
|
|
423 |
apply(simp split del: split_if)
|
|
424 |
apply(erule Parallel_Strong_Soundness_aux_aux)
|
|
425 |
apply(simp_all add: split del:split_if)
|
|
426 |
apply force
|
|
427 |
apply(rule interfree_lemma)
|
|
428 |
apply simp_all
|
|
429 |
done
|
|
430 |
|
|
431 |
lemma Parallel_Strong_Soundness:
|
|
432 |
"\<lbrakk>(Parallel Ts, s) -P*\<rightarrow> (Parallel Rs, t); interfree Ts; j<length Rs;
|
|
433 |
\<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>
|
|
434 |
if com(Rs ! j) = None then t\<in>post(Ts ! j) else t\<in>pre (the(com(Rs ! j)))"
|
|
435 |
apply(drule Parallel_Strong_Soundness_aux)
|
|
436 |
apply simp+
|
|
437 |
done
|
|
438 |
|
15102
|
439 |
lemma oghoare_sound [rule_format]: "\<parallel>- p c q \<longrightarrow> \<parallel>= p c q"
|
13020
|
440 |
apply (unfold com_validity_def)
|
|
441 |
apply(rule oghoare_induct)
|
|
442 |
apply(rule TrueI)+
|
|
443 |
--{* Parallel *}
|
|
444 |
apply(simp add: SEM_def sem_def)
|
|
445 |
apply clarify
|
|
446 |
apply(frule Parallel_length_post_PStar)
|
|
447 |
apply clarify
|
|
448 |
apply(drule_tac j=i in Parallel_Strong_Soundness)
|
|
449 |
apply clarify
|
|
450 |
apply simp
|
|
451 |
apply force
|
|
452 |
apply simp
|
|
453 |
apply(erule_tac V = "\<forall>i. ?P i" in thin_rl)
|
|
454 |
apply(drule_tac s = "length Rs" in sym)
|
|
455 |
apply(erule allE, erule impE, assumption)
|
|
456 |
apply(force dest: nth_mem simp add: All_None_def)
|
|
457 |
--{* Basic *}
|
|
458 |
apply(simp add: SEM_def sem_def)
|
|
459 |
apply(force dest: rtrancl_imp_UN_rel_pow Basic_ntran)
|
|
460 |
--{* Seq *}
|
|
461 |
apply(rule subset_trans)
|
|
462 |
prefer 2 apply assumption
|
|
463 |
apply(simp add: L3_5ii L3_5i)
|
|
464 |
--{* Cond *}
|
|
465 |
apply(simp add: L3_5iv)
|
|
466 |
--{* While *}
|
|
467 |
apply(simp add: L3_5v)
|
15102
|
468 |
apply (blast dest: SEM_fwhile)
|
13020
|
469 |
--{* Conseq *}
|
15102
|
470 |
apply(auto simp add: SEM_def sem_def)
|
13020
|
471 |
done
|
|
472 |
|
|
473 |
end |