--- a/doc-src/LaTeXsugar/Sugar/document/Sugar.tex Mon Aug 27 22:14:17 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,585 +0,0 @@
-%
-\begin{isabellebody}%
-\def\isabellecontext{Sugar}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isatagtheory
-%
-\endisatagtheory
-{\isafoldtheory}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isamarkupsection{Introduction%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-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]}!
-and seeing Isabelle typeset it for them:
-\begin{isabelle}%
-{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C53756D3E}{\isasymSum}}x{\isaliteral{5C3C696E3E}{\isasymin}}A{\isaliteral{2E}{\isachardot}}\ {\isaliteral{5C3C53756D3E}{\isasymSum}}y{\isaliteral{5C3C696E3E}{\isasymin}}B{\isaliteral{2E}{\isachardot}}\ f\ x\ y{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C53756D3E}{\isasymSum}}{\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}\ y{\isaliteral{29}{\isacharparenright}}{\isaliteral{5C3C696E3E}{\isasymin}}A\ {\isaliteral{5C3C74696D65733E}{\isasymtimes}}\ B{\isaliteral{2E}{\isachardot}}\ f\ x\ y{\isaliteral{29}{\isacharparenright}}%
-\end{isabelle}
-No typos, no omissions, no sweat.
-If you have not experienced that joy, read Chapter 4, \emph{Presenting
-Theories}, \cite{LNCS2283} first.
-
-If you have mastered the art of Isabelle's \emph{antiquotations},
-i.e.\ things like the above \verb!@!\verb!{thm...}!, beware: in your vanity
-you may be tempted to think that all readers of the stunning ps or pdf
-documents you can now produce at the drop of a hat will be struck with
-awe at the beauty unfolding in front of their eyes. Until one day you
-come across that very critical of readers known as the ``common referee''.
-He has the nasty habit of refusing to understand unfamiliar notation
-like Isabelle's infamous \isa{{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}\ {\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}} no matter how many times you
-explain it in your paper. Even worse, he thinks that using \isa{{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}\ {\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}} for anything other than denotational semantics is a cardinal sin
-that must be punished by instant rejection.
-
-
-This document shows you how to make Isabelle and \LaTeX\ cooperate to
-produce ordinary looking mathematics that hides the fact that it was
-typeset by a machine. You merely need to load the right files:
-\begin{itemize}
-\item Import theory \texttt{LaTeXsugar} in the header of your own
-theory. You may also want bits of \texttt{OptionalSugar}, which you can
-copy selectively into your own theory or import as a whole. Both
-theories live in \texttt{HOL/Library} and are found automatically.
-
-\item Should you need additional \LaTeX\ packages (the text will tell
-you so), you include them at the beginning of your \LaTeX\ document,
-typically in \texttt{root.tex}. For a start, you should
-\verb!\usepackage{amssymb}! --- otherwise typesetting
-\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}x{\isaliteral{2E}{\isachardot}}\ P\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} will fail because the AMS symbol
-\isa{{\isaliteral{5C3C6E6578697374733E}{\isasymnexists}}} is missing.
-\end{itemize}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsection{HOL syntax%
-}
-\isamarkuptrue%
-%
-\isamarkupsubsection{Logic%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-The formula \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C6E6F743E}{\isasymnot}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C6578697374733E}{\isasymexists}}x{\isaliteral{2E}{\isachardot}}\ P\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} is typeset as \isa{{\isaliteral{5C3C6E6578697374733E}{\isasymnexists}}x{\isaliteral{2E}{\isachardot}}\ P\ x}.
-
-The predefined constructs \isa{if}, \isa{let} and
-\isa{case} are set in sans serif font to distinguish them from
-other functions. This improves readability:
-\begin{itemize}
-\item \isa{\textsf{if}\ b\ \textsf{then}\ e\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ \textsf{else}\ e\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}} instead of \isa{if\ b\ then\ e\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ else\ e\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}}.
-\item \isa{\textsf{let}\ x\ {\isaliteral{3D}{\isacharequal}}\ e\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ \textsf{in}\ e\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}} instead of \isa{let\ x\ {\isaliteral{3D}{\isacharequal}}\ e\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ in\ e\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}}.
-\item \isa{\textsf{case}\ x\ \textsf{of}\ True\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ e\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{7C}{\isacharbar}}\ False\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ e\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}} instead of\\
- \isa{case\ x\ of\ True\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ e\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ {\isaliteral{7C}{\isacharbar}}\ False\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ e\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}}.
-\end{itemize}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Sets%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-Although set syntax in HOL is already close to
-standard, we provide a few further improvements:
-\begin{itemize}
-\item \isa{{\isaliteral{7B}{\isacharbraceleft}}x\ {\isaliteral{7C}{\isacharbar}}\ P{\isaliteral{7D}{\isacharbraceright}}} instead of \isa{{\isaliteral{7B}{\isacharbraceleft}}x{\isaliteral{2E}{\isachardot}}\ P{\isaliteral{7D}{\isacharbraceright}}}.
-\item \isa{{\isaliteral{5C3C656D7074797365743E}{\isasymemptyset}}} instead of \isa{{\isaliteral{7B}{\isacharbraceleft}}{\isaliteral{7D}{\isacharbraceright}}}, where
- \isa{{\isaliteral{5C3C656D7074797365743E}{\isasymemptyset}}} is also input syntax.
-\item \isa{{\isaliteral{7B}{\isacharbraceleft}}a{\isaliteral{2C}{\isacharcomma}}\ b{\isaliteral{2C}{\isacharcomma}}\ c{\isaliteral{7D}{\isacharbraceright}}\ {\isaliteral{5C3C756E696F6E3E}{\isasymunion}}\ M} instead of \isa{insert\ a\ {\isaliteral{28}{\isacharparenleft}}insert\ b\ {\isaliteral{28}{\isacharparenleft}}insert\ c\ M{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}}.
-\end{itemize}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Lists%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-If lists are used heavily, the following notations increase readability:
-\begin{itemize}
-\item \isa{x{\isaliteral{5C3C63646F743E}{\isasymcdot}}xs} instead of \isa{x\ {\isaliteral{23}{\isacharhash}}\ xs},
- where \isa{x{\isaliteral{5C3C63646F743E}{\isasymcdot}}xs} is also input syntax.
-If you prefer more space around the $\cdot$ you have to redefine
-\verb!\isasymcdot! in \LaTeX:
-\verb!\renewcommand{\isasymcdot}{\isamath{\,\cdot\,}}!
-
-\item \isa{{\isaliteral{7C}{\isacharbar}}xs{\isaliteral{7C}{\isacharbar}}} instead of \isa{length\ xs}.
-\item \isa{xs\ensuremath{_{[\mathit{n}]}}} instead of \isa{nth\ xs\ n},
- the $n$th element of \isa{xs}.
-
-\item Human readers are good at converting automatically from lists to
-sets. Hence \texttt{OptionalSugar} contains syntax for suppressing the
-conversion function \isa{set}: for example, \isa{{\isaliteral{22}{\isachardoublequote}}x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ set\ xs{\isaliteral{22}{\isachardoublequote}}}
-becomes \isa{x\ {\isaliteral{5C3C696E3E}{\isasymin}}\ xs}.
-
-\item The \isa{{\isaliteral{40}{\isacharat}}} operation associates implicitly to the right,
-which leads to unpleasant line breaks if the term is too long for one
-line. To avoid this, \texttt{OptionalSugar} contains syntax to group
-\isa{{\isaliteral{40}{\isacharat}}}-terms to the left before printing, which leads to better
-line breaking behaviour:
-\begin{isabelle}%
-term\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{0}}\ \isacharat\ term\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\ \isacharat\ term\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{2}}\ \isacharat\ term\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{3}}\ \isacharat\ term\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{4}}\ \isacharat\ term\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{5}}\ \isacharat\ term\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{6}}\ \isacharat\ term\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{7}}\ \isacharat\ term\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{8}}\ \isacharat\ term\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{9}}\ \isacharat\ term\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{0}}%
-\end{isabelle}
-
-\end{itemize}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Numbers%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-Coercions between numeric types are alien to mathematicians who
-consider, for example, \isa{nat} as a subset of \isa{int}.
-\texttt{OptionalSugar} contains syntax for suppressing numeric coercions such
-as \isa{int} \isa{{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}} \isa{nat\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ int}. For example,
-\isa{{\isaliteral{22}{\isachardoublequote}}int\ {\isadigit{5}}{\isaliteral{22}{\isachardoublequote}}} is printed as \isa{{\isadigit{5}}}. Embeddings of types
-\isa{nat}, \isa{int}, \isa{real} are covered; non-injective coercions such
-as \isa{nat} \isa{{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}} \isa{int\ {\isaliteral{5C3C52696768746172726F773E}{\isasymRightarrow}}\ nat} are not and should not be
-hidden.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsection{Printing theorems%
-}
-\isamarkuptrue%
-%
-\isamarkupsubsection{Question marks%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-If you print anything, especially theorems, containing
-schematic variables they are prefixed with a question mark:
-\verb!@!\verb!{thm conjI}! results in \isa{{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}{\isaliteral{3F}{\isacharquery}}P{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{3F}{\isacharquery}}Q{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{3F}{\isacharquery}}P\ {\isaliteral{5C3C616E643E}{\isasymand}}\ {\isaliteral{3F}{\isacharquery}}Q}. Most of the time
-you would rather not see the question marks. There is an attribute
-\verb!no_vars! that you can attach to the theorem that turns its
-schematic into ordinary free variables: \verb!@!\verb!{thm conjI[no_vars]}!
-results in \isa{{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}P{\isaliteral{3B}{\isacharsemicolon}}\ Q{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ P\ {\isaliteral{5C3C616E643E}{\isasymand}}\ Q}.
-
-This \verb!no_vars! business can become a bit tedious.
-If you would rather never see question marks, simply put
-\begin{quote}
-\verb|Printer.show_question_marks_default := false|\verb!;!
-\end{quote}
-at the beginning of your file \texttt{ROOT.ML}.
-The rest of this document is produced with this flag set to \texttt{false}.
-
-Hint: Setting \verb|Printer.show_question_marks_default| to \texttt{false} only
-suppresses question marks; variables that end in digits,
-e.g. \isa{x{\isadigit{1}}}, are still printed with a trailing \isa{{\isaliteral{2E}{\isachardot}}{\isadigit{0}}},
-e.g. \isa{x{\isadigit{1}}{\isaliteral{2E}{\isachardot}}{\isadigit{0}}}, their internal index. This can be avoided by
-turning the last digit into a subscript: write \verb!x\<^isub>1! and
-obtain the much nicer \isa{x\isaliteral{5C3C5E697375623E}{}\isactrlisub {\isadigit{1}}}.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Qualified names%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-If there are multiple declarations of the same name, Isabelle prints
-the qualified name, for example \isa{T{\isaliteral{2E}{\isachardot}}length}, where \isa{T} is the
-theory it is defined in, to distinguish it from the predefined \isa{{\isaliteral{22}{\isachardoublequote}}List{\isaliteral{2E}{\isachardot}}length{\isaliteral{22}{\isachardoublequote}}}. 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.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Variable names\label{sec:varnames}%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-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}:
-\isa{{\isaliteral{5C3C6C6272616B6B3E}{\isasymlbrakk}}{\isaliteral{5C3C7068693E}{\isasymphi}}{\isaliteral{3B}{\isacharsemicolon}}\ {\isaliteral{5C3C7073693E}{\isasympsi}}{\isaliteral{5C3C726272616B6B3E}{\isasymrbrakk}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ {\isaliteral{5C3C7068693E}{\isasymphi}}\ {\isaliteral{5C3C616E643E}{\isasymand}}\ {\isaliteral{5C3C7073693E}{\isasympsi}}} is the result of
-\begin{quote}
-\verb!@!\verb!{thm conjI[where P = \<phi> and Q = \<psi>]}!
-\end{quote}
-To support the ``\_''-notation for irrelevant variables
-the constant \texttt{DUMMY} has been introduced:
-\isa{fst\ {\isaliteral{28}{\isacharparenleft}}a{\isaliteral{2C}{\isacharcomma}}\ \_{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ a} is produced by
-\begin{quote}
-\verb!@!\verb!{thm fst_conv[where b = DUMMY]}!
-\end{quote}
-Variables that are bound by quantifiers or lambdas cannot be renamed
-like this. Instead, the attribute \texttt{rename\_abs} does the
-job. It expects a list of names or underscores, similar to the
-\texttt{of} attribute:
-\begin{quote}
-\verb!@!\verb!{thm split_paired_All[rename_abs _ l r]}!
-\end{quote}
-produces \isa{{\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}x{\isaliteral{2E}{\isachardot}}\ P\ x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ {\isaliteral{28}{\isacharparenleft}}{\isaliteral{5C3C666F72616C6C3E}{\isasymforall}}l\ r{\isaliteral{2E}{\isachardot}}\ P\ {\isaliteral{28}{\isacharparenleft}}l{\isaliteral{2C}{\isacharcomma}}\ r{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}}.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Inference rules%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-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.
-
-Writing \verb!@!\verb!{thm[mode=Rule] conjI}! produces
-\isa{\mbox{}\inferrule{\mbox{P}\\\ \mbox{Q}}{\mbox{P\ {\isaliteral{5C3C616E643E}{\isasymand}}\ Q}}}, even in the middle of a sentence.
-If you prefer your inference rule on a separate line, maybe with a name,
-\begin{center}
-\isa{\mbox{}\inferrule{\mbox{P}\\\ \mbox{Q}}{\mbox{P\ {\isaliteral{5C3C616E643E}{\isasymand}}\ Q}}} {\sc conjI}
-\end{center}
-is produced by
-\begin{quote}
-\verb!\begin{center}!\\
-\verb!@!\verb!{thm[mode=Rule] conjI} {\sc conjI}!\\
-\verb!\end{center}!
-\end{quote}
-It is not recommended to use the standard \texttt{display} option
-together with \texttt{Rule} because centering does not work and because
-the line breaking mechanisms of \texttt{display} and \texttt{mathpartir} can
-clash.
-
-Of course you can display multiple rules in this fashion:
-\begin{quote}
-\verb!\begin{center}!\\
-\verb!@!\verb!{thm[mode=Rule] conjI} {\sc conjI} \\[1ex]!\\
-\verb!@!\verb!{thm[mode=Rule] conjE} {\sc disjI$_1$} \qquad!\\
-\verb!@!\verb!{thm[mode=Rule] disjE} {\sc disjI$_2$}!\\
-\verb!\end{center}!
-\end{quote}
-yields
-\begin{center}\small
-\isa{\mbox{}\inferrule{\mbox{P}\\\ \mbox{Q}}{\mbox{P\ {\isaliteral{5C3C616E643E}{\isasymand}}\ Q}}} {\sc conjI} \\[1ex]
-\isa{\mbox{}\inferrule{\mbox{P}}{\mbox{P\ {\isaliteral{5C3C6F723E}{\isasymor}}\ Q}}} {\sc disjI$_1$} \qquad
-\isa{\mbox{}\inferrule{\mbox{Q}}{\mbox{P\ {\isaliteral{5C3C6F723E}{\isasymor}}\ Q}}} {\sc disjI$_2$}
-\end{center}
-
-The \texttt{mathpartir} package copes well if there are too many
-premises for one line:
-\begin{center}
-\isa{\mbox{}\inferrule{\mbox{A\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ B}\\\ \mbox{B\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ C}\\\ \mbox{C\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ D}\\\ \mbox{D\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ E}\\\ \mbox{E\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ F}\\\ \mbox{F\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ G}\\\ \mbox{G\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ H}\\\ \mbox{H\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ I}\\\ \mbox{I\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ J}\\\ \mbox{J\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ K}}{\mbox{A\ {\isaliteral{5C3C6C6F6E6772696768746172726F773E}{\isasymlongrightarrow}}\ K}}}
-\end{center}
-
-Limitations: 1. Premises and conclusion must each not be longer than
-the line. 2. Premises that are \isa{{\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}}-implications are again
-displayed with a horizontal line, which looks at least unusual.
-
-
-In case you print theorems without premises no rule will be printed by the
-\texttt{Rule} print mode. However, you can use \texttt{Axiom} instead:
-\begin{quote}
-\verb!\begin{center}!\\
-\verb!@!\verb!{thm[mode=Axiom] refl} {\sc refl}! \\
-\verb!\end{center}!
-\end{quote}
-yields
-\begin{center}
-\isa{\mbox{}\inferrule{\mbox{}}{\mbox{t\ {\isaliteral{3D}{\isacharequal}}\ t}}} {\sc refl}
-\end{center}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Displays and font sizes%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-When displaying theorems with the \texttt{display} option, e.g.
-\verb!@!\verb!{thm[display] refl}! \begin{isabelle}%
-t\ {\isaliteral{3D}{\isacharequal}}\ t%
-\end{isabelle} 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.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-\isacommand{lemma}\isamarkupfalse%
-\ {\isaliteral{22}{\isachardoublequoteopen}}t\ {\isaliteral{3D}{\isacharequal}}\ t{\isaliteral{22}{\isachardoublequoteclose}}%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\begin{isamarkuptext}%
-\noindent Otherwise \verb!\isastyleminor! is used,
-which does not modify the font size (assuming you stick to the default
-\verb!\isabellestyle{it}! in \texttt{root.tex}). If you prefer
-normal font size throughout your text, include
-\begin{quote}
-\verb!\renewcommand{\isastyle}{\isastyleminor}!
-\end{quote}
-in \texttt{root.tex}. On the other hand, if you like the small font,
-just put \verb!\isastyle! in front of the text in question,
-e.g.\ at the start of one of the center-environments above.
-
-The advantage of the display option is that you can display a whole
-list of theorems in one go. For example,
-\verb!@!\verb!{thm[display] append.simps}!
-generates \begin{isabelle}%
-{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ \isacharat\ ys\ {\isaliteral{3D}{\isacharequal}}\ ys\isasep\isanewline%
-x{\isaliteral{5C3C63646F743E}{\isasymcdot}}xs\ \isacharat\ ys\ {\isaliteral{3D}{\isacharequal}}\ x{\isaliteral{5C3C63646F743E}{\isasymcdot}}xs\ \isacharat\ ys%
-\end{isabelle}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{If-then%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-If you prefer a fake ``natural language'' style you can produce
-the body of
-\newtheorem{theorem}{Theorem}
-\begin{theorem}
-\isa{{\normalsize{}If\,}\ \mbox{i\ {\isaliteral{5C3C6C653E}{\isasymle}}\ j}\ {\normalsize \,and\,}\ \mbox{j\ {\isaliteral{5C3C6C653E}{\isasymle}}\ k}\ {\normalsize \,then\,}\ i\ {\isaliteral{5C3C6C653E}{\isasymle}}\ k{\isaliteral{2E}{\isachardot}}}
-\end{theorem}
-by typing
-\begin{quote}
-\verb!@!\verb!{thm[mode=IfThen] le_trans}!
-\end{quote}
-
-In order to prevent odd line breaks, the premises are put into boxes.
-At times this is too drastic:
-\begin{theorem}
-\isa{{\normalsize{}If\,}\ \mbox{longpremise}\ {\normalsize \,and\,}\ \mbox{longerpremise}\ {\normalsize \,and\,}\ \mbox{P\ {\isaliteral{28}{\isacharparenleft}}f\ {\isaliteral{28}{\isacharparenleft}}f\ {\isaliteral{28}{\isacharparenleft}}f\ {\isaliteral{28}{\isacharparenleft}}f\ {\isaliteral{28}{\isacharparenleft}}f\ {\isaliteral{28}{\isacharparenleft}}f\ {\isaliteral{28}{\isacharparenleft}}f\ {\isaliteral{28}{\isacharparenleft}}f\ {\isaliteral{28}{\isacharparenleft}}f\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}}\ {\normalsize \,and\,}\ \mbox{longestpremise}\ {\normalsize \,then\,}\ conclusion{\isaliteral{2E}{\isachardot}}}
-\end{theorem}
-In which case you should use \texttt{IfThenNoBox} instead of
-\texttt{IfThen}:
-\begin{theorem}
-\isa{{\normalsize{}If\,}\ longpremise\ {\normalsize \,and\,}\ longerpremise\ {\normalsize \,and\,}\ P\ {\isaliteral{28}{\isacharparenleft}}f\ {\isaliteral{28}{\isacharparenleft}}f\ {\isaliteral{28}{\isacharparenleft}}f\ {\isaliteral{28}{\isacharparenleft}}f\ {\isaliteral{28}{\isacharparenleft}}f\ {\isaliteral{28}{\isacharparenleft}}f\ {\isaliteral{28}{\isacharparenleft}}f\ {\isaliteral{28}{\isacharparenleft}}f\ {\isaliteral{28}{\isacharparenleft}}f\ x{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}{\isaliteral{29}{\isacharparenright}}\ {\normalsize \,and\,}\ longestpremise\ {\normalsize \,then\,}\ conclusion{\isaliteral{2E}{\isachardot}}}
-\end{theorem}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Doing it yourself\label{sec:yourself}%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-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}
-\item \verb!@!\verb!{thm (prem 1)! $thm$\verb!}!
-prints premise 1 of $thm$.
-\item \verb!@!\verb!{thm (concl)! $thm$\verb!}!
-prints the conclusion of $thm$.
-\end{itemize}
-For example, ``from \isa{Q} and
-\isa{P} we conclude \isa{P\ {\isaliteral{5C3C616E643E}{\isasymand}}\ Q}''
-is produced by
-\begin{quote}
-\verb!from !\verb!@!\verb!{thm (prem 2) conjI}! \verb!and !\verb!@!\verb!{thm (prem 1) conjI}!\\
-\verb!we conclude !\verb!@!\verb!{thm (concl) conjI}!
-\end{quote}
-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}.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsubsection{Patterns%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-In \S\ref{sec:varnames} we shows how to create patterns containing
- ``\isa{\_}''.
- You can drive this game even further and extend the syntax of let
- bindings such that certain functions like \isa{fst}, \isa{hd},
- etc.\ are printed as patterns. \texttt{OptionalSugar} provides the
- following:
-
- \begin{center}
- \begin{tabular}{l@ {~~produced by~~}l}
- \isa{\textsf{let}\ {\isaliteral{28}{\isacharparenleft}}x{\isaliteral{2C}{\isacharcomma}}\ \_{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ p\ \textsf{in}\ t} & \verb!@!\verb!{term "let x = fst p in t"}!\\
- \isa{\textsf{let}\ {\isaliteral{28}{\isacharparenleft}}\_{\isaliteral{2C}{\isacharcomma}}\ x{\isaliteral{29}{\isacharparenright}}\ {\isaliteral{3D}{\isacharequal}}\ p\ \textsf{in}\ t} & \verb!@!\verb!{term "let x = snd p in t"}!\\
- \isa{\textsf{let}\ x{\isaliteral{5C3C63646F743E}{\isasymcdot}}\_\ {\isaliteral{3D}{\isacharequal}}\ xs\ \textsf{in}\ t} & \verb!@!\verb!{term "let x = hd xs in t"}!\\
- \isa{\textsf{let}\ \_{\isaliteral{5C3C63646F743E}{\isasymcdot}}x\ {\isaliteral{3D}{\isacharequal}}\ xs\ \textsf{in}\ t} & \verb!@!\verb!{term "let x = tl xs in t"}!\\
- \isa{\textsf{let}\ Some\ x\ {\isaliteral{3D}{\isacharequal}}\ y\ \textsf{in}\ t} & \verb!@!\verb!{term "let x = the y in t"}!\\
- \end{tabular}
- \end{center}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsection{Proofs%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-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.\
-\ref{fig:proof}. This was achieved with the \isakeyword{text\_raw} command:%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\begin{figure}
- \begin{center}\begin{minipage}{0.6\textwidth}
- \isastyleminor\isamarkuptrue
-\isacommand{lemma}\isamarkupfalse%
-\ True\isanewline
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-\isacommand{proof}\isamarkupfalse%
-\ {\isaliteral{2D}{\isacharminus}}\isanewline
-\ \ %
-\isamarkupcmt{pretty trivial%
-}
-\isanewline
-\ \ \isacommand{show}\isamarkupfalse%
-\ True\ \isacommand{by}\isamarkupfalse%
-\ force\isanewline
-\isacommand{qed}\isamarkupfalse%
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\end{minipage}\end{center}
- \caption{Example proof in a figure.}\label{fig:proof}
- \end{figure}
-%
-\begin{isamarkuptext}%
-\begin{quote}
-\small
-\verb!text_raw {!\verb!*!\\
-\verb! \begin{figure}!\\
-\verb! \begin{center}\begin{minipage}{0.6\textwidth}!\\
-\verb! \isastyleminor\isamarkuptrue!\\
-\verb!*!\verb!}!\\
-\verb!lemma True!\\
-\verb!proof -!\\
-\verb! -- "pretty trivial"!\\
-\verb! show True by force!\\
-\verb!qed!\\
-\verb!text_raw {!\verb!*!\\
-\verb! \end{minipage}\end{center}!\\
-\verb! \caption{Example proof in a figure.}\label{fig:proof}!\\
-\verb! \end{figure}!\\
-\verb!*!\verb!}!
-\end{quote}
-
-Other theory text, e.g.\ definitions, can be put in figures, too.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isamarkupsection{Styles\label{sec:styles}%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-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 \isa{{\isaliteral{3D}{\isacharequal}}} 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}
-
- 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@ {~~\isa{{\isaliteral{3D}{\isacharequal}}}~~}l}
- \isa{{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ \isacharat\ ys} & \isa{ys}\\
- \isa{x{\isaliteral{5C3C63646F743E}{\isasymcdot}}xs\ \isacharat\ ys} & \isa{x{\isaliteral{5C3C63646F743E}{\isasymcdot}}xs\ \isacharat\ ys}
- \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.~\isa{{\isaliteral{3D}{\isacharequal}}}, \isa{{\isaliteral{5C3C65717569763E}{\isasymequiv}}}, \isa{{\isaliteral{3C}{\isacharless}}}).
-
- 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}
- \isa{xs\ {\isaliteral{5C3C6E6F7465713E}{\isasymnoteq}}\ {\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ hd\ xs{\isaliteral{5C3C63646F743E}{\isasymcdot}}tl\ xs\ {\isaliteral{3D}{\isacharequal}}\ xs}
- \end{center}
- To print just the conclusion,
- \begin{center}
- \isa{hd\ xs{\isaliteral{5C3C63646F743E}{\isasymcdot}}tl\ xs\ {\isaliteral{3D}{\isacharequal}}\ xs}
- \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.
-
- 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 \verb|Term_Style|.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-%
-\isatagtheory
-%
-\endisatagtheory
-{\isafoldtheory}%
-%
-\isadelimtheory
-%
-\endisadelimtheory
-\end{isabellebody}%
-%%% Local Variables:
-%%% mode: latex
-%%% TeX-master: "root"
-%%% End: