9722
|
1 |
%
|
|
2 |
\begin{isabellebody}%
|
9924
|
3 |
\def\isabellecontext{Ifexpr}%
|
17056
|
4 |
%
|
|
5 |
\isadelimtheory
|
|
6 |
%
|
|
7 |
\endisadelimtheory
|
|
8 |
%
|
|
9 |
\isatagtheory
|
|
10 |
%
|
|
11 |
\endisatagtheory
|
|
12 |
{\isafoldtheory}%
|
|
13 |
%
|
|
14 |
\isadelimtheory
|
|
15 |
%
|
|
16 |
\endisadelimtheory
|
|
17 |
\isamarkuptrue%
|
8749
|
18 |
%
|
10878
|
19 |
\isamarkupsubsection{Case Study: Boolean Expressions%
|
10395
|
20 |
}
|
11866
|
21 |
\isamarkuptrue%
|
9933
|
22 |
%
|
8749
|
23 |
\begin{isamarkuptext}%
|
11456
|
24 |
\label{sec:boolex}\index{boolean expressions example|(}
|
9933
|
25 |
The aim of this case study is twofold: it shows how to model boolean
|
|
26 |
expressions and some algorithms for manipulating them, and it demonstrates
|
|
27 |
the constructs introduced above.%
|
|
28 |
\end{isamarkuptext}%
|
11866
|
29 |
\isamarkuptrue%
|
9933
|
30 |
%
|
10978
|
31 |
\isamarkupsubsubsection{Modelling Boolean Expressions%
|
10395
|
32 |
}
|
11866
|
33 |
\isamarkuptrue%
|
9933
|
34 |
%
|
|
35 |
\begin{isamarkuptext}%
|
8749
|
36 |
We want to represent boolean expressions built up from variables and
|
|
37 |
constants by negation and conjunction. The following datatype serves exactly
|
|
38 |
that purpose:%
|
|
39 |
\end{isamarkuptext}%
|
17056
|
40 |
\isamarkupfalse%
|
9673
|
41 |
\isacommand{datatype}\ boolex\ {\isacharequal}\ Const\ bool\ {\isacharbar}\ Var\ nat\ {\isacharbar}\ Neg\ boolex\isanewline
|
17056
|
42 |
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ {\isacharbar}\ And\ boolex\ boolex\isamarkuptrue%
|
11866
|
43 |
%
|
8749
|
44 |
\begin{isamarkuptext}%
|
|
45 |
\noindent
|
9541
|
46 |
The two constants are represented by \isa{Const\ True} and
|
|
47 |
\isa{Const\ False}. Variables are represented by terms of the form
|
9792
|
48 |
\isa{Var\ n}, where \isa{n} is a natural number (type \isa{nat}).
|
8749
|
49 |
For example, the formula $P@0 \land \neg P@1$ is represented by the term
|
10187
|
50 |
\isa{And\ {\isacharparenleft}Var\ {\isadigit{0}}{\isacharparenright}\ {\isacharparenleft}Neg\ {\isacharparenleft}Var\ {\isadigit{1}}{\isacharparenright}{\isacharparenright}}.
|
8749
|
51 |
|
10978
|
52 |
\subsubsection{The Value of a Boolean Expression}
|
8749
|
53 |
|
|
54 |
The value of a boolean expression depends on the value of its variables.
|
9792
|
55 |
Hence the function \isa{value} takes an additional parameter, an
|
|
56 |
\emph{environment} of type \isa{nat\ {\isasymRightarrow}\ bool}, which maps variables to their
|
|
57 |
values:%
|
8749
|
58 |
\end{isamarkuptext}%
|
17056
|
59 |
\isamarkupfalse%
|
9673
|
60 |
\isacommand{consts}\ value\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}boolex\ {\isasymRightarrow}\ {\isacharparenleft}nat\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ bool{\isachardoublequote}\isanewline
|
11866
|
61 |
\isamarkupfalse%
|
8749
|
62 |
\isacommand{primrec}\isanewline
|
9673
|
63 |
{\isachardoublequote}value\ {\isacharparenleft}Const\ b{\isacharparenright}\ env\ {\isacharequal}\ b{\isachardoublequote}\isanewline
|
|
64 |
{\isachardoublequote}value\ {\isacharparenleft}Var\ x{\isacharparenright}\ \ \ env\ {\isacharequal}\ env\ x{\isachardoublequote}\isanewline
|
|
65 |
{\isachardoublequote}value\ {\isacharparenleft}Neg\ b{\isacharparenright}\ \ \ env\ {\isacharequal}\ {\isacharparenleft}{\isasymnot}\ value\ b\ env{\isacharparenright}{\isachardoublequote}\isanewline
|
17056
|
66 |
{\isachardoublequote}value\ {\isacharparenleft}And\ b\ c{\isacharparenright}\ env\ {\isacharequal}\ {\isacharparenleft}value\ b\ env\ {\isasymand}\ value\ c\ env{\isacharparenright}{\isachardoublequote}\isamarkuptrue%
|
11866
|
67 |
%
|
8749
|
68 |
\begin{isamarkuptext}%
|
|
69 |
\noindent
|
10878
|
70 |
\subsubsection{If-Expressions}
|
8749
|
71 |
|
|
72 |
An alternative and often more efficient (because in a certain sense
|
|
73 |
canonical) representation are so-called \emph{If-expressions} built up
|
|
74 |
from constants (\isa{CIF}), variables (\isa{VIF}) and conditionals
|
|
75 |
(\isa{IF}):%
|
|
76 |
\end{isamarkuptext}%
|
17056
|
77 |
\isamarkupfalse%
|
|
78 |
\isacommand{datatype}\ ifex\ {\isacharequal}\ CIF\ bool\ {\isacharbar}\ VIF\ nat\ {\isacharbar}\ IF\ ifex\ ifex\ ifex\isamarkuptrue%
|
11866
|
79 |
%
|
8749
|
80 |
\begin{isamarkuptext}%
|
|
81 |
\noindent
|
10971
|
82 |
The evaluation of If-expressions proceeds as for \isa{boolex}:%
|
8749
|
83 |
\end{isamarkuptext}%
|
17056
|
84 |
\isamarkupfalse%
|
9673
|
85 |
\isacommand{consts}\ valif\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}ifex\ {\isasymRightarrow}\ {\isacharparenleft}nat\ {\isasymRightarrow}\ bool{\isacharparenright}\ {\isasymRightarrow}\ bool{\isachardoublequote}\isanewline
|
11866
|
86 |
\isamarkupfalse%
|
8749
|
87 |
\isacommand{primrec}\isanewline
|
9673
|
88 |
{\isachardoublequote}valif\ {\isacharparenleft}CIF\ b{\isacharparenright}\ \ \ \ env\ {\isacharequal}\ b{\isachardoublequote}\isanewline
|
|
89 |
{\isachardoublequote}valif\ {\isacharparenleft}VIF\ x{\isacharparenright}\ \ \ \ env\ {\isacharequal}\ env\ x{\isachardoublequote}\isanewline
|
|
90 |
{\isachardoublequote}valif\ {\isacharparenleft}IF\ b\ t\ e{\isacharparenright}\ env\ {\isacharequal}\ {\isacharparenleft}if\ valif\ b\ env\ then\ valif\ t\ env\isanewline
|
17056
|
91 |
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ else\ valif\ e\ env{\isacharparenright}{\isachardoublequote}\isamarkuptrue%
|
11866
|
92 |
%
|
8749
|
93 |
\begin{isamarkuptext}%
|
10978
|
94 |
\subsubsection{Converting Boolean and If-Expressions}
|
8749
|
95 |
|
|
96 |
The type \isa{boolex} is close to the customary representation of logical
|
8771
|
97 |
formulae, whereas \isa{ifex} is designed for efficiency. It is easy to
|
8749
|
98 |
translate from \isa{boolex} into \isa{ifex}:%
|
|
99 |
\end{isamarkuptext}%
|
17056
|
100 |
\isamarkupfalse%
|
10187
|
101 |
\isacommand{consts}\ bool{\isadigit{2}}if\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}boolex\ {\isasymRightarrow}\ ifex{\isachardoublequote}\isanewline
|
11866
|
102 |
\isamarkupfalse%
|
8749
|
103 |
\isacommand{primrec}\isanewline
|
10187
|
104 |
{\isachardoublequote}bool{\isadigit{2}}if\ {\isacharparenleft}Const\ b{\isacharparenright}\ {\isacharequal}\ CIF\ b{\isachardoublequote}\isanewline
|
|
105 |
{\isachardoublequote}bool{\isadigit{2}}if\ {\isacharparenleft}Var\ x{\isacharparenright}\ \ \ {\isacharequal}\ VIF\ x{\isachardoublequote}\isanewline
|
|
106 |
{\isachardoublequote}bool{\isadigit{2}}if\ {\isacharparenleft}Neg\ b{\isacharparenright}\ \ \ {\isacharequal}\ IF\ {\isacharparenleft}bool{\isadigit{2}}if\ b{\isacharparenright}\ {\isacharparenleft}CIF\ False{\isacharparenright}\ {\isacharparenleft}CIF\ True{\isacharparenright}{\isachardoublequote}\isanewline
|
17056
|
107 |
{\isachardoublequote}bool{\isadigit{2}}if\ {\isacharparenleft}And\ b\ c{\isacharparenright}\ {\isacharequal}\ IF\ {\isacharparenleft}bool{\isadigit{2}}if\ b{\isacharparenright}\ {\isacharparenleft}bool{\isadigit{2}}if\ c{\isacharparenright}\ {\isacharparenleft}CIF\ False{\isacharparenright}{\isachardoublequote}\isamarkuptrue%
|
11866
|
108 |
%
|
8749
|
109 |
\begin{isamarkuptext}%
|
|
110 |
\noindent
|
10187
|
111 |
At last, we have something we can verify: that \isa{bool{\isadigit{2}}if} preserves the
|
8749
|
112 |
value of its argument:%
|
|
113 |
\end{isamarkuptext}%
|
17056
|
114 |
\isamarkupfalse%
|
|
115 |
\isacommand{lemma}\ {\isachardoublequote}valif\ {\isacharparenleft}bool{\isadigit{2}}if\ b{\isacharparenright}\ env\ {\isacharequal}\ value\ b\ env{\isachardoublequote}%
|
|
116 |
\isadelimproof
|
|
117 |
%
|
|
118 |
\endisadelimproof
|
|
119 |
%
|
|
120 |
\isatagproof
|
11866
|
121 |
\isamarkuptrue%
|
16069
|
122 |
%
|
|
123 |
\begin{isamarkuptxt}%
|
|
124 |
\noindent
|
|
125 |
The proof is canonical:%
|
|
126 |
\end{isamarkuptxt}%
|
17056
|
127 |
\isamarkupfalse%
|
16069
|
128 |
\isacommand{apply}{\isacharparenleft}induct{\isacharunderscore}tac\ b{\isacharparenright}\isanewline
|
15481
|
129 |
\isamarkupfalse%
|
16069
|
130 |
\isacommand{apply}{\isacharparenleft}auto{\isacharparenright}\isanewline
|
11866
|
131 |
\isamarkupfalse%
|
17056
|
132 |
\isacommand{done}%
|
|
133 |
\endisatagproof
|
|
134 |
{\isafoldproof}%
|
|
135 |
%
|
|
136 |
\isadelimproof
|
|
137 |
%
|
|
138 |
\endisadelimproof
|
|
139 |
\isamarkuptrue%
|
11866
|
140 |
%
|
8749
|
141 |
\begin{isamarkuptext}%
|
|
142 |
\noindent
|
|
143 |
In fact, all proofs in this case study look exactly like this. Hence we do
|
|
144 |
not show them below.
|
|
145 |
|
|
146 |
More interesting is the transformation of If-expressions into a normal form
|
|
147 |
where the first argument of \isa{IF} cannot be another \isa{IF} but
|
|
148 |
must be a constant or variable. Such a normal form can be computed by
|
9792
|
149 |
repeatedly replacing a subterm of the form \isa{IF\ {\isacharparenleft}IF\ b\ x\ y{\isacharparenright}\ z\ u} by
|
|
150 |
\isa{IF\ b\ {\isacharparenleft}IF\ x\ z\ u{\isacharparenright}\ {\isacharparenleft}IF\ y\ z\ u{\isacharparenright}}, which has the same value. The following
|
8749
|
151 |
primitive recursive functions perform this task:%
|
|
152 |
\end{isamarkuptext}%
|
17056
|
153 |
\isamarkupfalse%
|
9673
|
154 |
\isacommand{consts}\ normif\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}ifex\ {\isasymRightarrow}\ ifex\ {\isasymRightarrow}\ ifex\ {\isasymRightarrow}\ ifex{\isachardoublequote}\isanewline
|
11866
|
155 |
\isamarkupfalse%
|
8749
|
156 |
\isacommand{primrec}\isanewline
|
9673
|
157 |
{\isachardoublequote}normif\ {\isacharparenleft}CIF\ b{\isacharparenright}\ \ \ \ t\ e\ {\isacharequal}\ IF\ {\isacharparenleft}CIF\ b{\isacharparenright}\ t\ e{\isachardoublequote}\isanewline
|
|
158 |
{\isachardoublequote}normif\ {\isacharparenleft}VIF\ x{\isacharparenright}\ \ \ \ t\ e\ {\isacharequal}\ IF\ {\isacharparenleft}VIF\ x{\isacharparenright}\ t\ e{\isachardoublequote}\isanewline
|
|
159 |
{\isachardoublequote}normif\ {\isacharparenleft}IF\ b\ t\ e{\isacharparenright}\ u\ f\ {\isacharequal}\ normif\ b\ {\isacharparenleft}normif\ t\ u\ f{\isacharparenright}\ {\isacharparenleft}normif\ e\ u\ f{\isacharparenright}{\isachardoublequote}\isanewline
|
8749
|
160 |
\isanewline
|
11866
|
161 |
\isamarkupfalse%
|
9673
|
162 |
\isacommand{consts}\ norm\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}ifex\ {\isasymRightarrow}\ ifex{\isachardoublequote}\isanewline
|
11866
|
163 |
\isamarkupfalse%
|
8749
|
164 |
\isacommand{primrec}\isanewline
|
9673
|
165 |
{\isachardoublequote}norm\ {\isacharparenleft}CIF\ b{\isacharparenright}\ \ \ \ {\isacharequal}\ CIF\ b{\isachardoublequote}\isanewline
|
|
166 |
{\isachardoublequote}norm\ {\isacharparenleft}VIF\ x{\isacharparenright}\ \ \ \ {\isacharequal}\ VIF\ x{\isachardoublequote}\isanewline
|
17056
|
167 |
{\isachardoublequote}norm\ {\isacharparenleft}IF\ b\ t\ e{\isacharparenright}\ {\isacharequal}\ normif\ b\ {\isacharparenleft}norm\ t{\isacharparenright}\ {\isacharparenleft}norm\ e{\isacharparenright}{\isachardoublequote}\isamarkuptrue%
|
11866
|
168 |
%
|
8749
|
169 |
\begin{isamarkuptext}%
|
|
170 |
\noindent
|
11456
|
171 |
Their interplay is tricky; we leave it to you to develop an
|
8749
|
172 |
intuitive understanding. Fortunately, Isabelle can help us to verify that the
|
|
173 |
transformation preserves the value of the expression:%
|
|
174 |
\end{isamarkuptext}%
|
17056
|
175 |
\isamarkupfalse%
|
|
176 |
\isacommand{theorem}\ {\isachardoublequote}valif\ {\isacharparenleft}norm\ b{\isacharparenright}\ env\ {\isacharequal}\ valif\ b\ env{\isachardoublequote}%
|
|
177 |
\isadelimproof
|
|
178 |
%
|
|
179 |
\endisadelimproof
|
|
180 |
%
|
|
181 |
\isatagproof
|
|
182 |
%
|
|
183 |
\endisatagproof
|
|
184 |
{\isafoldproof}%
|
|
185 |
%
|
|
186 |
\isadelimproof
|
|
187 |
%
|
|
188 |
\endisadelimproof
|
11866
|
189 |
\isamarkuptrue%
|
|
190 |
%
|
8749
|
191 |
\begin{isamarkuptext}%
|
|
192 |
\noindent
|
|
193 |
The proof is canonical, provided we first show the following simplification
|
11456
|
194 |
lemma, which also helps to understand what \isa{normif} does:%
|
8749
|
195 |
\end{isamarkuptext}%
|
17056
|
196 |
\isamarkupfalse%
|
9673
|
197 |
\isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\isanewline
|
17056
|
198 |
\ \ {\isachardoublequote}{\isasymforall}t\ e{\isachardot}\ valif\ {\isacharparenleft}normif\ b\ t\ e{\isacharparenright}\ env\ {\isacharequal}\ valif\ {\isacharparenleft}IF\ b\ t\ e{\isacharparenright}\ env{\isachardoublequote}%
|
|
199 |
\isadelimproof
|
|
200 |
%
|
|
201 |
\endisadelimproof
|
|
202 |
%
|
|
203 |
\isatagproof
|
|
204 |
%
|
|
205 |
\endisatagproof
|
|
206 |
{\isafoldproof}%
|
|
207 |
%
|
|
208 |
\isadelimproof
|
|
209 |
%
|
|
210 |
\endisadelimproof
|
|
211 |
%
|
|
212 |
\isadelimproof
|
|
213 |
%
|
|
214 |
\endisadelimproof
|
|
215 |
%
|
|
216 |
\isatagproof
|
|
217 |
%
|
|
218 |
\endisatagproof
|
|
219 |
{\isafoldproof}%
|
|
220 |
%
|
|
221 |
\isadelimproof
|
|
222 |
%
|
|
223 |
\endisadelimproof
|
|
224 |
\isamarkuptrue%
|
11866
|
225 |
%
|
8749
|
226 |
\begin{isamarkuptext}%
|
|
227 |
\noindent
|
|
228 |
Note that the lemma does not have a name, but is implicitly used in the proof
|
9792
|
229 |
of the theorem shown above because of the \isa{{\isacharbrackleft}simp{\isacharbrackright}} attribute.
|
8749
|
230 |
|
|
231 |
But how can we be sure that \isa{norm} really produces a normal form in
|
11456
|
232 |
the above sense? We define a function that tests If-expressions for normality:%
|
8749
|
233 |
\end{isamarkuptext}%
|
17056
|
234 |
\isamarkupfalse%
|
9673
|
235 |
\isacommand{consts}\ normal\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}ifex\ {\isasymRightarrow}\ bool{\isachardoublequote}\isanewline
|
11866
|
236 |
\isamarkupfalse%
|
8749
|
237 |
\isacommand{primrec}\isanewline
|
9673
|
238 |
{\isachardoublequote}normal{\isacharparenleft}CIF\ b{\isacharparenright}\ {\isacharequal}\ True{\isachardoublequote}\isanewline
|
|
239 |
{\isachardoublequote}normal{\isacharparenleft}VIF\ x{\isacharparenright}\ {\isacharequal}\ True{\isachardoublequote}\isanewline
|
|
240 |
{\isachardoublequote}normal{\isacharparenleft}IF\ b\ t\ e{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}normal\ t\ {\isasymand}\ normal\ e\ {\isasymand}\isanewline
|
17056
|
241 |
\ \ \ \ \ {\isacharparenleft}case\ b\ of\ CIF\ b\ {\isasymRightarrow}\ True\ {\isacharbar}\ VIF\ x\ {\isasymRightarrow}\ True\ {\isacharbar}\ IF\ x\ y\ z\ {\isasymRightarrow}\ False{\isacharparenright}{\isacharparenright}{\isachardoublequote}\isamarkuptrue%
|
11866
|
242 |
%
|
8749
|
243 |
\begin{isamarkuptext}%
|
|
244 |
\noindent
|
11456
|
245 |
Now we prove \isa{normal\ {\isacharparenleft}norm\ b{\isacharparenright}}. Of course, this requires a lemma about
|
8749
|
246 |
normality of \isa{normif}:%
|
|
247 |
\end{isamarkuptext}%
|
17056
|
248 |
\isamarkupfalse%
|
|
249 |
\isacommand{lemma}\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isasymforall}t\ e{\isachardot}\ normal{\isacharparenleft}normif\ b\ t\ e{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}normal\ t\ {\isasymand}\ normal\ e{\isacharparenright}{\isachardoublequote}%
|
|
250 |
\isadelimproof
|
|
251 |
%
|
|
252 |
\endisadelimproof
|
|
253 |
%
|
|
254 |
\isatagproof
|
|
255 |
%
|
|
256 |
\endisatagproof
|
|
257 |
{\isafoldproof}%
|
|
258 |
%
|
|
259 |
\isadelimproof
|
|
260 |
%
|
|
261 |
\endisadelimproof
|
|
262 |
%
|
|
263 |
\isadelimproof
|
|
264 |
%
|
|
265 |
\endisadelimproof
|
|
266 |
%
|
|
267 |
\isatagproof
|
|
268 |
%
|
|
269 |
\endisatagproof
|
|
270 |
{\isafoldproof}%
|
|
271 |
%
|
|
272 |
\isadelimproof
|
|
273 |
%
|
|
274 |
\endisadelimproof
|
11866
|
275 |
\isamarkuptrue%
|
|
276 |
%
|
9933
|
277 |
\begin{isamarkuptext}%
|
|
278 |
\medskip
|
10795
|
279 |
How do we come up with the required lemmas? Try to prove the main theorems
|
|
280 |
without them and study carefully what \isa{auto} leaves unproved. This
|
|
281 |
can provide the clue. The necessity of universal quantification
|
9933
|
282 |
(\isa{{\isasymforall}t\ e}) in the two lemmas is explained in
|
|
283 |
\S\ref{sec:InductionHeuristics}
|
|
284 |
|
|
285 |
\begin{exercise}
|
|
286 |
We strengthen the definition of a \isa{normal} If-expression as follows:
|
|
287 |
the first argument of all \isa{IF}s must be a variable. Adapt the above
|
|
288 |
development to this changed requirement. (Hint: you may need to formulate
|
|
289 |
some of the goals as implications (\isa{{\isasymlongrightarrow}}) rather than
|
|
290 |
equalities (\isa{{\isacharequal}}).)
|
11456
|
291 |
\end{exercise}
|
|
292 |
\index{boolean expressions example|)}%
|
9933
|
293 |
\end{isamarkuptext}%
|
17056
|
294 |
%
|
|
295 |
\isadelimproof
|
|
296 |
%
|
|
297 |
\endisadelimproof
|
|
298 |
%
|
|
299 |
\isatagproof
|
|
300 |
%
|
|
301 |
\endisatagproof
|
|
302 |
{\isafoldproof}%
|
|
303 |
%
|
|
304 |
\isadelimproof
|
|
305 |
%
|
|
306 |
\endisadelimproof
|
|
307 |
%
|
|
308 |
\isadelimproof
|
|
309 |
%
|
|
310 |
\endisadelimproof
|
|
311 |
%
|
|
312 |
\isatagproof
|
|
313 |
%
|
|
314 |
\endisatagproof
|
|
315 |
{\isafoldproof}%
|
|
316 |
%
|
|
317 |
\isadelimproof
|
|
318 |
%
|
|
319 |
\endisadelimproof
|
|
320 |
%
|
|
321 |
\isadelimproof
|
|
322 |
%
|
|
323 |
\endisadelimproof
|
|
324 |
%
|
|
325 |
\isatagproof
|
|
326 |
%
|
|
327 |
\endisatagproof
|
|
328 |
{\isafoldproof}%
|
|
329 |
%
|
|
330 |
\isadelimproof
|
|
331 |
%
|
|
332 |
\endisadelimproof
|
|
333 |
%
|
|
334 |
\isadelimproof
|
|
335 |
%
|
|
336 |
\endisadelimproof
|
|
337 |
%
|
|
338 |
\isatagproof
|
|
339 |
%
|
|
340 |
\endisatagproof
|
|
341 |
{\isafoldproof}%
|
|
342 |
%
|
|
343 |
\isadelimproof
|
|
344 |
%
|
|
345 |
\endisadelimproof
|
|
346 |
%
|
|
347 |
\isadelimtheory
|
|
348 |
%
|
|
349 |
\endisadelimtheory
|
|
350 |
%
|
|
351 |
\isatagtheory
|
|
352 |
%
|
|
353 |
\endisatagtheory
|
|
354 |
{\isafoldtheory}%
|
|
355 |
%
|
|
356 |
\isadelimtheory
|
|
357 |
%
|
|
358 |
\endisadelimtheory
|
9933
|
359 |
\end{isabellebody}%
|
9145
|
360 |
%%% Local Variables:
|
|
361 |
%%% mode: latex
|
|
362 |
%%% TeX-master: "root"
|
|
363 |
%%% End:
|