# HG changeset patch
# User haftmann
# Date 1450730054 -3600
# Node ID 5c68d06f97b37ef71bdaa0c020a9ff55a8cdec58
# Parent  76189756ff654dacf441596c2ccd6eb71cddf06b# Parent  42d902e074e831fe9573b56ddcb9b009653a6dc6
merged

diff -r 42d902e074e8 -r 5c68d06f97b3 CONTRIBUTORS
--- a/CONTRIBUTORS	Mon Dec 21 17:20:57 2015 +0100
+++ b/CONTRIBUTORS	Mon Dec 21 21:34:14 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.
diff -r 42d902e074e8 -r 5c68d06f97b3 NEWS
--- a/NEWS	Mon Dec 21 17:20:57 2015 +0100
+++ b/NEWS	Mon Dec 21 21:34:14 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
diff -r 42d902e074e8 -r 5c68d06f97b3 src/Doc/Codegen/Further.thy
--- a/src/Doc/Codegen/Further.thy	Mon Dec 21 17:20:57 2015 +0100
+++ b/src/Doc/Codegen/Further.thy	Mon Dec 21 21:34:14 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)
diff -r 42d902e074e8 -r 5c68d06f97b3 src/Doc/Isar_Ref/Spec.thy
--- a/src/Doc/Isar_Ref/Spec.thy	Mon Dec 21 17:20:57 2015 +0100
+++ b/src/Doc/Isar_Ref/Spec.thy	Mon Dec 21 21:34:14 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
diff -r 42d902e074e8 -r 5c68d06f97b3 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Mon Dec 21 17:20:57 2015 +0100
+++ b/src/HOL/Finite_Set.thy	Mon Dec 21 21:34:14 2015 +0100
@@ -1209,7 +1209,7 @@
   But now that we have @{const fold} things are easy:
 \<close>
 
-permanent_interpretation card: folding "\<lambda>_. Suc" 0
+global_interpretation card: folding "\<lambda>_. Suc" 0
   defines card = "folding.F (\<lambda>_. Suc) 0"
   by standard rule
 
diff -r 42d902e074e8 -r 5c68d06f97b3 src/HOL/IMP/Abs_Int1_const.thy
--- a/src/HOL/IMP/Abs_Int1_const.thy	Mon Dec 21 17:20:57 2015 +0100
+++ b/src/HOL/IMP/Abs_Int1_const.thy	Mon Dec 21 21:34:14 2015 +0100
@@ -53,7 +53,7 @@
 end
 
 
-permanent_interpretation Val_semilattice
+global_interpretation Val_semilattice
 where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const
 proof (standard, goal_cases)
   case (1 a b) thus ?case
@@ -66,7 +66,7 @@
   case 4 thus ?case by(auto simp: plus_const_cases split: const.split)
 qed
 
-permanent_interpretation Abs_Int
+global_interpretation Abs_Int
 where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const
 defines AI_const = AI and step_const = step' and aval'_const = aval'
 ..
@@ -120,7 +120,7 @@
 
 text{* Monotonicity: *}
 
-permanent_interpretation Abs_Int_mono
+global_interpretation Abs_Int_mono
 where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const
 proof (standard, goal_cases)
   case 1 thus ?case by(auto simp: plus_const_cases split: const.split)
@@ -131,7 +131,7 @@
 definition m_const :: "const \<Rightarrow> nat" where
 "m_const x = (if x = Any then 0 else 1)"
 
-permanent_interpretation Abs_Int_measure
+global_interpretation Abs_Int_measure
 where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const
 and m = m_const and h = "1"
 proof (standard, goal_cases)
diff -r 42d902e074e8 -r 5c68d06f97b3 src/HOL/IMP/Abs_Int1_parity.thy
--- a/src/HOL/IMP/Abs_Int1_parity.thy	Mon Dec 21 17:20:57 2015 +0100
+++ b/src/HOL/IMP/Abs_Int1_parity.thy	Mon Dec 21 21:34:14 2015 +0100
@@ -102,7 +102,7 @@
 text{* First we instantiate the abstract value interface and prove that the
 functions on type @{typ parity} have all the necessary properties: *}
 
-permanent_interpretation Val_semilattice
+global_interpretation Val_semilattice
 where \<gamma> = \<gamma>_parity and num' = num_parity and plus' = plus_parity
 proof (standard, goal_cases) txt{* subgoals are the locale axioms *}
   case 1 thus ?case by(auto simp: less_eq_parity_def)
@@ -124,7 +124,7 @@
 proofs (they happened in the instatiation above) but delivers the
 instantiated abstract interpreter which we call @{text AI_parity}: *}
 
-permanent_interpretation Abs_Int
+global_interpretation Abs_Int
 where \<gamma> = \<gamma>_parity and num' = num_parity and plus' = plus_parity
 defines aval_parity = aval' and step_parity = step' and AI_parity = AI
 ..
@@ -155,7 +155,7 @@
 
 subsubsection "Termination"
 
-permanent_interpretation Abs_Int_mono
+global_interpretation Abs_Int_mono
 where \<gamma> = \<gamma>_parity and num' = num_parity and plus' = plus_parity
 proof (standard, goal_cases)
   case (1 _ a1 _ a2) thus ?case
@@ -166,7 +166,7 @@
 definition m_parity :: "parity \<Rightarrow> nat" where
 "m_parity x = (if x = Either then 0 else 1)"
 
-permanent_interpretation Abs_Int_measure
+global_interpretation Abs_Int_measure
 where \<gamma> = \<gamma>_parity and num' = num_parity and plus' = plus_parity
 and m = m_parity and h = "1"
 proof (standard, goal_cases)
diff -r 42d902e074e8 -r 5c68d06f97b3 src/HOL/IMP/Abs_Int2_ivl.thy
--- a/src/HOL/IMP/Abs_Int2_ivl.thy	Mon Dec 21 17:20:57 2015 +0100
+++ b/src/HOL/IMP/Abs_Int2_ivl.thy	Mon Dec 21 21:34:14 2015 +0100
@@ -302,7 +302,7 @@
   "\<lbrakk>Fin y1 \<le> x1; Fin y2 \<le> x2\<rbrakk> \<Longrightarrow> Fin(y1 + y2::'a::ordered_ab_group_add) \<le> x1 + x2"
 by(drule (1) add_mono) simp
 
-permanent_interpretation Val_semilattice
+global_interpretation Val_semilattice
 where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
 proof (standard, goal_cases)
   case 1 thus ?case by transfer (simp add: le_iff_subset)
@@ -318,7 +318,7 @@
 qed
 
 
-permanent_interpretation Val_lattice_gamma
+global_interpretation Val_lattice_gamma
 where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
 defines aval_ivl = aval'
 proof (standard, goal_cases)
@@ -327,7 +327,7 @@
   case 2 show ?case unfolding bot_ivl_def by transfer simp
 qed
 
-permanent_interpretation Val_inv
+global_interpretation Val_inv
 where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
 and test_num' = in_ivl
 and inv_plus' = inv_plus_ivl and inv_less' = inv_less_ivl
@@ -350,7 +350,7 @@
     done
 qed
 
-permanent_interpretation Abs_Int_inv
+global_interpretation Abs_Int_inv
 where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
 and test_num' = in_ivl
 and inv_plus' = inv_plus_ivl and inv_less' = inv_less_ivl
@@ -384,7 +384,7 @@
 apply(auto simp: below_rep_def le_iff_subset split: if_splits prod.split)
 by(auto simp: is_empty_rep_iff \<gamma>_rep_cases split: extended.splits)
 
-permanent_interpretation Abs_Int_inv_mono
+global_interpretation Abs_Int_inv_mono
 where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
 and test_num' = in_ivl
 and inv_plus' = inv_plus_ivl and inv_less' = inv_less_ivl
diff -r 42d902e074e8 -r 5c68d06f97b3 src/HOL/IMP/Abs_Int3.thy
--- a/src/HOL/IMP/Abs_Int3.thy	Mon Dec 21 17:20:57 2015 +0100
+++ b/src/HOL/IMP/Abs_Int3.thy	Mon Dec 21 21:34:14 2015 +0100
@@ -256,7 +256,7 @@
 
 end
 
-permanent_interpretation Abs_Int_wn
+global_interpretation Abs_Int_wn
 where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
 and test_num' = in_ivl
 and inv_plus' = inv_plus_ivl and inv_less' = inv_less_ivl
@@ -541,7 +541,7 @@
          split: prod.splits if_splits extended.split)
 
 
-permanent_interpretation Abs_Int_wn_measure
+global_interpretation Abs_Int_wn_measure
 where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = "op +"
 and test_num' = in_ivl
 and inv_plus' = inv_plus_ivl and inv_less' = inv_less_ivl
diff -r 42d902e074e8 -r 5c68d06f97b3 src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_const.thy
--- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_const.thy	Mon Dec 21 17:20:57 2015 +0100
+++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den0_const.thy	Mon Dec 21 21:34:14 2015 +0100
@@ -47,13 +47,13 @@
 
 end
 
-permanent_interpretation Rep rep_cval
+global_interpretation Rep rep_cval
 proof
   case goal1 thus ?case
     by(cases a, cases b, simp, simp, cases b, simp, simp)
 qed
 
-permanent_interpretation Val_abs rep_cval Const plus_cval
+global_interpretation Val_abs rep_cval Const plus_cval
 proof
   case goal1 show ?case by simp
 next
@@ -61,7 +61,7 @@
     by(cases a1, cases a2, simp, simp, cases a2, simp, simp)
 qed
 
-permanent_interpretation Abs_Int rep_cval Const plus_cval "(iter' 3)"
+global_interpretation Abs_Int rep_cval Const plus_cval "(iter' 3)"
 defines AI_const = AI
 and aval'_const = aval'
 proof qed (auto simp: iter'_pfp_above)
diff -r 42d902e074e8 -r 5c68d06f97b3 src/HOL/IMP/Abs_Int_Den/Abs_Int_den1_ivl.thy
--- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den1_ivl.thy	Mon Dec 21 17:20:57 2015 +0100
+++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den1_ivl.thy	Mon Dec 21 21:34:14 2015 +0100
@@ -166,13 +166,13 @@
          I (max_option False (l1 + Some 1) l2) h2)
    else (I (max_option False l1 l2) h1, I l2 (min_option True h1 h2)))"
 
-permanent_interpretation Rep rep_ivl
+global_interpretation Rep rep_ivl
 proof
   case goal1 thus ?case
     by(auto simp: rep_ivl_def le_ivl_def le_option_def split: ivl.split option.split if_splits)
 qed
 
-permanent_interpretation Val_abs rep_ivl num_ivl plus_ivl
+global_interpretation Val_abs rep_ivl num_ivl plus_ivl
 proof
   case goal1 thus ?case by(simp add: rep_ivl_def num_ivl_def)
 next
@@ -180,7 +180,7 @@
     by(auto simp add: rep_ivl_def plus_ivl_def split: ivl.split option.splits)
 qed
 
-permanent_interpretation Rep1 rep_ivl
+global_interpretation Rep1 rep_ivl
 proof
   case goal1 thus ?case
     by(auto simp add: rep_ivl_def meet_ivl_def empty_def min_option_def max_option_def split: ivl.split option.split)
@@ -188,7 +188,7 @@
   case goal2 show ?case by(auto simp add: Bot_ivl_def rep_ivl_def empty_def)
 qed
 
-permanent_interpretation
+global_interpretation
   Val_abs1 rep_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl
 proof
   case goal1 thus ?case
@@ -200,7 +200,7 @@
       auto simp: rep_ivl_def min_option_def max_option_def le_option_def split: if_splits option.splits)
 qed
 
-permanent_interpretation
+global_interpretation
   Abs_Int1 rep_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl "(iter' 3)"
 defines afilter_ivl = afilter
 and bfilter_ivl = bfilter
diff -r 42d902e074e8 -r 5c68d06f97b3 src/HOL/IMP/Abs_Int_Den/Abs_Int_den2.thy
--- a/src/HOL/IMP/Abs_Int_Den/Abs_Int_den2.thy	Mon Dec 21 17:20:57 2015 +0100
+++ b/src/HOL/IMP/Abs_Int_Den/Abs_Int_den2.thy	Mon Dec 21 21:34:14 2015 +0100
@@ -192,7 +192,7 @@
 
 end
 
-permanent_interpretation
+global_interpretation
   Abs_Int1 rep_ivl num_ivl plus_ivl filter_plus_ivl filter_less_ivl "(iter' 3 2)"
 defines afilter_ivl' = afilter
 and bfilter_ivl' = bfilter
diff -r 42d902e074e8 -r 5c68d06f97b3 src/HOL/IMP/Abs_Int_ITP/Abs_Int1_const_ITP.thy
--- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int1_const_ITP.thy	Mon Dec 21 17:20:57 2015 +0100
+++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int1_const_ITP.thy	Mon Dec 21 21:34:14 2015 +0100
@@ -52,7 +52,7 @@
 end
 
 
-permanent_interpretation Val_abs
+global_interpretation Val_abs
 where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const
 proof
   case goal1 thus ?case
@@ -66,7 +66,7 @@
     by(auto simp: plus_const_cases split: const.split)
 qed
 
-permanent_interpretation Abs_Int
+global_interpretation Abs_Int
 where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const
 defines AI_const = AI and step_const = step' and aval'_const = aval'
 ..
@@ -114,7 +114,7 @@
 
 text{* Monotonicity: *}
 
-permanent_interpretation Abs_Int_mono
+global_interpretation Abs_Int_mono
 where \<gamma> = \<gamma>_const and num' = Const and plus' = plus_const
 proof
   case goal1 thus ?case
diff -r 42d902e074e8 -r 5c68d06f97b3 src/HOL/IMP/Abs_Int_ITP/Abs_Int1_parity_ITP.thy
--- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int1_parity_ITP.thy	Mon Dec 21 17:20:57 2015 +0100
+++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int1_parity_ITP.thy	Mon Dec 21 21:34:14 2015 +0100
@@ -113,7 +113,7 @@
 proofs (they happened in the instatiation above) but delivers the
 instantiated abstract interpreter which we call AI: *}
 
-permanent_interpretation Abs_Int
+global_interpretation Abs_Int
 where \<gamma> = \<gamma>_parity and num' = num_parity and plus' = plus_parity
 defines aval_parity = aval' and step_parity = step' and AI_parity = AI
 ..
@@ -141,7 +141,7 @@
 
 subsubsection "Termination"
 
-permanent_interpretation Abs_Int_mono
+global_interpretation Abs_Int_mono
 where \<gamma> = \<gamma>_parity and num' = num_parity and plus' = plus_parity
 proof
   case goal1 thus ?case
diff -r 42d902e074e8 -r 5c68d06f97b3 src/HOL/IMP/Abs_Int_ITP/Abs_Int2_ivl_ITP.thy
--- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int2_ivl_ITP.thy	Mon Dec 21 17:20:57 2015 +0100
+++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int2_ivl_ITP.thy	Mon Dec 21 21:34:14 2015 +0100
@@ -165,7 +165,7 @@
          I (max_option False (l1 + Some 1) l2) h2)
    else (I (max_option False l1 l2) h1, I l2 (min_option True h1 h2)))"
 
-permanent_interpretation Val_abs
+global_interpretation Val_abs
 where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = plus_ivl
 proof
   case goal1 thus ?case
@@ -179,7 +179,7 @@
     by(auto simp add: \<gamma>_ivl_def plus_ivl_def split: ivl.split option.splits)
 qed
 
-permanent_interpretation Val_abs1_gamma
+global_interpretation Val_abs1_gamma
 where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = plus_ivl
 defines aval_ivl = aval'
 proof
@@ -198,7 +198,7 @@
 done
 
 
-permanent_interpretation Val_abs1
+global_interpretation Val_abs1
 where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = plus_ivl
 and test_num' = in_ivl
 and filter_plus' = filter_plus_ivl and filter_less' = filter_less_ivl
@@ -215,7 +215,7 @@
       auto simp: \<gamma>_ivl_def min_option_def max_option_def le_option_def split: if_splits option.splits)
 qed
 
-permanent_interpretation Abs_Int1
+global_interpretation Abs_Int1
 where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = plus_ivl
 and test_num' = in_ivl
 and filter_plus' = filter_plus_ivl and filter_less' = filter_less_ivl
@@ -229,7 +229,7 @@
 
 text{* Monotonicity: *}
 
-permanent_interpretation Abs_Int1_mono
+global_interpretation Abs_Int1_mono
 where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = plus_ivl
 and test_num' = in_ivl
 and filter_plus' = filter_plus_ivl and filter_less' = filter_less_ivl
diff -r 42d902e074e8 -r 5c68d06f97b3 src/HOL/IMP/Abs_Int_ITP/Abs_Int3_ITP.thy
--- a/src/HOL/IMP/Abs_Int_ITP/Abs_Int3_ITP.thy	Mon Dec 21 17:20:57 2015 +0100
+++ b/src/HOL/IMP/Abs_Int_ITP/Abs_Int3_ITP.thy	Mon Dec 21 21:34:14 2015 +0100
@@ -225,7 +225,7 @@
 
 end
 
-permanent_interpretation Abs_Int2
+global_interpretation Abs_Int2
 where \<gamma> = \<gamma>_ivl and num' = num_ivl and plus' = plus_ivl
 and test_num' = in_ivl
 and filter_plus' = filter_plus_ivl and filter_less' = filter_less_ivl
diff -r 42d902e074e8 -r 5c68d06f97b3 src/HOL/IMP/Abs_Int_ITP/Collecting_ITP.thy
--- a/src/HOL/IMP/Abs_Int_ITP/Collecting_ITP.thy	Mon Dec 21 17:20:57 2015 +0100
+++ b/src/HOL/IMP/Abs_Int_ITP/Collecting_ITP.thy	Mon Dec 21 21:34:14 2015 +0100
@@ -89,7 +89,7 @@
  WHILE b DO lift F c (sub\<^sub>1 ` M)
  {F (post ` M)}"
 
-permanent_interpretation Complete_Lattice_ix "%c. {c'. strip c' = c}" "lift Inter"
+global_interpretation Complete_Lattice_ix "%c. {c'. strip c' = c}" "lift Inter"
 proof
   case goal1
   have "a:A \<Longrightarrow> lift Inter (strip a) A \<le> a"
diff -r 42d902e074e8 -r 5c68d06f97b3 src/HOL/IMP/Collecting.thy
--- a/src/HOL/IMP/Collecting.thy	Mon Dec 21 17:20:57 2015 +0100
+++ b/src/HOL/IMP/Collecting.thy	Mon Dec 21 21:34:14 2015 +0100
@@ -94,7 +94,7 @@
 definition Inf_acom :: "com \<Rightarrow> 'a::complete_lattice acom set \<Rightarrow> 'a acom" where
 "Inf_acom c M = annotate (\<lambda>p. INF C:M. anno C p) c"
 
-permanent_interpretation
+global_interpretation
   Complete_Lattice "{C. strip C = c}" "Inf_acom c" for c
 proof (standard, goal_cases)
   case 1 thus ?case
diff -r 42d902e074e8 -r 5c68d06f97b3 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Mon Dec 21 17:20:57 2015 +0100
+++ b/src/HOL/Library/Multiset.thy	Mon Dec 21 21:34:14 2015 +0100
@@ -1054,7 +1054,7 @@
 lemma mset_map: "mset (map f xs) = image_mset f (mset xs)"
   by (induct xs) simp_all
 
-permanent_interpretation mset_set: folding "\<lambda>x M. {#x#} + M" "{#}"
+global_interpretation mset_set: folding "\<lambda>x M. {#x#} + M" "{#}"
   defines mset_set = "folding.F (\<lambda>x M. {#x#} + M) {#}"
   by standard (simp add: fun_eq_iff ac_simps)
 
diff -r 42d902e074e8 -r 5c68d06f97b3 src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Mon Dec 21 17:20:57 2015 +0100
+++ b/src/Pure/Isar/class.ML	Mon Dec 21 21:34:14 2015 +0100
@@ -686,7 +686,8 @@
         notes = Generic_Target.notes Generic_Target.theory_target_notes,
         abbrev = Generic_Target.abbrev Generic_Target.theory_target_abbrev,
         declaration = K Generic_Target.theory_declaration,
-        subscription = Generic_Target.theory_registration,
+        theory_registration = Generic_Target.theory_registration,
+        locale_dependency = fn _ => error "Not possible in instantiation target",
         pretty = pretty,
         exit = conclude #> Local_Theory.target_of #> Sign.change_end_local}
   end;
diff -r 42d902e074e8 -r 5c68d06f97b3 src/Pure/Isar/interpretation.ML
--- a/src/Pure/Isar/interpretation.ML	Mon Dec 21 17:20:57 2015 +0100
+++ b/src/Pure/Isar/interpretation.ML	Mon Dec 21 21:34:14 2015 +0100
@@ -11,33 +11,38 @@
   type 'a rewrites = (Attrib.binding * 'a) list
 
   (*interpretation in proofs*)
-  val interpret: Expression.expression_i -> term rewrites -> bool -> Proof.state -> Proof.state
-  val interpret_cmd: Expression.expression -> string rewrites -> bool -> Proof.state -> Proof.state
+  val interpret: Expression.expression_i ->
+    term rewrites -> bool -> Proof.state -> Proof.state
+  val interpret_cmd: Expression.expression ->
+    string rewrites -> bool -> Proof.state -> Proof.state
 
-  (*algebraic view*)
+  (*interpretation in local theories*)
+  val interpretation: Expression.expression_i ->
+    term rewrites -> local_theory -> Proof.state
+  val interpretation_cmd: Expression.expression ->
+    string rewrites -> local_theory -> Proof.state
+
+  (*interpretation into global theories*)
   val global_interpretation: Expression.expression_i ->
-    term defines -> term rewrites -> theory -> Proof.state
-  val global_sublocale: string -> Expression.expression_i ->
-    term defines -> term rewrites -> theory -> Proof.state
-  val global_sublocale_cmd: xstring * Position.T -> Expression.expression ->
-    string defines -> string rewrites -> theory -> Proof.state
+    term defines -> term rewrites -> local_theory -> Proof.state
+  val global_interpretation_cmd: Expression.expression ->
+    string defines -> string rewrites -> local_theory -> Proof.state
+
+  (*interpretation between locales*)
   val sublocale: Expression.expression_i ->
     term defines -> term rewrites -> local_theory -> Proof.state
   val sublocale_cmd: Expression.expression ->
     string defines -> string rewrites -> local_theory -> Proof.state
-
-  (*local-theory-based view*)
-  val ephemeral_interpretation: Expression.expression_i ->
-    term rewrites -> local_theory -> Proof.state
-  val permanent_interpretation: Expression.expression_i ->
-    term defines -> term rewrites -> local_theory -> Proof.state
-  val permanent_interpretation_cmd: Expression.expression ->
-    string defines -> string rewrites -> local_theory -> Proof.state
+  val global_sublocale: string -> Expression.expression_i ->
+    term defines -> term rewrites -> theory -> Proof.state
+  val global_sublocale_cmd: xstring * Position.T -> Expression.expression ->
+    string defines -> string rewrites -> theory -> Proof.state
 
   (*mixed Isar interface*)
-  val interpretation: Expression.expression_i -> term rewrites -> local_theory -> Proof.state
-  val interpretation_cmd: Expression.expression -> string rewrites ->
-    local_theory -> Proof.state
+  val isar_interpretation: Expression.expression_i ->
+    term rewrites -> local_theory -> Proof.state
+  val isar_interpretation_cmd: Expression.expression ->
+    string rewrites -> local_theory -> Proof.state
 end;
 
 structure Interpretation : INTERPRETATION =
@@ -172,28 +177,46 @@
 in
 
 fun interpret expression = gen_interpret cert_interpretation expression;
+
 fun interpret_cmd raw_expression = gen_interpret read_interpretation raw_expression;
 
 end;
 
 
-(* algebraic view *)
+(* interpretation in local theories *)
+
+fun interpretation expression =
+  generic_interpretation cert_interpretation Element.witness_proof_eqs
+    Local_Theory.notes_kind Locale.activate_fragment expression;
+
+fun interpretation_cmd raw_expression =
+  generic_interpretation read_interpretation Element.witness_proof_eqs
+    Local_Theory.notes_kind Locale.activate_fragment raw_expression;
+
+
+(* interpretation into global theories *)
+
+fun global_interpretation expression =
+  generic_interpretation_with_defs cert_interpretation Element.witness_proof_eqs
+    Local_Theory.notes_kind Local_Theory.theory_registration expression;
+
+fun global_interpretation_cmd raw_expression =
+  generic_interpretation_with_defs read_interpretation Element.witness_proof_eqs
+    Local_Theory.notes_kind Local_Theory.theory_registration raw_expression;
+
+
+(* interpretation between locales *)
+
+fun sublocale expression =
+  generic_interpretation_with_defs cert_interpretation Element.witness_proof_eqs
+    Local_Theory.notes_kind Local_Theory.locale_dependency expression;
+
+fun sublocale_cmd raw_expression =
+  generic_interpretation_with_defs read_interpretation Element.witness_proof_eqs
+    Local_Theory.notes_kind Local_Theory.locale_dependency raw_expression;
 
 local
 
-fun gen_global_interpretation prep_interpretation expression
-    raw_defs raw_eqns thy = 
-  let
-    val lthy = Named_Target.theory_init thy;
-    fun setup_proof after_qed =
-      Element.witness_proof_eqs
-        (fn wits => fn eqs => after_qed wits eqs #> Local_Theory.exit);
-  in
-    lthy |>
-      generic_interpretation_with_defs prep_interpretation setup_proof
-        Local_Theory.notes_kind Local_Theory.subscription expression raw_defs raw_eqns
-  end;
-
 fun gen_global_sublocale prep_loc prep_interpretation
     raw_locale expression raw_defs raw_eqns thy =
   let
@@ -204,56 +227,16 @@
   in
     lthy |>
       generic_interpretation_with_defs prep_interpretation setup_proof
-        Local_Theory.notes_kind Local_Theory.subscription expression raw_defs raw_eqns
+        Local_Theory.notes_kind Local_Theory.locale_dependency expression raw_defs raw_eqns
   end;
 
-fun subscribe_locale_only lthy =
-  let
-    val _ =
-      if Named_Target.is_theory lthy
-      then error "Not possible on level of global theory"
-      else ();
-  in Local_Theory.subscription end;
-
-fun gen_sublocale prep_interpretation expression raw_defs raw_eqns lthy =
-  generic_interpretation_with_defs prep_interpretation Element.witness_proof_eqs
-    Local_Theory.notes_kind (subscribe_locale_only lthy) expression raw_defs raw_eqns lthy;
-
 in
 
-fun global_interpretation expression =
-  gen_global_interpretation cert_interpretation expression;
 fun global_sublocale expression =
   gen_global_sublocale (K I) cert_interpretation expression;
+
 fun global_sublocale_cmd raw_expression =
   gen_global_sublocale Locale.check read_interpretation raw_expression;
-fun sublocale expression =
-  gen_sublocale cert_interpretation expression;
-fun sublocale_cmd raw_expression =
-  gen_sublocale read_interpretation raw_expression;
-
-end;
-
-
-(* local-theory-based view *)
-
-local
-
-fun gen_permanent_interpretation prep_interpretation expression raw_defs raw_eqns =
-  Local_Theory.assert_bottom true
-  #> generic_interpretation_with_defs prep_interpretation Element.witness_proof_eqs
-    Local_Theory.notes_kind Local_Theory.subscription expression raw_defs raw_eqns
-
-in
-
-fun ephemeral_interpretation expression =
-  generic_interpretation cert_interpretation Element.witness_proof_eqs
-    Local_Theory.notes_kind Locale.activate_fragment expression;
-
-fun permanent_interpretation expression =
-  gen_permanent_interpretation cert_interpretation expression;
-fun permanent_interpretation_cmd raw_expression =
-  gen_permanent_interpretation read_interpretation raw_expression;
 
 end;
 
@@ -262,21 +245,21 @@
 
 local
 
-fun subscribe_or_activate lthy =
+fun register_or_activate lthy =
   if Named_Target.is_theory lthy
-  then Local_Theory.subscription
+  then Local_Theory.theory_registration
   else Locale.activate_fragment;
 
-fun gen_local_theory_interpretation prep_interpretation expression raw_eqns lthy =
+fun gen_isar_interpretation prep_interpretation expression raw_eqns lthy =
   generic_interpretation prep_interpretation Element.witness_proof_eqs
-    Local_Theory.notes_kind (subscribe_or_activate lthy) expression raw_eqns lthy;
+    Local_Theory.notes_kind (register_or_activate lthy) expression raw_eqns lthy;
 
 in
 
-fun interpretation expression =
-  gen_local_theory_interpretation cert_interpretation expression;
-fun interpretation_cmd raw_expression =
-  gen_local_theory_interpretation read_interpretation raw_expression;
+fun isar_interpretation expression =
+  gen_isar_interpretation cert_interpretation expression;
+fun isar_interpretation_cmd raw_expression =
+  gen_isar_interpretation read_interpretation raw_expression;
 
 end;
 
diff -r 42d902e074e8 -r 5c68d06f97b3 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Mon Dec 21 17:20:57 2015 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Mon Dec 21 21:34:14 2015 +0100
@@ -407,6 +407,12 @@
     Scan.optional
       (@{keyword "rewrites"} |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) [];
 
+val _ =
+  Outer_Syntax.command @{command_keyword interpret}
+    "prove interpretation of locale expression in proof context"
+    (interpretation_args >> (fn (expr, equations) =>
+      Toplevel.proof' (Interpretation.interpret_cmd expr equations)));
+
 val interpretation_args_with_defs =
   Parse.!!! Parse_Spec.locale_expression --
     (Scan.optional (@{keyword "defines"} |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":"
@@ -415,6 +421,12 @@
       (@{keyword "rewrites"} |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) []);
 
 val _ =
+  Outer_Syntax.local_theory_to_proof @{command_keyword global_interpretation}
+    "prove interpretation of locale expression into global theory"
+    (interpretation_args_with_defs
+      >> (fn (expr, (defs, equations)) => Interpretation.global_interpretation_cmd expr defs equations));
+
+val _ =
   Outer_Syntax.command @{command_keyword sublocale}
     "prove sublocale relation between a locale and a locale expression"
     ((Parse.position Parse.xname --| (@{keyword "\<subseteq>"} || @{keyword "<"}) --
@@ -424,22 +436,11 @@
         Toplevel.local_theory_to_proof NONE NONE (Interpretation.sublocale_cmd expr defs equations)));
 
 val _ =
-  Outer_Syntax.local_theory_to_proof @{command_keyword permanent_interpretation}
-    "prove interpretation of locale expression into named theory"
-    (interpretation_args_with_defs
-      >> (fn (expr, (defs, equations)) => Interpretation.permanent_interpretation_cmd expr defs equations));
+  Outer_Syntax.command @{command_keyword interpretation}
+    "prove interpretation of locale expression in local theory or into global theory"
+    (interpretation_args >> (fn (expr, equations) =>
+      Toplevel.local_theory_to_proof NONE NONE (Interpretation.isar_interpretation_cmd expr equations)));
 
-val _ =
-  Outer_Syntax.command @{command_keyword interpretation}
-    "prove interpretation of locale expression in local theory"
-    (interpretation_args >> (fn (expr, equations) =>
-      Toplevel.local_theory_to_proof NONE NONE (Interpretation.interpretation_cmd expr equations)));
-
-val _ =
-  Outer_Syntax.command @{command_keyword interpret}
-    "prove interpretation of locale expression in proof context"
-    (interpretation_args >> (fn (expr, equations) =>
-      Toplevel.proof' (Interpretation.interpret_cmd expr equations)));
 
 
 (* classes *)
diff -r 42d902e074e8 -r 5c68d06f97b3 src/Pure/Isar/local_theory.ML
--- a/src/Pure/Isar/local_theory.ML	Mon Dec 21 17:20:57 2015 +0100
+++ b/src/Pure/Isar/local_theory.ML	Mon Dec 21 21:34:14 2015 +0100
@@ -52,7 +52,9 @@
   val abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory ->
     (term * term) * local_theory
   val declaration: {syntax: bool, pervasive: bool} -> declaration -> local_theory -> local_theory
-  val subscription: string * morphism -> (morphism * bool) option -> morphism ->
+  val theory_registration: string * morphism -> (morphism * bool) option -> morphism ->
+    local_theory -> local_theory
+  val locale_dependency: string * morphism -> (morphism * bool) option -> morphism ->
     local_theory -> local_theory
   val pretty: local_theory -> Pretty.T list
   val add_thms_dynamic: binding * (Context.generic -> thm list) -> local_theory -> local_theory
@@ -92,7 +94,9 @@
   abbrev: Syntax.mode -> (binding * mixfix) * term -> local_theory ->
     (term * term) * local_theory,
   declaration: {syntax: bool, pervasive: bool} -> declaration -> local_theory -> local_theory,
-  subscription: string * morphism -> (morphism * bool) option -> morphism ->
+  theory_registration: string * morphism -> (morphism * bool) option -> morphism ->
+     local_theory -> local_theory,
+  locale_dependency: string * morphism -> (morphism * bool) option -> morphism ->
      local_theory -> local_theory,
   pretty: local_theory -> Pretty.T list,
   exit: local_theory -> Proof.context};
@@ -267,8 +271,10 @@
 val define_internal = operation2 #define true;
 val notes_kind = operation2 #notes;
 val declaration = operation2 #declaration;
-fun subscription dep_morph mixin export =
-  assert_bottom true #> operation (fn ops => #subscription ops dep_morph mixin export);
+fun theory_registration dep_morph mixin export =
+  assert_bottom true #> operation (fn ops => #theory_registration ops dep_morph mixin export);
+fun locale_dependency dep_morph mixin export =
+  assert_bottom true #> operation (fn ops => #locale_dependency ops dep_morph mixin export);
 
 
 (* theorems *)
diff -r 42d902e074e8 -r 5c68d06f97b3 src/Pure/Isar/named_target.ML
--- a/src/Pure/Isar/named_target.ML	Mon Dec 21 17:20:57 2015 +0100
+++ b/src/Pure/Isar/named_target.ML	Mon Dec 21 21:34:14 2015 +0100
@@ -89,8 +89,12 @@
 fun declaration ("", _) flags decl = Generic_Target.theory_declaration decl
   | declaration (locale, _) flags decl = Generic_Target.locale_declaration locale flags decl;
 
-fun subscription ("", _) = Generic_Target.theory_registration
-  | subscription (locale, _) = Generic_Target.locale_dependency locale;
+fun theory_registration ("", _) = Generic_Target.theory_registration
+  | theory_registration _ = (fn _ => error "Not possible in theory target");
+
+fun locale_dependency ("", false) = (fn _ => error "Not possible in locale target")
+  | locale_dependency ("", true) = (fn _ => error "Not possible in class target")
+  | locale_dependency (locale, _) = Generic_Target.locale_dependency locale;
 
 fun pretty (target, is_class) ctxt =
   if target = "" then
@@ -144,7 +148,8 @@
         notes = Generic_Target.notes (notes name_data),
         abbrev = abbrev name_data,
         declaration = declaration name_data,
-        subscription = subscription name_data,
+        theory_registration = theory_registration name_data,
+        locale_dependency = locale_dependency name_data,
         pretty = pretty name_data,
         exit = the_default I before_exit
           #> Local_Theory.target_of #> Sign.change_end_local}
diff -r 42d902e074e8 -r 5c68d06f97b3 src/Pure/Isar/overloading.ML
--- a/src/Pure/Isar/overloading.ML	Mon Dec 21 17:20:57 2015 +0100
+++ b/src/Pure/Isar/overloading.ML	Mon Dec 21 21:34:14 2015 +0100
@@ -204,7 +204,8 @@
         notes = Generic_Target.notes Generic_Target.theory_target_notes,
         abbrev = Generic_Target.abbrev Generic_Target.theory_target_abbrev,
         declaration = K Generic_Target.theory_declaration,
-        subscription = Generic_Target.theory_registration,
+        theory_registration = Generic_Target.theory_registration,
+        locale_dependency = fn _ => error "Not possible in overloading target",
         pretty = pretty,
         exit = conclude #> Local_Theory.target_of #> Sign.change_end_local}
   end;
diff -r 42d902e074e8 -r 5c68d06f97b3 src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Mon Dec 21 17:20:57 2015 +0100
+++ b/src/Pure/Pure.thy	Mon Dec 21 21:34:14 2015 +0100
@@ -35,8 +35,8 @@
   and "include" "including" :: prf_decl
   and "print_bundles" :: diag
   and "context" "locale" "experiment" :: thy_decl_block
-  and "permanent_interpretation" "interpretation" "sublocale" :: thy_goal
   and "interpret" :: prf_goal % "proof"
+  and "interpretation" "global_interpretation" "sublocale" :: thy_goal
   and "class" :: thy_decl_block
   and "subclass" :: thy_goal
   and "instantiation" :: thy_decl_block