# Theory CompoTraces

Up to index of Isabelle/HOLCF/IOA

theory CompoTraces
imports CompoScheds ShortExecutions
uses [CompoTraces.ML]
begin

    (*  Title:      HOLCF/IOA/meta_theory/CompoTraces.thy
        ID:         $Id: CompoTraces.thy,v 1.9 2005/09/02 15:24:00 wenzelm Exp $
        Author:     Olaf Müller
    *)

    header {* Compositionality on Trace level *}

    theory CompoTraces
    imports CompoScheds ShortExecutions
    begin

    consts

     mksch      ::"('a,'s)ioa => ('a,'t)ioa => 'a Seq -> 'a Seq -> 'a Seq -> 'a Seq"
     par_traces ::"['a trace_module,'a trace_module] => 'a trace_module"

    defs

    mksch_def:
      "mksch A B == (fix$(LAM h tr schA schB. case tr of
           nil => nil
        | x##xs =>
          (case x of
            UU => UU
          | Def y =>
             (if y:act A then
                 (if y:act B then
                       ((Takewhile (%a. a:int A)$schA)
                          @@ (Takewhile (%a. a:int B)$schB)
                               @@ (y>>(h$xs
                                        $(TL$(Dropwhile (%a. a:int A)$schA))
                                        $(TL$(Dropwhile (%a. a:int B)$schB))
                        )))
                  else
                     ((Takewhile (%a. a:int A)$schA)
                      @@ (y>>(h$xs
                               $(TL$(Dropwhile (%a. a:int A)$schA))
                               $schB)))
                  )
              else
                 (if y:act B then
                     ((Takewhile (%a. a:int B)$schB)
                         @@ (y>>(h$xs
                                  $schA
                                  $(TL$(Dropwhile (%a. a:int B)$schB))
                                  )))
                 else
                   UU
                 )
             )
           )))"

    par_traces_def:
      "par_traces TracesA TracesB ==
           let trA = fst TracesA; sigA = snd TracesA;
               trB = fst TracesB; sigB = snd TracesB
           in
           (    {tr. Filter (%a. a:actions sigA)$tr : trA}
            Int {tr. Filter (%a. a:actions sigB)$tr : trB}
            Int {tr. Forall (%x. x:(externals sigA Un externals sigB)) tr},
            asig_comp sigA sigB)"

    axioms

    finiteR_mksch:
      "Finite (mksch A B$tr$x$y) --> Finite tr"

    ML {* use_legacy_bindings (the_context ()) *}

    end

## mksch rewrite rules

theorem mksch_unfold:

      mksch A B =
      (LAM tr schA schB.
          case tr of nil => nil
          | x ## xs =>
              case x of UU => UU
              | Def y =>
                  if y ∈ act A
                  then if y ∈ act B
                       then Takewhile (%a. a ∈ int A)·schA @@
                            Takewhile (%a. a ∈ int B)·schB @@
                            y>>mksch A
                                B·xs·(TL·(Dropwhile
                                           (%a.
       a ∈ int A)·schA))·(TL·(Dropwhile (%a. a ∈ int B)·schB))
                       else Takewhile (%a. a ∈ int A)·schA @@
                            y>>mksch A B·xs·(TL·(Dropwhile (%a. a ∈ int A)·schA))·schB
                  else if y ∈ act B
                       then Takewhile (%a. a ∈ int B)·schB @@
                            y>>mksch A B·xs·schA·(TL·(Dropwhile (%a. a ∈ int B)·schB))
                       else UU)

theorem mksch_UU:

      mksch A B·UU·schA·schB = UU

theorem mksch_nil:

      mksch A B·nil·schA·schB = nil

theorem mksch_cons1:

      [| x ∈ act A; x ∉ act B |]
      ==> mksch A B·(x>>tr)·schA·schB =
          Takewhile (%a. a ∈ int A)·schA @@
          x>>mksch A B·tr·(TL·(Dropwhile (%a. a ∈ int A)·schA))·schB

theorem mksch_cons2:

      [| x ∉ act A; x ∈ act B |]
      ==> mksch A B·(x>>tr)·schA·schB =
          Takewhile (%a. a ∈ int B)·schB @@
          x>>mksch A B·tr·schA·(TL·(Dropwhile (%a. a ∈ int B)·schB))

theorem mksch_cons3:

      [| x ∈ act A; x ∈ act B |]
      ==> mksch A B·(x>>tr)·schA·schB =
          Takewhile (%a. a ∈ int A)·schA @@
          Takewhile (%a. a ∈ int B)·schB @@
          x>>mksch A
              B·tr·(TL·(Dropwhile
                         (%a. a ∈ int A)·schA))·(TL·(Dropwhile (%a. a ∈ int B)·schB))

## Lemmata for ==>

theorem compatibility_consequence1:

      (eB ∧ ¬ eA --> ¬ A) --> (A ∧ (eA ∨ eB)) = (eA ∧ A)

theorem compatibility_consequence2:

      (eB ∧ ¬ eA --> ¬ A) --> (A ∧ (eB ∨ eA)) = (eA ∧ A)

## Lemmata for <==

theorem subst_lemma1:

      [| f << g x; x = h x |] ==> f << g (h x)

theorem subst_lemma2:

      [| f x = y>>g; x = h x |] ==> f (h x) = y>>g

theorem ForallAorB_mksch:

      [| compatible A B; Forall (%x. x ∈ act (A || B)) tr |]
      ==> Forall (%x. x ∈ act (A || B)) (mksch A B·tr·schA·schB)

theorem ForallBnAmksch:

      [| compatible B A; Forall (%x. x ∈ act B ∧ x ∉ act A) tr |]
      ==> Forall (%x. x ∈ act B ∧ x ∉ act A) (mksch A B·tr·schA·schB)

theorem ForallAnBmksch:

      [| compatible A B; Forall (%x. x ∈ act A ∧ x ∉ act B) tr |]
      ==> Forall (%x. x ∈ act A ∧ x ∉ act B) (mksch A B·tr·schA·schB)

theorem FiniteL_mksch:

      [| Finite tr; is_asig (asig_of A); is_asig (asig_of B);
         Forall (%x. x ∈ act A) x ∧
         Forall (%x. x ∈ act B) y ∧
         Filter (%a. a ∈ ext A)·x = Filter (%a. a ∈ act A)·tr ∧
         Filter (%a. a ∈ ext B)·y = Filter (%a. a ∈ act B)·tr ∧
         Forall (%x. x ∈ ext (A || B)) tr |]
      ==> Finite (mksch A B·tr·x·y)

theorem reduceA_mksch1:

      [| Finite bs; is_asig (asig_of A); is_asig (asig_of B); compatible A B;
         Forall (%x. x ∈ act B) y ∧
         Forall (%x. x ∈ act B ∧ x ∉ act A) bs ∧
         Filter (%a. a ∈ ext B)·y = Filter (%a. a ∈ act B)·(bs @@ z) |]
      ==> ∃y1 y2.
             mksch A B·(bs @@ z)·x·y = y1 @@ mksch A B·z·x·y2 ∧
             Forall (%x. x ∈ act B ∧ x ∉ act A) y1 ∧
             Finite y1 ∧ y = y1 @@ y2 ∧ Filter (%a. a ∈ ext B)·y1 = bs

theorem reduceA_mksch:

      [| Finite bs; is_asig (asig_of A); is_asig (asig_of B); compatible A B;
         Forall (%x. x ∈ act B) y; Forall (%x. x ∈ act B ∧ x ∉ act A) bs;
         Filter (%a. a ∈ ext B)·y = Filter (%a. a ∈ act B)·(bs @@ z) |]
      ==> ∃y1 y2.
             mksch A B·(bs @@ z)·x·y = y1 @@ mksch A B·z·x·y2 ∧
             Forall (%x. x ∈ act B ∧ x ∉ act A) y1 ∧
             Finite y1 ∧ y = y1 @@ y2 ∧ Filter (%a. a ∈ ext B)·y1 = bs

theorem reduceB_mksch1:

      [| Finite as; is_asig (asig_of A); is_asig (asig_of B); compatible A B;
         Forall (%x. x ∈ act A) x ∧
         Forall (%x. x ∈ act A ∧ x ∉ act B) as ∧
         Filter (%a. a ∈ ext A)·x = Filter (%a. a ∈ act A)·(as @@ z) |]
      ==> ∃x1 x2.
             mksch A B·(as @@ z)·x·y = x1 @@ mksch A B·z·x2·y ∧
             Forall (%x. x ∈ act A ∧ x ∉ act B) x1 ∧
             Finite x1 ∧ x = x1 @@ x2 ∧ Filter (%a. a ∈ ext A)·x1 = as

theorem reduceB_mksch:

      [| Finite as; is_asig (asig_of A); is_asig (asig_of B); compatible A B;
         Forall (%x. x ∈ act A) x; Forall (%x. x ∈ act A ∧ x ∉ act B) as;
         Filter (%a. a ∈ ext A)·x = Filter (%a. a ∈ act A)·(as @@ z) |]
      ==> ∃x1 x2.
             mksch A B·(as @@ z)·x·y = x1 @@ mksch A B·z·x2·y ∧
             Forall (%x. x ∈ act A ∧ x ∉ act B) x1 ∧
             Finite x1 ∧ x = x1 @@ x2 ∧ Filter (%a. a ∈ ext A)·x1 = as

## Filtering external actions out of mksch(tr,schA,schB) yields the oracle tr

theorem FilterA_mksch_is_tr:

      [| compatible A B; compatible B A; is_asig (asig_of A); is_asig (asig_of B) |]
      ==> ∀schA schB.
             Forall (%x. x ∈ act A) schA ∧
             Forall (%x. x ∈ act B) schB ∧
             Forall (%x. x ∈ ext (A || B)) tr ∧
             Filter (%a. a ∈ act A)·tr << Filter (%a. a ∈ ext A)·schA ∧
             Filter (%a. a ∈ act B)·tr << Filter (%a. a ∈ ext B)·schB -->
             Filter (%a. a ∈ ext (A || B))·(mksch A B·tr·schA·schB) = tr

## Filter of mksch(tr,schA,schB) to A is schA -- take lemma proof

theorem FilterAmksch_is_schA:

      [| compatible A B; compatible B A; is_asig (asig_of A); is_asig (asig_of B) |]
      ==> Forall (%x. x ∈ ext (A || B)) tr ∧
          Forall (%x. x ∈ act A) schA ∧
          Forall (%x. x ∈ act B) schB ∧
          Filter (%a. a ∈ ext A)·schA = Filter (%a. a ∈ act A)·tr ∧
          Filter (%a. a ∈ ext B)·schB = Filter (%a. a ∈ act B)·tr ∧
          LastActExtsch A schA ∧ LastActExtsch B schB -->
          Filter (%a. a ∈ act A)·(mksch A B·tr·schA·schB) = schA

## Filter of mksch(tr,schA,schB) to B is schB -- take lemma proof

theorem FilterBmksch_is_schB:

      [| compatible A B; compatible B A; is_asig (asig_of A); is_asig (asig_of B) |]
      ==> Forall (%x. x ∈ ext (A || B)) tr ∧
          Forall (%x. x ∈ act A) schA ∧
          Forall (%x. x ∈ act B) schB ∧
          Filter (%a. a ∈ ext A)·schA = Filter (%a. a ∈ act A)·tr ∧
          Filter (%a. a ∈ ext B)·schB = Filter (%a. a ∈ act B)·tr ∧
          LastActExtsch A schA ∧ LastActExtsch B schB -->
          Filter (%a. a ∈ act B)·(mksch A B·tr·schA·schB) = schB

## COMPOSITIONALITY on TRACE Level -- Main Theorem

theorem compositionality_tr:

      [| is_trans_of A; is_trans_of B; compatible A B; compatible B A;
         is_asig (asig_of A); is_asig (asig_of B) |]
      ==> (tr ∈ traces (A || B)) =
          (Filter (%a. a ∈ act A)·tr ∈ traces A ∧
           Filter (%a. a ∈ act B)·tr ∈ traces B ∧ Forall (%x. x ∈ ext (A || B)) tr)

theorem compositionality_tr_modules:

      [| is_trans_of A; is_trans_of B; compatible A B; compatible B A;
         is_asig (asig_of A); is_asig (asig_of B) |]
      ==> Traces (A || B) = par_traces (Traces A) (Traces B)