*To*: Lars Noschinski <noschinl at in.tum.de>*Subject*: Re: [isabelle] Duplicate constant declaration in sublocale*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Date*: Fri, 19 Apr 2013 12:27:42 +0200*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <5171115B.6060502@in.tum.de>*References*: <5171115B.6060502@in.tum.de>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:17.0) Gecko/20130329 Thunderbird/17.0.5

Hi Lars,

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 On 19/04/13 11:41, Lars Noschinski wrote:

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

**Follow-Ups**:**Re: [isabelle] Duplicate constant declaration in sublocale***From:*Lars Noschinski

**References**:**[isabelle] Duplicate constant declaration in sublocale***From:*Lars Noschinski

- Previous by Date: [isabelle] Duplicate constant declaration in sublocale
- Next by Date: [isabelle] CfP: OpenMath workshop at CICM (10 July, Bath, UK), submission deadline 7 June
- Previous by Thread: [isabelle] Duplicate constant declaration in sublocale
- Next by Thread: Re: [isabelle] Duplicate constant declaration in sublocale
- Cl-isabelle-users April 2013 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list