Isabelle 中的归纳定义是有限生成的吗？

Question

Peter Aczel 的经典论文 An Introduction to Inductive Definitions

表示，在归纳定义中，

a rule is a pair (X,x), where X is a set, called the set of premisses and x is the conclusion. The rule will usually be written X->x.

现在，这并没有说明集合 X 的有限性。

根据我的记忆，实际的验证任务只涉及有限前提集 Xs，例如

处的自反和传递闭包

我有两个相关问题：

Answer 1

是的，它必须是有限的。你怎么会写下无限多的规则？

当然，你拥有HOL的所有表达能力，所以你可以写出像‘∀x’这样的东西。 f x ≤ f (x + 1)’，这在某种意义上对应于无限多个子句‘f 0 ≤ f 1’、‘f 1 ≤ f 2’等，但这仍然只是一个假设。

编辑：作为对您评论的回应，您可以像这样在 Isabelle 中捕获这个示例（如果我理解正确的话）

inductive acc :: "('a ⇒ 'a ⇒ bool) ⇒ 'a ⇒ bool" for lt where
  "(⋀x. lt x a ⟹ acc lt x) ⟹ acc lt a"

这里，lt代表‘小于’，代表某种关系。这实际上几乎就是 Isabelle/HOL 中 Wellfounded 理论中的 Wellfounded.acc（如“可访问部分”）所做的以及它是如何定义的。一个可能稍微好一点的介绍是这样的：

context
  fixes lt :: "'a ⇒ 'a ⇒ bool" (infix "≺" 50)
begin

inductive acc :: "'a ⇒ bool" where
  "(⋀x. x ≺ a ⟹ acc x) ⟹ acc a"

end

我只浏览了您链接的文章，但在我看来，他讨论的内容不如伊莎贝尔的归纳谓词笼统。在我看来，他提供了一种定义归纳谓词 P 的方法，该谓词采用单个参数，并且所有产生式规则都必须采用 (∀x∈A(a). P(x)) ⟹ P(a) 形式。正如您在上面看到的，这可以很容易地在 Isabelle 中建模。

Are inductive definitions finitely generated in Isabelle?