author | mueller |
Wed, 30 Apr 1997 11:20:15 +0200 | |
changeset 3071 | 981258186b71 |
child 3275 | 3f53f2c876f4 |
permissions | -rw-r--r-- |
3071 | 1 |
(* Title: HOLCF/IOA/meta_theory/Compositionality.thy |
2 |
ID: |
|
3 |
Author: Olaf M"uller |
|
4 |
Copyright 1997 TU Muenchen |
|
5 |
||
6 |
Compositionality of I/O automata |
|
7 |
*) |
|
8 |
||
9 |
Compositionality = CompoTraces + |
|
10 |
||
11 |
rules |
|
12 |
||
13 |
compotraces |
|
14 |
"[| compat_ioas A B; compat_ioas B A; |
|
15 |
is_asig(asig_of A); is_asig(asig_of B)|] |
|
16 |
==> traces(A||B) = |
|
17 |
{tr. (Filter (%a.a:act A)`tr : traces A & |
|
18 |
Filter (%a.a:act B)`tr : traces B & |
|
19 |
Forall (%x. x:ext(A||B)) tr)}" |
|
20 |
||
21 |
end |