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 架构的证明所描述的纪律，恰恰就是无需公理的纪律。new_axiomnew_axiom 之所以仍然属于本 API，是因为 C* 内存模型用到了它：带类型的内存谓词中的带类型内存规则正是作为公理引入的，在本参考手册中凡出现之处都会如此标注。

一次定义在引入常量的同时返回刻画该常量的定理，因此理论的增长不带来任何新的假设。各种定义形式的区别，在于它们接受的等式形状。

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.

遇到语法错误、或末尾有未解析完的输入时，解析会失败；打印则从不失败。string_of_*string_of_* 函数产生的记号正是解析器所接受的记号，因此打印到错误信息里的项可以直接粘回源文件。

解析带自由变量的项时，随之而来的问题是这些变量具有什么类型。隐式类型上下文给出了答案：

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* 断言看上去不带类型，背后正是这一机制：引擎在解析提到这些变量的规约之前，先把作用域内程序变量的隐式类型写入上下文。

最后一组管理的是证明器随时间演进的状态，而非逻辑内容。一个检查点记录整个理论；恢复某个检查点会把理论回滚，并使此后创建的所有对象句柄失效。

int checkpoint();

int checkpoint();

Saves an in-memory checkpoint of all theory state and returns its id. Checkpoints are session-scoped: they do not survive a server restart.

• raises — Never fails.

void restore(int id);

void restore(int id);

Rolls all theory state back to the given checkpoint. Object handles created after the checkpoint become invalid (using one returns an error); handles created before it stay valid. Checkpoints newer than the restored one are dropped. When the server runs with a state directory, the journal is truncated accordingly, so the rollback also survives a restart.

• raises — Fails if the checkpoint id is unknown.

int_list list_checkpoints();

int_list list_checkpoints();

Lists the ids of all live checkpoints.

• raises — Never fails.

void drop_checkpoint(int id);

void drop_checkpoint(int id);

Discards a checkpoint without restoring it.

• raises — Fails if the checkpoint id is unknown.

cstr save_snapshot();

cstr save_snapshot();

Forces a warm-start snapshot to be written now (normally written on graceful shutdown). Returns the snapshot path, or "" when the server runs without a state directory.

• raises — Never fails.

void release_handles();

void release_handles();

Frees every object handle (type, term, theorem, conversion) that is NOT protected by a live checkpoint, unpinning the underlying OCaml GC roots so the OCaml GC can reclaim them. Checkpoints and the handles they depend on are preserved; theory state (constants, axioms, definitions) is NOT rolled back. With no live checkpoints this frees ALL handles. Intended to be called at a session boundary.

• raises — Never fails.

定理就是一个相继式，仅此而已：一组假设加一个结论，用 dest_thmdest_thm、hyphyp 和 conclconcl 读取。它进入这个世界的方式只有两类：或者因为理论被扩展——一次声明、一条公理，或某种返回自身刻画定理的定义形式——或者因为某条推理规则产生了它。理论是全局的、可枚举的、按名字索引的；解析器与打印器把它同具体语法连接起来；会话函数则让长时间运行的证明器可以把这一切回滚。

本页缺少的，是定理的第三个来源，也是最常见的来源。这里没有任何东西能把一条定理变换为另一条定理。