author | paulson |
Thu, 11 Nov 1999 10:25:17 +0100 | |
changeset 8005 | b64d86018785 |
parent 7965 | a00ad4ca6232 |
child 8041 | e3237d8c18d6 |
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 |
|
7841 | 8 |
Stop using o (composition)? |
7689 | 9 |
|
10 |
guarantees_PLam_I looks wrong: refers to lift_prog |
|
6828 | 11 |
*) |
12 |
||
7841 | 13 |
(*Eliminating the "o" operator gives associativity for free*) |
14 |
val o_simp = simplify (simpset() addsimps [o_def]); |
|
7399
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
15 |
|
7538 | 16 |
Goal "(ALL i: lessThan n. f i <= g i) --> sum f n <= sum g n"; |
17 |
by (induct_tac "n" 1); |
|
18 |
by Auto_tac; |
|
19 |
by (dres_inst_tac [("x","n")] bspec 1); |
|
20 |
by Auto_tac; |
|
21 |
by (arith_tac 1); |
|
22 |
qed_spec_mp "sum_mono"; |
|
23 |
||
7540 | 24 |
Goal "ALL xs. xs <= ys --> tokens xs <= tokens ys"; |
25 |
by (induct_tac "ys" 1); |
|
26 |
by (auto_tac (claset(), simpset() addsimps [prefix_Cons])); |
|
27 |
qed_spec_mp "tokens_mono_prefix"; |
|
28 |
||
29 |
Goalw [mono_def] "mono tokens"; |
|
30 |
by (blast_tac (claset() addIs [tokens_mono_prefix]) 1); |
|
31 |
qed "mono_tokens"; |
|
7399
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
32 |
|
6840 | 33 |
(*Generalized version allowing different clients*) |
34 |
Goal "[| Alloc : alloc_spec; \ |
|
35 |
\ Client : (lessThan Nclients) funcset client_spec; \ |
|
36 |
\ Network : network_spec |] \ |
|
37 |
\ ==> (extend sysOfAlloc Alloc) \ |
|
38 |
\ Join (extend sysOfClient (PLam (lessThan Nclients) Client)) \ |
|
39 |
\ Join Network : system_spec"; |
|
40 |
||
41 |
Goal "System : system_spec"; |
|
42 |
||
43 |
||
6828 | 44 |
Goalw [sysOfAlloc_def] "inj sysOfAlloc"; |
45 |
by (rtac injI 1); |
|
7347 | 46 |
by (auto_tac (claset() addSWrapper record_split_wrapper, simpset())); |
6828 | 47 |
qed "inj_sysOfAlloc"; |
48 |
||
49 |
Goalw [sysOfAlloc_def] "surj sysOfAlloc"; |
|
50 |
by (res_inst_tac [("f", "%s. ((| allocGiv = allocGiv s, \ |
|
51 |
\ allocAsk = allocAsk s, \ |
|
52 |
\ allocRel = allocRel s |), \ |
|
53 |
\ client s)")] surjI 1); |
|
7347 | 54 |
by (auto_tac (claset() addSWrapper record_split_wrapper, simpset())); |
6828 | 55 |
qed "surj_sysOfAlloc"; |
56 |
||
57 |
AddIffs [inj_sysOfAlloc, surj_sysOfAlloc]; |
|
58 |
||
7482 | 59 |
Goalw [good_map_def] "good_map sysOfAlloc"; |
60 |
by Auto_tac; |
|
61 |
qed "good_map_sysOfAlloc"; |
|
7689 | 62 |
Addsimps [good_map_sysOfAlloc]; |
7399
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
63 |
|
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
64 |
(*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
|
65 |
Goal "!!s. inv sysOfAlloc s = \ |
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
66 |
\ ((| allocGiv = allocGiv s, \ |
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
67 |
\ allocAsk = allocAsk s, \ |
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
68 |
\ allocRel = allocRel s|), \ |
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
69 |
\ client s)"; |
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
70 |
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
|
71 |
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
|
72 |
simpset() addsimps [sysOfAlloc_def])); |
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
73 |
qed "inv_sysOfAlloc_eq"; |
7538 | 74 |
Addsimps [inv_sysOfAlloc_eq]; |
7399
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
75 |
|
7365 | 76 |
(**SHOULD NOT BE NECESSARY: The various injections into the system |
77 |
state need to be treated symmetrically or done automatically*) |
|
7347 | 78 |
Goalw [sysOfClient_def] "inj sysOfClient"; |
79 |
by (rtac injI 1); |
|
80 |
by (auto_tac (claset() addSDs [inj_sysOfAlloc RS injD] |
|
7841 | 81 |
addSWrapper record_split_wrapper, |
82 |
simpset())); |
|
7347 | 83 |
qed "inj_sysOfClient"; |
84 |
||
85 |
Goalw [sysOfClient_def] "surj sysOfClient"; |
|
86 |
by (cut_facts_tac [surj_sysOfAlloc] 1); |
|
87 |
by (rewtac surj_def); |
|
88 |
by Auto_tac; |
|
89 |
by (Blast_tac 1); |
|
90 |
qed "surj_sysOfClient"; |
|
91 |
||
92 |
AddIffs [inj_sysOfClient, surj_sysOfClient]; |
|
93 |
||
7482 | 94 |
Goalw [good_map_def] "good_map sysOfClient"; |
95 |
by Auto_tac; |
|
96 |
qed "good_map_sysOfClient"; |
|
7689 | 97 |
Addsimps [good_map_sysOfClient]; |
6828 | 98 |
|
7347 | 99 |
(*MUST BE AUTOMATED: even the statement of such results*) |
100 |
Goal "!!s. inv sysOfClient s = \ |
|
101 |
\ (client s, \ |
|
102 |
\ (| allocGiv = allocGiv s, \ |
|
103 |
\ allocAsk = allocAsk s, \ |
|
104 |
\ allocRel = allocRel s|) )"; |
|
105 |
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
|
106 |
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
|
107 |
simpset() addsimps [sysOfAlloc_def, sysOfClient_def])); |
7365 | 108 |
qed "inv_sysOfClient_eq"; |
7689 | 109 |
Addsimps [inv_sysOfClient_eq]; |
6837 | 110 |
|
111 |
||
7365 | 112 |
Open_locale "System"; |
113 |
||
114 |
val Alloc = thm "Alloc"; |
|
115 |
val Client = thm "Client"; |
|
116 |
val Network = thm "Network"; |
|
117 |
val System_def = thm "System_def"; |
|
118 |
||
119 |
AddIffs [finite_lessThan]; |
|
120 |
||
121 |
(*Client : <unfolded specification> *) |
|
122 |
val Client_Spec = |
|
123 |
rewrite_rule [client_spec_def, client_increasing_def, |
|
124 |
client_bounded_def, client_progress_def] Client; |
|
125 |
||
126 |
Goal "Client : UNIV guarantees Increasing ask"; |
|
127 |
by (cut_facts_tac [Client_Spec] 1); |
|
128 |
by (asm_full_simp_tac (simpset() addsimps [guarantees_Int_right]) 1); |
|
129 |
qed "Client_Increasing_ask"; |
|
130 |
||
131 |
Goal "Client : UNIV guarantees Increasing rel"; |
|
132 |
by (cut_facts_tac [Client_Spec] 1); |
|
133 |
by (asm_full_simp_tac (simpset() addsimps [guarantees_Int_right]) 1); |
|
134 |
qed "Client_Increasing_rel"; |
|
135 |
||
136 |
AddIffs [Client_Increasing_ask, Client_Increasing_rel]; |
|
137 |
||
138 |
Goal "Client : UNIV guarantees Always {s. ALL elt : set (ask s). elt <= NbT}"; |
|
139 |
by (cut_facts_tac [Client_Spec] 1); |
|
140 |
by Auto_tac; |
|
141 |
qed "Client_Bounded"; |
|
142 |
||
143 |
(*Client_Progress is cumbersome to state*) |
|
144 |
val Client_Progress = Client_Spec RS IntD2; |
|
6828 | 145 |
|
146 |
||
7365 | 147 |
(*Network : <unfolded specification> *) |
148 |
val Network_Spec = |
|
149 |
rewrite_rule [network_spec_def, network_ask_def, |
|
150 |
network_giv_def, network_rel_def] Network; |
|
151 |
||
152 |
(*CANNOT use bind_thm: it puts the theorem into standard form, in effect |
|
153 |
exporting it from the locale*) |
|
7689 | 154 |
val Network_Ask = Network_Spec RS IntD1 RS IntD1 RS INT_D; |
7540 | 155 |
val Network_Giv = Network_Spec RS IntD1 RS IntD2 RS INT_D; |
7365 | 156 |
val Network_Rel = Network_Spec RS IntD2 RS INT_D; |
157 |
||
158 |
||
159 |
(*Alloc : <unfolded specification> *) |
|
160 |
val Alloc_Spec = |
|
161 |
rewrite_rule [alloc_spec_def, alloc_increasing_def, |
|
162 |
alloc_safety_def, alloc_progress_def] Alloc; |
|
163 |
||
7540 | 164 |
Goal "i < Nclients ==> Alloc : UNIV guarantees Increasing (sub i o allocGiv)"; |
7365 | 165 |
by (cut_facts_tac [Alloc_Spec] 1); |
166 |
by (asm_full_simp_tac (simpset() addsimps [guarantees_INT_right]) 1); |
|
167 |
qed "Alloc_Increasing"; |
|
168 |
||
169 |
val Alloc_Safety = Alloc_Spec RS IntD1 RS IntD2; |
|
170 |
val Alloc_Progress = (Alloc_Spec RS IntD2 |
|
171 |
|> simplify (simpset() addsimps [guarantees_INT_right])) |
|
172 |
RS bspec RS spec; |
|
173 |
||
174 |
||
7347 | 175 |
|
7365 | 176 |
(*Not sure what to say about the other components because they involve |
177 |
extend*) |
|
7399
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
178 |
Goalw [System_def] "Network <= System"; |
7365 | 179 |
by (blast_tac (claset() addIs [componentI]) 1); |
180 |
qed "Network_component_System"; |
|
181 |
||
7399
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
182 |
Goalw [System_def] "(extend sysOfAlloc Alloc) <= System"; |
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
183 |
by (blast_tac (claset() addIs [componentI]) 1); |
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
184 |
qed "Alloc_component_System"; |
7365 | 185 |
|
7399
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
186 |
AddIffs [Network_component_System, Alloc_component_System]; |
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
187 |
|
7365 | 188 |
|
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
189 |
fun alloc_export th = good_map_sysOfAlloc RS export th |> simplify (simpset()); |
7689 | 190 |
|
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
191 |
fun client_export th = good_map_sysOfClient RS export th |> simplify (simpset()); |
7689 | 192 |
|
7540 | 193 |
(*NEED AUTOMATIC PROPAGATION of Alloc_Increasing*) |
194 |
Goal "i < Nclients \ |
|
195 |
\ ==> extend sysOfAlloc Alloc : UNIV guarantees Increasing (sub i o allocGiv)"; |
|
196 |
by (dtac (Alloc_Increasing RS alloc_export extend_guar_Increasing) 1); |
|
197 |
by (auto_tac (claset(), simpset() addsimps [o_def])); |
|
198 |
qed "extend_Alloc_Increasing_allocGiv"; |
|
199 |
||
7841 | 200 |
Goalw [System_def] |
201 |
"i < Nclients ==> System : Increasing (sub i o allocGiv)"; |
|
202 |
by (rtac (extend_Alloc_Increasing_allocGiv RS |
|
203 |
guarantees_Join_I1 RS guaranteesD) 1); |
|
204 |
by Auto_tac; |
|
205 |
qed "System_Increasing_allocGiv"; |
|
7365 | 206 |
|
7841 | 207 |
|
7365 | 208 |
|
7841 | 209 |
Goalw [System_def] |
210 |
"i < Nclients ==> System : Increasing (ask o sub i o client)"; |
|
211 |
by (rtac (client_export extend_guar_Increasing RS guarantees_Join_I2 |
|
212 |
RS guaranteesD) 1); |
|
213 |
by (rtac (lift_prog_guar_Increasing RS guarantees_PLam_I) 1); |
|
214 |
by Auto_tac; |
|
215 |
qed "System_Increasing_ask"; |
|
216 |
||
7365 | 217 |
Goalw [System_def] |
218 |
"i < Nclients ==> System : Increasing (rel o sub i o client)"; |
|
7841 | 219 |
by (rtac (client_export extend_guar_Increasing RS guarantees_Join_I2 |
7689 | 220 |
RS guaranteesD) 1); |
221 |
by (rtac (lift_prog_guar_Increasing RS guarantees_PLam_I) 1); |
|
222 |
(*gets Client_Increasing_rel from simpset*) |
|
223 |
by Auto_tac; |
|
7347 | 224 |
qed "System_Increasing_rel"; |
6828 | 225 |
|
226 |
||
7841 | 227 |
(** Follows consequences. |
228 |
The "Always (INT ...) formulation expresses the general safety property |
|
229 |
and allows it to be combined using Always_Int_rule below. **) |
|
230 |
||
231 |
Goal "System : Always (INT i: lessThan Nclients. \ |
|
232 |
\ {s. (giv o sub i o client) s <= (sub i o allocGiv) s})"; |
|
233 |
by (auto_tac (claset(), |
|
234 |
simpset() delsimps [o_apply] |
|
235 |
addsimps [Always_INT_distrib, Follows_Bounded, |
|
236 |
Network_Giv RS component_guaranteesD, |
|
237 |
extend_Alloc_Increasing_allocGiv RS component_guaranteesD])); |
|
238 |
qed "Always_giv_le_allocGiv"; |
|
239 |
||
240 |
Goal "System : Always (INT i: lessThan Nclients. \ |
|
241 |
\ {s. (sub i o allocAsk) s <= (ask o sub i o client) s})"; |
|
242 |
by (auto_tac (claset(), |
|
243 |
simpset() delsimps [o_apply] |
|
244 |
addsimps [Always_INT_distrib, Follows_Bounded, |
|
245 |
[Network_Ask, System_Increasing_ask] MRS component_guaranteesD])); |
|
246 |
qed "Always_allocAsk_le_ask"; |
|
247 |
||
248 |
Goal "System : Always (INT i: lessThan Nclients. \ |
|
249 |
\ {s. (sub i o allocRel) s <= (rel o sub i o client) s})"; |
|
250 |
by (auto_tac (claset(), |
|
251 |
simpset() delsimps [o_apply] |
|
252 |
addsimps [Always_INT_distrib, Follows_Bounded, |
|
253 |
[Network_Rel, System_Increasing_rel] MRS component_guaranteesD])); |
|
254 |
qed "Always_allocRel_le_rel"; |
|
255 |
||
256 |
||
257 |
(*** Proof of the safety property (1) ***) |
|
258 |
||
259 |
(*safety (1), step 1 is System_Increasing_rel*) |
|
260 |
||
7689 | 261 |
(*safety (1), step 2*) |
7365 | 262 |
Goal "i < Nclients ==> System : Increasing (sub i o allocRel)"; |
263 |
by (rtac Follows_Increasing1 1); |
|
264 |
by (blast_tac (claset() addIs [Network_Rel RS component_guaranteesD, |
|
7540 | 265 |
System_Increasing_rel]) 1); |
7365 | 266 |
qed "System_Increasing_allocRel"; |
6828 | 267 |
|
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
268 |
|
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
269 |
|
7689 | 270 |
(*safety (1), step 3*) |
7399
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
271 |
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
|
272 |
\ <= 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
|
273 |
by (res_inst_tac |
7537 | 274 |
[("X", "(INT i : lessThan Nclients. Increasing (sub i o allocRel))")] |
275 |
component_guaranteesD 1); |
|
7482 | 276 |
by (rtac Alloc_component_System 3); |
7537 | 277 |
by (force_tac (claset(), simpset() addsimps [System_Increasing_allocRel]) 2); |
7538 | 278 |
by (rtac (Alloc_Safety RS project_guarantees) 1); |
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
279 |
(*1: Increasing precondition*) |
7841 | 280 |
by (rtac (alloc_export projecting_Increasing RS projecting_weaken RS |
281 |
projecting_INT) 1); |
|
7537 | 282 |
by Auto_tac; |
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
283 |
by (asm_full_simp_tac (simpset() addsimps [o_def]) 1); |
7538 | 284 |
(*2: Always postcondition*) |
7826
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
285 |
by (rtac ((alloc_export extending_Always RS extending_weaken)) 1); |
c6a8b73b6c2a
working shapshot with "projecting" and "extending"
paulson
parents:
7689
diff
changeset
|
286 |
by Auto_tac; |
7538 | 287 |
by (asm_full_simp_tac |
288 |
(simpset() addsimps [alloc_export Collect_eq_extend_set RS sym]) 1); |
|
289 |
qed "System_sum_bounded"; |
|
7537 | 290 |
|
7841 | 291 |
(** Follows reasoning **) |
292 |
||
7540 | 293 |
Goal "System : Always (INT i: lessThan Nclients. \ |
294 |
\ {s. (tokens o giv o sub i o client) s \ |
|
295 |
\ <= (tokens o sub i o allocGiv) s})"; |
|
7841 | 296 |
by (rtac (Always_giv_le_allocGiv RS Always_weaken) 1); |
297 |
by (auto_tac (claset() addIs [tokens_mono_prefix], simpset())); |
|
298 |
qed "Always_tokens_giv_le_allocGiv"; |
|
7540 | 299 |
|
300 |
Goal "System : Always (INT i: lessThan Nclients. \ |
|
301 |
\ {s. (tokens o sub i o allocRel) s \ |
|
302 |
\ <= (tokens o rel o sub i o client) s})"; |
|
7841 | 303 |
by (rtac (Always_allocRel_le_rel RS Always_weaken) 1); |
304 |
by (auto_tac (claset() addIs [tokens_mono_prefix], simpset())); |
|
305 |
qed "Always_tokens_allocRel_le_rel"; |
|
7540 | 306 |
|
7841 | 307 |
(*safety (1), step 4 (final result!) *) |
7540 | 308 |
Goal "System : Always {s. sum (%i. (tokens o giv o sub i o client)s) Nclients \ |
309 |
\ <= NbT + sum (%i. (tokens o rel o sub i o client)s) Nclients}"; |
|
7841 | 310 |
by (rtac (Always_Int_rule [System_sum_bounded, Always_tokens_giv_le_allocGiv, |
311 |
Always_tokens_allocRel_le_rel] RS Always_weaken) 1); |
|
7538 | 312 |
by Auto_tac; |
7540 | 313 |
by (rtac (sum_mono RS order_trans) 1); |
314 |
by (dtac order_trans 2); |
|
315 |
by (rtac ([order_refl, sum_mono] MRS add_le_mono) 2); |
|
316 |
by (assume_tac 3); |
|
7482 | 317 |
by Auto_tac; |
7540 | 318 |
qed "System_safety"; |
7399
cf780c2bcccf
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
paulson
parents:
7365
diff
changeset
|
319 |
|
7689 | 320 |
|
321 |
||
322 |
(*** Proof of the progress property (2) ***) |
|
323 |
||
7965 | 324 |
(** Lemmas about localTo **) |
325 |
||
326 |
Goal "extend sysOfAlloc F : client localTo[C] extend sysOfClient G"; |
|
327 |
by (rtac localTo_UNIV_imp_localTo 1); |
|
328 |
by (simp_tac (simpset() addsimps [LOCALTO_def, Diff_def, extend_def, |
|
329 |
stable_def, constrains_def, |
|
330 |
image_eq_UN, extend_act_def, |
|
331 |
sysOfAlloc_def, sysOfClient_def]) 1); |
|
332 |
by (Force_tac 1); |
|
333 |
qed "sysOfAlloc_in_client_localTo_xl_Client"; |
|
334 |
||
335 |
Goal "extend sysOfClient (plam i:I. F) : \ |
|
336 |
\ (sub i o client) localTo[C] extend sysOfClient (lift_prog i F)"; |
|
337 |
by (rtac localTo_UNIV_imp_localTo 1); |
|
338 |
by (rtac (client_export (extend_set_UNIV_eq RS equalityD2 RSN |
|
339 |
(2, extend_localTo_extend_I))) 1); |
|
340 |
by (rtac PLam_sub_localTo 1); |
|
341 |
qed "sysOfClient_in_client_localTo_xl_Client"; |
|
342 |
||
343 |
||
344 |
(*Now there are proofs identical to System_Increasing_rel and |
|
7689 | 345 |
System_Increasing_allocRel: tactics needed!*) |
346 |
||
7841 | 347 |
(*progress (2), step 1 is System_Increasing_ask and System_Increasing_rel*) |
7689 | 348 |
|
7841 | 349 |
(*progress (2), step 2; see also System_Increasing_allocRel*) |
7689 | 350 |
Goal "i < Nclients ==> System : Increasing (sub i o allocAsk)"; |
351 |
by (rtac Follows_Increasing1 1); |
|
352 |
by (blast_tac (claset() addIs [Network_Ask RS component_guaranteesD, |
|
353 |
System_Increasing_ask]) 1); |
|
354 |
qed "System_Increasing_allocAsk"; |
|
355 |
||
7841 | 356 |
val Client_i_Bounded = |
357 |
[Client_Bounded, projecting_UNIV, lift_export extending_Always] |
|
358 |
MRS drop_prog_guarantees; |
|
359 |
||
360 |
val UNIV_guar_Always = |
|
361 |
[asm_rl, projecting_UNIV, extending_Always] |
|
362 |
MRS project_guarantees; |
|
363 |
||
364 |
||
7689 | 365 |
(*progress (2), step 3*) |
7841 | 366 |
(*All this trouble just to lift "Client_Bounded" through two extend ops*) |
7689 | 367 |
Goalw [System_def] |
368 |
"i < Nclients \ |
|
369 |
\ ==> System : Always \ |
|
370 |
\ {s. ALL elt : set ((ask o sub i o client) s). elt <= NbT}"; |
|
7841 | 371 |
by (rtac (guarantees_PLam_I RS client_export UNIV_guar_Always RS |
7689 | 372 |
guarantees_Join_I2 RS guaranteesD RS Always_weaken) 1); |
7841 | 373 |
by (rtac Client_i_Bounded 1); |
7689 | 374 |
by (auto_tac(claset(), |
7841 | 375 |
simpset() addsimps [lift_export Collect_eq_extend_set RS sym, |
7689 | 376 |
client_export Collect_eq_extend_set RS sym])); |
7841 | 377 |
qed "System_Bounded_ask"; |
378 |
||
379 |
(*progress (2), step 4*) |
|
380 |
Goal "System : Always {s. ALL i : lessThan Nclients. \ |
|
381 |
\ ALL elt : set ((sub i o allocAsk) s). elt <= NbT}"; |
|
382 |
by (auto_tac (claset(), |
|
383 |
simpset() addsimps [Collect_ball_eq, Always_INT_distrib])); |
|
384 |
by (rtac (Always_Int_rule [Always_allocAsk_le_ask, System_Bounded_ask] |
|
385 |
RS Always_weaken) 1); |
|
386 |
by (auto_tac(claset() addDs [set_mono], simpset())); |
|
387 |
qed "System_Bounded_allocAsk"; |
|
388 |
||
7965 | 389 |
(*progress (2), step 5 is System_Increasing_allocGiv*) |
7841 | 390 |
|
7965 | 391 |
(*progress (2), step 6*) |
7841 | 392 |
Goal "i < Nclients ==> System : Increasing (giv o sub i o client)"; |
393 |
by (rtac Follows_Increasing1 1); |
|
394 |
by (blast_tac (claset() addIs [Network_Giv RS component_guaranteesD, |
|
395 |
System_Increasing_allocGiv]) 1); |
|
396 |
qed "System_Increasing_giv"; |
|
397 |
||
7965 | 398 |
(*Lemma (?). A LOT of work just to lift "Client_Progress" to the array*) |
7841 | 399 |
Goal "lift_prog i Client \ |
7965 | 400 |
\ : Increasing (giv o sub i) Int (sub i LocalTo (lift_prog i Client)) \ |
7841 | 401 |
\ guarantees \ |
402 |
\ (INT h. {s. h <= (giv o sub i) s & \ |
|
403 |
\ h pfixGe (ask o sub i) s} \ |
|
404 |
\ LeadsTo {s. tokens h <= (tokens o rel o sub i) s})"; |
|
7878
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
405 |
by (rtac (Client_Progress RS drop_prog_guarantees) 1); |
7965 | 406 |
by (rtac (lift_export extending_LeadsTo RS extending_weaken RS |
407 |
extending_INT) 2); |
|
7878
43b03d412b82
working version with localTo[C] instead of localTo
paulson
parents:
7841
diff
changeset
|
408 |
by (rtac subset_refl 4); |
7841 | 409 |
by (simp_tac (simpset()addsimps [lift_export Collect_eq_extend_set RS sym]) 3); |
7965 | 410 |
by (force_tac (claset(), simpset() addsimps [sub_def, lift_prog_correct]) 2); |
7841 | 411 |
by (rtac (lift_export projecting_Increasing RS projecting_weaken) 1); |
412 |
by (auto_tac (claset(), simpset() addsimps [o_def])); |
|
413 |
qed "Client_i_Progress"; |
|
414 |
||
7965 | 415 |
(*needed??*) |
416 |
Goalw [PLam_def] |
|
417 |
"(plam x:lessThan Nclients. Client) \ |
|
418 |
\ : (INT i : lessThan Nclients. \ |
|
419 |
\ Increasing (giv o sub i) Int (sub i LocalTo (lift_prog i Client))) \ |
|
420 |
\ guarantees \ |
|
421 |
\ (INT i : lessThan Nclients. \ |
|
422 |
\ INT h. {s. h <= (giv o sub i) s & \ |
|
423 |
\ h pfixGe (ask o sub i) s} \ |
|
424 |
\ LeadsTo {s. tokens h <= (tokens o rel o sub i) s})"; |
|
425 |
br guarantees_JN_INT 1; |
|
426 |
br Client_i_Progress 1; |
|
427 |
qed "PLam_Client_Progress"; |
|
7947 | 428 |
|
7965 | 429 |
(*progress (2), step 7*) |