author | wenzelm |
Fri, 09 Nov 2001 00:09:47 +0100 | |
changeset 12114 | a8e860c86252 |
parent 11479 | 697dcaaf478f |
child 12195 | ed2893765a08 |
permissions | -rw-r--r-- |
11479 | 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 |
||
12114
a8e860c86252
eliminated old "symbols" syntax, use "xsymbols" instead;
wenzelm
parents:
11479
diff
changeset
|
53 |
syntax (xsymbols) |
11479 | 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 |