Derived Inference Rules

In this section, HOL proofs and theorems are made concrete. The notion of proof is defined abstractly in the manual §LOGIC: a proof of a sequent $(\Gamma,t)$ from a set of sequents $\Delta$ (with respect to a deductive system $\mathcal{D}$) was defined to be a chain of sequents culminating in $(\Gamma,t)$, such that every element of the chain either belongs to $\Delta$ or else follows from $\Delta$ and earlier elements of the chain by deduction. The notion of a theorem was also defined in §LOGIC: a theorem of a deductive system is a sequent that follows from the empty set of sequents by deduction; i.e., it is the last element of a proof in the deductive system from the empty set of sequents.

The deductive system of HOL was sketched in Section§Rules, where the eight families of primitive inferences making up the deductive system were specified by diagrams. It was explained that these families of inferences are represented in HOL via ML functions, and that theorems are represented by an ML abstract type called thm. The eight ML functions corresponding to the inferences are operations of the type thm, and each of the eight returns a value of type thm. It was explained that the type thm has primitive destructors, but no primitive constructor; and that, in that way, the logic is protected against the computation of theorems except by functions representing primitive inferences, or compositions of these.

Finally, the primitive HOL logic was supplemented by three primitive constants and four axioms, to form the basic logic. The primitive inferences, together with the primitive constants, the five axioms, and a collection of definitions, give a starting point for constructing proofs, and hence computing theorems. However, proving even the simplest theorems from this minimal basis costs considerable effort. The basis does not immediately provide the transitivity of equality, for example, or a means of universal quantification; both of these themselves have to be derived.

Simple Derivations

As an illustration of a proof in HOL, the following chain of theorems forms a proof (from the empty set, in the HOL deductive system), for the particular terms $\mathtt{t}_1$ and $\mathtt{t}_2$, both of HOL type :bool

1. $t_1 \Rightarrow t_2 \vdash t_1 \Rightarrow t_2$

2. $t_1\; |- t_1$

3. $t_1 \Rightarrow t_2, \; t_1 \vdash t_2$

That is, the third theorem follows from the first and second.

In the session below, the proof is performed in the HOL system, using the ML functions ASSUME and MP.

> show_assums := true;
val it = (): unit

> val th1 = ASSUME ``t1 ==> t2``
val th1 =  [t1 ⇒ t2] ⊢ t1 ⇒ t2: thm

> val th2 = ASSUME ``t1:bool``
val th2 =  [t1] ⊢ t1: thm

> MP th1 th2;
val it =  [t1, t1 ⇒ t2] ⊢ t2: thm

In the following, the Count.inferences function is used to count the number of primitive inferences performed in the course of applying the function to the argument. In the first invocation, this means that only the modus ponens step is counted. We create an artificial function to see the count of all three inference steps in the second interaction:

> Count.inferences (MP (ASSUME ``t1 ==> t2``)) (ASSUME ``t1:bool``);
Axioms: 0, Defs: 0, Disk: 0, Orcl: 0, Prims: 1; Total: 1
val it =  [t1, t1 ⇒ t2] ⊢ t2: thm

> fun f () = MP (ASSUME ``t1 ==> t2``) (ASSUME ``t1:bool``);
val f = fn: unit -> thm

> Count.inferences f ();
Axioms: 0, Defs: 0, Disk: 0, Orcl: 0, Prims: 3; Total: 3
val it =  [t1, t1 ⇒ t2] ⊢ t2: thm

Each of the three inference steps of the abstract proof corresponds to the application of an ML function in the performance of the proof in HOL; and each of the ML functions corresponds to a primitive inference of the deductive system.

It is worth emphasising that, in either case, every primitive inference in the proof chain is made, in the sense that for each inference, the corresponding ML function is evaluated. That is, HOL permits no short-cut around the necessity of performing complete proofs. The short-cut provided by derived inference rules (as implemented in ML) is around the necessity of specifying every step; something that would be impossible for a proof of any length. It can be seen from this that the derived rule, and its representation as an ML function, is essential to the HOL methodology; theorem proving would be otherwise impossible.

There are, of course, an infinite number of proofs of the form shown in the example that can be conducted in HOL: one for every pair of :bool-typed terms. Moreover, every time a theorem of the form

$$t_1 \Rightarrow \ t_2, \ t_1 \ \vdash \ t_2$$

is required, its proof must be constructed anew. To capture the general pattern of inference, an ML function can be written to implement an inference rule as a derivation from the primitive inferences. Abstractly, a derived inference rule is a rule that can be justified on the basis of the primitive inference rules (and/or the axioms). In the present case, the rule required undischarged assumptions. It is specified for HOL by

      Γ |- t1 ==> t2
     -----------------
      Γ ∪ {t1} |-  t2

This general rule is valid because, from a HOL theorem of the form $\Gamma \vdash t_1 \Rightarrow t_2$, the theorem $\Gamma \cup\{t_1\} \vdash t_2$ can be derived as in the specific instance above. The rule can be implemented in ML as a function (UNDISCH, say) that calls the appropriate sequence of primitive inferences. The ML definition of UNDISCH is simply

> fun UNDISCH th = MP th (ASSUME $ fst $ dest_imp $ concl th);
val UNDISCH = fn: thm -> thm

This code provides a function that maps a theorem to a theorem; that is, performs proofs in HOL. The following session illustrates the use of the derived rule on a consequence of the axiom IMP_ANTISYM_AX. (The inferences are counted. Assume that the printing of theorems has been adjusted as above and th is bound as shown below:

> val th = SPEC ``t2:bool`` $ SPEC ``t1:bool`` IMP_ANTISYM_AX;
val th =  [] ⊢ (t1 ⇒ t2) ⇒ (t2 ⇒ t1) ⇒ (t1 ⇔ t2): thm

> Count.inferences UNDISCH th;
Axioms: 0, Defs: 0, Disk: 0, Orcl: 0, Prims: 2; Total: 2
val it =  [t1 ⇒ t2] ⊢ (t2 ⇒ t1) ⇒ (t1 ⇔ t2): thm

> Count.inferences UNDISCH it;
Axioms: 0, Defs: 0, Disk: 0, Orcl: 0, Prims: 2; Total: 2
val it =  [t1 ⇒ t2, t2 ⇒ t1] ⊢ t1 ⇔ t2: thm

Each successful application of UNDISCH to a theorem invokes an application of ASSUME, followed by an application of MP; UNDISCH constructs the 2-step proof for any given theorem of the appropriate form. As can be seen, it relies on the class of ML functions that access HOL syntax: in particular, concl to produce the conclusion of the theorem, dest_imp to separate the implication, and the selector fst to choose the antecedent.

This particular example is very simple, but a derived inference rule can perform proofs of arbitrary length. It can also make use of previously defined rules. In this way, the normal inference patterns can be developed much more quickly and easily; transitivity, generalization, and so on, support the familiar patterns of inference.

A number of derived inference rules are pre-defined when the HOL system is entered (UNDISCH is one of the first). In Section, the abstract derivations are given for the pre-defined rules that reflect the more usual inference patterns of the predicate (and lambda) calculi. Like those shown, some of the pre-defined derived rules in HOL generate relatively short proofs. Others invoke thousands of primitive inferences, and clearly save a great deal of effort. Furthermore, rules can be defined by the user to make still larger steps, or to implement more specialized patterns.

All of the pre-defined derived rules in HOL are described in §REFERENCE.

Derivation of the Standard Rules

The HOL system provides all the standard introduction and elimination rules of the predicate calculus pre-defined as derived inferences. It is these derived rules, rather than the primitive rules, that one normally uses in practice. In this section, the derivations of some of the standard rules are given, in sequence. These derivations only use the axioms and definitions in the theory bool (see Section, the eight primitive inferences of the HOL logic, and inferences defined earlier in the sequence.

Theorems, in accordance with the definition given at the beginning of this chapter, are treated as rules without hypotheses; thus the derivation of a theorem resembles the derivation of a rule except in not having hypotheses. (The derivation of TRUTH, Section, is the only example given of this, but there are several others in HOL.) There are also some rules that are intrinsically more general than theorems. For example, for any two terms $t_1$ and $t_2$, the theorem $\vdash(\lambda{x}.t_1)t_2 = t_1[t_2/x]$ follows by the primitive rule BETA_CONV. The rule BETA_CONV returns a theorem for each pair of terms $t_1$ and $t_2$, and is therefore equivalent to an infinite family of theorems. No single theorem can be expressed in the HOL logic that is equivalent to BETA_CONV. See Chapter for further discussion of this point. Note that UNDISCH is not a rule of this sort, as it can, in fact, be expresed as a theorem.

For each derivation given below, there is an ML function definition in the HOL system that implements the derived rule as a procedure in ML. The actual implementation in the HOL system differs in some cases from the derivations given here, since the system code has been optimised for improved performance.

In addition, for reasons that are mostly historical, not all the inferences that are derived in terms of the abstract logic are actually derived in the current version of the HOL system. That is, there are currently a number of rules that are installed in the system on an “axiomatic” basis, all of which should be derived by explicit inference. These rules' status does not actually compromise the consistency of the logic. In effect, the existing HOL system has a deductive system more comprehensive than the one presented abstractly, but the model outlined in §LOGIC would easily extend to cover it. The derivations that follow consist of sequences of numbered steps each of which

1. is an axiom, or
2. is a hypothesis of the rule being derived, or
3. follows from preceding steps by a rule of inference (either primitive or previously derived).

Adding an assumption

   ADD_ASSUM : term -> thm -> thm

   Γ |- t
  ---------------
   Γ ∪ {t'} |- t

Undischarging

   UNDISCH : thm -> thm

   Γ |- t1 ==> t2
  ---------------
   Γ ∪ {t1} |- t2

Symmetry of equality

   SYM : thm -> thm

   Γ |- t1 = t2
  ---------------
   Γ |- t2 = t1

Transitivity of equality

   TRANS : thm -> thm -> thm

   Γ₁ |- t₁ = t₂ ,   Γ₂ |- t₂ = t3
  ---------------------------------
     Γ₁ ∪ Γ₂ |- t₁ = t3

Application of a term to a theorem

   AP_TERM : term -> thm -> thm

   Γ |- t₁ = t₂
  ------------------
   Γ |- t t₁ = t t₂

Application of a theorem to a term

   AP_THM : thm -> conv

   Γ |- t₁ = t₂
  ------------------
   Γ |- t₁ t = t₂ t

Modus Ponens for equality

   EQ_MP : thm -> thm -> thm

   Γ₁ |- t₁ = t₂ ,   Γ₂ |- t₁
  ---------------------------
     Γ₁ ∪ Γ₂ |- t₁ = t₂

Implication from equality

   EQ_IMP_RULE : thm -> thm * thm

          Γ |- t₁ = t₂
  ----------------------------------
   Γ |- t₁ ==> t₂ ,   Γ |- t₂ ==> t₁

$\mathsf{T}$-introduction

   TRUTH : thm

  ------------
     |- T

Equality-with-$\mathsf{T}$ elimination

   EQT_ELIM : thm -> thm

   Γ |- t = T
  -------------
   Γ |- t

Specialization ($\forall$-elimination)

   SPEC : term -> thm -> thm

   Γ |- ∀x. t
  -------------------
   Γ |- t[t'/x]

The notation $t[t'/x]$ denotes the result of replacing each free occurrence of $x$ in $t$ by $t'$. Renaming ensures that no free variables in a resulting occurrence of $t'$ will become bound.

Equality-with-$\mathsf{T}$\ introduction

   EQT_INTRO : thm -> thm

   Γ |- t
  -------------
   Γ |- t = T

Generalization ($\forall$-introduction)

   GEN : term -> thm -> thm

   Γ |- t
  ---------------
   Γ |- ∀x. t

Restriction: variable $x$ can not occur free in $\Gamma$.

Remark: The conventional notation for universal quantification, i.e. $\forall x.\; t$, is, in HOL, surface syntax for the underlying *term structure $\forall(\lambda{x}.\;t)$. This underlying structure is used to give clarity to some derivations in the following.

Simple $\alpha$-conversion

   SIMPLE_ALPHA

  ----------------------------------
   |- (λx₁. t) x₁ = (λx₂. t) x₂

Restriction: neither $x_1$ nor $x_2$ may occur free in $t$.

Remark: SIMPLE_ALPHA is not actually defined in the HOL system, as it is subsumed by other rules. It is included here just to support a later derivation in this section.

$\eta$-conversion

   ETA_CONV : conv

  -------------------
   |- (λx'. t x') = t

Restriction: $x'$ does not occur free in $t$.

Remark: we use $x'$ rather than just $x$ to motivate the use of SIMPLE_ALPHA in the derivation below.

Remark: In the HOL system, the type abbreviation conv = term -> thm describes SML functions that, when given a term $t_1$, return a theorem $\vdash t_1 = t_2$.

Extensionality

   EXT : thm -> thm

   Γ |- ∀x. t₁ x = t₂ x
  ----------------------
   Γ |- t₁ = t₂

Restriction: $x$ must not occur free in $t_1$ or $t_2$.

Choice introduction

   SELECT_INTRO : thm -> thm

   Γ |- t₁ t₂
  ----------------
   Γ |- t₁ (ε t₁)

Choice elimination

   SELECT_ELIM : thm -> term * thm -> thm


   Γ₁ |- t₁ (ε t₁) ,  Γ₂,t₁(v) |- t
  ----------------------------------
   Γ₁ ∪ Γ₂ |- t

Restriction: $v$ occurs nowhere except in the assumption $t_1\ v$ of the second hypothesis.

Existential introduction

   EXISTS : term * term -> thm -> thm

   Γ |- t₁[t₂]
  ---------------
   Γ |- ∃x. t₁[x]

Notation: $t_1[t_2]$ denotes a term $t_1$ with some free occurrences of $t_2$ singled out, and $t_1[x]$ denotes the result of replacing these occurrences of $t_1$ by $x$.

Existential elimination

   CHOOSE : term * thm -> thm -> thm

   Γ₁ |- ∃x. t[x] ,  Γ₂,t[v] |- t'
  ----------------------------------
   Γ₁ ∪ Γ₂ |- t'

Restrictions: $v$ must not be free in $Γ_1,Γ_2$ or $t$.

Applying a definition to one argument

Given an equation where the right-hand sde is a lambda-abstraction, one can derive an equation characterising the application of the function to a specified argument.

   RIGHT_BETA : thm -> thm

   Γ |- t = (λx. t₁ x) t₂
  ----------------------------------
   Γ |- t = t₁[t₂]

Applying a definition to multiple arguments

   RIGHT_LIST_BETA : thm -> thm

   Γ |- t = (λx₁…xₙ. t'[x₁,…,xₙ]) t₁ … tₙ
  -------------------------------------------------
   Γ |- t = t'[t₁,…,tₙ]

For readability, let $\mathcal{M} = \lambda{x_1\cdots x_n}.\; t'[x_1,\ldots,x_n]$ in the following:

Conjunction introduction

   CONJ : thm -> thm -> thm

   Γ₁ |- t₁  ,  Γ₂ |- t₂
  -----------------------
   Γ₁ ∪ Γ₂ |- t₁ ∧ t₂

Conjunction elimination

   CONJUNCT1 : thm -> thm
   CONJUNCT2 : thm -> thm

   Γ |- t₁ ∧ t₂
  -----------------------
   Γ |- t₁  ,  Γ |- t₂

Right disjunction introduction

   DISJ1 : thm -> conv

   Γ |- t₁
  --------------
   Γ |- t₁ ∨ t₂

Left disjunction introduction

   DISJ2 : term -> thm -> thm

   Γ |- t₂
  --------------
   Γ |- t₁ ∨ t₂

Disjunction elimination

   DISJ_CASES : thm -> thm -> thm -> thm

   Γ |- t₁ ∨ t₂  ,  Γ₁,t₁ |- t  ,  Γ₂,t₂ |- t
  --------------------------------------------
   Γ ∪ Γ₁ ∪ Γ₂ |- t

Classical contradiction rule

   CCONTR : term -> thm -> thm

   Γ, ¬t |- F
  ------------
   Γ |- t

Rewriting

Included in the set of derived inferences provided in HOL is a group of rules with complex definitions that do a limited amount of “automatic” theorem-proving in the form of rewriting. The ideas and implementation were originally developed by Milner and Wadsworth for Edinburgh LCF, and were later implemented more flexibly and efficiently by Paulson and Huet for Cambridge LCF. One basic rewriting rule, REWRITE_RULE, is illustrated here. Although HOL proofs typically feature more elaborate rewriters (such as SIMP_RULE, documented in Section), the underlying ideas are the same.

REWRITE_RULE uses a list of equational theorems (theorems whose conclusions can be regarded as having the form $t_1 = t_2$) to replace any subterms of an object theorem that “match” $t_1$ by the corresponding instance of $t_2$. The rule matches recursively and to any depth, until no more replacements can be made, using internally defined search, matching and instantiation algorithms. The validity of REWRITE_RULE rests ultimately on the primitive rules SUBST (for making the substitutions); INST_TYPE (for instantiating types); and the derived rules for generalization and specialization (see Section and Section for instantiating terms. The definition of REWRITE_RULE in ML also relies on a large number of general and HOL-oriented SML functions.

In practice, derived rules like REWRITE_RULE can play a central role in proofs, because they can perform a very large number of inferences which may happen in a complex and unpredictable order. This power is increased by the fact that any existing equational theorem can be supplied as a `rewrite rule', including a standard HOL set of pre-proved tautologies; and these rewrite rules can interact with each other in the rewriting process to transform the original theorem.

The application of REWRITE_RULE, in the session below, illustrates that replacements are made at all levels of the structure of a term. The example is a formula of natural number arithmetic: the infixes > and < are the usual “greater than” and “less than” relations, respectively, and SUC names the usual successor function on natural numbers. Use is made of the pre-existing definition of >, bound to arithmeticTheory.GREATER_DEF in SML (see §REFERENCE). The inference counting facility is used again, and the printing of theorems is adjusted as above.

> Count.inferences
    (REWRITE_RULE [arithmeticTheory.GREATER_DEF])
    (ASSUME ``SUC 3 > 0 /\ SUC 2 > 0 /\ SUC 1 > 0 /\ SUC 0 > 0``);
Axioms: 0, Defs: 0, Disk: 0, Orcl: 0, Prims: 11; Total: 11
val it =  [.] ⊢ 0 < SUC 3 ∧ 0 < SUC 2 ∧ 0 < SUC 1 ∧ 0 < SUC 0:
   thm

Notice that rewriting equations can be extracted from universally quantified theorems. To construct the proof step-wise, with all of the instantiations, substitutions, uses of transitivity, etc, would be a lengthy process. The rewriting rules make it easy, and do so whilst still generating the entire chain of inferences.