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.

--
  Peter







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