|
1 (* Title: ZF/UNITY/Union.thy |
|
2 ID: $Id$ |
|
3 Author: Sidi O Ehmety, Computer Laboratory |
|
4 Copyright 2001 University of Cambridge |
|
5 |
|
6 Unions of programs |
|
7 |
|
8 Partly from Misra's Chapter 5: Asynchronous Compositions of Programs |
|
9 |
|
10 Theory ported form HOL.. |
|
11 |
|
12 *) |
|
13 |
|
14 Union = SubstAx + FP + |
|
15 |
|
16 constdefs |
|
17 |
|
18 (*FIXME: conjoin Init(F) Int Init(G) ~= 0 *) |
|
19 ok :: [i, i] => o (infixl 65) |
|
20 "F ok G == Acts(F) <= AllowedActs(G) & |
|
21 Acts(G) <= AllowedActs(F)" |
|
22 |
|
23 (*FIXME: conjoin (INT i:I. Init(F(i))) ~= 0 *) |
|
24 OK :: [i, i=>i] => o |
|
25 "OK(I,F) == (ALL i:I. ALL j: I-{i}. Acts(F(i)) <= AllowedActs(F(j)))" |
|
26 |
|
27 JOIN :: [i, i=>i] => i |
|
28 "JOIN(I,F) == if I = 0 then SKIP else |
|
29 mk_program(INT i:I. Init(F(i)), UN i:I. Acts(F(i)), |
|
30 INT i:I. AllowedActs(F(i)))" |
|
31 |
|
32 Join :: [i, i] => i (infixl 65) |
|
33 "F Join G == mk_program (Init(F) Int Init(G), Acts(F) Un Acts(G), |
|
34 AllowedActs(F) Int AllowedActs(G))" |
|
35 (*Characterizes safety properties. Used with specifying AllowedActs*) |
|
36 safety_prop :: "i => o" |
|
37 "safety_prop(X) == SKIP:X & |
|
38 (ALL G:program. Acts(G) <= (UN F:X. Acts(F)) --> G:X)" |
|
39 |
|
40 property :: i |
|
41 "property == Pow(program)" |
|
42 |
|
43 |
|
44 syntax |
|
45 "@JOIN1" :: [pttrns, i] => i ("(3JN _./ _)" 10) |
|
46 "@JOIN" :: [pttrn, i, i] => i ("(3JN _:_./ _)" 10) |
|
47 |
|
48 translations |
|
49 "JN x:A. B" == "JOIN(A, (%x. B))" |
|
50 "JN x y. B" == "JN x. JN y. B" |
|
51 "JN x. B" == "JOIN(state,(%x. B))" |
|
52 |
|
53 syntax (symbols) |
|
54 SKIP :: i ("\\<bottom>") |
|
55 "op Join" :: [i, i] => i (infixl "\\<squnion>" 65) |
|
56 "@JOIN1" :: [pttrns, i] => i ("(3\\<Squnion> _./ _)" 10) |
|
57 "@JOIN" :: [pttrn, i, i] => i ("(3\\<Squnion> _:_./ _)" 10) |
|
58 |
|
59 end |