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