Re: [isabelle] unused_thms in proofs



+1!

Gerwin


> On 29.04.2016, at 18:58, Manuel Eberl <eberlm at in.tum.de> wrote:
>
> 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
>>>
>>>
>>
>
>


________________________________

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.