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，后续无论怎样编程都无法破坏它。