equal
deleted
inserted
replaced
87 |
87 |
88 lemma alloc_prog_preserves: |
88 lemma alloc_prog_preserves: |
89 "alloc_prog \<in> (\<Inter>x \<in> var-{giv, available_tok, NbR}. preserves(lift(x)))" |
89 "alloc_prog \<in> (\<Inter>x \<in> var-{giv, available_tok, NbR}. preserves(lift(x)))" |
90 apply (rule Inter_var_DiffI, force) |
90 apply (rule Inter_var_DiffI, force) |
91 apply (rule ballI) |
91 apply (rule ballI) |
92 apply (rule preservesI, constrains) |
92 apply (rule preservesI, safety) |
93 done |
93 done |
94 |
94 |
95 (* As a special case of the rule above *) |
95 (* As a special case of the rule above *) |
96 |
96 |
97 lemma alloc_prog_preserves_rel_ask_tok: |
97 lemma alloc_prog_preserves_rel_ask_tok: |
127 apply auto |
127 apply auto |
128 done |
128 done |
129 |
129 |
130 (** Safety property: (28) **) |
130 (** Safety property: (28) **) |
131 lemma alloc_prog_Increasing_giv: "alloc_prog \<in> program guarantees Incr(lift(giv))" |
131 lemma alloc_prog_Increasing_giv: "alloc_prog \<in> program guarantees Incr(lift(giv))" |
132 apply (auto intro!: increasing_imp_Increasing simp add: guar_def increasing_def alloc_prog_ok_iff alloc_prog_Allowed, constrains+) |
132 apply (auto intro!: increasing_imp_Increasing simp add: guar_def increasing_def alloc_prog_ok_iff alloc_prog_Allowed, safety+) |
133 apply (auto dest: ActsD) |
133 apply (auto dest: ActsD) |
134 apply (drule_tac f = "lift (giv) " in preserves_imp_eq) |
134 apply (drule_tac f = "lift (giv) " in preserves_imp_eq) |
135 apply auto |
135 apply auto |
136 done |
136 done |
137 |
137 |
138 lemma giv_Bounded_lamma1: |
138 lemma giv_Bounded_lamma1: |
139 "alloc_prog \<in> stable({s\<in>state. s`NbR \<le> length(s`rel)} \<inter> |
139 "alloc_prog \<in> stable({s\<in>state. s`NbR \<le> length(s`rel)} \<inter> |
140 {s\<in>state. s`available_tok #+ tokens(s`giv) = |
140 {s\<in>state. s`available_tok #+ tokens(s`giv) = |
141 NbT #+ tokens(take(s`NbR, s`rel))})" |
141 NbT #+ tokens(take(s`NbR, s`rel))})" |
142 apply constrains |
142 apply safety |
143 apply auto |
143 apply auto |
144 apply (simp add: diff_add_0 add_commute diff_add_inverse add_assoc add_diff_inverse) |
144 apply (simp add: diff_add_0 add_commute diff_add_inverse add_assoc add_diff_inverse) |
145 apply (simp (no_asm_simp) add: take_succ) |
145 apply (simp (no_asm_simp) add: take_succ) |
146 done |
146 done |
147 |
147 |
207 apply (auto intro!: AlwaysI simp add: guar_def) |
207 apply (auto intro!: AlwaysI simp add: guar_def) |
208 apply (subgoal_tac "G \<in> preserves (lift (giv))") |
208 apply (subgoal_tac "G \<in> preserves (lift (giv))") |
209 prefer 2 apply (simp add: alloc_prog_ok_iff) |
209 prefer 2 apply (simp add: alloc_prog_ok_iff) |
210 apply (rule_tac P = "%x y. <x,y> \<in> prefix(tokbag)" and A = "list(nat)" |
210 apply (rule_tac P = "%x y. <x,y> \<in> prefix(tokbag)" and A = "list(nat)" |
211 in stable_Join_Stable) |
211 in stable_Join_Stable) |
212 apply constrains |
212 apply safety |
213 prefer 2 apply (simp add: lift_def, clarify) |
213 prefer 2 apply (simp add: lift_def, clarify) |
214 apply (drule_tac a = k in Increasing_imp_Stable, auto) |
214 apply (drule_tac a = k in Increasing_imp_Stable, auto) |
215 done |
215 done |
216 |
216 |
217 subsection{* Towards proving the liveness property, (31) *} |
217 subsection{* Towards proving the liveness property, (31) *} |
237 done |
237 done |
238 |
238 |
239 lemma alloc_prog_rel_Stable_NbR_lemma: |
239 lemma alloc_prog_rel_Stable_NbR_lemma: |
240 "[| G \<in> program; alloc_prog ok G; k\<in>nat |] |
240 "[| G \<in> program; alloc_prog ok G; k\<in>nat |] |
241 ==> alloc_prog \<squnion> G \<in> Stable({s\<in>state . k \<le> succ(s ` NbR)})" |
241 ==> alloc_prog \<squnion> G \<in> Stable({s\<in>state . k \<le> succ(s ` NbR)})" |
242 apply (auto intro!: stable_imp_Stable simp add: alloc_prog_ok_iff, constrains, auto) |
242 apply (auto intro!: stable_imp_Stable simp add: alloc_prog_ok_iff, safety, auto) |
243 apply (blast intro: le_trans leI) |
243 apply (blast intro: le_trans leI) |
244 apply (drule_tac f = "lift (NbR)" and A = nat in preserves_imp_increasing) |
244 apply (drule_tac f = "lift (NbR)" and A = nat in preserves_imp_increasing) |
245 apply (drule_tac [2] g = succ in imp_increasing_comp) |
245 apply (drule_tac [2] g = succ in imp_increasing_comp) |
246 apply (rule_tac [2] mono_succ) |
246 apply (rule_tac [2] mono_succ) |
247 apply (drule_tac [4] x = k in increasing_imp_stable) |
247 apply (drule_tac [4] x = k in increasing_imp_stable) |
361 done |
361 done |
362 |
362 |
363 lemma alloc_prog_giv_Stable_lemma: |
363 lemma alloc_prog_giv_Stable_lemma: |
364 "[| G \<in> program; alloc_prog ok G; k\<in>nat |] |
364 "[| G \<in> program; alloc_prog ok G; k\<in>nat |] |
365 ==> alloc_prog \<squnion> G \<in> Stable({s\<in>state . k \<le> length(s`giv)})" |
365 ==> alloc_prog \<squnion> G \<in> Stable({s\<in>state . k \<le> length(s`giv)})" |
366 apply (auto intro!: stable_imp_Stable simp add: alloc_prog_ok_iff, constrains) |
366 apply (auto intro!: stable_imp_Stable simp add: alloc_prog_ok_iff, safety) |
367 apply (auto intro: leI) |
367 apply (auto intro: leI) |
368 apply (drule_tac f = "lift (giv)" and g = length in imp_preserves_comp) |
368 apply (drule_tac f = "lift (giv)" and g = length in imp_preserves_comp) |
369 apply (drule_tac f = "length comp lift (giv)" and A = nat and r = Le in preserves_imp_increasing) |
369 apply (drule_tac f = "length comp lift (giv)" and A = nat and r = Le in preserves_imp_increasing) |
370 apply (drule_tac [2] x = k in increasing_imp_stable) |
370 apply (drule_tac [2] x = k in increasing_imp_stable) |
371 prefer 3 apply (simp add: Le_def comp_def) |
371 prefer 3 apply (simp add: Le_def comp_def) |