author | huffman |
Thu, 18 Feb 2010 13:29:59 -0800 | |
changeset 35215 | a03462cbf86f |
parent 35174 | e15040ae75d7 |
child 39302 | d7728f65b353 |
permissions | -rw-r--r-- |
3071 | 1 |
(* Title: HOLCF/IOA/meta_theory/CompoExecs.thy |
12218 | 2 |
Author: Olaf Müller |
17233 | 3 |
*) |
3071 | 4 |
|
17233 | 5 |
header {* Compositionality on Execution level *} |
3071 | 6 |
|
17233 | 7 |
theory CompoExecs |
8 |
imports Traces |
|
9 |
begin |
|
3071 | 10 |
|
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
11 |
definition |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
12 |
ProjA2 :: "('a,'s * 't)pairs -> ('a,'s)pairs" where |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
13 |
"ProjA2 = Map (%x.(fst x,fst(snd x)))" |
3071 | 14 |
|
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
15 |
definition |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
16 |
ProjA :: "('a,'s * 't)execution => ('a,'s)execution" where |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
17 |
"ProjA ex = (fst (fst ex), ProjA2$(snd ex))" |
3521 | 18 |
|
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
19 |
definition |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
20 |
ProjB2 :: "('a,'s * 't)pairs -> ('a,'t)pairs" where |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
21 |
"ProjB2 = Map (%x.(fst x,snd(snd x)))" |
3071 | 22 |
|
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
23 |
definition |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
24 |
ProjB :: "('a,'s * 't)execution => ('a,'t)execution" where |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
25 |
"ProjB ex = (snd (fst ex), ProjB2$(snd ex))" |
3071 | 26 |
|
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
27 |
definition |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
28 |
Filter_ex2 :: "'a signature => ('a,'s)pairs -> ('a,'s)pairs" where |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
29 |
"Filter_ex2 sig = Filter (%x. fst x:actions sig)" |
3071 | 30 |
|
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
31 |
definition |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
32 |
Filter_ex :: "'a signature => ('a,'s)execution => ('a,'s)execution" where |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
33 |
"Filter_ex sig ex = (fst ex,Filter_ex2 sig$(snd ex))" |
3071 | 34 |
|
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
35 |
definition |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
36 |
stutter2 :: "'a signature => ('a,'s)pairs -> ('s => tr)" where |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
37 |
"stutter2 sig = (fix$(LAM h ex. (%s. case ex of |
3071 | 38 |
nil => TT |
17233 | 39 |
| x##xs => (flift1 |
3521 | 40 |
(%p.(If Def ((fst p)~:actions sig) |
17233 | 41 |
then Def (s=(snd p)) |
3071 | 42 |
else TT fi) |
17233 | 43 |
andalso (h$xs) (snd p)) |
10835 | 44 |
$x) |
17233 | 45 |
)))" |
3071 | 46 |
|
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
47 |
definition |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
48 |
stutter :: "'a signature => ('a,'s)execution => bool" where |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
49 |
"stutter sig ex = ((stutter2 sig$(snd ex)) (fst ex) ~= FF)" |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
50 |
|
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
51 |
definition |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
52 |
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
|
53 |
"par_execs ExecsA ExecsB = |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
54 |
(let exA = fst ExecsA; sigA = snd ExecsA; |
17233 | 55 |
exB = fst ExecsB; sigB = snd ExecsB |
3521 | 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)} |
|
3842 | 61 |
Int {ex. Forall (%x. fst x:(actions sigA Un actions sigB)) (snd ex)}, |
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
62 |
asig_comp sigA sigB))" |
19741 | 63 |
|
64 |
||
35215
a03462cbf86f
get rid of warnings about duplicate simp rules in all HOLCF theories
huffman
parents:
35174
diff
changeset
|
65 |
lemmas [simp del] = split_paired_All |
19741 | 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 |
||
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
121 |
lemma Filter_ex2_cons: "Filter_ex2 sig$(at >> xs) = |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
122 |
(if (fst at:actions sig) |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
123 |
then at >> (Filter_ex2 sig$xs) |
19741 | 124 |
else Filter_ex2 sig$xs)" |
125 |
||
126 |
apply (simp add: Filter_ex2_def) |
|
127 |
done |
|
128 |
||
129 |
||
130 |
(* ---------------------------------------------------------------- *) |
|
131 |
(* stutter2 *) |
|
132 |
(* ---------------------------------------------------------------- *) |
|
133 |
||
134 |
||
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
135 |
lemma stutter2_unfold: "stutter2 sig = (LAM ex. (%s. case ex of |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
136 |
nil => TT |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
137 |
| x##xs => (flift1 |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
138 |
(%p.(If Def ((fst p)~:actions sig) |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
139 |
then Def (s=(snd p)) |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
140 |
else TT fi) |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
141 |
andalso (stutter2 sig$xs) (snd p)) |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
142 |
$x) |
19741 | 143 |
))" |
144 |
apply (rule trans) |
|
145 |
apply (rule fix_eq2) |
|
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
146 |
apply (simp only: stutter2_def) |
19741 | 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 |
||
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
161 |
lemma stutter2_cons: "(stutter2 sig$(at>>xs)) s = |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
162 |
((if (fst at)~:actions sig then Def (s=snd at) else TT) |
19741 | 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 |
||
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
186 |
lemma stutter_cons: "stutter sig (s, (a,t)>>ex) = |
19741 | 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 |
||
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
214 |
lemma lemma_1_1a: "!s. is_exec_frag (A||B) (s,xs) |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
215 |
--> is_exec_frag A (fst s, Filter_ex2 (asig_of A)$(ProjA2$xs)) & |
19741 | 216 |
is_exec_frag B (snd s, Filter_ex2 (asig_of B)$(ProjB2$xs))" |
217 |
||
27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
26359
diff
changeset
|
218 |
apply (tactic {* pair_induct_tac @{context} "xs" [@{thm is_exec_frag_def}] 1 *}) |
19741 | 219 |
(* main case *) |
26359 | 220 |
apply (auto simp add: trans_of_defs2) |
19741 | 221 |
done |
222 |
||
223 |
||
224 |
(* --------------------------------------------------------------------- *) |
|
225 |
(* Lemma_1_1b : is_ex_fr (A||B) implies stuttering on Projections *) |
|
226 |
(* --------------------------------------------------------------------- *) |
|
227 |
||
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
228 |
lemma lemma_1_1b: "!s. is_exec_frag (A||B) (s,xs) |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
229 |
--> stutter (asig_of A) (fst s,ProjA2$xs) & |
19741 | 230 |
stutter (asig_of B) (snd s,ProjB2$xs)" |
231 |
||
27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
26359
diff
changeset
|
232 |
apply (tactic {* pair_induct_tac @{context} "xs" |
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
26359
diff
changeset
|
233 |
[@{thm stutter_def}, @{thm is_exec_frag_def}] 1 *}) |
19741 | 234 |
(* main case *) |
26359 | 235 |
apply (auto simp add: trans_of_defs2) |
19741 | 236 |
done |
237 |
||
238 |
||
239 |
(* --------------------------------------------------------------------- *) |
|
240 |
(* Lemma_1_1c : Executions of A||B have only A- or B-actions *) |
|
241 |
(* --------------------------------------------------------------------- *) |
|
242 |
||
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
243 |
lemma lemma_1_1c: "!s. (is_exec_frag (A||B) (s,xs) |
19741 | 244 |
--> Forall (%x. fst x:act (A||B)) xs)" |
245 |
||
27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
26359
diff
changeset
|
246 |
apply (tactic {* pair_induct_tac @{context} "xs" [@{thm Forall_def}, @{thm sforall_def}, |
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
26359
diff
changeset
|
247 |
@{thm is_exec_frag_def}] 1 *}) |
19741 | 248 |
(* main case *) |
26359 | 249 |
apply auto |
250 |
apply (simp add: trans_of_defs2 actions_asig_comp asig_of_par) |
|
19741 | 251 |
done |
252 |
||
253 |
||
254 |
(* ----------------------------------------------------------------------- *) |
|
255 |
(* Lemma_1_2 : ex A, exB, stuttering and forall a:A|B implies ex (A||B) *) |
|
256 |
(* ----------------------------------------------------------------------- *) |
|
257 |
||
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
258 |
lemma lemma_1_2: |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
259 |
"!s. is_exec_frag A (fst s,Filter_ex2 (asig_of A)$(ProjA2$xs)) & |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
260 |
is_exec_frag B (snd s,Filter_ex2 (asig_of B)$(ProjB2$xs)) & |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
261 |
stutter (asig_of A) (fst s,(ProjA2$xs)) & |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
262 |
stutter (asig_of B) (snd s,(ProjB2$xs)) & |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
263 |
Forall (%x. fst x:act (A||B)) xs |
19741 | 264 |
--> is_exec_frag (A||B) (s,xs)" |
265 |
||
27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
26359
diff
changeset
|
266 |
apply (tactic {* pair_induct_tac @{context} "xs" [@{thm Forall_def}, @{thm sforall_def}, |
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
26359
diff
changeset
|
267 |
@{thm is_exec_frag_def}, @{thm stutter_def}] 1 *}) |
26359 | 268 |
apply (auto simp add: trans_of_defs1 actions_asig_comp asig_of_par) |
19741 | 269 |
done |
270 |
||
271 |
||
272 |
subsection {* COMPOSITIONALITY on EXECUTION Level -- Main Theorem *} |
|
273 |
||
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
274 |
lemma compositionality_ex: |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
275 |
"(ex:executions(A||B)) = |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
276 |
(Filter_ex (asig_of A) (ProjA ex) : executions A & |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
277 |
Filter_ex (asig_of B) (ProjB ex) : executions B & |
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
278 |
stutter (asig_of A) (ProjA ex) & stutter (asig_of B) (ProjB ex) & |
19741 | 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) |
|
27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
26359
diff
changeset
|
282 |
apply (tactic {* pair_tac @{context} "ex" 1 *}) |
19741 | 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 |
||
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
295 |
lemma compositionality_ex_modules: |
19741 | 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_ext) |
|
300 |
apply (simp add: compositionality_ex actions_of_par) |
|
301 |
done |
|
17233 | 302 |
|
303 |
end |