Email Gateway (Aug 19 2022 at 10:56): Email Gateway (Aug 19 2022 at 10:56):From: Lars Noschinski <noschinl@in.tum.de>
Hi,
I have locale A, B and I want to declare B as a sublocale of A. In doing
so, some of the constants in A can be replaced by simpler ones. I tried
to use the same names first, but got the following error from the
sublocale command:
Duplicate constant declaration "local.g" vs. "local.g"
This is not to surprising. However, if I change the definition of g in B
by removing the explicit type annotation (or use some other type
variable there), the sublocale command succeeds (of course, this is not
a solution to my problem, because I want to have exactly the specified
type for my constant).
Can anyone explain to me what is happening here? Is there a way to
declare B a sublocale of A without adding a prefix to A?
-- Lars
=====================
theory Sublocale_Equations imports Main
begin
record ('a,'b) rec =
proj :: "'b ⇒ 'a"
locale A = fixes G :: "('a, 'b) rec" begin
definition g :: "'a ⇒ 'b ⇒ bool" where
"g u e = (proj G e = u)"
end
locale B = fixes dummy :: 'a begin
definition "to_rec = ⦇ proj = (fst :: 'a × 'a ⇒ 'a) ⦈"
definition g :: "'a ⇒ ('a × 'a) ⇒ bool" where
"g u e = (fst e = u)"
lemma [simp]: "proj to_rec = fst" by (auto simp: to_rec_def)
lemma [simp]:
"A.g to_rec = g"
by (auto simp: g_def A.g_def fun_eq_iff to_rec_def)
end
sublocale B ⊆ A "to_rec"
where "proj to_rec = fst" and "A.g to_rec = B.g"
apply unfold_locales
apply auto
done
=======
Email Gateway (Aug 19 2022 at 10:56):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Lars,
This looks really weird and I don't have an explanation, either, But you can make B a
sublocale of A if you move g's definition in A into the locale declaration:
locale A = fixes G :: "('a, 'b) rec"
fixes g :: "'a => 'b => bool"
defines g_def: "g u e == proj G e = u"
begin
end
Andreas
Email Gateway (Aug 19 2022 at 10:57):From: Lars Noschinski <noschinl@in.tum.de>
Hi Andreas,
Thanks for your suggestion. Unfortunately, this is not an option for me
as g is defined much later than the the locale.
-- Lars
Email Gateway (Aug 19 2022 at 11:04):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Lars,
I have no concrete idea, but I guess this is due to the pitfalls of
parsing and processing those interpretation expressions, as Clemens has
indicated on a similar thread on isabelle-dev.
Cheers,
Florian
signature.asc
Last updated: Apr 18 2024 at 20:16 UTC