# HG changeset patch # User wenzelm # Date 1165187147 -3600 # Node ID e7c1f1a77d18555bc432ea71dae3b9b3bd01bcb9 # Parent 2cc00b360b2c0fbe18743a057c82f345d9534ec4 converted legacy ML script; diff -r 2cc00b360b2c -r e7c1f1a77d18 src/HOL/IsaMakefile --- a/src/HOL/IsaMakefile Sun Dec 03 23:25:41 2006 +0100 +++ b/src/HOL/IsaMakefile Mon Dec 04 00:05:47 2006 +0100 @@ -441,10 +441,9 @@ UNITY/Simple/Deadlock.thy UNITY/Simple/Lift.thy UNITY/Simple/Mutex.thy \ UNITY/Simple/NSP_Bad.thy UNITY/Simple/Network.thy\ UNITY/Simple/Reach.thy UNITY/Simple/Reachability.thy UNITY/Simple/Token.thy\ - UNITY/Comp/Alloc.ML UNITY/Comp/Alloc.thy \ - UNITY/Comp/AllocBase.thy UNITY/Comp/AllocImpl.thy UNITY/Comp/Client.thy \ - UNITY/Comp/Counter.thy UNITY/Comp/Counterc.thy UNITY/Comp/Handshake.thy \ - UNITY/Comp/PriorityAux.thy \ + UNITY/Comp/Alloc.thy UNITY/Comp/AllocBase.thy UNITY/Comp/AllocImpl.thy \ + UNITY/Comp/Client.thy UNITY/Comp/Counter.thy UNITY/Comp/Counterc.thy \ + UNITY/Comp/Handshake.thy UNITY/Comp/PriorityAux.thy \ UNITY/Comp/Priority.thy UNITY/Comp/Progress.thy \ UNITY/Comp/TimerArray.thy\ UNITY/document/root.tex diff -r 2cc00b360b2c -r e7c1f1a77d18 src/HOL/UNITY/Comp/Alloc.ML --- a/src/HOL/UNITY/Comp/Alloc.ML Sun Dec 03 23:25:41 2006 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,745 +0,0 @@ -(* 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]; - - -(* FIXME no longer works -- had been commented out unintentially for a long time - -(*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. (\\i: lessThan Nclients. (tokens o sub i o allocGiv) s) \ -\ <= NbT + (\\i: lessThan Nclients. (tokens o sub i o allocRel) s)}"; -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 2cc00b360b2c -r e7c1f1a77d18 src/HOL/UNITY/Comp/Alloc.thy --- a/src/HOL/UNITY/Comp/Alloc.thy Sun Dec 03 23:25:41 2006 +0100 +++ b/src/HOL/UNITY/Comp/Alloc.thy Mon Dec 04 00:05:47 2006 +0100 @@ -259,6 +259,853 @@ (plam x: lessThan Nclients. rename client_map Client))" **) -ML {* use_legacy_bindings (the_context ()) *} +(*Perhaps equalities.ML shouldn't add this in the first place!*) +declare image_Collect [simp del] + +declare subset_preserves_o [THEN [2] rev_subsetD, intro] +declare subset_preserves_o [THEN [2] rev_subsetD, simp] +declare funPair_o_distrib [simp] +declare Always_INT_distrib [simp] +declare o_apply [simp del] + +(*For rewriting of specifications related by "guarantees"*) +lemmas [simp] = + 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 [THEN image_Int] + bij_image_Collect_eq + +ML {* +(*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]; +*} + +lemmas lessThanBspec = lessThan_iff [THEN iffD2, THEN [2] bspec] + +ML {* +local + val lessThanBspec = thm "lessThanBspec" +in +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 +end +*} + +(*** bijectivity of sysOfAlloc [MUST BE AUTOMATED] ***) +ML {* +val record_auto_tac = + auto_tac (claset() addIs [ext] addSWrapper record_split_wrapper, + simpset() addsimps [thm "sysOfAlloc_def", thm "sysOfClient_def", + thm "client_map_def", thm "non_dummy_def", thm "funPair_def", thm "o_apply", thm "Let_def"]) +*} + + +lemma inj_sysOfAlloc [iff]: "inj sysOfAlloc" + apply (unfold sysOfAlloc_def Let_def) + apply (rule inj_onI) + apply (tactic record_auto_tac) + done + +(*We need the inverse; also having it simplifies the proof of surjectivity*) +lemma inv_sysOfAlloc_eq [simp]: "!!s. inv sysOfAlloc s = + (| allocGiv = allocGiv s, + allocAsk = allocAsk s, + allocRel = allocRel s, + allocState_d.dummy = (client s, dummy s) |)" + apply (rule inj_sysOfAlloc [THEN inv_f_eq]) + apply (tactic record_auto_tac) + done + +lemma surj_sysOfAlloc [iff]: "surj sysOfAlloc" + apply (simp add: surj_iff expand_fun_eq o_apply) + apply (tactic record_auto_tac) + done + +lemma bij_sysOfAlloc [iff]: "bij sysOfAlloc" + apply (blast intro: bijI) + done + + +(*** bijectivity of sysOfClient ***) + +lemma inj_sysOfClient [iff]: "inj sysOfClient" + apply (unfold sysOfClient_def) + apply (rule inj_onI) + apply (tactic record_auto_tac) + done + +lemma inv_sysOfClient_eq [simp]: "!!s. inv sysOfClient s = + (client s, + (| allocGiv = allocGiv s, + allocAsk = allocAsk s, + allocRel = allocRel s, + allocState_d.dummy = systemState.dummy s|) )" + apply (rule inj_sysOfClient [THEN inv_f_eq]) + apply (tactic record_auto_tac) + done + +lemma surj_sysOfClient [iff]: "surj sysOfClient" + apply (simp add: surj_iff expand_fun_eq o_apply) + apply (tactic record_auto_tac) + done + +lemma bij_sysOfClient [iff]: "bij sysOfClient" + apply (blast intro: bijI) + done + + +(*** bijectivity of client_map ***) + +lemma inj_client_map [iff]: "inj client_map" + apply (unfold inj_on_def) + apply (tactic record_auto_tac) + done + +lemma inv_client_map_eq [simp]: "!!s. inv client_map s = + (%(x,y).(|giv = giv x, ask = ask x, rel = rel x, + clientState_d.dummy = y|)) s" + apply (rule inj_client_map [THEN inv_f_eq]) + apply (tactic record_auto_tac) + done + +lemma surj_client_map [iff]: "surj client_map" + apply (simp add: surj_iff expand_fun_eq o_apply) + apply (tactic record_auto_tac) + done + +lemma bij_client_map [iff]: "bij client_map" + apply (blast intro: bijI) + done + + +(** o-simprules for client_map **) + +lemma fst_o_client_map: "fst o client_map = non_dummy" + apply (unfold client_map_def) + apply (rule fst_o_funPair) + done + +ML {* bind_thms ("fst_o_client_map'", make_o_equivs (thm "fst_o_client_map")) *} +declare fst_o_client_map' [simp] + +lemma snd_o_client_map: "snd o client_map = clientState_d.dummy" + apply (unfold client_map_def) + apply (rule snd_o_funPair) + done + +ML {* bind_thms ("snd_o_client_map'", make_o_equivs (thm "snd_o_client_map")) *} +declare snd_o_client_map' [simp] + +(** o-simprules for sysOfAlloc [MUST BE AUTOMATED] **) + +lemma client_o_sysOfAlloc: "client o sysOfAlloc = fst o allocState_d.dummy " + apply (tactic record_auto_tac) + done + +ML {* bind_thms ("client_o_sysOfAlloc'", make_o_equivs (thm "client_o_sysOfAlloc")) *} +declare client_o_sysOfAlloc' [simp] + +lemma allocGiv_o_sysOfAlloc_eq: "allocGiv o sysOfAlloc = allocGiv" + apply (tactic record_auto_tac) + done + +ML {* bind_thms ("allocGiv_o_sysOfAlloc_eq'", make_o_equivs (thm "allocGiv_o_sysOfAlloc_eq")) *} +declare allocGiv_o_sysOfAlloc_eq' [simp] + +lemma allocAsk_o_sysOfAlloc_eq: "allocAsk o sysOfAlloc = allocAsk" + apply (tactic record_auto_tac) + done + +ML {* bind_thms ("allocAsk_o_sysOfAlloc_eq'", make_o_equivs (thm "allocAsk_o_sysOfAlloc_eq")) *} +declare allocAsk_o_sysOfAlloc_eq' [simp] + +lemma allocRel_o_sysOfAlloc_eq: "allocRel o sysOfAlloc = allocRel" + apply (tactic record_auto_tac) + done + +ML {* bind_thms ("allocRel_o_sysOfAlloc_eq'", make_o_equivs (thm "allocRel_o_sysOfAlloc_eq")) *} +declare allocRel_o_sysOfAlloc_eq' [simp] + +(** o-simprules for sysOfClient [MUST BE AUTOMATED] **) + +lemma client_o_sysOfClient: "client o sysOfClient = fst" + apply (tactic record_auto_tac) + done + +ML {* bind_thms ("client_o_sysOfClient'", make_o_equivs (thm "client_o_sysOfClient")) *} +declare client_o_sysOfClient' [simp] + +lemma allocGiv_o_sysOfClient_eq: "allocGiv o sysOfClient = allocGiv o snd " + apply (tactic record_auto_tac) + done + +ML {* bind_thms ("allocGiv_o_sysOfClient_eq'", make_o_equivs (thm "allocGiv_o_sysOfClient_eq")) *} +declare allocGiv_o_sysOfClient_eq' [simp] + +lemma allocAsk_o_sysOfClient_eq: "allocAsk o sysOfClient = allocAsk o snd " + apply (tactic record_auto_tac) + done + +ML {* bind_thms ("allocAsk_o_sysOfClient_eq'", make_o_equivs (thm "allocAsk_o_sysOfClient_eq")) *} +declare allocAsk_o_sysOfClient_eq' [simp] + +lemma allocRel_o_sysOfClient_eq: "allocRel o sysOfClient = allocRel o snd " + apply (tactic record_auto_tac) + done + +ML {* bind_thms ("allocRel_o_sysOfClient_eq'", make_o_equivs (thm "allocRel_o_sysOfClient_eq")) *} +declare allocRel_o_sysOfClient_eq' [simp] + +lemma allocGiv_o_inv_sysOfAlloc_eq: "allocGiv o inv sysOfAlloc = allocGiv" + apply (simp add: o_def) + done + +ML {* bind_thms ("allocGiv_o_inv_sysOfAlloc_eq'", make_o_equivs (thm "allocGiv_o_inv_sysOfAlloc_eq")) *} +declare allocGiv_o_inv_sysOfAlloc_eq' [simp] + +lemma allocAsk_o_inv_sysOfAlloc_eq: "allocAsk o inv sysOfAlloc = allocAsk" + apply (simp add: o_def) + done + +ML {* bind_thms ("allocAsk_o_inv_sysOfAlloc_eq'", make_o_equivs (thm "allocAsk_o_inv_sysOfAlloc_eq")) *} +declare allocAsk_o_inv_sysOfAlloc_eq' [simp] + +lemma allocRel_o_inv_sysOfAlloc_eq: "allocRel o inv sysOfAlloc = allocRel" + apply (simp add: o_def) + done + +ML {* bind_thms ("allocRel_o_inv_sysOfAlloc_eq'", make_o_equivs (thm "allocRel_o_inv_sysOfAlloc_eq")) *} +declare allocRel_o_inv_sysOfAlloc_eq' [simp] + +lemma rel_inv_client_map_drop_map: "(rel o inv client_map o drop_map i o inv sysOfClient) = + rel o sub i o client" + apply (simp add: o_def drop_map_def) + done + +ML {* bind_thms ("rel_inv_client_map_drop_map'", make_o_equivs (thm "rel_inv_client_map_drop_map")) *} +declare rel_inv_client_map_drop_map [simp] + +lemma ask_inv_client_map_drop_map: "(ask o inv client_map o drop_map i o inv sysOfClient) = + ask o sub i o client" + apply (simp add: o_def drop_map_def) + done + +ML {* bind_thms ("ask_inv_client_map_drop_map'", make_o_equivs (thm "ask_inv_client_map_drop_map")) *} +declare ask_inv_client_map_drop_map [simp] + +(** +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 +**) + +declare finite_lessThan [iff] + +(*Client : *) +lemmas 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 + +ML {* +val [Client_Increasing_ask, Client_Increasing_rel, + Client_Bounded, Client_Progress, Client_AllowedActs, + Client_preserves_giv, Client_preserves_dummy] = + thm "Client" |> simplify (simpset() addsimps (thms "client_spec_simps") ) + |> list_of_Int; + +bind_thm ("Client_Increasing_ask", Client_Increasing_ask); +bind_thm ("Client_Increasing_rel", Client_Increasing_rel); +bind_thm ("Client_Bounded", Client_Bounded); +bind_thm ("Client_Progress", Client_Progress); +bind_thm ("Client_AllowedActs", Client_AllowedActs); +bind_thm ("Client_preserves_giv", Client_preserves_giv); +bind_thm ("Client_preserves_dummy", Client_preserves_dummy); +*} + +declare + Client_Increasing_ask [iff] + Client_Increasing_rel [iff] + Client_Bounded [iff] + Client_preserves_giv [iff] + Client_preserves_dummy [iff] + + +(*Network : *) +lemmas 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 + +ML {* +val [Network_Ask, Network_Giv, Network_Rel, Network_AllowedActs, + Network_preserves_allocGiv, Network_preserves_rel, + Network_preserves_ask] = + thm "Network" |> simplify (simpset() addsimps (thms "network_spec_simps")) + |> list_of_Int; + +bind_thm ("Network_Ask", Network_Ask); +bind_thm ("Network_Giv", Network_Giv); +bind_thm ("Network_Rel", Network_Rel); +bind_thm ("Network_AllowedActs", Network_AllowedActs); +bind_thm ("Network_preserves_allocGiv", Network_preserves_allocGiv); +bind_thm ("Network_preserves_rel", Network_preserves_rel); +bind_thm ("Network_preserves_ask", Network_preserves_ask); +*} + +declare Network_preserves_allocGiv [iff] + +declare + Network_preserves_rel [simp] + Network_preserves_ask [simp] + +declare + Network_preserves_rel [simplified o_def, simp] + Network_preserves_ask [simplified o_def, simp] + +(*Alloc : *) +lemmas alloc_spec_simps = + alloc_spec_def alloc_increasing_def alloc_safety_def + alloc_progress_def alloc_allowed_acts_def alloc_preserves_def + +ML {* +val [Alloc_Increasing_0, Alloc_Safety, Alloc_Progress, Alloc_AllowedActs, + Alloc_preserves_allocRel, Alloc_preserves_allocAsk, + Alloc_preserves_dummy] = + thm "Alloc" |> simplify (simpset() addsimps (thms "alloc_spec_simps")) + |> list_of_Int; + +bind_thm ("Alloc_Increasing_0", Alloc_Increasing_0); +bind_thm ("Alloc_Safety", Alloc_Safety); +bind_thm ("Alloc_Progress", Alloc_Progress); +bind_thm ("Alloc_AllowedActs", Alloc_AllowedActs); +bind_thm ("Alloc_preserves_allocRel", Alloc_preserves_allocRel); +bind_thm ("Alloc_preserves_allocAsk", Alloc_preserves_allocAsk); +bind_thm ("Alloc_preserves_dummy", Alloc_preserves_dummy); +*} + +(*Strip off the INT in the guarantees postcondition*) +ML +{* +bind_thm ("Alloc_Increasing", normalize Alloc_Increasing_0) +*} + +declare + Alloc_preserves_allocRel [iff] + Alloc_preserves_allocAsk [iff] + Alloc_preserves_dummy [iff] + + +(** Components lemmas [MUST BE AUTOMATED] **) + +lemma Network_component_System: "Network Join + ((rename sysOfClient + (plam x: (lessThan Nclients). rename client_map Client)) Join + rename sysOfAlloc Alloc) + = System" + apply (simp add: System_def Join_ac) + done + +lemma Client_component_System: "(rename sysOfClient + (plam x: (lessThan Nclients). rename client_map Client)) Join + (Network Join rename sysOfAlloc Alloc) = System" + apply (simp add: System_def Join_ac) + done + +lemma Alloc_component_System: "rename sysOfAlloc Alloc Join + ((rename sysOfClient (plam x: (lessThan Nclients). rename client_map Client)) Join + Network) = System" + apply (simp add: System_def Join_ac) + done + +declare + Client_component_System [iff] + Network_component_System [iff] + Alloc_component_System [iff] + +(** These preservation laws should be generated automatically **) + +lemma Client_Allowed [simp]: "Allowed Client = preserves rel Int preserves ask" + apply (auto simp add: Allowed_def Client_AllowedActs safety_prop_Acts_iff) + done + +lemma Network_Allowed [simp]: "Allowed Network = + preserves allocRel Int + (INT i: lessThan Nclients. preserves(giv o sub i o client))" + apply (auto simp add: Allowed_def Network_AllowedActs safety_prop_Acts_iff) + done + +lemma Alloc_Allowed [simp]: "Allowed Alloc = preserves allocGiv" + apply (auto simp add: Allowed_def Alloc_AllowedActs safety_prop_Acts_iff) + done + +(*needed in rename_client_map_tac*) +lemma OK_lift_rename_Client [simp]: "OK I (%i. lift i (rename client_map Client))" + apply (rule OK_lift_I) + apply auto + apply (drule_tac w1 = rel in subset_preserves_o [THEN [2] rev_subsetD]) + apply (drule_tac [2] w1 = ask in subset_preserves_o [THEN [2] rev_subsetD]) + apply (auto simp add: o_def split_def) + done + + +(*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! +*) +ML +{* +val rename_client_map_tac = + EVERY [ + simp_tac (simpset() addsimps [thm "rename_guarantees_eq_rename_inv"]) 1, + rtac (thm "guarantees_PLam_I") 1, + assume_tac 2, + (*preserves: routine reasoning*) + asm_simp_tac (simpset() addsimps [thm "lift_preserves_sub"]) 2, + (*the guarantee for "lift i (rename client_map Client)" *) + asm_simp_tac + (simpset() addsimps [thm "lift_guarantees_eq_lift_inv", + thm "rename_guarantees_eq_rename_inv", + thm "bij_imp_bij_inv", thm "surj_rename" RS thm "surj_range", + thm "inv_inv_eq"]) 1, + asm_simp_tac + (simpset() addsimps [thm "o_def", thm "non_dummy_def", thm "guarantees_Int_right"]) 1] +*} + +(*Lifting Client_Increasing to systemState*) +lemma rename_Client_Increasing: "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)" + apply (tactic rename_client_map_tac) + sorry + +lemma preserves_sub_fst_lift_map: "[| F : preserves w; i ~= j |] + ==> F : preserves (sub i o fst o lift_map j o funPair v w)" + apply (auto simp add: lift_map_def split_def linorder_neq_iff o_def) + apply (drule_tac [!] subset_preserves_o [THEN [2] rev_subsetD]) + apply (auto simp add: o_def) + done + +lemma client_preserves_giv_oo_client_map: "[| i < Nclients; j < Nclients |] + ==> Client : preserves (giv o sub i o fst o lift_map j o client_map)" + apply (case_tac "i=j") + apply (simp add: o_def non_dummy_def) + sorry +(* + apply (drule Client_preserves_dummy [THEN preserves_sub_fst_lift_map]) + apply (drule_tac [!] subset_preserves_o [THEN [2] rev_subsetD]) + apply (simp add: o_def client_map_def) + done +*) + +lemma rename_sysOfClient_ok_Network: + "rename sysOfClient (plam x: lessThan Nclients. rename client_map Client) + ok Network" + apply (auto simp add: ok_iff_Allowed client_preserves_giv_oo_client_map) + done + +lemma rename_sysOfClient_ok_Alloc: + "rename sysOfClient (plam x: lessThan Nclients. rename client_map Client) + ok rename sysOfAlloc Alloc" + apply (simp add: ok_iff_Allowed) + done + +lemma rename_sysOfAlloc_ok_Network: "rename sysOfAlloc Alloc ok Network" + apply (simp add: ok_iff_Allowed) + done + +declare + rename_sysOfClient_ok_Network [iff] + rename_sysOfClient_ok_Alloc [iff] + rename_sysOfAlloc_ok_Network [iff] + +(*The "ok" laws, re-oriented*) +declare + rename_sysOfClient_ok_Network [THEN ok_sym, iff] + rename_sysOfClient_ok_Alloc [THEN ok_sym, iff] + rename_sysOfAlloc_ok_Network [THEN ok_sym] + +lemma System_Increasing: "i < Nclients + ==> System : Increasing (ask o sub i o client) Int + Increasing (rel o sub i o client)" + apply (rule component_guaranteesD [OF rename_Client_Increasing Client_component_System]) + apply auto + done + +lemmas rename_guarantees_sysOfAlloc_I = + bij_sysOfAlloc [THEN rename_rename_guarantees_eq, THEN iffD2, standard] + + +(*Lifting Alloc_Increasing up to the level of systemState*) +ML {* +bind_thm ("rename_Alloc_Increasing", + thm "Alloc_Increasing" RS thm "rename_guarantees_sysOfAlloc_I" + |> simplify (simpset() addsimps [thm "surj_rename" RS thm "surj_range", thm "o_def"])) +*} + +lemma System_Increasing_allocGiv: + "i < Nclients ==> System : Increasing (sub i o allocGiv)" + apply (unfold System_def) + apply (simp add: o_def) + sorry +(* + apply (rule rename_Alloc_Increasing [THEN guarantees_Join_I1, THEN guaranteesD]) + apply auto + done +*) + +ML {* +bind_thms ("System_Increasing'", list_of_Int (thm "System_Increasing")) +*} + +declare System_Increasing' [intro!] + +(** Follows consequences. + The "Always (INT ...) formulation expresses the general safety property + and allows it to be combined using Always_Int_rule below. **) + +lemma System_Follows_rel: + "i < Nclients ==> System : ((sub i o allocRel) Fols (rel o sub i o client))" + apply (auto intro!: Network_Rel [THEN component_guaranteesD]) + sorry + +lemma System_Follows_ask: + "i < Nclients ==> System : ((sub i o allocAsk) Fols (ask o sub i o client))" + sorry +(* + apply (auto intro!: [Network_Ask [THEN component_guaranteesD]]) + done +*) + +lemma System_Follows_allocGiv: + "i < Nclients ==> System : (giv o sub i o client) Fols (sub i o allocGiv)" + apply (auto intro!: Network_Giv [THEN component_guaranteesD] + rename_Alloc_Increasing [THEN component_guaranteesD]) + apply (simp_all add: o_def non_dummy_def) + sorry +(* + apply (auto intro!: rename_Alloc_Increasing [THEN component_guaranteesD]) + done +*) + +lemma Always_giv_le_allocGiv: "System : Always (INT i: lessThan Nclients. + {s. (giv o sub i o client) s <= (sub i o allocGiv) s})" + apply auto + sorry +(* + apply (erule System_Follows_allocGiv [THEN Follows_Bounded]) + done +*) + +lemma Always_allocAsk_le_ask: "System : Always (INT i: lessThan Nclients. + {s. (sub i o allocAsk) s <= (ask o sub i o client) s})" + apply auto + sorry +(* + apply (erule System_Follows_ask [THEN Follows_Bounded]) + done +*) + +lemma Always_allocRel_le_rel: "System : Always (INT i: lessThan Nclients. + {s. (sub i o allocRel) s <= (rel o sub i o client) s})" + sorry +(* + apply (auto intro!: Follows_Bounded System_Follows_rel) + done +*) + +(*** 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) *) +lemmas System_Increasing_allocRel = System_Follows_rel [THEN Follows_Increasing1, standard] + +(*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.*) +ML {* + val rename_Alloc_Safety = + thm "Alloc_Safety" RS thm "rename_guarantees_sysOfAlloc_I" + |> simplify (simpset() addsimps [o_def]) +*} + +(*safety (1), step 3*) +(* +lemma System_sum_bounded: + "System : Always {s. (\i: lessThan Nclients. (tokens o sub i o allocGiv) s) + <= NbT + (\i: lessThan Nclients. (tokens o sub i o allocRel) s)}" + apply (simp add: o_apply) + apply (rule rename_Alloc_Safety [THEN component_guaranteesD]) + apply (auto simp add: o_simp System_Increasing_allocRel) + done +*) + +(** Follows reasoning **) + +lemma Always_tokens_giv_le_allocGiv: "System : Always (INT i: lessThan Nclients. + {s. (tokens o giv o sub i o client) s + <= (tokens o sub i o allocGiv) s})" + apply (rule Always_giv_le_allocGiv [THEN Always_weaken]) + apply (auto intro: tokens_mono_prefix simp add: o_apply) + done + +lemma Always_tokens_allocRel_le_rel: "System : Always (INT i: lessThan Nclients. + {s. (tokens o sub i o allocRel) s + <= (tokens o rel o sub i o client) s})" + apply (rule Always_allocRel_le_rel [THEN Always_weaken]) + apply (auto intro: tokens_mono_prefix simp add: o_apply) + done + +(*safety (1), step 4 (final result!) *) +lemma System_safety: "System : system_safety" + apply (unfold system_safety_def) + sorry +(* + apply (tactic {* rtac (Always_Int_rule [thm "System_sum_bounded", + thm "Always_tokens_giv_le_allocGiv", thm "Always_tokens_allocRel_le_rel"] RS + thm "Always_weaken") 1 *}) + apply auto + apply (rule setsum_fun_mono [THEN order_trans]) + apply (drule_tac [2] order_trans) + apply (rule_tac [2] add_le_mono [OF order_refl setsum_fun_mono]) + prefer 3 apply assumption + apply auto + done +*) + +(*** 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) *) +lemmas System_Increasing_allocAsk = System_Follows_ask [THEN Follows_Increasing1, standard] + +(*progress (2), step 3: lifting "Client_Bounded" to systemState*) +lemma rename_Client_Bounded: "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}" + apply (tactic rename_client_map_tac) + sorry + +lemma System_Bounded_ask: "i < Nclients + ==> System : Always + {s. ALL elt : set ((ask o sub i o client) s). elt <= NbT}" + apply (rule component_guaranteesD [OF rename_Client_Bounded Client_component_System]) + apply auto + done + +lemma Collect_all_imp_eq: "{x. ALL y. P y --> Q x y} = (INT y: {y. P y}. {x. Q x y})" + apply blast + done + +(*progress (2), step 4*) +lemma System_Bounded_allocAsk: "System : Always {s. ALL i System : Increasing (giv o sub i o client) *) +lemmas System_Increasing_giv = System_Follows_allocGiv [THEN Follows_Increasing1, standard] + + +lemma rename_Client_Progress: "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})" + apply (tactic rename_client_map_tac) + sorry +(* + apply (simp add: Client_Progress [simplified o_def]) + done +*) + + +(*progress (2), step 7*) +lemma System_Client_Progress: + "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})" + apply (rule INT_I) +(*Couldn't have just used Auto_tac since the "INT h" must be kept*) + apply (rule component_guaranteesD [OF rename_Client_Progress Client_component_System]) + apply (auto simp add: System_Increasing_giv) + done + +(*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} *) +(* +bind_thm ("lemma", + [thm "System_Follows_ask" RS thm "Follows_Bounded", + thm "System_Follows_allocGiv" RS thm "Follows_LeadsTo"] MRS thm "Always_LeadsToD"); +*) + +(*A more complicated variant of the previous one*) +(* +val lemma2 = [lemma, + System_Follows_ask RS Follows_Increasing1 RS IncreasingD] + MRS PSP_Stable; +*) + +lemma lemma3: "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}" + apply (rule single_LeadsTo_I) + sorry +(* + apply (rule_tac k6 = "h" and x2 = " (sub i o allocAsk) s" in lemma2 [THEN LeadsTo_weaken]) + apply auto + apply (blast intro: trans_Ge [THEN trans_genPrefix THEN transD] prefix_imp_pfixGe) + done +*) + + +(*progress (2), step 8: Client i's "release" action is visible system-wide*) +lemma System_Alloc_Client_Progress: "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}" + apply (rule LeadsTo_Trans) + prefer 2 + apply (drule System_Follows_rel [THEN + mono_tokens [THEN mono_Follows_o, THEN [2] rev_subsetD], + THEN Follows_LeadsTo]) + apply (simp add: o_assoc) + apply (rule LeadsTo_Trans) + apply (cut_tac [2] System_Client_Progress) + prefer 2 + apply (blast intro: LeadsTo_Basis) + apply (erule lemma3) + done + +(*Lifting Alloc_Progress up to the level of systemState*) +ML {* +bind_thm ("rename_Alloc_Progress", + thm "Alloc_Progress" RS thm "rename_guarantees_sysOfAlloc_I" + |> simplify (simpset() addsimps [thm "o_def"])) +*} + +(*progress (2), step 9*) +lemma System_Alloc_Progress: + "System : (INT i : (lessThan Nclients). + INT h. {s. h <= (sub i o allocAsk) s} + LeadsTo {s. h pfixLe (sub i o allocGiv) s})" + apply (simp only: o_apply sub_def) + sorry +(* + apply (rule rename_Alloc_Progress [THEN component_guaranteesD]) + apply (auto simp add: + System_Increasing_allocRel [simplified o_def] + System_Increasing_allocAsk [simplified o_def] + System_Bounded_allocAsk [simplified o_def] + System_Alloc_Client_Progress [simplified o_def]) + done +*) + + +(*progress (2), step 10 (final result!) *) +lemma System_Progress: "System : system_progress" + apply (unfold system_progress_def) + apply (cut_tac System_Alloc_Progress) + apply (blast intro: LeadsTo_Trans + System_Follows_allocGiv [THEN Follows_LeadsTo_pfixLe] + System_Follows_ask [THEN Follows_LeadsTo]) + done + + +(*Ultimate goal*) +lemma System_correct: "System : system_spec" + apply (unfold system_spec_def) + apply (blast intro: System_safety System_Progress) + done + + +(** SOME lemmas no longer used **) + +lemma non_dummy_eq_o_funPair: "non_dummy = (% (g,a,r). (| giv = g, ask = a, rel = r |)) o + (funPair giv (funPair ask rel))" + apply (rule ext) + apply (auto simp add: o_def non_dummy_def) + done + +lemma preserves_non_dummy_eq: "(preserves non_dummy) = + (preserves rel Int preserves ask Int preserves giv)" + apply (simp add: non_dummy_eq_o_funPair) + apply auto + apply (drule_tac w1 = rel in subset_preserves_o [THEN [2] rev_subsetD]) + apply (drule_tac [2] w1 = ask in subset_preserves_o [THEN [2] rev_subsetD]) + apply (drule_tac [3] w1 = giv in subset_preserves_o [THEN [2] rev_subsetD]) + apply (auto simp add: o_def) + done + +(*Could go to Extend.ML*) +lemma bij_fst_inv_inv_eq: "bij f ==> fst (inv (%(x, u). inv f x) z) = f z" + apply (rule fst_inv_equalityI) + apply (rule_tac f = "%z. (f z, ?h z) " in surjI) + apply (simp add: bij_is_inj inv_f_f) + apply (simp add: bij_is_surj surj_f_inv_f) + done end