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.

Then the list predicate is defined as follows:

We assume the following.

## 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

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

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)

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 )

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

## Decidability of equality

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