author skalberg Sat, 17 Apr 2004 20:04:23 +0200 changeset 14619 8876ad83b1fb parent 14618 068bb99f3ebd child 14620 1be590fd2422
Added documentation for ax_specification, as well as a small comparison of ax_specification and specification.
--- a/doc-src/IsarRef/logics.tex	Sat Apr 17 17:08:53 2004 +0200
+++ b/doc-src/IsarRef/logics.tex	Sat Apr 17 20:04:23 2004 +0200
@@ -538,10 +538,11 @@
\indexisarcmdof{HOL}{specification}
\begin{matharray}{rcl}
\isarcmd{specification} & : & \isartrans{theory}{proof(prove)} \\
+  \isarcmd{ax_specification} & : & \isartrans{theory}{proof(prove)} \\
\end{matharray}

\begin{rail}
-'specification' '(' (decl +) ')' (thmdecl? prop +)
+('specification' | 'ax\_specification') '(' (decl +) ')' \\ (thmdecl? prop +)
;
\end{rail}
@@ -552,12 +553,26 @@
constants given in $\mathit{decls}$.  After finishing the proof, the
theory will be augmented with definitions for the given constants,
as well as with theorems stating the properties for these constants.
+\item [$\isarkeyword{ax_specification}~decls~\phi$] sets up a goal stating
+  the existence of terms with the properties specified to hold for the
+  constants given in $\mathit{decls}$.  After finishing the proof, the
+  theory will be augmented with axioms expressing the properties given
+  in the first place.
\item[$decl$] declares a constant to be defined by the specification
given.  The definition for the constant $c$ is bound to the name
$c$\_def unless a theorem name is given in the declaration.
Overloaded constants should be declared as such.
\end{descr}

+Whether to use $\isarkeyword{specification}$ or $\isarkeyword{ax_specification}$
+is to some extent a matter of style.  $\isarkeyword{specification}$ introduces no new axioms,
+and so by construction cannot introduce inconsistencies, whereas $\isarkeyword{ax_specification}$
+does introduce axioms, but only after the user has explicitly proven it to be
+safe.  A practical issue must be considered, though: After introducing two constants
+with the same properties using $\isarkeyword{specification}$, one can prove
+that the two constants are, in fact, equal.  If this might be a problem,
+one should use $\isarkeyword{ax_specification}$.
+
\subsection{(Co)Inductive sets}\label{sec:hol-inductive}

\indexisarcmdof{HOL}{inductive}\indexisarcmdof{HOL}{coinductive}\indexisarattof{HOL}{mono}