Isabelle 记录更新重新排序

Question

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不起作用，这么简单的证明我必须调用sledgehammer？ Isabelle 不应该能够弄清楚，如果更新字段不同，它们就会通勤吗？

有办法教伊莎贝尔这个吗？

Answer 1

标准的“启发式”是，您通常可以通过注入

cases

或

induct

调用来增加记录（以及产品数据类型）的自动方法的范围。这也适用于这种情况：

lemma "P (rec ⦇ a := 2, b := 3 ⦈) ⟹ P (rec ⦇b := 3, a := 2⦈)"
  apply (cases rec)
  (* proof state:
    ⋀a b c more.
       P (rec⦇a := 2, b := 3⦈) ⟹
       rec = ⦇a = a, b = b, c = c, … = more⦈ ⟹ P (rec⦇b := 3, a := 2⦈)
  *)
  by simp

【我得跑去开会了。今天晚些时候，我将扩展有关其他子问题/记录的一般问题的答案。]