HOL API：推理规则

hol_prover_client.hhol_prover_client.h 提供证明助手的客户端接口，其中声明的每个函数都用一层简单的 C 封装，将调用转发给由 C* 符号执行引擎驱动的 HOL Light 进程。接口传递的 hol_termhol_term、 hol_theoremhol_theorem、hol_typehol_type、hol_conversionhol_conversion 都是只含一个字段的不透明结构体，保存着指向该进程中对象的句柄。接口返回的所有对象，包括 cstrcstr 字符串，都由工具链链接的垃圾回收器管理，无需手动释放。

规则应用失败时，除了返回空的哨兵值（empty_theoremempty_theorem、empty_termempty_term、empty_typeempty_type、 empty_conversionempty_conversion 或空列表），还会记录失败原因。IS_NULLIS_NULL 用于检测这类返回值， get_last_status()get_last_status() 与 get_last_error()get_last_error() 则分别获取状态码与错误消息。头文件建议检查状态而非返回值；证明代码通常用 proof_util.hproof_util.h 的 TRYTRY 与 ENSUREENSURE 宏完成这项检查，详见符号执行与运行时 API页。

下列条目的 raises 一行说明规则会在什么情况下失败，内容取自头文件；其中 never fails（不会失败）的说法也来自头文件。

这十条规则分为三组：从 refl_rulerefl_rule 到 beta_prim_rulebeta_prim_rule 的等式规则沿项的结构，依据合同性质构造等式定理；assume_ruleassume_rule、eq_mp_ruleeq_mp_rule 与 deduct_antisym_rulededuct_antisym_rule 三条命题规则引入与卸除假设，支持逻辑中的蕴含推理；两条实例化规则则分别替换类型变量和自由项变量。

hol_theorem refl_rule(hol_term tm);

hol_theorem refl_rule(hol_term tm);

----------  REFL
 |- t = t

----------  REFL
 |- t = t

Returns theorem expressing reflexivity of equality.

• raises — Never fails.

hol_theorem trans_rule(hol_theorem th1, hol_theorem th2);

hol_theorem trans_rule(hol_theorem th1, hol_theorem th2);

 A1 |- t1 = t2   A2 |- t2' = t3
--------------------------------  TRANS
      A1 u A2 |- t1 = t3

 A1 |- t1 = t2   A2 |- t2' = t3
--------------------------------  TRANS
      A1 u A2 |- t1 = t3

Uses transitivity of equality on two equational theorems.

• raises — Fails unless the theorems are equational, with the right side of the first being the same as the left side of the second, up to alpha-equivalence.

hol_theorem mk_comb_rule(hol_theorem th1, hol_theorem th2);

hol_theorem mk_comb_rule(hol_theorem th1, hol_theorem th2);

    A1 |- f = g   A2 |- x = y
   ---------------------------  MK_COMB
       A1 u A2 |- f x = g y

    A1 |- f = g   A2 |- x = y
   ---------------------------  MK_COMB
       A1 u A2 |- f x = g y

Proves equality of combinations constructed from equal functions and operands.

• raises — Fails unless both theorems are equational and f and g are functions whose domain types are the same as the types of x and y respectively.

hol_theorem abs_rule(hol_term tm, hol_theorem th);

hol_theorem abs_rule(hol_term tm, hol_theorem th);

      A |- t1 = t2
------------------------  ABS `x`            [Where x is not free in A]
 A |- (\x.t1) = (\x.t2)

      A |- t1 = t2
------------------------  ABS `x`            [Where x is not free in A]
 A |- (\x.t1) = (\x.t2)

Abstracts both sides of an equation.

• raises — Fails if the theorem is not an equation, or if the variable x is free in the assumptions A.

hol_theorem beta_prim_rule(hol_term tm);

hol_theorem beta_prim_rule(hol_term tm);

------------------------  BETA
 |- (\x. t[x]) x = t[x]

------------------------  BETA
 |- (\x. t[x]) x = t[x]

Special primitive case of beta-reduction.

• raises — Fails if the term is not of the required form.

hol_theorem assume_rule(hol_term tm);

hol_theorem assume_rule(hol_term tm);

--------  ASSUME `t`
 t |- t

--------  ASSUME `t`
 t |- t

Introduces an assumption.

• raises — Fails unless the term t has type bool.

hol_theorem eq_mp_rule(hol_theorem th1, hol_theorem th2);

hol_theorem eq_mp_rule(hol_theorem th1, hol_theorem th2);

 A1 |- t1 <=> t2   A2 |- t1'
-----------------------------  EQ_MP
      A1 u A2 |- t2

 A1 |- t1 <=> t2   A2 |- t1'
-----------------------------  EQ_MP
      A1 u A2 |- t2

Equality version of the Modus Ponens rule.

• raises — Fails unless the first theorem is equational and its left side is the same as the conclusion of the second theorem (and is therefore of type bool), up to alpha-conversion.

hol_theorem deduct_antisym_rule(hol_theorem th1, hol_theorem th2);

hol_theorem deduct_antisym_rule(hol_theorem th1, hol_theorem th2);

      A |- p       B |- q
----------------------------------  DEDUCT_ANTISYM
 (A - {q}) u (B - {p}) |- p <=> q

      A |- p       B |- q
----------------------------------  DEDUCT_ANTISYM
 (A - {q}) u (B - {p}) |- p <=> q

Deduces logical equivalence from deduction in both directions.

• raises — Never fails.

hol_theorem inst_type_rule(hol_type_pair_list ty_pairs, hol_theorem th);

hol_theorem inst_type_rule(hol_type_pair_list ty_pairs, hol_theorem th);

            A |- t
-----------------------------------  INST_TYPE [ty1,tv1;...;tyn,tvn]
 A[ty1,...,tyn/tv1,...,tvn]
     |- t[ty1,...,tyn/tv1,...,tvn]

            A |- t
-----------------------------------  INST_TYPE [ty1,tv1;...;tyn,tvn]
 A[ty1,...,tyn/tv1,...,tvn]
     |- t[ty1,...,tyn/tv1,...,tvn]

Instantiates types in a theorem.

• raises — Never fails.

hol_theorem inst_rule(hol_term_pair_list tm_pairs, hol_theorem th);

hol_theorem inst_rule(hol_term_pair_list tm_pairs, hol_theorem th);

            A |- t
-------------------------------  INST [t1,x1;...;tn,xn]
 A[t1,...,tn/x1,...,xn]
     |- t[t1,...,tn/x1,...,xn]

            A |- t
-------------------------------  INST [t1,x1;...;tn,xn]
 A[t1,...,tn/x1,...,xn]
     |- t[t1,...,tn/x1,...,xn]

Instantiates free variables in a theorem.

• raises — Fails if any of the pairs ti,xi in the instantiation list has xi and ti with different types, or xi a non-variable. Multiple instances of the same xi in the list are not trapped, but only the first one will be used consistently.

以下都是派生规则。无论实现多么复杂，返回的定理都由原始推理步骤构造而成。例如， arith_rulearith_rule 运行一整套线性算术判定过程，也遵循这一原则。因此，这里按规则对目标的作用分组，而不按实现所需的工作量分组。

头文件用推理规则图给出大多数规则，横线右侧标注了规则在 HOL Light 策略层中的名称： spec_rulespec_rule 对应 HOL Light 的 SPECSPEC，mp_rulemp_rule 对应 MPMP。阅读 HOL Light 资料时，可以根据这一对应关系查找规则：这些名称指的都是本页中的同一批规则。

这组规则用于操作等式：对两边应用同一个函数、反转等式、归约等式，或依据某个运算符的结合律与交换律将等式规范化。

hol_theorem ac_rule(hol_theorem th, hol_term tm);

hol_theorem ac_rule(hol_theorem th, hol_term tm);

Proves equality of terms using associative, commutative, and optionally idempotence laws.

• raises — Fails if the terms are not proved equivalent under the appropriate laws. This may happen because the input theorem does not have the correct canonical form. Examples: AC ADD_AC 1 + 2 + 3 = 2 + 1 + 31 + 2 + 3 = 2 + 1 + 3 yield |- 1 + 2 + 3 = 2 + 1 + 3 AC CONJ_ACI p /\ (q /\ p) <=> (p /\ q) /\ (p /\ q)p /\ (q /\ p) <=> (p /\ q) /\ (p /\ q) yield |- p /\ q /\ p <=> (p /\ q) /\ p /\ q

hol_theorem ap_term_rule(hol_term tm, hol_theorem th);

hol_theorem ap_term_rule(hol_term tm, hol_theorem th);

   A |- x = y
----------------  AP_TERM `f`
 A |- f x = f y

   A |- x = y
----------------  AP_TERM `f`
 A |- f x = f y

Applies a function to both sides of an equational theorem.

• raises — Fails unless the theorem is equational and the supplied term is a function whose domain type is the same as the type of both sides of the equation.

hol_theorem ap_thm_rule(hol_theorem th, hol_term tm);

hol_theorem ap_thm_rule(hol_theorem th, hol_term tm);

   A |- f = g
----------------  AP_THM (A |- f = g) `x`
 A |- f x = g x

   A |- f = g
----------------  AP_THM (A |- f = g) `x`
 A |- f x = g x

Proves equality of equal functions applied to a term.

• raises — Fails unless the conclusion of the theorem is an equation, both sides of which are functions whose domain type is the same as that of the supplied term.

hol_theorem beta_rule(hol_theorem th);

hol_theorem beta_rule(hol_theorem th);

 A |- ....((\x. s1) s2)....
----------------------------  BETA_RULE
   A |- ....(s1[s2/x])....

 A |- ....((\x. s1) s2)....
----------------------------  BETA_RULE
   A |- ....(s1[s2/x])....

Beta-reduces all the beta-redexes in the conclusion of a theorem.

• raises — Never fails.

hol_theorem gsym_rule(hol_theorem th);

hol_theorem gsym_rule(hol_theorem th);

 A |- ..(s1 = s2)...(t1 = t2)..
--------------------------------  GSYM
 A |- ..(s2 = s1)...(t2 = t1)..

 A |- ..(s1 = s2)...(t1 = t2)..
--------------------------------  GSYM
 A |- ..(s2 = s1)...(t2 = t1)..

Reverses the first equation(s) encountered in a top-down search.

• raises — Never fails.

hol_theorem sym_rule(hol_theorem th);

hol_theorem sym_rule(hol_theorem th);

 A |- t1 = t2
--------------  SYM
 A |- t2 = t1

 A |- t1 = t2
--------------  SYM
 A |- t2 = t1

Swaps left-hand and right-hand sides of an equation.

• raises — Fails unless the theorem is equational.

hol_theorem alpha_rule(hol_term tm1, hol_term tm2);

hol_theorem alpha_rule(hol_term tm1, hol_term tm2);

-------------  ALPHA `t1` `t1'`
 |- t1 = t1'

-------------  ALPHA `t1` `t1'`
 |- t1 = t1'

Proves equality of alpha-equivalent terms.

• raises — Fails unless the terms provided are alpha-equivalent.

这组规则处理合取、蕴含、析取，以及与真值相等的两种形式。mp_rulemp_rule 就是假言推理； match_mp_rulematch_mp_rule 则先将蕴含式实例化，证明脚本引用一般引理时通常需要后一种规则。

hol_theorem conj_rule(hol_theorem th1, hol_theorem th2);

hol_theorem conj_rule(hol_theorem th1, hol_theorem th2);

 A1 |- t1      A2 |- t2
------------------------  CONJ
  A1 u A2 |- t1 /\ t2

 A1 |- t1      A2 |- t2
------------------------  CONJ
  A1 u A2 |- t1 /\ t2

Introduces a conjunction.

• raises — Never fails.

hol_theorem conjunct1_rule(hol_theorem th);

hol_theorem conjunct1_rule(hol_theorem th);

 A |- t1 /\ t2
---------------  CONJUNCT1
    A |- t1

 A |- t1 /\ t2
---------------  CONJUNCT1
    A |- t1

Extracts left conjunct of theorem.

• raises — Fails unless the input theorem is a conjunction.

hol_theorem conjunct2_rule(hol_theorem th);

hol_theorem conjunct2_rule(hol_theorem th);

 A |- t1 /\ t2
---------------  CONJUNCT2
    A |- t2

 A |- t1 /\ t2
---------------  CONJUNCT2
    A |- t2

Extracts right conjunct of theorem.

• raises — Fails unless the input theorem is a conjunction.

hol_theorem disch_rule(hol_term tm, hol_theorem th);

hol_theorem disch_rule(hol_term tm, hol_theorem th);

       A |- t
--------------------  DISCH `u`
 A - {u} |- u ==> t

       A |- t
--------------------  DISCH `u`
 A - {u} |- u ==> t

Discharges an assumption.

• raises — Fails if u is not of type bool.

hol_theorem disch_all_rule(hol_theorem th);

hol_theorem disch_all_rule(hol_theorem th);

      A1, ..., An |- t
----------------------------  DISCH_ALL
 |- A1 ==> ... ==> An ==> t

      A1, ..., An |- t
----------------------------  DISCH_ALL
 |- A1 ==> ... ==> An ==> t

Discharges all hypotheses of a theorem.

• raises — Never fails.

hol_theorem eqt_elim_rule(hol_theorem th);

hol_theorem eqt_elim_rule(hol_theorem th);

 A |- tm <=> T
---------------  EQT_ELIM
   A |- tm

 A |- tm <=> T
---------------  EQT_ELIM
   A |- tm

Eliminates equality with true.

• raises — Fails if the argument theorem is not of the form A |- tm <=> T.

hol_theorem eqt_intro_rule(hol_theorem th);

hol_theorem eqt_intro_rule(hol_theorem th);

   A |- tm
---------------  EQT_INTRO
 A |- tm <=> T

   A |- tm
---------------  EQT_INTRO
 A |- tm <=> T

Introduces equality with true.

• raises — Never fails.

hol_theorem match_mp_rule(hol_theorem th1, hol_theorem th2);

hol_theorem match_mp_rule(hol_theorem th1, hol_theorem th2);

 A1 |- !x1..xn. t1 ==> t2   A2 |- t1'
--------------------------------------  MATCH_MP
       A1 u A2 |- !xa..xk. t2'

 A1 |- !x1..xn. t1 ==> t2   A2 |- t1'
--------------------------------------  MATCH_MP
       A1 u A2 |- !xa..xk. t2'

Modus Ponens inference rule with automatic matching.

• raises — Fails unless the first theorem is a (possibly repeatedly universally quantified) implication whose antecedent can be instantiated to match the conclusion of the second theorem, without instantiating any variables which are free in A1, the first theorem's assumption list.

hol_theorem mp_rule(hol_theorem th1, hol_theorem th2);

hol_theorem mp_rule(hol_theorem th1, hol_theorem th2);

 A1 |- t1 ==> t2   A2 |- t1
----------------------------  MP
       A1 u A2 |- t2

 A1 |- t1 ==> t2   A2 |- t1
----------------------------  MP
       A1 u A2 |- t2

Implements the Modus Ponens inference rule.

• raises — Fails unless the first theorem is an implication whose antecedent is the same as the conclusion of the second theorem (up to alpha-conversion).

hol_theorem prove_hyp_rule(hol_theorem th1, hol_theorem th2);

hol_theorem prove_hyp_rule(hol_theorem th1, hol_theorem th2);

  A1 |- t1     A2 |- t2
-------------------------  PROVE_HYP
  A1 u (A2 - {t1}) |- t2

  A1 |- t1     A2 |- t2
-------------------------  PROVE_HYP
  A1 u (A2 - {t1}) |- t2

Eliminates a provable assumption from a theorem.

• raises — Never fails.

hol_theorem taut_rule(hol_term tm);

hol_theorem taut_rule(hol_term tm);

Proves a propositional tautology.

• raises — Fails if the term is not a propositional tautology.

hol_theorem undisch_rule(hol_theorem th);

hol_theorem undisch_rule(hol_theorem th);

 A |- t1 ==> t2
----------------  UNDISCH
  A, t1 |- t2

 A |- t1 ==> t2
----------------  UNDISCH
  A, t1 |- t2

Undischarges the antecedent of an implicative theorem.

• raises — Fails if the theorem is not an implication.

hol_theorem disj1_rule(hol_theorem th, hol_term tm);

hol_theorem disj1_rule(hol_theorem th, hol_term tm);

    A |- t1
---------------  DISJ1 (A |- t1) `t2`
 A |- t1 \/ t2

    A |- t1
---------------  DISJ1 (A |- t1) `t2`
 A |- t1 \/ t2

Introduces a right disjunct into the conclusion of a theorem.

• raises — Fails unless the term argument is of type bool.

hol_theorem disj2_rule(hol_term tm, hol_theorem th);

hol_theorem disj2_rule(hol_term tm, hol_theorem th);

   A |- t2
---------------  DISJ2 `t1`
 A |- t1 \/ t2

   A |- t2
---------------  DISJ2 `t1`
 A |- t1 \/ t2

Introduces a left disjunct into the conclusion of a theorem.

• raises — Fails if the term argument is not of type bool.

hol_theorem disj_cases_rule(hol_theorem th1, hol_theorem th2, hol_theorem th3);

hol_theorem disj_cases_rule(hol_theorem th1, hol_theorem th2, hol_theorem th3);

      A |- t1 \/ t2     A1 |- t      A2 |- t
--------------------------------------------------  DISJ_CASES
      A u (A1 - {t1}) u (A2 - {t2}) |- t

      A |- t1 \/ t2     A1 |- t      A2 |- t
--------------------------------------------------  DISJ_CASES
      A u (A1 - {t1}) u (A2 - {t2}) |- t

Eliminates disjunction by cases.

• raises — Fails if the first argument is not a disjunctive theorem, or if the conclusions of the other two theorems are not alpha-convertible.

hol_theorem eqf_elim_rule(hol_theorem th);

hol_theorem eqf_elim_rule(hol_theorem th);

 A |- tm <=> F
---------------  EQF_ELIM
   A |- ~tm

 A |- tm <=> F
---------------  EQF_ELIM
   A |- ~tm

Eliminates equality with false.

• raises — Fails if the argument theorem is not of the form A |- tm <=> F.

hol_theorem eqf_intro_rule(hol_theorem th);

hol_theorem eqf_intro_rule(hol_theorem th);

   A |- ~tm
---------------  EQF_INTRO
 A |- tm <=> F

   A |- ~tm
---------------  EQF_INTRO
 A |- tm <=> F

Introduces equality with false.

• raises — Fails if the argument theorem is not a negation.

这组规则用于引入与消去 !! 和 ??。specspec 系列将全称量词实例化，ispecispec 系列还会同时将类型实例化；gen_rulegen_rule 及其变体用于全称化，前提是相应变量不出现在假设之中。

hol_theorem gen_rule(hol_term v, hol_theorem th);

hol_theorem gen_rule(hol_term v, hol_theorem th);

   A |- t
------------  GEN `x`                [where x is not free in A]
 A |- !x. t

   A |- t
------------  GEN `x`                [where x is not free in A]
 A |- !x. t

Generalizes the conclusion of a theorem.

• raises — Fails if x is not a variable, or if it is free in any of the assumptions.

hol_theorem genl_rule(hol_term_list vs, hol_theorem th);

hol_theorem genl_rule(hol_term_list vs, hol_theorem th);

      A |- t
------------------  GENL `[x1;...;xn]`       [where no xi is free in A]
 A |- !x1...xn. t

      A |- t
------------------  GENL `[x1;...;xn]`       [where no xi is free in A]
 A |- !x1...xn. t

Generalizes zero or more variables in the conclusion of a theorem.

• raises — Fails unless all the terms in the list are variables, none of which are free in the assumption list.

hol_theorem gen_all_rule(hol_theorem th);

hol_theorem gen_all_rule(hol_theorem th);

      A |- t
------------------  GEN_ALL
 A |- !x1...xn. t

      A |- t
------------------  GEN_ALL
 A |- !x1...xn. t

Generalizes the conclusion of a theorem over its own free variables.

• raises — Never fails.

hol_theorem ispec_rule(hol_term tm, hol_theorem th);

hol_theorem ispec_rule(hol_term tm, hol_theorem th);

   A |- !x:ty.tm
----------------------  ISPEC `t:ty'`
 A[ty'/ty] |- tm[t/x]

   A |- !x:ty.tm
----------------------  ISPEC `t:ty'`
 A[ty'/ty] |- tm[t/x]

Specializes a theorem, with type instantiation if necessary.

• raises — Fails if the input theorem is not universally quantified, or if the type of the given term is not an instance of the type of the quantified variable.

hol_theorem ispecl_rule(hol_term_list tms, hol_theorem th);

hol_theorem ispecl_rule(hol_term_list tms, hol_theorem th);

      A |- !x1...xn.t
-----------------------------  ISPECL [`t1`,...,`tn`]
 A' |- t[t1,...tn/x1,...,xn]

      A |- !x1...xn.t
-----------------------------  ISPECL [`t1`,...,`tn`]
 A' |- t[t1,...tn/x1,...,xn]

Specializes a theorem zero or more times, with type instantiation if necessary.

• raises — Fails if the list of terms is longer than the number of quantified variables in the term, or if the type instantiation fails.

hol_theorem spec_rule(hol_term tm, hol_theorem th);

hol_theorem spec_rule(hol_term tm, hol_theorem th);

  A |- !x. t
--------------  SPEC `u`
 A |- t[u/x]

  A |- !x. t
--------------  SPEC `u`
 A |- t[u/x]

Specializes the conclusion of a theorem.

• raises — Fails if the theorem's conclusion is not universally quantified, or if x and u have different types.

hol_theorem specl_rule(hol_term_list tms, hol_theorem th);

hol_theorem specl_rule(hol_term_list tms, hol_theorem th);

    A |- !x1...xn. t
-------------------------  SPECL [`u1`;...;`un`]
 A |- t[u1/x1]...[un/xn]

    A |- !x1...xn. t
-------------------------  SPECL [`u1`;...;`un`]
 A |- t[u1/x1]...[un/xn]

Specializes zero or more variables in the conclusion of a theorem.

• raises — Fails unless each of the terms is of the same as that of the appropriate quantified variable in the original theorem.

hol_theorem spec_all_rule(hol_theorem th);

hol_theorem spec_all_rule(hol_theorem th);

    A |- !x1...xn. t
---------------------------  SPEC_ALL
 A |- t[x1'/x1]...[xn'/xn]

    A |- !x1...xn. t
---------------------------  SPEC_ALL
 A |- t[x1'/x1]...[xn'/xn]

Specializes the conclusion of a theorem with its own quantified variables.

• raises — Never fails.

hol_theorem simple_choose_rule(hol_term v, hol_theorem th);

hol_theorem simple_choose_rule(hol_term v, hol_theorem th);

Existentially quantifies a hypothesis of a theorem.

• raises — Fails if v is not a variable or if it is free in the conclusion of the theorem th.

hol_theorem choose_rule(hol_term tm, hol_theorem th1, hol_theorem th2);

hol_theorem choose_rule(hol_term tm, hol_theorem th1, hol_theorem th2);

 A1 |- ?x. s[x]    A2 |- t
-------------------------------  CHOOSE (`v`,(A1 |- ?x. s))
  A1 u (A2 - {s[v/x]}) |- t

 A1 |- ?x. s[x]    A2 |- t
-------------------------------  CHOOSE (`v`,(A1 |- ?x. s))
  A1 u (A2 - {s[v/x]}) |- t

Eliminates existential quantification using deduction from a particular witness.

• raises — Fails unless the terms and theorems correspond as indicated above.

hol_theorem exists_rule(hol_term tm1, hol_term tm2, hol_theorem th);

hol_theorem exists_rule(hol_term tm1, hol_term tm2, hol_theorem th);

 A |- p[u/x]
-------------  EXISTS (`?x. p`,`u`)
 A |- ?x. p

 A |- p[u/x]
-------------  EXISTS (`?x. p`,`u`)
 A |- ?x. p

Introduces existential quantification given a particular witness.

• raises — Fails unless the substituted pattern is the same as the conclusion of the theorem.

hol_theorem simple_exists_rule(hol_term v, hol_theorem th);

hol_theorem simple_exists_rule(hol_term v, hol_theorem th);

Introduces an existential quantifier over a variable in a theorem.

• raises — Fails if v is not a variable.

原始规则 inst_ruleinst_rule 与 inst_type_ruleinst_type_rule 根据显式给出的配对列表执行替换。 term_matchterm_match 将一个项与另一个项匹配时，会生成高阶实例化对象（详见 HOL API：类型与项页）， instantiate_ruleinstantiate_rule 则将该对象应用到定理的结论上。

hol_theorem instantiate_rule(hol_instantiation inst, hol_theorem th);

hol_theorem instantiate_rule(hol_instantiation inst, hol_theorem th);

Applies a higher-order instantiation to conclusion of a theorem.

• raises — Fails if the instantiation is impossible because of free term or type variables in the hypotheses.

这四条规则直接证明目标，而非变换定理：三条分别处理自然数、整数与实数上的线性算术，另一条将实数命题转换为整数命题。其余判定过程（环、域、机器字、集合、一阶证明器）与共用同一套机制的求解器一起，列在 HOL API：变换与求解器页。

hol_theorem arith_rule(hol_term tm);

hol_theorem arith_rule(hol_term tm);

Automatically proves natural number arithmetic theorems needing basic rearrangement and linear inequality reasoning only.

• raises — Fails if the term is not of type bool or if it cannot be proved using the basic methods employed, e.g. requiring nonlinear inequality reasoning. Examples: ARITH_RULE x = 1 ==> y <= 1 \/ x < yx = 1 ==> y <= 1 \/ x < y yield |- x = 1 ==> y <= 1 \/ x < y ARITH_RULE 2 * a * b EXP 2 <= b * a * b ==> (SUC c - SUC(a * b * b) <= c)2 * a * b EXP 2 <= b * a * b ==> (SUC c - SUC(a * b * b) <= c) yield |- 2 * a * b EXP 2 <= b * a * b ==> SUC c - SUC (a * b * b) <= c

hol_theorem int_arith_rule(hol_term tm);

hol_theorem int_arith_rule(hol_term tm);

Proves integer theorems needing basic rearrangement and linear inequality reasoning only.

• raises — Fails if the term is not boolean or if it cannot be proved using the basic methods employed, e.g. requiring nonlinear inequality reasoning. Examples: INT_ARITH !x y:int. x <= y + &1 ==> x + &2 < y + &4!x y:int. x <= y + &1 ==> x + &2 < y + &4 yield |- !x y. x <= y + &1 ==> x + &2 < y + &4 INT_ARITH (x + y:int) pow 2 = x pow 2 + &2 * x * y + y pow 2(x + y:int) pow 2 = x pow 2 + &2 * x * y + y pow 2 yield |- (x + y) pow 2 = x pow 2 + &2 * x * y + y pow 2

hol_theorem int_of_real_thm_rule(hol_theorem th);

hol_theorem int_of_real_thm_rule(hol_theorem th);

Map a universally quantified theorem from reals to integers.

• raises — Never fails.

hol_theorem real_arith_rule(hol_term tm);

hol_theorem real_arith_rule(hol_term tm);

Attempt to prove term using basic algebra and linear arithmetic over the reals.

• raises — Fails if the term cannot be proved by REAL_ARITH. Examples: REAL_ARITH (&1 + x) * (&1 - x) * (&1 + x pow 2) < &1 ==> &0 < x pow 4(&1 + x) * (&1 - x) * (&1 + x pow 2) < &1 ==> &0 < x pow 4 yield |- (&1 + x) * (&1 - x) * (&1 + x pow 2) < &1 ==> &0 < x pow 4

头文件在这些规则之间还穿插了少量其他类型的声明。相应说明见各自所属的页面；这里一并列出，以便完整覆盖头文件的这一部分。

重写规则，以及获取和应用具名变换的两个函数，详见 HOL API：变换与求解器页：

定理查找、解析、打印、相等性检测与项匹配，详见 HOL API：类型与项页与 HOL API：理论与定理页：

系统中的每一条定理都由十条原始规则生成。本页其余规则构成了便于使用的派生层，包括合同与等式操作、命题规则与量词规则、实例化，以及算术判定过程。调用一条规则即可应用它；调用失败时通过状态报告，成功时返回一个 hol_theoremhol_theorem，后续无论怎样编程都无法破坏这条定理。