author | paulson |
Sun, 13 Jun 1999 13:52:50 +0200 | |
changeset 6822 | 8932f33259d4 |
parent 6646 | 3ea726909fff |
child 7364 | a979e8a2ee18 |
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 |
|
7 |
||
8 |
From Chandy and Sanders, "Reasoning About Program Composition" |
|
9 |
*) |
|
10 |
||
11 |
Comp = Union + |
|
12 |
||
13 |
constdefs |
|
14 |
||
15 |
(*Existential and Universal properties. I formalize the two-program |
|
16 |
case, proving equivalence with Chandy and Sanders's n-ary definitions*) |
|
17 |
||
18 |
ex_prop :: 'a program set => bool |
|
6295
351b3c2b0d83
removed the infernal States, eqStates, compatible, etc.
paulson
parents:
6138
diff
changeset
|
19 |
"ex_prop X == ALL F G. F:X | G: X --> (F Join G) : X" |
5597 | 20 |
|
21 |
strict_ex_prop :: 'a program set => bool |
|
6295
351b3c2b0d83
removed the infernal States, eqStates, compatible, etc.
paulson
parents:
6138
diff
changeset
|
22 |
"strict_ex_prop X == ALL F G. (F:X | G: X) = (F Join G : X)" |
5597 | 23 |
|
24 |
uv_prop :: 'a program set => bool |
|
6295
351b3c2b0d83
removed the infernal States, eqStates, compatible, etc.
paulson
parents:
6138
diff
changeset
|
25 |
"uv_prop X == SKIP : X & (ALL F G. F:X & G: X --> (F Join G) : X)" |
5597 | 26 |
|
27 |
strict_uv_prop :: 'a program set => bool |
|
6295
351b3c2b0d83
removed the infernal States, eqStates, compatible, etc.
paulson
parents:
6138
diff
changeset
|
28 |
"strict_uv_prop X == SKIP : X & (ALL F G. (F:X & G: X) = (F Join G : X))" |
5597 | 29 |
|
5612
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
30 |
(*Ill-defined programs can arise through "Join"*) |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
31 |
welldef :: 'a program set |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
32 |
"welldef == {F. Init F ~= {}}" |
5597 | 33 |
|
6646 | 34 |
component :: ['a program, 'a program] => bool (infixl 50) |
35 |
"F component H == EX G. F Join G = H" |
|
5597 | 36 |
|
6822 | 37 |
guarantees :: ['a program set, 'a program set] => 'a program set |
38 |
(infixl "guar" 65) |
|
39 |
"X guar Y == {F. ALL H. F component H --> H:X --> H:Y}" |
|
5597 | 40 |
|
5612
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
41 |
refines :: ['a program, 'a program, 'a program set] => bool |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
42 |
("(3_ refines _ wrt _)" [10,10,10] 10) |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
43 |
"G refines F wrt X == |
6295
351b3c2b0d83
removed the infernal States, eqStates, compatible, etc.
paulson
parents:
6138
diff
changeset
|
44 |
ALL H. (F Join H) : welldef Int X --> G Join H : welldef Int X" |
5612
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
45 |
|
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
46 |
iso_refines :: ['a program, 'a program, 'a program set] => bool |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
47 |
("(3_ iso'_refines _ wrt _)" [10,10,10] 10) |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
48 |
"G iso_refines F wrt X == |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
49 |
F : welldef Int X --> G : welldef Int X" |
e981ca6f7332
Finished proofs to end of section 5.1 of Chandy and Sanders
paulson
parents:
5597
diff
changeset
|
50 |
|
5597 | 51 |
end |