author | wenzelm |
Mon, 08 Nov 2010 00:00:47 +0100 | |
changeset 40406 | 313a24b66a8d |
parent 38980 | af73cf0dc31f |
child 42289 | dafae095d733 |
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}% |
40406 | 29 |
{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C53756D3E}{\isasymSum}}x{\isaliteral{5C3C696E3E}{\isasymin}}A{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C53756D3E}{\isasymSum}}y{\isaliteral{5C3C696E3E}{\isasymin}}B{\isaliteral{2E}{\isachardot}}\ f\ x\ y{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C53756D3E}{\isasymSum}}{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}\ y{\isaliteral{29}{\isacharparenright}}{\isaliteral{5C3C696E3E}{\isasymin}}A\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ B{\isaliteral{2E}{\isachardot}}\ f\ x\ y{\isaliteral{29}{\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 |
40406 | 42 |
like Isabelle's infamous \isa{{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}\ {\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}} no matter how many times you |
43 |
explain it in your paper. Even worse, he thinks that using \isa{{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}\ {\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}} for anything other than denotational semantics is a cardinal sin |
|
15893
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 |
|
40406 | 60 |
\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}x{\isaliteral{2E}{\isachardot}}\ P\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} will fail because the AMS symbol |
61 |
\isa{{\isaliteral{5C3C6E6578697374733E}{\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}% |
40406 | 75 |
The formula \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}x{\isaliteral{2E}{\isachardot}}\ P\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} is typeset as \isa{{\isaliteral{5C3C6E6578697374733E}{\isasymnexists}}x{\isaliteral{2E}{\isachardot}}\ P\ x}. |
16154 | 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} |
40406 | 81 |
\item \isa{\textsf{if}\ b\ \textsf{then}\ e\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ \textsf{else}\ e\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}} instead of \isa{if\ b\ then\ e\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ else\ e\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}}. |
82 |
\item \isa{\textsf{let}\ x\ {\isaliteral{3D}{\isacharequal}}\ e\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ \textsf{in}\ e\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}} instead of \isa{let\ x\ {\isaliteral{3D}{\isacharequal}}\ e\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ in\ e\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}}. |
|
83 |
\item \isa{\textsf{case}\ x\ \textsf{of}\ True\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ e\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{7C}{\isacharbar}}\ False\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ e\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}} instead of\\ |
|
84 |
\isa{case\ x\ of\ True\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ e\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{7C}{\isacharbar}}\ False\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ e\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}}. |
|
15893
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} |
40406 | 97 |
\item \isa{{\isaliteral{7B}{\isacharbraceleft}}x\ {\isaliteral{7C}{\isacharbar}}\ P{\isaliteral{7D}{\isacharbraceright}}} instead of \isa{{\isaliteral{7B}{\isacharbraceleft}}x{\isaliteral{2E}{\isachardot}}\ P{\isaliteral{7D}{\isacharbraceright}}}. |
98 |
\item \isa{{\isaliteral{5C3C656D7074797365743E}{\isasymemptyset}}} instead of \isa{{\isaliteral{7B}{\isacharbraceleft}}{\isaliteral{7D}{\isacharbraceright}}}, where |
|
99 |
\isa{{\isaliteral{5C3C656D7074797365743E}{\isasymemptyset}}} is also input syntax. |
|
100 |
\item \isa{{\isaliteral{7B}{\isacharbraceleft}}a{\isaliteral{2C}{\isacharcomma}}\ b{\isaliteral{2C}{\isacharcomma}}\ c{\isaliteral{7D}{\isacharbraceright}}\ {\isaliteral{5C3C756E696F6E3E}{\isasymunion}}\ M} instead of \isa{insert\ a\ {\isaliteral{28}{\isacharparenleft}}insert\ b\ {\isaliteral{28}{\isacharparenleft}}insert\ c\ M{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}}. |
|
15893
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} |
40406 | 112 |
\item \isa{x{\isaliteral{5C3C63646F743E}{\isasymcdot}}xs} instead of \isa{x\ {\isaliteral{23}{\isacharhash}}\ xs}, |
113 |
where \isa{x{\isaliteral{5C3C63646F743E}{\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 |
|
40406 | 118 |
\item \isa{{\isaliteral{7C}{\isacharbar}}xs{\isaliteral{7C}{\isacharbar}}} instead of \isa{length\ xs}. |
15893
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 |
40406 | 124 |
conversion function \isa{set}: for example, \isa{{\isaliteral{22}{\isachardoublequote}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ set\ xs{\isaliteral{22}{\isachardoublequote}}} |
125 |
becomes \isa{x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ xs}. |
|
22834 | 126 |
|
40406 | 127 |
\item The \isa{{\isaliteral{40}{\isacharat}}} operation associates implicitly to the right, |
15893
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 |
40406 | 130 |
\isa{{\isaliteral{40}{\isacharat}}}-terms to the left before printing, which leads to better |
15893
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}% |
40406 | 133 |
term\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{0}}\ \isacharat\ term\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ \isacharat\ term\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}\ \isacharat\ term\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{3}}\ \isacharat\ term\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{4}}\ \isacharat\ term\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{5}}\ \isacharat\ term\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{6}}\ \isacharat\ term\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{7}}\ \isacharat\ term\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{8}}\ \isacharat\ term\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{9}}\ \isacharat\ term\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{0}}% |
15893
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 |
|
40406 | 148 |
as \isa{int} \isa{{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}} \isa{nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ int}. For example, |
149 |
\isa{{\isaliteral{22}{\isachardoublequote}}int\ {\isadigit{5}}{\isaliteral{22}{\isachardoublequote}}} is printed as \isa{{\isadigit{5}}}. Embeddings of types |
|
30502 | 150 |
\isa{nat}, \isa{int}, \isa{real} are covered; non-injective coercions such |
40406 | 151 |
as \isa{nat} \isa{{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}} \isa{int\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat} are not and should not be |
30502 | 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: |
40406 | 167 |
\verb!@!\verb!{thm conjI}! results in \isa{{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}{\isaliteral{3F}{\isacharquery}}P{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{3F}{\isacharquery}}Q{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{3F}{\isacharquery}}P\ {\isaliteral{5C3C616E643E}{\isasymand}}\ {\isaliteral{3F}{\isacharquery}}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]}! |
40406 | 171 |
results in \isa{{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}P{\isaliteral{3B}{\isacharsemicolon}}\ Q{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ {\isaliteral{5C3C616E643E}{\isasymand}}\ Q}. |
15893
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 |
34877
ded5b770ec1c
formal antiquotations for ML snippets; no "open" unsynchronized references
haftmann
parents:
33323
diff
changeset
|
175 |
\begin{quote} |
38980
af73cf0dc31f
turned show_question_marks into proper configuration option;
wenzelm
parents:
38798
diff
changeset
|
176 |
\verb|show_question_marks_default := false|\verb!;! |
34877
ded5b770ec1c
formal antiquotations for ML snippets; no "open" unsynchronized references
haftmann
parents:
33323
diff
changeset
|
177 |
\end{quote} |
15893
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 |
|
38980
af73cf0dc31f
turned show_question_marks into proper configuration option;
wenzelm
parents:
38798
diff
changeset
|
181 |
Hint: Setting \verb!show_question_marks_default! to \texttt{false} only |
33323 | 182 |
suppresses question marks; variables that end in digits, |
40406 | 183 |
e.g. \isa{x{\isadigit{1}}}, are still printed with a trailing \isa{{\isaliteral{2E}{\isachardot}}{\isadigit{0}}}, |
184 |
e.g. \isa{x{\isadigit{1}}{\isaliteral{2E}{\isachardot}}{\isadigit{0}}}, their internal index. This can be avoided by |
|
33323 | 185 |
turning the last digit into a subscript: write \verb!x\<^isub>1! and |
40406 | 186 |
obtain the much nicer \isa{x\isaliteral{5C3C5E697375623E}{}\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 |
% |
24496 | 190 |
\isamarkupsubsection{Qualified names% |
191 |
} |
|
192 |
\isamarkuptrue% |
|
193 |
% |
|
194 |
\begin{isamarkuptext}% |
|
195 |
If there are multiple declarations of the same name, Isabelle prints |
|
40406 | 196 |
the qualified name, for example \isa{T{\isaliteral{2E}{\isachardot}}length}, where \isa{T} is the |
197 |
theory it is defined in, to distinguish it from the predefined \isa{{\isaliteral{22}{\isachardoublequote}}List{\isaliteral{2E}{\isachardot}}length{\isaliteral{22}{\isachardoublequote}}}. In case there is no danger of confusion, you can insist on |
|
24496 | 198 |
short names (no qualifiers) by setting \verb!short_names!, typically |
199 |
in \texttt{ROOT.ML}: |
|
34877
ded5b770ec1c
formal antiquotations for ML snippets; no "open" unsynchronized references
haftmann
parents:
33323
diff
changeset
|
200 |
\begin{quote} |
38798
89f273ab1d42
expanded some aliases from structure Unsynchronized;
wenzelm
parents:
36138
diff
changeset
|
201 |
\verb|short_names := true|\verb!;! |
34877
ded5b770ec1c
formal antiquotations for ML snippets; no "open" unsynchronized references
haftmann
parents:
33323
diff
changeset
|
202 |
\end{quote}% |
24496 | 203 |
\end{isamarkuptext}% |
204 |
\isamarkuptrue% |
|
205 |
% |
|
17134 | 206 |
\isamarkupsubsection{Variable names\label{sec:varnames}% |
16396 | 207 |
} |
208 |
\isamarkuptrue% |
|
209 |
% |
|
210 |
\begin{isamarkuptext}% |
|
211 |
It sometimes happens that you want to change the name of a |
|
212 |
variable in a theorem before printing it. This can easily be achieved |
|
213 |
with the help of Isabelle's instantiation attribute \texttt{where}: |
|
40406 | 214 |
\isa{{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}{\isaliteral{5C3C7068693E}{\isasymphi}}{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{5C3C7073693E}{\isasympsi}}{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ {\isaliteral{5C3C7073693E}{\isasympsi}}} is the result of |
16396 | 215 |
\begin{quote} |
216 |
\verb!@!\verb!{thm conjI[where P = \<phi> and Q = \<psi>]}! |
|
217 |
\end{quote} |
|
218 |
To support the ``\_''-notation for irrelevant variables |
|
219 |
the constant \texttt{DUMMY} has been introduced: |
|
40406 | 220 |
\isa{fst\ {\isaliteral{28}{\isacharparenleft}}a{\isaliteral{2C}{\isacharcomma}}\ \_{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ a} is produced by |
16396 | 221 |
\begin{quote} |
222 |
\verb!@!\verb!{thm fst_conv[where b = DUMMY]}! |
|
36138
1faa0fc34174
advertise [rename_abs] attribute in LaTeXsugar -- wish I had known about this earier.
krauss
parents:
34878
diff
changeset
|
223 |
\end{quote} |
1faa0fc34174
advertise [rename_abs] attribute in LaTeXsugar -- wish I had known about this earier.
krauss
parents:
34878
diff
changeset
|
224 |
Variables that are bound by quantifiers or lambdas cannot be renamed |
1faa0fc34174
advertise [rename_abs] attribute in LaTeXsugar -- wish I had known about this earier.
krauss
parents:
34878
diff
changeset
|
225 |
like this. Instead, the attribute \texttt{rename\_abs} does the |
1faa0fc34174
advertise [rename_abs] attribute in LaTeXsugar -- wish I had known about this earier.
krauss
parents:
34878
diff
changeset
|
226 |
job. It expects a list of names or underscores, similar to the |
1faa0fc34174
advertise [rename_abs] attribute in LaTeXsugar -- wish I had known about this earier.
krauss
parents:
34878
diff
changeset
|
227 |
\texttt{of} attribute: |
1faa0fc34174
advertise [rename_abs] attribute in LaTeXsugar -- wish I had known about this earier.
krauss
parents:
34878
diff
changeset
|
228 |
\begin{quote} |
1faa0fc34174
advertise [rename_abs] attribute in LaTeXsugar -- wish I had known about this earier.
krauss
parents:
34878
diff
changeset
|
229 |
\verb!@!\verb!{thm split_paired_All[rename_abs _ l r]}! |
1faa0fc34174
advertise [rename_abs] attribute in LaTeXsugar -- wish I had known about this earier.
krauss
parents:
34878
diff
changeset
|
230 |
\end{quote} |
40406 | 231 |
produces \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ P\ x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}l\ r{\isaliteral{2E}{\isachardot}}\ P\ {\isaliteral{28}{\isacharparenleft}}l{\isaliteral{2C}{\isacharcomma}}\ r{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}}.% |
16396 | 232 |
\end{isamarkuptext}% |
233 |
\isamarkuptrue% |
|
234 |
% |
|
15893
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
235 |
\isamarkupsubsection{Inference rules% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
236 |
} |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
237 |
\isamarkuptrue% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
238 |
% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
239 |
\begin{isamarkuptext}% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
240 |
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
|
241 |
R\'emy's \texttt{mathpartir} package~\cite{mathpartir} |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
242 |
for typesetting inference rules in your \LaTeX\ file. |
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 |
Writing \verb!@!\verb!{thm[mode=Rule] conjI}! produces |
40406 | 245 |
\isa{\mbox{}\inferrule{\mbox{P}\\\ \mbox{Q}}{\mbox{P\ {\isaliteral{5C3C616E643E}{\isasymand}}\ Q}}}, even in the middle of a sentence. |
15893
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
246 |
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
|
247 |
\begin{center} |
40406 | 248 |
\isa{\mbox{}\inferrule{\mbox{P}\\\ \mbox{Q}}{\mbox{P\ {\isaliteral{5C3C616E643E}{\isasymand}}\ Q}}} {\sc conjI} |
15893
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
249 |
\end{center} |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
250 |
is produced by |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
251 |
\begin{quote} |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
252 |
\verb!\begin{center}!\\ |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
253 |
\verb!@!\verb!{thm[mode=Rule] conjI} {\sc conjI}!\\ |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
254 |
\verb!\end{center}! |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
255 |
\end{quote} |
24497 | 256 |
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
|
257 |
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
|
258 |
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
|
259 |
clash. |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
260 |
|
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
261 |
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
|
262 |
\begin{quote} |
24497 | 263 |
\verb!\begin{center}!\\ |
15893
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
264 |
\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
|
265 |
\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
|
266 |
\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
|
267 |
\verb!\end{center}! |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
268 |
\end{quote} |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
269 |
yields |
24497 | 270 |
\begin{center}\small |
40406 | 271 |
\isa{\mbox{}\inferrule{\mbox{P}\\\ \mbox{Q}}{\mbox{P\ {\isaliteral{5C3C616E643E}{\isasymand}}\ Q}}} {\sc conjI} \\[1ex] |
272 |
\isa{\mbox{}\inferrule{\mbox{P}}{\mbox{P\ {\isaliteral{5C3C6F723E}{\isasymor}}\ Q}}} {\sc disjI$_1$} \qquad |
|
273 |
\isa{\mbox{}\inferrule{\mbox{Q}}{\mbox{P\ {\isaliteral{5C3C6F723E}{\isasymor}}\ Q}}} {\sc disjI$_2$} |
|
15893
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
274 |
\end{center} |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
275 |
|
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
276 |
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
|
277 |
premises for one line: |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
278 |
\begin{center} |
40406 | 279 |
\isa{\mbox{}\inferrule{\mbox{A\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ B}\\\ \mbox{B\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ C}\\\ \mbox{C\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ D}\\\ \mbox{D\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ E}\\\ \mbox{E\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ F}\\\ \mbox{F\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ G}\\\ \mbox{G\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ H}\\\ \mbox{H\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ I}\\\ \mbox{I\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ J}\\\ \mbox{J\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ K}}{\mbox{A\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ K}}} |
15893
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
280 |
\end{center} |
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 |
Limitations: 1. Premises and conclusion must each not be longer than |
40406 | 283 |
the line. 2. Premises that are \isa{{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}}-implications are again |
22387 | 284 |
displayed with a horizontal line, which looks at least unusual. |
285 |
||
286 |
||
287 |
In case you print theorems without premises no rule will be printed by the |
|
288 |
\texttt{Rule} print mode. However, you can use \texttt{Axiom} instead: |
|
289 |
\begin{quote} |
|
24497 | 290 |
\verb!\begin{center}!\\ |
22387 | 291 |
\verb!@!\verb!{thm[mode=Axiom] refl} {\sc refl}! \\ |
292 |
\verb!\end{center}! |
|
293 |
\end{quote} |
|
294 |
yields |
|
24497 | 295 |
\begin{center} |
40406 | 296 |
\isa{\mbox{}\inferrule{\mbox{}}{\mbox{t\ {\isaliteral{3D}{\isacharequal}}\ t}}} {\sc refl} |
22387 | 297 |
\end{center}% |
15893
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
298 |
\end{isamarkuptext}% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
299 |
\isamarkuptrue% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
300 |
% |
24497 | 301 |
\isamarkupsubsection{Displays and font sizes% |
302 |
} |
|
303 |
\isamarkuptrue% |
|
304 |
% |
|
305 |
\begin{isamarkuptext}% |
|
306 |
When displaying theorems with the \texttt{display} option, e.g. |
|
307 |
\verb!@!\verb!{thm[display] refl}! \begin{isabelle}% |
|
40406 | 308 |
t\ {\isaliteral{3D}{\isacharequal}}\ t% |
24497 | 309 |
\end{isabelle} the theorem is |
310 |
set in small font. It uses the \LaTeX-macro \verb!\isastyle!, |
|
311 |
which is also the style that regular theory text is set in, e.g.% |
|
312 |
\end{isamarkuptext}% |
|
313 |
\isamarkuptrue% |
|
314 |
\isacommand{lemma}\isamarkupfalse% |
|
40406 | 315 |
\ {\isaliteral{22}{\isachardoublequoteopen}}t\ {\isaliteral{3D}{\isacharequal}}\ t{\isaliteral{22}{\isachardoublequoteclose}}% |
24497 | 316 |
\isadelimproof |
317 |
% |
|
318 |
\endisadelimproof |
|
319 |
% |
|
320 |
\isatagproof |
|
321 |
% |
|
322 |
\endisatagproof |
|
323 |
{\isafoldproof}% |
|
324 |
% |
|
325 |
\isadelimproof |
|
326 |
% |
|
327 |
\endisadelimproof |
|
328 |
% |
|
329 |
\begin{isamarkuptext}% |
|
330 |
\noindent Otherwise \verb!\isastyleminor! is used, |
|
331 |
which does not modify the font size (assuming you stick to the default |
|
332 |
\verb!\isabellestyle{it}! in \texttt{root.tex}). If you prefer |
|
333 |
normal font size throughout your text, include |
|
334 |
\begin{quote} |
|
335 |
\verb!\renewcommand{\isastyle}{\isastyleminor}! |
|
336 |
\end{quote} |
|
337 |
in \texttt{root.tex}. On the other hand, if you like the small font, |
|
338 |
just put \verb!\isastyle! in front of the text in question, |
|
339 |
e.g.\ at the start of one of the center-environments above. |
|
340 |
||
341 |
The advantage of the display option is that you can display a whole |
|
342 |
list of theorems in one go. For example, |
|
343 |
\verb!@!\verb!{thm[display] foldl.simps}! |
|
344 |
generates \begin{isabelle}% |
|
40406 | 345 |
foldl\ f\ a\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{3D}{\isacharequal}}\ a\isasep\isanewline% |
346 |
foldl\ f\ a\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{5C3C63646F743E}{\isasymcdot}}xs{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ foldl\ f\ {\isaliteral{28}{\isacharparenleft}}f\ a\ x{\isaliteral{29}{\isacharparenright}}\ xs% |
|
24497 | 347 |
\end{isabelle}% |
348 |
\end{isamarkuptext}% |
|
349 |
\isamarkuptrue% |
|
350 |
% |
|
15893
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
351 |
\isamarkupsubsection{If-then% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
352 |
} |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
353 |
\isamarkuptrue% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
354 |
% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
355 |
\begin{isamarkuptext}% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
356 |
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
|
357 |
the body of |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
358 |
\newtheorem{theorem}{Theorem} |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
359 |
\begin{theorem} |
40406 | 360 |
\isa{{\normalsize{}If\,}\ \mbox{i\ {\isaliteral{5C3C6C653E}{\isasymle}}\ j}\ {\normalsize \,and\,}\ \mbox{j\ {\isaliteral{5C3C6C653E}{\isasymle}}\ k}\ {\normalsize \,then\,}\ i\ {\isaliteral{5C3C6C653E}{\isasymle}}\ k{\isaliteral{2E}{\isachardot}}} |
15893
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
361 |
\end{theorem} |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
362 |
by typing |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
363 |
\begin{quote} |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
364 |
\verb!@!\verb!{thm[mode=IfThen] le_trans}! |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
365 |
\end{quote} |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
366 |
|
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
367 |
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
|
368 |
At times this is too drastic: |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
369 |
\begin{theorem} |
40406 | 370 |
\isa{{\normalsize{}If\,}\ \mbox{longpremise}\ {\normalsize \,and\,}\ \mbox{longerpremise}\ {\normalsize \,and\,}\ \mbox{P\ {\isaliteral{28}{\isacharparenleft}}f\ {\isaliteral{28}{\isacharparenleft}}f\ {\isaliteral{28}{\isacharparenleft}}f\ {\isaliteral{28}{\isacharparenleft}}f\ {\isaliteral{28}{\isacharparenleft}}f\ {\isaliteral{28}{\isacharparenleft}}f\ {\isaliteral{28}{\isacharparenleft}}f\ {\isaliteral{28}{\isacharparenleft}}f\ {\isaliteral{28}{\isacharparenleft}}f\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}}\ {\normalsize \,and\,}\ \mbox{longestpremise}\ {\normalsize \,then\,}\ conclusion{\isaliteral{2E}{\isachardot}}} |
15893
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
371 |
\end{theorem} |
16154 | 372 |
In which case you should use \texttt{IfThenNoBox} instead of |
373 |
\texttt{IfThen}: |
|
15893
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
374 |
\begin{theorem} |
40406 | 375 |
\isa{{\normalsize{}If\,}\ longpremise\ {\normalsize \,and\,}\ longerpremise\ {\normalsize \,and\,}\ P\ {\isaliteral{28}{\isacharparenleft}}f\ {\isaliteral{28}{\isacharparenleft}}f\ {\isaliteral{28}{\isacharparenleft}}f\ {\isaliteral{28}{\isacharparenleft}}f\ {\isaliteral{28}{\isacharparenleft}}f\ {\isaliteral{28}{\isacharparenleft}}f\ {\isaliteral{28}{\isacharparenleft}}f\ {\isaliteral{28}{\isacharparenleft}}f\ {\isaliteral{28}{\isacharparenleft}}f\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\normalsize \,and\,}\ longestpremise\ {\normalsize \,then\,}\ conclusion{\isaliteral{2E}{\isachardot}}} |
15893
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
376 |
\end{theorem}% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
377 |
\end{isamarkuptext}% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
378 |
\isamarkuptrue% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
379 |
% |
16166 | 380 |
\isamarkupsubsection{Doing it yourself\label{sec:yourself}% |
16154 | 381 |
} |
382 |
\isamarkuptrue% |
|
383 |
% |
|
384 |
\begin{isamarkuptext}% |
|
385 |
If for some reason you want or need to present theorems your |
|
386 |
own way, you can extract the premises and the conclusion explicitly |
|
387 |
and combine them as you like: |
|
388 |
\begin{itemize} |
|
32893 | 389 |
\item \verb!@!\verb!{thm (prem 1)! $thm$\verb!}! |
390 |
prints premise 1 of $thm$. |
|
391 |
\item \verb!@!\verb!{thm (concl)! $thm$\verb!}! |
|
16154 | 392 |
prints the conclusion of $thm$. |
393 |
\end{itemize} |
|
394 |
For example, ``from \isa{Q} and |
|
40406 | 395 |
\isa{P} we conclude \isa{P\ {\isaliteral{5C3C616E643E}{\isasymand}}\ Q}'' |
16154 | 396 |
is produced by |
397 |
\begin{quote} |
|
32893 | 398 |
\verb!from !\verb!@!\verb!{thm (prem 2) conjI}! \verb!and !\verb!@!\verb!{thm (prem 1) conjI}!\\ |
399 |
\verb!we conclude !\verb!@!\verb!{thm (concl) conjI}! |
|
16154 | 400 |
\end{quote} |
401 |
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
|
402 |
Styles like \verb!(prem 1)! are a general mechanism explained |
16154 | 403 |
in \S\ref{sec:styles}.% |
404 |
\end{isamarkuptext}% |
|
405 |
\isamarkuptrue% |
|
406 |
% |
|
15893
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
407 |
\isamarkupsubsection{Patterns% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
408 |
} |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
409 |
\isamarkuptrue% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
410 |
% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
411 |
\begin{isamarkuptext}% |
17134 | 412 |
In \S\ref{sec:varnames} we shows how to create patterns containing |
413 |
``\isa{\_}''. |
|
15893
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
414 |
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
|
415 |
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
|
416 |
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
|
417 |
following: |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
418 |
|
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
419 |
\begin{center} |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
420 |
\begin{tabular}{l@ {~~produced by~~}l} |
40406 | 421 |
\isa{\textsf{let}\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}\ \_{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ p\ \textsf{in}\ t} & \verb!@!\verb!{term "let x = fst p in t"}!\\ |
422 |
\isa{\textsf{let}\ {\isaliteral{28}{\isacharparenleft}}\_{\isaliteral{2C}{\isacharcomma}}\ x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ p\ \textsf{in}\ t} & \verb!@!\verb!{term "let x = snd p in t"}!\\ |
|
423 |
\isa{\textsf{let}\ x{\isaliteral{5C3C63646F743E}{\isasymcdot}}\_\ {\isaliteral{3D}{\isacharequal}}\ xs\ \textsf{in}\ t} & \verb!@!\verb!{term "let x = hd xs in t"}!\\ |
|
424 |
\isa{\textsf{let}\ \_{\isaliteral{5C3C63646F743E}{\isasymcdot}}x\ {\isaliteral{3D}{\isacharequal}}\ xs\ \textsf{in}\ t} & \verb!@!\verb!{term "let x = tl xs in t"}!\\ |
|
425 |
\isa{\textsf{let}\ Some\ x\ {\isaliteral{3D}{\isacharequal}}\ y\ \textsf{in}\ t} & \verb!@!\verb!{term "let x = the y in t"}!\\ |
|
15893
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
426 |
\end{tabular} |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
427 |
\end{center}% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
428 |
\end{isamarkuptext}% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
429 |
\isamarkuptrue% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
430 |
% |
16155 | 431 |
\isamarkupsection{Proofs% |
15893
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
432 |
} |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
433 |
\isamarkuptrue% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
434 |
% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
435 |
\begin{isamarkuptext}% |
24497 | 436 |
Full proofs, even if written in beautiful Isar style, are |
437 |
likely to be too long and detailed to be included in conference |
|
438 |
papers, but some key lemmas might be of interest. |
|
439 |
It is usually easiest to put them in figures like the one in Fig.\ |
|
440 |
\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
|
441 |
\end{isamarkuptext}% |
17175 | 442 |
\isamarkuptrue% |
15893
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
443 |
% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
444 |
\begin{figure} |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
445 |
\begin{center}\begin{minipage}{0.6\textwidth} |
24497 | 446 |
\isastyleminor\isamarkuptrue |
17175 | 447 |
\isacommand{lemma}\isamarkupfalse% |
448 |
\ True\isanewline |
|
17125 | 449 |
% |
450 |
\isadelimproof |
|
451 |
% |
|
452 |
\endisadelimproof |
|
453 |
% |
|
454 |
\isatagproof |
|
17175 | 455 |
\isacommand{proof}\isamarkupfalse% |
40406 | 456 |
\ {\isaliteral{2D}{\isacharminus}}\isanewline |
15893
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
457 |
\ \ % |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
458 |
\isamarkupcmt{pretty trivial% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
459 |
} |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
460 |
\isanewline |
17175 | 461 |
\ \ \isacommand{show}\isamarkupfalse% |
462 |
\ True\ \isacommand{by}\isamarkupfalse% |
|
463 |
\ force\isanewline |
|
464 |
\isacommand{qed}\isamarkupfalse% |
|
465 |
% |
|
17125 | 466 |
\endisatagproof |
467 |
{\isafoldproof}% |
|
468 |
% |
|
469 |
\isadelimproof |
|
470 |
% |
|
471 |
\endisadelimproof |
|
15893
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
472 |
% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
473 |
\end{minipage}\end{center} |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
474 |
\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
|
475 |
\end{figure} |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
476 |
% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
477 |
\begin{isamarkuptext}% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
478 |
\begin{quote} |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
479 |
\small |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
480 |
\verb!text_raw {!\verb!*!\\ |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
481 |
\verb! \begin{figure}!\\ |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
482 |
\verb! \begin{center}\begin{minipage}{0.6\textwidth}!\\ |
24497 | 483 |
\verb! \isastyleminor\isamarkuptrue!\\ |
15893
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
484 |
\verb!*!\verb!}!\\ |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
485 |
\verb!lemma True!\\ |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
486 |
\verb!proof -!\\ |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
487 |
\verb! -- "pretty trivial"!\\ |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
488 |
\verb! show True by force!\\ |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
489 |
\verb!qed!\\ |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
490 |
\verb!text_raw {!\verb!*!\\ |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
491 |
\verb! \end{minipage}\end{center}!\\ |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
492 |
\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
|
493 |
\verb! \end{figure}!\\ |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
494 |
\verb!*!\verb!}! |
24497 | 495 |
\end{quote} |
496 |
||
497 |
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
|
498 |
\end{isamarkuptext}% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
499 |
\isamarkuptrue% |
15953 | 500 |
% |
16155 | 501 |
\isamarkupsection{Styles\label{sec:styles}% |
15953 | 502 |
} |
503 |
\isamarkuptrue% |
|
504 |
% |
|
505 |
\begin{isamarkuptext}% |
|
506 |
The \verb!thm! antiquotation works nicely for single theorems, but |
|
507 |
sets of equations as used in definitions are more difficult to |
|
40406 | 508 |
typeset nicely: people tend to prefer aligned \isa{{\isaliteral{3D}{\isacharequal}}} signs. |
15953 | 509 |
|
510 |
To deal with such cases where it is desirable to dive into the structure |
|
16040 | 511 |
of terms and theorems, Isabelle offers antiquotations featuring |
15953 | 512 |
``styles'': |
513 |
||
514 |
\begin{quote} |
|
32893 | 515 |
\verb!@!\verb!{thm (style) thm}!\\ |
516 |
\verb!@!\verb!{prop (style) thm}!\\ |
|
32898
e871d897969c
term styles also cover antiquotations term_type and typeof
haftmann
parents:
32893
diff
changeset
|
517 |
\verb!@!\verb!{term (style) term}!\\ |
e871d897969c
term styles also cover antiquotations term_type and typeof
haftmann
parents:
32893
diff
changeset
|
518 |
\verb!@!\verb!{term_type (style) term}!\\ |
e871d897969c
term styles also cover antiquotations term_type and typeof
haftmann
parents:
32893
diff
changeset
|
519 |
\verb!@!\verb!{typeof (style) term}!\\ |
15953 | 520 |
\end{quote} |
521 |
||
32898
e871d897969c
term styles also cover antiquotations term_type and typeof
haftmann
parents:
32893
diff
changeset
|
522 |
A ``style'' is a transformation of a term. There are predefined |
32893 | 523 |
styles, namely \verb!lhs! and \verb!rhs!, \verb!prem! with one argument, and \verb!concl!. |
16166 | 524 |
For example, |
16076 | 525 |
the output |
15953 | 526 |
\begin{center} |
40406 | 527 |
\begin{tabular}{l@ {~~\isa{{\isaliteral{3D}{\isacharequal}}}~~}l} |
528 |
\isa{foldl\ f\ a\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}} & \isa{a}\\ |
|
529 |
\isa{foldl\ f\ a\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{5C3C63646F743E}{\isasymcdot}}xs{\isaliteral{29}{\isacharparenright}}} & \isa{foldl\ f\ {\isaliteral{28}{\isacharparenleft}}f\ a\ x{\isaliteral{29}{\isacharparenright}}\ xs} |
|
15953 | 530 |
\end{tabular} |
531 |
\end{center} |
|
532 |
is produced by the following code: |
|
533 |
\begin{quote} |
|
534 |
\verb!\begin{center}!\\ |
|
535 |
\verb!\begin{tabular}{l@ {~~!\verb!@!\verb!{text "="}~~}l}!\\ |
|
33323 | 536 |
\verb!@!\verb!{thm (lhs) foldl_Nil} & @!\verb!{thm (rhs) foldl_Nil}\\!\\ |
32893 | 537 |
\verb!@!\verb!{thm (lhs) foldl_Cons} & @!\verb!{thm (rhs) foldl_Cons}!\\ |
15953 | 538 |
\verb!\end{tabular}!\\ |
539 |
\verb!\end{center}! |
|
540 |
\end{quote} |
|
541 |
Note the space between \verb!@! and \verb!{! in the tabular argument. |
|
542 |
It prevents Isabelle from interpreting \verb!@ {~~...~~}! |
|
16076 | 543 |
as an antiquotation. The styles \verb!lhs! and \verb!rhs! |
27094 | 544 |
extract the left hand side (or right hand side respectively) from the |
16076 | 545 |
conclusion of propositions consisting of a binary operator |
40406 | 546 |
(e.~g.~\isa{{\isaliteral{3D}{\isacharequal}}}, \isa{{\isaliteral{5C3C65717569763E}{\isasymequiv}}}, \isa{{\isaliteral{3C}{\isacharless}}}). |
15953 | 547 |
|
16166 | 548 |
Likewise, \verb!concl! may be used as a style to show just the |
16076 | 549 |
conclusion of a proposition. For example, take \verb!hd_Cons_tl!: |
16040 | 550 |
\begin{center} |
40406 | 551 |
\isa{xs\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ hd\ xs{\isaliteral{5C3C63646F743E}{\isasymcdot}}tl\ xs\ {\isaliteral{3D}{\isacharequal}}\ xs} |
16040 | 552 |
\end{center} |
553 |
To print just the conclusion, |
|
15953 | 554 |
\begin{center} |
40406 | 555 |
\isa{hd\ xs{\isaliteral{5C3C63646F743E}{\isasymcdot}}tl\ xs\ {\isaliteral{3D}{\isacharequal}}\ xs} |
15953 | 556 |
\end{center} |
16040 | 557 |
type |
15953 | 558 |
\begin{quote} |
559 |
\verb!\begin{center}!\\ |
|
33323 | 560 |
\verb!@!\verb!{thm (concl) hd_Cons_tl}!\\ |
15953 | 561 |
\verb!\end{center}! |
562 |
\end{quote} |
|
17134 | 563 |
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
|
564 |
the style, as in this example. |
17125 | 565 |
|
16166 | 566 |
Further use cases can be found in \S\ref{sec:yourself}. |
15953 | 567 |
If you are not afraid of ML, you may also define your own styles. |
32893 | 568 |
Have a look at module \verb|Term_Style|.% |
15953 | 569 |
\end{isamarkuptext}% |
17175 | 570 |
\isamarkuptrue% |
17125 | 571 |
% |
572 |
\isadelimtheory |
|
573 |
% |
|
574 |
\endisadelimtheory |
|
575 |
% |
|
576 |
\isatagtheory |
|
577 |
% |
|
578 |
\endisatagtheory |
|
579 |
{\isafoldtheory}% |
|
580 |
% |
|
581 |
\isadelimtheory |
|
582 |
% |
|
583 |
\endisadelimtheory |
|
15893
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
584 |
\end{isabellebody}% |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
585 |
%%% Local Variables: |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
586 |
%%% mode: latex |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
587 |
%%% TeX-master: "root" |
c0cd613a49eb
move generated files to document/, avoid CVS file overwrite in generated/
kleing
parents:
diff
changeset
|
588 |
%%% End: |