Also, if ever giving a pattern to match your chosen assumption doesn't
suit, you can use ASSUM_LIST - which gives you a list of all assumptions
to use in constructing your next tactic, and you can pick one of that
list.
But note the caveat in the doc page about relying on the order of
assumptions.
Cheers,
Jeremy
On 08/17/2018 03:58 AM, Chun Tian (binghe) wrote:
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
------------------------------------------------------------------------------
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
------------------------------------------------------------------------------
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
