# Re: [isabelle] Problems with multiple patterns in simproc_setup

• To: cl-isabelle-users at lists.cam.ac.uk
• Subject: Re: [isabelle] Problems with multiple patterns in simproc_setup
• Date: Thu, 24 Oct 2019 13:59:51 +0200
• 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

Ok, thank you all for your replies. I see what is happening now. I'm just asking myself if this behavior is intended or "just came to be"? What I can say though is that it obviously wasn't the behavior I was expecting and as far as I can tell it is also not documented (although I'm
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"), 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 "(\i=1..3. i) = (\i=0..2. (i ::

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 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








• Follow-Ups:

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.