src/HOLCF/IOA/meta_theory/CompoScheds.thy
author mueller
Thu Jul 17 12:43:32 1997 +0200 (1997-07-17)
changeset 3521 bdc51b4c6050
parent 3275 3f53f2c876f4
child 3842 b55686a7b22c
permissions -rw-r--r--
changes needed for adding fairness
mueller@3071
     1
(*  Title:      HOLCF/IOA/meta_theory/CompoScheds.thy
mueller@3275
     2
    ID:         $Id$
mueller@3071
     3
    Author:     Olaf M"uller
mueller@3071
     4
    Copyright   1996  TU Muenchen
mueller@3071
     5
mueller@3071
     6
Compositionality on Schedule level.
mueller@3071
     7
*) 
mueller@3071
     8
mueller@3071
     9
CompoScheds = CompoExecs + 
mueller@3071
    10
mueller@3071
    11
mueller@3071
    12
mueller@3071
    13
consts
mueller@3071
    14
mueller@3071
    15
 mkex     ::"('a,'s)ioa => ('a,'t)ioa => 'a Seq =>
mueller@3071
    16
              ('a,'s)execution => ('a,'t)execution =>('a,'s*'t)execution" 
mueller@3071
    17
 mkex2    ::"('a,'s)ioa => ('a,'t)ioa => 'a Seq -> 
mueller@3071
    18
              ('a,'s)pairs -> ('a,'t)pairs -> 
mueller@3071
    19
              ('s => 't => ('a,'s*'t)pairs)"
mueller@3521
    20
 par_scheds ::"['a schedule_module,'a schedule_module] => 'a schedule_module"
mueller@3521
    21
mueller@3071
    22
mueller@3071
    23
mueller@3071
    24
defs
mueller@3071
    25
mueller@3071
    26
mkex_def  
mueller@3071
    27
  "mkex A B sch exA exB == 
mueller@3071
    28
       ((fst exA,fst exB),
mueller@3071
    29
        (mkex2 A B`sch`(snd exA)`(snd exB)) (fst exA) (fst exB))"
mueller@3071
    30
mueller@3071
    31
mkex2_def
mueller@3071
    32
  "mkex2 A B == (fix`(LAM h sch exA exB. (%s t. case sch of 
mueller@3071
    33
       nil => nil
mueller@3071
    34
    | x##xs => 
mueller@3071
    35
      (case x of 
mueller@3071
    36
        Undef => UU
mueller@3071
    37
      | Def y => 
mueller@3071
    38
         (if y:act A then 
mueller@3071
    39
             (if y:act B then 
mueller@3071
    40
                (case HD`exA of
mueller@3071
    41
                   Undef => UU
mueller@3071
    42
                 | Def a => (case HD`exB of
mueller@3071
    43
                              Undef => UU
mueller@3071
    44
                            | Def b => 
mueller@3071
    45
                   (y,(snd a,snd b))>>
mueller@3071
    46
                     (h`xs`(TL`exA)`(TL`exB)) (snd a) (snd b)))
mueller@3071
    47
              else
mueller@3071
    48
                (case HD`exA of
mueller@3071
    49
                   Undef => UU
mueller@3071
    50
                 | Def a => 
mueller@3071
    51
                   (y,(snd a,t))>>(h`xs`(TL`exA)`exB) (snd a) t)
mueller@3071
    52
              )
mueller@3071
    53
          else 
mueller@3071
    54
             (if y:act B then 
mueller@3071
    55
                (case HD`exB of
mueller@3071
    56
                   Undef => UU
mueller@3071
    57
                 | Def b => 
mueller@3071
    58
                   (y,(s,snd b))>>(h`xs`exA`(TL`exB)) s (snd b))
mueller@3071
    59
             else
mueller@3071
    60
               UU
mueller@3071
    61
             )
mueller@3071
    62
         )
mueller@3071
    63
       ))))"
mueller@3071
    64
mueller@3521
    65
par_scheds_def
mueller@3521
    66
  "par_scheds SchedsA SchedsB == 
mueller@3521
    67
       let schA = fst SchedsA; sigA = snd SchedsA; 
mueller@3521
    68
           schB = fst SchedsB; sigB = snd SchedsB       
mueller@3521
    69
       in
mueller@3521
    70
       (    {sch. Filter (%a.a:actions sigA)`sch : schA}
mueller@3521
    71
        Int {sch. Filter (%a.a:actions sigB)`sch : schB}
mueller@3521
    72
        Int {sch. Forall (%x. x:(actions sigA Un actions sigB)) sch},
mueller@3521
    73
        asig_comp sigA sigB)"
mueller@3521
    74
mueller@3521
    75
end