|
1 (*<*) |
|
2 theory Sugar |
|
3 imports Main |
|
4 begin |
|
5 (*>*) |
|
6 |
|
7 section "Introduction" |
|
8 |
|
9 text{* This document is for those Isabelle users that have mastered |
|
10 the art of mixing \LaTeX\ text and Isabelle theories and never want to |
|
11 typeset a theorem by hand anymore because they have experienced the |
|
12 bliss of writing \verb!@!\verb!{thm[display]setsum_cartesian_product[no_vars]}! |
|
13 and seeing Isabelle typeset it for them: |
|
14 @{thm[display,eta_contract=false] setsum_cartesian_product[no_vars]} |
|
15 No typos, no omissions, no sweat! |
|
16 If you have not experienced that joy, read chapter 4, \emph{Presenting |
|
17 Theories}, of \cite{LNCS2283} first. |
|
18 |
|
19 If you have mastered the art of Isabelle's \emph{antiquotations}, |
|
20 i.e.\ things like the above \verb!@!\verb!{thm...}!, beware: in your vanity |
|
21 you may be tempted to think that all readers of the stunning ps or pdf |
|
22 documents you can now produce at the drop of a hat will be struck with |
|
23 awe at the beauty unfolding in front of their eyes. Until one day you |
|
24 come across that very critical of readers known as the ``common referee''. |
|
25 He has the nasty habit of refusing to understand unfamiliar notation |
|
26 like Isabelle's infamous @{text"\<lbrakk> \<rbrakk> \<Longrightarrow>"} no matter how many times you |
|
27 explain it in your paper. Even worse, he thinks that using @{text"\<lbrakk> |
|
28 \<rbrakk>"} for anything other than denotational semantics is a cardinal sin |
|
29 that must be punished by immediate rejection. |
|
30 |
|
31 |
|
32 This document shows you how to make Isabelle and \LaTeX\ cooperate to |
|
33 produce ordinary looking mathematics that hides the fact that it was |
|
34 typeset by a machine. This involves additional syntax-related |
|
35 declarations for your theory file and corresponding \LaTeX\ macros. We |
|
36 explain how to use them but show neither. They can be downloaded from |
|
37 the web. |
|
38 |
|
39 *} |
|
40 |
|
41 section "Printing theorems" |
|
42 |
|
43 subsection "Inference rules" |
|
44 |
|
45 (*<*) |
|
46 syntax (Rule output) |
|
47 "==>" :: "prop \<Rightarrow> prop \<Rightarrow> prop" |
|
48 ("\<^raw:\mbox{}\inferrule{>_\<^raw:}>\<^raw:{>_\<^raw:}>") |
|
49 |
|
50 "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop" |
|
51 ("\<^raw:\mbox{}\inferrule{>_\<^raw:}>\<^raw:{>_\<^raw:}>") |
|
52 |
|
53 "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" |
|
54 ("_\<^raw:\\>/ _") |
|
55 |
|
56 "_asm" :: "prop \<Rightarrow> asms" ("_") |
|
57 (*>*) |
|
58 |
|
59 text{* To print theorems as inference rules you need to include the |
|
60 \texttt{Rule} output syntax declarations in your theory and Didier |
|
61 Remy's \texttt{mathpartir} package for typesetting inference rules in |
|
62 your \LaTeX\ file. |
|
63 |
|
64 Writing \verb!@!\verb!{thm[mode=Rule] conjI[no_vars]}! produces |
|
65 @{thm[mode=Rule] conjI[no_vars]}, even in the middle of a sentence. |
|
66 The standard \texttt{display} attribute, i.e.\ writing |
|
67 \verb![mode=Rule,display]! instead of \verb![mode=Rule]!, |
|
68 displays the rule on a separate line using a smaller font: |
|
69 @{thm[mode=Rule,display] conjI[no_vars]} |
|
70 Centering a display does not work directly. Instead you can enclose the |
|
71 non-displayed variant in a \texttt{center} environment: |
|
72 |
|
73 \begin{quote} |
|
74 \verb!\begin{center}!\\ |
|
75 \verb!@!\verb!{thm[mode=Rule] conjI[no_vars]} {\sc conjI}!\\ |
|
76 \verb!\end{center}! |
|
77 \end{quote} |
|
78 also adds a label to the rule and yields |
|
79 \begin{center} |
|
80 @{thm[mode=Rule] conjI[no_vars]} {\sc conjI} |
|
81 \end{center} |
|
82 Of course you can display multiple rules in this fashion: |
|
83 \begin{quote} |
|
84 \verb!\begin{center}\isastyle!\\ |
|
85 \verb!@!\verb!{thm[mode=Rule] conjI[no_vars]} {\sc conjI} \\[1ex]!\\ |
|
86 \verb!@!\verb!{thm[mode=Rule] conjE[no_vars]} {\sc disjI$_1$} \qquad!\\ |
|
87 \verb!@!\verb!{thm[mode=Rule] disjE[no_vars]} {\sc disjI$_2$}!\\ |
|
88 \verb!\end{center}! |
|
89 \end{quote} |
|
90 yields |
|
91 \begin{center}\isastyle |
|
92 @{thm[mode=Rule] conjI[no_vars]} {\sc conjI} \\[1ex] |
|
93 @{thm[mode=Rule] disjI1[no_vars]} {\sc disjI$_1$} \qquad |
|
94 @{thm[mode=Rule] disjI2[no_vars]} {\sc disjI$_2$} |
|
95 \end{center} |
|
96 Note that we included \verb!\isastyle! to obtain |
|
97 the smaller font that otherwise comes only with \texttt{display}. |
|
98 |
|
99 *} |
|
100 (*<*) |
|
101 end |
|
102 (*>*) |