*To*: Mathias Fleury <mathias.fleury12 at gmail.com>*Subject*: Re: [isabelle] Cancellation simprocs*From*: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>*Date*: Sat, 4 Mar 2017 10:01:43 +0100*Cc*: Isabelle User <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <d7439ffe-4953-f125-18a7-6285875c61ea@gmail.com>*Organization*: TU Munich*References*: <cc5b9e49-8068-d9fc-ee11-b63deaeda102@gmail.com> <dd136cf4-2337-890f-5074-3808c059d652@informatik.tu-muenchen.de> <d7439ffe-4953-f125-18a7-6285875c61ea@gmail.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101 Thunderbird/45.7.0

Hi Matthias, > * the simprocs on natural numbers are crucial for the linarith, meaning > that even small differences can have huge consequences. > * LPS does not always do what people would expect, e.g. > ~~/HOL/ex/Simproc_Tests.thy: > (* FIXME "Suc (i + 3) \<equiv> i + 4" *) > assume "4 * Suc 0 + i = u" have "Suc (i + 3) = u" > by (tactic \<open>test @{context} [ at {simproc > nat_combine_numerals}]\<close>) fact > > If we want to replace LPS, should we aim at full compatibility to avoid > breaking proofs or try to fix the FIXMEs from Simproc_Test? linarith is indeed a world on its own and IMHO it would be OK if linarith would retain its current simproc, even if that is not used any where else. For a generalized simproc it would be fine if some proofs have to be amended, if the number of breaking proofs does not rise to high; this happens routinely when maintaining proof automation. The usual approach to figure out is: * Make the intended change. * See whether HOL can get run with reasonable effort. * Build as much as possible from distro and AFP. Iterate over breaking proofs. * Over time you get an idea what the impact of the change is: * How many breaking proofs? * How big is the amount of ÂawkwardÂ breaking proofs compared to ÂstreamlinedÂ breaking proofs? * Is there are recurring pattern how proofs can be repaired? * Is there yet another thing to change e.g. concerning the simplifier setup to get to a cleaner situation again? * â >> * Note that technically the cancellation simproc implementations are >> notoriously outdated; the state of the are is to implement such a >> simproc in a locale and then interpret it onto the desired instances. >> Detail can be found in Amine Chaieb and Makarius Wenzel: Context aware >> Calculation and Deduction --- Ring Equalities via GrÃbner Bases in >> Isabelle. And in src/HOL/Semiring_Normalization.thy > That should make the implementation a bit cleaner. I'll look into that. I'll appreciate that. Cheers, Florian > > > Best, > Mathias >> Best, >> Florian >> > > -- PGP available: http://isabelle.in.tum.de/~haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

**Attachment:
signature.asc**

**Follow-Ups**:**Re: [isabelle] Cancellation simprocs***From:*Lawrence Paulson

**References**:**Re: [isabelle] Cancellation simprocs***From:*Florian Haftmann

**Re: [isabelle] Cancellation simprocs***From:*Mathias Fleury

- Previous by Date: Re: [isabelle] isar in PIDE : strange behavior
- Next by Date: Re: [isabelle] Cancellation simprocs
- Previous by Thread: Re: [isabelle] Cancellation simprocs
- Next by Thread: Re: [isabelle] Cancellation simprocs
- Cl-isabelle-users March 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