Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Conditional simplification of constants


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

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

I have a constant f :: (real ⇒ real) ⇒ (real ⇒ real) set.

I also have the following lemma for the behaviour of f on constant
functions:

lemma f_const: "c ≠ 0 ⟹ f (λ_. c) = f(λ_. 1)"

I want to automatically normalise every term of the form "f (λ_. c)" to
"f (λ_. 1)" with the simplifier.
However, adding f_const to the simplifier does not work, because then
the simplifier will loop rewriting "f (λ_. 1)" to itself.

I therefore tried the following rule:

lemma f_const': "c ≠ 0 ⟹ c ≠ 1 ⟹ f (λ_. c) = f(λ_. 1)"

That seems to work better in the simpset, but the simplifier still
occasionally loops. Swapping "c ≠ 0" and "c ≠ 1" in the premises does
not seem to change that.

Is there a way to get the simplifier to only rewrite if "c" is not equal
to 1? (equal on the expression level, not the term level. Rewriting "f
(λ_. 0+1)" to "f (λ_. 1)" is fine, but rewriting "f (λ_. 1)" to "f (λ_.
1)" is not) Should I write a simproc to do this? Or is there a better way?

Cheers,

Manuel

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

From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Hi Manuel,

In Isabelle2015-RC*, there is the predicate NO_MATCH (defined in HOL.thy) that tests
whether a term does not match a pattern (implemented via a simproc). So you could write

lemma f_const: "c ~= 0 ==> NO_MATCH (1 :: real) c ==> f (%_. c) = f (%_. 1)"

Best,
Andreas


Last updated: Mar 28 2024 at 20:16 UTC