Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Strange simplifier behaviour

Email Gateway (Aug 22 2022 at 09:13):

From: Makarius <makarius@sketis.net>
The isar-ref manual section "9.3.2 Declaring rules" provides a
specification of "simp" rules. There are also some explicit examples of
HO things that don't work, by the very construction of all this.

Makarius

Email Gateway (Aug 22 2022 at 09:20):

From: Manuel Eberl <eberlm@in.tum.de>
Hallo,

I found that the simplifier fails to apply certain simplification rules
when I would have expected it to. This occurs both in the development
version and Isabelle 2014. (see attachment)

I suspect it has something to do with higher-order unification. Is there
some kind of workaround?

Cheers,

Manuel
Foo.thy

Email Gateway (Aug 22 2022 at 09:23):

From: Tobias Nipkow <nipkow@in.tum.de>
On 01/04/2015 16:56, Manuel Eberl wrote:

Hallo,

I found that the simplifier fails to apply certain simplification rules
when I would have expected it to. This occurs both in the development
version and Isabelle 2014. (see attachment)

I suspect it has something to do with higher-order unification.

HO Matching. The simplifier only works reliably with higher-order patterns on
the left-hand side: free variables may only be applied to distinct bound variables.

Tobias

Is there
some kind of workaround?

Cheers,

Manuel

smime.p7s

Last updated: Apr 26 2024 at 08:19 UTC