isabelle - 对第二个论点 Isar 的归纳

Question

inductive T :: "alpha list ⇒ bool" where
 Tε : "T []" |
 TaTb : "T l ⟹ T r ⟹ T (l @ a#(r @ [b]))"

lemma Tapp: "⟦T l;  T r⟧ ⟹ T (l@r)"
proof (induction r rule: T.induct)

我收到“无法应用初始证明方法⌂”

在 Isabelle 中，rotate_tac我猜可以使用归纳法来处理所需的论点，Isar 的等价物是什么？用“假设”和“显示”重新表述引理会有所帮助吗？

Answer 1

规则归纳总是在目标的最左边。因此，Isabelle/Isar 解决方案包括反转前提的顺序：

lemma Tapp: "⟦T r;  T l⟧ ⟹ T (l@r)"
proof (induction r rule: T.induct)
...

或者，使用assumesand shows：

lemma Tapp: assumes "T r" and "T l" shows "T (l@r)"
using assms proof (induction r rule: T.induct)
...