theory Interpretation_in_nested_targets
  imports Main
begin

locale injection =
  fixes f :: ‹'a → 'b›
  assumes eqI: ‹f x = f y ==> x = y›
begin

lemma eq_iff:
  ‹x = y ⟷ f x = f y›
  by (auto intro: eqI)

lemma inv_apply:
  ‹inv f (f x) = x›
  by (rule inv_f_f) (simp add: eqI injI)

end

context
  fixes f :: ‹'a::linorder → 'b::linorder›
  assumes ‹strict_mono f›
begin

global_interpretation strict_mono: injection f
  by standard (simp add: ‹strict_mono f› 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