61 "(!!act s s'. [| act: Acts; (s,s') : act; s: A |] ==> s': A') \ |
61 "(!!act s s'. [| act: Acts; (s,s') : act; s: A |] ==> s': A') \ |
62 \ ==> constrains Acts A A'"; |
62 \ ==> constrains Acts A A'"; |
63 by (blast_tac (claset() addIs prems) 1); |
63 by (blast_tac (claset() addIs prems) 1); |
64 qed "constrainsI"; |
64 qed "constrainsI"; |
65 |
65 |
66 goalw thy [constrains_def] |
66 Goalw [constrains_def] |
67 "!!Acts. [| constrains Acts A A'; act: Acts; (s,s'): act; s: A |] \ |
67 "!!Acts. [| constrains Acts A A'; act: Acts; (s,s'): act; s: A |] \ |
68 \ ==> s': A'"; |
68 \ ==> s': A'"; |
69 by (Blast_tac 1); |
69 by (Blast_tac 1); |
70 qed "constrainsD"; |
70 qed "constrainsD"; |
71 |
71 |
72 goalw thy [constrains_def] "constrains Acts {} B"; |
72 Goalw [constrains_def] "constrains Acts {} B"; |
73 by (Blast_tac 1); |
73 by (Blast_tac 1); |
74 qed "constrains_empty"; |
74 qed "constrains_empty"; |
75 |
75 |
76 goalw thy [constrains_def] "constrains Acts A UNIV"; |
76 Goalw [constrains_def] "constrains Acts A UNIV"; |
77 by (Blast_tac 1); |
77 by (Blast_tac 1); |
78 qed "constrains_UNIV"; |
78 qed "constrains_UNIV"; |
79 AddIffs [constrains_empty, constrains_UNIV]; |
79 AddIffs [constrains_empty, constrains_UNIV]; |
80 |
80 |
81 goalw thy [constrains_def] |
81 Goalw [constrains_def] |
82 "!!Acts. [| constrains Acts A A'; A'<=B' |] ==> constrains Acts A B'"; |
82 "!!Acts. [| constrains Acts A A'; A'<=B' |] ==> constrains Acts A B'"; |
83 by (Blast_tac 1); |
83 by (Blast_tac 1); |
84 qed "constrains_weaken_R"; |
84 qed "constrains_weaken_R"; |
85 |
85 |
86 goalw thy [constrains_def] |
86 Goalw [constrains_def] |
87 "!!Acts. [| constrains Acts A A'; B<=A |] ==> constrains Acts B A'"; |
87 "!!Acts. [| constrains Acts A A'; B<=A |] ==> constrains Acts B A'"; |
88 by (Blast_tac 1); |
88 by (Blast_tac 1); |
89 qed "constrains_weaken_L"; |
89 qed "constrains_weaken_L"; |
90 |
90 |
91 goalw thy [constrains_def] |
91 Goalw [constrains_def] |
92 "!!Acts. [| constrains Acts A A'; B<=A; A'<=B' |] ==> constrains Acts B B'"; |
92 "!!Acts. [| constrains Acts A A'; B<=A; A'<=B' |] ==> constrains Acts B B'"; |
93 by (Blast_tac 1); |
93 by (Blast_tac 1); |
94 qed "constrains_weaken"; |
94 qed "constrains_weaken"; |
95 |
95 |
96 (*Set difference: UNUSED*) |
96 (*Set difference: UNUSED*) |
97 goalw thy [constrains_def] |
97 Goalw [constrains_def] |
98 "!!C. [| constrains Acts (A-B) C; constrains Acts B C |] \ |
98 "!!C. [| constrains Acts (A-B) C; constrains Acts B C |] \ |
99 \ ==> constrains Acts A C"; |
99 \ ==> constrains Acts A C"; |
100 by (Blast_tac 1); |
100 by (Blast_tac 1); |
101 qed "constrains_Diff"; |
101 qed "constrains_Diff"; |
102 |
102 |
103 (** Union **) |
103 (** Union **) |
104 |
104 |
105 goalw thy [constrains_def] |
105 Goalw [constrains_def] |
106 "!!Acts. [| constrains Acts A A'; constrains Acts B B' |] \ |
106 "!!Acts. [| constrains Acts A A'; constrains Acts B B' |] \ |
107 \ ==> constrains Acts (A Un B) (A' Un B')"; |
107 \ ==> constrains Acts (A Un B) (A' Un B')"; |
108 by (Blast_tac 1); |
108 by (Blast_tac 1); |
109 qed "constrains_Un"; |
109 qed "constrains_Un"; |
110 |
110 |
111 goalw thy [constrains_def] |
111 Goalw [constrains_def] |
112 "!!Acts. ALL i:I. constrains Acts (A i) (A' i) \ |
112 "!!Acts. ALL i:I. constrains Acts (A i) (A' i) \ |
113 \ ==> constrains Acts (UN i:I. A i) (UN i:I. A' i)"; |
113 \ ==> constrains Acts (UN i:I. A i) (UN i:I. A' i)"; |
114 by (Blast_tac 1); |
114 by (Blast_tac 1); |
115 qed "ball_constrains_UN"; |
115 qed "ball_constrains_UN"; |
116 |
116 |
117 goalw thy [constrains_def] |
117 Goalw [constrains_def] |
118 "!!Acts. [| ALL i. constrains Acts (A i) (A' i) |] \ |
118 "!!Acts. [| ALL i. constrains Acts (A i) (A' i) |] \ |
119 \ ==> constrains Acts (UN i. A i) (UN i. A' i)"; |
119 \ ==> constrains Acts (UN i. A i) (UN i. A' i)"; |
120 by (Blast_tac 1); |
120 by (Blast_tac 1); |
121 qed "all_constrains_UN"; |
121 qed "all_constrains_UN"; |
122 |
122 |
123 (** Intersection **) |
123 (** Intersection **) |
124 |
124 |
125 goalw thy [constrains_def] |
125 Goalw [constrains_def] |
126 "!!Acts. [| constrains Acts A A'; constrains Acts B B' |] \ |
126 "!!Acts. [| constrains Acts A A'; constrains Acts B B' |] \ |
127 \ ==> constrains Acts (A Int B) (A' Int B')"; |
127 \ ==> constrains Acts (A Int B) (A' Int B')"; |
128 by (Blast_tac 1); |
128 by (Blast_tac 1); |
129 qed "constrains_Int"; |
129 qed "constrains_Int"; |
130 |
130 |
131 goalw thy [constrains_def] |
131 Goalw [constrains_def] |
132 "!!Acts. ALL i:I. constrains Acts (A i) (A' i) \ |
132 "!!Acts. ALL i:I. constrains Acts (A i) (A' i) \ |
133 \ ==> constrains Acts (INT i:I. A i) (INT i:I. A' i)"; |
133 \ ==> constrains Acts (INT i:I. A i) (INT i:I. A' i)"; |
134 by (Blast_tac 1); |
134 by (Blast_tac 1); |
135 qed "ball_constrains_INT"; |
135 qed "ball_constrains_INT"; |
136 |
136 |
137 goalw thy [constrains_def] |
137 Goalw [constrains_def] |
138 "!!Acts. [| ALL i. constrains Acts (A i) (A' i) |] \ |
138 "!!Acts. [| ALL i. constrains Acts (A i) (A' i) |] \ |
139 \ ==> constrains Acts (INT i. A i) (INT i. A' i)"; |
139 \ ==> constrains Acts (INT i. A i) (INT i. A' i)"; |
140 by (Blast_tac 1); |
140 by (Blast_tac 1); |
141 qed "all_constrains_INT"; |
141 qed "all_constrains_INT"; |
142 |
142 |
143 goalw thy [stable_def, constrains_def] |
143 Goalw [stable_def, constrains_def] |
144 "!!Acts. [| stable Acts C; constrains Acts A (C Un A') |] \ |
144 "!!Acts. [| stable Acts C; constrains Acts A (C Un A') |] \ |
145 \ ==> constrains Acts (C Un A) (C Un A')"; |
145 \ ==> constrains Acts (C Un A) (C Un A')"; |
146 by (Blast_tac 1); |
146 by (Blast_tac 1); |
147 qed "stable_constrains_Un"; |
147 qed "stable_constrains_Un"; |
148 |
148 |
149 goalw thy [stable_def, constrains_def] |
149 Goalw [stable_def, constrains_def] |
150 "!!Acts. [| stable Acts C; constrains Acts (C Int A) A' |] \ |
150 "!!Acts. [| stable Acts C; constrains Acts (C Int A) A' |] \ |
151 \ ==> constrains Acts (C Int A) (C Int A')"; |
151 \ ==> constrains Acts (C Int A) (C Int A')"; |
152 by (Blast_tac 1); |
152 by (Blast_tac 1); |
153 qed "stable_constrains_Int"; |
153 qed "stable_constrains_Int"; |
154 |
154 |
155 |
155 |
156 (*** stable ***) |
156 (*** stable ***) |
157 |
157 |
158 goalw thy [stable_def] |
158 Goalw [stable_def] |
159 "!!Acts. constrains Acts A A ==> stable Acts A"; |
159 "!!Acts. constrains Acts A A ==> stable Acts A"; |
160 by (assume_tac 1); |
160 by (assume_tac 1); |
161 qed "stableI"; |
161 qed "stableI"; |
162 |
162 |
163 goalw thy [stable_def] |
163 Goalw [stable_def] |
164 "!!Acts. stable Acts A ==> constrains Acts A A"; |
164 "!!Acts. stable Acts A ==> constrains Acts A A"; |
165 by (assume_tac 1); |
165 by (assume_tac 1); |
166 qed "stableD"; |
166 qed "stableD"; |
167 |
167 |
168 goalw thy [stable_def] |
168 Goalw [stable_def] |
169 "!!Acts. [| stable Acts A; stable Acts A' |] \ |
169 "!!Acts. [| stable Acts A; stable Acts A' |] \ |
170 \ ==> stable Acts (A Un A')"; |
170 \ ==> stable Acts (A Un A')"; |
171 by (blast_tac (claset() addIs [constrains_Un]) 1); |
171 by (blast_tac (claset() addIs [constrains_Un]) 1); |
172 qed "stable_Un"; |
172 qed "stable_Un"; |
173 |
173 |
174 goalw thy [stable_def] |
174 Goalw [stable_def] |
175 "!!Acts. [| stable Acts A; stable Acts A' |] \ |
175 "!!Acts. [| stable Acts A; stable Acts A' |] \ |
176 \ ==> stable Acts (A Int A')"; |
176 \ ==> stable Acts (A Int A')"; |
177 by (blast_tac (claset() addIs [constrains_Int]) 1); |
177 by (blast_tac (claset() addIs [constrains_Int]) 1); |
178 qed "stable_Int"; |
178 qed "stable_Int"; |
179 |
179 |
180 goalw thy [constrains_def] |
180 Goalw [constrains_def] |
181 "!!Acts. [| constrains Acts A A'; id: Acts |] ==> A<=A'"; |
181 "!!Acts. [| constrains Acts A A'; id: Acts |] ==> A<=A'"; |
182 by (Blast_tac 1); |
182 by (Blast_tac 1); |
183 qed "constrains_imp_subset"; |
183 qed "constrains_imp_subset"; |
184 |
184 |
185 |
185 |
186 goalw thy [constrains_def] |
186 Goalw [constrains_def] |
187 "!!Acts. [| id: Acts; constrains Acts A B; constrains Acts B C |] \ |
187 "!!Acts. [| id: Acts; constrains Acts A B; constrains Acts B C |] \ |
188 \ ==> constrains Acts A C"; |
188 \ ==> constrains Acts A C"; |
189 by (Blast_tac 1); |
189 by (Blast_tac 1); |
190 qed "constrains_trans"; |
190 qed "constrains_trans"; |
191 |
191 |
192 |
192 |
193 (*The Elimination Theorem. The "free" m has become universally quantified! |
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 |
194 Should the premise be !!m instead of ALL m ? Would make it harder to use |
195 in forward proof.*) |
195 in forward proof.*) |
196 goalw thy [constrains_def] |
196 Goalw [constrains_def] |
197 "!!Acts. [| ALL m. constrains Acts {s. s x = m} (B m) |] \ |
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)"; |
198 \ ==> constrains Acts {s. P(s x)} (UN m. {s. P(m)} Int B m)"; |
199 by (Blast_tac 1); |
199 by (Blast_tac 1); |
200 qed "elimination"; |
200 qed "elimination"; |
201 |
201 |
202 (*As above, but for the trivial case of a one-variable state, in which the |
202 (*As above, but for the trivial case of a one-variable state, in which the |
203 state is identified with its one variable.*) |
203 state is identified with its one variable.*) |
204 goalw thy [constrains_def] |
204 Goalw [constrains_def] |
205 "!!Acts. [| ALL m. constrains Acts {m} (B m) |] \ |
205 "!!Acts. [| ALL m. constrains Acts {m} (B m) |] \ |
206 \ ==> constrains Acts {s. P s} (UN m. {s. P(m)} Int B m)"; |
206 \ ==> constrains Acts {s. P s} (UN m. {s. P(m)} Int B m)"; |
207 by (Blast_tac 1); |
207 by (Blast_tac 1); |
208 qed "elimination_sing"; |
208 qed "elimination_sing"; |
209 |
209 |
210 |
210 |
211 goalw thy [constrains_def] |
211 Goalw [constrains_def] |
212 "!!Acts. [| constrains Acts A (A' Un B); constrains Acts B B'; id: Acts |] \ |
212 "!!Acts. [| constrains Acts A (A' Un B); constrains Acts B B'; id: Acts |] \ |
213 \ ==> constrains Acts A (A' Un B')"; |
213 \ ==> constrains Acts A (A' Un B')"; |
214 by (Blast_tac 1); |
214 by (Blast_tac 1); |
215 qed "constrains_cancel"; |
215 qed "constrains_cancel"; |
216 |
216 |
217 |
217 |
218 |
218 |
219 (*** Theoretical Results from Section 6 ***) |
219 (*** Theoretical Results from Section 6 ***) |
220 |
220 |
221 goalw thy [constrains_def, strongest_rhs_def] |
221 Goalw [constrains_def, strongest_rhs_def] |
222 "constrains Acts A (strongest_rhs Acts A )"; |
222 "constrains Acts A (strongest_rhs Acts A )"; |
223 by (Blast_tac 1); |
223 by (Blast_tac 1); |
224 qed "constrains_strongest_rhs"; |
224 qed "constrains_strongest_rhs"; |
225 |
225 |
226 goalw thy [constrains_def, strongest_rhs_def] |
226 Goalw [constrains_def, strongest_rhs_def] |
227 "!!Acts. constrains Acts A B ==> strongest_rhs Acts A <= B"; |
227 "!!Acts. constrains Acts A B ==> strongest_rhs Acts A <= B"; |
228 by (Blast_tac 1); |
228 by (Blast_tac 1); |
229 qed "strongest_rhs_is_strongest"; |
229 qed "strongest_rhs_is_strongest"; |