检查 Isabelle 中的数据类型

编程问答 2022-05-15

问题描述

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

有没有办法在自己的程序中检查/打印数据类型的定义，而不必在源代码中手动搜索？

解决方法

当您在 Isabelle 中使用 datatype 时，您实际上是在定义一个新类型、几个新常量和新定理。

一个简单的例子。当你写

datatype blub = A | B

  1. 您定义新类型 blub。

  2. 你定义了几个常量：

    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"

  3. 您定义新定理：

    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} 定义的}.

isabelle