Re: [isabelle] Conflicting locales with a common signature



Hi Michael,

> Thanks -- but I think I already have that in locexp. It seems that
> Isabelle thinks the parameter f of loc1 and the parameter f of loc2 are
> distinct (even both loc1 and loc2 inherit that from sig_loc), so are
> there ways to somehow associate them together? 

You just need to give both parameters the same name on import, e.g.:

locale A =
  fixes f
  assumes involutory: "f ∘ f = id"

locale B =
  fixes g
  assumes idempotency: "g ∘ g = g"

locale C = A h + B h for h
begin

lemma "h = id"
using involutory idempotency by simp

end

Note also that the concept of locale import has little to do with the
object-oriented concept of inheritance, so it is rarely helpful to think
in that category.

Hope this helps,
	Florian

-- 

Home:
http://www.in.tum.de/~haftmann

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

Attachment: signature.asc
Description: OpenPGP digital signature



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.