author | wenzelm |
Sun, 17 Jan 2016 00:14:45 +0100 | |
changeset 62195 | 799a5306e2ed |
parent 62116 | bc178c0fe1a1 |
child 63120 | 629a4c5e953e |
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" |
|
62195 | 203 |
by (pair_induct xs) |
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)" |
|
62195 | 217 |
apply (pair_induct xs simp: is_exec_frag_def Forall_def sforall_def) |
62116 | 218 |
text \<open>main case\<close> |
219 |
apply auto |
|
220 |
apply (simp add: trans_of_defs2 actions_asig_comp asig_of_par) |
|
221 |
done |
|
19741 | 222 |
|
223 |
||
62116 | 224 |
subsubsection \<open>Lemmas for \<open>\<Longleftarrow>\<close>\<close> |
19741 | 225 |
|
62116 | 226 |
text \<open> |
227 |
Filtering actions out of \<open>mkex (sch, exA, exB)\<close> yields the oracle \<open>sch\<close> |
|
228 |
structural induction. |
|
229 |
\<close> |
|
19741 | 230 |
|
62116 | 231 |
lemma Mapfst_mkex_is_sch: |
232 |
"\<forall>exA exB s t. |
|
233 |
Forall (\<lambda>x. x \<in> act (A \<parallel> B)) sch \<and> |
|
234 |
Filter (\<lambda>a. a \<in> act A) $ sch \<sqsubseteq> filter_act $ exA \<and> |
|
235 |
Filter (\<lambda>a. a \<in> act B) $ sch \<sqsubseteq> filter_act $ exB \<longrightarrow> |
|
236 |
filter_act $ (snd (mkex A B sch (s, exA) (t, exB))) = sch" |
|
62195 | 237 |
apply (Seq_induct sch simp: Filter_def Forall_def sforall_def mkex_def) |
19741 | 238 |
|
62116 | 239 |
text \<open>main case: splitting into 4 cases according to \<open>a \<in> A\<close>, \<open>a \<in> B\<close>\<close> |
240 |
apply auto |
|
19741 | 241 |
|
62116 | 242 |
text \<open>Case \<open>y \<in> A\<close>, \<open>y \<in> B\<close>\<close> |
62195 | 243 |
apply (Seq_case_simp exA) |
62116 | 244 |
text \<open>Case \<open>exA = UU\<close>, Case \<open>exA = nil\<close>\<close> |
245 |
text \<open> |
|
246 |
These \<open>UU\<close> and \<open>nil\<close> cases are the only places where the assumption |
|
247 |
\<open>filter A sch \<sqsubseteq> f_act exA\<close> is used! |
|
248 |
\<open>\<longrightarrow>\<close> to generate a contradiction using \<open>\<not> a \<leadsto> ss \<sqsubseteq> UU nil\<close>, |
|
249 |
using theorems \<open>Cons_not_less_UU\<close> and \<open>Cons_not_less_nil\<close>.\<close> |
|
62195 | 250 |
apply (Seq_case_simp exB) |
62116 | 251 |
text \<open>Case \<open>exA = a \<leadsto> x\<close>, \<open>exB = b \<leadsto> y\<close>\<close> |
252 |
text \<open> |
|
62195 | 253 |
Here it is important that @{method Seq_case_simp} uses no \<open>!full!_simp_tac\<close> |
62116 | 254 |
for the cons case, as otherwise \<open>mkex_cons_3\<close> would not be rewritten |
255 |
without use of \<open>rotate_tac\<close>: then tactic would not be generally |
|
256 |
applicable.\<close> |
|
257 |
apply simp |
|
19741 | 258 |
|
62116 | 259 |
text \<open>Case \<open>y \<in> A\<close>, \<open>y \<notin> B\<close>\<close> |
62195 | 260 |
apply (Seq_case_simp exA) |
62116 | 261 |
apply simp |
19741 | 262 |
|
62116 | 263 |
text \<open>Case \<open>y \<notin> A\<close>, \<open>y \<in> B\<close>\<close> |
62195 | 264 |
apply (Seq_case_simp exB) |
62116 | 265 |
apply simp |
19741 | 266 |
|
62116 | 267 |
text \<open>Case \<open>y \<notin> A\<close>, \<open>y \<notin> B\<close>\<close> |
268 |
apply (simp add: asig_of_par actions_asig_comp) |
|
269 |
done |
|
19741 | 270 |
|
271 |
||
62116 | 272 |
text \<open>Generalizing the proof above to a proof method:\<close> |
62002 | 273 |
ML \<open> |
27208
5fe899199f85
proper context for tactics derived from res_inst_tac;
wenzelm
parents:
26359
diff
changeset
|
274 |
fun mkex_induct_tac ctxt sch exA exB = |
62116 | 275 |
EVERY' [ |
276 |
Seq_induct_tac ctxt sch |
|
277 |
@{thms Filter_def Forall_def sforall_def mkex_def stutter_def}, |
|
278 |
asm_full_simp_tac ctxt, |
|
279 |
SELECT_GOAL |
|
280 |
(safe_tac (Context.raw_transfer (Proof_Context.theory_of ctxt) @{theory_context Fun})), |
|
281 |
Seq_case_simp_tac ctxt exA, |
|
282 |
Seq_case_simp_tac ctxt exB, |
|
283 |
asm_full_simp_tac ctxt, |
|
284 |
Seq_case_simp_tac ctxt exA, |
|
285 |
asm_full_simp_tac ctxt, |
|
286 |
Seq_case_simp_tac ctxt exB, |
|
287 |
asm_full_simp_tac ctxt, |
|
288 |
asm_full_simp_tac (ctxt addsimps @{thms asig_of_par actions_asig_comp})] |
|
62002 | 289 |
\<close> |
19741 | 290 |
|
62002 | 291 |
method_setup mkex_induct = \<open> |
46469 | 292 |
Scan.lift (Args.name -- Args.name -- Args.name) |
62116 | 293 |
>> (fn ((sch, exA), exB) => fn ctxt => |
294 |
SIMPLE_METHOD' (mkex_induct_tac ctxt sch exA exB)) |
|
62002 | 295 |
\<close> |
46469 | 296 |
|
19741 | 297 |
|
62116 | 298 |
text \<open> |
299 |
Projection of \<open>mkex (sch, exA, exB)\<close> onto \<open>A\<close> stutters on \<open>A\<close> |
|
300 |
structural induction. |
|
301 |
\<close> |
|
19741 | 302 |
|
62116 | 303 |
lemma stutterA_mkex: |
304 |
"\<forall>exA exB s t. |
|
305 |
Forall (\<lambda>x. x \<in> act (A \<parallel> B)) sch \<and> |
|
306 |
Filter (\<lambda>a. a \<in> act A) $ sch \<sqsubseteq> filter_act $ exA \<and> |
|
307 |
Filter (\<lambda>a. a \<in> act B) $ sch \<sqsubseteq> filter_act $ exB \<longrightarrow> |
|
308 |
stutter (asig_of A) (s, ProjA2 $ (snd (mkex A B sch (s, exA) (t, exB))))" |
|
46469 | 309 |
by (mkex_induct sch exA exB) |
19741 | 310 |
|
62116 | 311 |
lemma stutter_mkex_on_A: |
312 |
"Forall (\<lambda>x. x \<in> act (A \<parallel> B)) sch \<Longrightarrow> |
|
313 |
Filter (\<lambda>a. a \<in> act A) $ sch \<sqsubseteq> filter_act $ (snd exA) \<Longrightarrow> |
|
314 |
Filter (\<lambda>a. a \<in> act B) $ sch \<sqsubseteq> filter_act $ (snd exB) \<Longrightarrow> |
|
315 |
stutter (asig_of A) (ProjA (mkex A B sch exA exB))" |
|
316 |
apply (cut_tac stutterA_mkex) |
|
317 |
apply (simp add: stutter_def ProjA_def mkex_def) |
|
318 |
apply (erule allE)+ |
|
319 |
apply (drule mp) |
|
320 |
prefer 2 apply (assumption) |
|
321 |
apply simp |
|
322 |
done |
|
19741 | 323 |
|
324 |
||
62116 | 325 |
text \<open> |
326 |
Projection of \<open>mkex (sch, exA, exB)\<close> onto \<open>B\<close> stutters on \<open>B\<close> |
|
327 |
structural induction. |
|
328 |
\<close> |
|
19741 | 329 |
|
62116 | 330 |
lemma stutterB_mkex: |
331 |
"\<forall>exA exB s t. |
|
332 |
Forall (\<lambda>x. x \<in> act (A \<parallel> B)) sch \<and> |
|
333 |
Filter (\<lambda>a. a \<in> act A) $ sch \<sqsubseteq> filter_act $ exA \<and> |
|
334 |
Filter (\<lambda>a. a \<in> act B) $ sch \<sqsubseteq> filter_act $ exB \<longrightarrow> |
|
335 |
stutter (asig_of B) (t, ProjB2 $ (snd (mkex A B sch (s, exA) (t, exB))))" |
|
46469 | 336 |
by (mkex_induct sch exA exB) |
19741 | 337 |
|
338 |
||
62116 | 339 |
lemma stutter_mkex_on_B: |
340 |
"Forall (\<lambda>x. x \<in> act (A \<parallel> B)) sch \<Longrightarrow> |
|
341 |
Filter (\<lambda>a. a \<in> act A) $ sch \<sqsubseteq> filter_act $ (snd exA) \<Longrightarrow> |
|
342 |
Filter (\<lambda>a. a \<in> act B) $ sch \<sqsubseteq> filter_act $ (snd exB) \<Longrightarrow> |
|
343 |
stutter (asig_of B) (ProjB (mkex A B sch exA exB))" |
|
344 |
apply (cut_tac stutterB_mkex) |
|
345 |
apply (simp add: stutter_def ProjB_def mkex_def) |
|
346 |
apply (erule allE)+ |
|
347 |
apply (drule mp) |
|
348 |
prefer 2 apply (assumption) |
|
349 |
apply simp |
|
350 |
done |
|
19741 | 351 |
|
352 |
||
62116 | 353 |
text \<open> |
354 |
Filter of \<open>mkex (sch, exA, exB)\<close> to \<open>A\<close> after projection onto \<open>A\<close> is \<open>exA\<close>, |
|
355 |
using \<open>zip $ (proj1 $ exA) $ (proj2 $ exA)\<close> instead of \<open>exA\<close>, |
|
356 |
because of admissibility problems structural induction. |
|
357 |
\<close> |
|
19741 | 358 |
|
62116 | 359 |
lemma filter_mkex_is_exA_tmp: |
360 |
"\<forall>exA exB s t. |
|
361 |
Forall (\<lambda>x. x \<in> act (A \<parallel> B)) sch \<and> |
|
362 |
Filter (\<lambda>a. a \<in> act A) $ sch \<sqsubseteq> filter_act $ exA \<and> |
|
363 |
Filter (\<lambda>a. a \<in> act B) $ sch \<sqsubseteq> filter_act $ exB \<longrightarrow> |
|
364 |
Filter_ex2 (asig_of A) $ (ProjA2 $ (snd (mkex A B sch (s, exA) (t, exB)))) = |
|
365 |
Zip $ (Filter (\<lambda>a. a \<in> act A) $ sch) $ (Map snd $ exA)" |
|
46469 | 366 |
by (mkex_induct sch exB exA) |
19741 | 367 |
|
62116 | 368 |
text \<open> |
369 |
\<open>zip $ (proj1 $ y) $ (proj2 $ y) = y\<close> (using the lift operations) |
|
370 |
lemma for admissibility problems |
|
371 |
\<close> |
|
19741 | 372 |
|
62116 | 373 |
lemma Zip_Map_fst_snd: "Zip $ (Map fst $ y) $ (Map snd $ y) = y" |
62195 | 374 |
by (Seq_induct y) |
19741 | 375 |
|
376 |
||
62116 | 377 |
text \<open> |
378 |
\<open>filter A $ sch = proj1 $ ex \<longrightarrow> zip $ (filter A $ sch) $ (proj2 $ ex) = ex\<close> |
|
379 |
lemma for eliminating non admissible equations in assumptions |
|
380 |
\<close> |
|
381 |
||
382 |
lemma trick_against_eq_in_ass: |
|
383 |
"Filter (\<lambda>a. a \<in> act AB) $ sch = filter_act $ ex \<Longrightarrow> |
|
384 |
ex = Zip $ (Filter (\<lambda>a. a \<in> act AB) $ sch) $ (Map snd $ ex)" |
|
385 |
apply (simp add: filter_act_def) |
|
386 |
apply (rule Zip_Map_fst_snd [symmetric]) |
|
387 |
done |
|
388 |
||
389 |
text \<open> |
|
390 |
Filter of \<open>mkex (sch, exA, exB)\<close> to \<open>A\<close> after projection onto \<open>A\<close> is \<open>exA\<close> |
|
391 |
using the above trick. |
|
392 |
\<close> |
|
19741 | 393 |
|
62116 | 394 |
lemma filter_mkex_is_exA: |
395 |
"Forall (\<lambda>a. a \<in> act (A \<parallel> B)) sch \<Longrightarrow> |
|
396 |
Filter (\<lambda>a. a \<in> act A) $ sch = filter_act $ (snd exA) \<Longrightarrow> |
|
397 |
Filter (\<lambda>a. a \<in> act B) $ sch = filter_act $ (snd exB) \<Longrightarrow> |
|
398 |
Filter_ex (asig_of A) (ProjA (mkex A B sch exA exB)) = exA" |
|
399 |
apply (simp add: ProjA_def Filter_ex_def) |
|
62195 | 400 |
apply (pair exA) |
401 |
apply (pair exB) |
|
62116 | 402 |
apply (rule conjI) |
403 |
apply (simp (no_asm) add: mkex_def) |
|
404 |
apply (simplesubst trick_against_eq_in_ass) |
|
405 |
back |
|
406 |
apply assumption |
|
407 |
apply (simp add: filter_mkex_is_exA_tmp) |
|
408 |
done |
|
19741 | 409 |
|
62116 | 410 |
text \<open> |
411 |
Filter of \<open>mkex (sch, exA, exB)\<close> to \<open>B\<close> after projection onto \<open>B\<close> is \<open>exB\<close> |
|
412 |
using \<open>zip $ (proj1 $ exB) $ (proj2 $ exB)\<close> instead of \<open>exB\<close> |
|
413 |
because of admissibility problems structural induction. |
|
414 |
\<close> |
|
19741 | 415 |
|
62116 | 416 |
lemma filter_mkex_is_exB_tmp: |
417 |
"\<forall>exA exB s t. |
|
418 |
Forall (\<lambda>x. x \<in> act (A \<parallel> B)) sch \<and> |
|
419 |
Filter (\<lambda>a. a \<in> act A) $ sch \<sqsubseteq> filter_act $ exA \<and> |
|
420 |
Filter (\<lambda>a. a \<in> act B) $ sch \<sqsubseteq> filter_act $ exB \<longrightarrow> |
|
421 |
Filter_ex2 (asig_of B) $ (ProjB2 $ (snd (mkex A B sch (s, exA) (t, exB)))) = |
|
422 |
Zip $ (Filter (\<lambda>a. a \<in> act B) $ sch) $ (Map snd $ exB)" |
|
423 |
(*notice necessary change of arguments exA and exB*) |
|
424 |
by (mkex_induct sch exA exB) |
|
425 |
||
426 |
text \<open> |
|
427 |
Filter of \<open>mkex (sch, exA, exB)\<close> to \<open>A\<close> after projection onto \<open>B\<close> is \<open>exB\<close> |
|
428 |
using the above trick. |
|
429 |
\<close> |
|
19741 | 430 |
|
62116 | 431 |
lemma filter_mkex_is_exB: |
432 |
"Forall (\<lambda>a. a \<in> act (A \<parallel> B)) sch \<Longrightarrow> |
|
433 |
Filter (\<lambda>a. a \<in> act A) $ sch = filter_act $ (snd exA) \<Longrightarrow> |
|
434 |
Filter (\<lambda>a. a \<in> act B) $ sch = filter_act $ (snd exB) \<Longrightarrow> |
|
435 |
Filter_ex (asig_of B) (ProjB (mkex A B sch exA exB)) = exB" |
|
436 |
apply (simp add: ProjB_def Filter_ex_def) |
|
62195 | 437 |
apply (pair exA) |
438 |
apply (pair exB) |
|
62116 | 439 |
apply (rule conjI) |
62195 | 440 |
apply (simp add: mkex_def) |
62116 | 441 |
apply (simplesubst trick_against_eq_in_ass) |
442 |
back |
|
443 |
apply assumption |
|
444 |
apply (simp add: filter_mkex_is_exB_tmp) |
|
445 |
done |
|
19741 | 446 |
|
62116 | 447 |
lemma mkex_actions_in_AorB: |
448 |
\<comment> \<open>\<open>mkex\<close> has only \<open>A\<close>- or \<open>B\<close>-actions\<close> |
|
449 |
"\<forall>s t exA exB. |
|
450 |
Forall (\<lambda>x. x \<in> act (A \<parallel> B)) sch & |
|
451 |
Filter (\<lambda>a. a \<in> act A) $ sch \<sqsubseteq> filter_act $ exA \<and> |
|
452 |
Filter (\<lambda>a. a \<in> act B) $ sch \<sqsubseteq> filter_act $ exB \<longrightarrow> |
|
453 |
Forall (\<lambda>x. fst x \<in> act (A \<parallel> B)) (snd (mkex A B sch (s, exA) (t, exB)))" |
|
46469 | 454 |
by (mkex_induct sch exA exB) |
19741 | 455 |
|
456 |
||
62116 | 457 |
theorem compositionality_sch: |
458 |
"sch \<in> schedules (A \<parallel> B) \<longleftrightarrow> |
|
459 |
Filter (\<lambda>a. a \<in> act A) $ sch \<in> schedules A \<and> |
|
460 |
Filter (\<lambda>a. a \<in> act B) $ sch \<in> schedules B \<and> |
|
461 |
Forall (\<lambda>x. x \<in> act (A \<parallel> B)) sch" |
|
462 |
apply (simp add: schedules_def has_schedule_def) |
|
463 |
apply auto |
|
464 |
text \<open>\<open>\<Longrightarrow>\<close>\<close> |
|
465 |
apply (rule_tac x = "Filter_ex (asig_of A) (ProjA ex)" in bexI) |
|
466 |
prefer 2 |
|
467 |
apply (simp add: compositionality_ex) |
|
468 |
apply (simp (no_asm) add: Filter_ex_def ProjA_def lemma_2_1a lemma_2_1b) |
|
469 |
apply (rule_tac x = "Filter_ex (asig_of B) (ProjB ex)" in bexI) |
|
470 |
prefer 2 |
|
471 |
apply (simp add: compositionality_ex) |
|
62195 | 472 |
apply (simp add: Filter_ex_def ProjB_def lemma_2_1a lemma_2_1b) |
62116 | 473 |
apply (simp add: executions_def) |
62195 | 474 |
apply (pair ex) |
62116 | 475 |
apply (erule conjE) |
476 |
apply (simp add: sch_actions_in_AorB) |
|
477 |
text \<open>\<open>\<Longleftarrow>\<close>\<close> |
|
478 |
text \<open>\<open>mkex\<close> is exactly the construction of \<open>exA\<parallel>B\<close> out of \<open>exA\<close>, \<open>exB\<close>, |
|
479 |
and the oracle \<open>sch\<close>, we need here\<close> |
|
480 |
apply (rename_tac exA exB) |
|
481 |
apply (rule_tac x = "mkex A B sch exA exB" in bexI) |
|
482 |
text \<open>\<open>mkex\<close> actions are just the oracle\<close> |
|
62195 | 483 |
apply (pair exA) |
484 |
apply (pair exB) |
|
62116 | 485 |
apply (simp add: Mapfst_mkex_is_sch) |
486 |
text \<open>\<open>mkex\<close> is an execution -- use compositionality on ex-level\<close> |
|
487 |
apply (simp add: compositionality_ex) |
|
488 |
apply (simp add: stutter_mkex_on_A stutter_mkex_on_B filter_mkex_is_exB filter_mkex_is_exA) |
|
62195 | 489 |
apply (pair exA) |
490 |
apply (pair exB) |
|
62116 | 491 |
apply (simp add: mkex_actions_in_AorB) |
492 |
done |
|
19741 | 493 |
|
62116 | 494 |
theorem compositionality_sch_modules: |
495 |
"Scheds (A \<parallel> B) = par_scheds (Scheds A) (Scheds B)" |
|
496 |
apply (unfold Scheds_def par_scheds_def) |
|
497 |
apply (simp add: asig_of_par) |
|
498 |
apply (rule set_eqI) |
|
499 |
apply (simp add: compositionality_sch actions_of_par) |
|
500 |
done |
|
19741 | 501 |
|
502 |
declare compoex_simps [simp del] |
|
503 |
declare composch_simps [simp del] |
|
504 |
||
505 |
end |