[isabelle] Algebraic rule collections



Hi all,

in the context of
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2019-March/msg00017.html
(Conflicting rules in default simps vs. algebraic rule collections) I
revisited existing *_simps collections particulary in the HOL theories,
with the following insights:

* Collections mult_compare_simps and unit_simps seem to be never used
neither in the distro nor the AFP and hence I would suggest to remove them.

* There is the well-established chain ac_simps ⊆ algebra_simps ⊆
field_simps, which is also referenced in tutorials:

  * ac_simps for AC
  * algebra_simps for distributivity and such
  * field_simps with specific rules for division, preferring common
denominators.

* There are two somehow irregular variants:

  * divide_simps with more aggressive rewrites than field_simps wrt.
case distinctions
  * sign_simps introducing potential case splits on signs; this is
indeed quite old stuff dating back to at least 2f4be6844f7c in 2007,
which seems to have escaped any modernization or systematization so far,
but is used in a couple of places.

The rules in both these surely have their purpose, and it would be a
good idea to make them available more prominently.

So far my current thoughts on that:

a) The traditional chain is extended: ac_simps ⊆ algebra_simps ⊆
field_simps ⊆ field_split_simps, where field_split_simps adds the
potential case-splitting rules now in divide_simps and sign_simps.

b) I am a little bit uncomfortable with the well-established name
field_simps, though:

  * Most of its rules do not apply to fields but to the weaker
division_ring (which does not sound so odd for German speakers used to
think about »Körper« and »Schiefkörper«).

  * My original motivation was to find a collection to store some rules
about (partial) division in rings, and it is somehow strange that the
formally fitting collection is named after fields.

Hence suggestions for a better naming for field_simps and
field_split_simps are welcome.

Cheers,
	Florian

Attachment: signature.asc
Description: OpenPGP digital signature



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