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;
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),
nipkow@10835
    29
        (mkex2 A B$sch$(snd exA)$(snd exB)) (fst exA) (fst exB))"
mueller@3071
    30
mueller@3071
    31
mkex2_def
nipkow@10835
    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 
wenzelm@12028
    36
        UU => UU
mueller@3071
    37
      | Def y => 
mueller@3071
    38
         (if y:act A then 
mueller@3071
    39
             (if y:act B then 
nipkow@10835
    40
                (case HD$exA of
wenzelm@12028
    41
                   UU => UU
nipkow@10835
    42
                 | Def a => (case HD$exB of
wenzelm@12028
    43
                              UU => UU
mueller@3071
    44
                            | Def b => 
mueller@3071
    45
                   (y,(snd a,snd b))>>
nipkow@10835
    46
                     (h$xs$(TL$exA)$(TL$exB)) (snd a) (snd b)))
mueller@3071
    47
              else
nipkow@10835
    48
                (case HD$exA of
wenzelm@12028
    49
                   UU => UU
mueller@3071
    50
                 | Def a => 
nipkow@10835
    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 
nipkow@10835
    55
                (case HD$exB of
wenzelm@12028
    56
                   UU => UU
mueller@3071
    57
                 | Def b => 
nipkow@10835
    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
nipkow@10835
    70
       (    {sch. Filter (%a. a:actions sigA)$sch : schA}
nipkow@10835
    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