如何在Isabelle证明文档中验证并展示函数恒等示例？

问题背景 #

已定义函数：

definition "foo_function x = x+1"

需验证高阶函数等式：

id foo_function = foo_function

尝试过程中遇到以下问题：

• 执行value ‹id foo_function›触发Wellsortedness error
• value[simp] ‹id foo_function›在输出面板返回正确结果，但无法在证明文档中完成正式验证
• 使用lemma ‹id foo_function = foo_function› by eval等证明方法时，报错Wellsortedness error: Type 'a ⇒ 'a not of sort equal

解决方案 #

方法1：利用函数扩展性证明（推荐） #

Isabelle/HOL中，两个函数相等的核心判定规则是函数扩展性：若对所有输入，两个函数的输出都相同，则函数相等。基于此可以直接用简化规则完成证明：

lemma "id foo_function = foo_function"
  by simp

或者显式调用扩展性规则后简化：

lemma "id foo_function = foo_function"
  by (rule ext) simp

原理：ext规则将函数等式转化为∀x. (id foo_function) x = foo_function x，simp会展开id的定义（id f = f），自动得到∀x. foo_function x = foo_function x，进而通过自反性完成证明。

方法2：添加类型排序约束 #

报错的根源是Isabelle默认不认为函数类型'a ⇒ 'a属于equal排序类（支持等式判断的类型类）。可以显式指定类型参数的排序约束，让函数类型满足等式验证要求：

lemma "id (foo_function :: 'a::{equal} ⇒ 'a) = foo_function"
  by (rule refl)

这种方法需要额外的类型约束，适用性不如方法1广泛，仅在特定需要依赖equal类的场景下使用。

方法3：正确使用value命令验证 #

若仅需在交互界面查看计算结果，可给id foo_function指定具体类型（比如自然数上的函数）来规避排序错误：

value ‹id (foo_function :: nat ⇒ nat)›

执行后会输出foo_function，符合预期。

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