使用访问器时自动展开记录定义

Question

假设我有一个记录类型和这个类型的常量定义，例如：

record r =
  r_x :: int
  r_y :: int
  r_z :: int

definition "a ≡ ⦇r_x=1, r_y=2, r_z=3⦈"

现在我想证明一些关于a的事情，例如：

lemma "r_x a + r_y a = 3"

目前，我正在通过为不同的访问器定义简化引理来做这样的证明：

schematic_goal [simp]: "r_x a = ?x" by (simp add: a_def)
schematic_goal [simp]: "r_y a = ?x" by (simp add: a_def)
schematic_goal [simp]: "r_z a = ?x" by (simp add: a_def)

我的问题是：我能以某种方式自动导出这些引理吗？或者有没有展开定义的方法，当与访问函数一起使用时？

我不想通过添加 a_def 来证明原始引理，因为我通常只想展开 a 的用法，其中使用了访问器。

我不想使用缩写，因为这样简化器就可以处理记录中复杂的子项。

Answer 1

Isabelle2016 中没有内置的方法可以自动导出用户定义记录的选择器定理。如果您必须对同一记录类型的多个定义执行类似这样的操作，您可以按如下方式稍微自动化派生：

lemma r_sel:
  assumes "r ≡ ⦇r_x=x, r_y=y, r_z=z⦈"
  shows "r_x r = x" "r_y r = y" "r_z r = z"
using assms by(simp_all)

lemmas a_sel [simp] = r_sel[OF a_def]

引理r_sel对于每种记录类型只需要一次。然后，你用一行就得到了实例化（这里是a_sel）。对于记录转换器（即类似 f r = r(|r_x = foo|) 的东西），您可以证明相应的引理 r_upd 并导出转换器的实例。

如果您需要更多的自动化（或灵活性），您将不得不在 Isabelle/ML 中自己实现推导。通常，可以使用 Ctr_sugar 基础结构来构建此类选择器派生，但当前形式的记录包不能与 Ctr_sugar.

一起很好地工作。

使用访问器时自动展开记录定义

Automatically unfolding a record definition when accessor is used

isabelle