Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Pattern matching on extended records


view this post on Zulip Email Gateway (Jan 20 2023 at 15:29):

From: Rebecca Ghidini <ghidini@in.tum.de>
Hello,

I'm trying to write a function which uses pattern matching on an
extended record.

For example, if I define the following record:

record normal_record =
t1 :: nat
t2 :: nat

I can define functions with pattern matching on the fields of the
record:

fun test1 :: "normal_record => nat"
where
"test1 ((|t1 = a, t2 = b|)) = b"

Then I define an extended record:

record extended_record = normal_record +
t3 :: nat

But when I try to define a function in the same way as before, I get an
error:

fun test2 :: "extended_record => nat"
where
"test2 ((|t1 = a, t2 = b, t3 = c|)) = b + c"

This is the error:

exception THM 0 raised (line 755 of "drule.ML"):
infer_instantiate_types: type ?'z extended_record_scheme of variable
?r
cannot be unified with type (|t3 :: nat|) of term _av4
(⋀t1 t2 t3 more. ?r = (|t1 = t1, t2 = t2, t3 = t3, … = more|) ⟹ ?C) ⟹
?C

I tried to define the function in different ways, for example using "'a
extended_record_scheme"
instead of "extended_record" or adding the "more" field explicitly, but
I always get the same error.
I also tried pattern matching with "case … of", but it doesn't work,
because record is not a datatype constructor.

Obviously I could define the function like this:

fun test4 :: "extended_record => nat"
where
"test4 rec = t2 rec + t3 rec"

But given that I am working with larger records and more complicated
functions, I was wondering if there is a more
elegant way to write this function, by using pattern matching.

Thank you,
Rebecca


Last updated: Mar 28 2024 at 12:29 UTC