|
1 header {* \section{The Proof System} *} |
|
2 |
|
3 theory RG_Hoare imports RG_Tran begin |
|
4 |
|
5 subsection {* Proof System for Component Programs *} |
|
6 |
|
7 declare Un_subset_iff [iff del] |
|
8 declare Cons_eq_map_conv[iff] |
|
9 |
|
10 constdefs |
|
11 stable :: "'a set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> bool" |
|
12 "stable \<equiv> \<lambda>f g. (\<forall>x y. x \<in> f \<longrightarrow> (x, y) \<in> g \<longrightarrow> y \<in> f)" |
|
13 |
|
14 inductive |
|
15 rghoare :: "['a com, 'a set, ('a \<times> 'a) set, ('a \<times> 'a) set, 'a set] \<Rightarrow> bool" |
|
16 ("\<turnstile> _ sat [_, _, _, _]" [60,0,0,0,0] 45) |
|
17 where |
|
18 Basic: "\<lbrakk> pre \<subseteq> {s. f s \<in> post}; {(s,t). s \<in> pre \<and> (t=f s \<or> t=s)} \<subseteq> guar; |
|
19 stable pre rely; stable post rely \<rbrakk> |
|
20 \<Longrightarrow> \<turnstile> Basic f sat [pre, rely, guar, post]" |
|
21 |
|
22 | Seq: "\<lbrakk> \<turnstile> P sat [pre, rely, guar, mid]; \<turnstile> Q sat [mid, rely, guar, post] \<rbrakk> |
|
23 \<Longrightarrow> \<turnstile> Seq P Q sat [pre, rely, guar, post]" |
|
24 |
|
25 | Cond: "\<lbrakk> stable pre rely; \<turnstile> P1 sat [pre \<inter> b, rely, guar, post]; |
|
26 \<turnstile> P2 sat [pre \<inter> -b, rely, guar, post]; \<forall>s. (s,s)\<in>guar \<rbrakk> |
|
27 \<Longrightarrow> \<turnstile> Cond b P1 P2 sat [pre, rely, guar, post]" |
|
28 |
|
29 | While: "\<lbrakk> stable pre rely; (pre \<inter> -b) \<subseteq> post; stable post rely; |
|
30 \<turnstile> P sat [pre \<inter> b, rely, guar, pre]; \<forall>s. (s,s)\<in>guar \<rbrakk> |
|
31 \<Longrightarrow> \<turnstile> While b P sat [pre, rely, guar, post]" |
|
32 |
|
33 | Await: "\<lbrakk> stable pre rely; stable post rely; |
|
34 \<forall>V. \<turnstile> P sat [pre \<inter> b \<inter> {V}, {(s, t). s = t}, |
|
35 UNIV, {s. (V, s) \<in> guar} \<inter> post] \<rbrakk> |
|
36 \<Longrightarrow> \<turnstile> Await b P sat [pre, rely, guar, post]" |
|
37 |
|
38 | Conseq: "\<lbrakk> pre \<subseteq> pre'; rely \<subseteq> rely'; guar' \<subseteq> guar; post' \<subseteq> post; |
|
39 \<turnstile> P sat [pre', rely', guar', post'] \<rbrakk> |
|
40 \<Longrightarrow> \<turnstile> P sat [pre, rely, guar, post]" |
|
41 |
|
42 constdefs |
|
43 Pre :: "'a rgformula \<Rightarrow> 'a set" |
|
44 "Pre x \<equiv> fst(snd x)" |
|
45 Post :: "'a rgformula \<Rightarrow> 'a set" |
|
46 "Post x \<equiv> snd(snd(snd(snd x)))" |
|
47 Rely :: "'a rgformula \<Rightarrow> ('a \<times> 'a) set" |
|
48 "Rely x \<equiv> fst(snd(snd x))" |
|
49 Guar :: "'a rgformula \<Rightarrow> ('a \<times> 'a) set" |
|
50 "Guar x \<equiv> fst(snd(snd(snd x)))" |
|
51 Com :: "'a rgformula \<Rightarrow> 'a com" |
|
52 "Com x \<equiv> fst x" |
|
53 |
|
54 subsection {* Proof System for Parallel Programs *} |
|
55 |
|
56 types 'a par_rgformula = "('a rgformula) list \<times> 'a set \<times> ('a \<times> 'a) set \<times> ('a \<times> 'a) set \<times> 'a set" |
|
57 |
|
58 inductive |
|
59 par_rghoare :: "('a rgformula) list \<Rightarrow> 'a set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> 'a set \<Rightarrow> bool" |
|
60 ("\<turnstile> _ SAT [_, _, _, _]" [60,0,0,0,0] 45) |
|
61 where |
|
62 Parallel: |
|
63 "\<lbrakk> \<forall>i<length xs. rely \<union> (\<Union>j\<in>{j. j<length xs \<and> j\<noteq>i}. Guar(xs!j)) \<subseteq> Rely(xs!i); |
|
64 (\<Union>j\<in>{j. j<length xs}. Guar(xs!j)) \<subseteq> guar; |
|
65 pre \<subseteq> (\<Inter>i\<in>{i. i<length xs}. Pre(xs!i)); |
|
66 (\<Inter>i\<in>{i. i<length xs}. Post(xs!i)) \<subseteq> post; |
|
67 \<forall>i<length xs. \<turnstile> Com(xs!i) sat [Pre(xs!i),Rely(xs!i),Guar(xs!i),Post(xs!i)] \<rbrakk> |
|
68 \<Longrightarrow> \<turnstile> xs SAT [pre, rely, guar, post]" |
|
69 |
|
70 section {* Soundness*} |
|
71 |
|
72 subsubsection {* Some previous lemmas *} |
|
73 |
|
74 lemma tl_of_assum_in_assum: |
|
75 "(P, s) # (P, t) # xs \<in> assum (pre, rely) \<Longrightarrow> stable pre rely |
|
76 \<Longrightarrow> (P, t) # xs \<in> assum (pre, rely)" |
|
77 apply(simp add:assum_def) |
|
78 apply clarify |
|
79 apply(rule conjI) |
|
80 apply(erule_tac x=0 in allE) |
|
81 apply(simp (no_asm_use)only:stable_def) |
|
82 apply(erule allE,erule allE,erule impE,assumption,erule mp) |
|
83 apply(simp add:Env) |
|
84 apply clarify |
|
85 apply(erule_tac x="Suc i" in allE) |
|
86 apply simp |
|
87 done |
|
88 |
|
89 lemma etran_in_comm: |
|
90 "(P, t) # xs \<in> comm(guar, post) \<Longrightarrow> (P, s) # (P, t) # xs \<in> comm(guar, post)" |
|
91 apply(simp add:comm_def) |
|
92 apply clarify |
|
93 apply(case_tac i,simp+) |
|
94 done |
|
95 |
|
96 lemma ctran_in_comm: |
|
97 "\<lbrakk>(s, s) \<in> guar; (Q, s) # xs \<in> comm(guar, post)\<rbrakk> |
|
98 \<Longrightarrow> (P, s) # (Q, s) # xs \<in> comm(guar, post)" |
|
99 apply(simp add:comm_def) |
|
100 apply clarify |
|
101 apply(case_tac i,simp+) |
|
102 done |
|
103 |
|
104 lemma takecptn_is_cptn [rule_format, elim!]: |
|
105 "\<forall>j. c \<in> cptn \<longrightarrow> take (Suc j) c \<in> cptn" |
|
106 apply(induct "c") |
|
107 apply(force elim: cptn.cases) |
|
108 apply clarify |
|
109 apply(case_tac j) |
|
110 apply simp |
|
111 apply(rule CptnOne) |
|
112 apply simp |
|
113 apply(force intro:cptn.intros elim:cptn.cases) |
|
114 done |
|
115 |
|
116 lemma dropcptn_is_cptn [rule_format,elim!]: |
|
117 "\<forall>j<length c. c \<in> cptn \<longrightarrow> drop j c \<in> cptn" |
|
118 apply(induct "c") |
|
119 apply(force elim: cptn.cases) |
|
120 apply clarify |
|
121 apply(case_tac j,simp+) |
|
122 apply(erule cptn.cases) |
|
123 apply simp |
|
124 apply force |
|
125 apply force |
|
126 done |
|
127 |
|
128 lemma takepar_cptn_is_par_cptn [rule_format,elim]: |
|
129 "\<forall>j. c \<in> par_cptn \<longrightarrow> take (Suc j) c \<in> par_cptn" |
|
130 apply(induct "c") |
|
131 apply(force elim: cptn.cases) |
|
132 apply clarify |
|
133 apply(case_tac j,simp) |
|
134 apply(rule ParCptnOne) |
|
135 apply(force intro:par_cptn.intros elim:par_cptn.cases) |
|
136 done |
|
137 |
|
138 lemma droppar_cptn_is_par_cptn [rule_format]: |
|
139 "\<forall>j<length c. c \<in> par_cptn \<longrightarrow> drop j c \<in> par_cptn" |
|
140 apply(induct "c") |
|
141 apply(force elim: par_cptn.cases) |
|
142 apply clarify |
|
143 apply(case_tac j,simp+) |
|
144 apply(erule par_cptn.cases) |
|
145 apply simp |
|
146 apply force |
|
147 apply force |
|
148 done |
|
149 |
|
150 lemma tl_of_cptn_is_cptn: "\<lbrakk>x # xs \<in> cptn; xs \<noteq> []\<rbrakk> \<Longrightarrow> xs \<in> cptn" |
|
151 apply(subgoal_tac "1 < length (x # xs)") |
|
152 apply(drule dropcptn_is_cptn,simp+) |
|
153 done |
|
154 |
|
155 lemma not_ctran_None [rule_format]: |
|
156 "\<forall>s. (None, s)#xs \<in> cptn \<longrightarrow> (\<forall>i<length xs. ((None, s)#xs)!i -e\<rightarrow> xs!i)" |
|
157 apply(induct xs,simp+) |
|
158 apply clarify |
|
159 apply(erule cptn.cases,simp) |
|
160 apply simp |
|
161 apply(case_tac i,simp) |
|
162 apply(rule Env) |
|
163 apply simp |
|
164 apply(force elim:ctran.cases) |
|
165 done |
|
166 |
|
167 lemma cptn_not_empty [simp]:"[] \<notin> cptn" |
|
168 apply(force elim:cptn.cases) |
|
169 done |
|
170 |
|
171 lemma etran_or_ctran [rule_format]: |
|
172 "\<forall>m i. x\<in>cptn \<longrightarrow> m \<le> length x |
|
173 \<longrightarrow> (\<forall>i. Suc i < m \<longrightarrow> \<not> x!i -c\<rightarrow> x!Suc i) \<longrightarrow> Suc i < m |
|
174 \<longrightarrow> x!i -e\<rightarrow> x!Suc i" |
|
175 apply(induct x,simp) |
|
176 apply clarify |
|
177 apply(erule cptn.cases,simp) |
|
178 apply(case_tac i,simp) |
|
179 apply(rule Env) |
|
180 apply simp |
|
181 apply(erule_tac x="m - 1" in allE) |
|
182 apply(case_tac m,simp,simp) |
|
183 apply(subgoal_tac "(\<forall>i. Suc i < nata \<longrightarrow> (((P, t) # xs) ! i, xs ! i) \<notin> ctran)") |
|
184 apply force |
|
185 apply clarify |
|
186 apply(erule_tac x="Suc ia" in allE,simp) |
|
187 apply(erule_tac x="0" and P="\<lambda>j. ?H j \<longrightarrow> (?J j) \<notin> ctran" in allE,simp) |
|
188 done |
|
189 |
|
190 lemma etran_or_ctran2 [rule_format]: |
|
191 "\<forall>i. Suc i<length x \<longrightarrow> x\<in>cptn \<longrightarrow> (x!i -c\<rightarrow> x!Suc i \<longrightarrow> \<not> x!i -e\<rightarrow> x!Suc i) |
|
192 \<or> (x!i -e\<rightarrow> x!Suc i \<longrightarrow> \<not> x!i -c\<rightarrow> x!Suc i)" |
|
193 apply(induct x) |
|
194 apply simp |
|
195 apply clarify |
|
196 apply(erule cptn.cases,simp) |
|
197 apply(case_tac i,simp+) |
|
198 apply(case_tac i,simp) |
|
199 apply(force elim:etran.cases) |
|
200 apply simp |
|
201 done |
|
202 |
|
203 lemma etran_or_ctran2_disjI1: |
|
204 "\<lbrakk> x\<in>cptn; Suc i<length x; x!i -c\<rightarrow> x!Suc i\<rbrakk> \<Longrightarrow> \<not> x!i -e\<rightarrow> x!Suc i" |
|
205 by(drule etran_or_ctran2,simp_all) |
|
206 |
|
207 lemma etran_or_ctran2_disjI2: |
|
208 "\<lbrakk> x\<in>cptn; Suc i<length x; x!i -e\<rightarrow> x!Suc i\<rbrakk> \<Longrightarrow> \<not> x!i -c\<rightarrow> x!Suc i" |
|
209 by(drule etran_or_ctran2,simp_all) |
|
210 |
|
211 lemma not_ctran_None2 [rule_format]: |
|
212 "\<lbrakk> (None, s) # xs \<in>cptn; i<length xs\<rbrakk> \<Longrightarrow> \<not> ((None, s) # xs) ! i -c\<rightarrow> xs ! i" |
|
213 apply(frule not_ctran_None,simp) |
|
214 apply(case_tac i,simp) |
|
215 apply(force elim:etranE) |
|
216 apply simp |
|
217 apply(rule etran_or_ctran2_disjI2,simp_all) |
|
218 apply(force intro:tl_of_cptn_is_cptn) |
|
219 done |
|
220 |
|
221 lemma Ex_first_occurrence [rule_format]: "P (n::nat) \<longrightarrow> (\<exists>m. P m \<and> (\<forall>i<m. \<not> P i))"; |
|
222 apply(rule nat_less_induct) |
|
223 apply clarify |
|
224 apply(case_tac "\<forall>m. m<n \<longrightarrow> \<not> P m") |
|
225 apply auto |
|
226 done |
|
227 |
|
228 lemma stability [rule_format]: |
|
229 "\<forall>j k. x \<in> cptn \<longrightarrow> stable p rely \<longrightarrow> j\<le>k \<longrightarrow> k<length x \<longrightarrow> snd(x!j)\<in>p \<longrightarrow> |
|
230 (\<forall>i. (Suc i)<length x \<longrightarrow> |
|
231 (x!i -e\<rightarrow> x!(Suc i)) \<longrightarrow> (snd(x!i), snd(x!(Suc i))) \<in> rely) \<longrightarrow> |
|
232 (\<forall>i. j\<le>i \<and> i<k \<longrightarrow> x!i -e\<rightarrow> x!Suc i) \<longrightarrow> snd(x!k)\<in>p \<and> fst(x!j)=fst(x!k)" |
|
233 apply(induct x) |
|
234 apply clarify |
|
235 apply(force elim:cptn.cases) |
|
236 apply clarify |
|
237 apply(erule cptn.cases,simp) |
|
238 apply simp |
|
239 apply(case_tac k,simp,simp) |
|
240 apply(case_tac j,simp) |
|
241 apply(erule_tac x=0 in allE) |
|
242 apply(erule_tac x="nat" and P="\<lambda>j. (0\<le>j) \<longrightarrow> (?J j)" in allE,simp) |
|
243 apply(subgoal_tac "t\<in>p") |
|
244 apply(subgoal_tac "(\<forall>i. i < length xs \<longrightarrow> ((P, t) # xs) ! i -e\<rightarrow> xs ! i \<longrightarrow> (snd (((P, t) # xs) ! i), snd (xs ! i)) \<in> rely)") |
|
245 apply clarify |
|
246 apply(erule_tac x="Suc i" and P="\<lambda>j. (?H j) \<longrightarrow> (?J j)\<in>etran" in allE,simp) |
|
247 apply clarify |
|
248 apply(erule_tac x="Suc i" and P="\<lambda>j. (?H j) \<longrightarrow> (?J j) \<longrightarrow> (?T j)\<in>rely" in allE,simp) |
|
249 apply(erule_tac x=0 and P="\<lambda>j. (?H j) \<longrightarrow> (?J j)\<in>etran \<longrightarrow> ?T j" in allE,simp) |
|
250 apply(simp(no_asm_use) only:stable_def) |
|
251 apply(erule_tac x=s in allE) |
|
252 apply(erule_tac x=t in allE) |
|
253 apply simp |
|
254 apply(erule mp) |
|
255 apply(erule mp) |
|
256 apply(rule Env) |
|
257 apply simp |
|
258 apply(erule_tac x="nata" in allE) |
|
259 apply(erule_tac x="nat" and P="\<lambda>j. (?s\<le>j) \<longrightarrow> (?J j)" in allE,simp) |
|
260 apply(subgoal_tac "(\<forall>i. i < length xs \<longrightarrow> ((P, t) # xs) ! i -e\<rightarrow> xs ! i \<longrightarrow> (snd (((P, t) # xs) ! i), snd (xs ! i)) \<in> rely)") |
|
261 apply clarify |
|
262 apply(erule_tac x="Suc i" and P="\<lambda>j. (?H j) \<longrightarrow> (?J j)\<in>etran" in allE,simp) |
|
263 apply clarify |
|
264 apply(erule_tac x="Suc i" and P="\<lambda>j. (?H j) \<longrightarrow> (?J j) \<longrightarrow> (?T j)\<in>rely" in allE,simp) |
|
265 apply(case_tac k,simp,simp) |
|
266 apply(case_tac j) |
|
267 apply(erule_tac x=0 and P="\<lambda>j. (?H j) \<longrightarrow> (?J j)\<in>etran" in allE,simp) |
|
268 apply(erule etran.cases,simp) |
|
269 apply(erule_tac x="nata" in allE) |
|
270 apply(erule_tac x="nat" and P="\<lambda>j. (?s\<le>j) \<longrightarrow> (?J j)" in allE,simp) |
|
271 apply(subgoal_tac "(\<forall>i. i < length xs \<longrightarrow> ((Q, t) # xs) ! i -e\<rightarrow> xs ! i \<longrightarrow> (snd (((Q, t) # xs) ! i), snd (xs ! i)) \<in> rely)") |
|
272 apply clarify |
|
273 apply(erule_tac x="Suc i" and P="\<lambda>j. (?H j) \<longrightarrow> (?J j)\<in>etran" in allE,simp) |
|
274 apply clarify |
|
275 apply(erule_tac x="Suc i" and P="\<lambda>j. (?H j) \<longrightarrow> (?J j) \<longrightarrow> (?T j)\<in>rely" in allE,simp) |
|
276 done |
|
277 |
|
278 subsection {* Soundness of the System for Component Programs *} |
|
279 |
|
280 subsubsection {* Soundness of the Basic rule *} |
|
281 |
|
282 lemma unique_ctran_Basic [rule_format]: |
|
283 "\<forall>s i. x \<in> cptn \<longrightarrow> x ! 0 = (Some (Basic f), s) \<longrightarrow> |
|
284 Suc i<length x \<longrightarrow> x!i -c\<rightarrow> x!Suc i \<longrightarrow> |
|
285 (\<forall>j. Suc j<length x \<longrightarrow> i\<noteq>j \<longrightarrow> x!j -e\<rightarrow> x!Suc j)" |
|
286 apply(induct x,simp) |
|
287 apply simp |
|
288 apply clarify |
|
289 apply(erule cptn.cases,simp) |
|
290 apply(case_tac i,simp+) |
|
291 apply clarify |
|
292 apply(case_tac j,simp) |
|
293 apply(rule Env) |
|
294 apply simp |
|
295 apply clarify |
|
296 apply simp |
|
297 apply(case_tac i) |
|
298 apply(case_tac j,simp,simp) |
|
299 apply(erule ctran.cases,simp_all) |
|
300 apply(force elim: not_ctran_None) |
|
301 apply(ind_cases "((Some (Basic f), sa), Q, t) \<in> ctran" for sa Q t) |
|
302 apply simp |
|
303 apply(drule_tac i=nat in not_ctran_None,simp) |
|
304 apply(erule etranE,simp) |
|
305 done |
|
306 |
|
307 lemma exists_ctran_Basic_None [rule_format]: |
|
308 "\<forall>s i. x \<in> cptn \<longrightarrow> x ! 0 = (Some (Basic f), s) |
|
309 \<longrightarrow> i<length x \<longrightarrow> fst(x!i)=None \<longrightarrow> (\<exists>j<i. x!j -c\<rightarrow> x!Suc j)" |
|
310 apply(induct x,simp) |
|
311 apply simp |
|
312 apply clarify |
|
313 apply(erule cptn.cases,simp) |
|
314 apply(case_tac i,simp,simp) |
|
315 apply(erule_tac x=nat in allE,simp) |
|
316 apply clarify |
|
317 apply(rule_tac x="Suc j" in exI,simp,simp) |
|
318 apply clarify |
|
319 apply(case_tac i,simp,simp) |
|
320 apply(rule_tac x=0 in exI,simp) |
|
321 done |
|
322 |
|
323 lemma Basic_sound: |
|
324 " \<lbrakk>pre \<subseteq> {s. f s \<in> post}; {(s, t). s \<in> pre \<and> t = f s} \<subseteq> guar; |
|
325 stable pre rely; stable post rely\<rbrakk> |
|
326 \<Longrightarrow> \<Turnstile> Basic f sat [pre, rely, guar, post]" |
|
327 apply(unfold com_validity_def) |
|
328 apply clarify |
|
329 apply(simp add:comm_def) |
|
330 apply(rule conjI) |
|
331 apply clarify |
|
332 apply(simp add:cp_def assum_def) |
|
333 apply clarify |
|
334 apply(frule_tac j=0 and k=i and p=pre in stability) |
|
335 apply simp_all |
|
336 apply(erule_tac x=ia in allE,simp) |
|
337 apply(erule_tac i=i and f=f in unique_ctran_Basic,simp_all) |
|
338 apply(erule subsetD,simp) |
|
339 apply(case_tac "x!i") |
|
340 apply clarify |
|
341 apply(drule_tac s="Some (Basic f)" in sym,simp) |
|
342 apply(thin_tac "\<forall>j. ?H j") |
|
343 apply(force elim:ctran.cases) |
|
344 apply clarify |
|
345 apply(simp add:cp_def) |
|
346 apply clarify |
|
347 apply(frule_tac i="length x - 1" and f=f in exists_ctran_Basic_None,simp+) |
|
348 apply(case_tac x,simp+) |
|
349 apply(rule last_fst_esp,simp add:last_length) |
|
350 apply (case_tac x,simp+) |
|
351 apply(simp add:assum_def) |
|
352 apply clarify |
|
353 apply(frule_tac j=0 and k="j" and p=pre in stability) |
|
354 apply simp_all |
|
355 apply(erule_tac x=i in allE,simp) |
|
356 apply(erule_tac i=j and f=f in unique_ctran_Basic,simp_all) |
|
357 apply(case_tac "x!j") |
|
358 apply clarify |
|
359 apply simp |
|
360 apply(drule_tac s="Some (Basic f)" in sym,simp) |
|
361 apply(case_tac "x!Suc j",simp) |
|
362 apply(rule ctran.cases,simp) |
|
363 apply(simp_all) |
|
364 apply(drule_tac c=sa in subsetD,simp) |
|
365 apply clarify |
|
366 apply(frule_tac j="Suc j" and k="length x - 1" and p=post in stability,simp_all) |
|
367 apply(case_tac x,simp+) |
|
368 apply(erule_tac x=i in allE) |
|
369 apply(erule_tac i=j and f=f in unique_ctran_Basic,simp_all) |
|
370 apply arith+ |
|
371 apply(case_tac x) |
|
372 apply(simp add:last_length)+ |
|
373 done |
|
374 |
|
375 subsubsection{* Soundness of the Await rule *} |
|
376 |
|
377 lemma unique_ctran_Await [rule_format]: |
|
378 "\<forall>s i. x \<in> cptn \<longrightarrow> x ! 0 = (Some (Await b c), s) \<longrightarrow> |
|
379 Suc i<length x \<longrightarrow> x!i -c\<rightarrow> x!Suc i \<longrightarrow> |
|
380 (\<forall>j. Suc j<length x \<longrightarrow> i\<noteq>j \<longrightarrow> x!j -e\<rightarrow> x!Suc j)" |
|
381 apply(induct x,simp+) |
|
382 apply clarify |
|
383 apply(erule cptn.cases,simp) |
|
384 apply(case_tac i,simp+) |
|
385 apply clarify |
|
386 apply(case_tac j,simp) |
|
387 apply(rule Env) |
|
388 apply simp |
|
389 apply clarify |
|
390 apply simp |
|
391 apply(case_tac i) |
|
392 apply(case_tac j,simp,simp) |
|
393 apply(erule ctran.cases,simp_all) |
|
394 apply(force elim: not_ctran_None) |
|
395 apply(ind_cases "((Some (Await b c), sa), Q, t) \<in> ctran" for sa Q t,simp) |
|
396 apply(drule_tac i=nat in not_ctran_None,simp) |
|
397 apply(erule etranE,simp) |
|
398 done |
|
399 |
|
400 lemma exists_ctran_Await_None [rule_format]: |
|
401 "\<forall>s i. x \<in> cptn \<longrightarrow> x ! 0 = (Some (Await b c), s) |
|
402 \<longrightarrow> i<length x \<longrightarrow> fst(x!i)=None \<longrightarrow> (\<exists>j<i. x!j -c\<rightarrow> x!Suc j)" |
|
403 apply(induct x,simp+) |
|
404 apply clarify |
|
405 apply(erule cptn.cases,simp) |
|
406 apply(case_tac i,simp+) |
|
407 apply(erule_tac x=nat in allE,simp) |
|
408 apply clarify |
|
409 apply(rule_tac x="Suc j" in exI,simp,simp) |
|
410 apply clarify |
|
411 apply(case_tac i,simp,simp) |
|
412 apply(rule_tac x=0 in exI,simp) |
|
413 done |
|
414 |
|
415 lemma Star_imp_cptn: |
|
416 "(P, s) -c*\<rightarrow> (R, t) \<Longrightarrow> \<exists>l \<in> cp P s. (last l)=(R, t) |
|
417 \<and> (\<forall>i. Suc i<length l \<longrightarrow> l!i -c\<rightarrow> l!Suc i)" |
|
418 apply (erule converse_rtrancl_induct2) |
|
419 apply(rule_tac x="[(R,t)]" in bexI) |
|
420 apply simp |
|
421 apply(simp add:cp_def) |
|
422 apply(rule CptnOne) |
|
423 apply clarify |
|
424 apply(rule_tac x="(a, b)#l" in bexI) |
|
425 apply (rule conjI) |
|
426 apply(case_tac l,simp add:cp_def) |
|
427 apply(simp add:last_length) |
|
428 apply clarify |
|
429 apply(case_tac i,simp) |
|
430 apply(simp add:cp_def) |
|
431 apply force |
|
432 apply(simp add:cp_def) |
|
433 apply(case_tac l) |
|
434 apply(force elim:cptn.cases) |
|
435 apply simp |
|
436 apply(erule CptnComp) |
|
437 apply clarify |
|
438 done |
|
439 |
|
440 lemma Await_sound: |
|
441 "\<lbrakk>stable pre rely; stable post rely; |
|
442 \<forall>V. \<turnstile> P sat [pre \<inter> b \<inter> {s. s = V}, {(s, t). s = t}, |
|
443 UNIV, {s. (V, s) \<in> guar} \<inter> post] \<and> |
|
444 \<Turnstile> P sat [pre \<inter> b \<inter> {s. s = V}, {(s, t). s = t}, |
|
445 UNIV, {s. (V, s) \<in> guar} \<inter> post] \<rbrakk> |
|
446 \<Longrightarrow> \<Turnstile> Await b P sat [pre, rely, guar, post]" |
|
447 apply(unfold com_validity_def) |
|
448 apply clarify |
|
449 apply(simp add:comm_def) |
|
450 apply(rule conjI) |
|
451 apply clarify |
|
452 apply(simp add:cp_def assum_def) |
|
453 apply clarify |
|
454 apply(frule_tac j=0 and k=i and p=pre in stability,simp_all) |
|
455 apply(erule_tac x=ia in allE,simp) |
|
456 apply(subgoal_tac "x\<in> cp (Some(Await b P)) s") |
|
457 apply(erule_tac i=i in unique_ctran_Await,force,simp_all) |
|
458 apply(simp add:cp_def) |
|
459 --{* here starts the different part. *} |
|
460 apply(erule ctran.cases,simp_all) |
|
461 apply(drule Star_imp_cptn) |
|
462 apply clarify |
|
463 apply(erule_tac x=sa in allE) |
|
464 apply clarify |
|
465 apply(erule_tac x=sa in allE) |
|
466 apply(drule_tac c=l in subsetD) |
|
467 apply (simp add:cp_def) |
|
468 apply clarify |
|
469 apply(erule_tac x=ia and P="\<lambda>i. ?H i \<longrightarrow> (?J i,?I i)\<in>ctran" in allE,simp) |
|
470 apply(erule etranE,simp) |
|
471 apply simp |
|
472 apply clarify |
|
473 apply(simp add:cp_def) |
|
474 apply clarify |
|
475 apply(frule_tac i="length x - 1" in exists_ctran_Await_None,force) |
|
476 apply (case_tac x,simp+) |
|
477 apply(rule last_fst_esp,simp add:last_length) |
|
478 apply(case_tac x, (simp add:cptn_not_empty)+) |
|
479 apply clarify |
|
480 apply(simp add:assum_def) |
|
481 apply clarify |
|
482 apply(frule_tac j=0 and k="j" and p=pre in stability,simp_all) |
|
483 apply(erule_tac x=i in allE,simp) |
|
484 apply(erule_tac i=j in unique_ctran_Await,force,simp_all) |
|
485 apply(case_tac "x!j") |
|
486 apply clarify |
|
487 apply simp |
|
488 apply(drule_tac s="Some (Await b P)" in sym,simp) |
|
489 apply(case_tac "x!Suc j",simp) |
|
490 apply(rule ctran.cases,simp) |
|
491 apply(simp_all) |
|
492 apply(drule Star_imp_cptn) |
|
493 apply clarify |
|
494 apply(erule_tac x=sa in allE) |
|
495 apply clarify |
|
496 apply(erule_tac x=sa in allE) |
|
497 apply(drule_tac c=l in subsetD) |
|
498 apply (simp add:cp_def) |
|
499 apply clarify |
|
500 apply(erule_tac x=i and P="\<lambda>i. ?H i \<longrightarrow> (?J i,?I i)\<in>ctran" in allE,simp) |
|
501 apply(erule etranE,simp) |
|
502 apply simp |
|
503 apply clarify |
|
504 apply(frule_tac j="Suc j" and k="length x - 1" and p=post in stability,simp_all) |
|
505 apply(case_tac x,simp+) |
|
506 apply(erule_tac x=i in allE) |
|
507 apply(erule_tac i=j in unique_ctran_Await,force,simp_all) |
|
508 apply arith+ |
|
509 apply(case_tac x) |
|
510 apply(simp add:last_length)+ |
|
511 done |
|
512 |
|
513 subsubsection{* Soundness of the Conditional rule *} |
|
514 |
|
515 lemma Cond_sound: |
|
516 "\<lbrakk> stable pre rely; \<Turnstile> P1 sat [pre \<inter> b, rely, guar, post]; |
|
517 \<Turnstile> P2 sat [pre \<inter> - b, rely, guar, post]; \<forall>s. (s,s)\<in>guar\<rbrakk> |
|
518 \<Longrightarrow> \<Turnstile> (Cond b P1 P2) sat [pre, rely, guar, post]" |
|
519 apply(unfold com_validity_def) |
|
520 apply clarify |
|
521 apply(simp add:cp_def comm_def) |
|
522 apply(case_tac "\<exists>i. Suc i<length x \<and> x!i -c\<rightarrow> x!Suc i") |
|
523 prefer 2 |
|
524 apply simp |
|
525 apply clarify |
|
526 apply(frule_tac j="0" and k="length x - 1" and p=pre in stability,simp+) |
|
527 apply(case_tac x,simp+) |
|
528 apply(simp add:assum_def) |
|
529 apply(simp add:assum_def) |
|
530 apply(erule_tac m="length x" in etran_or_ctran,simp+) |
|
531 apply(case_tac x, (simp add:last_length)+) |
|
532 apply(erule exE) |
|
533 apply(drule_tac n=i and P="\<lambda>i. ?H i \<and> (?J i,?I i)\<in> ctran" in Ex_first_occurrence) |
|
534 apply clarify |
|
535 apply (simp add:assum_def) |
|
536 apply(frule_tac j=0 and k="m" and p=pre in stability,simp+) |
|
537 apply(erule_tac m="Suc m" in etran_or_ctran,simp+) |
|
538 apply(erule ctran.cases,simp_all) |
|
539 apply(erule_tac x="sa" in allE) |
|
540 apply(drule_tac c="drop (Suc m) x" in subsetD) |
|
541 apply simp |
|
542 apply clarify |
|
543 apply simp |
|
544 apply clarify |
|
545 apply(case_tac "i\<le>m") |
|
546 apply(drule le_imp_less_or_eq) |
|
547 apply(erule disjE) |
|
548 apply(erule_tac x=i in allE, erule impE, assumption) |
|
549 apply simp+ |
|
550 apply(erule_tac x="i - (Suc m)" and P="\<lambda>j. ?H j \<longrightarrow> ?J j \<longrightarrow> (?I j)\<in>guar" in allE) |
|
551 apply(subgoal_tac "(Suc m)+(i - Suc m) \<le> length x") |
|
552 apply(subgoal_tac "(Suc m)+Suc (i - Suc m) \<le> length x") |
|
553 apply(rotate_tac -2) |
|
554 apply simp |
|
555 apply arith |
|
556 apply arith |
|
557 apply(case_tac "length (drop (Suc m) x)",simp) |
|
558 apply(erule_tac x="sa" in allE) |
|
559 back |
|
560 apply(drule_tac c="drop (Suc m) x" in subsetD,simp) |
|
561 apply clarify |
|
562 apply simp |
|
563 apply clarify |
|
564 apply(case_tac "i\<le>m") |
|
565 apply(drule le_imp_less_or_eq) |
|
566 apply(erule disjE) |
|
567 apply(erule_tac x=i in allE, erule impE, assumption) |
|
568 apply simp |
|
569 apply simp |
|
570 apply(erule_tac x="i - (Suc m)" and P="\<lambda>j. ?H j \<longrightarrow> ?J j \<longrightarrow> (?I j)\<in>guar" in allE) |
|
571 apply(subgoal_tac "(Suc m)+(i - Suc m) \<le> length x") |
|
572 apply(subgoal_tac "(Suc m)+Suc (i - Suc m) \<le> length x") |
|
573 apply(rotate_tac -2) |
|
574 apply simp |
|
575 apply arith |
|
576 apply arith |
|
577 done |
|
578 |
|
579 subsubsection{* Soundness of the Sequential rule *} |
|
580 |
|
581 inductive_cases Seq_cases [elim!]: "(Some (Seq P Q), s) -c\<rightarrow> t" |
|
582 |
|
583 lemma last_lift_not_None: "fst ((lift Q) ((x#xs)!(length xs))) \<noteq> None" |
|
584 apply(subgoal_tac "length xs<length (x # xs)") |
|
585 apply(drule_tac Q=Q in lift_nth) |
|
586 apply(erule ssubst) |
|
587 apply (simp add:lift_def) |
|
588 apply(case_tac "(x # xs) ! length xs",simp) |
|
589 apply simp |
|
590 done |
|
591 |
|
592 declare map_eq_Cons_conv [simp del] Cons_eq_map_conv [simp del] |
|
593 lemma Seq_sound1 [rule_format]: |
|
594 "x\<in> cptn_mod \<Longrightarrow> \<forall>s P. x !0=(Some (Seq P Q), s) \<longrightarrow> |
|
595 (\<forall>i<length x. fst(x!i)\<noteq>Some Q) \<longrightarrow> |
|
596 (\<exists>xs\<in> cp (Some P) s. x=map (lift Q) xs)" |
|
597 apply(erule cptn_mod.induct) |
|
598 apply(unfold cp_def) |
|
599 apply safe |
|
600 apply simp_all |
|
601 apply(simp add:lift_def) |
|
602 apply(rule_tac x="[(Some Pa, sa)]" in exI,simp add:CptnOne) |
|
603 apply(subgoal_tac "(\<forall>i < Suc (length xs). fst (((Some (Seq Pa Q), t) # xs) ! i) \<noteq> Some Q)") |
|
604 apply clarify |
|
605 apply(rule_tac x="(Some Pa, sa) #(Some Pa, t) # zs" in exI,simp) |
|
606 apply(rule conjI,erule CptnEnv) |
|
607 apply(simp (no_asm_use) add:lift_def) |
|
608 apply clarify |
|
609 apply(erule_tac x="Suc i" in allE, simp) |
|
610 apply(ind_cases "((Some (Seq Pa Q), sa), None, t) \<in> ctran" for Pa sa t) |
|
611 apply(rule_tac x="(Some P, sa) # xs" in exI, simp add:cptn_iff_cptn_mod lift_def) |
|
612 apply(erule_tac x="length xs" in allE, simp) |
|
613 apply(simp only:Cons_lift_append) |
|
614 apply(subgoal_tac "length xs < length ((Some P, sa) # xs)") |
|
615 apply(simp only :nth_append length_map last_length nth_map) |
|
616 apply(case_tac "last((Some P, sa) # xs)") |
|
617 apply(simp add:lift_def) |
|
618 apply simp |
|
619 done |
|
620 declare map_eq_Cons_conv [simp del] Cons_eq_map_conv [simp del] |
|
621 |
|
622 lemma Seq_sound2 [rule_format]: |
|
623 "x \<in> cptn \<Longrightarrow> \<forall>s P i. x!0=(Some (Seq P Q), s) \<longrightarrow> i<length x |
|
624 \<longrightarrow> fst(x!i)=Some Q \<longrightarrow> |
|
625 (\<forall>j<i. fst(x!j)\<noteq>(Some Q)) \<longrightarrow> |
|
626 (\<exists>xs ys. xs \<in> cp (Some P) s \<and> length xs=Suc i |
|
627 \<and> ys \<in> cp (Some Q) (snd(xs !i)) \<and> x=(map (lift Q) xs)@tl ys)" |
|
628 apply(erule cptn.induct) |
|
629 apply(unfold cp_def) |
|
630 apply safe |
|
631 apply simp_all |
|
632 apply(case_tac i,simp+) |
|
633 apply(erule allE,erule impE,assumption,simp) |
|
634 apply clarify |
|
635 apply(subgoal_tac "(\<forall>j < nat. fst (((Some (Seq Pa Q), t) # xs) ! j) \<noteq> Some Q)",clarify) |
|
636 prefer 2 |
|
637 apply force |
|
638 apply(case_tac xsa,simp,simp) |
|
639 apply(rule_tac x="(Some Pa, sa) #(Some Pa, t) # list" in exI,simp) |
|
640 apply(rule conjI,erule CptnEnv) |
|
641 apply(simp (no_asm_use) add:lift_def) |
|
642 apply(rule_tac x=ys in exI,simp) |
|
643 apply(ind_cases "((Some (Seq Pa Q), sa), t) \<in> ctran" for Pa sa t) |
|
644 apply simp |
|
645 apply(rule_tac x="(Some Pa, sa)#[(None, ta)]" in exI,simp) |
|
646 apply(rule conjI) |
|
647 apply(drule_tac xs="[]" in CptnComp,force simp add:CptnOne,simp) |
|
648 apply(case_tac i, simp+) |
|
649 apply(case_tac nat,simp+) |
|
650 apply(rule_tac x="(Some Q,ta)#xs" in exI,simp add:lift_def) |
|
651 apply(case_tac nat,simp+) |
|
652 apply(force) |
|
653 apply(case_tac i, simp+) |
|
654 apply(case_tac nat,simp+) |
|
655 apply(erule_tac x="Suc nata" in allE,simp) |
|
656 apply clarify |
|
657 apply(subgoal_tac "(\<forall>j<Suc nata. fst (((Some (Seq P2 Q), ta) # xs) ! j) \<noteq> Some Q)",clarify) |
|
658 prefer 2 |
|
659 apply clarify |
|
660 apply force |
|
661 apply(rule_tac x="(Some Pa, sa)#(Some P2, ta)#(tl xsa)" in exI,simp) |
|
662 apply(rule conjI,erule CptnComp) |
|
663 apply(rule nth_tl_if,force,simp+) |
|
664 apply(rule_tac x=ys in exI,simp) |
|
665 apply(rule conjI) |
|
666 apply(rule nth_tl_if,force,simp+) |
|
667 apply(rule tl_zero,simp+) |
|
668 apply force |
|
669 apply(rule conjI,simp add:lift_def) |
|
670 apply(subgoal_tac "lift Q (Some P2, ta) =(Some (Seq P2 Q), ta)") |
|
671 apply(simp add:Cons_lift del:map.simps) |
|
672 apply(rule nth_tl_if) |
|
673 apply force |
|
674 apply simp+ |
|
675 apply(simp add:lift_def) |
|
676 done |
|
677 (* |
|
678 lemma last_lift_not_None3: "fst (last (map (lift Q) (x#xs))) \<noteq> None" |
|
679 apply(simp only:last_length [THEN sym]) |
|
680 apply(subgoal_tac "length xs<length (x # xs)") |
|
681 apply(drule_tac Q=Q in lift_nth) |
|
682 apply(erule ssubst) |
|
683 apply (simp add:lift_def) |
|
684 apply(case_tac "(x # xs) ! length xs",simp) |
|
685 apply simp |
|
686 done |
|
687 *) |
|
688 |
|
689 lemma last_lift_not_None2: "fst ((lift Q) (last (x#xs))) \<noteq> None" |
|
690 apply(simp only:last_length [THEN sym]) |
|
691 apply(subgoal_tac "length xs<length (x # xs)") |
|
692 apply(drule_tac Q=Q in lift_nth) |
|
693 apply(erule ssubst) |
|
694 apply (simp add:lift_def) |
|
695 apply(case_tac "(x # xs) ! length xs",simp) |
|
696 apply simp |
|
697 done |
|
698 |
|
699 lemma Seq_sound: |
|
700 "\<lbrakk>\<Turnstile> P sat [pre, rely, guar, mid]; \<Turnstile> Q sat [mid, rely, guar, post]\<rbrakk> |
|
701 \<Longrightarrow> \<Turnstile> Seq P Q sat [pre, rely, guar, post]" |
|
702 apply(unfold com_validity_def) |
|
703 apply clarify |
|
704 apply(case_tac "\<exists>i<length x. fst(x!i)=Some Q") |
|
705 prefer 2 |
|
706 apply (simp add:cp_def cptn_iff_cptn_mod) |
|
707 apply clarify |
|
708 apply(frule_tac Seq_sound1,force) |
|
709 apply force |
|
710 apply clarify |
|
711 apply(erule_tac x=s in allE,simp) |
|
712 apply(drule_tac c=xs in subsetD,simp add:cp_def cptn_iff_cptn_mod) |
|
713 apply(simp add:assum_def) |
|
714 apply clarify |
|
715 apply(erule_tac P="\<lambda>j. ?H j \<longrightarrow> ?J j \<longrightarrow> ?I j" in allE,erule impE, assumption) |
|
716 apply(simp add:snd_lift) |
|
717 apply(erule mp) |
|
718 apply(force elim:etranE intro:Env simp add:lift_def) |
|
719 apply(simp add:comm_def) |
|
720 apply(rule conjI) |
|
721 apply clarify |
|
722 apply(erule_tac P="\<lambda>j. ?H j \<longrightarrow> ?J j \<longrightarrow> ?I j" in allE,erule impE, assumption) |
|
723 apply(simp add:snd_lift) |
|
724 apply(erule mp) |
|
725 apply(case_tac "(xs!i)") |
|
726 apply(case_tac "(xs! Suc i)") |
|
727 apply(case_tac "fst(xs!i)") |
|
728 apply(erule_tac x=i in allE, simp add:lift_def) |
|
729 apply(case_tac "fst(xs!Suc i)") |
|
730 apply(force simp add:lift_def) |
|
731 apply(force simp add:lift_def) |
|
732 apply clarify |
|
733 apply(case_tac xs,simp add:cp_def) |
|
734 apply clarify |
|
735 apply (simp del:map.simps) |
|
736 apply(subgoal_tac "(map (lift Q) ((a, b) # list))\<noteq>[]") |
|
737 apply(drule last_conv_nth) |
|
738 apply (simp del:map.simps) |
|
739 apply(simp only:last_lift_not_None) |
|
740 apply simp |
|
741 --{* @{text "\<exists>i<length x. fst (x ! i) = Some Q"} *} |
|
742 apply(erule exE) |
|
743 apply(drule_tac n=i and P="\<lambda>i. i < length x \<and> fst (x ! i) = Some Q" in Ex_first_occurrence) |
|
744 apply clarify |
|
745 apply (simp add:cp_def) |
|
746 apply clarify |
|
747 apply(frule_tac i=m in Seq_sound2,force) |
|
748 apply simp+ |
|
749 apply clarify |
|
750 apply(simp add:comm_def) |
|
751 apply(erule_tac x=s in allE) |
|
752 apply(drule_tac c=xs in subsetD,simp) |
|
753 apply(case_tac "xs=[]",simp) |
|
754 apply(simp add:cp_def assum_def nth_append) |
|
755 apply clarify |
|
756 apply(erule_tac x=i in allE) |
|
757 back |
|
758 apply(simp add:snd_lift) |
|
759 apply(erule mp) |
|
760 apply(force elim:etranE intro:Env simp add:lift_def) |
|
761 apply simp |
|
762 apply clarify |
|
763 apply(erule_tac x="snd(xs!m)" in allE) |
|
764 apply(drule_tac c=ys in subsetD,simp add:cp_def assum_def) |
|
765 apply(case_tac "xs\<noteq>[]") |
|
766 apply(drule last_conv_nth,simp) |
|
767 apply(rule conjI) |
|
768 apply(erule mp) |
|
769 apply(case_tac "xs!m") |
|
770 apply(case_tac "fst(xs!m)",simp) |
|
771 apply(simp add:lift_def nth_append) |
|
772 apply clarify |
|
773 apply(erule_tac x="m+i" in allE) |
|
774 back |
|
775 back |
|
776 apply(case_tac ys,(simp add:nth_append)+) |
|
777 apply (case_tac i, (simp add:snd_lift)+) |
|
778 apply(erule mp) |
|
779 apply(case_tac "xs!m") |
|
780 apply(force elim:etran.cases intro:Env simp add:lift_def) |
|
781 apply simp |
|
782 apply simp |
|
783 apply clarify |
|
784 apply(rule conjI,clarify) |
|
785 apply(case_tac "i<m",simp add:nth_append) |
|
786 apply(simp add:snd_lift) |
|
787 apply(erule allE, erule impE, assumption, erule mp) |
|
788 apply(case_tac "(xs ! i)") |
|
789 apply(case_tac "(xs ! Suc i)") |
|
790 apply(case_tac "fst(xs ! i)",force simp add:lift_def) |
|
791 apply(case_tac "fst(xs ! Suc i)") |
|
792 apply (force simp add:lift_def) |
|
793 apply (force simp add:lift_def) |
|
794 apply(erule_tac x="i-m" in allE) |
|
795 back |
|
796 back |
|
797 apply(subgoal_tac "Suc (i - m) < length ys",simp) |
|
798 prefer 2 |
|
799 apply arith |
|
800 apply(simp add:nth_append snd_lift) |
|
801 apply(rule conjI,clarify) |
|
802 apply(subgoal_tac "i=m") |
|
803 prefer 2 |
|
804 apply arith |
|
805 apply clarify |
|
806 apply(simp add:cp_def) |
|
807 apply(rule tl_zero) |
|
808 apply(erule mp) |
|
809 apply(case_tac "lift Q (xs!m)",simp add:snd_lift) |
|
810 apply(case_tac "xs!m",case_tac "fst(xs!m)",simp add:lift_def snd_lift) |
|
811 apply(case_tac ys,simp+) |
|
812 apply(simp add:lift_def) |
|
813 apply simp |
|
814 apply force |
|
815 apply clarify |
|
816 apply(rule tl_zero) |
|
817 apply(rule tl_zero) |
|
818 apply (subgoal_tac "i-m=Suc(i-Suc m)") |
|
819 apply simp |
|
820 apply(erule mp) |
|
821 apply(case_tac ys,simp+) |
|
822 apply force |
|
823 apply arith |
|
824 apply force |
|
825 apply clarify |
|
826 apply(case_tac "(map (lift Q) xs @ tl ys)\<noteq>[]") |
|
827 apply(drule last_conv_nth) |
|
828 apply(simp add: snd_lift nth_append) |
|
829 apply(rule conjI,clarify) |
|
830 apply(case_tac ys,simp+) |
|
831 apply clarify |
|
832 apply(case_tac ys,simp+) |
|
833 done |
|
834 |
|
835 subsubsection{* Soundness of the While rule *} |
|
836 |
|
837 lemma last_append[rule_format]: |
|
838 "\<forall>xs. ys\<noteq>[] \<longrightarrow> ((xs@ys)!(length (xs@ys) - (Suc 0)))=(ys!(length ys - (Suc 0)))" |
|
839 apply(induct ys) |
|
840 apply simp |
|
841 apply clarify |
|
842 apply (simp add:nth_append length_append) |
|
843 done |
|
844 |
|
845 lemma assum_after_body: |
|
846 "\<lbrakk> \<Turnstile> P sat [pre \<inter> b, rely, guar, pre]; |
|
847 (Some P, s) # xs \<in> cptn_mod; fst (last ((Some P, s) # xs)) = None; s \<in> b; |
|
848 (Some (While b P), s) # (Some (Seq P (While b P)), s) # |
|
849 map (lift (While b P)) xs @ ys \<in> assum (pre, rely)\<rbrakk> |
|
850 \<Longrightarrow> (Some (While b P), snd (last ((Some P, s) # xs))) # ys \<in> assum (pre, rely)" |
|
851 apply(simp add:assum_def com_validity_def cp_def cptn_iff_cptn_mod) |
|
852 apply clarify |
|
853 apply(erule_tac x=s in allE) |
|
854 apply(drule_tac c="(Some P, s) # xs" in subsetD,simp) |
|
855 apply clarify |
|
856 apply(erule_tac x="Suc i" in allE) |
|
857 apply simp |
|
858 apply(simp add:Cons_lift_append nth_append snd_lift del:map.simps) |
|
859 apply(erule mp) |
|
860 apply(erule etranE,simp) |
|
861 apply(case_tac "fst(((Some P, s) # xs) ! i)") |
|
862 apply(force intro:Env simp add:lift_def) |
|
863 apply(force intro:Env simp add:lift_def) |
|
864 apply(rule conjI) |
|
865 apply clarify |
|
866 apply(simp add:comm_def last_length) |
|
867 apply clarify |
|
868 apply(rule conjI) |
|
869 apply(simp add:comm_def) |
|
870 apply clarify |
|
871 apply(erule_tac x="Suc(length xs + i)" in allE,simp) |
|
872 apply(case_tac i, simp add:nth_append Cons_lift_append snd_lift del:map.simps) |
|
873 apply(simp add:last_length) |
|
874 apply(erule mp) |
|
875 apply(case_tac "last xs") |
|
876 apply(simp add:lift_def) |
|
877 apply(simp add:Cons_lift_append nth_append snd_lift del:map.simps) |
|
878 done |
|
879 |
|
880 lemma While_sound_aux [rule_format]: |
|
881 "\<lbrakk> pre \<inter> - b \<subseteq> post; \<Turnstile> P sat [pre \<inter> b, rely, guar, pre]; \<forall>s. (s, s) \<in> guar; |
|
882 stable pre rely; stable post rely; x \<in> cptn_mod \<rbrakk> |
|
883 \<Longrightarrow> \<forall>s xs. x=(Some(While b P),s)#xs \<longrightarrow> x\<in>assum(pre, rely) \<longrightarrow> x \<in> comm (guar, post)" |
|
884 apply(erule cptn_mod.induct) |
|
885 apply safe |
|
886 apply (simp_all del:last.simps) |
|
887 --{* 5 subgoals left *} |
|
888 apply(simp add:comm_def) |
|
889 --{* 4 subgoals left *} |
|
890 apply(rule etran_in_comm) |
|
891 apply(erule mp) |
|
892 apply(erule tl_of_assum_in_assum,simp) |
|
893 --{* While-None *} |
|
894 apply(ind_cases "((Some (While b P), s), None, t) \<in> ctran" for s t) |
|
895 apply(simp add:comm_def) |
|
896 apply(simp add:cptn_iff_cptn_mod [THEN sym]) |
|
897 apply(rule conjI,clarify) |
|
898 apply(force simp add:assum_def) |
|
899 apply clarify |
|
900 apply(rule conjI, clarify) |
|
901 apply(case_tac i,simp,simp) |
|
902 apply(force simp add:not_ctran_None2) |
|
903 apply(subgoal_tac "\<forall>i. Suc i < length ((None, t) # xs) \<longrightarrow> (((None, t) # xs) ! i, ((None, t) # xs) ! Suc i)\<in> etran") |
|
904 prefer 2 |
|
905 apply clarify |
|
906 apply(rule_tac m="length ((None, s) # xs)" in etran_or_ctran,simp+) |
|
907 apply(erule not_ctran_None2,simp) |
|
908 apply simp+ |
|
909 apply(frule_tac j="0" and k="length ((None, s) # xs) - 1" and p=post in stability,simp+) |
|
910 apply(force simp add:assum_def subsetD) |
|
911 apply(simp add:assum_def) |
|
912 apply clarify |
|
913 apply(erule_tac x="i" in allE,simp) |
|
914 apply(erule_tac x="Suc i" in allE,simp) |
|
915 apply simp |
|
916 apply clarify |
|
917 apply (simp add:last_length) |
|
918 --{* WhileOne *} |
|
919 apply(thin_tac "P = While b P \<longrightarrow> ?Q") |
|
920 apply(rule ctran_in_comm,simp) |
|
921 apply(simp add:Cons_lift del:map.simps) |
|
922 apply(simp add:comm_def del:map.simps) |
|
923 apply(rule conjI) |
|
924 apply clarify |
|
925 apply(case_tac "fst(((Some P, sa) # xs) ! i)") |
|
926 apply(case_tac "((Some P, sa) # xs) ! i") |
|
927 apply (simp add:lift_def) |
|
928 apply(ind_cases "(Some (While b P), ba) -c\<rightarrow> t" for ba t) |
|
929 apply simp |
|
930 apply simp |
|
931 apply(simp add:snd_lift del:map.simps) |
|
932 apply(simp only:com_validity_def cp_def cptn_iff_cptn_mod) |
|
933 apply(erule_tac x=sa in allE) |
|
934 apply(drule_tac c="(Some P, sa) # xs" in subsetD) |
|
935 apply (simp add:assum_def del:map.simps) |
|
936 apply clarify |
|
937 apply(erule_tac x="Suc ia" in allE,simp add:snd_lift del:map.simps) |
|
938 apply(erule mp) |
|
939 apply(case_tac "fst(((Some P, sa) # xs) ! ia)") |
|
940 apply(erule etranE,simp add:lift_def) |
|
941 apply(rule Env) |
|
942 apply(erule etranE,simp add:lift_def) |
|
943 apply(rule Env) |
|
944 apply (simp add:comm_def del:map.simps) |
|
945 apply clarify |
|
946 apply(erule allE,erule impE,assumption) |
|
947 apply(erule mp) |
|
948 apply(case_tac "((Some P, sa) # xs) ! i") |
|
949 apply(case_tac "xs!i") |
|
950 apply(simp add:lift_def) |
|
951 apply(case_tac "fst(xs!i)") |
|
952 apply force |
|
953 apply force |
|
954 --{* last=None *} |
|
955 apply clarify |
|
956 apply(subgoal_tac "(map (lift (While b P)) ((Some P, sa) # xs))\<noteq>[]") |
|
957 apply(drule last_conv_nth) |
|
958 apply (simp del:map.simps) |
|
959 apply(simp only:last_lift_not_None) |
|
960 apply simp |
|
961 --{* WhileMore *} |
|
962 apply(thin_tac "P = While b P \<longrightarrow> ?Q") |
|
963 apply(rule ctran_in_comm,simp del:last.simps) |
|
964 --{* metiendo la hipotesis antes de dividir la conclusion. *} |
|
965 apply(subgoal_tac "(Some (While b P), snd (last ((Some P, sa) # xs))) # ys \<in> assum (pre, rely)") |
|
966 apply (simp del:last.simps) |
|
967 prefer 2 |
|
968 apply(erule assum_after_body) |
|
969 apply (simp del:last.simps)+ |
|
970 --{* lo de antes. *} |
|
971 apply(simp add:comm_def del:map.simps last.simps) |
|
972 apply(rule conjI) |
|
973 apply clarify |
|
974 apply(simp only:Cons_lift_append) |
|
975 apply(case_tac "i<length xs") |
|
976 apply(simp add:nth_append del:map.simps last.simps) |
|
977 apply(case_tac "fst(((Some P, sa) # xs) ! i)") |
|
978 apply(case_tac "((Some P, sa) # xs) ! i") |
|
979 apply (simp add:lift_def del:last.simps) |
|
980 apply(ind_cases "(Some (While b P), ba) -c\<rightarrow> t" for ba t) |
|
981 apply simp |
|
982 apply simp |
|
983 apply(simp add:snd_lift del:map.simps last.simps) |
|
984 apply(thin_tac " \<forall>i. i < length ys \<longrightarrow> ?P i") |
|
985 apply(simp only:com_validity_def cp_def cptn_iff_cptn_mod) |
|
986 apply(erule_tac x=sa in allE) |
|
987 apply(drule_tac c="(Some P, sa) # xs" in subsetD) |
|
988 apply (simp add:assum_def del:map.simps last.simps) |
|
989 apply clarify |
|
990 apply(erule_tac x="Suc ia" in allE,simp add:nth_append snd_lift del:map.simps last.simps, erule mp) |
|
991 apply(case_tac "fst(((Some P, sa) # xs) ! ia)") |
|
992 apply(erule etranE,simp add:lift_def) |
|
993 apply(rule Env) |
|
994 apply(erule etranE,simp add:lift_def) |
|
995 apply(rule Env) |
|
996 apply (simp add:comm_def del:map.simps) |
|
997 apply clarify |
|
998 apply(erule allE,erule impE,assumption) |
|
999 apply(erule mp) |
|
1000 apply(case_tac "((Some P, sa) # xs) ! i") |
|
1001 apply(case_tac "xs!i") |
|
1002 apply(simp add:lift_def) |
|
1003 apply(case_tac "fst(xs!i)") |
|
1004 apply force |
|
1005 apply force |
|
1006 --{* @{text "i \<ge> length xs"} *} |
|
1007 apply(subgoal_tac "i-length xs <length ys") |
|
1008 prefer 2 |
|
1009 apply arith |
|
1010 apply(erule_tac x="i-length xs" in allE,clarify) |
|
1011 apply(case_tac "i=length xs") |
|
1012 apply (simp add:nth_append snd_lift del:map.simps last.simps) |
|
1013 apply(simp add:last_length del:last.simps) |
|
1014 apply(erule mp) |
|
1015 apply(case_tac "last((Some P, sa) # xs)") |
|
1016 apply(simp add:lift_def del:last.simps) |
|
1017 --{* @{text "i>length xs"} *} |
|
1018 apply(case_tac "i-length xs") |
|
1019 apply arith |
|
1020 apply(simp add:nth_append del:map.simps last.simps) |
|
1021 apply(rotate_tac -3) |
|
1022 apply(subgoal_tac "i- Suc (length xs)=nat") |
|
1023 prefer 2 |
|
1024 apply arith |
|
1025 apply simp |
|
1026 --{* last=None *} |
|
1027 apply clarify |
|
1028 apply(case_tac ys) |
|
1029 apply(simp add:Cons_lift del:map.simps last.simps) |
|
1030 apply(subgoal_tac "(map (lift (While b P)) ((Some P, sa) # xs))\<noteq>[]") |
|
1031 apply(drule last_conv_nth) |
|
1032 apply (simp del:map.simps) |
|
1033 apply(simp only:last_lift_not_None) |
|
1034 apply simp |
|
1035 apply(subgoal_tac "((Some (Seq P (While b P)), sa) # map (lift (While b P)) xs @ ys)\<noteq>[]") |
|
1036 apply(drule last_conv_nth) |
|
1037 apply (simp del:map.simps last.simps) |
|
1038 apply(simp add:nth_append del:last.simps) |
|
1039 apply(subgoal_tac "((Some (While b P), snd (last ((Some P, sa) # xs))) # a # list)\<noteq>[]") |
|
1040 apply(drule last_conv_nth) |
|
1041 apply (simp del:map.simps last.simps) |
|
1042 apply simp |
|
1043 apply simp |
|
1044 done |
|
1045 |
|
1046 lemma While_sound: |
|
1047 "\<lbrakk>stable pre rely; pre \<inter> - b \<subseteq> post; stable post rely; |
|
1048 \<Turnstile> P sat [pre \<inter> b, rely, guar, pre]; \<forall>s. (s,s)\<in>guar\<rbrakk> |
|
1049 \<Longrightarrow> \<Turnstile> While b P sat [pre, rely, guar, post]" |
|
1050 apply(unfold com_validity_def) |
|
1051 apply clarify |
|
1052 apply(erule_tac xs="tl x" in While_sound_aux) |
|
1053 apply(simp add:com_validity_def) |
|
1054 apply force |
|
1055 apply simp_all |
|
1056 apply(simp add:cptn_iff_cptn_mod cp_def) |
|
1057 apply(simp add:cp_def) |
|
1058 apply clarify |
|
1059 apply(rule nth_equalityI) |
|
1060 apply simp_all |
|
1061 apply(case_tac x,simp+) |
|
1062 apply clarify |
|
1063 apply(case_tac i,simp+) |
|
1064 apply(case_tac x,simp+) |
|
1065 done |
|
1066 |
|
1067 subsubsection{* Soundness of the Rule of Consequence *} |
|
1068 |
|
1069 lemma Conseq_sound: |
|
1070 "\<lbrakk>pre \<subseteq> pre'; rely \<subseteq> rely'; guar' \<subseteq> guar; post' \<subseteq> post; |
|
1071 \<Turnstile> P sat [pre', rely', guar', post']\<rbrakk> |
|
1072 \<Longrightarrow> \<Turnstile> P sat [pre, rely, guar, post]" |
|
1073 apply(simp add:com_validity_def assum_def comm_def) |
|
1074 apply clarify |
|
1075 apply(erule_tac x=s in allE) |
|
1076 apply(drule_tac c=x in subsetD) |
|
1077 apply force |
|
1078 apply force |
|
1079 done |
|
1080 |
|
1081 subsubsection {* Soundness of the system for sequential component programs *} |
|
1082 |
|
1083 theorem rgsound: |
|
1084 "\<turnstile> P sat [pre, rely, guar, post] \<Longrightarrow> \<Turnstile> P sat [pre, rely, guar, post]" |
|
1085 apply(erule rghoare.induct) |
|
1086 apply(force elim:Basic_sound) |
|
1087 apply(force elim:Seq_sound) |
|
1088 apply(force elim:Cond_sound) |
|
1089 apply(force elim:While_sound) |
|
1090 apply(force elim:Await_sound) |
|
1091 apply(erule Conseq_sound,simp+) |
|
1092 done |
|
1093 |
|
1094 subsection {* Soundness of the System for Parallel Programs *} |
|
1095 |
|
1096 constdefs |
|
1097 ParallelCom :: "('a rgformula) list \<Rightarrow> 'a par_com" |
|
1098 "ParallelCom Ps \<equiv> map (Some \<circ> fst) Ps" |
|
1099 |
|
1100 lemma two: |
|
1101 "\<lbrakk> \<forall>i<length xs. rely \<union> (\<Union>j\<in>{j. j < length xs \<and> j \<noteq> i}. Guar (xs ! j)) |
|
1102 \<subseteq> Rely (xs ! i); |
|
1103 pre \<subseteq> (\<Inter>i\<in>{i. i < length xs}. Pre (xs ! i)); |
|
1104 \<forall>i<length xs. |
|
1105 \<Turnstile> Com (xs ! i) sat [Pre (xs ! i), Rely (xs ! i), Guar (xs ! i), Post (xs ! i)]; |
|
1106 length xs=length clist; x \<in> par_cp (ParallelCom xs) s; x\<in>par_assum(pre, rely); |
|
1107 \<forall>i<length clist. clist!i\<in>cp (Some(Com(xs!i))) s; x \<propto> clist \<rbrakk> |
|
1108 \<Longrightarrow> \<forall>j i. i<length clist \<and> Suc j<length x \<longrightarrow> (clist!i!j) -c\<rightarrow> (clist!i!Suc j) |
|
1109 \<longrightarrow> (snd(clist!i!j), snd(clist!i!Suc j)) \<in> Guar(xs!i)" |
|
1110 apply(unfold par_cp_def) |
|
1111 apply (rule ccontr) |
|
1112 --{* By contradiction: *} |
|
1113 apply (simp del: Un_subset_iff) |
|
1114 apply(erule exE) |
|
1115 --{* the first c-tran that does not satisfy the guarantee-condition is from @{text "\<sigma>_i"} at step @{text "m"}. *} |
|
1116 apply(drule_tac n=j and P="\<lambda>j. \<exists>i. ?H i j" in Ex_first_occurrence) |
|
1117 apply(erule exE) |
|
1118 apply clarify |
|
1119 --{* @{text "\<sigma>_i \<in> A(pre, rely_1)"} *} |
|
1120 apply(subgoal_tac "take (Suc (Suc m)) (clist!i) \<in> assum(Pre(xs!i), Rely(xs!i))") |
|
1121 --{* but this contradicts @{text "\<Turnstile> \<sigma>_i sat [pre_i,rely_i,guar_i,post_i]"} *} |
|
1122 apply(erule_tac x=i and P="\<lambda>i. ?H i \<longrightarrow> \<Turnstile> (?J i) sat [?I i,?K i,?M i,?N i]" in allE,erule impE,assumption) |
|
1123 apply(simp add:com_validity_def) |
|
1124 apply(erule_tac x=s in allE) |
|
1125 apply(simp add:cp_def comm_def) |
|
1126 apply(drule_tac c="take (Suc (Suc m)) (clist ! i)" in subsetD) |
|
1127 apply simp |
|
1128 apply (blast intro: takecptn_is_cptn) |
|
1129 apply simp |
|
1130 apply clarify |
|
1131 apply(erule_tac x=m and P="\<lambda>j. ?I j \<and> ?J j \<longrightarrow> ?H j" in allE) |
|
1132 apply (simp add:conjoin_def same_length_def) |
|
1133 apply(simp add:assum_def del: Un_subset_iff) |
|
1134 apply(rule conjI) |
|
1135 apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> ?I j \<in>cp (?K j) (?J j)" in allE) |
|
1136 apply(simp add:cp_def par_assum_def) |
|
1137 apply(drule_tac c="s" in subsetD,simp) |
|
1138 apply simp |
|
1139 apply clarify |
|
1140 apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> ?M \<union> UNION (?S j) (?T j) \<subseteq> (?L j)" in allE) |
|
1141 apply(simp del: Un_subset_iff) |
|
1142 apply(erule subsetD) |
|
1143 apply simp |
|
1144 apply(simp add:conjoin_def compat_label_def) |
|
1145 apply clarify |
|
1146 apply(erule_tac x=ia and P="\<lambda>j. ?H j \<longrightarrow> (?P j) \<or> ?Q j" in allE,simp) |
|
1147 --{* each etran in @{text "\<sigma>_1[0\<dots>m]"} corresponds to *} |
|
1148 apply(erule disjE) |
|
1149 --{* a c-tran in some @{text "\<sigma>_{ib}"} *} |
|
1150 apply clarify |
|
1151 apply(case_tac "i=ib",simp) |
|
1152 apply(erule etranE,simp) |
|
1153 apply(erule_tac x="ib" and P="\<lambda>i. ?H i \<longrightarrow> (?I i) \<or> (?J i)" in allE) |
|
1154 apply (erule etranE) |
|
1155 apply(case_tac "ia=m",simp) |
|
1156 apply simp |
|
1157 apply(erule_tac x=ia and P="\<lambda>j. ?H j \<longrightarrow> (\<forall> i. ?P i j)" in allE) |
|
1158 apply(subgoal_tac "ia<m",simp) |
|
1159 prefer 2 |
|
1160 apply arith |
|
1161 apply(erule_tac x=ib and P="\<lambda>j. (?I j, ?H j)\<in> ctran \<longrightarrow> (?P i j)" in allE,simp) |
|
1162 apply(simp add:same_state_def) |
|
1163 apply(erule_tac x=i and P="\<lambda>j. (?T j) \<longrightarrow> (\<forall>i. (?H j i) \<longrightarrow> (snd (?d j i))=(snd (?e j i)))" in all_dupE) |
|
1164 apply(erule_tac x=ib and P="\<lambda>j. (?T j) \<longrightarrow> (\<forall>i. (?H j i) \<longrightarrow> (snd (?d j i))=(snd (?e j i)))" in allE,simp) |
|
1165 --{* or an e-tran in @{text "\<sigma>"}, |
|
1166 therefore it satisfies @{text "rely \<or> guar_{ib}"} *} |
|
1167 apply (force simp add:par_assum_def same_state_def) |
|
1168 done |
|
1169 |
|
1170 |
|
1171 lemma three [rule_format]: |
|
1172 "\<lbrakk> xs\<noteq>[]; \<forall>i<length xs. rely \<union> (\<Union>j\<in>{j. j < length xs \<and> j \<noteq> i}. Guar (xs ! j)) |
|
1173 \<subseteq> Rely (xs ! i); |
|
1174 pre \<subseteq> (\<Inter>i\<in>{i. i < length xs}. Pre (xs ! i)); |
|
1175 \<forall>i<length xs. |
|
1176 \<Turnstile> Com (xs ! i) sat [Pre (xs ! i), Rely (xs ! i), Guar (xs ! i), Post (xs ! i)]; |
|
1177 length xs=length clist; x \<in> par_cp (ParallelCom xs) s; x \<in> par_assum(pre, rely); |
|
1178 \<forall>i<length clist. clist!i\<in>cp (Some(Com(xs!i))) s; x \<propto> clist \<rbrakk> |
|
1179 \<Longrightarrow> \<forall>j i. i<length clist \<and> Suc j<length x \<longrightarrow> (clist!i!j) -e\<rightarrow> (clist!i!Suc j) |
|
1180 \<longrightarrow> (snd(clist!i!j), snd(clist!i!Suc j)) \<in> rely \<union> (\<Union>j\<in>{j. j < length xs \<and> j \<noteq> i}. Guar (xs ! j))" |
|
1181 apply(drule two) |
|
1182 apply simp_all |
|
1183 apply clarify |
|
1184 apply(simp add:conjoin_def compat_label_def) |
|
1185 apply clarify |
|
1186 apply(erule_tac x=j and P="\<lambda>j. ?H j \<longrightarrow> (?J j \<and> (\<exists>i. ?P i j)) \<or> ?I j" in allE,simp) |
|
1187 apply(erule disjE) |
|
1188 prefer 2 |
|
1189 apply(force simp add:same_state_def par_assum_def) |
|
1190 apply clarify |
|
1191 apply(case_tac "i=ia",simp) |
|
1192 apply(erule etranE,simp) |
|
1193 apply(erule_tac x="ia" and P="\<lambda>i. ?H i \<longrightarrow> (?I i) \<or> (?J i)" in allE,simp) |
|
1194 apply(erule_tac x=j and P="\<lambda>j. \<forall>i. ?S j i \<longrightarrow> (?I j i, ?H j i)\<in> ctran \<longrightarrow> (?P i j)" in allE) |
|
1195 apply(erule_tac x=ia and P="\<lambda>j. ?S j \<longrightarrow> (?I j, ?H j)\<in> ctran \<longrightarrow> (?P j)" in allE) |
|
1196 apply(simp add:same_state_def) |
|
1197 apply(erule_tac x=i and P="\<lambda>j. (?T j) \<longrightarrow> (\<forall>i. (?H j i) \<longrightarrow> (snd (?d j i))=(snd (?e j i)))" in all_dupE) |
|
1198 apply(erule_tac x=ia and P="\<lambda>j. (?T j) \<longrightarrow> (\<forall>i. (?H j i) \<longrightarrow> (snd (?d j i))=(snd (?e j i)))" in allE,simp) |
|
1199 done |
|
1200 |
|
1201 lemma four: |
|
1202 "\<lbrakk>xs\<noteq>[]; \<forall>i < length xs. rely \<union> (\<Union>j\<in>{j. j < length xs \<and> j \<noteq> i}. Guar (xs ! j)) |
|
1203 \<subseteq> Rely (xs ! i); |
|
1204 (\<Union>j\<in>{j. j < length xs}. Guar (xs ! j)) \<subseteq> guar; |
|
1205 pre \<subseteq> (\<Inter>i\<in>{i. i < length xs}. Pre (xs ! i)); |
|
1206 \<forall>i < length xs. |
|
1207 \<Turnstile> Com (xs ! i) sat [Pre (xs ! i), Rely (xs ! i), Guar (xs ! i), Post (xs ! i)]; |
|
1208 x \<in> par_cp (ParallelCom xs) s; x \<in> par_assum (pre, rely); Suc i < length x; |
|
1209 x ! i -pc\<rightarrow> x ! Suc i\<rbrakk> |
|
1210 \<Longrightarrow> (snd (x ! i), snd (x ! Suc i)) \<in> guar" |
|
1211 apply(simp add: ParallelCom_def del: Un_subset_iff) |
|
1212 apply(subgoal_tac "(map (Some \<circ> fst) xs)\<noteq>[]") |
|
1213 prefer 2 |
|
1214 apply simp |
|
1215 apply(frule rev_subsetD) |
|
1216 apply(erule one [THEN equalityD1]) |
|
1217 apply(erule subsetD) |
|
1218 apply (simp del: Un_subset_iff) |
|
1219 apply clarify |
|
1220 apply(drule_tac pre=pre and rely=rely and x=x and s=s and xs=xs and clist=clist in two) |
|
1221 apply(assumption+) |
|
1222 apply(erule sym) |
|
1223 apply(simp add:ParallelCom_def) |
|
1224 apply assumption |
|
1225 apply(simp add:Com_def) |
|
1226 apply assumption |
|
1227 apply(simp add:conjoin_def same_program_def) |
|
1228 apply clarify |
|
1229 apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> fst(?I j)=(?J j)" in all_dupE) |
|
1230 apply(erule_tac x="Suc i" and P="\<lambda>j. ?H j \<longrightarrow> fst(?I j)=(?J j)" in allE) |
|
1231 apply(erule par_ctranE,simp) |
|
1232 apply(erule_tac x=i and P="\<lambda>j. \<forall>i. ?S j i \<longrightarrow> (?I j i, ?H j i)\<in> ctran \<longrightarrow> (?P i j)" in allE) |
|
1233 apply(erule_tac x=ia and P="\<lambda>j. ?S j \<longrightarrow> (?I j, ?H j)\<in> ctran \<longrightarrow> (?P j)" in allE) |
|
1234 apply(rule_tac x=ia in exI) |
|
1235 apply(simp add:same_state_def) |
|
1236 apply(erule_tac x=ia and P="\<lambda>j. (?T j) \<longrightarrow> (\<forall>i. (?H j i) \<longrightarrow> (snd (?d j i))=(snd (?e j i)))" in all_dupE,simp) |
|
1237 apply(erule_tac x=ia and P="\<lambda>j. (?T j) \<longrightarrow> (\<forall>i. (?H j i) \<longrightarrow> (snd (?d j i))=(snd (?e j i)))" in allE,simp) |
|
1238 apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> (snd (?d j))=(snd (?e j))" in all_dupE) |
|
1239 apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> (snd (?d j))=(snd (?e j))" in all_dupE,simp) |
|
1240 apply(erule_tac x="Suc i" and P="\<lambda>j. ?H j \<longrightarrow> (snd (?d j))=(snd (?e j))" in allE,simp) |
|
1241 apply(erule mp) |
|
1242 apply(subgoal_tac "r=fst(clist ! ia ! Suc i)",simp) |
|
1243 apply(drule_tac i=ia in list_eq_if) |
|
1244 back |
|
1245 apply simp_all |
|
1246 done |
|
1247 |
|
1248 lemma parcptn_not_empty [simp]:"[] \<notin> par_cptn" |
|
1249 apply(force elim:par_cptn.cases) |
|
1250 done |
|
1251 |
|
1252 lemma five: |
|
1253 "\<lbrakk>xs\<noteq>[]; \<forall>i<length xs. rely \<union> (\<Union>j\<in>{j. j < length xs \<and> j \<noteq> i}. Guar (xs ! j)) |
|
1254 \<subseteq> Rely (xs ! i); |
|
1255 pre \<subseteq> (\<Inter>i\<in>{i. i < length xs}. Pre (xs ! i)); |
|
1256 (\<Inter>i\<in>{i. i < length xs}. Post (xs ! i)) \<subseteq> post; |
|
1257 \<forall>i < length xs. |
|
1258 \<Turnstile> Com (xs ! i) sat [Pre (xs ! i), Rely (xs ! i), Guar (xs ! i), Post (xs ! i)]; |
|
1259 x \<in> par_cp (ParallelCom xs) s; x \<in> par_assum (pre, rely); |
|
1260 All_None (fst (last x)) \<rbrakk> \<Longrightarrow> snd (last x) \<in> post" |
|
1261 apply(simp add: ParallelCom_def del: Un_subset_iff) |
|
1262 apply(subgoal_tac "(map (Some \<circ> fst) xs)\<noteq>[]") |
|
1263 prefer 2 |
|
1264 apply simp |
|
1265 apply(frule rev_subsetD) |
|
1266 apply(erule one [THEN equalityD1]) |
|
1267 apply(erule subsetD) |
|
1268 apply(simp del: Un_subset_iff) |
|
1269 apply clarify |
|
1270 apply(subgoal_tac "\<forall>i<length clist. clist!i\<in>assum(Pre(xs!i), Rely(xs!i))") |
|
1271 apply(erule_tac x=i and P="\<lambda>i. ?H i \<longrightarrow> \<Turnstile> (?J i) sat [?I i,?K i,?M i,?N i]" in allE,erule impE,assumption) |
|
1272 apply(simp add:com_validity_def) |
|
1273 apply(erule_tac x=s in allE) |
|
1274 apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> (?I j) \<in> cp (?J j) s" in allE,simp) |
|
1275 apply(drule_tac c="clist!i" in subsetD) |
|
1276 apply (force simp add:Com_def) |
|
1277 apply(simp add:comm_def conjoin_def same_program_def del:last.simps) |
|
1278 apply clarify |
|
1279 apply(erule_tac x="length x - 1" and P="\<lambda>j. ?H j \<longrightarrow> fst(?I j)=(?J j)" in allE) |
|
1280 apply (simp add:All_None_def same_length_def) |
|
1281 apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> length(?J j)=(?K j)" in allE) |
|
1282 apply(subgoal_tac "length x - 1 < length x",simp) |
|
1283 apply(case_tac "x\<noteq>[]") |
|
1284 apply(simp add: last_conv_nth) |
|
1285 apply(erule_tac x="clist!i" in ballE) |
|
1286 apply(simp add:same_state_def) |
|
1287 apply(subgoal_tac "clist!i\<noteq>[]") |
|
1288 apply(simp add: last_conv_nth) |
|
1289 apply(case_tac x) |
|
1290 apply (force simp add:par_cp_def) |
|
1291 apply (force simp add:par_cp_def) |
|
1292 apply force |
|
1293 apply (force simp add:par_cp_def) |
|
1294 apply(case_tac x) |
|
1295 apply (force simp add:par_cp_def) |
|
1296 apply (force simp add:par_cp_def) |
|
1297 apply clarify |
|
1298 apply(simp add:assum_def) |
|
1299 apply(rule conjI) |
|
1300 apply(simp add:conjoin_def same_state_def par_cp_def) |
|
1301 apply clarify |
|
1302 apply(erule_tac x=ia and P="\<lambda>j. (?T j) \<longrightarrow> (\<forall>i. (?H j i) \<longrightarrow> (snd (?d j i))=(snd (?e j i)))" in allE,simp) |
|
1303 apply(erule_tac x=0 and P="\<lambda>j. ?H j \<longrightarrow> (snd (?d j))=(snd (?e j))" in allE) |
|
1304 apply(case_tac x,simp+) |
|
1305 apply (simp add:par_assum_def) |
|
1306 apply clarify |
|
1307 apply(drule_tac c="snd (clist ! ia ! 0)" in subsetD) |
|
1308 apply assumption |
|
1309 apply simp |
|
1310 apply clarify |
|
1311 apply(erule_tac x=ia in all_dupE) |
|
1312 apply(rule subsetD, erule mp, assumption) |
|
1313 apply(erule_tac pre=pre and rely=rely and x=x and s=s in three) |
|
1314 apply(erule_tac x=ic in allE,erule mp) |
|
1315 apply simp_all |
|
1316 apply(simp add:ParallelCom_def) |
|
1317 apply(force simp add:Com_def) |
|
1318 apply(simp add:conjoin_def same_length_def) |
|
1319 done |
|
1320 |
|
1321 lemma ParallelEmpty [rule_format]: |
|
1322 "\<forall>i s. x \<in> par_cp (ParallelCom []) s \<longrightarrow> |
|
1323 Suc i < length x \<longrightarrow> (x ! i, x ! Suc i) \<notin> par_ctran" |
|
1324 apply(induct_tac x) |
|
1325 apply(simp add:par_cp_def ParallelCom_def) |
|
1326 apply clarify |
|
1327 apply(case_tac list,simp,simp) |
|
1328 apply(case_tac i) |
|
1329 apply(simp add:par_cp_def ParallelCom_def) |
|
1330 apply(erule par_ctranE,simp) |
|
1331 apply(simp add:par_cp_def ParallelCom_def) |
|
1332 apply clarify |
|
1333 apply(erule par_cptn.cases,simp) |
|
1334 apply simp |
|
1335 apply(erule par_ctranE) |
|
1336 back |
|
1337 apply simp |
|
1338 done |
|
1339 |
|
1340 theorem par_rgsound: |
|
1341 "\<turnstile> c SAT [pre, rely, guar, post] \<Longrightarrow> |
|
1342 \<Turnstile> (ParallelCom c) SAT [pre, rely, guar, post]" |
|
1343 apply(erule par_rghoare.induct) |
|
1344 apply(case_tac xs,simp) |
|
1345 apply(simp add:par_com_validity_def par_comm_def) |
|
1346 apply clarify |
|
1347 apply(case_tac "post=UNIV",simp) |
|
1348 apply clarify |
|
1349 apply(drule ParallelEmpty) |
|
1350 apply assumption |
|
1351 apply simp |
|
1352 apply clarify |
|
1353 apply simp |
|
1354 apply(subgoal_tac "xs\<noteq>[]") |
|
1355 prefer 2 |
|
1356 apply simp |
|
1357 apply(thin_tac "xs = a # list") |
|
1358 apply(simp add:par_com_validity_def par_comm_def) |
|
1359 apply clarify |
|
1360 apply(rule conjI) |
|
1361 apply clarify |
|
1362 apply(erule_tac pre=pre and rely=rely and guar=guar and x=x and s=s and xs=xs in four) |
|
1363 apply(assumption+) |
|
1364 apply clarify |
|
1365 apply (erule allE, erule impE, assumption,erule rgsound) |
|
1366 apply(assumption+) |
|
1367 apply clarify |
|
1368 apply(erule_tac pre=pre and rely=rely and post=post and x=x and s=s and xs=xs in five) |
|
1369 apply(assumption+) |
|
1370 apply clarify |
|
1371 apply (erule allE, erule impE, assumption,erule rgsound) |
|
1372 apply(assumption+) |
|
1373 done |
|
1374 |
|
1375 end |