src/HOLCF/IOA/meta_theory/CompoScheds.ML
author paulson
Wed Dec 24 10:02:30 1997 +0100 (1997-12-24 ago)
changeset 4477 b3e5857d8d99
parent 4423 a129b817b58a
child 4520 d430a1b34928
permissions -rw-r--r--
New Auto_tac (by Oheimb), and new syntax (without parens), and expandshort
     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 thy "(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 thy "(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 thy "!!x.[| 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 [Cons_def,If_and_if]) 1);
    75 by (asm_full_simp_tac (simpset() addsimps [Cons_def]) 1);
    76 qed"mkex2_cons_1";
    77 
    78 goal thy "!!x.[| 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 [Cons_def,If_and_if]) 1);
    84 by (asm_full_simp_tac (simpset() addsimps [Cons_def]) 1);
    85 qed"mkex2_cons_2";
    86 
    87 goal thy "!!x.[| 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 [Cons_def,If_and_if]) 1);
    94 by (asm_full_simp_tac (simpset() addsimps [Cons_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 thy "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 thy "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 thy "!!x.[| 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] 
   116                        setloop (split_tac [expand_if]) ) 1);
   117 by (cut_inst_tac [("exA","a>>exA")] mkex2_cons_1 1);
   118 by Auto_tac;
   119 qed"mkex_cons_1";
   120 
   121 goal thy "!!x.[| x~:act A; x:act B |] \
   122 \   ==> mkex A B (x>>sch) (s,exA) (t,b>>exB) =  \ 
   123 \       ((s,t), (x,s,snd b) >> snd (mkex A B sch (s,exA) (snd b,exB)))";
   124 by (simp_tac (simpset() addsimps [mkex_def] 
   125                        setloop (split_tac [expand_if]) ) 1);
   126 by (cut_inst_tac [("exB","b>>exB")] mkex2_cons_2 1);
   127 by Auto_tac;
   128 qed"mkex_cons_2";
   129 
   130 goal thy "!!x.[| x:act A; x:act B |]  \
   131 \   ==>  mkex A B (x>>sch) (s,a>>exA) (t,b>>exB) = \
   132 \        ((s,t), (x,snd a,snd b) >> snd (mkex A B sch (snd a,exA) (snd b,exB)))";
   133 by (simp_tac (simpset() addsimps [mkex_def] 
   134                        setloop (split_tac [expand_if]) ) 1);
   135 by (cut_inst_tac [("exB","b>>exB"),("exA","a>>exA")] mkex2_cons_3 1);
   136 by Auto_tac;
   137 qed"mkex_cons_3";
   138 
   139 Delsimps [mkex2_UU,mkex2_nil,mkex2_cons_1,mkex2_cons_2,mkex2_cons_3];
   140 
   141 val composch_simps = [mkex_UU,mkex_nil,
   142                       mkex_cons_1,mkex_cons_2,mkex_cons_3];
   143 
   144 Addsimps composch_simps;
   145 
   146 
   147 
   148 (* ------------------------------------------------------------------ *)
   149 (*                      The following lemmata aim for                 *)
   150 (*             COMPOSITIONALITY   on    SCHEDULE     Level            *)
   151 (* ------------------------------------------------------------------ *)
   152 
   153 (* ---------------------------------------------------------------------- *)
   154              section   "Lemmas for ==>";
   155 (* ----------------------------------------------------------------------*)
   156 
   157 (* --------------------------------------------------------------------- *)
   158 (*    Lemma_2_1 :  tfilter(ex) and filter_act are commutative            *)
   159 (* --------------------------------------------------------------------- *)
   160 
   161 goalw thy [filter_act_def,Filter_ex2_def]
   162    "filter_act`(Filter_ex2 (asig_of A)`xs)=\
   163 \   Filter (%a. a:act A)`(filter_act`xs)";
   164 
   165 by (simp_tac (simpset() addsimps [MapFilter,o_def]) 1);
   166 qed"lemma_2_1a";
   167 
   168 
   169 (* --------------------------------------------------------------------- *)
   170 (*    Lemma_2_2 : State-projections do not affect filter_act             *)
   171 (* --------------------------------------------------------------------- *)
   172 
   173 goal thy 
   174    "filter_act`(ProjA2`xs) =filter_act`xs &\
   175 \   filter_act`(ProjB2`xs) =filter_act`xs";
   176 
   177 by (pair_induct_tac "xs" [] 1);
   178 qed"lemma_2_1b";
   179 
   180 
   181 (* --------------------------------------------------------------------- *)
   182 (*             Schedules of A||B have only  A- or B-actions              *)
   183 (* --------------------------------------------------------------------- *)
   184 
   185 (* FIX: very similar to lemma_1_1c, but it is not checking if every action element of 
   186    an ex is in A or B, but after projecting it onto the action schedule. Of course, this
   187    is the same proposition, but we cannot change this one, when then rather lemma_1_1c  *)
   188 
   189 goal thy "!s. is_exec_frag (A||B) (s,xs) \
   190 \  --> Forall (%x. x:act (A||B)) (filter_act`xs)";
   191 
   192 by (pair_induct_tac "xs" [is_exec_frag_def,Forall_def,sforall_def] 1);
   193 (* main case *)
   194 by (safe_tac set_cs);
   195 by (REPEAT (asm_full_simp_tac (simpset() addsimps trans_of_defs2 @ 
   196                                 [actions_asig_comp,asig_of_par]) 1));
   197 qed"sch_actions_in_AorB";
   198 
   199 
   200 (* --------------------------------------------------------------------------*)
   201                  section "Lemmas for <=="; 
   202 (* ---------------------------------------------------------------------------*)
   203 
   204 (*---------------------------------------------------------------------------
   205     Filtering actions out of mkex(sch,exA,exB) yields the oracle sch
   206                              structural induction
   207   --------------------------------------------------------------------------- *)
   208 
   209 goal thy "! exA exB s t. \
   210 \ Forall (%x. x:act (A||B)) sch  & \
   211 \ Filter (%a. a:act A)`sch << filter_act`exA &\
   212 \ Filter (%a. a:act B)`sch << filter_act`exB \
   213 \ --> filter_act`(snd (mkex A B sch (s,exA) (t,exB))) = sch";
   214 
   215 by (Seq_induct_tac "sch" [Filter_def,Forall_def,sforall_def,mkex_def] 1);
   216 
   217 (* main case *) 
   218 (* splitting into 4 cases according to a:A, a:B *)
   219 by (asm_full_simp_tac (simpset() setloop split_tac [expand_if]) 1);
   220 by (safe_tac set_cs);
   221 
   222 (* Case y:A, y:B *)
   223 by (Seq_case_simp_tac "exA" 1);
   224 (* Case exA=UU, Case exA=nil*)
   225 (* These UU and nil cases are the only places where the assumption filter A sch<<f_act exA 
   226    is used! --> to generate a contradiction using  ~a>>ss<< UU(nil), using theorems 
   227    Cons_not_less_UU and Cons_not_less_nil  *)
   228 by (Seq_case_simp_tac "exB" 1);
   229 (* Case exA=a>>x, exB=b>>y *)
   230 (* here it is important that Seq_case_simp_tac uses no !full!_simp_tac for the cons case, 
   231    as otherwise mkex_cons_3 would  not be rewritten without use of rotate_tac: then tactic 
   232    would not be generally applicable *)
   233 by (Asm_full_simp_tac 1);
   234 
   235 (* Case y:A, y~:B *)
   236 by (Seq_case_simp_tac "exB" 1);
   237 by (Asm_full_simp_tac 1);
   238 
   239 (* Case y~:A, y:B *)
   240 by (Seq_case_simp_tac "exA" 1);
   241 by (Asm_full_simp_tac 1);
   242 
   243 (* Case y~:A, y~:B *)
   244 by (asm_full_simp_tac (simpset() addsimps [asig_of_par,actions_asig_comp]) 1);
   245 qed"Mapfst_mkex_is_sch";
   246 
   247 
   248 (* generalizing the proof above to a tactic *)
   249 
   250 fun mkex_induct_tac sch exA exB = 
   251     EVERY1[Seq_induct_tac sch [Filter_def,Forall_def,sforall_def,mkex_def,stutter_def], 
   252            asm_full_simp_tac (simpset() setloop split_tac [expand_if]),
   253            SELECT_GOAL (safe_tac set_cs),
   254            Seq_case_simp_tac exA,
   255            Seq_case_simp_tac exB,
   256            Asm_full_simp_tac,
   257            Seq_case_simp_tac exB,
   258            Asm_full_simp_tac,
   259            Seq_case_simp_tac exA,
   260            Asm_full_simp_tac,
   261            asm_full_simp_tac (simpset() addsimps [asig_of_par,actions_asig_comp])
   262           ];
   263 
   264 
   265 
   266 (*---------------------------------------------------------------------------
   267                Projection of mkex(sch,exA,exB) onto A stutters on A
   268                              structural induction
   269   --------------------------------------------------------------------------- *)
   270 
   271 
   272 goal thy "! exA exB s t. \
   273 \ Forall (%x. x:act (A||B)) sch & \
   274 \ Filter (%a. a:act A)`sch << filter_act`exA &\
   275 \ Filter (%a. a:act B)`sch << filter_act`exB \
   276 \ --> stutter (asig_of A) (s,ProjA2`(snd (mkex A B sch (s,exA) (t,exB))))";
   277 
   278 by (mkex_induct_tac "sch" "exA" "exB");
   279 
   280 qed"stutterA_mkex";
   281 
   282 
   283 goal thy "!! sch.[|  \
   284 \ Forall (%x. x:act (A||B)) sch ; \
   285 \ Filter (%a. a:act A)`sch << filter_act`(snd exA) ;\
   286 \ Filter (%a. a:act B)`sch << filter_act`(snd exB) |] \
   287 \ ==> stutter (asig_of A) (ProjA (mkex A B sch exA exB))";
   288 
   289 by (cut_facts_tac [stutterA_mkex] 1);
   290 by (asm_full_simp_tac (simpset() addsimps [stutter_def,ProjA_def,mkex_def]) 1);
   291 by (REPEAT (etac allE 1));
   292 by (dtac mp 1);
   293 by (assume_tac 2);
   294 by (Asm_full_simp_tac 1);
   295 qed"stutter_mkex_on_A";
   296 
   297 
   298 (*---------------------------------------------------------------------------
   299                Projection of mkex(sch,exA,exB) onto B stutters on B
   300                              structural induction
   301   --------------------------------------------------------------------------- *)
   302 
   303 goal thy "! exA exB s t. \
   304 \ Forall (%x. x:act (A||B)) sch & \
   305 \ Filter (%a. a:act A)`sch << filter_act`exA &\
   306 \ Filter (%a. a:act B)`sch << filter_act`exB \
   307 \ --> stutter (asig_of B) (t,ProjB2`(snd (mkex A B sch (s,exA) (t,exB))))";
   308 
   309 by (mkex_induct_tac "sch" "exA" "exB");
   310 
   311 qed"stutterB_mkex";
   312 
   313 
   314 goal thy "!! sch.[|  \
   315 \ Forall (%x. x:act (A||B)) sch ; \
   316 \ Filter (%a. a:act A)`sch << filter_act`(snd exA) ;\
   317 \ Filter (%a. a:act B)`sch << filter_act`(snd exB) |] \
   318 \ ==> stutter (asig_of B) (ProjB (mkex A B sch exA exB))";
   319 
   320 by (cut_facts_tac [stutterB_mkex] 1);
   321 by (asm_full_simp_tac (simpset() addsimps [stutter_def,ProjB_def,mkex_def]) 1);
   322 by (REPEAT (etac allE 1));
   323 by (dtac mp 1);
   324 by (assume_tac 2);
   325 by (Asm_full_simp_tac 1);
   326 qed"stutter_mkex_on_B";
   327 
   328 
   329 (*---------------------------------------------------------------------------
   330      Filter of mkex(sch,exA,exB) to A after projection onto A is exA 
   331         --  using zip`(proj1`exA)`(proj2`exA) instead of exA    --
   332         --           because of admissibility problems          --
   333                              structural induction
   334   --------------------------------------------------------------------------- *)
   335 
   336 goal thy "! exA exB s t. \
   337 \ Forall (%x. x:act (A||B)) sch & \
   338 \ Filter (%a. a:act A)`sch << filter_act`exA  &\
   339 \ Filter (%a. a:act B)`sch << filter_act`exB \
   340 \ --> Filter_ex2 (asig_of A)`(ProjA2`(snd (mkex A B sch (s,exA) (t,exB)))) =   \
   341 \     Zip`(Filter (%a. a:act A)`sch)`(Map snd`exA)";
   342 
   343 by (mkex_induct_tac "sch" "exA" "exB");
   344 
   345 qed"filter_mkex_is_exA_tmp";
   346 
   347 (*---------------------------------------------------------------------------
   348                       zip`(proj1`y)`(proj2`y) = y   (using the lift operations)
   349                     lemma for admissibility problems         
   350   --------------------------------------------------------------------------- *)
   351 
   352 goal thy  "Zip`(Map fst`y)`(Map snd`y) = y";
   353 by (Seq_induct_tac "y" [] 1);
   354 qed"Zip_Map_fst_snd";
   355 
   356 
   357 (*---------------------------------------------------------------------------
   358       filter A`sch = proj1`ex   -->  zip`(filter A`sch)`(proj2`ex) = ex 
   359          lemma for eliminating non admissible equations in assumptions      
   360   --------------------------------------------------------------------------- *)
   361 
   362 (* Versuich 
   363 goal thy "(y~= nil & Map fst`x <<y) --> x= Zip`y`(Map snd`x)";
   364 by (Seq_induct_tac "x" [] 1);
   365 by (Seq_case_simp_tac "y" 2);
   366 by (pair_tac "a" 1);
   367 by Auto_tac;
   368 
   369 *)
   370 
   371 goal thy "!! sch ex. \
   372 \ Filter (%a. a:act AB)`sch = filter_act`ex  \
   373 \ ==> ex = Zip`(Filter (%a. a:act AB)`sch)`(Map snd`ex)";
   374 by (asm_full_simp_tac (simpset() addsimps [filter_act_def]) 1);
   375 by (rtac (Zip_Map_fst_snd RS sym) 1);
   376 qed"trick_against_eq_in_ass";
   377 
   378 (*---------------------------------------------------------------------------
   379      Filter of mkex(sch,exA,exB) to A after projection onto A is exA 
   380                        using the above trick
   381   --------------------------------------------------------------------------- *)
   382 
   383 
   384 goal thy "!!sch exA exB.\
   385 \ [| Forall (%a. a:act (A||B)) sch ; \
   386 \ Filter (%a. a:act A)`sch = filter_act`(snd exA)  ;\
   387 \ Filter (%a. a:act B)`sch = filter_act`(snd exB) |]\
   388 \ ==> Filter_ex (asig_of A) (ProjA (mkex A B sch exA exB)) = exA";
   389 by (asm_full_simp_tac (simpset() addsimps [ProjA_def,Filter_ex_def]) 1);
   390 by (pair_tac "exA" 1);
   391 by (pair_tac "exB" 1);
   392 by (rtac conjI 1);
   393 by (simp_tac (simpset() addsimps [mkex_def]) 1);
   394 by (stac trick_against_eq_in_ass 1);
   395 back();
   396 by (assume_tac 1);
   397 by (asm_full_simp_tac (simpset() addsimps [filter_mkex_is_exA_tmp]) 1);
   398 qed"filter_mkex_is_exA";
   399  
   400 
   401 (*---------------------------------------------------------------------------
   402      Filter of mkex(sch,exA,exB) to B after projection onto B is exB 
   403         --  using zip`(proj1`exB)`(proj2`exB) instead of exB    --
   404         --           because of admissibility problems          --
   405                              structural induction
   406   --------------------------------------------------------------------------- *)
   407 
   408 
   409 goal thy "! exA exB s t. \
   410 \ Forall (%x. x:act (A||B)) sch & \
   411 \ Filter (%a. a:act A)`sch << filter_act`exA  &\
   412 \ Filter (%a. a:act B)`sch << filter_act`exB \
   413 \ --> Filter_ex2 (asig_of B)`(ProjB2`(snd (mkex A B sch (s,exA) (t,exB)))) =   \
   414 \     Zip`(Filter (%a. a:act B)`sch)`(Map snd`exB)";
   415 
   416 (* notice necessary change of arguments exA and exB *)
   417 by (mkex_induct_tac "sch" "exB" "exA");
   418 
   419 qed"filter_mkex_is_exB_tmp";
   420 
   421 
   422 (*---------------------------------------------------------------------------
   423      Filter of mkex(sch,exA,exB) to A after projection onto B is exB 
   424                        using the above trick
   425   --------------------------------------------------------------------------- *)
   426 
   427 
   428 goal thy "!!sch exA exB.\
   429 \ [| Forall (%a. a:act (A||B)) sch ; \
   430 \ Filter (%a. a:act A)`sch = filter_act`(snd exA)  ;\
   431 \ Filter (%a. a:act B)`sch = filter_act`(snd exB) |]\
   432 \ ==> Filter_ex (asig_of B) (ProjB (mkex A B sch exA exB)) = exB";
   433 by (asm_full_simp_tac (simpset() addsimps [ProjB_def,Filter_ex_def]) 1);
   434 by (pair_tac "exA" 1);
   435 by (pair_tac "exB" 1);
   436 by (rtac conjI 1);
   437 by (simp_tac (simpset() addsimps [mkex_def]) 1);
   438 by (stac trick_against_eq_in_ass 1);
   439 back();
   440 by (assume_tac 1);
   441 by (asm_full_simp_tac (simpset() addsimps [filter_mkex_is_exB_tmp]) 1);
   442 qed"filter_mkex_is_exB";
   443 
   444 (* --------------------------------------------------------------------- *)
   445 (*                    mkex has only  A- or B-actions                    *)
   446 (* --------------------------------------------------------------------- *)
   447 
   448 
   449 goal thy "!s t exA exB. \
   450 \ Forall (%x. x : act (A || B)) sch &\
   451 \ Filter (%a. a:act A)`sch << filter_act`exA  &\
   452 \ Filter (%a. a:act B)`sch << filter_act`exB \
   453 \  --> Forall (%x. fst x : act (A ||B))   \
   454 \        (snd (mkex A B sch (s,exA) (t,exB)))";
   455 
   456 by (mkex_induct_tac "sch" "exA" "exB");
   457 
   458 qed"mkex_actions_in_AorB";
   459 
   460 
   461 (* ------------------------------------------------------------------ *)
   462 (*           COMPOSITIONALITY   on    SCHEDULE      Level             *)
   463 (*                          Main Theorem                              *)
   464 (* ------------------------------------------------------------------ *)
   465 
   466 goal thy  
   467 "sch : schedules (A||B) = \
   468 \ (Filter (%a. a:act A)`sch : schedules A &\
   469 \  Filter (%a. a:act B)`sch : schedules B &\
   470 \  Forall (%x. x:act (A||B)) sch)";
   471 
   472 by (simp_tac (simpset() addsimps [schedules_def, has_schedule_def]) 1);
   473 by (safe_tac set_cs); 
   474 (* ==> *) 
   475 by (res_inst_tac [("x","Filter_ex (asig_of A) (ProjA ex)")] bexI 1);
   476 by (asm_full_simp_tac (simpset() addsimps [compositionality_ex]) 2);
   477 by (simp_tac (simpset() addsimps [Filter_ex_def,ProjA_def,
   478                                  lemma_2_1a,lemma_2_1b]) 1); 
   479 by (res_inst_tac [("x","Filter_ex (asig_of B) (ProjB ex)")] bexI 1);
   480 by (asm_full_simp_tac (simpset() addsimps [compositionality_ex]) 2);
   481 by (simp_tac (simpset() addsimps [Filter_ex_def,ProjB_def,
   482                                  lemma_2_1a,lemma_2_1b]) 1);
   483 by (asm_full_simp_tac (simpset() addsimps [executions_def]) 1);
   484 by (pair_tac "ex" 1);
   485 by (etac conjE 1);
   486 by (asm_full_simp_tac (simpset() addsimps [sch_actions_in_AorB]) 1);
   487 
   488 (* <== *)
   489 
   490 (* mkex is exactly the construction of exA||B out of exA, exB, and the oracle sch,
   491    we need here *)
   492 ren "exA exB" 1;
   493 by (res_inst_tac [("x","mkex A B sch exA exB")] bexI 1);
   494 (* mkex actions are just the oracle *)
   495 by (pair_tac "exA" 1);
   496 by (pair_tac "exB" 1);
   497 by (asm_full_simp_tac (simpset() addsimps [Mapfst_mkex_is_sch]) 1);
   498 
   499 (* mkex is an execution -- use compositionality on ex-level *)
   500 by (asm_full_simp_tac (simpset() addsimps [compositionality_ex]) 1);
   501 by (asm_full_simp_tac (simpset() addsimps 
   502                  [stutter_mkex_on_A, stutter_mkex_on_B,
   503                   filter_mkex_is_exB,filter_mkex_is_exA]) 1);
   504 by (pair_tac "exA" 1);
   505 by (pair_tac "exB" 1);
   506 by (asm_full_simp_tac (simpset() addsimps [mkex_actions_in_AorB]) 1);
   507 qed"compositionality_sch";
   508 
   509 
   510 (* ------------------------------------------------------------------ *)
   511 (*           COMPOSITIONALITY   on    SCHEDULE      Level             *)
   512 (*                            For Modules                             *)
   513 (* ------------------------------------------------------------------ *)
   514 
   515 goalw thy [Scheds_def,par_scheds_def]
   516 
   517 "Scheds (A||B) = par_scheds (Scheds A) (Scheds B)";
   518 
   519 by (asm_full_simp_tac (simpset() addsimps [asig_of_par]) 1);
   520 by (rtac set_ext 1);
   521 by (asm_full_simp_tac (simpset() addsimps [compositionality_sch,actions_of_par]) 1);
   522 qed"compositionality_sch_modules";
   523 
   524 
   525 Delsimps compoex_simps;
   526 Delsimps composch_simps;