HOL API: Theories and Theorems

This page continues the reference for hol_prover_client.hhol_prover_client.h, the RPC client for HOL Light, begun in HOL API: Types and Terms. The same conventions apply: every call records a status, which get_last_status()get_last_status() reports and get_last_error()get_last_error() explains; failure values depend on the result type, and the status provides a uniform way to detect failure; every returned pointer is garbage-collected; and the header is generated from the prover’s interface description.

The previous page describes syntax; this page describes theorems. 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 up an existing theorem in the theory, by extending the theory with a new definition or axiom, or by applying an inference rule. The first two are documented below; the third is covered in HOL API: Inference Rules.

A theorem is a sequent: a list of hypotheses and a conclusion, written A |- tA |- t. The following three functions provide the only way to inspect its components. 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 in a dest_thm_resultsdest_thm_results struct: the field tmstms contains the hypotheses, and tmtm contains the conclusion. The functions hyphyp and conclconcl return the individual components. A theorem with an empty hypothesis list holds unconditionally in the current theory; a theorem with hypotheses asserts its conclusion under those hypotheses. The rules disch_ruledisch_rule and undisch_ruleundisch_rule convert between hypotheses and implications.

The theory is the prover’s global state: the declared type constructors, the constants and their generic types, the assumed axioms, and the derived definitional theorems. Declarations, axioms, and definitions extend this state; this section also includes helpers for proving existence. Most operations that introduce a name fail if it is already taken.

The two primitive declarations introduce a type constructor of a given arity or a constant of a given type, without attaching a defining property to the name. 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 introduces an abbreviation that the parser and printer expand. The abbreviation does not exist in the logic.

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 aims to avoid relying on such assumptions. The API still provides new_axiomnew_axiom, but the C* library no longer needs it: every typed-memory rule on Typed Memory Predicates is proved. Any remaining axioms come from the client. 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 a theorem that characterises it, extending the theory without adding an 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 defines recursion over an inductive type, given that type’s recursion theorem. The two prove_*_existsprove_*_exists functions provide the existence step separately, for cases that require manual control of the definition process. new_specificationnew_specification introduces one or more constants from a proved existence theorem, naming a value 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.

Proof code uses the two remaining forms. 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 stores theorems by name and supports enumeration of the theory. Proof code uses these operations to find theorems and theory declarations not introduced 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.

The theorems associated 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 functions 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 parser accepts the syntax 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 or 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 execution engine’s assertion syntax, which is used in symbolic-state dumps and error messages. It also implements printing for the runtime’s cst_print_assertioncst_print_assertion (on Symbolic Execution and Runtime API), which sends the term to the server rather than traversing it node by node. Unlike the other printers, it fails if the term contains a node it cannot render.

The implicit-type context determines the types of free variables when parsing a term:

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 why most C* assertions need no explicit type annotations: the engine installs the implicit types of the program variables in scope before parsing the specification that mentions them.

A theorem is a sequent consisting of hypotheses and a conclusion, which can be read with dest_thmdest_thm, hyphyp and conclconcl. It is produced either by extending the theory through an axiom or a definition form that returns its characterising theorem, or by applying an inference rule. The theory is global, enumerable and name-indexed, and the parser and printer connect it to concrete syntax.

The next page covers general inference rules, the most common way to derive theorems.