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