author | nipkow |
Thu, 12 May 2005 09:45:54 +0200 | |
changeset 15953 | 902b556e4bc0 |
parent 15917 | cd4983c76548 |
child 15960 | 9bd6550dc004 |
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, |
|
43 |
typically in \texttt{root.tex}. |
|
44 |
\end{itemize} |
|
15342 | 45 |
*} |
46 |
||
47 |
section{* HOL syntax*} |
|
48 |
||
49 |
subsection{* Logic *} |
|
50 |
||
51 |
text{* The predefined constructs @{text"if"}, @{text"let"} and |
|
52 |
@{text"case"} are set in sans serif font to distinguish them from |
|
53 |
other functions. This improves readability: |
|
54 |
\begin{itemize} |
|
55 |
\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"}. |
|
56 |
\item @{term"let x = e\<^isub>1 in e\<^isub>2"} instead of @{text"let x = e\<^isub>1 in e\<^isub>2"}. |
|
57 |
\item @{term"case x of True \<Rightarrow> e\<^isub>1 | False \<Rightarrow> e\<^isub>2"} instead of\\ |
|
58 |
@{text"case x of True \<Rightarrow> e\<^isub>1 | False \<Rightarrow> e\<^isub>2"}. |
|
59 |
\end{itemize} |
|
60 |
*} |
|
61 |
||
62 |
subsection{* Sets *} |
|
15337 | 63 |
|
15342 | 64 |
text{* Although set syntax in HOL is already close to |
65 |
standard, we provide a few further improvements: |
|
66 |
\begin{itemize} |
|
67 |
\item @{term"{x. P}"} instead of @{text"{x. P}"}. |
|
68 |
\item @{term"{}"} instead of @{text"{}"}. |
|
69 |
\item @{term"insert a (insert b (insert c M))"} instead of @{text"insert a (insert b (insert c M))"}. |
|
70 |
\end{itemize} |
|
71 |
*} |
|
72 |
||
73 |
subsection{* Lists *} |
|
74 |
||
75 |
text{* If lists are used heavily, the following notations increase readability: |
|
76 |
\begin{itemize} |
|
77 |
\item @{term"x # xs"} instead of @{text"x # xs"}. |
|
78 |
Exceptionally, @{term"x # xs"} is also input syntax. |
|
79 |
If you prefer more space around the $\cdot$ you have to redefine |
|
80 |
\verb!\isasymcdot! in \LaTeX: |
|
81 |
\verb!\renewcommand{\isasymcdot}{\isamath{\,\cdot\,}}! |
|
82 |
||
83 |
\item @{term"length xs"} instead of @{text"length xs"}. |
|
15385 | 84 |
\item @{term"nth xs n"} instead of @{text"nth xs n"}, |
15342 | 85 |
the $n$th element of @{text xs}. |
86 |
||
15366 | 87 |
\item The @{text"@"} operation associates implicitly to the right, |
88 |
which leads to unpleasant line breaks if the term is too long for one |
|
89 |
line. To avoid this, \texttt{OptionalSugar} contains syntax to group |
|
90 |
@{text"@"}-terms to the left before printing, which leads to better |
|
91 |
line breaking behaviour: |
|
15673 | 92 |
@{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 | 93 |
|
15342 | 94 |
\end{itemize} |
15337 | 95 |
*} |
96 |
||
97 |
section "Printing theorems" |
|
98 |
||
15689 | 99 |
subsection "Question marks" |
100 |
||
101 |
text{* If you print anything, especially theorems, containing |
|
102 |
schematic variables they are prefixed with a question mark: |
|
103 |
\verb!@!\verb!{thm conjI}! results in @{thm conjI}. Most of the time |
|
104 |
you would rather not see the question marks. There is an attribute |
|
105 |
\verb!no_vars! that you can attach to the theorem that turns its |
|
106 |
schematic into ordinary free variables: \verb!@!\verb!{thm conjI[no_vars]}! |
|
107 |
results in @{thm conjI[no_vars]}. |
|
108 |
||
109 |
This \verb!no_vars! business can become a bit tedious. |
|
110 |
If you would rather never see question marks, simply put |
|
111 |
\begin{verbatim} |
|
112 |
reset show_var_qmarks; |
|
113 |
\end{verbatim} |
|
114 |
at the beginning of your file \texttt{ROOT.ML}. |
|
115 |
The rest of this document is produced with this flag reset. |
|
116 |
*} |
|
117 |
||
118 |
(*<*)ML"reset show_var_qmarks"(*>*) |
|
119 |
||
15337 | 120 |
subsection "Inference rules" |
121 |
||
15342 | 122 |
text{* To print theorems as inference rules you need to include Didier |
123 |
R\'emy's \texttt{mathpartir} package~\cite{mathpartir} |
|
124 |
for typesetting inference rules in your \LaTeX\ file. |
|
15337 | 125 |
|
15689 | 126 |
Writing \verb!@!\verb!{thm[mode=Rule] conjI}! produces |
127 |
@{thm[mode=Rule] conjI}, even in the middle of a sentence. |
|
15342 | 128 |
If you prefer your inference rule on a separate line, maybe with a name, |
129 |
\begin{center} |
|
15689 | 130 |
@{thm[mode=Rule] conjI} {\sc conjI} |
15342 | 131 |
\end{center} |
132 |
is produced by |
|
15337 | 133 |
\begin{quote} |
134 |
\verb!\begin{center}!\\ |
|
15689 | 135 |
\verb!@!\verb!{thm[mode=Rule] conjI} {\sc conjI}!\\ |
15337 | 136 |
\verb!\end{center}! |
137 |
\end{quote} |
|
15342 | 138 |
It is not recommended to use the standard \texttt{display} attribute |
139 |
together with \texttt{Rule} because centering does not work and because |
|
140 |
the line breaking mechanisms of \texttt{display} and \texttt{mathpartir} can |
|
141 |
clash. |
|
142 |
||
15337 | 143 |
Of course you can display multiple rules in this fashion: |
144 |
\begin{quote} |
|
145 |
\verb!\begin{center}\isastyle!\\ |
|
15689 | 146 |
\verb!@!\verb!{thm[mode=Rule] conjI} {\sc conjI} \\[1ex]!\\ |
147 |
\verb!@!\verb!{thm[mode=Rule] conjE} {\sc disjI$_1$} \qquad!\\ |
|
148 |
\verb!@!\verb!{thm[mode=Rule] disjE} {\sc disjI$_2$}!\\ |
|
15337 | 149 |
\verb!\end{center}! |
150 |
\end{quote} |
|
151 |
yields |
|
152 |
\begin{center}\isastyle |
|
15689 | 153 |
@{thm[mode=Rule] conjI} {\sc conjI} \\[1ex] |
154 |
@{thm[mode=Rule] disjI1} {\sc disjI$_1$} \qquad |
|
155 |
@{thm[mode=Rule] disjI2} {\sc disjI$_2$} |
|
15337 | 156 |
\end{center} |
157 |
Note that we included \verb!\isastyle! to obtain |
|
158 |
the smaller font that otherwise comes only with \texttt{display}. |
|
159 |
||
15342 | 160 |
The \texttt{mathpartir} package copes well if there are too many |
161 |
premises for one line: |
|
162 |
\begin{center} |
|
163 |
@{prop[mode=Rule] "\<lbrakk> A \<longrightarrow> B; B \<longrightarrow> C; C \<longrightarrow> D; D \<longrightarrow> E; E \<longrightarrow> F; F \<longrightarrow> G; |
|
164 |
G \<longrightarrow> H; H \<longrightarrow> I; I \<longrightarrow> J; J \<longrightarrow> K \<rbrakk> \<Longrightarrow> A \<longrightarrow> K"} |
|
165 |
\end{center} |
|
166 |
||
15471 | 167 |
Limitations: 1. Premises and conclusion must each not be longer than |
168 |
the line. 2. Premises that are @{text"\<Longrightarrow>"}-implications are again |
|
169 |
displayed with a horizontal line, which looks at least unusual. |
|
170 |
||
15337 | 171 |
*} |
15342 | 172 |
|
173 |
subsection{*If-then*} |
|
174 |
||
175 |
text{* If you prefer a fake ``natural language'' style you can produce |
|
176 |
the body of |
|
177 |
\newtheorem{theorem}{Theorem} |
|
178 |
\begin{theorem} |
|
15689 | 179 |
@{thm[mode=IfThen] le_trans} |
15342 | 180 |
\end{theorem} |
181 |
by typing |
|
182 |
\begin{quote} |
|
15689 | 183 |
\verb!@!\verb!{thm[mode=IfThen] le_trans}! |
15342 | 184 |
\end{quote} |
185 |
||
186 |
In order to prevent odd line breaks, the premises are put into boxes. |
|
187 |
At times this is too drastic: |
|
188 |
\begin{theorem} |
|
189 |
@{prop[mode=IfThen] "longpremise \<Longrightarrow> longerpremise \<Longrightarrow> P(f(f(f(f(f(f(f(f(f(x)))))))))) \<Longrightarrow> longestpremise \<Longrightarrow> conclusion"} |
|
190 |
\end{theorem} |
|
191 |
In which case you should use \texttt{mode=IfThenNoBox} instead of |
|
192 |
\texttt{mode=IfThen}: |
|
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"} |
|
195 |
\end{theorem} |
|
15366 | 196 |
*} |
15342 | 197 |
|
15366 | 198 |
subsection "Patterns" |
199 |
||
200 |
text {* |
|
201 |
Sometimes functions ignore one or more of their |
|
202 |
arguments and some functional languages have nice |
|
15689 | 203 |
syntax for that as in @{thm hd.simps [where xs=DUMMY]}. |
15366 | 204 |
|
205 |
You can simulate this in Isabelle by instantiating the @{term xs} in |
|
15689 | 206 |
definition \mbox{@{thm hd.simps}} with a constant @{text DUMMY} that |
15366 | 207 |
is printed as @{term DUMMY}. The code for the pattern above is |
15689 | 208 |
\verb!@!\verb!{thm hd.simps [where xs=DUMMY]}!. |
15366 | 209 |
|
210 |
You can drive this game even further and extend the syntax of let |
|
211 |
bindings such that certain functions like @{term fst}, @{term hd}, |
|
15368 | 212 |
etc.\ are printed as patterns. \texttt{OptionalSugar} provides the |
213 |
following: |
|
15366 | 214 |
|
215 |
\begin{center} |
|
216 |
\begin{tabular}{l@ {~~produced by~~}l} |
|
217 |
@{term "let x = fst p in t"} & \verb!@!\verb!{term "let x = fst p in t"}!\\ |
|
218 |
@{term "let x = snd p in t"} & \verb!@!\verb!{term "let x = snd p in t"}!\\ |
|
219 |
@{term "let x = hd xs in t"} & \verb!@!\verb!{term "let x = hd xs in t"}!\\ |
|
220 |
@{term "let x = tl xs in t"} & \verb!@!\verb!{term "let x = tl xs in t"}!\\ |
|
221 |
@{term "let x = the y in t"} & \verb!@!\verb!{term "let x = the y in t"}!\\ |
|
222 |
\end{tabular} |
|
223 |
\end{center} |
|
224 |
*} |
|
225 |
||
226 |
subsection "Proofs" |
|
227 |
||
228 |
text {* |
|
15367 | 229 |
Full proofs, even if written in beautiful Isar style, are likely to |
15366 | 230 |
be too long and detailed to be included in conference papers, but |
231 |
some key lemmas might be of interest. |
|
232 |
||
233 |
It is usually easiest to put them in figures like the one in Fig.\ |
|
234 |
\ref{fig:proof}. This was achieved with the \isakeyword{text\_raw} |
|
235 |
command: |
|
236 |
*} |
|
237 |
text_raw {* |
|
238 |
\begin{figure} |
|
239 |
\begin{center}\begin{minipage}{0.6\textwidth} |
|
15428 | 240 |
\isastyle\isamarkuptrue |
15366 | 241 |
*} |
242 |
lemma True |
|
243 |
proof - |
|
244 |
-- "pretty trivial" |
|
245 |
show True by force |
|
246 |
qed |
|
15428 | 247 |
text_raw {* |
15366 | 248 |
\end{minipage}\end{center} |
249 |
\caption{Example proof in a figure.}\label{fig:proof} |
|
250 |
\end{figure} |
|
251 |
*} |
|
252 |
text {* |
|
253 |
||
254 |
\begin{quote} |
|
255 |
\small |
|
256 |
\verb!text_raw {!\verb!*!\\ |
|
257 |
\verb! \begin{figure}!\\ |
|
258 |
\verb! \begin{center}\begin{minipage}{0.6\textwidth}!\\ |
|
15428 | 259 |
\verb! \isastyle\isamarkuptrue!\\ |
15366 | 260 |
\verb!*!\verb!}!\\ |
261 |
\verb!lemma True!\\ |
|
262 |
\verb!proof -!\\ |
|
263 |
\verb! -- "pretty trivial"!\\ |
|
264 |
\verb! show True by force!\\ |
|
265 |
\verb!qed!\\ |
|
266 |
\verb!text_raw {!\verb!*!\\ |
|
267 |
\verb! \end{minipage}\end{center}!\\ |
|
268 |
\verb! \caption{Example proof in a figure.}\label{fig:proof}!\\ |
|
269 |
\verb! \end{figure}!\\ |
|
270 |
\verb!*!\verb!}! |
|
271 |
\end{quote} |
|
272 |
||
15342 | 273 |
*} |
274 |
||
15917
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
275 |
subsection "Styles" |
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
276 |
|
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
277 |
text {* |
15953 | 278 |
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
|
279 |
sets of equations as used in definitions are more difficult to |
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
280 |
typeset nicely: for some reason people tend to prefer aligned |
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
281 |
@{text "="} signs. |
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
282 |
|
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
283 |
To deal with such cases where it is desirable to dive into the structure |
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
284 |
of terms and theorems, Isabelle offers two antiquotations featuring |
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
285 |
``styles'': |
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
286 |
|
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
287 |
\begin{quote} |
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
288 |
\verb!@!\verb!{thm_style stylename thm}!\\ |
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
289 |
\verb!@!\verb!{term_style stylename term}! |
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
290 |
\end{quote} |
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
291 |
|
15953 | 292 |
A ``style'' is a transformation of terms. There are three predefined |
293 |
styles, named \verb!lhs!, \verb!rhs! and \verb!conclusion!, with obvious |
|
294 |
meanings. For example, the output |
|
15917
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
295 |
\begin{center} |
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
296 |
\begin{tabular}{l@ {~~@{text "="}~~}l} |
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
297 |
@{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
|
298 |
@{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
|
299 |
\end{tabular} |
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
300 |
\end{center} |
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
301 |
is produced by the following code: |
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
302 |
\begin{quote} |
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
303 |
\verb!\begin{center}!\\ |
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
304 |
\verb!\begin{tabular}{l@ {~~!\verb!@!\verb!{text "="}~~}l}!\\ |
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
305 |
\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
|
306 |
\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
|
307 |
\verb!\end{tabular}!\\ |
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
308 |
\verb!\end{center}! |
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
309 |
\end{quote} |
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
310 |
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
|
311 |
It prevents Isabelle from interpreting \verb!@ {~~...~~}! |
15953 | 312 |
as an antiquotation. Both styles \verb!lhs! and \verb!rhs! |
15917
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
313 |
try to be smart about the interpretation of the theorem they transform |
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
314 |
they work just as well for meta equality @{text "\<equiv>"} and other |
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
315 |
binary operators like @{text "<"}. |
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
316 |
|
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
317 |
Likewise \verb!conclusion! may be used as style to show just the conclusion |
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
318 |
of a formula: |
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
319 |
\begin{center} |
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
320 |
@{thm_style conclusion hd_Cons_tl} |
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
321 |
\end{center} |
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
322 |
is produced by |
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
323 |
\begin{quote} |
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
324 |
\verb!\begin{center}!\\ |
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
325 |
\verb!@!\verb!{thm_style conclusion hd_Cons_tl}!\\ |
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
326 |
\verb!\end{center}! |
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
327 |
\end{quote} |
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
328 |
|
15953 | 329 |
If you are not afraid of ML, you may also define your own styles. |
330 |
A style is simply implemented by an ML function of type \verb!term -> term!. |
|
15917
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
331 |
Have a look at the following example (which indeed shows just the way the |
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
332 |
\verb!lhs! style is implemented): |
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
333 |
\begin{quote} |
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
334 |
\verb!setup {!\verb!*!\\ |
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
335 |
\verb!let!\\ |
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
336 |
\verb! fun my_lhs (Const ("==", _) $ t $ _) = t!\\ |
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
337 |
\verb! | my_lhs (Const ("Trueprop", _) $ t) = my_lhs t!\\ |
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
338 |
\verb! | my_lhs (Const ("==>", _) $ _ $ t) = my_lhs t!\\ |
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
339 |
\verb! | my_lhs (_ $ t $ _) = t!\\ |
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
340 |
\verb! | my_lhs _ = error ("Binary operator expected")!\\ |
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
341 |
\verb! in [Style.put_style "new_lhs" my_lhs]!\\ |
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
342 |
\verb!end;!\\ |
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
343 |
\verb!*!\verb!}!\\ |
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
344 |
\end{quote} |
15953 | 345 |
This code must go into your theory file, not as part of your |
346 |
\LaTeX\ text but as a separate command in front of it. |
|
15917
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
347 |
Like in this example, it is recommended to put the definition of the style |
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
348 |
function into a \verb!let! expression, in order not to pollute the |
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
349 |
ML global namespace. The mapping from identifier name to the style function |
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
350 |
is done by the \verb!Style.put_style! expression which expects the desired |
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
351 |
style name and the style function as arguments. After this \verb!setup!, |
15953 | 352 |
there will be a new style available named \verb!new_lhs! allowing |
353 |
antiquoations like \verb!@!\verb!{thm_style new_lhs rev_map}! |
|
354 |
yielding @{thm_style lhs rev_map}. |
|
15917
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
355 |
|
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
356 |
The example above may be used as as a ``copy-and-paste'' pattern to write |
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
357 |
your own styles; for a description of the constructs used, please refer |
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
358 |
to the Isabelle reference manual. |
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
359 |
|
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
360 |
*} |
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
361 |
|
15337 | 362 |
(*<*) |
363 |
end |
|
364 |
(*>*) |