Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Local types do not work in for declarations of...

view this post on Zulip Email Gateway (Aug 22 2022 at 10:35):

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
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

Last updated: Apr 19 2024 at 16:20 UTC