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 form.

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.


	Makarius




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.