--- a/src/HOL/UNITY/Client.ML Mon May 03 19:03:35 1999 +0200
+++ b/src/HOL/UNITY/Client.ML Tue May 04 10:26:00 1999 +0200
@@ -79,9 +79,9 @@
(*Safety property 2: clients return the right number of tokens*)
Goal "Cli_prg : (Increasing giv Int (rel localTo Cli_prg)) \
-\ guarantees Invariant {s. rel s <= giv s}";
+\ guarantees Always {s. rel s <= giv s}";
by (rtac guaranteesI 1);
-by (rtac InvariantI 1);
+by (rtac AlwaysI 1);
by (Force_tac 1);
by (blast_tac (claset() addIs [Increasing_localTo_Stable,
stable_rel_le_giv]) 1);
@@ -104,12 +104,12 @@
Goal "Cli_prg : \
\ (Increasing giv Int (rel localTo Cli_prg) Int (ask localTo Cli_prg)) \
-\ guarantees Invariant ({s. size (ask s) <= Suc (size (rel s))} Int \
+\ guarantees Always ({s. size (ask s) <= Suc (size (rel s))} Int \
\ {s. size (rel s) <= size (giv s)})";
by (rtac guaranteesI 1);
by (Clarify_tac 1);
by (dtac (impOfSubs (rewrite_o Increasing_size)) 1);
-by (rtac InvariantI 1);
+by (rtac AlwaysI 1);
by (Force_tac 1);
by (rtac Stable_Int 1);
by (fast_tac (claset() addEs [impOfSubs (rewrite_o localTo_imp_o_localTo)]
@@ -123,18 +123,18 @@
Goal "Cli_prg : \
\ (Increasing giv Int (rel localTo Cli_prg) Int (ask localTo Cli_prg) \
-\ Int Invariant giv_meets_ask) \
+\ Int Always giv_meets_ask) \
\ guarantees ({s. k < size (giv s)} LeadsTo {s. k < size (rel s)})";
by (rtac guaranteesI 1);
by (Clarify_tac 1);
-by (rtac Stable_transient_reachable_LeadsTo 1);
+by (rtac Stable_transient_Always_LeadsTo 1);
by (res_inst_tac [("k", "k")] transient_lemma 2);
by (force_tac (claset() addDs [impOfSubs Increasing_size,
impOfSubs Increasing_Stable_less],
simpset()) 1);
by (rtac (make_elim (lemma1 RS guaranteesD)) 1);
- by (Blast_tac 1);
-by (auto_tac (claset(),
- simpset() addsimps [Invariant_eq_always, giv_meets_ask_def]));
+by (Blast_tac 1);
+by (auto_tac (claset(),
+ simpset() addsimps [Always_eq_includes_reachable, giv_meets_ask_def]));
by (ALLGOALS Force_tac);
qed "client_correct";
--- a/src/HOL/UNITY/Common.ML Mon May 03 19:03:35 1999 +0200
+++ b/src/HOL/UNITY/Common.ML Tue May 04 10:26:00 1999 +0200
@@ -23,9 +23,9 @@
Goal "[| Init F <= atMost n; \
\ ALL m. F : {m} Co (maxfg m); n: common |] \
-\ ==> F : Invariant (atMost n)";
-by (asm_simp_tac (simpset() addsimps [InvariantI, common_stable]) 1);
-qed "common_Invariant";
+\ ==> F : Always (atMost n)";
+by (asm_simp_tac (simpset() addsimps [AlwaysI, common_stable]) 1);
+qed "common_safety";
(*** Some programs that implement the safety property above ***)
--- a/src/HOL/UNITY/Constrains.ML Mon May 03 19:03:35 1999 +0200
+++ b/src/HOL/UNITY/Constrains.ML Tue May 04 10:26:00 1999 +0200
@@ -234,100 +234,102 @@
qed "Elimination_sing";
-(*** Specialized laws for handling Invariants ***)
+(*** Specialized laws for handling Always ***)
-(** Natural deduction rules for "Invariant F A" **)
+(** Natural deduction rules for "Always A" **)
-Goal "[| Init F<=A; F : Stable A |] ==> F : Invariant A";
-by (asm_simp_tac (simpset() addsimps [Invariant_def]) 1);
-qed "InvariantI";
+Goal "[| Init F<=A; F : Stable A |] ==> F : Always A";
+by (asm_simp_tac (simpset() addsimps [Always_def]) 1);
+qed "AlwaysI";
-Goal "F : Invariant A ==> Init F<=A & F : Stable A";
-by (asm_full_simp_tac (simpset() addsimps [Invariant_def]) 1);
-qed "InvariantD";
+Goal "F : Always A ==> Init F<=A & F : Stable A";
+by (asm_full_simp_tac (simpset() addsimps [Always_def]) 1);
+qed "AlwaysD";
-bind_thm ("InvariantE", InvariantD RS conjE);
+bind_thm ("AlwaysE", AlwaysD RS conjE);
-(*The set of all reachable states is the strongest Invariant*)
-Goal "F : Invariant A ==> reachable F <= A";
+(*The set of all reachable states is Always*)
+Goal "F : Always A ==> reachable F <= A";
by (full_simp_tac
(simpset() addsimps [Stable_def, Constrains_def, constrains_def,
- Invariant_def]) 1);
+ Always_def]) 1);
by (rtac subsetI 1);
by (etac reachable.induct 1);
by (REPEAT (blast_tac (claset() addIs reachable.intrs) 1));
-qed "Invariant_includes_reachable";
+qed "Always_includes_reachable";
-Goalw [Invariant_def, invariant_def, Stable_def, Constrains_def, stable_def]
- "F : invariant A ==> F : Invariant A";
+Goalw [Always_def, invariant_def, Stable_def, Constrains_def, stable_def]
+ "F : invariant A ==> F : Always A";
by (blast_tac (claset() addIs [constrains_reachable_Int]) 1);
-qed "invariant_imp_Invariant";
+qed "invariant_imp_Always";
-Goalw [Invariant_def, invariant_def, Stable_def, Constrains_def, stable_def]
- "Invariant A = {F. F : invariant (reachable F Int A)}";
+Goalw [Always_def, invariant_def, Stable_def, Constrains_def, stable_def]
+ "Always A = {F. F : invariant (reachable F Int A)}";
by (blast_tac (claset() addIs reachable.intrs) 1);
-qed "Invariant_eq_invariant_reachable";
+qed "Always_eq_invariant_reachable";
-(*Invariant is the "always" notion*)
-Goal "Invariant A = {F. reachable F <= A}";
+(*the RHS is the traditional definition of the "always" operator*)
+Goal "Always A = {F. reachable F <= A}";
by (auto_tac (claset() addDs [invariant_includes_reachable],
simpset() addsimps [Int_absorb2, invariant_reachable,
- Invariant_eq_invariant_reachable]));
-qed "Invariant_eq_always";
+ Always_eq_invariant_reachable]));
+qed "Always_eq_includes_reachable";
-Goal "Invariant A = (UN I: Pow A. invariant I)";
-by (simp_tac (simpset() addsimps [Invariant_eq_always]) 1);
+Goal "Always A = (UN I: Pow A. invariant I)";
+by (simp_tac (simpset() addsimps [Always_eq_includes_reachable]) 1);
by (blast_tac (claset() addIs [invariantI, impOfSubs Init_subset_reachable,
stable_reachable,
impOfSubs invariant_includes_reachable]) 1);
-qed "Invariant_eq_UN_invariant";
+qed "Always_eq_UN_invariant";
+
+Goal "[| F : Always A; A <= B |] ==> F : Always B";
+by (auto_tac (claset(), simpset() addsimps [Always_eq_includes_reachable]));
+qed "Always_weaken";
-(*** "Co" rules involving Invariant ***)
+(*** "Co" rules involving Always ***)
-Goal "[| F : Invariant INV; F : (INV Int A) Co A' |] \
+Goal "[| F : Always INV; F : (INV Int A) Co A' |] \
\ ==> F : A Co A'";
by (asm_full_simp_tac
- (simpset() addsimps [Invariant_includes_reachable RS Int_absorb2,
+ (simpset() addsimps [Always_includes_reachable RS Int_absorb2,
Constrains_def, Int_assoc RS sym]) 1);
-qed "Invariant_ConstrainsI";
+qed "Always_ConstrainsI";
-(* [| F : Invariant INV; F : (INV Int A) Co A |]
+(* [| F : Always INV; F : (INV Int A) Co A |]
==> F : Stable A *)
-bind_thm ("Invariant_StableI", Invariant_ConstrainsI RS StableI);
+bind_thm ("Always_StableI", Always_ConstrainsI RS StableI);
-Goal "[| F : Invariant INV; F : A Co A' |] \
+Goal "[| F : Always INV; F : A Co A' |] \
\ ==> F : A Co (INV Int A')";
by (asm_full_simp_tac
- (simpset() addsimps [Invariant_includes_reachable RS Int_absorb2,
+ (simpset() addsimps [Always_includes_reachable RS Int_absorb2,
Constrains_def, Int_assoc RS sym]) 1);
-qed "Invariant_ConstrainsD";
+qed "Always_ConstrainsD";
-bind_thm ("Invariant_StableD", StableD RSN (2,Invariant_ConstrainsD));
+bind_thm ("Always_StableD", StableD RSN (2,Always_ConstrainsD));
-(** Conjoining Invariants **)
+(** Conjoining Always properties **)
-Goal "[| F : Invariant A; F : Invariant B |] ==> F : Invariant (A Int B)";
-by (auto_tac (claset(), simpset() addsimps [Invariant_eq_always]));
-qed "Invariant_Int";
+Goal "[| F : Always A; F : Always B |] ==> F : Always (A Int B)";
+by (auto_tac (claset(), simpset() addsimps [Always_eq_includes_reachable]));
+qed "Always_Int";
(*Delete the nearest invariance assumption (which will be the second one
- used by Invariant_Int) *)
-val Invariant_thin =
+ used by Always_Int) *)
+val Always_thin =
read_instantiate_sg (sign_of thy)
- [("V", "?F : Invariant ?A")] thin_rl;
+ [("V", "?F : Always ?A")] thin_rl;
(*Combines two invariance ASSUMPTIONS into one. USEFUL??*)
-val Invariant_Int_tac = dtac Invariant_Int THEN'
- assume_tac THEN'
- etac Invariant_thin;
+val Always_Int_tac = dtac Always_Int THEN' assume_tac THEN' etac Always_thin;
(*Combines a list of invariance THEOREMS into one.*)
-val Invariant_Int_rule = foldr1 (fn (th1,th2) => [th1,th2] MRS Invariant_Int);
+val Always_Int_rule = foldr1 (fn (th1,th2) => [th1,th2] MRS Always_Int);
(*To allow expansion of the program's definition when appropriate*)
--- a/src/HOL/UNITY/Constrains.thy Mon May 03 19:03:35 1999 +0200
+++ b/src/HOL/UNITY/Constrains.thy Tue May 04 10:26:00 1999 +0200
@@ -46,8 +46,9 @@
Stable :: "'a set => 'a program set"
"Stable A == A Co A"
- Invariant :: "'a set => 'a program set"
- "Invariant A == {F. Init F <= A} Int Stable A"
+ (*Always is the weak form of "invariant"*)
+ Always :: "'a set => 'a program set"
+ "Always A == {F. Init F <= A} Int Stable A"
(*Polymorphic in both states and the meaning of <= *)
Increasing :: "['a => 'b::{ord}] => 'a program set"
--- a/src/HOL/UNITY/Handshake.ML Mon May 03 19:03:35 1999 +0200
+++ b/src/HOL/UNITY/Handshake.ML Tue May 04 10:26:00 1999 +0200
@@ -21,8 +21,8 @@
Addsimps [simp_of_set invFG_def];
-Goal "(F Join G) : Invariant invFG";
-by (rtac InvariantI 1);
+Goal "(F Join G) : Always invFG";
+by (rtac AlwaysI 1);
by (Force_tac 1);
by (rtac (constrains_imp_Constrains RS StableI) 1);
by (auto_tac (claset(), simpset() addsimps [constrains_Join]));
--- a/src/HOL/UNITY/Lift.ML Mon May 03 19:03:35 1999 +0200
+++ b/src/HOL/UNITY/Lift.ML Tue May 04 10:26:00 1999 +0200
@@ -67,43 +67,43 @@
AddIffs [Min_le_Max];
-Goal "Lprg : Invariant open_stop";
-by (rtac InvariantI 1);
+Goal "Lprg : Always open_stop";
+by (rtac AlwaysI 1);
by (Force_tac 1);
by (constrains_tac 1);
qed "open_stop";
-Goal "Lprg : Invariant stop_floor";
-by (rtac InvariantI 1);
+Goal "Lprg : Always stop_floor";
+by (rtac AlwaysI 1);
by (Force_tac 1);
by (constrains_tac 1);
qed "stop_floor";
(*This one needs open_stop, which was proved above*)
-Goal "Lprg : Invariant open_move";
-by (rtac InvariantI 1);
-by (rtac (open_stop RS Invariant_ConstrainsI RS StableI) 2);
+Goal "Lprg : Always open_move";
+by (rtac AlwaysI 1);
+by (rtac (open_stop RS Always_ConstrainsI RS StableI) 2);
by (Force_tac 1);
by (constrains_tac 1);
qed "open_move";
-Goal "Lprg : Invariant moving_up";
-by (rtac InvariantI 1);
+Goal "Lprg : Always moving_up";
+by (rtac AlwaysI 1);
by (Force_tac 1);
by (constrains_tac 1);
by (blast_tac (claset() addDs [zle_imp_zless_or_eq]) 1);
qed "moving_up";
-Goal "Lprg : Invariant moving_down";
-by (rtac InvariantI 1);
+Goal "Lprg : Always moving_down";
+by (rtac AlwaysI 1);
by (Force_tac 1);
by (constrains_tac 1);
by (blast_tac (claset() addDs [zle_imp_zless_or_eq]) 1);
qed "moving_down";
-Goal "Lprg : Invariant bounded";
-by (rtac InvariantI 1);
-by (rtac (Invariant_Int_rule [moving_up, moving_down] RS Invariant_StableI) 2);
+Goal "Lprg : Always bounded";
+by (rtac AlwaysI 1);
+by (rtac (Always_Int_rule [moving_up, moving_down] RS Always_StableI) 2);
by (Force_tac 1);
by (constrains_tac 1);
by (ALLGOALS Clarify_tac);
@@ -340,19 +340,19 @@
(*Now we observe that our integer metric is really a natural number*)
-Goal "reachable Lprg <= {s. #0 <= metric n s}";
-by (rtac (bounded RS Invariant_includes_reachable RS subset_trans) 1);
+Goal "Lprg : Always {s. #0 <= metric n s}";
+by (rtac (bounded RS Always_weaken) 1);
by (simp_tac (simpset() addsimps metric_simps @ zcompare_rls) 1);
by (auto_tac (claset(),
simpset() addsimps [zless_iff_Suc_zadd, zle_iff_zadd]));
by (REPEAT_FIRST (etac ssubst));
by (auto_tac (claset(), simpset() addsimps [zadd_int]));
-qed "reach_nonneg";
+qed "Always_nonneg";
-val R_thm11 = [reach_nonneg, E_thm11] MRS reachable_LeadsTo_weaken;
+val R_thm11 = [Always_nonneg, E_thm11] MRS Always_LeadsTo_weaken;
Goal "Lprg : (moving Int Req n) LeadsTo (stopped Int atFloor n)";
-by (rtac (reach_nonneg RS integ_0_le_induct) 1);
+by (rtac (Always_nonneg RS integ_0_le_induct) 1);
by (case_tac "#0 < z" 1);
(*If z <= #0 then actually z = #0*)
by (fold_tac [zle_def]);
@@ -374,8 +374,8 @@
by (rtac (lift_2 RS LeadsTo_Trans_Un') 2);
by (rtac (E_thm03 RS LeadsTo_Trans_Un') 2);
by (rtac E_thm02 2);
-by (rtac (open_move RS Invariant_LeadsToI) 1);
-by (rtac (open_stop RS Invariant_LeadsToI) 1);
+by (rtac (open_move RS Always_LeadsToI) 1);
+by (rtac (open_stop RS Always_LeadsToI) 1);
by (rtac subset_imp_LeadsTo 1);
by (Clarify_tac 1);
(*The case split is not essential but makes Blast_tac much faster.
--- a/src/HOL/UNITY/Mutex.ML Mon May 03 19:03:35 1999 +0200
+++ b/src/HOL/UNITY/Mutex.ML Tue May 04 10:26:00 1999 +0200
@@ -16,37 +16,34 @@
[U0_def, U1_def, U2_def, U3_def, U4_def,
V0_def, V1_def, V2_def, V3_def, V4_def]);
-Addsimps (map simp_of_set
- [invariantU_def, invariantV_def, bad_invariantU_def]);
+Addsimps (map simp_of_set [IU_def, IV_def, bad_IU_def]);
(*Simplification for records*)
Addsimps (thms"state.update_defs");
-Goal "Mutex : Invariant invariantU";
-by (rtac InvariantI 1);
+Goal "Mutex : Always IU";
+by (rtac AlwaysI 1);
by (constrains_tac 2);
by Auto_tac;
-qed "invariantU";
+qed "IU";
-Goal "Mutex : Invariant invariantV";
-by (rtac InvariantI 1);
+Goal "Mutex : Always IV";
+by (rtac AlwaysI 1);
by (constrains_tac 2);
by Auto_tac;
-qed "invariantV";
-
-val invariantUV = Invariant_Int_rule [invariantU, invariantV];
-
+qed "IV";
(*The safety property: mutual exclusion*)
-Goal "(reachable Mutex) Int {s. m s = #3 & n s = #3} = {}";
-by (cut_facts_tac [invariantUV RS Invariant_includes_reachable] 1);
+Goal "Mutex : Always {s. ~ (m s = #3 & n s = #3)}";
+by (rtac Always_weaken 1);
+by (rtac ([IU, IV] MRS Always_Int) 1);
by Auto_tac;
qed "mutual_exclusion";
(*The bad invariant FAILS in V1*)
-Goal "Mutex : Invariant bad_invariantU";
-by (rtac InvariantI 1);
+Goal "Mutex : Always bad_IU";
+by (rtac AlwaysI 1);
by (constrains_tac 2);
by (Force_tac 1);
(*Needs a decision procedure to simplify the resulting state*)
@@ -83,7 +80,7 @@
qed "U_F1";
Goal "Mutex : {s. ~ p s & m s = #2} LeadsTo {s. m s = #3}";
-by (cut_facts_tac [invariantU] 1);
+by (cut_facts_tac [IU] 1);
by (ensures_tac "U2" 1);
qed "U_F2";
@@ -112,7 +109,7 @@
(*Misra's F4*)
Goal "Mutex : {s. u s} LeadsTo {s. p s}";
-by (rtac ([invariantU, U_lemma123] MRS Invariant_LeadsTo_weaken) 1);
+by (rtac ([IU, U_lemma123] MRS Always_LeadsTo_weaken) 1);
by Auto_tac;
qed "u_Leadsto_p";
@@ -129,7 +126,7 @@
qed "V_F1";
Goal "Mutex : {s. p s & n s = #2} LeadsTo {s. n s = #3}";
-by (cut_facts_tac [invariantV] 1);
+by (cut_facts_tac [IV] 1);
by (ensures_tac "V2" 1);
qed "V_F2";
@@ -159,7 +156,7 @@
(*Misra's F4*)
Goal "Mutex : {s. v s} LeadsTo {s. ~ p s}";
-by (rtac ([invariantV, V_lemma123] MRS Invariant_LeadsTo_weaken) 1);
+by (rtac ([IV, V_lemma123] MRS Always_LeadsTo_weaken) 1);
by Auto_tac;
qed "v_Leadsto_not_p";
--- a/src/HOL/UNITY/Mutex.thy Mon May 03 19:03:35 1999 +0200
+++ b/src/HOL/UNITY/Mutex.thy Tue May 04 10:26:00 1999 +0200
@@ -60,18 +60,16 @@
(** The correct invariants **)
- invariantU :: state set
- "invariantU == {s. (u s = (#1 <= m s & m s <= #3)) &
- (m s = #3 --> ~ p s)}"
+ IU :: state set
+ "IU == {s. (u s = (#1 <= m s & m s <= #3)) & (m s = #3 --> ~ p s)}"
- invariantV :: state set
- "invariantV == {s. (v s = (#1 <= n s & n s <= #3)) &
- (n s = #3 --> p s)}"
+ IV :: state set
+ "IV == {s. (v s = (#1 <= n s & n s <= #3)) & (n s = #3 --> p s)}"
(** The faulty invariant (for U alone) **)
- bad_invariantU :: state set
- "bad_invariantU == {s. (u s = (#1 <= m s & m s <= #3)) &
- (#3 <= m s & m s <= #4 --> ~ p s)}"
+ bad_IU :: state set
+ "bad_IU == {s. (u s = (#1 <= m s & m s <= #3)) &
+ (#3 <= m s & m s <= #4 --> ~ p s)}"
end
--- a/src/HOL/UNITY/NSP_Bad.ML Mon May 03 19:03:35 1999 +0200
+++ b/src/HOL/UNITY/NSP_Bad.ML Tue May 04 10:26:00 1999 +0200
@@ -67,8 +67,8 @@
(*Spy never sees another agent's private key! (unless it's bad at start)*)
(*
- Goal "Nprg : Invariant {s. (Key (priK A) : parts (spies s)) = (A : bad)}";
- by (rtac InvariantI 1);
+ Goal "Nprg : Always {s. (Key (priK A) : parts (spies s)) = (A : bad)}";
+ by (rtac AlwaysI 1);
by (Force_tac 1);
by (constrains_tac 1);
by Auto_tac;
--- a/src/HOL/UNITY/Reach.ML Mon May 03 19:03:35 1999 +0200
+++ b/src/HOL/UNITY/Reach.ML Tue May 04 10:26:00 1999 +0200
@@ -29,8 +29,8 @@
Addsimps [simp_of_set reach_invariant_def];
-Goal "Rprg : Invariant reach_invariant";
-by (rtac InvariantI 1);
+Goal "Rprg : Always reach_invariant";
+by (rtac AlwaysI 1);
by Auto_tac; (*for the initial state; proof of stability remains*)
by (constrains_tac 1);
by (blast_tac (claset() addIs [r_into_rtrancl,rtrancl_trans]) 1);
@@ -138,6 +138,6 @@
Goal "Rprg : UNIV LeadsTo { %v. (init, v) : edges^* }";
by (stac (fixedpoint_invariant_correct RS sym) 1);
by (rtac ([reach_invariant, LeadsTo_fixedpoint]
- MRS Invariant_LeadsTo_weaken) 1);
+ MRS Always_LeadsTo_weaken) 1);
by Auto_tac;
qed "LeadsTo_correct";
--- a/src/HOL/UNITY/SubstAx.ML Mon May 03 19:03:35 1999 +0200
+++ b/src/HOL/UNITY/SubstAx.ML Tue May 04 10:26:00 1999 +0200
@@ -11,33 +11,21 @@
(*** Specialized laws for handling invariants ***)
-(** Conjoining a safety property **)
+(** Conjoining an Always property **)
-Goal "[| reachable F <= C; F : (C Int A) LeadsTo A' |] \
+Goal "[| F : Always C; F : (C Int A) LeadsTo A' |] \
\ ==> F : A LeadsTo A'";
by (asm_full_simp_tac
- (simpset() addsimps [LeadsTo_def, Int_absorb2, Int_assoc RS sym]) 1);
-qed "reachable_LeadsToI";
+ (simpset() addsimps [LeadsTo_def, Always_eq_includes_reachable,
+ Int_absorb2, Int_assoc RS sym]) 1);
+qed "Always_LeadsToI";
-Goal "[| reachable F <= C; F : A LeadsTo A' |] \
+Goal "[| F : Always C; F : A LeadsTo A' |] \
\ ==> F : A LeadsTo (C Int A')";
by (asm_full_simp_tac
- (simpset() addsimps [LeadsTo_def, Int_absorb2,
- Int_assoc RS sym]) 1);
-qed "reachable_LeadsToD";
-
-
-(** Conjoining an invariant **)
-
-(* [| Invariant F C; F : (C Int A) LeadsTo A' |] ==> F : A LeadsTo A' *)
-bind_thm ("Invariant_LeadsToI",
- Invariant_includes_reachable RS reachable_LeadsToI);
-
-(* [| Invariant F C; F : A LeadsTo A' |] ==> F : A LeadsTo (C Int A') *)
-bind_thm ("Invariant_LeadsToD",
- Invariant_includes_reachable RS reachable_LeadsToD);
-
-
+ (simpset() addsimps [LeadsTo_def, Always_eq_includes_reachable,
+ Int_absorb2, Int_assoc RS sym]) 1);
+qed "Always_LeadsToD";
(*** Introduction rules: Basis, Trans, Union ***)
@@ -115,12 +103,12 @@
LeadsTo_Trans]) 1);
qed "LeadsTo_weaken";
-Goal "[| reachable F <= C; F : A LeadsTo A'; \
+Goal "[| F : Always C; F : A LeadsTo A'; \
\ C Int B <= A; C Int A' <= B' |] \
\ ==> F : B LeadsTo B'";
-by (blast_tac (claset() addDs [reachable_LeadsToI] addIs[LeadsTo_weaken]
- addIs [reachable_LeadsToD]) 1);
-qed "reachable_LeadsTo_weaken";
+by (blast_tac (claset() addDs [Always_LeadsToI] addIs[LeadsTo_weaken]
+ addIs [Always_LeadsToD]) 1);
+qed "Always_LeadsTo_weaken";
(** Two theorems for "proof lattices" **)
@@ -150,7 +138,7 @@
qed "LeadsTo_Union_distrib";
-(** More rules using the premise "Invariant F" **)
+(** More rules using the premise "Always INV" **)
Goal "[| F : (A-A') Co (A Un A'); F : transient (A-A') |] \
\ ==> F : A LeadsTo A'";
@@ -160,24 +148,16 @@
by (blast_tac (claset() addIs [constrains_weaken]) 1);
qed "LeadsTo_Basis";
-Goal "[| F : Invariant INV; \
+Goal "[| F : Always INV; \
\ F : (INV Int (A-A')) Co (A Un A'); \
\ F : transient (INV Int (A-A')) |] \
\ ==> F : A LeadsTo A'";
-by (rtac Invariant_LeadsToI 1);
+by (rtac Always_LeadsToI 1);
by (assume_tac 1);
by (rtac LeadsTo_Basis 1);
by (blast_tac (claset() addIs [transient_strengthen]) 2);
-by (blast_tac (claset() addIs [Invariant_ConstrainsD RS Constrains_weaken]) 1);
-qed "Invariant_LeadsTo_Basis";
-
-Goal "[| F : Invariant INV; \
-\ F : A LeadsTo A'; INV Int B <= A; INV Int A' <= B' |] \
-\ ==> F : B LeadsTo B'";
-by (REPEAT (ares_tac [Invariant_includes_reachable,
- reachable_LeadsTo_weaken] 1));
-qed "Invariant_LeadsTo_weaken";
-
+by (blast_tac (claset() addIs [Always_ConstrainsD RS Constrains_weaken]) 1);
+qed "Always_LeadsTo_Basis";
(*Set difference: maybe combine with leadsTo_weaken_L??
This is the most useful form of the "disjunction" rule*)
@@ -251,9 +231,11 @@
(** The impossibility law **)
(*The set "A" may be non-empty, but it contains no reachable states*)
-Goal "F : A LeadsTo {} ==> reachable F Int A = {}";
-by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1);
-by (etac leadsTo_empty 1);
+Goal "F : A LeadsTo {} ==> F : Always (-A)";
+by (full_simp_tac (simpset() addsimps [LeadsTo_def,
+ Always_eq_includes_reachable]) 1);
+by (dtac leadsTo_empty 1);
+by Auto_tac;
qed "LeadsTo_empty";
@@ -295,12 +277,12 @@
Goal "[| F : Stable A; F : transient C; \
-\ reachable F <= (-A Un B Un C) |] ==> F : A LeadsTo B";
-by (etac reachable_LeadsTo_weaken 1);
+\ F : Always (-A Un B Un C) |] ==> F : A LeadsTo B";
+by (etac Always_LeadsTo_weaken 1);
by (rtac LeadsTo_Diff 1);
by (etac (transient_imp_leadsTo RS leadsTo_imp_LeadsTo RS PSP_stable2) 2);
by (ALLGOALS (blast_tac (claset() addIs [subset_imp_LeadsTo])));
-qed "Stable_transient_reachable_LeadsTo";
+qed "Stable_transient_Always_LeadsTo";
(*** Induction rules ***)
@@ -337,13 +319,13 @@
(*Integer version. Could generalize from #0 to any lower bound*)
val [reach, prem] =
-Goal "[| reachable F <= {s. #0 <= f s}; \
+Goal "[| F : Always {s. #0 <= f s}; \
\ !! z. F : (A Int {s. f s = z}) LeadsTo \
\ ((A Int {s. f s < z}) Un B) |] \
\ ==> F : A LeadsTo B";
by (res_inst_tac [("f", "nat o f")] (allI RS LessThan_induct) 1);
by (simp_tac (simpset() addsimps [vimage_def]) 1);
-by (rtac ([reach, prem] MRS reachable_LeadsTo_weaken) 1);
+by (rtac ([reach, prem] MRS Always_LeadsTo_weaken) 1);
by (auto_tac (claset(), simpset() addsimps [nat_eq_iff, nat_less_iff]));
qed "integ_0_le_induct";
@@ -412,8 +394,8 @@
(*proves "ensures/leadsTo" properties when the program is specified*)
fun ensures_tac sact =
SELECT_GOAL
- (EVERY [REPEAT (Invariant_Int_tac 1),
- etac Invariant_LeadsTo_Basis 1
+ (EVERY [REPEAT (Always_Int_tac 1),
+ etac Always_LeadsTo_Basis 1
ORELSE (*subgoal may involve LeadsTo, leadsTo or ensures*)
REPEAT (ares_tac [LeadsTo_Basis, ensuresI] 1),
(*now there are two subgoals: co & transient*)
--- a/src/HOL/UNITY/Union.ML Mon May 03 19:03:35 1999 +0200
+++ b/src/HOL/UNITY/Union.ML Tue May 04 10:26:00 1999 +0200
@@ -249,14 +249,14 @@
by (Blast_tac 1);
qed "stable_constrains_Join";
-(*Premise for G cannot use Invariant because Stable F A is weaker than
+(*Premise for G cannot use Always because Stable F A is weaker than
G : stable A *)
-Goal "[| F : stable A; G : invariant A |] ==> F Join G : Invariant A";
-by (full_simp_tac (simpset() addsimps [Invariant_def, invariant_def,
+Goal "[| F : stable A; G : invariant A |] ==> F Join G : Always A";
+by (full_simp_tac (simpset() addsimps [Always_def, invariant_def,
Stable_eq_stable, stable_Join]) 1);
by (force_tac(claset() addIs [stable_reachable, stable_Int],
simpset() addsimps [Acts_Join]) 1);
-qed "stable_Join_Invariant";
+qed "stable_Join_Always";
Goal "[| F : stable A; G : A ensures B |] ==> F Join G : A ensures B";
by (asm_simp_tac (simpset() addsimps [ensures_Join]) 1);