# HG changeset patch # User paulson # Date 929003978 -7200 # Node ID 4700ca722bbd5e11b642727acfed6a7f1bb6d4cd # Parent 731c848f6f0cfdb4432972e43c349da4ed402c58 Always_LeadsTo_pre. Always_LeadsTo_post: new equivalences suggested by Misra diff -r 731c848f6f0c -r 4700ca722bbd src/HOL/UNITY/SubstAx.ML --- 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 ***)