lemma alloc_prog_preserves_rel_ask_tok: "alloc_prog \
preserves(lift(rel)) \<inter> preserves(lift(ask)) \<inter> preserves(lift(tok))" apply auto apply (insert alloc_prog_preserves) apply (drule_tac [3] x = tok in Inter_var_DiffD) apply (drule_tac [2] x = ask in Inter_var_DiffD) apply (drule_tac x = rel in Inter_var_DiffD, auto) done
lemma alloc_prog_giv_Ensures_lemma: "\G \ program; k\nat; alloc_prog ok G;
alloc_prog \<squnion> G \<in> Incr(lift(ask))\<rbrakk> \<Longrightarrow>
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}
Ensures {s\<in>state. \<not> k <length(s`ask)} \<union> {s\<in>state. length(s`giv) \<noteq> k}" apply (rule EnsuresI, auto) apply (erule_tac [2] V = "G\u" for u in thin_rl) apply (rule_tac [2] act = alloc_giv_act in transientI) prefer 2 apply (simp add: alloc_prog_def [THEN def_prg_Acts]) apply (simp add: alloc_giv_act_def [THEN def_act_eq, THEN act_subset]) apply (auto simp add: alloc_prog_def [THEN def_prg_Acts] domain_def) apply (erule_tac [2] swap) apply (rule_tac [2] ReplaceI) 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) apply (auto intro!: state_update_type simp add: app_type) apply (rule_tac A = "{s\state . nth (length(s ` giv), s ` ask) \ s ` available_tok} \ {s\state . k < length(s ` ask) } \ {s\state. length(s`giv) =k}" and A' = "{s\state . nth (length(s ` giv), s ` ask) \ s ` available_tok} \ {s\state. \ k < length(s`ask) } \ {s\state . length(s ` giv) \ k}" in Constrains_weaken) apply (auto dest: ActsD simp add: Constrains_def constrains_def alloc_prog_def [THEN def_prg_Acts] alloc_prog_ok_iff) apply (subgoal_tac "length(xa ` giv @ [nth (length(xa ` giv), xa ` ask) ]) = length(xa ` giv) #+ 1") apply (rule_tac [2] trans) apply (rule_tac [2] length_app, auto) apply (rule_tac j = "xa ` available_tok"in le_trans, auto) apply (drule_tac f = "lift (available_tok)"in preserves_imp_eq) apply assumption+ apply auto apply (drule_tac a = "xa ` ask"and r = "prefix(tokbag)"and A = "list(tokbag)" in Increasing_imp_Stable) apply (auto simp add: prefix_iff) apply (drule StableD) apply (auto simp add: Constrains_def constrains_def, force) done
lemma alloc_prog_giv_Stable_lemma: "\G \ program; alloc_prog ok G; k\nat\ \<Longrightarrow> alloc_prog \<squnion> G \<in> Stable({s\<in>state . k \<le> length(s`giv)})" apply (auto intro!: stable_imp_Stable simp add: alloc_prog_ok_iff, safety) apply (auto intro: leI) apply (drule_tac f = "lift (giv)"and g = length in imp_preserves_comp) apply (drule_tac f = "length comp lift (giv)"and A = nat and r = Le in preserves_imp_increasing) apply (drule_tac [2] x = k in increasing_imp_stable) prefer 3 apply (simp add: Le_def comp_def) apply (auto simp add: length_type) done
(* Lemma 50, page 29 *)
lemma alloc_prog_giv_LeadsTo_lemma: "\G \ program; alloc_prog ok G;
alloc_prog \<squnion> G \<in> Incr(lift(ask)); k\<in>nat\<rbrakk> \<Longrightarrow> 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`giv)}" apply (subgoal_tac "alloc_prog \ G \ {s\state. nth (length(s`giv), s`ask) \ s`available_tok} \ {s\state. k < length(s`ask) } \ {s\state. length(s`giv) = k} \w {s\state. \ k {s\state. length(s`giv) \ k}") prefer 2 apply (blast intro: alloc_prog_giv_Ensures_lemma [THEN LeadsTo_Basis]) apply (subgoal_tac "alloc_prog \ G \ Stable ({s\state. k < length(s`ask) }) ") apply (drule PSP_Stable, assumption) apply (rule LeadsTo_weaken) apply (rule PSP_Stable) apply (rule_tac [2] k = k in alloc_prog_giv_Stable_lemma) apply (auto simp add: le_iff) apply (drule_tac a = "succ (k)"and g1 = length in imp_Increasing_comp [THEN Increasing_imp_Stable]) apply (rule mono_length) prefer 2 apply simp apply (simp_all add: refl_prefix Le_def comp_def length_type) done
text\<open>Lemma 51, page 29.
This theoremstates as invariant that if the number of
tokens given does not exceed the number returned, then the upper limit
(\<^term>\<open>NbT\<close>) does not exceed the number currently available.\<close> lemma alloc_prog_Always_lemma: "\G \ program; alloc_prog ok G;
alloc_prog \<squnion> G \<in> Incr(lift(ask));
alloc_prog \<squnion> G \<in> Incr(lift(rel))\<rbrakk> \<Longrightarrow> alloc_prog \<squnion> G \<in>
Always({s\<in>state. tokens(s`giv) \<le> tokens(take(s`NbR, s`rel)) \<longrightarrow>
NbT \<le> s`available_tok})" apply (subgoal_tac "alloc_prog \ G \<in> Always ({s\<in>state. s`NbR \<le> length(s`rel) } \<inter>
{s\<in>state. s`available_tok #+ tokens(s`giv) =
NbT #+ tokens(take (s`NbR, s`rel))})") apply (rule_tac [2] AlwaysI) apply (rule_tac [3] giv_Bounded_lemma2, auto) apply (rule Always_weaken, assumption, auto) apply (subgoal_tac "0 \ tokens(take (x ` NbR, x ` rel)) #- tokens(x`giv) ") prefer 2 apply (force) apply (subgoal_tac "x`available_tok =
NbT #+ (tokens(take(x`NbR,x`rel)) #- tokens(x`giv))") apply (simp add: ) apply (auto split: nat_diff_split dest: lt_trans2) done
subsubsection\<open>Main lemmas towards proving property (31)\<close>
lemma LeadsTo_strength_R: "\F \ C \w B'; F \ A-C \w B; B'<=B\ \ F \ A \w B" by (blast intro: LeadsTo_weaken LeadsTo_Un_Un)
lemma PSP_StableI: "\F \ Stable(C); F \ A - C \w B;
F \<in> A \<inter> C \<longmapsto>w B \<union> (state - C)\<rbrakk> \<Longrightarrow> F \<in> A \<longmapsto>w B" apply (rule_tac A = " (A-C) \ (A \ C)" in LeadsTo_weaken_L) prefer 2 apply blast apply (rule LeadsTo_Un, assumption) apply (blast intro: LeadsTo_weaken dest: PSP_Stable) done
lemma state_compl_eq [simp]: "state - {s\state. P(s)} = {s\state. \P(s)}" by auto
(*needed?*) lemma single_state_Diff_eq [simp]: "{s}-{x \ state. P(x)} = (if s\state \ P(s) then 0 else {s})" by auto
locale alloc_progress = fixes G assumes Gprog [intro,simp]: "G \ program" and okG [iff]: "alloc_prog ok G" and Incr_rel [intro]: "alloc_prog \ G \ Incr(lift(rel))" and Incr_ask [intro]: "alloc_prog \ G \ Incr(lift(ask))" and safety: "alloc_prog \ G \<in> Always(\<Inter>k \<in> nat. {s\<in>state. nth(k, s`ask) \<le> NbT})" and progress: "alloc_prog \ G \<in> (\<Inter>k\<in>nat. {s\<in>state. k \<le> tokens(s`giv)} \<longmapsto>w
{s\<in>state. k \<le> tokens(s`rel)})"
(*First step in proof of (31) -- the corrected version from Charpentier. This lemma implies that if a client releases some tokens then the Allocator
will eventually recognize that they've been released.*) lemma (in alloc_progress) tokens_take_NbR_lemma: "k \ tokbag \<Longrightarrow> alloc_prog \<squnion> G \<in>
{s\<in>state. k \<le> tokens(s`rel)} \<longmapsto>w {s\<in>state. k \<le> tokens(take(s`NbR, s`rel))}" apply (rule single_LeadsTo_I, safe) apply (rule_tac a1 = "s`rel"in Increasing_imp_Stable [THEN PSP_StableI]) apply (rule_tac [4] k1 = "length(s`rel)"in alloc_prog_NbR_LeadsTo_lemma3 [THEN LeadsTo_strength_R]) apply (rule_tac [8] subset_imp_LeadsTo) apply (auto intro!: Incr_rel) apply (rule_tac j = "tokens(take (length(s`rel), x`rel))"in le_trans) apply (rule_tac j = "tokens(take (length(s`rel), s`rel))"in le_trans) apply (auto intro!: tokens_mono take_mono simp add: prefix_iff) done
(*** Rest of proofs done by lcp ***)
(*Second step in proof of (31): by LHS of the guarantee and transivity of
\<longmapsto>w *) lemma (in alloc_progress) tokens_take_NbR_lemma2: "k \ tokbag \<Longrightarrow> alloc_prog \<squnion> G \<in>
{s\<in>state. tokens(s`giv) = k} \<longmapsto>w {s\<in>state. k \<le> tokens(take(s`NbR, s`rel))}" apply (rule LeadsTo_Trans) apply (rule_tac [2] tokens_take_NbR_lemma) prefer 2 apply assumption apply (insert progress) apply (blast intro: LeadsTo_weaken_L progress nat_into_Ord) done
(*Third step in proof of (31): by PSP with the fact that giv increases *) lemma (in alloc_progress) length_giv_disj: "\k \ tokbag; n \ nat\ \<Longrightarrow> alloc_prog \<squnion> G \<in>
{s\<in>state. length(s`giv) = n \<and> tokens(s`giv) = k} \<longmapsto>w
{s\<in>state. (length(s`giv) = n \<and> tokens(s`giv) = k \<and>
k \<le> tokens(take(s`NbR, s`rel))) | n < length(s`giv)}" apply (rule single_LeadsTo_I, safe) apply (rule_tac a1 = "s`giv"in Increasing_imp_Stable [THEN PSP_StableI]) apply (rule alloc_prog_Increasing_giv [THEN guaranteesD]) apply (simp_all add: Int_cons_left) apply (rule LeadsTo_weaken) apply (rule_tac k = "tokens(s`giv)"in tokens_take_NbR_lemma2) apply auto apply (force dest: prefix_length_le [THEN le_iff [THEN iffD1]]) apply (simp add: not_lt_iff_le) apply (force dest: prefix_length_le_equal) done
(*Fourth step in proof of (31): we apply lemma (51) *) lemma (in alloc_progress) length_giv_disj2: "\k \ tokbag; n \ nat\ \<Longrightarrow> alloc_prog \<squnion> G \<in>
{s\<in>state. length(s`giv) = n \<and> tokens(s`giv) = k} \<longmapsto>w
{s\<in>state. (length(s`giv) = n \<and> NbT \<le> s`available_tok) |
n < length(s`giv)}" apply (rule LeadsTo_weaken_R) apply (rule Always_LeadsToD [OF alloc_prog_Always_lemma length_giv_disj], auto) done
(*Fifth step in proof of (31): from the fourth step, taking the union over all
k\<in>nat *) lemma (in alloc_progress) length_giv_disj3: "n \ nat \<Longrightarrow> alloc_prog \<squnion> G \<in>
{s\<in>state. length(s`giv) = n} \<longmapsto>w
{s\<in>state. (length(s`giv) = n \<and> NbT \<le> s`available_tok) |
n < length(s`giv)}" apply (rule LeadsTo_weaken_L) apply (rule_tac I = nat in LeadsTo_UN) apply (rule_tac k = i in length_giv_disj2) apply (simp_all add: UN_conj_eq) done
(*Sixth step in proof of (31): from the fifth step, by PSP with the
assumption that ask increases *) lemma (in alloc_progress) length_ask_giv: "\k \ nat; n < k\ \<Longrightarrow> alloc_prog \<squnion> G \<in>
{s\<in>state. length(s`ask) = k \<and> length(s`giv) = n} \<longmapsto>w
{s\<in>state. (NbT \<le> s`available_tok \<and> length(s`giv) < length(s`ask) \<and>
length(s`giv) = n) |
n < length(s`giv)}" apply (rule single_LeadsTo_I, safe) apply (rule_tac a1 = "s`ask"and f1 = "lift(ask)" in Increasing_imp_Stable [THEN PSP_StableI]) apply (rule Incr_ask, simp_all) apply (rule LeadsTo_weaken) apply (rule_tac n = "length(s ` giv)"in length_giv_disj3) apply simp_all apply blast apply clarify apply simp apply (blast dest!: prefix_length_le intro: lt_trans2) done
(*Seventh step in proof of (31): no request (ask[k]) exceeds NbT *) lemma (in alloc_progress) length_ask_giv2: "\k \ nat; n < k\ \<Longrightarrow> alloc_prog \<squnion> G \<in>
{s\<in>state. length(s`ask) = k \<and> length(s`giv) = n} \<longmapsto>w
{s\<in>state. (nth(length(s`giv), s`ask) \<le> s`available_tok \<and>
length(s`giv) < length(s`ask) \<and> length(s`giv) = n) |
n < length(s`giv)}" apply (rule LeadsTo_weaken_R) apply (rule Always_LeadsToD [OF safety length_ask_giv], assumption+, clarify) apply (simp add: INT_iff) apply (drule_tac x = "length(x ` giv)"and P = "\x. f (x) \ NbT" for f in bspec) apply simp apply (blast intro: le_trans) done
(*Eighth step in proof of (31): by 50, we get |giv| > n. *) lemma (in alloc_progress) extend_giv: "\k \ nat; n < k\ \<Longrightarrow> alloc_prog \<squnion> G \<in>
{s\<in>state. length(s`ask) = k \<and> length(s`giv) = n} \<longmapsto>w {s\<in>state. n < length(s`giv)}" apply (rule LeadsTo_Un_duplicate) apply (rule LeadsTo_cancel1) apply (rule_tac [2] alloc_prog_giv_LeadsTo_lemma) apply (simp_all add: Incr_ask lt_nat_in_nat) apply (rule LeadsTo_weaken_R) apply (rule length_ask_giv2, auto) done
(*Ninth and tenth steps in proof of (31): by 50, we get |giv| > n. The report has an error: putting |ask|=k for the precondition fails because
we can't expect |ask| to remain fixed until |giv| increases.*) lemma (in alloc_progress) alloc_prog_ask_LeadsTo_giv: "k \ nat \<Longrightarrow> alloc_prog \<squnion> G \<in>
{s\<in>state. k \<le> length(s`ask)} \<longmapsto>w {s\<in>state. k \<le> length(s`giv)}" (* Proof by induction over the difference between k and n *) apply (rule_tac f = "\s\state. k #- length(s`giv)" in LessThan_induct) apply (auto simp add: lam_def Collect_vimage_eq) apply (rule single_LeadsTo_I, auto) apply (rename_tac "s0") apply (case_tac "length(s0 ` giv) < length(s0 ` ask) ") apply (rule_tac [2] subset_imp_LeadsTo) apply (auto simp add: not_lt_iff_le) prefer 2 apply (blast dest: le_imp_not_lt intro: lt_trans2) apply (rule_tac a1 = "s0`ask"and f1 = "lift (ask)" in Increasing_imp_Stable [THEN PSP_StableI]) apply (rule Incr_ask, simp) apply (force) apply (rule LeadsTo_weaken) apply (rule_tac n = "length(s0 ` giv)"and k = "length(s0 ` ask)" in extend_giv) apply (auto dest: not_lt_imp_le simp add: leI diff_lt_iff_lt) apply (blast dest!: prefix_length_le intro: lt_trans2) done
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
