--- 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);