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