*To*: Isabelle User <isabelle-users at cl.cam.ac.uk>*Subject*: [isabelle] Cancellation simprocs*From*: Mathias Fleury <mathias.fleury12 at gmail.com>*Date*: Fri, 24 Feb 2017 13:43:37 +0100*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.12; rv:45.0) Gecko/20100101 Thunderbird/45.7.1

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

- Previous by Date: Re: [isabelle] Formalization of soundness and completeness of natural deduction
- Next by Date: Re: [isabelle] newbie: Binomial extensions
- Previous by Thread: Re: [isabelle] Formalization of soundness and completeness of natural deduction
- Next by Thread: [isabelle] Call for participation: Workshop on Computer-aided Mathematical Proof, Cambridge UK, 10-14 July 2017
- Cl-isabelle-users February 2017 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list