Re: [isabelle] unused_thms in proofs

On 29/04/2016 10:39, Andreas Lochbihler wrote:
Dear all,

I have written several Isar-style proofs of lemmas each of which is quite long
(>1000 lines). As the proofs have evolved over time, I am not sure any more that
I use every intermediate result to prove the result. Is there any convenient way
to find out whether there are some unused intermediate steps?

I tried to use unused_thms before the final qed, but this gives me only
top-level theorems, not intermediate (named) facts stated with "have". I could
imagine a diagnostic command that one issues before the qed and it lists all the
unused intermediate facts since the last "next" or "proof" command on the same
level. If this is not available, could this be implemented and how hard would it
be? Would anyone else find such a functionality useful?

I would. Especially if it is integrated with the interface and marks such unused local facts (on demand).



Attachment: smime.p7s
Description: S/MIME Cryptographic Signature

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