[isabelle] Locale typedef



Dear all,

I'm working in HOL-Algebra and I would like to share a problem. The
formalism of algebraic structures proposed by this library is very
comprehensive, because it deals with sets of a certain type instead of all
the elements of a given type, and properties for operations are defined on
those sets. The problem is that to have these properties we need always to
prove that the elements which we talk about belong to this set. As a
consequence, a big part of almost all the proofs are results of the kind "a
: carrier G ==> b : carrier G ==> a + b : carrier G".

If membership to this set was seen as a type, many proofs of this library
could be shorten, so I wonder if there ism't a way to do this (at least
inside a proof). I know some tools to declare new types, but none of them
could solve this particular issue. I heard that locale typedefs could do
the job, but I didn't find any tutorial. Does anyone of you know how they
work or where could I find documentation for those?

Cheers,

Paulo.



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