# HG changeset patch
# User wenzelm
# Date 1129327693 -7200
# Node ID b039ea8bb9656a272c959109dbf54a5d37dded61
# Parent  efb52ea32b36880d6fd8cb88a605949dd7922eb4
added guess;

diff -r efb52ea32b36 -r b039ea8bb965 doc-src/IsarRef/generic.tex
--- a/doc-src/IsarRef/generic.tex	Sat Oct 15 00:08:12 2005 +0200
+++ b/doc-src/IsarRef/generic.tex	Sat Oct 15 00:08:13 2005 +0200
@@ -375,9 +375,10 @@
 
 \subsection{Generalized elimination}\label{sec:obtain}
 
-\indexisarcmd{obtain}
+\indexisarcmd{obtain}\indexisarcmd{guess}
 \begin{matharray}{rcl}
   \isarcmd{obtain} & : & \isartrans{proof(state)}{proof(prove)} \\
+  \isarcmd{guess}^* & : & \isartrans{proof(state)}{proof(prove)} \\
 \end{matharray}
 
 Generalized elimination means that additional elements with certain properties
@@ -392,6 +393,8 @@
 \begin{rail}
   'obtain' (vars + 'and') 'where' (props + 'and')
   ;
+  'guess' (vars + 'and')
+  ;
 \end{rail}
 
 $\OBTAINNAME$ is defined as a derived Isar command as follows, where $\vec b$
@@ -415,16 +418,31 @@
 Accordingly, the ``$that$'' reduction above is declared as simplification and
 introduction rule.
 
-\medskip
-
 In a sense, $\OBTAINNAME$ represents at the level of Isar proofs what would be
 meta-logical existential quantifiers and conjunctions.  This concept has a
 broad range of useful applications, ranging from plain elimination (or
-introduction) of object-level existentials and conjunctions, to elimination
+introduction) of object-level existential 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 a genuine assumption.
 
+\medskip
+
+The improper variant $\isarkeyword{guess}$ is similar to $\OBTAINNAME$, but
+derives the obtained statement from the course of reasoning!  The proof starts
+with a fixed goal $thesis$.  The subsequent proof may refine this to anything
+of the form like $\All{\vec x} \vec\phi \Imp thesis$, but must not introduce
+new subgoals.  The final goal state is then used as reduction rule for the
+obtain scheme described above.  Obtained parameters $\vec x$ are marked as
+internal by default, which prevents the proof context from being polluted by
+ad-hoc variables.  The variable names and type constraints given as arguments
+for $\isarkeyword{guess}$ specify a prefix of obtained parameters explicitly
+in the text.
+
+It is important to note that the facts introduced by $\OBTAINNAME$ and
+$\isarkeyword{guess}$ may not be polymorphic: any type-variables occurring
+here are fixed in the present context!
+
 
 \subsection{Calculational reasoning}\label{sec:calculation}