# [isabelle] Conditional simplification of constants

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

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