Next: Matching Up: User's manual of the Previous: Lexicographic ordering Contents

Basic definitions

To define the sums (disjoint union) of two predicates, we extend the language with two unary function symbols inl x and inr x .
$\begin{sort}[]~ \begin{center}sum['a,'b] \end{center}\end{sort}$

$\begin{constant}[]~ \begin{center}% \afdmath{}\text{\rm inl}\endafdmath{} : 'a $... ...'a, 'b] \SaveVerb{Verb}śinlś\marginpar{\UseVerb{Verb}}\end{center}\end{constant}$

$\begin{constant}[]~ \begin{center}% \afdmath{}\text{\rm inr}\endafdmath{} : 'b $... ...'a, 'b] \SaveVerb{Verb}śinrś\marginpar{\UseVerb{Verb}}\end{center}\end{constant}$

$\begin{definition}[ Sum of predicates ]~ \begin{center}% \afdmath{}(\text{\it A}... ...\SaveVerb{Verb}śSum A B zś\marginpar{\UseVerb{Verb}}\end{center}\end{definition}$

$\begin{axiom}[ ]\hspace{1cm} \begin{itemize} \item % \afdmath{}\text{\rm inl}.\t... ...box{}\endprettybox{}\endprettybox{}\endafdmmath{}} \par \end{itemize}\end{axiom}$

inl_not_inr.Sum added as elimination rule (abbrev: inl_not_inr , options: -i -n )

The last claim is added as invertible elimination rule.

$\begin{fact}[ Introduction rules for sums ]\hspace{1cm} \begin{itemize} \item % ... ...tion rule (abbrev: \verb ...$

$\begin{fact}[ elimination rules for sums ]\hspace{1cm} \begin{itemize} \item % \... ...ev: \verb ...$

These four rules and are added as invertible elimination rules.

Christophe Raffalli 2005-03-02