*To*: Ed Schwartz <edmcman at gmail.com>*Subject*: Re: [isabelle] Isar polymorphism problem*From*: Peter Lammich <lammich at in.tum.de>*Date*: Mon, 28 Apr 2014 17:35:39 +0200*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <CAHPz_Mq6WGbEq4KrdMdH9NDSJt7-0foS02-R13s0fji1OfPcQw@mail.gmail.com>*References*: <CAHPz_Mr8KgKU4966DTROET1AgtJs-gDfU-YQ=AVNZUzcDRxz6Q@mail.gmail.com> <1398688712.2438.74.camel@lapbroy33> <CAHPz_Mq6WGbEq4KrdMdH9NDSJt7-0foS02-R13s0fji1OfPcQw@mail.gmail.com>

A polymorphic type in a statement can be instantiated by any type. Thus, you can think of them as being implicitely universally qualified. > What I want to state instead is: > There exists a type 'a such that there is an a :: 'a and P a. > > Is there any way to state such a property in Isabelle? This is outside the expressiveness of HOL. > Another way of > thinking about this is that I want to state that there exists some > function of arity n, regardless of type, that has a certain property. You can prove the statement \<exists>f::'a1 => ... => 'an => 'b. P f However, in the proof you cannot make any additional assumptions about the type variables, in particular you cannot instantiate them. The only way in Isabelle/HOL to express types with certain properties are type-classes, which have several restrictions, e.g., they can only depend on one type variable. -- Peter

**Follow-Ups**:**Re: [isabelle] Isar polymorphism problem***From:*Makarius

**References**:**[isabelle] Isar polymorphism problem***From:*Edward Schwartz

**Re: [isabelle] Isar polymorphism problem***From:*Peter Lammich

- Previous by Date: [isabelle] ISABELLE WORKSHOP 2014 Call for submissions (Reminder)
- Next by Date: Re: [isabelle] Simpl References Reasoning
- Previous by Thread: Re: [isabelle] Isar polymorphism problem
- Next by Thread: Re: [isabelle] Isar polymorphism problem
- Cl-isabelle-users April 2014 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