Quelle Sugar.thy

Sprache: Isabelle

(*<*)
theory Sugar
imports
  "HOL-Library.LaTeXsugar"
  "HOL-Library.OptionalSugar"
begin
no_translations
  ("prop") "P ∧ Q ==> R" <= ("prop") "P ==> Q ==> R"
(*>*)
text‹
section{Introduction}

document is for those Isabelle users who have mastered
art of mixing \LaTeX\ text and Isabelle theories and never want to
a theorem by hand anymore because they have experienced the
of writing \verb!@!\verb!{thm[display,mode=latex_sum] sum_Suc_diff [no_vars]}!
seeing Isabelle typeset it for them:
{thm[display,mode=latex_sum] sum_Suc_diff[no_vars]}
typos, no omissions, no sweat.
you have not experienced that joy, read Chapter 4, \emph{Presenting
}, cite‹LNCS2283› first.

you have mastered the art of Isabelle's \emph{antiquotations},
.e.\ things like the above \verb!@!\verb!{thm...}!, beware: in your vanity
may be tempted to think that all readers of the stunning
you can now produce at the drop of a hat will be struck with
at the beauty unfolding in front of their eyes. Until one day you
across that very critical of readers known as the ``common referee''.
has the nasty habit of refusing to understand unfamiliar notation
Isabelle's infamous ‹[ ] ==>› no matter how many times you
it in your paper. Even worse, he thinks that using ‹[
]› for anything other than denotational semantics is a cardinal sin
must be punished by instant rejection.

document shows you how to make Isabelle and \LaTeX\ cooperate to
ordinary looking mathematics that hides the fact that it was
by a machine. You merely need to load the right files:
begin{itemize}
item Import theory \texttt{LaTeXsugar} in the header of your own
. You may also want bits of \texttt{OptionalSugar}, which you can
selectively into your own theory or import as a whole. Both
live in \texttt{HOL/Library}.

item Should you need additional \LaTeX\ packages (the text will tell
so), you include them at the beginning of your \LaTeX\ document,
in \texttt{root.tex}. For a start, you should
verb!\usepackage{amssymb}! --- otherwise typesetting
{prop[source]"¬(∃x. P x)"} will fail because the AMS symbol
‹∄› is missing.
end{itemize}

section{HOL syntax}

subsection{Logic}

formula @{prop[source]"¬(∃x. P x)"} is typeset as prop‹¬(∃x. P x)›.

predefined constructs ‹if›, ‹let› and
‹case› are set in sans serif font to distinguish them from
functions. This improves readability:
begin{itemize}
item term‹if b then e₁ else e₂› instead of ‹if b then e₁ else e₂›.
item term‹let x = e₁ in e₂› instead of ‹let x = e₁ in e₂›.
item term‹case x of True ==> e₁ | False ==> e₂› instead of\\
‹case x of True ==> e₁ | False ==> e₂›.
end{itemize}

subsection{Sets}

set syntax in HOL is already close to
, we provide a few further improvements:
begin{itemize}
item term‹{x. P}› instead of ‹{x. P}›.
item term‹{}› instead of ‹{}›, where
term‹{}› is also input syntax.
item term‹insert a (insert b (insert c M))› instead of ‹insert a (insert b (insert c M))›.
item term‹card A› instead of ‹card A›.
end{itemize}

subsection{Lists}

lists are used heavily, the following notations increase readability:
begin{itemize}
item term‹x # xs› instead of ‹x # xs›,
where term‹x # xs› is also input syntax.
item term‹length xs› instead of ‹length xs›.
item term‹nth xs n› instead of ‹nth xs n›,
the $n$th element of ‹xs›.

item Human readers are good at converting automatically from lists to
. Hence \texttt{OptionalSugar} contains syntax for suppressing the
function const‹set›: for example, @{prop[source]"x ∈ set xs"}
prop‹x ∈ set xs›.

item The ‹@› operation associates implicitly to the right,
leads to unpleasant line breaks if the term is too long for one
. To avoid this, \texttt{OptionalSugar} contains syntax to group
‹@›-terms to the left before printing, which leads to better
breaking behaviour:
{term[display]"term₀ @ term₁ @ term₂ @ term₃ @ term₄ @ term₅ @ term₆ @ term₇ @ term₈ @ term₉ @ term₁₀"}

end{itemize}

subsection{Numbers}

between numeric types are alien to mathematicians who
, for example, 🍋‹nat› as a subset of 🍋‹int›.
texttt{OptionalSugar} contains syntax for suppressing numeric coercions such
const‹int› ‹::› 🍋‹nat ==> int›. For example,
{term[source]"int 5"} is printed as term‹int 5›. Embeddings of types
🍋‹nat›, 🍋‹int›, 🍋‹real› are covered; non-injective coercions such
const‹nat› ‹::› 🍋‹int ==> nat› are not and should not be
.

section{Printing constants and their type}

of
verb!@!\verb!{const myconst}! \verb!@!\verb!{text "::"}! \verb!@!\verb!{typeof myconst}!,
can write \verb!@!\verb!{const_typ myconst}! using the new antiquotation
texttt{const\_typ} defined in \texttt{LaTeXsugar}. For example,
verb!@!\verb!{const_typ length}! produces 🪙‹length› (see below for how to suppress
question mark).
works both for genuine constants and for variables fixed in some context,
in a locale.

section{Printing theorems}

prop‹P ==> Q ==> R› syntax is a bit idiosyncratic. If you would like
avoid it, you can easily print the premises as a conjunction:
prop‹P ∧ Q ==> R›. See \texttt{OptionalSugar} for the required ``code''.

subsection{Question marks}

you print anything, especially theorems, containing
variables they are prefixed with a question mark:
verb!@!\verb!{thm conjI}! results in @{thm conjI}. Most of the time
would rather not see the question marks. There is an attribute
verb!no_vars! that you can attach to the theorem that turns its
into ordinary free variables:
begin{quote}
verb!@!\verb!{thm conjI[no_vars]}!\\
showout @{thm conjI[no_vars]}
end{quote}
\verb!no_vars! business can become a bit tedious.
you would rather never see question marks, simply put
begin{quote}
verb!options [show_question_marks = false]!
end{quote}
the relevant \texttt{ROOT} file, just before the \texttt{theories} for that session.
rest of this document is produced with this flag set to \texttt{false}.
›

(*<*)declare [[show_question_marks = false]](*>*)

subsection ‹Qualified names›

text‹If there are multiple declarations of the same name, Isabelle prints
qualified name, for example ‹T.length›, where ‹T› is the
it is defined in, to distinguish it from the predefined @{const[source]
List.length"}. In case there is no danger of confusion, you can insist on
names (no qualifiers) by setting the \verb!names_short!
option in the context.

subsection {Variable names\label{sec:varnames}}

sometimes happens that you want to change the name of a
in a theorem before printing it. This can easily be achieved
the help of Isabelle's instantiation attribute \texttt{where}:
begin{quote}
verb!@!\verb!{thm conjI[where P = φ and Q = ψ]}!\\
showout @{thm conjI[where P = φ and Q = ψ]}
end{quote}
support the ``\_''-notation for irrelevant variables
constant \texttt{DUMMY} has been introduced:
begin{quote}
verb!@!\verb!{thm fst_conv[of _ DUMMY]}!\\
showout @{thm fst_conv[of _ DUMMY]}
end{quote}
expected, the second argument has been replaced by ``\_'',
the first argument is the ugly ‹x1.0›, a schematic variable
suppressed question mark. Schematic variables that end in digits,
.g. ‹x1›, are still printed with a trailing ‹.0›,
.g. ‹x1.0›, their internal index. This can be avoided by
the last digit into a subscript: write 🍋‹x₁› and
the much nicer ‹x₁›. Alternatively, you can display trailing digits of
and free variables as subscripts with the \texttt{sub} style:
begin{quote}
verb!@!\verb!{thm (sub) fst_conv[of _ DUMMY]}!\\
showout @{thm (sub) fst_conv[of _ DUMMY]}
end{quote}
insertion of underscores can be automated with the \verb!dummy_pats! style:
begin{quote}
verb!@!\verb!{thm (dummy_pats,sub) fst_conv}!\\
showout @{thm (dummy_pats,sub) fst_conv}
end{quote}
theorem must be an equation. Then every schematic variable that occurs
the left-hand but not the right-hand side is replaced by \texttt{DUMMY}.
is convenient for displaying functional programs.

that are bound by quantifiers or lambdas can be renamed
the help of the attribute \verb!rename_abs!.
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]}!\\
showout @{thm split_paired_All[rename_abs _ l r]}
end{quote}

Isabelle $\eta$-contracts terms, for example in the following definition:
›
fun eta where
"eta (x ⋅ xs) = (∀y ∈ set xs. x < y)"
text‹
noindent
you now print the defining equation, the result is not what you hoped for:
begin{quote}
verb!@!\verb!{thm eta.simps}!\\
showout @{thm eta.simps}
end{quote}
such situations you can put the abstractions back by explicitly $\eta$-expanding upon output:
begin{quote}
verb!@!\verb!{thm (eta_expand z) eta.simps}!\\
showout @{thm (eta_expand z) eta.simps}
end{quote}
of a single variable \verb!z! you can give a whole list \verb!x y z!
perform multiple $\eta$-expansions.

subsection{Breaks and boxes}

longer formulas can easily lead to line breaks in unwanted places.
can be avoided by putting \LaTeX-like mboxes in formulas.
is a function @{const_typ mbox} that you can wrap around subterms and that
pretty-printed as a \LaTeX\ \verb$\mbox{ }$.
you are printing a term or formula, you can just insert @{const mbox}
you want. You can also insert it into theorems by
of the fact that @{const mbox} is defined as an identity function. Of course
need to adapt the proof accordingly.

the argument of @{const mbox} is an identifier or an application (i.e.\ of the highest precedence),
will be enclosed in parentheses. Thus \verb!x < mbox(f y)! results in @{term "x < mbox(f y)"}
\verb!x < mbox(y+z)! results in @{term "x < mbox(y+z)"}. You can switch off the
by using the variant @{const mbox0} instead of @{const mbox}:
verb!x < mbox0(y+z)! results in @{term "x < mbox0(y+z)"}.

subsection{Inference rules}

print theorems as inference rules you need to include Didier
\'emy's \texttt{mathpartir} package~cite‹mathpartir›
typesetting inference rules in your \LaTeX\ file.

\verb!@!\verb!{thm[mode=Rule] conjI}! produces
{thm[mode=Rule] conjI}, even in the middle of a sentence.
you prefer your inference rule on a separate line, maybe with a name,
begin{center}
{thm[mode=Rule] conjI} {\sc conjI}
end{center}
produced by
begin{quote}
verb!\begin{center}!\\
verb!@!\verb!{thm[mode=Rule] conjI} {\sc conjI}!\\
verb!\end{center}!
end{quote}
is not recommended to use the standard \texttt{display} option
with \texttt{Rule} because centering does not work and because
line breaking mechanisms of \texttt{display} and \texttt{mathpartir} can
.

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}

begin{center}\small
{thm[mode=Rule] conjI} {\sc conjI} \\[1ex]
{thm[mode=Rule] disjI1} {\sc disjI$_1$} \qquad
{thm[mode=Rule] disjI2} {\sc disjI$_2$}
end{center}

\texttt{mathpartir} package copes well if there are too many
for one line:
begin{center}
{prop[mode=Rule] "[ A ⟶ B; B ⟶ C; C ⟶ D; D ⟶ E; E ⟶ F; F ⟶ G;
G ⟶ H; H ⟶ I; I ⟶ J; J ⟶ K ] ==> A ⟶ K"}
end{center}

: 1. Premises and conclusion must each not be longer than
line. 2. Premises that are ‹==>›-implications are again
with a horizontal line, which looks at least unusual.

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}

begin{center}
{thm[mode=Axiom] refl} {\sc refl}
end{center}

subsection{Displays and font sizes}

displaying theorems with the \texttt{display} option, for example as in
verb!@!\verb!{thm[display] refl}! @{thm[display] refl} the theorem is
in small font. It uses the \LaTeX-macro \verb!\isastyle!,
is also the style that regular theory text is set in, e.g.›

lemma "t = t"
(*<*)oops(*>*)

text‹\noindent Otherwise \verb!\isastyleminor! is used,
does not modify the font size (assuming you stick to the default
verb!\isabellestyle{it}! in \texttt{root.tex}). If you prefer
font size throughout your text, include
begin{quote}
verb!\renewcommand{\isastyle}{\isastyleminor}!
end{quote}
\texttt{root.tex}. On the other hand, if you like the small font,
put \verb!\isastyle! in front of the text in question,
.g.\ at the start of one of the center-environments above.

advantage of the display option is that you can display a whole
of theorems in one go. For example,
verb!@!\verb!{thm[display] append.simps}!
@{thm[display] append.simps}

subsection{If-then}

you prefer a fake ``natural language'' style you can produce
body of
newtheorem{theorem}{Theorem}
begin{theorem}
{thm[mode=IfThen] le_trans}
end{theorem}
typing
begin{quote}
verb!@!\verb!{thm[mode=IfThen] le_trans}!
end{quote}

order to prevent odd line breaks, the premises are put into boxes.
times this is too drastic:
begin{theorem}
{prop[mode=IfThen] "longpremise ==> longerpremise ==> P(f(f(f(f(f(f(f(f(f(x)))))))))) ==> longestpremise ==> conclusion"}
end{theorem}
which case you should use \texttt{IfThenNoBox} instead of
texttt{IfThen}:
begin{theorem}
{prop[mode=IfThenNoBox] "longpremise ==> longerpremise ==> P(f(f(f(f(f(f(f(f(f(x)))))))))) ==> longestpremise ==> conclusion"}
end{theorem}

subsection{Doing it yourself\label{sec:yourself}}

for some reason you want or need to present theorems your
way, you can extract the premises and the conclusion explicitly
combine them as you like:
begin{itemize}
item \verb!@!\verb!{thm (prem 1)! $thm$\verb!}!
premise 1 of $thm$.
item \verb!@!\verb!{thm (concl)! $thm$\verb!}!
the conclusion of $thm$.
end{itemize}
example, ``from @{thm (prem 2) conjI} and
{thm (prem 1) conjI} we conclude @{thm (concl) conjI}''
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}
you can rearrange or hide premises and typeset the theorem as you like.
like \verb!(prem 1)! are a general mechanism explained
\S\ref{sec:styles}.

subsection{Patterns}

\S\ref{sec:varnames} we shows how to create patterns containing ``term‹DUMMY›''.
can drive this game even further and extend the syntax of let
such that certain functions like term‹fst›, term‹hd›,
.\ 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}

section {Styles\label{sec:styles}}

\verb!thm! antiquotation works nicely for single theorems, but
of equations as used in definitions are more difficult to
nicely: people tend to prefer aligned ‹=› signs.

deal with such cases where it is desirable to dive into the structure
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!.
example, the output
begin{center}
begin{tabular}{l@ {~~‹=›~~}l}
{thm (lhs) append_Nil} & @{thm (rhs) append_Nil}\\
{thm (lhs) append_Cons} & @{thm (rhs) append_Cons}
end{tabular}
end{center}
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}
the space between \verb!@! and \verb!{! in the tabular argument.
prevents Isabelle from interpreting \verb!@ {~~...~~}!
an antiquotation. The styles \verb!lhs! and \verb!rhs!
the left hand side (or right hand side respectively) from the
of propositions consisting of a binary operator
e.~g.~‹=›, ‹≡›, ‹<\<close>).

, \verb!concl! may be used as a style to show just the
of a proposition. For example, take \verb!hd_Cons_tl!:
begin{center}
@{thm hd_Cons_tl}
end{center}
print just the conclusion,
begin{center}
@{thm (concl) hd_Cons_tl}
end{center}

begin{quote}
\verb!\begin{center}!\\
\verb!@!\verb!{thm (concl) hd_Cons_tl}!\\
\verb!\end{center}!
end{quote}
that any options must be placed \emph{before} the style, as in this example.

use cases can be found in \S\ref{sec:yourself}.
you are not afraid of ML, you may also define your own styles.
a look at module 🪙‹Term_Style›.

section {Proofs}

proofs, even if written in beautiful Isar style, are
to be too long and detailed to be included in conference
, but some key lemmas might be of interest.
java.lang.NullPointerException: Cannot invoke "String.equals(Object)" because "macro" is null
ref{fig:proof}. This was achieved with the \isakeyword{text\_raw} command:
›
‹
\begin{figure}
\begin{center}\begin{minipage}{0.6\textwidth}
\isastyleminor\isamarkuptrue
›
True
-
show True by (rule TrueI)

‹
\end{minipage}\end{center}
\caption{Example proof in a figure.}\label{fig:proof}
\end{figure}
›
‹

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! show True by (rule TrueI)!\\
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}

theory text, e.g.\ definitions, can be put in figures, too.

section{Theory snippets}

section describes how to include snippets of a theory text in some other \LaTeX\ document.
typical scenario is that the description of your theory is not part of the theory text but
separate document that antiquotes bits of the theory. This works well for terms and theorems
there are no antiquotations, for example, for function definitions or proofs. Even if there are antiquotations,
output is usually a reformatted (by Isabelle) version of the input and may not look like
wanted it to look. Here is how to include a snippet of theory text (in \LaTeX\ form) in some
\LaTeX\ document, in 4 easy steps. Beware that these snippets are not processed by
antiquotation mechanism: the resulting \LaTeX\ text is more or less exactly what you wrote
the theory, without any added sugar.

subsection{Theory markup}

some markers at the beginning and the end of the theory snippet you want to cut out.
have to place the following lines before and after the snippet, where snippets must always be
lines of theory text:
begin{quote}
verb!\text_raw\!\verb!‹\snip{!\emph{snippetname}\verb!}{1}{2}{%\!\verb!›!\\
emph{theory text}\\
verb!\text_raw\!\verb!‹%endsnip\!\verb!›!
end{quote}
\emph{snippetname} should be a unique name for the snippet. The numbers \texttt{1}
\texttt{2} are explained in a moment.

subsection{Generate the \texttt{.tex} file}

your theory \texttt{T} with the \texttt{isabelle} \texttt{build} tool
generate the \LaTeX-file \texttt{T.tex} which is needed for the next step,
of marked snippets.
may also want to process \texttt{T.tex} to generate a pdf document.
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}
2 and 3 of \texttt{\char`\\snippet} are numbers (the \texttt{1}
\texttt{2} above) and determine how many newlines are inserted before and after the snippet.
\texttt{text\_raw} eats up all preceding and following newlines
they have to be inserted again in this manner. Otherwise the document generated from \texttt{T.tex}
look ugly around the snippets. It can take some iterations to get the number of required
exactly right.

subsection{Extract marked snippets}
label{subsec: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}
\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}

the preamble of the document where the snippets are to be used you define \texttt{\char`\\snip}
input \emph{snippets}\texttt{.tex}:
begin{verbatim}
newcommand{\snip}[4]
{\expandafter\newcommand\csname #1\endcsname{#4}}
input{snippets}
end{verbatim}
definition of \texttt{\char`\\snip} simply has the effect of defining for each snippet
emph{snippetname} a \LaTeX\ command \texttt{\char`\\}\emph{snippetname}
produces the corresponding snippet text. In the body of your document you can display that text
this:
begin{quote}
verb!\begin{isabelle}!\\
texttt{\char`\\}\emph{snippetname}\\
verb!\end{isabelle}!
end{quote}
\texttt{isabelle} environment is the one defined in the standard file
texttt{isabelle.sty} which most likely you are loading anyway.
›

(*<*)
end
(*>*)

Messung V0.5 in Prozent

¤ Dauer der Verarbeitung: 0.14 Sekunden (vorverarbeitet am 2026-06-10) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.