(cc'ing isabelle-dev)
On 06/30/2011 11:11 AM, Gerwin Klein wrote:
Hi Tom,
sounds like an easy addition to the record package (see below).
Can you think of anything speaking against generating this declaration?
Cheers,
Gerwin
I am not sure if it would generate bloat for very large records... But
on the other hand, it is just one constructor. Makarius or Stefan might
be able to comment. At least, I would be surprised if nobody had thought
about this idea before.
If there are no reasons against it, it would certainly be nice, as it
would also allow record patterns in case expressions, not just "fun"
definitions.
Alex
On 30/06/2011, at 10:38 AM, Alexander Krauss wrote:
Hi Anh,
record Foo =
x :: "nat"
y :: "nat"
fun bar :: "Foo => nat => nat"
where
"bar (| x = n1, y = n2|) z = compute n1 n2 z"
But it doesn't allow the record pattern there. I got the error
"Non-constructor pattern not allowed in sequential mode".
The fun command does not support record patterns, just datatype constructors
(even though records are much like datatypes).
How can we use record patterns in functions like the one above?
There are two possibilities: Either you use functions general patterns, which gives you
some manual (but trivial) proving work to do; see HOL/ex/Fundefs.thy for an example. Or,
which is probably easier, you use the "rep_datatype" command to instruct the
system to regard the record type you defined as a datatype: After the record definition,
do
rep_datatype Foo_ext
by (fact Foo.ext_induct) (fact Foo.ext_inject)
Then, the function definition works out of the box.
Someone who knows more about records can probably explain why this declaration
isn't issued internally by default...
Alex
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
