equal
deleted
inserted
replaced
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\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline |
|
24 {\isaliteral{22}{\isachardoublequoteopen}}add\ m\ {\isadigit{0}}\ {\isaliteral{3D}{\isacharequal}}\ m{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline |
|
25 {\isaliteral{22}{\isachardoublequoteopen}}add\ m\ {\isaliteral{28}{\isacharparenleft}}Suc\ n{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ add\ {\isaliteral{28}{\isacharparenleft}}Suc\ m{\isaliteral{29}{\isacharparenright}}\ n{\isaliteral{22}{\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 \ {\isaliteral{22}{\isachardoublequoteopen}}add\ m\ n\ {\isaliteral{3D}{\isacharequal}}\ m{\isaliteral{2B}{\isacharplus}}n{\isaliteral{22}{\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: |
|