# HG changeset patch # User paulson # Date 983802774 -3600 # Node ID ea13ff5a26d125531f4fbdad860c85f04be29376 # Parent 851c90b23a9ef1989b8a967edeaa1051481680bf reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp diff -r 851c90b23a9e -r ea13ff5a26d1 src/HOL/UNITY/Comp/Alloc.ML --- /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 : *) +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 : *) +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 : *) +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 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"; diff -r 851c90b23a9e -r ea13ff5a26d1 src/HOL/UNITY/Comp/Alloc.thy --- /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 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 diff -r 851c90b23a9e -r ea13ff5a26d1 src/HOL/UNITY/Comp/AllocBase.ML --- /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 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 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"; diff -r 851c90b23a9e -r ea13ff5a26d1 src/HOL/UNITY/Comp/AllocBase.thy --- /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 diff -r 851c90b23a9e -r ea13ff5a26d1 src/HOL/UNITY/Comp/AllocImpl.ML --- /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 \ +\ (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 \ +\ (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"; + + diff -r 851c90b23a9e -r ea13ff5a26d1 src/HOL/UNITY/Comp/AllocImpl.thy --- /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 diff -r 851c90b23a9e -r ea13ff5a26d1 src/HOL/UNITY/Comp/Client.ML --- /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 Client Join G : {s. rel s = k & k 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"; diff -r 851c90b23a9e -r ea13ff5a26d1 src/HOL/UNITY/Comp/Client.thy --- /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 diff -r 851c90b23a9e -r ea13ff5a26d1 src/HOL/UNITY/Comp/Counter.ML --- /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 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 (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(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 (JN i:{i. iint + +consts + sum :: "[nat,state]=>int" + sumj :: "[nat, nat, state]=>int" + +primrec (* sum I s = sigma_{icommand" + "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 diff -r 851c90b23a9e -r ea13ff5a26d1 src/HOL/UNITY/Comp/Counterc.ML --- /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 (sum I s = sumj I i s)"; +by (induct_tac "I" 1); +by Auto_tac; +qed_spec_mp "sum_sumj_eq1"; + +Goal "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 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 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 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 \ +\ ALL k. Component i: stable ({s. C s = c s i + sumj I i k} Int \ +\ {s. ALL j:{i. 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 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 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 (JN i:{i. iint" + c :: "state=>nat=>int" + +consts + sum :: "[nat,state]=>int" + sumj :: "[nat, nat, state]=>int" + +primrec (* sum I s = sigma_{icommand" + "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 diff -r 851c90b23a9e -r ea13ff5a26d1 src/HOL/UNITY/Comp/Handshake.ML --- /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"; diff -r 851c90b23a9e -r ea13ff5a26d1 src/HOL/UNITY/Comp/Handshake.thy --- /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 diff -r 851c90b23a9e -r ea13ff5a26d1 src/HOL/UNITY/Comp/Priority.ML --- /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 *) diff -r 851c90b23a9e -r ea13ff5a26d1 src/HOL/UNITY/Comp/Priority.thy --- /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 diff -r 851c90b23a9e -r ea13ff5a26d1 src/HOL/UNITY/Comp/PriorityAux.ML --- /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 \\*) +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"; + + + + + + + + + + + + + + diff -r 851c90b23a9e -r ea13ff5a26d1 src/HOL/UNITY/Comp/PriorityAux.thy --- /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 diff -r 851c90b23a9e -r ea13ff5a26d1 src/HOL/UNITY/Comp/README.html --- /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 @@ + +HOL/UNITY/README + +

UNITY: Examples Involving Program Composition

+ +

+The directory presents verification examples involving program composition. +They are mostly taken from the works of Chandy, Charpentier and Chandy. + +

+ +

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. + +

+

Last modified on $Date$ + +

+lcp@cl.cam.ac.uk +
+ diff -r 851c90b23a9e -r ea13ff5a26d1 src/HOL/UNITY/Comp/TimerArray.ML --- /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"; diff -r 851c90b23a9e -r ea13ff5a26d1 src/HOL/UNITY/Comp/TimerArray.thy --- /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