Email Gateway (Jan 25 2024 at 06:12): Email Gateway (Jan 25 2024 at 06:12):From: hannobecker@posteo.de
Hi,
The following is about surprisingly (to me) strict behavior of
adhoc_overloading w.r.t. locale hierarchies.
Suppose adhoc_overloading is used in the context of locale A:
consts foo_const :: 'a
declare [[show_variants]]
locale constA =
fixes some_nat::nat
begin
definition ‹some_nat_x2 ≡ some_nat + some_nat›
adhoc_overloading foo_const some_nat_x2
term ‹foo_const + (0 :: nat)› (* OK: "some_nat_x2 + 0" *)
end
Now, we inherit from A in the definition of another locale B and check
if the adhoc_overloading is inherited as well:
locale constB = A: constA some_nat for some_nat :: nat +
fixes another_nat::nat
begin
term ‹foo_const + (0 :: nat)› (* OK: "A.some_nat_x2 + 0" *)
end
This looks good. But it turns out that it only works if the locale
parameter names for A exactly match. The following does not work:
locale constC = A: constA some_other_nat for some_other_nat :: nat +
fixes another_nat::nat
begin
term ‹foo_const + (0 :: nat)› (* FAIL? Surprising! *)
end
This is very surprising to me. It is also different from how
locale-local named theorem list amendments are inherited, which works in
the constC case as well.
Is adhoc_overloading's behaviorintentional here?
I looked into the source code and noted that the adhoc_overloading
declaration goes through a very strict term filter when morphisms are
applied:
fun adhoc_overloading_cmd' add args phi =
let val args' = args
|> map (apsnd (map_filter (fn t =>
let val t' = Morphism.term phi t;
in if Term.aconv_untyped (t, t') then SOME t' else NONE end)));
in generic_adhoc_overloading_cmd add args' end;
If, for the sake of experiment only, I always return SOME t' (which is
almost certainly not the right thing in general, of course), the
rigidity observed above goes away, and inheritance works as expected in
the specific example. Should the term filter be weakened? Or is there a
reason why the rigidity of adhoc_overloading is deliberate here?
Cheers,
Hanno
PS: Here's the complete standalone example
theory Locales
imports Main "HOL-Library.Adhoc_Overloading"
begin
consts foo_const :: 'a
declare [[show_variants]]
locale constA =
fixes some_nat::nat
begin
definition ‹some_nat_x2 ≡ some_nat + some_nat›
adhoc_overloading foo_const some_nat_x2
text‹Inside the context of the locale, this works fine›
term ‹foo_const + (0 :: nat)› (* "some_nat_x2 + 0" *)
end
text‹Outside of the locale, the overloading is not visible, as
expected:›
term ‹foo_const + (0 :: nat)› (* fail *)
text‹Let's see if it inherits to sublocales:›
locale constB = A: constA some_nat for some_nat :: nat +
fixes another_nat::nat
begin
term ‹foo_const + (0 :: nat)› (* OK: "A.some_nat_x2 + 0" *)
end
text‹This looked good, but now for the weird bit: Try renaming the
parameter to A!›
locale constC = A: constA some_other_nat for some_other_nat :: nat +
fixes another_nat::nat
begin
term ‹foo_const + (0 :: nat)› (* FAIL? Surprising! *)
end
end
From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Hanno,
this behavior occurs similarly for notations:
locale A =
fixes f :: ‹'a ⇒ 'a›
begin
notation f (‹⦇_⦈›)
term ‹f x›
end
locale B = A f for f
begin
term ‹f x›
end
locale C = A g for g
begin
term ‹g x›
end
The corresponding code presumably is
https://isabelle.in.tum.de/repos/isabelle/file/Isabelle2023/src/Pure/Isar/proof_context.ML#l1174
Personally, I would be inclined to attribute that extra-logical behavior
to a specific tradition in Isabelle how syntax is handled and
approximated. But this might be illusive.
Cheers,
Florian
OpenPGP_0xA707172232CFA4E9.asc
OpenPGP_signature.asc
Last updated: Apr 29 2024 at 01:08 UTC