--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/Comp/Alloc.ML Mon Mar 05 15:32:54 2001 +0100
@@ -0,0 +1,744 @@
+(* Title: HOL/UNITY/Alloc
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1998 University of Cambridge
+
+Specification of Chandy and Charpentier's Allocator
+*)
+
+(*Perhaps equalities.ML shouldn't add this in the first place!*)
+Delsimps [image_Collect];
+
+AddIs [impOfSubs subset_preserves_o];
+Addsimps [impOfSubs subset_preserves_o];
+Addsimps [funPair_o_distrib];
+Addsimps [Always_INT_distrib];
+Delsimps [o_apply];
+
+(*Eliminate the "o" operator*)
+val o_simp = simplify (simpset() addsimps [o_def]);
+
+(*For rewriting of specifications related by "guarantees"*)
+Addsimps [rename_image_constrains, rename_image_stable,
+ rename_image_increasing, rename_image_invariant,
+ rename_image_Constrains, rename_image_Stable,
+ rename_image_Increasing, rename_image_Always,
+ rename_image_leadsTo, rename_image_LeadsTo,
+ rename_preserves, rename_image_preserves, lift_image_preserves,
+ bij_image_INT, bij_is_inj RS image_Int, bij_image_Collect_eq];
+
+(*Splits up conjunctions & intersections: like CONJUNCTS in the HOL system*)
+fun list_of_Int th =
+ (list_of_Int (th RS conjunct1) @ list_of_Int (th RS conjunct2))
+ handle THM _ => (list_of_Int (th RS IntD1) @ list_of_Int (th RS IntD2))
+ handle THM _ => (list_of_Int (th RS INT_D))
+ handle THM _ => (list_of_Int (th RS bspec))
+ handle THM _ => [th];
+
+(*Used just once, for Alloc_Increasing*)
+val lessThanBspec = lessThan_iff RS iffD2 RSN (2, bspec);
+fun normalize th =
+ normalize (th RS spec
+ handle THM _ => th RS lessThanBspec
+ handle THM _ => th RS bspec
+ handle THM _ => th RS (guarantees_INT_right_iff RS iffD1))
+ handle THM _ => th;
+
+
+
+(*** bijectivity of sysOfAlloc [MUST BE AUTOMATED] ***)
+
+val record_auto_tac =
+ auto_tac (claset() addIs [ext] addSWrapper record_split_wrapper,
+ simpset() addsimps [sysOfAlloc_def, sysOfClient_def,
+ client_map_def, non_dummy_def, funPair_def,
+ o_apply, Let_def]);
+
+
+Goalw [sysOfAlloc_def, Let_def] "inj sysOfAlloc";
+by (rtac injI 1);
+by record_auto_tac;
+qed "inj_sysOfAlloc";
+AddIffs [inj_sysOfAlloc];
+
+(*We need the inverse; also having it simplifies the proof of surjectivity*)
+Goal "!!s. inv sysOfAlloc s = \
+\ (| allocGiv = allocGiv s, \
+\ allocAsk = allocAsk s, \
+\ allocRel = allocRel s, \
+\ allocState_d.dummy = (client s, dummy s) |)";
+by (rtac (inj_sysOfAlloc RS inv_f_eq) 1);
+by record_auto_tac;
+qed "inv_sysOfAlloc_eq";
+Addsimps [inv_sysOfAlloc_eq];
+
+Goal "surj sysOfAlloc";
+by (simp_tac (simpset() addsimps [surj_iff, expand_fun_eq, o_apply]) 1);
+by record_auto_tac;
+qed "surj_sysOfAlloc";
+AddIffs [surj_sysOfAlloc];
+
+Goal "bij sysOfAlloc";
+by (blast_tac (claset() addIs [bijI]) 1);
+qed "bij_sysOfAlloc";
+AddIffs [bij_sysOfAlloc];
+
+
+(*** bijectivity of sysOfClient ***)
+
+Goalw [sysOfClient_def] "inj sysOfClient";
+by (rtac injI 1);
+by record_auto_tac;
+qed "inj_sysOfClient";
+AddIffs [inj_sysOfClient];
+
+Goal "!!s. inv sysOfClient s = \
+\ (client s, \
+\ (| allocGiv = allocGiv s, \
+\ allocAsk = allocAsk s, \
+\ allocRel = allocRel s, \
+\ allocState_d.dummy = systemState.dummy s|) )";
+by (rtac (inj_sysOfClient RS inv_f_eq) 1);
+by record_auto_tac;
+qed "inv_sysOfClient_eq";
+Addsimps [inv_sysOfClient_eq];
+
+Goal "surj sysOfClient";
+by (simp_tac (simpset() addsimps [surj_iff, expand_fun_eq, o_apply]) 1);
+by record_auto_tac;
+qed "surj_sysOfClient";
+AddIffs [surj_sysOfClient];
+
+Goal "bij sysOfClient";
+by (blast_tac (claset() addIs [bijI]) 1);
+qed "bij_sysOfClient";
+AddIffs [bij_sysOfClient];
+
+
+(*** bijectivity of client_map ***)
+
+Goalw [inj_on_def] "inj client_map";
+by record_auto_tac;
+qed "inj_client_map";
+AddIffs [inj_client_map];
+
+Goal "!!s. inv client_map s = \
+\ (%(x,y).(|giv = giv x, ask = ask x, rel = rel x, \
+\ clientState_d.dummy = y|)) s";
+by (rtac (inj_client_map RS inv_f_eq) 1);
+by record_auto_tac;
+qed "inv_client_map_eq";
+Addsimps [inv_client_map_eq];
+
+Goal "surj client_map";
+by (simp_tac (simpset() addsimps [surj_iff, expand_fun_eq, o_apply]) 1);
+by record_auto_tac;
+qed "surj_client_map";
+AddIffs [surj_client_map];
+
+Goal "bij client_map";
+by (blast_tac (claset() addIs [bijI]) 1);
+qed "bij_client_map";
+AddIffs [bij_client_map];
+
+
+(** o-simprules for client_map **)
+
+Goalw [client_map_def] "fst o client_map = non_dummy";
+by (rtac fst_o_funPair 1);
+qed "fst_o_client_map";
+Addsimps (make_o_equivs fst_o_client_map);
+
+Goalw [client_map_def] "snd o client_map = clientState_d.dummy";
+by (rtac snd_o_funPair 1);
+qed "snd_o_client_map";
+Addsimps (make_o_equivs snd_o_client_map);
+
+(** o-simprules for sysOfAlloc [MUST BE AUTOMATED] **)
+
+Goal "client o sysOfAlloc = fst o allocState_d.dummy ";
+by record_auto_tac;
+qed "client_o_sysOfAlloc";
+Addsimps (make_o_equivs client_o_sysOfAlloc);
+
+Goal "allocGiv o sysOfAlloc = allocGiv";
+by record_auto_tac;
+qed "allocGiv_o_sysOfAlloc_eq";
+Addsimps (make_o_equivs allocGiv_o_sysOfAlloc_eq);
+
+Goal "allocAsk o sysOfAlloc = allocAsk";
+by record_auto_tac;
+qed "allocAsk_o_sysOfAlloc_eq";
+Addsimps (make_o_equivs allocAsk_o_sysOfAlloc_eq);
+
+Goal "allocRel o sysOfAlloc = allocRel";
+by record_auto_tac;
+qed "allocRel_o_sysOfAlloc_eq";
+Addsimps (make_o_equivs allocRel_o_sysOfAlloc_eq);
+
+(** o-simprules for sysOfClient [MUST BE AUTOMATED] **)
+
+Goal "client o sysOfClient = fst";
+by record_auto_tac;
+qed "client_o_sysOfClient";
+Addsimps (make_o_equivs client_o_sysOfClient);
+
+Goal "allocGiv o sysOfClient = allocGiv o snd ";
+by record_auto_tac;
+qed "allocGiv_o_sysOfClient_eq";
+Addsimps (make_o_equivs allocGiv_o_sysOfClient_eq);
+
+Goal "allocAsk o sysOfClient = allocAsk o snd ";
+by record_auto_tac;
+qed "allocAsk_o_sysOfClient_eq";
+Addsimps (make_o_equivs allocAsk_o_sysOfClient_eq);
+
+Goal "allocRel o sysOfClient = allocRel o snd ";
+by record_auto_tac;
+qed "allocRel_o_sysOfClient_eq";
+Addsimps (make_o_equivs allocRel_o_sysOfClient_eq);
+
+Goal "allocGiv o inv sysOfAlloc = allocGiv";
+by (simp_tac (simpset() addsimps [o_def]) 1);
+qed "allocGiv_o_inv_sysOfAlloc_eq";
+Addsimps (make_o_equivs allocGiv_o_inv_sysOfAlloc_eq);
+
+Goal "allocAsk o inv sysOfAlloc = allocAsk";
+by (simp_tac (simpset() addsimps [o_def]) 1);
+qed "allocAsk_o_inv_sysOfAlloc_eq";
+Addsimps (make_o_equivs allocAsk_o_inv_sysOfAlloc_eq);
+
+Goal "allocRel o inv sysOfAlloc = allocRel";
+by (simp_tac (simpset() addsimps [o_def]) 1);
+qed "allocRel_o_inv_sysOfAlloc_eq";
+Addsimps (make_o_equivs allocRel_o_inv_sysOfAlloc_eq);
+
+Goal "(rel o inv client_map o drop_map i o inv sysOfClient) = \
+\ rel o sub i o client";
+by (simp_tac (simpset() addsimps [o_def, drop_map_def]) 1);
+qed "rel_inv_client_map_drop_map";
+Addsimps (make_o_equivs rel_inv_client_map_drop_map);
+
+Goal "(ask o inv client_map o drop_map i o inv sysOfClient) = \
+\ ask o sub i o client";
+by (simp_tac (simpset() addsimps [o_def, drop_map_def]) 1);
+qed "ask_inv_client_map_drop_map";
+Addsimps (make_o_equivs ask_inv_client_map_drop_map);
+
+(**
+Open_locale "System";
+
+val Alloc = thm "Alloc";
+val Client = thm "Client";
+val Network = thm "Network";
+val System_def = thm "System_def";
+
+CANNOT use bind_thm: it puts the theorem into standard form, in effect
+ exporting it from the locale
+**)
+
+AddIffs [finite_lessThan];
+
+(*Client : <unfolded specification> *)
+val client_spec_simps =
+ [client_spec_def, client_increasing_def, client_bounded_def,
+ client_progress_def, client_allowed_acts_def, client_preserves_def,
+ guarantees_Int_right];
+
+val [Client_Increasing_ask, Client_Increasing_rel,
+ Client_Bounded, Client_Progress, Client_AllowedActs,
+ Client_preserves_giv, Client_preserves_dummy] =
+ Client |> simplify (simpset() addsimps client_spec_simps)
+ |> list_of_Int;
+
+AddIffs [Client_Increasing_ask, Client_Increasing_rel, Client_Bounded,
+ Client_preserves_giv, Client_preserves_dummy];
+
+
+(*Network : <unfolded specification> *)
+val network_spec_simps =
+ [network_spec_def, network_ask_def, network_giv_def,
+ network_rel_def, network_allowed_acts_def, network_preserves_def,
+ ball_conj_distrib];
+
+val [Network_Ask, Network_Giv, Network_Rel, Network_AllowedActs,
+ Network_preserves_allocGiv, Network_preserves_rel,
+ Network_preserves_ask] =
+ Network |> simplify (simpset() addsimps network_spec_simps)
+ |> list_of_Int;
+
+AddIffs [Network_preserves_allocGiv];
+
+Addsimps [Network_preserves_rel, Network_preserves_ask];
+Addsimps [o_simp Network_preserves_rel, o_simp Network_preserves_ask];
+
+
+(*Alloc : <unfolded specification> *)
+val alloc_spec_simps =
+ [alloc_spec_def, alloc_increasing_def, alloc_safety_def,
+ alloc_progress_def, alloc_allowed_acts_def,
+ alloc_preserves_def];
+
+val [Alloc_Increasing_0, Alloc_Safety, Alloc_Progress, Alloc_AllowedActs,
+ Alloc_preserves_allocRel, Alloc_preserves_allocAsk,
+ Alloc_preserves_dummy] =
+ Alloc |> simplify (simpset() addsimps alloc_spec_simps)
+ |> list_of_Int;
+
+(*Strip off the INT in the guarantees postcondition*)
+val Alloc_Increasing = normalize Alloc_Increasing_0;
+
+AddIffs [Alloc_preserves_allocRel, Alloc_preserves_allocAsk,
+ Alloc_preserves_dummy];
+
+(** Components lemmas [MUST BE AUTOMATED] **)
+
+Goal "Network Join \
+\ ((rename sysOfClient \
+\ (plam x: (lessThan Nclients). rename client_map Client)) Join \
+\ rename sysOfAlloc Alloc) \
+\ = System";
+by (simp_tac (simpset() addsimps System_def::Join_ac) 1);
+qed "Network_component_System";
+
+Goal "(rename sysOfClient \
+\ (plam x: (lessThan Nclients). rename client_map Client)) Join \
+\ (Network Join rename sysOfAlloc Alloc) = System";
+by (simp_tac (simpset() addsimps System_def::Join_ac) 1);
+qed "Client_component_System";
+
+Goal "rename sysOfAlloc Alloc Join \
+\ ((rename sysOfClient (plam x: (lessThan Nclients). rename client_map Client)) Join \
+\ Network) = System";
+by (simp_tac (simpset() addsimps System_def::Join_ac) 1);
+qed "Alloc_component_System";
+
+AddIffs [Client_component_System, Network_component_System,
+ Alloc_component_System];
+
+(** These preservation laws should be generated automatically **)
+
+Goal "Allowed Client = preserves rel Int preserves ask";
+by (auto_tac (claset(),
+ simpset() addsimps [Allowed_def, Client_AllowedActs,
+ safety_prop_Acts_iff]));
+qed "Client_Allowed";
+Addsimps [Client_Allowed];
+
+Goal "Allowed Network = \
+\ preserves allocRel Int \
+\ (INT i: lessThan Nclients. preserves(giv o sub i o client))";
+by (auto_tac (claset(),
+ simpset() addsimps [Allowed_def, Network_AllowedActs,
+ safety_prop_Acts_iff]));
+qed "Network_Allowed";
+Addsimps [Network_Allowed];
+
+Goal "Allowed Alloc = preserves allocGiv";
+by (auto_tac (claset(),
+ simpset() addsimps [Allowed_def, Alloc_AllowedActs,
+ safety_prop_Acts_iff]));
+qed "Alloc_Allowed";
+Addsimps [Alloc_Allowed];
+
+Goal "OK I (%i. lift i (rename client_map Client))";
+by (rtac OK_lift_I 1);
+by Auto_tac;
+by (dres_inst_tac [("w1", "rel")] (impOfSubs subset_preserves_o) 1);
+by (dres_inst_tac [("w1", "ask")] (impOfSubs subset_preserves_o) 2);
+by (auto_tac (claset(), simpset() addsimps [o_def, split_def]));
+qed "OK_lift_rename_Client";
+Addsimps [OK_lift_rename_Client]; (*needed in rename_client_map_tac*
+
+(*The proofs of rename_Client_Increasing, rename_Client_Bounded and
+ rename_Client_Progress are similar. All require copying out the original
+ Client property. A forward proof can be constructed as follows:
+
+ Client_Increasing_ask RS
+ (bij_client_map RS rename_rename_guarantees_eq RS iffD2)
+ RS (lift_lift_guarantees_eq RS iffD2)
+ RS guarantees_PLam_I
+ RS (bij_sysOfClient RS rename_rename_guarantees_eq RS iffD2)
+ |> simplify (simpset() addsimps [lift_image_eq_rename, o_def, split_def,
+ surj_rename RS surj_range]);
+
+However, the "preserves" property remains to be discharged, and the unfolding
+of "o" and "sub" complicates subsequent reasoning.
+
+The following tactic works for all three proofs, though it certainly looks
+ad-hoc!
+*)
+val rename_client_map_tac =
+ EVERY [
+ simp_tac (simpset() addsimps [rename_guarantees_eq_rename_inv]) 1,
+ rtac guarantees_PLam_I 1,
+ assume_tac 2,
+ (*preserves: routine reasoning*)
+ asm_simp_tac (simpset() addsimps [lift_preserves_sub]) 2,
+ (*the guarantee for "lift i (rename client_map Client)" *)
+ asm_simp_tac
+ (simpset() addsimps [lift_guarantees_eq_lift_inv,
+ rename_guarantees_eq_rename_inv,
+ bij_imp_bij_inv, surj_rename RS surj_range,
+ inv_inv_eq]) 1,
+ asm_simp_tac
+ (simpset() addsimps [o_def, non_dummy_def, guarantees_Int_right]) 1];
+
+
+(*Lifting Client_Increasing to systemState*)
+Goal "i : I \
+\ ==> rename sysOfClient (plam x: I. rename client_map Client) : \
+\ UNIV guarantees \
+\ Increasing (ask o sub i o client) Int \
+\ Increasing (rel o sub i o client)";
+by rename_client_map_tac;
+qed "rename_Client_Increasing";
+
+Goal "[| F : preserves w; i ~= j |] \
+\ ==> F : preserves (sub i o fst o lift_map j o funPair v w)";
+by (auto_tac (claset(),
+ simpset() addsimps [lift_map_def, split_def, linorder_neq_iff, o_def]));
+by (ALLGOALS (dtac (impOfSubs subset_preserves_o)));
+by (auto_tac (claset(), simpset() addsimps [o_def]));
+qed "preserves_sub_fst_lift_map";
+
+Goal "[| i < Nclients; j < Nclients |] \
+\ ==> Client : preserves (giv o sub i o fst o lift_map j o client_map)";
+by (case_tac "i=j" 1);
+by (asm_full_simp_tac (simpset() addsimps [o_def, non_dummy_def]) 1);
+by (dtac (Client_preserves_dummy RS preserves_sub_fst_lift_map) 1);
+by (ALLGOALS (dtac (impOfSubs subset_preserves_o)));
+by (asm_full_simp_tac (simpset() addsimps [o_def, client_map_def]) 1);
+qed "client_preserves_giv_oo_client_map";
+
+Goal "rename sysOfClient (plam x: lessThan Nclients. rename client_map Client)\
+\ ok Network";
+by (auto_tac (claset(), simpset() addsimps [ok_iff_Allowed,
+ client_preserves_giv_oo_client_map]));
+qed "rename_sysOfClient_ok_Network";
+
+Goal "rename sysOfClient (plam x: lessThan Nclients. rename client_map Client)\
+\ ok rename sysOfAlloc Alloc";
+by (simp_tac (simpset() addsimps [ok_iff_Allowed]) 1);
+qed "rename_sysOfClient_ok_Alloc";
+
+Goal "rename sysOfAlloc Alloc ok Network";
+by (simp_tac (simpset() addsimps [ok_iff_Allowed]) 1);
+qed "rename_sysOfAlloc_ok_Network";
+
+AddIffs [rename_sysOfClient_ok_Network, rename_sysOfClient_ok_Alloc,
+ rename_sysOfAlloc_ok_Network];
+
+(*The "ok" laws, re-oriented*)
+AddIffs [rename_sysOfClient_ok_Network RS ok_sym,
+ rename_sysOfClient_ok_Alloc RS ok_sym,
+ rename_sysOfAlloc_ok_Network RS ok_sym];
+
+Goal "i < Nclients \
+\ ==> System : Increasing (ask o sub i o client) Int \
+\ Increasing (rel o sub i o client)";
+by (rtac ([rename_Client_Increasing,
+ Client_component_System] MRS component_guaranteesD) 1);
+by Auto_tac;
+qed "System_Increasing";
+
+bind_thm ("rename_guarantees_sysOfAlloc_I",
+ bij_sysOfAlloc RS rename_rename_guarantees_eq RS iffD2);
+
+
+(*Lifting Alloc_Increasing up to the level of systemState*)
+val rename_Alloc_Increasing =
+ Alloc_Increasing RS rename_guarantees_sysOfAlloc_I
+ |> simplify (simpset() addsimps [surj_rename RS surj_range, o_def]);
+
+Goalw [System_def]
+ "i < Nclients ==> System : Increasing (sub i o allocGiv)";
+by (simp_tac (simpset() addsimps [o_def]) 1);
+by (rtac (rename_Alloc_Increasing RS guarantees_Join_I1 RS guaranteesD) 1);
+by Auto_tac;
+qed "System_Increasing_allocGiv";
+
+AddSIs (list_of_Int System_Increasing);
+
+(** Follows consequences.
+ The "Always (INT ...) formulation expresses the general safety property
+ and allows it to be combined using Always_Int_rule below. **)
+
+Goal
+ "i < Nclients ==> System : ((sub i o allocRel) Fols (rel o sub i o client))";
+by (auto_tac (claset() addSIs [Network_Rel RS component_guaranteesD],
+ simpset()));
+qed "System_Follows_rel";
+
+Goal
+ "i < Nclients ==> System : ((sub i o allocAsk) Fols (ask o sub i o client))";
+by (auto_tac (claset() addSIs [Network_Ask RS component_guaranteesD],
+ simpset()));
+qed "System_Follows_ask";
+
+Goal
+ "i < Nclients ==> System : (giv o sub i o client) Fols (sub i o allocGiv)";
+by (auto_tac (claset() addSIs [Network_Giv RS component_guaranteesD,
+ rename_Alloc_Increasing RS component_guaranteesD],
+ simpset()));
+by (ALLGOALS (simp_tac (simpset() addsimps [o_def, non_dummy_def])));
+by (auto_tac
+ (claset() addSIs [rename_Alloc_Increasing RS component_guaranteesD],
+ simpset()));
+qed "System_Follows_allocGiv";
+
+Goal "System : Always (INT i: lessThan Nclients. \
+\ {s. (giv o sub i o client) s <= (sub i o allocGiv) s})";
+by Auto_tac;
+by (etac (System_Follows_allocGiv RS Follows_Bounded) 1);
+qed "Always_giv_le_allocGiv";
+
+Goal "System : Always (INT i: lessThan Nclients. \
+\ {s. (sub i o allocAsk) s <= (ask o sub i o client) s})";
+by Auto_tac;
+by (etac (System_Follows_ask RS Follows_Bounded) 1);
+qed "Always_allocAsk_le_ask";
+
+Goal "System : Always (INT i: lessThan Nclients. \
+\ {s. (sub i o allocRel) s <= (rel o sub i o client) s})";
+by (auto_tac (claset() addSIs [Follows_Bounded, System_Follows_rel],
+ simpset()));
+qed "Always_allocRel_le_rel";
+
+
+(*** Proof of the safety property (1) ***)
+
+(*safety (1), step 1 is System_Follows_rel*)
+
+(*safety (1), step 2*)
+(* i < Nclients ==> System : Increasing (sub i o allocRel) *)
+bind_thm ("System_Increasing_allocRel",
+ System_Follows_rel RS Follows_Increasing1);
+
+(*Lifting Alloc_safety up to the level of systemState.
+ Simplififying with o_def gets rid of the translations but it unfortunately
+ gets rid of the other "o"s too.*)
+val rename_Alloc_Safety =
+ Alloc_Safety RS rename_guarantees_sysOfAlloc_I
+ |> simplify (simpset() addsimps [o_def]);
+
+(*safety (1), step 3*)
+Goal
+ "System : Always {s. setsum (%i. (tokens o sub i o allocGiv) s) \
+\ (lessThan Nclients) \
+\ <= NbT + setsum (%i. (tokens o sub i o allocRel) s) \
+\ (lessThan Nclients)}";
+by (simp_tac (simpset() addsimps [o_apply]) 1);
+by (rtac (rename_Alloc_Safety RS component_guaranteesD) 1);
+by (auto_tac (claset(),
+ simpset() addsimps [o_simp System_Increasing_allocRel]));
+qed "System_sum_bounded";
+
+
+(** Follows reasoning **)
+
+Goal "System : Always (INT i: lessThan Nclients. \
+\ {s. (tokens o giv o sub i o client) s \
+\ <= (tokens o sub i o allocGiv) s})";
+by (rtac (Always_giv_le_allocGiv RS Always_weaken) 1);
+by (auto_tac (claset() addIs [tokens_mono_prefix],
+ simpset() addsimps [o_apply]));
+qed "Always_tokens_giv_le_allocGiv";
+
+Goal "System : Always (INT i: lessThan Nclients. \
+\ {s. (tokens o sub i o allocRel) s \
+\ <= (tokens o rel o sub i o client) s})";
+by (rtac (Always_allocRel_le_rel RS Always_weaken) 1);
+by (auto_tac (claset() addIs [tokens_mono_prefix],
+ simpset() addsimps [o_apply]));
+qed "Always_tokens_allocRel_le_rel";
+
+(*safety (1), step 4 (final result!) *)
+Goalw [system_safety_def] "System : system_safety";
+by (rtac (Always_Int_rule [System_sum_bounded, Always_tokens_giv_le_allocGiv,
+ Always_tokens_allocRel_le_rel] RS Always_weaken) 1);
+by Auto_tac;
+by (rtac (setsum_fun_mono RS order_trans) 1);
+by (dtac order_trans 2);
+by (rtac ([order_refl, setsum_fun_mono] MRS add_le_mono) 2);
+by (assume_tac 3);
+by Auto_tac;
+qed "System_safety";
+
+
+(*** Proof of the progress property (2) ***)
+
+(*progress (2), step 1 is System_Follows_ask and System_Follows_rel*)
+
+(*progress (2), step 2; see also System_Increasing_allocRel*)
+(* i < Nclients ==> System : Increasing (sub i o allocAsk) *)
+bind_thm ("System_Increasing_allocAsk",
+ System_Follows_ask RS Follows_Increasing1);
+
+(*progress (2), step 3: lifting "Client_Bounded" to systemState*)
+Goal "i : I \
+\ ==> rename sysOfClient (plam x: I. rename client_map Client) : \
+\ UNIV guarantees \
+\ Always {s. ALL elt : set ((ask o sub i o client) s). elt <= NbT}";
+by rename_client_map_tac;
+qed "rename_Client_Bounded";
+
+Goal "i < Nclients \
+\ ==> System : Always \
+\ {s. ALL elt : set ((ask o sub i o client) s). elt <= NbT}";
+by (rtac ([rename_Client_Bounded,
+ Client_component_System] MRS component_guaranteesD) 1);
+by Auto_tac;
+qed "System_Bounded_ask";
+
+Goal "{x. ALL y. P y --> Q x y} = (INT y: {y. P y}. {x. Q x y})";
+by (Blast_tac 1);
+qed "Collect_all_imp_eq";
+
+(*progress (2), step 4*)
+Goal "System : Always {s. ALL i<Nclients. \
+\ ALL elt : set ((sub i o allocAsk) s). elt <= NbT}";
+by (auto_tac (claset(), simpset() addsimps [Collect_all_imp_eq]));
+by (rtac (Always_Int_rule [Always_allocAsk_le_ask, System_Bounded_ask]
+ RS Always_weaken) 1);
+by (auto_tac (claset() addDs [set_mono], simpset()));
+qed "System_Bounded_allocAsk";
+
+(*progress (2), step 5 is System_Increasing_allocGiv*)
+
+(*progress (2), step 6*)
+(* i < Nclients ==> System : Increasing (giv o sub i o client) *)
+bind_thm ("System_Increasing_giv",
+ System_Follows_allocGiv RS Follows_Increasing1);
+
+
+Goal "i: I \
+\ ==> rename sysOfClient (plam x: I. rename client_map Client) \
+\ : Increasing (giv o sub i o client) \
+\ guarantees \
+\ (INT h. {s. h <= (giv o sub i o client) s & \
+\ h pfixGe (ask o sub i o client) s} \
+\ LeadsTo {s. tokens h <= (tokens o rel o sub i o client) s})";
+by rename_client_map_tac;
+by (asm_simp_tac (simpset() addsimps [o_simp Client_Progress]) 1);
+qed "rename_Client_Progress";
+
+
+(*progress (2), step 7*)
+Goal
+ "System : (INT i : (lessThan Nclients). \
+\ INT h. {s. h <= (giv o sub i o client) s & \
+\ h pfixGe (ask o sub i o client) s} \
+\ LeadsTo {s. tokens h <= (tokens o rel o sub i o client) s})";
+by (rtac INT_I 1);
+(*Couldn't have just used Auto_tac since the "INT h" must be kept*)
+by (rtac ([rename_Client_Progress,
+ Client_component_System] MRS component_guaranteesD) 1);
+by (auto_tac (claset(), simpset() addsimps [System_Increasing_giv]));
+qed "System_Client_Progress";
+
+(*Concludes
+ System : {s. k <= (sub i o allocGiv) s}
+ LeadsTo
+ {s. (sub i o allocAsk) s <= (ask o sub i o client) s} Int
+ {s. k <= (giv o sub i o client) s} *)
+val lemma =
+ [System_Follows_ask RS Follows_Bounded,
+ System_Follows_allocGiv RS Follows_LeadsTo] MRS Always_LeadsToD;
+
+(*A more complicated variant of the previous one*)
+val lemma2 = [lemma,
+ System_Follows_ask RS Follows_Increasing1 RS IncreasingD]
+ MRS PSP_Stable;
+
+Goal "i < Nclients \
+\ ==> System : {s. h <= (sub i o allocGiv) s & \
+\ h pfixGe (sub i o allocAsk) s} \
+\ LeadsTo \
+\ {s. h <= (giv o sub i o client) s & \
+\ h pfixGe (ask o sub i o client) s}";
+by (rtac single_LeadsTo_I 1);
+by (res_inst_tac [("k6", "h"), ("x2", "(sub i o allocAsk) s")]
+ (lemma2 RS LeadsTo_weaken) 1);
+by Auto_tac;
+by (blast_tac (claset() addIs [trans_Ge RS trans_genPrefix RS transD,
+ prefix_imp_pfixGe]) 1);
+val lemma3 = result();
+
+
+(*progress (2), step 8: Client i's "release" action is visible system-wide*)
+Goal "i < Nclients \
+\ ==> System : {s. h <= (sub i o allocGiv) s & \
+\ h pfixGe (sub i o allocAsk) s} \
+\ LeadsTo {s. tokens h <= (tokens o sub i o allocRel) s}";
+by (rtac LeadsTo_Trans 1);
+by (dtac (System_Follows_rel RS impOfSubs (mono_tokens RS mono_Follows_o) RS
+ Follows_LeadsTo) 2);
+by (asm_full_simp_tac (simpset() addsimps [o_assoc]) 2);
+by (rtac LeadsTo_Trans 1);
+by (cut_facts_tac [System_Client_Progress] 2);
+by (blast_tac (claset() addIs [LeadsTo_Basis]) 2);
+by (etac lemma3 1);
+qed "System_Alloc_Client_Progress";
+
+(*Lifting Alloc_Progress up to the level of systemState*)
+val rename_Alloc_Progress =
+ Alloc_Progress RS rename_guarantees_sysOfAlloc_I
+ |> simplify (simpset() addsimps [o_def]);
+
+(*progress (2), step 9*)
+Goal
+ "System : (INT i : (lessThan Nclients). \
+\ INT h. {s. h <= (sub i o allocAsk) s} \
+\ LeadsTo {s. h pfixLe (sub i o allocGiv) s})";
+(*Can't use simpset(): the "INT h" must be kept*)
+by (simp_tac (HOL_ss addsimps [o_apply, sub_def]) 1);
+by (rtac (rename_Alloc_Progress RS component_guaranteesD) 1);
+by (auto_tac (claset(),
+ simpset() addsimps [o_simp System_Increasing_allocRel,
+ o_simp System_Increasing_allocAsk,
+ o_simp System_Bounded_allocAsk,
+ o_simp System_Alloc_Client_Progress]));
+qed "System_Alloc_Progress";
+
+
+(*progress (2), step 10 (final result!) *)
+Goalw [system_progress_def] "System : system_progress";
+by (cut_facts_tac [System_Alloc_Progress] 1);
+by (blast_tac (claset() addIs [LeadsTo_Trans,
+ System_Follows_allocGiv RS Follows_LeadsTo_pfixLe,
+ System_Follows_ask RS Follows_LeadsTo]) 1);
+qed "System_Progress";
+
+
+(*Ultimate goal*)
+Goalw [system_spec_def] "System : system_spec";
+by (blast_tac (claset() addIs [System_safety, System_Progress]) 1);
+qed "System_correct";
+
+
+(** Some lemmas no longer used **)
+
+Goal "non_dummy = (% (g,a,r). (| giv = g, ask = a, rel = r |)) o \
+\ (funPair giv (funPair ask rel))";
+by (rtac ext 1);
+by (auto_tac (claset(), simpset() addsimps [o_def, non_dummy_def]));
+qed "non_dummy_eq_o_funPair";
+
+Goal "(preserves non_dummy) = \
+\ (preserves rel Int preserves ask Int preserves giv)";
+by (simp_tac (simpset() addsimps [non_dummy_eq_o_funPair]) 1);
+by Auto_tac;
+by (dres_inst_tac [("w1", "rel")] (impOfSubs subset_preserves_o) 1);
+by (dres_inst_tac [("w1", "ask")] (impOfSubs subset_preserves_o) 2);
+by (dres_inst_tac [("w1", "giv")] (impOfSubs subset_preserves_o) 3);
+by (auto_tac (claset(), simpset() addsimps [o_def]));
+qed "preserves_non_dummy_eq";
+
+(*Could go to Extend.ML*)
+Goal "bij f ==> fst (inv (%(x, u). inv f x) z) = f z";
+by (rtac fst_inv_equalityI 1);
+by (res_inst_tac [("f","%z. (f z, ?h z)")] surjI 1);
+by (asm_full_simp_tac (simpset() addsimps [bij_is_inj, inv_f_f]) 1);
+by (asm_full_simp_tac (simpset() addsimps [bij_is_surj, surj_f_inv_f]) 1);
+qed "bij_fst_inv_inv_eq";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/Comp/Alloc.thy Mon Mar 05 15:32:54 2001 +0100
@@ -0,0 +1,261 @@
+(* Title: HOL/UNITY/Alloc
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1998 University of Cambridge
+
+Specification of Chandy and Charpentier's Allocator
+*)
+
+Alloc = AllocBase + PPROD +
+
+(** State definitions. OUTPUT variables are locals **)
+
+record clientState =
+ giv :: nat list (*client's INPUT history: tokens GRANTED*)
+ ask :: nat list (*client's OUTPUT history: tokens REQUESTED*)
+ rel :: nat list (*client's OUTPUT history: tokens RELEASED*)
+
+record 'a clientState_d =
+ clientState +
+ dummy :: 'a (*dummy field for new variables*)
+
+constdefs
+ (*DUPLICATED FROM Client.thy, but with "tok" removed*)
+ (*Maybe want a special theory section to declare such maps*)
+ non_dummy :: 'a clientState_d => clientState
+ "non_dummy s == (|giv = giv s, ask = ask s, rel = rel s|)"
+
+ (*Renaming map to put a Client into the standard form*)
+ client_map :: "'a clientState_d => clientState*'a"
+ "client_map == funPair non_dummy dummy"
+
+
+record allocState =
+ allocGiv :: nat => nat list (*OUTPUT history: source of "giv" for i*)
+ allocAsk :: nat => nat list (*INPUT: allocator's copy of "ask" for i*)
+ allocRel :: nat => nat list (*INPUT: allocator's copy of "rel" for i*)
+
+record 'a allocState_d =
+ allocState +
+ dummy :: 'a (*dummy field for new variables*)
+
+record 'a systemState =
+ allocState +
+ client :: nat => clientState (*states of all clients*)
+ dummy :: 'a (*dummy field for new variables*)
+
+
+constdefs
+
+(** Resource allocation system specification **)
+
+ (*spec (1)*)
+ system_safety :: 'a systemState program set
+ "system_safety ==
+ Always {s. setsum(%i.(tokens o giv o sub i o client)s) (lessThan Nclients)
+ <= NbT + setsum(%i.(tokens o rel o sub i o client)s) (lessThan Nclients)}"
+
+ (*spec (2)*)
+ system_progress :: 'a systemState program set
+ "system_progress == INT i : lessThan Nclients.
+ INT h.
+ {s. h <= (ask o sub i o client)s} LeadsTo
+ {s. h pfixLe (giv o sub i o client) s}"
+
+ system_spec :: 'a systemState program set
+ "system_spec == system_safety Int system_progress"
+
+(** Client specification (required) ***)
+
+ (*spec (3)*)
+ client_increasing :: 'a clientState_d program set
+ "client_increasing ==
+ UNIV guarantees Increasing ask Int Increasing rel"
+
+ (*spec (4)*)
+ client_bounded :: 'a clientState_d program set
+ "client_bounded ==
+ UNIV guarantees Always {s. ALL elt : set (ask s). elt <= NbT}"
+
+ (*spec (5)*)
+ client_progress :: 'a clientState_d program set
+ "client_progress ==
+ Increasing giv guarantees
+ (INT h. {s. h <= giv s & h pfixGe ask s}
+ LeadsTo {s. tokens h <= (tokens o rel) s})"
+
+ (*spec: preserves part*)
+ client_preserves :: 'a clientState_d program set
+ "client_preserves == preserves giv Int preserves clientState_d.dummy"
+
+ (*environmental constraints*)
+ client_allowed_acts :: 'a clientState_d program set
+ "client_allowed_acts ==
+ {F. AllowedActs F =
+ insert Id (UNION (preserves (funPair rel ask)) Acts)}"
+
+ client_spec :: 'a clientState_d program set
+ "client_spec == client_increasing Int client_bounded Int client_progress
+ Int client_allowed_acts Int client_preserves"
+
+(** Allocator specification (required) ***)
+
+ (*spec (6)*)
+ alloc_increasing :: 'a allocState_d program set
+ "alloc_increasing ==
+ UNIV guarantees
+ (INT i : lessThan Nclients. Increasing (sub i o allocGiv))"
+
+ (*spec (7)*)
+ alloc_safety :: 'a allocState_d program set
+ "alloc_safety ==
+ (INT i : lessThan Nclients. Increasing (sub i o allocRel))
+ guarantees
+ Always {s. setsum(%i.(tokens o sub i o allocGiv)s) (lessThan Nclients)
+ <= NbT + setsum(%i.(tokens o sub i o allocRel)s) (lessThan Nclients)}"
+
+ (*spec (8)*)
+ alloc_progress :: 'a allocState_d program set
+ "alloc_progress ==
+ (INT i : lessThan Nclients. Increasing (sub i o allocAsk) Int
+ Increasing (sub i o allocRel))
+ Int
+ Always {s. ALL i<Nclients.
+ ALL elt : set ((sub i o allocAsk) s). elt <= NbT}
+ Int
+ (INT i : lessThan Nclients.
+ INT h. {s. h <= (sub i o allocGiv)s & h pfixGe (sub i o allocAsk)s}
+ LeadsTo
+ {s. tokens h <= (tokens o sub i o allocRel)s})
+ guarantees
+ (INT i : lessThan Nclients.
+ INT h. {s. h <= (sub i o allocAsk) s}
+ LeadsTo
+ {s. h pfixLe (sub i o allocGiv) s})"
+
+ (*NOTE: to follow the original paper, the formula above should have had
+ INT h. {s. h i <= (sub i o allocGiv)s & h i pfixGe (sub i o allocAsk)s}
+ LeadsTo
+ {s. tokens h i <= (tokens o sub i o allocRel)s})
+ thus h should have been a function variable. However, only h i is ever
+ looked at.*)
+
+ (*spec: preserves part*)
+ alloc_preserves :: 'a allocState_d program set
+ "alloc_preserves == preserves allocRel Int preserves allocAsk Int
+ preserves allocState_d.dummy"
+
+ (*environmental constraints*)
+ alloc_allowed_acts :: 'a allocState_d program set
+ "alloc_allowed_acts ==
+ {F. AllowedActs F =
+ insert Id (UNION (preserves allocGiv) Acts)}"
+
+ alloc_spec :: 'a allocState_d program set
+ "alloc_spec == alloc_increasing Int alloc_safety Int alloc_progress Int
+ alloc_allowed_acts Int alloc_preserves"
+
+(** Network specification ***)
+
+ (*spec (9.1)*)
+ network_ask :: 'a systemState program set
+ "network_ask == INT i : lessThan Nclients.
+ Increasing (ask o sub i o client) guarantees
+ ((sub i o allocAsk) Fols (ask o sub i o client))"
+
+ (*spec (9.2)*)
+ network_giv :: 'a systemState program set
+ "network_giv == INT i : lessThan Nclients.
+ Increasing (sub i o allocGiv)
+ guarantees
+ ((giv o sub i o client) Fols (sub i o allocGiv))"
+
+ (*spec (9.3)*)
+ network_rel :: 'a systemState program set
+ "network_rel == INT i : lessThan Nclients.
+ Increasing (rel o sub i o client)
+ guarantees
+ ((sub i o allocRel) Fols (rel o sub i o client))"
+
+ (*spec: preserves part*)
+ network_preserves :: 'a systemState program set
+ "network_preserves ==
+ preserves allocGiv Int
+ (INT i : lessThan Nclients. preserves (rel o sub i o client) Int
+ preserves (ask o sub i o client))"
+
+ (*environmental constraints*)
+ network_allowed_acts :: 'a systemState program set
+ "network_allowed_acts ==
+ {F. AllowedActs F =
+ insert Id
+ (UNION (preserves allocRel Int
+ (INT i: lessThan Nclients. preserves(giv o sub i o client)))
+ Acts)}"
+
+ network_spec :: 'a systemState program set
+ "network_spec == network_ask Int network_giv Int
+ network_rel Int network_allowed_acts Int
+ network_preserves"
+
+
+(** State mappings **)
+ sysOfAlloc :: "((nat => clientState) * 'a) allocState_d => 'a systemState"
+ "sysOfAlloc == %s. let (cl,xtr) = allocState_d.dummy s
+ in (| allocGiv = allocGiv s,
+ allocAsk = allocAsk s,
+ allocRel = allocRel s,
+ client = cl,
+ dummy = xtr|)"
+
+
+ sysOfClient :: "(nat => clientState) * 'a allocState_d => 'a systemState"
+ "sysOfClient == %(cl,al). (| allocGiv = allocGiv al,
+ allocAsk = allocAsk al,
+ allocRel = allocRel al,
+ client = cl,
+ systemState.dummy = allocState_d.dummy al|)"
+
+consts
+ Alloc :: 'a allocState_d program
+ Client :: 'a clientState_d program
+ Network :: 'a systemState program
+ System :: 'a systemState program
+
+rules
+ Alloc "Alloc : alloc_spec"
+ Client "Client : client_spec"
+ Network "Network : network_spec"
+
+defs
+ System_def
+ "System == rename sysOfAlloc Alloc Join Network Join
+ (rename sysOfClient
+ (plam x: lessThan Nclients. rename client_map Client))"
+
+
+(**
+locale System =
+ fixes
+ Alloc :: 'a allocState_d program
+ Client :: 'a clientState_d program
+ Network :: 'a systemState program
+ System :: 'a systemState program
+
+ assumes
+ Alloc "Alloc : alloc_spec"
+ Client "Client : client_spec"
+ Network "Network : network_spec"
+
+ defines
+ System_def
+ "System == rename sysOfAlloc Alloc
+ Join
+ Network
+ Join
+ (rename sysOfClient
+ (plam x: lessThan Nclients. rename client_map Client))"
+**)
+
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/Comp/AllocBase.ML Mon Mar 05 15:32:54 2001 +0100
@@ -0,0 +1,89 @@
+(* Title: HOL/UNITY/AllocBase.ML
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1998 University of Cambridge
+
+Basis declarations for Chandy and Charpentier's Allocator
+*)
+
+Goal "!!f :: nat=>nat. \
+\ (ALL i. i<n --> f i <= g i) --> \
+\ setsum f (lessThan n) <= setsum g (lessThan n)";
+by (induct_tac "n" 1);
+by (auto_tac (claset(), simpset() addsimps [lessThan_Suc]));
+by (dres_inst_tac [("x","n")] spec 1);
+by (arith_tac 1);
+qed_spec_mp "setsum_fun_mono";
+
+Goal "ALL xs. xs <= ys --> tokens xs <= tokens ys";
+by (induct_tac "ys" 1);
+by (auto_tac (claset(), simpset() addsimps [prefix_Cons]));
+qed_spec_mp "tokens_mono_prefix";
+
+Goalw [mono_def] "mono tokens";
+by (blast_tac (claset() addIs [tokens_mono_prefix]) 1);
+qed "mono_tokens";
+
+
+(** bag_of **)
+
+Goal "bag_of (l@l') = bag_of l + bag_of l'";
+by (induct_tac "l" 1);
+ by (asm_simp_tac (simpset() addsimps (thms "plus_ac0")) 2);
+by (Simp_tac 1);
+qed "bag_of_append";
+Addsimps [bag_of_append];
+
+Goal "mono (bag_of :: 'a list => ('a::order) multiset)";
+by (rtac monoI 1);
+by (rewtac prefix_def);
+by (etac genPrefix.induct 1);
+by Auto_tac;
+by (asm_full_simp_tac (simpset() addsimps [thm "union_le_mono"]) 1);
+by (etac order_trans 1);
+by (rtac (thm "union_upper1") 1);
+qed "mono_bag_of";
+
+(** setsum **)
+
+Addcongs [setsum_cong];
+
+Goal "setsum (%i. {#if i<k then f i else g i#}) (A Int lessThan k) = \
+\ setsum (%i. {#f i#}) (A Int lessThan k)";
+by (rtac setsum_cong 1);
+by Auto_tac;
+qed "bag_of_sublist_lemma";
+
+Goal "bag_of (sublist l A) = \
+\ setsum (%i. {# l!i #}) (A Int lessThan (length l))";
+by (rev_induct_tac "l" 1);
+by (Simp_tac 1);
+by (asm_simp_tac
+ (simpset() addsimps [sublist_append, Int_insert_right, lessThan_Suc,
+ nth_append, bag_of_sublist_lemma] @ thms "plus_ac0") 1);
+qed "bag_of_sublist";
+
+
+Goal "bag_of (sublist l (A Un B)) + bag_of (sublist l (A Int B)) = \
+\ bag_of (sublist l A) + bag_of (sublist l B)";
+by (subgoal_tac "A Int B Int {..length l(} = \
+\ (A Int {..length l(}) Int (B Int {..length l(})" 1);
+by (asm_simp_tac (simpset() addsimps [bag_of_sublist, Int_Un_distrib2,
+ setsum_Un_Int]) 1);
+by (Blast_tac 1);
+qed "bag_of_sublist_Un_Int";
+
+Goal "A Int B = {} \
+\ ==> bag_of (sublist l (A Un B)) = \
+\ bag_of (sublist l A) + bag_of (sublist l B)";
+by (asm_simp_tac (simpset() addsimps [bag_of_sublist_Un_Int RS sym]) 1);
+qed "bag_of_sublist_Un_disjoint";
+
+Goal "[| finite I; ALL i:I. ALL j:I. i~=j --> A i Int A j = {} |] \
+\ ==> bag_of (sublist l (UNION I A)) = \
+\ setsum (%i. bag_of (sublist l (A i))) I";
+by (asm_simp_tac (simpset() delsimps UN_simps addsimps (UN_simps RL [sym])
+ addsimps [bag_of_sublist]) 1);
+by (stac setsum_UN_disjoint 1);
+by Auto_tac;
+qed_spec_mp "bag_of_sublist_UN_disjoint";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/Comp/AllocBase.thy Mon Mar 05 15:32:54 2001 +0100
@@ -0,0 +1,31 @@
+(* Title: HOL/UNITY/AllocBase.thy
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1998 University of Cambridge
+
+Common declarations for Chandy and Charpentier's Allocator
+*)
+
+AllocBase = Rename + Follows +
+
+consts
+ NbT :: nat (*Number of tokens in system*)
+ Nclients :: nat (*Number of clients*)
+
+rules
+ NbT_pos "0 < NbT"
+
+(*This function merely sums the elements of a list*)
+consts tokens :: nat list => nat
+primrec
+ "tokens [] = 0"
+ "tokens (x#xs) = x + tokens xs"
+
+consts
+ bag_of :: 'a list => 'a multiset
+
+primrec
+ "bag_of [] = {#}"
+ "bag_of (x#xs) = {#x#} + bag_of xs"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/Comp/AllocImpl.ML Mon Mar 05 15:32:54 2001 +0100
@@ -0,0 +1,194 @@
+(* Title: HOL/UNITY/AllocImpl
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 2000 University of Cambridge
+
+Implementation of a multiple-client allocator from a single-client allocator
+*)
+
+AddIs [impOfSubs subset_preserves_o];
+Addsimps [funPair_o_distrib];
+Addsimps [Always_INT_distrib];
+Delsimps [o_apply];
+
+Open_locale "Merge";
+
+val Merge = thm "Merge_spec";
+
+Goal "Allowed M = (preserves merge.Out) Int (preserves merge.iOut)";
+by (cut_facts_tac [Merge] 1);
+by (auto_tac (claset(),
+ simpset() addsimps [merge_spec_def, merge_allowed_acts_def,
+ Allowed_def, safety_prop_Acts_iff]));
+qed "Merge_Allowed";
+
+Goal "M ok G = (G: preserves merge.Out & G: preserves merge.iOut & \
+\ M : Allowed G)";
+by (auto_tac (claset(), simpset() addsimps [Merge_Allowed, ok_iff_Allowed]));
+qed "M_ok_iff";
+AddIffs [M_ok_iff];
+
+Goal "[| G: preserves merge.Out; G: preserves merge.iOut; M : Allowed G |] \
+\ ==> M Join G : Always {s. length (merge.Out s) = length (merge.iOut s)}";
+by (cut_facts_tac [Merge] 1);
+by (force_tac (claset() addDs [guaranteesD],
+ simpset() addsimps [merge_spec_def, merge_eqOut_def]) 1);
+qed "Merge_Always_Out_eq_iOut";
+
+Goal "[| G: preserves merge.iOut; G: preserves merge.Out; M : Allowed G |] \
+\ ==> M Join G: Always {s. ALL elt : set (merge.iOut s). elt < Nclients}";
+by (cut_facts_tac [Merge] 1);
+by (force_tac (claset() addDs [guaranteesD],
+ simpset() addsimps [merge_spec_def, merge_bounded_def]) 1);
+qed "Merge_Bounded";
+
+Goal "[| G: preserves merge.iOut; G: preserves merge.Out; M : Allowed G |] \
+\ ==> M Join G : Always \
+\ {s. setsum (%i. bag_of (sublist (merge.Out s) \
+\ {k. k < length (iOut s) & iOut s ! k = i})) \
+\ (lessThan Nclients) = \
+\ (bag_of o merge.Out) s}";
+by (rtac ([[Merge_Always_Out_eq_iOut, Merge_Bounded] MRS Always_Int_I,
+ UNIV_AlwaysI] MRS (Always_Compl_Un_eq RS iffD1)) 1);
+ by Auto_tac;
+by (stac (bag_of_sublist_UN_disjoint RS sym) 1);
+ by (Simp_tac 1);
+ by (Blast_tac 1);
+by (asm_full_simp_tac (simpset() addsimps [set_conv_nth]) 1);
+by (subgoal_tac
+ "(UN i:lessThan Nclients. {k. k < length (iOut x) & iOut x ! k = i}) = \
+\ lessThan (length (iOut x))" 1);
+ by (Blast_tac 2);
+by (asm_simp_tac (simpset() addsimps [o_def]) 1);
+qed "Merge_Bag_Follows_lemma";
+
+Goal "M : (INT i: lessThan Nclients. Increasing (sub i o merge.In)) \
+\ guarantees \
+\ (bag_of o merge.Out) Fols \
+\ (%s. setsum (%i. (bag_of o sub i o merge.In) s) \
+\ (lessThan Nclients))";
+by (rtac (Merge_Bag_Follows_lemma RS Always_Follows1 RS guaranteesI) 1);
+by Auto_tac;
+by (rtac Follows_setsum 1);
+by (cut_facts_tac [Merge] 1);
+by (auto_tac (claset(),
+ simpset() addsimps [merge_spec_def, merge_follows_def, o_def]));
+by (dtac guaranteesD 1);
+by (best_tac
+ (claset() addIs [impOfSubs (mono_bag_of RS mono_Follows_apply)]) 3);
+by Auto_tac;
+qed "Merge_Bag_Follows";
+
+Close_locale "Merge";
+
+
+(** Distributor **)
+
+Open_locale "Distrib";
+
+val Distrib = thm "Distrib_spec";
+
+
+Goal "D : Increasing distr.In Int Increasing distr.iIn Int \
+\ Always {s. ALL elt : set (distr.iIn s). elt < Nclients} \
+\ guarantees \
+\ (INT i : lessThan Nclients. Increasing (sub i o distr.Out))";
+by (cut_facts_tac [Distrib] 1);
+by (full_simp_tac (simpset() addsimps [distr_spec_def, distr_follows_def]) 1);
+by (Clarify_tac 1);
+by (blast_tac (claset() addIs [guaranteesI, Follows_Increasing1]
+ addDs [guaranteesD]) 1);
+qed "Distr_Increasing_Out";
+
+Goal "[| G : preserves distr.Out; \
+\ D Join G : Always {s. ALL elt: set (distr.iIn s). elt < Nclients} |] \
+\ ==> D Join G : Always \
+\ {s. setsum (%i. bag_of (sublist (distr.In s) \
+\ {k. k < length (iIn s) & iIn s ! k = i})) \
+\ (lessThan Nclients) = \
+\ bag_of (sublist (distr.In s) (lessThan (length (iIn s))))}";
+by (etac ([asm_rl, UNIV_AlwaysI] MRS (Always_Compl_Un_eq RS iffD1)) 1);
+by Auto_tac;
+by (stac (bag_of_sublist_UN_disjoint RS sym) 1);
+ by (Simp_tac 1);
+ by (Blast_tac 1);
+by (asm_full_simp_tac (simpset() addsimps [set_conv_nth]) 1);
+by (subgoal_tac
+ "(UN i:lessThan Nclients. {k. k < length (iIn x) & iIn x ! k = i}) = \
+\ lessThan (length (iIn x))" 1);
+ by (Blast_tac 2);
+by (Asm_simp_tac 1);
+qed "Distr_Bag_Follows_lemma";
+
+Goal "D ok G = (G: preserves distr.Out & D : Allowed G)";
+by (cut_facts_tac [Distrib] 1);
+by (auto_tac (claset(),
+ simpset() addsimps [distr_spec_def, distr_allowed_acts_def,
+ Allowed_def, safety_prop_Acts_iff, ok_iff_Allowed]));
+qed "D_ok_iff";
+AddIffs [D_ok_iff];
+
+Goal
+ "D : Increasing distr.In Int Increasing distr.iIn Int \
+\ Always {s. ALL elt : set (distr.iIn s). elt < Nclients} \
+\ guarantees \
+\ (INT i : lessThan Nclients. \
+\ (%s. setsum (%i. (bag_of o sub i o distr.Out) s) (lessThan Nclients)) \
+\ Fols \
+\ (%s. bag_of (sublist (distr.In s) (lessThan (length(distr.iIn s))))))";
+by (rtac guaranteesI 1);
+by (Clarify_tac 1);
+by (rtac (Distr_Bag_Follows_lemma RS Always_Follows2) 1);
+by Auto_tac;
+by (rtac Follows_setsum 1);
+by (cut_facts_tac [Distrib] 1);
+by (auto_tac (claset(),
+ simpset() addsimps [distr_spec_def, distr_follows_def, o_def]));
+by (dtac guaranteesD 1);
+by (best_tac (claset() addIs [impOfSubs (mono_bag_of RS mono_Follows_apply)]) 3);
+by Auto_tac;
+qed "Distr_Bag_Follows";
+
+Close_locale "Distrib";
+
+
+Goal "!!f::nat=>nat. (INT i:(lessThan n). {s. f i <= g i s}) \
+\ <= {s. setsum f (lessThan n) <= setsum (%i. g i s) (lessThan n)}";
+by (induct_tac "n" 1);
+by (auto_tac (claset(), simpset() addsimps [lessThan_Suc]));
+qed "alloc_refinement_lemma";
+
+Goal
+"(INT i : lessThan Nclients. Increasing (sub i o allocAsk) Int \
+\ Increasing (sub i o allocRel)) \
+\ Int \
+\ Always {s. ALL i. i<Nclients --> \
+\ (ALL elt : set ((sub i o allocAsk) s). elt <= NbT)} \
+\ Int \
+\ (INT i : lessThan Nclients. \
+\ INT h. {s. h <= (sub i o allocGiv)s & h pfixGe (sub i o allocAsk)s} \
+\ LeadsTo {s. tokens h <= (tokens o sub i o allocRel)s}) \
+\ <= \
+\(INT i : lessThan Nclients. Increasing (sub i o allocAsk) Int \
+\ Increasing (sub i o allocRel)) \
+\ Int \
+\ Always {s. ALL i. i<Nclients --> \
+\ (ALL elt : set ((sub i o allocAsk) s). elt <= NbT)} \
+\ Int \
+\ (INT hf. (INT i : lessThan Nclients. \
+\ {s. hf i <= (sub i o allocGiv)s & hf i pfixGe (sub i o allocAsk)s}) \
+\ LeadsTo {s. setsum (%i. tokens (hf i)) (lessThan Nclients) <= \
+\ setsum (%i. (tokens o sub i o allocRel)s) (lessThan Nclients) })";
+by (auto_tac (claset(), simpset() addsimps [ball_conj_distrib]));
+by (rename_tac "F hf" 1);
+by (rtac ([Finite_stable_completion, alloc_refinement_lemma]
+ MRS LeadsTo_weaken_R) 1);
+ by (Blast_tac 1);
+ by (Blast_tac 1);
+by (subgoal_tac "F : Increasing (tokens o (sub i o allocRel))" 1);
+ by (blast_tac
+ (claset() addIs [impOfSubs (mono_tokens RS mono_Increasing_o)]) 2);
+by (asm_full_simp_tac (simpset() addsimps [Increasing_def, o_assoc]) 1);
+qed "alloc_refinement";
+
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/Comp/AllocImpl.thy Mon Mar 05 15:32:54 2001 +0100
@@ -0,0 +1,224 @@
+(* Title: HOL/UNITY/AllocImpl
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1998 University of Cambridge
+
+Implementation of a multiple-client allocator from a single-client allocator
+*)
+
+AllocImpl = AllocBase + Follows + PPROD +
+
+
+(** State definitions. OUTPUT variables are locals **)
+
+(*Type variable 'b is the type of items being merged*)
+record 'b merge =
+ In :: nat => 'b list (*merge's INPUT histories: streams to merge*)
+ Out :: 'b list (*merge's OUTPUT history: merged items*)
+ iOut :: nat list (*merge's OUTPUT history: origins of merged items*)
+
+record ('a,'b) merge_d =
+ 'b merge +
+ dummy :: 'a (*dummy field for new variables*)
+
+constdefs
+ non_dummy :: ('a,'b) merge_d => 'b merge
+ "non_dummy s == (|In = In s, Out = Out s, iOut = iOut s|)"
+
+record 'b distr =
+ In :: 'b list (*items to distribute*)
+ iIn :: nat list (*destinations of items to distribute*)
+ Out :: nat => 'b list (*distributed items*)
+
+record ('a,'b) distr_d =
+ 'b distr +
+ dummy :: 'a (*dummy field for new variables*)
+
+record allocState =
+ giv :: nat list (*OUTPUT history: source of tokens*)
+ ask :: nat list (*INPUT: tokens requested from allocator*)
+ rel :: nat list (*INPUT: tokens released to allocator*)
+
+record 'a allocState_d =
+ allocState +
+ dummy :: 'a (*dummy field for new variables*)
+
+record 'a systemState =
+ allocState +
+ mergeRel :: nat merge
+ mergeAsk :: nat merge
+ distr :: nat distr
+ dummy :: 'a (*dummy field for new variables*)
+
+
+constdefs
+
+(** Merge specification (the number of inputs is Nclients) ***)
+
+ (*spec (10)*)
+ merge_increasing :: ('a,'b) merge_d program set
+ "merge_increasing ==
+ UNIV guarantees (Increasing merge.Out) Int (Increasing merge.iOut)"
+
+ (*spec (11)*)
+ merge_eqOut :: ('a,'b) merge_d program set
+ "merge_eqOut ==
+ UNIV guarantees
+ Always {s. length (merge.Out s) = length (merge.iOut s)}"
+
+ (*spec (12)*)
+ merge_bounded :: ('a,'b) merge_d program set
+ "merge_bounded ==
+ UNIV guarantees
+ Always {s. ALL elt : set (merge.iOut s). elt < Nclients}"
+
+ (*spec (13)*)
+ merge_follows :: ('a,'b) merge_d program set
+ "merge_follows ==
+ (INT i : lessThan Nclients. Increasing (sub i o merge.In))
+ guarantees
+ (INT i : lessThan Nclients.
+ (%s. sublist (merge.Out s)
+ {k. k < size(merge.iOut s) & merge.iOut s! k = i})
+ Fols (sub i o merge.In))"
+
+ (*spec: preserves part*)
+ merge_preserves :: ('a,'b) merge_d program set
+ "merge_preserves == preserves merge.In Int preserves merge_d.dummy"
+
+ (*environmental constraints*)
+ merge_allowed_acts :: ('a,'b) merge_d program set
+ "merge_allowed_acts ==
+ {F. AllowedActs F =
+ insert Id (UNION (preserves (funPair merge.Out merge.iOut)) Acts)}"
+
+ merge_spec :: ('a,'b) merge_d program set
+ "merge_spec == merge_increasing Int merge_eqOut Int merge_bounded Int
+ merge_follows Int merge_allowed_acts Int merge_preserves"
+
+(** Distributor specification (the number of outputs is Nclients) ***)
+
+ (*spec (14)*)
+ distr_follows :: ('a,'b) distr_d program set
+ "distr_follows ==
+ Increasing distr.In Int Increasing distr.iIn Int
+ Always {s. ALL elt : set (distr.iIn s). elt < Nclients}
+ guarantees
+ (INT i : lessThan Nclients.
+ (sub i o distr.Out) Fols
+ (%s. sublist (distr.In s)
+ {k. k < size(distr.iIn s) & distr.iIn s ! k = i}))"
+
+ distr_allowed_acts :: ('a,'b) distr_d program set
+ "distr_allowed_acts ==
+ {D. AllowedActs D = insert Id (UNION (preserves distr.Out) Acts)}"
+
+ distr_spec :: ('a,'b) distr_d program set
+ "distr_spec == distr_follows Int distr_allowed_acts"
+
+(** Single-client allocator specification (required) ***)
+
+ (*spec (18)*)
+ alloc_increasing :: 'a allocState_d program set
+ "alloc_increasing == UNIV guarantees Increasing giv"
+
+ (*spec (19)*)
+ alloc_safety :: 'a allocState_d program set
+ "alloc_safety ==
+ Increasing rel
+ guarantees Always {s. tokens (giv s) <= NbT + tokens (rel s)}"
+
+ (*spec (20)*)
+ alloc_progress :: 'a allocState_d program set
+ "alloc_progress ==
+ Increasing ask Int Increasing rel Int
+ Always {s. ALL elt : set (ask s). elt <= NbT}
+ Int
+ (INT h. {s. h <= giv s & h pfixGe (ask s)}
+ LeadsTo
+ {s. tokens h <= tokens (rel s)})
+ guarantees (INT h. {s. h <= ask s} LeadsTo {s. h pfixLe giv s})"
+
+ (*spec: preserves part*)
+ alloc_preserves :: 'a allocState_d program set
+ "alloc_preserves == preserves rel Int
+ preserves ask Int
+ preserves allocState_d.dummy"
+
+
+ (*environmental constraints*)
+ alloc_allowed_acts :: 'a allocState_d program set
+ "alloc_allowed_acts ==
+ {F. AllowedActs F = insert Id (UNION (preserves giv) Acts)}"
+
+ alloc_spec :: 'a allocState_d program set
+ "alloc_spec == alloc_increasing Int alloc_safety Int alloc_progress Int
+ alloc_allowed_acts Int alloc_preserves"
+
+locale Merge =
+ fixes
+ M :: ('a,'b::order) merge_d program
+ assumes
+ Merge_spec "M : merge_spec"
+
+locale Distrib =
+ fixes
+ D :: ('a,'b::order) distr_d program
+ assumes
+ Distrib_spec "D : distr_spec"
+
+
+(****
+# (** Network specification ***)
+
+# (*spec (9.1)*)
+# network_ask :: 'a systemState program set
+# "network_ask == INT i : lessThan Nclients.
+# Increasing (ask o sub i o client)
+# guarantees[ask]
+# (ask Fols (ask o sub i o client))"
+
+# (*spec (9.2)*)
+# network_giv :: 'a systemState program set
+# "network_giv == INT i : lessThan Nclients.
+# Increasing giv
+# guarantees[giv o sub i o client]
+# ((giv o sub i o client) Fols giv )"
+
+# (*spec (9.3)*)
+# network_rel :: 'a systemState program set
+# "network_rel == INT i : lessThan Nclients.
+# Increasing (rel o sub i o client)
+# guarantees[rel]
+# (rel Fols (rel o sub i o client))"
+
+# (*spec: preserves part*)
+# network_preserves :: 'a systemState program set
+# "network_preserves == preserves giv Int
+# (INT i : lessThan Nclients.
+# preserves (funPair rel ask o sub i o client))"
+
+# network_spec :: 'a systemState program set
+# "network_spec == network_ask Int network_giv Int
+# network_rel Int network_preserves"
+
+
+# (** State mappings **)
+# sysOfAlloc :: "((nat => merge) * 'a) allocState_d => 'a systemState"
+# "sysOfAlloc == %s. let (cl,xtr) = allocState_d.dummy s
+# in (| giv = giv s,
+# ask = ask s,
+# rel = rel s,
+# client = cl,
+# dummy = xtr|)"
+
+
+# sysOfClient :: "(nat => merge) * 'a allocState_d => 'a systemState"
+# "sysOfClient == %(cl,al). (| giv = giv al,
+# ask = ask al,
+# rel = rel al,
+# client = cl,
+# systemState.dummy = allocState_d.dummy al|)"
+****)
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/Comp/Client.ML Mon Mar 05 15:32:54 2001 +0100
@@ -0,0 +1,174 @@
+(* Title: HOL/UNITY/Client
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1998 University of Cambridge
+
+Distributed Resource Management System: the Client
+*)
+
+Addsimps [Client_def RS def_prg_Init,
+ Client_def RS def_prg_AllowedActs];
+program_defs_ref := [Client_def];
+
+Addsimps (map simp_of_act [rel_act_def, tok_act_def, ask_act_def]);
+
+Goal "(Client ok G) = \
+\ (G : preserves rel & G : preserves ask & G : preserves tok &\
+\ Client : Allowed G)";
+by (auto_tac (claset(),
+ simpset() addsimps [ok_iff_Allowed, Client_def RS def_prg_Allowed]));
+qed "Client_ok_iff";
+AddIffs [Client_ok_iff];
+
+
+(*Safety property 1: ask, rel are increasing*)
+Goal "Client: UNIV guarantees Increasing ask Int Increasing rel";
+by (auto_tac
+ (claset() addSIs [increasing_imp_Increasing],
+ simpset() addsimps [guar_def, impOfSubs preserves_subset_increasing]));
+by (auto_tac (claset(), simpset() addsimps [increasing_def]));
+by (ALLGOALS constrains_tac);
+by Auto_tac;
+qed "increasing_ask_rel";
+
+Addsimps [nth_append, append_one_prefix];
+
+
+(*Safety property 2: the client never requests too many tokens.
+ With no Substitution Axiom, we must prove the two invariants
+ simultaneously.
+*)
+Goal "Client ok G \
+\ ==> Client Join G : \
+\ Always ({s. tok s <= NbT} Int \
+\ {s. ALL elt : set (ask s). elt <= NbT})";
+by Auto_tac;
+by (rtac (invariantI RS stable_Join_Always2) 1);
+by (fast_tac (claset() addSEs [impOfSubs preserves_subset_stable]
+ addSIs [stable_Int]) 3);
+by (constrains_tac 2);
+by (cut_inst_tac [("m", "tok s")] (NbT_pos RS mod_less_divisor) 2);
+by Auto_tac;
+qed "ask_bounded_lemma";
+
+(*export version, with no mention of tok in the postcondition, but
+ unfortunately tok must be declared local.*)
+Goal "Client: UNIV guarantees Always {s. ALL elt : set (ask s). elt <= NbT}";
+by (rtac guaranteesI 1);
+by (etac (ask_bounded_lemma RS Always_weaken) 1);
+by (rtac Int_lower2 1);
+qed "ask_bounded";
+
+
+(*** Towards proving the liveness property ***)
+
+Goal "Client: stable {s. rel s <= giv s}";
+by (constrains_tac 1);
+by Auto_tac;
+qed "stable_rel_le_giv";
+
+Goal "[| Client Join G : Increasing giv; G : preserves rel |] \
+\ ==> Client Join G : Stable {s. rel s <= giv s}";
+by (rtac (stable_rel_le_giv RS Increasing_preserves_Stable) 1);
+by Auto_tac;
+qed "Join_Stable_rel_le_giv";
+
+Goal "[| Client Join G : Increasing giv; G : preserves rel |] \
+\ ==> Client Join G : Always {s. rel s <= giv s}";
+by (force_tac (claset() addIs [AlwaysI, Join_Stable_rel_le_giv], simpset()) 1);
+qed "Join_Always_rel_le_giv";
+
+Goal "Client : transient {s. rel s = k & k<h & h <= giv s & h pfixGe ask s}";
+by (res_inst_tac [("act", "rel_act")] transientI 1);
+by (auto_tac (claset(),
+ simpset() addsimps [Domain_def, Client_def]));
+by (blast_tac (claset() addIs [less_le_trans, prefix_length_le,
+ strict_prefix_length_less]) 1);
+by (auto_tac (claset(),
+ simpset() addsimps [prefix_def, genPrefix_iff_nth, Ge_def]));
+by (blast_tac (claset() addIs [strict_prefix_length_less]) 1);
+qed "transient_lemma";
+
+
+Goal "[| Client Join G : Increasing giv; Client ok G |] \
+\ ==> Client Join G : {s. rel s = k & k<h & h <= giv s & h pfixGe ask s} \
+\ LeadsTo {s. k < rel s & rel s <= giv s & \
+\ h <= giv s & h pfixGe ask s}";
+by (rtac single_LeadsTo_I 1);
+by (ftac (increasing_ask_rel RS guaranteesD) 1);
+by Auto_tac;
+by (rtac (transient_lemma RS Join_transient_I1 RS transient_imp_leadsTo RS
+ leadsTo_imp_LeadsTo RS PSP_Stable RS LeadsTo_weaken) 1);
+by (rtac (Stable_Int RS Stable_Int RS Stable_Int) 1);
+by (eres_inst_tac [("f", "giv"), ("x", "giv s")] IncreasingD 1);
+by (eres_inst_tac [("f", "ask"), ("x", "ask s")] IncreasingD 1);
+by (eres_inst_tac [("f", "rel"), ("x", "rel s")] IncreasingD 1);
+by (etac Join_Stable_rel_le_giv 1);
+by (Blast_tac 1);
+by (blast_tac (claset() addIs [sym, order_less_le RS iffD2,
+ order_trans, prefix_imp_pfixGe,
+ pfixGe_trans]) 2);
+by (blast_tac (claset() addIs [order_less_imp_le, order_trans]) 1);
+qed "induct_lemma";
+
+
+Goal "[| Client Join G : Increasing giv; Client ok G |] \
+\ ==> Client Join G : {s. rel s < h & h <= giv s & h pfixGe ask s} \
+\ LeadsTo {s. h <= rel s}";
+by (res_inst_tac [("f", "%s. size h - size (rel s)")] LessThan_induct 1);
+by (auto_tac (claset(), simpset() addsimps [vimage_def]));
+by (rtac single_LeadsTo_I 1);
+by (rtac (induct_lemma RS LeadsTo_weaken) 1);
+by Auto_tac;
+by (blast_tac (claset() addIs [order_less_le RS iffD2]
+ addDs [common_prefix_linear]) 1);
+by (REPEAT (dtac strict_prefix_length_less 1));
+by (arith_tac 1);
+qed "rel_progress_lemma";
+
+
+Goal "[| Client Join G : Increasing giv; Client ok G |] \
+\ ==> Client Join G : {s. h <= giv s & h pfixGe ask s} \
+\ LeadsTo {s. h <= rel s}";
+by (rtac (Join_Always_rel_le_giv RS Always_LeadsToI) 1);
+by (rtac ([rel_progress_lemma, subset_refl RS subset_imp_LeadsTo] MRS
+ LeadsTo_Un RS LeadsTo_weaken_L) 3);
+by Auto_tac;
+by (blast_tac (claset() addIs [order_less_le RS iffD2]
+ addDs [common_prefix_linear]) 1);
+qed "client_progress_lemma";
+
+(*Progress property: all tokens that are given will be released*)
+Goal "Client : \
+\ Increasing giv guarantees \
+\ (INT h. {s. h <= giv s & h pfixGe ask s} LeadsTo {s. h <= rel s})";
+by (rtac guaranteesI 1);
+by (Clarify_tac 1);
+by (blast_tac (claset() addIs [client_progress_lemma]) 1);
+qed "client_progress";
+
+(*This shows that the Client won't alter other variables in any state
+ that it is combined with*)
+Goal "Client : preserves dummy";
+by (rewtac preserves_def);
+by Auto_tac;
+by (constrains_tac 1);
+by Auto_tac;
+qed "client_preserves_dummy";
+
+
+(** Obsolete lemmas from first version of the Client **)
+
+Goal "Client: stable {s. size (rel s) <= size (giv s)}";
+by (constrains_tac 1);
+by Auto_tac;
+qed "stable_size_rel_le_giv";
+
+(*clients return the right number of tokens*)
+Goal "Client : Increasing giv guarantees Always {s. rel s <= giv s}";
+by (rtac guaranteesI 1);
+by (rtac AlwaysI 1);
+by (Force_tac 1);
+by (blast_tac (claset() addIs [Increasing_preserves_Stable,
+ stable_rel_le_giv]) 1);
+qed "ok_guar_rel_prefix_giv";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/Comp/Client.thy Mon Mar 05 15:32:54 2001 +0100
@@ -0,0 +1,66 @@
+(* Title: HOL/UNITY/Client.thy
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1998 University of Cambridge
+
+Distributed Resource Management System: the Client
+*)
+
+Client = Rename + AllocBase +
+
+types
+ tokbag = nat (*tokbags could be multisets...or any ordered type?*)
+
+record state =
+ giv :: tokbag list (*input history: tokens granted*)
+ ask :: tokbag list (*output history: tokens requested*)
+ rel :: tokbag list (*output history: tokens released*)
+ tok :: tokbag (*current token request*)
+
+record 'a state_d =
+ state +
+ dummy :: 'a (*new variables*)
+
+
+(*Array indexing is translated to list indexing as A[n] == A!(n-1). *)
+
+constdefs
+
+ (** Release some tokens **)
+
+ rel_act :: "('a state_d * 'a state_d) set"
+ "rel_act == {(s,s').
+ EX nrel. nrel = size (rel s) &
+ s' = s (| rel := rel s @ [giv s!nrel] |) &
+ nrel < size (giv s) &
+ ask s!nrel <= giv s!nrel}"
+
+ (** Choose a new token requirement **)
+
+ (** Including s'=s suppresses fairness, allowing the non-trivial part
+ of the action to be ignored **)
+
+ tok_act :: "('a state_d * 'a state_d) set"
+ "tok_act == {(s,s'). s'=s | s' = s (|tok := Suc (tok s mod NbT) |)}"
+
+ ask_act :: "('a state_d * 'a state_d) set"
+ "ask_act == {(s,s'). s'=s |
+ (s' = s (|ask := ask s @ [tok s]|))}"
+
+ Client :: 'a state_d program
+ "Client ==
+ mk_program ({s. tok s : atMost NbT &
+ giv s = [] & ask s = [] & rel s = []},
+ {rel_act, tok_act, ask_act},
+ UN G: preserves rel Int preserves ask Int preserves tok.
+ Acts G)"
+
+ (*Maybe want a special theory section to declare such maps*)
+ non_dummy :: 'a state_d => state
+ "non_dummy s == (|giv = giv s, ask = ask s, rel = rel s, tok = tok s|)"
+
+ (*Renaming map to put a Client into the standard form*)
+ client_map :: "'a state_d => state*'a"
+ "client_map == funPair non_dummy dummy"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/Comp/Counter.ML Mon Mar 05 15:32:54 2001 +0100
@@ -0,0 +1,140 @@
+(* Title: HOL/UNITY/Counter
+ ID: $Id$
+ Author: Sidi O Ehmety, Cambridge University Computer Laboratory
+ Copyright 2001 University of Cambridge
+
+A family of similar counters, version close to the original.
+
+From Charpentier and Chandy,
+Examples of Program Composition Illustrating the Use of Universal Properties
+ In J. Rolim (editor), Parallel and Distributed Processing,
+ Spriner LNCS 1586 (1999), pages 1215-1227.
+*)
+
+Addsimps [Component_def RS def_prg_Init];
+program_defs_ref := [Component_def];
+Addsimps (map simp_of_act [a_def]);
+
+(* Theorems about sum and sumj *)
+Goal "ALL n. I<n --> sum I (s(c n := x)) = sum I s";
+by (induct_tac "I" 1);
+by Auto_tac;
+qed_spec_mp "sum_upd_gt";
+
+
+Goal "sum I (s(c I := x)) = sum I s";
+by (induct_tac "I" 1);
+by Auto_tac;
+by (simp_tac (simpset()
+ addsimps [rewrite_rule [fun_upd_def] sum_upd_gt]) 1);
+qed "sum_upd_eq";
+
+Goal "sum I (s(C := x)) = sum I s";
+by (induct_tac "I" 1);
+by Auto_tac;
+qed "sum_upd_C";
+
+Goal "sumj I i (s(c i := x)) = sumj I i s";
+by (induct_tac "I" 1);
+by Auto_tac;
+by (simp_tac (simpset() addsimps
+ [rewrite_rule [fun_upd_def] sum_upd_eq]) 1);
+qed "sumj_upd_ci";
+
+Goal "sumj I i (s(C := x)) = sumj I i s";
+by (induct_tac "I" 1);
+by Auto_tac;
+by (simp_tac (simpset()
+ addsimps [rewrite_rule [fun_upd_def] sum_upd_C]) 1);
+qed "sumj_upd_C";
+
+Goal "ALL i. I<i--> (sumj I i s = sum I s)";
+by (induct_tac "I" 1);
+by Auto_tac;
+qed_spec_mp "sumj_sum_gt";
+
+Goal "(sumj I I s = sum I s)";
+by (induct_tac "I" 1);
+by Auto_tac;
+by (simp_tac (simpset() addsimps [sumj_sum_gt]) 1);
+qed "sumj_sum_eq";
+
+Goal "ALL i. i<I-->(sum I s = s (c i) + sumj I i s)";
+by (induct_tac "I" 1);
+by (auto_tac (claset(), simpset() addsimps [linorder_neq_iff, sumj_sum_eq]));
+qed_spec_mp "sum_sumj";
+
+(* Correctness proofs for Components *)
+(* p2 and p3 proofs *)
+Goal "Component i : stable {s. s C = s (c i) + k}";
+by (constrains_tac 1);
+qed "p2";
+
+Goal
+"Component i: stable {s. ALL v. v~=c i & v~=C --> s v = k v}";
+by (constrains_tac 1);
+qed "p3";
+
+
+Goal
+"(ALL k. Component i: stable ({s. s C = s (c i) + sumj I i k} \
+\ Int {s. ALL v. v~=c i & v~=C --> s v = k v})) \
+\ = (Component i: stable {s. s C = s (c i) + sumj I i s})";
+by (auto_tac (claset(), simpset()
+ addsimps [constrains_def, stable_def,Component_def,
+ sumj_upd_C, sumj_upd_ci]));
+qed "p2_p3_lemma1";
+
+Goal
+"ALL k. Component i: stable ({s. s C = s (c i) + sumj I i k} Int \
+\ {s. ALL v. v~=c i & v~=C --> s v = k v})";
+by (blast_tac (claset() addIs [[p2, p3] MRS stable_Int]) 1);
+qed "p2_p3_lemma2";
+
+
+Goal
+"Component i: stable {s. s C = s (c i) + sumj I i s}";
+by (auto_tac (claset() addSIs [p2_p3_lemma2],
+ simpset() addsimps [p2_p3_lemma1 RS sym]));
+qed "p2_p3";
+
+(* Compositional Proof *)
+
+Goal "(ALL i. i < I --> s (c i) = #0) --> sum I s = #0";
+by (induct_tac "I" 1);
+by Auto_tac;
+qed "sum_0'";
+val sum0_lemma = (sum_0' RS mp) RS sym;
+
+(* I could'nt be empty *)
+Goalw [invariant_def]
+"!!I. 0<I ==> (JN i:{i. i<I}. Component i):invariant {s. s C = sum I s}";
+by (simp_tac (simpset() addsimps [JN_stable,Init_JN,sum_sumj]) 1);
+by (force_tac (claset() addIs [p2_p3, sum0_lemma RS sym], simpset()) 1);
+qed "safety";
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/Comp/Counter.thy Mon Mar 05 15:32:54 2001 +0100
@@ -0,0 +1,41 @@
+(* Title: HOL/UNITY/Counter
+ ID: $Id$
+ Author: Sidi O Ehmety, Cambridge University Computer Laboratory
+ Copyright 2001 University of Cambridge
+
+A family of similar counters, version close to the original.
+
+From Charpentier and Chandy,
+Examples of Program Composition Illustrating the Use of Universal Properties
+ In J. Rolim (editor), Parallel and Distributed Processing,
+ Spriner LNCS 1586 (1999), pages 1215-1227.
+*)
+
+Counter = Comp +
+(* Variables are names *)
+datatype name = C | c nat
+types state = name=>int
+
+consts
+ sum :: "[nat,state]=>int"
+ sumj :: "[nat, nat, state]=>int"
+
+primrec (* sum I s = sigma_{i<I}. s (c i) *)
+ "sum 0 s = #0"
+ "sum (Suc i) s = s (c i) + sum i s"
+
+primrec
+ "sumj 0 i s = #0"
+ "sumj (Suc n) i s = (if n=i then sum n s else s (c n) + sumj n i s)"
+
+types command = "(state*state)set"
+
+constdefs
+ a :: "nat=>command"
+ "a i == {(s, s'). s'=s(c i:= s (c i) + #1, C:= s C + #1)}"
+
+ Component :: "nat => state program"
+ "Component i ==
+ mk_program({s. s C = #0 & s (c i) = #0}, {a i},
+ UN G: preserves (%s. s (c i)). Acts G)"
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/Comp/Counterc.ML Mon Mar 05 15:32:54 2001 +0100
@@ -0,0 +1,124 @@
+(* Title: HOL/UNITY/Counterc
+ ID: $Id$
+ Author: Sidi O Ehmety, Cambridge University Computer Laboratory
+ Copyright 2001 University of Cambridge
+
+A family of similar counters, version with a full use of "compatibility "
+
+From Charpentier and Chandy,
+Examples of Program Composition Illustrating the Use of Universal Properties
+ In J. Rolim (editor), Parallel and Distributed Processing,
+ Spriner LNCS 1586 (1999), pages 1215-1227.
+*)
+
+Addsimps [Component_def RS def_prg_Init,
+Component_def RS def_prg_AllowedActs];
+program_defs_ref := [Component_def];
+Addsimps (map simp_of_act [a_def]);
+
+(* Theorems about sum and sumj *)
+Goal "ALL i. I<i--> (sum I s = sumj I i s)";
+by (induct_tac "I" 1);
+by Auto_tac;
+qed_spec_mp "sum_sumj_eq1";
+
+Goal "i<I --> sum I s = c s i + sumj I i s";
+by (induct_tac "I" 1);
+by (auto_tac (claset(), simpset() addsimps [linorder_neq_iff, sum_sumj_eq1]));
+qed_spec_mp "sum_sumj_eq2";
+
+Goal "(ALL i. i<I --> c s' i = c s i) --> (sum I s' = sum I s)";
+by (induct_tac "I" 1 THEN Auto_tac);
+qed_spec_mp "sum_ext";
+
+Goal "(ALL j. j<I & j~=i --> c s' j = c s j) --> (sumj I i s' = sumj I i s)";
+by (induct_tac "I" 1);
+by Safe_tac;
+by (auto_tac (claset() addSIs [sum_ext], simpset()));
+qed_spec_mp "sumj_ext";
+
+
+Goal "(ALL i. i<I --> c s i = #0) --> sum I s = #0";
+by (induct_tac "I" 1);
+by Auto_tac;
+qed "sum0";
+
+
+(* Safety properties for Components *)
+
+Goal "(Component i ok G) = \
+\ (G: preserves (%s. c s i) & Component i:Allowed G)";
+by (auto_tac (claset(),
+ simpset() addsimps [ok_iff_Allowed, Component_def RS def_prg_Allowed]));
+qed "Component_ok_iff";
+AddIffs [Component_ok_iff];
+AddIffs [OK_iff_ok];
+Addsimps [preserves_def];
+
+
+Goal "Component i: stable {s. C s = (c s) i + k}";
+by (constrains_tac 1);
+qed "p2";
+
+Goal "[| OK I Component; i:I |] \
+\ ==> Component i: stable {s. ALL j:I. j~=i --> c s j = c k j}";
+by (full_simp_tac (simpset() addsimps [stable_def, constrains_def]) 1);
+by (Blast_tac 1);
+qed "p3";
+
+
+Goal
+"[| OK {i. i<I} Component; i<I |] ==> \
+\ ALL k. Component i: stable ({s. C s = c s i + sumj I i k} Int \
+\ {s. ALL j:{i. i<I}. j~=i --> c s j = c k j})";
+by (blast_tac (claset() addIs [[p2, p3] MRS stable_Int]) 1);
+qed "p2_p3_lemma1";
+
+
+Goal "(ALL k. F:stable ({s. C s = (c s) i + sumj I i k} Int \
+\ {s. ALL j:{i. i<I}. j~=i --> c s j = c k j})) \
+\ ==> (F:stable {s. C s = c s i + sumj I i s})";
+by (full_simp_tac (simpset() addsimps [constrains_def, stable_def]) 1);
+by (force_tac (claset() addSIs [sumj_ext], simpset()) 1);
+qed "p2_p3_lemma2";
+
+
+Goal "[| OK {i. i<I} Component; i<I |] \
+\ ==> Component i: stable {s. C s = c s i + sumj I i s}";
+by (blast_tac (claset() addIs [p2_p3_lemma1 RS p2_p3_lemma2]) 1);
+qed "p2_p3";
+
+
+(* Compositional correctness *)
+Goalw [invariant_def]
+ "[| 0<I; OK {i. i<I} Component |] \
+\ ==> (JN i:{i. i<I}. (Component i)) : invariant {s. C s = sum I s}";
+by (simp_tac (simpset() addsimps [JN_stable, sum_sumj_eq2]) 1);
+by (auto_tac (claset() addSIs [sum0 RS mp, p2_p3],
+ simpset()));
+qed "safety";
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/Comp/Counterc.thy Mon Mar 05 15:32:54 2001 +0100
@@ -0,0 +1,43 @@
+(* Title: HOL/UNITY/Counterc
+ ID: $Id$
+ Author: Sidi O Ehmety, Cambridge University Computer Laboratory
+ Copyright 2001 University of Cambridge
+
+A family of similar counters, version with a full use of "compatibility "
+
+From Charpentier and Chandy,
+Examples of Program Composition Illustrating the Use of Universal Properties
+ In J. Rolim (editor), Parallel and Distributed Processing,
+ Spriner LNCS 1586 (1999), pages 1215-1227.
+*)
+
+Counterc = Comp +
+types state
+arities state :: term
+
+consts
+ C :: "state=>int"
+ c :: "state=>nat=>int"
+
+consts
+ sum :: "[nat,state]=>int"
+ sumj :: "[nat, nat, state]=>int"
+
+primrec (* sum I s = sigma_{i<I}. c s i *)
+ "sum 0 s = #0"
+ "sum (Suc i) s = (c s) i + sum i s"
+
+primrec
+ "sumj 0 i s = #0"
+ "sumj (Suc n) i s = (if n=i then sum n s else (c s) n + sumj n i s)"
+
+types command = "(state*state)set"
+
+constdefs
+ a :: "nat=>command"
+ "a i == {(s, s'). (c s') i = (c s) i + #1 & (C s') = (C s) + #1}"
+
+ Component :: "nat => state program"
+ "Component i == mk_program({s. C s = #0 & (c s) i = #0}, {a i},
+ UN G: preserves (%s. (c s) i). Acts G)"
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/Comp/Handshake.ML Mon Mar 05 15:32:54 2001 +0100
@@ -0,0 +1,49 @@
+(* Title: HOL/UNITY/Handshake
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1998 University of Cambridge
+
+Handshake Protocol
+
+From Misra, "Asynchronous Compositions of Programs", Section 5.3.2
+*)
+
+Addsimps [F_def RS def_prg_Init, G_def RS def_prg_Init];
+program_defs_ref := [F_def, G_def];
+
+Addsimps (map simp_of_act [cmdF_def, cmdG_def]);
+Addsimps [simp_of_set invFG_def];
+
+
+Goal "(F Join G) : Always invFG";
+by (rtac AlwaysI 1);
+by (Force_tac 1);
+by (rtac (constrains_imp_Constrains RS StableI) 1);
+by Auto_tac;
+by (constrains_tac 2);
+by (auto_tac (claset() addIs [order_antisym] addSEs [le_SucE], simpset()));
+by (constrains_tac 1);
+qed "invFG";
+
+Goal "(F Join G) : ({s. NF s = k} - {s. BB s}) LeadsTo \
+\ ({s. NF s = k} Int {s. BB s})";
+by (rtac (stable_Join_ensures1 RS leadsTo_Basis RS leadsTo_imp_LeadsTo) 1);
+by (ensures_tac "cmdG" 2);
+by (constrains_tac 1);
+qed "lemma2_1";
+
+Goal "(F Join G) : ({s. NF s = k} Int {s. BB s}) LeadsTo {s. k < NF s}";
+by (rtac (stable_Join_ensures2 RS leadsTo_Basis RS leadsTo_imp_LeadsTo) 1);
+by (constrains_tac 2);
+by (ensures_tac "cmdF" 1);
+qed "lemma2_2";
+
+Goal "(F Join G) : UNIV LeadsTo {s. m < NF s}";
+by (rtac LeadsTo_weaken_R 1);
+by (res_inst_tac [("f", "NF"), ("l","Suc m"), ("B","{}")]
+ GreaterThan_bounded_induct 1);
+(*The inductive step is (F Join G) : {x. NF x = ma} LeadsTo {x. ma < NF x}*)
+by (auto_tac (claset() addSIs [lemma2_1, lemma2_2]
+ addIs[LeadsTo_Trans, LeadsTo_Diff],
+ simpset() addsimps [vimage_def]));
+qed "progress";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/Comp/Handshake.thy Mon Mar 05 15:32:54 2001 +0100
@@ -0,0 +1,37 @@
+(* Title: HOL/UNITY/Handshake.thy
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1998 University of Cambridge
+
+Handshake Protocol
+
+From Misra, "Asynchronous Compositions of Programs", Section 5.3.2
+*)
+
+Handshake = Union +
+
+record state =
+ BB :: bool
+ NF :: nat
+ NG :: nat
+
+constdefs
+ (*F's program*)
+ cmdF :: "(state*state) set"
+ "cmdF == {(s,s'). s' = s (|NF:= Suc(NF s), BB:=False|) & BB s}"
+
+ F :: "state program"
+ "F == mk_program ({s. NF s = 0 & BB s}, {cmdF}, UNIV)"
+
+ (*G's program*)
+ cmdG :: "(state*state) set"
+ "cmdG == {(s,s'). s' = s (|NG:= Suc(NG s), BB:=True|) & ~ BB s}"
+
+ G :: "state program"
+ "G == mk_program ({s. NG s = 0 & BB s}, {cmdG}, UNIV)"
+
+ (*the joint invariant*)
+ invFG :: "state set"
+ "invFG == {s. NG s <= NF s & NF s <= Suc (NG s) & (BB s = (NF s = NG s))}"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/Comp/Priority.ML Mon Mar 05 15:32:54 2001 +0100
@@ -0,0 +1,239 @@
+(* Title: HOL/UNITY/Priority
+ ID: $Id$
+ Author: Sidi O Ehmety, Cambridge University Computer Laboratory
+ Copyright 2001 University of Cambridge
+
+The priority system
+
+From Charpentier and Chandy,
+Examples of Program Composition Illustrating the Use of Universal Properties
+ In J. Rolim (editor), Parallel and Distributed Processing,
+ Spriner LNCS 1586 (1999), pages 1215-1227.
+*)
+
+Addsimps [Component_def RS def_prg_Init];
+program_defs_ref := [Component_def, system_def];
+Addsimps [highest_def, lowest_def];
+Addsimps [simp_of_act act_def];
+Addsimps (map simp_of_set [Highest_def, Lowest_def]);
+
+
+
+
+(**** Component correctness proofs ****)
+
+(* neighbors is stable *)
+Goal "Component i: stable {s. neighbors k s = n}";
+by (constrains_tac 1);
+by Auto_tac;
+qed "Component_neighbors_stable";
+
+(* property 4 *)
+Goal
+"Component i: {s. ((i,j):s) = b} Int (- Highest i) co {s. ((i,j):s)=b}";
+by (constrains_tac 1);
+qed "Component_waits_priority";
+
+(* property 5: charpentier and Chandy mistakenly express it as
+ 'transient Highest i'. Consider the case where i has neighbors *)
+Goal
+ "Component i: {s. neighbors i s ~= {}} Int Highest i \
+\ ensures - Highest i";
+by (ensures_tac "act i" 1);
+by (REPEAT(Fast_tac 1));
+qed "Component_yields_priority";
+
+(* or better *)
+Goal "Component i: Highest i ensures Lowest i";
+by (ensures_tac "act i" 1);
+by (REPEAT(Fast_tac 1));
+qed "Component_yields_priority'";
+
+(* property 6: Component doesn't introduce cycle *)
+Goal "Component i: Highest i co Highest i Un Lowest i";
+by (constrains_tac 1);
+by (Fast_tac 1);
+qed "Component_well_behaves";
+
+(* property 7: local axiom *)
+Goal "Component i: stable {s. ALL j k. j~=i & k~=i--> ((j,k):s) = b j k}";
+by (constrains_tac 1);
+qed "locality";
+
+
+(**** System properties ****)
+(* property 8: strictly universal *)
+
+Goalw [Safety_def]
+ "system: stable Safety";
+by (rtac stable_INT 1);
+by (constrains_tac 1);
+by (Fast_tac 1);
+qed "Safety";
+
+(* property 13: universal *)
+Goal
+"system: {s. s = q} co {s. s=q} Un {s. EX i. derive i q s}";
+by (constrains_tac 1);
+by (Blast_tac 1);
+qed "p13";
+
+(* property 14: the 'above set' of a Component that hasn't got
+ priority doesn't increase *)
+Goal
+"ALL j. system: -Highest i Int {s. j~:above i s} co {s. j~:above i s}";
+by (Clarify_tac 1);
+by (cut_inst_tac [("i", "j")] reach_lemma 1);
+by (constrains_tac 1);
+by (auto_tac (claset(), simpset() addsimps [trancl_converse]));
+qed "above_not_increase";
+
+Goal
+"system: -Highest i Int {s. above i s = x} co {s. above i s <= x}";
+by (cut_inst_tac [("i", "i")] above_not_increase 1);
+by (asm_full_simp_tac (simpset() addsimps
+ [trancl_converse, constrains_def]) 1);
+by (Blast_tac 1);
+qed "above_not_increase'";
+
+
+
+(* p15: universal property: all Components well behave *)
+Goal "ALL i. system: Highest i co Highest i Un Lowest i";
+by (Clarify_tac 1);
+by (constrains_tac 1);
+by Auto_tac;
+qed "system_well_behaves";
+
+
+Goal "Acyclic = (INT i. {s. i~:above i s})";
+by (auto_tac (claset(), simpset()
+ addsimps [Acyclic_def, acyclic_def, trancl_converse]));
+qed "Acyclic_eq";
+
+
+val lemma = [above_not_increase RS spec,
+ system_well_behaves RS spec] MRS constrains_Un;
+Goal
+"system: stable Acyclic";
+by (auto_tac (claset() addSIs [stable_INT, stableI,
+ lemma RS constrains_weaken],
+ simpset() addsimps [Acyclic_eq,
+ image0_r_iff_image0_trancl,trancl_converse]));
+qed "Acyclic_stable";
+
+
+Goalw [Acyclic_def, Maximal_def]
+"Acyclic <= Maximal";
+by (Clarify_tac 1);
+by (dtac above_lemma_b 1);
+by Auto_tac;
+qed "Acyclic_subset_Maximal";
+
+(* property 17: original one is an invariant *)
+Goal
+"system: stable (Acyclic Int Maximal)";
+by (simp_tac (simpset() addsimps
+ [Acyclic_subset_Maximal RS Int_absorb2, Acyclic_stable]) 1);
+qed "Acyclic_Maximal_stable";
+
+
+(* propert 5: existential property *)
+
+Goal "system: Highest i leadsTo Lowest i";
+by (ensures_tac "act i" 1);
+by (auto_tac (claset(), simpset() addsimps [Component_def]));
+qed "Highest_leadsTo_Lowest";
+
+(* a lowest i can never be in any abover set *)
+Goal "Lowest i <= (INT k. {s. i~:above k s})";
+by (auto_tac (claset(),
+ simpset() addsimps [image0_r_iff_image0_trancl, trancl_converse]));
+qed "Lowest_above_subset";
+
+(* property 18: a simpler proof than the original, one which uses psp *)
+Goal "system: Highest i leadsTo (INT k. {s. i~:above k s})";
+by (rtac leadsTo_weaken_R 1);
+by (rtac Lowest_above_subset 2);
+by (rtac Highest_leadsTo_Lowest 1);
+qed "Highest_escapes_above";
+
+Goal
+"system: Highest j Int {s. j:above i s} leadsTo {s. j~:above i s}";
+by (blast_tac (claset() addIs
+ [[Highest_escapes_above, Int_lower1, INT_lower] MRS leadsTo_weaken]) 1);
+qed "Highest_escapes_above'";
+
+(*** The main result: above set decreases ***)
+(* The original proof of the following formula was wrong *)
+val above_decreases_lemma =
+[Highest_escapes_above', above_not_increase'] MRS psp RS leadsTo_weaken;
+
+Goal "Highest i = {s. above i s ={}}";
+by (auto_tac (claset(),
+ simpset() addsimps [image0_trancl_iff_image0_r]));
+qed "Highest_iff_above0";
+
+
+Goal
+"system: (UN j. {s. above i s = x} Int {s. j:above i s} Int Highest j) \
+\ leadsTo {s. above i s < x}";
+by (rtac leadsTo_UN 1);
+by (rtac single_leadsTo_I 1);
+by (Clarify_tac 1);
+by (res_inst_tac [("x2", "above i x")] above_decreases_lemma 1);
+by (ALLGOALS(full_simp_tac (simpset() delsimps [Highest_def]
+ addsimps [Highest_iff_above0])));
+by (REPEAT(Blast_tac 1));
+qed "above_decreases";
+
+(** Just a massage of conditions to have the desired form ***)
+Goalw [Maximal_def, Maximal'_def, Highest_def]
+"Maximal = Maximal'";
+by (Blast_tac 1);
+qed "Maximal_eq_Maximal'";
+
+Goal "x~={} ==> \
+\ Acyclic Int {s. above i s = x} <= \
+\ (UN j. {s. above i s = x} Int {s. j:above i s} Int Highest j)";
+by (res_inst_tac [("B", "Maximal' Int {s. above i s = x}")] subset_trans 1);
+by (simp_tac (simpset() addsimps [Maximal_eq_Maximal' RS sym]) 1);
+by (blast_tac (claset() addIs [Acyclic_subset_Maximal RS subsetD]) 1);
+by (simp_tac (simpset() delsimps [above_def] addsimps [Maximal'_def, Highest_iff_above0]) 1);
+by (Blast_tac 1);
+qed "Acyclic_subset";
+
+val above_decreases' = [above_decreases, Acyclic_subset] MRS leadsTo_weaken_L;
+val above_decreases_psp = [above_decreases', Acyclic_stable] MRS psp_stable;
+
+Goal
+"x~={}==> \
+\ system: Acyclic Int {s. above i s = x} leadsTo Acyclic Int {s. above i s < x}";
+by (etac (above_decreases_psp RS leadsTo_weaken) 1);
+by (Blast_tac 1);
+by Auto_tac;
+qed "above_decreases_psp'";
+
+
+val finite_psubset_induct = wf_finite_psubset RS leadsTo_wf_induct;
+val leadsTo_weaken_L' = rotate_prems 1 leadsTo_weaken_L;
+
+
+Goal "system: Acyclic leadsTo Highest i";
+by (res_inst_tac [("f", "%s. above i s")] finite_psubset_induct 1);
+by (asm_simp_tac (simpset() delsimps [Highest_def, above_def]
+ addsimps [Highest_iff_above0,
+ vimage_def, finite_psubset_def]) 1);
+by (Clarify_tac 1);
+by (case_tac "m={}" 1);
+by (rtac (Int_lower2 RS leadsTo_weaken_L') 1);
+by (force_tac (claset(), simpset() addsimps [leadsTo_refl]) 1);
+by (res_inst_tac [("A'", "Acyclic Int {x. above i x < m}")]
+ leadsTo_weaken_R 1);
+by (REPEAT(blast_tac (claset() addIs [above_decreases_psp']) 1));
+qed "Progress";
+
+(* We have proved all (relevant) theorems given in the paper *)
+(* We didn't assume any thing about the relation r *)
+(* It is not necessary that r be a priority relation as assumed in the original proof *)
+(* It suffices that we start from a state which is finite and acyclic *)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/Comp/Priority.thy Mon Mar 05 15:32:54 2001 +0100
@@ -0,0 +1,68 @@
+(* Title: HOL/UNITY/Priority
+ ID: $Id$
+ Author: Sidi O Ehmety, Cambridge University Computer Laboratory
+ Copyright 2001 University of Cambridge
+
+The priority system
+
+From Charpentier and Chandy,
+Examples of Program Composition Illustrating the Use of Universal Properties
+ In J. Rolim (editor), Parallel and Distributed Processing,
+ Spriner LNCS 1586 (1999), pages 1215-1227.
+*)
+
+Priority = PriorityAux + Comp + SubstAx +
+
+types state = "(vertex*vertex)set"
+types command = "vertex=>(state*state)set"
+
+consts
+ (* the initial state *)
+ init :: "(vertex*vertex)set"
+
+constdefs
+ (* from the definitions given in section 4.4 *)
+ (* i has highest priority in r *)
+ highest :: "[vertex, (vertex*vertex)set]=>bool"
+ "highest i r == A i r = {}"
+
+ (* i has lowest priority in r *)
+ lowest :: "[vertex, (vertex*vertex)set]=>bool"
+ "lowest i r == R i r = {}"
+
+ act :: command
+ "act i == {(s, s'). s'=reverse i s & highest i s}"
+
+ (* All components start with the same initial state *)
+ Component :: "vertex=>state program"
+ "Component i == mk_program({init}, {act i}, UNIV)"
+
+ (* Abbreviations *)
+ Highest :: "vertex=>state set"
+ "Highest i == {s. highest i s}"
+
+ Lowest :: "vertex=>state set"
+ "Lowest i == {s. lowest i s}"
+
+ Acyclic :: "state set"
+ "Acyclic == {s. acyclic s}"
+
+ (* Every above set has a maximal vertex: two equivalent defs. *)
+
+ Maximal :: "state set"
+ "Maximal == INT i. {s. ~highest i s-->(EX j:above i s. highest j s)}"
+
+ Maximal' :: "state set"
+ "Maximal' == INT i. Highest i Un (UN j. {s. j:above i s} Int Highest j)"
+
+
+ Safety :: "state set"
+ "Safety == INT i. {s. highest i s --> (ALL j:neighbors i s. ~highest j s)}"
+
+
+ (* Composition of a finite set of component;
+ the vertex 'UNIV' is finite by assumption *)
+
+ system :: "state program"
+ "system == JN i. Component i"
+end
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/Comp/PriorityAux.ML Mon Mar 05 15:32:54 2001 +0100
@@ -0,0 +1,116 @@
+(* Title: HOL/UNITY/PriorityAux
+ ID: $Id$
+ Author: Sidi O Ehmety, Cambridge University Computer Laboratory
+ Copyright 2001 University of Cambridge
+
+Auxiliary definitions needed in Priority.thy
+*)
+
+Addsimps [derive_def, derive1_def, symcl_def, A_def, R_def,
+ above_def, reach_def, reverse_def, neighbors_def];
+
+(*All vertex sets are finite \\<dots>*)
+AddIffs [[subset_UNIV, finite_vertex_univ] MRS finite_subset];
+
+(* and relatons over vertex are finite too *)
+AddIffs [[subset_UNIV, [finite_vertex_univ, finite_vertex_univ]
+ MRS finite_Prod_UNIV] MRS finite_subset];
+
+
+(* The equalities (above i r = {}) = (A i r = {})
+ and (reach i r = {}) = (R i r) rely on the following theorem *)
+
+Goal "((r^+)``{i} = {}) = (r``{i} = {})";
+by Auto_tac;
+by (etac trancl_induct 1);
+by Auto_tac;
+qed "image0_trancl_iff_image0_r";
+
+(* Another form usefull in some situation *)
+Goal "(r``{i}={}) = (ALL x. ((i,x):r^+) = False)";
+by Auto_tac;
+by (dtac (image0_trancl_iff_image0_r RS ssubst) 1);
+by Auto_tac;
+qed "image0_r_iff_image0_trancl";
+
+
+(* In finite universe acyclic coincides with wf *)
+Goal
+"!!r::(vertex*vertex)set. acyclic r = wf r";
+by (auto_tac (claset(), simpset() addsimps [wf_iff_acyclic_if_finite]));
+qed "acyclic_eq_wf";
+
+(* derive and derive1 are equivalent *)
+Goal "derive i r q = derive1 i r q";
+by Auto_tac;
+qed "derive_derive1_eq";
+
+(* Lemma 1 *)
+Goalw [reach_def]
+"[| x:reach i q; derive1 k r q |] ==> x~=k --> x:reach i r";
+by (etac ImageE 1);
+by (etac trancl_induct 1);
+by (case_tac "i=k" 1);
+by (auto_tac (claset() addIs [r_into_trancl], simpset()));
+by (dres_inst_tac [("x", "y")] spec 1);
+by (rotate_tac ~1 1);
+by (dres_inst_tac [("x", "z")] spec 1);
+by (auto_tac (claset() addDs [r_into_trancl] addIs [trancl_trans], simpset()));
+qed "lemma1_a";
+
+Goal "ALL k r q. derive k r q -->(reach i q <= (reach i r Un {k}))";
+by (REPEAT(rtac allI 1));
+by (rtac impI 1);
+by (rtac subsetI 1 THEN dtac lemma1_a 1);
+by (auto_tac (claset(), simpset() addsimps [derive_derive1_eq]
+ delsimps [reach_def, derive_def, derive1_def]));
+qed "reach_lemma";
+
+(* An other possible formulation of the above theorem based on
+ the equivalence x:reach y r = y:above x r *)
+Goal
+"(ALL i. reach i q <= (reach i r Un {k})) =\
+\ (ALL x. x~=k --> (ALL i. i~:above x r --> i~:above x q))";
+by (auto_tac (claset(), simpset() addsimps [trancl_converse]));
+qed "reach_above_lemma";
+
+(* Lemma 2 *)
+Goal
+"(z, i):r^+ ==> (ALL y. (y, z):r --> (y, i)~:r^+) = ((r^-1)``{z}={})";
+by Auto_tac;
+by (forw_inst_tac [("r", "r")] trancl_into_trancl2 1);
+by Auto_tac;
+qed "maximal_converse_image0";
+
+Goal
+ "acyclic r ==> A i r~={}-->(EX j:above i r. A j r = {})";
+by (full_simp_tac (simpset()
+ addsimps [acyclic_eq_wf, wf_eq_minimal]) 1);
+by (dres_inst_tac [("x", "((r^-1)^+)``{i}")] spec 1);
+by Auto_tac;
+by (rotate_tac ~1 1);
+by (asm_full_simp_tac (simpset()
+ addsimps [maximal_converse_image0, trancl_converse]) 1);
+qed "above_lemma_a";
+
+
+Goal
+ "acyclic r ==> above i r~={}-->(EX j:above i r. above j r = {})";
+by (dtac above_lemma_a 1);
+by (auto_tac (claset(), simpset()
+ addsimps [image0_trancl_iff_image0_r]));
+qed "above_lemma_b";
+
+
+
+
+
+
+
+
+
+
+
+
+
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/Comp/PriorityAux.thy Mon Mar 05 15:32:54 2001 +0100
@@ -0,0 +1,53 @@
+(* Title: HOL/UNITY/PriorityAux
+ ID: $Id$
+ Author: Sidi O Ehmety, Cambridge University Computer Laboratory
+ Copyright 2001 University of Cambridge
+
+Auxiliary definitions needed in Priority.thy
+*)
+
+PriorityAux = Main +
+
+types vertex
+arities vertex::term
+
+constdefs
+ (* symmetric closure: removes the orientation of a relation *)
+ symcl :: "(vertex*vertex)set=>(vertex*vertex)set"
+ "symcl r == r Un (r^-1)"
+
+ (* Neighbors of a vertex i *)
+ neighbors :: "[vertex, (vertex*vertex)set]=>vertex set"
+ "neighbors i r == ((r Un r^-1)``{i}) - {i}"
+
+ R :: "[vertex, (vertex*vertex)set]=>vertex set"
+ "R i r == r``{i}"
+
+ A :: "[vertex, (vertex*vertex)set]=>vertex set"
+ "A i r == (r^-1)``{i}"
+
+ (* reachable and above vertices: the original notation was R* and A* *)
+ reach :: "[vertex, (vertex*vertex)set]=> vertex set"
+ "reach i r == (r^+)``{i}"
+
+ above :: "[vertex, (vertex*vertex)set]=> vertex set"
+ "above i r == ((r^-1)^+)``{i}"
+
+ reverse :: "[vertex, (vertex*vertex) set]=>(vertex*vertex)set"
+ "reverse i r == (r - {(x,y). x=i | y=i} Int r) Un ({(x,y). x=i|y=i} Int r)^-1"
+
+ (* The original definition *)
+ derive1 :: "[vertex, (vertex*vertex)set, (vertex*vertex)set]=>bool"
+ "derive1 i r q == symcl r = symcl q &
+ (ALL k k'. k~=i & k'~=i -->((k,k'):r) = ((k,k'):q)) &
+ A i r = {} & R i q = {}"
+
+ (* Our alternative definition *)
+ derive :: "[vertex, (vertex*vertex)set, (vertex*vertex)set]=>bool"
+ "derive i r q == A i r = {} & (q = reverse i r)"
+
+rules
+ (* we assume that the universe of vertices is finite *)
+ finite_vertex_univ "finite (UNIV :: vertex set)"
+
+end
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/Comp/README.html Mon Mar 05 15:32:54 2001 +0100
@@ -0,0 +1,39 @@
+<!-- $Id$ -->
+<HTML><HEAD><TITLE>HOL/UNITY/README</TITLE></HEAD><BODY>
+
+<H2>UNITY: Examples Involving Program Composition</H2>
+
+<P>
+The directory presents verification examples involving program composition.
+They are mostly taken from the works of Chandy, Charpentier and Chandy.
+
+<UL>
+<LI>examples of <em>universal properties</em>:
+the counter (<A HREF="Counter.thy"><CODE>Counter.thy</CODE></A>)
+and priority system (<A HREF="Priority.thy"><CODE>Priority.thy</CODE></A>)
+
+<LI>the allocation system (<A HREF="Alloc.thy"><CODE>Alloc.thy</CODE></A>)
+
+<LI>client implementation (<A HREF="Client.thy"><CODE>Client.thy</CODE></A>)
+
+<LI>allocator implementation (<A HREF="AllocImpl.thy"><CODE>AllocImpl.thy</CODE></A>)
+
+<LI>the handshake protocol
+(<A HREF="Handshake.thy"><CODE>Handshake.thy</CODE></A>)
+
+<LI>the timer array (demonstrates arrays of processes)
+(<A HREF="TimerArray.thy"><CODE>TimerArray.thy</CODE></A>)
+</UL>
+
+<P> Safety proofs (invariants) are often proved automatically. Progress
+proofs involving ENSURES can sometimes be proved automatically. The
+level of automation appears to be about the same as in HOL-UNITY by Flemming
+Andersen et al.
+
+<HR>
+<P>Last modified on $Date$
+
+<ADDRESS>
+<A NAME="lcp@cl.cam.ac.uk" HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A>
+</ADDRESS>
+</BODY></HTML>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/Comp/TimerArray.ML Mon Mar 05 15:32:54 2001 +0100
@@ -0,0 +1,53 @@
+(* Title: HOL/UNITY/TimerArray.thy
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1998 University of Cambridge
+
+A trivial example of reasoning about an array of processes
+*)
+
+Addsimps [Timer_def RS def_prg_Init];
+program_defs_ref := [Timer_def];
+
+Addsimps [count_def, decr_def];
+
+(*Demonstrates induction, but not used in the following proof*)
+Goal "Timer : UNIV leadsTo {s. count s = 0}";
+by (res_inst_tac [("f", "count")] lessThan_induct 1);
+by (Simp_tac 1);
+by (case_tac "m" 1);
+by (force_tac (claset() addSIs [subset_imp_leadsTo], simpset()) 1);
+by (ensures_tac "decr" 1);
+qed "Timer_leadsTo_zero";
+
+Goal "Timer : preserves snd";
+by (rtac preservesI 1);
+by (constrains_tac 1);
+qed "Timer_preserves_snd";
+AddIffs [Timer_preserves_snd];
+
+Addsimps [PLam_stable];
+
+Goal "finite I \
+\ ==> (plam i: I. Timer) : UNIV leadsTo {(s,uu). ALL i:I. s i = 0}";
+by (eres_inst_tac [("A'1", "%i. lift_set i ({0} <*> UNIV)")]
+ (finite_stable_completion RS leadsTo_weaken) 1);
+by Auto_tac;
+(*Safety property, already reduced to the single Timer case*)
+by (constrains_tac 2);
+(*Progress property for the array of Timers*)
+by (res_inst_tac [("f", "sub i o fst")] lessThan_induct 1);
+by (case_tac "m" 1);
+(*Annoying need to massage the conditions to have the form (... <*> UNIV)*)
+by (auto_tac (claset() addIs [subset_imp_leadsTo],
+ simpset() addsimps [insert_absorb, lessThan_Suc RS sym,
+ lift_set_Un_distrib RS sym,
+ Times_Un_distrib1 RS sym,
+ Times_Diff_distrib1 RS sym]));
+by (rename_tac "n" 1);
+by (rtac PLam_leadsTo_Basis 1);
+by (auto_tac (claset(), simpset() addsimps [lessThan_Suc RS sym]));
+by (constrains_tac 1);
+by (res_inst_tac [("act", "decr")] transientI 1);
+by (auto_tac (claset(), simpset() addsimps [Timer_def]));
+qed "TimerArray_leadsTo_zero";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/Comp/TimerArray.thy Mon Mar 05 15:32:54 2001 +0100
@@ -0,0 +1,23 @@
+(* Title: HOL/UNITY/TimerArray.thy
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1998 University of Cambridge
+
+A trivial example of reasoning about an array of processes
+*)
+
+TimerArray = PPROD +
+
+types 'a state = "nat * 'a" (*second component allows new variables*)
+
+constdefs
+ count :: "'a state => nat"
+ "count s == fst s"
+
+ decr :: "('a state * 'a state) set"
+ "decr == UN n uu. {((Suc n, uu), (n,uu))}"
+
+ Timer :: 'a state program
+ "Timer == mk_program (UNIV, {decr}, UNIV)"
+
+end