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