[isabelle-dev] [isabelle] Duplicate constant declaration in sublocale
Florian Haftmann
florian.haftmann at informatik.tu-muenchen.de
Wed May 29 23:15:30 CEST 2013
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>
More information about the isabelle-dev
mailing list