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