src/HOLCF/IOA/meta_theory/CompoScheds.thy
author mueller
Wed May 21 15:08:52 1997 +0200 (1997-05-21)
changeset 3275 3f53f2c876f4
parent 3071 981258186b71
child 3521 bdc51b4c6050
permissions -rw-r--r--
changes for release 94-8
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@3071
    20
mueller@3071
    21
mueller@3071
    22
defs
mueller@3071
    23
mueller@3071
    24
mkex_def  
mueller@3071
    25
  "mkex A B sch exA exB == 
mueller@3071
    26
       ((fst exA,fst exB),
mueller@3071
    27
        (mkex2 A B`sch`(snd exA)`(snd exB)) (fst exA) (fst exB))"
mueller@3071
    28
mueller@3071
    29
mkex2_def
mueller@3071
    30
  "mkex2 A B == (fix`(LAM h sch exA exB. (%s t. case sch of 
mueller@3071
    31
       nil => nil
mueller@3071
    32
    | x##xs => 
mueller@3071
    33
      (case x of 
mueller@3071
    34
        Undef => UU
mueller@3071
    35
      | Def y => 
mueller@3071
    36
         (if y:act A then 
mueller@3071
    37
             (if y:act B then 
mueller@3071
    38
                (case HD`exA of
mueller@3071
    39
                   Undef => UU
mueller@3071
    40
                 | Def a => (case HD`exB of
mueller@3071
    41
                              Undef => UU
mueller@3071
    42
                            | Def b => 
mueller@3071
    43
                   (y,(snd a,snd b))>>
mueller@3071
    44
                     (h`xs`(TL`exA)`(TL`exB)) (snd a) (snd b)))
mueller@3071
    45
              else
mueller@3071
    46
                (case HD`exA of
mueller@3071
    47
                   Undef => UU
mueller@3071
    48
                 | Def a => 
mueller@3071
    49
                   (y,(snd a,t))>>(h`xs`(TL`exA)`exB) (snd a) t)
mueller@3071
    50
              )
mueller@3071
    51
          else 
mueller@3071
    52
             (if y:act B then 
mueller@3071
    53
                (case HD`exB of
mueller@3071
    54
                   Undef => UU
mueller@3071
    55
                 | Def b => 
mueller@3071
    56
                   (y,(s,snd b))>>(h`xs`exA`(TL`exB)) s (snd b))
mueller@3071
    57
             else
mueller@3071
    58
               UU
mueller@3071
    59
             )
mueller@3071
    60
         )
mueller@3071
    61
       ))))"
mueller@3071
    62
mueller@3071
    63
end