Isabelle/HOL 中的 primrec 和 fun 有什么区别？
What is the difference between primrec and fun in Isabelle/HOL?
我正在阅读 Isabelle 教程并试图理清我对使用 primrec 和乐趣的概念。到目前为止我搜索过的内容，包括答案 here；我知道 primrec 中的构造函数只能有一个方程，而 primrec 默认有 [simp] 而 fun 可以有多个方程，并且需要明确指定自动化策略。但是，我仍然很难清楚地理解它。
有好心人能举例说明一下吗？
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 列出的限制中的 none。使用 fun，几乎一切顺利。据我所知，primrec能做到的，fun也能做到。
function 还可以做很多其他事情，例如相互递归函数、部分函数（即不在所有输入上终止的函数）、条件函数方程等。请参阅 function package manual 了解更多信息。
function 命令的另一个特点是它为用它定义的每个函数生成许多有用的规则，例如 cases 规则、induction 规则、 elims规则等。此外，您还可以使用fun_cases命令自动导出专门的消除规则。手册中也对此进行了描述。
TL;DR：约阿希姆说的。 fun 通常是您要使用的。如果不够用function。您可以将 primrec 用于非常简单的函数，但这样做并没有真正的好处。另一个可能对可能的非终止函数感兴趣的替代方法是 inductive.
我正在阅读 Isabelle 教程并试图理清我对使用 primrec 和乐趣的概念。到目前为止我搜索过的内容，包括答案 here；我知道 primrec 中的构造函数只能有一个方程，而 primrec 默认有 [simp] 而 fun 可以有多个方程，并且需要明确指定自动化策略。但是，我仍然很难清楚地理解它。
有好心人能举例说明一下吗？
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 列出的限制中的 none。使用 fun，几乎一切顺利。据我所知，primrec能做到的，fun也能做到。
function 还可以做很多其他事情，例如相互递归函数、部分函数（即不在所有输入上终止的函数）、条件函数方程等。请参阅 function package manual 了解更多信息。
function 命令的另一个特点是它为用它定义的每个函数生成许多有用的规则，例如 cases 规则、induction 规则、 elims规则等。此外，您还可以使用fun_cases命令自动导出专门的消除规则。手册中也对此进行了描述。
TL;DR：约阿希姆说的。 fun 通常是您要使用的。如果不够用function。您可以将 primrec 用于非常简单的函数，但这样做并没有真正的好处。另一个可能对可能的非终止函数感兴趣的替代方法是 inductive.