Re: [isabelle] Problems with multiple patterns in simproc_setup

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,

Le jeu. 24 oct. 2019 à 09:30, Christoph Madlener <madlener at> 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

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