我正在阅读 Isabelle 教程并试图澄清我对使用 primrec 和 fun 的概念。到目前为止我搜索过的内容，包括答案here；我知道 primrec 中的构造函数只能有一个方程，而 primrec 默认有 [simp] 而 fun 可以有多个方程，并且需要明确指定自动化策略。但是，我仍然很难清楚地理解它。
哪位好心人可以举一些例子来解释一下？
【问题讨论】：
primrec是一个低级的工具，你通常不需要担心，简单地说始终使用fun。
标签： isabelle
primrec 在代数数据类型上执行 primitive recursion （或者已经设置为看起来像自然数的东西；我对它的内部了解不多）。这意味着您可以拥有的递归方案有很多限制：
f (x#xs) (y#ys) = … 或f n = (if n = 0 then … else …) 这样的事情。x # xs，但不能在 x # y # xs）f (Node l r) = … f l … f r …，但不能在f (Node l r) = … f (Node r l) …。fun 来自函数包，是function 的简化版本，它试图证明穷举性、模式不重叠和自动终止。这适用于实践中出现的大多数功能；如果没有，则必须使用function 并手动证明这些事情。终止通常是一个棘手的问题。
fun 和primrec 之间的主要区别在于fun 没有我上面列出的primrec 的限制。有了fun，几乎一切都顺利。据我所知，primrec 能做的一切，fun 也能做。
function 还可以做很多其他事情，例如相互递归函数、部分函数（即不在所有输入上终止的函数）、条件函数方程等。有关更多信息，请参阅 function package manual关于这个。
function 命令的另一个特点是它会为使用它定义的每个函数生成许多有用的规则，例如cases 规则、induction 规则、elims 规则等。 ，您可以使用fun_cases 命令自动导出专门的消除规则。手册中也对此进行了描述。
TL;DR：Joachim 所说的。 fun 通常是您想要使用的。如果还不够，请使用function。您可以将primrec 用于非常简单的功能，但这样做并没有真正的优势。另一个可能对非终止函数感兴趣的替代方法是inductive。
【讨论】：
fun也支持相互递归，不只是function。
size 函数的代数数据类型（例如，无限分支树），primrec 优于 fun，因为自动终止证明方法（fun 在内部调用）需要size 函数。在这种情况下，您必须进行手动终止证明，这可能相当繁琐。