summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | wenzelm |

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} -\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}