Added the specification command.
authorskalberg
Mon Jul 21 10:58:16 2003 +0200 (2003-07-21)
changeset 14119fb9c392644a1
parent 14118 05416ba8eef2
child 14120 3a73850c6c7d
Added the specification command.
NEWS
doc-src/IsarRef/logics.tex
     1.1 --- a/NEWS	Mon Jul 21 08:53:56 2003 +0200
     1.2 +++ b/NEWS	Mon Jul 21 10:58:16 2003 +0200
     1.3 @@ -110,6 +110,9 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* 'specification' command added, allowing for definition by
     1.8 +specification.
     1.9 +
    1.10  * arith(_tac)
    1.11  
    1.12   - Produces a counter example if it cannot prove a goal.
     2.1 --- a/doc-src/IsarRef/logics.tex	Mon Jul 21 08:53:56 2003 +0200
     2.2 +++ b/doc-src/IsarRef/logics.tex	Mon Jul 21 10:58:16 2003 +0200
     2.3 @@ -533,6 +533,31 @@
     2.4    ;
     2.5  \end{rail}
     2.6  
     2.7 +\subsection{Definition by specification}\label{sec:hol-specification}
     2.8 +
     2.9 +\indexisarcmdof{HOL}{specification}
    2.10 +\begin{matharray}{rcl}
    2.11 +  \isarcmd{specification} & : & \isartrans{theory}{proof(prove)} \\
    2.12 +\end{matharray}
    2.13 +
    2.14 +\begin{rail}
    2.15 +'specification' '(' (decl +) ')' thmdecl? prop
    2.16 +;
    2.17 +decl: ((name ':')? term '(overloaded)'?)
    2.18 +\end{rail}
    2.19 +
    2.20 +\begin{descr}
    2.21 +\item [$\isarkeyword{specification}~decls~\phi$] sets up a
    2.22 +  goal stating the existence of terms with the property specified to
    2.23 +  hold for the constants given in $\mathit{decls}$.  After finishing
    2.24 +  the proof, the theory will be augmented with definitions for the
    2.25 +  given constants, and a theorem stating the property for these
    2.26 +  constants is returned.
    2.27 +\item[$decl$] declares a constant to be defined by the specification
    2.28 +  given.  The definition for the constant $c$ is bound to the name
    2.29 +  $c$\_def unless a theorem name is given in the declaration.
    2.30 +  Overloaded constants should be declared as such.
    2.31 +\end{descr}
    2.32  
    2.33  \subsection{(Co)Inductive sets}\label{sec:hol-inductive}
    2.34