[isabelle-dev] Remaining uses of defer_recdef?
makarius at sketis.net
Thu Jun 11 14:00:50 CEST 2015
On Thu, 11 Jun 2015, Larry Paulson wrote:
> 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.
What is funny about the situation of 'recdef' (Slind, HOL4) vs. 'function'
(Krauss, Isabelle/HOL) is that the HOL4 workshop at CADE-2015 mentions
that topic under Development Ideas, see also
Is that just a question of which side of the river has greener grass?
There is some chance that I will attend the workshop, but I can't say much
about that topic.
More information about the isabelle-dev