*To*: Christian Sternagel <c.sternagel at gmail.com>*Subject*: Re: [isabelle] nat numerical constants simplifications*From*: Viorel Preoteasa <viorel.preoteasa at aalto.fi>*Date*: Tue, 28 Jan 2014 11:45:47 +0200*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <52E7782B.90308@gmail.com>*References*: <52E61A9F.6070201@inf.ethz.ch> <121E246E-27AA-4E99-BF04-87A3011FE7AE@aalto.fi> <52E7782B.90308@gmail.com>

Hi Chris, My context is more complicated than f … = f … I need to instantiate an assumption (forall n . …) with n, 1+n, 2+n, …, 10+n and among other things I get f (y (1 + n)) = 1 + f (y n) + 1 f (y (2 + n)) = 1 + f (y (1 + n)) + 1 … I need to get all these simplified to f (y (10 + n)) = f (y n) + 10 and ultimately prove f (y (10 + n)) >= 10 knowing that f (y n) >= 0. The problem occurred when using 3 + n which was not simplified anymore to Suc … . At first it seemed impossible to go forward, but then I remembered sledgehammer, and I used it. It suggested the lemma Suc3_eq_add_3. Using this lemma at the step (3+n), I could go forward. There were still some problems because I mixed (… + n) and (n + …), but then they were solved when changing everything to (… + n). Best regards, Viorel On 28 Jan 2014, at 11:28, Christian Sternagel <c.sternagel at gmail.com> wrote: > I would have suggested > > lemma "f (2 + (Suc n)) = f (3 + n)" > by (rule arg_cong) simp > > which works (thanks to backtracking?). Unfortunately, if you write the same as > > lemma "f (2 + (Suc n)) = f (3 + n)" > apply (rule arg_cong) > apply (simp) > done > > in order to see the intermediate results, the prove fails, since "apply (rule arg_cong)" does not change the goal. Is this intended? Is "rule" allowed to leave a goal unchanged? (Btw: a little instantiation helps, e.g., "apply (rule arg_cong [of _ _ f])"). > > 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:*Christian Sternagel

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

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

**Re: [isabelle] nat numerical constants simplifications***From:*Christian Sternagel

- Previous by Date: Re: [isabelle] nat numerical constants simplifications
- Next by Date: [isabelle] Avoiding foundational locale lemmas etc. in user space
- 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