*To*: Cl-isabelle Users <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] Problem with "additional type variables" in a definition*From*: Lars-Henrik Eriksson <lhe at it.uu.se>*Date*: Tue, 24 May 2016 17:04:01 +0200*In-reply-to*: <809030A8-4336-489A-ABD6-D8D555561B58@exchange.uibk.ac.at>*References*: <58B252C5-05D9-4412-B0DC-CD97FF5B1C36@it.uu.se> <809030A8-4336-489A-ABD6-D8D555561B58@exchange.uibk.ac.at>

24 maj 2016 kl. 12:09 skrev Thiemann, Rene <Rene.Thiemann at uibk.ac.at>: > > Dear Lars-Henrik, > > The problem is the implicit type âa in the definition of foo. To this end, Isabelle inserts a > dummy argument in the definition of foo of type (âa itself). So your definition becomes > > definition foo' :: "'a itself â bool" where > "foo' _ â â x :: 'a. Trueâ > > you also see this definition, if you perform a âprint_theoremsâ after your definition of âfooâ. > > Hope this helps, > RenÃ Dear RenÃ, Thank you. I suspected as much, but it doesn't really help me until I understand why and how this happens. It seems the extra argument to foo is not an ordinary argument but some kind of type argument. The definition does not become what you suggest but rather (using the command thm foo_def with show_types) foo TYPE(?'a) â âx::?'a. True Even more confusing, when the definition is in a locale where the additional type is also used in the locale definition, as in: locale test = assumes "âx :: 'a. True" begin definition foo :: "bool" ("f" 50) where "foo â âx :: 'a. True" abbreviation bar :: "bool" where "bar â foo" lemma "foo" unfolding foo_def by simp lemma "bar" sorry end then both the abbreviation and the lemma "foo" work (although the mixfix syntax is still dropped), however the lemma "bar" gives the same type error that lemma "foo" did in my original example. 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".) Lars-Henrik Lars-Henrik Eriksson, PhD, Senior Lecturer Computing Science, Dept. of Information Technology, Uppsala University, Sweden

**Follow-Ups**:

**References**:**[isabelle] Problem with "additional type variables" in a definition***From:*Lars-Henrik Eriksson

**Re: [isabelle] Problem with "additional type variables" in a definition***From:*Thiemann, Rene

- Previous by Date: Re: [isabelle] Isabelle 2005 request
- Next by Date: [isabelle] ThEdu at CICM'16 deadline approaching
- Previous by Thread: Re: [isabelle] Problem with "additional type variables" in a definition
- Next by Thread: Re: [isabelle] Problem with "additional type variables" in a definition
- Cl-isabelle-users May 2016 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list