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 <nip...@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.kl...@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.sew...@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 <makar...@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-...@in.tum.de >>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev >> >> _______________________________________________ >> isabelle-dev mailing list >> isabelle-...@in.tum.de >> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev >> > > _______________________________________________ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
