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