[isabelle-dev] Remaining uses of defer_recdef?

[Larry Paulson]

It looks like there is more work to do here then. Clearly the old package is doing something clever and we need to figure out what. Sadly, it probably isn’t worth a third Ph.D.
Larry

> On 11 Jun 2015, at 06:58, Tobias Nipkow <nipkow at in.tum.de> wrote:
> 
> "Function" and "recdef" work very differently. "Function" first disambiguates the patterns, then it defines the graph of the function as an inductive definition. "Recdef" turns the definitions into a single recursion equation with case-expressions on the rhs.
> 
> Concerning the minimum number of equations: neither definition facility finds a minimum, it is too hard: Alexander Krauss. Pattern minimization problems over recursive data types. ICFP 2008.
> 
> Tobias
> 
> On 10/06/2015 23:19, Larry Paulson wrote:
>> We need to figure out how recdef does it. The minimum number of equations is mathematically fixed, so recdef must be using conditional expressions or other tricks.
>> Larry
>> 
>>> On 9 Jun 2015, at 23:07, Gerwin Klein <gerwin.klein at nicta.com.au> wrote:
>>> 
>>> I can confirm that, at least that side is simple.
>>> 
>>> Tobias’ point about avoiding exponential blowup is important, though. Might still be too early to retire recdef entirely if it is substantially better for some kinds of definitions, esp if they are in use (I think the recdef in Simpl is one of these).
>>> 
>>> Cheers,
>>> Gerwin
>>> 
>>>> On 09.06.2015, at 11:27, Thomas Sewell <thomas.sewell at nicta.com.au> wrote:
>>>> 
>>>> I've had a quick scan over the NICTA repositories. It doesn't look like
>>>> there are any live original uses of recdef. There are recdefs in a copy
>>>> of Simpl-AFP, and in some backups of historical papers.
>>>> 
>>>> Short summary, NICTA doesn't have any stakes in recdef.
>>>> 
>>>> Cheers,
>>>>   Thomas.
>>>> 
>>>> On 08/06/15 06:13, Makarius wrote:
>>>>> On Sat, 6 Jun 2015, Gerwin Klein wrote:
>>>>> 
>>>>>> 
>>>>>>> On 06.06.2015, at 21:23, Makarius <makarius at sketis.net> wrote:
>>>>>>> 
>>>>>>> (2) 'defer_recdef' which is unused in the directly visible Isabelle
>>>>>>>  universe.  So it could be deleted today.
>>>>>>> 
>>>>>>> This mailing list thread is an opportunity to point out dark matter
>>>>>>> in the Isabelle universe, where 'defer_recdef' still occurs.
>>>>>>> Otherwise I will remove it soon, lets say within 1-2 weeks.
>>>>>> 
>>>>>> Unused in our part of the dark matter universe as well.
>>>>> 
>>>>> The thread has shifted over to actual 'recdef'. Are there remaining
>>>>> uses of 'recdef' in the NICTA dark matter?
>>>>> 
>>>>> So far I always thought the remaining uses in HOL-Decision_Procs are
>>>>> only a reminder that there are other important applications.
>>>>> 
>>>>> 
>>>>>   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.
>>> _______________________________________________
>>> isabelle-dev mailing list
>>> isabelle-dev at in.tum.de
>>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>> 
>> _______________________________________________
>> isabelle-dev mailing list
>> isabelle-dev at in.tum.de
>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>> 
> 
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev