27 "alloc_giv_act == |
27 "alloc_giv_act == |
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 == |
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), |
71 declare alloc_giv_act_def [THEN def_act_simp, simp] |
71 declare alloc_giv_act_def [THEN def_act_simp, simp] |
72 declare alloc_rel_act_def [THEN def_act_simp, simp] |
72 declare alloc_rel_act_def [THEN def_act_simp, simp] |
73 |
73 |
74 |
74 |
75 lemma alloc_prog_ok_iff: |
75 lemma alloc_prog_ok_iff: |
76 "\<forall>G \<in> program. (alloc_prog ok G) <-> |
76 "\<forall>G \<in> program. (alloc_prog ok G) \<longleftrightarrow> |
77 (G \<in> preserves(lift(giv)) & G \<in> preserves(lift(available_tok)) & |
77 (G \<in> preserves(lift(giv)) & G \<in> preserves(lift(available_tok)) & |
78 G \<in> preserves(lift(NbR)) & alloc_prog \<in> Allowed(G))" |
78 G \<in> preserves(lift(NbR)) & alloc_prog \<in> Allowed(G))" |
79 by (auto simp add: ok_iff_Allowed alloc_prog_def [THEN def_prg_Allowed]) |
79 by (auto simp add: ok_iff_Allowed alloc_prog_def [THEN def_prg_Allowed]) |
80 |
80 |
81 |
81 |
165 apply (auto simp add: Le_def length_type) |
165 apply (auto simp add: Le_def length_type) |
166 apply (auto dest: ActsD simp add: Stable_def Constrains_def constrains_def) |
166 apply (auto dest: ActsD simp add: Stable_def Constrains_def constrains_def) |
167 apply (drule_tac f = "lift (rel) " in preserves_imp_eq) |
167 apply (drule_tac f = "lift (rel) " in preserves_imp_eq) |
168 apply assumption+ |
168 apply assumption+ |
169 apply (force dest: ActsD) |
169 apply (force dest: ActsD) |
170 apply (erule_tac V = "\<forall>x \<in> Acts (alloc_prog) Un Acts (G). ?P(x)" in thin_rl) |
170 apply (erule_tac V = "\<forall>x \<in> Acts (alloc_prog) \<union> Acts (G). ?P(x)" in thin_rl) |
171 apply (erule_tac V = "alloc_prog \<in> stable (?u)" in thin_rl) |
171 apply (erule_tac V = "alloc_prog \<in> stable (?u)" in thin_rl) |
172 apply (drule_tac a = "xc`rel" and f = "lift (rel)" in Increasing_imp_Stable) |
172 apply (drule_tac a = "xc`rel" and f = "lift (rel)" in Increasing_imp_Stable) |
173 apply (auto simp add: Stable_def Constrains_def constrains_def) |
173 apply (auto simp add: Stable_def Constrains_def constrains_def) |
174 apply (drule bspec, force) |
174 apply (drule bspec, force) |
175 apply (drule subsetD) |
175 apply (drule subsetD) |
325 "[| G \<in> program; k\<in>nat; alloc_prog ok G; |
325 "[| 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)) |] ==> |
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)} Un {s\<in>state. length(s`giv) \<noteq> k}" |
330 Ensures {s\<in>state. ~ 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" in thin_rl) |
332 apply (erule_tac [2] V = "G\<notin>?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} Un {s\<in>state. ~ k < length(s`ask) } Un {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. ~ 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) |
375 ==> alloc_prog \<squnion> G \<in> |
375 ==> 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 LeadsTo {s\<in>state. k < length(s`giv)}" |
379 LeadsTo {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} LeadsTo {s\<in>state. ~ k <length(s`ask) } Un {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} LeadsTo {s\<in>state. ~ 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) |
399 lemma alloc_prog_Always_lemma: |
399 lemma alloc_prog_Always_lemma: |
400 "[| G \<in> program; alloc_prog ok G; |
400 "[| 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)) |] |
403 ==> alloc_prog \<squnion> G \<in> |
403 ==> alloc_prog \<squnion> G \<in> |
404 Always({s\<in>state. tokens(s`giv) \<le> tokens(take(s`NbR, s`rel)) --> |
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> |
409 {s\<in>state. s`available_tok #+ tokens(s`giv) = |
409 {s\<in>state. s`available_tok #+ tokens(s`giv) = |
427 "[| F \<in> C LeadsTo B'; F \<in> A-C LeadsTo B; B'<=B |] ==> F \<in> A LeadsTo B" |
427 "[| F \<in> C LeadsTo B'; F \<in> A-C LeadsTo B; B'<=B |] ==> F \<in> A LeadsTo 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 LeadsTo B; |
431 "[| F \<in> Stable(C); F \<in> A - C LeadsTo B; |
432 F \<in> A \<inter> C LeadsTo B Un (state - C) |] ==> F \<in> A LeadsTo B" |
432 F \<in> A \<inter> C LeadsTo B \<union> (state - C) |] ==> F \<in> A LeadsTo B" |
433 apply (rule_tac A = " (A-C) Un (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 |