--- a/src/HOL/UNITY/Common.ML Tue Aug 04 10:50:04 1998 +0200
+++ b/src/HOL/UNITY/Common.ML Tue Aug 04 10:50:33 1998 +0200
@@ -28,8 +28,8 @@
qed "common_stable";
Goal "[| ALL m. constrains Acts {m} (maxfg m); n: common |] \
-\ ==> reachable ({0},Acts) <= atMost n";
-by (rtac strongest_invariant 1);
+\ ==> invariant ({0},Acts) (atMost n)";
+by (rtac invariantI 1);
by (asm_simp_tac (simpset() addsimps [common_stable]) 2);
by (simp_tac (simpset() addsimps [atMost_def]) 1);
qed "common_invariant";
--- a/src/HOL/UNITY/Mutex.ML Tue Aug 04 10:50:04 1998 +0200
+++ b/src/HOL/UNITY/Mutex.ML Tue Aug 04 10:50:33 1998 +0200
@@ -27,78 +27,34 @@
Addsimps update_defs;
-(** Constrains/Ensures tactics: NEED TO BE GENERALIZED OVER ALL PROGRAMS
- [They have free occurrences of mutex_def and cmd_defs] **)
-
-(*proves "constrains" properties when the program is specified*)
-val constrains_tac =
- SELECT_GOAL
- (EVERY [rtac constrainsI 1,
- rewtac mutex_def,
- REPEAT_FIRST (eresolve_tac [insertE, emptyE]),
- rewrite_goals_tac cmd_defs,
- ALLGOALS (SELECT_GOAL Auto_tac)]);
-
-
-(*proves "ensures" properties when the program is specified*)
-fun ensures_tac sact =
- SELECT_GOAL
- (EVERY [etac reachable_LeadsTo_Basis 1
- ORELSE (*subgoal may involve LeadsTo, leadsTo or ensures*)
- REPEAT (ares_tac [leadsTo_imp_LeadsTo, leadsTo_Basis,
- ensuresI] 1),
- res_inst_tac [("act", sact)] transient_mem 2,
- simp_tac (simpset() addsimps (Domain_partial_func::cmd_defs)) 3,
- simp_tac (simpset() addsimps [mutex_def]) 2,
- constrains_tac 1,
- rewrite_goals_tac cmd_defs,
- ALLGOALS Clarify_tac,
- Auto_tac]);
+Addsimps [invariantU_def, invariantV_def];
-Goalw [stable_def, invariantU_def] "stable mutex invariantU";
-by (constrains_tac 1);
-qed "stable_invariantU";
-
-Goalw [stable_def, invariantV_def] "stable mutex invariantV";
-by (constrains_tac 1);
-qed "stable_invariantV";
-
-Goalw [MInit_def, invariantU_def] "MInit <= invariantU";
+Goalw [MInit_def] "invariant (MInit,mutex) invariantU";
+by (rtac invariantI 1);
+by (constrains_tac cmd_defs 2);
by Auto_tac;
-qed "MInit_invariantU";
+qed "invariantU";
-Goalw [MInit_def, invariantV_def] "MInit <= invariantV";
+Goalw [MInit_def] "invariant (MInit,mutex) invariantV";
+by (rtac invariantI 1);
+by (constrains_tac cmd_defs 2);
by Auto_tac;
-qed "MInit_invariantV";
+qed "invariantV";
-(*The intersection is an invariant of the system*)
-Goal "reachable (MInit,mutex) <= invariantU Int invariantV";
-by (simp_tac (simpset() addsimps
- [strongest_invariant, Int_greatest, stable_Int,
- stable_invariantU, stable_invariantV,
- MInit_invariantU,MInit_invariantV]) 1);
-qed "reachable_subset_invariant";
-
-val reachable_subset_invariant' =
- rewrite_rule [invariantU_def, invariantV_def] reachable_subset_invariant;
+val mutex_invariant = invariant_Int_rule [invariantU, invariantV];
-(*The safety property (mutual exclusion) follows from the claimed invar_s*)
-Goalw [invariantU_def, invariantV_def]
- "{s. MM s = 3 & NN s = 3} <= Compl (invariantU Int invariantV)";
+(*The safety property: mutual exclusion*)
+Goal "disjoint (reachable (MInit,mutex)) {s. MM s = 3 & NN s = 3}";
+by (cut_facts_tac [mutex_invariant RS invariant_includes_reachable] 1);
by Auto_tac;
-val lemma = result();
-
-Goal "{s. MM s = 3 & NN s = 3} <= Compl (reachable (MInit,mutex))";
-by (rtac ([lemma, reachable_subset_invariant RS Compl_anti_mono]
- MRS subset_trans) 1);
qed "mutual_exclusion";
(*The bad invariant FAILS in cmd1V*)
-Goalw [stable_def, bad_invariantU_def] "stable mutex bad_invariantU";
-by (constrains_tac 1);
+Goalw [bad_invariantU_def] "stable mutex bad_invariantU";
+by (constrains_tac cmd_defs 1);
by (REPEAT (trans_tac 1));
by (safe_tac (claset() addSEs [le_SucE]));
by (Asm_full_simp_tac 1);
@@ -112,23 +68,23 @@
(*** Progress for U ***)
Goalw [unless_def] "unless mutex {s. MM s=2} {s. MM s=3}";
-by (constrains_tac 1);
+by (constrains_tac cmd_defs 1);
qed "U_F0";
Goal "LeadsTo(MInit,mutex) {s. MM s=1} {s. PP s = VV s & MM s = 2}";
-by (ensures_tac "cmd1U" 1);
+by (ensures_tac cmd_defs "cmd1U" 1);
qed "U_F1";
Goal "LeadsTo(MInit,mutex) {s. ~ PP s & MM s = 2} {s. MM s = 3}";
-by (cut_facts_tac [reachable_subset_invariant'] 1);
-by (ensures_tac "cmd2U" 1);
+by (cut_facts_tac [mutex_invariant] 1);
+by (ensures_tac cmd_defs "cmd2U" 1);
qed "U_F2";
Goalw [mutex_def] "LeadsTo(MInit,mutex) {s. MM s = 3} {s. PP s}";
by (rtac leadsTo_imp_LeadsTo 1);
by (res_inst_tac [("B", "{s. MM s = 4}")] leadsTo_Trans 1);
-by (ensures_tac "cmd4U" 2);
-by (ensures_tac "cmd3U" 1);
+by (ensures_tac cmd_defs "cmd4U" 2);
+by (ensures_tac cmd_defs "cmd3U" 1);
qed "U_F3";
Goal "LeadsTo(MInit,mutex) {s. MM s = 2} {s. PP s}";
@@ -136,27 +92,25 @@
MRS LeadsTo_Diff) 1);
by (rtac ([U_F2, U_F3] MRS LeadsTo_Trans) 1);
by (auto_tac (claset() addSEs [less_SucE], simpset()));
-val lemma2 = result();
+val U_lemma2 = result();
Goal "LeadsTo(MInit,mutex) {s. MM s = 1} {s. PP s}";
-by (rtac ([U_F1 RS LeadsTo_weaken_R, lemma2] MRS LeadsTo_Trans) 1);
+by (rtac ([U_F1 RS LeadsTo_weaken_R, U_lemma2] MRS LeadsTo_Trans) 1);
by (Blast_tac 1);
-val lemma1 = result();
+val U_lemma1 = result();
Goal "LeadsTo(MInit,mutex) {s. 1 <= MM s & MM s <= 3} {s. PP s}";
by (simp_tac (simpset() addsimps [le_Suc_eq, conj_disj_distribL]
addcongs [rev_conj_cong]) 1);
by (simp_tac (simpset() addsimps [Collect_disj_eq, LeadsTo_Un_distrib,
- lemma1, lemma2, U_F3] ) 1);
-val lemma123 = result();
+ U_lemma1, U_lemma2, U_F3] ) 1);
+val U_lemma123 = result();
(*Misra's F4*)
Goal "LeadsTo(MInit,mutex) {s. UU s} {s. PP s}";
-by (rtac LeadsTo_weaken_L 1);
-by (rtac lemma123 1);
-by (cut_facts_tac [reachable_subset_invariant'] 1);
+by (rtac ([invariantU, U_lemma123] MRS invariant_LeadsTo_weaken) 1);
by Auto_tac;
qed "u_leadsto_p";
@@ -165,23 +119,23 @@
Goalw [unless_def] "unless mutex {s. NN s=2} {s. NN s=3}";
-by (constrains_tac 1);
+by (constrains_tac cmd_defs 1);
qed "V_F0";
Goal "LeadsTo(MInit,mutex) {s. NN s=1} {s. PP s = (~ UU s) & NN s = 2}";
-by (ensures_tac "cmd1V" 1);
+by (ensures_tac cmd_defs "cmd1V" 1);
qed "V_F1";
Goal "LeadsTo(MInit,mutex) {s. PP s & NN s = 2} {s. NN s = 3}";
-by (cut_facts_tac [reachable_subset_invariant'] 1);
-by (ensures_tac "cmd2V" 1);
+by (cut_facts_tac [mutex_invariant] 1);
+by (ensures_tac cmd_defs "cmd2V" 1);
qed "V_F2";
Goalw [mutex_def] "LeadsTo(MInit,mutex) {s. NN s = 3} {s. ~ PP s}";
by (rtac leadsTo_imp_LeadsTo 1);
by (res_inst_tac [("B", "{s. NN s = 4}")] leadsTo_Trans 1);
-by (ensures_tac "cmd4V" 2);
-by (ensures_tac "cmd3V" 1);
+by (ensures_tac cmd_defs "cmd4V" 2);
+by (ensures_tac cmd_defs "cmd3V" 1);
qed "V_F3";
Goal "LeadsTo(MInit,mutex) {s. NN s = 2} {s. ~ PP s}";
@@ -189,27 +143,24 @@
MRS LeadsTo_Diff) 1);
by (rtac ([V_F2, V_F3] MRS LeadsTo_Trans) 1);
by (auto_tac (claset() addSEs [less_SucE], simpset()));
-val lemma2 = result();
+val V_lemma2 = result();
Goal "LeadsTo(MInit,mutex) {s. NN s = 1} {s. ~ PP s}";
-by (rtac ([V_F1 RS LeadsTo_weaken_R, lemma2] MRS LeadsTo_Trans) 1);
+by (rtac ([V_F1 RS LeadsTo_weaken_R, V_lemma2] MRS LeadsTo_Trans) 1);
by (Blast_tac 1);
-val lemma1 = result();
-
+val V_lemma1 = result();
Goal "LeadsTo(MInit,mutex) {s. 1 <= NN s & NN s <= 3} {s. ~ PP s}";
by (simp_tac (simpset() addsimps [le_Suc_eq, conj_disj_distribL]
addcongs [rev_conj_cong]) 1);
by (simp_tac (simpset() addsimps [Collect_disj_eq, LeadsTo_Un_distrib,
- lemma1, lemma2, V_F3] ) 1);
-val lemma123 = result();
+ V_lemma1, V_lemma2, V_F3] ) 1);
+val V_lemma123 = result();
(*Misra's F4*)
Goal "LeadsTo(MInit,mutex) {s. VV s} {s. ~ PP s}";
-by (rtac LeadsTo_weaken_L 1);
-by (rtac lemma123 1);
-by (cut_facts_tac [reachable_subset_invariant'] 1);
+by (rtac ([invariantV, V_lemma123] MRS invariant_LeadsTo_weaken) 1);
by Auto_tac;
qed "v_leadsto_not_p";
--- a/src/HOL/UNITY/Mutex.thy Tue Aug 04 10:50:04 1998 +0200
+++ b/src/HOL/UNITY/Mutex.thy Tue Aug 04 10:50:33 1998 +0200
@@ -6,7 +6,7 @@
Based on "A Family of 2-Process Mutual Exclusion Algorithms" by J Misra
*)
-Mutex = UNITY + Traces + SubstAx +
+Mutex = SubstAx +
(*WE NEED A GENERAL TREATMENT OF NUMBERS!!*)
syntax
--- a/src/HOL/UNITY/Reach.ML Tue Aug 04 10:50:04 1998 +0200
+++ b/src/HOL/UNITY/Reach.ML Tue Aug 04 10:50:33 1998 +0200
@@ -29,54 +29,21 @@
(*All vertex sets are finite*)
AddIffs [[subset_UNIV, finite_graph] MRS finite_subset];
-
-(** Constrains/Ensures tactics: NEED TO BE GENERALIZED OVER ALL PROGRAMS **)
-
-(*proves "constrains" properties when the program is specified*)
-val constrains_tac =
- SELECT_GOAL
- (EVERY [rtac constrainsI 1,
- rewtac racts_def,
- REPEAT_FIRST (eresolve_tac [insertE, emptyE]),
- rewrite_goals_tac [racts_def, asgt_def],
- ALLGOALS (SELECT_GOAL Auto_tac)]);
-
+Addsimps [reach_invariant_def];
-(*proves "ensures" properties when the program is specified*)
-fun ensures_tac sact =
- SELECT_GOAL
- (EVERY [REPEAT (resolve_tac [LeadsTo_Basis, leadsTo_Basis, ensuresI] 1),
- res_inst_tac [("act", sact)] transient_mem 2,
- Simp_tac 2,
- constrains_tac 1,
- rewrite_goals_tac [racts_def, asgt_def],
- Auto_tac]);
-
-
-Goalw [stable_def, invariant_def]
- "stable racts invariant";
-by (constrains_tac 1);
+Goalw [rinit_def] "invariant (rinit,racts) reach_invariant";
+by (rtac invariantI 1);
+by Auto_tac; (*for the initial state; proof of stability remains*)
+by (constrains_tac [racts_def, asgt_def] 1);
by (blast_tac (claset() addIs [r_into_rtrancl,rtrancl_trans]) 1);
-qed "stable_invariant";
-
-Goalw [rinit_def, invariant_def] "rinit <= invariant";
-by Auto_tac;
-qed "rinit_invariant";
-
-Goal "reachable (rinit,racts) <= invariant";
-by (simp_tac (simpset() addsimps
- [strongest_invariant, stable_invariant, rinit_invariant]) 1);
-qed "reachable_subset_invariant";
-
-val reachable_subset_invariant' =
- rewrite_rule [invariant_def] reachable_subset_invariant;
+qed "reach_invariant";
(*** Fixedpoint ***)
(*If it reaches a fixedpoint, it has found a solution*)
-Goalw [fixedpoint_def, invariant_def]
- "fixedpoint Int invariant = { %v. (init, v) : edges^* }";
+Goalw [fixedpoint_def, reach_invariant_def]
+ "fixedpoint Int reach_invariant = { %v. (init, v) : edges^* }";
by (rtac equalityI 1);
by (blast_tac (claset() addIs [r_into_rtrancl,rtrancl_trans]) 2);
by (auto_tac (claset() addSIs [ext], simpset()));
@@ -153,7 +120,7 @@
Goal "(u,v): edges ==> \
\ ensures racts ((metric-``{m}) Int {s. s u & ~ s v}) \
\ (metric-``(lessThan m))";
-by (ensures_tac "asgt u v" 1);
+by (ensures_tac [racts_def, asgt_def] "asgt u v" 1);
by (cut_facts_tac [metric_le] 1);
by (fast_tac (claset() addSDs [le_imp_less_or_eq]) 1);
qed "edges_ensures";
@@ -180,8 +147,8 @@
Goal "LeadsTo(rinit,racts) UNIV { %v. (init, v) : edges^* }";
by (stac (fixedpoint_invariant_correct RS sym) 1);
-by (rtac (leadsTo_fixedpoint RS leadsTo_imp_LeadsTo RS LeadsTo_weaken_R) 1);
-by (cut_facts_tac [reachable_subset_invariant] 1);
-by (Blast_tac 1);
+by (rtac ([reach_invariant,
+ leadsTo_fixedpoint RS leadsTo_imp_LeadsTo]
+ MRS invariant_LeadsTo_weaken) 1);
+by Auto_tac;
qed "LeadsTo_correct";
-
--- a/src/HOL/UNITY/Reach.thy Tue Aug 04 10:50:04 1998 +0200
+++ b/src/HOL/UNITY/Reach.thy Tue Aug 04 10:50:33 1998 +0200
@@ -29,8 +29,8 @@
rinit :: "state set"
"rinit == {%v. v=init}"
- invariant :: state set
- "invariant == {s. (ALL v. s v --> (init, v) : edges^*) & s init}"
+ reach_invariant :: state set
+ "reach_invariant == {s. (ALL v. s v --> (init, v) : edges^*) & s init}"
fixedpoint :: state set
"fixedpoint == {s. ALL (u,v): edges. s u --> s v}"
--- a/src/HOL/UNITY/SubstAx.ML Tue Aug 04 10:50:04 1998 +0200
+++ b/src/HOL/UNITY/SubstAx.ML Tue Aug 04 10:50:33 1998 +0200
@@ -392,16 +392,59 @@
by (Blast_tac 1);
qed "reachable_transient";
-(*Eliminates the set "reachable (Init,Acts)" from the subgoals. This boosts
- efficiency because the term contains a full copy of the program.*)
-Goal "[| reachable (Init,Acts) <= INV; \
+(*Uses the premise "invariant (Init,Acts)". Raw theorem-proving on this
+ inclusion is slow: the term contains a copy of the program.*)
+Goal "[| invariant (Init,Acts) INV; \
\ constrains Acts (INV Int (A - A')) (A Un A'); \
\ transient Acts (INV Int (A-A')) |] \
\ ==> LeadsTo(Init,Acts) A A'";
+bd invariant_includes_reachable 1;
by (rtac LeadsTo_Basis 1);
by (blast_tac (claset() addSIs [reachable_transient]) 2);
by (rewtac constrains_def);
by (Blast_tac 1);
-qed "reachable_LeadsTo_Basis";
+qed "invariant_LeadsTo_Basis";
+
+
+Goal "[| invariant (Init,Acts) INV; \
+\ LeadsTo(Init,Acts) A A'; id: Acts; \
+\ INV Int B <= A; INV Int A' <= B' |] \
+\ ==> LeadsTo(Init,Acts) B B'";
+by (blast_tac (claset() addDs [invariant_includes_reachable]
+ addIs [LeadsTo_weaken]) 1);
+qed "invariant_LeadsTo_weaken";
+(** Constrains/Ensures tactics
+ main_def defines the main program as a set;
+ cmd_defs defines the separate commands
+**)
+
+(*proves "constrains" properties when the program is specified*)
+fun constrains_tac (main_def::cmd_defs) =
+ SELECT_GOAL
+ (EVERY [TRY (rtac stableI 1),
+ rtac constrainsI 1,
+ rewtac main_def,
+ REPEAT_FIRST (eresolve_tac [insertE, emptyE]),
+ rewrite_goals_tac cmd_defs,
+ ALLGOALS (SELECT_GOAL Auto_tac)]);
+
+
+(*proves "ensures" properties when the program is specified*)
+fun ensures_tac (main_def::cmd_defs) sact =
+ SELECT_GOAL
+ (EVERY [REPEAT (invariant_Int_tac 1),
+ etac invariant_LeadsTo_Basis 1
+ ORELSE (*subgoal may involve LeadsTo, leadsTo or ensures*)
+ REPEAT (ares_tac [leadsTo_imp_LeadsTo, leadsTo_Basis,
+ ensuresI] 1),
+ res_inst_tac [("act", sact)] transient_mem 2,
+ simp_tac (simpset() addsimps (Domain_partial_func::cmd_defs)) 3,
+ simp_tac (simpset() addsimps [main_def]) 2,
+ constrains_tac (main_def::cmd_defs) 1,
+ rewrite_goals_tac cmd_defs,
+ ALLGOALS Clarify_tac,
+ Auto_tac]);
+
+
--- a/src/HOL/UNITY/Traces.ML Tue Aug 04 10:50:04 1998 +0200
+++ b/src/HOL/UNITY/Traces.ML Tue Aug 04 10:50:33 1998 +0200
@@ -64,15 +64,53 @@
end;
-(*The strongest invariant is the set of all reachable states!*)
-Goalw [stable_def, constrains_def]
- "[| Init<=A; stable Acts A |] ==> reachable(Init,Acts) <= A";
+
+Goal "stable Acts (reachable(Init,Acts))";
+by (blast_tac (claset() addIs ([stableI, constrainsI] @ reachable.intrs)) 1);
+qed "stable_reachable";
+
+(*The set of all reachable states is an invariant...*)
+Goal "invariant (Init,Acts) (reachable(Init,Acts))";
+by (simp_tac (simpset() addsimps [invariant_def]) 1);
+by (blast_tac (claset() addIs (stable_reachable::reachable.intrs)) 1);
+qed "invariant_reachable";
+
+(*...in fact the strongest invariant!*)
+Goal "invariant (Init,Acts) A ==> reachable(Init,Acts) <= A";
+by (full_simp_tac
+ (simpset() addsimps [stable_def, constrains_def, invariant_def]) 1);
by (rtac subsetI 1);
by (etac reachable.induct 1);
by (REPEAT (blast_tac (claset() addIs reachable.intrs) 1));
-qed "strongest_invariant";
+qed "invariant_includes_reachable";
+
+(*If "A" includes the initial states and is stable then "A" is invariant.
+ Result is trivial from the definition, but it is handy.*)
+Goal "[| Init<=A; stable Acts A |] ==> invariant (Init,Acts) A";
+by (asm_simp_tac (simpset() addsimps [invariant_def]) 1);
+qed "invariantI";
+
+
+(** Conjoining invariants **)
-Goal "stable Acts (reachable(Init,Acts))";
-by (REPEAT (blast_tac (claset() addIs [stableI, constrainsI]
- addIs reachable.intrs) 1));
-qed "stable_reachable";
+Goal "[| invariant (Init,Acts) A; invariant (Init,Acts) B |] \
+\ ==> invariant (Init,Acts) (A Int B)";
+by (asm_full_simp_tac (simpset() addsimps [invariant_def, stable_Int]) 1);
+by Auto_tac;
+qed "invariant_Int";
+
+(*Delete the nearest invariance assumption (which will be the second one
+ used by invariant_Int) *)
+val invariant_thin =
+ read_instantiate_sg (sign_of thy)
+ [("V", "invariant ?Prg ?A")] thin_rl;
+
+(*Combines two invariance ASSUMPTIONS into one. USEFUL??*)
+val invariant_Int_tac = dtac invariant_Int THEN'
+ assume_tac THEN'
+ etac invariant_thin;
+
+(*Combines two invariance THEOREMS into one.*)
+val invariant_Int_rule = foldr1 (fn (th1,th2) => [th1,th2] MRS invariant_Int);
+
+
--- a/src/HOL/UNITY/Traces.thy Tue Aug 04 10:50:04 1998 +0200
+++ b/src/HOL/UNITY/Traces.thy Tue Aug 04 10:50:33 1998 +0200
@@ -24,7 +24,11 @@
==> (s', s#evs) : traces Init Acts"
-constdefs reachable :: "'a set * ('a * 'a)set set => 'a set"
+constdefs
+ reachable :: "'a set * ('a * 'a)set set => 'a set"
"reachable == %(Init,Acts). {s. EX evs. (s,evs): traces Init Acts}"
+ invariant :: "['a set * ('a * 'a)set set, 'a set] => bool"
+ "invariant == %(Init,Acts) A. Init <= A & stable Acts A"
+
end