# Theory CompoScheds

Up to index of Isabelle/HOLCF/IOA

theory CompoScheds
imports CompoExecs
uses [CompoScheds.ML]
begin

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

    header {* Compositionality on Schedule level *}

    theory CompoScheds
    imports CompoExecs
    begin

    consts

     mkex     ::"('a,'s)ioa => ('a,'t)ioa => 'a Seq =>
                  ('a,'s)execution => ('a,'t)execution =>('a,'s*'t)execution"
     mkex2    ::"('a,'s)ioa => ('a,'t)ioa => 'a Seq ->
                  ('a,'s)pairs -> ('a,'t)pairs ->
                  ('s => 't => ('a,'s*'t)pairs)"
     par_scheds ::"['a schedule_module,'a schedule_module] => 'a schedule_module"

    defs

    mkex_def:
      "mkex A B sch exA exB ==
           ((fst exA,fst exB),
            (mkex2 A B$sch$(snd exA)$(snd exB)) (fst exA) (fst exB))"

    mkex2_def:
      "mkex2 A B == (fix$(LAM h sch exA exB. (%s t. case sch of
           nil => nil
        | x##xs =>
          (case x of
            UU => UU
          | Def y =>
             (if y:act A then
                 (if y:act B then
                    (case HD$exA of
                       UU => UU
                     | Def a => (case HD$exB of
                                  UU => UU
                                | Def b =>
                       (y,(snd a,snd b))>>
                         (h$xs$(TL$exA)$(TL$exB)) (snd a) (snd b)))
                  else
                    (case HD$exA of
                       UU => UU
                     | Def a =>
                       (y,(snd a,t))>>(h$xs$(TL$exA)$exB) (snd a) t)
                  )
              else
                 (if y:act B then
                    (case HD$exB of
                       UU => UU
                     | Def b =>
                       (y,(s,snd b))>>(h$xs$exA$(TL$exB)) s (snd b))
                 else
                   UU
                 )
             )
           ))))"

    par_scheds_def:
      "par_scheds SchedsA SchedsB ==
           let schA = fst SchedsA; sigA = snd SchedsA;
               schB = fst SchedsB; sigB = snd SchedsB
           in
           (    {sch. Filter (%a. a:actions sigA)$sch : schA}
            Int {sch. Filter (%a. a:actions sigB)$sch : schB}
            Int {sch. Forall (%x. x:(actions sigA Un actions sigB)) sch},
            asig_comp sigA sigB)"

    ML {* use_legacy_bindings (the_context ()) *}

    end

## mkex rewrite rules

theorem mkex2_unfold:

      mkex2 A B =
      (LAM sch exA exB.
          (%s t. case sch of nil => nil
                 | x ## xs =>
                     case x of UU => UU
                     | Def y =>
                         if y ∈ act A
                         then if y ∈ act B
                              then case HD·exA of UU => UU
                                   | Def a =>
                                       case HD·exB of UU => UU
                                       | Def b =>
                                           (y, snd a, snd b)
                                           >>(mkex2 A B·xs·(TL·exA)·(TL·exB)) (snd a)
      (snd b)
                              else case HD·exA of UU => UU
                                   | Def a =>
                                       (y, snd a, t)
                                       >>(mkex2 A B·xs·(TL·exA)·exB) (snd a) t
                         else if y ∈ act B
                              then case HD·exB of UU => UU
                                   | Def b =>
                                       (y, s, snd b)
                                       >>(mkex2 A B·xs·exA·(TL·exB)) s (snd b)
                              else UU))

theorem mkex2_UU:

      (mkex2 A B·UU·exA·exB) s t = UU

theorem mkex2_nil:

      (mkex2 A B·nil·exA·exB) s t = nil

theorem mkex2_cons_1:

      [| x ∈ act A; x ∉ act B; HD·exA = Def a |]
      ==> (mkex2 A B·(x>>sch)·exA·exB) s t =
          (x, snd a, t)>>(mkex2 A B·sch·(TL·exA)·exB) (snd a) t

theorem mkex2_cons_2:

      [| x ∉ act A; x ∈ act B; HD·exB = Def b |]
      ==> (mkex2 A B·(x>>sch)·exA·exB) s t =
          (x, s, snd b)>>(mkex2 A B·sch·exA·(TL·exB)) s (snd b)

theorem mkex2_cons_3:

      [| x ∈ act A; x ∈ act B; HD·exA = Def a; HD·exB = Def b |]
      ==> (mkex2 A B·(x>>sch)·exA·exB) s t =
          (x, snd a, snd b)>>(mkex2 A B·sch·(TL·exA)·(TL·exB)) (snd a) (snd b)

theorem mkex_UU:

      mkex A B UU (s, exA) (t, exB) = ((s, t), UU)

theorem mkex_nil:

      mkex A B nil (s, exA) (t, exB) = ((s, t), nil)

theorem mkex_cons_1:

      [| x ∈ act A; x ∉ act B |]
      ==> mkex A B (x>>sch) (s, a>>exA) (t, exB) =
          ((s, t), (x, snd a, t)>>snd (mkex A B sch (snd a, exA) (t, exB)))

theorem mkex_cons_2:

      [| x ∉ act A; x ∈ act B |]
      ==> mkex A B (x>>sch) (s, exA) (t, b>>exB) =
          ((s, t), (x, s, snd b)>>snd (mkex A B sch (s, exA) (snd b, exB)))

theorem mkex_cons_3:

      [| x ∈ act A; x ∈ act B |]
      ==> mkex A B (x>>sch) (s, a>>exA) (t, b>>exB) =
          ((s, t), (x, snd a, snd b)>>snd (mkex A B sch (snd a, exA) (snd b, exB)))

## Lemmas for ==>

theorem lemma_2_1a:

      filter_act·(Filter_ex2 (asig_of A)·xs) = Filter (%a. a ∈ act A)·(filter_act·xs)

theorem lemma_2_1b:

      filter_act·(ProjA2·xs) = filter_act·xs ∧ filter_act·(ProjB2·xs) = filter_act·xs

theorem sch_actions_in_AorB:

      ∀s. is_exec_frag (A || B) (s, xs) -->
          Forall (%x. x ∈ act (A || B)) (filter_act·xs)

## Lemmas for <==

theorem Mapfst_mkex_is_sch:

      ∀exA exB s t.
         Forall (%x. x ∈ act (A || B)) sch ∧
         Filter (%a. a ∈ act A)·sch << filter_act·exA ∧
         Filter (%a. a ∈ act B)·sch << filter_act·exB -->
         filter_act·(snd (mkex A B sch (s, exA) (t, exB))) = sch

theorem stutterA_mkex:

      ∀exA exB s t.
         Forall (%x. x ∈ act (A || B)) sch ∧
         Filter (%a. a ∈ act A)·sch << filter_act·exA ∧
         Filter (%a. a ∈ act B)·sch << filter_act·exB -->
         stutter (asig_of A) (s, ProjA2·(snd (mkex A B sch (s, exA) (t, exB))))

theorem stutter_mkex_on_A:

      [| Forall (%x. x ∈ act (A || B)) sch;
         Filter (%a. a ∈ act A)·sch << filter_act·(snd exA);
         Filter (%a. a ∈ act B)·sch << filter_act·(snd exB) |]
      ==> stutter (asig_of A) (ProjA (mkex A B sch exA exB))

theorem stutterB_mkex:

      ∀exA exB s t.
         Forall (%x. x ∈ act (A || B)) sch ∧
         Filter (%a. a ∈ act A)·sch << filter_act·exA ∧
         Filter (%a. a ∈ act B)·sch << filter_act·exB -->
         stutter (asig_of B) (t, ProjB2·(snd (mkex A B sch (s, exA) (t, exB))))

theorem stutter_mkex_on_B:

      [| Forall (%x. x ∈ act (A || B)) sch;
         Filter (%a. a ∈ act A)·sch << filter_act·(snd exA);
         Filter (%a. a ∈ act B)·sch << filter_act·(snd exB) |]
      ==> stutter (asig_of B) (ProjB (mkex A B sch exA exB))

theorem filter_mkex_is_exA_tmp:

      ∀exA exB s t.
         Forall (%x. x ∈ act (A || B)) sch ∧
         Filter (%a. a ∈ act A)·sch << filter_act·exA ∧
         Filter (%a. a ∈ act B)·sch << filter_act·exB -->
         Filter_ex2 (asig_of A)·(ProjA2·(snd (mkex A B sch (s, exA) (t, exB)))) =
         Zip·(Filter (%a. a ∈ act A)·sch)·(Map snd·exA)

theorem Zip_Map_fst_snd:

      Zip·(Map fst·y)·(Map snd·y) = y

theorem trick_against_eq_in_ass:

      Filter (%a. a ∈ act AB)·sch = filter_act·ex
      ==> ex = Zip·(Filter (%a. a ∈ act AB)·sch)·(Map snd·ex)

theorem filter_mkex_is_exA:

      [| Forall (%a. a ∈ act (A || B)) sch;
         Filter (%a. a ∈ act A)·sch = filter_act·(snd exA);
         Filter (%a. a ∈ act B)·sch = filter_act·(snd exB) |]
      ==> Filter_ex (asig_of A) (ProjA (mkex A B sch exA exB)) = exA

theorem filter_mkex_is_exB_tmp:

      ∀exA exB s t.
         Forall (%x. x ∈ act (A || B)) sch ∧
         Filter (%a. a ∈ act A)·sch << filter_act·exA ∧
         Filter (%a. a ∈ act B)·sch << filter_act·exB -->
         Filter_ex2 (asig_of B)·(ProjB2·(snd (mkex A B sch (s, exA) (t, exB)))) =
         Zip·(Filter (%a. a ∈ act B)·sch)·(Map snd·exB)

theorem filter_mkex_is_exB:

      [| Forall (%a. a ∈ act (A || B)) sch;
         Filter (%a. a ∈ act A)·sch = filter_act·(snd exA);
         Filter (%a. a ∈ act B)·sch = filter_act·(snd exB) |]
      ==> Filter_ex (asig_of B) (ProjB (mkex A B sch exA exB)) = exB

theorem mkex_actions_in_AorB:

      ∀s t exA exB.
         Forall (%x. x ∈ act (A || B)) sch ∧
         Filter (%a. a ∈ act A)·sch << filter_act·exA ∧
         Filter (%a. a ∈ act B)·sch << filter_act·exB -->
         Forall (%x. fst x ∈ act (A || B)) (snd (mkex A B sch (s, exA) (t, exB)))

theorem compositionality_sch:

      (sch ∈ schedules (A || B)) =
      (Filter (%a. a ∈ act A)·sch ∈ schedules A ∧
       Filter (%a. a ∈ act B)·sch ∈ schedules B ∧ Forall (%x. x ∈ act (A || B)) sch)

theorem compositionality_sch_modules:

      Scheds (A || B) = par_scheds (Scheds A) (Scheds B)