src/HOLCF/IOA/meta_theory/CompoScheds.thy
author wenzelm
Mon Sep 06 19:13:10 2010 +0200 (2010-09-06)
changeset 39159 0dec18004e75
parent 35215 a03462cbf86f
child 39302 d7728f65b353
permissions -rw-r--r--
more antiquotations;
     1 (*  Title:      HOLCF/IOA/meta_theory/CompoScheds.thy
     2     Author:     Olaf Müller
     3 *)
     4 
     5 header {* 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 tactic *)
   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   let val ss = simpset_of ctxt in
   299     EVERY1[Seq_induct_tac ctxt sch defs,
   300            asm_full_simp_tac ss,
   301            SELECT_GOAL (safe_tac (global_claset_of @{theory Fun})),
   302            Seq_case_simp_tac ctxt exA,
   303            Seq_case_simp_tac ctxt exB,
   304            asm_full_simp_tac ss,
   305            Seq_case_simp_tac ctxt exA,
   306            asm_full_simp_tac ss,
   307            Seq_case_simp_tac ctxt exB,
   308            asm_full_simp_tac ss,
   309            asm_full_simp_tac (ss addsimps asigs)
   310           ]
   311   end
   312 
   313 end
   314 *}
   315 
   316 
   317 (*---------------------------------------------------------------------------
   318                Projection of mkex(sch,exA,exB) onto A stutters on A
   319                              structural induction
   320   --------------------------------------------------------------------------- *)
   321 
   322 lemma stutterA_mkex: "! exA exB s t.
   323   Forall (%x. x:act (A||B)) sch &
   324   Filter (%a. a:act A)$sch << filter_act$exA &
   325   Filter (%a. a:act B)$sch << filter_act$exB
   326   --> stutter (asig_of A) (s,ProjA2$(snd (mkex A B sch (s,exA) (t,exB))))"
   327 
   328 apply (tactic {* mkex_induct_tac @{context} "sch" "exA" "exB" *})
   329 done
   330 
   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 apply (tactic {* mkex_induct_tac @{context} "sch" "exA" "exB" *})
   358 done
   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 apply (tactic {* mkex_induct_tac @{context} "sch" "exB" "exA" *})
   389 done
   390 
   391 (*---------------------------------------------------------------------------
   392                       zip$(proj1$y)$(proj2$y) = y   (using the lift operations)
   393                     lemma for admissibility problems
   394   --------------------------------------------------------------------------- *)
   395 
   396 lemma Zip_Map_fst_snd: "Zip$(Map fst$y)$(Map snd$y) = y"
   397 apply (tactic {* Seq_induct_tac @{context} "y" [] 1 *})
   398 done
   399 
   400 
   401 (*---------------------------------------------------------------------------
   402       filter A$sch = proj1$ex   -->  zip$(filter A$sch)$(proj2$ex) = ex
   403          lemma for eliminating non admissible equations in assumptions
   404   --------------------------------------------------------------------------- *)
   405 
   406 lemma trick_against_eq_in_ass: "!! sch ex.
   407   Filter (%a. a:act AB)$sch = filter_act$ex
   408   ==> ex = Zip$(Filter (%a. a:act AB)$sch)$(Map snd$ex)"
   409 apply (simp add: filter_act_def)
   410 apply (rule Zip_Map_fst_snd [symmetric])
   411 done
   412 
   413 (*---------------------------------------------------------------------------
   414      Filter of mkex(sch,exA,exB) to A after projection onto A is exA
   415                        using the above trick
   416   --------------------------------------------------------------------------- *)
   417 
   418 
   419 lemma filter_mkex_is_exA: "!!sch exA exB.
   420   [| Forall (%a. a:act (A||B)) sch ;
   421   Filter (%a. a:act A)$sch = filter_act$(snd exA)  ;
   422   Filter (%a. a:act B)$sch = filter_act$(snd exB) |]
   423   ==> Filter_ex (asig_of A) (ProjA (mkex A B sch exA exB)) = exA"
   424 apply (simp add: ProjA_def Filter_ex_def)
   425 apply (tactic {* pair_tac @{context} "exA" 1 *})
   426 apply (tactic {* pair_tac @{context} "exB" 1 *})
   427 apply (rule conjI)
   428 apply (simp (no_asm) add: mkex_def)
   429 apply (simplesubst trick_against_eq_in_ass)
   430 back
   431 apply assumption
   432 apply (simp add: filter_mkex_is_exA_tmp)
   433 done
   434 
   435 
   436 (*---------------------------------------------------------------------------
   437      Filter of mkex(sch,exA,exB) to B after projection onto B is exB
   438         --  using zip$(proj1$exB)$(proj2$exB) instead of exB    --
   439         --           because of admissibility problems          --
   440                              structural induction
   441   --------------------------------------------------------------------------- *)
   442 
   443 lemma filter_mkex_is_exB_tmp: "! exA exB s t.
   444   Forall (%x. x:act (A||B)) sch &
   445   Filter (%a. a:act A)$sch << filter_act$exA  &
   446   Filter (%a. a:act B)$sch << filter_act$exB
   447   --> Filter_ex2 (asig_of B)$(ProjB2$(snd (mkex A B sch (s,exA) (t,exB)))) =
   448       Zip$(Filter (%a. a:act B)$sch)$(Map snd$exB)"
   449 
   450 (* notice necessary change of arguments exA and exB *)
   451 apply (tactic {* mkex_induct_tac @{context} "sch" "exA" "exB" *})
   452 done
   453 
   454 
   455 (*---------------------------------------------------------------------------
   456      Filter of mkex(sch,exA,exB) to A after projection onto B is exB
   457                        using the above trick
   458   --------------------------------------------------------------------------- *)
   459 
   460 
   461 lemma filter_mkex_is_exB: "!!sch exA exB.
   462   [| Forall (%a. a:act (A||B)) sch ;
   463   Filter (%a. a:act A)$sch = filter_act$(snd exA)  ;
   464   Filter (%a. a:act B)$sch = filter_act$(snd exB) |]
   465   ==> Filter_ex (asig_of B) (ProjB (mkex A B sch exA exB)) = exB"
   466 apply (simp add: ProjB_def Filter_ex_def)
   467 apply (tactic {* pair_tac @{context} "exA" 1 *})
   468 apply (tactic {* pair_tac @{context} "exB" 1 *})
   469 apply (rule conjI)
   470 apply (simp (no_asm) add: mkex_def)
   471 apply (simplesubst trick_against_eq_in_ass)
   472 back
   473 apply assumption
   474 apply (simp add: filter_mkex_is_exB_tmp)
   475 done
   476 
   477 (* --------------------------------------------------------------------- *)
   478 (*                    mkex has only  A- or B-actions                    *)
   479 (* --------------------------------------------------------------------- *)
   480 
   481 
   482 lemma mkex_actions_in_AorB: "!s t exA exB.
   483   Forall (%x. x : act (A || B)) sch &
   484   Filter (%a. a:act A)$sch << filter_act$exA  &
   485   Filter (%a. a:act B)$sch << filter_act$exB
   486    --> Forall (%x. fst x : act (A ||B))
   487          (snd (mkex A B sch (s,exA) (t,exB)))"
   488 apply (tactic {* mkex_induct_tac @{context} "sch" "exA" "exB" *})
   489 done
   490 
   491 
   492 (* ------------------------------------------------------------------ *)
   493 (*           COMPOSITIONALITY   on    SCHEDULE      Level             *)
   494 (*                          Main Theorem                              *)
   495 (* ------------------------------------------------------------------ *)
   496 
   497 lemma compositionality_sch:
   498 "(sch : schedules (A||B)) =
   499   (Filter (%a. a:act A)$sch : schedules A &
   500    Filter (%a. a:act B)$sch : schedules B &
   501    Forall (%x. x:act (A||B)) sch)"
   502 apply (simp (no_asm) add: schedules_def has_schedule_def)
   503 apply auto
   504 (* ==> *)
   505 apply (rule_tac x = "Filter_ex (asig_of A) (ProjA ex) " in bexI)
   506 prefer 2
   507 apply (simp add: compositionality_ex)
   508 apply (simp (no_asm) add: Filter_ex_def ProjA_def lemma_2_1a lemma_2_1b)
   509 apply (rule_tac x = "Filter_ex (asig_of B) (ProjB ex) " in bexI)
   510 prefer 2
   511 apply (simp add: compositionality_ex)
   512 apply (simp (no_asm) add: Filter_ex_def ProjB_def lemma_2_1a lemma_2_1b)
   513 apply (simp add: executions_def)
   514 apply (tactic {* pair_tac @{context} "ex" 1 *})
   515 apply (erule conjE)
   516 apply (simp add: sch_actions_in_AorB)
   517 
   518 (* <== *)
   519 
   520 (* mkex is exactly the construction of exA||B out of exA, exB, and the oracle sch,
   521    we need here *)
   522 apply (rename_tac exA exB)
   523 apply (rule_tac x = "mkex A B sch exA exB" in bexI)
   524 (* mkex actions are just the oracle *)
   525 apply (tactic {* pair_tac @{context} "exA" 1 *})
   526 apply (tactic {* pair_tac @{context} "exB" 1 *})
   527 apply (simp add: Mapfst_mkex_is_sch)
   528 
   529 (* mkex is an execution -- use compositionality on ex-level *)
   530 apply (simp add: compositionality_ex)
   531 apply (simp add: stutter_mkex_on_A stutter_mkex_on_B filter_mkex_is_exB filter_mkex_is_exA)
   532 apply (tactic {* pair_tac @{context} "exA" 1 *})
   533 apply (tactic {* pair_tac @{context} "exB" 1 *})
   534 apply (simp add: mkex_actions_in_AorB)
   535 done
   536 
   537 
   538 subsection {* COMPOSITIONALITY on SCHEDULE Level -- for Modules *}
   539 
   540 lemma compositionality_sch_modules:
   541   "Scheds (A||B) = par_scheds (Scheds A) (Scheds B)"
   542 
   543 apply (unfold Scheds_def par_scheds_def)
   544 apply (simp add: asig_of_par)
   545 apply (rule set_ext)
   546 apply (simp add: compositionality_sch actions_of_par)
   547 done
   548 
   549 
   550 declare compoex_simps [simp del]
   551 declare composch_simps [simp del]
   552 
   553 end