doc-src/LaTeXsugar/Sugar/Sugar.thy
author haftmann
Sat May 14 21:31:13 2005 +0200 (2005-05-14)
changeset 15960 9bd6550dc004
parent 15953 902b556e4bc0
child 15983 a53abeedc879
permissions -rw-r--r--
added Proof.context to antiquotation
     1 (*<*)
     2 theory Sugar
     3 imports LaTeXsugar OptionalSugar
     4 begin
     5 (*>*)
     6 
     7 section "Introduction"
     8 
     9 text{* This document is for those Isabelle users who 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}, \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 instant 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. You merely need to load the right files:
    35 \begin{itemize}
    36 \item Import theory \texttt{LaTeXsugar} in the header of your own
    37 theory.  You may also want bits of \texttt{OptionalSugar}, which you can
    38 copy selectively into your own theory or import as a whole.  Both
    39 theories live in \texttt{HOL/Library} and are found automatically.
    40 
    41 \item Should you need additional \LaTeX\ packages (the text will tell
    42 you so), you include them at the beginning of your \LaTeX\ document,
    43 typically in \texttt{root.tex}.
    44 \end{itemize}
    45 *}
    46 
    47 section{* HOL syntax*}
    48 
    49 subsection{* Logic *}
    50 
    51 text{* The predefined constructs @{text"if"}, @{text"let"} and
    52 @{text"case"} are set in sans serif font to distinguish them from
    53 other functions. This improves readability:
    54 \begin{itemize}
    55 \item @{term"if b then e\<^isub>1 else e\<^isub>2"} instead of @{text"if b then e\<^isub>1 else e\<^isub>2"}.
    56 \item @{term"let x = e\<^isub>1 in e\<^isub>2"} instead of @{text"let x = e\<^isub>1 in e\<^isub>2"}.
    57 \item @{term"case x of True \<Rightarrow> e\<^isub>1 | False \<Rightarrow> e\<^isub>2"} instead of\\
    58       @{text"case x of True \<Rightarrow> e\<^isub>1 | False \<Rightarrow> e\<^isub>2"}.
    59 \end{itemize}
    60 *}
    61 
    62 subsection{* Sets *}
    63 
    64 text{* Although set syntax in HOL is already close to
    65 standard, we provide a few further improvements:
    66 \begin{itemize}
    67 \item @{term"{x. P}"} instead of @{text"{x. P}"}.
    68 \item @{term"{}"} instead of @{text"{}"}.
    69 \item @{term"insert a (insert b (insert c M))"} instead of @{text"insert a (insert b (insert c M))"}.
    70 \end{itemize}
    71 *}
    72 
    73 subsection{* Lists *}
    74 
    75 text{* If lists are used heavily, the following notations increase readability:
    76 \begin{itemize}
    77 \item @{term"x # xs"} instead of @{text"x # xs"}.
    78       Exceptionally, @{term"x # xs"} is also input syntax.
    79 If you prefer more space around the $\cdot$ you have to redefine
    80 \verb!\isasymcdot! in \LaTeX:
    81 \verb!\renewcommand{\isasymcdot}{\isamath{\,\cdot\,}}!
    82 
    83 \item @{term"length xs"} instead of @{text"length xs"}.
    84 \item @{term"nth xs n"} instead of @{text"nth xs n"},
    85       the $n$th element of @{text xs}.
    86 
    87 \item The @{text"@"} operation associates implicitly to the right,
    88 which leads to unpleasant line breaks if the term is too long for one
    89 line. To avoid this, \texttt{OptionalSugar} contains syntax to group
    90 @{text"@"}-terms to the left before printing, which leads to better
    91 line breaking behaviour:
    92 @{term[display]"term\<^isub>0 @ term\<^isub>1 @ term\<^isub>2 @ term\<^isub>3 @ term\<^isub>4 @ term\<^isub>5 @ term\<^isub>6 @ term\<^isub>7 @ term\<^isub>8 @ term\<^isub>9 @ term\<^isub>1\<^isub>0"}
    93 
    94 \end{itemize}
    95 *}
    96 
    97 section "Printing theorems"
    98 
    99 subsection "Question marks"
   100 
   101 text{* If you print anything, especially theorems, containing
   102 schematic variables they are prefixed with a question mark:
   103 \verb!@!\verb!{thm conjI}! results in @{thm conjI}. Most of the time
   104 you would rather not see the question marks. There is an attribute
   105 \verb!no_vars! that you can attach to the theorem that turns its
   106 schematic into ordinary free variables: \verb!@!\verb!{thm conjI[no_vars]}!
   107 results in @{thm conjI[no_vars]}.
   108 
   109 This \verb!no_vars! business can become a bit tedious.
   110 If you would rather never see question marks, simply put
   111 \begin{verbatim}
   112 reset show_var_qmarks;
   113 \end{verbatim}
   114 at the beginning of your file \texttt{ROOT.ML}.
   115 The rest of this document is produced with this flag reset.
   116 *}
   117 
   118 (*<*)ML"reset show_var_qmarks"(*>*)
   119 
   120 subsection "Inference rules"
   121 
   122 text{* To print theorems as inference rules you need to include Didier
   123 R\'emy's \texttt{mathpartir} package~\cite{mathpartir}
   124 for typesetting inference rules in your \LaTeX\ file.
   125 
   126 Writing \verb!@!\verb!{thm[mode=Rule] conjI}! produces
   127 @{thm[mode=Rule] conjI}, even in the middle of a sentence.
   128 If you prefer your inference rule on a separate line, maybe with a name,
   129 \begin{center}
   130 @{thm[mode=Rule] conjI} {\sc conjI}
   131 \end{center}
   132 is produced by
   133 \begin{quote}
   134 \verb!\begin{center}!\\
   135 \verb!@!\verb!{thm[mode=Rule] conjI} {\sc conjI}!\\
   136 \verb!\end{center}!
   137 \end{quote}
   138 It is not recommended to use the standard \texttt{display} attribute
   139 together with \texttt{Rule} because centering does not work and because
   140 the line breaking mechanisms of \texttt{display} and \texttt{mathpartir} can
   141 clash.
   142 
   143 Of course you can display multiple rules in this fashion:
   144 \begin{quote}
   145 \verb!\begin{center}\isastyle!\\
   146 \verb!@!\verb!{thm[mode=Rule] conjI} {\sc conjI} \\[1ex]!\\
   147 \verb!@!\verb!{thm[mode=Rule] conjE} {\sc disjI$_1$} \qquad!\\
   148 \verb!@!\verb!{thm[mode=Rule] disjE} {\sc disjI$_2$}!\\
   149 \verb!\end{center}!
   150 \end{quote}
   151 yields
   152 \begin{center}\isastyle
   153 @{thm[mode=Rule] conjI} {\sc conjI} \\[1ex]
   154 @{thm[mode=Rule] disjI1} {\sc disjI$_1$} \qquad
   155 @{thm[mode=Rule] disjI2} {\sc disjI$_2$}
   156 \end{center}
   157 Note that we included \verb!\isastyle! to obtain
   158 the smaller font that otherwise comes only with \texttt{display}.
   159 
   160 The \texttt{mathpartir} package copes well if there are too many
   161 premises for one line:
   162 \begin{center}
   163 @{prop[mode=Rule] "\<lbrakk> A \<longrightarrow> B; B \<longrightarrow> C; C \<longrightarrow> D; D \<longrightarrow> E; E \<longrightarrow> F; F \<longrightarrow> G;
   164  G \<longrightarrow> H; H \<longrightarrow> I; I \<longrightarrow> J; J \<longrightarrow> K \<rbrakk> \<Longrightarrow> A \<longrightarrow> K"}
   165 \end{center}
   166 
   167 Limitations: 1. Premises and conclusion must each not be longer than
   168 the line.  2. Premises that are @{text"\<Longrightarrow>"}-implications are again
   169 displayed with a horizontal line, which looks at least unusual.
   170 
   171 *}
   172 
   173 subsection{*If-then*}
   174 
   175 text{* If you prefer a fake ``natural language'' style you can produce
   176 the body of
   177 \newtheorem{theorem}{Theorem}
   178 \begin{theorem}
   179 @{thm[mode=IfThen] le_trans}
   180 \end{theorem}
   181 by typing
   182 \begin{quote}
   183 \verb!@!\verb!{thm[mode=IfThen] le_trans}!
   184 \end{quote}
   185 
   186 In order to prevent odd line breaks, the premises are put into boxes.
   187 At times this is too drastic:
   188 \begin{theorem}
   189 @{prop[mode=IfThen] "longpremise \<Longrightarrow> longerpremise \<Longrightarrow> P(f(f(f(f(f(f(f(f(f(x)))))))))) \<Longrightarrow> longestpremise \<Longrightarrow> conclusion"}
   190 \end{theorem}
   191 In which case you should use \texttt{mode=IfThenNoBox} instead of
   192 \texttt{mode=IfThen}:
   193 \begin{theorem}
   194 @{prop[mode=IfThenNoBox] "longpremise \<Longrightarrow> longerpremise \<Longrightarrow> P(f(f(f(f(f(f(f(f(f(x)))))))))) \<Longrightarrow> longestpremise \<Longrightarrow> conclusion"}
   195 \end{theorem}
   196 *}
   197 
   198 subsection "Patterns"
   199 
   200 text {*
   201   Sometimes functions ignore one or more of their
   202   arguments and some functional languages have nice 
   203   syntax for that as in @{thm hd.simps [where xs=DUMMY]}.
   204 
   205   You can simulate this in Isabelle by instantiating the @{term xs} in
   206   definition \mbox{@{thm hd.simps}} with a constant @{text DUMMY} that
   207   is printed as @{term DUMMY}. The code for the pattern above is 
   208   \verb!@!\verb!{thm hd.simps [where xs=DUMMY]}!.
   209 
   210   You can drive this game even further and extend the syntax of let
   211   bindings such that certain functions like @{term fst}, @{term hd}, 
   212   etc.\ are printed as patterns. \texttt{OptionalSugar} provides the
   213   following:
   214   
   215   \begin{center}
   216   \begin{tabular}{l@ {~~produced by~~}l}
   217   @{term "let x = fst p in t"} & \verb!@!\verb!{term "let x = fst p in t"}!\\
   218   @{term "let x = snd p in t"} & \verb!@!\verb!{term "let x = snd p in t"}!\\
   219   @{term "let x = hd xs in t"} & \verb!@!\verb!{term "let x = hd xs in t"}!\\
   220   @{term "let x = tl xs in t"} & \verb!@!\verb!{term "let x = tl xs in t"}!\\
   221   @{term "let x = the y in t"} & \verb!@!\verb!{term "let x = the y in t"}!\\
   222   \end{tabular}
   223   \end{center}
   224 *}
   225 
   226 subsection "Proofs"
   227 
   228 text {*
   229   Full proofs, even if written in beautiful Isar style, are likely to
   230   be too long and detailed to be included in conference papers, but
   231   some key lemmas might be of interest.
   232 
   233   It is usually easiest to put them in figures like the one in Fig.\
   234   \ref{fig:proof}. This was achieved with the \isakeyword{text\_raw}
   235   command:
   236 *}
   237 text_raw {*
   238   \begin{figure}
   239   \begin{center}\begin{minipage}{0.6\textwidth}  
   240   \isastyle\isamarkuptrue
   241 *}
   242 lemma True
   243 proof -
   244   -- "pretty trivial"
   245   show True by force
   246 qed
   247 text_raw {*    
   248   \end{minipage}\end{center}
   249   \caption{Example proof in a figure.}\label{fig:proof}
   250   \end{figure}
   251 *}
   252 text {*
   253 
   254 \begin{quote}
   255 \small
   256 \verb!text_raw {!\verb!*!\\
   257 \verb!  \begin{figure}!\\
   258 \verb!  \begin{center}\begin{minipage}{0.6\textwidth}!\\
   259 \verb!  \isastyle\isamarkuptrue!\\
   260 \verb!*!\verb!}!\\
   261 \verb!lemma True!\\
   262 \verb!proof -!\\
   263 \verb!  -- "pretty trivial"!\\
   264 \verb!  show True by force!\\
   265 \verb!qed!\\
   266 \verb!text_raw {!\verb!*!\\
   267 \verb!  \end{minipage}\end{center}!\\
   268 \verb!  \caption{Example proof in a figure.}\label{fig:proof}!\\
   269 \verb!  \end{figure}!\\
   270 \verb!*!\verb!}!
   271 \end{quote}
   272   
   273 *}
   274 
   275 subsection "Styles"
   276 
   277 text {*
   278   The \verb!thm! antiquotation works nicely for single theorems, but
   279   sets of equations as used in definitions are more difficult to
   280   typeset nicely: for some reason people tend to prefer aligned 
   281   @{text "="} signs.
   282 
   283   To deal with such cases where it is desirable to dive into the structure
   284   of terms and theorems, Isabelle offers two antiquotations featuring
   285   ``styles'':
   286 
   287     \begin{quote}
   288     \verb!@!\verb!{thm_style stylename thm}!\\
   289     \verb!@!\verb!{term_style stylename term}!
   290     \end{quote}
   291 
   292   A ``style'' is a transformation of terms. There are three predefined
   293   styles, named \verb!lhs!, \verb!rhs! and \verb!conclusion!, with obvious
   294   meanings. For example, the output
   295   \begin{center}
   296   \begin{tabular}{l@ {~~@{text "="}~~}l}
   297   @{thm_style lhs foldl_Nil} & @{thm_style rhs foldl_Nil}\\
   298   @{thm_style lhs foldl_Cons} & @{thm_style rhs foldl_Cons}
   299   \end{tabular}
   300   \end{center}
   301   is produced by the following code:
   302   \begin{quote}
   303     \verb!\begin{center}!\\
   304     \verb!\begin{tabular}{l@ {~~!\verb!@!\verb!{text "="}~~}l}!\\
   305     \verb!@!\verb!{thm_style lhs foldl_Nil} & @!\verb!{thm_style rhs foldl_Nil}!\\
   306     \verb!@!\verb!{thm_style lhs foldl_Cons} & @!\verb!{thm_style rhs foldl_Cons}!\\
   307     \verb!\end{tabular}!\\
   308     \verb!\end{center}!
   309   \end{quote}
   310   Note the space between \verb!@! and \verb!{! in the tabular argument.
   311   It prevents Isabelle from interpreting \verb!@ {~~...~~}! 
   312   as an antiquotation. Both styles \verb!lhs! and \verb!rhs! 
   313   try to be smart about the interpretation of the theorem they transform
   314   they work just as well for meta equality @{text "\<equiv>"} and other
   315   binary operators like @{text "<"}.
   316 
   317   Likewise \verb!conclusion! may be used as style to show just the conclusion
   318   of a formula:
   319   \begin{center}
   320     @{thm_style conclusion hd_Cons_tl}
   321   \end{center}
   322   is produced by
   323   \begin{quote}
   324     \verb!\begin{center}!\\
   325     \verb!@!\verb!{thm_style conclusion hd_Cons_tl}!\\
   326     \verb!\end{center}!
   327   \end{quote}
   328 
   329   If you are not afraid of ML, you may also define your own styles.
   330   A style is implemented by an ML function of type
   331   \verb!Proof.context -> term -> term!.
   332   Have a look at the following example:
   333 
   334   \begin{quote}
   335     \verb!setup {!\verb!*!\\
   336     \verb!let!\\
   337     \verb!  fun my_lhs ctxt (Const ("==", _) $ t $ _) = t!\\
   338     \verb!    | my_lhs ctxt (Const ("Trueprop", _) $ t) = my_lhs ctxt t!\\
   339     \verb!    | my_lhs ctxt (Const ("==>", _) $ _ $ t) = my_lhs ctxt t!\\
   340     \verb!    | my_lhs ctxt (_ $ t $ _) = t!\\
   341     \verb!    | my_lhs ctxt _ = error ("Binary operator expected")!\\
   342     \verb!  in [TermStyle.update_style "new_lhs" my_lhs]!\\
   343     \verb!end;!\\
   344     \verb!*!\verb!}!\\
   345   \end{quote}
   346 
   347   This example indeed shows a way the \verb!lhs! style could be implemented;
   348   note that the real implementation is more sophisticated.
   349 
   350   This code must go into your theory file, not as part of your
   351   \LaTeX\ text but as a separate command in front of it.
   352   Like in this example, it is recommended to put the definition of the style
   353   function into a \verb!let! expression, in order not to pollute the
   354   ML global namespace. Each style receives the current proof context
   355   as first argument; this is necessary in situations where the current proof
   356   context has an impact on the style (which is the case e.~g.~when the
   357   style has some object-logic specific behaviour).
   358 
   359   The mapping from identifier name to the style function
   360   is done by the \verb!Style.update_style! expression which expects the desired
   361   style name and the style function as arguments.
   362   
   363   After this \verb!setup!,
   364   there will be a new style available named \verb!new_lhs!, thus allowing
   365   antiquoations like \verb!@!\verb!{thm_style new_lhs rev_map}!
   366   yielding @{thm_style lhs rev_map}.
   367 
   368   The example above may be used as as a ``copy-and-paste'' pattern to write
   369   your own styles; for a description of the constructs used, please refer
   370   to the Isabelle reference manual.
   371 
   372 
   373 *}
   374 
   375 (*<*)
   376 end
   377 (*>*)