Re: [isabelle] Error: Non-constructor pattern not allowed in sequential mode



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





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.