src/HOLCF/IOA/meta_theory/CompoTraces.thy
author huffman
Sun Mar 07 16:39:31 2010 -0800 (2010-03-07)
changeset 35642 f478d5a9d238
parent 35215 a03462cbf86f
child 36543 0e7fc5bf38de
permissions -rw-r--r--
generate separate qualified theorem name for each type's reach and take_lemma
     1 (*  Title:      HOLCF/IOA/meta_theory/CompoTraces.thy
     2     Author:     Olaf Müller
     3 *) 
     4 
     5 header {* Compositionality on Trace level *}
     6 
     7 theory CompoTraces
     8 imports CompoScheds ShortExecutions
     9 begin
    10  
    11 
    12 consts  
    13 
    14  mksch      ::"('a,'s)ioa => ('a,'t)ioa => 'a Seq -> 'a Seq -> 'a Seq -> 'a Seq" 
    15  par_traces ::"['a trace_module,'a trace_module] => 'a trace_module"
    16 
    17 defs
    18 
    19 mksch_def:
    20   "mksch A B == (fix$(LAM h tr schA schB. case tr of 
    21        nil => nil
    22     | x##xs => 
    23       (case x of 
    24         UU => UU
    25       | Def y => 
    26          (if y:act A then 
    27              (if y:act B then 
    28                    ((Takewhile (%a. a:int A)$schA)
    29                       @@ (Takewhile (%a. a:int B)$schB)
    30                            @@ (y>>(h$xs
    31                                     $(TL$(Dropwhile (%a. a:int A)$schA))
    32                                     $(TL$(Dropwhile (%a. a:int B)$schB))
    33                     )))
    34               else
    35                  ((Takewhile (%a. a:int A)$schA)
    36                   @@ (y>>(h$xs
    37                            $(TL$(Dropwhile (%a. a:int A)$schA))
    38                            $schB)))
    39               )
    40           else 
    41              (if y:act B then 
    42                  ((Takewhile (%a. a:int B)$schB)
    43                      @@ (y>>(h$xs
    44                               $schA
    45                               $(TL$(Dropwhile (%a. a:int B)$schB))
    46                               )))
    47              else
    48                UU
    49              )
    50          )
    51        )))"
    52 
    53 
    54 par_traces_def:
    55   "par_traces TracesA TracesB == 
    56        let trA = fst TracesA; sigA = snd TracesA; 
    57            trB = fst TracesB; sigB = snd TracesB       
    58        in
    59        (    {tr. Filter (%a. a:actions sigA)$tr : trA}
    60         Int {tr. Filter (%a. a:actions sigB)$tr : trB}
    61         Int {tr. Forall (%x. x:(externals sigA Un externals sigB)) tr},
    62         asig_comp sigA sigB)"
    63 
    64 axioms
    65 
    66 finiteR_mksch:
    67   "Finite (mksch A B$tr$x$y) --> Finite tr"
    68 
    69 
    70 declaration {* fn _ => Simplifier.map_ss (fn ss => ss setmksym (K NONE)) *}
    71 
    72 
    73 subsection "mksch rewrite rules"
    74 
    75 lemma mksch_unfold:
    76 "mksch A B = (LAM tr schA schB. case tr of 
    77        nil => nil
    78     | x##xs => 
    79       (case x of  
    80         UU => UU  
    81       | Def y => 
    82          (if y:act A then 
    83              (if y:act B then 
    84                    ((Takewhile (%a. a:int A)$schA) 
    85                          @@(Takewhile (%a. a:int B)$schB) 
    86                               @@(y>>(mksch A B$xs   
    87                                        $(TL$(Dropwhile (%a. a:int A)$schA))  
    88                                        $(TL$(Dropwhile (%a. a:int B)$schB))  
    89                     )))   
    90               else  
    91                  ((Takewhile (%a. a:int A)$schA)  
    92                       @@ (y>>(mksch A B$xs  
    93                               $(TL$(Dropwhile (%a. a:int A)$schA))  
    94                               $schB)))  
    95               )   
    96           else    
    97              (if y:act B then  
    98                  ((Takewhile (%a. a:int B)$schB)  
    99                        @@ (y>>(mksch A B$xs   
   100                               $schA   
   101                               $(TL$(Dropwhile (%a. a:int B)$schB))  
   102                               )))  
   103              else  
   104                UU  
   105              )  
   106          )  
   107        ))"
   108 apply (rule trans)
   109 apply (rule fix_eq2)
   110 apply (rule mksch_def)
   111 apply (rule beta_cfun)
   112 apply simp
   113 done
   114 
   115 lemma mksch_UU: "mksch A B$UU$schA$schB = UU"
   116 apply (subst mksch_unfold)
   117 apply simp
   118 done
   119 
   120 lemma mksch_nil: "mksch A B$nil$schA$schB = nil"
   121 apply (subst mksch_unfold)
   122 apply simp
   123 done
   124 
   125 lemma mksch_cons1: "[|x:act A;x~:act B|]   
   126     ==> mksch A B$(x>>tr)$schA$schB =  
   127           (Takewhile (%a. a:int A)$schA)  
   128           @@ (x>>(mksch A B$tr$(TL$(Dropwhile (%a. a:int A)$schA))  
   129                               $schB))"
   130 apply (rule trans)
   131 apply (subst mksch_unfold)
   132 apply (simp add: Consq_def If_and_if)
   133 apply (simp add: Consq_def)
   134 done
   135 
   136 lemma mksch_cons2: "[|x~:act A;x:act B|]  
   137     ==> mksch A B$(x>>tr)$schA$schB =  
   138          (Takewhile (%a. a:int B)$schB)   
   139           @@ (x>>(mksch A B$tr$schA$(TL$(Dropwhile (%a. a:int B)$schB))   
   140                              ))"
   141 apply (rule trans)
   142 apply (subst mksch_unfold)
   143 apply (simp add: Consq_def If_and_if)
   144 apply (simp add: Consq_def)
   145 done
   146 
   147 lemma mksch_cons3: "[|x:act A;x:act B|]  
   148     ==> mksch A B$(x>>tr)$schA$schB =  
   149              (Takewhile (%a. a:int A)$schA)  
   150           @@ ((Takewhile (%a. a:int B)$schB)   
   151           @@ (x>>(mksch A B$tr$(TL$(Dropwhile (%a. a:int A)$schA))  
   152                              $(TL$(Dropwhile (%a. a:int B)$schB))))   
   153               )"
   154 apply (rule trans)
   155 apply (subst mksch_unfold)
   156 apply (simp add: Consq_def If_and_if)
   157 apply (simp add: Consq_def)
   158 done
   159 
   160 lemmas compotr_simps = mksch_UU mksch_nil mksch_cons1 mksch_cons2 mksch_cons3
   161 
   162 declare compotr_simps [simp]
   163 
   164 
   165 subsection {* COMPOSITIONALITY on TRACE Level *}
   166 
   167 subsubsection "Lemmata for ==>"
   168 
   169 (* Consequence out of ext1_ext2_is_not_act1(2), which in turn are consequences out of
   170    the compatibility of IOA, in particular out of the condition that internals are
   171    really hidden. *)
   172 
   173 lemma compatibility_consequence1: "(eB & ~eA --> ~A) -->        
   174           (A & (eA | eB)) = (eA & A)"
   175 apply fast
   176 done
   177 
   178 
   179 (* very similar to above, only the commutativity of | is used to make a slight change *)
   180 
   181 lemma compatibility_consequence2: "(eB & ~eA --> ~A) -->        
   182           (A & (eB | eA)) = (eA & A)"
   183 apply fast
   184 done
   185 
   186 
   187 subsubsection "Lemmata for <=="
   188 
   189 (* Lemma for substitution of looping assumption in another specific assumption *)
   190 lemma subst_lemma1: "[| f << (g x) ; x=(h x) |] ==> f << g (h x)"
   191 by (erule subst)
   192 
   193 (* Lemma for substitution of looping assumption in another specific assumption *)
   194 lemma subst_lemma2: "[| (f x) = y >> g; x=(h x) |] ==> (f (h x)) = y >> g"
   195 by (erule subst)
   196 
   197 lemma ForallAorB_mksch [rule_format]:
   198   "!!A B. compatible A B ==>  
   199     ! schA schB. Forall (%x. x:act (A||B)) tr  
   200     --> Forall (%x. x:act (A||B)) (mksch A B$tr$schA$schB)"
   201 apply (tactic {* Seq_induct_tac @{context} "tr"
   202   [@{thm Forall_def}, @{thm sforall_def}, @{thm mksch_def}] 1 *})
   203 apply auto
   204 apply (simp add: actions_of_par)
   205 apply (case_tac "a:act A")
   206 apply (case_tac "a:act B")
   207 (* a:A, a:B *)
   208 apply simp
   209 apply (rule Forall_Conc_impl [THEN mp])
   210 apply (simp add: intA_is_not_actB int_is_act)
   211 apply (rule Forall_Conc_impl [THEN mp])
   212 apply (simp add: intA_is_not_actB int_is_act)
   213 (* a:A,a~:B *)
   214 apply simp
   215 apply (rule Forall_Conc_impl [THEN mp])
   216 apply (simp add: intA_is_not_actB int_is_act)
   217 apply (case_tac "a:act B")
   218 (* a~:A, a:B *)
   219 apply simp
   220 apply (rule Forall_Conc_impl [THEN mp])
   221 apply (simp add: intA_is_not_actB int_is_act)
   222 (* a~:A,a~:B *)
   223 apply auto
   224 done
   225 
   226 lemma ForallBnAmksch [rule_format (no_asm)]: "!!A B. compatible B A  ==>  
   227     ! schA schB.  (Forall (%x. x:act B & x~:act A) tr  
   228     --> Forall (%x. x:act B & x~:act A) (mksch A B$tr$schA$schB))"
   229 apply (tactic {* Seq_induct_tac @{context} "tr"
   230   [@{thm Forall_def}, @{thm sforall_def}, @{thm mksch_def}] 1 *})
   231 apply auto
   232 apply (rule Forall_Conc_impl [THEN mp])
   233 apply (simp add: intA_is_not_actB int_is_act)
   234 done
   235 
   236 lemma ForallAnBmksch [rule_format (no_asm)]: "!!A B. compatible A B ==>  
   237     ! schA schB.  (Forall (%x. x:act A & x~:act B) tr  
   238     --> Forall (%x. x:act A & x~:act B) (mksch A B$tr$schA$schB))"
   239 apply (tactic {* Seq_induct_tac @{context} "tr"
   240   [@{thm Forall_def}, @{thm sforall_def}, @{thm mksch_def}] 1 *})
   241 apply auto
   242 apply (rule Forall_Conc_impl [THEN mp])
   243 apply (simp add: intA_is_not_actB int_is_act)
   244 done
   245 
   246 (* safe-tac makes too many case distinctions with this lemma in the next proof *)
   247 declare FiniteConc [simp del]
   248 
   249 lemma FiniteL_mksch [rule_format (no_asm)]: "[| Finite tr; is_asig(asig_of A); is_asig(asig_of B) |] ==>  
   250     ! x y. Forall (%x. x:act A) x & Forall (%x. x:act B) y &  
   251            Filter (%a. a:ext A)$x = Filter (%a. a:act A)$tr &  
   252            Filter (%a. a:ext B)$y = Filter (%a. a:act B)$tr & 
   253            Forall (%x. x:ext (A||B)) tr  
   254            --> Finite (mksch A B$tr$x$y)"
   255 
   256 apply (erule Seq_Finite_ind)
   257 apply simp
   258 (* main case *)
   259 apply simp
   260 apply auto
   261 
   262 (* a: act A; a: act B *)
   263 apply (frule sym [THEN antisym_less_inverse, THEN conjunct1, THEN divide_Seq])
   264 apply (frule sym [THEN antisym_less_inverse, THEN conjunct1, THEN divide_Seq])
   265 back
   266 apply (erule conjE)+
   267 (* Finite (tw iA x) and Finite (tw iB y) *)
   268 apply (simp add: not_ext_is_int_or_not_act FiniteConc)
   269 (* now for conclusion IH applicable, but assumptions have to be transformed *)
   270 apply (drule_tac x = "x" and g = "Filter (%a. a:act A) $s" in subst_lemma2)
   271 apply assumption
   272 apply (drule_tac x = "y" and g = "Filter (%a. a:act B) $s" in subst_lemma2)
   273 apply assumption
   274 (* IH *)
   275 apply (simp add: not_ext_is_int_or_not_act ForallTL ForallDropwhile)
   276 
   277 (* a: act B; a~: act A *)
   278 apply (frule sym [THEN antisym_less_inverse, THEN conjunct1, THEN divide_Seq])
   279 
   280 apply (erule conjE)+
   281 (* Finite (tw iB y) *)
   282 apply (simp add: not_ext_is_int_or_not_act FiniteConc)
   283 (* now for conclusion IH applicable, but assumptions have to be transformed *)
   284 apply (drule_tac x = "y" and g = "Filter (%a. a:act B) $s" in subst_lemma2)
   285 apply assumption
   286 (* IH *)
   287 apply (simp add: not_ext_is_int_or_not_act ForallTL ForallDropwhile)
   288 
   289 (* a~: act B; a: act A *)
   290 apply (frule sym [THEN antisym_less_inverse, THEN conjunct1, THEN divide_Seq])
   291 
   292 apply (erule conjE)+
   293 (* Finite (tw iA x) *)
   294 apply (simp add: not_ext_is_int_or_not_act FiniteConc)
   295 (* now for conclusion IH applicable, but assumptions have to be transformed *)
   296 apply (drule_tac x = "x" and g = "Filter (%a. a:act A) $s" in subst_lemma2)
   297 apply assumption
   298 (* IH *)
   299 apply (simp add: not_ext_is_int_or_not_act ForallTL ForallDropwhile)
   300 
   301 (* a~: act B; a~: act A *)
   302 apply (fastsimp intro!: ext_is_act simp: externals_of_par)
   303 done
   304 
   305 declare FiniteConc [simp]
   306 
   307 declare FilterConc [simp del]
   308 
   309 lemma reduceA_mksch1 [rule_format (no_asm)]: " [| Finite bs; is_asig(asig_of A); is_asig(asig_of B);compatible A B|] ==>   
   310  ! y. Forall (%x. x:act B) y & Forall (%x. x:act B & x~:act A) bs & 
   311      Filter (%a. a:ext B)$y = Filter (%a. a:act B)$(bs @@ z)  
   312      --> (? y1 y2.  (mksch A B$(bs @@ z)$x$y) = (y1 @@ (mksch A B$z$x$y2)) &  
   313                     Forall (%x. x:act B & x~:act A) y1 &  
   314                     Finite y1 & y = (y1 @@ y2) &  
   315                     Filter (%a. a:ext B)$y1 = bs)"
   316 apply (frule_tac A1 = "A" in compat_commute [THEN iffD1])
   317 apply (erule Seq_Finite_ind)
   318 apply (rule allI)+
   319 apply (rule impI)
   320 apply (rule_tac x = "nil" in exI)
   321 apply (rule_tac x = "y" in exI)
   322 apply simp
   323 (* main case *)
   324 apply (rule allI)+
   325 apply (rule impI)
   326 apply simp
   327 apply (erule conjE)+
   328 apply simp
   329 (* divide_Seq on s *)
   330 apply (frule sym [THEN antisym_less_inverse, THEN conjunct1, THEN divide_Seq])
   331 apply (erule conjE)+
   332 (* transform assumption f eB y = f B (s@z) *)
   333 apply (drule_tac x = "y" and g = "Filter (%a. a:act B) $ (s@@z) " in subst_lemma2)
   334 apply assumption
   335 apply (simp add: not_ext_is_int_or_not_act FilterConc)
   336 (* apply IH *)
   337 apply (erule_tac x = "TL$ (Dropwhile (%a. a:int B) $y) " in allE)
   338 apply (simp add: ForallTL ForallDropwhile FilterConc)
   339 apply (erule exE)+
   340 apply (erule conjE)+
   341 apply (simp add: FilterConc)
   342 (* for replacing IH in conclusion *)
   343 apply (rotate_tac -2)
   344 (* instantiate y1a and y2a *)
   345 apply (rule_tac x = "Takewhile (%a. a:int B) $y @@ a>>y1" in exI)
   346 apply (rule_tac x = "y2" in exI)
   347 (* elminate all obligations up to two depending on Conc_assoc *)
   348 apply (simp add: intA_is_not_actB int_is_act int_is_not_ext FilterConc)
   349 apply (simp (no_asm) add: Conc_assoc FilterConc)
   350 done
   351 
   352 lemmas reduceA_mksch = conjI [THEN [6] conjI [THEN [5] reduceA_mksch1]]
   353 
   354 lemma reduceB_mksch1 [rule_format]:
   355 " [| Finite a_s; is_asig(asig_of A); is_asig(asig_of B);compatible A B|] ==>   
   356  ! x. Forall (%x. x:act A) x & Forall (%x. x:act A & x~:act B) a_s & 
   357      Filter (%a. a:ext A)$x = Filter (%a. a:act A)$(a_s @@ z)  
   358      --> (? x1 x2.  (mksch A B$(a_s @@ z)$x$y) = (x1 @@ (mksch A B$z$x2$y)) &  
   359                     Forall (%x. x:act A & x~:act B) x1 &  
   360                     Finite x1 & x = (x1 @@ x2) &  
   361                     Filter (%a. a:ext A)$x1 = a_s)"
   362 apply (frule_tac A1 = "A" in compat_commute [THEN iffD1])
   363 apply (erule Seq_Finite_ind)
   364 apply (rule allI)+
   365 apply (rule impI)
   366 apply (rule_tac x = "nil" in exI)
   367 apply (rule_tac x = "x" in exI)
   368 apply simp
   369 (* main case *)
   370 apply (rule allI)+
   371 apply (rule impI)
   372 apply simp
   373 apply (erule conjE)+
   374 apply simp
   375 (* divide_Seq on s *)
   376 apply (frule sym [THEN antisym_less_inverse, THEN conjunct1, THEN divide_Seq])
   377 apply (erule conjE)+
   378 (* transform assumption f eA x = f A (s@z) *)
   379 apply (drule_tac x = "x" and g = "Filter (%a. a:act A) $ (s@@z) " in subst_lemma2)
   380 apply assumption
   381 apply (simp add: not_ext_is_int_or_not_act FilterConc)
   382 (* apply IH *)
   383 apply (erule_tac x = "TL$ (Dropwhile (%a. a:int A) $x) " in allE)
   384 apply (simp add: ForallTL ForallDropwhile FilterConc)
   385 apply (erule exE)+
   386 apply (erule conjE)+
   387 apply (simp add: FilterConc)
   388 (* for replacing IH in conclusion *)
   389 apply (rotate_tac -2)
   390 (* instantiate y1a and y2a *)
   391 apply (rule_tac x = "Takewhile (%a. a:int A) $x @@ a>>x1" in exI)
   392 apply (rule_tac x = "x2" in exI)
   393 (* elminate all obligations up to two depending on Conc_assoc *)
   394 apply (simp add: intA_is_not_actB int_is_act int_is_not_ext FilterConc)
   395 apply (simp (no_asm) add: Conc_assoc FilterConc)
   396 done
   397 
   398 lemmas reduceB_mksch = conjI [THEN [6] conjI [THEN [5] reduceB_mksch1]]
   399 
   400 declare FilterConc [simp]
   401 
   402 
   403 subsection "Filtering external actions out of mksch(tr,schA,schB) yields the oracle tr"
   404 
   405 lemma FilterA_mksch_is_tr: 
   406 "!! A B. [| compatible A B; compatible B A; 
   407             is_asig(asig_of A); is_asig(asig_of B) |] ==>  
   408   ! schA schB. Forall (%x. x:act A) schA & Forall (%x. x:act B) schB &  
   409   Forall (%x. x:ext (A||B)) tr &  
   410   Filter (%a. a:act A)$tr << Filter (%a. a:ext A)$schA & 
   411   Filter (%a. a:act B)$tr << Filter (%a. a:ext B)$schB   
   412   --> Filter (%a. a:ext (A||B))$(mksch A B$tr$schA$schB) = tr"
   413 
   414 apply (tactic {* Seq_induct_tac @{context} "tr"
   415   [@{thm Forall_def}, @{thm sforall_def}, @{thm mksch_def}] 1 *})
   416 (* main case *)
   417 (* splitting into 4 cases according to a:A, a:B *)
   418 apply auto
   419 
   420 (* Case a:A, a:B *)
   421 apply (frule divide_Seq)
   422 apply (frule divide_Seq)
   423 back
   424 apply (erule conjE)+
   425 (* filtering internals of A in schA and of B in schB is nil *)
   426 apply (simp add: not_ext_is_int_or_not_act externals_of_par intA_is_not_extB int_is_not_ext)
   427 (* conclusion of IH ok, but assumptions of IH have to be transformed *)
   428 apply (drule_tac x = "schA" in subst_lemma1)
   429 apply assumption
   430 apply (drule_tac x = "schB" in subst_lemma1)
   431 apply assumption
   432 (* IH *)
   433 apply (simp add: not_ext_is_int_or_not_act ForallTL ForallDropwhile)
   434 
   435 (* Case a:A, a~:B *)
   436 apply (frule divide_Seq)
   437 apply (erule conjE)+
   438 (* filtering internals of A is nil *)
   439 apply (simp add: not_ext_is_int_or_not_act externals_of_par intA_is_not_extB int_is_not_ext)
   440 apply (drule_tac x = "schA" in subst_lemma1)
   441 apply assumption
   442 apply (simp add: not_ext_is_int_or_not_act ForallTL ForallDropwhile)
   443 
   444 (* Case a:B, a~:A *)
   445 apply (frule divide_Seq)
   446 apply (erule conjE)+
   447 (* filtering internals of A is nil *)
   448 apply (simp add: not_ext_is_int_or_not_act externals_of_par intA_is_not_extB int_is_not_ext)
   449 apply (drule_tac x = "schB" in subst_lemma1)
   450 back
   451 apply assumption
   452 apply (simp add: not_ext_is_int_or_not_act ForallTL ForallDropwhile)
   453 
   454 (* Case a~:A, a~:B *)
   455 apply (fastsimp intro!: ext_is_act simp: externals_of_par)
   456 done
   457 
   458 
   459 subsection" Filter of mksch(tr,schA,schB) to A is schA -- take lemma proof"
   460 
   461 lemma FilterAmksch_is_schA: "!! A B. [| compatible A B; compatible B A;  
   462   is_asig(asig_of A); is_asig(asig_of B) |] ==>  
   463   Forall (%x. x:ext (A||B)) tr &  
   464   Forall (%x. x:act A) schA & Forall (%x. x:act B) schB &  
   465   Filter (%a. a:ext A)$schA = Filter (%a. a:act A)$tr & 
   466   Filter (%a. a:ext B)$schB = Filter (%a. a:act B)$tr & 
   467   LastActExtsch A schA & LastActExtsch B schB   
   468   --> Filter (%a. a:act A)$(mksch A B$tr$schA$schB) = schA"
   469 apply (intro strip)
   470 apply (rule seq.take_lemma)
   471 apply (rule mp)
   472 prefer 2 apply assumption
   473 back back back back
   474 apply (rule_tac x = "schA" in spec)
   475 apply (rule_tac x = "schB" in spec)
   476 apply (rule_tac x = "tr" in spec)
   477 apply (tactic "thin_tac' 5 1")
   478 apply (rule nat_less_induct)
   479 apply (rule allI)+
   480 apply (rename_tac tr schB schA)
   481 apply (intro strip)
   482 apply (erule conjE)+
   483 
   484 apply (case_tac "Forall (%x. x:act B & x~:act A) tr")
   485 
   486 apply (rule seq_take_lemma [THEN iffD2, THEN spec])
   487 apply (tactic "thin_tac' 5 1")
   488 
   489 
   490 apply (case_tac "Finite tr")
   491 
   492 (* both sides of this equation are nil *)
   493 apply (subgoal_tac "schA=nil")
   494 apply (simp (no_asm_simp))
   495 (* first side: mksch = nil *)
   496 apply (auto intro!: ForallQFilterPnil ForallBnAmksch FiniteL_mksch)[1]
   497 (* second side: schA = nil *)
   498 apply (erule_tac A = "A" in LastActExtimplnil)
   499 apply (simp (no_asm_simp))
   500 apply (erule_tac Q = "%x. x:act B & x~:act A" in ForallQFilterPnil)
   501 apply assumption
   502 apply fast
   503 
   504 (* case ~ Finite s *)
   505 
   506 (* both sides of this equation are UU *)
   507 apply (subgoal_tac "schA=UU")
   508 apply (simp (no_asm_simp))
   509 (* first side: mksch = UU *)
   510 apply (auto intro!: ForallQFilterPUU finiteR_mksch [THEN mp, COMP rev_contrapos] ForallBnAmksch)[1]
   511 (* schA = UU *)
   512 apply (erule_tac A = "A" in LastActExtimplUU)
   513 apply (simp (no_asm_simp))
   514 apply (erule_tac Q = "%x. x:act B & x~:act A" in ForallQFilterPUU)
   515 apply assumption
   516 apply fast
   517 
   518 (* case" ~ Forall (%x.x:act B & x~:act A) s" *)
   519 
   520 apply (drule divide_Seq3)
   521 
   522 apply (erule exE)+
   523 apply (erule conjE)+
   524 apply hypsubst
   525 
   526 (* bring in lemma reduceA_mksch *)
   527 apply (frule_tac x = "schA" and y = "schB" and A = "A" and B = "B" in reduceA_mksch)
   528 apply assumption+
   529 apply (erule exE)+
   530 apply (erule conjE)+
   531 
   532 (* use reduceA_mksch to rewrite conclusion *)
   533 apply hypsubst
   534 apply simp
   535 
   536 (* eliminate the B-only prefix *)
   537 
   538 apply (subgoal_tac " (Filter (%a. a :act A) $y1) = nil")
   539 apply (erule_tac [2] ForallQFilterPnil)
   540 prefer 2 apply assumption
   541 prefer 2 apply fast
   542 
   543 (* Now real recursive step follows (in y) *)
   544 
   545 apply simp
   546 apply (case_tac "x:act A")
   547 apply (case_tac "x~:act B")
   548 apply (rotate_tac -2)
   549 apply simp
   550 
   551 apply (subgoal_tac "Filter (%a. a:act A & a:ext B) $y1=nil")
   552 apply (rotate_tac -1)
   553 apply simp
   554 (* eliminate introduced subgoal 2 *)
   555 apply (erule_tac [2] ForallQFilterPnil)
   556 prefer 2 apply assumption
   557 prefer 2 apply fast
   558 
   559 (* bring in divide Seq for s *)
   560 apply (frule sym [THEN antisym_less_inverse, THEN conjunct1, THEN divide_Seq])
   561 apply (erule conjE)+
   562 
   563 (* subst divide_Seq in conclusion, but only at the righest occurence *)
   564 apply (rule_tac t = "schA" in ssubst)
   565 back
   566 back
   567 back
   568 apply assumption
   569 
   570 (* reduce trace_takes from n to strictly smaller k *)
   571 apply (rule take_reduction)
   572 
   573 (* f A (tw iA) = tw ~eA *)
   574 apply (simp add: int_is_act not_ext_is_int_or_not_act)
   575 apply (rule refl)
   576 apply (simp add: int_is_act not_ext_is_int_or_not_act)
   577 apply (rotate_tac -11)
   578 
   579 (* now conclusion fulfills induction hypothesis, but assumptions are not ready *)
   580 
   581 (* assumption Forall tr *)
   582 (* assumption schB *)
   583 apply (simp add: ext_and_act)
   584 (* assumption schA *)
   585 apply (drule_tac x = "schA" and g = "Filter (%a. a:act A) $rs" in subst_lemma2)
   586 apply assumption
   587 apply (simp add: int_is_not_ext)
   588 (* assumptions concerning LastActExtsch, cannot be rewritten, as LastActExtsmalli are looping  *)
   589 apply (drule_tac sch = "schA" and P = "%a. a:int A" in LastActExtsmall1)
   590 apply (frule_tac ?sch1.0 = "y1" in LastActExtsmall2)
   591 apply assumption
   592 
   593 (* assumption Forall schA *)
   594 apply (drule_tac s = "schA" and P = "Forall (%x. x:act A) " in subst)
   595 apply assumption
   596 apply (simp add: int_is_act)
   597 
   598 (* case x:actions(asig_of A) & x: actions(asig_of B) *)
   599 
   600 
   601 apply (rotate_tac -2)
   602 apply simp
   603 
   604 apply (subgoal_tac "Filter (%a. a:act A & a:ext B) $y1=nil")
   605 apply (rotate_tac -1)
   606 apply simp
   607 (* eliminate introduced subgoal 2 *)
   608 apply (erule_tac [2] ForallQFilterPnil)
   609 prefer 2 apply (assumption)
   610 prefer 2 apply (fast)
   611 
   612 (* bring in divide Seq for s *)
   613 apply (frule sym [THEN antisym_less_inverse, THEN conjunct1, THEN divide_Seq])
   614 apply (erule conjE)+
   615 
   616 (* subst divide_Seq in conclusion, but only at the righest occurence *)
   617 apply (rule_tac t = "schA" in ssubst)
   618 back
   619 back
   620 back
   621 apply assumption
   622 
   623 (* f A (tw iA) = tw ~eA *)
   624 apply (simp add: int_is_act not_ext_is_int_or_not_act)
   625 
   626 (* rewrite assumption forall and schB *)
   627 apply (rotate_tac 13)
   628 apply (simp add: ext_and_act)
   629 
   630 (* divide_Seq for schB2 *)
   631 apply (frule_tac y = "y2" in sym [THEN antisym_less_inverse, THEN conjunct1, THEN divide_Seq])
   632 apply (erule conjE)+
   633 (* assumption schA *)
   634 apply (drule_tac x = "schA" and g = "Filter (%a. a:act A) $rs" in subst_lemma2)
   635 apply assumption
   636 apply (simp add: int_is_not_ext)
   637 
   638 (* f A (tw iB schB2) = nil *)
   639 apply (simp add: int_is_not_ext not_ext_is_int_or_not_act intA_is_not_actB)
   640 
   641 
   642 (* reduce trace_takes from n to strictly smaller k *)
   643 apply (rule take_reduction)
   644 apply (rule refl)
   645 apply (rule refl)
   646 
   647 (* now conclusion fulfills induction hypothesis, but assumptions are not all ready *)
   648 
   649 (* assumption schB *)
   650 apply (drule_tac x = "y2" and g = "Filter (%a. a:act B) $rs" in subst_lemma2)
   651 apply assumption
   652 apply (simp add: intA_is_not_actB int_is_not_ext)
   653 
   654 (* conclusions concerning LastActExtsch, cannot be rewritten, as LastActExtsmalli are looping  *)
   655 apply (drule_tac sch = "schA" and P = "%a. a:int A" in LastActExtsmall1)
   656 apply (frule_tac ?sch1.0 = "y1" in LastActExtsmall2)
   657 apply assumption
   658 apply (drule_tac sch = "y2" and P = "%a. a:int B" in LastActExtsmall1)
   659 
   660 (* assumption Forall schA, and Forall schA are performed by ForallTL,ForallDropwhile *)
   661 apply (simp add: ForallTL ForallDropwhile)
   662 
   663 (* case x~:A & x:B  *)
   664 (* cannot occur, as just this case has been scheduled out before as the B-only prefix *)
   665 apply (case_tac "x:act B")
   666 apply fast
   667 
   668 (* case x~:A & x~:B  *)
   669 (* cannot occur because of assumption: Forall (a:ext A | a:ext B) *)
   670 apply (rotate_tac -9)
   671 (* reduce forall assumption from tr to (x>>rs) *)
   672 apply (simp add: externals_of_par)
   673 apply (fast intro!: ext_is_act)
   674 
   675 done
   676 
   677 
   678 
   679 subsection" Filter of mksch(tr,schA,schB) to B is schB -- take lemma proof"
   680 
   681 lemma FilterBmksch_is_schB: "!! A B. [| compatible A B; compatible B A;  
   682   is_asig(asig_of A); is_asig(asig_of B) |] ==>  
   683   Forall (%x. x:ext (A||B)) tr &  
   684   Forall (%x. x:act A) schA & Forall (%x. x:act B) schB &  
   685   Filter (%a. a:ext A)$schA = Filter (%a. a:act A)$tr & 
   686   Filter (%a. a:ext B)$schB = Filter (%a. a:act B)$tr & 
   687   LastActExtsch A schA & LastActExtsch B schB   
   688   --> Filter (%a. a:act B)$(mksch A B$tr$schA$schB) = schB"
   689 apply (intro strip)
   690 apply (rule seq.take_lemma)
   691 apply (rule mp)
   692 prefer 2 apply assumption
   693 back back back back
   694 apply (rule_tac x = "schA" in spec)
   695 apply (rule_tac x = "schB" in spec)
   696 apply (rule_tac x = "tr" in spec)
   697 apply (tactic "thin_tac' 5 1")
   698 apply (rule nat_less_induct)
   699 apply (rule allI)+
   700 apply (rename_tac tr schB schA)
   701 apply (intro strip)
   702 apply (erule conjE)+
   703 
   704 apply (case_tac "Forall (%x. x:act A & x~:act B) tr")
   705 
   706 apply (rule seq_take_lemma [THEN iffD2, THEN spec])
   707 apply (tactic "thin_tac' 5 1")
   708 
   709 apply (case_tac "Finite tr")
   710 
   711 (* both sides of this equation are nil *)
   712 apply (subgoal_tac "schB=nil")
   713 apply (simp (no_asm_simp))
   714 (* first side: mksch = nil *)
   715 apply (auto intro!: ForallQFilterPnil ForallAnBmksch FiniteL_mksch)[1]
   716 (* second side: schA = nil *)
   717 apply (erule_tac A = "B" in LastActExtimplnil)
   718 apply (simp (no_asm_simp))
   719 apply (erule_tac Q = "%x. x:act A & x~:act B" in ForallQFilterPnil)
   720 apply assumption
   721 apply fast
   722 
   723 (* case ~ Finite tr *)
   724 
   725 (* both sides of this equation are UU *)
   726 apply (subgoal_tac "schB=UU")
   727 apply (simp (no_asm_simp))
   728 (* first side: mksch = UU *)
   729 apply (force intro!: ForallQFilterPUU finiteR_mksch [THEN mp, COMP rev_contrapos] ForallAnBmksch)
   730 (* schA = UU *)
   731 apply (erule_tac A = "B" in LastActExtimplUU)
   732 apply (simp (no_asm_simp))
   733 apply (erule_tac Q = "%x. x:act A & x~:act B" in ForallQFilterPUU)
   734 apply assumption
   735 apply fast
   736 
   737 (* case" ~ Forall (%x.x:act B & x~:act A) s" *)
   738 
   739 apply (drule divide_Seq3)
   740 
   741 apply (erule exE)+
   742 apply (erule conjE)+
   743 apply hypsubst
   744 
   745 (* bring in lemma reduceB_mksch *)
   746 apply (frule_tac y = "schB" and x = "schA" and A = "A" and B = "B" in reduceB_mksch)
   747 apply assumption+
   748 apply (erule exE)+
   749 apply (erule conjE)+
   750 
   751 (* use reduceB_mksch to rewrite conclusion *)
   752 apply hypsubst
   753 apply simp
   754 
   755 (* eliminate the A-only prefix *)
   756 
   757 apply (subgoal_tac "(Filter (%a. a :act B) $x1) = nil")
   758 apply (erule_tac [2] ForallQFilterPnil)
   759 prefer 2 apply (assumption)
   760 prefer 2 apply (fast)
   761 
   762 (* Now real recursive step follows (in x) *)
   763 
   764 apply simp
   765 apply (case_tac "x:act B")
   766 apply (case_tac "x~:act A")
   767 apply (rotate_tac -2)
   768 apply simp
   769 
   770 apply (subgoal_tac "Filter (%a. a:act B & a:ext A) $x1=nil")
   771 apply (rotate_tac -1)
   772 apply simp
   773 (* eliminate introduced subgoal 2 *)
   774 apply (erule_tac [2] ForallQFilterPnil)
   775 prefer 2 apply (assumption)
   776 prefer 2 apply (fast)
   777 
   778 (* bring in divide Seq for s *)
   779 apply (frule sym [THEN antisym_less_inverse, THEN conjunct1, THEN divide_Seq])
   780 apply (erule conjE)+
   781 
   782 (* subst divide_Seq in conclusion, but only at the righest occurence *)
   783 apply (rule_tac t = "schB" in ssubst)
   784 back
   785 back
   786 back
   787 apply assumption
   788 
   789 (* reduce trace_takes from n to strictly smaller k *)
   790 apply (rule take_reduction)
   791 
   792 (* f B (tw iB) = tw ~eB *)
   793 apply (simp add: int_is_act not_ext_is_int_or_not_act)
   794 apply (rule refl)
   795 apply (simp add: int_is_act not_ext_is_int_or_not_act)
   796 apply (rotate_tac -11)
   797 
   798 (* now conclusion fulfills induction hypothesis, but assumptions are not ready *)
   799 
   800 (* assumption schA *)
   801 apply (simp add: ext_and_act)
   802 (* assumption schB *)
   803 apply (drule_tac x = "schB" and g = "Filter (%a. a:act B) $rs" in subst_lemma2)
   804 apply assumption
   805 apply (simp add: int_is_not_ext)
   806 (* assumptions concerning LastActExtsch, cannot be rewritten, as LastActExtsmalli are looping  *)
   807 apply (drule_tac sch = "schB" and P = "%a. a:int B" in LastActExtsmall1)
   808 apply (frule_tac ?sch1.0 = "x1" in LastActExtsmall2)
   809 apply assumption
   810 
   811 (* assumption Forall schB *)
   812 apply (drule_tac s = "schB" and P = "Forall (%x. x:act B) " in subst)
   813 apply assumption
   814 apply (simp add: int_is_act)
   815 
   816 (* case x:actions(asig_of A) & x: actions(asig_of B) *)
   817 
   818 apply (rotate_tac -2)
   819 apply simp
   820 
   821 apply (subgoal_tac "Filter (%a. a:act B & a:ext A) $x1=nil")
   822 apply (rotate_tac -1)
   823 apply simp
   824 (* eliminate introduced subgoal 2 *)
   825 apply (erule_tac [2] ForallQFilterPnil)
   826 prefer 2 apply (assumption)
   827 prefer 2 apply (fast)
   828 
   829 (* bring in divide Seq for s *)
   830 apply (frule sym [THEN antisym_less_inverse, THEN conjunct1, THEN divide_Seq])
   831 apply (erule conjE)+
   832 
   833 (* subst divide_Seq in conclusion, but only at the righest occurence *)
   834 apply (rule_tac t = "schB" in ssubst)
   835 back
   836 back
   837 back
   838 apply assumption
   839 
   840 (* f B (tw iB) = tw ~eB *)
   841 apply (simp add: int_is_act not_ext_is_int_or_not_act)
   842 
   843 (* rewrite assumption forall and schB *)
   844 apply (rotate_tac 13)
   845 apply (simp add: ext_and_act)
   846 
   847 (* divide_Seq for schB2 *)
   848 apply (frule_tac y = "x2" in sym [THEN antisym_less_inverse, THEN conjunct1, THEN divide_Seq])
   849 apply (erule conjE)+
   850 (* assumption schA *)
   851 apply (drule_tac x = "schB" and g = "Filter (%a. a:act B) $rs" in subst_lemma2)
   852 apply assumption
   853 apply (simp add: int_is_not_ext)
   854 
   855 (* f B (tw iA schA2) = nil *)
   856 apply (simp add: int_is_not_ext not_ext_is_int_or_not_act intA_is_not_actB)
   857 
   858 
   859 (* reduce trace_takes from n to strictly smaller k *)
   860 apply (rule take_reduction)
   861 apply (rule refl)
   862 apply (rule refl)
   863 
   864 (* now conclusion fulfills induction hypothesis, but assumptions are not all ready *)
   865 
   866 (* assumption schA *)
   867 apply (drule_tac x = "x2" and g = "Filter (%a. a:act A) $rs" in subst_lemma2)
   868 apply assumption
   869 apply (simp add: intA_is_not_actB int_is_not_ext)
   870 
   871 (* conclusions concerning LastActExtsch, cannot be rewritten, as LastActExtsmalli are looping  *)
   872 apply (drule_tac sch = "schB" and P = "%a. a:int B" in LastActExtsmall1)
   873 apply (frule_tac ?sch1.0 = "x1" in LastActExtsmall2)
   874 apply assumption
   875 apply (drule_tac sch = "x2" and P = "%a. a:int A" in LastActExtsmall1)
   876 
   877 (* assumption Forall schA, and Forall schA are performed by ForallTL,ForallDropwhile *)
   878 apply (simp add: ForallTL ForallDropwhile)
   879 
   880 (* case x~:B & x:A  *)
   881 (* cannot occur, as just this case has been scheduled out before as the B-only prefix *)
   882 apply (case_tac "x:act A")
   883 apply fast
   884 
   885 (* case x~:B & x~:A  *)
   886 (* cannot occur because of assumption: Forall (a:ext A | a:ext B) *)
   887 apply (rotate_tac -9)
   888 (* reduce forall assumption from tr to (x>>rs) *)
   889 apply (simp add: externals_of_par)
   890 apply (fast intro!: ext_is_act)
   891 
   892 done
   893 
   894 
   895 subsection "COMPOSITIONALITY on TRACE Level -- Main Theorem"
   896 
   897 lemma compositionality_tr: 
   898 "!! A B. [| is_trans_of A; is_trans_of B; compatible A B; compatible B A;  
   899             is_asig(asig_of A); is_asig(asig_of B)|]  
   900         ==>  (tr: traces(A||B)) =  
   901              (Filter (%a. a:act A)$tr : traces A & 
   902               Filter (%a. a:act B)$tr : traces B & 
   903               Forall (%x. x:ext(A||B)) tr)"
   904 
   905 apply (simp (no_asm) add: traces_def has_trace_def)
   906 apply auto
   907 
   908 (* ==> *)
   909 (* There is a schedule of A *)
   910 apply (rule_tac x = "Filter (%a. a:act A) $sch" in bexI)
   911 prefer 2
   912 apply (simp add: compositionality_sch)
   913 apply (simp add: compatibility_consequence1 externals_of_par ext1_ext2_is_not_act1)
   914 (* There is a schedule of B *)
   915 apply (rule_tac x = "Filter (%a. a:act B) $sch" in bexI)
   916 prefer 2
   917 apply (simp add: compositionality_sch)
   918 apply (simp add: compatibility_consequence2 externals_of_par ext1_ext2_is_not_act2)
   919 (* Traces of A||B have only external actions from A or B *)
   920 apply (rule ForallPFilterP)
   921 
   922 (* <== *)
   923 
   924 (* replace schA and schB by Cut(schA) and Cut(schB) *)
   925 apply (drule exists_LastActExtsch)
   926 apply assumption
   927 apply (drule exists_LastActExtsch)
   928 apply assumption
   929 apply (erule exE)+
   930 apply (erule conjE)+
   931 (* Schedules of A(B) have only actions of A(B) *)
   932 apply (drule scheds_in_sig)
   933 apply assumption
   934 apply (drule scheds_in_sig)
   935 apply assumption
   936 
   937 apply (rename_tac h1 h2 schA schB)
   938 (* mksch is exactly the construction of trA||B out of schA, schB, and the oracle tr,
   939    we need here *)
   940 apply (rule_tac x = "mksch A B$tr$schA$schB" in bexI)
   941 
   942 (* External actions of mksch are just the oracle *)
   943 apply (simp add: FilterA_mksch_is_tr)
   944 
   945 (* mksch is a schedule -- use compositionality on sch-level *)
   946 apply (simp add: compositionality_sch)
   947 apply (simp add: FilterAmksch_is_schA FilterBmksch_is_schB)
   948 apply (erule ForallAorB_mksch)
   949 apply (erule ForallPForallQ)
   950 apply (erule ext_is_act)
   951 done
   952 
   953 
   954 
   955 subsection {* COMPOSITIONALITY on TRACE Level -- for Modules *}
   956 
   957 lemma compositionality_tr_modules: 
   958 
   959 "!! A B. [| is_trans_of A; is_trans_of B; compatible A B; compatible B A;  
   960             is_asig(asig_of A); is_asig(asig_of B)|]  
   961  ==> Traces (A||B) = par_traces (Traces A) (Traces B)"
   962 
   963 apply (unfold Traces_def par_traces_def)
   964 apply (simp add: asig_of_par)
   965 apply (rule set_ext)
   966 apply (simp add: compositionality_tr externals_of_par)
   967 done
   968 
   969 
   970 declaration {* fn _ => Simplifier.map_ss (fn ss => ss setmksym (SOME o symmetric_fun)) *}
   971 
   972 
   973 end