第二个参数 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)

我得到'Failed to apply initial proof method⌂'

在 Isabelle 中，可以使用 rotate_tac 我猜想通过归纳来处理所需的论点，Isar 等价物是什么？用 'assumes' & 'shows' 重新表述引理是否有帮助？

Answer 1

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

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

或者，使用 assumes 和 shows：

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

第二个参数 Isar 的归纳

Induction on second argument Isar

isabelle

isar