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