# HG changeset patch # User paulson # Date 951989369 -3600 # Node ID 108fcc85a767934e9f07965e27265d33b128cae4 # Parent 0e329578b0ef461e5b3c51a48cfc950cc69052f2 polished version of the Allocator using Rename diff -r 0e329578b0ef -r 108fcc85a767 src/HOL/UNITY/Alloc.ML --- a/src/HOL/UNITY/Alloc.ML Thu Mar 02 10:26:22 2000 +0100 +++ b/src/HOL/UNITY/Alloc.ML Thu Mar 02 10:29:29 2000 +0100 @@ -5,8 +5,6 @@ Specification of Chandy and Charpentier's Allocator -guarantees_PLam_I looks wrong: refers to lift_prog - Goal "(plam x: lessThan Nclients. Client) = x"; Client :: (clientState * ((nat => clientState) * 'b)) program *) @@ -21,8 +19,7 @@ AddIs [impOfSubs subset_preserves_o]; Addsimps [funPair_o_distrib]; -Addsimps [rename_preserves]; - +Addsimps [Always_INT_distrib]; Delsimps [o_apply]; (*Eliminate the "o" operator*) @@ -33,7 +30,9 @@ 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_image_leadsTo, rename_image_LeadsTo, + rename_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 = @@ -91,7 +90,7 @@ Addsimps [inv_sysOfAlloc_eq]; Goal "surj sysOfAlloc"; -by (simp_tac (simpset() addsimps [surj_iff, expand_fun_eq, o_def]) 1); +by (simp_tac (simpset() addsimps [surj_iff, expand_fun_eq, o_apply]) 1); by (auto_tac (claset() addSWrapper record_split_wrapper, simpset() addsimps [sysOfAlloc_def, Let_def])); qed "surj_sysOfAlloc"; @@ -124,7 +123,7 @@ Addsimps [inv_sysOfClient_eq]; Goal "surj sysOfClient"; -by (simp_tac (simpset() addsimps [surj_iff, expand_fun_eq, o_def]) 1); +by (simp_tac (simpset() addsimps [surj_iff, expand_fun_eq, o_apply]) 1); by (auto_tac (claset() addSWrapper record_split_wrapper, simpset() addsimps [sysOfClient_def])); qed "surj_sysOfClient"; @@ -154,7 +153,7 @@ Addsimps [inv_client_map_eq]; Goal "surj client_map"; -by (simp_tac (simpset() addsimps [surj_iff, expand_fun_eq, o_def]) 1); +by (simp_tac (simpset() addsimps [surj_iff, expand_fun_eq, o_apply]) 1); by (auto_tac (claset() addSWrapper record_split_wrapper, simpset() addsimps [client_map_def, non_extra_def])); qed "surj_client_map"; @@ -168,77 +167,73 @@ (** o-simprules for client_map **) -Goal "fst o client_map = non_extra"; -by (rtac ext 1); -by (auto_tac (claset() addSWrapper record_split_wrapper, - simpset() addsimps [o_def, client_map_def])); +Goalw [client_map_def] "fst o client_map = non_extra"; +by (rtac fst_o_funPair 1); qed "fst_o_client_map"; Addsimps (make_o_equivs fst_o_client_map); -Goal "snd o client_map = clientState_u.extra"; -by (rtac ext 1); -by (auto_tac (claset() addSWrapper record_split_wrapper, - simpset() addsimps [o_def, client_map_def])); +Goalw [client_map_def] "snd o client_map = clientState_u.extra"; +by (rtac snd_o_funPair 1); qed "snd_o_client_map"; Addsimps (make_o_equivs snd_o_client_map); -(** o-simprules for sysOfAlloc **) +(** o-simprules for sysOfAlloc [MUST BE AUTOMATED] **) Goal "client o sysOfAlloc = fst o allocState_u.extra "; by (rtac ext 1); by (auto_tac (claset() addSWrapper record_split_wrapper, - simpset() addsimps [o_def, sysOfAlloc_def, Let_def])); + simpset() addsimps [o_apply, sysOfAlloc_def, Let_def])); qed "client_o_sysOfAlloc"; Addsimps (make_o_equivs client_o_sysOfAlloc); Goal "allocGiv o sysOfAlloc = allocGiv"; by (rtac ext 1); by (auto_tac (claset() addSWrapper record_split_wrapper, - simpset() addsimps [sysOfAlloc_def, Let_def, o_def])); + simpset() addsimps [sysOfAlloc_def, Let_def, o_apply])); qed "allocGiv_o_sysOfAlloc_eq"; Addsimps (make_o_equivs allocGiv_o_sysOfAlloc_eq); Goal "allocAsk o sysOfAlloc = allocAsk"; by (rtac ext 1); by (auto_tac (claset() addSWrapper record_split_wrapper, - simpset() addsimps [sysOfAlloc_def, Let_def, o_def])); + simpset() addsimps [sysOfAlloc_def, Let_def, o_apply])); qed "allocAsk_o_sysOfAlloc_eq"; Addsimps (make_o_equivs allocAsk_o_sysOfAlloc_eq); Goal "allocRel o sysOfAlloc = allocRel"; by (rtac ext 1); by (auto_tac (claset() addSWrapper record_split_wrapper, - simpset() addsimps [sysOfAlloc_def, Let_def, o_def])); + simpset() addsimps [sysOfAlloc_def, Let_def, o_apply])); qed "allocRel_o_sysOfAlloc_eq"; Addsimps (make_o_equivs allocRel_o_sysOfAlloc_eq); -(** o-simprules for sysOfClient **) +(** o-simprules for sysOfClient [MUST BE AUTOMATED] **) Goal "client o sysOfClient = fst"; by (rtac ext 1); by (auto_tac (claset() addSWrapper record_split_wrapper, - simpset() addsimps [o_def, sysOfClient_def])); + simpset() addsimps [o_apply, sysOfClient_def])); qed "client_o_sysOfClient"; Addsimps (make_o_equivs client_o_sysOfClient); Goal "allocGiv o sysOfClient = allocGiv o snd "; by (rtac ext 1); by (auto_tac (claset() addSWrapper record_split_wrapper, - simpset() addsimps [sysOfClient_def, o_def])); + simpset() addsimps [sysOfClient_def, o_apply])); qed "allocGiv_o_sysOfClient_eq"; Addsimps (make_o_equivs allocGiv_o_sysOfClient_eq); Goal "allocAsk o sysOfClient = allocAsk o snd "; by (rtac ext 1); by (auto_tac (claset() addSWrapper record_split_wrapper, - simpset() addsimps [sysOfClient_def, o_def])); + simpset() addsimps [sysOfClient_def, o_apply])); qed "allocAsk_o_sysOfClient_eq"; Addsimps (make_o_equivs allocAsk_o_sysOfClient_eq); Goal "allocRel o sysOfClient = allocRel o snd "; by (rtac ext 1); by (auto_tac (claset() addSWrapper record_split_wrapper, - simpset() addsimps [sysOfClient_def, o_def])); + simpset() addsimps [sysOfClient_def, o_apply])); qed "allocRel_o_sysOfClient_eq"; Addsimps (make_o_equivs allocRel_o_sysOfClient_eq); @@ -302,10 +297,8 @@ AddIffs (Alloc_preserves |> simplify (simpset()) |> list_of_Int); -(** Components lemmas **) +(** Components lemmas [MUST BE AUTOMATED] **) -(*Alternative is to say that System = Network Join F such that F preserves - certain state variables*) Goal "Network Join \ \ ((rename sysOfClient \ \ (plam x: lessThan Nclients. rename client_map Client)) Join \ @@ -348,15 +341,30 @@ by (asm_simp_tac (simpset() addsimps [lift_preserves_sub]) 2); (*the guarantee for "lift i (rename client_map Client)" *) by (asm_simp_tac - (simpset() addsimps [lift_guarantees_eq_lift_inv, + (simpset() addsimps [lift_guarantees_eq_lift_inv, rename_guarantees_eq_rename_inv, bij_imp_bij_inv, surj_rename RS surj_range, - bij_rename, bij_image_INT, bij_is_inj RS image_Int, inv_inv_eq]) 1); by (asm_simp_tac (simpset() addsimps [o_def, non_extra_def, guarantees_Int_right]) 1); qed "rename_Client_Increasing"; +(*The proofs of rename_Client_Bounded and rename_Client_Progress are + similar to the one above. 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. +*) + Goal "i < Nclients \ \ ==> System : Increasing (ask o sub i o client) Int \ \ Increasing (rel o sub i o client)"; @@ -365,13 +373,14 @@ 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 = - [bij_sysOfAlloc RS rename_rename_guarantees_eq, Alloc_Increasing] MRS iffD2 - |> simplify - (simpset() addsimps [bij_rename, surj_rename RS surj_range, - bij_image_INT, - bij_image_Collect_eq, o_def]); + 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)"; @@ -411,22 +420,20 @@ Goal "System : Always (INT i: lessThan Nclients. \ \ {s. (giv o sub i o client) s <= (sub i o allocGiv) s})"; -by (auto_tac (claset(), - simpset() addsimps [Always_INT_distrib])); +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 (claset(), - simpset() addsimps [Always_INT_distrib])); +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() addsimps [Always_INT_distrib])); + simpset())); qed "Always_allocRel_le_rel"; @@ -441,22 +448,16 @@ (*Lifting Alloc_safety up to the level of systemState*) val rename_Alloc_Safety = - [bij_sysOfAlloc RS rename_rename_guarantees_eq, Alloc_Safety] MRS iffD2 - |> simplify - (simpset() addsimps [bij_rename, - bij_image_INT, - bij_image_Collect_eq, o_def]); + Alloc_Safety RS rename_guarantees_sysOfAlloc_I + |> simplify (simpset() addsimps [o_def]); (*safety (1), step 3*) Goal "System : Always {s. sum (%i. (tokens o sub i o allocGiv) s) Nclients \ \ <= NbT + sum (%i. (tokens o sub i o allocRel) s) Nclients}"; -by (simp_tac (simpset() addsimps [o_def]) 1); -by (rtac ([rename_Alloc_Safety, Alloc_component_System] MRS - component_guaranteesD) 1); -(*preserves*) -by (Simp_tac 2); -by (force_tac (claset(), - simpset() addsimps [o_simp System_Increasing_allocRel]) 1); +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"; @@ -518,12 +519,10 @@ by (asm_simp_tac (simpset() addsimps [lift_preserves_sub]) 2); (*the guarantee for "lift i (rename client_map Client)" *) by (asm_simp_tac - (simpset() addsimps [lift_guarantees_eq_lift_inv, + (simpset() addsimps [lift_guarantees_eq_lift_inv, rename_guarantees_eq_rename_inv, bij_imp_bij_inv, surj_rename RS surj_range, - bij_rename, bij_image_INT, bij_is_inj RS image_Int, - rename_image_Always, inv_inv_eq, - bij_image_Collect_eq]) 1); + inv_inv_eq]) 1); by (asm_simp_tac (simpset() addsimps [o_def, non_extra_def]) 1); qed "rename_Client_Bounded"; @@ -539,7 +538,7 @@ Goal "System : Always {s. ALL i : lessThan Nclients. \ \ ALL elt : set ((sub i o allocAsk) s). elt <= NbT}"; by (auto_tac (claset(), - simpset() addsimps [Collect_ball_eq, Always_INT_distrib])); + simpset() addsimps [Collect_ball_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())); @@ -567,13 +566,9 @@ by (asm_simp_tac (simpset() addsimps [lift_preserves_sub]) 2); (*the guarantee for "lift i (rename client_map Client)" *) by (asm_simp_tac - (simpset() addsimps [lift_guarantees_eq_lift_inv, + (simpset() addsimps [lift_guarantees_eq_lift_inv, rename_guarantees_eq_rename_inv, - bij_imp_bij_inv, surj_rename RS surj_range, - bij_rename, bij_image_INT, bij_is_inj RS image_Int, - rename_image_LeadsTo, rename_image_Increasing, - inv_inv_eq, - bij_image_Collect_eq]) 1); + bij_imp_bij_inv, inv_inv_eq]) 1); by (asm_simp_tac (simpset() addsimps [o_def, non_extra_def, rewrite_rule [o_def] Client_Progress]) 1); qed "rename_Client_Progress"; @@ -589,8 +584,7 @@ (*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 (asm_full_simp_tac - (simpset() addsimps [System_Increasing_giv]) 2); +by (asm_full_simp_tac (simpset() addsimps [System_Increasing_giv]) 2); by Auto_tac; qed "System_Client_Progress"; @@ -640,11 +634,8 @@ (*Lifting Alloc_Progress up to the level of systemState*) val rename_Alloc_Progress = - [bij_sysOfAlloc RS rename_rename_guarantees_eq, Alloc_Progress] MRS iffD2 - |> simplify - (simpset() addsimps [bij_rename, surj_rename RS surj_range, - bij_image_INT, bij_is_inj RS image_Int, - bij_image_Collect_eq, o_def]); + Alloc_Progress RS rename_guarantees_sysOfAlloc_I + |> simplify (simpset() addsimps [o_def]); (*progress (2), step 9*) Goal @@ -652,12 +643,8 @@ \ 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_def, sub_def]) 1); -by (rtac ([rename_Alloc_Progress, Alloc_component_System] MRS - component_guaranteesD) 1); -(*preserves*) -by (Simp_tac 2); -(*the guarantees precondition*) +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, diff -r 0e329578b0ef -r 108fcc85a767 src/HOL/UNITY/Lift_prog.ML --- a/src/HOL/UNITY/Lift_prog.ML Thu Mar 02 10:26:22 2000 +0100 +++ b/src/HOL/UNITY/Lift_prog.ML Thu Mar 02 10:29:29 2000 +0100 @@ -360,6 +360,8 @@ by (simp_tac (simpset() addsimps [lift_def, rename_preserves]) 1); qed "lift_preserves_eq"; +(*A useful rewrite. If o, sub have been rewritten out already then can also + use it as rewrite_rule [sub_def, o_def] lift_preserves_sub*) Goal "F : preserves snd \ \ ==> lift i F : preserves (v o sub j o fst) = \ \ (if i=j then F : preserves (v o fst) else True)"; diff -r 0e329578b0ef -r 108fcc85a767 src/HOL/UNITY/PPROD.ML --- a/src/HOL/UNITY/PPROD.ML Thu Mar 02 10:26:22 2000 +0100 +++ b/src/HOL/UNITY/PPROD.ML Thu Mar 02 10:29:29 2000 +0100 @@ -123,6 +123,10 @@ (*** guarantees properties ***) +(*This rule looks unsatisfactory because it refers to "lift". One must use + lift_guarantees_eq_lift_inv to rewrite the first subgoal and + something like lift_preserves_sub to rewrite the third. However there's + no obvious way to alternative for the third premise.*) Goalw [PLam_def] "[| lift i (F i): X guarantees[v] Y; i : I; \ \ ALL j:I. i~=j --> lift j (F j) : preserves v |] \ diff -r 0e329578b0ef -r 108fcc85a767 src/HOL/UNITY/Rename.ML --- a/src/HOL/UNITY/Rename.ML Thu Mar 02 10:26:22 2000 +0100 +++ b/src/HOL/UNITY/Rename.ML Thu Mar 02 10:29:29 2000 +0100 @@ -52,6 +52,12 @@ Addsimps [Init_rename, Acts_rename]; +(*Useful if we don't assume bij h*) +Goalw [rename_def, rename_act_def, extend_def] + "Acts (rename h F) = insert Id (rename_act h `` Acts F)"; +by (asm_simp_tac (simpset() addsimps [export Acts_extend]) 1); +qed "raw_Acts_rename"; + Goalw [rename_act_def, extend_act_def] "(s,s') : act ==> (h s, h s') : rename_act h act"; by Auto_tac; @@ -117,6 +123,8 @@ by Auto_tac; qed "rename_inv_eq"; +(** (rename h) is bijective <=> h is bijective **) + Goal "bij h ==> inj (rename h)"; by (asm_simp_tac (simpset() addsimps [inj_iff, expand_fun_eq, o_def, rename_inv_eq RS sym]) 1); @@ -131,6 +139,30 @@ by (blast_tac (claset() addIs [bijI, inj_rename, surj_rename]) 1); qed "bij_rename"; +Goalw [inj_on_def] "inj (rename h) ==> inj h"; +by Auto_tac; +by (dres_inst_tac [("x", "mk_program ({x}, {})")] spec 1); +by (dres_inst_tac [("x", "mk_program ({y}, {})")] spec 1); +by (auto_tac (claset(), + simpset() addsimps [program_equality_iff, raw_Acts_rename])); +qed "inj_rename_imp_inj"; + +Goalw [surj_def] "surj (rename h) ==> surj h"; +by Auto_tac; +by (dres_inst_tac [("x", "mk_program ({y}, {})")] spec 1); +by (auto_tac (claset() addSEs [equalityE], + simpset() addsimps [program_equality_iff, raw_Acts_rename])); +qed "surj_rename_imp_surj"; + +Goalw [bij_def] "bij (rename h) ==> bij h"; +by (asm_simp_tac + (simpset() addsimps [inj_rename_imp_inj, surj_rename_imp_surj]) 1); +qed "bij_rename_imp_bij"; + +Goal "bij (rename h) = bij h"; +by (blast_tac (claset() addIs [bij_rename, bij_rename_imp_bij]) 1); +qed "bij_rename_iff"; +AddIffs [bij_rename_iff]; (*** the lattice operations ***) @@ -139,10 +171,6 @@ qed "rename_SKIP"; Addsimps [rename_SKIP]; -Goalw [rename_def] "bij h ==> inj (rename h)"; -by (asm_simp_tac (simpset() addsimps [export inj_extend]) 1); -qed "inj_rename"; - Goalw [rename_def] "bij h ==> rename h (F Join G) = rename h F Join rename h G"; by (asm_simp_tac (simpset() addsimps [export extend_Join]) 1); diff -r 0e329578b0ef -r 108fcc85a767 src/HOL/UNITY/UNITY.ML --- a/src/HOL/UNITY/UNITY.ML Thu Mar 02 10:26:22 2000 +0100 +++ b/src/HOL/UNITY/UNITY.ML Thu Mar 02 10:29:29 2000 +0100 @@ -63,8 +63,7 @@ Addsimps [Acts_eq, Init_eq]; -(** The notation of equality for type "program" **) - +(** Equality for UNITY programs **) Goal "mk_program (Init F, Acts F) = F"; by (cut_inst_tac [("x", "F")] Rep_Program 1); @@ -84,6 +83,10 @@ by (auto_tac (claset(), simpset() addsimps [major])); qed "program_equalityE"; +Goal "(F=G) = (Init F = Init G & Acts F = Acts G)"; +by (blast_tac (claset() addIs [program_equalityI, program_equalityE]) 1); +qed "program_equality_iff"; + Addsimps [surjective_mk_program];