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])"

然后我定义了一个语法 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 的语法中没有这样的产生式。

这种情况对我来说毫无意义？ erule 是否会产生错误的目标？

Answer 1

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