Re: [isabelle] problem with locales

Dear Viorel,

when locales inherit from other locales, Isabelle always renames type variables of the inherited locales to 'a, 'b, 'c, etc. There are two ways to undo the renaming:

a) Do not use the locale feature of implicitly adding unmentioned parameters of imported locales to the for clause, but state them explicitly:

locale list = node nil for nil :: "'node" + ...

The drawback is that you have to redeclare mixfix syntax if your imported locale declares such for the parameter. If you do not plan to use syntax annotations anyway, this is the preferred way.

b) Constrain the parameter types using "constrains":

locale list = node +
  constrains nil :: "'node"
  fixes "next" :: "'node => node"

The advantage is that constrains does not delete mixfix syntax. However, Clemens has threatened to remove this rarely known feature in some futute release. Moreover, this often still gives you type error messages. I found that it works reliably if
1. the locale inherits from exactly one other locale,
2. you constrain all inherited parameters consistently, and
3. in the locale assumptions, you do not refer to constants defined in the inherited locale (or any of its anchestors).

Both solutions are not ideal and I would be glad if the locale mechanism did not rename type variable apparently randomly. However, I haven't yet been able to convince the Isabelle developpers solve this problem.

Best regards,

Am 07.11.2011 12:45, schrieb Viorel Preoteasa:
I have the following two locales:

locale node =
fixes nil :: "'node"
assumes infinite: "¬ finite (UNIV::'node set)"
definition "domain f = {x :: 'node . - (f x = (nil::'node))}"

locale list = node +
fixes "next" :: "'node => 'node"
fixes val :: "'node => 'node"
assumes "next (nil::'node) = nil"

These locales generate error "Type unification failed". If I drop the
definition from the first locale then I do not get this message.

More generally. Is there a standard mechanism to enforce
the type 'node from the first locale to be the same as the
type node from the second locale?

Best regards,


Karlsruher Institut für Technologie
IPD Snelting

Andreas Lochbihler
wissenschaftlicher Mitarbeiter
Adenauerring 20a, Geb. 50.41, Raum 031
76131 Karlsruhe

Telefon: +49 721 608-47399
Fax: +49 721 608-48457
E-Mail: andreas.lochbihler at
KIT - Universität des Landes Baden-Württemberg und nationales Forschungszentrum in der Helmholtz-Gemeinschaft

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