Re: [isabelle] Algebraic rule collections



After a second study, I recognized that the whole story is a little bit
more involved.

Concerning ac_simps ⊆ algebra_simps ⊆ field_simps – this inclusion does
just not hold:

a) ac_simps contains all kind of AC-rules (coprime, min, max, inf, sup,
…), but algebra_simps only those for + and *.

b) field_simps is no superset of algebra_simps, and in some sense they
work against each other:

	algebra_simps: (a + b) * c = a * c + b * c
		but not: (a + b) / c = a / c + b / c
	field_simps: a / c + b / c = (a + b) / c

It will need some further rounds of thinking to understand where to go
from here.

Cheers,
	Florian

Am 13.04.19 um 15:53 schrieb Florian Haftmann:
> 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.