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