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