--- a/src/Doc/IsarRef/Spec.thy Tue Sep 03 22:10:54 2013 +0200
+++ b/src/Doc/IsarRef/Spec.thy Tue Sep 03 22:30:52 2013 +0200
@@ -598,10 +598,9 @@
text {*
\begin{matharray}{rcl}
- @{command_def "interpretation"} & : & @{text "local_theory \<rightarrow> proof(prove)"} \\
+ @{command_def "interpretation"} & : & @{text "theory | 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 "sublocale"} & : & @{text "theory | 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}
@@ -610,20 +609,18 @@
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"}), (local) theories (command @{command
+ @{command "sublocale"}), theories and local theories (command @{command
"interpretation"}) and also within proof bodies (command @{command
"interpret"}).
@{rail "
- @@{command interpretation} @{syntax target}? @{syntax locale_expr} equations?
+ @@{command interpretation} @{syntax locale_expr} equations?
;
@@{command interpret} @{syntax locale_expr} equations?
;
- @@{command sublocale} @{syntax nameref} ('<' | '\<subseteq>') @{syntax locale_expr} \\
+ @@{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}
@@ -635,10 +632,34 @@
\begin{description}
\item @{command "interpretation"}~@{text "expr \<WHERE> eqns"}
- 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 local theory in a post-processing phase.
+ interprets @{text expr} in a theory or local theory. The command
+ generates proof obligations for the instantiated specifications
+ (assumes and defines elements). Once these are discharged by the
+ user, instantiated declarations (in particular, facts) are added to
+ the theory in a post-processing phase.
+
+ The command is aware of interpretations that are already active, 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 declarations of
+ interpretations that are already active. This avoids duplication of
+ interpreted declarations, in particular. Note that, in the case of a
+ locale with import, parts of the interpretation may already be
+ active. The command will only process declarations for new parts.
+
+ When adding declarations to locales, interpreted versions of these
+ declarations are added to the global theory for all interpretations
+ in the global theory as well. That is, interpretations in global
+ theories dynamically participate in any declarations added to
+ locales. (Note that if a global theory inherits additional
+ declarations for a locale through one parent and an interpretation
+ of that locale through another parent, the additional declarations
+ will not be interpreted.) In contrast, the lifetime of an
+ interpretation in a local theory is limited to the current context
+ block. At the closing @{command end} of the block the
+ interpretation and its declarations disappear. This enables local
+ interpretations, which are useful for auxilliary contructions,
+ without polluting the class or locale with interpreted declarations.
Free variables in the interpreted expression are allowed. They are
turned into schematic variables in the generated declarations. In
@@ -646,40 +667,15 @@
context --- for example, because a constant of that name exists ---
it may be added to the @{keyword "for"} clause.
- Additional equations, which are unfolded during
- post-processing, may be given after the keyword @{keyword "where"}.
- This is useful for interpreting concepts introduced through
- definitions. The equations must be proved.
-
- The command is aware of interpretations already active in the
- 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
- duplication of interpreted facts, in particular. Note that, in the
- case of a locale with import, parts of the interpretation may
- already be active. The command will only process facts for new
- parts.
-
- 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.
+ The equations @{text eqns} yield \emph{rewrite morphisms}, which are
+ unfolded during post-processing and are useful for interpreting
+ concepts introduced through definitions. The equations must be
+ proved.
\item @{command "interpret"}~@{text "expr \<WHERE> eqns"} interprets
@{text expr} in the proof context and is otherwise similar to
- interpretation in local theories. Note that rewrite rules given to
- @{command "interpret"} after the @{keyword "where"} keyword should be
+ interpretation in local theories. Note that for @{command
+ "interpret"} the @{text eqns} should be
explicitly universally quantified.
\item @{command "sublocale"}~@{text "name \<subseteq> expr \<WHERE>
@@ -688,34 +684,33 @@
the specification of @{text name} implies the specification of
@{text expr} is required. As in the localized version of the
theorem command, the proof is in the context of @{text name}. After
- the proof obligation has been discharged, the facts of @{text expr}
- become part of locale @{text name} as \emph{derived} context
- elements and are available when the context @{text name} is
- subsequently entered. Note that, like import, this is dynamic:
- facts added to a locale part of @{text expr} after interpretation
- become also available in @{text name}.
-
- Only specification fragments of @{text expr} that are not already
- part of @{text name} (be it imported, derived or a derived fragment
- of the import) are considered in this process. This enables
- circular interpretations provided that no infinite chains are
- generated in the locale hierarchy.
+ the proof obligation has been discharged, the locale hierarchy is
+ changed as if @{text name} imported @{text expr} (hence the name
+ @{command "sublocale"}). When the context of @{text name} is
+ subsequently entered, traversing the locale hierachy will involve
+ the locale instances of @{text expr}, and their declarations will be
+ added to the context. This makes @{command "sublocale"}
+ dynamic: extensions of a locale that is instantiated in @{text expr}
+ may take place after the @{command "sublocale"} declaration and
+ still become available in the context. Circular @{command
+ "sublocale"} declarations are allowed as long as they do not lead to
+ infinite chains. A detailed description of the \emph{roundup}
+ algorithm that administers traversing locale hierarchies is available
+ \cite{Ballarin2013}.
- If interpretations of @{text name} exist in the current theory, the
- command adds interpretations for @{text expr} as well, with the same
- qualifier, although only for fragments of @{text expr} that are not
- interpreted in the theory already.
+ If interpretations of @{text name} exist in the current global
+ theory, the command adds interpretations for @{text expr} as well,
+ with the same qualifier, although only for fragments of @{text expr}
+ that are not interpreted in the theory already.
- Equations given after @{keyword "where"} amend the morphism through
- which @{text expr} is interpreted. This enables to map definitions
- from the interpreted locales to entities of @{text name}. This
- feature is experimental.
+ The equations @{text eqns} amend the morphism through
+ which @{text expr} is interpreted. This enables mapping definitions
+ from the interpreted locales to entities of @{text name} and can
+ help break infinite chains induced by circular sublocale declarations.
- \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"}.
+ In a named context block the @{command sublocale} command may also
+ be used, but the locale argument must be omitted. The command then
+ refers to the locale (or class) target of the context block.
\item @{command "print_dependencies"}~@{text "expr"} is useful for
understanding the effect of an interpretation of @{text "expr"}. It
--- a/src/Doc/manual.bib Tue Sep 03 22:10:54 2013 +0200
+++ b/src/Doc/manual.bib Tue Sep 03 22:30:52 2013 +0200
@@ -161,6 +161,15 @@
note = {\url{http://isabelle.in.tum.de/doc/locales.pdf}}
}
+@article{Ballarin2013,
+ author = {Ballarin, Clemens},
+ journal = JAR,
+ note = {Online version; to appear in print.},
+ publisher = Springer,
+ title = {Locales: A Module System for Mathematical Theories},
+ url = {http://dx.doi.org/10.1007/s10817-013-9284-7},
+ year = {2013}}
+
@InCollection{Barendregt-Geuvers:2001,
author = {H. Barendregt and H. Geuvers},
title = {Proof Assistants using Dependent Type Systems},
--- a/src/FOL/ex/Locale_Test/Locale_Test1.thy Tue Sep 03 22:10:54 2013 +0200
+++ b/src/FOL/ex/Locale_Test/Locale_Test1.thy Tue Sep 03 22:30:52 2013 +0200
@@ -484,7 +484,9 @@
by unfold_locales
-subsection {* Equations *}
+subsection {* Interpretation *}
+
+subsection {* Rewrite morphism *}
locale logic_o =
fixes land (infixl "&&" 55)
@@ -516,7 +518,7 @@
x.lor_triv
-subsection {* Inheritance of mixins *}
+subsection {* Inheritance of rewrite morphisms *}
locale reflexive =
fixes le :: "'a => 'a => o" (infix "\<sqsubseteq>" 50)
@@ -549,7 +551,7 @@
by (simp add: reflexive.less_def[OF reflexive] gless_def)
qed
-text {* Mixin propagated along the locale hierarchy *}
+text {* Rewrite morphism propagated along the locale hierarchy *}
locale mixin2 = mixin
begin
@@ -559,11 +561,11 @@
interpretation le: mixin2 gle
by unfold_locales
-thm le.less_thm2 (* mixin applied *)
+thm le.less_thm2 (* rewrite morphism applied *)
lemma "gless(x, y) <-> gle(x, y) & x ~= y"
by (rule le.less_thm2)
-text {* Mixin does not leak to a side branch. *}
+text {* Rewrite morphism does not leak to a side branch. *}
locale mixin3 = reflexive
begin
@@ -573,10 +575,10 @@
interpretation le: mixin3 gle
by unfold_locales
-thm le.less_thm3 (* mixin not applied *)
+thm le.less_thm3 (* rewrite morphism not applied *)
lemma "reflexive.less(gle, x, y) <-> gle(x, y) & x ~= y" by (rule le.less_thm3)
-text {* Mixin only available in original context *}
+text {* Rewrite morphism only available in original context *}
locale mixin4_base = reflexive
@@ -604,11 +606,11 @@
interpretation le4: mixin4_combined gle' gle
by unfold_locales (rule grefl')
-thm le4.less_thm4' (* mixin not applied *)
+thm le4.less_thm4' (* rewrite morphism not applied *)
lemma "reflexive.less(gle, x, y) <-> gle(x, y) & x ~= y"
by (rule le4.less_thm4')
-text {* Inherited mixin applied to new theorem *}
+text {* Inherited rewrite morphism applied to new theorem *}
locale mixin5_base = reflexive
@@ -628,11 +630,11 @@
lemmas (in mixin5_inherited) less_thm5 = less_def
-thm le5.less_thm5 (* mixin applied *)
+thm le5.less_thm5 (* rewrite morphism applied *)
lemma "gless(x, y) <-> gle(x, y) & x ~= y"
by (rule le5.less_thm5)
-text {* Mixin pushed down to existing inherited locale *}
+text {* Rewrite morphism pushed down to existing inherited locale *}
locale mixin6_base = reflexive
@@ -657,7 +659,7 @@
lemma "gless(x, y) <-> gle(x, y) & x ~= y"
by (rule le6.less_thm6)
-text {* Existing mixin inherited through sublocale relation *}
+text {* Existing rewrite morphism inherited through sublocale relation *}
locale mixin7_base = reflexive
@@ -677,7 +679,7 @@
lemmas (in mixin7_inherited) less_thm7 = less_def
-thm le7.less_thm7 (* before, mixin not applied *)
+thm le7.less_thm7 (* before, rewrite morphism not applied *)
lemma "reflexive.less(gle, x, y) <-> gle(x, y) & x ~= y"
by (rule le7.less_thm7)
@@ -696,7 +698,7 @@
locale mixin_thy_merge = le: reflexive le + le': reflexive le' for le le'
-subsection {* Mixins in sublocale *}
+subsection {* Rewrite morphisms in sublocale *}
text {* Simulate a specification of left groups where unit and inverse are defined
rather than specified. This is possible, but not in FOL, due to the lack of a
@@ -745,7 +747,7 @@
lemma "dgrp.one(prod) = one" by (rule one_equation)
lemma "dgrp.inv(prod, x) = inv(x)" by (rule inv_equation)
-text {* Mixins applied *}
+text {* Rewrite morphisms applied *}
lemma "one = glob_one(prod)" by (rule one_def)
lemma "inv(x) = glob_inv(prod, x)" by (rule inv_def)
@@ -757,7 +759,7 @@
lemma "0 = glob_one (op +)" by (rule int.def.one_def)
lemma "- x = glob_inv(op +, x)" by (rule int.def.inv_def)
-text {* Roundup applies mixins at declaration level in DFS tree *}
+text {* Roundup applies rewrite morphisms at declaration level in DFS tree *}
locale roundup = fixes x assumes true: "x <-> True"
@@ -766,6 +768,23 @@
lemma (in roundup) "True & True <-> True" by (rule sub.true)
+section {* Interpretation in named contexts *}
+
+locale container
+begin
+interpretation private!: roundup True by unfold_locales rule
+lemmas true_copy = private.true
+end
+
+context container begin
+ML {* (Context.>> (fn generic => let val context = Context.proof_of generic
+ val _ = Proof_Context.get_thms context "private.true" in generic end);
+ error "thm private.true was persisted")
+ handle ERROR "Unknown fact \"private.true\"" => ([]:thm list); *}
+thm true_copy
+end
+
+
section {* Interpretation in proofs *}
lemma True