如何解决检查 Isabelle 中的数据类型
导入 Main
允许您使用 nat
和 int
等类型,但如果不深入挖掘源代码,您将无法获得有关如何定义这些类型的信息。
有没有办法在自己的程序中检查/打印数据类型的定义,而不必在源代码中手动搜索?
解决方法
当您在 Isabelle 中使用 datatype
时,您实际上是在定义一个新类型、几个新常量和新定理。
一个简单的例子。当你写
datatype blub = A | B
-
您定义新类型
blub
。 -
你定义了几个常量:
find_consts name: "blub." found 6 constant(s): Scratch.blub.case_blub :: "'a ⇒ 'a ⇒ blub ⇒ 'a" Scratch.blub.rec_blub :: "'a ⇒ 'a ⇒ blub ⇒ 'a" Scratch.blub.typerep_blub_IITN_blub_inst.typerep_blub_IITN_blub :: "blub.blub_IITN_blub itself ⇒ typerep" Scratch.blub.size_blub :: "blub ⇒ nat" Scratch.blub.A :: "blub" Scratch.blub.B :: "blub"
-
您定义新定理:
find_theorems name: "blub." found 28 theorem(s): Scratch.blub.simps(1): A ≠ B Scratch.blub.simps(2): B ≠ A Scratch.blub.size(3): size A = 0 Scratch.blub.size(4): size B = 0 Scratch.blub.size(1): size_blub A = 0 Scratch.blub.size(2): size_blub B = 0 ...
您可以使用相应的搜索命令或使用通用名称前缀的查询面板搜索新的常数和定理。 如果您想查看真正的定义,只需使用 jedit(例如 Ctrl-单击)跳转到定义即可。
对于像 nat
这样的基础类型,它有点复杂,因为 nat
是在 datatype
命令之前定义的,后来使其表现得好像它是用 {{1} 定义的}.
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。