|
1 (* Title: ZF/UNITY/Comp.thy |
|
2 ID: $Id$ |
|
3 Author: Sidi O Ehmety, Computer Laboratory |
|
4 Copyright 1998 University of Cambridge |
|
5 |
|
6 Composition |
|
7 From Chandy and Sanders, "Reasoning About Program Composition", |
|
8 Technical Report 2000-003, University of Florida, 2000. |
|
9 |
|
10 Revised by Sidi Ehmety on January 2001 |
|
11 |
|
12 Added: a strong form of the order relation over component and localize |
|
13 |
|
14 Theory ported from HOL. |
|
15 |
|
16 *) |
|
17 |
|
18 Comp = Union + |
|
19 |
|
20 constdefs |
|
21 |
|
22 component :: [i, i] => o (infixl 65) |
|
23 "F component H == (EX G. F Join G = H)" |
|
24 |
|
25 strict_component :: [i, i] => o (infixl "strict'_component" 65) |
|
26 "F strict_component H == F component H & F~=H" |
|
27 |
|
28 (* A stronger form of the component relation *) |
|
29 component_of :: "[i,i]=>o" (infixl "component'_of" 65) |
|
30 "F component_of H == (EX G. F ok G & F Join G = H)" |
|
31 |
|
32 strict_component_of :: "[i,i]=>o" (infixl "strict'_component'_of" 65) |
|
33 "F strict_component_of H == F component_of H & F~=H" |
|
34 |
|
35 (* preserves any state function f, in particular a variable *) |
|
36 preserves :: (i=>i)=>i |
|
37 "preserves(f) == {F:program. ALL z. F: stable({s:state. f(s) = z})}" |
|
38 |
|
39 localize :: "[i=>i, i] => i" |
|
40 "localize(f,F) == mk_program(Init(F), Acts(F), |
|
41 AllowedActs(F Int (UN G:preserves(f). Acts(G))))" |
|
42 |
|
43 |
|
44 end |