doc-src/LaTeXsugar/Sugar/Sugar.thy
author nipkow
Mon Nov 29 18:49:35 2004 +0100 (2004-11-29 ago)
changeset 15342 13bd3d12ec2f
parent 15337 628d87767434
child 15366 e6f595009734
permissions -rw-r--r--
*** empty log message ***
nipkow@15337
     1
(*<*)
nipkow@15337
     2
theory Sugar
nipkow@15342
     3
imports LaTeXsugar
nipkow@15337
     4
begin
nipkow@15337
     5
(*>*)
nipkow@15337
     6
nipkow@15337
     7
section "Introduction"
nipkow@15337
     8
nipkow@15337
     9
text{* This document is for those Isabelle users that 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
nipkow@15342
    35
\texttt{LaTeXsugar} in the header of your own theory. You may also
nipkow@15342
    36
need additional \LaTeX\ packages. These should be included
nipkow@15342
    37
at the beginning of your \LaTeX\ document, typically in \texttt{root.tex}.
nipkow@15342
    38
*}
nipkow@15342
    39
nipkow@15342
    40
section{* HOL syntax*}
nipkow@15342
    41
nipkow@15342
    42
subsection{* Logic *}
nipkow@15342
    43
nipkow@15342
    44
text{* The predefined constructs @{text"if"}, @{text"let"} and
nipkow@15342
    45
@{text"case"} are set in sans serif font to distinguish them from
nipkow@15342
    46
other functions. This improves readability:
nipkow@15342
    47
\begin{itemize}
nipkow@15342
    48
\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
    49
\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
    50
\item @{term"case x of True \<Rightarrow> e\<^isub>1 | False \<Rightarrow> e\<^isub>2"} instead of\\
nipkow@15342
    51
      @{text"case x of True \<Rightarrow> e\<^isub>1 | False \<Rightarrow> e\<^isub>2"}.
nipkow@15342
    52
\end{itemize}
nipkow@15342
    53
*}
nipkow@15342
    54
nipkow@15342
    55
subsection{* Sets *}
nipkow@15337
    56
nipkow@15342
    57
text{* Although set syntax in HOL is already close to
nipkow@15342
    58
standard, we provide a few further improvements:
nipkow@15342
    59
\begin{itemize}
nipkow@15342
    60
\item @{term"{x. P}"} instead of @{text"{x. P}"}.
nipkow@15342
    61
\item @{term"{}"} instead of @{text"{}"}.
nipkow@15342
    62
\item @{term"insert a (insert b (insert c M))"} instead of @{text"insert a (insert b (insert c M))"}.
nipkow@15342
    63
\end{itemize}
nipkow@15342
    64
*}
nipkow@15342
    65
nipkow@15342
    66
subsection{* Lists *}
nipkow@15342
    67
nipkow@15342
    68
text{* If lists are used heavily, the following notations increase readability:
nipkow@15342
    69
\begin{itemize}
nipkow@15342
    70
\item @{term"x # xs"} instead of @{text"x # xs"}.
nipkow@15342
    71
      Exceptionally, @{term"x # xs"} is also input syntax.
nipkow@15342
    72
If you prefer more space around the $\cdot$ you have to redefine
nipkow@15342
    73
\verb!\isasymcdot! in \LaTeX:
nipkow@15342
    74
\verb!\renewcommand{\isasymcdot}{\isamath{\,\cdot\,}}!
nipkow@15342
    75
nipkow@15342
    76
\item @{term"length xs"} instead of @{text"length xs"}.
nipkow@15342
    77
\item @{term"nth xs n"} instead of @{text"nth xs i"},
nipkow@15342
    78
      the $n$th element of @{text xs}.
nipkow@15342
    79
nipkow@15342
    80
%\item The @ {text"@"} operation associates implicitly to the right,
nipkow@15342
    81
%which leads to unpleasant line breaks if the term is too long for one
nipkow@15342
    82
%line. To avoid this, @ {text"@"}-terms are grouped to the left before
nipkow@15342
    83
%printing, which leads to better line breaking behaviour:
nipkow@15342
    84
%@ {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"}
nipkow@15342
    85
nipkow@15342
    86
\end{itemize}
nipkow@15337
    87
*}
nipkow@15337
    88
nipkow@15337
    89
section "Printing theorems"
nipkow@15337
    90
nipkow@15337
    91
subsection "Inference rules"
nipkow@15337
    92
nipkow@15342
    93
text{* To print theorems as inference rules you need to include Didier
nipkow@15342
    94
R\'emy's \texttt{mathpartir} package~\cite{mathpartir}
nipkow@15342
    95
for typesetting inference rules in your \LaTeX\ file.
nipkow@15337
    96
nipkow@15337
    97
Writing \verb!@!\verb!{thm[mode=Rule] conjI[no_vars]}! produces
nipkow@15337
    98
@{thm[mode=Rule] conjI[no_vars]}, even in the middle of a sentence.
nipkow@15342
    99
If you prefer your inference rule on a separate line, maybe with a name,
nipkow@15342
   100
\begin{center}
nipkow@15342
   101
@{thm[mode=Rule] conjI[no_vars]} {\sc conjI}
nipkow@15342
   102
\end{center}
nipkow@15342
   103
is produced by
nipkow@15337
   104
\begin{quote}
nipkow@15337
   105
\verb!\begin{center}!\\
nipkow@15337
   106
\verb!@!\verb!{thm[mode=Rule] conjI[no_vars]} {\sc conjI}!\\
nipkow@15337
   107
\verb!\end{center}!
nipkow@15337
   108
\end{quote}
nipkow@15342
   109
It is not recommended to use the standard \texttt{display} attribute
nipkow@15342
   110
together with \texttt{Rule} because centering does not work and because
nipkow@15342
   111
the line breaking mechanisms of \texttt{display} and \texttt{mathpartir} can
nipkow@15342
   112
clash.
nipkow@15342
   113
nipkow@15337
   114
Of course you can display multiple rules in this fashion:
nipkow@15337
   115
\begin{quote}
nipkow@15337
   116
\verb!\begin{center}\isastyle!\\
nipkow@15337
   117
\verb!@!\verb!{thm[mode=Rule] conjI[no_vars]} {\sc conjI} \\[1ex]!\\
nipkow@15337
   118
\verb!@!\verb!{thm[mode=Rule] conjE[no_vars]} {\sc disjI$_1$} \qquad!\\
nipkow@15337
   119
\verb!@!\verb!{thm[mode=Rule] disjE[no_vars]} {\sc disjI$_2$}!\\
nipkow@15337
   120
\verb!\end{center}!
nipkow@15337
   121
\end{quote}
nipkow@15337
   122
yields
nipkow@15337
   123
\begin{center}\isastyle
nipkow@15337
   124
@{thm[mode=Rule] conjI[no_vars]} {\sc conjI} \\[1ex]
nipkow@15337
   125
@{thm[mode=Rule] disjI1[no_vars]} {\sc disjI$_1$} \qquad
nipkow@15337
   126
@{thm[mode=Rule] disjI2[no_vars]} {\sc disjI$_2$}
nipkow@15337
   127
\end{center}
nipkow@15337
   128
Note that we included \verb!\isastyle! to obtain
nipkow@15337
   129
the smaller font that otherwise comes only with \texttt{display}.
nipkow@15337
   130
nipkow@15342
   131
The \texttt{mathpartir} package copes well if there are too many
nipkow@15342
   132
premises for one line:
nipkow@15342
   133
\begin{center}
nipkow@15342
   134
@{prop[mode=Rule] "\<lbrakk> A \<longrightarrow> B; B \<longrightarrow> C; C \<longrightarrow> D; D \<longrightarrow> E; E \<longrightarrow> F; F \<longrightarrow> G;
nipkow@15342
   135
 G \<longrightarrow> H; H \<longrightarrow> I; I \<longrightarrow> J; J \<longrightarrow> K \<rbrakk> \<Longrightarrow> A \<longrightarrow> K"}
nipkow@15342
   136
\end{center}
nipkow@15342
   137
nipkow@15342
   138
Limitations: premises and conclusion must each not be longer than the line.
nipkow@15337
   139
*}
nipkow@15342
   140
nipkow@15342
   141
subsection{*If-then*}
nipkow@15342
   142
nipkow@15342
   143
text{* If you prefer a fake ``natural language'' style you can produce
nipkow@15342
   144
the body of
nipkow@15342
   145
\newtheorem{theorem}{Theorem}
nipkow@15342
   146
\begin{theorem}
nipkow@15342
   147
@{thm[mode=IfThen,eta_contract=false] setsum_cartesian_product[no_vars]}
nipkow@15342
   148
\end{theorem}
nipkow@15342
   149
by typing
nipkow@15342
   150
\begin{quote}
nipkow@15342
   151
\verb!@!\verb!{thm[mode=IfThen] setsum_cartesian_product[no_vars]}!
nipkow@15342
   152
\end{quote}
nipkow@15342
   153
nipkow@15342
   154
In order to prevent odd line breaks, the premises are put into boxes.
nipkow@15342
   155
At times this is too drastic:
nipkow@15342
   156
\begin{theorem}
nipkow@15342
   157
@{prop[mode=IfThen] "longpremise \<Longrightarrow> longerpremise \<Longrightarrow> P(f(f(f(f(f(f(f(f(f(x)))))))))) \<Longrightarrow> longestpremise \<Longrightarrow> conclusion"}
nipkow@15342
   158
\end{theorem}
nipkow@15342
   159
In which case you should use \texttt{mode=IfThenNoBox} instead of
nipkow@15342
   160
\texttt{mode=IfThen}:
nipkow@15342
   161
\begin{theorem}
nipkow@15342
   162
@{prop[mode=IfThenNoBox] "longpremise \<Longrightarrow> longerpremise \<Longrightarrow> P(f(f(f(f(f(f(f(f(f(x)))))))))) \<Longrightarrow> longestpremise \<Longrightarrow> conclusion"}
nipkow@15342
   163
\end{theorem}
nipkow@15342
   164
nipkow@15342
   165
*}
nipkow@15342
   166
nipkow@15337
   167
(*<*)
nipkow@15337
   168
end
nipkow@15337
   169
(*>*)