src/HOL/UNITY/Alloc.ML
author paulson
Fri Sep 10 18:40:06 1999 +0200 (1999-09-10)
changeset 7537 875754b599df
parent 7482 7badd511844d
child 7538 357873391561
permissions -rw-r--r--
working snapshot
paulson@6828
     1
(*  Title:      HOL/UNITY/Alloc
paulson@6828
     2
    ID:         $Id$
paulson@6828
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
paulson@6828
     4
    Copyright   1998  University of Cambridge
paulson@6828
     5
paulson@6828
     6
Specification of Chandy and Charpentier's Allocator
paulson@6828
     7
*)
paulson@6828
     8
paulson@7399
     9
paulson@7399
    10
Goal "~ f #2 ==> ~ (!t::nat. (#0 <= t & t <= #10) --> f t)";
paulson@7399
    11
paulson@7399
    12
(*Useful examples:  singletonI RS subst_elem,  subst_elem RSN (2,IntI) *)
paulson@7399
    13
Goal "[| b:A;  a=b |] ==> a:A";
paulson@7399
    14
by (etac ssubst 1);
paulson@7399
    15
by (assume_tac 1);
paulson@7399
    16
qed "subst_elem";
paulson@7399
    17
paulson@7399
    18
paulson@7399
    19
paulson@7399
    20
paulson@6840
    21
(*Generalized version allowing different clients*)
paulson@6840
    22
Goal "[| Alloc : alloc_spec;  \
paulson@6840
    23
\        Client : (lessThan Nclients) funcset client_spec;  \
paulson@6840
    24
\        Network : network_spec |] \
paulson@6840
    25
\     ==> (extend sysOfAlloc Alloc) \
paulson@6840
    26
\         Join (extend sysOfClient (PLam (lessThan Nclients) Client)) \
paulson@6840
    27
\         Join Network : system_spec";
paulson@6840
    28
paulson@6840
    29
Goal "System : system_spec";
paulson@6840
    30
paulson@6840
    31
paulson@6828
    32
Goalw [sysOfAlloc_def] "inj sysOfAlloc";
paulson@6828
    33
by (rtac injI 1);
paulson@7347
    34
by (auto_tac (claset() addSWrapper record_split_wrapper, simpset()));
paulson@6828
    35
qed "inj_sysOfAlloc";
paulson@6828
    36
paulson@6828
    37
Goalw [sysOfAlloc_def] "surj sysOfAlloc";
paulson@6828
    38
by (res_inst_tac [("f", "%s. ((| allocGiv = allocGiv s,    \
paulson@6828
    39
\                                allocAsk = allocAsk s,    \
paulson@6828
    40
\                                allocRel = allocRel s |), \
paulson@6828
    41
\                             client s)")] surjI 1);
paulson@7347
    42
by (auto_tac (claset() addSWrapper record_split_wrapper, simpset()));
paulson@6828
    43
qed "surj_sysOfAlloc";
paulson@6828
    44
paulson@6828
    45
AddIffs [inj_sysOfAlloc, surj_sysOfAlloc];
paulson@6828
    46
paulson@7482
    47
Goalw [good_map_def] "good_map sysOfAlloc";
paulson@7482
    48
by Auto_tac;
paulson@7482
    49
qed "good_map_sysOfAlloc";
paulson@7399
    50
paulson@7399
    51
(*MUST BE AUTOMATED: even the statement of such results*)
paulson@7399
    52
Goal "!!s. inv sysOfAlloc s = \
paulson@7399
    53
\            ((| allocGiv = allocGiv s,   \
paulson@7399
    54
\                allocAsk = allocAsk s,   \
paulson@7399
    55
\                allocRel = allocRel s|), \
paulson@7399
    56
\             client s)";
paulson@7399
    57
by (rtac (inj_sysOfAlloc RS inv_f_eq) 1);
paulson@7399
    58
by (auto_tac (claset() addSWrapper record_split_wrapper, 
paulson@7399
    59
	      simpset() addsimps [sysOfAlloc_def]));
paulson@7399
    60
qed "inv_sysOfAlloc_eq";
paulson@7399
    61
paulson@7399
    62
paulson@7365
    63
(**SHOULD NOT BE NECESSARY: The various injections into the system
paulson@7365
    64
   state need to be treated symmetrically or done automatically*)
paulson@7347
    65
Goalw [sysOfClient_def] "inj sysOfClient";
paulson@7347
    66
by (rtac injI 1);
paulson@7347
    67
by (auto_tac (claset() addSDs [inj_sysOfAlloc RS injD]
paulson@7347
    68
		       addSWrapper record_split_wrapper, simpset()));
paulson@7347
    69
qed "inj_sysOfClient";
paulson@7347
    70
paulson@7347
    71
Goalw [sysOfClient_def] "surj sysOfClient";
paulson@7347
    72
by (cut_facts_tac [surj_sysOfAlloc] 1);
paulson@7347
    73
by (rewtac surj_def);
paulson@7347
    74
by Auto_tac;
paulson@7347
    75
by (Blast_tac 1);
paulson@7347
    76
qed "surj_sysOfClient";
paulson@7347
    77
paulson@7347
    78
AddIffs [inj_sysOfClient, surj_sysOfClient];
paulson@7347
    79
paulson@7482
    80
Goalw [good_map_def] "good_map sysOfClient";
paulson@7482
    81
by Auto_tac;
paulson@7482
    82
qed "good_map_sysOfClient";
paulson@6828
    83
paulson@7347
    84
(*MUST BE AUTOMATED: even the statement of such results*)
paulson@7347
    85
Goal "!!s. inv sysOfClient s = \
paulson@7347
    86
\            (client s, \
paulson@7347
    87
\             (| allocGiv = allocGiv s, \
paulson@7347
    88
\                allocAsk = allocAsk s, \
paulson@7347
    89
\                allocRel = allocRel s|) )";
paulson@7347
    90
by (rtac (inj_sysOfClient RS inv_f_eq) 1);
paulson@7399
    91
by (auto_tac (claset() addSWrapper record_split_wrapper, 
paulson@7399
    92
	      simpset() addsimps [sysOfAlloc_def, sysOfClient_def]));
paulson@7365
    93
qed "inv_sysOfClient_eq";
paulson@6837
    94
paulson@6837
    95
paulson@7365
    96
Open_locale "System";
paulson@7365
    97
paulson@7365
    98
val Alloc = thm "Alloc";
paulson@7365
    99
val Client = thm "Client";
paulson@7365
   100
val Network = thm "Network";
paulson@7365
   101
val System_def = thm "System_def";
paulson@7365
   102
paulson@7365
   103
AddIffs [finite_lessThan];
paulson@7365
   104
paulson@7365
   105
(*Client : <unfolded specification> *)
paulson@7365
   106
val Client_Spec =
paulson@7365
   107
    rewrite_rule [client_spec_def, client_increasing_def,
paulson@7365
   108
		  client_bounded_def, client_progress_def] Client;
paulson@7365
   109
paulson@7365
   110
Goal "Client : UNIV guarantees Increasing ask";
paulson@7365
   111
by (cut_facts_tac [Client_Spec] 1);
paulson@7365
   112
by (asm_full_simp_tac (simpset() addsimps [guarantees_Int_right]) 1);
paulson@7365
   113
qed "Client_Increasing_ask";
paulson@7365
   114
paulson@7365
   115
Goal "Client : UNIV guarantees Increasing rel";
paulson@7365
   116
by (cut_facts_tac [Client_Spec] 1);
paulson@7365
   117
by (asm_full_simp_tac (simpset() addsimps [guarantees_Int_right]) 1);
paulson@7365
   118
qed "Client_Increasing_rel";
paulson@7365
   119
paulson@7365
   120
AddIffs [Client_Increasing_ask, Client_Increasing_rel];
paulson@7365
   121
paulson@7365
   122
Goal "Client : UNIV guarantees Always {s. ALL elt : set (ask s). elt <= NbT}";
paulson@7365
   123
by (cut_facts_tac [Client_Spec] 1);
paulson@7365
   124
by Auto_tac;
paulson@7365
   125
qed "Client_Bounded";
paulson@7365
   126
paulson@7365
   127
(*Client_Progress is cumbersome to state*)
paulson@7365
   128
val Client_Progress = Client_Spec RS IntD2;
paulson@6828
   129
paulson@6828
   130
paulson@7365
   131
(*Network : <unfolded specification> *)
paulson@7365
   132
val Network_Spec =
paulson@7365
   133
    rewrite_rule [network_spec_def, network_ask_def,
paulson@7365
   134
		  network_giv_def, network_rel_def] Network;
paulson@7365
   135
paulson@7365
   136
(*CANNOT use bind_thm: it puts the theorem into standard form, in effect
paulson@7365
   137
  exporting it from the locale*)
paulson@7365
   138
val Network_Ask = Network_Spec RS IntD1 RS IntD1;
paulson@7365
   139
val Network_Giv = Network_Spec RS IntD1 RS IntD2;
paulson@7365
   140
val Network_Rel = Network_Spec RS IntD2 RS INT_D;
paulson@7365
   141
paulson@7365
   142
paulson@7365
   143
(*Alloc : <unfolded specification> *)
paulson@7365
   144
val Alloc_Spec =
paulson@7365
   145
    rewrite_rule [alloc_spec_def, alloc_increasing_def,
paulson@7365
   146
		  alloc_safety_def, alloc_progress_def] Alloc;
paulson@7365
   147
paulson@7365
   148
Goal "i < Nclients ==> Alloc : UNIV guarantees Increasing (sub i o allocAsk)";
paulson@7365
   149
by (cut_facts_tac [Alloc_Spec] 1);
paulson@7365
   150
by (asm_full_simp_tac (simpset() addsimps [guarantees_INT_right]) 1);
paulson@7365
   151
qed "Alloc_Increasing";
paulson@7365
   152
paulson@7365
   153
val Alloc_Safety = Alloc_Spec RS IntD1 RS IntD2;
paulson@7365
   154
val Alloc_Progress = (Alloc_Spec RS IntD2
paulson@7365
   155
                      |> simplify (simpset() addsimps [guarantees_INT_right]))
paulson@7365
   156
                     RS bspec RS spec;
paulson@7365
   157
		     
paulson@7365
   158
paulson@7347
   159
paulson@7365
   160
(*Not sure what to say about the other components because they involve
paulson@7365
   161
  extend*)
paulson@7399
   162
Goalw [System_def] "Network <= System";
paulson@7365
   163
by (blast_tac (claset() addIs [componentI]) 1);
paulson@7365
   164
qed "Network_component_System";
paulson@7365
   165
paulson@7399
   166
Goalw [System_def] "(extend sysOfAlloc Alloc) <= System";
paulson@7399
   167
by (blast_tac (claset() addIs [componentI]) 1);
paulson@7399
   168
qed "Alloc_component_System";
paulson@7365
   169
paulson@7399
   170
AddIffs [Network_component_System, Alloc_component_System];
paulson@7399
   171
paulson@7365
   172
paulson@7365
   173
(* F : UNIV guarantees Increasing func
paulson@7365
   174
   ==> extend sysOfClient F : UNIV guarantees Increasing (func o client) *)
paulson@7399
   175
val extend_Client_guar_Increasing =
paulson@7482
   176
  good_map_sysOfClient RS export extend_guar_Increasing
paulson@7365
   177
  |> simplify (simpset() addsimps [inv_sysOfClient_eq]);
paulson@7365
   178
paulson@7365
   179
paulson@7365
   180
(** Proof of property (1) **)
paulson@7365
   181
paulson@7365
   182
(*step 1*)
paulson@7365
   183
Goalw [System_def]
paulson@7365
   184
     "i < Nclients ==> System : Increasing (rel o sub i o client)";
paulson@7365
   185
by (rtac ([guaranteesI RS disjI2 RS guarantees_Join_I, UNIV_I] 
paulson@7365
   186
	  MRS guaranteesD) 1);
paulson@7365
   187
by (asm_simp_tac 
paulson@7365
   188
    (simpset() addsimps [guarantees_PLam_I, 
paulson@7399
   189
			 extend_Client_guar_Increasing RS guaranteesD,
paulson@7365
   190
			 lift_prog_guar_Increasing]) 1);
paulson@7347
   191
qed "System_Increasing_rel";
paulson@6828
   192
paulson@7365
   193
(*Note: the first step above performs simple quantifier reasoning.  It could
paulson@7365
   194
  be replaced by a proof mentioning no guarantees primitives*)
paulson@6828
   195
paulson@6828
   196
paulson@7365
   197
(*step 2*)
paulson@7365
   198
Goal "i < Nclients ==> System : Increasing (sub i o allocRel)";
paulson@7365
   199
by (rtac Follows_Increasing1 1);
paulson@7365
   200
by (blast_tac (claset() addIs [Network_Rel RS component_guaranteesD,
paulson@7365
   201
			       System_Increasing_rel, Network]) 1);
paulson@7365
   202
qed "System_Increasing_allocRel";
paulson@6828
   203
paulson@7399
   204
paulson@7399
   205
(*NEED TO PROVE something like this (maybe without premise)*)
paulson@7399
   206
Goal "i < Nclients ==> System : (sub i o allocRel) localTo Network";
paulson@7347
   207
paulson@7482
   208
fun alloc_export th = good_map_sysOfAlloc RS export th;
paulson@7399
   209
paulson@7399
   210
val extend_Alloc_guar_Increasing =
paulson@7399
   211
  alloc_export extend_guar_Increasing
paulson@7365
   212
  |> simplify (simpset() addsimps [inv_sysOfAlloc_eq]);
paulson@6828
   213
paulson@7399
   214
Goal "System : Always {s. sum (%i. (tokens o sub i o allocGiv) s) Nclients \
paulson@7399
   215
\                  <= NbT + sum (%i. (tokens o sub i o allocRel) s) Nclients}";
paulson@7399
   216
by (res_inst_tac 
paulson@7537
   217
    [("X", "(INT i : lessThan Nclients. Increasing (sub i o allocRel))")] 
paulson@7537
   218
    component_guaranteesD 1);
paulson@7482
   219
by (rtac Alloc_component_System 3);
paulson@7537
   220
by (force_tac (claset(), simpset() addsimps [System_Increasing_allocRel]) 2);
paulson@7482
   221
by (rtac project_guarantees 1);
paulson@7482
   222
by (rtac Alloc_Safety 1);
paulson@7537
   223
by Auto_tac;
paulson@7537
   224
by (rtac project_Increasing_I 1);
paulson@7537
   225
paulson@7399
   226
by (dtac (alloc_export (project_extend_Join RSN (2, subst_elem RS project_Always_D))) 2 
paulson@7399
   227
     THEN
paulson@7399
   228
     full_simp_tac
paulson@7399
   229
     (simpset() addsimps [inv_sysOfAlloc_eq,
paulson@7399
   230
			  alloc_export Collect_eq_extend_set RS sym]) 2);
paulson@7482
   231
by Auto_tac;
paulson@7399
   232
paulson@7482
   233
by (dtac bspec 1);
paulson@7399
   234
by (Blast_tac 1);
paulson@7399
   235
paulson@7399
   236
paulson@7399
   237
xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx;
paulson@7537
   238
FIRST STEP WAS
paulson@7537
   239
by (res_inst_tac 
paulson@7537
   240
    [("X", "(INT i : lessThan Nclients. (sub i o allocRel) localTo Network \
paulson@7537
   241
\                                       Int Increasing (sub i o allocRel))")] 
paulson@7537
   242
    component_guaranteesD 1);
paulson@7537
   243
paulson@7399
   244
paulson@7399
   245
       [| i < Nclients;
paulson@7399
   246
          extend sysOfAlloc Alloc Join G
paulson@7399
   247
          : (sub i o allocRel) localTo Network &
paulson@7399
   248
          extend sysOfAlloc Alloc Join G : Increasing (sub i o allocRel) |]
paulson@7399
   249
       ==> Alloc Join project sysOfAlloc G : Increasing (sub i o allocRel)
paulson@7399
   250
paulson@7399
   251
paulson@7399
   252
       [| i < Nclients;
paulson@7399
   253
          H : (sub i o allocRel) localTo Network &
paulson@7399
   254
          H : Increasing (sub i o allocRel) |]
paulson@7399
   255
       ==> project sysOfAlloc H : Increasing (sub i o allocRel)
paulson@7399
   256
paulson@7399
   257
Open_locale"Extend";
paulson@7399
   258
paulson@7399
   259
Goal "(H : (func o f) localTo G) ==> (project h H : func localTo (project h G))";
paulson@7399
   260
by (asm_full_simp_tac 
paulson@7399
   261
    (simpset() addsimps [localTo_def, 
paulson@7399
   262
			 project_extend_Join RS sym,
paulson@7399
   263
			 Diff_project_stable,
paulson@7399
   264
			 Collect_eq_extend_set RS sym]) 1);
paulson@7482
   265
by Auto_tac;
paulson@7482
   266
by (rtac Diff_project_stable 1);
paulson@7399
   267
PROBABLY FALSE;
paulson@7399
   268
paulson@7399
   269
by (Clarify_tac 1);
paulson@7399
   270
by (dres_inst_tac [("x","z")] spec 1);
paulson@7399
   271
paulson@7482
   272
by (rtac (alloc_export project_Always_D) 2);
paulson@7399
   273
paulson@7399
   274
by (rtac (alloc_export extend_Always RS iffD2) 2);
paulson@7399
   275
paulson@7399
   276
xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx;
paulson@7399
   277
paulson@7482
   278
by (rtac guaranteesI 1);
paulson@7399
   279
paulson@7399
   280
by (res_inst_tac 
paulson@7399
   281
    [("X", "(INT i : lessThan Nclients. Increasing (sub i o allocRel))")] 
paulson@7399
   282
    component_guaranteesD 1);;
paulson@7399
   283
paulson@7399
   284
paulson@7365
   285
by (rtac (Alloc_Safety RS component_guaranteesD) 1);
paulson@7399
   286
paulson@7399
   287
paulson@7482
   288
by (rtac (alloc_export guarantees_imp_extend_guarantees RS guarantees_weaken) 1);
paulson@7482
   289
by (rtac Alloc_Safety 1);