Hi. you can use PAT_ASSUM or PAT_X_ASSUM (or their versions in Q structure) to match an assumption and then use it as a theorem for your next tactic. PAT_ASSUM will keep the assumption untouched, while PAT_X_ASSUM will remove it, both are useful in certain cases.
For example, if there’s an assumption like ``!x. P x`` (P could be anything),
and you want to move it to goal as an antecedent, a tactic like:
Q.PAT_X_ASSUM `!x. P x` MP_TAC
or
Q.PAT_X_ASSUM `!x. P x` (fn thm => MP_TAC thm)
will do the job. In case you want to further treatment of that theorem before
calling MP_TAC, just expand above 2nd form inside the lambda-function. Check
reference manual for more details.
Hope this helps,
—Chun
> Il giorno 16 ago 2018, alle ore 18:07, Dylan Melville
> <dylanmelvi...@gmail.com> ha scritto:
>
> Is there anyway to reference a specific assumption of the current goal as a
> theorem?
> ------------------------------------------------------------------------------
> 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
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
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 hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
