author | wenzelm |
Sat, 01 Dec 2001 18:52:32 +0100 | |
changeset 12338 | de0f4a63baa5 |
parent 11190 | 44e157622cb2 |
child 13792 | d1811693899c |
permissions | -rw-r--r-- |
5597 | 1 |
(* Title: HOL/UNITY/Comp.thy |
2 |
ID: $Id$ |
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 1998 University of Cambridge |
|
5 |
||
6 |
Composition |
|
11190 | 7 |
From Chandy and Sanders, "Reasoning About Program Composition", |
8 |
Technical Report 2000-003, University of Florida, 2000. |
|
5597 | 9 |
|
11190 | 10 |
Revised by Sidi Ehmety on January 2001 |
11 |
||
12 |
Added: a strong form of the <= relation (component_of) and localize |
|
13 |
||
5597 | 14 |
*) |
15 |
||
16 |
Comp = Union + |
|
17 |
||
7399
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7364
diff
changeset
|
18 |
instance |
12338
de0f4a63baa5
renamed class "term" to "type" (actually "HOL.type");
wenzelm
parents:
11190
diff
changeset
|
19 |
program :: (type) ord |
5597 | 20 |
|
7399
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7364
diff
changeset
|
21 |
defs |
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7364
diff
changeset
|
22 |
component_def "F <= H == EX G. F Join G = H" |
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7364
diff
changeset
|
23 |
strict_component_def "(F < (H::'a program)) == (F <= H & F ~= H)" |
5612
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
24 |
|
11190 | 25 |
|
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7399
diff
changeset
|
26 |
constdefs |
11190 | 27 |
component_of :: "'a program=>'a program=> bool" |
28 |
(infixl "component'_of" 50) |
|
29 |
"F component_of H == EX G. F ok G & F Join G = H" |
|
30 |
||
31 |
strict_component_of :: "'a program\\<Rightarrow>'a program=> bool" |
|
32 |
(infixl "strict'_component'_of" 50) |
|
33 |
"F strict_component_of H == F component_of H & F~=H" |
|
34 |
||
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7399
diff
changeset
|
35 |
preserves :: "('a=>'b) => 'a program set" |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7399
diff
changeset
|
36 |
"preserves v == INT z. stable {s. v s = z}" |
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7399
diff
changeset
|
37 |
|
11190 | 38 |
localize :: "('a=>'b) => 'a program => 'a program" |
39 |
"localize v F == mk_program(Init F, Acts F, |
|
40 |
AllowedActs F Int (UN G:preserves v. Acts G))" |
|
41 |
||
8055
bb15396278fb
abolition of localTo: instead "guarantees" has local vars as extra argument
paulson
parents:
7399
diff
changeset
|
42 |
funPair :: "['a => 'b, 'a => 'c, 'a] => 'b * 'c" |
11190 | 43 |
"funPair f g == %x. (f x, g x)" |
5597 | 44 |
end |