--- a/src/HOL/UNITY/Alloc.ML Tue Nov 30 16:51:41 1999 +0100
+++ b/src/HOL/UNITY/Alloc.ML Tue Nov 30 16:54:10 1999 +0100
@@ -397,17 +397,21 @@
(*Lemma (?). A LOT of work just to lift "Client_Progress" to the array*)
Goal "lift_prog i Client \
-\ : Increasing (giv o sub i) Int (sub i LocalTo (lift_prog i Client)) \
-\ guarantees \
-\ (INT h. {s. h <= (giv o sub i) s & \
-\ h pfixGe (ask o sub i) s} \
-\ LeadsTo {s. tokens h <= (tokens o rel o sub i) s})";
+\ : Increasing (giv o sub i) Int \
+\ ((funPair rel ask o sub i) LocalTo (lift_prog i Client)) \
+\ guarantees \
+\ (INT h. {s. h <= (giv o sub i) s & \
+\ h pfixGe (ask o sub i) s} \
+\ LeadsTo[givenBy (funPair rel ask o sub i)] \
+\ {s. tokens h <= (tokens o rel o sub i) s})";
by (rtac (Client_Progress RS drop_prog_guarantees) 1);
-by (rtac (lift_export extending_LeadsTo RS extending_weaken RS
+by (rtac (lift_export extending_LeadsETo RS extending_weaken RS
extending_INT) 2);
by (rtac subset_refl 4);
-by (simp_tac (simpset()addsimps [lift_export Collect_eq_extend_set RS sym]) 3);
-by (force_tac (claset(), simpset() addsimps [sub_def, lift_prog_correct]) 2);
+by (simp_tac (simpset() addsimps [lift_export Collect_eq_extend_set RS sym,
+ sub_def]) 3);
+by (force_tac (claset(),
+ simpset() addsimps [sub_def, lift_prog_correct]) 2);
by (rtac (lift_export projecting_Increasing RS projecting_weaken) 1);
by (auto_tac (claset(), simpset() addsimps [o_def]));
qed "Client_i_Progress";
@@ -415,15 +419,123 @@
(*needed??*)
Goalw [PLam_def]
"(plam x:lessThan Nclients. Client) \
-\ : (INT i : lessThan Nclients. \
-\ Increasing (giv o sub i) Int (sub i LocalTo (lift_prog i Client))) \
-\ guarantees \
-\ (INT i : lessThan Nclients. \
-\ INT h. {s. h <= (giv o sub i) s & \
-\ h pfixGe (ask o sub i) s} \
-\ LeadsTo {s. tokens h <= (tokens o rel o sub i) s})";
-br guarantees_JN_INT 1;
-br Client_i_Progress 1;
+\ : (INT i : lessThan Nclients. \
+\ Increasing (giv o sub i) Int \
+\ ((funPair rel ask o sub i) LocalTo (lift_prog i Client))) \
+\ guarantees \
+\ (INT i : lessThan Nclients. \
+\ INT h. {s. h <= (giv o sub i) s & \
+\ h pfixGe (ask o sub i) s} \
+\ LeadsTo[givenBy (funPair rel ask o sub i)] \
+\ {s. tokens h <= (tokens o rel o sub i) s})";
+by (rtac guarantees_JN_INT 1);
+by (rtac Client_i_Progress 1);
qed "PLam_Client_Progress";
(*progress (2), step 7*)
+
+
+
+ [| ALL i:lessThan Nclients.
+ G : (sub i o client) LocalTo
+ extend sysOfClient (lift_prog i Client) |]
+ ==> G : client LocalTo
+ extend sysOfClient (plam i:lessThan Nclients. Client)
+
+
+
+
+ [| ALL i: I.
+ G : (sub i o client) LocalTo
+ extend sysOfClient (lift_prog i Client) |]
+ ==> G : client LocalTo
+ extend sysOfClient (plam x: I. Client)
+
+
+Goalw [LOCALTO_def, Diff_def, stable_def, constrains_def]
+ "[| ALL i. G : (sub i o v) localTo[C] F |] ==> G : v localTo[C] F";
+by Auto_tac;
+by (case_tac "Restrict C x: Restrict C `` Acts F" 1);
+by (blast_tac (claset() addSEs [equalityE]) 1);
+by (rtac ext 1);
+by (blast_tac (claset() addSDs [bspec]) 1);
+qed "all_sub_localTo";
+
+
+
+ G : (sub i o client) LocalTo extend sysOfClient (plam x: I. Client)
+
+
+xxxxxxxxxxxxxxxx;
+
+THIS PROOF requires an extra locality specification for Network:
+ Network : rel o sub i o client localTo[C]
+ extend sysOfClient (lift_prog i Client)
+and similarly for ask o sub i o client.
+
+
+
+Goalw [System_def]
+ "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[givenBy (funPair rel ask o sub i o client)] \
+\ {s. tokens h <= (tokens o rel o sub i o client) s})";
+by (rtac (guarantees_Join_I2 RS guaranteesD) 1);
+by (rtac (PLam_Client_Progress RS project_guarantees) 1);
+br extending_INT 2;
+by (rtac (client_export extending_LeadsETo RS extending_weaken RS extending_INT) 2);
+by (rtac subset_refl 4);
+by (simp_tac (simpset()addsimps [client_export Collect_eq_extend_set RS sym]) 3);
+by (fast_tac (claset() addIs [projecting_Int, projecting_INT,
+ client_export projecting_Increasing,
+ component_PLam,
+ client_export projecting_LocalTo]) 1);
+auto();
+
+be INT_lower 2;
+
+br projecting_INT 1;
+br projecting_Int 1;
+
+(*The next step goes wrong: it makes an impossible localTo subgoal*)
+(*blast_tac doesn't use HO unification*)
+by (fast_tac (claset() addIs [projecting_Int, projecting_INT,
+ client_export projecting_Increasing,
+ component_PLam,
+ client_export projecting_LocalTo]) 1);
+by (Clarify_tac 2);
+by (asm_simp_tac
+ (simpset() addsimps [rewrite_rule [System_def] System_Increasing_giv,
+ LocalTo_def, Join_localTo,
+ sysOfClient_in_client_localTo_xl_Client,
+ sysOfAlloc_in_client_localTo_xl_Client
+ RS localTo_imp_o_localTo,
+ self_localTo]) 2);
+by Auto_tac;
+
+
+
+OLD PROOF;
+by (rtac (guarantees_Join_I2 RS guaranteesD) 1);
+by (rtac (guarantees_PLam_I RS project_guarantees) 1);
+by (rtac Client_i_Progress 1);
+by (Force_tac 1);
+by (rtac (client_export extending_LeadsTo RS extending_weaken RS extending_INT) 2);
+by (rtac subset_refl 4);
+by (simp_tac (simpset()addsimps [client_export Collect_eq_extend_set RS sym]) 3);
+(*The next step goes wrong: it makes an impossible localTo subgoal*)
+(*blast_tac doesn't use HO unification*)
+by (fast_tac (claset() addIs [projecting_Int,
+ client_export projecting_Increasing,
+ component_PLam,
+ client_export projecting_LocalTo]) 1);
+by (asm_simp_tac
+ (simpset() addsimps [rewrite_rule [System_def] System_Increasing_giv,
+ LocalTo_def, Join_localTo,
+ sysOfClient_in_client_localTo_xl_Client,
+ sysOfAlloc_in_client_localTo_xl_Client]) 2);
+by Auto_tac;
+
+
+
--- a/src/HOL/UNITY/Alloc.thy Tue Nov 30 16:51:41 1999 +0100
+++ b/src/HOL/UNITY/Alloc.thy Tue Nov 30 16:54:10 1999 +0100
@@ -10,7 +10,7 @@
--but need invariants that values are non-negative
*)
-Alloc = Follows + Project + PPROD +
+Alloc = Follows + PPROD +
(*Duplicated from HOL/ex/NatSum.thy.
Maybe type should be [nat=>int, nat] => int**)
@@ -84,7 +84,7 @@
Increasing giv
guarantees
(INT h. {s. h <= giv s & h pfixGe ask s}
- LeadsTo
+ LeadsTo[givenBy (funPair rel ask)]
{s. tokens h <= (tokens o rel) s})"
client_spec :: clientState program set
--- a/src/HOL/UNITY/Client.ML Tue Nov 30 16:51:41 1999 +0100
+++ b/src/HOL/UNITY/Client.ML Tue Nov 30 16:54:10 1999 +0100
@@ -89,7 +89,7 @@
Goal "Cli_prg Join G \
\ : transient {s. size (giv s) = Suc k & \
\ size (rel s) = k & ask s ! k <= giv s ! k}";
-by (res_inst_tac [("act", "rel_act")] transient_mem 1);
+by (res_inst_tac [("act", "rel_act")] transientI 1);
by (auto_tac (claset(),
simpset() addsimps [Domain_def, Cli_prg_def]));
qed "transient_lemma";
--- a/src/HOL/UNITY/Extend.ML Tue Nov 30 16:51:41 1999 +0100
+++ b/src/HOL/UNITY/Extend.ML Tue Nov 30 16:54:10 1999 +0100
@@ -399,6 +399,11 @@
by (Force_tac 1);
qed "extend_constrains_project_set";
+Goal "extend h F : stable A ==> F : stable (project_set h A)";
+by (asm_full_simp_tac
+ (simpset() addsimps [stable_def, extend_constrains_project_set]) 1);
+qed "extend_stable_project_set";
+
(*** Diff, needed for localTo ***)
--- a/src/HOL/UNITY/Lift_prog.ML Tue Nov 30 16:51:41 1999 +0100
+++ b/src/HOL/UNITY/Lift_prog.ML Tue Nov 30 16:54:10 1999 +0100
@@ -49,7 +49,7 @@
Addsimps [Init_lift_prog];
Goalw [lift_prog_def] "Acts (lift_prog i F) = lift_act i `` Acts F";
-by (auto_tac (claset() addIs [Id_in_Acts RSN (2,image_eqI)], simpset()));
+by (auto_tac (claset() addIs [rev_image_eqI], simpset()));
qed "Acts_lift_prog";
Addsimps [Acts_lift_prog];
@@ -59,7 +59,7 @@
Addsimps [Init_drop_prog];
Goal "Acts (drop_prog i C F) = insert Id (drop_act i `` Restrict C `` Acts F)";
-by (auto_tac (claset() addIs [Id_in_Acts RSN (2,image_eqI)],
+by (auto_tac (claset() addIs [image_eqI],
simpset() addsimps [drop_prog_def]));
qed "Acts_drop_prog";
Addsimps [Acts_drop_prog];
@@ -391,6 +391,18 @@
(*** guarantees properties ***)
+(*The raw version*)
+val [xguary,drop_prog,lift_prog] =
+Goal "[| F : X guarantees Y; \
+\ !!G. lift_prog i F Join G : X' ==> F Join proj G i G : X; \
+\ !!G. [| F Join proj G i G : Y; lift_prog i F Join G : X' |] \
+\ ==> lift_prog i F Join G : Y' |] \
+\ ==> lift_prog i F : X' guarantees Y'";
+by (rtac (xguary RS guaranteesD RS lift_prog RS guaranteesI) 1);
+by (etac drop_prog 1);
+by (assume_tac 1);
+qed "drop_prog_guarantees_raw";
+
Goal "[| F : X guarantees Y; \
\ projecting C (lift_map i) F X' X; \
\ extending C (lift_map i) F X' Y' Y |] \
--- a/src/HOL/UNITY/Lift_prog.thy Tue Nov 30 16:51:41 1999 +0100
+++ b/src/HOL/UNITY/Lift_prog.thy Tue Nov 30 16:54:10 1999 +0100
@@ -6,7 +6,7 @@
lift_prog, etc: replication of components
*)
-Lift_prog = Project +
+Lift_prog = ELT +
constdefs
--- a/src/HOL/UNITY/Project.ML Tue Nov 30 16:51:41 1999 +0100
+++ b/src/HOL/UNITY/Project.ML Tue Nov 30 16:54:10 1999 +0100
@@ -12,7 +12,8 @@
(** projection: monotonicity for safety **)
-Goal "D <= C ==> project_act h (Restrict D act) <= project_act h (Restrict C act)";
+Goal "D <= C ==> \
+\ project_act h (Restrict D act) <= project_act h (Restrict C act)";
by (auto_tac (claset(), simpset() addsimps [project_act_def]));
qed "project_act_mono";
@@ -589,7 +590,7 @@
\ F Join project h C G : A ensures B |] \
\ ==> extend h F Join G : (C Int extend_set h A) ensures (extend_set h B)";
by (auto_tac (claset() addDs [extend_transient RS iffD2]
- addIs [transient_strengthen,
+ addIs [transient_strengthen, project_set_I,
project_unless RS unlessD, unlessI,
project_extend_constrains_I],
simpset() addsimps [ensures_def, Join_constrains,
@@ -608,7 +609,7 @@
by (etac leadsTo_induct 1);
by (asm_simp_tac (simpset() delsimps UN_simps
addsimps [Int_UN_distrib, leadsTo_UN, extend_set_Union]) 3);
-by (blast_tac (claset() addIs [psp_stable RS leadsTo_weaken,
+by (blast_tac (claset() addIs [psp_stable2 RS leadsTo_weaken_L,
leadsTo_Trans]) 2);
by (blast_tac (claset() addIs [leadsTo_Basis, Join_project_ensures]) 1);
val lemma = result();
@@ -673,7 +674,7 @@
by (rtac (xguary RS guaranteesD RS extend RS guaranteesI) 1);
by (etac project 1);
by (assume_tac 1);
-qed "project_guarantees_lemma";
+qed "project_guarantees_raw";
Goal "[| F : X guarantees Y; \
\ projecting C h F X' X; extending C h F X' Y' Y |] \
--- a/src/HOL/UNITY/SubstAx.ML Tue Nov 30 16:51:41 1999 +0100
+++ b/src/HOL/UNITY/SubstAx.ML Tue Nov 30 16:54:10 1999 +0100
@@ -424,7 +424,7 @@
ensuresI] 1),
(*now there are two subgoals: co & transient*)
simp_tac (simpset() addsimps !program_defs_ref) 2,
- res_inst_tac [("act", sact)] transient_mem 2,
+ res_inst_tac [("act", sact)] transientI 2,
(*simplify the command's domain*)
simp_tac (simpset() addsimps [Domain_def]) 3,
constrains_tac 1,
--- a/src/HOL/UNITY/SubstAx.thy Tue Nov 30 16:51:41 1999 +0100
+++ b/src/HOL/UNITY/SubstAx.thy Tue Nov 30 16:54:10 1999 +0100
@@ -8,10 +8,8 @@
SubstAx = WFair + Constrains +
-consts
- LeadsTo :: "['a set, 'a set] => 'a program set" (infixl 60)
+constdefs
+ LeadsTo :: "['a set, 'a set] => 'a program set" (infixl 60)
+ "A LeadsTo B == {F. F : (reachable F Int A) leadsTo B}"
-defs
- LeadsTo_def
- "A LeadsTo B == {F. F : (reachable F Int A) leadsTo B}"
end
--- a/src/HOL/UNITY/TimerArray.ML Tue Nov 30 16:51:41 1999 +0100
+++ b/src/HOL/UNITY/TimerArray.ML Tue Nov 30 16:54:10 1999 +0100
@@ -33,6 +33,6 @@
by (rtac PLam_leadsTo_Basis 1);
by (auto_tac (claset(), simpset() addsimps [lessThan_Suc RS sym]));
by (constrains_tac 1);
-by (res_inst_tac [("act", "decr")] transient_mem 1);
+by (res_inst_tac [("act", "decr")] transientI 1);
by (auto_tac (claset(), simpset() addsimps [Timer_def]));
qed "TimerArray_leadsTo_zero";
--- a/src/HOL/UNITY/Union.ML Tue Nov 30 16:51:41 1999 +0100
+++ b/src/HOL/UNITY/Union.ML Tue Nov 30 16:54:10 1999 +0100
@@ -338,6 +338,11 @@
by (Force_tac 1);
qed "localTo_imp_o_localTo";
+Goal "G : v LocalTo F ==> G : (f o v) LocalTo F";
+by (asm_full_simp_tac
+ (simpset() addsimps [LocalTo_def, localTo_imp_o_localTo]) 1);
+qed "LocalTo_imp_o_LocalTo";
+
(*NOT USED*)
Goalw [LOCALTO_def, stable_def, constrains_def]
"(%s. x) localTo[C] F = UNIV";
@@ -366,12 +371,17 @@
Join_left_absorb]) 1);
qed "self_Join_LocalTo";
+Goalw [LOCALTO_def]
+ "[| G : v localTo[C] F; F<=F' |] ==> G : v localTo[C] F'";
+by (Force_tac 1);
+qed "localTo_imp_o_localTo";
+
(*** Higher-level rules involving localTo and Join ***)
-Goal "[| F : {s. P (v s)} co {s. P' (v s)}; G : v localTo[C] F |] \
-\ ==> G : C Int {s. P (v s)} co {s. P' (v s)}";
+Goal "[| F : {s. P (v s)} co B; G : v localTo[C] F |] \
+\ ==> G : C Int {s. P (v s)} co B";
by (ftac constrains_imp_subset 1);
by (auto_tac (claset(),
simpset() addsimps [LOCALTO_def, stable_def, constrains_def,
@@ -392,12 +402,11 @@
by (Blast_tac 1);
qed "localTo_pairfun";
-Goal "[| F : {s. P (v s) (w s)} co {s. P' (v s) (w s)}; \
+Goal "[| F : {s. P (v s) (w s)} co B; \
\ G : v localTo[C] F; \
\ G : w localTo[C] F |] \
-\ ==> G : C Int {s. P (v s) (w s)} co {s. P' (v s) (w s)}";
-by (res_inst_tac [("A", "C Int {s. (%(x,y). P x y) (v s, w s)}"),
- ("A'", "{s. (%(x,y). P' x y) (v s, w s)}")]
+\ ==> G : C Int {s. P (v s) (w s)} co B";
+by (res_inst_tac [("A", "C Int {s. (%(x,y). P x y) (v s, w s)}")]
constrains_weaken 1);
by (rtac (localTo_pairfun RSN (2, constrains_localTo_constrains)) 1);
by Auto_tac;
--- a/src/HOL/UNITY/WFair.ML Tue Nov 30 16:51:41 1999 +0100
+++ b/src/HOL/UNITY/WFair.ML Tue Nov 30 16:54:10 1999 +0100
@@ -29,7 +29,16 @@
Goalw [transient_def]
"[| act: Acts F; A <= Domain act; act^^A <= -A |] ==> F : transient A";
by (Blast_tac 1);
-qed "transient_mem";
+qed "transientI";
+
+val major::prems =
+Goalw [transient_def]
+ "[| F : transient A; \
+\ !!act. [| act: Acts F; A <= Domain act; act^^A <= -A |] ==> P |] \
+\ ==> P";
+by (rtac (major RS CollectD RS bexE) 1);
+by (blast_tac (claset() addIs prems) 1);
+qed "transientE";
Goalw [transient_def] "transient UNIV = {}";
by Auto_tac;
@@ -53,27 +62,24 @@
by (Blast_tac 1);
qed "ensuresD";
-(*The L-version (precondition strengthening) doesn't hold for ENSURES*)
Goalw [ensures_def]
"[| F : A ensures A'; A'<=B' |] ==> F : A ensures B'";
by (blast_tac (claset() addIs [constrains_weaken, transient_strengthen]) 1);
qed "ensures_weaken_R";
-Goalw [ensures_def, constrains_def, transient_def]
- "F : A ensures UNIV";
-by Auto_tac;
-qed "ensures_UNIV";
-
+(*The L-version (precondition strengthening) fails, but we have this*)
Goalw [ensures_def]
- "[| F : stable C; \
-\ F : (C Int (A - A')) co (A Un A'); \
-\ F : transient (C Int (A-A')) |] \
-\ ==> F : (C Int A) ensures (C Int A')";
-by (asm_simp_tac (simpset() addsimps [Int_Un_distrib RS sym,
- Diff_Int_distrib RS sym,
- stable_constrains_Int]) 1);
+ "[| F : stable C; F : A ensures B |] \
+\ ==> F : (C Int A) ensures (C Int B)";
+by (auto_tac (claset(),
+ simpset() addsimps [ensures_def,
+ Int_Un_distrib RS sym,
+ Diff_Int_distrib RS sym]));
+by (blast_tac (claset() addIs [transient_strengthen]) 2);
+by (blast_tac (claset() addIs [stable_constrains_Int, constrains_weaken]) 1);
qed "stable_ensures_Int";
+(*NEVER USED*)
Goal "[| F : stable A; F : transient C; A <= B Un C |] ==> F : A ensures B";
by (asm_full_simp_tac (simpset() addsimps [ensures_def, stable_def]) 1);
by (blast_tac (claset() addIs [constrains_weaken, transient_strengthen]) 1);
@@ -96,11 +102,6 @@
(simpset() addsimps [leadsTo_Basis, ensuresI, Compl_partition]) 1);
qed "transient_imp_leadsTo";
-Goal "F : A leadsTo UNIV";
-by (blast_tac (claset() addIs [ensures_UNIV RS leadsTo_Basis]) 1);
-qed "leadsTo_UNIV";
-Addsimps [leadsTo_UNIV];
-
(*Useful with cancellation, disjunction*)
Goal "F : A leadsTo (A' Un A') ==> F : A leadsTo A'";
by (asm_full_simp_tac (simpset() addsimps Un_ac) 1);
@@ -164,6 +165,9 @@
bind_thm ("empty_leadsTo", empty_subsetI RS subset_imp_leadsTo);
Addsimps [empty_leadsTo];
+bind_thm ("leadsTo_UNIV", subset_UNIV RS subset_imp_leadsTo);
+Addsimps [leadsTo_UNIV];
+
Goal "[| F : A leadsTo A'; A'<=B' |] ==> F : A leadsTo B'";
by (blast_tac (claset() addIs [subset_imp_leadsTo, leadsTo_Trans]) 1);
@@ -210,22 +214,6 @@
addIs prems) 1);
qed "leadsTo_UN_UN";
-
-(*Version with no index set*)
-val prems = goal thy
- "(!! i. F : (A i) leadsTo (A' i)) \
-\ ==> F : (UN i. A i) leadsTo (UN i. A' i)";
-by (blast_tac (claset() addIs [leadsTo_UN_UN]
- addIs prems) 1);
-qed "leadsTo_UN_UN_noindex";
-
-(*Version with no index set*)
-Goal "ALL i. F : (A i) leadsTo (A' i) \
-\ ==> F : (UN i. A i) leadsTo (UN i. A' i)";
-by (blast_tac (claset() addIs [leadsTo_UN_UN]) 1);
-qed "all_leadsTo_UN_UN";
-
-
(*Binary union version*)
Goal "[| F : A leadsTo A'; F : B leadsTo B' |] \
\ ==> F : (A Un B) leadsTo (A' Un B')";