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

On Thu, 11 Jun 2015, Larry Paulson wrote: We must go forward and not back. Just to conclude the original question on this thread: 'defer_recdef' is unused, untested, unmaintained. So it falls under the normal garbage-collection of source code. I will remove it next week or so, unless ther

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 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 recursi

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?

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 wrote: "Function" and "re

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 wrote: > > "Function" and "recdef" work very differently. "Function"

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 e

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 wrote: > > I can confirm that, at least that side is simple. > > Tobias’ point abou

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 t

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?

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 to.

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 domai

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

On Sat, 6 Jun 2015, Gerwin Klein wrote: On 06.06.2015, at 21:23, Makarius 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 Isabelle universe, wh

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 t

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 i

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

>> On 7 Jun 2015, at 07:38, Dmitriy Traytel > > 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 conv

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 experie

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

> On 7 Jun 2015, at 07:38, Dmitriy Traytel 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 unconditional patter

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?

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 "spiri

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?

> On 6 Jun 2015, at 19:37, Tobias Nipkow 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 talking about thi

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 equa

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 > wrote: > >> The reason for the continued existence of recdef is that function can >> caus

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 > wil

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 s

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?

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 > wrote: > >> Cleaning up some obscure

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

[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