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