Re: [isabelle] problem with locales



Dear Andreas,

Using constrains solved my problem. Using this constrains declaration
seem like a nice solution to this problem. I don't see the reason to
remove it, but on the contrary to document it well.

I had earlier this problem and the way I solved it was by imposing
additional dummy assumptions on the imported constants.

Best regards,

Viorel



On 11/07/2011 02:01 PM, Andreas Lochbihler wrote:
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,
Andreas

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)"
begin
definition "domain f = {x :: 'node . - (f x = (nil::'node))}"
end

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,

Viorel








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