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.
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:
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
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
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.
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
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
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,
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
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
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
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
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
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
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
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
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
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
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:
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
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
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
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)
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
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
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
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
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
28 matches
Mail list logo
