Isabelle 中是否有限地生成了归纳定义？答案

【问题标题】：Are inductive definitions finitely generated in Isabelle?Isabelle 中是否有限地生成了归纳定义？
【发布时间】：2018-09-13 23:01:18
【问题描述】：

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

表示，在归纳定义中，

一个规则是一对(X,x)，其中X是一个集合，称为前提的集合，x是结论。规则通常写成 X->x。

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

据我记忆，实际验证任务仅涉及有限前提集 Xs，例如自反和传递闭包在

我有两个相关的问题：

【问题讨论】：

【解决方案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

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

【讨论】：

我问这个是因为后来在证明 Aczel 使用的规则可能具有无限前提，即 (a 规则，其中
mathoverflow.net/questions/296973/…
很可能在 Isabelle 中对此进行建模。如果你对这些无限多的规则有一些有限的表示，也应该可以在 Isabelle 的归纳谓词的上下文中使用它，但我必须看一个具体的例子。
查看MathOverflow问题中的例子，可能有无限的前提和无限的规则。
嗯，这很容易在 Isabelle 中用一个假设来建模。我更新了上面的答案。