Reputation: 513
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
anddefines
, 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
anddefines
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.)
Upvotes: 3
Views: 164
Reputation: 5078
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 ..."
Upvotes: 3