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