# [isabelle] Specification depends on extra type variables

Hello,
I am trying to define a constant which depends on an extra type
variable. A simplified version of the definition looks like:
definition
"f a = (?g . !u . g u = a)";
I have found an answer to a similar question in the Isabelle archive
which suggests having a dummy parameter for f which gives the
missing type:
definition
f :: "'a => ('b itself) => bool" where
"f a x = (?g . !u . g (u::'b) = a)";
However like this I have to use x as parameter for f everywhere.
Moreover, I am defining Hoare triples for some kind of programs,
and I want to use the syntax "|- _ {| _ |} _", but with this approach
I need a place for the extra dummy parameter also.

`The fact is that the type 'b must be a type variable. I cannot
``instantiate it
`at this point.
Another approach which seem to work is by defining an uninterpreted
constant, and give its concrete definition using an axiom:
consts
f :: "'a => bool";
axioms f_def:
"f a = (? g . !u . g u = a)";
Is the axiomatic solution unsound?
Best regards,
Viorel Preoteasa

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