[isabelle] type_synonym and dummy types

[Peter Lammich]

Hi, consider the following definition

  definition finite_rel :: "_ rel ⇒ bool" where "finite_rel ≡ finite"

I would expect to define a constant that is restricted to relations,
i.e., ('a*'a) set, as suggested by 

type_synonym 'a rel = "('a × 'a) set"


However, the expansion of type_synonym seems to take place before
expansion of underscores, such that I actually get

consts
  finite_rel :: "('a × 'b) set ⇒ bool"

i.e., a constant that is more general than expected.


Is this just a random feature, or is their some rationale behind?


--
  Peter

[Andreas Lochbihler]

Hi Peter,

I'd say that this is a random feature from user perspective, but I
believe that there is some rationale in terms of implementation
complexitz behind that. As you've observed, dummy types are instantiated
with fresh variables only after type abbreviations have been expanded.
The expansion mechanism would have to be more complicated if it had to
track which dummy types variables are derived from the same syntactic
input term.

By the way, IIRC I noticed this behaviour many years ago when we worked
together on our first joint formalisation and you had used dummy types
in there. Since then, I've tried to avoid dummy types unless for
experiments.

Best,
Andreas

Post by Peter Lammich
Hi, consider the following definition
definition finite_rel :: "_ rel ⇒ bool" where "finite_rel ≡ finite"
I would expect to define a constant that is restricted to relations,
i.e., ('a*'a) set, as suggested by
type_synonym 'a rel = "('a × 'a) set"
However, the expansion of type_synonym seems to take place before
expansion of underscores, such that I actually get
consts
finite_rel :: "('a × 'b) set ⇒ bool"
i.e., a constant that is more general than expected.
Is this just a random feature, or is their some rationale behind?
--
Peter

[Dominique Unruh]

Post by Andreas Lochbihler
I'd say that this is a random feature from user perspective, but I
believe that there is some rationale in terms of implementation
complexitz behind that. As you've observed, dummy types are instantiated
with fresh variables only after type abbreviations have been expanded.
The expansion mechanism would have to be more complicated if it had to
track which dummy types variables are derived from the same syntactic
input term.

Of course, that leaves the question open why not instantiate the dummy
types with fresh variables before expanding the type abbreviations.
(Of course, it might be that that's simply too hard to change now without
braking things.)

Best wishes,
Dominique.

Post by Andreas Lochbihler

Post by Peter Lammich
Hi, consider the following definition
definition finite_rel :: "_ rel ⇒ bool" where "finite_rel ≡ finite"
I would expect to define a constant that is restricted to relations,
i.e., ('a*'a) set, as suggested by
type_synonym 'a rel = "('a × 'a) set"
However, the expansion of type_synonym seems to take place before
expansion of underscores, such that I actually get
consts
finite_rel :: "('a × 'b) set ⇒ bool"
i.e., a constant that is more general than expected.
Is this just a random feature, or is their some rationale behind?
--
Peter