src/Doc/LaTeXsugar/Sugar.thy
author wenzelm
Mon, 07 Oct 2013 21:24:44 +0200
changeset 54313 da2e6282a4f5
parent 53015 a1119cf551e8
child 55417 01fbfb60c33e
permissions -rw-r--r--
native executable even for Linux, to avoid surprises with file managers opening executable script as text file;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
15337
nipkow
parents:
diff changeset
     1
(*<*)
nipkow
parents:
diff changeset
     2
theory Sugar
41413
64cd30d6b0b8 explicit file specifications -- avoid secondary load path;
wenzelm
parents: 38980
diff changeset
     3
imports "~~/src/HOL/Library/LaTeXsugar" "~~/src/HOL/Library/OptionalSugar"
15337
nipkow
parents:
diff changeset
     4
begin
nipkow
parents:
diff changeset
     5
(*>*)
49239
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
     6
text{*
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
     7
\section{Introduction}
15337
nipkow
parents:
diff changeset
     8
49239
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
     9
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}
49239
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
    48
15342
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
    49
49239
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
    50
\section{HOL syntax}
15342
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
    51
49239
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
    52
\subsection{Logic}
15342
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
    53
49239
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
    54
The formula @{prop[source]"\<not>(\<exists>x. P x)"} is typeset as @{prop"~(EX x. P x)"}.
16153
999ca183b4c7 \nexists und premsise1 .. 9
nipkow
parents: 16076
diff changeset
    55
999ca183b4c7 \nexists und premsise1 .. 9
nipkow
parents: 16076
diff changeset
    56
The predefined constructs @{text"if"}, @{text"let"} and
15342
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
    57
@{text"case"} are set in sans serif font to distinguish them from
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
    58
other functions. This improves readability:
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
    59
\begin{itemize}
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 49628
diff changeset
    60
\item @{term"if b then e\<^sub>1 else e\<^sub>2"} instead of @{text"if b then e\<^sub>1 else e\<^sub>2"}.
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 49628
diff changeset
    61
\item @{term"let x = e\<^sub>1 in e\<^sub>2"} instead of @{text"let x = e\<^sub>1 in e\<^sub>2"}.
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 49628
diff changeset
    62
\item @{term"case x of True \<Rightarrow> e\<^sub>1 | False \<Rightarrow> e\<^sub>2"} instead of\\
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 49628
diff changeset
    63
      @{text"case x of True \<Rightarrow> e\<^sub>1 | False \<Rightarrow> e\<^sub>2"}.
15342
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
    64
\end{itemize}
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
    65
49239
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
    66
\subsection{Sets}
15337
nipkow
parents:
diff changeset
    67
49239
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
    68
Although set syntax in HOL is already close to
15342
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
    69
standard, we provide a few further improvements:
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
    70
\begin{itemize}
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
    71
\item @{term"{x. P}"} instead of @{text"{x. P}"}.
27688
397de75836a1 *** empty log message ***
nipkow
parents: 27093
diff changeset
    72
\item @{term"{}"} instead of @{text"{}"}, where
397de75836a1 *** empty log message ***
nipkow
parents: 27093
diff changeset
    73
 @{term"{}"} is also input syntax.
15342
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
    74
\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
    75
\end{itemize}
49239
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
    76
15342
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
    77
49239
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
    78
\subsection{Lists}
15342
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
    79
49239
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
    80
If lists are used heavily, the following notations increase readability:
15342
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
    81
\begin{itemize}
27688
397de75836a1 *** empty log message ***
nipkow
parents: 27093
diff changeset
    82
\item @{term"x # xs"} instead of @{text"x # xs"},
397de75836a1 *** empty log message ***
nipkow
parents: 27093
diff changeset
    83
      where @{term"x # xs"} is also input syntax.
15342
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
    84
If you prefer more space around the $\cdot$ you have to redefine
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
    85
\verb!\isasymcdot! in \LaTeX:
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
    86
\verb!\renewcommand{\isasymcdot}{\isamath{\,\cdot\,}}!
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
    87
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
    88
\item @{term"length xs"} instead of @{text"length xs"}.
15385
26b05d4bc21a improvements by Larry and Micheal Wahler
kleing
parents: 15378
diff changeset
    89
\item @{term"nth xs n"} instead of @{text"nth xs n"},
15342
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
    90
      the $n$th element of @{text xs}.
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
    91
22834
bf67f798f063 added test about "set" supression
nipkow
parents: 22329
diff changeset
    92
\item Human readers are good at converting automatically from lists to
30502
b80d2621caee hiding numeric coercions in LaTeX
nipkow
parents: 27688
diff changeset
    93
sets. Hence \texttt{OptionalSugar} contains syntax for suppressing the
22834
bf67f798f063 added test about "set" supression
nipkow
parents: 22329
diff changeset
    94
conversion function @{const set}: for example, @{prop[source]"x \<in> set xs"}
bf67f798f063 added test about "set" supression
nipkow
parents: 22329
diff changeset
    95
becomes @{prop"x \<in> set xs"}.
bf67f798f063 added test about "set" supression
nipkow
parents: 22329
diff changeset
    96
15366
e6f595009734 more sugar
kleing
parents: 15342
diff changeset
    97
\item The @{text"@"} operation associates implicitly to the right,
e6f595009734 more sugar
kleing
parents: 15342
diff changeset
    98
which leads to unpleasant line breaks if the term is too long for one
e6f595009734 more sugar
kleing
parents: 15342
diff changeset
    99
line. To avoid this, \texttt{OptionalSugar} contains syntax to group
e6f595009734 more sugar
kleing
parents: 15342
diff changeset
   100
@{text"@"}-terms to the left before printing, which leads to better
e6f595009734 more sugar
kleing
parents: 15342
diff changeset
   101
line breaking behaviour:
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 49628
diff changeset
   102
@{term[display]"term\<^sub>0 @ term\<^sub>1 @ term\<^sub>2 @ term\<^sub>3 @ term\<^sub>4 @ term\<^sub>5 @ term\<^sub>6 @ term\<^sub>7 @ term\<^sub>8 @ term\<^sub>9 @ term\<^sub>1\<^sub>0"}
15366
e6f595009734 more sugar
kleing
parents: 15342
diff changeset
   103
15342
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
   104
\end{itemize}
49239
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   105
15337
nipkow
parents:
diff changeset
   106
49239
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   107
\subsection{Numbers}
30502
b80d2621caee hiding numeric coercions in LaTeX
nipkow
parents: 27688
diff changeset
   108
49239
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   109
Coercions between numeric types are alien to mathematicians who
30502
b80d2621caee hiding numeric coercions in LaTeX
nipkow
parents: 27688
diff changeset
   110
consider, for example, @{typ nat} as a subset of @{typ int}.
b80d2621caee hiding numeric coercions in LaTeX
nipkow
parents: 27688
diff changeset
   111
\texttt{OptionalSugar} contains syntax for suppressing numeric coercions such
b80d2621caee hiding numeric coercions in LaTeX
nipkow
parents: 27688
diff changeset
   112
as @{const int} @{text"::"} @{typ"nat \<Rightarrow> int"}. For example,
b80d2621caee hiding numeric coercions in LaTeX
nipkow
parents: 27688
diff changeset
   113
@{term[source]"int 5"} is printed as @{term "int 5"}. Embeddings of types
b80d2621caee hiding numeric coercions in LaTeX
nipkow
parents: 27688
diff changeset
   114
@{typ nat}, @{typ int}, @{typ real} are covered; non-injective coercions such
b80d2621caee hiding numeric coercions in LaTeX
nipkow
parents: 27688
diff changeset
   115
as @{const nat} @{text"::"} @{typ"int \<Rightarrow> nat"} are not and should not be
49239
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   116
hidden.
30502
b80d2621caee hiding numeric coercions in LaTeX
nipkow
parents: 27688
diff changeset
   117
15337
nipkow
parents:
diff changeset
   118
49239
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   119
\section{Printing theorems}
15689
621bd0d8048f section on qmark
nipkow
parents: 15673
diff changeset
   120
49239
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   121
\subsection{Question marks}
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   122
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   123
If you print anything, especially theorems, containing
15689
621bd0d8048f section on qmark
nipkow
parents: 15673
diff changeset
   124
schematic variables they are prefixed with a question mark:
621bd0d8048f section on qmark
nipkow
parents: 15673
diff changeset
   125
\verb!@!\verb!{thm conjI}! results in @{thm conjI}. Most of the time
621bd0d8048f section on qmark
nipkow
parents: 15673
diff changeset
   126
you would rather not see the question marks. There is an attribute
621bd0d8048f section on qmark
nipkow
parents: 15673
diff changeset
   127
\verb!no_vars! that you can attach to the theorem that turns its
621bd0d8048f section on qmark
nipkow
parents: 15673
diff changeset
   128
schematic into ordinary free variables: \verb!@!\verb!{thm conjI[no_vars]}!
621bd0d8048f section on qmark
nipkow
parents: 15673
diff changeset
   129
results in @{thm conjI[no_vars]}.
621bd0d8048f section on qmark
nipkow
parents: 15673
diff changeset
   130
621bd0d8048f section on qmark
nipkow
parents: 15673
diff changeset
   131
This \verb!no_vars! business can become a bit tedious.
621bd0d8048f section on qmark
nipkow
parents: 15673
diff changeset
   132
If you would rather never see question marks, simply put
34877
ded5b770ec1c formal antiquotations for ML snippets; no "open" unsynchronized references
haftmann
parents: 33323
diff changeset
   133
\begin{quote}
49239
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   134
\verb!options [show_question_marks = false]!
34877
ded5b770ec1c formal antiquotations for ML snippets; no "open" unsynchronized references
haftmann
parents: 33323
diff changeset
   135
\end{quote}
49239
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   136
into the relevant \texttt{ROOT} file, just before the \texttt{theories} for that session.
33323
1932908057c7 small fixes
nipkow
parents: 32898
diff changeset
   137
The rest of this document is produced with this flag set to \texttt{false}.
16075
8852058ecf8d added ? explanations
nipkow
parents: 16064
diff changeset
   138
49239
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   139
Hint: Setting \verb!show_question_marks! to \texttt{false} only
33323
1932908057c7 small fixes
nipkow
parents: 32898
diff changeset
   140
suppresses question marks; variables that end in digits,
1932908057c7 small fixes
nipkow
parents: 32898
diff changeset
   141
e.g. @{text"x1"}, are still printed with a trailing @{text".0"},
1932908057c7 small fixes
nipkow
parents: 32898
diff changeset
   142
e.g. @{text"x1.0"}, their internal index. This can be avoided by
53015
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 49628
diff changeset
   143
turning the last digit into a subscript: write \verb!x\<^sub>1! and
a1119cf551e8 standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents: 49628
diff changeset
   144
obtain the much nicer @{text"x\<^sub>1"}. *}
15689
621bd0d8048f section on qmark
nipkow
parents: 15673
diff changeset
   145
38980
af73cf0dc31f turned show_question_marks into proper configuration option;
wenzelm
parents: 38798
diff changeset
   146
(*<*)declare [[show_question_marks = false]](*>*)
15689
621bd0d8048f section on qmark
nipkow
parents: 15673
diff changeset
   147
24496
65f3b37f80b7 added short_names explanation
nipkow
parents: 22834
diff changeset
   148
subsection {*Qualified names*}
65f3b37f80b7 added short_names explanation
nipkow
parents: 22834
diff changeset
   149
65f3b37f80b7 added short_names explanation
nipkow
parents: 22834
diff changeset
   150
text{* If there are multiple declarations of the same name, Isabelle prints
65f3b37f80b7 added short_names explanation
nipkow
parents: 22834
diff changeset
   151
the qualified name, for example @{text "T.length"}, where @{text T} is the
65f3b37f80b7 added short_names explanation
nipkow
parents: 22834
diff changeset
   152
theory it is defined in, to distinguish it from the predefined @{const[source]
65f3b37f80b7 added short_names explanation
nipkow
parents: 22834
diff changeset
   153
"List.length"}. In case there is no danger of confusion, you can insist on
42669
04dfffda5671 more conventional naming scheme: names_long, names_short, names_unique;
wenzelm
parents: 42358
diff changeset
   154
short names (no qualifiers) by setting the \verb!names_short!
42358
b47d41d9f4b5 Name_Space: proper configuration options long_names, short_names, unique_names instead of former unsynchronized references;
wenzelm
parents: 42289
diff changeset
   155
configuration option in the context.
49239
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   156
24496
65f3b37f80b7 added short_names explanation
nipkow
parents: 22834
diff changeset
   157
49239
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   158
\subsection {Variable names\label{sec:varnames}}
16395
3446d2b6a19f documented DUMMY
nipkow
parents: 16175
diff changeset
   159
49239
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   160
It sometimes happens that you want to change the name of a
16395
3446d2b6a19f documented DUMMY
nipkow
parents: 16175
diff changeset
   161
variable in a theorem before printing it. This can easily be achieved
3446d2b6a19f documented DUMMY
nipkow
parents: 16175
diff changeset
   162
with the help of Isabelle's instantiation attribute \texttt{where}:
3446d2b6a19f documented DUMMY
nipkow
parents: 16175
diff changeset
   163
@{thm conjI[where P = \<phi> and Q = \<psi>]} is the result of
3446d2b6a19f documented DUMMY
nipkow
parents: 16175
diff changeset
   164
\begin{quote}
3446d2b6a19f documented DUMMY
nipkow
parents: 16175
diff changeset
   165
\verb!@!\verb!{thm conjI[where P = \<phi> and Q = \<psi>]}!
3446d2b6a19f documented DUMMY
nipkow
parents: 16175
diff changeset
   166
\end{quote}
3446d2b6a19f documented DUMMY
nipkow
parents: 16175
diff changeset
   167
To support the ``\_''-notation for irrelevant variables
3446d2b6a19f documented DUMMY
nipkow
parents: 16175
diff changeset
   168
the constant \texttt{DUMMY} has been introduced:
3446d2b6a19f documented DUMMY
nipkow
parents: 16175
diff changeset
   169
@{thm fst_conv[where b = DUMMY]} is produced by
3446d2b6a19f documented DUMMY
nipkow
parents: 16175
diff changeset
   170
\begin{quote}
3446d2b6a19f documented DUMMY
nipkow
parents: 16175
diff changeset
   171
\verb!@!\verb!{thm fst_conv[where b = DUMMY]}!
3446d2b6a19f documented DUMMY
nipkow
parents: 16175
diff changeset
   172
\end{quote}
36138
1faa0fc34174 advertise [rename_abs] attribute in LaTeXsugar -- wish I had known about this earier.
krauss
parents: 34890
diff changeset
   173
Variables that are bound by quantifiers or lambdas cannot be renamed
1faa0fc34174 advertise [rename_abs] attribute in LaTeXsugar -- wish I had known about this earier.
krauss
parents: 34890
diff changeset
   174
like this. Instead, the attribute \texttt{rename\_abs} does the
1faa0fc34174 advertise [rename_abs] attribute in LaTeXsugar -- wish I had known about this earier.
krauss
parents: 34890
diff changeset
   175
job. It expects a list of names or underscores, similar to the
1faa0fc34174 advertise [rename_abs] attribute in LaTeXsugar -- wish I had known about this earier.
krauss
parents: 34890
diff changeset
   176
\texttt{of} attribute:
1faa0fc34174 advertise [rename_abs] attribute in LaTeXsugar -- wish I had known about this earier.
krauss
parents: 34890
diff changeset
   177
\begin{quote}
1faa0fc34174 advertise [rename_abs] attribute in LaTeXsugar -- wish I had known about this earier.
krauss
parents: 34890
diff changeset
   178
\verb!@!\verb!{thm split_paired_All[rename_abs _ l r]}!
1faa0fc34174 advertise [rename_abs] attribute in LaTeXsugar -- wish I had known about this earier.
krauss
parents: 34890
diff changeset
   179
\end{quote}
1faa0fc34174 advertise [rename_abs] attribute in LaTeXsugar -- wish I had known about this earier.
krauss
parents: 34890
diff changeset
   180
produces @{thm split_paired_All[rename_abs _ l r]}.
49239
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   181
16395
3446d2b6a19f documented DUMMY
nipkow
parents: 16175
diff changeset
   182
49239
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   183
\subsection{Inference rules}
15337
nipkow
parents:
diff changeset
   184
49239
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   185
To print theorems as inference rules you need to include Didier
15342
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
   186
R\'emy's \texttt{mathpartir} package~\cite{mathpartir}
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
   187
for typesetting inference rules in your \LaTeX\ file.
15337
nipkow
parents:
diff changeset
   188
15689
621bd0d8048f section on qmark
nipkow
parents: 15673
diff changeset
   189
Writing \verb!@!\verb!{thm[mode=Rule] conjI}! produces
621bd0d8048f section on qmark
nipkow
parents: 15673
diff changeset
   190
@{thm[mode=Rule] conjI}, even in the middle of a sentence.
15342
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
   191
If you prefer your inference rule on a separate line, maybe with a name,
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
   192
\begin{center}
15689
621bd0d8048f section on qmark
nipkow
parents: 15673
diff changeset
   193
@{thm[mode=Rule] conjI} {\sc conjI}
15342
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
   194
\end{center}
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
   195
is produced by
15337
nipkow
parents:
diff changeset
   196
\begin{quote}
nipkow
parents:
diff changeset
   197
\verb!\begin{center}!\\
15689
621bd0d8048f section on qmark
nipkow
parents: 15673
diff changeset
   198
\verb!@!\verb!{thm[mode=Rule] conjI} {\sc conjI}!\\
15337
nipkow
parents:
diff changeset
   199
\verb!\end{center}!
nipkow
parents:
diff changeset
   200
\end{quote}
24497
7840f760a744 explained \isatstyle(minor)
nipkow
parents: 24496
diff changeset
   201
It is not recommended to use the standard \texttt{display} option
15342
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
   202
together with \texttt{Rule} because centering does not work and because
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
   203
the line breaking mechanisms of \texttt{display} and \texttt{mathpartir} can
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
   204
clash.
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
   205
15337
nipkow
parents:
diff changeset
   206
Of course you can display multiple rules in this fashion:
nipkow
parents:
diff changeset
   207
\begin{quote}
24497
7840f760a744 explained \isatstyle(minor)
nipkow
parents: 24496
diff changeset
   208
\verb!\begin{center}!\\
15689
621bd0d8048f section on qmark
nipkow
parents: 15673
diff changeset
   209
\verb!@!\verb!{thm[mode=Rule] conjI} {\sc conjI} \\[1ex]!\\
621bd0d8048f section on qmark
nipkow
parents: 15673
diff changeset
   210
\verb!@!\verb!{thm[mode=Rule] conjE} {\sc disjI$_1$} \qquad!\\
621bd0d8048f section on qmark
nipkow
parents: 15673
diff changeset
   211
\verb!@!\verb!{thm[mode=Rule] disjE} {\sc disjI$_2$}!\\
15337
nipkow
parents:
diff changeset
   212
\verb!\end{center}!
nipkow
parents:
diff changeset
   213
\end{quote}
nipkow
parents:
diff changeset
   214
yields
24497
7840f760a744 explained \isatstyle(minor)
nipkow
parents: 24496
diff changeset
   215
\begin{center}\small
15689
621bd0d8048f section on qmark
nipkow
parents: 15673
diff changeset
   216
@{thm[mode=Rule] conjI} {\sc conjI} \\[1ex]
621bd0d8048f section on qmark
nipkow
parents: 15673
diff changeset
   217
@{thm[mode=Rule] disjI1} {\sc disjI$_1$} \qquad
621bd0d8048f section on qmark
nipkow
parents: 15673
diff changeset
   218
@{thm[mode=Rule] disjI2} {\sc disjI$_2$}
15337
nipkow
parents:
diff changeset
   219
\end{center}
nipkow
parents:
diff changeset
   220
15342
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
   221
The \texttt{mathpartir} package copes well if there are too many
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
   222
premises for one line:
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
   223
\begin{center}
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
   224
@{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
   225
 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
   226
\end{center}
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
   227
15471
e7f069887ec2 *** empty log message ***
nipkow
parents: 15428
diff changeset
   228
Limitations: 1. Premises and conclusion must each not be longer than
e7f069887ec2 *** empty log message ***
nipkow
parents: 15428
diff changeset
   229
the line.  2. Premises that are @{text"\<Longrightarrow>"}-implications are again
e7f069887ec2 *** empty log message ***
nipkow
parents: 15428
diff changeset
   230
displayed with a horizontal line, which looks at least unusual.
e7f069887ec2 *** empty log message ***
nipkow
parents: 15428
diff changeset
   231
22329
e4325ce4e0c4 added example for print-mode Axiom
schirmer
parents: 21558
diff changeset
   232
e4325ce4e0c4 added example for print-mode Axiom
schirmer
parents: 21558
diff changeset
   233
In case you print theorems without premises no rule will be printed by the
e4325ce4e0c4 added example for print-mode Axiom
schirmer
parents: 21558
diff changeset
   234
\texttt{Rule} print mode. However, you can use \texttt{Axiom} instead:
e4325ce4e0c4 added example for print-mode Axiom
schirmer
parents: 21558
diff changeset
   235
\begin{quote}
24497
7840f760a744 explained \isatstyle(minor)
nipkow
parents: 24496
diff changeset
   236
\verb!\begin{center}!\\
22329
e4325ce4e0c4 added example for print-mode Axiom
schirmer
parents: 21558
diff changeset
   237
\verb!@!\verb!{thm[mode=Axiom] refl} {\sc refl}! \\
e4325ce4e0c4 added example for print-mode Axiom
schirmer
parents: 21558
diff changeset
   238
\verb!\end{center}!
e4325ce4e0c4 added example for print-mode Axiom
schirmer
parents: 21558
diff changeset
   239
\end{quote}
e4325ce4e0c4 added example for print-mode Axiom
schirmer
parents: 21558
diff changeset
   240
yields
24497
7840f760a744 explained \isatstyle(minor)
nipkow
parents: 24496
diff changeset
   241
\begin{center}
22329
e4325ce4e0c4 added example for print-mode Axiom
schirmer
parents: 21558
diff changeset
   242
@{thm[mode=Axiom] refl} {\sc refl} 
e4325ce4e0c4 added example for print-mode Axiom
schirmer
parents: 21558
diff changeset
   243
\end{center}
49239
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   244
15342
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
   245
49239
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   246
\subsection{Displays and font sizes}
24497
7840f760a744 explained \isatstyle(minor)
nipkow
parents: 24496
diff changeset
   247
49239
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   248
When displaying theorems with the \texttt{display} option, for example as in
24497
7840f760a744 explained \isatstyle(minor)
nipkow
parents: 24496
diff changeset
   249
\verb!@!\verb!{thm[display] refl}! @{thm[display] refl} the theorem is
7840f760a744 explained \isatstyle(minor)
nipkow
parents: 24496
diff changeset
   250
set in small font. It uses the \LaTeX-macro \verb!\isastyle!,
7840f760a744 explained \isatstyle(minor)
nipkow
parents: 24496
diff changeset
   251
which is also the style that regular theory text is set in, e.g. *}
7840f760a744 explained \isatstyle(minor)
nipkow
parents: 24496
diff changeset
   252
7840f760a744 explained \isatstyle(minor)
nipkow
parents: 24496
diff changeset
   253
lemma "t = t"
7840f760a744 explained \isatstyle(minor)
nipkow
parents: 24496
diff changeset
   254
(*<*)oops(*>*)
7840f760a744 explained \isatstyle(minor)
nipkow
parents: 24496
diff changeset
   255
7840f760a744 explained \isatstyle(minor)
nipkow
parents: 24496
diff changeset
   256
text{* \noindent Otherwise \verb!\isastyleminor! is used,
7840f760a744 explained \isatstyle(minor)
nipkow
parents: 24496
diff changeset
   257
which does not modify the font size (assuming you stick to the default
7840f760a744 explained \isatstyle(minor)
nipkow
parents: 24496
diff changeset
   258
\verb!\isabellestyle{it}! in \texttt{root.tex}). If you prefer
7840f760a744 explained \isatstyle(minor)
nipkow
parents: 24496
diff changeset
   259
normal font size throughout your text, include
7840f760a744 explained \isatstyle(minor)
nipkow
parents: 24496
diff changeset
   260
\begin{quote}
7840f760a744 explained \isatstyle(minor)
nipkow
parents: 24496
diff changeset
   261
\verb!\renewcommand{\isastyle}{\isastyleminor}!
7840f760a744 explained \isatstyle(minor)
nipkow
parents: 24496
diff changeset
   262
\end{quote}
7840f760a744 explained \isatstyle(minor)
nipkow
parents: 24496
diff changeset
   263
in \texttt{root.tex}. On the other hand, if you like the small font,
7840f760a744 explained \isatstyle(minor)
nipkow
parents: 24496
diff changeset
   264
just put \verb!\isastyle! in front of the text in question,
7840f760a744 explained \isatstyle(minor)
nipkow
parents: 24496
diff changeset
   265
e.g.\ at the start of one of the center-environments above.
7840f760a744 explained \isatstyle(minor)
nipkow
parents: 24496
diff changeset
   266
7840f760a744 explained \isatstyle(minor)
nipkow
parents: 24496
diff changeset
   267
The advantage of the display option is that you can display a whole
7840f760a744 explained \isatstyle(minor)
nipkow
parents: 24496
diff changeset
   268
list of theorems in one go. For example,
46187
f009e0fe8643 updated example -- List.foldl is no longer defined via primrec;
wenzelm
parents: 42669
diff changeset
   269
\verb!@!\verb!{thm[display] append.simps}!
f009e0fe8643 updated example -- List.foldl is no longer defined via primrec;
wenzelm
parents: 42669
diff changeset
   270
generates @{thm[display] append.simps}
49239
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   271
24497
7840f760a744 explained \isatstyle(minor)
nipkow
parents: 24496
diff changeset
   272
49239
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   273
\subsection{If-then}
15342
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
   274
49239
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   275
If you prefer a fake ``natural language'' style you can produce
15342
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
   276
the body of
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
   277
\newtheorem{theorem}{Theorem}
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
   278
\begin{theorem}
15689
621bd0d8048f section on qmark
nipkow
parents: 15673
diff changeset
   279
@{thm[mode=IfThen] le_trans}
15342
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
   280
\end{theorem}
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
   281
by typing
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
   282
\begin{quote}
15689
621bd0d8048f section on qmark
nipkow
parents: 15673
diff changeset
   283
\verb!@!\verb!{thm[mode=IfThen] le_trans}!
15342
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
   284
\end{quote}
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
   285
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
   286
In order to prevent odd line breaks, the premises are put into boxes.
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
   287
At times this is too drastic:
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
   288
\begin{theorem}
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
   289
@{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
   290
\end{theorem}
16153
999ca183b4c7 \nexists und premsise1 .. 9
nipkow
parents: 16076
diff changeset
   291
In which case you should use \texttt{IfThenNoBox} instead of
999ca183b4c7 \nexists und premsise1 .. 9
nipkow
parents: 16076
diff changeset
   292
\texttt{IfThen}:
15342
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
   293
\begin{theorem}
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
   294
@{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
   295
\end{theorem}
49239
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   296
15342
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
   297
49239
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   298
\subsection{Doing it yourself\label{sec:yourself}}
16153
999ca183b4c7 \nexists und premsise1 .. 9
nipkow
parents: 16076
diff changeset
   299
49239
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   300
If for some reason you want or need to present theorems your
16153
999ca183b4c7 \nexists und premsise1 .. 9
nipkow
parents: 16076
diff changeset
   301
own way, you can extract the premises and the conclusion explicitly
999ca183b4c7 \nexists und premsise1 .. 9
nipkow
parents: 16076
diff changeset
   302
and combine them as you like:
999ca183b4c7 \nexists und premsise1 .. 9
nipkow
parents: 16076
diff changeset
   303
\begin{itemize}
32891
d403b99287ff new generalized concept for term styles
haftmann
parents: 32833
diff changeset
   304
\item \verb!@!\verb!{thm (prem 1)! $thm$\verb!}!
d403b99287ff new generalized concept for term styles
haftmann
parents: 32833
diff changeset
   305
prints premise 1 of $thm$.
d403b99287ff new generalized concept for term styles
haftmann
parents: 32833
diff changeset
   306
\item \verb!@!\verb!{thm (concl)! $thm$\verb!}!
16153
999ca183b4c7 \nexists und premsise1 .. 9
nipkow
parents: 16076
diff changeset
   307
prints the conclusion of $thm$.
999ca183b4c7 \nexists und premsise1 .. 9
nipkow
parents: 16076
diff changeset
   308
\end{itemize}
32891
d403b99287ff new generalized concept for term styles
haftmann
parents: 32833
diff changeset
   309
For example, ``from @{thm (prem 2) conjI} and
d403b99287ff new generalized concept for term styles
haftmann
parents: 32833
diff changeset
   310
@{thm (prem 1) conjI} we conclude @{thm (concl) conjI}''
16153
999ca183b4c7 \nexists und premsise1 .. 9
nipkow
parents: 16076
diff changeset
   311
is produced by
999ca183b4c7 \nexists und premsise1 .. 9
nipkow
parents: 16076
diff changeset
   312
\begin{quote}
32891
d403b99287ff new generalized concept for term styles
haftmann
parents: 32833
diff changeset
   313
\verb!from !\verb!@!\verb!{thm (prem 2) conjI}! \verb!and !\verb!@!\verb!{thm (prem 1) conjI}!\\
d403b99287ff new generalized concept for term styles
haftmann
parents: 32833
diff changeset
   314
\verb!we conclude !\verb!@!\verb!{thm (concl) conjI}!
16153
999ca183b4c7 \nexists und premsise1 .. 9
nipkow
parents: 16076
diff changeset
   315
\end{quote}
999ca183b4c7 \nexists und premsise1 .. 9
nipkow
parents: 16076
diff changeset
   316
Thus you can rearrange or hide premises and typeset the theorem as you like.
32898
e871d897969c term styles also cover antiquotations term_type and typeof
haftmann
parents: 32891
diff changeset
   317
Styles like \verb!(prem 1)! are a general mechanism explained
16153
999ca183b4c7 \nexists und premsise1 .. 9
nipkow
parents: 16076
diff changeset
   318
in \S\ref{sec:styles}.
49239
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   319
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   320
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   321
\subsection{Patterns}
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   322
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   323
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   324
In \S\ref{sec:varnames} we shows how to create patterns containing ``@{term DUMMY}''.
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   325
You can drive this game even further and extend the syntax of let
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   326
bindings such that certain functions like @{term fst}, @{term hd}, 
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   327
etc.\ are printed as patterns. \texttt{OptionalSugar} provides the following:
16153
999ca183b4c7 \nexists und premsise1 .. 9
nipkow
parents: 16076
diff changeset
   328
49239
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   329
\begin{center}
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   330
\begin{tabular}{l@ {~~produced by~~}l}
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   331
@{term "let x = fst p in t"} & \verb!@!\verb!{term "let x = fst p in t"}!\\
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   332
@{term "let x = snd p in t"} & \verb!@!\verb!{term "let x = snd p in t"}!\\
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   333
@{term "let x = hd xs in t"} & \verb!@!\verb!{term "let x = hd xs in t"}!\\
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   334
@{term "let x = tl xs in t"} & \verb!@!\verb!{term "let x = tl xs in t"}!\\
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   335
@{term "let x = the y in t"} & \verb!@!\verb!{term "let x = the y in t"}!\\
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   336
\end{tabular}
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   337
\end{center}
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   338
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   339
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   340
\section {Styles\label{sec:styles}}
15366
e6f595009734 more sugar
kleing
parents: 15342
diff changeset
   341
49239
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   342
The \verb!thm! antiquotation works nicely for single theorems, but
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   343
sets of equations as used in definitions are more difficult to
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   344
typeset nicely: people tend to prefer aligned @{text "="} signs.
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   345
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   346
To deal with such cases where it is desirable to dive into the structure
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   347
of terms and theorems, Isabelle offers antiquotations featuring ``styles'':
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   348
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   349
\begin{quote}
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   350
\verb!@!\verb!{thm (style) thm}!\\
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   351
\verb!@!\verb!{prop (style) thm}!\\
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   352
\verb!@!\verb!{term (style) term}!\\
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   353
\verb!@!\verb!{term_type (style) term}!\\
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   354
\verb!@!\verb!{typeof (style) term}!\\
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   355
\end{quote}
15366
e6f595009734 more sugar
kleing
parents: 15342
diff changeset
   356
49239
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   357
 A ``style'' is a transformation of a term. There are predefined
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   358
 styles, namely \verb!lhs! and \verb!rhs!, \verb!prem! with one argument, and \verb!concl!.
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   359
For example, the output
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   360
\begin{center}
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   361
\begin{tabular}{l@ {~~@{text "="}~~}l}
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   362
@{thm (lhs) append_Nil} & @{thm (rhs) append_Nil}\\
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   363
@{thm (lhs) append_Cons} & @{thm (rhs) append_Cons}
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   364
\end{tabular}
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   365
\end{center}
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   366
is produced by the following code:
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   367
\begin{quote}
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   368
  \verb!\begin{center}!\\
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   369
  \verb!\begin{tabular}{l@ {~~!\verb!@!\verb!{text "="}~~}l}!\\
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   370
  \verb!@!\verb!{thm (lhs) append_Nil} & @!\verb!{thm (rhs) append_Nil}\\!\\
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   371
  \verb!@!\verb!{thm (lhs) append_Cons} & @!\verb!{thm (rhs) append_Cons}!\\
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   372
  \verb!\end{tabular}!\\
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   373
  \verb!\end{center}!
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   374
\end{quote}
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   375
Note the space between \verb!@! and \verb!{! in the tabular argument.
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   376
It prevents Isabelle from interpreting \verb!@ {~~...~~}! 
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   377
as an antiquotation. The styles \verb!lhs! and \verb!rhs!
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   378
extract the left hand side (or right hand side respectively) from the
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   379
conclusion of propositions consisting of a binary operator
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   380
(e.~g.~@{text "="}, @{text "\<equiv>"}, @{text "<"}).
15366
e6f595009734 more sugar
kleing
parents: 15342
diff changeset
   381
49239
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   382
Likewise, \verb!concl! may be used as a style to show just the
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   383
conclusion of a proposition. For example, take \verb!hd_Cons_tl!:
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   384
\begin{center}
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   385
  @{thm hd_Cons_tl}
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   386
\end{center}
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   387
To print just the conclusion,
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   388
\begin{center}
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   389
  @{thm (concl) hd_Cons_tl}
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   390
\end{center}
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   391
type
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   392
\begin{quote}
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   393
  \verb!\begin{center}!\\
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   394
  \verb!@!\verb!{thm (concl) hd_Cons_tl}!\\
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   395
  \verb!\end{center}!
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   396
\end{quote}
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   397
Beware that any options must be placed \emph{before} the style, as in this example.
15366
e6f595009734 more sugar
kleing
parents: 15342
diff changeset
   398
49239
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   399
Further use cases can be found in \S\ref{sec:yourself}.
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   400
If you are not afraid of ML, you may also define your own styles.
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   401
Have a look at module @{ML_struct Term_Style}.
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   402
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   403
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   404
\section {Proofs}
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   405
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   406
Full proofs, even if written in beautiful Isar style, are
24497
7840f760a744 explained \isatstyle(minor)
nipkow
parents: 24496
diff changeset
   407
likely to be too long and detailed to be included in conference
7840f760a744 explained \isatstyle(minor)
nipkow
parents: 24496
diff changeset
   408
papers, but some key lemmas might be of interest.
7840f760a744 explained \isatstyle(minor)
nipkow
parents: 24496
diff changeset
   409
It is usually easiest to put them in figures like the one in Fig.\
7840f760a744 explained \isatstyle(minor)
nipkow
parents: 24496
diff changeset
   410
\ref{fig:proof}. This was achieved with the \isakeyword{text\_raw} command:
15366
e6f595009734 more sugar
kleing
parents: 15342
diff changeset
   411
*}
e6f595009734 more sugar
kleing
parents: 15342
diff changeset
   412
text_raw {*
e6f595009734 more sugar
kleing
parents: 15342
diff changeset
   413
  \begin{figure}
e6f595009734 more sugar
kleing
parents: 15342
diff changeset
   414
  \begin{center}\begin{minipage}{0.6\textwidth}  
24497
7840f760a744 explained \isatstyle(minor)
nipkow
parents: 24496
diff changeset
   415
  \isastyleminor\isamarkuptrue
15366
e6f595009734 more sugar
kleing
parents: 15342
diff changeset
   416
*}
e6f595009734 more sugar
kleing
parents: 15342
diff changeset
   417
lemma True
e6f595009734 more sugar
kleing
parents: 15342
diff changeset
   418
proof -
e6f595009734 more sugar
kleing
parents: 15342
diff changeset
   419
  -- "pretty trivial"
e6f595009734 more sugar
kleing
parents: 15342
diff changeset
   420
  show True by force
e6f595009734 more sugar
kleing
parents: 15342
diff changeset
   421
qed
15428
3f1a674b7ec7 suggestions by Jeremy Siek
kleing
parents: 15385
diff changeset
   422
text_raw {*    
15366
e6f595009734 more sugar
kleing
parents: 15342
diff changeset
   423
  \end{minipage}\end{center}
e6f595009734 more sugar
kleing
parents: 15342
diff changeset
   424
  \caption{Example proof in a figure.}\label{fig:proof}
e6f595009734 more sugar
kleing
parents: 15342
diff changeset
   425
  \end{figure}
e6f595009734 more sugar
kleing
parents: 15342
diff changeset
   426
*}
e6f595009734 more sugar
kleing
parents: 15342
diff changeset
   427
text {*
e6f595009734 more sugar
kleing
parents: 15342
diff changeset
   428
e6f595009734 more sugar
kleing
parents: 15342
diff changeset
   429
\begin{quote}
e6f595009734 more sugar
kleing
parents: 15342
diff changeset
   430
\small
e6f595009734 more sugar
kleing
parents: 15342
diff changeset
   431
\verb!text_raw {!\verb!*!\\
e6f595009734 more sugar
kleing
parents: 15342
diff changeset
   432
\verb!  \begin{figure}!\\
e6f595009734 more sugar
kleing
parents: 15342
diff changeset
   433
\verb!  \begin{center}\begin{minipage}{0.6\textwidth}!\\
24497
7840f760a744 explained \isatstyle(minor)
nipkow
parents: 24496
diff changeset
   434
\verb!  \isastyleminor\isamarkuptrue!\\
15366
e6f595009734 more sugar
kleing
parents: 15342
diff changeset
   435
\verb!*!\verb!}!\\
e6f595009734 more sugar
kleing
parents: 15342
diff changeset
   436
\verb!lemma True!\\
e6f595009734 more sugar
kleing
parents: 15342
diff changeset
   437
\verb!proof -!\\
e6f595009734 more sugar
kleing
parents: 15342
diff changeset
   438
\verb!  -- "pretty trivial"!\\
e6f595009734 more sugar
kleing
parents: 15342
diff changeset
   439
\verb!  show True by force!\\
e6f595009734 more sugar
kleing
parents: 15342
diff changeset
   440
\verb!qed!\\
e6f595009734 more sugar
kleing
parents: 15342
diff changeset
   441
\verb!text_raw {!\verb!*!\\
e6f595009734 more sugar
kleing
parents: 15342
diff changeset
   442
\verb!  \end{minipage}\end{center}!\\
e6f595009734 more sugar
kleing
parents: 15342
diff changeset
   443
\verb!  \caption{Example proof in a figure.}\label{fig:proof}!\\
e6f595009734 more sugar
kleing
parents: 15342
diff changeset
   444
\verb!  \end{figure}!\\
e6f595009734 more sugar
kleing
parents: 15342
diff changeset
   445
\verb!*!\verb!}!
e6f595009734 more sugar
kleing
parents: 15342
diff changeset
   446
\end{quote}
24497
7840f760a744 explained \isatstyle(minor)
nipkow
parents: 24496
diff changeset
   447
7840f760a744 explained \isatstyle(minor)
nipkow
parents: 24496
diff changeset
   448
Other theory text, e.g.\ definitions, can be put in figures, too.
15342
13bd3d12ec2f *** empty log message ***
nipkow
parents: 15337
diff changeset
   449
49239
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   450
\section{Theory snippets}
15917
cd4983c76548 Added short description of thm_style and term_style antiquotation
haftmann
parents: 15689
diff changeset
   451
49239
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   452
This section describes how to include snippets of a theory text in some other \LaTeX\ document.
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   453
The typical scenario is that the description of your theory is not part of the theory text but
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   454
a separate document that antiquotes bits of the theory. This works well for terms and theorems
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   455
but there are no antiquotations, for example, for function definitions or proofs. Even if there are antiquotations,
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   456
the output is usually a reformatted (by Isabelle) version of the input and may not look like
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   457
you wanted it to look. Here is how to include a snippet of theory text (in \LaTeX\ form) in some
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   458
other \LaTeX\ document, in 4 easy steps. Beware that these snippets are not processed by
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   459
any antiquotation mechanism: the resulting \LaTeX\ text is more or less exactly what you wrote
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   460
in the theory, without any added sugar.
15917
cd4983c76548 Added short description of thm_style and term_style antiquotation
haftmann
parents: 15689
diff changeset
   461
49239
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   462
\subsection{Theory markup}
15917
cd4983c76548 Added short description of thm_style and term_style antiquotation
haftmann
parents: 15689
diff changeset
   463
49239
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   464
Include some markers at the beginning and the end of the theory snippet you want to cut out.
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   465
You have to place the following lines before and after the snippet, where snippets must always be
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   466
consecutive lines of theory text:
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   467
\begin{quote}
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   468
\verb!\text_raw{!\verb!*\snip{!\emph{snippetname}\verb!}{1}{2}{%*!\verb!}!\\
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   469
\emph{theory text}\\
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   470
\verb!\text_raw{!\verb!*!\verb!}%endsnip*!\verb!}!
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   471
\end{quote}
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   472
where \emph{snippetname} should be a unique name for the snippet. The numbers \texttt{1}
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   473
and \texttt{2} are explained in a moment.
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   474
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   475
\subsection{Generate the \texttt{.tex} file}
15917
cd4983c76548 Added short description of thm_style and term_style antiquotation
haftmann
parents: 15689
diff changeset
   476
49239
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   477
Run your theory \texttt{T} with the \texttt{isabelle} \texttt{build} tool
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   478
to generate the \LaTeX-file \texttt{T.tex} which is needed for the next step,
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   479
extraction of marked snippets.
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   480
You may also want to process \texttt{T.tex} to generate a pdf document.
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   481
This requires a definition of \texttt{\char`\\snippet}:
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   482
\begin{verbatim}
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   483
\newcommand{\repeatisanl}[1]
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   484
  {\ifnum#1=0\else\isanewline\repeatisanl{\numexpr#1-1}\fi}
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   485
\newcommand{\snip}[4]{\repeatisanl#2#4\repeatisanl#3}
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   486
\end{verbatim}
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   487
Parameter 2 and 3 of \texttt{\char`\\snippet} are numbers (the \texttt{1}
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   488
and \texttt{2} above) and determine how many newlines are inserted before and after the snippet.
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   489
Unfortunately \texttt{text\_raw} eats up all preceding and following newlines
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   490
and they have to be inserted again in this manner. Otherwise the document generated from \texttt{T.tex}
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   491
will look ugly around the snippets. It can take some iterations to get the number of required
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   492
newlines exactly right.
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   493
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   494
\subsection{Extract marked snippets}
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   495
\label{subsec:extract}
15917
cd4983c76548 Added short description of thm_style and term_style antiquotation
haftmann
parents: 15689
diff changeset
   496
49239
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   497
Extract the marked bits of text with a shell-level script, e.g.
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   498
\begin{quote}
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   499
\verb!sed -n '/\\snip{/,/endsnip/p' T.tex > !\emph{snippets}\verb!.tex!
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   500
\end{quote}
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   501
File \emph{snippets}\texttt{.tex} (the name is arbitrary) now contains a sequence of blocks like this
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   502
\begin{quote}
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   503
\verb!\snip{!\emph{snippetname}\verb!}{1}{2}{%!\\
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   504
\emph{theory text}\\
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   505
\verb!}%endsnip!
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   506
\end{quote}
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   507
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   508
\subsection{Including snippets}
17031
ffa73448025e added hint for position of aqu options in connection with styles
haftmann
parents: 16395
diff changeset
   509
49239
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   510
In the preamble of the document where the snippets are to be used you define \texttt{\char`\\snip}
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   511
and input \emph{snippets}\texttt{.tex}:
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   512
\begin{verbatim}
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   513
\newcommand{\snip}[4]
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   514
  {\expandafter\newcommand\csname #1\endcsname{#4}}
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   515
\input{snippets}
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   516
\end{verbatim}
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   517
This definition of \texttt{\char`\\snip} simply has the effect of defining for each snippet
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   518
\emph{snippetname} a \LaTeX\ command \texttt{\char`\\}\emph{snippetname}
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   519
that produces the corresponding snippet text. In the body of your document you can display that text
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   520
like this:
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   521
\begin{quote}
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   522
\verb!\begin{isabelle}!\\
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   523
\texttt{\char`\\}\emph{snippetname}\\
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   524
\verb!\end{isabelle}!
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   525
\end{quote}
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   526
The \texttt{isabelle} environment is the one defined in the standard file
fdac10715b6b added snippets
nipkow
parents: 48985
diff changeset
   527
\texttt{isabelle.sty} which most likely you are loading anyway.
49628
8262d35eff20 new antiquotation const_typ
nipkow
parents: 49239
diff changeset
   528
8262d35eff20 new antiquotation const_typ
nipkow
parents: 49239
diff changeset
   529
8262d35eff20 new antiquotation const_typ
nipkow
parents: 49239
diff changeset
   530
\section{Antiquotation}
8262d35eff20 new antiquotation const_typ
nipkow
parents: 49239
diff changeset
   531
8262d35eff20 new antiquotation const_typ
nipkow
parents: 49239
diff changeset
   532
You want to show a constant and its type? Instead of going
8262d35eff20 new antiquotation const_typ
nipkow
parents: 49239
diff changeset
   533
\verb!@!\verb!{const myconst}! \verb!@!\verb!{text "::"}! \verb!@!\verb!{typeof myconst}!,
8262d35eff20 new antiquotation const_typ
nipkow
parents: 49239
diff changeset
   534
you can just write \verb!@!\verb!{const_typ myconst}! using the new antiquotation
8262d35eff20 new antiquotation const_typ
nipkow
parents: 49239
diff changeset
   535
\texttt{const\_typ} defined in \texttt{LaTeXsugar}. For example,
8262d35eff20 new antiquotation const_typ
nipkow
parents: 49239
diff changeset
   536
\verb!@!\verb!{const_typ length}! produces @{const_typ length}.
8262d35eff20 new antiquotation const_typ
nipkow
parents: 49239
diff changeset
   537
15917
cd4983c76548 Added short description of thm_style and term_style antiquotation
haftmann
parents: 15689
diff changeset
   538
*}
cd4983c76548 Added short description of thm_style and term_style antiquotation
haftmann
parents: 15689
diff changeset
   539
15337
nipkow
parents:
diff changeset
   540
(*<*)
nipkow
parents:
diff changeset
   541
end
16175
nipkow
parents: 16167
diff changeset
   542
(*>*)