1.1 --- a/NEWS Wed Oct 02 23:05:36 2013 +0200
1.2 +++ b/NEWS Thu Oct 03 00:39:16 2013 +0200
1.3 @@ -103,10 +103,11 @@
1.4
1.5 *** Pure ***
1.6
1.7 -* Target-sensitive commands 'interpretation' and 'sublocale'.
1.8 -Particularly, 'interpretation' now allows for non-persistent
1.9 -interpretation within "context ... begin ... end" blocks. See
1.10 -"isar-ref" manual for details.
1.11 +* Commands 'interpretation' and 'sublocale' are now target-sensitive.
1.12 +In particular, 'interpretation' allows for non-persistent
1.13 +interpretation within "context ... begin ... end" blocks offering a
1.14 +light-weight alternative to 'sublocale'. See "isar-ref" manual for
1.15 +details.
1.16
1.17 * Improved locales diagnostic command 'print_dependencies'.
1.18
2.1 --- a/src/Doc/IsarRef/Spec.thy Wed Oct 02 23:05:36 2013 +0200
2.2 +++ b/src/Doc/IsarRef/Spec.thy Thu Oct 03 00:39:16 2013 +0200
2.3 @@ -257,7 +257,7 @@
2.4 including trace by metis
2.5
2.6
2.7 -section {* Basic specification elements *}
2.8 +section {* Basic specification elements \label{sec:basic-spec} *}
2.9
2.10 text {*
2.11 \begin{matharray}{rcll}
2.12 @@ -400,23 +400,36 @@
2.13 section {* Locales \label{sec:locale} *}
2.14
2.15 text {*
2.16 - Locales are parametric named local contexts, consisting of a list of
2.17 - declaration elements that are modeled after the Isar proof context
2.18 - commands (cf.\ \secref{sec:proof-context}).
2.19 + A locale is a functor that maps parameters (including implicit type
2.20 + parameters) and a specification to a list of declarations. The
2.21 + syntax of locales is modeled after the Isar proof context commands
2.22 + (cf.\ \secref{sec:proof-context}).
2.23 +
2.24 + Locale hierarchies are supported by maintaining a graph of
2.25 + dependencies between locale instances in the global theory.
2.26 + Dependencies may be introduced through import (where a locale is
2.27 + defined as sublocale of the imported instances) or by proving that
2.28 + an existing locale is a sublocale of one or several locale
2.29 + instances.
2.30 +
2.31 + A locale may be opened with the purpose of appending to its list of
2.32 + declarations (cf.\ \secref{sec:target}). When opening a locale
2.33 + declarations from all dependencies are collected and are presented
2.34 + as a local theory. In this process, which is called \emph{roundup},
2.35 + redundant locale instances are omitted. A locale instance is
2.36 + redundant if it is subsumed by an instance encountered earlier. A
2.37 + more detailed description of this process is available elsewhere
2.38 + \cite{Ballarin2013}.
2.39 *}
2.40
2.41
2.42 subsection {* Locale expressions \label{sec:locale-expr} *}
2.43
2.44 text {*
2.45 - A \emph{locale expression} denotes a structured context composed of
2.46 - instances of existing locales. The context consists of a list of
2.47 - instances of declaration elements from the locales. Two locale
2.48 - instances are equal if they are of the same locale and the
2.49 - parameters are instantiated with equivalent terms. Declaration
2.50 - elements from equal instances are never repeated, thus avoiding
2.51 - duplicate declarations. More precisely, declarations from instances
2.52 - that are subsumed by earlier instances are omitted.
2.53 + A \emph{locale expression} denotes a context composed of instances
2.54 + of existing locales. The context consists of the declaration
2.55 + elements from the locale instances. Redundant locale instances are
2.56 + omitted according to roundup.
2.57
2.58 @{rail "
2.59 @{syntax_def locale_expr}: (instance + '+') (@'for' (@{syntax \"fixes\"} + @'and'))?
2.60 @@ -432,7 +445,7 @@
2.61
2.62 A locale instance consists of a reference to a locale and either
2.63 positional or named parameter instantiations. Identical
2.64 - instantiations (that is, those that instante a parameter by itself)
2.65 + instantiations (that is, those that instantiate a parameter by itself)
2.66 may be omitted. The notation `@{text "_"}' enables to omit the
2.67 instantiation for a parameter inside a positional instantiation.
2.68
2.69 @@ -451,7 +464,8 @@
2.70 ``\texttt{?}'' nor ``\texttt{!}'' are present, the command's default
2.71 is used. For @{command "interpretation"} and @{command "interpret"}
2.72 the default is ``mandatory'', for @{command "locale"} and @{command
2.73 - "sublocale"} the default is ``optional''.
2.74 + "sublocale"} the default is ``optional''. Qualifiers play no role
2.75 + in determining whether one locale instance subsumes another.
2.76 *}
2.77
2.78
2.79 @@ -497,14 +511,15 @@
2.80 care of the most general typing that the combined context elements
2.81 may acquire.
2.82
2.83 - The @{text import} consists of a structured locale expression; see
2.84 - \secref{sec:proof-context} above. Its for clause defines the local
2.85 - parameters of the @{text import}. In addition, locale parameters
2.86 - whose instantance is omitted automatically extend the (possibly
2.87 - empty) for clause: they are inserted at its beginning. This means
2.88 - that these parameters may be referred to from within the expression
2.89 - and also in the subsequent context elements and provides a
2.90 - notational convenience for the inheritance of parameters in locale
2.91 + The @{text import} consists of a locale expression; see
2.92 + \secref{sec:proof-context} above. Its @{keyword "for"} clause defines
2.93 + the parameters of @{text import}. These are parameters of
2.94 + the defined locale. Locale parameters whose instantiation is
2.95 + omitted automatically extend the (possibly empty) @{keyword "for"}
2.96 + clause: they are inserted at its beginning. This means that these
2.97 + parameters may be referred to from within the expression and also in
2.98 + the subsequent context elements and provides a notational
2.99 + convenience for the inheritance of parameters in locale
2.100 declarations.
2.101
2.102 The @{text body} consists of context elements.
2.103 @@ -520,7 +535,7 @@
2.104 \item @{element "constrains"}~@{text "x :: \<tau>"} introduces a type
2.105 constraint @{text \<tau>} on the local parameter @{text x}. This
2.106 element is deprecated. The type constraint should be introduced in
2.107 - the for clause or the relevant @{element "fixes"} element.
2.108 + the @{keyword "for"} clause or the relevant @{element "fixes"} element.
2.109
2.110 \item @{element "assumes"}~@{text "a: \<phi>\<^sub>1 \<dots> \<phi>\<^sub>n"}
2.111 introduces local premises, similar to @{command "assume"} within a
2.112 @@ -538,11 +553,12 @@
2.113 include arbitrary declarations in any attribute specifications
2.114 included here, e.g.\ a local @{attribute simp} rule.
2.115
2.116 - The initial @{text import} specification of a locale expression
2.117 - maintains a dynamic relation to the locales being referenced
2.118 - (benefiting from any later fact declarations in the obvious manner).
2.119 + \end{description}
2.120
2.121 - \end{description}
2.122 + Both @{element "assumes"} and @{element "defines"} elements
2.123 + contribute to the locale specification. When defining an operation
2.124 + derived from the parameters, @{command "definition"}
2.125 + (\secref{sec:basic-spec}) is usually more appropriate.
2.126
2.127 Note that ``@{text "(\<IS> p\<^sub>1 \<dots> p\<^sub>n)"}'' patterns given
2.128 in the syntax of @{element "assumes"} and @{element "defines"} above
2.129 @@ -560,8 +576,8 @@
2.130 specification text.
2.131
2.132 In any case, the predicate arguments are those locale parameters
2.133 - that actually occur in the respective piece of text. Also note that
2.134 - these predicates operate at the meta-level in theory, but the locale
2.135 + that actually occur in the respective piece of text. Also these
2.136 + predicates operate at the meta-level in theory, but the locale
2.137 packages attempts to internalize statements according to the
2.138 object-logic setup (e.g.\ replacing @{text \<And>} by @{text \<forall>}, and
2.139 @{text "\<Longrightarrow>"} by @{text "\<longrightarrow>"} in HOL; see also
2.140 @@ -578,12 +594,13 @@
2.141
2.142 \item @{command "locale_deps"} visualizes all locales and their
2.143 relations as a Hasse diagram. This includes locales defined as type
2.144 - classes (\secref{sec:class}).
2.145 + classes (\secref{sec:class}). See also @{command
2.146 + "print_dependencies"} below.
2.147
2.148 \item @{method intro_locales} and @{method unfold_locales}
2.149 repeatedly expand all introduction rules of locale predicates of the
2.150 theory. While @{method intro_locales} only applies the @{text
2.151 - loc.intro} introduction rules and therefore does not decend to
2.152 + loc.intro} introduction rules and therefore does not descend to
2.153 assumptions, @{method unfold_locales} is more aggressive and applies
2.154 @{text loc_axioms.intro} as well. Both methods are aware of locale
2.155 specifications entailed by the context, both from target statements,
2.156 @@ -605,12 +622,12 @@
2.157 @{command_def "print_interps"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
2.158 \end{matharray}
2.159
2.160 - Locale expressions may be instantiated, and the instantiated facts
2.161 - added to the current context. This requires a proof of the
2.162 - instantiated specification and is called \emph{locale
2.163 - interpretation}. Interpretation is possible in locales (command
2.164 - @{command "sublocale"}), theories and local theories (command @{command
2.165 - "interpretation"}) and also within proof bodies (command @{command
2.166 + Locales may be instantiated, and the resulting instantiated
2.167 + declarations added to the current context. This requires proof (of
2.168 + the instantiated specification) and is called \emph{locale
2.169 + interpretation}. Interpretation is possible in locales (@{command
2.170 + "sublocale"}), global and local theories (@{command
2.171 + "interpretation"}) and also within proof bodies (@{command
2.172 "interpret"}).
2.173
2.174 @{rail "
2.175 @@ -632,40 +649,40 @@
2.176 \begin{description}
2.177
2.178 \item @{command "interpretation"}~@{text "expr \<WHERE> eqns"}
2.179 - interprets @{text expr} in a theory or local theory. The command
2.180 - generates proof obligations for the instantiated specifications
2.181 - (assumes and defines elements). Once these are discharged by the
2.182 - user, instantiated declarations (in particular, facts) are added to
2.183 - the theory in a post-processing phase.
2.184 + interprets @{text expr} in a global or local theory. The command
2.185 + generates proof obligations for the instantiated specifications.
2.186 + Once these are discharged by the user, instantiated declarations (in
2.187 + particular, facts) are added to the theory in a post-processing
2.188 + phase.
2.189
2.190 - The command is aware of interpretations that are already active, but
2.191 - does not simplify the goal automatically. In order to simplify the
2.192 - proof obligations use methods @{method intro_locales} or @{method
2.193 - unfold_locales}. Post-processing is not applied to declarations of
2.194 - interpretations that are already active. This avoids duplication of
2.195 - interpreted declarations, in particular. Note that, in the case of a
2.196 - locale with import, parts of the interpretation may already be
2.197 - active. The command will only process declarations for new parts.
2.198 + The command is aware of interpretations that are already active.
2.199 + Post-processing is achieved through a variant of roundup that takes
2.200 + the interpretations of the current global or local theory into
2.201 + account. In order to simplify the proof obligations according to
2.202 + existing interpretations use methods @{method intro_locales} or
2.203 + @{method unfold_locales}.
2.204
2.205 When adding declarations to locales, interpreted versions of these
2.206 declarations are added to the global theory for all interpretations
2.207 in the global theory as well. That is, interpretations in global
2.208 theories dynamically participate in any declarations added to
2.209 - locales. (Note that if a global theory inherits additional
2.210 - declarations for a locale through one parent and an interpretation
2.211 - of that locale through another parent, the additional declarations
2.212 - will not be interpreted.) In contrast, the lifetime of an
2.213 - interpretation in a local theory is limited to the current context
2.214 - block. At the closing @{command end} of the block the
2.215 - interpretation and its declarations disappear. This enables local
2.216 - interpretations, which are useful for auxilliary contructions,
2.217 - without polluting the class or locale with interpreted declarations.
2.218 + locales.
2.219 +
2.220 + In contrast, the lifetime of an interpretation in a local theory is
2.221 + limited to the current context block. At the closing @{command end}
2.222 + of the block the interpretation and its declarations disappear.
2.223 + This enables establishing facts based on interpretations without
2.224 + creating permanent links to the interpreted locale instances, as
2.225 + would be the case with @{command sublocale}.
2.226 + While @{command "interpretation"}~@{text "(\<IN> c)
2.227 + \<dots>"} is technically possible, it is not useful since its result is
2.228 + discarded immediately.
2.229
2.230 Free variables in the interpreted expression are allowed. They are
2.231 turned into schematic variables in the generated declarations. In
2.232 order to use a free variable whose name is already bound in the
2.233 context --- for example, because a constant of that name exists ---
2.234 - it may be added to the @{keyword "for"} clause.
2.235 + add it to the @{keyword "for"} clause.
2.236
2.237 The equations @{text eqns} yield \emph{rewrite morphisms}, which are
2.238 unfolded during post-processing and are useful for interpreting
2.239 @@ -687,16 +704,14 @@
2.240 the proof obligation has been discharged, the locale hierarchy is
2.241 changed as if @{text name} imported @{text expr} (hence the name
2.242 @{command "sublocale"}). When the context of @{text name} is
2.243 - subsequently entered, traversing the locale hierachy will involve
2.244 + subsequently entered, traversing the locale hierarchy will involve
2.245 the locale instances of @{text expr}, and their declarations will be
2.246 added to the context. This makes @{command "sublocale"}
2.247 dynamic: extensions of a locale that is instantiated in @{text expr}
2.248 may take place after the @{command "sublocale"} declaration and
2.249 still become available in the context. Circular @{command
2.250 "sublocale"} declarations are allowed as long as they do not lead to
2.251 - infinite chains. A detailed description of the \emph{roundup}
2.252 - algorithm that administers traversing locale hierarchies is available
2.253 - \cite{Ballarin2013}.
2.254 + infinite chains.
2.255
2.256 If interpretations of @{text name} exist in the current global
2.257 theory, the command adds interpretations for @{text expr} as well,
2.258 @@ -706,20 +721,22 @@
2.259 The equations @{text eqns} amend the morphism through
2.260 which @{text expr} is interpreted. This enables mapping definitions
2.261 from the interpreted locales to entities of @{text name} and can
2.262 - help break infinite chains induced by circular sublocale declarations.
2.263 + help break infinite chains induced by circular @{command
2.264 + "sublocale"} declarations.
2.265
2.266 In a named context block the @{command sublocale} command may also
2.267 be used, but the locale argument must be omitted. The command then
2.268 refers to the locale (or class) target of the context block.
2.269
2.270 \item @{command "print_dependencies"}~@{text "expr"} is useful for
2.271 - understanding the effect of an interpretation of @{text "expr"}. It
2.272 - lists all locale instances for which interpretations would be added
2.273 - to the current context. Variant @{command
2.274 - "print_dependencies"}@{text "!"} does not generalize parameters and
2.275 - assumes an empty context --- that is, it prints all locale instances
2.276 - that would be considered for interpretation. The latter is useful
2.277 - for understanding the dependencies of a locale expression.
2.278 + understanding the effect of an interpretation of @{text "expr"} in
2.279 + the current context. It lists all locale instances for which
2.280 + interpretations would be added to the current context. Variant
2.281 + @{command "print_dependencies"}@{text "!"} does not generalize
2.282 + parameters and assumes an empty context --- that is, it prints all
2.283 + locale instances that would be considered for interpretation. The
2.284 + latter is useful for understanding the dependencies of a locale
2.285 + expression.
2.286
2.287 \item @{command "print_interps"}~@{text "locale"} lists all
2.288 interpretations of @{text "locale"} in the current theory or proof
2.289 @@ -730,6 +747,13 @@
2.290 \end{description}
2.291
2.292 \begin{warn}
2.293 + If a global theory inherits declarations (body elements) for a
2.294 + locale from one parent and an interpretation of that locale from
2.295 + another parent, the interpretation will not be applied to the
2.296 + declarations.
2.297 + \end{warn}
2.298 +
2.299 + \begin{warn}
2.300 Since attributes are applied to interpreted theorems,
2.301 interpretation may modify the context of common proof tools, e.g.\
2.302 the Simplifier or Classical Reasoner. As the behavior of such