The HOL more arithmetic Library

Paul Curzon

University of Cambridge, Computer Laboratory

New Museums Site, Pembroke Street Cambridge, CB2 3QG, England.

May 1993

Authors

This library is the combination of the arithmetic theories of the following people:

Mike Benjamin (British Aerospace Sowerby Research Centre, Bristol, U.K.), R. J. Boulton (University of Cambridge, Computer Laboratory, U.K.), Albert J. Camilleri (Hewlett-Packard Laboratories, Bristol, U.K.), Rachel Cardell-Oliver (University of Cambridge, Computer Laboratory, U.K.), Paul Curzon (University of Cambridge, Computer Laboratory, U.K.), Elsa L. Gunter (AT&T Bell Labs, USA) , Jeff Joyce (University of British Columbia, Canada), Philippe Leveilley (Ecole Polytechnique, Paris, France), Wim Ploegaerts (Imec vzw. Leuven, Belgium), Wai Wong (University of Cambridge, Computer Laboratory, U.K.).

Wim Ploegaerts compiled the theorems which came from other libraries in the HOL system and made many useful suggestions about the organization of the library. iv

Contents

1 The more arithmetic Library 3 1.1 The Theory more arithmetic . . . . . . . . . . . . . . . . . . . . . . . . . 3 1.2 The Theory ineq . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 1.3 The Theory zero ineq . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 1.4 The Theory suc . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 1.5 The Theory pre . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 1.6 The Theory add . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 1.7 The Theory sub . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 1.8 The Theory mult . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 1.9 The Theory div mod . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 1.10 The Theory min max . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 1.11 The Theory odd even . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 1.12 Using the Library . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7

1.12.1 An Example of a Session . . . . . . . . . . . . . . . . . . . . . . . . 8 1.12.2 The load more arithmetic Function . . . . . . . . . . . . . . . . . 9

2 ML Functions in the more arithmetic Library 11

3 Pre-proved Theorems 15 3.1 Theorems about Inequalities . . . . . . . . . . . . . . . . . . . . . . . . . . 15 3.2 Theorems about 0 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15 3.3 Theorems about SUC . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16 3.4 Theorems about PRE . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17 3.5 Theorems about Addition . . . . . . . . . . . . . . . . . . . . . . . . . . . 17 3.6 Theorems about Subtraction . . . . . . . . . . . . . . . . . . . . . . . . . . 19 3.7 Theorems about Multiplication and Exponential Functions . . . . . . . . . 22 3.8 Theorems about Division . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22 3.9 Theorems about Maximum and Minimum . . . . . . . . . . . . . . . . . . 23 3.10 Theorems about Odd and Even Numbers . . . . . . . . . . . . . . . . . . . 24

Index 25 2 Contents

Chapter 1

The more arithmetic Library

This document describes the facilities provided by the more_arithmetic library. The library contains an ad hoc collection of definitions and theorems about arithmetic which extends the standard theory arithmetic. Included are many general purpose theorems about the arithmetic operators defined in the theory arithmetic. In addition, definitions of new operators are given with associated theorems. Several conversions related to arithmetic are also provided. The library is split into several theories, the ancestry of which is shown below.

  more arithmeticpre zero ineq odd even min max                                                  mult    div mod ineq               suc sub add arithmetic

A complete list of the arithmetic theorems which are available in the library is given in Chapter 3. Due to the large number of theorems, users of the library may find the theorem retrieval library of help. The above hierarchy should be kept in mind when searching for theorems. All definitions and theorems from the ancestor theories are automatically loaded, if possible, when their names are first mentioned during a HOL session.

1.1 The Theory more arithmetic

The theory more_arithmetic is the descendant theory of all the theories in the library. It contains no theorems or definitions itself.

4 Chapter 1. The more arithmetic Library

1.2 The Theory ineq

The theory ineq contains an ad hoc collection of theorems about the inequality operators. It contains no new definitions. Below is a selection of the theorems that have been preproved in this theory.

   EQ_LESS_EQ          |- !a b. (a = b) = a <= b /\ b <= a
   NOT_EQ_LESS_EQ      |- !a b. ~(a = b) = a < b \/ b < a
   LESS_EQ_LESS_EQ_EQ  |- !m n. m <= n /\ n <= m = (m = n)

1.3 The Theory zero ineq

The theory zero_ineq contains an ad hoc collection of theorems about zero and the inequality operators. It contains no new definitions. The theorems that have been preproved in this theory are given below.

   M_LESS_0_LESS     |- !m n. m < n ==> 0 < n
   LESS1EQ0          |- !m. m < 1 = (m = 0)
   NOT_EQ_0          |- !m. ~(m = 0) ==> m >= 1
   LESS_EQ_0_EQ      |- !m. m <= 0 ==> (m = 0)
   GREATER_NOT_ZERO  |- !x. 0 < x ==> ~(x = 0)
   NOT_0_AND_MORE    |- !x. ~((x = 0) /\ 0 < x)

1.4 The Theory suc

The theory suc contains an ad hoc collection of theorems about SUC. It contains no new definitions. The theorems that have been pre-proved in this theory include but are not restricted to the following:

   NOT_SUC_LESS_EQ_0     |- !n. ~(SUC n) <= 0
   SUC_GREATER_EQ_SUC    |- !n m. (SUC m) >= (SUC n) = m >= n
   NOT_SUC_LESS_EQ_SELF  |- !n. ~(SUC n) <= n
   SUC_NOT_0             |- !n. ~(SUC n = 0)

1.5. The Theory pre 5

1.5 The Theory pre

The theory pre contains an ad hoc collection of theorems about PRE. It contains no new definitions. The theorems that have been pre-proved in this theory include but are not restricted to the following:

   SUC_PRE      |- !n. 0 < n ==> (SUC(PRE n) = n)
   PRE_MONO     |- !m n. (PRE m) < (PRE n) ==> m < n
   PRE_LESS_EQ  |- !n. (PRE n) <= n
   PRE_ADD      |- !n m. 0 < n ==> (PRE(n + m) = (PRE n) + m)
   PRE_K_K      |- !k. 0 < k ==> (PRE k) < k

1.6 The Theory add

The theory add contains an ad hoc collection of theorems about addition. It contains no new definitions. The theorems that have been pre-proved in this theory include but are not restricted to the following:

   LESS_EQ_ADD1    |- !p n. p <= (n + p)
   ADD_SYM_ASSOC   |- !a b c. a + (b + c) = b + (a + c)
   LESS_EQ_SPLIT   |- !m n p. (m + n) <= p ==> n <= p /\ m <= p
   ADDL_GREATER    |- !m n p. m < n ==> m < (p + n)
   LESS_ADD1       |- !a. a < (a + 1)

1.7 The Theory sub

The theory sub contains an ad hoc collection of theorems about subtraction. It contains no new definitions. The theorems that have been pre-proved in this theory include but are not restricted to the following:

   SUB_LE_ADD      |- !n m p. n <= p ==> (m <= (p - n) = (n + m) <= p)
   NOT_0_SUB       |- !m n. ~(m - n = 0) ==> ~(m = 0)
   ADD_SUB_SYM     |- !a c. (c + a) - c = a
   SUB_ADD_SELF    |- !m n. ~m < n ==> ((m - n) + n = m)
   SUB_BOTH_SIDES  |- !m n p. (m = n) ==> (m - p = n - p)

1.8 The Theory mult

The theory mult contains an ad hoc collection of theorems about multiplication and exponentials. It contains no new definitions. The theorems that have been pre-proved in this theory include but are not restricted to the following:

   LESS_MONO_MULT1       |- !m n p. m <= n ==> (p * m) <= (p * n)
   LESS_MULT_PLUS_DIFF   |- !n k l. k < l ==> ((k * n) + n) <= (l * n)
   LEFT_SUB_DISTRIB      |- !m n p. m * (n - p) = (m * n) - (m * p)
   ONE_LESS_TWO_EXP_SUC  |- !n. 1 < (2 EXP (SUC n))

1.9 The Theory div mod

The theory div_mod contains an ad hoc collection of theorems about the division operators DIV and MOD. It contains no new definitions. The theorems that have been pre-proved in this theory include but are not restricted to the following:

   SUC_MOD_SELF    |- !n. (SUC n) MOD (SUC n) = 0
   SUC_DIV_SELF    |- !n. (SUC n) DIV (SUC n) = 1
   ADD_DIV_ADD_DIV
     |- !n. 0 < n ==> (!x r. ((x * n) + r) DIV n = x + (r DIV n))
   MOD_MULT_MOD
     |- !m n. 0 < n /\ 0 < m ==> (!x. (x MOD (n * m)) MOD n = x MOD n)

1.10 The Theory min max

The theory min_max contains definitions of predicates which test for the maximum and minimum of two numbers. Associated theorems are also pre-proved. MAX returns the largest of its two arguments. MIN returns the smallest of its two arguments. They are defined in HOL as follows.

   MAX_DEF  |- !n p. MAX n p = (n <= p => p | n)
   MIN_DEF  |- !n p. MIN n p = (n <= p => n | p)

The theorems that have been pre-proved in this theory include but are not restricted to the following:

   MAX_0     |- !n. MAX 0 n = n
   MAX_SYM   |- !n p. MAX n p = MAX p n
   MAX_REFL  |- !n. MAX n n = n
   MIN_0     |- !n. MIN 0 n = 0
   MIN_SYM   |- !n p. MIN n p = MIN p n
   MIN_REFL  |- !n. MIN n n = n

MAX and MIN are also defined in the bags library (that is where these definitions were taken from) so incompatibility problems may arise if the two libraries are used at once.

1.11 The Theory odd even

The theory odd_even contains theorems about the predicates ODD and EVEN which test for odd and even numbers, respectively. The theorems that have been pre-proved in this theory include but are not restricted to the following:

   EVEN_ODD_0        |- EVEN 0 /\ ~ODD 0
   EVEN_ODD_SUC      |- !n.  (EVEN(SUC n) = ODD n) /\
                             (ODD(SUC n) = EVEN n)
   EVEN_IMPL_MULT    |- !n m. EVEN n \/ EVEN m ==> EVEN(n * m)

1.12 Using the Library

The more_arithmetic library is loaded into a user’s HOL session using the function load_library (see the HOL manual for a general description of library loading). First, the internal HOL search paths are updated. A pathname to the more_arithmetic library is added to the search path, so that theorems may be autoloaded from the constituent theories of the library; and the HOL help search path is updated with a pathname to online help files for the ML functions in the library.

After updating search paths, the load sequence for more_arithmetic depends on the current state of the HOL session. If the system is in draft mode, the library theory more_arithmetic is added as a new parent to the current theory. If the system is not in draft mode, but the current theory is an ancestor of the more_arithmetic theory in the library (e.g. the user is in a fresh HOL session) then the more_arithmetic theory is made into the current theory. In both cases, the ML functions in the library are loaded into HOL and the theorems in the library theories are set up to be autoloaded on demand. The more_arithmetic library is at this point fully loaded into the user’s HOL session.

1.12.1 An Example of a Session

The following session shows how the more_arithmetic library may be loaded using the function load_library. Suppose, beginning in a fresh HOL session, the user wishes to create a theory foo whose parents include the theories in the more_arithmetic library. This may be done as follows:

1

 #new_theory `foo`;;
 () : void
 #load_library `more arithmetic`;;

⋮

 Library `more arithmetic` loaded.
 () : void

Loading the library while drafting the theory foo makes the theory more_arithmetic into a parent of foo. The same effect could have been achieved (in a fresh session) by first loading the library and then creating foo:

1

 #load_library `more arithmetic`;;

⋮

 Library `more arithmetic` loaded.
 () : void
 #new_theory `foo`;;
 () : void

Here, the theory more_arithmetic is first made the current theory of the new session. It then automatically becomes a parent of foo when this theory is created by new_theory.

Now, suppose that foo has been created as shown above, and the user does some work in this theory, quits HOL and in a later session wishes to load the theory foo. This must be done by first loading the more_arithmetic library and then loading the theory foo.

1

 #load_library `more arithmetic`;;

⋮

 Library `more arithmetic` loaded.
 () : void
 #load_theory `foo`;;
 Theory foo loaded
 () : void

This sequence of actions ensures that the system finds the parent theory more_arithmetic when it comes to load foo, since loading the library updates the search path.

1.12.2 The load more arithmetic Function

The more_arithmetic library may in many cases simply be loaded into the system as illustrated by the examples given above. There are, however, certain situations in which the more_arithmetic library cannot be fully loaded at the time when the load_library is used. This occurs when the system is not in draft mode and the current theory is not an ancestor of the theory more_arithmetic. In this case, loading the library can and will update the search paths, as usual. But the more_arithmetic theory in the library can neither be made into a parent of the current theory nor can it be made the current theory. This means that autoloading from the library cannot at this stage be activated. Nor can the ML code in the library be loaded into HOL, since it requires access to some of the theorems in the library.

In the situation described above—when the system is not in draft mode and the current theory is not an ancestor of the theory more_arithmetic—the library load sequence defines an ML function called load_more_arithmetic in the current HOL session. If at a future point in the session the more_arithmetic theory (now accessible via the search path) becomes an ancestor of the current theory, this function can then be used to complete loading of the library. Evaluating

    load_more_arithmetic();;

in such a context loads the ML functions of the more_arithmetic library into HOL and activates autoloading from its theory files. The function load_more_arithmetic fails if the theory more_arithmetic is not a parent of the current theory.

Note that the function load_more_arithmetic becomes available when loading the more_arithmetic library only if the more_arithmetic theory at that point can neither be made into a new parent (i.e. the system is not in draft mode) nor be made the current theory.

10 Chapter 1. The more arithmetic Library

ML Functions in the more arithmetic Library

This chapter provides documentation on all the ML functions that are made available in HOL when the more_arithmetic library is loaded. This documentation is also available online via the help facility.

 GEN_INDUCT_RULE

GEN_INDUCT_RULE : (thm -> thm -> thm)

Synopsis

Performs a proof by general mathematical induction on the natural numbers.

Description

The derived inference rule GEN_INDUCT_RULE implements the rule of general mathematical induction:

    A1 |- P[0/n]      A2 |- !n. (!m. m < n ==> P[m/n]) ==> P
   ----------------------------------------------------------  GEN_INDUCT_RULE
                        A1 u A2 |- !n. P

When supplied with a theorem A1 |- P[0/n], which asserts the base case of a proof of the proposition P by general induction on n, and the theorem

   A2 |- !n. (!m. m < n ==> P[m/n]) ==> P

which asserts the step case in the induction on n, the inference rule GEN_INDUCT_RULE

returns A1 u A2 |- !n. P.

Failure

A call to GEN_INDUCT_RULE th1 th2 fails if the theorems th1 and th2 do not have the

forms A1 |- P[0/n] and A2 |- !n. (!m. m < n ==> P[m/n]) ==> P respectively.

See also

GEN_INDUCT_TAC, INDUCT.

 GEN_INDUCT_TAC

GEN_INDUCT_TAC : tactic

Synopsis

Performs tactical proof by general mathematical induction on the natural numbers.

Description

GEN_INDUCT_TAC reduces a goal !n.P, where n has type num, to two subgoals corresponding to the base and step cases in a proof by general mathematical induction on n. The induction hypothesis appears among the assumptions of the subgoal for the step case. The specification of GEN_INDUCT_TAC is:

                          A ?- !n. P
   ========================================================  GEN_INDUCT_TAC
    A ?- P[0/n]     A u {!m. m < n' ==> P[m/n]} ?- P[n'/n]

where n' is a primed variant of n that does not appear free in the assumptions A (usually, n' just equals n). When GEN_INDUCT_TAC is applied to a goal of the form !n.P, where n does not appear free in P, the subgoals are just A ?- P and A u {!m. m < n' ==> P} ?- P.

Failure

GEN_INDUCT_TAC g fails unless the conclusion of the goal g has the form !n.t, where the variable n has type num.

See also

GEN_INDUCT_RULE, INDUCT_TAC.

 NUM_EQ_PLUS_CONV

NUM_EQ_PLUS_CONV : (term -> conv)

Synopsis

Adds a given expression of type :num to both sides of an equality between natural numbers.

Description

When applied to terms of the form "n" and "p = q", where n, p and q have type :num, the conversion NUM_EQ_PLUS_CONV returns the theorem:

   |-  (p = q) = (p + n = q + n)

Failure

Fails if the first term does not have type :num or the second does not have the form "p = q", where p and q are terms of type :num.

See also

NUM_LESS_EQ_PLUS_CONV, NUM_LESS_PLUS_CONV.

 NUM_LESS_EQ_PLUS_CONV

NUM_LESS_EQ_PLUS_CONV : (term -> conv)

Synopsis

Adds a given expression of type :num to both sides of a less-than-or-equal expression.

Description

When applied to terms of the form "n" and "p <= q", where n, p and q have type :num, the conversion NUM_LESS_EQ_PLUS_CONV returns the theorem:

   |-  p <= q = (p + n) <= (q + n)

Failure

Fails if the first term does not have type :num or the second does not have the form

"p <= q".

See also

NUM_EQ_PLUS_CONV, NUM_LESS_PLUS_CONV.

 NUM_LESS_PLUS_CONV

NUM_LESS_PLUS_CONV : (term -> conv)

Synopsis

Adds a given expression of type :num to both sides of a less expression.

Description

When applied to terms of the form "n" and "p < q", where n, p and q have type :num, the conversion NUM_LESS_PLUS_CONV returns the theorem:

   |-  p < q = (p + n) < (q + n)

Failure

Fails if the first term does not have type :num or the second does not have the form

"p < q".

See also

NUM_EQ_PLUS_CONV, NUM_LESS_EQ_PLUS_CONV.

Pre-proved Theorems

This chapter gives all the definitions and theorems in the more_arithmetic library. The theorems are grouped into sections according to subject matter. Some theorems could be classified under more than one subject, but each theorem is listed in only one section. The reader may therefore have to consult more than one section when searching for any particular theorem.

When the library is loaded, all the theorems in the library are set up to autoload when their names are mentioned in ML. The name of the theory in which each theorem is stored is given in parentheses after the name of the theorem.

3.1 Theorems about Inequalities

GEN_INDUCTION (ineq)
  |- !P. P 0 /\ (!n. (!m. m < n ==> P m) ==> P n) ==> (!n. P n)
GREATER_EQ_ANTISYM (ineq)
  |- !n m. ~(n >= m /\ n < m)
LESS_EQ_LESS_EQ_EQ (ineq)
  |- !m n. m <= n /\ n <= m = (m = n)
LESS_IS_NOT_LESS_OR_EQ (ineq)
  |- !x y. x < y = ~y <= x
NOT_EQ_LESS_EQ (ineq)
  |- !a b. ~(a = b) = a < b \/ b < a
NOT_LESS_AND_GREATER (ineq)
  |- !n m. n < m ==> ~m < n

3.2 Theorems about 0

GREATER_NOT_ZERO (zero ineq)
  |- !x. 0 < x ==> ~(x = 0)

16 Chapter 3. Pre-proved Theorems

LESS1EQ0 (zero ineq)
  |- !m. m < 1 = (m = 0)
LESS_EQ_0_EQ (zero ineq)
  |- !m. m <= 0 ==> (m = 0)
M_LESS_0_LESS (zero ineq)
  |- !m n. m < n ==> 0 < n
NOT_0_AND_MORE (zero ineq)
  |- !x. ~((x = 0) /\ 0 < x)
NOT_EQ_0 (zero ineq)
  |- !m. ~(m = 0) ==> m >= 1

3.3 Theorems about SUC

LESS_EQ_LESS_SUC (suc)
  |- !m n. m <= n = m < (SUC n)
NOT_0_GREATER_EQ_SUC (suc)
  |- !n. ~0 >= (SUC n)
NOT_FORALL_SUC_LESS_EQ (suc)
  |- ~(!n m. (SUC m) <= n)
NOT_SUC_LESS_EQ_SELF (suc)
  |- !n. ~(SUC n) <= n
SUC_0 (suc)
  |- 1 = SUC 0
SUC_GREATER_EQ_SUC (suc)
  |- !n m. (SUC m) >= (SUC n) = m >= n
SUC_LESS_EQ (suc)
  |- !m n. m <= n /\ ~(m = n) ==> (SUC m) <= n
SUC_NOT_0 (suc)
  |- !n. ~(SUC n = 0)

3.4. Theorems about PRE 17

3.4 Theorems about PRE

LESS_IMP_LESS_EQ_PRE (pre)
  |- !m n. 0 < n ==> (m < n = m <= (PRE n))
PRE_ADD (pre)
  |- !n m. 0 < n ==> (PRE(n + m) = (PRE n) + m)
PRE_K_K (pre)
  |- !k. 0 < k ==> (PRE k) < k
PRE_LESS (pre)
  |- !b. 0 < b /\ b < a ==> (PRE b) < a
PRE_LESS_EQ (pre)
  |- !n. (PRE n) <= n
PRE_MONO (pre)
  |- !m n. (PRE m) < (PRE n) ==> m < n
PRE_MONO_LESS_EQ (pre)
  |- !m n. m < n ==> (PRE m) <= (PRE n)
SUC_LESS_EQ_PRE (pre)
  |- !m n. 0 < n ==> (SUC m) <= n ==> m <= (PRE n)
SUC_LESS_PRE (pre)
  |- !m n. (SUC m) < n ==> m < (PRE n)
SUC_PRE (pre)
  |- !n. 0 < n ==> (SUC(PRE n) = n)

3.5 Theorems about Addition

ADDL_GREATER (add)
  |- !m n p. m < n ==> m < (p + n)
ADDL_GREATER_EQ (add)
  |- !m n p. m <= n ==> m <= (p + n)
ADDR_GREATER (add)
  |- !m n p. m < n ==> m < (n + p)

ADDR_GREATER_EQ (add)
  |- !m n p. m <= n ==> m <= (n + p)
ADD_EQ_LESS_EQ (add)
  |- !m n p. (m + n = p) ==> m <= p
ADD_EQ_LESS_IMP_LESS (add)
  |- !n m k l. (k + m = l + n) /\ k < l ==> n < m
ADD_GREATER_EQ (add)
  |- !m n. (m + n) >= m
ADD_MONO_LESS (add)
  |- !m n p. (m + p) < (m + n) = p < n
ADD_SUC_0 (add)
  |- !m. SUC m = (SUC 0) + m
ADD_SYM_ASSOC (add)
  |- !a b c. a + (b + c) = b + (a + c)
GREATER_EQ_SPLIT (add)
  |- !m n p. p >= (m + n) ==> p >= n /\ p >= m
LESS_ADD1 (add)
  |- !a. a < (a + 1)
LESS_ADD_ASSOC (add)
  |- !a b c d. a < (b + c) ==> a < (b + (c + d))
LESS_EQ_ADD1 (add)
  |- !p n. p <= (n + p)
LESS_EQ_MONO_ADD_EQ0 (add)
  |- !m n p. m <= n = (p + m) <= (p + n)
LESS_EQ_MONO_ADD_EQ1 (add)
  |- !m p. (m + p) <= p = m <= 0
LESS_EQ_SPLIT (add)
  |- !m n p. (m + n) <= p ==> n <= p /\ m <= p
LESS_LESS_EQ (add)
  |- !a b. a < b = (a + 1) <= b

3.6. Theorems about Subtraction 19

LESS_LESS_EQ_MONO (add)
  |- (!m n p q. m < p /\ n <= q ==> (m + n) < (p + q)) /\
     (!m n p q. m <= p /\ n < q ==> (m + n) < (p + q))
LESS_LESS_MONO (add)
  |- !m n p q. m < p /\ n < q ==> (m + n) < (p + q)
LESS_TRANS_ADD (add)
  |- !m n p q. m < (n + p) /\ p < q ==> m < (n + q)
NOT_1_TWICE (add)
  |- !n. ~(1 = n + n)
NOT_ADD_LESS (add)
  |- !m n. ~(m + n) < n
NOT_LESS_IMP_LESS_EQ_ADD1 (add)
  |- !a b. ~a < b ==> b <= (a + 1)
SUC_LESS_N_LESS (add)
  |- !m n. (m + 1) < n ==> m < n
SUM_LESS (add)
  |- !m n p. (m + n) < p ==> m < p /\ n < p

3.6 Theorems about Subtraction

ADD_EQ_IMP_SUB_EQ (sub)
  |- !a b c. (a = b + c) ==> (a - b = c)
ADD_LESS_EQ_SUB (sub)
  |- !n m p. n <= p ==> ((n + m) <= p = m <= (p - n))
ADD_SUB_SYM (sub)
  |- !a c. (c + a) - c = a
GREATER_EQ_SUB_LESS_TO_ADD (sub)
  |- !n m p. p >= n ==> ((p - n) < m = p < (n + m))
LESS_EQ_ADD_SUB1 (sub)
  |- !m n p. p <= n ==> (m + (n - p) = (m + n) - p)
LESS_EQ_SUB_1 (sub)
  |- !a b. a <= b ==> (a - 1) <= (b - 1)

LESS_EQ_SUB_ADD (sub)
  |- !m n p. p <= m ==> ((m - p) + n = (m + n) - p)
LESS_PRE (sub)
  |- !i m. i < (m - 1) ==> i < m
LESS_SUB_IMP_INV (sub)
  |- !k l. 0 < (k - l) ==> l < k
LESS_SUB_IMP_SUM_LESS (sub)
  |- !i m. i < (m - 1) /\ 1 < m ==> (i + 1) < m
LESS_SUB_TO_ADDL_LESS (sub)
  |- !m n p. n <= m ==> (p < (m - n) = (n + p) < m)
LESS_SUB_TO_ADDR_LESS (sub)
  |- !m n p. p <= m ==> (n < (m - p) = (n + p) < m)
LESS_TWICE_IMP_LESS_SUB (sub)
  |- !a b m. a < m /\ b < m /\ m <= (a + b) ==> ((a + b) - m) < m
NOT_0_SUB (sub)
  |- !m n. ~(m - n = 0) ==> ~(m = 0)
NOT_LESS_SUB (sub)
  |- !m n. ~m < (m - n)
NOT_SUB_0 (sub)
  |- !m n. m < n ==> ~(n - m = 0)
PRE_LESS_LESS_SUC (sub)
  |- !i m. i < (m - 1) /\ 0 < m ==> (i + 1) < m
PRE_SUB_SUC (sub)
  |- !m n. m < n ==> (PRE(n - m) = n - (SUC m))
SMALLER_SUM (sub)
  |- !m n p. m < p /\ n < p ==> ~((m + n) - p) > m
SUB_1_LESS (sub)
  |- !m n. ~(m = 0) /\ m < (SUC n) ==> (m - 1) < n
SUB_1_LESS_EQ (sub)
  |- !m n. m < n ==> (n - 1) >= m
SUB_ADD_SELF (sub)
  |- !m n. ~m < n ==> ((m - n) + n = m)

3.6. Theorems about Subtraction 21

SUB_BOTH_SIDES (sub)
  |- !m n p. (m = n) ==> (m - p = n - p)
SUB_EQ_SUB_ADD_SUB (sub)
  |- !a b c. a <= b /\ b <= c ==> (c - a = (c - b) + (b - a))
SUB_GREATER_0 (sub)
  |- !a b. a < b ==> (b - a) > 0
SUB_GREATER_EQ_ADD (sub)
  |- !n m p. p >= n ==> ((p - n) >= m = p >= (n + m))
SUB_LESS_BOTH_SIDES (sub)
  |- !m n p. p <= m /\ m < n ==> (m - p) < (n - p)
SUB_LESS_EQ_SUB1 (sub)
  |- !x. x > 0 ==> (!a. (a - x) <= (a - 1))
SUB_LESS_EQ_SUB_SUC (sub)
  |- !a b c n. 0 < c /\ a <= (b - n) ==> (a - c) <= (b - (SUC n))
SUB_LESS_TO_LESS_ADDL (sub)
  |- !m n p. n <= m ==> ((m - n) < p = m < (n + p))
SUB_LESS_TO_LESS_ADDR (sub)
  |- !m n p. p <= m ==> ((m - p) < n = m < (n + p))
SUB_LE_ADD (sub)
  |- !n m p. n <= p ==> (m <= (p - n) = (n + m) <= p)
SUB_PRE_SUB_1 (sub)
  |- !a b. 0 < b ==> ((a - (PRE b)) - 1 = a - b)
SUB_SUB_ID (sub)
  |- !k l. l < k ==> (k - (k - l) = l)
SUB_SUC (sub)
  |- !k m. m < k ==> (k - m = SUC(k - (SUC m)))
SUB_SUC_PRE_SUB (sub)
  |- !n m. 0 < n ==> (n - (SUC m) = (PRE n) - m)
SUC_SUB (sub)
  |- !m n.
      (m < n ==> ((SUC m) - n = 0)) /\
      (~m < n ==> ((SUC m) - n = SUC(m - n)))

3.7 Theorems about Multiplication and Exponential Functions

EXP1 (mult)
  |- !n. n EXP 1 = n
LESS_MONO_MULT1 (mult)
  |- !m n p. m <= n ==> (p * m) <= (p * n)
LESS_MULT_PLUS_DIFF (mult)
  |- !n k l. k < l ==> ((k * n) + n) <= (l * n)
NOT_MULT_LESS_0 (mult)
  |- !m n. 0 < m /\ 0 < n ==> 0 < (m * n)
ONE_LESS_EQ_TWO_EXP (mult)
  |- !n. 1 <= (2 EXP n)
ONE_LESS_TWO_EXP_SUC (mult)
  |- !n. 1 < (2 EXP (SUC n))
ZERO_LESS_TWO_EXP (mult)
  |- !n. 0 < (2 EXP n)

3.8 Theorems about Division

ADD_DIV_ADD_DIV (div mod)
  |- !n. 0 < n ==> (!x r. ((x * n) + r) DIV n = x + (r DIV n))
ADD_DIV_SUC_DIV (div mod)
  |- !n. 0 < n ==> (!r. (n + r) DIV n = SUC(r DIV n))
DIV_DIV_DIV_MULT (div mod)
  |- !m n. 0 < m /\ 0 < n ==> (!x. (x DIV m) DIV n = x DIV (m * n))
DIV_ONE (div mod)
  |- !q. q DIV (SUC 0) = q
LESS_DIV_EQ_ZERO (div mod)
  |- !r n. r < n ==> (r DIV n = 0)
LESS_EQ_MONO_DIV (div mod)
  |- !n. 0 < n ==> (!p q. p <= q ==> (p DIV n) <= (q DIV n))

3.9. Theorems about Maximum and Minimum 23

MOD_MULT_MOD (div mod)
  |- !m n. 0 < n /\ 0 < m ==> (!x. (x MOD (n * m)) MOD n = x MOD n)
MULT_DIV (div mod)
  |- !n q. 0 < n ==> ((q * n) DIV n = q)
SUC_DIV_CASES (div mod)
  |- !n.
      0 < n ==>
      (!x. ((SUC x) DIV n = x DIV n) \/ ((SUC x) DIV n = SUC(x DIV n)))
SUC_DIV_SELF (div mod)
  |- !n. (SUC n) DIV (SUC n) = 1
SUC_MOD (div mod)
  |- !n m. (SUC n) < m ==> ((SUC n) MOD m = SUC(n MOD m))
SUC_MOD_SELF (div mod)
  |- !n. (SUC n) MOD (SUC n) = 0

3.9 Theorems about Maximum and Minimum

MAX_0 (min max)
  |- !n. MAX 0 n = n
MAX_DEF (min max)
  |- !n p. MAX n p = (n <= p => p | n)
MAX_REFL (min max)
  |- !n. MAX n n = n
MAX_SUC (min max)
  |- !n. MAX n(SUC n) = SUC n
MAX_SYM (min max)
  |- !n p. MAX n p = MAX p n
MIN_0 (min max)
  |- !n. MIN 0 n = 0
MIN_DEF (min max)
  |- !n p. MIN n p = (n <= p => n | p)
MIN_REFL (min max)
  |- !n. MIN n n = n

MIN_SUC (min max)
  |- !n. MIN n(SUC n) = n
MIN_SYM (min max)
  |- !n p. MIN n p = MIN p n
SUC_MAX (min max)
  |- !n p. MAX(SUC n)(SUC p) = SUC(MAX n p)
SUC_MIN (min max)
  |- !n p. MIN(SUC n)(SUC p) = SUC(MIN n p)

3.10 Theorems about Odd and Even Numbers

EVEN_MULT (odd even)
  |- !n m. EVEN n \/ EVEN m ==> EVEN(n * m)
EVEN_ODD_0 (odd even)
  |- EVEN 0 /\ ~ODD 0
EVEN_ODD_PLUS_CASES (odd even)
  |- !n m.
      (ODD n /\ ODD m ==> EVEN(n + m)) /\
      (ODD n /\ EVEN m ==> ODD(n + m)) /\
      (EVEN n /\ EVEN m ==> EVEN(n + m))
EVEN_ODD_SUC (odd even)
  |- !n. (EVEN(SUC n) = ODD n) /\ (ODD(SUC n) = EVEN n)
MULT_EVEN (odd even)
  |- !n m. EVEN(n * m) ==> EVEN n \/ EVEN m
MULT_ODD (odd even)
  |- !n m. ODD(n * m) ==> ODD n /\ ODD m
NOT_EVEN_ODD_SUC_EVEN_ODD (odd even)
  |- !n. (~EVEN(SUC n) = EVEN n) /\ (~ODD(SUC n) = ODD n)
ODD_MULT (odd even)
  |- !n m. ODD n /\ ODD m ==> ODD(n * m)

Index

add, theory, 5

ADD_DIV_ADD_DIV, 6, 22
ADD_DIV_SUC_DIV, 22
ADD_EQ_IMP_SUB_EQ, 19
ADD_EQ_LESS_EQ, 18
ADD_EQ_LESS_IMP_LESS, 18
ADD_GREATER_EQ, 18
ADD_LESS_EQ_SUB, 19
ADD_MONO_LESS, 18
ADD_SUB_SYM, 5, 19
ADD_SUC_0, 18
ADD_SYM_ASSOC, 5, 18
ADDL_GREATER, 5, 17
ADDL_GREATER_EQ, 17
ADDR_GREATER, 17
ADDR_GREATER_EQ, 18
DIV, 6
DIV_DIV_DIV_MULT, 22
DIV_ONE, 22

div_mod, theory, 6

EQ_LESS_EQ, 4
EVEN, 7
EVEN_IMPL_MULT, 7
EVEN_MULT, 24
EVEN_ODD_0, 7, 24
EVEN_ODD_PLUS_CASES, 24
EVEN_ODD_SUC, 7, 24
EXP1, 22
GEN_INDUCT_RULE, 11
GEN_INDUCT_TAC, 12
GEN_INDUCTION, 15

                                       GREATER_EQ_ANTISYM, 15
                                       GREATER_EQ_SPLIT, 18
                                       GREATER_EQ_SUB_LESS_TO_ADD, 19
                                       GREATER_NOT_ZERO, 4, 15

ineq, theory, 4

                                       LEFT_SUB_DISTRIB, 6
                                       LESS1EQ0, 4, 16
                                       LESS_ADD1, 5, 18
                                       LESS_ADD_ASSOC, 18
                                       LESS_DIV_EQ_ZERO, 22
                                       LESS_EQ_0_EQ, 4, 16
                                       LESS_EQ_ADD1, 5, 18
                                       LESS_EQ_ADD_SUB1, 19
                                       LESS_EQ_LESS_EQ_EQ, 4, 15
                                       LESS_EQ_LESS_SUC, 16
                                       LESS_EQ_MONO_ADD_EQ0, 18
                                       LESS_EQ_MONO_ADD_EQ1, 18
                                       LESS_EQ_MONO_DIV, 22
                                       LESS_EQ_SPLIT, 5, 18
                                       LESS_EQ_SUB_1, 19
                                       LESS_EQ_SUB_ADD, 20
                                       LESS_IMP_LESS_EQ_PRE, 17
                                       LESS_IS_NOT_LESS_OR_EQ, 15
                                       LESS_LESS_EQ, 18
                                       LESS_LESS_EQ_MONO, 19
                                       LESS_LESS_MONO, 19
                                       LESS_MONO_MULT1, 6, 22
                                       LESS_MULT_PLUS_DIFF, 6, 22
                                       LESS_PRE, 20
                                       LESS_SUB_IMP_INV, 20
                                       LESS_SUB_IMP_SUM_LESS, 20

\underline{26 Index}

LESS_SUB_TO_ADDL_LESS, 20
LESS_SUB_TO_ADDR_LESS, 20
LESS_TRANS_ADD, 19
LESS_TWICE_IMP_LESS_SUB, 20
load_more_arithmetic, 9
M_LESS_0_LESS, 4, 16
MAX, 6
MAX_0, 7, 23
MAX_DEF, 6, 23
MAX_REFL, 7, 23
MAX_SUC, 23
MAX_SYM, 7, 23
MIN, 6
MIN_0, 7, 23
MIN_DEF, 6, 23

min_max, theory, 6

MIN_REFL, 7, 23
MIN_SUC, 24
MIN_SYM, 7, 24
MOD, 6
MOD_MULT_MOD, 6, 23
more_arithmetic, theory, 3

mult, theory, 6

MULT_DIV, 23
MULT_EVEN, 24
MULT_ODD, 24
NOT_0_AND_MORE, 4, 16
NOT_0_GREATER_EQ_SUC, 16
NOT_0_SUB, 5, 20
NOT_1_TWICE, 19
NOT_ADD_LESS, 19
NOT_EQ_0, 4, 16
NOT_EQ_LESS_EQ, 4, 15
NOT_EVEN_ODD_SUC_EVEN_ODD, 24
NOT_FORALL_SUC_LESS_EQ, 16
NOT_LESS_AND_GREATER, 15
NOT_LESS_IMP_LESS_EQ_ADD1, 19
NOT_LESS_SUB, 20
NOT_MULT_LESS_0, 22

                                       NOT_SUB_0, 20
                                       NOT_SUC_LESS_EQ_0, 4
                                       NOT_SUC_LESS_EQ_SELF, 4, 16
                                       NUM_EQ_PLUS_CONV, 12
                                       NUM_LESS_EQ_PLUS_CONV, 13
                                       NUM_LESS_PLUS_CONV, 13
                                       ODD, 7
                                       ODD_MULT, 24

odd_even, theory, 7

                                       ONE_LESS_EQ_TWO_EXP, 22
                                       ONE_LESS_TWO_EXP_SUC, 6, 22

pre, theory, 5

                                       PRE_ADD, 5, 17
                                       PRE_K_K, 5, 17
                                       PRE_LESS, 17
                                       PRE_LESS_EQ, 5, 17
                                       PRE_LESS_LESS_SUC, 20
                                       PRE_MONO, 5, 17
                                       PRE_MONO_LESS_EQ, 17
                                       PRE_SUB_SUC, 20
                                       SMALLER_SUM, 20

sub, theory, 5

                                       SUB_1_LESS, 20
                                       SUB_1_LESS_EQ, 20
                                       SUB_ADD_SELF, 5, 20
                                       SUB_BOTH_SIDES, 5, 21
                                       SUB_EQ_SUB_ADD_SUB, 21
                                       SUB_GREATER_0, 21
                                       SUB_GREATER_EQ_ADD, 21
                                       SUB_LE_ADD, 5, 21
                                       SUB_LESS_BOTH_SIDES, 21
                                       SUB_LESS_EQ_SUB1, 21
                                       SUB_LESS_EQ_SUB_SUC, 21
                                       SUB_LESS_TO_LESS_ADDL, 21
                                       SUB_LESS_TO_LESS_ADDR, 21
                                       SUB_PRE_SUB_1, 21
                                       SUB_SUB_ID, 21
                                       SUB_SUC, 21

\underline{Index 27}

SUB_SUC_PRE_SUB, 21

suc, theory, 4

SUC_0, 16
SUC_DIV_CASES, 23
SUC_DIV_SELF, 6, 23
SUC_GREATER_EQ_SUC, 4, 16
SUC_LESS_EQ, 16
SUC_LESS_EQ_PRE, 17
SUC_LESS_N_LESS, 19
SUC_LESS_PRE, 17
SUC_MAX, 24
SUC_MIN, 24
SUC_MOD, 23
SUC_MOD_SELF, 6, 23
SUC_NOT_0, 4, 16
SUC_PRE, 5, 17
SUC_SUB, 21
SUM_LESS, 19
zero_ineq, theory, 4
ZERO_LESS_TWO_EXP, 22