src/HOL/UNITY/Comp/Alloc.thy
author wenzelm
Mon Sep 06 19:13:10 2010 +0200 (2010-09-06)
changeset 39159 0dec18004e75
parent 38012 3ca193a6ae5a
child 39198 f967a16dfcdd
permissions -rw-r--r--
more antiquotations;
     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 Join Network Join
   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                  Join
   272                  Network
   273                  Join
   274                  (rename sysOfClient
   275                   (plam x: lessThan Nclients. rename client_map Client))"
   276 **)
   277 
   278 (*Perhaps equalities.ML shouldn't add this in the first place!*)
   279 declare image_Collect [simp del]
   280 
   281 declare subset_preserves_o [THEN [2] rev_subsetD, intro]
   282 declare subset_preserves_o [THEN [2] rev_subsetD, simp]
   283 declare funPair_o_distrib [simp]
   284 declare Always_INT_distrib [simp]
   285 declare o_apply [simp del]
   286 
   287 (*For rewriting of specifications related by "guarantees"*)
   288 lemmas [simp] =
   289   rename_image_constrains
   290   rename_image_stable
   291   rename_image_increasing
   292   rename_image_invariant
   293   rename_image_Constrains
   294   rename_image_Stable
   295   rename_image_Increasing
   296   rename_image_Always
   297   rename_image_leadsTo
   298   rename_image_LeadsTo
   299   rename_preserves
   300   rename_image_preserves
   301   lift_image_preserves
   302   bij_image_INT
   303   bij_is_inj [THEN image_Int]
   304   bij_image_Collect_eq
   305 
   306 ML {*
   307 (*Splits up conjunctions & intersections: like CONJUNCTS in the HOL system*)
   308 fun list_of_Int th =
   309     (list_of_Int (th RS conjunct1) @ list_of_Int (th RS conjunct2))
   310     handle THM _ => (list_of_Int (th RS IntD1) @ list_of_Int (th RS IntD2))
   311     handle THM _ => (list_of_Int (th RS @{thm INT_D}))
   312     handle THM _ => (list_of_Int (th RS bspec))
   313     handle THM _ => [th];
   314 *}
   315 
   316 lemmas lessThanBspec = lessThan_iff [THEN iffD2, THEN [2] bspec]
   317 
   318 attribute_setup normalized = {*
   319 let
   320   fun normalized th =
   321     normalized (th RS spec
   322       handle THM _ => th RS @{thm lessThanBspec}
   323       handle THM _ => th RS bspec
   324       handle THM _ => th RS (@{thm guarantees_INT_right_iff} RS iffD1))
   325     handle THM _ => th;
   326 in
   327   Scan.succeed (Thm.rule_attribute (K normalized))
   328 end
   329 *} ""
   330 
   331 (*** bijectivity of sysOfAlloc [MUST BE AUTOMATED] ***)
   332 ML {*
   333 fun record_auto_tac (cs, ss) =
   334   auto_tac (cs addIs [ext] addSWrapper Record.split_wrapper,
   335     ss addsimps [@{thm sysOfAlloc_def}, @{thm sysOfClient_def},
   336       @{thm client_map_def}, @{thm non_dummy_def}, @{thm funPair_def},
   337       @{thm o_apply}, @{thm Let_def}])
   338 *}
   339 
   340 method_setup record_auto = {*
   341   Scan.succeed (fn ctxt => SIMPLE_METHOD (record_auto_tac (clasimpset_of ctxt)))
   342 *} ""
   343 
   344 lemma inj_sysOfAlloc [iff]: "inj sysOfAlloc"
   345   apply (unfold sysOfAlloc_def Let_def)
   346   apply (rule inj_onI)
   347   apply record_auto
   348   done
   349 
   350 text{*We need the inverse; also having it simplifies the proof of surjectivity*}
   351 lemma inv_sysOfAlloc_eq [simp]: "!!s. inv sysOfAlloc s =
   352              (| allocGiv = allocGiv s,
   353                 allocAsk = allocAsk s,
   354                 allocRel = allocRel s,
   355                 allocState_d.dummy = (client s, dummy s) |)"
   356   apply (rule inj_sysOfAlloc [THEN inv_f_eq])
   357   apply record_auto
   358   done
   359 
   360 lemma surj_sysOfAlloc [iff]: "surj sysOfAlloc"
   361   apply (simp add: surj_iff expand_fun_eq o_apply)
   362   apply record_auto
   363   done
   364 
   365 lemma bij_sysOfAlloc [iff]: "bij sysOfAlloc"
   366   apply (blast intro: bijI)
   367   done
   368 
   369 
   370 subsubsection{*bijectivity of @{term sysOfClient}*}
   371 
   372 lemma inj_sysOfClient [iff]: "inj sysOfClient"
   373   apply (unfold sysOfClient_def)
   374   apply (rule inj_onI)
   375   apply record_auto
   376   done
   377 
   378 lemma inv_sysOfClient_eq [simp]: "!!s. inv sysOfClient s =
   379              (client s,
   380               (| allocGiv = allocGiv s,
   381                  allocAsk = allocAsk s,
   382                  allocRel = allocRel s,
   383                  allocState_d.dummy = systemState.dummy s|) )"
   384   apply (rule inj_sysOfClient [THEN inv_f_eq])
   385   apply record_auto
   386   done
   387 
   388 lemma surj_sysOfClient [iff]: "surj sysOfClient"
   389   apply (simp add: surj_iff expand_fun_eq o_apply)
   390   apply record_auto
   391   done
   392 
   393 lemma bij_sysOfClient [iff]: "bij sysOfClient"
   394   apply (blast intro: bijI)
   395   done
   396 
   397 
   398 subsubsection{*bijectivity of @{term client_map}*}
   399 
   400 lemma inj_client_map [iff]: "inj client_map"
   401   apply (unfold inj_on_def)
   402   apply record_auto
   403   done
   404 
   405 lemma inv_client_map_eq [simp]: "!!s. inv client_map s =
   406              (%(x,y).(|giv = giv x, ask = ask x, rel = rel x,
   407                        clientState_d.dummy = y|)) s"
   408   apply (rule inj_client_map [THEN inv_f_eq])
   409   apply record_auto
   410   done
   411 
   412 lemma surj_client_map [iff]: "surj client_map"
   413   apply (simp add: surj_iff expand_fun_eq o_apply)
   414   apply record_auto
   415   done
   416 
   417 lemma bij_client_map [iff]: "bij client_map"
   418   apply (blast intro: bijI)
   419   done
   420 
   421 
   422 text{*o-simprules for @{term client_map}*}
   423 
   424 lemma fst_o_client_map: "fst o client_map = non_dummy"
   425   apply (unfold client_map_def)
   426   apply (rule fst_o_funPair)
   427   done
   428 
   429 ML {* bind_thms ("fst_o_client_map'", make_o_equivs @{thm fst_o_client_map}) *}
   430 declare fst_o_client_map' [simp]
   431 
   432 lemma snd_o_client_map: "snd o client_map = clientState_d.dummy"
   433   apply (unfold client_map_def)
   434   apply (rule snd_o_funPair)
   435   done
   436 
   437 ML {* bind_thms ("snd_o_client_map'", make_o_equivs @{thm snd_o_client_map}) *}
   438 declare snd_o_client_map' [simp]
   439 
   440 
   441 subsection{*o-simprules for @{term sysOfAlloc} [MUST BE AUTOMATED]*}
   442 
   443 lemma client_o_sysOfAlloc: "client o sysOfAlloc = fst o allocState_d.dummy "
   444   apply record_auto
   445   done
   446 
   447 ML {* bind_thms ("client_o_sysOfAlloc'", make_o_equivs @{thm client_o_sysOfAlloc}) *}
   448 declare client_o_sysOfAlloc' [simp]
   449 
   450 lemma allocGiv_o_sysOfAlloc_eq: "allocGiv o sysOfAlloc = allocGiv"
   451   apply record_auto
   452   done
   453 
   454 ML {* bind_thms ("allocGiv_o_sysOfAlloc_eq'", make_o_equivs @{thm allocGiv_o_sysOfAlloc_eq}) *}
   455 declare allocGiv_o_sysOfAlloc_eq' [simp]
   456 
   457 lemma allocAsk_o_sysOfAlloc_eq: "allocAsk o sysOfAlloc = allocAsk"
   458   apply record_auto
   459   done
   460 
   461 ML {* bind_thms ("allocAsk_o_sysOfAlloc_eq'", make_o_equivs @{thm allocAsk_o_sysOfAlloc_eq}) *}
   462 declare allocAsk_o_sysOfAlloc_eq' [simp]
   463 
   464 lemma allocRel_o_sysOfAlloc_eq: "allocRel o sysOfAlloc = allocRel"
   465   apply record_auto
   466   done
   467 
   468 ML {* bind_thms ("allocRel_o_sysOfAlloc_eq'", make_o_equivs @{thm allocRel_o_sysOfAlloc_eq}) *}
   469 declare allocRel_o_sysOfAlloc_eq' [simp]
   470 
   471 
   472 subsection{* o-simprules for @{term sysOfClient} [MUST BE AUTOMATED]*}
   473 
   474 lemma client_o_sysOfClient: "client o sysOfClient = fst"
   475   apply record_auto
   476   done
   477 
   478 ML {* bind_thms ("client_o_sysOfClient'", make_o_equivs @{thm client_o_sysOfClient}) *}
   479 declare client_o_sysOfClient' [simp]
   480 
   481 lemma allocGiv_o_sysOfClient_eq: "allocGiv o sysOfClient = allocGiv o snd "
   482   apply record_auto
   483   done
   484 
   485 ML {* bind_thms ("allocGiv_o_sysOfClient_eq'", make_o_equivs @{thm allocGiv_o_sysOfClient_eq}) *}
   486 declare allocGiv_o_sysOfClient_eq' [simp]
   487 
   488 lemma allocAsk_o_sysOfClient_eq: "allocAsk o sysOfClient = allocAsk o snd "
   489   apply record_auto
   490   done
   491 
   492 ML {* bind_thms ("allocAsk_o_sysOfClient_eq'", make_o_equivs @{thm allocAsk_o_sysOfClient_eq}) *}
   493 declare allocAsk_o_sysOfClient_eq' [simp]
   494 
   495 lemma allocRel_o_sysOfClient_eq: "allocRel o sysOfClient = allocRel o snd "
   496   apply record_auto
   497   done
   498 
   499 ML {* bind_thms ("allocRel_o_sysOfClient_eq'", make_o_equivs @{thm allocRel_o_sysOfClient_eq}) *}
   500 declare allocRel_o_sysOfClient_eq' [simp]
   501 
   502 lemma allocGiv_o_inv_sysOfAlloc_eq: "allocGiv o inv sysOfAlloc = allocGiv"
   503   apply (simp add: o_def)
   504   done
   505 
   506 ML {* bind_thms ("allocGiv_o_inv_sysOfAlloc_eq'", make_o_equivs @{thm allocGiv_o_inv_sysOfAlloc_eq}) *}
   507 declare allocGiv_o_inv_sysOfAlloc_eq' [simp]
   508 
   509 lemma allocAsk_o_inv_sysOfAlloc_eq: "allocAsk o inv sysOfAlloc = allocAsk"
   510   apply (simp add: o_def)
   511   done
   512 
   513 ML {* bind_thms ("allocAsk_o_inv_sysOfAlloc_eq'", make_o_equivs @{thm allocAsk_o_inv_sysOfAlloc_eq}) *}
   514 declare allocAsk_o_inv_sysOfAlloc_eq' [simp]
   515 
   516 lemma allocRel_o_inv_sysOfAlloc_eq: "allocRel o inv sysOfAlloc = allocRel"
   517   apply (simp add: o_def)
   518   done
   519 
   520 ML {* bind_thms ("allocRel_o_inv_sysOfAlloc_eq'", make_o_equivs @{thm allocRel_o_inv_sysOfAlloc_eq}) *}
   521 declare allocRel_o_inv_sysOfAlloc_eq' [simp]
   522 
   523 lemma rel_inv_client_map_drop_map: "(rel o inv client_map o drop_map i o inv sysOfClient) =
   524       rel o sub i o client"
   525   apply (simp add: o_def drop_map_def)
   526   done
   527 
   528 ML {* bind_thms ("rel_inv_client_map_drop_map'", make_o_equivs @{thm rel_inv_client_map_drop_map}) *}
   529 declare rel_inv_client_map_drop_map [simp]
   530 
   531 lemma ask_inv_client_map_drop_map: "(ask o inv client_map o drop_map i o inv sysOfClient) =
   532       ask o sub i o client"
   533   apply (simp add: o_def drop_map_def)
   534   done
   535 
   536 ML {* bind_thms ("ask_inv_client_map_drop_map'", make_o_equivs @{thm ask_inv_client_map_drop_map}) *}
   537 declare ask_inv_client_map_drop_map [simp]
   538 
   539 
   540 declare finite_lessThan [iff]
   541 
   542 text{*Client : <unfolded specification> *}
   543 lemmas client_spec_simps =
   544   client_spec_def client_increasing_def client_bounded_def
   545   client_progress_def client_allowed_acts_def client_preserves_def
   546   guarantees_Int_right
   547 
   548 ML {*
   549 val [Client_Increasing_ask, Client_Increasing_rel,
   550      Client_Bounded, Client_Progress, Client_AllowedActs,
   551      Client_preserves_giv, Client_preserves_dummy] =
   552         @{thm Client} |> simplify (@{simpset} addsimps @{thms client_spec_simps})
   553                |> list_of_Int;
   554 
   555 bind_thm ("Client_Increasing_ask", Client_Increasing_ask);
   556 bind_thm ("Client_Increasing_rel", Client_Increasing_rel);
   557 bind_thm ("Client_Bounded", Client_Bounded);
   558 bind_thm ("Client_Progress", Client_Progress);
   559 bind_thm ("Client_AllowedActs", Client_AllowedActs);
   560 bind_thm ("Client_preserves_giv", Client_preserves_giv);
   561 bind_thm ("Client_preserves_dummy", Client_preserves_dummy);
   562 *}
   563 
   564 declare
   565   Client_Increasing_ask [iff]
   566   Client_Increasing_rel [iff]
   567   Client_Bounded [iff]
   568   Client_preserves_giv [iff]
   569   Client_preserves_dummy [iff]
   570 
   571 
   572 text{*Network : <unfolded specification> *}
   573 lemmas network_spec_simps =
   574   network_spec_def network_ask_def network_giv_def
   575   network_rel_def network_allowed_acts_def network_preserves_def
   576   ball_conj_distrib
   577 
   578 ML {*
   579 val [Network_Ask, Network_Giv, Network_Rel, Network_AllowedActs,
   580      Network_preserves_allocGiv, Network_preserves_rel,
   581      Network_preserves_ask]  =
   582         @{thm Network} |> simplify (@{simpset} addsimps @{thms network_spec_simps})
   583                 |> list_of_Int;
   584 
   585 bind_thm ("Network_Ask", Network_Ask);
   586 bind_thm ("Network_Giv", Network_Giv);
   587 bind_thm ("Network_Rel", Network_Rel);
   588 bind_thm ("Network_AllowedActs", Network_AllowedActs);
   589 bind_thm ("Network_preserves_allocGiv", Network_preserves_allocGiv);
   590 bind_thm ("Network_preserves_rel", Network_preserves_rel);
   591 bind_thm ("Network_preserves_ask", Network_preserves_ask);
   592 *}
   593 
   594 declare Network_preserves_allocGiv [iff]
   595 
   596 declare
   597   Network_preserves_rel [simp]
   598   Network_preserves_ask [simp]
   599 
   600 declare
   601   Network_preserves_rel [simplified o_def, simp]
   602   Network_preserves_ask [simplified o_def, simp]
   603 
   604 text{*Alloc : <unfolded specification> *}
   605 lemmas alloc_spec_simps =
   606   alloc_spec_def alloc_increasing_def alloc_safety_def
   607   alloc_progress_def alloc_allowed_acts_def alloc_preserves_def
   608 
   609 ML {*
   610 val [Alloc_Increasing_0, Alloc_Safety, Alloc_Progress, Alloc_AllowedActs,
   611      Alloc_preserves_allocRel, Alloc_preserves_allocAsk,
   612      Alloc_preserves_dummy] =
   613         @{thm Alloc} |> simplify (@{simpset} addsimps @{thms alloc_spec_simps})
   614               |> list_of_Int;
   615 
   616 bind_thm ("Alloc_Increasing_0", Alloc_Increasing_0);
   617 bind_thm ("Alloc_Safety", Alloc_Safety);
   618 bind_thm ("Alloc_Progress", Alloc_Progress);
   619 bind_thm ("Alloc_AllowedActs", Alloc_AllowedActs);
   620 bind_thm ("Alloc_preserves_allocRel", Alloc_preserves_allocRel);
   621 bind_thm ("Alloc_preserves_allocAsk", Alloc_preserves_allocAsk);
   622 bind_thm ("Alloc_preserves_dummy", Alloc_preserves_dummy);
   623 *}
   624 
   625 text{*Strip off the INT in the guarantees postcondition*}
   626 
   627 lemmas Alloc_Increasing = Alloc_Increasing_0 [normalized]
   628 
   629 declare
   630   Alloc_preserves_allocRel [iff]
   631   Alloc_preserves_allocAsk [iff]
   632   Alloc_preserves_dummy [iff]
   633 
   634 
   635 subsection{*Components Lemmas [MUST BE AUTOMATED]*}
   636 
   637 lemma Network_component_System: "Network Join
   638       ((rename sysOfClient
   639         (plam x: (lessThan Nclients). rename client_map Client)) Join
   640        rename sysOfAlloc Alloc)
   641       = System"
   642   by (simp add: System_def Join_ac)
   643 
   644 lemma Client_component_System: "(rename sysOfClient
   645        (plam x: (lessThan Nclients). rename client_map Client)) Join
   646       (Network Join rename sysOfAlloc Alloc)  =  System"
   647   by (simp add: System_def Join_ac)
   648 
   649 lemma Alloc_component_System: "rename sysOfAlloc Alloc Join
   650        ((rename sysOfClient (plam x: (lessThan Nclients). rename client_map Client)) Join
   651         Network)  =  System"
   652   by (simp add: System_def Join_ac)
   653 
   654 declare
   655   Client_component_System [iff]
   656   Network_component_System [iff]
   657   Alloc_component_System [iff]
   658 
   659 
   660 text{** These preservation laws should be generated automatically **}
   661 
   662 lemma Client_Allowed [simp]: "Allowed Client = preserves rel Int preserves ask"
   663   by (auto simp add: Allowed_def Client_AllowedActs safety_prop_Acts_iff)
   664 
   665 lemma Network_Allowed [simp]: "Allowed Network =
   666         preserves allocRel Int
   667         (INT i: lessThan Nclients. preserves(giv o sub i o client))"
   668   by (auto simp add: Allowed_def Network_AllowedActs safety_prop_Acts_iff)
   669 
   670 lemma Alloc_Allowed [simp]: "Allowed Alloc = preserves allocGiv"
   671   by (auto simp add: Allowed_def Alloc_AllowedActs safety_prop_Acts_iff)
   672 
   673 text{*needed in @{text rename_client_map_tac}*}
   674 lemma OK_lift_rename_Client [simp]: "OK I (%i. lift i (rename client_map Client))"
   675   apply (rule OK_lift_I)
   676   apply auto
   677   apply (drule_tac w1 = rel in subset_preserves_o [THEN [2] rev_subsetD])
   678   apply (drule_tac [2] w1 = ask in subset_preserves_o [THEN [2] rev_subsetD])
   679   apply (auto simp add: o_def split_def)
   680   done
   681 
   682 lemma fst_lift_map_eq_fst [simp]: "fst (lift_map i x) i = fst x"
   683 apply (insert fst_o_lift_map [of i])
   684 apply (drule fun_cong [where x=x])
   685 apply (simp add: o_def);
   686 done
   687 
   688 lemma fst_o_lift_map' [simp]:
   689      "(f \<circ> sub i \<circ> fst \<circ> lift_map i \<circ> g) = f o fst o g"
   690 apply (subst fst_o_lift_map [symmetric])
   691 apply (simp only: o_assoc)
   692 done
   693 
   694 
   695 (*The proofs of rename_Client_Increasing, rename_Client_Bounded and
   696   rename_Client_Progress are similar.  All require copying out the original
   697   Client property.  A forward proof can be constructed as follows:
   698 
   699   Client_Increasing_ask RS
   700       (bij_client_map RS rename_rename_guarantees_eq RS iffD2)
   701   RS (lift_lift_guarantees_eq RS iffD2)
   702   RS guarantees_PLam_I
   703   RS (bij_sysOfClient RS rename_rename_guarantees_eq RS iffD2)
   704   |> simplify (simpset() addsimps [lift_image_eq_rename, o_def, split_def,
   705                                    surj_rename RS surj_range])
   706 
   707 However, the "preserves" property remains to be discharged, and the unfolding
   708 of "o" and "sub" complicates subsequent reasoning.
   709 
   710 The following tactic works for all three proofs, though it certainly looks
   711 ad-hoc!
   712 *)
   713 ML
   714 {*
   715 fun rename_client_map_tac ss =
   716   EVERY [
   717     simp_tac (ss addsimps [@{thm rename_guarantees_eq_rename_inv}]) 1,
   718     rtac @{thm guarantees_PLam_I} 1,
   719     assume_tac 2,
   720          (*preserves: routine reasoning*)
   721     asm_simp_tac (ss addsimps [@{thm lift_preserves_sub}]) 2,
   722          (*the guarantee for  "lift i (rename client_map Client)" *)
   723     asm_simp_tac
   724         (ss addsimps [@{thm lift_guarantees_eq_lift_inv},
   725                       @{thm rename_guarantees_eq_rename_inv},
   726                       @{thm bij_imp_bij_inv}, @{thm surj_rename} RS @{thm surj_range},
   727                       @{thm inv_inv_eq}]) 1,
   728     asm_simp_tac
   729         (@{simpset} addsimps [@{thm o_def}, @{thm non_dummy_def}, @{thm guarantees_Int_right}]) 1]
   730 *}
   731 
   732 method_setup rename_client_map = {*
   733   Scan.succeed (fn ctxt =>
   734     SIMPLE_METHOD (rename_client_map_tac (simpset_of ctxt)))
   735 *} ""
   736 
   737 text{*Lifting @{text Client_Increasing} to @{term systemState}*}
   738 lemma rename_Client_Increasing: "i : I
   739       ==> rename sysOfClient (plam x: I. rename client_map Client) :
   740             UNIV  guarantees
   741             Increasing (ask o sub i o client) Int
   742             Increasing (rel o sub i o client)"
   743   by rename_client_map
   744 
   745 lemma preserves_sub_fst_lift_map: "[| F : preserves w; i ~= j |]
   746       ==> F : preserves (sub i o fst o lift_map j o funPair v w)"
   747   apply (auto simp add: lift_map_def split_def linorder_neq_iff o_def)
   748   apply (drule_tac [!] subset_preserves_o [THEN [2] rev_subsetD])
   749   apply (auto simp add: o_def)
   750   done
   751 
   752 lemma client_preserves_giv_oo_client_map: "[| i < Nclients; j < Nclients |]
   753       ==> Client : preserves (giv o sub i o fst o lift_map j o client_map)"
   754   apply (case_tac "i=j")
   755   apply (simp, simp add: o_def non_dummy_def)
   756   apply (drule Client_preserves_dummy [THEN preserves_sub_fst_lift_map])
   757   apply (drule_tac [!] subset_preserves_o [THEN [2] rev_subsetD])
   758   apply (simp add: o_def client_map_def)
   759   done
   760 
   761 lemma rename_sysOfClient_ok_Network:
   762   "rename sysOfClient (plam x: lessThan Nclients. rename client_map Client)
   763     ok Network"
   764   by (auto simp add: ok_iff_Allowed client_preserves_giv_oo_client_map)
   765 
   766 lemma rename_sysOfClient_ok_Alloc:
   767   "rename sysOfClient (plam x: lessThan Nclients. rename client_map Client)
   768     ok rename sysOfAlloc Alloc"
   769   by (simp add: ok_iff_Allowed)
   770 
   771 lemma rename_sysOfAlloc_ok_Network: "rename sysOfAlloc Alloc ok Network"
   772   by (simp add: ok_iff_Allowed)
   773 
   774 declare
   775   rename_sysOfClient_ok_Network [iff]
   776   rename_sysOfClient_ok_Alloc [iff]
   777   rename_sysOfAlloc_ok_Network [iff]
   778 
   779 text{*The "ok" laws, re-oriented.
   780   But not sure this works: theorem @{text ok_commute} is needed below*}
   781 declare
   782   rename_sysOfClient_ok_Network [THEN ok_sym, iff]
   783   rename_sysOfClient_ok_Alloc [THEN ok_sym, iff]
   784   rename_sysOfAlloc_ok_Network [THEN ok_sym]
   785 
   786 lemma System_Increasing: "i < Nclients
   787       ==> System : Increasing (ask o sub i o client) Int
   788                    Increasing (rel o sub i o client)"
   789   apply (rule component_guaranteesD [OF rename_Client_Increasing Client_component_System])
   790   apply auto
   791   done
   792 
   793 lemmas rename_guarantees_sysOfAlloc_I =
   794   bij_sysOfAlloc [THEN rename_rename_guarantees_eq, THEN iffD2, standard]
   795 
   796 
   797 (*Lifting Alloc_Increasing up to the level of systemState*)
   798 lemmas rename_Alloc_Increasing =
   799   Alloc_Increasing
   800     [THEN rename_guarantees_sysOfAlloc_I,
   801      simplified surj_rename [THEN surj_range] o_def sub_apply
   802                 rename_image_Increasing bij_sysOfAlloc
   803                 allocGiv_o_inv_sysOfAlloc_eq'];
   804 
   805 lemma System_Increasing_allocGiv:
   806      "i < Nclients ==> System : Increasing (sub i o allocGiv)"
   807   apply (unfold System_def)
   808   apply (simp add: o_def)
   809   apply (rule rename_Alloc_Increasing [THEN guarantees_Join_I1, THEN guaranteesD])
   810   apply auto
   811   done
   812 
   813 
   814 ML {*
   815 bind_thms ("System_Increasing'", list_of_Int @{thm System_Increasing})
   816 *}
   817 
   818 declare System_Increasing' [intro!]
   819 
   820 text{* Follows consequences.
   821     The "Always (INT ...) formulation expresses the general safety property
   822     and allows it to be combined using @{text Always_Int_rule} below. *}
   823 
   824 lemma System_Follows_rel:
   825   "i < Nclients ==> System : ((sub i o allocRel) Fols (rel o sub i o client))"
   826   apply (auto intro!: Network_Rel [THEN component_guaranteesD])
   827   apply (simp add: ok_commute [of Network])
   828   done
   829 
   830 lemma System_Follows_ask:
   831   "i < Nclients ==> System : ((sub i o allocAsk) Fols (ask o sub i o client))"
   832   apply (auto intro!: Network_Ask [THEN component_guaranteesD])
   833   apply (simp add: ok_commute [of Network])
   834   done
   835 
   836 lemma System_Follows_allocGiv:
   837   "i < Nclients ==> System : (giv o sub i o client) Fols (sub i o allocGiv)"
   838   apply (auto intro!: Network_Giv [THEN component_guaranteesD]
   839     rename_Alloc_Increasing [THEN component_guaranteesD])
   840   apply (simp_all add: o_def non_dummy_def ok_commute [of Network])
   841   apply (auto intro!: rename_Alloc_Increasing [THEN component_guaranteesD])
   842   done
   843 
   844 
   845 lemma Always_giv_le_allocGiv: "System : Always (INT i: lessThan Nclients.
   846                        {s. (giv o sub i o client) s \<le> (sub i o allocGiv) s})"
   847   apply auto
   848   apply (erule System_Follows_allocGiv [THEN Follows_Bounded])
   849   done
   850 
   851 
   852 lemma Always_allocAsk_le_ask: "System : Always (INT i: lessThan Nclients.
   853                        {s. (sub i o allocAsk) s \<le> (ask o sub i o client) s})"
   854   apply auto
   855   apply (erule System_Follows_ask [THEN Follows_Bounded])
   856   done
   857 
   858 
   859 lemma Always_allocRel_le_rel: "System : Always (INT i: lessThan Nclients.
   860                        {s. (sub i o allocRel) s \<le> (rel o sub i o client) s})"
   861   by (auto intro!: Follows_Bounded System_Follows_rel)
   862 
   863 
   864 subsection{*Proof of the safety property (1)*}
   865 
   866 text{*safety (1), step 1 is @{text System_Follows_rel}*}
   867 
   868 text{*safety (1), step 2*}
   869 (* i < Nclients ==> System : Increasing (sub i o allocRel) *)
   870 lemmas System_Increasing_allocRel = System_Follows_rel [THEN Follows_Increasing1, standard]
   871 
   872 (*Lifting Alloc_safety up to the level of systemState.
   873   Simplifying with o_def gets rid of the translations but it unfortunately
   874   gets rid of the other "o"s too.*)
   875 
   876 text{*safety (1), step 3*}
   877 lemma System_sum_bounded:
   878     "System : Always {s. (\<Sum>i \<in> lessThan Nclients. (tokens o sub i o allocGiv) s)
   879             \<le> NbT + (\<Sum>i \<in> lessThan Nclients. (tokens o sub i o allocRel) s)}"
   880   apply (simp add: o_apply)
   881   apply (insert Alloc_Safety [THEN rename_guarantees_sysOfAlloc_I])
   882   apply (simp add: o_def);
   883   apply (erule component_guaranteesD)
   884   apply (auto simp add: System_Increasing_allocRel [simplified sub_apply o_def])
   885   done
   886 
   887 text{* Follows reasoning*}
   888 
   889 lemma Always_tokens_giv_le_allocGiv: "System : Always (INT i: lessThan Nclients.
   890                           {s. (tokens o giv o sub i o client) s
   891                            \<le> (tokens o sub i o allocGiv) s})"
   892   apply (rule Always_giv_le_allocGiv [THEN Always_weaken])
   893   apply (auto intro: tokens_mono_prefix simp add: o_apply)
   894   done
   895 
   896 lemma Always_tokens_allocRel_le_rel: "System : Always (INT i: lessThan Nclients.
   897                           {s. (tokens o sub i o allocRel) s
   898                            \<le> (tokens o rel o sub i o client) s})"
   899   apply (rule Always_allocRel_le_rel [THEN Always_weaken])
   900   apply (auto intro: tokens_mono_prefix simp add: o_apply)
   901   done
   902 
   903 text{*safety (1), step 4 (final result!) *}
   904 theorem System_safety: "System : system_safety"
   905   apply (unfold system_safety_def)
   906   apply (tactic {* rtac (Always_Int_rule [@{thm System_sum_bounded},
   907     @{thm Always_tokens_giv_le_allocGiv}, @{thm Always_tokens_allocRel_le_rel}] RS
   908     @{thm Always_weaken}) 1 *})
   909   apply auto
   910   apply (rule setsum_fun_mono [THEN order_trans])
   911   apply (drule_tac [2] order_trans)
   912   apply (rule_tac [2] add_le_mono [OF order_refl setsum_fun_mono])
   913   prefer 3 apply assumption
   914   apply auto
   915   done
   916 
   917 subsection {* Proof of the progress property (2) *}
   918 
   919 text{*progress (2), step 1 is @{text System_Follows_ask} and
   920       @{text System_Follows_rel}*}
   921 
   922 text{*progress (2), step 2; see also @{text System_Increasing_allocRel}*}
   923 (* i < Nclients ==> System : Increasing (sub i o allocAsk) *)
   924 lemmas System_Increasing_allocAsk =  System_Follows_ask [THEN Follows_Increasing1, standard]
   925 
   926 text{*progress (2), step 3: lifting @{text Client_Bounded} to systemState*}
   927 lemma rename_Client_Bounded: "i : I
   928     ==> rename sysOfClient (plam x: I. rename client_map Client) :
   929           UNIV  guarantees
   930           Always {s. ALL elt : set ((ask o sub i o client) s). elt \<le> NbT}"
   931   by rename_client_map
   932 
   933 
   934 lemma System_Bounded_ask: "i < Nclients
   935       ==> System : Always
   936                     {s. ALL elt : set ((ask o sub i o client) s). elt \<le> NbT}"
   937   apply (rule component_guaranteesD [OF rename_Client_Bounded Client_component_System])
   938   apply auto
   939   done
   940 
   941 lemma Collect_all_imp_eq: "{x. ALL y. P y --> Q x y} = (INT y: {y. P y}. {x. Q x y})"
   942   apply blast
   943   done
   944 
   945 text{*progress (2), step 4*}
   946 lemma System_Bounded_allocAsk: "System : Always {s. ALL i<Nclients.
   947                           ALL elt : set ((sub i o allocAsk) s). elt \<le> NbT}"
   948   apply (auto simp add: Collect_all_imp_eq)
   949   apply (tactic {* rtac (Always_Int_rule [@{thm Always_allocAsk_le_ask},
   950     @{thm System_Bounded_ask}] RS @{thm Always_weaken}) 1 *})
   951   apply (auto dest: set_mono)
   952   done
   953 
   954 text{*progress (2), step 5 is @{text System_Increasing_allocGiv}*}
   955 
   956 text{*progress (2), step 6*}
   957 (* i < Nclients ==> System : Increasing (giv o sub i o client) *)
   958 lemmas System_Increasing_giv =  System_Follows_allocGiv [THEN Follows_Increasing1, standard]
   959 
   960 
   961 lemma rename_Client_Progress: "i: I
   962    ==> rename sysOfClient (plam x: I. rename client_map Client)
   963         : Increasing (giv o sub i o client)
   964           guarantees
   965           (INT h. {s. h \<le> (giv o sub i o client) s &
   966                             h pfixGe (ask o sub i o client) s}
   967                   LeadsTo {s. tokens h \<le> (tokens o rel o sub i o client) s})"
   968   apply rename_client_map
   969   apply (simp add: Client_Progress [simplified o_def])
   970   done
   971 
   972 
   973 text{*progress (2), step 7*}
   974 lemma System_Client_Progress:
   975   "System : (INT i : (lessThan Nclients).
   976             INT h. {s. h \<le> (giv o sub i o client) s &
   977                        h pfixGe (ask o sub i o client) s}
   978                 LeadsTo {s. tokens h \<le> (tokens o rel o sub i o client) s})"
   979   apply (rule INT_I)
   980 (*Couldn't have just used Auto_tac since the "INT h" must be kept*)
   981   apply (rule component_guaranteesD [OF rename_Client_Progress Client_component_System])
   982   apply (auto simp add: System_Increasing_giv)
   983   done
   984 
   985 (*Concludes
   986  System : {s. k \<le> (sub i o allocGiv) s}
   987           LeadsTo
   988           {s. (sub i o allocAsk) s \<le> (ask o sub i o client) s} Int
   989           {s. k \<le> (giv o sub i o client) s} *)
   990 
   991 lemmas System_lemma1 =
   992   Always_LeadsToD [OF System_Follows_ask [THEN Follows_Bounded]
   993                       System_Follows_allocGiv [THEN Follows_LeadsTo]]
   994 
   995 lemmas System_lemma2 =
   996   PSP_Stable [OF System_lemma1
   997               System_Follows_ask [THEN Follows_Increasing1, THEN IncreasingD]]
   998 
   999 
  1000 lemma System_lemma3: "i < Nclients
  1001       ==> System : {s. h \<le> (sub i o allocGiv) s &
  1002                        h pfixGe (sub i o allocAsk) s}
  1003                    LeadsTo
  1004                    {s. h \<le> (giv o sub i o client) s &
  1005                        h pfixGe (ask o sub i o client) s}"
  1006   apply (rule single_LeadsTo_I)
  1007   apply (rule_tac k6 = "h" and x2 = " (sub i o allocAsk) s"
  1008          in System_lemma2 [THEN LeadsTo_weaken])
  1009   apply auto
  1010   apply (blast intro: trans_Ge [THEN trans_genPrefix, THEN transD] prefix_imp_pfixGe)
  1011   done
  1012 
  1013 
  1014 text{*progress (2), step 8: Client i's "release" action is visible system-wide*}
  1015 lemma System_Alloc_Client_Progress: "i < Nclients
  1016       ==> System : {s. h \<le> (sub i o allocGiv) s &
  1017                        h pfixGe (sub i o allocAsk) s}
  1018                    LeadsTo {s. tokens h \<le> (tokens o sub i o allocRel) s}"
  1019   apply (rule LeadsTo_Trans)
  1020    prefer 2
  1021    apply (drule System_Follows_rel [THEN
  1022      mono_tokens [THEN mono_Follows_o, THEN [2] rev_subsetD],
  1023      THEN Follows_LeadsTo])
  1024    apply (simp add: o_assoc)
  1025   apply (rule LeadsTo_Trans)
  1026    apply (cut_tac [2] System_Client_Progress)
  1027    prefer 2
  1028    apply (blast intro: LeadsTo_Basis)
  1029   apply (erule System_lemma3)
  1030   done
  1031 
  1032 text{*Lifting @{text Alloc_Progress} up to the level of systemState*}
  1033 
  1034 text{*progress (2), step 9*}
  1035 lemma System_Alloc_Progress:
  1036  "System : (INT i : (lessThan Nclients).
  1037             INT h. {s. h \<le> (sub i o allocAsk) s}
  1038                    LeadsTo {s. h pfixLe (sub i o allocGiv) s})"
  1039   apply (simp only: o_apply sub_def)
  1040   apply (insert Alloc_Progress [THEN rename_guarantees_sysOfAlloc_I])
  1041   apply (simp add: o_def del: INT_iff)
  1042   apply (erule component_guaranteesD)
  1043   apply (auto simp add:
  1044     System_Increasing_allocRel [simplified sub_apply o_def]
  1045     System_Increasing_allocAsk [simplified sub_apply o_def]
  1046     System_Bounded_allocAsk [simplified sub_apply o_def]
  1047     System_Alloc_Client_Progress [simplified sub_apply o_def])
  1048   done
  1049 
  1050 text{*progress (2), step 10 (final result!) *}
  1051 lemma System_Progress: "System : system_progress"
  1052   apply (unfold system_progress_def)
  1053   apply (cut_tac System_Alloc_Progress)
  1054   apply (blast intro: LeadsTo_Trans
  1055     System_Follows_allocGiv [THEN Follows_LeadsTo_pfixLe]
  1056     System_Follows_ask [THEN Follows_LeadsTo])
  1057   done
  1058 
  1059 
  1060 theorem System_correct: "System : system_spec"
  1061   apply (unfold system_spec_def)
  1062   apply (blast intro: System_safety System_Progress)
  1063   done
  1064 
  1065 
  1066 text{* Some obsolete lemmas *}
  1067 
  1068 lemma non_dummy_eq_o_funPair: "non_dummy = (% (g,a,r). (| giv = g, ask = a, rel = r |)) o
  1069                               (funPair giv (funPair ask rel))"
  1070   apply (rule ext)
  1071   apply (auto simp add: o_def non_dummy_def)
  1072   done
  1073 
  1074 lemma preserves_non_dummy_eq: "(preserves non_dummy) =
  1075       (preserves rel Int preserves ask Int preserves giv)"
  1076   apply (simp add: non_dummy_eq_o_funPair)
  1077   apply auto
  1078     apply (drule_tac w1 = rel in subset_preserves_o [THEN [2] rev_subsetD])
  1079     apply (drule_tac [2] w1 = ask in subset_preserves_o [THEN [2] rev_subsetD])
  1080     apply (drule_tac [3] w1 = giv in subset_preserves_o [THEN [2] rev_subsetD])
  1081     apply (auto simp add: o_def)
  1082   done
  1083 
  1084 text{*Could go to Extend.ML*}
  1085 lemma bij_fst_inv_inv_eq: "bij f ==> fst (inv (%(x, u). inv f x) z) = f z"
  1086   apply (rule fst_inv_equalityI)
  1087    apply (rule_tac f = "%z. (f z, ?h z) " in surjI)
  1088    apply (simp add: bij_is_inj inv_f_f)
  1089   apply (simp add: bij_is_surj surj_f_inv_f)
  1090   done
  1091 
  1092 end