doc-src/LaTeXsugar/Sugar/Sugar.thy
author nipkow
Wed, 15 Jun 2005 09:01:15 +0200
changeset 16395 3446d2b6a19f
parent 16175 749e6b68ca84
child 17031 ffa73448025e
permissions -rw-r--r--
documented DUMMY
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
15385
26b05d4bc21a improvements by Larry and Micheal Wahler
kleing
parents: 15378
diff changeset
     9
text{* This document is for those Isabelle users who have mastered
15337
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
15471
e7f069887ec2 *** empty log message ***
nipkow
parents: 15428
diff changeset
    34
typeset by a machine. You merely need to load the right files:
e7f069887ec2 *** empty log message ***
nipkow
parents: 15428
diff changeset
    35
\begin{itemize}
e7f069887ec2 *** empty log message ***
nipkow
parents: 15428
diff changeset
    36
\item Import theory \texttt{LaTeXsugar} in the header of your own
e7f069887ec2 *** empty log message ***
nipkow
parents: 15428
diff changeset
    37
theory.  You may also want bits of \texttt{OptionalSugar}, which you can
e7f069887ec2 *** empty log message ***
nipkow
parents: 15428
diff changeset
    38
copy selectively into your own theory or import as a whole.  Both
e7f069887ec2 *** empty log message ***
nipkow
parents: 15428
diff changeset
    39
theories live in \texttt{HOL/Library} and are found automatically.
15378
b1c5add0a65e link to tar.gz
kleing
parents: 15373
diff changeset
    40
15471
e7f069887ec2 *** empty log message ***
nipkow
parents: 15428
diff changeset
    41
\item Should you need additional \LaTeX\ packages (the text will tell
e7f069887ec2 *** empty log message ***
nipkow
parents: 15428
diff changeset
    42
you so), you include them at the beginning of your \LaTeX\ document,
16153
999ca183b4c7 \nexists und premsise1 .. 9
nipkow
parents: 16076
diff changeset
    43
typically in \texttt{root.tex}. For a start, you should
999ca183b4c7 \nexists und premsise1 .. 9
nipkow
parents: 16076
diff changeset
    44
\verb!\usepackage{amssymb}! --- otherwise typesetting
999ca183b4c7 \nexists und premsise1 .. 9
nipkow
parents: 16076
diff changeset
    45
@{prop[source]"\<not>(\<exists>x. P x)"} will fail because the AMS symbol
999ca183b4c7 \nexists und premsise1 .. 9
nipkow
parents: 16076
diff changeset
    46
@{text"\<nexists>"} is missing.
15471
e7f069887ec2 *** empty log message ***
nipkow
parents: 15428
diff changeset
    47
\end{itemize}
15342
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
    48
*}
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
    49
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
    50
section{* HOL syntax*}
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
    51
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
    52
subsection{* Logic *}
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
    53
16153
999ca183b4c7 \nexists und premsise1 .. 9
nipkow
parents: 16076
diff changeset
    54
text{* 
999ca183b4c7 \nexists und premsise1 .. 9
nipkow
parents: 16076
diff changeset
    55
  The formula @{prop[source]"\<not>(\<exists>x. P x)"} is typeset as @{prop"~(EX x. P x)"}.
999ca183b4c7 \nexists und premsise1 .. 9
nipkow
parents: 16076
diff changeset
    56
999ca183b4c7 \nexists und premsise1 .. 9
nipkow
parents: 16076
diff changeset
    57
The predefined constructs @{text"if"}, @{text"let"} and
15342
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
    58
@{text"case"} are set in sans serif font to distinguish them from
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
    59
other functions. This improves readability:
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
    60
\begin{itemize}
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
    61
\item @{term"if b then e\<^isub>1 else e\<^isub>2"} instead of @{text"if b then e\<^isub>1 else e\<^isub>2"}.
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
    62
\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
    63
\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
    64
      @{text"case x of True \<Rightarrow> e\<^isub>1 | False \<Rightarrow> e\<^isub>2"}.
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
    65
\end{itemize}
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
    66
*}
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
    67
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
    68
subsection{* Sets *}
15337
nipkow
parents:
diff changeset
    69
15342
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
    70
text{* Although set syntax in HOL is already close to
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
    71
standard, we provide a few further improvements:
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
    72
\begin{itemize}
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
    73
\item @{term"{x. P}"} instead of @{text"{x. P}"}.
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
    74
\item @{term"{}"} instead of @{text"{}"}.
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
    75
\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
    76
\end{itemize}
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
    77
*}
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
    78
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
    79
subsection{* Lists *}
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
    80
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
    81
text{* If lists are used heavily, the following notations increase readability:
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
    82
\begin{itemize}
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
    83
\item @{term"x # xs"} instead of @{text"x # xs"}.
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
    84
      Exceptionally, @{term"x # xs"} is also input syntax.
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
    85
If you prefer more space around the $\cdot$ you have to redefine
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
    86
\verb!\isasymcdot! in \LaTeX:
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
    87
\verb!\renewcommand{\isasymcdot}{\isamath{\,\cdot\,}}!
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
    88
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
    89
\item @{term"length xs"} instead of @{text"length xs"}.
15385
26b05d4bc21a improvements by Larry and Micheal Wahler
kleing
parents: 15378
diff changeset
    90
\item @{term"nth xs n"} instead of @{text"nth xs n"},
15342
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
    91
      the $n$th element of @{text xs}.
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
    92
15366
e6f595009734 more sugar
kleing
parents: 15342
diff changeset
    93
\item The @{text"@"} operation associates implicitly to the right,
e6f595009734 more sugar
kleing
parents: 15342
diff changeset
    94
which leads to unpleasant line breaks if the term is too long for one
e6f595009734 more sugar
kleing
parents: 15342
diff changeset
    95
line. To avoid this, \texttt{OptionalSugar} contains syntax to group
e6f595009734 more sugar
kleing
parents: 15342
diff changeset
    96
@{text"@"}-terms to the left before printing, which leads to better
e6f595009734 more sugar
kleing
parents: 15342
diff changeset
    97
line breaking behaviour:
15673
60c56561bcf4 added term_8;
wenzelm
parents: 15491
diff changeset
    98
@{term[display]"term\<^isub>0 @ term\<^isub>1 @ term\<^isub>2 @ term\<^isub>3 @ term\<^isub>4 @ term\<^isub>5 @ term\<^isub>6 @ term\<^isub>7 @ term\<^isub>8 @ term\<^isub>9 @ term\<^isub>1\<^isub>0"}
15366
e6f595009734 more sugar
kleing
parents: 15342
diff changeset
    99
15342
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
   100
\end{itemize}
15337
nipkow
parents:
diff changeset
   101
*}
nipkow
parents:
diff changeset
   102
nipkow
parents:
diff changeset
   103
section "Printing theorems"
nipkow
parents:
diff changeset
   104
15689
621bd0d8048f section on qmark
nipkow
parents: 15673
diff changeset
   105
subsection "Question marks"
621bd0d8048f section on qmark
nipkow
parents: 15673
diff changeset
   106
621bd0d8048f section on qmark
nipkow
parents: 15673
diff changeset
   107
text{* If you print anything, especially theorems, containing
621bd0d8048f section on qmark
nipkow
parents: 15673
diff changeset
   108
schematic variables they are prefixed with a question mark:
621bd0d8048f section on qmark
nipkow
parents: 15673
diff changeset
   109
\verb!@!\verb!{thm conjI}! results in @{thm conjI}. Most of the time
621bd0d8048f section on qmark
nipkow
parents: 15673
diff changeset
   110
you would rather not see the question marks. There is an attribute
621bd0d8048f section on qmark
nipkow
parents: 15673
diff changeset
   111
\verb!no_vars! that you can attach to the theorem that turns its
621bd0d8048f section on qmark
nipkow
parents: 15673
diff changeset
   112
schematic into ordinary free variables: \verb!@!\verb!{thm conjI[no_vars]}!
621bd0d8048f section on qmark
nipkow
parents: 15673
diff changeset
   113
results in @{thm conjI[no_vars]}.
621bd0d8048f section on qmark
nipkow
parents: 15673
diff changeset
   114
621bd0d8048f section on qmark
nipkow
parents: 15673
diff changeset
   115
This \verb!no_vars! business can become a bit tedious.
621bd0d8048f section on qmark
nipkow
parents: 15673
diff changeset
   116
If you would rather never see question marks, simply put
621bd0d8048f section on qmark
nipkow
parents: 15673
diff changeset
   117
\begin{verbatim}
15983
a53abeedc879 renamed show_var_qmarks to show_question_marks;
wenzelm
parents: 15960
diff changeset
   118
reset show_question_marks;
15689
621bd0d8048f section on qmark
nipkow
parents: 15673
diff changeset
   119
\end{verbatim}
621bd0d8048f section on qmark
nipkow
parents: 15673
diff changeset
   120
at the beginning of your file \texttt{ROOT.ML}.
621bd0d8048f section on qmark
nipkow
parents: 15673
diff changeset
   121
The rest of this document is produced with this flag reset.
16075
8852058ecf8d added ? explanations
nipkow
parents: 16064
diff changeset
   122
8852058ecf8d added ? explanations
nipkow
parents: 16064
diff changeset
   123
Hint: Resetting \verb!show_question_marks! only supresses question
8852058ecf8d added ? explanations
nipkow
parents: 16064
diff changeset
   124
marks; variables that end in digits, e.g. @{text"x1"}, are still
8852058ecf8d added ? explanations
nipkow
parents: 16064
diff changeset
   125
printed with a trailing @{text".0"}, e.g. @{text"x1.0"}, their
8852058ecf8d added ? explanations
nipkow
parents: 16064
diff changeset
   126
internal index. This can be avoided by turning the last digit into a
8852058ecf8d added ? explanations
nipkow
parents: 16064
diff changeset
   127
subscript: write \verb!x\<^isub>1! and obtain the much nicer @{text"x\<^isub>1"}. *}
15689
621bd0d8048f section on qmark
nipkow
parents: 15673
diff changeset
   128
15983
a53abeedc879 renamed show_var_qmarks to show_question_marks;
wenzelm
parents: 15960
diff changeset
   129
(*<*)ML"reset show_question_marks"(*>*)
15689
621bd0d8048f section on qmark
nipkow
parents: 15673
diff changeset
   130
16395
3446d2b6a19f documented DUMMY
nipkow
parents: 16175
diff changeset
   131
subsection "Variable names"
3446d2b6a19f documented DUMMY
nipkow
parents: 16175
diff changeset
   132
3446d2b6a19f documented DUMMY
nipkow
parents: 16175
diff changeset
   133
text{* It sometimes happens that you want to change the name of a
3446d2b6a19f documented DUMMY
nipkow
parents: 16175
diff changeset
   134
variable in a theorem before printing it. This can easily be achieved
3446d2b6a19f documented DUMMY
nipkow
parents: 16175
diff changeset
   135
with the help of Isabelle's instantiation attribute \texttt{where}:
3446d2b6a19f documented DUMMY
nipkow
parents: 16175
diff changeset
   136
@{thm conjI[where P = \<phi> and Q = \<psi>]} is the result of
3446d2b6a19f documented DUMMY
nipkow
parents: 16175
diff changeset
   137
\begin{quote}
3446d2b6a19f documented DUMMY
nipkow
parents: 16175
diff changeset
   138
\verb!@!\verb!{thm conjI[where P = \<phi> and Q = \<psi>]}!
3446d2b6a19f documented DUMMY
nipkow
parents: 16175
diff changeset
   139
\end{quote}
3446d2b6a19f documented DUMMY
nipkow
parents: 16175
diff changeset
   140
To support the ``\_''-notation for irrelevant variables
3446d2b6a19f documented DUMMY
nipkow
parents: 16175
diff changeset
   141
the constant \texttt{DUMMY} has been introduced:
3446d2b6a19f documented DUMMY
nipkow
parents: 16175
diff changeset
   142
@{thm fst_conv[where b = DUMMY]} is produced by
3446d2b6a19f documented DUMMY
nipkow
parents: 16175
diff changeset
   143
\begin{quote}
3446d2b6a19f documented DUMMY
nipkow
parents: 16175
diff changeset
   144
\verb!@!\verb!{thm fst_conv[where b = DUMMY]}!
3446d2b6a19f documented DUMMY
nipkow
parents: 16175
diff changeset
   145
\end{quote}
3446d2b6a19f documented DUMMY
nipkow
parents: 16175
diff changeset
   146
*}
3446d2b6a19f documented DUMMY
nipkow
parents: 16175
diff changeset
   147
15337
nipkow
parents:
diff changeset
   148
subsection "Inference rules"
nipkow
parents:
diff changeset
   149
15342
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
   150
text{* To print theorems as inference rules you need to include Didier
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
   151
R\'emy's \texttt{mathpartir} package~\cite{mathpartir}
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
   152
for typesetting inference rules in your \LaTeX\ file.
15337
nipkow
parents:
diff changeset
   153
15689
621bd0d8048f section on qmark
nipkow
parents: 15673
diff changeset
   154
Writing \verb!@!\verb!{thm[mode=Rule] conjI}! produces
621bd0d8048f section on qmark
nipkow
parents: 15673
diff changeset
   155
@{thm[mode=Rule] conjI}, even in the middle of a sentence.
15342
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
   156
If you prefer your inference rule on a separate line, maybe with a name,
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
   157
\begin{center}
15689
621bd0d8048f section on qmark
nipkow
parents: 15673
diff changeset
   158
@{thm[mode=Rule] conjI} {\sc conjI}
15342
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
   159
\end{center}
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
   160
is produced by
15337
nipkow
parents:
diff changeset
   161
\begin{quote}
nipkow
parents:
diff changeset
   162
\verb!\begin{center}!\\
15689
621bd0d8048f section on qmark
nipkow
parents: 15673
diff changeset
   163
\verb!@!\verb!{thm[mode=Rule] conjI} {\sc conjI}!\\
15337
nipkow
parents:
diff changeset
   164
\verb!\end{center}!
nipkow
parents:
diff changeset
   165
\end{quote}
15342
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
   166
It is not recommended to use the standard \texttt{display} attribute
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
   167
together with \texttt{Rule} because centering does not work and because
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
   168
the line breaking mechanisms of \texttt{display} and \texttt{mathpartir} can
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
   169
clash.
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
   170
15337
nipkow
parents:
diff changeset
   171
Of course you can display multiple rules in this fashion:
nipkow
parents:
diff changeset
   172
\begin{quote}
nipkow
parents:
diff changeset
   173
\verb!\begin{center}\isastyle!\\
15689
621bd0d8048f section on qmark
nipkow
parents: 15673
diff changeset
   174
\verb!@!\verb!{thm[mode=Rule] conjI} {\sc conjI} \\[1ex]!\\
621bd0d8048f section on qmark
nipkow
parents: 15673
diff changeset
   175
\verb!@!\verb!{thm[mode=Rule] conjE} {\sc disjI$_1$} \qquad!\\
621bd0d8048f section on qmark
nipkow
parents: 15673
diff changeset
   176
\verb!@!\verb!{thm[mode=Rule] disjE} {\sc disjI$_2$}!\\
15337
nipkow
parents:
diff changeset
   177
\verb!\end{center}!
nipkow
parents:
diff changeset
   178
\end{quote}
nipkow
parents:
diff changeset
   179
yields
nipkow
parents:
diff changeset
   180
\begin{center}\isastyle
15689
621bd0d8048f section on qmark
nipkow
parents: 15673
diff changeset
   181
@{thm[mode=Rule] conjI} {\sc conjI} \\[1ex]
621bd0d8048f section on qmark
nipkow
parents: 15673
diff changeset
   182
@{thm[mode=Rule] disjI1} {\sc disjI$_1$} \qquad
621bd0d8048f section on qmark
nipkow
parents: 15673
diff changeset
   183
@{thm[mode=Rule] disjI2} {\sc disjI$_2$}
15337
nipkow
parents:
diff changeset
   184
\end{center}
nipkow
parents:
diff changeset
   185
Note that we included \verb!\isastyle! to obtain
nipkow
parents:
diff changeset
   186
the smaller font that otherwise comes only with \texttt{display}.
nipkow
parents:
diff changeset
   187
15342
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
   188
The \texttt{mathpartir} package copes well if there are too many
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
   189
premises for one line:
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
   190
\begin{center}
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
   191
@{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
   192
 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
   193
\end{center}
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
   194
15471
e7f069887ec2 *** empty log message ***
nipkow
parents: 15428
diff changeset
   195
Limitations: 1. Premises and conclusion must each not be longer than
e7f069887ec2 *** empty log message ***
nipkow
parents: 15428
diff changeset
   196
the line.  2. Premises that are @{text"\<Longrightarrow>"}-implications are again
e7f069887ec2 *** empty log message ***
nipkow
parents: 15428
diff changeset
   197
displayed with a horizontal line, which looks at least unusual.
e7f069887ec2 *** empty log message ***
nipkow
parents: 15428
diff changeset
   198
15337
nipkow
parents:
diff changeset
   199
*}
15342
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
   200
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
   201
subsection{*If-then*}
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
   202
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
   203
text{* If you prefer a fake ``natural language'' style you can produce
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
   204
the body of
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
   205
\newtheorem{theorem}{Theorem}
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
   206
\begin{theorem}
15689
621bd0d8048f section on qmark
nipkow
parents: 15673
diff changeset
   207
@{thm[mode=IfThen] le_trans}
15342
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
   208
\end{theorem}
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
   209
by typing
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
   210
\begin{quote}
15689
621bd0d8048f section on qmark
nipkow
parents: 15673
diff changeset
   211
\verb!@!\verb!{thm[mode=IfThen] le_trans}!
15342
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
   212
\end{quote}
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
   213
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
   214
In order to prevent odd line breaks, the premises are put into boxes.
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
   215
At times this is too drastic:
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
   216
\begin{theorem}
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
   217
@{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
   218
\end{theorem}
16153
999ca183b4c7 \nexists und premsise1 .. 9
nipkow
parents: 16076
diff changeset
   219
In which case you should use \texttt{IfThenNoBox} instead of
999ca183b4c7 \nexists und premsise1 .. 9
nipkow
parents: 16076
diff changeset
   220
\texttt{IfThen}:
15342
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
   221
\begin{theorem}
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
   222
@{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
   223
\end{theorem}
15366
e6f595009734 more sugar
kleing
parents: 15342
diff changeset
   224
*}
15342
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
   225
16166
346bb10d4bbb some refinements
haftmann
parents: 16165
diff changeset
   226
subsection{* Doing it yourself\label{sec:yourself}*}
16153
999ca183b4c7 \nexists und premsise1 .. 9
nipkow
parents: 16076
diff changeset
   227
999ca183b4c7 \nexists und premsise1 .. 9
nipkow
parents: 16076
diff changeset
   228
text{* If for some reason you want or need to present theorems your
999ca183b4c7 \nexists und premsise1 .. 9
nipkow
parents: 16076
diff changeset
   229
own way, you can extract the premises and the conclusion explicitly
999ca183b4c7 \nexists und premsise1 .. 9
nipkow
parents: 16076
diff changeset
   230
and combine them as you like:
999ca183b4c7 \nexists und premsise1 .. 9
nipkow
parents: 16076
diff changeset
   231
\begin{itemize}
16167
b2e4c4058b71 renamed premise* to prem
haftmann
parents: 16166
diff changeset
   232
\item \verb!@!\verb!{thm_style prem1! $thm$\verb!}!
b2e4c4058b71 renamed premise* to prem
haftmann
parents: 16166
diff changeset
   233
prints premise 1 of $thm$ (and similarly up to \texttt{prem9}).
16165
dbe9ee8ffcdd concl antiqutations
haftmann
parents: 16155
diff changeset
   234
\item \verb!@!\verb!{thm_style concl! $thm$\verb!}!
16153
999ca183b4c7 \nexists und premsise1 .. 9
nipkow
parents: 16076
diff changeset
   235
prints the conclusion of $thm$.
999ca183b4c7 \nexists und premsise1 .. 9
nipkow
parents: 16076
diff changeset
   236
\end{itemize}
16167
b2e4c4058b71 renamed premise* to prem
haftmann
parents: 16166
diff changeset
   237
For example, ``from @{thm_style prem2 conjI} and
b2e4c4058b71 renamed premise* to prem
haftmann
parents: 16166
diff changeset
   238
@{thm_style prem1 conjI} we conclude @{thm_style concl conjI}''
16153
999ca183b4c7 \nexists und premsise1 .. 9
nipkow
parents: 16076
diff changeset
   239
is produced by
999ca183b4c7 \nexists und premsise1 .. 9
nipkow
parents: 16076
diff changeset
   240
\begin{quote}
16175
nipkow
parents: 16167
diff changeset
   241
\verb!from !\verb!@!\verb!{thm_style prem2 conjI}! \verb!and !\verb!@!\verb!{thm_style prem1 conjI}!\\
16165
dbe9ee8ffcdd concl antiqutations
haftmann
parents: 16155
diff changeset
   242
\verb!we conclude !\verb!@!\verb!{thm_style concl conjI}!
16153
999ca183b4c7 \nexists und premsise1 .. 9
nipkow
parents: 16076
diff changeset
   243
\end{quote}
999ca183b4c7 \nexists und premsise1 .. 9
nipkow
parents: 16076
diff changeset
   244
Thus you can rearrange or hide premises and typeset the theorem as you like.
999ca183b4c7 \nexists und premsise1 .. 9
nipkow
parents: 16076
diff changeset
   245
The \verb!thm_style! antiquotation is a general mechanism explained
999ca183b4c7 \nexists und premsise1 .. 9
nipkow
parents: 16076
diff changeset
   246
in \S\ref{sec:styles}.
999ca183b4c7 \nexists und premsise1 .. 9
nipkow
parents: 16076
diff changeset
   247
*}
999ca183b4c7 \nexists und premsise1 .. 9
nipkow
parents: 16076
diff changeset
   248
15366
e6f595009734 more sugar
kleing
parents: 15342
diff changeset
   249
subsection "Patterns"
e6f595009734 more sugar
kleing
parents: 15342
diff changeset
   250
e6f595009734 more sugar
kleing
parents: 15342
diff changeset
   251
text {*
e6f595009734 more sugar
kleing
parents: 15342
diff changeset
   252
  Sometimes functions ignore one or more of their
e6f595009734 more sugar
kleing
parents: 15342
diff changeset
   253
  arguments and some functional languages have nice 
15689
621bd0d8048f section on qmark
nipkow
parents: 15673
diff changeset
   254
  syntax for that as in @{thm hd.simps [where xs=DUMMY]}.
15366
e6f595009734 more sugar
kleing
parents: 15342
diff changeset
   255
e6f595009734 more sugar
kleing
parents: 15342
diff changeset
   256
  You can simulate this in Isabelle by instantiating the @{term xs} in
15689
621bd0d8048f section on qmark
nipkow
parents: 15673
diff changeset
   257
  definition \mbox{@{thm hd.simps}} with a constant @{text DUMMY} that
15366
e6f595009734 more sugar
kleing
parents: 15342
diff changeset
   258
  is printed as @{term DUMMY}. The code for the pattern above is 
15689
621bd0d8048f section on qmark
nipkow
parents: 15673
diff changeset
   259
  \verb!@!\verb!{thm hd.simps [where xs=DUMMY]}!.
15366
e6f595009734 more sugar
kleing
parents: 15342
diff changeset
   260
e6f595009734 more sugar
kleing
parents: 15342
diff changeset
   261
  You can drive this game even further and extend the syntax of let
e6f595009734 more sugar
kleing
parents: 15342
diff changeset
   262
  bindings such that certain functions like @{term fst}, @{term hd}, 
15368
kleing
parents: 15367
diff changeset
   263
  etc.\ are printed as patterns. \texttt{OptionalSugar} provides the
kleing
parents: 15367
diff changeset
   264
  following:
15366
e6f595009734 more sugar
kleing
parents: 15342
diff changeset
   265
  
e6f595009734 more sugar
kleing
parents: 15342
diff changeset
   266
  \begin{center}
e6f595009734 more sugar
kleing
parents: 15342
diff changeset
   267
  \begin{tabular}{l@ {~~produced by~~}l}
e6f595009734 more sugar
kleing
parents: 15342
diff changeset
   268
  @{term "let x = fst p in t"} & \verb!@!\verb!{term "let x = fst p in t"}!\\
e6f595009734 more sugar
kleing
parents: 15342
diff changeset
   269
  @{term "let x = snd p in t"} & \verb!@!\verb!{term "let x = snd p in t"}!\\
e6f595009734 more sugar
kleing
parents: 15342
diff changeset
   270
  @{term "let x = hd xs in t"} & \verb!@!\verb!{term "let x = hd xs in t"}!\\
e6f595009734 more sugar
kleing
parents: 15342
diff changeset
   271
  @{term "let x = tl xs in t"} & \verb!@!\verb!{term "let x = tl xs in t"}!\\
e6f595009734 more sugar
kleing
parents: 15342
diff changeset
   272
  @{term "let x = the y in t"} & \verb!@!\verb!{term "let x = the y in t"}!\\
e6f595009734 more sugar
kleing
parents: 15342
diff changeset
   273
  \end{tabular}
e6f595009734 more sugar
kleing
parents: 15342
diff changeset
   274
  \end{center}
e6f595009734 more sugar
kleing
parents: 15342
diff changeset
   275
*}
e6f595009734 more sugar
kleing
parents: 15342
diff changeset
   276
16155
a6403c6c5339 fixed sectioning
nipkow
parents: 16153
diff changeset
   277
section "Proofs"
15366
e6f595009734 more sugar
kleing
parents: 15342
diff changeset
   278
e6f595009734 more sugar
kleing
parents: 15342
diff changeset
   279
text {*
15367
ac18081228ae fixed typo
kleing
parents: 15366
diff changeset
   280
  Full proofs, even if written in beautiful Isar style, are likely to
15366
e6f595009734 more sugar
kleing
parents: 15342
diff changeset
   281
  be too long and detailed to be included in conference papers, but
e6f595009734 more sugar
kleing
parents: 15342
diff changeset
   282
  some key lemmas might be of interest.
e6f595009734 more sugar
kleing
parents: 15342
diff changeset
   283
e6f595009734 more sugar
kleing
parents: 15342
diff changeset
   284
  It is usually easiest to put them in figures like the one in Fig.\
e6f595009734 more sugar
kleing
parents: 15342
diff changeset
   285
  \ref{fig:proof}. This was achieved with the \isakeyword{text\_raw}
e6f595009734 more sugar
kleing
parents: 15342
diff changeset
   286
  command:
e6f595009734 more sugar
kleing
parents: 15342
diff changeset
   287
*}
e6f595009734 more sugar
kleing
parents: 15342
diff changeset
   288
text_raw {*
e6f595009734 more sugar
kleing
parents: 15342
diff changeset
   289
  \begin{figure}
e6f595009734 more sugar
kleing
parents: 15342
diff changeset
   290
  \begin{center}\begin{minipage}{0.6\textwidth}  
15428
3f1a674b7ec7 suggestions by Jeremy Siek
kleing
parents: 15385
diff changeset
   291
  \isastyle\isamarkuptrue
15366
e6f595009734 more sugar
kleing
parents: 15342
diff changeset
   292
*}
e6f595009734 more sugar
kleing
parents: 15342
diff changeset
   293
lemma True
e6f595009734 more sugar
kleing
parents: 15342
diff changeset
   294
proof -
e6f595009734 more sugar
kleing
parents: 15342
diff changeset
   295
  -- "pretty trivial"
e6f595009734 more sugar
kleing
parents: 15342
diff changeset
   296
  show True by force
e6f595009734 more sugar
kleing
parents: 15342
diff changeset
   297
qed
15428
3f1a674b7ec7 suggestions by Jeremy Siek
kleing
parents: 15385
diff changeset
   298
text_raw {*    
15366
e6f595009734 more sugar
kleing
parents: 15342
diff changeset
   299
  \end{minipage}\end{center}
e6f595009734 more sugar
kleing
parents: 15342
diff changeset
   300
  \caption{Example proof in a figure.}\label{fig:proof}
e6f595009734 more sugar
kleing
parents: 15342
diff changeset
   301
  \end{figure}
e6f595009734 more sugar
kleing
parents: 15342
diff changeset
   302
*}
e6f595009734 more sugar
kleing
parents: 15342
diff changeset
   303
text {*
e6f595009734 more sugar
kleing
parents: 15342
diff changeset
   304
e6f595009734 more sugar
kleing
parents: 15342
diff changeset
   305
\begin{quote}
e6f595009734 more sugar
kleing
parents: 15342
diff changeset
   306
\small
e6f595009734 more sugar
kleing
parents: 15342
diff changeset
   307
\verb!text_raw {!\verb!*!\\
e6f595009734 more sugar
kleing
parents: 15342
diff changeset
   308
\verb!  \begin{figure}!\\
e6f595009734 more sugar
kleing
parents: 15342
diff changeset
   309
\verb!  \begin{center}\begin{minipage}{0.6\textwidth}!\\
15428
3f1a674b7ec7 suggestions by Jeremy Siek
kleing
parents: 15385
diff changeset
   310
\verb!  \isastyle\isamarkuptrue!\\
15366
e6f595009734 more sugar
kleing
parents: 15342
diff changeset
   311
\verb!*!\verb!}!\\
e6f595009734 more sugar
kleing
parents: 15342
diff changeset
   312
\verb!lemma True!\\
e6f595009734 more sugar
kleing
parents: 15342
diff changeset
   313
\verb!proof -!\\
e6f595009734 more sugar
kleing
parents: 15342
diff changeset
   314
\verb!  -- "pretty trivial"!\\
e6f595009734 more sugar
kleing
parents: 15342
diff changeset
   315
\verb!  show True by force!\\
e6f595009734 more sugar
kleing
parents: 15342
diff changeset
   316
\verb!qed!\\
e6f595009734 more sugar
kleing
parents: 15342
diff changeset
   317
\verb!text_raw {!\verb!*!\\
e6f595009734 more sugar
kleing
parents: 15342
diff changeset
   318
\verb!  \end{minipage}\end{center}!\\
e6f595009734 more sugar
kleing
parents: 15342
diff changeset
   319
\verb!  \caption{Example proof in a figure.}\label{fig:proof}!\\
e6f595009734 more sugar
kleing
parents: 15342
diff changeset
   320
\verb!  \end{figure}!\\
e6f595009734 more sugar
kleing
parents: 15342
diff changeset
   321
\verb!*!\verb!}!
e6f595009734 more sugar
kleing
parents: 15342
diff changeset
   322
\end{quote}
e6f595009734 more sugar
kleing
parents: 15342
diff changeset
   323
  
15342
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
   324
*}
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
   325
16155
a6403c6c5339 fixed sectioning
nipkow
parents: 16153
diff changeset
   326
section {*Styles\label{sec:styles}*}
15917
cd4983c76548 Added short description of thm_style and term_style antiquotation
haftmann
parents: 15689
diff changeset
   327
cd4983c76548 Added short description of thm_style and term_style antiquotation
haftmann
parents: 15689
diff changeset
   328
text {*
15953
902b556e4bc0 fixed a few things and added Haftmann as author
nipkow
parents: 15917
diff changeset
   329
  The \verb!thm! antiquotation works nicely for single theorems, but
15917
cd4983c76548 Added short description of thm_style and term_style antiquotation
haftmann
parents: 15689
diff changeset
   330
  sets of equations as used in definitions are more difficult to
16040
6e7616eba0b8 some adaptions
haftmann
parents: 15983
diff changeset
   331
  typeset nicely: people tend to prefer aligned @{text "="} signs.
15917
cd4983c76548 Added short description of thm_style and term_style antiquotation
haftmann
parents: 15689
diff changeset
   332
cd4983c76548 Added short description of thm_style and term_style antiquotation
haftmann
parents: 15689
diff changeset
   333
  To deal with such cases where it is desirable to dive into the structure
16040
6e7616eba0b8 some adaptions
haftmann
parents: 15983
diff changeset
   334
  of terms and theorems, Isabelle offers antiquotations featuring
15917
cd4983c76548 Added short description of thm_style and term_style antiquotation
haftmann
parents: 15689
diff changeset
   335
  ``styles'':
cd4983c76548 Added short description of thm_style and term_style antiquotation
haftmann
parents: 15689
diff changeset
   336
cd4983c76548 Added short description of thm_style and term_style antiquotation
haftmann
parents: 15689
diff changeset
   337
    \begin{quote}
cd4983c76548 Added short description of thm_style and term_style antiquotation
haftmann
parents: 15689
diff changeset
   338
    \verb!@!\verb!{thm_style stylename thm}!\\
cd4983c76548 Added short description of thm_style and term_style antiquotation
haftmann
parents: 15689
diff changeset
   339
    \verb!@!\verb!{term_style stylename term}!
cd4983c76548 Added short description of thm_style and term_style antiquotation
haftmann
parents: 15689
diff changeset
   340
    \end{quote}
cd4983c76548 Added short description of thm_style and term_style antiquotation
haftmann
parents: 15689
diff changeset
   341
16040
6e7616eba0b8 some adaptions
haftmann
parents: 15983
diff changeset
   342
  A ``style'' is a transformation of propositions. There are predefined
16167
b2e4c4058b71 renamed premise* to prem
haftmann
parents: 16166
diff changeset
   343
  styles, namly \verb!lhs! and \verb!rhs!, \verb!prem1! up to \verb!prem9!, and \verb!concl!.
16166
346bb10d4bbb some refinements
haftmann
parents: 16165
diff changeset
   344
  For example, 
16076
03e8a88c0b54 tuned thm_style section
kleing
parents: 16075
diff changeset
   345
  the output
15917
cd4983c76548 Added short description of thm_style and term_style antiquotation
haftmann
parents: 15689
diff changeset
   346
  \begin{center}
cd4983c76548 Added short description of thm_style and term_style antiquotation
haftmann
parents: 15689
diff changeset
   347
  \begin{tabular}{l@ {~~@{text "="}~~}l}
cd4983c76548 Added short description of thm_style and term_style antiquotation
haftmann
parents: 15689
diff changeset
   348
  @{thm_style lhs foldl_Nil} & @{thm_style rhs foldl_Nil}\\
cd4983c76548 Added short description of thm_style and term_style antiquotation
haftmann
parents: 15689
diff changeset
   349
  @{thm_style lhs foldl_Cons} & @{thm_style rhs foldl_Cons}
cd4983c76548 Added short description of thm_style and term_style antiquotation
haftmann
parents: 15689
diff changeset
   350
  \end{tabular}
cd4983c76548 Added short description of thm_style and term_style antiquotation
haftmann
parents: 15689
diff changeset
   351
  \end{center}
cd4983c76548 Added short description of thm_style and term_style antiquotation
haftmann
parents: 15689
diff changeset
   352
  is produced by the following code:
cd4983c76548 Added short description of thm_style and term_style antiquotation
haftmann
parents: 15689
diff changeset
   353
  \begin{quote}
cd4983c76548 Added short description of thm_style and term_style antiquotation
haftmann
parents: 15689
diff changeset
   354
    \verb!\begin{center}!\\
cd4983c76548 Added short description of thm_style and term_style antiquotation
haftmann
parents: 15689
diff changeset
   355
    \verb!\begin{tabular}{l@ {~~!\verb!@!\verb!{text "="}~~}l}!\\
cd4983c76548 Added short description of thm_style and term_style antiquotation
haftmann
parents: 15689
diff changeset
   356
    \verb!@!\verb!{thm_style lhs foldl_Nil} & @!\verb!{thm_style rhs foldl_Nil}!\\
cd4983c76548 Added short description of thm_style and term_style antiquotation
haftmann
parents: 15689
diff changeset
   357
    \verb!@!\verb!{thm_style lhs foldl_Cons} & @!\verb!{thm_style rhs foldl_Cons}!\\
cd4983c76548 Added short description of thm_style and term_style antiquotation
haftmann
parents: 15689
diff changeset
   358
    \verb!\end{tabular}!\\
cd4983c76548 Added short description of thm_style and term_style antiquotation
haftmann
parents: 15689
diff changeset
   359
    \verb!\end{center}!
cd4983c76548 Added short description of thm_style and term_style antiquotation
haftmann
parents: 15689
diff changeset
   360
  \end{quote}
cd4983c76548 Added short description of thm_style and term_style antiquotation
haftmann
parents: 15689
diff changeset
   361
  Note the space between \verb!@! and \verb!{! in the tabular argument.
cd4983c76548 Added short description of thm_style and term_style antiquotation
haftmann
parents: 15689
diff changeset
   362
  It prevents Isabelle from interpreting \verb!@ {~~...~~}! 
16076
03e8a88c0b54 tuned thm_style section
kleing
parents: 16075
diff changeset
   363
  as an antiquotation. The styles \verb!lhs! and \verb!rhs!
16040
6e7616eba0b8 some adaptions
haftmann
parents: 15983
diff changeset
   364
  extract the left hand side (or right hand side respectivly) from the
16076
03e8a88c0b54 tuned thm_style section
kleing
parents: 16075
diff changeset
   365
  conclusion of propositions consisting of a binary operator
16040
6e7616eba0b8 some adaptions
haftmann
parents: 15983
diff changeset
   366
  (e.~g.~@{text "="}, @{text "\<equiv>"}, @{text "<"}).
15917
cd4983c76548 Added short description of thm_style and term_style antiquotation
haftmann
parents: 15689
diff changeset
   367
16165
dbe9ee8ffcdd concl antiqutations
haftmann
parents: 16155
diff changeset
   368
  Likewise, \verb!concl! may be used as a style to show just the
16076
03e8a88c0b54 tuned thm_style section
kleing
parents: 16075
diff changeset
   369
  conclusion of a proposition. For example, take \verb!hd_Cons_tl!:
16040
6e7616eba0b8 some adaptions
haftmann
parents: 15983
diff changeset
   370
  \begin{center}
6e7616eba0b8 some adaptions
haftmann
parents: 15983
diff changeset
   371
    @{thm hd_Cons_tl}
6e7616eba0b8 some adaptions
haftmann
parents: 15983
diff changeset
   372
  \end{center}
6e7616eba0b8 some adaptions
haftmann
parents: 15983
diff changeset
   373
  To print just the conclusion,
15917
cd4983c76548 Added short description of thm_style and term_style antiquotation
haftmann
parents: 15689
diff changeset
   374
  \begin{center}
16165
dbe9ee8ffcdd concl antiqutations
haftmann
parents: 16155
diff changeset
   375
    @{thm_style concl hd_Cons_tl}
15917
cd4983c76548 Added short description of thm_style and term_style antiquotation
haftmann
parents: 15689
diff changeset
   376
  \end{center}
16040
6e7616eba0b8 some adaptions
haftmann
parents: 15983
diff changeset
   377
  type
15917
cd4983c76548 Added short description of thm_style and term_style antiquotation
haftmann
parents: 15689
diff changeset
   378
  \begin{quote}
cd4983c76548 Added short description of thm_style and term_style antiquotation
haftmann
parents: 15689
diff changeset
   379
    \verb!\begin{center}!\\
16165
dbe9ee8ffcdd concl antiqutations
haftmann
parents: 16155
diff changeset
   380
    \verb!@!\verb!{thm_style concl hd_Cons_tl}!\\
15917
cd4983c76548 Added short description of thm_style and term_style antiquotation
haftmann
parents: 15689
diff changeset
   381
    \verb!\end{center}!
cd4983c76548 Added short description of thm_style and term_style antiquotation
haftmann
parents: 15689
diff changeset
   382
  \end{quote}
cd4983c76548 Added short description of thm_style and term_style antiquotation
haftmann
parents: 15689
diff changeset
   383
16166
346bb10d4bbb some refinements
haftmann
parents: 16165
diff changeset
   384
  Further use cases can be found in \S\ref{sec:yourself}.
346bb10d4bbb some refinements
haftmann
parents: 16165
diff changeset
   385
15953
902b556e4bc0 fixed a few things and added Haftmann as author
nipkow
parents: 15917
diff changeset
   386
  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
   387
  A style is implemented by an ML function of type
9bd6550dc004 added Proof.context to antiquotation
haftmann
parents: 15953
diff changeset
   388
  \verb!Proof.context -> term -> term!.
9bd6550dc004 added Proof.context to antiquotation
haftmann
parents: 15953
diff changeset
   389
  Have a look at the following example:
9bd6550dc004 added Proof.context to antiquotation
haftmann
parents: 15953
diff changeset
   390
16040
6e7616eba0b8 some adaptions
haftmann
parents: 15983
diff changeset
   391
*}
16075
8852058ecf8d added ? explanations
nipkow
parents: 16064
diff changeset
   392
(*<*)
16040
6e7616eba0b8 some adaptions
haftmann
parents: 15983
diff changeset
   393
setup {*
6e7616eba0b8 some adaptions
haftmann
parents: 15983
diff changeset
   394
let
6e7616eba0b8 some adaptions
haftmann
parents: 15983
diff changeset
   395
  fun my_concl ctxt = Logic.strip_imp_concl
6e7616eba0b8 some adaptions
haftmann
parents: 15983
diff changeset
   396
  in [TermStyle.add_style "my_concl" my_concl]
6e7616eba0b8 some adaptions
haftmann
parents: 15983
diff changeset
   397
end;
6e7616eba0b8 some adaptions
haftmann
parents: 15983
diff changeset
   398
*}
16075
8852058ecf8d added ? explanations
nipkow
parents: 16064
diff changeset
   399
(*>*)
16040
6e7616eba0b8 some adaptions
haftmann
parents: 15983
diff changeset
   400
text {*
6e7616eba0b8 some adaptions
haftmann
parents: 15983
diff changeset
   401
15917
cd4983c76548 Added short description of thm_style and term_style antiquotation
haftmann
parents: 15689
diff changeset
   402
  \begin{quote}
cd4983c76548 Added short description of thm_style and term_style antiquotation
haftmann
parents: 15689
diff changeset
   403
    \verb!setup {!\verb!*!\\
cd4983c76548 Added short description of thm_style and term_style antiquotation
haftmann
parents: 15689
diff changeset
   404
    \verb!let!\\
16040
6e7616eba0b8 some adaptions
haftmann
parents: 15983
diff changeset
   405
    \verb!  fun my_concl ctxt = Logic.strip_imp_concl!\\
6e7616eba0b8 some adaptions
haftmann
parents: 15983
diff changeset
   406
    \verb!  in [TermStyle.add_style "my_concl" my_concl]!\\
15917
cd4983c76548 Added short description of thm_style and term_style antiquotation
haftmann
parents: 15689
diff changeset
   407
    \verb!end;!\\
cd4983c76548 Added short description of thm_style and term_style antiquotation
haftmann
parents: 15689
diff changeset
   408
    \verb!*!\verb!}!\\
cd4983c76548 Added short description of thm_style and term_style antiquotation
haftmann
parents: 15689
diff changeset
   409
  \end{quote}
15960
9bd6550dc004 added Proof.context to antiquotation
haftmann
parents: 15953
diff changeset
   410
16076
03e8a88c0b54 tuned thm_style section
kleing
parents: 16075
diff changeset
   411
  \noindent
16165
dbe9ee8ffcdd concl antiqutations
haftmann
parents: 16155
diff changeset
   412
  This example shows how the \verb!concl! style is implemented
16076
03e8a88c0b54 tuned thm_style section
kleing
parents: 16075
diff changeset
   413
  and may be used as as a ``copy-and-paste'' pattern to write your own styles.
15960
9bd6550dc004 added Proof.context to antiquotation
haftmann
parents: 15953
diff changeset
   414
16076
03e8a88c0b54 tuned thm_style section
kleing
parents: 16075
diff changeset
   415
  The code should go into your theory file, separate from the \LaTeX\ text.
16040
6e7616eba0b8 some adaptions
haftmann
parents: 15983
diff changeset
   416
  The \verb!let! expression avoids polluting the
15960
9bd6550dc004 added Proof.context to antiquotation
haftmann
parents: 15953
diff changeset
   417
  ML global namespace. Each style receives the current proof context
16076
03e8a88c0b54 tuned thm_style section
kleing
parents: 16075
diff changeset
   418
  as first argument; this is helpful in situations where the
03e8a88c0b54 tuned thm_style section
kleing
parents: 16075
diff changeset
   419
  style has some object-logic specific behaviour for example.
15960
9bd6550dc004 added Proof.context to antiquotation
haftmann
parents: 15953
diff changeset
   420
9bd6550dc004 added Proof.context to antiquotation
haftmann
parents: 15953
diff changeset
   421
  The mapping from identifier name to the style function
16064
7953879aa6cf ML_idf antiquotation
haftmann
parents: 16040
diff changeset
   422
  is done by the @{ML_idf TermStyle.add_style} expression which expects the desired
15960
9bd6550dc004 added Proof.context to antiquotation
haftmann
parents: 15953
diff changeset
   423
  style name and the style function as arguments.
9bd6550dc004 added Proof.context to antiquotation
haftmann
parents: 15953
diff changeset
   424
  
9bd6550dc004 added Proof.context to antiquotation
haftmann
parents: 15953
diff changeset
   425
  After this \verb!setup!,
16040
6e7616eba0b8 some adaptions
haftmann
parents: 15983
diff changeset
   426
  there will be a new style available named \verb!my_concl!, thus allowing
6e7616eba0b8 some adaptions
haftmann
parents: 15983
diff changeset
   427
  antiquoations like \verb!@!\verb!{thm_style my_concl hd_Cons_tl}!
6e7616eba0b8 some adaptions
haftmann
parents: 15983
diff changeset
   428
  yielding @{thm_style my_concl hd_Cons_tl}.
15917
cd4983c76548 Added short description of thm_style and term_style antiquotation
haftmann
parents: 15689
diff changeset
   429
cd4983c76548 Added short description of thm_style and term_style antiquotation
haftmann
parents: 15689
diff changeset
   430
*}
cd4983c76548 Added short description of thm_style and term_style antiquotation
haftmann
parents: 15689
diff changeset
   431
15337
nipkow
parents:
diff changeset
   432
(*<*)
nipkow
parents:
diff changeset
   433
end
16175
nipkow
parents: 16167
diff changeset
   434
(*>*)