--- 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 : <unfolded specification> *)
-val client_spec_simps =
- [client_spec_def, client_increasing_def, client_bounded_def,
- client_progress_def, client_allowed_acts_def, client_preserves_def,
- guarantees_Int_right];
-
-val [Client_Increasing_ask, Client_Increasing_rel,
- Client_Bounded, Client_Progress, Client_AllowedActs,
- Client_preserves_giv, Client_preserves_dummy] =
- Client |> simplify (simpset() addsimps client_spec_simps)
- |> list_of_Int;
-
-AddIffs [Client_Increasing_ask, Client_Increasing_rel, Client_Bounded,
- Client_preserves_giv, Client_preserves_dummy];
-
-
-(*Network : <unfolded specification> *)
-val network_spec_simps =
- [network_spec_def, network_ask_def, network_giv_def,
- network_rel_def, network_allowed_acts_def, network_preserves_def,
- ball_conj_distrib];
-
-val [Network_Ask, Network_Giv, Network_Rel, Network_AllowedActs,
- Network_preserves_allocGiv, Network_preserves_rel,
- Network_preserves_ask] =
- Network |> simplify (simpset() addsimps network_spec_simps)
- |> list_of_Int;
-
-AddIffs [Network_preserves_allocGiv];
-
-Addsimps [Network_preserves_rel, Network_preserves_ask];
-Addsimps [o_simp Network_preserves_rel, o_simp Network_preserves_ask];
-
-
-(*Alloc : <unfolded specification> *)
-val alloc_spec_simps =
- [alloc_spec_def, alloc_increasing_def, alloc_safety_def,
- alloc_progress_def, alloc_allowed_acts_def,
- alloc_preserves_def];
-
-val [Alloc_Increasing_0, Alloc_Safety, Alloc_Progress, Alloc_AllowedActs,
- Alloc_preserves_allocRel, Alloc_preserves_allocAsk,
- Alloc_preserves_dummy] =
- Alloc |> simplify (simpset() addsimps alloc_spec_simps)
- |> list_of_Int;
-
-(*Strip off the INT in the guarantees postcondition*)
-val Alloc_Increasing = normalize Alloc_Increasing_0;
-
-AddIffs [Alloc_preserves_allocRel, Alloc_preserves_allocAsk,
- Alloc_preserves_dummy];
-
-(** Components lemmas [MUST BE AUTOMATED] **)
-
-Goal "Network Join \
-\ ((rename sysOfClient \
-\ (plam x: (lessThan Nclients). rename client_map Client)) Join \
-\ rename sysOfAlloc Alloc) \
-\ = System";
-by (simp_tac (simpset() addsimps System_def::Join_ac) 1);
-qed "Network_component_System";
-
-Goal "(rename sysOfClient \
-\ (plam x: (lessThan Nclients). rename client_map Client)) Join \
-\ (Network Join rename sysOfAlloc Alloc) = System";
-by (simp_tac (simpset() addsimps System_def::Join_ac) 1);
-qed "Client_component_System";
-
-Goal "rename sysOfAlloc Alloc Join \
-\ ((rename sysOfClient (plam x: (lessThan Nclients). rename client_map Client)) Join \
-\ Network) = System";
-by (simp_tac (simpset() addsimps System_def::Join_ac) 1);
-qed "Alloc_component_System";
-
-AddIffs [Client_component_System, Network_component_System,
- Alloc_component_System];
-
-(** These preservation laws should be generated automatically **)
-
-Goal "Allowed Client = preserves rel Int preserves ask";
-by (auto_tac (claset(),
- simpset() addsimps [Allowed_def, Client_AllowedActs,
- safety_prop_Acts_iff]));
-qed "Client_Allowed";
-Addsimps [Client_Allowed];
-
-Goal "Allowed Network = \
-\ preserves allocRel Int \
-\ (INT i: lessThan Nclients. preserves(giv o sub i o client))";
-by (auto_tac (claset(),
- simpset() addsimps [Allowed_def, Network_AllowedActs,
- safety_prop_Acts_iff]));
-qed "Network_Allowed";
-Addsimps [Network_Allowed];
-
-Goal "Allowed Alloc = preserves allocGiv";
-by (auto_tac (claset(),
- simpset() addsimps [Allowed_def, Alloc_AllowedActs,
- safety_prop_Acts_iff]));
-qed "Alloc_Allowed";
-Addsimps [Alloc_Allowed];
-
-Goal "OK I (%i. lift i (rename client_map Client))";
-by (rtac OK_lift_I 1);
-by Auto_tac;
-by (dres_inst_tac [("w1", "rel")] (impOfSubs subset_preserves_o) 1);
-by (dres_inst_tac [("w1", "ask")] (impOfSubs subset_preserves_o) 2);
-by (auto_tac (claset(), simpset() addsimps [o_def, split_def]));
-qed "OK_lift_rename_Client";
-Addsimps [OK_lift_rename_Client]; (*needed in rename_client_map_tac*)
-
-(*The proofs of rename_Client_Increasing, rename_Client_Bounded and
- rename_Client_Progress are similar. All require copying out the original
- Client property. A forward proof can be constructed as follows:
-
- Client_Increasing_ask RS
- (bij_client_map RS rename_rename_guarantees_eq RS iffD2)
- RS (lift_lift_guarantees_eq RS iffD2)
- RS guarantees_PLam_I
- RS (bij_sysOfClient RS rename_rename_guarantees_eq RS iffD2)
- |> simplify (simpset() addsimps [lift_image_eq_rename, o_def, split_def,
- surj_rename RS surj_range]);
-
-However, the "preserves" property remains to be discharged, and the unfolding
-of "o" and "sub" complicates subsequent reasoning.
-
-The following tactic works for all three proofs, though it certainly looks
-ad-hoc!
-*)
-val rename_client_map_tac =
- EVERY [
- simp_tac (simpset() addsimps [rename_guarantees_eq_rename_inv]) 1,
- rtac guarantees_PLam_I 1,
- assume_tac 2,
- (*preserves: routine reasoning*)
- asm_simp_tac (simpset() addsimps [lift_preserves_sub]) 2,
- (*the guarantee for "lift i (rename client_map Client)" *)
- asm_simp_tac
- (simpset() addsimps [lift_guarantees_eq_lift_inv,
- rename_guarantees_eq_rename_inv,
- bij_imp_bij_inv, surj_rename RS surj_range,
- inv_inv_eq]) 1,
- asm_simp_tac
- (simpset() addsimps [o_def, non_dummy_def, guarantees_Int_right]) 1];
-
-
-(* 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. (\\<Sum>i: lessThan Nclients. (tokens o sub i o allocGiv) s) \
-\ <= NbT + (\\<Sum>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<Nclients. \
-\ ALL elt : set ((sub i o allocAsk) s). elt <= NbT}";
-by (auto_tac (claset(), simpset() addsimps [Collect_all_imp_eq]));
-by (rtac (Always_Int_rule [Always_allocAsk_le_ask, System_Bounded_ask]
- RS Always_weaken) 1);
-by (auto_tac (claset() addDs [set_mono], simpset()));
-qed "System_Bounded_allocAsk";
-
-(*progress (2), step 5 is System_Increasing_allocGiv*)
-
-(*progress (2), step 6*)
-(* i < Nclients ==> System : Increasing (giv o sub i o client) *)
-bind_thm ("System_Increasing_giv",
- System_Follows_allocGiv RS Follows_Increasing1);
-
-
-Goal "i: I \
-\ ==> rename sysOfClient (plam x: I. rename client_map Client) \
-\ : Increasing (giv o sub i o client) \
-\ guarantees \
-\ (INT h. {s. h <= (giv o sub i o client) s & \
-\ h pfixGe (ask o sub i o client) s} \
-\ LeadsTo {s. tokens h <= (tokens o rel o sub i o client) s})";
-by rename_client_map_tac;
-by (asm_simp_tac (simpset() addsimps [o_simp Client_Progress]) 1);
-qed "rename_Client_Progress";
-
-
-(*progress (2), step 7*)
-Goal
- "System : (INT i : (lessThan Nclients). \
-\ INT h. {s. h <= (giv o sub i o client) s & \
-\ h pfixGe (ask o sub i o client) s} \
-\ LeadsTo {s. tokens h <= (tokens o rel o sub i o client) s})";
-by (rtac INT_I 1);
-(*Couldn't have just used Auto_tac since the "INT h" must be kept*)
-by (rtac ([rename_Client_Progress,
- Client_component_System] MRS component_guaranteesD) 1);
-by (auto_tac (claset(), simpset() addsimps [System_Increasing_giv]));
-qed "System_Client_Progress";
-
-(*Concludes
- System : {s. k <= (sub i o allocGiv) s}
- LeadsTo
- {s. (sub i o allocAsk) s <= (ask o sub i o client) s} Int
- {s. k <= (giv o sub i o client) s} *)
-val lemma =
- [System_Follows_ask RS Follows_Bounded,
- System_Follows_allocGiv RS Follows_LeadsTo] MRS Always_LeadsToD;
-
-(*A more complicated variant of the previous one*)
-val lemma2 = [lemma,
- System_Follows_ask RS Follows_Increasing1 RS IncreasingD]
- MRS PSP_Stable;
-
-Goal "i < Nclients \
-\ ==> System : {s. h <= (sub i o allocGiv) s & \
-\ h pfixGe (sub i o allocAsk) s} \
-\ LeadsTo \
-\ {s. h <= (giv o sub i o client) s & \
-\ h pfixGe (ask o sub i o client) s}";
-by (rtac single_LeadsTo_I 1);
-by (res_inst_tac [("k6", "h"), ("x2", "(sub i o allocAsk) s")]
- (lemma2 RS LeadsTo_weaken) 1);
-by Auto_tac;
-by (blast_tac (claset() addIs [trans_Ge RS trans_genPrefix RS transD,
- prefix_imp_pfixGe]) 1);
-val lemma3 = result();
-
-
-(*progress (2), step 8: Client i's "release" action is visible system-wide*)
-Goal "i < Nclients \
-\ ==> System : {s. h <= (sub i o allocGiv) s & \
-\ h pfixGe (sub i o allocAsk) s} \
-\ LeadsTo {s. tokens h <= (tokens o sub i o allocRel) s}";
-by (rtac LeadsTo_Trans 1);
-by (dtac (System_Follows_rel RS impOfSubs (mono_tokens RS mono_Follows_o) RS
- Follows_LeadsTo) 2);
-by (asm_full_simp_tac (simpset() addsimps [o_assoc]) 2);
-by (rtac LeadsTo_Trans 1);
-by (cut_facts_tac [System_Client_Progress] 2);
-by (blast_tac (claset() addIs [LeadsTo_Basis]) 2);
-by (etac lemma3 1);
-qed "System_Alloc_Client_Progress";
-
-(*Lifting Alloc_Progress up to the level of systemState*)
-val rename_Alloc_Progress =
- Alloc_Progress RS rename_guarantees_sysOfAlloc_I
- |> simplify (simpset() addsimps [o_def]);
-
-(*progress (2), step 9*)
-Goal
- "System : (INT i : (lessThan Nclients). \
-\ INT h. {s. h <= (sub i o allocAsk) s} \
-\ LeadsTo {s. h pfixLe (sub i o allocGiv) s})";
-(*Can't use simpset(): the "INT h" must be kept*)
-by (simp_tac (HOL_ss addsimps [o_apply, sub_def]) 1);
-by (rtac (rename_Alloc_Progress RS component_guaranteesD) 1);
-by (auto_tac (claset(),
- simpset() addsimps [o_simp System_Increasing_allocRel,
- o_simp System_Increasing_allocAsk,
- o_simp System_Bounded_allocAsk,
- o_simp System_Alloc_Client_Progress]));
-qed "System_Alloc_Progress";
-
-
-(*progress (2), step 10 (final result!) *)
-Goalw [system_progress_def] "System : system_progress";
-by (cut_facts_tac [System_Alloc_Progress] 1);
-by (blast_tac (claset() addIs [LeadsTo_Trans,
- System_Follows_allocGiv RS Follows_LeadsTo_pfixLe,
- System_Follows_ask RS Follows_LeadsTo]) 1);
-qed "System_Progress";
-
-
-(*Ultimate goal*)
-Goalw [system_spec_def] "System : system_spec";
-by (blast_tac (claset() addIs [System_safety, System_Progress]) 1);
-qed "System_correct";
-
-
-(** SOME lemmas no longer used **)
-
-Goal "non_dummy = (% (g,a,r). (| giv = g, ask = a, rel = r |)) o \
-\ (funPair giv (funPair ask rel))";
-by (rtac ext 1);
-by (auto_tac (claset(), simpset() addsimps [o_def, non_dummy_def]));
-qed "non_dummy_eq_o_funPair";
-
-Goal "(preserves non_dummy) = \
-\ (preserves rel Int preserves ask Int preserves giv)";
-by (simp_tac (simpset() addsimps [non_dummy_eq_o_funPair]) 1);
-by Auto_tac;
-by (dres_inst_tac [("w1", "rel")] (impOfSubs subset_preserves_o) 1);
-by (dres_inst_tac [("w1", "ask")] (impOfSubs subset_preserves_o) 2);
-by (dres_inst_tac [("w1", "giv")] (impOfSubs subset_preserves_o) 3);
-by (auto_tac (claset(), simpset() addsimps [o_def]));
-qed "preserves_non_dummy_eq";
-
-(*Could go to Extend.ML*)
-Goal "bij f ==> fst (inv (%(x, u). inv f x) z) = f z";
-by (rtac fst_inv_equalityI 1);
-by (res_inst_tac [("f","%z. (f z, ?h z)")] surjI 1);
-by (asm_full_simp_tac (simpset() addsimps [bij_is_inj, inv_f_f]) 1);
-by (asm_full_simp_tac (simpset() addsimps [bij_is_surj, surj_f_inv_f]) 1);
-qed "bij_fst_inv_inv_eq";
-*)
--- 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 : <unfolded specification> *)
+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 : <unfolded specification> *)
+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 : <unfolded specification> *)
+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. (\<Sum>i: lessThan Nclients. (tokens o sub i o allocGiv) s)
+ <= NbT + (\<Sum>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<Nclients.
+ ALL elt : set ((sub i o allocAsk) s). elt <= NbT}"
+ apply (auto simp add: Collect_all_imp_eq)
+ apply (tactic {* rtac (Always_Int_rule [thm "Always_allocAsk_le_ask",
+ thm "System_Bounded_ask"] RS thm "Always_weaken") 1 *})
+ apply (auto dest: set_mono)
+ done
+
+(*progress (2), step 5 is System_Increasing_allocGiv*)
+
+(*progress (2), step 6*)
+(* i < Nclients ==> 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