doc-src/LaTeXsugar/Sugar/Sugar.thy
author wenzelm
Wed Dec 29 17:34:41 2010 +0100 (2010-12-29)
changeset 41413 64cd30d6b0b8
parent 38980 af73cf0dc31f
child 42289 dafae095d733
permissions -rw-r--r--
explicit file specifications -- avoid secondary load path;
     1 (*<*)
     2 theory Sugar
     3 imports "~~/src/HOL/Library/LaTeXsugar" "~~/src/HOL/Library/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"{}"}, where
    75  @{term"{}"} is also input syntax.
    76 \item @{term"insert a (insert b (insert c M))"} instead of @{text"insert a (insert b (insert c M))"}.
    77 \end{itemize}
    78 *}
    79 
    80 subsection{* Lists *}
    81 
    82 text{* If lists are used heavily, the following notations increase readability:
    83 \begin{itemize}
    84 \item @{term"x # xs"} instead of @{text"x # xs"},
    85       where @{term"x # xs"} is also input syntax.
    86 If you prefer more space around the $\cdot$ you have to redefine
    87 \verb!\isasymcdot! in \LaTeX:
    88 \verb!\renewcommand{\isasymcdot}{\isamath{\,\cdot\,}}!
    89 
    90 \item @{term"length xs"} instead of @{text"length xs"}.
    91 \item @{term"nth xs n"} instead of @{text"nth xs n"},
    92       the $n$th element of @{text xs}.
    93 
    94 \item Human readers are good at converting automatically from lists to
    95 sets. Hence \texttt{OptionalSugar} contains syntax for suppressing the
    96 conversion function @{const set}: for example, @{prop[source]"x \<in> set xs"}
    97 becomes @{prop"x \<in> set xs"}.
    98 
    99 \item The @{text"@"} operation associates implicitly to the right,
   100 which leads to unpleasant line breaks if the term is too long for one
   101 line. To avoid this, \texttt{OptionalSugar} contains syntax to group
   102 @{text"@"}-terms to the left before printing, which leads to better
   103 line breaking behaviour:
   104 @{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"}
   105 
   106 \end{itemize}
   107 *}
   108 
   109 subsection{* Numbers *}
   110 
   111 text{* Coercions between numeric types are alien to mathematicians who
   112 consider, for example, @{typ nat} as a subset of @{typ int}.
   113 \texttt{OptionalSugar} contains syntax for suppressing numeric coercions such
   114 as @{const int} @{text"::"} @{typ"nat \<Rightarrow> int"}. For example,
   115 @{term[source]"int 5"} is printed as @{term "int 5"}. Embeddings of types
   116 @{typ nat}, @{typ int}, @{typ real} are covered; non-injective coercions such
   117 as @{const nat} @{text"::"} @{typ"int \<Rightarrow> nat"} are not and should not be
   118 hidden. *}
   119 
   120 section "Printing theorems"
   121 
   122 subsection "Question marks"
   123 
   124 text{* If you print anything, especially theorems, containing
   125 schematic variables they are prefixed with a question mark:
   126 \verb!@!\verb!{thm conjI}! results in @{thm conjI}. Most of the time
   127 you would rather not see the question marks. There is an attribute
   128 \verb!no_vars! that you can attach to the theorem that turns its
   129 schematic into ordinary free variables: \verb!@!\verb!{thm conjI[no_vars]}!
   130 results in @{thm conjI[no_vars]}.
   131 
   132 This \verb!no_vars! business can become a bit tedious.
   133 If you would rather never see question marks, simply put
   134 \begin{quote}
   135 @{ML "show_question_marks_default := false"}\verb!;!
   136 \end{quote}
   137 at the beginning of your file \texttt{ROOT.ML}.
   138 The rest of this document is produced with this flag set to \texttt{false}.
   139 
   140 Hint: Setting \verb!show_question_marks_default! to \texttt{false} only
   141 suppresses question marks; variables that end in digits,
   142 e.g. @{text"x1"}, are still printed with a trailing @{text".0"},
   143 e.g. @{text"x1.0"}, their internal index. This can be avoided by
   144 turning the last digit into a subscript: write \verb!x\<^isub>1! and
   145 obtain the much nicer @{text"x\<^isub>1"}. *}
   146 
   147 (*<*)declare [[show_question_marks = false]](*>*)
   148 
   149 subsection {*Qualified names*}
   150 
   151 text{* If there are multiple declarations of the same name, Isabelle prints
   152 the qualified name, for example @{text "T.length"}, where @{text T} is the
   153 theory it is defined in, to distinguish it from the predefined @{const[source]
   154 "List.length"}. In case there is no danger of confusion, you can insist on
   155 short names (no qualifiers) by setting \verb!short_names!, typically
   156 in \texttt{ROOT.ML}:
   157 \begin{quote}
   158 @{ML "short_names := true"}\verb!;!
   159 \end{quote}
   160 *}
   161 
   162 subsection {*Variable names\label{sec:varnames}*}
   163 
   164 text{* It sometimes happens that you want to change the name of a
   165 variable in a theorem before printing it. This can easily be achieved
   166 with the help of Isabelle's instantiation attribute \texttt{where}:
   167 @{thm conjI[where P = \<phi> and Q = \<psi>]} is the result of
   168 \begin{quote}
   169 \verb!@!\verb!{thm conjI[where P = \<phi> and Q = \<psi>]}!
   170 \end{quote}
   171 To support the ``\_''-notation for irrelevant variables
   172 the constant \texttt{DUMMY} has been introduced:
   173 @{thm fst_conv[where b = DUMMY]} is produced by
   174 \begin{quote}
   175 \verb!@!\verb!{thm fst_conv[where b = DUMMY]}!
   176 \end{quote}
   177 Variables that are bound by quantifiers or lambdas cannot be renamed
   178 like this. Instead, the attribute \texttt{rename\_abs} does the
   179 job. It expects a list of names or underscores, similar to the
   180 \texttt{of} attribute:
   181 \begin{quote}
   182 \verb!@!\verb!{thm split_paired_All[rename_abs _ l r]}!
   183 \end{quote}
   184 produces @{thm split_paired_All[rename_abs _ l r]}.
   185 *}
   186 
   187 subsection "Inference rules"
   188 
   189 text{* To print theorems as inference rules you need to include Didier
   190 R\'emy's \texttt{mathpartir} package~\cite{mathpartir}
   191 for typesetting inference rules in your \LaTeX\ file.
   192 
   193 Writing \verb!@!\verb!{thm[mode=Rule] conjI}! produces
   194 @{thm[mode=Rule] conjI}, even in the middle of a sentence.
   195 If you prefer your inference rule on a separate line, maybe with a name,
   196 \begin{center}
   197 @{thm[mode=Rule] conjI} {\sc conjI}
   198 \end{center}
   199 is produced by
   200 \begin{quote}
   201 \verb!\begin{center}!\\
   202 \verb!@!\verb!{thm[mode=Rule] conjI} {\sc conjI}!\\
   203 \verb!\end{center}!
   204 \end{quote}
   205 It is not recommended to use the standard \texttt{display} option
   206 together with \texttt{Rule} because centering does not work and because
   207 the line breaking mechanisms of \texttt{display} and \texttt{mathpartir} can
   208 clash.
   209 
   210 Of course you can display multiple rules in this fashion:
   211 \begin{quote}
   212 \verb!\begin{center}!\\
   213 \verb!@!\verb!{thm[mode=Rule] conjI} {\sc conjI} \\[1ex]!\\
   214 \verb!@!\verb!{thm[mode=Rule] conjE} {\sc disjI$_1$} \qquad!\\
   215 \verb!@!\verb!{thm[mode=Rule] disjE} {\sc disjI$_2$}!\\
   216 \verb!\end{center}!
   217 \end{quote}
   218 yields
   219 \begin{center}\small
   220 @{thm[mode=Rule] conjI} {\sc conjI} \\[1ex]
   221 @{thm[mode=Rule] disjI1} {\sc disjI$_1$} \qquad
   222 @{thm[mode=Rule] disjI2} {\sc disjI$_2$}
   223 \end{center}
   224 
   225 The \texttt{mathpartir} package copes well if there are too many
   226 premises for one line:
   227 \begin{center}
   228 @{prop[mode=Rule] "\<lbrakk> A \<longrightarrow> B; B \<longrightarrow> C; C \<longrightarrow> D; D \<longrightarrow> E; E \<longrightarrow> F; F \<longrightarrow> G;
   229  G \<longrightarrow> H; H \<longrightarrow> I; I \<longrightarrow> J; J \<longrightarrow> K \<rbrakk> \<Longrightarrow> A \<longrightarrow> K"}
   230 \end{center}
   231 
   232 Limitations: 1. Premises and conclusion must each not be longer than
   233 the line.  2. Premises that are @{text"\<Longrightarrow>"}-implications are again
   234 displayed with a horizontal line, which looks at least unusual.
   235 
   236 
   237 In case you print theorems without premises no rule will be printed by the
   238 \texttt{Rule} print mode. However, you can use \texttt{Axiom} instead:
   239 \begin{quote}
   240 \verb!\begin{center}!\\
   241 \verb!@!\verb!{thm[mode=Axiom] refl} {\sc refl}! \\
   242 \verb!\end{center}!
   243 \end{quote}
   244 yields
   245 \begin{center}
   246 @{thm[mode=Axiom] refl} {\sc refl} 
   247 \end{center}
   248 *}
   249 
   250 subsection "Displays and font sizes"
   251 
   252 text{* When displaying theorems with the \texttt{display} option, e.g.
   253 \verb!@!\verb!{thm[display] refl}! @{thm[display] refl} the theorem is
   254 set in small font. It uses the \LaTeX-macro \verb!\isastyle!,
   255 which is also the style that regular theory text is set in, e.g. *}
   256 
   257 lemma "t = t"
   258 (*<*)oops(*>*)
   259 
   260 text{* \noindent Otherwise \verb!\isastyleminor! is used,
   261 which does not modify the font size (assuming you stick to the default
   262 \verb!\isabellestyle{it}! in \texttt{root.tex}). If you prefer
   263 normal font size throughout your text, include
   264 \begin{quote}
   265 \verb!\renewcommand{\isastyle}{\isastyleminor}!
   266 \end{quote}
   267 in \texttt{root.tex}. On the other hand, if you like the small font,
   268 just put \verb!\isastyle! in front of the text in question,
   269 e.g.\ at the start of one of the center-environments above.
   270 
   271 The advantage of the display option is that you can display a whole
   272 list of theorems in one go. For example,
   273 \verb!@!\verb!{thm[display] foldl.simps}!
   274 generates @{thm[display] foldl.simps}
   275 *}
   276 
   277 subsection "If-then"
   278 
   279 text{* If you prefer a fake ``natural language'' style you can produce
   280 the body of
   281 \newtheorem{theorem}{Theorem}
   282 \begin{theorem}
   283 @{thm[mode=IfThen] le_trans}
   284 \end{theorem}
   285 by typing
   286 \begin{quote}
   287 \verb!@!\verb!{thm[mode=IfThen] le_trans}!
   288 \end{quote}
   289 
   290 In order to prevent odd line breaks, the premises are put into boxes.
   291 At times this is too drastic:
   292 \begin{theorem}
   293 @{prop[mode=IfThen] "longpremise \<Longrightarrow> longerpremise \<Longrightarrow> P(f(f(f(f(f(f(f(f(f(x)))))))))) \<Longrightarrow> longestpremise \<Longrightarrow> conclusion"}
   294 \end{theorem}
   295 In which case you should use \texttt{IfThenNoBox} instead of
   296 \texttt{IfThen}:
   297 \begin{theorem}
   298 @{prop[mode=IfThenNoBox] "longpremise \<Longrightarrow> longerpremise \<Longrightarrow> P(f(f(f(f(f(f(f(f(f(x)))))))))) \<Longrightarrow> longestpremise \<Longrightarrow> conclusion"}
   299 \end{theorem}
   300 *}
   301 
   302 subsection{* Doing it yourself\label{sec:yourself}*}
   303 
   304 text{* If for some reason you want or need to present theorems your
   305 own way, you can extract the premises and the conclusion explicitly
   306 and combine them as you like:
   307 \begin{itemize}
   308 \item \verb!@!\verb!{thm (prem 1)! $thm$\verb!}!
   309 prints premise 1 of $thm$.
   310 \item \verb!@!\verb!{thm (concl)! $thm$\verb!}!
   311 prints the conclusion of $thm$.
   312 \end{itemize}
   313 For example, ``from @{thm (prem 2) conjI} and
   314 @{thm (prem 1) conjI} we conclude @{thm (concl) conjI}''
   315 is produced by
   316 \begin{quote}
   317 \verb!from !\verb!@!\verb!{thm (prem 2) conjI}! \verb!and !\verb!@!\verb!{thm (prem 1) conjI}!\\
   318 \verb!we conclude !\verb!@!\verb!{thm (concl) conjI}!
   319 \end{quote}
   320 Thus you can rearrange or hide premises and typeset the theorem as you like.
   321 Styles like \verb!(prem 1)! are a general mechanism explained
   322 in \S\ref{sec:styles}.
   323 *}
   324 
   325 subsection "Patterns"
   326 
   327 text {*
   328 
   329   In \S\ref{sec:varnames} we shows how to create patterns containing
   330   ``@{term DUMMY}''.
   331   You can drive this game even further and extend the syntax of let
   332   bindings such that certain functions like @{term fst}, @{term hd}, 
   333   etc.\ are printed as patterns. \texttt{OptionalSugar} provides the
   334   following:
   335   
   336   \begin{center}
   337   \begin{tabular}{l@ {~~produced by~~}l}
   338   @{term "let x = fst p in t"} & \verb!@!\verb!{term "let x = fst p in t"}!\\
   339   @{term "let x = snd p in t"} & \verb!@!\verb!{term "let x = snd p in t"}!\\
   340   @{term "let x = hd xs in t"} & \verb!@!\verb!{term "let x = hd xs in t"}!\\
   341   @{term "let x = tl xs in t"} & \verb!@!\verb!{term "let x = tl xs in t"}!\\
   342   @{term "let x = the y in t"} & \verb!@!\verb!{term "let x = the y in t"}!\\
   343   \end{tabular}
   344   \end{center}
   345 *}
   346 
   347 section "Proofs"
   348 
   349 text {* Full proofs, even if written in beautiful Isar style, are
   350 likely to be too long and detailed to be included in conference
   351 papers, but some key lemmas might be of interest.
   352 It is usually easiest to put them in figures like the one in Fig.\
   353 \ref{fig:proof}. This was achieved with the \isakeyword{text\_raw} command:
   354 *}
   355 text_raw {*
   356   \begin{figure}
   357   \begin{center}\begin{minipage}{0.6\textwidth}  
   358   \isastyleminor\isamarkuptrue
   359 *}
   360 lemma True
   361 proof -
   362   -- "pretty trivial"
   363   show True by force
   364 qed
   365 text_raw {*    
   366   \end{minipage}\end{center}
   367   \caption{Example proof in a figure.}\label{fig:proof}
   368   \end{figure}
   369 *}
   370 text {*
   371 
   372 \begin{quote}
   373 \small
   374 \verb!text_raw {!\verb!*!\\
   375 \verb!  \begin{figure}!\\
   376 \verb!  \begin{center}\begin{minipage}{0.6\textwidth}!\\
   377 \verb!  \isastyleminor\isamarkuptrue!\\
   378 \verb!*!\verb!}!\\
   379 \verb!lemma True!\\
   380 \verb!proof -!\\
   381 \verb!  -- "pretty trivial"!\\
   382 \verb!  show True by force!\\
   383 \verb!qed!\\
   384 \verb!text_raw {!\verb!*!\\
   385 \verb!  \end{minipage}\end{center}!\\
   386 \verb!  \caption{Example proof in a figure.}\label{fig:proof}!\\
   387 \verb!  \end{figure}!\\
   388 \verb!*!\verb!}!
   389 \end{quote}
   390 
   391 Other theory text, e.g.\ definitions, can be put in figures, too.
   392 *}
   393 
   394 section {*Styles\label{sec:styles}*}
   395 
   396 text {*
   397   The \verb!thm! antiquotation works nicely for single theorems, but
   398   sets of equations as used in definitions are more difficult to
   399   typeset nicely: people tend to prefer aligned @{text "="} signs.
   400 
   401   To deal with such cases where it is desirable to dive into the structure
   402   of terms and theorems, Isabelle offers antiquotations featuring
   403   ``styles'':
   404 
   405     \begin{quote}
   406     \verb!@!\verb!{thm (style) thm}!\\
   407     \verb!@!\verb!{prop (style) thm}!\\
   408     \verb!@!\verb!{term (style) term}!\\
   409     \verb!@!\verb!{term_type (style) term}!\\
   410     \verb!@!\verb!{typeof (style) term}!\\
   411     \end{quote}
   412 
   413   A ``style'' is a transformation of a term. There are predefined
   414   styles, namely \verb!lhs! and \verb!rhs!, \verb!prem! with one argument, and \verb!concl!.
   415   For example, 
   416   the output
   417   \begin{center}
   418   \begin{tabular}{l@ {~~@{text "="}~~}l}
   419   @{thm (lhs) foldl_Nil} & @{thm (rhs) foldl_Nil}\\
   420   @{thm (lhs) foldl_Cons} & @{thm (rhs) foldl_Cons}
   421   \end{tabular}
   422   \end{center}
   423   is produced by the following code:
   424   \begin{quote}
   425     \verb!\begin{center}!\\
   426     \verb!\begin{tabular}{l@ {~~!\verb!@!\verb!{text "="}~~}l}!\\
   427     \verb!@!\verb!{thm (lhs) foldl_Nil} & @!\verb!{thm (rhs) foldl_Nil}\\!\\
   428     \verb!@!\verb!{thm (lhs) foldl_Cons} & @!\verb!{thm (rhs) foldl_Cons}!\\
   429     \verb!\end{tabular}!\\
   430     \verb!\end{center}!
   431   \end{quote}
   432   Note the space between \verb!@! and \verb!{! in the tabular argument.
   433   It prevents Isabelle from interpreting \verb!@ {~~...~~}! 
   434   as an antiquotation. The styles \verb!lhs! and \verb!rhs!
   435   extract the left hand side (or right hand side respectively) from the
   436   conclusion of propositions consisting of a binary operator
   437   (e.~g.~@{text "="}, @{text "\<equiv>"}, @{text "<"}).
   438 
   439   Likewise, \verb!concl! may be used as a style to show just the
   440   conclusion of a proposition. For example, take \verb!hd_Cons_tl!:
   441   \begin{center}
   442     @{thm hd_Cons_tl}
   443   \end{center}
   444   To print just the conclusion,
   445   \begin{center}
   446     @{thm (concl) hd_Cons_tl}
   447   \end{center}
   448   type
   449   \begin{quote}
   450     \verb!\begin{center}!\\
   451     \verb!@!\verb!{thm (concl) hd_Cons_tl}!\\
   452     \verb!\end{center}!
   453   \end{quote}
   454   Beware that any options must be placed \emph{before}
   455   the style, as in this example.
   456 
   457   Further use cases can be found in \S\ref{sec:yourself}.
   458   If you are not afraid of ML, you may also define your own styles.
   459   Have a look at module @{ML_struct Term_Style}.
   460 *}
   461 
   462 (*<*)
   463 end
   464 (*>*)