[isabelle] Specializing types in locales



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

Attachment: Type_Specialization_Locales.thy
Description: application/isabelle-theory



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