HOL API: Inference Rules

hol_prover_client.hhol_prover_client.h provides the proof assistant’s client interface. Each function it declares is a thin C wrapper around a call to the HOL Light process driven by C*‘s symbolic execution engine. The objects passed through this interface — hol_termhol_term, hol_theoremhol_theorem, hol_typehol_type, hol_conversionhol_conversion — are opaque one-field structs containing handles to objects in that process. All returned objects, including cstrcstr strings, are managed by the garbage collector linked into the toolchain and require no manual deallocation.

Failed calls that return basic objects or object pairs use the corresponding empty_*empty_* sentinels. Test basic objects with IS_NULLIS_NULL and object pairs with IS_NULL_PAIRIS_NULL_PAIR. String and list interfaces can return NULLNULL on error; a zero-length list is valid. The header recommends checking get_last_status()get_last_status() to determine whether a call failed and using get_last_error()get_last_error() to retrieve the error message. Proof code normally uses the TRYTRY and ENSUREENSURE macros of proof_util.hproof_util.h for status checks, as described in Symbolic Execution and Runtime API.

The raises line in each entry below gives the failure conditions documented in the header; never fails is also a claim from the header.

The ten rules form three groups: the equality rules refl_rulerefl_rule through beta_prim_rulebeta_prim_rule, which construct equational theorems by congruence over term structure; the propositional rules assume_ruleassume_rule, eq_mp_ruleeq_mp_rule and deduct_antisym_rulededuct_antisym_rule, which introduce and discharge assumptions to support reasoning about implication; and the two instantiation rules, which substitute for type variables and 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.

All rules below are derived: each constructs its result through primitive inference steps. This includes arith_rulearith_rule, which runs a full linear-arithmetic decision procedure. The entries are grouped by their effect on a goal rather than the complexity of their implementation.

The header presents most rules as inference-rule diagrams, with the HOL Light tactic-level name to the right of the line: spec_rulespec_rule corresponds to HOL Light’s SPECSPEC, and mp_rulemp_rule to MPMP. These names identify the same rules in HOL Light documentation.

These rules apply a function to both sides of an equation, reverse or reduce an equation, or normalise it modulo an operator’s associative and commutative laws.

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.

These rules handle conjunction, implication, disjunction and the two forms of equality with a truth value. mp_rulemp_rule applies modus ponens; match_mp_rulematch_mp_rule first instantiates the implication, as proof scripts normally need 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.

These rules introduce and eliminate !! and ??. The specspec family instantiates a universal quantifier, and the ispecispec family also instantiates types. gen_rulegen_rule and its variants generalise, provided the variable does not occur 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 rules inst_ruleinst_rule and inst_type_ruleinst_type_rule substitute using an explicit list of pairs. A higher-order instantiation is the object that term_matchterm_match produces when matching one term against another, as documented in HOL API: Types and Terms. instantiate_ruleinstantiate_rule applies this object to a theorem’s conclusion.

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.

This group contains three procedures that take a term and prove a theorem using linear arithmetic over the naturals, integers or reals, and one rule that transforms an existing theorem. The transfer rule int_of_real_thm_ruleint_of_real_thm_rule maps a universally quantified theorem from reals to integers. The remaining decision procedures — rings, fields, machine words, sets, first-order provers — are documented in HOL API: Conversions and Solvers, alongside the solvers that use the same mechanisms.

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 includes a few other declarations among the rules. They are documented on the corresponding reference pages and listed here to account for every declaration in this part of the header.

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:

Within a fixed theory, derived proofs reduce to the ten primitive inference rules. The derived rules on this page provide congruence and equality manipulation, propositional and quantifier reasoning, instantiation, and arithmetic procedures. Calling a rule applies it; the status reports failure, and a successful call returns a hol_theoremhol_theorem justified by the theory’s axioms and definitions and any assumptions recorded in the theorem.