15337
|
1 |
(*<*)
|
|
2 |
theory Sugar
|
15366
|
3 |
imports LaTeXsugar OptionalSugar
|
15337
|
4 |
begin
|
|
5 |
(*>*)
|
|
6 |
|
|
7 |
section "Introduction"
|
|
8 |
|
|
9 |
text{* This document is for those Isabelle users that have mastered
|
|
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
|
15342
|
34 |
typeset by a machine. You merely need to import theory
|
15378
|
35 |
\texttt{LaTeXsugar} in the header of your own theory and copy the bits
|
|
36 |
of \texttt{OptionalSugar} that you want to use. You may also need
|
|
37 |
additional \LaTeX\ packages. These should be included at the beginning
|
|
38 |
of your \LaTeX\ document, typically in \texttt{root.tex}.
|
|
39 |
|
|
40 |
The theories and support files are available from \cite{tar}.
|
15342
|
41 |
*}
|
|
42 |
|
|
43 |
section{* HOL syntax*}
|
|
44 |
|
|
45 |
subsection{* Logic *}
|
|
46 |
|
|
47 |
text{* The predefined constructs @{text"if"}, @{text"let"} and
|
|
48 |
@{text"case"} are set in sans serif font to distinguish them from
|
|
49 |
other functions. This improves readability:
|
|
50 |
\begin{itemize}
|
|
51 |
\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"}.
|
|
52 |
\item @{term"let x = e\<^isub>1 in e\<^isub>2"} instead of @{text"let x = e\<^isub>1 in e\<^isub>2"}.
|
|
53 |
\item @{term"case x of True \<Rightarrow> e\<^isub>1 | False \<Rightarrow> e\<^isub>2"} instead of\\
|
|
54 |
@{text"case x of True \<Rightarrow> e\<^isub>1 | False \<Rightarrow> e\<^isub>2"}.
|
|
55 |
\end{itemize}
|
|
56 |
*}
|
|
57 |
|
|
58 |
subsection{* Sets *}
|
15337
|
59 |
|
15342
|
60 |
text{* Although set syntax in HOL is already close to
|
|
61 |
standard, we provide a few further improvements:
|
|
62 |
\begin{itemize}
|
|
63 |
\item @{term"{x. P}"} instead of @{text"{x. P}"}.
|
|
64 |
\item @{term"{}"} instead of @{text"{}"}.
|
|
65 |
\item @{term"insert a (insert b (insert c M))"} instead of @{text"insert a (insert b (insert c M))"}.
|
|
66 |
\end{itemize}
|
|
67 |
*}
|
|
68 |
|
|
69 |
subsection{* Lists *}
|
|
70 |
|
|
71 |
text{* If lists are used heavily, the following notations increase readability:
|
|
72 |
\begin{itemize}
|
|
73 |
\item @{term"x # xs"} instead of @{text"x # xs"}.
|
|
74 |
Exceptionally, @{term"x # xs"} is also input syntax.
|
|
75 |
If you prefer more space around the $\cdot$ you have to redefine
|
|
76 |
\verb!\isasymcdot! in \LaTeX:
|
|
77 |
\verb!\renewcommand{\isasymcdot}{\isamath{\,\cdot\,}}!
|
|
78 |
|
|
79 |
\item @{term"length xs"} instead of @{text"length xs"}.
|
|
80 |
\item @{term"nth xs n"} instead of @{text"nth xs i"},
|
|
81 |
the $n$th element of @{text xs}.
|
|
82 |
|
15366
|
83 |
\item The @{text"@"} operation associates implicitly to the right,
|
|
84 |
which leads to unpleasant line breaks if the term is too long for one
|
|
85 |
line. To avoid this, \texttt{OptionalSugar} contains syntax to group
|
|
86 |
@{text"@"}-terms to the left before printing, which leads to better
|
|
87 |
line breaking behaviour:
|
|
88 |
@{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>9 @ term\<^isub>1\<^isub>0"}
|
|
89 |
|
15342
|
90 |
\end{itemize}
|
15337
|
91 |
*}
|
|
92 |
|
|
93 |
section "Printing theorems"
|
|
94 |
|
|
95 |
subsection "Inference rules"
|
|
96 |
|
15342
|
97 |
text{* To print theorems as inference rules you need to include Didier
|
|
98 |
R\'emy's \texttt{mathpartir} package~\cite{mathpartir}
|
|
99 |
for typesetting inference rules in your \LaTeX\ file.
|
15337
|
100 |
|
|
101 |
Writing \verb!@!\verb!{thm[mode=Rule] conjI[no_vars]}! produces
|
|
102 |
@{thm[mode=Rule] conjI[no_vars]}, even in the middle of a sentence.
|
15342
|
103 |
If you prefer your inference rule on a separate line, maybe with a name,
|
|
104 |
\begin{center}
|
|
105 |
@{thm[mode=Rule] conjI[no_vars]} {\sc conjI}
|
|
106 |
\end{center}
|
|
107 |
is produced by
|
15337
|
108 |
\begin{quote}
|
|
109 |
\verb!\begin{center}!\\
|
|
110 |
\verb!@!\verb!{thm[mode=Rule] conjI[no_vars]} {\sc conjI}!\\
|
|
111 |
\verb!\end{center}!
|
|
112 |
\end{quote}
|
15342
|
113 |
It is not recommended to use the standard \texttt{display} attribute
|
|
114 |
together with \texttt{Rule} because centering does not work and because
|
|
115 |
the line breaking mechanisms of \texttt{display} and \texttt{mathpartir} can
|
|
116 |
clash.
|
|
117 |
|
15337
|
118 |
Of course you can display multiple rules in this fashion:
|
|
119 |
\begin{quote}
|
|
120 |
\verb!\begin{center}\isastyle!\\
|
|
121 |
\verb!@!\verb!{thm[mode=Rule] conjI[no_vars]} {\sc conjI} \\[1ex]!\\
|
|
122 |
\verb!@!\verb!{thm[mode=Rule] conjE[no_vars]} {\sc disjI$_1$} \qquad!\\
|
|
123 |
\verb!@!\verb!{thm[mode=Rule] disjE[no_vars]} {\sc disjI$_2$}!\\
|
|
124 |
\verb!\end{center}!
|
|
125 |
\end{quote}
|
|
126 |
yields
|
|
127 |
\begin{center}\isastyle
|
|
128 |
@{thm[mode=Rule] conjI[no_vars]} {\sc conjI} \\[1ex]
|
|
129 |
@{thm[mode=Rule] disjI1[no_vars]} {\sc disjI$_1$} \qquad
|
|
130 |
@{thm[mode=Rule] disjI2[no_vars]} {\sc disjI$_2$}
|
|
131 |
\end{center}
|
|
132 |
Note that we included \verb!\isastyle! to obtain
|
|
133 |
the smaller font that otherwise comes only with \texttt{display}.
|
|
134 |
|
15342
|
135 |
The \texttt{mathpartir} package copes well if there are too many
|
|
136 |
premises for one line:
|
|
137 |
\begin{center}
|
|
138 |
@{prop[mode=Rule] "\<lbrakk> A \<longrightarrow> B; B \<longrightarrow> C; C \<longrightarrow> D; D \<longrightarrow> E; E \<longrightarrow> F; F \<longrightarrow> G;
|
|
139 |
G \<longrightarrow> H; H \<longrightarrow> I; I \<longrightarrow> J; J \<longrightarrow> K \<rbrakk> \<Longrightarrow> A \<longrightarrow> K"}
|
|
140 |
\end{center}
|
|
141 |
|
|
142 |
Limitations: premises and conclusion must each not be longer than the line.
|
15337
|
143 |
*}
|
15342
|
144 |
|
|
145 |
subsection{*If-then*}
|
|
146 |
|
|
147 |
text{* If you prefer a fake ``natural language'' style you can produce
|
|
148 |
the body of
|
|
149 |
\newtheorem{theorem}{Theorem}
|
|
150 |
\begin{theorem}
|
|
151 |
@{thm[mode=IfThen,eta_contract=false] setsum_cartesian_product[no_vars]}
|
|
152 |
\end{theorem}
|
|
153 |
by typing
|
|
154 |
\begin{quote}
|
|
155 |
\verb!@!\verb!{thm[mode=IfThen] setsum_cartesian_product[no_vars]}!
|
|
156 |
\end{quote}
|
|
157 |
|
|
158 |
In order to prevent odd line breaks, the premises are put into boxes.
|
|
159 |
At times this is too drastic:
|
|
160 |
\begin{theorem}
|
|
161 |
@{prop[mode=IfThen] "longpremise \<Longrightarrow> longerpremise \<Longrightarrow> P(f(f(f(f(f(f(f(f(f(x)))))))))) \<Longrightarrow> longestpremise \<Longrightarrow> conclusion"}
|
|
162 |
\end{theorem}
|
|
163 |
In which case you should use \texttt{mode=IfThenNoBox} instead of
|
|
164 |
\texttt{mode=IfThen}:
|
|
165 |
\begin{theorem}
|
|
166 |
@{prop[mode=IfThenNoBox] "longpremise \<Longrightarrow> longerpremise \<Longrightarrow> P(f(f(f(f(f(f(f(f(f(x)))))))))) \<Longrightarrow> longestpremise \<Longrightarrow> conclusion"}
|
|
167 |
\end{theorem}
|
15366
|
168 |
*}
|
15342
|
169 |
|
15366
|
170 |
subsection {*Definitions and Equations*}
|
|
171 |
|
|
172 |
text {*
|
|
173 |
The \verb!thm! antiquotation works nicely for proper theorems, but
|
15368
|
174 |
sets of equations as used in definitions are more difficult to
|
15366
|
175 |
typeset nicely: for some reason people tend to prefer aligned
|
|
176 |
@{text "="} signs.
|
|
177 |
|
|
178 |
Isabelle2005 will have a nice mechanism for that, namely the two
|
|
179 |
antiquotations \verb!@!\verb!{lhs thm}! and \verb!@!\verb!{rhs thm}!.
|
|
180 |
|
|
181 |
\begin{center}
|
|
182 |
\begin{tabular}{l@ {~~@{text "="}~~}l}
|
|
183 |
@{lhs foldl_Nil[no_vars]} & @{rhs foldl_Nil[no_vars]}\\
|
|
184 |
@{lhs foldl_Cons[no_vars]} & @{rhs foldl_Cons[no_vars]}
|
|
185 |
\end{tabular}
|
|
186 |
\end{center}
|
|
187 |
|
|
188 |
\noindent
|
|
189 |
is produced by the following code:
|
|
190 |
|
|
191 |
\begin{quote}
|
|
192 |
\verb!\begin{center}!\\
|
|
193 |
\verb!\begin{tabular}{l@ {~~!\verb!@!\verb!{text "="}~~}l}!\\
|
|
194 |
\verb!@!\verb!{lhs foldl_Nil[no_vars]} & @!\verb!{rhs foldl_Nil[no_vars]}!\\
|
|
195 |
\verb!@!\verb!{lhs foldl_Cons[no_vars]} & @!\verb!{rhs foldl_Cons[no_vars]}!\\
|
|
196 |
\verb!\end{tabular}!\\
|
|
197 |
\verb!\end{center}!
|
|
198 |
\end{quote}
|
|
199 |
|
|
200 |
\noindent
|
|
201 |
Note the space between \verb!@! and \verb!{! in the tabular argument.
|
|
202 |
It prevents Isabelle from interpreting \verb!@ {~~...~~}!
|
|
203 |
as antiquotation. \verb!@!\verb!{lhs thm}! and \verb!@!\verb!{rhs thm}!
|
|
204 |
try to be smart about the interpretation of the theorem they
|
|
205 |
print, they work just as well for meta equality @{text "\<equiv>"} and other
|
|
206 |
binary operators like @{text "<"}.
|
|
207 |
|
|
208 |
Should you lack both the development version of Isabelle and a time
|
|
209 |
machine, you can still try to simulate the effect using the equation syntax
|
|
210 |
in \texttt{sugar.sty} and \texttt{OptionalSugar}.
|
|
211 |
|
|
212 |
\begin{center}
|
|
213 |
\begin{tabular}{l@ { }l@ { }l}
|
|
214 |
\setcounter{isatabs}{0}%
|
|
215 |
@{thm [mode=tab] foldl_Nil[no_vars]}\nl
|
|
216 |
@{thm [mode=tab] foldl_Cons[no_vars]}
|
|
217 |
\end{tabular}
|
|
218 |
\end{center}
|
|
219 |
|
|
220 |
\noindent
|
|
221 |
is produced by:
|
|
222 |
|
|
223 |
\begin{quote}
|
|
224 |
\verb!\begin{center}!\\
|
|
225 |
\verb!\begin{tabular}{l@ { }l@ { }l}!\\
|
|
226 |
\verb!\setcounter{isatabs}{0}%!\\
|
|
227 |
\verb!@!\verb!{thm [mode=tab] foldl_Nil[no_vars]}\nl!\\
|
|
228 |
\verb!@!\verb!{thm [mode=tab] foldl_Cons[no_vars]}!\\
|
|
229 |
\verb!\end{tabular}!\\
|
|
230 |
\verb!\end{center}!
|
|
231 |
\end{quote}
|
|
232 |
|
|
233 |
\noindent
|
|
234 |
These \LaTeX\ macros are not as flexible as the antiquotations
|
|
235 |
above, they only work for proper equations and definitions and they
|
|
236 |
only work correctly if the left hand side does not contain any
|
|
237 |
@{text "="} signs.
|
|
238 |
*}
|
|
239 |
|
|
240 |
subsection "Patterns"
|
|
241 |
|
|
242 |
text {*
|
|
243 |
Sometimes functions ignore one or more of their
|
|
244 |
arguments and some functional languages have nice
|
|
245 |
syntax for that as in @{thm hd.simps [where xs=DUMMY,no_vars]}.
|
|
246 |
|
|
247 |
You can simulate this in Isabelle by instantiating the @{term xs} in
|
|
248 |
definition \mbox{@{thm hd.simps[no_vars]}} with a constant @{text DUMMY} that
|
|
249 |
is printed as @{term DUMMY}. The code for the pattern above is
|
15373
|
250 |
\verb!@!\verb!{thm hd.simps [where xs=DUMMY,no_vars]}!.
|
15366
|
251 |
|
|
252 |
You can drive this game even further and extend the syntax of let
|
|
253 |
bindings such that certain functions like @{term fst}, @{term hd},
|
15368
|
254 |
etc.\ are printed as patterns. \texttt{OptionalSugar} provides the
|
|
255 |
following:
|
15366
|
256 |
|
|
257 |
\begin{center}
|
|
258 |
\begin{tabular}{l@ {~~produced by~~}l}
|
|
259 |
@{term "let x = fst p in t"} & \verb!@!\verb!{term "let x = fst p in t"}!\\
|
|
260 |
@{term "let x = snd p in t"} & \verb!@!\verb!{term "let x = snd p in t"}!\\
|
|
261 |
@{term "let x = hd xs in t"} & \verb!@!\verb!{term "let x = hd xs in t"}!\\
|
|
262 |
@{term "let x = tl xs in t"} & \verb!@!\verb!{term "let x = tl xs in t"}!\\
|
|
263 |
@{term "let x = the y in t"} & \verb!@!\verb!{term "let x = the y in t"}!\\
|
|
264 |
\end{tabular}
|
|
265 |
\end{center}
|
|
266 |
*}
|
|
267 |
|
|
268 |
subsection "Proofs"
|
|
269 |
|
|
270 |
text {*
|
15367
|
271 |
Full proofs, even if written in beautiful Isar style, are likely to
|
15366
|
272 |
be too long and detailed to be included in conference papers, but
|
|
273 |
some key lemmas might be of interest.
|
|
274 |
|
|
275 |
It is usually easiest to put them in figures like the one in Fig.\
|
|
276 |
\ref{fig:proof}. This was achieved with the \isakeyword{text\_raw}
|
|
277 |
command:
|
|
278 |
*}
|
|
279 |
text_raw {*
|
|
280 |
\begin{figure}
|
|
281 |
\begin{center}\begin{minipage}{0.6\textwidth}
|
|
282 |
\begin{isabellebody}
|
|
283 |
*}
|
|
284 |
lemma True
|
|
285 |
proof -
|
|
286 |
-- "pretty trivial"
|
|
287 |
show True by force
|
|
288 |
qed
|
|
289 |
text_raw {*
|
|
290 |
\end{isabellebody}
|
|
291 |
\end{minipage}\end{center}
|
|
292 |
\caption{Example proof in a figure.}\label{fig:proof}
|
|
293 |
\end{figure}
|
|
294 |
*}
|
|
295 |
text {*
|
|
296 |
|
|
297 |
\begin{quote}
|
|
298 |
\small
|
|
299 |
\verb!text_raw {!\verb!*!\\
|
|
300 |
\verb! \begin{figure}!\\
|
|
301 |
\verb! \begin{center}\begin{minipage}{0.6\textwidth}!\\
|
|
302 |
\verb! \begin{isabellebody}!\\
|
|
303 |
\verb!*!\verb!}!\\
|
|
304 |
\verb!lemma True!\\
|
|
305 |
\verb!proof -!\\
|
|
306 |
\verb! -- "pretty trivial"!\\
|
|
307 |
\verb! show True by force!\\
|
|
308 |
\verb!qed!\\
|
|
309 |
\verb!text_raw {!\verb!*!\\
|
|
310 |
\verb! \end{isabellebody}!\\
|
|
311 |
\verb! \end{minipage}\end{center}!\\
|
|
312 |
\verb! \caption{Example proof in a figure.}\label{fig:proof}!\\
|
|
313 |
\verb! \end{figure}!\\
|
|
314 |
\verb!*!\verb!}!
|
|
315 |
\end{quote}
|
|
316 |
|
15342
|
317 |
*}
|
|
318 |
|
15337
|
319 |
(*<*)
|
|
320 |
end
|
|
321 |
(*>*) |