Hi Yaqing,
I could enhance my Tactician tool to do this sort of thing. In fact, a
new release is long overdue, so I'll try to find the time to do this
soon (but am too busy in the next few weeks).
But you say you're looking for a quick patch. One approach would be to
apply the original conversion, and then try taking out members of the
theorem list and keeping the same result. I can probably knock up the
code for this tonight.
Note that this idea gives you something a slightly different from
removing unused theorems - it's a list that removes any unused theorems
plus potentially others that have no effect on the overall result
(whether the original rewrite used them or not). Which of these two are
you interested in (or does it make no difference to you)?
Best,
Mark.
On 31/01/2018 12:49, Yaqing Jiang wrote:
Sometimes when I'm using REWRITE_CONV[th1;th2...] to rewrite a term,
not all the theorems in th1,th2,... are used.
Anyone knows if there is a simple way of finding out which theorems
were actually applied?
I know there are methods that tracking the entire dependencies of a
proven theorem, but a small patch of REWRITE_CONV would work for me.
By the way, I'm using HOL Light, so things might be different. I
should be able to adapt the idea to HOL Light.
Best regards,
Yaqing
------------------------------------------------------------------------------
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
