Next: Properties of basic operations Up: User's manual of the Previous: Definition of functions on   Contents

Subsections

# Basic definitions.

To define the natural numbers, we extend the language with one contant symbol 0 and one unary function symbol S x. Then the natural numbers are defined by the following predicate I N x

## Introduction rules for I N.

N0.total.N added as introduction rule (abbrev: N0 , options:  -i -c )

S.total.N added as introduction rule (abbrev: S , options:  -i -c )

## Elimination rules for I N.

### Elimination by case on I N.

case_left.N added as elimination rule (abbrev: case , options:  -n )

rec.N added as elimination rule (abbrev: rec , options:  )

The introduction rules are added with the command new_intro -c. The option -c indicates that 0 and S are constructors and the trivial tactic will try to use these rules when the goal is of the form P 0 or P (S t) even if P is a unification variable.

The elimination rules are added with the command new_elim using the option -n for case.N. This tells PhoX that this second rule is not necessary for completeness.

The abbreviations are given with the rules. For instance, elim case.N with H is equivalent to elim H with [case] and elim N0.total.N  is equivalent to intro N0.

## left rules for = on I N

We add usual axioms of Peano Arithmetic.

We also prove the following left rules for natural numbers (the first one is an axiom ).

./nat.tex ./nat_ax.tex

ProductsChristophe Raffalli, Paul RoziereEquipe de Logique, Université Chambéry, Paris VII

Next: Properties of basic operations Up: User's manual of the Previous: Definition of functions on   Contents
Christophe Raffalli 2005-03-02