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

lemma "h = id"
using involutory idempotency by simp


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,



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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