Re: [isabelle] The type class for integer division

>> We currently define the type class semiring_numeral_div in the theory
> Divides, see attached snippet below. This type class is already general
> enough to allow some facts involving linearly ordered arithmetic types
> to be proved just once and be valid over the range from nat to real. The
> only problem is that type real is not an instance of
> semiring_numeral_div, for obvious reasons. Would it not be appropriate
> to attach the axiom le_add_diff_inverse2 to a more general type class,
> such as linordered_semidom?
> this is surely something with can be taken into account.  I have
> recently refined the type class hierarchy to reflect the concept of
> Âpartial inverse additive operation up to a certain degree, and this
> could be the next step.

After a closer look at the whole matter, moving le_add_diff_inverse2 to
linordered_semidom seems reasonable (cf. class_deps "{linorder,
semiring, minus}")



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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