numLib.SUC_TO_NUMERAL_DEFN

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

num_CONV