doc-src/IsarRef/Thy/document/HOL_Specific.tex
 changeset 27047 2dcdea037385 parent 27042 8fcf19f2168b child 27103 d8549f4d900b
     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 +%