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

On 01/28/2014 10:45 AM, Viorel Preoteasa wrote:

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.

I see.

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

cheers chris

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

**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

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

- Previous by Date: [isabelle] formalising abstract machines
- Next by Date: Re: [isabelle] formalising abstract machines
- Previous by Thread: Re: [isabelle] nat numerical constants simplifications
- Next by Thread: [isabelle] TAP 2014: 2nd Call for Contributions
- 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