doc-src/IsarRef/generic.tex
changeset 9480 7afb808b6b3e
parent 9438 6131037f8a11
child 9606 1bf495402ae9
     1.1 --- a/doc-src/IsarRef/generic.tex	Mon Jul 31 12:50:33 2000 +0200
     1.2 +++ b/doc-src/IsarRef/generic.tex	Mon Jul 31 14:33:40 2000 +0200
     1.3 @@ -206,47 +206,40 @@
     1.4  
     1.5  \indexisarcmd{obtain}
     1.6  \begin{matharray}{rcl}
     1.7 -  \isarcmd{obtain} & : & \isartrans{proof(prove)}{proof(state)} \\
     1.8 +  \isarcmd{obtain} & : & \isartrans{proof(state)}{proof(prove)} \\
     1.9  \end{matharray}
    1.10  
    1.11 -Generalized existence reasoning means that additional elements with certain
    1.12 -properties are introduced, together with a soundness proof of that context
    1.13 -change (the rest of the main goal is left unchanged).
    1.14 -
    1.15 -Syntactically, the $\OBTAINNAME$ language element is like an initial proof
    1.16 -method to the present goal, followed by a proof of its additional claim,
    1.17 -followed by the actual context commands (using the syntax of $\FIXNAME$ and
    1.18 -$\ASSUMENAME$, see \S\ref{sec:proof-context}).
    1.19 +Generalized existence means that additional elements with certain properties
    1.20 +may introduced in the current context.  Technically, the $\OBTAINNAME$
    1.21 +language element is like a declaration of $\FIXNAME$ and $\ASSUMENAME$ (see
    1.22 +also see \S\ref{sec:proof-context}), together with a soundness proof of its
    1.23 +additional claim.  According to the nature of existential reasoning,
    1.24 +assumptions get eliminated from any result exported from the context later,
    1.25 +provided that the corresponding parameters do \emph{not} occur in the
    1.26 +conclusion.
    1.27  
    1.28  \begin{rail}
    1.29    'obtain' (vars + 'and') comment? \\ 'where' (assm comment? + 'and')
    1.30    ;
    1.31  \end{rail}
    1.32  
    1.33 -$\OBTAINNAME$ is defined as a derived Isar command as follows; here the
    1.34 -preceding goal shall be $\psi$, with (optional) facts $\vec b$ indicated for
    1.35 -forward chaining.
    1.36 +$\OBTAINNAME$ is defined as a derived Isar command as follows, where $\vec b$
    1.37 +shall refer to (optional) facts indicated for forward chaining.
    1.38  \begin{matharray}{l}
    1.39 -  \OBTAIN{\vec x}{a}{\vec \phi}~~\langle proof\rangle \equiv {} \\[0.5ex]
    1.40 -  \quad \PROOF{succeed} \\
    1.41 -  \qquad \DEF{}{thesis \equiv \psi} \\
    1.42 -  \qquad \PRESUME{that}{\All{\vec x} \vec\phi \Imp thesis} \\
    1.43 -  \qquad \FROM{\vec b}~\SHOW{}{thesis}~~\langle proof\rangle \\
    1.44 -  \quad \NEXT \\
    1.45 -  \qquad \FIX{\vec x}~\ASSUME{a}{\vec\phi} \\
    1.46 +  \langle facts~\vec b\rangle \\
    1.47 +  \OBTAIN{\vec x}{a}{\vec \phi}~~\langle proof\rangle \equiv {} \\[1ex]
    1.48 +  \quad \BG \\
    1.49 +  \qquad \FIX{thesis} \\
    1.50 +  \qquad \ASSUME{that [simp, intro]}{\All{\vec x} \vec\phi \Imp thesis} \\
    1.51 +  \qquad \FROM{\vec b}~\HAVE{}{thesis}~~\langle proof\rangle \\
    1.52 +  \quad \EN \\
    1.53 +  \quad \FIX{\vec x}~\ASSUMENAME^{obtained}~{a}~{\vec\phi} \\
    1.54  \end{matharray}
    1.55  
    1.56  Typically, the soundness proof is relatively straight-forward, often just by
    1.57  canonical automated tools such as $\BY{simp}$ (see \S\ref{sec:simp}) or
    1.58 -$\BY{blast}$ (see \S\ref{sec:classical-auto}).  Note that the ``$that$''
    1.59 -presumption above is usually declared as simplification and (unsafe)
    1.60 -introduction rule, depending on the object-logic's policy,
    1.61 -though.\footnote{HOL and HOLCF do this already.}
    1.62 -
    1.63 -The original goal statement is wrapped into a local definition in order to
    1.64 -avoid any automated tools descending into it.  Usually, any statement would
    1.65 -admit the intended reduction anyway; only in very rare cases $thesis_def$ has
    1.66 -to be expanded to complete the soundness proof.
    1.67 +$\BY{blast}$ (see \S\ref{sec:classical-auto}).  Accordingly, the ``$that$''
    1.68 +reduction above is declared as simplification and introduction rule.
    1.69  
    1.70  \medskip
    1.71  
    1.72 @@ -255,6 +248,8 @@
    1.73  broad range of useful applications, ranging from plain elimination (or even
    1.74  introduction) of object-level existentials and conjunctions, to elimination
    1.75  over results of symbolic evaluation of recursive definitions, for example.
    1.76 +Also note that $\OBTAINNAME$ without parameters acts much like $\HAVENAME$,
    1.77 +where the result is treated as an assumption.
    1.78  
    1.79  
    1.80  \section{Miscellaneous methods and attributes}