# HG changeset patch # User wenzelm # Date 1212441143 -7200 # Node ID 2dcdea03738591fc5ecfea6b14317e66690f1de0 # Parent 51c2635dd89cb773c39634f8afd81dcc8ab57387 updated generated file; diff -r 51c2635dd89c -r 2dcdea037385 doc-src/IsarRef/Thy/document/Generic.tex --- 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% % diff -r 51c2635dd89c -r 2dcdea037385 doc-src/IsarRef/Thy/document/HOL_Specific.tex --- 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 diff -r 51c2635dd89c -r 2dcdea037385 doc-src/IsarRef/Thy/document/Spec.tex --- 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%