HOL API: Conversions and Solvers

The rules of the previous page take theorems and produce theorems. This page covers the other two ways hol_prover_client.hhol_prover_client.h reaches a theorem: a conversion, which rewrites a term and returns the equation justifying the rewrite, and a solver, which is handed a term and returns it proved.

Both are how proof code avoids doing propositional bookkeeping by hand. A purification obligation left over from symbolic execution is usually not interesting mathematics — it is arithmetic, or a machine-word identity, or an equality that follows from unfolding a definition — and the point of this half of the API is that such goals are closed by one call rather than by a sequence of primitive steps.

A conversion is a function from a term to a theorem: given tt it returns |- t = t'|- t = t', the equation that licenses replacing tt by t't'. It is the unit that the whole rewriting machinery is built from, and the type hol_conversionhol_conversion is an opaque handle to one, exactly like hol_termhol_term and hol_theoremhol_theorem.

Conversions can be named. The prover keeps an environment of them: add_conversionadd_conversion registers one under a name, list_conversionslist_conversions reports the names in use, and get_conversion_by_nameget_conversion_by_name retrieves one — which is how a conversion built in one proof function becomes available to another, and how the conversions the engine installs are reached. apply_conversionapply_conversion runs a conversion on a term to get the equation; conv_ruleconv_rule lifts it to a rule, applying it to a theorem’s conclusion and rewriting the theorem in place.

hol_conversion get_conversion_by_name(const_cstr s);

hol_conversion get_conversion_by_name(const_cstr s);

Looks up a defined conversion by name.

• raises — Fails if no conversion has this name.

hol_theorem conv_rule(hol_conversion conv, hol_theorem th);

hol_theorem conv_rule(hol_conversion conv, hol_theorem th);

    A |- t
--------------  CONV_RULE c (which maps `t` into `A' |- t = t'`)
 A u A' |- t'

    A |- t
--------------  CONV_RULE c (which maps `t` into `A' |- t = t'`)
 A u A' |- t'

Makes an inference rule from a conversion.

• raises — Fails if the conversion fails when applied to the conclusion of the theorem.

hol_theorem apply_conversion(hol_conversion conv, hol_term tm);

hol_theorem apply_conversion(hol_conversion conv, hol_term tm);

Applies a conversion to a term to get a theorem.

• raises — Fails if the conversion fails.

bool add_conversion(const_cstr name, hol_conversion conv);

bool add_conversion(const_cstr name, hol_conversion conv);

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

• raises — Never fails.

cstr_list list_conversions();

cstr_list list_conversions();

Lists the names of all conversions in the environment.

• raises — Never fails.

A conversion on its own rewrites the whole term it is given, at the top level. The combinators below are what direct it somewhere useful, and they come in three families.

Combining conversions: then_convthen_conv sequences two, orelse_convorelse_conv tries the second if the first fails, every_convevery_conv and first_convfirst_conv are their list forms, try_convtry_conv turns failure into the identity, changed_convchanged_conv turns a no-op into failure — which is what makes a repetition terminate — and cache_convcache_conv memoises.

Traversal: depth_convdepth_conv, once_depth_convonce_depth_conv, redepth_convredepth_conv, top_depth_convtop_depth_conv and top_sweep_convtop_sweep_conv apply a conversion throughout a term, differing in direction (bottom-up or top-down), in whether they repeat, and in whether they revisit subterms they have already changed. Divergence is a real possibility for the repeating ones, and the header says so entry by entry.

Targeting: rand_convrand_conv, rator_convrator_conv, abs_convabs_conv, binder_convbinder_conv, land_convland_conv, binop_convbinop_conv, binop2_convbinop2_conv, comb_convcomb_conv, comb2_convcomb2_conv, sub_convsub_conv, depth_binop_convdepth_binop_conv, list_convlist_conv, path_convpath_conv and pat_convpat_conv descend into a specific part of the term — an operator, an operand, the body of an abstraction or binder, one side of a binary operator, a position named by a path string, or the subterms matched by a pattern.

hol_conversion gen_alpha_conv(hol_term v);

hol_conversion gen_alpha_conv(hol_term v);

Renames the bound variable of an abstraction or binder.

• raises — Fails if the given term is not a variable or the applied term does not have one of the forms \x. t\x. t or b (\x. t)b (\x. t), or if the types of x and v differ, or if v is already free in the body t.

hol_conversion rand_conv(hol_conversion conv);

hol_conversion rand_conv(hol_conversion conv);

Applies a conversion to the operand of an application.

• raises — Fails if the applied term is not an application or if it has the form t1 t2t1 t2 but the conversion fails when applied to the term t2.

hol_conversion pat_conv(hol_term tm, hol_conversion conv);

hol_conversion pat_conv(hol_term tm, hol_conversion conv);

Applies a conversion at subterms identified by a pattern lambda-abstraction.

• raises — Never fails until applied to a term, but then it may fail if the core conversion does on the chosen subterms.

hol_conversion rator_conv(hol_conversion conv);

hol_conversion rator_conv(hol_conversion conv);

Applies a conversion to the operator of an application.

• raises — Fails if the applied term is not an application of if it has the form t1 t2t1 t2 but the conversion fails when applied to the term t1.

hol_conversion abs_conv(hol_conversion conv);

hol_conversion abs_conv(hol_conversion conv);

Applies a conversion to the body of an abstraction.

• raises — Fails if the applied term is not an abstraction or if it has the form \x. t\x. t but the given conversion fails when applied to the term t, or if the theorem returned has assumptions in which the abstractd variable x is free.

hol_conversion binop2_conv(hol_conversion conv1, hol_conversion conv2);

hol_conversion binop2_conv(hol_conversion conv1, hol_conversion conv2);

Applies conversions to the two arguments of a binary operator.

• raises — Fails if the applied term is not binary of if it has the form op l rop l r but the given conversions fail or return inappropriate theorems.

hol_conversion binop_conv(hol_conversion conv);

hol_conversion binop_conv(hol_conversion conv);

Applies a conversion to both arguments of a binary operator.

• raises — Fails if the applied term is not binary of if it has the form op l rop l r but the given conversion fails or returns an inappropriate theorem.

hol_conversion comb_conv(hol_conversion conv);

hol_conversion comb_conv(hol_conversion conv);

Applies a conversion to the two sides of an application.

• raises — Fails if the applied term or if it has the form f xf x but the given conversion fails when applied to the term f or x, or it returns inappropriate theorems.

hol_conversion depth_conv(hol_conversion conv);

hol_conversion depth_conv(hol_conversion conv);

Applies a conversion repeatedly to all the sub-terms of a term, in bottom-up order.

• raises — Never fails, but may diverge.

hol_conversion every_conv(hol_conversion_list convs);

hol_conversion every_conv(hol_conversion_list convs);

Applies in sequence all the conversions in a given list of conversions.

• raises — Fails if any one of the given conversions fails.

hol_conversion first_conv(hol_conversion_list convs);

hol_conversion first_conv(hol_conversion_list convs);

Applies the first of the conversions in a given list that succeeds.

• raises — Fails if all the given conversions fail.

hol_conversion assoc_conv(hol_theorem th);

hol_conversion assoc_conv(hol_theorem th);

Right-associates a term with respect to an associative binary operator.

• raises — Fails if the given theorem is malformed.

hol_conversion binder_conv(hol_conversion conv);

hol_conversion binder_conv(hol_conversion conv);

Applies conversion to the body of a binder.

• raises — Fails if the applied term is not a binder or if it has the form b (\x. t)b (\x. t) but the given conversion fails when applied to t or returns an inappropriate theorem.

hol_conversion cache_conv(hol_conversion conv);

hol_conversion cache_conv(hol_conversion conv);

Accelerates a conversion by cacheing previous results.

• raises — Fails if the given conversion would fail.

hol_conversion comb2_conv(hol_conversion conv1, hol_conversion conv2);

hol_conversion comb2_conv(hol_conversion conv1, hol_conversion conv2);

Applies two conversions to the two sides of an application.

• raises — Fails if the applied term or if it has the form f xf x but the given conversions fail when applied to the term f or x, or they return inappropriate theorems.

hol_conversion depth_binop_conv(hol_term tm, hol_conversion conv);

hol_conversion depth_binop_conv(hol_term tm, hol_conversion conv);

Applied a conversion to the leaves of a tree of binary operator expressions.

• raises — Fails if the given conversion would fail.

hol_conversion changed_conv(hol_conversion conv);

hol_conversion changed_conv(hol_conversion conv);

Makes a conversion fail if applying it leaves a term unchanged.

• raises — Fails when the given conversion would fail or yield a reflexive theorem.

hol_conversion land_conv(hol_conversion conv);

hol_conversion land_conv(hol_conversion conv);

Applies a conversion to left-hand argument of binary operator.

• raises — Fails if the underlying conversion does or returns an inappropriate theorem.

hol_conversion list_conv(hol_conversion conv);

hol_conversion list_conv(hol_conversion conv);

Applies a conversion to each element of a list.

• raises — Fails if the conversion fails on any list element.

hol_conversion once_depth_conv(hol_conversion conv);

hol_conversion once_depth_conv(hol_conversion conv);

Applies a conversion once to the first suitable sub-term(s) encountered in top-down order.

• raises — Never fails.

hol_conversion orelse_conv(hol_conversion conv1, hol_conversion conv2);

hol_conversion orelse_conv(hol_conversion conv1, hol_conversion conv2);

Applies the first of two conversions that succeeds.

• raises — Fails if both given conversions would fail.

hol_conversion path_conv(const_cstr s, hol_conversion conv);

hol_conversion path_conv(const_cstr s, hol_conversion conv);

Applies a conversion to the subterm indicated by a path string.

• raises — Fails if applied to a term when the path is not meaningful or if the given conversion would fail.

hol_conversion prop_atom_conv(hol_conversion conv);

hol_conversion prop_atom_conv(hol_conversion conv);

Applies a conversion to the ‘atomic subformulas’ of a formula.

• raises — Never fails.

hol_conversion redepth_conv(hol_conversion conv);

hol_conversion redepth_conv(hol_conversion conv);

Applies a conversion bottom-up to all subterms, retraversing changed ones.

• raises — Never fails, but may diverge.

hol_conversion sub_conv(hol_conversion conv);

hol_conversion sub_conv(hol_conversion conv);

Applies a conversion to the top-level subterms of a term.

• raises — Fails if the applied term is an abstraction \x. t\x. t and the given conversion fails when applied to t, or the term is an application t1 t2t1 t2 and the given conversion fails when applied to t1 or t2.

hol_conversion then_conv(hol_conversion conv1, hol_conversion conv2);

hol_conversion then_conv(hol_conversion conv1, hol_conversion conv2);

Applies two conversions in sequence.

• raises — Fails if either conversion would fail.

hol_conversion top_depth_conv(hol_conversion conv);

hol_conversion top_depth_conv(hol_conversion conv);

Applies a conversion top-down to all subterms, retraversing changed ones.

• raises — Never fails, but may diverge.

hol_conversion top_sweep_conv(hol_conversion conv);

hol_conversion top_sweep_conv(hol_conversion conv);

Repeatedly applies a conversion top-down at all levels, but after descending to subterms, does not return to higher ones.

• raises — Never fails.

hol_conversion try_conv(hol_conversion conv);

hol_conversion try_conv(hol_conversion conv);

Attempts to apply a conversion; applies identity conversion in case of failure.

• raises — Never fails.

Rewriting is the standard use of all of the above: turn a list of equational theorems into a conversion and apply it everywhere until nothing changes. The family is large but systematic, and the name says what a member does.

A _conv_conv rewrites a term, a _rule_rule rewrites a theorem’s conclusion. A pure_pure_ prefix means only the supplied theorems are used, without the built-in tautologies and standard simplifications the plain forms add. A once_once_ prefix means one pass instead of repetition to a fixed point — the way to avoid the divergence the plain forms warn about. An asm_asm_ prefix means the theorem’s own assumptions are used as rewrites as well. The simpsimp forms are stronger than the rewriterewrite forms: they perform conditional, contextual simplification, discharging side conditions as they go, and are what a proof normally reaches for first.

hol_theorem once_rewrite_rule(hol_theorem_list ths, hol_theorem th);

hol_theorem once_rewrite_rule(hol_theorem_list ths, hol_theorem th);

Rewrites a theorem, including built-in tautologies in the list of rewrites.

• raises — Never fails.

hol_theorem rewrite_rule(hol_theorem_list ths, hol_theorem th);

hol_theorem rewrite_rule(hol_theorem_list ths, hol_theorem th);

Rewrites a theorem including built-in tautologies in the list of rewrites.

• raises — Never fails, but may diverge if the sequence of rewrites is non-terminating.

hol_conversion rewrite_conv(hol_theorem_list ths);

hol_conversion rewrite_conv(hol_theorem_list ths);

Rewrites a term including built-in tautologies in the list of rewrites.

• raises — Never fails, but may diverge if the sequence of rewrites is non-terminating.

hol_conversion pure_rewrite_conv(hol_theorem_list ths);

hol_conversion pure_rewrite_conv(hol_theorem_list ths);

Rewrites a term with only the given list of rewrites.

• raises — Never fails, but may diverge.

hol_theorem pure_rewrite_rule(hol_theorem_list ths, hol_theorem th);

hol_theorem pure_rewrite_rule(hol_theorem_list ths, hol_theorem th);

Rewrites a theorem with only the given list of rewrites.

• raises — Never fails, but may diverge.

hol_conversion once_rewrite_conv(hol_theorem_list ths);

hol_conversion once_rewrite_conv(hol_theorem_list ths);

Rewrites a term, including built-in tautologies in the list of rewrites.

• raises — Never fails.

hol_conversion pure_once_rewrite_conv(hol_theorem_list ths);

hol_conversion pure_once_rewrite_conv(hol_theorem_list ths);

Rewrites a term once with only the given list of rewrites.

• raises — Never fails.

hol_theorem pure_once_rewrite_rule(hol_theorem_list ths, hol_theorem th);

hol_theorem pure_once_rewrite_rule(hol_theorem_list ths, hol_theorem th);

Rewrites a theorem once with only the given list of rewrites.

• raises — Never fails.

hol_theorem simp_rule(hol_theorem_list ths, hol_theorem target);

hol_theorem simp_rule(hol_theorem_list ths, hol_theorem target);

Simplify conclusion of a theorem repeatedly by conditional contextual rewriting.

• raises — Never fails.

hol_conversion simp_conv(hol_theorem_list ths);

hol_conversion simp_conv(hol_theorem_list ths);

Simplify a term repeatedly by conditional contextual rewriting.

• raises — Never fails.

hol_conversion once_simp_conv(hol_theorem_list ths);

hol_conversion once_simp_conv(hol_theorem_list ths);

Simplify a term once by conditional contextual rewriting.

• raises — Never fails.

hol_theorem asm_rewrite_rule(hol_theorem_list ths, hol_theorem th);

hol_theorem asm_rewrite_rule(hol_theorem_list ths, hol_theorem th);

Rewrites a theorem including built-in rewrites and the theorem's assumptions.

• raises — Never fails, but may diverge.

hol_theorem once_asm_rewrite_rule(hol_theorem_list ths, hol_theorem th);

hol_theorem once_asm_rewrite_rule(hol_theorem_list ths, hol_theorem th);

Rewrites a theorem once including built-in rewrites and the theorem's assumptions.

• raises — Never fails.

hol_theorem pure_asm_rewrite_rule(hol_theorem_list ths, hol_theorem th);

hol_theorem pure_asm_rewrite_rule(hol_theorem_list ths, hol_theorem th);

Rewrites a theorem including the theorem's assumptions as rewrites.

• raises — Never fails, but may diverge.

hol_theorem pure_once_asm_rewrite_rule(hol_theorem_list ths, hol_theorem th);

hol_theorem pure_once_asm_rewrite_rule(hol_theorem_list ths, hol_theorem th);

Rewrites a theorem once, including the theorem's assumptions as rewrites.

• raises — Never fails.

hol_conversion higher_rewrite_conv(hol_theorem_list ths, bool b);

hol_conversion higher_rewrite_conv(hol_theorem_list ths, bool b);

Rewrites once using more general higher order matching.

• raises — Fails if no match is found.

hol_conversion imp_rewr_conv(hol_theorem th);

hol_conversion imp_rewr_conv(hol_theorem th);

Basic conditional rewriting conversion.

• raises — Fails if the theorem is not of the right form or the two terms cannot be matched.

hol_conversion rewr_conv(hol_theorem th);

hol_conversion rewr_conv(hol_theorem th);

Uses an instance of a given equation to rewrite a term.

• raises — Fails if the given theorem is not an equation or an equation universally quantified at the outermost level.

hol_conversion sublet_conv(hol_conversion conv);

hol_conversion sublet_conv(hol_conversion conv);

Applies subconversion to RHSs of toplevel let-term.

• raises — Fails if the applied term is not a toplevel let-term or if the given conversion would fail on RHSs.

hol_conversion subs_conv(hol_theorem_list ths);

hol_conversion subs_conv(hol_theorem_list ths);

Substitution conversion.

• raises — Fails if the given theorems are not equational.

hol_conversion pure_simp_conv(hol_theorem_list ths);

hol_conversion pure_simp_conv(hol_theorem_list ths);

Simplifies a term repeatedly by conditional contextual rewriting, not using default simplifications.

• raises — Never fails.

The functions in this section take a term and return it proved, or fail. They are the top of the API in terms of leverage and the bottom in terms of predictability: each one is complete for a specific fragment and simply fails outside it, so the skill in using them is knowing which fragment a goal falls into.

General-purpose proof search over first-order logic, given a list of theorems to use as the background theory. meson_solvermeson_solver is the workhorse; the others differ in search strategy, and a goal one of them cannot find is sometimes found immediately by another.

hol_theorem meson_solver(hol_theorem_list ths, hol_term tm);

hol_theorem meson_solver(hol_theorem_list ths, hol_term tm);

Proves a first-order logic theorem using the MESON algorithm.

• raises — Fails if the term is unprovable within the search bounds.

hol_theorem metis_solver(hol_theorem_list ths, hol_term tm);

hol_theorem metis_solver(hol_theorem_list ths, hol_term tm);

Proves a first-order logic theorem using the METIS algorithm.

• raises — Fails if the term is unprovable within the search bounds.

hol_theorem lean_cop_solver(hol_theorem_list ths, hol_term tm);

hol_theorem lean_cop_solver(hol_theorem_list ths, hol_term tm);

Proves a first-order logic theorem using the leanCop connection-based prover

• raises — Fails if the term is unprovable within the search bounds.

hol_theorem nano_cop_solver(hol_theorem_list ths, hol_term tm);

hol_theorem nano_cop_solver(hol_theorem_list ths, hol_term tm);

Proves a first-order logic theorem using the nanoCoP connection-based prover

• raises — Fails if the term is unprovable within the search bounds.

hol_theorem itaut_rule(hol_term tm);

hol_theorem itaut_rule(hol_term tm);

Attempts to prove term using intuitionistic first-order logic.

• raises — Fails if the goal is non-Boolean. May also fail if it's unprovable, though more usually this results in indefinite looping.

Algebraic normalisation over the numeric types: ring identities over the integers, the reals and the naturals, elementary divisibility, field facts with their side conditions, and the ideal-membership conversion that produces the certificate behind them.

hol_theorem integer_rule(hol_term tm);

hol_theorem integer_rule(hol_term tm);

Automatically prove elementary divisibility property over the integers.

• raises — Fails if the goal is not accessible to the methods used.

hol_theorem int_ring_rule(hol_term tm);

hol_theorem int_ring_rule(hol_term tm);

Ring decision procedure instantiated to integers.

• raises — Fails if the formula is unprovable by the methods employed.

hol_theorem real_ring_rule(hol_term tm);

hol_theorem real_ring_rule(hol_term tm);

Ring decision procedure instantiated to real numbers.

• raises — Fails if the formula is unprovable by the methods employed.

hol_theorem num_ring_rule(hol_term tm);

hol_theorem num_ring_rule(hol_term tm);

Ring decision procedure instantiated to natural numbers.

• raises — Fails if the formula is unprovable by the methods employed.

hol_theorem real_field_rule(hol_term tm);

hol_theorem real_field_rule(hol_term tm);

Prove basic field facts over the reals.

• raises — Fails if the term is not provable using the methods described.

hol_conversion real_ideal_conv(hol_term_list tms);

hol_conversion real_ideal_conv(hol_term_list tms);

Produces identity proving ideal membership over the reals.

• raises — Fails if the terms are ill-typed, or if ideal membership fails.

Goals about fixed-width words, which is where C* verification tends to land once a specification talks about the bit-level meaning of an integer type. The four word_*word_* rules escalate from algebraic reasoning to full bit-level expansion, and bitblast_rulebitblast_rule reduces the goal to a BDD computation.

hol_theorem word_rule(hol_term tm);

hol_theorem word_rule(hol_term tm);

Proves for simple algebraic properties about machine words. May fail.

hol_theorem word_bitwise_rule(hol_term tm);

hol_theorem word_bitwise_rule(hol_term tm);

Proves for bitwise-type properties of logical operations about machine words. May fail.

hol_theorem word_arith_rule(hol_term tm);

hol_theorem word_arith_rule(hol_term tm);

Proves for things involving numerical values about machine words. May fail.

hol_theorem word_blast_rule(hol_term tm);

hol_theorem word_blast_rule(hol_term tm);

Proves for fixed-size bitwise expansions followed by arithmetic about machine words. May fail.

hol_theorem bitblast_rule(hol_term tm);

hol_theorem bitblast_rule(hol_term tm);

A BDD-based "flattening" or "bit-blasting" rule about machine words. May fail.

hol_theorem set_rule(hol_term tm);

hol_theorem set_rule(hol_term tm);

Attempt to prove elementary set-theoretic lemma (via MESON).

• raises — Fails if the simple translation does not suffice, or the resulting goal is too deep for MESON.

The tail of the header is not sorted by subject: rules, definition forms and session control are interleaved with the conversions. Those declarations are documented on the pages where they belong, and listed here so that this stretch of the header is accounted for.

Four inference rules declared this late are documented with the rest of the rules on HOL API: Inference Rules:

Definition forms and the accessors for the theorems a datatype definition generates are covered by HOL API: Theories and Theorems:

So are the theorem database and the session controls — checkpoints, snapshots and handle release:

String and numeral literals, variable generation, type equality and the composition of instantiations are covered by HOL API: Types and Terms:

Type abbreviations and the implicit-type context belong with the rest of the theory state on HOL API: Theories and Theorems:

A conversion is a term-to-equation function; the combinators aim it at a subterm and control how far it repeats; rewriting is the standard instance of that pattern; and the solvers close whole goals in one call within the fragment each of them decides. Together with the inference rules of the previous page, this is the complete user-facing surface of hol_prover_client.hhol_prover_client.h, and the end of the kernel-header group.