author | nipkow |
Thu, 29 Oct 2009 15:47:03 +0100 | |
changeset 33323 | 1932908057c7 |
parent 32898 | e871d897969c |
child 34877 | ded5b770ec1c |
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}% |
17125 | 4 |
% |
5 |
\isadelimtheory |
|
6 |
% |
|
7 |
\endisadelimtheory |
|
8 |
% |
|
9 |
\isatagtheory |
|
10 |
% |
|
11 |
\endisatagtheory |
|
12 |
{\isafoldtheory}% |
|
13 |
% |
|
14 |
\isadelimtheory |
|
15 |
% |
|
16 |
\endisadelimtheory |
|
15893
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
17 |
% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
18 |
\isamarkupsection{Introduction% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
19 |
} |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
20 |
\isamarkuptrue% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
21 |
% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
22 |
\begin{isamarkuptext}% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
23 |
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
|
24 |
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
|
25 |
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
|
26 |
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
|
27 |
and seeing Isabelle typeset it for them: |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
28 |
\begin{isabelle}% |
17214 | 29 |
{\isacharparenleft}{\isasymSum}x{\isasymin}A{\isachardot}\ {\isasymSum}y{\isasymin}B{\isachardot}\ f\ x\ y{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}{\isasymSum}{\isacharparenleft}x{\isacharcomma}\ y{\isacharparenright}{\isasymin}A\ {\isasymtimes}\ B{\isachardot}\ f\ x\ y{\isacharparenright}% |
15893
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
30 |
\end{isabelle} |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
31 |
No typos, no omissions, no sweat. |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
32 |
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
|
33 |
Theories}, \cite{LNCS2283} first. |
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 |
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
|
36 |
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
|
37 |
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
|
38 |
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
|
39 |
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
|
40 |
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
|
41 |
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
|
42 |
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
|
43 |
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
|
44 |
that must be punished by instant rejection. |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
45 |
|
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
46 |
|
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
47 |
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
|
48 |
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
|
49 |
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
|
50 |
\begin{itemize} |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
51 |
\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
|
52 |
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
|
53 |
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
|
54 |
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
|
55 |
|
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
56 |
\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
|
57 |
you so), you include them at the beginning of your \LaTeX\ document, |
16154 | 58 |
typically in \texttt{root.tex}. For a start, you should |
59 |
\verb!\usepackage{amssymb}! --- otherwise typesetting |
|
60 |
\isa{{\isachardoublequote}{\isasymnot}{\isacharparenleft}{\isasymexists}x{\isachardot}\ P\ x{\isacharparenright}{\isachardoublequote}} will fail because the AMS symbol |
|
61 |
\isa{{\isasymnexists}} is missing. |
|
15893
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
62 |
\end{itemize}% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
63 |
\end{isamarkuptext}% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
64 |
\isamarkuptrue% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
65 |
% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
66 |
\isamarkupsection{HOL syntax% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
67 |
} |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
68 |
\isamarkuptrue% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
69 |
% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
70 |
\isamarkupsubsection{Logic% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
71 |
} |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
72 |
\isamarkuptrue% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
73 |
% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
74 |
\begin{isamarkuptext}% |
16154 | 75 |
The formula \isa{{\isachardoublequote}{\isasymnot}{\isacharparenleft}{\isasymexists}x{\isachardot}\ P\ x{\isacharparenright}{\isachardoublequote}} is typeset as \isa{{\isasymnexists}x{\isachardot}\ P\ x}. |
76 |
||
15893
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
77 |
The predefined constructs \isa{if}, \isa{let} and |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
78 |
\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
|
79 |
other functions. This improves readability: |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
80 |
\begin{itemize} |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
81 |
\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
|
82 |
\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
|
83 |
\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
|
84 |
\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
|
85 |
\end{itemize}% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
86 |
\end{isamarkuptext}% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
87 |
\isamarkuptrue% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
88 |
% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
89 |
\isamarkupsubsection{Sets% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
90 |
} |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
91 |
\isamarkuptrue% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
92 |
% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
93 |
\begin{isamarkuptext}% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
94 |
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
|
95 |
standard, we provide a few further improvements: |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
96 |
\begin{itemize} |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
97 |
\item \isa{{\isacharbraceleft}x\ {\isacharbar}\ P{\isacharbraceright}} instead of \isa{{\isacharbraceleft}x{\isachardot}\ P{\isacharbraceright}}. |
27688 | 98 |
\item \isa{{\isasymemptyset}} instead of \isa{{\isacharbraceleft}{\isacharbraceright}}, where |
99 |
\isa{{\isasymemptyset}} is also input syntax. |
|
15893
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
100 |
\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
|
101 |
\end{itemize}% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
102 |
\end{isamarkuptext}% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
103 |
\isamarkuptrue% |
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 |
\isamarkupsubsection{Lists% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
106 |
} |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
107 |
\isamarkuptrue% |
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 |
\begin{isamarkuptext}% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
110 |
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
|
111 |
\begin{itemize} |
27688 | 112 |
\item \isa{x{\isasymcdot}xs} instead of \isa{x\ {\isacharhash}\ xs}, |
113 |
where \isa{x{\isasymcdot}xs} is also input syntax. |
|
15893
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
114 |
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
|
115 |
\verb!\isasymcdot! in \LaTeX: |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
116 |
\verb!\renewcommand{\isasymcdot}{\isamath{\,\cdot\,}}! |
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 |
\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
|
119 |
\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
|
120 |
the $n$th element of \isa{xs}. |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
121 |
|
22834 | 122 |
\item Human readers are good at converting automatically from lists to |
30502 | 123 |
sets. Hence \texttt{OptionalSugar} contains syntax for suppressing the |
22834 | 124 |
conversion function \isa{set}: for example, \isa{{\isachardoublequote}x\ {\isasymin}\ set\ xs{\isachardoublequote}} |
125 |
becomes \isa{x\ {\isasymin}\ xs}. |
|
126 |
||
15893
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
127 |
\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
|
128 |
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
|
129 |
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
|
130 |
\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
|
131 |
line breaking behaviour: |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
132 |
\begin{isabelle}% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
133 |
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
|
134 |
\end{isabelle} |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
135 |
|
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
136 |
\end{itemize}% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
137 |
\end{isamarkuptext}% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
138 |
\isamarkuptrue% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
139 |
% |
30502 | 140 |
\isamarkupsubsection{Numbers% |
141 |
} |
|
142 |
\isamarkuptrue% |
|
143 |
% |
|
144 |
\begin{isamarkuptext}% |
|
145 |
Coercions between numeric types are alien to mathematicians who |
|
146 |
consider, for example, \isa{nat} as a subset of \isa{int}. |
|
147 |
\texttt{OptionalSugar} contains syntax for suppressing numeric coercions such |
|
148 |
as \isa{int} \isa{{\isacharcolon}{\isacharcolon}} \isa{nat\ {\isasymRightarrow}\ int}. For example, |
|
149 |
\isa{{\isachardoublequote}int\ {\isadigit{5}}{\isachardoublequote}} is printed as \isa{{\isadigit{5}}}. Embeddings of types |
|
150 |
\isa{nat}, \isa{int}, \isa{real} are covered; non-injective coercions such |
|
151 |
as \isa{nat} \isa{{\isacharcolon}{\isacharcolon}} \isa{int\ {\isasymRightarrow}\ nat} are not and should not be |
|
152 |
hidden.% |
|
153 |
\end{isamarkuptext}% |
|
154 |
\isamarkuptrue% |
|
155 |
% |
|
15893
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
156 |
\isamarkupsection{Printing theorems% |
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 |
\isamarkupsubsection{Question marks% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
161 |
} |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
162 |
\isamarkuptrue% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
163 |
% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
164 |
\begin{isamarkuptext}% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
165 |
If you print anything, especially theorems, containing |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
166 |
schematic variables they are prefixed with a question mark: |
29297 | 167 |
\verb!@!\verb!{thm conjI}! results in \isa{{\isasymlbrakk}P{\isacharsemicolon}\ Q{\isasymrbrakk}\ {\isasymLongrightarrow}\ P\ {\isasymand}\ Q}. Most of the time |
15893
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
168 |
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
|
169 |
\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
|
170 |
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
|
171 |
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
|
172 |
|
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
173 |
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
|
174 |
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
|
175 |
\begin{verbatim} |
33323 | 176 |
show_question_marks := false; |
15893
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
177 |
\end{verbatim} |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
178 |
at the beginning of your file \texttt{ROOT.ML}. |
33323 | 179 |
The rest of this document is produced with this flag set to \texttt{false}. |
16075 | 180 |
|
33323 | 181 |
Hint: Setting \verb!show_question_marks! to \texttt{false} only |
182 |
suppresses question marks; variables that end in digits, |
|
183 |
e.g. \isa{x{\isadigit{1}}}, are still printed with a trailing \isa{{\isachardot}{\isadigit{0}}}, |
|
184 |
e.g. \isa{x{\isadigit{1}}{\isachardot}{\isadigit{0}}}, their internal index. This can be avoided by |
|
185 |
turning the last digit into a subscript: write \verb!x\<^isub>1! and |
|
186 |
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
|
187 |
\end{isamarkuptext}% |
17175 | 188 |
\isamarkuptrue% |
17125 | 189 |
% |
190 |
\isadelimML |
|
191 |
% |
|
192 |
\endisadelimML |
|
193 |
% |
|
194 |
\isatagML |
|
195 |
% |
|
196 |
\endisatagML |
|
197 |
{\isafoldML}% |
|
198 |
% |
|
199 |
\isadelimML |
|
200 |
% |
|
201 |
\endisadelimML |
|
15893
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
202 |
% |
24496 | 203 |
\isamarkupsubsection{Qualified names% |
204 |
} |
|
205 |
\isamarkuptrue% |
|
206 |
% |
|
207 |
\begin{isamarkuptext}% |
|
208 |
If there are multiple declarations of the same name, Isabelle prints |
|
209 |
the qualified name, for example \isa{T{\isachardot}length}, where \isa{T} is the |
|
210 |
theory it is defined in, to distinguish it from the predefined \isa{{\isachardoublequote}List{\isachardot}length{\isachardoublequote}}. In case there is no danger of confusion, you can insist on |
|
211 |
short names (no qualifiers) by setting \verb!short_names!, typically |
|
212 |
in \texttt{ROOT.ML}: |
|
213 |
\begin{verbatim} |
|
214 |
set short_names; |
|
215 |
\end{verbatim}% |
|
216 |
\end{isamarkuptext}% |
|
217 |
\isamarkuptrue% |
|
218 |
% |
|
17134 | 219 |
\isamarkupsubsection{Variable names\label{sec:varnames}% |
16396 | 220 |
} |
221 |
\isamarkuptrue% |
|
222 |
% |
|
223 |
\begin{isamarkuptext}% |
|
224 |
It sometimes happens that you want to change the name of a |
|
225 |
variable in a theorem before printing it. This can easily be achieved |
|
226 |
with the help of Isabelle's instantiation attribute \texttt{where}: |
|
227 |
\isa{{\isasymlbrakk}{\isasymphi}{\isacharsemicolon}\ {\isasympsi}{\isasymrbrakk}\ {\isasymLongrightarrow}\ {\isasymphi}\ {\isasymand}\ {\isasympsi}} is the result of |
|
228 |
\begin{quote} |
|
229 |
\verb!@!\verb!{thm conjI[where P = \<phi> and Q = \<psi>]}! |
|
230 |
\end{quote} |
|
231 |
To support the ``\_''-notation for irrelevant variables |
|
232 |
the constant \texttt{DUMMY} has been introduced: |
|
233 |
\isa{fst\ {\isacharparenleft}a{\isacharcomma}\ \_{\isacharparenright}\ {\isacharequal}\ a} is produced by |
|
234 |
\begin{quote} |
|
235 |
\verb!@!\verb!{thm fst_conv[where b = DUMMY]}! |
|
236 |
\end{quote}% |
|
237 |
\end{isamarkuptext}% |
|
238 |
\isamarkuptrue% |
|
239 |
% |
|
15893
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
240 |
\isamarkupsubsection{Inference rules% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
241 |
} |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
242 |
\isamarkuptrue% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
243 |
% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
244 |
\begin{isamarkuptext}% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
245 |
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
|
246 |
R\'emy's \texttt{mathpartir} package~\cite{mathpartir} |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
247 |
for typesetting inference rules in your \LaTeX\ file. |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
248 |
|
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
249 |
Writing \verb!@!\verb!{thm[mode=Rule] conjI}! produces |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
250 |
\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
|
251 |
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
|
252 |
\begin{center} |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
253 |
\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
|
254 |
\end{center} |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
255 |
is produced by |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
256 |
\begin{quote} |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
257 |
\verb!\begin{center}!\\ |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
258 |
\verb!@!\verb!{thm[mode=Rule] conjI} {\sc conjI}!\\ |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
259 |
\verb!\end{center}! |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
260 |
\end{quote} |
24497 | 261 |
It is not recommended to use the standard \texttt{display} option |
15893
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
262 |
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
|
263 |
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
|
264 |
clash. |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
265 |
|
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
266 |
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
|
267 |
\begin{quote} |
24497 | 268 |
\verb!\begin{center}!\\ |
15893
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
269 |
\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
|
270 |
\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
|
271 |
\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
|
272 |
\verb!\end{center}! |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
273 |
\end{quote} |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
274 |
yields |
24497 | 275 |
\begin{center}\small |
15893
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
276 |
\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
|
277 |
\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
|
278 |
\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
|
279 |
\end{center} |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
280 |
|
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
281 |
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
|
282 |
premises for one line: |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
283 |
\begin{center} |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
284 |
\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
|
285 |
\end{center} |
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 |
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
|
288 |
the line. 2. Premises that are \isa{{\isasymLongrightarrow}}-implications are again |
22387 | 289 |
displayed with a horizontal line, which looks at least unusual. |
290 |
||
291 |
||
292 |
In case you print theorems without premises no rule will be printed by the |
|
293 |
\texttt{Rule} print mode. However, you can use \texttt{Axiom} instead: |
|
294 |
\begin{quote} |
|
24497 | 295 |
\verb!\begin{center}!\\ |
22387 | 296 |
\verb!@!\verb!{thm[mode=Axiom] refl} {\sc refl}! \\ |
297 |
\verb!\end{center}! |
|
298 |
\end{quote} |
|
299 |
yields |
|
24497 | 300 |
\begin{center} |
22387 | 301 |
\isa{\mbox{}\inferrule{\mbox{}}{\mbox{t\ {\isacharequal}\ t}}} {\sc refl} |
302 |
\end{center}% |
|
15893
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
303 |
\end{isamarkuptext}% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
304 |
\isamarkuptrue% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
305 |
% |
24497 | 306 |
\isamarkupsubsection{Displays and font sizes% |
307 |
} |
|
308 |
\isamarkuptrue% |
|
309 |
% |
|
310 |
\begin{isamarkuptext}% |
|
311 |
When displaying theorems with the \texttt{display} option, e.g. |
|
312 |
\verb!@!\verb!{thm[display] refl}! \begin{isabelle}% |
|
313 |
t\ {\isacharequal}\ t% |
|
314 |
\end{isabelle} the theorem is |
|
315 |
set in small font. It uses the \LaTeX-macro \verb!\isastyle!, |
|
316 |
which is also the style that regular theory text is set in, e.g.% |
|
317 |
\end{isamarkuptext}% |
|
318 |
\isamarkuptrue% |
|
319 |
\isacommand{lemma}\isamarkupfalse% |
|
320 |
\ {\isachardoublequoteopen}t\ {\isacharequal}\ t{\isachardoublequoteclose}% |
|
321 |
\isadelimproof |
|
322 |
% |
|
323 |
\endisadelimproof |
|
324 |
% |
|
325 |
\isatagproof |
|
326 |
% |
|
327 |
\endisatagproof |
|
328 |
{\isafoldproof}% |
|
329 |
% |
|
330 |
\isadelimproof |
|
331 |
% |
|
332 |
\endisadelimproof |
|
333 |
% |
|
334 |
\begin{isamarkuptext}% |
|
335 |
\noindent Otherwise \verb!\isastyleminor! is used, |
|
336 |
which does not modify the font size (assuming you stick to the default |
|
337 |
\verb!\isabellestyle{it}! in \texttt{root.tex}). If you prefer |
|
338 |
normal font size throughout your text, include |
|
339 |
\begin{quote} |
|
340 |
\verb!\renewcommand{\isastyle}{\isastyleminor}! |
|
341 |
\end{quote} |
|
342 |
in \texttt{root.tex}. On the other hand, if you like the small font, |
|
343 |
just put \verb!\isastyle! in front of the text in question, |
|
344 |
e.g.\ at the start of one of the center-environments above. |
|
345 |
||
346 |
The advantage of the display option is that you can display a whole |
|
347 |
list of theorems in one go. For example, |
|
348 |
\verb!@!\verb!{thm[display] foldl.simps}! |
|
349 |
generates \begin{isabelle}% |
|
350 |
foldl\ f\ a\ {\isacharbrackleft}{\isacharbrackright}\ {\isacharequal}\ a\isasep\isanewline% |
|
351 |
foldl\ f\ a\ {\isacharparenleft}x{\isasymcdot}xs{\isacharparenright}\ {\isacharequal}\ foldl\ f\ {\isacharparenleft}f\ a\ x{\isacharparenright}\ xs% |
|
352 |
\end{isabelle}% |
|
353 |
\end{isamarkuptext}% |
|
354 |
\isamarkuptrue% |
|
355 |
% |
|
15893
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
356 |
\isamarkupsubsection{If-then% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
357 |
} |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
358 |
\isamarkuptrue% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
359 |
% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
360 |
\begin{isamarkuptext}% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
361 |
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
|
362 |
the body of |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
363 |
\newtheorem{theorem}{Theorem} |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
364 |
\begin{theorem} |
25731 | 365 |
\isa{{\normalsize{}If\,}\ \mbox{i\ {\isasymle}\ j}\ {\normalsize \,and\,}\ \mbox{j\ {\isasymle}\ k}\ {\normalsize \,then\,}\ i\ {\isasymle}\ k{\isachardot}} |
15893
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
366 |
\end{theorem} |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
367 |
by typing |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
368 |
\begin{quote} |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
369 |
\verb!@!\verb!{thm[mode=IfThen] le_trans}! |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
370 |
\end{quote} |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
371 |
|
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
372 |
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
|
373 |
At times this is too drastic: |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
374 |
\begin{theorem} |
25731 | 375 |
\isa{{\normalsize{}If\,}\ \mbox{longpremise}\ {\normalsize \,and\,}\ \mbox{longerpremise}\ {\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}}\ {\normalsize \,and\,}\ \mbox{longestpremise}\ {\normalsize \,then\,}\ conclusion{\isachardot}} |
15893
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
376 |
\end{theorem} |
16154 | 377 |
In which case you should use \texttt{IfThenNoBox} instead of |
378 |
\texttt{IfThen}: |
|
15893
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
379 |
\begin{theorem} |
25731 | 380 |
\isa{{\normalsize{}If\,}\ longpremise\ {\normalsize \,and\,}\ longerpremise\ {\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}\ {\normalsize \,and\,}\ longestpremise\ {\normalsize \,then\,}\ conclusion{\isachardot}} |
15893
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
381 |
\end{theorem}% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
382 |
\end{isamarkuptext}% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
383 |
\isamarkuptrue% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
384 |
% |
16166 | 385 |
\isamarkupsubsection{Doing it yourself\label{sec:yourself}% |
16154 | 386 |
} |
387 |
\isamarkuptrue% |
|
388 |
% |
|
389 |
\begin{isamarkuptext}% |
|
390 |
If for some reason you want or need to present theorems your |
|
391 |
own way, you can extract the premises and the conclusion explicitly |
|
392 |
and combine them as you like: |
|
393 |
\begin{itemize} |
|
32893 | 394 |
\item \verb!@!\verb!{thm (prem 1)! $thm$\verb!}! |
395 |
prints premise 1 of $thm$. |
|
396 |
\item \verb!@!\verb!{thm (concl)! $thm$\verb!}! |
|
16154 | 397 |
prints the conclusion of $thm$. |
398 |
\end{itemize} |
|
399 |
For example, ``from \isa{Q} and |
|
400 |
\isa{P} we conclude \isa{P\ {\isasymand}\ Q}'' |
|
401 |
is produced by |
|
402 |
\begin{quote} |
|
32893 | 403 |
\verb!from !\verb!@!\verb!{thm (prem 2) conjI}! \verb!and !\verb!@!\verb!{thm (prem 1) conjI}!\\ |
404 |
\verb!we conclude !\verb!@!\verb!{thm (concl) conjI}! |
|
16154 | 405 |
\end{quote} |
406 |
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:
32893
diff
changeset
|
407 |
Styles like \verb!(prem 1)! are a general mechanism explained |
16154 | 408 |
in \S\ref{sec:styles}.% |
409 |
\end{isamarkuptext}% |
|
410 |
\isamarkuptrue% |
|
411 |
% |
|
15893
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
412 |
\isamarkupsubsection{Patterns% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
413 |
} |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
414 |
\isamarkuptrue% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
415 |
% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
416 |
\begin{isamarkuptext}% |
17134 | 417 |
In \S\ref{sec:varnames} we shows how to create patterns containing |
418 |
``\isa{\_}''. |
|
15893
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
419 |
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
|
420 |
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
|
421 |
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
|
422 |
following: |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
423 |
|
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
424 |
\begin{center} |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
425 |
\begin{tabular}{l@ {~~produced by~~}l} |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
426 |
\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
|
427 |
\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
|
428 |
\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
|
429 |
\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
|
430 |
\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
|
431 |
\end{tabular} |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
432 |
\end{center}% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
433 |
\end{isamarkuptext}% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
434 |
\isamarkuptrue% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
435 |
% |
16155 | 436 |
\isamarkupsection{Proofs% |
15893
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
437 |
} |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
438 |
\isamarkuptrue% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
439 |
% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
440 |
\begin{isamarkuptext}% |
24497 | 441 |
Full proofs, even if written in beautiful Isar style, are |
442 |
likely to be too long and detailed to be included in conference |
|
443 |
papers, but some key lemmas might be of interest. |
|
444 |
It is usually easiest to put them in figures like the one in Fig.\ |
|
445 |
\ref{fig:proof}. This was achieved with the \isakeyword{text\_raw} command:% |
|
15893
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
446 |
\end{isamarkuptext}% |
17175 | 447 |
\isamarkuptrue% |
15893
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
448 |
% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
449 |
\begin{figure} |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
450 |
\begin{center}\begin{minipage}{0.6\textwidth} |
24497 | 451 |
\isastyleminor\isamarkuptrue |
17175 | 452 |
\isacommand{lemma}\isamarkupfalse% |
453 |
\ True\isanewline |
|
17125 | 454 |
% |
455 |
\isadelimproof |
|
456 |
% |
|
457 |
\endisadelimproof |
|
458 |
% |
|
459 |
\isatagproof |
|
17175 | 460 |
\isacommand{proof}\isamarkupfalse% |
461 |
\ {\isacharminus}\isanewline |
|
15893
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
462 |
\ \ % |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
463 |
\isamarkupcmt{pretty trivial% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
464 |
} |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
465 |
\isanewline |
17175 | 466 |
\ \ \isacommand{show}\isamarkupfalse% |
467 |
\ True\ \isacommand{by}\isamarkupfalse% |
|
468 |
\ force\isanewline |
|
469 |
\isacommand{qed}\isamarkupfalse% |
|
470 |
% |
|
17125 | 471 |
\endisatagproof |
472 |
{\isafoldproof}% |
|
473 |
% |
|
474 |
\isadelimproof |
|
475 |
% |
|
476 |
\endisadelimproof |
|
15893
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
477 |
% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
478 |
\end{minipage}\end{center} |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
479 |
\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
|
480 |
\end{figure} |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
481 |
% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
482 |
\begin{isamarkuptext}% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
483 |
\begin{quote} |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
484 |
\small |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
485 |
\verb!text_raw {!\verb!*!\\ |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
486 |
\verb! \begin{figure}!\\ |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
487 |
\verb! \begin{center}\begin{minipage}{0.6\textwidth}!\\ |
24497 | 488 |
\verb! \isastyleminor\isamarkuptrue!\\ |
15893
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
489 |
\verb!*!\verb!}!\\ |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
490 |
\verb!lemma True!\\ |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
491 |
\verb!proof -!\\ |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
492 |
\verb! -- "pretty trivial"!\\ |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
493 |
\verb! show True by force!\\ |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
494 |
\verb!qed!\\ |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
495 |
\verb!text_raw {!\verb!*!\\ |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
496 |
\verb! \end{minipage}\end{center}!\\ |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
497 |
\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
|
498 |
\verb! \end{figure}!\\ |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
499 |
\verb!*!\verb!}! |
24497 | 500 |
\end{quote} |
501 |
||
502 |
Other theory text, e.g.\ definitions, can be put in figures, too.% |
|
15893
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
503 |
\end{isamarkuptext}% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
504 |
\isamarkuptrue% |
15953 | 505 |
% |
16155 | 506 |
\isamarkupsection{Styles\label{sec:styles}% |
15953 | 507 |
} |
508 |
\isamarkuptrue% |
|
509 |
% |
|
510 |
\begin{isamarkuptext}% |
|
511 |
The \verb!thm! antiquotation works nicely for single theorems, but |
|
512 |
sets of equations as used in definitions are more difficult to |
|
16040 | 513 |
typeset nicely: people tend to prefer aligned \isa{{\isacharequal}} signs. |
15953 | 514 |
|
515 |
To deal with such cases where it is desirable to dive into the structure |
|
16040 | 516 |
of terms and theorems, Isabelle offers antiquotations featuring |
15953 | 517 |
``styles'': |
518 |
||
519 |
\begin{quote} |
|
32893 | 520 |
\verb!@!\verb!{thm (style) thm}!\\ |
521 |
\verb!@!\verb!{prop (style) thm}!\\ |
|
32898
e871d897969c
term styles also cover antiquotations term_type and typeof
haftmann
parents:
32893
diff
changeset
|
522 |
\verb!@!\verb!{term (style) term}!\\ |
e871d897969c
term styles also cover antiquotations term_type and typeof
haftmann
parents:
32893
diff
changeset
|
523 |
\verb!@!\verb!{term_type (style) term}!\\ |
e871d897969c
term styles also cover antiquotations term_type and typeof
haftmann
parents:
32893
diff
changeset
|
524 |
\verb!@!\verb!{typeof (style) term}!\\ |
15953 | 525 |
\end{quote} |
526 |
||
32898
e871d897969c
term styles also cover antiquotations term_type and typeof
haftmann
parents:
32893
diff
changeset
|
527 |
A ``style'' is a transformation of a term. There are predefined |
32893 | 528 |
styles, namely \verb!lhs! and \verb!rhs!, \verb!prem! with one argument, and \verb!concl!. |
16166 | 529 |
For example, |
16076 | 530 |
the output |
15953 | 531 |
\begin{center} |
532 |
\begin{tabular}{l@ {~~\isa{{\isacharequal}}~~}l} |
|
533 |
\isa{foldl\ f\ a\ {\isacharbrackleft}{\isacharbrackright}} & \isa{a}\\ |
|
534 |
\isa{foldl\ f\ a\ {\isacharparenleft}x{\isasymcdot}xs{\isacharparenright}} & \isa{foldl\ f\ {\isacharparenleft}f\ a\ x{\isacharparenright}\ xs} |
|
535 |
\end{tabular} |
|
536 |
\end{center} |
|
537 |
is produced by the following code: |
|
538 |
\begin{quote} |
|
539 |
\verb!\begin{center}!\\ |
|
540 |
\verb!\begin{tabular}{l@ {~~!\verb!@!\verb!{text "="}~~}l}!\\ |
|
33323 | 541 |
\verb!@!\verb!{thm (lhs) foldl_Nil} & @!\verb!{thm (rhs) foldl_Nil}\\!\\ |
32893 | 542 |
\verb!@!\verb!{thm (lhs) foldl_Cons} & @!\verb!{thm (rhs) foldl_Cons}!\\ |
15953 | 543 |
\verb!\end{tabular}!\\ |
544 |
\verb!\end{center}! |
|
545 |
\end{quote} |
|
546 |
Note the space between \verb!@! and \verb!{! in the tabular argument. |
|
547 |
It prevents Isabelle from interpreting \verb!@ {~~...~~}! |
|
16076 | 548 |
as an antiquotation. The styles \verb!lhs! and \verb!rhs! |
27094 | 549 |
extract the left hand side (or right hand side respectively) from the |
16076 | 550 |
conclusion of propositions consisting of a binary operator |
16040 | 551 |
(e.~g.~\isa{{\isacharequal}}, \isa{{\isasymequiv}}, \isa{{\isacharless}}). |
15953 | 552 |
|
16166 | 553 |
Likewise, \verb!concl! may be used as a style to show just the |
16076 | 554 |
conclusion of a proposition. For example, take \verb!hd_Cons_tl!: |
16040 | 555 |
\begin{center} |
33323 | 556 |
\isa{xs\ {\isasymnoteq}\ {\isacharbrackleft}{\isacharbrackright}\ {\isasymLongrightarrow}\ hd\ xs{\isasymcdot}tl\ xs\ {\isacharequal}\ xs} |
16040 | 557 |
\end{center} |
558 |
To print just the conclusion, |
|
15953 | 559 |
\begin{center} |
33323 | 560 |
\isa{hd\ xs{\isasymcdot}tl\ xs\ {\isacharequal}\ xs} |
15953 | 561 |
\end{center} |
16040 | 562 |
type |
15953 | 563 |
\begin{quote} |
564 |
\verb!\begin{center}!\\ |
|
33323 | 565 |
\verb!@!\verb!{thm (concl) hd_Cons_tl}!\\ |
15953 | 566 |
\verb!\end{center}! |
567 |
\end{quote} |
|
17134 | 568 |
Beware that any options must be placed \emph{before} |
32898
e871d897969c
term styles also cover antiquotations term_type and typeof
haftmann
parents:
32893
diff
changeset
|
569 |
the style, as in this example. |
17125 | 570 |
|
16166 | 571 |
Further use cases can be found in \S\ref{sec:yourself}. |
15953 | 572 |
If you are not afraid of ML, you may also define your own styles. |
32893 | 573 |
Have a look at module \verb|Term_Style|.% |
15953 | 574 |
\end{isamarkuptext}% |
17175 | 575 |
\isamarkuptrue% |
17125 | 576 |
% |
577 |
\isadelimtheory |
|
578 |
% |
|
579 |
\endisadelimtheory |
|
580 |
% |
|
581 |
\isatagtheory |
|
582 |
% |
|
583 |
\endisatagtheory |
|
584 |
{\isafoldtheory}% |
|
585 |
% |
|
586 |
\isadelimtheory |
|
587 |
% |
|
588 |
\endisadelimtheory |
|
15893
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
589 |
\end{isabellebody}% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
590 |
%%% Local Variables: |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
591 |
%%% mode: latex |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
592 |
%%% TeX-master: "root" |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
593 |
%%% End: |