什么是cterm？

Question

伊莎贝尔实施手册说：

Types ctyp and cterm represent certified types and terms, respectively. These are abstract datatypes that guarantee that its values have passed the full well-formedness (and well-typedness) checks, relative to the declarations of type constructors, constants etc. in the background theory.

我的理解是：当我写 cterm t 时，Isabelle 检查该术语是否根据其所在的理论构建良好。

The abstract types ctyp and cterm are part of the same inference kernel that is mainly responsible for thm. Thus syntactic operations on ctyp and cterm are located in the Thm module, even though theorems are not yet involved at that stage.

我的理解是：如果我想在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）进行的操作在哪里？

Answer 1

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

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

在大多数情况下，我会说工作流程是这样的：如果你得到一个 cterm 作为输入，你就把它变成一个常规术语。这个你可以轻松inspect/takeapart/whatever。在某些时候，你可能不得不再次将它变成一个 cterm（例如，因为你想用它实例化一些定理或以涉及内核的其他方式使用它）然后你只需使用 Thm.cterm_of 来做到这一点.

我不知道确切地 @{cterm …} 反引号在内部做了什么，但我想在一天结束时，它只是将其参数解析为一个 Isabelle 术语，然后使用 Thm.cterm_of.

之类的东西在当前上下文（即 @{context}）中证明它

Answer 2

为了使用 cterms 收集我的发现，我 post 一个答案。

这就是 cterm 在 Pure 中的样子：

abstype cterm =
  Cterm of {cert: Context.certificate, 
            t: term, T: typ, 
            maxidx: int,  
            sorts: sort Ord_List.T}

（待续）

什么是cterm？

What's a cterm?

ml

isabelle