|
1 |
|
2 header {* \section{Operational Semantics} *} |
|
3 |
|
4 theory RG_Tran = RG_Com: |
|
5 |
|
6 subsection {* Semantics of Component Programs *} |
|
7 |
|
8 subsubsection {* Environment transitions *} |
|
9 |
|
10 types 'a conf = "(('a com) option) \<times> 'a" |
|
11 |
|
12 consts etran :: "('a conf \<times> 'a conf) set" |
|
13 syntax "_etran" :: "'a conf \<Rightarrow> 'a conf \<Rightarrow> bool" ("_ -e\<rightarrow> _" [81,81] 80) |
|
14 translations "P -e\<rightarrow> Q" \<rightleftharpoons> "(P,Q) \<in> etran" |
|
15 inductive etran |
|
16 intros |
|
17 Env: "(P, s) -e\<rightarrow> (P, t)" |
|
18 |
|
19 subsubsection {* Component transitions *} |
|
20 |
|
21 consts ctran :: "('a conf \<times> 'a conf) set" |
|
22 syntax |
|
23 "_ctran" :: "'a conf \<Rightarrow> 'a conf \<Rightarrow> bool" ("_ -c\<rightarrow> _" [81,81] 80) |
|
24 "_ctran_*":: "'a conf \<Rightarrow> 'a conf \<Rightarrow> bool" ("_ -c*\<rightarrow> _" [81,81] 80) |
|
25 translations |
|
26 "P -c\<rightarrow> Q" \<rightleftharpoons> "(P,Q) \<in> ctran" |
|
27 "P -c*\<rightarrow> Q" \<rightleftharpoons> "(P,Q) \<in> ctran^*" |
|
28 |
|
29 inductive ctran |
|
30 intros |
|
31 Basic: "(Some(Basic f), s) -c\<rightarrow> (None, f s)" |
|
32 |
|
33 Seq1: "(Some P0, s) -c\<rightarrow> (None, t) \<Longrightarrow> (Some(Seq P0 P1), s) -c\<rightarrow> (Some P1, t)" |
|
34 |
|
35 Seq2: "(Some P0, s) -c\<rightarrow> (Some P2, t) \<Longrightarrow> (Some(Seq P0 P1), s) -c\<rightarrow> (Some(Seq P2 P1), t)" |
|
36 |
|
37 CondT: "s\<in>b \<Longrightarrow> (Some(Cond b P1 P2), s) -c\<rightarrow> (Some P1, s)" |
|
38 CondF: "s\<notin>b \<Longrightarrow> (Some(Cond b P1 P2), s) -c\<rightarrow> (Some P2, s)" |
|
39 |
|
40 WhileF: "s\<notin>b \<Longrightarrow> (Some(While b P), s) -c\<rightarrow> (None, s)" |
|
41 WhileT: "s\<in>b \<Longrightarrow> (Some(While b P), s) -c\<rightarrow> (Some(Seq P (While b P)), s)" |
|
42 |
|
43 Await: "\<lbrakk>s\<in>b; (Some P, s) -c*\<rightarrow> (None, t)\<rbrakk> \<Longrightarrow> (Some(Await b P), s) -c\<rightarrow> (None, t)" |
|
44 |
|
45 monos "rtrancl_mono" |
|
46 |
|
47 subsection {* Semantics of Parallel Programs *} |
|
48 |
|
49 types 'a par_conf = "('a par_com) \<times> 'a" |
|
50 consts |
|
51 par_etran :: "('a par_conf \<times> 'a par_conf) set" |
|
52 par_ctran :: "('a par_conf \<times> 'a par_conf) set" |
|
53 syntax |
|
54 "_par_etran":: "['a par_conf,'a par_conf] \<Rightarrow> bool" ("_ -pe\<rightarrow> _" [81,81] 80) |
|
55 "_par_ctran":: "['a par_conf,'a par_conf] \<Rightarrow> bool" ("_ -pc\<rightarrow> _" [81,81] 80) |
|
56 translations |
|
57 "P -pe\<rightarrow> Q" \<rightleftharpoons> "(P,Q) \<in> par_etran" |
|
58 "P -pc\<rightarrow> Q" \<rightleftharpoons> "(P,Q) \<in> par_ctran" |
|
59 |
|
60 inductive par_etran |
|
61 intros |
|
62 ParEnv: "(Ps, s) -pe\<rightarrow> (Ps, t)" |
|
63 |
|
64 inductive par_ctran |
|
65 intros |
|
66 ParComp: "\<lbrakk>i<length Ps; (Ps!i, s) -c\<rightarrow> (r, t)\<rbrakk> \<Longrightarrow> (Ps, s) -pc\<rightarrow> (Ps[i:=r], t)" |
|
67 |
|
68 subsection {* Computations *} |
|
69 |
|
70 subsubsection {* Sequential computations *} |
|
71 |
|
72 types 'a confs = "('a conf) list" |
|
73 consts cptn :: "('a confs) set" |
|
74 inductive "cptn" |
|
75 intros |
|
76 CptnOne: "[(P,s)] \<in> cptn" |
|
77 CptnEnv: "(P, t)#xs \<in> cptn \<Longrightarrow> (P,s)#(P,t)#xs \<in> cptn" |
|
78 CptnComp: "\<lbrakk>(P,s) -c\<rightarrow> (Q,t); (Q, t)#xs \<in> cptn \<rbrakk> \<Longrightarrow> (P,s)#(Q,t)#xs \<in> cptn" |
|
79 |
|
80 constdefs |
|
81 cp :: "('a com) option \<Rightarrow> 'a \<Rightarrow> ('a confs) set" |
|
82 "cp P s \<equiv> {l. l!0=(P,s) \<and> l \<in> cptn}" |
|
83 |
|
84 subsubsection {* Parallel computations *} |
|
85 |
|
86 types 'a par_confs = "('a par_conf) list" |
|
87 consts par_cptn :: "('a par_confs) set" |
|
88 inductive "par_cptn" |
|
89 intros |
|
90 ParCptnOne: "[(P,s)] \<in> par_cptn" |
|
91 ParCptnEnv: "(P,t)#xs \<in> par_cptn \<Longrightarrow> (P,s)#(P,t)#xs \<in> par_cptn" |
|
92 ParCptnComp: "\<lbrakk> (P,s) -pc\<rightarrow> (Q,t); (Q,t)#xs \<in> par_cptn \<rbrakk> \<Longrightarrow> (P,s)#(Q,t)#xs \<in> par_cptn" |
|
93 |
|
94 constdefs |
|
95 par_cp :: "'a par_com \<Rightarrow> 'a \<Rightarrow> ('a par_confs) set" |
|
96 "par_cp P s \<equiv> {l. l!0=(P,s) \<and> l \<in> par_cptn}" |
|
97 |
|
98 subsection{* Modular Definition of Computation *} |
|
99 |
|
100 constdefs |
|
101 lift :: "'a com \<Rightarrow> 'a conf \<Rightarrow> 'a conf" |
|
102 "lift Q \<equiv> \<lambda>(P, s). (if P=None then (Some Q,s) else (Some(Seq (the P) Q), s))" |
|
103 |
|
104 consts cptn_mod :: "('a confs) set" |
|
105 inductive "cptn_mod" |
|
106 intros |
|
107 CptnModOne: "[(P, s)] \<in> cptn_mod" |
|
108 CptnModEnv: "(P, t)#xs \<in> cptn_mod \<Longrightarrow> (P, s)#(P, t)#xs \<in> cptn_mod" |
|
109 CptnModNone: "\<lbrakk>(Some P, s) -c\<rightarrow> (None, t); (None, t)#xs \<in> cptn_mod \<rbrakk> \<Longrightarrow> (Some P,s)#(None, t)#xs \<in>cptn_mod" |
|
110 CptnModCondT: "\<lbrakk>(Some P0, s)#ys \<in> cptn_mod; s \<in> b \<rbrakk> \<Longrightarrow> (Some(Cond b P0 P1), s)#(Some P0, s)#ys \<in> cptn_mod" |
|
111 CptnModCondF: "\<lbrakk>(Some P1, s)#ys \<in> cptn_mod; s \<notin> b \<rbrakk> \<Longrightarrow> (Some(Cond b P0 P1), s)#(Some P1, s)#ys \<in> cptn_mod" |
|
112 CptnModSeq1: "\<lbrakk>(Some P0, s)#xs \<in> cptn_mod; zs=map (lift P1) xs \<rbrakk> |
|
113 \<Longrightarrow> (Some(Seq P0 P1), s)#zs \<in> cptn_mod" |
|
114 CptnModSeq2: |
|
115 "\<lbrakk>(Some P0, s)#xs \<in> cptn_mod; fst(last ((Some P0, s)#xs)) = None; |
|
116 (Some P1, snd(last ((Some P0, s)#xs)))#ys \<in> cptn_mod; |
|
117 zs=(map (lift P1) xs)@ys \<rbrakk> \<Longrightarrow> (Some(Seq P0 P1), s)#zs \<in> cptn_mod" |
|
118 |
|
119 CptnModWhile1: |
|
120 "\<lbrakk> (Some P, s)#xs \<in> cptn_mod; s \<in> b; zs=map (lift (While b P)) xs \<rbrakk> |
|
121 \<Longrightarrow> (Some(While b P), s)#(Some(Seq P (While b P)), s)#zs \<in> cptn_mod" |
|
122 CptnModWhile2: |
|
123 "\<lbrakk> (Some P, s)#xs \<in> cptn_mod; fst(last ((Some P, s)#xs))=None; s \<in> b; |
|
124 zs=(map (lift (While b P)) xs)@ys; |
|
125 (Some(While b P), snd(last ((Some P, s)#xs)))#ys \<in> cptn_mod\<rbrakk> |
|
126 \<Longrightarrow> (Some(While b P), s)#(Some(Seq P (While b P)), s)#zs \<in> cptn_mod" |
|
127 |
|
128 subsection {* Equivalence of Both Definitions.*} |
|
129 |
|
130 lemma last_length: "((a#xs)!(length xs))=last (a#xs)" |
|
131 apply simp |
|
132 apply(induct xs,simp+) |
|
133 apply(case_tac list) |
|
134 apply simp_all |
|
135 done |
|
136 |
|
137 lemma div_seq [rule_format]: "list \<in> cptn_mod \<Longrightarrow> |
|
138 (\<forall>s P Q zs. list=(Some (Seq P Q), s)#zs \<longrightarrow> |
|
139 (\<exists>xs. (Some P, s)#xs \<in> cptn_mod \<and> (zs=(map (lift Q) xs) \<or> |
|
140 ( fst(((Some P, s)#xs)!length xs)=None \<and> |
|
141 (\<exists>ys. (Some Q, snd(((Some P, s)#xs)!length xs))#ys \<in> cptn_mod |
|
142 \<and> zs=(map (lift (Q)) xs)@ys)))))" |
|
143 apply(erule cptn_mod.induct) |
|
144 apply simp_all |
|
145 apply clarify |
|
146 apply(force intro:CptnModOne) |
|
147 apply clarify |
|
148 apply(erule_tac x=Pa in allE) |
|
149 apply(erule_tac x=Q in allE) |
|
150 apply simp |
|
151 apply clarify |
|
152 apply(erule disjE) |
|
153 apply(rule_tac x="(Some Pa,t)#xsa" in exI) |
|
154 apply(rule conjI) |
|
155 apply clarify |
|
156 apply(erule CptnModEnv) |
|
157 apply(rule disjI1) |
|
158 apply(simp add:lift_def) |
|
159 apply clarify |
|
160 apply(rule_tac x="(Some Pa,t)#xsa" in exI) |
|
161 apply(rule conjI) |
|
162 apply(erule CptnModEnv) |
|
163 apply(rule disjI2) |
|
164 apply(rule conjI) |
|
165 apply(case_tac xsa,simp,simp) |
|
166 apply(rule_tac x="ys" in exI) |
|
167 apply(rule conjI) |
|
168 apply simp |
|
169 apply(simp add:lift_def) |
|
170 apply clarify |
|
171 apply(erule ctran.elims,simp_all) |
|
172 apply clarify |
|
173 apply(rule_tac x="xs" in exI) |
|
174 apply simp |
|
175 apply clarify |
|
176 apply(rule_tac x="xs" in exI) |
|
177 apply(simp add: last_length) |
|
178 done |
|
179 |
|
180 lemma cptn_onlyif_cptn_mod_aux [rule_format]: |
|
181 "\<forall>s Q t xs.((Some a, s), Q, t) \<in> ctran \<longrightarrow> (Q, t) # xs \<in> cptn_mod |
|
182 \<longrightarrow> (Some a, s) # (Q, t) # xs \<in> cptn_mod" |
|
183 apply(induct a) |
|
184 apply simp_all |
|
185 --{* basic *} |
|
186 apply clarify |
|
187 apply(erule ctran.elims,simp_all) |
|
188 apply(rule CptnModNone,rule Basic,simp) |
|
189 apply clarify |
|
190 apply(erule ctran.elims,simp_all) |
|
191 --{* Seq1 *} |
|
192 apply(rule_tac xs="[(None,ta)]" in CptnModSeq2) |
|
193 apply(erule CptnModNone) |
|
194 apply(rule CptnModOne) |
|
195 apply simp |
|
196 apply simp |
|
197 apply(simp add:lift_def) |
|
198 --{* Seq2 *} |
|
199 apply(erule_tac x=sa in allE) |
|
200 apply(erule_tac x="Some P2" in allE) |
|
201 apply(erule allE,erule impE, assumption) |
|
202 apply(drule div_seq,simp) |
|
203 apply force |
|
204 apply clarify |
|
205 apply(erule disjE) |
|
206 apply clarify |
|
207 apply(erule allE,erule impE, assumption) |
|
208 apply(erule_tac CptnModSeq1) |
|
209 apply(simp add:lift_def) |
|
210 apply clarify |
|
211 apply(erule allE,erule impE, assumption) |
|
212 apply(erule_tac CptnModSeq2) |
|
213 apply (simp add:last_length) |
|
214 apply (simp add:last_length) |
|
215 apply(simp add:lift_def) |
|
216 --{* Cond *} |
|
217 apply clarify |
|
218 apply(erule ctran.elims,simp_all) |
|
219 apply(force elim: CptnModCondT) |
|
220 apply(force elim: CptnModCondF) |
|
221 --{* While *} |
|
222 apply clarify |
|
223 apply(erule ctran.elims,simp_all) |
|
224 apply(rule CptnModNone,erule WhileF,simp) |
|
225 apply(drule div_seq,force) |
|
226 apply clarify |
|
227 apply (erule disjE) |
|
228 apply(force elim:CptnModWhile1) |
|
229 apply clarify |
|
230 apply(force simp add:last_length elim:CptnModWhile2) |
|
231 --{* await *} |
|
232 apply clarify |
|
233 apply(erule ctran.elims,simp_all) |
|
234 apply(rule CptnModNone,erule Await,simp+) |
|
235 done |
|
236 |
|
237 lemma cptn_onlyif_cptn_mod [rule_format]: "c \<in> cptn \<Longrightarrow> c \<in> cptn_mod" |
|
238 apply(erule cptn.induct) |
|
239 apply(rule CptnModOne) |
|
240 apply(erule CptnModEnv) |
|
241 apply(case_tac P) |
|
242 apply simp |
|
243 apply(erule ctran.elims,simp_all) |
|
244 apply(force elim:cptn_onlyif_cptn_mod_aux) |
|
245 done |
|
246 |
|
247 lemma lift_is_cptn: "c\<in>cptn \<Longrightarrow> map (lift P) c \<in> cptn" |
|
248 apply(erule cptn.induct) |
|
249 apply(force simp add:lift_def CptnOne) |
|
250 apply(force intro:CptnEnv simp add:lift_def) |
|
251 apply(force simp add:lift_def intro:CptnComp Seq2 Seq1 elim:ctran.elims) |
|
252 done |
|
253 |
|
254 lemma cptn_append_is_cptn [rule_format]: |
|
255 "\<forall>b a. b#c1\<in>cptn \<longrightarrow> a#c2\<in>cptn \<longrightarrow> (b#c1)!length c1=a \<longrightarrow> b#c1@c2\<in>cptn" |
|
256 apply(induct c1) |
|
257 apply simp |
|
258 apply clarify |
|
259 apply(erule cptn.elims,simp_all) |
|
260 apply(force intro:CptnEnv) |
|
261 apply(force elim:CptnComp) |
|
262 done |
|
263 |
|
264 lemma last_lift: "\<lbrakk>xs\<noteq>[]; fst(xs!(length xs - (Suc 0)))=None\<rbrakk> |
|
265 \<Longrightarrow> fst((map (lift P) xs)!(length (map (lift P) xs)- (Suc 0)))=(Some P)" |
|
266 apply(case_tac "(xs ! (length xs - (Suc 0)))") |
|
267 apply (simp add:lift_def) |
|
268 done |
|
269 |
|
270 lemma last_fst [rule_format]: "P((a#x)!length x) \<longrightarrow> \<not>P a \<longrightarrow> P (x!(length x - (Suc 0)))" |
|
271 apply(induct x,simp+) |
|
272 done |
|
273 |
|
274 lemma last_fst_esp: |
|
275 "fst(((Some a,s)#xs)!(length xs))=None \<Longrightarrow> fst(xs!(length xs - (Suc 0)))=None" |
|
276 apply(erule last_fst) |
|
277 apply simp |
|
278 done |
|
279 |
|
280 lemma last_snd: "xs\<noteq>[] \<Longrightarrow> |
|
281 snd(((map (lift P) xs))!(length (map (lift P) xs) - (Suc 0)))=snd(xs!(length xs - (Suc 0)))" |
|
282 apply(case_tac "(xs ! (length xs - (Suc 0)))",simp) |
|
283 apply (simp add:lift_def) |
|
284 done |
|
285 |
|
286 lemma Cons_lift: "(Some (Seq P Q), s) # (map (lift Q) xs) = map (lift Q) ((Some P, s) # xs)" |
|
287 by(simp add:lift_def) |
|
288 |
|
289 lemma Cons_lift_append: |
|
290 "(Some (Seq P Q), s) # (map (lift Q) xs) @ ys = map (lift Q) ((Some P, s) # xs)@ ys " |
|
291 by(simp add:lift_def) |
|
292 |
|
293 lemma lift_nth: "i<length xs \<Longrightarrow> map (lift Q) xs ! i = lift Q (xs! i)" |
|
294 by (simp add:lift_def) |
|
295 |
|
296 lemma snd_lift: "i< length xs \<Longrightarrow> snd(lift Q (xs ! i))= snd (xs ! i)" |
|
297 apply(case_tac "xs!i") |
|
298 apply(simp add:lift_def) |
|
299 done |
|
300 |
|
301 lemma cptn_if_cptn_mod: "c \<in> cptn_mod \<Longrightarrow> c \<in> cptn" |
|
302 apply(erule cptn_mod.induct) |
|
303 apply(rule CptnOne) |
|
304 apply(erule CptnEnv) |
|
305 apply(erule CptnComp,simp) |
|
306 apply(rule CptnComp) |
|
307 apply(erule CondT,simp) |
|
308 apply(rule CptnComp) |
|
309 apply(erule CondF,simp) |
|
310 --{* Seq1 *} |
|
311 apply(erule cptn.elims,simp_all) |
|
312 apply(rule CptnOne) |
|
313 apply clarify |
|
314 apply(drule_tac P=P1 in lift_is_cptn) |
|
315 apply(simp add:lift_def) |
|
316 apply(rule CptnEnv,simp) |
|
317 apply clarify |
|
318 apply(simp add:lift_def) |
|
319 apply(rule conjI) |
|
320 apply clarify |
|
321 apply(rule CptnComp) |
|
322 apply(rule Seq1,simp) |
|
323 apply(drule_tac P=P1 in lift_is_cptn) |
|
324 apply(simp add:lift_def) |
|
325 apply clarify |
|
326 apply(rule CptnComp) |
|
327 apply(rule Seq2,simp) |
|
328 apply(drule_tac P=P1 in lift_is_cptn) |
|
329 apply(simp add:lift_def) |
|
330 --{* Seq2 *} |
|
331 apply(rule cptn_append_is_cptn) |
|
332 apply(drule_tac P=P1 in lift_is_cptn) |
|
333 apply(simp add:lift_def) |
|
334 apply simp |
|
335 apply(case_tac "xs\<noteq>[]") |
|
336 apply(drule_tac P=P1 in last_lift) |
|
337 apply(rule last_fst_esp) |
|
338 apply (simp add:last_length) |
|
339 apply(simp add:Cons_lift del:map.simps) |
|
340 apply(rule conjI, clarify, simp) |
|
341 apply(case_tac "(((Some P0, s) # xs) ! length xs)") |
|
342 apply clarify |
|
343 apply (simp add:lift_def last_length) |
|
344 apply (simp add:last_length) |
|
345 --{* While1 *} |
|
346 apply(rule CptnComp) |
|
347 apply(rule WhileT,simp) |
|
348 apply(drule_tac P="While b P" in lift_is_cptn) |
|
349 apply(simp add:lift_def) |
|
350 --{* While2 *} |
|
351 apply(rule CptnComp) |
|
352 apply(rule WhileT,simp) |
|
353 apply(rule cptn_append_is_cptn) |
|
354 apply(drule_tac P="While b P" in lift_is_cptn) |
|
355 apply(simp add:lift_def) |
|
356 apply simp |
|
357 apply(case_tac "xs\<noteq>[]") |
|
358 apply(drule_tac P="While b P" in last_lift) |
|
359 apply(rule last_fst_esp,simp add:last_length) |
|
360 apply(simp add:Cons_lift del:map.simps) |
|
361 apply(rule conjI, clarify, simp) |
|
362 apply(case_tac "(((Some P, s) # xs) ! length xs)") |
|
363 apply clarify |
|
364 apply (simp add:last_length lift_def) |
|
365 apply simp |
|
366 done |
|
367 |
|
368 theorem cptn_iff_cptn_mod: "(c \<in> cptn) = (c \<in> cptn_mod)" |
|
369 apply(rule iffI) |
|
370 apply(erule cptn_onlyif_cptn_mod) |
|
371 apply(erule cptn_if_cptn_mod) |
|
372 done |
|
373 |
|
374 section {* Validity of Correctness Formulas*} |
|
375 |
|
376 subsection {* Validity for Component Programs. *} |
|
377 |
|
378 types 'a rgformula = "'a com \<times> 'a set \<times> ('a \<times> 'a) set \<times> ('a \<times> 'a) set \<times> 'a set" |
|
379 |
|
380 constdefs |
|
381 assum :: "('a set \<times> ('a \<times> 'a) set) \<Rightarrow> ('a confs) set" |
|
382 "assum \<equiv> \<lambda>(pre, rely). {c. snd(c!0) \<in> pre \<and> (\<forall>i. Suc i<length c \<longrightarrow> |
|
383 c!i -e\<rightarrow> c!(Suc i) \<longrightarrow> (snd(c!i), snd(c!Suc i)) \<in> rely)}" |
|
384 |
|
385 comm :: "(('a \<times> 'a) set \<times> 'a set) \<Rightarrow> ('a confs) set" |
|
386 "comm \<equiv> \<lambda>(guar, post). {c. (\<forall>i. Suc i<length c \<longrightarrow> |
|
387 c!i -c\<rightarrow> c!(Suc i) \<longrightarrow> (snd(c!i), snd(c!Suc i)) \<in> guar) \<and> |
|
388 (fst (last c) = None \<longrightarrow> snd (last c) \<in> post)}" |
|
389 |
|
390 com_validity :: "'a com \<Rightarrow> 'a set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> 'a set \<Rightarrow> bool" |
|
391 ("\<Turnstile> _ sat [_, _, _, _]" [60,0,0,0,0] 45) |
|
392 "\<Turnstile> P sat [pre, rely, guar, post] \<equiv> |
|
393 \<forall>s. cp (Some P) s \<inter> assum(pre, rely) \<subseteq> comm(guar, post)" |
|
394 |
|
395 subsection {* Validity for Parallel Programs. *} |
|
396 |
|
397 constdefs |
|
398 All_None :: "(('a com) option) list \<Rightarrow> bool" |
|
399 "All_None xs \<equiv> \<forall>c\<in>set xs. c=None" |
|
400 |
|
401 par_assum :: "('a set \<times> ('a \<times> 'a) set) \<Rightarrow> ('a par_confs) set" |
|
402 "par_assum \<equiv> \<lambda>(pre, rely). {c. snd(c!0) \<in> pre \<and> (\<forall>i. Suc i<length c \<longrightarrow> |
|
403 c!i -pe\<rightarrow> c!Suc i \<longrightarrow> (snd(c!i), snd(c!Suc i)) \<in> rely)}" |
|
404 |
|
405 par_comm :: "(('a \<times> 'a) set \<times> 'a set) \<Rightarrow> ('a par_confs) set" |
|
406 "par_comm \<equiv> \<lambda>(guar, post). {c. (\<forall>i. Suc i<length c \<longrightarrow> |
|
407 c!i -pc\<rightarrow> c!Suc i \<longrightarrow> (snd(c!i), snd(c!Suc i)) \<in> guar) \<and> |
|
408 (All_None (fst (last c)) \<longrightarrow> snd( last c) \<in> post)}" |
|
409 |
|
410 par_com_validity :: "'a par_com \<Rightarrow> 'a set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> 'a set |
|
411 \<Rightarrow> bool" ("\<Turnstile> _ SAT [_, _, _, _]" [60,0,0,0,0] 45) |
|
412 "\<Turnstile> Ps SAT [pre, rely, guar, post] \<equiv> |
|
413 \<forall>s. par_cp Ps s \<inter> par_assum(pre, rely) \<subseteq> par_comm(guar, post)" |
|
414 |
|
415 subsection {* Compositionality of the Semantics *} |
|
416 |
|
417 subsubsection {* Definition of the conjoin operator *} |
|
418 |
|
419 constdefs |
|
420 same_length :: "'a par_confs \<Rightarrow> ('a confs) list \<Rightarrow> bool" |
|
421 "same_length c clist \<equiv> (\<forall>i<length clist. length(clist!i)=length c)" |
|
422 |
|
423 same_state :: "'a par_confs \<Rightarrow> ('a confs) list \<Rightarrow> bool" |
|
424 "same_state c clist \<equiv> (\<forall>i <length clist. \<forall>j<length c. snd(c!j) = snd((clist!i)!j))" |
|
425 |
|
426 same_program :: "'a par_confs \<Rightarrow> ('a confs) list \<Rightarrow> bool" |
|
427 "same_program c clist \<equiv> (\<forall>j<length c. fst(c!j) = map (\<lambda>x. fst(nth x j)) clist)" |
|
428 |
|
429 compat_label :: "'a par_confs \<Rightarrow> ('a confs) list \<Rightarrow> bool" |
|
430 "compat_label c clist \<equiv> (\<forall>j. Suc j<length c \<longrightarrow> |
|
431 (c!j -pc\<rightarrow> c!Suc j \<and> (\<exists>i<length clist. (clist!i)!j -c\<rightarrow> (clist!i)! Suc j \<and> |
|
432 (\<forall>l<length clist. l\<noteq>i \<longrightarrow> (clist!l)!j -e\<rightarrow> (clist!l)! Suc j))) \<or> |
|
433 (c!j -pe\<rightarrow> c!Suc j \<and> (\<forall>i<length clist. (clist!i)!j -e\<rightarrow> (clist!i)! Suc j)))" |
|
434 |
|
435 conjoin :: "'a par_confs \<Rightarrow> ('a confs) list \<Rightarrow> bool" ("_ \<propto> _" [65,65] 64) |
|
436 "c \<propto> clist \<equiv> (same_length c clist) \<and> (same_state c clist) \<and> (same_program c clist) \<and> (compat_label c clist)" |
|
437 |
|
438 subsubsection {* Some previous lemmas *} |
|
439 |
|
440 lemma list_eq_if [rule_format]: "\<forall>ys. xs=ys \<longrightarrow> (length xs = length ys) \<longrightarrow> (\<forall>i<length xs. xs!i=ys!i)" |
|
441 apply (induct xs) |
|
442 apply simp |
|
443 apply clarify |
|
444 done |
|
445 |
|
446 lemma list_eq: "(length xs = length ys \<and> (\<forall>i<length xs. xs!i=ys!i)) = (xs=ys)" |
|
447 apply(rule iffI) |
|
448 apply clarify |
|
449 apply(erule nth_equalityI) |
|
450 apply simp+ |
|
451 done |
|
452 |
|
453 lemma nth_tl: "\<lbrakk> ys!0=a; ys\<noteq>[] \<rbrakk> \<Longrightarrow> ys=(a#(tl ys))" |
|
454 apply(case_tac ys) |
|
455 apply simp+ |
|
456 done |
|
457 |
|
458 lemma nth_tl_if [rule_format]: "ys\<noteq>[] \<longrightarrow> ys!0=a \<longrightarrow> P ys \<longrightarrow> P (a#(tl ys))" |
|
459 apply(induct ys) |
|
460 apply simp+ |
|
461 done |
|
462 |
|
463 lemma nth_tl_onlyif [rule_format]: "ys\<noteq>[] \<longrightarrow> ys!0=a \<longrightarrow> P (a#(tl ys)) \<longrightarrow> P ys" |
|
464 apply(induct ys) |
|
465 apply simp+ |
|
466 done |
|
467 |
|
468 lemma seq_not_eq1: "Seq c1 c2\<noteq>c1" |
|
469 apply(rule com.induct) |
|
470 apply simp_all |
|
471 apply clarify |
|
472 done |
|
473 |
|
474 lemma seq_not_eq2: "Seq c1 c2\<noteq>c2" |
|
475 apply(rule com.induct) |
|
476 apply simp_all |
|
477 apply clarify |
|
478 done |
|
479 |
|
480 lemma if_not_eq1: "Cond b c1 c2 \<noteq>c1" |
|
481 apply(rule com.induct) |
|
482 apply simp_all |
|
483 apply clarify |
|
484 done |
|
485 |
|
486 lemma if_not_eq2: "Cond b c1 c2\<noteq>c2" |
|
487 apply(rule com.induct) |
|
488 apply simp_all |
|
489 apply clarify |
|
490 done |
|
491 |
|
492 lemmas seq_and_if_not_eq [simp] = seq_not_eq1 seq_not_eq2 |
|
493 seq_not_eq1 [THEN not_sym] seq_not_eq2 [THEN not_sym] |
|
494 if_not_eq1 if_not_eq2 if_not_eq1 [THEN not_sym] if_not_eq2 [THEN not_sym] |
|
495 |
|
496 lemma prog_not_eq_in_ctran_aux [rule_format]: "(P,s) -c\<rightarrow> (Q,t) \<Longrightarrow> (P\<noteq>Q)" |
|
497 apply(erule ctran.induct) |
|
498 apply simp_all |
|
499 done |
|
500 |
|
501 lemma prog_not_eq_in_ctran [simp]: "\<not> (P,s) -c\<rightarrow> (P,t)" |
|
502 apply clarify |
|
503 apply(drule prog_not_eq_in_ctran_aux) |
|
504 apply simp |
|
505 done |
|
506 |
|
507 lemma prog_not_eq_in_par_ctran_aux [rule_format]: "(P,s) -pc\<rightarrow> (Q,t) \<Longrightarrow> (P\<noteq>Q)" |
|
508 apply(erule par_ctran.induct) |
|
509 apply(drule prog_not_eq_in_ctran_aux) |
|
510 apply clarify |
|
511 apply(drule list_eq_if) |
|
512 apply simp_all |
|
513 apply force |
|
514 done |
|
515 |
|
516 lemma prog_not_eq_in_par_ctran [simp]: "\<not> (P,s) -pc\<rightarrow> (P,t)" |
|
517 apply clarify |
|
518 apply(drule prog_not_eq_in_par_ctran_aux) |
|
519 apply simp |
|
520 done |
|
521 |
|
522 lemma tl_in_cptn: "\<lbrakk> a#xs \<in>cptn; xs\<noteq>[] \<rbrakk> \<Longrightarrow> xs\<in>cptn" |
|
523 apply(force elim:cptn.elims) |
|
524 done |
|
525 |
|
526 lemma tl_zero[rule_format]: "P (ys!Suc j) \<longrightarrow> Suc j<length ys \<longrightarrow> ys\<noteq>[] \<longrightarrow> P (tl(ys)!j)" |
|
527 apply(induct ys) |
|
528 apply simp_all |
|
529 done |
|
530 |
|
531 subsection {* The Semantics is Compositional *} |
|
532 |
|
533 lemma aux_if [rule_format]: |
|
534 "\<forall>xs s clist. (length clist = length xs \<and> (\<forall>i<length xs. (xs!i,s)#clist!i \<in> cptn) |
|
535 \<and> ((xs, s)#ys \<propto> map (\<lambda>i. (fst i,s)#snd i) (zip xs clist)) |
|
536 \<longrightarrow> (xs, s)#ys \<in> par_cptn)" |
|
537 apply(induct ys) |
|
538 apply(clarify) |
|
539 apply(rule ParCptnOne) |
|
540 apply(clarify) |
|
541 apply(simp add:conjoin_def compat_label_def) |
|
542 apply clarify |
|
543 apply(erule_tac x="0" and P="\<lambda>j. ?H j \<longrightarrow> (?P j \<or> ?Q j)" in all_dupE,simp) |
|
544 apply(erule disjE) |
|
545 --{* first step is a Component step *} |
|
546 apply clarify |
|
547 apply simp |
|
548 apply(subgoal_tac "a=(xs[i:=(fst(clist!i!0))])") |
|
549 apply(subgoal_tac "b=snd(clist!i!0)",simp) |
|
550 prefer 2 |
|
551 apply(simp add: same_state_def) |
|
552 apply(erule_tac x=i in allE,erule impE,assumption, |
|
553 erule_tac x=1 and P="\<lambda>j. (?H j) \<longrightarrow> (snd (?d j))=(snd (?e j))" in allE,simp) |
|
554 prefer 2 |
|
555 apply(simp add:same_program_def) |
|
556 apply(erule_tac x=1 and P="\<lambda>j. ?H j \<longrightarrow> (fst (?s j))=(?t j)" in allE,simp) |
|
557 apply(rule nth_equalityI,simp) |
|
558 apply clarify |
|
559 apply(case_tac "i=ia",simp,simp) |
|
560 apply(erule_tac x=ia and P="\<lambda>j. ?H j \<longrightarrow> ?I j \<longrightarrow> ?J j" in allE) |
|
561 apply(drule_tac t=i in not_sym,simp) |
|
562 apply(erule etran.elims,simp) |
|
563 apply(rule ParCptnComp) |
|
564 apply(erule ParComp,simp) |
|
565 --{* applying the induction hypothesis *} |
|
566 apply(erule_tac x="xs[i := fst (clist ! i ! 0)]" in allE) |
|
567 apply(erule_tac x="snd (clist ! i ! 0)" in allE) |
|
568 apply(erule mp) |
|
569 apply(rule_tac x="map tl clist" in exI,simp) |
|
570 apply(rule conjI,clarify) |
|
571 apply(case_tac "i=ia",simp) |
|
572 apply(rule nth_tl_if) |
|
573 apply(force simp add:same_length_def length_Suc_conv) |
|
574 apply simp |
|
575 apply(erule allE,erule impE,assumption,erule tl_in_cptn) |
|
576 apply(force simp add:same_length_def length_Suc_conv) |
|
577 apply(rule nth_tl_if) |
|
578 apply(force simp add:same_length_def length_Suc_conv) |
|
579 apply(simp add:same_state_def) |
|
580 apply(erule_tac x=ia in allE, erule impE, assumption, |
|
581 erule_tac x=1 and P="\<lambda>j. ?H j \<longrightarrow> (snd (?d j))=(snd (?e j))" in allE) |
|
582 apply(erule_tac x=ia and P="\<lambda>j. ?H j \<longrightarrow> ?I j \<longrightarrow> ?J j" in allE) |
|
583 apply(drule_tac t=i in not_sym,simp) |
|
584 apply(erule etran.elims,simp) |
|
585 apply(erule allE,erule impE,assumption,erule tl_in_cptn) |
|
586 apply(force simp add:same_length_def length_Suc_conv) |
|
587 apply(simp add:same_length_def same_state_def) |
|
588 apply(rule conjI) |
|
589 apply clarify |
|
590 apply(case_tac j,simp,simp) |
|
591 apply(erule_tac x=ia in allE, erule impE, assumption, |
|
592 erule_tac x="Suc(Suc nat)" and P="\<lambda>j. ?H j \<longrightarrow> (snd (?d j))=(snd (?e j))" in allE,simp) |
|
593 apply(force simp add:same_length_def length_Suc_conv) |
|
594 apply(rule conjI) |
|
595 apply(simp add:same_program_def) |
|
596 apply clarify |
|
597 apply(case_tac j,simp) |
|
598 apply(rule nth_equalityI,simp) |
|
599 apply clarify |
|
600 apply(case_tac "i=ia",simp,simp) |
|
601 apply(erule_tac x="Suc(Suc nat)" and P="\<lambda>j. ?H j \<longrightarrow> (fst (?s j))=(?t j)" in allE,simp) |
|
602 apply(rule nth_equalityI,simp,simp) |
|
603 apply(force simp add:length_Suc_conv) |
|
604 apply(rule allI,rule impI) |
|
605 apply(erule_tac x="Suc j" and P="\<lambda>j. ?H j \<longrightarrow> (?I j \<or> ?J j)" in allE,simp) |
|
606 apply(erule disjE) |
|
607 apply clarify |
|
608 apply(rule_tac x=ia in exI,simp) |
|
609 apply(case_tac "i=ia",simp) |
|
610 apply(rule conjI) |
|
611 apply(force simp add: length_Suc_conv) |
|
612 apply clarify |
|
613 apply(erule_tac x=l and P="\<lambda>j. ?H j \<longrightarrow> ?I j \<longrightarrow> ?J j" in allE,erule impE,assumption) |
|
614 apply(erule_tac x=l and P="\<lambda>j. ?H j \<longrightarrow> ?I j \<longrightarrow> ?J j" in allE,erule impE,assumption) |
|
615 apply simp |
|
616 apply(case_tac j,simp) |
|
617 apply(rule tl_zero) |
|
618 apply(drule_tac t=l in not_sym,simp) |
|
619 apply(erule_tac x=l in allE, erule impE, assumption, |
|
620 erule_tac x=1 and P="\<lambda>j. (?H j) \<longrightarrow> (snd (?d j))=(snd (?e j))" in allE,simp) |
|
621 apply(force elim:etran.elims intro:Env) |
|
622 apply force |
|
623 apply force |
|
624 apply simp |
|
625 apply(rule tl_zero) |
|
626 apply(erule tl_zero) |
|
627 apply force |
|
628 apply force |
|
629 apply force |
|
630 apply force |
|
631 apply(rule conjI,simp) |
|
632 apply(rule nth_tl_if) |
|
633 apply force |
|
634 apply(erule_tac x=ia in allE, erule impE, assumption, |
|
635 erule_tac x=1 and P="\<lambda>j. ?H j \<longrightarrow> (snd (?d j))=(snd (?e j))" in allE) |
|
636 apply(erule_tac x=ia and P="\<lambda>j. ?H j \<longrightarrow> ?I j \<longrightarrow> ?J j" in allE) |
|
637 apply(drule_tac t=i in not_sym,simp) |
|
638 apply(erule etran.elims,simp) |
|
639 apply(erule tl_zero) |
|
640 apply force |
|
641 apply force |
|
642 apply clarify |
|
643 apply(case_tac "i=l",simp) |
|
644 apply(rule nth_tl_if) |
|
645 apply(erule_tac x=l and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE,force) |
|
646 apply simp |
|
647 apply(erule_tac P="\<lambda>j. ?H j \<longrightarrow> ?I j \<longrightarrow> ?J j" in allE,erule impE,assumption,erule impE,assumption) |
|
648 apply(erule tl_zero,force) |
|
649 apply(erule_tac x=l and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE,force) |
|
650 apply(rule nth_tl_if) |
|
651 apply(erule_tac x=l and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE,force) |
|
652 apply(erule_tac x=l in allE, erule impE, assumption, |
|
653 erule_tac x=1 and P="\<lambda>j. ?H j \<longrightarrow> (snd (?d j))=(snd (?e j))" in allE) |
|
654 apply(erule_tac x=l and P="\<lambda>j. ?H j \<longrightarrow> ?I j \<longrightarrow> ?J j" in allE,erule impE, assumption,simp) |
|
655 apply(drule not_sym,erule impE,assumption ) |
|
656 apply(erule etran.elims,simp) |
|
657 apply(rule tl_zero) |
|
658 apply force |
|
659 apply force |
|
660 apply(erule_tac x=l and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE,force) |
|
661 apply(rule disjI2) |
|
662 apply(case_tac j,simp) |
|
663 apply clarify |
|
664 apply(rule tl_zero) |
|
665 apply(erule_tac x=ia and P="\<lambda>j. ?H j \<longrightarrow> ?I j\<in>etran" in allE,erule impE, assumption) |
|
666 apply(case_tac "i=ia",simp,simp) |
|
667 apply(erule_tac x=ia in allE, erule impE, assumption, |
|
668 erule_tac x=1 and P="\<lambda>j. ?H j \<longrightarrow> (snd (?d j))=(snd (?e j))" in allE) |
|
669 apply(erule_tac x=ia and P="\<lambda>j. ?H j \<longrightarrow> ?I j \<longrightarrow> ?J j" in allE,erule impE, assumption,simp) |
|
670 apply(drule not_sym,erule impE,assumption) |
|
671 apply(force elim:etran.elims intro:Env) |
|
672 apply force |
|
673 apply(erule_tac x=ia and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE,force) |
|
674 apply simp |
|
675 apply clarify |
|
676 apply(rule tl_zero) |
|
677 apply(rule tl_zero,force) |
|
678 apply force |
|
679 apply(erule_tac x=ia and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE,force) |
|
680 apply force |
|
681 apply(erule_tac x=ia and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE,force) |
|
682 --{* first step is an environmental step *} |
|
683 apply clarify |
|
684 apply(erule par_etran.elims) |
|
685 apply simp |
|
686 apply(rule ParCptnEnv) |
|
687 apply(erule_tac x="Ps" in allE) |
|
688 apply(erule_tac x="t" in allE) |
|
689 apply(erule mp) |
|
690 apply(rule_tac x="map tl clist" in exI,simp) |
|
691 apply(rule conjI) |
|
692 apply clarify |
|
693 apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> (?I ?s j) \<in> cptn" in allE,simp) |
|
694 apply(erule cptn.elims) |
|
695 apply(simp add:same_length_def) |
|
696 apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE,force) |
|
697 apply(simp add:same_state_def) |
|
698 apply(erule_tac x=i in allE, erule impE, assumption, |
|
699 erule_tac x=1 and P="\<lambda>j. ?H j \<longrightarrow> (snd (?d j))=(snd (?e j))" in allE,simp) |
|
700 apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> ?J j \<in>etran" in allE,simp) |
|
701 apply(erule etran.elims,simp) |
|
702 apply(simp add:same_state_def same_length_def) |
|
703 apply(rule conjI,clarify) |
|
704 apply(case_tac j,simp,simp) |
|
705 apply(erule_tac x=i in allE, erule impE, assumption, |
|
706 erule_tac x="Suc(Suc nat)" and P="\<lambda>j. ?H j \<longrightarrow> (snd (?d j))=(snd (?e j))" in allE,simp) |
|
707 apply(rule tl_zero) |
|
708 apply(simp) |
|
709 apply force |
|
710 apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE,force) |
|
711 apply(rule conjI) |
|
712 apply(simp add:same_program_def) |
|
713 apply clarify |
|
714 apply(case_tac j,simp) |
|
715 apply(rule nth_equalityI,simp) |
|
716 apply clarify |
|
717 apply simp |
|
718 apply(erule_tac x="Suc(Suc nat)" and P="\<lambda>j. ?H j \<longrightarrow> (fst (?s j))=(?t j)" in allE,simp) |
|
719 apply(rule nth_equalityI,simp,simp) |
|
720 apply(force simp add:length_Suc_conv) |
|
721 apply(rule allI,rule impI) |
|
722 apply(erule_tac x="Suc j" and P="\<lambda>j. ?H j \<longrightarrow> (?I j \<or> ?J j)" in allE,simp) |
|
723 apply(erule disjE) |
|
724 apply clarify |
|
725 apply(rule_tac x=i in exI,simp) |
|
726 apply(rule conjI) |
|
727 apply(erule_tac x=i and P="\<lambda>i. ?H i \<longrightarrow> ?J i \<in>etran" in allE, erule impE, assumption) |
|
728 apply(erule etran.elims,simp) |
|
729 apply(erule_tac x=i in allE, erule impE, assumption, |
|
730 erule_tac x=1 and P="\<lambda>j. (?H j) \<longrightarrow> (snd (?d j))=(snd (?e j))" in allE,simp) |
|
731 apply(rule nth_tl_if) |
|
732 apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE,force) |
|
733 apply simp |
|
734 apply(erule tl_zero,force) |
|
735 apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE,force) |
|
736 apply clarify |
|
737 apply(erule_tac x=l and P="\<lambda>i. ?H i \<longrightarrow> ?J i \<in>etran" in allE, erule impE, assumption) |
|
738 apply(erule etran.elims,simp) |
|
739 apply(erule_tac x=l in allE, erule impE, assumption, |
|
740 erule_tac x=1 and P="\<lambda>j. (?H j) \<longrightarrow> (snd (?d j))=(snd (?e j))" in allE,simp) |
|
741 apply(rule nth_tl_if) |
|
742 apply(erule_tac x=l and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE,force) |
|
743 apply simp |
|
744 apply(rule tl_zero,force) |
|
745 apply force |
|
746 apply(erule_tac x=l and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE,force) |
|
747 apply(rule disjI2) |
|
748 apply simp |
|
749 apply clarify |
|
750 apply(case_tac j,simp) |
|
751 apply(rule tl_zero) |
|
752 apply(erule_tac x=i and P="\<lambda>i. ?H i \<longrightarrow> ?J i \<in>etran" in allE, erule impE, assumption) |
|
753 apply(erule_tac x=i and P="\<lambda>i. ?H i \<longrightarrow> ?J i \<in>etran" in allE, erule impE, assumption) |
|
754 apply(force elim:etran.elims intro:Env) |
|
755 apply force |
|
756 apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE,force) |
|
757 apply simp |
|
758 apply(rule tl_zero) |
|
759 apply(rule tl_zero,force) |
|
760 apply force |
|
761 apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE,force) |
|
762 apply force |
|
763 apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE,force) |
|
764 done |
|
765 |
|
766 lemma less_Suc_0 [iff]: "(n < Suc 0) = (n = 0)" |
|
767 by auto |
|
768 |
|
769 lemma aux_onlyif [rule_format]: "\<forall>xs s. (xs, s)#ys \<in> par_cptn \<longrightarrow> |
|
770 (\<exists>clist. (length clist = length xs) \<and> |
|
771 (xs, s)#ys \<propto> map (\<lambda>i. (fst i,s)#(snd i)) (zip xs clist) \<and> |
|
772 (\<forall>i<length xs. (xs!i,s)#(clist!i) \<in> cptn))" |
|
773 apply(induct ys) |
|
774 apply(clarify) |
|
775 apply(rule_tac x="map (\<lambda>i. []) [0..length xs(]" in exI) |
|
776 apply(simp add: conjoin_def same_length_def same_state_def same_program_def compat_label_def) |
|
777 apply(rule conjI) |
|
778 apply(rule nth_equalityI,simp,simp) |
|
779 apply(force intro: cptn.intros) |
|
780 apply(clarify) |
|
781 apply(erule par_cptn.elims,simp) |
|
782 apply simp |
|
783 apply(erule_tac x="xs" in allE) |
|
784 apply(erule_tac x="t" in allE,simp) |
|
785 apply clarify |
|
786 apply(rule_tac x="(map (\<lambda>j. (P!j, t)#(clist!j)) [0..length P(])" in exI,simp) |
|
787 apply(rule conjI) |
|
788 prefer 2 |
|
789 apply clarify |
|
790 apply(rule CptnEnv,simp) |
|
791 apply(simp add:conjoin_def same_length_def same_state_def) |
|
792 apply (rule conjI) |
|
793 apply clarify |
|
794 apply(case_tac j,simp,simp) |
|
795 apply(rule conjI) |
|
796 apply(simp add:same_program_def) |
|
797 apply clarify |
|
798 apply(case_tac j,simp) |
|
799 apply(rule nth_equalityI,simp,simp) |
|
800 apply simp |
|
801 apply(rule nth_equalityI,simp,simp) |
|
802 apply(simp add:compat_label_def) |
|
803 apply clarify |
|
804 apply(case_tac j,simp) |
|
805 apply(simp add:ParEnv) |
|
806 apply clarify |
|
807 apply(simp add:Env) |
|
808 apply simp |
|
809 apply(erule_tac x=nat in allE,erule impE, assumption) |
|
810 apply(erule disjE,simp) |
|
811 apply clarify |
|
812 apply(rule_tac x=i in exI,simp) |
|
813 apply force |
|
814 apply(erule par_ctran.elims,simp) |
|
815 apply(erule_tac x="Ps[i:=r]" in allE) |
|
816 apply(erule_tac x="ta" in allE,simp) |
|
817 apply clarify |
|
818 apply(rule_tac x="(map (\<lambda>j. (Ps!j, ta)#(clist!j)) [0..length Ps(]) [i:=((r, ta)#(clist!i))]" in exI,simp) |
|
819 apply(rule conjI) |
|
820 prefer 2 |
|
821 apply clarify |
|
822 apply(case_tac "i=ia",simp) |
|
823 apply(erule CptnComp) |
|
824 apply(erule_tac x=ia and P="\<lambda>j. ?H j \<longrightarrow> (?I j \<in> cptn)" in allE,simp) |
|
825 apply simp |
|
826 apply(erule_tac x=ia in allE) |
|
827 apply(rule CptnEnv,simp) |
|
828 apply(simp add:conjoin_def) |
|
829 apply (rule conjI) |
|
830 apply(simp add:same_length_def) |
|
831 apply clarify |
|
832 apply(case_tac "i=ia",simp,simp) |
|
833 apply(rule conjI) |
|
834 apply(simp add:same_state_def) |
|
835 apply clarify |
|
836 apply(case_tac j,simp,simp) |
|
837 apply(case_tac "i=ia",simp,simp) |
|
838 apply(rule conjI) |
|
839 apply(simp add:same_program_def) |
|
840 apply clarify |
|
841 apply(case_tac j,simp) |
|
842 apply(rule nth_equalityI,simp,simp) |
|
843 apply simp |
|
844 apply(rule nth_equalityI,simp,simp) |
|
845 apply(erule_tac x=nat and P="\<lambda>j. ?H j \<longrightarrow> (fst (?a j))=((?b j))" in allE) |
|
846 apply(case_tac nat) |
|
847 apply clarify |
|
848 apply(case_tac "i=ia",simp,simp) |
|
849 apply clarify |
|
850 apply(case_tac "i=ia",simp,simp) |
|
851 apply(simp add:compat_label_def) |
|
852 apply clarify |
|
853 apply(case_tac j) |
|
854 apply(rule conjI,simp) |
|
855 apply(erule ParComp,assumption) |
|
856 apply clarify |
|
857 apply(rule_tac x=i in exI,simp) |
|
858 apply clarify |
|
859 apply(drule not_sym,simp) |
|
860 apply(rule Env) |
|
861 apply simp |
|
862 apply(erule_tac x=nat and P="\<lambda>j. ?H j \<longrightarrow> (?P j \<or> ?Q j)" in allE,simp) |
|
863 apply(erule disjE) |
|
864 apply clarify |
|
865 apply(rule_tac x=ia in exI,simp) |
|
866 apply(rule conjI) |
|
867 apply(case_tac "i=ia",simp,simp) |
|
868 apply(rotate_tac -1,simp) |
|
869 apply clarify |
|
870 apply(case_tac "i=l",simp) |
|
871 apply(case_tac "l=ia",simp,simp) |
|
872 apply(erule_tac x=l in allE,erule impE,assumption,erule impE, assumption,simp) |
|
873 apply simp |
|
874 apply(erule_tac x=l in allE,erule impE,assumption,erule impE, assumption,simp) |
|
875 apply clarify |
|
876 apply(erule_tac x=ia and P="\<lambda>j. ?H j \<longrightarrow> (?P j)\<in>etran" in allE, erule impE, assumption) |
|
877 apply(case_tac "i=ia",simp) |
|
878 apply(rotate_tac -1,simp) |
|
879 done |
|
880 |
|
881 lemma one_iff_aux: "xs\<noteq>[] \<Longrightarrow> (\<forall>ys. ((xs, s)#ys \<in> par_cptn) = |
|
882 (\<exists>clist. length clist= length xs \<and> |
|
883 ((xs, s)#ys \<propto> map (\<lambda>i. (fst i,s)#(snd i)) (zip xs clist)) \<and> |
|
884 (\<forall>i<length xs. (xs!i,s)#(clist!i) \<in> cptn))) = |
|
885 (par_cp (xs) s = {c. \<exists>clist. (length clist)=(length xs) \<and> |
|
886 (\<forall>i<length clist. (clist!i) \<in> cp(xs!i) s) \<and> c \<propto> clist})" |
|
887 apply (rule iffI) |
|
888 apply(rule subset_antisym) |
|
889 apply(rule subsetI) |
|
890 apply(clarify) |
|
891 apply(simp add:par_cp_def cp_def) |
|
892 apply(case_tac x) |
|
893 apply(force elim:par_cptn.elims) |
|
894 apply simp |
|
895 apply(erule_tac x="list" in allE) |
|
896 apply clarify |
|
897 apply simp |
|
898 apply(rule_tac x="map (\<lambda>i. (fst i, s) # snd i) (zip xs clist)" in exI,simp) |
|
899 apply(rule subsetI) |
|
900 apply(clarify) |
|
901 apply(case_tac x) |
|
902 apply(erule_tac x=0 in allE) |
|
903 apply(simp add:cp_def conjoin_def same_length_def same_program_def same_state_def compat_label_def) |
|
904 apply clarify |
|
905 apply(erule cptn.elims,force,force,force) |
|
906 apply(simp add:par_cp_def conjoin_def same_length_def same_program_def same_state_def compat_label_def) |
|
907 apply clarify |
|
908 apply(erule_tac x=0 and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in all_dupE) |
|
909 apply(subgoal_tac "a = xs") |
|
910 apply(subgoal_tac "b = s",simp) |
|
911 prefer 3 |
|
912 apply(erule_tac x=0 and P="\<lambda>j. ?H j \<longrightarrow> (fst (?s j))=((?t j))" in allE) |
|
913 apply (simp add:cp_def) |
|
914 apply(rule nth_equalityI,simp,simp) |
|
915 prefer 2 |
|
916 apply(erule_tac x=0 in allE) |
|
917 apply (simp add:cp_def) |
|
918 apply(erule_tac x=0 and P="\<lambda>j. ?H j \<longrightarrow> (\<forall>i. ?T i \<longrightarrow> (snd (?d j i))=(snd (?e j i)))" in allE,simp) |
|
919 apply(erule_tac x=0 and P="\<lambda>j. ?H j \<longrightarrow> (snd (?d j))=(snd (?e j))" in allE,simp) |
|
920 apply(erule_tac x=list in allE) |
|
921 apply(rule_tac x="map tl clist" in exI,simp) |
|
922 apply(rule conjI) |
|
923 apply clarify |
|
924 apply(case_tac j,simp) |
|
925 apply(erule_tac x=i in allE, erule impE, assumption, |
|
926 erule_tac x="0" and P="\<lambda>j. ?H j \<longrightarrow> (snd (?d j))=(snd (?e j))" in allE,simp) |
|
927 apply(erule_tac x=i in allE, erule impE, assumption, |
|
928 erule_tac x="Suc nat" and P="\<lambda>j. ?H j \<longrightarrow> (snd (?d j))=(snd (?e j))" in allE) |
|
929 apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE) |
|
930 apply(case_tac "clist!i",simp,simp) |
|
931 apply(rule conjI) |
|
932 apply clarify |
|
933 apply(rule nth_equalityI,simp,simp) |
|
934 apply(case_tac j) |
|
935 apply clarify |
|
936 apply(erule_tac x=i in allE) |
|
937 apply(simp add:cp_def) |
|
938 apply clarify |
|
939 apply simp |
|
940 apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE) |
|
941 apply(case_tac "clist!i",simp,simp) |
|
942 apply(thin_tac "?H = (\<exists>i. ?J i)") |
|
943 apply(rule conjI) |
|
944 apply clarify |
|
945 apply(erule_tac x=j in allE,erule impE, assumption,erule disjE) |
|
946 apply clarify |
|
947 apply(rule_tac x=i in exI,simp) |
|
948 apply(case_tac j,simp) |
|
949 apply(rule conjI) |
|
950 apply(erule_tac x=i in allE) |
|
951 apply(simp add:cp_def) |
|
952 apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE) |
|
953 apply(case_tac "clist!i",simp,simp) |
|
954 apply clarify |
|
955 apply(erule_tac x=l in allE) |
|
956 apply(erule_tac x=l and P="\<lambda>j. ?H j \<longrightarrow> ?I j \<longrightarrow> ?J j" in allE) |
|
957 apply clarify |
|
958 apply(simp add:cp_def) |
|
959 apply(erule_tac x=l and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE) |
|
960 apply(case_tac "clist!l",simp,simp) |
|
961 apply simp |
|
962 apply(rule conjI) |
|
963 apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE) |
|
964 apply(case_tac "clist!i",simp,simp) |
|
965 apply clarify |
|
966 apply(erule_tac x=l and P="\<lambda>j. ?H j \<longrightarrow> ?I j \<longrightarrow> ?J j" in allE) |
|
967 apply(erule_tac x=l and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE) |
|
968 apply(case_tac "clist!l",simp,simp) |
|
969 apply clarify |
|
970 apply(erule_tac x=i in allE) |
|
971 apply(simp add:cp_def) |
|
972 apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE) |
|
973 apply(case_tac "clist!i",simp) |
|
974 apply(rule nth_tl_if,simp,simp) |
|
975 apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> (?P j)\<in>etran" in allE, erule impE, assumption,simp) |
|
976 apply(simp add:cp_def) |
|
977 apply clarify |
|
978 apply(rule nth_tl_if) |
|
979 apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE) |
|
980 apply(case_tac "clist!i",simp,simp) |
|
981 apply force |
|
982 apply force |
|
983 apply clarify |
|
984 apply(rule iffI) |
|
985 apply(simp add:par_cp_def) |
|
986 apply(erule_tac c="(xs, s) # ys" in equalityCE) |
|
987 apply simp |
|
988 apply clarify |
|
989 apply(rule_tac x="map tl clist" in exI) |
|
990 apply simp |
|
991 apply (rule conjI) |
|
992 apply(simp add:conjoin_def cp_def) |
|
993 apply(rule conjI) |
|
994 apply clarify |
|
995 apply(unfold same_length_def) |
|
996 apply clarify |
|
997 apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE,simp) |
|
998 apply(rule conjI) |
|
999 apply(simp add:same_state_def) |
|
1000 apply clarify |
|
1001 apply(erule_tac x=i in allE, erule impE, assumption, |
|
1002 erule_tac x=j and P="\<lambda>j. ?H j \<longrightarrow> (snd (?d j))=(snd (?e j))" in allE) |
|
1003 apply(case_tac j,simp) |
|
1004 apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE) |
|
1005 apply(case_tac "clist!i",simp,simp) |
|
1006 apply(rule conjI) |
|
1007 apply(simp add:same_program_def) |
|
1008 apply clarify |
|
1009 apply(rule nth_equalityI,simp,simp) |
|
1010 apply(case_tac j,simp) |
|
1011 apply clarify |
|
1012 apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE) |
|
1013 apply(case_tac "clist!i",simp,simp) |
|
1014 apply clarify |
|
1015 apply(simp add:compat_label_def) |
|
1016 apply(rule allI,rule impI) |
|
1017 apply(erule_tac x=j in allE,erule impE, assumption) |
|
1018 apply(erule disjE) |
|
1019 apply clarify |
|
1020 apply(rule_tac x=i in exI,simp) |
|
1021 apply(rule conjI) |
|
1022 apply(erule_tac x=i in allE) |
|
1023 apply(case_tac j,simp) |
|
1024 apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE) |
|
1025 apply(case_tac "clist!i",simp,simp) |
|
1026 apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE) |
|
1027 apply(case_tac "clist!i",simp,simp) |
|
1028 apply clarify |
|
1029 apply(erule_tac x=l and P="\<lambda>j. ?H j \<longrightarrow> ?I j \<longrightarrow> ?J j" in allE) |
|
1030 apply(erule_tac x=l and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE) |
|
1031 apply(case_tac "clist!l",simp,simp) |
|
1032 apply(erule_tac x=l in allE,simp) |
|
1033 apply(rule disjI2) |
|
1034 apply clarify |
|
1035 apply(rule tl_zero) |
|
1036 apply(case_tac j,simp,simp) |
|
1037 apply(rule tl_zero,force) |
|
1038 apply force |
|
1039 apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE,force) |
|
1040 apply force |
|
1041 apply(erule_tac x=i and P="\<lambda>j. ?H j \<longrightarrow> (length (?s j) = ?t)" in allE,force) |
|
1042 apply clarify |
|
1043 apply(erule_tac x=i in allE) |
|
1044 apply(simp add:cp_def) |
|
1045 apply(rule nth_tl_if) |
|
1046 apply(simp add:conjoin_def) |
|
1047 apply clarify |
|
1048 apply(simp add:same_length_def) |
|
1049 apply(erule_tac x=i in allE,simp) |
|
1050 apply simp |
|
1051 apply simp |
|
1052 apply simp |
|
1053 apply clarify |
|
1054 apply(erule_tac c="(xs, s) # ys" in equalityCE) |
|
1055 apply(simp add:par_cp_def) |
|
1056 apply simp |
|
1057 apply(erule_tac x="map (\<lambda>i. (fst i, s) # snd i) (zip xs clist)" in allE) |
|
1058 apply simp |
|
1059 apply clarify |
|
1060 apply(simp add:cp_def) |
|
1061 done |
|
1062 |
|
1063 theorem one: "xs\<noteq>[] \<Longrightarrow> |
|
1064 par_cp xs s = {c. \<exists>clist. (length clist)=(length xs) \<and> |
|
1065 (\<forall>i<length clist. (clist!i) \<in> cp(xs!i) s) \<and> c \<propto> clist}" |
|
1066 apply(frule one_iff_aux) |
|
1067 apply(drule sym) |
|
1068 apply(erule iffD2) |
|
1069 apply clarify |
|
1070 apply(rule iffI) |
|
1071 apply(erule aux_onlyif) |
|
1072 apply clarify |
|
1073 apply(force intro:aux_if) |
|
1074 done |
|
1075 |
|
1076 end |