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