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

$\begin{definition}[ Church integers ]\hspace{1cm} \begin{itemize} \item nat \ite... ...h{} \SaveVerb{Verb}¶N x¶\marginpar{\UseVerb{Verb}} \end{itemize}\end{definition}$

Introduction rules for I N.

$\begin{fact}[% \afdmath{}\text{\rm N}0.\text{\rm total}.\text{\rm N}\endafdmath{... ...\hspace{-0.2em}N}\ibreak{0.2em}{2.em} 0\endprettybox{}\endafdmmath{} \end{fact}$

$\begin{fact}[% \afdmath{}\text{\rm S}.\text{\rm total}.\text{\rm N}\endafdmath{}... ...em} \text{\it x}\right)\endprettybox{}\endprettybox{}\endafdmmath{} \end{fact}$

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.

Induction on natural number as an elimination rule.

$\begin{fact}[% \afdmath{}\text{\rm rec}.\text{\rm N}\endafdmath{}]Induction on %... ...x}\endprettybox{}\endprettybox{}\right)\endprettybox{}\endafdmmath{} \end{fact}$

Elimination by case on I N.

$\begin{fact}[% \afdmath{}\text{\rm case}.\text{\rm N}\endafdmath{}]case on % \af... ...{}\endprettybox{}\endprettybox{}\right)\endprettybox{}\endafdmmath{} \end{fact}$

$\begin{fact}[% \afdmath{}\text{\rm case}\_\text{\rm left}.\text{\rm N}\endafdmat... ...em} \text{\it x}\endprettybox{}\right)\endprettybox{}\endafdmmath{} \end{fact}$

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.
$\begin{axiom}[ ]\hspace{1cm} \begin{itemize} \item % \afdmath{}\text{\rm N}0\_\t... ...ndprettybox{}\right)\endprettybox{}\endafdmmath{}} \par \end{itemize}\end{axiom}$

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

$\begin{fact}[ Showing that integers are distincts. ]\hspace{1cm} \begin{itemize}... ...(abbrev: \verb ...$

./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