--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarTut/Tutorial/document/Tutorial.tex Thu Jun 06 15:34:52 2002 +0200
@@ -0,0 +1,687 @@
+%
+\begin{isabellebody}%
+\def\isabellecontext{Tutorial}%
+\isamarkupfalse%
+%
+\isamarkupchapter{Introduction%
+}
+\isamarkuptrue%
+%
+\isamarkupsection{Step-by-step examples%
+}
+\isamarkuptrue%
+%
+\isamarkupsubsection{Summing natural numbers%
+}
+\isamarkuptrue%
+\isacommand{theorem}\ {\isachardoublequote}{\isadigit{2}}\ {\isacharasterisk}\ {\isacharparenleft}{\isasymSum}i\ {\isacharless}\ n\ {\isacharplus}\ {\isadigit{1}}{\isachardot}\ i{\isacharparenright}\ {\isacharequal}\ n\ {\isacharasterisk}\ {\isacharparenleft}n\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}{\isachardoublequote}\ \ {\isacharparenleft}\isakeyword{is}\ {\isachardoublequote}{\isacharquery}P\ n{\isachardoublequote}{\isacharparenright}\isanewline
+\isamarkupfalse%
+\isacommand{proof}\ {\isacharparenleft}induct\ n{\isacharparenright}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{case}\ {\isadigit{0}}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{then}\ \isamarkupfalse%
+\isacommand{show}\ {\isachardoublequote}{\isacharquery}P\ {\isadigit{0}}{\isachardoublequote}\ \isamarkupfalse%
+\isacommand{by}\ simp\isanewline
+\isamarkupfalse%
+\isacommand{next}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{case}\ {\isacharparenleft}Suc\ n{\isacharparenright}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{let}\ {\isachardoublequote}{\isacharquery}S\ n\ {\isacharequal}\ {\isacharunderscore}{\isachardoublequote}\ {\isacharequal}\ {\isachardoublequote}{\isacharquery}P\ n{\isachardoublequote}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{have}\ {\isachardoublequote}{\isacharquery}S\ {\isacharparenleft}n\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}\ {\isacharequal}\ {\isacharquery}S\ n\ {\isacharplus}\ {\isadigit{2}}\ {\isacharasterisk}\ {\isacharparenleft}n\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}{\isachardoublequote}\ \isamarkupfalse%
+\isacommand{by}\ simp\isanewline
+\ \ \isamarkupfalse%
+\isacommand{also}\ \isamarkupfalse%
+\isacommand{have}\ {\isachardoublequote}{\isacharquery}S\ n\ {\isacharequal}\ n\ {\isacharasterisk}\ {\isacharparenleft}n\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}{\isachardoublequote}\ \isamarkupfalse%
+\isacommand{{\isachardot}}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{also}\ \isamarkupfalse%
+\isacommand{have}\ {\isachardoublequote}{\isasymdots}\ {\isacharplus}\ {\isadigit{2}}\ {\isacharasterisk}\ {\isacharparenleft}n\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}n\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}\ {\isacharasterisk}\ {\isacharparenleft}n\ {\isacharplus}\ {\isadigit{2}}{\isacharparenright}{\isachardoublequote}\ \isamarkupfalse%
+\isacommand{by}\ simp\isanewline
+\ \ \isamarkupfalse%
+\isacommand{finally}\ \isamarkupfalse%
+\isacommand{show}\ {\isachardoublequote}{\isacharquery}P\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isachardoublequote}\ \isamarkupfalse%
+\isacommand{by}\ simp\isanewline
+\isamarkupfalse%
+\isacommand{qed}\isanewline
+\isanewline
+\isamarkupfalse%
+\isacommand{theorem}\ {\isachardoublequote}{\isadigit{2}}\ {\isacharasterisk}\ {\isacharparenleft}{\isasymSum}i\ {\isacharless}\ n\ {\isacharplus}\ {\isadigit{1}}{\isachardot}\ i{\isacharparenright}\ {\isacharequal}\ n\ {\isacharasterisk}\ {\isacharparenleft}n\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}{\isachardoublequote}\isanewline
+\isamarkupfalse%
+\isacommand{proof}\ {\isacharparenleft}induct\ n{\isacharparenright}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{case}\ {\isadigit{0}}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{then}\ \isamarkupfalse%
+\isacommand{show}\ {\isacharquery}case\ \isamarkupfalse%
+\isacommand{by}\ simp\isanewline
+\isamarkupfalse%
+\isacommand{next}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{case}\ Suc\isanewline
+\ \ \isamarkupfalse%
+\isacommand{then}\ \isamarkupfalse%
+\isacommand{show}\ {\isacharquery}case\ \isamarkupfalse%
+\isacommand{by}\ simp\isanewline
+\isamarkupfalse%
+\isacommand{qed}\isanewline
+\isanewline
+\isamarkupfalse%
+\isacommand{theorem}\ {\isachardoublequote}{\isadigit{2}}\ {\isacharasterisk}\ {\isacharparenleft}{\isasymSum}i\ {\isacharless}\ n\ {\isacharplus}\ {\isadigit{1}}{\isachardot}\ i{\isacharparenright}\ {\isacharequal}\ n\ {\isacharasterisk}\ {\isacharparenleft}n\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}{\isachardoublequote}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{by}\ {\isacharparenleft}induct\ n{\isacharparenright}\ simp{\isacharunderscore}all\isanewline
+\ \ \ \ \isanewline
+\isamarkupfalse%
+\isacommand{theorem}\ {\isachardoublequote}{\isadigit{2}}\ {\isacharasterisk}\ {\isacharparenleft}{\isasymSum}i\ {\isacharless}\ n\ {\isacharplus}\ {\isadigit{1}}{\isachardot}\ i{\isacharparenright}\ {\isacharequal}\ n\ {\isacharasterisk}\ {\isacharparenleft}n\ {\isacharplus}\ {\isadigit{1}}{\isacharparenright}{\isachardoublequote}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{apply}\ {\isacharparenleft}induct\ n{\isacharparenright}\isanewline
+\ \ \ \isamarkupfalse%
+\isacommand{apply}\ simp{\isacharunderscore}all\isanewline
+\ \ \isamarkupfalse%
+\isacommand{done}\isamarkupfalse%
+%
+\isamarkupchapter{Interaction and debugging%
+}
+\isamarkuptrue%
+%
+\isamarkupchapter{Calculational reasoning%
+}
+\isamarkuptrue%
+%
+\isamarkupchapter{Proof by cases and induction%
+}
+\isamarkuptrue%
+%
+\isamarkupchapter{General natural deduction%
+}
+\isamarkuptrue%
+%
+\isamarkupchapter{Example: FIXME%
+}
+\isamarkuptrue%
+%
+\isamarkupchapter{FIXME%
+}
+\isamarkuptrue%
+%
+\isamarkupsection{Formal document preparation%
+}
+\isamarkuptrue%
+%
+\isamarkupsubsection{Example%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+See this very document itself.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsection{Getting started%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\verb"isatool mkdir Test && isatool make"%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsection{Human-readable proof composition in Isar%
+}
+\isamarkuptrue%
+%
+\isamarkupsubsection{Getting started%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Claim a trivial goal in order to enter proof mode \isa{{\isasymdots}}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\ True\isanewline
+\isamarkupfalse%
+\isacommand{proof}\isamarkupfalse%
+%
+\begin{isamarkuptxt}%
+After the canonical initial refinement step we are left
+ within an \emph{proof body}.%
+\end{isamarkuptxt}%
+\isamarkuptrue%
+%
+\begin{isamarkuptxt}%
+Here we may augment the present local {proof context} as we
+ please.%
+\end{isamarkuptxt}%
+\ \ \isamarkuptrue%
+\isacommand{fix}\ something\isanewline
+\ \ \isamarkupfalse%
+\isacommand{assume}\ a{\isacharcolon}\ {\isachardoublequote}anything\ something{\isachardoublequote}\isamarkupfalse%
+%
+\begin{isamarkuptxt}%
+Note that the present configuration may be inspected by
+ several \emph{diagnostic commands}.%
+\end{isamarkuptxt}%
+\ \ \isamarkuptrue%
+\isacommand{term}\ something\ \ %
+\isamarkupcmt{\isa{something{\isasymColon}{\isacharprime}a}%
+}
+\isanewline
+\ \ \isamarkupfalse%
+\isacommand{term}\ anything\ \ %
+\isamarkupcmt{\isa{anything{\isasymColon}{\isacharprime}a\ {\isasymRightarrow}\ bool}%
+}
+\isanewline
+\ \ \isamarkupfalse%
+\isacommand{thm}\ a\ \ %
+\isamarkupcmt{\isa{anything\ something}%
+}
+\isamarkupfalse%
+%
+\begin{isamarkuptxt}%
+We may state local (auxiliary) results as well.%
+\end{isamarkuptxt}%
+\ \ \isamarkuptrue%
+\isacommand{have}\ True\ \isamarkupfalse%
+\isacommand{proof}\ \isamarkupfalse%
+\isacommand{qed}\isamarkupfalse%
+%
+\begin{isamarkuptxt}%
+We are now satisfied.%
+\end{isamarkuptxt}%
+\isamarkuptrue%
+\isacommand{qed}\isamarkupfalse%
+%
+\isamarkupsubsection{Calculational Reasoning%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Isar is mainly about Natural Deduction, but Calculational Reasoning
+ turns out as a simplified instance of that, so we demonstrate it
+ first.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsubsection{Transitive chains%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Technique: establish a chain of local facts, separated by \cmd{also}
+ and terminated by \cmd{finally}; another goal has to follow to point
+ out the final result.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\ {\isachardoublequote}x{\isadigit{1}}\ {\isacharequal}\ x{\isadigit{4}}{\isachardoublequote}\isanewline
+\isamarkupfalse%
+\isacommand{proof}\ {\isacharminus}\ \ %
+\isamarkupcmt{do nothing yet%
+}
+\isanewline
+\ \ \isamarkupfalse%
+\isacommand{have}\ {\isachardoublequote}x{\isadigit{1}}\ {\isacharequal}\ x{\isadigit{2}}{\isachardoublequote}\ \isamarkupfalse%
+\isacommand{sorry}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{also}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{have}\ {\isachardoublequote}x{\isadigit{2}}\ {\isacharequal}\ x{\isadigit{3}}{\isachardoublequote}\ \isamarkupfalse%
+\isacommand{sorry}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{also}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{have}\ {\isachardoublequote}x{\isadigit{3}}\ {\isacharequal}\ x{\isadigit{4}}{\isachardoublequote}\ \isamarkupfalse%
+\isacommand{sorry}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{finally}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{show}\ {\isachardoublequote}x{\isadigit{1}}\ {\isacharequal}\ x{\isadigit{4}}{\isachardoublequote}\ \isamarkupfalse%
+\isacommand{{\isachardot}}\isanewline
+\isamarkupfalse%
+\isacommand{qed}\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+This may be written more succinctly, using the special term binds
+ ``\isa{{\isasymdots}}'' (for the right-hand side of the last statement) and
+ ``\isa{{\isacharquery}thesis}'' (for the original claim at the head of the
+ proof).%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\ {\isachardoublequote}x{\isadigit{1}}\ {\isacharequal}\ x{\isadigit{4}}{\isachardoublequote}\isanewline
+\isamarkupfalse%
+\isacommand{proof}\ {\isacharminus}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{have}\ {\isachardoublequote}x{\isadigit{1}}\ {\isacharequal}\ x{\isadigit{2}}{\isachardoublequote}\ \isamarkupfalse%
+\isacommand{sorry}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{also}\ \isamarkupfalse%
+\isacommand{have}\ {\isachardoublequote}{\isasymdots}\ {\isacharequal}\ x{\isadigit{3}}{\isachardoublequote}\ \isamarkupfalse%
+\isacommand{sorry}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{also}\ \isamarkupfalse%
+\isacommand{have}\ {\isachardoublequote}{\isasymdots}\ {\isacharequal}\ x{\isadigit{4}}{\isachardoublequote}\ \isamarkupfalse%
+\isacommand{sorry}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{finally}\ \isamarkupfalse%
+\isacommand{show}\ {\isacharquery}thesis\ \isamarkupfalse%
+\isacommand{{\isachardot}}\isanewline
+\isamarkupfalse%
+\isacommand{qed}\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+The (implicit) forward-chaining steps involved in \cmd{also} and
+ \cmd{finally} are declared in the current context. The main library
+ of Isabelle/HOL already knows about (mixed) transitivities of \isa{{\isacharequal}}, \isa{{\isacharless}}, \isa{{\isasymle}} etc.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\ {\isachardoublequote}{\isacharparenleft}x{\isadigit{1}}{\isacharcolon}{\isacharcolon}nat{\isacharparenright}\ {\isacharless}\ x{\isadigit{6}}{\isachardoublequote}\isanewline
+\ \ %
+\isamarkupcmt{restriction to type \isa{nat} ensures that \isa{{\isacharless}} is really transitive%
+}
+\isanewline
+\isamarkupfalse%
+\isacommand{proof}\ {\isacharminus}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{have}\ {\isachardoublequote}x{\isadigit{1}}\ {\isacharless}\ x{\isadigit{2}}{\isachardoublequote}\ \isamarkupfalse%
+\isacommand{sorry}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{also}\ \isamarkupfalse%
+\isacommand{have}\ {\isachardoublequote}{\isasymdots}\ {\isasymle}\ x{\isadigit{3}}{\isachardoublequote}\ \isamarkupfalse%
+\isacommand{sorry}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{also}\ \isamarkupfalse%
+\isacommand{have}\ {\isachardoublequote}{\isasymdots}\ {\isacharequal}\ x{\isadigit{4}}{\isachardoublequote}\ \isamarkupfalse%
+\isacommand{sorry}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{also}\ \isamarkupfalse%
+\isacommand{have}\ {\isachardoublequote}{\isasymdots}\ {\isacharless}\ x{\isadigit{5}}{\isachardoublequote}\ \isamarkupfalse%
+\isacommand{sorry}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{also}\ \isamarkupfalse%
+\isacommand{have}\ {\isachardoublequote}{\isasymdots}\ {\isacharequal}\ x{\isadigit{6}}{\isachardoublequote}\ \isamarkupfalse%
+\isacommand{sorry}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{finally}\ \isamarkupfalse%
+\isacommand{show}\ {\isacharquery}thesis\ \isamarkupfalse%
+\isacommand{{\isachardot}}\isanewline
+\isamarkupfalse%
+\isacommand{qed}\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+We may also calculate on propositions.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\ True\isanewline
+\isamarkupfalse%
+\isacommand{proof}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{have}\ {\isachardoublequote}A\ {\isasymlongrightarrow}\ B\ {\isasymlongrightarrow}\ C{\isachardoublequote}\ \isamarkupfalse%
+\isacommand{sorry}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{also}\ \isamarkupfalse%
+\isacommand{have}\ A\ \isamarkupfalse%
+\isacommand{sorry}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{also}\ \isamarkupfalse%
+\isacommand{have}\ B\ \isamarkupfalse%
+\isacommand{sorry}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{finally}\ \isamarkupfalse%
+\isacommand{have}\ C\ \isamarkupfalse%
+\isacommand{{\isachardot}}\isanewline
+\isamarkupfalse%
+\isacommand{qed}\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+This is getting pretty close to Dijkstra's preferred proof style.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\ True\isanewline
+\isamarkupfalse%
+\isacommand{proof}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{have}\ {\isacharbrackleft}trans{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}{\isasymAnd}X\ Y\ Z{\isachardot}\ X\ {\isasymlongrightarrow}\ Y\ {\isasymLongrightarrow}\ Y\ {\isasymlongrightarrow}\ Z\ {\isasymLongrightarrow}\ X\ {\isasymlongrightarrow}\ Z{\isachardoublequote}\ \isamarkupfalse%
+\isacommand{by}\ rules\isanewline
+\ \ \isamarkupfalse%
+\isacommand{have}\ {\isachardoublequote}A\ {\isasymlongrightarrow}\ B{\isachardoublequote}\ \isamarkupfalse%
+\isacommand{sorry}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{also}\ \isamarkupfalse%
+\isacommand{have}\ {\isachardoublequote}{\isasymdots}\ {\isasymlongrightarrow}\ C{\isachardoublequote}\ \isamarkupfalse%
+\isacommand{sorry}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{also}\ \isamarkupfalse%
+\isacommand{have}\ {\isachardoublequote}{\isasymdots}\ {\isasymlongrightarrow}\ D{\isachardoublequote}\ \isamarkupfalse%
+\isacommand{sorry}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{finally}\ \isamarkupfalse%
+\isacommand{have}\ {\isachardoublequote}A\ {\isasymlongrightarrow}\ D{\isachardoublequote}\ \isamarkupfalse%
+\isacommand{{\isachardot}}\isanewline
+\isamarkupfalse%
+\isacommand{qed}\isamarkupfalse%
+%
+\isamarkupsubsubsection{Degenerate calculations and bigstep reasoning%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Instead of \cmd{also}/\cmd{finally} we may use degenerative steps
+ \cmd{moreover}/\cmd{ultimately} to accumulate facts, without
+ applying any forward rules yet.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\ True\isanewline
+\isamarkupfalse%
+\isacommand{proof}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{have}\ A\ \isamarkupfalse%
+\isacommand{sorry}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{moreover}\ \isamarkupfalse%
+\isacommand{have}\ B\ \isamarkupfalse%
+\isacommand{sorry}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{moreover}\ \isamarkupfalse%
+\isacommand{have}\ C\ \isamarkupfalse%
+\isacommand{sorry}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{ultimately}\ \isamarkupfalse%
+\isacommand{have}\ A\ \isakeyword{and}\ B\ \isakeyword{and}\ C\ \isamarkupfalse%
+\isacommand{{\isachardot}}\ \ %
+\isamarkupcmt{Pretty obvious, right?%
+}
+\isanewline
+\isamarkupfalse%
+\isacommand{qed}\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+Both kinds of calculational elements may be used together.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\ True\isanewline
+\isamarkupfalse%
+\isacommand{proof}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{assume}\ reasoning{\isacharunderscore}pattern\ {\isacharbrackleft}trans{\isacharbrackright}{\isacharcolon}\ {\isachardoublequote}A\ {\isasymLongrightarrow}\ B\ {\isasymLongrightarrow}\ C\ {\isasymLongrightarrow}\ D{\isachardoublequote}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{have}\ A\ \isamarkupfalse%
+\isacommand{sorry}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{moreover}\ \isamarkupfalse%
+\isacommand{have}\ B\ \isamarkupfalse%
+\isacommand{sorry}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{moreover}\ \isamarkupfalse%
+\isacommand{have}\ C\ \isamarkupfalse%
+\isacommand{sorry}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{finally}\ \isamarkupfalse%
+\isacommand{have}\ D\ \isamarkupfalse%
+\isacommand{{\isachardot}}\isanewline
+\isamarkupfalse%
+\isacommand{qed}\isamarkupfalse%
+%
+\isamarkupsubsection{Natural deduction%
+}
+\isamarkuptrue%
+%
+\isamarkupsubsubsection{Primitive patterns%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+The default theory context admits to perform canonical single-step
+ reasoning (similar to Gentzen) without further ado.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\ True\isanewline
+\isamarkupfalse%
+\isacommand{proof}\isanewline
+\isanewline
+\ \ \isamarkupfalse%
+\isacommand{have}\ True\ \isamarkupfalse%
+\isacommand{{\isachardot}{\isachardot}}\isanewline
+\isanewline
+\ \ \isamarkupfalse%
+\isacommand{{\isacharbraceleft}}\ \isamarkupfalse%
+\isacommand{assume}\ False\isanewline
+\ \ \ \ \isamarkupfalse%
+\isacommand{then}\ \isamarkupfalse%
+\isacommand{have}\ C\ \isamarkupfalse%
+\isacommand{{\isachardot}{\isachardot}}\ \isamarkupfalse%
+\isacommand{{\isacharbraceright}}\isanewline
+\isanewline
+\ \ \isamarkupfalse%
+\isacommand{have}\ {\isachardoublequote}{\isasymnot}\ A{\isachardoublequote}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{proof}\isanewline
+\ \ \ \ \isamarkupfalse%
+\isacommand{assume}\ A\isanewline
+\ \ \ \ \isamarkupfalse%
+\isacommand{show}\ False\ \isamarkupfalse%
+\isacommand{sorry}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{qed}\isanewline
+\isanewline
+\ \ \isamarkupfalse%
+\isacommand{{\isacharbraceleft}}\ \isamarkupfalse%
+\isacommand{assume}\ {\isachardoublequote}{\isasymnot}\ A{\isachardoublequote}\ \isakeyword{and}\ A\isanewline
+\ \ \ \ \isamarkupfalse%
+\isacommand{then}\ \isamarkupfalse%
+\isacommand{have}\ C\ \isamarkupfalse%
+\isacommand{{\isachardot}{\isachardot}}\ \isamarkupfalse%
+\isacommand{{\isacharbraceright}}\isanewline
+\isanewline
+\ \ \isamarkupfalse%
+\isacommand{have}\ {\isachardoublequote}A\ {\isasymlongrightarrow}\ B{\isachardoublequote}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{proof}\isanewline
+\ \ \ \ \isamarkupfalse%
+\isacommand{assume}\ A\isanewline
+\ \ \ \ \isamarkupfalse%
+\isacommand{show}\ B\ \isamarkupfalse%
+\isacommand{sorry}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{qed}\isanewline
+\isanewline
+\ \ \isamarkupfalse%
+\isacommand{{\isacharbraceleft}}\ \isamarkupfalse%
+\isacommand{assume}\ {\isachardoublequote}A\ {\isasymlongrightarrow}\ B{\isachardoublequote}\ \isakeyword{and}\ A\isanewline
+\ \ \ \ \isamarkupfalse%
+\isacommand{then}\ \isamarkupfalse%
+\isacommand{have}\ B\ \isamarkupfalse%
+\isacommand{{\isachardot}{\isachardot}}\ \isamarkupfalse%
+\isacommand{{\isacharbraceright}}\isanewline
+\isanewline
+\ \ \isamarkupfalse%
+\isacommand{have}\ {\isachardoublequote}A\ {\isasymand}\ B{\isachardoublequote}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{proof}\isanewline
+\ \ \ \ \isamarkupfalse%
+\isacommand{show}\ A\ \isamarkupfalse%
+\isacommand{sorry}\isanewline
+\ \ \ \ \isamarkupfalse%
+\isacommand{show}\ B\ \isamarkupfalse%
+\isacommand{sorry}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{qed}\isanewline
+\isanewline
+\ \ \isamarkupfalse%
+\isacommand{{\isacharbraceleft}}\ \isamarkupfalse%
+\isacommand{assume}\ {\isachardoublequote}A\ {\isasymand}\ B{\isachardoublequote}\isanewline
+\ \ \ \ \isamarkupfalse%
+\isacommand{then}\ \isamarkupfalse%
+\isacommand{have}\ A\ \isamarkupfalse%
+\isacommand{{\isachardot}{\isachardot}}\ \isamarkupfalse%
+\isacommand{{\isacharbraceright}}\isanewline
+\isanewline
+\ \ \isamarkupfalse%
+\isacommand{{\isacharbraceleft}}\ \isamarkupfalse%
+\isacommand{assume}\ {\isachardoublequote}A\ {\isasymand}\ B{\isachardoublequote}\isanewline
+\ \ \ \ \isamarkupfalse%
+\isacommand{then}\ \isamarkupfalse%
+\isacommand{have}\ B\ \isamarkupfalse%
+\isacommand{{\isachardot}{\isachardot}}\ \isamarkupfalse%
+\isacommand{{\isacharbraceright}}\isanewline
+\isanewline
+\ \ \isamarkupfalse%
+\isacommand{{\isacharbraceleft}}\ \isamarkupfalse%
+\isacommand{assume}\ A\isanewline
+\ \ \ \ \isamarkupfalse%
+\isacommand{then}\ \isamarkupfalse%
+\isacommand{have}\ {\isachardoublequote}A\ {\isasymor}\ B{\isachardoublequote}\ \isamarkupfalse%
+\isacommand{{\isachardot}{\isachardot}}\ \isamarkupfalse%
+\isacommand{{\isacharbraceright}}\isanewline
+\isanewline
+\ \ \isamarkupfalse%
+\isacommand{{\isacharbraceleft}}\ \isamarkupfalse%
+\isacommand{assume}\ B\isanewline
+\ \ \ \ \isamarkupfalse%
+\isacommand{then}\ \isamarkupfalse%
+\isacommand{have}\ {\isachardoublequote}A\ {\isasymor}\ B{\isachardoublequote}\ \isamarkupfalse%
+\isacommand{{\isachardot}{\isachardot}}\ \isamarkupfalse%
+\isacommand{{\isacharbraceright}}\isanewline
+\isanewline
+\ \ \isamarkupfalse%
+\isacommand{{\isacharbraceleft}}\ \isamarkupfalse%
+\isacommand{assume}\ {\isachardoublequote}A\ {\isasymor}\ B{\isachardoublequote}\isanewline
+\ \ \ \ \isamarkupfalse%
+\isacommand{then}\ \isamarkupfalse%
+\isacommand{have}\ C\isanewline
+\ \ \ \ \isamarkupfalse%
+\isacommand{proof}\isanewline
+\ \ \ \ \ \ \isamarkupfalse%
+\isacommand{assume}\ A\isanewline
+\ \ \ \ \ \ \isamarkupfalse%
+\isacommand{then}\ \isamarkupfalse%
+\isacommand{show}\ {\isacharquery}thesis\ \isamarkupfalse%
+\isacommand{sorry}\isanewline
+\ \ \ \ \isamarkupfalse%
+\isacommand{next}\isanewline
+\ \ \ \ \ \ \isamarkupfalse%
+\isacommand{assume}\ B\isanewline
+\ \ \ \ \ \ \isamarkupfalse%
+\isacommand{then}\ \isamarkupfalse%
+\isacommand{show}\ {\isacharquery}thesis\ \isamarkupfalse%
+\isacommand{sorry}\isanewline
+\ \ \ \ \isamarkupfalse%
+\isacommand{qed}\ \isamarkupfalse%
+\isacommand{{\isacharbraceright}}\isanewline
+\isanewline
+\ \ \isamarkupfalse%
+\isacommand{have}\ {\isachardoublequote}{\isasymforall}x{\isachardot}\ P\ x{\isachardoublequote}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{proof}\isanewline
+\ \ \ \ \isamarkupfalse%
+\isacommand{fix}\ x\isanewline
+\ \ \ \ \isamarkupfalse%
+\isacommand{show}\ {\isachardoublequote}P\ x{\isachardoublequote}\ \isamarkupfalse%
+\isacommand{sorry}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{qed}\isanewline
+\isanewline
+\ \ \isamarkupfalse%
+\isacommand{{\isacharbraceleft}}\ \isamarkupfalse%
+\isacommand{assume}\ {\isachardoublequote}{\isasymforall}x{\isachardot}\ P\ x{\isachardoublequote}\isanewline
+\ \ \ \ \isamarkupfalse%
+\isacommand{then}\ \isamarkupfalse%
+\isacommand{have}\ {\isachardoublequote}P\ t{\isachardoublequote}\ \isamarkupfalse%
+\isacommand{{\isachardot}{\isachardot}}\ \isamarkupfalse%
+\isacommand{{\isacharbraceright}}\isanewline
+\isanewline
+\ \ \isamarkupfalse%
+\isacommand{have}\ {\isachardoublequote}{\isasymexists}x{\isachardot}\ P\ x{\isachardoublequote}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{proof}\isanewline
+\ \ \ \ \isamarkupfalse%
+\isacommand{show}\ {\isachardoublequote}P\ t{\isachardoublequote}\ \isamarkupfalse%
+\isacommand{sorry}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{qed}\isanewline
+\ \ \isanewline
+\ \ \isamarkupfalse%
+\isacommand{{\isacharbraceleft}}\ \isamarkupfalse%
+\isacommand{assume}\ {\isachardoublequote}{\isasymexists}x{\isachardot}\ P\ x{\isachardoublequote}\isanewline
+\ \ \ \ \isamarkupfalse%
+\isacommand{then}\ \isamarkupfalse%
+\isacommand{obtain}\ x\ \isakeyword{where}\ {\isachardoublequote}P\ x{\isachardoublequote}\ \isamarkupfalse%
+\isacommand{{\isachardot}{\isachardot}}\isanewline
+\ \ \ \ \isamarkupfalse%
+\isacommand{note}\ nothing\ \ %
+\isamarkupcmt{relax%
+}
+\ \isamarkupfalse%
+\isacommand{{\isacharbraceright}}\isanewline
+\isamarkupfalse%
+\isacommand{qed}\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+Certainly, this works with derived rules for defined concepts in the
+ same manner. E.g.\ use the simple-typed set-theory of Isabelle/HOL.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{lemma}\ True\isanewline
+\isamarkupfalse%
+\isacommand{proof}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{have}\ {\isachardoublequote}y\ {\isasymin}\ {\isacharparenleft}{\isasymInter}x\ {\isasymin}\ A{\isachardot}\ B\ x{\isacharparenright}{\isachardoublequote}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{proof}\isanewline
+\ \ \ \ \isamarkupfalse%
+\isacommand{fix}\ x\isanewline
+\ \ \ \ \isamarkupfalse%
+\isacommand{assume}\ {\isachardoublequote}x\ {\isasymin}\ A{\isachardoublequote}\isanewline
+\ \ \ \ \isamarkupfalse%
+\isacommand{show}\ {\isachardoublequote}y\ {\isasymin}\ B\ x{\isachardoublequote}\ \isamarkupfalse%
+\isacommand{sorry}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{qed}\isanewline
+\isanewline
+\ \ \isamarkupfalse%
+\isacommand{have}\ {\isachardoublequote}y\ {\isasymin}\ {\isacharparenleft}{\isasymUnion}x\ {\isasymin}\ A{\isachardot}\ B\ x{\isacharparenright}{\isachardoublequote}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{proof}\isanewline
+\ \ \ \ \isamarkupfalse%
+\isacommand{show}\ {\isachardoublequote}a\ {\isasymin}\ A{\isachardoublequote}\ \isamarkupfalse%
+\isacommand{sorry}\isanewline
+\ \ \ \ \isamarkupfalse%
+\isacommand{show}\ {\isachardoublequote}y\ {\isasymin}\ B\ a{\isachardoublequote}\ \isamarkupfalse%
+\isacommand{sorry}\isanewline
+\ \ \isamarkupfalse%
+\isacommand{qed}\isanewline
+\isamarkupfalse%
+\isacommand{qed}\isamarkupfalse%
+%
+\isamarkupsubsubsection{Variations in structure%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+The design of the Isar language takes the user seriously%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isamarkupsubsubsection{Generalized elimination%
+}
+\isamarkuptrue%
+%
+\isamarkupsubsubsection{Scalable cases and induction%
+}
+\isamarkuptrue%
+%
+\isamarkupsection{Assimilating the old tactical style%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Improper commands:
+ Observation: every Isar subproof may start with a ``script'' of%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isamarkupfalse%
+\end{isabellebody}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarTut/Tutorial/document/isabelle.sty Thu Jun 06 15:34:52 2002 +0200
@@ -0,0 +1,157 @@
+%%
+%% Author: Markus Wenzel, TU Muenchen
+%% License: GPL (GNU GENERAL PUBLIC LICENSE)
+%%
+%% macros for Isabelle generated LaTeX output
+%%
+
+%%% Simple document preparation (based on theory token language and symbols)
+
+% isabelle environments
+
+\newcommand{\isabellecontext}{UNKNOWN}
+
+\newcommand{\isastyle}{\small\tt\slshape}
+\newcommand{\isastyleminor}{\small\tt\slshape}
+\newcommand{\isastylescript}{\footnotesize\tt\slshape}
+\newcommand{\isastyletext}{\normalsize\rm}
+\newcommand{\isastyletxt}{\rm}
+\newcommand{\isastylecmt}{\rm}
+
+%symbol markup -- \emph achieves decent spacing via italic corrections
+\newcommand{\isamath}[1]{\emph{$#1$}}
+\newcommand{\isatext}[1]{\emph{#1}}
+\newcommand{\isascriptstyle}{\def\isamath##1{##1}\def\isatext##1{\mbox{\isastylescript##1}}}
+\newcommand{\isactrlsub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
+\newcommand{\isactrlsup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
+\newcommand{\isactrlbold}[1]{{\bfseries\upshape\boldmath#1}}
+
+\newdimen\isa@parindent\newdimen\isa@parskip
+
+\newenvironment{isabellebody}{%
+\isamarkuptrue\par%
+\isa@parindent\parindent\parindent0pt%
+\isa@parskip\parskip\parskip0pt%
+\isastyle}{\par}
+
+\newenvironment{isabelle}
+{\begin{trivlist}\begin{isabellebody}\item\relax}
+{\end{isabellebody}\end{trivlist}}
+
+\newcommand{\isa}[1]{\emph{\isastyleminor #1}}
+
+\newcommand{\isaindent}[1]{\hphantom{#1}}
+\newcommand{\isanewline}{\mbox{}\\\mbox{}}
+\newcommand{\isadigit}[1]{#1}
+
+\chardef\isacharbang=`\!
+\chardef\isachardoublequote=`\"
+\chardef\isacharhash=`\#
+\chardef\isachardollar=`\$
+\chardef\isacharpercent=`\%
+\chardef\isacharampersand=`\&
+\chardef\isacharprime=`\'
+\chardef\isacharparenleft=`\(
+\chardef\isacharparenright=`\)
+\chardef\isacharasterisk=`\*
+\chardef\isacharplus=`\+
+\chardef\isacharcomma=`\,
+\chardef\isacharminus=`\-
+\chardef\isachardot=`\.
+\chardef\isacharslash=`\/
+\chardef\isacharcolon=`\:
+\chardef\isacharsemicolon=`\;
+\chardef\isacharless=`\<
+\chardef\isacharequal=`\=
+\chardef\isachargreater=`\>
+\chardef\isacharquery=`\?
+\chardef\isacharat=`\@
+\chardef\isacharbrackleft=`\[
+\chardef\isacharbackslash=`\\
+\chardef\isacharbrackright=`\]
+\chardef\isacharcircum=`\^
+\chardef\isacharunderscore=`\_
+\chardef\isacharbackquote=`\`
+\chardef\isacharbraceleft=`\{
+\chardef\isacharbar=`\|
+\chardef\isacharbraceright=`\}
+\chardef\isachartilde=`\~
+
+
+% keyword and section markup
+
+\newcommand{\isakeywordcharunderscore}{\_}
+\newcommand{\isakeyword}[1]
+{\emph{\bf\def\isachardot{.}\def\isacharunderscore{\isakeywordcharunderscore}%
+\def\isacharbraceleft{\{}\def\isacharbraceright{\}}#1}}
+\newcommand{\isacommand}[1]{\isakeyword{#1}}
+
+\newcommand{\isamarkupheader}[1]{\section{#1}}
+\newcommand{\isamarkupchapter}[1]{\chapter{#1}}
+\newcommand{\isamarkupsection}[1]{\section{#1}}
+\newcommand{\isamarkupsubsection}[1]{\subsection{#1}}
+\newcommand{\isamarkupsubsubsection}[1]{\subsubsection{#1}}
+\newcommand{\isamarkupsect}[1]{\section{#1}}
+\newcommand{\isamarkupsubsect}[1]{\subsection{#1}}
+\newcommand{\isamarkupsubsubsect}[1]{\subsubsection{#1}}
+
+\newif\ifisamarkup
+\newcommand{\isabeginpar}{\par\ifisamarkup\relax\else\medskip\fi}
+\newcommand{\isaendpar}{\par\medskip}
+\newenvironment{isapar}{\parindent\isa@parindent\parskip\isa@parskip\isabeginpar}{\isaendpar}
+\newenvironment{isamarkuptext}{\isastyletext\begin{isapar}}{\end{isapar}}
+\newenvironment{isamarkuptxt}{\isastyletxt\begin{isapar}}{\end{isapar}}
+\newcommand{\isamarkupcmt}[1]{{\isastylecmt--- #1}}
+
+
+% alternative styles
+
+\newcommand{\isabellestyle}{}
+\def\isabellestyle#1{\csname isabellestyle#1\endcsname}
+
+\newcommand{\isabellestylett}{%
+\renewcommand{\isastyle}{\small\tt}%
+\renewcommand{\isastyleminor}{\small\tt}%
+\renewcommand{\isastylescript}{\footnotesize\tt}%
+}
+\newcommand{\isabellestyleit}{%
+\renewcommand{\isastyle}{\small\it}%
+\renewcommand{\isastyleminor}{\it}%
+\renewcommand{\isastylescript}{\footnotesize\it}%
+\renewcommand{\isakeywordcharunderscore}{\mbox{-}}%
+\renewcommand{\isacharbang}{\isamath{!}}%
+\renewcommand{\isachardoublequote}{}%
+\renewcommand{\isacharhash}{\isamath{\#}}%
+\renewcommand{\isachardollar}{\isamath{\$}}%
+\renewcommand{\isacharpercent}{\isamath{\%}}%
+\renewcommand{\isacharampersand}{\isamath{\&}}%
+\renewcommand{\isacharprime}{\isamath{\mskip2mu{'}\mskip-2mu}}%
+\renewcommand{\isacharparenleft}{\isamath{(}}%
+\renewcommand{\isacharparenright}{\isamath{)}}%
+\renewcommand{\isacharasterisk}{\isamath{*}}%
+\renewcommand{\isacharplus}{\isamath{+}}%
+\renewcommand{\isacharcomma}{\isamath{\mathord,}}%
+\renewcommand{\isacharminus}{\isamath{-}}%
+\renewcommand{\isachardot}{\isamath{\mathord.}}%
+\renewcommand{\isacharslash}{\isamath{/}}%
+\renewcommand{\isacharcolon}{\isamath{\mathord:}}%
+\renewcommand{\isacharsemicolon}{\isamath{\mathord;}}%
+\renewcommand{\isacharless}{\isamath{<}}%
+\renewcommand{\isacharequal}{\isamath{=}}%
+\renewcommand{\isachargreater}{\isamath{>}}%
+\renewcommand{\isacharat}{\isamath{@}}%
+\renewcommand{\isacharbrackleft}{\isamath{[}}%
+\renewcommand{\isacharbrackright}{\isamath{]}}%
+\renewcommand{\isacharunderscore}{\mbox{-}}%
+\renewcommand{\isacharbraceleft}{\isamath{\{}}%
+\renewcommand{\isacharbar}{\isamath{\mid}}%
+\renewcommand{\isacharbraceright}{\isamath{\}}}%
+\renewcommand{\isachartilde}{\isamath{{}\sp{\sim}}}%
+}
+
+\newcommand{\isabellestylesl}{%
+\isabellestyleit%
+\renewcommand{\isastyle}{\small\sl}%
+\renewcommand{\isastyleminor}{\sl}%
+\renewcommand{\isastylescript}{\footnotesize\sl}%
+}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/IsarTut/Tutorial/document/isabellesym.sty Thu Jun 06 15:34:52 2002 +0200
@@ -0,0 +1,354 @@
+%%
+%% Author: Markus Wenzel, TU Muenchen
+%% License: GPL (GNU GENERAL PUBLIC LICENSE)
+%%
+%% definitions of standard Isabelle symbols
+%%
+
+% symbol definitions
+
+\newcommand{\isasymzero}{\isatext{\textzerooldstyle}} %requires textcomp
+\newcommand{\isasymone}{\isatext{\textoneoldstyle}} %requires textcomp
+\newcommand{\isasymtwo}{\isatext{\texttwooldstyle}} %requires textcomp
+\newcommand{\isasymthree}{\isatext{\textthreeoldstyle}} %requires textcomp
+\newcommand{\isasymfour}{\isatext{\textfouroldstyle}} %requires textcomp
+\newcommand{\isasymfive}{\isatext{\textfiveoldstyle}} %requires textcomp
+\newcommand{\isasymsix}{\isatext{\textsixoldstyle}} %requires textcomp
+\newcommand{\isasymseven}{\isatext{\textsevenoldstyle}} %requires textcomp
+\newcommand{\isasymeight}{\isatext{\texteightoldstyle}} %requires textcomp
+\newcommand{\isasymnine}{\isatext{\textnineoldstyle}} %requires textcomp
+\newcommand{\isasymA}{\isamath{\mathcal{A}}}
+\newcommand{\isasymB}{\isamath{\mathcal{B}}}
+\newcommand{\isasymC}{\isamath{\mathcal{C}}}
+\newcommand{\isasymD}{\isamath{\mathcal{D}}}
+\newcommand{\isasymE}{\isamath{\mathcal{E}}}
+\newcommand{\isasymF}{\isamath{\mathcal{F}}}
+\newcommand{\isasymG}{\isamath{\mathcal{G}}}
+\newcommand{\isasymH}{\isamath{\mathcal{H}}}
+\newcommand{\isasymI}{\isamath{\mathcal{I}}}
+\newcommand{\isasymJ}{\isamath{\mathcal{J}}}
+\newcommand{\isasymK}{\isamath{\mathcal{K}}}
+\newcommand{\isasymL}{\isamath{\mathcal{L}}}
+\newcommand{\isasymM}{\isamath{\mathcal{M}}}
+\newcommand{\isasymN}{\isamath{\mathcal{N}}}
+\newcommand{\isasymO}{\isamath{\mathcal{O}}}
+\newcommand{\isasymP}{\isamath{\mathcal{P}}}
+\newcommand{\isasymQ}{\isamath{\mathcal{Q}}}
+\newcommand{\isasymR}{\isamath{\mathcal{R}}}
+\newcommand{\isasymS}{\isamath{\mathcal{S}}}
+\newcommand{\isasymT}{\isamath{\mathcal{T}}}
+\newcommand{\isasymU}{\isamath{\mathcal{U}}}
+\newcommand{\isasymV}{\isamath{\mathcal{V}}}
+\newcommand{\isasymW}{\isamath{\mathcal{W}}}
+\newcommand{\isasymX}{\isamath{\mathcal{X}}}
+\newcommand{\isasymY}{\isamath{\mathcal{Y}}}
+\newcommand{\isasymZ}{\isamath{\mathcal{Z}}}
+\newcommand{\isasyma}{\isamath{\mathrm{a}}}
+\newcommand{\isasymb}{\isamath{\mathrm{b}}}
+\newcommand{\isasymc}{\isamath{\mathrm{c}}}
+\newcommand{\isasymd}{\isamath{\mathrm{d}}}
+\newcommand{\isasyme}{\isamath{\mathrm{e}}}
+\newcommand{\isasymf}{\isamath{\mathrm{f}}}
+\newcommand{\isasymg}{\isamath{\mathrm{g}}}
+\newcommand{\isasymh}{\isamath{\mathrm{h}}}
+\newcommand{\isasymi}{\isamath{\mathrm{i}}}
+\newcommand{\isasymj}{\isamath{\mathrm{j}}}
+\newcommand{\isasymk}{\isamath{\mathrm{k}}}
+\newcommand{\isasyml}{\isamath{\mathrm{l}}}
+\newcommand{\isasymm}{\isamath{\mathrm{m}}}
+\newcommand{\isasymn}{\isamath{\mathrm{n}}}
+\newcommand{\isasymo}{\isamath{\mathrm{o}}}
+\newcommand{\isasymp}{\isamath{\mathrm{p}}}
+\newcommand{\isasymq}{\isamath{\mathrm{q}}}
+\newcommand{\isasymr}{\isamath{\mathrm{r}}}
+\newcommand{\isasyms}{\isamath{\mathrm{s}}}
+\newcommand{\isasymt}{\isamath{\mathrm{t}}}
+\newcommand{\isasymu}{\isamath{\mathrm{u}}}
+\newcommand{\isasymv}{\isamath{\mathrm{v}}}
+\newcommand{\isasymw}{\isamath{\mathrm{w}}}
+\newcommand{\isasymx}{\isamath{\mathrm{x}}}
+\newcommand{\isasymy}{\isamath{\mathrm{y}}}
+\newcommand{\isasymz}{\isamath{\mathrm{z}}}
+\newcommand{\isasymAA}{\isamath{\mathfrak{A}}} %requires eufrak
+\newcommand{\isasymBB}{\isamath{\mathfrak{B}}} %requires eufrak
+\newcommand{\isasymCC}{\isamath{\mathfrak{C}}} %requires eufrak
+\newcommand{\isasymDD}{\isamath{\mathfrak{D}}} %requires eufrak
+\newcommand{\isasymEE}{\isamath{\mathfrak{E}}} %requires eufrak
+\newcommand{\isasymFF}{\isamath{\mathfrak{F}}} %requires eufrak
+\newcommand{\isasymGG}{\isamath{\mathfrak{G}}} %requires eufrak
+\newcommand{\isasymHH}{\isamath{\mathfrak{H}}} %requires eufrak
+\newcommand{\isasymII}{\isamath{\mathfrak{I}}} %requires eufrak
+\newcommand{\isasymJJ}{\isamath{\mathfrak{J}}} %requires eufrak
+\newcommand{\isasymKK}{\isamath{\mathfrak{K}}} %requires eufrak
+\newcommand{\isasymLL}{\isamath{\mathfrak{L}}} %requires eufrak
+\newcommand{\isasymMM}{\isamath{\mathfrak{M}}} %requires eufrak
+\newcommand{\isasymNN}{\isamath{\mathfrak{N}}} %requires eufrak
+\newcommand{\isasymOO}{\isamath{\mathfrak{O}}} %requires eufrak
+\newcommand{\isasymPP}{\isamath{\mathfrak{P}}} %requires eufrak
+\newcommand{\isasymQQ}{\isamath{\mathfrak{Q}}} %requires eufrak
+\newcommand{\isasymRR}{\isamath{\mathfrak{R}}} %requires eufrak
+\newcommand{\isasymSS}{\isamath{\mathfrak{S}}} %requires eufrak
+\newcommand{\isasymTT}{\isamath{\mathfrak{T}}} %requires eufrak
+\newcommand{\isasymUU}{\isamath{\mathfrak{U}}} %requires eufrak
+\newcommand{\isasymVV}{\isamath{\mathfrak{V}}} %requires eufrak
+\newcommand{\isasymWW}{\isamath{\mathfrak{W}}} %requires eufrak
+\newcommand{\isasymXX}{\isamath{\mathfrak{X}}} %requires eufrak
+\newcommand{\isasymYY}{\isamath{\mathfrak{Y}}} %requires eufrak
+\newcommand{\isasymZZ}{\isamath{\mathfrak{Z}}} %requires eufrak
+\newcommand{\isasymaa}{\isamath{\mathfrak{a}}} %requires eufrak
+\newcommand{\isasymbb}{\isamath{\mathfrak{b}}} %requires eufrak
+\newcommand{\isasymcc}{\isamath{\mathfrak{c}}} %requires eufrak
+\newcommand{\isasymdd}{\isamath{\mathfrak{d}}} %requires eufrak
+\newcommand{\isasymee}{\isamath{\mathfrak{e}}} %requires eufrak
+\newcommand{\isasymff}{\isamath{\mathfrak{f}}} %requires eufrak
+\newcommand{\isasymgg}{\isamath{\mathfrak{g}}} %requires eufrak
+\newcommand{\isasymhh}{\isamath{\mathfrak{h}}} %requires eufrak
+\newcommand{\isasymii}{\isamath{\mathfrak{i}}} %requires eufrak
+\newcommand{\isasymjj}{\isamath{\mathfrak{j}}} %requires eufrak
+\newcommand{\isasymkk}{\isamath{\mathfrak{k}}} %requires eufrak
+\newcommand{\isasymll}{\isamath{\mathfrak{l}}} %requires eufrak
+\newcommand{\isasymmm}{\isamath{\mathfrak{m}}} %requires eufrak
+\newcommand{\isasymnn}{\isamath{\mathfrak{n}}} %requires eufrak
+\newcommand{\isasymoo}{\isamath{\mathfrak{o}}} %requires eufrak
+\newcommand{\isasympp}{\isamath{\mathfrak{p}}} %requires eufrak
+\newcommand{\isasymqq}{\isamath{\mathfrak{q}}} %requires eufrak
+\newcommand{\isasymrr}{\isamath{\mathfrak{r}}} %requires eufrak
+\newcommand{\isasymss}{\isamath{\mathfrak{s}}} %requires eufrak
+\newcommand{\isasymtt}{\isamath{\mathfrak{t}}} %requires eufrak
+\newcommand{\isasymuu}{\isamath{\mathfrak{u}}} %requires eufrak
+\newcommand{\isasymvv}{\isamath{\mathfrak{v}}} %requires eufrak
+\newcommand{\isasymww}{\isamath{\mathfrak{w}}} %requires eufrak
+\newcommand{\isasymxx}{\isamath{\mathfrak{x}}} %requires eufrak
+\newcommand{\isasymyy}{\isamath{\mathfrak{y}}} %requires eufrak
+\newcommand{\isasymzz}{\isamath{\mathfrak{z}}} %requires eufrak
+\newcommand{\isasymalpha}{\isamath{\alpha}}
+\newcommand{\isasymbeta}{\isamath{\beta}}
+\newcommand{\isasymgamma}{\isamath{\gamma}}
+\newcommand{\isasymdelta}{\isamath{\delta}}
+\newcommand{\isasymepsilon}{\isamath{\varepsilon}}
+\newcommand{\isasymzeta}{\isamath{\zeta}}
+\newcommand{\isasymeta}{\isamath{\eta}}
+\newcommand{\isasymtheta}{\isamath{\vartheta}}
+\newcommand{\isasymiota}{\isamath{\iota}}
+\newcommand{\isasymkappa}{\isamath{\kappa}}
+\newcommand{\isasymlambda}{\isamath{\lambda}}
+\newcommand{\isasymmu}{\isamath{\mu}}
+\newcommand{\isasymnu}{\isamath{\nu}}
+\newcommand{\isasymxi}{\isamath{\xi}}
+\newcommand{\isasympi}{\isamath{\pi}}
+\newcommand{\isasymrho}{\isamath{\varrho}}
+\newcommand{\isasymsigma}{\isamath{\sigma}}
+\newcommand{\isasymtau}{\isamath{\tau}}
+\newcommand{\isasymupsilon}{\isamath{\upsilon}}
+\newcommand{\isasymphi}{\isamath{\varphi}}
+\newcommand{\isasymchi}{\isamath{\chi}}
+\newcommand{\isasympsi}{\isamath{\psi}}
+\newcommand{\isasymomega}{\isamath{\omega}}
+\newcommand{\isasymGamma}{\isamath{\Gamma}}
+\newcommand{\isasymDelta}{\isamath{\Delta}}
+\newcommand{\isasymTheta}{\isamath{\Theta}}
+\newcommand{\isasymLambda}{\isamath{\Lambda}}
+\newcommand{\isasymXi}{\isamath{\Xi}}
+\newcommand{\isasymPi}{\isamath{\Pi}}
+\newcommand{\isasymSigma}{\isamath{\Sigma}}
+\newcommand{\isasymUpsilon}{\isamath{\Upsilon}}
+\newcommand{\isasymPhi}{\isamath{\Phi}}
+\newcommand{\isasymPsi}{\isamath{\Psi}}
+\newcommand{\isasymOmega}{\isamath{\Omega}}
+\newcommand{\isasymbool}{\isamath{\mathrm{I}\mkern-3.8mu\mathrm{B}}}
+\newcommand{\isasymcomplex}{\isamath{\mathrm{C}\mkern-15mu{\phantom{\mathrm{t}}\vrule}\mkern9mu}}
+\newcommand{\isasymnat}{\isamath{\mathrm{I}\mkern-3.8mu\mathrm{N}}}
+\newcommand{\isasymrat}{\isamath{\mathrm{Q}\mkern-16mu{\phantom{\mathrm{t}}\vrule}\mkern10mu}}
+\newcommand{\isasymreal}{\isamath{\mathrm{I}\mkern-3.8mu\mathrm{R}}}
+\newcommand{\isasymint}{\isamath{\mathsf{Z}\mkern-7.5mu\mathsf{Z}}}
+\newcommand{\isasymleftarrow}{\isamath{\leftarrow}}
+\newcommand{\isasymlongleftarrow}{\isamath{\longleftarrow}}
+\newcommand{\isasymrightarrow}{\isamath{\rightarrow}}
+\newcommand{\isasymlongrightarrow}{\isamath{\longrightarrow}}
+\newcommand{\isasymLeftarrow}{\isamath{\Leftarrow}}
+\newcommand{\isasymLongleftarrow}{\isamath{\Longleftarrow}}
+\newcommand{\isasymRightarrow}{\isamath{\Rightarrow}}
+\newcommand{\isasymLongrightarrow}{\isamath{\Longrightarrow}}
+\newcommand{\isasymleftrightarrow}{\isamath{\leftrightarrow}}
+\newcommand{\isasymlongleftrightarrow}{\isamath{\longleftrightarrow}}
+\newcommand{\isasymLeftrightarrow}{\isamath{\Leftrightarrow}}
+\newcommand{\isasymLongleftrightarrow}{\isamath{\Longleftrightarrow}}
+\newcommand{\isasymmapsto}{\isamath{\mapsto}}
+\newcommand{\isasymlongmapsto}{\isamath{\longmapsto}}
+\newcommand{\isasymmidarrow}{\isamath{\relbar}}
+\newcommand{\isasymMidarrow}{\isamath{\Relbar}}
+\newcommand{\isasymhookleftarrow}{\isamath{\hookleftarrow}}
+\newcommand{\isasymhookrightarrow}{\isamath{\hookrightarrow}}
+\newcommand{\isasymleftharpoondown}{\isamath{\leftharpoondown}}
+\newcommand{\isasymrightharpoondown}{\isamath{\rightharpoondown}}
+\newcommand{\isasymleftharpoonup}{\isamath{\leftharpoonup}}
+\newcommand{\isasymrightharpoonup}{\isamath{\rightharpoonup}}
+\newcommand{\isasymrightleftharpoons}{\isamath{\rightleftharpoons}}
+\newcommand{\isasymleadsto}{\isamath{\leadsto}} %requires latexsym
+\newcommand{\isasymup}{\isamath{\uparrow}}
+\newcommand{\isasymUp}{\isamath{\Uparrow}}
+\newcommand{\isasymdown}{\isamath{\downarrow}}
+\newcommand{\isasymDown}{\isamath{\Downarrow}}
+\newcommand{\isasymupdown}{\isamath{\updownarrow}}
+\newcommand{\isasymUpdown}{\isamath{\Updownarrow}}
+\newcommand{\isasymlangle}{\isamath{\langle}}
+\newcommand{\isasymrangle}{\isamath{\rangle}}
+\newcommand{\isasymlceil}{\isamath{\lceil}}
+\newcommand{\isasymrceil}{\isamath{\rceil}}
+\newcommand{\isasymlfloor}{\isamath{\lfloor}}
+\newcommand{\isasymrfloor}{\isamath{\rfloor}}
+\newcommand{\isasymlparr}{\isamath{\mathopen{(\mkern-3mu\mid}}}
+\newcommand{\isasymrparr}{\isamath{\mathclose{\mid\mkern-3mu)}}}
+\newcommand{\isasymlbrakk}{\isamath{\mathopen{\lbrack\mkern-3mu\lbrack}}}
+\newcommand{\isasymrbrakk}{\isamath{\mathclose{\rbrack\mkern-3mu\rbrack}}}
+\newcommand{\isasymlbrace}{\isamath{\mathopen{\lbrace\mkern-4.5mu\mid}}}
+\newcommand{\isasymrbrace}{\isamath{\mathclose{\mid\mkern-4.5mu\rbrace}}}
+\newcommand{\isasymguillemotleft}{\isatext{\flqq}} %requires babel
+\newcommand{\isasymguillemotright}{\isatext{\frqq}} %requires babel
+\newcommand{\isasymColon}{\isamath{\mathrel{::}}}
+\newcommand{\isasymnot}{\isamath{\neg}}
+\newcommand{\isasymbottom}{\isamath{\bot}}
+\newcommand{\isasymtop}{\isamath{\top}}
+\newcommand{\isasymand}{\isamath{\wedge}}
+\newcommand{\isasymAnd}{\isamath{\bigwedge}}
+\newcommand{\isasymor}{\isamath{\vee}}
+\newcommand{\isasymOr}{\isamath{\bigvee}}
+\newcommand{\isasymforall}{\isamath{\forall\,}}
+\newcommand{\isasymexists}{\isamath{\exists\,}}
+\newcommand{\isasymbox}{\isamath{\Box}} %requires latexsym
+\newcommand{\isasymdiamond}{\isamath{\Diamond}} %requires latexsym
+\newcommand{\isasymturnstile}{\isamath{\vdash}}
+\newcommand{\isasymTurnstile}{\isamath{\models}}
+\newcommand{\isasymtturnstile}{\isamath{\vdash\!\!\!\vdash}}
+\newcommand{\isasymTTurnstile}{\isamath{\mid\!\models}}
+\newcommand{\isasymstileturn}{\isamath{\dashv}}
+\newcommand{\isasymsurd}{\isamath{\surd}}
+\newcommand{\isasymle}{\isamath{\le}}
+\newcommand{\isasymge}{\isamath{\ge}}
+\newcommand{\isasymlless}{\isamath{\ll}}
+\newcommand{\isasymggreater}{\isamath{\gg}}
+\newcommand{\isasymlesssim}{\isamath{\lesssim}} %requires amssymb
+\newcommand{\isasymgreatersim}{\isamath{\gtrsim}} %requires amssymb
+\newcommand{\isasymlessapprox}{\isamath{\lessapprox}} %requires amssymb
+\newcommand{\isasymgreaterapprox}{\isamath{\gtrapprox}} %requires amssymb
+\newcommand{\isasymin}{\isamath{\in}}
+\newcommand{\isasymnotin}{\isamath{\notin}}
+\newcommand{\isasymsubset}{\isamath{\subset}}
+\newcommand{\isasymsupset}{\isamath{\supset}}
+\newcommand{\isasymsubseteq}{\isamath{\subseteq}}
+\newcommand{\isasymsupseteq}{\isamath{\supseteq}}
+\newcommand{\isasymsqsubset}{\isamath{\sqsubset}}
+\newcommand{\isasymsqsupset}{\isamath{\sqsupset}} %requires latexsym
+\newcommand{\isasymsqsubseteq}{\isamath{\sqsubseteq}}
+\newcommand{\isasymsqsupseteq}{\isamath{\sqsupseteq}}
+\newcommand{\isasyminter}{\isamath{\cap}}
+\newcommand{\isasymInter}{\isamath{\bigcap\,}}
+\newcommand{\isasymunion}{\isamath{\cup}}
+\newcommand{\isasymUnion}{\isamath{\bigcup\,}}
+\newcommand{\isasymsqunion}{\isamath{\sqcup}}
+\newcommand{\isasymSqunion}{\isamath{\bigsqcup\,}}
+\newcommand{\isasymsqinter}{\isamath{\sqcap}}
+\newcommand{\isasymSqinter}{\isamath{\bigsqcap\,}} %requires stmaryrd
+\newcommand{\isasymuplus}{\isamath{\uplus}}
+\newcommand{\isasymUplus}{\isamath{\biguplus\,}}
+\newcommand{\isasymnoteq}{\isamath{\not=}}
+\newcommand{\isasymsim}{\isamath{\sim}}
+\newcommand{\isasymdoteq}{\isamath{\doteq}}
+\newcommand{\isasymsimeq}{\isamath{\simeq}}
+\newcommand{\isasymapprox}{\isamath{\approx}}
+\newcommand{\isasymasymp}{\isamath{\asymp}}
+\newcommand{\isasymcong}{\isamath{\cong}}
+\newcommand{\isasymsmile}{\isamath{\smile}}
+\newcommand{\isasymequiv}{\isamath{\equiv}}
+\newcommand{\isasymfrown}{\isamath{\frown}}
+\newcommand{\isasympropto}{\isamath{\propto}}
+\newcommand{\isasymbowtie}{\isamath{\bowtie}}
+\newcommand{\isasymprec}{\isamath{\prec}}
+\newcommand{\isasymsucc}{\isamath{\succ}}
+\newcommand{\isasympreceq}{\isamath{\preceq}}
+\newcommand{\isasymsucceq}{\isamath{\succeq}}
+\newcommand{\isasymparallel}{\isamath{\parallel}}
+\newcommand{\isasymbar}{\isamath{\mid}}
+\newcommand{\isasymplusminus}{\isamath{\pm}}
+\newcommand{\isasymminusplus}{\isamath{\mp}}
+\newcommand{\isasymtimes}{\isamath{\times}}
+\newcommand{\isasymdiv}{\isamath{\div}}
+\newcommand{\isasymcdot}{\isamath{\cdot}}
+\newcommand{\isasymstar}{\isamath{\star}}
+\newcommand{\isasymbullet}{\boldmath\isamath{\mathchoice{\displaystyle{\cdot}}{\textstyle{\cdot}}{\scriptstyle{\bullet}}{\scriptscriptstyle{\bullet}}}}
+\newcommand{\isasymcirc}{\isamath{\circ}}
+\newcommand{\isasymdagger}{\isamath{\dagger}}
+\newcommand{\isasymddagger}{\isamath{\ddagger}}
+\newcommand{\isasymlhd}{\isamath{\lhd}}
+\newcommand{\isasymrhd}{\isamath{\rhd}}
+\newcommand{\isasymunlhd}{\isamath{\unlhd}}
+\newcommand{\isasymunrhd}{\isamath{\unrhd}}
+\newcommand{\isasymtriangleleft}{\isamath{\triangleleft}}
+\newcommand{\isasymtriangleright}{\isamath{\triangleright}}
+\newcommand{\isasymtriangle}{\isamath{\triangle}}
+\newcommand{\isasymtriangleq}{\isamath{\triangleq}} %requires amssymb
+\newcommand{\isasymoplus}{\isamath{\oplus}}
+\newcommand{\isasymOplus}{\isamath{\bigoplus\,}}
+\newcommand{\isasymotimes}{\isamath{\otimes}}
+\newcommand{\isasymOtimes}{\isamath{\bigotimes\,}}
+\newcommand{\isasymodot}{\isamath{\odot}}
+\newcommand{\isasymOdot}{\isamath{\bigodot\,}}
+\newcommand{\isasymominus}{\isamath{\ominus}}
+\newcommand{\isasymoslash}{\isamath{\oslash}}
+\newcommand{\isasymdots}{\isamath{\dots}}
+\newcommand{\isasymcdots}{\isamath{\cdots}}
+\newcommand{\isasymSum}{\isamath{\sum\,}}
+\newcommand{\isasymProd}{\isamath{\prod\,}}
+\newcommand{\isasymCoprod}{\isamath{\coprod\,}}
+\newcommand{\isasyminfinity}{\isamath{\infty}}
+\newcommand{\isasymintegral}{\isamath{\int\,}}
+\newcommand{\isasymointegral}{\isamath{\oint\,}}
+\newcommand{\isasymclubsuit}{\isamath{\clubsuit}}
+\newcommand{\isasymdiamondsuit}{\isamath{\diamondsuit}}
+\newcommand{\isasymheartsuit}{\isamath{\heartsuit}}
+\newcommand{\isasymspadesuit}{\isamath{\spadesuit}}
+\newcommand{\isasymaleph}{\isamath{\aleph}}
+\newcommand{\isasymemptyset}{\isamath{\emptyset}}
+\newcommand{\isasymnabla}{\isamath{\nabla}}
+\newcommand{\isasympartial}{\isamath{\partial}}
+\newcommand{\isasymRe}{\isamath{\Re}}
+\newcommand{\isasymIm}{\isamath{\Im}}
+\newcommand{\isasymflat}{\isamath{\flat}}
+\newcommand{\isasymnatural}{\isamath{\natural}}
+\newcommand{\isasymsharp}{\isamath{\sharp}}
+\newcommand{\isasymangle}{\isamath{\angle}}
+\newcommand{\isasymcopyright}{\isatext{\rm\copyright}}
+\newcommand{\isasymregistered}{\isatext{\rm\textregistered}}
+\newcommand{\isasymhyphen}{\isatext{\rm-}}
+\newcommand{\isasyminverse}{\isamath{{}^{-1}}}
+\newcommand{\isasymonesuperior}{\isamath{\mathonesuperior}} %requires latin1
+\newcommand{\isasymonequarter}{\isatext{\rm\textonequarter}} %requires latin1
+\newcommand{\isasymtwosuperior}{\isamath{\mathtwosuperior}} %requires latin1
+\newcommand{\isasymonehalf}{\isatext{\rm\textonehalf}} %requires latin1
+\newcommand{\isasymthreesuperior}{\isamath{\maththreesuperior}} %requires latin1
+\newcommand{\isasymthreequarters}{\isatext{\rm\textthreequarters}} %requires latin1
+\newcommand{\isasymordfeminine}{\isatext{\rm\textordfeminine}}
+\newcommand{\isasymordmasculine}{\isatext{\rm\textordmasculine}}
+\newcommand{\isasymsection}{\isatext{\rm\S}}
+\newcommand{\isasymparagraph}{\isatext{\rm\P}}
+\newcommand{\isasymexclamdown}{\isatext{\rm\textexclamdown}}
+\newcommand{\isasymquestiondown}{\isatext{\rm\textquestiondown}}
+\newcommand{\isasymeuro}{\isatext{\EUR}} %requires marvosym
+\newcommand{\isasympounds}{\isamath{\pounds}}
+\newcommand{\isasymyen}{\isatext{\yen}} %requires amssymb
+\newcommand{\isasymcent}{\isatext{\cent}} %requires wasysym
+\newcommand{\isasymcurrency}{\isatext{\currency}} %requires wasysym
+\newcommand{\isasymdegree}{\isatext{\rm\textdegree}} %requires latin1
+\newcommand{\isasymamalg}{\isamath{\amalg}}
+\newcommand{\isasymmho}{\isamath{\mho}} %requires latexsym
+\newcommand{\isasymlozenge}{\isamath{\lozenge}} %requires amssym
+\newcommand{\isasymJoin}{\isamath{\Join}} %requires latexsym
+\newcommand{\isasymwp}{\isamath{\wp}}
+\newcommand{\isasymwrong}{\isamath{\wr}}
+\newcommand{\isasymstruct}{\isamath{\diamond}}
+\newcommand{\isasymacute}{\isatext{\'\relax}}
+\newcommand{\isasymindex}{\isatext{\i}}
+\newcommand{\isasymdieresis}{\isatext{\"\relax}}
+\newcommand{\isasymcedilla}{\isatext{\c\relax}}
+\newcommand{\isasymhungarumlaut}{\isatext{\H\relax}}
+\newcommand{\isasymspacespace}{\isamath{~~}}