Re: [isabelle] Conditional simplification of constants

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)"


On 28/04/15 17:43, Manuel Eberl wrote:

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?


