# HG changeset patch
# User wenzelm
# Date 965046820 -7200
# Node ID 7afb808b6b3ecafa1832c353ec861298287141c2
# Parent  f3ab2f3c19a237409d713744d4df59d05ec434fb
updated 'obtain';

diff -r f3ab2f3c19a2 -r 7afb808b6b3e doc-src/IsarRef/generic.tex
--- a/doc-src/IsarRef/generic.tex	Mon Jul 31 12:50:33 2000 +0200
+++ b/doc-src/IsarRef/generic.tex	Mon Jul 31 14:33:40 2000 +0200
@@ -206,47 +206,40 @@
 
 \indexisarcmd{obtain}
 \begin{matharray}{rcl}
-  \isarcmd{obtain} & : & \isartrans{proof(prove)}{proof(state)} \\
+  \isarcmd{obtain} & : & \isartrans{proof(state)}{proof(prove)} \\
 \end{matharray}
 
-Generalized existence reasoning means that additional elements with certain
-properties are introduced, together with a soundness proof of that context
-change (the rest of the main goal is left unchanged).
-
-Syntactically, the $\OBTAINNAME$ language element is like an initial proof
-method to the present goal, followed by a proof of its additional claim,
-followed by the actual context commands (using the syntax of $\FIXNAME$ and
-$\ASSUMENAME$, see \S\ref{sec:proof-context}).
+Generalized existence means that additional elements with certain properties
+may introduced in the current context.  Technically, the $\OBTAINNAME$
+language element is like a declaration of $\FIXNAME$ and $\ASSUMENAME$ (see
+also see \S\ref{sec:proof-context}), together with a soundness proof of its
+additional claim.  According to the nature of existential reasoning,
+assumptions get eliminated from any result exported from the context later,
+provided that the corresponding parameters do \emph{not} occur in the
+conclusion.
 
 \begin{rail}
   'obtain' (vars + 'and') comment? \\ 'where' (assm comment? + 'and')
   ;
 \end{rail}
 
-$\OBTAINNAME$ is defined as a derived Isar command as follows; here the
-preceding goal shall be $\psi$, with (optional) facts $\vec b$ indicated for
-forward chaining.
+$\OBTAINNAME$ is defined as a derived Isar command as follows, where $\vec b$
+shall refer to (optional) facts indicated for forward chaining.
 \begin{matharray}{l}
-  \OBTAIN{\vec x}{a}{\vec \phi}~~\langle proof\rangle \equiv {} \\[0.5ex]
-  \quad \PROOF{succeed} \\
-  \qquad \DEF{}{thesis \equiv \psi} \\
-  \qquad \PRESUME{that}{\All{\vec x} \vec\phi \Imp thesis} \\
-  \qquad \FROM{\vec b}~\SHOW{}{thesis}~~\langle proof\rangle \\
-  \quad \NEXT \\
-  \qquad \FIX{\vec x}~\ASSUME{a}{\vec\phi} \\
+  \langle facts~\vec b\rangle \\
+  \OBTAIN{\vec x}{a}{\vec \phi}~~\langle proof\rangle \equiv {} \\[1ex]
+  \quad \BG \\
+  \qquad \FIX{thesis} \\
+  \qquad \ASSUME{that [simp, intro]}{\All{\vec x} \vec\phi \Imp thesis} \\
+  \qquad \FROM{\vec b}~\HAVE{}{thesis}~~\langle proof\rangle \\
+  \quad \EN \\
+  \quad \FIX{\vec x}~\ASSUMENAME^{obtained}~{a}~{\vec\phi} \\
 \end{matharray}
 
 Typically, the soundness proof is relatively straight-forward, often just by
 canonical automated tools such as $\BY{simp}$ (see \S\ref{sec:simp}) or
-$\BY{blast}$ (see \S\ref{sec:classical-auto}).  Note that the ``$that$''
-presumption above is usually declared as simplification and (unsafe)
-introduction rule, depending on the object-logic's policy,
-though.\footnote{HOL and HOLCF do this already.}
-
-The original goal statement is wrapped into a local definition in order to
-avoid any automated tools descending into it.  Usually, any statement would
-admit the intended reduction anyway; only in very rare cases $thesis_def$ has
-to be expanded to complete the soundness proof.
+$\BY{blast}$ (see \S\ref{sec:classical-auto}).  Accordingly, the ``$that$''
+reduction above is declared as simplification and introduction rule.
 
 \medskip
 
@@ -255,6 +248,8 @@
 broad range of useful applications, ranging from plain elimination (or even
 introduction) of object-level existentials and conjunctions, to elimination
 over results of symbolic evaluation of recursive definitions, for example.
+Also note that $\OBTAINNAME$ without parameters acts much like $\HAVENAME$,
+where the result is treated as an assumption.
 
 
 \section{Miscellaneous methods and attributes}