src/HOL/UNITY/Comp/AllocImpl.thy
author wenzelm
Sat Jun 14 23:19:51 2008 +0200 (2008-06-14)
changeset 27208 5fe899199f85
parent 16417 9bc16273c2d4
child 32960 69916a850301
permissions -rw-r--r--
proper context for tactics derived from res_inst_tac;
paulson@11194
     1
(*  Title:      HOL/UNITY/AllocImpl
paulson@11194
     2
    ID:         $Id$
paulson@11194
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@11194
     4
    Copyright   1998  University of Cambridge
paulson@11194
     5
*)
paulson@11194
     6
paulson@14089
     7
header{*Implementation of a multiple-client allocator from a single-client allocator*}
paulson@14089
     8
haftmann@16417
     9
theory AllocImpl imports AllocBase Follows PPROD begin
paulson@11194
    10
paulson@11194
    11
paulson@11194
    12
(** State definitions.  OUTPUT variables are locals **)
paulson@11194
    13
paulson@11194
    14
(*Type variable 'b is the type of items being merged*)
paulson@11194
    15
record 'b merge =
paulson@14114
    16
  In   :: "nat => 'b list"  (*merge's INPUT histories: streams to merge*)
paulson@14114
    17
  Out  :: "'b list"         (*merge's OUTPUT history: merged items*)
paulson@14089
    18
  iOut :: "nat list"        (*merge's OUTPUT history: origins of merged items*)
paulson@11194
    19
paulson@11194
    20
record ('a,'b) merge_d =
paulson@14089
    21
  "'b merge" +
paulson@11194
    22
  dummy :: 'a       (*dummy field for new variables*)
paulson@11194
    23
paulson@11194
    24
constdefs
paulson@14089
    25
  non_dummy :: "('a,'b) merge_d => 'b merge"
paulson@11194
    26
    "non_dummy s == (|In = In s, Out = Out s, iOut = iOut s|)"
paulson@11194
    27
paulson@11194
    28
record 'b distr =
paulson@14089
    29
  In  :: "'b list"          (*items to distribute*)
paulson@14089
    30
  iIn :: "nat list"         (*destinations of items to distribute*)
paulson@14089
    31
  Out :: "nat => 'b list"   (*distributed items*)
paulson@11194
    32
paulson@11194
    33
record ('a,'b) distr_d =
paulson@14089
    34
  "'b distr" +
paulson@11194
    35
  dummy :: 'a       (*dummy field for new variables*)
paulson@11194
    36
paulson@11194
    37
record allocState =
paulson@14089
    38
  giv :: "nat list"   (*OUTPUT history: source of tokens*)
paulson@14089
    39
  ask :: "nat list"   (*INPUT: tokens requested from allocator*)
paulson@14089
    40
  rel :: "nat list"   (*INPUT: tokens released to allocator*)
paulson@11194
    41
paulson@11194
    42
record 'a allocState_d =
paulson@11194
    43
  allocState +
paulson@11194
    44
  dummy    :: 'a                (*dummy field for new variables*)
paulson@11194
    45
paulson@11194
    46
record 'a systemState =
paulson@11194
    47
  allocState +
paulson@14089
    48
  mergeRel :: "nat merge"
paulson@14089
    49
  mergeAsk :: "nat merge"
paulson@14089
    50
  distr    :: "nat distr"
paulson@11194
    51
  dummy    :: 'a                  (*dummy field for new variables*)
paulson@11194
    52
paulson@11194
    53
paulson@11194
    54
constdefs
paulson@11194
    55
paulson@11194
    56
(** Merge specification (the number of inputs is Nclients) ***)
paulson@11194
    57
paulson@11194
    58
  (*spec (10)*)
paulson@14089
    59
  merge_increasing :: "('a,'b) merge_d program set"
paulson@11194
    60
    "merge_increasing ==
paulson@11194
    61
         UNIV guarantees (Increasing merge.Out) Int (Increasing merge.iOut)"
paulson@11194
    62
paulson@11194
    63
  (*spec (11)*)
paulson@14089
    64
  merge_eqOut :: "('a,'b) merge_d program set"
paulson@11194
    65
    "merge_eqOut ==
paulson@11194
    66
         UNIV guarantees
paulson@11194
    67
         Always {s. length (merge.Out s) = length (merge.iOut s)}"
paulson@11194
    68
paulson@11194
    69
  (*spec (12)*)
paulson@14089
    70
  merge_bounded :: "('a,'b) merge_d program set"
paulson@11194
    71
    "merge_bounded ==
paulson@11194
    72
         UNIV guarantees
paulson@14089
    73
         Always {s. \<forall>elt \<in> set (merge.iOut s). elt < Nclients}"
paulson@11194
    74
paulson@11194
    75
  (*spec (13)*)
paulson@14089
    76
  merge_follows :: "('a,'b) merge_d program set"
paulson@11194
    77
    "merge_follows ==
paulson@14089
    78
	 (\<Inter>i \<in> lessThan Nclients. Increasing (sub i o merge.In))
paulson@11194
    79
	 guarantees
paulson@14114
    80
	 (\<Inter>i \<in> lessThan Nclients.
paulson@14114
    81
	  (%s. sublist (merge.Out s)
paulson@11194
    82
                       {k. k < size(merge.iOut s) & merge.iOut s! k = i})
paulson@11194
    83
	  Fols (sub i o merge.In))"
paulson@11194
    84
paulson@11194
    85
  (*spec: preserves part*)
paulson@14089
    86
  merge_preserves :: "('a,'b) merge_d program set"
paulson@11194
    87
    "merge_preserves == preserves merge.In Int preserves merge_d.dummy"
paulson@11194
    88
paulson@11194
    89
  (*environmental constraints*)
paulson@14089
    90
  merge_allowed_acts :: "('a,'b) merge_d program set"
paulson@11194
    91
    "merge_allowed_acts ==
paulson@11194
    92
       {F. AllowedActs F =
paulson@11194
    93
	    insert Id (UNION (preserves (funPair merge.Out merge.iOut)) Acts)}"
paulson@11194
    94
paulson@14089
    95
  merge_spec :: "('a,'b) merge_d program set"
paulson@11194
    96
    "merge_spec == merge_increasing Int merge_eqOut Int merge_bounded Int
paulson@11194
    97
                   merge_follows Int merge_allowed_acts Int merge_preserves"
paulson@11194
    98
paulson@11194
    99
(** Distributor specification (the number of outputs is Nclients) ***)
paulson@11194
   100
paulson@11194
   101
  (*spec (14)*)
paulson@14089
   102
  distr_follows :: "('a,'b) distr_d program set"
paulson@11194
   103
    "distr_follows ==
paulson@11194
   104
	 Increasing distr.In Int Increasing distr.iIn Int
paulson@14089
   105
	 Always {s. \<forall>elt \<in> set (distr.iIn s). elt < Nclients}
paulson@11194
   106
	 guarantees
paulson@14114
   107
	 (\<Inter>i \<in> lessThan Nclients.
paulson@11194
   108
	  (sub i o distr.Out) Fols
paulson@14114
   109
	  (%s. sublist (distr.In s)
paulson@11194
   110
                       {k. k < size(distr.iIn s) & distr.iIn s ! k = i}))"
paulson@11194
   111
paulson@14089
   112
  distr_allowed_acts :: "('a,'b) distr_d program set"
paulson@11194
   113
    "distr_allowed_acts ==
paulson@11194
   114
       {D. AllowedActs D = insert Id (UNION (preserves distr.Out) Acts)}"
paulson@11194
   115
paulson@14089
   116
  distr_spec :: "('a,'b) distr_d program set"
paulson@11194
   117
    "distr_spec == distr_follows Int distr_allowed_acts"
paulson@11194
   118
paulson@11194
   119
(** Single-client allocator specification (required) ***)
paulson@11194
   120
paulson@11194
   121
  (*spec (18)*)
paulson@14089
   122
  alloc_increasing :: "'a allocState_d program set"
paulson@11194
   123
    "alloc_increasing == UNIV  guarantees  Increasing giv"
paulson@11194
   124
paulson@11194
   125
  (*spec (19)*)
paulson@14089
   126
  alloc_safety :: "'a allocState_d program set"
paulson@11194
   127
    "alloc_safety ==
paulson@11194
   128
	 Increasing rel
paulson@14114
   129
         guarantees  Always {s. tokens (giv s) \<le> NbT + tokens (rel s)}"
paulson@11194
   130
paulson@11194
   131
  (*spec (20)*)
paulson@14089
   132
  alloc_progress :: "'a allocState_d program set"
paulson@11194
   133
    "alloc_progress ==
paulson@11194
   134
	 Increasing ask Int Increasing rel Int
paulson@14114
   135
         Always {s. \<forall>elt \<in> set (ask s). elt \<le> NbT}
paulson@11194
   136
         Int
paulson@14114
   137
         (\<Inter>h. {s. h \<le> giv s & h pfixGe (ask s)}
paulson@11194
   138
		 LeadsTo
paulson@14114
   139
	         {s. tokens h \<le> tokens (rel s)})
paulson@14114
   140
         guarantees  (\<Inter>h. {s. h \<le> ask s} LeadsTo {s. h pfixLe giv s})"
paulson@11194
   141
paulson@11194
   142
  (*spec: preserves part*)
paulson@14089
   143
  alloc_preserves :: "'a allocState_d program set"
paulson@11194
   144
    "alloc_preserves == preserves rel Int
paulson@11194
   145
                        preserves ask Int
paulson@11194
   146
                        preserves allocState_d.dummy"
paulson@14114
   147
paulson@11194
   148
paulson@11194
   149
  (*environmental constraints*)
paulson@14089
   150
  alloc_allowed_acts :: "'a allocState_d program set"
paulson@11194
   151
    "alloc_allowed_acts ==
paulson@11194
   152
       {F. AllowedActs F = insert Id (UNION (preserves giv) Acts)}"
paulson@11194
   153
paulson@14089
   154
  alloc_spec :: "'a allocState_d program set"
paulson@11194
   155
    "alloc_spec == alloc_increasing Int alloc_safety Int alloc_progress Int
paulson@11194
   156
                   alloc_allowed_acts Int alloc_preserves"
paulson@11194
   157
paulson@11194
   158
locale Merge =
paulson@14089
   159
  fixes M :: "('a,'b::order) merge_d program"
paulson@11194
   160
  assumes
paulson@14089
   161
    Merge_spec:  "M  \<in> merge_spec"
paulson@11194
   162
paulson@11194
   163
locale Distrib =
paulson@14089
   164
  fixes D :: "('a,'b::order) distr_d program"
paulson@11194
   165
  assumes
paulson@14089
   166
    Distrib_spec:  "D \<in> distr_spec"
paulson@11194
   167
paulson@11194
   168
paulson@11194
   169
(****
paulson@14089
   170
#  {** Network specification ***}
paulson@11194
   171
paulson@14089
   172
#    {*spec (9.1)*}
paulson@14089
   173
#    network_ask :: "'a systemState program set
paulson@14089
   174
#	"network_ask == \<Inter>i \<in> lessThan Nclients.
paulson@11194
   175
#			    Increasing (ask o sub i o client)
paulson@11194
   176
#			    guarantees[ask]
paulson@11194
   177
#			    (ask  Fols (ask o sub i o client))"
paulson@11194
   178
paulson@14089
   179
#    {*spec (9.2)*}
paulson@14089
   180
#    network_giv :: "'a systemState program set
paulson@14089
   181
#	"network_giv == \<Inter>i \<in> lessThan Nclients.
paulson@14114
   182
#			    Increasing giv
paulson@11194
   183
#			    guarantees[giv o sub i o client]
paulson@14089
   184
#			    ((giv o sub i o client) Fols giv)"
paulson@11194
   185
paulson@14089
   186
#    {*spec (9.3)*}
paulson@14089
   187
#    network_rel :: "'a systemState program set
paulson@14089
   188
#	"network_rel == \<Inter>i \<in> lessThan Nclients.
paulson@11194
   189
#			    Increasing (rel o sub i o client)
paulson@11194
   190
#			    guarantees[rel]
paulson@11194
   191
#			    (rel  Fols (rel o sub i o client))"
paulson@11194
   192
paulson@14089
   193
#    {*spec: preserves part*}
paulson@14089
   194
#	network_preserves :: "'a systemState program set
paulson@11194
   195
#	"network_preserves == preserves giv  Int
paulson@14089
   196
#			      (\<Inter>i \<in> lessThan Nclients.
paulson@11194
   197
#			       preserves (funPair rel ask o sub i o client))"
paulson@11194
   198
paulson@14089
   199
#    network_spec :: "'a systemState program set
paulson@11194
   200
#	"network_spec == network_ask Int network_giv Int
paulson@11194
   201
#			 network_rel Int network_preserves"
paulson@11194
   202
paulson@11194
   203
paulson@14089
   204
#  {** State mappings **}
paulson@11194
   205
#    sysOfAlloc :: "((nat => merge) * 'a) allocState_d => 'a systemState"
paulson@11194
   206
#	"sysOfAlloc == %s. let (cl,xtr) = allocState_d.dummy s
paulson@11194
   207
#			   in (| giv = giv s,
paulson@11194
   208
#				 ask = ask s,
paulson@11194
   209
#				 rel = rel s,
paulson@11194
   210
#				 client   = cl,
paulson@11194
   211
#				 dummy    = xtr|)"
paulson@11194
   212
paulson@11194
   213
paulson@11194
   214
#    sysOfClient :: "(nat => merge) * 'a allocState_d => 'a systemState"
paulson@11194
   215
#	"sysOfClient == %(cl,al). (| giv = giv al,
paulson@11194
   216
#				     ask = ask al,
paulson@11194
   217
#				     rel = rel al,
paulson@11194
   218
#				     client   = cl,
paulson@11194
   219
#				     systemState.dummy = allocState_d.dummy al|)"
paulson@11194
   220
****)
paulson@11194
   221
paulson@14089
   222
paulson@14089
   223
declare subset_preserves_o [THEN subsetD, intro]
paulson@14089
   224
declare funPair_o_distrib [simp]
paulson@14089
   225
declare Always_INT_distrib [simp]
paulson@14089
   226
declare o_apply [simp del]
paulson@14089
   227
paulson@14089
   228
paulson@14089
   229
subsection{*Theorems for Merge*}
paulson@14089
   230
paulson@14089
   231
lemma (in Merge) Merge_Allowed:
paulson@14089
   232
     "Allowed M = (preserves merge.Out) Int (preserves merge.iOut)"
paulson@14089
   233
apply (cut_tac Merge_spec)
paulson@14114
   234
apply (auto simp add: merge_spec_def merge_allowed_acts_def Allowed_def
paulson@14114
   235
                      safety_prop_Acts_iff)
paulson@14089
   236
done
paulson@14089
   237
paulson@14089
   238
lemma (in Merge) M_ok_iff [iff]:
paulson@14114
   239
     "M ok G = (G \<in> preserves merge.Out & G \<in> preserves merge.iOut &
paulson@14089
   240
                     M \<in> Allowed G)"
paulson@14089
   241
by (auto simp add: Merge_Allowed ok_iff_Allowed)
paulson@14089
   242
paulson@14089
   243
paulson@14089
   244
lemma (in Merge) Merge_Always_Out_eq_iOut:
paulson@14114
   245
     "[| G \<in> preserves merge.Out; G \<in> preserves merge.iOut; M \<in> Allowed G |]
paulson@14089
   246
      ==> M Join G \<in> Always {s. length (merge.Out s) = length (merge.iOut s)}"
paulson@14089
   247
apply (cut_tac Merge_spec)
paulson@14089
   248
apply (force dest: guaranteesD simp add: merge_spec_def merge_eqOut_def)
paulson@14089
   249
done
paulson@14089
   250
paulson@14089
   251
lemma (in Merge) Merge_Bounded:
paulson@14114
   252
     "[| G \<in> preserves merge.iOut; G \<in> preserves merge.Out; M \<in> Allowed G |]
paulson@14089
   253
      ==> M Join G \<in> Always {s. \<forall>elt \<in> set (merge.iOut s). elt < Nclients}"
paulson@14089
   254
apply (cut_tac Merge_spec)
paulson@14089
   255
apply (force dest: guaranteesD simp add: merge_spec_def merge_bounded_def)
paulson@14089
   256
done
paulson@14089
   257
paulson@14089
   258
lemma (in Merge) Merge_Bag_Follows_lemma:
paulson@14114
   259
     "[| G \<in> preserves merge.iOut; G \<in> preserves merge.Out; M \<in> Allowed G |]
paulson@14114
   260
  ==> M Join G \<in> Always
paulson@14114
   261
          {s. (\<Sum>i \<in> lessThan Nclients. bag_of (sublist (merge.Out s)
paulson@14114
   262
                                  {k. k < length (iOut s) & iOut s ! k = i})) =
paulson@14089
   263
              (bag_of o merge.Out) s}"
paulson@14114
   264
apply (rule Always_Compl_Un_eq [THEN iffD1])
paulson@14114
   265
apply (blast intro: Always_Int_I [OF Merge_Always_Out_eq_iOut Merge_Bounded])
paulson@14114
   266
apply (rule UNIV_AlwaysI, clarify)
paulson@14089
   267
apply (subst bag_of_sublist_UN_disjoint [symmetric])
paulson@14089
   268
  apply (simp)
paulson@14089
   269
 apply blast
paulson@14089
   270
apply (simp add: set_conv_nth)
paulson@14089
   271
apply (subgoal_tac
paulson@14089
   272
       "(\<Union>i \<in> lessThan Nclients. {k. k < length (iOut x) & iOut x ! k = i}) =
paulson@14089
   273
       lessThan (length (iOut x))")
paulson@14089
   274
 apply (simp (no_asm_simp) add: o_def)
paulson@14089
   275
apply blast
paulson@14089
   276
done
paulson@14089
   277
paulson@14089
   278
lemma (in Merge) Merge_Bag_Follows:
paulson@14114
   279
     "M \<in> (\<Inter>i \<in> lessThan Nclients. Increasing (sub i o merge.In))
paulson@14114
   280
          guarantees
paulson@14114
   281
             (bag_of o merge.Out) Fols
paulson@14114
   282
             (%s. \<Sum>i \<in> lessThan Nclients. (bag_of o sub i o merge.In) s)"
paulson@14089
   283
apply (rule Merge_Bag_Follows_lemma [THEN Always_Follows1, THEN guaranteesI], auto)
paulson@14089
   284
apply (rule Follows_setsum)
paulson@14089
   285
apply (cut_tac Merge_spec)
paulson@14089
   286
apply (auto simp add: merge_spec_def merge_follows_def o_def)
paulson@14114
   287
apply (drule guaranteesD)
paulson@14089
   288
  prefer 3
paulson@14089
   289
  apply (best intro: mono_bag_of [THEN mono_Follows_apply, THEN subsetD], auto)
paulson@14089
   290
done
paulson@14089
   291
paulson@14089
   292
paulson@14089
   293
subsection{*Theorems for Distributor*}
paulson@14089
   294
paulson@14089
   295
lemma (in Distrib) Distr_Increasing_Out:
paulson@14114
   296
     "D \<in> Increasing distr.In Int Increasing distr.iIn Int
paulson@14114
   297
          Always {s. \<forall>elt \<in> set (distr.iIn s). elt < Nclients}
paulson@14114
   298
          guarantees
paulson@14089
   299
          (\<Inter>i \<in> lessThan Nclients. Increasing (sub i o distr.Out))"
paulson@14089
   300
apply (cut_tac Distrib_spec)
paulson@14089
   301
apply (simp add: distr_spec_def distr_follows_def)
paulson@14089
   302
apply clarify
paulson@14089
   303
apply (blast intro: guaranteesI Follows_Increasing1 dest: guaranteesD)
paulson@14089
   304
done
paulson@14089
   305
paulson@14089
   306
lemma (in Distrib) Distr_Bag_Follows_lemma:
paulson@14114
   307
     "[| G \<in> preserves distr.Out;
paulson@14114
   308
         D Join G \<in> Always {s. \<forall>elt \<in> set (distr.iIn s). elt < Nclients} |]
paulson@14114
   309
  ==> D Join G \<in> Always
paulson@14114
   310
          {s. (\<Sum>i \<in> lessThan Nclients. bag_of (sublist (distr.In s)
paulson@14114
   311
                                  {k. k < length (iIn s) & iIn s ! k = i})) =
paulson@14089
   312
              bag_of (sublist (distr.In s) (lessThan (length (iIn s))))}"
paulson@14089
   313
apply (erule Always_Compl_Un_eq [THEN iffD1])
paulson@14089
   314
apply (rule UNIV_AlwaysI, clarify)
paulson@14089
   315
apply (subst bag_of_sublist_UN_disjoint [symmetric])
paulson@14089
   316
  apply (simp (no_asm))
paulson@14089
   317
 apply blast
paulson@14089
   318
apply (simp add: set_conv_nth)
paulson@14089
   319
apply (subgoal_tac
paulson@14114
   320
       "(\<Union>i \<in> lessThan Nclients. {k. k < length (iIn x) & iIn x ! k = i}) =
paulson@14089
   321
        lessThan (length (iIn x))")
paulson@14089
   322
 apply (simp (no_asm_simp))
paulson@14089
   323
apply blast
paulson@14089
   324
done
paulson@14089
   325
paulson@14089
   326
lemma (in Distrib) D_ok_iff [iff]:
paulson@14089
   327
     "D ok G = (G \<in> preserves distr.Out & D \<in> Allowed G)"
paulson@14089
   328
apply (cut_tac Distrib_spec)
paulson@14114
   329
apply (auto simp add: distr_spec_def distr_allowed_acts_def Allowed_def
paulson@14089
   330
                      safety_prop_Acts_iff ok_iff_Allowed)
paulson@14089
   331
done
paulson@14089
   332
paulson@14114
   333
lemma (in Distrib) Distr_Bag_Follows:
paulson@14114
   334
 "D \<in> Increasing distr.In Int Increasing distr.iIn Int
paulson@14114
   335
      Always {s. \<forall>elt \<in> set (distr.iIn s). elt < Nclients}
paulson@14114
   336
      guarantees
paulson@14114
   337
       (\<Inter>i \<in> lessThan Nclients.
paulson@14114
   338
        (%s. \<Sum>i \<in> lessThan Nclients. (bag_of o sub i o distr.Out) s)
paulson@14114
   339
        Fols
paulson@14089
   340
        (%s. bag_of (sublist (distr.In s) (lessThan (length(distr.iIn s))))))"
paulson@14089
   341
apply (rule guaranteesI, clarify)
paulson@14089
   342
apply (rule Distr_Bag_Follows_lemma [THEN Always_Follows2], auto)
paulson@14089
   343
apply (rule Follows_setsum)
paulson@14089
   344
apply (cut_tac Distrib_spec)
paulson@14089
   345
apply (auto simp add: distr_spec_def distr_follows_def o_def)
paulson@14089
   346
apply (drule guaranteesD)
paulson@14089
   347
  prefer 3
paulson@14089
   348
  apply (best intro: mono_bag_of [THEN mono_Follows_apply, THEN subsetD], auto)
paulson@14089
   349
done
paulson@14089
   350
paulson@14089
   351
paulson@14089
   352
subsection{*Theorems for Allocator*}
paulson@14089
   353
paulson@14089
   354
lemma alloc_refinement_lemma:
paulson@14114
   355
     "!!f::nat=>nat. (\<Inter>i \<in> lessThan n. {s. f i \<le> g i s})
nipkow@15074
   356
      \<subseteq> {s. (SUM x: lessThan n. f x) \<le> (SUM x: lessThan n. g x s)}"
paulson@14089
   357
apply (induct_tac "n")
paulson@14089
   358
apply (auto simp add: lessThan_Suc)
paulson@14089
   359
done
paulson@14089
   360
paulson@14114
   361
lemma alloc_refinement:
paulson@14114
   362
"(\<Inter>i \<in> lessThan Nclients. Increasing (sub i o allocAsk) Int
paulson@14114
   363
                           Increasing (sub i o allocRel))
paulson@14114
   364
  Int
paulson@14114
   365
  Always {s. \<forall>i. i<Nclients -->
paulson@14114
   366
              (\<forall>elt \<in> set ((sub i o allocAsk) s). elt \<le> NbT)}
paulson@14114
   367
  Int
paulson@14114
   368
  (\<Inter>i \<in> lessThan Nclients.
paulson@14114
   369
   \<Inter>h. {s. h \<le> (sub i o allocGiv)s & h pfixGe (sub i o allocAsk)s}
paulson@14114
   370
        LeadsTo {s. tokens h \<le> (tokens o sub i o allocRel)s})
paulson@14114
   371
  \<subseteq>
paulson@14114
   372
 (\<Inter>i \<in> lessThan Nclients. Increasing (sub i o allocAsk) Int
paulson@14114
   373
                           Increasing (sub i o allocRel))
paulson@14114
   374
  Int
paulson@14114
   375
  Always {s. \<forall>i. i<Nclients -->
paulson@14114
   376
              (\<forall>elt \<in> set ((sub i o allocAsk) s). elt \<le> NbT)}
paulson@14114
   377
  Int
paulson@14114
   378
  (\<Inter>hf. (\<Inter>i \<in> lessThan Nclients.
paulson@14114
   379
         {s. hf i \<le> (sub i o allocGiv)s & hf i pfixGe (sub i o allocAsk)s})
paulson@14114
   380
  LeadsTo {s. (\<Sum>i \<in> lessThan Nclients. tokens (hf i)) \<le>
paulson@14114
   381
              (\<Sum>i \<in> lessThan Nclients. (tokens o sub i o allocRel)s)})"
paulson@14089
   382
apply (auto simp add: ball_conj_distrib)
paulson@14089
   383
apply (rename_tac F hf)
paulson@14089
   384
apply (rule LeadsTo_weaken_R [OF Finite_stable_completion alloc_refinement_lemma], blast, blast)
paulson@14089
   385
apply (subgoal_tac "F \<in> Increasing (tokens o (sub i o allocRel))")
paulson@14089
   386
 apply (simp add: Increasing_def o_assoc)
paulson@14089
   387
apply (blast intro: mono_tokens [THEN mono_Increasing_o, THEN subsetD])
paulson@14089
   388
done
paulson@14089
   389
paulson@11194
   390
end