4776
|
1 |
(* Title: HOL/UNITY/UNITY
|
|
2 |
ID: $Id$
|
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory
|
|
4 |
Copyright 1998 University of Cambridge
|
|
5 |
|
|
6 |
The basic UNITY theory (revised version, based upon the "co" operator)
|
|
7 |
|
|
8 |
From Misra, "A Logic for Concurrent Programming", 1994
|
|
9 |
*)
|
|
10 |
|
|
11 |
set proof_timing;
|
|
12 |
HOL_quantifiers := false;
|
|
13 |
|
|
14 |
|
|
15 |
(*CAN BOOLEAN SIMPLIFICATION BE AUTOMATED?*)
|
|
16 |
|
|
17 |
(** Rewrites rules to eliminate A. Conditions can be satisfied by letting B
|
|
18 |
be any set including A Int C and contained in A Un C, such as B=A or B=C.
|
|
19 |
**)
|
|
20 |
|
|
21 |
goal thy "!!x. [| A Int C <= B; B <= A Un C |] \
|
|
22 |
\ ==> (A Int B) Un (Compl A Int C) = B Un C";
|
|
23 |
by (Blast_tac 1);
|
|
24 |
|
|
25 |
goal thy "!!x. [| A Int C <= B; B <= A Un C |] \
|
|
26 |
\ ==> (A Un B) Int (Compl A Un C) = B Int C";
|
|
27 |
by (Blast_tac 1);
|
|
28 |
|
|
29 |
(*The base B=A*)
|
|
30 |
goal thy "A Un (Compl A Int C) = A Un C";
|
|
31 |
by (Blast_tac 1);
|
|
32 |
|
|
33 |
goal thy "A Int (Compl A Un C) = A Int C";
|
|
34 |
by (Blast_tac 1);
|
|
35 |
|
|
36 |
(*The base B=C*)
|
|
37 |
goal thy "(A Int C) Un (Compl A Int C) = C";
|
|
38 |
by (Blast_tac 1);
|
|
39 |
|
|
40 |
goal thy "(A Un C) Int (Compl A Un C) = C";
|
|
41 |
by (Blast_tac 1);
|
|
42 |
|
|
43 |
|
|
44 |
(** More ad-hoc rules **)
|
|
45 |
|
|
46 |
goal thy "A Un B - (A - B) = B";
|
|
47 |
by (Blast_tac 1);
|
|
48 |
qed "Un_Diff_Diff";
|
|
49 |
|
|
50 |
goal thy "A Int (B - C) Un C = A Int B Un C";
|
|
51 |
by (Blast_tac 1);
|
|
52 |
qed "Int_Diff_Un";
|
|
53 |
|
|
54 |
|
|
55 |
open UNITY;
|
|
56 |
|
|
57 |
|
|
58 |
(*** constrains ***)
|
|
59 |
|
|
60 |
val prems = goalw thy [constrains_def]
|
|
61 |
"(!!act s s'. [| act: Acts; (s,s') : act; s: A |] ==> s': A') \
|
|
62 |
\ ==> constrains Acts A A'";
|
|
63 |
by (blast_tac (claset() addIs prems) 1);
|
|
64 |
qed "constrainsI";
|
|
65 |
|
|
66 |
goalw thy [constrains_def]
|
|
67 |
"!!Acts. [| constrains Acts A A'; act: Acts; (s,s'): act; s: A |] \
|
|
68 |
\ ==> s': A'";
|
|
69 |
by (Blast_tac 1);
|
|
70 |
qed "constrainsD";
|
|
71 |
|
|
72 |
goalw thy [constrains_def] "constrains Acts {} B";
|
|
73 |
by (Blast_tac 1);
|
|
74 |
qed "constrains_empty";
|
|
75 |
|
|
76 |
goalw thy [constrains_def] "constrains Acts A UNIV";
|
|
77 |
by (Blast_tac 1);
|
|
78 |
qed "constrains_UNIV";
|
|
79 |
AddIffs [constrains_empty, constrains_UNIV];
|
|
80 |
|
|
81 |
goalw thy [constrains_def]
|
|
82 |
"!!Acts. [| constrains Acts A A'; A'<=B' |] ==> constrains Acts A B'";
|
|
83 |
by (Blast_tac 1);
|
|
84 |
qed "constrains_weaken_R";
|
|
85 |
|
|
86 |
goalw thy [constrains_def]
|
|
87 |
"!!Acts. [| constrains Acts A A'; B<=A |] ==> constrains Acts B A'";
|
|
88 |
by (Blast_tac 1);
|
|
89 |
qed "constrains_weaken_L";
|
|
90 |
|
|
91 |
goalw thy [constrains_def]
|
|
92 |
"!!Acts. [| constrains Acts A A'; B<=A; A'<=B' |] ==> constrains Acts B B'";
|
|
93 |
by (Blast_tac 1);
|
|
94 |
qed "constrains_weaken";
|
|
95 |
|
|
96 |
(*Set difference: UNUSED*)
|
|
97 |
goalw thy [constrains_def]
|
|
98 |
"!!C. [| constrains Acts (A-B) C; constrains Acts B C |] \
|
|
99 |
\ ==> constrains Acts A C";
|
|
100 |
by (Blast_tac 1);
|
|
101 |
qed "constrains_Diff";
|
|
102 |
|
|
103 |
(** Union **)
|
|
104 |
|
|
105 |
goalw thy [constrains_def]
|
|
106 |
"!!Acts. [| constrains Acts A A'; constrains Acts B B' |] \
|
|
107 |
\ ==> constrains Acts (A Un B) (A' Un B')";
|
|
108 |
by (Blast_tac 1);
|
|
109 |
qed "constrains_Un";
|
|
110 |
|
|
111 |
goalw thy [constrains_def]
|
|
112 |
"!!Acts. ALL i:I. constrains Acts (A i) (A' i) \
|
|
113 |
\ ==> constrains Acts (UN i:I. A i) (UN i:I. A' i)";
|
|
114 |
by (Blast_tac 1);
|
|
115 |
qed "ball_constrains_UN";
|
|
116 |
|
|
117 |
goalw thy [constrains_def]
|
|
118 |
"!!Acts. [| ALL i. constrains Acts (A i) (A' i) |] \
|
|
119 |
\ ==> constrains Acts (UN i. A i) (UN i. A' i)";
|
|
120 |
by (Blast_tac 1);
|
|
121 |
qed "all_constrains_UN";
|
|
122 |
|
|
123 |
(** Intersection **)
|
|
124 |
|
|
125 |
goalw thy [constrains_def]
|
|
126 |
"!!Acts. [| constrains Acts A A'; constrains Acts B B' |] \
|
|
127 |
\ ==> constrains Acts (A Int B) (A' Int B')";
|
|
128 |
by (Blast_tac 1);
|
|
129 |
qed "constrains_Int";
|
|
130 |
|
|
131 |
goalw thy [constrains_def]
|
|
132 |
"!!Acts. ALL i:I. constrains Acts (A i) (A' i) \
|
|
133 |
\ ==> constrains Acts (INT i:I. A i) (INT i:I. A' i)";
|
|
134 |
by (Blast_tac 1);
|
|
135 |
qed "ball_constrains_INT";
|
|
136 |
|
|
137 |
goalw thy [constrains_def]
|
|
138 |
"!!Acts. [| ALL i. constrains Acts (A i) (A' i) |] \
|
|
139 |
\ ==> constrains Acts (INT i. A i) (INT i. A' i)";
|
|
140 |
by (Blast_tac 1);
|
|
141 |
qed "all_constrains_INT";
|
|
142 |
|
|
143 |
goalw thy [stable_def, constrains_def]
|
|
144 |
"!!Acts. [| stable Acts C; constrains Acts A (C Un A') |] \
|
|
145 |
\ ==> constrains Acts (C Un A) (C Un A')";
|
|
146 |
by (Blast_tac 1);
|
|
147 |
qed "stable_constrains_Un";
|
|
148 |
|
|
149 |
goalw thy [stable_def, constrains_def]
|
|
150 |
"!!Acts. [| stable Acts C; constrains Acts (C Int A) A' |] \
|
|
151 |
\ ==> constrains Acts (C Int A) (C Int A')";
|
|
152 |
by (Blast_tac 1);
|
|
153 |
qed "stable_constrains_Int";
|
|
154 |
|
|
155 |
|
|
156 |
(*** stable ***)
|
|
157 |
|
|
158 |
goalw thy [stable_def]
|
|
159 |
"!!Acts. constrains Acts A A ==> stable Acts A";
|
|
160 |
by (assume_tac 1);
|
|
161 |
qed "stableI";
|
|
162 |
|
|
163 |
goalw thy [stable_def]
|
|
164 |
"!!Acts. stable Acts A ==> constrains Acts A A";
|
|
165 |
by (assume_tac 1);
|
|
166 |
qed "stableD";
|
|
167 |
|
|
168 |
goalw thy [stable_def]
|
|
169 |
"!!Acts. [| stable Acts A; stable Acts A' |] \
|
|
170 |
\ ==> stable Acts (A Un A')";
|
|
171 |
by (blast_tac (claset() addIs [constrains_Un]) 1);
|
|
172 |
qed "stable_Un";
|
|
173 |
|
|
174 |
goalw thy [stable_def]
|
|
175 |
"!!Acts. [| stable Acts A; stable Acts A' |] \
|
|
176 |
\ ==> stable Acts (A Int A')";
|
|
177 |
by (blast_tac (claset() addIs [constrains_Int]) 1);
|
|
178 |
qed "stable_Int";
|
|
179 |
|
|
180 |
goalw thy [constrains_def]
|
|
181 |
"!!Acts. [| constrains Acts A A'; id: Acts |] ==> A<=A'";
|
|
182 |
by (Blast_tac 1);
|
|
183 |
qed "constrains_imp_subset";
|
|
184 |
|
|
185 |
|
|
186 |
goalw thy [constrains_def]
|
|
187 |
"!!Acts. [| id: Acts; constrains Acts A B; constrains Acts B C |] \
|
|
188 |
\ ==> constrains Acts A C";
|
|
189 |
by (Blast_tac 1);
|
|
190 |
qed "constrains_trans";
|
|
191 |
|
|
192 |
|
|
193 |
(*The Elimination Theorem. The "free" m has become universally quantified!
|
|
194 |
Should the premise be !!m instead of ALL m ? Would make it harder to use
|
|
195 |
in forward proof.*)
|
|
196 |
goalw thy [constrains_def]
|
|
197 |
"!!Acts. [| ALL m. constrains Acts {s. s x = m} (B m) |] \
|
|
198 |
\ ==> constrains Acts {s. P(s x)} (UN m. {s. P(m)} Int B m)";
|
|
199 |
by (Blast_tac 1);
|
|
200 |
qed "elimination";
|
|
201 |
|
|
202 |
(*As above, but for the trivial case of a one-variable state, in which the
|
|
203 |
state is identified with its one variable.*)
|
|
204 |
goalw thy [constrains_def]
|
|
205 |
"!!Acts. [| ALL m. constrains Acts {m} (B m) |] \
|
|
206 |
\ ==> constrains Acts {s. P s} (UN m. {s. P(m)} Int B m)";
|
|
207 |
by (Blast_tac 1);
|
|
208 |
qed "elimination_sing";
|
|
209 |
|
|
210 |
|
|
211 |
goalw thy [constrains_def]
|
|
212 |
"!!Acts. [| constrains Acts A (A' Un B); constrains Acts B B'; id: Acts |] \
|
|
213 |
\ ==> constrains Acts A (A' Un B')";
|
|
214 |
by (Blast_tac 1);
|
|
215 |
qed "constrains_cancel";
|
|
216 |
|
|
217 |
|
|
218 |
|
|
219 |
(*** Theoretical Results from Section 6 ***)
|
|
220 |
|
|
221 |
goalw thy [constrains_def, strongest_rhs_def]
|
|
222 |
"constrains Acts A (strongest_rhs Acts A )";
|
|
223 |
by (Blast_tac 1);
|
|
224 |
qed "constrains_strongest_rhs";
|
|
225 |
|
|
226 |
goalw thy [constrains_def, strongest_rhs_def]
|
|
227 |
"!!Acts. constrains Acts A B ==> strongest_rhs Acts A <= B";
|
|
228 |
by (Blast_tac 1);
|
|
229 |
qed "strongest_rhs_is_strongest";
|