在 Isabelle 中检查数据类型

Question

导入 Main 允许您使用 nat 和 int 等类型，但如果不深入挖掘源代码，您将无法获得有关如何定义这些类型的信息。

有没有办法check/print在自己的程序中定义数据类型，而无需在源代码中手动搜索？

Answer 1

当你在伊莎贝尔中使用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-click）跳转到定义。

对于像 nat 这样的基础类型，它有点复杂，因为 nat 是在 datatype 命令之前定义的，后来的行为就好像它是用 [= 定义的一样13=].

在 Isabelle 中检查数据类型

Checking datatypes in Isabelle

isabelle