Isabelle proof助手(2020)中有没有办法检查预定义函数的定义，例如div(或缩写和其他定义)？
在学习 Isabelle 时，我发现理解像div这样的函数是如何定义的很有帮助的。 我知道您可以打印或签入Coq，但无法在Isabelle中获取定义。
我试图将鼠标悬停在Isabelle/jEdit中的上下文菜单上，但找不到任何东西。在互联网上搜索似乎也没有提供任何相关内容。
常量Ctrl+Click通常会带您进入其定义(无论通过什么方式定义常量，无论是definition、inductive还是fun)。这也适用于类型和定理！
但是，对于类型类中定义的div之类的内容，这会转到声明。还有一些其他实例(例如来自区域设置解释的常量，如sum)，您也不会到达您想要的地方。
我不知道有任何统一的机制来访问定义(至少在没有深入研究 Isabelle 的 ML 接口的情况下不会)。
但是，典型情况如下(假设常量称为foo)：
- 对于"正常"定义(使用
definition命令)，定理简称为foo_def。对于其他一些工具，如primrec，_def定理也是可访问的。 - 对于类型类如
(+)、(*)、(-)、(div)、(mod)、gcd、size等类型的常量，名称是foo_type_def，其中type是所讨论的类型。例如，请参阅plus_nat_def、size_list_def。 - 对于用
fun/function/etc 定义的函数，_def定理是隐藏的，因为它来自复杂的内部结构，只会让用户感到困惑，而且毫无用处。我认为它在内部构建了某种调用图，然后通过它定义函数——我不确定细节。无论如何，对于fun，您应该看到foo.simps引理作为定义(如果函数没有在任何地方终止，则foo.psimps)。
( - 共)归纳谓词(用
inductive/coinductive定义)的特征在于它们的foo.intros规则。不过，他们也有foo.simps。 - 某些常量(如数据类型构造函数)根本没有可见的定义。我建议你像神奇地从天上掉下来一样对待它们，并具有它们的特征(注入性、详尽性等)。;)
对于具有花哨语法的函数，如(+)，您可以通过用鼠标Ctrl+hovering它或(在大多数情况下)Ctrl+clicking它来找到基础常量的名称。
如果所有其他方法都失败了，您还可以像这样查看常量的内部表示：
ML_val ‹@{term "(+)"}›
这将输出以下内容：
val it = Const ("Groups.plus_class.plus", "'a ⇒ 'a ⇒ 'a"): term
所以你可以看到常量的名字是plus(它的全名是Groups.plus_class.plus)。事实上，plus_nat_def给了你自然数加法的定义。
最后，请注意，有时人们会以一种方式定义事物，然后通过显示相等性来添加额外的"替代"定义，例如is_singleton_defvs.is_singleton_altdef.在许多情况下，最好使用派生属性，而不是一直扩展定义。定义有时可以包含技术细节，例如"函数在错误输入上的行为如何"(例如除以零或负数的对数)，并且通常最好尽可能避免证明依赖于这些细节。