Isabelle构造自然数集合函数报错及无限集处理咨询

1. 代码错误原因 #

你写的函数类型标注里用了'nat，这是类型变量（带单引号的是类型变量），而非Isabelle内置的自然数具体类型nat。类型变量默认没有ord排序约束，而<运算符要求操作数必须属于具备排序关系的ord类，所以才会报类型不匹配的错误——哪怕你把b换成固定自然数，类型变量'nat的约束问题依然存在。

2. 修正后的代码 #

把类型标注里的'nat改成具体类型nat即可，甚至可以省略集合里的:: nat（Isabelle能自动推断类型）：

fun set_of_nats :: "nat ⇒ nat set" where
  "set_of_nats b = {a. a < b}"

如果要显式指定集合元素类型，也可以写成：

fun set_of_nats :: "nat ⇒ nat set" where
  "set_of_nats b = {a :: nat. a < b}"

3. 关于无限集的处理 #

Isabelle/HOL完全支持定义和推理无限集：

• 直接用谓词定义即可，比如所有大于5的自然数集合：{a :: nat. a > 5}
• 逻辑层面可以对无限集进行各种推理，比如证明某个元素是否属于该集合、集合的基数是否无限等
• 注意：无限集无法被代码生成工具转换成可执行的程序（因为计算机无法存储无限元素），但这只影响代码执行，不影响逻辑推理。

内容的提问来源于stack exchange，提问作者Jonas