[isabelle] Generalised congruence rewriting with the simplifier



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.