src/HOLCF/IOA/meta_theory/CompoScheds.thy
author wenzelm
Sat Nov 03 01:39:17 2001 +0100 (2001-11-03)
changeset 12028 52aa183c15bb
parent 10835 f4745d77e620
child 12218 6597093b77e7
permissions -rw-r--r--
replaced Undef by UU;
     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  par_scheds ::"['a schedule_module,'a schedule_module] => 'a schedule_module"
    21 
    22 
    23 
    24 defs
    25 
    26 mkex_def  
    27   "mkex A B sch exA exB == 
    28        ((fst exA,fst exB),
    29         (mkex2 A B$sch$(snd exA)$(snd exB)) (fst exA) (fst exB))"
    30 
    31 mkex2_def
    32   "mkex2 A B == (fix$(LAM h sch exA exB. (%s t. case sch of 
    33        nil => nil
    34     | x##xs => 
    35       (case x of 
    36         UU => UU
    37       | Def y => 
    38          (if y:act A then 
    39              (if y:act B then 
    40                 (case HD$exA of
    41                    UU => UU
    42                  | Def a => (case HD$exB of
    43                               UU => UU
    44                             | Def b => 
    45                    (y,(snd a,snd b))>>
    46                      (h$xs$(TL$exA)$(TL$exB)) (snd a) (snd b)))
    47               else
    48                 (case HD$exA of
    49                    UU => UU
    50                  | Def a => 
    51                    (y,(snd a,t))>>(h$xs$(TL$exA)$exB) (snd a) t)
    52               )
    53           else 
    54              (if y:act B then 
    55                 (case HD$exB of
    56                    UU => UU
    57                  | Def b => 
    58                    (y,(s,snd b))>>(h$xs$exA$(TL$exB)) s (snd b))
    59              else
    60                UU
    61              )
    62          )
    63        ))))"
    64 
    65 par_scheds_def
    66   "par_scheds SchedsA SchedsB == 
    67        let schA = fst SchedsA; sigA = snd SchedsA; 
    68            schB = fst SchedsB; sigB = snd SchedsB       
    69        in
    70        (    {sch. Filter (%a. a:actions sigA)$sch : schA}
    71         Int {sch. Filter (%a. a:actions sigB)$sch : schB}
    72         Int {sch. Forall (%x. x:(actions sigA Un actions sigB)) sch},
    73         asig_comp sigA sigB)"
    74 
    75 end