Re: [isabelle] The type class for integer division

> Shall we do this, then? Must something else be done or checked first?

I don't see any obstacle except striving to be consistent, i.e.

Step 1: Re-Join comm_semiring_1_diff_distrib into comm_semiring_1
Step 2: Attach le_add_diff_inverse2 to linordered_semidom

and doing consecutive changes in the sources.

Hence we just state that our distribution's type classes demand a
partial inverse operation for addition with certain properties, beyond
what can be justified from the current specifications -- which is not
critical since these specifications are pragmatically developed and not
an exact counterpart of any development from literature.  If at some
time in the future this will expose problems, our system is flexible
enough to insert more intermediate points into the class hierarchy, even
within a particular application.


>> On 2 Jun 2015, at 20:49, Florian Haftmann <florian.haftmann at> wrote:
>>>> 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}")
>> 	Florian
>> -- 
>> PGP available:


PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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