src/HOL/UNITY/Alloc.ML
author paulson
Wed Oct 13 12:05:25 1999 +0200 (1999-10-13)
changeset 7841 65d91d13fc13
parent 7826 c6a8b73b6c2a
child 7878 43b03d412b82
permissions -rw-r--r--
working snapshot; more steps in Alloc
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@7841
     8
Stop using o (composition)?
paulson@7689
     9
paulson@7689
    10
guarantees_PLam_I looks wrong: refers to lift_prog
paulson@6828
    11
*)
paulson@6828
    12
paulson@7841
    13
(*Eliminating the "o" operator gives associativity for free*)
paulson@7841
    14
val o_simp = simplify (simpset() addsimps [o_def]);
paulson@7399
    15
paulson@7538
    16
Goal "(ALL i: lessThan n. f i <= g i) --> sum f n <= sum g n";
paulson@7538
    17
by (induct_tac "n" 1);
paulson@7538
    18
by Auto_tac;
paulson@7538
    19
by (dres_inst_tac [("x","n")] bspec 1);
paulson@7538
    20
by Auto_tac;
paulson@7538
    21
by (arith_tac 1);
paulson@7538
    22
qed_spec_mp "sum_mono";
paulson@7538
    23
paulson@7540
    24
Goal "ALL xs. xs <= ys --> tokens xs <= tokens ys";
paulson@7540
    25
by (induct_tac "ys" 1);
paulson@7540
    26
by (auto_tac (claset(), simpset() addsimps [prefix_Cons]));
paulson@7540
    27
qed_spec_mp "tokens_mono_prefix";
paulson@7540
    28
paulson@7540
    29
Goalw [mono_def] "mono tokens";
paulson@7540
    30
by (blast_tac (claset() addIs [tokens_mono_prefix]) 1);
paulson@7540
    31
qed "mono_tokens";
paulson@7399
    32
paulson@6840
    33
(*Generalized version allowing different clients*)
paulson@6840
    34
Goal "[| Alloc : alloc_spec;  \
paulson@6840
    35
\        Client : (lessThan Nclients) funcset client_spec;  \
paulson@6840
    36
\        Network : network_spec |] \
paulson@6840
    37
\     ==> (extend sysOfAlloc Alloc) \
paulson@6840
    38
\         Join (extend sysOfClient (PLam (lessThan Nclients) Client)) \
paulson@6840
    39
\         Join Network : system_spec";
paulson@6840
    40
paulson@6840
    41
Goal "System : system_spec";
paulson@6840
    42
paulson@6840
    43
paulson@6828
    44
Goalw [sysOfAlloc_def] "inj sysOfAlloc";
paulson@6828
    45
by (rtac injI 1);
paulson@7347
    46
by (auto_tac (claset() addSWrapper record_split_wrapper, simpset()));
paulson@6828
    47
qed "inj_sysOfAlloc";
paulson@6828
    48
paulson@6828
    49
Goalw [sysOfAlloc_def] "surj sysOfAlloc";
paulson@6828
    50
by (res_inst_tac [("f", "%s. ((| allocGiv = allocGiv s,    \
paulson@6828
    51
\                                allocAsk = allocAsk s,    \
paulson@6828
    52
\                                allocRel = allocRel s |), \
paulson@6828
    53
\                             client s)")] surjI 1);
paulson@7347
    54
by (auto_tac (claset() addSWrapper record_split_wrapper, simpset()));
paulson@6828
    55
qed "surj_sysOfAlloc";
paulson@6828
    56
paulson@6828
    57
AddIffs [inj_sysOfAlloc, surj_sysOfAlloc];
paulson@6828
    58
paulson@7482
    59
Goalw [good_map_def] "good_map sysOfAlloc";
paulson@7482
    60
by Auto_tac;
paulson@7482
    61
qed "good_map_sysOfAlloc";
paulson@7689
    62
Addsimps [good_map_sysOfAlloc];
paulson@7399
    63
paulson@7399
    64
(*MUST BE AUTOMATED: even the statement of such results*)
paulson@7399
    65
Goal "!!s. inv sysOfAlloc s = \
paulson@7399
    66
\            ((| allocGiv = allocGiv s,   \
paulson@7399
    67
\                allocAsk = allocAsk s,   \
paulson@7399
    68
\                allocRel = allocRel s|), \
paulson@7399
    69
\             client s)";
paulson@7399
    70
by (rtac (inj_sysOfAlloc RS inv_f_eq) 1);
paulson@7399
    71
by (auto_tac (claset() addSWrapper record_split_wrapper, 
paulson@7399
    72
	      simpset() addsimps [sysOfAlloc_def]));
paulson@7399
    73
qed "inv_sysOfAlloc_eq";
paulson@7538
    74
Addsimps [inv_sysOfAlloc_eq];
paulson@7399
    75
paulson@7826
    76
paulson@7826
    77
(*SHOULD NOT BE NECESSARY????????????????
paulson@7826
    78
Goal "!!z. (| allocGiv = allocGiv z, allocAsk = allocAsk z, \
paulson@7826
    79
\             allocRel = allocRel z |) = z";
paulson@7826
    80
by (auto_tac (claset() addSWrapper record_split_wrapper, 
paulson@7826
    81
	      simpset()));
paulson@7826
    82
qed "allocState_eq";
paulson@7826
    83
Addsimps [allocState_eq];
paulson@7826
    84
????*)
paulson@7826
    85
paulson@7365
    86
(**SHOULD NOT BE NECESSARY: The various injections into the system
paulson@7365
    87
   state need to be treated symmetrically or done automatically*)
paulson@7347
    88
Goalw [sysOfClient_def] "inj sysOfClient";
paulson@7347
    89
by (rtac injI 1);
paulson@7347
    90
by (auto_tac (claset() addSDs [inj_sysOfAlloc RS injD]
paulson@7841
    91
		       addSWrapper record_split_wrapper, 
paulson@7841
    92
	      simpset()));
paulson@7347
    93
qed "inj_sysOfClient";
paulson@7347
    94
paulson@7347
    95
Goalw [sysOfClient_def] "surj sysOfClient";
paulson@7347
    96
by (cut_facts_tac [surj_sysOfAlloc] 1);
paulson@7347
    97
by (rewtac surj_def);
paulson@7347
    98
by Auto_tac;
paulson@7347
    99
by (Blast_tac 1);
paulson@7347
   100
qed "surj_sysOfClient";
paulson@7347
   101
paulson@7347
   102
AddIffs [inj_sysOfClient, surj_sysOfClient];
paulson@7347
   103
paulson@7482
   104
Goalw [good_map_def] "good_map sysOfClient";
paulson@7482
   105
by Auto_tac;
paulson@7482
   106
qed "good_map_sysOfClient";
paulson@7689
   107
Addsimps [good_map_sysOfClient];
paulson@6828
   108
paulson@7347
   109
(*MUST BE AUTOMATED: even the statement of such results*)
paulson@7347
   110
Goal "!!s. inv sysOfClient s = \
paulson@7347
   111
\            (client s, \
paulson@7347
   112
\             (| allocGiv = allocGiv s, \
paulson@7347
   113
\                allocAsk = allocAsk s, \
paulson@7347
   114
\                allocRel = allocRel s|) )";
paulson@7347
   115
by (rtac (inj_sysOfClient RS inv_f_eq) 1);
paulson@7399
   116
by (auto_tac (claset() addSWrapper record_split_wrapper, 
paulson@7399
   117
	      simpset() addsimps [sysOfAlloc_def, sysOfClient_def]));
paulson@7365
   118
qed "inv_sysOfClient_eq";
paulson@7689
   119
Addsimps [inv_sysOfClient_eq];
paulson@6837
   120
paulson@6837
   121
paulson@7365
   122
Open_locale "System";
paulson@7365
   123
paulson@7365
   124
val Alloc = thm "Alloc";
paulson@7365
   125
val Client = thm "Client";
paulson@7365
   126
val Network = thm "Network";
paulson@7365
   127
val System_def = thm "System_def";
paulson@7365
   128
paulson@7365
   129
AddIffs [finite_lessThan];
paulson@7365
   130
paulson@7365
   131
(*Client : <unfolded specification> *)
paulson@7365
   132
val Client_Spec =
paulson@7365
   133
    rewrite_rule [client_spec_def, client_increasing_def,
paulson@7365
   134
		  client_bounded_def, client_progress_def] Client;
paulson@7365
   135
paulson@7365
   136
Goal "Client : UNIV guarantees Increasing ask";
paulson@7365
   137
by (cut_facts_tac [Client_Spec] 1);
paulson@7365
   138
by (asm_full_simp_tac (simpset() addsimps [guarantees_Int_right]) 1);
paulson@7365
   139
qed "Client_Increasing_ask";
paulson@7365
   140
paulson@7365
   141
Goal "Client : UNIV guarantees Increasing rel";
paulson@7365
   142
by (cut_facts_tac [Client_Spec] 1);
paulson@7365
   143
by (asm_full_simp_tac (simpset() addsimps [guarantees_Int_right]) 1);
paulson@7365
   144
qed "Client_Increasing_rel";
paulson@7365
   145
paulson@7365
   146
AddIffs [Client_Increasing_ask, Client_Increasing_rel];
paulson@7365
   147
paulson@7365
   148
Goal "Client : UNIV guarantees Always {s. ALL elt : set (ask s). elt <= NbT}";
paulson@7365
   149
by (cut_facts_tac [Client_Spec] 1);
paulson@7365
   150
by Auto_tac;
paulson@7365
   151
qed "Client_Bounded";
paulson@7365
   152
paulson@7365
   153
(*Client_Progress is cumbersome to state*)
paulson@7365
   154
val Client_Progress = Client_Spec RS IntD2;
paulson@6828
   155
paulson@6828
   156
paulson@7365
   157
(*Network : <unfolded specification> *)
paulson@7365
   158
val Network_Spec =
paulson@7365
   159
    rewrite_rule [network_spec_def, network_ask_def,
paulson@7365
   160
		  network_giv_def, network_rel_def] Network;
paulson@7365
   161
paulson@7365
   162
(*CANNOT use bind_thm: it puts the theorem into standard form, in effect
paulson@7365
   163
  exporting it from the locale*)
paulson@7689
   164
val Network_Ask = Network_Spec RS IntD1 RS IntD1 RS INT_D;
paulson@7540
   165
val Network_Giv = Network_Spec RS IntD1 RS IntD2 RS INT_D;
paulson@7365
   166
val Network_Rel = Network_Spec RS IntD2 RS INT_D;
paulson@7365
   167
paulson@7365
   168
paulson@7365
   169
(*Alloc : <unfolded specification> *)
paulson@7365
   170
val Alloc_Spec =
paulson@7365
   171
    rewrite_rule [alloc_spec_def, alloc_increasing_def,
paulson@7365
   172
		  alloc_safety_def, alloc_progress_def] Alloc;
paulson@7365
   173
paulson@7540
   174
Goal "i < Nclients ==> Alloc : UNIV guarantees Increasing (sub i o allocGiv)";
paulson@7365
   175
by (cut_facts_tac [Alloc_Spec] 1);
paulson@7365
   176
by (asm_full_simp_tac (simpset() addsimps [guarantees_INT_right]) 1);
paulson@7365
   177
qed "Alloc_Increasing";
paulson@7365
   178
paulson@7365
   179
val Alloc_Safety = Alloc_Spec RS IntD1 RS IntD2;
paulson@7365
   180
val Alloc_Progress = (Alloc_Spec RS IntD2
paulson@7365
   181
                      |> simplify (simpset() addsimps [guarantees_INT_right]))
paulson@7365
   182
                     RS bspec RS spec;
paulson@7365
   183
		     
paulson@7365
   184
paulson@7347
   185
paulson@7365
   186
(*Not sure what to say about the other components because they involve
paulson@7365
   187
  extend*)
paulson@7399
   188
Goalw [System_def] "Network <= System";
paulson@7365
   189
by (blast_tac (claset() addIs [componentI]) 1);
paulson@7365
   190
qed "Network_component_System";
paulson@7365
   191
paulson@7399
   192
Goalw [System_def] "(extend sysOfAlloc Alloc) <= System";
paulson@7399
   193
by (blast_tac (claset() addIs [componentI]) 1);
paulson@7399
   194
qed "Alloc_component_System";
paulson@7365
   195
paulson@7399
   196
AddIffs [Network_component_System, Alloc_component_System];
paulson@7399
   197
paulson@7365
   198
paulson@7826
   199
fun alloc_export th = good_map_sysOfAlloc RS export th |> simplify (simpset());
paulson@7689
   200
paulson@7826
   201
fun client_export th = good_map_sysOfClient RS export th |> simplify (simpset());
paulson@7689
   202
paulson@7540
   203
(*NEED AUTOMATIC PROPAGATION of Alloc_Increasing*)
paulson@7540
   204
Goal "i < Nclients \
paulson@7540
   205
\ ==> extend sysOfAlloc Alloc : UNIV guarantees Increasing (sub i o allocGiv)";
paulson@7540
   206
by (dtac (Alloc_Increasing RS alloc_export extend_guar_Increasing) 1);
paulson@7540
   207
by (auto_tac (claset(), simpset() addsimps [o_def]));
paulson@7540
   208
qed "extend_Alloc_Increasing_allocGiv";
paulson@7540
   209
paulson@7841
   210
Goalw [System_def]
paulson@7841
   211
     "i < Nclients ==> System : Increasing (sub i o allocGiv)";
paulson@7841
   212
by (rtac (extend_Alloc_Increasing_allocGiv RS 
paulson@7841
   213
	  guarantees_Join_I1 RS guaranteesD) 1);
paulson@7841
   214
by Auto_tac;
paulson@7841
   215
qed "System_Increasing_allocGiv";
paulson@7365
   216
paulson@7841
   217
paulson@7365
   218
paulson@7841
   219
Goalw [System_def]
paulson@7841
   220
     "i < Nclients ==> System : Increasing (ask o sub i o client)";
paulson@7841
   221
by (rtac (client_export extend_guar_Increasing RS guarantees_Join_I2 
paulson@7841
   222
	  RS guaranteesD) 1);
paulson@7841
   223
by (rtac (lift_prog_guar_Increasing RS guarantees_PLam_I) 1);
paulson@7841
   224
by Auto_tac;
paulson@7841
   225
qed "System_Increasing_ask";
paulson@7841
   226
paulson@7365
   227
Goalw [System_def]
paulson@7365
   228
     "i < Nclients ==> System : Increasing (rel o sub i o client)";
paulson@7841
   229
by (rtac (client_export extend_guar_Increasing RS guarantees_Join_I2 
paulson@7689
   230
	  RS guaranteesD) 1);
paulson@7689
   231
by (rtac (lift_prog_guar_Increasing RS guarantees_PLam_I) 1);
paulson@7689
   232
(*gets Client_Increasing_rel from simpset*)
paulson@7689
   233
by Auto_tac;
paulson@7347
   234
qed "System_Increasing_rel";
paulson@6828
   235
paulson@6828
   236
paulson@7841
   237
(** Follows consequences.
paulson@7841
   238
    The "Always (INT ...) formulation expresses the general safety property
paulson@7841
   239
    and allows it to be combined using Always_Int_rule below. **)
paulson@7841
   240
paulson@7841
   241
Goal "System : Always (INT i: lessThan Nclients. \
paulson@7841
   242
\                      {s. (giv o sub i o client) s <= (sub i o allocGiv) s})";
paulson@7841
   243
by (auto_tac (claset(), 
paulson@7841
   244
	      simpset() delsimps [o_apply]
paulson@7841
   245
	                addsimps [Always_INT_distrib, Follows_Bounded,
paulson@7841
   246
				  Network_Giv RS component_guaranteesD,
paulson@7841
   247
	     extend_Alloc_Increasing_allocGiv RS component_guaranteesD]));
paulson@7841
   248
qed "Always_giv_le_allocGiv";
paulson@7841
   249
paulson@7841
   250
Goal "System : Always (INT i: lessThan Nclients. \
paulson@7841
   251
\                      {s. (sub i o allocAsk) s <= (ask o sub i o client) s})";
paulson@7841
   252
by (auto_tac (claset(), 
paulson@7841
   253
	      simpset() delsimps [o_apply]
paulson@7841
   254
	      addsimps [Always_INT_distrib, Follows_Bounded,
paulson@7841
   255
	     [Network_Ask, System_Increasing_ask] MRS component_guaranteesD]));
paulson@7841
   256
qed "Always_allocAsk_le_ask";
paulson@7841
   257
paulson@7841
   258
Goal "System : Always (INT i: lessThan Nclients. \
paulson@7841
   259
\                      {s. (sub i o allocRel) s <= (rel o sub i o client) s})";
paulson@7841
   260
by (auto_tac (claset(), 
paulson@7841
   261
	      simpset() delsimps [o_apply]
paulson@7841
   262
	                addsimps [Always_INT_distrib, Follows_Bounded,
paulson@7841
   263
	     [Network_Rel, System_Increasing_rel] MRS component_guaranteesD]));
paulson@7841
   264
qed "Always_allocRel_le_rel";
paulson@7841
   265
paulson@7841
   266
paulson@7841
   267
(*** Proof of the safety property (1) ***)
paulson@7841
   268
paulson@7841
   269
(*safety (1), step 1 is System_Increasing_rel*)
paulson@7841
   270
paulson@7689
   271
(*safety (1), step 2*)
paulson@7365
   272
Goal "i < Nclients ==> System : Increasing (sub i o allocRel)";
paulson@7365
   273
by (rtac Follows_Increasing1 1);
paulson@7365
   274
by (blast_tac (claset() addIs [Network_Rel RS component_guaranteesD,
paulson@7540
   275
			       System_Increasing_rel]) 1);
paulson@7365
   276
qed "System_Increasing_allocRel";
paulson@6828
   277
paulson@7826
   278
paulson@7826
   279
paulson@7689
   280
(*safety (1), step 3*)
paulson@7399
   281
Goal "System : Always {s. sum (%i. (tokens o sub i o allocGiv) s) Nclients \
paulson@7399
   282
\                  <= NbT + sum (%i. (tokens o sub i o allocRel) s) Nclients}";
paulson@7399
   283
by (res_inst_tac 
paulson@7537
   284
    [("X", "(INT i : lessThan Nclients. Increasing (sub i o allocRel))")] 
paulson@7537
   285
    component_guaranteesD 1);
paulson@7482
   286
by (rtac Alloc_component_System 3);
paulson@7537
   287
by (force_tac (claset(), simpset() addsimps [System_Increasing_allocRel]) 2);
paulson@7538
   288
by (rtac (Alloc_Safety RS project_guarantees) 1);
paulson@7826
   289
(*1: Increasing precondition*)
paulson@7841
   290
by (rtac (alloc_export projecting_Increasing RS projecting_weaken RS 
paulson@7841
   291
	  projecting_INT) 1);
paulson@7537
   292
by Auto_tac;
paulson@7826
   293
by (asm_full_simp_tac (simpset() addsimps [o_def]) 1);
paulson@7538
   294
(*2: Always postcondition*)
paulson@7826
   295
by (rtac ((alloc_export extending_Always RS extending_weaken)) 1);
paulson@7826
   296
by Auto_tac;
paulson@7538
   297
by (asm_full_simp_tac
paulson@7538
   298
     (simpset() addsimps [alloc_export Collect_eq_extend_set RS sym]) 1);
paulson@7538
   299
qed "System_sum_bounded";
paulson@7537
   300
paulson@7841
   301
(** Follows reasoning **)
paulson@7841
   302
paulson@7540
   303
Goal "System : Always (INT i: lessThan Nclients. \
paulson@7540
   304
\                         {s. (tokens o giv o sub i o client) s \
paulson@7540
   305
\                          <= (tokens o sub i o allocGiv) s})";
paulson@7841
   306
by (rtac (Always_giv_le_allocGiv RS Always_weaken) 1);
paulson@7841
   307
by (auto_tac (claset() addIs [tokens_mono_prefix], simpset()));
paulson@7841
   308
qed "Always_tokens_giv_le_allocGiv";
paulson@7540
   309
paulson@7540
   310
Goal "System : Always (INT i: lessThan Nclients. \
paulson@7540
   311
\                         {s. (tokens o sub i o allocRel) s \
paulson@7540
   312
\                          <= (tokens o rel o sub i o client) s})";
paulson@7841
   313
by (rtac (Always_allocRel_le_rel RS Always_weaken) 1);
paulson@7841
   314
by (auto_tac (claset() addIs [tokens_mono_prefix], simpset()));
paulson@7841
   315
qed "Always_tokens_allocRel_le_rel";
paulson@7540
   316
paulson@7841
   317
(*safety (1), step 4 (final result!) *)
paulson@7540
   318
Goal "System : Always {s. sum (%i. (tokens o giv o sub i o client)s) Nclients \
paulson@7540
   319
\              <= NbT + sum (%i. (tokens o rel o sub i o client)s) Nclients}";
paulson@7841
   320
by (rtac (Always_Int_rule [System_sum_bounded, Always_tokens_giv_le_allocGiv, 
paulson@7841
   321
			   Always_tokens_allocRel_le_rel] RS Always_weaken) 1);
paulson@7538
   322
by Auto_tac;
paulson@7540
   323
by (rtac (sum_mono RS order_trans) 1);
paulson@7540
   324
by (dtac order_trans 2);
paulson@7540
   325
by (rtac ([order_refl, sum_mono] MRS add_le_mono) 2);
paulson@7540
   326
by (assume_tac 3);
paulson@7482
   327
by Auto_tac;
paulson@7540
   328
qed "System_safety";
paulson@7399
   329
paulson@7689
   330
paulson@7689
   331
paulson@7689
   332
(*** Proof of the progress property (2) ***)
paulson@7689
   333
paulson@7689
   334
(*we begin with proofs identical to System_Increasing_rel and
paulson@7689
   335
  System_Increasing_allocRel: tactics needed!*)
paulson@7689
   336
paulson@7841
   337
(*progress (2), step 1 is System_Increasing_ask and System_Increasing_rel*)
paulson@7689
   338
paulson@7841
   339
(*progress (2), step 2; see also System_Increasing_allocRel*)
paulson@7689
   340
Goal "i < Nclients ==> System : Increasing (sub i o allocAsk)";
paulson@7689
   341
by (rtac Follows_Increasing1 1);
paulson@7689
   342
by (blast_tac (claset() addIs [Network_Ask RS component_guaranteesD,
paulson@7689
   343
			       System_Increasing_ask]) 1);
paulson@7689
   344
qed "System_Increasing_allocAsk";
paulson@7689
   345
paulson@7841
   346
val Client_i_Bounded =
paulson@7841
   347
    [Client_Bounded, projecting_UNIV, lift_export extending_Always] 
paulson@7841
   348
    MRS drop_prog_guarantees;
paulson@7841
   349
paulson@7841
   350
val UNIV_guar_Always =
paulson@7841
   351
    [asm_rl, projecting_UNIV, extending_Always] 
paulson@7841
   352
    MRS project_guarantees;
paulson@7841
   353
paulson@7841
   354
paulson@7689
   355
(*progress (2), step 3*)
paulson@7841
   356
(*All this trouble just to lift "Client_Bounded" through two extend ops*)
paulson@7689
   357
Goalw [System_def]
paulson@7689
   358
     "i < Nclients \
paulson@7689
   359
\   ==> System : Always \
paulson@7689
   360
\                 {s. ALL elt : set ((ask o sub i o client) s). elt <= NbT}";
paulson@7841
   361
by (rtac (guarantees_PLam_I RS client_export UNIV_guar_Always RS
paulson@7689
   362
	  guarantees_Join_I2 RS guaranteesD RS Always_weaken) 1);
paulson@7841
   363
by (rtac Client_i_Bounded 1);
paulson@7689
   364
by (auto_tac(claset(),
paulson@7841
   365
	 simpset() addsimps [lift_export Collect_eq_extend_set RS sym,
paulson@7689
   366
			     client_export Collect_eq_extend_set RS sym]));
paulson@7841
   367
qed "System_Bounded_ask";
paulson@7841
   368
paulson@7841
   369
(*progress (2), step 4*)
paulson@7841
   370
Goal "System : Always {s. ALL i : lessThan Nclients. \
paulson@7841
   371
\                          ALL elt : set ((sub i o allocAsk) s). elt <= NbT}";
paulson@7841
   372
by (auto_tac (claset(), 
paulson@7841
   373
	      simpset() addsimps [Collect_ball_eq, Always_INT_distrib]));
paulson@7841
   374
by (rtac (Always_Int_rule [Always_allocAsk_le_ask, System_Bounded_ask] 
paulson@7841
   375
    RS Always_weaken) 1);
paulson@7841
   376
by (auto_tac(claset() addDs [set_mono], simpset()));
paulson@7841
   377
qed "System_Bounded_allocAsk";
paulson@7841
   378
paulson@7841
   379
(*progress (2), step 5*)
paulson@7841
   380
paulson@7841
   381
Goal "i < Nclients ==> System : Increasing (giv o sub i o client)";
paulson@7841
   382
by (rtac Follows_Increasing1 1);
paulson@7841
   383
by (blast_tac (claset() addIs [Network_Giv RS component_guaranteesD,
paulson@7841
   384
			       System_Increasing_allocGiv]) 1);
paulson@7841
   385
qed "System_Increasing_giv";
paulson@7841
   386
paulson@7841
   387
(*progress (2), step 6*)
paulson@7841
   388
paulson@7841
   389
(*A LOT of work just to lift "Client_Progress" to the array*)
paulson@7841
   390
Goal "lift_prog i Client \
paulson@7841
   391
\  : Increasing (giv o sub i) Int ((%z. z i) localTo (lift_prog i Client)) \
paulson@7841
   392
\    guarantees \
paulson@7841
   393
\    (INT h. {s. h <=  (giv o sub i) s & \
paulson@7841
   394
\                       h pfixGe (ask o sub i) s}  \
paulson@7841
   395
\            LeadsTo {s. tokens h <= (tokens o rel o sub i) s})";
paulson@7841
   396
br (Client_Progress RS drop_prog_guarantees) 1;
paulson@7841
   397
br (lift_export extending_LeadsTo RS extending_weaken RS extending_INT) 2;
paulson@7841
   398
br subset_refl 4;
paulson@7841
   399
by (simp_tac (simpset()addsimps [lift_export Collect_eq_extend_set RS sym]) 3);
paulson@7841
   400
by (force_tac (claset(), simpset() addsimps [lift_prog_correct]) 2);
paulson@7841
   401
by (rtac (lift_export projecting_Increasing RS projecting_weaken) 1);
paulson@7841
   402
by (auto_tac (claset(), simpset() addsimps [o_def]));
paulson@7841
   403
qed "Client_i_Progress";
paulson@7841
   404
paulson@7841
   405
Goalw [System_def]
paulson@7841
   406
     "i < Nclients \
paulson@7841
   407
\ ==> System : (INT h. {s. h <=  (giv o sub i o client) s & \
paulson@7841
   408
\                       h pfixGe (ask o sub i o client) s}  \
paulson@7841
   409
\            LeadsTo {s. tokens h <= (tokens o rel o sub i o client) s})";
paulson@7841
   410
by (rtac (guarantees_Join_I2 RS guaranteesD) 1);
paulson@7841
   411
br (guarantees_PLam_I RS project_guarantees) 1;
paulson@7841
   412
br Client_i_Progress  1;
paulson@7841
   413
by (Force_tac 1);
paulson@7841
   414
br (client_export extending_LeadsTo RS extending_weaken RS extending_INT) 2;
paulson@7841
   415
br subset_refl 4;
paulson@7841
   416
by (simp_tac (simpset()addsimps [client_export Collect_eq_extend_set RS sym]) 3);
paulson@7841
   417
br projecting_Int 1;
paulson@7841
   418
br (client_export projecting_Increasing) 1;
paulson@7841
   419
br (client_export projecting_localTo) 1;
paulson@7841
   420
paulson@7841
   421
by (simp_tac (simpset()addsimps [lift_prog_correct]) 1);
paulson@7841
   422
paulson@7841
   423
by (rtac (client_export ) 1);
paulson@7841
   424
paulson@7841
   425
Client_Progress;