Re: [isabelle] Question about classes

Hi Viorel,

> I will also declare an uninterpreted constant
> consts
>  pair:: "'a => 'b => 'c::well_founded_transitive"
> instantiation "*":: (well_founded_transitive, well_founded_transitive)
> well_founded_transitive
> begin ...end
> axioms pair_def: "pair a b = (a, b)";
> I have tested this approach and it seems to work. I also
> think that I am not introducing inconsistencies, because
> I only introduce this axiom once after I instantiate
> the class for pairs.

Yes, since your axiom is nothing else than a definition -- a copy of
Pair :: 'a => 'b => 'a * 'b, essentially.  In that case you should use
the "overloading" target (see §5.7. of the Isabelle reference manual).

Hope this helps



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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