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