--- a/doc-src/IsarRef/Thy/document/Generic.tex Mon Jun 02 23:12:09 2008 +0200
+++ b/doc-src/IsarRef/Thy/document/Generic.tex Mon Jun 02 23:12:23 2008 +0200
@@ -173,8 +173,8 @@
\item [\hyperlink{attribute.rotated}{\mbox{\isa{rotated}}}~\isa{n}] rotate the premises of a
theorem by \isa{n} (default 1).
- \item [\hyperlink{attribute.Pure.elim-format}{\mbox{\isa{Pure{\isachardot}elim{\isacharunderscore}format}}}] turns a destruction rule into
- elimination rule format, by resolving with the rule \isa{{\isachardoublequote}PROP\ A\ {\isasymLongrightarrow}\ {\isacharparenleft}PROP\ A\ {\isasymLongrightarrow}\ PROP\ B{\isacharparenright}\ {\isasymLongrightarrow}\ PROP\ B{\isachardoublequote}}.
+ \item [\hyperlink{attribute.Pure.elim-format}{\mbox{\isa{elim{\isacharunderscore}format}}}] turns a destruction rule
+ into elimination rule format, by resolving with the rule \isa{{\isachardoublequote}PROP\ A\ {\isasymLongrightarrow}\ {\isacharparenleft}PROP\ A\ {\isasymLongrightarrow}\ PROP\ B{\isacharparenright}\ {\isasymLongrightarrow}\ PROP\ B{\isachardoublequote}}.
Note that the Classical Reasoner (\secref{sec:classical}) provides
its own version of this operation.
@@ -191,6 +191,72 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
+\isamarkupsubsection{Low-level equational reasoning%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\begin{matharray}{rcl}
+ \indexdef{}{method}{subst}\hypertarget{method.subst}{\hyperlink{method.subst}{\mbox{\isa{subst}}}} & : & \isarmeth \\
+ \indexdef{}{method}{hypsubst}\hypertarget{method.hypsubst}{\hyperlink{method.hypsubst}{\mbox{\isa{hypsubst}}}} & : & \isarmeth \\
+ \indexdef{}{method}{split}\hypertarget{method.split}{\hyperlink{method.split}{\mbox{\isa{split}}}} & : & \isarmeth \\
+ \end{matharray}
+
+ \begin{rail}
+ 'subst' ('(' 'asm' ')')? ('(' (nat+) ')')? thmref
+ ;
+ 'split' ('(' 'asm' ')')? thmrefs
+ ;
+ \end{rail}
+
+ These methods provide low-level facilities for equational reasoning
+ that are intended for specialized applications only. Normally,
+ single step calculations would be performed in a structured text
+ (see also \secref{sec:calculation}), while the Simplifier methods
+ provide the canonical way for automated normalization (see
+ \secref{sec:simplifier}).
+
+ \begin{descr}
+
+ \item [\hyperlink{method.subst}{\mbox{\isa{subst}}}~\isa{eq}] performs a single substitution
+ step using rule \isa{eq}, which may be either a meta or object
+ equality.
+
+ \item [\hyperlink{method.subst}{\mbox{\isa{subst}}}~\isa{{\isachardoublequote}{\isacharparenleft}asm{\isacharparenright}\ eq{\isachardoublequote}}] substitutes in an
+ assumption.
+
+ \item [\hyperlink{method.subst}{\mbox{\isa{subst}}}~\isa{{\isachardoublequote}{\isacharparenleft}i\ {\isasymdots}\ j{\isacharparenright}\ eq{\isachardoublequote}}] performs several
+ substitutions in the conclusion. The numbers \isa{i} to \isa{j}
+ indicate the positions to substitute at. Positions are ordered from
+ the top of the term tree moving down from left to right. For
+ example, in \isa{{\isachardoublequote}{\isacharparenleft}a\ {\isacharplus}\ b{\isacharparenright}\ {\isacharplus}\ {\isacharparenleft}c\ {\isacharplus}\ d{\isacharparenright}{\isachardoublequote}} there are three positions
+ where commutativity of \isa{{\isachardoublequote}{\isacharplus}{\isachardoublequote}} is applicable: 1 refers to the
+ whole term, 2 to \isa{{\isachardoublequote}a\ {\isacharplus}\ b{\isachardoublequote}} and 3 to \isa{{\isachardoublequote}c\ {\isacharplus}\ d{\isachardoublequote}}.
+
+ If the positions in the list \isa{{\isachardoublequote}{\isacharparenleft}i\ {\isasymdots}\ j{\isacharparenright}{\isachardoublequote}} are non-overlapping
+ (e.g.\ \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{2}}\ {\isadigit{3}}{\isacharparenright}{\isachardoublequote}} in \isa{{\isachardoublequote}{\isacharparenleft}a\ {\isacharplus}\ b{\isacharparenright}\ {\isacharplus}\ {\isacharparenleft}c\ {\isacharplus}\ d{\isacharparenright}{\isachardoublequote}}) you may
+ assume all substitutions are performed simultaneously. Otherwise
+ the behaviour of \isa{subst} is not specified.
+
+ \item [\hyperlink{method.subst}{\mbox{\isa{subst}}}~\isa{{\isachardoublequote}{\isacharparenleft}asm{\isacharparenright}\ {\isacharparenleft}i\ {\isasymdots}\ j{\isacharparenright}\ eq{\isachardoublequote}}] performs the
+ substitutions in the assumptions. Positions \isa{{\isachardoublequote}{\isadigit{1}}\ {\isasymdots}\ i\isactrlsub {\isadigit{1}}{\isachardoublequote}}
+ refer to assumption 1, positions \isa{{\isachardoublequote}i\isactrlsub {\isadigit{1}}\ {\isacharplus}\ {\isadigit{1}}\ {\isasymdots}\ i\isactrlsub {\isadigit{2}}{\isachardoublequote}}
+ to assumption 2, and so on.
+
+ \item [\hyperlink{method.hypsubst}{\mbox{\isa{hypsubst}}}] performs substitution using some
+ assumption; this only works for equations of the form \isa{{\isachardoublequote}x\ {\isacharequal}\ t{\isachardoublequote}} where \isa{x} is a free or bound variable.
+
+ \item [\hyperlink{method.split}{\mbox{\isa{split}}}~\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}}] performs
+ single-step case splitting using the given rules. By default,
+ splitting is performed in the conclusion of a goal; the \isa{{\isachardoublequote}{\isacharparenleft}asm{\isacharparenright}{\isachardoublequote}} option indicates to operate on assumptions instead.
+
+ Note that the \hyperlink{method.simp}{\mbox{\isa{simp}}} method already involves repeated
+ application of split rules as declared in the current context.
+
+ \end{descr}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
\isamarkupsubsection{Further tactic emulations \label{sec:tactics}%
}
\isamarkuptrue%
@@ -498,72 +564,6 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isamarkupsubsection{Low-level equational reasoning%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-\begin{matharray}{rcl}
- \indexdef{}{method}{subst}\hypertarget{method.subst}{\hyperlink{method.subst}{\mbox{\isa{subst}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
- \indexdef{}{method}{hypsubst}\hypertarget{method.hypsubst}{\hyperlink{method.hypsubst}{\mbox{\isa{hypsubst}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
- \indexdef{}{method}{split}\hypertarget{method.split}{\hyperlink{method.split}{\mbox{\isa{split}}}}\isa{{\isachardoublequote}\isactrlsup {\isacharasterisk}{\isachardoublequote}} & : & \isarmeth \\
- \end{matharray}
-
- \begin{rail}
- 'subst' ('(' 'asm' ')')? ('(' (nat+) ')')? thmref
- ;
- 'split' ('(' 'asm' ')')? thmrefs
- ;
- \end{rail}
-
- These methods provide low-level facilities for equational reasoning
- that are intended for specialized applications only. Normally,
- single step calculations would be performed in a structured text
- (see also \secref{sec:calculation}), while the Simplifier methods
- provide the canonical way for automated normalization (see
- \secref{sec:simplifier}).
-
- \begin{descr}
-
- \item [\hyperlink{method.subst}{\mbox{\isa{subst}}}~\isa{eq}] performs a single substitution
- step using rule \isa{eq}, which may be either a meta or object
- equality.
-
- \item [\hyperlink{method.subst}{\mbox{\isa{subst}}}~\isa{{\isachardoublequote}{\isacharparenleft}asm{\isacharparenright}\ eq{\isachardoublequote}}] substitutes in an
- assumption.
-
- \item [\hyperlink{method.subst}{\mbox{\isa{subst}}}~\isa{{\isachardoublequote}{\isacharparenleft}i\ {\isasymdots}\ j{\isacharparenright}\ eq{\isachardoublequote}}] performs several
- substitutions in the conclusion. The numbers \isa{i} to \isa{j}
- indicate the positions to substitute at. Positions are ordered from
- the top of the term tree moving down from left to right. For
- example, in \isa{{\isachardoublequote}{\isacharparenleft}a\ {\isacharplus}\ b{\isacharparenright}\ {\isacharplus}\ {\isacharparenleft}c\ {\isacharplus}\ d{\isacharparenright}{\isachardoublequote}} there are three positions
- where commutativity of \isa{{\isachardoublequote}{\isacharplus}{\isachardoublequote}} is applicable: 1 refers to the
- whole term, 2 to \isa{{\isachardoublequote}a\ {\isacharplus}\ b{\isachardoublequote}} and 3 to \isa{{\isachardoublequote}c\ {\isacharplus}\ d{\isachardoublequote}}.
-
- If the positions in the list \isa{{\isachardoublequote}{\isacharparenleft}i\ {\isasymdots}\ j{\isacharparenright}{\isachardoublequote}} are non-overlapping
- (e.g.\ \isa{{\isachardoublequote}{\isacharparenleft}{\isadigit{2}}\ {\isadigit{3}}{\isacharparenright}{\isachardoublequote}} in \isa{{\isachardoublequote}{\isacharparenleft}a\ {\isacharplus}\ b{\isacharparenright}\ {\isacharplus}\ {\isacharparenleft}c\ {\isacharplus}\ d{\isacharparenright}{\isachardoublequote}}) you may
- assume all substitutions are performed simultaneously. Otherwise
- the behaviour of \isa{subst} is not specified.
-
- \item [\hyperlink{method.subst}{\mbox{\isa{subst}}}~\isa{{\isachardoublequote}{\isacharparenleft}asm{\isacharparenright}\ {\isacharparenleft}i\ {\isasymdots}\ j{\isacharparenright}\ eq{\isachardoublequote}}] performs the
- substitutions in the assumptions. Positions \isa{{\isachardoublequote}{\isadigit{1}}\ {\isasymdots}\ i\isactrlsub {\isadigit{1}}{\isachardoublequote}}
- refer to assumption 1, positions \isa{{\isachardoublequote}i\isactrlsub {\isadigit{1}}\ {\isacharplus}\ {\isadigit{1}}\ {\isasymdots}\ i\isactrlsub {\isadigit{2}}{\isachardoublequote}}
- to assumption 2, and so on.
-
- \item [\hyperlink{method.hypsubst}{\mbox{\isa{hypsubst}}}] performs substitution using some
- assumption; this only works for equations of the form \isa{{\isachardoublequote}x\ {\isacharequal}\ t{\isachardoublequote}} where \isa{x} is a free or bound variable.
-
- \item [\hyperlink{method.split}{\mbox{\isa{split}}}~\isa{{\isachardoublequote}a\isactrlsub {\isadigit{1}}\ {\isasymdots}\ a\isactrlsub n{\isachardoublequote}}] performs
- single-step case splitting using the given rules. By default,
- splitting is performed in the conclusion of a goal; the \isa{{\isachardoublequote}{\isacharparenleft}asm{\isacharparenright}{\isachardoublequote}} option indicates to operate on assumptions instead.
-
- Note that the \hyperlink{method.simp}{\mbox{\isa{simp}}} method already involves repeated
- application of split rules as declared in the current context.
-
- \end{descr}%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
\isamarkupsection{The Classical Reasoner \label{sec:classical}%
}
\isamarkuptrue%
@@ -778,7 +778,7 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isamarkupsection{General logic setup \label{sec:object-logic}%
+\isamarkupsection{Object-logic setup \label{sec:object-logic}%
}
\isamarkuptrue%
%
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex Mon Jun 02 23:12:09 2008 +0200
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex Mon Jun 02 23:12:23 2008 +0200
@@ -616,54 +616,6 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
-\isamarkupsection{Definition by specification \label{sec:hol-specification}%
-}
-\isamarkuptrue%
-%
-\begin{isamarkuptext}%
-\begin{matharray}{rcl}
- \indexdef{HOL}{command}{specification}\hypertarget{command.HOL.specification}{\hyperlink{command.HOL.specification}{\mbox{\isa{\isacommand{specification}}}}} & : & \isartrans{theory}{proof(prove)} \\
- \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)} \\
- \end{matharray}
-
- \begin{rail}
- ('specification' | 'ax\_specification') '(' (decl +) ')' \\ (thmdecl? prop +)
- ;
- decl: ((name ':')? term '(' 'overloaded' ')'?)
- \end{rail}
-
- \begin{descr}
-
- \item [\hyperlink{command.HOL.specification}{\mbox{\isa{\isacommand{specification}}}}~\isa{{\isachardoublequote}decls\ {\isasymphi}{\isachardoublequote}}] sets up a
- goal stating the existence of terms with the properties specified to
- hold for the constants given in \isa{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 [\hyperlink{command.HOL.ax-specification}{\mbox{\isa{\isacommand{ax{\isacharunderscore}specification}}}}~\isa{{\isachardoublequote}decls\ {\isasymphi}{\isachardoublequote}}] sets
- up a goal stating the existence of terms with the properties
- specified to hold for the constants given in \isa{decls}. After
- finishing the proof, the theory will be augmented with axioms
- expressing the properties given in the first place.
-
- \item [\isa{decl}] declares a constant to be defined by the
- specification given. The definition for the constant \isa{c} is
- bound to the name \isa{c{\isacharunderscore}def} unless a theorem name is given in
- the declaration. Overloaded constants should be declared as such.
-
- \end{descr}
-
- 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
- construction cannot introduce inconsistencies, whereas \hyperlink{command.HOL.ax-specification}{\mbox{\isa{\isacommand{ax{\isacharunderscore}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 \hyperlink{command.HOL.specification}{\mbox{\isa{\isacommand{specification}}}}, one can prove
- that the two constants are, in fact, equal. If this might be a
- problem, one should use \hyperlink{command.HOL.ax-specification}{\mbox{\isa{\isacommand{ax{\isacharunderscore}specification}}}}.%
-\end{isamarkuptext}%
-\isamarkuptrue%
-%
\isamarkupsection{Inductive and coinductive definitions \label{sec:hol-inductive}%
}
\isamarkuptrue%
@@ -1140,6 +1092,54 @@
\end{isamarkuptext}%
\isamarkuptrue%
%
+\isamarkupsection{Definition by specification \label{sec:hol-specification}%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\begin{matharray}{rcl}
+ \indexdef{HOL}{command}{specification}\hypertarget{command.HOL.specification}{\hyperlink{command.HOL.specification}{\mbox{\isa{\isacommand{specification}}}}} & : & \isartrans{theory}{proof(prove)} \\
+ \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)} \\
+ \end{matharray}
+
+ \begin{rail}
+ ('specification' | 'ax\_specification') '(' (decl +) ')' \\ (thmdecl? prop +)
+ ;
+ decl: ((name ':')? term '(' 'overloaded' ')'?)
+ \end{rail}
+
+ \begin{descr}
+
+ \item [\hyperlink{command.HOL.specification}{\mbox{\isa{\isacommand{specification}}}}~\isa{{\isachardoublequote}decls\ {\isasymphi}{\isachardoublequote}}] sets up a
+ goal stating the existence of terms with the properties specified to
+ hold for the constants given in \isa{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 [\hyperlink{command.HOL.ax-specification}{\mbox{\isa{\isacommand{ax{\isacharunderscore}specification}}}}~\isa{{\isachardoublequote}decls\ {\isasymphi}{\isachardoublequote}}] sets
+ up a goal stating the existence of terms with the properties
+ specified to hold for the constants given in \isa{decls}. After
+ finishing the proof, the theory will be augmented with axioms
+ expressing the properties given in the first place.
+
+ \item [\isa{decl}] declares a constant to be defined by the
+ specification given. The definition for the constant \isa{c} is
+ bound to the name \isa{c{\isacharunderscore}def} unless a theorem name is given in
+ the declaration. Overloaded constants should be declared as such.
+
+ \end{descr}
+
+ 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
+ construction cannot introduce inconsistencies, whereas \hyperlink{command.HOL.ax-specification}{\mbox{\isa{\isacommand{ax{\isacharunderscore}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 \hyperlink{command.HOL.specification}{\mbox{\isa{\isacommand{specification}}}}, one can prove
+ that the two constants are, in fact, equal. If this might be a
+ problem, one should use \hyperlink{command.HOL.ax-specification}{\mbox{\isa{\isacommand{ax{\isacharunderscore}specification}}}}.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
\isadelimtheory
%
\endisadelimtheory
--- a/doc-src/IsarRef/Thy/document/Spec.tex Mon Jun 02 23:12:09 2008 +0200
+++ b/doc-src/IsarRef/Thy/document/Spec.tex Mon Jun 02 23:12:23 2008 +0200
@@ -20,7 +20,7 @@
%
\endisadelimtheory
%
-\isamarkupchapter{Specifications%
+\isamarkupchapter{Theory specifications%
}
\isamarkuptrue%
%
@@ -1100,7 +1100,7 @@
\begin{matharray}{rcll}
\indexdef{}{command}{axioms}\hypertarget{command.axioms}{\hyperlink{command.axioms}{\mbox{\isa{\isacommand{axioms}}}}} & : & \isartrans{theory}{theory} & (axiomatic!) \\
\indexdef{}{command}{lemmas}\hypertarget{command.lemmas}{\hyperlink{command.lemmas}{\mbox{\isa{\isacommand{lemmas}}}}} & : & \isarkeep{local{\dsh}theory} \\
- \indexdef{}{command}{theorems}\hypertarget{command.theorems}{\hyperlink{command.theorems}{\mbox{\isa{\isacommand{theorems}}}}} & : & isarkeep{local{\dsh}theory} \\
+ \indexdef{}{command}{theorems}\hypertarget{command.theorems}{\hyperlink{command.theorems}{\mbox{\isa{\isacommand{theorems}}}}} & : & \isarkeep{local{\dsh}theory} \\
\end{matharray}
\begin{rail}
@@ -1319,15 +1319,15 @@
%FIXME proper antiquotations
\begin{ttbox}
val parse_ast_translation:
- (string * (Context.generic -> ast list -> ast)) list
+ (string * (Proof.context -> ast list -> ast)) list
val parse_translation:
- (string * (Context.generic -> term list -> term)) list
+ (string * (Proof.context -> term list -> term)) list
val print_translation:
- (string * (Context.generic -> term list -> term)) list
+ (string * (Proof.context -> term list -> term)) list
val typed_print_translation:
- (string * (Context.generic -> bool -> typ -> term list -> term)) list
+ (string * (Proof.context -> bool -> typ -> term list -> term)) list
val print_ast_translation:
- (string * (Context.generic -> ast list -> ast)) list
+ (string * (Proof.context -> ast list -> ast)) list
\end{ttbox}%
\end{isamarkuptext}%
\isamarkuptrue%