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 (*>*)