src/HOLCF/IOA/meta_theory/CompoTraces.ML
author nipkow
Tue Jan 09 15:36:30 2001 +0100 (2001-01-09)
changeset 10835 f4745d77e620
parent 10230 5eb935d6cc69
child 11655 923e4d0d36d5
permissions -rw-r--r--
` -> $
     1 (*  Title:      HOLCF/IOA/meta_theory/CompoTraces.ML
     2     ID:		$Id$
     3     Author:     Olaf M"uller
     4     Copyright   1996  TU Muenchen
     5  
     6 Compositionality on Trace level.
     7 *) 
     8 
     9 simpset_ref () := simpset() setmksym (K None);
    10 
    11 (* ---------------------------------------------------------------- *)
    12                    section "mksch rewrite rules";
    13 (* ---------------------------------------------------------------- *)
    14 
    15 
    16 
    17 
    18 bind_thm ("mksch_unfold", fix_prover2 thy mksch_def 
    19 "mksch A B = (LAM tr schA schB. case tr of \
    20 \       nil => nil\
    21 \    | x##xs => \
    22 \      (case x of  \ 
    23 \        Undef => UU  \
    24 \      | Def y => \
    25 \         (if y:act A then \
    26 \             (if y:act B then \ 
    27 \                   ((Takewhile (%a. a:int A)$schA) \
    28 \                         @@(Takewhile (%a. a:int B)$schB) \
    29 \                              @@(y>>(mksch A B$xs   \
    30 \                                       $(TL$(Dropwhile (%a. a:int A)$schA))  \
    31 \                                       $(TL$(Dropwhile (%a. a:int B)$schB))  \
    32 \                    )))   \
    33 \              else  \
    34 \                 ((Takewhile (%a. a:int A)$schA)  \
    35 \                      @@ (y>>(mksch A B$xs  \
    36 \                              $(TL$(Dropwhile (%a. a:int A)$schA))  \
    37 \                              $schB)))  \
    38 \              )   \
    39 \          else    \
    40 \             (if y:act B then  \ 
    41 \                 ((Takewhile (%a. a:int B)$schB)  \
    42 \                       @@ (y>>(mksch A B$xs   \
    43 \                              $schA   \
    44 \                              $(TL$(Dropwhile (%a. a:int B)$schB))  \
    45 \                              )))  \
    46 \             else  \
    47 \               UU  \
    48 \             )  \
    49 \         )  \
    50 \       ))");
    51 
    52 
    53 Goal "mksch A B$UU$schA$schB = UU";
    54 by (stac mksch_unfold 1);
    55 by (Simp_tac 1);
    56 qed"mksch_UU";
    57 
    58 Goal "mksch A B$nil$schA$schB = nil";
    59 by (stac mksch_unfold 1);
    60 by (Simp_tac 1);
    61 qed"mksch_nil";
    62 
    63 Goal "[|x:act A;x~:act B|]  \
    64 \   ==> mksch A B$(x>>tr)$schA$schB = \
    65 \         (Takewhile (%a. a:int A)$schA) \
    66 \         @@ (x>>(mksch A B$tr$(TL$(Dropwhile (%a. a:int A)$schA)) \
    67 \                             $schB))";
    68 by (rtac trans 1);
    69 by (stac mksch_unfold 1);
    70 by (asm_full_simp_tac (simpset() addsimps [Consq_def,If_and_if]) 1);
    71 by (simp_tac (simpset() addsimps [Consq_def]) 1);
    72 qed"mksch_cons1";
    73 
    74 Goal "[|x~:act A;x:act B|] \
    75 \   ==> mksch A B$(x>>tr)$schA$schB = \
    76 \        (Takewhile (%a. a:int B)$schB)  \
    77 \         @@ (x>>(mksch A B$tr$schA$(TL$(Dropwhile (%a. a:int B)$schB))  \
    78 \                            ))";
    79 by (rtac trans 1);
    80 by (stac mksch_unfold 1);
    81 by (asm_full_simp_tac (simpset() addsimps [Consq_def,If_and_if]) 1);
    82 by (simp_tac (simpset() addsimps [Consq_def]) 1);
    83 qed"mksch_cons2";
    84 
    85 Goal "[|x:act A;x:act B|] \
    86 \   ==> mksch A B$(x>>tr)$schA$schB = \
    87 \            (Takewhile (%a. a:int A)$schA) \
    88 \         @@ ((Takewhile (%a. a:int B)$schB)  \
    89 \         @@ (x>>(mksch A B$tr$(TL$(Dropwhile (%a. a:int A)$schA)) \
    90 \                            $(TL$(Dropwhile (%a. a:int B)$schB))))  \
    91 \             )";
    92 by (rtac trans 1);
    93 by (stac mksch_unfold 1);
    94 by (asm_full_simp_tac (simpset() addsimps [Consq_def,If_and_if]) 1);
    95 by (simp_tac (simpset() addsimps [Consq_def]) 1);
    96 qed"mksch_cons3";
    97 
    98 val compotr_simps =[mksch_UU,mksch_nil, mksch_cons1,mksch_cons2,mksch_cons3];
    99 
   100 Addsimps compotr_simps;
   101 
   102 
   103 (* ------------------------------------------------------------------ *)
   104 (*                      The following lemmata aim for                 *)
   105 (*               COMPOSITIONALITY   on    TRACE     Level             *)
   106 (* ------------------------------------------------------------------ *)
   107 
   108 
   109 (* ---------------------------------------------------------------------------- *)
   110                       section"Lemmata for ==>";                      
   111 (* ---------------------------------------------------------------------------- *)
   112 
   113 (* Consequence out of ext1_ext2_is_not_act1(2), which in turn are consequences out of 
   114    the compatibility of IOA, in particular out of the condition that internals are 
   115    really hidden. *)
   116 
   117 Goal "(eB & ~eA --> ~A) -->       \
   118 \         (A & (eA | eB)) = (eA & A)";
   119 by (Fast_tac 1);
   120 qed"compatibility_consequence1";
   121 
   122 
   123 (* very similar to above, only the commutativity of | is used to make a slight change *)
   124 
   125 Goal "(eB & ~eA --> ~A) -->       \
   126 \         (A & (eB | eA)) = (eA & A)";
   127 by (Fast_tac 1);
   128 qed"compatibility_consequence2";
   129 
   130 
   131 (* ---------------------------------------------------------------------------- *)
   132                       section"Lemmata for <==";                      
   133 (* ---------------------------------------------------------------------------- *)
   134 
   135 
   136 (* Lemma for substitution of looping assumption in another specific assumption *) 
   137 val [p1,p2] = goal thy "[| f << (g x) ; x=(h x) |] ==> f << g (h x)";
   138 by (cut_facts_tac [p1] 1);
   139 by (etac (p2 RS subst) 1);
   140 qed"subst_lemma1";
   141 
   142 (* Lemma for substitution of looping assumption in another specific assumption *) 
   143 val [p1,p2] = goal thy "[| (f x) = y >> g; x=(h x) |] ==> (f (h x)) = y >> g";
   144 by (cut_facts_tac [p1] 1);
   145 by (etac (p2 RS subst) 1);
   146 qed"subst_lemma2";
   147 
   148 
   149 Goal "!!A B. compatible A B ==> \
   150 \   ! schA schB. Forall (%x. x:act (A||B)) tr \
   151 \   --> Forall (%x. x:act (A||B)) (mksch A B$tr$schA$schB)";
   152 by (Seq_induct_tac "tr" [Forall_def,sforall_def,mksch_def] 1); 
   153 by (safe_tac set_cs);
   154 by (asm_full_simp_tac (simpset() addsimps [actions_of_par]) 1);
   155 by (case_tac "a:act A" 1);
   156 by (case_tac "a:act B" 1);
   157 (* a:A, a:B *)
   158 by (Asm_full_simp_tac 1);
   159 by (rtac (Forall_Conc_impl RS mp) 1);
   160 by (asm_full_simp_tac (simpset() addsimps [ForallPTakewhileQ,intA_is_not_actB,int_is_act]) 1);
   161 by (rtac (Forall_Conc_impl RS mp) 1);
   162 by (asm_full_simp_tac (simpset() addsimps [ForallPTakewhileQ,intA_is_not_actB,int_is_act]) 1);
   163 (* a:A,a~:B *)
   164 by (Asm_full_simp_tac 1);
   165 by (rtac (Forall_Conc_impl RS mp) 1);
   166 by (asm_full_simp_tac (simpset() addsimps [ForallPTakewhileQ,intA_is_not_actB,int_is_act]) 1);
   167 by (case_tac "a:act B" 1);
   168 (* a~:A, a:B *)
   169 by (Asm_full_simp_tac 1);
   170 by (rtac (Forall_Conc_impl RS mp) 1);
   171 by (asm_full_simp_tac (simpset() addsimps [ForallPTakewhileQ,intA_is_not_actB,int_is_act]) 1);
   172 (* a~:A,a~:B *)
   173 by Auto_tac;
   174 qed_spec_mp"ForallAorB_mksch";
   175 
   176 Goal "!!A B. compatible B A  ==> \
   177 \   ! schA schB.  (Forall (%x. x:act B & x~:act A) tr \
   178 \   --> Forall (%x. x:act B & x~:act A) (mksch A B$tr$schA$schB))";
   179 
   180 by (Seq_induct_tac "tr" [Forall_def,sforall_def,mksch_def] 1);
   181 by (safe_tac set_cs);
   182 by (rtac (Forall_Conc_impl RS mp) 1);
   183 by (asm_full_simp_tac (simpset() addsimps [ForallPTakewhileQ,
   184                             intA_is_not_actB,int_is_act]) 1);
   185 qed_spec_mp "ForallBnAmksch";
   186 
   187 Goal "!!A B. compatible A B ==> \
   188 \   ! schA schB.  (Forall (%x. x:act A & x~:act B) tr \
   189 \   --> Forall (%x. x:act A & x~:act B) (mksch A B$tr$schA$schB))";
   190 
   191 by (Seq_induct_tac "tr" [Forall_def,sforall_def,mksch_def] 1);
   192 by (safe_tac set_cs);
   193 by (Asm_full_simp_tac 1);
   194 by (rtac (Forall_Conc_impl RS mp) 1);
   195 by (asm_full_simp_tac (simpset() addsimps [ForallPTakewhileQ,
   196                        intA_is_not_actB,int_is_act]) 1);
   197 qed_spec_mp"ForallAnBmksch";
   198 
   199 (* safe-tac makes too many case distinctions with this lemma in the next proof *)
   200 Delsimps [FiniteConc];
   201 
   202 Goal "[| Finite tr; is_asig(asig_of A); is_asig(asig_of B) |] ==> \
   203 \   ! x y. Forall (%x. x:act A) x & Forall (%x. x:act B) y & \
   204 \          Filter (%a. a:ext A)$x = Filter (%a. a:act A)$tr & \
   205 \          Filter (%a. a:ext B)$y = Filter (%a. a:act B)$tr &\
   206 \          Forall (%x. x:ext (A||B)) tr \
   207 \          --> Finite (mksch A B$tr$x$y)";
   208 
   209 by (etac Seq_Finite_ind  1);
   210 by (Asm_full_simp_tac 1);
   211 (* main case *)
   212 by (Asm_full_simp_tac 1);
   213 by (safe_tac set_cs);
   214 
   215 (* a: act A; a: act B *)
   216 by (forward_tac [sym RS antisym_less_inverse RS conjunct1 RS divide_Seq] 1);
   217 by (forward_tac [sym RS antisym_less_inverse RS conjunct1 RS divide_Seq] 1);
   218 back();
   219 by (REPEAT (etac conjE 1));
   220 (* Finite (tw iA x) and Finite (tw iB y) *)
   221 by (asm_full_simp_tac (simpset() addsimps 
   222           [not_ext_is_int_or_not_act,FiniteConc]) 1);
   223 (* now for conclusion IH applicable, but assumptions have to be transformed *)
   224 by (dres_inst_tac [("x","x"),
   225                    ("g","Filter (%a. a:act A)$s")] subst_lemma2 1);
   226 by (assume_tac 1);
   227 by (dres_inst_tac [("x","y"),
   228                    ("g","Filter (%a. a:act B)$s")] subst_lemma2 1);
   229 by (assume_tac 1);
   230 (* IH *)
   231 by (asm_full_simp_tac (simpset()
   232         addsimps [not_ext_is_int_or_not_act,ForallTL,ForallDropwhile]) 1);
   233 
   234 (* a: act B; a~: act A *)
   235 by (forward_tac [sym RS antisym_less_inverse RS conjunct1 RS divide_Seq] 1);
   236 
   237 by (REPEAT (etac conjE 1));
   238 (* Finite (tw iB y) *)
   239 by (asm_full_simp_tac (simpset() addsimps 
   240           [not_ext_is_int_or_not_act,FiniteConc]) 1);
   241 (* now for conclusion IH applicable, but assumptions have to be transformed *)
   242 by (dres_inst_tac [("x","y"),
   243                    ("g","Filter (%a. a:act B)$s")] subst_lemma2 1);
   244 by (assume_tac 1);
   245 (* IH *)
   246 by (asm_full_simp_tac (simpset()
   247        addsimps [not_ext_is_int_or_not_act,ForallTL,ForallDropwhile]) 1);
   248 
   249 (* a~: act B; a: act A *)
   250 by (forward_tac [sym RS antisym_less_inverse RS conjunct1 RS divide_Seq] 1);
   251 
   252 by (REPEAT (etac conjE 1));
   253 (* Finite (tw iA x) *)
   254 by (asm_full_simp_tac (simpset() addsimps 
   255           [not_ext_is_int_or_not_act,FiniteConc]) 1);
   256 (* now for conclusion IH applicable, but assumptions have to be transformed *)
   257 by (dres_inst_tac [("x","x"),
   258                    ("g","Filter (%a. a:act A)$s")] subst_lemma2 1);
   259 by (assume_tac 1);
   260 (* IH *)
   261 by (asm_full_simp_tac (simpset()
   262        addsimps [not_ext_is_int_or_not_act,ForallTL,ForallDropwhile]) 1);
   263 
   264 (* a~: act B; a~: act A *)
   265 by (fast_tac (claset() addSIs [ext_is_act] 
   266                       addss (simpset() addsimps [externals_of_par]) ) 1);
   267 qed_spec_mp"FiniteL_mksch";
   268 
   269 Addsimps [FiniteConc];
   270 
   271 
   272 (* otherwise subst_lemma2 does not fit exactly, just to avoid a subst_lemma3 *)
   273 Delsimps [FilterConc]; 
   274 
   275 Goal " [| Finite bs; is_asig(asig_of A); is_asig(asig_of B);compatible A B|] ==>  \
   276 \! y. Forall (%x. x:act B) y & Forall (%x. x:act B & x~:act A) bs &\
   277 \    Filter (%a. a:ext B)$y = Filter (%a. a:act B)$(bs @@ z) \
   278 \    --> (? y1 y2.  (mksch A B$(bs @@ z)$x$y) = (y1 @@ (mksch A B$z$x$y2)) & \
   279 \                   Forall (%x. x:act B & x~:act A) y1 & \
   280 \                   Finite y1 & y = (y1 @@ y2) & \
   281 \                   Filter (%a. a:ext B)$y1 = bs)";
   282 by (forw_inst_tac [("A1","A")] (compat_commute RS iffD1) 1);
   283 by (etac Seq_Finite_ind  1);
   284 by (REPEAT (rtac allI 1));
   285 by (rtac impI 1);
   286 by (res_inst_tac [("x","nil")] exI 1);
   287 by (res_inst_tac [("x","y")] exI 1);
   288 by (Asm_full_simp_tac 1);
   289 (* main case *)
   290 by (REPEAT (rtac allI 1));
   291 by (rtac impI 1);
   292 by (Asm_full_simp_tac 1);
   293 by (REPEAT (etac conjE 1));
   294 by (Asm_full_simp_tac 1);
   295 (* divide_Seq on s *)
   296 by (forward_tac [sym RS antisym_less_inverse RS conjunct1 RS divide_Seq] 1);
   297 by (REPEAT (etac conjE 1));
   298 (* transform assumption f eB y = f B (s@z) *)
   299 by (dres_inst_tac [("x","y"),
   300                    ("g","Filter (%a. a:act B)$(s@@z)")] subst_lemma2 1);
   301 by (assume_tac 1);
   302 Addsimps [FilterConc]; 
   303 by (asm_full_simp_tac (simpset() addsimps [not_ext_is_int_or_not_act]) 1);
   304 (* apply IH *)
   305 by (eres_inst_tac [("x","TL$(Dropwhile (%a. a:int B)$y)")] allE 1);
   306 by (asm_full_simp_tac (simpset() addsimps [ForallTL,ForallDropwhile])1);
   307 by (REPEAT (etac exE 1));
   308 by (REPEAT (etac conjE 1));
   309 by (Asm_full_simp_tac 1); 
   310 (* for replacing IH in conclusion *)
   311 by (rotate_tac ~2 1); 
   312 by (Asm_full_simp_tac 1); 
   313 (* instantiate y1a and y2a *)
   314 by (res_inst_tac [("x","Takewhile (%a. a:int B)$y @@ a>>y1")] exI 1);
   315 by (res_inst_tac [("x","y2")] exI 1);
   316 (* elminate all obligations up to two depending on Conc_assoc *)
   317 by (asm_full_simp_tac (simpset() addsimps [ForallPTakewhileQ, intA_is_not_actB,
   318              int_is_act,int_is_not_ext]) 1); 
   319 by (simp_tac (simpset() addsimps [Conc_assoc]) 1); 
   320 qed_spec_mp "reduceA_mksch1";
   321 
   322 bind_thm("reduceA_mksch",conjI RSN (6,conjI RSN (5,reduceA_mksch1)));
   323 
   324 
   325 (* otherwise subst_lemma2 does not fit exactly, just to avoid a subst_lemma3 *)
   326 Delsimps [FilterConc]; 
   327 
   328 
   329 Goal " [| Finite as; is_asig(asig_of A); is_asig(asig_of B);compatible A B|] ==>  \
   330 \! x. Forall (%x. x:act A) x & Forall (%x. x:act A & x~:act B) as &\
   331 \    Filter (%a. a:ext A)$x = Filter (%a. a:act A)$(as @@ z) \
   332 \    --> (? x1 x2.  (mksch A B$(as @@ z)$x$y) = (x1 @@ (mksch A B$z$x2$y)) & \
   333 \                   Forall (%x. x:act A & x~:act B) x1 & \
   334 \                   Finite x1 & x = (x1 @@ x2) & \
   335 \                   Filter (%a. a:ext A)$x1 = as)";
   336 by (forw_inst_tac [("A1","A")] (compat_commute RS iffD1) 1);
   337 by (etac Seq_Finite_ind  1);
   338 by (REPEAT (rtac allI 1));
   339 by (rtac impI 1);
   340 by (res_inst_tac [("x","nil")] exI 1);
   341 by (res_inst_tac [("x","x")] exI 1);
   342 by (Asm_full_simp_tac 1);
   343 (* main case *)
   344 by (REPEAT (rtac allI 1));
   345 by (rtac impI 1);
   346 by (Asm_full_simp_tac 1);
   347 by (REPEAT (etac conjE 1));
   348 by (Asm_full_simp_tac 1);
   349 (* divide_Seq on s *)
   350 by (forward_tac [sym RS antisym_less_inverse RS conjunct1 RS divide_Seq] 1);
   351 by (REPEAT (etac conjE 1));
   352 (* transform assumption f eA x = f A (s@z) *)
   353 by (dres_inst_tac [("x","x"),
   354                    ("g","Filter (%a. a:act A)$(s@@z)")] subst_lemma2 1);
   355 by (assume_tac 1);
   356 Addsimps [FilterConc]; 
   357 by (asm_full_simp_tac (simpset() addsimps [not_ext_is_int_or_not_act]) 1);
   358 (* apply IH *)
   359 by (eres_inst_tac [("x","TL$(Dropwhile (%a. a:int A)$x)")] allE 1);
   360 by (asm_full_simp_tac (simpset() addsimps [ForallTL,ForallDropwhile])1);
   361 by (REPEAT (etac exE 1));
   362 by (REPEAT (etac conjE 1));
   363 by (Asm_full_simp_tac 1); 
   364 (* for replacing IH in conclusion *)
   365 by (rotate_tac ~2 1); 
   366 by (Asm_full_simp_tac 1); 
   367 (* instantiate y1a and y2a *)
   368 by (res_inst_tac [("x","Takewhile (%a. a:int A)$x @@ a>>x1")] exI 1);
   369 by (res_inst_tac [("x","x2")] exI 1);
   370 (* elminate all obligations up to two depending on Conc_assoc *)
   371 by (asm_full_simp_tac (simpset() addsimps [ForallPTakewhileQ, intA_is_not_actB,
   372              int_is_act,int_is_not_ext]) 1); 
   373 by (simp_tac (simpset() addsimps [Conc_assoc]) 1); 
   374 qed_spec_mp"reduceB_mksch1";
   375 
   376 bind_thm("reduceB_mksch",conjI RSN (6,conjI RSN (5,reduceB_mksch1)));
   377 
   378 
   379 (*
   380 
   381 
   382 Goal "Finite y ==> ! z tr. Forall (%a.a:ext (A||B)) tr & \
   383 \                             y = z @@ mksch A B$tr$a$b\
   384 \                             --> Finite tr";
   385 by (etac Seq_Finite_ind  1);
   386 by Auto_tac;
   387 by (Seq_case_simp_tac "tr" 1);
   388 (* tr = UU *)
   389 by (asm_full_simp_tac (simpset() addsimps [nil_is_Conc]) 1);
   390 (* tr = nil *)
   391 by Auto_tac;
   392 (* tr = Conc *)
   393 ren "s ss" 1;
   394 
   395 by (case_tac "s:act A" 1);
   396 by (case_tac "s:act B" 1);
   397 by (rotate_tac ~2 1);
   398 by (rotate_tac ~2 2);
   399 by (asm_full_simp_tac (simpset() addsimps [nil_is_Conc,nil_is_Conc2]) 1);
   400 by (asm_full_simp_tac (simpset() addsimps [nil_is_Conc,nil_is_Conc2]) 1);
   401 by (case_tac "s:act B" 1);
   402 by (rotate_tac ~2 1);
   403 by (asm_full_simp_tac (simpset() addsimps [nil_is_Conc,nil_is_Conc2]) 1);
   404 by (fast_tac (claset() addSIs [ext_is_act] 
   405                       addss (simpset() addsimps [externals_of_par]) ) 1);
   406 (* main case *)
   407 by (Seq_case_simp_tac "tr" 1);
   408 (* tr = UU *)
   409 by (asm_full_simp_tac (simpset() addsimps [Conc_Conc_eq]) 1);
   410 by Auto_tac;
   411 (* tr = nil ok *)
   412 (* tr = Conc *)
   413 by (Seq_case_simp_tac "z" 1);
   414 (* z = UU ok *)
   415 (* z = nil *)
   416 
   417 (* z= Cons *)
   418 
   419 
   420 by (case_tac "aaa:act A" 2);
   421 by (case_tac "aaa:act B" 2);
   422 by (rotate_tac ~2 2);
   423 by (rotate_tac ~2 3);
   424 by (asm_full_simp_tac (HOL_basic_ss addsimps [mksch_cons3]) 2);
   425 by (eres_inst_tac [("x","sb@@Takewhile (%a. a: int A)$a @@ Takewhile (%a. a:int B)$b@@(aaa>>nil)")] allE 2);
   426 by (eres_inst_tac [("x","sa")] allE 2);
   427 by (asm_full_simp_tac (simpset() addsimps [Conc_assoc])2);
   428 
   429 
   430 
   431 by (eres_inst_tac [("x","sa")] allE 1);
   432 by (Asm_full_simp_tac 1);
   433 by (case_tac "aaa:act A" 1);
   434 by (case_tac "aaa:act B" 1);
   435 by (rotate_tac ~2 1);
   436 by (rotate_tac ~2 2);
   437 by (asm_full_simp_tac (simpset() addsimps [Conc_Conc_eq]) 1);
   438 
   439 
   440 
   441 Goal "(x>>xs = y @@ z) = ((y=nil & x>>xs=z) | (? ys. y=x>>ys & xs=ys@@z))";
   442 by (Seq_case_simp_tac "y" 1);
   443 by Auto_tac;
   444 qed"Conc_Conc_eq";
   445 
   446 Goal "!! (y::'a Seq).Finite y ==> ~ y= x@@UU";
   447 by (etac Seq_Finite_ind 1);
   448 by (Seq_case_simp_tac "x" 1);
   449 by (Seq_case_simp_tac "x" 1);
   450 by Auto_tac;
   451 qed"FiniteConcUU1";
   452 
   453 Goal "~ Finite ((x::'a Seq)@@UU)";
   454 by (auto_tac (claset() addDs [FiniteConcUU1], simpset()));
   455 qed"FiniteConcUU";
   456 
   457 finiteR_mksch
   458   "Finite (mksch A B$tr$x$y) --> Finite tr"
   459 *)
   460 
   461 
   462  
   463 (*------------------------------------------------------------------------------------- *)
   464  section"Filtering external actions out of mksch(tr,schA,schB) yields the oracle tr";
   465 (*                             structural induction
   466   ------------------------------------------------------------------------------------- *)
   467 
   468 Goal 
   469 "!! A B. [| compatible A B; compatible B A;\
   470 \           is_asig(asig_of A); is_asig(asig_of B) |] ==> \
   471 \ ! schA schB. Forall (%x. x:act A) schA & Forall (%x. x:act B) schB & \
   472 \ Forall (%x. x:ext (A||B)) tr & \
   473 \ Filter (%a. a:act A)$tr << Filter (%a. a:ext A)$schA &\
   474 \ Filter (%a. a:act B)$tr << Filter (%a. a:ext B)$schB  \
   475 \ --> Filter (%a. a:ext (A||B))$(mksch A B$tr$schA$schB) = tr";
   476 
   477 by (Seq_induct_tac "tr" [Forall_def,sforall_def,mksch_def] 1);
   478 
   479 (* main case *) 
   480 (* splitting into 4 cases according to a:A, a:B *)
   481 by (Asm_full_simp_tac 1);
   482 by (safe_tac set_cs);
   483 
   484 (* Case a:A, a:B *)
   485 by (ftac divide_Seq 1);
   486 by (ftac divide_Seq 1);
   487 back();
   488 by (REPEAT (etac conjE 1));
   489 (* filtering internals of A in schA and of B in schB is nil *)
   490 by (asm_full_simp_tac (simpset() addsimps 
   491           [not_ext_is_int_or_not_act,
   492            externals_of_par, intA_is_not_extB,int_is_not_ext]) 1);
   493 (* conclusion of IH ok, but assumptions of IH have to be transformed *)
   494 by (dres_inst_tac [("x","schA")] subst_lemma1 1);
   495 by (assume_tac 1);
   496 by (dres_inst_tac [("x","schB")] subst_lemma1 1);
   497 by (assume_tac 1);
   498 (* IH *)
   499 by (asm_full_simp_tac (simpset() addsimps [not_ext_is_int_or_not_act,
   500                    ForallTL,ForallDropwhile]) 1);
   501 
   502 (* Case a:A, a~:B *)
   503 by (ftac divide_Seq 1);
   504 by (REPEAT (etac conjE 1));
   505 (* filtering internals of A is nil *)
   506 by (asm_full_simp_tac (simpset() addsimps 
   507           [not_ext_is_int_or_not_act,
   508            externals_of_par, intA_is_not_extB,int_is_not_ext]) 1);
   509 by (dres_inst_tac [("x","schA")] subst_lemma1 1);
   510 by (assume_tac 1);
   511 by (asm_full_simp_tac (simpset() addsimps [not_ext_is_int_or_not_act,
   512                     ForallTL,ForallDropwhile]) 1);
   513 
   514 (* Case a:B, a~:A *)
   515 by (ftac divide_Seq 1);
   516 by (REPEAT (etac conjE 1));
   517 (* filtering internals of A is nil *)
   518 by (asm_full_simp_tac (simpset() addsimps 
   519           [not_ext_is_int_or_not_act,
   520            externals_of_par, intA_is_not_extB,int_is_not_ext]) 1);
   521 by (dres_inst_tac [("x","schB")] subst_lemma1 1);
   522 back();
   523 by (assume_tac 1);
   524 by (asm_full_simp_tac (simpset() addsimps [not_ext_is_int_or_not_act,
   525                     ForallTL,ForallDropwhile]) 1);
   526 
   527 (* Case a~:A, a~:B *)
   528 by (fast_tac (claset() addSIs [ext_is_act] 
   529                       addss (simpset() addsimps [externals_of_par]) ) 1);
   530 qed"FilterA_mksch_is_tr";
   531 
   532 
   533 
   534 (*
   535 
   536 ***************************************************************8
   537 With uncomplete take lemma rule should be reused afterwards !!!!!!!!!!!!!!!!!
   538 **********************************************************************
   539 
   540 (*---------------------------------------------------------------------------
   541               Filter of mksch(tr,schA,schB) to A is schA 
   542                              take lemma
   543   --------------------------------------------------------------------------- *)
   544 
   545 Goal "!! A B. [| compatible A B; compatible B A; \
   546 \ is_asig(asig_of A); is_asig(asig_of B) |] ==> \
   547 \ Forall (%x. x:ext (A||B)) tr & \
   548 \ Forall (%x. x:act A) schA & Forall (%x. x:act B) schB & \
   549 \ Filter (%a. a:ext A)$schA = Filter (%a. a:act A)$tr &\
   550 \ Filter (%a. a:ext B)$schB = Filter (%a. a:act B)$tr &\
   551 \ LastActExtsch A schA & LastActExtsch B schB  \
   552 \ --> Filter (%a. a:act A)$(mksch A B$tr$schA$schB) = schA";
   553 
   554 by (res_inst_tac [("Q","%x. x:act B & x~:act A"),("x","tr")] take_lemma_less_induct 1);
   555 by (REPEAT (etac conjE 1));
   556 
   557 by (case_tac "Finite s" 1);
   558 
   559 (* both sides of this equation are nil *)
   560 by (subgoal_tac "schA=nil" 1);
   561 by (Asm_simp_tac 1);
   562 (* first side: mksch = nil *)
   563 by (SELECT_GOAL (auto_tac (claset() addSIs [ForallQFilterPnil,ForallBnAmksch,FiniteL_mksch],
   564                            simpset())) 1);
   565 (* second side: schA = nil *)
   566 by (eres_inst_tac [("A","A")] LastActExtimplnil 1);
   567 by (Asm_simp_tac 1);
   568 by (SELECT_GOAL (auto_tac (claset() addSIs [ForallQFilterPnil],
   569                            simpset())) 1);
   570 
   571 (* case ~ Finite s *)
   572 
   573 (* both sides of this equation are UU *)
   574 by (subgoal_tac "schA=UU" 1);
   575 by (Asm_simp_tac 1);
   576 (* first side: mksch = UU *)
   577 by (SELECT_GOAL (auto_tac (claset() addSIs [ForallQFilterPUU,
   578                                            (finiteR_mksch RS mp COMP rev_contrapos),
   579                                             ForallBnAmksch],
   580                            simpset())) 1);
   581 (* schA = UU *)
   582 by (eres_inst_tac [("A","A")] LastActExtimplUU 1);
   583 by (Asm_simp_tac 1);
   584 by (SELECT_GOAL (auto_tac (claset() addSIs [ForallQFilterPUU],
   585                            simpset())) 1);
   586 
   587 (* case" ~ Forall (%x.x:act B & x~:act A) s" *)
   588 
   589 by (REPEAT (etac conjE 1));
   590 
   591 (* bring in lemma reduceA_mksch *)
   592 by (forw_inst_tac [("y","schB"),("x","schA")] reduceA_mksch 1);
   593 by (REPEAT (atac 1));
   594 by (REPEAT (etac exE 1));
   595 by (REPEAT (etac conjE 1));
   596 
   597 (* use reduceA_mksch to rewrite conclusion *)
   598 by (hyp_subst_tac 1);
   599 by (Asm_full_simp_tac  1);
   600 
   601 (* eliminate the B-only prefix *)
   602 
   603 by (subgoal_tac "(Filter (%a. a :act A)$y1) = nil" 1);
   604 by (etac ForallQFilterPnil 2);
   605 by (assume_tac 2);
   606 by (Fast_tac 2);
   607 
   608 (* Now real recursive step follows (in y) *)
   609 
   610 by (Asm_full_simp_tac  1);
   611 by (case_tac "y:act A" 1);
   612 by (case_tac "y~:act B" 1);
   613 by (rotate_tac ~2 1);
   614 by (Asm_full_simp_tac 1);
   615 
   616 by (subgoal_tac "Filter (%a. a:act A & a:ext B)$y1=nil" 1);
   617 by (rotate_tac ~1 1);
   618 by (Asm_full_simp_tac  1);
   619 (* eliminate introduced subgoal 2 *)
   620 by (etac ForallQFilterPnil 2);
   621 by (assume_tac 2);
   622 by (Fast_tac 2);
   623  
   624 (* bring in divide Seq for s *)
   625 by (forward_tac [sym RS antisym_less_inverse RS conjunct1 RS divide_Seq] 1);
   626 by (REPEAT (etac conjE 1));
   627 
   628 (* subst divide_Seq in conclusion, but only at the righest occurence *)
   629 by (res_inst_tac [("t","schA")] ssubst 1);
   630 back();
   631 back();
   632 back();
   633 by (assume_tac 1);
   634 
   635 (* reduce trace_takes from n to strictly smaller k *)
   636 by (rtac take_reduction 1);
   637 
   638 (* f A (tw iA) = tw ~eA *)
   639 by (asm_full_simp_tac (simpset() addsimps [FilterPTakewhileQid,int_is_act,
   640                               not_ext_is_int_or_not_act]) 1);
   641 by (rtac refl 1);
   642 
   643 (* now conclusion fulfills induction hypothesis, but assumptions are not ready *)
   644 (*
   645 
   646 nacessary anymore ???????????????? 
   647 by (rotate_tac ~10 1);
   648 
   649 *)
   650 (* assumption schB *)
   651 by (asm_full_simp_tac (simpset() addsimps [ext_and_act]) 1);
   652 (* assumption schA *)
   653 by (dres_inst_tac [("x","schA"),
   654                    ("g","Filter (%a. a:act A)$s2")] subst_lemma2 1);
   655 by (assume_tac 1);
   656 by (Asm_full_simp_tac 1);
   657 (* assumptions concerning LastActExtsch, cannot be rewritten, as LastActExtsmalli are looping  *)
   658 by (dres_inst_tac [("sch","schA"),("P","%a. a:int A")] LastActExtsmall1 1);
   659 by (dres_inst_tac [("sch1.0","y1")]  LastActExtsmall2 1);
   660 by (assume_tac 1);
   661 
   662 FIX: problem: schA and schB are not quantified in the new take lemma version !!!
   663 
   664 by (Asm_full_simp_tac 1);
   665 
   666 **********************************************************************************************
   667 *)
   668 
   669 
   670 
   671 (*--------------------------------------------------------------------------- *)
   672 
   673      section" Filter of mksch(tr,schA,schB) to A is schA -- take lemma proof";  
   674   
   675 (*  --------------------------------------------------------------------------- *)
   676 
   677 
   678 
   679 Goal "!! A B. [| compatible A B; compatible B A; \
   680 \ is_asig(asig_of A); is_asig(asig_of B) |] ==> \
   681 \ Forall (%x. x:ext (A||B)) tr & \
   682 \ Forall (%x. x:act A) schA & Forall (%x. x:act B) schB & \
   683 \ Filter (%a. a:ext A)$schA = Filter (%a. a:act A)$tr &\
   684 \ Filter (%a. a:ext B)$schB = Filter (%a. a:act B)$tr &\
   685 \ LastActExtsch A schA & LastActExtsch B schB  \
   686 \ --> Filter (%a. a:act A)$(mksch A B$tr$schA$schB) = schA";
   687 
   688 by (strip_tac 1);
   689 by (resolve_tac seq.take_lemmas 1);
   690 by (rtac mp 1);
   691 by (assume_tac 2);
   692 back();back();back();back();
   693 by (res_inst_tac [("x","schA")] spec 1);
   694 by (res_inst_tac [("x","schB")] spec 1);
   695 by (res_inst_tac [("x","tr")] spec 1);
   696 by (thin_tac' 5 1);
   697 by (rtac nat_less_induct 1);
   698 by (REPEAT (rtac allI 1));
   699 ren "tr schB schA" 1;
   700 by (strip_tac 1);
   701 by (REPEAT (etac conjE 1));
   702 
   703 by (case_tac "Forall (%x. x:act B & x~:act A) tr" 1);
   704 
   705 by (rtac (seq_take_lemma RS iffD2 RS spec) 1);
   706 by (thin_tac' 5 1);
   707 
   708 
   709 by (case_tac "Finite tr" 1);
   710 
   711 (* both sides of this equation are nil *)
   712 by (subgoal_tac "schA=nil" 1);
   713 by (Asm_simp_tac 1);
   714 (* first side: mksch = nil *)
   715 by (SELECT_GOAL (auto_tac (claset() addSIs [ForallQFilterPnil,ForallBnAmksch,FiniteL_mksch],
   716                            simpset())) 1);
   717 (* second side: schA = nil *)
   718 by (eres_inst_tac [("A","A")] LastActExtimplnil 1);
   719 by (Asm_simp_tac 1);
   720 by (eres_inst_tac [("Q","%x. x:act B & x~:act A")] ForallQFilterPnil 1);
   721 by (assume_tac 1);
   722 by (Fast_tac 1);
   723 
   724 (* case ~ Finite s *)
   725 
   726 (* both sides of this equation are UU *)
   727 by (subgoal_tac "schA=UU" 1);
   728 by (Asm_simp_tac 1);
   729 (* first side: mksch = UU *)
   730 by (SELECT_GOAL (auto_tac (claset() addSIs [ForallQFilterPUU,
   731         (finiteR_mksch RS mp COMP rev_contrapos),ForallBnAmksch],simpset())) 1);
   732 (* schA = UU *)
   733 by (eres_inst_tac [("A","A")] LastActExtimplUU 1);
   734 by (Asm_simp_tac 1);
   735 by (eres_inst_tac [("Q","%x. x:act B & x~:act A")] ForallQFilterPUU 1);
   736 by (assume_tac 1);
   737 by (Fast_tac 1);
   738 
   739 (* case" ~ Forall (%x.x:act B & x~:act A) s" *)
   740 
   741 by (dtac divide_Seq3 1);
   742 
   743 by (REPEAT (etac exE 1));
   744 by (REPEAT (etac conjE 1));
   745 by (hyp_subst_tac 1);
   746 
   747 (* bring in lemma reduceA_mksch *)
   748 by (forw_inst_tac [("x","schA"),("y","schB"),("A","A"),("B","B")] reduceA_mksch 1);
   749 by (REPEAT (atac 1));
   750 by (REPEAT (etac exE 1));
   751 by (REPEAT (etac conjE 1));
   752 
   753 (* use reduceA_mksch to rewrite conclusion *)
   754 by (hyp_subst_tac 1);
   755 by (Asm_full_simp_tac  1);
   756 
   757 (* eliminate the B-only prefix *)
   758 
   759 by (subgoal_tac "(Filter (%a. a :act A)$y1) = nil" 1);
   760 by (etac ForallQFilterPnil 2);
   761 by (assume_tac 2);
   762 by (Fast_tac 2);
   763 
   764 (* Now real recursive step follows (in y) *)
   765 
   766 by (Asm_full_simp_tac  1);
   767 by (case_tac "x:act A" 1);
   768 by (case_tac "x~:act B" 1);
   769 by (rotate_tac ~2 1);
   770 by (Asm_full_simp_tac 1);
   771 
   772 by (subgoal_tac "Filter (%a. a:act A & a:ext B)$y1=nil" 1);
   773 by (rotate_tac ~1 1);
   774 by (Asm_full_simp_tac  1);
   775 (* eliminate introduced subgoal 2 *)
   776 by (etac ForallQFilterPnil 2);
   777 by (assume_tac 2);
   778 by (Fast_tac 2);
   779  
   780 (* bring in divide Seq for s *)
   781 by (forward_tac [sym RS antisym_less_inverse RS conjunct1 RS divide_Seq] 1);
   782 by (REPEAT (etac conjE 1));
   783 
   784 (* subst divide_Seq in conclusion, but only at the righest occurence *)
   785 by (res_inst_tac [("t","schA")] ssubst 1);
   786 back();
   787 back();
   788 back();
   789 by (assume_tac 1);
   790 
   791 (* reduce trace_takes from n to strictly smaller k *)
   792 by (rtac take_reduction 1);
   793 
   794 (* f A (tw iA) = tw ~eA *)
   795 by (asm_full_simp_tac (simpset() addsimps [FilterPTakewhileQid,int_is_act,
   796                               not_ext_is_int_or_not_act]) 1);
   797 by (rtac refl 1);
   798 by (asm_full_simp_tac (simpset() addsimps [int_is_act,
   799                               not_ext_is_int_or_not_act]) 1);
   800 by (rotate_tac ~11 1);
   801 
   802 (* now conclusion fulfills induction hypothesis, but assumptions are not ready *)
   803 
   804 (* assumption Forall tr *)
   805 by (asm_full_simp_tac (simpset() addsimps [Forall_Conc]) 1);
   806 (* assumption schB *)
   807 by (asm_full_simp_tac (simpset() addsimps [Forall_Conc,ext_and_act]) 1);
   808 by (REPEAT (etac conjE 1));
   809 (* assumption schA *)
   810 by (dres_inst_tac [("x","schA"),
   811                    ("g","Filter (%a. a:act A)$rs")] subst_lemma2 1);
   812 by (assume_tac 1);
   813 by (asm_full_simp_tac (simpset() addsimps [int_is_not_ext]) 1);
   814 (* assumptions concerning LastActExtsch, cannot be rewritten, as LastActExtsmalli are looping  *)
   815 by (dres_inst_tac [("sch","schA"),("P","%a. a:int A")] LastActExtsmall1 1);
   816 by (forw_inst_tac [("sch1.0","y1")]  LastActExtsmall2 1);
   817 by (assume_tac 1);
   818 
   819 (* assumption Forall schA *)
   820 by (dres_inst_tac [("s","schA"),
   821                    ("P","Forall (%x. x:act A)")] subst 1);
   822 by (assume_tac 1);
   823 by (asm_full_simp_tac (simpset() addsimps [ForallPTakewhileQ, int_is_act]) 1);
   824 
   825 (* case x:actions(asig_of A) & x: actions(asig_of B) *)
   826 
   827 
   828 by (rotate_tac ~2 1);
   829 by (Asm_full_simp_tac  1);
   830 
   831 by (subgoal_tac "Filter (%a. a:act A & a:ext B)$y1=nil" 1);
   832 by (rotate_tac ~1 1);
   833 by (Asm_full_simp_tac  1);
   834 (* eliminate introduced subgoal 2 *)
   835 by (etac ForallQFilterPnil 2);
   836 by (assume_tac 2);
   837 by (Fast_tac 2);
   838 
   839 (* bring in divide Seq for s *)
   840 by (forward_tac [sym RS antisym_less_inverse RS conjunct1 RS divide_Seq] 1);
   841 by (REPEAT (etac conjE 1));
   842 
   843 (* subst divide_Seq in conclusion, but only at the righest occurence *)
   844 by (res_inst_tac [("t","schA")] ssubst 1);
   845 back();
   846 back();
   847 back();
   848 by (assume_tac 1);
   849 
   850 (* f A (tw iA) = tw ~eA *)
   851 by (asm_full_simp_tac (simpset() addsimps [FilterPTakewhileQid,int_is_act,
   852                               not_ext_is_int_or_not_act]) 1);
   853 
   854 (* rewrite assumption forall and schB *)
   855 by (rotate_tac 13 1);
   856 by (asm_full_simp_tac (simpset() addsimps [ext_and_act]) 1);
   857 
   858 (* divide_Seq for schB2 *)
   859 by (forw_inst_tac [("y","y2")] (sym RS antisym_less_inverse RS conjunct1 RS divide_Seq) 1);
   860 by (REPEAT (etac conjE 1));
   861 (* assumption schA *)
   862 by (dres_inst_tac [("x","schA"),
   863                    ("g","Filter (%a. a:act A)$rs")] subst_lemma2 1);
   864 by (assume_tac 1);
   865 by (asm_full_simp_tac (simpset() addsimps [int_is_not_ext]) 1);
   866 
   867 (* f A (tw iB schB2) = nil *) 
   868 by (asm_full_simp_tac (simpset() addsimps [int_is_not_ext,not_ext_is_int_or_not_act,
   869              intA_is_not_actB]) 1);
   870 
   871 
   872 (* reduce trace_takes from n to strictly smaller k *)
   873 by (rtac take_reduction 1);
   874 by (rtac refl 1);
   875 by (rtac refl 1);
   876 
   877 (* now conclusion fulfills induction hypothesis, but assumptions are not all ready *)
   878 
   879 (* assumption schB *)
   880 by (dres_inst_tac [("x","y2"),
   881                    ("g","Filter (%a. a:act B)$rs")] subst_lemma2 1);
   882 by (assume_tac 1);
   883 by (asm_full_simp_tac (simpset() addsimps [intA_is_not_actB,int_is_not_ext]) 1);
   884 
   885 (* conclusions concerning LastActExtsch, cannot be rewritten, as LastActExtsmalli are looping  *)
   886 by (dres_inst_tac [("sch","schA"),("P","%a. a:int A")] LastActExtsmall1 1);
   887 by (forw_inst_tac [("sch1.0","y1")]  LastActExtsmall2 1);
   888 by (assume_tac 1);
   889 by (dres_inst_tac [("sch","y2"),("P","%a. a:int B")] LastActExtsmall1 1);
   890 
   891 (* assumption Forall schA, and Forall schA are performed by ForallTL,ForallDropwhile *)
   892 by (asm_full_simp_tac (simpset() addsimps [ForallTL,ForallDropwhile]) 1);
   893 
   894 (* case x~:A & x:B  *)
   895 (* cannot occur, as just this case has been scheduled out before as the B-only prefix *)
   896 by (case_tac "x:act B" 1);
   897 by (Fast_tac 1);
   898 
   899 (* case x~:A & x~:B  *)
   900 (* cannot occur because of assumption: Forall (a:ext A | a:ext B) *)
   901 by (rotate_tac ~9 1);
   902 (* reduce forall assumption from tr to (x>>rs) *)
   903 by (asm_full_simp_tac (simpset() addsimps [externals_of_par]) 1);
   904 by (REPEAT (etac conjE 1));
   905 by (fast_tac (claset() addSIs [ext_is_act]) 1);
   906 
   907 qed"FilterAmksch_is_schA";
   908 
   909 
   910 
   911 (*---------------------------------------------------------------------------  *)
   912 
   913    section" Filter of mksch(tr,schA,schB) to B is schB -- take lemma proof";
   914                 
   915 (*  --------------------------------------------------------------------------- *)
   916 
   917 
   918 
   919 Goal "!! A B. [| compatible A B; compatible B A; \
   920 \ is_asig(asig_of A); is_asig(asig_of B) |] ==> \
   921 \ Forall (%x. x:ext (A||B)) tr & \
   922 \ Forall (%x. x:act A) schA & Forall (%x. x:act B) schB & \
   923 \ Filter (%a. a:ext A)$schA = Filter (%a. a:act A)$tr &\
   924 \ Filter (%a. a:ext B)$schB = Filter (%a. a:act B)$tr &\
   925 \ LastActExtsch A schA & LastActExtsch B schB  \
   926 \ --> Filter (%a. a:act B)$(mksch A B$tr$schA$schB) = schB";
   927 
   928 by (strip_tac 1);
   929 by (resolve_tac seq.take_lemmas 1);
   930 by (rtac mp 1);
   931 by (assume_tac 2);
   932 back();back();back();back();
   933 by (res_inst_tac [("x","schA")] spec 1);
   934 by (res_inst_tac [("x","schB")] spec 1);
   935 by (res_inst_tac [("x","tr")] spec 1);
   936 by (thin_tac' 5 1);
   937 by (rtac nat_less_induct 1);
   938 by (REPEAT (rtac allI 1));
   939 ren "tr schB schA" 1;
   940 by (strip_tac 1);
   941 by (REPEAT (etac conjE 1));
   942 
   943 by (case_tac "Forall (%x. x:act A & x~:act B) tr" 1);
   944 
   945 by (rtac (seq_take_lemma RS iffD2 RS spec) 1);
   946 by (thin_tac' 5 1);
   947 
   948 
   949 by (case_tac "Finite tr" 1);
   950 
   951 (* both sides of this equation are nil *)
   952 by (subgoal_tac "schB=nil" 1);
   953 by (Asm_simp_tac 1);
   954 (* first side: mksch = nil *)
   955 by (SELECT_GOAL (auto_tac (claset() addSIs [ForallQFilterPnil,ForallAnBmksch,FiniteL_mksch],
   956                            simpset())) 1);
   957 (* second side: schA = nil *)
   958 by (eres_inst_tac [("A","B")] LastActExtimplnil 1);
   959 by (Asm_simp_tac 1);
   960 by (eres_inst_tac [("Q","%x. x:act A & x~:act B")] ForallQFilterPnil 1);
   961 by (assume_tac 1);
   962 by (Fast_tac 1);
   963 
   964 (* case ~ Finite tr *)
   965 
   966 (* both sides of this equation are UU *)
   967 by (subgoal_tac "schB=UU" 1);
   968 by (Asm_simp_tac 1);
   969 (* first side: mksch = UU *)
   970 by (force_tac (claset() addSIs [ForallQFilterPUU,
   971                                 (finiteR_mksch RS mp COMP rev_contrapos),
   972                                   ForallAnBmksch],
   973                simpset()) 1);
   974 (* schA = UU *)
   975 by (eres_inst_tac [("A","B")] LastActExtimplUU 1);
   976 by (Asm_simp_tac 1);
   977 by (eres_inst_tac [("Q","%x. x:act A & x~:act B")] ForallQFilterPUU 1);
   978 by (assume_tac 1);
   979 by (Fast_tac 1);
   980 
   981 (* case" ~ Forall (%x.x:act B & x~:act A) s" *)
   982 
   983 by (dtac divide_Seq3 1);
   984 
   985 by (REPEAT (etac exE 1));
   986 by (REPEAT (etac conjE 1));
   987 by (hyp_subst_tac 1);
   988 
   989 (* bring in lemma reduceB_mksch *)
   990 by (forw_inst_tac [("y","schB"),("x","schA"),("A","A"),("B","B")] reduceB_mksch 1);
   991 by (REPEAT (atac 1));
   992 by (REPEAT (etac exE 1));
   993 by (REPEAT (etac conjE 1));
   994 
   995 (* use reduceB_mksch to rewrite conclusion *)
   996 by (hyp_subst_tac 1);
   997 by (Asm_full_simp_tac  1);
   998 
   999 (* eliminate the A-only prefix *)
  1000 
  1001 by (subgoal_tac "(Filter (%a. a :act B)$x1) = nil" 1);
  1002 by (etac ForallQFilterPnil 2);
  1003 by (assume_tac 2);
  1004 by (Fast_tac 2);
  1005 
  1006 (* Now real recursive step follows (in x) *)
  1007 
  1008 by (Asm_full_simp_tac  1);
  1009 by (case_tac "x:act B" 1);
  1010 by (case_tac "x~:act A" 1);
  1011 by (rotate_tac ~2 1);
  1012 by (Asm_full_simp_tac 1);
  1013 
  1014 by (subgoal_tac "Filter (%a. a:act B & a:ext A)$x1=nil" 1);
  1015 by (rotate_tac ~1 1);
  1016 by (Asm_full_simp_tac  1);
  1017 (* eliminate introduced subgoal 2 *)
  1018 by (etac ForallQFilterPnil 2);
  1019 by (assume_tac 2);
  1020 by (Fast_tac 2);
  1021  
  1022 (* bring in divide Seq for s *)
  1023 by (forward_tac [sym RS antisym_less_inverse RS conjunct1 RS divide_Seq] 1);
  1024 by (REPEAT (etac conjE 1));
  1025 
  1026 (* subst divide_Seq in conclusion, but only at the righest occurence *)
  1027 by (res_inst_tac [("t","schB")] ssubst 1);
  1028 back();
  1029 back();
  1030 back();
  1031 by (assume_tac 1);
  1032 
  1033 (* reduce trace_takes from n to strictly smaller k *)
  1034 by (rtac take_reduction 1);
  1035 
  1036 (* f B (tw iB) = tw ~eB *)
  1037 by (asm_full_simp_tac (simpset() addsimps [FilterPTakewhileQid,int_is_act,
  1038                               not_ext_is_int_or_not_act]) 1);
  1039 by (rtac refl 1);
  1040 by (asm_full_simp_tac (simpset() addsimps [int_is_act,
  1041                               not_ext_is_int_or_not_act]) 1);
  1042 by (rotate_tac ~11 1);
  1043 
  1044 (* now conclusion fulfills induction hypothesis, but assumptions are not ready *)
  1045 
  1046 (* assumption Forall tr *)
  1047 by (asm_full_simp_tac (simpset() addsimps [Forall_Conc]) 1);
  1048 (* assumption schA *)
  1049 by (asm_full_simp_tac (simpset() addsimps [Forall_Conc,ext_and_act]) 1);
  1050 by (REPEAT (etac conjE 1));
  1051 (* assumption schB *)
  1052 by (dres_inst_tac [("x","schB"),
  1053                    ("g","Filter (%a. a:act B)$rs")] subst_lemma2 1);
  1054 by (assume_tac 1);
  1055 by (asm_full_simp_tac (simpset() addsimps [int_is_not_ext]) 1);
  1056 (* assumptions concerning LastActExtsch, cannot be rewritten, as LastActExtsmalli are looping  *)
  1057 by (dres_inst_tac [("sch","schB"),("P","%a. a:int B")] LastActExtsmall1 1);
  1058 by (forw_inst_tac [("sch1.0","x1")]  LastActExtsmall2 1);
  1059 by (assume_tac 1);
  1060 
  1061 (* assumption Forall schB *)
  1062 by (dres_inst_tac [("s","schB"),
  1063                    ("P","Forall (%x. x:act B)")] subst 1);
  1064 by (assume_tac 1);
  1065 by (asm_full_simp_tac (simpset() addsimps [ForallPTakewhileQ, int_is_act]) 1);
  1066 
  1067 (* case x:actions(asig_of A) & x: actions(asig_of B) *)
  1068 
  1069 
  1070 by (rotate_tac ~2 1);
  1071 by (Asm_full_simp_tac  1);
  1072 
  1073 by (subgoal_tac "Filter (%a. a:act B & a:ext A)$x1=nil" 1);
  1074 by (rotate_tac ~1 1);
  1075 by (Asm_full_simp_tac  1);
  1076 (* eliminate introduced subgoal 2 *)
  1077 by (etac ForallQFilterPnil 2);
  1078 by (assume_tac 2);
  1079 by (Fast_tac 2);
  1080  
  1081 (* bring in divide Seq for s *)
  1082 by (forward_tac [sym RS antisym_less_inverse RS conjunct1 RS divide_Seq] 1);
  1083 by (REPEAT (etac conjE 1));
  1084 
  1085 (* subst divide_Seq in conclusion, but only at the righest occurence *)
  1086 by (res_inst_tac [("t","schB")] ssubst 1);
  1087 back();
  1088 back();
  1089 back();
  1090 by (assume_tac 1);
  1091 
  1092 (* f B (tw iB) = tw ~eB *)
  1093 by (asm_full_simp_tac (simpset() addsimps [FilterPTakewhileQid,int_is_act,
  1094                               not_ext_is_int_or_not_act]) 1);
  1095 
  1096 (* rewrite assumption forall and schB *)
  1097 by (rotate_tac 13 1);
  1098 by (asm_full_simp_tac (simpset() addsimps [ext_and_act]) 1);
  1099 
  1100 (* divide_Seq for schB2 *)
  1101 by (forw_inst_tac [("y","x2")] (sym RS antisym_less_inverse RS conjunct1 RS divide_Seq) 1);
  1102 by (REPEAT (etac conjE 1));
  1103 (* assumption schA *)
  1104 by (dres_inst_tac [("x","schB"),
  1105                    ("g","Filter (%a. a:act B)$rs")] subst_lemma2 1);
  1106 by (assume_tac 1);
  1107 by (asm_full_simp_tac (simpset() addsimps [int_is_not_ext]) 1);
  1108 
  1109 (* f B (tw iA schA2) = nil *) 
  1110 by (asm_full_simp_tac (simpset() addsimps [int_is_not_ext,not_ext_is_int_or_not_act,
  1111              intA_is_not_actB]) 1);
  1112 
  1113 
  1114 (* reduce trace_takes from n to strictly smaller k *)
  1115 by (rtac take_reduction 1);
  1116 by (rtac refl 1);
  1117 by (rtac refl 1);
  1118 
  1119 (* now conclusion fulfills induction hypothesis, but assumptions are not all ready *)
  1120 
  1121 (* assumption schA *)
  1122 by (dres_inst_tac [("x","x2"),
  1123                    ("g","Filter (%a. a:act A)$rs")] subst_lemma2 1);
  1124 by (assume_tac 1);
  1125 by (asm_full_simp_tac (simpset() addsimps [intA_is_not_actB,int_is_not_ext]) 1);
  1126 
  1127 (* conclusions concerning LastActExtsch, cannot be rewritten, as LastActExtsmalli are looping  *)
  1128 by (dres_inst_tac [("sch","schB"),("P","%a. a:int B")] LastActExtsmall1 1);
  1129 by (forw_inst_tac [("sch1.0","x1")]  LastActExtsmall2 1);
  1130 by (assume_tac 1);
  1131 by (dres_inst_tac [("sch","x2"),("P","%a. a:int A")] LastActExtsmall1 1);
  1132 
  1133 (* assumption Forall schA, and Forall schA are performed by ForallTL,ForallDropwhile *)
  1134 by (asm_full_simp_tac (simpset() addsimps [ForallTL,ForallDropwhile]) 1);
  1135 
  1136 (* case x~:B & x:A  *)
  1137 (* cannot occur, as just this case has been scheduled out before as the B-only prefix *)
  1138 by (case_tac "x:act A" 1);
  1139 by (Fast_tac 1);
  1140 
  1141 (* case x~:B & x~:A  *)
  1142 (* cannot occur because of assumption: Forall (a:ext A | a:ext B) *)
  1143 by (rotate_tac ~9 1);
  1144 (* reduce forall assumption from tr to (x>>rs) *)
  1145 by (asm_full_simp_tac (simpset() addsimps [externals_of_par]) 1);
  1146 by (REPEAT (etac conjE 1));
  1147 by (fast_tac (claset() addSIs [ext_is_act]) 1);
  1148 
  1149 qed"FilterBmksch_is_schB";
  1150 
  1151 
  1152 
  1153 (* ------------------------------------------------------------------ *)
  1154          section"COMPOSITIONALITY on TRACE Level -- Main Theorem";
  1155 (* ------------------------------------------------------------------ *)
  1156  
  1157 Goal 
  1158 "!! A B. [| is_trans_of A; is_trans_of B; compatible A B; compatible B A; \
  1159 \           is_asig(asig_of A); is_asig(asig_of B)|] \
  1160 \       ==>  tr: traces(A||B) = \
  1161 \            (Filter (%a. a:act A)$tr : traces A &\
  1162 \             Filter (%a. a:act B)$tr : traces B &\
  1163 \             Forall (%x. x:ext(A||B)) tr)";
  1164 
  1165 by (simp_tac (simpset() addsimps [traces_def,has_trace_def]) 1);
  1166 by (safe_tac set_cs);
  1167  
  1168 (* ==> *) 
  1169 (* There is a schedule of A *)
  1170 by (res_inst_tac [("x","Filter (%a. a:act A)$sch")] bexI 1);
  1171 by (asm_full_simp_tac (simpset() addsimps [compositionality_sch]) 2);
  1172 by (asm_full_simp_tac (simpset() addsimps [compatibility_consequence1,
  1173                   externals_of_par,ext1_ext2_is_not_act1]) 1);
  1174 (* There is a schedule of B *)
  1175 by (res_inst_tac [("x","Filter (%a. a:act B)$sch")] bexI 1);
  1176 by (asm_full_simp_tac (simpset() addsimps [compositionality_sch]) 2);
  1177 by (asm_full_simp_tac (simpset() addsimps [compatibility_consequence2,
  1178                   externals_of_par,ext1_ext2_is_not_act2]) 1);
  1179 (* Traces of A||B have only external actions from A or B *)  
  1180 by (rtac ForallPFilterP 1);
  1181 
  1182 (* <== *)
  1183 
  1184 (* replace schA and schB by Cut(schA) and Cut(schB) *)
  1185 by (dtac exists_LastActExtsch 1);
  1186 by (assume_tac 1);
  1187 by (dtac exists_LastActExtsch 1);
  1188 by (assume_tac 1);
  1189 by (REPEAT (etac exE 1));
  1190 by (REPEAT (etac conjE 1));
  1191 (* Schedules of A(B) have only actions of A(B) *)
  1192 by (dtac scheds_in_sig 1);
  1193 by (assume_tac 1);
  1194 by (dtac scheds_in_sig 1);
  1195 by (assume_tac 1);
  1196 
  1197 ren "h1 h2 schA schB" 1;
  1198 (* mksch is exactly the construction of trA||B out of schA, schB, and the oracle tr,
  1199    we need here *)
  1200 by (res_inst_tac [("x","mksch A B$tr$schA$schB")] bexI 1);
  1201 
  1202 (* External actions of mksch are just the oracle *)
  1203 by (asm_full_simp_tac (simpset() addsimps [FilterA_mksch_is_tr RS spec RS spec RS mp]) 1);
  1204 
  1205 (* mksch is a schedule -- use compositionality on sch-level *)
  1206 by (asm_full_simp_tac (simpset() addsimps [compositionality_sch]) 1);
  1207 by (asm_full_simp_tac (simpset() addsimps [FilterAmksch_is_schA,FilterBmksch_is_schB]) 1);
  1208 by (etac ForallAorB_mksch 1);
  1209 by (etac ForallPForallQ 1);
  1210 by (etac ext_is_act 1);
  1211 qed"compositionality_tr";
  1212 
  1213 
  1214 
  1215 (* ------------------------------------------------------------------ *)
  1216 (*           COMPOSITIONALITY   on    TRACE         Level             *)
  1217 (*                            For Modules                             *)
  1218 (* ------------------------------------------------------------------ *)
  1219 
  1220 Goalw [Traces_def,par_traces_def]
  1221 
  1222 "!! A B. [| is_trans_of A; is_trans_of B; compatible A B; compatible B A; \
  1223 \           is_asig(asig_of A); is_asig(asig_of B)|] \
  1224 \==> Traces (A||B) = par_traces (Traces A) (Traces B)";
  1225 
  1226 by (asm_full_simp_tac (simpset() addsimps [asig_of_par]) 1);
  1227 by (rtac set_ext 1);
  1228 by (asm_full_simp_tac (simpset() addsimps [compositionality_tr,externals_of_par]) 1);
  1229 qed"compositionality_tr_modules";
  1230 
  1231 
  1232 simpset_ref () := simpset() setmksym (Some o symmetric_fun);