Re: [isabelle-dev] Remaining uses of defer_recdef?

2015-06-11 Thread 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 nip...@in.tum.de wrote: Function and recdef work very differently.

Re: [isabelle-dev] Remaining uses of defer_recdef?

2015-06-11 Thread 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 nip...@in.tum.de wrote:

Re: [isabelle-dev] Remaining uses of defer_recdef?

2015-06-11 Thread Tobias Nipkow
On 11/06/2015 14:00, Makarius wrote: Is that just a question of which side of the river has greener grass? Function does a number of things very nicely, eg nested recursion and partiality. That is worth taking on board. Tobias smime.p7s Description: S/MIME Cryptographic Signature

Re: [isabelle-dev] Remaining uses of defer_recdef?

2015-06-11 Thread Larry Paulson
Absolutely, totally. We must go forward and not back. Larry On 11 Jun 2015, at 13:27, Tobias Nipkow nip...@in.tum.de wrote: On 11/06/2015 14:00, Makarius wrote: Is that just a question of which side of the river has greener grass? Function does a number of things very nicely, eg nested

Re: [isabelle-dev] Remaining uses of defer_recdef?

2015-06-10 Thread Larry Paulson
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.

Re: [isabelle-dev] Remaining uses of defer_recdef?

2015-06-10 Thread Tobias Nipkow
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

Re: [isabelle-dev] Remaining uses of defer_recdef?

2015-06-09 Thread Gerwin Klein
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

Re: [isabelle-dev] Remaining uses of defer_recdef?

2015-06-08 Thread Thomas Sewell
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,

Re: [isabelle-dev] Remaining uses of defer_recdef?

2015-06-08 Thread Andreas Lochbihler
On 06/06/15 17:11, Florian Haftmann wrote: So are there any experience reports that the combinatorial explosion in pattern matching in fun/function had to be worked around somehow? Or do we have to conclude that the pattern complexity of the applications in src/HOL/Decision_Procs is indeed

Re: [isabelle-dev] Remaining uses of defer_recdef?

2015-06-08 Thread Tobias Nipkow
A frequent use case is this: you have 5-10 interesting patterns where stuff happens and an otherwise pattern with a simple rhs. In that case you do want to write those 5-10 patterns explicitly and let the definition facility take care of the hundreds of patterns that the default case expands

Re: [isabelle-dev] Remaining uses of defer_recdef?

2015-06-07 Thread Larry Paulson
On 7 Jun 2015, at 07:38, Dmitriy Traytel tray...@in.tum.de wrote: I'm not sure if this is something for the repository though, since it has a factor of 2 impact on the build-time: Thanks for investigating. But how do we explain this? Possibly “fun” insists on converting on creating

Re: [isabelle-dev] Remaining uses of defer_recdef?

2015-06-07 Thread Florian Haftmann
So are there any experience reports that the combinatorial explosion in pattern matching in fun/function had to be worked around somehow? Or do we have to conclude that the pattern complexity of the applications in src/HOL/Decision_Procs is indeed domain-specific? I have some experience with

Re: [isabelle-dev] Remaining uses of defer_recdef?

2015-06-07 Thread Florian Haftmann
On 7 Jun 2015, at 07:38, Dmitriy Traytel tray...@in.tum.de mailto:tray...@in.tum.de wrote: I'm not sure if this is something for the repository though, since it has a factor of 2 impact on the build-time: Thanks for investigating. But how do we explain this? Possibly “fun” insists on

Re: [isabelle-dev] Remaining uses of defer_recdef?

2015-06-07 Thread Florian Haftmann
I could not believe that recdef could not be replaced by fun, so here is the patch that removes usages of recdef from Decision_Procs. The proof rules that come out of the function package are fine (one just needs a few split_format (complete) attributes in a few places). I'm not sure if

Re: [isabelle-dev] Remaining uses of defer_recdef?

2015-06-07 Thread Larry Paulson
I suggest looking for ways for users to avoid exponential blowup. Presumably this means avoiding deeply nested patterns in favour of conditional expressions in some cases. Such a formalisation might be easier to reason with too, who wants an induction rule with hundreds of cases? But coming up

Re: [isabelle-dev] Remaining uses of defer_recdef?

2015-06-07 Thread Florian Haftmann
I could not believe that recdef could not be replaced by fun, so here is the patch that removes usages of recdef from Decision_Procs. The proof rules that come out of the function package are fine (one just needs a few split_format (complete) attributes in a few places). Let me emphasize this

Re: [isabelle-dev] Remaining uses of defer_recdef?

2015-06-07 Thread Makarius
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

Re: [isabelle-dev] Remaining uses of defer_recdef?

2015-06-07 Thread Dmitriy Traytel
Hi, I could not believe that recdef could not be replaced by fun, so here is the patch that removes usages of recdef from Decision_Procs. The proof rules that come out of the function package are fine (one just needs a few split_format (complete) attributes in a few places). I'm not sure if

Re: [isabelle-dev] Remaining uses of defer_recdef?

2015-06-06 Thread Makarius
On Sat, 6 Jun 2015, Larry Paulson wrote: I’d be happy to see the complete phasing out of TFL. It’s had its day. It was always a tricky thing to maintain. I’m amazed that it still works despite all of the many fundamental changes to system APIs. There are actually two remaining parts of TFL:

Re: [isabelle-dev] Remaining uses of defer_recdef?

2015-06-06 Thread Tobias Nipkow
The reason for the continued existence of recdef is that function can cause a combinatorial explosion the way it compiles pattern matches. I just tried Cooper.thy and changing one of the recdefs to function makes Isabelle go blue (purple) in the face until one gives up. Hardware alone will not

Re: [isabelle-dev] Remaining uses of defer_recdef?

2015-06-06 Thread Florian Haftmann
The reason for the continued existence of recdef is that function can cause a combinatorial explosion the way it compiles pattern matches. I just tried Cooper.thy and changing one of the recdefs to function makes Isabelle go blue (purple) in the face until one gives up. Hardware alone will

Re: [isabelle-dev] Remaining uses of defer_recdef?

2015-06-06 Thread Amine Chaieb
I remember trying to convert Cooper's as well as other Decision proc's recdefs to fun, also with the help of Alex but gave up at some point. I think the killer at the time was rather the induction principle and not the simp rules. The one derived by recdef really fits the definition and

Re: [isabelle-dev] Remaining uses of defer_recdef?

2015-06-06 Thread Dmitriy Traytel
Hi Florian, On 06.06.2015 17:11, Florian Haftmann wrote: The reason for the continued existence of recdef is that function can cause a combinatorial explosion the way it compiles pattern matches. I just tried Cooper.thy and changing one of the recdefs to function makes Isabelle go blue (purple)

Re: [isabelle-dev] Remaining uses of defer_recdef?

2015-06-06 Thread Larry Paulson
Pattern matching is a convenience, and can always be eliminated manually. Is there really no reasonable way to re-express the definitions in Cooper.thy? Larry On 6 Jun 2015, at 16:11, Florian Haftmann florian.haftm...@informatik.tu-muenchen.de wrote: The reason for the continued existence

Re: [isabelle-dev] Remaining uses of defer_recdef?

2015-06-06 Thread Tobias Nipkow
On 06/06/2015 20:11, Larry Paulson wrote: Pattern matching is a convenience, and can always be eliminated manually. Is there really no reasonable way to re-express the definitions in Cooper.thy? You can always turn all patterns of the lhs into cases on the rhs and derive the individual

Re: [isabelle-dev] Remaining uses of defer_recdef?

2015-06-06 Thread Larry Paulson
On 6 Jun 2015, at 19:37, Tobias Nipkow nip...@in.tum.de wrote: You can always turn all patterns of the lhs into cases on the rhs and derive the individual equations as lemmas. You also need to derive an induction principle. I would rather keep recdef than do all that by hand. Are we

Re: [isabelle-dev] Remaining uses of defer_recdef?

2015-06-05 Thread Florian Haftmann
Cleaning up some obscure corners of the system, I've come across the old defer_recdef command. Are there any remaining uses of this historical relic? I don't see any in the main Isabelle repository + AFP. Some years ago the idea was to let recdef stand as long as there are examples in the

Re: [isabelle-dev] Remaining uses of defer_recdef?

2015-06-05 Thread Larry Paulson
I’d be happy to see the complete phasing out of TFL. It’s had its day. It was always a tricky thing to maintain. I’m amazed that it still works despite all of the many fundamental changes to system APIs. Larry On 5 Jun 2015, at 21:42, Florian Haftmann

[isabelle-dev] Remaining uses of defer_recdef?

2015-06-03 Thread Makarius
Cleaning up some obscure corners of the system, I've come across the old defer_recdef command. Are there any remaining uses of this historical relic? I don't see any in the main Isabelle repository + AFP. Makarius ___ isabelle-dev mailing