src/HOLCF/IOA/meta_theory/CompoExecs.thy
author mueller
Thu Jul 17 12:43:32 1997 +0200 (1997-07-17)
changeset 3521 bdc51b4c6050
parent 3275 3f53f2c876f4
child 3842 b55686a7b22c
permissions -rw-r--r--
changes needed for adding fairness
mueller@3071
     1
(*  Title:      HOLCF/IOA/meta_theory/CompoExecs.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 Execution level.
mueller@3071
     7
*)  
mueller@3071
     8
mueller@3071
     9
CompoExecs = Traces + 
mueller@3071
    10
mueller@3071
    11
mueller@3071
    12
consts 
mueller@3071
    13
mueller@3071
    14
 ProjA      ::"('a,'s * 't)execution => ('a,'s)execution"
mueller@3071
    15
 ProjA2     ::"('a,'s * 't)pairs     -> ('a,'s)pairs"
mueller@3071
    16
 ProjB      ::"('a,'s * 't)execution => ('a,'t)execution"
mueller@3071
    17
 ProjB2     ::"('a,'s * 't)pairs     -> ('a,'t)pairs"
mueller@3521
    18
 Filter_ex  ::"'a signature => ('a,'s)execution => ('a,'s)execution"
mueller@3521
    19
 Filter_ex2 ::"'a signature => ('a,'s)pairs     -> ('a,'s)pairs" 
mueller@3521
    20
 stutter    ::"'a signature => ('a,'s)execution => bool" 
mueller@3521
    21
 stutter2   ::"'a signature => ('a,'s)pairs     -> ('s => tr)"
mueller@3521
    22
mueller@3521
    23
 par_execs  ::"[('a,'s)execution_module,('a,'t)execution_module] => ('a,'s*'t)execution_module"
mueller@3071
    24
mueller@3071
    25
mueller@3071
    26
defs 
mueller@3071
    27
mueller@3071
    28
mueller@3071
    29
ProjA_def
mueller@3071
    30
 "ProjA ex == (fst (fst ex), ProjA2`(snd ex))" 
mueller@3071
    31
mueller@3071
    32
ProjB_def
mueller@3071
    33
 "ProjB ex == (snd (fst ex), ProjB2`(snd ex))" 
mueller@3071
    34
mueller@3071
    35
mueller@3071
    36
ProjA2_def
mueller@3071
    37
  "ProjA2 == Map (%x.(fst x,fst(snd x)))"
mueller@3071
    38
mueller@3071
    39
ProjB2_def
mueller@3071
    40
  "ProjB2 == Map (%x.(fst x,snd(snd x)))"
mueller@3071
    41
 
mueller@3071
    42
mueller@3071
    43
Filter_ex_def
mueller@3521
    44
  "Filter_ex sig ex == (fst ex,Filter_ex2 sig`(snd ex))"
mueller@3071
    45
mueller@3071
    46
mueller@3071
    47
Filter_ex2_def
mueller@3521
    48
  "Filter_ex2 sig ==  Filter (%x.fst x:actions sig)"
mueller@3071
    49
mueller@3071
    50
stutter_def
mueller@3521
    51
  "stutter sig ex == ((stutter2 sig`(snd ex)) (fst ex) ~= FF)"
mueller@3071
    52
mueller@3071
    53
stutter2_def
mueller@3521
    54
  "stutter2 sig ==(fix`(LAM h ex. (%s. case ex of 
mueller@3071
    55
      nil => TT
mueller@3071
    56
    | x##xs => (flift1 
mueller@3521
    57
            (%p.(If Def ((fst p)~:actions sig)
mueller@3071
    58
                 then Def (s=(snd p)) 
mueller@3071
    59
                 else TT fi)
mueller@3071
    60
                andalso (h`xs) (snd p)) 
mueller@3071
    61
             `x)
mueller@3071
    62
   )))" 
mueller@3071
    63
mueller@3521
    64
par_execs_def
mueller@3521
    65
  "par_execs ExecsA ExecsB == 
mueller@3521
    66
       let exA = fst ExecsA; sigA = snd ExecsA; 
mueller@3521
    67
           exB = fst ExecsB; sigB = snd ExecsB       
mueller@3521
    68
       in
mueller@3521
    69
       (    {ex. Filter_ex sigA (ProjA ex) : exA}
mueller@3521
    70
        Int {ex. Filter_ex sigB (ProjB ex) : exB}
mueller@3521
    71
        Int {ex. stutter sigA (ProjA ex)}
mueller@3521
    72
        Int {ex. stutter sigB (ProjB ex)}
mueller@3521
    73
        Int {ex. Forall (%x.fst x:(actions sigA Un actions sigB)) (snd ex)},
mueller@3521
    74
        asig_comp sigA sigB)"
mueller@3071
    75
mueller@3071
    76
end