[isabelle] Cancellation simprocs

Hello list,

there are several simprocs that are able to cancel terms, i.e. simplify
"a + b + c = b + d" to "a + c = d".

Current problem: none of the simprocs is activated on
cancel_comm_monoid_add (i.e., the earliest point where the cancellation
is possible).

Here is the situation as far as I can tell:

	_L_arry _P_aulson's cancellation _s_improc on nat/int/...
	Brian Huffman's _G__r_oup cancellation _s_improc
	My _M_ultiset cancellation _s_improc
	My _G__e_neralised _m_ultiset cancellation _s_improc
used in this email
	- (2016-1 only) ~~/src/HOL/Library/multiset*.ML

	- (devel only) ~~/src/HOL/Library/Cancellation.thy
Works on:
	nat / int / ...
	cancel_comm_monoid_add, but activated only on groups
	cancel_comm_monoid_add, but activated only on multisets
cancel_comm_monoid_add, but activated only on multisets
Special feature
	- support the product
- does additional simplification on the output
	- support repeat_mset, replicate_mset,...
	- support an iterate_add operator (for multisets: repeat_mset,
replicate_mset,...; for natural numbers, it would be the product)

There are some points to notice:

(1) The aim behind generalising the MS to GeMS is to support multiset
variants with constructors and special operators (like signed multisets
in $AFP/Nested_Multisets_Ordinals/Signed_Multiset.thy). There might be
other types that have a operator that behaves like a multiplication by nat.

(2) We cannot activate the simprocs on cancel_comm_monoid_add.
Otherwise, tactics like linarith fails: linarith relies on the
additional simplification done by LPS (like replacing â-1 * xâ by â- xâ).

(3) I am not sure that GrS and GeMS do the exact same thing on the same

To solve the problem, I have locally activated GeMS where I have
hard-coded that the simproc does not apply on types where LPS applies.
It worked without problem. However, I am not sure that testing the AFP
and the Isabelle distribution is sufficient to declare that (3) does not
cause problems.

Does somebody have an opinion on the matter? Or should I just proceed
and activate my GeMS simproc on all cancel_comm_monoid_add types (except
those where LPS applies)?



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