Isabelle记录更新重排问题：auto为何无法证明字段更新可交换？

首先给出示例代码：

record r =
  a :: nat
  b :: nat
  c :: nat

lemma "P (r ⦇ a := 2, b := 3 ⦈) ⟹ P (r ⦇b := 3, a := 2⦈)"
  apply auto ― ‹doesn't work›
  by (metis r.simps(5) r.simps(6) r.surjective)

为什么auto无法识别不同字段的更新操作可交换？ #

• auto的推理依赖默认的简化规则集（simpset）和经典逻辑规则，而不同字段的记录更新可交换这个性质，并没有被默认包含在这些规则里。Isabelle的记录更新是函数式实现的，虽然逻辑上顺序不影响结果，但这个等价性需要结合记录的满射性和字段更新的底层公理才能推导，auto不会主动触发这类跨公理的组合推理。
• auto的核心是快速应用已有规则完成简化或证明，对于这种需要多个底层公理配合才能得出的结论，不在它默认的处理范围内。

如何让Isabelle具备该推理能力？ #

有两种实用方法：

1. 自定义简化引理并加入规则集 #

先证明通用的不同字段更新交换引理，然后将其加入简化规则集，这样auto就能自动识别并应用这个等价性：

-- 证明通用的两字段更新交换引理
lemma record_update_swap:
  "⦇ r with a := x, b := y ⦈ = ⦇ r with b := y, a := x ⦈"
  by (metis r.simps(5) r.simps(6) r.surjective)

-- 将引理添加到默认简化规则集
declare record_update_swap[simp]

-- 现在auto可以自动完成证明
lemma "P (r ⦇ a := 2, b := 3 ⦈) ⟹ P (r ⦇b := 3, a := 2⦈)"
  apply auto
  done

如果需要覆盖任意不同字段的情况，可以进一步泛化这个引理，适配更多记录类型和字段组合。

2. 显式补充记录相关简化规则 #

Isabelle为记录自动生成了一组底层简化规则record_simps，结合记录的满射性规则，手动补充给auto即可完成推理：

lemma "P (r ⦇ a := 2, b := 3 ⦈) ⟹ P (r ⦇b := 3, a := 2⦈)"
  apply (auto simp add: record_simps r.surjective)
  done

这种方式不需要自定义引理，但每次证明类似问题时都需要手动指定补充规则。

内容的提问来源于stack exchange，提问作者Mathieu Paturel