author | nipkow |
Fri, 31 Aug 2007 15:56:19 +0200 | |
changeset 24497 | 7840f760a744 |
parent 24496 | 65f3b37f80b7 |
child 27093 | 66d6da816be7 |
permissions | -rw-r--r-- |
15337 | 1 |
(*<*) |
2 |
theory Sugar |
|
15366 | 3 |
imports LaTeXsugar OptionalSugar |
15337 | 4 |
begin |
5 |
(*>*) |
|
6 |
||
7 |
section "Introduction" |
|
8 |
||
15385 | 9 |
text{* This document is for those Isabelle users who have mastered |
15337 | 10 |
the art of mixing \LaTeX\ text and Isabelle theories and never want to |
11 |
typeset a theorem by hand anymore because they have experienced the |
|
12 |
bliss of writing \verb!@!\verb!{thm[display]setsum_cartesian_product[no_vars]}! |
|
13 |
and seeing Isabelle typeset it for them: |
|
14 |
@{thm[display,eta_contract=false] setsum_cartesian_product[no_vars]} |
|
15342 | 15 |
No typos, no omissions, no sweat. |
16 |
If you have not experienced that joy, read Chapter 4, \emph{Presenting |
|
17 |
Theories}, \cite{LNCS2283} first. |
|
15337 | 18 |
|
19 |
If you have mastered the art of Isabelle's \emph{antiquotations}, |
|
20 |
i.e.\ things like the above \verb!@!\verb!{thm...}!, beware: in your vanity |
|
21 |
you may be tempted to think that all readers of the stunning ps or pdf |
|
22 |
documents you can now produce at the drop of a hat will be struck with |
|
23 |
awe at the beauty unfolding in front of their eyes. Until one day you |
|
24 |
come across that very critical of readers known as the ``common referee''. |
|
25 |
He has the nasty habit of refusing to understand unfamiliar notation |
|
26 |
like Isabelle's infamous @{text"\<lbrakk> \<rbrakk> \<Longrightarrow>"} no matter how many times you |
|
27 |
explain it in your paper. Even worse, he thinks that using @{text"\<lbrakk> |
|
28 |
\<rbrakk>"} for anything other than denotational semantics is a cardinal sin |
|
15342 | 29 |
that must be punished by instant rejection. |
15337 | 30 |
|
31 |
||
32 |
This document shows you how to make Isabelle and \LaTeX\ cooperate to |
|
33 |
produce ordinary looking mathematics that hides the fact that it was |
|
15471 | 34 |
typeset by a machine. You merely need to load the right files: |
35 |
\begin{itemize} |
|
36 |
\item Import theory \texttt{LaTeXsugar} in the header of your own |
|
37 |
theory. You may also want bits of \texttt{OptionalSugar}, which you can |
|
38 |
copy selectively into your own theory or import as a whole. Both |
|
39 |
theories live in \texttt{HOL/Library} and are found automatically. |
|
15378 | 40 |
|
15471 | 41 |
\item Should you need additional \LaTeX\ packages (the text will tell |
42 |
you so), you include them at the beginning of your \LaTeX\ document, |
|
16153 | 43 |
typically in \texttt{root.tex}. For a start, you should |
44 |
\verb!\usepackage{amssymb}! --- otherwise typesetting |
|
45 |
@{prop[source]"\<not>(\<exists>x. P x)"} will fail because the AMS symbol |
|
46 |
@{text"\<nexists>"} is missing. |
|
15471 | 47 |
\end{itemize} |
15342 | 48 |
*} |
49 |
||
50 |
section{* HOL syntax*} |
|
51 |
||
52 |
subsection{* Logic *} |
|
53 |
||
16153 | 54 |
text{* |
55 |
The formula @{prop[source]"\<not>(\<exists>x. P x)"} is typeset as @{prop"~(EX x. P x)"}. |
|
56 |
||
57 |
The predefined constructs @{text"if"}, @{text"let"} and |
|
15342 | 58 |
@{text"case"} are set in sans serif font to distinguish them from |
59 |
other functions. This improves readability: |
|
60 |
\begin{itemize} |
|
61 |
\item @{term"if b then e\<^isub>1 else e\<^isub>2"} instead of @{text"if b then e\<^isub>1 else e\<^isub>2"}. |
|
62 |
\item @{term"let x = e\<^isub>1 in e\<^isub>2"} instead of @{text"let x = e\<^isub>1 in e\<^isub>2"}. |
|
63 |
\item @{term"case x of True \<Rightarrow> e\<^isub>1 | False \<Rightarrow> e\<^isub>2"} instead of\\ |
|
64 |
@{text"case x of True \<Rightarrow> e\<^isub>1 | False \<Rightarrow> e\<^isub>2"}. |
|
65 |
\end{itemize} |
|
66 |
*} |
|
67 |
||
68 |
subsection{* Sets *} |
|
15337 | 69 |
|
15342 | 70 |
text{* Although set syntax in HOL is already close to |
71 |
standard, we provide a few further improvements: |
|
72 |
\begin{itemize} |
|
73 |
\item @{term"{x. P}"} instead of @{text"{x. P}"}. |
|
74 |
\item @{term"{}"} instead of @{text"{}"}. |
|
75 |
\item @{term"insert a (insert b (insert c M))"} instead of @{text"insert a (insert b (insert c M))"}. |
|
76 |
\end{itemize} |
|
77 |
*} |
|
78 |
||
79 |
subsection{* Lists *} |
|
80 |
||
81 |
text{* If lists are used heavily, the following notations increase readability: |
|
82 |
\begin{itemize} |
|
83 |
\item @{term"x # xs"} instead of @{text"x # xs"}. |
|
84 |
Exceptionally, @{term"x # xs"} is also input syntax. |
|
85 |
If you prefer more space around the $\cdot$ you have to redefine |
|
86 |
\verb!\isasymcdot! in \LaTeX: |
|
87 |
\verb!\renewcommand{\isasymcdot}{\isamath{\,\cdot\,}}! |
|
88 |
||
89 |
\item @{term"length xs"} instead of @{text"length xs"}. |
|
15385 | 90 |
\item @{term"nth xs n"} instead of @{text"nth xs n"}, |
15342 | 91 |
the $n$th element of @{text xs}. |
92 |
||
22834 | 93 |
\item Human readers are good at converting automatically from lists to |
94 |
sets. Hence \texttt{OptionalSugar} contains syntax for supressing the |
|
95 |
conversion function @{const set}: for example, @{prop[source]"x \<in> set xs"} |
|
96 |
becomes @{prop"x \<in> set xs"}. |
|
97 |
||
15366 | 98 |
\item The @{text"@"} operation associates implicitly to the right, |
99 |
which leads to unpleasant line breaks if the term is too long for one |
|
100 |
line. To avoid this, \texttt{OptionalSugar} contains syntax to group |
|
101 |
@{text"@"}-terms to the left before printing, which leads to better |
|
102 |
line breaking behaviour: |
|
15673 | 103 |
@{term[display]"term\<^isub>0 @ term\<^isub>1 @ term\<^isub>2 @ term\<^isub>3 @ term\<^isub>4 @ term\<^isub>5 @ term\<^isub>6 @ term\<^isub>7 @ term\<^isub>8 @ term\<^isub>9 @ term\<^isub>1\<^isub>0"} |
15366 | 104 |
|
15342 | 105 |
\end{itemize} |
15337 | 106 |
*} |
107 |
||
108 |
section "Printing theorems" |
|
109 |
||
15689 | 110 |
subsection "Question marks" |
111 |
||
112 |
text{* If you print anything, especially theorems, containing |
|
113 |
schematic variables they are prefixed with a question mark: |
|
114 |
\verb!@!\verb!{thm conjI}! results in @{thm conjI}. Most of the time |
|
115 |
you would rather not see the question marks. There is an attribute |
|
116 |
\verb!no_vars! that you can attach to the theorem that turns its |
|
117 |
schematic into ordinary free variables: \verb!@!\verb!{thm conjI[no_vars]}! |
|
118 |
results in @{thm conjI[no_vars]}. |
|
119 |
||
120 |
This \verb!no_vars! business can become a bit tedious. |
|
121 |
If you would rather never see question marks, simply put |
|
122 |
\begin{verbatim} |
|
15983 | 123 |
reset show_question_marks; |
15689 | 124 |
\end{verbatim} |
125 |
at the beginning of your file \texttt{ROOT.ML}. |
|
126 |
The rest of this document is produced with this flag reset. |
|
16075 | 127 |
|
128 |
Hint: Resetting \verb!show_question_marks! only supresses question |
|
129 |
marks; variables that end in digits, e.g. @{text"x1"}, are still |
|
130 |
printed with a trailing @{text".0"}, e.g. @{text"x1.0"}, their |
|
131 |
internal index. This can be avoided by turning the last digit into a |
|
132 |
subscript: write \verb!x\<^isub>1! and obtain the much nicer @{text"x\<^isub>1"}. *} |
|
15689 | 133 |
|
15983 | 134 |
(*<*)ML"reset show_question_marks"(*>*) |
15689 | 135 |
|
24496 | 136 |
subsection {*Qualified names*} |
137 |
||
138 |
text{* If there are multiple declarations of the same name, Isabelle prints |
|
139 |
the qualified name, for example @{text "T.length"}, where @{text T} is the |
|
140 |
theory it is defined in, to distinguish it from the predefined @{const[source] |
|
141 |
"List.length"}. In case there is no danger of confusion, you can insist on |
|
142 |
short names (no qualifiers) by setting \verb!short_names!, typically |
|
143 |
in \texttt{ROOT.ML}: |
|
144 |
\begin{verbatim} |
|
145 |
set short_names; |
|
146 |
\end{verbatim} |
|
147 |
*} |
|
148 |
||
17127 | 149 |
subsection {*Variable names\label{sec:varnames}*} |
16395 | 150 |
|
151 |
text{* It sometimes happens that you want to change the name of a |
|
152 |
variable in a theorem before printing it. This can easily be achieved |
|
153 |
with the help of Isabelle's instantiation attribute \texttt{where}: |
|
154 |
@{thm conjI[where P = \<phi> and Q = \<psi>]} is the result of |
|
155 |
\begin{quote} |
|
156 |
\verb!@!\verb!{thm conjI[where P = \<phi> and Q = \<psi>]}! |
|
157 |
\end{quote} |
|
158 |
To support the ``\_''-notation for irrelevant variables |
|
159 |
the constant \texttt{DUMMY} has been introduced: |
|
160 |
@{thm fst_conv[where b = DUMMY]} is produced by |
|
161 |
\begin{quote} |
|
162 |
\verb!@!\verb!{thm fst_conv[where b = DUMMY]}! |
|
163 |
\end{quote} |
|
164 |
*} |
|
165 |
||
15337 | 166 |
subsection "Inference rules" |
167 |
||
15342 | 168 |
text{* To print theorems as inference rules you need to include Didier |
169 |
R\'emy's \texttt{mathpartir} package~\cite{mathpartir} |
|
170 |
for typesetting inference rules in your \LaTeX\ file. |
|
15337 | 171 |
|
15689 | 172 |
Writing \verb!@!\verb!{thm[mode=Rule] conjI}! produces |
173 |
@{thm[mode=Rule] conjI}, even in the middle of a sentence. |
|
15342 | 174 |
If you prefer your inference rule on a separate line, maybe with a name, |
175 |
\begin{center} |
|
15689 | 176 |
@{thm[mode=Rule] conjI} {\sc conjI} |
15342 | 177 |
\end{center} |
178 |
is produced by |
|
15337 | 179 |
\begin{quote} |
180 |
\verb!\begin{center}!\\ |
|
15689 | 181 |
\verb!@!\verb!{thm[mode=Rule] conjI} {\sc conjI}!\\ |
15337 | 182 |
\verb!\end{center}! |
183 |
\end{quote} |
|
24497 | 184 |
It is not recommended to use the standard \texttt{display} option |
15342 | 185 |
together with \texttt{Rule} because centering does not work and because |
186 |
the line breaking mechanisms of \texttt{display} and \texttt{mathpartir} can |
|
187 |
clash. |
|
188 |
||
15337 | 189 |
Of course you can display multiple rules in this fashion: |
190 |
\begin{quote} |
|
24497 | 191 |
\verb!\begin{center}!\\ |
15689 | 192 |
\verb!@!\verb!{thm[mode=Rule] conjI} {\sc conjI} \\[1ex]!\\ |
193 |
\verb!@!\verb!{thm[mode=Rule] conjE} {\sc disjI$_1$} \qquad!\\ |
|
194 |
\verb!@!\verb!{thm[mode=Rule] disjE} {\sc disjI$_2$}!\\ |
|
15337 | 195 |
\verb!\end{center}! |
196 |
\end{quote} |
|
197 |
yields |
|
24497 | 198 |
\begin{center}\small |
15689 | 199 |
@{thm[mode=Rule] conjI} {\sc conjI} \\[1ex] |
200 |
@{thm[mode=Rule] disjI1} {\sc disjI$_1$} \qquad |
|
201 |
@{thm[mode=Rule] disjI2} {\sc disjI$_2$} |
|
15337 | 202 |
\end{center} |
203 |
||
15342 | 204 |
The \texttt{mathpartir} package copes well if there are too many |
205 |
premises for one line: |
|
206 |
\begin{center} |
|
207 |
@{prop[mode=Rule] "\<lbrakk> A \<longrightarrow> B; B \<longrightarrow> C; C \<longrightarrow> D; D \<longrightarrow> E; E \<longrightarrow> F; F \<longrightarrow> G; |
|
208 |
G \<longrightarrow> H; H \<longrightarrow> I; I \<longrightarrow> J; J \<longrightarrow> K \<rbrakk> \<Longrightarrow> A \<longrightarrow> K"} |
|
209 |
\end{center} |
|
210 |
||
15471 | 211 |
Limitations: 1. Premises and conclusion must each not be longer than |
212 |
the line. 2. Premises that are @{text"\<Longrightarrow>"}-implications are again |
|
213 |
displayed with a horizontal line, which looks at least unusual. |
|
214 |
||
22329 | 215 |
|
216 |
In case you print theorems without premises no rule will be printed by the |
|
217 |
\texttt{Rule} print mode. However, you can use \texttt{Axiom} instead: |
|
218 |
\begin{quote} |
|
24497 | 219 |
\verb!\begin{center}!\\ |
22329 | 220 |
\verb!@!\verb!{thm[mode=Axiom] refl} {\sc refl}! \\ |
221 |
\verb!\end{center}! |
|
222 |
\end{quote} |
|
223 |
yields |
|
24497 | 224 |
\begin{center} |
22329 | 225 |
@{thm[mode=Axiom] refl} {\sc refl} |
226 |
\end{center} |
|
15337 | 227 |
*} |
15342 | 228 |
|
24497 | 229 |
subsection "Displays and font sizes" |
230 |
||
231 |
text{* When displaying theorems with the \texttt{display} option, e.g. |
|
232 |
\verb!@!\verb!{thm[display] refl}! @{thm[display] refl} the theorem is |
|
233 |
set in small font. It uses the \LaTeX-macro \verb!\isastyle!, |
|
234 |
which is also the style that regular theory text is set in, e.g. *} |
|
235 |
||
236 |
lemma "t = t" |
|
237 |
(*<*)oops(*>*) |
|
238 |
||
239 |
text{* \noindent Otherwise \verb!\isastyleminor! is used, |
|
240 |
which does not modify the font size (assuming you stick to the default |
|
241 |
\verb!\isabellestyle{it}! in \texttt{root.tex}). If you prefer |
|
242 |
normal font size throughout your text, include |
|
243 |
\begin{quote} |
|
244 |
\verb!\renewcommand{\isastyle}{\isastyleminor}! |
|
245 |
\end{quote} |
|
246 |
in \texttt{root.tex}. On the other hand, if you like the small font, |
|
247 |
just put \verb!\isastyle! in front of the text in question, |
|
248 |
e.g.\ at the start of one of the center-environments above. |
|
249 |
||
250 |
The advantage of the display option is that you can display a whole |
|
251 |
list of theorems in one go. For example, |
|
252 |
\verb!@!\verb!{thm[display] foldl.simps}! |
|
253 |
generates @{thm[display] foldl.simps} |
|
254 |
*} |
|
255 |
||
256 |
subsection "If-then" |
|
15342 | 257 |
|
258 |
text{* If you prefer a fake ``natural language'' style you can produce |
|
259 |
the body of |
|
260 |
\newtheorem{theorem}{Theorem} |
|
261 |
\begin{theorem} |
|
15689 | 262 |
@{thm[mode=IfThen] le_trans} |
15342 | 263 |
\end{theorem} |
264 |
by typing |
|
265 |
\begin{quote} |
|
15689 | 266 |
\verb!@!\verb!{thm[mode=IfThen] le_trans}! |
15342 | 267 |
\end{quote} |
268 |
||
269 |
In order to prevent odd line breaks, the premises are put into boxes. |
|
270 |
At times this is too drastic: |
|
271 |
\begin{theorem} |
|
272 |
@{prop[mode=IfThen] "longpremise \<Longrightarrow> longerpremise \<Longrightarrow> P(f(f(f(f(f(f(f(f(f(x)))))))))) \<Longrightarrow> longestpremise \<Longrightarrow> conclusion"} |
|
273 |
\end{theorem} |
|
16153 | 274 |
In which case you should use \texttt{IfThenNoBox} instead of |
275 |
\texttt{IfThen}: |
|
15342 | 276 |
\begin{theorem} |
277 |
@{prop[mode=IfThenNoBox] "longpremise \<Longrightarrow> longerpremise \<Longrightarrow> P(f(f(f(f(f(f(f(f(f(x)))))))))) \<Longrightarrow> longestpremise \<Longrightarrow> conclusion"} |
|
278 |
\end{theorem} |
|
15366 | 279 |
*} |
15342 | 280 |
|
16166 | 281 |
subsection{* Doing it yourself\label{sec:yourself}*} |
16153 | 282 |
|
283 |
text{* If for some reason you want or need to present theorems your |
|
284 |
own way, you can extract the premises and the conclusion explicitly |
|
285 |
and combine them as you like: |
|
286 |
\begin{itemize} |
|
16167 | 287 |
\item \verb!@!\verb!{thm_style prem1! $thm$\verb!}! |
288 |
prints premise 1 of $thm$ (and similarly up to \texttt{prem9}). |
|
16165 | 289 |
\item \verb!@!\verb!{thm_style concl! $thm$\verb!}! |
16153 | 290 |
prints the conclusion of $thm$. |
291 |
\end{itemize} |
|
16167 | 292 |
For example, ``from @{thm_style prem2 conjI} and |
293 |
@{thm_style prem1 conjI} we conclude @{thm_style concl conjI}'' |
|
16153 | 294 |
is produced by |
295 |
\begin{quote} |
|
16175 | 296 |
\verb!from !\verb!@!\verb!{thm_style prem2 conjI}! \verb!and !\verb!@!\verb!{thm_style prem1 conjI}!\\ |
16165 | 297 |
\verb!we conclude !\verb!@!\verb!{thm_style concl conjI}! |
16153 | 298 |
\end{quote} |
299 |
Thus you can rearrange or hide premises and typeset the theorem as you like. |
|
300 |
The \verb!thm_style! antiquotation is a general mechanism explained |
|
301 |
in \S\ref{sec:styles}. |
|
302 |
*} |
|
303 |
||
15366 | 304 |
subsection "Patterns" |
305 |
||
306 |
text {* |
|
307 |
||
17127 | 308 |
In \S\ref{sec:varnames} we shows how to create patterns containing |
309 |
``@{term DUMMY}''. |
|
15366 | 310 |
You can drive this game even further and extend the syntax of let |
311 |
bindings such that certain functions like @{term fst}, @{term hd}, |
|
15368 | 312 |
etc.\ are printed as patterns. \texttt{OptionalSugar} provides the |
313 |
following: |
|
15366 | 314 |
|
315 |
\begin{center} |
|
316 |
\begin{tabular}{l@ {~~produced by~~}l} |
|
317 |
@{term "let x = fst p in t"} & \verb!@!\verb!{term "let x = fst p in t"}!\\ |
|
318 |
@{term "let x = snd p in t"} & \verb!@!\verb!{term "let x = snd p in t"}!\\ |
|
319 |
@{term "let x = hd xs in t"} & \verb!@!\verb!{term "let x = hd xs in t"}!\\ |
|
320 |
@{term "let x = tl xs in t"} & \verb!@!\verb!{term "let x = tl xs in t"}!\\ |
|
321 |
@{term "let x = the y in t"} & \verb!@!\verb!{term "let x = the y in t"}!\\ |
|
322 |
\end{tabular} |
|
323 |
\end{center} |
|
324 |
*} |
|
325 |
||
16155 | 326 |
section "Proofs" |
15366 | 327 |
|
24497 | 328 |
text {* Full proofs, even if written in beautiful Isar style, are |
329 |
likely to be too long and detailed to be included in conference |
|
330 |
papers, but some key lemmas might be of interest. |
|
331 |
It is usually easiest to put them in figures like the one in Fig.\ |
|
332 |
\ref{fig:proof}. This was achieved with the \isakeyword{text\_raw} command: |
|
15366 | 333 |
*} |
334 |
text_raw {* |
|
335 |
\begin{figure} |
|
336 |
\begin{center}\begin{minipage}{0.6\textwidth} |
|
24497 | 337 |
\isastyleminor\isamarkuptrue |
15366 | 338 |
*} |
339 |
lemma True |
|
340 |
proof - |
|
341 |
-- "pretty trivial" |
|
342 |
show True by force |
|
343 |
qed |
|
15428 | 344 |
text_raw {* |
15366 | 345 |
\end{minipage}\end{center} |
346 |
\caption{Example proof in a figure.}\label{fig:proof} |
|
347 |
\end{figure} |
|
348 |
*} |
|
349 |
text {* |
|
350 |
||
351 |
\begin{quote} |
|
352 |
\small |
|
353 |
\verb!text_raw {!\verb!*!\\ |
|
354 |
\verb! \begin{figure}!\\ |
|
355 |
\verb! \begin{center}\begin{minipage}{0.6\textwidth}!\\ |
|
24497 | 356 |
\verb! \isastyleminor\isamarkuptrue!\\ |
15366 | 357 |
\verb!*!\verb!}!\\ |
358 |
\verb!lemma True!\\ |
|
359 |
\verb!proof -!\\ |
|
360 |
\verb! -- "pretty trivial"!\\ |
|
361 |
\verb! show True by force!\\ |
|
362 |
\verb!qed!\\ |
|
363 |
\verb!text_raw {!\verb!*!\\ |
|
364 |
\verb! \end{minipage}\end{center}!\\ |
|
365 |
\verb! \caption{Example proof in a figure.}\label{fig:proof}!\\ |
|
366 |
\verb! \end{figure}!\\ |
|
367 |
\verb!*!\verb!}! |
|
368 |
\end{quote} |
|
24497 | 369 |
|
370 |
Other theory text, e.g.\ definitions, can be put in figures, too. |
|
15342 | 371 |
*} |
372 |
||
16155 | 373 |
section {*Styles\label{sec:styles}*} |
15917
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
374 |
|
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
375 |
text {* |
15953 | 376 |
The \verb!thm! antiquotation works nicely for single theorems, but |
15917
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
377 |
sets of equations as used in definitions are more difficult to |
16040 | 378 |
typeset nicely: people tend to prefer aligned @{text "="} signs. |
15917
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
379 |
|
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
380 |
To deal with such cases where it is desirable to dive into the structure |
16040 | 381 |
of terms and theorems, Isabelle offers antiquotations featuring |
15917
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
382 |
``styles'': |
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
383 |
|
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
384 |
\begin{quote} |
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
385 |
\verb!@!\verb!{thm_style stylename thm}!\\ |
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
386 |
\verb!@!\verb!{term_style stylename term}! |
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
387 |
\end{quote} |
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
388 |
|
16040 | 389 |
A ``style'' is a transformation of propositions. There are predefined |
21558 | 390 |
styles, namely \verb!lhs! and \verb!rhs!, \verb!prem1! up to \verb!prem9!, and \verb!concl!. |
16166 | 391 |
For example, |
16076 | 392 |
the output |
15917
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
393 |
\begin{center} |
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
394 |
\begin{tabular}{l@ {~~@{text "="}~~}l} |
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
395 |
@{thm_style lhs foldl_Nil} & @{thm_style rhs foldl_Nil}\\ |
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
396 |
@{thm_style lhs foldl_Cons} & @{thm_style rhs foldl_Cons} |
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
397 |
\end{tabular} |
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
398 |
\end{center} |
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
399 |
is produced by the following code: |
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
400 |
\begin{quote} |
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
401 |
\verb!\begin{center}!\\ |
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
402 |
\verb!\begin{tabular}{l@ {~~!\verb!@!\verb!{text "="}~~}l}!\\ |
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
403 |
\verb!@!\verb!{thm_style lhs foldl_Nil} & @!\verb!{thm_style rhs foldl_Nil}!\\ |
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
404 |
\verb!@!\verb!{thm_style lhs foldl_Cons} & @!\verb!{thm_style rhs foldl_Cons}!\\ |
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
405 |
\verb!\end{tabular}!\\ |
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
406 |
\verb!\end{center}! |
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
407 |
\end{quote} |
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
408 |
Note the space between \verb!@! and \verb!{! in the tabular argument. |
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
409 |
It prevents Isabelle from interpreting \verb!@ {~~...~~}! |
16076 | 410 |
as an antiquotation. The styles \verb!lhs! and \verb!rhs! |
16040 | 411 |
extract the left hand side (or right hand side respectivly) from the |
16076 | 412 |
conclusion of propositions consisting of a binary operator |
16040 | 413 |
(e.~g.~@{text "="}, @{text "\<equiv>"}, @{text "<"}). |
15917
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
414 |
|
16165 | 415 |
Likewise, \verb!concl! may be used as a style to show just the |
16076 | 416 |
conclusion of a proposition. For example, take \verb!hd_Cons_tl!: |
16040 | 417 |
\begin{center} |
17031
ffa73448025e
added hint for position of aqu options in connection with styles
haftmann
parents:
16395
diff
changeset
|
418 |
@{thm [show_types] hd_Cons_tl} |
16040 | 419 |
\end{center} |
420 |
To print just the conclusion, |
|
15917
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
421 |
\begin{center} |
17031
ffa73448025e
added hint for position of aqu options in connection with styles
haftmann
parents:
16395
diff
changeset
|
422 |
@{thm_style [show_types] concl hd_Cons_tl} |
15917
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
423 |
\end{center} |
16040 | 424 |
type |
15917
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
425 |
\begin{quote} |
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
426 |
\verb!\begin{center}!\\ |
17031
ffa73448025e
added hint for position of aqu options in connection with styles
haftmann
parents:
16395
diff
changeset
|
427 |
\verb!@!\verb!{thm_style [show_types] concl hd_Cons_tl}!\\ |
15917
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
428 |
\verb!\end{center}! |
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
429 |
\end{quote} |
17127 | 430 |
Beware that any options must be placed \emph{before} |
17031
ffa73448025e
added hint for position of aqu options in connection with styles
haftmann
parents:
16395
diff
changeset
|
431 |
the name of the style, as in this example. |
ffa73448025e
added hint for position of aqu options in connection with styles
haftmann
parents:
16395
diff
changeset
|
432 |
|
16166 | 433 |
Further use cases can be found in \S\ref{sec:yourself}. |
434 |
||
15953 | 435 |
If you are not afraid of ML, you may also define your own styles. |
15960 | 436 |
A style is implemented by an ML function of type |
437 |
\verb!Proof.context -> term -> term!. |
|
438 |
Have a look at the following example: |
|
439 |
||
16040 | 440 |
*} |
16075 | 441 |
(*<*) |
16040 | 442 |
setup {* |
443 |
let |
|
444 |
fun my_concl ctxt = Logic.strip_imp_concl |
|
18708 | 445 |
in TermStyle.add_style "my_concl" my_concl |
16040 | 446 |
end; |
447 |
*} |
|
16075 | 448 |
(*>*) |
16040 | 449 |
text {* |
450 |
||
15917
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
451 |
\begin{quote} |
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
452 |
\verb!setup {!\verb!*!\\ |
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
453 |
\verb!let!\\ |
16040 | 454 |
\verb! fun my_concl ctxt = Logic.strip_imp_concl!\\ |
18708 | 455 |
\verb! in TermStyle.add_style "my_concl" my_concl!\\ |
15917
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
456 |
\verb!end;!\\ |
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
457 |
\verb!*!\verb!}!\\ |
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
458 |
\end{quote} |
15960 | 459 |
|
16076 | 460 |
\noindent |
16165 | 461 |
This example shows how the \verb!concl! style is implemented |
16076 | 462 |
and may be used as as a ``copy-and-paste'' pattern to write your own styles. |
15960 | 463 |
|
16076 | 464 |
The code should go into your theory file, separate from the \LaTeX\ text. |
16040 | 465 |
The \verb!let! expression avoids polluting the |
15960 | 466 |
ML global namespace. Each style receives the current proof context |
16076 | 467 |
as first argument; this is helpful in situations where the |
468 |
style has some object-logic specific behaviour for example. |
|
15960 | 469 |
|
470 |
The mapping from identifier name to the style function |
|
17123 | 471 |
is done by the @{ML TermStyle.add_style} expression which expects the desired |
15960 | 472 |
style name and the style function as arguments. |
473 |
||
474 |
After this \verb!setup!, |
|
16040 | 475 |
there will be a new style available named \verb!my_concl!, thus allowing |
476 |
antiquoations like \verb!@!\verb!{thm_style my_concl hd_Cons_tl}! |
|
477 |
yielding @{thm_style my_concl hd_Cons_tl}. |
|
15917
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
478 |
|
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
479 |
*} |
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
480 |
|
15337 | 481 |
(*<*) |
482 |
end |
|
16175 | 483 |
(*>*) |