# HG changeset patch # User paulson # Date 902220633 -7200 # Node ID bbcd79ef7cf25d167fe80ff630f881b45f349e54 # Parent 2fd94efb9d6462e997a6d07b08490c6ed6881723 Constant "invariant" and new constrains_tac, ensures_tac diff -r 2fd94efb9d64 -r bbcd79ef7cf2 src/HOL/UNITY/Common.ML --- 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"; diff -r 2fd94efb9d64 -r bbcd79ef7cf2 src/HOL/UNITY/Mutex.ML --- 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"; diff -r 2fd94efb9d64 -r bbcd79ef7cf2 src/HOL/UNITY/Mutex.thy --- 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 diff -r 2fd94efb9d64 -r bbcd79ef7cf2 src/HOL/UNITY/Reach.ML --- 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"; - diff -r 2fd94efb9d64 -r bbcd79ef7cf2 src/HOL/UNITY/Reach.thy --- 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}" diff -r 2fd94efb9d64 -r bbcd79ef7cf2 src/HOL/UNITY/SubstAx.ML --- 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]); + + diff -r 2fd94efb9d64 -r bbcd79ef7cf2 src/HOL/UNITY/Traces.ML --- 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); + + diff -r 2fd94efb9d64 -r bbcd79ef7cf2 src/HOL/UNITY/Traces.thy --- 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