src/HOLCF/IOA/meta_theory/CompoExecs.thy
author mueller
Wed Apr 30 11:20:15 1997 +0200 (1997-04-30)
changeset 3071 981258186b71
child 3275 3f53f2c876f4
permissions -rw-r--r--
New meta theory for IOA based on HOLCF.
mueller@3071
     1
(*  Title:      HOLCF/IOA/meta_theory/CompoExecs.thy
mueller@3071
     2
    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@3071
    18
 Filter_ex  ::"('a,'s)ioa => ('a,'s)execution => ('a,'s)execution"
mueller@3071
    19
 Filter_ex2 ::"('a,'s)ioa => ('a,'s)pairs     -> ('a,'s)pairs" 
mueller@3071
    20
 stutter    ::"('a,'s)ioa => ('a,'s)execution => bool" 
mueller@3071
    21
 stutter2   ::"('a,'s)ioa => ('a,'s)pairs     -> ('s => tr)"
mueller@3071
    22
mueller@3071
    23
mueller@3071
    24
defs 
mueller@3071
    25
mueller@3071
    26
mueller@3071
    27
ProjA_def
mueller@3071
    28
 "ProjA ex == (fst (fst ex), ProjA2`(snd ex))" 
mueller@3071
    29
mueller@3071
    30
ProjB_def
mueller@3071
    31
 "ProjB ex == (snd (fst ex), ProjB2`(snd ex))" 
mueller@3071
    32
mueller@3071
    33
mueller@3071
    34
ProjA2_def
mueller@3071
    35
  "ProjA2 == Map (%x.(fst x,fst(snd x)))"
mueller@3071
    36
mueller@3071
    37
ProjB2_def
mueller@3071
    38
  "ProjB2 == Map (%x.(fst x,snd(snd x)))"
mueller@3071
    39
 
mueller@3071
    40
mueller@3071
    41
Filter_ex_def
mueller@3071
    42
  "Filter_ex A ex == (fst ex,Filter_ex2 A`(snd ex))"
mueller@3071
    43
mueller@3071
    44
mueller@3071
    45
Filter_ex2_def
mueller@3071
    46
  "Filter_ex2 A ==  Filter (%x.fst x:act A)"
mueller@3071
    47
mueller@3071
    48
stutter_def
mueller@3071
    49
  "stutter A ex == ((stutter2 A`(snd ex)) (fst ex) ~= FF)"
mueller@3071
    50
mueller@3071
    51
stutter2_def
mueller@3071
    52
  "stutter2 A ==(fix`(LAM h ex. (%s. case ex of 
mueller@3071
    53
      nil => TT
mueller@3071
    54
    | x##xs => (flift1 
mueller@3071
    55
            (%p.(If Def ((fst p)~:act A)
mueller@3071
    56
                 then Def (s=(snd p)) 
mueller@3071
    57
                 else TT fi)
mueller@3071
    58
                andalso (h`xs) (snd p)) 
mueller@3071
    59
             `x)
mueller@3071
    60
   )))" 
mueller@3071
    61
mueller@3071
    62
mueller@3071
    63
mueller@3071
    64
mueller@3071
    65
end