--- a/src/ZF/UNITY/AllocImpl.thy Tue Jun 24 10:42:34 2003 +0200
+++ b/src/ZF/UNITY/AllocImpl.thy Tue Jun 24 16:32:59 2003 +0200
@@ -7,21 +7,6 @@
Charpentier and Chandy, section 7 (page 17).
*)
-(*LOCALE NEEDED FOR PROOF OF GUARANTEES THEOREM*)
-
-(*????FIXME: sort out this mess
-FoldSet.cons_Int_right_lemma1:
- ?x \<in> ?D \<Longrightarrow> cons(?x, ?C) \<inter> ?D = cons(?x, ?C \<inter> ?D)
-FoldSet.cons_Int_right_lemma2: ?x \<notin> ?D \<Longrightarrow> cons(?x, ?C) \<inter> ?D = ?C \<inter> ?D
-Multiset.cons_Int_right_cases:
- cons(?x, ?A) \<inter> ?B = (if ?x \<in> ?B then cons(?x, ?A \<inter> ?B) else ?A \<inter> ?B)
-UNITYMisc.Int_cons_right:
- ?A \<inter> cons(?a, ?B) = (if ?a \<in> ?A then cons(?a, ?A \<inter> ?B) else ?A \<inter> ?B)
-UNITYMisc.Int_succ_right:
- ?A \<inter> succ(?k) = (if ?k \<in> ?A then cons(?k, ?A \<inter> ?k) else ?A \<inter> ?k)
-*)
-
-
theory AllocImpl = ClientImpl:
consts
@@ -34,10 +19,10 @@
"available_tok" == "Var([succ(succ(2))])"
axioms
- alloc_type_assumes:
+ alloc_type_assumes [simp]:
"type_of(NbR) = nat & type_of(available_tok)=nat"
- alloc_default_val_assumes:
+ alloc_default_val_assumes [simp]:
"default_val(NbR) = 0 & default_val(available_tok)=0"
constdefs
@@ -67,25 +52,20 @@
preserves(lift(giv)). Acts(G))"
-declare alloc_type_assumes [simp] alloc_default_val_assumes [simp]
-
lemma available_tok_value_type [simp,TC]: "s\<in>state ==> s`available_tok \<in> nat"
apply (unfold state_def)
-apply (drule_tac a = "available_tok" in apply_type)
-apply auto
+apply (drule_tac a = available_tok in apply_type, auto)
done
lemma NbR_value_type [simp,TC]: "s\<in>state ==> s`NbR \<in> nat"
apply (unfold state_def)
-apply (drule_tac a = "NbR" in apply_type)
-apply auto
+apply (drule_tac a = NbR in apply_type, auto)
done
(** The Alloc Program **)
lemma alloc_prog_type [simp,TC]: "alloc_prog \<in> program"
-apply (simp add: alloc_prog_def)
-done
+by (simp add: alloc_prog_def)
declare alloc_prog_def [THEN def_prg_Init, simp]
declare alloc_prog_def [THEN def_prg_AllowedActs, simp]
@@ -107,11 +87,9 @@
lemma alloc_prog_preserves:
"alloc_prog \<in> (\<Inter>x \<in> var-{giv, available_tok, NbR}. preserves(lift(x)))"
-apply (rule Inter_var_DiffI)
-apply (force );
+apply (rule Inter_var_DiffI, force)
apply (rule ballI)
-apply (rule preservesI)
-apply (constrains)
+apply (rule preservesI, constrains)
done
(* As a special case of the rule above *)
@@ -121,10 +99,9 @@
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)
-apply auto
+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_Allowed:
@@ -152,8 +129,7 @@
(** Safety property: (28) **)
lemma alloc_prog_Increasing_giv: "alloc_prog \<in> program guarantees Incr(lift(giv))"
-apply (auto intro!: increasing_imp_Increasing simp add: guar_def increasing_def alloc_prog_ok_iff alloc_prog_Allowed)
-apply constrains+
+apply (auto intro!: increasing_imp_Increasing simp add: guar_def increasing_def alloc_prog_ok_iff alloc_prog_Allowed, constrains+)
apply (auto dest: ActsD)
apply (drule_tac f = "lift (giv) " in preserves_imp_eq)
apply auto
@@ -163,7 +139,7 @@
"alloc_prog \<in> stable({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 (constrains)
+apply constrains
apply auto
apply (simp add: diff_add_0 add_commute diff_add_inverse add_assoc add_diff_inverse)
apply (simp (no_asm_simp) add: take_succ)
@@ -180,13 +156,13 @@
apply (subgoal_tac "G \<in> preserves (fun_pair (lift (available_tok), fun_pair (lift (NbR), lift (giv))))")
apply (rotate_tac -1)
apply (cut_tac A = "nat * nat * list(nat)"
- and P = "%<m,n,l> y. n \<le> length(y) &
+ and P = "%<m,n,l> y. n \<le> length(y) &
m #+ tokens(l) = NbT #+ tokens(take(n,y))"
- and g = "lift(rel)" and F = "alloc_prog"
+ and g = "lift(rel)" and F = alloc_prog
in stable_Join_Stable)
-prefer 3 apply assumption;
+prefer 3 apply assumption
apply (auto simp add: Collect_conj_eq)
-apply (frule_tac g = "length" in imp_Increasing_comp)
+apply (frule_tac g = length in imp_Increasing_comp)
apply (blast intro: mono_length)
apply (auto simp add: refl_prefix)
apply (drule_tac a=xa and f = "length comp lift(rel)" in Increasing_imp_Stable)
@@ -200,11 +176,9 @@
apply (erule_tac V = "alloc_prog \<in> stable (?u)" in thin_rl)
apply (drule_tac a = "xc`rel" and f = "lift (rel)" in Increasing_imp_Stable)
apply (auto simp add: Stable_def Constrains_def constrains_def)
-apply (drule bspec)
-apply force
+apply (drule bspec, force)
apply (drule subsetD)
-apply (rule imageI)
-apply assumption
+apply (rule imageI, assumption)
apply (auto simp add: prefix_take_iff)
apply (rotate_tac -1)
apply (erule ssubst)
@@ -219,9 +193,8 @@
apply (auto simp add: guar_def)
apply (rule Always_weaken)
apply (rule AlwaysI)
-apply (rule_tac [2] giv_Bounded_lemma2)
-apply auto
-apply (rule_tac j = "NbT #+ tokens (take (x` NbR, x`rel))" in le_trans)
+apply (rule_tac [2] giv_Bounded_lemma2, auto)
+apply (rule_tac j = "NbT #+ tokens(take (x` NbR, x`rel))" in le_trans)
apply (erule subst)
apply (auto intro!: tokens_mono simp add: prefix_take_iff min_def length_take)
done
@@ -234,105 +207,96 @@
apply (auto intro!: AlwaysI simp add: guar_def)
apply (subgoal_tac "G \<in> preserves (lift (giv))")
prefer 2 apply (simp add: alloc_prog_ok_iff)
-apply (rule_tac P = "%x y. <x,y>:prefix(tokbag)" and A = "list(nat)"
+apply (rule_tac P = "%x y. <x,y>:prefix(tokbag)" and A = "list(nat)"
in stable_Join_Stable)
-apply (constrains)
- prefer 2 apply (simp add: lift_def);
- apply (clarify );
-apply (drule_tac a = "k" in Increasing_imp_Stable)
-apply auto
+apply constrains
+ prefer 2 apply (simp add: lift_def, clarify)
+apply (drule_tac a = k in Increasing_imp_Stable, auto)
done
-(**** Towards proving the liveness property, (31) ****)
+subsection{* Towards proving the liveness property, (31) *}
-(*** First, we lead up to a proof of Lemma 49, page 28. ***)
+subsubsection{*First, we lead up to a proof of Lemma 49, page 28.*}
lemma alloc_prog_transient_lemma:
-"G \<in> program ==> \<forall>k\<in>nat. alloc_prog Join G \<in>
- transient({s\<in>state. k \<le> length(s`rel)}
- \<inter> {s\<in>state. succ(s`NbR) = k})"
+ "[|G \<in> program; k\<in>nat|]
+ ==> alloc_prog Join G \<in>
+ transient({s\<in>state. k \<le> length(s`rel)} \<inter>
+ {s\<in>state. succ(s`NbR) = k})"
apply auto
apply (erule_tac V = "G\<notin>?u" in thin_rl)
-apply (rule_tac act = "alloc_rel_act" in transientI)
+apply (rule_tac act = alloc_rel_act in transientI)
apply (simp (no_asm) add: alloc_prog_def [THEN def_prg_Acts])
apply (simp (no_asm) add: alloc_rel_act_def [THEN def_act_eq, THEN act_subset])
apply (auto simp add: alloc_prog_def [THEN def_prg_Acts] domain_def)
apply (rule ReplaceI)
apply (rule_tac x = "x (available_tok:= x`available_tok #+ nth (x`NbR, x`rel),
- NbR:=succ (x`NbR))"
+ NbR:=succ (x`NbR))"
in exI)
apply (auto intro!: state_update_type)
done
lemma alloc_prog_rel_Stable_NbR_lemma:
-"[| G \<in> program; alloc_prog ok G; k\<in>nat |] ==>
- alloc_prog Join G \<in> Stable({s\<in>state . k \<le> succ(s ` NbR)})"
-apply (auto intro!: stable_imp_Stable simp add: alloc_prog_ok_iff)
-apply constrains
-apply auto
+ "[| G \<in> program; alloc_prog ok G; k\<in>nat |]
+ ==> alloc_prog Join G \<in> Stable({s\<in>state . k \<le> succ(s ` NbR)})"
+apply (auto intro!: stable_imp_Stable simp add: alloc_prog_ok_iff, constrains, auto)
apply (blast intro: le_trans leI)
-apply (drule_tac f = "lift (NbR)" and A = "nat" in preserves_imp_increasing)
-apply (drule_tac [2] g = "succ" in imp_increasing_comp)
+apply (drule_tac f = "lift (NbR)" and A = nat in preserves_imp_increasing)
+apply (drule_tac [2] g = succ in imp_increasing_comp)
apply (rule_tac [2] mono_succ)
-apply (drule_tac [4] x = "k" in increasing_imp_stable)
- prefer 5 apply (simp add: Le_def comp_def)
-apply auto
+apply (drule_tac [4] x = k in increasing_imp_stable)
+ prefer 5 apply (simp add: Le_def comp_def, auto)
done
-lemma alloc_prog_NbR_LeadsTo_lemma [rule_format (no_asm)]:
-"[| G \<in> program; alloc_prog ok G;
- alloc_prog Join G \<in> Incr(lift(rel)) |] ==>
- \<forall>k\<in>nat. alloc_prog Join G \<in>
- {s\<in>state. k \<le> length(s`rel)} \<inter> {s\<in>state. succ(s`NbR) = k}
- LeadsTo {s\<in>state. k \<le> s`NbR}"
-apply clarify
-apply (subgoal_tac "alloc_prog Join G \<in> Stable ({s\<in>state. k \<le> length (s`rel) }) ")
-apply (drule_tac [2] a = "k" and g1 = "length" in imp_Increasing_comp [THEN Increasing_imp_Stable])
+lemma alloc_prog_NbR_LeadsTo_lemma:
+ "[| G \<in> program; alloc_prog ok G;
+ alloc_prog Join G \<in> Incr(lift(rel)); k\<in>nat |]
+ ==> alloc_prog Join G \<in>
+ {s\<in>state. k \<le> length(s`rel)} \<inter> {s\<in>state. succ(s`NbR) = k}
+ LeadsTo {s\<in>state. k \<le> s`NbR}"
+apply (subgoal_tac "alloc_prog Join G \<in> Stable ({s\<in>state. k \<le> length (s`rel)})")
+apply (drule_tac [2] a = k and g1 = length in imp_Increasing_comp [THEN Increasing_imp_Stable])
apply (rule_tac [2] mono_length)
- prefer 3 apply (simp add: );
+ prefer 3 apply simp
apply (simp_all add: refl_prefix Le_def comp_def length_type)
apply (rule LeadsTo_weaken)
apply (rule PSP_Stable)
-prefer 2 apply (assumption)
+prefer 2 apply assumption
apply (rule PSP_Stable)
apply (rule_tac [2] alloc_prog_rel_Stable_NbR_lemma)
-apply (rule alloc_prog_transient_lemma [THEN bspec, THEN transient_imp_leadsTo, THEN leadsTo_imp_LeadsTo])
-apply assumption+
+apply (rule alloc_prog_transient_lemma [THEN transient_imp_leadsTo, THEN leadsTo_imp_LeadsTo], assumption+)
apply (auto dest: not_lt_imp_le elim: lt_asym simp add: le_iff)
done
lemma alloc_prog_NbR_LeadsTo_lemma2 [rule_format]:
- "[| G :program; alloc_prog ok G; alloc_prog Join G \<in> Incr(lift(rel)) |]
- ==> \<forall>k\<in>nat. \<forall>n \<in> nat. n < k -->
- alloc_prog Join G \<in>
- {s\<in>state . k \<le> length(s ` rel)} \<inter> {s\<in>state . s ` NbR = n}
- LeadsTo {x \<in> state. k \<le> length(x`rel)} \<inter>
- (\<Union>m \<in> greater_than(n). {x \<in> state. x ` NbR=m})"
+ "[| G \<in> program; alloc_prog ok G; alloc_prog Join G \<in> Incr(lift(rel));
+ k\<in>nat; n \<in> nat; n < k |]
+ ==> alloc_prog Join G \<in>
+ {s\<in>state . k \<le> length(s ` rel)} \<inter> {s\<in>state . s ` NbR = n}
+ LeadsTo {x \<in> state. k \<le> length(x`rel)} \<inter>
+ (\<Union>m \<in> greater_than(n). {x \<in> state. x ` NbR=m})"
apply (unfold greater_than_def)
-apply clarify
-apply (rule_tac A' = "{x \<in> state. k \<le> length (x`rel) } \<inter> {x \<in> state. n < x`NbR}" in LeadsTo_weaken_R)
+apply (rule_tac A' = "{x \<in> state. k \<le> length(x`rel)} \<inter> {x \<in> state. n < x`NbR}"
+ in LeadsTo_weaken_R)
apply safe
apply (subgoal_tac "alloc_prog Join G \<in> Stable ({s\<in>state. k \<le> length (s`rel) }) ")
-apply (drule_tac [2] a = "k" and g1 = "length" in imp_Increasing_comp [THEN Increasing_imp_Stable])
+apply (drule_tac [2] a = k and g1 = length in imp_Increasing_comp [THEN Increasing_imp_Stable])
apply (rule_tac [2] mono_length)
- prefer 3 apply (simp add: );
+ prefer 3 apply simp
apply (simp_all add: refl_prefix Le_def comp_def length_type)
apply (subst Int_commute)
apply (rule_tac A = " ({s \<in> state . k \<le> length (s ` rel) } \<inter> {s\<in>state . s ` NbR = n}) \<inter> {s\<in>state. k \<le> length (s`rel) }" in LeadsTo_weaken_L)
-apply (rule PSP_Stable)
-apply safe
+apply (rule PSP_Stable, safe)
apply (rule_tac B = "{x \<in> state . n < length (x ` rel) } \<inter> {s\<in>state . s ` NbR = n}" in LeadsTo_Trans)
apply (rule_tac [2] LeadsTo_weaken)
apply (rule_tac [2] k = "succ (n)" in alloc_prog_NbR_LeadsTo_lemma)
-apply (simp_all add: )
-apply (rule subset_imp_LeadsTo)
-apply auto
+apply simp_all
+apply (rule subset_imp_LeadsTo, auto)
apply (blast intro: lt_trans2)
done
-lemma Collect_vimage_eq: "u\<in>nat ==> {<s, f(s)>. s \<in> state} -`` u = {s\<in>state. f(s) < u}"
-apply (force simp add: lt_def)
-done
+lemma Collect_vimage_eq: "u\<in>nat ==> {<s,f(s)>. s \<in> A} -`` u = {s\<in>A. f(s) < u}"
+by (force simp add: lt_def)
(* Lemma 49, page 28 *)
@@ -343,26 +307,22 @@
{s\<in>state. k \<le> length(s`rel)} LeadsTo {s\<in>state. k \<le> s`NbR}"
(* Proof by induction over the difference between k and n *)
apply (rule_tac f = "\<lambda>s\<in>state. k #- s`NbR" in LessThan_induct)
-apply (simp_all add: lam_def)
-apply auto
-apply (rule single_LeadsTo_I)
-apply auto
+apply (simp_all add: lam_def, auto)
+apply (rule single_LeadsTo_I, auto)
apply (simp (no_asm_simp) add: Collect_vimage_eq)
apply (rename_tac "s0")
apply (case_tac "s0`NbR < k")
-apply (rule_tac [2] subset_imp_LeadsTo)
-apply safe
+apply (rule_tac [2] subset_imp_LeadsTo, safe)
apply (auto dest!: not_lt_imp_le)
apply (rule LeadsTo_weaken)
-apply (rule_tac n = "s0`NbR" in alloc_prog_NbR_LeadsTo_lemma2)
-apply safe
-prefer 3 apply (assumption)
+apply (rule_tac n = "s0`NbR" in alloc_prog_NbR_LeadsTo_lemma2, safe)
+prefer 3 apply assumption
apply (auto split add: nat_diff_split simp add: greater_than_def not_lt_imp_le not_le_iff_lt)
apply (blast dest: lt_asym)
apply (force dest: add_lt_elim2)
done
-(** Towards proving lemma 50, page 29 **)
+subsubsection{*Towards proving lemma 50, page 29*}
lemma alloc_prog_giv_Ensures_lemma:
"[| G \<in> program; k\<in>nat; alloc_prog ok G;
@@ -371,27 +331,23 @@
{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. ~ k <length(s`ask)} Un {s\<in>state. length(s`giv) \<noteq> k}"
-apply (rule EnsuresI)
-apply auto
+apply (rule EnsuresI, auto)
apply (erule_tac [2] V = "G\<notin>?u" in thin_rl)
-apply (rule_tac [2] act = "alloc_giv_act" in transientI)
+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 (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\<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)
-apply safe
-apply (auto dest: ActsD simp add: Constrains_def constrains_def length_app 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 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)
+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)
-apply auto
-apply (rule_tac j = "xa ` available_tok" in le_trans)
-apply auto
+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
@@ -399,19 +355,17 @@
in Increasing_imp_Stable)
apply (auto simp add: prefix_iff)
apply (drule StableD)
-apply (auto simp add: Constrains_def constrains_def)
-apply force
+apply (auto simp add: Constrains_def constrains_def, force)
done
lemma alloc_prog_giv_Stable_lemma:
"[| G \<in> program; alloc_prog ok G; k\<in>nat |]
==> alloc_prog Join G \<in> Stable({s\<in>state . k \<le> length(s`giv)})"
-apply (auto intro!: stable_imp_Stable simp add: alloc_prog_ok_iff)
-apply (constrains)
-apply (auto intro: leI simp add: length_app)
-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)
+apply (auto intro!: stable_imp_Stable simp add: alloc_prog_ok_iff, constrains)
+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
@@ -420,24 +374,23 @@
lemma alloc_prog_giv_LeadsTo_lemma:
"[| G \<in> program; alloc_prog ok G;
- alloc_prog Join G \<in> Incr(lift(ask)); k\<in>nat |] ==>
- alloc_prog Join 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`giv)}"
-apply (subgoal_tac "alloc_prog Join 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}")
+ alloc_prog Join G \<in> Incr(lift(ask)); k\<in>nat |]
+ ==> alloc_prog Join 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`giv)}"
+apply (subgoal_tac "alloc_prog Join 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}")
prefer 2 apply (blast intro: alloc_prog_giv_Ensures_lemma [THEN LeadsTo_Basis])
-apply (subgoal_tac "alloc_prog Join G \<in> Stable ({s\<in>state. k < length (s`ask) }) ")
-apply (drule PSP_Stable)
-apply assumption
+apply (subgoal_tac "alloc_prog Join G \<in> Stable ({s\<in>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 (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 (drule_tac a = "succ (k)" and g1 = length in imp_Increasing_comp [THEN Increasing_imp_Stable])
apply (rule mono_length)
- prefer 2 apply (simp add: );
+ prefer 2 apply simp
apply (simp_all add: refl_prefix Le_def comp_def length_type)
done
@@ -452,69 +405,72 @@
==> alloc_prog Join G \<in>
Always({s\<in>state. tokens(s`giv) \<le> tokens(take(s`NbR, s`rel)) -->
NbT \<le> s`available_tok})"
-apply (subgoal_tac "alloc_prog Join 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 (subgoal_tac "alloc_prog Join 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)
-apply auto
-apply (rule Always_weaken)
-apply assumption
-apply auto
-apply (subgoal_tac "0 \<le> tokens (take (x ` NbR, x ` rel)) #- tokens (x`giv) ")
+apply (rule_tac [3] giv_Bounded_lemma2, auto)
+apply (rule Always_weaken, assumption, auto)
+apply (subgoal_tac "0 \<le> tokens(take (x ` NbR, x ` rel)) #- tokens(x`giv) ")
apply (rule_tac [2] nat_diff_split [THEN iffD2])
- prefer 2 apply (force );
+ prefer 2 apply force
apply (subgoal_tac "x`available_tok =
- NbT #+ (tokens(take(x`NbR,x`rel)) #- tokens (x`giv))")
+ NbT #+ (tokens(take(x`NbR,x`rel)) #- tokens(x`giv))")
apply (simp (no_asm_simp))
-apply (rule nat_diff_split [THEN iffD2])
-apply auto
-apply (drule_tac j = "tokens (x ` giv)" in lt_trans2)
+apply (rule nat_diff_split [THEN iffD2], auto)
+apply (drule_tac j = "tokens(x ` giv)" in lt_trans2)
apply assumption
apply auto
done
-(* Main lemmas towards proving property (31) *)
+subsubsection{* Main lemmas towards proving property (31)*}
lemma LeadsTo_strength_R:
"[| F \<in> C LeadsTo B'; F \<in> A-C LeadsTo B; B'<=B |] ==> F \<in> A LeadsTo B"
-by (blast intro: LeadsTo_weaken LeadsTo_Un_Un)
+by (blast intro: LeadsTo_weaken LeadsTo_Un_Un)
lemma PSP_StableI:
"[| F \<in> Stable(C); F \<in> A - C LeadsTo B;
F \<in> A \<inter> C LeadsTo B Un (state - C) |] ==> F \<in> A LeadsTo B"
apply (rule_tac A = " (A-C) Un (A \<inter> C)" in LeadsTo_weaken_L)
- prefer 2 apply (blast)
-apply (rule LeadsTo_Un)
-apply assumption
-apply (blast intro: LeadsTo_weaken dest: PSP_Stable)
+ 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\<in>state. P(s)} = {s\<in>state. ~P(s)}"
-apply auto
-done
+by auto
(*needed?*)
lemma single_state_Diff_eq [simp]: "{s}-{x \<in> state. P(x)} = (if s\<in>state & P(s) then 0 else {s})"
-apply auto
-done
+by auto
+
+locale alloc_progress =
+ fixes G
+ assumes Gprog [intro,simp]: "G \<in> program"
+ and okG [iff]: "alloc_prog ok G"
+ and Incr_rel [intro]: "alloc_prog Join G \<in> Incr(lift(rel))"
+ and Incr_ask [intro]: "alloc_prog Join G \<in> Incr(lift(ask))"
+ and safety: "alloc_prog Join G
+ \<in> Always(\<Inter>k \<in> nat. {s\<in>state. nth(k, s`ask) \<le> NbT})"
+ and progress: "alloc_prog Join G
+ \<in> (\<Inter>k\<in>nat. {s\<in>state. k \<le> tokens(s`giv)} LeadsTo
+ {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 alloc_prog_LeadsTo_tokens_take_NbR_lemma:
-"[| alloc_prog Join G \<in> Incr(lift(rel));
- G \<in> program; alloc_prog ok G; k \<in> tokbag |]
+lemma (in alloc_progress) tokens_take_NbR_lemma:
+ "k \<in> tokbag
==> alloc_prog Join G \<in>
{s\<in>state. k \<le> tokens(s`rel)}
LeadsTo {s\<in>state. k \<le> tokens(take(s`NbR, s`rel))}"
-apply (rule single_LeadsTo_I)
-apply safe
+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 [4] k1 = "length(s`rel)" in alloc_prog_NbR_LeadsTo_lemma3 [THEN LeadsTo_strength_R])
apply (rule_tac [8] subset_imp_LeadsTo)
-apply auto
-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!: 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
@@ -522,256 +478,184 @@
(*Second step in proof of (31): by LHS of the guarantee and transivity of
LeadsTo *)
-lemma alloc_prog_LeadsTo_tokens_take_NbR_lemma2:
-"[| alloc_prog Join G \<in> Incr(lift(rel));
- G \<in> program; alloc_prog ok G; k \<in> tokbag;
- alloc_prog Join G \<in>
- (\<Inter>k\<in>nat. {s\<in>state. k \<le> tokens(s`giv)} LeadsTo {s\<in>state. k \<le> tokens(s`rel)}) |]
- ==> alloc_prog Join G \<in>
- {s\<in>state. tokens(s`giv) = k}
- LeadsTo {s\<in>state. k \<le> tokens(take(s`NbR, s`rel))}"
+lemma (in alloc_progress) tokens_take_NbR_lemma2:
+ "k \<in> tokbag
+ ==> alloc_prog Join G \<in>
+ {s\<in>state. tokens(s`giv) = k}
+ LeadsTo {s\<in>state. k \<le> tokens(take(s`NbR, s`rel))}"
apply (rule LeadsTo_Trans)
-apply (rule_tac [2] alloc_prog_LeadsTo_tokens_take_NbR_lemma)
-apply (blast intro: LeadsTo_weaken_L nat_into_Ord)
-apply assumption+
+ 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 alloc_prog_LeadsTo_length_giv_disj:
-"[| alloc_prog Join G \<in> Incr(lift(rel));
- G \<in> program; alloc_prog ok G; k \<in> tokbag; n \<in> nat;
- alloc_prog Join G \<in>
- (\<Inter>k\<in>nat. {s\<in>state. k \<le> tokens(s`giv)} LeadsTo {s\<in>state. k \<le> tokens(s`rel)}) |]
- ==> alloc_prog Join G \<in>
- {s\<in>state. length(s`giv) = n & tokens(s`giv) = k}
- LeadsTo
- {s\<in>state. (length(s`giv) = n & tokens(s`giv) = k &
- k \<le> tokens(take(s`NbR, s`rel))) | n < length(s`giv)}"
-apply (rule single_LeadsTo_I)
-apply safe
+lemma (in alloc_progress) length_giv_disj:
+ "[| k \<in> tokbag; n \<in> nat |]
+ ==> alloc_prog Join G \<in>
+ {s\<in>state. length(s`giv) = n & tokens(s`giv) = k}
+ LeadsTo
+ {s\<in>state. (length(s`giv) = n & tokens(s`giv) = k &
+ 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 alloc_prog_LeadsTo_tokens_take_NbR_lemma2)
-apply simp_all
-apply safe
-apply (drule prefix_length_le [THEN le_iff [THEN iffD1]])
-apply (force simp add:)
+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 (drule prefix_length_le_equal)
-apply assumption
-apply (simp add:)
+apply (force dest: prefix_length_le_equal)
done
(*Fourth step in proof of (31): we apply lemma (51) *)
-lemma alloc_prog_LeadsTo_length_giv_disj2:
-"[| alloc_prog Join G \<in> Incr(lift(rel));
- alloc_prog Join G \<in> Incr(lift(ask));
- G \<in> program; alloc_prog ok G; k \<in> tokbag; n \<in> nat;
- alloc_prog Join G \<in>
- (\<Inter>k\<in>nat. {s\<in>state. k \<le> tokens(s`giv)} LeadsTo {s\<in>state. k \<le> tokens(s`rel)}) |]
- ==> alloc_prog Join G \<in>
- {s\<in>state. length(s`giv) = n & tokens(s`giv) = k}
- LeadsTo
- {s\<in>state. (length(s`giv) = n & NbT \<le> s`available_tok) |
- n < length(s`giv)}"
+lemma (in alloc_progress) length_giv_disj2:
+ "[|k \<in> tokbag; n \<in> nat|]
+ ==> alloc_prog Join G \<in>
+ {s\<in>state. length(s`giv) = n & tokens(s`giv) = k}
+ LeadsTo
+ {s\<in>state. (length(s`giv) = n & NbT \<le> s`available_tok) |
+ n < length(s`giv)}"
apply (rule LeadsTo_weaken_R)
-apply (rule Always_LeadsToD [OF alloc_prog_Always_lemma alloc_prog_LeadsTo_length_giv_disj])
-apply auto
+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 alloc_prog_LeadsTo_length_giv_disj3:
-"[| alloc_prog Join G \<in> Incr(lift(rel));
- alloc_prog Join G \<in> Incr(lift(ask));
- G \<in> program; alloc_prog ok G; n \<in> nat;
- alloc_prog Join G \<in>
- (\<Inter>k\<in>nat. {s\<in>state. k \<le> tokens(s`giv)} LeadsTo {s\<in>state. k \<le> tokens(s`rel)}) |]
- ==> alloc_prog Join G \<in>
- {s\<in>state. length(s`giv) = n}
- LeadsTo
- {s\<in>state. (length(s`giv) = n & NbT \<le> s`available_tok) |
- n < length(s`giv)}"
+lemma (in alloc_progress) length_giv_disj3:
+ "n \<in> nat
+ ==> alloc_prog Join G \<in>
+ {s\<in>state. length(s`giv) = n}
+ LeadsTo
+ {s\<in>state. (length(s`giv) = n & 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 alloc_prog_LeadsTo_length_giv_disj2)
+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 alloc_prog_LeadsTo_length_ask_giv:
-"[| alloc_prog Join G \<in> Incr(lift(rel));
- alloc_prog Join G \<in> Incr(lift(ask));
- G \<in> program; alloc_prog ok G; k \<in> nat; n < k;
- alloc_prog Join G \<in>
- (\<Inter>k\<in>nat. {s\<in>state. k \<le> tokens(s`giv)} LeadsTo {s\<in>state. k \<le> tokens(s`rel)}) |]
+lemma (in alloc_progress) length_ask_giv:
+ "[|k \<in> nat; n < k|]
==> alloc_prog Join G \<in>
{s\<in>state. length(s`ask) = k & length(s`giv) = n}
LeadsTo
{s\<in>state. (NbT \<le> s`available_tok & length(s`giv) < length(s`ask) &
length(s`giv) = n) |
n < length(s`giv)}"
-apply (rule single_LeadsTo_I)
-apply safe
-apply (rule_tac a1 = "s`ask" and f1 = "lift (ask)" in Increasing_imp_Stable [THEN PSP_StableI])
-apply assumption
-apply simp_all
+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 alloc_prog_LeadsTo_length_giv_disj3)
+apply (rule_tac n = "length(s ` giv)" in length_giv_disj3)
apply simp_all
-apply (blast intro:)
+apply blast
apply clarify
-apply (simp add:)
+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 alloc_prog_LeadsTo_length_ask_giv2:
-"[| alloc_prog Join G \<in> Incr(lift(rel));
- alloc_prog Join G \<in> Incr(lift(ask));
- G \<in> program; alloc_prog ok G; k \<in> nat; n < k;
- alloc_prog Join G \<in>
- Always(\<Inter>k \<in> nat. {s\<in>state. nth(k, s`ask) \<le> NbT});
- alloc_prog Join G \<in>
- (\<Inter>k\<in>nat. {s\<in>state. k \<le> tokens(s`giv)} LeadsTo {s\<in>state. k \<le> tokens(s`rel)}) |]
- ==> alloc_prog Join G \<in>
- {s\<in>state. length(s`ask) = k & length(s`giv) = n}
- LeadsTo
- {s\<in>state. (nth(length(s`giv), s`ask) \<le> s`available_tok &
- length(s`giv) < length(s`ask) & length(s`giv) = n) |
- n < length(s`giv)}"
+lemma (in alloc_progress) length_ask_giv2:
+ "[|k \<in> nat; n < k|]
+ ==> alloc_prog Join G \<in>
+ {s\<in>state. length(s`ask) = k & length(s`giv) = n}
+ LeadsTo
+ {s\<in>state. (nth(length(s`giv), s`ask) \<le> s`available_tok &
+ length(s`giv) < length(s`ask) & length(s`giv) = n) |
+ n < length(s`giv)}"
apply (rule LeadsTo_weaken_R)
-apply (erule Always_LeadsToD [OF asm_rl alloc_prog_LeadsTo_length_ask_giv])
-apply assumption+
-apply clarify
-apply (simp add: INT_iff)
-apply clarify
-apply (drule_tac x = "length (x ` giv)" and P = "%x. ?f (x) \<le> NbT" in bspec)
-apply (simp add:)
+apply (rule Always_LeadsToD [OF safety length_ask_giv], assumption+, clarify)
+apply (simp add: INT_iff, clarify)
+apply (drule_tac x = "length(x ` giv)" and P = "%x. ?f (x) \<le> NbT" in bspec)
+apply simp
apply (blast intro: le_trans)
done
-(*Eighth step in proof of (31): by (50), we get |giv| > n. *)
-lemma alloc_prog_LeadsTo_extend_giv:
-"[| alloc_prog Join G \<in> Incr(lift(rel));
- alloc_prog Join G \<in> Incr(lift(ask));
- G \<in> program; alloc_prog ok G; k \<in> nat; n < k;
- alloc_prog Join G \<in>
- Always(\<Inter>k \<in> nat. {s\<in>state. nth(k, s`ask) \<le> NbT});
- alloc_prog Join G \<in>
- (\<Inter>k\<in>nat. {s\<in>state. k \<le> tokens(s`giv)} LeadsTo {s\<in>state. k \<le> tokens(s`rel)}) |]
- ==> alloc_prog Join G \<in>
- {s\<in>state. length(s`ask) = k & length(s`giv) = n}
- LeadsTo {s\<in>state. n < length(s`giv)}"
+(*Eighth step in proof of (31): by 50, we get |giv| > n. *)
+lemma (in alloc_progress) extend_giv:
+ "[| k \<in> nat; n < k|]
+ ==> alloc_prog Join G \<in>
+ {s\<in>state. length(s`ask) = k & length(s`giv) = n}
+ LeadsTo {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 safe;
- prefer 2 apply (simp add: lt_nat_in_nat)
+apply (simp_all add: Incr_ask lt_nat_in_nat)
apply (rule LeadsTo_weaken_R)
-apply (rule alloc_prog_LeadsTo_length_ask_giv2)
-apply auto
+apply (rule length_ask_giv2, auto)
done
-(*Ninth and tenth steps in proof of (31): by (50), we get |giv| > n.
+(*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 alloc_prog_ask_LeadsTo_giv:
-"[| alloc_prog Join G \<in> Incr(lift(rel));
- alloc_prog Join G \<in> Incr(lift(ask));
- G \<in> program; alloc_prog ok G; k \<in> nat;
- alloc_prog Join G \<in>
- Always(\<Inter>k \<in> nat. {s\<in>state. nth(k, s`ask) \<le> NbT});
- alloc_prog Join G \<in>
- (\<Inter>k\<in>nat. {s\<in>state. k \<le> tokens(s`giv)} LeadsTo {s\<in>state. k \<le> tokens(s`rel)}) |]
+lemma (in alloc_progress) alloc_prog_ask_LeadsTo_giv:
+ "k \<in> nat
==> alloc_prog Join G \<in>
{s\<in>state. k \<le> length(s`ask)} LeadsTo {s\<in>state. k \<le> length(s`giv)}"
(* Proof by induction over the difference between k and n *)
-apply (rule_tac f = "\<lambda>s\<in>state. k #- length (s`giv)" in LessThan_induct)
-apply (simp_all add: lam_def)
- prefer 2 apply (force)
-apply clarify
-apply (simp add: Collect_vimage_eq)
-apply (rule single_LeadsTo_I)
-apply safe
-apply simp
+apply (rule_tac f = "\<lambda>s\<in>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 (case_tac "length(s0 ` giv) < length(s0 ` ask) ")
apply (rule_tac [2] subset_imp_LeadsTo)
- apply safe
- prefer 2
- apply (simp add: not_lt_iff_le)
- apply (blast dest: le_imp_not_lt intro: lt_trans2)
-apply (rule_tac a1 = "s0`ask" and f1 = "lift (ask)"
+ 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 assumption
-apply (simp add:)
-apply (force simp add:)
+apply (rule Incr_ask, simp)
+apply (force)
apply (rule LeadsTo_weaken)
-apply (rule_tac n = "length (s0 ` giv)" and k = "length (s0 ` ask)"
- in alloc_prog_LeadsTo_extend_giv)
-apply simp_all
- apply (force simp add:)
-apply clarify
-apply (simp add:)
-apply (erule disjE)
- apply (blast dest!: prefix_length_le intro: lt_trans2)
-apply (rule not_lt_imp_le)
-apply clarify
-apply (simp_all add: leI diff_lt_iff_lt)
+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
(*Final lemma: combine previous result with lemma (30)*)
-lemma alloc_prog_progress_lemma:
-"[| alloc_prog Join G \<in> Incr(lift(rel));
- alloc_prog Join G \<in> Incr(lift(ask));
- G \<in> program; alloc_prog ok G; h \<in> list(tokbag);
- alloc_prog Join G \<in> Always(\<Inter>k \<in> nat. {s\<in>state. nth(k, s`ask) \<le> NbT});
- alloc_prog Join G \<in>
- (\<Inter>k\<in>nat. {s\<in>state. k \<le> tokens(s`giv)} LeadsTo
- {s\<in>state. k \<le> tokens(s`rel)}) |]
- ==> alloc_prog Join G \<in>
- {s\<in>state. <h, s`ask> \<in> prefix(tokbag)} LeadsTo
- {s\<in>state. <h, s`giv> \<in> prefix(tokbag)}"
+lemma (in alloc_progress) final:
+ "h \<in> list(tokbag)
+ ==> alloc_prog Join G \<in>
+ {s\<in>state. <h, s`ask> \<in> prefix(tokbag)} LeadsTo
+ {s\<in>state. <h, s`giv> \<in> prefix(tokbag)}"
apply (rule single_LeadsTo_I)
- prefer 2 apply (simp)
+ prefer 2 apply simp
apply (rename_tac s0)
-apply (rule_tac a1 = "s0`ask" and f1 = "lift (ask)"
+apply (rule_tac a1 = "s0`ask" and f1 = "lift (ask)"
in Increasing_imp_Stable [THEN PSP_StableI])
- apply assumption
- prefer 2 apply (force simp add:)
-apply (simp_all add: Int_cons_left)
+ apply (rule Incr_ask)
+ apply (simp_all add: Int_cons_left)
apply (rule LeadsTo_weaken)
-apply (rule_tac k1 = "length (s0 ` ask)"
+apply (rule_tac k1 = "length(s0 ` ask)"
in Always_LeadsToD [OF alloc_prog_ask_prefix_giv [THEN guaranteesD]
alloc_prog_ask_LeadsTo_giv])
-apply simp_all
-apply (force simp add:)
-apply (force simp add:)
-apply (blast intro: length_le_prefix_imp_prefix prefix_trans prefix_length_le lt_trans2)
+apply (auto simp add: Incr_ask)
+apply (blast intro: length_le_prefix_imp_prefix prefix_trans prefix_length_le
+ lt_trans2)
done
(** alloc_prog liveness property (31), page 18 **)
-(*missing the LeadsTo assumption on the lhs!?!?!*)
-lemma alloc_prog_progress:
+theorem alloc_prog_progress:
"alloc_prog \<in>
Incr(lift(ask)) \<inter> Incr(lift(rel)) \<inter>
Always(\<Inter>k \<in> nat. {s\<in>state. nth(k, s`ask) \<le> NbT}) \<inter>
- (\<Inter>k\<in>nat. {s\<in>state. k \<le> tokens(s`giv)} LeadsTo
+ (\<Inter>k\<in>nat. {s\<in>state. k \<le> tokens(s`giv)} LeadsTo
{s\<in>state. k \<le> tokens(s`rel)})
guarantees (\<Inter>h \<in> list(tokbag).
{s\<in>state. <h, s`ask> \<in> prefix(tokbag)} LeadsTo
{s\<in>state. <h, s`giv> \<in> prefix(tokbag)})"
apply (rule guaranteesI)
-apply (rule INT_I)
-apply (rule alloc_prog_progress_lemma)
-apply simp_all
-apply (blast intro:)
+apply (rule INT_I [OF _ list.Nil])
+apply (rule alloc_progress.final)
+apply (simp_all add: alloc_progress_def)
done