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