# [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.*