Re: [isabelle] unused_thms in proofs



I had a brief look at this a while ago. My understanding is that a
(small) change might be needed.

OK, so, PThms track the derivation steps of thms. There are special
nodes which mark where thms (and their derivations) are named. This is
called through Thm.name_derivation, and via Global_Theory.name_thm.

Point is, globally-anonymous facts, such as steps in proofs, don't have
named derivations (currently). So proof term summaries will see them as
just part of the proof of the facts they result in.

Well, they could be optionally given dummy names. That would break the
usual rule that names in the PThms (other than Pure.blah) look up facts,
but would allow you to check whether they were really used.

The other option would be to check whether they were syntactically used,
of course.

Cheers,
    Thomas.

On 02/05/16 23:35, Makarius wrote:
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



________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.




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