--- a/src/Doc/LaTeXsugar/Sugar.thy Sun Sep 09 21:22:31 2012 +0200
+++ b/src/Doc/LaTeXsugar/Sugar.thy Mon Sep 10 06:46:17 2012 +0200
@@ -3,10 +3,10 @@
imports "~~/src/HOL/Library/LaTeXsugar" "~~/src/HOL/Library/OptionalSugar"
begin
(*>*)
+text{*
+\section{Introduction}
-section "Introduction"
-
-text{* This document is for those Isabelle users who have mastered
+This document is for those Isabelle users who have mastered
the art of mixing \LaTeX\ text and Isabelle theories and never want to
typeset a theorem by hand anymore because they have experienced the
bliss of writing \verb!@!\verb!{thm[display]setsum_cartesian_product[no_vars]}!
@@ -45,14 +45,13 @@
@{prop[source]"\<not>(\<exists>x. P x)"} will fail because the AMS symbol
@{text"\<nexists>"} is missing.
\end{itemize}
-*}
+
-section{* HOL syntax*}
+\section{HOL syntax}
-subsection{* Logic *}
+\subsection{Logic}
-text{*
- The formula @{prop[source]"\<not>(\<exists>x. P x)"} is typeset as @{prop"~(EX x. P x)"}.
+The formula @{prop[source]"\<not>(\<exists>x. P x)"} is typeset as @{prop"~(EX x. P x)"}.
The predefined constructs @{text"if"}, @{text"let"} and
@{text"case"} are set in sans serif font to distinguish them from
@@ -63,11 +62,10 @@
\item @{term"case x of True \<Rightarrow> e\<^isub>1 | False \<Rightarrow> e\<^isub>2"} instead of\\
@{text"case x of True \<Rightarrow> e\<^isub>1 | False \<Rightarrow> e\<^isub>2"}.
\end{itemize}
-*}
-subsection{* Sets *}
+\subsection{Sets}
-text{* Although set syntax in HOL is already close to
+Although set syntax in HOL is already close to
standard, we provide a few further improvements:
\begin{itemize}
\item @{term"{x. P}"} instead of @{text"{x. P}"}.
@@ -75,11 +73,11 @@
@{term"{}"} is also input syntax.
\item @{term"insert a (insert b (insert c M))"} instead of @{text"insert a (insert b (insert c M))"}.
\end{itemize}
-*}
+
-subsection{* Lists *}
+\subsection{Lists}
-text{* If lists are used heavily, the following notations increase readability:
+If lists are used heavily, the following notations increase readability:
\begin{itemize}
\item @{term"x # xs"} instead of @{text"x # xs"},
where @{term"x # xs"} is also input syntax.
@@ -104,24 +102,25 @@
@{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"}
\end{itemize}
-*}
+
-subsection{* Numbers *}
+\subsection{Numbers}
-text{* Coercions between numeric types are alien to mathematicians who
+Coercions between numeric types are alien to mathematicians who
consider, for example, @{typ nat} as a subset of @{typ int}.
\texttt{OptionalSugar} contains syntax for suppressing numeric coercions such
as @{const int} @{text"::"} @{typ"nat \<Rightarrow> int"}. For example,
@{term[source]"int 5"} is printed as @{term "int 5"}. Embeddings of types
@{typ nat}, @{typ int}, @{typ real} are covered; non-injective coercions such
as @{const nat} @{text"::"} @{typ"int \<Rightarrow> nat"} are not and should not be
-hidden. *}
+hidden.
-section "Printing theorems"
-subsection "Question marks"
+\section{Printing theorems}
-text{* If you print anything, especially theorems, containing
+\subsection{Question marks}
+
+If you print anything, especially theorems, containing
schematic variables they are prefixed with a question mark:
\verb!@!\verb!{thm conjI}! results in @{thm conjI}. Most of the time
you would rather not see the question marks. There is an attribute
@@ -132,12 +131,12 @@
This \verb!no_vars! business can become a bit tedious.
If you would rather never see question marks, simply put
\begin{quote}
-@{ML "Printer.show_question_marks_default := false"}\verb!;!
+\verb!options [show_question_marks = false]!
\end{quote}
-at the beginning of your file \texttt{ROOT.ML}.
+into the relevant \texttt{ROOT} file, just before the \texttt{theories} for that session.
The rest of this document is produced with this flag set to \texttt{false}.
-Hint: Setting @{ML Printer.show_question_marks_default} to \texttt{false} only
+Hint: Setting \verb!show_question_marks! to \texttt{false} only
suppresses question marks; variables that end in digits,
e.g. @{text"x1"}, are still printed with a trailing @{text".0"},
e.g. @{text"x1.0"}, their internal index. This can be avoided by
@@ -154,11 +153,11 @@
"List.length"}. In case there is no danger of confusion, you can insist on
short names (no qualifiers) by setting the \verb!names_short!
configuration option in the context.
-*}
+
-subsection {*Variable names\label{sec:varnames}*}
+\subsection {Variable names\label{sec:varnames}}
-text{* It sometimes happens that you want to change the name of a
+It sometimes happens that you want to change the name of a
variable in a theorem before printing it. This can easily be achieved
with the help of Isabelle's instantiation attribute \texttt{where}:
@{thm conjI[where P = \<phi> and Q = \<psi>]} is the result of
@@ -179,11 +178,11 @@
\verb!@!\verb!{thm split_paired_All[rename_abs _ l r]}!
\end{quote}
produces @{thm split_paired_All[rename_abs _ l r]}.
-*}
+
-subsection "Inference rules"
+\subsection{Inference rules}
-text{* To print theorems as inference rules you need to include Didier
+To print theorems as inference rules you need to include Didier
R\'emy's \texttt{mathpartir} package~\cite{mathpartir}
for typesetting inference rules in your \LaTeX\ file.
@@ -242,11 +241,11 @@
\begin{center}
@{thm[mode=Axiom] refl} {\sc refl}
\end{center}
-*}
+
-subsection "Displays and font sizes"
+\subsection{Displays and font sizes}
-text{* When displaying theorems with the \texttt{display} option, e.g.
+When displaying theorems with the \texttt{display} option, for example as in
\verb!@!\verb!{thm[display] refl}! @{thm[display] refl} the theorem is
set in small font. It uses the \LaTeX-macro \verb!\isastyle!,
which is also the style that regular theory text is set in, e.g. *}
@@ -269,11 +268,11 @@
list of theorems in one go. For example,
\verb!@!\verb!{thm[display] append.simps}!
generates @{thm[display] append.simps}
-*}
+
-subsection "If-then"
+\subsection{If-then}
-text{* If you prefer a fake ``natural language'' style you can produce
+If you prefer a fake ``natural language'' style you can produce
the body of
\newtheorem{theorem}{Theorem}
\begin{theorem}
@@ -294,11 +293,11 @@
\begin{theorem}
@{prop[mode=IfThenNoBox] "longpremise \<Longrightarrow> longerpremise \<Longrightarrow> P(f(f(f(f(f(f(f(f(f(x)))))))))) \<Longrightarrow> longestpremise \<Longrightarrow> conclusion"}
\end{theorem}
-*}
+
-subsection{* Doing it yourself\label{sec:yourself}*}
+\subsection{Doing it yourself\label{sec:yourself}}
-text{* If for some reason you want or need to present theorems your
+If for some reason you want or need to present theorems your
own way, you can extract the premises and the conclusion explicitly
and combine them as you like:
\begin{itemize}
@@ -317,33 +316,94 @@
Thus you can rearrange or hide premises and typeset the theorem as you like.
Styles like \verb!(prem 1)! are a general mechanism explained
in \S\ref{sec:styles}.
-*}
+
+
+\subsection{Patterns}
+
+
+In \S\ref{sec:varnames} we shows how to create patterns containing ``@{term DUMMY}''.
+You can drive this game even further and extend the syntax of let
+bindings such that certain functions like @{term fst}, @{term hd},
+etc.\ are printed as patterns. \texttt{OptionalSugar} provides the following:
-subsection "Patterns"
+\begin{center}
+\begin{tabular}{l@ {~~produced by~~}l}
+@{term "let x = fst p in t"} & \verb!@!\verb!{term "let x = fst p in t"}!\\
+@{term "let x = snd p in t"} & \verb!@!\verb!{term "let x = snd p in t"}!\\
+@{term "let x = hd xs in t"} & \verb!@!\verb!{term "let x = hd xs in t"}!\\
+@{term "let x = tl xs in t"} & \verb!@!\verb!{term "let x = tl xs in t"}!\\
+@{term "let x = the y in t"} & \verb!@!\verb!{term "let x = the y in t"}!\\
+\end{tabular}
+\end{center}
+
+
+\section {Styles\label{sec:styles}}
-text {*
+The \verb!thm! antiquotation works nicely for single theorems, but
+sets of equations as used in definitions are more difficult to
+typeset nicely: people tend to prefer aligned @{text "="} signs.
+
+To deal with such cases where it is desirable to dive into the structure
+of terms and theorems, Isabelle offers antiquotations featuring ``styles'':
+
+\begin{quote}
+\verb!@!\verb!{thm (style) thm}!\\
+\verb!@!\verb!{prop (style) thm}!\\
+\verb!@!\verb!{term (style) term}!\\
+\verb!@!\verb!{term_type (style) term}!\\
+\verb!@!\verb!{typeof (style) term}!\\
+\end{quote}
- In \S\ref{sec:varnames} we shows how to create patterns containing
- ``@{term DUMMY}''.
- You can drive this game even further and extend the syntax of let
- bindings such that certain functions like @{term fst}, @{term hd},
- etc.\ are printed as patterns. \texttt{OptionalSugar} provides the
- following:
-
- \begin{center}
- \begin{tabular}{l@ {~~produced by~~}l}
- @{term "let x = fst p in t"} & \verb!@!\verb!{term "let x = fst p in t"}!\\
- @{term "let x = snd p in t"} & \verb!@!\verb!{term "let x = snd p in t"}!\\
- @{term "let x = hd xs in t"} & \verb!@!\verb!{term "let x = hd xs in t"}!\\
- @{term "let x = tl xs in t"} & \verb!@!\verb!{term "let x = tl xs in t"}!\\
- @{term "let x = the y in t"} & \verb!@!\verb!{term "let x = the y in t"}!\\
- \end{tabular}
- \end{center}
-*}
+ A ``style'' is a transformation of a term. There are predefined
+ styles, namely \verb!lhs! and \verb!rhs!, \verb!prem! with one argument, and \verb!concl!.
+For example, the output
+\begin{center}
+\begin{tabular}{l@ {~~@{text "="}~~}l}
+@{thm (lhs) append_Nil} & @{thm (rhs) append_Nil}\\
+@{thm (lhs) append_Cons} & @{thm (rhs) append_Cons}
+\end{tabular}
+\end{center}
+is produced by the following code:
+\begin{quote}
+ \verb!\begin{center}!\\
+ \verb!\begin{tabular}{l@ {~~!\verb!@!\verb!{text "="}~~}l}!\\
+ \verb!@!\verb!{thm (lhs) append_Nil} & @!\verb!{thm (rhs) append_Nil}\\!\\
+ \verb!@!\verb!{thm (lhs) append_Cons} & @!\verb!{thm (rhs) append_Cons}!\\
+ \verb!\end{tabular}!\\
+ \verb!\end{center}!
+\end{quote}
+Note the space between \verb!@! and \verb!{! in the tabular argument.
+It prevents Isabelle from interpreting \verb!@ {~~...~~}!
+as an antiquotation. The styles \verb!lhs! and \verb!rhs!
+extract the left hand side (or right hand side respectively) from the
+conclusion of propositions consisting of a binary operator
+(e.~g.~@{text "="}, @{text "\<equiv>"}, @{text "<"}).
-section "Proofs"
+Likewise, \verb!concl! may be used as a style to show just the
+conclusion of a proposition. For example, take \verb!hd_Cons_tl!:
+\begin{center}
+ @{thm hd_Cons_tl}
+\end{center}
+To print just the conclusion,
+\begin{center}
+ @{thm (concl) hd_Cons_tl}
+\end{center}
+type
+\begin{quote}
+ \verb!\begin{center}!\\
+ \verb!@!\verb!{thm (concl) hd_Cons_tl}!\\
+ \verb!\end{center}!
+\end{quote}
+Beware that any options must be placed \emph{before} the style, as in this example.
-text {* Full proofs, even if written in beautiful Isar style, are
+Further use cases can be found in \S\ref{sec:yourself}.
+If you are not afraid of ML, you may also define your own styles.
+Have a look at module @{ML_struct Term_Style}.
+
+
+\section {Proofs}
+
+Full proofs, even if written in beautiful Isar style, are
likely to be too long and detailed to be included in conference
papers, but some key lemmas might be of interest.
It is usually easiest to put them in figures like the one in Fig.\
@@ -386,74 +446,85 @@
\end{quote}
Other theory text, e.g.\ definitions, can be put in figures, too.
-*}
-section {*Styles\label{sec:styles}*}
+\section{Theory snippets}
-text {*
- The \verb!thm! antiquotation works nicely for single theorems, but
- sets of equations as used in definitions are more difficult to
- typeset nicely: people tend to prefer aligned @{text "="} signs.
+This section describes how to include snippets of a theory text in some other \LaTeX\ document.
+The typical scenario is that the description of your theory is not part of the theory text but
+a separate document that antiquotes bits of the theory. This works well for terms and theorems
+but there are no antiquotations, for example, for function definitions or proofs. Even if there are antiquotations,
+the output is usually a reformatted (by Isabelle) version of the input and may not look like
+you wanted it to look. Here is how to include a snippet of theory text (in \LaTeX\ form) in some
+other \LaTeX\ document, in 4 easy steps. Beware that these snippets are not processed by
+any antiquotation mechanism: the resulting \LaTeX\ text is more or less exactly what you wrote
+in the theory, without any added sugar.
- To deal with such cases where it is desirable to dive into the structure
- of terms and theorems, Isabelle offers antiquotations featuring
- ``styles'':
+\subsection{Theory markup}
- \begin{quote}
- \verb!@!\verb!{thm (style) thm}!\\
- \verb!@!\verb!{prop (style) thm}!\\
- \verb!@!\verb!{term (style) term}!\\
- \verb!@!\verb!{term_type (style) term}!\\
- \verb!@!\verb!{typeof (style) term}!\\
- \end{quote}
+Include some markers at the beginning and the end of the theory snippet you want to cut out.
+You have to place the following lines before and after the snippet, where snippets must always be
+consecutive lines of theory text:
+\begin{quote}
+\verb!\text_raw{!\verb!*\snip{!\emph{snippetname}\verb!}{1}{2}{%*!\verb!}!\\
+\emph{theory text}\\
+\verb!\text_raw{!\verb!*!\verb!}%endsnip*!\verb!}!
+\end{quote}
+where \emph{snippetname} should be a unique name for the snippet. The numbers \texttt{1}
+and \texttt{2} are explained in a moment.
+
+\subsection{Generate the \texttt{.tex} file}
- A ``style'' is a transformation of a term. There are predefined
- styles, namely \verb!lhs! and \verb!rhs!, \verb!prem! with one argument, and \verb!concl!.
- For example,
- the output
- \begin{center}
- \begin{tabular}{l@ {~~@{text "="}~~}l}
- @{thm (lhs) append_Nil} & @{thm (rhs) append_Nil}\\
- @{thm (lhs) append_Cons} & @{thm (rhs) append_Cons}
- \end{tabular}
- \end{center}
- is produced by the following code:
- \begin{quote}
- \verb!\begin{center}!\\
- \verb!\begin{tabular}{l@ {~~!\verb!@!\verb!{text "="}~~}l}!\\
- \verb!@!\verb!{thm (lhs) append_Nil} & @!\verb!{thm (rhs) append_Nil}\\!\\
- \verb!@!\verb!{thm (lhs) append_Cons} & @!\verb!{thm (rhs) append_Cons}!\\
- \verb!\end{tabular}!\\
- \verb!\end{center}!
- \end{quote}
- Note the space between \verb!@! and \verb!{! in the tabular argument.
- It prevents Isabelle from interpreting \verb!@ {~~...~~}!
- as an antiquotation. The styles \verb!lhs! and \verb!rhs!
- extract the left hand side (or right hand side respectively) from the
- conclusion of propositions consisting of a binary operator
- (e.~g.~@{text "="}, @{text "\<equiv>"}, @{text "<"}).
+Run your theory \texttt{T} with the \texttt{isabelle} \texttt{build} tool
+to generate the \LaTeX-file \texttt{T.tex} which is needed for the next step,
+extraction of marked snippets.
+You may also want to process \texttt{T.tex} to generate a pdf document.
+This requires a definition of \texttt{\char`\\snippet}:
+\begin{verbatim}
+\newcommand{\repeatisanl}[1]
+ {\ifnum#1=0\else\isanewline\repeatisanl{\numexpr#1-1}\fi}
+\newcommand{\snip}[4]{\repeatisanl#2#4\repeatisanl#3}
+\end{verbatim}
+Parameter 2 and 3 of \texttt{\char`\\snippet} are numbers (the \texttt{1}
+and \texttt{2} above) and determine how many newlines are inserted before and after the snippet.
+Unfortunately \texttt{text\_raw} eats up all preceding and following newlines
+and they have to be inserted again in this manner. Otherwise the document generated from \texttt{T.tex}
+will look ugly around the snippets. It can take some iterations to get the number of required
+newlines exactly right.
+
+\subsection{Extract marked snippets}
+\label{subsec:extract}
- Likewise, \verb!concl! may be used as a style to show just the
- conclusion of a proposition. For example, take \verb!hd_Cons_tl!:
- \begin{center}
- @{thm hd_Cons_tl}
- \end{center}
- To print just the conclusion,
- \begin{center}
- @{thm (concl) hd_Cons_tl}
- \end{center}
- type
- \begin{quote}
- \verb!\begin{center}!\\
- \verb!@!\verb!{thm (concl) hd_Cons_tl}!\\
- \verb!\end{center}!
- \end{quote}
- Beware that any options must be placed \emph{before}
- the style, as in this example.
+Extract the marked bits of text with a shell-level script, e.g.
+\begin{quote}
+\verb!sed -n '/\\snip{/,/endsnip/p' T.tex > !\emph{snippets}\verb!.tex!
+\end{quote}
+File \emph{snippets}\texttt{.tex} (the name is arbitrary) now contains a sequence of blocks like this
+\begin{quote}
+\verb!\snip{!\emph{snippetname}\verb!}{1}{2}{%!\\
+\emph{theory text}\\
+\verb!}%endsnip!
+\end{quote}
+
+\subsection{Including snippets}
- Further use cases can be found in \S\ref{sec:yourself}.
- If you are not afraid of ML, you may also define your own styles.
- Have a look at module @{ML_struct Term_Style}.
+In the preamble of the document where the snippets are to be used you define \texttt{\char`\\snip}
+and input \emph{snippets}\texttt{.tex}:
+\begin{verbatim}
+\newcommand{\snip}[4]
+ {\expandafter\newcommand\csname #1\endcsname{#4}}
+\input{snippets}
+\end{verbatim}
+This definition of \texttt{\char`\\snip} simply has the effect of defining for each snippet
+\emph{snippetname} a \LaTeX\ command \texttt{\char`\\}\emph{snippetname}
+that produces the corresponding snippet text. In the body of your document you can display that text
+like this:
+\begin{quote}
+\verb!\begin{isabelle}!\\
+\texttt{\char`\\}\emph{snippetname}\\
+\verb!\end{isabelle}!
+\end{quote}
+The \texttt{isabelle} environment is the one defined in the standard file
+\texttt{isabelle.sty} which most likely you are loading anyway.
*}
(*<*)