Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Generalised congruence rewriting with the simp...


view this post on Zulip Email Gateway (Aug 22 2022 at 09:44):

From: Manuel Eberl <eberlm@in.tum.de>
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


Last updated: Mar 29 2024 at 08:18 UTC