Re: [isabelle] Problem with "additional type variables" in a definition



On 24/05/16 17:04, Lars-Henrik Eriksson wrote:
> 24 maj 2016 kl. 12:09 skrev Thiemann, Rene <Rene.Thiemann at uibk.ac.at>:
> 
> Is there some document that describes the behaviour of definitions in the presence of "additional" type variables? I find no explanation of it neither in the Isabelle/Isar Reference Manual, nor in the Tutorial on Locales. (I have specifically searched for "itself" and "TYPE".)

See the "implementation" manual section "2.3.2 Auxiliary connectives";
it also refers to Section 2.2 about "hidden polymorphism", which is the
problem being solved here. Section "2.3.3 Sort hypotheses" is also related.

There is a much longer story behind all that, going back to early
versions of Gordon-style HOL that allowed such "hidden polymorphism" in
definitions that were not definitions. That caused a total existence
failure of the logic.


	Makarius





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