--- a/NEWS Sat Apr 14 23:52:17 2012 +0100
+++ b/NEWS Sun Apr 15 13:15:14 2012 +0200
@@ -50,6 +50,30 @@
*** Pure ***
+* Auxiliary contexts indicate block structure for specifications with
+additional parameters and assumptions. Such unnamed contexts may be
+nested within other targets, like 'theory', 'locale', 'class',
+'instantiation' etc. Results from the local context are generalized
+accordingly and applied to the enclosing target context. Example:
+
+ context
+ fixes x y z :: 'a
+ assumes xy: "x = y" and yz: "y = z"
+ begin
+
+ lemma my_trans: "x = z" using xy yz by simp
+
+ end
+
+ thm my_trans
+
+The most basic application is to factor-out context elements of
+several fixes/assumes/shows theorem statements, e.g. see
+~~/src/HOL/Isar_Examples/Group_Context.thy
+
+Any other local theory specification element works within the "context
+... begin ... end" block as well.
+
* Rule composition via attribute "OF" (or ML functions OF/MRS) is more
tolerant against multiple unifiers, as long as the final result is
unique. (As before, rules are composed in canonical right-to-left
--- a/doc-src/IsarRef/Thy/Spec.thy Sat Apr 14 23:52:17 2012 +0100
+++ b/doc-src/IsarRef/Thy/Spec.thy Sun Apr 15 13:15:14 2012 +0200
@@ -104,14 +104,20 @@
section {* Local theory targets \label{sec:target} *}
-text {*
- A local theory target is a context managed separately within the
- enclosing theory. Contexts may introduce parameters (fixed
+text {* A local theory target is a context managed separately within
+ the enclosing theory. Contexts may introduce parameters (fixed
variables) and assumptions (hypotheses). Definitions and theorems
- depending on the context may be added incrementally later on. Named
- contexts refer to locales (cf.\ \secref{sec:locale}) or type classes
- (cf.\ \secref{sec:class}); the name ``@{text "-"}'' signifies the
- global theory context.
+ depending on the context may be added incrementally later on.
+
+ \emph{Named contexts} refer to locales (cf.\ \secref{sec:locale}) or
+ type classes (cf.\ \secref{sec:class}); the name ``@{text "-"}''
+ signifies the global theory context.
+
+ \emph{Unnamed contexts} may introduce additional parameters and
+ assumptions, and results produced in the context are generalized
+ accordingly. Such auxiliary contexts may be nested within other
+ targets, like @{command "locale"}, @{command "class"}, @{command
+ "instantiation"}, @{command "overloading"}.
\begin{matharray}{rcll}
@{command_def "context"} & : & @{text "theory \<rightarrow> local_theory"} \\
@@ -119,7 +125,7 @@
\end{matharray}
@{rail "
- @@{command context} @{syntax nameref} @'begin'
+ @@{command context} (@{syntax nameref} | (@{syntax context_elem}+)) @'begin'
;
@{syntax_def target}: '(' @'in' @{syntax nameref} ')'
@@ -127,16 +133,23 @@
\begin{description}
- \item @{command "context"}~@{text "c \<BEGIN>"} recommences an
- existing locale or class context @{text c}. Note that locale and
- class definitions allow to include the @{keyword "begin"} keyword as
- well, in order to continue the local theory immediately after the
- initial specification.
+ \item @{command "context"}~@{text "c \<BEGIN>"} opens a named
+ context, by recommencing an existing locale or class @{text c}.
+ Note that locale and class definitions allow to include the
+ @{keyword "begin"} keyword as well, in order to continue the local
+ theory immediately after the initial specification.
+
+ \item @{command "context"}~@{text "elements \<BEGIN>"} opens an
+ unnamed context, by extending the enclosing global or local theory
+ target by the given context elements (@{text "\<FIXES>"}, @{text
+ "\<ASSUMES>"} etc.). This means any results stemming from
+ definitions and proofs in the extended context will be exported into
+ the enclosing target by lifting over extra parameters and premises.
- \item @{command (local) "end"} concludes the current local theory
- and continues the enclosing global theory. Note that a global
- @{command (global) "end"} has a different meaning: it concludes the
- theory itself (\secref{sec:begin-thy}).
+ \item @{command (local) "end"} concludes the current local theory,
+ according to the nesting of contexts. Note that a global @{command
+ (global) "end"} has a different meaning: it concludes the theory
+ itself (\secref{sec:begin-thy}).
\item @{text "("}@{keyword_def "in"}~@{text "c)"} given after any
local theory command specifies an immediate target, e.g.\
@@ -166,7 +179,11 @@
generalizing the parameters of the context. For example, @{text "a:
B[x]"} becomes @{text "c.a: A[?x] \<Longrightarrow> B[?x]"}, again for arbitrary
@{text "?x"}.
-*}
+
+ \medskip The Isabelle/HOL library contains numerous applications of
+ locales and classes, e.g.\ see @{file "~~/src/HOL/Algebra"}. An
+ example for an unnamed auxiliary contexts is given in @{file
+ "~~/src/HOL/Isar_Examples/Group_Context.thy"}. *}
section {* Basic specification elements *}
--- a/doc-src/IsarRef/Thy/document/Spec.tex Sat Apr 14 23:52:17 2012 +0100
+++ b/doc-src/IsarRef/Thy/document/Spec.tex Sun Apr 15 13:15:14 2012 +0200
@@ -167,13 +167,19 @@
\isamarkuptrue%
%
\begin{isamarkuptext}%
-A local theory target is a context managed separately within the
- enclosing theory. Contexts may introduce parameters (fixed
+A local theory target is a context managed separately within
+ the enclosing theory. Contexts may introduce parameters (fixed
variables) and assumptions (hypotheses). Definitions and theorems
- depending on the context may be added incrementally later on. Named
- contexts refer to locales (cf.\ \secref{sec:locale}) or type classes
- (cf.\ \secref{sec:class}); the name ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{22}{\isachardoublequote}}}'' signifies the
- global theory context.
+ depending on the context may be added incrementally later on.
+
+ \emph{Named contexts} refer to locales (cf.\ \secref{sec:locale}) or
+ type classes (cf.\ \secref{sec:class}); the name ``\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{2D}{\isacharminus}}{\isaliteral{22}{\isachardoublequote}}}''
+ signifies the global theory context.
+
+ \emph{Unnamed contexts} may introduce additional parameters and
+ assumptions, and results produced in the context are generalized
+ accordingly. Such auxiliary contexts may be nested within other
+ targets, like \hyperlink{command.locale}{\mbox{\isa{\isacommand{locale}}}}, \hyperlink{command.class}{\mbox{\isa{\isacommand{class}}}}, \hyperlink{command.instantiation}{\mbox{\isa{\isacommand{instantiation}}}}, \hyperlink{command.overloading}{\mbox{\isa{\isacommand{overloading}}}}.
\begin{matharray}{rcll}
\indexdef{}{command}{context}\hypertarget{command.context}{\hyperlink{command.context}{\mbox{\isa{\isacommand{context}}}}} & : & \isa{{\isaliteral{22}{\isachardoublequote}}theory\ {\isaliteral{5C3C72696768746172726F773E}{\isasymrightarrow}}\ local{\isaliteral{5F}{\isacharunderscore}}theory{\isaliteral{22}{\isachardoublequote}}} \\
@@ -181,9 +187,16 @@
\end{matharray}
\begin{railoutput}
-\rail@begin{1}{}
+\rail@begin{3}{}
\rail@term{\hyperlink{command.context}{\mbox{\isa{\isacommand{context}}}}}[]
+\rail@bar
\rail@nont{\hyperlink{syntax.nameref}{\mbox{\isa{nameref}}}}[]
+\rail@nextbar{1}
+\rail@plus
+\rail@nont{\hyperlink{syntax.context-elem}{\mbox{\isa{context{\isaliteral{5F}{\isacharunderscore}}elem}}}}[]
+\rail@nextplus{2}
+\rail@endplus
+\rail@endbar
\rail@term{\isa{\isakeyword{begin}}}[]
\rail@end
\rail@begin{1}{\indexdef{}{syntax}{target}\hypertarget{syntax.target}{\hyperlink{syntax.target}{\mbox{\isa{target}}}}}
@@ -197,16 +210,21 @@
\begin{description}
- \item \hyperlink{command.context}{\mbox{\isa{\isacommand{context}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}c\ {\isaliteral{5C3C424547494E3E}{\isasymBEGIN}}{\isaliteral{22}{\isachardoublequote}}} recommences an
- existing locale or class context \isa{c}. Note that locale and
- class definitions allow to include the \hyperlink{keyword.begin}{\mbox{\isa{\isakeyword{begin}}}} keyword as
- well, in order to continue the local theory immediately after the
- initial specification.
+ \item \hyperlink{command.context}{\mbox{\isa{\isacommand{context}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}c\ {\isaliteral{5C3C424547494E3E}{\isasymBEGIN}}{\isaliteral{22}{\isachardoublequote}}} opens a named
+ context, by recommencing an existing locale or class \isa{c}.
+ Note that locale and class definitions allow to include the
+ \hyperlink{keyword.begin}{\mbox{\isa{\isakeyword{begin}}}} keyword as well, in order to continue the local
+ theory immediately after the initial specification.
+
+ \item \hyperlink{command.context}{\mbox{\isa{\isacommand{context}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}elements\ {\isaliteral{5C3C424547494E3E}{\isasymBEGIN}}{\isaliteral{22}{\isachardoublequote}}} opens an
+ unnamed context, by extending the enclosing global or local theory
+ target by the given context elements (\isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C46495845533E}{\isasymFIXES}}{\isaliteral{22}{\isachardoublequote}}}, \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{5C3C415353554D45533E}{\isasymASSUMES}}{\isaliteral{22}{\isachardoublequote}}} etc.). This means any results stemming from
+ definitions and proofs in the extended context will be exported into
+ the enclosing target by lifting over extra parameters and premises.
- \item \hyperlink{command.local.end}{\mbox{\isa{\isacommand{end}}}} concludes the current local theory
- and continues the enclosing global theory. Note that a global
- \hyperlink{command.global.end}{\mbox{\isa{\isacommand{end}}}} has a different meaning: it concludes the
- theory itself (\secref{sec:begin-thy}).
+ \item \hyperlink{command.local.end}{\mbox{\isa{\isacommand{end}}}} concludes the current local theory,
+ according to the nesting of contexts. Note that a global \hyperlink{command.global.end}{\mbox{\isa{\isacommand{end}}}} has a different meaning: it concludes the theory
+ itself (\secref{sec:begin-thy}).
\item \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{28}{\isacharparenleft}}{\isaliteral{22}{\isachardoublequote}}}\indexdef{}{keyword}{in}\hypertarget{keyword.in}{\hyperlink{keyword.in}{\mbox{\isa{\isakeyword{in}}}}}~\isa{{\isaliteral{22}{\isachardoublequote}}c{\isaliteral{29}{\isacharparenright}}{\isaliteral{22}{\isachardoublequote}}} given after any
local theory command specifies an immediate target, e.g.\
@@ -233,7 +251,11 @@
Theorems are exported by discharging the assumptions and
generalizing the parameters of the context. For example, \isa{{\isaliteral{22}{\isachardoublequote}}a{\isaliteral{3A}{\isacharcolon}}\ B{\isaliteral{5B}{\isacharbrackleft}}x{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}} becomes \isa{{\isaliteral{22}{\isachardoublequote}}c{\isaliteral{2E}{\isachardot}}a{\isaliteral{3A}{\isacharcolon}}\ A{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{3F}{\isacharquery}}x{\isaliteral{5D}{\isacharbrackright}}\ {\isaliteral{5C3C4C6F6E6772696768746172726F773E}{\isasymLongrightarrow}}\ B{\isaliteral{5B}{\isacharbrackleft}}{\isaliteral{3F}{\isacharquery}}x{\isaliteral{5D}{\isacharbrackright}}{\isaliteral{22}{\isachardoublequote}}}, again for arbitrary
- \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3F}{\isacharquery}}x{\isaliteral{22}{\isachardoublequote}}}.%
+ \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{3F}{\isacharquery}}x{\isaliteral{22}{\isachardoublequote}}}.
+
+ \medskip The Isabelle/HOL library contains numerous applications of
+ locales and classes, e.g.\ see \verb|~~/src/HOL/Algebra|. An
+ example for an unnamed auxiliary contexts is given in \verb|~~/src/HOL/Isar_Examples/Group_Context.thy|.%
\end{isamarkuptext}%
\isamarkuptrue%
%