Re: [isabelle] Duplicate constant declaration in sublocale

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"


On 19/04/13 11:41, Lars Noschinski wrote:

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

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)"


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)


sublocale B ⊆ A "to_rec"
    where "proj to_rec = fst" and "A.g to_rec = B.g"
   apply unfold_locales
   apply auto

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