# [isabelle] Generalised congruence rewriting with the simplifier

• To: isabelle-users at cl.cam.ac.uk
• Subject: [isabelle] Generalised congruence rewriting with the simplifier
• From: Manuel Eberl <eberlm at in.tum.de>
• Date: Sun, 03 May 2015 14:31:54 +0200
• User-agent: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Thunderbird/31.6.0

```Hallo,

I have a lemma that states that

f â Î(g) â L(f) = L(g)

I also have the following two rules on Î:

f â Î(g)
f1 â Î(g1) â f2 â Î(g2) â (Îx. f1 x * f2 x) â Î(Îx. g1 x * g2 x)

These rules together basically allow me to rewrite expressions of the
form "L(Îx. â * f x * â)" to "L(Îx. â * g x * â)" if I can show "f â
Î(g)", i.e. I can rewrite factors under a "L" individually and
independently.

I would like to get the simplifier to do this automatically, i.e.
whenever there is an expression of the form "L(Îx. f1 x * â * fk x)",
try to rewrite every factor individually by using the simp rules to find
an "fi" distinct from "gi" such that "fi â Î(gi)" and then rewriting the
factor "fi" to "gi".

For example, if I have a simp rule that states "(Î_. c) â Î(Îx. 1)", and
I have an expression like "L(Îx. x * 2 * x)", that should be rewritten
to "L(Îx. x * 1 * x)".

I could easily write a simproc that does that, but I wonder if this can
also be done in a more straightforward and scalable way, e.g. with
simp/cong rules.

Cheers,

Manuel

```

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