doc-src/LaTeXsugar/Sugar/Sugar.thy
author schirmer
Fri Feb 16 11:01:16 2007 +0100 (2007-02-16)
changeset 22329 e4325ce4e0c4
parent 21558 63278052bb72
child 22834 bf67f798f063
permissions -rw-r--r--
added example for print-mode Axiom
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@15342
    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@15337
    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@15342
    74
\item @{term"{}"} instead of @{text"{}"}.
nipkow@15342
    75
\item @{term"insert a (insert b (insert c M))"} instead of @{text"insert a (insert b (insert c M))"}.
nipkow@15342
    76
\end{itemize}
nipkow@15342
    77
*}
nipkow@15342
    78
nipkow@15342
    79
subsection{* Lists *}
nipkow@15342
    80
nipkow@15342
    81
text{* If lists are used heavily, the following notations increase readability:
nipkow@15342
    82
\begin{itemize}
nipkow@15342
    83
\item @{term"x # xs"} instead of @{text"x # xs"}.
nipkow@15342
    84
      Exceptionally, @{term"x # xs"} is also input syntax.
nipkow@15342
    85
If you prefer more space around the $\cdot$ you have to redefine
nipkow@15342
    86
\verb!\isasymcdot! in \LaTeX:
nipkow@15342
    87
\verb!\renewcommand{\isasymcdot}{\isamath{\,\cdot\,}}!
nipkow@15342
    88
nipkow@15342
    89
\item @{term"length xs"} instead of @{text"length xs"}.
kleing@15385
    90
\item @{term"nth xs n"} instead of @{text"nth xs n"},
nipkow@15342
    91
      the $n$th element of @{text xs}.
nipkow@15342
    92
kleing@15366
    93
\item The @{text"@"} operation associates implicitly to the right,
kleing@15366
    94
which leads to unpleasant line breaks if the term is too long for one
kleing@15366
    95
line. To avoid this, \texttt{OptionalSugar} contains syntax to group
kleing@15366
    96
@{text"@"}-terms to the left before printing, which leads to better
kleing@15366
    97
line breaking behaviour:
wenzelm@15673
    98
@{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
    99
nipkow@15342
   100
\end{itemize}
nipkow@15337
   101
*}
nipkow@15337
   102
nipkow@15337
   103
section "Printing theorems"
nipkow@15337
   104
nipkow@15689
   105
subsection "Question marks"
nipkow@15689
   106
nipkow@15689
   107
text{* If you print anything, especially theorems, containing
nipkow@15689
   108
schematic variables they are prefixed with a question mark:
nipkow@15689
   109
\verb!@!\verb!{thm conjI}! results in @{thm conjI}. Most of the time
nipkow@15689
   110
you would rather not see the question marks. There is an attribute
nipkow@15689
   111
\verb!no_vars! that you can attach to the theorem that turns its
nipkow@15689
   112
schematic into ordinary free variables: \verb!@!\verb!{thm conjI[no_vars]}!
nipkow@15689
   113
results in @{thm conjI[no_vars]}.
nipkow@15689
   114
nipkow@15689
   115
This \verb!no_vars! business can become a bit tedious.
nipkow@15689
   116
If you would rather never see question marks, simply put
nipkow@15689
   117
\begin{verbatim}
wenzelm@15983
   118
reset show_question_marks;
nipkow@15689
   119
\end{verbatim}
nipkow@15689
   120
at the beginning of your file \texttt{ROOT.ML}.
nipkow@15689
   121
The rest of this document is produced with this flag reset.
nipkow@16075
   122
nipkow@16075
   123
Hint: Resetting \verb!show_question_marks! only supresses question
nipkow@16075
   124
marks; variables that end in digits, e.g. @{text"x1"}, are still
nipkow@16075
   125
printed with a trailing @{text".0"}, e.g. @{text"x1.0"}, their
nipkow@16075
   126
internal index. This can be avoided by turning the last digit into a
nipkow@16075
   127
subscript: write \verb!x\<^isub>1! and obtain the much nicer @{text"x\<^isub>1"}. *}
nipkow@15689
   128
wenzelm@15983
   129
(*<*)ML"reset show_question_marks"(*>*)
nipkow@15689
   130
nipkow@17127
   131
subsection {*Variable names\label{sec:varnames}*}
nipkow@16395
   132
nipkow@16395
   133
text{* It sometimes happens that you want to change the name of a
nipkow@16395
   134
variable in a theorem before printing it. This can easily be achieved
nipkow@16395
   135
with the help of Isabelle's instantiation attribute \texttt{where}:
nipkow@16395
   136
@{thm conjI[where P = \<phi> and Q = \<psi>]} is the result of
nipkow@16395
   137
\begin{quote}
nipkow@16395
   138
\verb!@!\verb!{thm conjI[where P = \<phi> and Q = \<psi>]}!
nipkow@16395
   139
\end{quote}
nipkow@16395
   140
To support the ``\_''-notation for irrelevant variables
nipkow@16395
   141
the constant \texttt{DUMMY} has been introduced:
nipkow@16395
   142
@{thm fst_conv[where b = DUMMY]} is produced by
nipkow@16395
   143
\begin{quote}
nipkow@16395
   144
\verb!@!\verb!{thm fst_conv[where b = DUMMY]}!
nipkow@16395
   145
\end{quote}
nipkow@16395
   146
*}
nipkow@16395
   147
nipkow@15337
   148
subsection "Inference rules"
nipkow@15337
   149
nipkow@15342
   150
text{* To print theorems as inference rules you need to include Didier
nipkow@15342
   151
R\'emy's \texttt{mathpartir} package~\cite{mathpartir}
nipkow@15342
   152
for typesetting inference rules in your \LaTeX\ file.
nipkow@15337
   153
nipkow@15689
   154
Writing \verb!@!\verb!{thm[mode=Rule] conjI}! produces
nipkow@15689
   155
@{thm[mode=Rule] conjI}, even in the middle of a sentence.
nipkow@15342
   156
If you prefer your inference rule on a separate line, maybe with a name,
nipkow@15342
   157
\begin{center}
nipkow@15689
   158
@{thm[mode=Rule] conjI} {\sc conjI}
nipkow@15342
   159
\end{center}
nipkow@15342
   160
is produced by
nipkow@15337
   161
\begin{quote}
nipkow@15337
   162
\verb!\begin{center}!\\
nipkow@15689
   163
\verb!@!\verb!{thm[mode=Rule] conjI} {\sc conjI}!\\
nipkow@15337
   164
\verb!\end{center}!
nipkow@15337
   165
\end{quote}
nipkow@15342
   166
It is not recommended to use the standard \texttt{display} attribute
nipkow@15342
   167
together with \texttt{Rule} because centering does not work and because
nipkow@15342
   168
the line breaking mechanisms of \texttt{display} and \texttt{mathpartir} can
nipkow@15342
   169
clash.
nipkow@15342
   170
nipkow@15337
   171
Of course you can display multiple rules in this fashion:
nipkow@15337
   172
\begin{quote}
nipkow@15337
   173
\verb!\begin{center}\isastyle!\\
nipkow@15689
   174
\verb!@!\verb!{thm[mode=Rule] conjI} {\sc conjI} \\[1ex]!\\
nipkow@15689
   175
\verb!@!\verb!{thm[mode=Rule] conjE} {\sc disjI$_1$} \qquad!\\
nipkow@15689
   176
\verb!@!\verb!{thm[mode=Rule] disjE} {\sc disjI$_2$}!\\
nipkow@15337
   177
\verb!\end{center}!
nipkow@15337
   178
\end{quote}
nipkow@15337
   179
yields
nipkow@15337
   180
\begin{center}\isastyle
nipkow@15689
   181
@{thm[mode=Rule] conjI} {\sc conjI} \\[1ex]
nipkow@15689
   182
@{thm[mode=Rule] disjI1} {\sc disjI$_1$} \qquad
nipkow@15689
   183
@{thm[mode=Rule] disjI2} {\sc disjI$_2$}
nipkow@15337
   184
\end{center}
nipkow@15337
   185
Note that we included \verb!\isastyle! to obtain
nipkow@15337
   186
the smaller font that otherwise comes only with \texttt{display}.
nipkow@15337
   187
nipkow@15342
   188
The \texttt{mathpartir} package copes well if there are too many
nipkow@15342
   189
premises for one line:
nipkow@15342
   190
\begin{center}
nipkow@15342
   191
@{prop[mode=Rule] "\<lbrakk> A \<longrightarrow> B; B \<longrightarrow> C; C \<longrightarrow> D; D \<longrightarrow> E; E \<longrightarrow> F; F \<longrightarrow> G;
nipkow@15342
   192
 G \<longrightarrow> H; H \<longrightarrow> I; I \<longrightarrow> J; J \<longrightarrow> K \<rbrakk> \<Longrightarrow> A \<longrightarrow> K"}
nipkow@15342
   193
\end{center}
nipkow@15342
   194
nipkow@15471
   195
Limitations: 1. Premises and conclusion must each not be longer than
nipkow@15471
   196
the line.  2. Premises that are @{text"\<Longrightarrow>"}-implications are again
nipkow@15471
   197
displayed with a horizontal line, which looks at least unusual.
nipkow@15471
   198
schirmer@22329
   199
schirmer@22329
   200
In case you print theorems without premises no rule will be printed by the
schirmer@22329
   201
\texttt{Rule} print mode. However, you can use \texttt{Axiom} instead:
schirmer@22329
   202
\begin{quote}
schirmer@22329
   203
\verb!\begin{center}\isastyle!\\
schirmer@22329
   204
\verb!@!\verb!{thm[mode=Axiom] refl} {\sc refl}! \\
schirmer@22329
   205
\verb!\end{center}!
schirmer@22329
   206
\end{quote}
schirmer@22329
   207
yields
schirmer@22329
   208
\begin{center}\isastyle
schirmer@22329
   209
@{thm[mode=Axiom] refl} {\sc refl} 
schirmer@22329
   210
\end{center}
schirmer@22329
   211
schirmer@22329
   212
schirmer@22329
   213
nipkow@15337
   214
*}
nipkow@15342
   215
nipkow@15342
   216
subsection{*If-then*}
nipkow@15342
   217
nipkow@15342
   218
text{* If you prefer a fake ``natural language'' style you can produce
nipkow@15342
   219
the body of
nipkow@15342
   220
\newtheorem{theorem}{Theorem}
nipkow@15342
   221
\begin{theorem}
nipkow@15689
   222
@{thm[mode=IfThen] le_trans}
nipkow@15342
   223
\end{theorem}
nipkow@15342
   224
by typing
nipkow@15342
   225
\begin{quote}
nipkow@15689
   226
\verb!@!\verb!{thm[mode=IfThen] le_trans}!
nipkow@15342
   227
\end{quote}
nipkow@15342
   228
nipkow@15342
   229
In order to prevent odd line breaks, the premises are put into boxes.
nipkow@15342
   230
At times this is too drastic:
nipkow@15342
   231
\begin{theorem}
nipkow@15342
   232
@{prop[mode=IfThen] "longpremise \<Longrightarrow> longerpremise \<Longrightarrow> P(f(f(f(f(f(f(f(f(f(x)))))))))) \<Longrightarrow> longestpremise \<Longrightarrow> conclusion"}
nipkow@15342
   233
\end{theorem}
nipkow@16153
   234
In which case you should use \texttt{IfThenNoBox} instead of
nipkow@16153
   235
\texttt{IfThen}:
nipkow@15342
   236
\begin{theorem}
nipkow@15342
   237
@{prop[mode=IfThenNoBox] "longpremise \<Longrightarrow> longerpremise \<Longrightarrow> P(f(f(f(f(f(f(f(f(f(x)))))))))) \<Longrightarrow> longestpremise \<Longrightarrow> conclusion"}
nipkow@15342
   238
\end{theorem}
kleing@15366
   239
*}
nipkow@15342
   240
haftmann@16166
   241
subsection{* Doing it yourself\label{sec:yourself}*}
nipkow@16153
   242
nipkow@16153
   243
text{* If for some reason you want or need to present theorems your
nipkow@16153
   244
own way, you can extract the premises and the conclusion explicitly
nipkow@16153
   245
and combine them as you like:
nipkow@16153
   246
\begin{itemize}
haftmann@16167
   247
\item \verb!@!\verb!{thm_style prem1! $thm$\verb!}!
haftmann@16167
   248
prints premise 1 of $thm$ (and similarly up to \texttt{prem9}).
haftmann@16165
   249
\item \verb!@!\verb!{thm_style concl! $thm$\verb!}!
nipkow@16153
   250
prints the conclusion of $thm$.
nipkow@16153
   251
\end{itemize}
haftmann@16167
   252
For example, ``from @{thm_style prem2 conjI} and
haftmann@16167
   253
@{thm_style prem1 conjI} we conclude @{thm_style concl conjI}''
nipkow@16153
   254
is produced by
nipkow@16153
   255
\begin{quote}
nipkow@16175
   256
\verb!from !\verb!@!\verb!{thm_style prem2 conjI}! \verb!and !\verb!@!\verb!{thm_style prem1 conjI}!\\
haftmann@16165
   257
\verb!we conclude !\verb!@!\verb!{thm_style concl conjI}!
nipkow@16153
   258
\end{quote}
nipkow@16153
   259
Thus you can rearrange or hide premises and typeset the theorem as you like.
nipkow@16153
   260
The \verb!thm_style! antiquotation is a general mechanism explained
nipkow@16153
   261
in \S\ref{sec:styles}.
nipkow@16153
   262
*}
nipkow@16153
   263
kleing@15366
   264
subsection "Patterns"
kleing@15366
   265
kleing@15366
   266
text {*
kleing@15366
   267
nipkow@17127
   268
  In \S\ref{sec:varnames} we shows how to create patterns containing
nipkow@17127
   269
  ``@{term DUMMY}''.
kleing@15366
   270
  You can drive this game even further and extend the syntax of let
kleing@15366
   271
  bindings such that certain functions like @{term fst}, @{term hd}, 
kleing@15368
   272
  etc.\ are printed as patterns. \texttt{OptionalSugar} provides the
kleing@15368
   273
  following:
kleing@15366
   274
  
kleing@15366
   275
  \begin{center}
kleing@15366
   276
  \begin{tabular}{l@ {~~produced by~~}l}
kleing@15366
   277
  @{term "let x = fst p in t"} & \verb!@!\verb!{term "let x = fst p in t"}!\\
kleing@15366
   278
  @{term "let x = snd p in t"} & \verb!@!\verb!{term "let x = snd p in t"}!\\
kleing@15366
   279
  @{term "let x = hd xs in t"} & \verb!@!\verb!{term "let x = hd xs in t"}!\\
kleing@15366
   280
  @{term "let x = tl xs in t"} & \verb!@!\verb!{term "let x = tl xs in t"}!\\
kleing@15366
   281
  @{term "let x = the y in t"} & \verb!@!\verb!{term "let x = the y in t"}!\\
kleing@15366
   282
  \end{tabular}
kleing@15366
   283
  \end{center}
kleing@15366
   284
*}
kleing@15366
   285
nipkow@16155
   286
section "Proofs"
kleing@15366
   287
kleing@15366
   288
text {*
kleing@15367
   289
  Full proofs, even if written in beautiful Isar style, are likely to
kleing@15366
   290
  be too long and detailed to be included in conference papers, but
kleing@15366
   291
  some key lemmas might be of interest.
kleing@15366
   292
kleing@15366
   293
  It is usually easiest to put them in figures like the one in Fig.\
kleing@15366
   294
  \ref{fig:proof}. This was achieved with the \isakeyword{text\_raw}
kleing@15366
   295
  command:
kleing@15366
   296
*}
kleing@15366
   297
text_raw {*
kleing@15366
   298
  \begin{figure}
kleing@15366
   299
  \begin{center}\begin{minipage}{0.6\textwidth}  
kleing@15428
   300
  \isastyle\isamarkuptrue
kleing@15366
   301
*}
kleing@15366
   302
lemma True
kleing@15366
   303
proof -
kleing@15366
   304
  -- "pretty trivial"
kleing@15366
   305
  show True by force
kleing@15366
   306
qed
kleing@15428
   307
text_raw {*    
kleing@15366
   308
  \end{minipage}\end{center}
kleing@15366
   309
  \caption{Example proof in a figure.}\label{fig:proof}
kleing@15366
   310
  \end{figure}
kleing@15366
   311
*}
kleing@15366
   312
text {*
kleing@15366
   313
kleing@15366
   314
\begin{quote}
kleing@15366
   315
\small
kleing@15366
   316
\verb!text_raw {!\verb!*!\\
kleing@15366
   317
\verb!  \begin{figure}!\\
kleing@15366
   318
\verb!  \begin{center}\begin{minipage}{0.6\textwidth}!\\
kleing@15428
   319
\verb!  \isastyle\isamarkuptrue!\\
kleing@15366
   320
\verb!*!\verb!}!\\
kleing@15366
   321
\verb!lemma True!\\
kleing@15366
   322
\verb!proof -!\\
kleing@15366
   323
\verb!  -- "pretty trivial"!\\
kleing@15366
   324
\verb!  show True by force!\\
kleing@15366
   325
\verb!qed!\\
kleing@15366
   326
\verb!text_raw {!\verb!*!\\
kleing@15366
   327
\verb!  \end{minipage}\end{center}!\\
kleing@15366
   328
\verb!  \caption{Example proof in a figure.}\label{fig:proof}!\\
kleing@15366
   329
\verb!  \end{figure}!\\
kleing@15366
   330
\verb!*!\verb!}!
kleing@15366
   331
\end{quote}
kleing@15366
   332
  
nipkow@15342
   333
*}
nipkow@15342
   334
nipkow@16155
   335
section {*Styles\label{sec:styles}*}
haftmann@15917
   336
haftmann@15917
   337
text {*
nipkow@15953
   338
  The \verb!thm! antiquotation works nicely for single theorems, but
haftmann@15917
   339
  sets of equations as used in definitions are more difficult to
haftmann@16040
   340
  typeset nicely: people tend to prefer aligned @{text "="} signs.
haftmann@15917
   341
haftmann@15917
   342
  To deal with such cases where it is desirable to dive into the structure
haftmann@16040
   343
  of terms and theorems, Isabelle offers antiquotations featuring
haftmann@15917
   344
  ``styles'':
haftmann@15917
   345
haftmann@15917
   346
    \begin{quote}
haftmann@15917
   347
    \verb!@!\verb!{thm_style stylename thm}!\\
haftmann@15917
   348
    \verb!@!\verb!{term_style stylename term}!
haftmann@15917
   349
    \end{quote}
haftmann@15917
   350
haftmann@16040
   351
  A ``style'' is a transformation of propositions. There are predefined
webertj@21558
   352
  styles, namely \verb!lhs! and \verb!rhs!, \verb!prem1! up to \verb!prem9!, and \verb!concl!.
haftmann@16166
   353
  For example, 
kleing@16076
   354
  the output
haftmann@15917
   355
  \begin{center}
haftmann@15917
   356
  \begin{tabular}{l@ {~~@{text "="}~~}l}
haftmann@15917
   357
  @{thm_style lhs foldl_Nil} & @{thm_style rhs foldl_Nil}\\
haftmann@15917
   358
  @{thm_style lhs foldl_Cons} & @{thm_style rhs foldl_Cons}
haftmann@15917
   359
  \end{tabular}
haftmann@15917
   360
  \end{center}
haftmann@15917
   361
  is produced by the following code:
haftmann@15917
   362
  \begin{quote}
haftmann@15917
   363
    \verb!\begin{center}!\\
haftmann@15917
   364
    \verb!\begin{tabular}{l@ {~~!\verb!@!\verb!{text "="}~~}l}!\\
haftmann@15917
   365
    \verb!@!\verb!{thm_style lhs foldl_Nil} & @!\verb!{thm_style rhs foldl_Nil}!\\
haftmann@15917
   366
    \verb!@!\verb!{thm_style lhs foldl_Cons} & @!\verb!{thm_style rhs foldl_Cons}!\\
haftmann@15917
   367
    \verb!\end{tabular}!\\
haftmann@15917
   368
    \verb!\end{center}!
haftmann@15917
   369
  \end{quote}
haftmann@15917
   370
  Note the space between \verb!@! and \verb!{! in the tabular argument.
haftmann@15917
   371
  It prevents Isabelle from interpreting \verb!@ {~~...~~}! 
kleing@16076
   372
  as an antiquotation. The styles \verb!lhs! and \verb!rhs!
haftmann@16040
   373
  extract the left hand side (or right hand side respectivly) from the
kleing@16076
   374
  conclusion of propositions consisting of a binary operator
haftmann@16040
   375
  (e.~g.~@{text "="}, @{text "\<equiv>"}, @{text "<"}).
haftmann@15917
   376
haftmann@16165
   377
  Likewise, \verb!concl! may be used as a style to show just the
kleing@16076
   378
  conclusion of a proposition. For example, take \verb!hd_Cons_tl!:
haftmann@16040
   379
  \begin{center}
haftmann@17031
   380
    @{thm [show_types] hd_Cons_tl}
haftmann@16040
   381
  \end{center}
haftmann@16040
   382
  To print just the conclusion,
haftmann@15917
   383
  \begin{center}
haftmann@17031
   384
    @{thm_style [show_types] concl hd_Cons_tl}
haftmann@15917
   385
  \end{center}
haftmann@16040
   386
  type
haftmann@15917
   387
  \begin{quote}
haftmann@15917
   388
    \verb!\begin{center}!\\
haftmann@17031
   389
    \verb!@!\verb!{thm_style [show_types] concl hd_Cons_tl}!\\
haftmann@15917
   390
    \verb!\end{center}!
haftmann@15917
   391
  \end{quote}
nipkow@17127
   392
  Beware that any options must be placed \emph{before}
haftmann@17031
   393
  the name of the style, as in this example.
haftmann@17031
   394
haftmann@16166
   395
  Further use cases can be found in \S\ref{sec:yourself}.
haftmann@16166
   396
nipkow@15953
   397
  If you are not afraid of ML, you may also define your own styles.
haftmann@15960
   398
  A style is implemented by an ML function of type
haftmann@15960
   399
  \verb!Proof.context -> term -> term!.
haftmann@15960
   400
  Have a look at the following example:
haftmann@15960
   401
haftmann@16040
   402
*}
nipkow@16075
   403
(*<*)
haftmann@16040
   404
setup {*
haftmann@16040
   405
let
haftmann@16040
   406
  fun my_concl ctxt = Logic.strip_imp_concl
wenzelm@18708
   407
  in TermStyle.add_style "my_concl" my_concl
haftmann@16040
   408
end;
haftmann@16040
   409
*}
nipkow@16075
   410
(*>*)
haftmann@16040
   411
text {*
haftmann@16040
   412
haftmann@15917
   413
  \begin{quote}
haftmann@15917
   414
    \verb!setup {!\verb!*!\\
haftmann@15917
   415
    \verb!let!\\
haftmann@16040
   416
    \verb!  fun my_concl ctxt = Logic.strip_imp_concl!\\
wenzelm@18708
   417
    \verb!  in TermStyle.add_style "my_concl" my_concl!\\
haftmann@15917
   418
    \verb!end;!\\
haftmann@15917
   419
    \verb!*!\verb!}!\\
haftmann@15917
   420
  \end{quote}
haftmann@15960
   421
kleing@16076
   422
  \noindent
haftmann@16165
   423
  This example shows how the \verb!concl! style is implemented
kleing@16076
   424
  and may be used as as a ``copy-and-paste'' pattern to write your own styles.
haftmann@15960
   425
kleing@16076
   426
  The code should go into your theory file, separate from the \LaTeX\ text.
haftmann@16040
   427
  The \verb!let! expression avoids polluting the
haftmann@15960
   428
  ML global namespace. Each style receives the current proof context
kleing@16076
   429
  as first argument; this is helpful in situations where the
kleing@16076
   430
  style has some object-logic specific behaviour for example.
haftmann@15960
   431
haftmann@15960
   432
  The mapping from identifier name to the style function
nipkow@17123
   433
  is done by the @{ML TermStyle.add_style} expression which expects the desired
haftmann@15960
   434
  style name and the style function as arguments.
haftmann@15960
   435
  
haftmann@15960
   436
  After this \verb!setup!,
haftmann@16040
   437
  there will be a new style available named \verb!my_concl!, thus allowing
haftmann@16040
   438
  antiquoations like \verb!@!\verb!{thm_style my_concl hd_Cons_tl}!
haftmann@16040
   439
  yielding @{thm_style my_concl hd_Cons_tl}.
haftmann@15917
   440
haftmann@15917
   441
*}
haftmann@15917
   442
nipkow@15337
   443
(*<*)
nipkow@15337
   444
end
nipkow@16175
   445
(*>*)