author | wenzelm |

Mon Jul 31 14:33:40 2000 +0200 (2000-07-31) | |

changeset 9480 | 7afb808b6b3e |

parent 9479 | f3ab2f3c19a2 |

child 9481 | b16624f1ea38 |

updated 'obtain';

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}