373 |
373 |
374 \section{Derived proof schemes} |
374 \section{Derived proof schemes} |
375 |
375 |
376 \subsection{Generalized elimination}\label{sec:obtain} |
376 \subsection{Generalized elimination}\label{sec:obtain} |
377 |
377 |
378 \indexisarcmd{obtain} |
378 \indexisarcmd{obtain}\indexisarcmd{guess} |
379 \begin{matharray}{rcl} |
379 \begin{matharray}{rcl} |
380 \isarcmd{obtain} & : & \isartrans{proof(state)}{proof(prove)} \\ |
380 \isarcmd{obtain} & : & \isartrans{proof(state)}{proof(prove)} \\ |
|
381 \isarcmd{guess}^* & : & \isartrans{proof(state)}{proof(prove)} \\ |
381 \end{matharray} |
382 \end{matharray} |
382 |
383 |
383 Generalized elimination means that additional elements with certain properties |
384 Generalized elimination means that additional elements with certain properties |
384 may be introduced in the current context, by virtue of a locally proven |
385 may be introduced in the current context, by virtue of a locally proven |
385 ``soundness statement''. Technically speaking, the $\OBTAINNAME$ language |
386 ``soundness statement''. Technically speaking, the $\OBTAINNAME$ language |
389 eliminated from any result exported from the context later, provided that the |
390 eliminated from any result exported from the context later, provided that the |
390 corresponding parameters do \emph{not} occur in the conclusion. |
391 corresponding parameters do \emph{not} occur in the conclusion. |
391 |
392 |
392 \begin{rail} |
393 \begin{rail} |
393 'obtain' (vars + 'and') 'where' (props + 'and') |
394 'obtain' (vars + 'and') 'where' (props + 'and') |
|
395 ; |
|
396 'guess' (vars + 'and') |
394 ; |
397 ; |
395 \end{rail} |
398 \end{rail} |
396 |
399 |
397 $\OBTAINNAME$ is defined as a derived Isar command as follows, where $\vec b$ |
400 $\OBTAINNAME$ is defined as a derived Isar command as follows, where $\vec b$ |
398 shall refer to (optional) facts indicated for forward chaining. |
401 shall refer to (optional) facts indicated for forward chaining. |
413 Typically, the soundness proof is relatively straight-forward, often just by |
416 Typically, the soundness proof is relatively straight-forward, often just by |
414 canonical automated tools such as ``$\BY{simp}$'' or ``$\BY{blast}$''. |
417 canonical automated tools such as ``$\BY{simp}$'' or ``$\BY{blast}$''. |
415 Accordingly, the ``$that$'' reduction above is declared as simplification and |
418 Accordingly, the ``$that$'' reduction above is declared as simplification and |
416 introduction rule. |
419 introduction rule. |
417 |
420 |
418 \medskip |
|
419 |
|
420 In a sense, $\OBTAINNAME$ represents at the level of Isar proofs what would be |
421 In a sense, $\OBTAINNAME$ represents at the level of Isar proofs what would be |
421 meta-logical existential quantifiers and conjunctions. This concept has a |
422 meta-logical existential quantifiers and conjunctions. This concept has a |
422 broad range of useful applications, ranging from plain elimination (or |
423 broad range of useful applications, ranging from plain elimination (or |
423 introduction) of object-level existentials and conjunctions, to elimination |
424 introduction) of object-level existential and conjunctions, to elimination |
424 over results of symbolic evaluation of recursive definitions, for example. |
425 over results of symbolic evaluation of recursive definitions, for example. |
425 Also note that $\OBTAINNAME$ without parameters acts much like $\HAVENAME$, |
426 Also note that $\OBTAINNAME$ without parameters acts much like $\HAVENAME$, |
426 where the result is treated as a genuine assumption. |
427 where the result is treated as a genuine assumption. |
|
428 |
|
429 \medskip |
|
430 |
|
431 The improper variant $\isarkeyword{guess}$ is similar to $\OBTAINNAME$, but |
|
432 derives the obtained statement from the course of reasoning! The proof starts |
|
433 with a fixed goal $thesis$. The subsequent proof may refine this to anything |
|
434 of the form like $\All{\vec x} \vec\phi \Imp thesis$, but must not introduce |
|
435 new subgoals. The final goal state is then used as reduction rule for the |
|
436 obtain scheme described above. Obtained parameters $\vec x$ are marked as |
|
437 internal by default, which prevents the proof context from being polluted by |
|
438 ad-hoc variables. The variable names and type constraints given as arguments |
|
439 for $\isarkeyword{guess}$ specify a prefix of obtained parameters explicitly |
|
440 in the text. |
|
441 |
|
442 It is important to note that the facts introduced by $\OBTAINNAME$ and |
|
443 $\isarkeyword{guess}$ may not be polymorphic: any type-variables occurring |
|
444 here are fixed in the present context! |
427 |
445 |
428 |
446 |
429 \subsection{Calculational reasoning}\label{sec:calculation} |
447 \subsection{Calculational reasoning}\label{sec:calculation} |
430 |
448 |
431 \indexisarcmd{also}\indexisarcmd{finally} |
449 \indexisarcmd{also}\indexisarcmd{finally} |