HOL API：变换与求解器

上一页介绍的规则接受定理并产生定理。本页介绍 hol_prover_client.hhol_prover_client.h 生成定理的另外两种方式：变换重写一个项，并返回为这次重写提供依据的等式；求解器接受一个项，证明后返回相应的定理。

两者都能省去证明代码中手工处理命题的工作。符号执行留下的纯化义务通常只是常规的数学问题，例如算术、机器字恒等式，或展开某个定义便能得到的等式。本页这部分 API 让我们通过一次调用解决这类目标，无需逐步使用原始规则。

变换是从项到定理的函数：给定 tt，它返回 |- t = t'|- t = t'，这条等式就是将 tt 替换为 t't' 的依据。整套重写机制都由变换构成。类型 hol_conversionhol_conversion 表示指向变换的不透明句柄，与 hol_termhol_term、hol_theoremhol_theorem 的用法相同。

变换可以命名，证明器会维护这些命名变换的环境：add_conversionadd_conversion 按给定名称注册变换， list_conversionslist_conversions 列出已使用的名称，get_conversion_by_nameget_conversion_by_name 按名称获取变换。这样，一个证明函数就能使用另一个证明函数中构造的变换，也能获取引擎安装的变换。 apply_conversionapply_conversion 对一个项应用变换，得到相应的等式；conv_ruleconv_rule 则将变换提升为规则，对定理的结论应用变换，就地重写该定理。

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.

变换单独使用时，会在顶层重写传入的整个项。下面的组合子可以控制变换的应用位置和方式，分为三类。

组合变换：then_convthen_conv 将两个变换按顺序串联，orelse_convorelse_conv 在第一个变换失败时尝试第二个， every_convevery_conv 与 first_convfirst_conv 是两者对应的列表形式。try_convtry_conv 在变换失败时返回恒等变换的结果，changed_convchanged_conv 则在变换未产生变化时失败，从而让重复应用变换的过程终止。 cache_convcache_conv 用于记忆化。

遍历：depth_convdepth_conv、once_depth_convonce_depth_conv、redepth_convredepth_conv、top_depth_convtop_depth_conv 与 top_sweep_convtop_sweep_conv 将变换应用到项的各处，区别在于遍历方向（自底向上还是自顶向下）、是否重复，以及是否重新访问已经改写过的子项。重复应用变换的组合子可能导致发散，头文件在相应条目中逐一说明了这一点。

定位：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 与 pat_convpat_conv 将变换应用到项的特定部分，例如运算符、操作数、抽象或绑定子的体、二元运算符的某一侧、路径字符串指定的位置，或模式匹配到的子项。

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.

重写是上述机制的标准用法：将一个等式定理列表转换为一个变换，再将它应用到项的各处，直到不再产生变化。这类函数虽然数量较多，但命名有规律，可以从名称判断各函数的行为。

_conv_conv 重写一个项，_rule_rule 重写一条定理的结论。前缀 pure_pure_ 表示只使用所提供的定理，不使用普通形式附加的内置重言式与标准化简。前缀 once_once_ 表示只遍历一次，不重复到不动点，从而避免普通形式的说明中警告的发散问题。前缀 asm_asm_ 表示将定理自身的假设也用作重写规则。simpsimp 系列比 rewriterewrite 系列更强：它们根据上下文执行带条件的化简，并在此过程中卸除附加条件，通常是证明时首先使用的工具。

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.

本节的函数接受一个项，成功时返回证明该项的定理，否则失败。在本 API 中，这些函数单次调用能完成的工作最多，结果却最难预测：每个函数都对某个特定片段完备，超出这个片段则会失败。因此，使用时的关键是判断目标属于哪个片段。

这类函数以给定的定理列表为背景理论，在一阶逻辑上执行通用证明搜索。 meson_solvermeson_solver 是常用的求解器；其余几个采用不同的搜索策略，一个求解器无法证明的目标，有时另一个立即就能证明。

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.

这类函数处理数值类型上的代数规范化，包括整数、实数与自然数上的环恒等式、初等整除性、带附加条件的域事实，以及为这些结果生成证书的理想成员变换。

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.

这类函数处理定宽字的目标。规约一旦涉及某个整数类型在位层面的含义，C* 验证往往就会产生这类目标。四条 word_*word_* 规则提供的推理方式从代数推理逐步扩展到完整的位层展开， bitblast_rulebitblast_rule 则将目标归约为一次 BDD 计算。

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.

头文件尾部没有按主题排序，推理规则、定义形式和少数工具链内部函数与变换交错排列。这些声明的文档位于各自所属的页面，内部函数则只列出名称。本节汇总这些条目，以确认头文件的这一段已被完整覆盖。

在头文件尾部声明的四条推理规则，与其他规则一同列于 HOL API：推理规则页：

定义形式及相应的访问器详见 HOL API：理论与定理页，这些访问器用于获取数据类型定义所生成的定理：

在此声明的两个定理数据库函数同样详见该页：

字符串与数值字面量、变量生成、类型相等性以及实例化的复合，详见 HOL API：类型与项页：

类型缩写与隐式类型上下文，与理论状态的其他部分一同列于 HOL API：理论与定理页：

C* 的断言打印器也在该页的解析与打印一节介绍：

这一区间剩余的声明是工具链内部函数（证明器会话与项的结构转储），不属于证明块 API：

变换是从项到等式的函数；组合子指定变换作用的子项，并控制重复应用的过程；重写是这一模式的标准实例；求解器则在各自能判定的片段内，通过一次调用解决整个目标。加上上一页的推理规则，我们便介绍了 hol_prover_client.hhol_prover_client.h 面向用户的完整接口，内核头文件这一组参考页也到此结束。