--- a/src/HOL/UNITY/Alloc.ML Thu Dec 16 17:01:16 1999 +0100
+++ b/src/HOL/UNITY/Alloc.ML Fri Dec 17 10:30:48 1999 +0100
@@ -13,6 +13,8 @@
AddIs [impOfSubs subset_preserves_o];
Addsimps [funPair_o_distrib];
+Delsimps [o_apply];
+
(*Eliminating the "o" operator gives associativity for free*)
val o_simp = simplify (simpset() addsimps [o_def]);
@@ -35,6 +37,27 @@
handle THM _ => th RS (guarantees_INT_right_iff RS iffD1))
handle THM _ => th;
+(*Currently UNUSED, but possibly of interest*)
+Goal "F : Increasing func ==> F : Stable {s. h pfixGe (func s)}";
+by (asm_full_simp_tac
+ (simpset() addsimps [Increasing_def, Stable_def, Constrains_def,
+ constrains_def]) 1);
+by (blast_tac (claset() addIs [trans_Ge RS trans_genPrefix RS transD,
+ prefix_imp_pfixGe]) 1);
+qed "Increasing_imp_Stable_pfixGe";
+
+(*Currently UNUSED, but possibly of interest*)
+Goal "ALL z. F : {s. z <= f s} LeadsTo {s. z <= g s} \
+\ ==> F : {s. z pfixGe f s} LeadsTo {s. z pfixGe g s}";
+by (rtac single_LeadsTo_I 1);
+by (dres_inst_tac [("x", "f s")] spec 1);
+by (etac LeadsTo_weaken 1);
+by (blast_tac (claset() addIs [trans_Ge RS trans_genPrefix RS transD,
+ prefix_imp_pfixGe]) 2);
+by (Blast_tac 1);
+qed "LeadsTo_le_imp_pfixGe";
+
+
Goal "(ALL i: lessThan n. f i <= g i) --> sum f n <= sum g n";
by (induct_tac "n" 1);
by Auto_tac;
@@ -282,8 +305,7 @@
RS guaranteesD) 1);
by (rtac (lift_prog_guar_Increasing RS guarantees_PLam_I) 1);
by (auto_tac (claset(),
- simpset() delsimps [o_apply]
- addsimps [sub_fold, Network_preserves_rel_ask]));
+ simpset() addsimps [Network_preserves_rel_ask]));
qed "System_Increasing_ask";
Goalw [System_def]
@@ -293,13 +315,10 @@
by (rtac (lift_prog_guar_Increasing RS guarantees_PLam_I) 1);
(*gets Client_Increasing_rel from simpset*)
by (auto_tac (claset(),
- simpset() delsimps [o_apply]
- addsimps [sub_fold, Network_preserves_rel_ask]));
+ simpset() addsimps [Network_preserves_rel_ask]));
qed "System_Increasing_rel";
-
-(*Not sure what to say about the other components because they involve
- extend*)
+(** Components lemmas **)
(*Alternative is to say that System = Network Join F such that F preserves
certain state variables*)
@@ -323,28 +342,45 @@
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 [System_Increasing_rel,
+ 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 [System_Increasing_ask,
+ 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,
+ extend_Alloc_Increasing_allocGiv 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 (claset(),
- simpset() delsimps [o_apply] addsimps [Always_INT_distrib]));
-br Follows_Bounded 1;
-br (Network_Giv RS component_guaranteesD) 1;
-br (extend_Alloc_Increasing_allocGiv RS component_guaranteesD) 2;
-by Auto_tac;
+ simpset() addsimps [Always_INT_distrib]));
+by (etac (System_Follows_allocGiv RS Follows_Bounded) 1);
qed "Always_giv_le_allocGiv";
Goal "System : Always (INT i: lessThan Nclients. \
\ {s. (sub i o allocAsk) s <= (ask o sub i o client) s})";
-by (auto_tac (claset() addSIs [Follows_Bounded, System_Increasing_ask,
- Network_Ask RS component_guaranteesD],
- simpset() delsimps [o_apply] addsimps [Always_INT_distrib]));
+by (auto_tac (claset(),
+ simpset() addsimps [Always_INT_distrib]));
+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_Increasing_rel,
- Network_Rel RS component_guaranteesD],
- simpset() delsimps [o_apply] addsimps [Always_INT_distrib]));
+by (auto_tac (claset() addSIs [Follows_Bounded, System_Follows_rel],
+ simpset() addsimps [Always_INT_distrib]));
qed "Always_allocRel_le_rel";
@@ -354,9 +390,7 @@
(*safety (1), step 2*)
Goal "i < Nclients ==> System : Increasing (sub i o allocRel)";
-by (rtac Follows_Increasing1 1);
-by (blast_tac (claset() addIs [Network_Rel RS component_guaranteesD,
- System_Increasing_rel]) 1);
+by (etac (System_Follows_rel RS Follows_Increasing1) 1);
qed "System_Increasing_allocRel";
(*safety (1), step 3*)
@@ -386,14 +420,16 @@
\ {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()));
+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()));
+by (auto_tac (claset() addIs [tokens_mono_prefix],
+ simpset() addsimps [o_apply]));
qed "Always_tokens_allocRel_le_rel";
(*safety (1), step 4 (final result!) *)
@@ -444,7 +480,7 @@
guarantees_Join_I2 RS guaranteesD RS Always_weaken) 1);
by (rtac Client_i_Bounded 1);
by (auto_tac(claset(),
- simpset() addsimps [lift_export Collect_eq_extend_set RS sym,
+ simpset() addsimps [o_apply, lift_export Collect_eq_extend_set RS sym,
client_export Collect_eq_extend_set RS sym]));
qed "System_Bounded_ask";
@@ -509,7 +545,47 @@
by (rtac (client_export extending_LeadsETo RS extending_weaken RS
extending_INT) 1);
by (auto_tac (claset(),
- simpset() addsimps [client_export Collect_eq_extend_set RS sym]));
+ simpset() addsimps [o_apply, client_export Collect_eq_extend_set RS sym]));
qed "System_Client_Progress";
+val lemma =
+ [System_Follows_ask RS Follows_Bounded,
+ System_Follows_allocGiv RS Follows_LeadsTo] MRS Always_LeadsToD;
+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*)
+Goal
+ "System : (INT i : lessThan Nclients. \
+\ INT h. {s. h <= (sub i o allocGiv) s & \
+\ h pfixGe (sub i o allocAsk) s} \
+\ LeadsTo {s. tokens h <= (tokens o sub i o allocRel) s})";
+by Auto_tac;
+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 (rtac (impOfSubs LeadsETo_subset_LeadsTo) 2);
+by (cut_facts_tac [System_Client_Progress] 2);
+by (Force_tac 2);
+by (simp_tac (simpset() addsimps [Collect_conj_eq]) 1);
+by (etac lemma3 1);
+qed "System_Alloc_Progress";
--- a/src/HOL/UNITY/ELT.ML Thu Dec 16 17:01:16 1999 +0100
+++ b/src/HOL/UNITY/ELT.ML Fri Dec 17 10:30:48 1999 +0100
@@ -120,7 +120,6 @@
by (blast_tac (claset() addIs [leadsETo_Basis]) 1);
qed "leadsETo_mono";
-
val prems = Goalw [leadsETo_def]
"(!!A. A : S ==> F : (A Int C) leadsTo[CC] B) ==> F : (Union S Int C) leadsTo[CC] B";
by (simp_tac (HOL_ss addsimps [Int_Union_Union]) 1);
@@ -350,6 +349,58 @@
qed "Join_leadsETo_stable_imp_leadsETo";
+(**** Relationship with traditional "leadsTo", strong & weak ****)
+
+(** strong **)
+
+Goal "(A leadsTo[CC] B) <= (A leadsTo B)";
+by Safe_tac;
+by (etac leadsETo_induct 1);
+by (blast_tac (claset() addIs [leadsTo_Union]) 3);
+by (blast_tac (claset() addIs [leadsTo_Trans]) 2);
+by (blast_tac (claset() addIs [leadsTo_Basis]) 1);
+qed "leadsETo_subset_leadsTo";
+
+Goal "(A leadsTo[UNIV] B) = (A leadsTo B)";
+by Safe_tac;
+by (etac (impOfSubs leadsETo_subset_leadsTo) 1);
+(*right-to-left case*)
+by (etac leadsTo_induct 1);
+by (blast_tac (claset() addIs [leadsETo_Union]) 3);
+by (blast_tac (claset() addIs [leadsETo_Trans]) 2);
+by (blast_tac (claset() addIs [leadsETo_Basis]) 1);
+qed "leadsETo_UNIV_eq_leadsTo";
+
+(** weak **)
+
+Goalw [LeadsETo_def, LeadsTo_def] "(A LeadsTo[CC] B) <= (A LeadsTo B)";
+by (blast_tac (claset() addIs [impOfSubs leadsETo_subset_leadsTo]) 1);
+qed "LeadsETo_subset_LeadsTo";
+
+(*Postcondition can be strengthened to (reachable F Int B) *)
+Goal "F : A ensures B ==> F : (reachable F Int A) ensures B";
+by (rtac (stable_ensures_Int RS ensures_weaken_R) 1);
+by (auto_tac (claset(), simpset() addsimps [stable_reachable]));
+qed "reachable_ensures";
+
+Goal "F : A leadsTo B ==> F : (reachable F Int A) leadsTo[Pow(reachable F)] B";
+by (etac leadsTo_induct 1);
+by (stac Int_Union 3);
+by (blast_tac (claset() addIs [leadsETo_UN]) 3);
+by (blast_tac (claset() addDs [e_psp_stable2]
+ addIs [leadsETo_Trans, stable_reachable,
+ leadsETo_weaken_L]) 2);
+by (blast_tac (claset() addIs [reachable_ensures, leadsETo_Basis]) 1);
+val lemma = result();
+
+Goal "(A LeadsTo[UNIV] B) = (A LeadsTo B)";
+by Safe_tac;
+by (etac (impOfSubs LeadsETo_subset_LeadsTo) 1);
+(*right-to-left case*)
+by (rewrite_goals_tac [LeadsETo_def, LeadsTo_def]);
+by (fast_tac (claset() addEs [lemma RS leadsETo_weaken]) 1);
+qed "LeadsETo_UNIV_eq_LeadsTo";
+
(**** EXTEND/PROJECT PROPERTIES ****)
--- a/src/HOL/UNITY/GenPrefix.ML Thu Dec 16 17:01:16 1999 +0100
+++ b/src/HOL/UNITY/GenPrefix.ML Fri Dec 17 10:30:48 1999 +0100
@@ -343,3 +343,18 @@
qed "trans_Ge";
AddIffs [reflexive_Ge, antisym_Ge, trans_Ge];
+
+Goal "r<=s ==> genPrefix r <= genPrefix s";
+by (Clarify_tac 1);
+by (etac genPrefix.induct 1);
+by (auto_tac (claset() addIs [genPrefix.append], simpset()));
+qed "genPrefix_mono";
+
+Goalw [prefix_def, Le_def] "xs<=ys ==> xs pfixLe ys";
+by (blast_tac (claset() addIs [impOfSubs genPrefix_mono]) 1);
+qed "prefix_imp_pfixLe";
+
+Goalw [prefix_def, Ge_def] "xs<=ys ==> xs pfixGe ys";
+by (blast_tac (claset() addIs [impOfSubs genPrefix_mono]) 1);
+qed "prefix_imp_pfixGe";
+