src/ZF/UNITY/AllocImpl.thy
author wenzelm
Sat Nov 01 14:20:38 2014 +0100 (2014-11-01)
changeset 58860 fee7cfa69c50
parent 46823 57bf0cecb366
child 59788 6f7b6adac439
permissions -rw-r--r--
eliminated spurious semicolons;
     1 (*  Title:      ZF/UNITY/AllocImpl.thy
     2     Author:     Sidi O Ehmety, Cambridge University Computer Laboratory
     3     Copyright   2002  University of Cambridge
     4 
     5 Single-client allocator implementation.
     6 Charpentier and Chandy, section 7 (page 17).
     7 *)
     8 
     9 theory AllocImpl imports ClientImpl begin
    10 
    11 abbreviation
    12   NbR :: i            (*number of consumed messages*)  where
    13   "NbR == Var([succ(2)])"
    14 
    15 abbreviation
    16   available_tok :: i  (*number of free tokens (T in paper)*)  where
    17   "available_tok == Var([succ(succ(2))])"
    18 
    19 axiomatization where
    20   alloc_type_assumes [simp]:
    21   "type_of(NbR) = nat & type_of(available_tok)=nat" and
    22 
    23   alloc_default_val_assumes [simp]:
    24   "default_val(NbR)  = 0 & default_val(available_tok)=0"
    25 
    26 definition
    27   "alloc_giv_act ==
    28        {<s, t> \<in> state*state.
    29         \<exists>k. k = length(s`giv) &
    30             t = s(giv := s`giv @ [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}"
    33 
    34 definition
    35   "alloc_rel_act ==
    36        {<s, t> \<in> state*state.
    37         t = s(available_tok := s`available_tok #+ nth(s`NbR, s`rel),
    38               NbR := succ(s`NbR)) &
    39         s`NbR < length(s`rel)}"
    40 
    41 definition
    42   (*The initial condition s`giv=[] is missing from the
    43     original definition: S. O. Ehmety *)
    44   "alloc_prog ==
    45        mk_program({s:state. s`available_tok=NbT & s`NbR=0 & s`giv=Nil},
    46                   {alloc_giv_act, alloc_rel_act},
    47                   \<Union>G \<in> preserves(lift(available_tok)) \<inter>
    48                         preserves(lift(NbR)) \<inter>
    49                         preserves(lift(giv)). Acts(G))"
    50 
    51 
    52 lemma available_tok_value_type [simp,TC]: "s\<in>state ==> s`available_tok \<in> nat"
    53 apply (unfold state_def)
    54 apply (drule_tac a = available_tok in apply_type, auto)
    55 done
    56 
    57 lemma NbR_value_type [simp,TC]: "s\<in>state ==> s`NbR \<in> nat"
    58 apply (unfold state_def)
    59 apply (drule_tac a = NbR in apply_type, auto)
    60 done
    61 
    62 (** The Alloc Program **)
    63 
    64 lemma alloc_prog_type [simp,TC]: "alloc_prog \<in> program"
    65 by (simp add: alloc_prog_def)
    66 
    67 declare alloc_prog_def [THEN def_prg_Init, simp]
    68 declare alloc_prog_def [THEN def_prg_AllowedActs, simp]
    69 declare alloc_prog_def [program]
    70 
    71 declare  alloc_giv_act_def [THEN def_act_simp, simp]
    72 declare  alloc_rel_act_def [THEN def_act_simp, simp]
    73 
    74 
    75 lemma alloc_prog_ok_iff:
    76 "\<forall>G \<in> program. (alloc_prog ok G) \<longleftrightarrow>
    77      (G \<in> preserves(lift(giv)) & G \<in> preserves(lift(available_tok)) &
    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])
    80 
    81 
    82 lemma alloc_prog_preserves:
    83     "alloc_prog \<in> (\<Inter>x \<in> var-{giv, available_tok, NbR}. preserves(lift(x)))"
    84 apply (rule Inter_var_DiffI, force)
    85 apply (rule ballI)
    86 apply (rule preservesI, safety)
    87 done
    88 
    89 (* As a special case of the rule above *)
    90 
    91 lemma alloc_prog_preserves_rel_ask_tok:
    92     "alloc_prog \<in>
    93        preserves(lift(rel)) \<inter> preserves(lift(ask)) \<inter> preserves(lift(tok))"
    94 apply auto
    95 apply (insert alloc_prog_preserves)
    96 apply (drule_tac [3] x = tok in Inter_var_DiffD)
    97 apply (drule_tac [2] x = ask in Inter_var_DiffD)
    98 apply (drule_tac x = rel in Inter_var_DiffD, auto)
    99 done
   100 
   101 lemma alloc_prog_Allowed:
   102 "Allowed(alloc_prog) =
   103   preserves(lift(giv)) \<inter> preserves(lift(available_tok)) \<inter> preserves(lift(NbR))"
   104 apply (cut_tac v="lift(giv)" in preserves_type)
   105 apply (auto simp add: Allowed_def client_prog_def [THEN def_prg_Allowed]
   106                       cons_Int_distrib safety_prop_Acts_iff)
   107 done
   108 
   109 (* In particular we have *)
   110 lemma alloc_prog_ok_client_prog: "alloc_prog ok client_prog"
   111 apply (auto simp add: ok_iff_Allowed)
   112 apply (cut_tac alloc_prog_preserves)
   113 apply (cut_tac [2] client_prog_preserves)
   114 apply (auto simp add: alloc_prog_Allowed client_prog_Allowed)
   115 apply (drule_tac [6] B = "preserves (lift (NbR))" in InterD)
   116 apply (drule_tac [5] B = "preserves (lift (available_tok))" in InterD)
   117 apply (drule_tac [4] B = "preserves (lift (giv))" in InterD)
   118 apply (drule_tac [3] B = "preserves (lift (tok))" in InterD)
   119 apply (drule_tac [2] B = "preserves (lift (ask))" in InterD)
   120 apply (drule_tac B = "preserves (lift (rel))" in InterD)
   121 apply auto
   122 done
   123 
   124 (** Safety property: (28) **)
   125 lemma alloc_prog_Increasing_giv: "alloc_prog \<in> program guarantees Incr(lift(giv))"
   126 apply (auto intro!: increasing_imp_Increasing simp add: guar_def
   127   Increasing.increasing_def alloc_prog_ok_iff alloc_prog_Allowed, safety+)
   128 apply (auto dest: ActsD)
   129 apply (drule_tac f = "lift (giv) " in preserves_imp_eq)
   130 apply auto
   131 done
   132 
   133 lemma giv_Bounded_lamma1:
   134 "alloc_prog \<in> stable({s\<in>state. s`NbR \<le> length(s`rel)} \<inter>
   135                      {s\<in>state. s`available_tok #+ tokens(s`giv) =
   136                                  NbT #+ tokens(take(s`NbR, s`rel))})"
   137 apply safety
   138 apply auto
   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)
   141 done
   142 
   143 lemma giv_Bounded_lemma2:
   144 "[| G \<in> program; alloc_prog ok G; alloc_prog \<squnion> G \<in> Incr(lift(rel)) |]
   145   ==> 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) =
   147     NbT #+ tokens(take(s`NbR, s`rel))})"
   148 apply (cut_tac giv_Bounded_lamma1)
   149 apply (cut_tac alloc_prog_preserves_rel_ask_tok)
   150 apply (auto simp add: Collect_conj_eq [symmetric] alloc_prog_ok_iff)
   151 apply (subgoal_tac "G \<in> preserves (fun_pair (lift (available_tok), fun_pair (lift (NbR), lift (giv))))")
   152 apply (rotate_tac -1)
   153 apply (cut_tac A = "nat * nat * list(nat)"
   154              and P = "%<m,n,l> y. n \<le> length(y) &
   155                                   m #+ tokens(l) = NbT #+ tokens(take(n,y))"
   156              and g = "lift(rel)" and F = alloc_prog
   157        in stable_Join_Stable)
   158 prefer 3 apply assumption
   159 apply (auto simp add: Collect_conj_eq)
   160 apply (frule_tac g = length in imp_Increasing_comp)
   161 apply (blast intro: mono_length)
   162 apply (auto simp add: refl_prefix)
   163 apply (drule_tac a=xa and f = "length comp lift(rel)" in Increasing_imp_Stable)
   164 apply assumption
   165 apply (auto simp add: Le_def length_type)
   166 apply (auto dest: ActsD simp add: Stable_def Constrains_def constrains_def)
   167 apply (drule_tac f = "lift (rel) " in preserves_imp_eq)
   168 apply assumption+
   169 apply (force dest: ActsD)
   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)
   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)
   174 apply (drule bspec, force)
   175 apply (drule subsetD)
   176 apply (rule imageI, assumption)
   177 apply (auto simp add: prefix_take_iff)
   178 apply (rotate_tac -1)
   179 apply (erule ssubst)
   180 apply (auto simp add: take_take min_def)
   181 done
   182 
   183 (*Property (29), page 18:
   184   the number of tokens in circulation never exceeds NbT*)
   185 lemma alloc_prog_giv_Bounded: "alloc_prog \<in> Incr(lift(rel))
   186       guarantees Always({s\<in>state. tokens(s`giv) \<le> NbT #+ tokens(s`rel)})"
   187 apply (cut_tac NbT_pos)
   188 apply (auto simp add: guar_def)
   189 apply (rule Always_weaken)
   190 apply (rule AlwaysI)
   191 apply (rule_tac [2] giv_Bounded_lemma2, auto)
   192 apply (rule_tac j = "NbT #+ tokens(take (x` NbR, x`rel))" in le_trans)
   193 apply (erule subst)
   194 apply (auto intro!: tokens_mono simp add: prefix_take_iff min_def length_take)
   195 done
   196 
   197 (*Property (30), page 18: the number of tokens given never exceeds the number
   198   asked for*)
   199 lemma alloc_prog_ask_prefix_giv:
   200      "alloc_prog \<in> Incr(lift(ask)) guarantees
   201                    Always({s\<in>state. <s`giv, s`ask> \<in> prefix(tokbag)})"
   202 apply (auto intro!: AlwaysI simp add: guar_def)
   203 apply (subgoal_tac "G \<in> preserves (lift (giv))")
   204  prefer 2 apply (simp add: alloc_prog_ok_iff)
   205 apply (rule_tac P = "%x y. <x,y> \<in> prefix(tokbag)" and A = "list(nat)"
   206        in stable_Join_Stable)
   207 apply safety
   208  prefer 2 apply (simp add: lift_def, clarify)
   209 apply (drule_tac a = k in Increasing_imp_Stable, auto)
   210 done
   211 
   212 subsection{* Towards proving the liveness property, (31) *}
   213 
   214 subsubsection{*First, we lead up to a proof of Lemma 49, page 28.*}
   215 
   216 lemma alloc_prog_transient_lemma:
   217      "[|G \<in> program; k\<in>nat|]
   218       ==> alloc_prog \<squnion> G \<in>
   219              transient({s\<in>state. k \<le> length(s`rel)} \<inter>
   220              {s\<in>state. succ(s`NbR) = k})"
   221 apply auto
   222 apply (erule_tac V = "G\<notin>?u" in thin_rl)
   223 apply (rule_tac act = alloc_rel_act in transientI)
   224 apply (simp (no_asm) add: alloc_prog_def [THEN def_prg_Acts])
   225 apply (simp (no_asm) add: alloc_rel_act_def [THEN def_act_eq, THEN act_subset])
   226 apply (auto simp add: alloc_prog_def [THEN def_prg_Acts] domain_def)
   227 apply (rule ReplaceI)
   228 apply (rule_tac x = "x (available_tok:= x`available_tok #+ nth (x`NbR, x`rel),
   229                         NbR:=succ (x`NbR))"
   230        in exI)
   231 apply (auto intro!: state_update_type)
   232 done
   233 
   234 lemma alloc_prog_rel_Stable_NbR_lemma:
   235     "[| G \<in> program; alloc_prog ok G; k\<in>nat |]
   236      ==> 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)
   238 apply (blast intro: le_trans leI)
   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)
   241 apply (rule_tac [2] mono_succ)
   242 apply (drule_tac [4] x = k in increasing_imp_stable)
   243     prefer 5 apply (simp add: Le_def comp_def, auto)
   244 done
   245 
   246 lemma alloc_prog_NbR_LeadsTo_lemma:
   247      "[| G \<in> program; alloc_prog ok G;
   248          alloc_prog \<squnion> G \<in> Incr(lift(rel)); k\<in>nat |]
   249       ==> alloc_prog \<squnion> G \<in>
   250             {s\<in>state. k \<le> length(s`rel)} \<inter> {s\<in>state. succ(s`NbR) = k}
   251             LeadsTo {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)})")
   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)
   255     prefer 3 apply simp
   256 apply (simp_all add: refl_prefix Le_def comp_def length_type)
   257 apply (rule LeadsTo_weaken)
   258 apply (rule PSP_Stable)
   259 prefer 2 apply assumption
   260 apply (rule PSP_Stable)
   261 apply (rule_tac [2] alloc_prog_rel_Stable_NbR_lemma)
   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)
   264 done
   265 
   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));
   268         k\<in>nat; n \<in> nat; n < k |]
   269       ==> alloc_prog \<squnion> G \<in>
   270             {s\<in>state . k \<le> length(s ` rel)} \<inter> {s\<in>state . s ` NbR = n}
   271                LeadsTo {x \<in> state. k \<le> length(x`rel)} \<inter>
   272                  (\<Union>m \<in> greater_than(n). {x \<in> state. x ` NbR=m})"
   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}"
   275        in LeadsTo_weaken_R)
   276 apply safe
   277 apply (subgoal_tac "alloc_prog \<squnion> G \<in> Stable ({s\<in>state. k \<le> length (s`rel) }) ")
   278 apply (drule_tac [2] a = k and g1 = length in imp_Increasing_comp [THEN Increasing_imp_Stable])
   279 apply (rule_tac [2] mono_length)
   280     prefer 3 apply simp
   281 apply (simp_all add: refl_prefix Le_def comp_def length_type)
   282 apply (subst Int_commute [of _ "{x \<in> state . n < x ` NbR}"])
   283 apply (rule_tac A = "({s \<in> state . k \<le> length (s ` rel) } \<inter>
   284                       {s\<in>state . s ` NbR = n}) \<inter> {s\<in>state. k \<le> length(s`rel)}"
   285        in LeadsTo_weaken_L)
   286 apply (rule PSP_Stable, safe)
   287 apply (rule_tac B = "{x \<in> state . n < length (x ` rel) } \<inter> {s\<in>state . s ` NbR = n}" in LeadsTo_Trans)
   288 apply (rule_tac [2] LeadsTo_weaken)
   289 apply (rule_tac [2] k = "succ (n)" in alloc_prog_NbR_LeadsTo_lemma)
   290 apply simp_all
   291 apply (rule subset_imp_LeadsTo, auto)
   292 apply (blast intro: lt_trans2)
   293 done
   294 
   295 lemma Collect_vimage_eq: "u\<in>nat ==> {<s,f(s)>. s \<in> A} -`` u = {s\<in>A. f(s) < u}"
   296 by (force simp add: lt_def)
   297 
   298 (* Lemma 49, page 28 *)
   299 
   300 lemma alloc_prog_NbR_LeadsTo_lemma3:
   301   "[|G \<in> program; alloc_prog ok G; alloc_prog \<squnion> G \<in> Incr(lift(rel));
   302      k\<in>nat|]
   303    ==> alloc_prog \<squnion> G \<in>
   304            {s\<in>state. k \<le> length(s`rel)} LeadsTo {s\<in>state. k \<le> s`NbR}"
   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)
   307 apply (simp_all add: lam_def, auto)
   308 apply (rule single_LeadsTo_I, auto)
   309 apply (simp (no_asm_simp) add: Collect_vimage_eq)
   310 apply (rename_tac "s0")
   311 apply (case_tac "s0`NbR < k")
   312 apply (rule_tac [2] subset_imp_LeadsTo, safe)
   313 apply (auto dest!: not_lt_imp_le)
   314 apply (rule LeadsTo_weaken)
   315 apply (rule_tac n = "s0`NbR" in alloc_prog_NbR_LeadsTo_lemma2, safe)
   316 prefer 3 apply assumption
   317 apply (auto split add: nat_diff_split simp add: greater_than_def not_lt_imp_le not_le_iff_lt)
   318 apply (blast dest: lt_asym)
   319 apply (force dest: add_lt_elim2)
   320 done
   321 
   322 subsubsection{*Towards proving lemma 50, page 29*}
   323 
   324 lemma alloc_prog_giv_Ensures_lemma:
   325 "[| G \<in> program; k\<in>nat; alloc_prog ok G;
   326   alloc_prog \<squnion> G \<in> Incr(lift(ask)) |] ==>
   327   alloc_prog \<squnion> G \<in>
   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}
   330   Ensures {s\<in>state. ~ k <length(s`ask)} \<union> {s\<in>state. length(s`giv) \<noteq> k}"
   331 apply (rule EnsuresI, auto)
   332 apply (erule_tac [2] V = "G\<notin>?u" in thin_rl)
   333 apply (rule_tac [2] act = alloc_giv_act in transientI)
   334  prefer 2
   335  apply (simp add: alloc_prog_def [THEN def_prg_Acts])
   336  apply (simp add: alloc_giv_act_def [THEN def_act_eq, THEN act_subset])
   337 apply (auto simp add: alloc_prog_def [THEN def_prg_Acts] domain_def)
   338 apply (erule_tac [2] swap)
   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)
   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)
   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")
   345 apply (rule_tac [2] trans)
   346 apply (rule_tac [2] length_app, auto)
   347 apply (rule_tac j = "xa ` available_tok" in le_trans, auto)
   348 apply (drule_tac f = "lift (available_tok)" in preserves_imp_eq)
   349 apply assumption+
   350 apply auto
   351 apply (drule_tac a = "xa ` ask" and r = "prefix(tokbag)" and A = "list(tokbag)"
   352        in Increasing_imp_Stable)
   353 apply (auto simp add: prefix_iff)
   354 apply (drule StableD)
   355 apply (auto simp add: Constrains_def constrains_def, force)
   356 done
   357 
   358 lemma alloc_prog_giv_Stable_lemma:
   359 "[| G \<in> program; alloc_prog ok G; k\<in>nat |]
   360   ==> 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)
   362 apply (auto intro: leI)
   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)
   365 apply (drule_tac [2] x = k in increasing_imp_stable)
   366  prefer 3 apply (simp add: Le_def comp_def)
   367 apply (auto simp add: length_type)
   368 done
   369 
   370 (* Lemma 50, page 29 *)
   371 
   372 lemma alloc_prog_giv_LeadsTo_lemma:
   373 "[| G \<in> program; alloc_prog ok G;
   374     alloc_prog \<squnion> G \<in> Incr(lift(ask)); k\<in>nat |]
   375  ==> alloc_prog \<squnion> G \<in>
   376         {s\<in>state. nth(length(s`giv), s`ask) \<le> s`available_tok} \<inter>
   377         {s\<in>state.  k < length(s`ask)} \<inter>
   378         {s\<in>state. length(s`giv) = k}
   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) } \<union> {s\<in>state. length(s`giv) \<noteq> k}")
   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) }) ")
   383 apply (drule PSP_Stable, assumption)
   384 apply (rule LeadsTo_weaken)
   385 apply (rule PSP_Stable)
   386 apply (rule_tac [2] k = k in alloc_prog_giv_Stable_lemma)
   387 apply (auto simp add: le_iff)
   388 apply (drule_tac a = "succ (k)" and g1 = length in imp_Increasing_comp [THEN Increasing_imp_Stable])
   389 apply (rule mono_length)
   390  prefer 2 apply simp
   391 apply (simp_all add: refl_prefix Le_def comp_def length_type)
   392 done
   393 
   394 
   395 text{*Lemma 51, page 29.
   396   This theorem states as invariant that if the number of
   397   tokens given does not exceed the number returned, then the upper limit
   398   (@{term NbT}) does not exceed the number currently available.*}
   399 lemma alloc_prog_Always_lemma:
   400 "[| G \<in> program; alloc_prog ok G;
   401     alloc_prog \<squnion> G \<in> Incr(lift(ask));
   402     alloc_prog \<squnion> G \<in> Incr(lift(rel)) |]
   403   ==> alloc_prog \<squnion> G \<in>
   404         Always({s\<in>state. tokens(s`giv) \<le> tokens(take(s`NbR, s`rel)) \<longrightarrow>
   405                 NbT \<le> s`available_tok})"
   406 apply (subgoal_tac
   407        "alloc_prog \<squnion> G
   408           \<in> Always ({s\<in>state. s`NbR \<le> length(s`rel) } \<inter>
   409                     {s\<in>state. s`available_tok #+ tokens(s`giv) = 
   410                               NbT #+ tokens(take (s`NbR, s`rel))})")
   411 apply (rule_tac [2] AlwaysI)
   412 apply (rule_tac [3] giv_Bounded_lemma2, auto)
   413 apply (rule Always_weaken, assumption, auto)
   414 apply (subgoal_tac "0 \<le> tokens(take (x ` NbR, x ` rel)) #- tokens(x`giv) ")
   415  prefer 2 apply (force)
   416 apply (subgoal_tac "x`available_tok =
   417                     NbT #+ (tokens(take(x`NbR,x`rel)) #- tokens(x`giv))")
   418 apply (simp add: )
   419 apply (auto split add: nat_diff_split dest: lt_trans2)
   420 done
   421 
   422 
   423 
   424 subsubsection{* Main lemmas towards proving property (31)*}
   425 
   426 lemma LeadsTo_strength_R:
   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)
   429 
   430 lemma PSP_StableI:
   431 "[| F \<in> Stable(C); F \<in> A - C 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) \<union> (A \<inter> C)" in LeadsTo_weaken_L)
   434  prefer 2 apply blast
   435 apply (rule LeadsTo_Un, assumption)
   436 apply (blast intro: LeadsTo_weaken dest: PSP_Stable)
   437 done
   438 
   439 lemma state_compl_eq [simp]: "state - {s\<in>state. P(s)} = {s\<in>state. ~P(s)}"
   440 by auto
   441 
   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})"
   444 by auto
   445 
   446 
   447 locale alloc_progress =
   448  fixes G
   449  assumes Gprog [intro,simp]: "G \<in> program"
   450      and okG [iff]:          "alloc_prog ok G"
   451      and Incr_rel [intro]:   "alloc_prog \<squnion> G \<in> Incr(lift(rel))"
   452      and Incr_ask [intro]:   "alloc_prog \<squnion> G \<in> Incr(lift(ask))"
   453      and safety:   "alloc_prog \<squnion> G
   454                       \<in> Always(\<Inter>k \<in> nat. {s\<in>state. nth(k, s`ask) \<le> NbT})"
   455      and progress: "alloc_prog \<squnion> G
   456                       \<in> (\<Inter>k\<in>nat. {s\<in>state. k \<le> tokens(s`giv)} LeadsTo
   457                         {s\<in>state. k \<le> tokens(s`rel)})"
   458 
   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
   461   will eventually recognize that they've been released.*)
   462 lemma (in alloc_progress) tokens_take_NbR_lemma:
   463  "k \<in> tokbag
   464   ==> alloc_prog \<squnion> G \<in>
   465         {s\<in>state. k \<le> tokens(s`rel)}
   466         LeadsTo {s\<in>state. k \<le> tokens(take(s`NbR, s`rel))}"
   467 apply (rule single_LeadsTo_I, safe)
   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])
   470 apply (rule_tac [8] subset_imp_LeadsTo)
   471 apply (auto intro!: Incr_rel)
   472 apply (rule_tac j = "tokens(take (length(s`rel), x`rel))" in le_trans)
   473 apply (rule_tac j = "tokens(take (length(s`rel), s`rel))" in le_trans)
   474 apply (auto intro!: tokens_mono take_mono simp add: prefix_iff)
   475 done
   476 
   477 (*** Rest of proofs done by lcp ***)
   478 
   479 (*Second step in proof of (31): by LHS of the guarantee and transivity of
   480   LeadsTo *)
   481 lemma (in alloc_progress) tokens_take_NbR_lemma2:
   482      "k \<in> tokbag
   483       ==> alloc_prog \<squnion> G \<in>
   484             {s\<in>state. tokens(s`giv) = k}
   485             LeadsTo {s\<in>state. k \<le> tokens(take(s`NbR, s`rel))}"
   486 apply (rule LeadsTo_Trans)
   487  apply (rule_tac [2] tokens_take_NbR_lemma)
   488  prefer 2 apply assumption
   489 apply (insert progress) 
   490 apply (blast intro: LeadsTo_weaken_L progress nat_into_Ord)
   491 done
   492 
   493 (*Third step in proof of (31): by PSP with the fact that giv increases *)
   494 lemma (in alloc_progress) length_giv_disj:
   495      "[| k \<in> tokbag; n \<in> nat |]
   496       ==> alloc_prog \<squnion> G \<in>
   497             {s\<in>state. length(s`giv) = n & tokens(s`giv) = k}
   498             LeadsTo
   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)}"
   501 apply (rule single_LeadsTo_I, safe)
   502 apply (rule_tac a1 = "s`giv" in Increasing_imp_Stable [THEN PSP_StableI])
   503 apply (rule alloc_prog_Increasing_giv [THEN guaranteesD])
   504 apply (simp_all add: Int_cons_left)
   505 apply (rule LeadsTo_weaken)
   506 apply (rule_tac k = "tokens(s`giv)" in tokens_take_NbR_lemma2)
   507 apply auto
   508 apply (force dest: prefix_length_le [THEN le_iff [THEN iffD1]]) 
   509 apply (simp add: not_lt_iff_le)
   510 apply (force dest: prefix_length_le_equal) 
   511 done
   512 
   513 (*Fourth step in proof of (31): we apply lemma (51) *)
   514 lemma (in alloc_progress) length_giv_disj2:
   515      "[|k \<in> tokbag; n \<in> nat|]
   516       ==> alloc_prog \<squnion> G \<in>
   517             {s\<in>state. length(s`giv) = n & tokens(s`giv) = k}
   518             LeadsTo
   519               {s\<in>state. (length(s`giv) = n & NbT \<le> s`available_tok) |
   520                         n < length(s`giv)}"
   521 apply (rule LeadsTo_weaken_R)
   522 apply (rule Always_LeadsToD [OF alloc_prog_Always_lemma length_giv_disj], auto)
   523 done
   524 
   525 (*Fifth step in proof of (31): from the fourth step, taking the union over all
   526   k\<in>nat *)
   527 lemma (in alloc_progress) length_giv_disj3:
   528      "n \<in> nat
   529       ==> alloc_prog \<squnion> G \<in>
   530             {s\<in>state. length(s`giv) = n}
   531             LeadsTo
   532               {s\<in>state. (length(s`giv) = n & NbT \<le> s`available_tok) |
   533                         n < length(s`giv)}"
   534 apply (rule LeadsTo_weaken_L)
   535 apply (rule_tac I = nat in LeadsTo_UN)
   536 apply (rule_tac k = i in length_giv_disj2)
   537 apply (simp_all add: UN_conj_eq)
   538 done
   539 
   540 (*Sixth step in proof of (31): from the fifth step, by PSP with the
   541   assumption that ask increases *)
   542 lemma (in alloc_progress) length_ask_giv:
   543  "[|k \<in> nat;  n < k|]
   544   ==> alloc_prog \<squnion> G \<in>
   545         {s\<in>state. length(s`ask) = k & length(s`giv) = n}
   546         LeadsTo
   547           {s\<in>state. (NbT \<le> s`available_tok & length(s`giv) < length(s`ask) &
   548                      length(s`giv) = n) |
   549                     n < length(s`giv)}"
   550 apply (rule single_LeadsTo_I, safe)
   551 apply (rule_tac a1 = "s`ask" and f1 = "lift(ask)" 
   552        in Increasing_imp_Stable [THEN PSP_StableI])
   553 apply (rule Incr_ask, simp_all)
   554 apply (rule LeadsTo_weaken)
   555 apply (rule_tac n = "length(s ` giv)" in length_giv_disj3)
   556 apply simp_all
   557 apply blast
   558 apply clarify
   559 apply simp
   560 apply (blast dest!: prefix_length_le intro: lt_trans2)
   561 done
   562 
   563 
   564 (*Seventh step in proof of (31): no request (ask[k]) exceeds NbT *)
   565 lemma (in alloc_progress) length_ask_giv2:
   566      "[|k \<in> nat;  n < k|]
   567       ==> alloc_prog \<squnion> G \<in>
   568             {s\<in>state. length(s`ask) = k & length(s`giv) = n}
   569             LeadsTo
   570               {s\<in>state. (nth(length(s`giv), s`ask) \<le> s`available_tok &
   571                          length(s`giv) < length(s`ask) & length(s`giv) = n) |
   572                         n < length(s`giv)}"
   573 apply (rule LeadsTo_weaken_R)
   574 apply (rule Always_LeadsToD [OF safety length_ask_giv], assumption+, clarify)
   575 apply (simp add: INT_iff)
   576 apply (drule_tac x = "length(x ` giv)" and P = "%x. ?f (x) \<le> NbT" in bspec)
   577 apply simp
   578 apply (blast intro: le_trans)
   579 done
   580 
   581 (*Eighth step in proof of (31): by 50, we get |giv| > n. *)
   582 lemma (in alloc_progress) extend_giv:
   583      "[| k \<in> nat;  n < k|]
   584       ==> alloc_prog \<squnion> G \<in>
   585             {s\<in>state. length(s`ask) = k & length(s`giv) = n}
   586             LeadsTo {s\<in>state. n < length(s`giv)}"
   587 apply (rule LeadsTo_Un_duplicate)
   588 apply (rule LeadsTo_cancel1)
   589 apply (rule_tac [2] alloc_prog_giv_LeadsTo_lemma)
   590 apply (simp_all add: Incr_ask lt_nat_in_nat)
   591 apply (rule LeadsTo_weaken_R)
   592 apply (rule length_ask_giv2, auto)
   593 done
   594 
   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
   597   we can't expect |ask| to remain fixed until |giv| increases.*)
   598 lemma (in alloc_progress) alloc_prog_ask_LeadsTo_giv:
   599  "k \<in> nat
   600   ==> alloc_prog \<squnion> G \<in>
   601         {s\<in>state. k \<le> length(s`ask)} LeadsTo {s\<in>state. k \<le> length(s`giv)}"
   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)
   604 apply (auto simp add: lam_def Collect_vimage_eq)
   605 apply (rule single_LeadsTo_I, auto)
   606 apply (rename_tac "s0")
   607 apply (case_tac "length(s0 ` giv) < length(s0 ` ask) ")
   608  apply (rule_tac [2] subset_imp_LeadsTo)
   609   apply (auto simp add: not_lt_iff_le)
   610  prefer 2 apply (blast dest: le_imp_not_lt intro: lt_trans2)
   611 apply (rule_tac a1 = "s0`ask" and f1 = "lift (ask)"
   612        in Increasing_imp_Stable [THEN PSP_StableI])
   613 apply (rule Incr_ask, simp)
   614 apply (force)
   615 apply (rule LeadsTo_weaken)
   616 apply (rule_tac n = "length(s0 ` giv)" and k = "length(s0 ` ask)"
   617        in extend_giv) 
   618 apply (auto dest: not_lt_imp_le simp add: leI diff_lt_iff_lt) 
   619 apply (blast dest!: prefix_length_le intro: lt_trans2)
   620 done
   621 
   622 (*Final lemma: combine previous result with lemma (30)*)
   623 lemma (in alloc_progress) final:
   624      "h \<in> list(tokbag)
   625       ==> alloc_prog \<squnion> G
   626             \<in> {s\<in>state. <h, s`ask> \<in> prefix(tokbag)} LeadsTo
   627               {s\<in>state. <h, s`giv> \<in> prefix(tokbag)}"
   628 apply (rule single_LeadsTo_I)
   629  prefer 2 apply simp
   630 apply (rename_tac s0)
   631 apply (rule_tac a1 = "s0`ask" and f1 = "lift (ask)"
   632        in Increasing_imp_Stable [THEN PSP_StableI])
   633    apply (rule Incr_ask)
   634   apply (simp_all add: Int_cons_left)
   635 apply (rule LeadsTo_weaken)
   636 apply (rule_tac k1 = "length(s0 ` ask)"
   637        in Always_LeadsToD [OF alloc_prog_ask_prefix_giv [THEN guaranteesD]
   638                               alloc_prog_ask_LeadsTo_giv])
   639 apply (auto simp add: Incr_ask)
   640 apply (blast intro: length_le_prefix_imp_prefix prefix_trans prefix_length_le 
   641                     lt_trans2)
   642 done
   643 
   644 (** alloc_prog liveness property (31), page 18 **)
   645 
   646 theorem alloc_prog_progress:
   647 "alloc_prog \<in>
   648     Incr(lift(ask)) \<inter> Incr(lift(rel)) \<inter>
   649     Always(\<Inter>k \<in> nat. {s\<in>state. nth(k, s`ask) \<le> NbT}) \<inter>
   650     (\<Inter>k\<in>nat. {s\<in>state. k \<le> tokens(s`giv)} LeadsTo
   651               {s\<in>state. k \<le> tokens(s`rel)})
   652   guarantees (\<Inter>h \<in> list(tokbag).
   653               {s\<in>state. <h, s`ask> \<in> prefix(tokbag)} LeadsTo
   654               {s\<in>state. <h, s`giv> \<in> prefix(tokbag)})"
   655 apply (rule guaranteesI)
   656 apply (rule INT_I)
   657 apply (rule alloc_progress.final)
   658 apply (auto simp add: alloc_progress_def)
   659 done
   660 
   661 end