[isabelle-dev] Remaining uses of defer_recdef?

[Makarius]

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 
http://www.cl.cam.ac.uk/~rk436/hol15/

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.


 	Makarius