isabelle - 什么是cterm？

Question

伊莎贝尔实施手册说：

类型 ctyp 和 cterm 分别代表经过认证的类型和术语。这些是抽象数据类型，相对于背景理论中类型构造函数、常量等的声明，它们保证其值已通过完整的格式良好（和类型良好）检查。

我的理解是：当我写 时cterm t，Isabelle 会根据它所在的理论检查该术语是否正确构建。

抽象类型 ctyp 和 cterm 是主要负责 thm 的同一推理内核的一部分。因此，对 ctyp 和 cterm 的句法操作位于 Thm 模块中，即使在那个阶段还没有涉及定理。

我的理解是：如果我想在 ML 级别修改 cterm，我将使用 Thm 模块的操作（我在哪里可以找到该模块？）

此外，它看起来像是cterm t一个将理论级别的术语转换为 ML 级别的术语的实体。所以我在声明中检查了 cterm 的代码：

ML_val ‹
  some_simproc @{context} @{cterm "some_term"}
›

并访问 ml_antiquotations.ML：

ML_Antiquotation.value \<^binding>‹cterm› (Args.term >> (fn t =>
    "Thm.cterm_of ML_context " ^ ML_Syntax.atomic (ML_Syntax.print_term t))) #>

以我目前的知识，这行代码对我来说是不可读的。

我想知道是否有人可以对 cterm 给出更好的低级解释。下面的代码是什么意思？cterm 根据理论术语执行的检查在哪里？我们可以对 cterms（上面的模块 Thm）进行的操作在哪里？

标签： isabelleml

Answer 1

“c”代表“认证”（或“检查”？不确定）。cterm 基本上是经过检查的术语。@{cterm …}反引用允许您简单地写下术语并在各种上下文中直接获取 cterm（在这种情况下可能是 ML 的上下文，即您直接获取具有预期内容的 cterm 值）。这同样适用于常规术语，即@{term …}.

您可以使用结构中的函数直接操作 cterms Thm（顺便提一下，可以在 中找到~~/src/Pure/thm.ML；这些基本 ML 文件中的大多数都在Pure目录中）。但是，根据我的经验，将 cterm 转换为常规术语通常更容易（使用Thm.term_of- 不像Thm.cterm_of，这是一个非常便宜的操作），然后使用该术语代替。仅当您最终需要另一个 cterm 时，直接操作 cterms 才真正有意义，因为重新认证条款相当昂贵（不过，除非您的代码被经常调用，否则它可能并不是真正的性能问题）。

在大多数情况下，我会说工作流程是这样的：如果您将 cterm 作为输入，则将其转换为常规术语。您可以轻松地检查/拆开/无论如何。在某些时候，您可能不得不再次将它变成一个 cterm（例如，因为您想用它实例化一些定理或以涉及内核的其他方式使用它），然后您就可以使用它Thm.cterm_of来执行此操作。

我不确切知道反引号在内部做了什么@{cterm …}，但我想在一天结束时，它只是将其参数解析为 Isabelle 术语，然后使用当前上下文（即@{context}）使用类似Thm.cterm_of.