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

做我想做的事。但是我怎么能用“新风格”伊萨尔写那行呢？如您所见，我只是想告诉 Isabelle 如何P在我的函数的归纳规则中实例化变量f。

Answer 1

我会说您已经在使用 Isar 样式，因为没有apply.

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

此外，通常不需要P手动实例化，因为统一会给你P. 也许您必须重新制定目标才能实现这一目标。proof在 Isar 样式中，在您启动 a之后也会发生统一show，因此这是避免明确给出它的另一种选择。