Constrains, Stable, Invariant...more of the substitution axiom, but Union
does not work well with them
--- a/src/HOL/UNITY/Common.ML Thu Aug 13 17:44:50 1998 +0200
+++ b/src/HOL/UNITY/Common.ML Thu Aug 13 18:06:40 1998 +0200
@@ -11,25 +11,21 @@
*)
(*Misra's property CMT4: t exceeds no common meeting time*)
-Goal "[| ALL m. constrains acts {m} (maxfg m); n: common |] \
-\ ==> stable acts (atMost n)";
-by (dres_inst_tac [("P", "%t. t<=n")] elimination_sing 1);
+Goal "[| ALL m. Constrains prg {m} (maxfg m); n: common |] \
+\ ==> Stable prg (atMost n)";
+by (dres_inst_tac [("M", "{t. t<=n}")] Elimination_sing 1);
by (asm_full_simp_tac
- (simpset() addsimps [atMost_def, stable_def, common_def, maxfg_def,
- constrains_def, le_max_iff_disj]) 1);
-by (Clarify_tac 1);
-by (dtac bspec 1);
-by (assume_tac 1);
-by (blast_tac (claset() addSEs [subsetCE]
- addIs [order_eq_refl, fmono, gmono, le_trans]) 1);
+ (simpset() addsimps [atMost_def, Stable_def, common_def, maxfg_def,
+ le_max_iff_disj]) 1);
+by (etac Constrains_weaken_R 1);
+by (blast_tac (claset() addIs [order_eq_refl, fmono, gmono, le_trans]) 1);
qed "common_stable";
-Goal "[| ALL m. constrains acts {m} (maxfg m); n: common |] \
-\ ==> invariant (|Init={0}, Acts=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";
+Goal "[| Init prg <= atMost n; \
+\ ALL m. Constrains prg {m} (maxfg m); n: common |] \
+\ ==> Invariant prg (atMost n)";
+by (asm_simp_tac (simpset() addsimps [InvariantI, common_stable]) 1);
+qed "common_Invariant";
(*** Some programs that implement the safety property above ***)
@@ -71,23 +67,23 @@
Addsimps [atMost_Int_atLeast];
-Goal "[| ALL m. constrains acts {m} (maxfg m); \
-\ ALL m: lessThan n. leadsTo acts {m} (greaterThan m); \
-\ n: common; id: acts |] \
-\ ==> leadsTo acts (atMost n) common";
-by (rtac leadsTo_weaken_R 1);
-by (res_inst_tac [("f","%x. x"), ("l", "n")] greaterThan_bounded_induct 1);
+Goal "[| ALL m. Constrains prg {m} (maxfg m); \
+\ ALL m: lessThan n. LeadsTo prg {m} (greaterThan m); \
+\ n: common; id: Acts prg |] \
+\ ==> LeadsTo prg (atMost n) common";
+by (rtac LeadsTo_weaken_R 1);
+by (res_inst_tac [("f","%x. x"), ("l", "n")] GreaterThan_bounded_induct 1);
by (ALLGOALS Asm_simp_tac);
by (rtac subset_refl 2);
-by (blast_tac (claset() addDs [psp_stable2]
- addIs [common_stable, leadsTo_weaken_R]) 1);
+by (blast_tac (claset() addDs [PSP_stable2]
+ addIs [common_stable, LeadsTo_weaken_R]) 1);
val lemma = result();
(*The "ALL m: Compl common" form echoes CMT6.*)
-Goal "[| ALL m. constrains acts {m} (maxfg m); \
-\ ALL m: Compl common. leadsTo acts {m} (greaterThan m); \
-\ n: common; id: acts |] \
-\ ==> leadsTo acts (atMost (LEAST n. n: common)) common";
+Goal "[| ALL m. Constrains prg {m} (maxfg m); \
+\ ALL m: Compl common. LeadsTo prg {m} (greaterThan m); \
+\ n: common; id: Acts prg |] \
+\ ==> LeadsTo prg (atMost (LEAST n. n: common)) common";
by (rtac lemma 1);
by (ALLGOALS Asm_simp_tac);
by (etac LeastI 2);
--- a/src/HOL/UNITY/Common.thy Thu Aug 13 17:44:50 1998 +0200
+++ b/src/HOL/UNITY/Common.thy Thu Aug 13 18:06:40 1998 +0200
@@ -10,7 +10,7 @@
From Misra, "A Logic for Concurrent Programming" (1994), sections 5.1 and 13.1.
*)
-Common = WFair + Traces +
+Common = SubstAx +
consts
ftime,gtime :: nat=>nat
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/Constrains.ML Thu Aug 13 18:06:40 1998 +0200
@@ -0,0 +1,262 @@
+(* Title: HOL/UNITY/Constrains
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1998 University of Cambridge
+
+Safety relations: restricted to the set of reachable states.
+*)
+
+
+
+(**MOVE TO EQUALITIES.ML**)
+
+Goal "(A Un B <= C) = (A <= C & B <= C)";
+by (Blast_tac 1);
+qed "Un_subset_iff";
+
+Goal "(C <= A Int B) = (C <= A & C <= B)";
+by (Blast_tac 1);
+qed "Int_subset_iff";
+
+
+(*** Constrains ***)
+
+(*constrains (Acts prg) B B'
+ ==> constrains (Acts prg) (reachable prg Int B) (reachable prg Int B')*)
+bind_thm ("constrains_reachable_Int",
+ subset_refl RS
+ rewrite_rule [stable_def] stable_reachable RS
+ constrains_Int);
+
+Goalw [Constrains_def]
+ "constrains (Acts prg) A A' ==> Constrains prg A A'";
+by (etac constrains_reachable_Int 1);
+qed "constrains_imp_Constrains";
+
+val prems = Goal
+ "(!!act s s'. [| act: Acts prg; (s,s') : act; s: A |] ==> s': A') \
+\ ==> Constrains prg A A'";
+by (rtac constrains_imp_Constrains 1);
+by (blast_tac (claset() addIs (constrainsI::prems)) 1);
+qed "ConstrainsI";
+
+Goalw [Constrains_def, constrains_def] "Constrains prg {} B";
+by (Blast_tac 1);
+qed "Constrains_empty";
+
+Goal "Constrains prg A UNIV";
+by (blast_tac (claset() addIs [ConstrainsI]) 1);
+qed "Constrains_UNIV";
+AddIffs [Constrains_empty, Constrains_UNIV];
+
+
+Goalw [Constrains_def]
+ "[| Constrains prg A A'; A'<=B' |] ==> Constrains prg A B'";
+by (blast_tac (claset() addIs [constrains_weaken_R]) 1);
+qed "Constrains_weaken_R";
+
+Goalw [Constrains_def]
+ "[| Constrains prg A A'; B<=A |] ==> Constrains prg B A'";
+by (blast_tac (claset() addIs [constrains_weaken_L]) 1);
+qed "Constrains_weaken_L";
+
+Goalw [Constrains_def]
+ "[| Constrains prg A A'; B<=A; A'<=B' |] ==> Constrains prg B B'";
+by (blast_tac (claset() addIs [constrains_weaken]) 1);
+qed "Constrains_weaken";
+
+(** Union **)
+
+Goalw [Constrains_def]
+ "[| Constrains prg A A'; Constrains prg B B' |] \
+\ ==> Constrains prg (A Un B) (A' Un B')";
+by (blast_tac (claset() addIs [constrains_Un RS constrains_weaken]) 1);
+qed "Constrains_Un";
+
+Goalw [Constrains_def]
+ "ALL i:I. Constrains prg (A i) (A' i) \
+\ ==> Constrains prg (UN i:I. A i) (UN i:I. A' i)";
+by (dtac ball_constrains_UN 1);
+by (blast_tac (claset() addIs [constrains_weaken]) 1);
+qed "ball_Constrains_UN";
+
+(** Intersection **)
+
+Goalw [Constrains_def]
+ "[| Constrains prg A A'; Constrains prg B B' |] \
+\ ==> Constrains prg (A Int B) (A' Int B')";
+by (blast_tac (claset() addIs [constrains_Int RS constrains_weaken]) 1);
+qed "Constrains_Int";
+
+Goalw [Constrains_def]
+ "[| ALL i:I. Constrains prg (A i) (A' i) |] \
+\ ==> Constrains prg (INT i:I. A i) (INT i:I. A' i)";
+by (dtac ball_constrains_INT 1);
+by (blast_tac (claset() addIs [constrains_reachable_Int, constrains_weaken]) 1);
+qed "ball_Constrains_INT";
+
+Goalw [Constrains_def]
+ "[| Constrains prg A A'; id: Acts prg |] ==> reachable prg Int A <= A'";
+by (dtac constrains_imp_subset 1);
+by (assume_tac 1);
+by (full_simp_tac (simpset() addsimps [Int_subset_iff, Int_lower1]) 1);
+qed "Constrains_imp_subset";
+
+Goalw [Constrains_def]
+ "[| id: Acts prg; Constrains prg A B; Constrains prg B C |] \
+\ ==> Constrains prg A C";
+by (blast_tac (claset() addIs [constrains_trans, constrains_weaken]) 1);
+qed "Constrains_trans";
+
+
+(*** Stable ***)
+
+Goal "Stable prg A = stable (Acts prg) (reachable prg Int A)";
+by (simp_tac (simpset() addsimps [Stable_def, Constrains_def, stable_def]) 1);
+qed "Stable_eq_stable";
+
+Goalw [Stable_def] "Constrains prg A A ==> Stable prg A";
+by (assume_tac 1);
+qed "StableI";
+
+Goalw [Stable_def] "Stable prg A ==> Constrains prg A A";
+by (assume_tac 1);
+qed "StableD";
+
+Goalw [Stable_def]
+ "[| Stable prg A; Stable prg A' |] ==> Stable prg (A Un A')";
+by (blast_tac (claset() addIs [Constrains_Un]) 1);
+qed "Stable_Un";
+
+Goalw [Stable_def]
+ "[| Stable prg A; Stable prg A' |] ==> Stable prg (A Int A')";
+by (blast_tac (claset() addIs [Constrains_Int]) 1);
+qed "Stable_Int";
+
+Goalw [Stable_def]
+ "[| Stable prg C; Constrains prg A (C Un A') |] \
+\ ==> Constrains prg (C Un A) (C Un A')";
+by (blast_tac (claset() addIs [Constrains_Un RS Constrains_weaken]) 1);
+qed "Stable_Constrains_Un";
+
+Goalw [Stable_def]
+ "[| Stable prg C; Constrains prg (C Int A) A' |] \
+\ ==> Constrains prg (C Int A) (C Int A')";
+by (blast_tac (claset() addIs [Constrains_Int RS Constrains_weaken]) 1);
+qed "Stable_Constrains_Int";
+
+Goalw [Stable_def]
+ "(ALL i:I. Stable prg (A i)) ==> Stable prg (INT i:I. A i)";
+by (etac ball_Constrains_INT 1);
+qed "ball_Stable_INT";
+
+Goal "Stable prg (reachable prg)";
+by (simp_tac (simpset() addsimps [Stable_eq_stable, stable_reachable]) 1);
+qed "Stable_reachable";
+
+
+
+(*** The Elimination Theorem. The "free" m has become universally quantified!
+ Should the premise be !!m instead of ALL m ? Would make it harder to use
+ in forward proof. ***)
+
+Goalw [Constrains_def, constrains_def]
+ "[| ALL m. Constrains prg {s. s x = m} (B m) |] \
+\ ==> Constrains prg {s. s x : M} (UN m:M. B m)";
+by (Blast_tac 1);
+qed "Elimination";
+
+(*As above, but for the trivial case of a one-variable state, in which the
+ state is identified with its one variable.*)
+Goalw [Constrains_def, constrains_def]
+ "(ALL m. Constrains prg {m} (B m)) ==> Constrains prg M (UN m:M. B m)";
+by (Blast_tac 1);
+qed "Elimination_sing";
+
+Goalw [Constrains_def, constrains_def]
+ "[| Constrains prg A (A' Un B); Constrains prg B B'; id: Acts prg |] \
+\ ==> Constrains prg A (A' Un B')";
+by (Blast_tac 1);
+qed "Constrains_cancel";
+
+
+(*** Specialized laws for handling Invariants ***)
+
+(** Natural deduction rules for "Invariant prg A" **)
+
+Goal "[| Init prg<=A; Stable prg A |] ==> Invariant prg A";
+by (asm_simp_tac (simpset() addsimps [Invariant_def]) 1);
+qed "InvariantI";
+
+Goal "Invariant prg A ==> Init prg<=A & Stable prg A";
+by (asm_full_simp_tac (simpset() addsimps [Invariant_def]) 1);
+qed "InvariantD";
+
+bind_thm ("InvariantE", InvariantD RS conjE);
+
+
+(*The set of all reachable states is an Invariant...*)
+Goal "Invariant prg (reachable prg)";
+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 prg A ==> reachable prg <= A";
+by (full_simp_tac
+ (simpset() addsimps [Stable_def, Constrains_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 "Invariant_includes_reachable";
+
+
+Goal "Invariant prg INV ==> reachable prg Int INV = reachable prg";
+by (dtac Invariant_includes_reachable 1);
+by (Blast_tac 1);
+qed "reachable_Int_INV";
+
+Goal "[| Invariant prg INV; Constrains prg (INV Int A) A' |] \
+\ ==> Constrains prg A A'";
+by (asm_full_simp_tac
+ (simpset() addsimps [Constrains_def, reachable_Int_INV,
+ Int_assoc RS sym]) 1);
+qed "Invariant_ConstrainsI";
+
+bind_thm ("Invariant_StableI", Invariant_ConstrainsI RS StableI);
+
+Goal "[| Invariant prg INV; Constrains prg A A' |] \
+\ ==> Constrains prg A (INV Int A')";
+by (asm_full_simp_tac
+ (simpset() addsimps [Constrains_def, reachable_Int_INV,
+ Int_assoc RS sym]) 1);
+qed "Invariant_ConstrainsD";
+
+bind_thm ("Invariant_StableD", StableD RSN (2,Invariant_ConstrainsD));
+
+
+
+(** Conjoining Invariants **)
+
+Goal "[| Invariant prg A; Invariant prg B |] ==> Invariant prg (A Int B)";
+by (auto_tac (claset(),
+ simpset() addsimps [Invariant_def, Stable_Int]));
+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);
+
+
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/Constrains.thy Thu Aug 13 18:06:40 1998 +0200
@@ -0,0 +1,28 @@
+(* Title: HOL/UNITY/Constrains
+ ID: $Id$
+ Author: Lawrence C Paulson, Cambridge University Computer Laboratory
+ Copyright 1998 University of Cambridge
+
+Safety relations: restricted to the set of reachable states.
+*)
+
+Constrains = UNITY + Traces +
+
+constdefs
+
+ Constrains :: "['a program, 'a set, 'a set] => bool"
+ "Constrains prg A B ==
+ constrains (Acts prg)
+ (reachable prg Int A)
+ (reachable prg Int B)"
+
+ Stable :: "'a program => 'a set => bool"
+ "Stable prg A == Constrains prg A A"
+
+ Unless :: "['a program, 'a set, 'a set] => bool"
+ "Unless prg A B == Constrains prg (A-B) (A Un B)"
+
+ Invariant :: "['a program, 'a set] => bool"
+ "Invariant prg A == (Init prg) <= A & Stable prg A"
+
+end
--- a/src/HOL/UNITY/Handshake.ML Thu Aug 13 17:44:50 1998 +0200
+++ b/src/HOL/UNITY/Handshake.ML Thu Aug 13 18:06:40 1998 +0200
@@ -22,40 +22,40 @@
AddIffs [id_in_Acts];
-Goalw [prgF_def, prgG_def] "invariant (Join prgF prgG) invFG";
-by (rtac invariantI 1);
-by (force_tac (claset(),
- simpset() addsimps [Join_def]) 1);
-by (auto_tac (claset(), simpset() addsimps [stable_Join]));
+Goalw [prgF_def, prgG_def] "Invariant (Join prgF prgG) invFG";
+by (rtac InvariantI 1);
+by (Force_tac 1);
+by (rtac (constrains_imp_Constrains RS StableI) 1);
+by (auto_tac (claset(), simpset() addsimps [constrains_Join]));
by (constrains_tac [prgG_def,cmdG_def] 2);
by (auto_tac (claset() addIs [le_anti_sym] addSEs [le_SucE], simpset()));
by (constrains_tac [prgF_def,cmdF_def] 1);
qed "invFG";
Goal "LeadsTo (Join prgF prgG) {s. NF s = k & ~ BB s} {s. NF s = k & BB s}";
-br (ensures_stable_Join1 RS leadsTo_Basis RS leadsTo_imp_LeadsTo) 1;
+by (rtac (ensures_stable_Join1 RS leadsTo_Basis RS leadsTo_imp_LeadsTo) 1);
by (ensures_tac [prgG_def,cmdG_def] "cmdG" 2);
by (constrains_tac [prgF_def,cmdF_def] 1);
qed "lemma2_1";
Goal "LeadsTo (Join prgF prgG) {s. NF s = k & BB s} {s. k < NF s}";
-br (ensures_stable_Join2 RS leadsTo_Basis RS leadsTo_imp_LeadsTo) 1;
+by (rtac (ensures_stable_Join2 RS leadsTo_Basis RS leadsTo_imp_LeadsTo) 1);
by (constrains_tac [prgG_def,cmdG_def] 2);
by (ensures_tac [prgF_def,cmdF_def] "cmdF" 1);
qed "lemma2_2";
Goal "LeadsTo (Join prgF prgG) UNIV {s. m < NF s}";
-br LeadsTo_weaken_R 1;
+by (rtac LeadsTo_weaken_R 1);
by (res_inst_tac [("f", "NF"), ("l","Suc m"), ("B","{}")]
GreaterThan_bounded_induct 1);
by (auto_tac (claset(), simpset() addsimps [vimage_def]));
by (trans_tac 2);
(*The inductive step: LeadsTo (Join prgF prgG) {x. NF x = ma} {x. ma < NF x}*)
-br LeadsTo_Diff 1;
-br lemma2_2 2;
-br LeadsTo_Trans 1;
-br lemma2_2 2;
-br (lemma2_1 RS LeadsTo_weaken_L) 1;
+by (rtac LeadsTo_Diff 1);
+by (rtac lemma2_2 2);
+by (rtac LeadsTo_Trans 1);
+by (rtac lemma2_2 2);
+by (rtac (lemma2_1 RS LeadsTo_weaken_L) 1);
by Auto_tac;
qed "progress";
--- a/src/HOL/UNITY/Lift.ML Thu Aug 13 17:44:50 1998 +0200
+++ b/src/HOL/UNITY/Lift.ML Thu Aug 13 18:06:40 1998 +0200
@@ -44,34 +44,36 @@
qed "less_imp_le_pred";
-Goalw [Lprg_def] "invariant Lprg open_stop";
-by (rtac invariantI 1);
+Goalw [Lprg_def] "Invariant Lprg open_stop";
+by (rtac InvariantI 1);
by (Force_tac 1);
by (constrains_tac (cmd_defs@always_defs) 1);
qed "open_stop";
-Goalw [Lprg_def] "invariant Lprg stop_floor";
-by (rtac invariantI 1);
+Goalw [Lprg_def] "Invariant Lprg stop_floor";
+by (rtac InvariantI 1);
by (Force_tac 1);
by (constrains_tac (cmd_defs@always_defs) 1);
qed "stop_floor";
-(*Should not have to prove open_stop concurrently!!*)
-Goalw [Lprg_def] "invariant Lprg (open_stop Int open_move)";
-by (rtac invariantI 1);
+(*This one needs open_stop, which was proved above*)
+Goal "Invariant Lprg open_move";
+by (rtac InvariantI 1);
+br (open_stop RS Invariant_ConstrainsI RS StableI) 2;
+bw Lprg_def;
by (Force_tac 1);
by (constrains_tac (cmd_defs@always_defs) 1);
qed "open_move";
-Goalw [Lprg_def] "invariant Lprg moving_up";
-by (rtac invariantI 1);
+Goalw [Lprg_def] "Invariant Lprg moving_up";
+by (rtac InvariantI 1);
by (Force_tac 1);
by (constrains_tac (cmd_defs@always_defs) 1);
by (blast_tac (claset() addDs [le_imp_less_or_eq]) 1);
qed "moving_up";
-Goalw [Lprg_def] "invariant Lprg moving_down";
-by (rtac invariantI 1);
+Goalw [Lprg_def] "Invariant Lprg moving_down";
+by (rtac InvariantI 1);
by (Force_tac 1);
by (constrains_tac (cmd_defs@always_defs) 1);
by (dres_inst_tac [("m","f")] le_imp_less_or_eq 3);
@@ -82,8 +84,8 @@
xxxxxxxxxxxxxxxx;
-Goalw [Lprg_def] "invariant Lprg bounded";
-by (rtac invariantI 1);
+Goalw [Lprg_def] "Invariant Lprg bounded";
+by (rtac InvariantI 1);
by (Force_tac 1);
by (constrains_tac (cmd_defs@always_defs) 1);
by (ALLGOALS
@@ -94,8 +96,8 @@
by (blast_tac (claset() addIs [diff_le_self, le_trans]) 3);
qed "bounded";
-Goalw [Lprg_def] "invariant Lprg invariantV";
-by (rtac invariantI 1);
+Goalw [Lprg_def] "Invariant Lprg invariantV";
+by (rtac InvariantI 1);
by (constrains_tac cmd_defs 2);
by Auto_tac;
qed "invariantV";
@@ -122,7 +124,7 @@
Goal "LeadsTo Lprg {s. ~ PP s & MM s = 2} {s. MM s = 3}";
by (cut_facts_tac [invariantUV] 1);
-bw Lprg_def;
+by (rewtac Lprg_def);
by (ensures_tac cmd_defs "cmd2U" 1);
qed "U_F2";
--- a/src/HOL/UNITY/Mutex.ML Thu Aug 13 17:44:50 1998 +0200
+++ b/src/HOL/UNITY/Mutex.ML Thu Aug 13 18:06:40 1998 +0200
@@ -26,34 +26,35 @@
Addsimps update_defs;
-
Addsimps [invariantU_def, invariantV_def];
-Goalw [Mprg_def] "invariant Mprg invariantU";
-by (rtac invariantI 1);
+Goalw [Mprg_def] "Invariant Mprg invariantU";
+by (rtac InvariantI 1);
by (constrains_tac cmd_defs 2);
by Auto_tac;
qed "invariantU";
-Goalw [Mprg_def] "invariant Mprg invariantV";
-by (rtac invariantI 1);
+Goalw [Mprg_def] "Invariant Mprg invariantV";
+by (rtac InvariantI 1);
by (constrains_tac cmd_defs 2);
by Auto_tac;
qed "invariantV";
-val invariantUV = invariant_Int_rule [invariantU, invariantV];
+val invariantUV = Invariant_Int_rule [invariantU, invariantV];
(*The safety property: mutual exclusion*)
Goal "(reachable Mprg) Int {s. MM s = 3 & NN s = 3} = {}";
-by (cut_facts_tac [invariantUV RS invariant_includes_reachable] 1);
+by (cut_facts_tac [invariantUV RS Invariant_includes_reachable] 1);
by Auto_tac;
qed "mutual_exclusion";
(*The bad invariant FAILS in cmd1V*)
-Goalw [bad_invariantU_def] "stable (Acts Mprg) bad_invariantU";
+Goalw [Mprg_def, bad_invariantU_def] "Invariant Mprg bad_invariantU";
+by (rtac InvariantI 1);
+by (Force_tac 1);
by (constrains_tac cmd_defs 1);
by (REPEAT (trans_tac 1));
by (safe_tac (claset() addSEs [le_SucE]));
@@ -67,7 +68,7 @@
(*** Progress for U ***)
-Goalw [unless_def] "unless (Acts Mprg) {s. MM s=2} {s. MM s=3}";
+Goalw [Unless_def] "Unless Mprg {s. MM s=2} {s. MM s=3}";
by (constrains_tac cmd_defs 1);
qed "U_F0";
@@ -77,13 +78,12 @@
Goal "LeadsTo Mprg {s. ~ PP s & MM s = 2} {s. MM s = 3}";
by (cut_facts_tac [invariantUV] 1);
-bw Mprg_def;
+by (rewtac Mprg_def);
by (ensures_tac cmd_defs "cmd2U" 1);
qed "U_F2";
Goal "LeadsTo Mprg {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 (res_inst_tac [("B", "{s. MM s = 4}")] LeadsTo_Trans 1);
by (ensures_tac cmd_defs "cmd4U" 2);
by (ensures_tac cmd_defs "cmd3U" 1);
qed "U_F3";
@@ -109,15 +109,15 @@
(*Misra's F4*)
Goal "LeadsTo Mprg {s. UU s} {s. PP s}";
-by (rtac ([invariantU, U_lemma123] MRS invariant_LeadsTo_weaken) 1);
+by (rtac ([invariantU, U_lemma123] MRS Invariant_LeadsTo_weaken) 1);
by Auto_tac;
-qed "u_leadsto_p";
+qed "u_Leadsto_p";
(*** Progress for V ***)
-Goalw [unless_def] "unless (Acts Mprg) {s. NN s=2} {s. NN s=3}";
+Goalw [Unless_def] "Unless Mprg {s. NN s=2} {s. NN s=3}";
by (constrains_tac cmd_defs 1);
qed "V_F0";
@@ -131,8 +131,7 @@
qed "V_F2";
Goal "LeadsTo Mprg {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 (res_inst_tac [("B", "{s. NN s = 4}")] LeadsTo_Trans 1);
by (ensures_tac cmd_defs "cmd4V" 2);
by (ensures_tac cmd_defs "cmd3V" 1);
qed "V_F3";
@@ -159,9 +158,9 @@
(*Misra's F4*)
Goal "LeadsTo Mprg {s. VV s} {s. ~ PP s}";
-by (rtac ([invariantV, V_lemma123] MRS invariant_LeadsTo_weaken) 1);
+by (rtac ([invariantV, V_lemma123] MRS Invariant_LeadsTo_weaken) 1);
by Auto_tac;
-qed "v_leadsto_not_p";
+qed "v_Leadsto_not_p";
(** Absence of starvation **)
@@ -174,10 +173,10 @@
by (simp_tac (simpset() addsimps [Collect_conj_eq] ) 1);
by (stac Un_commute 1);
by (rtac LeadsTo_Un_duplicate 1);
-by (rtac ([v_leadsto_not_p, U_F0] MRS PSP_unless RSN(2, LeadsTo_cancel2)) 1);
+by (rtac ([v_Leadsto_not_p, U_F0] MRS PSP_Unless RSN(2, LeadsTo_cancel2)) 1);
by (rtac (U_F1 RS LeadsTo_weaken_R) 1);
by (auto_tac (claset() addSEs [less_SucE], simpset()));
-qed "m1_leadsto_3";
+qed "m1_Leadsto_3";
(*The same for V*)
@@ -188,7 +187,7 @@
by (simp_tac (simpset() addsimps [Collect_conj_eq] ) 1);
by (stac Un_commute 1);
by (rtac LeadsTo_Un_duplicate 1);
-by (rtac ([u_leadsto_p, V_F0] MRS PSP_unless RSN(2, LeadsTo_cancel2)) 1);
+by (rtac ([u_Leadsto_p, V_F0] MRS PSP_Unless RSN(2, LeadsTo_cancel2)) 1);
by (rtac (V_F1 RS LeadsTo_weaken_R) 1);
by (auto_tac (claset() addSEs [less_SucE], simpset()));
-qed "n1_leadsto_3";
+qed "n1_Leadsto_3";
--- a/src/HOL/UNITY/Reach.ML Thu Aug 13 17:44:50 1998 +0200
+++ b/src/HOL/UNITY/Reach.ML Thu Aug 13 18:06:40 1998 +0200
@@ -31,8 +31,8 @@
Addsimps [reach_invariant_def];
-Goalw [Rprg_def] "invariant Rprg reach_invariant";
-by (rtac invariantI 1);
+Goalw [Rprg_def] "Invariant Rprg reach_invariant";
+by (rtac InvariantI 1);
by Auto_tac; (*for the initial state; proof of stability remains*)
by (constrains_tac [Rprg_def, asgt_def] 1);
by (blast_tac (claset() addIs [r_into_rtrancl,rtrancl_trans]) 1);
@@ -117,38 +117,31 @@
simpset() addsimps [fun_upd_idem]));
qed "metric_le";
-Goal "(u,v): edges ==> \
-\ ensures (Acts Rprg) ((metric-``{m}) Int {s. s u & ~ s v}) \
-\ (metric-``(lessThan m))";
-by (ensures_tac [Rprg_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";
-
-Goal "leadsTo (Acts Rprg) ((metric-``{m}) - fixedpoint) (metric-``(lessThan m))";
+Goal "LeadsTo Rprg ((metric-``{m}) - fixedpoint) (metric-``(lessThan m))";
by (simp_tac (simpset() addsimps [Diff_fixedpoint]) 1);
-by (rtac leadsTo_UN 1);
-by (split_all_tac 1);
-by (asm_simp_tac (simpset() addsimps [edges_ensures RS leadsTo_Basis]) 1);
-qed "leadsTo_Diff_fixedpoint";
+by (rtac LeadsTo_UN 1);
+by Auto_tac;
+by (ensures_tac [Rprg_def, asgt_def] "asgt a b" 1);
+by (cut_facts_tac [metric_le RS le_imp_less_or_eq] 1);
+by (Fast_tac 1);
+qed "LeadsTo_Diff_fixedpoint";
-Goal "leadsTo (Acts Rprg) (metric-``{m}) (metric-``(lessThan m) Un fixedpoint)";
-by (rtac (leadsTo_Diff_fixedpoint RS leadsTo_weaken_R RS leadsTo_Diff) 1);
-by (ALLGOALS (blast_tac (claset() addIs [subset_imp_leadsTo])));
-qed "leadsTo_Un_fixedpoint";
+Goal "LeadsTo Rprg (metric-``{m}) (metric-``(lessThan m) Un fixedpoint)";
+by (rtac (LeadsTo_Diff_fixedpoint RS LeadsTo_weaken_R RS LeadsTo_Diff) 1);
+by (ALLGOALS (blast_tac (claset() addIs [subset_imp_LeadsTo])));
+qed "LeadsTo_Un_fixedpoint";
(*Execution in any state leads to a fixedpoint (i.e. can terminate)*)
-Goal "leadsTo (Acts Rprg) UNIV fixedpoint";
-by (rtac lessThan_induct 1);
+Goal "LeadsTo Rprg UNIV fixedpoint";
+by (rtac LessThan_induct 1);
by Auto_tac;
-by (rtac leadsTo_Un_fixedpoint 1);
-qed "leadsTo_fixedpoint";
+by (rtac LeadsTo_Un_fixedpoint 1);
+qed "LeadsTo_fixedpoint";
Goal "LeadsTo Rprg UNIV { %v. (init, v) : edges^* }";
by (stac (fixedpoint_invariant_correct RS sym) 1);
-by (rtac ([reach_invariant,
- leadsTo_fixedpoint RS leadsTo_imp_LeadsTo]
- MRS invariant_LeadsTo_weaken) 1);
+by (rtac ([reach_invariant, LeadsTo_fixedpoint]
+ MRS Invariant_LeadsTo_weaken) 1);
by Auto_tac;
qed "LeadsTo_correct";
--- a/src/HOL/UNITY/SubstAx.ML Thu Aug 13 17:44:50 1998 +0200
+++ b/src/HOL/UNITY/SubstAx.ML Thu Aug 13 18:06:40 1998 +0200
@@ -7,32 +7,22 @@
*)
-(*constrains (Acts prg) B B'
- ==> constrains (Acts prg) (reachable prg Int B) (reachable prg Int B')*)
-bind_thm ("constrains_reachable",
- rewrite_rule [stable_def] stable_reachable RS constrains_Int);
-
(*** Specialized laws for handling invariants ***)
-Goal "invariant prg INV ==> reachable prg Int INV = reachable prg";
-bd invariant_includes_reachable 1;
-by (Blast_tac 1);
-qed "reachable_Int_INV";
-
-Goal "[| invariant prg INV; LeadsTo prg (INV Int A) A' |] \
+Goal "[| Invariant prg INV; LeadsTo prg (INV Int A) A' |] \
\ ==> LeadsTo prg A A'";
by (asm_full_simp_tac
(simpset() addsimps [LeadsTo_def, reachable_Int_INV,
Int_assoc RS sym]) 1);
-qed "invariant_LeadsToI";
+qed "Invariant_LeadsToI";
-Goal "[| invariant prg INV; LeadsTo prg A A' |] \
+Goal "[| Invariant prg INV; LeadsTo prg A A' |] \
\ ==> LeadsTo prg A (INV Int A')";
by (asm_full_simp_tac
(simpset() addsimps [LeadsTo_def, reachable_Int_INV,
Int_assoc RS sym]) 1);
-qed "invariant_LeadsToD";
+qed "Invariant_LeadsToD";
(*** Introduction rules: Basis, Trans, Union ***)
@@ -42,9 +32,6 @@
by (blast_tac (claset() addIs [psp_stable2, stable_reachable]) 1);
qed "leadsTo_imp_LeadsTo";
-(* ensures (Acts prg) A B ==> LeadsTo prg A B *)
-bind_thm ("LeadsTo_Basis", leadsTo_Basis RS leadsTo_imp_LeadsTo);
-
Goal "[| LeadsTo prg A B; LeadsTo prg B C |] ==> LeadsTo prg A C";
by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1);
by (blast_tac (claset() addIs [leadsTo_Trans]) 1);
@@ -138,33 +125,37 @@
qed "LeadsTo_weaken";
-(** More rules using the premise "invariant prg" **)
+(** More rules using the premise "Invariant prg" **)
-Goal "[| invariant prg INV; \
-\ constrains (Acts prg) (INV Int (A-A')) (A Un A'); \
+Goalw [LeadsTo_def, Constrains_def]
+ "[| Constrains prg (A-A') (A Un A'); transient (Acts prg) (A-A') |] \
+\ ==> LeadsTo prg A A'";
+by (rtac (ensuresI RS leadsTo_Basis) 1);
+by (blast_tac (claset() addIs [transient_strengthen]) 2);
+by (blast_tac (claset() addIs [constrains_weaken]) 1);
+qed "LeadsTo_Basis";
+
+Goal "[| Invariant prg INV; \
+\ Constrains prg (INV Int (A-A')) (A Un A'); \
\ transient (Acts prg) (INV Int (A-A')) |] \
\ ==> LeadsTo prg A A'";
-br invariant_LeadsToI 1;
-ba 1;
-by (rtac (ensuresI RS LeadsTo_Basis) 1);
-by (ALLGOALS
- (full_simp_tac (simpset() addsimps [Int_Diff, Int_Un_distrib RS sym,
- Diff_Int_distrib RS sym])));
-be invariantE 1;
-by (blast_tac (claset() addSDs [stable_constrains_Int]
- addIs [constrains_weaken]) 1);
-qed "invariant_LeadsTo_Basis";
+by (rtac Invariant_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 "[| invariant prg INV; \
+Goal "[| Invariant prg INV; \
\ LeadsTo prg A A'; id: Acts prg; \
\ INV Int B <= A; INV Int A' <= B' |] \
\ ==> LeadsTo prg B B'";
-br invariant_LeadsToI 1;
-ba 1;
-bd invariant_LeadsToD 1;
-ba 1;
+by (rtac Invariant_LeadsToI 1);
+by (assume_tac 1);
+by (dtac Invariant_LeadsToD 1);
+by (assume_tac 1);
by (blast_tac (claset()addIs [LeadsTo_weaken]) 1);
-qed "invariant_LeadsTo_weaken";
+qed "Invariant_LeadsTo_weaken";
(*Set difference: maybe combine with leadsTo_weaken_L??
@@ -250,43 +241,39 @@
(** PSP: Progress-Safety-Progress **)
(*Special case of PSP: Misra's "stable conjunction". Doesn't need id:Acts. *)
-Goal "[| LeadsTo prg A A'; stable (Acts prg) B |] \
-\ ==> LeadsTo prg (A Int B) (A' Int B)";
-by (asm_full_simp_tac (simpset() addsimps [LeadsTo_def, Int_assoc RS sym,
- psp_stable]) 1);
+Goal
+ "[| LeadsTo prg A A'; Stable prg B |] ==> LeadsTo prg (A Int B) (A' Int B)";
+by (full_simp_tac (simpset() addsimps [LeadsTo_def, Stable_eq_stable]) 1);
+by (dtac psp_stable 1);
+by (assume_tac 1);
+by (asm_full_simp_tac (simpset() addsimps Int_ac) 1);
qed "PSP_stable";
-Goal "[| LeadsTo prg A A'; stable (Acts prg) B |] \
+Goal "[| LeadsTo prg A A'; Stable prg B |] \
\ ==> LeadsTo prg (B Int A) (B Int A')";
by (asm_simp_tac (simpset() addsimps (PSP_stable::Int_ac)) 1);
qed "PSP_stable2";
-
-Goal "[| LeadsTo prg A A'; constrains (Acts prg) B B'; id: Acts prg |] \
+Goalw [LeadsTo_def, Constrains_def]
+ "[| LeadsTo prg A A'; Constrains prg B B'; id: Acts prg |] \
\ ==> LeadsTo prg (A Int B) ((A' Int B) Un (B' - B))";
-by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1);
-by (dtac psp 1);
-by (etac constrains_reachable 1);
-by (etac leadsTo_weaken 2);
-by (ALLGOALS Blast_tac);
+by (blast_tac (claset() addDs [psp] addIs [leadsTo_weaken]) 1);
qed "PSP";
-Goal "[| LeadsTo prg A A'; constrains (Acts prg) B B'; id: Acts prg |] \
+Goal "[| LeadsTo prg A A'; Constrains prg B B'; id: Acts prg |] \
\ ==> LeadsTo prg (B Int A) ((B Int A') Un (B' - B))";
by (asm_simp_tac (simpset() addsimps (PSP::Int_ac)) 1);
qed "PSP2";
-Goalw [unless_def]
- "[| LeadsTo prg A A'; unless (Acts prg) B B'; id: Acts prg |] \
+Goalw [Unless_def]
+ "[| LeadsTo prg A A'; Unless prg B B'; id: Acts prg |] \
\ ==> LeadsTo prg (A Int B) ((A' Int B) Un B')";
by (dtac PSP 1);
by (assume_tac 1);
-by (asm_full_simp_tac (simpset() addsimps [Un_Diff_Diff, Int_Diff_Un]) 2);
-by (asm_full_simp_tac (simpset() addsimps [Diff_Int_distrib]) 2);
-by (etac LeadsTo_Diff 2);
-by (blast_tac (claset() addIs [subset_imp_LeadsTo]) 2);
-by Auto_tac;
-qed "PSP_unless";
+by (blast_tac (claset() addIs [LeadsTo_Diff, LeadsTo_weaken,
+ subset_imp_LeadsTo]) 2);
+by (assume_tac 1);
+qed "PSP_Unless";
(*** Induction rules ***)
@@ -294,7 +281,7 @@
(** Meta or object quantifier ????? **)
Goal "[| wf r; \
\ ALL m. LeadsTo prg (A Int f-``{m}) \
-\ ((A Int f-``(r^-1 ^^ {m})) Un B); \
+\ ((A Int f-``(r^-1 ^^ {m})) Un B); \
\ id: Acts prg |] \
\ ==> LeadsTo prg A B";
by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1);
@@ -353,49 +340,42 @@
(*** Completion: Binary and General Finite versions ***)
-Goal "[| LeadsTo prg A A'; stable (Acts prg) A'; \
-\ LeadsTo prg B B'; stable (Acts prg) B'; id: Acts prg |] \
+Goal "[| LeadsTo prg A A'; Stable prg A'; \
+\ LeadsTo prg B B'; Stable prg B'; id: Acts prg |] \
\ ==> LeadsTo prg (A Int B) (A' Int B')";
-by (full_simp_tac (simpset() addsimps [LeadsTo_def]) 1);
-by (blast_tac (claset() addIs [stable_completion RS leadsTo_weaken]
- addSIs [stable_Int, stable_reachable]) 1);
+by (full_simp_tac (simpset() addsimps [LeadsTo_def, Stable_eq_stable]) 1);
+by (blast_tac (claset() addIs [stable_completion, leadsTo_weaken]) 1);
qed "Stable_completion";
-Goal "[| finite I; id: Acts prg |] \
+Goal "[| finite I; id: Acts prg |] \
\ ==> (ALL i:I. LeadsTo prg (A i) (A' i)) --> \
-\ (ALL i:I. stable (Acts prg) (A' i)) --> \
+\ (ALL i:I. Stable prg (A' i)) --> \
\ LeadsTo prg (INT i:I. A i) (INT i:I. A' i)";
by (etac finite_induct 1);
by (Asm_simp_tac 1);
-by (asm_simp_tac
- (simpset() addsimps [Stable_completion, stable_def,
- ball_constrains_INT]) 1);
+by (asm_simp_tac (simpset() addsimps [Stable_completion, ball_Stable_INT]) 1);
qed_spec_mp "Finite_stable_completion";
-Goal "[| LeadsTo prg A (A' Un C); constrains (Acts prg) A' (A' Un C); \
-\ LeadsTo prg B (B' Un C); constrains (Acts prg) B' (B' Un C); \
+Goal "[| LeadsTo prg A (A' Un C); Constrains prg A' (A' Un C); \
+\ LeadsTo prg B (B' Un C); Constrains prg B' (B' Un C); \
\ id: Acts prg |] \
\ ==> LeadsTo prg (A Int B) ((A' Int B') Un C)";
-by (full_simp_tac (simpset() addsimps [LeadsTo_def, Int_Un_distrib]) 1);
-by (dtac completion 1);
-by (assume_tac 2);
-by (ALLGOALS
- (asm_simp_tac
- (simpset() addsimps [constrains_reachable, Int_Un_distrib RS sym])));
-by (blast_tac (claset() addIs [leadsTo_weaken]) 1);
+by (full_simp_tac (simpset() addsimps [LeadsTo_def, Constrains_def,
+ Int_Un_distrib]) 1);
+by (blast_tac (claset() addIs [completion, leadsTo_weaken]) 1);
qed "Completion";
Goal "[| finite I; id: Acts prg |] \
\ ==> (ALL i:I. LeadsTo prg (A i) (A' i Un C)) --> \
-\ (ALL i:I. constrains (Acts prg) (A' i) (A' i Un C)) --> \
+\ (ALL i:I. Constrains prg (A' i) (A' i Un C)) --> \
\ LeadsTo prg (INT i:I. A i) ((INT i:I. A' i) Un C)";
by (etac finite_induct 1);
by (ALLGOALS Asm_simp_tac);
by (Clarify_tac 1);
-by (dtac ball_constrains_INT 1);
+by (dtac ball_Constrains_INT 1);
by (asm_full_simp_tac (simpset() addsimps [Completion]) 1);
qed "Finite_completion";
@@ -408,22 +388,22 @@
(*proves "constrains" properties when the program is specified*)
fun constrains_tac (main_def::cmd_defs) =
SELECT_GOAL
- (EVERY [TRY (rtac stableI 1),
+ (EVERY [REPEAT (resolve_tac [StableI, stableI,
+ constrains_imp_Constrains] 1),
rtac constrainsI 1,
full_simp_tac (simpset() addsimps [main_def]) 1,
- REPEAT_FIRST (eresolve_tac [disjE]),
+ REPEAT_FIRST (etac disjE ),
rewrite_goals_tac cmd_defs,
ALLGOALS (SELECT_GOAL Auto_tac)]);
-(*proves "ensures" properties when the program is specified*)
+(*proves "ensures/leadsTo" 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
+ (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),
+ REPEAT (ares_tac [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,
--- a/src/HOL/UNITY/SubstAx.thy Thu Aug 13 17:44:50 1998 +0200
+++ b/src/HOL/UNITY/SubstAx.thy Thu Aug 13 18:06:40 1998 +0200
@@ -6,7 +6,7 @@
LeadsTo relation: restricted to the set of reachable states.
*)
-SubstAx = WFair + Traces +
+SubstAx = WFair + Constrains +
constdefs
--- a/src/HOL/UNITY/Traces.ML Thu Aug 13 17:44:50 1998 +0200
+++ b/src/HOL/UNITY/Traces.ML Thu Aug 13 18:06:40 1998 +0200
@@ -16,59 +16,7 @@
by (ALLGOALS (blast_tac (claset() addIs (reachable.intrs @ traces.intrs))));
qed "reachable_equiv_traces";
-Goal "stable (Acts prg) (reachable prg)";
+Goal "acts <= Acts prg ==> stable acts (reachable prg)";
by (blast_tac (claset() addIs ([stableI, constrainsI] @ reachable.intrs)) 1);
qed "stable_reachable";
-(*The set of all reachable states is an invariant...*)
-Goal "invariant prg (reachable prg)";
-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 prg A ==> reachable prg <= 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 "invariant_includes_reachable";
-
-
-(** Natural deduction rules for "invariant prg A" **)
-
-Goal "[| (Init prg)<=A; stable (Acts prg) A |] ==> invariant prg A";
-by (asm_simp_tac (simpset() addsimps [invariant_def]) 1);
-qed "invariantI";
-
-Goal "invariant prg A ==> (Init prg)<=A & stable (Acts prg) A";
-by (asm_full_simp_tac (simpset() addsimps [invariant_def]) 1);
-qed "invariantD";
-
-bind_thm ("invariantE", invariantD RS conjE);
-
-
-(** Conjoining invariants **)
-
-Goal "[| invariant prg A; invariant prg B |] \
-\ ==> invariant prg (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 Thu Aug 13 17:44:50 1998 +0200
+++ b/src/HOL/UNITY/Traces.thy Thu Aug 13 18:06:40 1998 +0200
@@ -38,8 +38,4 @@
Acts "[| act: Acts prg; s : reachable prg; (s,s'): act |]
==> s' : reachable prg"
-constdefs
- invariant :: "['a program, 'a set] => bool"
- "invariant prg A == (Init prg) <= A & stable (Acts prg) A"
-
end
--- a/src/HOL/UNITY/UNITY.ML Thu Aug 13 17:44:50 1998 +0200
+++ b/src/HOL/UNITY/UNITY.ML Thu Aug 13 18:06:40 1998 +0200
@@ -21,8 +21,7 @@
qed "constrainsI";
Goalw [constrains_def]
- "[| constrains acts A A'; act: acts; (s,s'): act; s: A |] \
-\ ==> s': A'";
+ "[| constrains acts A A'; act: acts; (s,s'): act; s: A |] ==> s': A'";
by (Blast_tac 1);
qed "constrainsD";
@@ -90,8 +89,7 @@
by (Blast_tac 1);
qed "all_constrains_INT";
-Goalw [constrains_def]
- "[| constrains acts A A'; id: acts |] ==> A<=A'";
+Goalw [constrains_def] "[| constrains acts A A'; id: acts |] ==> A<=A'";
by (Blast_tac 1);
qed "constrains_imp_subset";
@@ -104,25 +102,21 @@
(*** stable ***)
-Goalw [stable_def]
- "constrains acts A A ==> stable acts A";
+Goalw [stable_def] "constrains acts A A ==> stable acts A";
by (assume_tac 1);
qed "stableI";
-Goalw [stable_def]
- "stable acts A ==> constrains acts A A";
+Goalw [stable_def] "stable acts A ==> constrains acts A A";
by (assume_tac 1);
qed "stableD";
Goalw [stable_def]
- "[| stable acts A; stable acts A' |] \
-\ ==> stable acts (A Un A')";
+ "[| stable acts A; stable acts A' |] ==> stable acts (A Un A')";
by (blast_tac (claset() addIs [constrains_Un]) 1);
qed "stable_Un";
Goalw [stable_def]
- "[| stable acts A; stable acts A' |] \
-\ ==> stable acts (A Int A')";
+ "[| stable acts A; stable acts A' |] ==> stable acts (A Int A')";
by (blast_tac (claset() addIs [constrains_Int]) 1);
qed "stable_Int";
@@ -144,15 +138,15 @@
in forward proof.*)
Goalw [constrains_def]
"[| ALL m. constrains acts {s. s x = m} (B m) |] \
-\ ==> constrains acts {s. P(s x)} (UN m. {s. P(m)} Int B m)";
+\ ==> constrains acts {s. s x : M} (UN m:M. B m)";
by (Blast_tac 1);
qed "elimination";
+
(*As above, but for the trivial case of a one-variable state, in which the
state is identified with its one variable.*)
Goalw [constrains_def]
- "[| ALL m. constrains acts {m} (B m) |] \
-\ ==> constrains acts {s. P s} (UN m. {s. P(m)} Int B m)";
+ "(ALL m. constrains acts {m} (B m)) ==> constrains acts M (UN m:M. B m)";
by (Blast_tac 1);
qed "elimination_sing";
--- a/src/HOL/UNITY/Union.ML Thu Aug 13 17:44:50 1998 +0200
+++ b/src/HOL/UNITY/Union.ML Thu Aug 13 18:06:40 1998 +0200
@@ -11,133 +11,35 @@
Maybe Join instead of Un, and JOIN for UNION
*)
-(*** Safety: constrains, stable, FP ***)
-
-Goalw [constrains_def]
- "constrains (UN i:I. acts i) A B = (ALL i:I. constrains (acts i) A B)";
-by (Blast_tac 1);
-qed "constrains_UN";
-
-Goalw [constrains_def]
- "constrains (actsF Un actsG) A B = \
-\ (constrains actsF A B & constrains actsG A B)";
-by (simp_tac (simpset() addsimps [ball_Un]) 1);
-qed "constrains_Un";
-
-(*Provable by constrains_Un and constrains_weaken, but why bother?*)
-Goalw [constrains_def]
- "[| constrains actsF A A'; constrains actsG B B' |] \
-\ ==> constrains (actsF Un actsG) (A Int B) (A' Un B')";
-by (Blast_tac 1);
-qed "constrains_Un_weaken";
-Goalw [stable_def] "stable (UN i:I. acts i) A = (ALL i:I. stable (acts i) A)";
-by (simp_tac (simpset() addsimps [constrains_UN]) 1);
-qed "stable_UN";
-
-Goalw [stable_def]
- "stable (actsF Un actsG) A = (stable actsF A & stable actsG A)";
-by (simp_tac (simpset() addsimps [constrains_Un]) 1);
-qed "stable_Un";
+Goal "Init (Join prgF prgG) = Init prgF Int Init prgG";
+by (simp_tac (simpset() addsimps [Join_def]) 1);
+qed "Init_Join";
-Goal "stable (Acts (Join prgF prgG)) A = \
-\ (stable (Acts prgF) A & stable (Acts prgG) A)";
-by (simp_tac (simpset() addsimps [Join_def, stable_Un]) 1);
-qed "stable_Join";
-
-Goalw [FP_def] "FP (UN i:I. acts i) = (INT i:I. FP (acts i))";
-by (simp_tac (simpset() addsimps [stable_UN, INTER_def]) 1);
-qed "FP_UN";
-
-
-(*** Progress: transient, ensures ***)
-
-Goalw [transient_def]
- "transient (UN i:I. acts i) A = (EX i:I. transient (acts i) A)";
-by (Simp_tac 1);
-qed "transient_UN";
+Goal "Acts (Join prgF prgG) = Acts prgF Un Acts prgG";
+by (simp_tac (simpset() addsimps [Join_def]) 1);
+qed "Acts_Join";
-Goalw [ensures_def,transient_def]
- "ensures (UN i:I. acts i) A B = \
-\ ((ALL i:I. constrains (acts i) (A-B) (A Un B)) & \
-\ (EX i:I. ensures (acts i) A B))";
-by (simp_tac (simpset() addsimps [constrains_UN]) 1);
-by Auto_tac;
-qed "ensures_UN";
-
-(*Alternative proof: simplify using ensures_def,transient_def,constrains_Un*)
-Goal "ensures (actsF Un actsG) A B = \
-\ (constrains actsF (A-B) (A Un B) & \
-\ constrains actsG (A-B) (A Un B) & \
-\ (ensures actsF A B | ensures actsG A B))";
-by (simp_tac (simpset() addcongs [conj_cong]
- addsimps [ensures_UN, Un_eq_UN,
- all_bool_eq, ex_bool_eq]) 1);
-qed "ensures_Un";
-
-(*Or a longer proof via constrains_imp_subset*)
-Goalw [stable_def, constrains_def]
- "[| stable actsF A; constrains actsG A A'; id: actsG |] \
-\ ==> constrains (actsF Un actsG) A A'";
-by (asm_simp_tac (simpset() addsimps [ball_Un]) 1);
-by (Blast_tac 1);
-qed "stable_constrains_Un";
+Goal "Init (JN i:I. prg i) = (INT i:I. Init (prg i))";
+by (simp_tac (simpset() addsimps [JOIN_def]) 1);
+qed "Init_JN";
-Goalw [Join_def]
- "[| stable (Acts prgF) A; invariant prgG A |] \
-\ ==> invariant (Join prgF prgG) A";
-by (asm_full_simp_tac (simpset() addsimps [invariant_def, stable_Un]) 1);
-by (Blast_tac 1);
-qed "stable_Join_invariant";
-
-Goal "[| stable actsF A; ensures actsG A B |] \
-\ ==> ensures (actsF Un actsG) A B";
-by (asm_simp_tac (simpset() addsimps [ensures_Un]) 1);
-by (asm_full_simp_tac (simpset() addsimps [stable_def, ensures_def]) 1);
-by (etac constrains_weaken 1);
-by Auto_tac;
-qed "ensures_stable_Un1";
+Goal "Acts (JN i:I. prg i) = (UN i:I. Acts (prg i))";
+by (simp_tac (simpset() addsimps [JOIN_def]) 1);
+qed "Acts_JN";
-Goal "[| stable (Acts prgF) A; ensures (Acts prgG) A B |] \
-\ ==> ensures (Acts (Join prgF prgG)) A B";
-by (asm_simp_tac (simpset() addsimps [Join_def, ensures_stable_Un1]) 1);
-qed "ensures_stable_Join1";
-
-(*As above, but exchanging the roles of F and G*)
-Goal "[| ensures actsF A B; stable actsG A |] \
-\ ==> ensures (actsF Un actsG) A B";
-by (stac Un_commute 1);
-by (blast_tac (claset() addIs [ensures_stable_Un1]) 1);
-qed "ensures_stable_Un2";
-
-Goal "[| ensures (Acts prgF) A B; stable (Acts prgG) A |] \
-\ ==> ensures (Acts (Join prgF prgG)) A B";
-by (asm_simp_tac (simpset() addsimps [Join_def, ensures_stable_Un2]) 1);
-qed "ensures_stable_Join2";
-
+Addsimps [Init_Join, Init_JN];
(** Theoretical issues **)
-Goalw [Join_def] "Join prgF prgG = Join prgG prgF";
-by (simp_tac (simpset() addsimps [Un_commute, Int_commute]) 1);
+Goal "Join prgF prgG = Join prgG prgF";
+by (simp_tac (simpset() addsimps [Join_def, Un_commute, Int_commute]) 1);
qed "Join_commute";
-Goalw [Join_def] "Join (Join prgF prgG) prgH = Join prgF (Join prgG prgH)";
-by (simp_tac (simpset() addsimps [Un_assoc, Int_assoc]) 1);
+Goal "Join (Join prgF prgG) prgH = Join prgF (Join prgG prgH)";
+by (simp_tac (simpset() addsimps [Join_def, Un_assoc, Int_assoc]) 1);
qed "Join_assoc";
-(**NOT PROVABLE because no "surjective pairing" for records
-Goalw [Join_def, Null_def] "id: Acts prgF ==> Join prgF Null = prgF";
-by (asm_simp_tac (simpset() addsimps [insert_absorb]) 1);
-qed "Join_Null";
-*)
-
-(**NOT PROVABLE because no "surjective pairing" for records
-Goalw [Join_def] "Join prgF prgF = prgF";
-auto();
-qed "Join_absorb";
-*)
-
(*
val field_defs = thms"program.field_defs";
@@ -149,3 +51,124 @@
val update_convs = thms"program.update_convs";
val simps = thms"program.simps";
*)
+
+
+(**NOT PROVABLE because no "surjective pairing" for records
+Goalw [Join_def, Null_def] "id: Acts prgF ==> Join prgF Null = prgF";
+by (asm_simp_tac (simpset() addsimps [insert_absorb]) 1);
+qed "Join_Null";
+*)
+
+(**NOT PROVABLE because no "surjective pairing" for records
+Goalw [Join_def] "Join prgF prgF = prgF";
+by Auto_tac;
+qed "Join_absorb";
+*)
+
+
+
+(*** Safety: constrains, stable, FP ***)
+
+Goalw [constrains_def, JOIN_def]
+ "constrains (Acts (JN i:I. prg i)) A B = \
+\ (ALL i:I. constrains (Acts (prg i)) A B)";
+by Auto_tac;
+qed "constrains_JN";
+
+(**FAILS, I think; see 5.4.1, Substitution Axiom.
+Goalw [Constrains_def]
+ "Constrains (JN i:I. prg i) A B = (ALL i:I. Constrains (prg i) A B)";
+by (simp_tac (simpset() addsimps [constrains_JN]) 1);
+by (Blast_tac 1);
+qed "Constrains_JN";
+**)
+
+Goalw [constrains_def, Join_def]
+ "constrains (Acts (Join prgF prgG)) A B = \
+\ (constrains (Acts prgF) A B & constrains (Acts prgG) A B)";
+by (simp_tac (simpset() addsimps [ball_Un]) 1);
+qed "constrains_Join";
+
+Goal "[| constrains (Acts prgF) A A'; constrains (Acts prgG) B B' |] \
+\ ==> constrains (Acts (Join prgF prgG)) (A Int B) (A' Un B')";
+by (simp_tac (simpset() addsimps [constrains_Join]) 1);
+by (blast_tac (claset() addIs [constrains_weaken]) 1);
+qed "constrains_Join_weaken";
+
+Goalw [stable_def]
+ "stable (Acts (JN i:I. prg i)) A = (ALL i:I. stable (Acts (prg i)) A)";
+by (simp_tac (simpset() addsimps [constrains_JN]) 1);
+qed "stable_JN";
+
+Goal "stable (Acts (Join prgF prgG)) A = \
+\ (stable (Acts prgF) A & stable (Acts prgG) A)";
+by (simp_tac (simpset() addsimps [stable_def, constrains_Join]) 1);
+qed "stable_Join";
+
+Goalw [FP_def] "FP (Acts (JN i:I. prg i)) = (INT i:I. FP (Acts (prg i)))";
+by (simp_tac (simpset() addsimps [stable_JN, INTER_def]) 1);
+qed "FP_JN";
+
+
+(*** Progress: transient, ensures ***)
+
+Goalw [transient_def, JOIN_def]
+ "transient (Acts (JN i:I. prg i)) A = (EX i:I. transient (Acts (prg i)) A)";
+by (Simp_tac 1);
+qed "transient_JN";
+
+Goalw [transient_def, Join_def]
+ "transient (Acts (Join prgF prgG)) A = \
+\ (transient (Acts prgF) A | transient (Acts prgG) A)";
+by (simp_tac (simpset() addsimps [bex_Un]) 1);
+qed "transient_Join";
+
+Goalw [ensures_def]
+ "ensures (Acts (JN i:I. prg i)) A B = \
+\ ((ALL i:I. constrains (Acts (prg i)) (A-B) (A Un B)) & \
+\ (EX i:I. ensures (Acts (prg i)) A B))";
+by (auto_tac (claset(),
+ simpset() addsimps [constrains_JN, transient_JN]));
+qed "ensures_JN";
+
+Goalw [ensures_def]
+ "ensures (Acts (Join prgF prgG)) A B = \
+\ (constrains (Acts prgF) (A-B) (A Un B) & \
+\ constrains (Acts prgG) (A-B) (A Un B) & \
+\ (ensures (Acts prgF) A B | ensures (Acts prgG) A B))";
+by (auto_tac (claset(),
+ simpset() addsimps [constrains_Join, transient_Join]));
+qed "ensures_Join";
+
+Goalw [stable_def, constrains_def, Join_def]
+ "[| stable (Acts prgF) A; constrains (Acts prgG) A A'; id: Acts prgG |] \
+\ ==> constrains (Acts (Join prgF prgG)) A A'";
+by (asm_simp_tac (simpset() addsimps [ball_Un]) 1);
+by (Blast_tac 1);
+qed "stable_constrains_Join";
+
+(*Premises cannot use Invariant because Stable prgF A is weaker than
+ stable (Acts prgG) A *)
+Goal "[| stable (Acts prgF) A; Init prgG <= A; stable (Acts prgG) A |] \
+\ ==> Invariant (Join prgF prgG) A";
+by (simp_tac (simpset() addsimps [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";
+
+Goal "[| stable (Acts prgF) A; ensures (Acts prgG) A B |] \
+\ ==> ensures (Acts (Join prgF prgG)) A B";
+by (asm_simp_tac (simpset() addsimps [ensures_Join]) 1);
+by (asm_full_simp_tac (simpset() addsimps [stable_def, ensures_def]) 1);
+by (etac constrains_weaken 1);
+by Auto_tac;
+qed "ensures_stable_Join1";
+
+(*As above, but exchanging the roles of F and G*)
+Goal "[| ensures (Acts prgF) A B; stable (Acts prgG) A |] \
+\ ==> ensures (Acts (Join prgF prgG)) A B";
+by (stac Join_commute 1);
+by (blast_tac (claset() addIs [ensures_stable_Join1]) 1);
+qed "ensures_stable_Join2";
+
--- a/src/HOL/UNITY/Union.thy Thu Aug 13 17:44:50 1998 +0200
+++ b/src/HOL/UNITY/Union.thy Thu Aug 13 18:06:40 1998 +0200
@@ -11,6 +11,9 @@
Union = SubstAx + FP +
constdefs
+ JOIN :: ['a set, 'a => 'b program] => 'b program
+ "JOIN I prg == (|Init = INT i:I. Init (prg i),
+ Acts = UN i:I. Acts (prg i)|)"
Join :: ['a program, 'a program] => 'a program
"Join prgF prgG == (|Init = Init prgF Int Init prgG,
@@ -19,4 +22,10 @@
Null :: 'a program
"Null == (|Init = UNIV, Acts = {id}|)"
+syntax
+ "@JOIN" :: [pttrn, 'a set, 'b set] => 'b set ("(3JN _:_./ _)" 10)
+
+translations
+ "JN x:A. B" == "JOIN A (%x. B)"
+
end