How to use a definition written on locale parameters in the assumptions of the locale?

Question

If there is some definition on the parameters of a locale which would make the assumptions of the locale easier to write and/or read and/or understand (either because the function is quite complicated so would simplify the statement of the assumptions, or its name makes the assumptions easier to read and understand), what is the best way to define that function?

As a contrived example, say we want to incorporate the function fg into the statement of the assumptions (not actually useful here of course):

locale defined_after =
  fixes f :: "'a ⇒ 'b ⇒ 'c"
    and g :: "'b ⇒ 'a"
  assumes "∀a. ∃b. f a b = f (g b) b"
      and univ: "(UNIV::'b set) = {b}"
begin

definition fg :: "'b ⇒ 'c" where
  "fg b ≡ f (g b) b"

lemma "∀b b'. fg b = fg b'" using univ the_elem_eq by (metis (full_types))

(* etc *)

end

One might think to use defines:

locale defined_during =
  fixes f :: "'a ⇒ 'b ⇒ 'c"
    and g :: "'b ⇒ 'a"
    and fg :: "'b ⇒ 'c" 
  defines fg_def: "fg b ≡ f (g b) b"
  assumes "∀a. ∃b. f a b = fg b"
      and univ: "(UNIV::'b set) = {b}"
begin

lemma "∀b b'. fg b = fg b'" using univ the_elem_eq by (metis (full_types))

end

but the locales.pdf document seems to suggest it is deprecated (but by what I'm not sure):

The grammar is complete with the exception of the context elements constrains and defines, which are provided for backward compatibility.

Ctrl-hovering over fg in the lemma in the locale defined_after names it as constant "local.fg" whereas in defined_during it is fixed fg\nfree variable. It does however achieve defined_after_def being equal to defined_during_def (i.e. there are no additional parameters or assumptions in the latter), which the third option does not:

locale extra_defined_during =
  fixes f :: "'a ⇒ 'b ⇒ 'c"
    and g :: "'b ⇒ 'a"
    and fg :: "'b ⇒ 'c" 
  assumes fg_def: "fg b ≡ f (g b) b"
      and "∀a. ∃b. f a b = fg b"
      and univ: "(UNIV::'b set) = {b}"
begin

lemma "∀b b'. fg b = fg b'" using univ the_elem_eq by (metis (full_types))

end

which also has the same Ctrl-hover text for fg in the lemma as the defined_during locale does.

Maybe there's something about it in one of the PDFs on the website, or in the NEWS file, but I can't find anything obvious. isar-ref.pdf makes a comment:

Both assumes and defines elements contribute to the locale specification. When defining an operation derived from the parameters, definition (§5.4) is usually more appropriate.

But I'm not sure how to use this information. Presumably it is saying that when one doesn't gain much by doing what I am asking about, one should proceed as in the locale defined_after (unless the quote means one can use definition inside a locale definition), which is not what I want. (As an aside: the first sentence of this quote would have suggested to me that defines is somehow equivalent to the third option which introduces an extra parameter and assumption, but that isn't the case. Maybe understanding what the possibly-subtler-than-it-appears-Isabelle-jargon "locale specification" means would explain what is causing the Ctrl-hover text to differ between the first and second option, I don't know.)

Answer 1

The specification element defines is indeed nothing that I would recommend to use. It goes back to a time when definition was not available inside a locale context and all definitions had to be done in the locale declaration itself.

Nowadays, the standard approach to your problem is to split the locale into two parts: First define a locale l1 without the complicated assumption, but with the relevant parameters. (If you need some assumptions to justify the definition, e.g. for the termination proof of function, include those assumptions.) Then define your function fg inside l1 as usual. Finally, define your actual locale l that extends l1. You can then use the definition of fg in the assumptions of l.

locale l = l1 + assumes "... fg ..."