131 Goalw [guar_def] |
132 Goalw [guar_def] |
132 "Z guarantees[v] (X Int Y) = (Z guarantees[v] X) Int (Z guarantees[v] Y)"; |
133 "Z guarantees[v] (X Int Y) = (Z guarantees[v] X) Int (Z guarantees[v] Y)"; |
133 by (Blast_tac 1); |
134 by (Blast_tac 1); |
134 qed "guarantees_Int_right"; |
135 qed "guarantees_Int_right"; |
135 |
136 |
|
137 Goal "(F : X guarantees[v] (INTER I Y)) = \ |
|
138 \ (ALL i:I. F : X guarantees[v] (Y i))"; |
|
139 by (simp_tac (simpset() addsimps [guarantees_INT_right]) 1); |
|
140 qed "guarantees_INT_right_iff"; |
|
141 |
136 Goalw [guar_def] "(X guarantees[v] Y) = (UNIV guarantees[v] (-X Un Y))"; |
142 Goalw [guar_def] "(X guarantees[v] Y) = (UNIV guarantees[v] (-X Un Y))"; |
137 by (Blast_tac 1); |
143 by (Blast_tac 1); |
138 qed "shunting"; |
144 qed "shunting"; |
139 |
145 |
140 Goalw [guar_def] "(X guarantees[v] Y) = -Y guarantees[v] -X"; |
146 Goalw [guar_def] "(X guarantees[v] Y) = -Y guarantees[v] -X"; |
178 "[| F: U guarantees[v] V; G: X guarantees[v] Y; \ |
184 "[| F: U guarantees[v] V; G: X guarantees[v] Y; \ |
179 \ F : preserves v; G : preserves v |] \ |
185 \ F : preserves v; G : preserves v |] \ |
180 \ ==> F Join G: (U Int X) guarantees[v] (V Int Y)"; |
186 \ ==> F Join G: (U Int X) guarantees[v] (V Int Y)"; |
181 by (Simp_tac 1); |
187 by (Simp_tac 1); |
182 by Safe_tac; |
188 by Safe_tac; |
183 by (asm_full_simp_tac (simpset() addsimps [Join_preserves, Join_assoc]) 1); |
189 by (asm_full_simp_tac (simpset() addsimps [Join_assoc]) 1); |
184 by (subgoal_tac "F Join G Join Ga = G Join (F Join Ga)" 1); |
190 by (subgoal_tac "F Join G Join Ga = G Join (F Join Ga)" 1); |
185 by (asm_full_simp_tac (simpset() addsimps [Join_preserves]) 1); |
191 by (Asm_full_simp_tac 1); |
186 by (asm_simp_tac (simpset() addsimps Join_ac) 1); |
192 by (asm_simp_tac (simpset() addsimps Join_ac) 1); |
187 qed "guarantees_Join_Int"; |
193 qed "guarantees_Join_Int"; |
188 |
194 |
189 Goalw [guar_def] |
195 Goalw [guar_def] |
190 "[| F: U guarantees[v] V; G: X guarantees[v] Y; \ |
196 "[| F: U guarantees[v] V; G: X guarantees[v] Y; \ |
191 \ F : preserves v; G : preserves v |] \ |
197 \ F : preserves v; G : preserves v |] \ |
192 \ ==> F Join G: (U Un X) guarantees[v] (V Un Y)"; |
198 \ ==> F Join G: (U Un X) guarantees[v] (V Un Y)"; |
193 by (Simp_tac 1); |
199 by (Simp_tac 1); |
194 by Safe_tac; |
200 by Safe_tac; |
195 by (asm_full_simp_tac (simpset() addsimps [Join_preserves, Join_assoc]) 1); |
201 by (asm_full_simp_tac (simpset() addsimps [Join_assoc]) 1); |
196 by (subgoal_tac "F Join G Join Ga = G Join (F Join Ga)" 1); |
202 by (subgoal_tac "F Join G Join Ga = G Join (F Join Ga)" 1); |
197 by (asm_full_simp_tac (simpset() addsimps [Join_preserves]) 1); |
203 by (Asm_full_simp_tac 1); |
198 by (asm_simp_tac (simpset() addsimps Join_ac) 1); |
204 by (asm_simp_tac (simpset() addsimps Join_ac) 1); |
199 qed "guarantees_Join_Un"; |
205 qed "guarantees_Join_Un"; |
200 |
206 |
201 Goalw [guar_def] |
207 Goalw [guar_def] |
202 "[| ALL i:I. F i : X i guarantees[v] Y i; \ |
208 "[| ALL i:I. F i : X i guarantees[v] Y i; \ |
203 \ ALL i:I. F i : preserves v |] \ |
209 \ ALL i:I. F i : preserves v |] \ |
204 \ ==> (JOIN I F) : (INTER I X) guarantees[v] (INTER I Y)"; |
210 \ ==> (JOIN I F) : (INTER I X) guarantees[v] (INTER I Y)"; |
205 by Auto_tac; |
211 by Auto_tac; |
206 by (ball_tac 1); |
212 by (ball_tac 1); |
207 by (dres_inst_tac [("x", "JOIN I F Join G")] spec 1); |
213 by (dres_inst_tac [("x", "JOIN I F Join G")] spec 1); |
208 by (asm_full_simp_tac (simpset() addsimps [Join_assoc RS sym, JN_absorb, |
214 by (asm_full_simp_tac (simpset() addsimps [Join_assoc RS sym, JN_absorb]) 1); |
209 Join_preserves, JN_preserves]) 1); |
|
210 qed "guarantees_JN_INT"; |
215 qed "guarantees_JN_INT"; |
211 |
216 |
212 Goalw [guar_def] |
217 Goalw [guar_def] |
213 "[| ALL i:I. F i : X i guarantees[v] Y i; \ |
218 "[| ALL i:I. F i : X i guarantees[v] Y i; \ |
214 \ ALL i:I. F i : preserves v |] \ |
219 \ ALL i:I. F i : preserves v |] \ |
216 by Auto_tac; |
221 by Auto_tac; |
217 by (ball_tac 1); |
222 by (ball_tac 1); |
218 by (dres_inst_tac [("x", "JOIN I F Join G")] spec 1); |
223 by (dres_inst_tac [("x", "JOIN I F Join G")] spec 1); |
219 by (auto_tac |
224 by (auto_tac |
220 (claset(), |
225 (claset(), |
221 simpset() addsimps [Join_assoc RS sym, JN_absorb, |
226 simpset() addsimps [Join_assoc RS sym, JN_absorb])); |
222 Join_preserves, JN_preserves])); |
|
223 qed "guarantees_JN_UN"; |
227 qed "guarantees_JN_UN"; |
224 |
228 |
225 |
229 |
226 (*** guarantees[v] laws for breaking down the program, by lcp ***) |
230 (*** guarantees[v] laws for breaking down the program, by lcp ***) |
227 |
231 |
228 Goalw [guar_def] |
232 Goalw [guar_def] |
229 "[| F: X guarantees[v] Y; G: preserves v |] \ |
233 "[| F: X guarantees[v] Y; G: preserves v |] \ |
230 \ ==> F Join G: X guarantees[v] Y"; |
234 \ ==> F Join G: X guarantees[v] Y"; |
231 by (Simp_tac 1); |
235 by (Simp_tac 1); |
232 by Safe_tac; |
236 by Safe_tac; |
233 by (asm_full_simp_tac (simpset() addsimps [Join_preserves, Join_assoc]) 1); |
237 by (asm_full_simp_tac (simpset() addsimps [Join_assoc]) 1); |
234 qed "guarantees_Join_I1"; |
238 qed "guarantees_Join_I1"; |
235 |
239 |
236 Goal "[| G: X guarantees[v] Y; F: preserves v |] \ |
240 Goal "[| G: X guarantees[v] Y; F: preserves v |] \ |
237 \ ==> F Join G: X guarantees[v] Y"; |
241 \ ==> F Join G: X guarantees[v] Y"; |
238 by (stac Join_commute 1); |
242 by (stac Join_commute 1); |
244 \ ALL j:I. i~=j --> F j : preserves v |] \ |
248 \ ALL j:I. i~=j --> F j : preserves v |] \ |
245 \ ==> (JN i:I. (F i)) : X guarantees[v] Y"; |
249 \ ==> (JN i:I. (F i)) : X guarantees[v] Y"; |
246 by (Clarify_tac 1); |
250 by (Clarify_tac 1); |
247 by (dres_inst_tac [("x", "JOIN (I-{i}) F Join G")] spec 1); |
251 by (dres_inst_tac [("x", "JOIN (I-{i}) F Join G")] spec 1); |
248 by (auto_tac (claset(), |
252 by (auto_tac (claset(), |
249 simpset() addsimps [JN_Join_diff, Join_assoc RS sym, |
253 simpset() addsimps [JN_Join_diff, Join_assoc RS sym])); |
250 Join_preserves, JN_preserves])); |
|
251 qed "guarantees_JN_I"; |
254 qed "guarantees_JN_I"; |
252 |
255 |
253 |
256 |
254 (*** well-definedness ***) |
257 (*** well-definedness ***) |
255 |
258 |