1(*  Title:      HOL/HOLCF/IOA/CompoScheds.thy
2    Author:     Olaf M��ller
3*)
4
5section \<open>Compositionality on Schedule level\<close>
6
7theory CompoScheds
8imports CompoExecs
9begin
10
11definition 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 \<cdot>
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 \<cdot> exA of
26                      UU \<Rightarrow> UU
27                    | Def a \<Rightarrow>
28                        (case HD \<cdot> exB of
29                          UU \<Rightarrow> UU
30                        | Def b \<Rightarrow>
31                           (y, (snd a, snd b)) \<leadsto>
32                            (h \<cdot> xs \<cdot> (TL \<cdot> exA) \<cdot> (TL \<cdot> exB)) (snd a) (snd b)))
33                  else
34                    (case HD \<cdot> exA of
35                      UU \<Rightarrow> UU
36                    | Def a \<Rightarrow> (y, (snd a, t)) \<leadsto> (h \<cdot> xs \<cdot> (TL \<cdot> exA) \<cdot> exB) (snd a) t))
37                else
38                  (if y \<in> act B then
39                    (case HD \<cdot> exB of
40                      UU \<Rightarrow> UU
41                    | Def b \<Rightarrow> (y, (s, snd b)) \<leadsto> (h \<cdot> xs \<cdot> exA \<cdot> (TL \<cdot> exB)) s (snd b))
42                   else UU))))))"
43
44definition 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 \<cdot> sch \<cdot> (snd exA) \<cdot> (snd exB)) (fst exA) (fst exB))"
48
49definition 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 (\<lambda>a. a\<in>actions sigA)\<cdot>sch \<in> schA} \<inter>
56       {sch. Filter (\<lambda>a. a\<in>actions sigB)\<cdot>sch \<in> schB} \<inter>
57       {sch. Forall (\<lambda>x. x\<in>(actions sigA Un actions sigB)) sch},
58        asig_comp sigA sigB))"
59
60
61subsection \<open>\<open>mkex\<close> rewrite rules\<close>
62
63lemma mkex2_unfold:
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 \<cdot> exA of
76                      UU \<Rightarrow> UU
77                    | Def a \<Rightarrow>
78                        (case HD \<cdot> exB of
79                          UU \<Rightarrow> UU
80                        | Def b \<Rightarrow>
81                            (y, (snd a, snd b)) \<leadsto>
82                              (mkex2 A B \<cdot> xs \<cdot> (TL \<cdot> exA) \<cdot> (TL \<cdot> exB)) (snd a) (snd b)))
83                   else
84                     (case HD \<cdot> exA of
85                       UU \<Rightarrow> UU
86                     | Def a \<Rightarrow> (y, (snd a, t)) \<leadsto> (mkex2 A B \<cdot> xs \<cdot> (TL \<cdot> exA) \<cdot> exB) (snd a) t))
87                 else
88                   (if y \<in> act B then
89                     (case HD \<cdot> exB of
90                       UU \<Rightarrow> UU
91                     | Def b \<Rightarrow> (y, (s, snd b)) \<leadsto> (mkex2 A B \<cdot> xs \<cdot> exA \<cdot> (TL \<cdot> 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
99
100lemma mkex2_UU: "(mkex2 A B \<cdot> UU \<cdot> exA \<cdot> exB) s t = UU"
101  apply (subst mkex2_unfold)
102  apply simp
103  done
104
105lemma mkex2_nil: "(mkex2 A B \<cdot> nil \<cdot> exA \<cdot> exB) s t = nil"
106  apply (subst mkex2_unfold)
107  apply simp
108  done
109
110lemma mkex2_cons_1:
111  "x \<in> act A \<Longrightarrow> x \<notin> act B \<Longrightarrow> HD \<cdot> exA = Def a \<Longrightarrow>
112    (mkex2 A B \<cdot> (x \<leadsto> sch) \<cdot> exA \<cdot> exB) s t =
113      (x, snd a,t) \<leadsto> (mkex2 A B \<cdot> sch \<cdot> (TL \<cdot> exA) \<cdot> 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
119
120lemma mkex2_cons_2:
121  "x \<notin> act A \<Longrightarrow> x \<in> act B \<Longrightarrow> HD \<cdot> exB = Def b \<Longrightarrow>
122    (mkex2 A B \<cdot> (x \<leadsto> sch) \<cdot> exA \<cdot> exB) s t =
123      (x, s, snd b) \<leadsto> (mkex2 A B \<cdot> sch \<cdot> exA \<cdot> (TL \<cdot> 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
129
130lemma mkex2_cons_3:
131  "x \<in> act A \<Longrightarrow> x \<in> act B \<Longrightarrow> HD \<cdot> exA = Def a \<Longrightarrow> HD \<cdot> exB = Def b \<Longrightarrow>
132    (mkex2 A B \<cdot> (x \<leadsto> sch) \<cdot> exA \<cdot> exB) s t =
133      (x, snd a,snd b) \<leadsto> (mkex2 A B \<cdot> sch \<cdot> (TL \<cdot> exA) \<cdot> (TL \<cdot> 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
139
140declare mkex2_UU [simp] mkex2_nil [simp] mkex2_cons_1 [simp]
141  mkex2_cons_2 [simp] mkex2_cons_3 [simp]
142
143
144subsection \<open>\<open>mkex\<close>\<close>
145
146lemma mkex_UU: "mkex A B UU  (s,exA) (t,exB) = ((s,t),UU)"
147  by (simp add: mkex_def)
148
149lemma mkex_nil: "mkex A B nil (s,exA) (t,exB) = ((s,t),nil)"
150  by (simp add: mkex_def)
151
152lemma 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
160
161lemma 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
169
170lemma 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
178
179declare 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
182lemmas composch_simps = mkex_UU mkex_nil mkex_cons_1 mkex_cons_2 mkex_cons_3
183
184declare composch_simps [simp]
185
186
187subsection \<open>Compositionality on schedule level\<close>
188
189subsubsection \<open>Lemmas for \<open>\<Longrightarrow>\<close>\<close>
190
191lemma lemma_2_1a:
192  \<comment> \<open>\<open>tfilter ex\<close> and \<open>filter_act\<close> are commutative\<close>
193  "filter_act \<cdot> (Filter_ex2 (asig_of A) \<cdot> xs) =
194    Filter (\<lambda>a. a \<in> act A) \<cdot> (filter_act \<cdot> xs)"
195  apply (unfold filter_act_def Filter_ex2_def)
196  apply (simp add: MapFilter o_def)
197  done
198
199lemma lemma_2_1b:
200  \<comment> \<open>State-projections do not affect \<open>filter_act\<close>\<close>
201  "filter_act \<cdot> (ProjA2 \<cdot> xs) = filter_act \<cdot> xs \<and>
202    filter_act \<cdot> (ProjB2 \<cdot> xs) = filter_act \<cdot> xs"
203  by (pair_induct xs)
204
205
206text \<open>
207  Schedules of \<open>A \<parallel> B\<close> have only \<open>A\<close>- or \<open>B\<close>-actions.
208
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>
214
215lemma 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 \<cdot> xs)"
217  apply (pair_induct xs simp: is_exec_frag_def Forall_def sforall_def)
218  text \<open>main case\<close>
219  apply auto
220  apply (simp add: trans_of_defs2 actions_asig_comp asig_of_par)
221  done
222
223
224subsubsection \<open>Lemmas for \<open>\<Longleftarrow>\<close>\<close>
225
226text \<open>
227  Filtering actions out of \<open>mkex (sch, exA, exB)\<close> yields the oracle \<open>sch\<close>
228  structural induction.
229\<close>
230
231lemma 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) \<cdot> sch \<sqsubseteq> filter_act \<cdot> exA \<and>
235    Filter (\<lambda>a. a \<in> act B) \<cdot> sch \<sqsubseteq> filter_act \<cdot> exB \<longrightarrow>
236    filter_act \<cdot> (snd (mkex A B sch (s, exA) (t, exB))) = sch"
237  apply (Seq_induct sch simp: Filter_def Forall_def sforall_def mkex_def)
238
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
241
242  text \<open>Case \<open>y \<in> A\<close>, \<open>y \<in> B\<close>\<close>
243  apply (Seq_case_simp exA)
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>
250  apply (Seq_case_simp exB)
251  text \<open>Case \<open>exA = a \<leadsto> x\<close>, \<open>exB = b \<leadsto> y\<close>\<close>
252  text \<open>
253    Here it is important that @{method Seq_case_simp} uses no \<open>!full!_simp_tac\<close>
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
258
259  text \<open>Case \<open>y \<in> A\<close>, \<open>y \<notin> B\<close>\<close>
260  apply (Seq_case_simp exA)
261  apply simp
262
263  text \<open>Case \<open>y \<notin> A\<close>, \<open>y \<in> B\<close>\<close>
264  apply (Seq_case_simp exB)
265  apply simp
266
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
270
271
272text \<open>Generalizing the proof above to a proof method:\<close>
273ML \<open>
274fun mkex_induct_tac ctxt sch exA exB =
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})]
289\<close>
290
291method_setup mkex_induct = \<open>
292  Scan.lift (Args.embedded -- Args.embedded -- Args.embedded)
293    >> (fn ((sch, exA), exB) => fn ctxt =>
294      SIMPLE_METHOD' (mkex_induct_tac ctxt sch exA exB))
295\<close>
296
297
298text \<open>
299  Projection of \<open>mkex (sch, exA, exB)\<close> onto \<open>A\<close> stutters on \<open>A\<close>
300  structural induction.
301\<close>
302
303lemma 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) \<cdot> sch \<sqsubseteq> filter_act \<cdot> exA \<and>
307    Filter (\<lambda>a. a \<in> act B) \<cdot> sch \<sqsubseteq> filter_act \<cdot> exB \<longrightarrow>
308    stutter (asig_of A) (s, ProjA2 \<cdot> (snd (mkex A B sch (s, exA) (t, exB))))"
309  by (mkex_induct sch exA exB)
310
311lemma stutter_mkex_on_A:
312  "Forall (\<lambda>x. x \<in> act (A \<parallel> B)) sch \<Longrightarrow>
313    Filter (\<lambda>a. a \<in> act A) \<cdot> sch \<sqsubseteq> filter_act \<cdot> (snd exA) \<Longrightarrow>
314    Filter (\<lambda>a. a \<in> act B) \<cdot> sch \<sqsubseteq> filter_act \<cdot> (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
323
324
325text \<open>
326  Projection of \<open>mkex (sch, exA, exB)\<close> onto \<open>B\<close> stutters on \<open>B\<close>
327  structural induction.
328\<close>
329
330lemma 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) \<cdot> sch \<sqsubseteq> filter_act \<cdot> exA \<and>
334    Filter (\<lambda>a. a \<in> act B) \<cdot> sch \<sqsubseteq> filter_act \<cdot> exB \<longrightarrow>
335    stutter (asig_of B) (t, ProjB2 \<cdot> (snd (mkex A B sch (s, exA) (t, exB))))"
336  by (mkex_induct sch exA exB)
337
338
339lemma stutter_mkex_on_B:
340  "Forall (\<lambda>x. x \<in> act (A \<parallel> B)) sch \<Longrightarrow>
341   Filter (\<lambda>a. a \<in> act A) \<cdot> sch \<sqsubseteq> filter_act \<cdot> (snd exA) \<Longrightarrow>
342   Filter (\<lambda>a. a \<in> act B) \<cdot> sch \<sqsubseteq> filter_act \<cdot> (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
351
352
353text \<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 \<cdot> (proj1 \<cdot> exA) \<cdot> (proj2 \<cdot> exA)\<close> instead of \<open>exA\<close>,
356  because of admissibility problems structural induction.
357\<close>
358
359lemma 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) \<cdot> sch \<sqsubseteq> filter_act \<cdot> exA \<and>
363    Filter (\<lambda>a. a \<in> act B) \<cdot> sch \<sqsubseteq> filter_act \<cdot> exB \<longrightarrow>
364    Filter_ex2 (asig_of A) \<cdot> (ProjA2 \<cdot> (snd (mkex A B sch (s, exA) (t, exB)))) =
365      Zip \<cdot> (Filter (\<lambda>a. a \<in> act A) \<cdot> sch) \<cdot> (Map snd \<cdot> exA)"
366  by (mkex_induct sch exB exA)
367
368text \<open>
369  \<open>zip \<cdot> (proj1 \<cdot> y) \<cdot> (proj2 \<cdot> y) = y\<close>  (using the lift operations)
370  lemma for admissibility problems
371\<close>
372
373lemma Zip_Map_fst_snd: "Zip \<cdot> (Map fst \<cdot> y) \<cdot> (Map snd \<cdot> y) = y"
374  by (Seq_induct y)
375
376
377text \<open>
378  \<open>filter A \<cdot> sch = proj1 \<cdot> ex \<longrightarrow> zip \<cdot> (filter A \<cdot> sch) \<cdot> (proj2 \<cdot> ex) = ex\<close>
379  lemma for eliminating non admissible equations in assumptions
380\<close>
381
382lemma trick_against_eq_in_ass:
383  "Filter (\<lambda>a. a \<in> act AB) \<cdot> sch = filter_act \<cdot> ex \<Longrightarrow>
384    ex = Zip \<cdot> (Filter (\<lambda>a. a \<in> act AB) \<cdot> sch) \<cdot> (Map snd \<cdot> ex)"
385  apply (simp add: filter_act_def)
386  apply (rule Zip_Map_fst_snd [symmetric])
387  done
388
389text \<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>
393
394lemma filter_mkex_is_exA:
395  "Forall (\<lambda>a. a \<in> act (A \<parallel> B)) sch \<Longrightarrow>
396    Filter (\<lambda>a. a \<in> act A) \<cdot> sch = filter_act \<cdot> (snd exA) \<Longrightarrow>
397    Filter (\<lambda>a. a \<in> act B) \<cdot> sch = filter_act \<cdot> (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)
400  apply (pair exA)
401  apply (pair exB)
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
409
410text \<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 \<cdot> (proj1 \<cdot> exB) \<cdot> (proj2 \<cdot> exB)\<close> instead of \<open>exB\<close>
413  because of admissibility problems structural induction.
414\<close>
415
416lemma 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) \<cdot> sch \<sqsubseteq> filter_act \<cdot> exA \<and>
420    Filter (\<lambda>a. a \<in> act B) \<cdot> sch \<sqsubseteq> filter_act \<cdot> exB \<longrightarrow>
421    Filter_ex2 (asig_of B) \<cdot> (ProjB2 \<cdot> (snd (mkex A B sch (s, exA) (t, exB)))) =
422      Zip \<cdot> (Filter (\<lambda>a. a \<in> act B) \<cdot> sch) \<cdot> (Map snd \<cdot> exB)"
423  (*notice necessary change of arguments exA and exB*)
424  by (mkex_induct sch exA exB)
425
426text \<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>
430
431lemma filter_mkex_is_exB:
432  "Forall (\<lambda>a. a \<in> act (A \<parallel> B)) sch \<Longrightarrow>
433    Filter (\<lambda>a. a \<in> act A) \<cdot> sch = filter_act \<cdot> (snd exA) \<Longrightarrow>
434    Filter (\<lambda>a. a \<in> act B) \<cdot> sch = filter_act \<cdot> (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)
437  apply (pair exA)
438  apply (pair exB)
439  apply (rule conjI)
440  apply (simp add: mkex_def)
441  apply (simplesubst trick_against_eq_in_ass)
442  back
443  apply assumption
444  apply (simp add: filter_mkex_is_exB_tmp)
445  done
446
447lemma 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) \<cdot> sch \<sqsubseteq> filter_act \<cdot> exA \<and>
452    Filter (\<lambda>a. a \<in> act B) \<cdot> sch \<sqsubseteq> filter_act \<cdot> exB \<longrightarrow>
453    Forall (\<lambda>x. fst x \<in> act (A \<parallel> B)) (snd (mkex A B sch (s, exA) (t, exB)))"
454  by (mkex_induct sch exA exB)
455
456
457theorem compositionality_sch:
458  "sch \<in> schedules (A \<parallel> B) \<longleftrightarrow>
459    Filter (\<lambda>a. a \<in> act A) \<cdot> sch \<in> schedules A \<and>
460    Filter (\<lambda>a. a \<in> act B) \<cdot> 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)
472  apply (simp add: Filter_ex_def ProjB_def lemma_2_1a lemma_2_1b)
473  apply (simp add: executions_def)
474  apply (pair ex)
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>
483  apply (pair exA)
484  apply (pair exB)
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)
489  apply (pair exA)
490  apply (pair exB)
491  apply (simp add: mkex_actions_in_AorB)
492  done
493
494theorem 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
501
502declare compoex_simps [simp del]
503declare composch_simps [simp del]
504
505end
506