*To*: Manuel Eberl <eberlm at in.tum.de>, "cl-isabelle-users at lists.cam.ac.uk" <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] Conditional simplification of constants*From*: Andreas Lochbihler <andreas.lochbihler at inf.ethz.ch>*Date*: Tue, 28 Apr 2015 17:55:56 +0200*In-reply-to*: <553FAAB5.5090809@in.tum.de>*References*: <553FAAB5.5090809@in.tum.de>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Thunderbird/31.6.0

Hi Manuel,

lemma f_const: "c ~= 0 ==> NO_MATCH (1 :: real) c ==> f (%_. c) = f (%_. 1)" Best, Andreas On 28/04/15 17:43, Manuel Eberl wrote:

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

**References**:**[isabelle] Conditional simplification of constants***From:*Manuel Eberl

- Previous by Date: Re: [isabelle] Reasoning with the option type
- Next by Date: Re: [isabelle] Reasoning with the option type
- Previous by Thread: [isabelle] Conditional simplification of constants
- Next by Thread: Re: [isabelle] Cl-isabelle-users Digest, Vol 118, Issue 47
- Cl-isabelle-users April 2015 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list