|
1 % |
|
2 \begin{isabellebody}% |
|
3 \def\isabellecontext{ABexpr}% |
|
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 \index{datatypes!mutually recursive}% |
|
20 Sometimes it is necessary to define two datatypes that depend on each |
|
21 other. This is called \textbf{mutual recursion}. As an example consider a |
|
22 language of arithmetic and boolean expressions where |
|
23 \begin{itemize} |
|
24 \item arithmetic expressions contain boolean expressions because there are |
|
25 conditional expressions like ``if $m<n$ then $n-m$ else $m-n$'', |
|
26 and |
|
27 \item boolean expressions contain arithmetic expressions because of |
|
28 comparisons like ``$m<n$''. |
|
29 \end{itemize} |
|
30 In Isabelle this becomes% |
|
31 \end{isamarkuptext}% |
|
32 \isamarkuptrue% |
|
33 \isacommand{datatype}\isamarkupfalse% |
|
34 \ {\isaliteral{27}{\isacharprime}}a\ aexp\ {\isaliteral{3D}{\isacharequal}}\ IF\ \ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ bexp{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ aexp{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ aexp{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
35 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{7C}{\isacharbar}}\ Sum\ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ aexp{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ aexp{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
36 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{7C}{\isacharbar}}\ Diff\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ aexp{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ aexp{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
37 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{7C}{\isacharbar}}\ Var\ {\isaliteral{27}{\isacharprime}}a\isanewline |
|
38 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{7C}{\isacharbar}}\ Num\ nat\isanewline |
|
39 \isakeyword{and}\ \ \ \ \ \ {\isaliteral{27}{\isacharprime}}a\ bexp\ {\isaliteral{3D}{\isacharequal}}\ Less\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ aexp{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ aexp{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
40 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{7C}{\isacharbar}}\ And\ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ bexp{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ bexp{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
41 \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isaliteral{7C}{\isacharbar}}\ Neg\ \ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ bexp{\isaliteral{22}{\isachardoublequoteclose}}% |
|
42 \begin{isamarkuptext}% |
|
43 \noindent |
|
44 Type \isa{aexp} is similar to \isa{expr} in \S\ref{sec:ExprCompiler}, |
|
45 except that we have added an \isa{IF} constructor, |
|
46 fixed the values to be of type \isa{nat} and declared the two binary |
|
47 operations \isa{Sum} and \isa{Diff}. Boolean |
|
48 expressions can be arithmetic comparisons, conjunctions and negations. |
|
49 The semantics is given by two evaluation functions:% |
|
50 \end{isamarkuptext}% |
|
51 \isamarkuptrue% |
|
52 \isacommand{primrec}\isamarkupfalse% |
|
53 \ evala\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ aexp\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{and}\isanewline |
|
54 \ \ \ \ \ \ \ \ \ evalb\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{27}{\isacharprime}}a\ bexp\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ bool{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline |
|
55 {\isaliteral{22}{\isachardoublequoteopen}}evala\ {\isaliteral{28}{\isacharparenleft}}IF\ b\ a{\isadigit{1}}\ a{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ env\ {\isaliteral{3D}{\isacharequal}}\isanewline |
|
56 \ \ \ {\isaliteral{28}{\isacharparenleft}}if\ evalb\ b\ env\ then\ evala\ a{\isadigit{1}}\ env\ else\ evala\ a{\isadigit{2}}\ env{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline |
|
57 {\isaliteral{22}{\isachardoublequoteopen}}evala\ {\isaliteral{28}{\isacharparenleft}}Sum\ a{\isadigit{1}}\ a{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ env\ {\isaliteral{3D}{\isacharequal}}\ evala\ a{\isadigit{1}}\ env\ {\isaliteral{2B}{\isacharplus}}\ evala\ a{\isadigit{2}}\ env{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline |
|
58 {\isaliteral{22}{\isachardoublequoteopen}}evala\ {\isaliteral{28}{\isacharparenleft}}Diff\ a{\isadigit{1}}\ a{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ env\ {\isaliteral{3D}{\isacharequal}}\ evala\ a{\isadigit{1}}\ env\ {\isaliteral{2D}{\isacharminus}}\ evala\ a{\isadigit{2}}\ env{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline |
|
59 {\isaliteral{22}{\isachardoublequoteopen}}evala\ {\isaliteral{28}{\isacharparenleft}}Var\ v{\isaliteral{29}{\isacharparenright}}\ env\ {\isaliteral{3D}{\isacharequal}}\ env\ v{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline |
|
60 {\isaliteral{22}{\isachardoublequoteopen}}evala\ {\isaliteral{28}{\isacharparenleft}}Num\ n{\isaliteral{29}{\isacharparenright}}\ env\ {\isaliteral{3D}{\isacharequal}}\ n{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline |
|
61 \isanewline |
|
62 {\isaliteral{22}{\isachardoublequoteopen}}evalb\ {\isaliteral{28}{\isacharparenleft}}Less\ a{\isadigit{1}}\ a{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ env\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}evala\ a{\isadigit{1}}\ env\ {\isaliteral{3C}{\isacharless}}\ evala\ a{\isadigit{2}}\ env{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline |
|
63 {\isaliteral{22}{\isachardoublequoteopen}}evalb\ {\isaliteral{28}{\isacharparenleft}}And\ b{\isadigit{1}}\ b{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ env\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}evalb\ b{\isadigit{1}}\ env\ {\isaliteral{5C3C616E643E}{\isasymand}}\ evalb\ b{\isadigit{2}}\ env{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline |
|
64 {\isaliteral{22}{\isachardoublequoteopen}}evalb\ {\isaliteral{28}{\isacharparenleft}}Neg\ b{\isaliteral{29}{\isacharparenright}}\ env\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}\ evalb\ b\ env{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}% |
|
65 \begin{isamarkuptext}% |
|
66 \noindent |
|
67 |
|
68 Both take an expression and an environment (a mapping from variables |
|
69 \isa{{\isaliteral{27}{\isacharprime}}a} to values \isa{nat}) and return its arithmetic/boolean |
|
70 value. Since the datatypes are mutually recursive, so are functions |
|
71 that operate on them. Hence they need to be defined in a single |
|
72 \isacommand{primrec} section. Notice the \isakeyword{and} separating |
|
73 the declarations of \isa{evala} and \isa{evalb}. Their defining |
|
74 equations need not be split into two groups; |
|
75 the empty line is purely for readability. |
|
76 |
|
77 In the same fashion we also define two functions that perform substitution:% |
|
78 \end{isamarkuptext}% |
|
79 \isamarkuptrue% |
|
80 \isacommand{primrec}\isamarkupfalse% |
|
81 \ substa\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ aexp{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ aexp\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ aexp{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{and}\isanewline |
|
82 \ \ \ \ \ \ \ \ \ substb\ {\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}\ {\isaliteral{22}{\isachardoublequoteopen}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{27}{\isacharprime}}a\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ aexp{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ bexp\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}b\ bexp{\isaliteral{22}{\isachardoublequoteclose}}\ \isakeyword{where}\isanewline |
|
83 {\isaliteral{22}{\isachardoublequoteopen}}substa\ s\ {\isaliteral{28}{\isacharparenleft}}IF\ b\ a{\isadigit{1}}\ a{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\isanewline |
|
84 \ \ \ IF\ {\isaliteral{28}{\isacharparenleft}}substb\ s\ b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}substa\ s\ a{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}substa\ s\ a{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline |
|
85 {\isaliteral{22}{\isachardoublequoteopen}}substa\ s\ {\isaliteral{28}{\isacharparenleft}}Sum\ a{\isadigit{1}}\ a{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ Sum\ {\isaliteral{28}{\isacharparenleft}}substa\ s\ a{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}substa\ s\ a{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline |
|
86 {\isaliteral{22}{\isachardoublequoteopen}}substa\ s\ {\isaliteral{28}{\isacharparenleft}}Diff\ a{\isadigit{1}}\ a{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ Diff\ {\isaliteral{28}{\isacharparenleft}}substa\ s\ a{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}substa\ s\ a{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline |
|
87 {\isaliteral{22}{\isachardoublequoteopen}}substa\ s\ {\isaliteral{28}{\isacharparenleft}}Var\ v{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ s\ v{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline |
|
88 {\isaliteral{22}{\isachardoublequoteopen}}substa\ s\ {\isaliteral{28}{\isacharparenleft}}Num\ n{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ Num\ n{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline |
|
89 \isanewline |
|
90 {\isaliteral{22}{\isachardoublequoteopen}}substb\ s\ {\isaliteral{28}{\isacharparenleft}}Less\ a{\isadigit{1}}\ a{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ Less\ {\isaliteral{28}{\isacharparenleft}}substa\ s\ a{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}substa\ s\ a{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline |
|
91 {\isaliteral{22}{\isachardoublequoteopen}}substb\ s\ {\isaliteral{28}{\isacharparenleft}}And\ b{\isadigit{1}}\ b{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ And\ {\isaliteral{28}{\isacharparenleft}}substb\ s\ b{\isadigit{1}}{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{28}{\isacharparenleft}}substb\ s\ b{\isadigit{2}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\ {\isaliteral{7C}{\isacharbar}}\isanewline |
|
92 {\isaliteral{22}{\isachardoublequoteopen}}substb\ s\ {\isaliteral{28}{\isacharparenleft}}Neg\ b{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ Neg\ {\isaliteral{28}{\isacharparenleft}}substb\ s\ b{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}% |
|
93 \begin{isamarkuptext}% |
|
94 \noindent |
|
95 Their first argument is a function mapping variables to expressions, the |
|
96 substitution. It is applied to all variables in the second argument. As a |
|
97 result, the type of variables in the expression may change from \isa{{\isaliteral{27}{\isacharprime}}a} |
|
98 to \isa{{\isaliteral{27}{\isacharprime}}b}. Note that there are only arithmetic and no boolean variables. |
|
99 |
|
100 Now we can prove a fundamental theorem about the interaction between |
|
101 evaluation and substitution: applying a substitution $s$ to an expression $a$ |
|
102 and evaluating the result in an environment $env$ yields the same result as |
|
103 evaluation $a$ in the environment that maps every variable $x$ to the value |
|
104 of $s(x)$ under $env$. If you try to prove this separately for arithmetic or |
|
105 boolean expressions (by induction), you find that you always need the other |
|
106 theorem in the induction step. Therefore you need to state and prove both |
|
107 theorems simultaneously:% |
|
108 \end{isamarkuptext}% |
|
109 \isamarkuptrue% |
|
110 \isacommand{lemma}\isamarkupfalse% |
|
111 \ {\isaliteral{22}{\isachardoublequoteopen}}evala\ {\isaliteral{28}{\isacharparenleft}}substa\ s\ a{\isaliteral{29}{\isacharparenright}}\ env\ {\isaliteral{3D}{\isacharequal}}\ evala\ a\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x{\isaliteral{2E}{\isachardot}}\ evala\ {\isaliteral{28}{\isacharparenleft}}s\ x{\isaliteral{29}{\isacharparenright}}\ env{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\isanewline |
|
112 \ \ \ \ \ \ \ \ evalb\ {\isaliteral{28}{\isacharparenleft}}substb\ s\ b{\isaliteral{29}{\isacharparenright}}\ env\ {\isaliteral{3D}{\isacharequal}}\ evalb\ b\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6C616D6264613E}{\isasymlambda}}x{\isaliteral{2E}{\isachardot}}\ evala\ {\isaliteral{28}{\isacharparenleft}}s\ x{\isaliteral{29}{\isacharparenright}}\ env{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequoteclose}}\isanewline |
|
113 % |
|
114 \isadelimproof |
|
115 % |
|
116 \endisadelimproof |
|
117 % |
|
118 \isatagproof |
|
119 \isacommand{apply}\isamarkupfalse% |
|
120 {\isaliteral{28}{\isacharparenleft}}induct{\isaliteral{5F}{\isacharunderscore}}tac\ a\ \isakeyword{and}\ b{\isaliteral{29}{\isacharparenright}}% |
|
121 \begin{isamarkuptxt}% |
|
122 \noindent The resulting 8 goals (one for each constructor) are proved in one fell swoop:% |
|
123 \end{isamarkuptxt}% |
|
124 \isamarkuptrue% |
|
125 \isacommand{apply}\isamarkupfalse% |
|
126 \ simp{\isaliteral{5F}{\isacharunderscore}}all% |
|
127 \endisatagproof |
|
128 {\isafoldproof}% |
|
129 % |
|
130 \isadelimproof |
|
131 % |
|
132 \endisadelimproof |
|
133 % |
|
134 \begin{isamarkuptext}% |
|
135 In general, given $n$ mutually recursive datatypes $\tau@1$, \dots, $\tau@n$, |
|
136 an inductive proof expects a goal of the form |
|
137 \[ P@1(x@1)\ \land \dots \land P@n(x@n) \] |
|
138 where each variable $x@i$ is of type $\tau@i$. Induction is started by |
|
139 \begin{isabelle} |
|
140 \isacommand{apply}\isa{{\isaliteral{28}{\isacharparenleft}}induct{\isaliteral{5F}{\isacharunderscore}}tac} $x@1$ \isacommand{and} \dots\ \isacommand{and} $x@n$\isa{{\isaliteral{29}{\isacharparenright}}} |
|
141 \end{isabelle} |
|
142 |
|
143 \begin{exercise} |
|
144 Define a function \isa{norma} of type \isa{{\isaliteral{27}{\isacharprime}}a\ aexp\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ {\isaliteral{27}{\isacharprime}}a\ aexp} that |
|
145 replaces \isa{IF}s with complex boolean conditions by nested |
|
146 \isa{IF}s; it should eliminate the constructors |
|
147 \isa{And} and \isa{Neg}, leaving only \isa{Less}. |
|
148 Prove that \isa{norma} |
|
149 preserves the value of an expression and that the result of \isa{norma} |
|
150 is really normal, i.e.\ no more \isa{And}s and \isa{Neg}s occur in |
|
151 it. ({\em Hint:} proceed as in \S\ref{sec:boolex} and read the discussion |
|
152 of type annotations following lemma \isa{subst{\isaliteral{5F}{\isacharunderscore}}id} below). |
|
153 \end{exercise}% |
|
154 \end{isamarkuptext}% |
|
155 \isamarkuptrue% |
|
156 % |
|
157 \isadelimproof |
|
158 % |
|
159 \endisadelimproof |
|
160 % |
|
161 \isatagproof |
|
162 % |
|
163 \endisatagproof |
|
164 {\isafoldproof}% |
|
165 % |
|
166 \isadelimproof |
|
167 % |
|
168 \endisadelimproof |
|
169 % |
|
170 \isadelimproof |
|
171 % |
|
172 \endisadelimproof |
|
173 % |
|
174 \isatagproof |
|
175 % |
|
176 \endisatagproof |
|
177 {\isafoldproof}% |
|
178 % |
|
179 \isadelimproof |
|
180 % |
|
181 \endisadelimproof |
|
182 % |
|
183 \isadelimtheory |
|
184 % |
|
185 \endisadelimtheory |
|
186 % |
|
187 \isatagtheory |
|
188 % |
|
189 \endisatagtheory |
|
190 {\isafoldtheory}% |
|
191 % |
|
192 \isadelimtheory |
|
193 % |
|
194 \endisadelimtheory |
|
195 \end{isabellebody}% |
|
196 %%% Local Variables: |
|
197 %%% mode: latex |
|
198 %%% TeX-master: "root" |
|
199 %%% End: |