src/ZF/UNITY/AllocImpl.thy
changeset 76213 e44d86131648
parent 69593 3dda49e08b9d
child 76214 0c18df79b1c8
equal deleted inserted replaced
76212:f2094906e491 76213:e44d86131648
     8 
     8 
     9 theory AllocImpl imports ClientImpl begin
     9 theory AllocImpl imports ClientImpl begin
    10 
    10 
    11 abbreviation
    11 abbreviation
    12   NbR :: i            (*number of consumed messages*)  where
    12   NbR :: i            (*number of consumed messages*)  where
    13   "NbR == Var([succ(2)])"
    13   "NbR \<equiv> Var([succ(2)])"
    14 
    14 
    15 abbreviation
    15 abbreviation
    16   available_tok :: i  (*number of free tokens (T in paper)*)  where
    16   available_tok :: i  (*number of free tokens (T in paper)*)  where
    17   "available_tok == Var([succ(succ(2))])"
    17   "available_tok \<equiv> Var([succ(succ(2))])"
    18 
    18 
    19 axiomatization where
    19 axiomatization where
    20   alloc_type_assumes [simp]:
    20   alloc_type_assumes [simp]:
    21   "type_of(NbR) = nat & type_of(available_tok)=nat" and
    21   "type_of(NbR) = nat & type_of(available_tok)=nat" and
    22 
    22 
    23   alloc_default_val_assumes [simp]:
    23   alloc_default_val_assumes [simp]:
    24   "default_val(NbR)  = 0 & default_val(available_tok)=0"
    24   "default_val(NbR)  = 0 & default_val(available_tok)=0"
    25 
    25 
    26 definition
    26 definition
    27   "alloc_giv_act ==
    27   "alloc_giv_act \<equiv>
    28        {<s, t> \<in> state*state.
    28        {<s, t> \<in> state*state.
    29         \<exists>k. k = length(s`giv) &
    29         \<exists>k. k = length(s`giv) &
    30             t = s(giv := s`giv @ [nth(k, s`ask)],
    30             t = s(giv := s`giv @ [nth(k, s`ask)],
    31                   available_tok := s`available_tok #- 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}"
    32             k < length(s`ask) & nth(k, s`ask) \<le> s`available_tok}"
    33 
    33 
    34 definition
    34 definition
    35   "alloc_rel_act ==
    35   "alloc_rel_act \<equiv>
    36        {<s, t> \<in> state*state.
    36        {<s, t> \<in> state*state.
    37         t = s(available_tok := s`available_tok #+ nth(s`NbR, s`rel),
    37         t = s(available_tok := s`available_tok #+ nth(s`NbR, s`rel),
    38               NbR := succ(s`NbR)) &
    38               NbR := succ(s`NbR)) &
    39         s`NbR < length(s`rel)}"
    39         s`NbR < length(s`rel)}"
    40 
    40 
    41 definition
    41 definition
    42   (*The initial condition s`giv=[] is missing from the
    42   (*The initial condition s`giv=[] is missing from the
    43     original definition: S. O. Ehmety *)
    43     original definition: S. O. Ehmety *)
    44   "alloc_prog ==
    44   "alloc_prog \<equiv>
    45        mk_program({s:state. s`available_tok=NbT & s`NbR=0 & s`giv=Nil},
    45        mk_program({s:state. s`available_tok=NbT & s`NbR=0 & s`giv=Nil},
    46                   {alloc_giv_act, alloc_rel_act},
    46                   {alloc_giv_act, alloc_rel_act},
    47                   \<Union>G \<in> preserves(lift(available_tok)) \<inter>
    47                   \<Union>G \<in> preserves(lift(available_tok)) \<inter>
    48                         preserves(lift(NbR)) \<inter>
    48                         preserves(lift(NbR)) \<inter>
    49                         preserves(lift(giv)). Acts(G))"
    49                         preserves(lift(giv)). Acts(G))"
    50 
    50 
    51 
    51 
    52 lemma available_tok_value_type [simp,TC]: "s\<in>state ==> s`available_tok \<in> nat"
    52 lemma available_tok_value_type [simp,TC]: "s\<in>state \<Longrightarrow> s`available_tok \<in> nat"
    53 apply (unfold state_def)
    53 apply (unfold state_def)
    54 apply (drule_tac a = available_tok in apply_type, auto)
    54 apply (drule_tac a = available_tok in apply_type, auto)
    55 done
    55 done
    56 
    56 
    57 lemma NbR_value_type [simp,TC]: "s\<in>state ==> s`NbR \<in> nat"
    57 lemma NbR_value_type [simp,TC]: "s\<in>state \<Longrightarrow> s`NbR \<in> nat"
    58 apply (unfold state_def)
    58 apply (unfold state_def)
    59 apply (drule_tac a = NbR in apply_type, auto)
    59 apply (drule_tac a = NbR in apply_type, auto)
    60 done
    60 done
    61 
    61 
    62 (** The Alloc Program **)
    62 (** The Alloc Program **)
   139 apply (simp add: diff_add_0 add_commute diff_add_inverse add_assoc add_diff_inverse)
   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)
   140 apply (simp (no_asm_simp) add: take_succ)
   141 done
   141 done
   142 
   142 
   143 lemma giv_Bounded_lemma2:
   143 lemma giv_Bounded_lemma2:
   144 "[| G \<in> program; alloc_prog ok G; alloc_prog \<squnion> G \<in> Incr(lift(rel)) |]
   144 "\<lbrakk>G \<in> program; alloc_prog ok G; alloc_prog \<squnion> G \<in> Incr(lift(rel))\<rbrakk>
   145   ==> alloc_prog \<squnion> G \<in> Stable({s\<in>state. s`NbR \<le> length(s`rel)} \<inter>
   145   \<Longrightarrow> 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) =
   146    {s\<in>state. s`available_tok #+ tokens(s`giv) =
   147     NbT #+ tokens(take(s`NbR, s`rel))})"
   147     NbT #+ tokens(take(s`NbR, s`rel))})"
   148 apply (cut_tac giv_Bounded_lamma1)
   148 apply (cut_tac giv_Bounded_lamma1)
   149 apply (cut_tac alloc_prog_preserves_rel_ask_tok)
   149 apply (cut_tac alloc_prog_preserves_rel_ask_tok)
   150 apply (auto simp add: Collect_conj_eq [symmetric] alloc_prog_ok_iff)
   150 apply (auto simp add: Collect_conj_eq [symmetric] alloc_prog_ok_iff)
   212 subsection\<open>Towards proving the liveness property, (31)\<close>
   212 subsection\<open>Towards proving the liveness property, (31)\<close>
   213 
   213 
   214 subsubsection\<open>First, we lead up to a proof of Lemma 49, page 28.\<close>
   214 subsubsection\<open>First, we lead up to a proof of Lemma 49, page 28.\<close>
   215 
   215 
   216 lemma alloc_prog_transient_lemma:
   216 lemma alloc_prog_transient_lemma:
   217      "[|G \<in> program; k\<in>nat|]
   217      "\<lbrakk>G \<in> program; k\<in>nat\<rbrakk>
   218       ==> alloc_prog \<squnion> G \<in>
   218       \<Longrightarrow> alloc_prog \<squnion> G \<in>
   219              transient({s\<in>state. k \<le> length(s`rel)} \<inter>
   219              transient({s\<in>state. k \<le> length(s`rel)} \<inter>
   220              {s\<in>state. succ(s`NbR) = k})"
   220              {s\<in>state. succ(s`NbR) = k})"
   221 apply auto
   221 apply auto
   222 apply (erule_tac V = "G\<notin>u" for u in thin_rl)
   222 apply (erule_tac V = "G\<notin>u" for u in thin_rl)
   223 apply (rule_tac act = alloc_rel_act in transientI)
   223 apply (rule_tac act = alloc_rel_act in transientI)
   230        in exI)
   230        in exI)
   231 apply (auto intro!: state_update_type)
   231 apply (auto intro!: state_update_type)
   232 done
   232 done
   233 
   233 
   234 lemma alloc_prog_rel_Stable_NbR_lemma:
   234 lemma alloc_prog_rel_Stable_NbR_lemma:
   235     "[| G \<in> program; alloc_prog ok G; k\<in>nat |]
   235     "\<lbrakk>G \<in> program; alloc_prog ok G; k\<in>nat\<rbrakk>
   236      ==> alloc_prog \<squnion> G \<in> Stable({s\<in>state . k \<le> succ(s ` NbR)})"
   236      \<Longrightarrow> 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)
   237 apply (auto intro!: stable_imp_Stable simp add: alloc_prog_ok_iff, safety, auto)
   238 apply (blast intro: le_trans leI)
   238 apply (blast intro: le_trans leI)
   239 apply (drule_tac f = "lift (NbR)" and A = nat in preserves_imp_increasing)
   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)
   240 apply (drule_tac [2] g = succ in imp_increasing_comp)
   241 apply (rule_tac [2] mono_succ)
   241 apply (rule_tac [2] mono_succ)
   242 apply (drule_tac [4] x = k in increasing_imp_stable)
   242 apply (drule_tac [4] x = k in increasing_imp_stable)
   243     prefer 5 apply (simp add: Le_def comp_def, auto)
   243     prefer 5 apply (simp add: Le_def comp_def, auto)
   244 done
   244 done
   245 
   245 
   246 lemma alloc_prog_NbR_LeadsTo_lemma:
   246 lemma alloc_prog_NbR_LeadsTo_lemma:
   247      "[| G \<in> program; alloc_prog ok G;
   247      "\<lbrakk>G \<in> program; alloc_prog ok G;
   248          alloc_prog \<squnion> G \<in> Incr(lift(rel)); k\<in>nat |]
   248          alloc_prog \<squnion> G \<in> Incr(lift(rel)); k\<in>nat\<rbrakk>
   249       ==> alloc_prog \<squnion> G \<in>
   249       \<Longrightarrow> alloc_prog \<squnion> G \<in>
   250             {s\<in>state. k \<le> length(s`rel)} \<inter> {s\<in>state. succ(s`NbR) = k}
   250             {s\<in>state. k \<le> length(s`rel)} \<inter> {s\<in>state. succ(s`NbR) = k}
   251             \<longmapsto>w {s\<in>state. k \<le> s`NbR}"
   251             \<longmapsto>w {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)})")
   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])
   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)
   254 apply (rule_tac [2] mono_length)
   262 apply (rule alloc_prog_transient_lemma [THEN transient_imp_leadsTo, THEN leadsTo_imp_LeadsTo], assumption+)
   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)
   263 apply (auto dest: not_lt_imp_le elim: lt_asym simp add: le_iff)
   264 done
   264 done
   265 
   265 
   266 lemma alloc_prog_NbR_LeadsTo_lemma2 [rule_format]:
   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));
   267     "\<lbrakk>G \<in> program; alloc_prog ok G; alloc_prog \<squnion> G \<in> Incr(lift(rel));
   268         k\<in>nat; n \<in> nat; n < k |]
   268         k\<in>nat; n \<in> nat; n < k\<rbrakk>
   269       ==> alloc_prog \<squnion> G \<in>
   269       \<Longrightarrow> alloc_prog \<squnion> G \<in>
   270             {s\<in>state . k \<le> length(s ` rel)} \<inter> {s\<in>state . s ` NbR = n}
   270             {s\<in>state . k \<le> length(s ` rel)} \<inter> {s\<in>state . s ` NbR = n}
   271                \<longmapsto>w {x \<in> state. k \<le> length(x`rel)} \<inter>
   271                \<longmapsto>w {x \<in> state. k \<le> length(x`rel)} \<inter>
   272                  (\<Union>m \<in> greater_than(n). {x \<in> state. x ` NbR=m})"
   272                  (\<Union>m \<in> greater_than(n). {x \<in> state. x ` NbR=m})"
   273 apply (unfold greater_than_def)
   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}"
   274 apply (rule_tac A' = "{x \<in> state. k \<le> length(x`rel)} \<inter> {x \<in> state. n < x`NbR}"
   290 apply simp_all
   290 apply simp_all
   291 apply (rule subset_imp_LeadsTo, auto)
   291 apply (rule subset_imp_LeadsTo, auto)
   292 apply (blast intro: lt_trans2)
   292 apply (blast intro: lt_trans2)
   293 done
   293 done
   294 
   294 
   295 lemma Collect_vimage_eq: "u\<in>nat ==> {<s,f(s)>. s \<in> A} -`` u = {s\<in>A. f(s) < u}"
   295 lemma Collect_vimage_eq: "u\<in>nat \<Longrightarrow> {<s,f(s)>. s \<in> A} -`` u = {s\<in>A. f(s) < u}"
   296 by (force simp add: lt_def)
   296 by (force simp add: lt_def)
   297 
   297 
   298 (* Lemma 49, page 28 *)
   298 (* Lemma 49, page 28 *)
   299 
   299 
   300 lemma alloc_prog_NbR_LeadsTo_lemma3:
   300 lemma alloc_prog_NbR_LeadsTo_lemma3:
   301   "[|G \<in> program; alloc_prog ok G; alloc_prog \<squnion> G \<in> Incr(lift(rel));
   301   "\<lbrakk>G \<in> program; alloc_prog ok G; alloc_prog \<squnion> G \<in> Incr(lift(rel));
   302      k\<in>nat|]
   302      k\<in>nat\<rbrakk>
   303    ==> alloc_prog \<squnion> G \<in>
   303    \<Longrightarrow> alloc_prog \<squnion> G \<in>
   304            {s\<in>state. k \<le> length(s`rel)} \<longmapsto>w {s\<in>state. k \<le> s`NbR}"
   304            {s\<in>state. k \<le> length(s`rel)} \<longmapsto>w {s\<in>state. k \<le> s`NbR}"
   305 (* Proof by induction over the difference between k and n *)
   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)
   306 apply (rule_tac f = "\<lambda>s\<in>state. k #- s`NbR" in LessThan_induct)
   307 apply (simp_all add: lam_def, auto)
   307 apply (simp_all add: lam_def, auto)
   308 apply (rule single_LeadsTo_I, auto)
   308 apply (rule single_LeadsTo_I, auto)
   320 done
   320 done
   321 
   321 
   322 subsubsection\<open>Towards proving lemma 50, page 29\<close>
   322 subsubsection\<open>Towards proving lemma 50, page 29\<close>
   323 
   323 
   324 lemma alloc_prog_giv_Ensures_lemma:
   324 lemma alloc_prog_giv_Ensures_lemma:
   325 "[| G \<in> program; k\<in>nat; alloc_prog ok G;
   325 "\<lbrakk>G \<in> program; k\<in>nat; alloc_prog ok G;
   326   alloc_prog \<squnion> G \<in> Incr(lift(ask)) |] ==>
   326   alloc_prog \<squnion> G \<in> Incr(lift(ask))\<rbrakk> \<Longrightarrow>
   327   alloc_prog \<squnion> G \<in>
   327   alloc_prog \<squnion> G \<in>
   328   {s\<in>state. nth(length(s`giv), s`ask) \<le> s`available_tok} \<inter>
   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}
   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}"
   330   Ensures {s\<in>state. \<not> k <length(s`ask)} \<union> {s\<in>state. length(s`giv) \<noteq> k}"
   331 apply (rule EnsuresI, auto)
   331 apply (rule EnsuresI, auto)
   332 apply (erule_tac [2] V = "G\<notin>u" for u in thin_rl)
   332 apply (erule_tac [2] V = "G\<notin>u" for u in thin_rl)
   333 apply (rule_tac [2] act = alloc_giv_act in transientI)
   333 apply (rule_tac [2] act = alloc_giv_act in transientI)
   334  prefer 2
   334  prefer 2
   335  apply (simp add: alloc_prog_def [THEN def_prg_Acts])
   335  apply (simp add: alloc_prog_def [THEN def_prg_Acts])
   337 apply (auto simp add: alloc_prog_def [THEN def_prg_Acts] domain_def)
   337 apply (auto simp add: alloc_prog_def [THEN def_prg_Acts] domain_def)
   338 apply (erule_tac [2] swap)
   338 apply (erule_tac [2] swap)
   339 apply (rule_tac [2] ReplaceI)
   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)
   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)
   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)
   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. \<not> 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)
   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")
   344 apply (subgoal_tac "length(xa ` giv @ [nth (length(xa ` giv), xa ` ask) ]) = length(xa ` giv) #+ 1")
   345 apply (rule_tac [2] trans)
   345 apply (rule_tac [2] trans)
   346 apply (rule_tac [2] length_app, auto)
   346 apply (rule_tac [2] length_app, auto)
   347 apply (rule_tac j = "xa ` available_tok" in le_trans, auto)
   347 apply (rule_tac j = "xa ` available_tok" in le_trans, auto)
   354 apply (drule StableD)
   354 apply (drule StableD)
   355 apply (auto simp add: Constrains_def constrains_def, force)
   355 apply (auto simp add: Constrains_def constrains_def, force)
   356 done
   356 done
   357 
   357 
   358 lemma alloc_prog_giv_Stable_lemma:
   358 lemma alloc_prog_giv_Stable_lemma:
   359 "[| G \<in> program; alloc_prog ok G; k\<in>nat |]
   359 "\<lbrakk>G \<in> program; alloc_prog ok G; k\<in>nat\<rbrakk>
   360   ==> alloc_prog \<squnion> G \<in> Stable({s\<in>state . k \<le> length(s`giv)})"
   360   \<Longrightarrow> 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)
   361 apply (auto intro!: stable_imp_Stable simp add: alloc_prog_ok_iff, safety)
   362 apply (auto intro: leI)
   362 apply (auto intro: leI)
   363 apply (drule_tac f = "lift (giv)" and g = length in imp_preserves_comp)
   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)
   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)
   365 apply (drule_tac [2] x = k in increasing_imp_stable)
   368 done
   368 done
   369 
   369 
   370 (* Lemma 50, page 29 *)
   370 (* Lemma 50, page 29 *)
   371 
   371 
   372 lemma alloc_prog_giv_LeadsTo_lemma:
   372 lemma alloc_prog_giv_LeadsTo_lemma:
   373 "[| G \<in> program; alloc_prog ok G;
   373 "\<lbrakk>G \<in> program; alloc_prog ok G;
   374     alloc_prog \<squnion> G \<in> Incr(lift(ask)); k\<in>nat |]
   374     alloc_prog \<squnion> G \<in> Incr(lift(ask)); k\<in>nat\<rbrakk>
   375  ==> alloc_prog \<squnion> G \<in>
   375  \<Longrightarrow> alloc_prog \<squnion> G \<in>
   376         {s\<in>state. nth(length(s`giv), s`ask) \<le> s`available_tok} \<inter>
   376         {s\<in>state. nth(length(s`giv), s`ask) \<le> s`available_tok} \<inter>
   377         {s\<in>state.  k < length(s`ask)} \<inter>
   377         {s\<in>state.  k < length(s`ask)} \<inter>
   378         {s\<in>state. length(s`giv) = k}
   378         {s\<in>state. length(s`giv) = k}
   379         \<longmapsto>w {s\<in>state. k < length(s`giv)}"
   379         \<longmapsto>w {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} \<longmapsto>w {s\<in>state. ~ k <length(s`ask) } \<union> {s\<in>state. length(s`giv) \<noteq> k}")
   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} \<longmapsto>w {s\<in>state. \<not> 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])
   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) }) ")
   382 apply (subgoal_tac "alloc_prog \<squnion> G \<in> Stable ({s\<in>state. k < length(s`ask) }) ")
   383 apply (drule PSP_Stable, assumption)
   383 apply (drule PSP_Stable, assumption)
   384 apply (rule LeadsTo_weaken)
   384 apply (rule LeadsTo_weaken)
   385 apply (rule PSP_Stable)
   385 apply (rule PSP_Stable)
   395 text\<open>Lemma 51, page 29.
   395 text\<open>Lemma 51, page 29.
   396   This theorem states as invariant that if the number of
   396   This theorem states as invariant that if the number of
   397   tokens given does not exceed the number returned, then the upper limit
   397   tokens given does not exceed the number returned, then the upper limit
   398   (\<^term>\<open>NbT\<close>) does not exceed the number currently available.\<close>
   398   (\<^term>\<open>NbT\<close>) does not exceed the number currently available.\<close>
   399 lemma alloc_prog_Always_lemma:
   399 lemma alloc_prog_Always_lemma:
   400 "[| G \<in> program; alloc_prog ok G;
   400 "\<lbrakk>G \<in> program; alloc_prog ok G;
   401     alloc_prog \<squnion> G \<in> Incr(lift(ask));
   401     alloc_prog \<squnion> G \<in> Incr(lift(ask));
   402     alloc_prog \<squnion> G \<in> Incr(lift(rel)) |]
   402     alloc_prog \<squnion> G \<in> Incr(lift(rel))\<rbrakk>
   403   ==> alloc_prog \<squnion> G \<in>
   403   \<Longrightarrow> alloc_prog \<squnion> G \<in>
   404         Always({s\<in>state. tokens(s`giv) \<le> tokens(take(s`NbR, s`rel)) \<longrightarrow>
   404         Always({s\<in>state. tokens(s`giv) \<le> tokens(take(s`NbR, s`rel)) \<longrightarrow>
   405                 NbT \<le> s`available_tok})"
   405                 NbT \<le> s`available_tok})"
   406 apply (subgoal_tac
   406 apply (subgoal_tac
   407        "alloc_prog \<squnion> G
   407        "alloc_prog \<squnion> G
   408           \<in> Always ({s\<in>state. s`NbR \<le> length(s`rel) } \<inter>
   408           \<in> Always ({s\<in>state. s`NbR \<le> length(s`rel) } \<inter>
   422 
   422 
   423 
   423 
   424 subsubsection\<open>Main lemmas towards proving property (31)\<close>
   424 subsubsection\<open>Main lemmas towards proving property (31)\<close>
   425 
   425 
   426 lemma LeadsTo_strength_R:
   426 lemma LeadsTo_strength_R:
   427     "[|  F \<in> C \<longmapsto>w B'; F \<in> A-C \<longmapsto>w B; B'<=B |] ==> F \<in> A \<longmapsto>w  B"
   427     "\<lbrakk>F \<in> C \<longmapsto>w B'; F \<in> A-C \<longmapsto>w B; B'<=B\<rbrakk> \<Longrightarrow> F \<in> A \<longmapsto>w  B"
   428 by (blast intro: LeadsTo_weaken LeadsTo_Un_Un)
   428 by (blast intro: LeadsTo_weaken LeadsTo_Un_Un)
   429 
   429 
   430 lemma PSP_StableI:
   430 lemma PSP_StableI:
   431 "[| F \<in> Stable(C); F \<in> A - C \<longmapsto>w B;
   431 "\<lbrakk>F \<in> Stable(C); F \<in> A - C \<longmapsto>w B;
   432    F \<in> A \<inter> C \<longmapsto>w B \<union> (state - C) |] ==> F \<in> A \<longmapsto>w  B"
   432    F \<in> A \<inter> C \<longmapsto>w B \<union> (state - C)\<rbrakk> \<Longrightarrow> F \<in> A \<longmapsto>w  B"
   433 apply (rule_tac A = " (A-C) \<union> (A \<inter> C)" in LeadsTo_weaken_L)
   433 apply (rule_tac A = " (A-C) \<union> (A \<inter> C)" in LeadsTo_weaken_L)
   434  prefer 2 apply blast
   434  prefer 2 apply blast
   435 apply (rule LeadsTo_Un, assumption)
   435 apply (rule LeadsTo_Un, assumption)
   436 apply (blast intro: LeadsTo_weaken dest: PSP_Stable)
   436 apply (blast intro: LeadsTo_weaken dest: PSP_Stable)
   437 done
   437 done
   438 
   438 
   439 lemma state_compl_eq [simp]: "state - {s\<in>state. P(s)} = {s\<in>state. ~P(s)}"
   439 lemma state_compl_eq [simp]: "state - {s\<in>state. P(s)} = {s\<in>state. \<not>P(s)}"
   440 by auto
   440 by auto
   441 
   441 
   442 (*needed?*)
   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})"
   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
   444 by auto
   459 (*First step in proof of (31) -- the corrected version from Charpentier.
   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
   460   This lemma implies that if a client releases some tokens then the Allocator
   461   will eventually recognize that they've been released.*)
   461   will eventually recognize that they've been released.*)
   462 lemma (in alloc_progress) tokens_take_NbR_lemma:
   462 lemma (in alloc_progress) tokens_take_NbR_lemma:
   463  "k \<in> tokbag
   463  "k \<in> tokbag
   464   ==> alloc_prog \<squnion> G \<in>
   464   \<Longrightarrow> alloc_prog \<squnion> G \<in>
   465         {s\<in>state. k \<le> tokens(s`rel)}
   465         {s\<in>state. k \<le> tokens(s`rel)}
   466         \<longmapsto>w {s\<in>state. k \<le> tokens(take(s`NbR, s`rel))}"
   466         \<longmapsto>w {s\<in>state. k \<le> tokens(take(s`NbR, s`rel))}"
   467 apply (rule single_LeadsTo_I, safe)
   467 apply (rule single_LeadsTo_I, safe)
   468 apply (rule_tac a1 = "s`rel" in Increasing_imp_Stable [THEN PSP_StableI])
   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])
   469 apply (rule_tac [4] k1 = "length(s`rel)" in alloc_prog_NbR_LeadsTo_lemma3 [THEN LeadsTo_strength_R])
   478 
   478 
   479 (*Second step in proof of (31): by LHS of the guarantee and transivity of
   479 (*Second step in proof of (31): by LHS of the guarantee and transivity of
   480   \<longmapsto>w *)
   480   \<longmapsto>w *)
   481 lemma (in alloc_progress) tokens_take_NbR_lemma2:
   481 lemma (in alloc_progress) tokens_take_NbR_lemma2:
   482      "k \<in> tokbag
   482      "k \<in> tokbag
   483       ==> alloc_prog \<squnion> G \<in>
   483       \<Longrightarrow> alloc_prog \<squnion> G \<in>
   484             {s\<in>state. tokens(s`giv) = k}
   484             {s\<in>state. tokens(s`giv) = k}
   485             \<longmapsto>w {s\<in>state. k \<le> tokens(take(s`NbR, s`rel))}"
   485             \<longmapsto>w {s\<in>state. k \<le> tokens(take(s`NbR, s`rel))}"
   486 apply (rule LeadsTo_Trans)
   486 apply (rule LeadsTo_Trans)
   487  apply (rule_tac [2] tokens_take_NbR_lemma)
   487  apply (rule_tac [2] tokens_take_NbR_lemma)
   488  prefer 2 apply assumption
   488  prefer 2 apply assumption
   490 apply (blast intro: LeadsTo_weaken_L progress nat_into_Ord)
   490 apply (blast intro: LeadsTo_weaken_L progress nat_into_Ord)
   491 done
   491 done
   492 
   492 
   493 (*Third step in proof of (31): by PSP with the fact that giv increases *)
   493 (*Third step in proof of (31): by PSP with the fact that giv increases *)
   494 lemma (in alloc_progress) length_giv_disj:
   494 lemma (in alloc_progress) length_giv_disj:
   495      "[| k \<in> tokbag; n \<in> nat |]
   495      "\<lbrakk>k \<in> tokbag; n \<in> nat\<rbrakk>
   496       ==> alloc_prog \<squnion> G \<in>
   496       \<Longrightarrow> alloc_prog \<squnion> G \<in>
   497             {s\<in>state. length(s`giv) = n & tokens(s`giv) = k}
   497             {s\<in>state. length(s`giv) = n & tokens(s`giv) = k}
   498             \<longmapsto>w
   498             \<longmapsto>w
   499               {s\<in>state. (length(s`giv) = n & tokens(s`giv) = k &
   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)}"
   500                          k \<le> tokens(take(s`NbR, s`rel))) | n < length(s`giv)}"
   501 apply (rule single_LeadsTo_I, safe)
   501 apply (rule single_LeadsTo_I, safe)
   510 apply (force dest: prefix_length_le_equal) 
   510 apply (force dest: prefix_length_le_equal) 
   511 done
   511 done
   512 
   512 
   513 (*Fourth step in proof of (31): we apply lemma (51) *)
   513 (*Fourth step in proof of (31): we apply lemma (51) *)
   514 lemma (in alloc_progress) length_giv_disj2:
   514 lemma (in alloc_progress) length_giv_disj2:
   515      "[|k \<in> tokbag; n \<in> nat|]
   515      "\<lbrakk>k \<in> tokbag; n \<in> nat\<rbrakk>
   516       ==> alloc_prog \<squnion> G \<in>
   516       \<Longrightarrow> alloc_prog \<squnion> G \<in>
   517             {s\<in>state. length(s`giv) = n & tokens(s`giv) = k}
   517             {s\<in>state. length(s`giv) = n & tokens(s`giv) = k}
   518             \<longmapsto>w
   518             \<longmapsto>w
   519               {s\<in>state. (length(s`giv) = n & NbT \<le> s`available_tok) |
   519               {s\<in>state. (length(s`giv) = n & NbT \<le> s`available_tok) |
   520                         n < length(s`giv)}"
   520                         n < length(s`giv)}"
   521 apply (rule LeadsTo_weaken_R)
   521 apply (rule LeadsTo_weaken_R)
   524 
   524 
   525 (*Fifth step in proof of (31): from the fourth step, taking the union over all
   525 (*Fifth step in proof of (31): from the fourth step, taking the union over all
   526   k\<in>nat *)
   526   k\<in>nat *)
   527 lemma (in alloc_progress) length_giv_disj3:
   527 lemma (in alloc_progress) length_giv_disj3:
   528      "n \<in> nat
   528      "n \<in> nat
   529       ==> alloc_prog \<squnion> G \<in>
   529       \<Longrightarrow> alloc_prog \<squnion> G \<in>
   530             {s\<in>state. length(s`giv) = n}
   530             {s\<in>state. length(s`giv) = n}
   531             \<longmapsto>w
   531             \<longmapsto>w
   532               {s\<in>state. (length(s`giv) = n & NbT \<le> s`available_tok) |
   532               {s\<in>state. (length(s`giv) = n & NbT \<le> s`available_tok) |
   533                         n < length(s`giv)}"
   533                         n < length(s`giv)}"
   534 apply (rule LeadsTo_weaken_L)
   534 apply (rule LeadsTo_weaken_L)
   538 done
   538 done
   539 
   539 
   540 (*Sixth step in proof of (31): from the fifth step, by PSP with the
   540 (*Sixth step in proof of (31): from the fifth step, by PSP with the
   541   assumption that ask increases *)
   541   assumption that ask increases *)
   542 lemma (in alloc_progress) length_ask_giv:
   542 lemma (in alloc_progress) length_ask_giv:
   543  "[|k \<in> nat;  n < k|]
   543  "\<lbrakk>k \<in> nat;  n < k\<rbrakk>
   544   ==> alloc_prog \<squnion> G \<in>
   544   \<Longrightarrow> alloc_prog \<squnion> G \<in>
   545         {s\<in>state. length(s`ask) = k & length(s`giv) = n}
   545         {s\<in>state. length(s`ask) = k & length(s`giv) = n}
   546         \<longmapsto>w
   546         \<longmapsto>w
   547           {s\<in>state. (NbT \<le> s`available_tok & length(s`giv) < length(s`ask) &
   547           {s\<in>state. (NbT \<le> s`available_tok & length(s`giv) < length(s`ask) &
   548                      length(s`giv) = n) |
   548                      length(s`giv) = n) |
   549                     n < length(s`giv)}"
   549                     n < length(s`giv)}"
   561 done
   561 done
   562 
   562 
   563 
   563 
   564 (*Seventh step in proof of (31): no request (ask[k]) exceeds NbT *)
   564 (*Seventh step in proof of (31): no request (ask[k]) exceeds NbT *)
   565 lemma (in alloc_progress) length_ask_giv2:
   565 lemma (in alloc_progress) length_ask_giv2:
   566      "[|k \<in> nat;  n < k|]
   566      "\<lbrakk>k \<in> nat;  n < k\<rbrakk>
   567       ==> alloc_prog \<squnion> G \<in>
   567       \<Longrightarrow> alloc_prog \<squnion> G \<in>
   568             {s\<in>state. length(s`ask) = k & length(s`giv) = n}
   568             {s\<in>state. length(s`ask) = k & length(s`giv) = n}
   569             \<longmapsto>w
   569             \<longmapsto>w
   570               {s\<in>state. (nth(length(s`giv), s`ask) \<le> s`available_tok &
   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) |
   571                          length(s`giv) < length(s`ask) & length(s`giv) = n) |
   572                         n < length(s`giv)}"
   572                         n < length(s`giv)}"
   578 apply (blast intro: le_trans)
   578 apply (blast intro: le_trans)
   579 done
   579 done
   580 
   580 
   581 (*Eighth step in proof of (31): by 50, we get |giv| > n. *)
   581 (*Eighth step in proof of (31): by 50, we get |giv| > n. *)
   582 lemma (in alloc_progress) extend_giv:
   582 lemma (in alloc_progress) extend_giv:
   583      "[| k \<in> nat;  n < k|]
   583      "\<lbrakk>k \<in> nat;  n < k\<rbrakk>
   584       ==> alloc_prog \<squnion> G \<in>
   584       \<Longrightarrow> alloc_prog \<squnion> G \<in>
   585             {s\<in>state. length(s`ask) = k & length(s`giv) = n}
   585             {s\<in>state. length(s`ask) = k & length(s`giv) = n}
   586             \<longmapsto>w {s\<in>state. n < length(s`giv)}"
   586             \<longmapsto>w {s\<in>state. n < length(s`giv)}"
   587 apply (rule LeadsTo_Un_duplicate)
   587 apply (rule LeadsTo_Un_duplicate)
   588 apply (rule LeadsTo_cancel1)
   588 apply (rule LeadsTo_cancel1)
   589 apply (rule_tac [2] alloc_prog_giv_LeadsTo_lemma)
   589 apply (rule_tac [2] alloc_prog_giv_LeadsTo_lemma)
   595 (*Ninth and tenth steps in proof of (31): by 50, we get |giv| > n.
   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
   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.*)
   597   we can't expect |ask| to remain fixed until |giv| increases.*)
   598 lemma (in alloc_progress) alloc_prog_ask_LeadsTo_giv:
   598 lemma (in alloc_progress) alloc_prog_ask_LeadsTo_giv:
   599  "k \<in> nat
   599  "k \<in> nat
   600   ==> alloc_prog \<squnion> G \<in>
   600   \<Longrightarrow> alloc_prog \<squnion> G \<in>
   601         {s\<in>state. k \<le> length(s`ask)} \<longmapsto>w {s\<in>state. k \<le> length(s`giv)}"
   601         {s\<in>state. k \<le> length(s`ask)} \<longmapsto>w {s\<in>state. k \<le> length(s`giv)}"
   602 (* Proof by induction over the difference between k and n *)
   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)
   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)
   604 apply (auto simp add: lam_def Collect_vimage_eq)
   605 apply (rule single_LeadsTo_I, auto)
   605 apply (rule single_LeadsTo_I, auto)
   620 done
   620 done
   621 
   621 
   622 (*Final lemma: combine previous result with lemma (30)*)
   622 (*Final lemma: combine previous result with lemma (30)*)
   623 lemma (in alloc_progress) final:
   623 lemma (in alloc_progress) final:
   624      "h \<in> list(tokbag)
   624      "h \<in> list(tokbag)
   625       ==> alloc_prog \<squnion> G
   625       \<Longrightarrow> alloc_prog \<squnion> G
   626             \<in> {s\<in>state. <h, s`ask> \<in> prefix(tokbag)} \<longmapsto>w
   626             \<in> {s\<in>state. <h, s`ask> \<in> prefix(tokbag)} \<longmapsto>w
   627               {s\<in>state. <h, s`giv> \<in> prefix(tokbag)}"
   627               {s\<in>state. <h, s`giv> \<in> prefix(tokbag)}"
   628 apply (rule single_LeadsTo_I)
   628 apply (rule single_LeadsTo_I)
   629  prefer 2 apply simp
   629  prefer 2 apply simp
   630 apply (rename_tac s0)
   630 apply (rename_tac s0)