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
Conceivably we could introduce a prefix syntax for type constraints, e.g.
[:real:]of_nat k
I’d find such a thing useful from time to time.
My personal favourite would be System-F-style type instantiation
of_nat [real] k
instead of type annotations but there are hardly any
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)
My proposal of [: :] is suggestive of typing and should be good enough,
considering that such “type casts” would seldom be necessary.
Larry
On 6 Jun 2015, at 16:06, Florian Haftmann
florian.haftm...@informatik.tu-muenchen.de wrote:
Conceivably we could introduce a prefix syntax for type
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
10 matches
Mail list logo
