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
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
