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