doc-src/LaTeXsugar/Sugar/Sugar.thy
author wenzelm
Thu Jan 19 21:22:08 2006 +0100 (2006-01-19 ago)
changeset 18708 4b3dadb4fe33
parent 17127 65e340b6a56f
child 21558 63278052bb72
permissions -rw-r--r--
setup: theory -> theory;
     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}. For a start, you should
    44 \verb!\usepackage{amssymb}! --- otherwise typesetting
    45 @{prop[source]"\<not>(\<exists>x. P x)"} will fail because the AMS symbol
    46 @{text"\<nexists>"} is missing.
    47 \end{itemize}
    48 *}
    49 
    50 section{* HOL syntax*}
    51 
    52 subsection{* Logic *}
    53 
    54 text{* 
    55   The formula @{prop[source]"\<not>(\<exists>x. P x)"} is typeset as @{prop"~(EX x. P x)"}.
    56 
    57 The predefined constructs @{text"if"}, @{text"let"} and
    58 @{text"case"} are set in sans serif font to distinguish them from
    59 other functions. This improves readability:
    60 \begin{itemize}
    61 \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"}.
    62 \item @{term"let x = e\<^isub>1 in e\<^isub>2"} instead of @{text"let x = e\<^isub>1 in e\<^isub>2"}.
    63 \item @{term"case x of True \<Rightarrow> e\<^isub>1 | False \<Rightarrow> e\<^isub>2"} instead of\\
    64       @{text"case x of True \<Rightarrow> e\<^isub>1 | False \<Rightarrow> e\<^isub>2"}.
    65 \end{itemize}
    66 *}
    67 
    68 subsection{* Sets *}
    69 
    70 text{* Although set syntax in HOL is already close to
    71 standard, we provide a few further improvements:
    72 \begin{itemize}
    73 \item @{term"{x. P}"} instead of @{text"{x. P}"}.
    74 \item @{term"{}"} instead of @{text"{}"}.
    75 \item @{term"insert a (insert b (insert c M))"} instead of @{text"insert a (insert b (insert c M))"}.
    76 \end{itemize}
    77 *}
    78 
    79 subsection{* Lists *}
    80 
    81 text{* If lists are used heavily, the following notations increase readability:
    82 \begin{itemize}
    83 \item @{term"x # xs"} instead of @{text"x # xs"}.
    84       Exceptionally, @{term"x # xs"} is also input syntax.
    85 If you prefer more space around the $\cdot$ you have to redefine
    86 \verb!\isasymcdot! in \LaTeX:
    87 \verb!\renewcommand{\isasymcdot}{\isamath{\,\cdot\,}}!
    88 
    89 \item @{term"length xs"} instead of @{text"length xs"}.
    90 \item @{term"nth xs n"} instead of @{text"nth xs n"},
    91       the $n$th element of @{text xs}.
    92 
    93 \item The @{text"@"} operation associates implicitly to the right,
    94 which leads to unpleasant line breaks if the term is too long for one
    95 line. To avoid this, \texttt{OptionalSugar} contains syntax to group
    96 @{text"@"}-terms to the left before printing, which leads to better
    97 line breaking behaviour:
    98 @{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"}
    99 
   100 \end{itemize}
   101 *}
   102 
   103 section "Printing theorems"
   104 
   105 subsection "Question marks"
   106 
   107 text{* If you print anything, especially theorems, containing
   108 schematic variables they are prefixed with a question mark:
   109 \verb!@!\verb!{thm conjI}! results in @{thm conjI}. Most of the time
   110 you would rather not see the question marks. There is an attribute
   111 \verb!no_vars! that you can attach to the theorem that turns its
   112 schematic into ordinary free variables: \verb!@!\verb!{thm conjI[no_vars]}!
   113 results in @{thm conjI[no_vars]}.
   114 
   115 This \verb!no_vars! business can become a bit tedious.
   116 If you would rather never see question marks, simply put
   117 \begin{verbatim}
   118 reset show_question_marks;
   119 \end{verbatim}
   120 at the beginning of your file \texttt{ROOT.ML}.
   121 The rest of this document is produced with this flag reset.
   122 
   123 Hint: Resetting \verb!show_question_marks! only supresses question
   124 marks; variables that end in digits, e.g. @{text"x1"}, are still
   125 printed with a trailing @{text".0"}, e.g. @{text"x1.0"}, their
   126 internal index. This can be avoided by turning the last digit into a
   127 subscript: write \verb!x\<^isub>1! and obtain the much nicer @{text"x\<^isub>1"}. *}
   128 
   129 (*<*)ML"reset show_question_marks"(*>*)
   130 
   131 subsection {*Variable names\label{sec:varnames}*}
   132 
   133 text{* It sometimes happens that you want to change the name of a
   134 variable in a theorem before printing it. This can easily be achieved
   135 with the help of Isabelle's instantiation attribute \texttt{where}:
   136 @{thm conjI[where P = \<phi> and Q = \<psi>]} is the result of
   137 \begin{quote}
   138 \verb!@!\verb!{thm conjI[where P = \<phi> and Q = \<psi>]}!
   139 \end{quote}
   140 To support the ``\_''-notation for irrelevant variables
   141 the constant \texttt{DUMMY} has been introduced:
   142 @{thm fst_conv[where b = DUMMY]} is produced by
   143 \begin{quote}
   144 \verb!@!\verb!{thm fst_conv[where b = DUMMY]}!
   145 \end{quote}
   146 *}
   147 
   148 subsection "Inference rules"
   149 
   150 text{* To print theorems as inference rules you need to include Didier
   151 R\'emy's \texttt{mathpartir} package~\cite{mathpartir}
   152 for typesetting inference rules in your \LaTeX\ file.
   153 
   154 Writing \verb!@!\verb!{thm[mode=Rule] conjI}! produces
   155 @{thm[mode=Rule] conjI}, even in the middle of a sentence.
   156 If you prefer your inference rule on a separate line, maybe with a name,
   157 \begin{center}
   158 @{thm[mode=Rule] conjI} {\sc conjI}
   159 \end{center}
   160 is produced by
   161 \begin{quote}
   162 \verb!\begin{center}!\\
   163 \verb!@!\verb!{thm[mode=Rule] conjI} {\sc conjI}!\\
   164 \verb!\end{center}!
   165 \end{quote}
   166 It is not recommended to use the standard \texttt{display} attribute
   167 together with \texttt{Rule} because centering does not work and because
   168 the line breaking mechanisms of \texttt{display} and \texttt{mathpartir} can
   169 clash.
   170 
   171 Of course you can display multiple rules in this fashion:
   172 \begin{quote}
   173 \verb!\begin{center}\isastyle!\\
   174 \verb!@!\verb!{thm[mode=Rule] conjI} {\sc conjI} \\[1ex]!\\
   175 \verb!@!\verb!{thm[mode=Rule] conjE} {\sc disjI$_1$} \qquad!\\
   176 \verb!@!\verb!{thm[mode=Rule] disjE} {\sc disjI$_2$}!\\
   177 \verb!\end{center}!
   178 \end{quote}
   179 yields
   180 \begin{center}\isastyle
   181 @{thm[mode=Rule] conjI} {\sc conjI} \\[1ex]
   182 @{thm[mode=Rule] disjI1} {\sc disjI$_1$} \qquad
   183 @{thm[mode=Rule] disjI2} {\sc disjI$_2$}
   184 \end{center}
   185 Note that we included \verb!\isastyle! to obtain
   186 the smaller font that otherwise comes only with \texttt{display}.
   187 
   188 The \texttt{mathpartir} package copes well if there are too many
   189 premises for one line:
   190 \begin{center}
   191 @{prop[mode=Rule] "\<lbrakk> A \<longrightarrow> B; B \<longrightarrow> C; C \<longrightarrow> D; D \<longrightarrow> E; E \<longrightarrow> F; F \<longrightarrow> G;
   192  G \<longrightarrow> H; H \<longrightarrow> I; I \<longrightarrow> J; J \<longrightarrow> K \<rbrakk> \<Longrightarrow> A \<longrightarrow> K"}
   193 \end{center}
   194 
   195 Limitations: 1. Premises and conclusion must each not be longer than
   196 the line.  2. Premises that are @{text"\<Longrightarrow>"}-implications are again
   197 displayed with a horizontal line, which looks at least unusual.
   198 
   199 *}
   200 
   201 subsection{*If-then*}
   202 
   203 text{* If you prefer a fake ``natural language'' style you can produce
   204 the body of
   205 \newtheorem{theorem}{Theorem}
   206 \begin{theorem}
   207 @{thm[mode=IfThen] le_trans}
   208 \end{theorem}
   209 by typing
   210 \begin{quote}
   211 \verb!@!\verb!{thm[mode=IfThen] le_trans}!
   212 \end{quote}
   213 
   214 In order to prevent odd line breaks, the premises are put into boxes.
   215 At times this is too drastic:
   216 \begin{theorem}
   217 @{prop[mode=IfThen] "longpremise \<Longrightarrow> longerpremise \<Longrightarrow> P(f(f(f(f(f(f(f(f(f(x)))))))))) \<Longrightarrow> longestpremise \<Longrightarrow> conclusion"}
   218 \end{theorem}
   219 In which case you should use \texttt{IfThenNoBox} instead of
   220 \texttt{IfThen}:
   221 \begin{theorem}
   222 @{prop[mode=IfThenNoBox] "longpremise \<Longrightarrow> longerpremise \<Longrightarrow> P(f(f(f(f(f(f(f(f(f(x)))))))))) \<Longrightarrow> longestpremise \<Longrightarrow> conclusion"}
   223 \end{theorem}
   224 *}
   225 
   226 subsection{* Doing it yourself\label{sec:yourself}*}
   227 
   228 text{* If for some reason you want or need to present theorems your
   229 own way, you can extract the premises and the conclusion explicitly
   230 and combine them as you like:
   231 \begin{itemize}
   232 \item \verb!@!\verb!{thm_style prem1! $thm$\verb!}!
   233 prints premise 1 of $thm$ (and similarly up to \texttt{prem9}).
   234 \item \verb!@!\verb!{thm_style concl! $thm$\verb!}!
   235 prints the conclusion of $thm$.
   236 \end{itemize}
   237 For example, ``from @{thm_style prem2 conjI} and
   238 @{thm_style prem1 conjI} we conclude @{thm_style concl conjI}''
   239 is produced by
   240 \begin{quote}
   241 \verb!from !\verb!@!\verb!{thm_style prem2 conjI}! \verb!and !\verb!@!\verb!{thm_style prem1 conjI}!\\
   242 \verb!we conclude !\verb!@!\verb!{thm_style concl conjI}!
   243 \end{quote}
   244 Thus you can rearrange or hide premises and typeset the theorem as you like.
   245 The \verb!thm_style! antiquotation is a general mechanism explained
   246 in \S\ref{sec:styles}.
   247 *}
   248 
   249 subsection "Patterns"
   250 
   251 text {*
   252 
   253   In \S\ref{sec:varnames} we shows how to create patterns containing
   254   ``@{term DUMMY}''.
   255   You can drive this game even further and extend the syntax of let
   256   bindings such that certain functions like @{term fst}, @{term hd}, 
   257   etc.\ are printed as patterns. \texttt{OptionalSugar} provides the
   258   following:
   259   
   260   \begin{center}
   261   \begin{tabular}{l@ {~~produced by~~}l}
   262   @{term "let x = fst p in t"} & \verb!@!\verb!{term "let x = fst p in t"}!\\
   263   @{term "let x = snd p in t"} & \verb!@!\verb!{term "let x = snd p in t"}!\\
   264   @{term "let x = hd xs in t"} & \verb!@!\verb!{term "let x = hd xs in t"}!\\
   265   @{term "let x = tl xs in t"} & \verb!@!\verb!{term "let x = tl xs in t"}!\\
   266   @{term "let x = the y in t"} & \verb!@!\verb!{term "let x = the y in t"}!\\
   267   \end{tabular}
   268   \end{center}
   269 *}
   270 
   271 section "Proofs"
   272 
   273 text {*
   274   Full proofs, even if written in beautiful Isar style, are likely to
   275   be too long and detailed to be included in conference papers, but
   276   some key lemmas might be of interest.
   277 
   278   It is usually easiest to put them in figures like the one in Fig.\
   279   \ref{fig:proof}. This was achieved with the \isakeyword{text\_raw}
   280   command:
   281 *}
   282 text_raw {*
   283   \begin{figure}
   284   \begin{center}\begin{minipage}{0.6\textwidth}  
   285   \isastyle\isamarkuptrue
   286 *}
   287 lemma True
   288 proof -
   289   -- "pretty trivial"
   290   show True by force
   291 qed
   292 text_raw {*    
   293   \end{minipage}\end{center}
   294   \caption{Example proof in a figure.}\label{fig:proof}
   295   \end{figure}
   296 *}
   297 text {*
   298 
   299 \begin{quote}
   300 \small
   301 \verb!text_raw {!\verb!*!\\
   302 \verb!  \begin{figure}!\\
   303 \verb!  \begin{center}\begin{minipage}{0.6\textwidth}!\\
   304 \verb!  \isastyle\isamarkuptrue!\\
   305 \verb!*!\verb!}!\\
   306 \verb!lemma True!\\
   307 \verb!proof -!\\
   308 \verb!  -- "pretty trivial"!\\
   309 \verb!  show True by force!\\
   310 \verb!qed!\\
   311 \verb!text_raw {!\verb!*!\\
   312 \verb!  \end{minipage}\end{center}!\\
   313 \verb!  \caption{Example proof in a figure.}\label{fig:proof}!\\
   314 \verb!  \end{figure}!\\
   315 \verb!*!\verb!}!
   316 \end{quote}
   317   
   318 *}
   319 
   320 section {*Styles\label{sec:styles}*}
   321 
   322 text {*
   323   The \verb!thm! antiquotation works nicely for single theorems, but
   324   sets of equations as used in definitions are more difficult to
   325   typeset nicely: people tend to prefer aligned @{text "="} signs.
   326 
   327   To deal with such cases where it is desirable to dive into the structure
   328   of terms and theorems, Isabelle offers antiquotations featuring
   329   ``styles'':
   330 
   331     \begin{quote}
   332     \verb!@!\verb!{thm_style stylename thm}!\\
   333     \verb!@!\verb!{term_style stylename term}!
   334     \end{quote}
   335 
   336   A ``style'' is a transformation of propositions. There are predefined
   337   styles, namly \verb!lhs! and \verb!rhs!, \verb!prem1! up to \verb!prem9!, and \verb!concl!.
   338   For example, 
   339   the output
   340   \begin{center}
   341   \begin{tabular}{l@ {~~@{text "="}~~}l}
   342   @{thm_style lhs foldl_Nil} & @{thm_style rhs foldl_Nil}\\
   343   @{thm_style lhs foldl_Cons} & @{thm_style rhs foldl_Cons}
   344   \end{tabular}
   345   \end{center}
   346   is produced by the following code:
   347   \begin{quote}
   348     \verb!\begin{center}!\\
   349     \verb!\begin{tabular}{l@ {~~!\verb!@!\verb!{text "="}~~}l}!\\
   350     \verb!@!\verb!{thm_style lhs foldl_Nil} & @!\verb!{thm_style rhs foldl_Nil}!\\
   351     \verb!@!\verb!{thm_style lhs foldl_Cons} & @!\verb!{thm_style rhs foldl_Cons}!\\
   352     \verb!\end{tabular}!\\
   353     \verb!\end{center}!
   354   \end{quote}
   355   Note the space between \verb!@! and \verb!{! in the tabular argument.
   356   It prevents Isabelle from interpreting \verb!@ {~~...~~}! 
   357   as an antiquotation. The styles \verb!lhs! and \verb!rhs!
   358   extract the left hand side (or right hand side respectivly) from the
   359   conclusion of propositions consisting of a binary operator
   360   (e.~g.~@{text "="}, @{text "\<equiv>"}, @{text "<"}).
   361 
   362   Likewise, \verb!concl! may be used as a style to show just the
   363   conclusion of a proposition. For example, take \verb!hd_Cons_tl!:
   364   \begin{center}
   365     @{thm [show_types] hd_Cons_tl}
   366   \end{center}
   367   To print just the conclusion,
   368   \begin{center}
   369     @{thm_style [show_types] concl hd_Cons_tl}
   370   \end{center}
   371   type
   372   \begin{quote}
   373     \verb!\begin{center}!\\
   374     \verb!@!\verb!{thm_style [show_types] concl hd_Cons_tl}!\\
   375     \verb!\end{center}!
   376   \end{quote}
   377   Beware that any options must be placed \emph{before}
   378   the name of the style, as in this example.
   379 
   380   Further use cases can be found in \S\ref{sec:yourself}.
   381 
   382   If you are not afraid of ML, you may also define your own styles.
   383   A style is implemented by an ML function of type
   384   \verb!Proof.context -> term -> term!.
   385   Have a look at the following example:
   386 
   387 *}
   388 (*<*)
   389 setup {*
   390 let
   391   fun my_concl ctxt = Logic.strip_imp_concl
   392   in TermStyle.add_style "my_concl" my_concl
   393 end;
   394 *}
   395 (*>*)
   396 text {*
   397 
   398   \begin{quote}
   399     \verb!setup {!\verb!*!\\
   400     \verb!let!\\
   401     \verb!  fun my_concl ctxt = Logic.strip_imp_concl!\\
   402     \verb!  in TermStyle.add_style "my_concl" my_concl!\\
   403     \verb!end;!\\
   404     \verb!*!\verb!}!\\
   405   \end{quote}
   406 
   407   \noindent
   408   This example shows how the \verb!concl! style is implemented
   409   and may be used as as a ``copy-and-paste'' pattern to write your own styles.
   410 
   411   The code should go into your theory file, separate from the \LaTeX\ text.
   412   The \verb!let! expression avoids polluting the
   413   ML global namespace. Each style receives the current proof context
   414   as first argument; this is helpful in situations where the
   415   style has some object-logic specific behaviour for example.
   416 
   417   The mapping from identifier name to the style function
   418   is done by the @{ML TermStyle.add_style} expression which expects the desired
   419   style name and the style function as arguments.
   420   
   421   After this \verb!setup!,
   422   there will be a new style available named \verb!my_concl!, thus allowing
   423   antiquoations like \verb!@!\verb!{thm_style my_concl hd_Cons_tl}!
   424   yielding @{thm_style my_concl hd_Cons_tl}.
   425 
   426 *}
   427 
   428 (*<*)
   429 end
   430 (*>*)