HOL API: Theories and Theorems

This page continues the reference for hol_prover_client.hhol_prover_client.h, the RPC client for HOL Light, from HOL API: Types and Terms. The conventions established there hold unchanged: every call records a status, which get_last_status()get_last_status() reports and get_last_error()get_last_error() explains; a failed call returns an empty_*empty_* sentinel rather than NULLNULL, tested with IS_NULLIS_NULL; every returned pointer is garbage-collected; and the header is generated from the prover’s interface description.

Where the previous page dealt with syntax, this one deals with what is true. A hol_theoremhol_theorem is the only object in the API that carries a claim, and it can be obtained in exactly three ways: by looking one up in the theory, by extending the theory with a new definition or axiom, or by applying an inference rule to theorems already in hand. The first two are documented below; the third is HOL API: Inference Rules.

A theorem is a sequent: a list of hypotheses and a conclusion, written A |- tA |- t. The three functions here are the only way to look inside one, and none of them fails.

dest_thm_results dest_thm(hol_theorem th);

dest_thm_results dest_thm(hol_theorem th);

Breaks a theorem into assumption list and conclusion.

• raises — Never fails.

hol_term_list hyp(hol_theorem th);

hol_term_list hyp(hol_theorem th);

Returns the hypotheses of a theorem.

• raises — Never fails.

hol_term concl(hol_theorem th);

hol_term concl(hol_theorem th);

Returns the conclusion of a theorem.

• raises — Never fails.

dest_thmdest_thm returns both components at once in a dest_thm_resultsdest_thm_results struct — the field tmstms for the hypotheses, tmtm for the conclusion — while hyphyp and conclconcl are the individual projections. A theorem whose hypothesis list is empty is a theorem of the theory outright; one with hypotheses claims its conclusion only relative to them, which is what disch_ruledisch_rule and undisch_ruleundisch_rule trade against an implication.

The theory is the prover’s global state: the type constructors that exist, the constants that exist and their generic types, the axioms that have been assumed, and the definitional theorems that have been derived. Every function in this section mutates it, and most of them fail when the name they introduce is already taken.

The two primitive declarations introduce a name with no defining property attached — a type constructor of a stated arity, or a constant of a stated type. Nothing is proved about them; only an axiom or a definition can say what they mean.

void new_tyconst(const_cstr s, int i);

void new_tyconst(const_cstr s, int i);

Declares a new type or type constructor.

• raises — Fails if there is already a type operator of that name.

void new_const(const_cstr s, hol_type ty);

void new_const(const_cstr s, hol_type ty);

Declares a new constant.

• raises — Fails if there is already a constant of that name in the current theory.

void new_tyabbrev(const_cstr s, hol_type ty);

void new_tyabbrev(const_cstr s, hol_type ty);

Sets up a new type abbreviation.

• raises — Never fails.

new_tyabbrevnew_tyabbrev is different in kind: an abbreviation is expanded by the parser and printer and does not exist in the logic at all.

hol_theorem new_axiom(hol_term tm);

hol_theorem new_axiom(hol_term tm);

Sets up a new axiom.

• raises — Fails if the given term does not have type bool.

An axiom is an unproved assumption, and the LCF discipline described in LCF-Based Proof is precisely the discipline of not needing one. new_axiomnew_axiom is part of the API all the same, but the C* library no longer needs it: every typed-memory rule on Typed Memory Predicates is proved. What remains is the client’s own. An axiom a proof block adds is listed in the axiomsaxioms array of the verification report, in the order it was added (see cst_print_vccst_print_vc on Symbolic Execution and Runtime API), and a run whose array is not empty is not a completed proof.

A definition introduces a constant and returns the theorem that characterises it, so the theory grows without any new assumption. The forms differ in the shape of the equation they accept.

hol_theorem new_basic_definition(hol_term tm);

hol_theorem new_basic_definition(hol_term tm);

Makes a simple new definition of the form c = t.

• raises — Fails if c is already a constant.

hol_theorem new_const_definition(hol_term tm);

hol_theorem new_const_definition(hol_term tm);

Declares a new constant and a definitional axiom of the form c v1 ... vn = t.

• raises — Fails if c is already a constant or if the definition does not have the right form.

hol_theorem new_fun_definition(hol_term tm);

hol_theorem new_fun_definition(hol_term tm);

Defines a general recursive function.

• raises — Fails if the definition is malformed or if some of the necessary conditions for the definition to be admissible cannot be proved automatically, or if there is already a constant of the given name.

hol_theorem new_rec_definition(hol_theorem th, hol_term tm);

hol_theorem new_rec_definition(hol_theorem th, hol_term tm);

Defines a recursive function over inductive type.

• raises — Fails if the definition cannot be matched up with the recursion theorem provided, or if there is already a constant of the given name.

hol_theorem prove_rec_definition_exists(hol_theorem th, hol_term tm);

hol_theorem prove_rec_definition_exists(hol_theorem th, hol_term tm);

Prove existence of recursive function over inductive type.

• raises — Fails if the clauses cannot be matched up with the recursion theorem.

hol_theorem prove_general_rec_definition_exists(hol_term tm);

hol_theorem prove_general_rec_definition_exists(hol_term tm);

Proves existence of general recursive function.

• raises — Fails only if the definition is malformed. However it is possible that for an inadmissible definition the assumptions of the theorem may not hold.

hol_theorem new_specification(const_cstr_list s, hol_theorem th);

hol_theorem new_specification(const_cstr_list s, hol_theorem th);

Introduces a constant or constants satisfying a given property.

• raises — Fails if any one of the given name is already a constant.

new_basic_definitionnew_basic_definition handles the primitive form c = tc = t; new_const_definitionnew_const_definition accepts the curried form c v1 ... vn = tc v1 ... vn = t and abstracts the arguments itself; new_fun_definitionnew_fun_definition accepts a general recursive definition and discharges the admissibility conditions automatically. new_rec_definitionnew_rec_definition is the version for a recursion over an inductive type, given that type’s recursion theorem, and the two prove_*_existsprove_*_exists functions expose the existence step on its own, for cases where the automatic definition machinery has to be driven by hand. new_specificationnew_specification introduces one or more constants from a proved existence theorem — the way to name a value that is characterised by a property rather than by an expression.

new_basic_type_definition_results new_basic_type_definition(const_cstr s,
                                                            const_cstr mk,
                                                            const_cstr dest,
                                                            hol_theorem th);

new_basic_type_definition_results new_basic_type_definition(const_cstr s,
                                                            const_cstr mk,
                                                            const_cstr dest,
                                                            hol_theorem th);

Introduces a new type in bijection with a nonempty subset of an existing type.

• raises — Fails if any of the type or constant names is already in use, if the theorem has a nonempty list of hypotheses, if the conclusion of the theorem is not a combination, or if its rator contains free variables.

hol_theorem new_type_bijection_definition(const_cstr s, const_cstr mk,
                                          const_cstr dest, hol_theorem th);

hol_theorem new_type_bijection_definition(const_cstr s, const_cstr mk,
                                          const_cstr dest, hol_theorem th);

Introduces a new type in bijection with a nonempty subset of an existing type.

• raises — Fails if any of the type or constant names is already in use, if the theorem has a nonempty list of hypotheses, if the conclusion of the theorem is not an existentially quantified term, or the conclusion contains free variables.

new_datatype_definition_results new_datatype_definition(const_cstr s);

new_datatype_definition_results new_datatype_definition(const_cstr s);

Automatically define user-specified inductive data types.

• raises — Fails if one of the types or constructor constants is already defined, or if there are certain improper kinds of recursion, e.g. involving function spaces of one of the types being defined.

new_inductive_definition_results new_inductive_definition(hol_term tm);

new_inductive_definition_results new_inductive_definition(hol_term tm);

Define a relation or family of relations inductively.

• raises — Fails if the clauses are malformed, if the constants are already in use, or if there are unproven monotonicity hypotheses.

new_basic_type_definitionnew_basic_type_definition is the HOL Light primitive: given a theorem |- P x|- P x witnessing that a subset of an existing type is nonempty, it introduces a new type in bijection with that subset and returns the two theorems relating the abstraction and representation functions. new_type_bijection_definitionnew_type_bijection_definition is the variant taking an existentially quantified witness.

The two remaining forms are the ones proof code actually uses. new_datatype_definitionnew_datatype_definition takes the textual description of an algebraic data type and returns its induction and recursion theorems; new_inductive_definitionnew_inductive_definition defines a relation as the least one closed under a set of clauses, returning the rules, the induction principle and the cases theorem.

The prover keeps a name-indexed store of theorems, and the theory itself can be enumerated. Together these are how proof code finds something it did not prove locally.

hol_theorem get_theorem_by_name(const_cstr s);

hol_theorem get_theorem_by_name(const_cstr s);

Looks up a proved theorem by name.

• raises — Fails if no theorem has this name.

bool add_theorem(const_cstr name, hol_theorem th);

bool add_theorem(const_cstr name, hol_theorem th);

Adds a proved theorem to the environment with the given name. Returns true if successful, false if a theorem with this name already exists.

• raises — Never fails.

cstr_list list_theorems();

cstr_list list_theorems();

Lists the names of all theorems in the environment.

• raises — Never fails.

add_theoremadd_theorem returns falsefalse rather than failing when the name is taken, so registering the same theorem twice in a session is detectable without inspecting the status. get_theorem_by_nameget_theorem_by_name does fail on an unknown name.

The enumeration functions report what the theory currently contains:

int get_tyconst_arity(const_cstr s);

int get_tyconst_arity(const_cstr s);

Returns the arity of a type constructor.

• raises — Fails if there is no type constructor of that name.

hol_ty_const_list get_all_tyconsts();

hol_ty_const_list get_all_tyconsts();

Lists all the types presently declared.

• raises — Never fails.

hol_type get_const_type(const_cstr s);

hol_type get_const_type(const_cstr s);

Gets the generic type of a constant from the name of the constant.

• raises — Fails if the given name is not the name of a constant.

hol_const_list get_all_consts();

hol_const_list get_all_consts();

Returns a list of the constants currently defined.

• raises — Never fails.

hol_theorem_list get_all_axioms();

hol_theorem_list get_all_axioms();

Returns the current set of axioms.

• raises — Never fails.

hol_theorem_list get_all_definitions();

hol_theorem_list get_all_definitions();

Returns the current set of primitive definitions.

• raises — Never fails.

Finally, the theorems that come with an inductive type introduced by new_datatype_definitionnew_datatype_definition are retrieved by the type’s name rather than stored under a theorem name:

hol_theorem get_datatype_cases(const_cstr s);

hol_theorem get_datatype_cases(const_cstr s);

Produce cases theorem for an inductive type.

• raises — Fails if the given name is not the name of a recursive type.

hol_theorem get_datatype_distinctness(const_cstr s);

hol_theorem get_datatype_distinctness(const_cstr s);

Produce distinctness theorem for an inductive type.

• raises — Fails if the given name is not the name of a recursive type, or if the type has only one constructor.

hol_theorem get_datatype_induct(const_cstr s);

hol_theorem get_datatype_induct(const_cstr s);

Produce the structural induction theorem for an inductive type.

• raises — Fails if the given name is not the name of a registered inductive type.

hol_theorem get_datatype_injectivity(const_cstr s);

hol_theorem get_datatype_injectivity(const_cstr s);

Produce injectivity theorem for an inductive type.

• raises — Fails if the given name is not the name of a recursive type, or if all its constructors are nullary.

These four are the standard tools for reasoning about a user-defined data type: get_datatype_inductget_datatype_induct for structural induction, get_datatype_casesget_datatype_cases for a case split, and get_datatype_distinctnessget_datatype_distinctness and get_datatype_injectivityget_datatype_injectivity for the facts that different constructors produce different values and that a constructor is injective in its arguments.

Building a term with mk_combmk_comb and mk_constmk_const is precise but verbose. The alternative is to write the term in concrete syntax and let the prover parse it. The syntax accepted is the one documented on HOL Light Syntax, together with the C* additions on C* Extensions — the same notation that appears between backticks in a C* source file.

hol_type parse_type(const_cstr s);

hol_type parse_type(const_cstr s);

Parses a string into a type.

• raises — Fails in the event of a syntax error or unparsed input.

hol_term parse_term(const_cstr s);

hol_term parse_term(const_cstr s);

Parses a string into a term.

• raises — Fails in the event of a syntax error or unparsed input.

cstr string_of_type(hol_type ty);

cstr string_of_type(hol_type ty);

Converts a type to a string representation.

• raises — Never fails.

cstr string_of_term(hol_term tm);

cstr string_of_term(hol_term tm);

Converts a term to a string representation.

• raises — Never fails.

cstr string_of_thm(hol_theorem th);

cstr string_of_thm(hol_theorem th);

Converts a theorem to a string representation.

• raises — Never fails.

cstr cst_assertion_string(hol_term tm);

cstr cst_assertion_string(hol_term tm);

C* assertion printer: renders a HOL hprop/bool term in the symbolic engine's assertion syntax (data_atdata_at, **** as **, &x&x, x@prex@pre, (v:T)(v:T) annotations, WithWith/RequireRequire/EnsureEnsure function specs, ...). This is the server-side port of the C* runtime's cst_print_assertioncst_print_assertion, which used to walk the term one RPC per node.

• raises — Fails if the term contains a node the printer cannot render.

Parsing fails on a syntax error and on unparsed trailing input; the string_of_*string_of_* printers never fail. They produce the same notation the parser accepts, so a term printed into an error message can be pasted back into a source file.

cst_assertion_stringcst_assertion_string is the C* addition to this group. It renders an hprophprop or boolbool term in the symbolic engine’s own assertion syntax, the one the engine prints in symbolic-state dumps and error messages, and it is the printer behind the runtime’s cst_print_assertioncst_print_assertion (on Symbolic Execution and Runtime API), which sends the term to the server rather than walking it node by node. Unlike the other printers it can fail, on a term that contains a node it cannot render.

Parsing a term with free variables raises the question of what type those variables have. The implicit-type context answers it:

hol_text_type_pair_list get_the_implicit_types();

hol_text_type_pair_list get_the_implicit_types();

Returns the implicit types of all variables in the current context.

• raises — Never fails.

void set_the_implicit_types(hol_text_type_pair_list tys);

void set_the_implicit_types(hol_text_type_pair_list tys);

Restrict variables to a particular type or type scheme.

• raises — Never fails.

set_the_implicit_typesset_the_implicit_types restricts named variables to a type or type scheme, so that a later parse_termparse_term resolves them without an explicit annotation. This is the mechanism behind the type-free look of most C* assertions: the engine installs the implicit types of the program variables in scope before parsing the specification that mentions them.

A theorem is a sequent and nothing more: hypotheses and a conclusion, readable with dest_thmdest_thm, hyphyp and conclconcl. It enters the world either because the theory was extended — a declaration, an axiom, or one of the definition forms that returns its own characterising theorem — or because an inference rule produced it. The theory is global, enumerable and name-indexed, and the parser and printer connect it to concrete syntax.

What is missing from this page is the third and by far the most common source of theorems. Nothing here transforms one theorem into another.