SUC_TO_NUMERAL_DEFN_CONV : conv
STRUCTURE
SYNOPSIS
Translates equations using SUC n to use numeral constructors instead.
DESCRIPTION
This conversion modifies conjunctions of universally quantified equations so that any argument terms of the form SUC x on the LHS of the equations (with x one of the equation’s universally quantified variables), are translated to a form appropriate for rewriting when the argument term is a numeral.

This procedure uses the following theorem:

  |- !f g. (!n. f (SUC n) = g n (SUC n)) =
           (!n. f (NUMERAL (NUMERAL_BIT1 n)) =
                g (NUMERAL (NUMERAL_BIT1 n))
                  (NUMERAL (NUMERAL_BIT1 n) - 1)) /\
           (!n. f (NUMERAL (NUMERAL_BIT2 n)) =
                g (NUMERAL (NUMERAL_BIT2 n))
                  (NUMERAL (NUMERAL_BIT1 n)))
EXAMPLE
- CONV_RULE SUC_TO_NUMERAL_DEFN_CONV arithmeticTheory.FACT;
> val it =
    |- (FACT 0 = 1) /\
       (!n.
          FACT (NUMERAL (NUMERAL_BIT1 n)) =
            NUMERAL (NUMERAL_BIT1 n) *
            FACT (NUMERAL (NUMERAL_BIT1 n) - 1)) /\
       !n.
         FACT (NUMERAL (NUMERAL_BIT2 n)) =
           NUMERAL (NUMERAL_BIT2 n) *
           FACT (NUMERAL (NUMERAL_BIT1 n)) : thm
FAILURE
Fails if the input term is not the conjunction of universally quantified equations, where there may be just one conjunct, and where equations may have no quantification at all. Those conjuncts which don’t involve terms of the form SUC x are returned unchanged.
COMMENTS
Useful for translating definitions over numbers (which often involve SUC terms), into a form that can be used to work with numerals easily.
SEEALSO
HOL  Kananaskis-10