![\begin{definition}[ graph of a function defined by a test ]~
\begin{center}%
\af...
...aveVerb{Verb}ifP b x y z\marginpar{\UseVerb{Verb}}\end{center}\end{definition}](img88.png)
![\begin{definition}[ function defined by a test ]~
\begin{center}%
\afdmath{}{\ma...
...{Verb}if b then x else y\marginpar{\UseVerb{Verb}}\end{center}\end{definition}](img89.png)
Using the definite description operator, we can introduce a new function symbol if b then x else y.
![\begin{fact}[ Basic properties of %
\afdmath{}\$\text{\rm if}\endafdmath{}]\hspa...
...\rm if}.\text{\rm B}\endafdmath{} added as equation
\par
\end{itemize}\end{fact}](img90.png)
An alternative would be to add if b then x else y as a constant and replace the previous theorems by axioms. We prefer to limit the number of axioms because this should help to detect a contradiction in our assumptions. Moreover, we are not replacing two axioms by a more powerful one, because the definite description principle is a conservative axiom.
case.if.B added as introduction rule (abbrev: if , options: -t )
The case.if.B theorem can not be added as an introduction rule
because it would be an introduction rule for any predicate !
Nevertheless it is added as a "totality rule" (using the command new_intro -t. This tells the trivial tactic to use it when the goal is
of the form P (if b then c_1 else c_2) with P atomic. This is
useful to prove that functions using $if are total.
![\begin{fact}[ We prove the totality of these functions ]\hspace{1cm}
\begin{item...
...rule (abbrev: \verb ...](img93.png)
![\begin{fact}[ The equation for %
\afdmath{}\land\endafdmath{}]\hspace{1cm}
\begi...
...rFalse}.\text{\rm B}\endafdmath{} added as equation
\par
\end{itemize}\end{fact}](img94.png)
![\begin{fact}[ The equation for %
\afdmath{}\lor\endafdmath{}]\hspace{1cm}
\begin...
...rFalse}.\text{\rm B}\endafdmath{} added as equation
\par
\end{itemize}\end{fact}](img95.png)
![\begin{fact}[ The equation for %
\afdmath{}\neg\endafdmath{}]\hspace{1cm}
\begin...
... False}.\text{\rm B}\endafdmath{} added as equation
\par
\end{itemize}\end{fact}](img96.png)
Natural numbers : second order definitionChristophe Raffalli, Paul RoziereParis VII, Paris XII university