doc-src/TutorialI/Misc/document/natsum.tex

*** empty log message ***

%
\begin{isabellebody}%
\def\isabellecontext{natsum}%
%
\begin{isamarkuptext}%
\noindent
In particular, there are \isa{case}-expressions, for example
\begin{isabelle}%
\ \ \ \ \ case\ n\ of\ {\isadigit{0}}\ {\isasymRightarrow}\ {\isadigit{0}}\ {\isacharbar}\ Suc\ m\ {\isasymRightarrow}\ m%
\end{isabelle}
primitive recursion, for example%
\end{isamarkuptext}%
\isacommand{consts}\ sum\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
\isacommand{primrec}\ {\isachardoublequote}sum\ {\isadigit{0}}\ {\isacharequal}\ {\isadigit{0}}{\isachardoublequote}\isanewline
\ \ \ \ \ \ \ \ {\isachardoublequote}sum\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ Suc\ n\ {\isacharplus}\ sum\ n{\isachardoublequote}%
\begin{isamarkuptext}%
\noindent
and induction, for example%
\end{isamarkuptext}%
\isacommand{lemma}\ {\isachardoublequote}sum\ n\ {\isacharplus}\ sum\ n\ {\isacharequal}\ n{\isacharasterisk}{\isacharparenleft}Suc\ n{\isacharparenright}{\isachardoublequote}\isanewline
\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ n{\isacharparenright}\isanewline
\isacommand{apply}{\isacharparenleft}auto{\isacharparenright}\isanewline
\isacommand{done}\isanewline
\end{isabellebody}%
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "root"
%%% End: