author | wenzelm |
Fri, 06 Nov 2015 23:31:11 +0100 | |
changeset 61594 | 07a903c8cc91 |
parent 58620 | 7435b6a3f72e |
child 61645 | ae5e55d03e45 |
permissions | -rw-r--r-- |
15337 | 1 |
(*<*) |
2 |
theory Sugar |
|
41413
64cd30d6b0b8
explicit file specifications -- avoid secondary load path;
wenzelm
parents:
38980
diff
changeset
|
3 |
imports "~~/src/HOL/Library/LaTeXsugar" "~~/src/HOL/Library/OptionalSugar" |
15337 | 4 |
begin |
5 |
(*>*) |
|
49239 | 6 |
text{* |
7 |
\section{Introduction} |
|
15337 | 8 |
|
49239 | 9 |
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 |
|
56977 | 12 |
bliss of writing \verb!@!\verb!{thm[display,mode=latex_sum] setsum_Suc_diff [no_vars]}! |
15337 | 13 |
and seeing Isabelle typeset it for them: |
56977 | 14 |
@{thm[display,mode=latex_sum] setsum_Suc_diff[no_vars]} |
15342 | 15 |
No typos, no omissions, no sweat. |
16 |
If you have not experienced that joy, read Chapter 4, \emph{Presenting |
|
58620 | 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} |
49239 | 48 |
|
15342 | 49 |
|
49239 | 50 |
\section{HOL syntax} |
15342 | 51 |
|
49239 | 52 |
\subsection{Logic} |
15342 | 53 |
|
49239 | 54 |
The formula @{prop[source]"\<not>(\<exists>x. P x)"} is typeset as @{prop"~(EX x. P x)"}. |
16153 | 55 |
|
56 |
The predefined constructs @{text"if"}, @{text"let"} and |
|
15342 | 57 |
@{text"case"} are set in sans serif font to distinguish them from |
58 |
other functions. This improves readability: |
|
59 |
\begin{itemize} |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49628
diff
changeset
|
60 |
\item @{term"if b then e\<^sub>1 else e\<^sub>2"} instead of @{text"if b then e\<^sub>1 else e\<^sub>2"}. |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49628
diff
changeset
|
61 |
\item @{term"let x = e\<^sub>1 in e\<^sub>2"} instead of @{text"let x = e\<^sub>1 in e\<^sub>2"}. |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49628
diff
changeset
|
62 |
\item @{term"case x of True \<Rightarrow> e\<^sub>1 | False \<Rightarrow> e\<^sub>2"} instead of\\ |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49628
diff
changeset
|
63 |
@{text"case x of True \<Rightarrow> e\<^sub>1 | False \<Rightarrow> e\<^sub>2"}. |
15342 | 64 |
\end{itemize} |
65 |
||
49239 | 66 |
\subsection{Sets} |
15337 | 67 |
|
49239 | 68 |
Although set syntax in HOL is already close to |
15342 | 69 |
standard, we provide a few further improvements: |
70 |
\begin{itemize} |
|
71 |
\item @{term"{x. P}"} instead of @{text"{x. P}"}. |
|
27688 | 72 |
\item @{term"{}"} instead of @{text"{}"}, where |
73 |
@{term"{}"} is also input syntax. |
|
15342 | 74 |
\item @{term"insert a (insert b (insert c M))"} instead of @{text"insert a (insert b (insert c M))"}. |
56977 | 75 |
\item @{term"card A"} instead of @{text"card A"}. |
15342 | 76 |
\end{itemize} |
49239 | 77 |
|
15342 | 78 |
|
49239 | 79 |
\subsection{Lists} |
15342 | 80 |
|
49239 | 81 |
If lists are used heavily, the following notations increase readability: |
15342 | 82 |
\begin{itemize} |
27688 | 83 |
\item @{term"x # xs"} instead of @{text"x # xs"}, |
84 |
where @{term"x # xs"} is also input syntax. |
|
15342 | 85 |
\item @{term"length xs"} instead of @{text"length xs"}. |
15385 | 86 |
\item @{term"nth xs n"} instead of @{text"nth xs n"}, |
15342 | 87 |
the $n$th element of @{text xs}. |
88 |
||
22834 | 89 |
\item Human readers are good at converting automatically from lists to |
30502 | 90 |
sets. Hence \texttt{OptionalSugar} contains syntax for suppressing the |
22834 | 91 |
conversion function @{const set}: for example, @{prop[source]"x \<in> set xs"} |
92 |
becomes @{prop"x \<in> set xs"}. |
|
93 |
||
15366 | 94 |
\item The @{text"@"} operation associates implicitly to the right, |
95 |
which leads to unpleasant line breaks if the term is too long for one |
|
96 |
line. To avoid this, \texttt{OptionalSugar} contains syntax to group |
|
97 |
@{text"@"}-terms to the left before printing, which leads to better |
|
98 |
line breaking behaviour: |
|
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49628
diff
changeset
|
99 |
@{term[display]"term\<^sub>0 @ term\<^sub>1 @ term\<^sub>2 @ term\<^sub>3 @ term\<^sub>4 @ term\<^sub>5 @ term\<^sub>6 @ term\<^sub>7 @ term\<^sub>8 @ term\<^sub>9 @ term\<^sub>1\<^sub>0"} |
15366 | 100 |
|
15342 | 101 |
\end{itemize} |
49239 | 102 |
|
15337 | 103 |
|
49239 | 104 |
\subsection{Numbers} |
30502 | 105 |
|
49239 | 106 |
Coercions between numeric types are alien to mathematicians who |
30502 | 107 |
consider, for example, @{typ nat} as a subset of @{typ int}. |
108 |
\texttt{OptionalSugar} contains syntax for suppressing numeric coercions such |
|
109 |
as @{const int} @{text"::"} @{typ"nat \<Rightarrow> int"}. For example, |
|
110 |
@{term[source]"int 5"} is printed as @{term "int 5"}. Embeddings of types |
|
111 |
@{typ nat}, @{typ int}, @{typ real} are covered; non-injective coercions such |
|
112 |
as @{const nat} @{text"::"} @{typ"int \<Rightarrow> nat"} are not and should not be |
|
49239 | 113 |
hidden. |
30502 | 114 |
|
15337 | 115 |
|
49239 | 116 |
\section{Printing theorems} |
15689 | 117 |
|
49239 | 118 |
\subsection{Question marks} |
119 |
||
120 |
If you print anything, especially theorems, containing |
|
15689 | 121 |
schematic variables they are prefixed with a question mark: |
122 |
\verb!@!\verb!{thm conjI}! results in @{thm conjI}. Most of the time |
|
123 |
you would rather not see the question marks. There is an attribute |
|
124 |
\verb!no_vars! that you can attach to the theorem that turns its |
|
125 |
schematic into ordinary free variables: \verb!@!\verb!{thm conjI[no_vars]}! |
|
126 |
results in @{thm conjI[no_vars]}. |
|
127 |
||
128 |
This \verb!no_vars! business can become a bit tedious. |
|
129 |
If you would rather never see question marks, simply put |
|
34877
ded5b770ec1c
formal antiquotations for ML snippets; no "open" unsynchronized references
haftmann
parents:
33323
diff
changeset
|
130 |
\begin{quote} |
49239 | 131 |
\verb!options [show_question_marks = false]! |
34877
ded5b770ec1c
formal antiquotations for ML snippets; no "open" unsynchronized references
haftmann
parents:
33323
diff
changeset
|
132 |
\end{quote} |
49239 | 133 |
into the relevant \texttt{ROOT} file, just before the \texttt{theories} for that session. |
33323 | 134 |
The rest of this document is produced with this flag set to \texttt{false}. |
16075 | 135 |
|
49239 | 136 |
Hint: Setting \verb!show_question_marks! to \texttt{false} only |
33323 | 137 |
suppresses question marks; variables that end in digits, |
138 |
e.g. @{text"x1"}, are still printed with a trailing @{text".0"}, |
|
139 |
e.g. @{text"x1.0"}, their internal index. This can be avoided by |
|
61594 | 140 |
turning the last digit into a subscript: write \<^verbatim>\<open>x\<^sub>1\<close> and |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
49628
diff
changeset
|
141 |
obtain the much nicer @{text"x\<^sub>1"}. *} |
15689 | 142 |
|
38980
af73cf0dc31f
turned show_question_marks into proper configuration option;
wenzelm
parents:
38798
diff
changeset
|
143 |
(*<*)declare [[show_question_marks = false]](*>*) |
15689 | 144 |
|
24496 | 145 |
subsection {*Qualified names*} |
146 |
||
147 |
text{* If there are multiple declarations of the same name, Isabelle prints |
|
148 |
the qualified name, for example @{text "T.length"}, where @{text T} is the |
|
149 |
theory it is defined in, to distinguish it from the predefined @{const[source] |
|
150 |
"List.length"}. In case there is no danger of confusion, you can insist on |
|
42669
04dfffda5671
more conventional naming scheme: names_long, names_short, names_unique;
wenzelm
parents:
42358
diff
changeset
|
151 |
short names (no qualifiers) by setting the \verb!names_short! |
42358
b47d41d9f4b5
Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
wenzelm
parents:
42289
diff
changeset
|
152 |
configuration option in the context. |
49239 | 153 |
|
24496 | 154 |
|
49239 | 155 |
\subsection {Variable names\label{sec:varnames}} |
16395 | 156 |
|
49239 | 157 |
It sometimes happens that you want to change the name of a |
16395 | 158 |
variable in a theorem before printing it. This can easily be achieved |
159 |
with the help of Isabelle's instantiation attribute \texttt{where}: |
|
160 |
@{thm conjI[where P = \<phi> and Q = \<psi>]} is the result of |
|
161 |
\begin{quote} |
|
162 |
\verb!@!\verb!{thm conjI[where P = \<phi> and Q = \<psi>]}! |
|
163 |
\end{quote} |
|
164 |
To support the ``\_''-notation for irrelevant variables |
|
165 |
the constant \texttt{DUMMY} has been introduced: |
|
55417
01fbfb60c33e
adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
blanchet
parents:
53015
diff
changeset
|
166 |
@{thm fst_conv[of _ DUMMY]} is produced by |
16395 | 167 |
\begin{quote} |
55417
01fbfb60c33e
adapted to 'xxx_{case,rec}' renaming, to new theorem names, and to new variable names in theorems
blanchet
parents:
53015
diff
changeset
|
168 |
\verb!@!\verb!{thm fst_conv[of _ DUMMY]}! |
16395 | 169 |
\end{quote} |
36138
1faa0fc34174
advertise [rename_abs] attribute in LaTeXsugar -- wish I had known about this earier.
krauss
parents:
34890
diff
changeset
|
170 |
Variables that are bound by quantifiers or lambdas cannot be renamed |
1faa0fc34174
advertise [rename_abs] attribute in LaTeXsugar -- wish I had known about this earier.
krauss
parents:
34890
diff
changeset
|
171 |
like this. Instead, the attribute \texttt{rename\_abs} does the |
1faa0fc34174
advertise [rename_abs] attribute in LaTeXsugar -- wish I had known about this earier.
krauss
parents:
34890
diff
changeset
|
172 |
job. It expects a list of names or underscores, similar to the |
1faa0fc34174
advertise [rename_abs] attribute in LaTeXsugar -- wish I had known about this earier.
krauss
parents:
34890
diff
changeset
|
173 |
\texttt{of} attribute: |
1faa0fc34174
advertise [rename_abs] attribute in LaTeXsugar -- wish I had known about this earier.
krauss
parents:
34890
diff
changeset
|
174 |
\begin{quote} |
1faa0fc34174
advertise [rename_abs] attribute in LaTeXsugar -- wish I had known about this earier.
krauss
parents:
34890
diff
changeset
|
175 |
\verb!@!\verb!{thm split_paired_All[rename_abs _ l r]}! |
1faa0fc34174
advertise [rename_abs] attribute in LaTeXsugar -- wish I had known about this earier.
krauss
parents:
34890
diff
changeset
|
176 |
\end{quote} |
1faa0fc34174
advertise [rename_abs] attribute in LaTeXsugar -- wish I had known about this earier.
krauss
parents:
34890
diff
changeset
|
177 |
produces @{thm split_paired_All[rename_abs _ l r]}. |
49239 | 178 |
|
16395 | 179 |
|
49239 | 180 |
\subsection{Inference rules} |
15337 | 181 |
|
49239 | 182 |
To print theorems as inference rules you need to include Didier |
58620 | 183 |
R\'emy's \texttt{mathpartir} package~@{cite mathpartir} |
15342 | 184 |
for typesetting inference rules in your \LaTeX\ file. |
15337 | 185 |
|
15689 | 186 |
Writing \verb!@!\verb!{thm[mode=Rule] conjI}! produces |
187 |
@{thm[mode=Rule] conjI}, even in the middle of a sentence. |
|
15342 | 188 |
If you prefer your inference rule on a separate line, maybe with a name, |
189 |
\begin{center} |
|
15689 | 190 |
@{thm[mode=Rule] conjI} {\sc conjI} |
15342 | 191 |
\end{center} |
192 |
is produced by |
|
15337 | 193 |
\begin{quote} |
194 |
\verb!\begin{center}!\\ |
|
15689 | 195 |
\verb!@!\verb!{thm[mode=Rule] conjI} {\sc conjI}!\\ |
15337 | 196 |
\verb!\end{center}! |
197 |
\end{quote} |
|
24497 | 198 |
It is not recommended to use the standard \texttt{display} option |
15342 | 199 |
together with \texttt{Rule} because centering does not work and because |
200 |
the line breaking mechanisms of \texttt{display} and \texttt{mathpartir} can |
|
201 |
clash. |
|
202 |
||
15337 | 203 |
Of course you can display multiple rules in this fashion: |
204 |
\begin{quote} |
|
24497 | 205 |
\verb!\begin{center}!\\ |
15689 | 206 |
\verb!@!\verb!{thm[mode=Rule] conjI} {\sc conjI} \\[1ex]!\\ |
207 |
\verb!@!\verb!{thm[mode=Rule] conjE} {\sc disjI$_1$} \qquad!\\ |
|
208 |
\verb!@!\verb!{thm[mode=Rule] disjE} {\sc disjI$_2$}!\\ |
|
15337 | 209 |
\verb!\end{center}! |
210 |
\end{quote} |
|
211 |
yields |
|
24497 | 212 |
\begin{center}\small |
15689 | 213 |
@{thm[mode=Rule] conjI} {\sc conjI} \\[1ex] |
214 |
@{thm[mode=Rule] disjI1} {\sc disjI$_1$} \qquad |
|
215 |
@{thm[mode=Rule] disjI2} {\sc disjI$_2$} |
|
15337 | 216 |
\end{center} |
217 |
||
15342 | 218 |
The \texttt{mathpartir} package copes well if there are too many |
219 |
premises for one line: |
|
220 |
\begin{center} |
|
221 |
@{prop[mode=Rule] "\<lbrakk> A \<longrightarrow> B; B \<longrightarrow> C; C \<longrightarrow> D; D \<longrightarrow> E; E \<longrightarrow> F; F \<longrightarrow> G; |
|
222 |
G \<longrightarrow> H; H \<longrightarrow> I; I \<longrightarrow> J; J \<longrightarrow> K \<rbrakk> \<Longrightarrow> A \<longrightarrow> K"} |
|
223 |
\end{center} |
|
224 |
||
15471 | 225 |
Limitations: 1. Premises and conclusion must each not be longer than |
226 |
the line. 2. Premises that are @{text"\<Longrightarrow>"}-implications are again |
|
227 |
displayed with a horizontal line, which looks at least unusual. |
|
228 |
||
22329 | 229 |
|
230 |
In case you print theorems without premises no rule will be printed by the |
|
231 |
\texttt{Rule} print mode. However, you can use \texttt{Axiom} instead: |
|
232 |
\begin{quote} |
|
24497 | 233 |
\verb!\begin{center}!\\ |
22329 | 234 |
\verb!@!\verb!{thm[mode=Axiom] refl} {\sc refl}! \\ |
235 |
\verb!\end{center}! |
|
236 |
\end{quote} |
|
237 |
yields |
|
24497 | 238 |
\begin{center} |
22329 | 239 |
@{thm[mode=Axiom] refl} {\sc refl} |
240 |
\end{center} |
|
49239 | 241 |
|
15342 | 242 |
|
49239 | 243 |
\subsection{Displays and font sizes} |
24497 | 244 |
|
49239 | 245 |
When displaying theorems with the \texttt{display} option, for example as in |
24497 | 246 |
\verb!@!\verb!{thm[display] refl}! @{thm[display] refl} the theorem is |
247 |
set in small font. It uses the \LaTeX-macro \verb!\isastyle!, |
|
248 |
which is also the style that regular theory text is set in, e.g. *} |
|
249 |
||
250 |
lemma "t = t" |
|
251 |
(*<*)oops(*>*) |
|
252 |
||
253 |
text{* \noindent Otherwise \verb!\isastyleminor! is used, |
|
254 |
which does not modify the font size (assuming you stick to the default |
|
255 |
\verb!\isabellestyle{it}! in \texttt{root.tex}). If you prefer |
|
256 |
normal font size throughout your text, include |
|
257 |
\begin{quote} |
|
258 |
\verb!\renewcommand{\isastyle}{\isastyleminor}! |
|
259 |
\end{quote} |
|
260 |
in \texttt{root.tex}. On the other hand, if you like the small font, |
|
261 |
just put \verb!\isastyle! in front of the text in question, |
|
262 |
e.g.\ at the start of one of the center-environments above. |
|
263 |
||
264 |
The advantage of the display option is that you can display a whole |
|
265 |
list of theorems in one go. For example, |
|
46187
f009e0fe8643
updated example -- List.foldl is no longer defined via primrec;
wenzelm
parents:
42669
diff
changeset
|
266 |
\verb!@!\verb!{thm[display] append.simps}! |
f009e0fe8643
updated example -- List.foldl is no longer defined via primrec;
wenzelm
parents:
42669
diff
changeset
|
267 |
generates @{thm[display] append.simps} |
49239 | 268 |
|
24497 | 269 |
|
49239 | 270 |
\subsection{If-then} |
15342 | 271 |
|
49239 | 272 |
If you prefer a fake ``natural language'' style you can produce |
15342 | 273 |
the body of |
274 |
\newtheorem{theorem}{Theorem} |
|
275 |
\begin{theorem} |
|
15689 | 276 |
@{thm[mode=IfThen] le_trans} |
15342 | 277 |
\end{theorem} |
278 |
by typing |
|
279 |
\begin{quote} |
|
15689 | 280 |
\verb!@!\verb!{thm[mode=IfThen] le_trans}! |
15342 | 281 |
\end{quote} |
282 |
||
283 |
In order to prevent odd line breaks, the premises are put into boxes. |
|
284 |
At times this is too drastic: |
|
285 |
\begin{theorem} |
|
286 |
@{prop[mode=IfThen] "longpremise \<Longrightarrow> longerpremise \<Longrightarrow> P(f(f(f(f(f(f(f(f(f(x)))))))))) \<Longrightarrow> longestpremise \<Longrightarrow> conclusion"} |
|
287 |
\end{theorem} |
|
16153 | 288 |
In which case you should use \texttt{IfThenNoBox} instead of |
289 |
\texttt{IfThen}: |
|
15342 | 290 |
\begin{theorem} |
291 |
@{prop[mode=IfThenNoBox] "longpremise \<Longrightarrow> longerpremise \<Longrightarrow> P(f(f(f(f(f(f(f(f(f(x)))))))))) \<Longrightarrow> longestpremise \<Longrightarrow> conclusion"} |
|
292 |
\end{theorem} |
|
49239 | 293 |
|
15342 | 294 |
|
49239 | 295 |
\subsection{Doing it yourself\label{sec:yourself}} |
16153 | 296 |
|
49239 | 297 |
If for some reason you want or need to present theorems your |
16153 | 298 |
own way, you can extract the premises and the conclusion explicitly |
299 |
and combine them as you like: |
|
300 |
\begin{itemize} |
|
32891 | 301 |
\item \verb!@!\verb!{thm (prem 1)! $thm$\verb!}! |
302 |
prints premise 1 of $thm$. |
|
303 |
\item \verb!@!\verb!{thm (concl)! $thm$\verb!}! |
|
16153 | 304 |
prints the conclusion of $thm$. |
305 |
\end{itemize} |
|
32891 | 306 |
For example, ``from @{thm (prem 2) conjI} and |
307 |
@{thm (prem 1) conjI} we conclude @{thm (concl) conjI}'' |
|
16153 | 308 |
is produced by |
309 |
\begin{quote} |
|
32891 | 310 |
\verb!from !\verb!@!\verb!{thm (prem 2) conjI}! \verb!and !\verb!@!\verb!{thm (prem 1) conjI}!\\ |
311 |
\verb!we conclude !\verb!@!\verb!{thm (concl) conjI}! |
|
16153 | 312 |
\end{quote} |
313 |
Thus you can rearrange or hide premises and typeset the theorem as you like. |
|
32898
e871d897969c
term styles also cover antiquotations term_type and typeof
haftmann
parents:
32891
diff
changeset
|
314 |
Styles like \verb!(prem 1)! are a general mechanism explained |
16153 | 315 |
in \S\ref{sec:styles}. |
49239 | 316 |
|
317 |
||
318 |
\subsection{Patterns} |
|
319 |
||
320 |
||
321 |
In \S\ref{sec:varnames} we shows how to create patterns containing ``@{term DUMMY}''. |
|
322 |
You can drive this game even further and extend the syntax of let |
|
323 |
bindings such that certain functions like @{term fst}, @{term hd}, |
|
324 |
etc.\ are printed as patterns. \texttt{OptionalSugar} provides the following: |
|
16153 | 325 |
|
49239 | 326 |
\begin{center} |
327 |
\begin{tabular}{l@ {~~produced by~~}l} |
|
328 |
@{term "let x = fst p in t"} & \verb!@!\verb!{term "let x = fst p in t"}!\\ |
|
329 |
@{term "let x = snd p in t"} & \verb!@!\verb!{term "let x = snd p in t"}!\\ |
|
330 |
@{term "let x = hd xs in t"} & \verb!@!\verb!{term "let x = hd xs in t"}!\\ |
|
331 |
@{term "let x = tl xs in t"} & \verb!@!\verb!{term "let x = tl xs in t"}!\\ |
|
332 |
@{term "let x = the y in t"} & \verb!@!\verb!{term "let x = the y in t"}!\\ |
|
333 |
\end{tabular} |
|
334 |
\end{center} |
|
335 |
||
336 |
||
337 |
\section {Styles\label{sec:styles}} |
|
15366 | 338 |
|
49239 | 339 |
The \verb!thm! antiquotation works nicely for single theorems, but |
340 |
sets of equations as used in definitions are more difficult to |
|
341 |
typeset nicely: people tend to prefer aligned @{text "="} signs. |
|
342 |
||
343 |
To deal with such cases where it is desirable to dive into the structure |
|
344 |
of terms and theorems, Isabelle offers antiquotations featuring ``styles'': |
|
345 |
||
346 |
\begin{quote} |
|
347 |
\verb!@!\verb!{thm (style) thm}!\\ |
|
348 |
\verb!@!\verb!{prop (style) thm}!\\ |
|
349 |
\verb!@!\verb!{term (style) term}!\\ |
|
350 |
\verb!@!\verb!{term_type (style) term}!\\ |
|
351 |
\verb!@!\verb!{typeof (style) term}!\\ |
|
352 |
\end{quote} |
|
15366 | 353 |
|
49239 | 354 |
A ``style'' is a transformation of a term. There are predefined |
355 |
styles, namely \verb!lhs! and \verb!rhs!, \verb!prem! with one argument, and \verb!concl!. |
|
356 |
For example, the output |
|
357 |
\begin{center} |
|
358 |
\begin{tabular}{l@ {~~@{text "="}~~}l} |
|
359 |
@{thm (lhs) append_Nil} & @{thm (rhs) append_Nil}\\ |
|
360 |
@{thm (lhs) append_Cons} & @{thm (rhs) append_Cons} |
|
361 |
\end{tabular} |
|
362 |
\end{center} |
|
363 |
is produced by the following code: |
|
364 |
\begin{quote} |
|
365 |
\verb!\begin{center}!\\ |
|
366 |
\verb!\begin{tabular}{l@ {~~!\verb!@!\verb!{text "="}~~}l}!\\ |
|
367 |
\verb!@!\verb!{thm (lhs) append_Nil} & @!\verb!{thm (rhs) append_Nil}\\!\\ |
|
368 |
\verb!@!\verb!{thm (lhs) append_Cons} & @!\verb!{thm (rhs) append_Cons}!\\ |
|
369 |
\verb!\end{tabular}!\\ |
|
370 |
\verb!\end{center}! |
|
371 |
\end{quote} |
|
372 |
Note the space between \verb!@! and \verb!{! in the tabular argument. |
|
373 |
It prevents Isabelle from interpreting \verb!@ {~~...~~}! |
|
374 |
as an antiquotation. The styles \verb!lhs! and \verb!rhs! |
|
375 |
extract the left hand side (or right hand side respectively) from the |
|
376 |
conclusion of propositions consisting of a binary operator |
|
377 |
(e.~g.~@{text "="}, @{text "\<equiv>"}, @{text "<"}). |
|
15366 | 378 |
|
49239 | 379 |
Likewise, \verb!concl! may be used as a style to show just the |
380 |
conclusion of a proposition. For example, take \verb!hd_Cons_tl!: |
|
381 |
\begin{center} |
|
382 |
@{thm hd_Cons_tl} |
|
383 |
\end{center} |
|
384 |
To print just the conclusion, |
|
385 |
\begin{center} |
|
386 |
@{thm (concl) hd_Cons_tl} |
|
387 |
\end{center} |
|
388 |
type |
|
389 |
\begin{quote} |
|
390 |
\verb!\begin{center}!\\ |
|
391 |
\verb!@!\verb!{thm (concl) hd_Cons_tl}!\\ |
|
392 |
\verb!\end{center}! |
|
393 |
\end{quote} |
|
394 |
Beware that any options must be placed \emph{before} the style, as in this example. |
|
15366 | 395 |
|
49239 | 396 |
Further use cases can be found in \S\ref{sec:yourself}. |
397 |
If you are not afraid of ML, you may also define your own styles. |
|
55837 | 398 |
Have a look at module @{ML_structure Term_Style}. |
49239 | 399 |
|
400 |
||
401 |
\section {Proofs} |
|
402 |
||
403 |
Full proofs, even if written in beautiful Isar style, are |
|
24497 | 404 |
likely to be too long and detailed to be included in conference |
405 |
papers, but some key lemmas might be of interest. |
|
406 |
It is usually easiest to put them in figures like the one in Fig.\ |
|
407 |
\ref{fig:proof}. This was achieved with the \isakeyword{text\_raw} command: |
|
15366 | 408 |
*} |
409 |
text_raw {* |
|
410 |
\begin{figure} |
|
411 |
\begin{center}\begin{minipage}{0.6\textwidth} |
|
24497 | 412 |
\isastyleminor\isamarkuptrue |
15366 | 413 |
*} |
414 |
lemma True |
|
415 |
proof - |
|
416 |
-- "pretty trivial" |
|
417 |
show True by force |
|
418 |
qed |
|
15428 | 419 |
text_raw {* |
15366 | 420 |
\end{minipage}\end{center} |
421 |
\caption{Example proof in a figure.}\label{fig:proof} |
|
422 |
\end{figure} |
|
423 |
*} |
|
424 |
text {* |
|
425 |
||
426 |
\begin{quote} |
|
427 |
\small |
|
428 |
\verb!text_raw {!\verb!*!\\ |
|
429 |
\verb! \begin{figure}!\\ |
|
430 |
\verb! \begin{center}\begin{minipage}{0.6\textwidth}!\\ |
|
24497 | 431 |
\verb! \isastyleminor\isamarkuptrue!\\ |
15366 | 432 |
\verb!*!\verb!}!\\ |
433 |
\verb!lemma True!\\ |
|
434 |
\verb!proof -!\\ |
|
435 |
\verb! -- "pretty trivial"!\\ |
|
436 |
\verb! show True by force!\\ |
|
437 |
\verb!qed!\\ |
|
438 |
\verb!text_raw {!\verb!*!\\ |
|
439 |
\verb! \end{minipage}\end{center}!\\ |
|
440 |
\verb! \caption{Example proof in a figure.}\label{fig:proof}!\\ |
|
441 |
\verb! \end{figure}!\\ |
|
442 |
\verb!*!\verb!}! |
|
443 |
\end{quote} |
|
24497 | 444 |
|
445 |
Other theory text, e.g.\ definitions, can be put in figures, too. |
|
15342 | 446 |
|
49239 | 447 |
\section{Theory snippets} |
15917
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
448 |
|
49239 | 449 |
This section describes how to include snippets of a theory text in some other \LaTeX\ document. |
450 |
The typical scenario is that the description of your theory is not part of the theory text but |
|
451 |
a separate document that antiquotes bits of the theory. This works well for terms and theorems |
|
452 |
but there are no antiquotations, for example, for function definitions or proofs. Even if there are antiquotations, |
|
453 |
the output is usually a reformatted (by Isabelle) version of the input and may not look like |
|
454 |
you wanted it to look. Here is how to include a snippet of theory text (in \LaTeX\ form) in some |
|
455 |
other \LaTeX\ document, in 4 easy steps. Beware that these snippets are not processed by |
|
456 |
any antiquotation mechanism: the resulting \LaTeX\ text is more or less exactly what you wrote |
|
457 |
in the theory, without any added sugar. |
|
15917
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
458 |
|
49239 | 459 |
\subsection{Theory markup} |
15917
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
460 |
|
49239 | 461 |
Include some markers at the beginning and the end of the theory snippet you want to cut out. |
462 |
You have to place the following lines before and after the snippet, where snippets must always be |
|
463 |
consecutive lines of theory text: |
|
464 |
\begin{quote} |
|
465 |
\verb!\text_raw{!\verb!*\snip{!\emph{snippetname}\verb!}{1}{2}{%*!\verb!}!\\ |
|
466 |
\emph{theory text}\\ |
|
467 |
\verb!\text_raw{!\verb!*!\verb!}%endsnip*!\verb!}! |
|
468 |
\end{quote} |
|
469 |
where \emph{snippetname} should be a unique name for the snippet. The numbers \texttt{1} |
|
470 |
and \texttt{2} are explained in a moment. |
|
471 |
||
472 |
\subsection{Generate the \texttt{.tex} file} |
|
15917
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
473 |
|
49239 | 474 |
Run your theory \texttt{T} with the \texttt{isabelle} \texttt{build} tool |
475 |
to generate the \LaTeX-file \texttt{T.tex} which is needed for the next step, |
|
476 |
extraction of marked snippets. |
|
477 |
You may also want to process \texttt{T.tex} to generate a pdf document. |
|
478 |
This requires a definition of \texttt{\char`\\snippet}: |
|
479 |
\begin{verbatim} |
|
480 |
\newcommand{\repeatisanl}[1] |
|
481 |
{\ifnum#1=0\else\isanewline\repeatisanl{\numexpr#1-1}\fi} |
|
482 |
\newcommand{\snip}[4]{\repeatisanl#2#4\repeatisanl#3} |
|
483 |
\end{verbatim} |
|
484 |
Parameter 2 and 3 of \texttt{\char`\\snippet} are numbers (the \texttt{1} |
|
485 |
and \texttt{2} above) and determine how many newlines are inserted before and after the snippet. |
|
486 |
Unfortunately \texttt{text\_raw} eats up all preceding and following newlines |
|
487 |
and they have to be inserted again in this manner. Otherwise the document generated from \texttt{T.tex} |
|
488 |
will look ugly around the snippets. It can take some iterations to get the number of required |
|
489 |
newlines exactly right. |
|
490 |
||
491 |
\subsection{Extract marked snippets} |
|
492 |
\label{subsec:extract} |
|
15917
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
493 |
|
49239 | 494 |
Extract the marked bits of text with a shell-level script, e.g. |
495 |
\begin{quote} |
|
496 |
\verb!sed -n '/\\snip{/,/endsnip/p' T.tex > !\emph{snippets}\verb!.tex! |
|
497 |
\end{quote} |
|
498 |
File \emph{snippets}\texttt{.tex} (the name is arbitrary) now contains a sequence of blocks like this |
|
499 |
\begin{quote} |
|
500 |
\verb!\snip{!\emph{snippetname}\verb!}{1}{2}{%!\\ |
|
501 |
\emph{theory text}\\ |
|
502 |
\verb!}%endsnip! |
|
503 |
\end{quote} |
|
504 |
||
505 |
\subsection{Including snippets} |
|
17031
ffa73448025e
added hint for position of aqu options in connection with styles
haftmann
parents:
16395
diff
changeset
|
506 |
|
49239 | 507 |
In the preamble of the document where the snippets are to be used you define \texttt{\char`\\snip} |
508 |
and input \emph{snippets}\texttt{.tex}: |
|
509 |
\begin{verbatim} |
|
510 |
\newcommand{\snip}[4] |
|
511 |
{\expandafter\newcommand\csname #1\endcsname{#4}} |
|
512 |
\input{snippets} |
|
513 |
\end{verbatim} |
|
514 |
This definition of \texttt{\char`\\snip} simply has the effect of defining for each snippet |
|
515 |
\emph{snippetname} a \LaTeX\ command \texttt{\char`\\}\emph{snippetname} |
|
516 |
that produces the corresponding snippet text. In the body of your document you can display that text |
|
517 |
like this: |
|
518 |
\begin{quote} |
|
519 |
\verb!\begin{isabelle}!\\ |
|
520 |
\texttt{\char`\\}\emph{snippetname}\\ |
|
521 |
\verb!\end{isabelle}! |
|
522 |
\end{quote} |
|
523 |
The \texttt{isabelle} environment is the one defined in the standard file |
|
524 |
\texttt{isabelle.sty} which most likely you are loading anyway. |
|
49628 | 525 |
|
526 |
||
527 |
\section{Antiquotation} |
|
528 |
||
529 |
You want to show a constant and its type? Instead of going |
|
530 |
\verb!@!\verb!{const myconst}! \verb!@!\verb!{text "::"}! \verb!@!\verb!{typeof myconst}!, |
|
531 |
you can just write \verb!@!\verb!{const_typ myconst}! using the new antiquotation |
|
532 |
\texttt{const\_typ} defined in \texttt{LaTeXsugar}. For example, |
|
533 |
\verb!@!\verb!{const_typ length}! produces @{const_typ length}. |
|
534 |
||
15917
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
535 |
*} |
cd4983c76548
Added short description of thm_style and term_style antiquotation
haftmann
parents:
15689
diff
changeset
|
536 |
|
15337 | 537 |
(*<*) |
538 |
end |
|
16175 | 539 |
(*>*) |