*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] Problems with multiple patterns in simproc_setup*From*: Christoph Madlener <madlener at in.tum.de>*Date*: Thu, 24 Oct 2019 13:59:51 +0200*In-reply-to*: <-ggfyglniiu62-116s5a-s2kdo71cd0xw-px6bug-uksta0-gkdzqjpwu21jom7fts-f4zh7c-6uwj5v-x1q19x-9b2fcw-7pll1v-z36oo95keg82-fr1278-n1pouuxggg2syeyw8vkc0yarsojwle-22d0tp.1571906641749@email.android.com>*References*: <a32406e5ff6165f0aeba1885b148003e@in.tum.de> <CAG2fU9ixypTHE67Z6cSzio4==91Nq3mS=9rBb6vm0jfWjusVuA@mail.gmail.com> <8c6c2b3e-a99d-e5ca-e949-3a315750381d@in.tum.de> <-ggfyglniiu62-116s5a-s2kdo71cd0xw-px6bug-uksta0-gkdzqjpwu21jom7fts-f4zh7c-6uwj5v-x1q19x-9b2fcw-7pll1v-z36oo95keg82-fr1278-n1pouuxggg2syeyw8vkc0yarsojwle-22d0tp.1571906641749@email.android.com>*User-agent*: Roundcube Webmail/1.3.3

also not sure what a good place for this information would be). On 2019-10-24 10:44, lammich at in.tum.de wrote:

Another common beginner's trap is the simultaneous type inference on lemmas. At some point, you write down a list of statements in a single lemma. This perfectly makes sense if the statements are related and are proved with the same by (auto...) method. However it is all too easy to have such lemmas a less general type than intended, due to all statements being typed simultaneously. I still run into this trap occasionally... Peter -------- Original Message -------- Subject: Re: [isabelle] Problems with multiple patterns in simproc_setup From: Tobias Nipkow <nipkow at in.tum.de> To: cl-isabelle-users at lists.cam.ac.uk CC:This raises the question why type inference is applied to two alternative patterns simultaneously. Function definitions (fun in Isabelle) don't do that and it would be better if the simproc setup didn't do it either. Tobias On 24/10/2019 09:44, Mathias Fleury wrote:Hi Christoph, The problem is type inference. With ("prod f A" | "sum f B"), fgets thetype 'a::type ⇒ 'b::{comm_monoid_add,comm_monoid_mult}. However,in yourlemmas, you get only either comm_monoid_add or comm_monoid_multbut notboth. If you force the types to have both: lemma "(\i=1..3. i) = (\i=0..2. (i :: 'b::{zero,numeral,ord,comm_monoid_add,comm_monoid_mult}) + 1)" then the simproc triggers. The reason why [\\prod f A\, \\sum f A\] 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 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 attachedexample,when multiple patterns for the simproc contain the same variable,thesimproc isn't triggered for any of the given patterns. (I also encountered a case where the simproc was triggered for some, butnot allgiven patterns) The problem can be avoided by either using unique identifiers,callingsimproc_setup multiple times or using Simplifier.make_simproc -notethat for the latter the patterns work as expected. I alsoattached anexample with working solutions. Best regards, Christoph

**Follow-Ups**:

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

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

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

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

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