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
     1 (*  Title:      HOLCF/IOA/meta_theory/CompoScheds.thy
     2     ID:         $Id$
     3     Author:     Olaf M"uller
     4     Copyright   1996  TU Muenchen
     5 
     6 Compositionality on Schedule level.
     7 *) 
     8 
     9 CompoScheds = CompoExecs + 
    10 
    11 
    12 
    13 consts
    14 
    15  mkex     ::"('a,'s)ioa => ('a,'t)ioa => 'a Seq =>
    16               ('a,'s)execution => ('a,'t)execution =>('a,'s*'t)execution" 
    17  mkex2    ::"('a,'s)ioa => ('a,'t)ioa => 'a Seq -> 
    18               ('a,'s)pairs -> ('a,'t)pairs -> 
    19               ('s => 't => ('a,'s*'t)pairs)"
    20 
    21 
    22 defs
    23 
    24 mkex_def  
    25   "mkex A B sch exA exB == 
    26        ((fst exA,fst exB),
    27         (mkex2 A B`sch`(snd exA)`(snd exB)) (fst exA) (fst exB))"
    28 
    29 mkex2_def
    30   "mkex2 A B == (fix`(LAM h sch exA exB. (%s t. case sch of 
    31        nil => nil
    32     | x##xs => 
    33       (case x of 
    34         Undef => UU
    35       | Def y => 
    36          (if y:act A then 
    37              (if y:act B then 
    38                 (case HD`exA of
    39                    Undef => UU
    40                  | Def a => (case HD`exB of
    41                               Undef => UU
    42                             | Def b => 
    43                    (y,(snd a,snd b))>>
    44                      (h`xs`(TL`exA)`(TL`exB)) (snd a) (snd b)))
    45               else
    46                 (case HD`exA of
    47                    Undef => UU
    48                  | Def a => 
    49                    (y,(snd a,t))>>(h`xs`(TL`exA)`exB) (snd a) t)
    50               )
    51           else 
    52              (if y:act B then 
    53                 (case HD`exB of
    54                    Undef => UU
    55                  | Def b => 
    56                    (y,(s,snd b))>>(h`xs`exA`(TL`exB)) s (snd b))
    57              else
    58                UU
    59              )
    60          )
    61        ))))"
    62 
    63 end