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 (mythtactic o ASSUME) `assumption`
where mythtactic is a continuation/thm_tactic such as mp_tac, strip_assume_tac,
drule.
By using this version, you can write the assumption between single quotations,
and hopefully not need to write quite so many type annotations.
If you want to remove the assumption and work on it with mythtactic, then use
Q.UNDISCH_THEN `assumption` mythtactic
There's probably an argument for defining the first form above, perhaps as
Q.ASSUME_THEN, so that you could write
Q.ASSUME_THEN `assumption` mythtactic
Michael
On 17/8/18, 05:20, "Mario Xerxes Castelán Castro" <marioxcc...@yandex.com>
wrote:
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 produced where the assumption was not eliminated).
On 16/08/18 11:07, Dylan Melville wrote:
> 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
