这个 Isabelle 证明是否需要归纳法？

Question

我正在尝试证明生成器函数会产生某些仍然非常简单的模式。 pattern_0_1 生成交替的 0 和 1 列表。我已经成功证明对于任何长度大于 0 的列表，第一项为零。但是，应用相同的技术未能证明第二个元素始终为 1。我的猜测是这里根本不需要归纳法。对于完成第二个引理的正确方法，我将不胜感激。

fun pattern_0_1 :: "nat ⇒ nat ⇒ nat list" where
"pattern_0_1 0 item  = []" |
"pattern_0_1 len item =  item # (pattern_0_1 (len - 1) (if item = 0 then 1 else 0))"

lemma item_0_is_0 : "lng ≥ 1 ⟹ pattern_0_1 lng 0 ! 0 = 0"
  apply(induction lng)
  apply(simp)
  by auto

lemma item_1_is_1 : "lng ≥ 2 ⟹ pattern_0_1 lng 0 ! 1 = 1"
  apply(induction lng)
  apply(simp)
  sorry

Answer 1

不需要归纳法（它会是，你会展示一些关于所有偶数或所有奇数位置的信息）。在这里，案例分析就足够了，所以你得到案例0、1和> = 2。所以，你的证明可以通过

完成

apply(cases lng; cases "lng - 1"; auto)

其中第一个 cases 将是 0 或 >= 1，第二个 cases 将区分 1 和 >= 2。

这个 Isabelle 证明是否需要归纳法？

Is induction required in this Isabelle proof?

isabelle