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