HOL API：理论与定理

本页承接HOL API：类型与项，继续介绍 HOL Light 的 RPC 客户端 hol_prover_client.hhol_prover_client.h。上一页的约定仍然适用：每次调用都会记录状态，由 get_last_status()get_last_status() 报告、get_last_error()get_last_error() 解释；调用失败时返回 empty_*empty_* 哨兵值而非 NULLNULL，用 IS_NULLIS_NULL 检测；所有返回的指针都由垃圾回收管理；头文件由证明器的接口描述生成。

上一页讨论语法，本页则讨论哪些命题为真。hol_theoremhol_theorem 是本 API 中唯一表达断言的对象，获取它只有三种途径：从理论中查找定理，用新的定义或公理扩展理论，或对已有定理应用推理规则。本页介绍前两种；第三种见HOL API：推理规则。

一条定理就是一个相继式，由假设列表和结论组成，写作 A |- tA |- t。只有下面三个函数可以查看定理的内部结构，它们都不会失败。

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 通过一个 dest_thm_resultsdest_thm_results 结构体同时返回这两个部分：字段 tmstms 保存假设，tmtm 保存结论；hyphyp 与 conclconcl 则分别提取假设和结论。如果假设列表为空，这条定理就在当前理论中无条件成立；如果带有假设，结论就只在这些假设下成立。disch_ruledisch_rule 与 undisch_ruleundisch_rule 可以在假设与蕴含之间相互转换。

理论就是证明器的全局状态，包括已有的类型构造子、常量及其泛型类型、已假设的公理，以及已导出的定义定理。本节的每个函数都会修改理论，其中多数函数在要引入的名字已被占用时会失败。

两个原始声明分别引入一个给定元数的类型构造子和一个给定类型的常量，但都不为名字赋予任何定义性质。声明不会证明它们的任何性质；只有公理或定义才能说明它们的含义。

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 的作用有所不同：类型缩写由解析器和打印器展开，并不存在于逻辑中。

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.

公理是未经证明的假设，基于 LCF 架构的证明所介绍的方法正是为了避免依赖这样的假设。API 仍然提供 new_axiomnew_axiom，但 C* 证明库已经不再需要它：带类型的内存谓词中的每一条带类型内存规则都已得到证明。因此，剩下的公理只能来自客户端。证明块添加的公理会按添加顺序列入验证报告的 axiomsaxioms 数组（见符号执行与运行时 API页的 cst_print_vccst_print_vc）。如果该数组非空，这次运行就不能算作一份完成的证明。

定义在引入常量的同时返回刻画该常量的定理，因此可以扩展理论而不增加任何假设。各种定义形式的区别在于所接受的等式形式。

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 处理原始形式 c = tc = t；new_const_definitionnew_const_definition 接受柯里化形式 c v1 ... vn = tc v1 ... vn = t，并自动对参数作抽象；new_fun_definitionnew_fun_definition 接受一般的递归定义，并自动卸除可容许性条件。new_rec_definitionnew_rec_definition 用于定义归纳类型上的递归，需要提供该类型的递归定理；两个 prove_*_existsprove_*_exists 函数单独提供存在性证明这一步，供需要手工控制自动定义机制的场合使用。new_specificationnew_specification 根据一条已证明的存在定理引入一个或多个常量：当一个值由性质而非表达式刻画时，可以用这种方式为它命名。

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 是 HOL Light 的原始操作：给定定理 |- P x|- P x，以此作为已有类型的某个子集非空的例证，该函数引入一个与此子集之间存在双射的新类型，并返回两条定理，描述抽象函数与表示函数之间的关系。new_type_bijection_definitionnew_type_bijection_definition 是它的变体，接受存在量化的例证。

证明代码实际使用的是余下两种形式。new_datatype_definitionnew_datatype_definition 接受一个代数数据类型的文本描述，返回它的归纳定理与递归定理；new_inductive_definitionnew_inductive_definition 将一个关系定义为在一组子句下封闭的最小关系，返回规则、归纳原理和分情形定理。

证明器按名字存储和索引定理，也支持枚举理论本身。借助这两种方式，证明代码可以查找在本地证明之外已有的内容。

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 返回 falsefalse，但调用不会失败。因此，在一次会话中重复注册同一条定理时，无需检查状态就能发现重复。get_theorem_by_nameget_theorem_by_name 遇到未知名字时则会失败。

枚举函数报告理论当前包含的内容：

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.

由 new_datatype_definitionnew_datatype_definition 引入的归纳类型还附带一些定理。这些定理按类型名获取，不以定理名存储：

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.

这四个函数是对用户自定义数据类型进行推理的标准工具：get_datatype_inductget_datatype_induct 用于结构归纳，get_datatype_casesget_datatype_cases 用于分情形讨论，get_datatype_distinctnessget_datatype_distinctness 与 get_datatype_injectivityget_datatype_injectivity 则分别给出“不同构造子产生不同的值”和“构造子对其参数是单射的”这两条事实。

用 mk_combmk_comb 和 mk_constmk_const 构造项很精确，但写法冗长。另一种做法是用具体语法写出项，交给证明器解析。解析器接受的语法见HOL Light 语法及C* 的扩展，也就是 C* 源文件中反引号之间所用的记号。

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.

遇到语法错误或末尾有未解析的输入时，解析会失败；string_of_*string_of_* 打印函数则从不失败。它们输出的记号可以由解析器接受，因此错误信息中打印的项可以直接粘贴回源文件。

cst_assertion_stringcst_assertion_string 是 C* 在这组函数中增加的打印函数。它将一个 hprophprop 或 boolbool 项渲染为符号执行引擎的断言语法，即引擎在符号状态转储和错误信息中使用的写法。运行时的 cst_print_assertioncst_print_assertion（见符号执行与运行时 API）就是通过它完成打印的：整个项被发送到服务器端渲染，无需逐个遍历节点。与其他打印函数不同，如果项中包含无法渲染的节点，这个函数就会失败。

解析含有自由变量的项时，需要确定这些变量的类型。这由隐式类型上下文决定：

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 将具名变量限定为某个类型或类型模式，使后续的 parse_termparse_term 无需显式标注就能确定这些变量的类型。多数 C* 断言看上去不带类型，依靠的正是这一机制：引擎先将作用域内程序变量的隐式类型写入上下文，再解析使用这些变量的规约。

定理就是一个相继式，由假设和结论组成，可以用 dest_thmdest_thm、hyphyp 和 conclconcl 读取。定理只有两类生成方式：一类是扩展理论，包括增设公理，以及返回刻画定理的各种定义形式；另一类是应用推理规则。理论是全局的，可以枚举，也可以按名字索引；解析器与打印器将它与具体语法联系起来。

开头列出的第三种获取定理的途径最为常见，但尚未在本页介绍：本页的函数都不能将一条定理变换为另一条定理。