HOL API: Inference Rules

hol_prover_client.hhol_prover_client.h is the client side of the proof assistant: each function it declares is a thin C wrapper over a call into the HOL Light process that C*‘s symbolic execution engine drives. The objects it traffics in — hol_termhol_term, hol_theoremhol_theorem, hol_typehol_type, hol_conversionhol_conversion — are opaque one-field structs carrying a handle into that process. Everything they hand back, including cstrcstr strings, is managed by the garbage collector the toolchain links in; none of it is ever freed by hand.

Failure is not reported through the return value alone. A rule that cannot be applied returns an empty sentinel — empty_theoremempty_theorem, empty_termempty_term, empty_typeempty_type, empty_conversionempty_conversion, or an empty list — and records why. IS_NULLIS_NULL tests such a result, while get_last_status()get_last_status() and get_last_error()get_last_error() retrieve the status code and the message; the header recommends checking the status rather than the value, and in proof code that check is normally written with the TRYTRY and ENSUREENSURE macros of proof_util.hproof_util.h, described in Symbolic Execution and Runtime API.

The raises line on the entries below is the header’s own account of when a rule fails; where it says never fails, that too is the header’s word.

The ten fall into three groups: the equality rules refl_rulerefl_rule through beta_prim_rulebeta_prim_rule, which build equational theorems congruently over the term structure; the propositional rules assume_ruleassume_rule, eq_mp_ruleeq_mp_rule and deduct_antisym_rulededuct_antisym_rule, which introduce and discharge assumptions and are what make the logic’s implication work; and the two instantiation rules, which substitute for type variables and for free term variables.

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.

Everything below is derived. However elaborate the implementation — and arith_rulearith_rule runs a full linear-arithmetic decision procedure — the theorem that comes back was built by primitive steps, and the entries are grouped here by what they do to a goal rather than by how hard they work to do it.

The header states most of them as an inference-rule diagram, with the HOL Light tactic-level name of the rule to the right of the line: spec_rulespec_rule is HOL Light’s SPECSPEC, mp_rulemp_rule its MPMP. That correspondence is worth keeping in mind when reading HOL Light material, whose rules are the same rules under those names.

Rules that move an equation around: apply a function to both sides, reverse it, reduce it, or normalise modulo the associative and commutative laws of an operator.

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.

Conjunction, implication, disjunction and the two forms of equality with a truth value. mp_rulemp_rule is modus ponens on the nose; match_mp_rulematch_mp_rule is the version that instantiates the implication first, which is what proof scripts normally want when citing a general lemma.

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.

Introduction and elimination for !! and ??. The specspec family instantiates a universal, the ispecispec family does the same but instantiates the types as well; gen_rulegen_rule and its variants generalise, subject to the variable not occurring in the assumptions.

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.

The primitive inst_ruleinst_rule and inst_type_ruleinst_type_rule substitute along an explicit list of pairs. A higher-order instantiation — the object term_matchterm_match produces when matching one term against another, documented in HOL API: Types and Terms — is applied to a theorem’s conclusion by 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.

Four rules that prove goals outright rather than transform a theorem: linear arithmetic over the naturals, over the integers and over the reals, plus the transfer rule that reads an integer statement off a real one. The remaining decision procedures — rings, fields, machine words, sets, first-order provers — are on HOL API: Conversions and Solvers, where they sit next to the solvers they share machinery with.

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

The header interleaves a few declarations of other kinds among the rules. They are documented on the pages where they belong, and listed here so that this stretch of the header is accounted for.

The rewriting rules, and the two functions that fetch and apply a named conversion, are covered by HOL API: Conversions and Solvers:

Theorem lookup, parsing, printing, equality tests and term matching are covered by HOL API: Types and Terms and HOL API: Theories and Theorems:

Ten primitive rules generate every theorem in the system; the rest of this page is the derived layer that makes them usable — congruence and equality manipulation, the propositional and quantifier rules, instantiation, and the arithmetic procedures. A rule is applied by calling it, its failure is reported through the status, and its result is a hol_theoremhol_theorem that no amount of later programming can corrupt.