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

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?

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?

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?

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?

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?

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?

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?

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?

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?

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?

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?

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?

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?

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?

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?

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?

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?

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?

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?

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?

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?

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?

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?

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?

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?

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?

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?

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?

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