191 In which case you should use \texttt{mode=IfThenNoBox} instead of |
191 In which case you should use \texttt{mode=IfThenNoBox} instead of |
192 \texttt{mode=IfThen}: |
192 \texttt{mode=IfThen}: |
193 \begin{theorem} |
193 \begin{theorem} |
194 @{prop[mode=IfThenNoBox] "longpremise \<Longrightarrow> longerpremise \<Longrightarrow> P(f(f(f(f(f(f(f(f(f(x)))))))))) \<Longrightarrow> longestpremise \<Longrightarrow> conclusion"} |
194 @{prop[mode=IfThenNoBox] "longpremise \<Longrightarrow> longerpremise \<Longrightarrow> P(f(f(f(f(f(f(f(f(f(x)))))))))) \<Longrightarrow> longestpremise \<Longrightarrow> conclusion"} |
195 \end{theorem} |
195 \end{theorem} |
196 *} |
|
197 |
|
198 subsection {*Definitions and Equations*} |
|
199 |
|
200 text {* |
|
201 The \verb!thm! antiquotation works nicely for proper theorems, but |
|
202 sets of equations as used in definitions are more difficult to |
|
203 typeset nicely: for some reason people tend to prefer aligned |
|
204 @{text "="} signs. |
|
205 |
|
206 Isabelle2005 has a nice mechanism for this, namely the two |
|
207 antiquotations \verb!@!\verb!{lhs thm}! and \verb!@!\verb!{rhs thm}!. |
|
208 |
|
209 \begin{center} |
|
210 \begin{tabular}{l@ {~~@{text "="}~~}l} |
|
211 @{lhs foldl_Nil} & @{rhs foldl_Nil}\\ |
|
212 @{lhs foldl_Cons} & @{rhs foldl_Cons} |
|
213 \end{tabular} |
|
214 \end{center} |
|
215 |
|
216 \noindent |
|
217 is produced by the following code: |
|
218 |
|
219 \begin{quote} |
|
220 \verb!\begin{center}!\\ |
|
221 \verb!\begin{tabular}{l@ {~~!\verb!@!\verb!{text "="}~~}l}!\\ |
|
222 \verb!@!\verb!{lhs foldl_Nil} & @!\verb!{rhs foldl_Nil}!\\ |
|
223 \verb!@!\verb!{lhs foldl_Cons} & @!\verb!{rhs foldl_Cons}!\\ |
|
224 \verb!\end{tabular}!\\ |
|
225 \verb!\end{center}! |
|
226 \end{quote} |
|
227 |
|
228 \noindent |
|
229 Note the space between \verb!@! and \verb!{! in the tabular argument. |
|
230 It prevents Isabelle from interpreting \verb!@ {~~...~~}! |
|
231 as antiquotation. \verb!@!\verb!{lhs thm}! and \verb!@!\verb!{rhs thm}! |
|
232 try to be smart about the interpretation of the theorem they |
|
233 print, they work just as well for meta equality @{text "\<equiv>"} and other |
|
234 binary operators like @{text "<"}. |
|
235 *} |
196 *} |
236 |
197 |
237 subsection "Patterns" |
198 subsection "Patterns" |
238 |
199 |
239 text {* |
200 text {* |
309 \verb!*!\verb!}! |
270 \verb!*!\verb!}! |
310 \end{quote} |
271 \end{quote} |
311 |
272 |
312 *} |
273 *} |
313 |
274 |
|
275 subsection "Styles" |
|
276 |
|
277 text {* |
|
278 The \verb!thm! antiquotation works nicely for proper theorems, but |
|
279 sets of equations as used in definitions are more difficult to |
|
280 typeset nicely: for some reason people tend to prefer aligned |
|
281 @{text "="} signs. |
|
282 |
|
283 To deal with such cases where it is desirable to dive into the structure |
|
284 of terms and theorems, Isabelle offers two antiquotations featuring |
|
285 ``styles'': |
|
286 |
|
287 \begin{quote} |
|
288 \verb!@!\verb!{thm_style stylename thm}!\\ |
|
289 \verb!@!\verb!{term_style stylename term}! |
|
290 \end{quote} |
|
291 |
|
292 A ``style'' is a transformation of terms; there are three predefined |
|
293 styles, named \verb!lhs!, \verb!rhs! and \verb!concl!, which obvious |
|
294 meanings, e.~g.~the output |
|
295 |
|
296 \begin{center} |
|
297 \begin{tabular}{l@ {~~@{text "="}~~}l} |
|
298 @{thm_style lhs foldl_Nil} & @{thm_style rhs foldl_Nil}\\ |
|
299 @{thm_style lhs foldl_Cons} & @{thm_style rhs foldl_Cons} |
|
300 \end{tabular} |
|
301 \end{center} |
|
302 |
|
303 \noindent |
|
304 is produced by the following code: |
|
305 |
|
306 \begin{quote} |
|
307 \verb!\begin{center}!\\ |
|
308 \verb!\begin{tabular}{l@ {~~!\verb!@!\verb!{text "="}~~}l}!\\ |
|
309 \verb!@!\verb!{thm_style lhs foldl_Nil} & @!\verb!{thm_style rhs foldl_Nil}!\\ |
|
310 \verb!@!\verb!{thm_style lhs foldl_Cons} & @!\verb!{thm_style rhs foldl_Cons}!\\ |
|
311 \verb!\end{tabular}!\\ |
|
312 \verb!\end{center}! |
|
313 \end{quote} |
|
314 |
|
315 \noindent |
|
316 Note the space between \verb!@! and \verb!{! in the tabular argument. |
|
317 It prevents Isabelle from interpreting \verb!@ {~~...~~}! |
|
318 as antiquotation. Both styles \verb!lhs! and \verb!rhs! |
|
319 try to be smart about the interpretation of the theorem they transform |
|
320 they work just as well for meta equality @{text "\<equiv>"} and other |
|
321 binary operators like @{text "<"}. |
|
322 |
|
323 Likewise \verb!conclusion! may be used as style to show just the conclusion |
|
324 of a formula: |
|
325 |
|
326 \begin{center} |
|
327 @{thm_style conclusion hd_Cons_tl} |
|
328 \end{center} |
|
329 |
|
330 \noindent |
|
331 is produced by |
|
332 |
|
333 \begin{quote} |
|
334 \verb!\begin{center}!\\ |
|
335 \verb!@!\verb!{thm_style conclusion hd_Cons_tl}!\\ |
|
336 \verb!\end{center}! |
|
337 \end{quote} |
|
338 |
|
339 If you aren't afraid about ML, you may also define your own styles; |
|
340 a style is simply implemented by a ML function \verb!Term.term -> Term.term!. |
|
341 Have a look at the following example (which indeed shows just the way the |
|
342 \verb!lhs! style is implemented): |
|
343 |
|
344 \begin{quote} |
|
345 \verb!setup {!\verb!*!\\ |
|
346 \verb!!\\ |
|
347 \verb!let!\\ |
|
348 \verb! fun my_lhs (Const ("==", _) $ t $ _) = t!\\ |
|
349 \verb! | my_lhs (Const ("Trueprop", _) $ t) = my_lhs t!\\ |
|
350 \verb! | my_lhs (Const ("==>", _) $ _ $ t) = my_lhs t!\\ |
|
351 \verb! | my_lhs (_ $ t $ _) = t!\\ |
|
352 \verb! | my_lhs _ = error ("Binary operator expected")!\\ |
|
353 \verb! in [Style.put_style "new_lhs" my_lhs]!\\ |
|
354 \verb!end;!\\ |
|
355 \verb!!\\ |
|
356 \verb!*!\verb!}!\\ |
|
357 \end{quote} |
|
358 |
|
359 Like in this example, it is recommended to put the definition of the style |
|
360 function into a \verb!let! expression, in order not to pollute the |
|
361 ML global namespace. The mapping from identifier name to the style function |
|
362 is done by the \verb!Style.put_style! expression which expects the desired |
|
363 style name and the style function as arguments. After this \verb!setup!, |
|
364 there will be a new style available named \verb!new_lhs!, then allowing |
|
365 antiquoations like \verb!@!\verb!{term_style new_lhs rev_map}! |
|
366 yielding \verb!rev (map f xs)!. |
|
367 |
|
368 The example above may be used as as a ``copy-and-paste'' pattern to write |
|
369 your own styles; for a description of the constructs used, please refer |
|
370 to the Isabelle reference manual. |
|
371 |
|
372 *} |
|
373 |
314 (*<*) |
374 (*<*) |
315 end |
375 end |
316 (*>*) |
376 (*>*) |