Always_LeadsTo_pre. Always_LeadsTo_post: new equivalences suggested by Misra

--- a/src/HOL/UNITY/SubstAx.ML	Thu Jun 10 10:38:41 1999 +0200
+++ b/src/HOL/UNITY/SubstAx.ML	Thu Jun 10 10:39:38 1999 +0200
@@ -21,19 +21,23 @@
 
 (** Conjoining an Always property **)
 
-Goal "[| F : Always C;  F : (C Int A) LeadsTo A' |]   \
-\     ==> F : A LeadsTo A'";
+Goal "F : Always INV ==> (F : (INV Int A) LeadsTo A') = (F : A LeadsTo A')";
 by (asm_full_simp_tac
     (simpset() addsimps [LeadsTo_def, Always_eq_includes_reachable,
 			 Int_absorb2, Int_assoc RS sym]) 1);
-qed "Always_LeadsToI";
+qed "Always_LeadsTo_pre";
 
-Goal "[| F : Always C;  F : A LeadsTo A' |]   \
-\     ==> F : A LeadsTo (C Int A')";
+Goal "F : Always INV ==> (F : A LeadsTo (INV Int A')) = (F : A LeadsTo A')";
 by (asm_full_simp_tac
     (simpset() addsimps [LeadsTo_eq_leadsTo, Always_eq_includes_reachable, 
 			 Int_absorb2, Int_assoc RS sym]) 1);
-qed "Always_LeadsToD";
+qed "Always_LeadsTo_post";
+
+(* [| F : Always C;  F : (C Int A) LeadsTo A' |] ==> F : A LeadsTo A' *)
+bind_thm ("Always_LeadsToI", Always_LeadsTo_pre RS iffD1);
+
+(* [| F : Always INV;  F : A LeadsTo A' |] ==> F : A LeadsTo (INV Int A') *)
+bind_thm ("Always_LeadsToD", Always_LeadsTo_post RS iffD2);
 
 
 (*** Introduction rules: Basis, Trans, Union ***)