*To*: cl-isabelle-users at lists.cam.ac.uk*Subject*: Re: [isabelle] nat numerical constants simplifications*From*: Christian Sternagel <c.sternagel at gmail.com>*Date*: Tue, 28 Jan 2014 10:28:11 +0100*In-reply-to*: <121E246E-27AA-4E99-BF04-87A3011FE7AE@aalto.fi>*References*: <52E61A9F.6070201@inf.ethz.ch> <121E246E-27AA-4E99-BF04-87A3011FE7AE@aalto.fi>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:24.0) Gecko/20100101 Thunderbird/24.2.0

I would have suggested lemma "f (2 + (Suc n)) = f (3 + n)" by (rule arg_cong) simp

lemma "f (2 + (Suc n)) = f (3 + n)" apply (rule arg_cong) apply (simp) done

cheers chris On 01/27/2014 03:56 PM, Viorel Preoteasa wrote:

I have the following two lemmas: lemma "(2 + (Suc n)) = (3 + n)" by simp lemma "f (2 + (Suc n)) = f (3 + n)" by simp The first one is proved by simp, but the proof on the second lemma fails. How can I simplify numerical constants in context? Best regards, Viorel Preoteasa

**Follow-Ups**:**Re: [isabelle] nat numerical constants simplifications***From:*Viorel Preoteasa

**References**:**[isabelle] Attributes use wrong context in lemma statement***From:*Andreas Lochbihler

**[isabelle] nat numerical constants simplifications***From:*Viorel Preoteasa

- Previous by Date: Re: [isabelle] Locales and bundles in Isabelle – a short comparion
- Next by Date: Re: [isabelle] nat numerical constants simplifications
- Previous by Thread: Re: [isabelle] nat numerical constants simplifications
- Next by Thread: Re: [isabelle] nat numerical constants simplifications
- Cl-isabelle-users January 2014 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