[isabelle] Duplicate constant declaration in sublocale



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.