author | wenzelm |
Mon, 11 Jan 2016 00:04:23 +0100 | |
changeset 62116 | bc178c0fe1a1 |
parent 62008 | cbedaddc9351 |
child 62195 | 799a5306e2ed |
permissions | -rw-r--r-- |
62008 | 1 |
(* Title: HOL/HOLCF/IOA/CompoScheds.thy |
40945 | 2 |
Author: Olaf Müller |
17233 | 3 |
*) |
3071 | 4 |
|
62002 | 5 |
section \<open>Compositionality on Schedule level\<close> |
3071 | 6 |
|
17233 | 7 |
theory CompoScheds |
8 |
imports CompoExecs |
|
9 |
begin |
|
3071 | 10 |
|
62116 | 11 |
definition mkex2 :: "('a, 's) ioa \<Rightarrow> ('a, 't) ioa \<Rightarrow> 'a Seq \<rightarrow> |
12 |
('a, 's) pairs \<rightarrow> ('a, 't) pairs \<rightarrow> ('s \<Rightarrow> 't \<Rightarrow> ('a, 's \<times> 't) pairs)" |
|
13 |
where "mkex2 A B = |
|
14 |
(fix $ |
|
15 |
(LAM h sch exA exB. |
|
16 |
(\<lambda>s t. |
|
17 |
case sch of |
|
18 |
nil \<Rightarrow> nil |
|
19 |
| x ## xs \<Rightarrow> |
|
20 |
(case x of |
|
21 |
UU \<Rightarrow> UU |
|
22 |
| Def y \<Rightarrow> |
|
23 |
(if y \<in> act A then |
|
24 |
(if y \<in> act B then |
|
25 |
(case HD $ exA of |
|
26 |
UU \<Rightarrow> UU |
|
27 |
| Def a \<Rightarrow> |
|
28 |
(case HD $ exB of |
|
29 |
UU \<Rightarrow> UU |
|
30 |
| Def b \<Rightarrow> |
|
31 |
(y, (snd a, snd b)) \<leadsto> |
|
32 |
(h $ xs $ (TL $ exA) $ (TL $ exB)) (snd a) (snd b))) |
|
33 |
else |
|
34 |
(case HD $ exA of |
|
35 |
UU \<Rightarrow> UU |
|
36 |
| Def a \<Rightarrow> (y, (snd a, t)) \<leadsto> (h $ xs $ (TL $ exA) $ exB) (snd a) t)) |
|
37 |
else |
|
38 |
(if y \<in> act B then |
|
39 |
(case HD $ exB of |
|
40 |
UU \<Rightarrow> UU |
|
41 |
| Def b \<Rightarrow> (y, (s, snd b)) \<leadsto> (h $ xs $ exA $ (TL $ exB)) s (snd b)) |
|
42 |
else UU))))))" |
|
3071 | 43 |
|
62116 | 44 |
definition mkex :: "('a, 's) ioa \<Rightarrow> ('a, 't) ioa \<Rightarrow> 'a Seq \<Rightarrow> |
45 |
('a, 's) execution \<Rightarrow> ('a, 't) execution \<Rightarrow> ('a, 's \<times> 't) execution" |
|
46 |
where "mkex A B sch exA exB = |
|
47 |
((fst exA, fst exB), (mkex2 A B $ sch $ (snd exA) $ (snd exB)) (fst exA) (fst exB))" |
|
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
48 |
|
62116 | 49 |
definition par_scheds :: "'a schedule_module \<Rightarrow> 'a schedule_module \<Rightarrow> 'a schedule_module" |
50 |
where "par_scheds SchedsA SchedsB = |
|
51 |
(let |
|
52 |
schA = fst SchedsA; sigA = snd SchedsA; |
|
53 |
schB = fst SchedsB; sigB = snd SchedsB |
|
54 |
in |
|
55 |
({sch. Filter (%a. a:actions sigA)$sch : schA} \<inter> |
|
56 |
{sch. Filter (%a. a:actions sigB)$sch : schB} \<inter> |
|
57 |
{sch. Forall (%x. x:(actions sigA Un actions sigB)) sch}, |
|
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
58 |
asig_comp sigA sigB))" |
3521 | 59 |
|
19741 | 60 |
|
62116 | 61 |
subsection \<open>\<open>mkex\<close> rewrite rules\<close> |
19741 | 62 |
|
63 |
lemma mkex2_unfold: |
|
62116 | 64 |
"mkex2 A B = |
65 |
(LAM sch exA exB. |
|
66 |
(\<lambda>s t. |
|
67 |
case sch of |
|
68 |
nil \<Rightarrow> nil |
|
69 |
| x ## xs \<Rightarrow> |
|
70 |
(case x of |
|
71 |
UU \<Rightarrow> UU |
|
72 |
| Def y \<Rightarrow> |
|
73 |
(if y \<in> act A then |
|
74 |
(if y \<in> act B then |
|
75 |
(case HD $ exA of |
|
76 |
UU \<Rightarrow> UU |
|
77 |
| Def a \<Rightarrow> |
|
78 |
(case HD $ exB of |
|
79 |
UU \<Rightarrow> UU |
|
80 |
| Def b \<Rightarrow> |
|
81 |
(y, (snd a, snd b)) \<leadsto> |
|
82 |
(mkex2 A B $ xs $ (TL $ exA) $ (TL $ exB)) (snd a) (snd b))) |
|
83 |
else |
|
84 |
(case HD $ exA of |
|
85 |
UU \<Rightarrow> UU |
|
86 |
| Def a \<Rightarrow> (y, (snd a, t)) \<leadsto> (mkex2 A B $ xs $ (TL $ exA) $ exB) (snd a) t)) |
|
87 |
else |
|
88 |
(if y \<in> act B then |
|
89 |
(case HD $ exB of |
|
90 |
UU \<Rightarrow> UU |
|
91 |
| Def b \<Rightarrow> (y, (s, snd b)) \<leadsto> (mkex2 A B $ xs $ exA $ (TL $ exB)) s (snd b)) |
|
92 |
else UU)))))" |
|
93 |
apply (rule trans) |
|
94 |
apply (rule fix_eq2) |
|
95 |
apply (simp only: mkex2_def) |
|
96 |
apply (rule beta_cfun) |
|
97 |
apply simp |
|
98 |
done |
|
19741 | 99 |
|
62116 | 100 |
lemma mkex2_UU: "(mkex2 A B $ UU $ exA $ exB) s t = UU" |
101 |
apply (subst mkex2_unfold) |
|
102 |
apply simp |
|
103 |
done |
|
104 |
||
105 |
lemma mkex2_nil: "(mkex2 A B $ nil $ exA $ exB) s t = nil" |
|
106 |
apply (subst mkex2_unfold) |
|
107 |
apply simp |
|
108 |
done |
|
19741 | 109 |
|
62116 | 110 |
lemma mkex2_cons_1: |
111 |
"x \<in> act A \<Longrightarrow> x \<notin> act B \<Longrightarrow> HD $ exA = Def a \<Longrightarrow> |
|
112 |
(mkex2 A B $ (x \<leadsto> sch) $ exA $ exB) s t = |
|
113 |
(x, snd a,t) \<leadsto> (mkex2 A B $ sch $ (TL $ exA) $ exB) (snd a) t" |
|
114 |
apply (rule trans) |
|
115 |
apply (subst mkex2_unfold) |
|
116 |
apply (simp add: Consq_def If_and_if) |
|
117 |
apply (simp add: Consq_def) |
|
118 |
done |
|
19741 | 119 |
|
62116 | 120 |
lemma mkex2_cons_2: |
121 |
"x \<notin> act A \<Longrightarrow> x \<in> act B \<Longrightarrow> HD $ exB = Def b \<Longrightarrow> |
|
122 |
(mkex2 A B $ (x \<leadsto> sch) $ exA $ exB) s t = |
|
123 |
(x, s, snd b) \<leadsto> (mkex2 A B $ sch $ exA $ (TL $ exB)) s (snd b)" |
|
124 |
apply (rule trans) |
|
125 |
apply (subst mkex2_unfold) |
|
126 |
apply (simp add: Consq_def If_and_if) |
|
127 |
apply (simp add: Consq_def) |
|
128 |
done |
|
19741 | 129 |
|
62116 | 130 |
lemma mkex2_cons_3: |
131 |
"x \<in> act A \<Longrightarrow> x \<in> act B \<Longrightarrow> HD $ exA = Def a \<Longrightarrow> HD $ exB = Def b \<Longrightarrow> |
|
132 |
(mkex2 A B $ (x \<leadsto> sch) $ exA $ exB) s t = |
|
133 |
(x, snd a,snd b) \<leadsto> (mkex2 A B $ sch $ (TL $ exA) $ (TL $ exB)) (snd a) (snd b)" |
|
134 |
apply (rule trans) |
|
135 |
apply (subst mkex2_unfold) |
|
136 |
apply (simp add: Consq_def If_and_if) |
|
137 |
apply (simp add: Consq_def) |
|
138 |
done |
|
19741 | 139 |
|
140 |
declare mkex2_UU [simp] mkex2_nil [simp] mkex2_cons_1 [simp] |
|
141 |
mkex2_cons_2 [simp] mkex2_cons_3 [simp] |
|
142 |
||
143 |
||
62116 | 144 |
subsection \<open>\<open>mkex\<close>\<close> |
19741 | 145 |
|
146 |
lemma mkex_UU: "mkex A B UU (s,exA) (t,exB) = ((s,t),UU)" |
|
62116 | 147 |
by (simp add: mkex_def) |
19741 | 148 |
|
149 |
lemma mkex_nil: "mkex A B nil (s,exA) (t,exB) = ((s,t),nil)" |
|
62116 | 150 |
by (simp add: mkex_def) |
19741 | 151 |
|
62116 | 152 |
lemma mkex_cons_1: |
153 |
"x \<in> act A \<Longrightarrow> x \<notin> act B \<Longrightarrow> |
|
154 |
mkex A B (x \<leadsto> sch) (s, a \<leadsto> exA) (t, exB) = |
|
155 |
((s, t), (x, snd a, t) \<leadsto> snd (mkex A B sch (snd a, exA) (t, exB)))" |
|
156 |
apply (unfold mkex_def) |
|
157 |
apply (cut_tac exA = "a \<leadsto> exA" in mkex2_cons_1) |
|
158 |
apply auto |
|
159 |
done |
|
19741 | 160 |
|
62116 | 161 |
lemma mkex_cons_2: |
162 |
"x \<notin> act A \<Longrightarrow> x \<in> act B \<Longrightarrow> |
|
163 |
mkex A B (x \<leadsto> sch) (s, exA) (t, b \<leadsto> exB) = |
|
164 |
((s, t), (x, s, snd b) \<leadsto> snd (mkex A B sch (s, exA) (snd b, exB)))" |
|
165 |
apply (unfold mkex_def) |
|
166 |
apply (cut_tac exB = "b\<leadsto>exB" in mkex2_cons_2) |
|
167 |
apply auto |
|
168 |
done |
|
19741 | 169 |
|
62116 | 170 |
lemma mkex_cons_3: |
171 |
"x \<in> act A \<Longrightarrow> x \<in> act B \<Longrightarrow> |
|
172 |
mkex A B (x \<leadsto> sch) (s, a \<leadsto> exA) (t, b \<leadsto> exB) = |
|
173 |
((s, t), (x, snd a, snd b) \<leadsto> snd (mkex A B sch (snd a, exA) (snd b, exB)))" |
|
174 |
apply (unfold mkex_def) |
|
175 |
apply (cut_tac exB = "b\<leadsto>exB" and exA = "a\<leadsto>exA" in mkex2_cons_3) |
|
176 |
apply auto |
|
177 |
done |
|
19741 | 178 |
|
179 |
declare mkex2_UU [simp del] mkex2_nil [simp del] |
|
180 |
mkex2_cons_1 [simp del] mkex2_cons_2 [simp del] mkex2_cons_3 [simp del] |
|
181 |
||
182 |
lemmas composch_simps = mkex_UU mkex_nil mkex_cons_1 mkex_cons_2 mkex_cons_3 |
|
183 |
||
184 |
declare composch_simps [simp] |
|
185 |
||
186 |
||
62116 | 187 |
subsection \<open>Compositionality on schedule level\<close> |
19741 | 188 |
|
62116 | 189 |
subsubsection \<open>Lemmas for \<open>\<Longrightarrow>\<close>\<close> |
19741 | 190 |
|
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
191 |
lemma lemma_2_1a: |
62116 | 192 |
\<comment> \<open>\<open>tfilter ex\<close> and \<open>filter_act\<close> are commutative\<close> |
193 |
"filter_act $ (Filter_ex2 (asig_of A) $ xs) = |
|
194 |
Filter (\<lambda>a. a \<in> act A) $ (filter_act $ xs)" |
|
195 |
apply (unfold filter_act_def Filter_ex2_def) |
|
196 |
apply (simp add: MapFilter o_def) |
|
197 |
done |
|
19741 | 198 |
|
25135
4f8176c940cf
modernized specifications ('definition', 'axiomatization');
wenzelm
parents:
19741
diff
changeset
|
199 |
lemma lemma_2_1b: |
62116 | 200 |
\<comment> \<open>State-projections do not affect \<open>filter_act\<close>\<close> |
201 |
"filter_act $ (ProjA2 $ xs) = filter_act $ xs \<and> |
|
202 |
filter_act $ (ProjB2 $ xs) = filter_act $ xs" |
|
203 |
by (tactic \<open>pair_induct_tac @{context} "xs" [] 1\<close>) |
|
19741 | 204 |
|
205 |
||
62116 | 206 |
text \<open> |
207 |
Schedules of \<open>A \<parallel> B\<close> have only \<open>A\<close>- or \<open>B\<close>-actions. |
|
19741 | 208 |
|
62116 | 209 |
Very similar to \<open>lemma_1_1c\<close>, but it is not checking if every action element |
210 |
of an \<open>ex\<close> is in \<open>A\<close> or \<open>B\<close>, but after projecting it onto the action |
|
211 |
schedule. Of course, this is the same proposition, but we cannot change this |
|
212 |
one, when then rather \<open>lemma_1_1c\<close>. |
|
213 |
\<close> |
|
19741 | 214 |
|
62116 | 215 |
lemma sch_actions_in_AorB: |
216 |
"\<forall>s. is_exec_frag (A \<parallel> B) (s, xs) \<longrightarrow> Forall (\<lambda>x. x \<in> act (A \<parallel> B)) (filter_act $ xs)" |
|
217 |
apply (tactic \<open>pair_induct_tac @{context} "xs" |
|
218 |
@{thms is_exec_frag_def Forall_def sforall_def} 1\<close>) |
|
219 |
text \<open>main case\<close> |
|
220 |
apply auto |
|
221 |
apply (simp add: trans_of_defs2 actions_asig_comp asig_of_par) |
|
222 |
done |
|
19741 | 223 |
|
224 |
||
62116 | 225 |
subsubsection \<open>Lemmas for \<open>\<Longleftarrow>\<close>\<close> |
19741 | 226 |
|
62116 | 227 |
text \<open> |
228 |
Filtering actions out of \<open>mkex (sch, exA, exB)\<close> yields the oracle \<open>sch\<close> |
|
229 |
structural induction. |
|
230 |
\<close> |
|
19741 | 231 |
|
62116 | 232 |
lemma Mapfst_mkex_is_sch: |
233 |
"\<forall>exA exB s t. |
|
234 |
Forall (\<lambda>x. x \<in> act (A \<parallel> B)) sch \<and> |
|
235 |
Filter (\<lambda>a. a \<in> act A) $ sch \<sqsubseteq> filter_act $ exA \<and> |
|
236 |
Filter (\<lambda>a. a \<in> act B) $ sch \<sqsubseteq> filter_act $ exB \<longrightarrow> |
|
237 |
filter_act $ (snd (mkex A B sch (s, exA) (t, exB))) = sch" |
|
238 |
apply (tactic \<open>Seq_induct_tac @{context} "sch" [@{thm Filter_def}, @{thm Forall_def}, |
|
239 |
@{thm sforall_def}, @{thm mkex_def}] 1\<close>) |
|
19741 | 240 |
|
62116 | 241 |
text \<open>main case: splitting into 4 cases according to \<open>a \<in> A\<close>, \<open>a \<in> B\<close>\<close> |
242 |
apply auto |
|
19741 | 243 |
|
62116 | 244 |
text \<open>Case \<open>y \<in> A\<close>, \<open>y \<in> B\<close>\<close> |
245 |
apply (tactic \<open>Seq_case_simp_tac @{context} "exA" 1\<close>) |
|
246 |
text \<open>Case \<open>exA = UU\<close>, Case \<open>exA = nil\<close>\<close> |
|
247 |
text \<open> |
|
248 |
These \<open>UU\<close> and \<open>nil\<close> cases are the only places where the assumption |
|
249 |
\<open>filter A sch \<sqsubseteq> f_act exA\<close> is used! |
|
250 |
\<open>\<longrightarrow>\<close> to generate a contradiction using \<open>\<not> a \<leadsto> ss \<sqsubseteq> UU nil\<close>, |
|
251 |
using theorems \<open>Cons_not_less_UU\<close> and \<open>Cons_not_less_nil\<close>.\<close> |
|
252 |
apply (tactic \<open>Seq_case_simp_tac @{context} "exB" 1\<close>) |
|
253 |
text \<open>Case \<open>exA = a \<leadsto> x\<close>, \<open>exB = b \<leadsto> y\<close>\<close> |
|
254 |
text \<open> |
|
255 |
Here it is important that \<open>Seq_case_simp_tac\<close> uses no \<open>!full!_simp_tac\<close> |
|
256 |
for the cons case, as otherwise \<open>mkex_cons_3\<close> would not be rewritten |
|
257 |
without use of \<open>rotate_tac\<close>: then tactic would not be generally |
|
258 |
applicable.\<close> |
|
259 |
apply simp |
|
19741 | 260 |
|
62116 | 261 |
text \<open>Case \<open>y \<in> A\<close>, \<open>y \<notin> B\<close>\<close> |
262 |
apply (tactic \<open>Seq_case_simp_tac @{context} "exA" 1\<close>) |
|
263 |
apply simp |
|
19741 | 264 |
|
62116 | 265 |
text \<open>Case \<open>y \<notin> A\<close>, \<open>y \<in> B\<close>\<close> |
266 |
apply (tactic \<open>Seq_case_simp_tac @{context} "exB" 1\<close>) |
|
267 |
apply simp |
|
19741 | 268 |
|
62116 | 269 |
text \<open>Case \<open>y \<notin> A\<close>, \<open>y \<notin> B\<close>\<close> |
270 |
apply (simp add: asig_of_par actions_asig_comp) |
|
271 |
done |
|
19741 | 272 |
|
273 |
||
62116 | 274 |
text \<open>Generalizing the proof above to a proof method:\<close> |
62002 | 275 |
ML \<open> |
27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
26359
diff
changeset
|
276 |
fun mkex_induct_tac ctxt sch exA exB = |
62116 | 277 |
EVERY' [ |
278 |
Seq_induct_tac ctxt sch |
|
279 |
@{thms Filter_def Forall_def sforall_def mkex_def stutter_def}, |
|
280 |
asm_full_simp_tac ctxt, |
|
281 |
SELECT_GOAL |
|
282 |
(safe_tac (Context.raw_transfer (Proof_Context.theory_of ctxt) @{theory_context Fun})), |
|
283 |
Seq_case_simp_tac ctxt exA, |
|
284 |
Seq_case_simp_tac ctxt exB, |
|
285 |
asm_full_simp_tac ctxt, |
|
286 |
Seq_case_simp_tac ctxt exA, |
|
287 |
asm_full_simp_tac ctxt, |
|
288 |
Seq_case_simp_tac ctxt exB, |
|
289 |
asm_full_simp_tac ctxt, |
|
290 |
asm_full_simp_tac (ctxt addsimps @{thms asig_of_par actions_asig_comp})] |
|
62002 | 291 |
\<close> |
19741 | 292 |
|
62002 | 293 |
method_setup mkex_induct = \<open> |
46469 | 294 |
Scan.lift (Args.name -- Args.name -- Args.name) |
62116 | 295 |
>> (fn ((sch, exA), exB) => fn ctxt => |
296 |
SIMPLE_METHOD' (mkex_induct_tac ctxt sch exA exB)) |
|
62002 | 297 |
\<close> |
46469 | 298 |
|
19741 | 299 |
|
62116 | 300 |
text \<open> |
301 |
Projection of \<open>mkex (sch, exA, exB)\<close> onto \<open>A\<close> stutters on \<open>A\<close> |
|
302 |
structural induction. |
|
303 |
\<close> |
|
19741 | 304 |
|
62116 | 305 |
lemma stutterA_mkex: |
306 |
"\<forall>exA exB s t. |
|
307 |
Forall (\<lambda>x. x \<in> act (A \<parallel> B)) sch \<and> |
|
308 |
Filter (\<lambda>a. a \<in> act A) $ sch \<sqsubseteq> filter_act $ exA \<and> |
|
309 |
Filter (\<lambda>a. a \<in> act B) $ sch \<sqsubseteq> filter_act $ exB \<longrightarrow> |
|
310 |
stutter (asig_of A) (s, ProjA2 $ (snd (mkex A B sch (s, exA) (t, exB))))" |
|
46469 | 311 |
by (mkex_induct sch exA exB) |
19741 | 312 |
|
62116 | 313 |
lemma stutter_mkex_on_A: |
314 |
"Forall (\<lambda>x. x \<in> act (A \<parallel> B)) sch \<Longrightarrow> |
|
315 |
Filter (\<lambda>a. a \<in> act A) $ sch \<sqsubseteq> filter_act $ (snd exA) \<Longrightarrow> |
|
316 |
Filter (\<lambda>a. a \<in> act B) $ sch \<sqsubseteq> filter_act $ (snd exB) \<Longrightarrow> |
|
317 |
stutter (asig_of A) (ProjA (mkex A B sch exA exB))" |
|
318 |
apply (cut_tac stutterA_mkex) |
|
319 |
apply (simp add: stutter_def ProjA_def mkex_def) |
|
320 |
apply (erule allE)+ |
|
321 |
apply (drule mp) |
|
322 |
prefer 2 apply (assumption) |
|
323 |
apply simp |
|
324 |
done |
|
19741 | 325 |
|
326 |
||
62116 | 327 |
text \<open> |
328 |
Projection of \<open>mkex (sch, exA, exB)\<close> onto \<open>B\<close> stutters on \<open>B\<close> |
|
329 |
structural induction. |
|
330 |
\<close> |
|
19741 | 331 |
|
62116 | 332 |
lemma stutterB_mkex: |
333 |
"\<forall>exA exB s t. |
|
334 |
Forall (\<lambda>x. x \<in> act (A \<parallel> B)) sch \<and> |
|
335 |
Filter (\<lambda>a. a \<in> act A) $ sch \<sqsubseteq> filter_act $ exA \<and> |
|
336 |
Filter (\<lambda>a. a \<in> act B) $ sch \<sqsubseteq> filter_act $ exB \<longrightarrow> |
|
337 |
stutter (asig_of B) (t, ProjB2 $ (snd (mkex A B sch (s, exA) (t, exB))))" |
|
46469 | 338 |
by (mkex_induct sch exA exB) |
19741 | 339 |
|
340 |
||
62116 | 341 |
lemma stutter_mkex_on_B: |
342 |
"Forall (\<lambda>x. x \<in> act (A \<parallel> B)) sch \<Longrightarrow> |
|
343 |
Filter (\<lambda>a. a \<in> act A) $ sch \<sqsubseteq> filter_act $ (snd exA) \<Longrightarrow> |
|
344 |
Filter (\<lambda>a. a \<in> act B) $ sch \<sqsubseteq> filter_act $ (snd exB) \<Longrightarrow> |
|
345 |
stutter (asig_of B) (ProjB (mkex A B sch exA exB))" |
|
346 |
apply (cut_tac stutterB_mkex) |
|
347 |
apply (simp add: stutter_def ProjB_def mkex_def) |
|
348 |
apply (erule allE)+ |
|
349 |
apply (drule mp) |
|
350 |
prefer 2 apply (assumption) |
|
351 |
apply simp |
|
352 |
done |
|
19741 | 353 |
|
354 |
||
62116 | 355 |
text \<open> |
356 |
Filter of \<open>mkex (sch, exA, exB)\<close> to \<open>A\<close> after projection onto \<open>A\<close> is \<open>exA\<close>, |
|
357 |
using \<open>zip $ (proj1 $ exA) $ (proj2 $ exA)\<close> instead of \<open>exA\<close>, |
|
358 |
because of admissibility problems structural induction. |
|
359 |
\<close> |
|
19741 | 360 |
|
62116 | 361 |
lemma filter_mkex_is_exA_tmp: |
362 |
"\<forall>exA exB s t. |
|
363 |
Forall (\<lambda>x. x \<in> act (A \<parallel> B)) sch \<and> |
|
364 |
Filter (\<lambda>a. a \<in> act A) $ sch \<sqsubseteq> filter_act $ exA \<and> |
|
365 |
Filter (\<lambda>a. a \<in> act B) $ sch \<sqsubseteq> filter_act $ exB \<longrightarrow> |
|
366 |
Filter_ex2 (asig_of A) $ (ProjA2 $ (snd (mkex A B sch (s, exA) (t, exB)))) = |
|
367 |
Zip $ (Filter (\<lambda>a. a \<in> act A) $ sch) $ (Map snd $ exA)" |
|
46469 | 368 |
by (mkex_induct sch exB exA) |
19741 | 369 |
|
62116 | 370 |
text \<open> |
371 |
\<open>zip $ (proj1 $ y) $ (proj2 $ y) = y\<close> (using the lift operations) |
|
372 |
lemma for admissibility problems |
|
373 |
\<close> |
|
19741 | 374 |
|
62116 | 375 |
lemma Zip_Map_fst_snd: "Zip $ (Map fst $ y) $ (Map snd $ y) = y" |
376 |
by (tactic \<open>Seq_induct_tac @{context} "y" [] 1\<close>) |
|
19741 | 377 |
|
378 |
||
62116 | 379 |
text \<open> |
380 |
\<open>filter A $ sch = proj1 $ ex \<longrightarrow> zip $ (filter A $ sch) $ (proj2 $ ex) = ex\<close> |
|
381 |
lemma for eliminating non admissible equations in assumptions |
|
382 |
\<close> |
|
383 |
||
384 |
lemma trick_against_eq_in_ass: |
|
385 |
"Filter (\<lambda>a. a \<in> act AB) $ sch = filter_act $ ex \<Longrightarrow> |
|
386 |
ex = Zip $ (Filter (\<lambda>a. a \<in> act AB) $ sch) $ (Map snd $ ex)" |
|
387 |
apply (simp add: filter_act_def) |
|
388 |
apply (rule Zip_Map_fst_snd [symmetric]) |
|
389 |
done |
|
390 |
||
391 |
text \<open> |
|
392 |
Filter of \<open>mkex (sch, exA, exB)\<close> to \<open>A\<close> after projection onto \<open>A\<close> is \<open>exA\<close> |
|
393 |
using the above trick. |
|
394 |
\<close> |
|
19741 | 395 |
|
62116 | 396 |
lemma filter_mkex_is_exA: |
397 |
"Forall (\<lambda>a. a \<in> act (A \<parallel> B)) sch \<Longrightarrow> |
|
398 |
Filter (\<lambda>a. a \<in> act A) $ sch = filter_act $ (snd exA) \<Longrightarrow> |
|
399 |
Filter (\<lambda>a. a \<in> act B) $ sch = filter_act $ (snd exB) \<Longrightarrow> |
|
400 |
Filter_ex (asig_of A) (ProjA (mkex A B sch exA exB)) = exA" |
|
401 |
apply (simp add: ProjA_def Filter_ex_def) |
|
402 |
apply (tactic \<open>pair_tac @{context} "exA" 1\<close>) |
|
403 |
apply (tactic \<open>pair_tac @{context} "exB" 1\<close>) |
|
404 |
apply (rule conjI) |
|
405 |
apply (simp (no_asm) add: mkex_def) |
|
406 |
apply (simplesubst trick_against_eq_in_ass) |
|
407 |
back |
|
408 |
apply assumption |
|
409 |
apply (simp add: filter_mkex_is_exA_tmp) |
|
410 |
done |
|
19741 | 411 |
|
62116 | 412 |
text \<open> |
413 |
Filter of \<open>mkex (sch, exA, exB)\<close> to \<open>B\<close> after projection onto \<open>B\<close> is \<open>exB\<close> |
|
414 |
using \<open>zip $ (proj1 $ exB) $ (proj2 $ exB)\<close> instead of \<open>exB\<close> |
|
415 |
because of admissibility problems structural induction. |
|
416 |
\<close> |
|
19741 | 417 |
|
62116 | 418 |
lemma filter_mkex_is_exB_tmp: |
419 |
"\<forall>exA exB s t. |
|
420 |
Forall (\<lambda>x. x \<in> act (A \<parallel> B)) sch \<and> |
|
421 |
Filter (\<lambda>a. a \<in> act A) $ sch \<sqsubseteq> filter_act $ exA \<and> |
|
422 |
Filter (\<lambda>a. a \<in> act B) $ sch \<sqsubseteq> filter_act $ exB \<longrightarrow> |
|
423 |
Filter_ex2 (asig_of B) $ (ProjB2 $ (snd (mkex A B sch (s, exA) (t, exB)))) = |
|
424 |
Zip $ (Filter (\<lambda>a. a \<in> act B) $ sch) $ (Map snd $ exB)" |
|
425 |
(*notice necessary change of arguments exA and exB*) |
|
426 |
by (mkex_induct sch exA exB) |
|
427 |
||
428 |
text \<open> |
|
429 |
Filter of \<open>mkex (sch, exA, exB)\<close> to \<open>A\<close> after projection onto \<open>B\<close> is \<open>exB\<close> |
|
430 |
using the above trick. |
|
431 |
\<close> |
|
19741 | 432 |
|
62116 | 433 |
lemma filter_mkex_is_exB: |
434 |
"Forall (\<lambda>a. a \<in> act (A \<parallel> B)) sch \<Longrightarrow> |
|
435 |
Filter (\<lambda>a. a \<in> act A) $ sch = filter_act $ (snd exA) \<Longrightarrow> |
|
436 |
Filter (\<lambda>a. a \<in> act B) $ sch = filter_act $ (snd exB) \<Longrightarrow> |
|
437 |
Filter_ex (asig_of B) (ProjB (mkex A B sch exA exB)) = exB" |
|
438 |
apply (simp add: ProjB_def Filter_ex_def) |
|
439 |
apply (tactic \<open>pair_tac @{context} "exA" 1\<close>) |
|
440 |
apply (tactic \<open>pair_tac @{context} "exB" 1\<close>) |
|
441 |
apply (rule conjI) |
|
442 |
apply (simp (no_asm) add: mkex_def) |
|
443 |
apply (simplesubst trick_against_eq_in_ass) |
|
444 |
back |
|
445 |
apply assumption |
|
446 |
apply (simp add: filter_mkex_is_exB_tmp) |
|
447 |
done |
|
19741 | 448 |
|
62116 | 449 |
lemma mkex_actions_in_AorB: |
450 |
\<comment> \<open>\<open>mkex\<close> has only \<open>A\<close>- or \<open>B\<close>-actions\<close> |
|
451 |
"\<forall>s t exA exB. |
|
452 |
Forall (\<lambda>x. x \<in> act (A \<parallel> B)) sch & |
|
453 |
Filter (\<lambda>a. a \<in> act A) $ sch \<sqsubseteq> filter_act $ exA \<and> |
|
454 |
Filter (\<lambda>a. a \<in> act B) $ sch \<sqsubseteq> filter_act $ exB \<longrightarrow> |
|
455 |
Forall (\<lambda>x. fst x \<in> act (A \<parallel> B)) (snd (mkex A B sch (s, exA) (t, exB)))" |
|
46469 | 456 |
by (mkex_induct sch exA exB) |
19741 | 457 |
|
458 |
||
62116 | 459 |
theorem compositionality_sch: |
460 |
"sch \<in> schedules (A \<parallel> B) \<longleftrightarrow> |
|
461 |
Filter (\<lambda>a. a \<in> act A) $ sch \<in> schedules A \<and> |
|
462 |
Filter (\<lambda>a. a \<in> act B) $ sch \<in> schedules B \<and> |
|
463 |
Forall (\<lambda>x. x \<in> act (A \<parallel> B)) sch" |
|
464 |
apply (simp add: schedules_def has_schedule_def) |
|
465 |
apply auto |
|
466 |
text \<open>\<open>\<Longrightarrow>\<close>\<close> |
|
467 |
apply (rule_tac x = "Filter_ex (asig_of A) (ProjA ex)" in bexI) |
|
468 |
prefer 2 |
|
469 |
apply (simp add: compositionality_ex) |
|
470 |
apply (simp (no_asm) add: Filter_ex_def ProjA_def lemma_2_1a lemma_2_1b) |
|
471 |
apply (rule_tac x = "Filter_ex (asig_of B) (ProjB ex)" in bexI) |
|
472 |
prefer 2 |
|
473 |
apply (simp add: compositionality_ex) |
|
474 |
apply (simp (no_asm) add: Filter_ex_def ProjB_def lemma_2_1a lemma_2_1b) |
|
475 |
apply (simp add: executions_def) |
|
476 |
apply (tactic \<open>pair_tac @{context} "ex" 1\<close>) |
|
477 |
apply (erule conjE) |
|
478 |
apply (simp add: sch_actions_in_AorB) |
|
479 |
text \<open>\<open>\<Longleftarrow>\<close>\<close> |
|
480 |
text \<open>\<open>mkex\<close> is exactly the construction of \<open>exA\<parallel>B\<close> out of \<open>exA\<close>, \<open>exB\<close>, |
|
481 |
and the oracle \<open>sch\<close>, we need here\<close> |
|
482 |
apply (rename_tac exA exB) |
|
483 |
apply (rule_tac x = "mkex A B sch exA exB" in bexI) |
|
484 |
text \<open>\<open>mkex\<close> actions are just the oracle\<close> |
|
485 |
apply (tactic \<open>pair_tac @{context} "exA" 1\<close>) |
|
486 |
apply (tactic \<open>pair_tac @{context} "exB" 1\<close>) |
|
487 |
apply (simp add: Mapfst_mkex_is_sch) |
|
488 |
text \<open>\<open>mkex\<close> is an execution -- use compositionality on ex-level\<close> |
|
489 |
apply (simp add: compositionality_ex) |
|
490 |
apply (simp add: stutter_mkex_on_A stutter_mkex_on_B filter_mkex_is_exB filter_mkex_is_exA) |
|
491 |
apply (tactic \<open>pair_tac @{context} "exA" 1\<close>) |
|
492 |
apply (tactic \<open>pair_tac @{context} "exB" 1\<close>) |
|
493 |
apply (simp add: mkex_actions_in_AorB) |
|
494 |
done |
|
19741 | 495 |
|
62116 | 496 |
theorem compositionality_sch_modules: |
497 |
"Scheds (A \<parallel> B) = par_scheds (Scheds A) (Scheds B)" |
|
498 |
apply (unfold Scheds_def par_scheds_def) |
|
499 |
apply (simp add: asig_of_par) |
|
500 |
apply (rule set_eqI) |
|
501 |
apply (simp add: compositionality_sch actions_of_par) |
|
502 |
done |
|
19741 | 503 |
|
504 |
declare compoex_simps [simp del] |
|
505 |
declare composch_simps [simp del] |
|
506 |
||
507 |
end |