Access elements of data types

Question

Is it possible in Isabelle to access the individual elements of a data type? Let's say I have the following data type:

datatype foo = mat int int int int 

and (e.g. in a lemma)

fixes A :: foo

Is it possible to access the single elements of A? Or alternatively, fix the single elements (fix a b c d :: int) and then define A as mat a b c d?

Answer 1

Alternatively it is possible to define custom extractor functions when specifying a data type. In your case, for example

datatype foo = Mat (mat_a : int) (mat_b : int) (mat_c : int) (mat_d : int)

would work.

Then you can access the first element of a foo value x by mat_a x, the second by mat_b x, and so on.

Example:

 value "mat_a (Mat 1 2 3 4)"

"1" :: "int"