Может ли Эруле создать ошибочные подцели?

Question

У меня есть следующая грамматика, определенная в Изабель:

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.

Эта ситуация не имеет смысла для меня? Создает ли Эруле ложные цели?

Answer 1

Правила индукции, такие как T.induct, обычно должны использоваться с induction методом доказательства, а не erule. Метод induction гарантирует, что все утверждение становится частью индуктивных утверждений, тогда как при erule только заключение является частью индуктивного аргумента; другие предположения в основном игнорируются для индукции. Это можно увидеть в последнем целевом состоянии, где в индуктивном утверждении указан целевой параметр xsa, тогда как важнейшее предположение count xs Open = count xs Close все еще говорит о переменной xs. Итак, шаг доказательства должен быть apply(induction rule: T.induct). Тогда есть шанс доказать это утверждение.