Re: [isabelle] Duplicate constant declaration in sublocale
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?
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)
"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"
This archive was generated by a fusion of
Pipermail (Mailman edition) and