isabelle - 数据类型的访问元素

Question

Isabelle 是否可以访问数据类型的各个元素？假设我有以下数据类型：

datatype foo = mat int int int int 

和（例如在引理中）

fixes A :: foo

是否可以访问 A 的单个元素？或者，修复单个元素 ( fix a b c d :: int)，然后定义A为mat a b c d?

Answer 1

Answer 2

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"