1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/HOL/UNITY/Comp/Alloc.ML Mon Mar 05 15:32:54 2001 +0100
1.3 @@ -0,0 +1,744 @@
1.4 +(* Title: HOL/UNITY/Alloc
1.5 + ID: $Id$
1.6 + Author: Lawrence C Paulson, Cambridge University Computer Laboratory
1.7 + Copyright 1998 University of Cambridge
1.8 +
1.9 +Specification of Chandy and Charpentier's Allocator
1.10 +*)
1.11 +
1.12 +(*Perhaps equalities.ML shouldn't add this in the first place!*)
1.13 +Delsimps [image_Collect];
1.14 +
1.15 +AddIs [impOfSubs subset_preserves_o];
1.16 +Addsimps [impOfSubs subset_preserves_o];
1.17 +Addsimps [funPair_o_distrib];
1.18 +Addsimps [Always_INT_distrib];
1.19 +Delsimps [o_apply];
1.20 +
1.21 +(*Eliminate the "o" operator*)
1.22 +val o_simp = simplify (simpset() addsimps [o_def]);
1.23 +
1.24 +(*For rewriting of specifications related by "guarantees"*)
1.25 +Addsimps [rename_image_constrains, rename_image_stable,
1.26 + rename_image_increasing, rename_image_invariant,
1.27 + rename_image_Constrains, rename_image_Stable,
1.28 + rename_image_Increasing, rename_image_Always,
1.29 + rename_image_leadsTo, rename_image_LeadsTo,
1.30 + rename_preserves, rename_image_preserves, lift_image_preserves,
1.31 + bij_image_INT, bij_is_inj RS image_Int, bij_image_Collect_eq];
1.32 +
1.33 +(*Splits up conjunctions & intersections: like CONJUNCTS in the HOL system*)
1.34 +fun list_of_Int th =
1.35 + (list_of_Int (th RS conjunct1) @ list_of_Int (th RS conjunct2))
1.36 + handle THM _ => (list_of_Int (th RS IntD1) @ list_of_Int (th RS IntD2))
1.37 + handle THM _ => (list_of_Int (th RS INT_D))
1.38 + handle THM _ => (list_of_Int (th RS bspec))
1.39 + handle THM _ => [th];
1.40 +
1.41 +(*Used just once, for Alloc_Increasing*)
1.42 +val lessThanBspec = lessThan_iff RS iffD2 RSN (2, bspec);
1.43 +fun normalize th =
1.44 + normalize (th RS spec
1.45 + handle THM _ => th RS lessThanBspec
1.46 + handle THM _ => th RS bspec
1.47 + handle THM _ => th RS (guarantees_INT_right_iff RS iffD1))
1.48 + handle THM _ => th;
1.49 +
1.50 +
1.51 +
1.52 +(*** bijectivity of sysOfAlloc [MUST BE AUTOMATED] ***)
1.53 +
1.54 +val record_auto_tac =
1.55 + auto_tac (claset() addIs [ext] addSWrapper record_split_wrapper,
1.56 + simpset() addsimps [sysOfAlloc_def, sysOfClient_def,
1.57 + client_map_def, non_dummy_def, funPair_def,
1.58 + o_apply, Let_def]);
1.59 +
1.60 +
1.61 +Goalw [sysOfAlloc_def, Let_def] "inj sysOfAlloc";
1.62 +by (rtac injI 1);
1.63 +by record_auto_tac;
1.64 +qed "inj_sysOfAlloc";
1.65 +AddIffs [inj_sysOfAlloc];
1.66 +
1.67 +(*We need the inverse; also having it simplifies the proof of surjectivity*)
1.68 +Goal "!!s. inv sysOfAlloc s = \
1.69 +\ (| allocGiv = allocGiv s, \
1.70 +\ allocAsk = allocAsk s, \
1.71 +\ allocRel = allocRel s, \
1.72 +\ allocState_d.dummy = (client s, dummy s) |)";
1.73 +by (rtac (inj_sysOfAlloc RS inv_f_eq) 1);
1.74 +by record_auto_tac;
1.75 +qed "inv_sysOfAlloc_eq";
1.76 +Addsimps [inv_sysOfAlloc_eq];
1.77 +
1.78 +Goal "surj sysOfAlloc";
1.79 +by (simp_tac (simpset() addsimps [surj_iff, expand_fun_eq, o_apply]) 1);
1.80 +by record_auto_tac;
1.81 +qed "surj_sysOfAlloc";
1.82 +AddIffs [surj_sysOfAlloc];
1.83 +
1.84 +Goal "bij sysOfAlloc";
1.85 +by (blast_tac (claset() addIs [bijI]) 1);
1.86 +qed "bij_sysOfAlloc";
1.87 +AddIffs [bij_sysOfAlloc];
1.88 +
1.89 +
1.90 +(*** bijectivity of sysOfClient ***)
1.91 +
1.92 +Goalw [sysOfClient_def] "inj sysOfClient";
1.93 +by (rtac injI 1);
1.94 +by record_auto_tac;
1.95 +qed "inj_sysOfClient";
1.96 +AddIffs [inj_sysOfClient];
1.97 +
1.98 +Goal "!!s. inv sysOfClient s = \
1.99 +\ (client s, \
1.100 +\ (| allocGiv = allocGiv s, \
1.101 +\ allocAsk = allocAsk s, \
1.102 +\ allocRel = allocRel s, \
1.103 +\ allocState_d.dummy = systemState.dummy s|) )";
1.104 +by (rtac (inj_sysOfClient RS inv_f_eq) 1);
1.105 +by record_auto_tac;
1.106 +qed "inv_sysOfClient_eq";
1.107 +Addsimps [inv_sysOfClient_eq];
1.108 +
1.109 +Goal "surj sysOfClient";
1.110 +by (simp_tac (simpset() addsimps [surj_iff, expand_fun_eq, o_apply]) 1);
1.111 +by record_auto_tac;
1.112 +qed "surj_sysOfClient";
1.113 +AddIffs [surj_sysOfClient];
1.114 +
1.115 +Goal "bij sysOfClient";
1.116 +by (blast_tac (claset() addIs [bijI]) 1);
1.117 +qed "bij_sysOfClient";
1.118 +AddIffs [bij_sysOfClient];
1.119 +
1.120 +
1.121 +(*** bijectivity of client_map ***)
1.122 +
1.123 +Goalw [inj_on_def] "inj client_map";
1.124 +by record_auto_tac;
1.125 +qed "inj_client_map";
1.126 +AddIffs [inj_client_map];
1.127 +
1.128 +Goal "!!s. inv client_map s = \
1.129 +\ (%(x,y).(|giv = giv x, ask = ask x, rel = rel x, \
1.130 +\ clientState_d.dummy = y|)) s";
1.131 +by (rtac (inj_client_map RS inv_f_eq) 1);
1.132 +by record_auto_tac;
1.133 +qed "inv_client_map_eq";
1.134 +Addsimps [inv_client_map_eq];
1.135 +
1.136 +Goal "surj client_map";
1.137 +by (simp_tac (simpset() addsimps [surj_iff, expand_fun_eq, o_apply]) 1);
1.138 +by record_auto_tac;
1.139 +qed "surj_client_map";
1.140 +AddIffs [surj_client_map];
1.141 +
1.142 +Goal "bij client_map";
1.143 +by (blast_tac (claset() addIs [bijI]) 1);
1.144 +qed "bij_client_map";
1.145 +AddIffs [bij_client_map];
1.146 +
1.147 +
1.148 +(** o-simprules for client_map **)
1.149 +
1.150 +Goalw [client_map_def] "fst o client_map = non_dummy";
1.151 +by (rtac fst_o_funPair 1);
1.152 +qed "fst_o_client_map";
1.153 +Addsimps (make_o_equivs fst_o_client_map);
1.154 +
1.155 +Goalw [client_map_def] "snd o client_map = clientState_d.dummy";
1.156 +by (rtac snd_o_funPair 1);
1.157 +qed "snd_o_client_map";
1.158 +Addsimps (make_o_equivs snd_o_client_map);
1.159 +
1.160 +(** o-simprules for sysOfAlloc [MUST BE AUTOMATED] **)
1.161 +
1.162 +Goal "client o sysOfAlloc = fst o allocState_d.dummy ";
1.163 +by record_auto_tac;
1.164 +qed "client_o_sysOfAlloc";
1.165 +Addsimps (make_o_equivs client_o_sysOfAlloc);
1.166 +
1.167 +Goal "allocGiv o sysOfAlloc = allocGiv";
1.168 +by record_auto_tac;
1.169 +qed "allocGiv_o_sysOfAlloc_eq";
1.170 +Addsimps (make_o_equivs allocGiv_o_sysOfAlloc_eq);
1.171 +
1.172 +Goal "allocAsk o sysOfAlloc = allocAsk";
1.173 +by record_auto_tac;
1.174 +qed "allocAsk_o_sysOfAlloc_eq";
1.175 +Addsimps (make_o_equivs allocAsk_o_sysOfAlloc_eq);
1.176 +
1.177 +Goal "allocRel o sysOfAlloc = allocRel";
1.178 +by record_auto_tac;
1.179 +qed "allocRel_o_sysOfAlloc_eq";
1.180 +Addsimps (make_o_equivs allocRel_o_sysOfAlloc_eq);
1.181 +
1.182 +(** o-simprules for sysOfClient [MUST BE AUTOMATED] **)
1.183 +
1.184 +Goal "client o sysOfClient = fst";
1.185 +by record_auto_tac;
1.186 +qed "client_o_sysOfClient";
1.187 +Addsimps (make_o_equivs client_o_sysOfClient);
1.188 +
1.189 +Goal "allocGiv o sysOfClient = allocGiv o snd ";
1.190 +by record_auto_tac;
1.191 +qed "allocGiv_o_sysOfClient_eq";
1.192 +Addsimps (make_o_equivs allocGiv_o_sysOfClient_eq);
1.193 +
1.194 +Goal "allocAsk o sysOfClient = allocAsk o snd ";
1.195 +by record_auto_tac;
1.196 +qed "allocAsk_o_sysOfClient_eq";
1.197 +Addsimps (make_o_equivs allocAsk_o_sysOfClient_eq);
1.198 +
1.199 +Goal "allocRel o sysOfClient = allocRel o snd ";
1.200 +by record_auto_tac;
1.201 +qed "allocRel_o_sysOfClient_eq";
1.202 +Addsimps (make_o_equivs allocRel_o_sysOfClient_eq);
1.203 +
1.204 +Goal "allocGiv o inv sysOfAlloc = allocGiv";
1.205 +by (simp_tac (simpset() addsimps [o_def]) 1);
1.206 +qed "allocGiv_o_inv_sysOfAlloc_eq";
1.207 +Addsimps (make_o_equivs allocGiv_o_inv_sysOfAlloc_eq);
1.208 +
1.209 +Goal "allocAsk o inv sysOfAlloc = allocAsk";
1.210 +by (simp_tac (simpset() addsimps [o_def]) 1);
1.211 +qed "allocAsk_o_inv_sysOfAlloc_eq";
1.212 +Addsimps (make_o_equivs allocAsk_o_inv_sysOfAlloc_eq);
1.213 +
1.214 +Goal "allocRel o inv sysOfAlloc = allocRel";
1.215 +by (simp_tac (simpset() addsimps [o_def]) 1);
1.216 +qed "allocRel_o_inv_sysOfAlloc_eq";
1.217 +Addsimps (make_o_equivs allocRel_o_inv_sysOfAlloc_eq);
1.218 +
1.219 +Goal "(rel o inv client_map o drop_map i o inv sysOfClient) = \
1.220 +\ rel o sub i o client";
1.221 +by (simp_tac (simpset() addsimps [o_def, drop_map_def]) 1);
1.222 +qed "rel_inv_client_map_drop_map";
1.223 +Addsimps (make_o_equivs rel_inv_client_map_drop_map);
1.224 +
1.225 +Goal "(ask o inv client_map o drop_map i o inv sysOfClient) = \
1.226 +\ ask o sub i o client";
1.227 +by (simp_tac (simpset() addsimps [o_def, drop_map_def]) 1);
1.228 +qed "ask_inv_client_map_drop_map";
1.229 +Addsimps (make_o_equivs ask_inv_client_map_drop_map);
1.230 +
1.231 +(**
1.232 +Open_locale "System";
1.233 +
1.234 +val Alloc = thm "Alloc";
1.235 +val Client = thm "Client";
1.236 +val Network = thm "Network";
1.237 +val System_def = thm "System_def";
1.238 +
1.239 +CANNOT use bind_thm: it puts the theorem into standard form, in effect
1.240 + exporting it from the locale
1.241 +**)
1.242 +
1.243 +AddIffs [finite_lessThan];
1.244 +
1.245 +(*Client : <unfolded specification> *)
1.246 +val client_spec_simps =
1.247 + [client_spec_def, client_increasing_def, client_bounded_def,
1.248 + client_progress_def, client_allowed_acts_def, client_preserves_def,
1.249 + guarantees_Int_right];
1.250 +
1.251 +val [Client_Increasing_ask, Client_Increasing_rel,
1.252 + Client_Bounded, Client_Progress, Client_AllowedActs,
1.253 + Client_preserves_giv, Client_preserves_dummy] =
1.254 + Client |> simplify (simpset() addsimps client_spec_simps)
1.255 + |> list_of_Int;
1.256 +
1.257 +AddIffs [Client_Increasing_ask, Client_Increasing_rel, Client_Bounded,
1.258 + Client_preserves_giv, Client_preserves_dummy];
1.259 +
1.260 +
1.261 +(*Network : <unfolded specification> *)
1.262 +val network_spec_simps =
1.263 + [network_spec_def, network_ask_def, network_giv_def,
1.264 + network_rel_def, network_allowed_acts_def, network_preserves_def,
1.265 + ball_conj_distrib];
1.266 +
1.267 +val [Network_Ask, Network_Giv, Network_Rel, Network_AllowedActs,
1.268 + Network_preserves_allocGiv, Network_preserves_rel,
1.269 + Network_preserves_ask] =
1.270 + Network |> simplify (simpset() addsimps network_spec_simps)
1.271 + |> list_of_Int;
1.272 +
1.273 +AddIffs [Network_preserves_allocGiv];
1.274 +
1.275 +Addsimps [Network_preserves_rel, Network_preserves_ask];
1.276 +Addsimps [o_simp Network_preserves_rel, o_simp Network_preserves_ask];
1.277 +
1.278 +
1.279 +(*Alloc : <unfolded specification> *)
1.280 +val alloc_spec_simps =
1.281 + [alloc_spec_def, alloc_increasing_def, alloc_safety_def,
1.282 + alloc_progress_def, alloc_allowed_acts_def,
1.283 + alloc_preserves_def];
1.284 +
1.285 +val [Alloc_Increasing_0, Alloc_Safety, Alloc_Progress, Alloc_AllowedActs,
1.286 + Alloc_preserves_allocRel, Alloc_preserves_allocAsk,
1.287 + Alloc_preserves_dummy] =
1.288 + Alloc |> simplify (simpset() addsimps alloc_spec_simps)
1.289 + |> list_of_Int;
1.290 +
1.291 +(*Strip off the INT in the guarantees postcondition*)
1.292 +val Alloc_Increasing = normalize Alloc_Increasing_0;
1.293 +
1.294 +AddIffs [Alloc_preserves_allocRel, Alloc_preserves_allocAsk,
1.295 + Alloc_preserves_dummy];
1.296 +
1.297 +(** Components lemmas [MUST BE AUTOMATED] **)
1.298 +
1.299 +Goal "Network Join \
1.300 +\ ((rename sysOfClient \
1.301 +\ (plam x: (lessThan Nclients). rename client_map Client)) Join \
1.302 +\ rename sysOfAlloc Alloc) \
1.303 +\ = System";
1.304 +by (simp_tac (simpset() addsimps System_def::Join_ac) 1);
1.305 +qed "Network_component_System";
1.306 +
1.307 +Goal "(rename sysOfClient \
1.308 +\ (plam x: (lessThan Nclients). rename client_map Client)) Join \
1.309 +\ (Network Join rename sysOfAlloc Alloc) = System";
1.310 +by (simp_tac (simpset() addsimps System_def::Join_ac) 1);
1.311 +qed "Client_component_System";
1.312 +
1.313 +Goal "rename sysOfAlloc Alloc Join \
1.314 +\ ((rename sysOfClient (plam x: (lessThan Nclients). rename client_map Client)) Join \
1.315 +\ Network) = System";
1.316 +by (simp_tac (simpset() addsimps System_def::Join_ac) 1);
1.317 +qed "Alloc_component_System";
1.318 +
1.319 +AddIffs [Client_component_System, Network_component_System,
1.320 + Alloc_component_System];
1.321 +
1.322 +(** These preservation laws should be generated automatically **)
1.323 +
1.324 +Goal "Allowed Client = preserves rel Int preserves ask";
1.325 +by (auto_tac (claset(),
1.326 + simpset() addsimps [Allowed_def, Client_AllowedActs,
1.327 + safety_prop_Acts_iff]));
1.328 +qed "Client_Allowed";
1.329 +Addsimps [Client_Allowed];
1.330 +
1.331 +Goal "Allowed Network = \
1.332 +\ preserves allocRel Int \
1.333 +\ (INT i: lessThan Nclients. preserves(giv o sub i o client))";
1.334 +by (auto_tac (claset(),
1.335 + simpset() addsimps [Allowed_def, Network_AllowedActs,
1.336 + safety_prop_Acts_iff]));
1.337 +qed "Network_Allowed";
1.338 +Addsimps [Network_Allowed];
1.339 +
1.340 +Goal "Allowed Alloc = preserves allocGiv";
1.341 +by (auto_tac (claset(),
1.342 + simpset() addsimps [Allowed_def, Alloc_AllowedActs,
1.343 + safety_prop_Acts_iff]));
1.344 +qed "Alloc_Allowed";
1.345 +Addsimps [Alloc_Allowed];
1.346 +
1.347 +Goal "OK I (%i. lift i (rename client_map Client))";
1.348 +by (rtac OK_lift_I 1);
1.349 +by Auto_tac;
1.350 +by (dres_inst_tac [("w1", "rel")] (impOfSubs subset_preserves_o) 1);
1.351 +by (dres_inst_tac [("w1", "ask")] (impOfSubs subset_preserves_o) 2);
1.352 +by (auto_tac (claset(), simpset() addsimps [o_def, split_def]));
1.353 +qed "OK_lift_rename_Client";
1.354 +Addsimps [OK_lift_rename_Client]; (*needed in rename_client_map_tac*
1.355 +
1.356 +(*The proofs of rename_Client_Increasing, rename_Client_Bounded and
1.357 + rename_Client_Progress are similar. All require copying out the original
1.358 + Client property. A forward proof can be constructed as follows:
1.359 +
1.360 + Client_Increasing_ask RS
1.361 + (bij_client_map RS rename_rename_guarantees_eq RS iffD2)
1.362 + RS (lift_lift_guarantees_eq RS iffD2)
1.363 + RS guarantees_PLam_I
1.364 + RS (bij_sysOfClient RS rename_rename_guarantees_eq RS iffD2)
1.365 + |> simplify (simpset() addsimps [lift_image_eq_rename, o_def, split_def,
1.366 + surj_rename RS surj_range]);
1.367 +
1.368 +However, the "preserves" property remains to be discharged, and the unfolding
1.369 +of "o" and "sub" complicates subsequent reasoning.
1.370 +
1.371 +The following tactic works for all three proofs, though it certainly looks
1.372 +ad-hoc!
1.373 +*)
1.374 +val rename_client_map_tac =
1.375 + EVERY [
1.376 + simp_tac (simpset() addsimps [rename_guarantees_eq_rename_inv]) 1,
1.377 + rtac guarantees_PLam_I 1,
1.378 + assume_tac 2,
1.379 + (*preserves: routine reasoning*)
1.380 + asm_simp_tac (simpset() addsimps [lift_preserves_sub]) 2,
1.381 + (*the guarantee for "lift i (rename client_map Client)" *)
1.382 + asm_simp_tac
1.383 + (simpset() addsimps [lift_guarantees_eq_lift_inv,
1.384 + rename_guarantees_eq_rename_inv,
1.385 + bij_imp_bij_inv, surj_rename RS surj_range,
1.386 + inv_inv_eq]) 1,
1.387 + asm_simp_tac
1.388 + (simpset() addsimps [o_def, non_dummy_def, guarantees_Int_right]) 1];
1.389 +
1.390 +
1.391 +(*Lifting Client_Increasing to systemState*)
1.392 +Goal "i : I \
1.393 +\ ==> rename sysOfClient (plam x: I. rename client_map Client) : \
1.394 +\ UNIV guarantees \
1.395 +\ Increasing (ask o sub i o client) Int \
1.396 +\ Increasing (rel o sub i o client)";
1.397 +by rename_client_map_tac;
1.398 +qed "rename_Client_Increasing";
1.399 +
1.400 +Goal "[| F : preserves w; i ~= j |] \
1.401 +\ ==> F : preserves (sub i o fst o lift_map j o funPair v w)";
1.402 +by (auto_tac (claset(),
1.403 + simpset() addsimps [lift_map_def, split_def, linorder_neq_iff, o_def]));
1.404 +by (ALLGOALS (dtac (impOfSubs subset_preserves_o)));
1.405 +by (auto_tac (claset(), simpset() addsimps [o_def]));
1.406 +qed "preserves_sub_fst_lift_map";
1.407 +
1.408 +Goal "[| i < Nclients; j < Nclients |] \
1.409 +\ ==> Client : preserves (giv o sub i o fst o lift_map j o client_map)";
1.410 +by (case_tac "i=j" 1);
1.411 +by (asm_full_simp_tac (simpset() addsimps [o_def, non_dummy_def]) 1);
1.412 +by (dtac (Client_preserves_dummy RS preserves_sub_fst_lift_map) 1);
1.413 +by (ALLGOALS (dtac (impOfSubs subset_preserves_o)));
1.414 +by (asm_full_simp_tac (simpset() addsimps [o_def, client_map_def]) 1);
1.415 +qed "client_preserves_giv_oo_client_map";
1.416 +
1.417 +Goal "rename sysOfClient (plam x: lessThan Nclients. rename client_map Client)\
1.418 +\ ok Network";
1.419 +by (auto_tac (claset(), simpset() addsimps [ok_iff_Allowed,
1.420 + client_preserves_giv_oo_client_map]));
1.421 +qed "rename_sysOfClient_ok_Network";
1.422 +
1.423 +Goal "rename sysOfClient (plam x: lessThan Nclients. rename client_map Client)\
1.424 +\ ok rename sysOfAlloc Alloc";
1.425 +by (simp_tac (simpset() addsimps [ok_iff_Allowed]) 1);
1.426 +qed "rename_sysOfClient_ok_Alloc";
1.427 +
1.428 +Goal "rename sysOfAlloc Alloc ok Network";
1.429 +by (simp_tac (simpset() addsimps [ok_iff_Allowed]) 1);
1.430 +qed "rename_sysOfAlloc_ok_Network";
1.431 +
1.432 +AddIffs [rename_sysOfClient_ok_Network, rename_sysOfClient_ok_Alloc,
1.433 + rename_sysOfAlloc_ok_Network];
1.434 +
1.435 +(*The "ok" laws, re-oriented*)
1.436 +AddIffs [rename_sysOfClient_ok_Network RS ok_sym,
1.437 + rename_sysOfClient_ok_Alloc RS ok_sym,
1.438 + rename_sysOfAlloc_ok_Network RS ok_sym];
1.439 +
1.440 +Goal "i < Nclients \
1.441 +\ ==> System : Increasing (ask o sub i o client) Int \
1.442 +\ Increasing (rel o sub i o client)";
1.443 +by (rtac ([rename_Client_Increasing,
1.444 + Client_component_System] MRS component_guaranteesD) 1);
1.445 +by Auto_tac;
1.446 +qed "System_Increasing";
1.447 +
1.448 +bind_thm ("rename_guarantees_sysOfAlloc_I",
1.449 + bij_sysOfAlloc RS rename_rename_guarantees_eq RS iffD2);
1.450 +
1.451 +
1.452 +(*Lifting Alloc_Increasing up to the level of systemState*)
1.453 +val rename_Alloc_Increasing =
1.454 + Alloc_Increasing RS rename_guarantees_sysOfAlloc_I
1.455 + |> simplify (simpset() addsimps [surj_rename RS surj_range, o_def]);
1.456 +
1.457 +Goalw [System_def]
1.458 + "i < Nclients ==> System : Increasing (sub i o allocGiv)";
1.459 +by (simp_tac (simpset() addsimps [o_def]) 1);
1.460 +by (rtac (rename_Alloc_Increasing RS guarantees_Join_I1 RS guaranteesD) 1);
1.461 +by Auto_tac;
1.462 +qed "System_Increasing_allocGiv";
1.463 +
1.464 +AddSIs (list_of_Int System_Increasing);
1.465 +
1.466 +(** Follows consequences.
1.467 + The "Always (INT ...) formulation expresses the general safety property
1.468 + and allows it to be combined using Always_Int_rule below. **)
1.469 +
1.470 +Goal
1.471 + "i < Nclients ==> System : ((sub i o allocRel) Fols (rel o sub i o client))";
1.472 +by (auto_tac (claset() addSIs [Network_Rel RS component_guaranteesD],
1.473 + simpset()));
1.474 +qed "System_Follows_rel";
1.475 +
1.476 +Goal
1.477 + "i < Nclients ==> System : ((sub i o allocAsk) Fols (ask o sub i o client))";
1.478 +by (auto_tac (claset() addSIs [Network_Ask RS component_guaranteesD],
1.479 + simpset()));
1.480 +qed "System_Follows_ask";
1.481 +
1.482 +Goal
1.483 + "i < Nclients ==> System : (giv o sub i o client) Fols (sub i o allocGiv)";
1.484 +by (auto_tac (claset() addSIs [Network_Giv RS component_guaranteesD,
1.485 + rename_Alloc_Increasing RS component_guaranteesD],
1.486 + simpset()));
1.487 +by (ALLGOALS (simp_tac (simpset() addsimps [o_def, non_dummy_def])));
1.488 +by (auto_tac
1.489 + (claset() addSIs [rename_Alloc_Increasing RS component_guaranteesD],
1.490 + simpset()));
1.491 +qed "System_Follows_allocGiv";
1.492 +
1.493 +Goal "System : Always (INT i: lessThan Nclients. \
1.494 +\ {s. (giv o sub i o client) s <= (sub i o allocGiv) s})";
1.495 +by Auto_tac;
1.496 +by (etac (System_Follows_allocGiv RS Follows_Bounded) 1);
1.497 +qed "Always_giv_le_allocGiv";
1.498 +
1.499 +Goal "System : Always (INT i: lessThan Nclients. \
1.500 +\ {s. (sub i o allocAsk) s <= (ask o sub i o client) s})";
1.501 +by Auto_tac;
1.502 +by (etac (System_Follows_ask RS Follows_Bounded) 1);
1.503 +qed "Always_allocAsk_le_ask";
1.504 +
1.505 +Goal "System : Always (INT i: lessThan Nclients. \
1.506 +\ {s. (sub i o allocRel) s <= (rel o sub i o client) s})";
1.507 +by (auto_tac (claset() addSIs [Follows_Bounded, System_Follows_rel],
1.508 + simpset()));
1.509 +qed "Always_allocRel_le_rel";
1.510 +
1.511 +
1.512 +(*** Proof of the safety property (1) ***)
1.513 +
1.514 +(*safety (1), step 1 is System_Follows_rel*)
1.515 +
1.516 +(*safety (1), step 2*)
1.517 +(* i < Nclients ==> System : Increasing (sub i o allocRel) *)
1.518 +bind_thm ("System_Increasing_allocRel",
1.519 + System_Follows_rel RS Follows_Increasing1);
1.520 +
1.521 +(*Lifting Alloc_safety up to the level of systemState.
1.522 + Simplififying with o_def gets rid of the translations but it unfortunately
1.523 + gets rid of the other "o"s too.*)
1.524 +val rename_Alloc_Safety =
1.525 + Alloc_Safety RS rename_guarantees_sysOfAlloc_I
1.526 + |> simplify (simpset() addsimps [o_def]);
1.527 +
1.528 +(*safety (1), step 3*)
1.529 +Goal
1.530 + "System : Always {s. setsum (%i. (tokens o sub i o allocGiv) s) \
1.531 +\ (lessThan Nclients) \
1.532 +\ <= NbT + setsum (%i. (tokens o sub i o allocRel) s) \
1.533 +\ (lessThan Nclients)}";
1.534 +by (simp_tac (simpset() addsimps [o_apply]) 1);
1.535 +by (rtac (rename_Alloc_Safety RS component_guaranteesD) 1);
1.536 +by (auto_tac (claset(),
1.537 + simpset() addsimps [o_simp System_Increasing_allocRel]));
1.538 +qed "System_sum_bounded";
1.539 +
1.540 +
1.541 +(** Follows reasoning **)
1.542 +
1.543 +Goal "System : Always (INT i: lessThan Nclients. \
1.544 +\ {s. (tokens o giv o sub i o client) s \
1.545 +\ <= (tokens o sub i o allocGiv) s})";
1.546 +by (rtac (Always_giv_le_allocGiv RS Always_weaken) 1);
1.547 +by (auto_tac (claset() addIs [tokens_mono_prefix],
1.548 + simpset() addsimps [o_apply]));
1.549 +qed "Always_tokens_giv_le_allocGiv";
1.550 +
1.551 +Goal "System : Always (INT i: lessThan Nclients. \
1.552 +\ {s. (tokens o sub i o allocRel) s \
1.553 +\ <= (tokens o rel o sub i o client) s})";
1.554 +by (rtac (Always_allocRel_le_rel RS Always_weaken) 1);
1.555 +by (auto_tac (claset() addIs [tokens_mono_prefix],
1.556 + simpset() addsimps [o_apply]));
1.557 +qed "Always_tokens_allocRel_le_rel";
1.558 +
1.559 +(*safety (1), step 4 (final result!) *)
1.560 +Goalw [system_safety_def] "System : system_safety";
1.561 +by (rtac (Always_Int_rule [System_sum_bounded, Always_tokens_giv_le_allocGiv,
1.562 + Always_tokens_allocRel_le_rel] RS Always_weaken) 1);
1.563 +by Auto_tac;
1.564 +by (rtac (setsum_fun_mono RS order_trans) 1);
1.565 +by (dtac order_trans 2);
1.566 +by (rtac ([order_refl, setsum_fun_mono] MRS add_le_mono) 2);
1.567 +by (assume_tac 3);
1.568 +by Auto_tac;
1.569 +qed "System_safety";
1.570 +
1.571 +
1.572 +(*** Proof of the progress property (2) ***)
1.573 +
1.574 +(*progress (2), step 1 is System_Follows_ask and System_Follows_rel*)
1.575 +
1.576 +(*progress (2), step 2; see also System_Increasing_allocRel*)
1.577 +(* i < Nclients ==> System : Increasing (sub i o allocAsk) *)
1.578 +bind_thm ("System_Increasing_allocAsk",
1.579 + System_Follows_ask RS Follows_Increasing1);
1.580 +
1.581 +(*progress (2), step 3: lifting "Client_Bounded" to systemState*)
1.582 +Goal "i : I \
1.583 +\ ==> rename sysOfClient (plam x: I. rename client_map Client) : \
1.584 +\ UNIV guarantees \
1.585 +\ Always {s. ALL elt : set ((ask o sub i o client) s). elt <= NbT}";
1.586 +by rename_client_map_tac;
1.587 +qed "rename_Client_Bounded";
1.588 +
1.589 +Goal "i < Nclients \
1.590 +\ ==> System : Always \
1.591 +\ {s. ALL elt : set ((ask o sub i o client) s). elt <= NbT}";
1.592 +by (rtac ([rename_Client_Bounded,
1.593 + Client_component_System] MRS component_guaranteesD) 1);
1.594 +by Auto_tac;
1.595 +qed "System_Bounded_ask";
1.596 +
1.597 +Goal "{x. ALL y. P y --> Q x y} = (INT y: {y. P y}. {x. Q x y})";
1.598 +by (Blast_tac 1);
1.599 +qed "Collect_all_imp_eq";
1.600 +
1.601 +(*progress (2), step 4*)
1.602 +Goal "System : Always {s. ALL i<Nclients. \
1.603 +\ ALL elt : set ((sub i o allocAsk) s). elt <= NbT}";
1.604 +by (auto_tac (claset(), simpset() addsimps [Collect_all_imp_eq]));
1.605 +by (rtac (Always_Int_rule [Always_allocAsk_le_ask, System_Bounded_ask]
1.606 + RS Always_weaken) 1);
1.607 +by (auto_tac (claset() addDs [set_mono], simpset()));
1.608 +qed "System_Bounded_allocAsk";
1.609 +
1.610 +(*progress (2), step 5 is System_Increasing_allocGiv*)
1.611 +
1.612 +(*progress (2), step 6*)
1.613 +(* i < Nclients ==> System : Increasing (giv o sub i o client) *)
1.614 +bind_thm ("System_Increasing_giv",
1.615 + System_Follows_allocGiv RS Follows_Increasing1);
1.616 +
1.617 +
1.618 +Goal "i: I \
1.619 +\ ==> rename sysOfClient (plam x: I. rename client_map Client) \
1.620 +\ : Increasing (giv o sub i o client) \
1.621 +\ guarantees \
1.622 +\ (INT h. {s. h <= (giv o sub i o client) s & \
1.623 +\ h pfixGe (ask o sub i o client) s} \
1.624 +\ LeadsTo {s. tokens h <= (tokens o rel o sub i o client) s})";
1.625 +by rename_client_map_tac;
1.626 +by (asm_simp_tac (simpset() addsimps [o_simp Client_Progress]) 1);
1.627 +qed "rename_Client_Progress";
1.628 +
1.629 +
1.630 +(*progress (2), step 7*)
1.631 +Goal
1.632 + "System : (INT i : (lessThan Nclients). \
1.633 +\ INT h. {s. h <= (giv o sub i o client) s & \
1.634 +\ h pfixGe (ask o sub i o client) s} \
1.635 +\ LeadsTo {s. tokens h <= (tokens o rel o sub i o client) s})";
1.636 +by (rtac INT_I 1);
1.637 +(*Couldn't have just used Auto_tac since the "INT h" must be kept*)
1.638 +by (rtac ([rename_Client_Progress,
1.639 + Client_component_System] MRS component_guaranteesD) 1);
1.640 +by (auto_tac (claset(), simpset() addsimps [System_Increasing_giv]));
1.641 +qed "System_Client_Progress";
1.642 +
1.643 +(*Concludes
1.644 + System : {s. k <= (sub i o allocGiv) s}
1.645 + LeadsTo
1.646 + {s. (sub i o allocAsk) s <= (ask o sub i o client) s} Int
1.647 + {s. k <= (giv o sub i o client) s} *)
1.648 +val lemma =
1.649 + [System_Follows_ask RS Follows_Bounded,
1.650 + System_Follows_allocGiv RS Follows_LeadsTo] MRS Always_LeadsToD;
1.651 +
1.652 +(*A more complicated variant of the previous one*)
1.653 +val lemma2 = [lemma,
1.654 + System_Follows_ask RS Follows_Increasing1 RS IncreasingD]
1.655 + MRS PSP_Stable;
1.656 +
1.657 +Goal "i < Nclients \
1.658 +\ ==> System : {s. h <= (sub i o allocGiv) s & \
1.659 +\ h pfixGe (sub i o allocAsk) s} \
1.660 +\ LeadsTo \
1.661 +\ {s. h <= (giv o sub i o client) s & \
1.662 +\ h pfixGe (ask o sub i o client) s}";
1.663 +by (rtac single_LeadsTo_I 1);
1.664 +by (res_inst_tac [("k6", "h"), ("x2", "(sub i o allocAsk) s")]
1.665 + (lemma2 RS LeadsTo_weaken) 1);
1.666 +by Auto_tac;
1.667 +by (blast_tac (claset() addIs [trans_Ge RS trans_genPrefix RS transD,
1.668 + prefix_imp_pfixGe]) 1);
1.669 +val lemma3 = result();
1.670 +
1.671 +
1.672 +(*progress (2), step 8: Client i's "release" action is visible system-wide*)
1.673 +Goal "i < Nclients \
1.674 +\ ==> System : {s. h <= (sub i o allocGiv) s & \
1.675 +\ h pfixGe (sub i o allocAsk) s} \
1.676 +\ LeadsTo {s. tokens h <= (tokens o sub i o allocRel) s}";
1.677 +by (rtac LeadsTo_Trans 1);
1.678 +by (dtac (System_Follows_rel RS impOfSubs (mono_tokens RS mono_Follows_o) RS
1.679 + Follows_LeadsTo) 2);
1.680 +by (asm_full_simp_tac (simpset() addsimps [o_assoc]) 2);
1.681 +by (rtac LeadsTo_Trans 1);
1.682 +by (cut_facts_tac [System_Client_Progress] 2);
1.683 +by (blast_tac (claset() addIs [LeadsTo_Basis]) 2);
1.684 +by (etac lemma3 1);
1.685 +qed "System_Alloc_Client_Progress";
1.686 +
1.687 +(*Lifting Alloc_Progress up to the level of systemState*)
1.688 +val rename_Alloc_Progress =
1.689 + Alloc_Progress RS rename_guarantees_sysOfAlloc_I
1.690 + |> simplify (simpset() addsimps [o_def]);
1.691 +
1.692 +(*progress (2), step 9*)
1.693 +Goal
1.694 + "System : (INT i : (lessThan Nclients). \
1.695 +\ INT h. {s. h <= (sub i o allocAsk) s} \
1.696 +\ LeadsTo {s. h pfixLe (sub i o allocGiv) s})";
1.697 +(*Can't use simpset(): the "INT h" must be kept*)
1.698 +by (simp_tac (HOL_ss addsimps [o_apply, sub_def]) 1);
1.699 +by (rtac (rename_Alloc_Progress RS component_guaranteesD) 1);
1.700 +by (auto_tac (claset(),
1.701 + simpset() addsimps [o_simp System_Increasing_allocRel,
1.702 + o_simp System_Increasing_allocAsk,
1.703 + o_simp System_Bounded_allocAsk,
1.704 + o_simp System_Alloc_Client_Progress]));
1.705 +qed "System_Alloc_Progress";
1.706 +
1.707 +
1.708 +(*progress (2), step 10 (final result!) *)
1.709 +Goalw [system_progress_def] "System : system_progress";
1.710 +by (cut_facts_tac [System_Alloc_Progress] 1);
1.711 +by (blast_tac (claset() addIs [LeadsTo_Trans,
1.712 + System_Follows_allocGiv RS Follows_LeadsTo_pfixLe,
1.713 + System_Follows_ask RS Follows_LeadsTo]) 1);
1.714 +qed "System_Progress";
1.715 +
1.716 +
1.717 +(*Ultimate goal*)
1.718 +Goalw [system_spec_def] "System : system_spec";
1.719 +by (blast_tac (claset() addIs [System_safety, System_Progress]) 1);
1.720 +qed "System_correct";
1.721 +
1.722 +
1.723 +(** Some lemmas no longer used **)
1.724 +
1.725 +Goal "non_dummy = (% (g,a,r). (| giv = g, ask = a, rel = r |)) o \
1.726 +\ (funPair giv (funPair ask rel))";
1.727 +by (rtac ext 1);
1.728 +by (auto_tac (claset(), simpset() addsimps [o_def, non_dummy_def]));
1.729 +qed "non_dummy_eq_o_funPair";
1.730 +
1.731 +Goal "(preserves non_dummy) = \
1.732 +\ (preserves rel Int preserves ask Int preserves giv)";
1.733 +by (simp_tac (simpset() addsimps [non_dummy_eq_o_funPair]) 1);
1.734 +by Auto_tac;
1.735 +by (dres_inst_tac [("w1", "rel")] (impOfSubs subset_preserves_o) 1);
1.736 +by (dres_inst_tac [("w1", "ask")] (impOfSubs subset_preserves_o) 2);
1.737 +by (dres_inst_tac [("w1", "giv")] (impOfSubs subset_preserves_o) 3);
1.738 +by (auto_tac (claset(), simpset() addsimps [o_def]));
1.739 +qed "preserves_non_dummy_eq";
1.740 +
1.741 +(*Could go to Extend.ML*)
1.742 +Goal "bij f ==> fst (inv (%(x, u). inv f x) z) = f z";
1.743 +by (rtac fst_inv_equalityI 1);
1.744 +by (res_inst_tac [("f","%z. (f z, ?h z)")] surjI 1);
1.745 +by (asm_full_simp_tac (simpset() addsimps [bij_is_inj, inv_f_f]) 1);
1.746 +by (asm_full_simp_tac (simpset() addsimps [bij_is_surj, surj_f_inv_f]) 1);
1.747 +qed "bij_fst_inv_inv_eq";
2.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
2.2 +++ b/src/HOL/UNITY/Comp/Alloc.thy Mon Mar 05 15:32:54 2001 +0100
2.3 @@ -0,0 +1,261 @@
2.4 +(* Title: HOL/UNITY/Alloc
2.5 + ID: $Id$
2.6 + Author: Lawrence C Paulson, Cambridge University Computer Laboratory
2.7 + Copyright 1998 University of Cambridge
2.8 +
2.9 +Specification of Chandy and Charpentier's Allocator
2.10 +*)
2.11 +
2.12 +Alloc = AllocBase + PPROD +
2.13 +
2.14 +(** State definitions. OUTPUT variables are locals **)
2.15 +
2.16 +record clientState =
2.17 + giv :: nat list (*client's INPUT history: tokens GRANTED*)
2.18 + ask :: nat list (*client's OUTPUT history: tokens REQUESTED*)
2.19 + rel :: nat list (*client's OUTPUT history: tokens RELEASED*)
2.20 +
2.21 +record 'a clientState_d =
2.22 + clientState +
2.23 + dummy :: 'a (*dummy field for new variables*)
2.24 +
2.25 +constdefs
2.26 + (*DUPLICATED FROM Client.thy, but with "tok" removed*)
2.27 + (*Maybe want a special theory section to declare such maps*)
2.28 + non_dummy :: 'a clientState_d => clientState
2.29 + "non_dummy s == (|giv = giv s, ask = ask s, rel = rel s|)"
2.30 +
2.31 + (*Renaming map to put a Client into the standard form*)
2.32 + client_map :: "'a clientState_d => clientState*'a"
2.33 + "client_map == funPair non_dummy dummy"
2.34 +
2.35 +
2.36 +record allocState =
2.37 + allocGiv :: nat => nat list (*OUTPUT history: source of "giv" for i*)
2.38 + allocAsk :: nat => nat list (*INPUT: allocator's copy of "ask" for i*)
2.39 + allocRel :: nat => nat list (*INPUT: allocator's copy of "rel" for i*)
2.40 +
2.41 +record 'a allocState_d =
2.42 + allocState +
2.43 + dummy :: 'a (*dummy field for new variables*)
2.44 +
2.45 +record 'a systemState =
2.46 + allocState +
2.47 + client :: nat => clientState (*states of all clients*)
2.48 + dummy :: 'a (*dummy field for new variables*)
2.49 +
2.50 +
2.51 +constdefs
2.52 +
2.53 +(** Resource allocation system specification **)
2.54 +
2.55 + (*spec (1)*)
2.56 + system_safety :: 'a systemState program set
2.57 + "system_safety ==
2.58 + Always {s. setsum(%i.(tokens o giv o sub i o client)s) (lessThan Nclients)
2.59 + <= NbT + setsum(%i.(tokens o rel o sub i o client)s) (lessThan Nclients)}"
2.60 +
2.61 + (*spec (2)*)
2.62 + system_progress :: 'a systemState program set
2.63 + "system_progress == INT i : lessThan Nclients.
2.64 + INT h.
2.65 + {s. h <= (ask o sub i o client)s} LeadsTo
2.66 + {s. h pfixLe (giv o sub i o client) s}"
2.67 +
2.68 + system_spec :: 'a systemState program set
2.69 + "system_spec == system_safety Int system_progress"
2.70 +
2.71 +(** Client specification (required) ***)
2.72 +
2.73 + (*spec (3)*)
2.74 + client_increasing :: 'a clientState_d program set
2.75 + "client_increasing ==
2.76 + UNIV guarantees Increasing ask Int Increasing rel"
2.77 +
2.78 + (*spec (4)*)
2.79 + client_bounded :: 'a clientState_d program set
2.80 + "client_bounded ==
2.81 + UNIV guarantees Always {s. ALL elt : set (ask s). elt <= NbT}"
2.82 +
2.83 + (*spec (5)*)
2.84 + client_progress :: 'a clientState_d program set
2.85 + "client_progress ==
2.86 + Increasing giv guarantees
2.87 + (INT h. {s. h <= giv s & h pfixGe ask s}
2.88 + LeadsTo {s. tokens h <= (tokens o rel) s})"
2.89 +
2.90 + (*spec: preserves part*)
2.91 + client_preserves :: 'a clientState_d program set
2.92 + "client_preserves == preserves giv Int preserves clientState_d.dummy"
2.93 +
2.94 + (*environmental constraints*)
2.95 + client_allowed_acts :: 'a clientState_d program set
2.96 + "client_allowed_acts ==
2.97 + {F. AllowedActs F =
2.98 + insert Id (UNION (preserves (funPair rel ask)) Acts)}"
2.99 +
2.100 + client_spec :: 'a clientState_d program set
2.101 + "client_spec == client_increasing Int client_bounded Int client_progress
2.102 + Int client_allowed_acts Int client_preserves"
2.103 +
2.104 +(** Allocator specification (required) ***)
2.105 +
2.106 + (*spec (6)*)
2.107 + alloc_increasing :: 'a allocState_d program set
2.108 + "alloc_increasing ==
2.109 + UNIV guarantees
2.110 + (INT i : lessThan Nclients. Increasing (sub i o allocGiv))"
2.111 +
2.112 + (*spec (7)*)
2.113 + alloc_safety :: 'a allocState_d program set
2.114 + "alloc_safety ==
2.115 + (INT i : lessThan Nclients. Increasing (sub i o allocRel))
2.116 + guarantees
2.117 + Always {s. setsum(%i.(tokens o sub i o allocGiv)s) (lessThan Nclients)
2.118 + <= NbT + setsum(%i.(tokens o sub i o allocRel)s) (lessThan Nclients)}"
2.119 +
2.120 + (*spec (8)*)
2.121 + alloc_progress :: 'a allocState_d program set
2.122 + "alloc_progress ==
2.123 + (INT i : lessThan Nclients. Increasing (sub i o allocAsk) Int
2.124 + Increasing (sub i o allocRel))
2.125 + Int
2.126 + Always {s. ALL i<Nclients.
2.127 + ALL elt : set ((sub i o allocAsk) s). elt <= NbT}
2.128 + Int
2.129 + (INT i : lessThan Nclients.
2.130 + INT h. {s. h <= (sub i o allocGiv)s & h pfixGe (sub i o allocAsk)s}
2.131 + LeadsTo
2.132 + {s. tokens h <= (tokens o sub i o allocRel)s})
2.133 + guarantees
2.134 + (INT i : lessThan Nclients.
2.135 + INT h. {s. h <= (sub i o allocAsk) s}
2.136 + LeadsTo
2.137 + {s. h pfixLe (sub i o allocGiv) s})"
2.138 +
2.139 + (*NOTE: to follow the original paper, the formula above should have had
2.140 + INT h. {s. h i <= (sub i o allocGiv)s & h i pfixGe (sub i o allocAsk)s}
2.141 + LeadsTo
2.142 + {s. tokens h i <= (tokens o sub i o allocRel)s})
2.143 + thus h should have been a function variable. However, only h i is ever
2.144 + looked at.*)
2.145 +
2.146 + (*spec: preserves part*)
2.147 + alloc_preserves :: 'a allocState_d program set
2.148 + "alloc_preserves == preserves allocRel Int preserves allocAsk Int
2.149 + preserves allocState_d.dummy"
2.150 +
2.151 + (*environmental constraints*)
2.152 + alloc_allowed_acts :: 'a allocState_d program set
2.153 + "alloc_allowed_acts ==
2.154 + {F. AllowedActs F =
2.155 + insert Id (UNION (preserves allocGiv) Acts)}"
2.156 +
2.157 + alloc_spec :: 'a allocState_d program set
2.158 + "alloc_spec == alloc_increasing Int alloc_safety Int alloc_progress Int
2.159 + alloc_allowed_acts Int alloc_preserves"
2.160 +
2.161 +(** Network specification ***)
2.162 +
2.163 + (*spec (9.1)*)
2.164 + network_ask :: 'a systemState program set
2.165 + "network_ask == INT i : lessThan Nclients.
2.166 + Increasing (ask o sub i o client) guarantees
2.167 + ((sub i o allocAsk) Fols (ask o sub i o client))"
2.168 +
2.169 + (*spec (9.2)*)
2.170 + network_giv :: 'a systemState program set
2.171 + "network_giv == INT i : lessThan Nclients.
2.172 + Increasing (sub i o allocGiv)
2.173 + guarantees
2.174 + ((giv o sub i o client) Fols (sub i o allocGiv))"
2.175 +
2.176 + (*spec (9.3)*)
2.177 + network_rel :: 'a systemState program set
2.178 + "network_rel == INT i : lessThan Nclients.
2.179 + Increasing (rel o sub i o client)
2.180 + guarantees
2.181 + ((sub i o allocRel) Fols (rel o sub i o client))"
2.182 +
2.183 + (*spec: preserves part*)
2.184 + network_preserves :: 'a systemState program set
2.185 + "network_preserves ==
2.186 + preserves allocGiv Int
2.187 + (INT i : lessThan Nclients. preserves (rel o sub i o client) Int
2.188 + preserves (ask o sub i o client))"
2.189 +
2.190 + (*environmental constraints*)
2.191 + network_allowed_acts :: 'a systemState program set
2.192 + "network_allowed_acts ==
2.193 + {F. AllowedActs F =
2.194 + insert Id
2.195 + (UNION (preserves allocRel Int
2.196 + (INT i: lessThan Nclients. preserves(giv o sub i o client)))
2.197 + Acts)}"
2.198 +
2.199 + network_spec :: 'a systemState program set
2.200 + "network_spec == network_ask Int network_giv Int
2.201 + network_rel Int network_allowed_acts Int
2.202 + network_preserves"
2.203 +
2.204 +
2.205 +(** State mappings **)
2.206 + sysOfAlloc :: "((nat => clientState) * 'a) allocState_d => 'a systemState"
2.207 + "sysOfAlloc == %s. let (cl,xtr) = allocState_d.dummy s
2.208 + in (| allocGiv = allocGiv s,
2.209 + allocAsk = allocAsk s,
2.210 + allocRel = allocRel s,
2.211 + client = cl,
2.212 + dummy = xtr|)"
2.213 +
2.214 +
2.215 + sysOfClient :: "(nat => clientState) * 'a allocState_d => 'a systemState"
2.216 + "sysOfClient == %(cl,al). (| allocGiv = allocGiv al,
2.217 + allocAsk = allocAsk al,
2.218 + allocRel = allocRel al,
2.219 + client = cl,
2.220 + systemState.dummy = allocState_d.dummy al|)"
2.221 +
2.222 +consts
2.223 + Alloc :: 'a allocState_d program
2.224 + Client :: 'a clientState_d program
2.225 + Network :: 'a systemState program
2.226 + System :: 'a systemState program
2.227 +
2.228 +rules
2.229 + Alloc "Alloc : alloc_spec"
2.230 + Client "Client : client_spec"
2.231 + Network "Network : network_spec"
2.232 +
2.233 +defs
2.234 + System_def
2.235 + "System == rename sysOfAlloc Alloc Join Network Join
2.236 + (rename sysOfClient
2.237 + (plam x: lessThan Nclients. rename client_map Client))"
2.238 +
2.239 +
2.240 +(**
2.241 +locale System =
2.242 + fixes
2.243 + Alloc :: 'a allocState_d program
2.244 + Client :: 'a clientState_d program
2.245 + Network :: 'a systemState program
2.246 + System :: 'a systemState program
2.247 +
2.248 + assumes
2.249 + Alloc "Alloc : alloc_spec"
2.250 + Client "Client : client_spec"
2.251 + Network "Network : network_spec"
2.252 +
2.253 + defines
2.254 + System_def
2.255 + "System == rename sysOfAlloc Alloc
2.256 + Join
2.257 + Network
2.258 + Join
2.259 + (rename sysOfClient
2.260 + (plam x: lessThan Nclients. rename client_map Client))"
2.261 +**)
2.262 +
2.263 +
2.264 +end
3.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
3.2 +++ b/src/HOL/UNITY/Comp/AllocBase.ML Mon Mar 05 15:32:54 2001 +0100
3.3 @@ -0,0 +1,89 @@
3.4 +(* Title: HOL/UNITY/AllocBase.ML
3.5 + ID: $Id$
3.6 + Author: Lawrence C Paulson, Cambridge University Computer Laboratory
3.7 + Copyright 1998 University of Cambridge
3.8 +
3.9 +Basis declarations for Chandy and Charpentier's Allocator
3.10 +*)
3.11 +
3.12 +Goal "!!f :: nat=>nat. \
3.13 +\ (ALL i. i<n --> f i <= g i) --> \
3.14 +\ setsum f (lessThan n) <= setsum g (lessThan n)";
3.15 +by (induct_tac "n" 1);
3.16 +by (auto_tac (claset(), simpset() addsimps [lessThan_Suc]));
3.17 +by (dres_inst_tac [("x","n")] spec 1);
3.18 +by (arith_tac 1);
3.19 +qed_spec_mp "setsum_fun_mono";
3.20 +
3.21 +Goal "ALL xs. xs <= ys --> tokens xs <= tokens ys";
3.22 +by (induct_tac "ys" 1);
3.23 +by (auto_tac (claset(), simpset() addsimps [prefix_Cons]));
3.24 +qed_spec_mp "tokens_mono_prefix";
3.25 +
3.26 +Goalw [mono_def] "mono tokens";
3.27 +by (blast_tac (claset() addIs [tokens_mono_prefix]) 1);
3.28 +qed "mono_tokens";
3.29 +
3.30 +
3.31 +(** bag_of **)
3.32 +
3.33 +Goal "bag_of (l@l') = bag_of l + bag_of l'";
3.34 +by (induct_tac "l" 1);
3.35 + by (asm_simp_tac (simpset() addsimps (thms "plus_ac0")) 2);
3.36 +by (Simp_tac 1);
3.37 +qed "bag_of_append";
3.38 +Addsimps [bag_of_append];
3.39 +
3.40 +Goal "mono (bag_of :: 'a list => ('a::order) multiset)";
3.41 +by (rtac monoI 1);
3.42 +by (rewtac prefix_def);
3.43 +by (etac genPrefix.induct 1);
3.44 +by Auto_tac;
3.45 +by (asm_full_simp_tac (simpset() addsimps [thm "union_le_mono"]) 1);
3.46 +by (etac order_trans 1);
3.47 +by (rtac (thm "union_upper1") 1);
3.48 +qed "mono_bag_of";
3.49 +
3.50 +(** setsum **)
3.51 +
3.52 +Addcongs [setsum_cong];
3.53 +
3.54 +Goal "setsum (%i. {#if i<k then f i else g i#}) (A Int lessThan k) = \
3.55 +\ setsum (%i. {#f i#}) (A Int lessThan k)";
3.56 +by (rtac setsum_cong 1);
3.57 +by Auto_tac;
3.58 +qed "bag_of_sublist_lemma";
3.59 +
3.60 +Goal "bag_of (sublist l A) = \
3.61 +\ setsum (%i. {# l!i #}) (A Int lessThan (length l))";
3.62 +by (rev_induct_tac "l" 1);
3.63 +by (Simp_tac 1);
3.64 +by (asm_simp_tac
3.65 + (simpset() addsimps [sublist_append, Int_insert_right, lessThan_Suc,
3.66 + nth_append, bag_of_sublist_lemma] @ thms "plus_ac0") 1);
3.67 +qed "bag_of_sublist";
3.68 +
3.69 +
3.70 +Goal "bag_of (sublist l (A Un B)) + bag_of (sublist l (A Int B)) = \
3.71 +\ bag_of (sublist l A) + bag_of (sublist l B)";
3.72 +by (subgoal_tac "A Int B Int {..length l(} = \
3.73 +\ (A Int {..length l(}) Int (B Int {..length l(})" 1);
3.74 +by (asm_simp_tac (simpset() addsimps [bag_of_sublist, Int_Un_distrib2,
3.75 + setsum_Un_Int]) 1);
3.76 +by (Blast_tac 1);
3.77 +qed "bag_of_sublist_Un_Int";
3.78 +
3.79 +Goal "A Int B = {} \
3.80 +\ ==> bag_of (sublist l (A Un B)) = \
3.81 +\ bag_of (sublist l A) + bag_of (sublist l B)";
3.82 +by (asm_simp_tac (simpset() addsimps [bag_of_sublist_Un_Int RS sym]) 1);
3.83 +qed "bag_of_sublist_Un_disjoint";
3.84 +
3.85 +Goal "[| finite I; ALL i:I. ALL j:I. i~=j --> A i Int A j = {} |] \
3.86 +\ ==> bag_of (sublist l (UNION I A)) = \
3.87 +\ setsum (%i. bag_of (sublist l (A i))) I";
3.88 +by (asm_simp_tac (simpset() delsimps UN_simps addsimps (UN_simps RL [sym])
3.89 + addsimps [bag_of_sublist]) 1);
3.90 +by (stac setsum_UN_disjoint 1);
3.91 +by Auto_tac;
3.92 +qed_spec_mp "bag_of_sublist_UN_disjoint";
4.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
4.2 +++ b/src/HOL/UNITY/Comp/AllocBase.thy Mon Mar 05 15:32:54 2001 +0100
4.3 @@ -0,0 +1,31 @@
4.4 +(* Title: HOL/UNITY/AllocBase.thy
4.5 + ID: $Id$
4.6 + Author: Lawrence C Paulson, Cambridge University Computer Laboratory
4.7 + Copyright 1998 University of Cambridge
4.8 +
4.9 +Common declarations for Chandy and Charpentier's Allocator
4.10 +*)
4.11 +
4.12 +AllocBase = Rename + Follows +
4.13 +
4.14 +consts
4.15 + NbT :: nat (*Number of tokens in system*)
4.16 + Nclients :: nat (*Number of clients*)
4.17 +
4.18 +rules
4.19 + NbT_pos "0 < NbT"
4.20 +
4.21 +(*This function merely sums the elements of a list*)
4.22 +consts tokens :: nat list => nat
4.23 +primrec
4.24 + "tokens [] = 0"
4.25 + "tokens (x#xs) = x + tokens xs"
4.26 +
4.27 +consts
4.28 + bag_of :: 'a list => 'a multiset
4.29 +
4.30 +primrec
4.31 + "bag_of [] = {#}"
4.32 + "bag_of (x#xs) = {#x#} + bag_of xs"
4.33 +
4.34 +end
5.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
5.2 +++ b/src/HOL/UNITY/Comp/AllocImpl.ML Mon Mar 05 15:32:54 2001 +0100
5.3 @@ -0,0 +1,194 @@
5.4 +(* Title: HOL/UNITY/AllocImpl
5.5 + ID: $Id$
5.6 + Author: Lawrence C Paulson, Cambridge University Computer Laboratory
5.7 + Copyright 2000 University of Cambridge
5.8 +
5.9 +Implementation of a multiple-client allocator from a single-client allocator
5.10 +*)
5.11 +
5.12 +AddIs [impOfSubs subset_preserves_o];
5.13 +Addsimps [funPair_o_distrib];
5.14 +Addsimps [Always_INT_distrib];
5.15 +Delsimps [o_apply];
5.16 +
5.17 +Open_locale "Merge";
5.18 +
5.19 +val Merge = thm "Merge_spec";
5.20 +
5.21 +Goal "Allowed M = (preserves merge.Out) Int (preserves merge.iOut)";
5.22 +by (cut_facts_tac [Merge] 1);
5.23 +by (auto_tac (claset(),
5.24 + simpset() addsimps [merge_spec_def, merge_allowed_acts_def,
5.25 + Allowed_def, safety_prop_Acts_iff]));
5.26 +qed "Merge_Allowed";
5.27 +
5.28 +Goal "M ok G = (G: preserves merge.Out & G: preserves merge.iOut & \
5.29 +\ M : Allowed G)";
5.30 +by (auto_tac (claset(), simpset() addsimps [Merge_Allowed, ok_iff_Allowed]));
5.31 +qed "M_ok_iff";
5.32 +AddIffs [M_ok_iff];
5.33 +
5.34 +Goal "[| G: preserves merge.Out; G: preserves merge.iOut; M : Allowed G |] \
5.35 +\ ==> M Join G : Always {s. length (merge.Out s) = length (merge.iOut s)}";
5.36 +by (cut_facts_tac [Merge] 1);
5.37 +by (force_tac (claset() addDs [guaranteesD],
5.38 + simpset() addsimps [merge_spec_def, merge_eqOut_def]) 1);
5.39 +qed "Merge_Always_Out_eq_iOut";
5.40 +
5.41 +Goal "[| G: preserves merge.iOut; G: preserves merge.Out; M : Allowed G |] \
5.42 +\ ==> M Join G: Always {s. ALL elt : set (merge.iOut s). elt < Nclients}";
5.43 +by (cut_facts_tac [Merge] 1);
5.44 +by (force_tac (claset() addDs [guaranteesD],
5.45 + simpset() addsimps [merge_spec_def, merge_bounded_def]) 1);
5.46 +qed "Merge_Bounded";
5.47 +
5.48 +Goal "[| G: preserves merge.iOut; G: preserves merge.Out; M : Allowed G |] \
5.49 +\ ==> M Join G : Always \
5.50 +\ {s. setsum (%i. bag_of (sublist (merge.Out s) \
5.51 +\ {k. k < length (iOut s) & iOut s ! k = i})) \
5.52 +\ (lessThan Nclients) = \
5.53 +\ (bag_of o merge.Out) s}";
5.54 +by (rtac ([[Merge_Always_Out_eq_iOut, Merge_Bounded] MRS Always_Int_I,
5.55 + UNIV_AlwaysI] MRS (Always_Compl_Un_eq RS iffD1)) 1);
5.56 + by Auto_tac;
5.57 +by (stac (bag_of_sublist_UN_disjoint RS sym) 1);
5.58 + by (Simp_tac 1);
5.59 + by (Blast_tac 1);
5.60 +by (asm_full_simp_tac (simpset() addsimps [set_conv_nth]) 1);
5.61 +by (subgoal_tac
5.62 + "(UN i:lessThan Nclients. {k. k < length (iOut x) & iOut x ! k = i}) = \
5.63 +\ lessThan (length (iOut x))" 1);
5.64 + by (Blast_tac 2);
5.65 +by (asm_simp_tac (simpset() addsimps [o_def]) 1);
5.66 +qed "Merge_Bag_Follows_lemma";
5.67 +
5.68 +Goal "M : (INT i: lessThan Nclients. Increasing (sub i o merge.In)) \
5.69 +\ guarantees \
5.70 +\ (bag_of o merge.Out) Fols \
5.71 +\ (%s. setsum (%i. (bag_of o sub i o merge.In) s) \
5.72 +\ (lessThan Nclients))";
5.73 +by (rtac (Merge_Bag_Follows_lemma RS Always_Follows1 RS guaranteesI) 1);
5.74 +by Auto_tac;
5.75 +by (rtac Follows_setsum 1);
5.76 +by (cut_facts_tac [Merge] 1);
5.77 +by (auto_tac (claset(),
5.78 + simpset() addsimps [merge_spec_def, merge_follows_def, o_def]));
5.79 +by (dtac guaranteesD 1);
5.80 +by (best_tac
5.81 + (claset() addIs [impOfSubs (mono_bag_of RS mono_Follows_apply)]) 3);
5.82 +by Auto_tac;
5.83 +qed "Merge_Bag_Follows";
5.84 +
5.85 +Close_locale "Merge";
5.86 +
5.87 +
5.88 +(** Distributor **)
5.89 +
5.90 +Open_locale "Distrib";
5.91 +
5.92 +val Distrib = thm "Distrib_spec";
5.93 +
5.94 +
5.95 +Goal "D : Increasing distr.In Int Increasing distr.iIn Int \
5.96 +\ Always {s. ALL elt : set (distr.iIn s). elt < Nclients} \
5.97 +\ guarantees \
5.98 +\ (INT i : lessThan Nclients. Increasing (sub i o distr.Out))";
5.99 +by (cut_facts_tac [Distrib] 1);
5.100 +by (full_simp_tac (simpset() addsimps [distr_spec_def, distr_follows_def]) 1);
5.101 +by (Clarify_tac 1);
5.102 +by (blast_tac (claset() addIs [guaranteesI, Follows_Increasing1]
5.103 + addDs [guaranteesD]) 1);
5.104 +qed "Distr_Increasing_Out";
5.105 +
5.106 +Goal "[| G : preserves distr.Out; \
5.107 +\ D Join G : Always {s. ALL elt: set (distr.iIn s). elt < Nclients} |] \
5.108 +\ ==> D Join G : Always \
5.109 +\ {s. setsum (%i. bag_of (sublist (distr.In s) \
5.110 +\ {k. k < length (iIn s) & iIn s ! k = i})) \
5.111 +\ (lessThan Nclients) = \
5.112 +\ bag_of (sublist (distr.In s) (lessThan (length (iIn s))))}";
5.113 +by (etac ([asm_rl, UNIV_AlwaysI] MRS (Always_Compl_Un_eq RS iffD1)) 1);
5.114 +by Auto_tac;
5.115 +by (stac (bag_of_sublist_UN_disjoint RS sym) 1);
5.116 + by (Simp_tac 1);
5.117 + by (Blast_tac 1);
5.118 +by (asm_full_simp_tac (simpset() addsimps [set_conv_nth]) 1);
5.119 +by (subgoal_tac
5.120 + "(UN i:lessThan Nclients. {k. k < length (iIn x) & iIn x ! k = i}) = \
5.121 +\ lessThan (length (iIn x))" 1);
5.122 + by (Blast_tac 2);
5.123 +by (Asm_simp_tac 1);
5.124 +qed "Distr_Bag_Follows_lemma";
5.125 +
5.126 +Goal "D ok G = (G: preserves distr.Out & D : Allowed G)";
5.127 +by (cut_facts_tac [Distrib] 1);
5.128 +by (auto_tac (claset(),
5.129 + simpset() addsimps [distr_spec_def, distr_allowed_acts_def,
5.130 + Allowed_def, safety_prop_Acts_iff, ok_iff_Allowed]));
5.131 +qed "D_ok_iff";
5.132 +AddIffs [D_ok_iff];
5.133 +
5.134 +Goal
5.135 + "D : Increasing distr.In Int Increasing distr.iIn Int \
5.136 +\ Always {s. ALL elt : set (distr.iIn s). elt < Nclients} \
5.137 +\ guarantees \
5.138 +\ (INT i : lessThan Nclients. \
5.139 +\ (%s. setsum (%i. (bag_of o sub i o distr.Out) s) (lessThan Nclients)) \
5.140 +\ Fols \
5.141 +\ (%s. bag_of (sublist (distr.In s) (lessThan (length(distr.iIn s))))))";
5.142 +by (rtac guaranteesI 1);
5.143 +by (Clarify_tac 1);
5.144 +by (rtac (Distr_Bag_Follows_lemma RS Always_Follows2) 1);
5.145 +by Auto_tac;
5.146 +by (rtac Follows_setsum 1);
5.147 +by (cut_facts_tac [Distrib] 1);
5.148 +by (auto_tac (claset(),
5.149 + simpset() addsimps [distr_spec_def, distr_follows_def, o_def]));
5.150 +by (dtac guaranteesD 1);
5.151 +by (best_tac (claset() addIs [impOfSubs (mono_bag_of RS mono_Follows_apply)]) 3);
5.152 +by Auto_tac;
5.153 +qed "Distr_Bag_Follows";
5.154 +
5.155 +Close_locale "Distrib";
5.156 +
5.157 +
5.158 +Goal "!!f::nat=>nat. (INT i:(lessThan n). {s. f i <= g i s}) \
5.159 +\ <= {s. setsum f (lessThan n) <= setsum (%i. g i s) (lessThan n)}";
5.160 +by (induct_tac "n" 1);
5.161 +by (auto_tac (claset(), simpset() addsimps [lessThan_Suc]));
5.162 +qed "alloc_refinement_lemma";
5.163 +
5.164 +Goal
5.165 +"(INT i : lessThan Nclients. Increasing (sub i o allocAsk) Int \
5.166 +\ Increasing (sub i o allocRel)) \
5.167 +\ Int \
5.168 +\ Always {s. ALL i. i<Nclients --> \
5.169 +\ (ALL elt : set ((sub i o allocAsk) s). elt <= NbT)} \
5.170 +\ Int \
5.171 +\ (INT i : lessThan Nclients. \
5.172 +\ INT h. {s. h <= (sub i o allocGiv)s & h pfixGe (sub i o allocAsk)s} \
5.173 +\ LeadsTo {s. tokens h <= (tokens o sub i o allocRel)s}) \
5.174 +\ <= \
5.175 +\(INT i : lessThan Nclients. Increasing (sub i o allocAsk) Int \
5.176 +\ Increasing (sub i o allocRel)) \
5.177 +\ Int \
5.178 +\ Always {s. ALL i. i<Nclients --> \
5.179 +\ (ALL elt : set ((sub i o allocAsk) s). elt <= NbT)} \
5.180 +\ Int \
5.181 +\ (INT hf. (INT i : lessThan Nclients. \
5.182 +\ {s. hf i <= (sub i o allocGiv)s & hf i pfixGe (sub i o allocAsk)s}) \
5.183 +\ LeadsTo {s. setsum (%i. tokens (hf i)) (lessThan Nclients) <= \
5.184 +\ setsum (%i. (tokens o sub i o allocRel)s) (lessThan Nclients) })";
5.185 +by (auto_tac (claset(), simpset() addsimps [ball_conj_distrib]));
5.186 +by (rename_tac "F hf" 1);
5.187 +by (rtac ([Finite_stable_completion, alloc_refinement_lemma]
5.188 + MRS LeadsTo_weaken_R) 1);
5.189 + by (Blast_tac 1);
5.190 + by (Blast_tac 1);
5.191 +by (subgoal_tac "F : Increasing (tokens o (sub i o allocRel))" 1);
5.192 + by (blast_tac
5.193 + (claset() addIs [impOfSubs (mono_tokens RS mono_Increasing_o)]) 2);
5.194 +by (asm_full_simp_tac (simpset() addsimps [Increasing_def, o_assoc]) 1);
5.195 +qed "alloc_refinement";
5.196 +
5.197 +
6.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
6.2 +++ b/src/HOL/UNITY/Comp/AllocImpl.thy Mon Mar 05 15:32:54 2001 +0100
6.3 @@ -0,0 +1,224 @@
6.4 +(* Title: HOL/UNITY/AllocImpl
6.5 + ID: $Id$
6.6 + Author: Lawrence C Paulson, Cambridge University Computer Laboratory
6.7 + Copyright 1998 University of Cambridge
6.8 +
6.9 +Implementation of a multiple-client allocator from a single-client allocator
6.10 +*)
6.11 +
6.12 +AllocImpl = AllocBase + Follows + PPROD +
6.13 +
6.14 +
6.15 +(** State definitions. OUTPUT variables are locals **)
6.16 +
6.17 +(*Type variable 'b is the type of items being merged*)
6.18 +record 'b merge =
6.19 + In :: nat => 'b list (*merge's INPUT histories: streams to merge*)
6.20 + Out :: 'b list (*merge's OUTPUT history: merged items*)
6.21 + iOut :: nat list (*merge's OUTPUT history: origins of merged items*)
6.22 +
6.23 +record ('a,'b) merge_d =
6.24 + 'b merge +
6.25 + dummy :: 'a (*dummy field for new variables*)
6.26 +
6.27 +constdefs
6.28 + non_dummy :: ('a,'b) merge_d => 'b merge
6.29 + "non_dummy s == (|In = In s, Out = Out s, iOut = iOut s|)"
6.30 +
6.31 +record 'b distr =
6.32 + In :: 'b list (*items to distribute*)
6.33 + iIn :: nat list (*destinations of items to distribute*)
6.34 + Out :: nat => 'b list (*distributed items*)
6.35 +
6.36 +record ('a,'b) distr_d =
6.37 + 'b distr +
6.38 + dummy :: 'a (*dummy field for new variables*)
6.39 +
6.40 +record allocState =
6.41 + giv :: nat list (*OUTPUT history: source of tokens*)
6.42 + ask :: nat list (*INPUT: tokens requested from allocator*)
6.43 + rel :: nat list (*INPUT: tokens released to allocator*)
6.44 +
6.45 +record 'a allocState_d =
6.46 + allocState +
6.47 + dummy :: 'a (*dummy field for new variables*)
6.48 +
6.49 +record 'a systemState =
6.50 + allocState +
6.51 + mergeRel :: nat merge
6.52 + mergeAsk :: nat merge
6.53 + distr :: nat distr
6.54 + dummy :: 'a (*dummy field for new variables*)
6.55 +
6.56 +
6.57 +constdefs
6.58 +
6.59 +(** Merge specification (the number of inputs is Nclients) ***)
6.60 +
6.61 + (*spec (10)*)
6.62 + merge_increasing :: ('a,'b) merge_d program set
6.63 + "merge_increasing ==
6.64 + UNIV guarantees (Increasing merge.Out) Int (Increasing merge.iOut)"
6.65 +
6.66 + (*spec (11)*)
6.67 + merge_eqOut :: ('a,'b) merge_d program set
6.68 + "merge_eqOut ==
6.69 + UNIV guarantees
6.70 + Always {s. length (merge.Out s) = length (merge.iOut s)}"
6.71 +
6.72 + (*spec (12)*)
6.73 + merge_bounded :: ('a,'b) merge_d program set
6.74 + "merge_bounded ==
6.75 + UNIV guarantees
6.76 + Always {s. ALL elt : set (merge.iOut s). elt < Nclients}"
6.77 +
6.78 + (*spec (13)*)
6.79 + merge_follows :: ('a,'b) merge_d program set
6.80 + "merge_follows ==
6.81 + (INT i : lessThan Nclients. Increasing (sub i o merge.In))
6.82 + guarantees
6.83 + (INT i : lessThan Nclients.
6.84 + (%s. sublist (merge.Out s)
6.85 + {k. k < size(merge.iOut s) & merge.iOut s! k = i})
6.86 + Fols (sub i o merge.In))"
6.87 +
6.88 + (*spec: preserves part*)
6.89 + merge_preserves :: ('a,'b) merge_d program set
6.90 + "merge_preserves == preserves merge.In Int preserves merge_d.dummy"
6.91 +
6.92 + (*environmental constraints*)
6.93 + merge_allowed_acts :: ('a,'b) merge_d program set
6.94 + "merge_allowed_acts ==
6.95 + {F. AllowedActs F =
6.96 + insert Id (UNION (preserves (funPair merge.Out merge.iOut)) Acts)}"
6.97 +
6.98 + merge_spec :: ('a,'b) merge_d program set
6.99 + "merge_spec == merge_increasing Int merge_eqOut Int merge_bounded Int
6.100 + merge_follows Int merge_allowed_acts Int merge_preserves"
6.101 +
6.102 +(** Distributor specification (the number of outputs is Nclients) ***)
6.103 +
6.104 + (*spec (14)*)
6.105 + distr_follows :: ('a,'b) distr_d program set
6.106 + "distr_follows ==
6.107 + Increasing distr.In Int Increasing distr.iIn Int
6.108 + Always {s. ALL elt : set (distr.iIn s). elt < Nclients}
6.109 + guarantees
6.110 + (INT i : lessThan Nclients.
6.111 + (sub i o distr.Out) Fols
6.112 + (%s. sublist (distr.In s)
6.113 + {k. k < size(distr.iIn s) & distr.iIn s ! k = i}))"
6.114 +
6.115 + distr_allowed_acts :: ('a,'b) distr_d program set
6.116 + "distr_allowed_acts ==
6.117 + {D. AllowedActs D = insert Id (UNION (preserves distr.Out) Acts)}"
6.118 +
6.119 + distr_spec :: ('a,'b) distr_d program set
6.120 + "distr_spec == distr_follows Int distr_allowed_acts"
6.121 +
6.122 +(** Single-client allocator specification (required) ***)
6.123 +
6.124 + (*spec (18)*)
6.125 + alloc_increasing :: 'a allocState_d program set
6.126 + "alloc_increasing == UNIV guarantees Increasing giv"
6.127 +
6.128 + (*spec (19)*)
6.129 + alloc_safety :: 'a allocState_d program set
6.130 + "alloc_safety ==
6.131 + Increasing rel
6.132 + guarantees Always {s. tokens (giv s) <= NbT + tokens (rel s)}"
6.133 +
6.134 + (*spec (20)*)
6.135 + alloc_progress :: 'a allocState_d program set
6.136 + "alloc_progress ==
6.137 + Increasing ask Int Increasing rel Int
6.138 + Always {s. ALL elt : set (ask s). elt <= NbT}
6.139 + Int
6.140 + (INT h. {s. h <= giv s & h pfixGe (ask s)}
6.141 + LeadsTo
6.142 + {s. tokens h <= tokens (rel s)})
6.143 + guarantees (INT h. {s. h <= ask s} LeadsTo {s. h pfixLe giv s})"
6.144 +
6.145 + (*spec: preserves part*)
6.146 + alloc_preserves :: 'a allocState_d program set
6.147 + "alloc_preserves == preserves rel Int
6.148 + preserves ask Int
6.149 + preserves allocState_d.dummy"
6.150 +
6.151 +
6.152 + (*environmental constraints*)
6.153 + alloc_allowed_acts :: 'a allocState_d program set
6.154 + "alloc_allowed_acts ==
6.155 + {F. AllowedActs F = insert Id (UNION (preserves giv) Acts)}"
6.156 +
6.157 + alloc_spec :: 'a allocState_d program set
6.158 + "alloc_spec == alloc_increasing Int alloc_safety Int alloc_progress Int
6.159 + alloc_allowed_acts Int alloc_preserves"
6.160 +
6.161 +locale Merge =
6.162 + fixes
6.163 + M :: ('a,'b::order) merge_d program
6.164 + assumes
6.165 + Merge_spec "M : merge_spec"
6.166 +
6.167 +locale Distrib =
6.168 + fixes
6.169 + D :: ('a,'b::order) distr_d program
6.170 + assumes
6.171 + Distrib_spec "D : distr_spec"
6.172 +
6.173 +
6.174 +(****
6.175 +# (** Network specification ***)
6.176 +
6.177 +# (*spec (9.1)*)
6.178 +# network_ask :: 'a systemState program set
6.179 +# "network_ask == INT i : lessThan Nclients.
6.180 +# Increasing (ask o sub i o client)
6.181 +# guarantees[ask]
6.182 +# (ask Fols (ask o sub i o client))"
6.183 +
6.184 +# (*spec (9.2)*)
6.185 +# network_giv :: 'a systemState program set
6.186 +# "network_giv == INT i : lessThan Nclients.
6.187 +# Increasing giv
6.188 +# guarantees[giv o sub i o client]
6.189 +# ((giv o sub i o client) Fols giv )"
6.190 +
6.191 +# (*spec (9.3)*)
6.192 +# network_rel :: 'a systemState program set
6.193 +# "network_rel == INT i : lessThan Nclients.
6.194 +# Increasing (rel o sub i o client)
6.195 +# guarantees[rel]
6.196 +# (rel Fols (rel o sub i o client))"
6.197 +
6.198 +# (*spec: preserves part*)
6.199 +# network_preserves :: 'a systemState program set
6.200 +# "network_preserves == preserves giv Int
6.201 +# (INT i : lessThan Nclients.
6.202 +# preserves (funPair rel ask o sub i o client))"
6.203 +
6.204 +# network_spec :: 'a systemState program set
6.205 +# "network_spec == network_ask Int network_giv Int
6.206 +# network_rel Int network_preserves"
6.207 +
6.208 +
6.209 +# (** State mappings **)
6.210 +# sysOfAlloc :: "((nat => merge) * 'a) allocState_d => 'a systemState"
6.211 +# "sysOfAlloc == %s. let (cl,xtr) = allocState_d.dummy s
6.212 +# in (| giv = giv s,
6.213 +# ask = ask s,
6.214 +# rel = rel s,
6.215 +# client = cl,
6.216 +# dummy = xtr|)"
6.217 +
6.218 +
6.219 +# sysOfClient :: "(nat => merge) * 'a allocState_d => 'a systemState"
6.220 +# "sysOfClient == %(cl,al). (| giv = giv al,
6.221 +# ask = ask al,
6.222 +# rel = rel al,
6.223 +# client = cl,
6.224 +# systemState.dummy = allocState_d.dummy al|)"
6.225 +****)
6.226 +
6.227 +end
7.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
7.2 +++ b/src/HOL/UNITY/Comp/Client.ML Mon Mar 05 15:32:54 2001 +0100
7.3 @@ -0,0 +1,174 @@
7.4 +(* Title: HOL/UNITY/Client
7.5 + ID: $Id$
7.6 + Author: Lawrence C Paulson, Cambridge University Computer Laboratory
7.7 + Copyright 1998 University of Cambridge
7.8 +
7.9 +Distributed Resource Management System: the Client
7.10 +*)
7.11 +
7.12 +Addsimps [Client_def RS def_prg_Init,
7.13 + Client_def RS def_prg_AllowedActs];
7.14 +program_defs_ref := [Client_def];
7.15 +
7.16 +Addsimps (map simp_of_act [rel_act_def, tok_act_def, ask_act_def]);
7.17 +
7.18 +Goal "(Client ok G) = \
7.19 +\ (G : preserves rel & G : preserves ask & G : preserves tok &\
7.20 +\ Client : Allowed G)";
7.21 +by (auto_tac (claset(),
7.22 + simpset() addsimps [ok_iff_Allowed, Client_def RS def_prg_Allowed]));
7.23 +qed "Client_ok_iff";
7.24 +AddIffs [Client_ok_iff];
7.25 +
7.26 +
7.27 +(*Safety property 1: ask, rel are increasing*)
7.28 +Goal "Client: UNIV guarantees Increasing ask Int Increasing rel";
7.29 +by (auto_tac
7.30 + (claset() addSIs [increasing_imp_Increasing],
7.31 + simpset() addsimps [guar_def, impOfSubs preserves_subset_increasing]));
7.32 +by (auto_tac (claset(), simpset() addsimps [increasing_def]));
7.33 +by (ALLGOALS constrains_tac);
7.34 +by Auto_tac;
7.35 +qed "increasing_ask_rel";
7.36 +
7.37 +Addsimps [nth_append, append_one_prefix];
7.38 +
7.39 +
7.40 +(*Safety property 2: the client never requests too many tokens.
7.41 + With no Substitution Axiom, we must prove the two invariants
7.42 + simultaneously.
7.43 +*)
7.44 +Goal "Client ok G \
7.45 +\ ==> Client Join G : \
7.46 +\ Always ({s. tok s <= NbT} Int \
7.47 +\ {s. ALL elt : set (ask s). elt <= NbT})";
7.48 +by Auto_tac;
7.49 +by (rtac (invariantI RS stable_Join_Always2) 1);
7.50 +by (fast_tac (claset() addSEs [impOfSubs preserves_subset_stable]
7.51 + addSIs [stable_Int]) 3);
7.52 +by (constrains_tac 2);
7.53 +by (cut_inst_tac [("m", "tok s")] (NbT_pos RS mod_less_divisor) 2);
7.54 +by Auto_tac;
7.55 +qed "ask_bounded_lemma";
7.56 +
7.57 +(*export version, with no mention of tok in the postcondition, but
7.58 + unfortunately tok must be declared local.*)
7.59 +Goal "Client: UNIV guarantees Always {s. ALL elt : set (ask s). elt <= NbT}";
7.60 +by (rtac guaranteesI 1);
7.61 +by (etac (ask_bounded_lemma RS Always_weaken) 1);
7.62 +by (rtac Int_lower2 1);
7.63 +qed "ask_bounded";
7.64 +
7.65 +
7.66 +(*** Towards proving the liveness property ***)
7.67 +
7.68 +Goal "Client: stable {s. rel s <= giv s}";
7.69 +by (constrains_tac 1);
7.70 +by Auto_tac;
7.71 +qed "stable_rel_le_giv";
7.72 +
7.73 +Goal "[| Client Join G : Increasing giv; G : preserves rel |] \
7.74 +\ ==> Client Join G : Stable {s. rel s <= giv s}";
7.75 +by (rtac (stable_rel_le_giv RS Increasing_preserves_Stable) 1);
7.76 +by Auto_tac;
7.77 +qed "Join_Stable_rel_le_giv";
7.78 +
7.79 +Goal "[| Client Join G : Increasing giv; G : preserves rel |] \
7.80 +\ ==> Client Join G : Always {s. rel s <= giv s}";
7.81 +by (force_tac (claset() addIs [AlwaysI, Join_Stable_rel_le_giv], simpset()) 1);
7.82 +qed "Join_Always_rel_le_giv";
7.83 +
7.84 +Goal "Client : transient {s. rel s = k & k<h & h <= giv s & h pfixGe ask s}";
7.85 +by (res_inst_tac [("act", "rel_act")] transientI 1);
7.86 +by (auto_tac (claset(),
7.87 + simpset() addsimps [Domain_def, Client_def]));
7.88 +by (blast_tac (claset() addIs [less_le_trans, prefix_length_le,
7.89 + strict_prefix_length_less]) 1);
7.90 +by (auto_tac (claset(),
7.91 + simpset() addsimps [prefix_def, genPrefix_iff_nth, Ge_def]));
7.92 +by (blast_tac (claset() addIs [strict_prefix_length_less]) 1);
7.93 +qed "transient_lemma";
7.94 +
7.95 +
7.96 +Goal "[| Client Join G : Increasing giv; Client ok G |] \
7.97 +\ ==> Client Join G : {s. rel s = k & k<h & h <= giv s & h pfixGe ask s} \
7.98 +\ LeadsTo {s. k < rel s & rel s <= giv s & \
7.99 +\ h <= giv s & h pfixGe ask s}";
7.100 +by (rtac single_LeadsTo_I 1);
7.101 +by (ftac (increasing_ask_rel RS guaranteesD) 1);
7.102 +by Auto_tac;
7.103 +by (rtac (transient_lemma RS Join_transient_I1 RS transient_imp_leadsTo RS
7.104 + leadsTo_imp_LeadsTo RS PSP_Stable RS LeadsTo_weaken) 1);
7.105 +by (rtac (Stable_Int RS Stable_Int RS Stable_Int) 1);
7.106 +by (eres_inst_tac [("f", "giv"), ("x", "giv s")] IncreasingD 1);
7.107 +by (eres_inst_tac [("f", "ask"), ("x", "ask s")] IncreasingD 1);
7.108 +by (eres_inst_tac [("f", "rel"), ("x", "rel s")] IncreasingD 1);
7.109 +by (etac Join_Stable_rel_le_giv 1);
7.110 +by (Blast_tac 1);
7.111 +by (blast_tac (claset() addIs [sym, order_less_le RS iffD2,
7.112 + order_trans, prefix_imp_pfixGe,
7.113 + pfixGe_trans]) 2);
7.114 +by (blast_tac (claset() addIs [order_less_imp_le, order_trans]) 1);
7.115 +qed "induct_lemma";
7.116 +
7.117 +
7.118 +Goal "[| Client Join G : Increasing giv; Client ok G |] \
7.119 +\ ==> Client Join G : {s. rel s < h & h <= giv s & h pfixGe ask s} \
7.120 +\ LeadsTo {s. h <= rel s}";
7.121 +by (res_inst_tac [("f", "%s. size h - size (rel s)")] LessThan_induct 1);
7.122 +by (auto_tac (claset(), simpset() addsimps [vimage_def]));
7.123 +by (rtac single_LeadsTo_I 1);
7.124 +by (rtac (induct_lemma RS LeadsTo_weaken) 1);
7.125 +by Auto_tac;
7.126 +by (blast_tac (claset() addIs [order_less_le RS iffD2]
7.127 + addDs [common_prefix_linear]) 1);
7.128 +by (REPEAT (dtac strict_prefix_length_less 1));
7.129 +by (arith_tac 1);
7.130 +qed "rel_progress_lemma";
7.131 +
7.132 +
7.133 +Goal "[| Client Join G : Increasing giv; Client ok G |] \
7.134 +\ ==> Client Join G : {s. h <= giv s & h pfixGe ask s} \
7.135 +\ LeadsTo {s. h <= rel s}";
7.136 +by (rtac (Join_Always_rel_le_giv RS Always_LeadsToI) 1);
7.137 +by (rtac ([rel_progress_lemma, subset_refl RS subset_imp_LeadsTo] MRS
7.138 + LeadsTo_Un RS LeadsTo_weaken_L) 3);
7.139 +by Auto_tac;
7.140 +by (blast_tac (claset() addIs [order_less_le RS iffD2]
7.141 + addDs [common_prefix_linear]) 1);
7.142 +qed "client_progress_lemma";
7.143 +
7.144 +(*Progress property: all tokens that are given will be released*)
7.145 +Goal "Client : \
7.146 +\ Increasing giv guarantees \
7.147 +\ (INT h. {s. h <= giv s & h pfixGe ask s} LeadsTo {s. h <= rel s})";
7.148 +by (rtac guaranteesI 1);
7.149 +by (Clarify_tac 1);
7.150 +by (blast_tac (claset() addIs [client_progress_lemma]) 1);
7.151 +qed "client_progress";
7.152 +
7.153 +(*This shows that the Client won't alter other variables in any state
7.154 + that it is combined with*)
7.155 +Goal "Client : preserves dummy";
7.156 +by (rewtac preserves_def);
7.157 +by Auto_tac;
7.158 +by (constrains_tac 1);
7.159 +by Auto_tac;
7.160 +qed "client_preserves_dummy";
7.161 +
7.162 +
7.163 +(** Obsolete lemmas from first version of the Client **)
7.164 +
7.165 +Goal "Client: stable {s. size (rel s) <= size (giv s)}";
7.166 +by (constrains_tac 1);
7.167 +by Auto_tac;
7.168 +qed "stable_size_rel_le_giv";
7.169 +
7.170 +(*clients return the right number of tokens*)
7.171 +Goal "Client : Increasing giv guarantees Always {s. rel s <= giv s}";
7.172 +by (rtac guaranteesI 1);
7.173 +by (rtac AlwaysI 1);
7.174 +by (Force_tac 1);
7.175 +by (blast_tac (claset() addIs [Increasing_preserves_Stable,
7.176 + stable_rel_le_giv]) 1);
7.177 +qed "ok_guar_rel_prefix_giv";
8.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
8.2 +++ b/src/HOL/UNITY/Comp/Client.thy Mon Mar 05 15:32:54 2001 +0100
8.3 @@ -0,0 +1,66 @@
8.4 +(* Title: HOL/UNITY/Client.thy
8.5 + ID: $Id$
8.6 + Author: Lawrence C Paulson, Cambridge University Computer Laboratory
8.7 + Copyright 1998 University of Cambridge
8.8 +
8.9 +Distributed Resource Management System: the Client
8.10 +*)
8.11 +
8.12 +Client = Rename + AllocBase +
8.13 +
8.14 +types
8.15 + tokbag = nat (*tokbags could be multisets...or any ordered type?*)
8.16 +
8.17 +record state =
8.18 + giv :: tokbag list (*input history: tokens granted*)
8.19 + ask :: tokbag list (*output history: tokens requested*)
8.20 + rel :: tokbag list (*output history: tokens released*)
8.21 + tok :: tokbag (*current token request*)
8.22 +
8.23 +record 'a state_d =
8.24 + state +
8.25 + dummy :: 'a (*new variables*)
8.26 +
8.27 +
8.28 +(*Array indexing is translated to list indexing as A[n] == A!(n-1). *)
8.29 +
8.30 +constdefs
8.31 +
8.32 + (** Release some tokens **)
8.33 +
8.34 + rel_act :: "('a state_d * 'a state_d) set"
8.35 + "rel_act == {(s,s').
8.36 + EX nrel. nrel = size (rel s) &
8.37 + s' = s (| rel := rel s @ [giv s!nrel] |) &
8.38 + nrel < size (giv s) &
8.39 + ask s!nrel <= giv s!nrel}"
8.40 +
8.41 + (** Choose a new token requirement **)
8.42 +
8.43 + (** Including s'=s suppresses fairness, allowing the non-trivial part
8.44 + of the action to be ignored **)
8.45 +
8.46 + tok_act :: "('a state_d * 'a state_d) set"
8.47 + "tok_act == {(s,s'). s'=s | s' = s (|tok := Suc (tok s mod NbT) |)}"
8.48 +
8.49 + ask_act :: "('a state_d * 'a state_d) set"
8.50 + "ask_act == {(s,s'). s'=s |
8.51 + (s' = s (|ask := ask s @ [tok s]|))}"
8.52 +
8.53 + Client :: 'a state_d program
8.54 + "Client ==
8.55 + mk_program ({s. tok s : atMost NbT &
8.56 + giv s = [] & ask s = [] & rel s = []},
8.57 + {rel_act, tok_act, ask_act},
8.58 + UN G: preserves rel Int preserves ask Int preserves tok.
8.59 + Acts G)"
8.60 +
8.61 + (*Maybe want a special theory section to declare such maps*)
8.62 + non_dummy :: 'a state_d => state
8.63 + "non_dummy s == (|giv = giv s, ask = ask s, rel = rel s, tok = tok s|)"
8.64 +
8.65 + (*Renaming map to put a Client into the standard form*)
8.66 + client_map :: "'a state_d => state*'a"
8.67 + "client_map == funPair non_dummy dummy"
8.68 +
8.69 +end
9.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
9.2 +++ b/src/HOL/UNITY/Comp/Counter.ML Mon Mar 05 15:32:54 2001 +0100
9.3 @@ -0,0 +1,140 @@
9.4 +(* Title: HOL/UNITY/Counter
9.5 + ID: $Id$
9.6 + Author: Sidi O Ehmety, Cambridge University Computer Laboratory
9.7 + Copyright 2001 University of Cambridge
9.8 +
9.9 +A family of similar counters, version close to the original.
9.10 +
9.11 +From Charpentier and Chandy,
9.12 +Examples of Program Composition Illustrating the Use of Universal Properties
9.13 + In J. Rolim (editor), Parallel and Distributed Processing,
9.14 + Spriner LNCS 1586 (1999), pages 1215-1227.
9.15 +*)
9.16 +
9.17 +Addsimps [Component_def RS def_prg_Init];
9.18 +program_defs_ref := [Component_def];
9.19 +Addsimps (map simp_of_act [a_def]);
9.20 +
9.21 +(* Theorems about sum and sumj *)
9.22 +Goal "ALL n. I<n --> sum I (s(c n := x)) = sum I s";
9.23 +by (induct_tac "I" 1);
9.24 +by Auto_tac;
9.25 +qed_spec_mp "sum_upd_gt";
9.26 +
9.27 +
9.28 +Goal "sum I (s(c I := x)) = sum I s";
9.29 +by (induct_tac "I" 1);
9.30 +by Auto_tac;
9.31 +by (simp_tac (simpset()
9.32 + addsimps [rewrite_rule [fun_upd_def] sum_upd_gt]) 1);
9.33 +qed "sum_upd_eq";
9.34 +
9.35 +Goal "sum I (s(C := x)) = sum I s";
9.36 +by (induct_tac "I" 1);
9.37 +by Auto_tac;
9.38 +qed "sum_upd_C";
9.39 +
9.40 +Goal "sumj I i (s(c i := x)) = sumj I i s";
9.41 +by (induct_tac "I" 1);
9.42 +by Auto_tac;
9.43 +by (simp_tac (simpset() addsimps
9.44 + [rewrite_rule [fun_upd_def] sum_upd_eq]) 1);
9.45 +qed "sumj_upd_ci";
9.46 +
9.47 +Goal "sumj I i (s(C := x)) = sumj I i s";
9.48 +by (induct_tac "I" 1);
9.49 +by Auto_tac;
9.50 +by (simp_tac (simpset()
9.51 + addsimps [rewrite_rule [fun_upd_def] sum_upd_C]) 1);
9.52 +qed "sumj_upd_C";
9.53 +
9.54 +Goal "ALL i. I<i--> (sumj I i s = sum I s)";
9.55 +by (induct_tac "I" 1);
9.56 +by Auto_tac;
9.57 +qed_spec_mp "sumj_sum_gt";
9.58 +
9.59 +Goal "(sumj I I s = sum I s)";
9.60 +by (induct_tac "I" 1);
9.61 +by Auto_tac;
9.62 +by (simp_tac (simpset() addsimps [sumj_sum_gt]) 1);
9.63 +qed "sumj_sum_eq";
9.64 +
9.65 +Goal "ALL i. i<I-->(sum I s = s (c i) + sumj I i s)";
9.66 +by (induct_tac "I" 1);
9.67 +by (auto_tac (claset(), simpset() addsimps [linorder_neq_iff, sumj_sum_eq]));
9.68 +qed_spec_mp "sum_sumj";
9.69 +
9.70 +(* Correctness proofs for Components *)
9.71 +(* p2 and p3 proofs *)
9.72 +Goal "Component i : stable {s. s C = s (c i) + k}";
9.73 +by (constrains_tac 1);
9.74 +qed "p2";
9.75 +
9.76 +Goal
9.77 +"Component i: stable {s. ALL v. v~=c i & v~=C --> s v = k v}";
9.78 +by (constrains_tac 1);
9.79 +qed "p3";
9.80 +
9.81 +
9.82 +Goal
9.83 +"(ALL k. Component i: stable ({s. s C = s (c i) + sumj I i k} \
9.84 +\ Int {s. ALL v. v~=c i & v~=C --> s v = k v})) \
9.85 +\ = (Component i: stable {s. s C = s (c i) + sumj I i s})";
9.86 +by (auto_tac (claset(), simpset()
9.87 + addsimps [constrains_def, stable_def,Component_def,
9.88 + sumj_upd_C, sumj_upd_ci]));
9.89 +qed "p2_p3_lemma1";
9.90 +
9.91 +Goal
9.92 +"ALL k. Component i: stable ({s. s C = s (c i) + sumj I i k} Int \
9.93 +\ {s. ALL v. v~=c i & v~=C --> s v = k v})";
9.94 +by (blast_tac (claset() addIs [[p2, p3] MRS stable_Int]) 1);
9.95 +qed "p2_p3_lemma2";
9.96 +
9.97 +
9.98 +Goal
9.99 +"Component i: stable {s. s C = s (c i) + sumj I i s}";
9.100 +by (auto_tac (claset() addSIs [p2_p3_lemma2],
9.101 + simpset() addsimps [p2_p3_lemma1 RS sym]));
9.102 +qed "p2_p3";
9.103 +
9.104 +(* Compositional Proof *)
9.105 +
9.106 +Goal "(ALL i. i < I --> s (c i) = #0) --> sum I s = #0";
9.107 +by (induct_tac "I" 1);
9.108 +by Auto_tac;
9.109 +qed "sum_0'";
9.110 +val sum0_lemma = (sum_0' RS mp) RS sym;
9.111 +
9.112 +(* I could'nt be empty *)
9.113 +Goalw [invariant_def]
9.114 +"!!I. 0<I ==> (JN i:{i. i<I}. Component i):invariant {s. s C = sum I s}";
9.115 +by (simp_tac (simpset() addsimps [JN_stable,Init_JN,sum_sumj]) 1);
9.116 +by (force_tac (claset() addIs [p2_p3, sum0_lemma RS sym], simpset()) 1);
9.117 +qed "safety";
9.118 +
9.119 +
9.120 +
9.121 +
9.122 +
9.123 +
9.124 +
9.125 +
9.126 +
9.127 +
9.128 +
9.129 +
9.130 +
9.131 +
9.132 +
9.133 +
9.134 +
9.135 +
9.136 +
9.137 +
9.138 +
9.139 +
9.140 +
9.141 +
9.142 +
9.143 +
10.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
10.2 +++ b/src/HOL/UNITY/Comp/Counter.thy Mon Mar 05 15:32:54 2001 +0100
10.3 @@ -0,0 +1,41 @@
10.4 +(* Title: HOL/UNITY/Counter
10.5 + ID: $Id$
10.6 + Author: Sidi O Ehmety, Cambridge University Computer Laboratory
10.7 + Copyright 2001 University of Cambridge
10.8 +
10.9 +A family of similar counters, version close to the original.
10.10 +
10.11 +From Charpentier and Chandy,
10.12 +Examples of Program Composition Illustrating the Use of Universal Properties
10.13 + In J. Rolim (editor), Parallel and Distributed Processing,
10.14 + Spriner LNCS 1586 (1999), pages 1215-1227.
10.15 +*)
10.16 +
10.17 +Counter = Comp +
10.18 +(* Variables are names *)
10.19 +datatype name = C | c nat
10.20 +types state = name=>int
10.21 +
10.22 +consts
10.23 + sum :: "[nat,state]=>int"
10.24 + sumj :: "[nat, nat, state]=>int"
10.25 +
10.26 +primrec (* sum I s = sigma_{i<I}. s (c i) *)
10.27 + "sum 0 s = #0"
10.28 + "sum (Suc i) s = s (c i) + sum i s"
10.29 +
10.30 +primrec
10.31 + "sumj 0 i s = #0"
10.32 + "sumj (Suc n) i s = (if n=i then sum n s else s (c n) + sumj n i s)"
10.33 +
10.34 +types command = "(state*state)set"
10.35 +
10.36 +constdefs
10.37 + a :: "nat=>command"
10.38 + "a i == {(s, s'). s'=s(c i:= s (c i) + #1, C:= s C + #1)}"
10.39 +
10.40 + Component :: "nat => state program"
10.41 + "Component i ==
10.42 + mk_program({s. s C = #0 & s (c i) = #0}, {a i},
10.43 + UN G: preserves (%s. s (c i)). Acts G)"
10.44 +end
11.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
11.2 +++ b/src/HOL/UNITY/Comp/Counterc.ML Mon Mar 05 15:32:54 2001 +0100
11.3 @@ -0,0 +1,124 @@
11.4 +(* Title: HOL/UNITY/Counterc
11.5 + ID: $Id$
11.6 + Author: Sidi O Ehmety, Cambridge University Computer Laboratory
11.7 + Copyright 2001 University of Cambridge
11.8 +
11.9 +A family of similar counters, version with a full use of "compatibility "
11.10 +
11.11 +From Charpentier and Chandy,
11.12 +Examples of Program Composition Illustrating the Use of Universal Properties
11.13 + In J. Rolim (editor), Parallel and Distributed Processing,
11.14 + Spriner LNCS 1586 (1999), pages 1215-1227.
11.15 +*)
11.16 +
11.17 +Addsimps [Component_def RS def_prg_Init,
11.18 +Component_def RS def_prg_AllowedActs];
11.19 +program_defs_ref := [Component_def];
11.20 +Addsimps (map simp_of_act [a_def]);
11.21 +
11.22 +(* Theorems about sum and sumj *)
11.23 +Goal "ALL i. I<i--> (sum I s = sumj I i s)";
11.24 +by (induct_tac "I" 1);
11.25 +by Auto_tac;
11.26 +qed_spec_mp "sum_sumj_eq1";
11.27 +
11.28 +Goal "i<I --> sum I s = c s i + sumj I i s";
11.29 +by (induct_tac "I" 1);
11.30 +by (auto_tac (claset(), simpset() addsimps [linorder_neq_iff, sum_sumj_eq1]));
11.31 +qed_spec_mp "sum_sumj_eq2";
11.32 +
11.33 +Goal "(ALL i. i<I --> c s' i = c s i) --> (sum I s' = sum I s)";
11.34 +by (induct_tac "I" 1 THEN Auto_tac);
11.35 +qed_spec_mp "sum_ext";
11.36 +
11.37 +Goal "(ALL j. j<I & j~=i --> c s' j = c s j) --> (sumj I i s' = sumj I i s)";
11.38 +by (induct_tac "I" 1);
11.39 +by Safe_tac;
11.40 +by (auto_tac (claset() addSIs [sum_ext], simpset()));
11.41 +qed_spec_mp "sumj_ext";
11.42 +
11.43 +
11.44 +Goal "(ALL i. i<I --> c s i = #0) --> sum I s = #0";
11.45 +by (induct_tac "I" 1);
11.46 +by Auto_tac;
11.47 +qed "sum0";
11.48 +
11.49 +
11.50 +(* Safety properties for Components *)
11.51 +
11.52 +Goal "(Component i ok G) = \
11.53 +\ (G: preserves (%s. c s i) & Component i:Allowed G)";
11.54 +by (auto_tac (claset(),
11.55 + simpset() addsimps [ok_iff_Allowed, Component_def RS def_prg_Allowed]));
11.56 +qed "Component_ok_iff";
11.57 +AddIffs [Component_ok_iff];
11.58 +AddIffs [OK_iff_ok];
11.59 +Addsimps [preserves_def];
11.60 +
11.61 +
11.62 +Goal "Component i: stable {s. C s = (c s) i + k}";
11.63 +by (constrains_tac 1);
11.64 +qed "p2";
11.65 +
11.66 +Goal "[| OK I Component; i:I |] \
11.67 +\ ==> Component i: stable {s. ALL j:I. j~=i --> c s j = c k j}";
11.68 +by (full_simp_tac (simpset() addsimps [stable_def, constrains_def]) 1);
11.69 +by (Blast_tac 1);
11.70 +qed "p3";
11.71 +
11.72 +
11.73 +Goal
11.74 +"[| OK {i. i<I} Component; i<I |] ==> \
11.75 +\ ALL k. Component i: stable ({s. C s = c s i + sumj I i k} Int \
11.76 +\ {s. ALL j:{i. i<I}. j~=i --> c s j = c k j})";
11.77 +by (blast_tac (claset() addIs [[p2, p3] MRS stable_Int]) 1);
11.78 +qed "p2_p3_lemma1";
11.79 +
11.80 +
11.81 +Goal "(ALL k. F:stable ({s. C s = (c s) i + sumj I i k} Int \
11.82 +\ {s. ALL j:{i. i<I}. j~=i --> c s j = c k j})) \
11.83 +\ ==> (F:stable {s. C s = c s i + sumj I i s})";
11.84 +by (full_simp_tac (simpset() addsimps [constrains_def, stable_def]) 1);
11.85 +by (force_tac (claset() addSIs [sumj_ext], simpset()) 1);
11.86 +qed "p2_p3_lemma2";
11.87 +
11.88 +
11.89 +Goal "[| OK {i. i<I} Component; i<I |] \
11.90 +\ ==> Component i: stable {s. C s = c s i + sumj I i s}";
11.91 +by (blast_tac (claset() addIs [p2_p3_lemma1 RS p2_p3_lemma2]) 1);
11.92 +qed "p2_p3";
11.93 +
11.94 +
11.95 +(* Compositional correctness *)
11.96 +Goalw [invariant_def]
11.97 + "[| 0<I; OK {i. i<I} Component |] \
11.98 +\ ==> (JN i:{i. i<I}. (Component i)) : invariant {s. C s = sum I s}";
11.99 +by (simp_tac (simpset() addsimps [JN_stable, sum_sumj_eq2]) 1);
11.100 +by (auto_tac (claset() addSIs [sum0 RS mp, p2_p3],
11.101 + simpset()));
11.102 +qed "safety";
11.103 +
11.104 +
11.105 +
11.106 +
11.107 +
11.108 +
11.109 +
11.110 +
11.111 +
11.112 +
11.113 +
11.114 +
11.115 +
11.116 +
11.117 +
11.118 +
11.119 +
11.120 +
11.121 +
11.122 +
11.123 +
11.124 +
11.125 +
11.126 +
11.127 +
12.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
12.2 +++ b/src/HOL/UNITY/Comp/Counterc.thy Mon Mar 05 15:32:54 2001 +0100
12.3 @@ -0,0 +1,43 @@
12.4 +(* Title: HOL/UNITY/Counterc
12.5 + ID: $Id$
12.6 + Author: Sidi O Ehmety, Cambridge University Computer Laboratory
12.7 + Copyright 2001 University of Cambridge
12.8 +
12.9 +A family of similar counters, version with a full use of "compatibility "
12.10 +
12.11 +From Charpentier and Chandy,
12.12 +Examples of Program Composition Illustrating the Use of Universal Properties
12.13 + In J. Rolim (editor), Parallel and Distributed Processing,
12.14 + Spriner LNCS 1586 (1999), pages 1215-1227.
12.15 +*)
12.16 +
12.17 +Counterc = Comp +
12.18 +types state
12.19 +arities state :: term
12.20 +
12.21 +consts
12.22 + C :: "state=>int"
12.23 + c :: "state=>nat=>int"
12.24 +
12.25 +consts
12.26 + sum :: "[nat,state]=>int"
12.27 + sumj :: "[nat, nat, state]=>int"
12.28 +
12.29 +primrec (* sum I s = sigma_{i<I}. c s i *)
12.30 + "sum 0 s = #0"
12.31 + "sum (Suc i) s = (c s) i + sum i s"
12.32 +
12.33 +primrec
12.34 + "sumj 0 i s = #0"
12.35 + "sumj (Suc n) i s = (if n=i then sum n s else (c s) n + sumj n i s)"
12.36 +
12.37 +types command = "(state*state)set"
12.38 +
12.39 +constdefs
12.40 + a :: "nat=>command"
12.41 + "a i == {(s, s'). (c s') i = (c s) i + #1 & (C s') = (C s) + #1}"
12.42 +
12.43 + Component :: "nat => state program"
12.44 + "Component i == mk_program({s. C s = #0 & (c s) i = #0}, {a i},
12.45 + UN G: preserves (%s. (c s) i). Acts G)"
12.46 +end
13.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
13.2 +++ b/src/HOL/UNITY/Comp/Handshake.ML Mon Mar 05 15:32:54 2001 +0100
13.3 @@ -0,0 +1,49 @@
13.4 +(* Title: HOL/UNITY/Handshake
13.5 + ID: $Id$
13.6 + Author: Lawrence C Paulson, Cambridge University Computer Laboratory
13.7 + Copyright 1998 University of Cambridge
13.8 +
13.9 +Handshake Protocol
13.10 +
13.11 +From Misra, "Asynchronous Compositions of Programs", Section 5.3.2
13.12 +*)
13.13 +
13.14 +Addsimps [F_def RS def_prg_Init, G_def RS def_prg_Init];
13.15 +program_defs_ref := [F_def, G_def];
13.16 +
13.17 +Addsimps (map simp_of_act [cmdF_def, cmdG_def]);
13.18 +Addsimps [simp_of_set invFG_def];
13.19 +
13.20 +
13.21 +Goal "(F Join G) : Always invFG";
13.22 +by (rtac AlwaysI 1);
13.23 +by (Force_tac 1);
13.24 +by (rtac (constrains_imp_Constrains RS StableI) 1);
13.25 +by Auto_tac;
13.26 +by (constrains_tac 2);
13.27 +by (auto_tac (claset() addIs [order_antisym] addSEs [le_SucE], simpset()));
13.28 +by (constrains_tac 1);
13.29 +qed "invFG";
13.30 +
13.31 +Goal "(F Join G) : ({s. NF s = k} - {s. BB s}) LeadsTo \
13.32 +\ ({s. NF s = k} Int {s. BB s})";
13.33 +by (rtac (stable_Join_ensures1 RS leadsTo_Basis RS leadsTo_imp_LeadsTo) 1);
13.34 +by (ensures_tac "cmdG" 2);
13.35 +by (constrains_tac 1);
13.36 +qed "lemma2_1";
13.37 +
13.38 +Goal "(F Join G) : ({s. NF s = k} Int {s. BB s}) LeadsTo {s. k < NF s}";
13.39 +by (rtac (stable_Join_ensures2 RS leadsTo_Basis RS leadsTo_imp_LeadsTo) 1);
13.40 +by (constrains_tac 2);
13.41 +by (ensures_tac "cmdF" 1);
13.42 +qed "lemma2_2";
13.43 +
13.44 +Goal "(F Join G) : UNIV LeadsTo {s. m < NF s}";
13.45 +by (rtac LeadsTo_weaken_R 1);
13.46 +by (res_inst_tac [("f", "NF"), ("l","Suc m"), ("B","{}")]
13.47 + GreaterThan_bounded_induct 1);
13.48 +(*The inductive step is (F Join G) : {x. NF x = ma} LeadsTo {x. ma < NF x}*)
13.49 +by (auto_tac (claset() addSIs [lemma2_1, lemma2_2]
13.50 + addIs[LeadsTo_Trans, LeadsTo_Diff],
13.51 + simpset() addsimps [vimage_def]));
13.52 +qed "progress";
14.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
14.2 +++ b/src/HOL/UNITY/Comp/Handshake.thy Mon Mar 05 15:32:54 2001 +0100
14.3 @@ -0,0 +1,37 @@
14.4 +(* Title: HOL/UNITY/Handshake.thy
14.5 + ID: $Id$
14.6 + Author: Lawrence C Paulson, Cambridge University Computer Laboratory
14.7 + Copyright 1998 University of Cambridge
14.8 +
14.9 +Handshake Protocol
14.10 +
14.11 +From Misra, "Asynchronous Compositions of Programs", Section 5.3.2
14.12 +*)
14.13 +
14.14 +Handshake = Union +
14.15 +
14.16 +record state =
14.17 + BB :: bool
14.18 + NF :: nat
14.19 + NG :: nat
14.20 +
14.21 +constdefs
14.22 + (*F's program*)
14.23 + cmdF :: "(state*state) set"
14.24 + "cmdF == {(s,s'). s' = s (|NF:= Suc(NF s), BB:=False|) & BB s}"
14.25 +
14.26 + F :: "state program"
14.27 + "F == mk_program ({s. NF s = 0 & BB s}, {cmdF}, UNIV)"
14.28 +
14.29 + (*G's program*)
14.30 + cmdG :: "(state*state) set"
14.31 + "cmdG == {(s,s'). s' = s (|NG:= Suc(NG s), BB:=True|) & ~ BB s}"
14.32 +
14.33 + G :: "state program"
14.34 + "G == mk_program ({s. NG s = 0 & BB s}, {cmdG}, UNIV)"
14.35 +
14.36 + (*the joint invariant*)
14.37 + invFG :: "state set"
14.38 + "invFG == {s. NG s <= NF s & NF s <= Suc (NG s) & (BB s = (NF s = NG s))}"
14.39 +
14.40 +end
15.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
15.2 +++ b/src/HOL/UNITY/Comp/Priority.ML Mon Mar 05 15:32:54 2001 +0100
15.3 @@ -0,0 +1,239 @@
15.4 +(* Title: HOL/UNITY/Priority
15.5 + ID: $Id$
15.6 + Author: Sidi O Ehmety, Cambridge University Computer Laboratory
15.7 + Copyright 2001 University of Cambridge
15.8 +
15.9 +The priority system
15.10 +
15.11 +From Charpentier and Chandy,
15.12 +Examples of Program Composition Illustrating the Use of Universal Properties
15.13 + In J. Rolim (editor), Parallel and Distributed Processing,
15.14 + Spriner LNCS 1586 (1999), pages 1215-1227.
15.15 +*)
15.16 +
15.17 +Addsimps [Component_def RS def_prg_Init];
15.18 +program_defs_ref := [Component_def, system_def];
15.19 +Addsimps [highest_def, lowest_def];
15.20 +Addsimps [simp_of_act act_def];
15.21 +Addsimps (map simp_of_set [Highest_def, Lowest_def]);
15.22 +
15.23 +
15.24 +
15.25 +
15.26 +(**** Component correctness proofs ****)
15.27 +
15.28 +(* neighbors is stable *)
15.29 +Goal "Component i: stable {s. neighbors k s = n}";
15.30 +by (constrains_tac 1);
15.31 +by Auto_tac;
15.32 +qed "Component_neighbors_stable";
15.33 +
15.34 +(* property 4 *)
15.35 +Goal
15.36 +"Component i: {s. ((i,j):s) = b} Int (- Highest i) co {s. ((i,j):s)=b}";
15.37 +by (constrains_tac 1);
15.38 +qed "Component_waits_priority";
15.39 +
15.40 +(* property 5: charpentier and Chandy mistakenly express it as
15.41 + 'transient Highest i'. Consider the case where i has neighbors *)
15.42 +Goal
15.43 + "Component i: {s. neighbors i s ~= {}} Int Highest i \
15.44 +\ ensures - Highest i";
15.45 +by (ensures_tac "act i" 1);
15.46 +by (REPEAT(Fast_tac 1));
15.47 +qed "Component_yields_priority";
15.48 +
15.49 +(* or better *)
15.50 +Goal "Component i: Highest i ensures Lowest i";
15.51 +by (ensures_tac "act i" 1);
15.52 +by (REPEAT(Fast_tac 1));
15.53 +qed "Component_yields_priority'";
15.54 +
15.55 +(* property 6: Component doesn't introduce cycle *)
15.56 +Goal "Component i: Highest i co Highest i Un Lowest i";
15.57 +by (constrains_tac 1);
15.58 +by (Fast_tac 1);
15.59 +qed "Component_well_behaves";
15.60 +
15.61 +(* property 7: local axiom *)
15.62 +Goal "Component i: stable {s. ALL j k. j~=i & k~=i--> ((j,k):s) = b j k}";
15.63 +by (constrains_tac 1);
15.64 +qed "locality";
15.65 +
15.66 +
15.67 +(**** System properties ****)
15.68 +(* property 8: strictly universal *)
15.69 +
15.70 +Goalw [Safety_def]
15.71 + "system: stable Safety";
15.72 +by (rtac stable_INT 1);
15.73 +by (constrains_tac 1);
15.74 +by (Fast_tac 1);
15.75 +qed "Safety";
15.76 +
15.77 +(* property 13: universal *)
15.78 +Goal
15.79 +"system: {s. s = q} co {s. s=q} Un {s. EX i. derive i q s}";
15.80 +by (constrains_tac 1);
15.81 +by (Blast_tac 1);
15.82 +qed "p13";
15.83 +
15.84 +(* property 14: the 'above set' of a Component that hasn't got
15.85 + priority doesn't increase *)
15.86 +Goal
15.87 +"ALL j. system: -Highest i Int {s. j~:above i s} co {s. j~:above i s}";
15.88 +by (Clarify_tac 1);
15.89 +by (cut_inst_tac [("i", "j")] reach_lemma 1);
15.90 +by (constrains_tac 1);
15.91 +by (auto_tac (claset(), simpset() addsimps [trancl_converse]));
15.92 +qed "above_not_increase";
15.93 +
15.94 +Goal
15.95 +"system: -Highest i Int {s. above i s = x} co {s. above i s <= x}";
15.96 +by (cut_inst_tac [("i", "i")] above_not_increase 1);
15.97 +by (asm_full_simp_tac (simpset() addsimps
15.98 + [trancl_converse, constrains_def]) 1);
15.99 +by (Blast_tac 1);
15.100 +qed "above_not_increase'";
15.101 +
15.102 +
15.103 +
15.104 +(* p15: universal property: all Components well behave *)
15.105 +Goal "ALL i. system: Highest i co Highest i Un Lowest i";
15.106 +by (Clarify_tac 1);
15.107 +by (constrains_tac 1);
15.108 +by Auto_tac;
15.109 +qed "system_well_behaves";
15.110 +
15.111 +
15.112 +Goal "Acyclic = (INT i. {s. i~:above i s})";
15.113 +by (auto_tac (claset(), simpset()
15.114 + addsimps [Acyclic_def, acyclic_def, trancl_converse]));
15.115 +qed "Acyclic_eq";
15.116 +
15.117 +
15.118 +val lemma = [above_not_increase RS spec,
15.119 + system_well_behaves RS spec] MRS constrains_Un;
15.120 +Goal
15.121 +"system: stable Acyclic";
15.122 +by (auto_tac (claset() addSIs [stable_INT, stableI,
15.123 + lemma RS constrains_weaken],
15.124 + simpset() addsimps [Acyclic_eq,
15.125 + image0_r_iff_image0_trancl,trancl_converse]));
15.126 +qed "Acyclic_stable";
15.127 +
15.128 +
15.129 +Goalw [Acyclic_def, Maximal_def]
15.130 +"Acyclic <= Maximal";
15.131 +by (Clarify_tac 1);
15.132 +by (dtac above_lemma_b 1);
15.133 +by Auto_tac;
15.134 +qed "Acyclic_subset_Maximal";
15.135 +
15.136 +(* property 17: original one is an invariant *)
15.137 +Goal
15.138 +"system: stable (Acyclic Int Maximal)";
15.139 +by (simp_tac (simpset() addsimps
15.140 + [Acyclic_subset_Maximal RS Int_absorb2, Acyclic_stable]) 1);
15.141 +qed "Acyclic_Maximal_stable";
15.142 +
15.143 +
15.144 +(* propert 5: existential property *)
15.145 +
15.146 +Goal "system: Highest i leadsTo Lowest i";
15.147 +by (ensures_tac "act i" 1);
15.148 +by (auto_tac (claset(), simpset() addsimps [Component_def]));
15.149 +qed "Highest_leadsTo_Lowest";
15.150 +
15.151 +(* a lowest i can never be in any abover set *)
15.152 +Goal "Lowest i <= (INT k. {s. i~:above k s})";
15.153 +by (auto_tac (claset(),
15.154 + simpset() addsimps [image0_r_iff_image0_trancl, trancl_converse]));
15.155 +qed "Lowest_above_subset";
15.156 +
15.157 +(* property 18: a simpler proof than the original, one which uses psp *)
15.158 +Goal "system: Highest i leadsTo (INT k. {s. i~:above k s})";
15.159 +by (rtac leadsTo_weaken_R 1);
15.160 +by (rtac Lowest_above_subset 2);
15.161 +by (rtac Highest_leadsTo_Lowest 1);
15.162 +qed "Highest_escapes_above";
15.163 +
15.164 +Goal
15.165 +"system: Highest j Int {s. j:above i s} leadsTo {s. j~:above i s}";
15.166 +by (blast_tac (claset() addIs
15.167 + [[Highest_escapes_above, Int_lower1, INT_lower] MRS leadsTo_weaken]) 1);
15.168 +qed "Highest_escapes_above'";
15.169 +
15.170 +(*** The main result: above set decreases ***)
15.171 +(* The original proof of the following formula was wrong *)
15.172 +val above_decreases_lemma =
15.173 +[Highest_escapes_above', above_not_increase'] MRS psp RS leadsTo_weaken;
15.174 +
15.175 +Goal "Highest i = {s. above i s ={}}";
15.176 +by (auto_tac (claset(),
15.177 + simpset() addsimps [image0_trancl_iff_image0_r]));
15.178 +qed "Highest_iff_above0";
15.179 +
15.180 +
15.181 +Goal
15.182 +"system: (UN j. {s. above i s = x} Int {s. j:above i s} Int Highest j) \
15.183 +\ leadsTo {s. above i s < x}";
15.184 +by (rtac leadsTo_UN 1);
15.185 +by (rtac single_leadsTo_I 1);
15.186 +by (Clarify_tac 1);
15.187 +by (res_inst_tac [("x2", "above i x")] above_decreases_lemma 1);
15.188 +by (ALLGOALS(full_simp_tac (simpset() delsimps [Highest_def]
15.189 + addsimps [Highest_iff_above0])));
15.190 +by (REPEAT(Blast_tac 1));
15.191 +qed "above_decreases";
15.192 +
15.193 +(** Just a massage of conditions to have the desired form ***)
15.194 +Goalw [Maximal_def, Maximal'_def, Highest_def]
15.195 +"Maximal = Maximal'";
15.196 +by (Blast_tac 1);
15.197 +qed "Maximal_eq_Maximal'";
15.198 +
15.199 +Goal "x~={} ==> \
15.200 +\ Acyclic Int {s. above i s = x} <= \
15.201 +\ (UN j. {s. above i s = x} Int {s. j:above i s} Int Highest j)";
15.202 +by (res_inst_tac [("B", "Maximal' Int {s. above i s = x}")] subset_trans 1);
15.203 +by (simp_tac (simpset() addsimps [Maximal_eq_Maximal' RS sym]) 1);
15.204 +by (blast_tac (claset() addIs [Acyclic_subset_Maximal RS subsetD]) 1);
15.205 +by (simp_tac (simpset() delsimps [above_def] addsimps [Maximal'_def, Highest_iff_above0]) 1);
15.206 +by (Blast_tac 1);
15.207 +qed "Acyclic_subset";
15.208 +
15.209 +val above_decreases' = [above_decreases, Acyclic_subset] MRS leadsTo_weaken_L;
15.210 +val above_decreases_psp = [above_decreases', Acyclic_stable] MRS psp_stable;
15.211 +
15.212 +Goal
15.213 +"x~={}==> \
15.214 +\ system: Acyclic Int {s. above i s = x} leadsTo Acyclic Int {s. above i s < x}";
15.215 +by (etac (above_decreases_psp RS leadsTo_weaken) 1);
15.216 +by (Blast_tac 1);
15.217 +by Auto_tac;
15.218 +qed "above_decreases_psp'";
15.219 +
15.220 +
15.221 +val finite_psubset_induct = wf_finite_psubset RS leadsTo_wf_induct;
15.222 +val leadsTo_weaken_L' = rotate_prems 1 leadsTo_weaken_L;
15.223 +
15.224 +
15.225 +Goal "system: Acyclic leadsTo Highest i";
15.226 +by (res_inst_tac [("f", "%s. above i s")] finite_psubset_induct 1);
15.227 +by (asm_simp_tac (simpset() delsimps [Highest_def, above_def]
15.228 + addsimps [Highest_iff_above0,
15.229 + vimage_def, finite_psubset_def]) 1);
15.230 +by (Clarify_tac 1);
15.231 +by (case_tac "m={}" 1);
15.232 +by (rtac (Int_lower2 RS leadsTo_weaken_L') 1);
15.233 +by (force_tac (claset(), simpset() addsimps [leadsTo_refl]) 1);
15.234 +by (res_inst_tac [("A'", "Acyclic Int {x. above i x < m}")]
15.235 + leadsTo_weaken_R 1);
15.236 +by (REPEAT(blast_tac (claset() addIs [above_decreases_psp']) 1));
15.237 +qed "Progress";
15.238 +
15.239 +(* We have proved all (relevant) theorems given in the paper *)
15.240 +(* We didn't assume any thing about the relation r *)
15.241 +(* It is not necessary that r be a priority relation as assumed in the original proof *)
15.242 +(* It suffices that we start from a state which is finite and acyclic *)
16.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
16.2 +++ b/src/HOL/UNITY/Comp/Priority.thy Mon Mar 05 15:32:54 2001 +0100
16.3 @@ -0,0 +1,68 @@
16.4 +(* Title: HOL/UNITY/Priority
16.5 + ID: $Id$
16.6 + Author: Sidi O Ehmety, Cambridge University Computer Laboratory
16.7 + Copyright 2001 University of Cambridge
16.8 +
16.9 +The priority system
16.10 +
16.11 +From Charpentier and Chandy,
16.12 +Examples of Program Composition Illustrating the Use of Universal Properties
16.13 + In J. Rolim (editor), Parallel and Distributed Processing,
16.14 + Spriner LNCS 1586 (1999), pages 1215-1227.
16.15 +*)
16.16 +
16.17 +Priority = PriorityAux + Comp + SubstAx +
16.18 +
16.19 +types state = "(vertex*vertex)set"
16.20 +types command = "vertex=>(state*state)set"
16.21 +
16.22 +consts
16.23 + (* the initial state *)
16.24 + init :: "(vertex*vertex)set"
16.25 +
16.26 +constdefs
16.27 + (* from the definitions given in section 4.4 *)
16.28 + (* i has highest priority in r *)
16.29 + highest :: "[vertex, (vertex*vertex)set]=>bool"
16.30 + "highest i r == A i r = {}"
16.31 +
16.32 + (* i has lowest priority in r *)
16.33 + lowest :: "[vertex, (vertex*vertex)set]=>bool"
16.34 + "lowest i r == R i r = {}"
16.35 +
16.36 + act :: command
16.37 + "act i == {(s, s'). s'=reverse i s & highest i s}"
16.38 +
16.39 + (* All components start with the same initial state *)
16.40 + Component :: "vertex=>state program"
16.41 + "Component i == mk_program({init}, {act i}, UNIV)"
16.42 +
16.43 + (* Abbreviations *)
16.44 + Highest :: "vertex=>state set"
16.45 + "Highest i == {s. highest i s}"
16.46 +
16.47 + Lowest :: "vertex=>state set"
16.48 + "Lowest i == {s. lowest i s}"
16.49 +
16.50 + Acyclic :: "state set"
16.51 + "Acyclic == {s. acyclic s}"
16.52 +
16.53 + (* Every above set has a maximal vertex: two equivalent defs. *)
16.54 +
16.55 + Maximal :: "state set"
16.56 + "Maximal == INT i. {s. ~highest i s-->(EX j:above i s. highest j s)}"
16.57 +
16.58 + Maximal' :: "state set"
16.59 + "Maximal' == INT i. Highest i Un (UN j. {s. j:above i s} Int Highest j)"
16.60 +
16.61 +
16.62 + Safety :: "state set"
16.63 + "Safety == INT i. {s. highest i s --> (ALL j:neighbors i s. ~highest j s)}"
16.64 +
16.65 +
16.66 + (* Composition of a finite set of component;
16.67 + the vertex 'UNIV' is finite by assumption *)
16.68 +
16.69 + system :: "state program"
16.70 + "system == JN i. Component i"
16.71 +end
16.72 \ No newline at end of file
17.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
17.2 +++ b/src/HOL/UNITY/Comp/PriorityAux.ML Mon Mar 05 15:32:54 2001 +0100
17.3 @@ -0,0 +1,116 @@
17.4 +(* Title: HOL/UNITY/PriorityAux
17.5 + ID: $Id$
17.6 + Author: Sidi O Ehmety, Cambridge University Computer Laboratory
17.7 + Copyright 2001 University of Cambridge
17.8 +
17.9 +Auxiliary definitions needed in Priority.thy
17.10 +*)
17.11 +
17.12 +Addsimps [derive_def, derive1_def, symcl_def, A_def, R_def,
17.13 + above_def, reach_def, reverse_def, neighbors_def];
17.14 +
17.15 +(*All vertex sets are finite \\<dots>*)
17.16 +AddIffs [[subset_UNIV, finite_vertex_univ] MRS finite_subset];
17.17 +
17.18 +(* and relatons over vertex are finite too *)
17.19 +AddIffs [[subset_UNIV, [finite_vertex_univ, finite_vertex_univ]
17.20 + MRS finite_Prod_UNIV] MRS finite_subset];
17.21 +
17.22 +
17.23 +(* The equalities (above i r = {}) = (A i r = {})
17.24 + and (reach i r = {}) = (R i r) rely on the following theorem *)
17.25 +
17.26 +Goal "((r^+)``{i} = {}) = (r``{i} = {})";
17.27 +by Auto_tac;
17.28 +by (etac trancl_induct 1);
17.29 +by Auto_tac;
17.30 +qed "image0_trancl_iff_image0_r";
17.31 +
17.32 +(* Another form usefull in some situation *)
17.33 +Goal "(r``{i}={}) = (ALL x. ((i,x):r^+) = False)";
17.34 +by Auto_tac;
17.35 +by (dtac (image0_trancl_iff_image0_r RS ssubst) 1);
17.36 +by Auto_tac;
17.37 +qed "image0_r_iff_image0_trancl";
17.38 +
17.39 +
17.40 +(* In finite universe acyclic coincides with wf *)
17.41 +Goal
17.42 +"!!r::(vertex*vertex)set. acyclic r = wf r";
17.43 +by (auto_tac (claset(), simpset() addsimps [wf_iff_acyclic_if_finite]));
17.44 +qed "acyclic_eq_wf";
17.45 +
17.46 +(* derive and derive1 are equivalent *)
17.47 +Goal "derive i r q = derive1 i r q";
17.48 +by Auto_tac;
17.49 +qed "derive_derive1_eq";
17.50 +
17.51 +(* Lemma 1 *)
17.52 +Goalw [reach_def]
17.53 +"[| x:reach i q; derive1 k r q |] ==> x~=k --> x:reach i r";
17.54 +by (etac ImageE 1);
17.55 +by (etac trancl_induct 1);
17.56 +by (case_tac "i=k" 1);
17.57 +by (auto_tac (claset() addIs [r_into_trancl], simpset()));
17.58 +by (dres_inst_tac [("x", "y")] spec 1);
17.59 +by (rotate_tac ~1 1);
17.60 +by (dres_inst_tac [("x", "z")] spec 1);
17.61 +by (auto_tac (claset() addDs [r_into_trancl] addIs [trancl_trans], simpset()));
17.62 +qed "lemma1_a";
17.63 +
17.64 +Goal "ALL k r q. derive k r q -->(reach i q <= (reach i r Un {k}))";
17.65 +by (REPEAT(rtac allI 1));
17.66 +by (rtac impI 1);
17.67 +by (rtac subsetI 1 THEN dtac lemma1_a 1);
17.68 +by (auto_tac (claset(), simpset() addsimps [derive_derive1_eq]
17.69 + delsimps [reach_def, derive_def, derive1_def]));
17.70 +qed "reach_lemma";
17.71 +
17.72 +(* An other possible formulation of the above theorem based on
17.73 + the equivalence x:reach y r = y:above x r *)
17.74 +Goal
17.75 +"(ALL i. reach i q <= (reach i r Un {k})) =\
17.76 +\ (ALL x. x~=k --> (ALL i. i~:above x r --> i~:above x q))";
17.77 +by (auto_tac (claset(), simpset() addsimps [trancl_converse]));
17.78 +qed "reach_above_lemma";
17.79 +
17.80 +(* Lemma 2 *)
17.81 +Goal
17.82 +"(z, i):r^+ ==> (ALL y. (y, z):r --> (y, i)~:r^+) = ((r^-1)``{z}={})";
17.83 +by Auto_tac;
17.84 +by (forw_inst_tac [("r", "r")] trancl_into_trancl2 1);
17.85 +by Auto_tac;
17.86 +qed "maximal_converse_image0";
17.87 +
17.88 +Goal
17.89 + "acyclic r ==> A i r~={}-->(EX j:above i r. A j r = {})";
17.90 +by (full_simp_tac (simpset()
17.91 + addsimps [acyclic_eq_wf, wf_eq_minimal]) 1);
17.92 +by (dres_inst_tac [("x", "((r^-1)^+)``{i}")] spec 1);
17.93 +by Auto_tac;
17.94 +by (rotate_tac ~1 1);
17.95 +by (asm_full_simp_tac (simpset()
17.96 + addsimps [maximal_converse_image0, trancl_converse]) 1);
17.97 +qed "above_lemma_a";
17.98 +
17.99 +
17.100 +Goal
17.101 + "acyclic r ==> above i r~={}-->(EX j:above i r. above j r = {})";
17.102 +by (dtac above_lemma_a 1);
17.103 +by (auto_tac (claset(), simpset()
17.104 + addsimps [image0_trancl_iff_image0_r]));
17.105 +qed "above_lemma_b";
17.106 +
17.107 +
17.108 +
17.109 +
17.110 +
17.111 +
17.112 +
17.113 +
17.114 +
17.115 +
17.116 +
17.117 +
17.118 +
17.119 +
18.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
18.2 +++ b/src/HOL/UNITY/Comp/PriorityAux.thy Mon Mar 05 15:32:54 2001 +0100
18.3 @@ -0,0 +1,53 @@
18.4 +(* Title: HOL/UNITY/PriorityAux
18.5 + ID: $Id$
18.6 + Author: Sidi O Ehmety, Cambridge University Computer Laboratory
18.7 + Copyright 2001 University of Cambridge
18.8 +
18.9 +Auxiliary definitions needed in Priority.thy
18.10 +*)
18.11 +
18.12 +PriorityAux = Main +
18.13 +
18.14 +types vertex
18.15 +arities vertex::term
18.16 +
18.17 +constdefs
18.18 + (* symmetric closure: removes the orientation of a relation *)
18.19 + symcl :: "(vertex*vertex)set=>(vertex*vertex)set"
18.20 + "symcl r == r Un (r^-1)"
18.21 +
18.22 + (* Neighbors of a vertex i *)
18.23 + neighbors :: "[vertex, (vertex*vertex)set]=>vertex set"
18.24 + "neighbors i r == ((r Un r^-1)``{i}) - {i}"
18.25 +
18.26 + R :: "[vertex, (vertex*vertex)set]=>vertex set"
18.27 + "R i r == r``{i}"
18.28 +
18.29 + A :: "[vertex, (vertex*vertex)set]=>vertex set"
18.30 + "A i r == (r^-1)``{i}"
18.31 +
18.32 + (* reachable and above vertices: the original notation was R* and A* *)
18.33 + reach :: "[vertex, (vertex*vertex)set]=> vertex set"
18.34 + "reach i r == (r^+)``{i}"
18.35 +
18.36 + above :: "[vertex, (vertex*vertex)set]=> vertex set"
18.37 + "above i r == ((r^-1)^+)``{i}"
18.38 +
18.39 + reverse :: "[vertex, (vertex*vertex) set]=>(vertex*vertex)set"
18.40 + "reverse i r == (r - {(x,y). x=i | y=i} Int r) Un ({(x,y). x=i|y=i} Int r)^-1"
18.41 +
18.42 + (* The original definition *)
18.43 + derive1 :: "[vertex, (vertex*vertex)set, (vertex*vertex)set]=>bool"
18.44 + "derive1 i r q == symcl r = symcl q &
18.45 + (ALL k k'. k~=i & k'~=i -->((k,k'):r) = ((k,k'):q)) &
18.46 + A i r = {} & R i q = {}"
18.47 +
18.48 + (* Our alternative definition *)
18.49 + derive :: "[vertex, (vertex*vertex)set, (vertex*vertex)set]=>bool"
18.50 + "derive i r q == A i r = {} & (q = reverse i r)"
18.51 +
18.52 +rules
18.53 + (* we assume that the universe of vertices is finite *)
18.54 + finite_vertex_univ "finite (UNIV :: vertex set)"
18.55 +
18.56 +end
19.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
19.2 +++ b/src/HOL/UNITY/Comp/README.html Mon Mar 05 15:32:54 2001 +0100
19.3 @@ -0,0 +1,39 @@
19.4 +<!-- $Id$ -->
19.5 +<HTML><HEAD><TITLE>HOL/UNITY/README</TITLE></HEAD><BODY>
19.6 +
19.7 +<H2>UNITY: Examples Involving Program Composition</H2>
19.8 +
19.9 +<P>
19.10 +The directory presents verification examples involving program composition.
19.11 +They are mostly taken from the works of Chandy, Charpentier and Chandy.
19.12 +
19.13 +<UL>
19.14 +<LI>examples of <em>universal properties</em>:
19.15 +the counter (<A HREF="Counter.thy"><CODE>Counter.thy</CODE></A>)
19.16 +and priority system (<A HREF="Priority.thy"><CODE>Priority.thy</CODE></A>)
19.17 +
19.18 +<LI>the allocation system (<A HREF="Alloc.thy"><CODE>Alloc.thy</CODE></A>)
19.19 +
19.20 +<LI>client implementation (<A HREF="Client.thy"><CODE>Client.thy</CODE></A>)
19.21 +
19.22 +<LI>allocator implementation (<A HREF="AllocImpl.thy"><CODE>AllocImpl.thy</CODE></A>)
19.23 +
19.24 +<LI>the handshake protocol
19.25 +(<A HREF="Handshake.thy"><CODE>Handshake.thy</CODE></A>)
19.26 +
19.27 +<LI>the timer array (demonstrates arrays of processes)
19.28 +(<A HREF="TimerArray.thy"><CODE>TimerArray.thy</CODE></A>)
19.29 +</UL>
19.30 +
19.31 +<P> Safety proofs (invariants) are often proved automatically. Progress
19.32 +proofs involving ENSURES can sometimes be proved automatically. The
19.33 +level of automation appears to be about the same as in HOL-UNITY by Flemming
19.34 +Andersen et al.
19.35 +
19.36 +<HR>
19.37 +<P>Last modified on $Date$
19.38 +
19.39 +<ADDRESS>
19.40 +<A NAME="lcp@cl.cam.ac.uk" HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A>
19.41 +</ADDRESS>
19.42 +</BODY></HTML>
20.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
20.2 +++ b/src/HOL/UNITY/Comp/TimerArray.ML Mon Mar 05 15:32:54 2001 +0100
20.3 @@ -0,0 +1,53 @@
20.4 +(* Title: HOL/UNITY/TimerArray.thy
20.5 + ID: $Id$
20.6 + Author: Lawrence C Paulson, Cambridge University Computer Laboratory
20.7 + Copyright 1998 University of Cambridge
20.8 +
20.9 +A trivial example of reasoning about an array of processes
20.10 +*)
20.11 +
20.12 +Addsimps [Timer_def RS def_prg_Init];
20.13 +program_defs_ref := [Timer_def];
20.14 +
20.15 +Addsimps [count_def, decr_def];
20.16 +
20.17 +(*Demonstrates induction, but not used in the following proof*)
20.18 +Goal "Timer : UNIV leadsTo {s. count s = 0}";
20.19 +by (res_inst_tac [("f", "count")] lessThan_induct 1);
20.20 +by (Simp_tac 1);
20.21 +by (case_tac "m" 1);
20.22 +by (force_tac (claset() addSIs [subset_imp_leadsTo], simpset()) 1);
20.23 +by (ensures_tac "decr" 1);
20.24 +qed "Timer_leadsTo_zero";
20.25 +
20.26 +Goal "Timer : preserves snd";
20.27 +by (rtac preservesI 1);
20.28 +by (constrains_tac 1);
20.29 +qed "Timer_preserves_snd";
20.30 +AddIffs [Timer_preserves_snd];
20.31 +
20.32 +Addsimps [PLam_stable];
20.33 +
20.34 +Goal "finite I \
20.35 +\ ==> (plam i: I. Timer) : UNIV leadsTo {(s,uu). ALL i:I. s i = 0}";
20.36 +by (eres_inst_tac [("A'1", "%i. lift_set i ({0} <*> UNIV)")]
20.37 + (finite_stable_completion RS leadsTo_weaken) 1);
20.38 +by Auto_tac;
20.39 +(*Safety property, already reduced to the single Timer case*)
20.40 +by (constrains_tac 2);
20.41 +(*Progress property for the array of Timers*)
20.42 +by (res_inst_tac [("f", "sub i o fst")] lessThan_induct 1);
20.43 +by (case_tac "m" 1);
20.44 +(*Annoying need to massage the conditions to have the form (... <*> UNIV)*)
20.45 +by (auto_tac (claset() addIs [subset_imp_leadsTo],
20.46 + simpset() addsimps [insert_absorb, lessThan_Suc RS sym,
20.47 + lift_set_Un_distrib RS sym,
20.48 + Times_Un_distrib1 RS sym,
20.49 + Times_Diff_distrib1 RS sym]));
20.50 +by (rename_tac "n" 1);
20.51 +by (rtac PLam_leadsTo_Basis 1);
20.52 +by (auto_tac (claset(), simpset() addsimps [lessThan_Suc RS sym]));
20.53 +by (constrains_tac 1);
20.54 +by (res_inst_tac [("act", "decr")] transientI 1);
20.55 +by (auto_tac (claset(), simpset() addsimps [Timer_def]));
20.56 +qed "TimerArray_leadsTo_zero";
21.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
21.2 +++ b/src/HOL/UNITY/Comp/TimerArray.thy Mon Mar 05 15:32:54 2001 +0100
21.3 @@ -0,0 +1,23 @@
21.4 +(* Title: HOL/UNITY/TimerArray.thy
21.5 + ID: $Id$
21.6 + Author: Lawrence C Paulson, Cambridge University Computer Laboratory
21.7 + Copyright 1998 University of Cambridge
21.8 +
21.9 +A trivial example of reasoning about an array of processes
21.10 +*)
21.11 +
21.12 +TimerArray = PPROD +
21.13 +
21.14 +types 'a state = "nat * 'a" (*second component allows new variables*)
21.15 +
21.16 +constdefs
21.17 + count :: "'a state => nat"
21.18 + "count s == fst s"
21.19 +
21.20 + decr :: "('a state * 'a state) set"
21.21 + "decr == UN n uu. {((Suc n, uu), (n,uu))}"
21.22 +
21.23 + Timer :: 'a state program
21.24 + "Timer == mk_program (UNIV, {decr}, UNIV)"
21.25 +
21.26 +end