Mario is right if you are happy to write the whole assumption out (as he
describes), or if you have your hands on the relevant term some other way.
If you also want the benefit of parsing a string into a term in the context of
the current goal, you might also want to try
QTY_TAC bool
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
In HOL4 you can use the “ASSUME” primitive inference rule, passing the
same term as it appears in the hypotheses (up to α-conversion). Make
sure that the types of the constants are the same, for otherwise this
will fail (it will be either detected and an exception is raised or a
theorem is
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
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
