added guess;
Sat, 15 Oct 2005 00:08:13 +0200
changeset 17864 b039ea8bb965
parent 17863 efb52ea32b36
child 17865 5b0c3dcfbad2
added guess;
--- 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}
   \isarcmd{obtain} & : & \isartrans{proof(state)}{proof(prove)} \\
+  \isarcmd{guess}^* & : & \isartrans{proof(state)}{proof(prove)} \\
 Generalized elimination means that additional elements with certain properties
@@ -392,6 +393,8 @@
   'obtain' (vars + 'and') 'where' (props + 'and')
+  'guess' (vars + 'and')
+  ;
 $\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.
 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.
+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}