[isabelle] Additional Type Parameter when Interpreting Locale Using 'for' Clause



Dear all,

I recently stumbled upon the following behavior in Isabelle which I
find surprising and which affects me negatively. In the attached
theory, the constant "bar" is defined in the locale "foo". This locale
is then interpreted as "baz" using a 'for' clause to retain the
parameter "f".

I had expected that "baz.bar" would be "% f. foo.bar f 0" :: "('a =>
'b) => 'b". Instead, it is "% type f. foo.bar f 0" :: "'a itself =>
('a => 'b) => 'b". Why is there a type parameter, given that the type
variable "'a" is already determined by the parameter "f"? It seems
that Andreas Lochbihler has already stumbled upon the same issue
(https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2010-April/msg00029.html),
but it did not get any replies. It seems that everything works when I
instantiate the parameter "type" with "TYPE('a)", but I would prefer
if I didn't have to do that.

Regards,
 Julian

Attachment: TypeParameter.thy
Description: Binary data



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