Re: [isabelle] unused_thms in proofs



This would definitely be useful! +1 - chris

On 04/29/2016 11:11 AM, Gerwin Klein wrote:
> +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.