120 |
128 |
121 (*** guarantees ***) |
129 (*** guarantees ***) |
122 |
130 |
123 val prems = Goal |
131 val prems = Goal |
124 "(!!G. [| F Join G : X; Disjoint F G |] ==> F Join G : Y) \ |
132 "(!!G. [| F Join G : X; Disjoint F G |] ==> F Join G : Y) \ |
125 \ ==> F : X guar Y"; |
133 \ ==> F : X guarantees Y"; |
126 by (simp_tac (simpset() addsimps [guarantees_def, component_eq]) 1); |
134 by (simp_tac (simpset() addsimps [guar_def, component_eq]) 1); |
127 by (blast_tac (claset() addIs prems) 1); |
135 by (blast_tac (claset() addIs prems) 1); |
128 qed "guaranteesI"; |
136 qed "guaranteesI"; |
129 |
137 |
130 Goalw [guarantees_def, component_def] |
138 Goalw [guar_def, component_def] |
131 "[| F : X guar Y; F Join G : X |] ==> F Join G : Y"; |
139 "[| F : X guarantees Y; F Join G : X |] ==> F Join G : Y"; |
132 by (Blast_tac 1); |
140 by (Blast_tac 1); |
133 qed "guaranteesD"; |
141 qed "guaranteesD"; |
134 |
142 |
|
143 (*This version of guaranteesD matches more easily in the conclusion*) |
|
144 Goalw [guar_def] |
|
145 "[| F : X guarantees Y; H : X; F component H |] ==> H : Y"; |
|
146 by (Blast_tac 1); |
|
147 qed "component_guaranteesD"; |
|
148 |
135 (*This equation is more intuitive than the official definition*) |
149 (*This equation is more intuitive than the official definition*) |
136 Goal "(F : X guar Y) = \ |
150 Goal "(F : X guarantees Y) = \ |
137 \ (ALL G. F Join G : X & Disjoint F G --> F Join G : Y)"; |
151 \ (ALL G. F Join G : X & Disjoint F G --> F Join G : Y)"; |
138 by (simp_tac (simpset() addsimps [guarantees_def, component_eq]) 1); |
152 by (simp_tac (simpset() addsimps [guar_def, component_eq]) 1); |
139 by (Blast_tac 1); |
153 by (Blast_tac 1); |
140 qed "guarantees_eq"; |
154 qed "guarantees_eq"; |
141 |
155 |
142 Goalw [guarantees_def] "[| F: X guar X'; Y <= X; X' <= Y' |] ==> F: Y guar Y'"; |
156 Goalw [guar_def] |
|
157 "[| F: X guarantees X'; Y <= X; X' <= Y' |] ==> F: Y guarantees Y'"; |
143 by (Blast_tac 1); |
158 by (Blast_tac 1); |
144 qed "guarantees_weaken"; |
159 qed "guarantees_weaken"; |
145 |
160 |
146 Goalw [guarantees_def] "[| F: X guar Y; F component F' |] ==> F': X guar Y"; |
161 Goalw [guar_def] |
|
162 "[| F: X guarantees Y; F component F' |] ==> F': X guarantees Y"; |
147 by (blast_tac (claset() addIs [component_trans]) 1); |
163 by (blast_tac (claset() addIs [component_trans]) 1); |
148 qed "guarantees_weaken_prog"; |
164 qed "guarantees_weaken_prog"; |
149 |
165 |
150 Goalw [guarantees_def] "X <= Y ==> X guar Y = UNIV"; |
166 Goalw [guar_def] "X <= Y ==> X guarantees Y = UNIV"; |
151 by (Blast_tac 1); |
167 by (Blast_tac 1); |
152 qed "subset_imp_guarantees_UNIV"; |
168 qed "subset_imp_guarantees_UNIV"; |
153 |
169 |
154 (*Equivalent to subset_imp_guarantees_UNIV but more intuitive*) |
170 (*Equivalent to subset_imp_guarantees_UNIV but more intuitive*) |
155 Goalw [guarantees_def] "X <= Y ==> F : X guar Y"; |
171 Goalw [guar_def] "X <= Y ==> F : X guarantees Y"; |
156 by (Blast_tac 1); |
172 by (Blast_tac 1); |
157 qed "subset_imp_guarantees"; |
173 qed "subset_imp_guarantees"; |
158 |
174 |
159 (*Remark at end of section 4.1*) |
175 (*Remark at end of section 4.1*) |
160 Goalw [guarantees_def] "ex_prop Y = (Y = UNIV guar Y)"; |
176 Goalw [guar_def] "ex_prop Y = (Y = UNIV guarantees Y)"; |
161 by (simp_tac (simpset() addsimps [ex_prop_equiv]) 1); |
177 by (simp_tac (simpset() addsimps [ex_prop_equiv]) 1); |
162 by (blast_tac (claset() addEs [equalityE]) 1); |
178 by (blast_tac (claset() addEs [equalityE]) 1); |
163 qed "ex_prop_equiv2"; |
179 qed "ex_prop_equiv2"; |
164 |
180 |
165 (** Distributive laws. Re-orient to perform miniscoping **) |
181 (** Distributive laws. Re-orient to perform miniscoping **) |
166 |
182 |
167 Goalw [guarantees_def] |
183 Goalw [guar_def] |
168 "(UN X:XX. X) guar Y = (INT X:XX. X guar Y)"; |
184 "(UN i:I. X i) guarantees Y = (INT i:I. X i guarantees Y)"; |
169 by (Blast_tac 1); |
185 by (Blast_tac 1); |
170 qed "guarantees_UN_left"; |
186 qed "guarantees_UN_left"; |
171 |
187 |
172 Goalw [guarantees_def] |
188 Goalw [guar_def] |
173 "(X Un Y) guar Z = (X guar Z) Int (Y guar Z)"; |
189 "(X Un Y) guarantees Z = (X guarantees Z) Int (Y guarantees Z)"; |
174 by (Blast_tac 1); |
190 by (Blast_tac 1); |
175 qed "guarantees_Un_left"; |
191 qed "guarantees_Un_left"; |
176 |
192 |
177 Goalw [guarantees_def] |
193 Goalw [guar_def] |
178 "X guar (INT Y:YY. Y) = (INT Y:YY. X guar Y)"; |
194 "X guarantees (INT i:I. Y i) = (INT i:I. X guarantees Y i)"; |
179 by (Blast_tac 1); |
195 by (Blast_tac 1); |
180 qed "guarantees_INT_right"; |
196 qed "guarantees_INT_right"; |
181 |
197 |
182 Goalw [guarantees_def] |
198 Goalw [guar_def] |
183 "Z guar (X Int Y) = (Z guar X) Int (Z guar Y)"; |
199 "Z guarantees (X Int Y) = (Z guarantees X) Int (Z guarantees Y)"; |
184 by (Blast_tac 1); |
200 by (Blast_tac 1); |
185 qed "guarantees_Int_right"; |
201 qed "guarantees_Int_right"; |
186 |
202 |
187 Goalw [guarantees_def] "(X guar Y) = (UNIV guar (-X Un Y))"; |
203 Goalw [guar_def] "(X guarantees Y) = (UNIV guarantees (-X Un Y))"; |
188 by (Blast_tac 1); |
204 by (Blast_tac 1); |
189 qed "shunting"; |
205 qed "shunting"; |
190 |
206 |
191 Goalw [guarantees_def] "(X guar Y) = -Y guar -X"; |
207 Goalw [guar_def] "(X guarantees Y) = -Y guarantees -X"; |
192 by (Blast_tac 1); |
208 by (Blast_tac 1); |
193 qed "contrapositive"; |
209 qed "contrapositive"; |
194 |
210 |
195 (** The following two can be expressed using intersection and subset, which |
211 (** The following two can be expressed using intersection and subset, which |
196 is more faithful to the text but looks cryptic. |
212 is more faithful to the text but looks cryptic. |
197 **) |
213 **) |
198 |
214 |
199 Goalw [guarantees_def] |
215 Goalw [guar_def] |
200 "[| F : V guar X; F : (X Int Y) guar Z |]\ |
216 "[| F : V guarantees X; F : (X Int Y) guarantees Z |]\ |
201 \ ==> F : (V Int Y) guar Z"; |
217 \ ==> F : (V Int Y) guarantees Z"; |
202 by (Blast_tac 1); |
218 by (Blast_tac 1); |
203 qed "combining1"; |
219 qed "combining1"; |
204 |
220 |
205 Goalw [guarantees_def] |
221 Goalw [guar_def] |
206 "[| F : V guar (X Un Y); F : Y guar Z |]\ |
222 "[| F : V guarantees (X Un Y); F : Y guarantees Z |]\ |
207 \ ==> F : V guar (X Un Z)"; |
223 \ ==> F : V guarantees (X Un Z)"; |
208 by (Blast_tac 1); |
224 by (Blast_tac 1); |
209 qed "combining2"; |
225 qed "combining2"; |
210 |
226 |
211 (** The following two follow Chandy-Sanders, but the use of object-quantifiers |
227 (** The following two follow Chandy-Sanders, but the use of object-quantifiers |
212 does not suit Isabelle... **) |
228 does not suit Isabelle... **) |
213 |
229 |
214 (*Premise should be (!!i. i: I ==> F: X guar Y i) *) |
230 (*Premise should be (!!i. i: I ==> F: X guarantees Y i) *) |
215 Goalw [guarantees_def] |
231 Goalw [guar_def] |
216 "ALL i:I. F : X guar (Y i) ==> F : X guar (INT i:I. Y i)"; |
232 "ALL i:I. F : X guarantees (Y i) ==> F : X guarantees (INT i:I. Y i)"; |
217 by (Blast_tac 1); |
233 by (Blast_tac 1); |
218 qed "all_guarantees"; |
234 qed "all_guarantees"; |
219 |
235 |
220 (*Premises should be [| F: X guar Y i; i: I |] *) |
236 (*Premises should be [| F: X guarantees Y i; i: I |] *) |
221 Goalw [guarantees_def] |
237 Goalw [guar_def] |
222 "EX i:I. F : X guar (Y i) ==> F : X guar (UN i:I. Y i)"; |
238 "EX i:I. F : X guarantees (Y i) ==> F : X guarantees (UN i:I. Y i)"; |
223 by (Blast_tac 1); |
239 by (Blast_tac 1); |
224 qed "ex_guarantees"; |
240 qed "ex_guarantees"; |
225 |
241 |
226 (*** Additional guarantees laws, by lcp ***) |
242 (*** Additional guarantees laws, by lcp ***) |
227 |
243 |
228 Goalw [guarantees_def] |
244 Goalw [guar_def] |
229 "[| F: U guar V; G: X guar Y |] ==> F Join G: (U Int X) guar (V Int Y)"; |
245 "[| F: U guarantees V; G: X guarantees Y |] \ |
|
246 \ ==> F Join G: (U Int X) guarantees (V Int Y)"; |
230 by (simp_tac (simpset() addsimps [Join_component_iff]) 1); |
247 by (simp_tac (simpset() addsimps [Join_component_iff]) 1); |
231 by (Blast_tac 1); |
248 by (Blast_tac 1); |
232 qed "guarantees_Join_Int"; |
249 qed "guarantees_Join_Int"; |
233 |
250 |
234 Goalw [guarantees_def] |
251 Goalw [guar_def] |
235 "[| F: U guar V; G: X guar Y |] ==> F Join G: (U Un X) guar (V Un Y)"; |
252 "[| F: U guarantees V; G: X guarantees Y |] \ |
|
253 \ ==> F Join G: (U Un X) guarantees (V Un Y)"; |
236 by (simp_tac (simpset() addsimps [Join_component_iff]) 1); |
254 by (simp_tac (simpset() addsimps [Join_component_iff]) 1); |
237 by (Blast_tac 1); |
255 by (Blast_tac 1); |
238 qed "guarantees_Join_Un"; |
256 qed "guarantees_Join_Un"; |
239 |
257 |
240 Goal "((JOIN I F) component H) = (ALL i: I. F i component H)"; |
258 Goal "((JOIN I F) component H) = (ALL i: I. F i component H)"; |
241 by (simp_tac (simpset() addsimps [component_eq_subset, Acts_JN]) 1); |
259 by (simp_tac (simpset() addsimps [component_eq_subset, Acts_JN]) 1); |
242 by (Blast_tac 1); |
260 by (Blast_tac 1); |
243 qed "JN_component_iff"; |
261 qed "JN_component_iff"; |
244 |
262 |
245 Goalw [guarantees_def] |
263 Goalw [guar_def] |
246 "[| ALL i:I. F i : X i guar Y i |] \ |
264 "[| ALL i:I. F i : X i guarantees Y i |] \ |
247 \ ==> (JOIN I F) : (INTER I X) guar (INTER I Y)"; |
265 \ ==> (JOIN I F) : (INTER I X) guarantees (INTER I Y)"; |
248 by (simp_tac (simpset() addsimps [JN_component_iff]) 1); |
266 by (simp_tac (simpset() addsimps [JN_component_iff]) 1); |
249 by (Blast_tac 1); |
267 by (Blast_tac 1); |
250 bind_thm ("guarantees_JN_INT", ballI RS result()); |
268 bind_thm ("guarantees_JN_INT", ballI RS result()); |
251 |
269 |
252 Goalw [guarantees_def] |
270 Goalw [guar_def] |
253 "[| ALL i:I. F i : X i guar Y i |] \ |
271 "[| ALL i:I. F i : X i guarantees Y i |] \ |
254 \ ==> (JOIN I F) : (UNION I X) guar (UNION I Y)"; |
272 \ ==> (JOIN I F) : (UNION I X) guarantees (UNION I Y)"; |
255 by (simp_tac (simpset() addsimps [JN_component_iff]) 1); |
273 by (simp_tac (simpset() addsimps [JN_component_iff]) 1); |
256 by (Blast_tac 1); |
274 by (Blast_tac 1); |
257 bind_thm ("guarantees_JN_UN", ballI RS result()); |
275 bind_thm ("guarantees_JN_UN", ballI RS result()); |
258 |
276 |
259 |
277 |
260 (*** guarantees laws for breaking down the program, by lcp ***) |
278 (*** guarantees laws for breaking down the program, by lcp ***) |
261 |
279 |
262 Goalw [guarantees_def] |
280 Goalw [guar_def] |
263 "F: X guar Y | G: X guar Y ==> F Join G: X guar Y"; |
281 "F: X guarantees Y | G: X guarantees Y ==> F Join G: X guarantees Y"; |
264 by (simp_tac (simpset() addsimps [Join_component_iff]) 1); |
282 by (simp_tac (simpset() addsimps [Join_component_iff]) 1); |
265 by (Blast_tac 1); |
283 by (Blast_tac 1); |
266 qed "guarantees_Join_I"; |
284 qed "guarantees_Join_I"; |
267 |
285 |
268 Goalw [guarantees_def] |
286 Goalw [guar_def] |
269 "[| i : I; F i: X guar Y |] ==> (JN i:I. (F i)) : X guar Y"; |
287 "[| i : I; F i: X guarantees Y |] ==> (JN i:I. (F i)) : X guarantees Y"; |
270 by (simp_tac (simpset() addsimps [JN_component_iff]) 1); |
288 by (simp_tac (simpset() addsimps [JN_component_iff]) 1); |
271 by (Blast_tac 1); |
289 by (Blast_tac 1); |
272 qed "guarantees_JN_I"; |
290 qed "guarantees_JN_I"; |
273 |
291 |
274 |
292 |