src/HOL/UNITY/Comp/Alloc.thy
author wenzelm
Sat Jun 14 23:19:51 2008 +0200 (2008-06-14)
changeset 27208 5fe899199f85
parent 25995 21b51f748daf
child 30510 4120fc59dd85
permissions -rw-r--r--
proper context for tactics derived from res_inst_tac;
paulson@21710
     1
(*  ID:         $Id$
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
Specification of Chandy and Charpentier's Allocator
paulson@11194
     6
*)
paulson@11194
     7
wenzelm@17310
     8
theory Alloc
paulson@21710
     9
imports AllocBase "../PPROD"
wenzelm@17310
    10
begin
paulson@11194
    11
paulson@21710
    12
subsection{*State definitions.  OUTPUT variables are locals*}
paulson@11194
    13
paulson@11194
    14
record clientState =
paulson@21710
    15
  giv :: "nat list"   --{*client's INPUT history:  tokens GRANTED*}
paulson@21710
    16
  ask :: "nat list"   --{*client's OUTPUT history: tokens REQUESTED*}
paulson@21710
    17
  rel :: "nat list"   --{*client's OUTPUT history: tokens RELEASED*}
paulson@11194
    18
paulson@11194
    19
record 'a clientState_d =
paulson@11194
    20
  clientState +
paulson@21710
    21
  dummy :: 'a       --{*dummy field for new variables*}
paulson@11194
    22
paulson@11194
    23
constdefs
paulson@21710
    24
  --{*DUPLICATED FROM Client.thy, but with "tok" removed*}
paulson@21710
    25
  --{*Maybe want a special theory section to declare such maps*}
wenzelm@17310
    26
  non_dummy :: "'a clientState_d => clientState"
paulson@11194
    27
    "non_dummy s == (|giv = giv s, ask = ask s, rel = rel s|)"
paulson@11194
    28
paulson@21710
    29
  --{*Renaming map to put a Client into the standard form*}
paulson@11194
    30
  client_map :: "'a clientState_d => clientState*'a"
paulson@11194
    31
    "client_map == funPair non_dummy dummy"
paulson@11194
    32
wenzelm@24147
    33
paulson@11194
    34
record allocState =
paulson@21710
    35
  allocGiv :: "nat => nat list"   --{*OUTPUT history: source of "giv" for i*}
paulson@21710
    36
  allocAsk :: "nat => nat list"   --{*INPUT: allocator's copy of "ask" for i*}
paulson@21710
    37
  allocRel :: "nat => nat list"   --{*INPUT: allocator's copy of "rel" for i*}
paulson@11194
    38
paulson@11194
    39
record 'a allocState_d =
paulson@11194
    40
  allocState +
paulson@21710
    41
  dummy    :: 'a                --{*dummy field for new variables*}
paulson@11194
    42
paulson@11194
    43
record 'a systemState =
paulson@11194
    44
  allocState +
paulson@21710
    45
  client :: "nat => clientState"  --{*states of all clients*}
paulson@21710
    46
  dummy  :: 'a                    --{*dummy field for new variables*}
paulson@11194
    47
paulson@11194
    48
paulson@11194
    49
constdefs
paulson@11194
    50
paulson@21710
    51
--{** Resource allocation system specification **}
paulson@11194
    52
paulson@21710
    53
  --{*spec (1)*}
wenzelm@17310
    54
  system_safety :: "'a systemState program set"
paulson@11194
    55
    "system_safety ==
nipkow@15074
    56
     Always {s. (SUM i: lessThan Nclients. (tokens o giv o sub i o client)s)
paulson@21710
    57
     \<le> NbT + (SUM i: lessThan Nclients. (tokens o rel o sub i o client)s)}"
paulson@11194
    58
paulson@21710
    59
  --{*spec (2)*}
wenzelm@17310
    60
  system_progress :: "'a systemState program set"
paulson@11194
    61
    "system_progress == INT i : lessThan Nclients.
wenzelm@24147
    62
                        INT h.
wenzelm@24147
    63
                          {s. h \<le> (ask o sub i o client)s} LeadsTo
wenzelm@24147
    64
                          {s. h pfixLe (giv o sub i o client) s}"
paulson@11194
    65
wenzelm@17310
    66
  system_spec :: "'a systemState program set"
paulson@11194
    67
    "system_spec == system_safety Int system_progress"
paulson@11194
    68
paulson@21710
    69
--{** Client specification (required) ***}
paulson@11194
    70
paulson@21710
    71
  --{*spec (3)*}
wenzelm@17310
    72
  client_increasing :: "'a clientState_d program set"
paulson@11194
    73
    "client_increasing ==
paulson@11194
    74
         UNIV guarantees  Increasing ask Int Increasing rel"
paulson@11194
    75
paulson@21710
    76
  --{*spec (4)*}
wenzelm@17310
    77
  client_bounded :: "'a clientState_d program set"
paulson@11194
    78
    "client_bounded ==
paulson@21710
    79
         UNIV guarantees  Always {s. ALL elt : set (ask s). elt \<le> NbT}"
paulson@11194
    80
paulson@21710
    81
  --{*spec (5)*}
wenzelm@17310
    82
  client_progress :: "'a clientState_d program set"
paulson@11194
    83
    "client_progress ==
wenzelm@24147
    84
         Increasing giv  guarantees
wenzelm@24147
    85
         (INT h. {s. h \<le> giv s & h pfixGe ask s}
wenzelm@24147
    86
                 LeadsTo {s. tokens h \<le> (tokens o rel) s})"
paulson@11194
    87
paulson@21710
    88
  --{*spec: preserves part*}
wenzelm@17310
    89
  client_preserves :: "'a clientState_d program set"
paulson@11194
    90
    "client_preserves == preserves giv Int preserves clientState_d.dummy"
paulson@11194
    91
paulson@21710
    92
  --{*environmental constraints*}
wenzelm@17310
    93
  client_allowed_acts :: "'a clientState_d program set"
paulson@11194
    94
    "client_allowed_acts ==
paulson@11194
    95
       {F. AllowedActs F =
wenzelm@24147
    96
            insert Id (UNION (preserves (funPair rel ask)) Acts)}"
paulson@11194
    97
wenzelm@17310
    98
  client_spec :: "'a clientState_d program set"
paulson@11194
    99
    "client_spec == client_increasing Int client_bounded Int client_progress
paulson@11194
   100
                    Int client_allowed_acts Int client_preserves"
paulson@11194
   101
paulson@21710
   102
--{** Allocator specification (required) **}
paulson@11194
   103
paulson@21710
   104
  --{*spec (6)*}
wenzelm@17310
   105
  alloc_increasing :: "'a allocState_d program set"
paulson@11194
   106
    "alloc_increasing ==
wenzelm@24147
   107
         UNIV  guarantees
wenzelm@24147
   108
         (INT i : lessThan Nclients. Increasing (sub i o allocGiv))"
paulson@11194
   109
paulson@21710
   110
  --{*spec (7)*}
wenzelm@17310
   111
  alloc_safety :: "'a allocState_d program set"
paulson@11194
   112
    "alloc_safety ==
wenzelm@24147
   113
         (INT i : lessThan Nclients. Increasing (sub i o allocRel))
paulson@11194
   114
         guarantees
wenzelm@24147
   115
         Always {s. (SUM i: lessThan Nclients. (tokens o sub i o allocGiv)s)
paulson@21710
   116
         \<le> NbT + (SUM i: lessThan Nclients. (tokens o sub i o allocRel)s)}"
paulson@11194
   117
paulson@21710
   118
  --{*spec (8)*}
wenzelm@17310
   119
  alloc_progress :: "'a allocState_d program set"
paulson@11194
   120
    "alloc_progress ==
wenzelm@24147
   121
         (INT i : lessThan Nclients. Increasing (sub i o allocAsk) Int
wenzelm@24147
   122
                                     Increasing (sub i o allocRel))
paulson@11194
   123
         Int
paulson@11194
   124
         Always {s. ALL i<Nclients.
wenzelm@24147
   125
                     ALL elt : set ((sub i o allocAsk) s). elt \<le> NbT}
paulson@11194
   126
         Int
wenzelm@24147
   127
         (INT i : lessThan Nclients.
wenzelm@24147
   128
          INT h. {s. h \<le> (sub i o allocGiv)s & h pfixGe (sub i o allocAsk)s}
wenzelm@24147
   129
                 LeadsTo
wenzelm@24147
   130
                 {s. tokens h \<le> (tokens o sub i o allocRel)s})
paulson@11194
   131
         guarantees
wenzelm@24147
   132
             (INT i : lessThan Nclients.
wenzelm@24147
   133
              INT h. {s. h \<le> (sub i o allocAsk) s}
wenzelm@24147
   134
                     LeadsTo
wenzelm@24147
   135
                     {s. h pfixLe (sub i o allocGiv) s})"
paulson@11194
   136
paulson@11194
   137
  (*NOTE: to follow the original paper, the formula above should have had
wenzelm@24147
   138
        INT h. {s. h i \<le> (sub i o allocGiv)s & h i pfixGe (sub i o allocAsk)s}
wenzelm@24147
   139
               LeadsTo
wenzelm@24147
   140
               {s. tokens h i \<le> (tokens o sub i o allocRel)s})
paulson@11194
   141
    thus h should have been a function variable.  However, only h i is ever
paulson@11194
   142
    looked at.*)
paulson@11194
   143
paulson@21710
   144
  --{*spec: preserves part*}
wenzelm@17310
   145
  alloc_preserves :: "'a allocState_d program set"
paulson@11194
   146
    "alloc_preserves == preserves allocRel Int preserves allocAsk Int
paulson@11194
   147
                        preserves allocState_d.dummy"
wenzelm@24147
   148
paulson@21710
   149
  --{*environmental constraints*}
wenzelm@17310
   150
  alloc_allowed_acts :: "'a allocState_d program set"
paulson@11194
   151
    "alloc_allowed_acts ==
paulson@11194
   152
       {F. AllowedActs F =
wenzelm@24147
   153
            insert Id (UNION (preserves allocGiv) Acts)}"
paulson@11194
   154
wenzelm@17310
   155
  alloc_spec :: "'a allocState_d program set"
paulson@11194
   156
    "alloc_spec == alloc_increasing Int alloc_safety Int alloc_progress Int
paulson@11194
   157
                   alloc_allowed_acts Int alloc_preserves"
paulson@11194
   158
paulson@21710
   159
--{** Network specification **}
paulson@11194
   160
paulson@21710
   161
  --{*spec (9.1)*}
wenzelm@17310
   162
  network_ask :: "'a systemState program set"
paulson@11194
   163
    "network_ask == INT i : lessThan Nclients.
wenzelm@24147
   164
                        Increasing (ask o sub i o client)  guarantees
wenzelm@24147
   165
                        ((sub i o allocAsk) Fols (ask o sub i o client))"
paulson@11194
   166
paulson@21710
   167
  --{*spec (9.2)*}
wenzelm@17310
   168
  network_giv :: "'a systemState program set"
paulson@11194
   169
    "network_giv == INT i : lessThan Nclients.
wenzelm@24147
   170
                        Increasing (sub i o allocGiv)
wenzelm@24147
   171
                        guarantees
wenzelm@24147
   172
                        ((giv o sub i o client) Fols (sub i o allocGiv))"
paulson@11194
   173
paulson@21710
   174
  --{*spec (9.3)*}
wenzelm@17310
   175
  network_rel :: "'a systemState program set"
paulson@11194
   176
    "network_rel == INT i : lessThan Nclients.
wenzelm@24147
   177
                        Increasing (rel o sub i o client)
wenzelm@24147
   178
                        guarantees
wenzelm@24147
   179
                        ((sub i o allocRel) Fols (rel o sub i o client))"
paulson@11194
   180
paulson@21710
   181
  --{*spec: preserves part*}
wenzelm@17310
   182
  network_preserves :: "'a systemState program set"
paulson@11194
   183
    "network_preserves ==
paulson@11194
   184
       preserves allocGiv  Int
paulson@11194
   185
       (INT i : lessThan Nclients. preserves (rel o sub i o client)  Int
paulson@11194
   186
                                   preserves (ask o sub i o client))"
wenzelm@24147
   187
paulson@21710
   188
  --{*environmental constraints*}
wenzelm@17310
   189
  network_allowed_acts :: "'a systemState program set"
paulson@11194
   190
    "network_allowed_acts ==
paulson@11194
   191
       {F. AllowedActs F =
paulson@11194
   192
           insert Id
wenzelm@24147
   193
            (UNION (preserves allocRel Int
wenzelm@24147
   194
                    (INT i: lessThan Nclients. preserves(giv o sub i o client)))
wenzelm@24147
   195
                  Acts)}"
paulson@11194
   196
wenzelm@17310
   197
  network_spec :: "'a systemState program set"
paulson@11194
   198
    "network_spec == network_ask Int network_giv Int
paulson@11194
   199
                     network_rel Int network_allowed_acts Int
paulson@11194
   200
                     network_preserves"
paulson@11194
   201
paulson@11194
   202
paulson@21710
   203
--{** State mappings **}
paulson@11194
   204
  sysOfAlloc :: "((nat => clientState) * 'a) allocState_d => 'a systemState"
paulson@11194
   205
    "sysOfAlloc == %s. let (cl,xtr) = allocState_d.dummy s
paulson@11194
   206
                       in (| allocGiv = allocGiv s,
wenzelm@24147
   207
                             allocAsk = allocAsk s,
wenzelm@24147
   208
                             allocRel = allocRel s,
wenzelm@24147
   209
                             client   = cl,
wenzelm@24147
   210
                             dummy    = xtr|)"
paulson@11194
   211
paulson@11194
   212
paulson@11194
   213
  sysOfClient :: "(nat => clientState) * 'a allocState_d => 'a systemState"
paulson@11194
   214
    "sysOfClient == %(cl,al). (| allocGiv = allocGiv al,
wenzelm@24147
   215
                                 allocAsk = allocAsk al,
wenzelm@24147
   216
                                 allocRel = allocRel al,
wenzelm@24147
   217
                                 client   = cl,
wenzelm@24147
   218
                                 systemState.dummy = allocState_d.dummy al|)"
paulson@11194
   219
wenzelm@24147
   220
consts
wenzelm@17310
   221
    Alloc   :: "'a allocState_d program"
wenzelm@17310
   222
    Client  :: "'a clientState_d program"
wenzelm@17310
   223
    Network :: "'a systemState program"
wenzelm@17310
   224
    System  :: "'a systemState program"
wenzelm@24147
   225
wenzelm@17310
   226
axioms
wenzelm@17310
   227
    Alloc:   "Alloc   : alloc_spec"
wenzelm@17310
   228
    Client:  "Client  : client_spec"
wenzelm@17310
   229
    Network: "Network : network_spec"
paulson@11194
   230
paulson@11194
   231
defs
wenzelm@17310
   232
    System_def:
paulson@11194
   233
      "System == rename sysOfAlloc Alloc Join Network Join
paulson@11194
   234
                 (rename sysOfClient
wenzelm@24147
   235
                  (plam x: lessThan Nclients. rename client_map Client))"
paulson@11194
   236
paulson@11194
   237
paulson@11194
   238
(**
paulson@11194
   239
locale System =
wenzelm@24147
   240
  fixes
paulson@11194
   241
    Alloc   :: 'a allocState_d program
paulson@11194
   242
    Client  :: 'a clientState_d program
paulson@11194
   243
    Network :: 'a systemState program
paulson@11194
   244
    System  :: 'a systemState program
paulson@11194
   245
paulson@11194
   246
  assumes
paulson@11194
   247
    Alloc   "Alloc   : alloc_spec"
paulson@11194
   248
    Client  "Client  : client_spec"
paulson@11194
   249
    Network "Network : network_spec"
paulson@11194
   250
paulson@11194
   251
  defines
paulson@11194
   252
    System_def
paulson@11194
   253
      "System == rename sysOfAlloc Alloc
paulson@11194
   254
                 Join
paulson@11194
   255
                 Network
paulson@11194
   256
                 Join
paulson@11194
   257
                 (rename sysOfClient
wenzelm@24147
   258
                  (plam x: lessThan Nclients. rename client_map Client))"
paulson@11194
   259
**)
paulson@11194
   260
wenzelm@21632
   261
(*Perhaps equalities.ML shouldn't add this in the first place!*)
wenzelm@21632
   262
declare image_Collect [simp del]
wenzelm@21632
   263
wenzelm@21632
   264
declare subset_preserves_o [THEN [2] rev_subsetD, intro]
wenzelm@21632
   265
declare subset_preserves_o [THEN [2] rev_subsetD, simp]
wenzelm@21632
   266
declare funPair_o_distrib [simp]
wenzelm@21632
   267
declare Always_INT_distrib [simp]
wenzelm@21632
   268
declare o_apply [simp del]
wenzelm@21632
   269
wenzelm@21632
   270
(*For rewriting of specifications related by "guarantees"*)
wenzelm@21632
   271
lemmas [simp] =
wenzelm@21632
   272
  rename_image_constrains
wenzelm@21632
   273
  rename_image_stable
wenzelm@21632
   274
  rename_image_increasing
wenzelm@21632
   275
  rename_image_invariant
wenzelm@21632
   276
  rename_image_Constrains
wenzelm@21632
   277
  rename_image_Stable
wenzelm@21632
   278
  rename_image_Increasing
wenzelm@21632
   279
  rename_image_Always
wenzelm@21632
   280
  rename_image_leadsTo
wenzelm@21632
   281
  rename_image_LeadsTo
wenzelm@21632
   282
  rename_preserves
wenzelm@21632
   283
  rename_image_preserves
wenzelm@21632
   284
  lift_image_preserves
wenzelm@21632
   285
  bij_image_INT
wenzelm@21632
   286
  bij_is_inj [THEN image_Int]
wenzelm@21632
   287
  bij_image_Collect_eq
wenzelm@21632
   288
wenzelm@21632
   289
ML {*
wenzelm@21632
   290
(*Splits up conjunctions & intersections: like CONJUNCTS in the HOL system*)
wenzelm@24147
   291
fun list_of_Int th =
wenzelm@21632
   292
    (list_of_Int (th RS conjunct1) @ list_of_Int (th RS conjunct2))
wenzelm@21632
   293
    handle THM _ => (list_of_Int (th RS IntD1) @ list_of_Int (th RS IntD2))
wenzelm@24147
   294
    handle THM _ => (list_of_Int (th RS @{thm INT_D}))
wenzelm@21632
   295
    handle THM _ => (list_of_Int (th RS bspec))
wenzelm@21632
   296
    handle THM _ => [th];
wenzelm@21632
   297
*}
wenzelm@21632
   298
wenzelm@21632
   299
lemmas lessThanBspec = lessThan_iff [THEN iffD2, THEN [2] bspec]
wenzelm@21632
   300
wenzelm@24147
   301
setup {*
wenzelm@24147
   302
let
wenzelm@24147
   303
  fun normalized th =
wenzelm@24147
   304
    normalized (th RS spec
wenzelm@24147
   305
      handle THM _ => th RS @{thm lessThanBspec}
wenzelm@24147
   306
      handle THM _ => th RS bspec
wenzelm@24147
   307
      handle THM _ => th RS (@{thm guarantees_INT_right_iff} RS iffD1))
wenzelm@24147
   308
    handle THM _ => th;
wenzelm@21632
   309
in
wenzelm@24147
   310
  Attrib.add_attributes [("normalized", Attrib.no_args (Thm.rule_attribute (K normalized)), "")]
wenzelm@21632
   311
end
wenzelm@21632
   312
*}
wenzelm@21632
   313
wenzelm@21632
   314
(*** bijectivity of sysOfAlloc [MUST BE AUTOMATED] ***)
wenzelm@21632
   315
ML {*
wenzelm@24147
   316
fun record_auto_tac (cs, ss) =
wenzelm@24147
   317
  auto_tac (cs addIs [ext] addSWrapper record_split_wrapper,
wenzelm@24147
   318
    ss addsimps [@{thm sysOfAlloc_def}, @{thm sysOfClient_def},
wenzelm@24147
   319
      @{thm client_map_def}, @{thm non_dummy_def}, @{thm funPair_def},
wenzelm@24147
   320
      @{thm o_apply}, @{thm Let_def}])
wenzelm@21632
   321
*}
wenzelm@21632
   322
wenzelm@24147
   323
method_setup record_auto = {*
wenzelm@24147
   324
  Method.ctxt_args (fn ctxt => Method.SIMPLE_METHOD (record_auto_tac (local_clasimpset_of ctxt)))
wenzelm@24147
   325
*} ""
wenzelm@21632
   326
wenzelm@21632
   327
lemma inj_sysOfAlloc [iff]: "inj sysOfAlloc"
wenzelm@21632
   328
  apply (unfold sysOfAlloc_def Let_def)
wenzelm@21632
   329
  apply (rule inj_onI)
wenzelm@24147
   330
  apply record_auto
wenzelm@21632
   331
  done
wenzelm@21632
   332
paulson@21710
   333
text{*We need the inverse; also having it simplifies the proof of surjectivity*}
wenzelm@24147
   334
lemma inv_sysOfAlloc_eq [simp]: "!!s. inv sysOfAlloc s =
wenzelm@24147
   335
             (| allocGiv = allocGiv s,
wenzelm@24147
   336
                allocAsk = allocAsk s,
wenzelm@24147
   337
                allocRel = allocRel s,
wenzelm@21632
   338
                allocState_d.dummy = (client s, dummy s) |)"
wenzelm@21632
   339
  apply (rule inj_sysOfAlloc [THEN inv_f_eq])
wenzelm@24147
   340
  apply record_auto
wenzelm@21632
   341
  done
wenzelm@21632
   342
wenzelm@21632
   343
lemma surj_sysOfAlloc [iff]: "surj sysOfAlloc"
wenzelm@21632
   344
  apply (simp add: surj_iff expand_fun_eq o_apply)
wenzelm@24147
   345
  apply record_auto
wenzelm@21632
   346
  done
wenzelm@21632
   347
wenzelm@21632
   348
lemma bij_sysOfAlloc [iff]: "bij sysOfAlloc"
wenzelm@21632
   349
  apply (blast intro: bijI)
wenzelm@21632
   350
  done
wenzelm@21632
   351
wenzelm@21632
   352
paulson@21710
   353
subsubsection{*bijectivity of @{term sysOfClient}*}
wenzelm@21632
   354
wenzelm@21632
   355
lemma inj_sysOfClient [iff]: "inj sysOfClient"
wenzelm@21632
   356
  apply (unfold sysOfClient_def)
wenzelm@21632
   357
  apply (rule inj_onI)
wenzelm@24147
   358
  apply record_auto
wenzelm@21632
   359
  done
wenzelm@21632
   360
wenzelm@24147
   361
lemma inv_sysOfClient_eq [simp]: "!!s. inv sysOfClient s =
wenzelm@24147
   362
             (client s,
wenzelm@24147
   363
              (| allocGiv = allocGiv s,
wenzelm@24147
   364
                 allocAsk = allocAsk s,
wenzelm@24147
   365
                 allocRel = allocRel s,
wenzelm@21632
   366
                 allocState_d.dummy = systemState.dummy s|) )"
wenzelm@21632
   367
  apply (rule inj_sysOfClient [THEN inv_f_eq])
wenzelm@24147
   368
  apply record_auto
wenzelm@21632
   369
  done
wenzelm@21632
   370
wenzelm@21632
   371
lemma surj_sysOfClient [iff]: "surj sysOfClient"
wenzelm@21632
   372
  apply (simp add: surj_iff expand_fun_eq o_apply)
wenzelm@24147
   373
  apply record_auto
wenzelm@21632
   374
  done
wenzelm@21632
   375
wenzelm@21632
   376
lemma bij_sysOfClient [iff]: "bij sysOfClient"
wenzelm@21632
   377
  apply (blast intro: bijI)
wenzelm@21632
   378
  done
wenzelm@21632
   379
wenzelm@21632
   380
paulson@21710
   381
subsubsection{*bijectivity of @{term client_map}*}
wenzelm@21632
   382
wenzelm@21632
   383
lemma inj_client_map [iff]: "inj client_map"
wenzelm@21632
   384
  apply (unfold inj_on_def)
wenzelm@24147
   385
  apply record_auto
wenzelm@21632
   386
  done
wenzelm@21632
   387
wenzelm@24147
   388
lemma inv_client_map_eq [simp]: "!!s. inv client_map s =
wenzelm@24147
   389
             (%(x,y).(|giv = giv x, ask = ask x, rel = rel x,
wenzelm@21632
   390
                       clientState_d.dummy = y|)) s"
wenzelm@21632
   391
  apply (rule inj_client_map [THEN inv_f_eq])
wenzelm@24147
   392
  apply record_auto
wenzelm@21632
   393
  done
wenzelm@21632
   394
wenzelm@21632
   395
lemma surj_client_map [iff]: "surj client_map"
wenzelm@21632
   396
  apply (simp add: surj_iff expand_fun_eq o_apply)
wenzelm@24147
   397
  apply record_auto
wenzelm@21632
   398
  done
wenzelm@21632
   399
wenzelm@21632
   400
lemma bij_client_map [iff]: "bij client_map"
wenzelm@21632
   401
  apply (blast intro: bijI)
wenzelm@21632
   402
  done
wenzelm@21632
   403
wenzelm@21632
   404
paulson@21710
   405
text{*o-simprules for @{term client_map}*}
wenzelm@21632
   406
wenzelm@21632
   407
lemma fst_o_client_map: "fst o client_map = non_dummy"
wenzelm@21632
   408
  apply (unfold client_map_def)
wenzelm@21632
   409
  apply (rule fst_o_funPair)
wenzelm@21632
   410
  done
wenzelm@21632
   411
wenzelm@21632
   412
ML {* bind_thms ("fst_o_client_map'", make_o_equivs (thm "fst_o_client_map")) *}
wenzelm@21632
   413
declare fst_o_client_map' [simp]
wenzelm@21632
   414
wenzelm@21632
   415
lemma snd_o_client_map: "snd o client_map = clientState_d.dummy"
wenzelm@21632
   416
  apply (unfold client_map_def)
wenzelm@21632
   417
  apply (rule snd_o_funPair)
wenzelm@21632
   418
  done
wenzelm@21632
   419
wenzelm@21632
   420
ML {* bind_thms ("snd_o_client_map'", make_o_equivs (thm "snd_o_client_map")) *}
wenzelm@21632
   421
declare snd_o_client_map' [simp]
wenzelm@21632
   422
paulson@21710
   423
paulson@21710
   424
subsection{*o-simprules for @{term sysOfAlloc} [MUST BE AUTOMATED]*}
wenzelm@21632
   425
wenzelm@21632
   426
lemma client_o_sysOfAlloc: "client o sysOfAlloc = fst o allocState_d.dummy "
wenzelm@24147
   427
  apply record_auto
wenzelm@21632
   428
  done
wenzelm@21632
   429
wenzelm@21632
   430
ML {* bind_thms ("client_o_sysOfAlloc'", make_o_equivs (thm "client_o_sysOfAlloc")) *}
wenzelm@21632
   431
declare client_o_sysOfAlloc' [simp]
wenzelm@21632
   432
wenzelm@21632
   433
lemma allocGiv_o_sysOfAlloc_eq: "allocGiv o sysOfAlloc = allocGiv"
wenzelm@24147
   434
  apply record_auto
wenzelm@21632
   435
  done
wenzelm@21632
   436
wenzelm@21632
   437
ML {* bind_thms ("allocGiv_o_sysOfAlloc_eq'", make_o_equivs (thm "allocGiv_o_sysOfAlloc_eq")) *}
wenzelm@21632
   438
declare allocGiv_o_sysOfAlloc_eq' [simp]
wenzelm@21632
   439
wenzelm@21632
   440
lemma allocAsk_o_sysOfAlloc_eq: "allocAsk o sysOfAlloc = allocAsk"
wenzelm@24147
   441
  apply record_auto
wenzelm@21632
   442
  done
wenzelm@21632
   443
wenzelm@21632
   444
ML {* bind_thms ("allocAsk_o_sysOfAlloc_eq'", make_o_equivs (thm "allocAsk_o_sysOfAlloc_eq")) *}
wenzelm@21632
   445
declare allocAsk_o_sysOfAlloc_eq' [simp]
wenzelm@21632
   446
wenzelm@21632
   447
lemma allocRel_o_sysOfAlloc_eq: "allocRel o sysOfAlloc = allocRel"
wenzelm@24147
   448
  apply record_auto
wenzelm@21632
   449
  done
wenzelm@21632
   450
wenzelm@21632
   451
ML {* bind_thms ("allocRel_o_sysOfAlloc_eq'", make_o_equivs (thm "allocRel_o_sysOfAlloc_eq")) *}
wenzelm@21632
   452
declare allocRel_o_sysOfAlloc_eq' [simp]
wenzelm@21632
   453
paulson@21710
   454
paulson@21710
   455
subsection{* o-simprules for @{term sysOfClient} [MUST BE AUTOMATED]*}
wenzelm@21632
   456
wenzelm@21632
   457
lemma client_o_sysOfClient: "client o sysOfClient = fst"
wenzelm@24147
   458
  apply record_auto
wenzelm@21632
   459
  done
wenzelm@21632
   460
wenzelm@21632
   461
ML {* bind_thms ("client_o_sysOfClient'", make_o_equivs (thm "client_o_sysOfClient")) *}
wenzelm@21632
   462
declare client_o_sysOfClient' [simp]
wenzelm@21632
   463
wenzelm@21632
   464
lemma allocGiv_o_sysOfClient_eq: "allocGiv o sysOfClient = allocGiv o snd "
wenzelm@24147
   465
  apply record_auto
wenzelm@21632
   466
  done
wenzelm@21632
   467
wenzelm@21632
   468
ML {* bind_thms ("allocGiv_o_sysOfClient_eq'", make_o_equivs (thm "allocGiv_o_sysOfClient_eq")) *}
wenzelm@21632
   469
declare allocGiv_o_sysOfClient_eq' [simp]
wenzelm@21632
   470
wenzelm@21632
   471
lemma allocAsk_o_sysOfClient_eq: "allocAsk o sysOfClient = allocAsk o snd "
wenzelm@24147
   472
  apply record_auto
wenzelm@21632
   473
  done
wenzelm@21632
   474
wenzelm@21632
   475
ML {* bind_thms ("allocAsk_o_sysOfClient_eq'", make_o_equivs (thm "allocAsk_o_sysOfClient_eq")) *}
wenzelm@21632
   476
declare allocAsk_o_sysOfClient_eq' [simp]
wenzelm@21632
   477
wenzelm@21632
   478
lemma allocRel_o_sysOfClient_eq: "allocRel o sysOfClient = allocRel o snd "
wenzelm@24147
   479
  apply record_auto
wenzelm@21632
   480
  done
wenzelm@21632
   481
wenzelm@21632
   482
ML {* bind_thms ("allocRel_o_sysOfClient_eq'", make_o_equivs (thm "allocRel_o_sysOfClient_eq")) *}
wenzelm@21632
   483
declare allocRel_o_sysOfClient_eq' [simp]
wenzelm@21632
   484
wenzelm@21632
   485
lemma allocGiv_o_inv_sysOfAlloc_eq: "allocGiv o inv sysOfAlloc = allocGiv"
wenzelm@21632
   486
  apply (simp add: o_def)
wenzelm@21632
   487
  done
wenzelm@21632
   488
wenzelm@21632
   489
ML {* bind_thms ("allocGiv_o_inv_sysOfAlloc_eq'", make_o_equivs (thm "allocGiv_o_inv_sysOfAlloc_eq")) *}
wenzelm@21632
   490
declare allocGiv_o_inv_sysOfAlloc_eq' [simp]
wenzelm@21632
   491
wenzelm@21632
   492
lemma allocAsk_o_inv_sysOfAlloc_eq: "allocAsk o inv sysOfAlloc = allocAsk"
wenzelm@21632
   493
  apply (simp add: o_def)
wenzelm@21632
   494
  done
wenzelm@21632
   495
wenzelm@21632
   496
ML {* bind_thms ("allocAsk_o_inv_sysOfAlloc_eq'", make_o_equivs (thm "allocAsk_o_inv_sysOfAlloc_eq")) *}
wenzelm@21632
   497
declare allocAsk_o_inv_sysOfAlloc_eq' [simp]
wenzelm@21632
   498
wenzelm@21632
   499
lemma allocRel_o_inv_sysOfAlloc_eq: "allocRel o inv sysOfAlloc = allocRel"
wenzelm@21632
   500
  apply (simp add: o_def)
wenzelm@21632
   501
  done
wenzelm@21632
   502
wenzelm@21632
   503
ML {* bind_thms ("allocRel_o_inv_sysOfAlloc_eq'", make_o_equivs (thm "allocRel_o_inv_sysOfAlloc_eq")) *}
wenzelm@21632
   504
declare allocRel_o_inv_sysOfAlloc_eq' [simp]
wenzelm@21632
   505
wenzelm@24147
   506
lemma rel_inv_client_map_drop_map: "(rel o inv client_map o drop_map i o inv sysOfClient) =
wenzelm@21632
   507
      rel o sub i o client"
wenzelm@21632
   508
  apply (simp add: o_def drop_map_def)
wenzelm@21632
   509
  done
wenzelm@21632
   510
wenzelm@21632
   511
ML {* bind_thms ("rel_inv_client_map_drop_map'", make_o_equivs (thm "rel_inv_client_map_drop_map")) *}
wenzelm@21632
   512
declare rel_inv_client_map_drop_map [simp]
wenzelm@21632
   513
wenzelm@24147
   514
lemma ask_inv_client_map_drop_map: "(ask o inv client_map o drop_map i o inv sysOfClient) =
wenzelm@21632
   515
      ask o sub i o client"
wenzelm@21632
   516
  apply (simp add: o_def drop_map_def)
wenzelm@21632
   517
  done
wenzelm@21632
   518
wenzelm@21632
   519
ML {* bind_thms ("ask_inv_client_map_drop_map'", make_o_equivs (thm "ask_inv_client_map_drop_map")) *}
wenzelm@21632
   520
declare ask_inv_client_map_drop_map [simp]
wenzelm@21632
   521
wenzelm@21632
   522
wenzelm@21632
   523
declare finite_lessThan [iff]
wenzelm@21632
   524
paulson@21710
   525
text{*Client : <unfolded specification> *}
wenzelm@21632
   526
lemmas client_spec_simps =
wenzelm@21632
   527
  client_spec_def client_increasing_def client_bounded_def
wenzelm@21632
   528
  client_progress_def client_allowed_acts_def client_preserves_def
wenzelm@21632
   529
  guarantees_Int_right
wenzelm@21632
   530
wenzelm@21632
   531
ML {*
wenzelm@21632
   532
val [Client_Increasing_ask, Client_Increasing_rel,
wenzelm@24147
   533
     Client_Bounded, Client_Progress, Client_AllowedActs,
wenzelm@21632
   534
     Client_preserves_giv, Client_preserves_dummy] =
wenzelm@24147
   535
        @{thm Client} |> simplify (@{simpset} addsimps @{thms client_spec_simps})
wenzelm@21632
   536
               |> list_of_Int;
wenzelm@21632
   537
wenzelm@21632
   538
bind_thm ("Client_Increasing_ask", Client_Increasing_ask);
wenzelm@21632
   539
bind_thm ("Client_Increasing_rel", Client_Increasing_rel);
wenzelm@21632
   540
bind_thm ("Client_Bounded", Client_Bounded);
wenzelm@21632
   541
bind_thm ("Client_Progress", Client_Progress);
wenzelm@21632
   542
bind_thm ("Client_AllowedActs", Client_AllowedActs);
wenzelm@21632
   543
bind_thm ("Client_preserves_giv", Client_preserves_giv);
wenzelm@21632
   544
bind_thm ("Client_preserves_dummy", Client_preserves_dummy);
wenzelm@21632
   545
*}
wenzelm@21632
   546
wenzelm@21632
   547
declare
wenzelm@21632
   548
  Client_Increasing_ask [iff]
wenzelm@21632
   549
  Client_Increasing_rel [iff]
wenzelm@21632
   550
  Client_Bounded [iff]
wenzelm@21632
   551
  Client_preserves_giv [iff]
wenzelm@21632
   552
  Client_preserves_dummy [iff]
wenzelm@21632
   553
wenzelm@21632
   554
paulson@21710
   555
text{*Network : <unfolded specification> *}
wenzelm@21632
   556
lemmas network_spec_simps =
wenzelm@21632
   557
  network_spec_def network_ask_def network_giv_def
wenzelm@21632
   558
  network_rel_def network_allowed_acts_def network_preserves_def
wenzelm@21632
   559
  ball_conj_distrib
wenzelm@21632
   560
wenzelm@21632
   561
ML {*
wenzelm@21632
   562
val [Network_Ask, Network_Giv, Network_Rel, Network_AllowedActs,
wenzelm@24147
   563
     Network_preserves_allocGiv, Network_preserves_rel,
wenzelm@24147
   564
     Network_preserves_ask]  =
wenzelm@24147
   565
        @{thm Network} |> simplify (@{simpset} addsimps @{thms network_spec_simps})
wenzelm@21632
   566
                |> list_of_Int;
wenzelm@21632
   567
wenzelm@21632
   568
bind_thm ("Network_Ask", Network_Ask);
wenzelm@21632
   569
bind_thm ("Network_Giv", Network_Giv);
wenzelm@21632
   570
bind_thm ("Network_Rel", Network_Rel);
wenzelm@21632
   571
bind_thm ("Network_AllowedActs", Network_AllowedActs);
wenzelm@21632
   572
bind_thm ("Network_preserves_allocGiv", Network_preserves_allocGiv);
wenzelm@21632
   573
bind_thm ("Network_preserves_rel", Network_preserves_rel);
wenzelm@21632
   574
bind_thm ("Network_preserves_ask", Network_preserves_ask);
wenzelm@21632
   575
*}
wenzelm@21632
   576
wenzelm@21632
   577
declare Network_preserves_allocGiv [iff]
wenzelm@21632
   578
wenzelm@21632
   579
declare
wenzelm@21632
   580
  Network_preserves_rel [simp]
wenzelm@21632
   581
  Network_preserves_ask [simp]
wenzelm@21632
   582
wenzelm@21632
   583
declare
wenzelm@21632
   584
  Network_preserves_rel [simplified o_def, simp]
wenzelm@21632
   585
  Network_preserves_ask [simplified o_def, simp]
wenzelm@21632
   586
paulson@21710
   587
text{*Alloc : <unfolded specification> *}
wenzelm@21632
   588
lemmas alloc_spec_simps =
wenzelm@21632
   589
  alloc_spec_def alloc_increasing_def alloc_safety_def
wenzelm@21632
   590
  alloc_progress_def alloc_allowed_acts_def alloc_preserves_def
wenzelm@21632
   591
wenzelm@21632
   592
ML {*
wenzelm@21632
   593
val [Alloc_Increasing_0, Alloc_Safety, Alloc_Progress, Alloc_AllowedActs,
wenzelm@24147
   594
     Alloc_preserves_allocRel, Alloc_preserves_allocAsk,
wenzelm@24147
   595
     Alloc_preserves_dummy] =
wenzelm@24147
   596
        @{thm Alloc} |> simplify (@{simpset} addsimps @{thms alloc_spec_simps})
wenzelm@21632
   597
              |> list_of_Int;
wenzelm@21632
   598
wenzelm@21632
   599
bind_thm ("Alloc_Increasing_0", Alloc_Increasing_0);
wenzelm@21632
   600
bind_thm ("Alloc_Safety", Alloc_Safety);
wenzelm@21632
   601
bind_thm ("Alloc_Progress", Alloc_Progress);
wenzelm@21632
   602
bind_thm ("Alloc_AllowedActs", Alloc_AllowedActs);
wenzelm@21632
   603
bind_thm ("Alloc_preserves_allocRel", Alloc_preserves_allocRel);
wenzelm@21632
   604
bind_thm ("Alloc_preserves_allocAsk", Alloc_preserves_allocAsk);
wenzelm@21632
   605
bind_thm ("Alloc_preserves_dummy", Alloc_preserves_dummy);
wenzelm@21632
   606
*}
wenzelm@21632
   607
paulson@21710
   608
text{*Strip off the INT in the guarantees postcondition*}
wenzelm@24147
   609
wenzelm@24147
   610
lemmas Alloc_Increasing = Alloc_Increasing_0 [normalized]
wenzelm@21632
   611
wenzelm@21632
   612
declare
wenzelm@21632
   613
  Alloc_preserves_allocRel [iff]
wenzelm@21632
   614
  Alloc_preserves_allocAsk [iff]
wenzelm@21632
   615
  Alloc_preserves_dummy [iff]
wenzelm@21632
   616
wenzelm@21632
   617
paulson@21710
   618
subsection{*Components Lemmas [MUST BE AUTOMATED]*}
wenzelm@21632
   619
wenzelm@24147
   620
lemma Network_component_System: "Network Join
wenzelm@24147
   621
      ((rename sysOfClient
wenzelm@24147
   622
        (plam x: (lessThan Nclients). rename client_map Client)) Join
wenzelm@24147
   623
       rename sysOfAlloc Alloc)
wenzelm@21632
   624
      = System"
paulson@21710
   625
  by (simp add: System_def Join_ac)
wenzelm@21632
   626
wenzelm@24147
   627
lemma Client_component_System: "(rename sysOfClient
wenzelm@24147
   628
       (plam x: (lessThan Nclients). rename client_map Client)) Join
wenzelm@21632
   629
      (Network Join rename sysOfAlloc Alloc)  =  System"
paulson@21710
   630
  by (simp add: System_def Join_ac)
wenzelm@21632
   631
wenzelm@24147
   632
lemma Alloc_component_System: "rename sysOfAlloc Alloc Join
wenzelm@24147
   633
       ((rename sysOfClient (plam x: (lessThan Nclients). rename client_map Client)) Join
wenzelm@21632
   634
        Network)  =  System"
paulson@21710
   635
  by (simp add: System_def Join_ac)
wenzelm@21632
   636
wenzelm@21632
   637
declare
wenzelm@21632
   638
  Client_component_System [iff]
wenzelm@21632
   639
  Network_component_System [iff]
wenzelm@21632
   640
  Alloc_component_System [iff]
wenzelm@21632
   641
paulson@21710
   642
paulson@21710
   643
text{** These preservation laws should be generated automatically **}
wenzelm@21632
   644
wenzelm@21632
   645
lemma Client_Allowed [simp]: "Allowed Client = preserves rel Int preserves ask"
paulson@21710
   646
  by (auto simp add: Allowed_def Client_AllowedActs safety_prop_Acts_iff)
wenzelm@21632
   647
wenzelm@24147
   648
lemma Network_Allowed [simp]: "Allowed Network =
wenzelm@24147
   649
        preserves allocRel Int
wenzelm@21632
   650
        (INT i: lessThan Nclients. preserves(giv o sub i o client))"
paulson@21710
   651
  by (auto simp add: Allowed_def Network_AllowedActs safety_prop_Acts_iff)
wenzelm@21632
   652
wenzelm@21632
   653
lemma Alloc_Allowed [simp]: "Allowed Alloc = preserves allocGiv"
paulson@21710
   654
  by (auto simp add: Allowed_def Alloc_AllowedActs safety_prop_Acts_iff)
wenzelm@21632
   655
paulson@21710
   656
text{*needed in @{text rename_client_map_tac}*}
wenzelm@21632
   657
lemma OK_lift_rename_Client [simp]: "OK I (%i. lift i (rename client_map Client))"
wenzelm@21632
   658
  apply (rule OK_lift_I)
wenzelm@21632
   659
  apply auto
wenzelm@21632
   660
  apply (drule_tac w1 = rel in subset_preserves_o [THEN [2] rev_subsetD])
wenzelm@21632
   661
  apply (drule_tac [2] w1 = ask in subset_preserves_o [THEN [2] rev_subsetD])
wenzelm@21632
   662
  apply (auto simp add: o_def split_def)
wenzelm@21632
   663
  done
wenzelm@21632
   664
paulson@21710
   665
lemma fst_lift_map_eq_fst [simp]: "fst (lift_map i x) i = fst x"
paulson@21710
   666
apply (insert fst_o_lift_map [of i])
wenzelm@24147
   667
apply (drule fun_cong [where x=x])
paulson@21710
   668
apply (simp add: o_def);
paulson@21710
   669
done
paulson@21710
   670
paulson@21710
   671
lemma fst_o_lift_map' [simp]:
paulson@21710
   672
     "(f \<circ> sub i \<circ> fst \<circ> lift_map i \<circ> g) = f o fst o g"
wenzelm@24147
   673
apply (subst fst_o_lift_map [symmetric])
wenzelm@24147
   674
apply (simp only: o_assoc)
paulson@21710
   675
done
paulson@21710
   676
wenzelm@21632
   677
wenzelm@21632
   678
(*The proofs of rename_Client_Increasing, rename_Client_Bounded and
wenzelm@21632
   679
  rename_Client_Progress are similar.  All require copying out the original
wenzelm@21632
   680
  Client property.  A forward proof can be constructed as follows:
wenzelm@21632
   681
wenzelm@21632
   682
  Client_Increasing_ask RS
wenzelm@21632
   683
      (bij_client_map RS rename_rename_guarantees_eq RS iffD2)
wenzelm@21632
   684
  RS (lift_lift_guarantees_eq RS iffD2)
wenzelm@21632
   685
  RS guarantees_PLam_I
wenzelm@21632
   686
  RS (bij_sysOfClient RS rename_rename_guarantees_eq RS iffD2)
wenzelm@24147
   687
  |> simplify (simpset() addsimps [lift_image_eq_rename, o_def, split_def,
wenzelm@24147
   688
                                   surj_rename RS surj_range])
wenzelm@21632
   689
wenzelm@21632
   690
However, the "preserves" property remains to be discharged, and the unfolding
wenzelm@21632
   691
of "o" and "sub" complicates subsequent reasoning.
wenzelm@21632
   692
wenzelm@21632
   693
The following tactic works for all three proofs, though it certainly looks
wenzelm@21632
   694
ad-hoc!
wenzelm@21632
   695
*)
wenzelm@21632
   696
ML
wenzelm@21632
   697
{*
wenzelm@24147
   698
fun rename_client_map_tac ss =
wenzelm@21632
   699
  EVERY [
wenzelm@25995
   700
    simp_tac (ss addsimps [@{thm rename_guarantees_eq_rename_inv}]) 1,
wenzelm@24147
   701
    rtac @{thm guarantees_PLam_I} 1,
wenzelm@21632
   702
    assume_tac 2,
wenzelm@24147
   703
         (*preserves: routine reasoning*)
wenzelm@24147
   704
    asm_simp_tac (ss addsimps [@{thm lift_preserves_sub}]) 2,
wenzelm@24147
   705
         (*the guarantee for  "lift i (rename client_map Client)" *)
wenzelm@21632
   706
    asm_simp_tac
wenzelm@24147
   707
        (ss addsimps [@{thm lift_guarantees_eq_lift_inv},
wenzelm@24147
   708
                      @{thm rename_guarantees_eq_rename_inv},
wenzelm@24147
   709
                      @{thm bij_imp_bij_inv}, @{thm surj_rename} RS @{thm surj_range},
wenzelm@24147
   710
                      @{thm inv_inv_eq}]) 1,
wenzelm@21632
   711
    asm_simp_tac
wenzelm@24147
   712
        (@{simpset} addsimps [@{thm o_def}, @{thm non_dummy_def}, @{thm guarantees_Int_right}]) 1]
wenzelm@21632
   713
*}
wenzelm@21632
   714
wenzelm@24147
   715
method_setup rename_client_map = {*
wenzelm@24147
   716
  Method.ctxt_args (fn ctxt =>
wenzelm@24147
   717
    Method.SIMPLE_METHOD (rename_client_map_tac (local_simpset_of ctxt)))
wenzelm@24147
   718
*} ""
wenzelm@24147
   719
paulson@21710
   720
text{*Lifting @{text Client_Increasing} to @{term systemState}*}
wenzelm@24147
   721
lemma rename_Client_Increasing: "i : I
wenzelm@24147
   722
      ==> rename sysOfClient (plam x: I. rename client_map Client) :
wenzelm@24147
   723
            UNIV  guarantees
wenzelm@24147
   724
            Increasing (ask o sub i o client) Int
wenzelm@21632
   725
            Increasing (rel o sub i o client)"
wenzelm@24147
   726
  by rename_client_map
wenzelm@21632
   727
wenzelm@24147
   728
lemma preserves_sub_fst_lift_map: "[| F : preserves w; i ~= j |]
wenzelm@21632
   729
      ==> F : preserves (sub i o fst o lift_map j o funPair v w)"
wenzelm@21632
   730
  apply (auto simp add: lift_map_def split_def linorder_neq_iff o_def)
wenzelm@21632
   731
  apply (drule_tac [!] subset_preserves_o [THEN [2] rev_subsetD])
wenzelm@21632
   732
  apply (auto simp add: o_def)
wenzelm@21632
   733
  done
wenzelm@21632
   734
wenzelm@24147
   735
lemma client_preserves_giv_oo_client_map: "[| i < Nclients; j < Nclients |]
wenzelm@21632
   736
      ==> Client : preserves (giv o sub i o fst o lift_map j o client_map)"
wenzelm@24147
   737
  apply (case_tac "i=j")
paulson@21710
   738
  apply (simp, simp add: o_def non_dummy_def)
wenzelm@21632
   739
  apply (drule Client_preserves_dummy [THEN preserves_sub_fst_lift_map])
wenzelm@21632
   740
  apply (drule_tac [!] subset_preserves_o [THEN [2] rev_subsetD])
wenzelm@21632
   741
  apply (simp add: o_def client_map_def)
wenzelm@21632
   742
  done
wenzelm@21632
   743
wenzelm@21632
   744
lemma rename_sysOfClient_ok_Network:
wenzelm@24147
   745
  "rename sysOfClient (plam x: lessThan Nclients. rename client_map Client)
wenzelm@21632
   746
    ok Network"
paulson@21710
   747
  by (auto simp add: ok_iff_Allowed client_preserves_giv_oo_client_map)
wenzelm@21632
   748
wenzelm@21632
   749
lemma rename_sysOfClient_ok_Alloc:
wenzelm@24147
   750
  "rename sysOfClient (plam x: lessThan Nclients. rename client_map Client)
wenzelm@21632
   751
    ok rename sysOfAlloc Alloc"
paulson@21710
   752
  by (simp add: ok_iff_Allowed)
wenzelm@21632
   753
wenzelm@21632
   754
lemma rename_sysOfAlloc_ok_Network: "rename sysOfAlloc Alloc ok Network"
paulson@21710
   755
  by (simp add: ok_iff_Allowed)
wenzelm@21632
   756
wenzelm@21632
   757
declare
wenzelm@21632
   758
  rename_sysOfClient_ok_Network [iff]
wenzelm@21632
   759
  rename_sysOfClient_ok_Alloc [iff]
wenzelm@21632
   760
  rename_sysOfAlloc_ok_Network [iff]
wenzelm@21632
   761
wenzelm@24147
   762
text{*The "ok" laws, re-oriented.
paulson@21710
   763
  But not sure this works: theorem @{text ok_commute} is needed below*}
wenzelm@21632
   764
declare
wenzelm@21632
   765
  rename_sysOfClient_ok_Network [THEN ok_sym, iff]
wenzelm@21632
   766
  rename_sysOfClient_ok_Alloc [THEN ok_sym, iff]
wenzelm@21632
   767
  rename_sysOfAlloc_ok_Network [THEN ok_sym]
wenzelm@21632
   768
wenzelm@21632
   769
lemma System_Increasing: "i < Nclients
wenzelm@24147
   770
      ==> System : Increasing (ask o sub i o client) Int
wenzelm@21632
   771
                   Increasing (rel o sub i o client)"
wenzelm@21632
   772
  apply (rule component_guaranteesD [OF rename_Client_Increasing Client_component_System])
wenzelm@21632
   773
  apply auto
wenzelm@21632
   774
  done
wenzelm@21632
   775
wenzelm@21632
   776
lemmas rename_guarantees_sysOfAlloc_I =
wenzelm@21632
   777
  bij_sysOfAlloc [THEN rename_rename_guarantees_eq, THEN iffD2, standard]
wenzelm@21632
   778
wenzelm@21632
   779
wenzelm@21632
   780
(*Lifting Alloc_Increasing up to the level of systemState*)
paulson@21710
   781
lemmas rename_Alloc_Increasing =
paulson@21710
   782
  Alloc_Increasing
wenzelm@24147
   783
    [THEN rename_guarantees_sysOfAlloc_I,
wenzelm@24147
   784
     simplified surj_rename [THEN surj_range] o_def sub_apply
wenzelm@24147
   785
                rename_image_Increasing bij_sysOfAlloc
paulson@21710
   786
                allocGiv_o_inv_sysOfAlloc_eq'];
wenzelm@21632
   787
wenzelm@24147
   788
lemma System_Increasing_allocGiv:
wenzelm@21632
   789
     "i < Nclients ==> System : Increasing (sub i o allocGiv)"
wenzelm@21632
   790
  apply (unfold System_def)
wenzelm@21632
   791
  apply (simp add: o_def)
wenzelm@21632
   792
  apply (rule rename_Alloc_Increasing [THEN guarantees_Join_I1, THEN guaranteesD])
wenzelm@21632
   793
  apply auto
wenzelm@21632
   794
  done
paulson@21710
   795
wenzelm@21632
   796
wenzelm@21632
   797
ML {*
wenzelm@21632
   798
bind_thms ("System_Increasing'", list_of_Int (thm "System_Increasing"))
wenzelm@21632
   799
*}
wenzelm@21632
   800
wenzelm@21632
   801
declare System_Increasing' [intro!]
wenzelm@21632
   802
paulson@21710
   803
text{* Follows consequences.
wenzelm@21632
   804
    The "Always (INT ...) formulation expresses the general safety property
paulson@21710
   805
    and allows it to be combined using @{text Always_Int_rule} below. *}
wenzelm@21632
   806
wenzelm@24147
   807
lemma System_Follows_rel:
wenzelm@21632
   808
  "i < Nclients ==> System : ((sub i o allocRel) Fols (rel o sub i o client))"
wenzelm@21632
   809
  apply (auto intro!: Network_Rel [THEN component_guaranteesD])
wenzelm@24147
   810
  apply (simp add: ok_commute [of Network])
paulson@21710
   811
  done
wenzelm@21632
   812
wenzelm@24147
   813
lemma System_Follows_ask:
wenzelm@21632
   814
  "i < Nclients ==> System : ((sub i o allocAsk) Fols (ask o sub i o client))"
paulson@21710
   815
  apply (auto intro!: Network_Ask [THEN component_guaranteesD])
wenzelm@24147
   816
  apply (simp add: ok_commute [of Network])
wenzelm@21632
   817
  done
wenzelm@21632
   818
wenzelm@24147
   819
lemma System_Follows_allocGiv:
wenzelm@21632
   820
  "i < Nclients ==> System : (giv o sub i o client) Fols (sub i o allocGiv)"
wenzelm@21632
   821
  apply (auto intro!: Network_Giv [THEN component_guaranteesD]
wenzelm@21632
   822
    rename_Alloc_Increasing [THEN component_guaranteesD])
paulson@21710
   823
  apply (simp_all add: o_def non_dummy_def ok_commute [of Network])
wenzelm@21632
   824
  apply (auto intro!: rename_Alloc_Increasing [THEN component_guaranteesD])
wenzelm@21632
   825
  done
paulson@21710
   826
wenzelm@21632
   827
wenzelm@24147
   828
lemma Always_giv_le_allocGiv: "System : Always (INT i: lessThan Nclients.
paulson@21710
   829
                       {s. (giv o sub i o client) s \<le> (sub i o allocGiv) s})"
wenzelm@21632
   830
  apply auto
wenzelm@21632
   831
  apply (erule System_Follows_allocGiv [THEN Follows_Bounded])
wenzelm@21632
   832
  done
paulson@21710
   833
wenzelm@21632
   834
wenzelm@24147
   835
lemma Always_allocAsk_le_ask: "System : Always (INT i: lessThan Nclients.
paulson@21710
   836
                       {s. (sub i o allocAsk) s \<le> (ask o sub i o client) s})"
wenzelm@21632
   837
  apply auto
wenzelm@21632
   838
  apply (erule System_Follows_ask [THEN Follows_Bounded])
wenzelm@21632
   839
  done
paulson@21710
   840
wenzelm@21632
   841
wenzelm@24147
   842
lemma Always_allocRel_le_rel: "System : Always (INT i: lessThan Nclients.
paulson@21710
   843
                       {s. (sub i o allocRel) s \<le> (rel o sub i o client) s})"
paulson@21710
   844
  by (auto intro!: Follows_Bounded System_Follows_rel)
paulson@21710
   845
wenzelm@21632
   846
paulson@21710
   847
subsection{*Proof of the safety property (1)*}
wenzelm@21632
   848
paulson@21710
   849
text{*safety (1), step 1 is @{text System_Follows_rel}*}
wenzelm@21632
   850
paulson@21710
   851
text{*safety (1), step 2*}
wenzelm@21632
   852
(* i < Nclients ==> System : Increasing (sub i o allocRel) *)
wenzelm@21632
   853
lemmas System_Increasing_allocRel = System_Follows_rel [THEN Follows_Increasing1, standard]
wenzelm@21632
   854
wenzelm@21632
   855
(*Lifting Alloc_safety up to the level of systemState.
paulson@21710
   856
  Simplifying with o_def gets rid of the translations but it unfortunately
wenzelm@21632
   857
  gets rid of the other "o"s too.*)
wenzelm@21632
   858
paulson@21710
   859
text{*safety (1), step 3*}
wenzelm@24147
   860
lemma System_sum_bounded:
paulson@21710
   861
    "System : Always {s. (\<Sum>i \<in> lessThan Nclients. (tokens o sub i o allocGiv) s)
paulson@21710
   862
            \<le> NbT + (\<Sum>i \<in> lessThan Nclients. (tokens o sub i o allocRel) s)}"
wenzelm@21632
   863
  apply (simp add: o_apply)
wenzelm@24147
   864
  apply (insert Alloc_Safety [THEN rename_guarantees_sysOfAlloc_I])
wenzelm@24147
   865
  apply (simp add: o_def);
wenzelm@24147
   866
  apply (erule component_guaranteesD)
paulson@21710
   867
  apply (auto simp add: System_Increasing_allocRel [simplified sub_apply o_def])
wenzelm@21632
   868
  done
wenzelm@21632
   869
paulson@21710
   870
text{* Follows reasoning*}
wenzelm@21632
   871
wenzelm@24147
   872
lemma Always_tokens_giv_le_allocGiv: "System : Always (INT i: lessThan Nclients.
wenzelm@24147
   873
                          {s. (tokens o giv o sub i o client) s
paulson@21710
   874
                           \<le> (tokens o sub i o allocGiv) s})"
wenzelm@21632
   875
  apply (rule Always_giv_le_allocGiv [THEN Always_weaken])
wenzelm@21632
   876
  apply (auto intro: tokens_mono_prefix simp add: o_apply)
wenzelm@21632
   877
  done
wenzelm@21632
   878
wenzelm@24147
   879
lemma Always_tokens_allocRel_le_rel: "System : Always (INT i: lessThan Nclients.
wenzelm@24147
   880
                          {s. (tokens o sub i o allocRel) s
paulson@21710
   881
                           \<le> (tokens o rel o sub i o client) s})"
wenzelm@21632
   882
  apply (rule Always_allocRel_le_rel [THEN Always_weaken])
wenzelm@21632
   883
  apply (auto intro: tokens_mono_prefix simp add: o_apply)
wenzelm@21632
   884
  done
wenzelm@21632
   885
paulson@21710
   886
text{*safety (1), step 4 (final result!) *}
paulson@21710
   887
theorem System_safety: "System : system_safety"
wenzelm@21632
   888
  apply (unfold system_safety_def)
wenzelm@21632
   889
  apply (tactic {* rtac (Always_Int_rule [thm "System_sum_bounded",
wenzelm@21632
   890
    thm "Always_tokens_giv_le_allocGiv", thm "Always_tokens_allocRel_le_rel"] RS
wenzelm@21632
   891
    thm "Always_weaken") 1 *})
wenzelm@21632
   892
  apply auto
wenzelm@21632
   893
  apply (rule setsum_fun_mono [THEN order_trans])
wenzelm@21632
   894
  apply (drule_tac [2] order_trans)
wenzelm@21632
   895
  apply (rule_tac [2] add_le_mono [OF order_refl setsum_fun_mono])
wenzelm@21632
   896
  prefer 3 apply assumption
wenzelm@21632
   897
  apply auto
wenzelm@21632
   898
  done
wenzelm@21632
   899
paulson@21710
   900
subsection {* Proof of the progress property (2) *}
wenzelm@21632
   901
paulson@21710
   902
text{*progress (2), step 1 is @{text System_Follows_ask} and
paulson@21710
   903
      @{text System_Follows_rel}*}
wenzelm@21632
   904
paulson@21710
   905
text{*progress (2), step 2; see also @{text System_Increasing_allocRel}*}
wenzelm@21632
   906
(* i < Nclients ==> System : Increasing (sub i o allocAsk) *)
wenzelm@21632
   907
lemmas System_Increasing_allocAsk =  System_Follows_ask [THEN Follows_Increasing1, standard]
wenzelm@21632
   908
paulson@21710
   909
text{*progress (2), step 3: lifting @{text Client_Bounded} to systemState*}
wenzelm@24147
   910
lemma rename_Client_Bounded: "i : I
wenzelm@24147
   911
    ==> rename sysOfClient (plam x: I. rename client_map Client) :
wenzelm@24147
   912
          UNIV  guarantees
paulson@21710
   913
          Always {s. ALL elt : set ((ask o sub i o client) s). elt \<le> NbT}"
wenzelm@24147
   914
  by rename_client_map
paulson@21710
   915
wenzelm@21632
   916
wenzelm@24147
   917
lemma System_Bounded_ask: "i < Nclients
wenzelm@24147
   918
      ==> System : Always
paulson@21710
   919
                    {s. ALL elt : set ((ask o sub i o client) s). elt \<le> NbT}"
wenzelm@21632
   920
  apply (rule component_guaranteesD [OF rename_Client_Bounded Client_component_System])
wenzelm@21632
   921
  apply auto
wenzelm@21632
   922
  done
wenzelm@21632
   923
wenzelm@21632
   924
lemma Collect_all_imp_eq: "{x. ALL y. P y --> Q x y} = (INT y: {y. P y}. {x. Q x y})"
wenzelm@21632
   925
  apply blast
wenzelm@21632
   926
  done
wenzelm@21632
   927
paulson@21710
   928
text{*progress (2), step 4*}
wenzelm@24147
   929
lemma System_Bounded_allocAsk: "System : Always {s. ALL i<Nclients.
paulson@21710
   930
                          ALL elt : set ((sub i o allocAsk) s). elt \<le> NbT}"
wenzelm@21632
   931
  apply (auto simp add: Collect_all_imp_eq)
wenzelm@21632
   932
  apply (tactic {* rtac (Always_Int_rule [thm "Always_allocAsk_le_ask",
wenzelm@21632
   933
    thm "System_Bounded_ask"] RS thm "Always_weaken") 1 *})
wenzelm@21632
   934
  apply (auto dest: set_mono)
wenzelm@21632
   935
  done
wenzelm@21632
   936
paulson@21710
   937
text{*progress (2), step 5 is @{text System_Increasing_allocGiv}*}
wenzelm@21632
   938
paulson@21710
   939
text{*progress (2), step 6*}
wenzelm@21632
   940
(* i < Nclients ==> System : Increasing (giv o sub i o client) *)
wenzelm@21632
   941
lemmas System_Increasing_giv =  System_Follows_allocGiv [THEN Follows_Increasing1, standard]
wenzelm@21632
   942
wenzelm@21632
   943
wenzelm@24147
   944
lemma rename_Client_Progress: "i: I
wenzelm@24147
   945
   ==> rename sysOfClient (plam x: I. rename client_map Client)
wenzelm@24147
   946
        : Increasing (giv o sub i o client)
wenzelm@24147
   947
          guarantees
wenzelm@24147
   948
          (INT h. {s. h \<le> (giv o sub i o client) s &
wenzelm@24147
   949
                            h pfixGe (ask o sub i o client) s}
paulson@21710
   950
                  LeadsTo {s. tokens h \<le> (tokens o rel o sub i o client) s})"
wenzelm@24147
   951
  apply rename_client_map
wenzelm@21632
   952
  apply (simp add: Client_Progress [simplified o_def])
wenzelm@21632
   953
  done
wenzelm@21632
   954
wenzelm@21632
   955
paulson@21710
   956
text{*progress (2), step 7*}
wenzelm@24147
   957
lemma System_Client_Progress:
wenzelm@24147
   958
  "System : (INT i : (lessThan Nclients).
wenzelm@24147
   959
            INT h. {s. h \<le> (giv o sub i o client) s &
wenzelm@24147
   960
                       h pfixGe (ask o sub i o client) s}
paulson@21710
   961
                LeadsTo {s. tokens h \<le> (tokens o rel o sub i o client) s})"
wenzelm@21632
   962
  apply (rule INT_I)
wenzelm@21632
   963
(*Couldn't have just used Auto_tac since the "INT h" must be kept*)
wenzelm@21632
   964
  apply (rule component_guaranteesD [OF rename_Client_Progress Client_component_System])
wenzelm@21632
   965
  apply (auto simp add: System_Increasing_giv)
wenzelm@21632
   966
  done
wenzelm@21632
   967
wenzelm@21632
   968
(*Concludes
wenzelm@24147
   969
 System : {s. k \<le> (sub i o allocGiv) s}
wenzelm@21632
   970
          LeadsTo
paulson@21710
   971
          {s. (sub i o allocAsk) s \<le> (ask o sub i o client) s} Int
paulson@21710
   972
          {s. k \<le> (giv o sub i o client) s} *)
wenzelm@21632
   973
paulson@21710
   974
lemmas System_lemma1 =
paulson@21710
   975
  Always_LeadsToD [OF System_Follows_ask [THEN Follows_Bounded]
paulson@21710
   976
                      System_Follows_allocGiv [THEN Follows_LeadsTo]]
wenzelm@21632
   977
paulson@21710
   978
lemmas System_lemma2 =
paulson@21710
   979
  PSP_Stable [OF System_lemma1
wenzelm@24147
   980
              System_Follows_ask [THEN Follows_Increasing1, THEN IncreasingD]]
paulson@21710
   981
paulson@21710
   982
wenzelm@24147
   983
lemma System_lemma3: "i < Nclients
wenzelm@24147
   984
      ==> System : {s. h \<le> (sub i o allocGiv) s &
wenzelm@24147
   985
                       h pfixGe (sub i o allocAsk) s}
wenzelm@24147
   986
                   LeadsTo
wenzelm@24147
   987
                   {s. h \<le> (giv o sub i o client) s &
wenzelm@21632
   988
                       h pfixGe (ask o sub i o client) s}"
wenzelm@21632
   989
  apply (rule single_LeadsTo_I)
wenzelm@24147
   990
  apply (rule_tac k6 = "h" and x2 = " (sub i o allocAsk) s"
paulson@21710
   991
         in System_lemma2 [THEN LeadsTo_weaken])
wenzelm@21632
   992
  apply auto
paulson@21710
   993
  apply (blast intro: trans_Ge [THEN trans_genPrefix, THEN transD] prefix_imp_pfixGe)
wenzelm@21632
   994
  done
wenzelm@21632
   995
wenzelm@21632
   996
paulson@21710
   997
text{*progress (2), step 8: Client i's "release" action is visible system-wide*}
wenzelm@24147
   998
lemma System_Alloc_Client_Progress: "i < Nclients
wenzelm@24147
   999
      ==> System : {s. h \<le> (sub i o allocGiv) s &
wenzelm@24147
  1000
                       h pfixGe (sub i o allocAsk) s}
paulson@21710
  1001
                   LeadsTo {s. tokens h \<le> (tokens o sub i o allocRel) s}"
wenzelm@21632
  1002
  apply (rule LeadsTo_Trans)
wenzelm@21632
  1003
   prefer 2
wenzelm@21632
  1004
   apply (drule System_Follows_rel [THEN
wenzelm@21632
  1005
     mono_tokens [THEN mono_Follows_o, THEN [2] rev_subsetD],
wenzelm@21632
  1006
     THEN Follows_LeadsTo])
wenzelm@21632
  1007
   apply (simp add: o_assoc)
wenzelm@21632
  1008
  apply (rule LeadsTo_Trans)
wenzelm@21632
  1009
   apply (cut_tac [2] System_Client_Progress)
wenzelm@21632
  1010
   prefer 2
wenzelm@21632
  1011
   apply (blast intro: LeadsTo_Basis)
paulson@21710
  1012
  apply (erule System_lemma3)
wenzelm@21632
  1013
  done
wenzelm@21632
  1014
paulson@21710
  1015
text{*Lifting @{text Alloc_Progress} up to the level of systemState*}
wenzelm@21632
  1016
paulson@21710
  1017
text{*progress (2), step 9*}
wenzelm@24147
  1018
lemma System_Alloc_Progress:
wenzelm@24147
  1019
 "System : (INT i : (lessThan Nclients).
wenzelm@24147
  1020
            INT h. {s. h \<le> (sub i o allocAsk) s}
wenzelm@21632
  1021
                   LeadsTo {s. h pfixLe (sub i o allocGiv) s})"
wenzelm@21632
  1022
  apply (simp only: o_apply sub_def)
wenzelm@24147
  1023
  apply (insert Alloc_Progress [THEN rename_guarantees_sysOfAlloc_I])
wenzelm@24147
  1024
  apply (simp add: o_def del: Set.INT_iff);
paulson@21710
  1025
  apply (erule component_guaranteesD)
wenzelm@24147
  1026
  apply (auto simp add:
paulson@21710
  1027
    System_Increasing_allocRel [simplified sub_apply o_def]
paulson@21710
  1028
    System_Increasing_allocAsk [simplified sub_apply o_def]
paulson@21710
  1029
    System_Bounded_allocAsk [simplified sub_apply o_def]
paulson@21710
  1030
    System_Alloc_Client_Progress [simplified sub_apply o_def])
wenzelm@21632
  1031
  done
wenzelm@21632
  1032
paulson@21710
  1033
text{*progress (2), step 10 (final result!) *}
wenzelm@21632
  1034
lemma System_Progress: "System : system_progress"
wenzelm@21632
  1035
  apply (unfold system_progress_def)
wenzelm@21632
  1036
  apply (cut_tac System_Alloc_Progress)
wenzelm@21632
  1037
  apply (blast intro: LeadsTo_Trans
wenzelm@21632
  1038
    System_Follows_allocGiv [THEN Follows_LeadsTo_pfixLe]
wenzelm@21632
  1039
    System_Follows_ask [THEN Follows_LeadsTo])
wenzelm@21632
  1040
  done
wenzelm@21632
  1041
wenzelm@21632
  1042
paulson@21710
  1043
theorem System_correct: "System : system_spec"
wenzelm@21632
  1044
  apply (unfold system_spec_def)
wenzelm@21632
  1045
  apply (blast intro: System_safety System_Progress)
wenzelm@21632
  1046
  done
wenzelm@21632
  1047
wenzelm@21632
  1048
paulson@21710
  1049
text{* Some obsolete lemmas *}
wenzelm@21632
  1050
wenzelm@24147
  1051
lemma non_dummy_eq_o_funPair: "non_dummy = (% (g,a,r). (| giv = g, ask = a, rel = r |)) o
wenzelm@21632
  1052
                              (funPair giv (funPair ask rel))"
wenzelm@21632
  1053
  apply (rule ext)
wenzelm@21632
  1054
  apply (auto simp add: o_def non_dummy_def)
wenzelm@21632
  1055
  done
wenzelm@21632
  1056
wenzelm@24147
  1057
lemma preserves_non_dummy_eq: "(preserves non_dummy) =
wenzelm@21632
  1058
      (preserves rel Int preserves ask Int preserves giv)"
wenzelm@21632
  1059
  apply (simp add: non_dummy_eq_o_funPair)
wenzelm@21632
  1060
  apply auto
wenzelm@21632
  1061
    apply (drule_tac w1 = rel in subset_preserves_o [THEN [2] rev_subsetD])
wenzelm@21632
  1062
    apply (drule_tac [2] w1 = ask in subset_preserves_o [THEN [2] rev_subsetD])
wenzelm@21632
  1063
    apply (drule_tac [3] w1 = giv in subset_preserves_o [THEN [2] rev_subsetD])
wenzelm@21632
  1064
    apply (auto simp add: o_def)
wenzelm@21632
  1065
  done
wenzelm@21632
  1066
paulson@21710
  1067
text{*Could go to Extend.ML*}
wenzelm@21632
  1068
lemma bij_fst_inv_inv_eq: "bij f ==> fst (inv (%(x, u). inv f x) z) = f z"
wenzelm@21632
  1069
  apply (rule fst_inv_equalityI)
wenzelm@21632
  1070
   apply (rule_tac f = "%z. (f z, ?h z) " in surjI)
wenzelm@21632
  1071
   apply (simp add: bij_is_inj inv_f_f)
wenzelm@21632
  1072
  apply (simp add: bij_is_surj surj_f_inv_f)
wenzelm@21632
  1073
  done
paulson@11194
  1074
paulson@11194
  1075
end