# HG changeset patch # User paulson # Date 941120043 -7200 # Node ID a00ad4ca623250f85f70abd32e469150a3cafed6 # Parent 6b3e345c47b359ebcffe2e4b424609049dc9dd2c expandshort; tidied diff -r 6b3e345c47b3 -r a00ad4ca6232 src/HOL/UNITY/Alloc.ML --- a/src/HOL/UNITY/Alloc.ML Thu Oct 28 16:07:12 1999 +0200 +++ b/src/HOL/UNITY/Alloc.ML Thu Oct 28 16:14:03 1999 +0200 @@ -73,16 +73,6 @@ qed "inv_sysOfAlloc_eq"; Addsimps [inv_sysOfAlloc_eq]; - -(*SHOULD NOT BE NECESSARY???????????????? -Goal "!!z. (| allocGiv = allocGiv z, allocAsk = allocAsk z, \ -\ allocRel = allocRel z |) = z"; -by (auto_tac (claset() addSWrapper record_split_wrapper, - simpset())); -qed "allocState_eq"; -Addsimps [allocState_eq]; -????*) - (**SHOULD NOT BE NECESSARY: The various injections into the system state need to be treated symmetrically or done automatically*) Goalw [sysOfClient_def] "inj sysOfClient"; @@ -331,7 +321,27 @@ (*** Proof of the progress property (2) ***) -(*we begin with proofs identical to System_Increasing_rel and +(** Lemmas about localTo **) + +Goal "extend sysOfAlloc F : client localTo[C] extend sysOfClient G"; +by (rtac localTo_UNIV_imp_localTo 1); +by (simp_tac (simpset() addsimps [LOCALTO_def, Diff_def, extend_def, + stable_def, constrains_def, + image_eq_UN, extend_act_def, + sysOfAlloc_def, sysOfClient_def]) 1); +by (Force_tac 1); +qed "sysOfAlloc_in_client_localTo_xl_Client"; + +Goal "extend sysOfClient (plam i:I. F) : \ +\ (sub i o client) localTo[C] extend sysOfClient (lift_prog i F)"; +by (rtac localTo_UNIV_imp_localTo 1); +by (rtac (client_export (extend_set_UNIV_eq RS equalityD2 RSN + (2, extend_localTo_extend_I))) 1); +by (rtac PLam_sub_localTo 1); +qed "sysOfClient_in_client_localTo_xl_Client"; + + +(*Now there are proofs identical to System_Increasing_rel and System_Increasing_allocRel: tactics needed!*) (*progress (2), step 1 is System_Increasing_ask and System_Increasing_rel*) @@ -376,85 +386,44 @@ by (auto_tac(claset() addDs [set_mono], simpset())); qed "System_Bounded_allocAsk"; -(*progress (2), step 5*) +(*progress (2), step 5 is System_Increasing_allocGiv*) +(*progress (2), step 6*) Goal "i < Nclients ==> System : Increasing (giv o sub i o client)"; by (rtac Follows_Increasing1 1); by (blast_tac (claset() addIs [Network_Giv RS component_guaranteesD, System_Increasing_allocGiv]) 1); qed "System_Increasing_giv"; -(*progress (2), step 6*) - -(*A LOT of work just to lift "Client_Progress" to the array*) +(*Lemma (?). A LOT of work just to lift "Client_Progress" to the array*) Goal "lift_prog i Client \ -\ : Increasing (giv o sub i) Int ((%z. z i) LocalTo (lift_prog i Client)) \ +\ : Increasing (giv o sub i) Int (sub i LocalTo (lift_prog i Client)) \ \ guarantees \ \ (INT h. {s. h <= (giv o sub i) s & \ \ h pfixGe (ask o sub i) s} \ \ LeadsTo {s. tokens h <= (tokens o rel o sub i) s})"; by (rtac (Client_Progress RS drop_prog_guarantees) 1); -by (rtac (lift_export extending_LeadsTo RS extending_weaken RS extending_INT) 2); +by (rtac (lift_export extending_LeadsTo RS extending_weaken RS + extending_INT) 2); by (rtac subset_refl 4); by (simp_tac (simpset()addsimps [lift_export Collect_eq_extend_set RS sym]) 3); -by (force_tac (claset(), simpset() addsimps [lift_prog_correct]) 2); +by (force_tac (claset(), simpset() addsimps [sub_def, lift_prog_correct]) 2); by (rtac (lift_export projecting_Increasing RS projecting_weaken) 1); by (auto_tac (claset(), simpset() addsimps [o_def])); qed "Client_i_Progress"; -Goal "extend sysOfAlloc F \ -\ : (v o client) localTo[C] extend sysOfClient (lift_prog i Client)"; -br localTo_UNIV_imp_localTo 1; -by (simp_tac (simpset() addsimps [LOCALTO_def, Diff_def, extend_def, - stable_def, constrains_def, - image_eq_UN, extend_act_def, - sysOfAlloc_def, sysOfClient_def]) 1); -by (Force_tac 1); -qed "sysOfAlloc_in_client_localTo_xl_Client"; - -Goal "extend sysOfClient (plam x: I. Client) : ((%z. z i) o client) \ -\ localTo[C] extend sysOfClient (lift_prog i Client)"; -br localTo_UNIV_imp_localTo 1; -by (rtac (client_export (extend_set_UNIV_eq RS equalityD2 RSN - (2, extend_localTo_extend_I))) 1); -br (rewrite_rule [sub_def] PLam_sub_localTo) 1; -qed "sysOfClient_in_client_localTo_xl_Client"; - -xxxxxxxxxxxxxxxx; - -THIS PROOF requires an extra locality specification for Network: - Network : rel o sub i o client localTo[C] - extend sysOfClient (lift_prog i Client) -and similarly for ask o sub i o client. - -The LeadsTo rule must be refined so as not to require the whole of client to -be local, since giv is written by the Network. +(*needed??*) +Goalw [PLam_def] + "(plam x:lessThan Nclients. Client) \ +\ : (INT i : lessThan Nclients. \ +\ Increasing (giv o sub i) Int (sub i LocalTo (lift_prog i Client))) \ +\ guarantees \ +\ (INT i : lessThan Nclients. \ +\ INT h. {s. h <= (giv o sub i) s & \ +\ h pfixGe (ask o sub i) s} \ +\ LeadsTo {s. tokens h <= (tokens o rel o sub i) s})"; +br guarantees_JN_INT 1; +br Client_i_Progress 1; +qed "PLam_Client_Progress"; - -Goalw [System_def] - "i < Nclients \ -\ ==> System : (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 (guarantees_Join_I2 RS guaranteesD) 1); -by (rtac (guarantees_PLam_I RS project_guarantees) 1); -by (rtac Client_i_Progress 1); -by (Force_tac 1); -by (rtac (client_export extending_LeadsTo RS extending_weaken RS extending_INT) 2); -by (rtac subset_refl 4); -by (simp_tac (simpset()addsimps [client_export Collect_eq_extend_set RS sym]) 3); -(*The next step goes wrong: it makes an impossible localTo subgoal*) -(*blast_tac doesn't use HO unification*) -by (fast_tac (claset() addIs [projecting_Int, - client_export projecting_Increasing, - component_PLam, - client_export projecting_LocalTo]) 1); -by (asm_simp_tac - (simpset() addsimps [rewrite_rule [System_def] System_Increasing_giv, - LocalTo_def, Join_localTo, - sysOfClient_in_client_localTo_xl_Client, - sysOfAlloc_in_client_localTo_xl_Client]) 2); -auto(); - - - +(*progress (2), step 7*)