src/HOLCF/IOA/meta_theory/CompoTraces.thy
author nipkow
Tue Jan 09 15:36:30 2001 +0100 (2001-01-09)
changeset 10835 f4745d77e620
parent 3842 b55686a7b22c
child 12028 52aa183c15bb
permissions -rw-r--r--
` -> $
     1 (*  Title:      HOLCF/IOA/meta_theory/CompoTraces.thy
     2     ID:         $Id$
     3     Author:     Olaf M"uller
     4     Copyright   1996  TU Muenchen
     5 
     6 Compositionality on Trace level.
     7 *) 
     8 
     9 CompoTraces = CompoScheds + ShortExecutions +
    10  
    11 
    12 consts  
    13 
    14  mksch      ::"('a,'s)ioa => ('a,'t)ioa => 'a Seq -> 'a Seq -> 'a Seq -> 'a Seq" 
    15  par_traces ::"['a trace_module,'a trace_module] => 'a trace_module"
    16 
    17 defs
    18 
    19 mksch_def
    20   "mksch A B == (fix$(LAM h tr schA schB. case tr of 
    21        nil => nil
    22     | x##xs => 
    23       (case x of 
    24         Undef => UU
    25       | Def y => 
    26          (if y:act A then 
    27              (if y:act B then 
    28                    ((Takewhile (%a. a:int A)$schA)
    29                       @@ (Takewhile (%a. a:int B)$schB)
    30                            @@ (y>>(h$xs
    31                                     $(TL$(Dropwhile (%a. a:int A)$schA))
    32                                     $(TL$(Dropwhile (%a. a:int B)$schB))
    33                     )))
    34               else
    35                  ((Takewhile (%a. a:int A)$schA)
    36                   @@ (y>>(h$xs
    37                            $(TL$(Dropwhile (%a. a:int A)$schA))
    38                            $schB)))
    39               )
    40           else 
    41              (if y:act B then 
    42                  ((Takewhile (%a. a:int B)$schB)
    43                      @@ (y>>(h$xs
    44                               $schA
    45                               $(TL$(Dropwhile (%a. a:int B)$schB))
    46                               )))
    47              else
    48                UU
    49              )
    50          )
    51        )))"
    52 
    53 
    54 par_traces_def
    55   "par_traces TracesA TracesB == 
    56        let trA = fst TracesA; sigA = snd TracesA; 
    57            trB = fst TracesB; sigB = snd TracesB       
    58        in
    59        (    {tr. Filter (%a. a:actions sigA)$tr : trA}
    60         Int {tr. Filter (%a. a:actions sigB)$tr : trB}
    61         Int {tr. Forall (%x. x:(externals sigA Un externals sigB)) tr},
    62         asig_comp sigA sigB)"
    63 
    64 rules
    65 
    66 
    67 finiteR_mksch
    68   "Finite (mksch A B$tr$x$y) --> Finite tr"
    69 
    70 
    71 
    72 end