author | paulson |
Tue, 31 Aug 1999 15:58:38 +0200 | |
changeset 7400 | fbd5582761e6 |
child 8055 | bb15396278fb |
permissions | -rw-r--r-- |
7400
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
1 |
(* Title: HOL/UNITY/Guar.thy |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
2 |
ID: $Id$ |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
4 |
Copyright 1999 University of Cambridge |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
5 |
|
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
6 |
Guarantees, etc. |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
7 |
|
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
8 |
From Chandy and Sanders, "Reasoning About Program Composition" |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
9 |
*) |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
10 |
|
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
11 |
Guar = Comp + |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
12 |
|
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
13 |
instance program :: (term) order |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
14 |
(component_refl, component_trans, component_antisym, |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
15 |
program_less_le) |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
16 |
|
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
17 |
constdefs |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
18 |
|
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
19 |
(*Existential and Universal properties. I formalize the two-program |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
20 |
case, proving equivalence with Chandy and Sanders's n-ary definitions*) |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
21 |
|
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
22 |
ex_prop :: 'a program set => bool |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
23 |
"ex_prop X == ALL F G. F:X | G: X --> (F Join G) : X" |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
24 |
|
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
25 |
strict_ex_prop :: 'a program set => bool |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
26 |
"strict_ex_prop X == ALL F G. (F:X | G: X) = (F Join G : X)" |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
27 |
|
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
28 |
uv_prop :: 'a program set => bool |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
29 |
"uv_prop X == SKIP : X & (ALL F G. F:X & G: X --> (F Join G) : X)" |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
30 |
|
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
31 |
strict_uv_prop :: 'a program set => bool |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
32 |
"strict_uv_prop X == SKIP : X & (ALL F G. (F:X & G: X) = (F Join G : X))" |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
33 |
|
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
34 |
(*Ill-defined programs can arise through "Join"*) |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
35 |
welldef :: 'a program set |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
36 |
"welldef == {F. Init F ~= {}}" |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
37 |
|
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
38 |
guar :: ['a program set, 'a program set] => 'a program set |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
39 |
(infixl "guarantees" 55) (*higher than membership, lower than Co*) |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
40 |
"X guarantees Y == {F. ALL H. F <= H --> H:X --> H:Y}" |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
41 |
|
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
42 |
refines :: ['a program, 'a program, 'a program set] => bool |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
43 |
("(3_ refines _ wrt _)" [10,10,10] 10) |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
44 |
"G refines F wrt X == |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
45 |
ALL H. (F Join H) : welldef Int X --> G Join H : welldef Int X" |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
46 |
|
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
47 |
iso_refines :: ['a program, 'a program, 'a program set] => bool |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
48 |
("(3_ iso'_refines _ wrt _)" [10,10,10] 10) |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
49 |
"G iso_refines F wrt X == |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
50 |
F : welldef Int X --> G : welldef Int X" |
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
51 |
|
fbd5582761e6
new files HOL/UNITY/Guar.{thy,ML}: theory file gets the instance declaration
paulson
parents:
diff
changeset
|
52 |
end |