erule会产生错误的子目标吗

Question

我在Isabelle中定义了以下语法：

inductive S where
S_empty: "S []" |
S_append: "S xs ⟹ S ys ⟹ S (xs @ ys)" |
S_paren: "S xs ⟹ S (Open # xs @ [Close])"

然后我定义了一个gramar T，它在概念上只添加了以下规则：

T_left: "T xs ⟹ T (Open # xs)"

然后我试图证明以下定理：

theorem T_S:
"T xs ⟹ count xs Open = count xs Close ⟹ S xs"
apply(erule T.induct)
apply(simp add: S_empty)
apply(simp add: S_append)
apply(simp add: S_paren)
oops

令我惊讶的是，最后的目标似乎是错误的：

⋀xsa. count xs Open = count xs Close ⟹ T xsa ⟹ S xsa ⟹ S (Open # xsa)

所以这里S (Open # xsa)不能成立，因为在假定S xsa的语法中没有这样的生成。

这种情况对我来说毫无意义？埃鲁尔创造的目标是假的吗？

Answer 1

像T.induct这样的归纳规则通常应该与induction证明方法一起使用，而不是与erule一起使用。induction方法确保整个陈述成为归纳陈述的一部分，而erule方法只有结论是归纳论点的一部分；归纳法基本上忽略了其他假设。这可以在最后一个目标状态中看到，其中归纳语句涉及目标参数xsa，而关键假设count xs Open = count xs Close仍然涉及变量xs。因此，证明步骤应该是apply(induction rule: T.induct)。那么就有机会证明这一说法。