4 \noindent |
4 \noindent |
5 In particular, there are \isa{case}-expressions, for example |
5 In particular, there are \isa{case}-expressions, for example |
6 \begin{quote} |
6 \begin{quote} |
7 |
7 |
8 \begin{isabelle}% |
8 \begin{isabelle}% |
9 case\ \mbox{n}\ of\ 0\ {\isasymRightarrow}\ 0\ |\ Suc\ \mbox{m}\ {\isasymRightarrow}\ \mbox{m} |
9 case\ \mbox{n}\ of\ \isadigit{0}\ {\isasymRightarrow}\ \isadigit{0}\ {\isacharbar}\ Suc\ \mbox{m}\ {\isasymRightarrow}\ \mbox{m} |
10 \end{isabelle}% |
10 \end{isabelle}% |
11 |
11 |
12 \end{quote} |
12 \end{quote} |
13 primitive recursion, for example% |
13 primitive recursion, for example% |
14 \end{isamarkuptext}% |
14 \end{isamarkuptext}% |
15 \isacommand{consts}\ sum\ ::\ {"}nat\ {\isasymRightarrow}\ nat{"}\isanewline |
15 \isacommand{consts}\ sum\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline |
16 \isacommand{primrec}\ {"}sum\ 0\ =\ 0{"}\isanewline |
16 \isacommand{primrec}\ {\isachardoublequote}sum\ \isadigit{0}\ {\isacharequal}\ \isadigit{0}{\isachardoublequote}\isanewline |
17 \ \ \ \ \ \ \ \ {"}sum\ (Suc\ n)\ =\ Suc\ n\ +\ sum\ n{"}% |
17 \ \ \ \ \ \ \ \ {\isachardoublequote}sum\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ Suc\ n\ {\isacharplus}\ sum\ n{\isachardoublequote}% |
18 \begin{isamarkuptext}% |
18 \begin{isamarkuptext}% |
19 \noindent |
19 \noindent |
20 and induction, for example% |
20 and induction, for example% |
21 \end{isamarkuptext}% |
21 \end{isamarkuptext}% |
22 \isacommand{lemma}\ {"}sum\ n\ +\ sum\ n\ =\ n*(Suc\ n){"}\isanewline |
22 \isacommand{lemma}\ {\isachardoublequote}sum\ n\ {\isacharplus}\ sum\ n\ {\isacharequal}\ n{\isacharasterisk}{\isacharparenleft}Suc\ n{\isacharparenright}{\isachardoublequote}\isanewline |
23 \isacommand{apply}(induct\_tac\ n)\isanewline |
23 \isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ n{\isacharparenright}\isanewline |
24 \isacommand{by}(auto)\isanewline |
24 \isacommand{by}{\isacharparenleft}auto{\isacharparenright}\isanewline |
25 \end{isabelle}% |
25 \end{isabelle}% |
26 %%% Local Variables: |
26 %%% Local Variables: |
27 %%% mode: latex |
27 %%% mode: latex |
28 %%% TeX-master: "root" |
28 %%% TeX-master: "root" |
29 %%% End: |
29 %%% End: |