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