--- a/src/HOL/UNITY/SubstAx.ML Tue Oct 13 10:50:56 1998 +0200
+++ b/src/HOL/UNITY/SubstAx.ML Tue Oct 13 10:55:33 1998 +0200
@@ -92,7 +92,7 @@
by (blast_tac (claset() addIs [LeadsTo_Union]) 1);
qed "LeadsTo_Un";
-Goal "[| A <= B |] ==> LeadsTo F A B";
+Goal "A <= B ==> LeadsTo F A B";
by (simp_tac (simpset() addsimps [LeadsTo_def]) 1);
by (blast_tac (claset() addIs [subset_imp_leadsTo]) 1);
qed "subset_imp_LeadsTo";
@@ -178,11 +178,8 @@
\ LeadsTo F A A'; \
\ INV Int B <= A; INV Int A' <= B' |] \
\ ==> LeadsTo F B B'";
-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);
+by (REPEAT (ares_tac [Invariant_includes_reachable,
+ reachable_LeadsTo_weaken] 1));
qed "Invariant_LeadsTo_weaken";
@@ -269,9 +266,8 @@
(** PSP: Progress-Safety-Progress **)
-(*Special case of PSP: Misra's "stable conjunction". Doesn't need id:Acts. *)
-Goal
- "[| LeadsTo F A A'; Stable F B |] ==> LeadsTo F (A Int B) (A' Int B)";
+(*Special case of PSP: Misra's "stable conjunction"*)
+Goal "[| LeadsTo F A A'; Stable F B |] ==> LeadsTo F (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);
--- a/src/HOL/UNITY/Union.ML Tue Oct 13 10:50:56 1998 +0200
+++ b/src/HOL/UNITY/Union.ML Tue Oct 13 10:55:33 1998 +0200
@@ -163,7 +163,7 @@
qed "ensures_Join";
Goalw [stable_def, constrains_def, Join_def]
- "[| stable (Acts F) A; constrains (Acts G) A A'; Id: Acts G |] \
+ "[| stable (Acts F) A; constrains (Acts G) A A' |] \
\ ==> constrains (Acts (F Join G)) A A'";
by (asm_simp_tac (simpset() addsimps [ball_Un]) 1);
by (Blast_tac 1);
@@ -172,7 +172,7 @@
(*Premises cannot use Invariant because Stable F A is weaker than
stable (Acts G) A *)
Goal "[| stable (Acts F) A; Init G <= A; stable (Acts G) A |] \
-\ ==> Invariant (F Join G) A";
+\ ==> Invariant (F Join G) A";
by (simp_tac (simpset() addsimps [Invariant_def, Stable_eq_stable,
stable_Join]) 1);
by (force_tac(claset() addIs [stable_reachable, stable_Int],