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