global interpretation into nested targets

--- a/NEWS	Wed Jun 09 18:04:21 2021 +0000
+++ b/NEWS	Wed Jun 09 18:04:22 2021 +0000
@@ -103,6 +103,13 @@
 no longer required.
 
 
+*** Pure ***
+
+* "global_interpretation" is applicable in instantiation and overloading
+targets and in any nested target built on top of a target supporting
+"global_interpretation".
+
+
 *** HOL ***
 
 * Theory "HOL-Library.Multiset": dedicated predicate "multiset" is gone,

--- a/src/Doc/Isar_Ref/Spec.thy	Wed Jun 09 18:04:21 2021 +0000
+++ b/src/Doc/Isar_Ref/Spec.thy	Wed Jun 09 18:04:22 2021 +0000
@@ -738,6 +738,9 @@
   free variable whose name is already bound in the context --- for example,
   because a constant of that name exists --- add it to the \<^theory_text>\<open>for\<close> clause.
 
+  When used in a nested target, resulting declarations are propagated
+  through the whole target stack.
+
   \<^descr> \<^theory_text>\<open>sublocale name \<subseteq> expr defines defs\<close> interprets \<open>expr\<close>
   into the locale \<open>name\<close>. A proof that the specification of \<open>name\<close> implies the
   specification of \<open>expr\<close> is required. As in the localized version of the

--- a/src/HOL/Library/Lexord.thy	Wed Jun 09 18:04:21 2021 +0000
+++ b/src/HOL/Library/Lexord.thy	Wed Jun 09 18:04:22 2021 +0000
@@ -194,8 +194,6 @@
     apply (auto simp add: dvd_strict_def)
   done
 
-print_theorems
-
 global_interpretation lex_dvd: preordering lex_dvd lex_dvd_strict
   by (fact dvd.preordering)
 

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/ex/Interpretation_in_nested_targets.thy	Wed Jun 09 18:04:22 2021 +0000
@@ -0,0 +1,36 @@
+theory Interpretation_in_nested_targets
+  imports Main
+begin
+
+locale injection =
+  fixes f :: \<open>'a \<Rightarrow> 'b\<close>
+  assumes eqI: \<open>f x = f y \<Longrightarrow> x = y\<close>
+begin
+
+lemma eq_iff:
+  \<open>x = y \<longleftrightarrow> f x = f y\<close>
+  by (auto intro: eqI)
+
+lemma inv_apply:
+  \<open>inv f (f x) = x\<close>
+  by (rule inv_f_f) (simp add: eqI injI)
+
+end
+
+context
+  fixes f :: \<open>'a::linorder \<Rightarrow> 'b::linorder\<close>
+  assumes \<open>strict_mono f\<close>
+begin
+
+global_interpretation strict_mono: injection f
+  by standard (simp add: \<open>strict_mono f\<close> strict_mono_eq)
+
+thm strict_mono.eq_iff
+thm strict_mono.inv_apply
+
+end
+
+thm strict_mono.eq_iff
+thm strict_mono.inv_apply
+
+end

--- a/src/Pure/Isar/generic_target.ML	Wed Jun 09 18:04:21 2021 +0000
+++ b/src/Pure/Isar/generic_target.ML	Wed Jun 09 18:04:22 2021 +0000
@@ -235,12 +235,13 @@
 fun standard_const pred prmode ((b, mx), rhs) =
   standard_declaration pred (const_decl (K true) prmode ((b, mx), rhs));
 
-fun local_interpretation registration lthy =
-  let val n = Local_Theory.level lthy in
-    lthy
-    |> Local_Theory.map_contexts (fn level =>
-      level = n - 1 ? Context.proof_map (Locale.add_registration registration))
-  end;
+fun standard_registration pred registration lthy =
+  Local_Theory.map_contexts (fn level =>
+    if pred (Local_Theory.level lthy, level)
+    then Context.proof_map (Locale.add_registration registration)
+    else I) lthy;
+
+val local_interpretation = standard_registration (fn (n, level) => level = n - 1);
 
 
 
@@ -406,7 +407,15 @@
 fun theory_declaration decl =
   background_declaration decl #> standard_declaration (K true) decl;
 
-val theory_registration = Local_Theory.raw_theory o Context.theory_map o Locale.add_registration;
+fun target_registration lthy {inst, mixin, export} =
+  {inst = inst, mixin = mixin,
+    export = export $> Proof_Context.export_morphism lthy (Local_Theory.target_of lthy)};
+
+fun theory_registration registration lthy =
+  lthy
+  |> (Local_Theory.raw_theory o Context.theory_map)
+    (Locale.add_registration (target_registration lthy registration))
+  |> standard_registration (K true) registration;
 
 
 (** locale target primitives **)
@@ -439,9 +448,10 @@
   locale_target_const locale (K true) prmode ((b, mx), rhs)
   #> standard_const (fn (this, other) => other <> 0 andalso this <> other) prmode ((b, mx), rhs);
 
-fun locale_dependency loc registration =
-  Local_Theory.raw_theory (Locale.add_dependency loc registration)
-  #> local_interpretation registration;
+fun locale_dependency loc registration lthy =
+  lthy
+  |> Local_Theory.raw_theory (Locale.add_dependency loc registration)
+  |> standard_registration (K true) registration;
 
 
 (** locale abbreviations **)

--- a/src/Pure/Isar/local_theory.ML	Wed Jun 09 18:04:21 2021 +0000
+++ b/src/Pure/Isar/local_theory.ML	Wed Jun 09 18:04:22 2021 +0000
@@ -253,6 +253,7 @@
 val operations_of = #operations o top_of;
 
 fun operation f lthy = f (operations_of lthy) lthy;
+fun operation1 f x = operation (fn ops => f ops x);
 fun operation2 f x y = operation (fn ops => f ops x y);
 
 
@@ -264,10 +265,9 @@
 val define_internal = operation2 #define true;
 val notes_kind = operation2 #notes;
 val declaration = operation2 #declaration;
-fun theory_registration registration =
-  assert_bottom #> operation (fn ops => #theory_registration ops registration);
+val theory_registration = operation1 #theory_registration;
 fun locale_dependency registration =
-  assert_bottom #> operation (fn ops => #locale_dependency ops registration);
+  assert_bottom #> operation1 #locale_dependency registration;
 
 
 (* theorems *)