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

Question

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

https://www.sciencedirect.com/science/article/pii/S0049237X08711200

说，在归纳定义中，

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，例如自反和传递闭包

https://isabelle.in.tum.de/dist/Isabelle2017/doc/tutorial.pdf#page=124

我有两个相关的问题:

1. 在 Isabelle 中是否可以使用无限前提？

2. 如果是，有没有实际的例子？

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 中建模。