Re: [isabelle] Specializing types in locales



Dear Mathieu,

Type instances (like other parameter instantiations) should be given in the locale expression. In your example, use something like

  locale foo1_nat_loc' = foo1_loc bar foo for bar :: nat and foo

to instantiate the parameter bar with some bar of type nat, which will become a parameter of the new locale.

The constrains element stems from times when locale expressions were based on renaming rather than instantiation. It is deprecated and will disappear in a future release of Isabelle.

Clemens


Quoting Mathieu Giorgino <mathieu.giorgino at irit.fr>:

Hello all,

In a locale, when a definition uses a parameter, specialization of one of his
type variables through constrains on an other parameter seems not possible.
However, it is possible with constrains on this parameter.

For example:

-------
locale foo1_loc =
  fixes bar :: "'a"
  fixes foo :: "'a"
begin
definition "foo' a = foo"
end

locale foo1_nat_loc = foo1_loc +
  constrains foo :: "nat"

(*
locale foo1_nat_loc' = foo1_loc +
  constrains bar :: "nat"
Error: Failed to meet type constrain
*)
-------

As a result, it seems impossible to specialize a type variable shared by
several parameters used in definitions:

-------
locale foo3_loc =
  fixes bar :: "'a"
  fixes foo :: "'a"
begin
definition "foobar = (foo, bar)"
end

(*
locale foo3_nat_loc = foo3_loc +
  constrains bar :: "nat"
  constrains foo :: "nat"
Error: Failed to meet type constrain
*)
-------

See attachment for more examples.

Is this a bug or is there any fundamental reason this doesn't work ?

To solve this problem, a great feature would be to have specializable type
declarations but I've understood it wasn't possible due to the logical
framework (quantification on types) in an email from Makarius:
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2009-July/msg00111.html

I know I could also use AWE, but there is no release for Isabelle 2009-2 (but
I haven't tried the one for Isabelle 2009-2 that could perhaps also work).

Furthermore in an other mail, Makarius said:
Trying a bit harder in the internal structures, one could support type
parameters on the RHS one day.
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2010-July/msg00033.html

Is this still a possibility ?


Thanks,

Mathieu Giorgino








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