src/HOL/HOLCF/IOA/meta_theory/CompoScheds.thy
author wenzelm
Sun Nov 09 17:04:14 2014 +0100 (2014-11-09)
changeset 58957 c9e744ea8a38
parent 58880 0baae4311a9f
child 61999 89291b5d0ede
permissions -rw-r--r--
proper context for match_tac etc.;
     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
   301           (safe_tac (Context.raw_transfer (Proof_Context.theory_of ctxt) @{theory_context Fun})),
   302          Seq_case_simp_tac ctxt exA,
   303          Seq_case_simp_tac ctxt exB,
   304          asm_full_simp_tac ctxt,
   305          Seq_case_simp_tac ctxt exA,
   306          asm_full_simp_tac ctxt,
   307          Seq_case_simp_tac ctxt exB,
   308          asm_full_simp_tac ctxt,
   309          asm_full_simp_tac (ctxt addsimps asigs)
   310         ]
   311 
   312 end
   313 *}
   314 
   315 method_setup mkex_induct = {*
   316   Scan.lift (Args.name -- Args.name -- Args.name)
   317     >> (fn ((sch, exA), exB) => fn ctxt => SIMPLE_METHOD' (mkex_induct_tac ctxt sch exA exB))
   318 *}
   319 
   320 
   321 (*---------------------------------------------------------------------------
   322                Projection of mkex(sch,exA,exB) onto A stutters on A
   323                              structural induction
   324   --------------------------------------------------------------------------- *)
   325 
   326 lemma stutterA_mkex: "! exA exB s t.
   327   Forall (%x. x:act (A||B)) sch &
   328   Filter (%a. a:act A)$sch << filter_act$exA &
   329   Filter (%a. a:act B)$sch << filter_act$exB
   330   --> stutter (asig_of A) (s,ProjA2$(snd (mkex A B sch (s,exA) (t,exB))))"
   331   by (mkex_induct sch exA exB)
   332 
   333 lemma stutter_mkex_on_A: "[|
   334   Forall (%x. x:act (A||B)) sch ;
   335   Filter (%a. a:act A)$sch << filter_act$(snd exA) ;
   336   Filter (%a. a:act B)$sch << filter_act$(snd exB) |]
   337   ==> stutter (asig_of A) (ProjA (mkex A B sch exA exB))"
   338 
   339 apply (cut_tac stutterA_mkex)
   340 apply (simp add: stutter_def ProjA_def mkex_def)
   341 apply (erule allE)+
   342 apply (drule mp)
   343 prefer 2 apply (assumption)
   344 apply simp
   345 done
   346 
   347 
   348 (*---------------------------------------------------------------------------
   349                Projection of mkex(sch,exA,exB) onto B stutters on B
   350                              structural induction
   351   --------------------------------------------------------------------------- *)
   352 
   353 lemma stutterB_mkex: "! exA exB s t.
   354   Forall (%x. x:act (A||B)) sch &
   355   Filter (%a. a:act A)$sch << filter_act$exA &
   356   Filter (%a. a:act B)$sch << filter_act$exB
   357   --> stutter (asig_of B) (t,ProjB2$(snd (mkex A B sch (s,exA) (t,exB))))"
   358   by (mkex_induct sch exA exB)
   359 
   360 
   361 lemma stutter_mkex_on_B: "[|
   362   Forall (%x. x:act (A||B)) sch ;
   363   Filter (%a. a:act A)$sch << filter_act$(snd exA) ;
   364   Filter (%a. a:act B)$sch << filter_act$(snd exB) |]
   365   ==> stutter (asig_of B) (ProjB (mkex A B sch exA exB))"
   366 apply (cut_tac stutterB_mkex)
   367 apply (simp add: stutter_def ProjB_def mkex_def)
   368 apply (erule allE)+
   369 apply (drule mp)
   370 prefer 2 apply (assumption)
   371 apply simp
   372 done
   373 
   374 
   375 (*---------------------------------------------------------------------------
   376      Filter of mkex(sch,exA,exB) to A after projection onto A is exA
   377         --  using zip$(proj1$exA)$(proj2$exA) instead of exA    --
   378         --           because of admissibility problems          --
   379                              structural induction
   380   --------------------------------------------------------------------------- *)
   381 
   382 lemma filter_mkex_is_exA_tmp: "! exA exB s t.
   383   Forall (%x. x:act (A||B)) sch &
   384   Filter (%a. a:act A)$sch << filter_act$exA  &
   385   Filter (%a. a:act B)$sch << filter_act$exB
   386   --> Filter_ex2 (asig_of A)$(ProjA2$(snd (mkex A B sch (s,exA) (t,exB)))) =
   387       Zip$(Filter (%a. a:act A)$sch)$(Map snd$exA)"
   388   by (mkex_induct sch exB exA)
   389 
   390 (*---------------------------------------------------------------------------
   391                       zip$(proj1$y)$(proj2$y) = y   (using the lift operations)
   392                     lemma for admissibility problems
   393   --------------------------------------------------------------------------- *)
   394 
   395 lemma Zip_Map_fst_snd: "Zip$(Map fst$y)$(Map snd$y) = y"
   396 apply (tactic {* Seq_induct_tac @{context} "y" [] 1 *})
   397 done
   398 
   399 
   400 (*---------------------------------------------------------------------------
   401       filter A$sch = proj1$ex   -->  zip$(filter A$sch)$(proj2$ex) = ex
   402          lemma for eliminating non admissible equations in assumptions
   403   --------------------------------------------------------------------------- *)
   404 
   405 lemma trick_against_eq_in_ass: "!! sch ex.
   406   Filter (%a. a:act AB)$sch = filter_act$ex
   407   ==> ex = Zip$(Filter (%a. a:act AB)$sch)$(Map snd$ex)"
   408 apply (simp add: filter_act_def)
   409 apply (rule Zip_Map_fst_snd [symmetric])
   410 done
   411 
   412 (*---------------------------------------------------------------------------
   413      Filter of mkex(sch,exA,exB) to A after projection onto A is exA
   414                        using the above trick
   415   --------------------------------------------------------------------------- *)
   416 
   417 
   418 lemma filter_mkex_is_exA: "!!sch exA exB.
   419   [| Forall (%a. a:act (A||B)) sch ;
   420   Filter (%a. a:act A)$sch = filter_act$(snd exA)  ;
   421   Filter (%a. a:act B)$sch = filter_act$(snd exB) |]
   422   ==> Filter_ex (asig_of A) (ProjA (mkex A B sch exA exB)) = exA"
   423 apply (simp add: ProjA_def Filter_ex_def)
   424 apply (tactic {* pair_tac @{context} "exA" 1 *})
   425 apply (tactic {* pair_tac @{context} "exB" 1 *})
   426 apply (rule conjI)
   427 apply (simp (no_asm) add: mkex_def)
   428 apply (simplesubst trick_against_eq_in_ass)
   429 back
   430 apply assumption
   431 apply (simp add: filter_mkex_is_exA_tmp)
   432 done
   433 
   434 
   435 (*---------------------------------------------------------------------------
   436      Filter of mkex(sch,exA,exB) to B after projection onto B is exB
   437         --  using zip$(proj1$exB)$(proj2$exB) instead of exB    --
   438         --           because of admissibility problems          --
   439                              structural induction
   440   --------------------------------------------------------------------------- *)
   441 
   442 lemma filter_mkex_is_exB_tmp: "! exA exB s t.
   443   Forall (%x. x:act (A||B)) sch &
   444   Filter (%a. a:act A)$sch << filter_act$exA  &
   445   Filter (%a. a:act B)$sch << filter_act$exB
   446   --> Filter_ex2 (asig_of B)$(ProjB2$(snd (mkex A B sch (s,exA) (t,exB)))) =
   447       Zip$(Filter (%a. a:act B)$sch)$(Map snd$exB)"
   448 
   449 (* notice necessary change of arguments exA and exB *)
   450   by (mkex_induct sch exA exB)
   451 
   452 
   453 (*---------------------------------------------------------------------------
   454      Filter of mkex(sch,exA,exB) to A after projection onto B is exB
   455                        using the above trick
   456   --------------------------------------------------------------------------- *)
   457 
   458 
   459 lemma filter_mkex_is_exB: "!!sch exA exB.
   460   [| Forall (%a. a:act (A||B)) sch ;
   461   Filter (%a. a:act A)$sch = filter_act$(snd exA)  ;
   462   Filter (%a. a:act B)$sch = filter_act$(snd exB) |]
   463   ==> Filter_ex (asig_of B) (ProjB (mkex A B sch exA exB)) = exB"
   464 apply (simp add: ProjB_def Filter_ex_def)
   465 apply (tactic {* pair_tac @{context} "exA" 1 *})
   466 apply (tactic {* pair_tac @{context} "exB" 1 *})
   467 apply (rule conjI)
   468 apply (simp (no_asm) add: mkex_def)
   469 apply (simplesubst trick_against_eq_in_ass)
   470 back
   471 apply assumption
   472 apply (simp add: filter_mkex_is_exB_tmp)
   473 done
   474 
   475 (* --------------------------------------------------------------------- *)
   476 (*                    mkex has only  A- or B-actions                    *)
   477 (* --------------------------------------------------------------------- *)
   478 
   479 
   480 lemma mkex_actions_in_AorB: "!s t exA exB.
   481   Forall (%x. x : act (A || B)) sch &
   482   Filter (%a. a:act A)$sch << filter_act$exA  &
   483   Filter (%a. a:act B)$sch << filter_act$exB
   484    --> Forall (%x. fst x : act (A ||B))
   485          (snd (mkex A B sch (s,exA) (t,exB)))"
   486   by (mkex_induct sch exA exB)
   487 
   488 
   489 (* ------------------------------------------------------------------ *)
   490 (*           COMPOSITIONALITY   on    SCHEDULE      Level             *)
   491 (*                          Main Theorem                              *)
   492 (* ------------------------------------------------------------------ *)
   493 
   494 lemma compositionality_sch:
   495 "(sch : schedules (A||B)) =
   496   (Filter (%a. a:act A)$sch : schedules A &
   497    Filter (%a. a:act B)$sch : schedules B &
   498    Forall (%x. x:act (A||B)) sch)"
   499 apply (simp (no_asm) add: schedules_def has_schedule_def)
   500 apply auto
   501 (* ==> *)
   502 apply (rule_tac x = "Filter_ex (asig_of A) (ProjA ex) " in bexI)
   503 prefer 2
   504 apply (simp add: compositionality_ex)
   505 apply (simp (no_asm) add: Filter_ex_def ProjA_def lemma_2_1a lemma_2_1b)
   506 apply (rule_tac x = "Filter_ex (asig_of B) (ProjB ex) " in bexI)
   507 prefer 2
   508 apply (simp add: compositionality_ex)
   509 apply (simp (no_asm) add: Filter_ex_def ProjB_def lemma_2_1a lemma_2_1b)
   510 apply (simp add: executions_def)
   511 apply (tactic {* pair_tac @{context} "ex" 1 *})
   512 apply (erule conjE)
   513 apply (simp add: sch_actions_in_AorB)
   514 
   515 (* <== *)
   516 
   517 (* mkex is exactly the construction of exA||B out of exA, exB, and the oracle sch,
   518    we need here *)
   519 apply (rename_tac exA exB)
   520 apply (rule_tac x = "mkex A B sch exA exB" in bexI)
   521 (* mkex actions are just the oracle *)
   522 apply (tactic {* pair_tac @{context} "exA" 1 *})
   523 apply (tactic {* pair_tac @{context} "exB" 1 *})
   524 apply (simp add: Mapfst_mkex_is_sch)
   525 
   526 (* mkex is an execution -- use compositionality on ex-level *)
   527 apply (simp add: compositionality_ex)
   528 apply (simp add: stutter_mkex_on_A stutter_mkex_on_B filter_mkex_is_exB filter_mkex_is_exA)
   529 apply (tactic {* pair_tac @{context} "exA" 1 *})
   530 apply (tactic {* pair_tac @{context} "exB" 1 *})
   531 apply (simp add: mkex_actions_in_AorB)
   532 done
   533 
   534 
   535 subsection {* COMPOSITIONALITY on SCHEDULE Level -- for Modules *}
   536 
   537 lemma compositionality_sch_modules:
   538   "Scheds (A||B) = par_scheds (Scheds A) (Scheds B)"
   539 
   540 apply (unfold Scheds_def par_scheds_def)
   541 apply (simp add: asig_of_par)
   542 apply (rule set_eqI)
   543 apply (simp add: compositionality_sch actions_of_par)
   544 done
   545 
   546 
   547 declare compoex_simps [simp del]
   548 declare composch_simps [simp del]
   549 
   550 end