# [isabelle] Duplicate constant declaration in sublocale

*To*: isabelle-users <isabelle-users at cl.cam.ac.uk>
*Subject*: [isabelle] Duplicate constant declaration in sublocale
*From*: Lars Noschinski <noschinl at in.tum.de>
*Date*: Fri, 19 Apr 2013 11:41:47 +0200
*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:10.0.12) Gecko/20130116 Icedove/10.0.12

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
=======

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*