--- a/doc-src/IsarRef/Thy/document/First_Order_Logic.tex Sun Feb 15 17:47:49 2009 +0100
+++ b/doc-src/IsarRef/Thy/document/First_Order_Logic.tex Sun Feb 15 17:48:02 2009 +0100
@@ -23,11 +23,11 @@
\endisadelimvisible
%
\begin{isamarkuptext}%
-In order to commence a new object-logic within Isabelle/Pure we
- introduce abstract syntactic categories \isa{{\isachardoublequote}i{\isachardoublequote}} for individuals
- and \isa{{\isachardoublequote}o{\isachardoublequote}} for object-propositions. The latter is embedded
- into the language of Pure propositions by means of a separate
- judgment.%
+\noindent In order to commence a new object-logic within
+ Isabelle/Pure we introduce abstract syntactic categories \isa{{\isachardoublequote}i{\isachardoublequote}}
+ for individuals and \isa{{\isachardoublequote}o{\isachardoublequote}} for object-propositions. The latter
+ is embedded into the language of Pure propositions by means of a
+ separate judgment.%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{typedecl}\isamarkupfalse%
@@ -298,9 +298,9 @@
\endisadelimproof
%
\begin{isamarkuptext}%
-Reasoning from basic axioms is often tedious. Our proofs work by
- producing various instances of the given rules (potentially the
- symmetric form) using the pattern ``\hyperlink{command.have}{\mbox{\isa{\isacommand{have}}}}~\isa{eq}~\hyperlink{command.by}{\mbox{\isa{\isacommand{by}}}}~\isa{{\isachardoublequote}{\isacharparenleft}rule\ r{\isacharparenright}{\isachardoublequote}}'' and composing the chain of
+\noindent Reasoning from basic axioms is often tedious. Our proofs
+ work by producing various instances of the given rules (potentially
+ the symmetric form) using the pattern ``\hyperlink{command.have}{\mbox{\isa{\isacommand{have}}}}~\isa{eq}~\hyperlink{command.by}{\mbox{\isa{\isacommand{by}}}}~\isa{{\isachardoublequote}{\isacharparenleft}rule\ r{\isacharparenright}{\isachardoublequote}}'' and composing the chain of
results via \hyperlink{command.also}{\mbox{\isa{\isacommand{also}}}}/\hyperlink{command.finally}{\mbox{\isa{\isacommand{finally}}}}. These steps may
involve any of the transitivity rules declared in
\secref{sec:framework-ex-equal}, namely \isa{trans} in combining
@@ -354,19 +354,19 @@
definitions in order to normalize each equational problem. A more
realistic object-logic would include proper setup for the Simplifier
(\secref{sec:simplifier}), the main automated tool for equational
- reasoning in Isabelle. Then ``\hyperlink{command.unfolding}{\mbox{\isa{\isacommand{unfolding}}}}~\isa{left{\isacharunderscore}inv}~\hyperlink{command.ddot}{\mbox{\isa{\isacommand{{\isachardot}{\isachardot}}}}}'' would become ``\hyperlink{command.by}{\mbox{\isa{\isacommand{by}}}}~\isa{{\isachardoublequote}{\isacharparenleft}simp\ add{\isacharcolon}\ left{\isacharunderscore}inv{\isacharparenright}{\isachardoublequote}}'' etc.%
+ reasoning in Isabelle. Then ``\hyperlink{command.unfolding}{\mbox{\isa{\isacommand{unfolding}}}}~\isa{left{\isacharunderscore}inv}~\hyperlink{command.ddot}{\mbox{\isa{\isacommand{{\isachardot}{\isachardot}}}}}'' would become ``\hyperlink{command.by}{\mbox{\isa{\isacommand{by}}}}~\isa{{\isachardoublequote}{\isacharparenleft}simp\ only{\isacharcolon}\ left{\isacharunderscore}inv{\isacharparenright}{\isachardoublequote}}'' etc.%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{end}\isamarkupfalse%
%
-\isamarkupsubsection{Propositional logic%
+\isamarkupsubsection{Propositional logic \label{sec:framework-ex-prop}%
}
\isamarkuptrue%
%
\begin{isamarkuptext}%
We axiomatize basic connectives of propositional logic: implication,
disjunction, and conjunction. The associated rules are modeled
- after Gentzen's natural deduction \cite{Gentzen:1935}.%
+ after Gentzen's system of Natural Deduction \cite{Gentzen:1935}.%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{axiomatization}\isamarkupfalse%
@@ -378,16 +378,16 @@
\isacommand{axiomatization}\isamarkupfalse%
\isanewline
\ \ disj\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}o\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ o{\isachardoublequoteclose}\ \ {\isacharparenleft}\isakeyword{infixr}\ {\isachardoublequoteopen}{\isasymor}{\isachardoublequoteclose}\ {\isadigit{3}}{\isadigit{0}}{\isacharparenright}\ \isakeyword{where}\isanewline
-\ \ disjE\ {\isacharbrackleft}elim{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}A\ {\isasymor}\ B\ {\isasymLongrightarrow}\ {\isacharparenleft}A\ {\isasymLongrightarrow}\ C{\isacharparenright}\ {\isasymLongrightarrow}\ {\isacharparenleft}B\ {\isasymLongrightarrow}\ C{\isacharparenright}\ {\isasymLongrightarrow}\ C{\isachardoublequoteclose}\ \isakeyword{and}\isanewline
\ \ disjI\isactrlisub {\isadigit{1}}\ {\isacharbrackleft}intro{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}A\ {\isasymLongrightarrow}\ A\ {\isasymor}\ B{\isachardoublequoteclose}\ \isakeyword{and}\isanewline
-\ \ disjI\isactrlisub {\isadigit{2}}\ {\isacharbrackleft}intro{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}B\ {\isasymLongrightarrow}\ A\ {\isasymor}\ B{\isachardoublequoteclose}\isanewline
+\ \ disjI\isactrlisub {\isadigit{2}}\ {\isacharbrackleft}intro{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}B\ {\isasymLongrightarrow}\ A\ {\isasymor}\ B{\isachardoublequoteclose}\ \isakeyword{and}\isanewline
+\ \ disjE\ {\isacharbrackleft}elim{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}A\ {\isasymor}\ B\ {\isasymLongrightarrow}\ {\isacharparenleft}A\ {\isasymLongrightarrow}\ C{\isacharparenright}\ {\isasymLongrightarrow}\ {\isacharparenleft}B\ {\isasymLongrightarrow}\ C{\isacharparenright}\ {\isasymLongrightarrow}\ C{\isachardoublequoteclose}\isanewline
\isanewline
\isacommand{axiomatization}\isamarkupfalse%
\isanewline
\ \ conj\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}o\ {\isasymRightarrow}\ o\ {\isasymRightarrow}\ o{\isachardoublequoteclose}\ \ {\isacharparenleft}\isakeyword{infixr}\ {\isachardoublequoteopen}{\isasymand}{\isachardoublequoteclose}\ {\isadigit{3}}{\isadigit{5}}{\isacharparenright}\ \isakeyword{where}\isanewline
\ \ conjI\ {\isacharbrackleft}intro{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}A\ {\isasymLongrightarrow}\ B\ {\isasymLongrightarrow}\ A\ {\isasymand}\ B{\isachardoublequoteclose}\ \isakeyword{and}\isanewline
-\ \ conjD\isactrlisub {\isadigit{1}}\ {\isacharbrackleft}dest{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}A\ {\isasymand}\ B\ {\isasymLongrightarrow}\ A{\isachardoublequoteclose}\ \isakeyword{and}\isanewline
-\ \ conjD\isactrlisub {\isadigit{2}}\ {\isacharbrackleft}dest{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}A\ {\isasymand}\ B\ {\isasymLongrightarrow}\ B{\isachardoublequoteclose}%
+\ \ conjD\isactrlisub {\isadigit{1}}{\isacharcolon}\ {\isachardoublequoteopen}A\ {\isasymand}\ B\ {\isasymLongrightarrow}\ A{\isachardoublequoteclose}\ \isakeyword{and}\isanewline
+\ \ conjD\isactrlisub {\isadigit{2}}{\isacharcolon}\ {\isachardoublequoteopen}A\ {\isasymand}\ B\ {\isasymLongrightarrow}\ B{\isachardoublequoteclose}%
\begin{isamarkuptext}%
\noindent The conjunctive destructions have the disadvantage that
decomposing \isa{{\isachardoublequote}A\ {\isasymand}\ B{\isachardoublequote}} involves an immediate decision which
@@ -410,12 +410,12 @@
\isanewline
\ \ \isacommand{from}\isamarkupfalse%
\ {\isacharbackquoteopen}A\ {\isasymand}\ B{\isacharbackquoteclose}\ \isacommand{show}\isamarkupfalse%
-\ A\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
-\isanewline
+\ A\ \isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}rule\ conjD\isactrlisub {\isadigit{1}}{\isacharparenright}\isanewline
\ \ \isacommand{from}\isamarkupfalse%
\ {\isacharbackquoteopen}A\ {\isasymand}\ B{\isacharbackquoteclose}\ \isacommand{show}\isamarkupfalse%
-\ B\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
-\isanewline
+\ B\ \isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}rule\ conjD\isactrlisub {\isadigit{2}}{\isacharparenright}\isanewline
\isacommand{qed}\isamarkupfalse%
%
\endisatagproof
@@ -454,8 +454,9 @@
\endisadelimproof
%
\begin{isamarkuptext}%
-Note that the analogous elimination for disjunction ``\isa{{\isachardoublequote}{\isasymASSUMES}\ A\ {\isasymor}\ B\ {\isasymOBTAINS}\ A\ {\isasymBBAR}\ B{\isachardoublequote}}'' coincides with the
- original axiomatization of \isa{{\isachardoublequote}disjE{\isachardoublequote}}.
+\noindent Note that the analogous elimination rule for disjunction
+ ``\isa{{\isachardoublequote}{\isasymASSUMES}\ A\ {\isasymor}\ B\ {\isasymOBTAINS}\ A\ {\isasymBBAR}\ B{\isachardoublequote}}'' coincides with
+ the original axiomatization of \isa{disjE}.
\medskip We continue propositional logic by introducing absurdity
with its characteristic elimination. Plain truth may then be
@@ -491,7 +492,8 @@
\endisadelimproof
%
\begin{isamarkuptext}%
-\medskip Now negation represents an implication towards absurdity:%
+\medskip\noindent Now negation represents an implication towards
+ absurdity:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{definition}\isamarkupfalse%
@@ -658,21 +660,21 @@
\endisadelimproof
%
\begin{isamarkuptext}%
-These examples illustrate both classical reasoning and non-trivial
- propositional proofs in general. All three rules characterize
- classical logic independently, but the original rule is already the
- most convenient to use, because it leaves the conclusion unchanged.
- Note that \isa{{\isachardoublequote}{\isacharparenleft}{\isasymnot}\ C\ {\isasymLongrightarrow}\ C{\isacharparenright}\ {\isasymLongrightarrow}\ C{\isachardoublequote}} fits again into our format for
- eliminations, despite the additional twist that the context refers
- to the main conclusion. So we may write \isa{{\isachardoublequote}classical{\isachardoublequote}} as the
- Isar statement ``\isa{{\isachardoublequote}{\isasymOBTAINS}\ {\isasymnot}\ thesis{\isachardoublequote}}''. This also
- explains nicely how classical reasoning really works: whatever the
- main \isa{thesis} might be, we may always assume its negation!%
+\noindent These examples illustrate both classical reasoning and
+ non-trivial propositional proofs in general. All three rules
+ characterize classical logic independently, but the original rule is
+ already the most convenient to use, because it leaves the conclusion
+ unchanged. Note that \isa{{\isachardoublequote}{\isacharparenleft}{\isasymnot}\ C\ {\isasymLongrightarrow}\ C{\isacharparenright}\ {\isasymLongrightarrow}\ C{\isachardoublequote}} fits again into our
+ format for eliminations, despite the additional twist that the
+ context refers to the main conclusion. So we may write \isa{classical} as the Isar statement ``\isa{{\isachardoublequote}{\isasymOBTAINS}\ {\isasymnot}\ thesis{\isachardoublequote}}''.
+ This also explains nicely how classical reasoning really works:
+ whatever the main \isa{thesis} might be, we may always assume its
+ negation!%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{end}\isamarkupfalse%
%
-\isamarkupsubsection{Quantifiers%
+\isamarkupsubsection{Quantifiers \label{sec:framework-ex-quant}%
}
\isamarkuptrue%
%
@@ -681,7 +683,7 @@
of the underlying framework. According to the well-known technique
introduced by Church \cite{church40}, quantifiers are operators on
predicates, which are syntactically represented as \isa{{\isachardoublequote}{\isasymlambda}{\isachardoublequote}}-terms
- of type \isa{{\isachardoublequote}i\ {\isasymRightarrow}\ o{\isachardoublequote}}. Specific binder notation relates \isa{{\isachardoublequote}All\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ B\ x{\isacharparenright}{\isachardoublequote}} to \isa{{\isachardoublequote}{\isasymforall}x{\isachardot}\ B\ x{\isachardoublequote}} etc.%
+ of type \isa{{\isachardoublequote}i\ {\isasymRightarrow}\ o{\isachardoublequote}}. Binder notation turns \isa{{\isachardoublequote}All\ {\isacharparenleft}{\isasymlambda}x{\isachardot}\ B\ x{\isacharparenright}{\isachardoublequote}} into \isa{{\isachardoublequote}{\isasymforall}x{\isachardot}\ B\ x{\isachardoublequote}} etc.%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{axiomatization}\isamarkupfalse%
@@ -696,10 +698,9 @@
\ \ exI\ {\isacharbrackleft}intro{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}B\ a\ {\isasymLongrightarrow}\ {\isacharparenleft}{\isasymexists}x{\isachardot}\ B\ x{\isacharparenright}{\isachardoublequoteclose}\ \isakeyword{and}\isanewline
\ \ exE\ {\isacharbrackleft}elim{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharparenleft}{\isasymexists}x{\isachardot}\ B\ x{\isacharparenright}\ {\isasymLongrightarrow}\ {\isacharparenleft}{\isasymAnd}x{\isachardot}\ B\ x\ {\isasymLongrightarrow}\ C{\isacharparenright}\ {\isasymLongrightarrow}\ C{\isachardoublequoteclose}%
\begin{isamarkuptext}%
-\noindent The \isa{exE} rule corresponds to an Isar statement
- ``\isa{{\isachardoublequote}{\isasymASSUMES}\ {\isasymexists}x{\isachardot}\ B\ x\ {\isasymOBTAINS}\ x\ {\isasymWHERE}\ B\ x{\isachardoublequote}}''. In the
- following example we illustrate quantifier reasoning with all four
- rules:%
+\noindent The statement of \isa{exE} corresponds to ``\isa{{\isachardoublequote}{\isasymASSUMES}\ {\isasymexists}x{\isachardot}\ B\ x\ {\isasymOBTAINS}\ x\ {\isasymWHERE}\ B\ x{\isachardoublequote}}'' in Isar. In the
+ subsequent example we illustrate quantifier reasoning involving all
+ four rules:%
\end{isamarkuptext}%
\isamarkuptrue%
\isacommand{theorem}\isamarkupfalse%
@@ -745,12 +746,657 @@
{\isafoldproof}%
%
\isadelimproof
+%
+\endisadelimproof
+%
+\isamarkupsubsection{Canonical reasoning patterns%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+The main rules of first-order predicate logic from
+ \secref{sec:framework-ex-prop} and \secref{sec:framework-ex-quant}
+ can now be summarized as follows, using the native Isar statement
+ format of \secref{sec:framework-stmt}.
+
+ \medskip
+ \begin{tabular}{l}
+ \isa{{\isachardoublequote}impI{\isacharcolon}\ {\isasymASSUMES}\ A\ {\isasymLongrightarrow}\ B\ {\isasymSHOWS}\ A\ {\isasymlongrightarrow}\ B{\isachardoublequote}} \\
+ \isa{{\isachardoublequote}impD{\isacharcolon}\ {\isasymASSUMES}\ A\ {\isasymlongrightarrow}\ B\ {\isasymAND}\ A\ {\isasymSHOWS}\ B{\isachardoublequote}} \\[1ex]
+
+ \isa{{\isachardoublequote}disjI\isactrlisub {\isadigit{1}}{\isacharcolon}\ {\isasymASSUMES}\ A\ {\isasymSHOWS}\ A\ {\isasymor}\ B{\isachardoublequote}} \\
+ \isa{{\isachardoublequote}disjI\isactrlisub {\isadigit{2}}{\isacharcolon}\ {\isasymASSUMES}\ B\ {\isasymSHOWS}\ A\ {\isasymor}\ B{\isachardoublequote}} \\
+ \isa{{\isachardoublequote}disjE{\isacharcolon}\ {\isasymASSUMES}\ A\ {\isasymor}\ B\ {\isasymOBTAINS}\ A\ {\isasymBBAR}\ B{\isachardoublequote}} \\[1ex]
+
+ \isa{{\isachardoublequote}conjI{\isacharcolon}\ {\isasymASSUMES}\ A\ {\isasymAND}\ B\ {\isasymSHOWS}\ A\ {\isasymand}\ B{\isachardoublequote}} \\
+ \isa{{\isachardoublequote}conjE{\isacharcolon}\ {\isasymASSUMES}\ A\ {\isasymand}\ B\ {\isasymOBTAINS}\ A\ {\isasymAND}\ B{\isachardoublequote}} \\[1ex]
+
+ \isa{{\isachardoublequote}falseE{\isacharcolon}\ {\isasymASSUMES}\ {\isasymbottom}\ {\isasymSHOWS}\ A{\isachardoublequote}} \\
+ \isa{{\isachardoublequote}trueI{\isacharcolon}\ {\isasymSHOWS}\ {\isasymtop}{\isachardoublequote}} \\[1ex]
+
+ \isa{{\isachardoublequote}notI{\isacharcolon}\ {\isasymASSUMES}\ A\ {\isasymLongrightarrow}\ {\isasymbottom}\ {\isasymSHOWS}\ {\isasymnot}\ A{\isachardoublequote}} \\
+ \isa{{\isachardoublequote}notE{\isacharcolon}\ {\isasymASSUMES}\ {\isasymnot}\ A\ {\isasymAND}\ A\ {\isasymSHOWS}\ B{\isachardoublequote}} \\[1ex]
+
+ \isa{{\isachardoublequote}allI{\isacharcolon}\ {\isasymASSUMES}\ {\isasymAnd}x{\isachardot}\ B\ x\ {\isasymSHOWS}\ {\isasymforall}x{\isachardot}\ B\ x{\isachardoublequote}} \\
+ \isa{{\isachardoublequote}allE{\isacharcolon}\ {\isasymASSUMES}\ {\isasymforall}x{\isachardot}\ B\ x\ {\isasymSHOWS}\ B\ a{\isachardoublequote}} \\[1ex]
+
+ \isa{{\isachardoublequote}exI{\isacharcolon}\ {\isasymASSUMES}\ B\ a\ {\isasymSHOWS}\ {\isasymexists}x{\isachardot}\ B\ x{\isachardoublequote}} \\
+ \isa{{\isachardoublequote}exE{\isacharcolon}\ {\isasymASSUMES}\ {\isasymexists}x{\isachardot}\ B\ x\ {\isasymOBTAINS}\ a\ {\isasymWHERE}\ B\ a{\isachardoublequote}}
+ \end{tabular}
+ \medskip
+
+ \noindent This essentially provides a declarative reading of Pure
+ rules as Isar reasoning patterns: the rule statements tells how a
+ canonical proof outline shall look like. Since the above rules have
+ already been declared as \hyperlink{attribute.Pure.intro}{\mbox{\isa{intro}}}, \hyperlink{attribute.Pure.elim}{\mbox{\isa{elim}}}, \hyperlink{attribute.Pure.dest}{\mbox{\isa{dest}}} --- each according to its
+ particular shape --- we can immediately write Isar proof texts as
+ follows:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+%
+\begin{minipage}[t]{0.4\textwidth}
\isanewline
+\ \ \isacommand{have}\isamarkupfalse%
+\ {\isachardoublequoteopen}A\ {\isasymlongrightarrow}\ B{\isachardoublequoteclose}\isanewline
+\ \ \isacommand{proof}\isamarkupfalse%
+\isanewline
+\ \ \ \ \isacommand{assume}\isamarkupfalse%
+\ A\isanewline
+\ \ \ \ \isacommand{show}\isamarkupfalse%
+\ B%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isadelimnoproof
+\ %
+\endisadelimnoproof
+%
+\isatagnoproof
+\isacommand{sorry}\isamarkupfalse%
+%
+\endisatagnoproof
+{\isafoldnoproof}%
+%
+\isadelimnoproof
+\isanewline
+%
+\endisadelimnoproof
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{qed}\isamarkupfalse%
+%
+\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}
+\isanewline
+\ \ \isacommand{have}\isamarkupfalse%
+\ {\isachardoublequoteopen}A\ {\isasymlongrightarrow}\ B{\isachardoublequoteclose}\ \isakeyword{and}\ A%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isadelimnoproof
+\ %
+\endisadelimnoproof
+%
+\isatagnoproof
+\isacommand{sorry}\isamarkupfalse%
+%
+\endisatagnoproof
+{\isafoldnoproof}%
+%
+\isadelimnoproof
+\isanewline
+%
+\endisadelimnoproof
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{then}\isamarkupfalse%
+\ \isacommand{have}\isamarkupfalse%
+\ B\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
+%
+\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}
+\isanewline
+\ \ \isacommand{have}\isamarkupfalse%
+\ A%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isadelimnoproof
+\ %
+\endisadelimnoproof
+%
+\isatagnoproof
+\isacommand{sorry}\isamarkupfalse%
+%
+\endisatagnoproof
+{\isafoldnoproof}%
+%
+\isadelimnoproof
+\isanewline
+%
+\endisadelimnoproof
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{then}\isamarkupfalse%
+\ \isacommand{have}\isamarkupfalse%
+\ {\isachardoublequoteopen}A\ {\isasymor}\ B{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
+\isanewline
+\isanewline
+\ \ \isacommand{have}\isamarkupfalse%
+\ B%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isadelimnoproof
+\ %
+\endisadelimnoproof
+%
+\isatagnoproof
+\isacommand{sorry}\isamarkupfalse%
+%
+\endisatagnoproof
+{\isafoldnoproof}%
+%
+\isadelimnoproof
+\isanewline
+%
+\endisadelimnoproof
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{then}\isamarkupfalse%
+\ \isacommand{have}\isamarkupfalse%
+\ {\isachardoublequoteopen}A\ {\isasymor}\ B{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
+%
+\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}
+\isanewline
+\ \ \isacommand{have}\isamarkupfalse%
+\ {\isachardoublequoteopen}A\ {\isasymor}\ B{\isachardoublequoteclose}%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isadelimnoproof
+\ %
+\endisadelimnoproof
+%
+\isatagnoproof
+\isacommand{sorry}\isamarkupfalse%
+%
+\endisatagnoproof
+{\isafoldnoproof}%
+%
+\isadelimnoproof
+\isanewline
+%
+\endisadelimnoproof
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{then}\isamarkupfalse%
+\ \isacommand{have}\isamarkupfalse%
+\ C\isanewline
+\ \ \isacommand{proof}\isamarkupfalse%
+\isanewline
+\ \ \ \ \isacommand{assume}\isamarkupfalse%
+\ A\isanewline
+\ \ \ \ \isacommand{then}\isamarkupfalse%
+\ \isacommand{show}\isamarkupfalse%
+\ C%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isadelimnoproof
+\ %
+\endisadelimnoproof
+%
+\isatagnoproof
+\isacommand{sorry}\isamarkupfalse%
+%
+\endisatagnoproof
+{\isafoldnoproof}%
+%
+\isadelimnoproof
+\isanewline
+%
+\endisadelimnoproof
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{next}\isamarkupfalse%
+\isanewline
+\ \ \ \ \isacommand{assume}\isamarkupfalse%
+\ B\isanewline
+\ \ \ \ \isacommand{then}\isamarkupfalse%
+\ \isacommand{show}\isamarkupfalse%
+\ C%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isadelimnoproof
+\ %
+\endisadelimnoproof
+%
+\isatagnoproof
+\isacommand{sorry}\isamarkupfalse%
+%
+\endisatagnoproof
+{\isafoldnoproof}%
+%
+\isadelimnoproof
+\isanewline
+%
+\endisadelimnoproof
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{qed}\isamarkupfalse%
+%
+\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}
+\isanewline
+\ \ \isacommand{have}\isamarkupfalse%
+\ A\ \isakeyword{and}\ B%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
%
\endisadelimproof
%
+\isadelimnoproof
+\ %
+\endisadelimnoproof
+%
+\isatagnoproof
+\isacommand{sorry}\isamarkupfalse%
+%
+\endisatagnoproof
+{\isafoldnoproof}%
+%
+\isadelimnoproof
+\isanewline
+%
+\endisadelimnoproof
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{then}\isamarkupfalse%
+\ \isacommand{have}\isamarkupfalse%
+\ {\isachardoublequoteopen}A\ {\isasymand}\ B{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
+%
+\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}
+\isanewline
+\ \ \isacommand{have}\isamarkupfalse%
+\ {\isachardoublequoteopen}A\ {\isasymand}\ B{\isachardoublequoteclose}%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isadelimnoproof
+\ %
+\endisadelimnoproof
+%
+\isatagnoproof
+\isacommand{sorry}\isamarkupfalse%
+%
+\endisatagnoproof
+{\isafoldnoproof}%
+%
+\isadelimnoproof
+\isanewline
+%
+\endisadelimnoproof
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{then}\isamarkupfalse%
+\ \isacommand{obtain}\isamarkupfalse%
+\ A\ \isakeyword{and}\ B\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
+%
+\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}
+\isanewline
+\ \ \isacommand{have}\isamarkupfalse%
+\ {\isachardoublequoteopen}{\isasymbottom}{\isachardoublequoteclose}%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isadelimnoproof
+\ %
+\endisadelimnoproof
+%
+\isatagnoproof
+\isacommand{sorry}\isamarkupfalse%
+%
+\endisatagnoproof
+{\isafoldnoproof}%
+%
+\isadelimnoproof
+\isanewline
+%
+\endisadelimnoproof
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{then}\isamarkupfalse%
+\ \isacommand{have}\isamarkupfalse%
+\ A\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
+%
+\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}
+\isanewline
+\ \ \isacommand{have}\isamarkupfalse%
+\ {\isachardoublequoteopen}{\isasymtop}{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
+%
+\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}
+\isanewline
+\ \ \isacommand{have}\isamarkupfalse%
+\ {\isachardoublequoteopen}{\isasymnot}\ A{\isachardoublequoteclose}\isanewline
+\ \ \isacommand{proof}\isamarkupfalse%
+\isanewline
+\ \ \ \ \isacommand{assume}\isamarkupfalse%
+\ A\isanewline
+\ \ \ \ \isacommand{then}\isamarkupfalse%
+\ \isacommand{show}\isamarkupfalse%
+\ {\isachardoublequoteopen}{\isasymbottom}{\isachardoublequoteclose}%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isadelimnoproof
+\ %
+\endisadelimnoproof
+%
+\isatagnoproof
+\isacommand{sorry}\isamarkupfalse%
+%
+\endisatagnoproof
+{\isafoldnoproof}%
+%
+\isadelimnoproof
+\isanewline
+%
+\endisadelimnoproof
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{qed}\isamarkupfalse%
+%
+\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}
+\isanewline
+\ \ \isacommand{have}\isamarkupfalse%
+\ {\isachardoublequoteopen}{\isasymnot}\ A{\isachardoublequoteclose}\ \isakeyword{and}\ A%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isadelimnoproof
+\ %
+\endisadelimnoproof
+%
+\isatagnoproof
+\isacommand{sorry}\isamarkupfalse%
+%
+\endisatagnoproof
+{\isafoldnoproof}%
+%
+\isadelimnoproof
+\isanewline
+%
+\endisadelimnoproof
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{then}\isamarkupfalse%
+\ \isacommand{have}\isamarkupfalse%
+\ B\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
+%
+\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}
+\isanewline
+\ \ \isacommand{have}\isamarkupfalse%
+\ {\isachardoublequoteopen}{\isasymforall}x{\isachardot}\ B\ x{\isachardoublequoteclose}\isanewline
+\ \ \isacommand{proof}\isamarkupfalse%
+\isanewline
+\ \ \ \ \isacommand{fix}\isamarkupfalse%
+\ x\isanewline
+\ \ \ \ \isacommand{show}\isamarkupfalse%
+\ {\isachardoublequoteopen}B\ x{\isachardoublequoteclose}%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isadelimnoproof
+\ %
+\endisadelimnoproof
+%
+\isatagnoproof
+\isacommand{sorry}\isamarkupfalse%
+%
+\endisatagnoproof
+{\isafoldnoproof}%
+%
+\isadelimnoproof
+\isanewline
+%
+\endisadelimnoproof
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{qed}\isamarkupfalse%
+%
+\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}
+\isanewline
+\ \ \isacommand{have}\isamarkupfalse%
+\ {\isachardoublequoteopen}{\isasymforall}x{\isachardot}\ B\ x{\isachardoublequoteclose}%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isadelimnoproof
+\ %
+\endisadelimnoproof
+%
+\isatagnoproof
+\isacommand{sorry}\isamarkupfalse%
+%
+\endisatagnoproof
+{\isafoldnoproof}%
+%
+\isadelimnoproof
+\isanewline
+%
+\endisadelimnoproof
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{then}\isamarkupfalse%
+\ \isacommand{have}\isamarkupfalse%
+\ {\isachardoublequoteopen}B\ a{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
+%
+\end{minipage}\\[3ex]\begin{minipage}[t]{0.4\textwidth}
+\isanewline
+\ \ \isacommand{have}\isamarkupfalse%
+\ {\isachardoublequoteopen}{\isasymexists}x{\isachardot}\ B\ x{\isachardoublequoteclose}\isanewline
+\ \ \isacommand{proof}\isamarkupfalse%
+\isanewline
+\ \ \ \ \isacommand{show}\isamarkupfalse%
+\ {\isachardoublequoteopen}B\ a{\isachardoublequoteclose}%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isadelimnoproof
+\ %
+\endisadelimnoproof
+%
+\isatagnoproof
+\isacommand{sorry}\isamarkupfalse%
+%
+\endisatagnoproof
+{\isafoldnoproof}%
+%
+\isadelimnoproof
+\isanewline
+%
+\endisadelimnoproof
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{qed}\isamarkupfalse%
+%
+\end{minipage}\qquad\begin{minipage}[t]{0.4\textwidth}
+\isanewline
+\ \ \isacommand{have}\isamarkupfalse%
+\ {\isachardoublequoteopen}{\isasymexists}x{\isachardot}\ B\ x{\isachardoublequoteclose}%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isadelimnoproof
+\ %
+\endisadelimnoproof
+%
+\isatagnoproof
+\isacommand{sorry}\isamarkupfalse%
+%
+\endisatagnoproof
+{\isafoldnoproof}%
+%
+\isadelimnoproof
+\isanewline
+%
+\endisadelimnoproof
+%
+\isadelimproof
+\ \ %
+\endisadelimproof
+%
+\isatagproof
+\isacommand{then}\isamarkupfalse%
+\ \isacommand{obtain}\isamarkupfalse%
+\ a\ \isakeyword{where}\ {\isachardoublequoteopen}B\ a{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
+%
+\end{minipage}
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\begin{isamarkuptext}%
+\bigskip\noindent Of course, these proofs are merely examples. As
+ sketched in \secref{sec:framework-subproof}, there is a fair amount
+ of flexibility in expressing Pure deductions in Isar. Here the user
+ is asked to express himself adequately, aiming at proof texts of
+ literary quality.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
\isadelimvisible
-\isanewline
%
\endisadelimvisible
%
@@ -761,9 +1407,9 @@
{\isafoldvisible}%
%
\isadelimvisible
-\isanewline
%
\endisadelimvisible
+\isanewline
\end{isabellebody}%
%%% Local Variables:
%%% mode: latex