8 |
8 |
9 theory AllocImpl imports ClientImpl begin |
9 theory AllocImpl imports ClientImpl begin |
10 |
10 |
11 abbreviation |
11 abbreviation |
12 NbR :: i (*number of consumed messages*) where |
12 NbR :: i (*number of consumed messages*) where |
13 "NbR == Var([succ(2)])" |
13 "NbR \<equiv> Var([succ(2)])" |
14 |
14 |
15 abbreviation |
15 abbreviation |
16 available_tok :: i (*number of free tokens (T in paper)*) where |
16 available_tok :: i (*number of free tokens (T in paper)*) where |
17 "available_tok == Var([succ(succ(2))])" |
17 "available_tok \<equiv> Var([succ(succ(2))])" |
18 |
18 |
19 axiomatization where |
19 axiomatization where |
20 alloc_type_assumes [simp]: |
20 alloc_type_assumes [simp]: |
21 "type_of(NbR) = nat & type_of(available_tok)=nat" and |
21 "type_of(NbR) = nat & type_of(available_tok)=nat" and |
22 |
22 |
23 alloc_default_val_assumes [simp]: |
23 alloc_default_val_assumes [simp]: |
24 "default_val(NbR) = 0 & default_val(available_tok)=0" |
24 "default_val(NbR) = 0 & default_val(available_tok)=0" |
25 |
25 |
26 definition |
26 definition |
27 "alloc_giv_act == |
27 "alloc_giv_act \<equiv> |
28 {<s, t> \<in> state*state. |
28 {<s, t> \<in> state*state. |
29 \<exists>k. k = length(s`giv) & |
29 \<exists>k. k = length(s`giv) & |
30 t = s(giv := s`giv @ [nth(k, s`ask)], |
30 t = s(giv := s`giv @ [nth(k, s`ask)], |
31 available_tok := s`available_tok #- nth(k, s`ask)) & |
31 available_tok := s`available_tok #- nth(k, s`ask)) & |
32 k < length(s`ask) & nth(k, s`ask) \<le> s`available_tok}" |
32 k < length(s`ask) & nth(k, s`ask) \<le> s`available_tok}" |
33 |
33 |
34 definition |
34 definition |
35 "alloc_rel_act == |
35 "alloc_rel_act \<equiv> |
36 {<s, t> \<in> state*state. |
36 {<s, t> \<in> state*state. |
37 t = s(available_tok := s`available_tok #+ nth(s`NbR, s`rel), |
37 t = s(available_tok := s`available_tok #+ nth(s`NbR, s`rel), |
38 NbR := succ(s`NbR)) & |
38 NbR := succ(s`NbR)) & |
39 s`NbR < length(s`rel)}" |
39 s`NbR < length(s`rel)}" |
40 |
40 |
41 definition |
41 definition |
42 (*The initial condition s`giv=[] is missing from the |
42 (*The initial condition s`giv=[] is missing from the |
43 original definition: S. O. Ehmety *) |
43 original definition: S. O. Ehmety *) |
44 "alloc_prog == |
44 "alloc_prog \<equiv> |
45 mk_program({s:state. s`available_tok=NbT & s`NbR=0 & s`giv=Nil}, |
45 mk_program({s:state. s`available_tok=NbT & s`NbR=0 & s`giv=Nil}, |
46 {alloc_giv_act, alloc_rel_act}, |
46 {alloc_giv_act, alloc_rel_act}, |
47 \<Union>G \<in> preserves(lift(available_tok)) \<inter> |
47 \<Union>G \<in> preserves(lift(available_tok)) \<inter> |
48 preserves(lift(NbR)) \<inter> |
48 preserves(lift(NbR)) \<inter> |
49 preserves(lift(giv)). Acts(G))" |
49 preserves(lift(giv)). Acts(G))" |
50 |
50 |
51 |
51 |
52 lemma available_tok_value_type [simp,TC]: "s\<in>state ==> s`available_tok \<in> nat" |
52 lemma available_tok_value_type [simp,TC]: "s\<in>state \<Longrightarrow> s`available_tok \<in> nat" |
53 apply (unfold state_def) |
53 apply (unfold state_def) |
54 apply (drule_tac a = available_tok in apply_type, auto) |
54 apply (drule_tac a = available_tok in apply_type, auto) |
55 done |
55 done |
56 |
56 |
57 lemma NbR_value_type [simp,TC]: "s\<in>state ==> s`NbR \<in> nat" |
57 lemma NbR_value_type [simp,TC]: "s\<in>state \<Longrightarrow> s`NbR \<in> nat" |
58 apply (unfold state_def) |
58 apply (unfold state_def) |
59 apply (drule_tac a = NbR in apply_type, auto) |
59 apply (drule_tac a = NbR in apply_type, auto) |
60 done |
60 done |
61 |
61 |
62 (** The Alloc Program **) |
62 (** The Alloc Program **) |
139 apply (simp add: diff_add_0 add_commute diff_add_inverse add_assoc add_diff_inverse) |
139 apply (simp add: diff_add_0 add_commute diff_add_inverse add_assoc add_diff_inverse) |
140 apply (simp (no_asm_simp) add: take_succ) |
140 apply (simp (no_asm_simp) add: take_succ) |
141 done |
141 done |
142 |
142 |
143 lemma giv_Bounded_lemma2: |
143 lemma giv_Bounded_lemma2: |
144 "[| G \<in> program; alloc_prog ok G; alloc_prog \<squnion> G \<in> Incr(lift(rel)) |] |
144 "\<lbrakk>G \<in> program; alloc_prog ok G; alloc_prog \<squnion> G \<in> Incr(lift(rel))\<rbrakk> |
145 ==> alloc_prog \<squnion> G \<in> Stable({s\<in>state. s`NbR \<le> length(s`rel)} \<inter> |
145 \<Longrightarrow> alloc_prog \<squnion> G \<in> Stable({s\<in>state. s`NbR \<le> length(s`rel)} \<inter> |
146 {s\<in>state. s`available_tok #+ tokens(s`giv) = |
146 {s\<in>state. s`available_tok #+ tokens(s`giv) = |
147 NbT #+ tokens(take(s`NbR, s`rel))})" |
147 NbT #+ tokens(take(s`NbR, s`rel))})" |
148 apply (cut_tac giv_Bounded_lamma1) |
148 apply (cut_tac giv_Bounded_lamma1) |
149 apply (cut_tac alloc_prog_preserves_rel_ask_tok) |
149 apply (cut_tac alloc_prog_preserves_rel_ask_tok) |
150 apply (auto simp add: Collect_conj_eq [symmetric] alloc_prog_ok_iff) |
150 apply (auto simp add: Collect_conj_eq [symmetric] alloc_prog_ok_iff) |
212 subsection\<open>Towards proving the liveness property, (31)\<close> |
212 subsection\<open>Towards proving the liveness property, (31)\<close> |
213 |
213 |
214 subsubsection\<open>First, we lead up to a proof of Lemma 49, page 28.\<close> |
214 subsubsection\<open>First, we lead up to a proof of Lemma 49, page 28.\<close> |
215 |
215 |
216 lemma alloc_prog_transient_lemma: |
216 lemma alloc_prog_transient_lemma: |
217 "[|G \<in> program; k\<in>nat|] |
217 "\<lbrakk>G \<in> program; k\<in>nat\<rbrakk> |
218 ==> alloc_prog \<squnion> G \<in> |
218 \<Longrightarrow> alloc_prog \<squnion> G \<in> |
219 transient({s\<in>state. k \<le> length(s`rel)} \<inter> |
219 transient({s\<in>state. k \<le> length(s`rel)} \<inter> |
220 {s\<in>state. succ(s`NbR) = k})" |
220 {s\<in>state. succ(s`NbR) = k})" |
221 apply auto |
221 apply auto |
222 apply (erule_tac V = "G\<notin>u" for u in thin_rl) |
222 apply (erule_tac V = "G\<notin>u" for u in thin_rl) |
223 apply (rule_tac act = alloc_rel_act in transientI) |
223 apply (rule_tac act = alloc_rel_act in transientI) |
230 in exI) |
230 in exI) |
231 apply (auto intro!: state_update_type) |
231 apply (auto intro!: state_update_type) |
232 done |
232 done |
233 |
233 |
234 lemma alloc_prog_rel_Stable_NbR_lemma: |
234 lemma alloc_prog_rel_Stable_NbR_lemma: |
235 "[| G \<in> program; alloc_prog ok G; k\<in>nat |] |
235 "\<lbrakk>G \<in> program; alloc_prog ok G; k\<in>nat\<rbrakk> |
236 ==> alloc_prog \<squnion> G \<in> Stable({s\<in>state . k \<le> succ(s ` NbR)})" |
236 \<Longrightarrow> alloc_prog \<squnion> G \<in> Stable({s\<in>state . k \<le> succ(s ` NbR)})" |
237 apply (auto intro!: stable_imp_Stable simp add: alloc_prog_ok_iff, safety, auto) |
237 apply (auto intro!: stable_imp_Stable simp add: alloc_prog_ok_iff, safety, auto) |
238 apply (blast intro: le_trans leI) |
238 apply (blast intro: le_trans leI) |
239 apply (drule_tac f = "lift (NbR)" and A = nat in preserves_imp_increasing) |
239 apply (drule_tac f = "lift (NbR)" and A = nat in preserves_imp_increasing) |
240 apply (drule_tac [2] g = succ in imp_increasing_comp) |
240 apply (drule_tac [2] g = succ in imp_increasing_comp) |
241 apply (rule_tac [2] mono_succ) |
241 apply (rule_tac [2] mono_succ) |
242 apply (drule_tac [4] x = k in increasing_imp_stable) |
242 apply (drule_tac [4] x = k in increasing_imp_stable) |
243 prefer 5 apply (simp add: Le_def comp_def, auto) |
243 prefer 5 apply (simp add: Le_def comp_def, auto) |
244 done |
244 done |
245 |
245 |
246 lemma alloc_prog_NbR_LeadsTo_lemma: |
246 lemma alloc_prog_NbR_LeadsTo_lemma: |
247 "[| G \<in> program; alloc_prog ok G; |
247 "\<lbrakk>G \<in> program; alloc_prog ok G; |
248 alloc_prog \<squnion> G \<in> Incr(lift(rel)); k\<in>nat |] |
248 alloc_prog \<squnion> G \<in> Incr(lift(rel)); k\<in>nat\<rbrakk> |
249 ==> alloc_prog \<squnion> G \<in> |
249 \<Longrightarrow> alloc_prog \<squnion> G \<in> |
250 {s\<in>state. k \<le> length(s`rel)} \<inter> {s\<in>state. succ(s`NbR) = k} |
250 {s\<in>state. k \<le> length(s`rel)} \<inter> {s\<in>state. succ(s`NbR) = k} |
251 \<longmapsto>w {s\<in>state. k \<le> s`NbR}" |
251 \<longmapsto>w {s\<in>state. k \<le> s`NbR}" |
252 apply (subgoal_tac "alloc_prog \<squnion> G \<in> Stable ({s\<in>state. k \<le> length (s`rel)})") |
252 apply (subgoal_tac "alloc_prog \<squnion> G \<in> Stable ({s\<in>state. k \<le> length (s`rel)})") |
253 apply (drule_tac [2] a = k and g1 = length in imp_Increasing_comp [THEN Increasing_imp_Stable]) |
253 apply (drule_tac [2] a = k and g1 = length in imp_Increasing_comp [THEN Increasing_imp_Stable]) |
254 apply (rule_tac [2] mono_length) |
254 apply (rule_tac [2] mono_length) |
262 apply (rule alloc_prog_transient_lemma [THEN transient_imp_leadsTo, THEN leadsTo_imp_LeadsTo], assumption+) |
262 apply (rule alloc_prog_transient_lemma [THEN transient_imp_leadsTo, THEN leadsTo_imp_LeadsTo], assumption+) |
263 apply (auto dest: not_lt_imp_le elim: lt_asym simp add: le_iff) |
263 apply (auto dest: not_lt_imp_le elim: lt_asym simp add: le_iff) |
264 done |
264 done |
265 |
265 |
266 lemma alloc_prog_NbR_LeadsTo_lemma2 [rule_format]: |
266 lemma alloc_prog_NbR_LeadsTo_lemma2 [rule_format]: |
267 "[| G \<in> program; alloc_prog ok G; alloc_prog \<squnion> G \<in> Incr(lift(rel)); |
267 "\<lbrakk>G \<in> program; alloc_prog ok G; alloc_prog \<squnion> G \<in> Incr(lift(rel)); |
268 k\<in>nat; n \<in> nat; n < k |] |
268 k\<in>nat; n \<in> nat; n < k\<rbrakk> |
269 ==> alloc_prog \<squnion> G \<in> |
269 \<Longrightarrow> alloc_prog \<squnion> G \<in> |
270 {s\<in>state . k \<le> length(s ` rel)} \<inter> {s\<in>state . s ` NbR = n} |
270 {s\<in>state . k \<le> length(s ` rel)} \<inter> {s\<in>state . s ` NbR = n} |
271 \<longmapsto>w {x \<in> state. k \<le> length(x`rel)} \<inter> |
271 \<longmapsto>w {x \<in> state. k \<le> length(x`rel)} \<inter> |
272 (\<Union>m \<in> greater_than(n). {x \<in> state. x ` NbR=m})" |
272 (\<Union>m \<in> greater_than(n). {x \<in> state. x ` NbR=m})" |
273 apply (unfold greater_than_def) |
273 apply (unfold greater_than_def) |
274 apply (rule_tac A' = "{x \<in> state. k \<le> length(x`rel)} \<inter> {x \<in> state. n < x`NbR}" |
274 apply (rule_tac A' = "{x \<in> state. k \<le> length(x`rel)} \<inter> {x \<in> state. n < x`NbR}" |
290 apply simp_all |
290 apply simp_all |
291 apply (rule subset_imp_LeadsTo, auto) |
291 apply (rule subset_imp_LeadsTo, auto) |
292 apply (blast intro: lt_trans2) |
292 apply (blast intro: lt_trans2) |
293 done |
293 done |
294 |
294 |
295 lemma Collect_vimage_eq: "u\<in>nat ==> {<s,f(s)>. s \<in> A} -`` u = {s\<in>A. f(s) < u}" |
295 lemma Collect_vimage_eq: "u\<in>nat \<Longrightarrow> {<s,f(s)>. s \<in> A} -`` u = {s\<in>A. f(s) < u}" |
296 by (force simp add: lt_def) |
296 by (force simp add: lt_def) |
297 |
297 |
298 (* Lemma 49, page 28 *) |
298 (* Lemma 49, page 28 *) |
299 |
299 |
300 lemma alloc_prog_NbR_LeadsTo_lemma3: |
300 lemma alloc_prog_NbR_LeadsTo_lemma3: |
301 "[|G \<in> program; alloc_prog ok G; alloc_prog \<squnion> G \<in> Incr(lift(rel)); |
301 "\<lbrakk>G \<in> program; alloc_prog ok G; alloc_prog \<squnion> G \<in> Incr(lift(rel)); |
302 k\<in>nat|] |
302 k\<in>nat\<rbrakk> |
303 ==> alloc_prog \<squnion> G \<in> |
303 \<Longrightarrow> alloc_prog \<squnion> G \<in> |
304 {s\<in>state. k \<le> length(s`rel)} \<longmapsto>w {s\<in>state. k \<le> s`NbR}" |
304 {s\<in>state. k \<le> length(s`rel)} \<longmapsto>w {s\<in>state. k \<le> s`NbR}" |
305 (* Proof by induction over the difference between k and n *) |
305 (* Proof by induction over the difference between k and n *) |
306 apply (rule_tac f = "\<lambda>s\<in>state. k #- s`NbR" in LessThan_induct) |
306 apply (rule_tac f = "\<lambda>s\<in>state. k #- s`NbR" in LessThan_induct) |
307 apply (simp_all add: lam_def, auto) |
307 apply (simp_all add: lam_def, auto) |
308 apply (rule single_LeadsTo_I, auto) |
308 apply (rule single_LeadsTo_I, auto) |
320 done |
320 done |
321 |
321 |
322 subsubsection\<open>Towards proving lemma 50, page 29\<close> |
322 subsubsection\<open>Towards proving lemma 50, page 29\<close> |
323 |
323 |
324 lemma alloc_prog_giv_Ensures_lemma: |
324 lemma alloc_prog_giv_Ensures_lemma: |
325 "[| G \<in> program; k\<in>nat; alloc_prog ok G; |
325 "\<lbrakk>G \<in> program; k\<in>nat; alloc_prog ok G; |
326 alloc_prog \<squnion> G \<in> Incr(lift(ask)) |] ==> |
326 alloc_prog \<squnion> G \<in> Incr(lift(ask))\<rbrakk> \<Longrightarrow> |
327 alloc_prog \<squnion> G \<in> |
327 alloc_prog \<squnion> G \<in> |
328 {s\<in>state. nth(length(s`giv), s`ask) \<le> s`available_tok} \<inter> |
328 {s\<in>state. nth(length(s`giv), s`ask) \<le> s`available_tok} \<inter> |
329 {s\<in>state. k < length(s`ask)} \<inter> {s\<in>state. length(s`giv)=k} |
329 {s\<in>state. k < length(s`ask)} \<inter> {s\<in>state. length(s`giv)=k} |
330 Ensures {s\<in>state. ~ k <length(s`ask)} \<union> {s\<in>state. length(s`giv) \<noteq> k}" |
330 Ensures {s\<in>state. \<not> k <length(s`ask)} \<union> {s\<in>state. length(s`giv) \<noteq> k}" |
331 apply (rule EnsuresI, auto) |
331 apply (rule EnsuresI, auto) |
332 apply (erule_tac [2] V = "G\<notin>u" for u in thin_rl) |
332 apply (erule_tac [2] V = "G\<notin>u" for u in thin_rl) |
333 apply (rule_tac [2] act = alloc_giv_act in transientI) |
333 apply (rule_tac [2] act = alloc_giv_act in transientI) |
334 prefer 2 |
334 prefer 2 |
335 apply (simp add: alloc_prog_def [THEN def_prg_Acts]) |
335 apply (simp add: alloc_prog_def [THEN def_prg_Acts]) |
337 apply (auto simp add: alloc_prog_def [THEN def_prg_Acts] domain_def) |
337 apply (auto simp add: alloc_prog_def [THEN def_prg_Acts] domain_def) |
338 apply (erule_tac [2] swap) |
338 apply (erule_tac [2] swap) |
339 apply (rule_tac [2] ReplaceI) |
339 apply (rule_tac [2] ReplaceI) |
340 apply (rule_tac [2] x = "x (giv := x ` giv @ [nth (length(x`giv), x ` ask) ], available_tok := x ` available_tok #- nth (length(x`giv), x ` ask))" in exI) |
340 apply (rule_tac [2] x = "x (giv := x ` giv @ [nth (length(x`giv), x ` ask) ], available_tok := x ` available_tok #- nth (length(x`giv), x ` ask))" in exI) |
341 apply (auto intro!: state_update_type simp add: app_type) |
341 apply (auto intro!: state_update_type simp add: app_type) |
342 apply (rule_tac A = "{s\<in>state . nth (length(s ` giv), s ` ask) \<le> s ` available_tok} \<inter> {s\<in>state . k < length(s ` ask) } \<inter> {s\<in>state. length(s`giv) =k}" and A' = "{s\<in>state . nth (length(s ` giv), s ` ask) \<le> s ` available_tok} \<union> {s\<in>state. ~ k < length(s`ask) } \<union> {s\<in>state . length(s ` giv) \<noteq> k}" in Constrains_weaken) |
342 apply (rule_tac A = "{s\<in>state . nth (length(s ` giv), s ` ask) \<le> s ` available_tok} \<inter> {s\<in>state . k < length(s ` ask) } \<inter> {s\<in>state. length(s`giv) =k}" and A' = "{s\<in>state . nth (length(s ` giv), s ` ask) \<le> s ` available_tok} \<union> {s\<in>state. \<not> k < length(s`ask) } \<union> {s\<in>state . length(s ` giv) \<noteq> k}" in Constrains_weaken) |
343 apply (auto dest: ActsD simp add: Constrains_def constrains_def alloc_prog_def [THEN def_prg_Acts] alloc_prog_ok_iff) |
343 apply (auto dest: ActsD simp add: Constrains_def constrains_def alloc_prog_def [THEN def_prg_Acts] alloc_prog_ok_iff) |
344 apply (subgoal_tac "length(xa ` giv @ [nth (length(xa ` giv), xa ` ask) ]) = length(xa ` giv) #+ 1") |
344 apply (subgoal_tac "length(xa ` giv @ [nth (length(xa ` giv), xa ` ask) ]) = length(xa ` giv) #+ 1") |
345 apply (rule_tac [2] trans) |
345 apply (rule_tac [2] trans) |
346 apply (rule_tac [2] length_app, auto) |
346 apply (rule_tac [2] length_app, auto) |
347 apply (rule_tac j = "xa ` available_tok" in le_trans, auto) |
347 apply (rule_tac j = "xa ` available_tok" in le_trans, auto) |
354 apply (drule StableD) |
354 apply (drule StableD) |
355 apply (auto simp add: Constrains_def constrains_def, force) |
355 apply (auto simp add: Constrains_def constrains_def, force) |
356 done |
356 done |
357 |
357 |
358 lemma alloc_prog_giv_Stable_lemma: |
358 lemma alloc_prog_giv_Stable_lemma: |
359 "[| G \<in> program; alloc_prog ok G; k\<in>nat |] |
359 "\<lbrakk>G \<in> program; alloc_prog ok G; k\<in>nat\<rbrakk> |
360 ==> alloc_prog \<squnion> G \<in> Stable({s\<in>state . k \<le> length(s`giv)})" |
360 \<Longrightarrow> alloc_prog \<squnion> G \<in> Stable({s\<in>state . k \<le> length(s`giv)})" |
361 apply (auto intro!: stable_imp_Stable simp add: alloc_prog_ok_iff, safety) |
361 apply (auto intro!: stable_imp_Stable simp add: alloc_prog_ok_iff, safety) |
362 apply (auto intro: leI) |
362 apply (auto intro: leI) |
363 apply (drule_tac f = "lift (giv)" and g = length in imp_preserves_comp) |
363 apply (drule_tac f = "lift (giv)" and g = length in imp_preserves_comp) |
364 apply (drule_tac f = "length comp lift (giv)" and A = nat and r = Le in preserves_imp_increasing) |
364 apply (drule_tac f = "length comp lift (giv)" and A = nat and r = Le in preserves_imp_increasing) |
365 apply (drule_tac [2] x = k in increasing_imp_stable) |
365 apply (drule_tac [2] x = k in increasing_imp_stable) |
368 done |
368 done |
369 |
369 |
370 (* Lemma 50, page 29 *) |
370 (* Lemma 50, page 29 *) |
371 |
371 |
372 lemma alloc_prog_giv_LeadsTo_lemma: |
372 lemma alloc_prog_giv_LeadsTo_lemma: |
373 "[| G \<in> program; alloc_prog ok G; |
373 "\<lbrakk>G \<in> program; alloc_prog ok G; |
374 alloc_prog \<squnion> G \<in> Incr(lift(ask)); k\<in>nat |] |
374 alloc_prog \<squnion> G \<in> Incr(lift(ask)); k\<in>nat\<rbrakk> |
375 ==> alloc_prog \<squnion> G \<in> |
375 \<Longrightarrow> alloc_prog \<squnion> G \<in> |
376 {s\<in>state. nth(length(s`giv), s`ask) \<le> s`available_tok} \<inter> |
376 {s\<in>state. nth(length(s`giv), s`ask) \<le> s`available_tok} \<inter> |
377 {s\<in>state. k < length(s`ask)} \<inter> |
377 {s\<in>state. k < length(s`ask)} \<inter> |
378 {s\<in>state. length(s`giv) = k} |
378 {s\<in>state. length(s`giv) = k} |
379 \<longmapsto>w {s\<in>state. k < length(s`giv)}" |
379 \<longmapsto>w {s\<in>state. k < length(s`giv)}" |
380 apply (subgoal_tac "alloc_prog \<squnion> G \<in> {s\<in>state. nth (length(s`giv), s`ask) \<le> s`available_tok} \<inter> {s\<in>state. k < length(s`ask) } \<inter> {s\<in>state. length(s`giv) = k} \<longmapsto>w {s\<in>state. ~ k <length(s`ask) } \<union> {s\<in>state. length(s`giv) \<noteq> k}") |
380 apply (subgoal_tac "alloc_prog \<squnion> G \<in> {s\<in>state. nth (length(s`giv), s`ask) \<le> s`available_tok} \<inter> {s\<in>state. k < length(s`ask) } \<inter> {s\<in>state. length(s`giv) = k} \<longmapsto>w {s\<in>state. \<not> k <length(s`ask) } \<union> {s\<in>state. length(s`giv) \<noteq> k}") |
381 prefer 2 apply (blast intro: alloc_prog_giv_Ensures_lemma [THEN LeadsTo_Basis]) |
381 prefer 2 apply (blast intro: alloc_prog_giv_Ensures_lemma [THEN LeadsTo_Basis]) |
382 apply (subgoal_tac "alloc_prog \<squnion> G \<in> Stable ({s\<in>state. k < length(s`ask) }) ") |
382 apply (subgoal_tac "alloc_prog \<squnion> G \<in> Stable ({s\<in>state. k < length(s`ask) }) ") |
383 apply (drule PSP_Stable, assumption) |
383 apply (drule PSP_Stable, assumption) |
384 apply (rule LeadsTo_weaken) |
384 apply (rule LeadsTo_weaken) |
385 apply (rule PSP_Stable) |
385 apply (rule PSP_Stable) |
395 text\<open>Lemma 51, page 29. |
395 text\<open>Lemma 51, page 29. |
396 This theorem states as invariant that if the number of |
396 This theorem states as invariant that if the number of |
397 tokens given does not exceed the number returned, then the upper limit |
397 tokens given does not exceed the number returned, then the upper limit |
398 (\<^term>\<open>NbT\<close>) does not exceed the number currently available.\<close> |
398 (\<^term>\<open>NbT\<close>) does not exceed the number currently available.\<close> |
399 lemma alloc_prog_Always_lemma: |
399 lemma alloc_prog_Always_lemma: |
400 "[| G \<in> program; alloc_prog ok G; |
400 "\<lbrakk>G \<in> program; alloc_prog ok G; |
401 alloc_prog \<squnion> G \<in> Incr(lift(ask)); |
401 alloc_prog \<squnion> G \<in> Incr(lift(ask)); |
402 alloc_prog \<squnion> G \<in> Incr(lift(rel)) |] |
402 alloc_prog \<squnion> G \<in> Incr(lift(rel))\<rbrakk> |
403 ==> alloc_prog \<squnion> G \<in> |
403 \<Longrightarrow> alloc_prog \<squnion> G \<in> |
404 Always({s\<in>state. tokens(s`giv) \<le> tokens(take(s`NbR, s`rel)) \<longrightarrow> |
404 Always({s\<in>state. tokens(s`giv) \<le> tokens(take(s`NbR, s`rel)) \<longrightarrow> |
405 NbT \<le> s`available_tok})" |
405 NbT \<le> s`available_tok})" |
406 apply (subgoal_tac |
406 apply (subgoal_tac |
407 "alloc_prog \<squnion> G |
407 "alloc_prog \<squnion> G |
408 \<in> Always ({s\<in>state. s`NbR \<le> length(s`rel) } \<inter> |
408 \<in> Always ({s\<in>state. s`NbR \<le> length(s`rel) } \<inter> |
422 |
422 |
423 |
423 |
424 subsubsection\<open>Main lemmas towards proving property (31)\<close> |
424 subsubsection\<open>Main lemmas towards proving property (31)\<close> |
425 |
425 |
426 lemma LeadsTo_strength_R: |
426 lemma LeadsTo_strength_R: |
427 "[| F \<in> C \<longmapsto>w B'; F \<in> A-C \<longmapsto>w B; B'<=B |] ==> F \<in> A \<longmapsto>w B" |
427 "\<lbrakk>F \<in> C \<longmapsto>w B'; F \<in> A-C \<longmapsto>w B; B'<=B\<rbrakk> \<Longrightarrow> F \<in> A \<longmapsto>w B" |
428 by (blast intro: LeadsTo_weaken LeadsTo_Un_Un) |
428 by (blast intro: LeadsTo_weaken LeadsTo_Un_Un) |
429 |
429 |
430 lemma PSP_StableI: |
430 lemma PSP_StableI: |
431 "[| F \<in> Stable(C); F \<in> A - C \<longmapsto>w B; |
431 "\<lbrakk>F \<in> Stable(C); F \<in> A - C \<longmapsto>w B; |
432 F \<in> A \<inter> C \<longmapsto>w B \<union> (state - C) |] ==> F \<in> A \<longmapsto>w B" |
432 F \<in> A \<inter> C \<longmapsto>w B \<union> (state - C)\<rbrakk> \<Longrightarrow> F \<in> A \<longmapsto>w B" |
433 apply (rule_tac A = " (A-C) \<union> (A \<inter> C)" in LeadsTo_weaken_L) |
433 apply (rule_tac A = " (A-C) \<union> (A \<inter> C)" in LeadsTo_weaken_L) |
434 prefer 2 apply blast |
434 prefer 2 apply blast |
435 apply (rule LeadsTo_Un, assumption) |
435 apply (rule LeadsTo_Un, assumption) |
436 apply (blast intro: LeadsTo_weaken dest: PSP_Stable) |
436 apply (blast intro: LeadsTo_weaken dest: PSP_Stable) |
437 done |
437 done |
438 |
438 |
439 lemma state_compl_eq [simp]: "state - {s\<in>state. P(s)} = {s\<in>state. ~P(s)}" |
439 lemma state_compl_eq [simp]: "state - {s\<in>state. P(s)} = {s\<in>state. \<not>P(s)}" |
440 by auto |
440 by auto |
441 |
441 |
442 (*needed?*) |
442 (*needed?*) |
443 lemma single_state_Diff_eq [simp]: "{s}-{x \<in> state. P(x)} = (if s\<in>state & P(s) then 0 else {s})" |
443 lemma single_state_Diff_eq [simp]: "{s}-{x \<in> state. P(x)} = (if s\<in>state & P(s) then 0 else {s})" |
444 by auto |
444 by auto |
459 (*First step in proof of (31) -- the corrected version from Charpentier. |
459 (*First step in proof of (31) -- the corrected version from Charpentier. |
460 This lemma implies that if a client releases some tokens then the Allocator |
460 This lemma implies that if a client releases some tokens then the Allocator |
461 will eventually recognize that they've been released.*) |
461 will eventually recognize that they've been released.*) |
462 lemma (in alloc_progress) tokens_take_NbR_lemma: |
462 lemma (in alloc_progress) tokens_take_NbR_lemma: |
463 "k \<in> tokbag |
463 "k \<in> tokbag |
464 ==> alloc_prog \<squnion> G \<in> |
464 \<Longrightarrow> alloc_prog \<squnion> G \<in> |
465 {s\<in>state. k \<le> tokens(s`rel)} |
465 {s\<in>state. k \<le> tokens(s`rel)} |
466 \<longmapsto>w {s\<in>state. k \<le> tokens(take(s`NbR, s`rel))}" |
466 \<longmapsto>w {s\<in>state. k \<le> tokens(take(s`NbR, s`rel))}" |
467 apply (rule single_LeadsTo_I, safe) |
467 apply (rule single_LeadsTo_I, safe) |
468 apply (rule_tac a1 = "s`rel" in Increasing_imp_Stable [THEN PSP_StableI]) |
468 apply (rule_tac a1 = "s`rel" in Increasing_imp_Stable [THEN PSP_StableI]) |
469 apply (rule_tac [4] k1 = "length(s`rel)" in alloc_prog_NbR_LeadsTo_lemma3 [THEN LeadsTo_strength_R]) |
469 apply (rule_tac [4] k1 = "length(s`rel)" in alloc_prog_NbR_LeadsTo_lemma3 [THEN LeadsTo_strength_R]) |
478 |
478 |
479 (*Second step in proof of (31): by LHS of the guarantee and transivity of |
479 (*Second step in proof of (31): by LHS of the guarantee and transivity of |
480 \<longmapsto>w *) |
480 \<longmapsto>w *) |
481 lemma (in alloc_progress) tokens_take_NbR_lemma2: |
481 lemma (in alloc_progress) tokens_take_NbR_lemma2: |
482 "k \<in> tokbag |
482 "k \<in> tokbag |
483 ==> alloc_prog \<squnion> G \<in> |
483 \<Longrightarrow> alloc_prog \<squnion> G \<in> |
484 {s\<in>state. tokens(s`giv) = k} |
484 {s\<in>state. tokens(s`giv) = k} |
485 \<longmapsto>w {s\<in>state. k \<le> tokens(take(s`NbR, s`rel))}" |
485 \<longmapsto>w {s\<in>state. k \<le> tokens(take(s`NbR, s`rel))}" |
486 apply (rule LeadsTo_Trans) |
486 apply (rule LeadsTo_Trans) |
487 apply (rule_tac [2] tokens_take_NbR_lemma) |
487 apply (rule_tac [2] tokens_take_NbR_lemma) |
488 prefer 2 apply assumption |
488 prefer 2 apply assumption |
490 apply (blast intro: LeadsTo_weaken_L progress nat_into_Ord) |
490 apply (blast intro: LeadsTo_weaken_L progress nat_into_Ord) |
491 done |
491 done |
492 |
492 |
493 (*Third step in proof of (31): by PSP with the fact that giv increases *) |
493 (*Third step in proof of (31): by PSP with the fact that giv increases *) |
494 lemma (in alloc_progress) length_giv_disj: |
494 lemma (in alloc_progress) length_giv_disj: |
495 "[| k \<in> tokbag; n \<in> nat |] |
495 "\<lbrakk>k \<in> tokbag; n \<in> nat\<rbrakk> |
496 ==> alloc_prog \<squnion> G \<in> |
496 \<Longrightarrow> alloc_prog \<squnion> G \<in> |
497 {s\<in>state. length(s`giv) = n & tokens(s`giv) = k} |
497 {s\<in>state. length(s`giv) = n & tokens(s`giv) = k} |
498 \<longmapsto>w |
498 \<longmapsto>w |
499 {s\<in>state. (length(s`giv) = n & tokens(s`giv) = k & |
499 {s\<in>state. (length(s`giv) = n & tokens(s`giv) = k & |
500 k \<le> tokens(take(s`NbR, s`rel))) | n < length(s`giv)}" |
500 k \<le> tokens(take(s`NbR, s`rel))) | n < length(s`giv)}" |
501 apply (rule single_LeadsTo_I, safe) |
501 apply (rule single_LeadsTo_I, safe) |
510 apply (force dest: prefix_length_le_equal) |
510 apply (force dest: prefix_length_le_equal) |
511 done |
511 done |
512 |
512 |
513 (*Fourth step in proof of (31): we apply lemma (51) *) |
513 (*Fourth step in proof of (31): we apply lemma (51) *) |
514 lemma (in alloc_progress) length_giv_disj2: |
514 lemma (in alloc_progress) length_giv_disj2: |
515 "[|k \<in> tokbag; n \<in> nat|] |
515 "\<lbrakk>k \<in> tokbag; n \<in> nat\<rbrakk> |
516 ==> alloc_prog \<squnion> G \<in> |
516 \<Longrightarrow> alloc_prog \<squnion> G \<in> |
517 {s\<in>state. length(s`giv) = n & tokens(s`giv) = k} |
517 {s\<in>state. length(s`giv) = n & tokens(s`giv) = k} |
518 \<longmapsto>w |
518 \<longmapsto>w |
519 {s\<in>state. (length(s`giv) = n & NbT \<le> s`available_tok) | |
519 {s\<in>state. (length(s`giv) = n & NbT \<le> s`available_tok) | |
520 n < length(s`giv)}" |
520 n < length(s`giv)}" |
521 apply (rule LeadsTo_weaken_R) |
521 apply (rule LeadsTo_weaken_R) |
578 apply (blast intro: le_trans) |
578 apply (blast intro: le_trans) |
579 done |
579 done |
580 |
580 |
581 (*Eighth step in proof of (31): by 50, we get |giv| > n. *) |
581 (*Eighth step in proof of (31): by 50, we get |giv| > n. *) |
582 lemma (in alloc_progress) extend_giv: |
582 lemma (in alloc_progress) extend_giv: |
583 "[| k \<in> nat; n < k|] |
583 "\<lbrakk>k \<in> nat; n < k\<rbrakk> |
584 ==> alloc_prog \<squnion> G \<in> |
584 \<Longrightarrow> alloc_prog \<squnion> G \<in> |
585 {s\<in>state. length(s`ask) = k & length(s`giv) = n} |
585 {s\<in>state. length(s`ask) = k & length(s`giv) = n} |
586 \<longmapsto>w {s\<in>state. n < length(s`giv)}" |
586 \<longmapsto>w {s\<in>state. n < length(s`giv)}" |
587 apply (rule LeadsTo_Un_duplicate) |
587 apply (rule LeadsTo_Un_duplicate) |
588 apply (rule LeadsTo_cancel1) |
588 apply (rule LeadsTo_cancel1) |
589 apply (rule_tac [2] alloc_prog_giv_LeadsTo_lemma) |
589 apply (rule_tac [2] alloc_prog_giv_LeadsTo_lemma) |
595 (*Ninth and tenth steps in proof of (31): by 50, we get |giv| > n. |
595 (*Ninth and tenth steps in proof of (31): by 50, we get |giv| > n. |
596 The report has an error: putting |ask|=k for the precondition fails because |
596 The report has an error: putting |ask|=k for the precondition fails because |
597 we can't expect |ask| to remain fixed until |giv| increases.*) |
597 we can't expect |ask| to remain fixed until |giv| increases.*) |
598 lemma (in alloc_progress) alloc_prog_ask_LeadsTo_giv: |
598 lemma (in alloc_progress) alloc_prog_ask_LeadsTo_giv: |
599 "k \<in> nat |
599 "k \<in> nat |
600 ==> alloc_prog \<squnion> G \<in> |
600 \<Longrightarrow> alloc_prog \<squnion> G \<in> |
601 {s\<in>state. k \<le> length(s`ask)} \<longmapsto>w {s\<in>state. k \<le> length(s`giv)}" |
601 {s\<in>state. k \<le> length(s`ask)} \<longmapsto>w {s\<in>state. k \<le> length(s`giv)}" |
602 (* Proof by induction over the difference between k and n *) |
602 (* Proof by induction over the difference between k and n *) |
603 apply (rule_tac f = "\<lambda>s\<in>state. k #- length(s`giv)" in LessThan_induct) |
603 apply (rule_tac f = "\<lambda>s\<in>state. k #- length(s`giv)" in LessThan_induct) |
604 apply (auto simp add: lam_def Collect_vimage_eq) |
604 apply (auto simp add: lam_def Collect_vimage_eq) |
605 apply (rule single_LeadsTo_I, auto) |
605 apply (rule single_LeadsTo_I, auto) |
620 done |
620 done |
621 |
621 |
622 (*Final lemma: combine previous result with lemma (30)*) |
622 (*Final lemma: combine previous result with lemma (30)*) |
623 lemma (in alloc_progress) final: |
623 lemma (in alloc_progress) final: |
624 "h \<in> list(tokbag) |
624 "h \<in> list(tokbag) |
625 ==> alloc_prog \<squnion> G |
625 \<Longrightarrow> alloc_prog \<squnion> G |
626 \<in> {s\<in>state. <h, s`ask> \<in> prefix(tokbag)} \<longmapsto>w |
626 \<in> {s\<in>state. <h, s`ask> \<in> prefix(tokbag)} \<longmapsto>w |
627 {s\<in>state. <h, s`giv> \<in> prefix(tokbag)}" |
627 {s\<in>state. <h, s`giv> \<in> prefix(tokbag)}" |
628 apply (rule single_LeadsTo_I) |
628 apply (rule single_LeadsTo_I) |
629 prefer 2 apply simp |
629 prefer 2 apply simp |
630 apply (rename_tac s0) |
630 apply (rename_tac s0) |