*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Problems with multiple patterns in simproc_setup*From*: Tobias Nipkow <nipkow at in.tum.de>*Date*: Thu, 24 Oct 2019 10:25:19 +0200*In-reply-to*: <CAG2fU9ixypTHE67Z6cSzio4==91Nq3mS=9rBb6vm0jfWjusVuA@mail.gmail.com>*References*: <a32406e5ff6165f0aeba1885b148003e@in.tum.de> <CAG2fU9ixypTHE67Z6cSzio4==91Nq3mS=9rBb6vm0jfWjusVuA@mail.gmail.com>*User-agent*: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.14; rv:68.0) Gecko/20100101 Thunderbird/68.1.2

Tobias On 24/10/2019 09:44, Mathias Fleury wrote:

Hi Christoph, The problem is type inference. With ("prod f A" | "sum f B"), f gets the type 'a::type ⇒ 'b::{comm_monoid_add,comm_monoid_mult}. However, in your lemmas, you get only either comm_monoid_add or comm_monoid_mult but not both. If you force the types to have both: lemma "(\<Sum>i=1..3. i) = (\<Sum>i=0..2. (i :: 'b::{zero,numeral,ord,comm_monoid_add,comm_monoid_mult}) + 1)" then the simproc triggers. The reason why [\<^term>\<open>prod f A\<close>, \<^term>\<open>sum f A\<close>] works is that the type inference is done separately in the two expressions instead of being done together. Best regards, Mathias Le jeu. 24 oct. 2019 à 09:30, Christoph Madlener <madlener at in.tum.de> a écrit :Hello, I am writing some simprocs and encountered a problem when using simproc_setup to install them. As you can see in the attached example, when multiple patterns for the simproc contain the same variable, the simproc isn't triggered for any of the given patterns. (I also encountered a case where the simproc was triggered for some, but not all given patterns) The problem can be avoided by either using unique identifiers, calling simproc_setup multiple times or using Simplifier.make_simproc - note that for the latter the patterns work as expected. I also attached an example with working solutions. Best regards, Christoph

**Attachment:
smime.p7s**

**Follow-Ups**:**Re: [isabelle] Problems with multiple patterns in simproc_setup***From:*lammich at in.tum.de

**References**:**[isabelle] Problems with multiple patterns in simproc_setup***From:*Christoph Madlener

**Re: [isabelle] Problems with multiple patterns in simproc_setup***From:*Mathias Fleury

- Previous by Date: [isabelle] Proof checking in Isabelle
- Next by Date: Re: [isabelle] Problems with multiple patterns in simproc_setup
- Previous by Thread: Re: [isabelle] Problems with multiple patterns in simproc_setup
- Next by Thread: Re: [isabelle] Problems with multiple patterns in simproc_setup
- Cl-isabelle-users October 2019 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