doc-src/LaTeXsugar/Sugar/document/Sugar.tex
author nipkow
Tue, 31 May 2005 12:16:42 +0200
changeset 16154 9bf4b6bf4372
parent 16076 03e8a88c0b54
child 16155 a6403c6c5339
permissions -rw-r--r--
\nexists
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
15893
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
     1
%
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
     2
\begin{isabellebody}%
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
     3
\def\isabellecontext{Sugar}%
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
     4
\isamarkupfalse%
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
     5
%
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
     6
\isamarkupsection{Introduction%
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
     7
}
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
     8
\isamarkuptrue%
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
     9
%
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
    10
\begin{isamarkuptext}%
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
    11
This document is for those Isabelle users who have mastered
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
    12
the art of mixing \LaTeX\ text and Isabelle theories and never want to
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
    13
typeset a theorem by hand anymore because they have experienced the
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
    14
bliss of writing \verb!@!\verb!{thm[display]setsum_cartesian_product[no_vars]}!
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
    15
and seeing Isabelle typeset it for them:
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
    16
\begin{isabelle}%
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
    17
{\isacharparenleft}{\isasymSum}x{\isasymin}A{\isachardot}\ {\isasymSum}y{\isasymin}B{\isachardot}\ f\ x\ y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isasymSum}z{\isasymin}A\ {\isasymtimes}\ B{\isachardot}\ f\ {\isacharparenleft}fst\ z{\isacharparenright}\ {\isacharparenleft}snd\ z{\isacharparenright}{\isacharparenright}%
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
    18
\end{isabelle}
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
    19
No typos, no omissions, no sweat.
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
    20
If you have not experienced that joy, read Chapter 4, \emph{Presenting
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
    21
Theories}, \cite{LNCS2283} first.
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
    22
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
    23
If you have mastered the art of Isabelle's \emph{antiquotations},
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
    24
i.e.\ things like the above \verb!@!\verb!{thm...}!, beware: in your vanity
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
    25
you may be tempted to think that all readers of the stunning ps or pdf
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
    26
documents you can now produce at the drop of a hat will be struck with
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
    27
awe at the beauty unfolding in front of their eyes. Until one day you
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
    28
come across that very critical of readers known as the ``common referee''.
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
    29
He has the nasty habit of refusing to understand unfamiliar notation
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
    30
like Isabelle's infamous \isa{{\isasymlbrakk}\ {\isasymrbrakk}\ {\isasymLongrightarrow}} no matter how many times you
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
    31
explain it in your paper. Even worse, he thinks that using \isa{{\isasymlbrakk}\ {\isasymrbrakk}} for anything other than denotational semantics is a cardinal sin
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
    32
that must be punished by instant rejection.
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
    33
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
    34
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
    35
This document shows you how to make Isabelle and \LaTeX\ cooperate to
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
    36
produce ordinary looking mathematics that hides the fact that it was
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
    37
typeset by a machine. You merely need to load the right files:
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
    38
\begin{itemize}
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
    39
\item Import theory \texttt{LaTeXsugar} in the header of your own
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
    40
theory.  You may also want bits of \texttt{OptionalSugar}, which you can
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
    41
copy selectively into your own theory or import as a whole.  Both
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
    42
theories live in \texttt{HOL/Library} and are found automatically.
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
    43
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
    44
\item Should you need additional \LaTeX\ packages (the text will tell
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
    45
you so), you include them at the beginning of your \LaTeX\ document,
16154
9bf4b6bf4372 \nexists
nipkow
parents: 16076
diff changeset
    46
typically in \texttt{root.tex}. For a start, you should
9bf4b6bf4372 \nexists
nipkow
parents: 16076
diff changeset
    47
\verb!\usepackage{amssymb}! --- otherwise typesetting
9bf4b6bf4372 \nexists
nipkow
parents: 16076
diff changeset
    48
\isa{{\isachardoublequote}{\isasymnot}{\isacharparenleft}{\isasymexists}x{\isachardot}\ P\ x{\isacharparenright}{\isachardoublequote}} will fail because the AMS symbol
9bf4b6bf4372 \nexists
nipkow
parents: 16076
diff changeset
    49
\isa{{\isasymnexists}} is missing.
15893
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
    50
\end{itemize}%
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
    51
\end{isamarkuptext}%
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
    52
\isamarkuptrue%
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
    53
%
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
    54
\isamarkupsection{HOL syntax%
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
    55
}
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
    56
\isamarkuptrue%
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
    57
%
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
    58
\isamarkupsubsection{Logic%
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
    59
}
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
    60
\isamarkuptrue%
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
    61
%
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
    62
\begin{isamarkuptext}%
16154
9bf4b6bf4372 \nexists
nipkow
parents: 16076
diff changeset
    63
The formula \isa{{\isachardoublequote}{\isasymnot}{\isacharparenleft}{\isasymexists}x{\isachardot}\ P\ x{\isacharparenright}{\isachardoublequote}} is typeset as \isa{{\isasymnexists}x{\isachardot}\ P\ x}.
9bf4b6bf4372 \nexists
nipkow
parents: 16076
diff changeset
    64
15893
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
    65
The predefined constructs \isa{if}, \isa{let} and
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
    66
\isa{case} are set in sans serif font to distinguish them from
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
    67
other functions. This improves readability:
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
    68
\begin{itemize}
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
    69
\item \isa{\textsf{if}\ b\ \textsf{then}\ e\isactrlisub {\isadigit{1}}\ \textsf{else}\ e\isactrlisub {\isadigit{2}}} instead of \isa{if\ b\ then\ e\isactrlisub {\isadigit{1}}\ else\ e\isactrlisub {\isadigit{2}}}.
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
    70
\item \isa{\textsf{let}\ x\ {\isacharequal}\ e\isactrlisub {\isadigit{1}}\ \textsf{in}\ e\isactrlisub {\isadigit{2}}} instead of \isa{let\ x\ {\isacharequal}\ e\isactrlisub {\isadigit{1}}\ in\ e\isactrlisub {\isadigit{2}}}.
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
    71
\item \isa{\textsf{case}\ x\ \textsf{of}\ True\ {\isasymRightarrow}\ e\isactrlisub {\isadigit{1}}\ {\isacharbar}\ False\ {\isasymRightarrow}\ e\isactrlisub {\isadigit{2}}} instead of\\
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
    72
      \isa{case\ x\ of\ True\ {\isasymRightarrow}\ e\isactrlisub {\isadigit{1}}\ {\isacharbar}\ False\ {\isasymRightarrow}\ e\isactrlisub {\isadigit{2}}}.
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
    73
\end{itemize}%
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
    74
\end{isamarkuptext}%
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
    75
\isamarkuptrue%
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
    76
%
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
    77
\isamarkupsubsection{Sets%
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
    78
}
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
    79
\isamarkuptrue%
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
    80
%
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
    81
\begin{isamarkuptext}%
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
    82
Although set syntax in HOL is already close to
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
    83
standard, we provide a few further improvements:
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
    84
\begin{itemize}
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
    85
\item \isa{{\isacharbraceleft}x\ {\isacharbar}\ P{\isacharbraceright}} instead of \isa{{\isacharbraceleft}x{\isachardot}\ P{\isacharbraceright}}.
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
    86
\item \isa{{\isasymemptyset}} instead of \isa{{\isacharbraceleft}{\isacharbraceright}}.
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
    87
\item \isa{{\isacharbraceleft}a{\isacharcomma}\ b{\isacharcomma}\ c{\isacharbraceright}\ {\isasymunion}\ M} instead of \isa{insert\ a\ {\isacharparenleft}insert\ b\ {\isacharparenleft}insert\ c\ M{\isacharparenright}{\isacharparenright}}.
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
    88
\end{itemize}%
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
    89
\end{isamarkuptext}%
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
    90
\isamarkuptrue%
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
    91
%
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
    92
\isamarkupsubsection{Lists%
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
    93
}
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
    94
\isamarkuptrue%
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
    95
%
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
    96
\begin{isamarkuptext}%
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
    97
If lists are used heavily, the following notations increase readability:
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
    98
\begin{itemize}
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
    99
\item \isa{x{\isasymcdot}xs} instead of \isa{x\ {\isacharhash}\ xs}.
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   100
      Exceptionally, \isa{x{\isasymcdot}xs} is also input syntax.
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   101
If you prefer more space around the $\cdot$ you have to redefine
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   102
\verb!\isasymcdot! in \LaTeX:
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   103
\verb!\renewcommand{\isasymcdot}{\isamath{\,\cdot\,}}!
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   104
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   105
\item \isa{{\isacharbar}xs{\isacharbar}} instead of \isa{length\ xs}.
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   106
\item \isa{xs\ensuremath{_{[\mathit{n}]}}} instead of \isa{nth\ xs\ n},
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   107
      the $n$th element of \isa{xs}.
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   108
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   109
\item The \isa{{\isacharat}} operation associates implicitly to the right,
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   110
which leads to unpleasant line breaks if the term is too long for one
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   111
line. To avoid this, \texttt{OptionalSugar} contains syntax to group
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   112
\isa{{\isacharat}}-terms to the left before printing, which leads to better
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   113
line breaking behaviour:
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   114
\begin{isabelle}%
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   115
term\isactrlisub {\isadigit{0}}\ \isacharat\ term\isactrlisub {\isadigit{1}}\ \isacharat\ term\isactrlisub {\isadigit{2}}\ \isacharat\ term\isactrlisub {\isadigit{3}}\ \isacharat\ term\isactrlisub {\isadigit{4}}\ \isacharat\ term\isactrlisub {\isadigit{5}}\ \isacharat\ term\isactrlisub {\isadigit{6}}\ \isacharat\ term\isactrlisub {\isadigit{7}}\ \isacharat\ term\isactrlisub {\isadigit{8}}\ \isacharat\ term\isactrlisub {\isadigit{9}}\ \isacharat\ term\isactrlisub {\isadigit{1}}\isactrlisub {\isadigit{0}}%
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   116
\end{isabelle}
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   117
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   118
\end{itemize}%
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   119
\end{isamarkuptext}%
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   120
\isamarkuptrue%
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   121
%
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   122
\isamarkupsection{Printing theorems%
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   123
}
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   124
\isamarkuptrue%
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   125
%
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   126
\isamarkupsubsection{Question marks%
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   127
}
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   128
\isamarkuptrue%
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   129
%
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   130
\begin{isamarkuptext}%
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   131
If you print anything, especially theorems, containing
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   132
schematic variables they are prefixed with a question mark:
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   133
\verb!@!\verb!{thm conjI}! results in \isa{{\isasymlbrakk}{\isacharquery}P{\isacharsemicolon}\ {\isacharquery}Q{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isacharquery}P\ {\isasymand}\ {\isacharquery}Q}. Most of the time
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   134
you would rather not see the question marks. There is an attribute
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   135
\verb!no_vars! that you can attach to the theorem that turns its
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   136
schematic into ordinary free variables: \verb!@!\verb!{thm conjI[no_vars]}!
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   137
results in \isa{{\isasymlbrakk}P{\isacharsemicolon}\ Q{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ {\isasymand}\ Q}.
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   138
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   139
This \verb!no_vars! business can become a bit tedious.
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   140
If you would rather never see question marks, simply put
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   141
\begin{verbatim}
15984
bc6ead9d6628 updated;
wenzelm
parents: 15960
diff changeset
   142
reset show_question_marks;
15893
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   143
\end{verbatim}
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   144
at the beginning of your file \texttt{ROOT.ML}.
16075
8852058ecf8d added ? explanations
nipkow
parents: 16040
diff changeset
   145
The rest of this document is produced with this flag reset.
8852058ecf8d added ? explanations
nipkow
parents: 16040
diff changeset
   146
8852058ecf8d added ? explanations
nipkow
parents: 16040
diff changeset
   147
Hint: Resetting \verb!show_question_marks! only supresses question
8852058ecf8d added ? explanations
nipkow
parents: 16040
diff changeset
   148
marks; variables that end in digits, e.g. \isa{x{\isadigit{1}}}, are still
8852058ecf8d added ? explanations
nipkow
parents: 16040
diff changeset
   149
printed with a trailing \isa{{\isachardot}{\isadigit{0}}}, e.g. \isa{x{\isadigit{1}}{\isachardot}{\isadigit{0}}}, their
8852058ecf8d added ? explanations
nipkow
parents: 16040
diff changeset
   150
internal index. This can be avoided by turning the last digit into a
8852058ecf8d added ? explanations
nipkow
parents: 16040
diff changeset
   151
subscript: write \verb!x\<^isub>1! and obtain the much nicer \isa{x\isactrlisub {\isadigit{1}}}.%
15893
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   152
\end{isamarkuptext}%
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   153
\isamarkuptrue%
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   154
\isamarkupfalse%
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   155
%
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   156
\isamarkupsubsection{Inference rules%
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   157
}
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   158
\isamarkuptrue%
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   159
%
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   160
\begin{isamarkuptext}%
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   161
To print theorems as inference rules you need to include Didier
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   162
R\'emy's \texttt{mathpartir} package~\cite{mathpartir}
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   163
for typesetting inference rules in your \LaTeX\ file.
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   164
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   165
Writing \verb!@!\verb!{thm[mode=Rule] conjI}! produces
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   166
\isa{\mbox{}\inferrule{\mbox{P}\\\ \mbox{Q}}{\mbox{P\ {\isasymand}\ Q}}}, even in the middle of a sentence.
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   167
If you prefer your inference rule on a separate line, maybe with a name,
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   168
\begin{center}
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   169
\isa{\mbox{}\inferrule{\mbox{P}\\\ \mbox{Q}}{\mbox{P\ {\isasymand}\ Q}}} {\sc conjI}
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   170
\end{center}
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   171
is produced by
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   172
\begin{quote}
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   173
\verb!\begin{center}!\\
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   174
\verb!@!\verb!{thm[mode=Rule] conjI} {\sc conjI}!\\
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   175
\verb!\end{center}!
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   176
\end{quote}
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   177
It is not recommended to use the standard \texttt{display} attribute
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   178
together with \texttt{Rule} because centering does not work and because
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   179
the line breaking mechanisms of \texttt{display} and \texttt{mathpartir} can
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   180
clash.
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   181
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   182
Of course you can display multiple rules in this fashion:
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   183
\begin{quote}
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   184
\verb!\begin{center}\isastyle!\\
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   185
\verb!@!\verb!{thm[mode=Rule] conjI} {\sc conjI} \\[1ex]!\\
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   186
\verb!@!\verb!{thm[mode=Rule] conjE} {\sc disjI$_1$} \qquad!\\
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   187
\verb!@!\verb!{thm[mode=Rule] disjE} {\sc disjI$_2$}!\\
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   188
\verb!\end{center}!
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   189
\end{quote}
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   190
yields
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   191
\begin{center}\isastyle
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   192
\isa{\mbox{}\inferrule{\mbox{P}\\\ \mbox{Q}}{\mbox{P\ {\isasymand}\ Q}}} {\sc conjI} \\[1ex]
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   193
\isa{\mbox{}\inferrule{\mbox{P}}{\mbox{P\ {\isasymor}\ Q}}} {\sc disjI$_1$} \qquad
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   194
\isa{\mbox{}\inferrule{\mbox{Q}}{\mbox{P\ {\isasymor}\ Q}}} {\sc disjI$_2$}
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   195
\end{center}
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   196
Note that we included \verb!\isastyle! to obtain
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   197
the smaller font that otherwise comes only with \texttt{display}.
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   198
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   199
The \texttt{mathpartir} package copes well if there are too many
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   200
premises for one line:
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   201
\begin{center}
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   202
\isa{\mbox{}\inferrule{\mbox{A\ {\isasymlongrightarrow}\ B}\\\ \mbox{B\ {\isasymlongrightarrow}\ C}\\\ \mbox{C\ {\isasymlongrightarrow}\ D}\\\ \mbox{D\ {\isasymlongrightarrow}\ E}\\\ \mbox{E\ {\isasymlongrightarrow}\ F}\\\ \mbox{F\ {\isasymlongrightarrow}\ G}\\\ \mbox{G\ {\isasymlongrightarrow}\ H}\\\ \mbox{H\ {\isasymlongrightarrow}\ I}\\\ \mbox{I\ {\isasymlongrightarrow}\ J}\\\ \mbox{J\ {\isasymlongrightarrow}\ K}}{\mbox{A\ {\isasymlongrightarrow}\ K}}}
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   203
\end{center}
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   204
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   205
Limitations: 1. Premises and conclusion must each not be longer than
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   206
the line.  2. Premises that are \isa{{\isasymLongrightarrow}}-implications are again
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   207
displayed with a horizontal line, which looks at least unusual.%
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   208
\end{isamarkuptext}%
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   209
\isamarkuptrue%
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   210
%
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   211
\isamarkupsubsection{If-then%
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   212
}
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   213
\isamarkuptrue%
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   214
%
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   215
\begin{isamarkuptext}%
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   216
If you prefer a fake ``natural language'' style you can produce
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   217
the body of
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   218
\newtheorem{theorem}{Theorem}
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   219
\begin{theorem}
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   220
\isa{{\rmfamily\upshape\normalsize{}If\,}\ \mbox{i\ {\isasymle}\ j}\ {\rmfamily\upshape\normalsize \,and\,}\ \mbox{j\ {\isasymle}\ k}\ {\rmfamily\upshape\normalsize \,then\,}\ i\ {\isasymle}\ k{\isachardot}}
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   221
\end{theorem}
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   222
by typing
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   223
\begin{quote}
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   224
\verb!@!\verb!{thm[mode=IfThen] le_trans}!
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   225
\end{quote}
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   226
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   227
In order to prevent odd line breaks, the premises are put into boxes.
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   228
At times this is too drastic:
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   229
\begin{theorem}
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   230
\isa{{\rmfamily\upshape\normalsize{}If\,}\ \mbox{longpremise}\ {\rmfamily\upshape\normalsize \,and\,}\ \mbox{longerpremise}\ {\rmfamily\upshape\normalsize \,and\,}\ \mbox{P\ {\isacharparenleft}f\ {\isacharparenleft}f\ {\isacharparenleft}f\ {\isacharparenleft}f\ {\isacharparenleft}f\ {\isacharparenleft}f\ {\isacharparenleft}f\ {\isacharparenleft}f\ {\isacharparenleft}f\ x{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharparenright}}\ {\rmfamily\upshape\normalsize \,and\,}\ \mbox{longestpremise}\ {\rmfamily\upshape\normalsize \,then\,}\ conclusion{\isachardot}}
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   231
\end{theorem}
16154
9bf4b6bf4372 \nexists
nipkow
parents: 16076
diff changeset
   232
In which case you should use \texttt{IfThenNoBox} instead of
9bf4b6bf4372 \nexists
nipkow
parents: 16076
diff changeset
   233
\texttt{IfThen}:
15893
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   234
\begin{theorem}
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   235
\isa{{\rmfamily\upshape\normalsize{}If\,}\ longpremise\ {\rmfamily\upshape\normalsize \,and\,}\ longerpremise\ {\rmfamily\upshape\normalsize \,and\,}\ P\ {\isacharparenleft}f\ {\isacharparenleft}f\ {\isacharparenleft}f\ {\isacharparenleft}f\ {\isacharparenleft}f\ {\isacharparenleft}f\ {\isacharparenleft}f\ {\isacharparenleft}f\ {\isacharparenleft}f\ x{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharparenright}{\isacharparenright}\ {\rmfamily\upshape\normalsize \,and\,}\ longestpremise\ {\rmfamily\upshape\normalsize \,then\,}\ conclusion{\isachardot}}
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   236
\end{theorem}%
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   237
\end{isamarkuptext}%
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   238
\isamarkuptrue%
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   239
%
16154
9bf4b6bf4372 \nexists
nipkow
parents: 16076
diff changeset
   240
\isamarkupsubsection{Doing it yourself%
9bf4b6bf4372 \nexists
nipkow
parents: 16076
diff changeset
   241
}
9bf4b6bf4372 \nexists
nipkow
parents: 16076
diff changeset
   242
\isamarkuptrue%
9bf4b6bf4372 \nexists
nipkow
parents: 16076
diff changeset
   243
%
9bf4b6bf4372 \nexists
nipkow
parents: 16076
diff changeset
   244
\begin{isamarkuptext}%
9bf4b6bf4372 \nexists
nipkow
parents: 16076
diff changeset
   245
If for some reason you want or need to present theorems your
9bf4b6bf4372 \nexists
nipkow
parents: 16076
diff changeset
   246
own way, you can extract the premises and the conclusion explicitly
9bf4b6bf4372 \nexists
nipkow
parents: 16076
diff changeset
   247
and combine them as you like:
9bf4b6bf4372 \nexists
nipkow
parents: 16076
diff changeset
   248
\begin{itemize}
9bf4b6bf4372 \nexists
nipkow
parents: 16076
diff changeset
   249
\item \verb!@!\verb!{thm_style premise1! $thm$\verb!}!
9bf4b6bf4372 \nexists
nipkow
parents: 16076
diff changeset
   250
prints premise 1 of $thm$ (and similarly up to \texttt{premise9}).
9bf4b6bf4372 \nexists
nipkow
parents: 16076
diff changeset
   251
\item \verb!@!\verb!{thm_style conclusion! $thm$\verb!}!
9bf4b6bf4372 \nexists
nipkow
parents: 16076
diff changeset
   252
prints the conclusion of $thm$.
9bf4b6bf4372 \nexists
nipkow
parents: 16076
diff changeset
   253
\end{itemize}
9bf4b6bf4372 \nexists
nipkow
parents: 16076
diff changeset
   254
For example, ``from \isa{Q} and
9bf4b6bf4372 \nexists
nipkow
parents: 16076
diff changeset
   255
\isa{P} we conclude \isa{P\ {\isasymand}\ Q}''
9bf4b6bf4372 \nexists
nipkow
parents: 16076
diff changeset
   256
is produced by
9bf4b6bf4372 \nexists
nipkow
parents: 16076
diff changeset
   257
\begin{quote}
9bf4b6bf4372 \nexists
nipkow
parents: 16076
diff changeset
   258
\verb!from !\verb!@!\verb!{thm_style premise2 conjI}!\\
9bf4b6bf4372 \nexists
nipkow
parents: 16076
diff changeset
   259
\verb!and !\verb!@!\verb!{thm_style premise1 conjI}!\\
9bf4b6bf4372 \nexists
nipkow
parents: 16076
diff changeset
   260
\verb!we conclude !\verb!@!\verb!{thm_style conclusion conjI}!
9bf4b6bf4372 \nexists
nipkow
parents: 16076
diff changeset
   261
\end{quote}
9bf4b6bf4372 \nexists
nipkow
parents: 16076
diff changeset
   262
Thus you can rearrange or hide premises and typeset the theorem as you like.
9bf4b6bf4372 \nexists
nipkow
parents: 16076
diff changeset
   263
The \verb!thm_style! antiquotation is a general mechanism explained
9bf4b6bf4372 \nexists
nipkow
parents: 16076
diff changeset
   264
in \S\ref{sec:styles}.%
9bf4b6bf4372 \nexists
nipkow
parents: 16076
diff changeset
   265
\end{isamarkuptext}%
9bf4b6bf4372 \nexists
nipkow
parents: 16076
diff changeset
   266
\isamarkuptrue%
9bf4b6bf4372 \nexists
nipkow
parents: 16076
diff changeset
   267
%
15893
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   268
\isamarkupsubsection{Patterns%
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   269
}
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   270
\isamarkuptrue%
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   271
%
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   272
\begin{isamarkuptext}%
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   273
Sometimes functions ignore one or more of their
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   274
  arguments and some functional languages have nice 
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   275
  syntax for that as in \isa{hd\ {\isacharparenleft}x{\isasymcdot}\_{\isacharparenright}\ {\isacharequal}\ x}.
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   276
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   277
  You can simulate this in Isabelle by instantiating the \isa{xs} in
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   278
  definition \mbox{\isa{hd\ {\isacharparenleft}x{\isasymcdot}xs{\isacharparenright}\ {\isacharequal}\ x}} with a constant \isa{DUMMY} that
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   279
  is printed as \isa{\_}. The code for the pattern above is 
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   280
  \verb!@!\verb!{thm hd.simps [where xs=DUMMY]}!.
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   281
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   282
  You can drive this game even further and extend the syntax of let
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   283
  bindings such that certain functions like \isa{fst}, \isa{hd}, 
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   284
  etc.\ are printed as patterns. \texttt{OptionalSugar} provides the
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   285
  following:
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   286
  
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   287
  \begin{center}
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   288
  \begin{tabular}{l@ {~~produced by~~}l}
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   289
  \isa{\textsf{let}\ {\isacharparenleft}x{\isacharcomma}\ \_{\isacharparenright}\ {\isacharequal}\ p\ \textsf{in}\ t} & \verb!@!\verb!{term "let x = fst p in t"}!\\
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   290
  \isa{\textsf{let}\ {\isacharparenleft}\_{\isacharcomma}\ x{\isacharparenright}\ {\isacharequal}\ p\ \textsf{in}\ t} & \verb!@!\verb!{term "let x = snd p in t"}!\\
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   291
  \isa{\textsf{let}\ x{\isasymcdot}\_\ {\isacharequal}\ xs\ \textsf{in}\ t} & \verb!@!\verb!{term "let x = hd xs in t"}!\\
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   292
  \isa{\textsf{let}\ \_{\isasymcdot}x\ {\isacharequal}\ xs\ \textsf{in}\ t} & \verb!@!\verb!{term "let x = tl xs in t"}!\\
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   293
  \isa{\textsf{let}\ Some\ x\ {\isacharequal}\ y\ \textsf{in}\ t} & \verb!@!\verb!{term "let x = the y in t"}!\\
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   294
  \end{tabular}
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   295
  \end{center}%
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   296
\end{isamarkuptext}%
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   297
\isamarkuptrue%
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   298
%
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   299
\isamarkupsubsection{Proofs%
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   300
}
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   301
\isamarkuptrue%
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   302
%
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   303
\begin{isamarkuptext}%
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   304
Full proofs, even if written in beautiful Isar style, are likely to
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   305
  be too long and detailed to be included in conference papers, but
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   306
  some key lemmas might be of interest.
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   307
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   308
  It is usually easiest to put them in figures like the one in Fig.\
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   309
  \ref{fig:proof}. This was achieved with the \isakeyword{text\_raw}
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   310
  command:%
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   311
\end{isamarkuptext}%
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   312
\isamarkuptrue%
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   313
%
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   314
\begin{figure}
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   315
  \begin{center}\begin{minipage}{0.6\textwidth}  
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   316
  \isastyle\isamarkuptrue
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   317
\isacommand{lemma}\ True\isanewline
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   318
\isamarkupfalse%
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   319
\isacommand{proof}\ {\isacharminus}\isanewline
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   320
\ \ %
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   321
\isamarkupcmt{pretty trivial%
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   322
}
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   323
\isanewline
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   324
\ \ \isamarkupfalse%
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   325
\isacommand{show}\ True\ \isamarkupfalse%
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   326
\isacommand{by}\ force\isanewline
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   327
\isamarkupfalse%
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   328
\isacommand{qed}\isamarkupfalse%
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   329
%
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   330
\end{minipage}\end{center}
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   331
  \caption{Example proof in a figure.}\label{fig:proof}
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   332
  \end{figure}
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   333
%
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   334
\begin{isamarkuptext}%
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   335
\begin{quote}
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   336
\small
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   337
\verb!text_raw {!\verb!*!\\
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   338
\verb!  \begin{figure}!\\
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   339
\verb!  \begin{center}\begin{minipage}{0.6\textwidth}!\\
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   340
\verb!  \isastyle\isamarkuptrue!\\
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   341
\verb!*!\verb!}!\\
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   342
\verb!lemma True!\\
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   343
\verb!proof -!\\
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   344
\verb!  -- "pretty trivial"!\\
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   345
\verb!  show True by force!\\
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   346
\verb!qed!\\
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   347
\verb!text_raw {!\verb!*!\\
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   348
\verb!  \end{minipage}\end{center}!\\
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   349
\verb!  \caption{Example proof in a figure.}\label{fig:proof}!\\
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   350
\verb!  \end{figure}!\\
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   351
\verb!*!\verb!}!
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   352
\end{quote}%
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   353
\end{isamarkuptext}%
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   354
\isamarkuptrue%
15953
902b556e4bc0 fixed a few things and added Haftmann as author
nipkow
parents: 15893
diff changeset
   355
%
16154
9bf4b6bf4372 \nexists
nipkow
parents: 16076
diff changeset
   356
\isamarkupsubsection{Styles\label{sec:styles}%
15953
902b556e4bc0 fixed a few things and added Haftmann as author
nipkow
parents: 15893
diff changeset
   357
}
902b556e4bc0 fixed a few things and added Haftmann as author
nipkow
parents: 15893
diff changeset
   358
\isamarkuptrue%
902b556e4bc0 fixed a few things and added Haftmann as author
nipkow
parents: 15893
diff changeset
   359
%
902b556e4bc0 fixed a few things and added Haftmann as author
nipkow
parents: 15893
diff changeset
   360
\begin{isamarkuptext}%
902b556e4bc0 fixed a few things and added Haftmann as author
nipkow
parents: 15893
diff changeset
   361
The \verb!thm! antiquotation works nicely for single theorems, but
902b556e4bc0 fixed a few things and added Haftmann as author
nipkow
parents: 15893
diff changeset
   362
  sets of equations as used in definitions are more difficult to
16040
6e7616eba0b8 some adaptions
haftmann
parents: 16001
diff changeset
   363
  typeset nicely: people tend to prefer aligned \isa{{\isacharequal}} signs.
15953
902b556e4bc0 fixed a few things and added Haftmann as author
nipkow
parents: 15893
diff changeset
   364
902b556e4bc0 fixed a few things and added Haftmann as author
nipkow
parents: 15893
diff changeset
   365
  To deal with such cases where it is desirable to dive into the structure
16040
6e7616eba0b8 some adaptions
haftmann
parents: 16001
diff changeset
   366
  of terms and theorems, Isabelle offers antiquotations featuring
15953
902b556e4bc0 fixed a few things and added Haftmann as author
nipkow
parents: 15893
diff changeset
   367
  ``styles'':
902b556e4bc0 fixed a few things and added Haftmann as author
nipkow
parents: 15893
diff changeset
   368
902b556e4bc0 fixed a few things and added Haftmann as author
nipkow
parents: 15893
diff changeset
   369
    \begin{quote}
902b556e4bc0 fixed a few things and added Haftmann as author
nipkow
parents: 15893
diff changeset
   370
    \verb!@!\verb!{thm_style stylename thm}!\\
902b556e4bc0 fixed a few things and added Haftmann as author
nipkow
parents: 15893
diff changeset
   371
    \verb!@!\verb!{term_style stylename term}!
902b556e4bc0 fixed a few things and added Haftmann as author
nipkow
parents: 15893
diff changeset
   372
    \end{quote}
902b556e4bc0 fixed a few things and added Haftmann as author
nipkow
parents: 15893
diff changeset
   373
16040
6e7616eba0b8 some adaptions
haftmann
parents: 16001
diff changeset
   374
  A ``style'' is a transformation of propositions. There are predefined
16076
03e8a88c0b54 tuned thm_style section
kleing
parents: 16075
diff changeset
   375
  styles, namly \verb!lhs!, \verb!rhs! and \verb!conclusion!. For example, 
03e8a88c0b54 tuned thm_style section
kleing
parents: 16075
diff changeset
   376
  the output
15953
902b556e4bc0 fixed a few things and added Haftmann as author
nipkow
parents: 15893
diff changeset
   377
  \begin{center}
902b556e4bc0 fixed a few things and added Haftmann as author
nipkow
parents: 15893
diff changeset
   378
  \begin{tabular}{l@ {~~\isa{{\isacharequal}}~~}l}
902b556e4bc0 fixed a few things and added Haftmann as author
nipkow
parents: 15893
diff changeset
   379
  \isa{foldl\ f\ a\ {\isacharbrackleft}{\isacharbrackright}} & \isa{a}\\
902b556e4bc0 fixed a few things and added Haftmann as author
nipkow
parents: 15893
diff changeset
   380
  \isa{foldl\ f\ a\ {\isacharparenleft}x{\isasymcdot}xs{\isacharparenright}} & \isa{foldl\ f\ {\isacharparenleft}f\ a\ x{\isacharparenright}\ xs}
902b556e4bc0 fixed a few things and added Haftmann as author
nipkow
parents: 15893
diff changeset
   381
  \end{tabular}
902b556e4bc0 fixed a few things and added Haftmann as author
nipkow
parents: 15893
diff changeset
   382
  \end{center}
902b556e4bc0 fixed a few things and added Haftmann as author
nipkow
parents: 15893
diff changeset
   383
  is produced by the following code:
902b556e4bc0 fixed a few things and added Haftmann as author
nipkow
parents: 15893
diff changeset
   384
  \begin{quote}
902b556e4bc0 fixed a few things and added Haftmann as author
nipkow
parents: 15893
diff changeset
   385
    \verb!\begin{center}!\\
902b556e4bc0 fixed a few things and added Haftmann as author
nipkow
parents: 15893
diff changeset
   386
    \verb!\begin{tabular}{l@ {~~!\verb!@!\verb!{text "="}~~}l}!\\
902b556e4bc0 fixed a few things and added Haftmann as author
nipkow
parents: 15893
diff changeset
   387
    \verb!@!\verb!{thm_style lhs foldl_Nil} & @!\verb!{thm_style rhs foldl_Nil}!\\
902b556e4bc0 fixed a few things and added Haftmann as author
nipkow
parents: 15893
diff changeset
   388
    \verb!@!\verb!{thm_style lhs foldl_Cons} & @!\verb!{thm_style rhs foldl_Cons}!\\
902b556e4bc0 fixed a few things and added Haftmann as author
nipkow
parents: 15893
diff changeset
   389
    \verb!\end{tabular}!\\
902b556e4bc0 fixed a few things and added Haftmann as author
nipkow
parents: 15893
diff changeset
   390
    \verb!\end{center}!
902b556e4bc0 fixed a few things and added Haftmann as author
nipkow
parents: 15893
diff changeset
   391
  \end{quote}
902b556e4bc0 fixed a few things and added Haftmann as author
nipkow
parents: 15893
diff changeset
   392
  Note the space between \verb!@! and \verb!{! in the tabular argument.
902b556e4bc0 fixed a few things and added Haftmann as author
nipkow
parents: 15893
diff changeset
   393
  It prevents Isabelle from interpreting \verb!@ {~~...~~}! 
16076
03e8a88c0b54 tuned thm_style section
kleing
parents: 16075
diff changeset
   394
  as an antiquotation. The styles \verb!lhs! and \verb!rhs!
16040
6e7616eba0b8 some adaptions
haftmann
parents: 16001
diff changeset
   395
  extract the left hand side (or right hand side respectivly) from the
16076
03e8a88c0b54 tuned thm_style section
kleing
parents: 16075
diff changeset
   396
  conclusion of propositions consisting of a binary operator
16040
6e7616eba0b8 some adaptions
haftmann
parents: 16001
diff changeset
   397
  (e.~g.~\isa{{\isacharequal}}, \isa{{\isasymequiv}}, \isa{{\isacharless}}).
15953
902b556e4bc0 fixed a few things and added Haftmann as author
nipkow
parents: 15893
diff changeset
   398
16076
03e8a88c0b54 tuned thm_style section
kleing
parents: 16075
diff changeset
   399
  Likewise, \verb!conclusion! may be used as a style to show just the
03e8a88c0b54 tuned thm_style section
kleing
parents: 16075
diff changeset
   400
  conclusion of a proposition. For example, take \verb!hd_Cons_tl!:
16040
6e7616eba0b8 some adaptions
haftmann
parents: 16001
diff changeset
   401
  \begin{center}
6e7616eba0b8 some adaptions
haftmann
parents: 16001
diff changeset
   402
    \isa{xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymLongrightarrow}\ hd\ xs{\isasymcdot}tl\ xs\ {\isacharequal}\ xs}
6e7616eba0b8 some adaptions
haftmann
parents: 16001
diff changeset
   403
  \end{center}
6e7616eba0b8 some adaptions
haftmann
parents: 16001
diff changeset
   404
  To print just the conclusion,
15953
902b556e4bc0 fixed a few things and added Haftmann as author
nipkow
parents: 15893
diff changeset
   405
  \begin{center}
902b556e4bc0 fixed a few things and added Haftmann as author
nipkow
parents: 15893
diff changeset
   406
    \isa{hd\ xs{\isasymcdot}tl\ xs\ {\isacharequal}\ xs}
902b556e4bc0 fixed a few things and added Haftmann as author
nipkow
parents: 15893
diff changeset
   407
  \end{center}
16040
6e7616eba0b8 some adaptions
haftmann
parents: 16001
diff changeset
   408
  type
15953
902b556e4bc0 fixed a few things and added Haftmann as author
nipkow
parents: 15893
diff changeset
   409
  \begin{quote}
902b556e4bc0 fixed a few things and added Haftmann as author
nipkow
parents: 15893
diff changeset
   410
    \verb!\begin{center}!\\
902b556e4bc0 fixed a few things and added Haftmann as author
nipkow
parents: 15893
diff changeset
   411
    \verb!@!\verb!{thm_style conclusion hd_Cons_tl}!\\
902b556e4bc0 fixed a few things and added Haftmann as author
nipkow
parents: 15893
diff changeset
   412
    \verb!\end{center}!
902b556e4bc0 fixed a few things and added Haftmann as author
nipkow
parents: 15893
diff changeset
   413
  \end{quote}
902b556e4bc0 fixed a few things and added Haftmann as author
nipkow
parents: 15893
diff changeset
   414
902b556e4bc0 fixed a few things and added Haftmann as author
nipkow
parents: 15893
diff changeset
   415
  If you are not afraid of ML, you may also define your own styles.
15960
9bd6550dc004 added Proof.context to antiquotation
haftmann
parents: 15953
diff changeset
   416
  A style is implemented by an ML function of type
9bd6550dc004 added Proof.context to antiquotation
haftmann
parents: 15953
diff changeset
   417
  \verb!Proof.context -> term -> term!.
16040
6e7616eba0b8 some adaptions
haftmann
parents: 16001
diff changeset
   418
  Have a look at the following example:%
6e7616eba0b8 some adaptions
haftmann
parents: 16001
diff changeset
   419
\end{isamarkuptext}%
6e7616eba0b8 some adaptions
haftmann
parents: 16001
diff changeset
   420
\isamarkuptrue%
16075
8852058ecf8d added ? explanations
nipkow
parents: 16040
diff changeset
   421
\isamarkupfalse%
16040
6e7616eba0b8 some adaptions
haftmann
parents: 16001
diff changeset
   422
%
6e7616eba0b8 some adaptions
haftmann
parents: 16001
diff changeset
   423
\begin{isamarkuptext}%
6e7616eba0b8 some adaptions
haftmann
parents: 16001
diff changeset
   424
\begin{quote}
15953
902b556e4bc0 fixed a few things and added Haftmann as author
nipkow
parents: 15893
diff changeset
   425
    \verb!setup {!\verb!*!\\
902b556e4bc0 fixed a few things and added Haftmann as author
nipkow
parents: 15893
diff changeset
   426
    \verb!let!\\
16040
6e7616eba0b8 some adaptions
haftmann
parents: 16001
diff changeset
   427
    \verb!  fun my_concl ctxt = Logic.strip_imp_concl!\\
6e7616eba0b8 some adaptions
haftmann
parents: 16001
diff changeset
   428
    \verb!  in [TermStyle.add_style "my_concl" my_concl]!\\
15953
902b556e4bc0 fixed a few things and added Haftmann as author
nipkow
parents: 15893
diff changeset
   429
    \verb!end;!\\
902b556e4bc0 fixed a few things and added Haftmann as author
nipkow
parents: 15893
diff changeset
   430
    \verb!*!\verb!}!\\
902b556e4bc0 fixed a few things and added Haftmann as author
nipkow
parents: 15893
diff changeset
   431
  \end{quote}
15960
9bd6550dc004 added Proof.context to antiquotation
haftmann
parents: 15953
diff changeset
   432
16076
03e8a88c0b54 tuned thm_style section
kleing
parents: 16075
diff changeset
   433
  \noindent
03e8a88c0b54 tuned thm_style section
kleing
parents: 16075
diff changeset
   434
  This example shows how the \verb!conclusion! style could have been implemented
03e8a88c0b54 tuned thm_style section
kleing
parents: 16075
diff changeset
   435
  and may be used as as a ``copy-and-paste'' pattern to write your own styles.
03e8a88c0b54 tuned thm_style section
kleing
parents: 16075
diff changeset
   436
  (The real implementation of \verb!conclusion! is a bit more sophisticated).
15960
9bd6550dc004 added Proof.context to antiquotation
haftmann
parents: 15953
diff changeset
   437
16076
03e8a88c0b54 tuned thm_style section
kleing
parents: 16075
diff changeset
   438
  The code should go into your theory file, separate from the \LaTeX\ text.
16040
6e7616eba0b8 some adaptions
haftmann
parents: 16001
diff changeset
   439
  The \verb!let! expression avoids polluting the
15960
9bd6550dc004 added Proof.context to antiquotation
haftmann
parents: 15953
diff changeset
   440
  ML global namespace. Each style receives the current proof context
16076
03e8a88c0b54 tuned thm_style section
kleing
parents: 16075
diff changeset
   441
  as first argument; this is helpful in situations where the
03e8a88c0b54 tuned thm_style section
kleing
parents: 16075
diff changeset
   442
  style has some object-logic specific behaviour for example.
15960
9bd6550dc004 added Proof.context to antiquotation
haftmann
parents: 15953
diff changeset
   443
9bd6550dc004 added Proof.context to antiquotation
haftmann
parents: 15953
diff changeset
   444
  The mapping from identifier name to the style function
16075
8852058ecf8d added ? explanations
nipkow
parents: 16040
diff changeset
   445
  is done by the \isa{TermStyle{\isachardot}add{\isacharunderscore}style} expression which expects the desired
15960
9bd6550dc004 added Proof.context to antiquotation
haftmann
parents: 15953
diff changeset
   446
  style name and the style function as arguments.
9bd6550dc004 added Proof.context to antiquotation
haftmann
parents: 15953
diff changeset
   447
  
9bd6550dc004 added Proof.context to antiquotation
haftmann
parents: 15953
diff changeset
   448
  After this \verb!setup!,
16040
6e7616eba0b8 some adaptions
haftmann
parents: 16001
diff changeset
   449
  there will be a new style available named \verb!my_concl!, thus allowing
6e7616eba0b8 some adaptions
haftmann
parents: 16001
diff changeset
   450
  antiquoations like \verb!@!\verb!{thm_style my_concl hd_Cons_tl}!
16076
03e8a88c0b54 tuned thm_style section
kleing
parents: 16075
diff changeset
   451
  yielding \isa{hd\ xs{\isasymcdot}tl\ xs\ {\isacharequal}\ xs}.%
15953
902b556e4bc0 fixed a few things and added Haftmann as author
nipkow
parents: 15893
diff changeset
   452
\end{isamarkuptext}%
902b556e4bc0 fixed a few things and added Haftmann as author
nipkow
parents: 15893
diff changeset
   453
\isamarkuptrue%
15893
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   454
\isamarkupfalse%
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   455
\end{isabellebody}%
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   456
%%% Local Variables:
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   457
%%% mode: latex
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   458
%%% TeX-master: "root"
c0cd613a49eb move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff changeset
   459
%%% End: