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
	Florian

-- 

Home:
http://www.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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