author | paulson |
Mon, 04 Oct 1999 13:47:28 +0200 | |
changeset 7689 | affe0c2fdfbf |
parent 7540 | 8af61a565a4a |
child 7826 | c6a8b73b6c2a |
permissions | -rw-r--r-- |
6828 | 1 |
(* Title: HOL/UNITY/Alloc |
2 |
ID: $Id$ |
|
3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
|
4 |
Copyright 1998 University of Cambridge |
|
5 |
||
6 |
Specification of Chandy and Charpentier's Allocator |
|
7540 | 7 |
|
8 |
STOP USING o (COMPOSITION), since function application is naturally associative |
|
7689 | 9 |
|
10 |
guarantees_PLam_I looks wrong: refers to lift_prog |
|
6828 | 11 |
*) |
12 |
||
7399
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
13 |
|
7538 | 14 |
Goal "(ALL i: lessThan n. f i <= g i) --> sum f n <= sum g n"; |
15 |
by (induct_tac "n" 1); |
|
16 |
by Auto_tac; |
|
17 |
by (dres_inst_tac [("x","n")] bspec 1); |
|
18 |
by Auto_tac; |
|
19 |
by (arith_tac 1); |
|
20 |
qed_spec_mp "sum_mono"; |
|
21 |
||
7540 | 22 |
Goal "ALL xs. xs <= ys --> tokens xs <= tokens ys"; |
23 |
by (induct_tac "ys" 1); |
|
24 |
by (auto_tac (claset(), simpset() addsimps [prefix_Cons])); |
|
25 |
qed_spec_mp "tokens_mono_prefix"; |
|
26 |
||
27 |
Goalw [mono_def] "mono tokens"; |
|
28 |
by (blast_tac (claset() addIs [tokens_mono_prefix]) 1); |
|
29 |
qed "mono_tokens"; |
|
7399
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
30 |
|
6840 | 31 |
(*Generalized version allowing different clients*) |
32 |
Goal "[| Alloc : alloc_spec; \ |
|
33 |
\ Client : (lessThan Nclients) funcset client_spec; \ |
|
34 |
\ Network : network_spec |] \ |
|
35 |
\ ==> (extend sysOfAlloc Alloc) \ |
|
36 |
\ Join (extend sysOfClient (PLam (lessThan Nclients) Client)) \ |
|
37 |
\ Join Network : system_spec"; |
|
38 |
||
39 |
Goal "System : system_spec"; |
|
40 |
||
41 |
||
6828 | 42 |
Goalw [sysOfAlloc_def] "inj sysOfAlloc"; |
43 |
by (rtac injI 1); |
|
7347 | 44 |
by (auto_tac (claset() addSWrapper record_split_wrapper, simpset())); |
6828 | 45 |
qed "inj_sysOfAlloc"; |
46 |
||
47 |
Goalw [sysOfAlloc_def] "surj sysOfAlloc"; |
|
48 |
by (res_inst_tac [("f", "%s. ((| allocGiv = allocGiv s, \ |
|
49 |
\ allocAsk = allocAsk s, \ |
|
50 |
\ allocRel = allocRel s |), \ |
|
51 |
\ client s)")] surjI 1); |
|
7347 | 52 |
by (auto_tac (claset() addSWrapper record_split_wrapper, simpset())); |
6828 | 53 |
qed "surj_sysOfAlloc"; |
54 |
||
55 |
AddIffs [inj_sysOfAlloc, surj_sysOfAlloc]; |
|
56 |
||
7482 | 57 |
Goalw [good_map_def] "good_map sysOfAlloc"; |
58 |
by Auto_tac; |
|
59 |
qed "good_map_sysOfAlloc"; |
|
7689 | 60 |
Addsimps [good_map_sysOfAlloc]; |
7399
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
61 |
|
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
62 |
(*MUST BE AUTOMATED: even the statement of such results*) |
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
63 |
Goal "!!s. inv sysOfAlloc s = \ |
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
64 |
\ ((| allocGiv = allocGiv s, \ |
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
65 |
\ allocAsk = allocAsk s, \ |
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
66 |
\ allocRel = allocRel s|), \ |
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
67 |
\ client s)"; |
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
68 |
by (rtac (inj_sysOfAlloc RS inv_f_eq) 1); |
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
69 |
by (auto_tac (claset() addSWrapper record_split_wrapper, |
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
70 |
simpset() addsimps [sysOfAlloc_def])); |
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
71 |
qed "inv_sysOfAlloc_eq"; |
7538 | 72 |
Addsimps [inv_sysOfAlloc_eq]; |
7399
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
73 |
|
7365 | 74 |
(**SHOULD NOT BE NECESSARY: The various injections into the system |
75 |
state need to be treated symmetrically or done automatically*) |
|
7347 | 76 |
Goalw [sysOfClient_def] "inj sysOfClient"; |
77 |
by (rtac injI 1); |
|
78 |
by (auto_tac (claset() addSDs [inj_sysOfAlloc RS injD] |
|
79 |
addSWrapper record_split_wrapper, simpset())); |
|
80 |
qed "inj_sysOfClient"; |
|
81 |
||
82 |
Goalw [sysOfClient_def] "surj sysOfClient"; |
|
83 |
by (cut_facts_tac [surj_sysOfAlloc] 1); |
|
84 |
by (rewtac surj_def); |
|
85 |
by Auto_tac; |
|
86 |
by (Blast_tac 1); |
|
87 |
qed "surj_sysOfClient"; |
|
88 |
||
89 |
AddIffs [inj_sysOfClient, surj_sysOfClient]; |
|
90 |
||
7482 | 91 |
Goalw [good_map_def] "good_map sysOfClient"; |
92 |
by Auto_tac; |
|
93 |
qed "good_map_sysOfClient"; |
|
7689 | 94 |
Addsimps [good_map_sysOfClient]; |
6828 | 95 |
|
7347 | 96 |
(*MUST BE AUTOMATED: even the statement of such results*) |
97 |
Goal "!!s. inv sysOfClient s = \ |
|
98 |
\ (client s, \ |
|
99 |
\ (| allocGiv = allocGiv s, \ |
|
100 |
\ allocAsk = allocAsk s, \ |
|
101 |
\ allocRel = allocRel s|) )"; |
|
102 |
by (rtac (inj_sysOfClient RS inv_f_eq) 1); |
|
7399
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
103 |
by (auto_tac (claset() addSWrapper record_split_wrapper, |
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
104 |
simpset() addsimps [sysOfAlloc_def, sysOfClient_def])); |
7365 | 105 |
qed "inv_sysOfClient_eq"; |
7689 | 106 |
Addsimps [inv_sysOfClient_eq]; |
6837 | 107 |
|
108 |
||
7365 | 109 |
Open_locale "System"; |
110 |
||
111 |
val Alloc = thm "Alloc"; |
|
112 |
val Client = thm "Client"; |
|
113 |
val Network = thm "Network"; |
|
114 |
val System_def = thm "System_def"; |
|
115 |
||
116 |
AddIffs [finite_lessThan]; |
|
117 |
||
118 |
(*Client : <unfolded specification> *) |
|
119 |
val Client_Spec = |
|
120 |
rewrite_rule [client_spec_def, client_increasing_def, |
|
121 |
client_bounded_def, client_progress_def] Client; |
|
122 |
||
123 |
Goal "Client : UNIV guarantees Increasing ask"; |
|
124 |
by (cut_facts_tac [Client_Spec] 1); |
|
125 |
by (asm_full_simp_tac (simpset() addsimps [guarantees_Int_right]) 1); |
|
126 |
qed "Client_Increasing_ask"; |
|
127 |
||
128 |
Goal "Client : UNIV guarantees Increasing rel"; |
|
129 |
by (cut_facts_tac [Client_Spec] 1); |
|
130 |
by (asm_full_simp_tac (simpset() addsimps [guarantees_Int_right]) 1); |
|
131 |
qed "Client_Increasing_rel"; |
|
132 |
||
133 |
AddIffs [Client_Increasing_ask, Client_Increasing_rel]; |
|
134 |
||
135 |
Goal "Client : UNIV guarantees Always {s. ALL elt : set (ask s). elt <= NbT}"; |
|
136 |
by (cut_facts_tac [Client_Spec] 1); |
|
137 |
by Auto_tac; |
|
138 |
qed "Client_Bounded"; |
|
139 |
||
140 |
(*Client_Progress is cumbersome to state*) |
|
141 |
val Client_Progress = Client_Spec RS IntD2; |
|
6828 | 142 |
|
143 |
||
7365 | 144 |
(*Network : <unfolded specification> *) |
145 |
val Network_Spec = |
|
146 |
rewrite_rule [network_spec_def, network_ask_def, |
|
147 |
network_giv_def, network_rel_def] Network; |
|
148 |
||
149 |
(*CANNOT use bind_thm: it puts the theorem into standard form, in effect |
|
150 |
exporting it from the locale*) |
|
7689 | 151 |
val Network_Ask = Network_Spec RS IntD1 RS IntD1 RS INT_D; |
7540 | 152 |
val Network_Giv = Network_Spec RS IntD1 RS IntD2 RS INT_D; |
7365 | 153 |
val Network_Rel = Network_Spec RS IntD2 RS INT_D; |
154 |
||
155 |
||
156 |
(*Alloc : <unfolded specification> *) |
|
157 |
val Alloc_Spec = |
|
158 |
rewrite_rule [alloc_spec_def, alloc_increasing_def, |
|
159 |
alloc_safety_def, alloc_progress_def] Alloc; |
|
160 |
||
7540 | 161 |
Goal "i < Nclients ==> Alloc : UNIV guarantees Increasing (sub i o allocGiv)"; |
7365 | 162 |
by (cut_facts_tac [Alloc_Spec] 1); |
163 |
by (asm_full_simp_tac (simpset() addsimps [guarantees_INT_right]) 1); |
|
164 |
qed "Alloc_Increasing"; |
|
165 |
||
166 |
val Alloc_Safety = Alloc_Spec RS IntD1 RS IntD2; |
|
167 |
val Alloc_Progress = (Alloc_Spec RS IntD2 |
|
168 |
|> simplify (simpset() addsimps [guarantees_INT_right])) |
|
169 |
RS bspec RS spec; |
|
170 |
||
171 |
||
7347 | 172 |
|
7365 | 173 |
(*Not sure what to say about the other components because they involve |
174 |
extend*) |
|
7399
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
175 |
Goalw [System_def] "Network <= System"; |
7365 | 176 |
by (blast_tac (claset() addIs [componentI]) 1); |
177 |
qed "Network_component_System"; |
|
178 |
||
7399
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
179 |
Goalw [System_def] "(extend sysOfAlloc Alloc) <= System"; |
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
180 |
by (blast_tac (claset() addIs [componentI]) 1); |
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
181 |
qed "Alloc_component_System"; |
7365 | 182 |
|
7399
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
183 |
AddIffs [Network_component_System, Alloc_component_System]; |
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
184 |
|
7365 | 185 |
|
7689 | 186 |
fun alloc_export th = good_map_sysOfAlloc RS export th; |
187 |
||
188 |
fun client_export th = good_map_sysOfClient RS export th; |
|
189 |
||
7365 | 190 |
(* F : UNIV guarantees Increasing func |
191 |
==> extend sysOfClient F : UNIV guarantees Increasing (func o client) *) |
|
7399
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
192 |
val extend_Client_guar_Increasing = |
7689 | 193 |
client_export extend_guar_Increasing |
7365 | 194 |
|> simplify (simpset() addsimps [inv_sysOfClient_eq]); |
195 |
||
7540 | 196 |
(*NEED AUTOMATIC PROPAGATION of Alloc_Increasing*) |
197 |
Goal "i < Nclients \ |
|
198 |
\ ==> extend sysOfAlloc Alloc : UNIV guarantees Increasing (sub i o allocGiv)"; |
|
199 |
by (dtac (Alloc_Increasing RS alloc_export extend_guar_Increasing) 1); |
|
200 |
by (auto_tac (claset(), simpset() addsimps [o_def])); |
|
201 |
qed "extend_Alloc_Increasing_allocGiv"; |
|
202 |
||
7365 | 203 |
|
7689 | 204 |
(*** Proof of the safety property (1) ***) |
7365 | 205 |
|
7689 | 206 |
(*safety (1), step 1*) |
7365 | 207 |
Goalw [System_def] |
208 |
"i < Nclients ==> System : Increasing (rel o sub i o client)"; |
|
7689 | 209 |
by (rtac (extend_Client_guar_Increasing RS guarantees_Join_I2 |
210 |
RS guaranteesD) 1); |
|
211 |
by (rtac (lift_prog_guar_Increasing RS guarantees_PLam_I) 1); |
|
212 |
(*gets Client_Increasing_rel from simpset*) |
|
213 |
by Auto_tac; |
|
7347 | 214 |
qed "System_Increasing_rel"; |
6828 | 215 |
|
216 |
||
7689 | 217 |
(*safety (1), step 2*) |
7365 | 218 |
Goal "i < Nclients ==> System : Increasing (sub i o allocRel)"; |
219 |
by (rtac Follows_Increasing1 1); |
|
220 |
by (blast_tac (claset() addIs [Network_Rel RS component_guaranteesD, |
|
7540 | 221 |
System_Increasing_rel]) 1); |
7365 | 222 |
qed "System_Increasing_allocRel"; |
6828 | 223 |
|
7689 | 224 |
(*safety (1), step 3*) |
7399
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
225 |
Goal "System : Always {s. sum (%i. (tokens o sub i o allocGiv) s) Nclients \ |
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
226 |
\ <= NbT + sum (%i. (tokens o sub i o allocRel) s) Nclients}"; |
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
227 |
by (res_inst_tac |
7537 | 228 |
[("X", "(INT i : lessThan Nclients. Increasing (sub i o allocRel))")] |
229 |
component_guaranteesD 1); |
|
7482 | 230 |
by (rtac Alloc_component_System 3); |
7537 | 231 |
by (force_tac (claset(), simpset() addsimps [System_Increasing_allocRel]) 2); |
7538 | 232 |
by (rtac (Alloc_Safety RS project_guarantees) 1); |
7537 | 233 |
by Auto_tac; |
7538 | 234 |
(*1: Increasing precondition*) |
235 |
by (stac (alloc_export project_Increasing) 1); |
|
236 |
by (force_tac |
|
237 |
(claset(), |
|
238 |
simpset() addsimps [o_def, alloc_export project_Increasing]) 1); |
|
239 |
(*2: Always postcondition*) |
|
240 |
by (dtac (subset_refl RS alloc_export project_Always_D) 1); |
|
241 |
by (asm_full_simp_tac |
|
242 |
(simpset() addsimps [alloc_export Collect_eq_extend_set RS sym]) 1); |
|
243 |
qed "System_sum_bounded"; |
|
7537 | 244 |
|
7689 | 245 |
(*safety (1), step 4*) |
7540 | 246 |
Goal "System : Always (INT i: lessThan Nclients. \ |
247 |
\ {s. (tokens o giv o sub i o client) s \ |
|
248 |
\ <= (tokens o sub i o allocGiv) s})"; |
|
249 |
by (auto_tac (claset(), |
|
250 |
simpset() delsimps [o_apply] |
|
251 |
addsimps [Always_INT_distrib])); |
|
252 |
by (rtac Follows_Bounded 1); |
|
253 |
by (simp_tac (HOL_ss addsimps [o_assoc RS sym]) 1); |
|
254 |
by (rtac (mono_tokens RS mono_Follows_o RS subsetD) 1); |
|
255 |
by (simp_tac (HOL_ss addsimps [o_assoc]) 1); |
|
256 |
by (blast_tac (claset() addIs [Network_Giv RS component_guaranteesD, |
|
257 |
extend_Alloc_Increasing_allocGiv RS component_guaranteesD]) 1); |
|
258 |
qed "System_Always_giv_le_allocGiv"; |
|
259 |
||
260 |
||
7689 | 261 |
(*safety (1), step 5*) |
7540 | 262 |
Goal "System : Always (INT i: lessThan Nclients. \ |
263 |
\ {s. (tokens o sub i o allocRel) s \ |
|
264 |
\ <= (tokens o rel o sub i o client) s})"; |
|
265 |
by (auto_tac (claset(), |
|
266 |
simpset() delsimps [o_apply] |
|
267 |
addsimps [Always_INT_distrib])); |
|
268 |
by (rtac Follows_Bounded 1); |
|
269 |
by (simp_tac (HOL_ss addsimps [o_assoc RS sym]) 1); |
|
270 |
by (rtac (mono_tokens RS mono_Follows_o RS subsetD) 1); |
|
271 |
by (simp_tac (HOL_ss addsimps [o_assoc]) 1); |
|
272 |
by (blast_tac (claset() addIs [Network_Rel RS component_guaranteesD, |
|
273 |
System_Increasing_rel]) 1); |
|
274 |
qed "System_Always_allocRel_le_rel"; |
|
275 |
||
276 |
||
7689 | 277 |
(*safety (1), step 6*) |
7540 | 278 |
Goal "System : Always {s. sum (%i. (tokens o giv o sub i o client)s) Nclients \ |
279 |
\ <= NbT + sum (%i. (tokens o rel o sub i o client)s) Nclients}"; |
|
280 |
by (rtac (Always_Int_rule [System_sum_bounded, System_Always_giv_le_allocGiv, |
|
281 |
System_Always_allocRel_le_rel] RS Always_weaken) 1); |
|
7538 | 282 |
by Auto_tac; |
7540 | 283 |
by (rtac (sum_mono RS order_trans) 1); |
284 |
by (dtac order_trans 2); |
|
285 |
by (rtac ([order_refl, sum_mono] MRS add_le_mono) 2); |
|
286 |
by (assume_tac 3); |
|
7482 | 287 |
by Auto_tac; |
7540 | 288 |
qed "System_safety"; |
7399
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
289 |
|
7689 | 290 |
|
291 |
||
292 |
(*** Proof of the progress property (2) ***) |
|
293 |
||
294 |
(*we begin with proofs identical to System_Increasing_rel and |
|
295 |
System_Increasing_allocRel: tactics needed!*) |
|
296 |
||
297 |
(*progress (2), step 1*) |
|
298 |
Goalw [System_def] |
|
299 |
"i < Nclients ==> System : Increasing (ask o sub i o client)"; |
|
300 |
by (rtac (extend_Client_guar_Increasing RS guarantees_Join_I2 |
|
301 |
RS guaranteesD) 1); |
|
302 |
by (rtac (lift_prog_guar_Increasing RS guarantees_PLam_I) 1); |
|
303 |
by Auto_tac; |
|
304 |
qed "System_Increasing_ask"; |
|
305 |
||
306 |
(*progress (2), step 2*) |
|
307 |
Goal "i < Nclients ==> System : Increasing (sub i o allocAsk)"; |
|
308 |
by (rtac Follows_Increasing1 1); |
|
309 |
by (blast_tac (claset() addIs [Network_Ask RS component_guaranteesD, |
|
310 |
System_Increasing_ask]) 1); |
|
311 |
qed "System_Increasing_allocAsk"; |
|
312 |
||
313 |
(*progress (2), step 3*) |
|
314 |
(*All this trouble just to lift "Client_Bounded" through two extemd ops*) |
|
315 |
Goalw [System_def] |
|
316 |
"i < Nclients \ |
|
317 |
\ ==> System : Always \ |
|
318 |
\ {s. ALL elt : set ((ask o sub i o client) s). elt <= NbT}"; |
|
319 |
by (rtac (lift_prog_guar_Always RS |
|
320 |
guarantees_PLam_I RS client_export extend_guar_Always RS |
|
321 |
guarantees_Join_I2 RS guaranteesD RS Always_weaken) 1); |
|
322 |
by (stac Always_UNIV_eq 1 THEN rtac Client_Bounded 1); |
|
323 |
by (auto_tac(claset(), |
|
324 |
simpset() addsimps [Collect_eq_lift_set RS sym, |
|
325 |
client_export Collect_eq_extend_set RS sym])); |
|
326 |
qed "System_Bounded"; |