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