Next:Defining functions by induction Up:User's manual of the Previous:Matching Contents

Subsections

Basic definitions and properties

Definitions and axioms

To define lists, we extend the language with one constant symbols [] and one binary function symbol x :: l.

$\begin{sort}[]~ \begin{center}list['a] \end{center}\end{sort}$

$\begin{constant}[ empty list ]~ \begin{center}% \afdmath{}[]\endafdmath{} : list['a] \SaveVerb{Verb}nil\marginpar{\UseVerb{Verb}}\end{center}\end{constant}$

$\begin{constant}[ cons ]~ \begin{center}% \afdmath{}\text{\it x}\,\, :: \;\;\;\;... ...['a] \SaveVerb{Verb}x :: y\marginpar{\UseVerb{Verb}}\end{center}\end{constant}$

Then the list predicate is defined as follows:

$\begin{definition}[]~ \begin{center}% \afdmath{}\rm I\hspace{-0.2em}L_{ \text{\i... ... \SaveVerb{Verb}List D x\marginpar{\UseVerb{Verb}}\end{center}\end{definition}$

We assume the following.

$\begin{axiom}[ ]\hspace{1cm} \begin{itemize} \item % \afdmath{}\text{\rm nil}\_\... ...ndprettybox{}\right)\endprettybox{}\endafdmmath{}} \par \end{itemize}\end{axiom}$

Rules on lists

We prove the introduction and elimination rules for lists.

These rules are added respectively as introdution and elimination rules, with the given abbreviations.

Introduction rules

$\begin{fact}[% \afdmath{}\text{\rm nil}.\text{\rm total}.\text{\rm List}\endafdm... ...}\ibreak{0.2em}{2.em} []\endprettybox{}\endprettybox{}\endafdmmath{} \end{fact}$

$\begin{fact}[% \afdmath{}\text{\rm cons}.\text{\rm total}.\text{\rm List}\endafd... ...;\; \text{\it l}\right)\endprettybox{}\endprettybox{}\endafdmmath{} \end{fact}$

nil.total.List added as introduction rule (abbrev: nil , options: -i -c )

cons.total.List added as introduction rule (abbrev: cons , options: -i -c )

Elimination rules

$\begin{fact}[% \afdmath{}\text{\rm rec}.\text{\rm List}\endafdmath{}]structural ... ...l}\endprettybox{}\endprettybox{}\right)\endprettybox{}\endafdmmath{} \end{fact}$

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

$\begin{fact}[% \afdmath{}\text{\rm case}\_\text{\rm left}.\text{\rm List}\endafd... ...em} \text{\it l}\endprettybox{}\right)\endprettybox{}\endafdmmath{} \end{fact}$

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

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

case.List added as elimination rule (abbrev: ocase , options: -n )

Left rules (eliminating list constructors)

$\begin{fact}[% \afdmath{}\text{\rm cons}\_\text{\rm not}\_\text{\rm nil}.\text{\... ...\ibreak{0.3em}{2.em} []\endprettybox{}\endprettybox{}\endafdmmath{} \end{fact}$

$\begin{fact}[% \afdmath{}\text{\rm cons}.\text{\rm injective}\_\text{\rm left}.\... ...reak{0.36em}{2.em} \text{\it X}\right)\endprettybox{}\endafdmmath{} \end{fact}$

These two facts and the first claim are added as invertible left rules. We close then definition of lists.

nil_not_cons.List added as elimination rule (abbrev: nil_not_cons , options: -i -n )

cons_not_nil.List added as elimination rule (abbrev: cons_not_nil , options: -i -n )

cons.injective_left.List added as elimination rule (abbrev: cons.injective_left , options: -i -n )

$\begin{fact}[% \afdmath{}\text{\rm cons}.\text{\rm left}.\text{\rm List}\endafdm... ...reak{0.36em}{2.em} \text{\it X}\right)\endprettybox{}\endafdmmath{} \end{fact}$

cons.left.List added as elimination rule (abbrev: cl , options: -i -n )

Decidability of equality

$\begin{fact}[% \afdmath{}\text{\rm eq}\_\text{\rm dec}.\text{\rm List}\endafdmat... ...-0.2em}L_{ \text{\it D}}\endprettybox{}\endprettybox{}\endafdmmath{} \end{fact}$

eq_dec.List added as introduction rule (abbrev: List , options: -i -t )

Next:Defining functions by induction Up:User's manual of the Previous:Matching Contents

Christophe Raffalli 2005-03-02