Re: [isabelle] unused_thms in proofs
On Mon, 2 May 2016, Jasmin Blanchette wrote:
That's a good idea. I don't know whether the current implementation of
reasoning actually supports such a command. Makarius might know better.
But if it does, I guess that this could be a reasonably-sized project
for a student.
For Sledgehammer (esp. MaSh), we had to do some fishing around in the
local context to retrieve facts in Isar proofs. I am under the
impression that all the information we would need is stored in some
I think the main challenge are such questions about internal naming of
derivations (the infamous PThm nodes). I've never fully understood the
scheme introduced by Larry Paulson and reformed by Stefan Berghofer, more
than 15 years ago. Nonetheless, I've tinkered with it out of necessity, to
make parallel proof checking work.
It is definitely worth revisiting all that, and unifying it with the
treatment in Sledgehammer.
Afterwards, a student project to wrap it up as PIDE print function etc.
would be rather trivial. Still worth to learn how that works, but from 6
weeks only 1 is probably required.
This archive was generated by a fusion of
Pipermail (Mailman edition) and