Isar中的规则归纳

Question

我想在Isabelle/Isar中做一个规则归纳。我发现

proof (rule_tac P="λn. f n ≥ n ∧ f n ≥ 1" in f.induct)

或

proof (rule f.induct[of "λn. f n ≥ n ∧ f n ≥ 1"])

照我说的做。但是我如何使用"new style“Isar来写这行呢？正如您所看到的，我只是试图告诉Isabelle如何在我的函数f的归纳规则中实例化P变量。

Answer 1

我想说你已经在使用Isar风格了，因为没有apply。

您还可以使用语法f.induct[where P="λn. f n ≥ n ∧ f n ≥ 1"]。

此外，通常没有必要手动实例化P，因为统一将为您提供P。也许你必须重新制定你的目标来实现这一点。在Isar风格中，当你启动一个show时，proof之后也会发生统一，所以这是避免显式给出它的另一个选择。