[isabelle] Local types do not work in for declarations of locales



Dear localisation experts,

I have a locale with polymorphic parameters and would like instantiate the type variables in a sublocale. I know of two ways to achieve this:

1. Declare the parameters in a for clause with the specialised types.
2. Use the context element constrains with the specialised types.

From past discussions on this mailing list, I have the impression that "constrains" is considered outdated and should be replaced with for clauses (for example in https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2014-February/msg00138.html).

I now ran into a problem with approach 1 when there are local type synonyms. Below is a minimal example. Locale l declares a type with a type variable, its sublocale l1 fixes a parameter whose type contains the local type, and l1's sublocale l2 tries to instantiate type type variable:

  locale l begin
  typedef 'a td = "UNIV :: 'a set" ..
  end

  locale l1 = l + fixes y :: "'a td"

  locale l2 = l1 y for y :: "bool td"

Here, I get an error in the last line claiming that td was an undefined type name. The declaration works if I use constrains instead of a for clause.

  locale l2 = l1 + constrains y :: "bool td"

Alternatively, I can go via the foundational type, but this seems to be somewhat ugly.

  locale l2 = l1 y for y :: "bool l.td"

Is this a known limitation of localised typedef/type_synonym and/or a valid reason for using the "deprecated" constrains element?

Best,
Andreas




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