证明生成的列表的属性

Question

我的目标是证明包含生成模式的列表的属性。 在第一个示例中，模式只是一个 0 序列，引理pattern_0_len证明生成的列表的长度确实等于生成器函数的长度参数。

theory pattern_0
imports Main
begin
fun pattern_0 :: "nat ⇒ nat list" where
"pattern_0 0 = []" |
"pattern_0 len =  (pattern_0 (len - 1)) @ [0]"
lemma pattern_0_len [simp]: "length (pattern_0 lng) = lng"
apply(induction lng)
apply(simp)
apply(auto)
done
end

在第二个示例中，生成器生成一个由 0， 1 项组成的序列。

theory pattern_0_1
imports Main
begin
fun pattern_0_1 :: "nat ⇒ nat ⇒ nat list" where
"pattern_0_1 0 item  = []" |
"pattern_0_1 len item =  (pattern_0_1 (len - 1) (if item = 0 then 1 else 0)) @ [item]"
lemma pattern_0_1_len [simp]: "length (pattern_0_1 lng item) = lng"
apply(induction lng)
apply(simp)
apply(auto)
done
end

不幸的是，pattern_0_1_len并不能证明(简单地说，目标正是归纳步骤(，我想了解为什么不这样做。是项目参数的存在"混淆"了伊莎贝尔吗？在这种情况下可以做什么，最好不声明任何关于模式是如何生成的？

Answer 1

附加参数确实是问题所在。例如，请考虑以下子目标：

1. ⋀lng. length (pattern_0_1 lng 0) = lng ⟹ item = 0 ⟹ length (pattern_0_1 lng (Suc 0)) = lng

你看到归纳假设只适用于零，但你需要它来一个。

修复很简单：

apply(induction lng arbitrary: item)

这指示归纳法首先推广变量item。然后，归纳假设变得更加广泛适用。