Re: [isabelle] unused_thms in proofs



Absolutely.


On 29/04/16 10:48, Tobias Nipkow wrote:


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

Tobias

Cheers,
Andreas








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