What's a cterm?

Question

The Isabelle implementation manual says:

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.

My understanding is: when I write cterm t, Isabelle checks that the term is well-built according to the theory where it lives in.

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.

My understanding is: if I want to modify a cterm at the ML level I will use operations of the Thm module (where can I find that module?)

Furthermore, it looks like cterm t is an entity that converts a term of the theory level to a term of the ML-level. So I inspect the code of cterm in the declaration:

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

and get to 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))) #>

This line of code is unreadable to me with my current knowledge.

I wonder if someone could give a better low-level explanation of cterm. What is the meaning of the code below? Where are located the checks that cterm performs on theory terms? Where are located the manipulations that we can do on cterms (the module Thm above)?

user_2144227 · Answer

The ‘c’ stands for ‘certified’ (Or ‘checked’? Not sure). A cterm is basically a term that has been undergone checking. The @{cterm …} antiquotation allows you to simply write down terms and directly get a cterm in various contexts (in this case probably the context of ML, i.e. you directly get a cterm value with the intended content). The same works for regular terms, i.e. @{term …}.

You can manipulate cterms directly using the functions from the Thm structure (which, incidentally, can be found in ~~/src/Pure/thm.ML; most of these basic ML files are in the Pure directory). However, in my experience, it is usually easier to just convert the cterm to a regular term (using Thm.term_of – unlike Thm.cterm_of, this is a very cheap operation) and then work with the term instead. Directly manipulating cterms only really makes sense if you need another cterm in the end, because re-certifying terms is fairly expensive (still, unless your code is called very often, it probably isn't really a performance problem).

In most cases, I would say the workflow is like this: If you get a cterm as an input, you turn it into a regular term. This you can easily inspect/take apart/whatever. At some point, you might have to turn it into a cterm again (e.g. because you want to instantiate some theorem with it or use it in some other way that involves the kernel) and then you just use Thm.cterm_of to do that.

I don't know exactly what the @{cterm …} antiquotation does internally, but I would imagine that at the end of the day, it just parses its parameter as an Isabelle term and then certifies it with the current context (i.e. @{context}) using something like Thm.cterm_of.

user_5069802 · Answer

To gather my findings with cterms, I post an answer.

This is how a cterm looks like in Pure:

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

(To be continued)

What's a cterm?

2 Answers