| author | nipkow |
| Tue, 05 Sep 2000 09:03:17 +0200 | |
| changeset 9834 | 109b11c4e77e |
| parent 9792 | bbefb6ce5cb2 |
| child 9924 | 3370f6aa3200 |
| permissions | -rw-r--r-- |
| nipkow@9722 | 1 |
% |
| nipkow@9722 | 2 |
\begin{isabellebody}%
|
| nipkow@8749 | 3 |
% |
| nipkow@8749 | 4 |
\begin{isamarkuptext}%
|
| nipkow@8749 | 5 |
\noindent |
| nipkow@9541 | 6 |
In particular, there are \isa{case}-expressions, for example
|
| nipkow@9834 | 7 |
% |
| nipkow@9541 | 8 |
\begin{isabelle}%
|
| nipkow@9834 | 9 |
\ \ \ \ \ case\ n\ of\ \isadigit{0}\ {\isasymRightarrow}\ \isadigit{0}\ {\isacharbar}\ Suc\ m\ {\isasymRightarrow}\ m%
|
| nipkow@9541 | 10 |
\end{isabelle}%
|
| nipkow@9541 | 11 |
|
| nipkow@8749 | 12 |
primitive recursion, for example% |
| nipkow@8749 | 13 |
\end{isamarkuptext}%
|
| wenzelm@9673 | 14 |
\isacommand{consts}\ sum\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
|
| wenzelm@9673 | 15 |
\isacommand{primrec}\ {\isachardoublequote}sum\ \isadigit{0}\ {\isacharequal}\ \isadigit{0}{\isachardoublequote}\isanewline
|
| wenzelm@9673 | 16 |
\ \ \ \ \ \ \ \ {\isachardoublequote}sum\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ Suc\ n\ {\isacharplus}\ sum\ n{\isachardoublequote}%
|
| nipkow@8749 | 17 |
\begin{isamarkuptext}%
|
| nipkow@8749 | 18 |
\noindent |
| nipkow@8749 | 19 |
and induction, for example% |
| nipkow@8749 | 20 |
\end{isamarkuptext}%
|
| wenzelm@9673 | 21 |
\isacommand{lemma}\ {\isachardoublequote}sum\ n\ {\isacharplus}\ sum\ n\ {\isacharequal}\ n{\isacharasterisk}{\isacharparenleft}Suc\ n{\isacharparenright}{\isachardoublequote}\isanewline
|
| wenzelm@9673 | 22 |
\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ n{\isacharparenright}\isanewline
|
| wenzelm@9673 | 23 |
\isacommand{by}{\isacharparenleft}auto{\isacharparenright}\isanewline
|
| nipkow@9722 | 24 |
\end{isabellebody}%
|
| wenzelm@9145 | 25 |
%%% Local Variables: |
| wenzelm@9145 | 26 |
%%% mode: latex |
| wenzelm@9145 | 27 |
%%% TeX-master: "root" |
| wenzelm@9145 | 28 |
%%% End: |