如何创建适当的引理来证明 Isabelle 中的这个引理？

Question

fun intersperse :: " 'a list ⇒ 'a ⇒ 'a list" where
  "intersperse (x#y#xs) a = x#(a#(intersperse (y#xs) a))"|
  "intersperse xs _ = xs"

lemma target:"map f (intersperse xs a) = intersperse (map f xs) (f a)"

这个引理看起来很直观，但我无法让伊莎贝尔证明这个引理。我在 xs 上尝试归纳法，但大锤仍然找不到证明。然后我尝试添加辅助引理，它们都很容易证明但对证明帮助不大target。不过，我将在下面列出我的尝试：

lemma intersp_1: "interspserse (xs@[y,x]) a = (intersperse (xs@[y]) a) @ [a,x]"
...done

lemma intersp_2:"map f (intersperse (xs@[b,x]) a) = (map f (intersperse (xs@[b]) a)) @ [(f a),(f x)]"
...done

lemma intersp_3: "map f (intersperse (x#y#xs) a) = (f x)#(f a)#(map f (intersperse (y#xs) a))"
...done

作为伊莎贝尔的新学习者，我有点被困在这里。我目前能想到的唯一解决方案是提出一个适当的引理，为求解器提供足够的提示。但是我不知道如何 "appropriately" 将 target 的归纳步骤（在 xs 上应用归纳之后）分解为补充引理。归纳步骤为

goal (1 subgoal):
 1. ⋀aa xs.
       map f (intersperse xs a) = intersperse (map f xs) (f a) ⟹
       map f (intersperse (aa # xs) a) = intersperse (map f (aa # xs)) (f a)

感谢任何帮助！

Answer 1

证明如下：

lemma target: "map f (intersperse xs a) = intersperse (map f xs) (f a)"
proof (induct xs)
  case Nil
  then show ?case by simp
next
  case (Cons x xs)
  consider "xs = []" | "∃y ys. xs = y # ys" by (meson list.exhaust)
  then show ?case using Cons by (cases; auto)
qed

这里的关键是 intersperse (x # []) a 和 intersperse (x # y # ys) a 匹配不同的模式，因此通过分别考虑每种情况，大锤可以轻松找到证明。

Answer 2

这是另一个选项：使用专门的归纳规则 intersperse:

lemma target:"map f (intersperse xs a) = intersperse (map f xs) (f a)"
  by (induct "(map f xs)" "f a" arbitrary: xs rule: intersperse.induct) auto

规则intersperse.induct包含三种情况：

x#y#xs
[]
[v]

这些可以通过自动求解，因为它们符合函数可用的简化规则。

由于引理中intersperse的参数不是变量，需要显式地给induct方法，用arbitrary说明变量部分是什么.

如何创建适当的引理来证明 Isabelle 中的这个引理？

How to create appropriate lemmas to prove this lemma in Isabelle?

isabelle