| author | Walther Neuper <neuper@ist.tugraz.at> |
| Thu, 12 Aug 2010 15:03:34 +0200 | |
| branch | isac-from-Isabelle2009-2 |
| changeset 37913 | 20e3616b2d9c |
| parent 27015 | f8537d69f514 |
| child 40685 | 313a24b66a8d |
| permissions | -rw-r--r-- |
1 %
2 \begin{isabellebody}%
3 \def\isabellecontext{Plus}%
4 %
5 \isadelimtheory
6 %
7 \endisadelimtheory
8 %
9 \isatagtheory
10 %
11 \endisatagtheory
12 {\isafoldtheory}%
13 %
14 \isadelimtheory
15 %
16 \endisadelimtheory
17 %
18 \begin{isamarkuptext}%
19 \noindent Define the following addition function%
20 \end{isamarkuptext}%
21 \isamarkuptrue%
22 \isacommand{primrec}\isamarkupfalse%
23 \ add\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ nat{\isachardoublequoteclose}\ \isakeyword{where}\isanewline
24 {\isachardoublequoteopen}add\ m\ {\isadigit{0}}\ {\isacharequal}\ m{\isachardoublequoteclose}\ {\isacharbar}\isanewline
25 {\isachardoublequoteopen}add\ m\ {\isacharparenleft}Suc\ n{\isacharparenright}\ {\isacharequal}\ add\ {\isacharparenleft}Suc\ m{\isacharparenright}\ n{\isachardoublequoteclose}%
26 \begin{isamarkuptext}%
27 \noindent and prove%
28 \end{isamarkuptext}%
29 \isamarkuptrue%
30 %
31 \isadelimproof
32 %
33 \endisadelimproof
34 %
35 \isatagproof
36 %
37 \endisatagproof
38 {\isafoldproof}%
39 %
40 \isadelimproof
41 %
42 \endisadelimproof
43 \isacommand{lemma}\isamarkupfalse%
44 \ {\isachardoublequoteopen}add\ m\ n\ {\isacharequal}\ m{\isacharplus}n{\isachardoublequoteclose}%
45 \isadelimproof
46 %
47 \endisadelimproof
48 %
49 \isatagproof
50 %
51 \endisatagproof
52 {\isafoldproof}%
53 %
54 \isadelimproof
55 %
56 \endisadelimproof
57 %
58 \isadelimtheory
59 %
60 \endisadelimtheory
61 %
62 \isatagtheory
63 %
64 \endisatagtheory
65 {\isafoldtheory}%
66 %
67 \isadelimtheory
68 %
69 \endisadelimtheory
70 \end{isabellebody}%
71 %%% Local Variables:
72 %%% mode: latex
73 %%% TeX-master: "root"
74 %%% End: