documentation on last state of the art concerning interpretation
authorhaftmann
Sat, 19 Dec 2015 17:03:17 +0100
changeset 61859 76189756ff65
parent 61858 f6ded81f5690
child 61892 5c68d06f97b3
documentation on last state of the art concerning interpretation
CONTRIBUTORS
NEWS
src/Doc/Codegen/Further.thy
src/Doc/Isar_Ref/Spec.thy
--- a/CONTRIBUTORS	Sat Dec 19 11:05:04 2015 +0100
+++ b/CONTRIBUTORS	Sat Dec 19 17:03:17 2015 +0100
@@ -6,6 +6,10 @@
 Contributions to this Isabelle version
 --------------------------------------
 
+* Autumn 2015: Florian Haftmann, TUM
+  Rewrite definitions for global interpretations and
+  sublocale declarations.
+
 * Autumn 2015: Andreas Lochbihler
   Bourbaki-Witt fixpoint theorem for increasing functions on
   chain-complete partial orders.
--- a/NEWS	Sat Dec 19 11:05:04 2015 +0100
+++ b/NEWS	Sat Dec 19 17:03:17 2015 +0100
@@ -346,12 +346,15 @@
     notation right.derived ("\<odot>''")
   end
 
-* Command 'sublocale' accepts rewrite definitions after keyword
+* Command 'global_interpreation' issues interpretations into
+global theories, with optional rewrite definitions following keyword
 'defines'.
 
-* Command 'permanent_interpretation' is available in Pure, without
-need to load a separate theory.  Keyword 'defines' identifies
-rewrite definitions, keyword 'rewrites' identifies rewrite equations.
+* Command 'sublocale' accepts optional rewrite definitions after
+keyword 'defines'.
+
+* Command 'permanent_interpretation' has been discontinued.  Use
+'global_interpretation' or 'sublocale' instead.
 INCOMPATIBILITY.
 
 * Command 'print_definitions' prints dependencies of definitional
--- a/src/Doc/Codegen/Further.thy	Sat Dec 19 11:05:04 2015 +0100
+++ b/src/Doc/Codegen/Further.thy	Sat Dec 19 17:03:17 2015 +0100
@@ -139,7 +139,8 @@
 
 text \<open>
   A technical issue comes to surface when generating code from
-  specifications stemming from locale interpretation.
+  specifications stemming from locale interpretation into global
+  theories.
 
   Let us assume a locale specifying a power operation on arbitrary
   types:
@@ -177,7 +178,7 @@
 
 text \<open>
   After an interpretation of this locale (say, @{command_def
-  interpretation} @{text "fun_power:"} @{term [source] "power (\<lambda>n (f
+  global_interpretation} @{text "fun_power:"} @{term [source] "power (\<lambda>n (f
   :: 'a \<Rightarrow> 'a). f ^^ n)"}), one could naively expect to have a constant @{text
   "fun_power.powers :: nat list \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a"} for which code
   can be generated.  But this not the case: internally, the term
@@ -185,12 +186,11 @@
   term @{term [source] "power.powers (\<lambda>n (f :: 'a \<Rightarrow> 'a). f ^^ n)"}
   (see @{cite "isabelle-locale"} for the details behind).
 
-  Fortunately, a succint solution is available:
-  @{command permanent_interpretation} with a dedicated
+  Fortunately, a succint solution is available: a dedicated
   rewrite definition:
 \<close>
 
-permanent_interpretation %quote fun_power: power "(\<lambda>n (f :: 'a \<Rightarrow> 'a). f ^^ n)"
+global_interpretation %quote fun_power: power "(\<lambda>n (f :: 'a \<Rightarrow> 'a). f ^^ n)"
   defines funpows = fun_power.powers
   by unfold_locales
     (simp_all add: fun_eq_iff funpow_mult mult.commute)
--- a/src/Doc/Isar_Ref/Spec.thy	Sat Dec 19 11:05:04 2015 +0100
+++ b/src/Doc/Isar_Ref/Spec.thy	Sat Dec 19 17:03:17 2015 +0100
@@ -607,9 +607,8 @@
   \begin{matharray}{rcl}
     @{command "interpretation"} & : & \<open>local_theory \<rightarrow> proof(prove)\<close> \\
     @{command_def "interpret"} & : & \<open>proof(state) | proof(chain) \<rightarrow> proof(prove)\<close> \\
-    @{command_def "interpretation"} & : & \<open>theory \<rightarrow> proof(prove)\<close> \\
+    @{command_def "global_interpretation"} & : & \<open>theory | local_theory \<rightarrow> proof(prove)\<close> \\
     @{command_def "sublocale"} & : & \<open>theory | local_theory \<rightarrow> proof(prove)\<close> \\
-    @{command_def "permanent_interpretation"} & : & \<open>local_theory \<rightarrow> proof(prove)\<close> \\
     @{command_def "print_dependencies"}\<open>\<^sup>*\<close> & : & \<open>context \<rightarrow>\<close> \\
     @{command_def "print_interps"}\<open>\<^sup>*\<close> & :  & \<open>context \<rightarrow>\<close> \\
   \end{matharray}
@@ -618,24 +617,20 @@
   added to the current context. This requires proof (of the instantiated
   specification) and is called \<^emph>\<open>locale interpretation\<close>. Interpretation is
   possible within arbitrary local theories (\<^theory_text>\<open>interpretation\<close>), within proof
-  bodies (\<^theory_text>\<open>interpret\<close>), into global theories (another variant of
-  \<^theory_text>\<open>interpretation\<close>) and into locales (\<^theory_text>\<open>sublocale\<close>). As a generalization,
-  interpretation into arbitrary local theories is possible, although this is
-  only implemented by certain targets (\<^theory_text>\<open>permanent_interpretation\<close>).
+  bodies (\<^theory_text>\<open>interpret\<close>), into global theories (\<^theory_text>\<open>global_interpretation\<close>) and
+  into locales (\<^theory_text>\<open>sublocale\<close>).
 
   @{rail \<open>
     @@{command interpretation} @{syntax locale_expr} equations?
     ;
     @@{command interpret} @{syntax locale_expr} equations?
     ;
-    @@{command interpretation} @{syntax locale_expr} equations?
+    @@{command global_interpretation} @{syntax locale_expr} \<newline>
+      definitions? equations?
     ;
     @@{command sublocale} (@{syntax nameref} ('<' | '\<subseteq>'))? @{syntax locale_expr} \<newline>
       definitions? equations?
     ;
-    @@{command permanent_interpretation} @{syntax locale_expr} \<newline>
-      definitions? equations?
-    ;
     @@{command print_dependencies} '!'? @{syntax locale_expr}
     ;
     @@{command print_interps} @{syntax nameref}
@@ -666,13 +661,13 @@
 
   Given definitions \<open>defs\<close> produce corresponding definitions in the local
   theory's underlying target \<^emph>\<open>and\<close> amend the morphism with the equations
-  stemming from the symmetric of the definitions. Hence they need not be
+  stemming from the symmetric of those definitions. Hence these need not be
   proved explicitly the user. Such rewrite definitions are a even more useful
   device for interpreting concepts introduced through definitions, but they
   are only supported for interpretation commands operating in a local theory
   whose implementing target actually supports this.  Note that despite
   the suggestive \<^theory_text>\<open>and\<close> connective, \<open>defs\<close>
-  are parsed sequentially without mutual recursion.
+  are processed sequentially without mutual recursion.
 
   \<^descr> \<^theory_text>\<open>interpretation expr rewrites eqns\<close> interprets \<open>expr\<close> into a local theory
   such that its lifetime is limited to the current context block (e.g. a
@@ -682,17 +677,21 @@
   interpreted locale instances, as would be the case with @{command
   sublocale}.
 
+  When used on the level of a global theory, there is no end of a current
+  context block, hence \<^theory_text>\<open>interpretation\<close> behaves identically to
+  \<^theory_text>\<open>global_interpretation\<close> then.
+
   \<^descr> \<^theory_text>\<open>interpret expr rewrites eqns\<close> interprets \<open>expr\<close> into a proof context:
   the interpretation and its declarations disappear when closing the current
   proof block. Note that for \<^theory_text>\<open>interpret\<close> the \<open>eqns\<close> should be explicitly
   universally quantified.
 
-  \<^descr> \<^theory_text>\<open>interpretation expr rewrites eqns\<close> interprets \<open>expr\<close> into a global
-  theory.
+  \<^descr> \<^theory_text>\<open>global_interpretation defines "defs" rewrites eqns\<close> interprets \<open>expr\<close>
+  into a global theory.
 
   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
+  global theory as well. That is, interpretations into global theories
   dynamically participate in any declarations added to locales.
 
   Free variables in the interpreted expression are allowed. They are turned
@@ -724,20 +723,6 @@
   locale argument must be omitted. The command then refers to the locale (or
   class) target of the context block.
 
-  \<^descr> \<^theory_text>\<open>permanent_interpretation defines "defs" rewrites eqns\<close> interprets \<open>expr\<close>
-  into the target of the current local theory. When adding declarations to
-  locales, interpreted versions of these declarations are added to any target
-  for all interpretations in that target as well. That is, permanent
-  interpretations dynamically participate in any declarations added to
-  locales.
-  
-  The local theory's underlying target must explicitly support permanent
-  interpretations. Prominent examples are global theories (where
-  \<^theory_text>\<open>permanent_interpretation\<close> technically corresponds to \<^theory_text>\<open>interpretation\<close>)
-  and locales (where \<^theory_text>\<open>permanent_interpretation\<close> technically corresponds to
-  \<^theory_text>\<open>sublocale\<close>). Unnamed contexts (see \secref{sec:target}) are not
-  admissible.
-
   \<^descr> \<^theory_text>\<open>print_dependencies expr\<close> is useful for understanding the effect of an
   interpretation of \<open>expr\<close> in the current context. It lists all locale
   instances for which interpretations would be added to the current context.
@@ -751,7 +736,6 @@
   \<^theory_text>\<open>interpretation\<close> or \<^theory_text>\<open>interpret\<close> and one or several \<^theory_text>\<open>sublocale\<close>
   declarations.
 
-
   \begin{warn}
     If a global theory inherits declarations (body elements) for a locale from
     one parent and an interpretation of that locale from another parent, the