# HG changeset patch
# User wenzelm
# Date 1234210390 -3600
# Node ID a06894e9b6e3eae528c2573ca2a9657b59d85367
# Parent  df4e53d18ebce6a8bbf8d1214da03ebdb0ffd879
updated generated files;

diff -r df4e53d18ebc -r a06894e9b6e3 doc-src/IsarRef/Thy/document/Framework.tex
--- a/doc-src/IsarRef/Thy/document/Framework.tex	Mon Feb 09 21:09:24 2009 +0100
+++ b/doc-src/IsarRef/Thy/document/Framework.tex	Mon Feb 09 21:13:10 2009 +0100
@@ -68,7 +68,232 @@
   object-logic.  Isabelle/HOL \cite{isa-tutorial} (simply-typed
   set-theory) is being used most of the time; Isabelle/ZF
   \cite{isabelle-ZF} is less extensively developed, although it would
-  probably fit better for classical mathematics.%
+  probably fit better for classical mathematics.
+
+  \medskip In order to illustrate typical natural deduction reasoning
+  in Isar, we shall refer to the background theory and library of
+  Isabelle/HOL.  This includes common notions of predicate logic,
+  naive set-theory etc.\ using fairly standard mathematical notation.
+  From the perspective of generic natural deduction there is nothing
+  special about the logical connectives of HOL (\isa{{\isachardoublequote}{\isasymand}{\isachardoublequote}}, \isa{{\isachardoublequote}{\isasymor}{\isachardoublequote}}, \isa{{\isachardoublequote}{\isasymforall}{\isachardoublequote}}, \isa{{\isachardoublequote}{\isasymexists}{\isachardoublequote}}, etc.), only the resulting reasoning
+  principles are relevant to the user.  There are similar rules
+  available for set-theory operators (\isa{{\isachardoublequote}{\isasyminter}{\isachardoublequote}}, \isa{{\isachardoublequote}{\isasymunion}{\isachardoublequote}}, \isa{{\isachardoublequote}{\isasymInter}{\isachardoublequote}}, \isa{{\isachardoublequote}{\isasymUnion}{\isachardoublequote}}, etc.), or any other theory developed in the
+  library (lattice theory, topology etc.).
+
+  Subsequently we briefly review fragments of Isar proof texts
+  corresponding directly to such general natural deduction schemes.
+  The examples shall refer to set-theory, to minimize the danger of
+  understanding connectives of predicate logic as something special.
+
+  \medskip The following deduction performs \isa{{\isachardoublequote}{\isasyminter}{\isachardoublequote}}-introduction,
+  working forwards from assumptions towards the conclusion.  We give
+  both the Isar text, and depict the primitive rule involved, as
+  determined by unification of the problem against rules from the
+  context.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\medskip\begin{minipage}{0.6\textwidth}
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+\ \ \ \ \isacommand{assume}\isamarkupfalse%
+\ {\isachardoublequoteopen}x\ {\isasymin}\ A{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}x\ {\isasymin}\ B{\isachardoublequoteclose}\isanewline
+\ \ \ \ \isacommand{then}\isamarkupfalse%
+\ \isacommand{have}\isamarkupfalse%
+\ {\isachardoublequoteopen}x\ {\isasymin}\ A\ {\isasyminter}\ B{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\end{minipage}\begin{minipage}{0.4\textwidth}
+%
+\begin{isamarkuptext}%
+\infer{\isa{{\isachardoublequote}x\ {\isasymin}\ A\ {\isasyminter}\ B{\isachardoublequote}}}{\isa{{\isachardoublequote}x\ {\isasymin}\ A{\isachardoublequote}} & \isa{{\isachardoublequote}x\ {\isasymin}\ B{\isachardoublequote}}}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\end{minipage}
+%
+\begin{isamarkuptext}%
+\medskip\noindent Note that \hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}} augments the
+  context, \hyperlink{command.then}{\mbox{\isa{\isacommand{then}}}} indicates that the current facts shall be
+  used in the next step, and \hyperlink{command.have}{\mbox{\isa{\isacommand{have}}}} states a local claim.
+  The two dots ``\hyperlink{command.ddot}{\mbox{\isa{\isacommand{{\isachardot}{\isachardot}}}}}'' above refer to a complete proof of
+  the claim, using the indicated facts and a canonical rule from the
+  context.  We could have been more explicit here by spelling out the
+  final proof step via the \hyperlink{command.by}{\mbox{\isa{\isacommand{by}}}} command:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+\ \ \ \ \isacommand{assume}\isamarkupfalse%
+\ {\isachardoublequoteopen}x\ {\isasymin}\ A{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}x\ {\isasymin}\ B{\isachardoublequoteclose}\isanewline
+\ \ \ \ \isacommand{then}\isamarkupfalse%
+\ \isacommand{have}\isamarkupfalse%
+\ {\isachardoublequoteopen}x\ {\isasymin}\ A\ {\isasyminter}\ B{\isachardoublequoteclose}\ \isacommand{by}\isamarkupfalse%
+\ {\isacharparenleft}rule\ IntI{\isacharparenright}%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\begin{isamarkuptext}%
+\noindent The format of the \isa{{\isachardoublequote}{\isasyminter}{\isachardoublequote}}-introduction rule represents
+  the most basic inference, which proceeds from given premises to a
+  conclusion, without any additional context involved.
+
+  \medskip The next example performs backwards introduction on \isa{{\isachardoublequote}{\isasymInter}{\isasymA}{\isachardoublequote}}, the intersection of all sets within a given set.  This
+  requires a nested proof of set membership within a local context of
+  an arbitrary-but-fixed member of the collection:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\medskip\begin{minipage}{0.6\textwidth}
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+\ \ \ \ \isacommand{have}\isamarkupfalse%
+\ {\isachardoublequoteopen}x\ {\isasymin}\ {\isasymInter}{\isasymA}{\isachardoublequoteclose}\isanewline
+\ \ \ \ \isacommand{proof}\isamarkupfalse%
+\isanewline
+\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
+\ A\isanewline
+\ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
+\ {\isachardoublequoteopen}A\ {\isasymin}\ {\isasymA}{\isachardoublequoteclose}\isanewline
+\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
+\ {\isachardoublequoteopen}x\ {\isasymin}\ A{\isachardoublequoteclose}\ \isacommand{sorry}\isamarkupfalse%
+\isanewline
+\ \ \ \ \isacommand{qed}\isamarkupfalse%
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\end{minipage}\begin{minipage}{0.4\textwidth}
+%
+\begin{isamarkuptext}%
+\infer{\isa{{\isachardoublequote}x\ {\isasymin}\ {\isasymInter}{\isasymA}{\isachardoublequote}}}{\infer*{\isa{{\isachardoublequote}x\ {\isasymin}\ A{\isachardoublequote}}}{\isa{{\isachardoublequote}{\isacharbrackleft}A{\isacharbrackright}{\isacharbrackleft}A\ {\isasymin}\ {\isasymA}{\isacharbrackright}{\isachardoublequote}}}}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\end{minipage}
+%
+\begin{isamarkuptext}%
+\medskip\noindent This Isar reasoning pattern again refers to the
+  primitive rule depicted above.  The system determines it in the
+  ``\hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}}'' step, which could have been spelt out more
+  explicitly as ``\hyperlink{command.proof}{\mbox{\isa{\isacommand{proof}}}}~\isa{{\isachardoublequote}{\isacharparenleft}{\isachardoublequote}}\hyperlink{method.rule}{\mbox{\isa{rule}}}~\hyperlink{fact.InterI}{\mbox{\isa{InterI}}}\isa{{\isachardoublequote}{\isacharparenright}{\isachardoublequote}}''.  Note that this rule involves both a local
+  parameter \isa{{\isachardoublequote}A{\isachardoublequote}} and an assumption \isa{{\isachardoublequote}A\ {\isasymin}\ {\isasymA}{\isachardoublequote}} in the
+  nested reasoning.  This kind of compound rule typically demands a
+  genuine sub-proof in Isar, working backwards rather than forwards as
+  seen before.  In the proof body we encounter the \hyperlink{command.fix}{\mbox{\isa{\isacommand{fix}}}}-\hyperlink{command.assume}{\mbox{\isa{\isacommand{assume}}}}-\hyperlink{command.show}{\mbox{\isa{\isacommand{show}}}} skeleton of nested
+  sub-proofs that is typical for Isar.  The final \hyperlink{command.show}{\mbox{\isa{\isacommand{show}}}} is
+  like \hyperlink{command.have}{\mbox{\isa{\isacommand{have}}}} followed by an additional refinement of the
+  enclosing claim, using the rule derived from the proof body.  The
+  \hyperlink{command.sorry}{\mbox{\isa{\isacommand{sorry}}}} command stands for a hole in the proof -- it may
+  be understood as an excuse for not providing a proper proof yet.
+
+  \medskip The next example involves \isa{{\isachardoublequote}{\isasymUnion}{\isasymA}{\isachardoublequote}}, which can be
+  characterized as the set of all \isa{{\isachardoublequote}x{\isachardoublequote}} such that \isa{{\isachardoublequote}{\isasymexists}A{\isachardot}\ x\ {\isasymin}\ A\ {\isasymand}\ A\ {\isasymin}\ {\isasymA}{\isachardoublequote}}.  The elimination rule for \isa{{\isachardoublequote}x\ {\isasymin}\ {\isasymUnion}{\isasymA}{\isachardoublequote}} does
+  not mention \isa{{\isachardoublequote}{\isasymexists}{\isachardoublequote}} and \isa{{\isachardoublequote}{\isasymand}{\isachardoublequote}} at all, but admits to obtain
+  directly a local \isa{{\isachardoublequote}A{\isachardoublequote}} such that \isa{{\isachardoublequote}x\ {\isasymin}\ A{\isachardoublequote}} and \isa{{\isachardoublequote}A\ {\isasymin}\ {\isasymA}{\isachardoublequote}} hold.  This corresponds to the following Isar proof and
+  inference rule, respectively:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\medskip\begin{minipage}{0.6\textwidth}
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+\ \ \ \ \isacommand{assume}\isamarkupfalse%
+\ {\isachardoublequoteopen}x\ {\isasymin}\ {\isasymUnion}{\isasymA}{\isachardoublequoteclose}\isanewline
+\ \ \ \ \isacommand{then}\isamarkupfalse%
+\ \isacommand{have}\isamarkupfalse%
+\ C\isanewline
+\ \ \ \ \isacommand{proof}\isamarkupfalse%
+\isanewline
+\ \ \ \ \ \ \isacommand{fix}\isamarkupfalse%
+\ A\isanewline
+\ \ \ \ \ \ \isacommand{assume}\isamarkupfalse%
+\ {\isachardoublequoteopen}x\ {\isasymin}\ A{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}A\ {\isasymin}\ {\isasymA}{\isachardoublequoteclose}\isanewline
+\ \ \ \ \ \ \isacommand{show}\isamarkupfalse%
+\ C\ \isacommand{sorry}\isamarkupfalse%
+\isanewline
+\ \ \ \ \isacommand{qed}\isamarkupfalse%
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\end{minipage}\begin{minipage}{0.4\textwidth}
+%
+\begin{isamarkuptext}%
+\infer{\isa{{\isachardoublequote}C{\isachardoublequote}}}{\isa{{\isachardoublequote}x\ {\isasymin}\ {\isasymUnion}{\isasymA}{\isachardoublequote}} & \infer*{\isa{{\isachardoublequote}C{\isachardoublequote}}~}{\isa{{\isachardoublequote}{\isacharbrackleft}A{\isacharbrackright}{\isacharbrackleft}x\ {\isasymin}\ A{\isacharcomma}\ A\ {\isasymin}\ {\isasymA}{\isacharbrackright}{\isachardoublequote}}}}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\end{minipage}
+%
+\begin{isamarkuptext}%
+\medskip\noindent Although the Isar proof follows the natural
+  deduction rule closely, the text reads not as natural as
+  anticipated.  There is a double occurrence of an arbitrary
+  conclusion \isa{{\isachardoublequote}C{\isachardoublequote}}, which represents the final result, but is
+  irrelevant for now.  This issue arises for any elimination rule
+  involving local parameters.  Isar provides the derived language
+  element \hyperlink{command.obtain}{\mbox{\isa{\isacommand{obtain}}}}, which is able to perform the same
+  elimination proof more conveniently:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\isatagproof
+\ \ \ \ \isacommand{assume}\isamarkupfalse%
+\ {\isachardoublequoteopen}x\ {\isasymin}\ {\isasymUnion}{\isasymA}{\isachardoublequoteclose}\isanewline
+\ \ \ \ \isacommand{then}\isamarkupfalse%
+\ \isacommand{obtain}\isamarkupfalse%
+\ A\ \isakeyword{where}\ {\isachardoublequoteopen}x\ {\isasymin}\ A{\isachardoublequoteclose}\ \isakeyword{and}\ {\isachardoublequoteopen}A\ {\isasymin}\ {\isasymA}{\isachardoublequoteclose}\ \isacommand{{\isachardot}{\isachardot}}\isamarkupfalse%
+%
+\endisatagproof
+{\isafoldproof}%
+%
+\isadelimproof
+%
+\endisadelimproof
+%
+\begin{isamarkuptext}%
+\noindent Here we avoid to mention the final conclusion \isa{{\isachardoublequote}C{\isachardoublequote}}
+  and return to plain forward reasoning.  The rule involved in the
+  ``\hyperlink{command.ddot}{\mbox{\isa{\isacommand{{\isachardot}{\isachardot}}}}}'' proof is the same as before.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
diff -r df4e53d18ebc -r a06894e9b6e3 doc-src/IsarRef/Thy/document/Outer_Syntax.tex
--- a/doc-src/IsarRef/Thy/document/Outer_Syntax.tex	Mon Feb 09 21:09:24 2009 +0100
+++ b/doc-src/IsarRef/Thy/document/Outer_Syntax.tex	Mon Feb 09 21:13:10 2009 +0100
@@ -185,10 +185,10 @@
   Isabelle as \verb|\<forall>|.  There are infinitely many Isabelle
   symbols like this, although proper presentation is left to front-end
   tools such as {\LaTeX} or Proof~General with the X-Symbol package.
-  A list of standard Isabelle symbols that work well with these tools
-  is given in \appref{app:symbols}.  Note that \verb|\<lambda>| does
-  not belong to the \isa{letter} category, since it is already used
-  differently in the Pure term language.%
+  A list of predefined Isabelle symbols that work well with these
+  tools is given in \appref{app:symbols}.  Note that \verb|\<lambda>|
+  does not belong to the \isa{letter} category, since it is already
+  used differently in the Pure term language.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 %
diff -r df4e53d18ebc -r a06894e9b6e3 doc-src/IsarRef/Thy/document/Symbols.tex
--- a/doc-src/IsarRef/Thy/document/Symbols.tex	Mon Feb 09 21:09:24 2009 +0100
+++ b/doc-src/IsarRef/Thy/document/Symbols.tex	Mon Feb 09 21:13:10 2009 +0100
@@ -20,7 +20,7 @@
 %
 \endisadelimtheory
 %
-\isamarkupchapter{Standard Isabelle symbols \label{app:symbols}%
+\isamarkupchapter{Predefined Isabelle symbols \label{app:symbols}%
 }
 \isamarkuptrue%
 %