[isabelle] Conflicting rules in default simps vs. algebraic rule collections.



Hi all,

in private conversation Manuel has pointed out to me that there is a
potential conflict in simp rules.

Have a look at

* add_num_frac [field_simps]:
    y ≠ 0 ⟹ z + x / y = (x + z * y) / y
    (in class field)
* div_mult_self1 [simp]:
    b ≠ 0 ⟹ (a + c * b) div b = c + a div b
    (in class euclidean_semiring_cancel)

where it is important to know that »_ / _« and »_ div _« is just
different surface syntax for the same operator.

Under normal circumstances, there are no types which are both instances
of field and ring classes, hence there is no problem; but certain
algebra applications require theory HOL-Library.Field_as_Ring, which
makes the field type classes subclasses of corresponding ring classes.
Thus any »(simp add: field_simps)« operates with both simp rules from
above which are effectively symmetric to each other, which is not a good
idea. (There are other similar pairs around, but this only example is
enough to understand the problem).

Generally, the rules in »field_simps« are directed towards establishing
common denominators, which is maybe what they are exactly intended for.
Hence the orientation of add_num_frac is sensible in its particular
context and div_mult_self1 should not be a default simp rule any longer
(it has been made such by me some time ago, not being aware of the issue
mentioned above). But it (or its symmetric) should still be available in
a rule collection.

So which one?

* »algebra_simps« would be a fitting name but its rules currently do not
state anything about division, and I presume this is exactly the purpose
of it.
* »field_simps« would make semantically sense but the name would be
misleading since there is no field involved in the general case.
* »divide_simps« would be a quite fitting name, quoth Field.thy: ‹Lemmas
‹divide_simps› move division to the outside and eliminates them on
(in)equalities.›

I am currently inclined to pursue the latter option, which would also
suggest to generalize the relevant lemmas to a common ancestor type class.

Any further suggestions?

Cheers,
	Florian

Attachment: signature.asc
Description: OpenPGP digital signature



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