3071
|
1 |
(* Title: HOLCF/IOA/meta_theory/CompoExecs.thy
|
3275
|
2 |
ID: $Id$
|
12218
|
3 |
Author: Olaf Müller
|
17233
|
4 |
*)
|
3071
|
5 |
|
17233
|
6 |
header {* Compositionality on Execution level *}
|
3071
|
7 |
|
17233
|
8 |
theory CompoExecs
|
|
9 |
imports Traces
|
|
10 |
begin
|
3071
|
11 |
|
17233
|
12 |
consts
|
3071
|
13 |
|
|
14 |
ProjA ::"('a,'s * 't)execution => ('a,'s)execution"
|
|
15 |
ProjA2 ::"('a,'s * 't)pairs -> ('a,'s)pairs"
|
|
16 |
ProjB ::"('a,'s * 't)execution => ('a,'t)execution"
|
|
17 |
ProjB2 ::"('a,'s * 't)pairs -> ('a,'t)pairs"
|
3521
|
18 |
Filter_ex ::"'a signature => ('a,'s)execution => ('a,'s)execution"
|
17233
|
19 |
Filter_ex2 ::"'a signature => ('a,'s)pairs -> ('a,'s)pairs"
|
|
20 |
stutter ::"'a signature => ('a,'s)execution => bool"
|
3521
|
21 |
stutter2 ::"'a signature => ('a,'s)pairs -> ('s => tr)"
|
|
22 |
|
|
23 |
par_execs ::"[('a,'s)execution_module,('a,'t)execution_module] => ('a,'s*'t)execution_module"
|
3071
|
24 |
|
|
25 |
|
17233
|
26 |
defs
|
3071
|
27 |
|
|
28 |
|
17233
|
29 |
ProjA_def:
|
|
30 |
"ProjA ex == (fst (fst ex), ProjA2$(snd ex))"
|
3071
|
31 |
|
17233
|
32 |
ProjB_def:
|
|
33 |
"ProjB ex == (snd (fst ex), ProjB2$(snd ex))"
|
3071
|
34 |
|
|
35 |
|
17233
|
36 |
ProjA2_def:
|
3071
|
37 |
"ProjA2 == Map (%x.(fst x,fst(snd x)))"
|
|
38 |
|
17233
|
39 |
ProjB2_def:
|
3071
|
40 |
"ProjB2 == Map (%x.(fst x,snd(snd x)))"
|
17233
|
41 |
|
3071
|
42 |
|
17233
|
43 |
Filter_ex_def:
|
10835
|
44 |
"Filter_ex sig ex == (fst ex,Filter_ex2 sig$(snd ex))"
|
3071
|
45 |
|
|
46 |
|
17233
|
47 |
Filter_ex2_def:
|
3842
|
48 |
"Filter_ex2 sig == Filter (%x. fst x:actions sig)"
|
3071
|
49 |
|
17233
|
50 |
stutter_def:
|
10835
|
51 |
"stutter sig ex == ((stutter2 sig$(snd ex)) (fst ex) ~= FF)"
|
3071
|
52 |
|
17233
|
53 |
stutter2_def:
|
|
54 |
"stutter2 sig ==(fix$(LAM h ex. (%s. case ex of
|
3071
|
55 |
nil => TT
|
17233
|
56 |
| x##xs => (flift1
|
3521
|
57 |
(%p.(If Def ((fst p)~:actions sig)
|
17233
|
58 |
then Def (s=(snd p))
|
3071
|
59 |
else TT fi)
|
17233
|
60 |
andalso (h$xs) (snd p))
|
10835
|
61 |
$x)
|
17233
|
62 |
)))"
|
3071
|
63 |
|
17233
|
64 |
par_execs_def:
|
|
65 |
"par_execs ExecsA ExecsB ==
|
|
66 |
let exA = fst ExecsA; sigA = snd ExecsA;
|
|
67 |
exB = fst ExecsB; sigB = snd ExecsB
|
3521
|
68 |
in
|
|
69 |
( {ex. Filter_ex sigA (ProjA ex) : exA}
|
|
70 |
Int {ex. Filter_ex sigB (ProjB ex) : exB}
|
|
71 |
Int {ex. stutter sigA (ProjA ex)}
|
|
72 |
Int {ex. stutter sigB (ProjB ex)}
|
3842
|
73 |
Int {ex. Forall (%x. fst x:(actions sigA Un actions sigB)) (snd ex)},
|
3521
|
74 |
asig_comp sigA sigB)"
|
3071
|
75 |
|
19741
|
76 |
|
|
77 |
|
|
78 |
lemmas [simp del] = ex_simps all_simps split_paired_All
|
|
79 |
|
|
80 |
|
|
81 |
section "recursive equations of operators"
|
|
82 |
|
|
83 |
|
|
84 |
(* ---------------------------------------------------------------- *)
|
|
85 |
(* ProjA2 *)
|
|
86 |
(* ---------------------------------------------------------------- *)
|
|
87 |
|
|
88 |
|
|
89 |
lemma ProjA2_UU: "ProjA2$UU = UU"
|
|
90 |
apply (simp add: ProjA2_def)
|
|
91 |
done
|
|
92 |
|
|
93 |
lemma ProjA2_nil: "ProjA2$nil = nil"
|
|
94 |
apply (simp add: ProjA2_def)
|
|
95 |
done
|
|
96 |
|
|
97 |
lemma ProjA2_cons: "ProjA2$((a,t)>>xs) = (a,fst t) >> ProjA2$xs"
|
|
98 |
apply (simp add: ProjA2_def)
|
|
99 |
done
|
|
100 |
|
|
101 |
|
|
102 |
(* ---------------------------------------------------------------- *)
|
|
103 |
(* ProjB2 *)
|
|
104 |
(* ---------------------------------------------------------------- *)
|
|
105 |
|
|
106 |
|
|
107 |
lemma ProjB2_UU: "ProjB2$UU = UU"
|
|
108 |
apply (simp add: ProjB2_def)
|
|
109 |
done
|
|
110 |
|
|
111 |
lemma ProjB2_nil: "ProjB2$nil = nil"
|
|
112 |
apply (simp add: ProjB2_def)
|
|
113 |
done
|
|
114 |
|
|
115 |
lemma ProjB2_cons: "ProjB2$((a,t)>>xs) = (a,snd t) >> ProjB2$xs"
|
|
116 |
apply (simp add: ProjB2_def)
|
|
117 |
done
|
|
118 |
|
|
119 |
|
|
120 |
|
|
121 |
(* ---------------------------------------------------------------- *)
|
|
122 |
(* Filter_ex2 *)
|
|
123 |
(* ---------------------------------------------------------------- *)
|
|
124 |
|
|
125 |
|
|
126 |
lemma Filter_ex2_UU: "Filter_ex2 sig$UU=UU"
|
|
127 |
apply (simp add: Filter_ex2_def)
|
|
128 |
done
|
|
129 |
|
|
130 |
lemma Filter_ex2_nil: "Filter_ex2 sig$nil=nil"
|
|
131 |
apply (simp add: Filter_ex2_def)
|
|
132 |
done
|
|
133 |
|
|
134 |
lemma Filter_ex2_cons: "Filter_ex2 sig$(at >> xs) =
|
|
135 |
(if (fst at:actions sig)
|
|
136 |
then at >> (Filter_ex2 sig$xs)
|
|
137 |
else Filter_ex2 sig$xs)"
|
|
138 |
|
|
139 |
apply (simp add: Filter_ex2_def)
|
|
140 |
done
|
|
141 |
|
|
142 |
|
|
143 |
(* ---------------------------------------------------------------- *)
|
|
144 |
(* stutter2 *)
|
|
145 |
(* ---------------------------------------------------------------- *)
|
|
146 |
|
|
147 |
|
|
148 |
lemma stutter2_unfold: "stutter2 sig = (LAM ex. (%s. case ex of
|
|
149 |
nil => TT
|
|
150 |
| x##xs => (flift1
|
|
151 |
(%p.(If Def ((fst p)~:actions sig)
|
|
152 |
then Def (s=(snd p))
|
|
153 |
else TT fi)
|
|
154 |
andalso (stutter2 sig$xs) (snd p))
|
|
155 |
$x)
|
|
156 |
))"
|
|
157 |
apply (rule trans)
|
|
158 |
apply (rule fix_eq2)
|
|
159 |
apply (rule stutter2_def)
|
|
160 |
apply (rule beta_cfun)
|
|
161 |
apply (simp add: flift1_def)
|
|
162 |
done
|
|
163 |
|
|
164 |
lemma stutter2_UU: "(stutter2 sig$UU) s=UU"
|
|
165 |
apply (subst stutter2_unfold)
|
|
166 |
apply simp
|
|
167 |
done
|
|
168 |
|
|
169 |
lemma stutter2_nil: "(stutter2 sig$nil) s = TT"
|
|
170 |
apply (subst stutter2_unfold)
|
|
171 |
apply simp
|
|
172 |
done
|
|
173 |
|
|
174 |
lemma stutter2_cons: "(stutter2 sig$(at>>xs)) s =
|
|
175 |
((if (fst at)~:actions sig then Def (s=snd at) else TT)
|
|
176 |
andalso (stutter2 sig$xs) (snd at))"
|
|
177 |
apply (rule trans)
|
|
178 |
apply (subst stutter2_unfold)
|
|
179 |
apply (simp add: Consq_def flift1_def If_and_if)
|
|
180 |
apply simp
|
|
181 |
done
|
|
182 |
|
|
183 |
|
|
184 |
declare stutter2_UU [simp] stutter2_nil [simp] stutter2_cons [simp]
|
|
185 |
|
|
186 |
|
|
187 |
(* ---------------------------------------------------------------- *)
|
|
188 |
(* stutter *)
|
|
189 |
(* ---------------------------------------------------------------- *)
|
|
190 |
|
|
191 |
lemma stutter_UU: "stutter sig (s, UU)"
|
|
192 |
apply (simp add: stutter_def)
|
|
193 |
done
|
|
194 |
|
|
195 |
lemma stutter_nil: "stutter sig (s, nil)"
|
|
196 |
apply (simp add: stutter_def)
|
|
197 |
done
|
|
198 |
|
|
199 |
lemma stutter_cons: "stutter sig (s, (a,t)>>ex) =
|
|
200 |
((a~:actions sig --> (s=t)) & stutter sig (t,ex))"
|
|
201 |
apply (simp add: stutter_def)
|
|
202 |
done
|
|
203 |
|
|
204 |
(* ----------------------------------------------------------------------------------- *)
|
|
205 |
|
|
206 |
declare stutter2_UU [simp del] stutter2_nil [simp del] stutter2_cons [simp del]
|
|
207 |
|
|
208 |
lemmas compoex_simps = ProjA2_UU ProjA2_nil ProjA2_cons
|
|
209 |
ProjB2_UU ProjB2_nil ProjB2_cons
|
|
210 |
Filter_ex2_UU Filter_ex2_nil Filter_ex2_cons
|
|
211 |
stutter_UU stutter_nil stutter_cons
|
|
212 |
|
|
213 |
declare compoex_simps [simp]
|
|
214 |
|
|
215 |
|
|
216 |
|
|
217 |
(* ------------------------------------------------------------------ *)
|
|
218 |
(* The following lemmata aim for *)
|
|
219 |
(* COMPOSITIONALITY on EXECUTION Level *)
|
|
220 |
(* ------------------------------------------------------------------ *)
|
|
221 |
|
|
222 |
|
|
223 |
(* --------------------------------------------------------------------- *)
|
|
224 |
(* Lemma_1_1a : is_ex_fr propagates from A||B to Projections A and B *)
|
|
225 |
(* --------------------------------------------------------------------- *)
|
|
226 |
|
|
227 |
lemma lemma_1_1a: "!s. is_exec_frag (A||B) (s,xs)
|
|
228 |
--> is_exec_frag A (fst s, Filter_ex2 (asig_of A)$(ProjA2$xs)) &
|
|
229 |
is_exec_frag B (snd s, Filter_ex2 (asig_of B)$(ProjB2$xs))"
|
|
230 |
|
|
231 |
apply (tactic {* pair_induct_tac "xs" [thm "is_exec_frag_def"] 1 *})
|
|
232 |
(* main case *)
|
|
233 |
apply (rename_tac ss a t)
|
|
234 |
apply (tactic "safe_tac set_cs")
|
|
235 |
apply (simp_all add: trans_of_defs2)
|
|
236 |
done
|
|
237 |
|
|
238 |
|
|
239 |
(* --------------------------------------------------------------------- *)
|
|
240 |
(* Lemma_1_1b : is_ex_fr (A||B) implies stuttering on Projections *)
|
|
241 |
(* --------------------------------------------------------------------- *)
|
|
242 |
|
|
243 |
lemma lemma_1_1b: "!s. is_exec_frag (A||B) (s,xs)
|
|
244 |
--> stutter (asig_of A) (fst s,ProjA2$xs) &
|
|
245 |
stutter (asig_of B) (snd s,ProjB2$xs)"
|
|
246 |
|
|
247 |
apply (tactic {* pair_induct_tac "xs" [thm "stutter_def", thm "is_exec_frag_def"] 1 *})
|
|
248 |
(* main case *)
|
|
249 |
apply (tactic "safe_tac set_cs")
|
|
250 |
apply (simp_all add: trans_of_defs2)
|
|
251 |
done
|
|
252 |
|
|
253 |
|
|
254 |
(* --------------------------------------------------------------------- *)
|
|
255 |
(* Lemma_1_1c : Executions of A||B have only A- or B-actions *)
|
|
256 |
(* --------------------------------------------------------------------- *)
|
|
257 |
|
|
258 |
lemma lemma_1_1c: "!s. (is_exec_frag (A||B) (s,xs)
|
|
259 |
--> Forall (%x. fst x:act (A||B)) xs)"
|
|
260 |
|
|
261 |
apply (tactic {* pair_induct_tac "xs" [thm "Forall_def", thm "sforall_def",
|
|
262 |
thm "is_exec_frag_def"] 1 *})
|
|
263 |
(* main case *)
|
|
264 |
apply (tactic "safe_tac set_cs")
|
|
265 |
apply (simp_all add: trans_of_defs2 actions_asig_comp asig_of_par)
|
|
266 |
done
|
|
267 |
|
|
268 |
|
|
269 |
(* ----------------------------------------------------------------------- *)
|
|
270 |
(* Lemma_1_2 : ex A, exB, stuttering and forall a:A|B implies ex (A||B) *)
|
|
271 |
(* ----------------------------------------------------------------------- *)
|
|
272 |
|
|
273 |
lemma lemma_1_2:
|
|
274 |
"!s. is_exec_frag A (fst s,Filter_ex2 (asig_of A)$(ProjA2$xs)) &
|
|
275 |
is_exec_frag B (snd s,Filter_ex2 (asig_of B)$(ProjB2$xs)) &
|
|
276 |
stutter (asig_of A) (fst s,(ProjA2$xs)) &
|
|
277 |
stutter (asig_of B) (snd s,(ProjB2$xs)) &
|
|
278 |
Forall (%x. fst x:act (A||B)) xs
|
|
279 |
--> is_exec_frag (A||B) (s,xs)"
|
|
280 |
|
|
281 |
apply (tactic {* pair_induct_tac "xs" [thm "Forall_def", thm "sforall_def",
|
|
282 |
thm "is_exec_frag_def", thm "stutter_def"] 1 *})
|
|
283 |
apply (simp add: trans_of_defs1 actions_asig_comp asig_of_par)
|
|
284 |
apply (tactic "safe_tac set_cs")
|
|
285 |
apply simp
|
|
286 |
apply simp
|
|
287 |
done
|
|
288 |
|
|
289 |
|
|
290 |
subsection {* COMPOSITIONALITY on EXECUTION Level -- Main Theorem *}
|
|
291 |
|
|
292 |
lemma compositionality_ex:
|
|
293 |
"(ex:executions(A||B)) =
|
|
294 |
(Filter_ex (asig_of A) (ProjA ex) : executions A &
|
|
295 |
Filter_ex (asig_of B) (ProjB ex) : executions B &
|
|
296 |
stutter (asig_of A) (ProjA ex) & stutter (asig_of B) (ProjB ex) &
|
|
297 |
Forall (%x. fst x:act (A||B)) (snd ex))"
|
|
298 |
|
|
299 |
apply (simp (no_asm) add: executions_def ProjB_def Filter_ex_def ProjA_def starts_of_par)
|
|
300 |
apply (tactic {* pair_tac "ex" 1 *})
|
|
301 |
apply (rule iffI)
|
|
302 |
(* ==> *)
|
|
303 |
apply (erule conjE)+
|
|
304 |
apply (simp add: lemma_1_1a lemma_1_1b lemma_1_1c)
|
|
305 |
(* <== *)
|
|
306 |
apply (erule conjE)+
|
|
307 |
apply (simp add: lemma_1_2)
|
|
308 |
done
|
|
309 |
|
|
310 |
|
|
311 |
subsection {* COMPOSITIONALITY on EXECUTION Level -- for Modules *}
|
|
312 |
|
|
313 |
lemma compositionality_ex_modules:
|
|
314 |
"Execs (A||B) = par_execs (Execs A) (Execs B)"
|
|
315 |
apply (unfold Execs_def par_execs_def)
|
|
316 |
apply (simp add: asig_of_par)
|
|
317 |
apply (rule set_ext)
|
|
318 |
apply (simp add: compositionality_ex actions_of_par)
|
|
319 |
done
|
17233
|
320 |
|
|
321 |
end
|