1.1 --- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Mon Jun 02 23:12:09 2008 +0200
     1.2 +++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Mon Jun 02 23:12:23 2008 +0200
     1.3 @@ -616,54 +616,6 @@
     1.4  \end{isamarkuptext}%
     1.5  \isamarkuptrue%
     1.6  %
     1.7 -\isamarkupsection{Definition by specification \label{sec:hol-specification}%
     1.8 -}
     1.9 -\isamarkuptrue%
    1.10 -%
    1.11 -\begin{isamarkuptext}%
    1.12 -\begin{matharray}{rcl}
    1.13 -    \indexdef{HOL}{command}{specification}\hypertarget{command.HOL.specification}{\hyperlink{command.HOL.specification}{\mbox{\isa{\isacommand{specification}}}}} & : & \isartrans{theory}{proof(prove)} \\
    1.14 -    \indexdef{HOL}{command}{ax\_specification}\hypertarget{command.HOL.ax-specification}{\hyperlink{command.HOL.ax-specification}{\mbox{\isa{\isacommand{ax{\isacharunderscore}specification}}}}} & : & \isartrans{theory}{proof(prove)} \\
    1.15 -  \end{matharray}
    1.16 -
    1.17 -  \begin{rail}
    1.18 -  ('specification' | 'ax\_specification') '(' (decl +) ')' \\ (thmdecl? prop +)
    1.19 -  ;
    1.20 -  decl: ((name ':')? term '(' 'overloaded' ')'?)
    1.21 -  \end{rail}
    1.22 -
    1.23 -  \begin{descr}
    1.24 -
    1.25 -  \item [\hyperlink{command.HOL.specification}{\mbox{\isa{\isacommand{specification}}}}~\isa{{\isachardoublequote}decls\ {\isasymphi}{\isachardoublequote}}] sets up a
    1.26 -  goal stating the existence of terms with the properties specified to
    1.27 -  hold for the constants given in \isa{decls}.  After finishing the
    1.28 -  proof, the theory will be augmented with definitions for the given
    1.29 -  constants, as well as with theorems stating the properties for these
    1.30 -  constants.
    1.31 -
    1.32 -  \item [\hyperlink{command.HOL.ax-specification}{\mbox{\isa{\isacommand{ax{\isacharunderscore}specification}}}}~\isa{{\isachardoublequote}decls\ {\isasymphi}{\isachardoublequote}}] sets
    1.33 -  up a goal stating the existence of terms with the properties
    1.34 -  specified to hold for the constants given in \isa{decls}.  After
    1.35 -  finishing the proof, the theory will be augmented with axioms
    1.36 -  expressing the properties given in the first place.
    1.37 -
    1.38 -  \item [\isa{decl}] declares a constant to be defined by the
    1.39 -  specification given.  The definition for the constant \isa{c} is
    1.40 -  bound to the name \isa{c{\isacharunderscore}def} unless a theorem name is given in
    1.41 -  the declaration.  Overloaded constants should be declared as such.
    1.42 -
    1.43 -  \end{descr}
    1.44 -
    1.45 -  Whether to use \hyperlink{command.HOL.specification}{\mbox{\isa{\isacommand{specification}}}} or \hyperlink{command.HOL.ax-specification}{\mbox{\isa{\isacommand{ax{\isacharunderscore}specification}}}} is to some extent a matter of style.  \hyperlink{command.HOL.specification}{\mbox{\isa{\isacommand{specification}}}} introduces no new axioms, and so by
    1.46 -  construction cannot introduce inconsistencies, whereas \hyperlink{command.HOL.ax-specification}{\mbox{\isa{\isacommand{ax{\isacharunderscore}specification}}}} does introduce axioms, but only after the
    1.47 -  user has explicitly proven it to be safe.  A practical issue must be
    1.48 -  considered, though: After introducing two constants with the same
    1.49 -  properties using \hyperlink{command.HOL.specification}{\mbox{\isa{\isacommand{specification}}}}, one can prove
    1.50 -  that the two constants are, in fact, equal.  If this might be a
    1.51 -  problem, one should use \hyperlink{command.HOL.ax-specification}{\mbox{\isa{\isacommand{ax{\isacharunderscore}specification}}}}.%
    1.52 -\end{isamarkuptext}%
    1.53 -\isamarkuptrue%
    1.54 -%
    1.55  \isamarkupsection{Inductive and coinductive definitions \label{sec:hol-inductive}%
    1.56  }
    1.57  \isamarkuptrue%
    1.58 @@ -1140,6 +1092,54 @@
    1.59  \end{isamarkuptext}%
    1.60  \isamarkuptrue%
    1.61  %
    1.62 +\isamarkupsection{Definition by specification \label{sec:hol-specification}%
    1.63 +}
    1.64 +\isamarkuptrue%
    1.65 +%
    1.66 +\begin{isamarkuptext}%
    1.67 +\begin{matharray}{rcl}
    1.68 +    \indexdef{HOL}{command}{specification}\hypertarget{command.HOL.specification}{\hyperlink{command.HOL.specification}{\mbox{\isa{\isacommand{specification}}}}} & : & \isartrans{theory}{proof(prove)} \\
    1.69 +    \indexdef{HOL}{command}{ax\_specification}\hypertarget{command.HOL.ax-specification}{\hyperlink{command.HOL.ax-specification}{\mbox{\isa{\isacommand{ax{\isacharunderscore}specification}}}}} & : & \isartrans{theory}{proof(prove)} \\
    1.70 +  \end{matharray}
    1.71 +
    1.72 +  \begin{rail}
    1.73 +  ('specification' | 'ax\_specification') '(' (decl +) ')' \\ (thmdecl? prop +)
    1.74 +  ;
    1.75 +  decl: ((name ':')? term '(' 'overloaded' ')'?)
    1.76 +  \end{rail}
    1.77 +
    1.78 +  \begin{descr}
    1.79 +
    1.80 +  \item [\hyperlink{command.HOL.specification}{\mbox{\isa{\isacommand{specification}}}}~\isa{{\isachardoublequote}decls\ {\isasymphi}{\isachardoublequote}}] sets up a
    1.81 +  goal stating the existence of terms with the properties specified to
    1.82 +  hold for the constants given in \isa{decls}.  After finishing the
    1.83 +  proof, the theory will be augmented with definitions for the given
    1.84 +  constants, as well as with theorems stating the properties for these
    1.85 +  constants.
    1.86 +
    1.87 +  \item [\hyperlink{command.HOL.ax-specification}{\mbox{\isa{\isacommand{ax{\isacharunderscore}specification}}}}~\isa{{\isachardoublequote}decls\ {\isasymphi}{\isachardoublequote}}] sets
    1.88 +  up a goal stating the existence of terms with the properties
    1.89 +  specified to hold for the constants given in \isa{decls}.  After
    1.90 +  finishing the proof, the theory will be augmented with axioms
    1.91 +  expressing the properties given in the first place.
    1.92 +
    1.93 +  \item [\isa{decl}] declares a constant to be defined by the
    1.94 +  specification given.  The definition for the constant \isa{c} is
    1.95 +  bound to the name \isa{c{\isacharunderscore}def} unless a theorem name is given in
    1.96 +  the declaration.  Overloaded constants should be declared as such.
    1.97 +
    1.98 +  \end{descr}
    1.99 +
   1.100 +  Whether to use \hyperlink{command.HOL.specification}{\mbox{\isa{\isacommand{specification}}}} or \hyperlink{command.HOL.ax-specification}{\mbox{\isa{\isacommand{ax{\isacharunderscore}specification}}}} is to some extent a matter of style.  \hyperlink{command.HOL.specification}{\mbox{\isa{\isacommand{specification}}}} introduces no new axioms, and so by
   1.101 +  construction cannot introduce inconsistencies, whereas \hyperlink{command.HOL.ax-specification}{\mbox{\isa{\isacommand{ax{\isacharunderscore}specification}}}} does introduce axioms, but only after the
   1.102 +  user has explicitly proven it to be safe.  A practical issue must be
   1.103 +  considered, though: After introducing two constants with the same
   1.104 +  properties using \hyperlink{command.HOL.specification}{\mbox{\isa{\isacommand{specification}}}}, one can prove
   1.105 +  that the two constants are, in fact, equal.  If this might be a
   1.106 +  problem, one should use \hyperlink{command.HOL.ax-specification}{\mbox{\isa{\isacommand{ax{\isacharunderscore}specification}}}}.%
   1.107 +\end{isamarkuptext}%
   1.108 +\isamarkuptrue%
   1.109 +%
   1.110  \isadelimtheory
   1.111  %
   1.112  \endisadelimtheory