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：理论与定理页：

变换是从项到等式的函数；组合子把它对准某个子项，并控制它重复到什么程度；重写是这一 模式的标准实例；求解器则在各自判定的片段之内，一次调用即解决整个目标。连同上一页的 推理规则，这就是 hol_prover_client.hhol_prover_client.h 面向用户的完整接口，也是内核头文件这一组的 终点。