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