[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:

Simproc
	_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
Abbreviation
used in this email
	LPS
	GrS
	MS
	GeMS
file
	~~/src/Provers/Arith/cancel_numerals.ML
~~/Provers/Arith/cancel_numeral_factor.ML
	~~/src/HOL/Tools/group_cancel.ML
	- (2016-1 only) ~~/src/HOL/Library/multiset*.ML

	- (devel only) ~~/src/HOL/Library/Cancellation.thy
~~/src/HOL/Library/Cancellation/cancel*.ML
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
formula.


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)?


Best,

Mathias



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