*To*: Christoph Madlener <madlener at in.tum.de>*Subject*: Re: [isabelle] Problems with multiple patterns in simproc_setup*From*: Mathias Fleury <mathias.fleury12 at gmail.com>*Date*: Thu, 24 Oct 2019 09:44:29 +0200*Cc*: Cl-isabelle Users <cl-isabelle-users at lists.cam.ac.uk>*In-reply-to*: <a32406e5ff6165f0aeba1885b148003e@in.tum.de>*References*: <a32406e5ff6165f0aeba1885b148003e@in.tum.de>

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 -- Mathias Fleury ENS Cachan - Antenne de Bretagne : ENS Rennes MIT 1 (Magister d'Informatique et Télécommunication) Université Rennes I - L3 R&I Recherche & Innovation + 33 (0) 6 04 15 87 93

**Follow-Ups**:**Re: [isabelle] Problems with multiple patterns in simproc_setup***From:*Tobias Nipkow

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

- Previous by Date: Re: [isabelle] primrec
- Next by Date: [isabelle] Proof checking in Isabelle
- Previous by Thread: [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