|
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"; |