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

[Alexander Krauss]

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