doc-src/LaTeXsugar/Sugar/Sugar.thy
author wenzelm
Wed Jul 25 12:38:54 2012 +0200 (2012-07-25)
changeset 48497 ba61aceaa18a
parent 46187 f009e0fe8643
permissions -rw-r--r--
some updates on "Building a repository version of Isabelle";
     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 "Printer.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 @{ML Printer.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 the \verb!names_short!
   156 configuration option in the context.
   157 *}
   158 
   159 subsection {*Variable names\label{sec:varnames}*}
   160 
   161 text{* It sometimes happens that you want to change the name of a
   162 variable in a theorem before printing it. This can easily be achieved
   163 with the help of Isabelle's instantiation attribute \texttt{where}:
   164 @{thm conjI[where P = \<phi> and Q = \<psi>]} is the result of
   165 \begin{quote}
   166 \verb!@!\verb!{thm conjI[where P = \<phi> and Q = \<psi>]}!
   167 \end{quote}
   168 To support the ``\_''-notation for irrelevant variables
   169 the constant \texttt{DUMMY} has been introduced:
   170 @{thm fst_conv[where b = DUMMY]} is produced by
   171 \begin{quote}
   172 \verb!@!\verb!{thm fst_conv[where b = DUMMY]}!
   173 \end{quote}
   174 Variables that are bound by quantifiers or lambdas cannot be renamed
   175 like this. Instead, the attribute \texttt{rename\_abs} does the
   176 job. It expects a list of names or underscores, similar to the
   177 \texttt{of} attribute:
   178 \begin{quote}
   179 \verb!@!\verb!{thm split_paired_All[rename_abs _ l r]}!
   180 \end{quote}
   181 produces @{thm split_paired_All[rename_abs _ l r]}.
   182 *}
   183 
   184 subsection "Inference rules"
   185 
   186 text{* To print theorems as inference rules you need to include Didier
   187 R\'emy's \texttt{mathpartir} package~\cite{mathpartir}
   188 for typesetting inference rules in your \LaTeX\ file.
   189 
   190 Writing \verb!@!\verb!{thm[mode=Rule] conjI}! produces
   191 @{thm[mode=Rule] conjI}, even in the middle of a sentence.
   192 If you prefer your inference rule on a separate line, maybe with a name,
   193 \begin{center}
   194 @{thm[mode=Rule] conjI} {\sc conjI}
   195 \end{center}
   196 is produced by
   197 \begin{quote}
   198 \verb!\begin{center}!\\
   199 \verb!@!\verb!{thm[mode=Rule] conjI} {\sc conjI}!\\
   200 \verb!\end{center}!
   201 \end{quote}
   202 It is not recommended to use the standard \texttt{display} option
   203 together with \texttt{Rule} because centering does not work and because
   204 the line breaking mechanisms of \texttt{display} and \texttt{mathpartir} can
   205 clash.
   206 
   207 Of course you can display multiple rules in this fashion:
   208 \begin{quote}
   209 \verb!\begin{center}!\\
   210 \verb!@!\verb!{thm[mode=Rule] conjI} {\sc conjI} \\[1ex]!\\
   211 \verb!@!\verb!{thm[mode=Rule] conjE} {\sc disjI$_1$} \qquad!\\
   212 \verb!@!\verb!{thm[mode=Rule] disjE} {\sc disjI$_2$}!\\
   213 \verb!\end{center}!
   214 \end{quote}
   215 yields
   216 \begin{center}\small
   217 @{thm[mode=Rule] conjI} {\sc conjI} \\[1ex]
   218 @{thm[mode=Rule] disjI1} {\sc disjI$_1$} \qquad
   219 @{thm[mode=Rule] disjI2} {\sc disjI$_2$}
   220 \end{center}
   221 
   222 The \texttt{mathpartir} package copes well if there are too many
   223 premises for one line:
   224 \begin{center}
   225 @{prop[mode=Rule] "\<lbrakk> A \<longrightarrow> B; B \<longrightarrow> C; C \<longrightarrow> D; D \<longrightarrow> E; E \<longrightarrow> F; F \<longrightarrow> G;
   226  G \<longrightarrow> H; H \<longrightarrow> I; I \<longrightarrow> J; J \<longrightarrow> K \<rbrakk> \<Longrightarrow> A \<longrightarrow> K"}
   227 \end{center}
   228 
   229 Limitations: 1. Premises and conclusion must each not be longer than
   230 the line.  2. Premises that are @{text"\<Longrightarrow>"}-implications are again
   231 displayed with a horizontal line, which looks at least unusual.
   232 
   233 
   234 In case you print theorems without premises no rule will be printed by the
   235 \texttt{Rule} print mode. However, you can use \texttt{Axiom} instead:
   236 \begin{quote}
   237 \verb!\begin{center}!\\
   238 \verb!@!\verb!{thm[mode=Axiom] refl} {\sc refl}! \\
   239 \verb!\end{center}!
   240 \end{quote}
   241 yields
   242 \begin{center}
   243 @{thm[mode=Axiom] refl} {\sc refl} 
   244 \end{center}
   245 *}
   246 
   247 subsection "Displays and font sizes"
   248 
   249 text{* When displaying theorems with the \texttt{display} option, e.g.
   250 \verb!@!\verb!{thm[display] refl}! @{thm[display] refl} the theorem is
   251 set in small font. It uses the \LaTeX-macro \verb!\isastyle!,
   252 which is also the style that regular theory text is set in, e.g. *}
   253 
   254 lemma "t = t"
   255 (*<*)oops(*>*)
   256 
   257 text{* \noindent Otherwise \verb!\isastyleminor! is used,
   258 which does not modify the font size (assuming you stick to the default
   259 \verb!\isabellestyle{it}! in \texttt{root.tex}). If you prefer
   260 normal font size throughout your text, include
   261 \begin{quote}
   262 \verb!\renewcommand{\isastyle}{\isastyleminor}!
   263 \end{quote}
   264 in \texttt{root.tex}. On the other hand, if you like the small font,
   265 just put \verb!\isastyle! in front of the text in question,
   266 e.g.\ at the start of one of the center-environments above.
   267 
   268 The advantage of the display option is that you can display a whole
   269 list of theorems in one go. For example,
   270 \verb!@!\verb!{thm[display] append.simps}!
   271 generates @{thm[display] append.simps}
   272 *}
   273 
   274 subsection "If-then"
   275 
   276 text{* If you prefer a fake ``natural language'' style you can produce
   277 the body of
   278 \newtheorem{theorem}{Theorem}
   279 \begin{theorem}
   280 @{thm[mode=IfThen] le_trans}
   281 \end{theorem}
   282 by typing
   283 \begin{quote}
   284 \verb!@!\verb!{thm[mode=IfThen] le_trans}!
   285 \end{quote}
   286 
   287 In order to prevent odd line breaks, the premises are put into boxes.
   288 At times this is too drastic:
   289 \begin{theorem}
   290 @{prop[mode=IfThen] "longpremise \<Longrightarrow> longerpremise \<Longrightarrow> P(f(f(f(f(f(f(f(f(f(x)))))))))) \<Longrightarrow> longestpremise \<Longrightarrow> conclusion"}
   291 \end{theorem}
   292 In which case you should use \texttt{IfThenNoBox} instead of
   293 \texttt{IfThen}:
   294 \begin{theorem}
   295 @{prop[mode=IfThenNoBox] "longpremise \<Longrightarrow> longerpremise \<Longrightarrow> P(f(f(f(f(f(f(f(f(f(x)))))))))) \<Longrightarrow> longestpremise \<Longrightarrow> conclusion"}
   296 \end{theorem}
   297 *}
   298 
   299 subsection{* Doing it yourself\label{sec:yourself}*}
   300 
   301 text{* If for some reason you want or need to present theorems your
   302 own way, you can extract the premises and the conclusion explicitly
   303 and combine them as you like:
   304 \begin{itemize}
   305 \item \verb!@!\verb!{thm (prem 1)! $thm$\verb!}!
   306 prints premise 1 of $thm$.
   307 \item \verb!@!\verb!{thm (concl)! $thm$\verb!}!
   308 prints the conclusion of $thm$.
   309 \end{itemize}
   310 For example, ``from @{thm (prem 2) conjI} and
   311 @{thm (prem 1) conjI} we conclude @{thm (concl) conjI}''
   312 is produced by
   313 \begin{quote}
   314 \verb!from !\verb!@!\verb!{thm (prem 2) conjI}! \verb!and !\verb!@!\verb!{thm (prem 1) conjI}!\\
   315 \verb!we conclude !\verb!@!\verb!{thm (concl) conjI}!
   316 \end{quote}
   317 Thus you can rearrange or hide premises and typeset the theorem as you like.
   318 Styles like \verb!(prem 1)! are a general mechanism explained
   319 in \S\ref{sec:styles}.
   320 *}
   321 
   322 subsection "Patterns"
   323 
   324 text {*
   325 
   326   In \S\ref{sec:varnames} we shows how to create patterns containing
   327   ``@{term DUMMY}''.
   328   You can drive this game even further and extend the syntax of let
   329   bindings such that certain functions like @{term fst}, @{term hd}, 
   330   etc.\ are printed as patterns. \texttt{OptionalSugar} provides the
   331   following:
   332   
   333   \begin{center}
   334   \begin{tabular}{l@ {~~produced by~~}l}
   335   @{term "let x = fst p in t"} & \verb!@!\verb!{term "let x = fst p in t"}!\\
   336   @{term "let x = snd p in t"} & \verb!@!\verb!{term "let x = snd p in t"}!\\
   337   @{term "let x = hd xs in t"} & \verb!@!\verb!{term "let x = hd xs in t"}!\\
   338   @{term "let x = tl xs in t"} & \verb!@!\verb!{term "let x = tl xs in t"}!\\
   339   @{term "let x = the y in t"} & \verb!@!\verb!{term "let x = the y in t"}!\\
   340   \end{tabular}
   341   \end{center}
   342 *}
   343 
   344 section "Proofs"
   345 
   346 text {* Full proofs, even if written in beautiful Isar style, are
   347 likely to be too long and detailed to be included in conference
   348 papers, but some key lemmas might be of interest.
   349 It is usually easiest to put them in figures like the one in Fig.\
   350 \ref{fig:proof}. This was achieved with the \isakeyword{text\_raw} command:
   351 *}
   352 text_raw {*
   353   \begin{figure}
   354   \begin{center}\begin{minipage}{0.6\textwidth}  
   355   \isastyleminor\isamarkuptrue
   356 *}
   357 lemma True
   358 proof -
   359   -- "pretty trivial"
   360   show True by force
   361 qed
   362 text_raw {*    
   363   \end{minipage}\end{center}
   364   \caption{Example proof in a figure.}\label{fig:proof}
   365   \end{figure}
   366 *}
   367 text {*
   368 
   369 \begin{quote}
   370 \small
   371 \verb!text_raw {!\verb!*!\\
   372 \verb!  \begin{figure}!\\
   373 \verb!  \begin{center}\begin{minipage}{0.6\textwidth}!\\
   374 \verb!  \isastyleminor\isamarkuptrue!\\
   375 \verb!*!\verb!}!\\
   376 \verb!lemma True!\\
   377 \verb!proof -!\\
   378 \verb!  -- "pretty trivial"!\\
   379 \verb!  show True by force!\\
   380 \verb!qed!\\
   381 \verb!text_raw {!\verb!*!\\
   382 \verb!  \end{minipage}\end{center}!\\
   383 \verb!  \caption{Example proof in a figure.}\label{fig:proof}!\\
   384 \verb!  \end{figure}!\\
   385 \verb!*!\verb!}!
   386 \end{quote}
   387 
   388 Other theory text, e.g.\ definitions, can be put in figures, too.
   389 *}
   390 
   391 section {*Styles\label{sec:styles}*}
   392 
   393 text {*
   394   The \verb!thm! antiquotation works nicely for single theorems, but
   395   sets of equations as used in definitions are more difficult to
   396   typeset nicely: people tend to prefer aligned @{text "="} signs.
   397 
   398   To deal with such cases where it is desirable to dive into the structure
   399   of terms and theorems, Isabelle offers antiquotations featuring
   400   ``styles'':
   401 
   402     \begin{quote}
   403     \verb!@!\verb!{thm (style) thm}!\\
   404     \verb!@!\verb!{prop (style) thm}!\\
   405     \verb!@!\verb!{term (style) term}!\\
   406     \verb!@!\verb!{term_type (style) term}!\\
   407     \verb!@!\verb!{typeof (style) term}!\\
   408     \end{quote}
   409 
   410   A ``style'' is a transformation of a term. There are predefined
   411   styles, namely \verb!lhs! and \verb!rhs!, \verb!prem! with one argument, and \verb!concl!.
   412   For example, 
   413   the output
   414   \begin{center}
   415   \begin{tabular}{l@ {~~@{text "="}~~}l}
   416   @{thm (lhs) append_Nil} & @{thm (rhs) append_Nil}\\
   417   @{thm (lhs) append_Cons} & @{thm (rhs) append_Cons}
   418   \end{tabular}
   419   \end{center}
   420   is produced by the following code:
   421   \begin{quote}
   422     \verb!\begin{center}!\\
   423     \verb!\begin{tabular}{l@ {~~!\verb!@!\verb!{text "="}~~}l}!\\
   424     \verb!@!\verb!{thm (lhs) append_Nil} & @!\verb!{thm (rhs) append_Nil}\\!\\
   425     \verb!@!\verb!{thm (lhs) append_Cons} & @!\verb!{thm (rhs) append_Cons}!\\
   426     \verb!\end{tabular}!\\
   427     \verb!\end{center}!
   428   \end{quote}
   429   Note the space between \verb!@! and \verb!{! in the tabular argument.
   430   It prevents Isabelle from interpreting \verb!@ {~~...~~}! 
   431   as an antiquotation. The styles \verb!lhs! and \verb!rhs!
   432   extract the left hand side (or right hand side respectively) from the
   433   conclusion of propositions consisting of a binary operator
   434   (e.~g.~@{text "="}, @{text "\<equiv>"}, @{text "<"}).
   435 
   436   Likewise, \verb!concl! may be used as a style to show just the
   437   conclusion of a proposition. For example, take \verb!hd_Cons_tl!:
   438   \begin{center}
   439     @{thm hd_Cons_tl}
   440   \end{center}
   441   To print just the conclusion,
   442   \begin{center}
   443     @{thm (concl) hd_Cons_tl}
   444   \end{center}
   445   type
   446   \begin{quote}
   447     \verb!\begin{center}!\\
   448     \verb!@!\verb!{thm (concl) hd_Cons_tl}!\\
   449     \verb!\end{center}!
   450   \end{quote}
   451   Beware that any options must be placed \emph{before}
   452   the style, as in this example.
   453 
   454   Further use cases can be found in \S\ref{sec:yourself}.
   455   If you are not afraid of ML, you may also define your own styles.
   456   Have a look at module @{ML_struct Term_Style}.
   457 *}
   458 
   459 (*<*)
   460 end
   461 (*>*)