[isabelle-dev] [isabelle] Duplicate constant declaration in sublocale

[Florian Haftmann]

Hi Lars,

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

maybe in the future this a solution to your problem:

> 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)
> 
> interpretation foo: A to_rec
> where
>   "proj to_rec = fst" and
>   "A.g to_rec = B.g"
>   apply unfold_locales
>   apply auto
>   done 
> 
> lemmas bar = foo.g_def

I.e. do an interpretation confined to the surface context and then
cherry-pick the lemmas you want.

Cheers,
	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 261 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20130529/dfe92707/attachment.asc>