Hi, OK, great, thanks! It seems that EQ_IMP_RULE is the key ... (I’ll remember FORALL_AND_THM too)
P. S. Just after my post, I found an ugly solution too ^_^: GEN_ALL (MATCH_MP AND1_THM (SPEC_ALL (ONCE_REWRITE_RULE [EQ_IMP_THM] th)) —Chun > Il giorno 22 gen 2017, alle ore 23:19, [email protected] ha > scritto: > > Try something like GEN_ALL o #1 o EQ_IMP_RULE o SPEC_ALL. > > Or following up on your rewriting approach, you might also rewrite with > > SIMP_RULE bool_ss [FORALL_AND_THM] > > to move the universal quantification in over the conjunctions. (This has the > issue that it might disturb other universal quantifications within the P or > Q…) > > Michael > > On 23/1/17, 09:08, "Chun Tian (binghe)" <[email protected]> wrote: > > Hi, > > suppose I have the following theorem: > > th = > |- !x. P x = Q x > > How can I convert it into this one? > > |- !x. P x ==> Q x > > As the first step, I tried "ONCE_REWRITE_RULE [EQ_IMP_THM] th", and got > this: > > |- !x. (P x ==> Q x) /\ (Q x ==> P x) > > But then I don’t know how to benefit from AND1_THM (|- ∀t1 t2. t1 ∧ t2 ⇒ > t1), or there’s a better method to do the whole thing? > > Regards, > > Chun Tian > > >
signature.asc
Description: Message signed with OpenPGP using GPGMail
------------------------------------------------------------------------------ Check out the vibrant tech community on one of the world's most engaging tech sites, SlashDot.org! http://sdm.link/slashdot
_______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
