Re: [isabelle] Problems with multiple patterns in simproc_setup

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.


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,

Le jeu. 24 oct. 2019 à 09:30, Christoph Madlener <madlener at> a
écrit :


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,

Attachment: smime.p7s
Description: S/MIME Cryptographic Signature

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