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