访问数据类型的元素

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

在逻辑层面上，您可以使用 case 语法来解构数据类型（即 case A of mat a b c d ⇒ …）。您还可以使用 fun 或 primrec 定义自己的投影函数，例如

primrec foo1 where "foo1 (mat a b c d) = a"

在证明中，您可以使用 obtain 和 cases 命令访问值，例如

obtain a b c d where "A = mat a b c d" by (cases A) auto

至于你关于定义的问题，你可以像这样在 Isar 证明中进行局部定义：

define A where "A = mat a b c d"

然后您可以使用定理 A_def.

展开该定义

如果你想在前提或目标中使用你的定义（并在证明后在定理中展开），你可以使用 defines:

lemma
  defines "A ≡ mat a b c d"
  shows   …

同样，这为您提供了一个事实 A_def，您可以使用它来展开定义。

您还可以使用 let ?A = mat a b c d 或与 is 进行模式匹配来引入缩写。与之前的定义相反，这些只是在句法层面上，即你输入 ?A，但在解析后，你有 mat a b c d，你也会在输出中看到 mat a b c d . is 是这样工作的：

lemma
  shows "P (mat a b c d)" (is "P ?A")
proof -
  term ?A

在"assumes"之后也有效。

Answer 2

或者，可以在指定数据类型时定义自定义提取器函数。例如你的情况

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

会起作用。

然后您可以通过 mat_a x 访问 foo 值 x 的第一个元素，通过 mat_b x 访问第二个元素，依此类推。

示例：

 value "mat_a (Mat 1 2 3 4)"

"1" :: "int"

Access elements of data types