Re: [isabelle] The type class for integer division



Am 02.06.2015 um 21:49 schrieb Florian Haftmann:
>>> 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}")

After a third look, one caveat is whether there are instances of
linordered_semidom which do not satisfy le_add_diff_inverse2 (maybe
polynomials)?

This should be figured out first.  In the past I introduced e.g.
comm_semiring_1_diff_distrib since I saw no striking argument why a
partial subtraction in any case should follow a distributive law.  Maybe
this has been a little bit overcritical.

If we move on to attach le_add_diff_inverse2 to linordered_semidom, we
should also remerge comm_semiring_1_diff_distrib into comm_semiring_1

	Florian

-- 

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.