Filter
Top Products
Chapter 9
Derived rules
HOL has a variety of other derived rules that are not conversions, or at least aren’t
used much as in the previous chapter. Here we cover some of the most basic ones.
9.1 Logical rules
All the logical constants are defined; we have seen the definitions above. From the
definitions, rules for manipulating them directly are derived, so for most purposes
users can forget that they aren’t primitives. Most of the rules are so-called intro-
duction and elimination rules of natural deduction (Prawitz 1965).
1
For example,
the introduction rule for conjunctions, CONJ, takes two theorems and gives a new
theorem that results from conjoining (‘anding’) them, e.g.
#CONJ (REFL ‘1‘) (ASSUME ‘x = 2‘);;
it : thm = x = 2 |- (1 = 1) /\ (x = 2)
Conversely, the elimination rules CONJUNCT1 and CONJUNCT2 take a theorem
with a conjunction as conclusion, and give new theorems for the left and right
arms. CONJ PAIR gives a pair of both, while CONJUNCTS repeatedly breaks down a
conjunctive theorem into a list of theorems.
#let th1 = CONJ (REFL ‘T‘) (ASSUME ‘p /\ q‘);;
th1 : thm = p /\ q |- (T = T) /\ p /\ q
#let th2 = CONJ (REFL ‘1‘) th1;;
th2 : thm = p /\ q |- (1 = 1) /\ (T = T) /\ p /\ q
#CONJ_PAIR th2;;
it : thm * thm = p /\ q |- 1 = 1, p /\ q |- (T = T) /\ p /\ q
#CONJUNCTS th2;;
it : thm list = [p /\ q |- 1 = 1; p /\ q |- T = T; p /\ q |- p; p /\ q |- q]
#CONJUNCT2 th1;;
it : thm = p /\ q |- p /\ q
Abstracting away a bit from the implementation in CAML, we can represent
the rules in the usual form as:
Γ p ∆ q
Γ ∪ ∆ p ∧ q
CONJ
1
Although HOL uses a sequent presentation, the conventional derived rules are natural deduc-
tion rules, i.e. introduction and elimination on the right, rather than left and right introduction.
71