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