Re: [isabelle] Isar polymorphism problem
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and