--- a/NEWS Tue Apr 23 17:46:12 2013 +0200
+++ b/NEWS Tue Apr 23 19:31:24 2013 +0200
@@ -31,6 +31,11 @@
*** Pure ***
+* Target-sensitive commands 'interpretation' and 'sublocale'.
+Particulary, 'interpretation' now allows for non-persistent
+interpretation within "context ... begin ... end" blocks.
+See "isar-ref" manual for details.
+
* Improved locales diagnostic command 'print_dependencies'.
* Discontinued obsolete 'axioms' command, which has been marked as
--- a/src/Doc/IsarRef/Spec.thy Tue Apr 23 17:46:12 2013 +0200
+++ b/src/Doc/IsarRef/Spec.thy Tue Apr 23 19:31:24 2013 +0200
@@ -598,9 +598,10 @@
text {*
\begin{matharray}{rcl}
- @{command_def "interpretation"} & : & @{text "theory \<rightarrow> proof(prove)"} \\
+ @{command_def "interpretation"} & : & @{text "local_theory \<rightarrow> proof(prove)"} \\
@{command_def "interpret"} & : & @{text "proof(state) | proof(chain) \<rightarrow> proof(prove)"} \\
@{command_def "sublocale"} & : & @{text "theory \<rightarrow> proof(prove)"} \\
+ @{command_def "sublocale"} & : & @{text "local_theory \<rightarrow> proof(prove)"} \\
@{command_def "print_dependencies"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
@{command_def "print_interps"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
\end{matharray}
@@ -609,18 +610,20 @@
added to the current context. This requires a proof of the
instantiated specification and is called \emph{locale
interpretation}. Interpretation is possible in locales (command
- @{command "sublocale"}), theories (command @{command
+ @{command "sublocale"}), (local) theories (command @{command
"interpretation"}) and also within proof bodies (command @{command
"interpret"}).
@{rail "
- @@{command interpretation} @{syntax locale_expr} equations?
+ @@{command interpretation} @{syntax target}? @{syntax locale_expr} equations?
;
@@{command interpret} @{syntax locale_expr} equations?
;
@@{command sublocale} @{syntax nameref} ('<' | '\<subseteq>') @{syntax locale_expr} \\
equations?
;
+ @@{command sublocale} @{syntax target}? @{syntax locale_expr} equations?
+ ;
@@{command print_dependencies} '!'? @{syntax locale_expr}
;
@@{command print_interps} @{syntax nameref}
@@ -632,10 +635,10 @@
\begin{description}
\item @{command "interpretation"}~@{text "expr \<WHERE> eqns"}
- interprets @{text expr} in the theory. The command generates proof
+ interprets @{text expr} in a local theory. The command generates proof
obligations for the instantiated specifications (assumes and defines
elements). Once these are discharged by the user, instantiated
- facts are added to the theory in a post-processing phase.
+ facts are added to the local theory in a post-processing phase.
Free variables in the interpreted expression are allowed. They are
turned into schematic variables in the generated declarations. In
@@ -649,7 +652,7 @@
definitions. The equations must be proved.
The command is aware of interpretations already active in the
- theory, but does not simplify the goal automatically. In order to
+ local theory, but does not simplify the goal automatically. In order to
simplify the proof obligations use methods @{method intro_locales}
or @{method unfold_locales}. Post-processing is not applied to
facts of interpretations that are already active. This avoids
@@ -658,17 +661,24 @@
already be active. The command will only process facts for new
parts.
- Adding facts to locales has the effect of adding interpreted facts
- to the theory for all interpretations as well. That is,
- interpretations dynamically participate in any facts added to
- locales. Note that if a theory inherits additional facts for a
+ If the local theory is a global theory target, the facts persist.
+ Even more, adding facts to locales has the effect of adding interpreted facts
+ to the global background theory for all interpretations as well. That is,
+ interpretations into global theories dynamically participate in any facts added to
+ locales.
+
+ If the local theory is not a global theory, the facts disappear
+ after the @{command end} confining the current context block
+ opened by @{command context}, similar to @{command interpret}.
+
+ Note that if a local theory inherits additional facts for a
locale through one parent and an interpretation of that locale
through another parent, the additional facts will not be
interpreted.
\item @{command "interpret"}~@{text "expr \<WHERE> eqns"} interprets
@{text expr} in the proof context and is otherwise similar to
- interpretation in theories. Note that rewrite rules given to
+ interpretation in local theories. Note that rewrite rules given to
@{command "interpret"} after the @{keyword "where"} keyword should be
explicitly universally quantified.
@@ -701,6 +711,12 @@
from the interpreted locales to entities of @{text name}. This
feature is experimental.
+ \item @{command "sublocale"}~@{text "expr \<WHERE> eqns"} is a syntactic
+ variant of @{command "sublocale"} which must be used in
+ the local theory context of a locale @{text name} only. Then it
+ is equivalent to @{command "sublocale"}~@{text "name \<subseteq> expr \<WHERE>
+ eqns"}.
+
\item @{command "print_dependencies"}~@{text "expr"} is useful for
understanding the effect of an interpretation of @{text "expr"}. It
lists all locale instances for which interpretations would be added
@@ -728,7 +744,7 @@
\end{warn}
\begin{warn}
- An interpretation in a theory or proof context may subsume previous
+ An interpretation in a local theory or proof context may subsume previous
interpretations. This happens if the same specification fragment
is interpreted twice and the instantiation of the second
interpretation is more general than the interpretation of the
@@ -797,7 +813,7 @@
class membership proofs.
\item @{command "instantiation"}~@{text "t :: (s\<^sub>1, \<dots>, s\<^sub>n)s
- \<BEGIN>"} opens a theory target (cf.\ \secref{sec:target}) which
+ \<BEGIN>"} opens a target (cf.\ \secref{sec:target}) which
allows to specify class operations @{text "f\<^sub>1, \<dots>, f\<^sub>n"} corresponding
to sort @{text s} at the particular type instance @{text "(\<alpha>\<^sub>1 :: s\<^sub>1,
\<dots>, \<alpha>\<^sub>n :: s\<^sub>n) t"}. A plain @{command "instance"} command in the