src/HOL/UNITY/Alloc.ML
author paulson
Mon Oct 11 10:53:39 1999 +0200 (1999-10-11)
changeset 7826 c6a8b73b6c2a
parent 7689 affe0c2fdfbf
child 7841 65d91d13fc13
permissions -rw-r--r--
working shapshot with "projecting" and "extending"
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@7540
     7
paulson@7540
     8
STOP USING o (COMPOSITION), since function application is naturally associative
paulson@7689
     9
paulson@7689
    10
guarantees_PLam_I looks wrong: refers to lift_prog
paulson@6828
    11
*)
paulson@6828
    12
paulson@7399
    13
paulson@7538
    14
Goal "(ALL i: lessThan n. f i <= g i) --> sum f n <= sum g n";
paulson@7538
    15
by (induct_tac "n" 1);
paulson@7538
    16
by Auto_tac;
paulson@7538
    17
by (dres_inst_tac [("x","n")] bspec 1);
paulson@7538
    18
by Auto_tac;
paulson@7538
    19
by (arith_tac 1);
paulson@7538
    20
qed_spec_mp "sum_mono";
paulson@7538
    21
paulson@7540
    22
Goal "ALL xs. xs <= ys --> tokens xs <= tokens ys";
paulson@7540
    23
by (induct_tac "ys" 1);
paulson@7540
    24
by (auto_tac (claset(), simpset() addsimps [prefix_Cons]));
paulson@7540
    25
qed_spec_mp "tokens_mono_prefix";
paulson@7540
    26
paulson@7540
    27
Goalw [mono_def] "mono tokens";
paulson@7540
    28
by (blast_tac (claset() addIs [tokens_mono_prefix]) 1);
paulson@7540
    29
qed "mono_tokens";
paulson@7399
    30
paulson@6840
    31
(*Generalized version allowing different clients*)
paulson@6840
    32
Goal "[| Alloc : alloc_spec;  \
paulson@6840
    33
\        Client : (lessThan Nclients) funcset client_spec;  \
paulson@6840
    34
\        Network : network_spec |] \
paulson@6840
    35
\     ==> (extend sysOfAlloc Alloc) \
paulson@6840
    36
\         Join (extend sysOfClient (PLam (lessThan Nclients) Client)) \
paulson@6840
    37
\         Join Network : system_spec";
paulson@6840
    38
paulson@6840
    39
Goal "System : system_spec";
paulson@6840
    40
paulson@6840
    41
paulson@6828
    42
Goalw [sysOfAlloc_def] "inj sysOfAlloc";
paulson@6828
    43
by (rtac injI 1);
paulson@7347
    44
by (auto_tac (claset() addSWrapper record_split_wrapper, simpset()));
paulson@6828
    45
qed "inj_sysOfAlloc";
paulson@6828
    46
paulson@6828
    47
Goalw [sysOfAlloc_def] "surj sysOfAlloc";
paulson@6828
    48
by (res_inst_tac [("f", "%s. ((| allocGiv = allocGiv s,    \
paulson@6828
    49
\                                allocAsk = allocAsk s,    \
paulson@6828
    50
\                                allocRel = allocRel s |), \
paulson@6828
    51
\                             client s)")] surjI 1);
paulson@7347
    52
by (auto_tac (claset() addSWrapper record_split_wrapper, simpset()));
paulson@6828
    53
qed "surj_sysOfAlloc";
paulson@6828
    54
paulson@6828
    55
AddIffs [inj_sysOfAlloc, surj_sysOfAlloc];
paulson@6828
    56
paulson@7482
    57
Goalw [good_map_def] "good_map sysOfAlloc";
paulson@7482
    58
by Auto_tac;
paulson@7482
    59
qed "good_map_sysOfAlloc";
paulson@7689
    60
Addsimps [good_map_sysOfAlloc];
paulson@7399
    61
paulson@7399
    62
(*MUST BE AUTOMATED: even the statement of such results*)
paulson@7399
    63
Goal "!!s. inv sysOfAlloc s = \
paulson@7399
    64
\            ((| allocGiv = allocGiv s,   \
paulson@7399
    65
\                allocAsk = allocAsk s,   \
paulson@7399
    66
\                allocRel = allocRel s|), \
paulson@7399
    67
\             client s)";
paulson@7399
    68
by (rtac (inj_sysOfAlloc RS inv_f_eq) 1);
paulson@7399
    69
by (auto_tac (claset() addSWrapper record_split_wrapper, 
paulson@7399
    70
	      simpset() addsimps [sysOfAlloc_def]));
paulson@7399
    71
qed "inv_sysOfAlloc_eq";
paulson@7538
    72
Addsimps [inv_sysOfAlloc_eq];
paulson@7399
    73
paulson@7826
    74
paulson@7826
    75
(*SHOULD NOT BE NECESSARY????????????????
paulson@7826
    76
Goal "!!z. (| allocGiv = allocGiv z, allocAsk = allocAsk z, \
paulson@7826
    77
\             allocRel = allocRel z |) = z";
paulson@7826
    78
by (auto_tac (claset() addSWrapper record_split_wrapper, 
paulson@7826
    79
	      simpset()));
paulson@7826
    80
qed "allocState_eq";
paulson@7826
    81
Addsimps [allocState_eq];
paulson@7826
    82
????*)
paulson@7826
    83
paulson@7365
    84
(**SHOULD NOT BE NECESSARY: The various injections into the system
paulson@7365
    85
   state need to be treated symmetrically or done automatically*)
paulson@7347
    86
Goalw [sysOfClient_def] "inj sysOfClient";
paulson@7347
    87
by (rtac injI 1);
paulson@7347
    88
by (auto_tac (claset() addSDs [inj_sysOfAlloc RS injD]
paulson@7347
    89
		       addSWrapper record_split_wrapper, simpset()));
paulson@7347
    90
qed "inj_sysOfClient";
paulson@7347
    91
paulson@7347
    92
Goalw [sysOfClient_def] "surj sysOfClient";
paulson@7347
    93
by (cut_facts_tac [surj_sysOfAlloc] 1);
paulson@7347
    94
by (rewtac surj_def);
paulson@7347
    95
by Auto_tac;
paulson@7347
    96
by (Blast_tac 1);
paulson@7347
    97
qed "surj_sysOfClient";
paulson@7347
    98
paulson@7347
    99
AddIffs [inj_sysOfClient, surj_sysOfClient];
paulson@7347
   100
paulson@7482
   101
Goalw [good_map_def] "good_map sysOfClient";
paulson@7482
   102
by Auto_tac;
paulson@7482
   103
qed "good_map_sysOfClient";
paulson@7689
   104
Addsimps [good_map_sysOfClient];
paulson@6828
   105
paulson@7347
   106
(*MUST BE AUTOMATED: even the statement of such results*)
paulson@7347
   107
Goal "!!s. inv sysOfClient s = \
paulson@7347
   108
\            (client s, \
paulson@7347
   109
\             (| allocGiv = allocGiv s, \
paulson@7347
   110
\                allocAsk = allocAsk s, \
paulson@7347
   111
\                allocRel = allocRel s|) )";
paulson@7347
   112
by (rtac (inj_sysOfClient RS inv_f_eq) 1);
paulson@7399
   113
by (auto_tac (claset() addSWrapper record_split_wrapper, 
paulson@7399
   114
	      simpset() addsimps [sysOfAlloc_def, sysOfClient_def]));
paulson@7365
   115
qed "inv_sysOfClient_eq";
paulson@7689
   116
Addsimps [inv_sysOfClient_eq];
paulson@6837
   117
paulson@6837
   118
paulson@7365
   119
Open_locale "System";
paulson@7365
   120
paulson@7365
   121
val Alloc = thm "Alloc";
paulson@7365
   122
val Client = thm "Client";
paulson@7365
   123
val Network = thm "Network";
paulson@7365
   124
val System_def = thm "System_def";
paulson@7365
   125
paulson@7365
   126
AddIffs [finite_lessThan];
paulson@7365
   127
paulson@7365
   128
(*Client : <unfolded specification> *)
paulson@7365
   129
val Client_Spec =
paulson@7365
   130
    rewrite_rule [client_spec_def, client_increasing_def,
paulson@7365
   131
		  client_bounded_def, client_progress_def] Client;
paulson@7365
   132
paulson@7365
   133
Goal "Client : UNIV guarantees Increasing ask";
paulson@7365
   134
by (cut_facts_tac [Client_Spec] 1);
paulson@7365
   135
by (asm_full_simp_tac (simpset() addsimps [guarantees_Int_right]) 1);
paulson@7365
   136
qed "Client_Increasing_ask";
paulson@7365
   137
paulson@7365
   138
Goal "Client : UNIV guarantees Increasing rel";
paulson@7365
   139
by (cut_facts_tac [Client_Spec] 1);
paulson@7365
   140
by (asm_full_simp_tac (simpset() addsimps [guarantees_Int_right]) 1);
paulson@7365
   141
qed "Client_Increasing_rel";
paulson@7365
   142
paulson@7365
   143
AddIffs [Client_Increasing_ask, Client_Increasing_rel];
paulson@7365
   144
paulson@7365
   145
Goal "Client : UNIV guarantees Always {s. ALL elt : set (ask s). elt <= NbT}";
paulson@7365
   146
by (cut_facts_tac [Client_Spec] 1);
paulson@7365
   147
by Auto_tac;
paulson@7365
   148
qed "Client_Bounded";
paulson@7365
   149
paulson@7365
   150
(*Client_Progress is cumbersome to state*)
paulson@7365
   151
val Client_Progress = Client_Spec RS IntD2;
paulson@6828
   152
paulson@6828
   153
paulson@7365
   154
(*Network : <unfolded specification> *)
paulson@7365
   155
val Network_Spec =
paulson@7365
   156
    rewrite_rule [network_spec_def, network_ask_def,
paulson@7365
   157
		  network_giv_def, network_rel_def] Network;
paulson@7365
   158
paulson@7365
   159
(*CANNOT use bind_thm: it puts the theorem into standard form, in effect
paulson@7365
   160
  exporting it from the locale*)
paulson@7689
   161
val Network_Ask = Network_Spec RS IntD1 RS IntD1 RS INT_D;
paulson@7540
   162
val Network_Giv = Network_Spec RS IntD1 RS IntD2 RS INT_D;
paulson@7365
   163
val Network_Rel = Network_Spec RS IntD2 RS INT_D;
paulson@7365
   164
paulson@7365
   165
paulson@7365
   166
(*Alloc : <unfolded specification> *)
paulson@7365
   167
val Alloc_Spec =
paulson@7365
   168
    rewrite_rule [alloc_spec_def, alloc_increasing_def,
paulson@7365
   169
		  alloc_safety_def, alloc_progress_def] Alloc;
paulson@7365
   170
paulson@7540
   171
Goal "i < Nclients ==> Alloc : UNIV guarantees Increasing (sub i o allocGiv)";
paulson@7365
   172
by (cut_facts_tac [Alloc_Spec] 1);
paulson@7365
   173
by (asm_full_simp_tac (simpset() addsimps [guarantees_INT_right]) 1);
paulson@7365
   174
qed "Alloc_Increasing";
paulson@7365
   175
paulson@7365
   176
val Alloc_Safety = Alloc_Spec RS IntD1 RS IntD2;
paulson@7365
   177
val Alloc_Progress = (Alloc_Spec RS IntD2
paulson@7365
   178
                      |> simplify (simpset() addsimps [guarantees_INT_right]))
paulson@7365
   179
                     RS bspec RS spec;
paulson@7365
   180
		     
paulson@7365
   181
paulson@7347
   182
paulson@7365
   183
(*Not sure what to say about the other components because they involve
paulson@7365
   184
  extend*)
paulson@7399
   185
Goalw [System_def] "Network <= System";
paulson@7365
   186
by (blast_tac (claset() addIs [componentI]) 1);
paulson@7365
   187
qed "Network_component_System";
paulson@7365
   188
paulson@7399
   189
Goalw [System_def] "(extend sysOfAlloc Alloc) <= System";
paulson@7399
   190
by (blast_tac (claset() addIs [componentI]) 1);
paulson@7399
   191
qed "Alloc_component_System";
paulson@7365
   192
paulson@7399
   193
AddIffs [Network_component_System, Alloc_component_System];
paulson@7399
   194
paulson@7365
   195
paulson@7826
   196
fun alloc_export th = good_map_sysOfAlloc RS export th |> simplify (simpset());
paulson@7689
   197
paulson@7826
   198
fun client_export th = good_map_sysOfClient RS export th |> simplify (simpset());
paulson@7689
   199
paulson@7365
   200
(* F : UNIV guarantees Increasing func
paulson@7365
   201
   ==> extend sysOfClient F : UNIV guarantees Increasing (func o client) *)
paulson@7399
   202
val extend_Client_guar_Increasing =
paulson@7826
   203
  client_export extend_guar_Increasing;
paulson@7365
   204
paulson@7540
   205
(*NEED AUTOMATIC PROPAGATION of Alloc_Increasing*)
paulson@7540
   206
Goal "i < Nclients \
paulson@7540
   207
\ ==> extend sysOfAlloc Alloc : UNIV guarantees Increasing (sub i o allocGiv)";
paulson@7540
   208
by (dtac (Alloc_Increasing RS alloc_export extend_guar_Increasing) 1);
paulson@7540
   209
by (auto_tac (claset(), simpset() addsimps [o_def]));
paulson@7540
   210
qed "extend_Alloc_Increasing_allocGiv";
paulson@7540
   211
paulson@7365
   212
paulson@7689
   213
(*** Proof of the safety property (1) ***)
paulson@7365
   214
paulson@7689
   215
(*safety (1), step 1*)
paulson@7365
   216
Goalw [System_def]
paulson@7365
   217
     "i < Nclients ==> System : Increasing (rel o sub i o client)";
paulson@7689
   218
by (rtac (extend_Client_guar_Increasing RS guarantees_Join_I2 
paulson@7689
   219
	  RS guaranteesD) 1);
paulson@7689
   220
by (rtac (lift_prog_guar_Increasing RS guarantees_PLam_I) 1);
paulson@7689
   221
(*gets Client_Increasing_rel from simpset*)
paulson@7689
   222
by Auto_tac;
paulson@7347
   223
qed "System_Increasing_rel";
paulson@6828
   224
paulson@6828
   225
paulson@7689
   226
(*safety (1), step 2*)
paulson@7365
   227
Goal "i < Nclients ==> System : Increasing (sub i o allocRel)";
paulson@7365
   228
by (rtac Follows_Increasing1 1);
paulson@7365
   229
by (blast_tac (claset() addIs [Network_Rel RS component_guaranteesD,
paulson@7540
   230
			       System_Increasing_rel]) 1);
paulson@7365
   231
qed "System_Increasing_allocRel";
paulson@6828
   232
paulson@7826
   233
paulson@7826
   234
paulson@7689
   235
(*safety (1), step 3*)
paulson@7399
   236
Goal "System : Always {s. sum (%i. (tokens o sub i o allocGiv) s) Nclients \
paulson@7399
   237
\                  <= NbT + sum (%i. (tokens o sub i o allocRel) s) Nclients}";
paulson@7399
   238
by (res_inst_tac 
paulson@7537
   239
    [("X", "(INT i : lessThan Nclients. Increasing (sub i o allocRel))")] 
paulson@7537
   240
    component_guaranteesD 1);
paulson@7482
   241
by (rtac Alloc_component_System 3);
paulson@7537
   242
by (force_tac (claset(), simpset() addsimps [System_Increasing_allocRel]) 2);
paulson@7538
   243
by (rtac (Alloc_Safety RS project_guarantees) 1);
paulson@7826
   244
(*1: Increasing precondition*)
paulson@7826
   245
br (ballI RS projecting_INT) 1;
paulson@7826
   246
by (rtac (alloc_export projecting_Increasing RS projecting_weaken) 1);
paulson@7537
   247
by Auto_tac;
paulson@7826
   248
by (asm_full_simp_tac (simpset() addsimps [o_def]) 1);
paulson@7538
   249
(*2: Always postcondition*)
paulson@7826
   250
by (rtac ((alloc_export extending_Always RS extending_weaken)) 1);
paulson@7826
   251
by Auto_tac;
paulson@7538
   252
by (asm_full_simp_tac
paulson@7538
   253
     (simpset() addsimps [alloc_export Collect_eq_extend_set RS sym]) 1);
paulson@7538
   254
qed "System_sum_bounded";
paulson@7537
   255
paulson@7689
   256
(*safety (1), step 4*)
paulson@7540
   257
Goal "System : Always (INT i: lessThan Nclients. \
paulson@7540
   258
\                         {s. (tokens o giv o sub i o client) s \
paulson@7540
   259
\                          <= (tokens o sub i o allocGiv) s})";
paulson@7540
   260
by (auto_tac (claset(), 
paulson@7540
   261
	      simpset() delsimps [o_apply]
paulson@7540
   262
			addsimps [Always_INT_distrib]));
paulson@7540
   263
by (rtac Follows_Bounded 1);
paulson@7540
   264
by (simp_tac (HOL_ss addsimps [o_assoc RS sym]) 1);
paulson@7540
   265
by (rtac (mono_tokens RS mono_Follows_o RS subsetD) 1);
paulson@7540
   266
by (simp_tac (HOL_ss addsimps [o_assoc]) 1);
paulson@7540
   267
by (blast_tac (claset() addIs [Network_Giv RS component_guaranteesD,
paulson@7540
   268
	  extend_Alloc_Increasing_allocGiv RS component_guaranteesD]) 1);
paulson@7540
   269
qed "System_Always_giv_le_allocGiv";
paulson@7540
   270
paulson@7540
   271
paulson@7689
   272
(*safety (1), step 5*)
paulson@7540
   273
Goal "System : Always (INT i: lessThan Nclients. \
paulson@7540
   274
\                         {s. (tokens o sub i o allocRel) s \
paulson@7540
   275
\                          <= (tokens o rel o sub i o client) s})";
paulson@7540
   276
by (auto_tac (claset(), 
paulson@7540
   277
	      simpset() delsimps [o_apply]
paulson@7540
   278
			addsimps [Always_INT_distrib]));
paulson@7540
   279
by (rtac Follows_Bounded 1);
paulson@7540
   280
by (simp_tac (HOL_ss addsimps [o_assoc RS sym]) 1);
paulson@7540
   281
by (rtac (mono_tokens RS mono_Follows_o RS subsetD) 1);
paulson@7540
   282
by (simp_tac (HOL_ss addsimps [o_assoc]) 1);
paulson@7540
   283
by (blast_tac (claset() addIs [Network_Rel RS component_guaranteesD,
paulson@7540
   284
			       System_Increasing_rel]) 1);
paulson@7540
   285
qed "System_Always_allocRel_le_rel";
paulson@7540
   286
paulson@7540
   287
paulson@7689
   288
(*safety (1), step 6*)
paulson@7540
   289
Goal "System : Always {s. sum (%i. (tokens o giv o sub i o client)s) Nclients \
paulson@7540
   290
\              <= NbT + sum (%i. (tokens o rel o sub i o client)s) Nclients}";
paulson@7540
   291
by (rtac (Always_Int_rule [System_sum_bounded, System_Always_giv_le_allocGiv, 
paulson@7540
   292
			   System_Always_allocRel_le_rel] RS Always_weaken) 1);
paulson@7538
   293
by Auto_tac;
paulson@7540
   294
by (rtac (sum_mono RS order_trans) 1);
paulson@7540
   295
by (dtac order_trans 2);
paulson@7540
   296
by (rtac ([order_refl, sum_mono] MRS add_le_mono) 2);
paulson@7540
   297
by (assume_tac 3);
paulson@7482
   298
by Auto_tac;
paulson@7540
   299
qed "System_safety";
paulson@7399
   300
paulson@7689
   301
paulson@7689
   302
paulson@7689
   303
(*** Proof of the progress property (2) ***)
paulson@7689
   304
paulson@7689
   305
(*we begin with proofs identical to System_Increasing_rel and
paulson@7689
   306
  System_Increasing_allocRel: tactics needed!*)
paulson@7689
   307
paulson@7689
   308
(*progress (2), step 1*)
paulson@7689
   309
Goalw [System_def]
paulson@7689
   310
     "i < Nclients ==> System : Increasing (ask o sub i o client)";
paulson@7689
   311
by (rtac (extend_Client_guar_Increasing RS guarantees_Join_I2 
paulson@7689
   312
	  RS guaranteesD) 1);
paulson@7689
   313
by (rtac (lift_prog_guar_Increasing RS guarantees_PLam_I) 1);
paulson@7689
   314
by Auto_tac;
paulson@7689
   315
qed "System_Increasing_ask";
paulson@7689
   316
paulson@7689
   317
(*progress (2), step 2*)
paulson@7689
   318
Goal "i < Nclients ==> System : Increasing (sub i o allocAsk)";
paulson@7689
   319
by (rtac Follows_Increasing1 1);
paulson@7689
   320
by (blast_tac (claset() addIs [Network_Ask RS component_guaranteesD,
paulson@7689
   321
			       System_Increasing_ask]) 1);
paulson@7689
   322
qed "System_Increasing_allocAsk";
paulson@7689
   323
paulson@7689
   324
(*progress (2), step 3*)
paulson@7689
   325
(*All this trouble just to lift "Client_Bounded" through two extemd ops*)
paulson@7689
   326
Goalw [System_def]
paulson@7689
   327
     "i < Nclients \
paulson@7689
   328
\   ==> System : Always \
paulson@7689
   329
\                 {s. ALL elt : set ((ask o sub i o client) s). elt <= NbT}";
paulson@7689
   330
by (rtac (lift_prog_guar_Always RS 
paulson@7689
   331
	  guarantees_PLam_I RS client_export extend_guar_Always RS
paulson@7689
   332
	  guarantees_Join_I2 RS guaranteesD RS Always_weaken) 1);
paulson@7689
   333
by (stac Always_UNIV_eq 1 THEN rtac Client_Bounded 1);
paulson@7689
   334
by (auto_tac(claset(),
paulson@7689
   335
	 simpset() addsimps [Collect_eq_lift_set RS sym,
paulson@7689
   336
			     client_export Collect_eq_extend_set RS sym]));
paulson@7689
   337
qed "System_Bounded";