[isabelle] Specification depends on extra type variables


I am trying to define a constant which depends on an extra type
variable. A simplified version of the definition looks like:

 "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:

 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:

 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.