src/HOLCF/IOA/meta_theory/Compositionality.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/Compositionality.thy
mueller@3071
     2
    ID:        
mueller@3071
     3
    Author:     Olaf M"uller
mueller@3071
     4
    Copyright   1997  TU Muenchen
mueller@3071
     5
mueller@3071
     6
Compositionality of I/O automata
mueller@3071
     7
*) 
mueller@3071
     8
mueller@3071
     9
Compositionality = CompoTraces + 
mueller@3071
    10
mueller@3071
    11
rules 
mueller@3071
    12
mueller@3071
    13
compotraces
mueller@3071
    14
"[| compat_ioas A B; compat_ioas B A; 
mueller@3071
    15
    is_asig(asig_of A); is_asig(asig_of B)|] 
mueller@3071
    16
 ==> traces(A||B) = 
mueller@3071
    17
     {tr. (Filter (%a.a:act A)`tr : traces A &
mueller@3071
    18
      Filter (%a.a:act B)`tr : traces B &
mueller@3071
    19
      Forall (%x. x:ext(A||B)) tr)}"
mueller@3071
    20
mueller@3071
    21
end