Check keyword arguments in remove-hyps when it operates on a (thm ...) form

[airbornemihir]

(Previously discussed on Slack.)

The tool remove-hyps (books/tools/remove-hyps.lisp) heuristically
removes hypotheses from (defthm ...) and (thm ...) forms. Under the
hood, it converts both into (defthm ...) events, which is slightly
problematic because thm and defthm have different keyword arguments
allowed. The log below shows the kind of problem that can arise.

ACL2 !>(include-book "tools/remove-hyps" :dir :system)

ACL2 !>(remove-hyps (thm (implies t (equal x x)) :instructions (prove)))
New form from REMOVE-HYPS:(THM (EQUAL X X) :INSTRUCTIONS (PROVE))

ACL2 !>(THM (EQUAL X X) :INSTRUCTIONS (PROVE)) ;; This is exactly the
;; event that remove-hyps gave us.
ACL2 Error in macro expansion: Illegal key/value args
(:INSTRUCTIONS (PROVE)) in macro expansion of
(THM (EQUAL X X) :INSTRUCTIONS (PROVE)).

ACL2 !>

[MattKaufmann]

For completeness I'll add the following comments on that same issue
from Slack. I haven't thought further about this and I don't have
near-term plans to do so.

Saturday August 29th

MattK 7:09 AM
@mihir Mehta The problem is that THM doesn't take :INSTRUCTIONS as an argument. Would you care to add this to books/system/to-do.txt?

MattK 9:18 AM
@mihir Mehta Better yet, THM could redone in terms of DEFTHM; see the comment in the definition of THM in ACL2 source file defthm.lisp.

Mihir Mehta 9:23 AM
Sure, I'll add a note in that file when I next push; it's good to know we use that file for items other than those strictly related to the prover.

MattK 1:49 PM
But actually, the fix to THM would be a prover change. I haven't thought about whether that would fix remove-hyps.

1:50
I should add: good point, @mihir Mehta. I'd prefer that books/systems/to-do.txt to be only about the ACL2 system. Items about books could go into GitHub Issues.